1fun load_path_add x = loadPath := !loadPath @ [concat Globals.HOLDIR x];
2load_path_add "/examples/mc-logic";
3load_path_add "/examples/ARM/v4";
4load_path_add "/tools/mlyacc/mlyacclib";
5
6use "prelim";
7hide "C";
8
9app load ["pred_setTheory", "rich_listTheory", "wordsLib", "arm_progLib",
10          "multiwordTheory"];
11
12quietdec := true;
13open HolKernel boolLib bossLib Parse;
14open pred_setTheory res_quanTheory arithmeticTheory 
15     wordsLib wordsTheory bitTheory;
16open pairTheory listTheory rich_listTheory relationTheory pairTheory;
17open set_sepTheory set_sepLib progTheory arm_progTheory 
18     arm_instTheory arm_progLib;
19open multiwordTheory;
20
21quietdec := false;
22
23infix \\ << >>
24
25val op \\ = op THEN;
26val op << = op THENL;
27val op >> = op THEN1;
28
29val RW = REWRITE_RULE;
30val RW1 = ONCE_REWRITE_RULE;
31
32fun MATCH_MP th1 th2 = 
33 let fun SIMPLE_MATCH_MP impth =
34      let val (hy,c) = dest_thm impth
35          val (vs,imp) = strip_forall c
36          val pat = fst(dest_imp imp) handle HOL_ERR _ 
37                    => raise ERR "SIMPLE_MATCH_MP" "not an implication"
38          val fvs = set_diff (free_vars pat) (free_varsl hy)
39          val gth = GSPEC (GENL fvs (SPECL vs impth))
40          val matchfn = match_term (fst(dest_imp(concl gth)))
41      in
42      fn th => MP (INST_TY_TERM (matchfn (concl th)) gth) th
43               handle e => raise wrap_exn "SIMPLE_MATCH_MP" "does not match" e
44      end
45 in
46  Drule.MATCH_MP th1 th2 handle HOL_ERR _ 
47  => (HOL_MESG "Drule.MATCH_MP fails, trying simpler version";
48      SIMPLE_MATCH_MP th1 th2)
49 end;
50
51
52(* lemmas *)
53
54val n2w_x_eq_0w = prove(
55  ``1073741824w = 0w:word30``,
56  ONCE_REWRITE_TAC [GSYM n2w_mod] \\ SIMP_TAC (std_ss++SIZES_ss) []);
57
58val ARM_PROG_COMPOSE_WEAKEN = prove(
59  ``ARM_PROG P code C Q {} ==> 
60    ARM_PROG P1 code C Q1 ((P * Q2,I) INSERT Z) ==>
61    SEP_IMP (Q * Q2) Q1 ==>
62    ARM_PROG P1 code C Q1 Z``,
63  REWRITE_TAC [ARM_PROG_THM] \\ REPEAT STRIP_TAC 
64  \\ Q.PAT_ASSUM `ARM_GPROG {(P,I)} ((code,I) INSERT C) {(Q,pcINC code)}` 
65    (ASSUME_TAC o RW [setSTAR_CLAUSES] o Q.SPEC `Q2` o MATCH_MP ARM_GPROG_FRAME)
66  \\ IMP_RES_TAC ARM_GPROG_WEAKEN_POST
67  \\ (MATCH_MP_TAC o RW [INSERT_UNION_EQ,UNION_EMPTY,UNION_IDEMPOT,INSERT_INSERT] o 
68      RW1 [UNION_COMM] o Q.SPECL [`Y`,`{}`,`{(P * Q2,I)}`,`C`,`C`,
69      `(Q1,pcINC code) INSERT Z`,`{(Q1,pcINC code)}`]) ARM_GPROG_COMPOSE
70  \\ ONCE_REWRITE_TAC [INSERT_COMM] \\ ASM_REWRITE_TAC []);
71
72(* helpers *)
73
74fun extract_spec th substs uni_list abs_list = let
75  val p = parse_in_context (free_varsl (concl th :: hyp th))
76  val ss = map (fn (x,y) => (p x |-> p y)) substs
77  val tm = (fst o dest_comb o concl) th
78  val tm = mk_comb(tm,(snd o dest_comb o snd o dest_comb o concl) th)
79  val tm = subst ss tm
80  val tm = foldr mk_forall tm (map p uni_list)
81  val tm = foldr mk_abs tm (map p abs_list)
82  in tm end;
83
84fun extract_assum th = let
85  val tm = (repeat (snd o dest_forall) o fst o dest_imp o concl) th
86  val th = (SPEC_ALL o ASSUME o fst o dest_imp) tm
87  in th end;
88
89fun tidy_up th1 th = let
90  val tm = (fst o dest_imp o concl) th1
91  val (tm,vs1) = repeat 
92                  (fn (tm,xs) => 
93                      let val (v,x) = dest_forall tm 
94                      in (x,xs@[v]) end) 
95                  (tm,[])
96  val tm = (snd o dest_imp) tm
97  val (tm,vs2) = repeat 
98                  (fn (tm,xs) => 
99                      let val (v,x) = dest_forall tm 
100                      in (x,xs@[v]) end) 
101                  (tm,[])
102  in (GENL vs1 o DISCH_ALL o GENL vs2) th end;
103
104
105(* definition *)
106
107val f32_def = Define 
108   `f32(x:word32,a:word32) =
109          if x=0w then a else f32(x-1w,a*x)`;
110
111val f32_ind = fetch "-" "f32_ind";
112
113
114val def = compile3 [f32_def];
115
116val f32_compiled_def = 
117 Define 
118   `f32_compiled (v1:word32,v2:word32) =
119      let v3 = (if v1 = 0w then v2
120                else let v4 = v1 - 1w in
121                     let v5 = v2 * v1 in
122                     let v6 = f32 (v4,v5) 
123                     in v6)
124      in
125        v3`;
126
127(* proof step 1: make a basic spec for a run through the code *)
128(*
129  make_spec' [
130("teq r0,#0",true),
131("beq 16",true)]
132*)
133
134  val th = (*  teq r0,#0  *) FST_PROG2 (SIMP_RULE (bool_ss++armINST_ss) [EVAL ``(w2w (0w :word8) :word32)``] (Q.INST [`c_flag`|->`AL`,`a`|->`0w`,`a_mode`|->`Imm 0w`,`x`|->`x1` ] arm_TEQ1))
135  val th = (*  beq 16     *) MOVE_COMPOSE th (FST_PROG2 (SIMP_RULE (bool_ss++armINST_ss) [EVAL ``(sw2sw (2w :word24) :word30)``] (Q.INST [`c_flag`|->`EQ`,`offset`|->`2w` ] arm_B2))) `x1*x2` `(x2)*(x1)` `x1*x2` `(x1)*(x2)`
136  val th = AUTO_HIDE_STATUS th
137  val th = SIMP_RULE (arith_ss++sep_ss++pcINC_ss) [wLENGTH_def,LENGTH,word_add_n2w] th
138  val th = APP_FRAME `cond (x1 = 0w:word32)` th
139  val th1 = th
140
141(*
142  make_spec' [
143("teq r0,#0",true),
144("beq 16",false),
145("mul r1,r0,r1",true),
146("sub r0,r0,#1",true),
147("b -16",true)]
148*)
149  val th = (*  teq r0,#0     *) FST_PROG2 (SIMP_RULE (bool_ss++armINST_ss) [EVAL ``(w2w (0w :word8) :word32)``] (Q.INST [`c_flag`|->`AL`,`a`|->`0w`,`a_mode`|->`Imm 0w`,`x`|->`x1` ] arm_TEQ1))
150  val th = (*  beq 16        *) MOVE_COMPOSE th (SND_PROG2 (SIMP_RULE (bool_ss++armINST_ss) [EVAL ``(sw2sw (2w :word24) :word30)``] (Q.INST [`c_flag`|->`EQ`,`offset`|->`2w` ] arm_B2))) `x1*x2` `(x2)*(x1)` `x1*x2` `(x1)*(x2)`
151  val th = (*  mul r1,r0,r1  *) MOVE_COMPOSE th (FST_PROG2 (SIMP_RULE (bool_ss++armINST_ss) [] (Q.INST [`c_flag`|->`AL`,`s_flag`|->`F`,`b`|->`1w`,`a`|->`0w`,`x`|->`x3`,`y`|->`y3` ] arm_MUL2))) `x1*x2` `(x1*x2)*(emp)` `x1*x2*x3` `(x3*x1)*(x2)`
152  val th = (*  sub r0,r0,#1  *) MOVE_COMPOSE th (FST_PROG2 (SIMP_RULE (bool_ss++armINST_ss) [EVAL ``(w2w (1w :word8) :word32)``] (Q.INST [`c_flag`|->`AL`,`s_flag`|->`F`,`a`|->`0w`,`a_mode`|->`Imm 1w`,`x`|->`x4` ] arm_SUB1))) `x1*x2*x3` `(x1*x3)*(x2)` `x1*x2` `(x1*x2)*(emp)`
153  val th = (*  b -16         *) MOVE_COMPOSE th (FST_PROG2 (SIMP_RULE (bool_ss++armINST_ss) [EVAL ``(sw2sw (16777210w :word24) :word30)``] (Q.INST [`c_flag`|->`AL`,`offset`|->`16777210w` ] arm_B2))) `x1*x2*x3` `(x2)*(x1*x3)` `x1` `(x1)*(emp)`
154  val th = AUTO_HIDE_STATUS th
155  val th = APP_FRAME `cond ~(x1 = 0w:word32)` th
156  val th = SIMP_RULE (arith_ss++sep_ss++pcINC_ss) [wLENGTH_def,LENGTH,word_add_n2w] th
157  val th1 = APP_FRAME `R 1w y3` th1 
158  val th1 = MOVE_PRE `S` th1
159  val th = SIMP_RULE (bool_ss++sep2_ss) [] th
160  val th1 = SIMP_RULE (bool_ss++sep2_ss) [] th1
161  val th = SIMP_RULE (bool_ss++sep_ss) [] (APP_MERGE th th1)
162  val th = RW [n2w_x_eq_0w,pcADD_0,INSERT_UNION_EQ,UNION_EMPTY] th
163  val th = RW1 [INSERT_COMM] th
164  val th = ABSORB_POST th
165
166  (* step 2: clean up pre- and postconditions *)
167  val th = AUTO_HIDE_POST1 [`R 0w`] th
168  val th = APP_WEAKEN1 th 
169    `~R 0w * R 1w (f32(x1,y3)) * ~S`
170   (SIMP_TAC (bool_ss++sep2_ss) [SEP_IMP_MOVE_COND]
171    \\ ONCE_REWRITE_TAC [f32_def] \\ REWRITE_TAC []
172    \\ SIMP_TAC (bool_ss++star_ss) [SEP_IMP_REFL])
173
174  (* step 3: instantiate induction and extract ind hyp *)
175  val tm = extract_spec th [] [] [`x1`,`y3`]
176  val ind = Q.GEN `P` (SIMP_RULE bool_ss [FST,SND] (Q.SPEC `\x. P (FST x) (SND x)` f32_ind))
177  val th1 = SIMP_RULE std_ss [] (ISPEC tm ind)
178  val asm = extract_assum th1
179  val asm = RW [GSYM ARM_PROG_MOVE_COND] asm
180
181  (* step 4: match step and prove postcondition *)
182  val asm = MATCH_MP ARM_PROG_COMPOSE_WEAKEN asm
183  val th = RW1 [GSYM (REWRITE_CONV [SEP_cond_CLAUSES] ``cond b * cond b``)] th
184  val th = RW [STAR_ASSOC] th
185(*  val th = Q.INST [`x1`|->`x`,`y3`|->`a`] th *)
186  val th = RW1 [WORD_MULT_COMM] th
187  val th = MATCH_MP asm th  (* MATCH_MP now works w.o. above Q.INST *)
188  val lemma = prove((fst o dest_imp o concl) th,
189    SIMP_TAC (bool_ss++sep2_ss) [SEP_IMP_MOVE_COND] \\ REPEAT STRIP_TAC
190    \\ CONV_TAC (RAND_CONV (ONCE_REWRITE_CONV [f32_def]))
191    \\ ASM_REWRITE_TAC [SEP_IMP_REFL])
192  val th = MP th lemma
193  
194  (* step 5: clean up *)
195(*   val th = MATCH_MP th1 (tidy_up th1 th) *)
196  val th2 = Q.GEN `x1` (Q.GEN `y3` (DISCH_ALL th));;
197  val th = MATCH_MP th1 th2
198  val th = SPEC_ALL (Q.SPECL [`x`,`a`] th)
199
200
201