source: src/ERTL/ERTLToLTLProof.ma @ 3252

Last change on this file since 3252 was 3252, checked in by piccolo, 7 years ago

proof obbligation added on ERTL to LTL proof

File size: 85.1 KB
Line 
1include "ERTL/ERTLToLTL.ma".
2include "ERTL/ERTL_semantics.ma".
3include "LTL/LTL_semantics.ma".
4include "common/AssocList.ma".
5include "joint/StatusSimulationHelper.ma".
6
7(* Inefficient, replace with Trie lookup *)
8definition lookup_stack_cost ≝
9 λp.λid : ident.
10  assoc_list_lookup ? ℕ id (eq_identifier …) p.
11
12(*TO BE MOVED*)
13definition ERTL_status ≝
14λprog : ertl_program.λstack_sizes.
15joint_abstract_status (mk_prog_params ERTL_semantics prog stack_sizes).
16
17definition LTL_status ≝
18λprog : ltl_program.λstack_sizes.
19joint_abstract_status (mk_prog_params LTL_semantics prog stack_sizes).
20
21definition local_clear_sb_type ≝ decision → bool.
22definition clear_sb_type ≝ label → local_clear_sb_type.
23
24(*function that will be used in order to retrieve ERTL-states from LTL-states.
25  Now it is an axiom. To be Implemented *)
26axiom to_be_cleared_sb : 
27∀live_before : valuation register_lattice.
28coloured_graph live_before → clear_sb_type.
29
30definition local_clear_fb_type ≝ vertex → bool.
31definition clear_fb_type ≝ label → local_clear_fb_type.
32
33
34(*function that will be used in order to clear ERTL-states from dead registers.
35  Now it is an axiom. To be implemented *)
36definition to_be_cleared_fb :
37∀live_before : valuation register_lattice.clear_fb_type≝
38λlive_before,pt,v.notb (lives v (live_before pt)).
39
40include "common/ExtraIdentifiers.ma".
41
42definition sigma_fb_register_env : local_clear_fb_type → register_env beval →
43register_env beval ≝
44λclear_fun,regs.find_all … regs (λi.λ_.notb (clear_fun (inl ?? i))).
45
46definition register_of_bitvector :  BitVector 6 → option Register≝
47λvect.
48let n ≝ nat_of_bitvector … vect in
49if eqb n 0 then Some ? Register00
50else if eqb n 1 then Some ? Register01
51else if eqb n 2 then Some ? Register02
52else if eqb n 3 then Some ? Register03
53else if eqb n 4 then Some ? Register04
54else if eqb n 5 then Some ? Register05
55else if eqb n 6 then Some ? Register06
56else if eqb n 7 then Some ? Register07
57else if eqb n 8 then Some ? Register10
58else if eqb n 9 then Some ? Register11
59else if eqb n 10 then Some ? Register12
60else if eqb n 11 then Some ? Register13
61else if eqb n 12 then Some ? Register14
62else if eqb n 13 then Some ? Register15
63else if eqb n 14 then Some ? Register16
64else if eqb n 15 then Some ? Register17
65else if eqb n 16 then Some ? Register20
66else if eqb n 17 then Some ? Register21
67else if eqb n 18 then Some ? Register22
68else if eqb n 19 then Some ? Register23
69else if eqb n 20 then Some ? Register24
70else if eqb n 21 then Some ? Register25
71else if eqb n 22 then Some ? Register26
72else if eqb n 23 then Some ? Register27
73else if eqb n 24 then Some ? Register30
74else if eqb n 25 then Some ? Register31
75else if eqb n 26 then Some ? Register32
76else if eqb n 27 then Some ? Register33
77else if eqb n 28 then Some ? Register34
78else if eqb n 29 then Some ? Register35
79else if eqb n 30 then Some ? Register36
80else if eqb n 31 then Some ? Register37
81else if eqb n 32 then Some ? RegisterA
82else if eqb n 33 then Some ? RegisterB
83else if eqb n 34 then Some ? RegisterDPL
84else if eqb n 35 then Some ? RegisterDPH
85else if eqb n 36 then Some ? RegisterCarry (* was -1, increment as needed *)
86else None ?.
87
88
89
90definition sigma_fb_hw_register_env : local_clear_fb_type → hw_register_env →
91hw_register_env ≝
92λclear_fun,regs.
93let f ≝ λvect,val,m.
94  match register_of_bitvector vect with
95  [ Some r ⇒
96     if (clear_fun (inr ?? r)) then
97      m
98     else
99      insert … vect val m
100  | None ⇒ m
101  ] in
102mk_hw_register_env … (fold … f (reg_env … regs) (Stub …)) BBundef.
103
104definition sigma_fb_regs : local_clear_fb_type → ertl_reg_env → ertl_reg_env ≝
105λclear_fun,regs.〈sigma_fb_register_env clear_fun (\fst regs),
106                 sigma_fb_hw_register_env clear_fun (\snd regs)〉.
107
108definition sigma_fb_frames : local_clear_fb_type →
109list (register_env beval × (Σb:block.block_region b=Code)) →
110list (register_env beval × (Σb:block.block_region b=Code)) ≝ 
111λclear_fun,frms.map … (λx.〈sigma_fb_register_env clear_fun (\fst x),\snd x〉) frms.
112
113definition sigma_fb_state:
114 ertl_program → local_clear_fb_type →
115  state ERTL_semantics → state ERTL_semantics ≝
116λprog,clear_fun,st.
117mk_state ?
118 (option_map ?? (sigma_fb_frames clear_fun) (st_frms … st))
119 (istack … st)
120 (if clear_fun (inr ?? RegisterCarry) then BBundef
121  else (carry … st))
122 (sigma_fb_regs clear_fun (regs … st)) (m … st) (stack_usage … st).
123
124axiom acc_is_dead : ∀fix_comp.∀prog : ertl_program.
125 ∀fn : joint_closed_internal_function ERTL (prog_names … prog). ∀l.
126 let after ≝ analyse_liveness fix_comp (prog_names … prog) fn in
127  ¬ lives (inr ? ? RegisterA) (livebefore  … fn after l).
128
129axiom dead_registers_in_dead :
130 ∀fix_comp.∀build : coloured_graph_computer.
131 ∀prog : ertl_program.
132 ∀fn : joint_closed_internal_function ERTL (prog_names … prog).
133 ∀l.
134 let after ≝ analyse_liveness fix_comp (prog_names … prog) fn in
135 let coloured_graph ≝ build … fn after in
136 ∀R : Register.
137  ¬ lives (inr ? ? R) (livebefore  … fn after l) →
138   to_be_cleared_sb … coloured_graph l R.
139   
140axiom sigma_sb_state: list (Σb.block_region b = Code) →
141 ertl_program → local_clear_sb_type → state LTL_semantics → state ERTL_semantics.
142
143definition dummy_state : state ERTL_semantics ≝
144mk_state ERTL_semantics
145   (None ?) empty_is BBundef 〈empty_map ? ?,mk_hw_register_env … (Stub …) BBundef〉
146   empty O.
147
148definition dummy_state_pc : state_pc ERTL_semantics ≝
149mk_state_pc ? dummy_state (null_pc one) (null_pc one).
150
151definition get_ertl_call_stack :
152list (register_env beval × (Σb:block.block_region b=Code)) →
153list (Σb:block.block_region b=Code) ≝ map … \snd.
154
155definition sigma_fb_state_pc :
156 fixpoint_computer → coloured_graph_computer → ertl_program → 
157  state_pc ERTL_semantics → state_pc ERTL_semantics ≝
158 λfix_comp,colour,prog,st.
159 let m ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in
160 let stacksizes ≝ lookup_stack_cost … m in 
161 let ge ≝ joint_globalenv ERTL_semantics prog stacksizes in
162 let globals ≝ prog_names … prog in
163 match fetch_internal_function … ge (pc_block (pc … st)) with
164  [ OK y ⇒
165     let pt ≝ point_of_pc ERTL_semantics (pc ? st) in
166     let after ≝ (analyse_liveness fix_comp (prog_names … prog) (\snd y)) in
167     let before ≝ livebefore … (\snd y) after in
168     mk_state_pc ? (sigma_fb_state prog (to_be_cleared_fb before pt) st) (pc … st) 
169      (last_pop … st)
170  | Error e ⇒ dummy_state_pc
171  ].
172
173definition sigma_sb_state_pc:
174 fixpoint_computer → coloured_graph_computer → 
175  ertl_program → list (Σb:block.block_region b=Code) → 
176  (block → list register) → lbl_funct_type →
177  regs_funct_type →  state_pc LTL_semantics → state_pc ERTL_semantics ≝
178 λfix_comp,build,prog,cs,init_regs,f_lbls,f_regs,st.
179  let init ≝ (λglobals,fn.«translate_data fix_comp build globals fn,?») in
180  let m ≝ (\snd (\fst (ertl_to_ltl fix_comp build prog))) in
181  let stacksizes ≝ lookup_stack_cost … m in 
182  let ge ≝ joint_globalenv ERTL_semantics prog stacksizes in
183  let globals ≝ prog_names … prog in
184  match fetch_internal_function … ge (pc_block (pc … st)) with
185  [ OK y ⇒ 
186     let pt ≝ point_of_pc ERTL_semantics (pc ? st) in
187     let after ≝ (analyse_liveness fix_comp (prog_names … prog) (\snd y)) in
188     let coloured_graph ≝ build … (\snd y) after in
189     mk_state_pc ? (sigma_sb_state cs prog
190                       (to_be_cleared_sb … coloured_graph pt) st) (pc … st) 
191                   (sigma_stored_pc ERTL_semantics LTL_semantics
192                      prog stacksizes init init_regs f_lbls f_regs (last_pop … st))
193  | Error e ⇒ dummy_state_pc
194  ].
195@hide_prf % qed.
196
197definition state_rel : fixpoint_computer → coloured_graph_computer →
198ertl_program → joint_state_relation ERTL_semantics LTL_semantics ≝
199λfix_comp,build,prog,pc,st1,st2.
200let m ≝ (\snd (\fst (ertl_to_ltl fix_comp build prog))) in
201let stacksizes ≝ lookup_stack_cost … m in 
202let ge ≝ joint_globalenv ERTL_semantics prog stacksizes in
203∃f,fn.fetch_internal_function … ge (pc_block pc)
204= return 〈f,fn〉 ∧
205let after ≝ (analyse_liveness fix_comp (prog_names … prog) fn) in
206let before ≝ livebefore … fn after in
207let coloured_graph ≝ build … fn after in
208match st_frms … st1 with
209[ None ⇒ False
210| Some frames ⇒
211 (sigma_fb_state prog (to_be_cleared_fb before (point_of_pc ERTL_semantics pc)) st1) =
212  (sigma_sb_state (get_ertl_call_stack frames) prog
213   (to_be_cleared_sb … coloured_graph (point_of_pc ERTL_semantics pc)) st2)
214].
215
216definition state_pc_rel :
217fixpoint_computer → coloured_graph_computer → 
218  ertl_program → (block → list register) → lbl_funct_type →
219  regs_funct_type →  joint_state_pc_relation ERTL_semantics LTL_semantics ≝
220 λfix_comp,build,prog,init_regs,f_lbls,f_regs,st1,st2.
221match st_frms … (st_no_pc … st1) with
222[ None ⇒ False
223| Some frames ⇒
224   sigma_fb_state_pc fix_comp build prog st1 =
225    sigma_sb_state_pc fix_comp build prog (get_ertl_call_stack frames) init_regs
226     f_lbls f_regs st2
227].
228
229definition write_decision :
230ℕ →  decision → beval → state LTL_LIN_state → res (state LTL_LIN_state) ≝
231λlocalss,d,bv,st.
232match d with
233[ decision_spill n ⇒
234  ! addrl ← hw_reg_retrieve (regs … st) RegisterSPL;
235  ! addrh ← hw_reg_retrieve (regs … st) RegisterSPH;
236  ! 〈newaddrl,new_carry〉 ←
237     be_op2 (carry … st) Add (BVByte (bitvector_of_nat 8 (localss + n))) addrl;
238  ! 〈newaddrh,new_carry'〉← be_op2 new_carry Addc zero_byte addrh;
239  ! ptr ← pointer_of_address 〈newaddrl,newaddrh〉;
240  ! new_mem ← opt_to_res ? [MSG FailedStore] (bestorev (m … st) ptr bv);
241  return
242   set_m ? new_mem
243   (set_regs LTL_semantics
244    (hwreg_store RegisterDPL newaddrl (hwreg_store RegisterDPH newaddrh (regs … st)))
245     (set_carry ? new_carry' st))
246| decision_colour r ⇒
247   !rgs  ← hw_reg_store r bv (regs … st);
248    return set_regs LTL_LIN_state rgs st
249].
250
251definition read_arg_decision : ℕ  → state LTL_LIN_state → arg_decision →
252res (beval × (state LTL_LIN_state)) ≝
253λlocalss,st,d.
254match d with
255[ arg_decision_colour r ⇒
256    return 〈hwreg_retrieve (regs … st) r,st〉
257| arg_decision_spill n ⇒
258  ! addrl ← hw_reg_retrieve (regs … st) RegisterSPL;
259  ! addrh ← hw_reg_retrieve (regs … st) RegisterSPH;
260  ! 〈newaddrl,new_carry〉 ←
261     be_op2 (carry … st) Add (BVByte (bitvector_of_nat 8 (localss + n))) addrl;
262  ! 〈newaddrh,new_carry'〉← be_op2 new_carry Addc zero_byte addrh;
263  ! ptr ← pointer_of_address 〈newaddrl,newaddrh〉;
264  ! bv ← opt_to_res ? [MSG FailedLoad] (beloadv (m … st) ptr);
265  return 〈bv,set_regs LTL_semantics (hwreg_store RegisterDPL newaddrl
266                                     (hwreg_store RegisterDPH newaddrh
267                                       (regs … st))) (set_carry ? new_carry' st)〉
268| arg_decision_imm b ⇒
269   return 〈BVByte b,st〉
270].
271
272axiom insensitive_to_be_cleared_sb :
273 ∀prog. ∀tb : local_clear_sb_type. ∀st : state LTL_LIN_state.
274  ∀d : decision.∀bv,st',localss,cs.tb d →
275  write_decision localss d bv st = return st' →
276   sigma_sb_state cs prog tb st =
277    sigma_sb_state cs prog tb st'.
278   
279lemma hw_reg_retrieve_write_decision_hit : ∀r : Register.∀bv : beval.∀localss.
280∀st : state LTL_LIN_state.
281∀st'. (write_decision localss r bv st) = return st' →
282hw_reg_retrieve (regs … st') r = return bv.
283#r #bv #localss #st #st' whd in match write_decision; normalize nodelta
284whd in match hw_reg_store; normalize nodelta >m_return_bind
285whd in ⊢ (??%% → ?); #EQ destruct(EQ)
286whd in match hw_reg_retrieve; normalize nodelta @eq_f
287whd in match hwreg_retrieve; whd in match hwreg_store; normalize nodelta
288@lookup_insert_hit
289qed.
290
291include alias "arithmetics/nat.ma".
292
293definition is_zero: nat → Prop ≝
294 λn. match n with [ O ⇒ True | S _ ⇒ False ].
295
296lemma furbo: ∀r,s. eqb (nat_of_register r) (nat_of_register s) → r = s.
297* normalize in ⊢ (∀_. ?(?%?) → ?);
298try ( #x cases x normalize * %) (* 24s *)
299qed.
300
301(* it is true but there are 1296 cases *)
302lemma nat_of_register_inj : ∀r,s.nat_of_register r = nat_of_register s →  r = s.
303#r #s #H @furbo @eqb_elim #H2 try % @(absurd … H H2)
304qed.
305 
306lemma eq_Register_elim : ∀P : bool → Prop.
307∀r,s: Register.(r=s → P true) → (r ≠s → P false) →
308P (eq_Register r s).
309#P #r #s #H1 #H2 whd in match eq_Register; normalize nodelta
310@eqb_elim
311[ #H @H1 @(nat_of_register_inj … H)
312| * #H @H2 % #EQ @H >EQ %
313]
314qed.
315
316lemma hwreg_retrieve_hwregstore_hit :
317∀regs,r,bv.
318hwreg_retrieve (hwreg_store r bv regs) r = bv.
319#regs #r #bv whd in match hwreg_retrieve; whd in match hwreg_store;
320normalize nodelta @lookup_insert_hit
321qed.
322
323axiom bitvector_of_register_inj : ∀r,s.
324bitvector_of_register r = bitvector_of_register s → r =s.
325
326lemma hwreg_retrieve_hwregstore_miss :
327∀regs,r,s,bv.
328r ≠ s →
329hwreg_retrieve (hwreg_store s bv regs) r = hwreg_retrieve regs r.
330#regs #r #s #bv * #H whd in match hwreg_retrieve; whd in match hwreg_store;
331normalize nodelta @lookup_insert_miss @eq_bv_elim
332[ #H1 @H @(bitvector_of_register_inj … H1) ] #_ @I
333qed.
334
335lemma hwreg_retrieve_insensitive_to_set_other :
336∀regs,r,b.
337hwreg_retrieve (hwreg_set_other b regs) r = hwreg_retrieve regs r.
338#regs #r #b %
339qed.
340
341axiom hwreg_store_idempotent : ∀r,bv1,bv2,regs.
342hwreg_store r bv1 (hwreg_store r bv2 regs) =
343hwreg_store r bv1 regs.
344
345axiom hwreg_store_commute : ∀r1,r2,bv1,bv2,regs.
346r1 ≠r2 →
347hwreg_store r1 bv1 (hwreg_store r2 bv2 regs) =
348hwreg_store r2 bv2 (hwreg_store r1 bv1 regs).
349
350axiom other_bit_insensitive_to_reg_store : ∀r,bv,regs.
351other_bit (hwreg_store r bv regs) = other_bit regs.
352
353axiom hwreg_store_retrieve_eq : ∀r,regs.
354hwreg_store r (hwreg_retrieve regs r) regs = regs.
355
356definition invariant_for_move :  arg_decision → Prop ≝
357λsrc.match src with
358[ arg_decision_colour r ⇒ r ≠ RegisterDPL ∧ r ≠ RegisterDPH
359| _ ⇒ True
360].
361
362lemma hwreg_store_set_other_commut : ∀regs,r,bv,b.
363hwreg_store r bv (hwreg_set_other b regs) =
364hwreg_set_other b (hwreg_store r bv regs).
365* #reg_env #other #r #bv #b %
366qed.
367
368lemma move_spec : ∀prog.∀stack_size.∀localss : nat.
369∀ carry_lives_after : bool.∀dest : decision.∀src : arg_decision.
370∀f : ident.
371∀s : state LTL_LIN_state.
372invariant_for_move src →
373repeat_eval_seq_no_pc LTL_semantics (mk_prog_params LTL_semantics prog stack_size) f
374   (move (prog_names … prog) localss carry_lives_after dest src) s =
375match src with
376[ arg_decision_spill n ⇒
377  match dest with
378  [ decision_spill n1 ⇒
379     if eqb n n1 then return s
380     else ! 〈bv,s'〉 ← (read_arg_decision localss s src);
381          let news ≝ set_regs LTL_semantics (hwreg_store RegisterA bv (regs … s')) s' in
382          ! s'' ← write_decision localss dest bv news;
383          let regSt1 ≝ (hwreg_store RegisterST1 bv (regs … s'')) in
384          if carry_lives_after then
385            return set_regs LTL_semantics (hwreg_set_other (carry … s) regSt1)
386                    (set_carry ? (carry … s) s'')
387          else
388            return set_regs LTL_semantics regSt1 s''
389   | decision_colour r ⇒
390        if eq_Register r RegisterA then
391         ! 〈bv,s'〉 ← (read_arg_decision localss s src);
392         ! s'' ← write_decision localss dest bv s';
393         if carry_lives_after then
394           return set_regs LTL_semantics (hwreg_set_other (carry … s) (regs … s''))
395                   (set_carry ? (carry … s) s'')
396         else
397           return s''
398        else
399         ! 〈bv,s'〉 ← (read_arg_decision localss s src);
400         let news ≝ set_regs LTL_semantics (hwreg_store RegisterA bv (regs … s')) s' in
401         ! s'' ← write_decision localss dest bv news;
402         if carry_lives_after then
403           return set_regs LTL_semantics (hwreg_set_other (carry … s) (regs … s''))
404                   (set_carry ? (carry … s) s'')
405         else
406           return s''
407   ]
408| arg_decision_colour r ⇒
409      match dest with
410      [ decision_spill _ ⇒
411        ! 〈bv,s'〉 ← (read_arg_decision localss s src);
412        let rgs ≝ if eq_Register r RegisterA then
413               hwreg_store RegisterST1 (hwreg_retrieve (regs … s') RegisterA)
414                (regs … s')
415              else
416               hwreg_store RegisterA (hwreg_retrieve (regs … s') r) (regs … s') in
417        ! s'' ← write_decision localss dest bv (set_regs LTL_semantics rgs s');
418        if carry_lives_after then
419           return set_regs LTL_semantics (hwreg_set_other (carry … s) (regs … s''))
420                   (set_carry ? (carry … s) s'')
421         else
422           return s''
423      | decision_colour r1 ⇒
424         if eq_Register r1 r then return s
425         else if eq_Register r1 RegisterA then
426               ! 〈bv,s'〉 ← (read_arg_decision localss s src);
427               write_decision localss dest bv s'
428         else ! 〈bv,s'〉 ← (read_arg_decision localss s src);
429               let rgs ≝ (hwreg_store RegisterA (hwreg_retrieve (regs … s) r) (regs … s')) in
430               write_decision localss dest bv (set_regs LTL_semantics rgs s')
431      ]     
432| arg_decision_imm b ⇒
433   match dest with
434   [ decision_spill _ ⇒
435      ! 〈bv,s'〉 ← (read_arg_decision localss s src);
436      let rgs ≝ hwreg_store RegisterA (BVByte b) (regs … s') in
437      ! s'' ← write_decision localss dest bv (set_regs LTL_semantics rgs s');
438      if carry_lives_after then
439           return set_regs LTL_semantics (hwreg_set_other (carry … s) (regs … s''))
440                   (set_carry ? (carry … s) s'')
441         else
442           return s''
443   | decision_colour r ⇒
444      ! 〈bv,s'〉 ← (read_arg_decision localss s src);
445      if eq_Register r RegisterA then 
446       write_decision localss dest bv s'
447      else
448       write_decision localss dest bv
449        (set_regs LTL_semantics
450         (hwreg_store RegisterA (BVByte b) (regs … s')) s')
451  ]
452].
453(*
454#prog #stack_size #localss #cl #dest #src #f #st #good
455inversion(repeat_eval_seq_no_pc ?????)
456[ #st' whd in match move; normalize nodelta
457  cases dest in good; -dest normalize nodelta
458  [ #off cases src -src normalize nodelta
459    [ #r whd in match invariant_for_move; normalize nodelta
460      whd in match preserve_carry_bit; normalize nodelta * #H1 #H2
461      cases cl -cl normalize nodelta
462      whd in match set_stack; normalize nodelta whd in match read_arg_decision;
463      normalize nodelta @eq_Register_elim
464      [1,3: #EQ destruct(EQ) normalize nodelta whd in match set_stack_a;
465            normalize nodelta
466      |*:   * #Hr normalize nodelta
467      ]
468      whd in match set_stack_not_a; whd in match set_dp_by_offset;
469      whd in match repeat_eval_seq_no_pc; normalize nodelta
470      whd in match (m_fold ??????) in ⊢ (??%?? → ?);
471      inversion (eval_seq_no_pc ??????) [2,4,6,8: #e #_ normalize nodelta #EQ destruct]
472      #st1 whd in match eval_seq_no_pc in ⊢ (% → ?); whd in match acca_arg_retrieve;
473      normalize nodelta
474      change with (hw_reg_retrieve ??) in match (acca_arg_retrieve_ ?????);
475      whd in match hw_reg_retrieve; normalize nodelta whd in match set_regs;
476      normalize nodelta >hwreg_retrieve_hwregstore_hit >m_return_bind
477      whd in match snd_arg_retrieve; normalize nodelta
478      whd in match (snd_arg_retrieve_ ?????); >hwreg_retrieve_hwregstore_miss
479      [2,4,6,8: % #ABS whd in ABS : (??%%); destruct(ABS)]
480      [1,2: >hwreg_retrieve_hwregstore_miss
481            [2,4: % #ABS whd in ABS : (??%%); destruct(ABS)] ]
482      [1,3: >hwreg_retrieve_insensitive_to_set_other ] >m_return_bind
483      #H @('bind_inversion H) -H * #x1 #x2 #EQx1x2 whd in match acca_store;
484      normalize nodelta change with (hw_reg_store ???) in match (acca_store_ ??????);
485      whd in match hw_reg_store; normalize nodelta >hwreg_store_idempotent
486      [ >hwreg_retrieve_insensitive_to_set_other ] >m_return_bind
487      whd in match set_carry; whd in match set_regs; normalize nodelta
488      whd in ⊢ (??%% → ?); #EQ destruct(EQ) whd in match (m_fold ??????) in ⊢ (??%?? → ?);
489      inversion (eval_seq_no_pc ??????) [2,4,6,8: #e #_ whd in ⊢ (??%%% → ?); #EQ destruct(EQ)]
490      #st'' whd in match set_regs; normalize nodelta >hwreg_retrieve_hwregstore_hit in ⊢ (% → ?);
491      >(hwreg_store_commute RegisterDPL RegisterA) [2,4,6,8: % normalize #EQ destruct]
492      >hwreg_store_idempotent whd in match eval_seq_no_pc in ⊢ (% → ?);
493      whd in match acca_arg_retrieve; normalize nodelta
494      change with (hw_reg_retrieve ??) in match (acca_arg_retrieve_ ?????) in ⊢ (% → ?);
495      whd in match hw_reg_retrieve; normalize nodelta >hwreg_retrieve_hwregstore_hit
496      >m_return_bind whd in match snd_arg_retrieve; normalize nodelta
497      whd in match (snd_arg_retrieve_ ?????);
498      >hwreg_retrieve_hwregstore_miss [2,4,6,8: % normalize #EQ destruct(EQ)]
499      >hwreg_retrieve_hwregstore_miss [2,4,6,8: % normalize #EQ destruct(EQ)]
500      [1,3: >hwreg_retrieve_hwregstore_miss [2,4: % normalize #EQ destruct(EQ)] ]
501      [1,3: >hwreg_retrieve_insensitive_to_set_other ] >m_return_bind
502      #H @('bind_inversion H) -H * #y1 #y2 #EQy1y2 whd in match acca_store;
503      normalize nodelta whd in match (acca_store_ ??????);
504      >hwreg_store_idempotent >m_return_bind whd in match set_carry;
505      whd in match set_regs; normalize nodelta whd in ⊢ (??%% → ?); #EQ
506      destruct(EQ) whd in match (m_fold ??????) in ⊢ (??%?? → ?);
507      inversion (eval_seq_no_pc ??????)
508      [2,4,6,8: #e #_ whd in ⊢ (??%%% → ?); #EQ destruct(EQ)] #st''
509      whd in match set_regs; normalize nodelta
510      [ >hwreg_retrieve_hwregstore_miss in ⊢ (??(??????(?????(??%?)??))?? → ?);
511        [2: normalize % #EQ destruct]
512        >hwreg_retrieve_hwregstore_miss in ⊢ (??(??????(?????(??%?)??))?? → ?);
513        [2: normalize % #EQ destruct]
514        >hwreg_retrieve_hwregstore_miss in ⊢ (??(??????(?????(??%?)??))?? → ?);
515        [2: normalize % #EQ destruct]
516        >hwreg_retrieve_hwregstore_hit in ⊢ (??(??????(?????(??%?)??))?? → ?);
517        >hwreg_retrieve_hwregstore_hit in ⊢ (??(??????(?????(???%)??))?? → ?);
518      | >hwreg_retrieve_hwregstore_hit
519      | >hwreg_retrieve_hwregstore_miss in ⊢ (??(??????(?????(??%?)??))?? → ?);
520        [2: normalize % #EQ destruct]
521        >hwreg_retrieve_hwregstore_miss in ⊢ (??(??????(?????(??%?)??))?? → ?);
522        [2: normalize % #EQ destruct]
523        >hwreg_retrieve_hwregstore_miss in ⊢ (??(??????(?????(??%?)??))?? → ?
524        );
525        [2: normalize % #EQ destruct]
526        >hwreg_retrieve_hwregstore_hit in ⊢ (??(??????(?????(??%?)??))?? → ?);
527        >hwreg_retrieve_hwregstore_hit in ⊢ (??(??????(?????(???%)??))?? → ?);
528      | >hwreg_retrieve_hwregstore_hit
529      ] 
530      whd in match eval_seq_no_pc in ⊢ (% → ?); whd in match dph_arg_retrieve;
531      normalize nodelta whd in ⊢ (??%?? → ?); inversion(pointer_of_address ?)
532      [2,4,6,8: #e #_ whd in ⊢ (??%?? → ?); #EQ destruct(EQ)] #ptr
533      [ >hwreg_retrieve_hwregstore_miss in ⊢ (% → ?); [2: normalize % #EQ destruct]
534        >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(???%?))?? → ?);
535        [2: normalize % #EQ destruct]
536        >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(???%?))?? → ?);
537        [2: normalize % #EQ destruct]
538        >hwreg_retrieve_hwregstore_hit in ⊢ (??(?(???%?))?? → ?);
539        >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(????%))?? → ?);
540        [2: normalize % #EQ destruct]
541        >hwreg_retrieve_hwregstore_hit in ⊢ (??(?(????%))?? → ?);
542      | >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(???%?))?? → ?);
543        [2: normalize % #EQ destruct]
544        >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(???%?))?? → ?);
545        [2: normalize % #EQ destruct]
546        >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(???%?))?? → ?);
547        [2: normalize % #EQ destruct]
548        >hwreg_retrieve_hwregstore_hit in ⊢ (??(?(???%?))?? → ?);
549        >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(????%))?? → ?);
550        [2: normalize % #EQ destruct]
551        >hwreg_retrieve_hwregstore_hit in ⊢ (??(?(????%))?? → ?);
552      | >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(???%?))?? → ?);
553        [2: normalize % #EQ destruct]
554        >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(???%?))?? → ?);
555        [2: normalize % #EQ destruct]
556        >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(???%?))?? → ?);
557        [2: normalize % #EQ destruct]
558        >hwreg_retrieve_hwregstore_hit in ⊢ (??(?(???%?))?? → ?);
559        >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(????%))?? → ?);
560        [2: normalize % #EQ destruct]
561        >hwreg_retrieve_hwregstore_hit in ⊢ (??(?(????%))?? → ?);
562      | >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(???%?))?? → ?);
563        [2: normalize % #EQ destruct]
564        >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(???%?))?? → ?);
565        [2: normalize % #EQ destruct]
566        >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(???%?))?? → ?);
567        [2: normalize % #EQ destruct]
568        >hwreg_retrieve_hwregstore_hit in ⊢ (??(?(???%?))?? → ?);
569        >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(????%))?? → ?);
570        [2: normalize % #EQ destruct]
571        >hwreg_retrieve_hwregstore_hit in ⊢ (??(?(????%))?? → ?);
572      ]
573      #EQptr normalize nodelta whd in match acca_arg_retrieve; normalize nodelta
574      whd in match (acca_arg_retrieve_ ?????);
575      [1,3: >hwreg_retrieve_hwregstore_hit >m_return_bind #H @('bind_inversion H) -H
576            #m1 #H lapply(opt_eq_from_res ???? H) -H #EQm1
577      |*: whd in ⊢ (??%?? → ?); inversion (opt_to_res ???)
578          [2,4: #e #_ normalize nodelta #EQ destruct] #m1 #H lapply(opt_eq_from_res ???? H)
579          -H
580          [ >hwreg_retrieve_hwregstore_hit in ⊢ (??(???%)? → ?);
581          | >hwreg_retrieve_hwregstore_hit in ⊢ (??(???%)? → ?);
582          ]
583          >hwreg_retrieve_hwregstore_miss [2,4: assumption]
584          >hwreg_retrieve_hwregstore_miss [2,4: % assumption]
585          >hwreg_retrieve_hwregstore_miss [2,4: assumption]
586          [ >hwreg_retrieve_insensitive_to_set_other ] #EQm1 normalize nodelta
587      ]
588      whd in match set_m; normalize nodelta
589      [1,2: whd in ⊢ (??%% → ?); |*: whd in ⊢ (??%%% → ?);] #EQ destruct(EQ)
590      whd in match (m_fold ??????) in ⊢ (??%?? → ?);
591      [1,3: whd in match set_carry; normalize nodelta
592            >other_bit_insensitive_to_reg_store >other_bit_insensitive_to_reg_store
593            >other_bit_insensitive_to_reg_store >other_bit_insensitive_to_reg_store
594            [ >other_bit_insensitive_to_reg_store ]
595            whd in match hwreg_set_other; normalize nodelta
596      ]
597      #EQ destruct(EQ) @sym_eq >m_return_bind whd in match write_decision;
598      normalize nodelta
599      whd in match hw_reg_retrieve; whd in match set_regs; normalize nodelta
600      >hwreg_retrieve_hwregstore_miss [2,4,6,8: normalize % #EQ destruct]
601      >m_return_bind
602      >hwreg_retrieve_hwregstore_miss [2,4,6,8: normalize % #EQ destruct]
603      >m_return_bind
604      >EQx1x2 >m_return_bind >EQy1y2 >m_return_bind >EQptr
605      >m_return_bind >EQm1 >m_return_bind @eq_f whd in match set_m;
606      normalize nodelta @eq_f3 [2,3,5,6,8,9,11,12: %]
607      >(hwreg_store_commute RegisterDPH RegisterA) in ⊢ (???(???%));
608      [2,4,6,8: % #EQ destruct]
609      [1,3: >(hwreg_store_idempotent RegisterA)
610              >(hwreg_store_commute RegisterA RegisterDPH) [2,4,6: % #EQ destruct]
611              >(hwreg_store_commute RegisterA RegisterDPL) [2,4,6: % #EQ destruct]
612      |*: >(hwreg_store_commute RegisterDPH RegisterA) [2,4: % #EQ destruct]
613        [ >(hwreg_store_idempotent RegisterA) in ⊢ (???%);
614        | >(hwreg_store_idempotent RegisterA) in ⊢ (???%);
615        ]
616        [2:  >(hwreg_store_commute RegisterA RegisterDPH) [2: % #EQ destruct]
617             >(hwreg_store_commute RegisterA RegisterDPH) [2: % #EQ destruct]
618             >(hwreg_store_commute RegisterA RegisterDPL) [2,4: % #EQ destruct]
619             >(hwreg_store_commute RegisterDPL RegisterDPH) in ⊢ (??%?); [%| % #EQ destruct]
620         |  >(hwreg_store_commute RegisterDPL RegisterA) [2: % #EQ destruct]
621            >(hwreg_store_commute RegisterDPL RegisterDPH) [2: % #EQ destruct]
622            %
623         ]
624      ]
625      [ >(hwreg_store_commute RegisterDPL RegisterDPH) in ⊢ (??%?);
626      | >(hwreg_store_commute RegisterDPL RegisterDPH) in ⊢ (??%?);
627      ]  [2,4: % #EQ destruct]
628      >(hwreg_store_commute RegisterA RegisterST1) [2,4: normalize % #EQ destruct]
629      [ <(hwreg_retrieve_insensitive_to_set_other … RegisterA (carry … st)) ]
630      >(hwreg_store_retrieve_eq RegisterA) %
631    | #off1 #_ @eqb_elim
632      [ #EQ destruct(EQ) normalize nodelta whd in ⊢ (??%?? → ?); #EQ destruct(EQ) % ]
633      #_ normalize nodelta whd in match get_stack; whd in match set_stack;
634      normalize nodelta whd in match set_dp_by_offset; whd in match set_stack_a;
635      normalize nodelta whd in match set_stack_not_a; normalize nodelta
636      whd in match repeat_eval_seq_no_pc; normalize nodelta
637      whd in match preserve_carry_bit; normalize nodelta cases cl -cl
638      normalize nodelta whd in match (m_fold ??????) in ⊢ (??%?? → ?);
639      inversion (eval_seq_no_pc ??????) [2,4: #e #_ normalize nodelta #EQ destruct(EQ)]
640      #st'' whd in match set_regs; whd in match eval_seq_no_pc in ⊢ (% → ?);
641      normalize nodelta whd in match acca_arg_retrieve; normalize nodelta
642      whd in match (acca_arg_retrieve_ ?????); >hwreg_retrieve_hwregstore_hit
643      >m_return_bind whd in match snd_arg_retrieve; normalize nodelta
644      whd in match (snd_arg_retrieve_ ?????); >hwreg_retrieve_hwregstore_miss
645      [2,4: % normalize #EQ destruct] [ >hwreg_retrieve_insensitive_to_set_other]
646      >m_return_bind #H @('bind_inversion H) -H * #x1 #x2 #EQx1x2
647      whd in match acca_store; normalize nodelta whd in match (acca_store_ ??????);
648      >hwreg_store_idempotent >m_return_bind whd in match set_carry;
649      whd in match set_regs; normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ)
650      whd in match (m_fold ??????) in ⊢ (??%?? → ?); whd in match set_regs;
651      normalize nodelta inversion (eval_seq_no_pc ??????)
652      [2,4: #e #_ normalize nodelta #EQ destruct(EQ)] #st''
653      >hwreg_retrieve_hwregstore_hit whd in match eval_seq_no_pc in ⊢ (% → ?);
654      normalize nodelta whd in match acca_arg_retrieve; normalize nodelta
655      whd in match (acca_arg_retrieve_ ?????); >hwreg_retrieve_hwregstore_hit
656      >m_return_bind whd in match snd_arg_retrieve; normalize nodelta
657      whd in match (snd_arg_retrieve_ ?????); >hwreg_retrieve_hwregstore_miss
658      [2,4: normalize % #EQ destruct] >hwreg_retrieve_hwregstore_miss
659      [2,4: normalize % #EQ destruct] >hwreg_retrieve_hwregstore_miss
660      [2,4: normalize % #EQ destruct]  [ >hwreg_retrieve_insensitive_to_set_other]
661      >m_return_bind #H @('bind_inversion H) -H * #y1 #y2 #EQy1y2
662      whd in match acca_store; normalize nodelta whd in match (acca_store_ ??????);
663      >hwreg_store_idempotent >(hwreg_store_commute RegisterDPL RegisterA)
664      [2,4: normalize % #EQ destruct] >hwreg_store_idempotent >m_return_bind
665      whd in match set_carry; whd in match set_regs; normalize nodelta
666      whd in ⊢ (??%% → ?); #EQ destruct(EQ) whd in match (m_fold ??????) in ⊢ (??%?? → ?); whd in match set_regs;
667      normalize nodelta inversion (eval_seq_no_pc ??????)
668      [2,4: #e #_ normalize nodelta #EQ destruct(EQ)] #st'' >hwreg_retrieve_hwregstore_hit
669      whd in match eval_seq_no_pc in ⊢ (% → ?); normalize nodelta whd in match dph_arg_retrieve;
670      whd in match dpl_arg_retrieve; normalize nodelta whd in ⊢ (??%?% → ?);
671      inversion (pointer_of_address ?) [2,4: #e #_ whd in ⊢ (??%?% → ?); #EQ destruct]
672      #ptr >hwreg_retrieve_hwregstore_miss [2,4: normalize % #EQ destruct]
673      [ >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(???%?))?? → ?); [2: normalize % #EQ destruct]
674      | >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(???%?))?? → ?); [2: normalize % #EQ destruct]
675      ]
676      [ >hwreg_retrieve_hwregstore_hit in ⊢ (??(?(???%?))?? → ?);
677      | >hwreg_retrieve_hwregstore_hit in ⊢ (??(?(???%?))?? → ?);
678      ]
679      >hwreg_retrieve_hwregstore_hit in ⊢ (??(?(????%))?? → ?); #EQptr normalize nodelta
680      #H @('bind_inversion H) -H #bv #H lapply(opt_eq_from_res ???? H) -H #EQbv
681      whd in match acca_store; normalize nodelta whd in match (acca_store_ ??????);
682      >(hwreg_store_commute RegisterDPH RegisterA) [2,4: normalize % #EQ destruct]
683      >hwreg_store_idempotent >m_return_bind whd in match set_regs; normalize nodelta
684      whd in ⊢ (??%% → ?); #EQ destruct(EQ) whd in match (m_fold ??????) in ⊢ (??%?? → ?); whd in match set_regs;
685      normalize nodelta inversion (eval_seq_no_pc ??????)
686      [2,4: #e #_ normalize nodelta #EQ destruct(EQ)] #st'' >hwreg_retrieve_hwregstore_hit
687      >(hwreg_store_commute RegisterST1 RegisterA) [2,4: normalize % #EQ destruct]
688      >hwreg_store_idempotent whd in match eval_seq_no_pc in ⊢ (% → ?);
689      normalize nodelta whd in match acca_arg_retrieve; normalize nodelta
690      whd in match (acca_arg_retrieve_ ?????); >hwreg_retrieve_hwregstore_hit
691      >m_return_bind whd in match snd_arg_retrieve; normalize nodelta
692      whd in match (snd_arg_retrieve_ ?????); >hwreg_retrieve_hwregstore_miss
693      [2,4: normalize % #EQ destruct(EQ)] >hwreg_retrieve_hwregstore_miss
694      [2,4: normalize % #EQ destruct(EQ)] >hwreg_retrieve_hwregstore_miss
695      [2,4: normalize % #EQ destruct(EQ)] >hwreg_retrieve_hwregstore_miss
696      [2,4: normalize % #EQ destruct(EQ)]  [ >hwreg_retrieve_insensitive_to_set_other]
697      >m_return_bind #H @('bind_inversion H) -H * #z1 #z2 #EQz1z2
698      whd in match acca_store; normalize nodelta whd in match (acca_store_ ??????);
699      >hwreg_store_idempotent >m_return_bind whd in match set_carry; whd in match set_regs;
700      normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ)
701      whd in match (m_fold ??????) in ⊢ (??%?? → ?); whd in match set_regs;
702      normalize nodelta inversion (eval_seq_no_pc ??????)
703      [2,4: #e #_ normalize nodelta #EQ destruct(EQ)] #st'' >hwreg_retrieve_hwregstore_hit
704      >(hwreg_store_commute RegisterDPL RegisterA) [2,4: normalize % #EQ destruct]
705      >hwreg_store_idempotent whd in match eval_seq_no_pc in ⊢ (% → ?);
706      normalize nodelta whd in match acca_arg_retrieve; normalize nodelta
707      whd in match (acca_arg_retrieve_ ?????); >hwreg_retrieve_hwregstore_hit
708      >m_return_bind whd in match snd_arg_retrieve; normalize nodelta
709      whd in match (snd_arg_retrieve_ ?????); >hwreg_retrieve_hwregstore_miss
710      [2,4: normalize % #EQ destruct(EQ)] >hwreg_retrieve_hwregstore_miss
711      [2,4: normalize % #EQ destruct(EQ)] >hwreg_retrieve_hwregstore_miss
712      [2,4: normalize % #EQ destruct(EQ)] >hwreg_retrieve_hwregstore_miss
713      [2,4: normalize % #EQ destruct(EQ)] >hwreg_retrieve_hwregstore_miss
714      [2,4: normalize % #EQ destruct(EQ)] [ >hwreg_retrieve_insensitive_to_set_other]
715      >m_return_bind #H @('bind_inversion H) -H * #w1 #w2 #EQw1w2 whd in match acca_store;
716      normalize nodelta whd in match (acca_store_ ??????); >hwreg_store_idempotent
717      >m_return_bind whd in match set_regs; whd in match set_carry; normalize nodelta
718      whd in ⊢ (??%% → ?); #EQ destruct(EQ) whd in match (m_fold ??????) in ⊢ (??%?? → ?); whd in match set_regs;
719      normalize nodelta inversion (eval_seq_no_pc ??????)
720      [2,4: #e #_ normalize nodelta #EQ destruct(EQ)] #st''
721      [ >hwreg_retrieve_hwregstore_miss in ⊢ (??(??????(?????(??%?)??))?? → ?);
722        [2: normalize % #EQ destruct]
723        >hwreg_retrieve_hwregstore_miss in ⊢ (??(??????(?????(??%?)??))?? → ?);
724        [2: normalize % #EQ destruct]
725        >hwreg_retrieve_hwregstore_miss in ⊢ (??(??????(?????(??%?)??))?? → ?);
726        [2: normalize % #EQ destruct]
727         >hwreg_retrieve_hwregstore_hit in ⊢ (??(??????(?????(??%?)??))?? → ?);
728      | >hwreg_retrieve_hwregstore_miss in ⊢ (??(??????(?????(??%?)??))?? → ?);
729        [2: normalize % #EQ destruct]
730        >hwreg_retrieve_hwregstore_miss in ⊢ (??(??????(?????(??%?)??))?? → ?);
731        [2: normalize % #EQ destruct]
732        >hwreg_retrieve_hwregstore_miss in ⊢ (??(??????(?????(??%?)??))?? → ?);
733        [2: normalize % #EQ destruct]
734         >hwreg_retrieve_hwregstore_hit in ⊢ (??(??????(?????(??%?)??))?? → ?);
735      ]
736      >hwreg_retrieve_hwregstore_hit >(hwreg_store_commute RegisterDPH RegisterA)
737      [2,4: normalize % #EQ destruct]  >hwreg_store_idempotent
738      whd in match eval_seq_no_pc in ⊢ (% → ?); normalize nodelta
739      whd in match dph_arg_retrieve; whd in match dpl_arg_retrieve; normalize nodelta;
740      whd in ⊢ (??%?% → ?); inversion (pointer_of_address ?); [2,4: #e #_ whd in ⊢ (??%?% → ?); #EQ destruct]
741      #ptr1 >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(???%?))?? → ?); [2,4: normalize % #EQ destruct]
742      [ >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(???%?))?? → ?); [2: normalize % #EQ destruct]
743        >hwreg_retrieve_hwregstore_hit in ⊢ (??(?(???%?))?? → ?);
744        >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(????%))?? → ?); [2: normalize % #EQ destruct]
745        >hwreg_retrieve_hwregstore_hit in ⊢ (??(?(????%))?? → ?);     
746      | >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(???%?))?? → ?); [2: normalize % #EQ destruct]
747        >hwreg_retrieve_hwregstore_hit in ⊢ (??(?(???%?))?? → ?);
748        >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(????%))?? → ?); [2: normalize % #EQ destruct]
749        >hwreg_retrieve_hwregstore_hit in ⊢ (??(?(????%))?? → ?);
750      ]
751      #EQptr1 normalize nodelta whd in match acca_arg_retrieve; normalize nodelta
752      whd in match (acca_arg_retrieve_ ?????); >hwreg_retrieve_hwregstore_hit
753      >m_return_bind #H @('bind_inversion H) -H #m1 #H lapply(opt_eq_from_res ???? H)
754      -H #EQm1 whd in match set_m; normalize nodelta whd in ⊢ (??%% → ?);
755      #EQ destruct(EQ) whd in match (m_fold ??????) in ⊢ (??%?? → ?);
756      [ >other_bit_insensitive_to_reg_store >other_bit_insensitive_to_reg_store
757        >other_bit_insensitive_to_reg_store >other_bit_insensitive_to_reg_store
758        >other_bit_insensitive_to_reg_store >other_bit_insensitive_to_reg_store
759        whd in match set_carry; normalize nodelta ]
760      #EQ destruct(EQ) @sym_eq whd in match read_arg_decision; normalize nodelta
761      >m_return_bind >m_return_bind >EQx1x2 >m_return_bind >EQy1y2
762      >m_return_bind >EQptr >m_return_bind >EQbv >m_return_bind
763      whd in match set_regs; whd in match write_decision; normalize nodelta
764      whd in match hw_reg_retrieve; normalize nodelta
765      >hwreg_retrieve_hwregstore_miss [2,4: normalize % #EQ destruct]
766      [ >hwreg_retrieve_hwregstore_miss in ⊢ (??(????(????%?)?)?);
767         [2: normalize % #EQ destruct]
768        >hwreg_retrieve_hwregstore_miss in ⊢ (??(????(????%?)?)?);
769        [2: normalize % #EQ destruct]
770      | >hwreg_retrieve_hwregstore_miss in ⊢ (??(????(????%?)?)?);
771        [2: normalize % #EQ destruct]
772        >hwreg_retrieve_hwregstore_miss in ⊢ (??(????(????%?)?)?);
773        [2: normalize % #EQ destruct]
774      ]
775      >m_return_bind >hwreg_retrieve_hwregstore_miss [2,4: normalize % #EQ destruct]
776      >hwreg_retrieve_hwregstore_miss [2,4: normalize % #EQ destruct]
777      >hwreg_retrieve_hwregstore_miss [2,4: normalize % #EQ destruct]
778      >m_return_bind >EQz1z2 >m_return_bind
779      >EQw1w2 >m_return_bind >EQptr1 >m_return_bind >EQm1 >m_return_bind
780       whd in match set_m; whd in match set_carry; whd in match set_regs;
781       normalize nodelta
782       @eq_f whd in match (other_bit ?); whd in match set_carry; normalize nodelta
783       @eq_f3 [2,3,5,6: %]
784       [ >(hwreg_store_commute RegisterDPH RegisterDPL) in ⊢ (???%); [2: normalize % #EQ destruct]
785         >(hwreg_store_commute RegisterA RegisterDPL) in ⊢ (???%); [2: normalize % #EQ destruct]
786         >(hwreg_store_commute RegisterST1 RegisterDPL) in ⊢ (??%?); [2: normalize % #EQ destruct]
787       | >(hwreg_store_commute RegisterDPH RegisterDPL) in ⊢ (???%); [2: normalize % #EQ destruct]
788         >(hwreg_store_commute RegisterA RegisterDPL) in ⊢ (???%); [2: normalize % #EQ destruct]
789         >(hwreg_store_commute RegisterST1 RegisterDPL) in ⊢ (??%?); [2: normalize % #EQ destruct]           
790       ] [<hwreg_store_set_other_commut] @eq_f3 [1,2,4,5: %]
791       [ >(hwreg_store_commute RegisterA RegisterDPH) in ⊢ (???%); [2: normalize % #EQ destruct]
792         >(hwreg_store_commute RegisterST1 RegisterDPH) in ⊢ (??%?); [2: normalize % #EQ destruct]
793       | >(hwreg_store_commute RegisterA RegisterDPH) in ⊢ (???%); [2: normalize % #EQ destruct]
794         >(hwreg_store_commute RegisterST1 RegisterDPH) in ⊢ (??%?); [2: normalize % #EQ destruct]
795       ] [<hwreg_store_set_other_commut] @eq_f3 [1,2,4,5: %]
796       [ <hwreg_store_set_other_commut <hwreg_store_set_other_commut
797         <hwreg_store_set_other_commut ]
798         >(hwreg_store_commute RegisterA RegisterST1) in ⊢ (???%); [2,4: normalize % #EQ destruct]         
799          @eq_f3 [1,2,4,5: %] @eq_f3 [1,2,4,5: %]
800         [<hwreg_store_set_other_commut ]
801         >(hwreg_store_commute RegisterDPL RegisterDPH) in ⊢ (??%?);
802         [2,4: normalize % #EQ destruct] %
803    | #by #_ whd in match preserve_carry_bit; whd in match set_stack_int; normalize nodelta
804      cases cl -cl normalize nodelta whd in match repeat_eval_seq_no_pc; normalize nodelta     
805      whd in match (m_fold ??????) in ⊢ (??%?? → ?); whd in match set_regs;
806      normalize nodelta inversion (eval_seq_no_pc ??????)
807      [2,4: #e #_ normalize nodelta #EQ destruct(EQ)] #st'' whd in match eval_seq_no_pc in ⊢ (% → ?);
808      normalize nodelta whd in match acca_arg_retrieve; normalize nodelta
809      whd in match (acca_arg_retrieve_ ?????); >hwreg_retrieve_hwregstore_hit
810      >m_return_bind whd in match snd_arg_retrieve; normalize nodelta
811      whd in match (snd_arg_retrieve_ ?????); >hwreg_retrieve_hwregstore_miss
812      [2,4: normalize % #EQ destruct] [ >hwreg_retrieve_insensitive_to_set_other]
813      >m_return_bind #H @('bind_inversion H) -H * #x1 #x2 #EQx1x2
814      whd in match acca_store; normalize nodelta whd in match (acca_store_ ??????);
815      >hwreg_store_idempotent >m_return_bind whd in match set_carry; whd in match set_regs;
816      normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ)
817      whd in match (m_fold ??????) in ⊢ (??%?? → ?); whd in match set_regs;
818      normalize nodelta inversion (eval_seq_no_pc ??????)
819      [2,4: #e #_ normalize nodelta #EQ destruct(EQ)] #st'' >hwreg_retrieve_hwregstore_hit
820      >(hwreg_store_commute RegisterDPL RegisterA) [2,4: normalize % #EQ destruct]
821      >hwreg_store_idempotent whd in match eval_seq_no_pc in ⊢ (% → ?);
822      normalize nodelta whd in match acca_arg_retrieve; normalize nodelta
823      whd in match (acca_arg_retrieve_ ?????); >hwreg_retrieve_hwregstore_hit
824      >m_return_bind whd in match snd_arg_retrieve; normalize nodelta
825      whd in match (snd_arg_retrieve_ ?????); >hwreg_retrieve_hwregstore_miss
826      [2,4: normalize % #EQ destruct] >hwreg_retrieve_hwregstore_miss
827      [2,4: normalize % #EQ destruct]  [ >hwreg_retrieve_insensitive_to_set_other]
828      >m_return_bind #H @('bind_inversion H) -H * #y1 #y2 #EQy1y2
829      whd in match acca_store; normalize nodelta whd in match (acca_store_ ??????);
830      >hwreg_store_idempotent >m_return_bind whd in match set_regs; whd in match set_carry;
831      normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ)
832      whd in match (m_fold ??????) in ⊢ (??%?? → ?); whd in match set_regs;
833      normalize nodelta inversion (eval_seq_no_pc ??????)
834      [2,4: #e #_ normalize nodelta #EQ destruct(EQ)] #st'' >hwreg_retrieve_hwregstore_hit
835      >(hwreg_store_commute RegisterDPH RegisterA) [2,4: normalize % #EQ destruct]
836      >hwreg_store_idempotent whd in match eval_seq_no_pc in ⊢ (% → ?);
837      normalize nodelta whd in match dph_arg_retrieve; normalize nodelta
838      whd in ⊢ (??%?% → ?); inversion (pointer_of_address ?) [2,4: #e #_ whd in ⊢ (??%?% → ?); #EQ destruct]
839      #ptr >hwreg_retrieve_hwregstore_miss [2,4: normalize % #EQ destruct]
840      [ >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(???%?))?? → ?); [2: normalize % #EQ destruct]
841        >hwreg_retrieve_hwregstore_hit in ⊢ (??(?(???%?))?? → ?);
842        >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(????%))?? → ?); [2: normalize % #EQ destruct]
843        >hwreg_retrieve_hwregstore_hit in ⊢ (??(?(????%))?? → ?);
844      | >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(???%?))?? → ?); [2: normalize % #EQ destruct]
845        >hwreg_retrieve_hwregstore_hit in ⊢ (??(?(???%?))?? → ?);
846        >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(????%))?? → ?); [2: normalize % #EQ destruct]
847        >hwreg_retrieve_hwregstore_hit in ⊢ (??(?(????%))?? → ?);
848      ]
849      #EQptr normalize nodelta whd in match acca_arg_retrieve; normalize nodelta
850      whd in match (acca_arg_retrieve_ ?????); >hwreg_retrieve_hwregstore_hit
851      >m_return_bind #H @('bind_inversion H) -H #m #H lapply(opt_eq_from_res ???? H) -H
852      #EQm whd in match set_m; normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ)
853      whd in match (m_fold ??????) in ⊢ (??%?? → ?); whd in match set_regs;
854      normalize nodelta whd in match set_carry; normalize nodelta
855      [ >other_bit_insensitive_to_reg_store >other_bit_insensitive_to_reg_store
856        >other_bit_insensitive_to_reg_store whd in match hwreg_set_other; normalize nodelta ]
857      #EQ destruct(EQ) @sym_eq whd in match read_arg_decision; normalize nodelta
858      >m_return_bind whd in match write_decision; normalize nodelta whd in match set_regs;
859      whd in match hw_reg_retrieve; normalize nodelta >hwreg_retrieve_hwregstore_miss
860      [2,4: % normalize #EQ destruct] >m_return_bind  >hwreg_retrieve_hwregstore_miss
861      [2,4: % normalize #EQ destruct] >m_return_bind >EQx1x2 >m_return_bind >EQy1y2
862      >m_return_bind >EQptr >m_return_bind >EQm >m_return_bind whd in match set_m;
863      whd in match set_regs; normalize nodelta @eq_f whd in match set_carry;
864      normalize nodelta @eq_f3 [2,3,5,6: %]
865      [ >(hwreg_store_commute RegisterDPH RegisterA) in ⊢ (??%?); [2: % normalize #EQ destruct]
866        >(hwreg_store_commute RegisterDPL RegisterA) in ⊢ (??%?); [2: % normalize #EQ destruct]
867      | >(hwreg_store_commute RegisterDPH RegisterA) in ⊢ (??%?); [2: % normalize #EQ destruct]
868        >(hwreg_store_commute RegisterDPL RegisterA) in ⊢ (??%?); [2: % normalize #EQ destruct]
869      ]
870      [2: @eq_f3 [1,2: %] >(hwreg_store_commute RegisterDPL RegisterDPH) in ⊢ (??%?);
871         [2: % normalize #EQ destruct]
872      |  >(hwreg_store_commute RegisterDPL RegisterDPH) in ⊢ (??%?); [2: % normalize #EQ destruct]
873      ]
874      %   
875    ] 
876  | #r cases src -src
877    [ #r1 * #H1 #H2 normalize nodelta @eq_Register_elim
878      [ #EQ destruct(EQ) normalize nodelta whd in ⊢ (??%?% → ?); #EQ destruct(EQ) % ]
879      #H3 normalize nodelta @eq_Register_elim normalize nodelta
880      [ #EQ destruct(EQ) whd in match repeat_eval_seq_no_pc; normalize nodelta
881        whd in match (m_fold ??????) in ⊢ (??%?? → ?); #EQ destruct(EQ)
882        @sym_eq whd in match read_arg_decision; normalize nodelta >m_return_bind
883        whd in match write_decision; normalize nodelta >m_return_bind
884        whd in match set_regs; normalize nodelta @eq_f % ]
885      #H4 normalize nodelta @eq_Register_elim
886      [ #EQ destruct(EQ) | #H5] normalize nodelta whd in ⊢ (??%?% → ?);
887      whd in match set_regs; normalize nodelta [2: >hwreg_retrieve_hwregstore_hit ]
888      #EQ destruct(EQ) @sym_eq whd in match read_arg_decision; normalize nodelta
889      >m_return_bind whd in match write_decision; normalize nodelta >m_return_bind
890      @eq_f whd in match set_regs; normalize nodelta cases cl normalize nodelta
891      @eq_f3 try % @eq_f3 [1,2,4,5: %] >hwreg_store_retrieve_eq %
892    | #n #_ normalize nodelta whd in match preserve_carry_bit; whd in match get_stack;
893      normalize nodelta whd in match set_dp_by_offset; normalize nodelta
894      cases cl -cl [ letin CL_TRUE ≝ it | letin CL_FALSE ≝ it ]
895      normalize nodelta whd in match repeat_eval_seq_no_pc;
896      normalize nodelta  whd in match (m_fold ??????) in ⊢ (??%?? → ?); whd in match set_regs;
897      normalize nodelta inversion (eval_seq_no_pc ??????)
898      [2,4: #e #_ normalize nodelta #EQ destruct(EQ)] #st''
899      whd in match eval_seq_no_pc in ⊢ (% → ?); normalize nodelta
900      whd in match acca_arg_retrieve; normalize nodelta
901      whd in match (acca_arg_retrieve_ ?????); >hwreg_retrieve_hwregstore_hit
902      >m_return_bind whd in match snd_arg_retrieve; normalize nodelta
903      whd in match (snd_arg_retrieve_ ?????); >hwreg_retrieve_hwregstore_miss
904      [2,4: normalize % #EQ destruct(EQ)] [ >hwreg_retrieve_insensitive_to_set_other]
905      >m_return_bind #H @('bind_inversion H) -H * #x1 #x2 #EQx1x2
906      whd in match acca_store; normalize nodelta whd in match (acca_store_ ??????);
907      >hwreg_store_idempotent >m_return_bind whd in match set_regs;     
908      whd in match set_carry; normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ)
909      whd in match (m_fold ??????) in ⊢ (??%?? → ?); whd in match set_regs;
910      normalize nodelta inversion (eval_seq_no_pc ??????)
911      [2,4: #e #_ normalize nodelta #EQ destruct(EQ)] #st'' >hwreg_retrieve_hwregstore_hit
912      whd in match eval_seq_no_pc in ⊢ (% → ?); normalize nodelta
913      whd in match acca_arg_retrieve; normalize nodelta
914      whd in match (acca_arg_retrieve_ ?????); >hwreg_retrieve_hwregstore_hit
915      >m_return_bind whd in match snd_arg_retrieve; normalize nodelta
916      whd in match (snd_arg_retrieve_ ?????); >hwreg_retrieve_hwregstore_miss
917      [2,4: normalize % #EQ destruct(EQ)] >hwreg_retrieve_hwregstore_miss
918      [2,4: normalize % #EQ destruct(EQ)] >hwreg_retrieve_hwregstore_miss
919      [2,4: normalize % #EQ destruct(EQ)] [ >hwreg_retrieve_insensitive_to_set_other]
920      >m_return_bind #H @('bind_inversion H) -H * #y1 #y2 #EQy1y2
921      whd in match acca_store; normalize nodelta whd in match (acca_store_ ??????);
922      >hwreg_store_idempotent >(hwreg_store_commute RegisterDPL RegisterA)
923      [2,4: normalize % #EQ destruct(EQ)] >hwreg_store_idempotent
924      >m_return_bind whd in match set_carry; whd in match set_regs; normalize nodelta
925      whd in ⊢ (??%% → ?); #EQ destruct(EQ)
926      whd in match (m_fold ??????) in ⊢ (??%?? → ?); whd in match set_regs;
927      normalize nodelta inversion (eval_seq_no_pc ??????)
928      [2,4: #e #_ normalize nodelta #EQ destruct(EQ)] #st'' >hwreg_retrieve_hwregstore_hit
929      whd in match eval_seq_no_pc in ⊢ (% → ?); normalize nodelta
930      whd in ⊢ (??%?? → ?); inversion (pointer_of_address ?)
931      [2,4: #e #_ whd in ⊢ (??%?% → ?); #EQ destruct(EQ)] #ptr >hwreg_retrieve_hwregstore_miss
932      [2,4: normalize % #EQ destruct(EQ)]
933      [ >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(???%?))?? → ?);
934        [2,4: normalize % #EQ destruct(EQ)]
935        >hwreg_retrieve_hwregstore_hit in ⊢ (??(?(???%?))?? → ?);
936        >hwreg_retrieve_hwregstore_hit in ⊢ (??(?(????%))?? → ?);
937      | >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(???%?))?? → ?);
938        [2,4: normalize % #EQ destruct(EQ)]
939        >hwreg_retrieve_hwregstore_hit in ⊢ (??(?(???%?))?? → ?);
940        >hwreg_retrieve_hwregstore_hit in ⊢ (??(?(????%))?? → ?);
941      ]
942      #EQptr normalize nodelta #H @('bind_inversion H) -H #bv #H
943      lapply(opt_eq_from_res ???? H) -H #EQbv whd in match acca_store;
944      normalize nodelta whd in match (acca_store_ ??????);
945      >(hwreg_store_commute RegisterDPH RegisterA)
946      [2,4: normalize % #EQ destruct(EQ)] >hwreg_store_idempotent
947      >m_return_bind whd in match set_regs; normalize nodelta whd in ⊢ (??%% → ?);
948      #EQ destruct(EQ) @eq_Register_elim [1,3: #EQ destruct(EQ) |*: #H1 ]
949      normalize nodelta whd in match (m_fold ??????) in ⊢ (??%?? → ?); whd in match set_regs;
950      normalize nodelta whd in match set_carry; whd in match set_regs;
951      normalize nodelta
952      [1,3: >other_bit_insensitive_to_reg_store >other_bit_insensitive_to_reg_store
953            >other_bit_insensitive_to_reg_store
954            [2: >other_bit_insensitive_to_reg_store ] ]
955      [1,4: >hwreg_retrieve_hwregstore_hit ] #EQ destruct(EQ) @sym_eq
956      whd in match read_arg_decision; normalize nodelta >m_return_bind
957      >m_return_bind >EQx1x2 >m_return_bind >EQy1y2 >m_return_bind
958      >EQptr >m_return_bind >EQbv >m_return_bind whd in match write_decision;
959      normalize nodelta whd in match set_regs; normalize nodelta
960      whd in match hw_reg_store; normalize nodelta >m_return_bind
961      @eq_f whd in match set_carry; whd in match (other_bit ?); normalize nodelta @eq_f3 [2,3,5,6,8,9,11,12: %]
962      [1,3: <hwreg_store_set_other_commut <hwreg_store_set_other_commut
963            <hwreg_store_set_other_commut [ <hwreg_store_set_other_commut]]
964      @eq_f3 [1,2,4,5,7,8,10,11: %]
965      >(hwreg_store_commute RegisterDPL RegisterDPH) in ⊢ (??%?);
966      [2,4,6,8: % normalize #EQ destruct] %
967    | #by #_ normalize nodelta @eq_Register_elim [#EQ destruct(EQ) | #H1 ]
968      whd in ⊢ (??%?? → ?); whd in match set_regs; normalize nodelta #EQ destruct(EQ)
969      @sym_eq whd in match read_arg_decision; normalize nodelta >m_return_bind
970      whd in match write_decision; normalize nodelta >m_return_bind
971      @eq_f whd in match set_regs; normalize nodelta [%] @eq_f3 [2,3: %]
972      >hwreg_retrieve_hwregstore_hit %
973    ]
974  ] 
975| cases daemon (*TODO*)
976] *)
977cases daemon qed.
978
979definition sigma_beval : fixpoint_computer → coloured_graph_computer → 
980  ertl_program → (block → list register) → lbl_funct_type →
981  regs_funct_type → beval → beval≝
982 λfix_comp,build,prog,init_regs,f_lbls,f_regs,bv.
983  let init ≝ (λglobals,fn.«translate_data fix_comp build globals fn,?») in
984  let m ≝ (\snd (\fst (ertl_to_ltl fix_comp build prog))) in
985  let stacksizes ≝ lookup_stack_cost … m in
986  match bv with
987  [ BVpc pc p ⇒ match sigma_pc_opt ERTL_semantics LTL_semantics prog stacksizes
988                       init init_regs f_lbls f_regs pc
989                with [Some pc' ⇒ BVpc pc' p | None ⇒ BVundef]
990  | _ ⇒ bv
991  ].
992  @hide_prf % qed.
993
994axiom ps_reg_retrieve_hw_reg_retrieve_commute :
995∀fix_comp,colour,prog,init_regs,f_lbls,f_regs,fn,pc.
996let after ≝ (analyse_liveness fix_comp (prog_names … prog) fn) in
997gen_preserving2 ?? gen_res_preserve ??????
998     (state_rel fix_comp colour prog pc)
999     (λr : register.λd : arg_decision.d =
1000      (colouring … (colour (prog_names … prog) fn after)
1001       (inl register Register r)))
1002     (λbv,bv'.bv = sigma_beval fix_comp colour prog init_regs f_lbls f_regs bv') …
1003     (λst1.ps_reg_retrieve (regs … st1))
1004     (λst,d.m_map Res ?? (\fst …)
1005      (read_arg_decision (joint_if_local_stacksize ?? fn) st d)).
1006     
1007(*set_theoretical axioms *)
1008axiom set_member_empty :∀A.∀DEC.∀a.¬set_member A DEC a (set_empty …).   
1009axiom set_member_singl : ∀A,DEC,a.set_member A DEC a (set_singleton … a).
1010axiom set_member_union1 : ∀A,DEC,x,y,a.set_member A DEC a x →
1011set_member A DEC a (set_union … x y).
1012axiom set_member_union2 : ∀A,DEC,x,y,a.set_member A DEC a y →
1013set_member A DEC a (set_union … x y).
1014axiom set_member_diff : ∀A,DEC,x,y,a.set_member A DEC a x →
1015¬set_member A DEC a y →
1016set_member A DEC a (set_diff … x y).
1017axiom set_member_subset_if:
1018 ∀A,DEC,S1,S2.
1019  set_subset A DEC S1 S2 →
1020   ∀x. set_member A DEC x S1 → set_member A DEC x S2.
1021axiom set_member_subset_onlyif:
1022 ∀A,DEC,S1,S2.
1023  (∀x. set_member A DEC x S1 → set_member A DEC x S2) →
1024   set_subset A DEC S1 S2.
1025   
1026lemma all_used_are_live_before :
1027∀fix_comp.
1028∀prog : ertl_program.
1029∀fn : joint_closed_internal_function ERTL (prog_names … prog).
1030∀l,stmt.
1031stmt_at … (joint_if_code … fn) l = return stmt →
1032∀r : register. set_member ? (eq_identifier …) r (\fst (used ? stmt)) →
1033let after ≝ (analyse_liveness fix_comp (prog_names … prog) fn) in
1034eliminable ? (after l) stmt = false →
1035lives (inl ? ? r)  (livebefore  … fn after l).
1036#fix_comp #prog #fn #l *
1037[ * [#c|* [#c_id | #c_ptr] #args #dest | #a #lbl | *
1038[ #str
1039| * * [#r1 | #R1]  * [1,3: * [1,3: #r |2,4: #R] |2,4: #b]
1040| #a
1041| * [ #r | #b]
1042| #i #i_spec #w #dpl #dph
1043| #op #a #b * [#r | #by]  * [1,3: #r'|2,4: #by']
1044| #op #a #a'
1045| * #a #a' * [1,3,5,7,9,11: #r |2,4,6,8,10,12: #b]
1046|
1047|
1048| #a #dpl #dph
1049| #dpl #dph #a
1050| * [|| #r ] (*|| * [|| #r] | #r #lbl | #r #lbl ] *)
1051]
1052] #nxt| * [ #lbl | | *] |*]
1053#EQstmt #r #H #H1 whd in match (lives ??); normalize  nodelta
1054whd in match (livebefore ????);  whd in EQstmt : (??%?); >EQstmt
1055normalize nodelta -EQstmt whd in match (statement_semantics ???);
1056whd in match(\fst ?); try( @(set_member_union2) assumption) >H1
1057normalize nodelta whd in match(\fst ?); @(set_member_union2) assumption
1058qed.
1059
1060lemma bool_of_beval_sigma_commute :
1061∀fix_comp,colour,prog,init_regs,f_lbls,f_regs.
1062gen_preserving … gen_res_preserve …
1063(λbv,bv'.bv = sigma_beval fix_comp colour prog init_regs f_lbls f_regs bv')
1064(λb1,b2.b1=b2) … bool_of_beval bool_of_beval.
1065#fix_comp #colour #prog #init_regs #f_lbls #f_regs whd in match bool_of_beval;
1066normalize nodelta * normalize nodelta
1067[|| #p1 #p2 #p| #b| #p | #ptr #p | #pc #p ]
1068try (#y #_ @res_preserve_error_gen)
1069* whd in match sigma_beval; normalize nodelta
1070[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'
1071|6,13,20,27: #ptr' #p'|7,14,21,28: #pc' #p'] #EQ destruct(EQ) try (@m_gen_return %)
1072cases(sigma_pc_opt ?????????) in EQ; normalize nodelta
1073[2,4,6,8: #pc''] #EQ destruct(EQ)
1074qed.
1075
1076lemma map_eval_add_dummy_variance_id :
1077∀X,Y.∀l,x.map_eval X Y (add_dummy_variance X Y l) x =l.
1078#X #Y #l elim l [//] #hd #tl normalize #IH #x >IH %
1079qed.
1080
1081lemma state_pc_eq : ∀p.∀st1,st2 : state_pc p.
1082st1 = st2 → st_no_pc … st1 = st_no_pc … st2 ∧
1083pc … st1 = pc … st2 ∧ last_pop … st1 = last_pop … st2.
1084#p * #st1 #pc1 #lp1 * #st2 #pc2 #lp2 #EQ destruct(EQ)
1085%{(refl …)} %{(refl …)} %
1086qed.
1087
1088(* Cut&paste da un altro file con nome split_on_last_append, unificare*)
1089lemma split_on_last_append_singl : ∀A : Type[0]. ∀pre : list A.
1090∀ last : A. split_on_last ? (pre@[last]) = return 〈pre,last〉.
1091#A #pre elim pre [#last %] #a #tl #IH #last whd in ⊢ (??%?);lapply(IH last)
1092whd in ⊢ (??%? → ?); #EQ >EQ %
1093qed.
1094
1095lemma split_on_last_append : ∀A : Type[0]. ∀l1,l2: list A.
1096 OptPred True (λres.
1097  split_on_last ? (l1@l2) = return 〈l1 @ \fst res, \snd res〉)
1098  (split_on_last … l2).
1099#A #l1 #l2 lapply l1 -l1 @(list_elim_left … l2) //
1100#hd #tl #IH #l1 whd >split_on_last_append_singl whd
1101<associative_append @split_on_last_append_singl
1102qed.
1103
1104lemma injective_OK: ∀A:Type[0].∀a,b:A. OK … a = OK … b → a=b.
1105 #A #a #b #EQ destruct %
1106qed.
1107
1108lemma eq_notb_true_to_eq_false:
1109 ∀b. (¬b) = true → b = false.
1110* // #abs normalize in abs; destruct
1111qed.
1112
1113lemma fold_insert_singleton : ∀A,B : Type[0].∀a :A.
1114∀i : Pos.∀f,b.
1115fold A B f (pm_set A i (Some ? a) (pm_leaf A)) b = f i a b.
1116#A #B #a #i elim i -i normalize
1117[//] #i #IH #f #b @IH
1118qed.
1119
1120lemma eq_f' : ∀A,B : Type[0].∀f,g : A → B. ∀x,y : A.
1121(∀w. f w = g w) → x = y → f x = g y. //
1122qed.
1123
1124lemma add_find_all_miss :  ∀tag,A.∀m : identifier_map tag A.
1125∀P : (identifier tag → A → bool).∀i,a.notb (P i a) →
1126find_all tag A (add tag A m i a) P =
1127match lookup tag A m i with
1128[ None ⇒ find_all tag A m P
1129| Some a ⇒ if P i a then find_all tag A (remove tag A m i) P else find_all tag A m P
1130].
1131cases daemon
1132qed.
1133   
1134     
1135lemma sigma_fb_state_insensitive_to_dead_reg:
1136 ∀prog,bv. ∀st: state ERTL_semantics. ∀l:label.
1137 ∀r: register. ∀before.
1138  set_member … (eq_identifier RegisterTag) r (\fst  (before l)) = false →
1139  sigma_fb_state prog
1140   (to_be_cleared_fb before l)
1141   (set_regs ERTL_semantics
1142    〈reg_store r bv (\fst  (regs ERTL_semantics st)),
1143    \snd  (regs ERTL_semantics st)〉 st)
1144  = sigma_fb_state prog (to_be_cleared_fb before l) st.
1145#prog #bv #st #l #r #before #dead whd in match sigma_fb_state; normalize nodelta
1146@eq_f3 [2,3: %] whd in match set_regs; normalize nodelta whd in match sigma_fb_regs;
1147normalize nodelta @eq_f2 [2: %] whd in match sigma_fb_register_env;
1148normalize nodelta whd in match reg_store; normalize nodelta
1149>add_find_all_miss [2: normalize >dead %] cases(lookup ????) [%] #a
1150normalize nodelta whd in match to_be_cleared_fb; whd in match lives;
1151normalize nodelta whd in match (plives ??); >dead %
1152qed.
1153
1154lemma sigma_fb_state_insensitive_to_dead_Reg:
1155 ∀prog,bv. ∀st: state ERTL_semantics. ∀l:label.
1156 ∀r: Register. ∀before.
1157  set_member … eq_Register r (\snd  (before l)) = false →
1158  sigma_fb_state prog
1159   (to_be_cleared_fb before l)
1160   (set_regs ERTL_semantics
1161     〈\fst  (regs ERTL_semantics st),
1162      hwreg_store r bv (\snd  (regs ERTL_semantics st))〉
1163      st)
1164  = sigma_fb_state prog (to_be_cleared_fb before l) st.
1165cases daemon (*TODO*)
1166qed.
1167
1168lemma sigma_fb_state_insensitive_to_dead_carry:
1169 ∀prog,bv. ∀st: state ERTL_semantics. ∀l:label. ∀before.
1170  set_member Register eq_Register RegisterCarry (\snd (before l)) = false →
1171   sigma_fb_state prog (to_be_cleared_fb before l) (set_carry ERTL_semantics bv st) =
1172   sigma_fb_state prog (to_be_cleared_fb before l) st.
1173#prog #b #st #l #cefore #dead whd in match sigma_fb_state; normalize nodelta
1174whd in match set_carry; normalize nodelta whd in match to_be_cleared_fb;
1175normalize nodelta whd in match (lives ??); >dead %
1176qed.
1177
1178lemma split_orb_false: ∀a,b:bool. orb a b = false → a = false ∧ b = false.
1179 ** normalize #abs destruct /2/
1180qed.
1181
1182lemma eta_set_carry:
1183 ∀P,st. set_carry P (carry P st) st = st.
1184#P * //
1185qed.
1186
1187lemma set_carry_set_regs_commute:
1188 ∀P,st,c,v. set_carry P c (set_regs P v st) = set_regs P v (set_carry P c st).
1189 #P * //
1190qed.
1191
1192lemma eliminable_step_to_eq_livebefore_liveafter:
1193 ∀prog,stackcost,fn.
1194 let p_in ≝ mk_prog_params ERTL_semantics prog stackcost in
1195 ∀st1: joint_abstract_status p_in.
1196 ∀stms: joint_seq ERTL_semantics (prog_names … prog). ∀next.
1197 let pt ≝ point_of_pc ERTL_semantics (pc ? st1) in
1198 stmt_at p_in ? (joint_if_code p_in … fn) pt = return (sequential … stms next) →
1199 ∀liveafter.
1200 eliminable_step (globals … p_in) (liveafter (point_of_pc ERTL_semantics (pc … st1))) stms = true →
1201  livebefore … fn liveafter pt = liveafter pt.
1202 #prog #stackcost #fn #st1 #stms #next #stmt_at #liveafter #Helim
1203 whd in ⊢ (??%?); whd in stmt_at:(??%?); cases (lookup ????) in stmt_at;
1204 normalize nodelta try (#abs whd in abs:(??%%); destruct (abs) @I)
1205 #stms' #EQ whd in EQ:(??%%); destruct (EQ) whd in ⊢ (??%?);
1206 whd in match eliminable; normalize nodelta >Helim %
1207qed.
1208
1209lemma set_subset_to_set_subst_set_union_left:
1210 ∀T,eqT,A,B,C. set_subset T eqT A B → set_subset … eqT A (set_union … B C).
1211 #T #eqT #A #B #C #H @set_member_subset_onlyif #x #K
1212 lapply (set_member_subset_if … H) #H2 /3 by set_member_union1/
1213qed.
1214
1215lemma set_subset_to_set_subst_set_union_right:
1216 ∀T,eqT,A,B,C. set_subset T eqT A C → set_subset … eqT A (set_union … B C).
1217 #T #eqT #A #B #C #H @set_member_subset_onlyif #x #K
1218 lapply (set_member_subset_if … H) #H2 /3 by set_member_union2/
1219qed.
1220
1221lemma rl_included_rl_join_left:
1222 ∀A,B,C. rl_included A B → rl_included A (rl_join B C).
1223 #A #B #C whd in match rl_included; normalize nodelta #H
1224 cases (andb_Prop_true … H) -H #H1 #H2 @andb_Prop
1225 /2 by set_subset_to_set_subst_set_union_left/
1226qed.
1227
1228lemma rl_included_rl_join_right:
1229 ∀A,B,C. rl_included A C → rl_included A (rl_join B C).
1230 #A #B #C whd in match rl_included; normalize nodelta #H
1231 cases (andb_Prop_true … H) -H #H1 #H2 @andb_Prop
1232 /2 by set_subset_to_set_subst_set_union_right/
1233qed.
1234
1235lemma set_subset_reflexive: ∀A,DEC,x. set_subset A DEC x x.
1236 /2/
1237qed.
1238
1239lemma rl_included_reflexive: ∀x. rl_included x x.
1240 /2/
1241qed.
1242
1243include alias "utilities/deqsets_extra.ma".
1244
1245lemma mem_of_fold_join:
1246 ∀F,dom.
1247  ∀x. x ∈ dom →
1248   rl_included (F x)
1249    (fold label (l_property register_lattice) rl_join rl_bottom (λl:label.true)
1250      F dom).
1251 #F #dom elim dom [ #x * ] #hd #tl #IH #x whd in match (? ∈ ?);
1252 @eqb_elim
1253 normalize nodelta #Hx #H change with (rl_join ??) in ⊢ (?(??%));
1254 destruct /3 by rl_included_rl_join_left,rl_included_rl_join_right/
1255qed.
1256
1257lemma set_subset_transitive:
1258 ∀A,DEC,S1,S2,S3.
1259  set_subset A DEC S1 S2 → set_subset … DEC S2 S3 → set_subset … DEC S1 S3.
1260 #A #DEC #S1 #S2 #S3
1261 #H1 lapply (set_member_subset_if … H1) -H1 #H1
1262 #H2 lapply (set_member_subset_if … H2) -H2 #H2
1263 @set_member_subset_onlyif /3 by/
1264qed.
1265
1266lemma rl_included_transitive:
1267 ∀S1,S2,S3. rl_included S1 S2 → rl_included S2 S3 → rl_included S1 S3.
1268 #S1 #S2 #S3 whd in match rl_included; normalize nodelta
1269 #H cases (andb_Prop_true … H) -H #H1 #H2
1270 #H cases (andb_Prop_true … H) -H #H3 #H4
1271 /3 by andb_Prop,set_subset_transitive/
1272qed.
1273
1274lemma rl_included_rl_diff_rl_empty:
1275 ∀S1. rl_included S1 (rl_diff S1 rl_bottom).
1276 #S1 whd in match (rl_included ??);
1277 lapply (set_member_subset_onlyif … (eq_identifier …) (\fst S1) (\fst (rl_diff S1 rl_bottom)))
1278 cases (set_subset ????)
1279 /3 by set_member_diff,set_member_subset_onlyif/
1280qed.
1281
1282lemma included_livebefore_livebeafter_stmt_labels:
1283 ∀fix_comp,globals,fn,l,stmt.
1284  let after ≝ analyse_liveness fix_comp globals fn in
1285   stmt_at … (joint_if_code ERTL … fn) l = Some … stmt →
1286  ∀nxt.
1287   nxt ∈
1288    stmt_labels (mk_stmt_params (g_u_pars ERTL) label (Some label) false)
1289     globals stmt →
1290  l_included register_lattice (livebefore … fn after nxt) (after l).
1291#fix_comp #globals #fn #l #stmt letin after ≝ (analyse_liveness ???) #EQlookup #nxt
1292#Hnxt lapply (fix_correct … after l) #spec @(rl_included_transitive … spec) -spec
1293whd in match (liveafter ????); whd in EQlookup:(??%?); >EQlookup -EQlookup normalize nodelta
1294/2 by mem_of_fold_join/
1295qed.
1296
1297axiom eq_sigma_state_monotonicity:
1298 ∀prog,live,graph,st1,st2,l1,l2,frames.
1299 st_frms ? st1 = return frames →
1300  rl_included (live l2) (live l1) →
1301  sigma_fb_state prog (to_be_cleared_fb live l1) st1 =
1302   sigma_sb_state (get_ertl_call_stack frames) prog
1303    (to_be_cleared_sb live graph l1) st2 →
1304  sigma_fb_state prog (to_be_cleared_fb live l2) st1 =
1305   sigma_sb_state (get_ertl_call_stack frames) prog
1306    (to_be_cleared_sb live graph l2) st2.
1307
1308
1309
1310lemma fetch_ok_sigma_state_ok : ∀fix_comp,colour,prog,init_regs,f_lbls,f_regs.
1311let m ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in
1312let stacksizes ≝ lookup_stack_cost … m in
1313∀st1,st2,f,fn. state_pc_rel fix_comp colour prog init_regs f_lbls f_regs st1 st2 →
1314fetch_internal_function …
1315(joint_globalenv ERTL_semantics prog stacksizes) (pc_block (pc … st1)) 
1316     = return 〈f,fn〉 →
1317let after ≝ (analyse_liveness fix_comp (prog_names … prog) fn) in
1318let before ≝ livebefore … fn after in
1319let coloured_graph ≝ colour … fn after in
1320match st_frms … (st_no_pc … st1) with
1321[ None ⇒ False
1322| Some frames ⇒
1323 (sigma_fb_state prog
1324  (to_be_cleared_fb before (point_of_pc ERTL_semantics (pc … st1)))
1325  (st_no_pc … st1)) =
1326 (sigma_sb_state (get_ertl_call_stack frames) prog
1327   (to_be_cleared_sb … coloured_graph (point_of_pc ERTL_semantics (pc … st1)))
1328  (st_no_pc … st2))
1329].
1330#fix_comp #colour #prog #init_regs #f_lbls #f_regs #st1 #st2 #f #fn
1331#H #EQfn whd in match state_pc_rel in H; normalize nodelta in H;
1332inversion (st_frms … st1) in H; [ #_ *] #frames #EQframes normalize nodelta
1333whd in match sigma_fb_state_pc; whd in match sigma_sb_state_pc;
1334normalize nodelta >EQfn normalize nodelta inversion(fetch_internal_function ????)
1335[2: #e #_ normalize nodelta whd in match dummy_state_pc; whd in match null_pc;
1336    normalize nodelta #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
1337    >fetch_internal_function_no_zero in EQfn; [2: >e1 %] whd in ⊢ (???% → ?);
1338    #ABS destruct(ABS) ]
1339* #f1 #fn1 #EQfn1 normalize nodelta #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ
1340destruct(EQ) <e1 in EQfn1; >EQfn whd in ⊢ (??%?? → ?); #EQ1 destruct(EQ1)
1341whd in match sigma_fb_state; normalize nodelta >e0 >e1 %
1342qed.
1343     
1344lemma fetch_ok_pc_ok : ∀fix_comp,colour,prog,init_regs,f_lbls,f_regs.
1345let m ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in
1346let stacksizes ≝ lookup_stack_cost … m in
1347∀st1,st2,f,fn. state_pc_rel fix_comp colour prog init_regs f_lbls f_regs st1 st2 →
1348fetch_internal_function …
1349(joint_globalenv ERTL_semantics prog stacksizes) (pc_block (pc … st1)) 
1350     = return 〈f,fn〉 → (pc … st1) = (pc … st2).
1351#fix_comp #colour #prog #init_regs #f_lbls #f_regs #st1 #st2 #f #fn
1352#H #EQfn whd in match state_pc_rel in H; normalize nodelta in H;
1353inversion (st_frms … st1) in H; [ #_ *] #frames #EQframes normalize nodelta
1354whd in match sigma_fb_state_pc; whd in match sigma_sb_state_pc;
1355normalize nodelta >EQfn normalize nodelta inversion(fetch_internal_function ????)
1356[2: #e #_ normalize nodelta whd in match dummy_state_pc; whd in match null_pc;
1357    normalize nodelta #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
1358    >fetch_internal_function_no_zero in EQfn; [2: >e1 %] whd in ⊢ (???% → ?);
1359    #ABS destruct(ABS) ]
1360* #f1 #fn1 #EQfn1 normalize nodelta #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ
1361destruct(EQ) <e1 in EQfn1; >EQfn whd in ⊢ (??%?? → ?); #EQ1 destruct(EQ1) %
1362qed.
1363
1364axiom colouring_reg_non_DPL_DPH : ∀fix_comp,colour,prog.
1365let m ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in
1366let stacksizes ≝ lookup_stack_cost … m in
1367∀bl,f,fn,R.∀r : register.
1368fetch_internal_function …
1369(joint_globalenv ERTL_semantics prog stacksizes) bl = return 〈f,fn〉 →
1370let after ≝ (analyse_liveness fix_comp (prog_names … prog) fn) in
1371let before ≝ livebefore … fn after in
1372colouring before (colour … fn after) (inl register Register r) =
1373decision_colour R → R ≠ RegisterDPL ∧ R ≠ RegisterDPH ∧
1374R ≠ RegisterA.
1375
1376axiom insensitive_to_be_cleared_sb_regs :
1377∀prog.∀tb : local_clear_sb_type. ∀st : state LTL_LIN_state.
1378∀bv.∀r : Register.∀cs.∀rgs. tb r →
1379sigma_sb_state cs prog tb (set_regs LTL_semantics rgs st) =
1380sigma_sb_state cs prog tb (set_regs LTL_semantics
1381          (hwreg_store r bv rgs) st).
1382
1383axiom insensitive_sb_to_hwreg_set_other :
1384∀prog.∀tb : local_clear_sb_type. ∀st : state LTL_LIN_state.
1385∀b,cs,rgs.
1386sigma_sb_state cs prog tb
1387 (set_regs LTL_semantics (hwreg_set_other b rgs) st) =
1388sigma_sb_state cs prog tb (set_regs LTL_semantics rgs st).
1389
1390axiom insensitive_to_be_cleared_carry :
1391∀prog.∀tb : local_clear_sb_type. ∀st : state LTL_LIN_state.
1392∀b.∀cs. tb RegisterCarry →
1393sigma_sb_state cs prog tb (set_carry LTL_semantics b st) =
1394sigma_sb_state cs prog tb st.
1395
1396axiom dpl_is_dead : ∀fix_comp.∀prog : ertl_program.
1397 ∀fn : joint_closed_internal_function ERTL (prog_names … prog). ∀l.
1398 let after ≝ analyse_liveness fix_comp (prog_names … prog) fn in
1399  ¬ lives (inr ? ? RegisterDPL) (livebefore  … fn after l).
1400
1401axiom dph_is_dead : ∀fix_comp.∀prog : ertl_program.
1402 ∀fn : joint_closed_internal_function ERTL (prog_names … prog). ∀l.
1403 let after ≝ analyse_liveness fix_comp (prog_names … prog) fn in
1404  ¬ lives (inr ? ? RegisterDPH) (livebefore  … fn after l).
1405
1406lemma m_return_if_commute :  ∀M : Monad.∀A : Type[0]. ∀a1,a2 : A.∀b : bool.
1407if b then m_return M A a1 else m_return M A a2 =
1408m_return M A (if b then a1 else a2).
1409#M #A #a1 #a2 * %
1410qed.
1411
1412lemma set_carry_eta :∀p.∀st : state p.set_carry p (carry … st) st = st.
1413#p * //
1414qed.
1415
1416lemma set_regs_eta :∀p.∀st : state p. set_regs p (regs … st) st = st.
1417#p * //
1418qed.
1419
1420lemma carry_sensitive_read_arg_decision :
1421∀prog.∀tb : local_clear_sb_type. ∀st,st' : state LTL_LIN_state.∀d,cs,bv,localss.
1422read_arg_decision localss st d = return 〈bv,st'〉 →
1423tb RegisterDPL → tb RegisterDPH → 
1424sigma_sb_state cs prog tb (set_carry … (carry … st') st) =
1425sigma_sb_state cs prog tb st'.
1426#prog #tb #st #st' * [#R | #n | #b ] #cs #bv #localss whd in match read_arg_decision;
1427normalize nodelta [1,3: whd in ⊢ (??%% → ?); #EQ destruct(EQ) #_ #_ >set_carry_eta %]
1428>m_return_bind >m_return_bind #H @('bind_inversion H) -H * #bv1 #b1 #_
1429#H @('bind_inversion H) -H * #bv2 #b2 #_ #H @('bind_inversion H) -H #ptr #_ #H
1430@('bind_inversion H) -H #bv3 #_ whd in ⊢ (??%% → ?); #EQ destruct(EQ) #H1 #H2
1431whd in match set_carry; normalize nodelta
1432change with (set_regs ?? (set_carry ? b2 st)) in ⊢ (???(????%));
1433<insensitive_to_be_cleared_sb_regs [2: assumption] <insensitive_to_be_cleared_sb_regs
1434[2: assumption] whd in match set_regs; whd in match set_carry; normalize nodelta %
1435qed.
1436
1437axiom set_carry_sigma_sb_state_commute :
1438∀prog,cs.∀st,st' : state LTL_LIN_state. ∀tb : local_clear_sb_type.
1439sigma_sb_state cs prog tb (set_carry  … (carry … st') st) =
1440set_carry … (carry … (sigma_sb_state cs prog tb st'))
1441 (sigma_sb_state cs prog tb st).
1442
1443lemma cond_commute :∀fix_comp,colour,prog,init_regs,f_lbls,f_regs.
1444let p_out ≝ (\fst (\fst (ertl_to_ltl fix_comp colour prog))) in
1445let m ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in
1446let n ≝ \snd (ertl_to_ltl fix_comp colour prog) in
1447let stacksizes ≝ lookup_stack_cost … m in
1448let init ≝ (λglobals,fn.«translate_data fix_comp colour globals fn,?») in
1449cond_commutation_statement ERTL_semantics LTL_semantics prog stacksizes
1450 init init_regs
1451 f_lbls f_regs (state_rel fix_comp colour prog)
1452 (state_pc_rel fix_comp colour prog init_regs f_lbls f_regs).
1453[2: @hide_prf %]
1454#fix_comp #colour #prog #init_regs #f_lbls #f_regs
1455whd in match cond_commutation_statement; normalize nodelta
1456#st1 #st2 #f #fn #r #ltrue #lfalse #bv #b * #Hbl #EQfetch
1457whd in match acca_retrieve; normalize nodelta change with (ps_reg_retrieve ??) in ⊢ (??%? → ?);
1458#EQbv #EQb #Rst1st2 #t_fn #EQt_fn whd normalize nodelta %{(refl …)} #mid #EQmid
1459cases(ps_reg_retrieve_hw_reg_retrieve_commute fix_comp colour prog init_regs f_lbls
1460f_regs fn (pc … st1) … (colouring … (inl ?? r)) … EQbv)
1461[6: %
1462|2: @(st_no_pc … st2)
1463|5: whd %{f} %{fn} >(proj1 … (fetch_statement_inv … EQfetch)) %{(refl …)}
1464    @(fetch_ok_sigma_state_ok … Rst1st2 …
1465         (proj1 ?? (fetch_statement_inv … EQfetch)))
1466|*:
1467]
1468#bv1 * inversion(colouring … (inl ?? r))
1469[ #n #EQcolouring
1470| #R #EQcolouring
1471  cases(colouring_reg_non_DPL_DPH …
1472                      (proj1 ?? (fetch_statement_inv … EQfetch)) … EQcolouring)
1473  * #RnoDPL #RnoDPH #RnoA
1474]
1475whd in match m_map; normalize nodelta #H @('bind_inversion H) -H *
1476#bv2 #st' #EQbv2 whd in ⊢ (??%% → ?); #EQ1 #EQ2 destruct(EQ1 EQ2)
1477% [2,4: %
1478     [1,3: >map_eval_add_dummy_variance_id in ⊢ (??%?); >move_spec in ⊢ (??%?);
1479       [2: @I | 4:  %{RnoDPL RnoDPH}] normalize nodelta
1480       [ >EQbv2 in ⊢ (??%?); | >EQbv2 in ⊢ (??%?); ] >m_return_bind
1481       whd in match write_decision; normalize nodelta >m_return_bind
1482       >m_return_if_commute in ⊢ (??%?); %
1483     |*: %
1484       [1,3: whd %{f} %{fn} %
1485           [1,3,5,7: @if_elim #_ >(proj1 … (fetch_statement_inv … EQfetch)) %]
1486           normalize nodelta
1487           lapply(fetch_ok_sigma_state_ok … Rst1st2 …
1488                                    (proj1 ?? (fetch_statement_inv … EQfetch)))
1489           normalize nodelta inversion (st_frms … (st_no_pc … st1)) [1,3: #_ * ]
1490           #frames #EQframes normalize nodelta #R_nopc_st1st2
1491           [ inversion(hlives RegisterCarry
1492              (analyse_liveness fix_comp
1493               (prog_names ERTL_semantics prog) fn
1494               (point_of_pc ERTL_semantics (pc … st1))))
1495             [ #carry_live | #carry_dead ]
1496           | @eq_Register_elim [ #EQ destruct(EQ) @⊥ cases RnoA #H @H %] #_
1497           ]
1498           normalize nodelta
1499           [ >insensitive_sb_to_hwreg_set_other
1500             whd in match set_regs in ⊢ (???(????(??%?))); normalize nodelta ]
1501           <insensitive_to_be_cleared_sb_regs
1502           [2,4,6: @dead_registers_in_dead @acc_is_dead ]
1503           [ whd in match set_regs; whd in match set_carry; normalize nodelta
1504             change with (set_carry ? (carry … (st_no_pc … st2)) st') in ⊢ (???(????%));
1505             >set_carry_sigma_sb_state_commute
1506           |*: >set_regs_eta
1507           ]
1508           <(carry_sensitive_read_arg_decision … EQbv2)
1509           [2,3,5,6,8,9: @dead_registers_in_dead [1,3,5: @dph_is_dead |*: @dpl_is_dead]]
1510           [ >set_carry_sigma_sb_state_commute
1511             change with (set_carry ?? (sigma_sb_state ? prog ? (st_no_pc … st2)))
1512                                                                            in ⊢ (???%);
1513             >set_carry_eta
1514           | >insensitive_to_be_cleared_carry
1515             [2: @dead_registers_in_dead cases daemon (*????*) ]
1516           | whd in EQbv2 : (??%%); destruct(EQbv2) >set_carry_eta
1517           ]
1518           @(eq_sigma_state_monotonicity … EQframes … R_nopc_st1st2)
1519           cases b normalize nodelta >point_of_pc_of_point
1520           letin after ≝ (analyse_liveness fix_comp … fn)
1521           letin before ≝ (livebefore … fn after)
1522           lapply (included_livebefore_livebeafter_stmt_labels
1523                      fix_comp … (proj2 ?? (fetch_statement_inv … EQfetch)))
1524           normalize in match (stmt_labels ???);
1525           change with after in match after;
1526           #H [2,4,6: lapply (H lfalse ?) [1,3,5: >memb_hd % ]
1527              |*: lapply (H ltrue ?) [1,3,5: >memb_cons try % >memb_hd %]]
1528           #K change with (bool_to_Prop (rl_included ??)) in K;
1529           @(rl_included_transitive … K) whd in match (livebefore ????);
1530           cases(fetch_statement_inv … EQfetch) #_ normalize nodelta
1531           whd in ⊢ (??%? → ?); #EQstmt >EQstmt normalize nodelta
1532           @rl_included_rl_join_left normalize in match (defined ??);
1533           @rl_included_rl_diff_rl_empty
1534       |*: %{it} %{(refl …)} %{bv1} %
1535           [1,3: [ @if_elim #_
1536                 | @eq_Register_elim [ #EQ destruct(EQ) @⊥ cases RnoA #H @H %] #_
1537                 ]
1538                 normalize nodelta change with (hw_reg_retrieve ??) in ⊢ (??%?);
1539                 whd in match hw_reg_retrieve; normalize nodelta @eq_f
1540                 whd in match set_regs; normalize nodelta
1541                 [ >hwreg_retrieve_insensitive_to_set_other]
1542                 >hwreg_retrieve_hwregstore_hit %
1543           |*: cases(bool_of_beval_sigma_commute fix_comp colour prog init_regs
1544                      f_lbls f_regs … bv1 … EQb) [2,4: %] #b1 * #EQb1 #EQ destruct(EQ)
1545                      assumption
1546           ]
1547       ]
1548    ]     
1549  |*:
1550  ]
1551qed.
1552           
1553lemma seq_commute :∀fix_comp,colour,prog,init_regs,f_lbls,f_regs.
1554let p_out ≝ (\fst (\fst (ertl_to_ltl fix_comp colour prog))) in
1555let m ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in
1556let n ≝ \snd (ertl_to_ltl fix_comp colour prog) in
1557let stacksizes ≝ lookup_stack_cost … m in
1558let init ≝ (λglobals,fn.«translate_data fix_comp colour globals fn,?») in
1559seq_commutation_statement ERTL_semantics LTL_semantics prog stacksizes
1560 init init_regs
1561 f_lbls f_regs (state_rel fix_comp colour prog)
1562 (state_pc_rel fix_comp colour prog init_regs f_lbls f_regs).
1563[2: @hide_prf %]
1564cases daemon (*TODO*)
1565qed.
1566
1567lemma return_commute :∀fix_comp,colour,prog,init_regs,f_lbls,f_regs.
1568let p_out ≝ (\fst (\fst (ertl_to_ltl fix_comp colour prog))) in
1569let m ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in
1570let n ≝ \snd (ertl_to_ltl fix_comp colour prog) in
1571let stacksizes ≝ lookup_stack_cost … m in
1572let init ≝ (λglobals,fn.«translate_data fix_comp colour globals fn,?») in
1573return_commutation_statement ERTL_semantics LTL_semantics prog stacksizes
1574 init init_regs
1575 f_lbls f_regs (state_rel fix_comp colour prog)
1576 (state_pc_rel fix_comp colour prog init_regs f_lbls f_regs).
1577[2: @hide_prf %]
1578cases daemon (*TODO*)
1579qed.
1580
1581lemma pre_main_commute : ∀fix_comp,colour,prog,init_regs,f_lbls,f_regs.
1582let p_out ≝ (\fst (\fst (ertl_to_ltl fix_comp colour prog))) in
1583let m ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in
1584let n ≝ \snd (ertl_to_ltl fix_comp colour prog) in
1585let stacksizes ≝ lookup_stack_cost … m in
1586let init ≝ (λglobals,fn.«translate_data fix_comp colour globals fn,?») in
1587b_graph_transform_program_props ERTL_semantics LTL_semantics stacksizes
1588  init prog init_regs f_lbls f_regs →
1589pre_main_commutation_statement  ERTL_semantics LTL_semantics prog stacksizes
1590 init init_regs
1591 f_lbls f_regs (state_rel fix_comp colour prog)
1592 (state_pc_rel fix_comp colour prog init_regs f_lbls f_regs).
1593[2: @hide_prf %]
1594cases daemon qed.
1595
1596(*
1597#fix_comp #colour #prog #init_regs #f_lbls #f_regs #good whd
1598#st1 #st1' #st2 #EQbl whd in match eval_state; normalize nodelta
1599whd in match fetch_statement; whd in match fetch_internal_function; normalize nodelta
1600whd in match fetch_function; normalize nodelta @eqZb_elim [2: * #H @⊥ @H assumption]
1601#_ normalize nodelta >m_return_bind #H @('bind_inversion H) -H ** #f #fn #stmt
1602#H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H #stmt1
1603#H lapply(opt_eq_from_res ???? H) -H whd in ⊢ (??%% → ?); cases st1 in EQbl; -st1
1604#st1 * #bl1 #pos1 #lp1 #EQbl1 normalize nodelta cases pos1 -pos1 normalize nodelta
1605[ #EQ destruct(EQ)
1606|*: * [2,3,5,6: #x ] whd in ⊢ (??%% → ?); #EQ destruct
1607]
1608whd in ⊢ (??%% → ?); #EQ destruct(EQ) normalize nodelta whd in match eval_statement_no_pc; normalize inversion(point_of_pc ERTL_semantics (pc … st1))
1609*)
1610
1611lemma call_commute : ∀fix_comp,colour,prog,init_regs,f_lbls,f_regs.
1612let p_out ≝ (\fst (\fst (ertl_to_ltl fix_comp colour prog))) in
1613let m ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in
1614let n ≝ \snd (ertl_to_ltl fix_comp colour prog) in
1615let stacksizes ≝ lookup_stack_cost … m in
1616let init ≝ (λglobals,fn.«translate_data fix_comp colour globals fn,?») in
1617call_commutation_statement ERTL_semantics LTL_semantics prog stacksizes
1618 init init_regs
1619 f_lbls f_regs (state_rel fix_comp colour prog)
1620 (state_pc_rel fix_comp colour prog init_regs f_lbls f_regs).
1621[2: @hide_prf %]
1622cases daemon qed.
1623
1624lemma goto_commute : ∀fix_comp,colour,prog,init_regs,f_lbls,f_regs.
1625let p_out ≝ (\fst (\fst (ertl_to_ltl fix_comp colour prog))) in
1626let m ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in
1627let n ≝ \snd (ertl_to_ltl fix_comp colour prog) in
1628let stacksizes ≝ lookup_stack_cost … m in
1629let init ≝ (λglobals,fn.«translate_data fix_comp colour globals fn,?») in
1630goto_commutation_statement ERTL_semantics LTL_semantics prog stacksizes
1631 init init_regs
1632 f_lbls f_regs (state_rel fix_comp colour prog)
1633 (state_pc_rel fix_comp colour prog init_regs f_lbls f_regs).
1634[2: @hide_prf %]
1635cases daemon qed.
1636
1637lemma tailcall_commute : ∀fix_comp,colour,prog,init_regs,f_lbls,f_regs.
1638let p_out ≝ (\fst (\fst (ertl_to_ltl fix_comp colour prog))) in
1639let m ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in
1640let n ≝ \snd (ertl_to_ltl fix_comp colour prog) in
1641let stacksizes ≝ lookup_stack_cost … m in
1642let init ≝ (λglobals,fn.«translate_data fix_comp colour globals fn,?») in
1643tailcall_commutation_statement ERTL_semantics LTL_semantics prog stacksizes
1644 init init_regs
1645 f_lbls f_regs (state_rel fix_comp colour prog)
1646 (state_pc_rel fix_comp colour prog init_regs f_lbls f_regs).
1647[2: @hide_prf %]
1648#fix_comp #colour #prog #init_regs #f_lbls #f_regs whd #st1 #st2
1649#f #fn *
1650qed.
1651
1652             
1653theorem ERTLToLTL_ok :
1654∀fix_comp : fixpoint_computer.
1655∀colour : coloured_graph_computer.
1656∀p_in : ertl_program.
1657let 〈p_out, m, n〉 ≝ ertl_to_ltl fix_comp colour p_in in
1658(* what should we do with n? *)
1659let stacksizes ≝ lookup_stack_cost m in
1660∀init_in.make_initial_state
1661  (mk_prog_params ERTL_semantics p_in stacksizes) = OK … init_in →
1662∃init_out.
1663  make_initial_state
1664   (mk_prog_params LTL_semantics p_out stacksizes) =
1665    OK ? init_out ∧
1666∃[1] R.
1667  status_simulation_with_init
1668    (joint_status ERTL_semantics p_in stacksizes)
1669    (joint_status LTL_semantics p_out stacksizes)
1670    R init_in init_out.
1671#fix_comp #colour #p_in #init_in #EQinit_in
1672letin p_out ≝ (\fst (\fst (ertl_to_ltl fix_comp colour p_in)))
1673letin m ≝ (\snd (\fst (ertl_to_ltl fix_comp colour p_in)))
1674letin n ≝ (\snd (ertl_to_ltl fix_comp colour p_in))
1675letin stacksizes ≝ (lookup_stack_cost m)
1676cases(make_b_graph_transform_program_props ERTL_semantics LTL_semantics stacksizes
1677     (λglobals : list ident.λfn.«translate_data fix_comp colour globals fn,(refl …)») p_in)
1678#init_regs * #f_lbls * #f_regs #good
1679@(joint_correctness ERTL_semantics LTL_semantics p_in stacksizes
1680(λglobals : list ident.λfn.«translate_data fix_comp colour globals fn,(refl …)»)
1681init_regs f_lbls f_regs (state_rel fix_comp colour p_in)
1682(state_pc_rel fix_comp colour p_in init_regs f_lbls f_regs) ? ? init_in EQinit_in)
1683%
1684[ @good
1685| #st1 #st2 #f #fn #Rst1st2 #EQfn whd %{f} %{fn} %{EQfn}
1686  @(fetch_ok_sigma_state_ok fix_comp colour p_in … Rst1st2 EQfn)
1687| #st1 #st2 #f #fn #Rst1st2 #EQfn @(fetch_ok_pc_ok fix_comp colour p_in … Rst1st2 EQfn)
1688| #st1 #st2 #f #fn #Rst1st2 #EQfn lapply Rst1st2 whd in match state_pc_rel;
1689  normalize nodelta cases(st_frms … st1) [*] #frames normalize nodelta
1690  whd in match sigma_fb_state_pc; whd in match sigma_sb_state_pc; normalize nodelta
1691  >EQfn normalize nodelta <(fetch_ok_pc_ok … Rst1st2 EQfn) >EQfn normalize nodelta
1692  #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) assumption
1693| #st1 #st2 #pc #lp1 #lp2 #f #fn #EQfn #Rst1st2 #EQ destruct(EQ) whd
1694  lapply Rst1st2 whd in match state_rel; normalize nodelta * #f1 * #fn1 >EQfn *
1695  whd in ⊢ (??%% → ?); #EQ destruct(EQ) cases(st_frms … st1) [*] #frames
1696  normalize nodelta #EQst whd in match sigma_fb_state_pc;
1697  whd in match sigma_sb_state_pc; normalize nodelta >EQfn
1698  normalize nodelta @eq_f3 [2,3: % | assumption]
1699| @pre_main_commute assumption
1700| #f #fn * #bl #pos #EQbl whd in match fetch_statement;
1701  whd in match fetch_internal_function; whd in match fetch_function;
1702  normalize nodelta @eqZb_elim [2: * #H @⊥ @H assumption]
1703  #_ normalize nodelta >m_return_bind #H @('bind_inversion H) -H #stmt 
1704  #H lapply(opt_eq_from_res ???? H) -H whd in ⊢ (??%% → ?);
1705  whd in match point_of_pc; normalize nodelta cases pos normalize nodelta
1706  [ #EQ destruct(EQ)
1707  |*: * [2,3,5,6: #x ] whd in ⊢ (??%% → ?); #EQ destruct
1708  ]
1709  whd in ⊢ (??%% → ?); #EQ destruct(EQ)
1710| @cond_commute
1711| @seq_commute
1712| #f #fn #bl #EQfn #id #args #dest #lbl whd #bl'
1713  %{(match id with [inl f1 ⇒ inl ?? f1 | inr x ⇒ inr ?? 〈it,it〉])}
1714  %{args} %{it} normalize nodelta cases id [ #f1 % | * #dpl #dph %]
1715| cases daemon (*TODO*)
1716| @return_commute
1717| @call_commute
1718| @goto_commute
1719| @tailcall_commute
1720| cases daemon (*TODO*)
1721| cases daemon (*TODO*)
1722| cases daemon (*TODO*)
1723| cases daemon (*TODO*)
1724]
1725qed.
Note: See TracBrowser for help on using the repository browser.