File ‹rmd/hash.siv›
*****************************************************************************
Semantic Analysis of SPARK Text
Examiner Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039
Copyright (C) 2010 Altran Praxis Limited, Bath, U.K.
*****************************************************************************
CREATED 29-NOV-2010, 14:30:20 SIMPLIFIED 29-NOV-2010, 14:30:20
SPARK Simplifier Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039
Copyright (C) 2010 Altran Praxis Limited, Bath, U.K.
function RMD.Hash
For path(s) from start to run-time check associated with statement of line 170:
function_hash_1.
*** true . /* all conclusions proved */
For path(s) from start to run-time check associated with statement of line 171:
function_hash_2.
*** true . /* all conclusions proved */
For path(s) from start to run-time check associated with statement of line 172:
function_hash_3.
*** true . /* all conclusions proved */
For path(s) from start to run-time check associated with statement of line 173:
function_hash_4.
*** true . /* all conclusions proved */
For path(s) from start to run-time check associated with statement of line 174:
function_hash_5.
*** true . /* all conclusions proved */
For path(s) from start to run-time check associated with statement of line 175:
function_hash_6.
*** true . /* all conclusions proved */
For path(s) from start to run-time check associated with statement of line 175:
function_hash_7.
*** true . /* all conclusions proved */
For path(s) from start to run-time check associated with statement of line 177:
function_hash_8.
*** true . /* all conclusions proved */
For path(s) from assertion of line 178 to run-time check associated with
statement of line 177:
function_hash_9.
*** true . /* all conclusions proved */
For path(s) from start to run-time check associated with statement of line 177:
function_hash_10.
*** true . /* all conclusions proved */
For path(s) from assertion of line 178 to run-time check associated with
statement of line 177:
function_hash_11.
*** true . /* all conclusions proved */
For path(s) from start to assertion of line 178:
function_hash_12.
H1: x__index__subtype__1__first = 0 .
H2: for_all(i___2 : integer, 0 <= i___2 and i___2 <= 15 -> for_all(i___1 :
integer, x__index__subtype__1__first <= i___1 and i___1 <=
x__index__subtype__1__last -> 0 <= element(element(x, [i___1]), [
i___2]) and element(element(x, [i___1]), [i___2]) <= 4294967295)) .
H3: x__index__subtype__1__last >= 0 .
H4: x__index__subtype__1__last <= 4294967296 .
H5: x__index__subtype__1__first <= x__index__subtype__1__last .
H6: mk__chain(h0 := ca__1, h1 := cb__1, h2 := cc__1, h3 := cd__1, h4 :=
ce__1) = round_spec(mk__chain(h0 := 1732584193, h1 := 4023233417, h2
:= 2562383102, h3 := 271733878, h4 := 3285377520), element(x, [
x__index__subtype__1__first])) .
H7: ca__1 >= 0 .
H8: ca__1 <= 4294967295 .
H9: cb__1 >= 0 .
H10: cb__1 <= 4294967295 .
H11: cc__1 >= 0 .
H12: cc__1 <= 4294967295 .
H13: cd__1 >= 0 .
H14: cd__1 <= 4294967295 .
H15: ce__1 >= 0 .
H16: ce__1 <= 4294967295 .
->
C1: mk__chain(h0 := ca__1, h1 := cb__1, h2 := cc__1, h3 := cd__1, h4 :=
ce__1) = rounds(mk__chain(h0 := 1732584193, h1 := 4023233417, h2 :=
2562383102, h3 := 271733878, h4 := 3285377520),
x__index__subtype__1__first + 1, x) .
For path(s) from assertion of line 178 to assertion of line 178:
function_hash_13.
H1: mk__chain(h0 := ca, h1 := cb, h2 := cc, h3 := cd, h4 := ce) = rounds(
mk__chain(h0 := 1732584193, h1 := 4023233417, h2 := 2562383102, h3 :=
271733878, h4 := 3285377520), loop__1__i + 1, x) .
H2: for_all(i___2 : integer, 0 <= i___2 and i___2 <= 15 -> for_all(i___1 :
integer, x__index__subtype__1__first <= i___1 and i___1 <=
x__index__subtype__1__last -> 0 <= element(element(x, [i___1]), [
i___2]) and element(element(x, [i___1]), [i___2]) <= 4294967295)) .
H3: x__index__subtype__1__first = 0 .
H4: loop__1__i >= 0 .
H5: loop__1__i <= 4294967296 .
H6: loop__1__i >= x__index__subtype__1__first .
H7: ca >= 0 .
H8: ca <= 4294967295 .
H9: cb >= 0 .
H10: cb <= 4294967295 .
H11: cc >= 0 .
H12: cc <= 4294967295 .
H13: cd >= 0 .
H14: cd <= 4294967295 .
H15: ce >= 0 .
H16: ce <= 4294967295 .
H17: loop__1__i + 1 <= x__index__subtype__1__last .
H18: mk__chain(h0 := ca__1, h1 := cb__1, h2 := cc__1, h3 := cd__1, h4 :=
ce__1) = round_spec(mk__chain(h0 := ca, h1 := cb, h2 := cc, h3 := cd,
h4 := ce), element(x, [loop__1__i + 1])) .
H19: ca__1 >= 0 .
H20: ca__1 <= 4294967295 .
H21: cb__1 >= 0 .
H22: cb__1 <= 4294967295 .
H23: cc__1 >= 0 .
H24: cc__1 <= 4294967295 .
H25: cd__1 >= 0 .
H26: cd__1 <= 4294967295 .
H27: ce__1 >= 0 .
H28: ce__1 <= 4294967295 .
H29: interfaces__unsigned_32__size >= 0 .
H30: word__size >= 0 .
H31: chain__size >= 0 .
H32: block_index__size >= 0 .
H33: block_index__base__first <= block_index__base__last .
H34: message_index__size >= 0 .
H35: message_index__base__first <= message_index__base__last .
H36: x__index__subtype__1__first <= x__index__subtype__1__last .
H37: block_index__base__first <= 0 .
H38: block_index__base__last >= 15 .
H39: message_index__base__first <= 0 .
H40: x__index__subtype__1__first >= 0 .
H41: x__index__subtype__1__last >= 0 .
H42: message_index__base__last >= 4294967296 .
H43: x__index__subtype__1__last <= 4294967296 .
H44: x__index__subtype__1__first <= 4294967296 .
->
C1: mk__chain(h0 := ca__1, h1 := cb__1, h2 := cc__1, h3 := cd__1, h4 :=
ce__1) = rounds(mk__chain(h0 := 1732584193, h1 := 4023233417, h2 :=
2562383102, h3 := 271733878, h4 := 3285377520), loop__1__i + 2, x) .
For path(s) from start to run-time check associated with statement of line 183:
function_hash_14.
*** true . /* all conclusions proved */
For path(s) from assertion of line 178 to run-time check associated with
statement of line 183:
function_hash_15.
*** true . /* all conclusions proved */
For path(s) from start to finish:
function_hash_16.
*** true . /* contradiction within hypotheses. */
For path(s) from assertion of line 178 to finish:
function_hash_17.
H1: mk__chain(h0 := ca, h1 := cb, h2 := cc, h3 := cd, h4 := ce) = rounds(
mk__chain(h0 := 1732584193, h1 := 4023233417, h2 := 2562383102, h3 :=
271733878, h4 := 3285377520), x__index__subtype__1__last + 1, x) .
H2: for_all(i___2 : integer, 0 <= i___2 and i___2 <= 15 -> for_all(i___1 :
integer, x__index__subtype__1__first <= i___1 and i___1 <=
x__index__subtype__1__last -> 0 <= element(element(x, [i___1]), [
i___2]) and element(element(x, [i___1]), [i___2]) <= 4294967295)) .
H3: x__index__subtype__1__first = 0 .
H4: x__index__subtype__1__last >= 0 .
H5: x__index__subtype__1__last <= 4294967296 .
H6: x__index__subtype__1__last >= x__index__subtype__1__first .
H7: ca >= 0 .
H8: ca <= 4294967295 .
H9: cb >= 0 .
H10: cb <= 4294967295 .
H11: cc >= 0 .
H12: cc <= 4294967295 .
H13: cd >= 0 .
H14: cd <= 4294967295 .
H15: ce >= 0 .
H16: ce <= 4294967295 .
H17: interfaces__unsigned_32__size >= 0 .
H18: word__size >= 0 .
H19: chain__size >= 0 .
H20: block_index__size >= 0 .
H21: block_index__base__first <= block_index__base__last .
H22: message_index__size >= 0 .
H23: message_index__base__first <= message_index__base__last .
H24: x__index__subtype__1__first <= x__index__subtype__1__last .
H25: block_index__base__first <= 0 .
H26: block_index__base__last >= 15 .
H27: message_index__base__first <= 0 .
H28: x__index__subtype__1__first >= 0 .
H29: message_index__base__last >= 4294967296 .
H30: x__index__subtype__1__first <= 4294967296 .
->
C1: mk__chain(h0 := ca, h1 := cb, h2 := cc, h3 := cd, h4 := ce) = rmd_hash(
x, x__index__subtype__1__last + 1) .