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