source: src/ERTL/ERTLToLTLProof.ma @ 3372

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

Added new implementation of labelling approach based on LTS and emmission of costlabels during transitions

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