Changeset 3371


Ignore:
Timestamp:
Jun 26, 2013, 2:22:28 PM (4 years ago)
Author:
piccolo
Message:

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

Added an overflow check in ERTL_semantics

Location:
src
Files:
10 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTL.ma

    r3263 r3371  
    1111  | RegisterDPL ⇒ False
    1212  | RegisterDPH ⇒ False
     13  | RegisterCarry ⇒ False
    1314  | Register04 (* = RegisterST0 *) ⇒ False
    1415  | Register05 (* = RegisterST1 *) ⇒ False
     
    2627  [ Register06 (* = RegisterSPL *) ⇒ False
    2728  | Register07 (* = RegisterSPH *) ⇒ False
     29  | RegisterCarry ⇒ False
    2830  | _ ⇒ True
    2931  ].
  • src/ERTL/ERTLToLTL.ma

    r3263 r3371  
    3838  ∀globals.nat → list (joint_seq LTL globals) ≝
    3939  λglobals,off.
    40   [ A ← byte_of_nat off
     40  let 〈off_h, off_l〉 ≝ (vsplit … 8 8 (bitvector_of_nat 16 off) : Byte × Byte) in
     41  [ A ← off_l
    4142  ; A ← A .Add. RegisterSPL
    4243  ; RegisterDPL ← A
    43   ; A ← zero_byte
     44  ; A ← off_h
    4445  ; A ← A .Addc. RegisterSPH
    4546  ; RegisterDPH ← A
     
    127128  ∀globals.ℕ → list (joint_seq LTL globals) ≝
    128129  λglobals,stack_sz.
    129   [ CLEAR_CARRY …
     130  let 〈off_h, off_l〉 ≝ (vsplit … 8 8 (bitvector_of_nat 16 stack_sz) : Byte × Byte) in
     131  [ CLEAR_CARRY ??
    130132  ; A ← RegisterSPL
    131   ; A ← A .Sub. byte_of_nat stack_sz
     133  ; A ← A .Sub. off_l
    132134  ; RegisterSPL ← A
    133135  ; A ← RegisterSPH
    134   ; A ← A .Sub. zero_byte
     136  ; A ← A .Sub. off_h
    135137  ; RegisterSPH ← A
    136138  ].
     
    139141  ∀globals.ℕ → list (joint_seq LTL globals) ≝
    140142  λglobals,stack_sz.
     143  let 〈off_h, off_l〉 ≝ (vsplit … 8 8 (bitvector_of_nat 16 stack_sz) : Byte × Byte) in
    141144  [ A ← RegisterSPL
    142   ; A ← A .Add. byte_of_nat stack_sz
     145  ; A ← A .Add. off_l
    143146  ; RegisterSPL ← A
    144147  ; A ← RegisterSPH
    145   ; A ← A .Addc. zero_byte
     148  ; A ← A .Addc. off_h
    146149  ; RegisterSPH ← A
    147150  ].
     
    406409 ∀globals.
    407410  joint_closed_internal_function ERTL globals →
    408   bind_new register (b_graph_translate_data ERTL LTL globals)
     411  bound_b_graph_translate_data ERTL LTL globals
    409412λthe_fixpoint,build,globals,int_fun.
    410413νν |RegisterCalleeSaved| as callee_saved_store in
     
    436439    ????).
    437440@hide_prf
    438 [3: #l #c % ]
     441[3: #l #c %
     442|5: #r0 #r1 #r2 #r3 #r4 #r5 #r6 #r7 %
     443]
    439444cases daemon (* TODO *)
    440445qed.
     
    449454   let ltlprog ≝ b_graph_transform_program … (translate_data the_fixpoint build) pr in
    450455   〈ltlprog, stack_cost … ltlprog, 2^16 - globals_stacksize … ltlprog〉.
    451 #r0 #r1 #r2 #r3 #r4 #r5 #r6 #r7 %
    452 qed.
    453456
    454457lemma ERTLToLTL_monotone_stacksizes :
  • src/ERTL/ERTLToLTLProof.ma

    r3261 r3371  
    2828λlocalss,live_fun,colour,R,sp,rgs,st.
    2929gen_preserving … gen_res_preserve …
    30     (λr : (Σr.bool_to_Prop(live_fun (inl ?? r))).λd.colour(inl ?? r) = d) R
     30    (λr,d.bool_to_Prop (live_fun (inl ?? r)) ∧ colour (inl ?? r) = d) R
    3131    (reg_retrieve rgs)
    3232    (λd.match d with
     
    3434        |decision_spill n ⇒ opt_to_res ? [MSG FailedLoad]
    3535                            (beloadv (\snd st)
    36                              (shift_pointer ? sp (bitvector_of_nat 8 (localss + n))))
     36                             (shift_pointer ? sp (bitvector_of_nat 16 (localss + n))))
    3737        ]).
    3838
    39 definition hw_relation : local_live_type → (beval → beval → Prop) →
    40 hw_register_env → hw_register_env → Prop ≝
    41 λlive_fun,R,hw1,hw2.
    42 ∀r : Register.live_fun (inr ?? r) →
    43 R (hwreg_retrieve hw1 r) (hwreg_retrieve hw2 r).
     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].   
    4456
    4557include alias "arithmetics/nat.ma".
    4658include alias "basics/logic.ma".
    4759
    48 (*filters now are axioms but they will be implemented *)
    49 axiom ertl_sp_filter : pointer → Prop.
    50 axiom ltl_sp_filter : pointer → Prop.
    51 
    52 definition mem_relation :
    53 (beval → beval → Prop) → bemem → bemem → Prop ≝
    54 λR,m1,m2.
     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
    5564gen_preserving ?? gen_opt_preserve ????
    56      (λptr1 : Σptr.ertl_sp_filter ptr.
    57      λptr2 : Σptr.ltl_sp_filter ptr.pi1 ?? ptr1 = pi1 ?? ptr2) R
    58      (beloadv m1) (beloadv m2).
    59 
    60 axiom frames_relation :
     65     (λptr1,ptr2.ERTL_validate_pointer … ge f st ptr1 = return it ∧ ptr1 = ptr2) R
     66     (beloadv m2) (beloadv m3).
     67
     68definition callee_saved_remap :
     69(Σb:block.block_region b=Code) → (block → list register) →
     70((Σb:block.block_region b=Code) → option (list register → vertex → decision)) →
     71decision → decision ≝
     72λbl,init_regs,colouring,d.
     73match d with
     74[ decision_spill n ⇒ decision_spill n
     75| decision_colour R ⇒
     76  match position_of ? (eq_Register R) RegisterCalleeSaved with
     77  [ Some n ⇒
     78    match nth_opt ? n (init_regs bl) with
     79    [Some r ⇒
     80        match colouring bl with
     81        [ Some color_fun ⇒ color_fun (init_regs bl) (inl ?? r)
     82        | None ⇒ d
     83        ]
     84    | None ⇒ d
     85    ]
     86  | None ⇒ d
     87  ]
     88].
     89(*
     90definition mem_relation : fixpoint_computer → coloured_graph_computer →
     91ertl_program → (beval → beval → Prop) → ident →  state ERTL_state →  bemem → bemem → Prop ≝
     92λfix_comp,build,prog,R,f,st,m2,m3.
     93let m1 ≝ (\snd (\fst (ertl_to_ltl fix_comp build prog))) in
     94let stacksizes ≝ lookup_stack_cost … m1 in 
     95let ge ≝ joint_globalenv ERTL_semantics prog stacksizes in
     96gen_preserving ?? gen_opt_preserve ????
     97     (λptr1,ptr2.ERTL_validate_pointer … ge f st ptr1 = return it ∧ ptr1 = ptr2) R
     98     (beloadv m2) (beloadv m3).
     99
     100definition callee_saved_remap : fixpoint_computer → coloured_graph_computer →
     101ertl_program → (Σb:block.block_region b=Code) → (block → list register) → decision → decision ≝
     102λfix_comp,build,prog,bl,init_regs,d.
     103match d with
     104[ decision_spill n ⇒ decision_spill n
     105| decision_colour R ⇒
     106  match position_of ? (eq_Register R) RegisterCalleeSaved with
     107  [ Some n ⇒
     108    match nth_opt ? n (init_regs bl) with
     109    [Some r ⇒
     110        let m1 ≝ (\snd (\fst (ertl_to_ltl fix_comp build prog))) in
     111        let stacksizes ≝ lookup_stack_cost … m1 in   
     112        let ge ≝ joint_globalenv ERTL_semantics prog stacksizes in
     113        match fetch_internal_function … ge bl with
     114        [ OK y ⇒
     115             let after ≝ (analyse_liveness fix_comp (prog_names … prog)
     116                          (\snd y) (init_regs bl)) in
     117             (colouring … (build (prog_names … prog) (\snd y) after (init_regs bl))
     118               (inl register Register r))
     119        | Error e ⇒ d
     120        ]
     121    | None ⇒ d
     122    ]
     123  | None ⇒ d
     124  ]
     125]. *)
     126
     127
     128let rec frames_relation_aux (prog : ertl_program) (stacksize : ident → option ℕ)
     129(color_f : (Σb:block.block_region b=Code) →  option (list register → vertex → decision))
     130(live_f : (Σb:block.block_region b=Code) → option (list register → label → vertex → bool))
     131(R : beval → beval → Prop) (frames : list ERTL_frame) (regs : hw_register_env)
     132(m : bemem) (acc : decision → decision) (init_regs : block → list register) on frames : Prop ≝
     133match frames with
     134[ nil ⇒ True
     135| cons hd tl ⇒
     136  let ge ≝ joint_globalenv ERTL_semantics prog stacksize in 
     137  ∃f,fn,color_fun,live_fun.
     138   fetch_internal_function … ge (pc_block (funct_pc hd)) = return 〈f,fn〉 ∧
     139   color_f (pc_block (funct_pc hd)) = Some ? color_fun ∧
     140   live_f (pc_block (funct_pc hd)) = Some ? live_fun ∧
     141   (gen_preserving … gen_res_preserve …
     142      (λr,d.
     143       bool_to_Prop
     144        (live_fun (init_regs (pc_block (funct_pc hd)))
     145          (point_of_pc ERTL_semantics (funct_pc hd)) (inl ?? r))  ∧
     146       d = acc (color_fun (init_regs (pc_block (funct_pc hd)))
     147                  (inl register Register r)))
     148      R (reg_retrieve (psd_reg_env hd))
     149      (λd.match d with
     150          [ decision_spill n ⇒
     151              opt_to_res ? [MSG FailedLoad]
     152               (beloadv m
     153                (shift_pointer ? (funct_sp hd)
     154                 (bitvector_of_nat 16 ((joint_if_local_stacksize … fn)  + n))))
     155          | decision_colour R ⇒ return hwreg_retrieve regs R
     156          ]))
     157    ∧ frames_relation_aux prog stacksize color_f live_f R tl regs m
     158      (λd.acc (callee_saved_remap (pc_block (funct_pc hd)) init_regs color_f d))
     159      init_regs
     160].
     161
     162(*
     163let rec frames_relation_aux (fix_comp : fixpoint_computer)
     164(build : coloured_graph_computer) (prog : ertl_program) (R : beval → beval → Prop)
     165(frames : list ERTL_frame) (regs : hw_register_env) (m : bemem)
     166(acc : decision → decision) (init_regs : block → list register) on frames : Prop ≝
     167match frames with
     168[ nil ⇒ True
     169| cons hd tl ⇒
     170  let m1 ≝ (\snd (\fst (ertl_to_ltl fix_comp build prog))) in
     171  let stacksizes ≝ lookup_stack_cost … m1 in   
     172  let ge ≝ joint_globalenv ERTL_semantics prog stacksizes in 
     173  ∃f,fn.
     174   fetch_internal_function … ge (pc_block (funct_pc hd)) = return 〈f,fn〉 ∧
     175   let after ≝ (analyse_liveness fix_comp (prog_names … prog) fn
     176                (init_regs (pc_block (funct_pc hd)))) in
     177   let before ≝ livebefore … fn (init_regs (pc_block (funct_pc hd))) after in
     178   let colour ≝ (colouring … (build (prog_names … prog) fn after
     179                   (init_regs (pc_block (funct_pc hd))))) in
     180   (gen_preserving … gen_res_preserve …
     181      (λr,d.
     182       bool_to_Prop (in_lattice (inl ?? r)
     183               (before (point_of_pc ERTL_semantics (funct_pc hd)))) ∧
     184       d = acc (colour (inl register Register r)))
     185      R (reg_retrieve (psd_reg_env hd))
     186      (λd.match d with
     187          [ decision_spill n ⇒
     188              opt_to_res ? [MSG FailedLoad]
     189               (beloadv m
     190                (shift_pointer ? (funct_sp hd)
     191                 (bitvector_of_nat 8 ((joint_if_local_stacksize … fn)  + n))))
     192          | decision_colour R ⇒ return hwreg_retrieve regs R
     193          ]))
     194   ∧ frames_relation_aux fix_comp build prog R tl regs m
     195      (λd.acc (callee_saved_remap fix_comp build prog (pc_block (funct_pc hd)) init_regs d))
     196      init_regs
     197].*)
     198
     199definition frames_relation :
     200∀prog : ertl_program.(ident → option ℕ) → (beval → beval → Prop) →
     201((Σb:block.block_region b=Code) →  option(list register → vertex → decision)) →
     202((Σb:block.block_region b=Code) → option(list register → live_type)) → list ERTL_frame →
     203hw_register_env → bemem → (block → list register) → Prop ≝
     204λprog,stacksize,R,color_fun,live_fun,frames,regs,m,init_regs.
     205frames_relation_aux prog stacksize color_fun live_fun R frames regs m (λx.x) init_regs.
     206
     207(*
    61208fixpoint_computer → coloured_graph_computer → 
    62 ertl_program → (beval → beval → Prop) →
    63 framesT ERTL_state → (hw_register_env × bemem) → Prop.
    64 
    65 (*
     209ertl_program → (beval → beval → Prop) → list ERTL_frame →
     210hw_register_env → bemem → (block → list register) → Prop ≝
     211λfix_comp,build,prog,R,frames,regs,m,init_regs.
     212 frames_relation_aux fix_comp build prog R frames regs m (λx.x) init_regs.
     213
     214
    66215definition register_of_bitvector :  BitVector 6 → option Register≝
    67216λvect.
     
    107256*)
    108257
    109 axiom acc_is_dead : ∀fix_comp.∀prog : ertl_program.
    110  ∀fn : joint_closed_internal_function ERTL (prog_names … prog). ∀l.
    111  let after ≝ analyse_liveness fix_comp (prog_names … prog) fn in
    112   ¬ in_lattice (inr ? ? RegisterA) (livebefore  … fn after l).
    113 (*
    114 axiom dead_registers_in_dead :
    115  ∀fix_comp.∀build : coloured_graph_computer.
    116  ∀prog : ertl_program.
    117  ∀fn : joint_closed_internal_function ERTL (prog_names … prog).
    118  ∀l.
    119  let after ≝ analyse_liveness fix_comp (prog_names … prog) fn in
    120  let coloured_graph ≝ build … fn after in
    121  ∀R : Register.
    122   ¬ lives (inr ? ? R) (livebefore  … fn after l) →
    123    to_be_cleared_sb … coloured_graph l R.
    124 *)
    125 
    126 definition dummy_state : state ERTL_semantics ≝
    127 mk_state ERTL_semantics
    128    (None ?) empty_is BBundef 〈empty_map ? ?,mk_hw_register_env … (Stub …) BBundef〉
    129    empty O.
    130 
    131 definition dummy_state_pc : state_pc ERTL_semantics ≝
    132 mk_state_pc ? dummy_state (null_pc one) (null_pc one).
    133 
    134 definition get_ertl_call_stack :
    135 list (register_env beval × (Σb:block.block_region b=Code)) →
    136 list (Σb:block.block_region b=Code) ≝ map … \snd.
    137 
    138 
    139 definition sigma_beval : fixpoint_computer → coloured_graph_computer → 
    140   ertl_program → (block → list register) → lbl_funct_type →
    141   regs_funct_type → beval → beval≝
    142  λfix_comp,build,prog,init_regs,f_lbls,f_regs,bv.
    143   let init ≝ (λglobals,fn.«translate_data fix_comp build globals fn,?») in
    144   let m ≝ (\snd (\fst (ertl_to_ltl fix_comp build prog))) in
    145   let stacksizes ≝ lookup_stack_cost … m in
    146   match bv with
    147   [ BVpc pc p ⇒ match sigma_pc_opt ERTL_semantics LTL_semantics prog stacksizes
    148                        init init_regs f_lbls f_regs pc
    149                 with [Some pc' ⇒ BVpc pc' p | None ⇒ BVundef]
    150   | _ ⇒ bv
    151   ].
    152   @hide_prf % qed.
    153 
    154 definition state_rel : fixpoint_computer → coloured_graph_computer →
    155 ertl_program →  (block → list register) → lbl_funct_type → regs_funct_type →
    156 joint_state_relation ERTL_semantics LTL_semantics ≝
    157 λfix_comp,build,prog,init_regs,f_lbls,f_regs,pc,st1,st2.
    158 let m1 ≝ (\snd (\fst (ertl_to_ltl fix_comp build prog))) in
    159 let stacksizes ≝ lookup_stack_cost … m1 in 
    160 let ge ≝ joint_globalenv ERTL_semantics prog stacksizes in
    161 ∃f,fn.fetch_internal_function … ge (pc_block pc)
    162 = return 〈f,fn〉 ∧
    163 let after ≝ (analyse_liveness fix_comp (prog_names … prog) fn) in
    164 let before ≝ livebefore … fn after in
    165 let coloured_graph ≝ build … fn after in
    166 let R ≝ λbv1,bv2.bv1 = sigma_beval fix_comp build prog init_regs f_lbls f_regs bv2 in
    167 let live_fun ≝ λv.in_lattice v (before (point_of_pc ERTL_semantics pc)) in
    168 match st_frms … st1 with
    169 [ None ⇒ False
    170 | Some frames ⇒
    171    mem_relation R (m … st1) (m … st2) ∧
    172    frames_relation fix_comp build prog R frames 〈regs … st2,m … st2〉 ∧
    173    hw_relation live_fun R (\snd (regs … st1)) (regs … st2) ∧
    174    make_is_relation_from_beval R (istack … st1) (istack … st2) ∧
    175    (live_fun (inr ?? RegisterCarry) → carry … st1 = carry … st2) ∧
    176    ∃ptr.sp … st2 = return ptr ∧
    177     ps_relation (joint_if_local_stacksize … fn) live_fun (colouring … coloured_graph)
    178      R ptr (\fst (regs … st1)) 〈regs … st2,m … st2〉
    179 ].
    180 
    181 definition state_pc_rel :
    182 fixpoint_computer → coloured_graph_computer → 
    183   ertl_program → (block → list register) → lbl_funct_type →
    184   regs_funct_type →  joint_state_pc_relation ERTL_semantics LTL_semantics ≝
    185 λfix_comp,build,prog,init_regs,f_lbls,f_regs,st1,st2.
    186 let m1 ≝ (\snd (\fst (ertl_to_ltl fix_comp build prog))) in
    187 let stacksizes ≝ lookup_stack_cost … m1 in 
    188 let init ≝ (λglobals,fn.«translate_data fix_comp build globals fn,?») in
    189  state_rel fix_comp build prog init_regs f_lbls f_regs (pc … st1) st1 st2 ∧
    190  pc … st1 = pc … st2 ∧
    191  (last_pop … st2 = sigma_stored_pc ERTL_semantics LTL_semantics prog stacksizes
    192                     init init_regs f_lbls f_regs (last_pop … st1)).
    193 @hide_prf % qed.
    194    
    195 lemma hw_reg_retrieve_write_decision_hit : ∀r : Register.∀bv : beval.∀localss.
    196 ∀st : state LTL_LIN_state.
    197 ∀st'. (write_decision localss r bv st) = return st' →
    198 hw_reg_retrieve (regs … st') r = return bv.
    199 #r #bv #localss #st #st' whd in match write_decision; normalize nodelta
    200 whd in match hw_reg_store; normalize nodelta >m_return_bind
    201 whd in ⊢ (??%% → ?); #EQ destruct(EQ)
    202 whd in match hw_reg_retrieve; normalize nodelta @eq_f
    203 whd in match hwreg_retrieve; whd in match hwreg_store; normalize nodelta
    204 @lookup_insert_hit
    205 qed.
    206 
    207 
    208 lemma ps_reg_retrieve_hw_reg_retrieve_commute :
    209 ∀fix_comp,colour,prog,init_regs,f_lbls,f_regs.∀f : ident.
    210 ∀fn : joint_closed_internal_function ERTL (prog_names … prog).
    211 ∀pc.
    212 let m1 ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in
    213 let stacksizes ≝ lookup_stack_cost … m1 in 
    214 let after ≝ (analyse_liveness fix_comp (prog_names … prog) fn) in
    215 fetch_internal_function … (joint_globalenv ERTL_semantics prog stacksizes)
    216 (pc_block pc) = return 〈f,fn〉 → 
    217 gen_preserving2 ?? gen_res_preserve ??????
    218      (state_rel fix_comp colour prog init_regs f_lbls f_regs pc)
    219      (λr :Σr : register.bool_to_Prop(in_lattice (inl ?? r)
    220        (livebefore … fn after (point_of_pc ERTL_semantics pc))).λd : decision.d =
    221       (colouring … (colour (prog_names … prog) fn after)
    222        (inl register Register r)))
    223      (λbv,bv'.bv = sigma_beval fix_comp colour prog init_regs f_lbls f_regs bv') …
    224      (λst1.ps_reg_retrieve (regs … st1))
    225      (λst,d.m_map Res ?? (\fst …)
    226       (read_arg_decision (joint_if_local_stacksize ?? fn) st d)).
    227 #fix_comp #colour #prog #init_regs #f_lbls #f_regs #f #fn #pc #EQfn #st1 #st2
    228 * #r #Hr #d whd in match state_rel; normalize nodelta * #f1 * #fn1
    229 >EQfn * whd in ⊢ (??%% → ?); #EQ destruct(EQ) inversion(st_frms … st1)
    230 [#_ *] #frames #EQframes normalize nodelta ***** #Hmem #Hrames #Hw_relation
    231 #His #Hcarry * #ptr * #EQptr whd in match ps_relation; whd in match gen_preserving;
    232 normalize nodelta #H #EQd #bv #EQbv cases(H «r,Hr» d ? bv EQbv)
    233 [2: <EQd in ⊢ (??%?); %] #bv' cases d
    234 [2: #R normalize nodelta * whd in ⊢ (??%% → ?); #EQ destruct(EQ)
    235     change with (hwreg_retrieve ??) in match (lookup ?????);
    236     #Hrel %{(hwreg_retrieve (regs … st2) R)} %
    237     [ whd in match m_map; whd in match read_arg_decision; normalize nodelta %]
    238     assumption ]
    239 xxxxxxxxxxxx
    240 
    241 [ #R whd in match ps_relation; normalize nodelta whd in match gen_preserving;
    242 normalize nodelta #H #EQR #bv #EQbv cases(H «r,Hr» R
    243      
    244258(*set_theoretical axioms *)
    245259axiom set_member_empty :∀A.∀DEC.∀a.¬set_member A DEC a (set_empty …).   
     
    260274  (∀x. set_member A DEC x S1 → set_member A DEC x S2) →
    261275   set_subset A DEC S1 S2.
     276
     277(*
     278
     279lemma acc_is_dead : ∀fix_comp.∀prog : ertl_program.
     280 ∀fn : joint_closed_internal_function ERTL (prog_names … prog). ∀l.∀rgs.
     281 let after ≝ analyse_liveness fix_comp (prog_names … prog) fn in
     282  in_lattice (inr ? ? RegisterA)
     283  (livebefore (prog_names … prog) fn rgs (after rgs) l) → False.
     284#fix_comp #prog #fn #l #rgs normalize nodelta
     285change with (set_member ????) in ⊢ (?% → ?); whd in match (livebefore ?????);
     286cases(lookup ????) normalize nodelta
     287[ cases(Prop_notb ? (set_member_empty Register eq_Register RegisterA)) #H @H]
     288#stmt whd in match statement_semantics; normalize nodelta @if_elim
     289[ check fix_correct ccccc
     290
     291*)
     292
     293(*
     294axiom dead_registers_in_dead :
     295 ∀fix_comp.∀build : coloured_graph_computer.
     296 ∀prog : ertl_program.
     297 ∀fn : joint_closed_internal_function ERTL (prog_names … prog).
     298 ∀l.
     299 let after ≝ analyse_liveness fix_comp (prog_names … prog) fn in
     300 let coloured_graph ≝ build … fn after in
     301 ∀R : Register.
     302  ¬ lives (inr ? ? R) (livebefore  … fn after l) →
     303   to_be_cleared_sb … coloured_graph l R.
     304*)
     305
     306definition dummy_state : state ERTL_semantics ≝
     307mk_state ERTL_semantics
     308   (None ?) empty_is BBundef 〈empty_map ? ?,mk_hw_register_env … (Stub …) BBundef〉
     309   empty O.
     310
     311definition dummy_state_pc : state_pc ERTL_semantics ≝
     312mk_state_pc ? dummy_state (null_pc one) (null_pc one).
     313
     314definition get_ertl_call_stack :
     315list (register_env beval × (Σb:block.block_region b=Code)) →
     316list (Σb:block.block_region b=Code) ≝ map … \snd.
     317
     318
     319definition sigma_beval :
     320  ertl_program → (ident → option ℕ) → ? → (block → list register) → lbl_funct_type →
     321  regs_funct_type → beval → beval≝
     322 λprog,stacksizes,init,init_regs,f_lbls,f_regs,bv.
     323  match bv with
     324  [ BVpc pc p ⇒ match sigma_pc_opt ERTL_semantics LTL_semantics prog stacksizes
     325                       init init_regs f_lbls f_regs pc
     326                with [Some pc' ⇒ BVpc pc' p | None ⇒ BVundef]
     327  | _ ⇒ bv
     328  ].
     329 
     330definition gen_state_rel :
     331∀prog : ertl_program.(ident → option ℕ) → ? →
     332((Σb:block.block_region b=Code) → option (list register → vertex → decision)) →
     333((Σb:block.block_region b=Code)→ option (list register → live_type)) →
     334? → ? →
     335(block → list register) →
     336lbl_funct_type → regs_funct_type →
     337joint_state_relation ERTL_semantics LTL_semantics ≝
     338λprog,stacksizes,init,color_f,live_f,color_fun,live_fun,init_regs,f_lbls,f_regs,pc,st1,st2.
     339let ge ≝ joint_globalenv ERTL_semantics prog stacksizes in
     340∃f,fn,ssize.
     341fetch_internal_function … ge (pc_block pc) = return 〈f,fn〉 ∧
     342stacksizes f = return ssize ∧
     343let R ≝ λbv1,bv2.bv1 = sigma_beval prog stacksizes init init_regs f_lbls f_regs bv2 in
     344match st_frms … st1 with
     345[ None ⇒ False
     346| Some frames ⇒
     347   mem_relation prog stacksizes R f st1 (m … st1) (m … st2) ∧
     348   frames_relation prog stacksizes R color_f live_f frames (regs … st2) (m … st2) init_regs ∧
     349   hw_relation (joint_if_local_stacksize … fn) (live_fun fn (point_of_pc ERTL_semantics pc))
     350    (color_fun fn) R (\snd (regs … st1)) (regs … st2) (m … st2) ∧
     351   make_is_relation_from_beval R (istack … st1) (istack … st2) ∧
     352   (live_fun fn (point_of_pc ERTL_semantics pc)
     353    (inr ?? RegisterCarry) → carry … st1 = carry … st2) ∧
     354   stack_usage … st1 = stack_usage … st2 ∧
     355   ∃ptr.sp … st2 = return ptr ∧
     356    le ((nat_of_bitvector … (offv (poff … ptr))) + ssize) (2^16 -1) ∧
     357    plus (nat_of_bitvector … (offv (poff … ptr))) (stack_usage … st2) = 2^16 ∧
     358    ps_relation (joint_if_local_stacksize … fn)
     359     (live_fun fn (point_of_pc ERTL_semantics pc))
     360     (color_fun fn)
     361     R ptr (\fst (regs … st1)) 〈regs … st2,m … st2〉
     362].
     363
     364
     365definition RegisterAlwaysDead ≝ [RegisterA; RegisterB; RegisterDPL; RegisterDPH; RegisterST1].
     366
     367definition state_rel :
     368fixpoint_computer → coloured_graph_computer →
     369ertl_program →  (block → list register) → lbl_funct_type → regs_funct_type →
     370joint_state_relation ERTL_semantics LTL_semantics ≝
     371λfix_comp,build,prog,init_regs,f_lbls,f_regs,pc.
     372let after ≝ λfn,callee.analyse_liveness fix_comp (prog_names … prog) fn callee in
     373let before ≝ λfn,callee.livebefore … fn callee (after fn callee) in
     374let coloured_graph ≝ λfn,callee.build … fn (after fn callee) callee in
     375let m1 ≝ (\snd (\fst (ertl_to_ltl fix_comp build prog))) in
     376let stacksizes ≝ lookup_stack_cost … m1 in
     377let init ≝ translate_data fix_comp build in
     378gen_state_rel prog stacksizes init
     379 (λbl.
     380   match fetch_internal_function …
     381          (joint_globalenv ERTL_semantics prog stacksizes) bl with
     382   [ OK x ⇒ Some ? (λcallee.colouring … (coloured_graph (\snd x) callee))
     383   | Error e ⇒ None ?
     384   ])
     385 (λbl.
     386   match fetch_internal_function …
     387          (joint_globalenv ERTL_semantics prog stacksizes) bl with
     388   [ OK x ⇒ Some ? (λcallee,l,v.
     389                     in_lattice v ((before (\snd x) callee) l) ∧
     390                     match v with
     391                     [ inl r ⇒ true
     392                     | inr R ⇒ all … (λR'.¬ eq_Register R' R) RegisterAlwaysDead
     393                     ])
     394   | Error e ⇒ None ?
     395   ]) (λfn.colouring … (coloured_graph fn (init_regs (pc_block pc))))
     396   (λfn,l,v. in_lattice v (before fn (init_regs (pc_block pc)) l) ∧
     397             match v with
     398             [ inl r ⇒ true
     399             | inr R ⇒ all … (λR'.¬ eq_Register R' R) RegisterAlwaysDead
     400             ])
     401    init_regs f_lbls f_regs pc.
     402(*
     403definition state_rel : fixpoint_computer → coloured_graph_computer →
     404ertl_program →  (block → list register) → lbl_funct_type → regs_funct_type →
     405joint_state_relation ERTL_semantics LTL_semantics ≝
     406λfix_comp,build,prog,init_regs,f_lbls,f_regs,pc,st1,st2.
     407let m1 ≝ (\snd (\fst (ertl_to_ltl fix_comp build prog))) in
     408let stacksizes ≝ lookup_stack_cost … m1 in 
     409let ge ≝ joint_globalenv ERTL_semantics prog stacksizes in
     410∃f,fn.fetch_internal_function … ge (pc_block pc)
     411= return 〈f,fn〉 ∧
     412let after ≝ (analyse_liveness fix_comp (prog_names … prog) fn (init_regs (pc_block pc))) in
     413let before ≝ livebefore … fn (init_regs (pc_block pc)) after in
     414let coloured_graph ≝ build … fn after (init_regs (pc_block pc)) in
     415let R ≝ λbv1,bv2.bv1 = sigma_beval fix_comp build prog init_regs f_lbls f_regs bv2 in
     416let live_fun ≝ λv.in_lattice v (before (point_of_pc ERTL_semantics pc)) in
     417match st_frms … st1 with
     418[ None ⇒ False
     419| Some frames ⇒
     420   mem_relation fix_comp build prog R f st1 (m … st1) (m … st2) ∧
     421   frames_relation fix_comp build prog R frames (regs … st2) (m … st2) init_regs ∧
     422   hw_relation live_fun R (\snd (regs … st1)) (regs … st2) ∧
     423   make_is_relation_from_beval R (istack … st1) (istack … st2) ∧
     424   (live_fun (inr ?? RegisterCarry) → carry … st1 = carry … st2) ∧
     425   ∃ptr.sp … st2 = return ptr ∧
     426    ps_relation (joint_if_local_stacksize … fn) live_fun (colouring … coloured_graph)
     427     R ptr (\fst (regs … st1)) 〈regs … st2,m … st2〉
     428].*)
     429
     430
     431definition state_pc_rel :
     432fixpoint_computer → coloured_graph_computer → 
     433  ertl_program → (block → list register) → lbl_funct_type →
     434  regs_funct_type →  joint_state_pc_relation ERTL_semantics LTL_semantics ≝
     435λfix_comp,build,prog,init_regs,f_lbls,f_regs,st1,st2.
     436let m1 ≝ (\snd (\fst (ertl_to_ltl fix_comp build prog))) in
     437let stacksizes ≝ lookup_stack_cost … m1 in 
     438let init ≝ translate_data fix_comp build in
     439 state_rel fix_comp build prog init_regs f_lbls f_regs (pc … st1) st1 st2 ∧
     440 pc … st1 = pc … st2 ∧
     441 (last_pop … st2 = sigma_stored_pc ERTL_semantics LTL_semantics prog stacksizes
     442                    init init_regs f_lbls f_regs (last_pop … st1)).
     443                   
    262444   
     445lemma hw_reg_retrieve_write_decision_hit : ∀r : Register.∀bv : beval.∀localss.
     446∀st : state LTL_LIN_state.
     447∀st'. (write_decision localss r bv st) = return st' →
     448hw_reg_retrieve (regs … st') r = return bv.
     449#r #bv #localss #st #st' whd in match write_decision; normalize nodelta
     450whd in match hw_reg_store; normalize nodelta >m_return_bind
     451whd in ⊢ (??%% → ?); #EQ destruct(EQ)
     452whd in match hw_reg_retrieve; normalize nodelta @eq_f
     453whd in match hwreg_retrieve; whd in match hwreg_store; normalize nodelta
     454@lookup_insert_hit
     455qed.
     456
     457lemma match_reg_elim : ∀ A : Type[0]. ∀ P : A → Prop. ∀ r : region.
     458∀f : (r = XData) → A. ∀g : (r = Code) → A. (∀ prf : r = XData.P (f prf)) →
     459(∀ prf : r = Code.P (g prf)) →
     460P ((match r return λx.(r = x → ?) with
     461    [XData ⇒ f | Code ⇒ g])(refl ? r)).
     462#A #P * #f #g #H1 #H2 normalize nodelta [ @H1 | @H2]
     463qed.
     464
     465definition xpointer_of_pointer : pointer → res xpointer ≝
     466λptr.
     467(match (ptype ptr) return λx.ptype ptr =x → ? with
     468 [ XData ⇒ λprf.OK xpointer «ptr,prf»
     469 | Code ⇒ λ_.Error xpointer [MSG BadPointer]
     470 ]) (refl …).
     471 
     472lemma xpointer_of_pointer_of_xpointer : ∀ptr : xpointer.
     473xpointer_of_pointer ptr = return ptr.
     474#ptr whd in match xpointer_of_pointer; normalize nodelta @match_reg_elim
     475[ cases ptr -ptr #ptr #prf #prf' % ]
     476 cases ptr -ptr #ptr #EQ #EQ1 @⊥ >EQ1 in EQ; #EQ destruct
     477qed.
     478
     479
     480lemma shift_pointer_commute :
     481∀w : Word.∀b : bebit.
     482gen_preserving … gen_res_preserve …
     483(λx,y.x = y)
     484(λx,y.x = y)
     485(λx.! ptr ← pointer_of_address x;
     486    ! ptr ← xpointer_of_pointer ptr;
     487    return shift_pointer ? ptr w)
     488(λx. let 〈w_h, w_l〉 ≝ vsplit … 8 8 w in
     489     ! 〈newaddrl,newcarry〉 ← be_op2 b Add (BVByte w_l) (\fst x);
     490     ! 〈newaddrh,newcarry'〉 ← be_op2 newcarry Addc (BVByte w_h) (\snd x);
     491     pointer_of_address 〈newaddrl,newaddrh〉).
     492cases daemon (*TODO*) qed.
     493(*     
     494#word #b * #bv1 #bv2 #y #EQ destruct(EQ)
     495whd in match pointer_of_address in ⊢ (???????%?); whd in match pointer_of_bevals;
     496normalize nodelta cases bv1 -bv1
     497[|| #pt1 #pt1' #p1 | #b | #p | #ptr1 #p1 | #pc1 #p1 ]
     498try @res_preserve_error_gen normalize nodelta cases bv2 -bv2
     499[|| #pt1 #pt1' #p1 | #b | #p | #ptr2 #p2 | #pc1 #p1 ]
     500try @res_preserve_error_gen normalize nodelta cases p1 -p1 #p1 #prf1
     501cases p2 -p2 #p2 #prf2 @eqb_elim [2: #_ @res_preserve_error_gen]
     502#EQ destruct(EQ) @eqb_elim [2: #_ @res_preserve_error_gen]
     503#EQ destruct(EQ) @eq_block_elim [2: #_ @res_preserve_error_gen]
     504cases ptr1 -ptr1 #bl1 #off1 cases ptr2 -ptr2 #bl2 #off2 #EQ destruct(EQ)
     505whd in match eq_bv_suffix; normalize nodelta @eq_bv_elim [2: #_ @res_preserve_error_gen]
     506cases off1 -off1 #off1 cases off2 -off2 #off2 normalize nodelta #EQvsplit
     507>m_return_bind whd in match xpointer_of_pointer; normalize nodelta @match_reg_elim
     508[2: #_ @res_preserve_error_gen] whd in match ptype; normalize nodelta #EQxptr
     509>m_return_bind whd in match shift_pointer; normalize nodelta whd in match shift_offset;
     510normalize nodelta whd in match be_op2; normalize nodelta whd in match be_add_sub_byte;
     511normalize nodelta whd in match ptype; normalize nodelta >EQxptr normalize nodelta
     512whd in match Bit_of_val; normalize nodelta >m_return_bind normalize nodelta
     513whd in match (op2 ?????); @pair_elim #lft #rgt normalize nodelta
     514@pair_elim #lft' #rgt' #EQrgt' #EQ destruct(EQ) >m_return_bind normalize nodelta
     515whd in match eq_add_or_sub; normalize nodelta @eq_block_elim [2: * #H @⊥ @H %]
     516#_ whd in match eq_bv_suffix; normalize nodelta >EQvsplit @eq_bv_elim
     517[2: * #H @⊥ @H %] #_ normalize nodelta @If_elim [2: @eqb_elim [#_ * #H @⊥ @H %] * #H @⊥ @H %]
     518#INUTILE @pair_elim #lft1 #rgt1 #EQlft1 >m_return_bind whd in match pointer_of_address;
     519whd in match pointer_of_bevals; normalize nodelta cases daemon (*TODO *)
     520qed.*)
     521
     522
     523lemma ps_reg_retrieve_hw_reg_retrieve_commute :
     524∀prog,stacksize,init,color_f,live_f,color_fun,live_fun.
     525∀init_regs : (block → list register).∀f_lbls,f_regs.∀f : ident.
     526∀fn : joint_closed_internal_function ERTL (prog_names … prog).
     527∀pc.
     528fetch_internal_function … (joint_globalenv ERTL_semantics prog stacksize)
     529 (pc_block pc) = return 〈f,fn〉→
     530gen_preserving2 ?? gen_res_preserve ??????
     531     (gen_state_rel prog stacksize init color_f live_f color_fun live_fun init_regs f_lbls f_regs pc)
     532     (λr,d.
     533      bool_to_Prop
     534        (live_fun fn (point_of_pc ERTL_semantics pc)
     535          (inl ?? r)) ∧
     536      d =
     537      (color_fun fn (inl register Register r)))
     538     (λbv,bv'.bv = sigma_beval prog stacksize init init_regs f_lbls f_regs bv') …
     539     (λst1.ps_reg_retrieve (regs … st1))
     540     (λst,d.m_map Res ?? (\fst …)
     541      (read_arg_decision (joint_if_local_stacksize ?? fn) st d)).
     542#prog #stacksize #init #color_f #live_f #color_fun #live_fun #init_regs #f_lbls
     543#f_regs #f #fn #pc #EQfn #st1 #st2 #r #d
     544whd in match gen_state_rel; normalize nodelta * #f1 * #fn1 * #ssize
     545** >EQfn whd in ⊢ (??%% → ?); #EQ1
     546destruct(EQ1) #EQssize inversion(st_frms … st1)
     547[#_ *] #frames #EQframes normalize nodelta ***** #Hmem #Hrames #Hw_relation
     548#His #Hcarry * #ptr ** #EQptr #Hssize whd in match ps_relation; whd in match gen_preserving;
     549normalize nodelta #H * #Hr #EQd #bv #EQbv cases(H r d ? bv EQbv)
     550[2: %{Hr} <EQd in ⊢ (??%?); %] #bv' cases d
     551[2: #R normalize nodelta * whd in ⊢ (??%% → ?); #EQ destruct(EQ)
     552    change with (hwreg_retrieve ??) in match (lookup ?????);
     553    #Hrel %{(hwreg_retrieve (regs … st2) R)} %
     554    [ whd in match m_map; whd in match read_arg_decision; normalize nodelta %]
     555    assumption ]
     556#n normalize nodelta * #H lapply(opt_eq_from_res ???? H) -H #EQbv' #EQ destruct(EQ)
     557%{bv'} % [2: %] whd in match m_map; whd in match read_arg_decision; normalize nodelta
     558@pair_elim #off_l #off_h #EQoff >m_return_bind >m_return_bind
     559lapply EQptr; -EQptr whd in match sp; normalize nodelta
     560change with (hwreg_retrieve_sp ?) in match (load_sp ??);
     561whd in match hwreg_retrieve_sp; normalize nodelta * #H @('bind_inversion H) -H
     562#s_ptr #EQs_ptr change with (xpointer_of_pointer ?) in ⊢ (??%? → ?); #EQptr
     563cases(shift_pointer_commute (bitvector_of_nat 16 (joint_if_local_stacksize … fn1 +n))
     564      (carry … st2) … 
     565      〈hwreg_retrieve (regs LTL_semantics st2) RegisterSPL,
     566       hwreg_retrieve (regs LTL_semantics st2) RegisterSPH〉 …)
     567[5: >EQs_ptr in ⊢ (??(????%?)?); >m_return_bind >EQptr in ⊢ (??(????%?)?);
     568    >m_return_bind %
     569|3: %
     570|*:
     571]
     572#ptr1 >EQoff normalize nodelta * #H @('bind_inversion H) -H #res #EQres #H
     573@('bind_inversion H) -H #res1 #EQres1 #EQptr1 #EQptr1' >EQres >m_return_bind
     574>EQres1 >m_return_bind >EQptr1 >m_return_bind destruct >EQbv' >m_return_bind #_ %
     575qed.
     576
    263577lemma all_used_are_live_before :
    264578∀fix_comp.
    265579∀prog : ertl_program.
    266580∀fn : joint_closed_internal_function ERTL (prog_names … prog).
    267 ∀l,stmt.
     581∀l,stmt.∀callee : list register.
    268582stmt_at … (joint_if_code … fn) l = return stmt →
    269 ∀r : register. set_member ? (eq_identifier …) r (\fst (used ? stmt)) →
    270 let after ≝ (analyse_liveness fix_comp (prog_names … prog) fn) in
     583∀r : register. set_member ? (eq_identifier …) r (\fst (used ? callee stmt)) →
     584let after ≝ (analyse_liveness fix_comp (prog_names … prog) fn callee) in
    271585eliminable ? (after l) stmt = false →
    272 lives (inl ? ? r)  (livebefore  … fn after l).
     586in_lattice (inl ? ? r)  (livebefore  ? fn callee after l).
    273587#fix_comp #prog #fn #l *
    274588[ * [#c|* [#c_id | #c_ptr] #args #dest | #a #lbl | *
    275589[ #str
    276 | * * [#r1 | #R1]  * [1,3: * [1,3: #r |2,4: #R] |2,4: #b]
     590| * * * [#r1 * | #R1 whd in match ertl_writable; normalize nodelta #HR1]  *
     591  [1,3: * * [1,3: #r * |2,4: #R whd in match ertl_readable; normalize nodelta #HR]
     592  |2,4: #b
     593  ]
    277594| #a
    278595| * [ #r | #b]
     
    285602| #a #dpl #dph
    286603| #dpl #dph #a
    287 | * [|| #r ] (*|| * [|| #r] | #r #lbl | #r #lbl ] *)
     604| * #r
    288605]
    289606] #nxt| * [ #lbl | | *] |*]
    290 #EQstmt #r #H #H1 whd in match (lives ??); normalize  nodelta
    291 whd in match (livebefore ????);  whd in EQstmt : (??%?); >EQstmt
    292 normalize nodelta -EQstmt whd in match (statement_semantics ???);
     607#callee #EQstmt #r #H #H1 whd in match (in_lattice ??); normalize  nodelta
     608whd in match (livebefore ?????);  whd in EQstmt : (??%?); >EQstmt
     609normalize nodelta -EQstmt whd in match (statement_semantics ????);
    293610whd in match(\fst ?); try( @(set_member_union2) assumption) >H1
    294611normalize nodelta whd in match(\fst ?); @(set_member_union2) assumption
    295612qed.
     613
    296614
    297615lemma bool_of_beval_sigma_commute :
     
    358676(∀w. f w = g w) → x = y → f x = g y. //
    359677qed.
    360 
    361 lemma add_find_all_miss :  ∀tag,A.∀m : identifier_map tag A.
    362 ∀P : (identifier tag → A → bool).∀i,a.notb (P i a) →
    363 find_all tag A (add tag A m i a) P =
    364 match lookup tag A m i with
    365 [ None ⇒ find_all tag A m P
    366 | Some a ⇒ if P i a then find_all tag A (remove tag A m i) P else find_all tag A m P
    367 ].
    368 cases daemon
    369 qed.
    370678   
    371      
     679(*     
    372680lemma sigma_fb_state_insensitive_to_dead_reg:
    373681 ∀prog,bv. ∀st: state ERTL_semantics. ∀l:label.
     
    412720normalize nodelta whd in match (lives ??); >dead %
    413721qed.
     722*)
    414723
    415724lemma split_orb_false: ∀a,b:bool. orb a b = false → a = false ∧ b = false.
     
    430739 ∀prog,stackcost,fn.
    431740 let p_in ≝ mk_prog_params ERTL_semantics prog stackcost in
    432  ∀st1: joint_abstract_status p_in.
    433741 ∀stms: joint_seq ERTL_semantics (prog_names … prog). ∀next.
    434  let pt ≝ point_of_pc ERTL_semantics (pc ? st1) in
     742 ∀pt.
    435743 stmt_at p_in ? (joint_if_code p_in … fn) pt = return (sequential … stms next) →
    436  ∀liveafter.
    437  eliminable_step (globals … p_in) (liveafter (point_of_pc ERTL_semantics (pc … st1))) stms = true →
    438   livebefore … fn liveafter pt = liveafter pt.
    439  #prog #stackcost #fn #st1 #stms #next #stmt_at #liveafter #Helim
     744 ∀liveafter,callee.
     745 eliminable_step (globals … p_in) (liveafter pt) stms = true →
     746  livebefore … fn callee liveafter pt = liveafter pt.
     747 #prog #stackcost #fn #stms #next #pt #stmt_at #liveafter #callee #Helim
    440748 whd in ⊢ (??%?); whd in stmt_at:(??%?); cases (lookup ????) in stmt_at;
    441749 normalize nodelta try (#abs whd in abs:(??%%); destruct (abs) @I)
     
    518826
    519827lemma included_livebefore_livebeafter_stmt_labels:
    520  ∀fix_comp,globals,fn,l,stmt.
    521   let after ≝ analyse_liveness fix_comp globals fn in
     828 ∀fix_comp,globals,fn,l,stmt,callee.
     829  let after ≝ analyse_liveness fix_comp globals fn callee in
    522830   stmt_at … (joint_if_code ERTL … fn) l = Some … stmt →
    523831  ∀nxt.
     
    525833    stmt_labels (mk_stmt_params (g_u_pars ERTL) label (Some label) false)
    526834     globals stmt →
    527   l_included register_lattice (livebefore … fn after nxt) (after l).
    528 #fix_comp #globals #fn #l #stmt letin after ≝ (analyse_liveness ???) #EQlookup #nxt
     835  l_included register_lattice (livebefore … fn callee after nxt) (after l).
     836#fix_comp #globals #fn #l #stmt #callee letin after ≝ (analyse_liveness ????)
     837#EQlookup #nxt
    529838#Hnxt lapply (fix_correct … after l) #spec @(rl_included_transitive … spec) -spec
    530 whd in match (liveafter ????); whd in EQlookup:(??%?); >EQlookup -EQlookup normalize nodelta
     839whd in match (liveafter ?????); whd in EQlookup:(??%?); >EQlookup -EQlookup normalize nodelta
    531840/2 by mem_of_fold_join/
    532841qed.
    533842
     843(*
    534844axiom eq_sigma_state_monotonicity:
    535845 ∀prog,live,graph,st1,st2,l1,l2,frames.
     
    552862(joint_globalenv ERTL_semantics prog stacksizes) (pc_block (pc … st1)) 
    553863     = return 〈f,fn〉 →
    554 let after ≝ (analyse_liveness fix_comp (prog_names … prog) fn) in
    555 let before ≝ livebefore … fn after in
    556 let coloured_graph ≝ colour … fn after in
     864let callee ≝ init_regs (pc_block (pc … st1)) in
     865let after ≝ (analyse_liveness fix_comp (prog_names … prog) fn callee) in
     866let before ≝ livebefore … fn callee after in
     867let coloured_graph ≝ colour … fn after callee in
    557868match st_frms … (st_no_pc … st1) with
    558869[ None ⇒ False
     
    599910qed.
    600911
    601 axiom colouring_reg_non_DPL_DPH : ∀fix_comp,colour,prog.
    602 let m ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in
    603 let stacksizes ≝ lookup_stack_cost … m in
    604 ∀bl,f,fn,R.∀r : register.
    605 fetch_internal_function …
    606 (joint_globalenv ERTL_semantics prog stacksizes) bl = return 〈f,fn〉 →
    607 let after ≝ (analyse_liveness fix_comp (prog_names … prog) fn) in
    608 let before ≝ livebefore … fn after in
    609 colouring before (colour … fn after) (inl register Register r) =
    610 decision_colour R → R ≠ RegisterDPL ∧ R ≠ RegisterDPH ∧
    611 R ≠ RegisterA.
    612 
     912*)
     913
     914(*
    613915axiom insensitive_to_be_cleared_sb_regs :
    614916∀prog.∀tb : local_clear_sb_type. ∀st : state LTL_LIN_state.
     
    630932sigma_sb_state cs prog tb (set_carry LTL_semantics b st) =
    631933sigma_sb_state cs prog tb st.
    632 
     934*)
     935(*
    633936axiom dpl_is_dead : ∀fix_comp.∀prog : ertl_program.
    634  ∀fn : joint_closed_internal_function ERTL (prog_names … prog). ∀l.
    635  let after ≝ analyse_liveness fix_comp (prog_names … prog) fn in
    636   ¬ lives (inr ? ? RegisterDPL) (livebefore  … fn after l).
     937 ∀fn : joint_closed_internal_function ERTL (prog_names … prog). ∀callee,l.
     938 let after ≝ analyse_liveness fix_comp (prog_names … prog) fn callee in
     939  in_lattice (inr ? ? RegisterDPL) (livebefore  … fn callee after l) → False.
    637940
    638941axiom dph_is_dead : ∀fix_comp.∀prog : ertl_program.
    639  ∀fn : joint_closed_internal_function ERTL (prog_names … prog). ∀l.
    640  let after ≝ analyse_liveness fix_comp (prog_names … prog) fn in
    641   ¬ lives (inr ? ? RegisterDPH) (livebefore  … fn after l).
     942 ∀fn : joint_closed_internal_function ERTL (prog_names … prog). ∀callee,l.
     943 let after ≝ analyse_liveness fix_comp (prog_names … prog) fn callee in
     944  in_lattice (inr ? ? RegisterDPH) (livebefore  … fn callee after l) → False.
     945*)
    642946
    643947lemma m_return_if_commute :  ∀M : Monad.∀A : Type[0]. ∀a1,a2 : A.∀b : bool.
     
    655959qed.
    656960
    657 lemma carry_sensitive_read_arg_decision :
    658 ∀prog.∀tb : local_clear_sb_type. ∀st,st' : state LTL_LIN_state.∀d,cs,bv,localss.
    659 read_arg_decision localss st d = return 〈bv,st'〉 →
    660 tb RegisterDPL → tb RegisterDPH → 
    661 sigma_sb_state cs prog tb (set_carry … (carry … st') st) =
    662 sigma_sb_state cs prog tb st'.
    663 #prog #tb #st #st' * [#R | #n | #b ] #cs #bv #localss whd in match read_arg_decision;
    664 normalize nodelta [1,3: whd in ⊢ (??%% → ?); #EQ destruct(EQ) #_ #_ >set_carry_eta %]
    665 >m_return_bind >m_return_bind #H @('bind_inversion H) -H * #bv1 #b1 #_
    666 #H @('bind_inversion H) -H * #bv2 #b2 #_ #H @('bind_inversion H) -H #ptr #_ #H
    667 @('bind_inversion H) -H #bv3 #_ whd in ⊢ (??%% → ?); #EQ destruct(EQ) #H1 #H2
    668 whd in match set_carry; normalize nodelta
    669 change with (set_regs ?? (set_carry ? b2 st)) in ⊢ (???(????%));
    670 <insensitive_to_be_cleared_sb_regs [2: assumption] <insensitive_to_be_cleared_sb_regs
    671 [2: assumption] whd in match set_regs; whd in match set_carry; normalize nodelta %
    672 qed.
    673 
    674 axiom set_carry_sigma_sb_state_commute :
    675 ∀prog,cs.∀st,st' : state LTL_LIN_state. ∀tb : local_clear_sb_type.
    676 sigma_sb_state cs prog tb (set_carry  … (carry … st') st) =
    677 set_carry … (carry … (sigma_sb_state cs prog tb st'))
    678  (sigma_sb_state cs prog tb st).
     961lemma commute_if : ∀A,B : Type[0].∀b : bool.∀x,y : A.∀f : A → B.
     962f (if b then x else y) = if b then f x else f y.
     963#A #B * // qed.
     964
     965
     966lemma colouring_is_never_forbidden: ∀fix_comp,colour,prog.
     967let m ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in
     968let stacksizes ≝ lookup_stack_cost … m in
     969∀bl,f,fn,callee,R.∀r : register.
     970fetch_internal_function …
     971(joint_globalenv ERTL_semantics prog stacksizes) bl = return 〈f,fn〉 →
     972let after ≝ (analyse_liveness fix_comp (prog_names … prog) fn callee) in
     973let before ≝ livebefore … fn callee after in
     974colouring … (colour … fn after callee)  (inl register Register r) =
     975decision_colour R → All ? (λr1.R ≠ r1) RegistersForbidden.
     976#fix_comp #colour #prog #bl #f #fn #callee #R #r #EQfn
     977normalize nodelta #EQcol %
     978[2: % [2: % [2: % [2: % [2: % [2: % [2: % [2: @I]]]]]]]] % #EQ
     979letin after ≝ (analyse_liveness fix_comp (prog_names … prog) fn callee)
     980lapply(prop_colouring … (colour … fn after callee)
     981        (an_identifier LabelTag one) (inl ?? r) (inr ?? R) ?)
     982[1,3,5,7,9,11,13,15: whd in match interferes; normalize nodelta
     983  @orb_Prop_r whd in match interferes_asym; normalize nodelta
     984  @orb_Prop_l destruct // ]
     985destruct >EQcol >hdw_same_colouring #H lapply(H (refl …)) #EQ1 destruct
     986qed.
     987
     988definition update_fun : ∀A,B : Type[0].(A → A → bool) → (A → B) → A → B → A → B ≝
     989λA,B,eq,f,x,d,a. if eq a x then d else f a.
     990
     991definition eq_vertex : vertex → vertex → bool ≝
     992λv1,v2.match v1 with
     993  [ inl r ⇒ match v2 with [inl r' ⇒ eq_identifier … r r' | _ ⇒ false ]
     994  | inr r ⇒ match v2 with [inr r' ⇒ eq_Register … r r' | _ ⇒ false ]
     995  ].
     996
     997lemma eq_vertex_elim : ∀P : bool → Prop.
     998∀v1,v2.(v1 = v2 → P true) → (v1 ≠ v2 → P false) → P (eq_vertex v1 v2).
     999#P * [#r1 | #R1] * [1,3: #r2 |*: #R2] #H1 #H2 whd in match eq_vertex; normalize nodelta
     1000[2,3: @H2 % #EQ destruct
     1001| @eq_identifier_elim #H3 [ @H1 destruct % | @H2 % #EQ destruct cases H3 #H @H %]
     1002| @eq_Register_elim #H3 [ @H1 destruct % | @H2 % #EQ destruct cases H3 #H @H %]
     1003]
     1004qed.
     1005
     1006include alias "arithmetics/nat.ma".
     1007
     1008lemma beloadv_bestorev_hit : ∀m,m',ptr,bv.
     1009bestorev m ptr bv = return m' →
     1010beloadv m' ptr = return bv.
     1011cases daemon (*TODO*)
     1012qed.
     1013
     1014lemma beloadv_bestorev_miss : ∀m,m',ptr1,ptr2,bv.
     1015ptr1 ≠ ptr2 →
     1016bestorev m ptr1 bv = return m' →
     1017beloadv m' ptr2 = beloadv m ptr2.
     1018cases daemon (*TODO*)
     1019qed.
     1020
     1021lemma shift_pointer_injective :
     1022∀m,ptr,n1,n2.shift_pointer m ptr n1 = shift_pointer m ptr n2 → n1 = n2.
     1023cases daemon qed.
     1024
     1025definition ertl_vertex_retrieve :  ertl_reg_env → vertex → res beval ≝
     1026λregs,v.match v with [inl r ⇒ ps_reg_retrieve regs r | inr r ⇒ hw_reg_retrieve regs r ].
     1027
     1028definition eq_decision : decision → decision → bool ≝
     1029λd1,d2.match d1 with
     1030[ decision_spill n1 ⇒ match d2 with [ decision_spill n2 ⇒ eqb n1 n2 | _ ⇒ false ]
     1031| decision_colour R1 ⇒ match d2 with [ decision_colour R2 ⇒ eq_Register R1 R2 | _ ⇒ false ]
     1032].
     1033
     1034lemma eq_decision_elim : ∀P : bool → Prop.∀d1,d2.(d1 = d2 → P true) → (d1 ≠ d2 → P false) →
     1035P (eq_decision d1 d2).
     1036#P * [#n1 | #R1] * [1,3: #n2 |*: #R2] whd in match eq_decision; normalize nodelta
     1037#H1 #H2
     1038[ @eqb_elim [#EQ destruct @H1 % | * #H @H2 % #EQ destruct @H %]
     1039|2,3: @H2 % #EQ destruct
     1040| @eq_Register_elim [ #EQ destruct @H1 % | * #H @H2 % #EQ destruct @H %]
     1041]
     1042qed.
     1043
     1044
     1045lemma vertex_retrieve_read_arg_decision_commute :
     1046∀prog,stacksize,init,color_f,live_f,color_fun,live_fun.
     1047∀init_regs : (block → list register).∀f_lbls,f_regs.∀f : ident.
     1048∀fn : joint_closed_internal_function ERTL (prog_names … prog).
     1049∀pc.
     1050fetch_internal_function … (joint_globalenv ERTL_semantics prog stacksize)
     1051 (pc_block pc) = return 〈f,fn〉→
     1052gen_preserving2 ?? gen_res_preserve ??????
     1053     (gen_state_rel prog stacksize init color_f live_f color_fun live_fun init_regs f_lbls f_regs pc)
     1054     (λv,d.
     1055      bool_to_Prop
     1056        (live_fun fn (point_of_pc ERTL_semantics pc) v) ∧
     1057      d =
     1058      (color_fun fn v))
     1059     (λbv,bv'.bv = sigma_beval prog stacksize init init_regs f_lbls f_regs bv') …
     1060     (λst1.ertl_vertex_retrieve (regs … st1))
     1061     (λst,d.m_map Res ?? (\fst …)
     1062      (read_arg_decision (joint_if_local_stacksize ?? fn) st d)).
     1063#prog #stacksize #init #color_f #live_f #color_fun #live_fun #init_regs #f_lbls #f_regs
     1064#f #fn #pc #EQfn #st1 #st2 *
     1065[ @ps_reg_retrieve_hw_reg_retrieve_commute assumption] #R #d * #f1 * #fn1 * #ssize
     1066** >EQfn whd in ⊢ (??%% → ?); #EQ1 destruct(EQ1) #_ cases(st_frms ??) [*] #frames
     1067normalize nodelta ***** #_ #H1 #_ #_ #_ #_ * #live_R #EQ destruct(EQ) #bv #EQbv
     1068lapply((proj2 ?? H1 …) R live_R) cases(color_fun ??) normalize nodelta [#n1 | #R1 ]
     1069whd in EQbv : (??%%); destruct(EQbv)
     1070[ inversion (hwreg_retrieve_sp ?) normalize nodelta [2: #e #_ *] #sp #EQsp
     1071  inversion(beloadv ??) normalize nodelta [ #_ *] #bv1 #EQbv1 #Hbv1 %{bv1}
     1072  % [2: assumption] whd in match m_map; whd in match read_arg_decision; normalize nodelta
     1073  @pair_elim #off_h #off_l #EQoff >m_return_bind >m_return_bind @('bind_inversion EQsp)
     1074  #ptr1 #EQptr1 @match_reg_elim
     1075   [2: #_ whd in ⊢ (??%% → ?); #EQ destruct] #prf whd in ⊢ (??%% → ?); #EQ destruct
     1076   cases(shift_pointer_commute
     1077         (bitvector_of_nat 16 (joint_if_local_stacksize … fn1 +n1)) (carry … st2) … 
     1078         〈hwreg_retrieve (regs LTL_semantics st2) RegisterSPL,
     1079          hwreg_retrieve (regs LTL_semantics st2) RegisterSPH〉 …)
     1080   [3: %
     1081   |5: >EQptr1 in ⊢ (??%?); >m_return_bind whd in match xpointer_of_pointer; normalize nodelta
     1082       @match_reg_elim [2: >prf in ⊢ (% → ?); #EQ destruct] #prf1 >m_return_bind %
     1083   |*:
     1084   ]
     1085   #x * >EQoff normalize nodelta #H @('bind_inversion H) -H #val1 #EQval1
     1086   #H @('bind_inversion H) -H #val2 #EQval2 #EQx #EQ destruct(EQ)
     1087   >EQval1 >m_return_bind >EQval2 >m_return_bind >EQx >m_return_bind >EQbv1 >m_return_bind %
     1088| #EQ %{(hwreg_retrieve (regs … st2) R1)} %{(refl …)} assumption
     1089]
     1090qed.
     1091
     1092lemma hwreg_retrieve_sp_insensitive_to_set_other : ∀b,rgs.
     1093hwreg_retrieve_sp (hwreg_set_other b rgs) = hwreg_retrieve_sp rgs.
     1094#b #rgs whd in match hwreg_retrieve_sp; normalize nodelta
     1095>hwreg_retrieve_insensitive_to_set_other >hwreg_retrieve_insensitive_to_set_other %
     1096qed.
     1097
     1098lemma hwreg_retrieve_sp_insensitive_to_regstore : ∀R,regs,bv.
     1099R ≠ RegisterSPL → R ≠ RegisterSPH →
     1100hwreg_retrieve_sp (hwreg_store R bv regs) = hwreg_retrieve_sp regs.
     1101#R #regs #bv #H1 #H2 whd in match hwreg_retrieve_sp; normalize nodelta
     1102>hwreg_retrieve_hwregstore_miss [2: @sym_not_eq assumption]
     1103>hwreg_retrieve_hwregstore_miss [2: @sym_not_eq assumption] %
     1104qed.
     1105
     1106lemma shift_pointer_inj : ∀n,ptr.∀b1,b2 : BitVector n.
     1107nat_of_bitvector … (offv (poff … ptr)) + nat_of_bitvector … b1 ≤ 2^16 - 1 →
     1108nat_of_bitvector … (offv (poff … ptr)) + nat_of_bitvector … b2 ≤ 2^16 - 1 →
     1109shift_pointer n ptr b1 = shift_pointer n ptr b2 →
     1110b1 = b2.
     1111cases daemon (*TODO*)
     1112qed.
     1113
     1114lemma update_color_lemma :
     1115∀fix_comp,colour,prog,init.
     1116∀color_f : ((Σb:block.block_region b=Code) → option (list register → vertex → decision)).
     1117∀live_f : ((Σb:block.block_region b=Code)→ option (list register → live_type)).
     1118∀color_fun : (joint_closed_internal_function ERTL (prog_names … prog) → vertex → decision).
     1119∀live_fun : (joint_closed_internal_function ERTL (prog_names … prog) → label → vertex → bool).
     1120let p_out ≝ (\fst (\fst (ertl_to_ltl fix_comp colour prog))) in
     1121let m1 ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in
     1122let stacksizes ≝ lookup_stack_cost … m1 in
     1123∀init_regs,f_lbls,f_regs,pc,st1,st2.
     1124∀v,new_col.∀f.∀fn : joint_closed_internal_function ? (prog_names … prog).
     1125 fetch_internal_function … (joint_globalenv ERTL_semantics prog stacksizes)
     1126 (pc_block pc) = return 〈f,fn〉 →
     1127 gen_state_rel prog stacksizes init color_f live_f color_fun live_fun init_regs
     1128 f_lbls f_regs pc st1 st2 →   
     1129if live_fun fn (point_of_pc ERTL_semantics pc) v
     1130then ∀bv.
     1131      ertl_vertex_retrieve (regs ? st1) v = return bv →
     1132      match new_col with
     1133      [ decision_colour R ⇒ sigma_beval prog stacksizes init init_regs f_lbls f_regs
     1134                           (hwreg_retrieve (regs … st2) R) = bv
     1135      | decision_spill n ⇒ ∃sp.hwreg_retrieve_sp (regs … st2) = return sp ∧
     1136                         ∃bv'.beloadv (m … st2)
     1137                               (shift_pointer ? sp
     1138                               (bitvector_of_nat 16 (joint_if_local_stacksize … fn + n))) = return bv'
     1139                             ∧ sigma_beval prog stacksizes init init_regs f_lbls f_regs bv' = bv                           
     1140      ]
     1141else True →
     1142gen_state_rel prog stacksizes init color_f live_f
     1143 (λfn.update_fun ?? eq_vertex (color_fun fn) v new_col) live_fun init_regs
     1144 f_lbls f_regs pc st1 st2.
     1145cases daemon qed.
     1146
     1147lemma update_live_fun_lemma :
     1148∀fix_comp,colour,prog,init.
     1149∀color_f : ((Σb:block.block_region b=Code) → option (list register → vertex → decision)).
     1150∀live_f : ((Σb:block.block_region b=Code)→ option (list register → live_type)).
     1151∀color_fun : (joint_closed_internal_function ERTL (prog_names … prog) → vertex → decision).
     1152∀live_fun : (joint_closed_internal_function ERTL (prog_names … prog) → label → vertex → bool).
     1153let p_out ≝ (\fst (\fst (ertl_to_ltl fix_comp colour prog))) in
     1154let m1 ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in
     1155let stacksizes ≝ lookup_stack_cost … m1 in
     1156∀init_regs,f_lbls,f_regs,pc,st1,st2.
     1157∀v,new_live.∀f.∀fn : joint_closed_internal_function ? (prog_names … prog).
     1158 fetch_internal_function … (joint_globalenv ERTL_semantics prog stacksizes)
     1159 (pc_block pc) = return 〈f,fn〉 →
     1160 gen_state_rel prog stacksizes init color_f live_f color_fun live_fun init_regs
     1161 f_lbls f_regs pc st1 st2 →   
     1162if new_live
     1163then if live_fun fn (point_of_pc ERTL_semantics pc) v
     1164     then True
     1165     else ∀bv.ertl_vertex_retrieve (regs … st1) v = return bv →
     1166          match color_fun fn v with
     1167          [ decision_colour R ⇒ sigma_beval prog stacksizes init init_regs f_lbls f_regs
     1168                                (hwreg_retrieve (regs … st2) R) = bv
     1169          | decision_spill n ⇒ ∃sp.hwreg_retrieve_sp (regs … st2) = return sp ∧
     1170                               ∃bv'.beloadv (m … st2)
     1171                               (shift_pointer ? sp
     1172                               (bitvector_of_nat 16 (joint_if_local_stacksize … fn + n))) = return bv'
     1173                               ∧ sigma_beval prog stacksizes init init_regs f_lbls f_regs bv' = bv
     1174          ]
     1175else True →
     1176gen_state_rel prog stacksizes init color_f live_f color_fun
     1177 (λfn.update_fun ?? (eq_identifier …) (live_fun fn) (point_of_pc ERTL_semantics pc)
     1178     (update_fun ?? eq_vertex (live_fun fn (point_of_pc ERTL_semantics pc)) v new_live))
     1179 init_regs f_lbls f_regs pc st1 st2.
     1180cases daemon qed. 
     1181
     1182lemma move_preserve :
     1183∀fix_comp,colour,prog,init.
     1184∀color_f : ((Σb:block.block_region b=Code) → option (list register → vertex → decision)).
     1185∀live_f : ((Σb:block.block_region b=Code)→ option (list register → live_type)).
     1186∀color_fun : (joint_closed_internal_function ERTL (prog_names … prog) → vertex → decision).
     1187∀live_fun : (joint_closed_internal_function ERTL (prog_names … prog) → label → vertex → bool).
     1188let p_out ≝ (\fst (\fst (ertl_to_ltl fix_comp colour prog))) in
     1189let m1 ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in
     1190let stacksizes ≝ lookup_stack_cost … m1 in
     1191 ∀init_regs : block → list register.∀f_lbls,f_regs. ∀pc,carry_lives_after.
     1192 ∀src,dest : decision.
     1193 ∀f.∀fn : joint_closed_internal_function ? (prog_names … prog).
     1194 fetch_internal_function … (joint_globalenv ERTL_semantics prog stacksizes)
     1195 (pc_block pc) = return 〈f,fn〉 → 
     1196∀v1,v2. color_fun fn v1 = src →
     1197color_fun fn v2 = dest →
     1198v2 ≠ (inr ?? RegisterCarry) →
     1199live_fun fn (point_of_pc ERTL_semantics pc) v1 →
     1200invariant_for_move src →
     1201(∀v. live_fun fn (point_of_pc ERTL_semantics pc) v →
     1202     color_fun fn v ≠ decision_colour RegisterDPL ∧
     1203     color_fun fn v ≠ decision_colour RegisterDPH ∧
     1204     color_fun fn v ≠ decision_colour RegisterST1) →
     1205live_fun fn (point_of_pc ERTL_semantics pc)
     1206 (inr ?? RegisterCarry) = carry_lives_after →
     1207gen_preserving ?? gen_res_preserve ????
     1208(λst1,st2.
     1209 gen_state_rel prog stacksizes init color_f live_f color_fun live_fun init_regs
     1210  f_lbls f_regs pc st1 st2 ∧
     1211 ∃bv.ertl_vertex_retrieve (regs … st1) v1 = return bv ∧
     1212 (∀v.live_fun fn (point_of_pc ERTL_semantics pc) v → v ≠ v1 → v ≠ v2 →
     1213     color_fun fn v = dest →
     1214     ertl_vertex_retrieve (regs … st1) v = return bv) ∧
     1215 (∀ptr.
     1216  sp … st2 = return ptr → 
     1217  match dest with
     1218  [ decision_spill n ⇒ 
     1219        ∀bv.bestorev (m … st2)
     1220         (shift_pointer ? ptr (bitvector_of_nat 16 ((joint_if_local_stacksize … fn) + n)))
     1221         bv ≠ None ?
     1222 | _ ⇒ True
     1223 ]))
     1224(gen_state_rel prog stacksizes init color_f live_f
     1225 (λfn.update_fun ?? eq_vertex (color_fun fn) v1 dest)
     1226 (λfn.update_fun ?? (eq_identifier …) (live_fun fn) (point_of_pc ERTL_semantics pc)
     1227   (update_fun ?? eq_vertex (live_fun fn (point_of_pc ERTL_semantics pc)) v2
     1228    (eq_decision src dest)))
     1229 init_regs f_lbls f_regs pc)
     1230(m_return ??)
     1231(repeat_eval_seq_no_pc LTL_semantics (mk_prog_params LTL_semantics p_out stacksizes) f
     1232   (move (prog_names … prog) (joint_if_local_stacksize … fn) carry_lives_after dest src)).
     1233#fix_comp #colour #prog #init #color_f #live_f #color_fun #live_fun #init_regs #f_lbls
     1234#f_regs #pc #carry_live #src #dst #f #fn #EQfn #v1 #v2 #EQsrc
     1235#EQdst * #v2_noCarry #v1_live #Hsrc #dst_spec #EQcarry_live #st1 #st2 * #Rst1st2 * #bv ** #EQbv
     1236#Hv1v2 #Hdst >move_spec [2: assumption]
     1237cases(vertex_retrieve_read_arg_decision_commute … init … EQfn … Rst1st2 … EQbv)
     1238[3: %{v1_live} % |2: ] #bv1 * whd in match m_map; normalize nodelta
     1239#H @('bind_inversion H) -H * #bv2 #st2' #EQread_arg whd in ⊢ (??%% → ?); #EQ1 #EQ2
     1240destruct(EQ1 EQ2) cases src in EQsrc Hsrc; normalize nodelta -src
     1241[ #n1 | #R1 ] #EQcol_src * [2: #R1_noDPL #R1_noDPH ] cases dst in EQdst Hdst Hv1v2 dst_spec;
     1242[1,3: #n2 |*: #R2 ] #EQcol_dst normalize nodelta [1,2: #Hn2 |*: #_] #Hv1v2 #dst_spec
     1243>EQcol_src in EQread_arg; #EQread_arg >EQread_arg whd in EQread_arg : (??%%);
     1244[2,4: lapply EQread_arg -EQread_arg @pair_elim #off_h_src #off_l_src #EQoff_src
     1245      >m_return_bind >m_return_bind #H @('bind_inversion H) -H #val1_src #EQval1_src
     1246      #H @('bind_inversion H) -H #val2_src #EQval2_src #H @('bind_inversion H) -H
     1247      #ptr_shift_src #EQptr_shift_src #H @('bind_inversion H) -H #bv_src #H
     1248      lapply(opt_eq_from_res ???? H) -H #EQbv_src whd in ⊢ (??%% → ?); #EQread_arg ]
     1249destruct(EQread_arg) >m_return_bind #st1' whd in ⊢ (??%% → ?); #EQ destruct(EQ)
     1250cases Rst1st2 #f1 * #fn1 * #ssize ** >EQfn whd in ⊢ (??%% → ?); #EQ1 destruct(EQ1)
     1251#EQssize inversion(st_frms ??) normalize nodelta [1,3,5,7: #_ *] #frames #EQframes ******
     1252#Hmem #Hframes #Hhw_reg #His #Hcarry #Hsu * #sp ***
     1253change with (hwreg_retrieve_sp ?) in ⊢ (??%? → ?); #EQsp #Hssize #Hstack_usage #Hps_reg
     1254[ @eqb_elim normalize nodelta [ #EQ destruct(EQ) %{st2} %{(refl …)} | * #src_dest_spec ]
     1255| @eq_Register_elim normalize nodelta [ #EQ destruct(EQ) | * #R2_noA ]
     1256| @eq_Register_elim normalize nodelta [ #EQ destruct(EQ) | * #R1_noA ]
     1257| @eq_Register_elim normalize nodelta
     1258   [ #EQ destruct(EQ) %{st2'} %{(refl …)}
     1259   | * #src_dest_spec @eq_Register_elim normalize nodelta [#EQ destruct(EQ) | * #R2_noA >m_return_bind ]
     1260   ]
     1261]
     1262[1,7: @(update_color_lemma … EQfn)
     1263  [1,3: @(update_live_fun_lemma … EQfn) [1,3: assumption] @eq_decision_elim
     1264    [2,4: * #H @⊥ @H %] #_ normalize nodelta inversion(live_fun ??)
     1265    [1,3: #_ @I] normalize nodelta >EQcol_dst normalize nodelta cases v2 in EQcol_dst; [1,3: #r |*: #R ] #EQcol_dst #v2_dead
     1266    normalize nodelta #bv1 whd in match ertl_vertex_retrieve; normalize nodelta #EQbv1
     1267    >EQcol_dst normalize nodelta
     1268    [1,3: %{sp} %{EQsp} cases v1 in EQcol_src v1_live EQbv; [1,3: #r1 |*: #R1] #EQcol_src
     1269          #v1_live whd in match ertl_vertex_retrieve; normalize nodelta
     1270          [1,2: #EQbv cases(Hps_reg r1 (decision_spill n2) … EQbv) [2,4: % assumption] #bv2
     1271          normalize nodelta
     1272   
     1273
     1274 
     1275 
     1276 
     1277   @(update_color_lemma … EQfn)
     1278    cases daemon (*TODO: it follows by extensionality:
     1279                          maybe to be merged with other proof obbligations *)
     1280  ]
     1281  * #src_dest_spec
     1282 
     1283
     1284[2,4:
     1285
     1286
     1287[1,3: whd in EQread_arg : (??%%); destruct(EQread_arg) @eq_Register_elim normalize nodelta
     1288 [ #EQ destruct(EQ) @('bind_inversion EQsp) #ptr #EQptr @match_reg_elim
     1289   [2: #_ whd in ⊢ (??%% → ?); #EQ destruct] #prf whd in ⊢ (??%% → ?);
     1290   #EQ destruct(EQ)
     1291   cases(shift_pointer_commute
     1292         (bitvector_of_nat 16 (joint_if_local_stacksize … fn1 +n2)) (carry … st2') … 
     1293         〈hwreg_retrieve (regs LTL_semantics st2') RegisterSPL,
     1294          hwreg_retrieve (regs LTL_semantics st2') RegisterSPH〉 …)
     1295   [3: %
     1296   |5: >EQptr in ⊢ (??%?); >m_return_bind whd in match xpointer_of_pointer; normalize nodelta
     1297       @match_reg_elim [2: >prf in ⊢ (% → ?); #EQ destruct] #prf1 >m_return_bind %
     1298   |*:
     1299   ]
     1300   #x * @pair_elim #offh #offl #EQoff #H @('bind_inversion H) -H #val1 #EQval1
     1301   #H @('bind_inversion H) -H #val2 #EQval2 #EQx #EQ destruct(EQ) %
     1302   [2: %
     1303       [ whd in match write_decision; whd in match set_regs; whd in match set_carry;
     1304         normalize nodelta > EQoff in ⊢ (??%?); normalize nodelta
     1305         >m_return_bind >m_return_bind >hwreg_retrieve_hwregstore_miss
     1306         [ >EQval1 in ⊢ (??%?); >m_return_bind >hwreg_retrieve_hwregstore_miss
     1307           [ >EQval2 in ⊢ (??%?); >m_return_bind >EQx in ⊢ (??%?); >m_return_bind
     1308             >(opt_to_opt_safe … (Hn2 … EQsp …)) >m_return_bind <commute_if
     1309             whd in match set_m; normalize nodelta %
     1310           ]
     1311         ]
     1312         normalize % #EQ destruct
     1313       | %{f1} %{fn1} %{ssize} % [ %{EQfn EQssize} ]
     1314         >EQframes normalize nodelta %
     1315         [ % [2: cases carry_live normalize nodelta assumption ]
     1316           % [2: whd in match update_fun; normalize nodelta @eq_identifier_elim
     1317                 [2: * #H @⊥ @H %] #_ normalize nodelta
     1318                 @eq_vertex_elim [ #EQ destruct @⊥ @v2_noCarry %] #_
     1319                 @eq_decision_elim [ #EQ destruct] #_ normalize nodelta
     1320                 destruct #H >H normalize nodelta @Hcarry assumption ]
     1321           % [2: @if_elim #_ assumption ] %
     1322           [2: whd in match update_fun; normalize nodelta @eq_identifier_elim
     1323               [2: * #H @⊥ @H %] #_ normalize nodelta %
     1324               [ cases carry_live normalize nodelta
     1325                 [ >hwreg_retrieve_sp_insensitive_to_set_other]
     1326                 >hwreg_retrieve_sp_insensitive_to_regstore
     1327                 [1,4: >hwreg_retrieve_sp_insensitive_to_regstore
     1328                   [1,4: >hwreg_retrieve_sp_insensitive_to_regstore
     1329                      [1,4:  @(proj1 … Hhw_reg) ] ] ]
     1330                 % normalize #EQ destruct
     1331               | #R' @eq_vertex_elim normalize nodelta [ #_ @eq_decision_elim [#EQ destruct] #_ *]
     1332                 #v2_noR' #live_R' @eq_vertex_elim
     1333                 [ #EQ destruct(EQ) normalize nodelta cases carry_live in EQcarry_live;
     1334                   #EQcarry_live normalize nodelta
     1335                   [ >hwreg_retrieve_sp_insensitive_to_set_other]
     1336                   >hwreg_retrieve_sp_insensitive_to_regstore
     1337                   [1,4: >hwreg_retrieve_sp_insensitive_to_regstore
     1338                     [1,4: >hwreg_retrieve_sp_insensitive_to_regstore ]]
     1339                   [1,4: |*: % normalize #EQ destruct]
     1340                   try >EQsp in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?]); normalize nodelta
     1341                   @opt_safe_elim #m' #EQm' >(beloadv_bestorev_hit … EQm')
     1342                   normalize nodelta whd in EQbv : (??%%);
     1343                   cut(∀A,a1,a2. OK A a1 = OK A a2 → a1 = a2)
     1344                   [1,3: #H1 #H2 #H3 #H4 destruct %] #AUX
     1345                   @(AUX … EQbv)
     1346                 | #v1_noR' normalize nodelta
     1347                   cut(bool_to_Prop(eq_decision (decision_spill n2) (color_fun fn1 (inr ?? R'))) ∨
     1348                       bool_to_Prop(¬ eq_decision (decision_spill n2) (color_fun fn1 (inr ?? R'))))
     1349                   [ @eq_decision_elim #_ [%%|%2%]] *
     1350                   [ @eq_decision_elim [2: #_ *] #EQ lapply(sym_eq ??? EQ) -EQ #EQcolR'
     1351                     #_ >EQcolR' normalize nodelta cases carry_live
     1352                     [ >hwreg_retrieve_sp_insensitive_to_set_other]
     1353                     >hwreg_retrieve_sp_insensitive_to_regstore
     1354                     [1,4: >hwreg_retrieve_sp_insensitive_to_regstore
     1355                     [1,4: >hwreg_retrieve_sp_insensitive_to_regstore ]]
     1356                     [1,4: |*: % normalize #EQ destruct]
     1357                     try >EQsp in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]); normalize nodelta
     1358                     @opt_safe_elim #m' #EQm' >(beloadv_bestorev_hit … EQm') normalize nodelta
     1359                     lapply(Hv1v2 (inr ?? R') live_R' v1_noR' v2_noR' EQcolR')
     1360                     whd in match ertl_vertex_retrieve;  normalize nodelta
     1361                     whd in ⊢ (??%% → ?); cut(∀A,a1,a2. OK A a1 = OK A a2 → a1 = a2)
     1362                     [1,3: #H1 #H2 #H3 #H4 destruct %] #AUX #EQ
     1363                     >(AUX ??? EQ) %
     1364                   | @eq_decision_elim [ #_ *] #Hnodet_R' #_ inversion(color_fun ??)
     1365                     [ #n3 #EQn3 normalize nodelta cases carry_live
     1366                       [ >hwreg_retrieve_sp_insensitive_to_set_other]
     1367                       >hwreg_retrieve_sp_insensitive_to_regstore
     1368                       [1,4: >hwreg_retrieve_sp_insensitive_to_regstore
     1369                       [1,4: >hwreg_retrieve_sp_insensitive_to_regstore ]]
     1370                       [1,4: |*: % normalize #EQ destruct]
     1371                       try >EQsp in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]); normalize nodelta
     1372                       @opt_safe_elim #m' #EQm' >(beloadv_bestorev_miss … EQm')
     1373                       [1,3: lapply(proj2 ?? Hhw_reg R' live_R') >EQn3 normalize nodelta
     1374                             >EQsp normalize nodelta #H @H ]
     1375                       % #ABS >EQn3 in Hnodet_R'; * #H @H @eq_f -H
     1376                       @(injective_plus_r … (joint_if_local_stacksize … fn1))
     1377                       cut(? : Prop)
     1378                       [3,6: cut(? : Prop)
     1379                         [3,6: #H1 #H2 @(eq_bitvector_of_nat_to_eq 16)
     1380                               [1,4: @H1 |2,5: @H2 ]
     1381                               @(shift_pointer_inj … ABS) >nat_of_bitvector_bitvector_of_nat_inverse
     1382                               try assumption @(transitive_le … Hssize)
     1383                               @monotonic_le_plus_r cases daemon (*TODO*)
     1384                         |1,4:
     1385                         |*: cases daemon (*TODO*)
     1386                         ]
     1387                       |1,4:
     1388                       |*: cases daemon (*TODO*)
     1389                       ]     
     1390                     | #R'' #EQR'' normalize nodelta cases carry_live normalize nodelta
     1391                       [ >hwreg_retrieve_insensitive_to_set_other ]
     1392                       >hwreg_retrieve_hwregstore_miss
     1393                       [1,3: >hwreg_retrieve_hwregstore_miss 
     1394                             [1,3: >hwreg_retrieve_hwregstore_miss
     1395                                 [1,3: lapply(proj2 ?? Hhw_reg R' live_R') > EQR''
     1396                                       normalize nodelta #H @H ] ] ]
     1397                        cases(dst_spec … live_R') * >EQR'' * #H1 * #H2 * #H3 % #EQ destruct(EQ)
     1398                        try(@H1 %) try(@H2 %) try(@H3 %)
     1399                       
     1400                       
     1401                         [@H3 try @H1 try @H2 try assumption
     1402                       cases daemon (*hypothesis on colouring function to be added TODO *)
     1403                     ] 
     1404                       
     1405                                   
     1406                              lapply EQssize whd in ⊢ (??%% → ?);
     1407                             whd in match ertl_to_ltl; normalize nodelta whd in match (stack_cost ??);
     1408                             whd in ⊢ (??%% → ?);
     1409                 xxxxxxxx
     1410                   
     1411                   
     1412                    <EQbv destruct(EQbv)
     1413                   
     1414                   
     1415                    whd in match hwreg_retrieve_sp;
     1416                   normalize nodelta                                                                 
     1417          @eq_vertex_elim
     1418     
     1419       
     1420         
     1421               
     1422                | normalize nodelta
     1423       
     1424       
     1425       
     1426       %{live_fun1} %{color_fun1} %
     1427         [%
     1428           [ %{EQfn}
     1429
     1430
     1431 
     1432cases src in EQsrc Hsrc; -src normalize nodelta
     1433[ #n1 | #R1 ] #EQcol_src * [2: #R1_noDPL #R1_noDPH] cases dst in EQdst Hdst;
     1434[1,3: #n2 |*: #R2 ] #EQcol_dst normalize nodelta [1,2: #Hn2 |*: #_]
     1435#st1' whd in ⊢ (??%% → ?); #EQ destruct(EQ)
     1436cases daemon (*TODO*)
     1437qed.
     1438
     1439
     1440
     1441
     1442
     1443
     1444
     1445
     1446
     1447lemma state_rel_insensitive_to_forbidden_Reg :
     1448 ∀fix_comp,colour,prog,init_regs,f_lbls,f_regs,pc.
     1449 let m ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in
     1450 let stacksizes ≝ lookup_stack_cost … m in
     1451 ∀f.∀fn : joint_closed_internal_function ? (prog_names … prog).
     1452 fetch_internal_function … (joint_globalenv ERTL_semantics prog stacksizes)
     1453 (pc_block pc) = return 〈f,fn〉 →
     1454 ∀st1 : state ERTL_state.∀st2.
     1455 ∀r,bv. Exists … (λr1.r = r1) RegisterAlwaysDead →
     1456 state_rel fix_comp colour prog init_regs f_lbls f_regs pc st1 st2 →
     1457 state_rel fix_comp colour prog init_regs f_lbls f_regs pc st1
     1458  (set_regs LTL_LIN_state (hwreg_store r bv (regs … st2)) st2).
     1459#fix_comp #colour #prog #init_regs #f_lbls #f_regs #pc #f #fn #EQfn #st1 #st2 #r
     1460#bv * [2: * [2: * [2: * [2: * [2: * ]]]] ] #EQ destruct(EQ) whd in match state_rel;
     1461whd in match gen_state_rel; normalize nodelta * #f1 * #fn1 * >EQfn whd in ⊢ (??%% → ?);
     1462#EQ destruct(EQ) cases(st_frms ??) [1,3,5,7,9: *] #frames normalize nodelta ***** 
     1463#Hmem #Hframes #Hhw_rel #His #Hcarry * #sp * #EQsp #Hpsd_reg %{f1} %{fn1} %{(refl …)} %
     1464[1,3,5,7,9: % [2,4,6,8,10: assumption ] % [2,4,6,8,10: assumption] % [1,3,5,7,9: % [1,3,5,7,9: assumption ]]]
     1465[1,2,3,4,5: whd in match set_regs; normalize nodelta lapply Hframes whd in match frames_relation;
     1466  normalize nodelta letin ID ≝ (λx : decision.x)
     1467  [ cut((∀r.r ≠ RegisterST1 → ID (decision_colour r) ≠ RegisterST1) ∧ ∀n.ID (decision_spill n) = decision_spill n)
     1468  | cut((∀r.r ≠ RegisterDPH → ID (decision_colour r) ≠ RegisterDPH) ∧ ∀n.ID (decision_spill n) = decision_spill n)
     1469  | cut((∀r.r ≠ RegisterDPL → ID (decision_colour r) ≠ RegisterDPL) ∧ ∀n.ID (decision_spill n) = decision_spill n)
     1470  | cut((∀r.r ≠ RegisterB → ID (decision_colour r) ≠ RegisterB) ∧ ∀n.ID (decision_spill n) = decision_spill n) 
     1471  | cut((∀r.r ≠ RegisterA → ID (decision_colour r) ≠ RegisterA) ∧ ∀n.ID (decision_spill n) = decision_spill n)
     1472  ]
     1473  [1,3,5,7,9: % try (#n %) #r normalize * #H %  #EQ destruct @H % ]
     1474  generalize in match ID; elim frames [1,3,5,7,9: #f #_ #_ @I]
     1475  #hd #tl #IH #acc #acc_spec * #f2 * #fn2 ** #EQfn2 #Hframe #Htl %{f2} %{fn2} %
     1476  [2,4,6,8,10: @IH try assumption % 
     1477    [1,3,5,7,9: #r #Hr whd in match callee_saved_remap; normalize nodelta
     1478      cases(position_of ???) normalize nodelta [1,3,5,7,9: @((proj1 ?? acc_spec) r Hr) ]
     1479      #x cases(nth_opt ???) normalize nodelta [1,3,5,7,9: @((proj1 ?? acc_spec) r Hr) ]
     1480      #r1 >EQfn2 normalize nodelta inversion(colouring  ???)
     1481      [1,3,5,7,9: #m |*: #R1 ] #EQcolouring
     1482      [1,2,3,4,5: >(proj2 ?? acc_spec) % #EQ destruct
     1483      |*: @((proj1 ?? acc_spec) R1 ?)
     1484         cases(colouring_is_never_forbidden … EQfn2 … EQcolouring) #H1
     1485         [5: #_ assumption] * #H [4: #_ assumption] * #H2 [3: #_ assumption] *
     1486         #H3 [2: #_ assumption ] * #_ * #_ * #_ * #H4 #_ @H4
     1487      ]
     1488    |*: #z whd in match callee_saved_remap; normalize nodelta @(proj2 … acc_spec)
     1489    ]
     1490  |*: %{EQfn2} #r #d * normalize nodelta @andb_elim @if_elim #r_live [2,4,6,8,10: *]
     1491     #_ #EQd #bv #EQbv cases(Hframe … d … EQbv)
     1492     [2,4,6,8,10: % [2,4,6,8,10: assumption] @andb_Prop try @I assumption]
     1493     #bv1 * #Hbv1 #EQ destruct(EQ) %{bv1} % [2,4,6,8,10: %] cases d in Hbv1 EQd;
     1494     normalize nodelta [1,3,5,7,9: #n #H #_ @H] #R1 whd in ⊢ (??%% → ?); #EQ destruct(EQ)
     1495     #EQd >hwreg_retrieve_hwregstore_miss % #EQ destruct(EQ)
     1496     inversion(colouring ???) in EQd; [1,3,5,7,9: #n #_ >(proj2 … acc_spec) #EQ destruct]
     1497     #R2 #EQr2 #ABS cases(colouring_is_never_forbidden … EQfn2 … EQr2)
     1498     [5: #H #_ |*: #_ * [4: #H #_ |*: #_ * [3: #H #_ |*: #_ * [2: #H #_ | #_ * #_ * #_ * #_ * #H #_ ] ] ]]
     1499     cases((proj1 … acc_spec) R2 H) #H1 @H1 <ABS %
     1500  ]
     1501|6,7,8,9,10: %
     1502  [1,3,5,7,9: whd in match hwreg_retrieve_sp in ⊢ (???%); normalize nodelta
     1503    whd in match set_regs; normalize nodelta >hwreg_retrieve_hwregstore_miss
     1504    [2,4,6,8,10: normalize % #EQ destruct] >hwreg_retrieve_hwregstore_miss
     1505    [2,4,6,8,10: normalize % #EQ destruct] @(proj1 … Hhw_rel)
     1506  |*: whd in match set_regs; normalize nodelta #R @andb_elim @if_elim
     1507    #R_live [2,4,6,8,10: *] #H
     1508    cases (all_All … (λx.¬eq_Register R x) RegisterAlwaysDead) #H1 #H2
     1509    lapply(H1 H) -H1 -H * @eq_Register_elim #R_noA ** @eq_Register_elim #R_noB **
     1510    @eq_Register_elim #R_noDPL ** @eq_Register_elim #R_noDPH ** @eq_Register_elim #R_noST1 * #_
     1511    >hdw_same_colouring normalize nodelta >hwreg_retrieve_hwregstore_miss
     1512    [2,4,6,8,10: assumption] lapply((proj2 … Hhw_rel) R ?) [2,4,6,8,10: >hdw_same_colouring #H @H]
     1513    @andb_Prop [1,3,5,7,9: assumption] @H2 %
     1514    [1,3,5,7,9: @eq_Register_elim try (#_ @I) #EQ >EQ in R_noA; * #H @H %]
     1515    % [1,3,5,7,9: @eq_Register_elim try (#_ @I) #EQ >EQ in R_noB; * #H @H %]
     1516    % [1,3,5,7,9: @eq_Register_elim try (#_ @I) #EQ >EQ in R_noDPL; * #H @H %]
     1517    % [1,3,5,7,9: @eq_Register_elim try (#_ @I) #EQ >EQ in R_noDPH; * #H @H %]
     1518    % [1,3,5,7,9: @eq_Register_elim try (#_ @I) #EQ >EQ in R_noST1; * #H @H %] @I
     1519  ]
     1520|11,12,13,14,15: %{sp} %
     1521  [1,3,5,7,9: whd in ⊢ (??%?); whd in match set_regs; normalize nodelta
     1522    >hwreg_retrieve_hwregstore_miss [2,4,6,8,10: normalize % #EQ destruct]
     1523    >hwreg_retrieve_hwregstore_miss [2,4,6,8,10: normalize % #EQ destruct] assumption
     1524  |*: #r #d * normalize nodelta @andb_elim @if_elim #r_live * #EQd cases d in EQd;
     1525    [1,3,5,7,9: #n |*: #R ] #EQcol normalize nodelta
     1526    [1,2,3,4,5: whd in match (m ??); @(Hpsd_reg r (decision_spill n)) % [2,4,6,8,10: assumption]
     1527       @andb_Prop try assumption @I
     1528    |*: >hwreg_retrieve_hwregstore_miss
     1529       [1,3,5,7,9: @(Hpsd_reg r (decision_colour R)) % [2,4,6,8,10: assumption] @andb_Prop try assumption @I]
     1530       cases(colouring_is_never_forbidden … EQfn … EQcol) [5: #H #_ assumption]
     1531       #_ * [4: #H #_ assumption] #_ * [3: #H #_ assumption] #_ * [2: #H #_ assumption ]
     1532       #_ * #_ * #_ * #_ * #H #_ assumption
     1533    ]
     1534  ]
     1535]
     1536qed.
     1537
     1538
     1539
     1540
     1541
     1542
     1543(*
     1544[ whd in match read_arg_decision; normalize nodelta >m_return_bind
     1545  whd in match write_decision; normalize nodelta @eq_Register_elim
     1546  [ #EQ destruct(EQ) whd in match set_regs; normalize nodelta
     1547    #st1'
     1548 * [ #src_spill | #src_col ] * [1,3: #dst_spill |*: #dst_col ] #f #fn
     1549#EQfn #v #EQsrc #v_live #Hsrc #st1' #st2 *** #Rst1st2 #Hv #Hspill #Hinterf
     1550>move_spec [2,4,6,8: assumption] #st1 whd in ⊢ (??%% → ?); #EQ destruct(EQ)
     1551normalize nodelta
     1552[ @eqb_elim normalize nodelta
     1553  [ #EQ destruct(EQ) %{st2} %{(refl …)} @(gen_state_rel_ext_color_fun … EQfn … Rst1st2)
     1554    #v' whd in match update_fun; normalize nodelta @eq_vertex_elim [2: #_ %]
     1555    #EQ destruct assumption ]
     1556  normalize nodelta in Hspill; cases Rst1st2
     1557  #f1 * #fn1 * >EQfn whd in ⊢ (??%% → ?); #EQ destruct(EQ)
     1558  inversion(st_frms ??) [1,3: #_ *] #frames #EQframes normalize nodelta *****
     1559  #Hmem #Hframes #Hhw_reg #His #Hcarry * #ptr * #EQptr #Hpsd_reg
     1560  cases v in v_live Hv EQsrc Hinterf; -v [ #r | #R ] #Hlive normalize nodelta
     1561  [ * #bv #EQbv | #_ ] #EQsrc #Hinterf
     1562  [ cases(Hpsd_reg … EQbv) [3: % assumption |2:] #bv' normalize nodelta *
     1563  #H lapply(opt_eq_from_res ???? H) -H #EQbv' #EQ destruct(EQ) #Hsrc_dst
     1564  cases(shift_pointer_commute
     1565          (bitvector_of_nat 8 ((joint_if_local_stacksize … fn1) + src_spill))
     1566          (carry … st2) …
     1567          〈hwreg_retrieve (regs LTL_semantics st2) RegisterSPL,
     1568           hwreg_retrieve (regs LTL_semantics st2) RegisterSPH〉 …)
     1569  [5: lapply EQptr change with (hwreg_retrieve_sp ?) in match (sp ??);
     1570      whd in match hwreg_retrieve_sp; normalize nodelta #H @('bind_inversion H)
     1571      #ptr1 #EQptr1 #H >EQptr1 in ⊢ (??%?); >m_return_bind
     1572      whd in match xpointer_of_pointer; normalize nodelta
     1573      >H >m_return_bind %
     1574  |3: %
     1575  |*:
     1576  ]
     1577  #ptr1 * #H @('bind_inversion H) -H #val1 #EQval1 #H @('bind_inversion H) -H
     1578  #val2 #EQval2 #EQptr1 #EQ destruct(EQ)
     1579  cases(shift_pointer_commute
     1580         (bitvector_of_nat 8 ((joint_if_local_stacksize … fn1) + dst_spill))
     1581          (\snd  val2) …
     1582          〈hwreg_retrieve (regs LTL_semantics st2) RegisterSPL,
     1583           hwreg_retrieve (regs LTL_semantics st2) RegisterSPH〉 …)
     1584  [5: lapply EQptr change with (hwreg_retrieve_sp ?) in match (sp ??);
     1585      whd in match hwreg_retrieve_sp; normalize nodelta #H @('bind_inversion H)
     1586      #ptr1 #EQptr1 #H >EQptr1 in ⊢ (??%?); >m_return_bind
     1587      whd in match xpointer_of_pointer; normalize nodelta
     1588      >H >m_return_bind %
     1589  |3: %
     1590  |*:
     1591  ]
     1592  #ptr2 * #H @('bind_inversion H) -H #val3 #EQval3 #H @('bind_inversion H) -H
     1593  #val4 #EQval4 #EQptr2 #EQ destruct(EQ) %
     1594  [2: %
     1595      [ whd in match read_arg_decision; normalize nodelta >m_return_bind >m_return_bind
     1596        >EQval1 in ⊢ (??%?); >m_return_bind >EQval2 in ⊢ (??%?);
     1597        >m_return_bind >EQptr1 in ⊢ (??%?); >m_return_bind >EQbv' in ⊢ (??%?);
     1598        >m_return_bind whd in match set_regs; whd in match set_carry; normalize nodelta
     1599        whd in match write_decision; normalize nodelta >m_return_bind >m_return_bind
     1600        >hwreg_retrieve_hwregstore_miss [2: normalize % #EQ destruct]
     1601        >hwreg_retrieve_hwregstore_miss in ⊢ (??(????(?????%?)?)?);
     1602        [2: normalize % #EQ destruct]
     1603        >hwreg_retrieve_hwregstore_miss in ⊢ (??(????(?????%?)?)?);
     1604        [2: normalize % #EQ destruct]
     1605        >hwreg_retrieve_hwregstore_miss [2: normalize % #EQ destruct]
     1606        >hwreg_retrieve_hwregstore_miss [2: normalize % #EQ destruct]
     1607        >hwreg_retrieve_hwregstore_miss [2: normalize % #EQ destruct]
     1608        >EQval3 in ⊢ (??%?); >m_return_bind >EQval4 in ⊢ (??%?);
     1609        >m_return_bind >EQptr2 in ⊢ (??%?); >m_return_bind
     1610        >(opt_to_opt_safe … (Hspill … EQptr bv')) in ⊢ (??%?); >m_return_bind
     1611        whd in match set_m; normalize nodelta whd in match set_regs; normalize nodelta
     1612        whd in match set_carry; normalize nodelta <commute_if in ⊢ (??%?); %
     1613      | %{f1} %{fn1} %{EQfn} >EQframes normalize nodelta %
     1614        [2: %{ptr} %
     1615        [ change with (hwreg_retrieve_sp ?) in match (sp ??); @if_elim #c_live
     1616          whd in match hwreg_retrieve_sp; normalize nodelta
     1617          [ >hwreg_retrieve_insensitive_to_set_other  >hwreg_retrieve_insensitive_to_set_other ]
     1618          >hwreg_retrieve_hwregstore_miss [2,4: normalize % #EQ destruct]
     1619          whd in ⊢ (??%?);
     1620          try >hwreg_retrieve_hwregstore_miss in ⊢ (??(match (?(???%?)) with [ _ ⇒ ? | _ ⇒ ? ])?);
     1621          [1,3: try >hwreg_retrieve_hwregstore_miss in ⊢ (??(match (?(???%?)) with [ _ ⇒ ? | _ ⇒ ? ])?);
     1622          [1,3: try >hwreg_retrieve_hwregstore_miss in ⊢ (??(match (?(???%?)) with [ _ ⇒ ? | _ ⇒ ? ])?);
     1623          [1,3: try >hwreg_retrieve_hwregstore_miss in ⊢ (??(match (?(???%?)) with [ _ ⇒ ? | _ ⇒ ? ])?);
     1624          [1,3: try >hwreg_retrieve_hwregstore_miss in ⊢ (??(match (?(???%?)) with [ _ ⇒ ? | _ ⇒ ? ])?);
     1625          [1,3: try >hwreg_retrieve_hwregstore_miss in ⊢ (??(match (?(????%)) with [ _ ⇒ ? | _ ⇒ ? ])?);
     1626             [1,3: try >hwreg_retrieve_hwregstore_miss in ⊢ (??(match (?(????%)) with [ _ ⇒ ? | _ ⇒ ? ])?);
     1627          [1,3: try >hwreg_retrieve_hwregstore_miss in ⊢ (??(match (?(????%)) with [ _ ⇒ ? | _ ⇒ ? ])?);
     1628          [1,3: try >hwreg_retrieve_hwregstore_miss in ⊢ (??(match (?(????%)) with [ _ ⇒ ? | _ ⇒ ? ])?);
     1629          [1,3: try >hwreg_retrieve_hwregstore_miss in ⊢ (??(match (?(????%)) with [ _ ⇒ ? | _ ⇒ ? ])?);
     1630          [1,3: try >hwreg_retrieve_hwregstore_miss in ⊢ (??(match (?(????%)) with [ _ ⇒ ? | _ ⇒ ? ])?);
     1631          [1,3: assumption ]]]]]]]]]]] normalize % #EQ destruct
     1632        | cases carry_live -carry_live normalize nodelta #r1 #d1 * #r1_live
     1633          whd in match update_fun; normalize nodelta @eq_vertex_elim
     1634          [1,3: #EQ destruct(EQ) normalize nodelta #EQ destruct(EQ) normalize nodelta
     1635            #bv1 change with (ps_reg_retrieve ??) in ⊢ (??%? → ?); >EQbv whd in ⊢ (??%% → ?);
     1636            #EQ destruct(EQ) %{bv'} % [2,4: %] @opt_safe_elim #m' #EQm'
     1637            >(beloadv_bestorev_hit … EQm') %         
     1638          |*: #Hdiff normalize nodelta #EQ destruct(EQ) inversion(color_fun ???)
     1639             [1,3: #n1 #EQn1 normalize nodelta #bv1 #EQbv1
     1640               letin ptr1 ≝ (shift_pointer ? ptr (bitvector_of_nat ? ((joint_if_local_stacksize … fn1) + dst_spill)))
     1641               letin ptr2≝ (shift_pointer ? ptr (bitvector_of_nat ? ((joint_if_local_stacksize … fn1) + n1)))
     1642               cut(bool_to_Prop(eq_pointer … ptr1 ptr2) ∨ bool_to_Prop (¬ eq_pointer … ptr1 ptr2))
     1643               [1,3: @eq_pointer_elim #_ [1,3: %% |*: %2 %]] * @eq_pointer_elim
     1644               #Hptr * 
     1645               [1,3: %{bv'} % [1,3: @opt_safe_elim #m' >Hptr #EQm' >(beloadv_bestorev_hit … EQm') %]
     1646                 normalize nodelta in Hinterf;
     1647                 cut(∀A.∀x,y.m_return Res A x = m_return Res A y → x = y)
     1648                 [1,3: #A #x #y whd in ⊢ (??%% → ?); #EQ destruct(EQ) %] #H @H -H
     1649                 <EQbv <EQbv1
     1650                 cut(n1 = dst_spill) [1,3: cases daemon (*TODO*) ] #EQ destruct(EQ)
     1651                 lapply(Hinterf (inl ?? r1) ? r1_live EQn1) [1,3: % #EQ destruct cases Hdiff #H @H %]
     1652                 whd in match ertl_vertex_retrieve; normalize nodelta #H >H %
     1653               |*: cases(Hpsd_reg … EQbv1) [3,6: % try assumption |*:]
     1654                 #bv2 normalize nodelta * #H lapply(opt_eq_from_res ???? H) -H
     1655                 #EQbv2 #EQ destruct(EQ) %{bv2} % try % @opt_safe_elim
     1656                 #m' #EQm' >(beloadv_bestorev_miss … Hptr EQm') whd in match ptr2;
     1657                 >EQbv2 %
     1658               ]
     1659             |*: cases daemon (*TODO*)       
     1660             ]
     1661          ]
     1662        ]
     1663      | cases daemon (*TODO*)
     1664      ]
     1665  ]]]] cases daemon (*TODO*) 
     1666qed.*)
    6791667
    6801668lemma cond_commute :∀fix_comp,colour,prog,init_regs,f_lbls,f_regs.
     
    6831671let n ≝ \snd (ertl_to_ltl fix_comp colour prog) in
    6841672let stacksizes ≝ lookup_stack_cost … m in
    685 let init ≝ (λglobals,fn.«translate_data fix_comp colour globals fn,?») in
     1673let init ≝ translate_data fix_comp colour in
    6861674cond_commutation_statement ERTL_semantics LTL_semantics prog stacksizes
    6871675 init init_regs
    688  f_lbls f_regs (state_rel fix_comp colour prog)
     1676 f_lbls f_regs (state_rel fix_comp colour prog init_regs f_lbls f_regs)
    6891677 (state_pc_rel fix_comp colour prog init_regs f_lbls f_regs).
    690 [2: @hide_prf %]
    6911678#fix_comp #colour #prog #init_regs #f_lbls #f_regs
    6921679whd in match cond_commutation_statement; normalize nodelta
    6931680#st1 #st2 #f #fn #r #ltrue #lfalse #bv #b * #Hbl #EQfetch
    694 whd in match acca_retrieve; normalize nodelta change with (ps_reg_retrieve ??) in ⊢ (??%? → ?);
    695 #EQbv #EQb #Rst1st2 #t_fn #EQt_fn whd normalize nodelta %{(refl …)} #mid #EQmid
    696 cases(ps_reg_retrieve_hw_reg_retrieve_commute fix_comp colour prog init_regs f_lbls
    697 f_regs fn (pc … st1) … (colouring … (inl ?? r)) … EQbv)
    698 [6: %
    699 |2: @(st_no_pc … st2)
    700 |5: whd %{f} %{fn} >(proj1 … (fetch_statement_inv … EQfetch)) %{(refl …)}
    701     @(fetch_ok_sigma_state_ok … Rst1st2 …
    702          (proj1 ?? (fetch_statement_inv … EQfetch)))
     1681whd in match acca_retrieve; normalize nodelta
     1682change with (ps_reg_retrieve ??) in ⊢ (??%? → ?);
     1683#EQbv #EQb whd in match state_pc_rel; normalize nodelta ** #Rst1st2 #_ #_
     1684#t_fn #_ #z1 #z2 #z3 #z4 #z5 #z6 #z7 #z8 whd #EQinit_regs
     1685whd normalize nodelta %{(refl …)} #mid #_ <EQinit_regs
     1686cases(ps_reg_retrieve_hw_reg_retrieve_commute prog ???? init_regs f_lbls
     1687f_regs f fn (pc … st1) ?????????)
     1688[6: @(proj1 … (fetch_statement_inv … EQfetch))
     1689|11: @Rst1st2
     1690|9: @r
     1691|12: % [ @andb_Prop [ @(all_used_are_live_before … (proj2 … (fetch_statement_inv … EQfetch))) // | @I ] | %]
     1692|14: @EQbv
    7031693|*:
    7041694]
    705 #bv1 * inversion(colouring … (inl ?? r))
    706 [ #n #EQcolouring
    707 | #R #EQcolouring
    708   cases(colouring_reg_non_DPL_DPH …
    709                       (proj1 ?? (fetch_statement_inv … EQfetch)) … EQcolouring)
    710   * #RnoDPL #RnoDPH #RnoA
     1695#bv1 * whd in match m_map; normalize nodelta #H @('bind_inversion H) -H
     1696* #bv2 #st2' #EQst2' whd in ⊢ (??%% → ?); #EQ1 #EQ2  destruct(EQ1 EQ2)
     1697(*letin after ≝ (λfn,callee.analyse_liveness fix_comp (prog_names … prog) fn callee)
     1698letin before ≝ (λfn,callee.livebefore … fn callee (after fn callee))
     1699letin live_fun ≝ (λfn,callee,l,v.in_lattice v ((before fn callee) l) ∧
     1700                   match v with [ inl r ⇒ true
     1701                | inr R ⇒ all … (λR'.¬ eq_Register R R') RegisterAlwaysDead
     1702                ]) *)
     1703letin aft ≝ (analyse_liveness fix_comp (prog_names … prog) fn (init_regs (pc_block (pc … st1))))
     1704letin carry_lives ≝ (h_in_lattice RegisterCarry (aft (point_of_pc ERTL_semantics (pc … st1))))
     1705letin color_of_r ≝ (colouring … (colour (prog_names … prog) fn aft (init_regs (pc_block (pc … st1))))(inl ?? r))
     1706(*letin color_fun ≝ (λfn1,callee,v.colouring … (colour (prog_names … prog) fn1 aft callee) v) *)
     1707cases(move_preserve fix_comp colour prog (translate_data fix_comp colour)  …
     1708       … init_regs f_lbls f_regs (pc … st1) carry_lives color_of_r RegisterA …
     1709      (proj1 ?? (fetch_statement_inv … EQfetch)) (inl ?? r) (inr ?? RegisterA) …
     1710      (st_no_pc … st1) (st_no_pc … st2) … (refl …))
     1711[8: % [2: #x #_ @I] %{Rst1st2} normalize nodelta % [2: @EQbv |]
     1712|4: %
     1713|5: @hdw_same_colouring
     1714|6: @andb_Prop [2: @I] whd in match (livebefore ?????);
     1715    change with (stmt_at ??? (point_of_pc ERTL_semantics ?)) in
     1716                           ⊢ (?(??match % with [_ ⇒ ? | _ ⇒ ? ]));
     1717    >(proj2 … (fetch_statement_inv … EQfetch)) normalize nodelta
     1718    whd in match statement_semantics; normalize nodelta 
     1719    whd in match statement_semantics; normalize nodelta
     1720    whd in match (defined ??); whd in match (used ???);
     1721    @set_member_union2 @set_member_singl
     1722|7: inversion(color_of_r) [#n | #R ] #EQcol [@I] 
     1723    cases(colouring_is_never_forbidden …
     1724                      (proj1 ?? (fetch_statement_inv … EQfetch)) … EQcol)  #_ * #_ *
     1725    #H1 * #H2 #_ % assumption
     1726|*:
    7111727]
    712 whd in match m_map; normalize nodelta #H @('bind_inversion H) -H *
    713 #bv2 #st' #EQbv2 whd in ⊢ (??%% → ?); #EQ1 #EQ2 destruct(EQ1 EQ2)
    714 % [2,4: %
    715      [1,3: >map_eval_add_dummy_variance_id in ⊢ (??%?); >move_spec in ⊢ (??%?);
    716        [2: @I | 4:  %{RnoDPL RnoDPH}] normalize nodelta
    717        [ >EQbv2 in ⊢ (??%?); | >EQbv2 in ⊢ (??%?); ] >m_return_bind
    718        whd in match write_decision; normalize nodelta >m_return_bind
    719        >m_return_if_commute in ⊢ (??%?); %
    720      |*: %
    721        [1,3: whd %{f} %{fn} %
    722            [1,3,5,7: @if_elim #_ >(proj1 … (fetch_statement_inv … EQfetch)) %]
    723            normalize nodelta
    724            lapply(fetch_ok_sigma_state_ok … Rst1st2 …
    725                                     (proj1 ?? (fetch_statement_inv … EQfetch)))
    726            normalize nodelta inversion (st_frms … (st_no_pc … st1)) [1,3: #_ * ]
    727            #frames #EQframes normalize nodelta #R_nopc_st1st2
    728            [ inversion(hlives RegisterCarry
    729               (analyse_liveness fix_comp
    730                (prog_names ERTL_semantics prog) fn
    731                (point_of_pc ERTL_semantics (pc … st1))))
    732              [ #carry_live | #carry_dead ]
    733            | @eq_Register_elim [ #EQ destruct(EQ) @⊥ cases RnoA #H @H %] #_
    734            ]
    735            normalize nodelta
    736            [ >insensitive_sb_to_hwreg_set_other
    737              whd in match set_regs in ⊢ (???(????(??%?))); normalize nodelta ]
    738            <insensitive_to_be_cleared_sb_regs
    739            [2,4,6: @dead_registers_in_dead @acc_is_dead ]
    740            [ whd in match set_regs; whd in match set_carry; normalize nodelta
    741              change with (set_carry ? (carry … (st_no_pc … st2)) st') in ⊢ (???(????%));
    742              >set_carry_sigma_sb_state_commute
    743            |*: >set_regs_eta
    744            ]
    745            <(carry_sensitive_read_arg_decision … EQbv2)
    746            [2,3,5,6,8,9: @dead_registers_in_dead [1,3,5: @dph_is_dead |*: @dpl_is_dead]]
    747            [ >set_carry_sigma_sb_state_commute
    748              change with (set_carry ?? (sigma_sb_state ? prog ? (st_no_pc … st2)))
    749                                                                             in ⊢ (???%);
    750              >set_carry_eta
    751            | >insensitive_to_be_cleared_carry
    752              [2: @dead_registers_in_dead cases daemon (*????*) ]
    753            | whd in EQbv2 : (??%%); destruct(EQbv2) >set_carry_eta
    754            ]
    755            @(eq_sigma_state_monotonicity … EQframes … R_nopc_st1st2)
    756            cases b normalize nodelta >point_of_pc_of_point
    757            letin after ≝ (analyse_liveness fix_comp … fn)
    758            letin before ≝ (livebefore … fn after)
    759            lapply (included_livebefore_livebeafter_stmt_labels
    760                       fix_comp … (proj2 ?? (fetch_statement_inv … EQfetch)))
    761            normalize in match (stmt_labels ???);
    762            change with after in match after;
    763            #H [2,4,6: lapply (H lfalse ?) [1,3,5: >memb_hd % ]
    764               |*: lapply (H ltrue ?) [1,3,5: >memb_cons try % >memb_hd %]]
    765            #K change with (bool_to_Prop (rl_included ??)) in K;
    766            @(rl_included_transitive … K) whd in match (livebefore ????);
    767            cases(fetch_statement_inv … EQfetch) #_ normalize nodelta
    768            whd in ⊢ (??%? → ?); #EQstmt >EQstmt normalize nodelta
    769            @rl_included_rl_join_left normalize in match (defined ??);
    770            @rl_included_rl_diff_rl_empty
    771        |*: %{it} %{(refl …)} %{bv1} %
    772            [1,3: [ @if_elim #_
    773                  | @eq_Register_elim [ #EQ destruct(EQ) @⊥ cases RnoA #H @H %] #_
    774                  ]
    775                  normalize nodelta change with (hw_reg_retrieve ??) in ⊢ (??%?);
    776                  whd in match hw_reg_retrieve; normalize nodelta @eq_f
    777                  whd in match set_regs; normalize nodelta
    778                  [ >hwreg_retrieve_insensitive_to_set_other]
    779                  >hwreg_retrieve_hwregstore_hit %
    780            |*: cases(bool_of_beval_sigma_commute fix_comp colour prog init_regs
    781                       f_lbls f_regs … bv1 … EQb) [2,4: %] #b1 * #EQb1 #EQ destruct(EQ)
    782                       assumption
    783            ]
    784        ]
    785     ]     
     1728#st2'' * #EQst2'' #Hst2'' %{st2''} % [ >map_eval_add_dummy_variance_id assumption ]
     1729%
     1730[ cases daemon (*TODO*)
     1731| %{it} %{(refl …)}
     1732  cases(ps_reg_retrieve_hw_reg_retrieve_commute prog ???? init_regs f_lbls
     1733        f_regs f fn (pc … st1) ?????????)
     1734  [6: @(proj1 … (fetch_statement_inv … EQfetch))
     1735  |11: @Hst2''
     1736  |14: @EQbv
     1737  |12: % [2: %] whd in match update_fun; normalize nodelta @andb_Prop [2: %]
     1738       whd in match (livebefore ?????);
     1739       change with (stmt_at ??? (point_of_pc ERTL_semantics ?)) in
     1740                         ⊢ (?(??match % with [_ ⇒ ? | _ ⇒ ? ]));
     1741       >(proj2 … (fetch_statement_inv … EQfetch)) normalize nodelta
     1742       whd in match statement_semantics; normalize nodelta 
     1743       whd in match statement_semantics; normalize nodelta
     1744       whd in match (defined ??); whd in match (used ???);
     1745       @set_member_union2 @set_member_singl
    7861746  |*:
    7871747  ]
    788 qed.
     1748  #bv2 * whd in ⊢ (??%% → ?); whd in match read_arg_decision; normalize nodelta
     1749  whd in match update_fun; normalize nodelta @eq_vertex_elim [2: * #H @⊥ @H %] #_
     1750  normalize nodelta #H1 #EQ1 %{bv2} %{H1} >EQ1 in EQb; #EQb
     1751  cases(bool_of_beval_sigma_commute … EQb) [9: %|*:] #b1 * #H2 #EQ2 destruct
     1752  assumption
     1753]
     1754qed. 
     1755 
     1756   whd in match eq_vertex; normalize nodelta
     1757  whd  in match eq_identifier; normalize nodelta normalize nodelta
     1758         
     1759 
     1760     
     1761              [2: @if_elim #_ [ >hwreg_retrieve_insensitive_to_set_other ] ]
     1762              >hwreg_retrieve_hwregstore_hit %]
     1763            cases(bool_of_beval_sigma_commute fix_comp colour prog init_regs f_lbls
     1764                    f_regs … bv1 (refl …) … EQb) #b1 * #H #EQ destruct assumption
     17654: % [2: #x #_ @I] % [ @Rst1st2  %{Rst1st2}               
     1766
     1767
     1768
     1769inversion(colouring … (inl … r)) [ #n | #R ] #EQcolouring >EQcolouring in EQst2';
     1770#EQst2'
     1771[2: cases(colouring_is_never_forbidden …
     1772                      (proj1 ?? (fetch_statement_inv … EQfetch)) … EQcolouring)
     1773   #RnoA * #_ * #RnoDPL * #RnoDPH #_ ] >map_eval_add_dummy_variance_id
     1774letin after ≝ (λfn,callee.analyse_liveness fix_comp (prog_names … prog) fn callee)
     1775letin before ≝ (λfn,callee.livebefore … fn callee (after fn callee))
     1776letin live_fun ≝ (λfn,callee,l,v.in_lattice v ((before fn callee) l) ∧
     1777                   match v with [ inl r ⇒ true
     1778                | inr R ⇒ all … (λR'.¬ eq_Register R R') RegisterAlwaysDead
     1779                ])
     1780<EQinit_regs in EQcolouring; #EQcolouring
     1781letin aft ≝ (analyse_liveness fix_comp (prog_names … prog) fn (init_regs (pc_block (pc … st1))))
     1782letin carry_lives ≝ (h_in_lattice RegisterCarry (aft (point_of_pc ERTL_semantics (pc … st1))))
     1783cases(move_preserve fix_comp colour prog (translate_data fix_comp colour)  …
     1784      live_fun … init_regs f_lbls f_regs (pc … st1) carry_lives …
     1785      (proj1 ?? (fetch_statement_inv … EQfetch)) … EQcolouring)
     1786[2: @RegisterA
     1787|3:   xxxxxxx   … init_regs … (return st1))   
     1788   
     1789   
     1790[2,4: %
     1791   [1,3: >map_eval_add_dummy_variance_id in ⊢ (??%?); >move_spec in ⊢ (??%?);
     1792         [2: % // |4: @I] normalize nodelta
     1793         [ @eq_Register_elim [ #EQ destruct @⊥ elim RnoA #H @H %] normalize nodelta #_ ]
     1794         try >EQst2' in ⊢ (??%?); try >m_return_bind in ⊢ (??%?); whd in match write_decision;
     1795         normalize nodelta try >m_return_bind in ⊢ (??%?);
     1796         [2: >m_return_if_commute in ⊢ (??%?);] %
     1797   |*: %
     1798       [1,3: [ whd in match hwreg_store; normalize nodelta @state_rel_insensitive_to_dead_Reg whd in match state_rel; normalize nodelta %{f} %{fn} %
     1799          [1,3: cases b @(proj1 … (fetch_statement_inv … EQfetch)) ]
     1800          cases Rst1st2 #f1 * #fn1 >(proj1 … (fetch_statement_inv … EQfetch)) *
     1801          whd in ⊢ (??%% → ?); #EQ destruct(EQ) normalize nodelta
     1802          cases(st_frms ??) [1,3: * ] #frames normalize nodelta ***** #Hmem #Hframes
     1803          #Hhw_reg #His #Hcarry * #stack_ptr * #EQsp #Hps_reg
     1804          whd in match read_arg_decision in EQst2'; normalize nodelta in EQst2';
     1805          [2:  >m_return_bind in EQst2'; >m_return_bind #H @('bind_inversion H) -H
     1806               * #x1 #x2 #_ #H @('bind_inversion H) -H * #y1 #y2 #_ #H @('bind_inversion H) -H
     1807               #ptr #_ #H @('bind_inversion H) -H #val #_ whd in ⊢ (??%% → ?); #EQst2'
     1808          | whd in EQst2' : (??%%);
     1809          ]
     1810          destruct(EQst2') %
     1811          [2,4: %{stack_ptr} %
     1812             [1,3: [ @if_elim #_] whd in match (sp ??); whd in match set_regs;
     1813                normalize nodelta
     1814                [ >hwreg_retrieve_insensitive_to_set_other
     1815                  >hwreg_retrieve_insensitive_to_set_other ]
     1816                >hwreg_retrieve_hwregstore_miss [2,4,6: % normalize #EQ destruct(EQ)]
     1817                [1,2: try >hwreg_retrieve_hwregstore_miss in ⊢ (??(match (?(???%?)) with [_ ⇒ ? | _ ⇒ ?])?);
     1818                   [2,4: % normalize #EQ destruct(EQ)]
     1819                   try >hwreg_retrieve_hwregstore_miss in ⊢ (??(match (?(???%?)) with [_ ⇒ ? | _ ⇒ ?])?);
     1820                   [2,4: % normalize #EQ destruct(EQ)] ]
     1821                >hwreg_retrieve_hwregstore_miss [2,4,6: % normalize #EQ destruct(EQ)]
     1822                [1,2: try >hwreg_retrieve_hwregstore_miss in ⊢ (??(match (?(????%)) with [_ ⇒ ? | _ ⇒ ?])?);
     1823                   [2,4: % normalize #EQ destruct(EQ)]
     1824                   try >hwreg_retrieve_hwregstore_miss in ⊢ (??(match (?(????%)) with [_ ⇒ ? | _ ⇒ ?])?);
     1825                   [2,4: % normalize #EQ destruct(EQ)] ]
     1826                assumption
     1827             |*: whd in match ps_relation; normalize nodelta #r1 #d1 *
     1828                <commute_if in ⊢ (% → ?); whd in match (pc_block ?); >point_of_pc_of_point
     1829                #Hr1 [ <commute_if in ⊢ (% → ?); whd in match (pc_block ?); ] #Hd1
     1830                #val1 #EQval1 cases(Hps_reg r1 d1 … EQval1)
     1831                [1,3: #val2 * #Hval2 #EQ destruct(EQ) %{val2} % [2,4: %]
     1832                   cases d1 in Hval2 Hd1; -d1 [1,3: #n1 |*: #R1] normalize nodelta
     1833                   [1,2: #EQbeload |*: whd in ⊢ (??%% → ?); #EQ destruct(EQ)]
     1834                   #Hdecision [1,2: [ @if_elim #_] assumption | @if_elim #_ ]
     1835                   @eq_f whd in match set_regs; whd in match set_carry;
     1836                   normalize nodelta
     1837                   cases(colouring_reg_non_DPL_DPH …
     1838                        (proj1 ?? (fetch_statement_inv … EQfetch)) … Hdecision) *
     1839                   #H1 #H2 #H3 [ >hwreg_retrieve_insensitive_to_set_other]
     1840                   >hwreg_retrieve_hwregstore_miss try assumption [3: %]
     1841                   >hwreg_retrieve_hwregstore_miss try assumption
     1842                   >hwreg_retrieve_hwregstore_miss try assumption %
     1843                |*: % [2,4: assumption]
     1844                    change with (bool_to_Prop (set_member ????))
     1845                    whd in match (livebefore ?????);
     1846                    change with (stmt_at ??? (point_of_pc ERTL_semantics ?)) in
     1847                          ⊢ (?(????(???match % with [_ ⇒ ? | _ ⇒ ? ])));
     1848                    >(proj2 … (fetch_statement_inv … EQfetch)) normalize nodelta
     1849                    whd in match statement_semantics; normalize nodelta
     1850                    whd in match (defined ??); whd in match (used ???);
     1851                    @set_member_union1 @set_member_diff [2,4: @set_member_empty]
     1852                    @(set_member_subset_if … Hr1)
     1853                    lapply(included_livebefore_livebeafter_stmt_labels
     1854                                 fix_comp … (init_regs (pc_block (pc … st1))) …
     1855                                 (proj2 ?? (fetch_statement_inv … EQfetch))
     1856                                 (if b then ltrue else lfalse) ?)
     1857                    [1,3: cases b normalize nodelta
     1858                          whd in match stmt_labels; whd in match stmt_explicit_labels;
     1859                          whd in match step_labels; normalize nodelta
     1860                          [1,3: >memb_cons [1,3: @I |*: @memb_hd] |*: >memb_hd @I ] ]
     1861                    whd in match (l_included ???); cases(set_subset ???)
     1862                    normalize nodelta [2,4: * |*: #_ @I]
     1863                ]     
     1864             ]
     1865          |*: %
     1866             [2,4: <commute_if in ⊢ (% → ?); whd in match (pc_block ?); >point_of_pc_of_point
     1867                #Hcarry1
     1868                [ <EQinit_regs @if_elim
     1869                  [ #H @Hcarry change with (bool_to_Prop (set_member ????))
     1870                    whd in match (livebefore ?????);
     1871                    change with (stmt_at ??? (point_of_pc ERTL_semantics ?)) in
     1872                           ⊢ (?(????(???match % with [_ ⇒ ? | _ ⇒ ? ])));
     1873                    >(proj2 … (fetch_statement_inv … EQfetch)) normalize nodelta
     1874                    whd in match statement_semantics; normalize nodelta
     1875                    whd in match (defined ??); whd in match (used ???);
     1876                    @set_member_union1 @set_member_diff [2: @set_member_empty]
     1877                    @(set_member_subset_if … Hcarry1)
     1878                    lapply(included_livebefore_livebeafter_stmt_labels
     1879                                 fix_comp … (init_regs (pc_block (pc … st1))) …
     1880                                 (proj2 ?? (fetch_statement_inv … EQfetch))
     1881                                 (if b then ltrue else lfalse) ?)
     1882                    [1,3: cases b normalize nodelta
     1883                          whd in match stmt_labels; whd in match stmt_explicit_labels;
     1884                          whd in match step_labels; normalize nodelta
     1885                          [1,3: >memb_cons [1,3: @I |*: @memb_hd] |*: >memb_hd @I ] ]
     1886                    whd in match (l_included ???); cases(set_subset Register ??)
     1887                    [ #_ @I] @if_elim #_ *
     1888                  | #ABS @⊥ elim(Prop_notb … ABS) #H @H -H
     1889                    @(set_member_subset_if … Hcarry1)
     1890                    lapply(included_livebefore_livebeafter_stmt_labels
     1891                                 fix_comp … (init_regs (pc_block (pc … st1))) …
     1892                                 (proj2 ?? (fetch_statement_inv … EQfetch))
     1893                                 (if b then ltrue else lfalse) ?)
     1894                    [1,3: cases b normalize nodelta
     1895                          whd in match stmt_labels; whd in match stmt_explicit_labels;
     1896                          whd in match step_labels; normalize nodelta
     1897                          [1,3: >memb_cons [1,3: @I |*: @memb_hd] |*: >memb_hd @I ] ]
     1898                    whd in match (l_included ???); cases(set_subset Register ??)
     1899                    [ #_ @I] @if_elim #_ *
     1900                  ] 
     1901                | whd in match set_regs; normalize nodelta @Hcarry
     1902                  change with (bool_to_Prop (set_member ????))
     1903                  whd in match (livebefore ?????);
     1904                  change with (stmt_at ??? (point_of_pc ERTL_semantics ?)) in
     1905                          ⊢ (?(????(???match % with [_ ⇒ ? | _ ⇒ ? ])));
     1906                   >(proj2 … (fetch_statement_inv … EQfetch)) normalize nodelta
     1907                   whd in match statement_semantics; normalize nodelta
     1908                   whd in match (defined ??); whd in match (used ???);
     1909                   @set_member_union1 @set_member_diff [2: @set_member_empty]
     1910                   @(set_member_subset_if … Hcarry1)
     1911                   lapply(included_livebefore_livebeafter_stmt_labels
     1912                                 fix_comp … (init_regs (pc_block (pc … st1))) …
     1913                                 (proj2 ?? (fetch_statement_inv … EQfetch))
     1914                                 (if b then ltrue else lfalse) ?)
     1915                   [1,3: cases b normalize nodelta
     1916                         whd in match stmt_labels; whd in match stmt_explicit_labels;
     1917                         whd in match step_labels; normalize nodelta
     1918                         [1,3: >memb_cons [1,3: @I |*: @memb_hd] |*: >memb_hd @I ] ]
     1919                   whd in match (l_included ???); cases(set_subset ???)
     1920                   normalize nodelta [2: * ] #H @H
     1921                ]   
     1922             |*: % [2,4: [ @if_elim #_ ] assumption] %
     1923                [2,4: whd in match hw_relation; normalize nodelta #R <commute_if
     1924                   whd in match (pc_block ?); >point_of_pc_of_point #HR
     1925                   [ <EQinit_regs @if_elim #Hcarry1 ] whd in match set_regs;
     1926                   normalize nodelta [  >hwreg_retrieve_insensitive_to_set_other]
     1927                   cut(bool_to_Prop(eq_Register R RegisterA) ∨ ¬ (bool_to_Prop (eq_Register R RegisterA)))
     1928                   [1,3,5: @eq_Register_elim #_ //] *
     1929                   [1,3,5: @eq_Register_elim [2,4,6: #_ *] #EQ destruct(EQ) #_ @⊥
     1930                      @(acc_is_dead fix_comp prog … fn1 …
     1931                         (if b then ltrue else lfalse) …
     1932                         (init_regs (pc_block (pc … st1)))) assumption ]
     1933                   @eq_Register_elim [1,3,5: #_ * #H @⊥ @H @I] #no_a #_
     1934                   >hwreg_retrieve_hwregstore_miss [2,4,6: assumption]
     1935                   [1,2: cut(bool_to_Prop(eq_Register R RegisterDPL) ∨ ¬ (bool_to_Prop (eq_Register R RegisterDPL))) 
     1936                      [1,3: @eq_Register_elim #_ //] * @eq_Register_elim
     1937                      [2,3,6,7: #_ * #H @⊥ @H @I] #H
     1938                        [1,3: destruct @⊥
     1939                           @(dpl_is_dead fix_comp prog … fn1 …
     1940                             (init_regs (pc_block (pc … st1)))
     1941                             (if b then ltrue else lfalse)) assumption ] #_
     1942                      >hwreg_retrieve_hwregstore_miss [2,4: assumption] 
     1943                      cut(bool_to_Prop(eq_Register R RegisterDPH) ∨ ¬ (bool_to_Prop (eq_Register R RegisterDPH))) 
     1944                      [1,3: @eq_Register_elim #_ //] * @eq_Register_elim
     1945                      [2,3,6,7: #_ * #H @⊥ @H @I] #H1
     1946                      [1,3: destruct @⊥
     1947                           @(dph_is_dead fix_comp prog … fn1 …
     1948                             (init_regs (pc_block (pc … st1)))
     1949                             (if b then ltrue else lfalse)) assumption ] #_
     1950                      >hwreg_retrieve_hwregstore_miss [2,4: assumption] ]
     1951                @(Hhw_reg R)
     1952                change with (bool_to_Prop (set_member ????))
     1953                whd in match (livebefore ?????);
     1954                change with (stmt_at ??? (point_of_pc ERTL_semantics ?)) in
     1955                          ⊢ (?(????(???match % with [_ ⇒ ? | _ ⇒ ? ])));
     1956                >(proj2 … (fetch_statement_inv … EQfetch)) normalize nodelta
     1957                whd in match statement_semantics; normalize nodelta
     1958                whd in match (defined ??); whd in match (used ???);
     1959                @set_member_union1 @set_member_diff [2,4,6: @set_member_empty]
     1960                @(set_member_subset_if … HR)
     1961                lapply(included_livebefore_livebeafter_stmt_labels
     1962                                 fix_comp … (init_regs (pc_block (pc … st1))) …
     1963                                 (proj2 ?? (fetch_statement_inv … EQfetch))
     1964                                 (if b then ltrue else lfalse) ?)
     1965                 [1,3,5: cases b normalize nodelta
     1966                         whd in match stmt_labels; whd in match stmt_explicit_labels;
     1967                         whd in match step_labels; normalize nodelta
     1968                         [1,3,5: >memb_cons [1,3,5: @I |*: @memb_hd] |*: >memb_hd @I ] ]
     1969                   whd in match (l_included ???); cases(set_subset ???)
     1970                   normalize nodelta [2,4,6: * ] #H @H
     1971              |*: % [1,3: [ @if_elim #_] assumption] cases daemon (*TODO*)
     1972              ]     
     1973             ]
     1974           ]
     1975         |*: %{it} %{(refl …)} %{bv1} %
     1976            [1,3: whd in ⊢ (??%?); whd in match set_regs; normalize nodelta
     1977              [2: @if_elim #_ [ >hwreg_retrieve_insensitive_to_set_other ] ]
     1978              >hwreg_retrieve_hwregstore_hit %]
     1979            cases(bool_of_beval_sigma_commute fix_comp colour prog init_regs f_lbls
     1980                    f_regs … bv1 (refl …) … EQb) #b1 * #H #EQ destruct assumption
     1981        ]
     1982      ]
     1983   |*:
     1984   ]
     1985qed.
     1986
     1987
     1988lemma gen_state_rel_insensitive_to_dead_reg :
     1989 ∀prog,stacksize,init,color_fun,live_fun.
     1990 ∀init_regs : block → list register.∀f_lbls,f_regs. ∀pc.
     1991 ∀f.∀fn : joint_closed_internal_function ? (prog_names … prog).
     1992 fetch_internal_function … (joint_globalenv ERTL_semantics prog stacksize)
     1993 (pc_block pc) = return 〈f,fn〉 →
     1994 ∀st1 : state ERTL_state.∀st2.
     1995 ∀psd_regs,hdw_regs.
     1996 ∀r,bv. ¬ live_fun fn (init_regs (pc_block pc)) (point_of_pc ERTL_semantics pc) (inl ? ? r) →
     1997 gen_state_rel prog stacksize init color_fun live_fun init_regs f_lbls f_regs pc
     1998   (set_regs ERTL_semantics 〈psd_regs,hdw_regs〉 st1) st2 →
     1999 gen_state_rel prog stacksize init color_fun live_fun init_regs f_lbls f_regs pc
     2000  (set_regs ERTL_semantics 〈reg_store r bv psd_regs,hdw_regs〉 st1) st2.
     2001#prog #stacksize #init #color_fun #live_fun #init_regs #f_lbls #f_regs #pc #f #fn
     2002#EQfn #st1 #st2 #psd #hdw #r #bv #r_dead whd in match state_rel; normalize nodelta *
     2003#f1 * #fn1 >EQfn * whd in ⊢ (??%% → ?); #EQ destruct(EQ) inversion (st_frms … st1)
     2004[ #EQframes whd in match (st_frms ??); >EQframes *] #frames #EQframes
     2005whd in match (st_frms ??); >EQframes normalize nodelta ***** whd in match (m ??);
     2006#Hmem #Hframes whd in match (\snd ?); #Hhw_regs whd in match (istack ??); #His
     2007whd in match (carry ??); #Hcarry * #sp * #EQsp whd in match set_regs in ⊢ (% → ?);
     2008normalize nodelta #Hps_regs %{f1} %{fn1} %{EQfn} whd in match (st_frms ??); >EQframes
     2009normalize nodelta %
     2010[ % [2: assumption] % [2: assumption] % [2: assumption] %{Hmem} assumption]
     2011%{sp} %{EQsp} whd #r1 #d1 * #r1_live #EQd1
     2012cut(bool_to_Prop(eq_identifier … r1 r) ∨ bool_to_Prop(¬ (eq_identifier … r1 r)))
     2013[ @eq_identifier_elim #_ [%%|%2%]] @eq_identifier_elim
     2014[ #EQ destruct >r1_live in r_dead; *] #r_no_r1 #_ whd in match reg_retrieve;
     2015  normalize nodelta whd in match set_regs; normalize nodelta whd in match reg_store;
     2016  normalize nodelta >lookup_add_miss [2: assumption] @Hps_regs % assumption
     2017qed.
     2018
     2019lemma sp_ok_on_writable_regs :
     2020∀st : state ERTL_state.∀bv.
     2021∀r.ertl_hdw_writable r →
     2022∀psd.
     2023sp … st = sp … (set_regs ERTL_state 〈psd,hwreg_store r bv (\snd (regs … st))〉 st).
     2024#st #bv #r #Hr #psd whd in ⊢ (??%%); whd in match set_regs; normalize nodelta
     2025>hwreg_retrieve_hwregstore_miss
     2026[ >hwreg_retrieve_hwregstore_miss [%]]
     2027cases r in Hr; whd in match ertl_hdw_writable; normalize nodelta * %
     2028whd in ⊢ (??%% → ?); #EQ destruct
     2029qed.
     2030
     2031lemma mem_insensitive_to_writable_set_regs :
     2032∀prog,stacksize,R,f,st,m1,m2.
     2033∀r.ertl_hdw_writable r →
     2034mem_relation prog stacksize R f st m1 m2 →
     2035∀psd.∀bv.
     2036mem_relation prog stacksize R f
     2037 (set_regs ERTL_state 〈psd,hwreg_store r bv (\snd (regs … st))〉 st) m1 m2.
     2038#prog #stacksize #R #f #st #m1 #m2 #r #Hr whd in match mem_relation;
     2039normalize nodelta #H whd in match ERTL_validate_pointer; normalize nodelta
     2040#psd #bv <(sp_ok_on_writable_regs … Hr … psd) assumption
     2041qed.
     2042 
     2043lemma gen_state_rel_insensitive_to_dead_Reg :
     2044 ∀prog,stacksize,init,color_fun,live_fun.
     2045 ∀init_regs : block → list register.∀f_lbls,f_regs. ∀pc.
     2046 ∀f.∀fn : joint_closed_internal_function ? (prog_names … prog).
     2047 fetch_internal_function … (joint_globalenv ERTL_semantics prog stacksize)
     2048 (pc_block pc) = return 〈f,fn〉 →
     2049 ∀st1 : state ERTL_state.∀st2.
     2050 ∀r,bv. ¬ live_fun fn (init_regs (pc_block pc)) (point_of_pc ERTL_semantics pc) (inr ? ? r) →
     2051 ertl_hdw_writable r →
     2052 gen_state_rel prog stacksize init color_fun live_fun init_regs f_lbls f_regs pc st1 st2 →
     2053 gen_state_rel prog stacksize init color_fun live_fun init_regs f_lbls f_regs pc
     2054  (set_regs ERTL_semantics 〈\fst (regs … st1),hwreg_store r bv (\snd (regs … st1))〉 st1) st2.
     2055#prog #stacksize #init #color_fun #live_fun #init_regs #f_lbls #f_regs #pc #f #fn
     2056#EQfn #st1 #st2 #R #bv #R_dead #R_writable
     2057whd in match gen_state_rel; normalize nodelta * #f1 * #fn1 >EQfn * whd in ⊢ (??%% → ?);
     2058#EQ destruct(EQ) whd in match (st_frms ??); cases(st_frms … st1) [*] #frames
     2059normalize nodelta ***** #Hmem #Hframes #Hhw_reg #His #Hcarry * #sp * #EQsp #Hps_regs
     2060%{f1} %{fn1} %{(refl …)} %
     2061[ % [2: assumption] % [2: assumption] %
     2062  [ % [2: assumption ]
     2063  | %
     2064    [ whd in match hwreg_retrieve_sp; normalize nodelta whd in match set_regs;
     2065      normalize nodelta >hwreg_retrieve_hwregstore_miss
     2066      [ >hwreg_retrieve_hwregstore_miss [ @(proj1 … (Hhw_reg))]]
     2067      % #EQ destruct assumption
     2068    | #r #r_live inversion(color_fun ???) [#r_spill | #r_col ] #EQcol normalize nodelta
     2069      whd in match set_regs; normalize nodelta >hwreg_retrieve_hwregstore_miss
     2070      [1,3: lapply(proj2 ?? (Hhw_reg) r r_live) >EQcol normalize nodelta #H @H]
     2071      % #EQ destruct(EQ) >r_live in R_dead; *
     2072    ]
     2073  ]
     2074| %{sp} %{EQsp} assumption
     2075]
     2076@mem_insensitive_to_writable_set_regs assumption
     2077qed.
     2078
     2079lemma state_rel_insensitive_to_dead_carry :
     2080 ∀prog,stacksize,init,color_fun,live_fun.
     2081 ∀init_regs : block → list register.∀f_lbls,f_regs. ∀pc.
     2082 ∀f.∀fn : joint_closed_internal_function ? (prog_names … prog).
     2083 fetch_internal_function … (joint_globalenv ERTL_semantics prog stacksize)
     2084 (pc_block pc) = return 〈f,fn〉 →
     2085 ∀st1 : state ERTL_state.∀st2.
     2086 ∀c. ¬ live_fun fn (init_regs (pc_block pc)) (point_of_pc ERTL_semantics pc) (inr ? ? RegisterCarry) →
     2087 gen_state_rel prog stacksize init color_fun live_fun init_regs f_lbls f_regs pc st1 st2 →
     2088 gen_state_rel prog stacksize init color_fun live_fun init_regs f_lbls f_regs pc
     2089  (set_carry ERTL_semantics c st1) st2.
     2090#prog #stacksize #init #color_fun #live_fun #init_regs #f_lbls #f_regs #pc #f #fn #EQfn #st1 #st2 #c
     2091#c_dead whd in match gen_state_rel; normalize nodelta * #f1 * #fn1 >EQfn * whd in ⊢ (??%% → ?);
     2092#EQ destruct(EQ) whd in match (st_frms ??); cases(st_frms ??) [*] #frames
     2093normalize nodelta ***** #H1 #H2 #H3 #H4 #H5 #H6 %{f1} %{fn1} %{(refl …)}
     2094% [2: assumption] % [ % [2: assumption] % [2: assumption] % assumption]
     2095#c_live >c_live in c_dead; *
     2096qed.
     2097
     2098
     2099
     2100
     2101
     2102
     2103
     2104
     2105lemma pair_eta : ∀A,B : Type[0].∀p : A × B. p = 〈\fst p,\snd p〉. // qed.
     2106
     2107lemma de_morgan_or : ∀a,b : bool. (notb (a ∨ b)) = true → (notb a) = true ∧ (notb b) = true.
     2108** normalize #EQ destruct %% qed.
     2109
     2110lemma be_op2_carry_preserve : ∀op.
     2111∀by,bv1,bv2,res,by'.be_op2 by op bv1 bv2 = return 〈res,by'〉 →
     2112if match op with [And ⇒ true | Or ⇒ true | Xor ⇒ true | _⇒ false] then
     2113by = by'
     2114else True.
     2115* normalize nodelta #by #bv1 #bv2 #res #by' try(#_ @I)
     2116whd in match be_op2; normalize nodelta
     2117[ #H @('bind_inversion H) -H #bi1 #_ #H @('bind_inversion H) -H #bi2 #_
     2118  whd in ⊢ (??%% → ?); #EQ destruct %
     2119| cases bv1 normalize nodelta
     2120  [|| #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc #p ]
     2121  [1,5,6,7: whd in ⊢ (??%% → ?); #EQ destruct(EQ)]
     2122  cases bv2 normalize nodelta
     2123  [1,2,8,9,15,16: whd in ⊢ (??%% → ?); #EQ destruct %
     2124  |3,10,17: #a1 #a2 #a3  whd in ⊢ (??%% → ?); [1,3: #EQ destruct %]
     2125            @if_elim #_ [2: #EQ destruct] @if_elim #_
     2126            whd in ⊢ (??%% → ?); #EQ destruct %
     2127  |4,11,18: #a1 whd in ⊢ (??%% → ?); [1,2: #EQ destruct %]
     2128            cases(op2 eval false Or by a1)
     2129            #a2 #a3 #EQ destruct %
     2130  |5,12,19: #a1
     2131  |6,13,20: #a1 #a2
     2132  |7,14,21: #a1 #a2
     2133  ]
     2134   whd in ⊢ (??%% → ?); #EQ destruct
     2135| cases bv1 normalize nodelta
     2136  [|| #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc #p ]
     2137  [1,2,3,7: whd in ⊢ (??%% → ?); #EQ destruct(EQ)]
     2138  cases bv2 normalize nodelta
     2139  [1,2,8,9,15,16: whd in ⊢ (??%% → ?); #EQ destruct
     2140  |3,10,17: #a1 #a2 #a3  whd in ⊢ (??%% → ?); #EQ destruct %
     2141  |4,11,18: #a1 whd in ⊢ (??%% → ?); [2,3: #EQ destruct %]
     2142            cases(op2 eval false Xor by a1)
     2143            #a2 #a3 #EQ destruct %
     2144  |5,12,19: #a1 [whd in ⊢ (??%% → ?); #EQ destruct]
     2145            @if_elim #_ whd in ⊢ (??%% → ?); #EQ destruct %
     2146  |6,13,20: #a1 #a2 [whd in ⊢ (??%% → ?); #EQ destruct]
     2147            @if_elim #_ whd in ⊢ (??%% → ?); #EQ destruct %
     2148  |7,14,21: #a1 #a2 whd in ⊢ (??%% → ?); #EQ destruct
     2149  ]
     2150]
     2151qed.
     2152
     2153lemma eq_true_to_bool : ∀b.b=true → bool_to_Prop(b).
     2154#b #EQ >EQ @I qed.
     2155
     2156
     2157lemma state_rel_insensitive_to_eliminable:
     2158 ∀fix_comp: fixpoint_computer.∀build.
     2159 ∀prog: ertl_program.
     2160 let m ≝ (\snd (\fst (ertl_to_ltl fix_comp build prog))) in
     2161 let stackcost≝ lookup_stack_cost … m in
     2162 ∀init_regs : block → list register.∀f_lbls,f_regs.
     2163 let p_in ≝ mk_prog_params ERTL_semantics prog stackcost in
     2164 ∀f. ∀fn : joint_closed_internal_function ??. ∀pc.
     2165 let after ≝ (analyse_liveness fix_comp (prog_names … prog) fn (init_regs (pc_block pc))) in
     2166 let before ≝ livebefore … fn (init_regs (pc_block pc)) after in
     2167 ∀st1 : state ERTL_state.
     2168 let pt ≝ point_of_pc ERTL_semantics pc in
     2169 ∀st1_no_pc. ∀stms: joint_seq ERTL(prog_names … prog). ∀next.
     2170 fetch_internal_function … (joint_globalenv ERTL_semantics prog stackcost) (pc_block pc) =
     2171 return 〈f,fn〉 →
     2172 stmt_at p_in … (joint_if_code p_in … fn) pt = return (sequential … stms next) →
     2173   eval_seq_no_pc ERTL_semantics
     2174   (prog_names … prog) (joint_globalenv ERTL_semantics prog stackcost)
     2175   f stms st1 =return st1_no_pc →
     2176   eliminable_step (globals ? p_in) (after pt) stms →
     2177   ∀st2.
     2178   state_rel fix_comp build prog init_regs f_lbls f_regs pc st1 st2 →
     2179   state_rel fix_comp build prog init_regs f_lbls f_regs
     2180    (pc_of_point ERTL_semantics (pc_block pc) next) st1_no_pc st2.
     2181#fix_comp #build #prog letin p_in ≝ (mk_prog_params ???) #init_regs
     2182#f_lbls #f_regs #f #fn #pc #st1 #st1' #stms #next #EQfn #stmtat #Heval #Helim
     2183#st2 #Rstst2 (* #f1 * #fn1
     2184* >EQfn in ⊢ (??%? → ?); whd in ⊢ (??%% → ?); #EQ destruct(EQ) normalize nodelta
     2185inversion(st_frms ??) [#_ *] #frames #EQframes normalize nodelta ***** #Hmem #Hframes
     2186#Hhwreg #His #Hcarry * #ptr * #EQptr #Hps_reg *)
     2187lapply (eliminable_step_to_eq_livebefore_liveafter … stmtat … (init_regs (pc_block pc)) … Helim)
     2188#EQlivebefore cases stms in stmtat Helim Heval; -stms
     2189[ #str
     2190| #pm (* *** [#r | #R #writable_R] * [ * [ ** [#r1 * | #R1 #readable_R1] | #by ] | ** [#r1 * | #R1 #Hreadable] | #by ] *)
     2191| #A
     2192| #A
     2193| #id #id_spec #arg1 #dpl #dph
     2194| #opaccs #A #B #A1 #B1
     2195| #op1 #A #A1
     2196| #op2 #A #A1 #snd_arg
     2197|
     2198|
     2199| #A #dpl #dph
     2200| #dpl #dph #A
     2201| * #r
     2202]
     2203#stmtat  try(change with (false) in ⊢ (?% → ?); * )
     2204whd in match eliminable_step; normalize nodelta
     2205[ cases pm in stmtat; ** [#r * | #R #R_writable] * [1,3: ** [1,3: #r1 * |*: #R1 #R1_readable ] |*: #by ]
     2206  #stmtat normalize nodelta #Helim whd in match eval_seq_no_pc; normalize nodelta
     2207  whd in match pair_reg_move; normalize nodelta #H @('bind_inversion H) -H
     2208  #rgs whd in ⊢ (??%% → ?); normalize nodelta
     2209  [1,2: inversion (ps_reg_retrieve ??) [2,4: #e normalize nodelta #_ #EQ destruct]
     2210    #bv #EQbv normalize nodelta whd in ⊢ (??%% → ?); ]
     2211  #EQ destruct(EQ) whd in ⊢ (??%% → ?); #EQ destruct(EQ)
     2212| #Helim whd in match eval_seq_no_pc; normalize nodelta whd in match dpl_store;
     2213  normalize nodelta >m_return_bind whd in ⊢ (??%% → ?); whd in match set_regs;
     2214  normalize nodelta #EQ destruct(EQ)
     2215| #Helim whd in match eval_seq_no_pc; normalize nodelta whd in match acca_arg_retrieve;
     2216  whd in match accb_arg_retrieve; normalize nodelta
     2217  change with (ps_arg_retrieve ??) in match (acca_arg_retrieve_ ?????);
     2218  #H @('bind_inversion H) -H #val1 #EQval1
     2219  change with (ps_arg_retrieve ??) in match (accb_arg_retrieve_ ?????);
     2220  #H @('bind_inversion H) -H #val2 #EQval2 #H @('bind_inversion H) -H
     2221  * #val3 #val4 #EQval34 whd in match acca_store; normalize nodelta
     2222  change with (ps_reg_store ???) in match (acca_store_ ??????); #H @('bind_inversion H)
     2223  -H #st1'' #H @('bind_inversion H) -H #new_rgs whd in ⊢ (??%% → ??%% → ?);
     2224  #EQ1 #EQ2 destruct(EQ1 EQ2) whd in match accb_store; normalize nodelta
     2225  change with (ps_reg_store ???) in match (accb_store_ ??????);
     2226  #H @('bind_inversion H) -H #new_rgs' whd in ⊢ (??%% → ?); #EQ destruct(EQ)
     2227  whd in match set_regs; normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ)
     2228| #Helim whd in match eval_seq_no_pc; normalize nodelta whd in match acca_retrieve;
     2229  normalize nodelta change with (ps_reg_retrieve ??) in match (acca_retrieve_ ?????);
     2230  #H @('bind_inversion H) -H #val1 #EQval1 #H @('bind_inversion H) -H
     2231  #val2 #EQval2 whd in match acca_store; normalize nodelta
     2232  change with (ps_reg_store ???) in match (acca_store_ ??????);
     2233  #H @('bind_inversion H) -H #new_rgs whd in ⊢ (??%% → ??%% → ?);
     2234  #EQ1 #EQ2 destruct(EQ1 EQ2)
     2235| cases op2 in stmtat; #stmtat normalize nodelta #Helim
     2236  whd in match eval_seq_no_pc; normalize nodelta whd in match acca_arg_retrieve;
     2237  normalize nodelta
     2238  change with (ps_arg_retrieve ??) in match (acca_arg_retrieve_ ?????);
     2239  #H @('bind_inversion H) -H #val1 #EQval1 whd in match snd_arg_retrieve;
     2240  normalize nodelta change with (ps_arg_retrieve ??) in match (snd_arg_retrieve_ ?????);
     2241  #H @('bind_inversion H) -H #val2 #EQval2 #H @('bind_inversion H) -H *
     2242  #val3 #by #EQval3 whd in match acca_store; normalize nodelta
     2243  change with (ps_reg_store ???) in match (acca_store_ ??????);
     2244  #H @('bind_inversion H) -H #st'' #H @('bind_inversion H) -H #new_rgs
     2245  whd in ⊢ (??%% → ??%% → ??%% → ?); #EQ1 #EQ2 #EQ3 destruct(EQ1 EQ2 EQ3)
     2246| #Helim whd in match eval_seq_no_pc; normalize nodelta whd in match dph_arg_retrieve;
     2247  whd in match dpl_arg_retrieve; normalize nodelta
     2248  change with (ps_arg_retrieve ??) in match (dpl_arg_retrieve_ ?????);
     2249  change with (ps_arg_retrieve ??) in match (dph_arg_retrieve_ ?????);
     2250  #H @('bind_inversion H) -H #val1 #EQval1 #H @('bind_inversion H) -H
     2251  #val2 #EQval2 #H @('bind_inversion H) -H #ind #EQind
     2252  #H @('bind_inversion H) -H #ok_ind #EQok_ind #H @('bind_inversion H) -H
     2253  #val3 #H lapply(opt_eq_from_res ???? H) -H #EQval3 whd in match acca_store;
     2254  normalize nodelta change with (ps_reg_store ???) in match (acca_store_ ??????);
     2255  #H @('bind_inversion H) -H #new_rgs whd in ⊢ (??%% → ??%% → ?);
     2256  #EQ1 #EQ2 destruct(EQ1 EQ2)
     2257| #Helim whd in match eval_seq_no_pc; normalize nodelta whd in ⊢ (??%% → ?);
     2258  whd in match (stack_sizes ????); inversion (opt_to_res ???) normalize nodelta
     2259  [2: #e #_ #EQ destruct(EQ)] #ssize #H lapply(opt_eq_from_res ???? H) -H
     2260  #EQssize whd in match ps_reg_store_status; normalize nodelta
     2261  #H @('bind_inversion H) -H #new_rgs whd in ⊢ (??%% → ??%% → ?);
     2262  #EQ1 #EQ2 destruct(EQ1 EQ2) 
     2263]
     2264[1,2,3,4,5,6,7,8,9,16,17: change with (set_regs ?? st1) in ⊢ (????????%?);
     2265  [1,3,5,7,8,9,10,11: @(state_rel_insensitive_to_dead_reg … f fn) [1,4,7,10,13,16,19,22: @EQfn]
     2266    [2,4,6,12,14,16: <pair_eta >set_regs_eta
     2267    |8,10: @(state_rel_insensitive_to_dead_reg … f fn) [1,4: @EQfn]
     2268       [2,4: <pair_eta >set_regs_eta]
     2269    ]
     2270  |*: @(state_rel_insensitive_to_dead_Reg … f fn) try @EQfn try @R_writable
     2271  ]
     2272|*: change with (set_regs ?? (set_carry ?? st1)) in ⊢ (????????%?);
     2273     @(state_rel_insensitive_to_dead_reg … f fn) try @EQfn
     2274     [2,4,6,8,10,12: <pair_eta  <set_carry_set_regs_commute
     2275       [4,5,6: lapply(be_op2_carry_preserve … EQval3) normalize nodelta
     2276               #EQ destruct(EQ) >set_regs_eta >set_carry_eta
     2277       |*: @(state_rel_insensitive_to_dead_carry … f fn) try @EQfn
     2278           [2,4,6: >set_regs_eta]
     2279       ]
     2280     ]
     2281]
     2282[9,10,11,12,13,14,15,16,17,18,19,21,23,31,32,33,34,35,36,37,38,39:
     2283  @notb_Prop % change with (bool_to_Prop(set_member ????)) in ⊢ (% → ?);
     2284  #ABS cases(Prop_notb … Helim) #H @H -H
     2285  lapply(included_livebefore_livebeafter_stmt_labels
     2286                                 fix_comp … (init_regs (pc_block pc)) … stmtat next ?)
     2287  [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43:
     2288    whd in match stmt_labels; whd in match stmt_explicit_labels;
     2289    whd in match stmt_implicit_label; normalize nodelta >memb_hd @I ]
     2290  whd in match (l_included ???); @if_elim try( #_ * ) #sb_regs #sb_Regs
     2291  [ @orb_Prop_l
     2292  | @orb_Prop_l @orb_Prop_l
     2293  |
     2294  |
     2295  |
     2296  | @orb_Prop_r
     2297  | @orb_Prop_l @orb_Prop_r
     2298  |
     2299  |
     2300  |
     2301  |
     2302  |
     2303  |
     2304  | @orb_Prop_l
     2305  | @orb_Prop_l
     2306  | @orb_Prop_l
     2307  | @orb_Prop_r
     2308  | @orb_Prop_r
     2309  | @orb_Prop_r
     2310  | @orb_Prop_r
     2311  | @orb_Prop_r
     2312  | @orb_Prop_r
     2313  ]
     2314  @(set_member_subset_if … ABS) >point_of_pc_of_point assumption
     2315|*: lapply Rstst2 whd in match state_rel; normalize nodelta * #f1 * #fn1 >EQfn
     2316  * whd in ⊢ (??%% → ?); #EQ destruct(EQ) cases(st_frms … st1)
     2317  [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33: *] #frames normalize nodelta
     2318  ***** #Hmem #Hframes #Hhw_reg #His #Hcarry * #sp * #EQsp #Hps_regs
     2319  %{f1} %{fn1} %{(refl …)} %
     2320  [2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34: %{sp} %{EQsp}
     2321    #r2 #d2 * change with (bool_to_Prop(set_member ????)) in ⊢ (% → ?);
     2322    >point_of_pc_of_point #r2_live #EQd2 @(Hps_regs r2 d2) % try assumption
     2323    >EQlivebefore change with (bool_to_Prop(set_member ????))
     2324    lapply(included_livebefore_livebeafter_stmt_labels
     2325                                 fix_comp … (init_regs (pc_block pc)) … stmtat next ?)
     2326    [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33:
     2327      whd in match stmt_labels; whd in match stmt_explicit_labels;
     2328      whd in match stmt_implicit_label; normalize nodelta >memb_hd @I ]
     2329      whd in match (l_included ???); @if_elim try( #_ * ) #H1 #H2
     2330      @(set_member_subset_if … r2_live) assumption
     2331  |*: %
     2332    [2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34: >point_of_pc_of_point
     2333      #carry_live @Hcarry >EQlivebefore change with (bool_to_Prop(set_member ????))
     2334      lapply(included_livebefore_livebeafter_stmt_labels
     2335                                 fix_comp … (init_regs (pc_block pc)) … stmtat next ?)
     2336      [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33:
     2337        whd in match stmt_labels; whd in match stmt_explicit_labels;
     2338        whd in match stmt_implicit_label; normalize nodelta >memb_hd @I ]
     2339      whd in match (l_included ???); @if_elim try( #_ * ) #H1 #H2
     2340      @(set_member_subset_if … carry_live) assumption
     2341    |*: % try @His %
     2342      [2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34: >point_of_pc_of_point
     2343        #R #R_live @(Hhw_reg R) >EQlivebefore  change with (bool_to_Prop(set_member ????))
     2344        lapply(included_livebefore_livebeafter_stmt_labels
     2345                                 fix_comp … (init_regs (pc_block pc)) … stmtat next ?)
     2346        [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33:
     2347          whd in match stmt_labels; whd in match stmt_explicit_labels;
     2348          whd in match stmt_implicit_label; normalize nodelta >memb_hd @I ]
     2349        whd in match (l_included ???); @if_elim try( #_ * ) #H1 #H2
     2350        @(set_member_subset_if … R_live) assumption
     2351      |*: % assumption
     2352      ]
     2353    ]
     2354  ]
     2355]
     2356qed.
     2357
     2358lemma notb_idempotent : ∀b.b = notb (notb b).
     2359* % qed.
     2360
    7892361           
    7902362lemma seq_commute :∀fix_comp,colour,prog,init_regs,f_lbls,f_regs.
     
    7932365let n ≝ \snd (ertl_to_ltl fix_comp colour prog) in
    7942366let stacksizes ≝ lookup_stack_cost … m in
    795 let init ≝ (λglobals,fn.«translate_data fix_comp colour globals fn,?») in
     2367let init ≝ translate_data fix_comp colour in
    7962368seq_commutation_statement ERTL_semantics LTL_semantics prog stacksizes
    7972369 init init_regs
    798  f_lbls f_regs (state_rel fix_comp colour prog)
     2370 f_lbls f_regs (state_rel fix_comp colour prog init_regs f_lbls f_regs)
    7992371 (state_pc_rel fix_comp colour prog init_regs f_lbls f_regs).
    800 [2: @hide_prf %]
    801 cases daemon (*TODO*)
    802 qed.
    803 
     2372#fix_comp #colour #prog #init_regs #f_lbls #f_regs #st1 #st1' #st2 #f #fn
     2373#stmt #nxt * #Hbl #EQfetch whd in match eval_state; normalize nodelta
     2374>EQfetch >m_return_bind whd in match eval_statement_no_pc; normalize nodelta
     2375#H @('bind_inversion H) -H #st1'' #EQst1'' whd in match eval_statement_advance;
     2376whd in match next; whd in match set_no_pc; whd in match set_pc; normalize nodelta
     2377whd in ⊢ (??%% → ?); #EQ destruct(EQ) whd in match state_pc_rel; normalize nodelta
     2378** #Rst1st2 #Hpc #Hlp #t_fn #EQt_fn #z1 #z2 #z3 #z4 #z5 #z6 #z7 #z8 whd #Hinit_regs
     2379whd @if_elim <Hinit_regs #Helim
     2380[ % [2: normalize nodelta %{(refl …)} %{(st_no_pc … st2)} %{(refl …)}
     2381        @(state_rel_insensitive_to_eliminable …
     2382          (proj1 … (fetch_statement_inv … EQfetch)) …
     2383          (proj2 … (fetch_statement_inv … EQfetch)) … EQst1'' … Helim) assumption |]]
     2384cases stmt in EQfetch EQst1'' Helim; -stmt
     2385[ #c #EQfetch whd in ⊢ (??%% → ?); #EQ destruct(EQ) #_ % [2: %{(refl …)} |]
     2386  %{(st_no_pc … st2)} %{(refl …)} cases Rst1st2 #f1 * #fn1
     2387  >(proj1 … (fetch_statement_inv … EQfetch)) * whd in ⊢ (??%% → ?); #EQ destruct(EQ)
     2388  whd in match state_rel; normalize nodelta cases(st_frms ??) [*] #frames
     2389  normalize nodelta ***** #H1 #H2 #H3 #H4 #H5 * #sp * #EQsp #H6 %{f1} %{fn1}
     2390  >(proj1 … (fetch_statement_inv … EQfetch)) %{(refl …)}
     2391  % [ % [ % [2: assumption] % [% assumption] ]]
     2392  [ #R >point_of_pc_of_point change with nxt in match (point_of_succ ???);
     2393    change with (set_member ????) in ⊢ (?% → ?); #Hlive @(H3 R)
     2394    change with (set_member ????) in ⊢ (?%);
     2395  | >point_of_pc_of_point change with nxt in match (point_of_succ ???);
     2396    change with (set_member ????) in ⊢ (?% → ?); #Hlive @H5
     2397    change with (set_member ????) in ⊢ (?%);
     2398  | %{sp} %{EQsp} #r #d * >point_of_pc_of_point
     2399    change with nxt in match (point_of_succ ???);
     2400    change with (set_member ????) in ⊢ (?% → ?); #Hlive #EQd
     2401    @(H6 r) % [2: assumption] change with (set_member ????) in ⊢ (?%);
     2402  ] 
     2403  whd in match (livebefore ?????);
     2404  change with (stmt_at ??? (point_of_pc ERTL_semantics ?)) in
     2405                           ⊢ (?(????(???match % with [_ ⇒ ? | _ ⇒ ? ])));
     2406  >(proj2 … (fetch_statement_inv … EQfetch)) normalize nodelta
     2407  whd in match statement_semantics; normalize nodelta
     2408  whd in match (defined ??); whd in match (used ???);
     2409  @set_member_union1 @set_member_diff [2,4,6: @set_member_empty]
     2410  @(set_member_subset_if … Hlive)
     2411  lapply(included_livebefore_livebeafter_stmt_labels fix_comp …
     2412         (init_regs (pc_block (pc … st1))) …
     2413         (proj2 ?? (fetch_statement_inv … EQfetch)) nxt ?)
     2414  [1,3,5: whd in match stmt_labels; whd in match stmt_explicit_labels;
     2415     whd in match step_labels; normalize nodelta >memb_hd @I]
     2416  whd in match (l_included ???);
     2417  [1,2: @if_elim [2,4: #_ *] #_]
     2418  cases(set_subset ???) normalize nodelta /2/
     2419| *** [#r_dest * | #R_dest #writeable_R_dest ] *
     2420  [1,3: ** [1,3: #r_src * |*: #R_src #readable_R_src] |*: #by ]  #EQfetch
     2421  whd in match eval_seq_no_pc; whd in match pair_reg_move; normalize nodelta
     2422  whd in match (pair_reg_move_ ?????); normalize nodelta
     2423  [1,2: inversion(ps_reg_retrieve ??) [2,4: #e #_ whd in ⊢ (??%% → ?); #EQ destruct(EQ)]
     2424    #bv whd in match ps_reg_retrieve; normalize nodelta #EQbv normalize nodelta ]
     2425  >m_return_bind whd in ⊢ (??%% → ?); #EQ destruct(EQ) whd in match eliminable_step;
     2426  normalize nodelta <notb_idempotent #dest_live cases daemon
     2427 (*FALSO perche' solo la destinazione e' viva e solo per i vivi vi e' preservazione !!! *)
     2428| #r #EQfetch whd in match eval_seq_no_pc; normalize nodelta
     2429  #H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H * #bv #st1'''
     2430  #EQst1''' whd in ⊢ (??%% → ?); #EQ destruct(EQ) #_ % [2: % [ %] | ]
     2431  cases(pop_ok ERTL_semantics LTL_semantics
     2432    (λbv1,bv2.bv1 = sigma_beval fix_comp colour prog init_regs f_lbls f_regs bv2)
     2433    (state_rel fix_comp colour prog init_regs f_lbls f_regs (pc ERTL_semantics st1)) 
     2434   … EQst1''')
     2435   
     2436   
     2437  inversion (colouring ?? (inl ?? r)) [ #n | #R ] #EQcolouring
     2438 
     2439
     2440 
    8042441lemma return_commute :∀fix_comp,colour,prog,init_regs,f_lbls,f_regs.
    8052442let p_out ≝ (\fst (\fst (ertl_to_ltl fix_comp colour prog))) in
  • src/ERTL/ERTL_semantics.ma

    r3265 r3371  
    3737record ERTL_frame : Type[0] ≝
    3838{ psd_reg_env : register_env beval
    39 ; funct_block : Σb:block.block_region b=Code
    40 ; fr_sp : xpointer (* just for correctness *)
     39; funct_pc : program_counter
     40; funct_sp : xpointer (* just for correctness *)
    4141}.
    4242
     
    6767  ! ss ← opt_to_res ? [MSG BadFunction; CTX … curr_id ] (stack_sizes … ge curr_id) ;
    6868  let o' ≝ off sp in
    69   if Zltb o' 0 ∨
    70     (Zleb (get_joint_if_local_stacksize … ge f) o' ∧
     69  if (Zleb (get_joint_if_local_stacksize … ge f) o' ∧
    7170     Zltb o' (minus ss (get_joint_if_params_stacksize … ge f))) ∨
    7271    Zleb ss o' then
     
    7574    ! frms ← opt_to_res ? (msg FrameErrorOnPop) (st_frms ? st) ;
    7675    m_fold ??? (λfr.λ_.
    77       ! 〈ign, f〉 ← fetch_internal_function … ge (funct_block fr) ;
    78       let o' ≝ off (fr_sp fr) in
    79       if Zltb o' 0 ∨
    80         (Zleb (get_joint_if_local_stacksize … ge f) o' ∧
    81          Zltb o' (minus ss (get_joint_if_params_stacksize … ge f))) ∨
    82         Zleb ss o' then
     76      ! 〈ign, f〉 ← fetch_internal_function … ge (pc_block (funct_pc fr)) ;
     77      let o' ≝ off (funct_sp fr) in
     78      if Zleb (get_joint_if_local_stacksize … ge f) o' ∧
     79         Zltb o' (minus ss (get_joint_if_params_stacksize … ge f)) then
    8380        Error … (msg BadPointer)
    8481      else return it) frms it
     
    113110  return
    114111  (set_frms ERTL_state
    115   ((mk_ERTL_frame (\fst (regs ERTL_state st')) (pc_block (pc ? st)) sp) :: frms)
     112  ((mk_ERTL_frame (\fst (regs ERTL_state st')) (pc ? st) sp) :: frms)
    116113    (set_regs ERTL_state 〈empty_map …,\snd (regs … st')〉 st')).
    117114
     
    128125       (set_frms ERTL_state tl st) in
    129126    ! 〈st'', pc〉 ← pop_ra … st' ;
    130     if eq_block (funct_block hd) (pc_block pc) then
     127    if eq_program_counter (funct_pc hd) pc then
    131128      ! sp ← sp … st'' ;
    132       ! framesize ← opt_to_res (msg FunctionNotFound) (stack_sizes … ge id);
     129      ! framesize ← opt_to_res ? (msg FunctionNotFound) (stack_sizes … ge id);
    133130      let framesize : Byte ≝ bitvector_of_nat 8 framesize in
    134131      let newsp ≝ shift_pointer … sp framesize in
    135       OK … 〈set_sp … newsp st'', pc〉
     132      let cs_regs : hw_register_env ≝
     133        foldl ?? (λregs,r.hwreg_store r BVundef regs) (\snd (regs …st''))
     134          (filter ? (λr.all … (λx.¬ eq_Register r x) RegisterRets)  RegisterCallerSaved)
     135       in
     136      OK … 〈set_sp ? newsp (set_regs ERTL_state 〈\fst (regs … st''),cs_regs〉
     137                            (set_carry ? BBundef st'')), pc〉
    136138    else Error ? [MSG BlockInFramesCorrupted]
    137139 ].
     
    159161  return set_regs ERTL_state env' st.
    160162
     163include alias "arithmetics/nat.ma".
    161164
    162165definition ertl_setup_call : ℕ → state ERTL_state → res (state ERTL_state) ≝
    163166λframesize,st.
    164167  ! sp ← sp … st ;
    165   let framesize : Byte ≝ bitvector_of_nat 8 framesize in
    166   let newsp ≝ neg_shift_pointer … sp framesize in
    167   return set_sp … newsp st.
     168  if leb (S (framesize + (stack_usage … st))) (2^16) then
     169   let framesize : Byte ≝ bitvector_of_nat 8 framesize in
     170   let newsp ≝ neg_shift_pointer … sp framesize in
     171   return set_sp … newsp st
     172  else
     173   Error … [MSG StackOverflow].
    168174@hide_prf whd in match newsp; cases sp #ptr #EQ <EQ % qed.
    169175 
  • src/ERTL/MoveCorrectness.ma

    r3253 r3371  
    2222match d with
    2323[ decision_spill n ⇒
     24  let 〈off_h, off_l〉 ≝ (vsplit … 8 8 (bitvector_of_nat 16 (localss + n)) : Byte × Byte) in
    2425  ! addrl ← hw_reg_retrieve (regs … st) RegisterSPL;
    2526  ! addrh ← hw_reg_retrieve (regs … st) RegisterSPH;
    2627  ! 〈newaddrl,new_carry〉 ←
    27      be_op2 (carry … st) Add (BVByte (bitvector_of_nat 8 (localss + n))) addrl;
    28   ! 〈newaddrh,new_carry'〉← be_op2 new_carry Addc zero_byte addrh;
     28     be_op2 (carry … st) Add (BVByte off_l) addrl;
     29  ! 〈newaddrh,new_carry'〉← be_op2 new_carry Addc (BVByte off_h) addrh;
    2930  ! ptr ← pointer_of_address 〈newaddrl,newaddrh〉;
    3031  ! new_mem ← opt_to_res ? [MSG FailedStore] (bestorev (m … st) ptr bv);
     
    4647    return 〈hwreg_retrieve (regs … st) r,st〉
    4748| arg_decision_spill n ⇒
     49  let 〈off_h, off_l〉 ≝ (vsplit … 8 8 (bitvector_of_nat 16 (localss + n)) : Byte × Byte) in
    4850  ! addrl ← hw_reg_retrieve (regs … st) RegisterSPL;
    4951  ! addrh ← hw_reg_retrieve (regs … st) RegisterSPH;
    5052  ! 〈newaddrl,new_carry〉 ←
    51      be_op2 (carry … st) Add (BVByte (bitvector_of_nat 8 (localss + n))) addrl;
    52   ! 〈newaddrh,new_carry'〉← be_op2 new_carry Addc zero_byte addrh;
     53     be_op2 (carry … st) Add (BVByte off_l) addrl;
     54  ! 〈newaddrh,new_carry'〉← be_op2 new_carry Addc (BVByte off_h) addrh;
    5355  ! ptr ← pointer_of_address 〈newaddrl,newaddrh〉;
    5456  ! bv ← opt_to_res ? [MSG FailedLoad] (beloadv (m … st) ptr);
     
    165167  whd in match repeat_eval_seq_no_pc; normalize nodelta
    166168  whd in match preserve_carry_bit; normalize nodelta cases cl -cl
    167   normalize nodelta whd in match (m_fold ??????) in ⊢ (??%?? → ?);
     169  normalize nodelta @pair_elim #off_h #off_l #EQoff_hl
     170  whd in match (m_fold ??????) in ⊢ (??%?? → ?);
    168171  inversion (eval_seq_no_pc ??????) [2,4: #e #_ normalize nodelta #EQ destruct(EQ)]
    169172  #st'' whd in match set_regs; whd in match eval_seq_no_pc in ⊢ (% → ?);
     
    207210  ]
    208211  >hwreg_retrieve_hwregstore_hit in ⊢ (??(?(????%))?? → ?); #EQptr normalize nodelta
    209   #H @('bind_inversion H) -H #bv #H lapply(opt_eq_from_res ???? H) -H #EQbv
     212  >m_return_bind #H @('bind_inversion H) -H
     213  #bv #H lapply(opt_eq_from_res ???? H) -H #EQbv
    210214  whd in match acca_store; normalize nodelta whd in match (acca_store_ ??????);
    211215  >(hwreg_store_commute RegisterDPH RegisterA) [2,4: normalize % #EQ destruct]
    212216  >hwreg_store_idempotent >m_return_bind whd in match set_regs; normalize nodelta
    213   whd in ⊢ (??%% → ?); #EQ destruct(EQ) whd in match (m_fold ??????) in ⊢ (??%?? → ?); whd in match set_regs;
    214   normalize nodelta inversion (eval_seq_no_pc ??????)
     217  whd in ⊢ (??%% → ?); #EQ destruct(EQ) whd in match set_dp_by_offset; normalize nodelta
     218  @pair_elim #off_h_d #off_l_d #EQoff_hld whd in match (m_fold ??????) in ⊢ (??%?? → ?); whd in match set_regs;
     219  normalize nodelta  inversion (eval_seq_no_pc ??????)
    215220  [2,4: #e #_ normalize nodelta #EQ destruct(EQ)] #st'' >hwreg_retrieve_hwregstore_hit
    216221  >(hwreg_store_commute RegisterST1 RegisterA) [2,4: normalize % #EQ destruct]
     
    280285      #EQptr1 normalize nodelta whd in match acca_arg_retrieve; normalize nodelta
    281286      whd in match (acca_arg_retrieve_ ?????); >hwreg_retrieve_hwregstore_hit
    282       >m_return_bind #H @('bind_inversion H) -H #m1 #H lapply(opt_eq_from_res ???? H)
     287      >m_return_bind >m_return_bind #H @('bind_inversion H) -H #m1 #H lapply(opt_eq_from_res ???? H)
    283288      -H #EQm1 whd in match set_m; normalize nodelta whd in ⊢ (??%% → ?);
    284289      #EQ destruct(EQ) whd in match (m_fold ??????) in ⊢ (??%?? → ?);
     
    288293        whd in match set_carry; normalize nodelta ]
    289294      #EQ destruct(EQ) @sym_eq whd in match read_arg_decision; normalize nodelta
     295      >EQoff_hl normalize nodelta
    290296      >m_return_bind >m_return_bind >EQx1x2 >m_return_bind >EQy1y2
    291297      >m_return_bind >EQptr >m_return_bind >EQbv >m_return_bind
    292298      whd in match set_regs; whd in match write_decision; normalize nodelta
     299      >EQoff_hld normalize nodelta
    293300      whd in match hw_reg_retrieve; normalize nodelta
    294301      >hwreg_retrieve_hwregstore_miss [2,4: normalize % #EQ destruct]
     
    369376      ]
    370377      whd in match set_stack_not_a; whd in match set_dp_by_offset;
    371       whd in match repeat_eval_seq_no_pc; normalize nodelta
     378      whd in match repeat_eval_seq_no_pc; normalize nodelta whd in match get_stack;
     379      normalize nodelta whd in match set_dp_by_offset; normalize  nodelta
     380      @pair_elim #off_hs #off_ls #EQoff_hls
    372381      whd in match (m_fold ??????) in ⊢ (??%?? → ?);
    373382      inversion (eval_seq_no_pc ??????) [2,4,6,8: #e #_ normalize nodelta #EQ destruct]
     
    433442      ]
    434443      #EQptr normalize nodelta whd in match acca_arg_retrieve; normalize nodelta
    435       whd in match (acca_arg_retrieve_ ?????);
     444      whd in match (acca_arg_retrieve_ ?????); >m_return_bind
    436445       #H @('bind_inversion H) -H  #m1 #H lapply(opt_eq_from_res ???? H) -H #EQm1
    437446       whd in match acca_store; normalize nodelta whd in match (acca_store_ ??????);
  • src/ERTL/liveness.ma

    r3263 r3371  
    7878      (* Potentially destroys all caller-save hardware registers. *)
    7979      ]
    80     | CALL _ _ _ ⇒ 〈set_empty …, set_from_list … RegisterCallerSaved
     80    | CALL _ _ _ ⇒ 〈set_empty …, set_from_list … (RegisterCallerSaved @ [RegisterCarry])
    8181    | COND r lbl_true ⇒ rl_bottom
    8282    | COST_LABEL clabel ⇒ rl_bottom
  • src/RTL/RTL_semantics.ma

    r3265 r3371  
    229229      (λst,reg_val.rtl_reg_store (\fst reg_val) (\snd reg_val) st)
    230230      st reg_vals in
    231     return 〈st, pc〉
     231    return 〈set_carry ? BBundef st, pc〉
    232232  ].
    233233
     
    255255      (λst,reg_val.rtl_reg_store (\fst reg_val) (\snd reg_val) st)
    256256      st reg_vals in
    257     return 〈st, pc〉
     257    return 〈set_carry ? BBundef st, pc〉
    258258  ].
    259259
  • src/joint/StatusSimulationHelper.ma

    r3154 r3371  
    181181* #l1 * #mid ** #EQmid #EQl1 whd in ⊢ (% → ?); #EQfin
    182182cases(bind_new_bind_new_instantiates' … Hregs
    183   (bind_new_bind_new_instantiates' … Hdata (goto_commutation … good …
    184        EQfetch Rst1st2 …)))
    185 [2: % assumption
    186 |4: <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in ⊢ (??%?); assumption
    187 |3:
     183  ((bind_new_bind_new_instantiates' … Hdata (goto_commutation … good …
     184       EQfetch Rst1st2 …) ? )))
     185[3: % assumption
     186|5: <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in ⊢ (??%?); assumption
     187|4:
     188|2: @sym_eq @(bind_new_bind_new_instantiates' … Hdata (pi2 ?? (init ? fn)))
    188189]
    189190#st2_fin ** #EQst2_fin #EQ destruct(EQ) #Hfin_rel
     
    332333    #H cases(H EQint_fn1) -H #data1 * #t_fn1 ** #EQt_fn1 #Hregs1 #good1
    333334    cases(bind_new_bind_new_instantiates' … Hregs
    334     (bind_new_bind_new_instantiates' ?????? Hdata
     335    ((bind_new_bind_new_instantiates' ?????? Hdata
    335336     (tailcall_commutation ?????????? good ???????? EQfetch ? EQbl … EQint_fn1 …
    336        EQssize_f … EQssize_f1 … EQst1_setup … Rst1st2 … EQt_fn1))) [2: % assumption]
     337       EQssize_f … EQssize_f1 … EQst1_setup … Rst1st2 … EQt_fn1)) ?))
     338    [3: % assumption
     339    |2: @sym_eq @(bind_new_bind_new_instantiates' … Hdata (pi2 ?? (init ? fn)))
     340    ]
    337341    #has_tail' * #id' * #arg' * #EQ destruct(EQ) * #st2_pre ** #EQst2_pre #EQt_bl
    338342    * #st2_after * #EQst2_after #H cases(bind_new_bind_new_instantiates' … Hregs1 H)
    339     -H #st2' * #EQst2' #fin_sem_rel
     343    -H [2: @sym_eq
     344           @(bind_new_bind_new_instantiates' … Hregs1 (pi2 ?? (init ? fn1)))]
     345    #st2' * #EQst2' #fin_sem_rel
    340346|2: whd in match fetch_internal_function; normalize nodelta >EQfn1 %
    341347|
     
    366372  whd in match fetch_statement; normalize nodelta >EQt_fn >m_return_bind
    367373  >point_of_pc_of_point >EQmid % ]
    368 cases good1 -good1 #_ #_ #_ #_ #_ #_ #_ #_ #_ cases(entry_is_cost … (pi2 ?? fn1))
     374cases good1 -good1 #_ #_ #_ #_ #_ #_ #_ #_ #_ #_ #_ cases(entry_is_cost … (pi2 ?? fn1))
    369375#nxt1 * #c #EQin #H lapply(H … EQin) -H normalize nodelta >(f_step_on_cost … data1)
    370376* #st_bl @eq_identifier_elim [2: * #H @⊥ @H % #_ ] #_
     
    582588]
    583589#EQ destruct(EQ) #n_costed
    584 lapply(b_graph_transform_program_fetch_statement … goodR (pc … st1) f fn ?)
    585 [2,4: @eqZb_elim [1,3: #ABS @⊥ >ABS in Hbl; #H @H %] #_ normalize nodelta
    586       #H cases(H EQfetch) -H |*:]
     590lapply(b_graph_transform_program_fetch_internal_function … goodR (pc_block (pc … st1)) f fn)
     591@eqZb_elim [1,3: #ABS @⊥ >ABS in Hbl; #H @H %] #_ normalize nodelta #H
     592cases(H (proj1 … (fetch_statement_inv … EQfetch))) -H
    587593#init_data * #t_fn1 **  >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch)
    588 #EQt_fn1 whd in ⊢ (% → ?); #Hinit normalize nodelta
    589 *** #blp #blm #bls * whd in ⊢ (% → ?); @if_elim
     594#EQt_fn1 #Hinit * #_ #_ #_ #_ #_ #_ #_ #_ #_ #_ #_ #H
     595lapply(H ?? (proj2 … (fetch_statement_inv … EQfetch))) -H normalize nodelta
     596 whd in ⊢ (% → ?);
     597*** #blp #blm #bls * @if_elim
    590598[1,3: @eq_identifier_elim [2,4: #_ cases(not_emptyb ??) *]
    591       whd in match point_of_pc; normalize nodelta whd in match (point_of_offset ??);
    592       #ABS #_ lapply(fetch_statement_inv … EQfetch) * #_
    593       >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch)
    594       whd in match point_of_pc; normalize nodelta whd in match (point_of_offset ??);
    595       <ABS cases(entry_is_cost … (pi2 ?? fn)) #nxt1 * #c #EQ >EQ #EQ1 destruct(EQ1)
     599      #ABS #_ lapply(fetch_statement_inv … EQfetch) * #_ <ABS
     600      cases(entry_is_cost … (pi2 ?? fn)) #nxt1 * #c #EQ >EQ #EQ1 destruct(EQ1)
    596601]
    597602#_ <(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) #EQbl whd in ⊢ (% → ?); *
    598603#l1 * #mid1 * #mid2 * #l2 *** #EQmid1 whd in ⊢ (% → ?); #seq_pre_l whd in ⊢ (% → ?); * #nxt1
    599604* #EQmid change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ)
    600 cases(bind_new_bind_new_instantiates' … EQbl (bind_new_bind_new_instantiates' … Hinit
    601                (cond_commutation … goodR … EQfetch EQbv EQbool Rst1st2 t_fn1 EQt_fn1)))
    602 [2,4: % assumption]
     605cases(bind_new_bind_new_instantiates' … EQbl ((bind_new_bind_new_instantiates' … Hinit
     606               (cond_commutation … goodR … EQfetch EQbv EQbool Rst1st2 t_fn1 EQt_fn1)) ?))
     607[2,5: @sym_eq >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch)
     608      @(bind_new_bind_new_instantiates' … Hinit (pi2 ?? (init ? fn)))
     609|3,6: % assumption
     610]
    603611#EQ destruct(EQ) #APP whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2)
    604612cases(APP … EQmid) -APP #st_pre_mid_no_pc * #EQst_pre_mid_no_pc *
    605613normalize nodelta
    606 #Hsem * #a' * #EQt_cond * #bv' * #EQbv' #rel_v_v'
     614#Hsem * #a' * #EQt_cond * #bv' * #EQbv' #rel_v_v' #_
    607615[ %{(mk_state_pc ? st_pre_mid_no_pc (pc_of_point P_in (pc_block (pc … st1)) ltrue)
    608616     (last_pop … st2))}
     
    775783#_ <(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) #EQbl
    776784>(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) #SBiC
    777 cases(bind_new_bind_new_instantiates' … EQbl (bind_new_bind_new_instantiates' … Hinit
    778                (seq_commutation … goodR … EQfetch EQeval Rst1st2 t_fn EQt_fn)))
    779                [2: % assumption]
     785cases(bind_new_bind_new_instantiates' … EQbl ((bind_new_bind_new_instantiates' … Hinit
     786               (seq_commutation … goodR … EQfetch EQeval Rst1st2 t_fn EQt_fn)) ? ))
     787[2: @sym_eq >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) 
     788    @(bind_new_bind_new_instantiates' … Hinit (pi2 ?? (init ? fn)))
     789|3: % assumption
     790]
    780791#l * #EQ destruct(EQ) * #st2_fin_no_pc * #EQst2_fin_no_pc #Rsem
    781792%{(mk_state_pc ? st2_fin_no_pc (pc_of_point P_out (pc_block (pc … st2)) nxt) (last_pop … st2))}
     
    10641075cases(next_of_call_pc_inv … EQnext_of_call) #f1 * #fn1 * #id * #args * #dest #EQcall
    10651076<(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in Hregs; #Hregs
    1066 cases(bind_new_bind_new_instantiates' … Hregs (bind_new_bind_new_instantiates' … Hinit
     1077cases(bind_new_bind_new_instantiates' … Hregs ((bind_new_bind_new_instantiates' … Hinit
    10671078 (return_commutation ?????????? good … Hbl EQfetch … EQssize … EQpop … EQcall …
    1068    Rst1st2 t_fn EQt_fn))) #EQ destruct(EQ) * #st_fin * #EQst_fin * #t_st_pop * #t_pc_pop
     1079   Rst1st2 t_fn EQt_fn)) ? ))
     1080[2: @sym_eq >(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch)
     1081    @(bind_new_bind_new_instantiates' … Hinit (pi2 ?? (init ? fn))) ] 
     1082#EQ destruct(EQ) * #st_fin * #EQst_fin * #t_st_pop * #t_pc_pop
    10691083** #EQt_pop #EQt_pc_pop @eqZb_elim #Hbl_pcpop normalize nodelta
    10701084[ * #sem_rel #EQt_next
     
    13471361#id' * #args' * #dest' #EQinstr
    13481362cases(bind_new_bind_new_instantiates' … (bind_instantiates_to_instantiate … Hregs)
    1349   (bind_new_bind_new_instantiates' … (bind_instantiates_to_instantiate … EQdata)
     1363  ((bind_new_bind_new_instantiates' … (bind_instantiates_to_instantiate … EQdata)
    13501364 (call_commutation … good … Hbl EQfetch bl EQbl … EQint_fn … EQst1_save … EQssize …
    1351    EQst1_no_pc'' … Rst1st2 … EQt_fn1)) … EQpc' EQt_call EQinstr)
     1365   EQst1_no_pc'' … Rst1st2 … EQt_fn1)) ?) … EQpc' EQt_call EQinstr)
     1366[2: @sym_eq
     1367    @(bind_new_bind_new_instantiates' …
     1368        (bind_instantiates_to_instantiate … EQdata) (pi2 ?? (init ? fn))) ]
    13521369#st2_pre ** #EQst2_pre #EQt_bl * #st2_save * #EQst2_save * #st2_after * #EQst2_after
    13531370#Hprologue
     
    13631380%{(mk_state_pc ? (increment_stack_usage p_out ssize st2_after)
    13641381   (pc_of_point p_out bl (joint_if_entry … t_fn1)) (last_pop … st2))}
    1365 cases(bind_new_bind_new_instantiates' … Hdata1 Hprologue) -Hprologue #st2' * #EQst2'
    1366 #fin_sem_rel cases good1 #_ #_ #_ #_ #_ #_ #_ #_ #_ cases(entry_is_cost … (pi2 ?? fn1))
     1382cases(bind_new_bind_new_instantiates' … Hdata1 Hprologue)
     1383[2: @sym_eq @(bind_new_bind_new_instantiates' … Hdata1 (pi2 ?? (init ? fn1)))] 
     1384-Hprologue #st2' * #EQst2'
     1385#fin_sem_rel cases good1 #_ #_ #_ #_ #_ #_ #_ #_ #_ #_ #_ cases(entry_is_cost … (pi2 ?? fn1))
    13671386#nxt1 * #c #EQcost #H lapply(H … EQcost) -H -good1 normalize nodelta
    13681387>(f_step_on_cost … data1) *** #pre1 #instr1 #post1 @eq_identifier_elim [2: * #H @⊥ @H %]
  • src/joint/StatusSimulationUtils.ma

    r3262 r3371  
    256256  return 〈f,t_fn〉 →
    257257  bind_new_P' ??
    258      (λregs1.λdata.bind_new_P' ??
     258     (λregs1.λdata.
     259     init_regs (pc_block (pc … st1)) = new_regs … data → bind_new_P' ??
    259260      (λregs2.λblp.
    260261       ∃l : list (joint_seq P_out (globals ? (mk_prog_params P_out trans_prog stack_sizes))).
     
    292293     return 〈f,t_fn〉 →
    293294    bind_new_P' ??
    294      (λregs1.λdata.bind_new_P' ??
     295     (λregs1.λdata.
     296      init_regs (pc_block (pc … st1)) = new_regs … data → bind_new_P' ??
    295297     (λregs2.λblp.(\snd blp) = [ ] ∧
    296298        ∀mid.
     
    342344  bind_new_P' ??
    343345     (λregs1.λdata.
    344       bind_new_P' ??
     346      init_regs (pc_block (pc … st1)) = new_regs … data → bind_new_P' ??
    345347      (λregs2.λblp.
    346348       \snd blp = (RETURN …) ∧
     
    426428  bind_new_P' ??
    427429    (λregs1.λdata.
    428      bind_new_P' ??
     430     init_regs (pc_block (pc … st1)) = new_regs … data → bind_new_P' ??
    429431      (λregs2.λblp.
    430432        ∀pc',t_fn,id',arg',dest',nxt1.
     
    448450       bind_new_P' ??
    449451         (λregs11.λdata1.
    450           ∃st2'.
     452          init_regs bl = new_regs … data1 → ∃st2'.
    451453           repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f1
    452454           (added_prologue … data1) (increment_stack_usage P_out n st2_after_call) =
     
    481483  bind_new_P' ??
    482484     (λregs1.λdata.
    483       bind_new_P' ??
     485      init_regs (pc_block (pc … st1)) = new_regs … data → bind_new_P' ??
    484486      (λregs2.λblp.
    485487        ∃st_fin. repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f
     
    523525   bind_new_P' ??
    524526    (λregs1.λdata.
    525      bind_new_P' ??
     527     init_regs (pc_block (pc … st1)) = new_regs … data → bind_new_P' ??
    526528      (λregs2.λblp.
    527529       ∃ has_tail',id',arg'.
     
    537539       bind_new_P' ??
    538540         (λregs11.λdata1.
    539           ∃st2'.
     541          init_regs bl = new_regs … data1 → ∃st2'.
    540542           repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f1
    541543           (added_prologue … data1) (increment_stack_usage P_out ssize_f1 st2_after) =
     
    782784lapply(b_graph_transform_program_fetch_internal_function … good … bl id fn)
    783785@eqZb_elim [ #EQ >EQ in Hbl; #H @⊥ @H %] #_ normalize nodelta #H cases(H EQfn) -H
    784 #data * #t_fn ** #EQt_fn #Hinit * #_ #_ #_ #pp_labs #_ #fresh_lab #_ #_ #_ #H
     786#data * #t_fn ** #EQt_fn #Hinit * #_ #_ #_ #_ #_ #pp_labs #_ #fresh_lab #_ #_ #_ #H
    785787lapply(H … EQstmt) -H normalize nodelta cases stmt in EQstmt; -stmt
    786788[ #j_step #nxt | #fin | * ] #EQstmt normalize nodelta **
     
    984986lapply(b_graph_transform_program_fetch_internal_function … good … (pc_block pc) f fn)
    985987@eqZb_elim [ #EQ >EQ in Hbl; * #H @⊥ @H %] #_ normalize nodelta #H cases(H EQfn) -H
    986 #data * #t_fn ** #EQt_fn #Hinit * #_ #_ #_ #pp_labs #_ #fresh_labs #_ #_ #_ #H
     988#data * #t_fn ** #EQt_fn #Hinit * #_ #_ #_ #_ #_ #pp_labs #_ #fresh_labs #_ #_ #_ #H
    987989lapply(H … EQstmt) -H normalize nodelta #H #_ %{data} >Hinit %{(refl …)}
    988990-EQfetch cases stmt in EQstmt H;
  • src/joint/lineariseProof.ma

    r2808 r3371  
    1818include "joint/semanticsUtils.ma".
    1919include "common/ExtraMonads.ma".
    20 (*
    21 !!!SPOSTATO IN extraGlobalenvs.ma!!!!
    22 
    23 include alias "common/PositiveMap.ma".
    24 
    25 lemma add_functs_functions_miss : ∀F. ∀ge : genv_t F.∀ l.∀ id.
    26 id < (nextfunction ? ge) →
    27 lookup_opt … id (functions ? ge) = None ? →
    28 lookup_opt … id (functions … (add_functs F ge l)) = None ?.
    29 #F #ge #l #id whd in match add_functs; normalize nodelta
    30 elim l -l [ #_ normalize //]
    31 * #id1 #f1 #tl #IND #H #H1 whd in match (foldr ?????);
    32 >lookup_opt_insert_miss [ inversion(lookup_opt ? ? ?) [ #_ %]
    33 #f1 #H3 <(drop_fn_lfn … f1 H3) @(IND H H1)
    34 | cut(nextfunction F ge ≤ nextfunction F (foldr … (add_funct F) ge tl))
    35 [elim tl [normalize //]
    36 #x #tl2 whd in match (foldr ?????) in ⊢ (? → %); #H %2{H} ]
    37 #H2 lapply(transitive_le … H H2) @lt_to_not_eq
    38 qed.
    39 
    40 lemma add_globals_functions_miss : ∀F,V,init. ∀gem : genv_t F × mem.∀ id,l.
    41 lookup_opt … id (functions ? (\fst gem)) = None ? →
    42 lookup_opt … id (functions … (\fst (add_globals F V init gem l))) = None ?.
    43 #F #V #init * #ge #m #id #l lapply ge -ge lapply m -m elim l [ #ge #m #H @H]
    44 ** #x1 #x2 #x3 #tl whd in match add_globals;
    45 normalize nodelta #IND #m #ge #H whd in match (foldl ?????); normalize nodelta
    46 cases(alloc m ? ? x2) #m1 #bl1 normalize nodelta @IND whd in match add_symbol;
    47 normalize nodelta inversion(lookup_opt ? ? ?) [ #_ %]
    48 #f1 #H3 <(drop_fn_lfn … f1 H3) assumption
    49 qed.
    50 
    51  
    52 lemma globalenv_no_minus_one :
    53  ∀F,V,i,p.
    54   find_funct_ptr … (globalenv F V i p) (mk_block Code (-1)) = None ?.
    55 #F #V #i #p
    56 whd in match find_funct_ptr; normalize nodelta
    57 whd in match globalenv;
    58 whd in match globalenv_allocmem; normalize nodelta
    59 @add_globals_functions_miss @add_functs_functions_miss normalize //
    60 qed.
    61 *)
    62 
    63 (* !!!spostato in semantics.ma ed aggiunto un include a extraGlobalenvs.ma!!!
    64 
    65 lemma fetch_internal_function_no_minus_one :
    66   ∀F,V,i,p,bl.
    67   block_id (pi1 … bl) = -1 →
    68   fetch_internal_function … (globalenv (λvars.fundef (F vars)) V i p)
    69     bl = Error … [MSG BadFunction].
    70  #F#V#i#p ** #r #id #EQ1 #EQ2 destruct
    71  whd in match fetch_internal_function;
    72   whd in match fetch_function; normalize nodelta
    73   >globalenv_no_minus_one
    74   cases (symbol_for_block ???) normalize //
    75 qed.
    76 
    77 *)
    78 
    79 (*spostato in ExtraMonads.ma
    80 
    81 lemma bind_option_inversion_star:
    82   ∀A,B: Type[0].∀P : Prop.∀f: option A. ∀g: A → option B. ∀y: B.
    83   (∀x.f = Some … x → g x = Some … y → P) →
    84   (! x ← f ; g x = Some … y) → P.
    85 #A #B #P #f #g #y #H #G elim (option_bind_inverse ????? G) #x * @H qed.
    86 
    87 interpretation "option bind inversion" 'bind_inversion =
    88   (bind_option_inversion_star ???????).
    89 
    90 lemma bind_inversion_star : ∀X,Y.∀P : Prop.
    91 ∀m : res X.∀f : X → res Y.∀v : Y.
    92 (∀x. m = return x → f x = return v → P) →
    93 ! x ← m ; f x = return v → P.
    94 #X #Y #P #m #f #v #H #G
    95 elim (bind_inversion ????? G) #x * @H qed.
    96 
    97 interpretation "res bind inversion" 'bind_inversion =
    98   (bind_inversion_star ???????).
    99 
    100 lemma IO_bind_inversion:
    101   ∀O,I,A,B.∀P : Prop.∀f: IO O I A. ∀g: A → IO O I B. ∀y: B.
    102   (∀x.f = return x → g x = return y → P) →
    103   (! x ← f ; g x = return y) → P.
    104 #O #I #A #B #P #f #g #y cases f normalize
    105 [ #o #f #_ #H destruct
    106 | #a #G #H @(G ? (refl …) H)
    107 | #e #_ #H destruct
    108 ] qed.
    109 
    110 interpretation "IO bind inversion" 'bind_inversion =
    111   (IO_bind_inversion ?????????).
    112 
    113 record MonadFunctRel (M1 : Monad) (M2 : Monad) : Type[1] ≝
    114   { m_frel :6> ∀X,Y.∀P : X → Prop.(∀x.P x → Y) → (M1 X → M2 Y → Prop)
    115   ; mfr_return : ∀X,Y,P,F,x,prf.m_frel X Y P F (return x) (return (F x prf))
    116   ; mfr_bind : ∀X,Y,Z,W,P,Q,F,G,m,n.
    117       m_frel X Y P F m n → ∀f,g.(∀x,prf.m_frel Z W Q G (f x) (g (F x prf))) →
    118                   m_frel ?? Q G (m_bind … m f) (m_bind … n g)
    119   ; m_frel_ext : ∀X,Y,P,F,G.(∀x,prf1,prf2.F x prf1 = G x prf2) → ∀u,v.m_frel X Y P F u v → m_frel X Y P G u v
    120   }.
    121 
    122 *)
    123 
    124 (*definition IO_preserve : ∀O,I.MonadFunctRel (IOMonad O I) (IOMonad O I) ≝
    125   λO,I.mk_MonadFunctRel ??
    126   (λX,Y,F,m,n.∀x.m = return x → n = return F x)
    127   ???.
    128 [ #X #Y #F #x #y whd in ⊢ (??%%→?); #EQ destruct(EQ) %
    129 | #X #Y #Z #W #F #G *
    130   [ #o #f | #u | #e ] #n #H #f #g #K #x
    131   whd in ⊢ (??%%→?); #EQ destruct(EQ)
    132   >(H ? (refl …)) @K @EQ
    133 | #X #Y #P #Q #H #z #w #G #x #EQ >(G … EQ) >H %
    134 ]
    135 qed.*)
    136 
    137 (* spostato in ExtraMonads.ma
    138 definition res_preserve : MonadFunctRel Res Res ≝
    139   mk_MonadFunctRel ??
    140   (λX,Y,P,F,m,n.∀x.m = return x → ∃prf.n = return F x prf)
    141   ???.
    142 [ #X #Y #P #F #x #prf #x' whd in ⊢ (??%%→?); #EQ destruct(EQ) %{prf} %
    143 | #X #Y #Z #W #P #Q #F #G *
    144   [ #u | #e ] #n #H #f #g #K #x
    145   whd in ⊢ (??%%→?); #EQ destruct(EQ)
    146   cases (H ? (refl …)) #prf #L >L @(K ? prf ? EQ)
    147 | #X #Y #P #F #G #H #u #v #K #x #EQ
    148   cases (K … EQ) #prf #EQ' %{prf} >EQ' >H try %
    149 ]
    150 qed.
    151 
    152 definition opt_preserve : MonadFunctRel Option Option ≝
    153   mk_MonadFunctRel ??
    154   (λX,Y,P,F,m,n.∀x.m = return x → ∃prf.n = return F x prf)
    155   ???.
    156 [ #X #Y #P #F #x #prf #x' whd in ⊢ (??%%→?); #EQ destruct(EQ) %{prf} %
    157 | #X #Y #Z #W #P #Q #F #G *
    158   [ | #u ] #n #H #f #g #K #x
    159   whd in ⊢ (??%%→?); #EQ destruct(EQ)
    160   cases (H ? (refl …)) #prf #L >L @(K ? prf ? EQ)
    161 | #X #Y #P #F #G #H #u #v #K #x #EQ
    162   cases (K … EQ) #prf #EQ' %{prf} >EQ' >H try %
    163 ]
    164 qed.
    165 
    166 definition io_preserve : ∀O,I.MonadFunctRel (IOMonad O I) (IOMonad O I) ≝
    167   λO,I.mk_MonadFunctRel ??
    168   (λX,Y,P,F,m,n.∀x.m = return x → ∃prf.n = return F x prf)
    169   ???.
    170 [ #X #Y #P #F #x #prf #x' whd in ⊢ (??%%→?); #EQ destruct(EQ) %{prf} %
    171 | #X #Y #Z #W #P #Q #F #G *
    172   [ #o #f | #u | #e ] #n #H #f #g #K #x
    173   whd in ⊢ (??%%→?); #EQ destruct(EQ)
    174   cases (H ? (refl …)) #prf #L >L @(K ? prf ? EQ)
    175 | #X #Y #P #F #G #H #u #v #K #x #EQ
    176   cases (K … EQ) #prf #EQ' %{prf} >EQ' >H try %
    177 ]
    178 qed.
    179 
    180 definition preserving ≝
    181   λM1,M2.λFR : MonadFunctRel M1 M2.
    182   λX,Y,A,B : Type[0].
    183   λP : X → Prop.
    184   λQ : A → Prop.
    185   λF : ∀x : X.P x → Y.
    186   λG : ∀a : A.Q a → B.
    187   λf : X → M1 A.
    188   λg : Y → M2 B.
    189   ∀x,prf.
    190   FR … G
    191     (f x) (g (F x prf)).
    192 
    193 definition preserving2 ≝
    194   λM1,M2.λFR : MonadFunctRel M1 M2.
    195   λX,Y,Z,W,A,B : Type[0].
    196   λP : X → Prop.
    197   λQ : Y → Prop.
    198   λR : A → Prop.
    199   λF : ∀x : X.P x → Z.
    200   λG : ∀y : Y.Q y → W.
    201   λH : ∀a : A.R a → B.
    202   λf : X → Y → M1 A.
    203   λg : Z → W → M2 B.
    204   ∀x,y,prf1,prf2.
    205   FR … H
    206     (f x y) (g (F x prf1) (G y prf2)).
    207 *)
     20
     21check mk_sem_graph_params
    20822
    20923definition graph_prog_params ≝
    210 λp,p',prog,stack_sizes.
    211 mk_prog_params (mk_sem_graph_params p p') prog stack_sizes.
     24λp,p',pre_main,prog,stack_sizes.
     25mk_prog_params (mk_sem_graph_params p p' pre_main) prog stack_sizes.
     26
     27check mk_sem_graph_params
    21228
    21329definition graph_abstract_status:
    214  ∀p:unserialized_params.
     30 ∀p:uns_params.
    21531  (∀F.sem_unserialized_params p F) →
     32   (∀prog : joint_program (mk_graph_params p).
     33    joint_closed_internal_function (mk_graph_params p) (prog_names … prog)) →
    21634    ∀prog : joint_program (mk_graph_params p).
    21735  (ident → option ℕ) →
    21836     abstract_status
    219  ≝
    220  λp,p',prog,stack_sizes.
    221  joint_abstract_status (graph_prog_params ? p' prog stack_sizes).
     37 ≝ 
     38 λp,p',pre_main,prog,stack_sizes.
     39 joint_abstract_status (graph_prog_params ? p' pre_main prog stack_sizes).
    22240
    22341definition lin_prog_params ≝
    224 λp,p',prog,stack_sizes.
    225 mk_prog_params (mk_sem_lin_params p p') prog stack_sizes.
     42λp,p',pre_main,prog,stack_sizes.
     43mk_prog_params (mk_sem_lin_params p p' pre_main) prog stack_sizes.
    22644
    22745definition lin_abstract_status:
    228  ∀p:unserialized_params.
     46 ∀p:uns_params.
    22947  (∀F.sem_unserialized_params p F) →
     48  (∀prog : joint_program (mk_lin_params p).
     49    joint_closed_internal_function (mk_lin_params p) (prog_names … prog)) →
    23050    ∀prog : joint_program (mk_lin_params p).
    23151  (ident → option ℕ) →
    23252     abstract_status
    23353 ≝
    234  λp,p',prog,stack_sizes.
    235  joint_abstract_status (lin_prog_params ? p' prog stack_sizes).
     54 λp,p',pre_main,prog,stack_sizes.
     55 joint_abstract_status (lin_prog_params ? p' pre_main prog stack_sizes).
    23656
    23757(*
Note: See TracChangeset for help on using the changeset viewer.