src/HOL/SPARK/Examples/RIPEMD-160/rmd/round.siv
changeset 41561 d1318f3c86ba
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/SPARK/Examples/RIPEMD-160/rmd/round.siv	Sat Jan 15 12:35:29 2011 +0100
     1.3 @@ -0,0 +1,834 @@
     1.4 +*****************************************************************************
     1.5 +                       Semantic Analysis of SPARK Text
     1.6 +    Examiner Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039
     1.7 +             Copyright (C) 2010 Altran Praxis Limited, Bath, U.K.
     1.8 +*****************************************************************************
     1.9 +
    1.10 +
    1.11 +CREATED 29-NOV-2010, 14:30:19  SIMPLIFIED 29-NOV-2010, 14:30:21
    1.12 +
    1.13 +SPARK Simplifier Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039
    1.14 +Copyright (C) 2010 Altran Praxis Limited, Bath, U.K.
    1.15 +
    1.16 +procedure RMD.Round
    1.17 +
    1.18 +
    1.19 +
    1.20 +
    1.21 +For path(s) from start to run-time check associated with statement of line 111:
    1.22 +
    1.23 +procedure_round_1.
    1.24 +*** true .          /* all conclusions proved */
    1.25 +
    1.26 +
    1.27 +For path(s) from start to run-time check associated with statement of line 112:
    1.28 +
    1.29 +procedure_round_2.
    1.30 +*** true .          /* all conclusions proved */
    1.31 +
    1.32 +
    1.33 +For path(s) from start to run-time check associated with statement of line 113:
    1.34 +
    1.35 +procedure_round_3.
    1.36 +*** true .          /* all conclusions proved */
    1.37 +
    1.38 +
    1.39 +For path(s) from start to run-time check associated with statement of line 114:
    1.40 +
    1.41 +procedure_round_4.
    1.42 +*** true .          /* all conclusions proved */
    1.43 +
    1.44 +
    1.45 +For path(s) from start to run-time check associated with statement of line 115:
    1.46 +
    1.47 +procedure_round_5.
    1.48 +*** true .          /* all conclusions proved */
    1.49 +
    1.50 +
    1.51 +For path(s) from start to run-time check associated with statement of line 116:
    1.52 +
    1.53 +procedure_round_6.
    1.54 +*** true .          /* all conclusions proved */
    1.55 +
    1.56 +
    1.57 +For path(s) from start to run-time check associated with statement of line 117:
    1.58 +
    1.59 +procedure_round_7.
    1.60 +*** true .          /* all conclusions proved */
    1.61 +
    1.62 +
    1.63 +For path(s) from start to run-time check associated with statement of line 118:
    1.64 +
    1.65 +procedure_round_8.
    1.66 +*** true .          /* all conclusions proved */
    1.67 +
    1.68 +
    1.69 +For path(s) from start to run-time check associated with statement of line 119:
    1.70 +
    1.71 +procedure_round_9.
    1.72 +*** true .          /* all conclusions proved */
    1.73 +
    1.74 +
    1.75 +For path(s) from start to run-time check associated with statement of line 120:
    1.76 +
    1.77 +procedure_round_10.
    1.78 +*** true .          /* all conclusions proved */
    1.79 +
    1.80 +
    1.81 +For path(s) from start to run-time check associated with statement of line 121:
    1.82 +
    1.83 +procedure_round_11.
    1.84 +*** true .          /* all conclusions proved */
    1.85 +
    1.86 +
    1.87 +For path(s) from start to run-time check associated with statement of line 121:
    1.88 +
    1.89 +procedure_round_12.
    1.90 +*** true .          /* all conclusions proved */
    1.91 +
    1.92 +
    1.93 +For path(s) from start to run-time check associated with statement of line 124:
    1.94 +
    1.95 +procedure_round_13.
    1.96 +*** true .          /* all conclusions proved */
    1.97 +
    1.98 +
    1.99 +For path(s) from assertion of line 147 to run-time check associated with 
   1.100 +          statement of line 124:
   1.101 +
   1.102 +procedure_round_14.
   1.103 +*** true .          /* all conclusions proved */
   1.104 +
   1.105 +
   1.106 +For path(s) from start to run-time check associated with statement of line 124:
   1.107 +
   1.108 +procedure_round_15.
   1.109 +*** true .          /* all conclusions proved */
   1.110 +
   1.111 +
   1.112 +For path(s) from assertion of line 147 to run-time check associated with 
   1.113 +          statement of line 124:
   1.114 +
   1.115 +procedure_round_16.
   1.116 +*** true .          /* all conclusions proved */
   1.117 +
   1.118 +
   1.119 +For path(s) from start to run-time check associated with statement of line 124:
   1.120 +
   1.121 +procedure_round_17.
   1.122 +*** true .          /* all conclusions proved */
   1.123 +
   1.124 +
   1.125 +For path(s) from assertion of line 147 to run-time check associated with 
   1.126 +          statement of line 124:
   1.127 +
   1.128 +procedure_round_18.
   1.129 +*** true .          /* all conclusions proved */
   1.130 +
   1.131 +
   1.132 +For path(s) from start to run-time check associated with statement of line 124:
   1.133 +
   1.134 +procedure_round_19.
   1.135 +*** true .          /* all conclusions proved */
   1.136 +
   1.137 +
   1.138 +For path(s) from assertion of line 147 to run-time check associated with 
   1.139 +          statement of line 124:
   1.140 +
   1.141 +procedure_round_20.
   1.142 +*** true .          /* all conclusions proved */
   1.143 +
   1.144 +
   1.145 +For path(s) from start to run-time check associated with statement of line 124:
   1.146 +
   1.147 +procedure_round_21.
   1.148 +*** true .          /* all conclusions proved */
   1.149 +
   1.150 +
   1.151 +For path(s) from assertion of line 147 to run-time check associated with 
   1.152 +          statement of line 124:
   1.153 +
   1.154 +procedure_round_22.
   1.155 +*** true .          /* all conclusions proved */
   1.156 +
   1.157 +
   1.158 +For path(s) from start to run-time check associated with statement of line 124:
   1.159 +
   1.160 +procedure_round_23.
   1.161 +*** true .          /* all conclusions proved */
   1.162 +
   1.163 +
   1.164 +For path(s) from assertion of line 147 to run-time check associated with 
   1.165 +          statement of line 124:
   1.166 +
   1.167 +procedure_round_24.
   1.168 +*** true .          /* all conclusions proved */
   1.169 +
   1.170 +
   1.171 +For path(s) from start to run-time check associated with statement of line 130:
   1.172 +
   1.173 +procedure_round_25.
   1.174 +*** true .          /* all conclusions proved */
   1.175 +
   1.176 +
   1.177 +For path(s) from assertion of line 147 to run-time check associated with 
   1.178 +          statement of line 130:
   1.179 +
   1.180 +procedure_round_26.
   1.181 +*** true .          /* all conclusions proved */
   1.182 +
   1.183 +
   1.184 +For path(s) from start to run-time check associated with statement of line 131:
   1.185 +
   1.186 +procedure_round_27.
   1.187 +*** true .          /* all conclusions proved */
   1.188 +
   1.189 +
   1.190 +For path(s) from assertion of line 147 to run-time check associated with 
   1.191 +          statement of line 131:
   1.192 +
   1.193 +procedure_round_28.
   1.194 +*** true .          /* all conclusions proved */
   1.195 +
   1.196 +
   1.197 +For path(s) from start to run-time check associated with statement of line 132:
   1.198 +
   1.199 +procedure_round_29.
   1.200 +*** true .          /* all conclusions proved */
   1.201 +
   1.202 +
   1.203 +For path(s) from assertion of line 147 to run-time check associated with 
   1.204 +          statement of line 132:
   1.205 +
   1.206 +procedure_round_30.
   1.207 +*** true .          /* all conclusions proved */
   1.208 +
   1.209 +
   1.210 +For path(s) from start to run-time check associated with statement of line 132:
   1.211 +
   1.212 +procedure_round_31.
   1.213 +*** true .          /* all conclusions proved */
   1.214 +
   1.215 +
   1.216 +For path(s) from assertion of line 147 to run-time check associated with 
   1.217 +          statement of line 132:
   1.218 +
   1.219 +procedure_round_32.
   1.220 +*** true .          /* all conclusions proved */
   1.221 +
   1.222 +
   1.223 +For path(s) from start to run-time check associated with statement of line 133:
   1.224 +
   1.225 +procedure_round_33.
   1.226 +*** true .          /* all conclusions proved */
   1.227 +
   1.228 +
   1.229 +For path(s) from assertion of line 147 to run-time check associated with 
   1.230 +          statement of line 133:
   1.231 +
   1.232 +procedure_round_34.
   1.233 +*** true .          /* all conclusions proved */
   1.234 +
   1.235 +
   1.236 +For path(s) from start to run-time check associated with statement of line 134:
   1.237 +
   1.238 +procedure_round_35.
   1.239 +*** true .          /* all conclusions proved */
   1.240 +
   1.241 +
   1.242 +For path(s) from assertion of line 147 to run-time check associated with 
   1.243 +          statement of line 134:
   1.244 +
   1.245 +procedure_round_36.
   1.246 +*** true .          /* all conclusions proved */
   1.247 +
   1.248 +
   1.249 +For path(s) from start to run-time check associated with statement of line 136:
   1.250 +
   1.251 +procedure_round_37.
   1.252 +*** true .          /* all conclusions proved */
   1.253 +
   1.254 +
   1.255 +For path(s) from assertion of line 147 to run-time check associated with 
   1.256 +          statement of line 136:
   1.257 +
   1.258 +procedure_round_38.
   1.259 +*** true .          /* all conclusions proved */
   1.260 +
   1.261 +
   1.262 +For path(s) from start to run-time check associated with statement of line 136:
   1.263 +
   1.264 +procedure_round_39.
   1.265 +*** true .          /* all conclusions proved */
   1.266 +
   1.267 +
   1.268 +For path(s) from assertion of line 147 to run-time check associated with 
   1.269 +          statement of line 136:
   1.270 +
   1.271 +procedure_round_40.
   1.272 +*** true .          /* all conclusions proved */
   1.273 +
   1.274 +
   1.275 +For path(s) from start to run-time check associated with statement of line 136:
   1.276 +
   1.277 +procedure_round_41.
   1.278 +*** true .          /* all conclusions proved */
   1.279 +
   1.280 +
   1.281 +For path(s) from assertion of line 147 to run-time check associated with 
   1.282 +          statement of line 136:
   1.283 +
   1.284 +procedure_round_42.
   1.285 +*** true .          /* all conclusions proved */
   1.286 +
   1.287 +
   1.288 +For path(s) from start to run-time check associated with statement of line 136:
   1.289 +
   1.290 +procedure_round_43.
   1.291 +*** true .          /* all conclusions proved */
   1.292 +
   1.293 +
   1.294 +For path(s) from assertion of line 147 to run-time check associated with 
   1.295 +          statement of line 136:
   1.296 +
   1.297 +procedure_round_44.
   1.298 +*** true .          /* all conclusions proved */
   1.299 +
   1.300 +
   1.301 +For path(s) from start to run-time check associated with statement of line 136:
   1.302 +
   1.303 +procedure_round_45.
   1.304 +*** true .          /* all conclusions proved */
   1.305 +
   1.306 +
   1.307 +For path(s) from assertion of line 147 to run-time check associated with 
   1.308 +          statement of line 136:
   1.309 +
   1.310 +procedure_round_46.
   1.311 +*** true .          /* all conclusions proved */
   1.312 +
   1.313 +
   1.314 +For path(s) from start to run-time check associated with statement of line 136:
   1.315 +
   1.316 +procedure_round_47.
   1.317 +*** true .          /* all conclusions proved */
   1.318 +
   1.319 +
   1.320 +For path(s) from assertion of line 147 to run-time check associated with 
   1.321 +          statement of line 136:
   1.322 +
   1.323 +procedure_round_48.
   1.324 +*** true .          /* all conclusions proved */
   1.325 +
   1.326 +
   1.327 +For path(s) from start to run-time check associated with statement of line 142:
   1.328 +
   1.329 +procedure_round_49.
   1.330 +*** true .          /* all conclusions proved */
   1.331 +
   1.332 +
   1.333 +For path(s) from assertion of line 147 to run-time check associated with 
   1.334 +          statement of line 142:
   1.335 +
   1.336 +procedure_round_50.
   1.337 +*** true .          /* all conclusions proved */
   1.338 +
   1.339 +
   1.340 +For path(s) from start to run-time check associated with statement of line 143:
   1.341 +
   1.342 +procedure_round_51.
   1.343 +*** true .          /* all conclusions proved */
   1.344 +
   1.345 +
   1.346 +For path(s) from assertion of line 147 to run-time check associated with 
   1.347 +          statement of line 143:
   1.348 +
   1.349 +procedure_round_52.
   1.350 +*** true .          /* all conclusions proved */
   1.351 +
   1.352 +
   1.353 +For path(s) from start to run-time check associated with statement of line 144:
   1.354 +
   1.355 +procedure_round_53.
   1.356 +*** true .          /* all conclusions proved */
   1.357 +
   1.358 +
   1.359 +For path(s) from assertion of line 147 to run-time check associated with 
   1.360 +          statement of line 144:
   1.361 +
   1.362 +procedure_round_54.
   1.363 +*** true .          /* all conclusions proved */
   1.364 +
   1.365 +
   1.366 +For path(s) from start to run-time check associated with statement of line 144:
   1.367 +
   1.368 +procedure_round_55.
   1.369 +*** true .          /* all conclusions proved */
   1.370 +
   1.371 +
   1.372 +For path(s) from assertion of line 147 to run-time check associated with 
   1.373 +          statement of line 144:
   1.374 +
   1.375 +procedure_round_56.
   1.376 +*** true .          /* all conclusions proved */
   1.377 +
   1.378 +
   1.379 +For path(s) from start to run-time check associated with statement of line 145:
   1.380 +
   1.381 +procedure_round_57.
   1.382 +*** true .          /* all conclusions proved */
   1.383 +
   1.384 +
   1.385 +For path(s) from assertion of line 147 to run-time check associated with 
   1.386 +          statement of line 145:
   1.387 +
   1.388 +procedure_round_58.
   1.389 +*** true .          /* all conclusions proved */
   1.390 +
   1.391 +
   1.392 +For path(s) from start to run-time check associated with statement of line 146:
   1.393 +
   1.394 +procedure_round_59.
   1.395 +*** true .          /* all conclusions proved */
   1.396 +
   1.397 +
   1.398 +For path(s) from assertion of line 147 to run-time check associated with 
   1.399 +          statement of line 146:
   1.400 +
   1.401 +procedure_round_60.
   1.402 +*** true .          /* all conclusions proved */
   1.403 +
   1.404 +
   1.405 +For path(s) from start to assertion of line 147:
   1.406 +
   1.407 +procedure_round_61.
   1.408 +H1:    ca >= 0 .
   1.409 +H2:    ca <= 4294967295 .
   1.410 +H3:    cb >= 0 .
   1.411 +H4:    cb <= 4294967295 .
   1.412 +H5:    cc >= 0 .
   1.413 +H6:    cc <= 4294967295 .
   1.414 +H7:    cd >= 0 .
   1.415 +H8:    cd <= 4294967295 .
   1.416 +H9:    ce >= 0 .
   1.417 +H10:   ce <= 4294967295 .
   1.418 +H11:   for_all(i___1 : integer, 0 <= i___1 and i___1 <= 15 -> 0 <= element(x, [
   1.419 +          i___1]) and element(x, [i___1]) <= 4294967295) .
   1.420 +H12:   s_l(0) >= 0 .
   1.421 +H13:   s_l(0) <= 15 .
   1.422 +H14:   s_l(0) = s_l_spec(0) .
   1.423 +H15:   f(0, cb, cc, cd) >= 0 .
   1.424 +H16:   f(0, cb, cc, cd) <= 4294967295 .
   1.425 +H17:   f(0, cb, cc, cd) = f_spec(0, cb, cc, cd) .
   1.426 +H18:   r_l(0) >= 0 .
   1.427 +H19:   r_l(0) <= 15 .
   1.428 +H20:   r_l(0) = r_l_spec(0) .
   1.429 +H21:   k_l(0) >= 0 .
   1.430 +H22:   k_l(0) <= 4294967295 .
   1.431 +H23:   k_l(0) = k_l_spec(0) .
   1.432 +H24:   (((ca + f(0, cb, cc, cd)) mod 4294967296 + element(x, [r_l(0)])) mod 
   1.433 +          4294967296 + k_l(0)) mod 4294967296 >= 0 .
   1.434 +H25:   (((ca + f(0, cb, cc, cd)) mod 4294967296 + element(x, [r_l(0)])) mod 
   1.435 +          4294967296 + k_l(0)) mod 4294967296 <= 4294967295 .
   1.436 +H26:   wordops__rotate(s_l(0), (((ca + f(0, cb, cc, cd)) mod 4294967296 + 
   1.437 +          element(x, [r_l(0)])) mod 4294967296 + k_l(0)) mod 4294967296) >= 0 .
   1.438 +H27:   wordops__rotate(s_l(0), (((ca + f(0, cb, cc, cd)) mod 4294967296 + 
   1.439 +          element(x, [r_l(0)])) mod 4294967296 + k_l(0)) mod 4294967296) <= 
   1.440 +          4294967295 .
   1.441 +H28:   wordops__rotate(s_l(0), (((ca + f(0, cb, cc, cd)) mod 4294967296 + 
   1.442 +          element(x, [r_l(0)])) mod 4294967296 + k_l(0)) mod 4294967296) = 
   1.443 +          wordops__rotate_left(s_l(0), (((ca + f(0, cb, cc, cd)) mod 4294967296 
   1.444 +          + element(x, [r_l(0)])) mod 4294967296 + k_l(0)) mod 4294967296) .
   1.445 +H29:   (wordops__rotate(s_l(0), (((ca + f(0, cb, cc, cd)) mod 4294967296 + 
   1.446 +          element(x, [r_l(0)])) mod 4294967296 + k_l(0)) mod 4294967296) + ce) 
   1.447 +          mod 4294967296 >= 0 .
   1.448 +H30:   (wordops__rotate(s_l(0), (((ca + f(0, cb, cc, cd)) mod 4294967296 + 
   1.449 +          element(x, [r_l(0)])) mod 4294967296 + k_l(0)) mod 4294967296) + ce) 
   1.450 +          mod 4294967296 <= 4294967295 .
   1.451 +H31:   wordops__rotate(10, cc) >= 0 .
   1.452 +H32:   wordops__rotate(10, cc) <= 4294967295 .
   1.453 +H33:   wordops__rotate(10, cc) = wordops__rotate_left(10, cc) .
   1.454 +H34:   s_r(0) >= 0 .
   1.455 +H35:   s_r(0) <= 15 .
   1.456 +H36:   s_r(0) = s_r_spec(0) .
   1.457 +H37:   79 >= round_index__base__first .
   1.458 +H38:   79 <= round_index__base__last .
   1.459 +H39:   f(79, cb, cc, cd) >= 0 .
   1.460 +H40:   f(79, cb, cc, cd) <= 4294967295 .
   1.461 +H41:   f(79, cb, cc, cd) = f_spec(79, cb, cc, cd) .
   1.462 +H42:   r_r(0) >= 0 .
   1.463 +H43:   r_r(0) <= 15 .
   1.464 +H44:   r_r(0) = r_r_spec(0) .
   1.465 +H45:   k_r(0) >= 0 .
   1.466 +H46:   k_r(0) <= 4294967295 .
   1.467 +H47:   k_r(0) = k_r_spec(0) .
   1.468 +H48:   (((ca + f(79, cb, cc, cd)) mod 4294967296 + element(x, [r_r(0)])) mod 
   1.469 +          4294967296 + k_r(0)) mod 4294967296 >= 0 .
   1.470 +H49:   (((ca + f(79, cb, cc, cd)) mod 4294967296 + element(x, [r_r(0)])) mod 
   1.471 +          4294967296 + k_r(0)) mod 4294967296 <= 4294967295 .
   1.472 +H50:   wordops__rotate(s_r(0), (((ca + f(79, cb, cc, cd)) mod 4294967296 + 
   1.473 +          element(x, [r_r(0)])) mod 4294967296 + k_r(0)) mod 4294967296) >= 0 .
   1.474 +H51:   wordops__rotate(s_r(0), (((ca + f(79, cb, cc, cd)) mod 4294967296 + 
   1.475 +          element(x, [r_r(0)])) mod 4294967296 + k_r(0)) mod 4294967296) <= 
   1.476 +          4294967295 .
   1.477 +H52:   wordops__rotate(s_r(0), (((ca + f(79, cb, cc, cd)) mod 4294967296 + 
   1.478 +          element(x, [r_r(0)])) mod 4294967296 + k_r(0)) mod 4294967296) = 
   1.479 +          wordops__rotate_left(s_r(0), (((ca + f(79, cb, cc, cd)) mod 
   1.480 +          4294967296 + element(x, [r_r(0)])) mod 4294967296 + k_r(0)) mod 
   1.481 +          4294967296) .
   1.482 +H53:   (wordops__rotate(s_r(0), (((ca + f(79, cb, cc, cd)) mod 4294967296 + 
   1.483 +          element(x, [r_r(0)])) mod 4294967296 + k_r(0)) mod 4294967296) + ce) 
   1.484 +          mod 4294967296 >= 0 .
   1.485 +H54:   (wordops__rotate(s_r(0), (((ca + f(79, cb, cc, cd)) mod 4294967296 + 
   1.486 +          element(x, [r_r(0)])) mod 4294967296 + k_r(0)) mod 4294967296) + ce) 
   1.487 +          mod 4294967296 <= 4294967295 .
   1.488 +H55:   integer__size >= 0 .
   1.489 +H56:   interfaces__unsigned_32__size >= 0 .
   1.490 +H57:   wordops__word__size >= 0 .
   1.491 +H58:   wordops__rotate_amount__size >= 0 .
   1.492 +H59:   word__size >= 0 .
   1.493 +H60:   chain__size >= 0 .
   1.494 +H61:   block_index__size >= 0 .
   1.495 +H62:   block_index__base__first <= block_index__base__last .
   1.496 +H63:   round_index__size >= 0 .
   1.497 +H64:   round_index__base__first <= round_index__base__last .
   1.498 +H65:   chain_pair__size >= 0 .
   1.499 +H66:   rotate_amount__size >= 0 .
   1.500 +H67:   block_index__base__first <= 0 .
   1.501 +H68:   block_index__base__last >= 15 .
   1.502 +H69:   round_index__base__first <= 0 .
   1.503 +H70:   round_index__base__last >= 79 .
   1.504 +       ->
   1.505 +C1:    mk__chain_pair(left := mk__chain(h0 := ce, h1 := (wordops__rotate(s_l(0)
   1.506 +          , (((ca + f(0, cb, cc, cd)) mod 4294967296 + element(x, [r_l(0)])) 
   1.507 +          mod 4294967296 + k_l(0)) mod 4294967296) + ce) mod 4294967296, h2 := 
   1.508 +          cb, h3 := wordops__rotate(10, cc), h4 := cd), right := mk__chain(h0 
   1.509 +          := ce, h1 := (wordops__rotate(s_r(0), (((ca + f(79, cb, cc, cd)) mod 
   1.510 +          4294967296 + element(x, [r_r(0)])) mod 4294967296 + k_r(0)) mod 
   1.511 +          4294967296) + ce) mod 4294967296, h2 := cb, h3 := wordops__rotate(10, 
   1.512 +          cc), h4 := cd)) = steps(mk__chain_pair(left := mk__chain(h0 := ca, h1 
   1.513 +          := cb, h2 := cc, h3 := cd, h4 := ce), right := mk__chain(h0 := ca, h1 
   1.514 +          := cb, h2 := cc, h3 := cd, h4 := ce)), 1, x) .
   1.515 +
   1.516 +
   1.517 +For path(s) from assertion of line 147 to assertion of line 147:
   1.518 +
   1.519 +procedure_round_62.
   1.520 +H1:    mk__chain_pair(left := mk__chain(h0 := cla, h1 := clb, h2 := clc, h3 := 
   1.521 +          cld, h4 := cle), right := mk__chain(h0 := cra, h1 := crb, h2 := crc, 
   1.522 +          h3 := crd, h4 := cre)) = steps(mk__chain_pair(left := mk__chain(h0 := 
   1.523 +          ca~, h1 := cb~, h2 := cc~, h3 := cd~, h4 := ce~), right := mk__chain(
   1.524 +          h0 := ca~, h1 := cb~, h2 := cc~, h3 := cd~, h4 := ce~)), loop__1__j + 
   1.525 +          1, x) .
   1.526 +H2:    ca~ >= 0 .
   1.527 +H3:    ca~ <= 4294967295 .
   1.528 +H4:    cb~ >= 0 .
   1.529 +H5:    cb~ <= 4294967295 .
   1.530 +H6:    cc~ >= 0 .
   1.531 +H7:    cc~ <= 4294967295 .
   1.532 +H8:    cd~ >= 0 .
   1.533 +H9:    cd~ <= 4294967295 .
   1.534 +H10:   ce~ >= 0 .
   1.535 +H11:   ce~ <= 4294967295 .
   1.536 +H12:   for_all(i___1 : integer, 0 <= i___1 and i___1 <= 15 -> 0 <= element(x, [
   1.537 +          i___1]) and element(x, [i___1]) <= 4294967295) .
   1.538 +H13:   loop__1__j >= 0 .
   1.539 +H14:   loop__1__j <= 78 .
   1.540 +H15:   s_l(loop__1__j + 1) >= 0 .
   1.541 +H16:   s_l(loop__1__j + 1) <= 15 .
   1.542 +H17:   s_l(loop__1__j + 1) = s_l_spec(loop__1__j + 1) .
   1.543 +H18:   cla >= 0 .
   1.544 +H19:   cla <= 4294967295 .
   1.545 +H20:   clb >= 0 .
   1.546 +H21:   clb <= 4294967295 .
   1.547 +H22:   clc >= 0 .
   1.548 +H23:   clc <= 4294967295 .
   1.549 +H24:   cld >= 0 .
   1.550 +H25:   cld <= 4294967295 .
   1.551 +H26:   f(loop__1__j + 1, clb, clc, cld) >= 0 .
   1.552 +H27:   f(loop__1__j + 1, clb, clc, cld) <= 4294967295 .
   1.553 +H28:   f(loop__1__j + 1, clb, clc, cld) = f_spec(loop__1__j + 1, clb, clc, cld) 
   1.554 +          .
   1.555 +H29:   r_l(loop__1__j + 1) >= 0 .
   1.556 +H30:   r_l(loop__1__j + 1) <= 15 .
   1.557 +H31:   r_l(loop__1__j + 1) = r_l_spec(loop__1__j + 1) .
   1.558 +H32:   k_l(loop__1__j + 1) >= 0 .
   1.559 +H33:   k_l(loop__1__j + 1) <= 4294967295 .
   1.560 +H34:   k_l(loop__1__j + 1) = k_l_spec(loop__1__j + 1) .
   1.561 +H35:   (((cla + f(loop__1__j + 1, clb, clc, cld)) mod 4294967296 + element(x, [
   1.562 +          r_l(loop__1__j + 1)])) mod 4294967296 + k_l(loop__1__j + 1)) mod 
   1.563 +          4294967296 >= 0 .
   1.564 +H36:   (((cla + f(loop__1__j + 1, clb, clc, cld)) mod 4294967296 + element(x, [
   1.565 +          r_l(loop__1__j + 1)])) mod 4294967296 + k_l(loop__1__j + 1)) mod 
   1.566 +          4294967296 <= 4294967295 .
   1.567 +H37:   wordops__rotate(s_l(loop__1__j + 1), (((cla + f(loop__1__j + 1, clb, 
   1.568 +          clc, cld)) mod 4294967296 + element(x, [r_l(loop__1__j + 1)])) mod 
   1.569 +          4294967296 + k_l(loop__1__j + 1)) mod 4294967296) >= 0 .
   1.570 +H38:   wordops__rotate(s_l(loop__1__j + 1), (((cla + f(loop__1__j + 1, clb, 
   1.571 +          clc, cld)) mod 4294967296 + element(x, [r_l(loop__1__j + 1)])) mod 
   1.572 +          4294967296 + k_l(loop__1__j + 1)) mod 4294967296) <= 4294967295 .
   1.573 +H39:   wordops__rotate(s_l(loop__1__j + 1), (((cla + f(loop__1__j + 1, clb, 
   1.574 +          clc, cld)) mod 4294967296 + element(x, [r_l(loop__1__j + 1)])) mod 
   1.575 +          4294967296 + k_l(loop__1__j + 1)) mod 4294967296) = 
   1.576 +          wordops__rotate_left(s_l(loop__1__j + 1), (((cla + f(loop__1__j + 1, 
   1.577 +          clb, clc, cld)) mod 4294967296 + element(x, [r_l(loop__1__j + 1)])) 
   1.578 +          mod 4294967296 + k_l(loop__1__j + 1)) mod 4294967296) .
   1.579 +H40:   cle >= 0 .
   1.580 +H41:   cle <= 4294967295 .
   1.581 +H42:   (wordops__rotate(s_l(loop__1__j + 1), (((cla + f(loop__1__j + 1, clb, 
   1.582 +          clc, cld)) mod 4294967296 + element(x, [r_l(loop__1__j + 1)])) mod 
   1.583 +          4294967296 + k_l(loop__1__j + 1)) mod 4294967296) + cle) mod 
   1.584 +          4294967296 >= 0 .
   1.585 +H43:   (wordops__rotate(s_l(loop__1__j + 1), (((cla + f(loop__1__j + 1, clb, 
   1.586 +          clc, cld)) mod 4294967296 + element(x, [r_l(loop__1__j + 1)])) mod 
   1.587 +          4294967296 + k_l(loop__1__j + 1)) mod 4294967296) + cle) mod 
   1.588 +          4294967296 <= 4294967295 .
   1.589 +H44:   wordops__rotate(10, clc) >= 0 .
   1.590 +H45:   wordops__rotate(10, clc) <= 4294967295 .
   1.591 +H46:   wordops__rotate(10, clc) = wordops__rotate_left(10, clc) .
   1.592 +H47:   s_r(loop__1__j + 1) >= 0 .
   1.593 +H48:   s_r(loop__1__j + 1) <= 15 .
   1.594 +H49:   s_r(loop__1__j + 1) = s_r_spec(loop__1__j + 1) .
   1.595 +H50:   cra >= 0 .
   1.596 +H51:   cra <= 4294967295 .
   1.597 +H52:   crb >= 0 .
   1.598 +H53:   crb <= 4294967295 .
   1.599 +H54:   crc >= 0 .
   1.600 +H55:   crc <= 4294967295 .
   1.601 +H56:   crd >= 0 .
   1.602 +H57:   crd <= 4294967295 .
   1.603 +H58:   79 - (loop__1__j + 1) >= round_index__base__first .
   1.604 +H59:   79 - (loop__1__j + 1) <= round_index__base__last .
   1.605 +H60:   f(79 - (loop__1__j + 1), crb, crc, crd) >= 0 .
   1.606 +H61:   f(79 - (loop__1__j + 1), crb, crc, crd) <= 4294967295 .
   1.607 +H62:   f(78 - loop__1__j, crb, crc, crd) = f_spec(78 - loop__1__j, crb, crc, 
   1.608 +          crd) .
   1.609 +H63:   r_r(loop__1__j + 1) >= 0 .
   1.610 +H64:   r_r(loop__1__j + 1) <= 15 .
   1.611 +H65:   r_r(loop__1__j + 1) = r_r_spec(loop__1__j + 1) .
   1.612 +H66:   k_r(loop__1__j + 1) >= 0 .
   1.613 +H67:   k_r(loop__1__j + 1) <= 4294967295 .
   1.614 +H68:   k_r(loop__1__j + 1) = k_r_spec(loop__1__j + 1) .
   1.615 +H69:   (((cra + f(79 - (loop__1__j + 1), crb, crc, crd)) mod 4294967296 + 
   1.616 +          element(x, [r_r(loop__1__j + 1)])) mod 4294967296 + k_r(loop__1__j + 
   1.617 +          1)) mod 4294967296 >= 0 .
   1.618 +H70:   (((cra + f(79 - (loop__1__j + 1), crb, crc, crd)) mod 4294967296 + 
   1.619 +          element(x, [r_r(loop__1__j + 1)])) mod 4294967296 + k_r(loop__1__j + 
   1.620 +          1)) mod 4294967296 <= 4294967295 .
   1.621 +H71:   wordops__rotate(s_r(loop__1__j + 1), (((cra + f(79 - (loop__1__j + 1), 
   1.622 +          crb, crc, crd)) mod 4294967296 + element(x, [r_r(loop__1__j + 1)])) 
   1.623 +          mod 4294967296 + k_r(loop__1__j + 1)) mod 4294967296) >= 0 .
   1.624 +H72:   wordops__rotate(s_r(loop__1__j + 1), (((cra + f(79 - (loop__1__j + 1), 
   1.625 +          crb, crc, crd)) mod 4294967296 + element(x, [r_r(loop__1__j + 1)])) 
   1.626 +          mod 4294967296 + k_r(loop__1__j + 1)) mod 4294967296) <= 4294967295 .
   1.627 +H73:   wordops__rotate(s_r(loop__1__j + 1), (((cra + f(79 - (loop__1__j + 1), 
   1.628 +          crb, crc, crd)) mod 4294967296 + element(x, [r_r(loop__1__j + 1)])) 
   1.629 +          mod 4294967296 + k_r(loop__1__j + 1)) mod 4294967296) = 
   1.630 +          wordops__rotate_left(s_r(loop__1__j + 1), (((cra + f(79 - (loop__1__j 
   1.631 +          + 1), crb, crc, crd)) mod 4294967296 + element(x, [r_r(loop__1__j + 1)
   1.632 +          ])) mod 4294967296 + k_r(loop__1__j + 1)) mod 4294967296) .
   1.633 +H74:   cre >= 0 .
   1.634 +H75:   cre <= 4294967295 .
   1.635 +H76:   (wordops__rotate(s_r(loop__1__j + 1), (((cra + f(79 - (loop__1__j + 1), 
   1.636 +          crb, crc, crd)) mod 4294967296 + element(x, [r_r(loop__1__j + 1)])) 
   1.637 +          mod 4294967296 + k_r(loop__1__j + 1)) mod 4294967296) + cre) mod 
   1.638 +          4294967296 >= 0 .
   1.639 +H77:   (wordops__rotate(s_r(loop__1__j + 1), (((cra + f(79 - (loop__1__j + 1), 
   1.640 +          crb, crc, crd)) mod 4294967296 + element(x, [r_r(loop__1__j + 1)])) 
   1.641 +          mod 4294967296 + k_r(loop__1__j + 1)) mod 4294967296) + cre) mod 
   1.642 +          4294967296 <= 4294967295 .
   1.643 +H78:   wordops__rotate(10, crc) >= 0 .
   1.644 +H79:   wordops__rotate(10, crc) <= 4294967295 .
   1.645 +H80:   wordops__rotate(10, crc) = wordops__rotate_left(10, crc) .
   1.646 +H81:   integer__size >= 0 .
   1.647 +H82:   interfaces__unsigned_32__size >= 0 .
   1.648 +H83:   wordops__word__size >= 0 .
   1.649 +H84:   wordops__rotate_amount__size >= 0 .
   1.650 +H85:   word__size >= 0 .
   1.651 +H86:   chain__size >= 0 .
   1.652 +H87:   block_index__size >= 0 .
   1.653 +H88:   block_index__base__first <= block_index__base__last .
   1.654 +H89:   round_index__size >= 0 .
   1.655 +H90:   round_index__base__first <= round_index__base__last .
   1.656 +H91:   chain_pair__size >= 0 .
   1.657 +H92:   rotate_amount__size >= 0 .
   1.658 +H93:   block_index__base__first <= 0 .
   1.659 +H94:   block_index__base__last >= 15 .
   1.660 +H95:   round_index__base__first <= 0 .
   1.661 +H96:   round_index__base__last >= 79 .
   1.662 +       ->
   1.663 +C1:    mk__chain_pair(left := mk__chain(h0 := cle, h1 := (wordops__rotate(s_l(
   1.664 +          loop__1__j + 1), (((cla + f(loop__1__j + 1, clb, clc, cld)) mod 
   1.665 +          4294967296 + element(x, [r_l(loop__1__j + 1)])) mod 4294967296 + k_l(
   1.666 +          loop__1__j + 1)) mod 4294967296) + cle) mod 4294967296, h2 := clb, h3 
   1.667 +          := wordops__rotate(10, clc), h4 := cld), right := mk__chain(h0 := 
   1.668 +          cre, h1 := (wordops__rotate(s_r(loop__1__j + 1), (((cra + f(79 - (
   1.669 +          loop__1__j + 1), crb, crc, crd)) mod 4294967296 + element(x, [r_r(
   1.670 +          loop__1__j + 1)])) mod 4294967296 + k_r(loop__1__j + 1)) mod 
   1.671 +          4294967296) + cre) mod 4294967296, h2 := crb, h3 := wordops__rotate(
   1.672 +          10, crc), h4 := crd)) = steps(mk__chain_pair(left := mk__chain(h0 := 
   1.673 +          ca~, h1 := cb~, h2 := cc~, h3 := cd~, h4 := ce~), right := mk__chain(
   1.674 +          h0 := ca~, h1 := cb~, h2 := cc~, h3 := cd~, h4 := ce~)), loop__1__j + 
   1.675 +          2, x) .
   1.676 +
   1.677 +
   1.678 +For path(s) from start to run-time check associated with statement of line 153:
   1.679 +
   1.680 +procedure_round_63.
   1.681 +*** true .          /* all conclusions proved */
   1.682 +
   1.683 +
   1.684 +For path(s) from assertion of line 147 to run-time check associated with 
   1.685 +          statement of line 153:
   1.686 +
   1.687 +procedure_round_64.
   1.688 +*** true .          /* all conclusions proved */
   1.689 +
   1.690 +
   1.691 +For path(s) from start to run-time check associated with statement of line 154:
   1.692 +
   1.693 +procedure_round_65.
   1.694 +*** true .          /* all conclusions proved */
   1.695 +
   1.696 +
   1.697 +For path(s) from assertion of line 147 to run-time check associated with 
   1.698 +          statement of line 154:
   1.699 +
   1.700 +procedure_round_66.
   1.701 +*** true .          /* all conclusions proved */
   1.702 +
   1.703 +
   1.704 +For path(s) from start to run-time check associated with statement of line 155:
   1.705 +
   1.706 +procedure_round_67.
   1.707 +*** true .          /* all conclusions proved */
   1.708 +
   1.709 +
   1.710 +For path(s) from assertion of line 147 to run-time check associated with 
   1.711 +          statement of line 155:
   1.712 +
   1.713 +procedure_round_68.
   1.714 +*** true .          /* all conclusions proved */
   1.715 +
   1.716 +
   1.717 +For path(s) from start to run-time check associated with statement of line 156:
   1.718 +
   1.719 +procedure_round_69.
   1.720 +*** true .          /* all conclusions proved */
   1.721 +
   1.722 +
   1.723 +For path(s) from assertion of line 147 to run-time check associated with 
   1.724 +          statement of line 156:
   1.725 +
   1.726 +procedure_round_70.
   1.727 +*** true .          /* all conclusions proved */
   1.728 +
   1.729 +
   1.730 +For path(s) from start to run-time check associated with statement of line 157:
   1.731 +
   1.732 +procedure_round_71.
   1.733 +*** true .          /* all conclusions proved */
   1.734 +
   1.735 +
   1.736 +For path(s) from assertion of line 147 to run-time check associated with 
   1.737 +          statement of line 157:
   1.738 +
   1.739 +procedure_round_72.
   1.740 +*** true .          /* all conclusions proved */
   1.741 +
   1.742 +
   1.743 +For path(s) from start to run-time check associated with statement of line 158:
   1.744 +
   1.745 +procedure_round_73.
   1.746 +*** true .          /* all conclusions proved */
   1.747 +
   1.748 +
   1.749 +For path(s) from assertion of line 147 to run-time check associated with 
   1.750 +          statement of line 158:
   1.751 +
   1.752 +procedure_round_74.
   1.753 +*** true .          /* all conclusions proved */
   1.754 +
   1.755 +
   1.756 +For path(s) from start to finish:
   1.757 +
   1.758 +procedure_round_75.
   1.759 +*** true .   /* contradiction within hypotheses. */
   1.760 +
   1.761 +
   1.762 +
   1.763 +For path(s) from assertion of line 147 to finish:
   1.764 +
   1.765 +procedure_round_76.
   1.766 +H1:    mk__chain_pair(left := mk__chain(h0 := cla, h1 := clb, h2 := clc, h3 := 
   1.767 +          cld, h4 := cle), right := mk__chain(h0 := cra, h1 := crb, h2 := crc, 
   1.768 +          h3 := crd, h4 := cre)) = steps(mk__chain_pair(left := mk__chain(h0 := 
   1.769 +          ca~, h1 := cb~, h2 := cc~, h3 := cd~, h4 := ce~), right := mk__chain(
   1.770 +          h0 := ca~, h1 := cb~, h2 := cc~, h3 := cd~, h4 := ce~)), 80, x) .
   1.771 +H2:    ca~ >= 0 .
   1.772 +H3:    ca~ <= 4294967295 .
   1.773 +H4:    cb~ >= 0 .
   1.774 +H5:    cb~ <= 4294967295 .
   1.775 +H6:    cc~ >= 0 .
   1.776 +H7:    cc~ <= 4294967295 .
   1.777 +H8:    cd~ >= 0 .
   1.778 +H9:    cd~ <= 4294967295 .
   1.779 +H10:   ce~ >= 0 .
   1.780 +H11:   ce~ <= 4294967295 .
   1.781 +H12:   for_all(i___1 : integer, 0 <= i___1 and i___1 <= 15 -> 0 <= element(x, [
   1.782 +          i___1]) and element(x, [i___1]) <= 4294967295) .
   1.783 +H13:   clc >= 0 .
   1.784 +H14:   clc <= 4294967295 .
   1.785 +H15:   crd >= 0 .
   1.786 +H16:   crd <= 4294967295 .
   1.787 +H17:   ((cb~ + clc) mod 4294967296 + crd) mod 4294967296 >= 0 .
   1.788 +H18:   ((cb~ + clc) mod 4294967296 + crd) mod 4294967296 <= 4294967295 .
   1.789 +H19:   cld >= 0 .
   1.790 +H20:   cld <= 4294967295 .
   1.791 +H21:   cre >= 0 .
   1.792 +H22:   cre <= 4294967295 .
   1.793 +H23:   ((cc~ + cld) mod 4294967296 + cre) mod 4294967296 >= 0 .
   1.794 +H24:   ((cc~ + cld) mod 4294967296 + cre) mod 4294967296 <= 4294967295 .
   1.795 +H25:   cle >= 0 .
   1.796 +H26:   cle <= 4294967295 .
   1.797 +H27:   cra >= 0 .
   1.798 +H28:   cra <= 4294967295 .
   1.799 +H29:   ((cd~ + cle) mod 4294967296 + cra) mod 4294967296 >= 0 .
   1.800 +H30:   ((cd~ + cle) mod 4294967296 + cra) mod 4294967296 <= 4294967295 .
   1.801 +H31:   cla >= 0 .
   1.802 +H32:   cla <= 4294967295 .
   1.803 +H33:   crb >= 0 .
   1.804 +H34:   crb <= 4294967295 .
   1.805 +H35:   ((ce~ + cla) mod 4294967296 + crb) mod 4294967296 >= 0 .
   1.806 +H36:   ((ce~ + cla) mod 4294967296 + crb) mod 4294967296 <= 4294967295 .
   1.807 +H37:   clb >= 0 .
   1.808 +H38:   clb <= 4294967295 .
   1.809 +H39:   crc >= 0 .
   1.810 +H40:   crc <= 4294967295 .
   1.811 +H41:   ((ca~ + clb) mod 4294967296 + crc) mod 4294967296 >= 0 .
   1.812 +H42:   ((ca~ + clb) mod 4294967296 + crc) mod 4294967296 <= 4294967295 .
   1.813 +H43:   integer__size >= 0 .
   1.814 +H44:   interfaces__unsigned_32__size >= 0 .
   1.815 +H45:   wordops__word__size >= 0 .
   1.816 +H46:   wordops__rotate_amount__size >= 0 .
   1.817 +H47:   word__size >= 0 .
   1.818 +H48:   chain__size >= 0 .
   1.819 +H49:   block_index__size >= 0 .
   1.820 +H50:   block_index__base__first <= block_index__base__last .
   1.821 +H51:   round_index__size >= 0 .
   1.822 +H52:   round_index__base__first <= round_index__base__last .
   1.823 +H53:   chain_pair__size >= 0 .
   1.824 +H54:   rotate_amount__size >= 0 .
   1.825 +H55:   block_index__base__first <= 0 .
   1.826 +H56:   block_index__base__last >= 15 .
   1.827 +H57:   round_index__base__first <= 0 .
   1.828 +H58:   round_index__base__last >= 79 .
   1.829 +       ->
   1.830 +C1:    mk__chain(h0 := ((cb~ + clc) mod 4294967296 + crd) mod 4294967296, h1 := 
   1.831 +          ((cc~ + cld) mod 4294967296 + cre) mod 4294967296, h2 := ((cd~ + cle) 
   1.832 +          mod 4294967296 + cra) mod 4294967296, h3 := ((ce~ + cla) mod 
   1.833 +          4294967296 + crb) mod 4294967296, h4 := ((ca~ + clb) mod 4294967296 + 
   1.834 +          crc) mod 4294967296) = round_spec(mk__chain(h0 := ca~, h1 := cb~, h2 
   1.835 +          := cc~, h3 := cd~, h4 := ce~), x) .
   1.836 +
   1.837 +