1(* interactive use:
2
3quietdec := true;
4loadPath := (concat Globals.HOLDIR "/examples/dev/sw") :: !loadPath;
5
6app load ["numLib", "relationTheory", "arithmeticTheory", "preARMTheory", "pairTheory",
7     "pred_setSimps", "pred_setTheory", "listTheory", "rich_listTheory", "whileTheory", "ARMCompositionTheory",
8      "CFLTheory"];
9
10quietdec := false;
11*)
12
13
14open HolKernel Parse boolLib bossLib numLib relationTheory arithmeticTheory preARMTheory pairTheory
15     pred_setSimps pred_setTheory listTheory rich_listTheory whileTheory ARMCompositionTheory CFLTheory;
16
17
18val _ = new_theory "CFL_Rules";
19
20(*---------------------------------------------------------------------------------*)
21(*      Simplifier on finite maps                                                  *)
22(*---------------------------------------------------------------------------------*)
23
24val set_ss = std_ss ++ SET_SPEC_ss ++ PRED_SET_ss;
25
26(*---------------------------------------------------------------------------------*)
27(*      Inference based on Hoare Logic                                             *)
28(*---------------------------------------------------------------------------------*)
29
30val _ = Globals.priming := NONE;
31
32(*---------------------------------------------------------------------------------*)
33(*      read from an data state                                                    *)
34(*---------------------------------------------------------------------------------*)
35
36val _ = Hol_datatype `
37    REXP = RR of MREG
38         | RM of MMEM
39         | RC of DATA
40         | PR of REXP # REXP
41    `;
42
43val mread_def = Define `
44     (mread st (RR r) = read st (toREG r)) /\
45     (mread st (RM m) = read st (toMEM m)) /\
46     (mread st (RC c) = c)`;
47
48val _ = add_rule {term_name = "mread", fixity = Suffix 60,
49                  pp_elements = [TOK "<", TM, TOK ">"],
50                  paren_style = OnlyIfNecessary,
51                  block_style = (AroundSameName, (PP.INCONSISTENT, 0))} handle HOL_ERR e => print (#message e);
52
53
54(*---------------------------------------------------------------------------------*)
55(*      The fp and sp point to the default positions                               *)
56(*---------------------------------------------------------------------------------*)
57
58val proper_def = Define `
59    proper = (\(regs,mem):DSTATE. (regs ' 11 = 100w) /\ (regs ' 13 = 100w))`;
60
61
62(*---------------------------------------------------------------------------------*)
63(*      Hoare Logic Style Specification                                            *)
64(*---------------------------------------------------------------------------------*)
65
66val HSPEC_def = Define `
67    HSPEC P S_cfl Q = !st. P st ==> Q (run_cfl S_cfl st)`;
68
69val _ = type_abbrev("HSPEC_TYPE", type_of (Term `HSPEC`));
70
71(*
72val _ = add_rule {term_name = "HSPEC",
73                  fixity = Infix (HOLgrammars.RIGHT, 3),
74                  pp_elements = [HardSpace 1, TOK "(", TM, TOK ")", HardSpace 1],
75                  paren_style = OnlyIfNecessary,
76                  block_style = (AroundEachPhrase,
77                                 (PP.INCONSISTENT, 0))};
78*)
79
80(*---------------------------------------------------------------------------------*)
81(*      Sequential Composition                                                     *)
82(*---------------------------------------------------------------------------------*)
83
84val CFL_SC_RULE = Q.store_thm (
85   "CFL_SC_RULE",
86   `!P Q R S1 S2. WELL_FORMED S1 /\ WELL_FORMED S2 /\
87      HSPEC P S1 Q /\ HSPEC Q S2 R ==>
88      HSPEC P (SC S1 S2) R`,
89    RW_TAC std_ss [HSPEC_def] THEN
90    METIS_TAC [CFL_SEMANTICS_SC]
91   );
92
93(*---------------------------------------------------------------------------------*)
94(*      Block Rule                                                                 *)
95(*      Block of assigment                                                         *)
96(*---------------------------------------------------------------------------------*)
97
98val BLK_EQ_SC = Q.store_thm (
99   "BLK_EQ_SC",
100   `!stm stmL st. (run_cfl (BLK (stm::stmL)) st = run_cfl (SC (BLK [stm]) (BLK stmL)) st) /\
101                  (run_cfl (BLK (SNOC stm stmL)) st = run_cfl (SC (BLK stmL) (BLK [stm])) st)`,
102
103   REPEAT GEN_TAC THEN
104   `WELL_FORMED (BLK [stm]) /\ WELL_FORMED (BLK stmL)` by
105               METIS_TAC [BLOCK_IS_WELL_FORMED] THEN
106   STRIP_TAC THENL [
107       `run_cfl (BLK [stm]) st = mdecode st stm` by (
108               RW_TAC list_ss [run_cfl_def, run_arm_def, translate_def, Once RUNTO_ADVANCE] THEN
109               RW_TAC list_ss [GSYM uploadCode_def, UPLOADCODE_LEM] THEN
110               RW_TAC list_ss [GSYM TRANSLATE_ASSIGMENT_CORRECT, ARMCompositionTheory.get_st_def, Once RUNTO_ADVANCE]
111           ) THEN
112           RW_TAC list_ss [CFL_SEMANTICS_BLK, CFL_SEMANTICS_SC],
113
114       RW_TAC list_ss [SNOC_APPEND, run_cfl_def, translate_def] THEN
115           `mk_SC (translate (BLK stmL)) [translate_assignment stm] = translate (BLK (stmL ++ [stm]))` by (
116               RW_TAC list_ss [ARMCompositionTheory.mk_SC_def] THEN
117               Induct_on `stmL` THENL [
118                   RW_TAC list_ss [translate_def],
119                   RW_TAC list_ss [translate_def] THEN
120                       METIS_TAC [BLOCK_IS_WELL_FORMED]
121               ]) THEN
122            METIS_TAC []
123       ]
124   );
125
126val EMPTY_BLK_AXIOM = Q.store_thm (
127   "EMPTY_BLK_AXIOM",
128   `!P Q. (!st. P st ==> Q st) ==>
129        HSPEC P (BLK []) Q`,
130    RW_TAC std_ss [HSPEC_def, CFL_SEMANTICS_BLK]
131  );
132
133val CFL_BLK_RULE = Q.store_thm (
134   "BLK_RULE",
135   `!P Q R stm stmL. HSPEC Q (BLK [stm]) R /\
136              HSPEC P (BLK stmL) Q ==>
137                HSPEC P (BLK (SNOC stm stmL)) R`,
138    RW_TAC std_ss [HSPEC_def] THEN
139    RW_TAC std_ss [BLK_EQ_SC] THEN
140    METIS_TAC [HSPEC_def, CFL_SC_RULE, BLOCK_IS_WELL_FORMED]
141  );
142
143
144(*---------------------------------------------------------------------------------*)
145(*      Conditional Jumps                                                          *)
146(*---------------------------------------------------------------------------------*)
147
148val CFL_CJ_RULE = Q.store_thm (
149   "CFL_CJ_RULE",
150   `!P Q cond S1 S2 st. WELL_FORMED S1 /\ WELL_FORMED S2 /\
151      HSPEC (\st.eval_il_cond cond st /\ P st) S1 Q /\ HSPEC (\st.~eval_il_cond cond st /\ P st) S2 Q ==>
152      HSPEC P (CJ cond S1 S2) Q`,
153    RW_TAC std_ss [HSPEC_def] THEN
154    METIS_TAC [CFL_SEMANTICS_CJ]
155   );
156
157
158val CFL_CJ_RULE_2 = Q.store_thm (
159   "CFL_CJ_RULE_2",
160   `!P Q cond S1 S2 st. WELL_FORMED S1 /\ WELL_FORMED S2 /\
161      HSPEC P S1 Q /\ HSPEC P S2 Q ==>
162      HSPEC P (CJ cond S1 S2) Q`,
163    RW_TAC std_ss [HSPEC_def] THEN
164    METIS_TAC [CFL_SEMANTICS_CJ]
165   );
166
167(*---------------------------------------------------------------------------------*)
168(*      Tail Recursion                                                             *)
169(*---------------------------------------------------------------------------------*)
170
171val CFL_TR_RULE = Q.store_thm (
172   "CFL_TR_RULE",
173   `!cond S_body P Q.
174        WELL_FORMED S_body /\  WF_TR (translate_condition cond, translate S_body) /\
175           HSPEC P S_body P ==> HSPEC P (TR cond S_body) P`,
176   RW_TAC std_ss [HSPEC_def] THEN
177   METIS_TAC [HOARE_TR_CFL]
178   );
179
180(*---------------------------------------------------------------------------------*)
181(*      Well-founded Tail Recursion                                                *)
182(*---------------------------------------------------------------------------------*)
183
184val WF_DEF_2 = Q.store_thm (
185   "WF_DEF_2",
186   `WF R = !P. (?w. P w) ==> ?min. P min /\ !b. R b min ==> ~P b`,
187   RW_TAC std_ss [relationTheory.WF_DEF]
188  );
189
190val WF_TR_LEM_1 = Q.store_thm (
191   "WF_TR_LEM_1",
192   `!cond ir. WELL_FORMED ir /\
193           WF (\st1 st0. ~eval_il_cond cond st0 /\ (st1 = run_cfl ir st0)) ==>
194           WF_TR (translate_condition cond,translate ir)`,
195
196   RW_TAC std_ss [WELL_FORMED_SUB_thm, WF_TR_def, WF_Loop_def, run_cfl_def, run_arm_def] THEN
197   POP_ASSUM MP_TAC THEN Q.ABBREV_TAC `arm = translate ir` THEN STRIP_TAC THEN
198   Q.EXISTS_TAC `\s1 s0. if eval_il_cond cond (get_st s0) then F else (get_st s1 = get_st (runTo (upload arm (\i. ARB) (FST (FST s0)))
199             (FST (FST s0) + LENGTH (translate ir)) s0))` THEN
200   STRIP_TAC THENL [
201      FULL_SIMP_TAC std_ss [WF_DEF_2, GSYM RIGHT_FORALL_IMP_THM] THEN
202          STRIP_TAC THEN
203          POP_ASSUM (ASSUME_TAC o Q.SPEC `\st. ?pc cpsr pcS. (P:STATEPCS->bool) (((pc,cpsr,st),pcS):STATEPCS)`) THEN
204          STRIP_TAC THEN
205          FULL_SIMP_TAC std_ss [GSYM RIGHT_EXISTS_IMP_THM] THEN
206          `?st pc cpsr pcS. w = ((pc,cpsr,st),pcS)` by METIS_TAC [ABS_PAIR_THM] THEN
207          FULL_SIMP_TAC std_ss [] THEN RES_TAC THEN
208          Q.EXISTS_TAC `((pc',cpsr',st0),pcS')` THEN
209          RW_TAC std_ss [Once get_st_def] THEN RES_TAC THEN
210          `get_st (runTo (upload arm (\i. ARB) pc') (pc'+LENGTH arm) ((pc',cpsr',st0),pcS')) =
211              get_st (runTo (upload arm (\i. ARB) 0) (LENGTH arm) ((0,0w,st0),{}))` by
212              METIS_TAC [well_formed_def, get_st_def, DSTATE_IRRELEVANT_PCS, status_independent_def, FST, DECIDE (Term `!x.0 + x = x`)] THEN
213          METIS_TAC [FST,SND,get_st_def, ABS_PAIR_THM],
214
215      RW_TAC std_ss [get_st_def, eval_il_cond_def] THEN
216          METIS_TAC [WELL_FORMED_INSTB]
217      ]
218   );
219
220val WF_TR_LEM_2 = Q.store_thm (
221   "WF_TR_LEM_2",
222    `!cond ir prj_f f cond_f.
223        (!st. cond_f (prj_f st) = eval_il_cond cond st) /\ (!st. prj_f (run_cfl ir st) = f (prj_f st)) /\
224        WF (\t1 t0. ~cond_f t0 /\ (t1 = f t0)) ==>
225           WF (\st1 st0. ~eval_il_cond cond st0 /\ (st1 = run_cfl ir st0))`,
226
227   RW_TAC std_ss [WF_DEF_2] THEN
228   Q.PAT_ASSUM `!P.p` (ASSUME_TAC o Q.SPEC `\t:'a. ?y:DSTATE. (prj_f y = t) /\ P y`) THEN
229   FULL_SIMP_TAC std_ss [GSYM RIGHT_EXISTS_IMP_THM] THEN
230   RES_TAC THEN
231   Q.EXISTS_TAC `y` THEN
232   RW_TAC std_ss [] THEN
233   `~cond_f (prj_f y)` by METIS_TAC [] THEN
234   RES_TAC THEN
235   Q.PAT_ASSUM `!t1.p` (ASSUME_TAC o Q.SPEC `prj_f (st1:DSTATE)`) THEN
236   METIS_TAC []
237  );
238
239val WF_TR_LEM_3 = Q.store_thm (
240   "WF_TR_LEM_3",
241   `!cond_f f. (?R. WF R /\ !t0 t1. ~cond_f t0 ==> R (f t0) t0) ==>
242            WF (\t1 t0. ~cond_f t0 /\ (t1 = f t0))`,
243   RW_TAC std_ss [] THEN
244   MATCH_MP_TAC WF_SUBSET THEN
245   Q.EXISTS_TAC `R` THEN
246   RW_TAC std_ss []
247   );
248
249val WF_TR_THM_1 = Q.store_thm (
250   "WF_TR_THM_1",
251    `!cond ir prj_f f cond_f pre_p.
252        (!st. cond_f (prj_f st) = eval_il_cond cond st) /\
253        (!st. pre_p st ==> (prj_f (run_cfl ir st) = f (prj_f st))) /\
254        WF (\t1 t0. ~cond_f t0 /\ (t1 = f t0)) ==>
255           WF (\st1 st0. (pre_p st0) /\ ~(eval_il_cond cond st0) /\ (st1 = run_cfl ir st0))`,
256
257   RW_TAC std_ss [WF_DEF_2] THEN
258   Q.PAT_ASSUM `!P.p` (ASSUME_TAC o Q.SPEC `\t:'a. ?y:DSTATE. (prj_f y = t) /\ P y`) THEN
259   FULL_SIMP_TAC std_ss [GSYM RIGHT_EXISTS_IMP_THM] THEN
260   RES_TAC THEN
261   Q.EXISTS_TAC `y` THEN
262   RW_TAC std_ss [] THEN
263   `~cond_f (prj_f y)` by METIS_TAC [] THEN
264   RES_TAC THEN
265   Q.PAT_ASSUM `!y1.p` (ASSUME_TAC o Q.SPEC `prj_f (run_cfl ir y)`) THEN
266   METIS_TAC []
267  );
268
269(*---------------------------------------------------------------------------------*)
270(*      Hoare Rules on Projection on Inputs and Ouputs (represented                *)
271(*                    by projective functions                                      *)
272(*      The pre-conditions and post-conditions (on data other than inputs and      *)
273(*        outputs) are also specified                                              *)
274(*---------------------------------------------------------------------------------*)
275
276val PSPEC_def = Define `
277    PSPEC ir (pre_p,post_p) stk_f (in_f,f,out_f) =
278        !v x. HSPEC (\st. pre_p st /\ (stk_f st = x) /\ (in_f st = v))
279                 ir (\st. post_p st /\ (stk_f st = x) /\ (out_f st = f v))`;
280
281val _ = type_abbrev("PSPEC_TYPE", type_of (Term `PSPEC`));
282
283val PSPEC_STACK = Q.store_thm (
284   "PSPEC_STACK",
285   `!ir pre_p post_p stk_f in_f f out_f x.
286     PSPEC ir (pre_p,post_p) stk_f (in_f,f,out_f)
287       ==>
288       HSPEC (\st. pre_p st /\ (stk_f st = x)) ir (\st. post_p st /\ (stk_f st = x))`,
289     RW_TAC std_ss [PSPEC_def, HSPEC_def]
290   );
291
292val PSPEC_CHARACTERISTIC = Q.store_thm (
293   "PSPEC_CHARACTERISTIC",
294   `!ir pre_p post_p stk_f in_f f out_f.
295     PSPEC ir (pre_p,post_p) stk_f (in_f,f,out_f)
296       ==>
297       HSPEC (\st. pre_p st /\ (in_f st = v)) ir (\st. post_p st /\ (out_f st = f v))`,
298     RW_TAC std_ss [PSPEC_def, HSPEC_def]
299   );
300
301val PRJ_SHUFFLE_RULE = Q.store_thm (
302   "PRJ_SHUFFLE_RULE",
303   `!ir pre_p post_p stk_f in_f f out_f shuffle_f.
304     PSPEC ir (pre_p,post_p) stk_f (in_f,f,out_f)
305       ==>
306       PSPEC ir (pre_p, post_p) stk_f (in_f, shuffle_f o f, shuffle_f o out_f)`,
307     RW_TAC std_ss [PSPEC_def, HSPEC_def]
308   );
309
310val PRJ_SHUFFLE_RULE2 = Q.store_thm (
311   "PRJ_SHUFFLE_RULE2",
312   `!ir pre_p post_p stk_f in_f f out_f g in_f'.
313     PSPEC ir (pre_p, post_p) stk_f (in_f, f, out_f) /\ (g o in_f' = f o in_f)
314       ==>
315       PSPEC ir (pre_p,post_p) stk_f (in_f', g, out_f)`,
316     RW_TAC std_ss [PSPEC_def, HSPEC_def] THEN
317     METIS_TAC [FUN_EQ_THM, combinTheory.o_THM]
318   );
319
320val PRJ_SC_RULE = Q.store_thm (
321   "PRJ_SC_RULE",
322   `!ir1 ir2 pre_p1 post_p1 post_p2 stk_f in_f1 f1 f2 out_f1 out_f2.
323     WELL_FORMED ir1 /\ WELL_FORMED ir2 /\
324     PSPEC ir1 (pre_p1,post_p1) stk_f (in_f1,f1,out_f1) /\ PSPEC ir2 (post_p1,post_p2) stk_f (out_f1,f2,out_f2)
325       ==>
326       PSPEC (SC ir1 ir2) (pre_p1,post_p2) stk_f (in_f1,f2 o f1,out_f2)`,
327
328     RW_TAC std_ss [PSPEC_def] THEN
329     METIS_TAC [CFL_SC_RULE]
330   );
331
332val PRJ_CJ_RULE = Q.store_thm (
333   "PRJ_CJ_RULE",
334   `!cond ir_t ir_f pre_p post_p stk_f cond_f in_f f1 f2 out_f.
335     WELL_FORMED ir_t /\ WELL_FORMED ir_f /\
336     PSPEC ir_t (pre_p,post_p) stk_f (in_f,f1,out_f) /\
337     PSPEC ir_f (pre_p, post_p) stk_f (in_f,f2,out_f) /\ (!st. cond_f (in_f st) = eval_il_cond cond st)
338        ==>
339       PSPEC (CJ cond ir_t ir_f) (pre_p,post_p) stk_f (in_f, (\v.if cond_f v then f1 v else f2 v), out_f)`,
340
341     RW_TAC std_ss [PSPEC_def, HSPEC_def] THEN
342     METIS_TAC [CFL_SEMANTICS_CJ]
343   );
344
345(* Need the theorems in ARMCompositionTheory to prove the PROJ_TR_RULE *)
346
347val PRJ_TR_RULE = Q.store_thm (
348   "PRJ_TR_RULE",
349   `!cond ir pre_p stk_f cond_f prj_f f.
350        WELL_FORMED ir /\  WF (\st1 st0. ~eval_il_cond cond st0 /\ (st1 = run_cfl ir st0)) /\
351        (!st. cond_f (prj_f st) = eval_il_cond cond st) /\ PSPEC ir (pre_p,pre_p) stk_f (prj_f,f,prj_f) ==>
352          PSPEC (TR cond ir) (pre_p,pre_p) stk_f (prj_f, WHILE ($~ o cond_f) f, prj_f)`,
353
354    RW_TAC std_ss [PSPEC_def] THEN
355    RW_TAC std_ss [HSPEC_def] THENL [
356        FULL_SIMP_TAC std_ss [HSPEC_def] THEN
357            METIS_TAC [SIMP_RULE std_ss [HSPEC_def] CFL_TR_RULE, WF_TR_LEM_1],
358
359        IMP_RES_TAC (SIMP_RULE std_ss [PSPEC_def] PSPEC_STACK) THEN
360            POP_ASSUM (ASSUME_TAC o Q.SPEC `(stk_f:DSTATE->'a) st`) THEN
361            IMP_RES_TAC WF_TR_LEM_1 THEN
362            IMP_RES_TAC (Q.SPECL [`cond`,`ir`,`\st1. pre_p st1 /\ ((stk_f:DSTATE->'a)
363                                  st1 = (stk_f:DSTATE->'a) st)`] CFL_TR_RULE) THEN
364            POP_ASSUM (ASSUME_TAC o Q.SPEC `st` o SIMP_RULE std_ss [HSPEC_def]) THEN
365            METIS_TAC [],
366
367        IMP_RES_TAC (SIMP_RULE std_ss [PSPEC_def] PSPEC_CHARACTERISTIC) THEN
368            Q.PAT_ASSUM `!v x.p` (K ALL_TAC) THEN
369            `WF_TR (translate_condition cond,translate ir)` by METIS_TAC [WF_TR_LEM_1] THEN
370            FULL_SIMP_TAC std_ss [WELL_FORMED_SUB_thm, HSPEC_def, run_cfl_def, run_arm_def, translate_def, eval_il_cond_def] THEN
371            Q.ABBREV_TAC `arm = translate ir` THEN
372            IMP_RES_TAC (SIMP_RULE set_ss [] (Q.SPECL [`translate_condition cond`,`arm`,`(\i. ARB)`,`(0,0w,st):STATE`,`{}`]
373                              ARMCompositionTheory.UNROLL_TR_LEM)) THEN
374            POP_ASSUM (ASSUME_TAC o Q.SPEC `st`) THEN
375            FULL_SIMP_TAC std_ss [FUNPOW, ARMCompositionTheory.get_st_def] THEN
376            NTAC 2 (POP_ASSUM (K ALL_TAC)) THEN
377            Induct_on `loopNum (translate_condition cond) arm (\i.ARB) ((0,0w,st),{})` THENL [
378              REWRITE_TAC [Once EQ_SYM_EQ] THEN RW_TAC std_ss [FUNPOW,ARMCompositionTheory.get_st_def] THEN
379              IMP_RES_TAC ARMCompositionTheory.LOOPNUM_BASIC THEN
380              FULL_SIMP_TAC arith_ss [Once WHILE, ARMCompositionTheory.get_st_def],
381
382            REWRITE_TAC [Once EQ_SYM_EQ] THEN RW_TAC std_ss [FUNPOW] THEN
383        IMP_RES_TAC ARMCompositionTheory.LOOPNUM_INDUCTIVE THEN
384              `v = loopNum (translate_condition cond) arm (\i.ARB) ((0,0w,SND (SND (FST (runTo (upload arm (\i.ARB) 0) (LENGTH arm)
385                   ((0,0w,st),{}))))),{})` by METIS_TAC [ABS_PAIR_THM,DECIDE (Term`!x.0+x=x`),
386                       ARMCompositionTheory.LOOPNUM_INDEPENDENT_OF_CPSR_PCS, ARMCompositionTheory.get_st_def,
387                       FST, SND, ARMCompositionTheory.DSTATE_IRRELEVANT_PCS,ARMCompositionTheory.well_formed_def] THEN
388              RES_TAC THEN Q.PAT_ASSUM `v = x` (ASSUME_TAC o GSYM) THEN
389              FULL_SIMP_TAC std_ss [] THEN POP_ASSUM (K ALL_TAC) THEN
390              Q.PAT_ASSUM `v = x` (ASSUME_TAC o GSYM) THEN FULL_SIMP_TAC std_ss [] THEN POP_ASSUM (K ALL_TAC) THEN
391              Q.PAT_ASSUM `~x` (ASSUME_TAC o SIMP_RULE std_ss [ARMCompositionTheory.get_st_def]) THEN
392              RW_TAC std_ss [Once WHILE] THEN
393              Q.UNABBREV_TAC `arm` THEN
394              `run_cfl ir st = SND (SND (FST (runTo (upload (translate ir) (\i. ARB) 0) (LENGTH (translate ir))
395                  ((0,0w,st),{}))))` by RW_TAC arith_ss [
396                   ARMCompositionTheory.get_st_def, run_cfl_def, run_arm_def] THEN
397              METIS_TAC [SND,FST,ARMCompositionTheory.get_st_def,ARMCompositionTheory.FUNPOW_DSTATE, ABS_PAIR_THM]
398            ]
399     ]
400   );
401
402val PRJ_TR_RULE_2 = Q.store_thm (
403   "PRJ_TR_RULE_2",
404   `!cond ir stk_f cond_f prj_f f.
405        WELL_FORMED ir /\ (!st. cond_f (prj_f st) = eval_il_cond cond st) /\
406        (?R. WF R /\ !t0 t1. ~cond_f t0 ==> R (f t0) t0) /\
407           PSPEC ir ((\st.T),(\st.T)) stk_f (prj_f,f,prj_f) ==>
408                    PSPEC (TR cond ir) ((\st.T),(\st.T)) stk_f (prj_f, WHILE ($~ o cond_f) f, prj_f)`,
409
410    SIMP_TAC std_ss [PSPEC_def, HSPEC_def] THEN
411    REPEAT GEN_TAC THEN NTAC 2 STRIP_TAC THEN
412    `WF (\st1 st0. ~eval_il_cond cond st0 /\ (st1 = run_cfl ir st0))` by METIS_TAC [WF_TR_LEM_2, WF_TR_LEM_3] THEN
413    METIS_TAC [SIMP_RULE std_ss [PSPEC_def, HSPEC_def] (Q.SPECL [`cond`,`ir`,`\st.T`] PRJ_TR_RULE)]
414  );
415
416
417(*---------------------------------------------------------------------------------*)
418(*      Rules for Conditions (projective function version)                         *)
419(*---------------------------------------------------------------------------------*)
420
421val PRJ_STRENGTHEN_RULE = Q.store_thm (
422   "PRJ_STRENGTHEN_RULE",
423   `!ir pre_p pre_p' post_p stk_f in_f f out_f.
424     WELL_FORMED ir /\
425     PSPEC ir (pre_p,post_p) stk_f (in_f,f,out_f) /\ (!st. pre_p' st ==> pre_p st) ==>
426       PSPEC ir (pre_p',post_p) stk_f (in_f,f,out_f)`,
427     RW_TAC std_ss [PSPEC_def, HSPEC_def]
428   );
429
430val PRJ_WEAKEN_RULE = Q.store_thm (
431   "PRJ_WEAKEN_RULE",
432   `!ir pre_p post_p post_p' stk_f in_f f out_f.
433     WELL_FORMED ir /\
434     PSPEC ir (pre_p,post_p) stk_f (in_f,f,out_f) /\ (!st. post_p st ==> post_p' st) ==>
435       PSPEC ir (pre_p,post_p') stk_f (in_f,f,out_f)`,
436     RW_TAC std_ss [PSPEC_def, HSPEC_def]
437   );
438
439(*---------------------------------------------------------------------------------*)
440(*      Rules for Stack (projective function version)                              *)
441(*---------------------------------------------------------------------------------*)
442
443val valid_push_def = Define `
444    valid_push (stk_f,in_f,f,out_f) (stk_f',in_f',g,out_f') =
445      !st st'. (stk_f st' = stk_f st) /\ (out_f st' = f (in_f st)) ==>
446         (stk_f' st' = stk_f' st) /\ (out_f' st' = g (in_f' st))`;
447
448val PRJ_POP_RULE = Q.store_thm (
449   "PRJ_POP_RULE",
450   `!ir pre_p post_p stk_f in_f f out_f stk_f' in_f' g out_f'.
451      PSPEC ir (pre_p,post_p) stk_f (in_f,f,out_f) /\
452        valid_push (stk_f,in_f,f,out_f) (stk_f',in_f',g,out_f')
453       ==>
454        PSPEC ir (pre_p,post_p) stk_f' (in_f', g, out_f')`,
455    RW_TAC list_ss [PSPEC_def, HSPEC_def, valid_push_def]
456   );
457
458val P_intact_def = Define `
459    P_intact (P,Q) (stk_f,stk_g) =
460     !st st'. (stk_f st' = stk_f st) /\ P st /\ Q st'
461           ==> (stk_g st' = stk_g st)`;
462
463val PRJ_PUSH_RULE = Q.store_thm (
464   "PRJ_PUSH_RULE",
465   `!ir pre_p post_p stk_f in_f f out_f e_f stk_g.
466      PSPEC ir (pre_p,post_p) stk_f (in_f,f,out_f) /\
467        P_intact (pre_p,post_p) (stk_f,stk_g)
468      ==> PSPEC ir (pre_p,post_p) stk_g (in_f, f, out_f)`,
469    RW_TAC list_ss [PSPEC_def, HSPEC_def, P_intact_def]
470   );
471
472(*---------------------------------------------------------------------------------*)
473(*      Hoare Rules on Projection on Inputs and Ouputs (represented by vectors)    *)
474(*      To overcome the type restriction on tuples in HOL definitions              *)
475(*---------------------------------------------------------------------------------*)
476
477(*   Vectors *)
478
479val _ = Hol_datatype `
480    VEXP = SG of DATA                (* registers *)
481         | VT of VEXP # VEXP         (* pairs     *)
482    `;
483
484val readv_def = Define `
485     (readv st (PR (a,b)) = VT (readv st a, readv st b)) /\
486     (readv st x = SG (mread st x))`;
487
488
489(* Vector Stack, modelled as a list of expression vectors *)
490
491val push_def = Define `
492    push x stk = x :: stk`;
493
494val top_def = Define `
495    top  = HD`;
496
497val pop_def = Define `
498    pop  = TL`;
499
500(* Specification on vectors *)
501
502val VSPEC_def = Define `
503    VSPEC ir (pre_p,post_p) stk (iv,f,ov) =
504        PSPEC ir (pre_p,post_p) (\st. MAP (readv st) stk) ((\st.readv st iv), f, (\st.readv st ov))
505    `;
506
507val _ = type_abbrev("VSPEC_TYPE", type_of (Term `VSPEC`));
508
509val V_SHUFFLE_RULE = Q.store_thm (
510   "V_SHUFFLE_RULE",
511   `!ir stk iv f ov g iv'.
512     VSPEC ir (pre_p,post_p) stk (iv,f,ov) /\ (!st. g (readv st iv') = f (readv st iv))
513       ==>
514       VSPEC ir (pre_p,post_p) stk (iv', g, ov)`,
515     RW_TAC std_ss [VSPEC_def, PSPEC_def, HSPEC_def]
516   );
517
518val V_SC_RULE = Q.store_thm (
519   "V_SC_RULE",
520   `!ir1 ir2 pre_p1 post_p1 post_p2 stk vi1 f1 vo1 f2 vo2.
521     WELL_FORMED ir1 /\ WELL_FORMED ir2 /\
522     VSPEC ir1 (pre_p1,post_p1) stk (vi1,f1,vo1) /\ VSPEC ir2 (post_p1,post_p2) stk (vo1,f2,vo2)
523       ==>
524       VSPEC (SC ir1 ir2) (pre_p1,post_p2) stk (vi1,f2 o f1,vo2)`,
525     RW_TAC std_ss [VSPEC_def] THEN
526     METIS_TAC [PRJ_SC_RULE]
527   );
528
529val V_CJ_RULE = Q.store_thm (
530   "V_CJ_RULE",
531   `!cond ir_t ir_f pre_p post_p stk cond_f iv f1 f2 ov.
532     WELL_FORMED ir_t /\ WELL_FORMED ir_f /\
533     VSPEC ir_t (pre_p,post_p) stk (iv,f1,ov) /\
534     VSPEC ir_f (pre_p, post_p) stk (iv,f2,ov) /\ (!st. cond_f (readv st iv) = eval_il_cond cond st)
535        ==>
536       VSPEC (CJ cond ir_t ir_f) (pre_p,post_p) stk (iv, (\v.if cond_f v then f1 v else f2 v), ov)`,
537     RW_TAC std_ss [VSPEC_def] THEN
538     FULL_SIMP_TAC std_ss [PRJ_CJ_RULE]
539   );
540
541(* Need the theorems in ARMCompositionTheory to prove the PROJ_TR_RULE *)
542
543val V_TR_RULE = Q.store_thm (
544   "V_TR_RULE",
545   `!cond ir pre_p stk cond_f iv f.
546        WELL_FORMED ir /\  WF (\st1 st0. ~eval_il_cond cond st0 /\ (st1 = run_cfl ir st0)) /\
547        (!st. cond_f (readv st iv) = eval_il_cond cond st) /\ VSPEC ir (pre_p,pre_p) stk (iv,f,iv) ==>
548          VSPEC (TR cond ir) (pre_p,pre_p) stk (iv, WHILE ($~ o cond_f) f, iv)`,
549
550    RW_TAC std_ss [VSPEC_def] THEN
551    FULL_SIMP_TAC std_ss [PRJ_TR_RULE]
552   );
553
554(*---------------------------------------------------------------------------------*)
555(*      Rules for Conditions (vector version)                                      *)
556(*---------------------------------------------------------------------------------*)
557
558val V_STRENGTHEN_RULE = Q.store_thm (
559   "V_STRENGTHEN_RULE",
560   `!ir pre_p pre_p' post_p stk iv f ov.
561     WELL_FORMED ir /\
562     VSPEC ir (pre_p,post_p) stk (iv,f,ov) /\ (!st. pre_p' st ==> pre_p st) ==>
563       VSPEC ir (pre_p',post_p) stk (iv,f,ov)`,
564     RW_TAC std_ss [VSPEC_def] THEN
565     METIS_TAC [PRJ_STRENGTHEN_RULE]
566   );
567
568val V_WEAKEN_RULE = Q.store_thm (
569   "V_WEAKEN_RULE",
570   `!ir pre_p post_p post_p' stk iv f ov.
571     WELL_FORMED ir /\
572     PSPEC ir (pre_p,post_p) stk (iv,f,ov) /\ (!st. post_p st ==> post_p' st) ==>
573       PSPEC ir (pre_p,post_p') stk (iv,f,ov)`,
574     RW_TAC std_ss [VSPEC_def] THEN
575     METIS_TAC [PRJ_WEAKEN_RULE]
576   );
577
578(*---------------------------------------------------------------------------------*)
579(*      Rules for Stack (vector version)                                           *)
580(*---------------------------------------------------------------------------------*)
581
582val V_POP_RULE = Q.store_thm (
583   "V_POP_RULE",
584   `!ir pre_p post_p stk iv f ov e g.
585      VSPEC ir (pre_p,post_p) (e::stk) (iv,f,ov) /\
586       (!st. g (readv st (PR(iv,e))) = VT (f (readv st iv), readv st e)) ==>
587         VSPEC ir (pre_p,post_p) stk (PR(iv,e), g, PR(ov,e))`,
588    RW_TAC list_ss [VSPEC_def, PSPEC_def, HSPEC_def, readv_def]
589   );
590
591val V_intact_def = Define `
592    V_intact (P,Q,e) =
593      ?x. (!st.P st ==> (readv st e = x)) /\ (!st.Q st ==> (readv st e = x))`;
594
595
596val V_PUSH_RULE = Q.store_thm (
597   "V_PUSH_RULE",
598   `!ir pre_p post_p stk iv f ov e.
599      VSPEC ir (pre_p,post_p) stk (iv,f,ov) /\ V_intact(pre_p, post_p, e)
600      ==>
601         VSPEC ir (pre_p,post_p) (e::stk) (iv, f, ov)`,
602    RW_TAC list_ss [VSPEC_def, PSPEC_def, HSPEC_def, V_intact_def, readv_def] THEN
603    METIS_TAC []
604   );
605
606
607(*---------------------------------------------------------------------------------*)
608(*      Rules for Well-formedness                                                  *)
609(*---------------------------------------------------------------------------------*)
610
611val WELL_FORMED_TR_RULE = Q.store_thm (
612   "WELL_FORMED_TR_RULE",
613   `!cond ir context_f.
614        WELL_FORMED ir /\  WF (\st1 st0. ~eval_il_cond cond st0 /\ (st1 = run_cfl ir st0)) ==>
615           WELL_FORMED (TR cond ir)`,
616
617    RW_TAC std_ss [] THEN
618    METIS_TAC [CFL_TR_IS_WELL_FORMED, WF_TR_LEM_1]
619   );
620
621val _ = export_theory();
622