source: src/ERTL/ERTLToLTLProof.ma

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

partial commit

File size: 138.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,d.bool_to_Prop (live_fun (inl ?? r)) ∧ 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 16 (localss + n))))
37        ]).
38
39
40definition hw_relation : ℕ → local_live_type → (vertex → decision)
41→ (beval → beval → Prop) → hw_register_env → hw_register_env →  bemem → Prop ≝
42λlocalss,live_fun,color_fun,R,hw1,hw2,mem.
43hwreg_retrieve_sp hw1 = hwreg_retrieve_sp hw2 ∧
44∀r : Register.r ≠ RegisterCarry → live_fun (inr ?? r) → hwreg_retrieve hw1 r ≠ BVundef →
45match color_fun (inr ?? r) with
46[ decision_colour r' ⇒ R (hwreg_retrieve hw1 r) (hwreg_retrieve hw2 r')
47| decision_spill n ⇒
48  match hwreg_retrieve_sp hw2 with
49  [ OK sp ⇒ match beloadv mem (shift_pointer ? sp (bitvector_of_nat 16 (localss + n))) with
50     [ Some bv ⇒ R (hwreg_retrieve hw1 r) bv
51     | None ⇒ False
52     ]
53  | Error e ⇒ False
54  ]
55].   
56
57include alias "arithmetics/nat.ma".
58include alias "basics/logic.ma".
59
60definition mem_relation : ertl_program → (ident → option ℕ) →
61(beval → beval → Prop) → ident → state ERTL_state → bemem → bemem → Prop ≝
62λprog,stacksizes,R,f,st,m2,m3.
63let ge ≝ joint_globalenv ERTL_semantics prog stacksizes in
64gen_preserving ?? gen_opt_preserve ????
65     (λptr1,ptr2.ERTL_validate_pointer … ge f st ptr1 = return it ∧ ptr1 = ptr2) R
66     (beloadv m2) (beloadv m3).
67
68(*
69definition callee_saved_remap :
70(Σb:block.block_region b=Code) → (block → list register) →
71((Σb:block.block_region b=Code) → option (list register → vertex → decision)) →
72decision → decision ≝
73λbl,init_regs,colouring,d.
74match d with
75[ decision_spill n ⇒ decision_spill n
76| decision_colour R ⇒
77  match position_of ? (eq_Register R) RegisterCalleeSaved with
78  [ Some n ⇒
79    match nth_opt ? n (init_regs bl) with
80    [Some r ⇒
81        match colouring bl with
82        [ Some color_fun ⇒ color_fun (init_regs bl) (inl ?? r)
83        | None ⇒ d
84        ]
85    | None ⇒ d
86    ]
87  | None ⇒ d
88  ]
89].
90*)
91
92(*
93definition mem_relation : fixpoint_computer → coloured_graph_computer →
94ertl_program → (beval → beval → Prop) → ident →  state ERTL_state →  bemem → bemem → Prop ≝
95λfix_comp,build,prog,R,f,st,m2,m3.
96let m1 ≝ (\snd (\fst (ertl_to_ltl fix_comp build prog))) in
97let stacksizes ≝ lookup_stack_cost … m1 in 
98let ge ≝ joint_globalenv ERTL_semantics prog stacksizes in
99gen_preserving ?? gen_opt_preserve ????
100     (λptr1,ptr2.ERTL_validate_pointer … ge f st ptr1 = return it ∧ ptr1 = ptr2) R
101     (beloadv m2) (beloadv m3).
102*)
103
104definition callee_saved_remap : fixpoint_computer → coloured_graph_computer →
105ertl_program → (Σb:block.block_region b=Code) → (block → list register) → decision → decision ≝
106λfix_comp,build,prog,bl,init_regs,d.
107match d with
108[ decision_spill n ⇒ decision_spill n
109| decision_colour R ⇒
110  match position_of ? (eq_Register R) RegisterCalleeSaved with
111  [ Some n ⇒
112    match nth_opt ? n (init_regs bl) with
113    [Some r ⇒
114        let m1 ≝ (\snd (\fst (ertl_to_ltl fix_comp build prog))) in
115        let stacksizes ≝ lookup_stack_cost … m1 in   
116        let ge ≝ joint_globalenv ERTL_semantics prog stacksizes in
117        match fetch_internal_function … ge bl with
118        [ OK y ⇒
119             let after ≝ (analyse_liveness fix_comp (prog_names … prog)
120                          (\snd y) (init_regs bl)) in
121             (colouring … (build (prog_names … prog) (\snd y) after (init_regs bl))
122               (inl register Register r))
123        | Error e ⇒ d
124        ]
125    | None ⇒ d
126    ]
127  | None ⇒ d
128  ]
129].
130
131(*
132let rec frames_relation_aux (prog : ertl_program) (stacksize : ident → option ℕ)
133(color_f : (Σb:block.block_region b=Code) →  option (list register → vertex → decision))
134(live_f : (Σb:block.block_region b=Code) → option (list register → label → vertex → bool))
135(R : beval → beval → Prop) (frames : list ERTL_frame) (regs : hw_register_env)
136(m : bemem) (acc : decision → decision) (init_regs : block → list register) on frames : Prop ≝
137match frames with
138[ nil ⇒ True
139| cons hd tl ⇒
140  let ge ≝ joint_globalenv ERTL_semantics prog stacksize in 
141  ∃f,fn,color_fun,live_fun.
142   fetch_internal_function … ge (pc_block (funct_pc hd)) = return 〈f,fn〉 ∧
143   color_f (pc_block (funct_pc hd)) = Some ? color_fun ∧
144   live_f (pc_block (funct_pc hd)) = Some ? live_fun ∧
145   (gen_preserving … gen_res_preserve …
146      (λr,d.
147       bool_to_Prop
148        (live_fun (init_regs (pc_block (funct_pc hd)))
149          (point_of_pc ERTL_semantics (funct_pc hd)) (inl ?? r))  ∧
150       d = acc (color_fun (init_regs (pc_block (funct_pc hd)))
151                  (inl register Register r)))
152      R (reg_retrieve (psd_reg_env hd))
153      (λd.match d with
154          [ decision_spill n ⇒
155              opt_to_res ? [MSG FailedLoad]
156               (beloadv m
157                (shift_pointer ? (funct_sp hd)
158                 (bitvector_of_nat 16 ((joint_if_local_stacksize … fn)  + n))))
159          | decision_colour R ⇒ return hwreg_retrieve regs R
160          ]))
161    ∧ frames_relation_aux prog stacksize color_f live_f R tl regs m
162      (λd.acc (callee_saved_remap (pc_block (funct_pc hd)) init_regs color_f d))
163      init_regs
164].*)
165
166let rec frames_relation_aux (fix_comp : fixpoint_computer)
167(build : coloured_graph_computer) (prog : ertl_program) (R : beval → beval → Prop)
168(frames : list ERTL_frame) (regs : hw_register_env) (m : bemem)
169(acc : decision → decision) (init_regs : block → list register) on frames : Prop ≝
170match frames with
171[ nil ⇒ True
172| cons hd tl ⇒
173  let m1 ≝ (\snd (\fst (ertl_to_ltl fix_comp build prog))) in
174  let stacksizes ≝ lookup_stack_cost … m1 in   
175  let ge ≝ joint_globalenv ERTL_semantics prog stacksizes in 
176  ∃f,fn.
177   fetch_internal_function … ge (pc_block (funct_pc hd)) = return 〈f,fn〉 ∧
178   let after ≝ (analyse_liveness fix_comp (prog_names … prog) fn
179                (init_regs (pc_block (funct_pc hd)))) in
180   let before ≝ livebefore … fn (init_regs (pc_block (funct_pc hd))) after in
181   let colour ≝ (colouring … (build (prog_names … prog) fn after
182                   (init_regs (pc_block (funct_pc hd))))) in
183   (gen_preserving … gen_res_preserve …
184      (λr,d.
185       bool_to_Prop (in_lattice (inl ?? r)
186               (before (point_of_pc ERTL_semantics (funct_pc hd)))) ∧
187       d = acc (colour (inl register Register r)))
188      R (reg_retrieve (psd_reg_env hd))
189      (λd.match d with
190          [ decision_spill n ⇒
191              opt_to_res ? [MSG FailedLoad]
192               (beloadv m
193                (shift_pointer ? (funct_sp hd)
194                 (bitvector_of_nat 8 ((joint_if_local_stacksize … fn)  + n))))
195          | decision_colour R ⇒ return hwreg_retrieve regs R
196          ]))
197   ∧ frames_relation_aux fix_comp build prog R tl regs m
198      (λd.acc (callee_saved_remap fix_comp build prog (pc_block (funct_pc hd)) init_regs d))
199      init_regs
200].
201
202definition frames_relation :
203(*
204∀prog : ertl_program.(ident → option ℕ) → (beval → beval → Prop) →
205((Σb:block.block_region b=Code) →  option(list register → vertex → decision)) →
206((Σb:block.block_region b=Code) → option(list register → live_type)) → list ERTL_frame →
207hw_register_env → bemem → (block → list register) → Prop ≝
208λprog,stacksize,R,color_fun,live_fun,frames,regs,m,init_regs.
209frames_relation_aux prog stacksize color_fun live_fun R frames regs m (λx.x) init_regs.
210*)
211fixpoint_computer → coloured_graph_computer → 
212ertl_program → (beval → beval → Prop) → list ERTL_frame →
213hw_register_env → bemem → (block → list register) → Prop ≝
214λfix_comp,build,prog,R,frames,regs,m,init_regs.
215 frames_relation_aux fix_comp build prog R frames regs m (λx.x) init_regs.
216
217(*
218definition register_of_bitvector :  BitVector 6 → option Register≝
219λvect.
220let n ≝ nat_of_bitvector … vect in
221if eqb n 0 then Some ? Register00
222else if eqb n 1 then Some ? Register01
223else if eqb n 2 then Some ? Register02
224else if eqb n 3 then Some ? Register03
225else if eqb n 4 then Some ? Register04
226else if eqb n 5 then Some ? Register05
227else if eqb n 6 then Some ? Register06
228else if eqb n 7 then Some ? Register07
229else if eqb n 8 then Some ? Register10
230else if eqb n 9 then Some ? Register11
231else if eqb n 10 then Some ? Register12
232else if eqb n 11 then Some ? Register13
233else if eqb n 12 then Some ? Register14
234else if eqb n 13 then Some ? Register15
235else if eqb n 14 then Some ? Register16
236else if eqb n 15 then Some ? Register17
237else if eqb n 16 then Some ? Register20
238else if eqb n 17 then Some ? Register21
239else if eqb n 18 then Some ? Register22
240else if eqb n 19 then Some ? Register23
241else if eqb n 20 then Some ? Register24
242else if eqb n 21 then Some ? Register25
243else if eqb n 22 then Some ? Register26
244else if eqb n 23 then Some ? Register27
245else if eqb n 24 then Some ? Register30
246else if eqb n 25 then Some ? Register31
247else if eqb n 26 then Some ? Register32
248else if eqb n 27 then Some ? Register33
249else if eqb n 28 then Some ? Register34
250else if eqb n 29 then Some ? Register35
251else if eqb n 30 then Some ? Register36
252else if eqb n 31 then Some ? Register37
253else if eqb n 32 then Some ? RegisterA
254else if eqb n 33 then Some ? RegisterB
255else if eqb n 34 then Some ? RegisterDPL
256else if eqb n 35 then Some ? RegisterDPH
257else if eqb n 36 then Some ? RegisterCarry (* was -1, increment as needed *)
258else None ?.
259*)
260
261(*set_theoretical axioms *)
262axiom set_member_empty :∀A.∀DEC.∀a.¬set_member A DEC a (set_empty …).   
263axiom set_member_singl : ∀A,DEC,a.set_member A DEC a (set_singleton … a).
264axiom set_member_union1 : ∀A,DEC,x,y,a.set_member A DEC a x →
265set_member A DEC a (set_union … x y).
266axiom set_member_union2 : ∀A,DEC,x,y,a.set_member A DEC a y →
267set_member A DEC a (set_union … x y).
268axiom set_member_diff : ∀A,DEC,x,y,a.set_member A DEC a x →
269¬set_member A DEC a y →
270set_member A DEC a (set_diff … x y).
271axiom set_member_subset_if:
272 ∀A,DEC,S1,S2.
273  set_subset A DEC S1 S2 →
274   ∀x. set_member A DEC x S1 → set_member A DEC x S2.
275axiom set_member_subset_onlyif:
276 ∀A,DEC,S1,S2.
277  (∀x. set_member A DEC x S1 → set_member A DEC x S2) →
278   set_subset A DEC S1 S2.
279
280(*
281
282lemma acc_is_dead : ∀fix_comp.∀prog : ertl_program.
283 ∀fn : joint_closed_internal_function ERTL (prog_names … prog). ∀l.∀rgs.
284 let after ≝ analyse_liveness fix_comp (prog_names … prog) fn in
285  in_lattice (inr ? ? RegisterA)
286  (livebefore (prog_names … prog) fn rgs (after rgs) l) → False.
287#fix_comp #prog #fn #l #rgs normalize nodelta
288change with (set_member ????) in ⊢ (?% → ?); whd in match (livebefore ?????);
289cases(lookup ????) normalize nodelta
290[ cases(Prop_notb ? (set_member_empty Register eq_Register RegisterA)) #H @H]
291#stmt whd in match statement_semantics; normalize nodelta @if_elim
292[ check fix_correct ccccc
293
294*)
295
296(*
297axiom dead_registers_in_dead :
298 ∀fix_comp.∀build : coloured_graph_computer.
299 ∀prog : ertl_program.
300 ∀fn : joint_closed_internal_function ERTL (prog_names … prog).
301 ∀l.
302 let after ≝ analyse_liveness fix_comp (prog_names … prog) fn in
303 let coloured_graph ≝ build … fn after in
304 ∀R : Register.
305  ¬ lives (inr ? ? R) (livebefore  … fn after l) →
306   to_be_cleared_sb … coloured_graph l R.
307*)
308
309definition dummy_state : state ERTL_semantics ≝
310mk_state ERTL_semantics
311   (None ?) empty_is BBundef 〈empty_map ? ?,mk_hw_register_env … (Stub …) BBundef〉
312   empty O.
313
314definition dummy_state_pc : state_pc ERTL_semantics ≝
315mk_state_pc ? dummy_state (null_pc one) (null_pc one).
316
317definition get_ertl_call_stack :
318list (register_env beval × (Σb:block.block_region b=Code)) →
319list (Σb:block.block_region b=Code) ≝ map … \snd.
320
321
322definition sigma_beval :
323  ertl_program → (ident → option ℕ) → ? → (block → list register) → lbl_funct_type →
324  regs_funct_type → beval → beval≝
325 λprog,stacksizes,init,init_regs,f_lbls,f_regs,bv.
326  match bv with
327  [ BVpc pc p ⇒ match sigma_pc_opt ERTL_semantics LTL_semantics prog stacksizes
328                       init init_regs f_lbls f_regs pc
329                with [Some pc' ⇒ BVpc pc' p | None ⇒ BVundef]
330  | _ ⇒ bv
331  ].
332 
333definition gen_state_rel :
334fixpoint_computer → coloured_graph_computer →
335ertl_program →  (block → list register) → lbl_funct_type → regs_funct_type →
336local_live_type →  (vertex → decision) →
337joint_state_relation ERTL_semantics LTL_semantics ≝
338λfix_comp,colour,prog,init_regs,f_lbls,f_regs,live_fun,color_fun,pc,st1,st2.
339let m1 ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in
340let stacksizes ≝ lookup_stack_cost … m1 in
341let ge ≝ joint_globalenv ERTL_semantics prog stacksizes in
342let init ≝ translate_data fix_comp colour in
343∃f,fn,ssize.
344fetch_internal_function … ge (pc_block pc) = return 〈f,fn〉 ∧
345stacksizes f = return ssize ∧
346let R ≝ λbv1,bv2.bv1 = sigma_beval prog stacksizes init init_regs f_lbls f_regs bv2 in
347match st_frms … st1 with
348[ None ⇒ False
349| Some frames ⇒
350   mem_relation prog stacksizes R f st1 (m … st1) (m … st2) ∧
351   frames_relation fix_comp colour prog R frames (regs … st2) (m … st2) init_regs ∧
352   hw_relation (joint_if_local_stacksize … fn) live_fun
353    color_fun R (\snd (regs … st1)) (regs … st2) (m … st2) ∧
354   make_is_relation_from_beval R (istack … st1) (istack … st2) ∧
355   ((live_fun (inr ?? RegisterCarry)) → carry … st1 ≠ BBundef → carry … st1 = carry … st2) ∧
356   stack_usage … st1 = stack_usage … st2 ∧
357   ∃ptr.sp … st2 = return ptr ∧
358    le ((nat_of_bitvector … (offv (poff … ptr))) + ssize) (2^16 -1) ∧
359    plus (nat_of_bitvector … (offv (poff … ptr))) (stack_usage … st2) = 2^16 ∧
360    ps_relation (joint_if_local_stacksize … fn) live_fun
361     color_fun R ptr (\fst (regs … st1)) 〈regs … st2,m … st2〉
362].
363
364
365definition RegisterAlwaysDead ≝ [RegisterA; RegisterB; RegisterDPL; RegisterDPH; RegisterST1].
366
367definition state_rel :
368fixpoint_computer → coloured_graph_computer →
369ertl_program →  (block → list register) → lbl_funct_type → regs_funct_type →
370joint_state_relation ERTL_semantics LTL_semantics ≝
371λfix_comp,build,prog,init_regs,f_lbls,f_regs,pc,st1,st2.
372let m1 ≝ (\snd (\fst (ertl_to_ltl fix_comp build prog))) in
373let stacksizes ≝ lookup_stack_cost … m1 in
374let ge ≝ joint_globalenv ERTL_semantics prog stacksizes in
375∃f,fn.
376fetch_internal_function … ge (pc_block pc) = return 〈f,fn〉 ∧
377let after ≝ analyse_liveness fix_comp (prog_names … prog) fn (init_regs (pc_block pc)) in
378let before ≝ livebefore … fn (init_regs (pc_block pc)) after in
379let coloured_graph ≝ build … fn after (init_regs (pc_block pc)) in
380gen_state_rel fix_comp build prog init_regs f_lbls f_regs
381(λv.in_lattice v (before (point_of_pc ERTL_semantics pc)) ∧
382       match v with
383             [ inl r ⇒ true
384             | inr R ⇒ all … (λR'.¬ eq_Register R' R) RegisterAlwaysDead
385             ])
386(colouring … coloured_graph) pc st1 st2.
387
388(*
389definition state_rel : fixpoint_computer → coloured_graph_computer →
390ertl_program →  (block → list register) → lbl_funct_type → regs_funct_type →
391joint_state_relation ERTL_semantics LTL_semantics ≝
392λfix_comp,build,prog,init_regs,f_lbls,f_regs,pc,st1,st2.
393let m1 ≝ (\snd (\fst (ertl_to_ltl fix_comp build prog))) in
394let stacksizes ≝ lookup_stack_cost … m1 in 
395let ge ≝ joint_globalenv ERTL_semantics prog stacksizes in
396∃f,fn.fetch_internal_function … ge (pc_block pc)
397= return 〈f,fn〉 ∧
398let after ≝ (analyse_liveness fix_comp (prog_names … prog) fn (init_regs (pc_block pc))) in
399let before ≝ livebefore … fn (init_regs (pc_block pc)) after in
400let coloured_graph ≝ build … fn after (init_regs (pc_block pc)) in
401let R ≝ λbv1,bv2.bv1 = sigma_beval fix_comp build prog init_regs f_lbls f_regs bv2 in
402let live_fun ≝ λv.in_lattice v (before (point_of_pc ERTL_semantics pc)) in
403match st_frms … st1 with
404[ None ⇒ False
405| Some frames ⇒
406   mem_relation fix_comp build prog R f st1 (m … st1) (m … st2) ∧
407   frames_relation fix_comp build prog R frames (regs … st2) (m … st2) init_regs ∧
408   hw_relation live_fun R (\snd (regs … st1)) (regs … st2) ∧
409   make_is_relation_from_beval R (istack … st1) (istack … st2) ∧
410   (live_fun (inr ?? RegisterCarry) → carry … st1 = carry … st2) ∧
411   ∃ptr.sp … st2 = return ptr ∧
412    ps_relation (joint_if_local_stacksize … fn) live_fun (colouring … coloured_graph)
413     R ptr (\fst (regs … st1)) 〈regs … st2,m … st2〉
414].*)
415
416
417definition state_pc_rel :
418fixpoint_computer → coloured_graph_computer → 
419  ertl_program → (block → list register) → lbl_funct_type →
420  regs_funct_type →  joint_state_pc_relation ERTL_semantics LTL_semantics ≝
421λfix_comp,build,prog,init_regs,f_lbls,f_regs,st1,st2.
422let m1 ≝ (\snd (\fst (ertl_to_ltl fix_comp build prog))) in
423let stacksizes ≝ lookup_stack_cost … m1 in 
424let init ≝ translate_data fix_comp build in
425 state_rel fix_comp build prog init_regs f_lbls f_regs (pc … st1) st1 st2 ∧
426 pc … st1 = pc … st2 ∧
427 (last_pop … st2 = sigma_stored_pc ERTL_semantics LTL_semantics prog stacksizes
428                    init init_regs f_lbls f_regs (last_pop … st1)).
429                   
430   
431lemma hw_reg_retrieve_write_decision_hit : ∀r : Register.∀bv : beval.∀localss.
432∀st : state LTL_LIN_state.
433∀st'. (write_decision localss r bv st) = return st' →
434hw_reg_retrieve (regs … st') r = return bv.
435#r #bv #localss #st #st' whd in match write_decision; normalize nodelta
436whd in match hw_reg_store; normalize nodelta >m_return_bind
437whd in ⊢ (??%% → ?); #EQ destruct(EQ)
438whd in match hw_reg_retrieve; normalize nodelta @eq_f
439whd in match hwreg_retrieve; whd in match hwreg_store; normalize nodelta
440@lookup_insert_hit
441qed.
442
443lemma match_reg_elim : ∀ A : Type[0]. ∀ P : A → Prop. ∀ r : region.
444∀f : (r = XData) → A. ∀g : (r = Code) → A. (∀ prf : r = XData.P (f prf)) →
445(∀ prf : r = Code.P (g prf)) →
446P ((match r return λx.(r = x → ?) with
447    [XData ⇒ f | Code ⇒ g])(refl ? r)).
448#A #P * #f #g #H1 #H2 normalize nodelta [ @H1 | @H2]
449qed.
450
451definition xpointer_of_pointer : pointer → res xpointer ≝
452λptr.
453(match (ptype ptr) return λx.ptype ptr =x → ? with
454 [ XData ⇒ λprf.OK xpointer «ptr,prf»
455 | Code ⇒ λ_.Error xpointer [MSG BadPointer]
456 ]) (refl …).
457 
458lemma xpointer_of_pointer_of_xpointer : ∀ptr : xpointer.
459xpointer_of_pointer ptr = return ptr.
460#ptr whd in match xpointer_of_pointer; normalize nodelta @match_reg_elim
461[ cases ptr -ptr #ptr #prf #prf' % ]
462 cases ptr -ptr #ptr #EQ #EQ1 @⊥ >EQ1 in EQ; #EQ destruct
463qed.
464
465
466lemma shift_pointer_commute :
467∀w : Word.∀b : bebit.
468gen_preserving … gen_res_preserve …
469(λx,y.x = y)
470(λx,y.x = y)
471(λx.! ptr ← pointer_of_address x;
472    ! ptr ← xpointer_of_pointer ptr;
473    return shift_pointer ? ptr w)
474(λx. let 〈w_h, w_l〉 ≝ vsplit … 8 8 w in
475     ! 〈newaddrl,newcarry〉 ← be_op2 b Add (BVByte w_l) (\fst x);
476     ! 〈newaddrh,newcarry'〉 ← be_op2 newcarry Addc (BVByte w_h) (\snd x);
477     pointer_of_address 〈newaddrl,newaddrh〉).
478cases daemon (*TODO*) qed.
479(*     
480#word #b * #bv1 #bv2 #y #EQ destruct(EQ)
481whd in match pointer_of_address in ⊢ (???????%?); whd in match pointer_of_bevals;
482normalize nodelta cases bv1 -bv1
483[|| #pt1 #pt1' #p1 | #b | #p | #ptr1 #p1 | #pc1 #p1 ]
484try @res_preserve_error_gen normalize nodelta cases bv2 -bv2
485[|| #pt1 #pt1' #p1 | #b | #p | #ptr2 #p2 | #pc1 #p1 ]
486try @res_preserve_error_gen normalize nodelta cases p1 -p1 #p1 #prf1
487cases p2 -p2 #p2 #prf2 @eqb_elim [2: #_ @res_preserve_error_gen]
488#EQ destruct(EQ) @eqb_elim [2: #_ @res_preserve_error_gen]
489#EQ destruct(EQ) @eq_block_elim [2: #_ @res_preserve_error_gen]
490cases ptr1 -ptr1 #bl1 #off1 cases ptr2 -ptr2 #bl2 #off2 #EQ destruct(EQ)
491whd in match eq_bv_suffix; normalize nodelta @eq_bv_elim [2: #_ @res_preserve_error_gen]
492cases off1 -off1 #off1 cases off2 -off2 #off2 normalize nodelta #EQvsplit
493>m_return_bind whd in match xpointer_of_pointer; normalize nodelta @match_reg_elim
494[2: #_ @res_preserve_error_gen] whd in match ptype; normalize nodelta #EQxptr
495>m_return_bind whd in match shift_pointer; normalize nodelta whd in match shift_offset;
496normalize nodelta whd in match be_op2; normalize nodelta whd in match be_add_sub_byte;
497normalize nodelta whd in match ptype; normalize nodelta >EQxptr normalize nodelta
498whd in match Bit_of_val; normalize nodelta >m_return_bind normalize nodelta
499whd in match (op2 ?????); @pair_elim #lft #rgt normalize nodelta
500@pair_elim #lft' #rgt' #EQrgt' #EQ destruct(EQ) >m_return_bind normalize nodelta
501whd in match eq_add_or_sub; normalize nodelta @eq_block_elim [2: * #H @⊥ @H %]
502#_ whd in match eq_bv_suffix; normalize nodelta >EQvsplit @eq_bv_elim
503[2: * #H @⊥ @H %] #_ normalize nodelta @If_elim [2: @eqb_elim [#_ * #H @⊥ @H %] * #H @⊥ @H %]
504#INUTILE @pair_elim #lft1 #rgt1 #EQlft1 >m_return_bind whd in match pointer_of_address;
505whd in match pointer_of_bevals; normalize nodelta cases daemon (*TODO *)
506qed.*)
507
508lemma ps_reg_retrieve_hw_reg_retrieve_commute :
509∀fix_comp,colour,prog,color_fun,live_fun.
510∀init_regs : (block → list register).∀f_lbls,f_regs.∀f : ident.
511∀fn : joint_closed_internal_function ERTL (prog_names … prog).
512∀pc.
513let m1 ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in
514let stacksize ≝ lookup_stack_cost … m1 in 
515fetch_internal_function … (joint_globalenv ERTL_semantics prog stacksize)
516 (pc_block pc) = return 〈f,fn〉→
517 let init ≝ translate_data fix_comp colour in
518gen_preserving2 ?? gen_res_preserve ??????
519     (gen_state_rel fix_comp colour prog init_regs f_lbls f_regs live_fun color_fun pc)
520     (λr,d.
521      bool_to_Prop (live_fun (inl ?? r)) ∧
522      d = (color_fun (inl register Register r)))
523     (λbv,bv'.bv = sigma_beval prog stacksize init init_regs f_lbls f_regs bv') …
524     (λst1.ps_reg_retrieve (regs … st1))
525     (λst,d.m_map Res ?? (\fst …)
526      (read_arg_decision (joint_if_local_stacksize ?? fn) st d)).
527#fix_comp #colour #prog #color_fun #live_fun #init_regs #f_lbls
528#f_regs #f #fn #pc #EQfn #st1 #st2 #r #d
529whd in match gen_state_rel; normalize nodelta * #f1 * #fn1 * #ssize
530** >EQfn whd in ⊢ (??%% → ?); #EQ1
531destruct(EQ1) #EQssize inversion(st_frms … st1)
532[#_ *] #frames #EQframes normalize nodelta ***** #Hmem #Hrames #Hw_relation
533#His #Hcarry * #ptr ** #EQptr #Hssize whd in match ps_relation; whd in match gen_preserving;
534normalize nodelta #H * #Hr #EQd #bv #EQbv cases(H r d ? bv EQbv)
535[2: %{Hr} <EQd in ⊢ (??%?); %] #bv' cases d
536[2: #R normalize nodelta * whd in ⊢ (??%% → ?); #EQ destruct(EQ)
537    change with (hwreg_retrieve ??) in match (lookup ?????);
538    #Hrel %{(hwreg_retrieve (regs … st2) R)} %
539    [ whd in match m_map; whd in match read_arg_decision; normalize nodelta %]
540    assumption ]
541#n normalize nodelta * #H lapply(opt_eq_from_res ???? H) -H #EQbv' #EQ destruct(EQ)
542%{bv'} % [2: %] whd in match m_map; whd in match read_arg_decision; normalize nodelta
543@pair_elim #off_l #off_h #EQoff >m_return_bind >m_return_bind
544lapply EQptr; -EQptr whd in match sp; normalize nodelta
545change with (hwreg_retrieve_sp ?) in match (load_sp ??);
546whd in match hwreg_retrieve_sp; normalize nodelta * #H @('bind_inversion H) -H
547#s_ptr #EQs_ptr change with (xpointer_of_pointer ?) in ⊢ (??%? → ?); #EQptr
548cases(shift_pointer_commute (bitvector_of_nat 16 (joint_if_local_stacksize … fn1 +n))
549      (carry … st2) … 
550      〈hwreg_retrieve (regs LTL_semantics st2) RegisterSPL,
551       hwreg_retrieve (regs LTL_semantics st2) RegisterSPH〉 …)
552[5: >EQs_ptr in ⊢ (??(????%?)?); >m_return_bind >EQptr in ⊢ (??(????%?)?);
553    >m_return_bind %
554|3: %
555|*:
556]
557#ptr1 >EQoff normalize nodelta * #H @('bind_inversion H) -H #res #EQres #H
558@('bind_inversion H) -H #res1 #EQres1 #EQptr1 #EQptr1' >EQres >m_return_bind
559>EQres1 >m_return_bind >EQptr1 >m_return_bind destruct >EQbv' >m_return_bind #_ %
560qed.
561
562lemma all_used_are_live_before :
563∀fix_comp.
564∀prog : ertl_program.
565∀fn : joint_closed_internal_function ERTL (prog_names … prog).
566∀l,stmt.∀callee : list register.
567stmt_at … (joint_if_code … fn) l = return stmt →
568∀r : register. set_member ? (eq_identifier …) r (\fst (used ? callee stmt)) →
569let after ≝ (analyse_liveness fix_comp (prog_names … prog) fn callee) in
570eliminable ? (after l) stmt = false →
571in_lattice (inl ? ? r)  (livebefore  ? fn callee after l).
572#fix_comp #prog #fn #l *
573[ * [#c|* [#c_id | #c_ptr] #args #dest | #a #lbl | *
574[ #str
575| * * * [#r1 * | #R1 whd in match ertl_writable; normalize nodelta #HR1]  *
576  [1,3: * * [1,3: #r * |2,4: #R whd in match ertl_readable; normalize nodelta #HR]
577  |2,4: #b
578  ]
579| #a
580| * [ #r | #b]
581| #i #i_spec #w #dpl #dph
582| #op #a #b * [#r | #by]  * [1,3: #r'|2,4: #by']
583| #op #a #a'
584| * #a #a' * [1,3,5,7,9,11: #r |2,4,6,8,10,12: #b]
585|
586|
587| #a #dpl #dph
588| #dpl #dph #a
589| * #r
590]
591] #nxt| * [ #lbl | | *] |*]
592#callee #EQstmt #r #H #H1 whd in match (in_lattice ??); normalize  nodelta
593whd in match (livebefore ?????);  whd in EQstmt : (??%?); >EQstmt
594normalize nodelta -EQstmt whd in match (statement_semantics ????);
595whd in match(\fst ?); try( @(set_member_union2) assumption) >H1
596normalize nodelta whd in match(\fst ?); @(set_member_union2) assumption
597qed.
598
599
600lemma bool_of_beval_sigma_commute :
601∀fix_comp,colour,prog,init_regs,f_lbls,f_regs.
602gen_preserving … gen_res_preserve …
603(λbv,bv'.bv = sigma_beval fix_comp colour prog init_regs f_lbls f_regs bv')
604(λb1,b2.b1=b2) … bool_of_beval bool_of_beval.
605#fix_comp #colour #prog #init_regs #f_lbls #f_regs whd in match bool_of_beval;
606normalize nodelta * normalize nodelta
607[|| #p1 #p2 #p| #b| #p | #ptr #p | #pc #p ]
608try (#y #_ @res_preserve_error_gen)
609* whd in match sigma_beval; normalize nodelta
610[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'
611|6,13,20,27: #ptr' #p'|7,14,21,28: #pc' #p'] #EQ destruct(EQ) try (@m_gen_return %)
612cases(sigma_pc_opt ?????????) in EQ; normalize nodelta
613[2,4,6,8: #pc''] #EQ destruct(EQ)
614qed.
615
616lemma map_eval_add_dummy_variance_id :
617∀X,Y.∀l,x.map_eval X Y (add_dummy_variance X Y l) x =l.
618#X #Y #l elim l [//] #hd #tl normalize #IH #x >IH %
619qed.
620
621lemma state_pc_eq : ∀p.∀st1,st2 : state_pc p.
622st1 = st2 → st_no_pc … st1 = st_no_pc … st2 ∧
623pc … st1 = pc … st2 ∧ last_pop … st1 = last_pop … st2.
624#p * #st1 #pc1 #lp1 * #st2 #pc2 #lp2 #EQ destruct(EQ)
625%{(refl …)} %{(refl …)} %
626qed.
627
628(* Cut&paste da un altro file con nome split_on_last_append, unificare*)
629lemma split_on_last_append_singl : ∀A : Type[0]. ∀pre : list A.
630∀ last : A. split_on_last ? (pre@[last]) = return 〈pre,last〉.
631#A #pre elim pre [#last %] #a #tl #IH #last whd in ⊢ (??%?);lapply(IH last)
632whd in ⊢ (??%? → ?); #EQ >EQ %
633qed.
634
635lemma split_on_last_append : ∀A : Type[0]. ∀l1,l2: list A.
636 OptPred True (λres.
637  split_on_last ? (l1@l2) = return 〈l1 @ \fst res, \snd res〉)
638  (split_on_last … l2).
639#A #l1 #l2 lapply l1 -l1 @(list_elim_left … l2) //
640#hd #tl #IH #l1 whd >split_on_last_append_singl whd
641<associative_append @split_on_last_append_singl
642qed.
643
644lemma injective_OK: ∀A:Type[0].∀a,b:A. OK … a = OK … b → a=b.
645 #A #a #b #EQ destruct %
646qed.
647
648lemma eq_notb_true_to_eq_false:
649 ∀b. (¬b) = true → b = false.
650* // #abs normalize in abs; destruct
651qed.
652
653lemma fold_insert_singleton : ∀A,B : Type[0].∀a :A.
654∀i : Pos.∀f,b.
655fold A B f (pm_set A i (Some ? a) (pm_leaf A)) b = f i a b.
656#A #B #a #i elim i -i normalize
657[//] #i #IH #f #b @IH
658qed.
659
660lemma eq_f' : ∀A,B : Type[0].∀f,g : A → B. ∀x,y : A.
661(∀w. f w = g w) → x = y → f x = g y. //
662qed.
663   
664(*     
665lemma sigma_fb_state_insensitive_to_dead_reg:
666 ∀prog,bv. ∀st: state ERTL_semantics. ∀l:label.
667 ∀r: register. ∀before.
668  set_member … (eq_identifier RegisterTag) r (\fst  (before l)) = false →
669  sigma_fb_state prog
670   (to_be_cleared_fb before l)
671   (set_regs ERTL_semantics
672    〈reg_store r bv (\fst  (regs ERTL_semantics st)),
673    \snd  (regs ERTL_semantics st)〉 st)
674  = sigma_fb_state prog (to_be_cleared_fb before l) st.
675#prog #bv #st #l #r #before #dead whd in match sigma_fb_state; normalize nodelta
676@eq_f3 [2,3: %] whd in match set_regs; normalize nodelta whd in match sigma_fb_regs;
677normalize nodelta @eq_f2 [2: %] whd in match sigma_fb_register_env;
678normalize nodelta whd in match reg_store; normalize nodelta
679>add_find_all_miss [2: normalize >dead %] cases(lookup ????) [%] #a
680normalize nodelta whd in match to_be_cleared_fb; whd in match lives;
681normalize nodelta whd in match (plives ??); >dead %
682qed.
683
684lemma sigma_fb_state_insensitive_to_dead_Reg:
685 ∀prog,bv. ∀st: state ERTL_semantics. ∀l:label.
686 ∀r: Register. ∀before.
687  set_member … eq_Register r (\snd  (before l)) = false →
688  sigma_fb_state prog
689   (to_be_cleared_fb before l)
690   (set_regs ERTL_semantics
691     〈\fst  (regs ERTL_semantics st),
692      hwreg_store r bv (\snd  (regs ERTL_semantics st))〉
693      st)
694  = sigma_fb_state prog (to_be_cleared_fb before l) st.
695cases daemon (*TODO*)
696qed.
697
698lemma sigma_fb_state_insensitive_to_dead_carry:
699 ∀prog,bv. ∀st: state ERTL_semantics. ∀l:label. ∀before.
700  set_member Register eq_Register RegisterCarry (\snd (before l)) = false →
701   sigma_fb_state prog (to_be_cleared_fb before l) (set_carry ERTL_semantics bv st) =
702   sigma_fb_state prog (to_be_cleared_fb before l) st.
703#prog #b #st #l #cefore #dead whd in match sigma_fb_state; normalize nodelta
704whd in match set_carry; normalize nodelta whd in match to_be_cleared_fb;
705normalize nodelta whd in match (lives ??); >dead %
706qed.
707*)
708
709lemma split_orb_false: ∀a,b:bool. orb a b = false → a = false ∧ b = false.
710 ** normalize #abs destruct /2/
711qed.
712
713lemma eta_set_carry:
714 ∀P,st. set_carry P (carry P st) st = st.
715#P * //
716qed.
717
718lemma set_carry_set_regs_commute:
719 ∀P,st,c,v. set_carry P c (set_regs P v st) = set_regs P v (set_carry P c st).
720 #P * //
721qed.
722
723lemma eliminable_step_to_eq_livebefore_liveafter:
724 ∀prog,stackcost,fn.
725 let p_in ≝ mk_prog_params ERTL_semantics prog stackcost in
726 ∀stms: joint_seq ERTL_semantics (prog_names … prog). ∀next.
727 ∀pt.
728 stmt_at p_in ? (joint_if_code p_in … fn) pt = return (sequential … stms next) →
729 ∀liveafter,callee.
730 eliminable_step (globals … p_in) (liveafter pt) stms = true →
731  livebefore … fn callee liveafter pt = liveafter pt.
732 #prog #stackcost #fn #stms #next #pt #stmt_at #liveafter #callee #Helim
733 whd in ⊢ (??%?); whd in stmt_at:(??%?); cases (lookup ????) in stmt_at;
734 normalize nodelta try (#abs whd in abs:(??%%); destruct (abs) @I)
735 #stms' #EQ whd in EQ:(??%%); destruct (EQ) whd in ⊢ (??%?);
736 whd in match eliminable; normalize nodelta >Helim %
737qed.
738
739lemma set_subset_to_set_subst_set_union_left:
740 ∀T,eqT,A,B,C. set_subset T eqT A B → set_subset … eqT A (set_union … B C).
741 #T #eqT #A #B #C #H @set_member_subset_onlyif #x #K
742 lapply (set_member_subset_if … H) #H2 /3 by set_member_union1/
743qed.
744
745lemma set_subset_to_set_subst_set_union_right:
746 ∀T,eqT,A,B,C. set_subset T eqT A C → set_subset … eqT A (set_union … B C).
747 #T #eqT #A #B #C #H @set_member_subset_onlyif #x #K
748 lapply (set_member_subset_if … H) #H2 /3 by set_member_union2/
749qed.
750
751lemma rl_included_rl_join_left:
752 ∀A,B,C. rl_included A B → rl_included A (rl_join B C).
753 #A #B #C whd in match rl_included; normalize nodelta #H
754 cases (andb_Prop_true … H) -H #H1 #H2 @andb_Prop
755 /2 by set_subset_to_set_subst_set_union_left/
756qed.
757
758lemma rl_included_rl_join_right:
759 ∀A,B,C. rl_included A C → rl_included A (rl_join B C).
760 #A #B #C whd in match rl_included; normalize nodelta #H
761 cases (andb_Prop_true … H) -H #H1 #H2 @andb_Prop
762 /2 by set_subset_to_set_subst_set_union_right/
763qed.
764
765lemma set_subset_reflexive: ∀A,DEC,x. set_subset A DEC x x.
766 /2/
767qed.
768
769lemma rl_included_reflexive: ∀x. rl_included x x.
770 /2/
771qed.
772
773include alias "utilities/deqsets_extra.ma".
774
775lemma mem_of_fold_join:
776 ∀F,dom.
777  ∀x. x ∈ dom →
778   rl_included (F x)
779    (fold label (l_property register_lattice) rl_join rl_bottom (λl:label.true)
780      F dom).
781 #F #dom elim dom [ #x * ] #hd #tl #IH #x whd in match (? ∈ ?);
782 @eqb_elim
783 normalize nodelta #Hx #H change with (rl_join ??) in ⊢ (?(??%));
784 destruct /3 by rl_included_rl_join_left,rl_included_rl_join_right/
785qed.
786
787lemma set_subset_transitive:
788 ∀A,DEC,S1,S2,S3.
789  set_subset A DEC S1 S2 → set_subset … DEC S2 S3 → set_subset … DEC S1 S3.
790 #A #DEC #S1 #S2 #S3
791 #H1 lapply (set_member_subset_if … H1) -H1 #H1
792 #H2 lapply (set_member_subset_if … H2) -H2 #H2
793 @set_member_subset_onlyif /3 by/
794qed.
795
796lemma rl_included_transitive:
797 ∀S1,S2,S3. rl_included S1 S2 → rl_included S2 S3 → rl_included S1 S3.
798 #S1 #S2 #S3 whd in match rl_included; normalize nodelta
799 #H cases (andb_Prop_true … H) -H #H1 #H2
800 #H cases (andb_Prop_true … H) -H #H3 #H4
801 /3 by andb_Prop,set_subset_transitive/
802qed.
803
804lemma rl_included_rl_diff_rl_empty:
805 ∀S1. rl_included S1 (rl_diff S1 rl_bottom).
806 #S1 whd in match (rl_included ??);
807 lapply (set_member_subset_onlyif … (eq_identifier …) (\fst S1) (\fst (rl_diff S1 rl_bottom)))
808 cases (set_subset ????)
809 /3 by set_member_diff,set_member_subset_onlyif/
810qed.
811
812lemma included_livebefore_livebeafter_stmt_labels:
813 ∀fix_comp,globals,fn,l,stmt,callee.
814  let after ≝ analyse_liveness fix_comp globals fn callee in
815   stmt_at … (joint_if_code ERTL … fn) l = Some … stmt →
816  ∀nxt.
817   nxt ∈
818    stmt_labels (mk_stmt_params (g_u_pars ERTL) label (Some label) false)
819     globals stmt →
820  l_included register_lattice (livebefore … fn callee after nxt) (after l).
821#fix_comp #globals #fn #l #stmt #callee letin after ≝ (analyse_liveness ????)
822#EQlookup #nxt
823#Hnxt lapply (fix_correct … after l) #spec @(rl_included_transitive … spec) -spec
824whd in match (liveafter ?????); whd in EQlookup:(??%?); >EQlookup -EQlookup normalize nodelta
825/2 by mem_of_fold_join/
826qed.
827
828(*
829axiom eq_sigma_state_monotonicity:
830 ∀prog,live,graph,st1,st2,l1,l2,frames.
831 st_frms ? st1 = return frames →
832  rl_included (live l2) (live l1) →
833  sigma_fb_state prog (to_be_cleared_fb live l1) st1 =
834   sigma_sb_state (get_ertl_call_stack frames) prog
835    (to_be_cleared_sb live graph l1) st2 →
836  sigma_fb_state prog (to_be_cleared_fb live l2) st1 =
837   sigma_sb_state (get_ertl_call_stack frames) prog
838    (to_be_cleared_sb live graph l2) st2.
839
840
841
842lemma fetch_ok_sigma_state_ok : ∀fix_comp,colour,prog,init_regs,f_lbls,f_regs.
843let m ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in
844let stacksizes ≝ lookup_stack_cost … m in
845∀st1,st2,f,fn. state_pc_rel fix_comp colour prog init_regs f_lbls f_regs st1 st2 →
846fetch_internal_function …
847(joint_globalenv ERTL_semantics prog stacksizes) (pc_block (pc … st1)) 
848     = return 〈f,fn〉 →
849let callee ≝ init_regs (pc_block (pc … st1)) in
850let after ≝ (analyse_liveness fix_comp (prog_names … prog) fn callee) in
851let before ≝ livebefore … fn callee after in
852let coloured_graph ≝ colour … fn after callee in
853match st_frms … (st_no_pc … st1) with
854[ None ⇒ False
855| Some frames ⇒
856 (sigma_fb_state prog
857  (to_be_cleared_fb before (point_of_pc ERTL_semantics (pc … st1)))
858  (st_no_pc … st1)) =
859 (sigma_sb_state (get_ertl_call_stack frames) prog
860   (to_be_cleared_sb … coloured_graph (point_of_pc ERTL_semantics (pc … st1)))
861  (st_no_pc … st2))
862].
863#fix_comp #colour #prog #init_regs #f_lbls #f_regs #st1 #st2 #f #fn
864#H #EQfn whd in match state_pc_rel in H; normalize nodelta in H;
865inversion (st_frms … st1) in H; [ #_ *] #frames #EQframes normalize nodelta
866whd in match sigma_fb_state_pc; whd in match sigma_sb_state_pc;
867normalize nodelta >EQfn normalize nodelta inversion(fetch_internal_function ????)
868[2: #e #_ normalize nodelta whd in match dummy_state_pc; whd in match null_pc;
869    normalize nodelta #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
870    >fetch_internal_function_no_zero in EQfn; [2: >e1 %] whd in ⊢ (???% → ?);
871    #ABS destruct(ABS) ]
872* #f1 #fn1 #EQfn1 normalize nodelta #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ
873destruct(EQ) <e1 in EQfn1; >EQfn whd in ⊢ (??%?? → ?); #EQ1 destruct(EQ1)
874whd in match sigma_fb_state; normalize nodelta >e0 >e1 %
875qed.
876     
877lemma fetch_ok_pc_ok : ∀fix_comp,colour,prog,init_regs,f_lbls,f_regs.
878let m ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in
879let stacksizes ≝ lookup_stack_cost … m in
880∀st1,st2,f,fn. state_pc_rel fix_comp colour prog init_regs f_lbls f_regs st1 st2 →
881fetch_internal_function …
882(joint_globalenv ERTL_semantics prog stacksizes) (pc_block (pc … st1)) 
883     = return 〈f,fn〉 → (pc … st1) = (pc … st2).
884#fix_comp #colour #prog #init_regs #f_lbls #f_regs #st1 #st2 #f #fn
885#H #EQfn whd in match state_pc_rel in H; normalize nodelta in H;
886inversion (st_frms … st1) in H; [ #_ *] #frames #EQframes normalize nodelta
887whd in match sigma_fb_state_pc; whd in match sigma_sb_state_pc;
888normalize nodelta >EQfn normalize nodelta inversion(fetch_internal_function ????)
889[2: #e #_ normalize nodelta whd in match dummy_state_pc; whd in match null_pc;
890    normalize nodelta #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
891    >fetch_internal_function_no_zero in EQfn; [2: >e1 %] whd in ⊢ (???% → ?);
892    #ABS destruct(ABS) ]
893* #f1 #fn1 #EQfn1 normalize nodelta #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ
894destruct(EQ) <e1 in EQfn1; >EQfn whd in ⊢ (??%?? → ?); #EQ1 destruct(EQ1) %
895qed.
896
897*)
898
899(*
900axiom insensitive_to_be_cleared_sb_regs :
901∀prog.∀tb : local_clear_sb_type. ∀st : state LTL_LIN_state.
902∀bv.∀r : Register.∀cs.∀rgs. tb r →
903sigma_sb_state cs prog tb (set_regs LTL_semantics rgs st) =
904sigma_sb_state cs prog tb (set_regs LTL_semantics
905          (hwreg_store r bv rgs) st).
906
907axiom insensitive_sb_to_hwreg_set_other :
908∀prog.∀tb : local_clear_sb_type. ∀st : state LTL_LIN_state.
909∀b,cs,rgs.
910sigma_sb_state cs prog tb
911 (set_regs LTL_semantics (hwreg_set_other b rgs) st) =
912sigma_sb_state cs prog tb (set_regs LTL_semantics rgs st).
913
914axiom insensitive_to_be_cleared_carry :
915∀prog.∀tb : local_clear_sb_type. ∀st : state LTL_LIN_state.
916∀b.∀cs. tb RegisterCarry →
917sigma_sb_state cs prog tb (set_carry LTL_semantics b st) =
918sigma_sb_state cs prog tb st.
919*)
920(*
921axiom dpl_is_dead : ∀fix_comp.∀prog : ertl_program.
922 ∀fn : joint_closed_internal_function ERTL (prog_names … prog). ∀callee,l.
923 let after ≝ analyse_liveness fix_comp (prog_names … prog) fn callee in
924  in_lattice (inr ? ? RegisterDPL) (livebefore  … fn callee after l) → False.
925
926axiom dph_is_dead : ∀fix_comp.∀prog : ertl_program.
927 ∀fn : joint_closed_internal_function ERTL (prog_names … prog). ∀callee,l.
928 let after ≝ analyse_liveness fix_comp (prog_names … prog) fn callee in
929  in_lattice (inr ? ? RegisterDPH) (livebefore  … fn callee after l) → False.
930*)
931
932lemma m_return_if_commute :  ∀M : Monad.∀A : Type[0]. ∀a1,a2 : A.∀b : bool.
933if b then m_return M A a1 else m_return M A a2 =
934m_return M A (if b then a1 else a2).
935#M #A #a1 #a2 * %
936qed.
937
938lemma set_carry_eta :∀p.∀st : state p.set_carry p (carry … st) st = st.
939#p * //
940qed.
941
942lemma set_regs_eta :∀p.∀st : state p. set_regs p (regs … st) st = st.
943#p * //
944qed.
945
946lemma commute_if : ∀A,B : Type[0].∀b : bool.∀x,y : A.∀f : A → B.
947f (if b then x else y) = if b then f x else f y.
948#A #B * // qed.
949
950
951lemma colouring_is_never_forbidden: ∀fix_comp,colour,prog.
952let m ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in
953let stacksizes ≝ lookup_stack_cost … m in
954∀bl,f,fn,callee,R.∀r : register.
955fetch_internal_function …
956(joint_globalenv ERTL_semantics prog stacksizes) bl = return 〈f,fn〉 →
957let after ≝ (analyse_liveness fix_comp (prog_names … prog) fn callee) in
958let before ≝ livebefore … fn callee after in
959colouring … (colour … fn after callee)  (inl register Register r) =
960decision_colour R → All ? (λr1.R ≠ r1) RegistersForbidden.
961#fix_comp #colour #prog #bl #f #fn #callee #R #r #EQfn
962normalize nodelta #EQcol %
963[2: % [2: % [2: % [2: % [2: % [2: % [2: % [2: @I]]]]]]]] % #EQ
964letin after ≝ (analyse_liveness fix_comp (prog_names … prog) fn callee)
965lapply(prop_colouring … (colour … fn after callee)
966        (an_identifier LabelTag one) (inl ?? r) (inr ?? R) ?)
967[1,3,5,7,9,11,13,15: whd in match interferes; normalize nodelta
968  @orb_Prop_r whd in match interferes_asym; normalize nodelta
969  @orb_Prop_l destruct // ]
970destruct >EQcol >hdw_same_colouring #H lapply(H (refl …)) #EQ1 destruct
971qed.
972
973definition update_fun : ∀A,B : Type[0].(A → A → bool) → (A → B) → A → B → A → B ≝
974λA,B,eq,f,x,d,a. if eq a x then d else f a.
975
976definition eq_vertex : vertex → vertex → bool ≝
977λv1,v2.match v1 with
978  [ inl r ⇒ match v2 with [inl r' ⇒ eq_identifier … r r' | _ ⇒ false ]
979  | inr r ⇒ match v2 with [inr r' ⇒ eq_Register … r r' | _ ⇒ false ]
980  ].
981
982lemma eq_vertex_elim : ∀P : bool → Prop.
983∀v1,v2.(v1 = v2 → P true) → (v1 ≠ v2 → P false) → P (eq_vertex v1 v2).
984#P * [#r1 | #R1] * [1,3: #r2 |*: #R2] #H1 #H2 whd in match eq_vertex; normalize nodelta
985[2,3: @H2 % #EQ destruct
986| @eq_identifier_elim #H3 [ @H1 destruct % | @H2 % #EQ destruct cases H3 #H @H %]
987| @eq_Register_elim #H3 [ @H1 destruct % | @H2 % #EQ destruct cases H3 #H @H %]
988]
989qed.
990
991include alias "arithmetics/nat.ma".
992
993lemma beloadv_bestorev_hit : ∀m,m',ptr,bv.
994bestorev m ptr bv = return m' →
995beloadv m' ptr = return bv.
996cases daemon (*TODO*)
997qed.
998
999lemma beloadv_bestorev_miss : ∀m,m',ptr1,ptr2,bv.
1000ptr1 ≠ ptr2 →
1001bestorev m ptr1 bv = return m' →
1002beloadv m' ptr2 = beloadv m ptr2.
1003cases daemon (*TODO*)
1004qed.
1005
1006lemma shift_pointer_injective :
1007∀m,ptr,n1,n2.shift_pointer m ptr n1 = shift_pointer m ptr n2 → n1 = n2.
1008cases daemon qed.
1009
1010axiom BadVertexValue : ErrorMessage.
1011
1012definition ertl_vertex_retrieve :  ertl_reg_env → vertex → res beval ≝
1013λregs,v.match v with
1014[inl r ⇒ ps_reg_retrieve regs r
1015| inr r ⇒ match hwreg_retrieve (\snd regs) r with
1016   [ BVundef ⇒ Error ? [MSG BadVertexValue]
1017   | _ ⇒ OK ? (hwreg_retrieve (\snd regs) r)
1018   ]
1019].
1020 
1021definition eq_decision : decision → decision → bool ≝
1022λd1,d2.match d1 with
1023[ decision_spill n1 ⇒ match d2 with [ decision_spill n2 ⇒ eqb n1 n2 | _ ⇒ false ]
1024| decision_colour R1 ⇒ match d2 with [ decision_colour R2 ⇒ eq_Register R1 R2 | _ ⇒ false ]
1025].
1026
1027lemma eq_decision_elim : ∀P : bool → Prop.∀d1,d2.(d1 = d2 → P true) → (d1 ≠ d2 → P false) →
1028P (eq_decision d1 d2).
1029#P * [#n1 | #R1] * [1,3: #n2 |*: #R2] whd in match eq_decision; normalize nodelta
1030#H1 #H2
1031[ @eqb_elim [#EQ destruct @H1 % | * #H @H2 % #EQ destruct @H %]
1032|2,3: @H2 % #EQ destruct
1033| @eq_Register_elim [ #EQ destruct @H1 % | * #H @H2 % #EQ destruct @H %]
1034]
1035qed.
1036
1037lemma ertl_vertex_retrieve_ok_on_hw_regs :
1038∀regs,r,bv.ertl_vertex_retrieve regs (inr ?? r) = return bv →
1039hwreg_retrieve (\snd regs) r = bv.
1040#regs #r #bv whd in match ertl_vertex_retrieve; normalize nodelta
1041cases(hwreg_retrieve ??) normalize nodelta
1042[|| #x #y #p | #b | #p | #ptr #p | #pc #p ]
1043#EQ whd in EQ : (???%); destruct %
1044qed.
1045
1046lemma hwreg_retrieve_sp_insensitive_to_set_other : ∀b,rgs.
1047hwreg_retrieve_sp (hwreg_set_other b rgs) = hwreg_retrieve_sp rgs.
1048#b #rgs whd in match hwreg_retrieve_sp; normalize nodelta
1049>hwreg_retrieve_insensitive_to_set_other >hwreg_retrieve_insensitive_to_set_other %
1050qed.
1051
1052lemma hwreg_retrieve_sp_insensitive_to_regstore : ∀R,regs,bv.
1053R ≠ RegisterSPL → R ≠ RegisterSPH →
1054hwreg_retrieve_sp (hwreg_store R bv regs) = hwreg_retrieve_sp regs.
1055#R #regs #bv #H1 #H2 whd in match hwreg_retrieve_sp; normalize nodelta
1056>hwreg_retrieve_hwregstore_miss [2: @sym_not_eq assumption]
1057>hwreg_retrieve_hwregstore_miss [2: @sym_not_eq assumption] %
1058qed.
1059
1060lemma vertex_retrieve_read_arg_decision_commute :
1061∀fix_comp,colour,prog,color_fun,live_fun.
1062∀init_regs : (block → list register).∀f_lbls,f_regs.∀f : ident.
1063∀fn : joint_closed_internal_function ERTL (prog_names … prog).
1064∀pc.
1065let m1 ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in
1066let stacksize ≝ lookup_stack_cost … m1 in 
1067fetch_internal_function … (joint_globalenv ERTL_semantics prog stacksize)
1068 (pc_block pc) = return 〈f,fn〉→
1069 let init ≝ translate_data fix_comp colour in
1070(∀v.∀R. color_fun v = decision_colour R → R = RegisterDPL ∨ R = RegisterDPH → ¬ live_fun v) →
1071bool_to_Prop (¬ live_fun (inr ?? RegisterDPL)) →
1072bool_to_Prop (¬ live_fun (inr ?? RegisterDPH)) →
1073gen_preserving2 ?? gen_res_preserve ??????
1074     (gen_state_rel fix_comp colour prog init_regs f_lbls f_regs live_fun color_fun pc)
1075     (λv,d.v ≠ (inr ?? RegisterCarry) ∧ bool_to_Prop(live_fun v) ∧ d = (color_fun v))
1076     (λx,y.\fst x = sigma_beval prog stacksize init init_regs f_lbls f_regs (\fst y) ∧
1077          gen_state_rel fix_comp colour prog init_regs f_lbls f_regs
1078           (update_fun … eq_vertex live_fun (inr ?? RegisterCarry) false)
1079           color_fun pc (\snd x) (\snd y)) …
1080     (λst1,v.! bv ← ertl_vertex_retrieve (regs … st1) v;
1081              return〈bv,st1〉)
1082     (λst,d.(read_arg_decision (joint_if_local_stacksize ?? fn) st d)).
1083#fix_comp #colour #prog #color_fun #live_fun #init_regs #f_lbls #f_regs
1084#f #fn #pc #EQfn #Hvert #Hdpl #Hdph #st1 #st2 *
1085[ #r #d #Rst1st2 ** #_ #live_r #colour_d * #bv #st #H @('bind_inversion H) -H
1086  #bv1 whd in match ertl_vertex_retrieve; normalize nodelta #EQbv1
1087  whd in ⊢ (??%% → ?); #EQ destruct(EQ)
1088  cases (ps_reg_retrieve_hw_reg_retrieve_commute … EQfn … Rst1st2 … EQbv1)
1089  [3: % assumption |2:] #fbv * whd in match m_map; normalize nodelta
1090  #H @('bind_inversion H) -H * #fbv1 #st2' #EQfbv1 whd in ⊢ (??%% → ?);
1091  #EQ destruct(EQ) #EQ destruct(EQ) %{〈fbv,st2'〉} %{EQfbv1} % [%]
1092  whd in match read_arg_decision in EQfbv1; normalize nodelta in EQfbv1;
1093  destruct cases (color_fun ?) in EQfbv1; [#n | #R] normalize nodelta
1094  [2: whd in ⊢ (??%% → ?); #EQ destruct(EQ)
1095  | @pair_elim #high #low #EQhl >m_return_bind >m_return_bind #H @('bind_inversion H) -H
1096    #val1 #EQval1 #H @('bind_inversion H) -H #val2 #EQval2 #H @('bind_inversion H)
1097    -H #ptr #EQptr #H @('bind_inversion H) -H #fbv1 #H lapply(opt_eq_from_res ???? H)
1098    -H #EQfbv1 whd in ⊢ (??%% → ?); #EQ destruct(EQ) whd in match set_carry;
1099    normalize nodelta
1100  ]
1101  cases Rst1st2 #f1 * #fn1 * #ssize ** >EQfn whd in ⊢ (??%% → ?);
1102  #EQ destruct(EQ) #EQssize inversion(st_frms ??) [1,3: #_ *] #frames #EQframes
1103  normalize nodelta ****** #Hmem #Hframes #Hhw #His #Hcarry #Hstack #Hpsregs
1104  %{f1} %{fn1} %{ssize} % [1,3: % assumption] >EQframes normalize nodelta %
1105  [2,4: cases Hpsregs -Hpsregs #ptr *** #EQptr #H1 #H2 #H3 %{ptr} %
1106    [1,3: % [2,4: assumption] % [1,2,4: assumption]
1107         change with (hwreg_retrieve_sp ?) in ⊢ (??%?);
1108         >hwreg_retrieve_sp_insensitive_to_regstore
1109         [ >hwreg_retrieve_sp_insensitive_to_regstore [ assumption]]
1110         normalize % #EQ destruct
1111    |*: #r1 #d1 * whd in match update_fun; normalize nodelta #r1_live #EQ destruct(EQ)
1112        #bv1 #EQbv1 [ @(H3 … EQbv1) % //] cases(H3 … EQbv1) [3: % [ assumption | % ] |2:]
1113        #bv1' inversion(color_fun ?) [ #n | #R ] #EQcol normalize nodelta *
1114        [ #H lapply(opt_eq_from_res ???? H) -H #EQbv1'
1115        | whd in ⊢ (??%% → ?); #EQ destruct(EQ)
1116        ]
1117        #EQ destruct(EQ) [ %{bv1'} % [ >EQbv1' % | %]]
1118        %{(hwreg_retrieve (regs … st2) R)} % [2: %] >hwreg_retrieve_hwregstore_miss
1119        [ >hwreg_retrieve_hwregstore_miss [%]] % #H lapply(Hvert … EQcol ?)
1120        [1,3: [%2|%] assumption] >r1_live *
1121    ]
1122  |*: % [2,4: assumption] % [2,4: *] % [2,4: assumption] %
1123      [2,4: [2: whd >hwreg_retrieve_sp_insensitive_to_regstore
1124               [ >hwreg_retrieve_sp_insensitive_to_regstore ] ]
1125            [2,3,4,5: normalize % #EQ destruct(EQ) |*: %{(proj1 ?? Hhw)} ]
1126            #r1 * #r1_no_c whd in match update_fun; normalize nodelta
1127            @eq_vertex_elim [1,3: #EQ destruct(EQ) @⊥ @r1_no_c % ] #_
1128            normalize nodelta #r1_live #r1_no_undef [2: @(proj2 … Hhw) [%] assumption]
1129            lapply(proj2 ?? Hhw … r1_live r1_no_undef) [% assumption]
1130            inversion(color_fun ?) normalize nodelta [ #n #_ #H @H]
1131            #R1 #HR1 #H >hwreg_retrieve_hwregstore_miss
1132            [ >hwreg_retrieve_hwregstore_miss [ @H ] ] % #H1
1133            lapply(Hvert … HR1 ?) [1,3: [%2|%] assumption] >r1_live *
1134            #H1 #H2 assumption
1135      |*: % [1,2,3: assumption ] cases daemon (*TODO in a separate lemma *)
1136      ]
1137  ]
1138]
1139#Reg #dec #Rst1st2 *** #Reg_nocarry #Reg_live #EQ destruct(EQ) * #bv #st1'
1140#H @('bind_inversion H) -H #bv1 #EQbv1 whd in ⊢ (??%% → ?); #EQ destruct(EQ)
1141cases Rst1st2 #f1 * #fn1 * #ssize ** >EQfn whd in ⊢ (??%% → ?); #EQ destruct(EQ)
1142#EQsszie inversion(st_frms ??) [ #_ *] #frames #EQframes normalize nodelta ******
1143#Hmem #Hframes #Hhw #His #Hcarry #Hstack #Hps cut(? : Prop)
1144[3: #H_nocarry lapply(proj2 ?? Hhw … Reg_live H_nocarry)
1145    [% #EQ destruct(EQ) @Reg_nocarry %] cases(color_fun ?) normalize nodelta
1146    [ #n inversion(hwreg_retrieve_sp ?) normalize nodelta [2: #e #_ *]
1147      #ptr #EQptr inversion(beloadv ??) [#_ *] #bv2 #EQbv2 normalize nodelta
1148      #Hbv2 @('bind_inversion EQptr) #ptr1 #EQptr1 @match_reg_elim
1149      [2: #_ whd in ⊢ (??%% → ?); #EQ destruct(EQ)] #prf whd in ⊢ (??%% → ?);
1150      #EQ destruct(EQ)
1151      cases(shift_pointer_commute (bitvector_of_nat 16 (joint_if_local_stacksize … fn1 +n))
1152                (carry … st2) … 
1153                〈hwreg_retrieve (regs LTL_semantics st2) RegisterSPL,
1154                 hwreg_retrieve (regs LTL_semantics st2) RegisterSPH〉 …)
1155     [5: >EQptr1 in ⊢ (??(????%?)?); >m_return_bind whd in match xpointer_of_pointer;
1156         normalize nodelta @match_reg_elim [2: >prf in ⊢ (% → ?); #EQ destruct(EQ)]
1157         #prf1 >m_return_bind %
1158      |3: %
1159      |*:
1160      ]
1161      @pair_elim #ptr_h #ptr_l #EQvsplit #ptr2 * #H @('bind_inversion H) -H #val1
1162      #EQval1 #H @('bind_inversion H) -H #val2 #EQval2 #EQptr2 #EQ destruct(EQ)
1163      %
1164      [ % [ @bv2]
1165      | %
1166        [ whd in match read_arg_decision; normalize nodelta >EQvsplit in ⊢ (??%?);
1167          normalize nodelta >m_return_bind >m_return_bind >EQval1 in ⊢ (??%?);
1168          >m_return_bind >EQval2 in ⊢ (??%?); >m_return_bind >EQptr2 in ⊢ (??%?);
1169          >m_return_bind >EQbv2 in ⊢ (??%?); %
1170        | % [ <Hbv2 whd in match ertl_vertex_retrieve in EQbv1; normalize nodelta in EQbv1;
1171              cases(hwreg_retrieve ??) in EQbv1; normalize nodelta
1172              try (whd in ⊢ (??%% → ?); #EQ destruct(EQ) %)
1173              try (#x1 whd in ⊢ (??%% → ?); #EQ destruct(EQ) %)
1174              try (#x1 #x2 whd in ⊢ (??%% → ?); #EQ destruct(EQ) %)
1175              #x1 #x2 #x3 whd in ⊢ (??%% → ?); #EQ destruct(EQ) % ]
1176          %{f1} %{fn1} %{ssize} % [ %{EQfn} assumption ] >EQframes normalize nodelta
1177          %
1178          [2: cases Hps #ptr3 *** change with (hwreg_retrieve_sp ?) in ⊢ (??%? → ?);
1179           >EQptr in ⊢ (% → ?); whd in ⊢ (??%% → ?); #EQ destruct(EQ) #H1 #H2 #H3
1180           %{(«ptr1,prf»)} whd in match set_regs; normalize nodelta
1181           %
1182           [ %
1183             [ % [2: assumption] change with (hwreg_retrieve_sp ?) in ⊢ (??%?);
1184               >hwreg_retrieve_sp_insensitive_to_regstore
1185               [ >hwreg_retrieve_sp_insensitive_to_regstore [ assumption] ]
1186               % normalize #EQ destruct
1187             | assumption
1188             ]
1189           ]
1190           #r1 #d1 * whd in match update_fun; normalize nodelta #live_r1 #EQ destruct(EQ)
1191           #bev #EQbev cases(H3 … (color_fun (inl ?? r1)) … EQbev) [2: %{live_r1} %]
1192           #bev1 inversion(color_fun ?) normalize nodelta [#n #_ #H1 %{bev1} assumption]
1193           #R1 #EQR1 * whd in ⊢ (??%% → ?); #EQ1 #EQ2 destruct %{(hwreg_retrieve (regs … st2) R1)}
1194           % [2: %] >hwreg_retrieve_hwregstore_miss [ >hwreg_retrieve_hwregstore_miss [%]]
1195           % #H lapply(Hvert … EQR1 ?) [1,3: [%2|%] assumption ] >live_r1 *
1196          | % [2: assumption] % [2: *] % [2: assumption ] % cases daemon (*TODO*)
1197          ]
1198        ]
1199      ]
1200    | cases daemon (*TODO*)
1201    ]
1202|
1203| whd in match ertl_vertex_retrieve in EQbv1; normalize nodelta in EQbv1;
1204  cases(hwreg_retrieve ??) in EQbv1; normalize nodelta
1205  [ whd in ⊢ (??%% → ?); #EQ destruct(EQ)
1206  |*: try( #H1 #H2 #H3 #H4) try( #H1 #H2 #H3) try( #H1 #H2) try( #H1) % #EQ destruct
1207  ]
1208]
1209qed.
1210
1211definition ertl_vertex_store : vertex → beval → state ERTL_state → state ERTL_state ≝
1212λv,bv,st.match v with
1213[ inl r ⇒ set_regs ERTL_state 〈reg_store r bv (\fst (regs … st)),\snd (regs … st)〉 st
1214| inr r ⇒ set_regs ERTL_state 〈\fst (regs … st),hwreg_store r bv (\snd (regs … st))〉 st
1215].
1216
1217lemma state_rel_insensitive_to_dead_write_decision :
1218∀fix_comp,colour,prog,color_fun,live_fun.
1219∀init_regs : (block → list register).∀f_lbls,f_regs.∀f : ident.
1220∀fn : joint_closed_internal_function ERTL (prog_names … prog).
1221∀pc.
1222let m1 ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in
1223let stacksize ≝ lookup_stack_cost … m1 in 
1224fetch_internal_function … (joint_globalenv ERTL_semantics prog stacksize)
1225 (pc_block pc) = return 〈f,fn〉→
1226∀r : Register.
1227In … RegisterAlwaysDead r →
1228∀bv.(∀v.color_fun v = (decision_colour r) → ¬ live_fun v) →
1229gen_preserving ?? gen_res_preserve ????
1230   (gen_state_rel fix_comp colour prog init_regs f_lbls f_regs live_fun color_fun pc)
1231   (gen_state_rel fix_comp colour prog init_regs f_lbls f_regs live_fun color_fun pc)
1232   (m_return …)
1233   (λst.write_decision (joint_if_local_stacksize ?? fn) (decision_colour r) bv st).
1234#fix_comp #colour #prog #color_fun #live_fun #init_regs #f_lbls #f_regs #f #fn #pc
1235#EQfn #r #r_forb #bv #Hr #st1 #st2 #Rst1st2 #st1' whd in ⊢ (??%% → ?);
1236#EQ destruct(EQ) %
1237[2: % [ whd in match write_decision; normalize nodelta >m_return_bind %] |]
1238cases Rst1st2 #f1 * #fn1 * #ssize ** >EQfn whd in ⊢ (??%% → ?); #EQ destruct(EQ)
1239#EQssize inversion(st_frms ??); [ #_ * ] #frames #EQframes normalize nodelta
1240****** #Hmem #Hframes #Hhw #His #Hcarry #Hstack * #sp *** #EQsp #H1 #H2 #Hps
1241%{f1} %{fn1} %{ssize} % [ %{EQfn} assumption ] >EQframes normalize nodelta
1242%
1243[2: %{sp} %
1244   [ % [2: assumption ] % [2: assumption ]
1245     change with (hwreg_retrieve_sp ?) in ⊢ (??%?); whd in match set_regs;
1246     normalize nodelta >hwreg_retrieve_sp_insensitive_to_regstore
1247     [ assumption ] % #EQ destruct(EQ) cases r_forb
1248     [1,3: normalize #EQ destruct(EQ) ] *
1249     [1,3: normalize #EQ destruct(EQ) ] *
1250     [1,3: normalize #EQ destruct(EQ) ] *
1251     [1,3: normalize #EQ destruct(EQ) ] *
1252     [1,3: normalize #EQ destruct(EQ) ] *
1253   | whd #r1 #d1 * #live_r1 #EQ destruct(EQ) #bv1 #EQbv1
1254     cases(Hps … (color_fun (inl ?? r1)) …  EQbv1) [2: % // ]
1255     #bv2 inversion(color_fun ?) normalize nodelta
1256     [#n #_ * #EQ1 #EQ2 destruct %{bv2} %{EQ1} % ]
1257     #R #EQR * whd in ⊢ (??%% → ?); #EQ1 #EQ2 destruct
1258     %{(hwreg_retrieve (regs … st2) R)} % [2: %]
1259     whd in match set_regs; normalize nodelta
1260     >hwreg_retrieve_hwregstore_miss [%] % #EQ destruct
1261     lapply(Hr … EQR) >live_r1 *
1262   ]
1263]
1264% [2: assumption] % [2: assumption ] % [2: assumption] cases daemon (*TODO*)
1265qed.
1266
1267lemma beloadv_ok_bestorev_ok :
1268∀m,ptr,bv,bv'.beloadv m ptr = return bv →
1269∃m'.bestorev m ptr bv' = return m'.
1270cases daemon (*TODO*)
1271qed.
1272
1273include alias "arithmetics/nat.ma".
1274
1275lemma vertex_retrieve_write_decision_commute :
1276∀fix_comp,colour,prog,color_fun,live_fun.
1277∀init_regs : (block → list register).∀f_lbls,f_regs.∀f : ident.
1278∀fn : joint_closed_internal_function ERTL (prog_names … prog).
1279∀pc.
1280let m1 ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in
1281let stacksize ≝ lookup_stack_cost … m1 in 
1282fetch_internal_function … (joint_globalenv ERTL_semantics prog stacksize)
1283 (pc_block pc) = return 〈f,fn〉→
1284 let init ≝ translate_data fix_comp colour in
1285(∀v.∀R. color_fun v = decision_colour R → R = RegisterDPL ∨ R = RegisterDPH → ¬ live_fun v) →
1286bool_to_Prop (¬ live_fun (inr ?? RegisterDPL)) →
1287bool_to_Prop (¬ live_fun (inr ?? RegisterDPH)) →
1288(∀v.∀n : ℕ.color_fun v = decision_spill n → le n (joint_if_stacksize … fn)) →
1289gen_preserving ?? gen_res_preserve ????
1290     (λx,y.gen_state_rel fix_comp colour prog init_regs f_lbls f_regs live_fun
1291             color_fun pc (\snd (\fst x)) (\snd (\fst y)) ∧
1292           (\fst (\fst x)) = sigma_beval prog stacksize init init_regs f_lbls f_regs (\fst (\fst y)) ∧
1293           (\snd x) ≠ (inr ?? RegisterCarry) ∧ bool_to_Prop(live_fun (\snd x)) ∧
1294           (\snd y) = (color_fun (\snd x)) ∧
1295           (∃bv'.ertl_vertex_retrieve (regs … (\snd (\fst x))) (\snd x) = return bv') ∧
1296           (∀v'.v' ≠ (\snd x) → bool_to_Prop (live_fun v') → color_fun v' = (\snd y) → 
1297                False))
1298     (gen_state_rel fix_comp colour prog init_regs f_lbls f_regs
1299         (update_fun … eq_vertex live_fun (inr ?? RegisterCarry) false)
1300         color_fun pc) …
1301     (λx.return ertl_vertex_store (\snd x) (\fst (\fst x)) (\snd (\fst x)))
1302     (λx.write_decision (joint_if_local_stacksize ?? fn) (\snd x) (\fst (\fst x)) (\snd (\fst x))).
1303#fix_comp #colour #prog #color_fun #live_fun #init_regs #f_lbls #f_regs #f #fn #pc
1304#EQfn #Hdpl_dph #dpl_dead #dph_dead #Hspill ** #bv1 #st1 * #r ** #bv2 #st2 #d ******* #f1 * #fn1 * #sszie **
1305>EQfn whd in ⊢ (??%% → ?); #EQ destruct(EQ) #EQsszie inversion(st_frms …) [1,3: #_ *]
1306#frames #EQframes normalize nodelta ****** #Hmem #Hframes #Hhw #His #Hcarry #Hstack
1307* #sp *** change with (hwreg_retrieve_sp ?) in ⊢ (??%? → ?); #EQsp #H1 #H2 #Hps #EQ destruct(EQ)
1308[ #_ | * #r_nocarry ] #live_r #EQ destruct(EQ) * #bv' #EQbv' #Hinterf #st1' whd in ⊢ (??%% → ?);
1309whd in match ertl_vertex_store; normalize nodelta #EQ destruct(EQ)
1310[ cases(Hps … EQbv') [3: % [ assumption | %] |*:] #bv'' inversion(color_fun …)
1311  [ #n | #R ] #EQcol normalize nodelta *
1312  [ #H lapply(opt_eq_from_res ???? H) -H #EQbv''
1313  | whd in ⊢ (??%% → ?); #EQ1
1314  ]
1315  #EQ2 destruct
1316  [ @('bind_inversion EQsp) #ptr #EQptr @match_reg_elim #prf whd in ⊢ (??%% → ?); #EQ destruct
1317    cases(shift_pointer_commute (bitvector_of_nat 16 (joint_if_local_stacksize … fn1 +n))
1318                (carry … st2) … 
1319                〈hwreg_retrieve (regs LTL_semantics st2) RegisterSPL,
1320                 hwreg_retrieve (regs LTL_semantics st2) RegisterSPH〉 …)
1321    [3: %
1322    |5: >EQptr in ⊢ (??%?); >m_return_bind whd in match xpointer_of_pointer; normalize nodelta
1323        @match_reg_elim [2: >prf in ⊢ (% → ?); #EQ destruct] #prf' >m_return_bind %
1324    |*:
1325    ]
1326    #ptr1 @pair_elim #x1 #x2 #EQx1x2 * #H @('bind_inversion H) -H #x1' #EQx1'
1327    #H @('bind_inversion H) -H #x2' #EQx2' #EQptr1 #EQ destruct(EQ)
1328    cases(beloadv_ok_bestorev_ok … bv2 … EQbv'') #m' #EQm'
1329    % [2: %
1330          [ whd in match write_decision; normalize nodelta
1331            >EQx1x2 in ⊢ (??%?); normalize nodelta >m_return_bind
1332            >m_return_bind >EQx1' in ⊢ (??%?); >m_return_bind
1333            >EQx2' in ⊢ (??%?); >m_return_bind >EQptr1 in ⊢ (??%?);
1334            >m_return_bind >EQm' in ⊢ (??%?); >m_return_bind %
1335          | whd %{f1} %{fn1} %{sszie} % [ % assumption ] >EQframes normalize nodelta
1336            %
1337            [2: %{(«ptr,prf»)} %
1338                [ % [2: assumption] % [2: assumption]
1339                change with (hwreg_retrieve_sp ?) in ⊢ (??%?); whd in match set_m;
1340                whd in match set_regs; normalize nodelta
1341                >hwreg_retrieve_sp_insensitive_to_regstore
1342                [ >hwreg_retrieve_sp_insensitive_to_regstore [assumption]]
1343                % normalize #EQ destruct ] #r1 #d1 * whd in match update_fun;
1344                normalize nodelta #liv_r1 #EQ destruct(EQ) #val1
1345                cut(eq_identifier … r r1 ∨ ¬ eq_identifier … r r1)
1346                [ @eq_identifier_elim #_ // ] @eq_identifier_elim
1347                [ #EQ destruct(EQ) #_ whd in match reg_retrieve; whd in match reg_store;
1348                  normalize nodelta >lookup_add_hit whd in ⊢ (??%% → ?); #EQ destruct
1349                  %{bv2} >EQcol normalize nodelta % [2: %] whd in match set_m; whd in match set_regs;
1350                  normalize nodelta >beloadv_bestorev_hit [% | @EQm' |*:]
1351                | #r_neq_r1 #_ whd in match reg_retrieve; whd in match reg_store;
1352                  normalize nodelta >lookup_add_miss
1353                  [2: % #EQ destruct cases r_neq_r1 #H @H %]
1354                  change with (ps_reg_retrieve ??) in ⊢ (??%? → ?);
1355                  #EQval1 cases(Hps … EQval1) [3: % [ assumption | %] |*:]
1356                  #val2 inversion(color_fun ?) [ #n1 | #R1 ] #col_r1 normalize nodelta *
1357                  [ #H lapply(opt_eq_from_res ???? H) -H #EQval2 | whd in ⊢ (??%% → ?); #EQ1 ]
1358                  #EQ2 %{val2} destruct %
1359                  [2,4: % |3: >hwreg_retrieve_hwregstore_miss [ >hwreg_retrieve_hwregstore_miss [%]]
1360                  % #EQ destruct(EQ) lapply(Hdpl_dph … col_r1 ?) [1,3: [ %2 | %] %]
1361                  >liv_r1 * ]
1362                  whd in match set_m; whd in match set_regs; normalize nodelta
1363                  cut(eqb … n n1 ∨ ¬ eqb … n n1) [ @eqb_elim #_ //]
1364                  @eqb_elim
1365                  [ #EQ destruct(EQ) #_ >(beloadv_bestorev_hit …  EQm')
1366                    whd in ⊢ (??%%); @eq_f
1367                    cases(Hinterf (inl ?? r1) ? liv_r1 ?)
1368                    [ % #EQ destruct cases r_neq_r1 #H @H %
1369                    | >EQcol >col_r1 %
1370                    ]
1371                  | * #n_no_n1 #_ >(beloadv_bestorev_miss … EQm')
1372                    [ >EQval2 % ]
1373                    % #ABS @n_no_n1
1374                    @(injective_plus_r (joint_if_local_stacksize … fn1))
1375                    @(eq_bitvector_of_nat_to_eq … (shift_pointer_injective … ABS))
1376                    whd change with (plus 1 ?) in ⊢ (?%?);
1377                    @monotonic_le_plus_r @(transitive_le … H1)
1378                    [ cut (joint_if_local_stacksize … fn1 + n ≤ sszie)
1379                      [ cases daemon (*TODO an invariant to be added*) ]
1380                      | cut (joint_if_local_stacksize … fn1 + n1 ≤ sszie)
1381                      [ cases daemon (*TODO an invariant to be added*) ]
1382                    ]
1383                    #H2 @(transitive_le … H2) @le_plus_n   
1384                  ]
1385                ]
1386            | % [2: assumption ] % [2: *] % [2: assumption] %
1387              [2: % [ >(proj1 … Hhw) >hwreg_retrieve_sp_insensitive_to_regstore
1388                      [ >hwreg_retrieve_sp_insensitive_to_regstore [%]] normalize % #EQ destruct]
1389                    #r1 * #r1_nocarry whd in match update_fun; normalize nodelta @eq_vertex_elim
1390                    [ #EQ @⊥ destruct(EQ) @r1_nocarry %] #_ normalize nodelta
1391                    #live_r1 #r1_noundef inversion(color_fun ?)
1392                    [ #n1 | #r1'] #col_r1 normalize nodelta
1393                    [ >hwreg_retrieve_sp_insensitive_to_regstore
1394                      [ >hwreg_retrieve_sp_insensitive_to_regstore ]
1395                      [2,3,4,5: normalize % #EQ destruct]
1396                      >EQsp normalize nodelta whd in match set_m; normalize nodelta
1397                      cases daemon (*TODO*)
1398                    | >hwreg_retrieve_hwregstore_miss
1399                      [ >hwreg_retrieve_hwregstore_miss ] [2,3: % #EQ destruct(EQ)
1400                      lapply(Hdpl_dph … col_r1 ?) [1,3: [ %2 | % ] %] >live_r1 * ]
1401                      lapply(proj2 … Hhw r1 … live_r1 r1_noundef) [% assumption]
1402                      >col_r1 normalize nodelta #H @H
1403                    ]
1404              | cases daemon (*TODO*)
1405              ]
1406            ]
1407       ]
1408    |
1409    ]
1410  |  cases daemon (*TODO*)   
1411  ]
1412| cases daemon (*TODO*)
1413]
1414qed.
1415
1416xxxxxxx     
1417                         @transitive_le\
1418                       
1419                       
1420                         check plus lapply injective_S whd in match injective;
1421                        normalize nodelta change with(plus ? 1 ≤ 2 ^16); check injective_plus_l
1422                 
1423               
1424           
1425 
1426 
1427
1428   %
1429  [2,4: %
1430        [1,3: whd in match write_decision; normalize nodelta [2: %] @pair_elim
1431              #h_l #h_h #EQh >m_return_bind >m_return_bind
1432              @('bind_inversion EQsp) #ptr #EQptr @match_reg_elim #prf whd in ⊢ (??%% → ?);
1433              #EQ destruct(EQ)
1434              cases(shift_pointer_commute (bitvector_of_nat 16 (joint_if_local_stacksize … fn1 +n))
1435                (carry … st2) … 
1436                〈hwreg_retrieve (regs LTL_semantics st2) RegisterSPL,
1437                 hwreg_retrieve (regs LTL_semantics st2) RegisterSPH〉 …)
1438              [
1439         
1440 inversion(color_fun …) [1,3: #n |*: #R ] #EQcol %
1441[2: %
1442    [ whd in match write_decision; normalize nodelta
1443
1444
1445[ cases(Hps … EQbv')
1446
1447
1448
1449#Rst1st2 ****
1450#EQ destruct(EQ) [ #_ | * #r_nocarry] #live_r #EQ destruct(EQ) #Hinterf #st1'
1451whd in ⊢ (??%% → ?); #EQ destruct(EQ) cases Rst1st2
1452[ cases(Hps … r)
1453
1454
1455
1456
1457
1458
1459
1460(*
1461lemma update_color_lemma :
1462∀fix_comp,colour,prog,init.
1463∀color_f : ((Σb:block.block_region b=Code) → option (list register → vertex → decision)).
1464∀live_f : ((Σb:block.block_region b=Code)→ option (list register → live_type)).
1465∀color_fun : (joint_closed_internal_function ERTL (prog_names … prog) → vertex → decision).
1466∀live_fun : (joint_closed_internal_function ERTL (prog_names … prog) → label → vertex → bool).
1467let p_out ≝ (\fst (\fst (ertl_to_ltl fix_comp colour prog))) in
1468let m1 ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in
1469let stacksizes ≝ lookup_stack_cost … m1 in
1470∀init_regs,f_lbls,f_regs,pc,st1,st2.
1471∀v,new_col.∀f.∀fn : joint_closed_internal_function ? (prog_names … prog).
1472 fetch_internal_function … (joint_globalenv ERTL_semantics prog stacksizes)
1473 (pc_block pc) = return 〈f,fn〉 →
1474 gen_state_rel prog stacksizes init color_f live_f color_fun live_fun init_regs
1475 f_lbls f_regs pc st1 st2 →   
1476if live_fun fn (point_of_pc ERTL_semantics pc) v
1477then ∀bv.
1478      ertl_vertex_retrieve (regs ? st1) v = return bv →
1479      match new_col with
1480      [ decision_colour R ⇒ sigma_beval prog stacksizes init init_regs f_lbls f_regs
1481                           (hwreg_retrieve (regs … st2) R) = bv
1482      | decision_spill n ⇒ ∃sp.hwreg_retrieve_sp (regs … st2) = return sp ∧
1483                         ∃bv'.beloadv (m … st2)
1484                               (shift_pointer ? sp
1485                               (bitvector_of_nat 16 (joint_if_local_stacksize … fn + n))) = return bv'
1486                             ∧ sigma_beval prog stacksizes init init_regs f_lbls f_regs bv' = bv                           
1487      ]
1488else True →
1489gen_state_rel prog stacksizes init color_f live_f
1490 (λfn.update_fun ?? eq_vertex (color_fun fn) v new_col) live_fun init_regs
1491 f_lbls f_regs pc st1 st2.
1492cases daemon qed.
1493
1494lemma update_live_fun_lemma :
1495∀fix_comp,colour,prog,init.
1496∀color_f : ((Σb:block.block_region b=Code) → option (list register → vertex → decision)).
1497∀live_f : ((Σb:block.block_region b=Code)→ option (list register → live_type)).
1498∀color_fun : (joint_closed_internal_function ERTL (prog_names … prog) → vertex → decision).
1499∀live_fun : (joint_closed_internal_function ERTL (prog_names … prog) → label → vertex → bool).
1500let p_out ≝ (\fst (\fst (ertl_to_ltl fix_comp colour prog))) in
1501let m1 ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in
1502let stacksizes ≝ lookup_stack_cost … m1 in
1503∀init_regs,f_lbls,f_regs,pc,st1,st2.
1504∀v,new_live.∀f.∀fn : joint_closed_internal_function ? (prog_names … prog).
1505 fetch_internal_function … (joint_globalenv ERTL_semantics prog stacksizes)
1506 (pc_block pc) = return 〈f,fn〉 →
1507 gen_state_rel prog stacksizes init color_f live_f color_fun live_fun init_regs
1508 f_lbls f_regs pc st1 st2 →   
1509if new_live
1510then if live_fun fn (point_of_pc ERTL_semantics pc) v
1511     then True
1512     else ∀bv.ertl_vertex_retrieve (regs … st1) v = return bv →
1513          match color_fun fn v with
1514          [ decision_colour R ⇒ sigma_beval prog stacksizes init init_regs f_lbls f_regs
1515                                (hwreg_retrieve (regs … st2) R) = bv
1516          | decision_spill n ⇒ ∃sp.hwreg_retrieve_sp (regs … st2) = return sp ∧
1517                               ∃bv'.beloadv (m … st2)
1518                               (shift_pointer ? sp
1519                               (bitvector_of_nat 16 (joint_if_local_stacksize … fn + n))) = return bv'
1520                               ∧ sigma_beval prog stacksizes init init_regs f_lbls f_regs bv' = bv
1521          ]
1522else True →
1523gen_state_rel prog stacksizes init color_f live_f color_fun
1524 (λfn.update_fun ?? (eq_identifier …) (live_fun fn) (point_of_pc ERTL_semantics pc)
1525     (update_fun ?? eq_vertex (live_fun fn (point_of_pc ERTL_semantics pc)) v new_live))
1526 init_regs f_lbls f_regs pc st1 st2.
1527cases daemon qed.  *)
1528
1529
1530
1531
1532
1533
1534
1535
1536(*
1537lemma state_rel_insensitive_to_forbidden_Reg :
1538 ∀fix_comp,colour,prog,init_regs,f_lbls,f_regs,pc.
1539 let m ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in
1540 let stacksizes ≝ lookup_stack_cost … m in
1541 ∀f.∀fn : joint_closed_internal_function ? (prog_names … prog).
1542 fetch_internal_function … (joint_globalenv ERTL_semantics prog stacksizes)
1543 (pc_block pc) = return 〈f,fn〉 →
1544 ∀st1 : state ERTL_state.∀st2.
1545 ∀r,bv. Exists … (λr1.r = r1) RegisterAlwaysDead →
1546 state_rel fix_comp colour prog init_regs f_lbls f_regs pc st1 st2 →
1547 state_rel fix_comp colour prog init_regs f_lbls f_regs pc st1
1548  (set_regs LTL_LIN_state (hwreg_store r bv (regs … st2)) st2).
1549#fix_comp #colour #prog #init_regs #f_lbls #f_regs #pc #f #fn #EQfn #st1 #st2 #r
1550#bv * [2: * [2: * [2: * [2: * [2: * ]]]] ] #EQ destruct(EQ) whd in match state_rel;
1551whd in match gen_state_rel; normalize nodelta * #f1 * #fn1 * >EQfn whd in ⊢ (??%% → ?);
1552#EQ destruct(EQ) cases(st_frms ??) [1,3,5,7,9: *] #frames normalize nodelta ***** 
1553#Hmem #Hframes #Hhw_rel #His #Hcarry * #sp * #EQsp #Hpsd_reg %{f1} %{fn1} %{(refl …)} %
1554[1,3,5,7,9: % [2,4,6,8,10: assumption ] % [2,4,6,8,10: assumption] % [1,3,5,7,9: % [1,3,5,7,9: assumption ]]]
1555[1,2,3,4,5: whd in match set_regs; normalize nodelta lapply Hframes whd in match frames_relation;
1556  normalize nodelta letin ID ≝ (λx : decision.x)
1557  [ cut((∀r.r ≠ RegisterST1 → ID (decision_colour r) ≠ RegisterST1) ∧ ∀n.ID (decision_spill n) = decision_spill n)
1558  | cut((∀r.r ≠ RegisterDPH → ID (decision_colour r) ≠ RegisterDPH) ∧ ∀n.ID (decision_spill n) = decision_spill n)
1559  | cut((∀r.r ≠ RegisterDPL → ID (decision_colour r) ≠ RegisterDPL) ∧ ∀n.ID (decision_spill n) = decision_spill n)
1560  | cut((∀r.r ≠ RegisterB → ID (decision_colour r) ≠ RegisterB) ∧ ∀n.ID (decision_spill n) = decision_spill n) 
1561  | cut((∀r.r ≠ RegisterA → ID (decision_colour r) ≠ RegisterA) ∧ ∀n.ID (decision_spill n) = decision_spill n)
1562  ]
1563  [1,3,5,7,9: % try (#n %) #r normalize * #H %  #EQ destruct @H % ]
1564  generalize in match ID; elim frames [1,3,5,7,9: #f #_ #_ @I]
1565  #hd #tl #IH #acc #acc_spec * #f2 * #fn2 ** #EQfn2 #Hframe #Htl %{f2} %{fn2} %
1566  [2,4,6,8,10: @IH try assumption % 
1567    [1,3,5,7,9: #r #Hr whd in match callee_saved_remap; normalize nodelta
1568      cases(position_of ???) normalize nodelta [1,3,5,7,9: @((proj1 ?? acc_spec) r Hr) ]
1569      #x cases(nth_opt ???) normalize nodelta [1,3,5,7,9: @((proj1 ?? acc_spec) r Hr) ]
1570      #r1 >EQfn2 normalize nodelta inversion(colouring  ???)
1571      [1,3,5,7,9: #m |*: #R1 ] #EQcolouring
1572      [1,2,3,4,5: >(proj2 ?? acc_spec) % #EQ destruct
1573      |*: @((proj1 ?? acc_spec) R1 ?)
1574         cases(colouring_is_never_forbidden … EQfn2 … EQcolouring) #H1
1575         [5: #_ assumption] * #H [4: #_ assumption] * #H2 [3: #_ assumption] *
1576         #H3 [2: #_ assumption ] * #_ * #_ * #_ * #H4 #_ @H4
1577      ]
1578    |*: #z whd in match callee_saved_remap; normalize nodelta @(proj2 … acc_spec)
1579    ]
1580  |*: %{EQfn2} #r #d * normalize nodelta @andb_elim @if_elim #r_live [2,4,6,8,10: *]
1581     #_ #EQd #bv #EQbv cases(Hframe … d … EQbv)
1582     [2,4,6,8,10: % [2,4,6,8,10: assumption] @andb_Prop try @I assumption]
1583     #bv1 * #Hbv1 #EQ destruct(EQ) %{bv1} % [2,4,6,8,10: %] cases d in Hbv1 EQd;
1584     normalize nodelta [1,3,5,7,9: #n #H #_ @H] #R1 whd in ⊢ (??%% → ?); #EQ destruct(EQ)
1585     #EQd >hwreg_retrieve_hwregstore_miss % #EQ destruct(EQ)
1586     inversion(colouring ???) in EQd; [1,3,5,7,9: #n #_ >(proj2 … acc_spec) #EQ destruct]
1587     #R2 #EQr2 #ABS cases(colouring_is_never_forbidden … EQfn2 … EQr2)
1588     [5: #H #_ |*: #_ * [4: #H #_ |*: #_ * [3: #H #_ |*: #_ * [2: #H #_ | #_ * #_ * #_ * #_ * #H #_ ] ] ]]
1589     cases((proj1 … acc_spec) R2 H) #H1 @H1 <ABS %
1590  ]
1591|6,7,8,9,10: %
1592  [1,3,5,7,9: whd in match hwreg_retrieve_sp in ⊢ (???%); normalize nodelta
1593    whd in match set_regs; normalize nodelta >hwreg_retrieve_hwregstore_miss
1594    [2,4,6,8,10: normalize % #EQ destruct] >hwreg_retrieve_hwregstore_miss
1595    [2,4,6,8,10: normalize % #EQ destruct] @(proj1 … Hhw_rel)
1596  |*: whd in match set_regs; normalize nodelta #R @andb_elim @if_elim
1597    #R_live [2,4,6,8,10: *] #H
1598    cases (all_All … (λx.¬eq_Register R x) RegisterAlwaysDead) #H1 #H2
1599    lapply(H1 H) -H1 -H * @eq_Register_elim #R_noA ** @eq_Register_elim #R_noB **
1600    @eq_Register_elim #R_noDPL ** @eq_Register_elim #R_noDPH ** @eq_Register_elim #R_noST1 * #_
1601    >hdw_same_colouring normalize nodelta >hwreg_retrieve_hwregstore_miss
1602    [2,4,6,8,10: assumption] lapply((proj2 … Hhw_rel) R ?) [2,4,6,8,10: >hdw_same_colouring #H @H]
1603    @andb_Prop [1,3,5,7,9: assumption] @H2 %
1604    [1,3,5,7,9: @eq_Register_elim try (#_ @I) #EQ >EQ in R_noA; * #H @H %]
1605    % [1,3,5,7,9: @eq_Register_elim try (#_ @I) #EQ >EQ in R_noB; * #H @H %]
1606    % [1,3,5,7,9: @eq_Register_elim try (#_ @I) #EQ >EQ in R_noDPL; * #H @H %]
1607    % [1,3,5,7,9: @eq_Register_elim try (#_ @I) #EQ >EQ in R_noDPH; * #H @H %]
1608    % [1,3,5,7,9: @eq_Register_elim try (#_ @I) #EQ >EQ in R_noST1; * #H @H %] @I
1609  ]
1610|11,12,13,14,15: %{sp} %
1611  [1,3,5,7,9: whd in ⊢ (??%?); whd in match set_regs; normalize nodelta
1612    >hwreg_retrieve_hwregstore_miss [2,4,6,8,10: normalize % #EQ destruct]
1613    >hwreg_retrieve_hwregstore_miss [2,4,6,8,10: normalize % #EQ destruct] assumption
1614  |*: #r #d * normalize nodelta @andb_elim @if_elim #r_live * #EQd cases d in EQd;
1615    [1,3,5,7,9: #n |*: #R ] #EQcol normalize nodelta
1616    [1,2,3,4,5: whd in match (m ??); @(Hpsd_reg r (decision_spill n)) % [2,4,6,8,10: assumption]
1617       @andb_Prop try assumption @I
1618    |*: >hwreg_retrieve_hwregstore_miss
1619       [1,3,5,7,9: @(Hpsd_reg r (decision_colour R)) % [2,4,6,8,10: assumption] @andb_Prop try assumption @I]
1620       cases(colouring_is_never_forbidden … EQfn … EQcol) [5: #H #_ assumption]
1621       #_ * [4: #H #_ assumption] #_ * [3: #H #_ assumption] #_ * [2: #H #_ assumption ]
1622       #_ * #_ * #_ * #_ * #H #_ assumption
1623    ]
1624  ]
1625]
1626qed.
1627*)
1628
1629
1630
1631
1632
1633(*
1634[ whd in match read_arg_decision; normalize nodelta >m_return_bind
1635  whd in match write_decision; normalize nodelta @eq_Register_elim
1636  [ #EQ destruct(EQ) whd in match set_regs; normalize nodelta
1637    #st1'
1638 * [ #src_spill | #src_col ] * [1,3: #dst_spill |*: #dst_col ] #f #fn
1639#EQfn #v #EQsrc #v_live #Hsrc #st1' #st2 *** #Rst1st2 #Hv #Hspill #Hinterf
1640>move_spec [2,4,6,8: assumption] #st1 whd in ⊢ (??%% → ?); #EQ destruct(EQ)
1641normalize nodelta
1642[ @eqb_elim normalize nodelta
1643  [ #EQ destruct(EQ) %{st2} %{(refl …)} @(gen_state_rel_ext_color_fun … EQfn … Rst1st2)
1644    #v' whd in match update_fun; normalize nodelta @eq_vertex_elim [2: #_ %]
1645    #EQ destruct assumption ]
1646  normalize nodelta in Hspill; cases Rst1st2
1647  #f1 * #fn1 * >EQfn whd in ⊢ (??%% → ?); #EQ destruct(EQ)
1648  inversion(st_frms ??) [1,3: #_ *] #frames #EQframes normalize nodelta *****
1649  #Hmem #Hframes #Hhw_reg #His #Hcarry * #ptr * #EQptr #Hpsd_reg
1650  cases v in v_live Hv EQsrc Hinterf; -v [ #r | #R ] #Hlive normalize nodelta
1651  [ * #bv #EQbv | #_ ] #EQsrc #Hinterf
1652  [ cases(Hpsd_reg … EQbv) [3: % assumption |2:] #bv' normalize nodelta *
1653  #H lapply(opt_eq_from_res ???? H) -H #EQbv' #EQ destruct(EQ) #Hsrc_dst
1654  cases(shift_pointer_commute
1655          (bitvector_of_nat 8 ((joint_if_local_stacksize … fn1) + src_spill))
1656          (carry … st2) …
1657          〈hwreg_retrieve (regs LTL_semantics st2) RegisterSPL,
1658           hwreg_retrieve (regs LTL_semantics st2) RegisterSPH〉 …)
1659  [5: lapply EQptr change with (hwreg_retrieve_sp ?) in match (sp ??);
1660      whd in match hwreg_retrieve_sp; normalize nodelta #H @('bind_inversion H)
1661      #ptr1 #EQptr1 #H >EQptr1 in ⊢ (??%?); >m_return_bind
1662      whd in match xpointer_of_pointer; normalize nodelta
1663      >H >m_return_bind %
1664  |3: %
1665  |*:
1666  ]
1667  #ptr1 * #H @('bind_inversion H) -H #val1 #EQval1 #H @('bind_inversion H) -H
1668  #val2 #EQval2 #EQptr1 #EQ destruct(EQ)
1669  cases(shift_pointer_commute
1670         (bitvector_of_nat 8 ((joint_if_local_stacksize … fn1) + dst_spill))
1671          (\snd  val2) …
1672          〈hwreg_retrieve (regs LTL_semantics st2) RegisterSPL,
1673           hwreg_retrieve (regs LTL_semantics st2) RegisterSPH〉 …)
1674  [5: lapply EQptr change with (hwreg_retrieve_sp ?) in match (sp ??);
1675      whd in match hwreg_retrieve_sp; normalize nodelta #H @('bind_inversion H)
1676      #ptr1 #EQptr1 #H >EQptr1 in ⊢ (??%?); >m_return_bind
1677      whd in match xpointer_of_pointer; normalize nodelta
1678      >H >m_return_bind %
1679  |3: %
1680  |*:
1681  ]
1682  #ptr2 * #H @('bind_inversion H) -H #val3 #EQval3 #H @('bind_inversion H) -H
1683  #val4 #EQval4 #EQptr2 #EQ destruct(EQ) %
1684  [2: %
1685      [ whd in match read_arg_decision; normalize nodelta >m_return_bind >m_return_bind
1686        >EQval1 in ⊢ (??%?); >m_return_bind >EQval2 in ⊢ (??%?);
1687        >m_return_bind >EQptr1 in ⊢ (??%?); >m_return_bind >EQbv' in ⊢ (??%?);
1688        >m_return_bind whd in match set_regs; whd in match set_carry; normalize nodelta
1689        whd in match write_decision; normalize nodelta >m_return_bind >m_return_bind
1690        >hwreg_retrieve_hwregstore_miss [2: normalize % #EQ destruct]
1691        >hwreg_retrieve_hwregstore_miss in ⊢ (??(????(?????%?)?)?);
1692        [2: normalize % #EQ destruct]
1693        >hwreg_retrieve_hwregstore_miss in ⊢ (??(????(?????%?)?)?);
1694        [2: normalize % #EQ destruct]
1695        >hwreg_retrieve_hwregstore_miss [2: normalize % #EQ destruct]
1696        >hwreg_retrieve_hwregstore_miss [2: normalize % #EQ destruct]
1697        >hwreg_retrieve_hwregstore_miss [2: normalize % #EQ destruct]
1698        >EQval3 in ⊢ (??%?); >m_return_bind >EQval4 in ⊢ (??%?);
1699        >m_return_bind >EQptr2 in ⊢ (??%?); >m_return_bind
1700        >(opt_to_opt_safe … (Hspill … EQptr bv')) in ⊢ (??%?); >m_return_bind
1701        whd in match set_m; normalize nodelta whd in match set_regs; normalize nodelta
1702        whd in match set_carry; normalize nodelta <commute_if in ⊢ (??%?); %
1703      | %{f1} %{fn1} %{EQfn} >EQframes normalize nodelta %
1704        [2: %{ptr} %
1705        [ change with (hwreg_retrieve_sp ?) in match (sp ??); @if_elim #c_live
1706          whd in match hwreg_retrieve_sp; normalize nodelta
1707          [ >hwreg_retrieve_insensitive_to_set_other  >hwreg_retrieve_insensitive_to_set_other ]
1708          >hwreg_retrieve_hwregstore_miss [2,4: normalize % #EQ destruct]
1709          whd in ⊢ (??%?);
1710          try >hwreg_retrieve_hwregstore_miss in ⊢ (??(match (?(???%?)) with [ _ ⇒ ? | _ ⇒ ? ])?);
1711          [1,3: try >hwreg_retrieve_hwregstore_miss in ⊢ (??(match (?(???%?)) with [ _ ⇒ ? | _ ⇒ ? ])?);
1712          [1,3: try >hwreg_retrieve_hwregstore_miss in ⊢ (??(match (?(???%?)) with [ _ ⇒ ? | _ ⇒ ? ])?);
1713          [1,3: try >hwreg_retrieve_hwregstore_miss in ⊢ (??(match (?(???%?)) with [ _ ⇒ ? | _ ⇒ ? ])?);
1714          [1,3: try >hwreg_retrieve_hwregstore_miss in ⊢ (??(match (?(???%?)) with [ _ ⇒ ? | _ ⇒ ? ])?);
1715          [1,3: try >hwreg_retrieve_hwregstore_miss in ⊢ (??(match (?(????%)) with [ _ ⇒ ? | _ ⇒ ? ])?);
1716             [1,3: try >hwreg_retrieve_hwregstore_miss in ⊢ (??(match (?(????%)) with [ _ ⇒ ? | _ ⇒ ? ])?);
1717          [1,3: try >hwreg_retrieve_hwregstore_miss in ⊢ (??(match (?(????%)) with [ _ ⇒ ? | _ ⇒ ? ])?);
1718          [1,3: try >hwreg_retrieve_hwregstore_miss in ⊢ (??(match (?(????%)) with [ _ ⇒ ? | _ ⇒ ? ])?);
1719          [1,3: try >hwreg_retrieve_hwregstore_miss in ⊢ (??(match (?(????%)) with [ _ ⇒ ? | _ ⇒ ? ])?);
1720          [1,3: try >hwreg_retrieve_hwregstore_miss in ⊢ (??(match (?(????%)) with [ _ ⇒ ? | _ ⇒ ? ])?);
1721          [1,3: assumption ]]]]]]]]]]] normalize % #EQ destruct
1722        | cases carry_live -carry_live normalize nodelta #r1 #d1 * #r1_live
1723          whd in match update_fun; normalize nodelta @eq_vertex_elim
1724          [1,3: #EQ destruct(EQ) normalize nodelta #EQ destruct(EQ) normalize nodelta
1725            #bv1 change with (ps_reg_retrieve ??) in ⊢ (??%? → ?); >EQbv whd in ⊢ (??%% → ?);
1726            #EQ destruct(EQ) %{bv'} % [2,4: %] @opt_safe_elim #m' #EQm'
1727            >(beloadv_bestorev_hit … EQm') %         
1728          |*: #Hdiff normalize nodelta #EQ destruct(EQ) inversion(color_fun ???)
1729             [1,3: #n1 #EQn1 normalize nodelta #bv1 #EQbv1
1730               letin ptr1 ≝ (shift_pointer ? ptr (bitvector_of_nat ? ((joint_if_local_stacksize … fn1) + dst_spill)))
1731               letin ptr2≝ (shift_pointer ? ptr (bitvector_of_nat ? ((joint_if_local_stacksize … fn1) + n1)))
1732               cut(bool_to_Prop(eq_pointer … ptr1 ptr2) ∨ bool_to_Prop (¬ eq_pointer … ptr1 ptr2))
1733               [1,3: @eq_pointer_elim #_ [1,3: %% |*: %2 %]] * @eq_pointer_elim
1734               #Hptr * 
1735               [1,3: %{bv'} % [1,3: @opt_safe_elim #m' >Hptr #EQm' >(beloadv_bestorev_hit … EQm') %]
1736                 normalize nodelta in Hinterf;
1737                 cut(∀A.∀x,y.m_return Res A x = m_return Res A y → x = y)
1738                 [1,3: #A #x #y whd in ⊢ (??%% → ?); #EQ destruct(EQ) %] #H @H -H
1739                 <EQbv <EQbv1
1740                 cut(n1 = dst_spill) [1,3: cases daemon (*TODO*) ] #EQ destruct(EQ)
1741                 lapply(Hinterf (inl ?? r1) ? r1_live EQn1) [1,3: % #EQ destruct cases Hdiff #H @H %]
1742                 whd in match ertl_vertex_retrieve; normalize nodelta #H >H %
1743               |*: cases(Hpsd_reg … EQbv1) [3,6: % try assumption |*:]
1744                 #bv2 normalize nodelta * #H lapply(opt_eq_from_res ???? H) -H
1745                 #EQbv2 #EQ destruct(EQ) %{bv2} % try % @opt_safe_elim
1746                 #m' #EQm' >(beloadv_bestorev_miss … Hptr EQm') whd in match ptr2;
1747                 >EQbv2 %
1748               ]
1749             |*: cases daemon (*TODO*)       
1750             ]
1751          ]
1752        ]
1753      | cases daemon (*TODO*)
1754      ]
1755  ]]]] cases daemon (*TODO*) 
1756qed.*)
1757
1758lemma cond_commute :∀fix_comp,colour,prog,init_regs,f_lbls,f_regs.
1759let p_out ≝ (\fst (\fst (ertl_to_ltl fix_comp colour prog))) in
1760let m ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in
1761let n ≝ \snd (ertl_to_ltl fix_comp colour prog) in
1762let stacksizes ≝ lookup_stack_cost … m in
1763let init ≝ translate_data fix_comp colour in
1764cond_commutation_statement ERTL_semantics LTL_semantics prog stacksizes
1765 init init_regs
1766 f_lbls f_regs (state_rel fix_comp colour prog init_regs f_lbls f_regs)
1767 (state_pc_rel fix_comp colour prog init_regs f_lbls f_regs).
1768#fix_comp #colour #prog #init_regs #f_lbls #f_regs
1769whd in match cond_commutation_statement; normalize nodelta
1770#st1 #st2 #f #fn #r #ltrue #lfalse #bv #b * #Hbl #EQfetch
1771whd in match acca_retrieve; normalize nodelta
1772change with (ps_reg_retrieve ??) in ⊢ (??%? → ?);
1773#EQbv #EQb whd in match state_pc_rel; normalize nodelta **
1774whd in match state_rel; normalize nodelta * #f1 * #fn1 *
1775>(proj1 … (fetch_statement_inv … EQfetch)) whd in ⊢ (???% → ?); #EQ destruct(EQ)
1776#Rst1st2 #_ #_ #t_fn #_ #z1 #z2 #z3 #z4 #z5 #z6 #z7 #z8 whd #EQinit_regs
1777whd normalize nodelta %{(refl …)} #mid #_ <EQinit_regs
1778>map_eval_add_dummy_variance_id >move_spec normalize nodelta
1779[2: whd inversion(colouring …) normalize nodelta [#n #_ @I] #R
1780    #EQR
1781    cases(colouring_is_never_forbidden … (proj1 … (fetch_statement_inv … EQfetch)) … EQR)
1782    #_ * #_ * #H1 * #H2 #_ %{H1 H2} ]
1783cases(vertex_retrieve_read_arg_decision_commute … (proj1 … (fetch_statement_inv … EQfetch)) … (inl ?? r) … Rst1st2 …)
1784[2: *
1785   [ #r1 #R #EQR * #EQ destruct
1786     cases(colouring_is_never_forbidden … (proj1 … (fetch_statement_inv … EQfetch)) … EQR)
1787     #_ * #_ * * #H1 * * #H2 #_ @⊥ try( @H1 %) @H2 %
1788   | #R1 #R2 >hdw_same_colouring #EQ destruct * #EQ destruct cases(in_lattice …) %
1789   ]
1790|3,4: cases(in_lattice …) %
1791|6: % [2: %] % [ % #EQ destruct]
1792    >(all_used_are_live_before fix_comp … (proj2 … (fetch_statement_inv … EQfetch)))
1793    [% | % | @set_member_singl]
1794|8: whd in match ertl_vertex_retrieve; normalize nodelta >EQbv in ⊢ (??%?); %
1795|*:
1796]
1797* #bv' #st2' * #EQst2' * #EQ destruct(EQ) #Rst1st2' >EQst2' >m_return_bind >m_return_bind
1798>m_return_bind >m_return_bind
1799cases(state_rel_insensitive_to_dead_write_decision … (proj1 … (fetch_statement_inv … EQfetch)) … RegisterA … bv' … Rst1st2' … (refl …))
1800[2: %%
1801|3: * [#r #EQr cases(colouring_is_never_forbidden … (proj1 … (fetch_statement_inv … EQfetch)) … EQr) * #H @⊥ @H %
1802      | #R >hdw_same_colouring #EQ destruct(EQ) whd in match update_fun; normalize nodelta
1803        cases(in_lattice …) %
1804      ]
1805]
1806#st2'' * #EQst2'' #Rst1st2'' >EQst2'' inversion(colouring …) normalize nodelta
1807[ #n | #R] #EQcol <commute_if % [2,4: %{(refl …)} |*:] %
1808[1,3: %{f1} %{fn1} % [1,3: @if_elim #_ @(proj1 ?? (fetch_statement_inv … EQfetch)) ]
1809  cases Rst1st2'' #f2 * #fn2 * #ssize ** >(proj1 ?? (fetch_statement_inv … EQfetch))
1810  whd in ⊢ (??%% → ?); #EQ destruct #EQssize inversion(st_frms …) [1,3: #_ *]
1811  #frames #EQframes ****** #Hmem #Hframes #Hhw #His #_ #Hstack * #sp *** #EQsp
1812  #H1 #H2 #Hps %{f2} %{fn2} %{ssize} %
1813  [1,3: @if_elim #_ %{(proj1 … (fetch_statement_inv … EQfetch))} assumption]
1814  >EQframes normalize nodelta %
1815  [2,4: %{sp}
1816      [| @eq_Register_elim
1817         [ #EQ destruct(EQ)
1818           cases(colouring_is_never_forbidden …
1819                         (proj1 … (fetch_statement_inv … EQfetch)) … EQcol)
1820           * #ABS #_ @⊥ @ABS % ]
1821         #RnoA normalize nodelta ] %
1822      [2,4: #r1 #d1 * @andb_elim @if_elim <commute_if in ⊢ (% → ?);
1823            whd in match (pc_block ?); >point_of_pc_of_point #r1_live *
1824            [ <commute_if in ⊢ (% → ?); ] whd in match (pc_block ?); #EQ
1825            destruct(EQ) #v1 #EQv1 cases(Hps … EQv1)
1826            [3,6: % [2,4: %] whd in match update_fun; normalize nodelta
1827                  whd in match (livebefore ?????);
1828                  change with (stmt_at ??? (point_of_pc ERTL_semantics ?)) in
1829                           ⊢ (?(?(??match % with [_ ⇒ ? | _ ⇒ ? ])?));
1830                  >(proj2 … (fetch_statement_inv … EQfetch)) normalize nodelta
1831                  whd in match statement_semantics; normalize nodelta
1832                  @andb_Prop [2,4: @I]
1833                  @set_member_union1 @set_member_diff [2,4: @set_member_empty]
1834                  @(set_member_subset_if … r1_live)
1835                  lapply(included_livebefore_livebeafter_stmt_labels
1836                                 fix_comp … (init_regs (pc_block (pc … st1))) …
1837                                 (proj2 ?? (fetch_statement_inv … EQfetch))
1838                                 (if b then ltrue else lfalse) ?)
1839                   [1,3: cases b normalize nodelta
1840                          whd in match stmt_labels; whd in match stmt_explicit_labels;
1841                          whd in match step_labels; normalize nodelta
1842                          [1,3: >memb_cons [1,3: @I |*: @memb_hd] |*: >memb_hd @I ] ]
1843                   whd in match (l_included ???); cases(set_subset (identifier ?) ??)
1844                   [1,3: #_ @I] @if_elim **
1845            |*:
1846            ]
1847            #v1' inversion(colouring …) normalize nodelta
1848            [1,3: #n #EQn * #H1 #EQ destruct(EQ) %{v1'} % [2,4: %]
1849                  [ >(commute_if ????? (λx.m LTL_semantics x))
1850                    whd in match (m ??); @if_elim #_ ]
1851                  whd in match write_decision in EQst2''; normalize nodelta in EQst2'';
1852                  >m_return_bind in EQst2''; whd in ⊢ (??%% → ?); #EQ destruct(EQ)
1853                  assumption
1854            |*: #R #EQR * whd in ⊢ (??%% → ?); #EQ1 #EQ2 destruct(EQ1 EQ2)   
1855                %{(hwreg_retrieve (regs … st2'') R)} % [2,3,4: % ] 
1856                @if_elim #_ whd in match set_regs; normalize nodelta
1857                [ >hwreg_retrieve_insensitive_to_set_other ]
1858                >hwreg_retrieve_hwregstore_miss
1859                [1,3: whd in match write_decision in EQst2''; normalize nodelta in EQst2'';
1860                      >m_return_bind in EQst2''; whd in ⊢ (??%% → ?); #EQ destruct(EQ)
1861                      >hwreg_retrieve_hwregstore_miss [1,3: %] ]
1862                % #EQ destruct(EQ)
1863                cases(colouring_is_never_forbidden …
1864                         (proj1 … (fetch_statement_inv … EQfetch)) … EQR)
1865                * #ABS #_ @ABS %
1866            ]
1867      |*: % try % try assumption
1868          [1,3: change with (hwreg_retrieve_sp ?) in ⊢ (??%?);
1869                [ @if_elim #_ whd in match set_regs; normalize nodelta
1870                  [ >hwreg_retrieve_sp_insensitive_to_set_other ]
1871                  >hwreg_retrieve_sp_insensitive_to_regstore
1872                  [1,4: whd in match write_decision in EQst2'';
1873                        normalize nodelta in EQst2''; >m_return_bind in EQst2'';
1874                        whd in ⊢ (??%% → ?); #EQ destruct(EQ)
1875                        change with (hwreg_retrieve_sp ?) in EQsp : (??%?);
1876                        >hwreg_retrieve_sp_insensitive_to_regstore in EQsp;
1877                        [1,4: //]
1878                  ]
1879                  % normalize #EQ destruct
1880               | @eq_Register_elim [2: #_ assumption ] #EQ destruct(EQ)
1881                 cases(colouring_is_never_forbidden …
1882                         (proj1 … (fetch_statement_inv … EQfetch)) … EQcol)
1883                 * #ABS #_ @⊥ @ABS %
1884               ]
1885          |*:     
1886         
1887         
1888         
1889                         
1890cases(ps_reg_retrieve_hw_reg_retrieve_commute prog ???? init_regs f_lbls
1891f_regs f fn (pc … st1) ?????????)
1892[6: @(proj1 … (fetch_statement_inv … EQfetch))
1893|11: @Rst1st2
1894|9: @r
1895|12: % [ @andb_Prop [ @(all_used_are_live_before … (proj2 … (fetch_statement_inv … EQfetch))) // | @I ] | %]
1896|14: @EQbv
1897|*:
1898]
1899#bv1 * whd in match m_map; normalize nodelta #H @('bind_inversion H) -H
1900* #bv2 #st2' #EQst2' whd in ⊢ (??%% → ?); #EQ1 #EQ2  destruct(EQ1 EQ2)
1901(*letin after ≝ (λfn,callee.analyse_liveness fix_comp (prog_names … prog) fn callee)
1902letin before ≝ (λfn,callee.livebefore … fn callee (after fn callee))
1903letin live_fun ≝ (λfn,callee,l,v.in_lattice v ((before fn callee) l) ∧
1904                   match v with [ inl r ⇒ true
1905                | inr R ⇒ all … (λR'.¬ eq_Register R R') RegisterAlwaysDead
1906                ]) *)
1907letin aft ≝ (analyse_liveness fix_comp (prog_names … prog) fn (init_regs (pc_block (pc … st1))))
1908letin carry_lives ≝ (h_in_lattice RegisterCarry (aft (point_of_pc ERTL_semantics (pc … st1))))
1909letin color_of_r ≝ (colouring … (colour (prog_names … prog) fn aft (init_regs (pc_block (pc … st1))))(inl ?? r))
1910(*letin color_fun ≝ (λfn1,callee,v.colouring … (colour (prog_names … prog) fn1 aft callee) v) *)
1911cases(move_preserve fix_comp colour prog (translate_data fix_comp colour)  …
1912       … init_regs f_lbls f_regs (pc … st1) carry_lives color_of_r RegisterA …
1913      (proj1 ?? (fetch_statement_inv … EQfetch)) (inl ?? r) (inr ?? RegisterA) …
1914      (st_no_pc … st1) (st_no_pc … st2) … (refl …))
1915[8: % [2: #x #_ @I] %{Rst1st2} normalize nodelta % [2: @EQbv |]
1916|4: %
1917|5: @hdw_same_colouring
1918|6: @andb_Prop [2: @I] whd in match (livebefore ?????);
1919    change with (stmt_at ??? (point_of_pc ERTL_semantics ?)) in
1920                           ⊢ (?(??match % with [_ ⇒ ? | _ ⇒ ? ]));
1921    >(proj2 … (fetch_statement_inv … EQfetch)) normalize nodelta
1922    whd in match statement_semantics; normalize nodelta 
1923    whd in match statement_semantics; normalize nodelta
1924    whd in match (defined ??); whd in match (used ???);
1925    @set_member_union2 @set_member_singl
1926|7: inversion(color_of_r) [#n | #R ] #EQcol [@I] 
1927    cases(colouring_is_never_forbidden …
1928                      (proj1 ?? (fetch_statement_inv … EQfetch)) … EQcol)  #_ * #_ *
1929    #H1 * #H2 #_ % assumption
1930|*:
1931]
1932#st2'' * #EQst2'' #Hst2'' %{st2''} % [ >map_eval_add_dummy_variance_id assumption ]
1933%
1934[ cases daemon (*TODO*)
1935| %{it} %{(refl …)}
1936  cases(ps_reg_retrieve_hw_reg_retrieve_commute prog ???? init_regs f_lbls
1937        f_regs f fn (pc … st1) ?????????)
1938  [6: @(proj1 … (fetch_statement_inv … EQfetch))
1939  |11: @Hst2''
1940  |14: @EQbv
1941  |12: % [2: %] whd in match update_fun; normalize nodelta @andb_Prop [2: %]
1942       whd in match (livebefore ?????);
1943       change with (stmt_at ??? (point_of_pc ERTL_semantics ?)) in
1944                         ⊢ (?(??match % with [_ ⇒ ? | _ ⇒ ? ]));
1945       >(proj2 … (fetch_statement_inv … EQfetch)) normalize nodelta
1946       whd in match statement_semantics; normalize nodelta 
1947       whd in match statement_semantics; normalize nodelta
1948       whd in match (defined ??); whd in match (used ???);
1949       @set_member_union2 @set_member_singl
1950  |*:
1951  ]
1952  #bv2 * whd in ⊢ (??%% → ?); whd in match read_arg_decision; normalize nodelta
1953  whd in match update_fun; normalize nodelta @eq_vertex_elim [2: * #H @⊥ @H %] #_
1954  normalize nodelta #H1 #EQ1 %{bv2} %{H1} >EQ1 in EQb; #EQb
1955  cases(bool_of_beval_sigma_commute … EQb) [9: %|*:] #b1 * #H2 #EQ2 destruct
1956  assumption
1957]
1958qed. 
1959 
1960   whd in match eq_vertex; normalize nodelta
1961  whd  in match eq_identifier; normalize nodelta normalize nodelta
1962         
1963 
1964     
1965              [2: @if_elim #_ [ >hwreg_retrieve_insensitive_to_set_other ] ]
1966              >hwreg_retrieve_hwregstore_hit %]
1967            cases(bool_of_beval_sigma_commute fix_comp colour prog init_regs f_lbls
1968                    f_regs … bv1 (refl …) … EQb) #b1 * #H #EQ destruct assumption
19694: % [2: #x #_ @I] % [ @Rst1st2  %{Rst1st2}               
1970
1971
1972
1973inversion(colouring … (inl … r)) [ #n | #R ] #EQcolouring >EQcolouring in EQst2';
1974#EQst2'
1975[2: cases(colouring_is_never_forbidden …
1976                      (proj1 ?? (fetch_statement_inv … EQfetch)) … EQcolouring)
1977   #RnoA * #_ * #RnoDPL * #RnoDPH #_ ] >map_eval_add_dummy_variance_id
1978letin after ≝ (λfn,callee.analyse_liveness fix_comp (prog_names … prog) fn callee)
1979letin before ≝ (λfn,callee.livebefore … fn callee (after fn callee))
1980letin live_fun ≝ (λfn,callee,l,v.in_lattice v ((before fn callee) l) ∧
1981                   match v with [ inl r ⇒ true
1982                | inr R ⇒ all … (λR'.¬ eq_Register R R') RegisterAlwaysDead
1983                ])
1984<EQinit_regs in EQcolouring; #EQcolouring
1985letin aft ≝ (analyse_liveness fix_comp (prog_names … prog) fn (init_regs (pc_block (pc … st1))))
1986letin carry_lives ≝ (h_in_lattice RegisterCarry (aft (point_of_pc ERTL_semantics (pc … st1))))
1987cases(move_preserve fix_comp colour prog (translate_data fix_comp colour)  …
1988      live_fun … init_regs f_lbls f_regs (pc … st1) carry_lives …
1989      (proj1 ?? (fetch_statement_inv … EQfetch)) … EQcolouring)
1990[2: @RegisterA
1991|3:   xxxxxxx   … init_regs … (return st1))   
1992   
1993   
1994[2,4: %
1995   [1,3: >map_eval_add_dummy_variance_id in ⊢ (??%?); >move_spec in ⊢ (??%?);
1996         [2: % // |4: @I] normalize nodelta
1997         [ @eq_Register_elim [ #EQ destruct @⊥ elim RnoA #H @H %] normalize nodelta #_ ]
1998         try >EQst2' in ⊢ (??%?); try >m_return_bind in ⊢ (??%?); whd in match write_decision;
1999         normalize nodelta try >m_return_bind in ⊢ (??%?);
2000         [2: >m_return_if_commute in ⊢ (??%?);] %
2001   |*: %
2002       [1,3: [ whd in match hwreg_store; normalize nodelta @state_rel_insensitive_to_dead_Reg whd in match state_rel; normalize nodelta %{f} %{fn} %
2003          [1,3: cases b @(proj1 … (fetch_statement_inv … EQfetch)) ]
2004          cases Rst1st2 #f1 * #fn1 >(proj1 … (fetch_statement_inv … EQfetch)) *
2005          whd in ⊢ (??%% → ?); #EQ destruct(EQ) normalize nodelta
2006          cases(st_frms ??) [1,3: * ] #frames normalize nodelta ***** #Hmem #Hframes
2007          #Hhw_reg #His #Hcarry * #stack_ptr * #EQsp #Hps_reg
2008          whd in match read_arg_decision in EQst2'; normalize nodelta in EQst2';
2009          [2:  >m_return_bind in EQst2'; >m_return_bind #H @('bind_inversion H) -H
2010               * #x1 #x2 #_ #H @('bind_inversion H) -H * #y1 #y2 #_ #H @('bind_inversion H) -H
2011               #ptr #_ #H @('bind_inversion H) -H #val #_ whd in ⊢ (??%% → ?); #EQst2'
2012          | whd in EQst2' : (??%%);
2013          ]
2014          destruct(EQst2') %
2015          [2,4: %{stack_ptr} %
2016             [1,3: [ @if_elim #_] whd in match (sp ??); whd in match set_regs;
2017                normalize nodelta
2018                [ >hwreg_retrieve_insensitive_to_set_other
2019                  >hwreg_retrieve_insensitive_to_set_other ]
2020                >hwreg_retrieve_hwregstore_miss [2,4,6: % normalize #EQ destruct(EQ)]
2021                [1,2: try >hwreg_retrieve_hwregstore_miss in ⊢ (??(match (?(???%?)) with [_ ⇒ ? | _ ⇒ ?])?);
2022                   [2,4: % normalize #EQ destruct(EQ)]
2023                   try >hwreg_retrieve_hwregstore_miss in ⊢ (??(match (?(???%?)) with [_ ⇒ ? | _ ⇒ ?])?);
2024                   [2,4: % normalize #EQ destruct(EQ)] ]
2025                >hwreg_retrieve_hwregstore_miss [2,4,6: % normalize #EQ destruct(EQ)]
2026                [1,2: try >hwreg_retrieve_hwregstore_miss in ⊢ (??(match (?(????%)) with [_ ⇒ ? | _ ⇒ ?])?);
2027                   [2,4: % normalize #EQ destruct(EQ)]
2028                   try >hwreg_retrieve_hwregstore_miss in ⊢ (??(match (?(????%)) with [_ ⇒ ? | _ ⇒ ?])?);
2029                   [2,4: % normalize #EQ destruct(EQ)] ]
2030                assumption
2031             |*: whd in match ps_relation; normalize nodelta #r1 #d1 *
2032                <commute_if in ⊢ (% → ?); whd in match (pc_block ?); >point_of_pc_of_point
2033                #Hr1 [ <commute_if in ⊢ (% → ?); whd in match (pc_block ?); ] #Hd1
2034                #val1 #EQval1 cases(Hps_reg r1 d1 … EQval1)
2035                [1,3: #val2 * #Hval2 #EQ destruct(EQ) %{val2} % [2,4: %]
2036                   cases d1 in Hval2 Hd1; -d1 [1,3: #n1 |*: #R1] normalize nodelta
2037                   [1,2: #EQbeload |*: whd in ⊢ (??%% → ?); #EQ destruct(EQ)]
2038                   #Hdecision [1,2: [ @if_elim #_] assumption | @if_elim #_ ]
2039                   @eq_f whd in match set_regs; whd in match set_carry;
2040                   normalize nodelta
2041                   cases(colouring_reg_non_DPL_DPH …
2042                        (proj1 ?? (fetch_statement_inv … EQfetch)) … Hdecision) *
2043                   #H1 #H2 #H3 [ >hwreg_retrieve_insensitive_to_set_other]
2044                   >hwreg_retrieve_hwregstore_miss try assumption [3: %]
2045                   >hwreg_retrieve_hwregstore_miss try assumption
2046                   >hwreg_retrieve_hwregstore_miss try assumption %
2047                |*: % [2,4: assumption]
2048                    change with (bool_to_Prop (set_member ????))
2049                    whd in match (livebefore ?????);
2050                    change with (stmt_at ??? (point_of_pc ERTL_semantics ?)) in
2051                          ⊢ (?(????(???match % with [_ ⇒ ? | _ ⇒ ? ])));
2052                    >(proj2 … (fetch_statement_inv … EQfetch)) normalize nodelta
2053                    whd in match statement_semantics; normalize nodelta
2054                    whd in match (defined ??); whd in match (used ???);
2055                    @set_member_union1 @set_member_diff [2,4: @set_member_empty]
2056                    @(set_member_subset_if … Hr1)
2057                    lapply(included_livebefore_livebeafter_stmt_labels
2058                                 fix_comp … (init_regs (pc_block (pc … st1))) …
2059                                 (proj2 ?? (fetch_statement_inv … EQfetch))
2060                                 (if b then ltrue else lfalse) ?)
2061                    [1,3: cases b normalize nodelta
2062                          whd in match stmt_labels; whd in match stmt_explicit_labels;
2063                          whd in match step_labels; normalize nodelta
2064                          [1,3: >memb_cons [1,3: @I |*: @memb_hd] |*: >memb_hd @I ] ]
2065                    whd in match (l_included ???); cases(set_subset ???)
2066                    normalize nodelta [2,4: * |*: #_ @I]
2067                ]     
2068             ]
2069          |*: %
2070             [2,4: <commute_if in ⊢ (% → ?); whd in match (pc_block ?); >point_of_pc_of_point
2071                #Hcarry1
2072                [ <EQinit_regs @if_elim
2073                  [ #H @Hcarry change with (bool_to_Prop (set_member ????))
2074                    whd in match (livebefore ?????);
2075                    change with (stmt_at ??? (point_of_pc ERTL_semantics ?)) in
2076                           ⊢ (?(????(???match % with [_ ⇒ ? | _ ⇒ ? ])));
2077                    >(proj2 … (fetch_statement_inv … EQfetch)) normalize nodelta
2078                    whd in match statement_semantics; normalize nodelta
2079                    whd in match (defined ??); whd in match (used ???);
2080                    @set_member_union1 @set_member_diff [2: @set_member_empty]
2081                    @(set_member_subset_if … Hcarry1)
2082                    lapply(included_livebefore_livebeafter_stmt_labels
2083                                 fix_comp … (init_regs (pc_block (pc … st1))) …
2084                                 (proj2 ?? (fetch_statement_inv … EQfetch))
2085                                 (if b then ltrue else lfalse) ?)
2086                    [1,3: cases b normalize nodelta
2087                          whd in match stmt_labels; whd in match stmt_explicit_labels;
2088                          whd in match step_labels; normalize nodelta
2089                          [1,3: >memb_cons [1,3: @I |*: @memb_hd] |*: >memb_hd @I ] ]
2090                    whd in match (l_included ???); cases(set_subset Register ??)
2091                    [ #_ @I] @if_elim #_ *
2092                  | #ABS @⊥ elim(Prop_notb … ABS) #H @H -H
2093                    @(set_member_subset_if … Hcarry1)
2094                    lapply(included_livebefore_livebeafter_stmt_labels
2095                                 fix_comp … (init_regs (pc_block (pc … st1))) …
2096                                 (proj2 ?? (fetch_statement_inv … EQfetch))
2097                                 (if b then ltrue else lfalse) ?)
2098                    [1,3: cases b normalize nodelta
2099                          whd in match stmt_labels; whd in match stmt_explicit_labels;
2100                          whd in match step_labels; normalize nodelta
2101                          [1,3: >memb_cons [1,3: @I |*: @memb_hd] |*: >memb_hd @I ] ]
2102                    whd in match (l_included ???); cases(set_subset Register ??)
2103                    [ #_ @I] @if_elim #_ *
2104                  ] 
2105                | whd in match set_regs; normalize nodelta @Hcarry
2106                  change with (bool_to_Prop (set_member ????))
2107                  whd in match (livebefore ?????);
2108                  change with (stmt_at ??? (point_of_pc ERTL_semantics ?)) in
2109                          ⊢ (?(????(???match % with [_ ⇒ ? | _ ⇒ ? ])));
2110                   >(proj2 … (fetch_statement_inv … EQfetch)) normalize nodelta
2111                   whd in match statement_semantics; normalize nodelta
2112                   whd in match (defined ??); whd in match (used ???);
2113                   @set_member_union1 @set_member_diff [2: @set_member_empty]
2114                   @(set_member_subset_if … Hcarry1)
2115                   lapply(included_livebefore_livebeafter_stmt_labels
2116                                 fix_comp … (init_regs (pc_block (pc … st1))) …
2117                                 (proj2 ?? (fetch_statement_inv … EQfetch))
2118                                 (if b then ltrue else lfalse) ?)
2119                   [1,3: cases b normalize nodelta
2120                         whd in match stmt_labels; whd in match stmt_explicit_labels;
2121                         whd in match step_labels; normalize nodelta
2122                         [1,3: >memb_cons [1,3: @I |*: @memb_hd] |*: >memb_hd @I ] ]
2123                   whd in match (l_included ???); cases(set_subset ???)
2124                   normalize nodelta [2: * ] #H @H
2125                ]   
2126             |*: % [2,4: [ @if_elim #_ ] assumption] %
2127                [2,4: whd in match hw_relation; normalize nodelta #R <commute_if
2128                   whd in match (pc_block ?); >point_of_pc_of_point #HR
2129                   [ <EQinit_regs @if_elim #Hcarry1 ] whd in match set_regs;
2130                   normalize nodelta [  >hwreg_retrieve_insensitive_to_set_other]
2131                   cut(bool_to_Prop(eq_Register R RegisterA) ∨ ¬ (bool_to_Prop (eq_Register R RegisterA)))
2132                   [1,3,5: @eq_Register_elim #_ //] *
2133                   [1,3,5: @eq_Register_elim [2,4,6: #_ *] #EQ destruct(EQ) #_ @⊥
2134                      @(acc_is_dead fix_comp prog … fn1 …
2135                         (if b then ltrue else lfalse) …
2136                         (init_regs (pc_block (pc … st1)))) assumption ]
2137                   @eq_Register_elim [1,3,5: #_ * #H @⊥ @H @I] #no_a #_
2138                   >hwreg_retrieve_hwregstore_miss [2,4,6: assumption]
2139                   [1,2: cut(bool_to_Prop(eq_Register R RegisterDPL) ∨ ¬ (bool_to_Prop (eq_Register R RegisterDPL))) 
2140                      [1,3: @eq_Register_elim #_ //] * @eq_Register_elim
2141                      [2,3,6,7: #_ * #H @⊥ @H @I] #H
2142                        [1,3: destruct @⊥
2143                           @(dpl_is_dead fix_comp prog … fn1 …
2144                             (init_regs (pc_block (pc … st1)))
2145                             (if b then ltrue else lfalse)) assumption ] #_
2146                      >hwreg_retrieve_hwregstore_miss [2,4: assumption] 
2147                      cut(bool_to_Prop(eq_Register R RegisterDPH) ∨ ¬ (bool_to_Prop (eq_Register R RegisterDPH))) 
2148                      [1,3: @eq_Register_elim #_ //] * @eq_Register_elim
2149                      [2,3,6,7: #_ * #H @⊥ @H @I] #H1
2150                      [1,3: destruct @⊥
2151                           @(dph_is_dead fix_comp prog … fn1 …
2152                             (init_regs (pc_block (pc … st1)))
2153                             (if b then ltrue else lfalse)) assumption ] #_
2154                      >hwreg_retrieve_hwregstore_miss [2,4: assumption] ]
2155                @(Hhw_reg R)
2156                change with (bool_to_Prop (set_member ????))
2157                whd in match (livebefore ?????);
2158                change with (stmt_at ??? (point_of_pc ERTL_semantics ?)) in
2159                          ⊢ (?(????(???match % with [_ ⇒ ? | _ ⇒ ? ])));
2160                >(proj2 … (fetch_statement_inv … EQfetch)) normalize nodelta
2161                whd in match statement_semantics; normalize nodelta
2162                whd in match (defined ??); whd in match (used ???);
2163                @set_member_union1 @set_member_diff [2,4,6: @set_member_empty]
2164                @(set_member_subset_if … HR)
2165                lapply(included_livebefore_livebeafter_stmt_labels
2166                                 fix_comp … (init_regs (pc_block (pc … st1))) …
2167                                 (proj2 ?? (fetch_statement_inv … EQfetch))
2168                                 (if b then ltrue else lfalse) ?)
2169                 [1,3,5: cases b normalize nodelta
2170                         whd in match stmt_labels; whd in match stmt_explicit_labels;
2171                         whd in match step_labels; normalize nodelta
2172                         [1,3,5: >memb_cons [1,3,5: @I |*: @memb_hd] |*: >memb_hd @I ] ]
2173                   whd in match (l_included ???); cases(set_subset ???)
2174                   normalize nodelta [2,4,6: * ] #H @H
2175              |*: % [1,3: [ @if_elim #_] assumption] cases daemon (*TODO*)
2176              ]     
2177             ]
2178           ]
2179         |*: %{it} %{(refl …)} %{bv1} %
2180            [1,3: whd in ⊢ (??%?); whd in match set_regs; normalize nodelta
2181              [2: @if_elim #_ [ >hwreg_retrieve_insensitive_to_set_other ] ]
2182              >hwreg_retrieve_hwregstore_hit %]
2183            cases(bool_of_beval_sigma_commute fix_comp colour prog init_regs f_lbls
2184                    f_regs … bv1 (refl …) … EQb) #b1 * #H #EQ destruct assumption
2185        ]
2186      ]
2187   |*:
2188   ]
2189qed.
2190
2191
2192lemma gen_state_rel_insensitive_to_dead_reg :
2193 ∀prog,stacksize,init,color_fun,live_fun.
2194 ∀init_regs : block → list register.∀f_lbls,f_regs. ∀pc.
2195 ∀f.∀fn : joint_closed_internal_function ? (prog_names … prog).
2196 fetch_internal_function … (joint_globalenv ERTL_semantics prog stacksize)
2197 (pc_block pc) = return 〈f,fn〉 →
2198 ∀st1 : state ERTL_state.∀st2.
2199 ∀psd_regs,hdw_regs.
2200 ∀r,bv. ¬ live_fun fn (init_regs (pc_block pc)) (point_of_pc ERTL_semantics pc) (inl ? ? r) →
2201 gen_state_rel prog stacksize init color_fun live_fun init_regs f_lbls f_regs pc
2202   (set_regs ERTL_semantics 〈psd_regs,hdw_regs〉 st1) st2 →
2203 gen_state_rel prog stacksize init color_fun live_fun init_regs f_lbls f_regs pc
2204  (set_regs ERTL_semantics 〈reg_store r bv psd_regs,hdw_regs〉 st1) st2.
2205#prog #stacksize #init #color_fun #live_fun #init_regs #f_lbls #f_regs #pc #f #fn
2206#EQfn #st1 #st2 #psd #hdw #r #bv #r_dead whd in match state_rel; normalize nodelta *
2207#f1 * #fn1 >EQfn * whd in ⊢ (??%% → ?); #EQ destruct(EQ) inversion (st_frms … st1)
2208[ #EQframes whd in match (st_frms ??); >EQframes *] #frames #EQframes
2209whd in match (st_frms ??); >EQframes normalize nodelta ***** whd in match (m ??);
2210#Hmem #Hframes whd in match (\snd ?); #Hhw_regs whd in match (istack ??); #His
2211whd in match (carry ??); #Hcarry * #sp * #EQsp whd in match set_regs in ⊢ (% → ?);
2212normalize nodelta #Hps_regs %{f1} %{fn1} %{EQfn} whd in match (st_frms ??); >EQframes
2213normalize nodelta %
2214[ % [2: assumption] % [2: assumption] % [2: assumption] %{Hmem} assumption]
2215%{sp} %{EQsp} whd #r1 #d1 * #r1_live #EQd1
2216cut(bool_to_Prop(eq_identifier … r1 r) ∨ bool_to_Prop(¬ (eq_identifier … r1 r)))
2217[ @eq_identifier_elim #_ [%%|%2%]] @eq_identifier_elim
2218[ #EQ destruct >r1_live in r_dead; *] #r_no_r1 #_ whd in match reg_retrieve;
2219  normalize nodelta whd in match set_regs; normalize nodelta whd in match reg_store;
2220  normalize nodelta >lookup_add_miss [2: assumption] @Hps_regs % assumption
2221qed.
2222
2223lemma sp_ok_on_writable_regs :
2224∀st : state ERTL_state.∀bv.
2225∀r.ertl_hdw_writable r →
2226∀psd.
2227sp … st = sp … (set_regs ERTL_state 〈psd,hwreg_store r bv (\snd (regs … st))〉 st).
2228#st #bv #r #Hr #psd whd in ⊢ (??%%); whd in match set_regs; normalize nodelta
2229>hwreg_retrieve_hwregstore_miss
2230[ >hwreg_retrieve_hwregstore_miss [%]]
2231cases r in Hr; whd in match ertl_hdw_writable; normalize nodelta * %
2232whd in ⊢ (??%% → ?); #EQ destruct
2233qed.
2234
2235lemma mem_insensitive_to_writable_set_regs :
2236∀prog,stacksize,R,f,st,m1,m2.
2237∀r.ertl_hdw_writable r →
2238mem_relation prog stacksize R f st m1 m2 →
2239∀psd.∀bv.
2240mem_relation prog stacksize R f
2241 (set_regs ERTL_state 〈psd,hwreg_store r bv (\snd (regs … st))〉 st) m1 m2.
2242#prog #stacksize #R #f #st #m1 #m2 #r #Hr whd in match mem_relation;
2243normalize nodelta #H whd in match ERTL_validate_pointer; normalize nodelta
2244#psd #bv <(sp_ok_on_writable_regs … Hr … psd) assumption
2245qed.
2246 
2247lemma gen_state_rel_insensitive_to_dead_Reg :
2248 ∀prog,stacksize,init,color_fun,live_fun.
2249 ∀init_regs : block → list register.∀f_lbls,f_regs. ∀pc.
2250 ∀f.∀fn : joint_closed_internal_function ? (prog_names … prog).
2251 fetch_internal_function … (joint_globalenv ERTL_semantics prog stacksize)
2252 (pc_block pc) = return 〈f,fn〉 →
2253 ∀st1 : state ERTL_state.∀st2.
2254 ∀r,bv. ¬ live_fun fn (init_regs (pc_block pc)) (point_of_pc ERTL_semantics pc) (inr ? ? r) →
2255 ertl_hdw_writable r →
2256 gen_state_rel prog stacksize init color_fun live_fun init_regs f_lbls f_regs pc st1 st2 →
2257 gen_state_rel prog stacksize init color_fun live_fun init_regs f_lbls f_regs pc
2258  (set_regs ERTL_semantics 〈\fst (regs … st1),hwreg_store r bv (\snd (regs … st1))〉 st1) st2.
2259#prog #stacksize #init #color_fun #live_fun #init_regs #f_lbls #f_regs #pc #f #fn
2260#EQfn #st1 #st2 #R #bv #R_dead #R_writable
2261whd in match gen_state_rel; normalize nodelta * #f1 * #fn1 >EQfn * whd in ⊢ (??%% → ?);
2262#EQ destruct(EQ) whd in match (st_frms ??); cases(st_frms … st1) [*] #frames
2263normalize nodelta ***** #Hmem #Hframes #Hhw_reg #His #Hcarry * #sp * #EQsp #Hps_regs
2264%{f1} %{fn1} %{(refl …)} %
2265[ % [2: assumption] % [2: assumption] %
2266  [ % [2: assumption ]
2267  | %
2268    [ whd in match hwreg_retrieve_sp; normalize nodelta whd in match set_regs;
2269      normalize nodelta >hwreg_retrieve_hwregstore_miss
2270      [ >hwreg_retrieve_hwregstore_miss [ @(proj1 … (Hhw_reg))]]
2271      % #EQ destruct assumption
2272    | #r #r_live inversion(color_fun ???) [#r_spill | #r_col ] #EQcol normalize nodelta
2273      whd in match set_regs; normalize nodelta >hwreg_retrieve_hwregstore_miss
2274      [1,3: lapply(proj2 ?? (Hhw_reg) r r_live) >EQcol normalize nodelta #H @H]
2275      % #EQ destruct(EQ) >r_live in R_dead; *
2276    ]
2277  ]
2278| %{sp} %{EQsp} assumption
2279]
2280@mem_insensitive_to_writable_set_regs assumption
2281qed.
2282
2283lemma state_rel_insensitive_to_dead_carry :
2284 ∀prog,stacksize,init,color_fun,live_fun.
2285 ∀init_regs : block → list register.∀f_lbls,f_regs. ∀pc.
2286 ∀f.∀fn : joint_closed_internal_function ? (prog_names … prog).
2287 fetch_internal_function … (joint_globalenv ERTL_semantics prog stacksize)
2288 (pc_block pc) = return 〈f,fn〉 →
2289 ∀st1 : state ERTL_state.∀st2.
2290 ∀c. ¬ live_fun fn (init_regs (pc_block pc)) (point_of_pc ERTL_semantics pc) (inr ? ? RegisterCarry) →
2291 gen_state_rel prog stacksize init color_fun live_fun init_regs f_lbls f_regs pc st1 st2 →
2292 gen_state_rel prog stacksize init color_fun live_fun init_regs f_lbls f_regs pc
2293  (set_carry ERTL_semantics c st1) st2.
2294#prog #stacksize #init #color_fun #live_fun #init_regs #f_lbls #f_regs #pc #f #fn #EQfn #st1 #st2 #c
2295#c_dead whd in match gen_state_rel; normalize nodelta * #f1 * #fn1 >EQfn * whd in ⊢ (??%% → ?);
2296#EQ destruct(EQ) whd in match (st_frms ??); cases(st_frms ??) [*] #frames
2297normalize nodelta ***** #H1 #H2 #H3 #H4 #H5 #H6 %{f1} %{fn1} %{(refl …)}
2298% [2: assumption] % [ % [2: assumption] % [2: assumption] % assumption]
2299#c_live >c_live in c_dead; *
2300qed.
2301
2302
2303
2304
2305
2306
2307
2308
2309lemma pair_eta : ∀A,B : Type[0].∀p : A × B. p = 〈\fst p,\snd p〉. // qed.
2310
2311lemma de_morgan_or : ∀a,b : bool. (notb (a ∨ b)) = true → (notb a) = true ∧ (notb b) = true.
2312** normalize #EQ destruct %% qed.
2313
2314lemma be_op2_carry_preserve : ∀op.
2315∀by,bv1,bv2,res,by'.be_op2 by op bv1 bv2 = return 〈res,by'〉 →
2316if match op with [And ⇒ true | Or ⇒ true | Xor ⇒ true | _⇒ false] then
2317by = by'
2318else True.
2319* normalize nodelta #by #bv1 #bv2 #res #by' try(#_ @I)
2320whd in match be_op2; normalize nodelta
2321[ #H @('bind_inversion H) -H #bi1 #_ #H @('bind_inversion H) -H #bi2 #_
2322  whd in ⊢ (??%% → ?); #EQ destruct %
2323| cases bv1 normalize nodelta
2324  [|| #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc #p ]
2325  [1,5,6,7: whd in ⊢ (??%% → ?); #EQ destruct(EQ)]
2326  cases bv2 normalize nodelta
2327  [1,2,8,9,15,16: whd in ⊢ (??%% → ?); #EQ destruct %
2328  |3,10,17: #a1 #a2 #a3  whd in ⊢ (??%% → ?); [1,3: #EQ destruct %]
2329            @if_elim #_ [2: #EQ destruct] @if_elim #_
2330            whd in ⊢ (??%% → ?); #EQ destruct %
2331  |4,11,18: #a1 whd in ⊢ (??%% → ?); [1,2: #EQ destruct %]
2332            cases(op2 eval false Or by a1)
2333            #a2 #a3 #EQ destruct %
2334  |5,12,19: #a1
2335  |6,13,20: #a1 #a2
2336  |7,14,21: #a1 #a2
2337  ]
2338   whd in ⊢ (??%% → ?); #EQ destruct
2339| cases bv1 normalize nodelta
2340  [|| #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc #p ]
2341  [1,2,3,7: whd in ⊢ (??%% → ?); #EQ destruct(EQ)]
2342  cases bv2 normalize nodelta
2343  [1,2,8,9,15,16: whd in ⊢ (??%% → ?); #EQ destruct
2344  |3,10,17: #a1 #a2 #a3  whd in ⊢ (??%% → ?); #EQ destruct %
2345  |4,11,18: #a1 whd in ⊢ (??%% → ?); [2,3: #EQ destruct %]
2346            cases(op2 eval false Xor by a1)
2347            #a2 #a3 #EQ destruct %
2348  |5,12,19: #a1 [whd in ⊢ (??%% → ?); #EQ destruct]
2349            @if_elim #_ whd in ⊢ (??%% → ?); #EQ destruct %
2350  |6,13,20: #a1 #a2 [whd in ⊢ (??%% → ?); #EQ destruct]
2351            @if_elim #_ whd in ⊢ (??%% → ?); #EQ destruct %
2352  |7,14,21: #a1 #a2 whd in ⊢ (??%% → ?); #EQ destruct
2353  ]
2354]
2355qed.
2356
2357lemma eq_true_to_bool : ∀b.b=true → bool_to_Prop(b).
2358#b #EQ >EQ @I qed.
2359
2360
2361lemma state_rel_insensitive_to_eliminable:
2362 ∀fix_comp: fixpoint_computer.∀build.
2363 ∀prog: ertl_program.
2364 let m ≝ (\snd (\fst (ertl_to_ltl fix_comp build prog))) in
2365 let stackcost≝ lookup_stack_cost … m in
2366 ∀init_regs : block → list register.∀f_lbls,f_regs.
2367 let p_in ≝ mk_prog_params ERTL_semantics prog stackcost in
2368 ∀f. ∀fn : joint_closed_internal_function ??. ∀pc.
2369 let after ≝ (analyse_liveness fix_comp (prog_names … prog) fn (init_regs (pc_block pc))) in
2370 let before ≝ livebefore … fn (init_regs (pc_block pc)) after in
2371 ∀st1 : state ERTL_state.
2372 let pt ≝ point_of_pc ERTL_semantics pc in
2373 ∀st1_no_pc. ∀stms: joint_seq ERTL(prog_names … prog). ∀next.
2374 fetch_internal_function … (joint_globalenv ERTL_semantics prog stackcost) (pc_block pc) =
2375 return 〈f,fn〉 →
2376 stmt_at p_in … (joint_if_code p_in … fn) pt = return (sequential … stms next) →
2377   eval_seq_no_pc ERTL_semantics
2378   (prog_names … prog) (joint_globalenv ERTL_semantics prog stackcost)
2379   f stms st1 =return st1_no_pc →
2380   eliminable_step (globals ? p_in) (after pt) stms →
2381   ∀st2.
2382   state_rel fix_comp build prog init_regs f_lbls f_regs pc st1 st2 →
2383   state_rel fix_comp build prog init_regs f_lbls f_regs
2384    (pc_of_point ERTL_semantics (pc_block pc) next) st1_no_pc st2.
2385#fix_comp #build #prog letin p_in ≝ (mk_prog_params ???) #init_regs
2386#f_lbls #f_regs #f #fn #pc #st1 #st1' #stms #next #EQfn #stmtat #Heval #Helim
2387#st2 #Rstst2 (* #f1 * #fn1
2388* >EQfn in ⊢ (??%? → ?); whd in ⊢ (??%% → ?); #EQ destruct(EQ) normalize nodelta
2389inversion(st_frms ??) [#_ *] #frames #EQframes normalize nodelta ***** #Hmem #Hframes
2390#Hhwreg #His #Hcarry * #ptr * #EQptr #Hps_reg *)
2391lapply (eliminable_step_to_eq_livebefore_liveafter … stmtat … (init_regs (pc_block pc)) … Helim)
2392#EQlivebefore cases stms in stmtat Helim Heval; -stms
2393[ #str
2394| #pm (* *** [#r | #R #writable_R] * [ * [ ** [#r1 * | #R1 #readable_R1] | #by ] | ** [#r1 * | #R1 #Hreadable] | #by ] *)
2395| #A
2396| #A
2397| #id #id_spec #arg1 #dpl #dph
2398| #opaccs #A #B #A1 #B1
2399| #op1 #A #A1
2400| #op2 #A #A1 #snd_arg
2401|
2402|
2403| #A #dpl #dph
2404| #dpl #dph #A
2405| * #r
2406]
2407#stmtat  try(change with (false) in ⊢ (?% → ?); * )
2408whd in match eliminable_step; normalize nodelta
2409[ cases pm in stmtat; ** [#r * | #R #R_writable] * [1,3: ** [1,3: #r1 * |*: #R1 #R1_readable ] |*: #by ]
2410  #stmtat normalize nodelta #Helim whd in match eval_seq_no_pc; normalize nodelta
2411  whd in match pair_reg_move; normalize nodelta #H @('bind_inversion H) -H
2412  #rgs whd in ⊢ (??%% → ?); normalize nodelta
2413  [1,2: inversion (ps_reg_retrieve ??) [2,4: #e normalize nodelta #_ #EQ destruct]
2414    #bv #EQbv normalize nodelta whd in ⊢ (??%% → ?); ]
2415  #EQ destruct(EQ) whd in ⊢ (??%% → ?); #EQ destruct(EQ)
2416| #Helim whd in match eval_seq_no_pc; normalize nodelta whd in match dpl_store;
2417  normalize nodelta >m_return_bind whd in ⊢ (??%% → ?); whd in match set_regs;
2418  normalize nodelta #EQ destruct(EQ)
2419| #Helim whd in match eval_seq_no_pc; normalize nodelta whd in match acca_arg_retrieve;
2420  whd in match accb_arg_retrieve; normalize nodelta
2421  change with (ps_arg_retrieve ??) in match (acca_arg_retrieve_ ?????);
2422  #H @('bind_inversion H) -H #val1 #EQval1
2423  change with (ps_arg_retrieve ??) in match (accb_arg_retrieve_ ?????);
2424  #H @('bind_inversion H) -H #val2 #EQval2 #H @('bind_inversion H) -H
2425  * #val3 #val4 #EQval34 whd in match acca_store; normalize nodelta
2426  change with (ps_reg_store ???) in match (acca_store_ ??????); #H @('bind_inversion H)
2427  -H #st1'' #H @('bind_inversion H) -H #new_rgs whd in ⊢ (??%% → ??%% → ?);
2428  #EQ1 #EQ2 destruct(EQ1 EQ2) whd in match accb_store; normalize nodelta
2429  change with (ps_reg_store ???) in match (accb_store_ ??????);
2430  #H @('bind_inversion H) -H #new_rgs' whd in ⊢ (??%% → ?); #EQ destruct(EQ)
2431  whd in match set_regs; normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ)
2432| #Helim whd in match eval_seq_no_pc; normalize nodelta whd in match acca_retrieve;
2433  normalize nodelta change with (ps_reg_retrieve ??) in match (acca_retrieve_ ?????);
2434  #H @('bind_inversion H) -H #val1 #EQval1 #H @('bind_inversion H) -H
2435  #val2 #EQval2 whd in match acca_store; normalize nodelta
2436  change with (ps_reg_store ???) in match (acca_store_ ??????);
2437  #H @('bind_inversion H) -H #new_rgs whd in ⊢ (??%% → ??%% → ?);
2438  #EQ1 #EQ2 destruct(EQ1 EQ2)
2439| cases op2 in stmtat; #stmtat normalize nodelta #Helim
2440  whd in match eval_seq_no_pc; normalize nodelta whd in match acca_arg_retrieve;
2441  normalize nodelta
2442  change with (ps_arg_retrieve ??) in match (acca_arg_retrieve_ ?????);
2443  #H @('bind_inversion H) -H #val1 #EQval1 whd in match snd_arg_retrieve;
2444  normalize nodelta change with (ps_arg_retrieve ??) in match (snd_arg_retrieve_ ?????);
2445  #H @('bind_inversion H) -H #val2 #EQval2 #H @('bind_inversion H) -H *
2446  #val3 #by #EQval3 whd in match acca_store; normalize nodelta
2447  change with (ps_reg_store ???) in match (acca_store_ ??????);
2448  #H @('bind_inversion H) -H #st'' #H @('bind_inversion H) -H #new_rgs
2449  whd in ⊢ (??%% → ??%% → ??%% → ?); #EQ1 #EQ2 #EQ3 destruct(EQ1 EQ2 EQ3)
2450| #Helim whd in match eval_seq_no_pc; normalize nodelta whd in match dph_arg_retrieve;
2451  whd in match dpl_arg_retrieve; normalize nodelta
2452  change with (ps_arg_retrieve ??) in match (dpl_arg_retrieve_ ?????);
2453  change with (ps_arg_retrieve ??) in match (dph_arg_retrieve_ ?????);
2454  #H @('bind_inversion H) -H #val1 #EQval1 #H @('bind_inversion H) -H
2455  #val2 #EQval2 #H @('bind_inversion H) -H #ind #EQind
2456  #H @('bind_inversion H) -H #ok_ind #EQok_ind #H @('bind_inversion H) -H
2457  #val3 #H lapply(opt_eq_from_res ???? H) -H #EQval3 whd in match acca_store;
2458  normalize nodelta change with (ps_reg_store ???) in match (acca_store_ ??????);
2459  #H @('bind_inversion H) -H #new_rgs whd in ⊢ (??%% → ??%% → ?);
2460  #EQ1 #EQ2 destruct(EQ1 EQ2)
2461| #Helim whd in match eval_seq_no_pc; normalize nodelta whd in ⊢ (??%% → ?);
2462  whd in match (stack_sizes ????); inversion (opt_to_res ???) normalize nodelta
2463  [2: #e #_ #EQ destruct(EQ)] #ssize #H lapply(opt_eq_from_res ???? H) -H
2464  #EQssize whd in match ps_reg_store_status; normalize nodelta
2465  #H @('bind_inversion H) -H #new_rgs whd in ⊢ (??%% → ??%% → ?);
2466  #EQ1 #EQ2 destruct(EQ1 EQ2) 
2467]
2468[1,2,3,4,5,6,7,8,9,16,17: change with (set_regs ?? st1) in ⊢ (????????%?);
2469  [1,3,5,7,8,9,10,11: @(state_rel_insensitive_to_dead_reg … f fn) [1,4,7,10,13,16,19,22: @EQfn]
2470    [2,4,6,12,14,16: <pair_eta >set_regs_eta
2471    |8,10: @(state_rel_insensitive_to_dead_reg … f fn) [1,4: @EQfn]
2472       [2,4: <pair_eta >set_regs_eta]
2473    ]
2474  |*: @(state_rel_insensitive_to_dead_Reg … f fn) try @EQfn try @R_writable
2475  ]
2476|*: change with (set_regs ?? (set_carry ?? st1)) in ⊢ (????????%?);
2477     @(state_rel_insensitive_to_dead_reg … f fn) try @EQfn
2478     [2,4,6,8,10,12: <pair_eta  <set_carry_set_regs_commute
2479       [4,5,6: lapply(be_op2_carry_preserve … EQval3) normalize nodelta
2480               #EQ destruct(EQ) >set_regs_eta >set_carry_eta
2481       |*: @(state_rel_insensitive_to_dead_carry … f fn) try @EQfn
2482           [2,4,6: >set_regs_eta]
2483       ]
2484     ]
2485]
2486[9,10,11,12,13,14,15,16,17,18,19,21,23,31,32,33,34,35,36,37,38,39:
2487  @notb_Prop % change with (bool_to_Prop(set_member ????)) in ⊢ (% → ?);
2488  #ABS cases(Prop_notb … Helim) #H @H -H
2489  lapply(included_livebefore_livebeafter_stmt_labels
2490                                 fix_comp … (init_regs (pc_block pc)) … stmtat next ?)
2491  [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43:
2492    whd in match stmt_labels; whd in match stmt_explicit_labels;
2493    whd in match stmt_implicit_label; normalize nodelta >memb_hd @I ]
2494  whd in match (l_included ???); @if_elim try( #_ * ) #sb_regs #sb_Regs
2495  [ @orb_Prop_l
2496  | @orb_Prop_l @orb_Prop_l
2497  |
2498  |
2499  |
2500  | @orb_Prop_r
2501  | @orb_Prop_l @orb_Prop_r
2502  |
2503  |
2504  |
2505  |
2506  |
2507  |
2508  | @orb_Prop_l
2509  | @orb_Prop_l
2510  | @orb_Prop_l
2511  | @orb_Prop_r
2512  | @orb_Prop_r
2513  | @orb_Prop_r
2514  | @orb_Prop_r
2515  | @orb_Prop_r
2516  | @orb_Prop_r
2517  ]
2518  @(set_member_subset_if … ABS) >point_of_pc_of_point assumption
2519|*: lapply Rstst2 whd in match state_rel; normalize nodelta * #f1 * #fn1 >EQfn
2520  * whd in ⊢ (??%% → ?); #EQ destruct(EQ) cases(st_frms … st1)
2521  [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33: *] #frames normalize nodelta
2522  ***** #Hmem #Hframes #Hhw_reg #His #Hcarry * #sp * #EQsp #Hps_regs
2523  %{f1} %{fn1} %{(refl …)} %
2524  [2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34: %{sp} %{EQsp}
2525    #r2 #d2 * change with (bool_to_Prop(set_member ????)) in ⊢ (% → ?);
2526    >point_of_pc_of_point #r2_live #EQd2 @(Hps_regs r2 d2) % try assumption
2527    >EQlivebefore change with (bool_to_Prop(set_member ????))
2528    lapply(included_livebefore_livebeafter_stmt_labels
2529                                 fix_comp … (init_regs (pc_block pc)) … stmtat next ?)
2530    [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33:
2531      whd in match stmt_labels; whd in match stmt_explicit_labels;
2532      whd in match stmt_implicit_label; normalize nodelta >memb_hd @I ]
2533      whd in match (l_included ???); @if_elim try( #_ * ) #H1 #H2
2534      @(set_member_subset_if … r2_live) assumption
2535  |*: %
2536    [2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34: >point_of_pc_of_point
2537      #carry_live @Hcarry >EQlivebefore change with (bool_to_Prop(set_member ????))
2538      lapply(included_livebefore_livebeafter_stmt_labels
2539                                 fix_comp … (init_regs (pc_block pc)) … stmtat next ?)
2540      [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33:
2541        whd in match stmt_labels; whd in match stmt_explicit_labels;
2542        whd in match stmt_implicit_label; normalize nodelta >memb_hd @I ]
2543      whd in match (l_included ???); @if_elim try( #_ * ) #H1 #H2
2544      @(set_member_subset_if … carry_live) assumption
2545    |*: % try @His %
2546      [2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34: >point_of_pc_of_point
2547        #R #R_live @(Hhw_reg R) >EQlivebefore  change with (bool_to_Prop(set_member ????))
2548        lapply(included_livebefore_livebeafter_stmt_labels
2549                                 fix_comp … (init_regs (pc_block pc)) … stmtat next ?)
2550        [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33:
2551          whd in match stmt_labels; whd in match stmt_explicit_labels;
2552          whd in match stmt_implicit_label; normalize nodelta >memb_hd @I ]
2553        whd in match (l_included ???); @if_elim try( #_ * ) #H1 #H2
2554        @(set_member_subset_if … R_live) assumption
2555      |*: % assumption
2556      ]
2557    ]
2558  ]
2559]
2560qed.
2561
2562lemma notb_idempotent : ∀b.b = notb (notb b).
2563* % qed.
2564
2565           
2566lemma seq_commute :∀fix_comp,colour,prog,init_regs,f_lbls,f_regs.
2567let p_out ≝ (\fst (\fst (ertl_to_ltl fix_comp colour prog))) in
2568let m ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in
2569let n ≝ \snd (ertl_to_ltl fix_comp colour prog) in
2570let stacksizes ≝ lookup_stack_cost … m in
2571let init ≝ translate_data fix_comp colour in
2572seq_commutation_statement ERTL_semantics LTL_semantics prog stacksizes
2573 init init_regs
2574 f_lbls f_regs (state_rel fix_comp colour prog init_regs f_lbls f_regs)
2575 (state_pc_rel fix_comp colour prog init_regs f_lbls f_regs).
2576#fix_comp #colour #prog #init_regs #f_lbls #f_regs #st1 #st1' #st2 #f #fn
2577#stmt #nxt * #Hbl #EQfetch whd in match eval_state; normalize nodelta
2578>EQfetch >m_return_bind whd in match eval_statement_no_pc; normalize nodelta
2579#H @('bind_inversion H) -H #st1'' #EQst1'' whd in match eval_statement_advance;
2580whd in match next; whd in match set_no_pc; whd in match set_pc; normalize nodelta
2581whd in ⊢ (??%% → ?); #EQ destruct(EQ) whd in match state_pc_rel; normalize nodelta
2582** #Rst1st2 #Hpc #Hlp #t_fn #EQt_fn #z1 #z2 #z3 #z4 #z5 #z6 #z7 #z8 whd #Hinit_regs
2583whd @if_elim <Hinit_regs #Helim
2584[ % [2: normalize nodelta %{(refl …)} %{(st_no_pc … st2)} %{(refl …)}
2585        @(state_rel_insensitive_to_eliminable …
2586          (proj1 … (fetch_statement_inv … EQfetch)) …
2587          (proj2 … (fetch_statement_inv … EQfetch)) … EQst1'' … Helim) assumption |]]
2588cases stmt in EQfetch EQst1'' Helim; -stmt
2589[ #c #EQfetch whd in ⊢ (??%% → ?); #EQ destruct(EQ) #_ % [2: %{(refl …)} |]
2590  %{(st_no_pc … st2)} %{(refl …)} cases Rst1st2 #f1 * #fn1
2591  >(proj1 … (fetch_statement_inv … EQfetch)) * whd in ⊢ (??%% → ?); #EQ destruct(EQ)
2592  whd in match state_rel; normalize nodelta cases(st_frms ??) [*] #frames
2593  normalize nodelta ***** #H1 #H2 #H3 #H4 #H5 * #sp * #EQsp #H6 %{f1} %{fn1}
2594  >(proj1 … (fetch_statement_inv … EQfetch)) %{(refl …)}
2595  % [ % [ % [2: assumption] % [% assumption] ]]
2596  [ #R >point_of_pc_of_point change with nxt in match (point_of_succ ???);
2597    change with (set_member ????) in ⊢ (?% → ?); #Hlive @(H3 R)
2598    change with (set_member ????) in ⊢ (?%);
2599  | >point_of_pc_of_point change with nxt in match (point_of_succ ???);
2600    change with (set_member ????) in ⊢ (?% → ?); #Hlive @H5
2601    change with (set_member ????) in ⊢ (?%);
2602  | %{sp} %{EQsp} #r #d * >point_of_pc_of_point
2603    change with nxt in match (point_of_succ ???);
2604    change with (set_member ????) in ⊢ (?% → ?); #Hlive #EQd
2605    @(H6 r) % [2: assumption] change with (set_member ????) in ⊢ (?%);
2606  ] 
2607  whd in match (livebefore ?????);
2608  change with (stmt_at ??? (point_of_pc ERTL_semantics ?)) in
2609                           ⊢ (?(????(???match % with [_ ⇒ ? | _ ⇒ ? ])));
2610  >(proj2 … (fetch_statement_inv … EQfetch)) normalize nodelta
2611  whd in match statement_semantics; normalize nodelta
2612  whd in match (defined ??); whd in match (used ???);
2613  @set_member_union1 @set_member_diff [2,4,6: @set_member_empty]
2614  @(set_member_subset_if … Hlive)
2615  lapply(included_livebefore_livebeafter_stmt_labels fix_comp …
2616         (init_regs (pc_block (pc … st1))) …
2617         (proj2 ?? (fetch_statement_inv … EQfetch)) nxt ?)
2618  [1,3,5: whd in match stmt_labels; whd in match stmt_explicit_labels;
2619     whd in match step_labels; normalize nodelta >memb_hd @I]
2620  whd in match (l_included ???);
2621  [1,2: @if_elim [2,4: #_ *] #_]
2622  cases(set_subset ???) normalize nodelta /2/
2623| *** [#r_dest * | #R_dest #writeable_R_dest ] *
2624  [1,3: ** [1,3: #r_src * |*: #R_src #readable_R_src] |*: #by ]  #EQfetch
2625  whd in match eval_seq_no_pc; whd in match pair_reg_move; normalize nodelta
2626  whd in match (pair_reg_move_ ?????); normalize nodelta
2627  [1,2: inversion(ps_reg_retrieve ??) [2,4: #e #_ whd in ⊢ (??%% → ?); #EQ destruct(EQ)]
2628    #bv whd in match ps_reg_retrieve; normalize nodelta #EQbv normalize nodelta ]
2629  >m_return_bind whd in ⊢ (??%% → ?); #EQ destruct(EQ) whd in match eliminable_step;
2630  normalize nodelta <notb_idempotent #dest_live cases daemon
2631 (*FALSO perche' solo la destinazione e' viva e solo per i vivi vi e' preservazione !!! *)
2632| #r #EQfetch whd in match eval_seq_no_pc; normalize nodelta
2633  #H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H * #bv #st1'''
2634  #EQst1''' whd in ⊢ (??%% → ?); #EQ destruct(EQ) #_ % [2: % [ %] | ]
2635  cases(pop_ok ERTL_semantics LTL_semantics
2636    (λbv1,bv2.bv1 = sigma_beval fix_comp colour prog init_regs f_lbls f_regs bv2)
2637    (state_rel fix_comp colour prog init_regs f_lbls f_regs (pc ERTL_semantics st1)) 
2638   … EQst1''')
2639   
2640   
2641  inversion (colouring ?? (inl ?? r)) [ #n | #R ] #EQcolouring
2642 
2643
2644 
2645lemma return_commute :∀fix_comp,colour,prog,init_regs,f_lbls,f_regs.
2646let p_out ≝ (\fst (\fst (ertl_to_ltl fix_comp colour prog))) in
2647let m ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in
2648let n ≝ \snd (ertl_to_ltl fix_comp colour prog) in
2649let stacksizes ≝ lookup_stack_cost … m in
2650let init ≝ (λglobals,fn.«translate_data fix_comp colour globals fn,?») in
2651return_commutation_statement ERTL_semantics LTL_semantics prog stacksizes
2652 init init_regs
2653 f_lbls f_regs (state_rel fix_comp colour prog)
2654 (state_pc_rel fix_comp colour prog init_regs f_lbls f_regs).
2655[2: @hide_prf %]
2656cases daemon (*TODO*)
2657qed.
2658
2659lemma pre_main_commute : ∀fix_comp,colour,prog,init_regs,f_lbls,f_regs.
2660let p_out ≝ (\fst (\fst (ertl_to_ltl fix_comp colour prog))) in
2661let m ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in
2662let n ≝ \snd (ertl_to_ltl fix_comp colour prog) in
2663let stacksizes ≝ lookup_stack_cost … m in
2664let init ≝ (λglobals,fn.«translate_data fix_comp colour globals fn,?») in
2665b_graph_transform_program_props ERTL_semantics LTL_semantics stacksizes
2666  init prog init_regs f_lbls f_regs →
2667pre_main_commutation_statement  ERTL_semantics LTL_semantics prog stacksizes
2668 init init_regs
2669 f_lbls f_regs (state_rel fix_comp colour prog)
2670 (state_pc_rel fix_comp colour prog init_regs f_lbls f_regs).
2671[2: @hide_prf %]
2672cases daemon qed.
2673
2674(*
2675#fix_comp #colour #prog #init_regs #f_lbls #f_regs #good whd
2676#st1 #st1' #st2 #EQbl whd in match eval_state; normalize nodelta
2677whd in match fetch_statement; whd in match fetch_internal_function; normalize nodelta
2678whd in match fetch_function; normalize nodelta @eqZb_elim [2: * #H @⊥ @H assumption]
2679#_ normalize nodelta >m_return_bind #H @('bind_inversion H) -H ** #f #fn #stmt
2680#H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H #stmt1
2681#H lapply(opt_eq_from_res ???? H) -H whd in ⊢ (??%% → ?); cases st1 in EQbl; -st1
2682#st1 * #bl1 #pos1 #lp1 #EQbl1 normalize nodelta cases pos1 -pos1 normalize nodelta
2683[ #EQ destruct(EQ)
2684|*: * [2,3,5,6: #x ] whd in ⊢ (??%% → ?); #EQ destruct
2685]
2686whd in ⊢ (??%% → ?); #EQ destruct(EQ) normalize nodelta whd in match eval_statement_no_pc; normalize inversion(point_of_pc ERTL_semantics (pc … st1))
2687*)
2688
2689lemma call_commute : ∀fix_comp,colour,prog,init_regs,f_lbls,f_regs.
2690let p_out ≝ (\fst (\fst (ertl_to_ltl fix_comp colour prog))) in
2691let m ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in
2692let n ≝ \snd (ertl_to_ltl fix_comp colour prog) in
2693let stacksizes ≝ lookup_stack_cost … m in
2694let init ≝ (λglobals,fn.«translate_data fix_comp colour globals fn,?») in
2695call_commutation_statement ERTL_semantics LTL_semantics prog stacksizes
2696 init init_regs
2697 f_lbls f_regs (state_rel fix_comp colour prog)
2698 (state_pc_rel fix_comp colour prog init_regs f_lbls f_regs).
2699[2: @hide_prf %]
2700cases daemon qed.
2701
2702lemma goto_commute : ∀fix_comp,colour,prog,init_regs,f_lbls,f_regs.
2703let p_out ≝ (\fst (\fst (ertl_to_ltl fix_comp colour prog))) in
2704let m ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in
2705let n ≝ \snd (ertl_to_ltl fix_comp colour prog) in
2706let stacksizes ≝ lookup_stack_cost … m in
2707let init ≝ (λglobals,fn.«translate_data fix_comp colour globals fn,?») in
2708goto_commutation_statement ERTL_semantics LTL_semantics prog stacksizes
2709 init init_regs
2710 f_lbls f_regs (state_rel fix_comp colour prog)
2711 (state_pc_rel fix_comp colour prog init_regs f_lbls f_regs).
2712[2: @hide_prf %]
2713cases daemon qed.
2714
2715lemma tailcall_commute : ∀fix_comp,colour,prog,init_regs,f_lbls,f_regs.
2716let p_out ≝ (\fst (\fst (ertl_to_ltl fix_comp colour prog))) in
2717let m ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in
2718let n ≝ \snd (ertl_to_ltl fix_comp colour prog) in
2719let stacksizes ≝ lookup_stack_cost … m in
2720let init ≝ (λglobals,fn.«translate_data fix_comp colour globals fn,?») in
2721tailcall_commutation_statement ERTL_semantics LTL_semantics prog stacksizes
2722 init init_regs
2723 f_lbls f_regs (state_rel fix_comp colour prog)
2724 (state_pc_rel fix_comp colour prog init_regs f_lbls f_regs).
2725[2: @hide_prf %]
2726#fix_comp #colour #prog #init_regs #f_lbls #f_regs whd #st1 #st2
2727#f #fn *
2728qed.
2729
2730             
2731theorem ERTLToLTL_ok :
2732∀fix_comp : fixpoint_computer.
2733∀colour : coloured_graph_computer.
2734∀p_in : ertl_program.
2735let 〈p_out, m, n〉 ≝ ertl_to_ltl fix_comp colour p_in in
2736(* what should we do with n? *)
2737let stacksizes ≝ lookup_stack_cost m in
2738∀init_in.make_initial_state
2739  (mk_prog_params ERTL_semantics p_in stacksizes) = OK … init_in →
2740∃init_out.
2741  make_initial_state
2742   (mk_prog_params LTL_semantics p_out stacksizes) =
2743    OK ? init_out ∧
2744∃[1] R.
2745  status_simulation_with_init
2746    (joint_status ERTL_semantics p_in stacksizes)
2747    (joint_status LTL_semantics p_out stacksizes)
2748    R init_in init_out.
2749#fix_comp #colour #p_in #init_in #EQinit_in
2750letin p_out ≝ (\fst (\fst (ertl_to_ltl fix_comp colour p_in)))
2751letin m ≝ (\snd (\fst (ertl_to_ltl fix_comp colour p_in)))
2752letin n ≝ (\snd (ertl_to_ltl fix_comp colour p_in))
2753letin stacksizes ≝ (lookup_stack_cost m)
2754cases(make_b_graph_transform_program_props ERTL_semantics LTL_semantics stacksizes
2755     (λglobals : list ident.λfn.«translate_data fix_comp colour globals fn,(refl …)») p_in)
2756#init_regs * #f_lbls * #f_regs #good
2757@(joint_correctness ERTL_semantics LTL_semantics p_in stacksizes
2758(λglobals : list ident.λfn.«translate_data fix_comp colour globals fn,(refl …)»)
2759init_regs f_lbls f_regs (state_rel fix_comp colour p_in)
2760(state_pc_rel fix_comp colour p_in init_regs f_lbls f_regs) ? ? init_in EQinit_in)
2761%
2762[ @good
2763| #st1 #st2 #f #fn #Rst1st2 #EQfn whd %{f} %{fn} %{EQfn}
2764  @(fetch_ok_sigma_state_ok fix_comp colour p_in … Rst1st2 EQfn)
2765| #st1 #st2 #f #fn #Rst1st2 #EQfn @(fetch_ok_pc_ok fix_comp colour p_in … Rst1st2 EQfn)
2766| #st1 #st2 #f #fn #Rst1st2 #EQfn lapply Rst1st2 whd in match state_pc_rel;
2767  normalize nodelta cases(st_frms … st1) [*] #frames normalize nodelta
2768  whd in match sigma_fb_state_pc; whd in match sigma_sb_state_pc; normalize nodelta
2769  >EQfn normalize nodelta <(fetch_ok_pc_ok … Rst1st2 EQfn) >EQfn normalize nodelta
2770  #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) assumption
2771| #st1 #st2 #pc #lp1 #lp2 #f #fn #EQfn #Rst1st2 #EQ destruct(EQ) whd
2772  lapply Rst1st2 whd in match state_rel; normalize nodelta * #f1 * #fn1 >EQfn *
2773  whd in ⊢ (??%% → ?); #EQ destruct(EQ) cases(st_frms … st1) [*] #frames
2774  normalize nodelta #EQst whd in match sigma_fb_state_pc;
2775  whd in match sigma_sb_state_pc; normalize nodelta >EQfn
2776  normalize nodelta @eq_f3 [2,3: % | assumption]
2777| @pre_main_commute assumption
2778| #f #fn * #bl #pos #EQbl whd in match fetch_statement;
2779  whd in match fetch_internal_function; whd in match fetch_function;
2780  normalize nodelta @eqZb_elim [2: * #H @⊥ @H assumption]
2781  #_ normalize nodelta >m_return_bind #H @('bind_inversion H) -H #stmt 
2782  #H lapply(opt_eq_from_res ???? H) -H whd in ⊢ (??%% → ?);
2783  whd in match point_of_pc; normalize nodelta cases pos normalize nodelta
2784  [ #EQ destruct(EQ)
2785  |*: * [2,3,5,6: #x ] whd in ⊢ (??%% → ?); #EQ destruct
2786  ]
2787  whd in ⊢ (??%% → ?); #EQ destruct(EQ)
2788| @cond_commute
2789| @seq_commute
2790| #f #fn #bl #EQfn #id #args #dest #lbl whd #bl'
2791  %{(match id with [inl f1 ⇒ inl ?? f1 | inr x ⇒ inr ?? 〈it,it〉])}
2792  %{args} %{it} normalize nodelta cases id [ #f1 % | * #dpl #dph %]
2793| cases daemon (*TODO*)
2794| @return_commute
2795| @call_commute
2796| @goto_commute
2797| @tailcall_commute
2798| cases daemon (*TODO*)
2799| cases daemon (*TODO*)
2800| cases daemon (*TODO*)
2801| cases daemon (*TODO*)
2802]
2803qed.
Note: See TracBrowser for help on using the repository browser.