1(*===========================================================================*) 2(* Secure Hash Algorithm *) 3(* *) 4(* HOL version of an ML implementation by Hiro Kuwahara. See also *) 5(* *) 6(* http://www.itl.nist.gov/fipspubs/fip180-1.htm *) 7(* *) 8(*===========================================================================*) 9 10(*****************************************************************************) 11(* NOTE: this file has been only partly translated to wordsLib. It won't *) 12(* work until further repairs are made. *) 13(*****************************************************************************) 14 15app load ["pairTools", "wordsLib", "stringLib"]; 16 17open stringTheory arithmeticTheory; 18 19numLib.prefer_num(); 20 21(* 22wordLib.pp_word_unsigned_hex(); 23word32Lib.pp_word_unsigned_hex(); 24*) 25 26val lemma = Q.prove 27(`!n L. n <= LENGTH L ==> n-1 <= LENGTH (TL L)`, 28 Induct_on `L` THEN RW_TAC list_ss []); 29 30 31(*---------------------------------------------------------------------------*) 32(* Some support stuff on lists, in particular a definition of TAKE. *) 33(*---------------------------------------------------------------------------*) 34 35val TAKE_def = 36 Define 37 `TAKE n L = 38 if n = 0 then ([],L) 39 else let (front,back) = TAKE (n-1) (TL L) 40 in (HD L::front,back)`; 41 42val TAKE_ind = fetch "-" "TAKE_ind"; 43 44val TAKE_THM = Q.prove 45(`!n L taken left. 46 n <= LENGTH L /\ ((taken,left) = TAKE n L) 47 ==> (taken ++ left = L) /\ (LENGTH taken = n)`, 48 recInduct TAKE_ind THEN REPEAT GEN_TAC THEN STRIP_TAC 49 THEN ONCE_REWRITE_TAC [TAKE_def] 50 THEN REPEAT GEN_TAC THEN COND_CASES_TAC THENL 51 [RW_TAC list_ss [] THEN RW_TAC list_ss [], 52 pairTools.LET_EQ_TAC [pairTheory.LET2_RATOR,pairTheory.LET2_RAND] 53 THEN RW_TAC list_ss [] 54 THEN FULL_SIMP_TAC list_ss [lemma] THENL 55 [MATCH_MP_TAC listTheory.CONS 56 THEN Cases_on `L` 57 THEN FULL_SIMP_TAC list_ss [], 58 RES_TAC THEN RW_TAC list_ss []]]); 59 60(*---------------------------------------------------------------------------*) 61(* Misc. support for 8 bit bytes and 32 bit words. *) 62(*---------------------------------------------------------------------------*) 63 64(*---------------------------------------------------------------------------*) 65(* Left rotate a word *) 66(*---------------------------------------------------------------------------*) 67 68val rotl32_def = Define 69 `rotl_w32 (a:word32) (b:num) = a #>> (32 - b)`; 70 71val _ = set_fixity "<<#" (Infixl 680); 72val _ = temp_overload_on ("<<#", Term `$rotl_w32`); 73 74(*---------------------------------------------------------------------------*) 75(* Trivial abbreviations. *) 76(*---------------------------------------------------------------------------*) 77(* 78val W8 = Define `W8 = word8$n2w`; 79val W32 = Define `W32 = word32$n2w`; 80*) 81(*---------------------------------------------------------------------------*) 82(* 64 copies of ZERO (W32) *) 83(*---------------------------------------------------------------------------*) 84 85val ZEROx64_def = 86 Define 87 `ZEROx64 = [0w; 0w; 0w; 0w; 0w; 0w; 0w; 0w; 88 0w; 0w; 0w; 0w; 0w; 0w; 0w; 0w; 89 0w; 0w; 0w; 0w; 0w; 0w; 0w; 0w; 90 0w; 0w; 0w; 0w; 0w; 0w; 0w; 0w; 91 0w; 0w; 0w; 0w; 0w; 0w; 0w; 0w; 92 0w; 0w; 0w; 0w; 0w; 0w; 0w; 0w; 93 0w; 0w; 0w; 0w; 0w; 0w; 0w; 0w; 94 0w; 0w; 0w; 0w; 0w; 0w; 0w; 0w] : word32 list`; 95 96(*---------------------------------------------------------------------------*) 97(* Convert from 8 bits to 32 bits *) 98(*---------------------------------------------------------------------------*) 99 100val w8to32 = Define `w8to32 word8 = W32(word8$w2n word8)`; 101 102(*---------------------------------------------------------------------------*) 103(* word32 <--> (word8 # word8 # word8 # word8) *) 104(*---------------------------------------------------------------------------*) 105 106val w8x4to32_def = 107 Define 108 `w8x4to32 w1 w2 w3 w4 = (w8to32(w1) << 24n) | (w8to32(w2) << 16n) | 109 (w8to32(w3) << 8n) | w8to32(w4)`; 110val w32to8x4_def = 111 Define 112 `w32to8x4 w = (W8 (word32$w2n((w:word32) >>> 24n)), 113 W8 (word32$w2n(w >>> 16n)), 114 W8 (word32$w2n(w >>> 8n)), 115 W8 (word32$w2n(w)))` ; 116 117val w32List_def = 118 Define 119 `(w32List (b1::b2::b3::b4::t) = w8x4to32 b1 b2 b3 b4::w32List t) /\ 120 (w32List other = [])`; 121 122val w8List_def = 123 Define 124 `(w8List [] = []) /\ 125 (w8List (h::t) = let (b1,b2,b3,b4) = w32to8x4 h in b1::b2::b3::b4::w8List t)`; 126 127(*---------------------------------------------------------------------------*) 128(* Translate 5 32 bit words to a 20-tuple of 8-bit words. *) 129(*---------------------------------------------------------------------------*) 130 131val w32x5to8_def = 132 Define 133 `w32x5to8 (w1,w2,w3,w4,w5) = 134 let (w1b1,w1b2,w1b3,w1b4) = w32to8x4 w1 in 135 let (w2b1,w2b2,w2b3,w2b4) = w32to8x4 w2 in 136 let (w3b1,w3b2,w3b3,w3b4) = w32to8x4 w3 in 137 let (w4b1,w4b2,w4b3,w4b4) = w32to8x4 w4 in 138 let (w5b1,w5b2,w5b3,w5b4) = w32to8x4 w5 139 in 140 (w1b1,w1b2,w1b3,w1b4,w2b1,w2b2,w2b3,w2b4, 141 w3b1,w3b2,w3b3,w3b4,w4b1,w4b2,w4b3,w4b4,w5b1,w5b2,w5b3,w5b4)`; 142 143 144(*---------------------------------------------------------------------------*) 145(* Padding *) 146(*---------------------------------------------------------------------------*) 147 148val div64 = CONV_RULE EVAL (Q.SPEC `64n` arithmeticTheory.DIVISION); 149val ndiv64 = Q.SPEC `n` div64; 150val n1div64 = Q.SPEC `n+1` div64; 151val swap_lem = 152 DECIDE (Term `!a b c d : num. a < b /\ c < d ==> (b-a < d-c = b+c < d+a)`); 153 154(*---------------------------------------------------------------------------*) 155(* Gross termination proof. Would be better in the integers. *) 156(*---------------------------------------------------------------------------*) 157 158val (appendPaddingBitsHelper_def, 159 appendPaddingBitsHelper_ind) = 160Defn.tprove 161(Hol_defn 162 "appendPaddingBitsHelper" 163 `appendPaddingBitsHelper n : word8 list = 164 if n MOD 64 = 56 then [] 165 else word8$word_0::appendPaddingBitsHelper (n+1)`, 166 WF_REL_TAC 167 `measure \n. if n MOD 64 <= 56 then 56 - n MOD 64 else 120 - n MOD 64` 168 THEN RW_TAC std_ss [] THENL 169 [`n MOD 64 < 56` by DECIDE_TAC 170 THEN WEAKEN_TAC (equal (Term `n MOD 64 <= 56`)) 171 THEN WEAKEN_TAC (equal (Term `~(n MOD 64 = 56)`)) 172 THEN FULL_SIMP_TAC std_ss [LESS_OR_EQ] THENL 173 [RW_TAC arith_ss [swap_lem] 174 THEN Induct_on `n DIV 64` THEN RW_TAC std_ss [] THENL 175 [MP_TAC ndiv64 176 THEN Q.PAT_ASSUM `x = y` (SUBST_ALL_TAC o SYM) 177 THEN RW_TAC arith_ss [] 178 THEN `(n=63) \/ n<63` by DECIDE_TAC THEN FULL_SIMP_TAC arith_ss [], 179 Q.PAT_ASSUM `$!M` (MP_TAC o Q.SPEC `v * 64n + n MOD 64`) 180 THEN RW_TAC arith_ss [] 181 THEN FULL_SIMP_TAC arith_ss [ADD_DIV_ADD_DIV] 182 THEN `n MOD 64 DIV 64 = 0` by RW_TAC arith_ss [LESS_DIV_EQ_ZERO] 183 THEN FULL_SIMP_TAC std_ss [] 184 THEN `(v * 64 + n MOD 64) MOD 64 = n MOD 64` 185 by RW_TAC arith_ss [MOD_MULT] 186 THEN FULL_SIMP_TAC arith_ss [] 187 THEN `(v * 64 + (n MOD 64 + 1)) MOD 64 = n MOD 64 + 1` 188 by RW_TAC arith_ss [MOD_MULT] 189 THEN `n MOD 64 + 1 = (n+1) MOD 64` 190 by RW_TAC arith_ss [Once (GSYM MOD_PLUS)] 191 THEN FULL_SIMP_TAC arith_ss []], 192 DECIDE_TAC], 193 ASSUME_TAC (CONJUNCT2 ndiv64) THEN DECIDE_TAC, 194 FULL_SIMP_TAC arith_ss [Once (GSYM MOD_PLUS)], 195 `56 < n MOD 64 /\ n MOD 64 < 64` by RW_TAC arith_ss [ndiv64] THEN 196 `56 < (n+1) MOD 64 /\ (n+1) MOD 64 < 64` by RW_TAC arith_ss [n1div64] 197 THEN REPEAT (WEAKEN_TAC is_neg) 198 THEN RW_TAC arith_ss [swap_lem] 199 THEN FULL_SIMP_TAC arith_ss [Once (GSYM MOD_PLUS)] 200 THEN `(n MOD 64 = 57) \/ (n MOD 64 = 58) \/ (n MOD 64 = 59) \/ 201 (n MOD 64 = 60) \/ (n MOD 64 = 61) \/ (n MOD 64 = 62) \/ 202 (n MOD 64 = 63)` by DECIDE_TAC THEN FULL_SIMP_TAC arith_ss []]); 203 204 205val computePaddingBits = 206 Define 207 `computePaddingBits len : word8 list = 208 W8(128)::appendPaddingBitsHelper (len+1n)`; 209 210val computeLengthBitsHelper_def = 211 Define 212 `computeLengthBitsHelper(len,i) = 213 if i = 0 then [] 214 else W8(word32$WORD_BITS 7 0 (W32 len >> ((i-1)*8))) 215 ::computeLengthBitsHelper(len,i-1)`; 216 217val computeLengthBits_def = 218 Define 219 `computeLengthBits len = computeLengthBitsHelper(len * 8n, 8)`; 220 221val appendPadding_def = 222 Define 223 `appendPadding input = 224 let len = LENGTH input 225 in input <> computePaddingBits(len) <> computeLengthBits(len)`; 226 227 228(*---------------------------------------------------------------------------*) 229(* There are 4 highly similar rounds of computation, each consisting of 20 *) 230(* highly similar steps. Higher order functions to the rescue! *) 231(*---------------------------------------------------------------------------*) 232 233val f1_def = Define `f1(a,b,c) = (c # (a & (b # c))) + W32 1518500249`; 234val f2_def = Define `f2(a,b,c) = (a # b # c) + W32 1859775393`; 235val f3_def = Define `f3(a,b,c) = ((a & b) | (c & (a | b))) + W32 2400959708`; 236val f4_def = Define `f4(a,b,c) = (a # b # c) + W32 3395469782`; 237 238 239val Helper_def = 240 Define 241 `Helper f n (a,b,c,d,e) w = 242 case n of 243 0 -> (a,(b <<# 30n),c,d,e+(a <<# 5n)+f(b,c,d)+w) 244 1 -> ((a <<# 30n),b,c,d+(e <<# 5n)+f(a,b,c)+w,e) 245 2 -> (a,b,c+(d <<# 5n)+f(e,a,b)+w,d,e <<# 30n) 246 3 -> (a,b+(c <<# 5n)+f(d,e,a)+w,c,d <<# 30n,e) 247 _ -> (a+(b <<# 5n)+f(c,d,e)+w,b,c <<# 30n,d,e)`; 248 249val Round_def = 250 Define 251 `(Round _ _ args [] = (args,[])) /\ 252 (Round helper i args (w::t) = 253 if i<20 then Round helper (i+1) (helper (i MOD 5) args w) t 254 else (args, w::t))`; 255 256val expand_def = 257 Define 258 `(expand (w0::w1::w2::w3::w4::w5::w6::w7::w8::w9:: 259 w10::w11::w12::w13::w14::w15::w16::t) 260 = let j = (w0 # w2 # w8 # w13) <<# 1n 261 in w0::expand(w1::w2::w3::w4::w5::w6::w7::w8:: 262 w9::w10::w11::w12::w13::w14::w15::j::t)) 263/\ (expand wlist = wlist)`; 264 265 266(*---------------------------------------------------------------------------*) 267(* Digest a block *) 268(*---------------------------------------------------------------------------*) 269 270val digestBlock_def = 271 Define 272 `digestBlock (block:word8 list) (h0,h1,h2,h3,h4) = 273 let wlist = expand (w32List block ++ ZEROx64) in 274 let (hbar1,wlist1) = Round (Helper f1) 0 (h0,h1,h2,h3,h4) wlist in 275 let (hbar2,wlist2) = Round (Helper f2) 0 hbar1 wlist1 in 276 let (hbar3,wlist3) = Round (Helper f3) 0 hbar2 wlist2 in 277 let (hbar4,wlist4) = Round (Helper f4) 0 hbar3 wlist3 in 278 let (a,b,c,d,e) = hbar4 279 in 280 (h0+a, h1+b, h2+c, h3+d, h4+e)`; 281 282(*---------------------------------------------------------------------------*) 283(* The LENGTH check is needed for termination proof. *) 284(*---------------------------------------------------------------------------*) 285 286val (digest_def,digest_ind) = Defn.tprove 287(Hol_defn 288 "digest" 289 `digest message Hbar = 290 if LENGTH message < 64 then Hbar 291 else let (next, rest) = TAKE 64 message 292 in digest rest (digestBlock next Hbar)`, 293 WF_REL_TAC `measure (LENGTH o FST)` 294 THEN RW_TAC list_ss [] 295 THEN `64 <= LENGTH message` by DECIDE_TAC 296 THEN IMP_RES_TAC TAKE_THM 297 THEN RW_TAC list_ss []); 298 299(*---------------------------------------------------------------------------*) 300(* Main entrypoint: compute the whole message digest *) 301(*---------------------------------------------------------------------------*) 302 303val H0_def = Define `H0 = W32 1732584193`; 304val H1_def = Define `H1 = W32 4023233417`; 305val H2_def = Define `H2 = W32 2562383102`; 306val H3_def = Define `H3 = W32 271733878`; 307val H4_def = Define `H4 = W32 3285377520`; 308 309val computeMD_def = 310 Define 311 `computeMD input = 312 let paddedMessage = appendPadding input in 313 let (a,b,c,d,e) = digest paddedMessage (H0,H1,H2,H3,H4) 314 in w32x5to8 (a,b,c,d,e)`; 315 316 317(*---------------------------------------------------------------------------*) 318(* Tests (currently need bespoke compset) *) 319(*---------------------------------------------------------------------------*) 320 321val char_to_w8_def = 322 Define 323 `char_to_w8 c = W8 (ORD c)`; 324 325val string_to_w8_list_def = 326 Define 327 `string_to_w8_list s = MAP char_to_w8 (EXPLODE s)`; 328 329val string_to_w8_thms = [char_to_w8_def, string_to_w8_list_def]; 330 331val pairs_and_lists = let open pairTheory listTheory 332 in 333 [CLOSED_PAIR_EQ, FST, SND,pair_case_thm, 334 CURRY_DEF,UNCURRY_DEF,PAIR_MAP_THM, 335 numeralTheory.numeral_funpow, (* LET_THM, *) 336 APPEND,APPEND_NIL, FLAT, HD, TL, 337 LENGTH, MAP, MAP2, NULL_DEF, MEM, EXISTS_DEF, 338 EVERY_DEF, ZIP, UNZIP, FILTER, FOLDL, FOLDR, 339 FOLDL, REVERSE_DEF, EL_compute, ALL_DISTINCT, 340 computeLib.lazyfy_thm list_case_compute, 341 list_size_def,FRONT_DEF,LAST_DEF] 342 end; 343 344val string_thms = let open stringTheory 345 in [ORD_CHR_COMPUTE,CHR_ORD,STRING_CASE_DEF,STRLEN_DEF, 346 EXPLODE_EQNS,IMPLODE_EQNS,STRCAT_EQNS] 347 end; 348 349val word8thms = 350 let open bitsTheory numeral_bitsTheory word8Theory 351 val THE_WL = SIMP_RULE arith_ss [HB_def,arithmeticTheory.ADD1] WL_def 352 val MOD_WL_EVAL = REWRITE_RULE [THE_WL,GSYM MOD_2EXP_def] MOD_WL_def; 353 val RRX_EVAL2 = GEN_ALL (REWRITE_RULE 354 [GSYM DIV2_def,RRXn_def,LSR_ONE_def,HB_def] RRX_EVAL); 355 val LT_EVAL = REWRITE_RULE [MSBn_def,THE_WL,MOD_WL_EVAL] LT_EVAL; 356 val LE_EVAL = REWRITE_RULE [MSBn_def,THE_WL,MOD_WL_EVAL] LE_EVAL; 357 val GT_EVAL = REWRITE_RULE [MSBn_def,THE_WL,MOD_WL_EVAL] GT_EVAL; 358 val GE_EVAL = REWRITE_RULE [MSBn_def,THE_WL,MOD_WL_EVAL] GE_EVAL; 359 val LO_EVAL = REWRITE_RULE [MOD_WL_EVAL] LO_EVAL; 360 val LS_EVAL = REWRITE_RULE [MOD_WL_EVAL] LS_EVAL; 361 val HI_EVAL = REWRITE_RULE [MOD_WL_EVAL] HI_EVAL; 362 val HS_EVAL = REWRITE_RULE [MOD_WL_EVAL] HS_EVAL; 363 in 364 [LT_EVAL, LE_EVAL, GT_EVAL, GE_EVAL, 365 LO_EVAL, LS_EVAL, HI_EVAL, HS_EVAL, 366 THE_WL, HB_def, word_0, word_1, word_L_def, word_H_def, word_T, 367 MOD_WL_EVAL, w2n_EVAL, n2w_11, 368 OR_def, AND_def, EOR_def, TWO_COMP_def, ONE_COMP_def, RRX_def,MSB_def, 369 ADD_EVAL, MUL_EVAL, word_sub, 370 ONE_COMP_EVAL, TWO_COMP_EVAL, 371 AND_EVAL, OR_EVAL, EOR_EVAL, 372 LSL_EVAL, LSR_THM, ASR_THM, ROR_THM, RRX_EVAL, 373 WORD_BIT_def, WORD_BITS_def, WORD_SLICE_def, 374 MSB_EVAL, LSB_EVAL, 375 iBITWISE, NUMERAL_BITWISE, NUMERAL_DIV2, SIGN_EXTEND_def, 376 DIVMOD_2EXP, iMOD_2EXP, NUMERAL_MOD_2EXP, NUMERAL_DIV_2EXP,TIMES_2EXP_def, 377 MSBn_def, LSBn_def, BITV_def, SBIT_def, BITS_def, BIT_def, SLICE_def] 378 end; 379 380val word32thms = 381let open bitsTheory numeral_bitsTheory word32Theory 382 val THE_WL = SIMP_RULE arith_ss [HB_def,arithmeticTheory.ADD1] WL_def 383 val MOD_WL_EVAL = REWRITE_RULE [THE_WL,GSYM MOD_2EXP_def] MOD_WL_def; 384 val LT_EVAL = REWRITE_RULE [MSBn_def,THE_WL,MOD_WL_EVAL] LT_EVAL; 385 val LE_EVAL = REWRITE_RULE [MSBn_def,THE_WL,MOD_WL_EVAL] LE_EVAL; 386 val GT_EVAL = REWRITE_RULE [MSBn_def,THE_WL,MOD_WL_EVAL] GT_EVAL; 387 val GE_EVAL = REWRITE_RULE [MSBn_def,THE_WL,MOD_WL_EVAL] GE_EVAL; 388 val LO_EVAL = REWRITE_RULE [MOD_WL_EVAL] LO_EVAL; 389 val LS_EVAL = REWRITE_RULE [MOD_WL_EVAL] LS_EVAL; 390 val HI_EVAL = REWRITE_RULE [MOD_WL_EVAL] HI_EVAL; 391 val HS_EVAL = REWRITE_RULE [MOD_WL_EVAL] HS_EVAL; 392 in 393 [LT_EVAL, LE_EVAL, GT_EVAL, GE_EVAL,LO_EVAL, LS_EVAL, HI_EVAL, HS_EVAL, 394 THE_WL, HB_def, word_0, word_1, word_L_def, word_H_def, word_T, 395 MOD_WL_EVAL, w2n_EVAL, n2w_11, 396 OR_def, AND_def, EOR_def, TWO_COMP_def, ONE_COMP_def, RRX_def,MSB_def, 397 ADD_EVAL, MUL_EVAL, word_sub,ONE_COMP_EVAL, TWO_COMP_EVAL, 398 AND_EVAL, OR_EVAL, EOR_EVAL,LSL_EVAL, LSR_THM, ASR_THM, ROR_THM, RRX_EVAL, 399 WORD_BIT_def, WORD_BITS_def, WORD_SLICE_def, 400 MSB_EVAL, LSB_EVAL, 401 iBITWISE, NUMERAL_BITWISE, NUMERAL_DIV2, SIGN_EXTEND_def, 402 DIVMOD_2EXP, iMOD_2EXP, NUMERAL_MOD_2EXP, NUMERAL_DIV_2EXP,TIMES_2EXP_def, 403 MSBn_def, LSBn_def, BITV_def, SBIT_def, BITS_def, BIT_def, SLICE_def] 404 end; 405 406 407val sha1thms = 408 [TAKE_def,rotl32_def, W8, W32, ZERO_def,ZEROx64_def, 409 w8to32, w8x4to32_def, w32to8x4_def, 410 w32List_def, w8List_def, w32x5to8_def,appendPaddingBitsHelper_def, 411 computePaddingBits, computeLengthBitsHelper_def,computeLengthBits_def, 412 appendPadding_def, f1_def, f2_def, f3_def, f4_def, 413 Helper_def, Round_def,expand_def, 414 digestBlock_def,digest_def,H0_def,H1_def,H2_def,H3_def,H4_def,computeMD_def]; 415 416val compset = reduceLib.num_compset(); 417 418val _ = try (computeLib.add_thms 419 (string_to_w8_thms @ string_thms @ pairs_and_lists @ 420 word8thms @ word32thms @ sha1thms)) 421 compset; 422 423val SHA1_CONV = computeLib.WEAK_CBV_CONV compset; 424 425(* 426val thm1 = SHA1_CONV (Term `appendPadding (string_to_w8_list "abc")`); 427val thm2 = SHA1_CONV (Term `LENGTH (appendPadding (string_to_w8_list "abc")) < 64`); 428val thm3 = SHA1_CONV (Term 429 `let (next,rest) = TAKE 64 (appendPadding (string_to_w8_list "abc")) in 430 let block1 = expand (w32List next <> ZEROx64) 431 in block1`); 432 433val thm4a = SHA1_CONV (Term 434 `let (next,rest) = TAKE 64 (appendPadding (string_to_w8_list "abc")) in 435 let block1 = expand (w32List next <> ZEROx64) in 436 doRound (Helper f1) 0 (H0,H1,H2,H3,H4) block1`); 437 438val thm4 = SHA1_CONV (Term 439 `let (next,rest) = TAKE 64 (appendPadding (string_to_w8_list "abc")) in 440 let block1 = expand (w32List next <> ZEROx64) in 441 doRound (Helper f1) 0 (H0,H1,H2,H3,H4) block1`); 442 443(* full computation *) 444val thm5 = Count.apply SHA1_CONV (Term `computeMD (string_to_w8_list "abc")`); 445 446 447(* Trying to deal with symbolic execution ... things get big *) 448 449infix Orelse; 450fun (p Orelse q) x = p x orelse q x; 451 452fun OR [] = K false 453 | OR [x] = same_const x 454 | OR (h::t) = same_const h Orelse OR t; 455 456fun RESTR_SHA_CONV clist = 457 Lib.with_flag (computeLib.stoppers,SOME (OR clist)) SHA1_CONV; 458 459val RESTR_SHA_TAC = Tactic.CONV_TAC o RESTR_SHA_CONV; 460val RESTR_SHA_RULE = Conv.CONV_RULE o RESTR_SHA_CONV; 461 462val thm = Count.apply SHA1_CONV 463 (Term `computeMD [W8 (ORD c1); W8 (ORD c2); W8 (ORD c3)]`); 464 465val thm' = Count.apply SHA1_CONV 466 (Term `computeMD ((W8 (ORD c)::string_to_w8_list "bc"))`); 467 468max_print_depth := 7; 469 470g `?c. computeMD ((W8 (ORD c)::string_to_w8_list "bc")) = 471 computeMD (string_to_w8_list "abc")`; 472e (SUBST_TAC [thm5]); 473e (CONV_TAC (QUANT_CONV (LHS_CONV SHA1_CONV))) 474 475e (REWRITE_TAC [thm5, thm]); 476 477- val M = mk_eq (rhs(concl thm'),rhs(concl thm5)); 478- set_goal ([], M); 479e (ONCE_REWRITE_TAC [pairTheory.PAIR_EQ]); 480e CONJ_TAC; 481max_print_depth := 20; 482val N = snd(top_goal()); 483set_goal([],N); 484 485val lem = Q.prove 486(`MOD_2EXP 8 (ORD c) = ORD c`, 487 RW_TAC arith_ss [bitsTheory.MOD_2EXP_def,stringTheory.ORD_BOUND]); 488 489g `FST(computeMD ((W8 (ORD c)::string_to_w8_list "bc"))) = 490 FST(computeMD (string_to_w8_list "abc"))`; 491e (SUBST_TAC [thm5]); 492e (CONV_TAC (LHS_CONV SHA1_CONV)); 493e EVAL_TAC; 494 495*) 496 497