1(* Title: HOL/SPARK/Examples/RIPEMD-160/Round.thy 2 Author: Fabian Immler, TU Muenchen 3 4Verification of the RIPEMD-160 hash function 5*) 6 7theory Round 8imports RMD_Specification 9begin 10 11spark_open \<open>rmd/round\<close> 12 13abbreviation 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 21abbreviation 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 26abbreviation 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 35abbreviation 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 40abbreviation 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 46abbreviation 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 49spark_proof_functions 50 steps = steps' 51 round_spec = round_spec 52 53lemma 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 61lemma 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 65lemma from_to_id: "from_chain_pair (to_chain_pair CC) = CC" 66proof (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 71qed 72 73lemma 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 78lemma 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))" 86proof - 87 have "nat (i + 1) = Suc (nat i)" using assms by simp 88 show ?thesis 89 unfolding \<open>nat (i + 1) = Suc (nat i)\<close> steps_step steps_to_steps' 90 .. 91qed 92 93lemma 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 153proof - 154 let ?MM = 4294967296 155 have AL: "uint(word_of_int e::word32) = e" 156 by (rule uint_word_of_int_id[OF \<open>0 <= e\<close> \<open>e <= ?M\<close>]) 157 have CL: "uint(word_of_int b::word32) = b" 158 by (rule uint_word_of_int_id[OF \<open>0 <= b\<close> \<open>b <= ?M\<close>]) 159 have DL: "True" .. 160 have EL: "uint(word_of_int d::word32) = d" 161 by (rule uint_word_of_int_id[OF \<open>0 <= d\<close> \<open>d <= ?M\<close>]) 162 have AR: "uint(word_of_int e'::word32) = e'" 163 by (rule uint_word_of_int_id[OF \<open>0 <= e'\<close> \<open>e' <= ?M\<close>]) 164 have CR: "uint(word_of_int b'::word32) = b'" 165 by (rule uint_word_of_int_id[OF \<open>0 <= b'\<close> \<open>b' <= ?M\<close>]) 166 have DR: "True" .. 167 have ER: "uint(word_of_int d'::word32) = d'" 168 by (rule uint_word_of_int_id[OF \<open>0 <= d'\<close> \<open>d' <= ?M\<close>]) 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 \<open>0 <= a\<close> \<open>a <= ?M\<close> 189 by (simp add: int_mod_eq') 190 have "?X mod ?MM = ?X" using \<open>0 <= ?X\<close> \<open>?X <= ?M\<close> 191 by (simp add: int_mod_eq') 192 have "e mod ?MM = e" using \<open>0 <= e\<close> \<open>e <= ?M\<close> 193 by (simp add: int_mod_eq') 194 have "(?MM::int) = 2 ^ LENGTH(32)" by simp 195 show ?thesis 196 unfolding 197 word_add_def 198 uint_word_of_int_id[OF \<open>0 <= a\<close> \<open>a <= ?M\<close>] 199 uint_word_of_int_id[OF \<open>0 <= ?X\<close> \<open>?X <= ?M\<close>] 200 int_word_uint 201 unfolding \<open>?MM = 2 ^ LENGTH(32)\<close> 202 unfolding word_uint.Abs_norm 203 by (simp add: 204 \<open>a mod ?MM = a\<close> 205 \<open>e mod ?MM = e\<close> 206 \<open>?X mod ?MM = ?X\<close>) 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 \<open>0 <= a'\<close> \<open>a' <= ?M\<close> 229 by (simp add: int_mod_eq') 230 have "?X mod ?MM = ?X" using \<open>0 <= ?X\<close> \<open>?X <= ?M\<close> 231 by (simp add: int_mod_eq') 232 have "e' mod ?MM = e'" using \<open>0 <= e'\<close> \<open>e' <= ?M\<close> 233 by (simp add: int_mod_eq') 234 have "(?MM::int) = 2 ^ LENGTH(32)" by simp 235 have nat_transfer: "79 - nat j = nat (79 - j)" 236 using nat_diff_distrib \<open>0 <= j\<close> \<open>j <= 79\<close> 237 by simp 238 show ?thesis 239 unfolding 240 word_add_def 241 uint_word_of_int_id[OF \<open>0 <= a'\<close> \<open>a' <= ?M\<close>] 242 uint_word_of_int_id[OF \<open>0 <= ?X\<close> \<open>?X <= ?M\<close>] 243 int_word_uint 244 nat_transfer 245 unfolding \<open>?MM = 2 ^ LENGTH(32)\<close> 246 unfolding word_uint.Abs_norm 247 by (simp add: 248 \<open>a' mod ?MM = a'\<close> 249 \<open>e' mod ?MM = e'\<close> 250 \<open>?X mod ?MM = ?X\<close>) 251 qed 252 253 show ?thesis 254 unfolding steps'_step[OF \<open>0 <= j\<close>] 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) 257qed 258 259spark_vc procedure_round_61 260proof - 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 \<open>0 <= ca\<close> \<open>ca <= ?M\<close>] 280 uint_word_of_int_id[OF \<open>0 <= cb\<close> \<open>cb <= ?M\<close>] 281 uint_word_of_int_id[OF \<open>0 <= cc\<close> \<open>cc <= ?M\<close>] 282 uint_word_of_int_id[OF \<open>0 <= cd\<close> \<open>cd <= ?M\<close>] 283 uint_word_of_int_id[OF \<open>0 <= ce\<close> \<open>ce <= ?M\<close>]) 284 let ?rotate_arg_l = 285 "((((ca + f 0 cb cc cd) mod 4294967296 + 286 x (r_l 0)) mod 4294967296 + k_l 0) mod 4294967296)" 287 let ?rotate_arg_r = 288 "((((ca + f 79 cb cc cd) mod 4294967296 + 289 x (r_r 0)) mod 4294967296 + k_r 0) mod 4294967296)" 290 note returns = 291 \<open>wordops__rotate (s_l 0) ?rotate_arg_l = 292 rotate_left (s_l 0) ?rotate_arg_l\<close> 293 \<open>wordops__rotate (s_r 0) ?rotate_arg_r = 294 rotate_left (s_r 0) ?rotate_arg_r\<close> 295 \<open>wordops__rotate 10 cc = rotate_left 10 cc\<close> 296 \<open>f 0 cb cc cd = f_spec 0 cb cc cd\<close> 297 \<open>f 79 cb cc cd = f_spec 79 cb cc cd\<close> 298 \<open>k_l 0 = k_l_spec 0\<close> 299 \<open>k_r 0 = k_r_spec 0\<close> 300 \<open>r_l 0 = r_l_spec 0\<close> 301 \<open>r_r 0 = r_r_spec 0\<close> 302 \<open>s_l 0 = s_l_spec 0\<close> 303 \<open>s_r 0 = s_r_spec 0\<close> 304 305 note x_borders = \<open>\<forall>i. 0 \<le> i \<and> i \<le> 15 \<longrightarrow> 0 \<le> x i \<and> x i \<le> ?M\<close> 306 307 from \<open>0 <= r_l 0\<close> \<open>r_l 0 <= 15\<close> 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 \<open>0 <= r_l 0\<close> \<open>r_l 0 <= 15\<close> 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 \<open>0 <= r_r 0\<close> \<open>r_r 0 <= 15\<close> 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 \<open>0 <= r_r 0\<close> \<open>r_r 0 <= 15\<close> 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 \<comment> \<open>upper bounds\<close> 328 H1 H3 H5 H7 H9 H1 H3 H5 H7 H9 \<comment> \<open>lower bounds\<close> 329 ] 330 from this[OF x_lower x_upper x_lower' x_upper' \<open>0 <= 0\<close> \<open>0 <= 79\<close>] 331 \<open>0 \<le> ca\<close> \<open>0 \<le> ce\<close> x_lower x_lower' 332 show ?thesis unfolding returns(1) returns(2) unfolding returns 333 by (simp del: mod_pos_pos_trivial mod_neg_neg_trivial) 334qed 335 336spark_vc procedure_round_62 337proof - 338 let ?M = "4294967295::int" 339 let ?rotate_arg_l = 340 "((((cla + f (loop__1__j + 1) clb clc cld) mod 4294967296 + 341 x (r_l (loop__1__j + 1))) mod 4294967296 + 342 k_l (loop__1__j + 1)) mod 4294967296)" 343 let ?rotate_arg_r = 344 "((((cra + f (79 - (loop__1__j + 1)) crb crc crd) mod 345 4294967296 + x (r_r (loop__1__j + 1))) mod 4294967296 + 346 k_r (loop__1__j + 1)) mod 4294967296)" 347 348 have s: "78 - loop__1__j = (79 - (loop__1__j + 1))" by simp 349 note returns = 350 \<open>wordops__rotate (s_l (loop__1__j + 1)) ?rotate_arg_l = 351 rotate_left (s_l (loop__1__j + 1)) ?rotate_arg_l\<close> 352 \<open>wordops__rotate (s_r (loop__1__j + 1)) ?rotate_arg_r = 353 rotate_left (s_r (loop__1__j + 1)) ?rotate_arg_r\<close> 354 \<open>f (loop__1__j + 1) clb clc cld = 355 f_spec (loop__1__j + 1) clb clc cld\<close> 356 \<open>f (78 - loop__1__j) crb crc crd = 357 f_spec (78 - loop__1__j) crb crc crd\<close>[simplified s] 358 \<open>wordops__rotate 10 clc = rotate_left 10 clc\<close> 359 \<open>wordops__rotate 10 crc = rotate_left 10 crc\<close> 360 \<open>k_l (loop__1__j + 1) = k_l_spec (loop__1__j + 1)\<close> 361 \<open>k_r (loop__1__j + 1) = k_r_spec (loop__1__j + 1)\<close> 362 \<open>r_l (loop__1__j + 1) = r_l_spec (loop__1__j + 1)\<close> 363 \<open>r_r (loop__1__j + 1) = r_r_spec (loop__1__j + 1)\<close> 364 \<open>s_l (loop__1__j + 1) = s_l_spec (loop__1__j + 1)\<close> 365 \<open>s_r (loop__1__j + 1) = s_r_spec (loop__1__j + 1)\<close> 366 367 note x_borders = \<open>\<forall>i. 0 \<le> i \<and> i \<le> 15 \<longrightarrow> 0 \<le> x i \<and> x i \<le> ?M\<close> 368 369 from \<open>0 <= r_l (loop__1__j + 1)\<close> \<open>r_l (loop__1__j + 1) <= 15\<close> 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 \<open>0 <= r_l (loop__1__j + 1)\<close> \<open>r_l (loop__1__j + 1) <= 15\<close> 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 \<open>0 <= r_r (loop__1__j + 1)\<close> \<open>r_r (loop__1__j + 1) <= 15\<close> 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 \<open>0 <= r_r (loop__1__j + 1)\<close> \<open>r_r (loop__1__j + 1) <= 15\<close> 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 \<open>0 <= loop__1__j\<close> have "0 <= loop__1__j + 1" by simp 386 from \<open>loop__1__j <= 78\<close> 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 \<open>cla <= ?M\<close> 392 \<open>clb <= ?M\<close> 393 \<open>clc <= ?M\<close> 394 \<open>cld <= ?M\<close> 395 \<open>cle <= ?M\<close> 396 \<open>cra <= ?M\<close> 397 \<open>crb <= ?M\<close> 398 \<open>crc <= ?M\<close> 399 \<open>crd <= ?M\<close> 400 \<open>cre <= ?M\<close> 401 402 \<open>0 <= cla\<close> 403 \<open>0 <= clb\<close> 404 \<open>0 <= clc\<close> 405 \<open>0 <= cld\<close> 406 \<open>0 <= cle\<close> 407 \<open>0 <= cra\<close> 408 \<open>0 <= crb\<close> 409 \<open>0 <= crc\<close> 410 \<open>0 <= crd\<close> 411 \<open>0 <= cre\<close>] 412 from this[OF 413 x_lower x_upper x_lower' x_upper' 414 \<open>0 <= loop__1__j + 1\<close> \<open>loop__1__j + 1 <= 79\<close>] 415 \<open>0 \<le> cla\<close> \<open>0 \<le> cle\<close> \<open>0 \<le> cra\<close> \<open>0 \<le> cre\<close> x_lower x_lower' 416 show ?thesis unfolding \<open>loop__1__j + 1 + 1 = loop__1__j + 2\<close> 417 unfolding returns(1) returns(2) unfolding returns 418 by (simp del: mod_pos_pos_trivial mod_neg_neg_trivial) 419 420qed 421 422spark_vc procedure_round_76 423proof - 424 let ?M = "4294967295 :: int" 425 let ?INIT_CHAIN = 426 "\<lparr>h0 = ca_init, h1 = cb_init, 427 h2 = cc_init, h3 = cd_init, 428 h4 = ce_init\<rparr>" 429 have steps_to_steps': 430 "steps 431 (\<lambda>n::nat. word_of_int (x (int n))) 432 (from_chain ?INIT_CHAIN, from_chain ?INIT_CHAIN) 433 80 = 434 from_chain_pair ( 435 steps' 436 (\<lparr>left = ?INIT_CHAIN, right = ?INIT_CHAIN\<rparr>) 437 80 438 x)" 439 unfolding from_to_id by simp 440 from 441 \<open>0 \<le> ca_init\<close> \<open>ca_init \<le> ?M\<close> 442 \<open>0 \<le> cb_init\<close> \<open>cb_init \<le> ?M\<close> 443 \<open>0 \<le> cc_init\<close> \<open>cc_init \<le> ?M\<close> 444 \<open>0 \<le> cd_init\<close> \<open>cd_init \<le> ?M\<close> 445 \<open>0 \<le> ce_init\<close> \<open>ce_init \<le> ?M\<close> 446 \<open>0 \<le> cla\<close> \<open>cla \<le> ?M\<close> 447 \<open>0 \<le> clb\<close> \<open>clb \<le> ?M\<close> 448 \<open>0 \<le> clc\<close> \<open>clc \<le> ?M\<close> 449 \<open>0 \<le> cld\<close> \<open>cld \<le> ?M\<close> 450 \<open>0 \<le> cle\<close> \<open>cle \<le> ?M\<close> 451 \<open>0 \<le> cra\<close> \<open>cra \<le> ?M\<close> 452 \<open>0 \<le> crb\<close> \<open>crb \<le> ?M\<close> 453 \<open>0 \<le> crc\<close> \<open>crc \<le> ?M\<close> 454 \<open>0 \<le> crd\<close> \<open>crd \<le> ?M\<close> 455 \<open>0 \<le> cre\<close> \<open>cre \<le> ?M\<close> 456 show ?thesis 457 unfolding round_def 458 unfolding steps_to_steps' 459 unfolding H1[symmetric] 460 by (simp add: uint_word_ariths(1) mod_simps 461 uint_word_of_int_id) 462qed 463 464spark_end 465 466end 467