author  haftmann 
Sat, 01 Mar 2014 17:08:39 +0100  
changeset 55818  d8b2f50705d0 
parent 45546  6dd3e88de4c2 
child 56798  939e88e79724 
permissions  rwrr 
41561  1 
(* Title: HOL/SPARK/Examples/RIPEMD160/Round.thy 
2 
Author: Fabian Immler, TU Muenchen 

3 

4 
Verification of the RIPEMD160 hash function 

5 
*) 

6 

7 
theory Round 

8 
imports RMD_Specification 

9 
begin 

10 

11 
spark_open "rmd/round.siv" 

12 

13 
abbreviation from_chain :: "chain \<Rightarrow> RMD.chain" where 

14 
"from_chain c \<equiv> ( 

15 
word_of_int (h0 c), 

16 
word_of_int (h1 c), 

17 
word_of_int (h2 c), 

18 
word_of_int (h3 c), 

19 
word_of_int (h4 c))" 

20 

21 
abbreviation from_chain_pair :: "chain_pair \<Rightarrow> RMD.chain \<times> RMD.chain" where 

22 
"from_chain_pair cc \<equiv> ( 

23 
from_chain (left cc), 

24 
from_chain (right cc))" 

25 

26 
abbreviation to_chain :: "RMD.chain \<Rightarrow> chain" where 

27 
"to_chain c \<equiv> 

28 
(let (h0, h1, h2, h3, h4) = c in 

29 
(h0 = uint h0, 

30 
h1 = uint h1, 

31 
h2 = uint h2, 

32 
h3 = uint h3, 

33 
h4 = uint h4))" 

34 

35 
abbreviation to_chain_pair :: "RMD.chain \<times> RMD.chain \<Rightarrow> chain_pair" where 

36 
"to_chain_pair c == (let (c1, c2) = c in 

37 
( left = to_chain c1, 

38 
right = to_chain c2 ))" 

39 

40 
abbreviation steps' :: "chain_pair \<Rightarrow> int \<Rightarrow> block \<Rightarrow> chain_pair" where 

41 
"steps' cc i b == to_chain_pair (steps 

42 
(\<lambda>n. word_of_int (b (int n))) 

43 
(from_chain_pair cc) 

44 
(nat i))" 

45 

46 
abbreviation round_spec :: "chain \<Rightarrow> block \<Rightarrow> chain" where 

47 
"round_spec c b == to_chain (round (\<lambda>n. word_of_int (b (int n))) (from_chain c))" 

48 

49 
spark_proof_functions 

50 
steps = steps' 

51 
round_spec = round_spec 

52 

53 
lemma uint_word_of_int_id: 

54 
assumes "0 <= (x::int)" 

55 
assumes "x <= 4294967295" 

56 
shows"uint(word_of_int x::word32) = x" 

57 
unfolding int_word_uint 

58 
using assms 

59 
by (simp add:int_mod_eq') 

60 

61 
lemma steps_step: "steps X cc (Suc i) = step_both X (steps X cc i) i" 

62 
unfolding steps_def 

63 
by (induct i) simp_all 

64 

65 
lemma from_to_id: "from_chain_pair (to_chain_pair CC) = CC" 

66 
proof (cases CC) 

67 
fix a::RMD.chain 

68 
fix b c d e f::word32 

69 
assume "CC = (a, b, c, d, e, f)" 

70 
thus ?thesis by (cases a) simp 

71 
qed 

72 

73 
lemma steps_to_steps': 

74 
"F A (steps X cc i) B = 

75 
F A (from_chain_pair (to_chain_pair (steps X cc i))) B" 

76 
unfolding from_to_id .. 

77 

78 
lemma steps'_step: 

79 
assumes "0 <= i" 

80 
shows 

81 
"steps' cc (i + 1) X = to_chain_pair ( 

82 
step_both 

83 
(\<lambda>n. word_of_int (X (int n))) 

84 
(from_chain_pair (steps' cc i X)) 

85 
(nat i))" 

86 
proof  

87 
have "nat (i + 1) = Suc (nat i)" using assms by simp 

88 
show ?thesis 

89 
unfolding `nat (i + 1) = Suc (nat i)` steps_step steps_to_steps' 

90 
.. 

91 
qed 

92 

93 
lemma step_from_hyp: 

94 
assumes 

95 
step_hyp: 

96 
"\<lparr>left = 

97 
\<lparr>h0 = a, h1 = b, h2 = c, h3 = d, h4 = e\<rparr>, 

98 
right = 

99 
\<lparr>h0 = a', h1 = b', h2 = c', h3 = d', h4 = e'\<rparr>\<rparr> = 

100 
steps' 

101 
(\<lparr>left = 

102 
\<lparr>h0 = a_0, h1 = b_0, h2 = c_0, 

103 
h3 = d_0, h4 = e_0\<rparr>, 

104 
right = 

105 
\<lparr>h0 = a_0, h1 = b_0, h2 = c_0, 

106 
h3 = d_0, h4 = e_0\<rparr>\<rparr>) 

107 
j x" 

108 
assumes "a <= 4294967295" (is "_ <= ?M") 

109 
assumes "b <= ?M" and "c <= ?M" and "d <= ?M" and "e <= ?M" 

110 
assumes "a' <= ?M" and "b' <= ?M" and "c' <= ?M" and "d' <= ?M" and "e' <= ?M" 

111 
assumes "0 <= a " and "0 <= b " and "0 <= c " and "0 <= d " and "0 <= e " 

112 
assumes "0 <= a'" and "0 <= b'" and "0 <= c'" and "0 <= d'" and "0 <= e'" 

113 
assumes "0 <= x (r_l_spec j)" and "x (r_l_spec j) <= ?M" 

114 
assumes "0 <= x (r_r_spec j)" and "x (r_r_spec j) <= ?M" 

115 
assumes "0 <= j" and "j <= 79" 

116 
shows 

117 
"\<lparr>left = 

118 
\<lparr>h0 = e, 

119 
h1 = 

120 
(rotate_left (s_l_spec j) 

121 
((((a + f_spec j b c d) mod 4294967296 + 

122 
x (r_l_spec j)) mod 

123 
4294967296 + 

124 
k_l_spec j) mod 

125 
4294967296) + 

126 
e) mod 

127 
4294967296, 

128 
h2 = b, h3 = rotate_left 10 c, 

129 
h4 = d\<rparr>, 

130 
right = 

131 
\<lparr>h0 = e', 

132 
h1 = 

133 
(rotate_left (s_r_spec j) 

134 
((((a' + f_spec (79  j) b' c' d') mod 

135 
4294967296 + 

136 
x (r_r_spec j)) mod 

137 
4294967296 + 

138 
k_r_spec j) mod 

139 
4294967296) + 

140 
e') mod 

141 
4294967296, 

142 
h2 = b', h3 = rotate_left 10 c', 

143 
h4 = d'\<rparr>\<rparr> = 

144 
steps' 

145 
(\<lparr>left = 

146 
\<lparr>h0 = a_0, h1 = b_0, h2 = c_0, 

147 
h3 = d_0, h4 = e_0\<rparr>, 

148 
right = 

149 
\<lparr>h0 = a_0, h1 = b_0, h2 = c_0, 

150 
h3 = d_0, h4 = e_0\<rparr>\<rparr>) 

151 
(j + 1) x" 

152 
using step_hyp 

153 
proof  

154 
let ?MM = 4294967296 

155 
have AL: "uint(word_of_int e::word32) = e" 

156 
by (rule uint_word_of_int_id[OF `0 <= e` `e <= ?M`]) 

157 
have CL: "uint(word_of_int b::word32) = b" 

158 
by (rule uint_word_of_int_id[OF `0 <= b` `b <= ?M`]) 

159 
have DL: "True" .. 

160 
have EL: "uint(word_of_int d::word32) = d" 

161 
by (rule uint_word_of_int_id[OF `0 <= d` `d <= ?M`]) 

162 
have AR: "uint(word_of_int e'::word32) = e'" 

163 
by (rule uint_word_of_int_id[OF `0 <= e'` `e' <= ?M`]) 

164 
have CR: "uint(word_of_int b'::word32) = b'" 

165 
by (rule uint_word_of_int_id[OF `0 <= b'` `b' <= ?M`]) 

166 
have DR: "True" .. 

167 
have ER: "uint(word_of_int d'::word32) = d'" 

168 
by (rule uint_word_of_int_id[OF `0 <= d'` `d' <= ?M`]) 

169 
have BL: 

170 
"(uint 

171 
(word_rotl (s (nat j)) 

172 
((word_of_int::int\<Rightarrow>word32) 

173 
((((a + f_spec j b c d) mod ?MM + 

174 
x (r_l_spec j)) mod ?MM + 

175 
k_l_spec j) mod ?MM))) + 

176 
e) mod ?MM 

177 
= 

178 
uint 

179 
(word_rotl (s (nat j)) 

180 
(word_of_int a + 

181 
f (nat j) (word_of_int b) 

182 
(word_of_int c) (word_of_int d) + 

183 
word_of_int (x (r_l_spec j)) + 

184 
K (nat j)) + 

185 
word_of_int e)" 

186 
(is "(uint (word_rotl _ (_ ((((_ + ?F) mod _ + ?X) mod _ + _) mod _))) + _) mod _ = _") 

187 
proof  

188 
have "a mod ?MM = a" using `0 <= a` `a <= ?M` 

189 
by (simp add: int_mod_eq') 

190 
have "?X mod ?MM = ?X" using `0 <= ?X` `?X <= ?M` 

191 
by (simp add: int_mod_eq') 

192 
have "e mod ?MM = e" using `0 <= e` `e <= ?M` 

193 
by (simp add: int_mod_eq') 

194 
have "(?MM::int) = 2 ^ len_of TYPE(32)" by simp 

195 
show ?thesis 

196 
unfolding 

45546
6dd3e88de4c2
HOLWord: removed many duplicate theorems (see NEWS)
huffman
parents:
41635
diff
changeset

197 
word_add_def 
41561  198 
uint_word_of_int_id[OF `0 <= a` `a <= ?M`] 
199 
uint_word_of_int_id[OF `0 <= ?X` `?X <= ?M`] 

200 
int_word_uint 

201 
unfolding `?MM = 2 ^ len_of TYPE(32)` 

202 
unfolding word_uint.Abs_norm 

203 
by (simp add: 

204 
`a mod ?MM = a` 

205 
`e mod ?MM = e` 

206 
`?X mod ?MM = ?X`) 

207 
qed 

208 

209 
have BR: 

210 
"(uint 

211 
(word_rotl (s' (nat j)) 

212 
((word_of_int::int\<Rightarrow>word32) 

213 
((((a' + f_spec (79  j) b' c' d') mod ?MM + 

214 
x (r_r_spec j)) mod ?MM + 

215 
k_r_spec j) mod ?MM))) + 

216 
e') mod ?MM 

217 
= 

218 
uint 

219 
(word_rotl (s' (nat j)) 

220 
(word_of_int a' + 

221 
f (79  nat j) (word_of_int b') 

222 
(word_of_int c') (word_of_int d') + 

223 
word_of_int (x (r_r_spec j)) + 

224 
K' (nat j)) + 

225 
word_of_int e')" 

226 
(is "(uint (word_rotl _ (_ ((((_ + ?F) mod _ + ?X) mod _ + _) mod _))) + _) mod _ = _") 

227 
proof  

228 
have "a' mod ?MM = a'" using `0 <= a'` `a' <= ?M` 

229 
by (simp add: int_mod_eq') 

230 
have "?X mod ?MM = ?X" using `0 <= ?X` `?X <= ?M` 

231 
by (simp add: int_mod_eq') 

232 
have "e' mod ?MM = e'" using `0 <= e'` `e' <= ?M` 

233 
by (simp add: int_mod_eq') 

234 
have "(?MM::int) = 2 ^ len_of TYPE(32)" by simp 

235 
have nat_transfer: "79  nat j = nat (79  j)" 

236 
using nat_diff_distrib `0 <= j` `j <= 79` 

237 
by simp 

238 
show ?thesis 

239 
unfolding 

45546
6dd3e88de4c2
HOLWord: removed many duplicate theorems (see NEWS)
huffman
parents:
41635
diff
changeset

240 
word_add_def 
41561  241 
uint_word_of_int_id[OF `0 <= a'` `a' <= ?M`] 
242 
uint_word_of_int_id[OF `0 <= ?X` `?X <= ?M`] 

243 
int_word_uint 

244 
nat_transfer 

245 
unfolding `?MM = 2 ^ len_of TYPE(32)` 

246 
unfolding word_uint.Abs_norm 

247 
by (simp add: 

248 
`a' mod ?MM = a'` 

249 
`e' mod ?MM = e'` 

250 
`?X mod ?MM = ?X`) 

251 
qed 

252 

253 
show ?thesis 

254 
unfolding steps'_step[OF `0 <= j`] step_hyp[symmetric] 

255 
step_both_def step_r_def step_l_def 

256 
by (simp add: AL BL CL DL EL AR BR CR DR ER) 

257 
qed 

258 

259 
spark_vc procedure_round_61 

260 
proof  

261 
let ?M = "4294967295::int" 

262 
have step_hyp: 

263 
"\<lparr>left = 

264 
\<lparr>h0 = ca, h1 = cb, h2 = cc, 

265 
h3 = cd, h4 = ce\<rparr>, 

266 
right = 

267 
\<lparr>h0 = ca, h1 = cb, h2 = cc, 

268 
h3 = cd, h4 = ce\<rparr>\<rparr> = 

269 
steps' 

270 
(\<lparr>left = 

271 
\<lparr>h0 = ca, h1 = cb, h2 = cc, 

272 
h3 = cd, h4 = ce\<rparr>, 

273 
right = 

274 
\<lparr>h0 = ca, h1 = cb, h2 = cc, 

275 
h3 = cd, h4 = ce\<rparr>\<rparr>) 

276 
0 x" 

277 
unfolding steps_def 

278 
by (simp add: 

279 
uint_word_of_int_id[OF `0 <= ca` `ca <= ?M`] 

280 
uint_word_of_int_id[OF `0 <= cb` `cb <= ?M`] 

281 
uint_word_of_int_id[OF `0 <= cc` `cc <= ?M`] 

282 
uint_word_of_int_id[OF `0 <= cd` `cd <= ?M`] 

283 
uint_word_of_int_id[OF `0 <= ce` `ce <= ?M`]) 

284 
let ?rotate_arg_l = 

41635
f938a6022d2e
Replaced smod by standard mod operator to reflect actual behaviour
berghofe
parents:
41561
diff
changeset

285 
"((((ca + f 0 cb cc cd) mod 4294967296 + 
f938a6022d2e
Replaced smod by standard mod operator to reflect actual behaviour
berghofe
parents:
41561
diff
changeset

286 
x (r_l 0)) mod 4294967296 + k_l 0) mod 4294967296)" 
41561  287 
let ?rotate_arg_r = 
41635
f938a6022d2e
Replaced smod by standard mod operator to reflect actual behaviour
berghofe
parents:
41561
diff
changeset

288 
"((((ca + f 79 cb cc cd) mod 4294967296 + 
f938a6022d2e
Replaced smod by standard mod operator to reflect actual behaviour
berghofe
parents:
41561
diff
changeset

289 
x (r_r 0)) mod 4294967296 + k_r 0) mod 4294967296)" 
41561  290 
note returns = 
291 
`wordops__rotate (s_l 0) ?rotate_arg_l = 

292 
rotate_left (s_l 0) ?rotate_arg_l` 

293 
`wordops__rotate (s_r 0) ?rotate_arg_r = 

294 
rotate_left (s_r 0) ?rotate_arg_r` 

295 
`wordops__rotate 10 cc = rotate_left 10 cc` 

296 
`f 0 cb cc cd = f_spec 0 cb cc cd` 

297 
`f 79 cb cc cd = f_spec 79 cb cc cd` 

298 
`k_l 0 = k_l_spec 0` 

299 
`k_r 0 = k_r_spec 0` 

300 
`r_l 0 = r_l_spec 0` 

301 
`r_r 0 = r_r_spec 0` 

302 
`s_l 0 = s_l_spec 0` 

303 
`s_r 0 = s_r_spec 0` 

304 

305 
note x_borders = `\<forall>i. 0 \<le> i \<and> i \<le> 15 \<longrightarrow> 0 \<le> x i \<and> x i \<le> ?M` 

306 

307 
from `0 <= r_l 0` `r_l 0 <= 15` x_borders 

308 
have "0 \<le> x (r_l 0)" by blast 

309 
hence x_lower: "0 <= x (r_l_spec 0)" unfolding returns . 

310 

311 
from `0 <= r_l 0` `r_l 0 <= 15` x_borders 

312 
have "x (r_l 0) <= ?M" by blast 

313 
hence x_upper: "x (r_l_spec 0) <= ?M" unfolding returns . 

314 

315 
from `0 <= r_r 0` `r_r 0 <= 15` x_borders 

316 
have "0 \<le> x (r_r 0)" by blast 

317 
hence x_lower': "0 <= x (r_r_spec 0)" unfolding returns . 

318 

319 
from `0 <= r_r 0` `r_r 0 <= 15` x_borders 

320 
have "x (r_r 0) <= ?M" by blast 

321 
hence x_upper': "x (r_r_spec 0) <= ?M" unfolding returns . 

322 

323 
have "0 <= (0::int)" by simp 

324 
have "0 <= (79::int)" by simp 

325 
note step_from_hyp [OF 

326 
step_hyp 

327 
H2 H4 H6 H8 H10 H2 H4 H6 H8 H10 (* upper bounds *) 

328 
H1 H3 H5 H7 H9 H1 H3 H5 H7 H9 (* lower bounds *) 

329 
] 

330 
from this[OF x_lower x_upper x_lower' x_upper' `0 <= 0` `0 <= 79`] 

331 
`0 \<le> ca` `0 \<le> ce` x_lower x_lower' 

332 
show ?thesis unfolding returns(1) returns(2) unfolding returns 

41635
f938a6022d2e
Replaced smod by standard mod operator to reflect actual behaviour
berghofe
parents:
41561
diff
changeset

333 
by simp 
41561  334 
qed 
335 

336 
spark_vc procedure_round_62 

337 
proof  

338 
let ?M = "4294967295::int" 

339 
let ?rotate_arg_l = 

41635
f938a6022d2e
Replaced smod by standard mod operator to reflect actual behaviour
berghofe
parents:
41561
diff
changeset

340 
"((((cla + f (loop__1__j + 1) clb clc cld) mod 4294967296 + 
f938a6022d2e
Replaced smod by standard mod operator to reflect actual behaviour
berghofe
parents:
41561
diff
changeset

341 
x (r_l (loop__1__j + 1))) mod 4294967296 + 
f938a6022d2e
Replaced smod by standard mod operator to reflect actual behaviour
berghofe
parents:
41561
diff
changeset

342 
k_l (loop__1__j + 1)) mod 4294967296)" 
41561  343 
let ?rotate_arg_r = 
41635
f938a6022d2e
Replaced smod by standard mod operator to reflect actual behaviour
berghofe
parents:
41561
diff
changeset

344 
"((((cra + f (79  (loop__1__j + 1)) crb crc crd) mod 
f938a6022d2e
Replaced smod by standard mod operator to reflect actual behaviour
berghofe
parents:
41561
diff
changeset

345 
4294967296 + x (r_r (loop__1__j + 1))) mod 4294967296 + 
f938a6022d2e
Replaced smod by standard mod operator to reflect actual behaviour
berghofe
parents:
41561
diff
changeset

346 
k_r (loop__1__j + 1)) mod 4294967296)" 
41561  347 

348 
have s: "78  loop__1__j = (79  (loop__1__j + 1))" by simp 

349 
note returns = 

350 
`wordops__rotate (s_l (loop__1__j + 1)) ?rotate_arg_l = 

351 
rotate_left (s_l (loop__1__j + 1)) ?rotate_arg_l` 

352 
`wordops__rotate (s_r (loop__1__j + 1)) ?rotate_arg_r = 

353 
rotate_left (s_r (loop__1__j + 1)) ?rotate_arg_r` 

354 
`f (loop__1__j + 1) clb clc cld = 

355 
f_spec (loop__1__j + 1) clb clc cld` 

356 
`f (78  loop__1__j) crb crc crd = 

357 
f_spec (78  loop__1__j) crb crc crd`[simplified s] 

358 
`wordops__rotate 10 clc = rotate_left 10 clc` 

359 
`wordops__rotate 10 crc = rotate_left 10 crc` 

360 
`k_l (loop__1__j + 1) = k_l_spec (loop__1__j + 1)` 

361 
`k_r (loop__1__j + 1) = k_r_spec (loop__1__j + 1)` 

362 
`r_l (loop__1__j + 1) = r_l_spec (loop__1__j + 1)` 

363 
`r_r (loop__1__j + 1) = r_r_spec (loop__1__j + 1)` 

364 
`s_l (loop__1__j + 1) = s_l_spec (loop__1__j + 1)` 

365 
`s_r (loop__1__j + 1) = s_r_spec (loop__1__j + 1)` 

366 

367 
note x_borders = `\<forall>i. 0 \<le> i \<and> i \<le> 15 \<longrightarrow> 0 \<le> x i \<and> x i \<le> ?M` 

368 

369 
from `0 <= r_l (loop__1__j + 1)` `r_l (loop__1__j + 1) <= 15` x_borders 

370 
have "0 \<le> x (r_l (loop__1__j + 1))" by blast 

371 
hence x_lower: "0 <= x (r_l_spec (loop__1__j + 1))" unfolding returns . 

372 

373 
from `0 <= r_l (loop__1__j + 1)` `r_l (loop__1__j + 1) <= 15` x_borders 

374 
have "x (r_l (loop__1__j + 1)) <= ?M" by blast 

375 
hence x_upper: "x (r_l_spec (loop__1__j + 1)) <= ?M" unfolding returns . 

376 

377 
from `0 <= r_r (loop__1__j + 1)` `r_r (loop__1__j + 1) <= 15` x_borders 

378 
have "0 \<le> x (r_r (loop__1__j + 1))" by blast 

379 
hence x_lower': "0 <= x (r_r_spec (loop__1__j + 1))" unfolding returns . 

380 

381 
from `0 <= r_r (loop__1__j + 1)` `r_r (loop__1__j + 1) <= 15` x_borders 

382 
have "x (r_r (loop__1__j + 1)) <= ?M" by blast 

383 
hence x_upper': "x (r_r_spec (loop__1__j + 1)) <= ?M" unfolding returns . 

384 

385 
from `0 <= loop__1__j` have "0 <= loop__1__j + 1" by simp 

386 
from `loop__1__j <= 78` have "loop__1__j + 1 <= 79" by simp 

387 

388 
have "loop__1__j + 1 + 1 = loop__1__j + 2" by simp 

389 

390 
note step_from_hyp[OF H1 

391 
`cla <= ?M` 

392 
`clb <= ?M` 

393 
`clc <= ?M` 

394 
`cld <= ?M` 

395 
`cle <= ?M` 

396 
`cra <= ?M` 

397 
`crb <= ?M` 

398 
`crc <= ?M` 

399 
`crd <= ?M` 

400 
`cre <= ?M` 

401 

402 
`0 <= cla` 

403 
`0 <= clb` 

404 
`0 <= clc` 

405 
`0 <= cld` 

406 
`0 <= cle` 

407 
`0 <= cra` 

408 
`0 <= crb` 

409 
`0 <= crc` 

410 
`0 <= crd` 

411 
`0 <= cre`] 

412 
from this[OF 

413 
x_lower x_upper x_lower' x_upper' 

414 
`0 <= loop__1__j + 1` `loop__1__j + 1 <= 79`] 

415 
`0 \<le> cla` `0 \<le> cle` `0 \<le> cra` `0 \<le> cre` x_lower x_lower' 

416 
show ?thesis unfolding `loop__1__j + 1 + 1 = loop__1__j + 2` 

417 
unfolding returns(1) returns(2) unfolding returns 

41635
f938a6022d2e
Replaced smod by standard mod operator to reflect actual behaviour
berghofe
parents:
41561
diff
changeset

418 
by simp 
41561  419 
qed 
420 

421 
spark_vc procedure_round_76 

422 
proof  

423 
let ?M = "4294967295 :: int" 

424 
let ?INIT_CHAIN = 

425 
"\<lparr>h0 = ca_init, h1 = cb_init, 

426 
h2 = cc_init, h3 = cd_init, 

427 
h4 = ce_init\<rparr>" 

428 
have steps_to_steps': 

429 
"steps 

430 
(\<lambda>n\<Colon>nat. word_of_int (x (int n))) 

431 
(from_chain ?INIT_CHAIN, from_chain ?INIT_CHAIN) 

432 
80 = 

433 
from_chain_pair ( 

434 
steps' 

435 
(\<lparr>left = ?INIT_CHAIN, right = ?INIT_CHAIN\<rparr>) 

436 
80 

437 
x)" 

438 
unfolding from_to_id by simp 

439 
from 

440 
`0 \<le> ca_init` `ca_init \<le> ?M` 

441 
`0 \<le> cb_init` `cb_init \<le> ?M` 

442 
`0 \<le> cc_init` `cc_init \<le> ?M` 

443 
`0 \<le> cd_init` `cd_init \<le> ?M` 

444 
`0 \<le> ce_init` `ce_init \<le> ?M` 

445 
`0 \<le> cla` `cla \<le> ?M` 

446 
`0 \<le> clb` `clb \<le> ?M` 

447 
`0 \<le> clc` `clc \<le> ?M` 

448 
`0 \<le> cld` `cld \<le> ?M` 

449 
`0 \<le> cle` `cle \<le> ?M` 

450 
`0 \<le> cra` `cra \<le> ?M` 

451 
`0 \<le> crb` `crb \<le> ?M` 

452 
`0 \<le> crc` `crc \<le> ?M` 

453 
`0 \<le> crd` `crd \<le> ?M` 

454 
`0 \<le> cre` `cre \<le> ?M` 

455 
show ?thesis 

456 
unfolding round_def 

457 
unfolding steps_to_steps' 

458 
unfolding H1[symmetric] 

55818  459 
by (simp add: uint_word_ariths(1) rdmods 
41561  460 
uint_word_of_int_id) 
461 
qed 

462 

463 
spark_end 

464 

465 
end 