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:20  SIMPLIFIED 29-NOV-2010, 14:30:20
9
10SPARK Simplifier Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039
11Copyright (C) 2010 Altran Praxis Limited, Bath, U.K.
12
13function RMD.Hash
14
15
16
17
18For path(s) from start to run-time check associated with statement of line 170:
19
20function_hash_1.
21*** true .          /* all conclusions proved */
22
23
24For path(s) from start to run-time check associated with statement of line 171:
25
26function_hash_2.
27*** true .          /* all conclusions proved */
28
29
30For path(s) from start to run-time check associated with statement of line 172:
31
32function_hash_3.
33*** true .          /* all conclusions proved */
34
35
36For path(s) from start to run-time check associated with statement of line 173:
37
38function_hash_4.
39*** true .          /* all conclusions proved */
40
41
42For path(s) from start to run-time check associated with statement of line 174:
43
44function_hash_5.
45*** true .          /* all conclusions proved */
46
47
48For path(s) from start to run-time check associated with statement of line 175:
49
50function_hash_6.
51*** true .          /* all conclusions proved */
52
53
54For path(s) from start to run-time check associated with statement of line 175:
55
56function_hash_7.
57*** true .          /* all conclusions proved */
58
59
60For path(s) from start to run-time check associated with statement of line 177:
61
62function_hash_8.
63*** true .          /* all conclusions proved */
64
65
66For path(s) from assertion of line 178 to run-time check associated with 
67          statement of line 177:
68
69function_hash_9.
70*** true .          /* all conclusions proved */
71
72
73For path(s) from start to run-time check associated with statement of line 177:
74
75function_hash_10.
76*** true .          /* all conclusions proved */
77
78
79For path(s) from assertion of line 178 to run-time check associated with 
80          statement of line 177:
81
82function_hash_11.
83*** true .          /* all conclusions proved */
84
85
86For path(s) from start to assertion of line 178:
87
88function_hash_12.
89H1:    x__index__subtype__1__first = 0 .
90H2:    for_all(i___2 : integer, 0 <= i___2 and i___2 <= 15 -> for_all(i___1 : 
91          integer, x__index__subtype__1__first <= i___1 and i___1 <= 
92          x__index__subtype__1__last -> 0 <= element(element(x, [i___1]), [
93          i___2]) and element(element(x, [i___1]), [i___2]) <= 4294967295)) .
94H3:    x__index__subtype__1__last >= 0 .
95H4:    x__index__subtype__1__last <= 4294967296 .
96H5:    x__index__subtype__1__first <= x__index__subtype__1__last .
97H6:    mk__chain(h0 := ca__1, h1 := cb__1, h2 := cc__1, h3 := cd__1, h4 := 
98          ce__1) = round_spec(mk__chain(h0 := 1732584193, h1 := 4023233417, h2 
99          := 2562383102, h3 := 271733878, h4 := 3285377520), element(x, [
100          x__index__subtype__1__first])) .
101H7:    ca__1 >= 0 .
102H8:    ca__1 <= 4294967295 .
103H9:    cb__1 >= 0 .
104H10:   cb__1 <= 4294967295 .
105H11:   cc__1 >= 0 .
106H12:   cc__1 <= 4294967295 .
107H13:   cd__1 >= 0 .
108H14:   cd__1 <= 4294967295 .
109H15:   ce__1 >= 0 .
110H16:   ce__1 <= 4294967295 .
111       ->
112C1:    mk__chain(h0 := ca__1, h1 := cb__1, h2 := cc__1, h3 := cd__1, h4 := 
113          ce__1) = rounds(mk__chain(h0 := 1732584193, h1 := 4023233417, h2 := 
114          2562383102, h3 := 271733878, h4 := 3285377520), 
115          x__index__subtype__1__first + 1, x) .
116
117
118For path(s) from assertion of line 178 to assertion of line 178:
119
120function_hash_13.
121H1:    mk__chain(h0 := ca, h1 := cb, h2 := cc, h3 := cd, h4 := ce) = rounds(
122          mk__chain(h0 := 1732584193, h1 := 4023233417, h2 := 2562383102, h3 := 
123          271733878, h4 := 3285377520), loop__1__i + 1, x) .
124H2:    for_all(i___2 : integer, 0 <= i___2 and i___2 <= 15 -> for_all(i___1 : 
125          integer, x__index__subtype__1__first <= i___1 and i___1 <= 
126          x__index__subtype__1__last -> 0 <= element(element(x, [i___1]), [
127          i___2]) and element(element(x, [i___1]), [i___2]) <= 4294967295)) .
128H3:    x__index__subtype__1__first = 0 .
129H4:    loop__1__i >= 0 .
130H5:    loop__1__i <= 4294967296 .
131H6:    loop__1__i >= x__index__subtype__1__first .
132H7:    ca >= 0 .
133H8:    ca <= 4294967295 .
134H9:    cb >= 0 .
135H10:   cb <= 4294967295 .
136H11:   cc >= 0 .
137H12:   cc <= 4294967295 .
138H13:   cd >= 0 .
139H14:   cd <= 4294967295 .
140H15:   ce >= 0 .
141H16:   ce <= 4294967295 .
142H17:   loop__1__i + 1 <= x__index__subtype__1__last .
143H18:   mk__chain(h0 := ca__1, h1 := cb__1, h2 := cc__1, h3 := cd__1, h4 := 
144          ce__1) = round_spec(mk__chain(h0 := ca, h1 := cb, h2 := cc, h3 := cd, 
145          h4 := ce), element(x, [loop__1__i + 1])) .
146H19:   ca__1 >= 0 .
147H20:   ca__1 <= 4294967295 .
148H21:   cb__1 >= 0 .
149H22:   cb__1 <= 4294967295 .
150H23:   cc__1 >= 0 .
151H24:   cc__1 <= 4294967295 .
152H25:   cd__1 >= 0 .
153H26:   cd__1 <= 4294967295 .
154H27:   ce__1 >= 0 .
155H28:   ce__1 <= 4294967295 .
156H29:   interfaces__unsigned_32__size >= 0 .
157H30:   word__size >= 0 .
158H31:   chain__size >= 0 .
159H32:   block_index__size >= 0 .
160H33:   block_index__base__first <= block_index__base__last .
161H34:   message_index__size >= 0 .
162H35:   message_index__base__first <= message_index__base__last .
163H36:   x__index__subtype__1__first <= x__index__subtype__1__last .
164H37:   block_index__base__first <= 0 .
165H38:   block_index__base__last >= 15 .
166H39:   message_index__base__first <= 0 .
167H40:   x__index__subtype__1__first >= 0 .
168H41:   x__index__subtype__1__last >= 0 .
169H42:   message_index__base__last >= 4294967296 .
170H43:   x__index__subtype__1__last <= 4294967296 .
171H44:   x__index__subtype__1__first <= 4294967296 .
172       ->
173C1:    mk__chain(h0 := ca__1, h1 := cb__1, h2 := cc__1, h3 := cd__1, h4 := 
174          ce__1) = rounds(mk__chain(h0 := 1732584193, h1 := 4023233417, h2 := 
175          2562383102, h3 := 271733878, h4 := 3285377520), loop__1__i + 2, x) .
176
177
178For path(s) from start to run-time check associated with statement of line 183:
179
180function_hash_14.
181*** true .          /* all conclusions proved */
182
183
184For path(s) from assertion of line 178 to run-time check associated with 
185          statement of line 183:
186
187function_hash_15.
188*** true .          /* all conclusions proved */
189
190
191For path(s) from start to finish:
192
193function_hash_16.
194*** true .   /* contradiction within hypotheses. */
195
196
197
198For path(s) from assertion of line 178 to finish:
199
200function_hash_17.
201H1:    mk__chain(h0 := ca, h1 := cb, h2 := cc, h3 := cd, h4 := ce) = rounds(
202          mk__chain(h0 := 1732584193, h1 := 4023233417, h2 := 2562383102, h3 := 
203          271733878, h4 := 3285377520), x__index__subtype__1__last + 1, x) .
204H2:    for_all(i___2 : integer, 0 <= i___2 and i___2 <= 15 -> for_all(i___1 : 
205          integer, x__index__subtype__1__first <= i___1 and i___1 <= 
206          x__index__subtype__1__last -> 0 <= element(element(x, [i___1]), [
207          i___2]) and element(element(x, [i___1]), [i___2]) <= 4294967295)) .
208H3:    x__index__subtype__1__first = 0 .
209H4:    x__index__subtype__1__last >= 0 .
210H5:    x__index__subtype__1__last <= 4294967296 .
211H6:    x__index__subtype__1__last >= x__index__subtype__1__first .
212H7:    ca >= 0 .
213H8:    ca <= 4294967295 .
214H9:    cb >= 0 .
215H10:   cb <= 4294967295 .
216H11:   cc >= 0 .
217H12:   cc <= 4294967295 .
218H13:   cd >= 0 .
219H14:   cd <= 4294967295 .
220H15:   ce >= 0 .
221H16:   ce <= 4294967295 .
222H17:   interfaces__unsigned_32__size >= 0 .
223H18:   word__size >= 0 .
224H19:   chain__size >= 0 .
225H20:   block_index__size >= 0 .
226H21:   block_index__base__first <= block_index__base__last .
227H22:   message_index__size >= 0 .
228H23:   message_index__base__first <= message_index__base__last .
229H24:   x__index__subtype__1__first <= x__index__subtype__1__last .
230H25:   block_index__base__first <= 0 .
231H26:   block_index__base__last >= 15 .
232H27:   message_index__base__first <= 0 .
233H28:   x__index__subtype__1__first >= 0 .
234H29:   message_index__base__last >= 4294967296 .
235H30:   x__index__subtype__1__first <= 4294967296 .
236       ->
237C1:    mk__chain(h0 := ca, h1 := cb, h2 := cc, h3 := cd, h4 := ce) = rmd_hash(
238          x, x__index__subtype__1__last + 1) .
239
240
241