source: src/ERTL/ERTLToLTLProof.ma @ 3253

Last change on this file since 3253 was 3253, checked in by piccolo, 6 years ago

some proof obbligation closed of ERTL to LTL proof

File size: 42.2 KB
Line 
1include "ERTL/ERTLToLTL.ma".
2include "ERTL/ERTL_semantics.ma".
3include "LTL/LTL_semantics.ma".
4include "common/AssocList.ma".
5include "joint/StatusSimulationHelper.ma".
6include "ERTL/MoveCorrectness.ma".
7
8(* Inefficient, replace with Trie lookup *)
9definition lookup_stack_cost ≝
10 λp.λid : ident.
11  assoc_list_lookup ? ℕ id (eq_identifier …) p.
12
13(*TO BE MOVED*)
14definition ERTL_status ≝
15λprog : ertl_program.λstack_sizes.
16joint_abstract_status (mk_prog_params ERTL_semantics prog stack_sizes).
17
18definition LTL_status ≝
19λprog : ltl_program.λstack_sizes.
20joint_abstract_status (mk_prog_params LTL_semantics prog stack_sizes).
21
22definition local_clear_sb_type ≝ decision → bool.
23definition clear_sb_type ≝ label → local_clear_sb_type.
24
25(*function that will be used in order to retrieve ERTL-states from LTL-states.
26  Now it is an axiom. To be Implemented *)
27axiom to_be_cleared_sb : 
28∀live_before : valuation register_lattice.
29coloured_graph live_before → clear_sb_type.
30
31definition local_clear_fb_type ≝ vertex → bool.
32definition clear_fb_type ≝ label → local_clear_fb_type.
33
34
35(*function that will be used in order to clear ERTL-states from dead registers.
36  Now it is an axiom. To be implemented *)
37definition to_be_cleared_fb :
38∀live_before : valuation register_lattice.clear_fb_type≝
39λlive_before,pt,v.notb (lives v (live_before pt)).
40
41include "common/ExtraIdentifiers.ma".
42
43definition sigma_fb_register_env : local_clear_fb_type → register_env beval →
44register_env beval ≝
45λclear_fun,regs.find_all … regs (λi.λ_.notb (clear_fun (inl ?? i))).
46
47definition register_of_bitvector :  BitVector 6 → option Register≝
48λvect.
49let n ≝ nat_of_bitvector … vect in
50if eqb n 0 then Some ? Register00
51else if eqb n 1 then Some ? Register01
52else if eqb n 2 then Some ? Register02
53else if eqb n 3 then Some ? Register03
54else if eqb n 4 then Some ? Register04
55else if eqb n 5 then Some ? Register05
56else if eqb n 6 then Some ? Register06
57else if eqb n 7 then Some ? Register07
58else if eqb n 8 then Some ? Register10
59else if eqb n 9 then Some ? Register11
60else if eqb n 10 then Some ? Register12
61else if eqb n 11 then Some ? Register13
62else if eqb n 12 then Some ? Register14
63else if eqb n 13 then Some ? Register15
64else if eqb n 14 then Some ? Register16
65else if eqb n 15 then Some ? Register17
66else if eqb n 16 then Some ? Register20
67else if eqb n 17 then Some ? Register21
68else if eqb n 18 then Some ? Register22
69else if eqb n 19 then Some ? Register23
70else if eqb n 20 then Some ? Register24
71else if eqb n 21 then Some ? Register25
72else if eqb n 22 then Some ? Register26
73else if eqb n 23 then Some ? Register27
74else if eqb n 24 then Some ? Register30
75else if eqb n 25 then Some ? Register31
76else if eqb n 26 then Some ? Register32
77else if eqb n 27 then Some ? Register33
78else if eqb n 28 then Some ? Register34
79else if eqb n 29 then Some ? Register35
80else if eqb n 30 then Some ? Register36
81else if eqb n 31 then Some ? Register37
82else if eqb n 32 then Some ? RegisterA
83else if eqb n 33 then Some ? RegisterB
84else if eqb n 34 then Some ? RegisterDPL
85else if eqb n 35 then Some ? RegisterDPH
86else if eqb n 36 then Some ? RegisterCarry (* was -1, increment as needed *)
87else None ?.
88
89
90
91definition sigma_fb_hw_register_env : local_clear_fb_type → hw_register_env →
92hw_register_env ≝
93λclear_fun,regs.
94let f ≝ λvect,val,m.
95  match register_of_bitvector vect with
96  [ Some r ⇒
97     if (clear_fun (inr ?? r)) then
98      m
99     else
100      insert … vect val m
101  | None ⇒ m
102  ] in
103mk_hw_register_env … (fold … f (reg_env … regs) (Stub …)) BBundef.
104
105definition sigma_fb_regs : local_clear_fb_type → ertl_reg_env → ertl_reg_env ≝
106λclear_fun,regs.〈sigma_fb_register_env clear_fun (\fst regs),
107                 sigma_fb_hw_register_env clear_fun (\snd regs)〉.
108
109definition sigma_fb_frames : local_clear_fb_type →
110list (register_env beval × (Σb:block.block_region b=Code)) →
111list (register_env beval × (Σb:block.block_region b=Code)) ≝ 
112λclear_fun,frms.map … (λx.〈sigma_fb_register_env clear_fun (\fst x),\snd x〉) frms.
113
114definition sigma_fb_state:
115 ertl_program → local_clear_fb_type →
116  state ERTL_semantics → state ERTL_semantics ≝
117λprog,clear_fun,st.
118mk_state ?
119 (option_map ?? (sigma_fb_frames clear_fun) (st_frms … st))
120 (istack … st)
121 (if clear_fun (inr ?? RegisterCarry) then BBundef
122  else (carry … st))
123 (sigma_fb_regs clear_fun (regs … st)) (m … st) (stack_usage … st).
124
125axiom acc_is_dead : ∀fix_comp.∀prog : ertl_program.
126 ∀fn : joint_closed_internal_function ERTL (prog_names … prog). ∀l.
127 let after ≝ analyse_liveness fix_comp (prog_names … prog) fn in
128  ¬ lives (inr ? ? RegisterA) (livebefore  … fn after l).
129
130axiom dead_registers_in_dead :
131 ∀fix_comp.∀build : coloured_graph_computer.
132 ∀prog : ertl_program.
133 ∀fn : joint_closed_internal_function ERTL (prog_names … prog).
134 ∀l.
135 let after ≝ analyse_liveness fix_comp (prog_names … prog) fn in
136 let coloured_graph ≝ build … fn after in
137 ∀R : Register.
138  ¬ lives (inr ? ? R) (livebefore  … fn after l) →
139   to_be_cleared_sb … coloured_graph l R.
140   
141axiom sigma_sb_state: list (Σb.block_region b = Code) →
142 ertl_program → local_clear_sb_type → state LTL_semantics → state ERTL_semantics.
143
144definition dummy_state : state ERTL_semantics ≝
145mk_state ERTL_semantics
146   (None ?) empty_is BBundef 〈empty_map ? ?,mk_hw_register_env … (Stub …) BBundef〉
147   empty O.
148
149definition dummy_state_pc : state_pc ERTL_semantics ≝
150mk_state_pc ? dummy_state (null_pc one) (null_pc one).
151
152definition get_ertl_call_stack :
153list (register_env beval × (Σb:block.block_region b=Code)) →
154list (Σb:block.block_region b=Code) ≝ map … \snd.
155
156definition sigma_fb_state_pc :
157 fixpoint_computer → coloured_graph_computer → ertl_program → 
158  state_pc ERTL_semantics → state_pc ERTL_semantics ≝
159 λfix_comp,colour,prog,st.
160 let m ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in
161 let stacksizes ≝ lookup_stack_cost … m in 
162 let ge ≝ joint_globalenv ERTL_semantics prog stacksizes in
163 let globals ≝ prog_names … prog in
164 match fetch_internal_function … ge (pc_block (pc … st)) with
165  [ OK y ⇒
166     let pt ≝ point_of_pc ERTL_semantics (pc ? st) in
167     let after ≝ (analyse_liveness fix_comp (prog_names … prog) (\snd y)) in
168     let before ≝ livebefore … (\snd y) after in
169     mk_state_pc ? (sigma_fb_state prog (to_be_cleared_fb before pt) st) (pc … st) 
170      (last_pop … st)
171  | Error e ⇒ dummy_state_pc
172  ].
173
174definition sigma_sb_state_pc:
175 fixpoint_computer → coloured_graph_computer → 
176  ertl_program → list (Σb:block.block_region b=Code) → 
177  (block → list register) → lbl_funct_type →
178  regs_funct_type →  state_pc LTL_semantics → state_pc ERTL_semantics ≝
179 λfix_comp,build,prog,cs,init_regs,f_lbls,f_regs,st.
180  let init ≝ (λglobals,fn.«translate_data fix_comp build globals fn,?») in
181  let m ≝ (\snd (\fst (ertl_to_ltl fix_comp build prog))) in
182  let stacksizes ≝ lookup_stack_cost … m in 
183  let ge ≝ joint_globalenv ERTL_semantics prog stacksizes in
184  let globals ≝ prog_names … prog in
185  match fetch_internal_function … ge (pc_block (pc … st)) with
186  [ OK y ⇒ 
187     let pt ≝ point_of_pc ERTL_semantics (pc ? st) in
188     let after ≝ (analyse_liveness fix_comp (prog_names … prog) (\snd y)) in
189     let coloured_graph ≝ build … (\snd y) after in
190     mk_state_pc ? (sigma_sb_state cs prog
191                       (to_be_cleared_sb … coloured_graph pt) st) (pc … st) 
192                   (sigma_stored_pc ERTL_semantics LTL_semantics
193                      prog stacksizes init init_regs f_lbls f_regs (last_pop … st))
194  | Error e ⇒ dummy_state_pc
195  ].
196@hide_prf % qed.
197
198definition state_rel : fixpoint_computer → coloured_graph_computer →
199ertl_program → joint_state_relation ERTL_semantics LTL_semantics ≝
200λfix_comp,build,prog,pc,st1,st2.
201let m ≝ (\snd (\fst (ertl_to_ltl fix_comp build prog))) in
202let stacksizes ≝ lookup_stack_cost … m in 
203let ge ≝ joint_globalenv ERTL_semantics prog stacksizes in
204∃f,fn.fetch_internal_function … ge (pc_block pc)
205= return 〈f,fn〉 ∧
206let after ≝ (analyse_liveness fix_comp (prog_names … prog) fn) in
207let before ≝ livebefore … fn after in
208let coloured_graph ≝ build … fn after in
209match st_frms … st1 with
210[ None ⇒ False
211| Some frames ⇒
212 (sigma_fb_state prog (to_be_cleared_fb before (point_of_pc ERTL_semantics pc)) st1) =
213  (sigma_sb_state (get_ertl_call_stack frames) prog
214   (to_be_cleared_sb … coloured_graph (point_of_pc ERTL_semantics pc)) st2)
215].
216
217definition state_pc_rel :
218fixpoint_computer → coloured_graph_computer → 
219  ertl_program → (block → list register) → lbl_funct_type →
220  regs_funct_type →  joint_state_pc_relation ERTL_semantics LTL_semantics ≝
221 λfix_comp,build,prog,init_regs,f_lbls,f_regs,st1,st2.
222match st_frms … (st_no_pc … st1) with
223[ None ⇒ False
224| Some frames ⇒
225   sigma_fb_state_pc fix_comp build prog st1 =
226    sigma_sb_state_pc fix_comp build prog (get_ertl_call_stack frames) init_regs
227     f_lbls f_regs st2
228].
229
230axiom insensitive_to_be_cleared_sb :
231 ∀prog. ∀tb : local_clear_sb_type. ∀st : state LTL_LIN_state.
232  ∀d : decision.∀bv,st',localss,cs.tb d →
233  write_decision localss d bv st = return st' →
234   sigma_sb_state cs prog tb st =
235    sigma_sb_state cs prog tb st'.
236   
237lemma hw_reg_retrieve_write_decision_hit : ∀r : Register.∀bv : beval.∀localss.
238∀st : state LTL_LIN_state.
239∀st'. (write_decision localss r bv st) = return st' →
240hw_reg_retrieve (regs … st') r = return bv.
241#r #bv #localss #st #st' whd in match write_decision; normalize nodelta
242whd in match hw_reg_store; normalize nodelta >m_return_bind
243whd in ⊢ (??%% → ?); #EQ destruct(EQ)
244whd in match hw_reg_retrieve; normalize nodelta @eq_f
245whd in match hwreg_retrieve; whd in match hwreg_store; normalize nodelta
246@lookup_insert_hit
247qed.
248
249definition sigma_beval : fixpoint_computer → coloured_graph_computer → 
250  ertl_program → (block → list register) → lbl_funct_type →
251  regs_funct_type → beval → beval≝
252 λfix_comp,build,prog,init_regs,f_lbls,f_regs,bv.
253  let init ≝ (λglobals,fn.«translate_data fix_comp build globals fn,?») in
254  let m ≝ (\snd (\fst (ertl_to_ltl fix_comp build prog))) in
255  let stacksizes ≝ lookup_stack_cost … m in
256  match bv with
257  [ BVpc pc p ⇒ match sigma_pc_opt ERTL_semantics LTL_semantics prog stacksizes
258                       init init_regs f_lbls f_regs pc
259                with [Some pc' ⇒ BVpc pc' p | None ⇒ BVundef]
260  | _ ⇒ bv
261  ].
262  @hide_prf % qed.
263
264axiom ps_reg_retrieve_hw_reg_retrieve_commute :
265∀fix_comp,colour,prog,init_regs,f_lbls,f_regs,fn,pc.
266let after ≝ (analyse_liveness fix_comp (prog_names … prog) fn) in
267gen_preserving2 ?? gen_res_preserve ??????
268     (state_rel fix_comp colour prog pc)
269     (λr : register.λd : arg_decision.d =
270      (colouring … (colour (prog_names … prog) fn after)
271       (inl register Register r)))
272     (λbv,bv'.bv = sigma_beval fix_comp colour prog init_regs f_lbls f_regs bv') …
273     (λst1.ps_reg_retrieve (regs … st1))
274     (λst,d.m_map Res ?? (\fst …)
275      (read_arg_decision (joint_if_local_stacksize ?? fn) st d)).
276     
277(*set_theoretical axioms *)
278axiom set_member_empty :∀A.∀DEC.∀a.¬set_member A DEC a (set_empty …).   
279axiom set_member_singl : ∀A,DEC,a.set_member A DEC a (set_singleton … a).
280axiom set_member_union1 : ∀A,DEC,x,y,a.set_member A DEC a x →
281set_member A DEC a (set_union … x y).
282axiom set_member_union2 : ∀A,DEC,x,y,a.set_member A DEC a y →
283set_member A DEC a (set_union … x y).
284axiom set_member_diff : ∀A,DEC,x,y,a.set_member A DEC a x →
285¬set_member A DEC a y →
286set_member A DEC a (set_diff … x y).
287axiom set_member_subset_if:
288 ∀A,DEC,S1,S2.
289  set_subset A DEC S1 S2 →
290   ∀x. set_member A DEC x S1 → set_member A DEC x S2.
291axiom set_member_subset_onlyif:
292 ∀A,DEC,S1,S2.
293  (∀x. set_member A DEC x S1 → set_member A DEC x S2) →
294   set_subset A DEC S1 S2.
295   
296lemma all_used_are_live_before :
297∀fix_comp.
298∀prog : ertl_program.
299∀fn : joint_closed_internal_function ERTL (prog_names … prog).
300∀l,stmt.
301stmt_at … (joint_if_code … fn) l = return stmt →
302∀r : register. set_member ? (eq_identifier …) r (\fst (used ? stmt)) →
303let after ≝ (analyse_liveness fix_comp (prog_names … prog) fn) in
304eliminable ? (after l) stmt = false →
305lives (inl ? ? r)  (livebefore  … fn after l).
306#fix_comp #prog #fn #l *
307[ * [#c|* [#c_id | #c_ptr] #args #dest | #a #lbl | *
308[ #str
309| * * [#r1 | #R1]  * [1,3: * [1,3: #r |2,4: #R] |2,4: #b]
310| #a
311| * [ #r | #b]
312| #i #i_spec #w #dpl #dph
313| #op #a #b * [#r | #by]  * [1,3: #r'|2,4: #by']
314| #op #a #a'
315| * #a #a' * [1,3,5,7,9,11: #r |2,4,6,8,10,12: #b]
316|
317|
318| #a #dpl #dph
319| #dpl #dph #a
320| * [|| #r ] (*|| * [|| #r] | #r #lbl | #r #lbl ] *)
321]
322] #nxt| * [ #lbl | | *] |*]
323#EQstmt #r #H #H1 whd in match (lives ??); normalize  nodelta
324whd in match (livebefore ????);  whd in EQstmt : (??%?); >EQstmt
325normalize nodelta -EQstmt whd in match (statement_semantics ???);
326whd in match(\fst ?); try( @(set_member_union2) assumption) >H1
327normalize nodelta whd in match(\fst ?); @(set_member_union2) assumption
328qed.
329
330lemma bool_of_beval_sigma_commute :
331∀fix_comp,colour,prog,init_regs,f_lbls,f_regs.
332gen_preserving … gen_res_preserve …
333(λbv,bv'.bv = sigma_beval fix_comp colour prog init_regs f_lbls f_regs bv')
334(λb1,b2.b1=b2) … bool_of_beval bool_of_beval.
335#fix_comp #colour #prog #init_regs #f_lbls #f_regs whd in match bool_of_beval;
336normalize nodelta * normalize nodelta
337[|| #p1 #p2 #p| #b| #p | #ptr #p | #pc #p ]
338try (#y #_ @res_preserve_error_gen)
339* whd in match sigma_beval; normalize nodelta
340[1,8,15,22: |2,9,16,23: |3,10,17,24: #p1' #p2' #p'|4,11,18,25: #b'|5,12,19,26: #p'
341|6,13,20,27: #ptr' #p'|7,14,21,28: #pc' #p'] #EQ destruct(EQ) try (@m_gen_return %)
342cases(sigma_pc_opt ?????????) in EQ; normalize nodelta
343[2,4,6,8: #pc''] #EQ destruct(EQ)
344qed.
345
346lemma map_eval_add_dummy_variance_id :
347∀X,Y.∀l,x.map_eval X Y (add_dummy_variance X Y l) x =l.
348#X #Y #l elim l [//] #hd #tl normalize #IH #x >IH %
349qed.
350
351lemma state_pc_eq : ∀p.∀st1,st2 : state_pc p.
352st1 = st2 → st_no_pc … st1 = st_no_pc … st2 ∧
353pc … st1 = pc … st2 ∧ last_pop … st1 = last_pop … st2.
354#p * #st1 #pc1 #lp1 * #st2 #pc2 #lp2 #EQ destruct(EQ)
355%{(refl …)} %{(refl …)} %
356qed.
357
358(* Cut&paste da un altro file con nome split_on_last_append, unificare*)
359lemma split_on_last_append_singl : ∀A : Type[0]. ∀pre : list A.
360∀ last : A. split_on_last ? (pre@[last]) = return 〈pre,last〉.
361#A #pre elim pre [#last %] #a #tl #IH #last whd in ⊢ (??%?);lapply(IH last)
362whd in ⊢ (??%? → ?); #EQ >EQ %
363qed.
364
365lemma split_on_last_append : ∀A : Type[0]. ∀l1,l2: list A.
366 OptPred True (λres.
367  split_on_last ? (l1@l2) = return 〈l1 @ \fst res, \snd res〉)
368  (split_on_last … l2).
369#A #l1 #l2 lapply l1 -l1 @(list_elim_left … l2) //
370#hd #tl #IH #l1 whd >split_on_last_append_singl whd
371<associative_append @split_on_last_append_singl
372qed.
373
374lemma injective_OK: ∀A:Type[0].∀a,b:A. OK … a = OK … b → a=b.
375 #A #a #b #EQ destruct %
376qed.
377
378lemma eq_notb_true_to_eq_false:
379 ∀b. (¬b) = true → b = false.
380* // #abs normalize in abs; destruct
381qed.
382
383lemma fold_insert_singleton : ∀A,B : Type[0].∀a :A.
384∀i : Pos.∀f,b.
385fold A B f (pm_set A i (Some ? a) (pm_leaf A)) b = f i a b.
386#A #B #a #i elim i -i normalize
387[//] #i #IH #f #b @IH
388qed.
389
390lemma eq_f' : ∀A,B : Type[0].∀f,g : A → B. ∀x,y : A.
391(∀w. f w = g w) → x = y → f x = g y. //
392qed.
393
394lemma add_find_all_miss :  ∀tag,A.∀m : identifier_map tag A.
395∀P : (identifier tag → A → bool).∀i,a.notb (P i a) →
396find_all tag A (add tag A m i a) P =
397match lookup tag A m i with
398[ None ⇒ find_all tag A m P
399| Some a ⇒ if P i a then find_all tag A (remove tag A m i) P else find_all tag A m P
400].
401cases daemon
402qed.
403   
404     
405lemma sigma_fb_state_insensitive_to_dead_reg:
406 ∀prog,bv. ∀st: state ERTL_semantics. ∀l:label.
407 ∀r: register. ∀before.
408  set_member … (eq_identifier RegisterTag) r (\fst  (before l)) = false →
409  sigma_fb_state prog
410   (to_be_cleared_fb before l)
411   (set_regs ERTL_semantics
412    〈reg_store r bv (\fst  (regs ERTL_semantics st)),
413    \snd  (regs ERTL_semantics st)〉 st)
414  = sigma_fb_state prog (to_be_cleared_fb before l) st.
415#prog #bv #st #l #r #before #dead whd in match sigma_fb_state; normalize nodelta
416@eq_f3 [2,3: %] whd in match set_regs; normalize nodelta whd in match sigma_fb_regs;
417normalize nodelta @eq_f2 [2: %] whd in match sigma_fb_register_env;
418normalize nodelta whd in match reg_store; normalize nodelta
419>add_find_all_miss [2: normalize >dead %] cases(lookup ????) [%] #a
420normalize nodelta whd in match to_be_cleared_fb; whd in match lives;
421normalize nodelta whd in match (plives ??); >dead %
422qed.
423
424lemma sigma_fb_state_insensitive_to_dead_Reg:
425 ∀prog,bv. ∀st: state ERTL_semantics. ∀l:label.
426 ∀r: Register. ∀before.
427  set_member … eq_Register r (\snd  (before l)) = false →
428  sigma_fb_state prog
429   (to_be_cleared_fb before l)
430   (set_regs ERTL_semantics
431     〈\fst  (regs ERTL_semantics st),
432      hwreg_store r bv (\snd  (regs ERTL_semantics st))〉
433      st)
434  = sigma_fb_state prog (to_be_cleared_fb before l) st.
435cases daemon (*TODO*)
436qed.
437
438lemma sigma_fb_state_insensitive_to_dead_carry:
439 ∀prog,bv. ∀st: state ERTL_semantics. ∀l:label. ∀before.
440  set_member Register eq_Register RegisterCarry (\snd (before l)) = false →
441   sigma_fb_state prog (to_be_cleared_fb before l) (set_carry ERTL_semantics bv st) =
442   sigma_fb_state prog (to_be_cleared_fb before l) st.
443#prog #b #st #l #cefore #dead whd in match sigma_fb_state; normalize nodelta
444whd in match set_carry; normalize nodelta whd in match to_be_cleared_fb;
445normalize nodelta whd in match (lives ??); >dead %
446qed.
447
448lemma split_orb_false: ∀a,b:bool. orb a b = false → a = false ∧ b = false.
449 ** normalize #abs destruct /2/
450qed.
451
452lemma eta_set_carry:
453 ∀P,st. set_carry P (carry P st) st = st.
454#P * //
455qed.
456
457lemma set_carry_set_regs_commute:
458 ∀P,st,c,v. set_carry P c (set_regs P v st) = set_regs P v (set_carry P c st).
459 #P * //
460qed.
461
462lemma eliminable_step_to_eq_livebefore_liveafter:
463 ∀prog,stackcost,fn.
464 let p_in ≝ mk_prog_params ERTL_semantics prog stackcost in
465 ∀st1: joint_abstract_status p_in.
466 ∀stms: joint_seq ERTL_semantics (prog_names … prog). ∀next.
467 let pt ≝ point_of_pc ERTL_semantics (pc ? st1) in
468 stmt_at p_in ? (joint_if_code p_in … fn) pt = return (sequential … stms next) →
469 ∀liveafter.
470 eliminable_step (globals … p_in) (liveafter (point_of_pc ERTL_semantics (pc … st1))) stms = true →
471  livebefore … fn liveafter pt = liveafter pt.
472 #prog #stackcost #fn #st1 #stms #next #stmt_at #liveafter #Helim
473 whd in ⊢ (??%?); whd in stmt_at:(??%?); cases (lookup ????) in stmt_at;
474 normalize nodelta try (#abs whd in abs:(??%%); destruct (abs) @I)
475 #stms' #EQ whd in EQ:(??%%); destruct (EQ) whd in ⊢ (??%?);
476 whd in match eliminable; normalize nodelta >Helim %
477qed.
478
479lemma set_subset_to_set_subst_set_union_left:
480 ∀T,eqT,A,B,C. set_subset T eqT A B → set_subset … eqT A (set_union … B C).
481 #T #eqT #A #B #C #H @set_member_subset_onlyif #x #K
482 lapply (set_member_subset_if … H) #H2 /3 by set_member_union1/
483qed.
484
485lemma set_subset_to_set_subst_set_union_right:
486 ∀T,eqT,A,B,C. set_subset T eqT A C → set_subset … eqT A (set_union … B C).
487 #T #eqT #A #B #C #H @set_member_subset_onlyif #x #K
488 lapply (set_member_subset_if … H) #H2 /3 by set_member_union2/
489qed.
490
491lemma rl_included_rl_join_left:
492 ∀A,B,C. rl_included A B → rl_included A (rl_join B C).
493 #A #B #C whd in match rl_included; normalize nodelta #H
494 cases (andb_Prop_true … H) -H #H1 #H2 @andb_Prop
495 /2 by set_subset_to_set_subst_set_union_left/
496qed.
497
498lemma rl_included_rl_join_right:
499 ∀A,B,C. rl_included A C → rl_included A (rl_join B C).
500 #A #B #C whd in match rl_included; normalize nodelta #H
501 cases (andb_Prop_true … H) -H #H1 #H2 @andb_Prop
502 /2 by set_subset_to_set_subst_set_union_right/
503qed.
504
505lemma set_subset_reflexive: ∀A,DEC,x. set_subset A DEC x x.
506 /2/
507qed.
508
509lemma rl_included_reflexive: ∀x. rl_included x x.
510 /2/
511qed.
512
513include alias "utilities/deqsets_extra.ma".
514
515lemma mem_of_fold_join:
516 ∀F,dom.
517  ∀x. x ∈ dom →
518   rl_included (F x)
519    (fold label (l_property register_lattice) rl_join rl_bottom (λl:label.true)
520      F dom).
521 #F #dom elim dom [ #x * ] #hd #tl #IH #x whd in match (? ∈ ?);
522 @eqb_elim
523 normalize nodelta #Hx #H change with (rl_join ??) in ⊢ (?(??%));
524 destruct /3 by rl_included_rl_join_left,rl_included_rl_join_right/
525qed.
526
527lemma set_subset_transitive:
528 ∀A,DEC,S1,S2,S3.
529  set_subset A DEC S1 S2 → set_subset … DEC S2 S3 → set_subset … DEC S1 S3.
530 #A #DEC #S1 #S2 #S3
531 #H1 lapply (set_member_subset_if … H1) -H1 #H1
532 #H2 lapply (set_member_subset_if … H2) -H2 #H2
533 @set_member_subset_onlyif /3 by/
534qed.
535
536lemma rl_included_transitive:
537 ∀S1,S2,S3. rl_included S1 S2 → rl_included S2 S3 → rl_included S1 S3.
538 #S1 #S2 #S3 whd in match rl_included; normalize nodelta
539 #H cases (andb_Prop_true … H) -H #H1 #H2
540 #H cases (andb_Prop_true … H) -H #H3 #H4
541 /3 by andb_Prop,set_subset_transitive/
542qed.
543
544lemma rl_included_rl_diff_rl_empty:
545 ∀S1. rl_included S1 (rl_diff S1 rl_bottom).
546 #S1 whd in match (rl_included ??);
547 lapply (set_member_subset_onlyif … (eq_identifier …) (\fst S1) (\fst (rl_diff S1 rl_bottom)))
548 cases (set_subset ????)
549 /3 by set_member_diff,set_member_subset_onlyif/
550qed.
551
552lemma included_livebefore_livebeafter_stmt_labels:
553 ∀fix_comp,globals,fn,l,stmt.
554  let after ≝ analyse_liveness fix_comp globals fn in
555   stmt_at … (joint_if_code ERTL … fn) l = Some … stmt →
556  ∀nxt.
557   nxt ∈
558    stmt_labels (mk_stmt_params (g_u_pars ERTL) label (Some label) false)
559     globals stmt →
560  l_included register_lattice (livebefore … fn after nxt) (after l).
561#fix_comp #globals #fn #l #stmt letin after ≝ (analyse_liveness ???) #EQlookup #nxt
562#Hnxt lapply (fix_correct … after l) #spec @(rl_included_transitive … spec) -spec
563whd in match (liveafter ????); whd in EQlookup:(??%?); >EQlookup -EQlookup normalize nodelta
564/2 by mem_of_fold_join/
565qed.
566
567axiom eq_sigma_state_monotonicity:
568 ∀prog,live,graph,st1,st2,l1,l2,frames.
569 st_frms ? st1 = return frames →
570  rl_included (live l2) (live l1) →
571  sigma_fb_state prog (to_be_cleared_fb live l1) st1 =
572   sigma_sb_state (get_ertl_call_stack frames) prog
573    (to_be_cleared_sb live graph l1) st2 →
574  sigma_fb_state prog (to_be_cleared_fb live l2) st1 =
575   sigma_sb_state (get_ertl_call_stack frames) prog
576    (to_be_cleared_sb live graph l2) st2.
577
578
579
580lemma fetch_ok_sigma_state_ok : ∀fix_comp,colour,prog,init_regs,f_lbls,f_regs.
581let m ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in
582let stacksizes ≝ lookup_stack_cost … m in
583∀st1,st2,f,fn. state_pc_rel fix_comp colour prog init_regs f_lbls f_regs st1 st2 →
584fetch_internal_function …
585(joint_globalenv ERTL_semantics prog stacksizes) (pc_block (pc … st1)) 
586     = return 〈f,fn〉 →
587let after ≝ (analyse_liveness fix_comp (prog_names … prog) fn) in
588let before ≝ livebefore … fn after in
589let coloured_graph ≝ colour … fn after in
590match st_frms … (st_no_pc … st1) with
591[ None ⇒ False
592| Some frames ⇒
593 (sigma_fb_state prog
594  (to_be_cleared_fb before (point_of_pc ERTL_semantics (pc … st1)))
595  (st_no_pc … st1)) =
596 (sigma_sb_state (get_ertl_call_stack frames) prog
597   (to_be_cleared_sb … coloured_graph (point_of_pc ERTL_semantics (pc … st1)))
598  (st_no_pc … st2))
599].
600#fix_comp #colour #prog #init_regs #f_lbls #f_regs #st1 #st2 #f #fn
601#H #EQfn whd in match state_pc_rel in H; normalize nodelta in H;
602inversion (st_frms … st1) in H; [ #_ *] #frames #EQframes normalize nodelta
603whd in match sigma_fb_state_pc; whd in match sigma_sb_state_pc;
604normalize nodelta >EQfn normalize nodelta inversion(fetch_internal_function ????)
605[2: #e #_ normalize nodelta whd in match dummy_state_pc; whd in match null_pc;
606    normalize nodelta #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
607    >fetch_internal_function_no_zero in EQfn; [2: >e1 %] whd in ⊢ (???% → ?);
608    #ABS destruct(ABS) ]
609* #f1 #fn1 #EQfn1 normalize nodelta #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ
610destruct(EQ) <e1 in EQfn1; >EQfn whd in ⊢ (??%?? → ?); #EQ1 destruct(EQ1)
611whd in match sigma_fb_state; normalize nodelta >e0 >e1 %
612qed.
613     
614lemma fetch_ok_pc_ok : ∀fix_comp,colour,prog,init_regs,f_lbls,f_regs.
615let m ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in
616let stacksizes ≝ lookup_stack_cost … m in
617∀st1,st2,f,fn. state_pc_rel fix_comp colour prog init_regs f_lbls f_regs st1 st2 →
618fetch_internal_function …
619(joint_globalenv ERTL_semantics prog stacksizes) (pc_block (pc … st1)) 
620     = return 〈f,fn〉 → (pc … st1) = (pc … st2).
621#fix_comp #colour #prog #init_regs #f_lbls #f_regs #st1 #st2 #f #fn
622#H #EQfn whd in match state_pc_rel in H; normalize nodelta in H;
623inversion (st_frms … st1) in H; [ #_ *] #frames #EQframes normalize nodelta
624whd in match sigma_fb_state_pc; whd in match sigma_sb_state_pc;
625normalize nodelta >EQfn normalize nodelta inversion(fetch_internal_function ????)
626[2: #e #_ normalize nodelta whd in match dummy_state_pc; whd in match null_pc;
627    normalize nodelta #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
628    >fetch_internal_function_no_zero in EQfn; [2: >e1 %] whd in ⊢ (???% → ?);
629    #ABS destruct(ABS) ]
630* #f1 #fn1 #EQfn1 normalize nodelta #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ
631destruct(EQ) <e1 in EQfn1; >EQfn whd in ⊢ (??%?? → ?); #EQ1 destruct(EQ1) %
632qed.
633
634axiom colouring_reg_non_DPL_DPH : ∀fix_comp,colour,prog.
635let m ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in
636let stacksizes ≝ lookup_stack_cost … m in
637∀bl,f,fn,R.∀r : register.
638fetch_internal_function …
639(joint_globalenv ERTL_semantics prog stacksizes) bl = return 〈f,fn〉 →
640let after ≝ (analyse_liveness fix_comp (prog_names … prog) fn) in
641let before ≝ livebefore … fn after in
642colouring before (colour … fn after) (inl register Register r) =
643decision_colour R → R ≠ RegisterDPL ∧ R ≠ RegisterDPH ∧
644R ≠ RegisterA.
645
646axiom insensitive_to_be_cleared_sb_regs :
647∀prog.∀tb : local_clear_sb_type. ∀st : state LTL_LIN_state.
648∀bv.∀r : Register.∀cs.∀rgs. tb r →
649sigma_sb_state cs prog tb (set_regs LTL_semantics rgs st) =
650sigma_sb_state cs prog tb (set_regs LTL_semantics
651          (hwreg_store r bv rgs) st).
652
653axiom insensitive_sb_to_hwreg_set_other :
654∀prog.∀tb : local_clear_sb_type. ∀st : state LTL_LIN_state.
655∀b,cs,rgs.
656sigma_sb_state cs prog tb
657 (set_regs LTL_semantics (hwreg_set_other b rgs) st) =
658sigma_sb_state cs prog tb (set_regs LTL_semantics rgs st).
659
660axiom insensitive_to_be_cleared_carry :
661∀prog.∀tb : local_clear_sb_type. ∀st : state LTL_LIN_state.
662∀b.∀cs. tb RegisterCarry →
663sigma_sb_state cs prog tb (set_carry LTL_semantics b st) =
664sigma_sb_state cs prog tb st.
665
666axiom dpl_is_dead : ∀fix_comp.∀prog : ertl_program.
667 ∀fn : joint_closed_internal_function ERTL (prog_names … prog). ∀l.
668 let after ≝ analyse_liveness fix_comp (prog_names … prog) fn in
669  ¬ lives (inr ? ? RegisterDPL) (livebefore  … fn after l).
670
671axiom dph_is_dead : ∀fix_comp.∀prog : ertl_program.
672 ∀fn : joint_closed_internal_function ERTL (prog_names … prog). ∀l.
673 let after ≝ analyse_liveness fix_comp (prog_names … prog) fn in
674  ¬ lives (inr ? ? RegisterDPH) (livebefore  … fn after l).
675
676lemma m_return_if_commute :  ∀M : Monad.∀A : Type[0]. ∀a1,a2 : A.∀b : bool.
677if b then m_return M A a1 else m_return M A a2 =
678m_return M A (if b then a1 else a2).
679#M #A #a1 #a2 * %
680qed.
681
682lemma set_carry_eta :∀p.∀st : state p.set_carry p (carry … st) st = st.
683#p * //
684qed.
685
686lemma set_regs_eta :∀p.∀st : state p. set_regs p (regs … st) st = st.
687#p * //
688qed.
689
690lemma carry_sensitive_read_arg_decision :
691∀prog.∀tb : local_clear_sb_type. ∀st,st' : state LTL_LIN_state.∀d,cs,bv,localss.
692read_arg_decision localss st d = return 〈bv,st'〉 →
693tb RegisterDPL → tb RegisterDPH → 
694sigma_sb_state cs prog tb (set_carry … (carry … st') st) =
695sigma_sb_state cs prog tb st'.
696#prog #tb #st #st' * [#R | #n | #b ] #cs #bv #localss whd in match read_arg_decision;
697normalize nodelta [1,3: whd in ⊢ (??%% → ?); #EQ destruct(EQ) #_ #_ >set_carry_eta %]
698>m_return_bind >m_return_bind #H @('bind_inversion H) -H * #bv1 #b1 #_
699#H @('bind_inversion H) -H * #bv2 #b2 #_ #H @('bind_inversion H) -H #ptr #_ #H
700@('bind_inversion H) -H #bv3 #_ whd in ⊢ (??%% → ?); #EQ destruct(EQ) #H1 #H2
701whd in match set_carry; normalize nodelta
702change with (set_regs ?? (set_carry ? b2 st)) in ⊢ (???(????%));
703<insensitive_to_be_cleared_sb_regs [2: assumption] <insensitive_to_be_cleared_sb_regs
704[2: assumption] whd in match set_regs; whd in match set_carry; normalize nodelta %
705qed.
706
707axiom set_carry_sigma_sb_state_commute :
708∀prog,cs.∀st,st' : state LTL_LIN_state. ∀tb : local_clear_sb_type.
709sigma_sb_state cs prog tb (set_carry  … (carry … st') st) =
710set_carry … (carry … (sigma_sb_state cs prog tb st'))
711 (sigma_sb_state cs prog tb st).
712
713lemma cond_commute :∀fix_comp,colour,prog,init_regs,f_lbls,f_regs.
714let p_out ≝ (\fst (\fst (ertl_to_ltl fix_comp colour prog))) in
715let m ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in
716let n ≝ \snd (ertl_to_ltl fix_comp colour prog) in
717let stacksizes ≝ lookup_stack_cost … m in
718let init ≝ (λglobals,fn.«translate_data fix_comp colour globals fn,?») in
719cond_commutation_statement ERTL_semantics LTL_semantics prog stacksizes
720 init init_regs
721 f_lbls f_regs (state_rel fix_comp colour prog)
722 (state_pc_rel fix_comp colour prog init_regs f_lbls f_regs).
723[2: @hide_prf %]
724#fix_comp #colour #prog #init_regs #f_lbls #f_regs
725whd in match cond_commutation_statement; normalize nodelta
726#st1 #st2 #f #fn #r #ltrue #lfalse #bv #b * #Hbl #EQfetch
727whd in match acca_retrieve; normalize nodelta change with (ps_reg_retrieve ??) in ⊢ (??%? → ?);
728#EQbv #EQb #Rst1st2 #t_fn #EQt_fn whd normalize nodelta %{(refl …)} #mid #EQmid
729cases(ps_reg_retrieve_hw_reg_retrieve_commute fix_comp colour prog init_regs f_lbls
730f_regs fn (pc … st1) … (colouring … (inl ?? r)) … EQbv)
731[6: %
732|2: @(st_no_pc … st2)
733|5: whd %{f} %{fn} >(proj1 … (fetch_statement_inv … EQfetch)) %{(refl …)}
734    @(fetch_ok_sigma_state_ok … Rst1st2 …
735         (proj1 ?? (fetch_statement_inv … EQfetch)))
736|*:
737]
738#bv1 * inversion(colouring … (inl ?? r))
739[ #n #EQcolouring
740| #R #EQcolouring
741  cases(colouring_reg_non_DPL_DPH …
742                      (proj1 ?? (fetch_statement_inv … EQfetch)) … EQcolouring)
743  * #RnoDPL #RnoDPH #RnoA
744]
745whd in match m_map; normalize nodelta #H @('bind_inversion H) -H *
746#bv2 #st' #EQbv2 whd in ⊢ (??%% → ?); #EQ1 #EQ2 destruct(EQ1 EQ2)
747% [2,4: %
748     [1,3: >map_eval_add_dummy_variance_id in ⊢ (??%?); >move_spec in ⊢ (??%?);
749       [2: @I | 4:  %{RnoDPL RnoDPH}] normalize nodelta
750       [ >EQbv2 in ⊢ (??%?); | >EQbv2 in ⊢ (??%?); ] >m_return_bind
751       whd in match write_decision; normalize nodelta >m_return_bind
752       >m_return_if_commute in ⊢ (??%?); %
753     |*: %
754       [1,3: whd %{f} %{fn} %
755           [1,3,5,7: @if_elim #_ >(proj1 … (fetch_statement_inv … EQfetch)) %]
756           normalize nodelta
757           lapply(fetch_ok_sigma_state_ok … Rst1st2 …
758                                    (proj1 ?? (fetch_statement_inv … EQfetch)))
759           normalize nodelta inversion (st_frms … (st_no_pc … st1)) [1,3: #_ * ]
760           #frames #EQframes normalize nodelta #R_nopc_st1st2
761           [ inversion(hlives RegisterCarry
762              (analyse_liveness fix_comp
763               (prog_names ERTL_semantics prog) fn
764               (point_of_pc ERTL_semantics (pc … st1))))
765             [ #carry_live | #carry_dead ]
766           | @eq_Register_elim [ #EQ destruct(EQ) @⊥ cases RnoA #H @H %] #_
767           ]
768           normalize nodelta
769           [ >insensitive_sb_to_hwreg_set_other
770             whd in match set_regs in ⊢ (???(????(??%?))); normalize nodelta ]
771           <insensitive_to_be_cleared_sb_regs
772           [2,4,6: @dead_registers_in_dead @acc_is_dead ]
773           [ whd in match set_regs; whd in match set_carry; normalize nodelta
774             change with (set_carry ? (carry … (st_no_pc … st2)) st') in ⊢ (???(????%));
775             >set_carry_sigma_sb_state_commute
776           |*: >set_regs_eta
777           ]
778           <(carry_sensitive_read_arg_decision … EQbv2)
779           [2,3,5,6,8,9: @dead_registers_in_dead [1,3,5: @dph_is_dead |*: @dpl_is_dead]]
780           [ >set_carry_sigma_sb_state_commute
781             change with (set_carry ?? (sigma_sb_state ? prog ? (st_no_pc … st2)))
782                                                                            in ⊢ (???%);
783             >set_carry_eta
784           | >insensitive_to_be_cleared_carry
785             [2: @dead_registers_in_dead cases daemon (*????*) ]
786           | whd in EQbv2 : (??%%); destruct(EQbv2) >set_carry_eta
787           ]
788           @(eq_sigma_state_monotonicity … EQframes … R_nopc_st1st2)
789           cases b normalize nodelta >point_of_pc_of_point
790           letin after ≝ (analyse_liveness fix_comp … fn)
791           letin before ≝ (livebefore … fn after)
792           lapply (included_livebefore_livebeafter_stmt_labels
793                      fix_comp … (proj2 ?? (fetch_statement_inv … EQfetch)))
794           normalize in match (stmt_labels ???);
795           change with after in match after;
796           #H [2,4,6: lapply (H lfalse ?) [1,3,5: >memb_hd % ]
797              |*: lapply (H ltrue ?) [1,3,5: >memb_cons try % >memb_hd %]]
798           #K change with (bool_to_Prop (rl_included ??)) in K;
799           @(rl_included_transitive … K) whd in match (livebefore ????);
800           cases(fetch_statement_inv … EQfetch) #_ normalize nodelta
801           whd in ⊢ (??%? → ?); #EQstmt >EQstmt normalize nodelta
802           @rl_included_rl_join_left normalize in match (defined ??);
803           @rl_included_rl_diff_rl_empty
804       |*: %{it} %{(refl …)} %{bv1} %
805           [1,3: [ @if_elim #_
806                 | @eq_Register_elim [ #EQ destruct(EQ) @⊥ cases RnoA #H @H %] #_
807                 ]
808                 normalize nodelta change with (hw_reg_retrieve ??) in ⊢ (??%?);
809                 whd in match hw_reg_retrieve; normalize nodelta @eq_f
810                 whd in match set_regs; normalize nodelta
811                 [ >hwreg_retrieve_insensitive_to_set_other]
812                 >hwreg_retrieve_hwregstore_hit %
813           |*: cases(bool_of_beval_sigma_commute fix_comp colour prog init_regs
814                      f_lbls f_regs … bv1 … EQb) [2,4: %] #b1 * #EQb1 #EQ destruct(EQ)
815                      assumption
816           ]
817       ]
818    ]     
819  |*:
820  ]
821qed.
822           
823lemma seq_commute :∀fix_comp,colour,prog,init_regs,f_lbls,f_regs.
824let p_out ≝ (\fst (\fst (ertl_to_ltl fix_comp colour prog))) in
825let m ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in
826let n ≝ \snd (ertl_to_ltl fix_comp colour prog) in
827let stacksizes ≝ lookup_stack_cost … m in
828let init ≝ (λglobals,fn.«translate_data fix_comp colour globals fn,?») in
829seq_commutation_statement ERTL_semantics LTL_semantics prog stacksizes
830 init init_regs
831 f_lbls f_regs (state_rel fix_comp colour prog)
832 (state_pc_rel fix_comp colour prog init_regs f_lbls f_regs).
833[2: @hide_prf %]
834cases daemon (*TODO*)
835qed.
836
837lemma return_commute :∀fix_comp,colour,prog,init_regs,f_lbls,f_regs.
838let p_out ≝ (\fst (\fst (ertl_to_ltl fix_comp colour prog))) in
839let m ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in
840let n ≝ \snd (ertl_to_ltl fix_comp colour prog) in
841let stacksizes ≝ lookup_stack_cost … m in
842let init ≝ (λglobals,fn.«translate_data fix_comp colour globals fn,?») in
843return_commutation_statement ERTL_semantics LTL_semantics prog stacksizes
844 init init_regs
845 f_lbls f_regs (state_rel fix_comp colour prog)
846 (state_pc_rel fix_comp colour prog init_regs f_lbls f_regs).
847[2: @hide_prf %]
848cases daemon (*TODO*)
849qed.
850
851lemma pre_main_commute : ∀fix_comp,colour,prog,init_regs,f_lbls,f_regs.
852let p_out ≝ (\fst (\fst (ertl_to_ltl fix_comp colour prog))) in
853let m ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in
854let n ≝ \snd (ertl_to_ltl fix_comp colour prog) in
855let stacksizes ≝ lookup_stack_cost … m in
856let init ≝ (λglobals,fn.«translate_data fix_comp colour globals fn,?») in
857b_graph_transform_program_props ERTL_semantics LTL_semantics stacksizes
858  init prog init_regs f_lbls f_regs →
859pre_main_commutation_statement  ERTL_semantics LTL_semantics prog stacksizes
860 init init_regs
861 f_lbls f_regs (state_rel fix_comp colour prog)
862 (state_pc_rel fix_comp colour prog init_regs f_lbls f_regs).
863[2: @hide_prf %]
864cases daemon qed.
865
866(*
867#fix_comp #colour #prog #init_regs #f_lbls #f_regs #good whd
868#st1 #st1' #st2 #EQbl whd in match eval_state; normalize nodelta
869whd in match fetch_statement; whd in match fetch_internal_function; normalize nodelta
870whd in match fetch_function; normalize nodelta @eqZb_elim [2: * #H @⊥ @H assumption]
871#_ normalize nodelta >m_return_bind #H @('bind_inversion H) -H ** #f #fn #stmt
872#H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H #stmt1
873#H lapply(opt_eq_from_res ???? H) -H whd in ⊢ (??%% → ?); cases st1 in EQbl; -st1
874#st1 * #bl1 #pos1 #lp1 #EQbl1 normalize nodelta cases pos1 -pos1 normalize nodelta
875[ #EQ destruct(EQ)
876|*: * [2,3,5,6: #x ] whd in ⊢ (??%% → ?); #EQ destruct
877]
878whd in ⊢ (??%% → ?); #EQ destruct(EQ) normalize nodelta whd in match eval_statement_no_pc; normalize inversion(point_of_pc ERTL_semantics (pc … st1))
879*)
880
881lemma call_commute : ∀fix_comp,colour,prog,init_regs,f_lbls,f_regs.
882let p_out ≝ (\fst (\fst (ertl_to_ltl fix_comp colour prog))) in
883let m ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in
884let n ≝ \snd (ertl_to_ltl fix_comp colour prog) in
885let stacksizes ≝ lookup_stack_cost … m in
886let init ≝ (λglobals,fn.«translate_data fix_comp colour globals fn,?») in
887call_commutation_statement ERTL_semantics LTL_semantics prog stacksizes
888 init init_regs
889 f_lbls f_regs (state_rel fix_comp colour prog)
890 (state_pc_rel fix_comp colour prog init_regs f_lbls f_regs).
891[2: @hide_prf %]
892cases daemon qed.
893
894lemma goto_commute : ∀fix_comp,colour,prog,init_regs,f_lbls,f_regs.
895let p_out ≝ (\fst (\fst (ertl_to_ltl fix_comp colour prog))) in
896let m ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in
897let n ≝ \snd (ertl_to_ltl fix_comp colour prog) in
898let stacksizes ≝ lookup_stack_cost … m in
899let init ≝ (λglobals,fn.«translate_data fix_comp colour globals fn,?») in
900goto_commutation_statement ERTL_semantics LTL_semantics prog stacksizes
901 init init_regs
902 f_lbls f_regs (state_rel fix_comp colour prog)
903 (state_pc_rel fix_comp colour prog init_regs f_lbls f_regs).
904[2: @hide_prf %]
905cases daemon qed.
906
907lemma tailcall_commute : ∀fix_comp,colour,prog,init_regs,f_lbls,f_regs.
908let p_out ≝ (\fst (\fst (ertl_to_ltl fix_comp colour prog))) in
909let m ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in
910let n ≝ \snd (ertl_to_ltl fix_comp colour prog) in
911let stacksizes ≝ lookup_stack_cost … m in
912let init ≝ (λglobals,fn.«translate_data fix_comp colour globals fn,?») in
913tailcall_commutation_statement ERTL_semantics LTL_semantics prog stacksizes
914 init init_regs
915 f_lbls f_regs (state_rel fix_comp colour prog)
916 (state_pc_rel fix_comp colour prog init_regs f_lbls f_regs).
917[2: @hide_prf %]
918#fix_comp #colour #prog #init_regs #f_lbls #f_regs whd #st1 #st2
919#f #fn *
920qed.
921
922             
923theorem ERTLToLTL_ok :
924∀fix_comp : fixpoint_computer.
925∀colour : coloured_graph_computer.
926∀p_in : ertl_program.
927let 〈p_out, m, n〉 ≝ ertl_to_ltl fix_comp colour p_in in
928(* what should we do with n? *)
929let stacksizes ≝ lookup_stack_cost m in
930∀init_in.make_initial_state
931  (mk_prog_params ERTL_semantics p_in stacksizes) = OK … init_in →
932∃init_out.
933  make_initial_state
934   (mk_prog_params LTL_semantics p_out stacksizes) =
935    OK ? init_out ∧
936∃[1] R.
937  status_simulation_with_init
938    (joint_status ERTL_semantics p_in stacksizes)
939    (joint_status LTL_semantics p_out stacksizes)
940    R init_in init_out.
941#fix_comp #colour #p_in #init_in #EQinit_in
942letin p_out ≝ (\fst (\fst (ertl_to_ltl fix_comp colour p_in)))
943letin m ≝ (\snd (\fst (ertl_to_ltl fix_comp colour p_in)))
944letin n ≝ (\snd (ertl_to_ltl fix_comp colour p_in))
945letin stacksizes ≝ (lookup_stack_cost m)
946cases(make_b_graph_transform_program_props ERTL_semantics LTL_semantics stacksizes
947     (λglobals : list ident.λfn.«translate_data fix_comp colour globals fn,(refl …)») p_in)
948#init_regs * #f_lbls * #f_regs #good
949@(joint_correctness ERTL_semantics LTL_semantics p_in stacksizes
950(λglobals : list ident.λfn.«translate_data fix_comp colour globals fn,(refl …)»)
951init_regs f_lbls f_regs (state_rel fix_comp colour p_in)
952(state_pc_rel fix_comp colour p_in init_regs f_lbls f_regs) ? ? init_in EQinit_in)
953%
954[ @good
955| #st1 #st2 #f #fn #Rst1st2 #EQfn whd %{f} %{fn} %{EQfn}
956  @(fetch_ok_sigma_state_ok fix_comp colour p_in … Rst1st2 EQfn)
957| #st1 #st2 #f #fn #Rst1st2 #EQfn @(fetch_ok_pc_ok fix_comp colour p_in … Rst1st2 EQfn)
958| #st1 #st2 #f #fn #Rst1st2 #EQfn lapply Rst1st2 whd in match state_pc_rel;
959  normalize nodelta cases(st_frms … st1) [*] #frames normalize nodelta
960  whd in match sigma_fb_state_pc; whd in match sigma_sb_state_pc; normalize nodelta
961  >EQfn normalize nodelta <(fetch_ok_pc_ok … Rst1st2 EQfn) >EQfn normalize nodelta
962  #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) assumption
963| #st1 #st2 #pc #lp1 #lp2 #f #fn #EQfn #Rst1st2 #EQ destruct(EQ) whd
964  lapply Rst1st2 whd in match state_rel; normalize nodelta * #f1 * #fn1 >EQfn *
965  whd in ⊢ (??%% → ?); #EQ destruct(EQ) cases(st_frms … st1) [*] #frames
966  normalize nodelta #EQst whd in match sigma_fb_state_pc;
967  whd in match sigma_sb_state_pc; normalize nodelta >EQfn
968  normalize nodelta @eq_f3 [2,3: % | assumption]
969| @pre_main_commute assumption
970| #f #fn * #bl #pos #EQbl whd in match fetch_statement;
971  whd in match fetch_internal_function; whd in match fetch_function;
972  normalize nodelta @eqZb_elim [2: * #H @⊥ @H assumption]
973  #_ normalize nodelta >m_return_bind #H @('bind_inversion H) -H #stmt 
974  #H lapply(opt_eq_from_res ???? H) -H whd in ⊢ (??%% → ?);
975  whd in match point_of_pc; normalize nodelta cases pos normalize nodelta
976  [ #EQ destruct(EQ)
977  |*: * [2,3,5,6: #x ] whd in ⊢ (??%% → ?); #EQ destruct
978  ]
979  whd in ⊢ (??%% → ?); #EQ destruct(EQ)
980| @cond_commute
981| @seq_commute
982| #f #fn #bl #EQfn #id #args #dest #lbl whd #bl'
983  %{(match id with [inl f1 ⇒ inl ?? f1 | inr x ⇒ inr ?? 〈it,it〉])}
984  %{args} %{it} normalize nodelta cases id [ #f1 % | * #dpl #dph %]
985| cases daemon (*TODO*)
986| @return_commute
987| @call_commute
988| @goto_commute
989| @tailcall_commute
990| cases daemon (*TODO*)
991| cases daemon (*TODO*)
992| cases daemon (*TODO*)
993| cases daemon (*TODO*)
994]
995qed.
Note: See TracBrowser for help on using the repository browser.