source: src/ERTL/ERTLToLTLProof.ma @ 3259

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

changed ERTL semantics:
1) added manipulation of stack pointer directly in the semantics
2) added values of Callee Saved in frames

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