1***************************************************************************** 2 Semantic Analysis of SPARK Text 3 Examiner Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039 4 Copyright (C) 2010 Altran Praxis Limited, Bath, U.K. 5***************************************************************************** 6 7 8CREATED 29-NOV-2010, 14:30:19 SIMPLIFIED 29-NOV-2010, 14:30:21 9 10SPARK Simplifier Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039 11Copyright (C) 2010 Altran Praxis Limited, Bath, U.K. 12 13procedure RMD.Round 14 15 16 17 18For path(s) from start to run-time check associated with statement of line 111: 19 20procedure_round_1. 21*** true . /* all conclusions proved */ 22 23 24For path(s) from start to run-time check associated with statement of line 112: 25 26procedure_round_2. 27*** true . /* all conclusions proved */ 28 29 30For path(s) from start to run-time check associated with statement of line 113: 31 32procedure_round_3. 33*** true . /* all conclusions proved */ 34 35 36For path(s) from start to run-time check associated with statement of line 114: 37 38procedure_round_4. 39*** true . /* all conclusions proved */ 40 41 42For path(s) from start to run-time check associated with statement of line 115: 43 44procedure_round_5. 45*** true . /* all conclusions proved */ 46 47 48For path(s) from start to run-time check associated with statement of line 116: 49 50procedure_round_6. 51*** true . /* all conclusions proved */ 52 53 54For path(s) from start to run-time check associated with statement of line 117: 55 56procedure_round_7. 57*** true . /* all conclusions proved */ 58 59 60For path(s) from start to run-time check associated with statement of line 118: 61 62procedure_round_8. 63*** true . /* all conclusions proved */ 64 65 66For path(s) from start to run-time check associated with statement of line 119: 67 68procedure_round_9. 69*** true . /* all conclusions proved */ 70 71 72For path(s) from start to run-time check associated with statement of line 120: 73 74procedure_round_10. 75*** true . /* all conclusions proved */ 76 77 78For path(s) from start to run-time check associated with statement of line 121: 79 80procedure_round_11. 81*** true . /* all conclusions proved */ 82 83 84For path(s) from start to run-time check associated with statement of line 121: 85 86procedure_round_12. 87*** true . /* all conclusions proved */ 88 89 90For path(s) from start to run-time check associated with statement of line 124: 91 92procedure_round_13. 93*** true . /* all conclusions proved */ 94 95 96For path(s) from assertion of line 147 to run-time check associated with 97 statement of line 124: 98 99procedure_round_14. 100*** true . /* all conclusions proved */ 101 102 103For path(s) from start to run-time check associated with statement of line 124: 104 105procedure_round_15. 106*** true . /* all conclusions proved */ 107 108 109For path(s) from assertion of line 147 to run-time check associated with 110 statement of line 124: 111 112procedure_round_16. 113*** true . /* all conclusions proved */ 114 115 116For path(s) from start to run-time check associated with statement of line 124: 117 118procedure_round_17. 119*** true . /* all conclusions proved */ 120 121 122For path(s) from assertion of line 147 to run-time check associated with 123 statement of line 124: 124 125procedure_round_18. 126*** true . /* all conclusions proved */ 127 128 129For path(s) from start to run-time check associated with statement of line 124: 130 131procedure_round_19. 132*** true . /* all conclusions proved */ 133 134 135For path(s) from assertion of line 147 to run-time check associated with 136 statement of line 124: 137 138procedure_round_20. 139*** true . /* all conclusions proved */ 140 141 142For path(s) from start to run-time check associated with statement of line 124: 143 144procedure_round_21. 145*** true . /* all conclusions proved */ 146 147 148For path(s) from assertion of line 147 to run-time check associated with 149 statement of line 124: 150 151procedure_round_22. 152*** true . /* all conclusions proved */ 153 154 155For path(s) from start to run-time check associated with statement of line 124: 156 157procedure_round_23. 158*** true . /* all conclusions proved */ 159 160 161For path(s) from assertion of line 147 to run-time check associated with 162 statement of line 124: 163 164procedure_round_24. 165*** true . /* all conclusions proved */ 166 167 168For path(s) from start to run-time check associated with statement of line 130: 169 170procedure_round_25. 171*** true . /* all conclusions proved */ 172 173 174For path(s) from assertion of line 147 to run-time check associated with 175 statement of line 130: 176 177procedure_round_26. 178*** true . /* all conclusions proved */ 179 180 181For path(s) from start to run-time check associated with statement of line 131: 182 183procedure_round_27. 184*** true . /* all conclusions proved */ 185 186 187For path(s) from assertion of line 147 to run-time check associated with 188 statement of line 131: 189 190procedure_round_28. 191*** true . /* all conclusions proved */ 192 193 194For path(s) from start to run-time check associated with statement of line 132: 195 196procedure_round_29. 197*** true . /* all conclusions proved */ 198 199 200For path(s) from assertion of line 147 to run-time check associated with 201 statement of line 132: 202 203procedure_round_30. 204*** true . /* all conclusions proved */ 205 206 207For path(s) from start to run-time check associated with statement of line 132: 208 209procedure_round_31. 210*** true . /* all conclusions proved */ 211 212 213For path(s) from assertion of line 147 to run-time check associated with 214 statement of line 132: 215 216procedure_round_32. 217*** true . /* all conclusions proved */ 218 219 220For path(s) from start to run-time check associated with statement of line 133: 221 222procedure_round_33. 223*** true . /* all conclusions proved */ 224 225 226For path(s) from assertion of line 147 to run-time check associated with 227 statement of line 133: 228 229procedure_round_34. 230*** true . /* all conclusions proved */ 231 232 233For path(s) from start to run-time check associated with statement of line 134: 234 235procedure_round_35. 236*** true . /* all conclusions proved */ 237 238 239For path(s) from assertion of line 147 to run-time check associated with 240 statement of line 134: 241 242procedure_round_36. 243*** true . /* all conclusions proved */ 244 245 246For path(s) from start to run-time check associated with statement of line 136: 247 248procedure_round_37. 249*** true . /* all conclusions proved */ 250 251 252For path(s) from assertion of line 147 to run-time check associated with 253 statement of line 136: 254 255procedure_round_38. 256*** true . /* all conclusions proved */ 257 258 259For path(s) from start to run-time check associated with statement of line 136: 260 261procedure_round_39. 262*** true . /* all conclusions proved */ 263 264 265For path(s) from assertion of line 147 to run-time check associated with 266 statement of line 136: 267 268procedure_round_40. 269*** true . /* all conclusions proved */ 270 271 272For path(s) from start to run-time check associated with statement of line 136: 273 274procedure_round_41. 275*** true . /* all conclusions proved */ 276 277 278For path(s) from assertion of line 147 to run-time check associated with 279 statement of line 136: 280 281procedure_round_42. 282*** true . /* all conclusions proved */ 283 284 285For path(s) from start to run-time check associated with statement of line 136: 286 287procedure_round_43. 288*** true . /* all conclusions proved */ 289 290 291For path(s) from assertion of line 147 to run-time check associated with 292 statement of line 136: 293 294procedure_round_44. 295*** true . /* all conclusions proved */ 296 297 298For path(s) from start to run-time check associated with statement of line 136: 299 300procedure_round_45. 301*** true . /* all conclusions proved */ 302 303 304For path(s) from assertion of line 147 to run-time check associated with 305 statement of line 136: 306 307procedure_round_46. 308*** true . /* all conclusions proved */ 309 310 311For path(s) from start to run-time check associated with statement of line 136: 312 313procedure_round_47. 314*** true . /* all conclusions proved */ 315 316 317For path(s) from assertion of line 147 to run-time check associated with 318 statement of line 136: 319 320procedure_round_48. 321*** true . /* all conclusions proved */ 322 323 324For path(s) from start to run-time check associated with statement of line 142: 325 326procedure_round_49. 327*** true . /* all conclusions proved */ 328 329 330For path(s) from assertion of line 147 to run-time check associated with 331 statement of line 142: 332 333procedure_round_50. 334*** true . /* all conclusions proved */ 335 336 337For path(s) from start to run-time check associated with statement of line 143: 338 339procedure_round_51. 340*** true . /* all conclusions proved */ 341 342 343For path(s) from assertion of line 147 to run-time check associated with 344 statement of line 143: 345 346procedure_round_52. 347*** true . /* all conclusions proved */ 348 349 350For path(s) from start to run-time check associated with statement of line 144: 351 352procedure_round_53. 353*** true . /* all conclusions proved */ 354 355 356For path(s) from assertion of line 147 to run-time check associated with 357 statement of line 144: 358 359procedure_round_54. 360*** true . /* all conclusions proved */ 361 362 363For path(s) from start to run-time check associated with statement of line 144: 364 365procedure_round_55. 366*** true . /* all conclusions proved */ 367 368 369For path(s) from assertion of line 147 to run-time check associated with 370 statement of line 144: 371 372procedure_round_56. 373*** true . /* all conclusions proved */ 374 375 376For path(s) from start to run-time check associated with statement of line 145: 377 378procedure_round_57. 379*** true . /* all conclusions proved */ 380 381 382For path(s) from assertion of line 147 to run-time check associated with 383 statement of line 145: 384 385procedure_round_58. 386*** true . /* all conclusions proved */ 387 388 389For path(s) from start to run-time check associated with statement of line 146: 390 391procedure_round_59. 392*** true . /* all conclusions proved */ 393 394 395For path(s) from assertion of line 147 to run-time check associated with 396 statement of line 146: 397 398procedure_round_60. 399*** true . /* all conclusions proved */ 400 401 402For path(s) from start to assertion of line 147: 403 404procedure_round_61. 405H1: ca >= 0 . 406H2: ca <= 4294967295 . 407H3: cb >= 0 . 408H4: cb <= 4294967295 . 409H5: cc >= 0 . 410H6: cc <= 4294967295 . 411H7: cd >= 0 . 412H8: cd <= 4294967295 . 413H9: ce >= 0 . 414H10: ce <= 4294967295 . 415H11: for_all(i___1 : integer, 0 <= i___1 and i___1 <= 15 -> 0 <= element(x, [ 416 i___1]) and element(x, [i___1]) <= 4294967295) . 417H12: s_l(0) >= 0 . 418H13: s_l(0) <= 15 . 419H14: s_l(0) = s_l_spec(0) . 420H15: f(0, cb, cc, cd) >= 0 . 421H16: f(0, cb, cc, cd) <= 4294967295 . 422H17: f(0, cb, cc, cd) = f_spec(0, cb, cc, cd) . 423H18: r_l(0) >= 0 . 424H19: r_l(0) <= 15 . 425H20: r_l(0) = r_l_spec(0) . 426H21: k_l(0) >= 0 . 427H22: k_l(0) <= 4294967295 . 428H23: k_l(0) = k_l_spec(0) . 429H24: (((ca + f(0, cb, cc, cd)) mod 4294967296 + element(x, [r_l(0)])) mod 430 4294967296 + k_l(0)) mod 4294967296 >= 0 . 431H25: (((ca + f(0, cb, cc, cd)) mod 4294967296 + element(x, [r_l(0)])) mod 432 4294967296 + k_l(0)) mod 4294967296 <= 4294967295 . 433H26: wordops__rotate(s_l(0), (((ca + f(0, cb, cc, cd)) mod 4294967296 + 434 element(x, [r_l(0)])) mod 4294967296 + k_l(0)) mod 4294967296) >= 0 . 435H27: wordops__rotate(s_l(0), (((ca + f(0, cb, cc, cd)) mod 4294967296 + 436 element(x, [r_l(0)])) mod 4294967296 + k_l(0)) mod 4294967296) <= 437 4294967295 . 438H28: wordops__rotate(s_l(0), (((ca + f(0, cb, cc, cd)) mod 4294967296 + 439 element(x, [r_l(0)])) mod 4294967296 + k_l(0)) mod 4294967296) = 440 wordops__rotate_left(s_l(0), (((ca + f(0, cb, cc, cd)) mod 4294967296 441 + element(x, [r_l(0)])) mod 4294967296 + k_l(0)) mod 4294967296) . 442H29: (wordops__rotate(s_l(0), (((ca + f(0, cb, cc, cd)) mod 4294967296 + 443 element(x, [r_l(0)])) mod 4294967296 + k_l(0)) mod 4294967296) + ce) 444 mod 4294967296 >= 0 . 445H30: (wordops__rotate(s_l(0), (((ca + f(0, cb, cc, cd)) mod 4294967296 + 446 element(x, [r_l(0)])) mod 4294967296 + k_l(0)) mod 4294967296) + ce) 447 mod 4294967296 <= 4294967295 . 448H31: wordops__rotate(10, cc) >= 0 . 449H32: wordops__rotate(10, cc) <= 4294967295 . 450H33: wordops__rotate(10, cc) = wordops__rotate_left(10, cc) . 451H34: s_r(0) >= 0 . 452H35: s_r(0) <= 15 . 453H36: s_r(0) = s_r_spec(0) . 454H37: 79 >= round_index__base__first . 455H38: 79 <= round_index__base__last . 456H39: f(79, cb, cc, cd) >= 0 . 457H40: f(79, cb, cc, cd) <= 4294967295 . 458H41: f(79, cb, cc, cd) = f_spec(79, cb, cc, cd) . 459H42: r_r(0) >= 0 . 460H43: r_r(0) <= 15 . 461H44: r_r(0) = r_r_spec(0) . 462H45: k_r(0) >= 0 . 463H46: k_r(0) <= 4294967295 . 464H47: k_r(0) = k_r_spec(0) . 465H48: (((ca + f(79, cb, cc, cd)) mod 4294967296 + element(x, [r_r(0)])) mod 466 4294967296 + k_r(0)) mod 4294967296 >= 0 . 467H49: (((ca + f(79, cb, cc, cd)) mod 4294967296 + element(x, [r_r(0)])) mod 468 4294967296 + k_r(0)) mod 4294967296 <= 4294967295 . 469H50: wordops__rotate(s_r(0), (((ca + f(79, cb, cc, cd)) mod 4294967296 + 470 element(x, [r_r(0)])) mod 4294967296 + k_r(0)) mod 4294967296) >= 0 . 471H51: wordops__rotate(s_r(0), (((ca + f(79, cb, cc, cd)) mod 4294967296 + 472 element(x, [r_r(0)])) mod 4294967296 + k_r(0)) mod 4294967296) <= 473 4294967295 . 474H52: wordops__rotate(s_r(0), (((ca + f(79, cb, cc, cd)) mod 4294967296 + 475 element(x, [r_r(0)])) mod 4294967296 + k_r(0)) mod 4294967296) = 476 wordops__rotate_left(s_r(0), (((ca + f(79, cb, cc, cd)) mod 477 4294967296 + element(x, [r_r(0)])) mod 4294967296 + k_r(0)) mod 478 4294967296) . 479H53: (wordops__rotate(s_r(0), (((ca + f(79, cb, cc, cd)) mod 4294967296 + 480 element(x, [r_r(0)])) mod 4294967296 + k_r(0)) mod 4294967296) + ce) 481 mod 4294967296 >= 0 . 482H54: (wordops__rotate(s_r(0), (((ca + f(79, cb, cc, cd)) mod 4294967296 + 483 element(x, [r_r(0)])) mod 4294967296 + k_r(0)) mod 4294967296) + ce) 484 mod 4294967296 <= 4294967295 . 485H55: integer__size >= 0 . 486H56: interfaces__unsigned_32__size >= 0 . 487H57: wordops__word__size >= 0 . 488H58: wordops__rotate_amount__size >= 0 . 489H59: word__size >= 0 . 490H60: chain__size >= 0 . 491H61: block_index__size >= 0 . 492H62: block_index__base__first <= block_index__base__last . 493H63: round_index__size >= 0 . 494H64: round_index__base__first <= round_index__base__last . 495H65: chain_pair__size >= 0 . 496H66: rotate_amount__size >= 0 . 497H67: block_index__base__first <= 0 . 498H68: block_index__base__last >= 15 . 499H69: round_index__base__first <= 0 . 500H70: round_index__base__last >= 79 . 501 -> 502C1: mk__chain_pair(left := mk__chain(h0 := ce, h1 := (wordops__rotate(s_l(0) 503 , (((ca + f(0, cb, cc, cd)) mod 4294967296 + element(x, [r_l(0)])) 504 mod 4294967296 + k_l(0)) mod 4294967296) + ce) mod 4294967296, h2 := 505 cb, h3 := wordops__rotate(10, cc), h4 := cd), right := mk__chain(h0 506 := ce, h1 := (wordops__rotate(s_r(0), (((ca + f(79, cb, cc, cd)) mod 507 4294967296 + element(x, [r_r(0)])) mod 4294967296 + k_r(0)) mod 508 4294967296) + ce) mod 4294967296, h2 := cb, h3 := wordops__rotate(10, 509 cc), h4 := cd)) = steps(mk__chain_pair(left := mk__chain(h0 := ca, h1 510 := cb, h2 := cc, h3 := cd, h4 := ce), right := mk__chain(h0 := ca, h1 511 := cb, h2 := cc, h3 := cd, h4 := ce)), 1, x) . 512 513 514For path(s) from assertion of line 147 to assertion of line 147: 515 516procedure_round_62. 517H1: mk__chain_pair(left := mk__chain(h0 := cla, h1 := clb, h2 := clc, h3 := 518 cld, h4 := cle), right := mk__chain(h0 := cra, h1 := crb, h2 := crc, 519 h3 := crd, h4 := cre)) = steps(mk__chain_pair(left := mk__chain(h0 := 520 ca~, h1 := cb~, h2 := cc~, h3 := cd~, h4 := ce~), right := mk__chain( 521 h0 := ca~, h1 := cb~, h2 := cc~, h3 := cd~, h4 := ce~)), loop__1__j + 522 1, x) . 523H2: ca~ >= 0 . 524H3: ca~ <= 4294967295 . 525H4: cb~ >= 0 . 526H5: cb~ <= 4294967295 . 527H6: cc~ >= 0 . 528H7: cc~ <= 4294967295 . 529H8: cd~ >= 0 . 530H9: cd~ <= 4294967295 . 531H10: ce~ >= 0 . 532H11: ce~ <= 4294967295 . 533H12: for_all(i___1 : integer, 0 <= i___1 and i___1 <= 15 -> 0 <= element(x, [ 534 i___1]) and element(x, [i___1]) <= 4294967295) . 535H13: loop__1__j >= 0 . 536H14: loop__1__j <= 78 . 537H15: s_l(loop__1__j + 1) >= 0 . 538H16: s_l(loop__1__j + 1) <= 15 . 539H17: s_l(loop__1__j + 1) = s_l_spec(loop__1__j + 1) . 540H18: cla >= 0 . 541H19: cla <= 4294967295 . 542H20: clb >= 0 . 543H21: clb <= 4294967295 . 544H22: clc >= 0 . 545H23: clc <= 4294967295 . 546H24: cld >= 0 . 547H25: cld <= 4294967295 . 548H26: f(loop__1__j + 1, clb, clc, cld) >= 0 . 549H27: f(loop__1__j + 1, clb, clc, cld) <= 4294967295 . 550H28: f(loop__1__j + 1, clb, clc, cld) = f_spec(loop__1__j + 1, clb, clc, cld) 551 . 552H29: r_l(loop__1__j + 1) >= 0 . 553H30: r_l(loop__1__j + 1) <= 15 . 554H31: r_l(loop__1__j + 1) = r_l_spec(loop__1__j + 1) . 555H32: k_l(loop__1__j + 1) >= 0 . 556H33: k_l(loop__1__j + 1) <= 4294967295 . 557H34: k_l(loop__1__j + 1) = k_l_spec(loop__1__j + 1) . 558H35: (((cla + f(loop__1__j + 1, clb, clc, cld)) mod 4294967296 + element(x, [ 559 r_l(loop__1__j + 1)])) mod 4294967296 + k_l(loop__1__j + 1)) mod 560 4294967296 >= 0 . 561H36: (((cla + f(loop__1__j + 1, clb, clc, cld)) mod 4294967296 + element(x, [ 562 r_l(loop__1__j + 1)])) mod 4294967296 + k_l(loop__1__j + 1)) mod 563 4294967296 <= 4294967295 . 564H37: wordops__rotate(s_l(loop__1__j + 1), (((cla + f(loop__1__j + 1, clb, 565 clc, cld)) mod 4294967296 + element(x, [r_l(loop__1__j + 1)])) mod 566 4294967296 + k_l(loop__1__j + 1)) mod 4294967296) >= 0 . 567H38: wordops__rotate(s_l(loop__1__j + 1), (((cla + f(loop__1__j + 1, clb, 568 clc, cld)) mod 4294967296 + element(x, [r_l(loop__1__j + 1)])) mod 569 4294967296 + k_l(loop__1__j + 1)) mod 4294967296) <= 4294967295 . 570H39: wordops__rotate(s_l(loop__1__j + 1), (((cla + f(loop__1__j + 1, clb, 571 clc, cld)) mod 4294967296 + element(x, [r_l(loop__1__j + 1)])) mod 572 4294967296 + k_l(loop__1__j + 1)) mod 4294967296) = 573 wordops__rotate_left(s_l(loop__1__j + 1), (((cla + f(loop__1__j + 1, 574 clb, clc, cld)) mod 4294967296 + element(x, [r_l(loop__1__j + 1)])) 575 mod 4294967296 + k_l(loop__1__j + 1)) mod 4294967296) . 576H40: cle >= 0 . 577H41: cle <= 4294967295 . 578H42: (wordops__rotate(s_l(loop__1__j + 1), (((cla + f(loop__1__j + 1, clb, 579 clc, cld)) mod 4294967296 + element(x, [r_l(loop__1__j + 1)])) mod 580 4294967296 + k_l(loop__1__j + 1)) mod 4294967296) + cle) mod 581 4294967296 >= 0 . 582H43: (wordops__rotate(s_l(loop__1__j + 1), (((cla + f(loop__1__j + 1, clb, 583 clc, cld)) mod 4294967296 + element(x, [r_l(loop__1__j + 1)])) mod 584 4294967296 + k_l(loop__1__j + 1)) mod 4294967296) + cle) mod 585 4294967296 <= 4294967295 . 586H44: wordops__rotate(10, clc) >= 0 . 587H45: wordops__rotate(10, clc) <= 4294967295 . 588H46: wordops__rotate(10, clc) = wordops__rotate_left(10, clc) . 589H47: s_r(loop__1__j + 1) >= 0 . 590H48: s_r(loop__1__j + 1) <= 15 . 591H49: s_r(loop__1__j + 1) = s_r_spec(loop__1__j + 1) . 592H50: cra >= 0 . 593H51: cra <= 4294967295 . 594H52: crb >= 0 . 595H53: crb <= 4294967295 . 596H54: crc >= 0 . 597H55: crc <= 4294967295 . 598H56: crd >= 0 . 599H57: crd <= 4294967295 . 600H58: 79 - (loop__1__j + 1) >= round_index__base__first . 601H59: 79 - (loop__1__j + 1) <= round_index__base__last . 602H60: f(79 - (loop__1__j + 1), crb, crc, crd) >= 0 . 603H61: f(79 - (loop__1__j + 1), crb, crc, crd) <= 4294967295 . 604H62: f(78 - loop__1__j, crb, crc, crd) = f_spec(78 - loop__1__j, crb, crc, 605 crd) . 606H63: r_r(loop__1__j + 1) >= 0 . 607H64: r_r(loop__1__j + 1) <= 15 . 608H65: r_r(loop__1__j + 1) = r_r_spec(loop__1__j + 1) . 609H66: k_r(loop__1__j + 1) >= 0 . 610H67: k_r(loop__1__j + 1) <= 4294967295 . 611H68: k_r(loop__1__j + 1) = k_r_spec(loop__1__j + 1) . 612H69: (((cra + f(79 - (loop__1__j + 1), crb, crc, crd)) mod 4294967296 + 613 element(x, [r_r(loop__1__j + 1)])) mod 4294967296 + k_r(loop__1__j + 614 1)) mod 4294967296 >= 0 . 615H70: (((cra + f(79 - (loop__1__j + 1), crb, crc, crd)) mod 4294967296 + 616 element(x, [r_r(loop__1__j + 1)])) mod 4294967296 + k_r(loop__1__j + 617 1)) mod 4294967296 <= 4294967295 . 618H71: wordops__rotate(s_r(loop__1__j + 1), (((cra + f(79 - (loop__1__j + 1), 619 crb, crc, crd)) mod 4294967296 + element(x, [r_r(loop__1__j + 1)])) 620 mod 4294967296 + k_r(loop__1__j + 1)) mod 4294967296) >= 0 . 621H72: wordops__rotate(s_r(loop__1__j + 1), (((cra + f(79 - (loop__1__j + 1), 622 crb, crc, crd)) mod 4294967296 + element(x, [r_r(loop__1__j + 1)])) 623 mod 4294967296 + k_r(loop__1__j + 1)) mod 4294967296) <= 4294967295 . 624H73: wordops__rotate(s_r(loop__1__j + 1), (((cra + f(79 - (loop__1__j + 1), 625 crb, crc, crd)) mod 4294967296 + element(x, [r_r(loop__1__j + 1)])) 626 mod 4294967296 + k_r(loop__1__j + 1)) mod 4294967296) = 627 wordops__rotate_left(s_r(loop__1__j + 1), (((cra + f(79 - (loop__1__j 628 + 1), crb, crc, crd)) mod 4294967296 + element(x, [r_r(loop__1__j + 1) 629 ])) mod 4294967296 + k_r(loop__1__j + 1)) mod 4294967296) . 630H74: cre >= 0 . 631H75: cre <= 4294967295 . 632H76: (wordops__rotate(s_r(loop__1__j + 1), (((cra + f(79 - (loop__1__j + 1), 633 crb, crc, crd)) mod 4294967296 + element(x, [r_r(loop__1__j + 1)])) 634 mod 4294967296 + k_r(loop__1__j + 1)) mod 4294967296) + cre) mod 635 4294967296 >= 0 . 636H77: (wordops__rotate(s_r(loop__1__j + 1), (((cra + f(79 - (loop__1__j + 1), 637 crb, crc, crd)) mod 4294967296 + element(x, [r_r(loop__1__j + 1)])) 638 mod 4294967296 + k_r(loop__1__j + 1)) mod 4294967296) + cre) mod 639 4294967296 <= 4294967295 . 640H78: wordops__rotate(10, crc) >= 0 . 641H79: wordops__rotate(10, crc) <= 4294967295 . 642H80: wordops__rotate(10, crc) = wordops__rotate_left(10, crc) . 643H81: integer__size >= 0 . 644H82: interfaces__unsigned_32__size >= 0 . 645H83: wordops__word__size >= 0 . 646H84: wordops__rotate_amount__size >= 0 . 647H85: word__size >= 0 . 648H86: chain__size >= 0 . 649H87: block_index__size >= 0 . 650H88: block_index__base__first <= block_index__base__last . 651H89: round_index__size >= 0 . 652H90: round_index__base__first <= round_index__base__last . 653H91: chain_pair__size >= 0 . 654H92: rotate_amount__size >= 0 . 655H93: block_index__base__first <= 0 . 656H94: block_index__base__last >= 15 . 657H95: round_index__base__first <= 0 . 658H96: round_index__base__last >= 79 . 659 -> 660C1: mk__chain_pair(left := mk__chain(h0 := cle, h1 := (wordops__rotate(s_l( 661 loop__1__j + 1), (((cla + f(loop__1__j + 1, clb, clc, cld)) mod 662 4294967296 + element(x, [r_l(loop__1__j + 1)])) mod 4294967296 + k_l( 663 loop__1__j + 1)) mod 4294967296) + cle) mod 4294967296, h2 := clb, h3 664 := wordops__rotate(10, clc), h4 := cld), right := mk__chain(h0 := 665 cre, h1 := (wordops__rotate(s_r(loop__1__j + 1), (((cra + f(79 - ( 666 loop__1__j + 1), crb, crc, crd)) mod 4294967296 + element(x, [r_r( 667 loop__1__j + 1)])) mod 4294967296 + k_r(loop__1__j + 1)) mod 668 4294967296) + cre) mod 4294967296, h2 := crb, h3 := wordops__rotate( 669 10, crc), h4 := crd)) = steps(mk__chain_pair(left := mk__chain(h0 := 670 ca~, h1 := cb~, h2 := cc~, h3 := cd~, h4 := ce~), right := mk__chain( 671 h0 := ca~, h1 := cb~, h2 := cc~, h3 := cd~, h4 := ce~)), loop__1__j + 672 2, x) . 673 674 675For path(s) from start to run-time check associated with statement of line 153: 676 677procedure_round_63. 678*** true . /* all conclusions proved */ 679 680 681For path(s) from assertion of line 147 to run-time check associated with 682 statement of line 153: 683 684procedure_round_64. 685*** true . /* all conclusions proved */ 686 687 688For path(s) from start to run-time check associated with statement of line 154: 689 690procedure_round_65. 691*** true . /* all conclusions proved */ 692 693 694For path(s) from assertion of line 147 to run-time check associated with 695 statement of line 154: 696 697procedure_round_66. 698*** true . /* all conclusions proved */ 699 700 701For path(s) from start to run-time check associated with statement of line 155: 702 703procedure_round_67. 704*** true . /* all conclusions proved */ 705 706 707For path(s) from assertion of line 147 to run-time check associated with 708 statement of line 155: 709 710procedure_round_68. 711*** true . /* all conclusions proved */ 712 713 714For path(s) from start to run-time check associated with statement of line 156: 715 716procedure_round_69. 717*** true . /* all conclusions proved */ 718 719 720For path(s) from assertion of line 147 to run-time check associated with 721 statement of line 156: 722 723procedure_round_70. 724*** true . /* all conclusions proved */ 725 726 727For path(s) from start to run-time check associated with statement of line 157: 728 729procedure_round_71. 730*** true . /* all conclusions proved */ 731 732 733For path(s) from assertion of line 147 to run-time check associated with 734 statement of line 157: 735 736procedure_round_72. 737*** true . /* all conclusions proved */ 738 739 740For path(s) from start to run-time check associated with statement of line 158: 741 742procedure_round_73. 743*** true . /* all conclusions proved */ 744 745 746For path(s) from assertion of line 147 to run-time check associated with 747 statement of line 158: 748 749procedure_round_74. 750*** true . /* all conclusions proved */ 751 752 753For path(s) from start to finish: 754 755procedure_round_75. 756*** true . /* contradiction within hypotheses. */ 757 758 759 760For path(s) from assertion of line 147 to finish: 761 762procedure_round_76. 763H1: mk__chain_pair(left := mk__chain(h0 := cla, h1 := clb, h2 := clc, h3 := 764 cld, h4 := cle), right := mk__chain(h0 := cra, h1 := crb, h2 := crc, 765 h3 := crd, h4 := cre)) = steps(mk__chain_pair(left := mk__chain(h0 := 766 ca~, h1 := cb~, h2 := cc~, h3 := cd~, h4 := ce~), right := mk__chain( 767 h0 := ca~, h1 := cb~, h2 := cc~, h3 := cd~, h4 := ce~)), 80, x) . 768H2: ca~ >= 0 . 769H3: ca~ <= 4294967295 . 770H4: cb~ >= 0 . 771H5: cb~ <= 4294967295 . 772H6: cc~ >= 0 . 773H7: cc~ <= 4294967295 . 774H8: cd~ >= 0 . 775H9: cd~ <= 4294967295 . 776H10: ce~ >= 0 . 777H11: ce~ <= 4294967295 . 778H12: for_all(i___1 : integer, 0 <= i___1 and i___1 <= 15 -> 0 <= element(x, [ 779 i___1]) and element(x, [i___1]) <= 4294967295) . 780H13: clc >= 0 . 781H14: clc <= 4294967295 . 782H15: crd >= 0 . 783H16: crd <= 4294967295 . 784H17: ((cb~ + clc) mod 4294967296 + crd) mod 4294967296 >= 0 . 785H18: ((cb~ + clc) mod 4294967296 + crd) mod 4294967296 <= 4294967295 . 786H19: cld >= 0 . 787H20: cld <= 4294967295 . 788H21: cre >= 0 . 789H22: cre <= 4294967295 . 790H23: ((cc~ + cld) mod 4294967296 + cre) mod 4294967296 >= 0 . 791H24: ((cc~ + cld) mod 4294967296 + cre) mod 4294967296 <= 4294967295 . 792H25: cle >= 0 . 793H26: cle <= 4294967295 . 794H27: cra >= 0 . 795H28: cra <= 4294967295 . 796H29: ((cd~ + cle) mod 4294967296 + cra) mod 4294967296 >= 0 . 797H30: ((cd~ + cle) mod 4294967296 + cra) mod 4294967296 <= 4294967295 . 798H31: cla >= 0 . 799H32: cla <= 4294967295 . 800H33: crb >= 0 . 801H34: crb <= 4294967295 . 802H35: ((ce~ + cla) mod 4294967296 + crb) mod 4294967296 >= 0 . 803H36: ((ce~ + cla) mod 4294967296 + crb) mod 4294967296 <= 4294967295 . 804H37: clb >= 0 . 805H38: clb <= 4294967295 . 806H39: crc >= 0 . 807H40: crc <= 4294967295 . 808H41: ((ca~ + clb) mod 4294967296 + crc) mod 4294967296 >= 0 . 809H42: ((ca~ + clb) mod 4294967296 + crc) mod 4294967296 <= 4294967295 . 810H43: integer__size >= 0 . 811H44: interfaces__unsigned_32__size >= 0 . 812H45: wordops__word__size >= 0 . 813H46: wordops__rotate_amount__size >= 0 . 814H47: word__size >= 0 . 815H48: chain__size >= 0 . 816H49: block_index__size >= 0 . 817H50: block_index__base__first <= block_index__base__last . 818H51: round_index__size >= 0 . 819H52: round_index__base__first <= round_index__base__last . 820H53: chain_pair__size >= 0 . 821H54: rotate_amount__size >= 0 . 822H55: block_index__base__first <= 0 . 823H56: block_index__base__last >= 15 . 824H57: round_index__base__first <= 0 . 825H58: round_index__base__last >= 79 . 826 -> 827C1: mk__chain(h0 := ((cb~ + clc) mod 4294967296 + crd) mod 4294967296, h1 := 828 ((cc~ + cld) mod 4294967296 + cre) mod 4294967296, h2 := ((cd~ + cle) 829 mod 4294967296 + cra) mod 4294967296, h3 := ((ce~ + cla) mod 830 4294967296 + crb) mod 4294967296, h4 := ((ca~ + clb) mod 4294967296 + 831 crc) mod 4294967296) = round_spec(mk__chain(h0 := ca~, h1 := cb~, h2 832 := cc~, h3 := cd~, h4 := ce~), x) . 833 834 835