source: src/ERTL/ERTLToLTLProof.ma @ 3371

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

Modified RTLsemantics and ERTLsemantics. Now the pop frame will set
to undef the carry bit and all RegisterCallerSaved? exept those used to
pass the return value of a function.

Added an overflow check in ERTL_semantics

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