source: src/ERTL/ERTLToLTLProof.ma @ 3261

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

reverted joint_semantics rtl_semantics and ltl_semantics

File size: 41.4 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  ¬ in_lattice (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.bv1 = sigma_beval fix_comp build prog init_regs f_lbls f_regs bv2 in
167let live_fun ≝ λv.in_lattice 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
207
208lemma ps_reg_retrieve_hw_reg_retrieve_commute :
209∀fix_comp,colour,prog,init_regs,f_lbls,f_regs.∀f : ident.
210∀fn : joint_closed_internal_function ERTL (prog_names … prog).
211∀pc.
212let m1 ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in
213let stacksizes ≝ lookup_stack_cost … m1 in 
214let after ≝ (analyse_liveness fix_comp (prog_names … prog) fn) in
215fetch_internal_function … (joint_globalenv ERTL_semantics prog stacksizes)
216(pc_block pc) = return 〈f,fn〉 → 
217gen_preserving2 ?? gen_res_preserve ??????
218     (state_rel fix_comp colour prog init_regs f_lbls f_regs pc)
219     (λr :Σr : register.bool_to_Prop(in_lattice (inl ?? r)
220       (livebefore … fn after (point_of_pc ERTL_semantics pc))).λd : decision.d =
221      (colouring … (colour (prog_names … prog) fn after)
222       (inl register Register r)))
223     (λbv,bv'.bv = sigma_beval fix_comp colour prog init_regs f_lbls f_regs bv') …
224     (λst1.ps_reg_retrieve (regs … st1))
225     (λst,d.m_map Res ?? (\fst …)
226      (read_arg_decision (joint_if_local_stacksize ?? fn) st d)).
227#fix_comp #colour #prog #init_regs #f_lbls #f_regs #f #fn #pc #EQfn #st1 #st2
228* #r #Hr #d whd in match state_rel; normalize nodelta * #f1 * #fn1
229>EQfn * whd in ⊢ (??%% → ?); #EQ destruct(EQ) inversion(st_frms … st1)
230[#_ *] #frames #EQframes normalize nodelta ***** #Hmem #Hrames #Hw_relation
231#His #Hcarry * #ptr * #EQptr whd in match ps_relation; whd in match gen_preserving;
232normalize nodelta #H #EQd #bv #EQbv cases(H «r,Hr» d ? bv EQbv)
233[2: <EQd in ⊢ (??%?); %] #bv' cases d
234[2: #R normalize nodelta * whd in ⊢ (??%% → ?); #EQ destruct(EQ)
235    change with (hwreg_retrieve ??) in match (lookup ?????);
236    #Hrel %{(hwreg_retrieve (regs … st2) R)} %
237    [ whd in match m_map; whd in match read_arg_decision; normalize nodelta %]
238    assumption ]
239xxxxxxxxxxxx
240
241[ #R whd in match ps_relation; normalize nodelta whd in match gen_preserving;
242normalize nodelta #H #EQR #bv #EQbv cases(H «r,Hr» R
243     
244(*set_theoretical axioms *)
245axiom set_member_empty :∀A.∀DEC.∀a.¬set_member A DEC a (set_empty …).   
246axiom set_member_singl : ∀A,DEC,a.set_member A DEC a (set_singleton … a).
247axiom set_member_union1 : ∀A,DEC,x,y,a.set_member A DEC a x →
248set_member A DEC a (set_union … x y).
249axiom set_member_union2 : ∀A,DEC,x,y,a.set_member A DEC a y →
250set_member A DEC a (set_union … x y).
251axiom set_member_diff : ∀A,DEC,x,y,a.set_member A DEC a x →
252¬set_member A DEC a y →
253set_member A DEC a (set_diff … x y).
254axiom set_member_subset_if:
255 ∀A,DEC,S1,S2.
256  set_subset A DEC S1 S2 →
257   ∀x. set_member A DEC x S1 → set_member A DEC x S2.
258axiom set_member_subset_onlyif:
259 ∀A,DEC,S1,S2.
260  (∀x. set_member A DEC x S1 → set_member A DEC x S2) →
261   set_subset A DEC S1 S2.
262   
263lemma all_used_are_live_before :
264∀fix_comp.
265∀prog : ertl_program.
266∀fn : joint_closed_internal_function ERTL (prog_names … prog).
267∀l,stmt.
268stmt_at … (joint_if_code … fn) l = return stmt →
269∀r : register. set_member ? (eq_identifier …) r (\fst (used ? stmt)) →
270let after ≝ (analyse_liveness fix_comp (prog_names … prog) fn) in
271eliminable ? (after l) stmt = false →
272lives (inl ? ? r)  (livebefore  … fn after l).
273#fix_comp #prog #fn #l *
274[ * [#c|* [#c_id | #c_ptr] #args #dest | #a #lbl | *
275[ #str
276| * * [#r1 | #R1]  * [1,3: * [1,3: #r |2,4: #R] |2,4: #b]
277| #a
278| * [ #r | #b]
279| #i #i_spec #w #dpl #dph
280| #op #a #b * [#r | #by]  * [1,3: #r'|2,4: #by']
281| #op #a #a'
282| * #a #a' * [1,3,5,7,9,11: #r |2,4,6,8,10,12: #b]
283|
284|
285| #a #dpl #dph
286| #dpl #dph #a
287| * [|| #r ] (*|| * [|| #r] | #r #lbl | #r #lbl ] *)
288]
289] #nxt| * [ #lbl | | *] |*]
290#EQstmt #r #H #H1 whd in match (lives ??); normalize  nodelta
291whd in match (livebefore ????);  whd in EQstmt : (??%?); >EQstmt
292normalize nodelta -EQstmt whd in match (statement_semantics ???);
293whd in match(\fst ?); try( @(set_member_union2) assumption) >H1
294normalize nodelta whd in match(\fst ?); @(set_member_union2) assumption
295qed.
296
297lemma bool_of_beval_sigma_commute :
298∀fix_comp,colour,prog,init_regs,f_lbls,f_regs.
299gen_preserving … gen_res_preserve …
300(λbv,bv'.bv = sigma_beval fix_comp colour prog init_regs f_lbls f_regs bv')
301(λb1,b2.b1=b2) … bool_of_beval bool_of_beval.
302#fix_comp #colour #prog #init_regs #f_lbls #f_regs whd in match bool_of_beval;
303normalize nodelta * normalize nodelta
304[|| #p1 #p2 #p| #b| #p | #ptr #p | #pc #p ]
305try (#y #_ @res_preserve_error_gen)
306* whd in match sigma_beval; normalize nodelta
307[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'
308|6,13,20,27: #ptr' #p'|7,14,21,28: #pc' #p'] #EQ destruct(EQ) try (@m_gen_return %)
309cases(sigma_pc_opt ?????????) in EQ; normalize nodelta
310[2,4,6,8: #pc''] #EQ destruct(EQ)
311qed.
312
313lemma map_eval_add_dummy_variance_id :
314∀X,Y.∀l,x.map_eval X Y (add_dummy_variance X Y l) x =l.
315#X #Y #l elim l [//] #hd #tl normalize #IH #x >IH %
316qed.
317
318lemma state_pc_eq : ∀p.∀st1,st2 : state_pc p.
319st1 = st2 → st_no_pc … st1 = st_no_pc … st2 ∧
320pc … st1 = pc … st2 ∧ last_pop … st1 = last_pop … st2.
321#p * #st1 #pc1 #lp1 * #st2 #pc2 #lp2 #EQ destruct(EQ)
322%{(refl …)} %{(refl …)} %
323qed.
324
325(* Cut&paste da un altro file con nome split_on_last_append, unificare*)
326lemma split_on_last_append_singl : ∀A : Type[0]. ∀pre : list A.
327∀ last : A. split_on_last ? (pre@[last]) = return 〈pre,last〉.
328#A #pre elim pre [#last %] #a #tl #IH #last whd in ⊢ (??%?);lapply(IH last)
329whd in ⊢ (??%? → ?); #EQ >EQ %
330qed.
331
332lemma split_on_last_append : ∀A : Type[0]. ∀l1,l2: list A.
333 OptPred True (λres.
334  split_on_last ? (l1@l2) = return 〈l1 @ \fst res, \snd res〉)
335  (split_on_last … l2).
336#A #l1 #l2 lapply l1 -l1 @(list_elim_left … l2) //
337#hd #tl #IH #l1 whd >split_on_last_append_singl whd
338<associative_append @split_on_last_append_singl
339qed.
340
341lemma injective_OK: ∀A:Type[0].∀a,b:A. OK … a = OK … b → a=b.
342 #A #a #b #EQ destruct %
343qed.
344
345lemma eq_notb_true_to_eq_false:
346 ∀b. (¬b) = true → b = false.
347* // #abs normalize in abs; destruct
348qed.
349
350lemma fold_insert_singleton : ∀A,B : Type[0].∀a :A.
351∀i : Pos.∀f,b.
352fold A B f (pm_set A i (Some ? a) (pm_leaf A)) b = f i a b.
353#A #B #a #i elim i -i normalize
354[//] #i #IH #f #b @IH
355qed.
356
357lemma eq_f' : ∀A,B : Type[0].∀f,g : A → B. ∀x,y : A.
358(∀w. f w = g w) → x = y → f x = g y. //
359qed.
360
361lemma add_find_all_miss :  ∀tag,A.∀m : identifier_map tag A.
362∀P : (identifier tag → A → bool).∀i,a.notb (P i a) →
363find_all tag A (add tag A m i a) P =
364match lookup tag A m i with
365[ None ⇒ find_all tag A m P
366| Some a ⇒ if P i a then find_all tag A (remove tag A m i) P else find_all tag A m P
367].
368cases daemon
369qed.
370   
371     
372lemma sigma_fb_state_insensitive_to_dead_reg:
373 ∀prog,bv. ∀st: state ERTL_semantics. ∀l:label.
374 ∀r: register. ∀before.
375  set_member … (eq_identifier RegisterTag) r (\fst  (before l)) = false →
376  sigma_fb_state prog
377   (to_be_cleared_fb before l)
378   (set_regs ERTL_semantics
379    〈reg_store r bv (\fst  (regs ERTL_semantics st)),
380    \snd  (regs ERTL_semantics st)〉 st)
381  = sigma_fb_state prog (to_be_cleared_fb before l) st.
382#prog #bv #st #l #r #before #dead whd in match sigma_fb_state; normalize nodelta
383@eq_f3 [2,3: %] whd in match set_regs; normalize nodelta whd in match sigma_fb_regs;
384normalize nodelta @eq_f2 [2: %] whd in match sigma_fb_register_env;
385normalize nodelta whd in match reg_store; normalize nodelta
386>add_find_all_miss [2: normalize >dead %] cases(lookup ????) [%] #a
387normalize nodelta whd in match to_be_cleared_fb; whd in match lives;
388normalize nodelta whd in match (plives ??); >dead %
389qed.
390
391lemma sigma_fb_state_insensitive_to_dead_Reg:
392 ∀prog,bv. ∀st: state ERTL_semantics. ∀l:label.
393 ∀r: Register. ∀before.
394  set_member … eq_Register r (\snd  (before l)) = false →
395  sigma_fb_state prog
396   (to_be_cleared_fb before l)
397   (set_regs ERTL_semantics
398     〈\fst  (regs ERTL_semantics st),
399      hwreg_store r bv (\snd  (regs ERTL_semantics st))〉
400      st)
401  = sigma_fb_state prog (to_be_cleared_fb before l) st.
402cases daemon (*TODO*)
403qed.
404
405lemma sigma_fb_state_insensitive_to_dead_carry:
406 ∀prog,bv. ∀st: state ERTL_semantics. ∀l:label. ∀before.
407  set_member Register eq_Register RegisterCarry (\snd (before l)) = false →
408   sigma_fb_state prog (to_be_cleared_fb before l) (set_carry ERTL_semantics bv st) =
409   sigma_fb_state prog (to_be_cleared_fb before l) st.
410#prog #b #st #l #cefore #dead whd in match sigma_fb_state; normalize nodelta
411whd in match set_carry; normalize nodelta whd in match to_be_cleared_fb;
412normalize nodelta whd in match (lives ??); >dead %
413qed.
414
415lemma split_orb_false: ∀a,b:bool. orb a b = false → a = false ∧ b = false.
416 ** normalize #abs destruct /2/
417qed.
418
419lemma eta_set_carry:
420 ∀P,st. set_carry P (carry P st) st = st.
421#P * //
422qed.
423
424lemma set_carry_set_regs_commute:
425 ∀P,st,c,v. set_carry P c (set_regs P v st) = set_regs P v (set_carry P c st).
426 #P * //
427qed.
428
429lemma eliminable_step_to_eq_livebefore_liveafter:
430 ∀prog,stackcost,fn.
431 let p_in ≝ mk_prog_params ERTL_semantics prog stackcost in
432 ∀st1: joint_abstract_status p_in.
433 ∀stms: joint_seq ERTL_semantics (prog_names … prog). ∀next.
434 let pt ≝ point_of_pc ERTL_semantics (pc ? st1) in
435 stmt_at p_in ? (joint_if_code p_in … fn) pt = return (sequential … stms next) →
436 ∀liveafter.
437 eliminable_step (globals … p_in) (liveafter (point_of_pc ERTL_semantics (pc … st1))) stms = true →
438  livebefore … fn liveafter pt = liveafter pt.
439 #prog #stackcost #fn #st1 #stms #next #stmt_at #liveafter #Helim
440 whd in ⊢ (??%?); whd in stmt_at:(??%?); cases (lookup ????) in stmt_at;
441 normalize nodelta try (#abs whd in abs:(??%%); destruct (abs) @I)
442 #stms' #EQ whd in EQ:(??%%); destruct (EQ) whd in ⊢ (??%?);
443 whd in match eliminable; normalize nodelta >Helim %
444qed.
445
446lemma set_subset_to_set_subst_set_union_left:
447 ∀T,eqT,A,B,C. set_subset T eqT A B → set_subset … eqT A (set_union … B C).
448 #T #eqT #A #B #C #H @set_member_subset_onlyif #x #K
449 lapply (set_member_subset_if … H) #H2 /3 by set_member_union1/
450qed.
451
452lemma set_subset_to_set_subst_set_union_right:
453 ∀T,eqT,A,B,C. set_subset T eqT A C → set_subset … eqT A (set_union … B C).
454 #T #eqT #A #B #C #H @set_member_subset_onlyif #x #K
455 lapply (set_member_subset_if … H) #H2 /3 by set_member_union2/
456qed.
457
458lemma rl_included_rl_join_left:
459 ∀A,B,C. rl_included A B → rl_included A (rl_join B C).
460 #A #B #C whd in match rl_included; normalize nodelta #H
461 cases (andb_Prop_true … H) -H #H1 #H2 @andb_Prop
462 /2 by set_subset_to_set_subst_set_union_left/
463qed.
464
465lemma rl_included_rl_join_right:
466 ∀A,B,C. rl_included A C → rl_included A (rl_join B C).
467 #A #B #C whd in match rl_included; normalize nodelta #H
468 cases (andb_Prop_true … H) -H #H1 #H2 @andb_Prop
469 /2 by set_subset_to_set_subst_set_union_right/
470qed.
471
472lemma set_subset_reflexive: ∀A,DEC,x. set_subset A DEC x x.
473 /2/
474qed.
475
476lemma rl_included_reflexive: ∀x. rl_included x x.
477 /2/
478qed.
479
480include alias "utilities/deqsets_extra.ma".
481
482lemma mem_of_fold_join:
483 ∀F,dom.
484  ∀x. x ∈ dom →
485   rl_included (F x)
486    (fold label (l_property register_lattice) rl_join rl_bottom (λl:label.true)
487      F dom).
488 #F #dom elim dom [ #x * ] #hd #tl #IH #x whd in match (? ∈ ?);
489 @eqb_elim
490 normalize nodelta #Hx #H change with (rl_join ??) in ⊢ (?(??%));
491 destruct /3 by rl_included_rl_join_left,rl_included_rl_join_right/
492qed.
493
494lemma set_subset_transitive:
495 ∀A,DEC,S1,S2,S3.
496  set_subset A DEC S1 S2 → set_subset … DEC S2 S3 → set_subset … DEC S1 S3.
497 #A #DEC #S1 #S2 #S3
498 #H1 lapply (set_member_subset_if … H1) -H1 #H1
499 #H2 lapply (set_member_subset_if … H2) -H2 #H2
500 @set_member_subset_onlyif /3 by/
501qed.
502
503lemma rl_included_transitive:
504 ∀S1,S2,S3. rl_included S1 S2 → rl_included S2 S3 → rl_included S1 S3.
505 #S1 #S2 #S3 whd in match rl_included; normalize nodelta
506 #H cases (andb_Prop_true … H) -H #H1 #H2
507 #H cases (andb_Prop_true … H) -H #H3 #H4
508 /3 by andb_Prop,set_subset_transitive/
509qed.
510
511lemma rl_included_rl_diff_rl_empty:
512 ∀S1. rl_included S1 (rl_diff S1 rl_bottom).
513 #S1 whd in match (rl_included ??);
514 lapply (set_member_subset_onlyif … (eq_identifier …) (\fst S1) (\fst (rl_diff S1 rl_bottom)))
515 cases (set_subset ????)
516 /3 by set_member_diff,set_member_subset_onlyif/
517qed.
518
519lemma included_livebefore_livebeafter_stmt_labels:
520 ∀fix_comp,globals,fn,l,stmt.
521  let after ≝ analyse_liveness fix_comp globals fn in
522   stmt_at … (joint_if_code ERTL … fn) l = Some … stmt →
523  ∀nxt.
524   nxt ∈
525    stmt_labels (mk_stmt_params (g_u_pars ERTL) label (Some label) false)
526     globals stmt →
527  l_included register_lattice (livebefore … fn after nxt) (after l).
528#fix_comp #globals #fn #l #stmt letin after ≝ (analyse_liveness ???) #EQlookup #nxt
529#Hnxt lapply (fix_correct … after l) #spec @(rl_included_transitive … spec) -spec
530whd in match (liveafter ????); whd in EQlookup:(??%?); >EQlookup -EQlookup normalize nodelta
531/2 by mem_of_fold_join/
532qed.
533
534axiom eq_sigma_state_monotonicity:
535 ∀prog,live,graph,st1,st2,l1,l2,frames.
536 st_frms ? st1 = return frames →
537  rl_included (live l2) (live l1) →
538  sigma_fb_state prog (to_be_cleared_fb live l1) st1 =
539   sigma_sb_state (get_ertl_call_stack frames) prog
540    (to_be_cleared_sb live graph l1) st2 →
541  sigma_fb_state prog (to_be_cleared_fb live l2) st1 =
542   sigma_sb_state (get_ertl_call_stack frames) prog
543    (to_be_cleared_sb live graph l2) st2.
544
545
546
547lemma fetch_ok_sigma_state_ok : ∀fix_comp,colour,prog,init_regs,f_lbls,f_regs.
548let m ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in
549let stacksizes ≝ lookup_stack_cost … m in
550∀st1,st2,f,fn. state_pc_rel fix_comp colour prog init_regs f_lbls f_regs st1 st2 →
551fetch_internal_function …
552(joint_globalenv ERTL_semantics prog stacksizes) (pc_block (pc … st1)) 
553     = return 〈f,fn〉 →
554let after ≝ (analyse_liveness fix_comp (prog_names … prog) fn) in
555let before ≝ livebefore … fn after in
556let coloured_graph ≝ colour … fn after in
557match st_frms … (st_no_pc … st1) with
558[ None ⇒ False
559| Some frames ⇒
560 (sigma_fb_state prog
561  (to_be_cleared_fb before (point_of_pc ERTL_semantics (pc … st1)))
562  (st_no_pc … st1)) =
563 (sigma_sb_state (get_ertl_call_stack frames) prog
564   (to_be_cleared_sb … coloured_graph (point_of_pc ERTL_semantics (pc … st1)))
565  (st_no_pc … st2))
566].
567#fix_comp #colour #prog #init_regs #f_lbls #f_regs #st1 #st2 #f #fn
568#H #EQfn whd in match state_pc_rel in H; normalize nodelta in H;
569inversion (st_frms … st1) in H; [ #_ *] #frames #EQframes normalize nodelta
570whd in match sigma_fb_state_pc; whd in match sigma_sb_state_pc;
571normalize nodelta >EQfn normalize nodelta inversion(fetch_internal_function ????)
572[2: #e #_ normalize nodelta whd in match dummy_state_pc; whd in match null_pc;
573    normalize nodelta #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
574    >fetch_internal_function_no_zero in EQfn; [2: >e1 %] whd in ⊢ (???% → ?);
575    #ABS destruct(ABS) ]
576* #f1 #fn1 #EQfn1 normalize nodelta #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ
577destruct(EQ) <e1 in EQfn1; >EQfn whd in ⊢ (??%?? → ?); #EQ1 destruct(EQ1)
578whd in match sigma_fb_state; normalize nodelta >e0 >e1 %
579qed.
580     
581lemma fetch_ok_pc_ok : ∀fix_comp,colour,prog,init_regs,f_lbls,f_regs.
582let m ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in
583let stacksizes ≝ lookup_stack_cost … m in
584∀st1,st2,f,fn. state_pc_rel fix_comp colour prog init_regs f_lbls f_regs st1 st2 →
585fetch_internal_function …
586(joint_globalenv ERTL_semantics prog stacksizes) (pc_block (pc … st1)) 
587     = return 〈f,fn〉 → (pc … st1) = (pc … st2).
588#fix_comp #colour #prog #init_regs #f_lbls #f_regs #st1 #st2 #f #fn
589#H #EQfn whd in match state_pc_rel in H; normalize nodelta in H;
590inversion (st_frms … st1) in H; [ #_ *] #frames #EQframes normalize nodelta
591whd in match sigma_fb_state_pc; whd in match sigma_sb_state_pc;
592normalize nodelta >EQfn normalize nodelta inversion(fetch_internal_function ????)
593[2: #e #_ normalize nodelta whd in match dummy_state_pc; whd in match null_pc;
594    normalize nodelta #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
595    >fetch_internal_function_no_zero in EQfn; [2: >e1 %] whd in ⊢ (???% → ?);
596    #ABS destruct(ABS) ]
597* #f1 #fn1 #EQfn1 normalize nodelta #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ
598destruct(EQ) <e1 in EQfn1; >EQfn whd in ⊢ (??%?? → ?); #EQ1 destruct(EQ1) %
599qed.
600
601axiom colouring_reg_non_DPL_DPH : ∀fix_comp,colour,prog.
602let m ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in
603let stacksizes ≝ lookup_stack_cost … m in
604∀bl,f,fn,R.∀r : register.
605fetch_internal_function …
606(joint_globalenv ERTL_semantics prog stacksizes) bl = return 〈f,fn〉 →
607let after ≝ (analyse_liveness fix_comp (prog_names … prog) fn) in
608let before ≝ livebefore … fn after in
609colouring before (colour … fn after) (inl register Register r) =
610decision_colour R → R ≠ RegisterDPL ∧ R ≠ RegisterDPH ∧
611R ≠ RegisterA.
612
613axiom insensitive_to_be_cleared_sb_regs :
614∀prog.∀tb : local_clear_sb_type. ∀st : state LTL_LIN_state.
615∀bv.∀r : Register.∀cs.∀rgs. tb r →
616sigma_sb_state cs prog tb (set_regs LTL_semantics rgs st) =
617sigma_sb_state cs prog tb (set_regs LTL_semantics
618          (hwreg_store r bv rgs) st).
619
620axiom insensitive_sb_to_hwreg_set_other :
621∀prog.∀tb : local_clear_sb_type. ∀st : state LTL_LIN_state.
622∀b,cs,rgs.
623sigma_sb_state cs prog tb
624 (set_regs LTL_semantics (hwreg_set_other b rgs) st) =
625sigma_sb_state cs prog tb (set_regs LTL_semantics rgs st).
626
627axiom insensitive_to_be_cleared_carry :
628∀prog.∀tb : local_clear_sb_type. ∀st : state LTL_LIN_state.
629∀b.∀cs. tb RegisterCarry →
630sigma_sb_state cs prog tb (set_carry LTL_semantics b st) =
631sigma_sb_state cs prog tb st.
632
633axiom dpl_is_dead : ∀fix_comp.∀prog : ertl_program.
634 ∀fn : joint_closed_internal_function ERTL (prog_names … prog). ∀l.
635 let after ≝ analyse_liveness fix_comp (prog_names … prog) fn in
636  ¬ lives (inr ? ? RegisterDPL) (livebefore  … fn after l).
637
638axiom dph_is_dead : ∀fix_comp.∀prog : ertl_program.
639 ∀fn : joint_closed_internal_function ERTL (prog_names … prog). ∀l.
640 let after ≝ analyse_liveness fix_comp (prog_names … prog) fn in
641  ¬ lives (inr ? ? RegisterDPH) (livebefore  … fn after l).
642
643lemma m_return_if_commute :  ∀M : Monad.∀A : Type[0]. ∀a1,a2 : A.∀b : bool.
644if b then m_return M A a1 else m_return M A a2 =
645m_return M A (if b then a1 else a2).
646#M #A #a1 #a2 * %
647qed.
648
649lemma set_carry_eta :∀p.∀st : state p.set_carry p (carry … st) st = st.
650#p * //
651qed.
652
653lemma set_regs_eta :∀p.∀st : state p. set_regs p (regs … st) st = st.
654#p * //
655qed.
656
657lemma carry_sensitive_read_arg_decision :
658∀prog.∀tb : local_clear_sb_type. ∀st,st' : state LTL_LIN_state.∀d,cs,bv,localss.
659read_arg_decision localss st d = return 〈bv,st'〉 →
660tb RegisterDPL → tb RegisterDPH → 
661sigma_sb_state cs prog tb (set_carry … (carry … st') st) =
662sigma_sb_state cs prog tb st'.
663#prog #tb #st #st' * [#R | #n | #b ] #cs #bv #localss whd in match read_arg_decision;
664normalize nodelta [1,3: whd in ⊢ (??%% → ?); #EQ destruct(EQ) #_ #_ >set_carry_eta %]
665>m_return_bind >m_return_bind #H @('bind_inversion H) -H * #bv1 #b1 #_
666#H @('bind_inversion H) -H * #bv2 #b2 #_ #H @('bind_inversion H) -H #ptr #_ #H
667@('bind_inversion H) -H #bv3 #_ whd in ⊢ (??%% → ?); #EQ destruct(EQ) #H1 #H2
668whd in match set_carry; normalize nodelta
669change with (set_regs ?? (set_carry ? b2 st)) in ⊢ (???(????%));
670<insensitive_to_be_cleared_sb_regs [2: assumption] <insensitive_to_be_cleared_sb_regs
671[2: assumption] whd in match set_regs; whd in match set_carry; normalize nodelta %
672qed.
673
674axiom set_carry_sigma_sb_state_commute :
675∀prog,cs.∀st,st' : state LTL_LIN_state. ∀tb : local_clear_sb_type.
676sigma_sb_state cs prog tb (set_carry  … (carry … st') st) =
677set_carry … (carry … (sigma_sb_state cs prog tb st'))
678 (sigma_sb_state cs prog tb st).
679
680lemma cond_commute :∀fix_comp,colour,prog,init_regs,f_lbls,f_regs.
681let p_out ≝ (\fst (\fst (ertl_to_ltl fix_comp colour prog))) in
682let m ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in
683let n ≝ \snd (ertl_to_ltl fix_comp colour prog) in
684let stacksizes ≝ lookup_stack_cost … m in
685let init ≝ (λglobals,fn.«translate_data fix_comp colour globals fn,?») in
686cond_commutation_statement ERTL_semantics LTL_semantics prog stacksizes
687 init init_regs
688 f_lbls f_regs (state_rel fix_comp colour prog)
689 (state_pc_rel fix_comp colour prog init_regs f_lbls f_regs).
690[2: @hide_prf %]
691#fix_comp #colour #prog #init_regs #f_lbls #f_regs
692whd in match cond_commutation_statement; normalize nodelta
693#st1 #st2 #f #fn #r #ltrue #lfalse #bv #b * #Hbl #EQfetch
694whd in match acca_retrieve; normalize nodelta change with (ps_reg_retrieve ??) in ⊢ (??%? → ?);
695#EQbv #EQb #Rst1st2 #t_fn #EQt_fn whd normalize nodelta %{(refl …)} #mid #EQmid
696cases(ps_reg_retrieve_hw_reg_retrieve_commute fix_comp colour prog init_regs f_lbls
697f_regs fn (pc … st1) … (colouring … (inl ?? r)) … EQbv)
698[6: %
699|2: @(st_no_pc … st2)
700|5: whd %{f} %{fn} >(proj1 … (fetch_statement_inv … EQfetch)) %{(refl …)}
701    @(fetch_ok_sigma_state_ok … Rst1st2 …
702         (proj1 ?? (fetch_statement_inv … EQfetch)))
703|*:
704]
705#bv1 * inversion(colouring … (inl ?? r))
706[ #n #EQcolouring
707| #R #EQcolouring
708  cases(colouring_reg_non_DPL_DPH …
709                      (proj1 ?? (fetch_statement_inv … EQfetch)) … EQcolouring)
710  * #RnoDPL #RnoDPH #RnoA
711]
712whd in match m_map; normalize nodelta #H @('bind_inversion H) -H *
713#bv2 #st' #EQbv2 whd in ⊢ (??%% → ?); #EQ1 #EQ2 destruct(EQ1 EQ2)
714% [2,4: %
715     [1,3: >map_eval_add_dummy_variance_id in ⊢ (??%?); >move_spec in ⊢ (??%?);
716       [2: @I | 4:  %{RnoDPL RnoDPH}] normalize nodelta
717       [ >EQbv2 in ⊢ (??%?); | >EQbv2 in ⊢ (??%?); ] >m_return_bind
718       whd in match write_decision; normalize nodelta >m_return_bind
719       >m_return_if_commute in ⊢ (??%?); %
720     |*: %
721       [1,3: whd %{f} %{fn} %
722           [1,3,5,7: @if_elim #_ >(proj1 … (fetch_statement_inv … EQfetch)) %]
723           normalize nodelta
724           lapply(fetch_ok_sigma_state_ok … Rst1st2 …
725                                    (proj1 ?? (fetch_statement_inv … EQfetch)))
726           normalize nodelta inversion (st_frms … (st_no_pc … st1)) [1,3: #_ * ]
727           #frames #EQframes normalize nodelta #R_nopc_st1st2
728           [ inversion(hlives RegisterCarry
729              (analyse_liveness fix_comp
730               (prog_names ERTL_semantics prog) fn
731               (point_of_pc ERTL_semantics (pc … st1))))
732             [ #carry_live | #carry_dead ]
733           | @eq_Register_elim [ #EQ destruct(EQ) @⊥ cases RnoA #H @H %] #_
734           ]
735           normalize nodelta
736           [ >insensitive_sb_to_hwreg_set_other
737             whd in match set_regs in ⊢ (???(????(??%?))); normalize nodelta ]
738           <insensitive_to_be_cleared_sb_regs
739           [2,4,6: @dead_registers_in_dead @acc_is_dead ]
740           [ whd in match set_regs; whd in match set_carry; normalize nodelta
741             change with (set_carry ? (carry … (st_no_pc … st2)) st') in ⊢ (???(????%));
742             >set_carry_sigma_sb_state_commute
743           |*: >set_regs_eta
744           ]
745           <(carry_sensitive_read_arg_decision … EQbv2)
746           [2,3,5,6,8,9: @dead_registers_in_dead [1,3,5: @dph_is_dead |*: @dpl_is_dead]]
747           [ >set_carry_sigma_sb_state_commute
748             change with (set_carry ?? (sigma_sb_state ? prog ? (st_no_pc … st2)))
749                                                                            in ⊢ (???%);
750             >set_carry_eta
751           | >insensitive_to_be_cleared_carry
752             [2: @dead_registers_in_dead cases daemon (*????*) ]
753           | whd in EQbv2 : (??%%); destruct(EQbv2) >set_carry_eta
754           ]
755           @(eq_sigma_state_monotonicity … EQframes … R_nopc_st1st2)
756           cases b normalize nodelta >point_of_pc_of_point
757           letin after ≝ (analyse_liveness fix_comp … fn)
758           letin before ≝ (livebefore … fn after)
759           lapply (included_livebefore_livebeafter_stmt_labels
760                      fix_comp … (proj2 ?? (fetch_statement_inv … EQfetch)))
761           normalize in match (stmt_labels ???);
762           change with after in match after;
763           #H [2,4,6: lapply (H lfalse ?) [1,3,5: >memb_hd % ]
764              |*: lapply (H ltrue ?) [1,3,5: >memb_cons try % >memb_hd %]]
765           #K change with (bool_to_Prop (rl_included ??)) in K;
766           @(rl_included_transitive … K) whd in match (livebefore ????);
767           cases(fetch_statement_inv … EQfetch) #_ normalize nodelta
768           whd in ⊢ (??%? → ?); #EQstmt >EQstmt normalize nodelta
769           @rl_included_rl_join_left normalize in match (defined ??);
770           @rl_included_rl_diff_rl_empty
771       |*: %{it} %{(refl …)} %{bv1} %
772           [1,3: [ @if_elim #_
773                 | @eq_Register_elim [ #EQ destruct(EQ) @⊥ cases RnoA #H @H %] #_
774                 ]
775                 normalize nodelta change with (hw_reg_retrieve ??) in ⊢ (??%?);
776                 whd in match hw_reg_retrieve; normalize nodelta @eq_f
777                 whd in match set_regs; normalize nodelta
778                 [ >hwreg_retrieve_insensitive_to_set_other]
779                 >hwreg_retrieve_hwregstore_hit %
780           |*: cases(bool_of_beval_sigma_commute fix_comp colour prog init_regs
781                      f_lbls f_regs … bv1 … EQb) [2,4: %] #b1 * #EQb1 #EQ destruct(EQ)
782                      assumption
783           ]
784       ]
785    ]     
786  |*:
787  ]
788qed.
789           
790lemma seq_commute :∀fix_comp,colour,prog,init_regs,f_lbls,f_regs.
791let p_out ≝ (\fst (\fst (ertl_to_ltl fix_comp colour prog))) in
792let m ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in
793let n ≝ \snd (ertl_to_ltl fix_comp colour prog) in
794let stacksizes ≝ lookup_stack_cost … m in
795let init ≝ (λglobals,fn.«translate_data fix_comp colour globals fn,?») in
796seq_commutation_statement ERTL_semantics LTL_semantics prog stacksizes
797 init init_regs
798 f_lbls f_regs (state_rel fix_comp colour prog)
799 (state_pc_rel fix_comp colour prog init_regs f_lbls f_regs).
800[2: @hide_prf %]
801cases daemon (*TODO*)
802qed.
803
804lemma return_commute :∀fix_comp,colour,prog,init_regs,f_lbls,f_regs.
805let p_out ≝ (\fst (\fst (ertl_to_ltl fix_comp colour prog))) in
806let m ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in
807let n ≝ \snd (ertl_to_ltl fix_comp colour prog) in
808let stacksizes ≝ lookup_stack_cost … m in
809let init ≝ (λglobals,fn.«translate_data fix_comp colour globals fn,?») in
810return_commutation_statement ERTL_semantics LTL_semantics prog stacksizes
811 init init_regs
812 f_lbls f_regs (state_rel fix_comp colour prog)
813 (state_pc_rel fix_comp colour prog init_regs f_lbls f_regs).
814[2: @hide_prf %]
815cases daemon (*TODO*)
816qed.
817
818lemma pre_main_commute : ∀fix_comp,colour,prog,init_regs,f_lbls,f_regs.
819let p_out ≝ (\fst (\fst (ertl_to_ltl fix_comp colour prog))) in
820let m ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in
821let n ≝ \snd (ertl_to_ltl fix_comp colour prog) in
822let stacksizes ≝ lookup_stack_cost … m in
823let init ≝ (λglobals,fn.«translate_data fix_comp colour globals fn,?») in
824b_graph_transform_program_props ERTL_semantics LTL_semantics stacksizes
825  init prog init_regs f_lbls f_regs →
826pre_main_commutation_statement  ERTL_semantics LTL_semantics prog stacksizes
827 init init_regs
828 f_lbls f_regs (state_rel fix_comp colour prog)
829 (state_pc_rel fix_comp colour prog init_regs f_lbls f_regs).
830[2: @hide_prf %]
831cases daemon qed.
832
833(*
834#fix_comp #colour #prog #init_regs #f_lbls #f_regs #good whd
835#st1 #st1' #st2 #EQbl whd in match eval_state; normalize nodelta
836whd in match fetch_statement; whd in match fetch_internal_function; normalize nodelta
837whd in match fetch_function; normalize nodelta @eqZb_elim [2: * #H @⊥ @H assumption]
838#_ normalize nodelta >m_return_bind #H @('bind_inversion H) -H ** #f #fn #stmt
839#H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H #stmt1
840#H lapply(opt_eq_from_res ???? H) -H whd in ⊢ (??%% → ?); cases st1 in EQbl; -st1
841#st1 * #bl1 #pos1 #lp1 #EQbl1 normalize nodelta cases pos1 -pos1 normalize nodelta
842[ #EQ destruct(EQ)
843|*: * [2,3,5,6: #x ] whd in ⊢ (??%% → ?); #EQ destruct
844]
845whd in ⊢ (??%% → ?); #EQ destruct(EQ) normalize nodelta whd in match eval_statement_no_pc; normalize inversion(point_of_pc ERTL_semantics (pc … st1))
846*)
847
848lemma call_commute : ∀fix_comp,colour,prog,init_regs,f_lbls,f_regs.
849let p_out ≝ (\fst (\fst (ertl_to_ltl fix_comp colour prog))) in
850let m ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in
851let n ≝ \snd (ertl_to_ltl fix_comp colour prog) in
852let stacksizes ≝ lookup_stack_cost … m in
853let init ≝ (λglobals,fn.«translate_data fix_comp colour globals fn,?») in
854call_commutation_statement ERTL_semantics LTL_semantics prog stacksizes
855 init init_regs
856 f_lbls f_regs (state_rel fix_comp colour prog)
857 (state_pc_rel fix_comp colour prog init_regs f_lbls f_regs).
858[2: @hide_prf %]
859cases daemon qed.
860
861lemma goto_commute : ∀fix_comp,colour,prog,init_regs,f_lbls,f_regs.
862let p_out ≝ (\fst (\fst (ertl_to_ltl fix_comp colour prog))) in
863let m ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in
864let n ≝ \snd (ertl_to_ltl fix_comp colour prog) in
865let stacksizes ≝ lookup_stack_cost … m in
866let init ≝ (λglobals,fn.«translate_data fix_comp colour globals fn,?») in
867goto_commutation_statement ERTL_semantics LTL_semantics prog stacksizes
868 init init_regs
869 f_lbls f_regs (state_rel fix_comp colour prog)
870 (state_pc_rel fix_comp colour prog init_regs f_lbls f_regs).
871[2: @hide_prf %]
872cases daemon qed.
873
874lemma tailcall_commute : ∀fix_comp,colour,prog,init_regs,f_lbls,f_regs.
875let p_out ≝ (\fst (\fst (ertl_to_ltl fix_comp colour prog))) in
876let m ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in
877let n ≝ \snd (ertl_to_ltl fix_comp colour prog) in
878let stacksizes ≝ lookup_stack_cost … m in
879let init ≝ (λglobals,fn.«translate_data fix_comp colour globals fn,?») in
880tailcall_commutation_statement ERTL_semantics LTL_semantics prog stacksizes
881 init init_regs
882 f_lbls f_regs (state_rel fix_comp colour prog)
883 (state_pc_rel fix_comp colour prog init_regs f_lbls f_regs).
884[2: @hide_prf %]
885#fix_comp #colour #prog #init_regs #f_lbls #f_regs whd #st1 #st2
886#f #fn *
887qed.
888
889             
890theorem ERTLToLTL_ok :
891∀fix_comp : fixpoint_computer.
892∀colour : coloured_graph_computer.
893∀p_in : ertl_program.
894let 〈p_out, m, n〉 ≝ ertl_to_ltl fix_comp colour p_in in
895(* what should we do with n? *)
896let stacksizes ≝ lookup_stack_cost m in
897∀init_in.make_initial_state
898  (mk_prog_params ERTL_semantics p_in stacksizes) = OK … init_in →
899∃init_out.
900  make_initial_state
901   (mk_prog_params LTL_semantics p_out stacksizes) =
902    OK ? init_out ∧
903∃[1] R.
904  status_simulation_with_init
905    (joint_status ERTL_semantics p_in stacksizes)
906    (joint_status LTL_semantics p_out stacksizes)
907    R init_in init_out.
908#fix_comp #colour #p_in #init_in #EQinit_in
909letin p_out ≝ (\fst (\fst (ertl_to_ltl fix_comp colour p_in)))
910letin m ≝ (\snd (\fst (ertl_to_ltl fix_comp colour p_in)))
911letin n ≝ (\snd (ertl_to_ltl fix_comp colour p_in))
912letin stacksizes ≝ (lookup_stack_cost m)
913cases(make_b_graph_transform_program_props ERTL_semantics LTL_semantics stacksizes
914     (λglobals : list ident.λfn.«translate_data fix_comp colour globals fn,(refl …)») p_in)
915#init_regs * #f_lbls * #f_regs #good
916@(joint_correctness ERTL_semantics LTL_semantics p_in stacksizes
917(λglobals : list ident.λfn.«translate_data fix_comp colour globals fn,(refl …)»)
918init_regs f_lbls f_regs (state_rel fix_comp colour p_in)
919(state_pc_rel fix_comp colour p_in init_regs f_lbls f_regs) ? ? init_in EQinit_in)
920%
921[ @good
922| #st1 #st2 #f #fn #Rst1st2 #EQfn whd %{f} %{fn} %{EQfn}
923  @(fetch_ok_sigma_state_ok fix_comp colour p_in … Rst1st2 EQfn)
924| #st1 #st2 #f #fn #Rst1st2 #EQfn @(fetch_ok_pc_ok fix_comp colour p_in … Rst1st2 EQfn)
925| #st1 #st2 #f #fn #Rst1st2 #EQfn lapply Rst1st2 whd in match state_pc_rel;
926  normalize nodelta cases(st_frms … st1) [*] #frames normalize nodelta
927  whd in match sigma_fb_state_pc; whd in match sigma_sb_state_pc; normalize nodelta
928  >EQfn normalize nodelta <(fetch_ok_pc_ok … Rst1st2 EQfn) >EQfn normalize nodelta
929  #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) assumption
930| #st1 #st2 #pc #lp1 #lp2 #f #fn #EQfn #Rst1st2 #EQ destruct(EQ) whd
931  lapply Rst1st2 whd in match state_rel; normalize nodelta * #f1 * #fn1 >EQfn *
932  whd in ⊢ (??%% → ?); #EQ destruct(EQ) cases(st_frms … st1) [*] #frames
933  normalize nodelta #EQst whd in match sigma_fb_state_pc;
934  whd in match sigma_sb_state_pc; normalize nodelta >EQfn
935  normalize nodelta @eq_f3 [2,3: % | assumption]
936| @pre_main_commute assumption
937| #f #fn * #bl #pos #EQbl whd in match fetch_statement;
938  whd in match fetch_internal_function; whd in match fetch_function;
939  normalize nodelta @eqZb_elim [2: * #H @⊥ @H assumption]
940  #_ normalize nodelta >m_return_bind #H @('bind_inversion H) -H #stmt 
941  #H lapply(opt_eq_from_res ???? H) -H whd in ⊢ (??%% → ?);
942  whd in match point_of_pc; normalize nodelta cases pos normalize nodelta
943  [ #EQ destruct(EQ)
944  |*: * [2,3,5,6: #x ] whd in ⊢ (??%% → ?); #EQ destruct
945  ]
946  whd in ⊢ (??%% → ?); #EQ destruct(EQ)
947| @cond_commute
948| @seq_commute
949| #f #fn #bl #EQfn #id #args #dest #lbl whd #bl'
950  %{(match id with [inl f1 ⇒ inl ?? f1 | inr x ⇒ inr ?? 〈it,it〉])}
951  %{args} %{it} normalize nodelta cases id [ #f1 % | * #dpl #dph %]
952| cases daemon (*TODO*)
953| @return_commute
954| @call_commute
955| @goto_commute
956| @tailcall_commute
957| cases daemon (*TODO*)
958| cases daemon (*TODO*)
959| cases daemon (*TODO*)
960| cases daemon (*TODO*)
961]
962qed.
Note: See TracBrowser for help on using the repository browser.