1(* ========================================================================= *) 2(* miller_rabin_def theory *) 3(* ========================================================================= *) 4 5(* ------------------------------------------------------------------------- *) 6(* Load and open relevant theories. *) 7(* (Comment out "load"s and "quietdec"s for compilation.) *) 8(* ------------------------------------------------------------------------- *) 9(* 10*) 11 12val () = loadPath := ["../../miller/ho_prover", 13 "../../miller/subtypes", 14 "../../miller/RSA", 15 "../../miller/formalize", 16 "../../miller/prob", 17 "../../miller/groups", 18 "../../miller/miller", 19 "../ml"] @ !loadPath; 20val () = app load 21 ["bossLib", "metisLib", "RealArith", 22 "pairTheory", "combinTheory", "listTheory", "arithmeticTheory", 23 "state_transformerTheory", 24 "miller_rabinTheory", 25 "encodeLib"]; 26val () = quietdec := true; 27 28open HolKernel Parse boolLib bossLib metisLib; 29open pairTheory combinTheory listTheory arithmeticTheory; 30open state_transformerTheory; 31open miller_rabinTheory; 32open encodeLib; 33 34(* 35*) 36val () = quietdec := false; 37 38(* ------------------------------------------------------------------------- *) 39(* Start a new theory called "miller_rabin_def". *) 40(* ------------------------------------------------------------------------- *) 41 42val _ = new_theory "miller_rabin_def"; 43 44(* ------------------------------------------------------------------------- *) 45(* Helper proof tools. *) 46(* ------------------------------------------------------------------------- *) 47 48val arith_ss = bossLib.arith_ss ++ boolSimps.LET_ss; 49 50infixr 0 << 51infixr 1 ++ || THENC ORELSEC ORELSER ## orelse_bdd_conv 52infix 2 >> 53 54val op ++ = op THEN; 55val op << = op THENL; 56val op >> = op THEN1; 57val op || = op ORELSE; 58val Know = Q_TAC KNOW_TAC; 59val Suff = Q_TAC SUFF_TAC; 60 61(* ------------------------------------------------------------------------- *) 62(* Helper theorems *) 63(* ------------------------------------------------------------------------- *) 64 65(*** 66val DIV_THEN_MULT = store_thm 67 ("DIV_THEN_MULT", 68 ``!p q. SUC q * (p DIV SUC q) <= p``, 69 NTAC 2 STRIP_TAC 70 ++ Know `?r. p = (p DIV SUC q) * SUC q + r` 71 >> (Know `0 < SUC q` >> DECIDE_TAC 72 ++ PROVE_TAC [DIVISION]) 73 ++ STRIP_TAC 74 ++ Suff `p = SUC q * (p DIV SUC q) + r` 75 >> (POP_ASSUM_LIST (K ALL_TAC) ++ DECIDE_TAC) 76 ++ PROVE_TAC [MULT_COMM]); 77 78val DIVISION_TWO = store_thm 79 ("DIVISION_TWO", 80 ``!n. (n = 2 * (n DIV 2) + (n MOD 2)) /\ ((n MOD 2 = 0) \/ (n MOD 2 = 1))``, 81 STRIP_TAC 82 ++ MP_TAC (Q.SPEC `2` DIVISION) 83 ++ Know `0:num < 2` >> DECIDE_TAC 84 ++ DISCH_THEN (fn th => REWRITE_TAC [th]) 85 ++ DISCH_THEN (MP_TAC o Q.SPEC `n`) 86 ++ RW_TAC bool_ss [] << 87 [PROVE_TAC [MULT_COMM], 88 DECIDE_TAC]); 89 90val DIV_TWO = store_thm 91 ("DIV_TWO", 92 ``!n. n = 2 * (n DIV 2) + (n MOD 2)``, 93 PROVE_TAC [DIVISION_TWO]); 94 95val MOD_TWO = store_thm 96 ("MOD_TWO", 97 ``!n. n MOD 2 = if EVEN n then 0 else 1``, 98 STRIP_TAC 99 ++ MP_TAC (Q.SPEC `n` DIVISION_TWO) 100 ++ STRIP_TAC << 101 [Q.PAT_ASSUM `n = X` MP_TAC 102 ++ RW_TAC std_ss [] 103 ++ PROVE_TAC [EVEN_DOUBLE, ODD_EVEN, ADD_CLAUSES], 104 Q.PAT_ASSUM `n = X` MP_TAC 105 ++ RW_TAC std_ss [] 106 ++ PROVE_TAC [ODD_DOUBLE, ODD_EVEN, ADD1]]); 107***) 108 109(* ------------------------------------------------------------------------- *) 110(* Definitions to port to ACL2. *) 111(* ------------------------------------------------------------------------- *) 112 113val (log2_def,log2_ind) = 114 (extra_numTheory.log2_def,extra_numTheory.log2_ind); 115 116(*** 117 Defn.tprove 118 let 119 val d = 120 Hol_defn "log2" 121 `(log2 0 = 0) /\ 122 (log2 n = SUC (log2 (n DIV 2)))` 123 124 val g = `measure (\x. x)` 125 in 126 (d, 127 WF_REL_TAC g 128 ++ STRIP_TAC 129 ++ Know `2 * (SUC v DIV 2) <= SUC v` 130 >> PROVE_TAC [TWO, DIV_THEN_MULT] 131 ++ DECIDE_TAC) 132 end; 133 134val _ = save_thm ("log2_def", log2_def); 135val _ = save_thm ("log2_ind", log2_ind); 136***) 137 138val log2a_def = Define ` 139 (log2a 0 _ = 0) /\ 140 (log2a _ 0 = 0) /\ 141 (log2a (SUC a) b = SUC (log2a a (b DIV 2)))`; 142 143val log2a_lemma = prove(``!x y. x <= y ==> (log2 x = log2a y x)``, 144 GEN_TAC ++ completeInduct_on `x` ++ 145 Cases ++ Cases_on `x` ++ RW_TAC arith_ss [log2a_def,log2_def] ++ 146 PAT_ASSUM ``!a:num.P`` (STRIP_ASSUME_TAC o SPEC ``SUC n' DIV 2``) ++ 147 FULL_SIMP_TAC arith_ss [DIV_LT_X,DIV_LE_X,DECIDE ``0 < 2n``]); 148 149val log2a_proof = store_thm("log2a_proof",``!x. log2 x = log2a x x``,RW_TAC arith_ss [log2a_lemma]); 150 151val (factor_twos_def,factor_twos_ind) = 152 (miller_rabinTheory.factor_twos_def,miller_rabinTheory.factor_twos_ind); 153(*** 154 Defn.tprove 155 let 156 val d = 157 Hol_defn "factor_twos" 158 `factor_twos n = 159 if 0 < n /\ EVEN n then 160 let (r,s) = factor_twos (n DIV 2) in (SUC r, s) 161 else (0, n)` 162 163 val g = `measure (\x. x)` 164 in 165 (d, 166 WF_REL_TAC g 167 ++ RW_TAC arith_ss [] 168 ++ Know `2 * (n DIV 2) <= n` 169 >> PROVE_TAC [TWO, DIV_THEN_MULT] 170 ++ DECIDE_TAC) 171 end; 172 173val _ = save_thm ("factor_twos_def", factor_twos_def); 174val _ = save_thm ("factor_twos_ind", factor_twos_ind); 175***) 176 177val factor_twosa_def = Define ` 178 (factor_twosa 0 _ = (0, 0)) /\ 179 (factor_twosa (SUC a) n = 180 if 0 < n /\ EVEN n then 181 let (r,s) = factor_twosa a (n DIV 2) in (SUC r, s) 182 else (0,n))`; 183 184val factor_twosa_lemma = prove(``!x y. x <= y ==> (factor_twos x = factor_twosa y x)``, 185 GEN_TAC ++ completeInduct_on `x` ++ 186 Cases ++ Cases_on `x` ++ ONCE_REWRITE_TAC [factor_twos_def] ++ 187 RW_TAC arith_ss [factor_twosa_def] ++ 188 PAT_ASSUM ``!a:num.P`` (STRIP_ASSUME_TAC o SPEC ``SUC n' DIV 2``) ++ 189 FULL_SIMP_TAC arith_ss [DIV_LT_X,DIV_LE_X,DECIDE ``0 < 2n``] ++ 190 POP_ASSUM (STRIP_ASSUME_TAC o SPEC ``n:num``) ++ 191 FULL_SIMP_TAC arith_ss []); 192 193val factor_twosa_proof = store_thm("factor_twosa_proof",``!x. factor_twos x = factor_twosa x x``, 194 RW_TAC arith_ss [factor_twosa_lemma]); 195 196val (modexp_def,modexp_ind) = 197 (miller_rabinTheory.modexp_def,miller_rabinTheory.modexp_ind); 198(*** 199 Defn.tprove 200 let 201 val d = 202 Hol_defn "modexp" 203 `modexp n a b = 204 if b = 0 then 1 205 else 206 let r = modexp n a (b DIV 2) in 207 let r2 = (r * r) MOD n in 208 if EVEN b then r2 else (r2 * a) MOD n` 209 210 val g = `measure (\(x,y,z). z)` 211 in 212 (d, 213 WF_REL_TAC g 214 ++ RW_TAC arith_ss [] 215 ++ Know `2 * (b DIV 2) <= b` 216 >> PROVE_TAC [TWO, DIV_THEN_MULT] 217 ++ DECIDE_TAC) 218 end; 219 220val _ = save_thm ("modexp_def", modexp_def); 221val _ = save_thm ("modexp_ind", modexp_ind); 222***) 223 224val modexpa_def = Define ` 225 (modexpa 0 n a b = 1) /\ 226 (modexpa _ _ _ 0 = 1) /\ 227 (modexpa (SUC v) n a b = 228 let r = modexpa v n a (b DIV 2) in 229 let r2 = (r * r) MOD n in 230 if EVEN b then r2 else (r2 * a) MOD n)`; 231 232val modexpa_lemma = prove(``!x y n a. x <= y ==> (modexp n a x = modexpa y n a x)``, 233 GEN_TAC ++ completeInduct_on `x` ++ 234 Cases ++ Cases_on `x` ++ ONCE_REWRITE_TAC [modexp_def] ++ 235 RW_TAC arith_ss [modexpa_def] ++ 236 PAT_ASSUM ``!a:num.P`` (STRIP_ASSUME_TAC o SPEC ``SUC n' DIV 2``) ++ 237 FULL_SIMP_TAC arith_ss [DIV_LT_X,DIV_LE_X,DECIDE ``0 < 2n``] ++ 238 POP_ASSUM (STRIP_ASSUME_TAC o SPEC ``n:num``) ++ 239 FULL_SIMP_TAC arith_ss []); 240 241val modexpa_proof = store_thm("modexpa_proof",``!n a b. modexp n a b = modexpa b n a b``, 242 RW_TAC arith_ss [modexpa_lemma]); 243 244val witness_tail_def = miller_rabinTheory.witness_tail_def; 245(*** 246 Define 247 `(witness_tail 0 n a = ~(a = 1)) /\ 248 (witness_tail (SUC r) n a = 249 let a2 = (a * a) MOD n in 250 if a2 = 1 then ~(a = 1) /\ ~(a = n - 1) 251 else witness_tail r n a2)`; 252***) 253 254val witness_def = miller_rabinTheory.witness_def; 255(*** 256 Define 257 `witness n a = 258 let (r, s) = factor_twos (n - 1) in 259 witness_tail r n (modexp n a s)`; 260***) 261 262val exists_witness_def = 263 Define 264 `(exists_witness n [] = F) /\ 265 (exists_witness n (hd::tl) = witness n hd \/ exists_witness n tl)`; 266 267val exists_witness_proof = store_thm("exists_witness_proof", 268 ``!n l. EXISTS (witness n) l = exists_witness n l``, 269 GEN_TAC ++ Induct ++ 270 RW_TAC std_ss [EXISTS_DEF,exists_witness_def]); 271 272val miller_rabin_list_def = 273 Define 274 `miller_rabin_list n l = 275 if n = 2 then T 276 else if (n = 1) \/ EVEN n then F 277 else ~(EXISTS (witness n) l)`; 278 279(* ------------------------------------------------------------------------- *) 280(* Theorems. *) 281(* ------------------------------------------------------------------------- *) 282 283val many_longcircuit_def = Define 284 `(many_longcircuit f b 0 = UNIT b) /\ 285 (many_longcircuit f b (SUC n) = 286 BIND f (\b'. many_longcircuit f (b /\ b') n))`; 287 288val indep_fn_many_longcircuit = prove 289 (``!f b n. f IN indep_fn ==> many_longcircuit f b n IN indep_fn``, 290 Induct_on `n` 291 ++ RW_TAC std_ss 292 [many_longcircuit_def, probTheory.INDEP_FN_UNIT, 293 probTheory.INDEP_FN_BIND]); 294 295val many_longcircuit_f = prove 296 (``!f n. 297 f IN indep_fn ==> 298 (prob bern { s | FST (many_longcircuit f F n s)} = 0)``, 299 Induct_on `n` 300 ++ RW_TAC std_ss [many_longcircuit_def, state_transformerTheory.UNIT_DEF, 301 pred_setTheory.GSPEC_F, probTheory.PROB_BERN_EMPTY] 302 ++ MP_TAC 303 (Q.SPECL 304 [`f`, `\b'. many_longcircuit f F n`, 305 `prob bern (FST o (f : (num -> bool) -> bool # (num -> bool)))`] 306 probTheory.PROB_BERN_BIND_BOOL_BOOL) 307 ++ MATCH_MP_TAC (PROVE [] ``a /\ (b ==> c) ==> ((a ==> b) ==> c)``) 308 ++ CONJ_TAC >> RW_TAC std_ss [indep_fn_many_longcircuit] 309 ++ Q.PAT_ASSUM `!f. P f` (MP_TAC o Q.SPEC `f`) 310 ++ Know `!g : (num -> bool) -> bool # (num -> bool). 311 FST o g = { s | FST (g s) }` 312 >> (RW_TAC std_ss [pred_setTheory.EXTENSION] 313 ++ RW_TAC std_ss [pred_setTheory.GSPECIFICATION] 314 ++ RW_TAC std_ss [IN_DEF]) 315 ++ DISCH_THEN (fn th => RW_TAC std_ss [th]) 316 ++ RW_TAC std_ss [realTheory.REAL_MUL_RZERO, realTheory.REAL_ADD_RID]); 317 318val many_longcircuit_t = prove 319 (``!f n. 320 f IN indep_fn ==> 321 (prob bern {s | FST (many_longcircuit f T n s)} = 322 prob bern {s | FST (many f n s)})``, 323 Induct_on `n` 324 ++ RW_TAC std_ss [probTheory.MANY, many_longcircuit_def] 325 ++ MP_TAC 326 (Q.SPECL 327 [`f`, `\b'. many_longcircuit f b' n`, 328 `prob bern (FST o (f : (num -> bool) -> bool # (num -> bool)))`] 329 probTheory.PROB_BERN_BIND_BOOL_BOOL) 330 ++ MATCH_MP_TAC (PROVE [] ``a /\ (b ==> c) ==> ((a ==> b) ==> c)``) 331 ++ CONJ_TAC >> RW_TAC std_ss [indep_fn_many_longcircuit] 332 ++ MP_TAC 333 (Q.SPECL 334 [`f`, `\b'. if b' then many f n else UNIT F`, 335 `prob bern (FST o (f : (num -> bool) -> bool # (num -> bool)))`] 336 probTheory.PROB_BERN_BIND_BOOL_BOOL) 337 ++ MATCH_MP_TAC (PROVE [] ``a /\ (b ==> c) ==> ((a ==> b) ==> c)``) 338 ++ CONJ_TAC >> RW_TAC std_ss [probTheory.INDEP_FN_MANY, 339 probTheory.INDEP_FN_UNIT] 340 ++ Q.PAT_ASSUM `!f. P f` (MP_TAC o Q.SPEC `f`) 341 ++ Know `!g : (num -> bool) -> bool # (num -> bool). 342 FST o g = { s | FST (g s) }` 343 >> (RW_TAC std_ss [pred_setTheory.EXTENSION] 344 ++ RW_TAC std_ss [pred_setTheory.GSPECIFICATION] 345 ++ RW_TAC std_ss [IN_DEF]) 346 ++ DISCH_THEN (fn th => RW_TAC std_ss [th]) 347 ++ AP_TERM_TAC 348 ++ AP_TERM_TAC 349 ++ RW_TAC std_ss [many_longcircuit_f, state_transformerTheory.UNIT_DEF, 350 pred_setTheory.GSPEC_F, probTheory.PROB_BERN_EMPTY]); 351 352val miller_rabin_uniform_def = Define 353 `miller_rabin_uniform n = 354 if n <= 2 then UNIT 0 355 else 356 BIND (prob_uniform_cut (2 * log2 (n - 1)) (n - 2)) (\a. UNIT (a + 2n))`; 357 358val miller_rabin_uniform_list_def = Define 359 `(miller_rabin_uniform_list n 0 = UNIT []) /\ 360 (miller_rabin_uniform_list n (SUC m) = 361 BIND (miller_rabin_uniform n) 362 (\a. BIND (miller_rabin_uniform_list n m) (\l. UNIT (a :: l))))`; 363 364val miller_rabin_list_empty = prove 365 (``!n. 366 ~(n = 1) /\ ~EVEN n ==> 367 (miller_rabin_list n [] = T)``, 368 RW_TAC std_ss [miller_rabin_list_def, EXISTS_DEF]); 369 370val miller_rabin_list_single = prove 371 (``!n x. 372 ~(n = 1) /\ ~EVEN n ==> 373 (miller_rabin_list n [x] = ~witness n x)``, 374 RW_TAC std_ss [miller_rabin_list_def, EXISTS_DEF] 375 ++ Know `EVEN 2` >> RW_TAC std_ss [] 376 ++ METIS_TAC []); 377 378val miller_rabin_list_append = prove 379 (``!n l l'. 380 ~(n = 1) /\ ~EVEN n ==> 381 (miller_rabin_list n (APPEND l l') = 382 miller_rabin_list n l /\ miller_rabin_list n l')``, 383 RW_TAC std_ss [] 384 ++ Induct_on `l` 385 ++ RW_TAC std_ss [APPEND, miller_rabin_list_empty] 386 ++ POP_ASSUM MP_TAC 387 ++ RW_TAC std_ss [miller_rabin_list_def, EXISTS_DEF] 388 ++ Know `EVEN 2` >> RW_TAC std_ss [] 389 ++ METIS_TAC []); 390 391val indep_fn_miller_rabin_uniform = prove 392 (``!n. miller_rabin_uniform n IN indep_fn``, 393 RW_TAC std_ss [miller_rabin_uniform_def, probTheory.INDEP_FN_UNIT] 394 ++ Cases_on `n - 2` 395 >> (Suff `F` >> PROVE_TAC [] 396 ++ DECIDE_TAC) 397 ++ RW_TAC std_ss [probTheory.INDEP_FN_UNIT, 398 probTheory.INDEP_FN_BIND, 399 prob_uniformTheory.INDEP_FN_PROB_UNIFORM_CUT]); 400 401val indep_fn_miller_rabin_uniform_list = prove 402 (``!n m. miller_rabin_uniform_list n m IN indep_fn``, 403 Induct_on `m` 404 ++ RW_TAC std_ss [miller_rabin_uniform_list_def, 405 probTheory.INDEP_FN_BIND, 406 probTheory.INDEP_FN_UNIT, 407 indep_fn_miller_rabin_uniform]); 408 409val miller_rabin_list_many_longcircuit = prove 410 (``!n m. 411 ~(n = 1) /\ ~EVEN n ==> 412 (BIND (miller_rabin_uniform_list n m) 413 (\l. UNIT (miller_rabin_list n l)) = 414 many_longcircuit 415 (BIND (miller_rabin_uniform n) (\a. UNIT (~witness n a))) T m)``, 416 RW_TAC std_ss [] 417 ++ Suff 418 `!m q. 419 BIND (miller_rabin_uniform_list n m) 420 (\l. UNIT (miller_rabin_list n (APPEND q l))) = 421 many_longcircuit 422 (BIND (miller_rabin_uniform n) 423 (\a. UNIT (~witness n a))) (miller_rabin_list n q) m` 424 >> (DISCH_THEN (MP_TAC o Q.SPECL [`m`,`[]`]) 425 ++ RW_TAC std_ss [APPEND, miller_rabin_list_empty]) 426 ++ Induct 427 ++ RW_TAC std_ss [miller_rabin_uniform_list_def, many_longcircuit_def, 428 state_transformerTheory.BIND_LEFT_UNIT, APPEND_NIL] 429 ++ RW_TAC std_ss [GSYM state_transformerTheory.BIND_ASSOC] 430 ++ AP_TERM_TAC 431 ++ ONCE_REWRITE_TAC [FUN_EQ_THM] 432 ++ RW_TAC std_ss [] 433 ++ RW_TAC std_ss [state_transformerTheory.BIND_LEFT_UNIT] 434 ++ Know `!l. q ++ (x :: l) = (q ++ [x]) ++ l` 435 >> (GEN_TAC 436 ++ Induct_on `q` 437 ++ RW_TAC std_ss [APPEND]) 438 ++ DISCH_THEN (fn th => ONCE_REWRITE_TAC [th]) 439 ++ POP_ASSUM (fn th => ONCE_REWRITE_TAC [Q.SPEC `q ++ [x]` th]) 440 ++ RW_TAC std_ss [miller_rabin_list_append, miller_rabin_list_single]); 441 442val miller_rabin_equivalence = prove 443 (``!n m. 444 ~(n = 1) /\ ~EVEN n ==> 445 (many (BIND (miller_rabin_uniform n) (\a. UNIT (~witness n a))) m = 446 miller_rabin$miller_rabin n m)``, 447 RW_TAC std_ss [miller_rabinTheory.miller_rabin_def] 448 ++ Induct_on `m` 449 ++ RW_TAC std_ss [probTheory.MANY] 450 ++ POP_ASSUM (K ALL_TAC) 451 ++ AP_THM_TAC 452 ++ ONCE_REWRITE_TAC [FUN_EQ_THM] 453 ++ ONCE_REWRITE_TAC [FUN_EQ_THM] 454 ++ Cases_on `n = 2` 455 >> (RW_TAC std_ss [] 456 ++ POP_ASSUM MP_TAC 457 ++ RW_TAC std_ss []) 458 ++ Cases_on `n <= 2` 459 >> (Suff `F` >> DECIDE_TAC 460 ++ Suff `~(n = 0)` >> DECIDE_TAC 461 ++ STRIP_TAC 462 ++ Q.PAT_ASSUM `~EVEN n` MP_TAC 463 ++ RW_TAC std_ss []) 464 ++ RW_TAC std_ss [state_transformerTheory.BIND_DEF, 465 state_transformerTheory.UNIT_DEF, 466 miller_rabinTheory.miller_rabin_1_def, 467 miller_rabin_uniform_def] 468 ++ RW_TAC std_ss [UNCURRY, FST, SND]); 469 470val MILLER_RABIN_COMPOSITE_ERROR = store_thm 471 ("MILLER_RABIN_COMPOSITE_ERROR", 472 ``!n m. 473 ~prime n ==> 474 prob bern {s | FST (BIND (miller_rabin_uniform_list n m) 475 (\l. UNIT (miller_rabin_list n l)) s)} <= 476 (1 / 2) pow m``, 477 RW_TAC std_ss [] 478 ++ Cases_on `n = 1` 479 >> (RW_TAC std_ss [miller_rabin_list_def, 480 state_transformerTheory.BIND_DEF, 481 state_transformerTheory.UNIT_DEF, UNCURRY, 482 pred_setTheory.GSPEC_F, probTheory.PROB_BERN_EMPTY] 483 ++ MATCH_MP_TAC realTheory.POW_POS 484 ++ RW_TAC std_ss [realTheory.REAL_HALF_BETWEEN]) 485 ++ Cases_on `EVEN n` 486 >> (Know `~(n = 2)` >> METIS_TAC [extra_arithTheory.PRIME_2] 487 ++ RW_TAC std_ss [miller_rabin_list_def, 488 state_transformerTheory.BIND_DEF, 489 state_transformerTheory.UNIT_DEF, UNCURRY, 490 pred_setTheory.GSPEC_F, probTheory.PROB_BERN_EMPTY] 491 ++ MATCH_MP_TAC realTheory.POW_POS 492 ++ RW_TAC std_ss [realTheory.REAL_HALF_BETWEEN]) 493 ++ RW_TAC std_ss [miller_rabin_list_many_longcircuit] 494 ++ RW_TAC std_ss [many_longcircuit_t, probTheory.INDEP_FN_BIND, 495 probTheory.INDEP_FN_UNIT, indep_fn_miller_rabin_uniform] 496 ++ RW_TAC std_ss [miller_rabin_equivalence] 497 ++ METIS_TAC [MILLER_RABIN_COMPOSITE_UPPER]); 498 499(* The top-level specification when the input number n is prime: *) 500(* whatever the input list l of bases, miller_rabin_list n l will always *) 501(* return true. *) 502 503val MILLER_RABIN_PRIME = store_thm 504 ("MILLER_RABIN_PRIME", 505 ``!n l. 506 prime n /\ EVERY (\a. 0 < a /\ a < n) l ==> 507 (miller_rabin_list n l = T)``, 508 RW_TAC bool_ss [miller_rabin_list_def] 509 ++ Cases_on `EVEN n` >> METIS_TAC [extra_arithTheory.NOT_PRIME_EVEN] 510 ++ Cases_on `n = 1` >> METIS_TAC [dividesTheory.NOT_PRIME_1] 511 ++ RW_TAC bool_ss [] 512 ++ DISJ2_TAC 513 ++ Induct_on `l` 514 ++ RW_TAC bool_ss [EXISTS_DEF,EVERY_DEF] 515 ++ METIS_TAC [WITNESS_CORRECT]); 516 517(* The top-level specification when the input number n is composite: *) 518(* If the input list l consists of m bases chosen uniformly at random, the *) 519(* probability that miller_rabin_list n l returns false is at least *) 520(* 1 - (1/2)^m. *) 521 522val MILLER_RABIN_COMPOSITE = store_thm 523 ("MILLER_RABIN_COMPOSITE", 524 ``!n m. 525 ~prime n ==> 526 1 - (1 / 2) pow m <= 527 prob bern {s | FST (BIND (miller_rabin_uniform_list n m) 528 (\l. UNIT (miller_rabin_list n l)) s) = F}``, 529 RW_TAC std_ss [] 530 ++ Know 531 `{s | ~FST (BIND (miller_rabin_uniform_list n m) 532 (\l. UNIT (miller_rabin_list n l)) s)} = 533 COMPL (I o FST o BIND (miller_rabin_uniform_list n m) 534 (\l. UNIT (miller_rabin_list n l)))` 535 >> (ONCE_REWRITE_TAC [pred_setTheory.EXTENSION] 536 ++ RW_TAC std_ss [pred_setTheory.GSPECIFICATION, 537 pred_setTheory.IN_COMPL] 538 ++ RW_TAC std_ss [pred_setTheory.SPECIFICATION, o_THM, I_THM]) 539 ++ DISCH_THEN (fn th => REWRITE_TAC [th]) 540 ++ RW_TAC std_ss [probabilityTheory.PROB_COMPL, 541 probTheory.PROB_SPACE_BERN, 542 probTheory.INDEP_FN_FST_EVENTS, 543 probTheory.INDEP_FN_BIND, 544 probTheory.INDEP_FN_UNIT, 545 indep_fn_miller_rabin_uniform_list] 546 ++ Know `!a b c : real. c <= b ==> a - b <= a - c` 547 >> RealArith.REAL_ARITH_TAC 548 ++ DISCH_THEN MATCH_MP_TAC 549 ++ MATCH_MP_TAC realTheory.REAL_LE_TRANS 550 ++ Q.EXISTS_TAC 551 `prob bern {s | FST (BIND (miller_rabin_uniform_list n m) 552 (\l. UNIT (miller_rabin_list n l)) s)}` 553 ++ REVERSE CONJ_TAC >> METIS_TAC [MILLER_RABIN_COMPOSITE_ERROR] 554 ++ Know `!a b : real. (a = b) ==> a <= b` 555 >> RealArith.REAL_ARITH_TAC 556 ++ DISCH_THEN MATCH_MP_TAC 557 ++ AP_TERM_TAC 558 ++ ONCE_REWRITE_TAC [pred_setTheory.EXTENSION] 559 ++ RW_TAC std_ss [pred_setTheory.GSPECIFICATION] 560 ++ RW_TAC std_ss [pred_setTheory.SPECIFICATION]); 561 562(*** 563(* ------------------------------------------------------------------------- *) 564(* Versions of the definitions suitable for exporting to ML *) 565(* ------------------------------------------------------------------------- *) 566 567val UNCURRY_ML = save_thm ("UNCURRY_ML", pairTheory.UNCURRY_DEF); 568 569val EVEN_ML = store_thm 570 ("EVEN_ML", 571 ``!n. EVEN n = (n MOD 2 = 0)``, 572 STRIP_TAC 573 ++ RW_TAC std_ss [MOD_TWO] 574 ++ DECIDE_TAC); 575 576val ODD_ML = store_thm 577 ("ODD_ML", 578 ``ODD = $~ o EVEN``, 579 RW_TAC std_ss [o_DEF, EVEN_ODD, FUN_EQ_THM]); 580 581val UNIT_ML = store_thm 582 ("UNIT_ML", 583 ``!x. UNIT x = \s. (x, s)``, 584 RW_TAC std_ss [UNIT_DEF]); 585 586val BIND_ML = store_thm 587 ("BIND_ML", 588 ``!f g. BIND f g = UNCURRY g o f``, 589 RW_TAC std_ss [BIND_DEF]); 590 591val MANY_ML = store_thm 592 ("MANY_ML", 593 ``!f n. 594 many f n = 595 if n = 0 then UNIT T 596 else BIND f (\x. if x then many f (n - 1) else UNIT F)``, 597 STRIP_TAC 598 ++ Cases 599 ++ RW_TAC std_ss [MANY, SUC_SUB1]); 600 601val LOG2_ML = store_thm 602 ("LOG2_ML", 603 ``!n. log2 n = if n = 0 then 0 else SUC (log2 (n DIV 2))``, 604 Cases 605 ++ RW_TAC std_ss [log2_def, SUC_SUB1]); 606 607val PROB_UNIF_ML = store_thm 608 ("PROB_UNIF_ML", 609 ``!n s. 610 prob_unif n s = 611 if n = 0 then (0, s) 612 else 613 let (m, s') = prob_unif (n DIV 2) s 614 in (if shd s' then 2 * m + 1 else 2 * m, stl s')``, 615 Cases 616 ++ RW_TAC std_ss [prob_unif_def, SUC_SUB1]); 617 618val PROB_UNIFORM_CUT_ML = store_thm 619 ("PROB_UNIFORM_CUT_ML", 620 ``!t n. 621 prob_uniform_cut t n = 622 if n = 0 then prob_uniform_cut t n 623 else if t = 0 then UNIT 0 624 else 625 BIND (prob_unif (n - 1)) 626 (\m. if m < n then UNIT m else prob_uniform_cut (t - 1) n)``, 627 Cases 628 ++ Cases 629 ++ RW_TAC std_ss [PROB_UNIFORM_CUT_MONAD, SUC_SUB1]); 630 631val FACTOR_TWOS_ML = save_thm ("FACTOR_TWOS_ML", factor_twos_def); 632 633val MODEXP_ML = save_thm ("MODEXP_ML", modexp_def); 634 635val WITNESS_TAIL_ML = store_thm 636 ("WITNESS_TAIL_ML", 637 ``!n a r. 638 witness_tail r n a = 639 if r = 0 then ~(a = 1) 640 else 641 let a2 = (a * a) MOD n 642 in if a2 = 1 then ~(a = 1) /\ ~(a = n - 1) 643 else witness_tail (r - 1) n a2``, 644 Cases_on `r` 645 ++ RW_TAC std_ss [witness_tail_def, SUC_SUB1]); 646 647val WITNESS_ML = save_thm ("WITNESS_ML", witness_def); 648 649val MILLER_RABIN_LIST_ML = 650 save_thm ("MILLER_RABIN_LIST_ML", miller_rabin_list_def); 651***) 652 653(* ------------------------------------------------------------------------- *) 654(* Converting the definitions to HOL/SEXP ... with tracing *) 655(* ------------------------------------------------------------------------- *) 656 657set_trace "EncodeLib.FunctionEncoding" 1; 658 659val (list_natp_rewrite,list_natp_def) = get_recogniser ``:num list``; 660 661(* ACL2 doesn't have this lemma, so include it for sake of termination *) 662val div_terminate = prove(``!a. 0 < a ==> a DIV 2 < a``,RW_TAC arith_ss [DIV_LT_X]); 663 664val (_,acl2_factor_twos_def) = 665 convert_definition_full 666 (SOME ``\a. 0 < a ==> a DIV 2 < a``) 667 [div_terminate,DECIDE ``~(2 = 0n)``] 668 factor_twos_def 669 670val (_,acl2_modexp_def) = 671 convert_definition_full 672 (SOME ``\a b c. ~(a = 0n) /\ (0 < c ==> c DIV 2 < c)``) 673 [div_terminate,DECIDE ``~(2 = 0n)``] 674 modexp_def; 675 676val (_,acl2_witness_tail_def) = 677 convert_definition_full 678 (SOME ``\a b c. ~(b = 0n)``) 679 [] 680 witness_tail_def; 681 682val (_,acl2_witness_def) = 683 convert_definition_full 684 (SOME ``\a b.~(a = 0n)``) 685 [] 686 witness_def; 687 688val (_,acl2_exists_ho_def) = 689 convert_definition 690 (INST_TYPE [``:'a`` |-> ``:num``] EXISTS_DEF); 691 692val (miller_rabin_list_correct,acl2_miller_rabin_list_def) = 693 convert_definition_full 694 (SOME ``\a b. ~(a = 0n)``) 695 [] 696 miller_rabin_list_def; 697 698val (witness_rewrite,acl2_exists_witness_def) = 699 flatten_HO_definition "acl2_exists_witness" acl2_exists_ho_def 700 ``acl2_EXISTS (\x. ite (natp x) (acl2_witness n x) (acl2_witness n (nat 0))) l``; 701 702(* ------------------------------------------------------------------------- *) 703(* Print out the definitions (removing 'andl') *) 704(* ------------------------------------------------------------------------- *) 705 706open TextIO sexp; 707 708val outs = openOut(FileSys.fullPath "../lisp/miller-rabin.lisp"); 709 710fun output_thm thm = 711let val string = ref "" 712 val _ = (print_mlsexp (fn s => string := (!string) ^ s) o 713 def_to_mlsexp_defun o REWRITE_RULE [sexpTheory.andl_def]) thm 714 val _ = string := (!string) ^ "\n\n" 715in 716 (print (!string) ; output(outs,!string)) 717end; 718 719val _ = output(outs,"(in-package \"ACL2\")\n\n"); 720 721val _ = output_thm acl2_factor_twos_def; 722val _ = output_thm acl2_modexp_def; 723val _ = output_thm acl2_witness_tail_def; 724val _ = output_thm acl2_witness_def; 725val _ = output_thm list_natp_def; 726val _ = output_thm (REWRITE_RULE [list_natp_rewrite] acl2_exists_witness_def); 727val _ = output_thm (REWRITE_RULE [list_natp_rewrite,witness_rewrite] acl2_miller_rabin_list_def); 728 729val _ = closeOut outs; 730 731(* ------------------------------------------------------------------------- *) 732(* Equivalence between miller_rabin_list and the acl2 version *) 733(* ------------------------------------------------------------------------- *) 734 735val _ = (print_thm miller_rabin_list_correct ; print "\n"); 736 737val miller_rabin_list_correct2 = 738 DISCH_ALL (REWRITE_RULE [SEXP_TO_BOOL_OF_BOOL] 739 (AP_TERM ``sexp_to_bool`` (UNDISCH (SPEC_ALL miller_rabin_list_correct)))); 740 741val miller_rabin_list_correct2 = 742 prove(``~(n = 0) ==> 743 (miller_rabin_list n = 744 sexp_to_bool o acl2_miller_rabin_list (nat n) o list nat)``, 745 RW_TAC arith_ss [FUN_EQ_THM] THEN MATCH_MP_TAC miller_rabin_list_correct2 746 THEN FIRST_ASSUM ACCEPT_TAC); 747