Changeset 2991


Ignore:
Timestamp:
Mar 27, 2013, 9:57:13 PM (4 years ago)
Author:
piccolo
Message:

Fixed cond and seq case in StatusSimulationHelper?

Added cost case in StatusSimulationHelper?

Location:
src
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLtoERTLptrOK.ma

    r2943 r2991  
    165165definition state_rel ≝ λprog : ertl_program.λf_lbls.
    166166λf_regs : (block → label → list register).
    167 λbl.λ_:label.λst1,st2.∃f,fn.
     167λbl.λ_ : label.λst1,st2.∃f,fn.
    168168fetch_internal_function ? (globalenv_noinit … prog) bl = return 〈f,fn〉 ∧
    169169let added ≝ added_registers ERTL (prog_var_names … prog) fn (f_regs bl) in
     
    842842       >(fetch_stmt_ok_sigma_pc_ok … EQfetch) in ⊢ (???(match % with [_ ⇒ ? | _ ⇒ ?]));
    843843       >EQfetch' in ⊢ (???(match % with [_ ⇒ ? | _ ⇒ ?])); normalize nodelta
     844       >(fetch_stmt_ok_sigma_state_ok … EQfetch) >EQc_bl >m_return_bind
     845       lapply EQc_bl' whd in match block_of_call; normalize nodelta
    844846       cases daemon (* CSC: The proof used to be %, why did it change? *)
     847                    (* This point will be generalized when the call case
     848                       will be available in StatusSimulationHelper*)
    845849       (*
    846850       XXX
  • src/common/StatusSimulation.ma

    r2870 r2991  
    361361    ] ≝
    362362  match tll1 with
    363   [ tll_base fl1' st1' st1'' tal1 H ⇒ ?
     363  [ tll_base fl1' rst1 rst1' tal1 H ⇒ ?
    364364  ]
    365365and status_simulation_produce_tal S1 S2 R
  • src/joint/StatusSimulationHelper.ma

    r2940 r2991  
    2424
    2525lemma pc_of_label_eq :
    26   ∀p,p'.let pars ≝ mk_sem_graph_params p p' in
     26  ∀pars: sem_graph_params.
    2727  ∀globals,ge,bl,i_fn,lbl.
    28   fetch_internal_function ? ge bl = return i_fn →
     28  fetch_internal_function ? globals ge bl = return i_fn →
    2929  pc_of_label pars globals ge bl lbl =
    3030    OK ? (pc_of_point pars bl lbl).
    31 #p #p' #globals #ge #bl #i_fn #lbl #EQf
     31#p #globals #ge #bl #i_fn #lbl #EQf
    3232whd in match pc_of_label;
    3333normalize nodelta >EQf >m_return_bind %
     
    4646qed.
    4747
     48let rec bind_instantiates B X (b : bind_new B X) (l : list B) on b : (option X) ≝
     49  match b with
     50  [ bret B ⇒
     51    match l with
     52    [ nil ⇒ Some ? B
     53    | _ ⇒ None ?
     54    ]
     55  | bnew f ⇒
     56    match l with
     57    [ nil ⇒ None ?
     58    | cons r l' ⇒
     59      bind_instantiates B X (f r) l'
     60    ]
     61  ].
     62 
     63lemma bind_instantiates_bind_new_instantiates : ∀B,X.∀b : bind_new B X.
     64∀l : list B.∀x : X.
     65bind_instantiates B X b l = Some ? x →
     66bind_new_instantiates B X x b l.
     67#B #X #b elim b
     68[#x1 * [2: #hd #tl] #x whd in ⊢ (??%? → ?); #EQ destruct(EQ) %
     69|#f #IH * [2: #hd #tl] #x whd in ⊢ (??%? → ?); [2: #EQ destruct(EQ)] #H
     70 whd @IH assumption
     71]
     72qed.
     73
     74lemma bind_new_instantiates_bind_instantiates : ∀B,X.∀b : bind_new B X.
     75∀l : list B.∀x : X.
     76bind_new_instantiates B X x b l →
     77bind_instantiates B X b l = Some ? x.
     78#B #X #b elim b
     79[ #x1 * [2: #hd #tl] #x whd in ⊢ (% → ?); [*] #EQ destruct(EQ) %
     80| #f #IH * [2: #hd #tl] #x whd in ⊢ (% → ?); [2: *] #H whd in ⊢ (??%?); @IH @H
     81]
     82qed.
     83
     84
    4885definition joint_state_relation ≝
    49 λP_in,P_out.(Σb:block.block_region b=Code) → label → state P_in → state P_out → Prop.
     86λP_in,P_out.program_counter → state P_in → state P_out → Prop.
    5087
    5188definition joint_state_pc_relation ≝ λP_in,P_out.state_pc P_in → state_pc P_out → Prop.
    5289
    53 definition sigma_map ≝  block → label → option label.
    54 definition lbl_funct ≝  block → label → (list label).
    55 definition regs_funct ≝ block → label → (list register).
    56 
    57 definition get_sigma : ∀p : sem_graph_params.
    58 joint_program p → lbl_funct → sigma_map ≝
    59 λp,prog,f_lbls.λbl,searched.
    60 let globals ≝ prog_var_names … prog in
    61 let ge ≝ globalenv_noinit … prog in
     90definition lbl_funct_type ≝  block → label → (list label).
     91definition regs_funct_type ≝ block → label → (list register).
     92
     93definition preamble_length ≝
     94λP_in : sem_graph_params.λP_out : sem_graph_params.λprog : joint_program P_in.
     95λstack_size : (ident → option ℕ).
     96λinit : ∀globals.joint_closed_internal_function P_in globals
     97         →bound_b_graph_translate_data P_in P_out globals.
     98λinit_regs : block → list register.
     99λf_regs : regs_funct_type.λbl : block.λlbl : label.
    62100! bl ← code_block_of_block bl ;
    63 ! 〈id,fn〉 ← res_to_opt … (fetch_internal_function … ge bl);
    64 !〈res,s〉 ← find ?? (joint_if_code  ?? fn)
    65                 (λlbl.λ_. match split_on_last … (f_lbls bl lbl) with
    66                           [None ⇒ eq_identifier … searched lbl
    67                           |Some x ⇒ eq_identifier … searched (\snd x)
    68                           ]);
     101! 〈id,fn〉 ← res_to_opt … (fetch_internal_function … (prog_var_names … prog)
     102                           (joint_globalenv P_in prog stack_size) bl);
     103! stmt ← stmt_at P_in (prog_var_names … prog) (joint_if_code … fn) lbl;
     104! data ← bind_instantiates ?? (init … fn) (init_regs bl);
     105match stmt with
     106[ sequential step nxt ⇒
     107    ! step_block ← bind_instantiates ?? (f_step … data lbl step) (f_regs bl lbl);
     108    return |\fst (\fst step_block)|
     109| final fin ⇒
     110    ! fin_block ← bind_instantiates ?? (f_fin … data lbl fin) (f_regs bl lbl);
     111    return |\fst fin_block|
     112| FCOND abs _ _ _ ⇒ Ⓧabs
     113].
     114
     115
     116definition sigma_label : ∀p_in,p_out : sem_graph_params.
     117joint_program p_in → (ident → option ℕ) →
     118(∀globals.joint_closed_internal_function p_in globals
     119         →bound_b_graph_translate_data p_in p_out globals) →
     120(block → list register) → lbl_funct_type → regs_funct_type →
     121block → label → option label ≝
     122λp_in,p_out,prog,stack_size,init,init_regs,f_lbls,f_regs,bl,searched.
     123! bl ← code_block_of_block bl ;
     124! 〈id,fn〉 ← res_to_opt … (fetch_internal_function … (prog_var_names … prog)
     125                           (joint_globalenv p_in prog stack_size) bl);
     126! 〈res,s〉 ←
     127 find ?? (joint_if_code ?? fn)
     128  (λlbl.λ_.match preamble_length … prog stack_size init init_regs f_regs bl lbl with
     129             [ None ⇒ false
     130             | Some n ⇒ match nth_opt ? n (lbl::(f_lbls bl lbl)) with
     131                         [ None ⇒ false
     132                         | Some x ⇒ eq_identifier … searched x
     133                         ]
     134             ]);
    69135return res.
    70136
    71 definition sigma_pc_opt :  ∀p_in,p_out : sem_graph_params.
    72 joint_program p_in →  lbl_funct →
     137lemma partial_inj_sigma :
     138∀p_in,p_out,prog,stack_size,init,init_regs.
     139∀f_lbls : lbl_funct_type.∀f_regs,bl,lbl1,lbl2.
     140sigma_label p_in p_out prog stack_size init init_regs f_lbls f_regs bl lbl1 ≠ None ?→
     141sigma_label p_in p_out prog stack_size init init_regs f_lbls f_regs bl lbl1 =
     142sigma_label p_in p_out prog stack_size init init_regs f_lbls f_regs bl lbl2 →
     143lbl1 = lbl2.
     144#p_in #p_out #prog #stack_size #init #init_regs #f_lbls #f_regs #bl #lbl1 #lbl2
     145inversion(sigma_label ????????? lbl1)
     146[ #_ * #H @⊥ @H %]
     147#lbl1' #H @('bind_inversion H) -H #bl' #EQbl'
     148#H @('bind_inversion H) -H * #f #fn #H lapply(res_eq_from_opt ??? H) -H
     149#EQfn #H @('bind_inversion H) -H * #res #stmt #H1 whd in ⊢ (??%? → ?);
     150#EQ destruct(EQ) #_ #H lapply(sym_eq ??? H) -H #H @('bind_inversion H) -H
     151#bl'' >EQbl' #EQ destruct(EQ) >EQfn >m_return_bind #H @('bind_inversion H) -H
     152* #lbl2' #stmt' #H2 whd in ⊢ (??%? → ?); #EQ destruct(EQ)
     153lapply(find_predicate ?????? H1) lapply(find_predicate ?????? H2)
     154cases (preamble_length ?????????) normalize nodelta [*] #n cases(nth_opt ???)
     155normalize nodelta
     156[*] #lbl @eq_identifier_elim [2: #_ *] #EQ destruct(EQ) #_ @eq_identifier_elim
     157[2: #_ *] #EQ destruct(EQ) #_ %
     158qed.
     159
     160definition sigma_pc_opt : 
     161∀p_in,p_out : sem_graph_params.
     162joint_program p_in → (ident → option ℕ) →
     163(∀globals.joint_closed_internal_function p_in globals
     164         →bound_b_graph_translate_data p_in p_out globals) →
     165(block → list register) → lbl_funct_type → regs_funct_type →
    73166program_counter → option program_counter ≝
    74 λp_in,p_out,prog,f_lbls,pc.
    75   let sigma ≝ get_sigma p_in prog f_lbls in
    76   let ertl_ptr_point ≝ point_of_pc p_out pc in
    77   if eqZb       (block_id (pc_block pc)) (-1) then (* check for dummy exit pc *)
    78     return pc
    79   else
    80        ! point ← sigma (pc_block pc) ertl_ptr_point;
    81        return pc_of_point p_in (pc_block pc) point.
     167λp_in,p_out,prog,stack_size,init,init_regs,f_lbls,f_regs,pc.
     168let target_point ≝ point_of_pc p_out pc in
     169if eqZb (block_id (pc_block pc)) (-1) then
     170 return pc
     171else
     172 ! source_point ← sigma_label p_in p_out prog stack_size init init_regs
     173                   f_lbls f_regs (pc_block pc) target_point;
     174 return pc_of_point p_in (pc_block pc) source_point.
     175
     176lemma sigma_stored_pc_inj :
     177∀p_in,p_out,prog,stack_size,init,init_regs,f_lbls,f_regs,pc,pc'.
     178sigma_pc_opt p_in p_out prog stack_size init init_regs f_lbls f_regs pc ≠ None ? →
     179sigma_pc_opt p_in p_out prog stack_size init init_regs f_lbls f_regs pc =
     180sigma_pc_opt p_in p_out prog stack_size init init_regs f_lbls f_regs pc' →
     181pc = pc'.
     182#p_in #p_out #prog #stack_size #init #init_regs #f_lbls #f_regs
     183* #bl1 #p1 * #bl2 #p2
     184inversion(sigma_pc_opt ??????) [#_ * #H @⊥ @H %] #pc1
     185whd in match sigma_pc_opt in ⊢ (% → ?); normalize nodelta
     186@eqZb_elim [2: *] normalize nodelta #Hbl
     187[ #H @('bind_inversion H) -H * #pt1 #EQpt1]
     188whd in ⊢ (??%? → ?); #EQ destruct(EQ)
     189#_ #H lapply(sym_eq ??? H) -H whd in match sigma_pc_opt;
     190normalize nodelta @eqZb_elim [2,4: *] #Hbl1 normalize nodelta
     191[1,2: #H @('bind_inversion H) -H * #pt2 #EQpt2] whd in match pc_of_point;
     192normalize nodelta whd in match (offset_of_point ??);
     193whd in ⊢ (??%% → ?); #EQ destruct(EQ)
     194[2,3: @⊥ [ >Hbl in Hbl1; | >Hbl1 in Hbl;] #H @H % |4: %]
     195whd in match (offset_of_point ??) in EQpt2;
     196<EQpt1 in EQpt2; #H lapply(partial_inj_sigma … (sym_eq ??? H))
     197[ >EQpt1 % #EQ -prog destruct(EQ)] whd in match point_of_pc; normalize nodelta
     198whd in match (point_of_offset ??); whd in match (point_of_offset ??);
     199#EQ -prog destruct(EQ) %
     200qed.
    82201
    83202definition sigma_stored_pc ≝
    84 λp_in,p_out,prog,f_lbls,pc. match sigma_pc_opt p_in p_out prog f_lbls pc with
     203λp_in,p_out,prog,stack_size,init,init_regs,f_lbls,f_regs,pc.
     204match sigma_pc_opt p_in p_out prog stack_size init init_regs f_lbls f_regs pc with
    85205      [None ⇒ null_pc (pc_offset … pc) | Some x ⇒ x].
     206
    86207
    87208record good_state_relation (P_in : sem_graph_params)
     
    90211   (init : ∀globals.joint_closed_internal_function P_in globals
    91212         →bound_b_graph_translate_data P_in P_out globals)
    92    (f_bl_r : block → list register) (f_lbls : lbl_funct) (f_regs : regs_funct)
    93    (good : b_graph_transform_program_props P_in P_out init prog f_bl_r f_lbls f_regs)
     213   (init_regs : block → list register) (f_lbls : lbl_funct_type)
     214   (f_regs : regs_funct_type)
    94215   (st_no_pc_rel : joint_state_relation P_in P_out)
    95216   (st_rel : joint_state_pc_relation P_in P_out) : Prop ≝
    96 { fetch_ok_sigma_state_ok :
     217{ good_translation :> b_graph_transform_program_props P_in P_out stack_sizes init
     218                     prog init_regs f_lbls f_regs
     219; fetch_ok_sigma_state_ok :
    97220   ∀st1,st2,f,fn. st_rel st1 st2 →
    98     fetch_internal_function ? (globalenv_noinit … prog)
    99      (pc_block (pc … st1))  = return 〈f,fn〉 →
    100      st_no_pc_rel (pc_block(pc … st1))
    101      (point_of_pc P_in (pc … st1))
    102      (st_no_pc … st1) (st_no_pc … st2)
     221    fetch_internal_function … (prog_var_names … prog)
     222     (joint_globalenv P_in prog stack_sizes) (pc_block (pc … st1)) 
     223     = return 〈f,fn〉 →
     224     st_no_pc_rel (pc … st1) (st_no_pc … st1) (st_no_pc … st2)
    103225; fetch_ok_pc_ok :
    104226  ∀st1,st2,f,fn.st_rel st1 st2 →
    105    fetch_internal_function ? (globalenv_noinit … prog)
    106   (pc_block (pc … st1))  = return 〈f,fn〉 →
     227   fetch_internal_function … (prog_var_names … prog)
     228     (joint_globalenv P_in prog stack_sizes) (pc_block (pc … st1)) 
     229     = return 〈f,fn〉 →
    107230   pc … st1 = pc … st2
    108231; fetch_ok_sigma_last_pop_ok :
    109232  ∀st1,st2,f,fn.st_rel st1 st2 →
    110    fetch_internal_function ? (globalenv_noinit … prog)
    111     (pc_block (pc … st1))  = return 〈f,fn〉 →
    112    (last_pop … st1) = sigma_stored_pc P_in P_out prog f_lbls (last_pop … st2)
     233   fetch_internal_function … (prog_var_names … prog)
     234     (joint_globalenv P_in prog stack_sizes) (pc_block (pc … st1)) 
     235     = return 〈f,fn〉 →
     236   (last_pop … st1) = sigma_stored_pc P_in P_out prog stack_sizes init init_regs
     237                       f_lbls f_regs (last_pop … st2)
    113238; st_rel_def :
    114239  ∀st1,st2,pc,lp1,lp2,f,fn.
    115   fetch_internal_function ? (globalenv_noinit … prog)
    116    (pc_block pc) = return 〈f,fn〉 →
    117    st_no_pc_rel (pc_block pc) (point_of_pc P_in pc) st1 st2 →
    118    lp1 = sigma_stored_pc P_in P_out prog f_lbls lp2 →
     240  fetch_internal_function … (prog_var_names … prog)
     241     (joint_globalenv P_in prog stack_sizes) (pc_block pc) = return 〈f,fn〉 →
     242   st_no_pc_rel pc st1 st2 →
     243   lp1 = sigma_stored_pc P_in P_out prog stack_sizes init init_regs
     244          f_lbls f_regs lp2 →
    119245  st_rel (mk_state_pc ? st1 pc lp1) (mk_state_pc ? st2 pc lp2)
    120 ; as_label_ok :
     246; as_label_ok_non_entry :
    121247  let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
    122248  ∀st1,st2,f,fn,stmt.
    123    fetch_statement ? (prog_var_names … prog)
    124    (globalenv_noinit … prog) (pc … st1) = return〈f,fn,stmt〉 →
    125    st_rel st1 st2 →
    126    as_label (joint_abstract_status (mk_prog_params P_in prog stack_sizes)) st1 =
    127     as_label (joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes)) st2
     249  fetch_statement … (prog_var_names … prog)
     250  (joint_globalenv P_in prog stack_sizes) (pc … st1) = return〈f,fn,stmt〉 →
     251  st_rel st1 st2 → point_of_pc P_in (pc … st1) ≠ joint_if_entry … fn →
     252  as_label (joint_status P_in prog stack_sizes) st1 =
     253  as_label (joint_status P_out trans_prog stack_sizes) st2
     254; pre_main_ok :
     255  let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
     256    ∀st1,st1' : joint_abstract_status (mk_prog_params P_in prog stack_sizes) .
     257    ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes).
     258    block_id … (pc_block (pc … st1)) = -1 →
     259    st_rel st1 st2 →
     260    as_label (joint_status P_in prog stack_sizes) st1 =
     261    as_label (joint_status P_out trans_prog stack_sizes) st2 ∧
     262    joint_classify … (mk_prog_params P_in prog stack_sizes) st1 =
     263    joint_classify … (mk_prog_params P_out trans_prog stack_sizes) st2 ∧
     264    (eval_state P_in (prog_var_names … prog) (joint_globalenv P_in prog stack_sizes)
     265      st1 = return st1' →
     266    ∃st2'. st_rel st1' st2' ∧
     267    eval_state P_out (prog_var_names … trans_prog)
     268     (joint_globalenv P_out trans_prog stack_sizes) st2 = return st2')
    128269; cond_commutation :
    129270    let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
     
    131272    ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes).
    132273    ∀f,fn,a,ltrue,lfalse.
     274    block_id … (pc_block (pc … st1)) ≠ -1 →
    133275    let cond ≝ (COND P_in ? a ltrue) in
    134     fetch_statement P_in … (ev_genv … (mk_prog_params P_in prog stack_sizes)) (pc … st1) =
     276    fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) =
    135277    return 〈f, fn,  sequential … cond lfalse〉 → 
    136     eval_state P_in (prog_var_names … ℕ prog) (ev_genv … (mk_prog_params P_in prog stack_sizes))
    137     st1 = return st1' →
     278    eval_state P_in (prog_var_names … prog)
     279    (joint_globalenv P_in prog stack_sizes) st1 = return st1' →
    138280    st_rel st1 st2 →
    139281    ∀t_fn.
    140     fetch_internal_function … (globalenv_noinit … trans_prog) (pc_block (pc … st2)) =
    141     return 〈f,t_fn〉 →
     282    fetch_internal_function … (prog_var_names … trans_prog)
     283     (joint_globalenv P_out trans_prog stack_sizes) (pc_block (pc … st2)) =
     284     return 〈f,t_fn〉 →
    142285    bind_new_P' ??
    143286     (λregs1.λdata.bind_new_P' ??
     
    147290          = return sequential P_out ? ((\snd (\fst blp)) mid) lfalse→
    148291         ∃st2_pre_mid_no_pc.
    149             repeat_eval_seq_no_pc (mk_prog_params P_out trans_prog stack_sizes) f (map_eval ?? (\fst (\fst blp)) mid)
    150                                    (st_no_pc ? st2)
     292            repeat_eval_seq_no_pc … (mk_prog_params P_out trans_prog stack_sizes) f
     293             (map_eval ?? (\fst (\fst blp)) mid) (st_no_pc ? st2)
    151294            = return st2_pre_mid_no_pc ∧
    152             st_no_pc_rel (pc_block(pc … st1'))
    153              (point_of_pc P_in … (pc … st1')) (st_no_pc … st1') (st2_pre_mid_no_pc) ∧
    154             joint_classify_step (mk_prog_params P_out trans_prog stack_sizes)
    155                                 ((\snd (\fst blp)) mid)  = cl_jump ∧
    156             cost_label_of_stmt (mk_prog_params P_out trans_prog stack_sizes)
     295            st_no_pc_rel (pc … st1') (st_no_pc … st1') (st2_pre_mid_no_pc) ∧
     296            joint_classify_step … ((\snd (\fst blp)) mid)  = cl_jump ∧
     297            cost_label_of_stmt P_out (prog_var_names … trans_prog)
    157298                               (sequential P_out ? ((\snd (\fst blp)) mid) lfalse) = None ? ∧
    158299            let st2_pre_mid ≝  mk_state_pc P_out st2_pre_mid_no_pc
     
    160301            let st2' ≝ mk_state_pc P_out st2_pre_mid_no_pc (pc … st1') (last_pop … st2) in
    161302            eval_statement_advance P_out (prog_var_names … trans_prog)
    162              (ev_genv … (mk_prog_params P_out trans_prog stack_sizes)) f t_fn
     303             (joint_globalenv P_out trans_prog stack_sizes) f t_fn
    163304             (sequential P_out ? ((\snd (\fst blp)) mid) lfalse) st2_pre_mid = return st2'
    164305   )  (f_step … data (point_of_pc P_in (pc … st1)) cond)   
     
    169310  ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes).
    170311  ∀f,fn,stmt,nxt.
     312  block_id … (pc_block (pc … st1)) ≠ -1 →
    171313  let seq ≝ (step_seq P_in ? stmt) in
    172   fetch_statement P_in … (ev_genv … (mk_prog_params P_in prog stack_sizes)) (pc … st1) =
     314  fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) =
    173315  return 〈f, fn,  sequential … seq nxt〉 → 
    174   eval_state P_in (prog_var_names … ℕ prog) (ev_genv … (mk_prog_params P_in prog stack_sizes))
     316  eval_state P_in (prog_var_names … prog) (joint_globalenv P_in prog stack_sizes)
    175317  st1 = return st1' →
    176318  st_rel st1 st2 →
    177319  ∀t_fn.
    178   fetch_internal_function … (globalenv_noinit … trans_prog) (pc_block (pc … st2)) =
     320  fetch_internal_function … (prog_var_names … trans_prog)
     321     (joint_globalenv P_out trans_prog stack_sizes) (pc_block (pc … st2)) =
    179322  return 〈f,t_fn〉 →
    180323  bind_new_P' ??
    181324     (λregs1.λdata.bind_new_P' ??
    182325      (λregs2.λblp.
    183        ∃l : list (joint_seq (mk_prog_params P_out trans_prog stack_sizes)
    184                             (globals (mk_prog_params P_out trans_prog stack_sizes))).
     326       ∃l : list (joint_seq P_out (prog_var_names … trans_prog)).
    185327                            blp = (ensure_step_block ?? l) ∧
    186328       ∃st2_fin_no_pc.
    187            repeat_eval_seq_no_pc (mk_prog_params P_out trans_prog stack_sizes) f
     329           repeat_eval_seq_no_pc (mk_prog_params P_out trans_prog stack_sizes) f
    188330              l  (st_no_pc … st2)= return st2_fin_no_pc ∧
    189            st_no_pc_rel (pc_block (pc … st1'))
    190             (point_of_pc P_in … (pc … st1'))
    191             (st_no_pc … st1') st2_fin_no_pc
     331           st_no_pc_rel (pc … st1') (st_no_pc … st1') st2_fin_no_pc
    192332      ) (f_step … data (point_of_pc P_in (pc … st1)) seq)
    193333     ) (init ? fn)
     334; cost_commutation :
     335  let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
     336  ∀st1,st2,pc.∀f,fn,c,nxt.
     337  block_id … (pc_block pc) ≠ -1 →
     338  st_no_pc_rel pc st1 st2 →
     339  fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) pc =
     340  return 〈f, fn,  sequential ?? (COST_LABEL ?? c) nxt〉 → 
     341  st_no_pc_rel (pc_of_point P_in (pc_block pc) nxt) st1 st2
    194342}.
     343
     344(*TO BE MOVED*)
     345lemma decidable_In : ∀A.∀l : list A. ∀a : A. (∀a'.decidable (a = a')) → 
     346decidable (In A l a).
     347#A #l elim l [ #a #_ %2 % *] #hd #tl #IH #a #DEC cases(IH a DEC)
     348[ #H % %2 assumption | * #H cases (DEC hd)
     349[ #H1 %1 %1 assumption | * #H1 %2 % * [ #H2 @H1 assumption | #H2 @H assumption]]
     350qed.
     351
     352lemma In_all : ∀A.∀l : list A. ∀ a : A.¬In A l a → All A (λx.x≠a) l.
     353#A #l elim l [ #a #_ @I] #hd #tl #IH #a * #H % [2: @IH % #H1 @H %2 assumption]
     354% #H1 @H % >H1 %
     355qed.
     356
     357lemma All_In : ∀A.∀l : list A. ∀ a : A.All A (λx.x≠a) l → ¬In A l a.
     358#A #l elim l [#a #_ % *] #hd #tl #IH #a ** #H1 #H2 % *
     359[ #H3 @H1 >H3 % | cases(IH a H2) #H3 #H4 @H3 assumption]
     360qed.
     361
     362lemma fetch_stmt_ok_succ_ok : ∀p : sem_graph_params.
     363∀prog : joint_program p.∀stack_size,f,fn,stmt,pc,pc',lbl.
     364In ? (stmt_labels p ? stmt) lbl→
     365fetch_statement p … (joint_globalenv p prog stack_size) pc = return 〈f,fn,stmt〉 →
     366pc' = pc_of_point p (pc_block pc) lbl →
     367∃stmt'.fetch_statement p … (joint_globalenv p prog stack_size) pc' = return 〈f,fn,stmt'〉.
     368#p #prog #stack_size #f #fn #stmt #pc #pc' #lbl #Hlbl #EQfetch
     369cases(fetch_statement_inv … EQfetch) #EQfn normalize nodelta #EQstmt
     370#EQ destruct(EQ) lapply(code_is_closed … (pi2 ?? fn) … EQstmt) *
     371cases(decidable_In ? (stmt_explicit_labels … stmt) lbl ?)
     372[3: * cases lbl #x #y cases(decidable_eq_pos … x y)
     373    [#EQ destruct % % | * #H %2 % #H1 @H destruct %]
     374| whd in ⊢ (% → ?); #H1 #H2 cases(Exists_All … H1 H2) #lbl1 * #EQ destruct
     375  whd in match code_has_label; whd in match code_has_point; normalize nodelta
     376  inversion(stmt_at ????) [#_ *] #stmt' #EQstmt' #_ #_ %{stmt'}
     377  whd in match fetch_statement; normalize nodelta >EQfn >m_return_bind
     378  >point_of_pc_of_point >EQstmt' %
     379| #H lapply(In_all ??? H) -H cases(Exists_append … Hlbl)
     380  [ cases stmt [ #step #nxt | #fin | *] whd in match stmt_implicit_label;
     381    normalize nodelta [2: *] * [2: *] #EQ destruct(EQ) #_ #_
     382    whd in match stmt_forall_succ; whd in match code_has_point; normalize nodelta
     383    inversion(stmt_at ????) [#_ *] #stmt' #EQstmt' #_ %{stmt'}
     384    whd in match fetch_statement; normalize nodelta >EQfn >m_return_bind
     385    >point_of_pc_of_point >EQstmt' %
     386  | #H1 #H2 cases(Exists_All … H1 H2) #x * #EQ destruct * #H @⊥ @H %
     387  ]
     388]
     389qed.
     390
     391
    195392
    196393lemma fetch_stmt_ok_sigma_state_ok : ∀ P_in , P_out: sem_graph_params.
    197394∀prog : joint_program P_in.
    198395∀stack_sizes.
     396∀ f_lbls,f_regs.∀f_bl_r.∀init.∀st_no_pc_rel,st_rel.
     397∀f,fn,stmt,st1,st2.
     398good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs
     399                    st_no_pc_rel st_rel →
     400st_rel st1 st2 →
     401fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) =
     402 return 〈f,fn,stmt〉 →
     403st_no_pc_rel (pc … st1) (st_no_pc … st1) (st_no_pc … st2).
     404#P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_lb_r #init #st_no_pc_rel
     405#st_rel #f #fn #stmt #st1 #st2 #goodR #Hst_rel #EQfetch
     406cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt
     407@(fetch_ok_sigma_state_ok … goodR … EQfn) assumption
     408qed.
     409
     410lemma fetch_stmt_ok_sigma_pc_ok : ∀ P_in , P_out: sem_graph_params.
     411∀prog : joint_program P_in.
     412∀stack_sizes.
    199413∀ f_lbls,f_regs.∀f_bl_r.∀init.
    200 ∀good : b_graph_transform_program_props P_in P_out init prog f_bl_r f_lbls f_regs.
    201414∀st_no_pc_rel,st_rel.
    202415∀f,fn,stmt,st1,st2.
    203 good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs good
     416good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs 
     417                    st_no_pc_rel st_rel →
     418st_rel st1 st2 →
     419fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) =
     420 return 〈f,fn,stmt〉 →
     421pc … st1 = pc … st2.
     422#P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_lb_r #init #st_no_pc_rel
     423#st_rel #f #fn #stmt #st1 #st2 #goodR #Hst_rel #EQfetch
     424cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt
     425@(fetch_ok_pc_ok … goodR … EQfn) assumption
     426qed.
     427
     428lemma fetch_stmt_ok_sigma_last_pop_ok : ∀ P_in , P_out: sem_graph_params.
     429∀prog : joint_program P_in.
     430∀stack_sizes.
     431∀ f_lbls,f_regs.∀f_bl_r.∀init.
     432∀st_no_pc_rel,st_rel.
     433∀f,fn,stmt,st1,st2.
     434good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs
    204435                    st_no_pc_rel st_rel →
    205436st_rel st1 st2 →
    206437fetch_statement P_in … (ev_genv … (mk_prog_params P_in prog stack_sizes)) (pc … st1) =
    207438 return 〈f,fn,stmt〉 →
    208 st_no_pc_rel (pc_block (pc … st1)) (point_of_pc P_in … (pc … st1)) (st_no_pc … st1) (st_no_pc … st2).
    209 #P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_lb_r #init #good #st_no_pc_rel
    210 #st_rel #f #fn #stmt #st1 #st2 #goodR #Hst_rel #EQfetch
    211 cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt
    212 @(fetch_ok_sigma_state_ok … goodR … EQfn) assumption
    213 qed.
    214 
    215 lemma fetch_stmt_ok_sigma_pc_ok : ∀ P_in , P_out: sem_graph_params.
    216 ∀prog : joint_program P_in.
    217 ∀stack_sizes.
    218 ∀ f_lbls,f_regs.∀f_bl_r.∀init.
    219 ∀good : b_graph_transform_program_props P_in P_out init prog f_bl_r f_lbls f_regs.
    220 ∀st_no_pc_rel,st_rel.
    221 ∀f,fn,stmt,st1,st2.
    222 good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs good
    223                     st_no_pc_rel st_rel →
    224 st_rel st1 st2 →
    225 fetch_statement P_in … (ev_genv … (mk_prog_params P_in prog stack_sizes)) (pc … st1) =
    226  return 〈f,fn,stmt〉 →
    227 pc … st1 = pc … st2.
    228 #P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_lb_r #init #good #st_no_pc_rel
    229 #st_rel #f #fn #stmt #st1 #st2 #goodR #Hst_rel #EQfetch
    230 cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt
    231 @(fetch_ok_pc_ok … goodR … EQfn) assumption
    232 qed.
    233 
    234 lemma fetch_stmt_ok_sigma_last_pop_ok : ∀ P_in , P_out: sem_graph_params.
    235 ∀prog : joint_program P_in.
    236 ∀stack_sizes.
    237 ∀ f_lbls,f_regs.∀f_bl_r.∀init.
    238 ∀good : b_graph_transform_program_props P_in P_out init prog f_bl_r f_lbls f_regs.
    239 ∀st_no_pc_rel,st_rel.
    240 ∀f,fn,stmt,st1,st2.
    241 good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs good
    242                     st_no_pc_rel st_rel →
    243 st_rel st1 st2 →
    244 fetch_statement P_in … (ev_genv … (mk_prog_params P_in prog stack_sizes)) (pc … st1) =
    245  return 〈f,fn,stmt〉 →
    246 (last_pop … st1) = sigma_stored_pc P_in P_out prog f_lbls (last_pop … st2).
    247 #P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_lb_r #init #good #st_no_pc_rel
     439(last_pop … st1) =
     440 sigma_stored_pc P_in P_out prog stack_sizes init f_bl_r f_lbls
     441  f_regs (last_pop … st2).
     442#P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_lb_r #init #st_no_pc_rel
    248443#st_rel #f #fn #stmt #st1 #st2 #goodR #Hst_rel #EQfetch
    249444cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt
     
    282477qed.*)
    283478
     479(*TO BE MOVED*)
     480lemma append_All : ∀A : Type[0]. ∀ P : A → Prop. ∀l1,l2 : list A.
     481All ? P (l1 @ l2) → All ? P l1 ∧ All ? P l2.
     482#A #P #l1 elim l1
     483[ #l2 change with l2 in ⊢ (???% → ?); #H % //]
     484#a #tl #IH #l2 change with (P a ∧ All A P (tl @ l2)) in ⊢ (% → ?);
     485* #H1 #H2 lapply(IH … H2) * #H3 #H4 % // whd % //
     486qed.
     487
    284488lemma general_eval_cond_ok : ∀ P_in , P_out: sem_graph_params.
    285489∀prog : joint_program P_in.
    286490∀stack_sizes.
    287491∀ f_lbls,f_regs.∀f_bl_r.∀init.
    288 ∀good : b_graph_transform_program_props P_in P_out init prog f_bl_r f_lbls f_regs.
    289492∀st_no_pc_rel,st_rel.
    290493let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in
    291494let trans_prog  ≝ b_graph_transform_program P_in P_out init prog in
    292495let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in
    293 good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs good
    294                     st_no_pc_rel st_rel 
     496good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs
     497                    st_no_pc_rel st_rel
    295498∀st1,st1' : joint_abstract_status prog_pars_in.
    296499∀st2 : joint_abstract_status prog_pars_out.
     
    298501∀fn : joint_closed_internal_function P_in (prog_var_names … prog).
    299502∀a,ltrue,lfalse.
     503block_id … (pc_block (pc … st1)) ≠ -1 →
    300504st_rel st1 st2 →
    301505 let cond ≝ (COND P_in ? a ltrue) in
    302506  fetch_statement P_in …
    303    (globalenv_noinit ? prog) (pc … st1) =
     507   (joint_globalenv P_in prog stack_sizes) (pc … st1) =
    304508     return 〈f, fn,  sequential … cond lfalse〉 →
    305  eval_state P_in (prog_var_names … prog)
    306   (ev_genv … prog_pars_in) st1 = return st1' →
     509 eval_state P_in (prog_var_names … prog)
     510  (joint_globalenv P_in prog stack_sizes) st1 = return st1' →
    307511as_costed (joint_abstract_status prog_pars_in) st1' →
    308512∃ st2'. st_rel st1' st2' ∧
    309513∃taf : trace_any_any_free (joint_abstract_status prog_pars_out) st2 st2'.
    310514bool_to_Prop (taaf_non_empty … taf).
    311 #P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_bl_r #init #good #st_no_pc_rel #st_rel
    312 #goodR #st1 #st1' #st2 #f #fn #a #ltrue #lfalse #Rst1st2 #EQfetch #EQeval
     515#P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_bl_r #init #st_no_pc_rel
     516#st_rel #goodR #st1 #st1' #st2 #f #fn #a #ltrue #lfalse * #Hbl #Rst1st2 #EQfetch
     517#EQeval
    313518@('bind_inversion EQeval) #x >EQfetch whd in ⊢ (??%% → ?); #EQ destruct(EQ)
    314519whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
    315520#H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H #bv #EQbv
    316521#H @('bind_inversion H) -H * #EQbool normalize nodelta whd in ⊢ (??%% → ?);
    317 cases(fetch_statement_inv … EQfetch) #EQfn #_
     522cases(fetch_statement_inv … EQfetch) #EQfn normalize nodelta #EQstmt
    318523[ >(pc_of_label_eq … EQfn)
    319524  normalize nodelta whd in match set_pc; normalize nodelta whd in ⊢ (??%? → ?);
    320525| whd in match next; whd in match set_pc; whd in match set_no_pc; normalize nodelta
    321526]
    322 #EQ destruct(EQ) #n_costed
    323 cases(b_graph_transform_program_fetch_statement … good … EQfetch)
     527#EQ destruct(EQ) #n_costed
     528lapply(b_graph_transform_program_fetch_statement … goodR (pc … st1) f fn ?)
     529[2,4: @eqZb_elim [1,3: #ABS @⊥ >ABS in Hbl; #H @H %] #_ normalize nodelta
     530      #H cases(H EQfetch) -H |*:]
    324531#init_data * #t_fn1 **  >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch)
    325 #EQt_fn1 whd in ⊢ (% → ?); #Hinit
    326 * #labs * #regs ** #EQlabs #EQf_regs normalize nodelta *** #blp #blm #bls *
    327 whd in ⊢ (% → ?); @if_elim
    328 [1,3: @eq_identifier_elim [2,4: #_ *] whd in match point_of_pc; normalize nodelta
    329   whd in match (point_of_offset ??); #ABS #_ lapply(fetch_statement_inv … EQfetch)
    330   * #_ >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) whd in match point_of_pc;
    331   normalize nodelta whd in match (point_of_offset ??); <ABS
    332   cases(entry_is_cost … (pi2 ?? fn)) #nxt1 * #c #EQ >EQ #EQ1 destruct(EQ1)
     532#EQt_fn1 whd in ⊢ (% → ?); #Hinit normalize nodelta
     533*** #blp #blm #bls * whd in ⊢ (% → ?); @if_elim
     534[1,3: @eq_identifier_elim [2,4: #_ cases(not_emptyb ??) *]
     535      whd in match point_of_pc; normalize nodelta whd in match (point_of_offset ??);
     536      #ABS #_ lapply(fetch_statement_inv … EQfetch) * #_
     537      >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch)
     538      whd in match point_of_pc; normalize nodelta whd in match (point_of_offset ??);
     539      <ABS cases(entry_is_cost … (pi2 ?? fn)) #nxt1 * #c #EQ >EQ #EQ1 destruct(EQ1)
    333540]
    334541#_ <(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) #EQbl whd in ⊢ (% → ?); *
     
    337544cases(bind_new_bind_new_instantiates … EQbl (bind_new_bind_new_instantiates … Hinit
    338545               (cond_commutation … goodR … EQfetch EQeval Rst1st2 t_fn1 EQt_fn1)))
     546[2,4: % assumption]
    339547#EQ destruct(EQ) #APP whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2)
    340548cases(APP … EQmid) -APP #st_pre_mid_no_pc **** whd in match set_no_pc; normalize nodelta
     
    368576]
    369577#taa_pre_mid %{(taaf_step_jump ? ??? taa_pre_mid ???) I}
    370 [1,4: whd <(as_label_ok ??????????? goodR st1' st2' f fn ?? H_fin) [1,4: assumption]
    371       cases daemon (*TODO: general lemma!*)
     578[1,4: cases(fetch_stmt_ok_succ_ok … (pc … st1) (pc … st1') … EQfetch ?)
     579      [2: @ltrue|3: %2 % % |4: % |6: @lfalse |7: % % |8: %] #stmt' #EQstmt'
     580      whd <(as_label_ok_non_entry … goodR … EQstmt' H_fin)
     581      [1,3: assumption
     582      |2,4: cases(entry_unused … (pi2 ?? fn) … EQstmt)
     583            [ whd in match stmt_forall_labels; whd in match stmt_labels;
     584              normalize nodelta #H cases(append_All … H) #_
     585              whd in match stmt_explicit_labels; whd in match step_labels;
     586              normalize nodelta * whd in match (point_of_label ????);
     587              * #H1 #_ #_ >point_of_pc_of_point % #H2 @H1 >H2 %
     588            | ** whd in match (point_of_label ????); #H1 #_ #_ % whd in match st1';
     589              #H2 @H1 <H2 whd in match succ_pc; whd in match point_of_pc;
     590              normalize nodelta whd in match pc_of_point; normalize nodelta
     591              >point_of_offset_of_point %
     592            ]
     593      ]
    372594|2,5: whd whd in match (as_classify ??); whd in match fetch_statement; normalize nodelta
    373595      >EQt_fn1 >m_return_bind >point_of_pc_of_point >EQmid normalize nodelta
     
    384606qed.
    385607
     608
     609lemma general_eval_seq_no_call_ok :∀ P_in , P_out: sem_graph_params.
     610∀prog : joint_program P_in.
     611∀stack_sizes.
     612∀ f_lbls,f_regs.∀f_bl_r.∀init.
     613∀st_no_pc_rel,st_rel.
     614let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in
     615let trans_prog  ≝ b_graph_transform_program P_in P_out init prog in
     616let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in
     617good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs
     618                    st_no_pc_rel st_rel →
     619∀st1,st1' : joint_abstract_status prog_pars_in.
     620∀st2 : joint_abstract_status prog_pars_out.
     621∀f.∀fn : joint_closed_internal_function P_in (prog_var_names … prog).
     622∀stmt,nxt.
     623block_id … (pc_block (pc … st1)) ≠ -1 →
     624st_rel st1 st2 →
     625 let seq ≝ (step_seq P_in ? stmt) in
     626  fetch_statement P_in …
     627   (joint_globalenv P_in prog stack_sizes) (pc … st1) =
     628     return 〈f, fn,  sequential ?? seq nxt〉 →
     629 eval_state P_in (prog_var_names … prog) (joint_globalenv P_in prog stack_sizes)
     630  st1 = return st1' →
     631∃st2'. st_rel st1' st2' ∧           
     632∃taf : trace_any_any_free (joint_abstract_status prog_pars_out) st2 st2'.           
     633 if taaf_non_empty … taf then True else  (*IT CAN BE SIMPLIFIED *)
     634(¬as_costed (joint_abstract_status (mk_prog_params P_in prog stack_sizes)) st1 ∨
     635 ¬as_costed (joint_abstract_status (mk_prog_params P_in prog stack_sizes)) st1').
     636#P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_bl_r #init #st_no_pc_rel #st_rel
     637#goodR #st1 #st1' #st2 #f #fn #stmt #nxt * #Hbl #Rst1st2 #EQfetch #EQeval
     638@('bind_inversion EQeval) #x >EQfetch whd in ⊢ (??%% → ?); #EQ destruct(EQ)
     639#H @('bind_inversion H) -H #st1_no_pc #H lapply(err_eq_from_io ????? H) -H
     640#EQst1_no_pc whd in ⊢ (??%% → ?); whd in match next; whd in match set_pc;
     641whd in match set_no_pc; normalize nodelta #EQ destruct(EQ)
     642lapply(b_graph_transform_program_fetch_statement … goodR (pc … st1) f fn ?)
     643[2: @eqZb_elim [ #ABS @⊥ >ABS in Hbl; #H @H %] #_ normalize nodelta
     644      #H cases(H EQfetch) -H |*:]
     645#init_data * #t_fn ** >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch)
     646#EQt_fn #Hinit normalize nodelta * #bl * @if_elim
     647[ @eq_identifier_elim [2: #_ cases(not_emptyb ??) *] whd in match point_of_pc;
     648  normalize nodelta whd in match (point_of_offset ??); #ABS #_
     649  lapply(fetch_statement_inv … EQfetch) * #_
     650  >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) whd in match point_of_pc;
     651  normalize nodelta whd in match (point_of_offset ??); <ABS
     652  cases(entry_is_cost … (pi2 ?? fn)) #nxt1 * #c #EQ >EQ #EQ1 destruct(EQ1)
     653]
     654#_ <(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) #EQbl
     655>(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) #SBiC
     656cases(bind_new_bind_new_instantiates … EQbl (bind_new_bind_new_instantiates … Hinit
     657               (seq_commutation … goodR … EQfetch EQeval Rst1st2 t_fn EQt_fn)))
     658               [2: % assumption]
     659#l * #EQ destruct(EQ) * #st2_fin_no_pc * #EQst2_fin_no_pc #Rsem
     660%{(mk_state_pc ? st2_fin_no_pc (pc_of_point P_out (pc_block (pc … st2)) nxt) (last_pop … st2))}
     661cases(fetch_statement_inv … EQfetch) >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch)
     662#EQfn #_
     663%
     664[ @(st_rel_def ?????????? goodR … f fn)
     665      [ change with (pc_block (pc … st2)) in match (pc_block ?); assumption
     666      | <(fetch_stmt_ok_sigma_pc_ok … goodR … EQfetch) assumption
     667      | @(fetch_stmt_ok_sigma_last_pop_ok … goodR … EQfetch) assumption
     668      ]
     669]
     670%{(produce_trace_any_any_free_coerced ? st2 f t_fn l ?? st2_fin_no_pc EQt_fn
     671                                      SBiC EQst2_fin_no_pc)}
     672@if_elim #_ [@I] % % whd in ⊢ (% → ?); * #H @H -H whd in ⊢ (??%?); >EQfetch %
     673qed.
     674
     675
     676lemma general_eval_cost_ok :
     677∀ P_in , P_out: sem_graph_params.
     678∀prog : joint_program P_in.
     679∀stack_sizes.
     680∀ f_lbls,f_regs.∀f_bl_r.∀init.
     681∀st_no_pc_rel,st_rel.
     682let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in
     683let trans_prog  ≝ b_graph_transform_program P_in P_out init prog in
     684let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in
     685good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs
     686                    st_no_pc_rel st_rel →
     687∀st1,st1' : joint_abstract_status prog_pars_in.
     688∀st2 : joint_abstract_status prog_pars_out.
     689∀f.
     690∀fn : joint_closed_internal_function P_in (prog_var_names … prog).∀c,nxt.
     691block_id … (pc_block (pc … st1)) ≠ -1 →
     692st_rel st1 st2 →
     693let cost ≝ COST_LABEL P_in ? c in
     694 fetch_statement P_in …
     695  (joint_globalenv P_in prog stack_sizes) (pc … st1) =
     696    return 〈f, fn,  sequential ?? cost nxt〉 →
     697 eval_state P_in (prog_var_names … prog) (ev_genv … prog_pars_in)
     698            st1 = return st1' →
     699∃ st2'. st_rel st1' st2' ∧
     700∃taf : trace_any_any_free
     701        (joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes))
     702        st2 st2'.
     703bool_to_Prop (taaf_non_empty … taf).
     704#P_in #P_out #prog #stack_size #f_lbls #f_regs #f_bl_r #init #st_no_pc_rel
     705#st_rel #goodR #st1 #st1' #st2 #f #fn #c #nxt * #Hbl #Rst1st2 normalize nodelta
     706#EQfetch
     707whd in match eval_state; whd in match eval_statement_no_pc; normalize nodelta
     708>EQfetch >m_return_bind normalize nodelta >m_return_bind whd in ⊢ (??%% → ?);
     709#EQ destruct(EQ)
     710%{(mk_state_pc ? (st_no_pc … st2) (pc_of_point P_out (pc_block (pc … st2)) nxt)
     711                 (last_pop … st2))} %
     712[ cases(fetch_statement_inv … EQfetch) #EQfn #_
     713  <(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch)
     714  whd in match (succ_pc ???); whd in match (point_of_succ ???);
     715  >set_no_pc_eta
     716  @(st_rel_def … prog … stack_size … goodR
     717          (st_no_pc … st1) (st_no_pc … st2)) [3: >EQfn in ⊢ (??%?); %|1,2:]
     718  [ @(cost_commutation … prog … stack_size … goodR … EQfetch) [ % assumption]
     719    @(fetch_stmt_ok_sigma_state_ok … goodR … Rst1st2 EQfetch)
     720  | @(fetch_stmt_ok_sigma_last_pop_ok … goodR … Rst1st2 EQfetch)
     721  ]
     722| lapply(b_graph_transform_program_fetch_statement … goodR (pc … st1) f fn ?)
     723  [2: @eqZb_elim [ #ABS @⊥ >ABS in Hbl; #H @H %] #_ normalize nodelta
     724      #H cases(H EQfetch) -H |*:]
     725  #init_data * #t_fn ** >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch)
     726  #EQt_fn #Hinit normalize nodelta * #bl *
     727  @if_elim @eq_identifier_elim [2: #_ cases(not_emptyb ??) *]
     728  [ #EQentry inversion(not_emptyb ??) [2: #_ *] #non_empty_pre #_ whd in ⊢ (% → ?);
     729    inversion (f_regs ??) [2: #x #y #_ #_ *] #EQregs normalize nodelta #EQ destruct(EQ)
     730    whd in ⊢ (% → ?); * #pre * #mid1 * #mid2 * #post *** #EQmid1 whd in ⊢ (% → ?);
     731    * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in ⊢ (% → ?); * #nxt1 * #EQt_stmt
     732    change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) whd in ⊢ (% → ?);
     733    * #EQ1 #EQ2 destruct(EQ1 EQ2)
     734  | #EQentry inversion(not_emptyb ??) [ #_ *] #empty_pre #_
     735    >(f_step_on_cost … init_data) whd in ⊢ (% → ?); inversion(f_regs ??) [2: #x #y #_ #_ *]
     736   #EQregs normalize nodelta #EQ destruct(EQ) whd in ⊢ (% → ?); * #pre * #mid1 *
     737   #mid2 * #post *** #EQmid1 * #EQ1 #EQ2 destruct(EQ1 EQ2) * #nxt1 * #EQt_stmt
     738   change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) * #EQ1 #EQ2 destruct(EQ1 EQ2)
     739  | #EQentry #_  >(f_step_on_cost … init_data) whd in ⊢ (% → ?);
     740    inversion(f_regs ??) [2: #x #y #_ #_ *] #EQregs normalize nodelta #EQ destruct(EQ)
     741    * #pre * #mid1 * #mid2 * #post *** #EQmid1 * #EQ1 #EQ2 destruct(EQ1 EQ2) *
     742    #nxt1 * #EQt_stmt change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ)
     743    * #EQ1 #EQ2 destruct(EQ1 EQ2)
     744  ] 
     745  %{(taaf_step … (taa_base …) …)}
     746  [3,6,9: @I
     747  |*: whd whd in ⊢ (??%?); whd in match fetch_statement; normalize nodelta
     748     >EQt_fn >m_return_bind >EQt_stmt >m_return_bind %
     749  ]
     750]
     751qed.
     752
    386753(*
    387 let rec taa_to_taaf  S st1 st2 (taa : trace_any_any S st1 st2) on taa :
    388 trace_any_any_free S st1 st2 ≝
    389 (match taa in trace_any_any return λs1,s2.λx.st1 = s1 → st2 = s2 → taa ≃ x → trace_any_any_free S s1 s2 with
    390 [taa_base st1' ⇒ λprf.?
    391 |taa_step st1' st2' st3' H I J tl ⇒ λprf.?
    392 ]) (refl … st1) (refl … st2) (refl_jmeq ? taa).
    393 *)
    394 
    395 lemma general_eval_seq_no_call_ok :∀ P_in , P_out: sem_graph_params.
     754lemma eval_return_ok :
     755∀ P_in , P_out: sem_graph_params.
    396756∀prog : joint_program P_in.
    397757∀stack_sizes.
     
    404764good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs good
    405765                    st_no_pc_rel st_rel →
    406 ∀st1,st1' : joint_abstract_status prog_pars_in.
    407 ∀st2 : joint_abstract_status prog_pars_out.
    408 ∀f.∀fn : joint_closed_internal_function P_in (prog_var_names … prog).
    409 ∀stmt,nxt.
    410 st_rel st1 st2 →
    411  let seq ≝ (step_seq P_in ? stmt) in
    412   fetch_statement P_in …
    413    (globalenv_noinit ? prog) (pc … st1) =
    414      return 〈f, fn,  sequential ?? seq nxt〉 →
    415  eval_state P_in (prog_var_names … ℕ prog) (ev_genv … prog_pars_in)
    416   st1 = return st1' →
    417 ∃st2'. st_rel st1' st2' ∧           
    418 ∃taf : trace_any_any_free (joint_abstract_status prog_pars_out) st2 st2'.           
    419  if taaf_non_empty … taf then True else  (*IT CAN BE SIMPLIFIED *)
    420 (¬as_costed (joint_abstract_status (mk_prog_params P_in prog stack_sizes)) st1 ∨
    421  ¬as_costed (joint_abstract_status (mk_prog_params P_in prog stack_sizes)) st1').
    422 #P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_bl_r #init #good #st_no_pc_rel #st_rel
    423 #goodR #st1 #st1' #st2 #f #fn #stmt #nxt #Rst1st2 #EQfetch #EQeval
    424 @('bind_inversion EQeval) #x >EQfetch whd in ⊢ (??%% → ?); #EQ destruct(EQ)
    425 #H @('bind_inversion H) -H #st1_no_pc #H lapply(err_eq_from_io ????? H) -H
    426 #EQst1_no_pc whd in ⊢ (??%% → ?); whd in match next; whd in match set_pc;
    427 whd in match set_no_pc; normalize nodelta #EQ destruct(EQ)
    428 cases(b_graph_transform_program_fetch_statement … good … EQfetch)
    429 #init_data * #t_fn ** >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch)
    430 #EQt_fn #Hinit * #labs * #regs ** #EQlabs #EQregs normalize nodelta * #bl * @if_elim
    431 [ @eq_identifier_elim [2: #_ *] whd in match point_of_pc; normalize nodelta
    432   whd in match (point_of_offset ??); #ABS #_ lapply(fetch_statement_inv … EQfetch)
    433   * #_ >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) whd in match point_of_pc;
    434   normalize nodelta whd in match (point_of_offset ??); <ABS
    435   cases(entry_is_cost … (pi2 ?? fn)) #nxt1 * #c #EQ >EQ #EQ1 destruct(EQ1)
    436 ]
    437 #_ <(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) #EQbl
    438 >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) #SBiC
    439 cases(bind_new_bind_new_instantiates … EQbl (bind_new_bind_new_instantiates … Hinit
    440                (seq_commutation … goodR … EQfetch EQeval Rst1st2 t_fn EQt_fn)))
    441 #l * #EQ destruct(EQ) * #st2_fin_no_pc * #EQst2_fin_no_pc #Rsem
    442 %{(mk_state_pc ? st2_fin_no_pc (pc_of_point P_out (pc_block (pc … st2)) nxt) (last_pop … st2))}
    443 cases(fetch_statement_inv … EQfetch) >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch)
    444 #EQfn #_
    445 %
    446 [ @(st_rel_def ??????????? goodR … f fn)
    447       [ change with (pc_block (pc … st2)) in match (pc_block ?); assumption
    448       | <(fetch_stmt_ok_sigma_pc_ok … goodR … EQfetch) assumption
    449       | @(fetch_stmt_ok_sigma_last_pop_ok … goodR … EQfetch) assumption
    450       ]
    451 ]
    452 %{(produce_trace_any_any_free_coerced ? st2 f t_fn l ?? st2_fin_no_pc EQt_fn
    453                                       SBiC EQst2_fin_no_pc)}
    454 @if_elim #_ [@I] % % whd in ⊢ (% → ?); * #H @H -H whd in ⊢ (??%?); >EQfetch %
    455 qed.
    456 
    457 (*
    458 lemma eval_cost_ok :
    459 ∀ P_in , P_out: sem_graph_params.
    460 ∀prog : joint_program P_in.
    461 ∀stack_sizes.
    462 ∀ f_lbls,f_regs.∀f_bl_r.∀init.
    463 ∀good : b_graph_transform_program_props P_in P_out init prog f_bl_r f_lbls f_regs.
    464 let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in
    465 let trans_prog  ≝ b_graph_transform_program P_in P_out init prog in
    466 let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in
    467 ∀ R : joint_abstract_status prog_pars_in → joint_abstract_status prog_pars_out → Prop.
    468 ∀st1,st1' : joint_abstract_status prog_pars_in.
     766∀st1,st1' :  joint_abstract_status prog_pars_in.
    469767∀st2 : joint_abstract_status prog_pars_out.
    470768∀f.
    471 ∀fn : joint_closed_internal_function P_in (prog_var_names … prog).∀c,nxt.
    472 R st1 st2 →
    473 let cost ≝ COST_LABEL P_in ? c in
    474  fetch_statement P_in …
    475   (globalenv_noinit ? prog) (pc … st1) =
    476     return 〈f, fn,  sequential ?? cost nxt〉 →
    477  eval_state P_in (prog_var_names … ℕ prog) (ev_genv … prog_pars_in)
    478             st1 = return st1' →
    479 ∃ st2'. R st1' st2' ∧
    480 ∃taf : trace_any_any_free
    481         (joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes))
    482         st2 st2'.
    483 bool_to_Prop (taaf_non_empty … taf).
    484 #P_in #P_out #prog #stack_size #f_lbls #f_regs #f_bl_r #init #good #R #st1 #st1'
    485 #st2 #f #fn #c #nxt #Rst1st2 normalize nodelta #EQfetch whd in match eval_state;
    486 whd in match eval_statement_no_pc; normalize nodelta >EQfetch >m_return_bind
    487 normalize nodelta >m_return_bind whd in ⊢ (??%% → ?); #EQ destruct(EQ)
     769∀fn : joint_closed_internal_function P_in (prog_var_names … prog).
    488770*)
     771
  • src/joint/Traces.ma

    r2968 r2991  
    208208
    209209definition cost_label_of_stmt :
    210   ∀p : sem_params.∀pars.joint_statement p (globals p pars) → option costlabel ≝
    211   λp,pars,s.match s with
     210  ∀p,globals.joint_statement p globals → option costlabel ≝
     211  λp,g,s.match s with
    212212  [ sequential s _ ⇒
    213213    match s with
Note: See TracChangeset for help on using the changeset viewer.