Changeset 2883


Ignore:
Timestamp:
Mar 15, 2013, 6:33:18 PM (4 years ago)
Author:
piccolo
Message:

partial commit

Location:
src
Files:
6 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLtoERTLptrOK.ma

    r2843 r2883  
    157157#EQt_fn >EQt_fn >m_return_bind >(fetch_stmt_ok_sigma_pc_ok … EQfetch) in EQt_stmt;
    158158#EQt_stmt >EQt_stmt %
     159qed.
     160
     161include "joint/StatusSimulationHelper.ma".
     162
     163lemma make_ERTL_To_ERTLptr_good_state_relation :
     164∀prog : ertl_program.
     165let p_out ≝ ertl_to_ertlptr prog in
     166∀stack_sizes.
     167∃init_regs : block → list register.
     168∃f_lbls : block → label → list label.
     169∃f_regs : block → label → list register.
     170∃good : b_graph_transform_program_props ERTL_semantics ERTLptr_semantics
     171        (λglobals,fn.«translate_data globals fn,(refl …)»)
     172        prog init_regs f_lbls f_regs.
     173good_state_relation ERTL_semantics ERTLptr_semantics prog stack_sizes
     174 (λglobals,fn.«translate_data globals fn,(refl …)»)
     175 (sem_rel … (ERTLptrStatusSimulation prog … good)).
     176#prog #stack_sizes
     177cases(make_b_graph_transform_program_props ERTL_semantics ERTLptr_semantics
     178          (λglobals,fn.«translate_data globals fn,(refl …)») prog)
     179#init_regs * #f_lbls * #f_regs #good %{init_regs} %{f_lbls} %{f_regs} %{good}
     180%
     181[#s1 #s2 #f #fn #stmt whd in ⊢ (% → ?); #EQ destruct(EQ) @fetch_stmt_ok_sigma_pc_ok
     182| #st1 #st2 #f #fn #stmt #EQfetch whd in ⊢ (% → ?); #EQ destruct(EQ)
     183  lapply(as_label_ok … good st2 … EQfetch) #EQ <EQ in ⊢ (??%?); %
     184| normalize nodelta whd in ⊢ (% → % → % → ?); #st1 #st1' #st2 #f #fn
     185  #a #ltrue #lfalse #EQfetch cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt
     186   whd in match eval_state; whd in match eval_statement_no_pc;
     187  normalize nodelta >EQfetch >m_return_bind normalize nodelta >m_return_bind
     188  whd in match eval_statement_advance; normalize nodelta
     189  change with (ps_reg_retrieve ??) in match (acca_retrieve ?????);
     190  #H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H
     191  #bv whd in match set_no_pc; normalize nodelta #EQbv
     192   #H @('bind_inversion H) -H * #EQbool normalize nodelta
     193   [whd in match goto; normalize nodelta >(pc_of_label_eq … EQfn)
     194    >m_return_bind] whd in ⊢ (??%% → ?); #EQ destruct(EQ)
     195  whd in ⊢ (% → ?); #EQ destruct(EQ) >(fetch_stmt_ok_sigma_state_ok … EQfetch) in EQbv;
     196  whd in match sigma_state; normalize nodelta #EQbv
     197  cases(ps_reg_retrieve_ok ?????? EQbv) #bv1 * #EQbv1 #EQ destruct(EQ)
     198  cases(bool_of_beval_ok … EQbool) #b * #EQb #EQ destruct(EQ) #t_fn #EQt_fn
     199  whd %{(refl …)} #mid #EQt_stmt %{(st_no_pc … st2)} %{(refl …)}
     200  % [1,3: %{(refl …)} %]
     201  %{(set_pc ? (pc_of_point ERTLptr_semantics (pc_block (pc … st2)) ?) st2)}
     202  [@ltrue |3: @lfalse] whd in match fetch_statement; normalize nodelta
     203  >EQt_fn >m_return_bind >point_of_pc_of_point >EQt_stmt >m_return_bind
     204  normalize nodelta >m_return_bind
     205  change with (ps_reg_retrieve ??) in match (acca_retrieve ?????);
     206  >EQbv1 >m_return_bind >EQb >m_return_bind normalize nodelta
     207  [ >(pc_of_label_eq … EQt_fn) >m_return_bind] %{(refl …)}
     208  whd whd in match sigma_state_pc; normalize nodelta
     209  change with (pc_block (pc … st2)) in match (pc_block ?);
     210  <(fetch_stmt_ok_sigma_pc_ok … EQfetch) >EQfn %
     211]
    159212qed.
    160213
  • src/ERTLptr/ERTLptrToLTL.ma

    r2844 r2883  
    2323  the offset does not need the stack size to be computed *)
    2424
     25check ltl_lin_seq
    2526definition preserve_carry_bit :
    26   ∀globals.bool → list (joint_seq LTL globals) → list (joint_seq LTL globals) ≝
     27 (λglobals:list ident
     28  .λdo_it:bool
     29   .λsteps:step_block LTL globals
     30    .if do_it 
     31     then 〈[λ_:code_point LTL.SAVE_CARRY]@ \fst  (\fst  steps),
     32              \snd  (\fst  steps),
     33              \snd  steps@[RESTORE_CARRY]〉 
     34     else steps ).
     35
     36
     37  ∀globals.bool → step_block LTL globals → step_block LTL globals ≝
    2738  λglobals,do_it,steps.
    28   if do_it then SAVE_CARRY :: steps @ [RESTORE_CARRY] else steps.
     39  if do_it then
     40    〈[?] @ (\fst(\fst steps)),
     41     \snd(\fst steps),
     42      (\snd  steps) @ [RESTORE_CARRY]〉
     43  else steps.
     44#_ @SAVE_CARRY
     45qed.
     46check preserve_carry_bit
    2947
    3048(* for notation *)
  • src/ERTLptr/ERTLptrToLTLProof.ma

    r2863 r2883  
    2525program_counter → program_counter.
    2626
     27
     28definition clear_sb_type ≝ label → decision → bool.
     29 
     30axiom to_be_cleared_sb : 
     31∀after : valuation register_lattice. coloured_graph after → clear_sb_type.
     32
     33definition clear_fb_type ≝ label → vertex → bool.
     34
     35axiom to_be_cleared_fb :
     36∀after : valuation register_lattice.clear_fb_type.
     37
    2738axiom sigma_fb_state: ertlptr_program → (block → label → list label) →
    28  (block → label → list register) → list register →
    29   state ERTLptr_semantics → state ERTLptr_semantics.
    30 
     39 (block → label → list register) →
     40 clear_fb_type → state ERTLptr_semantics → state ERTLptr_semantics.
     41
     42axiom acc_is_dead : ∀fix_comp.∀prog : ertlptr_program.
     43∀fn : joint_closed_internal_function ERTLptr (prog_var_names … prog).
     44∀l.
     45let after ≝ (analyse_liveness fix_comp (prog_var_names … prog) fn) in
     46¬ lives (inr ? ? RegisterA) (livebefore  … fn l after).
     47
     48axiom dead_registers_in_dead :  ∀fix_comp.∀build : coloured_graph_computer.
     49∀prog : ertlptr_program.
     50∀fn : joint_closed_internal_function ERTLptr (prog_var_names … prog).
     51∀l.
     52let after ≝ (analyse_liveness fix_comp (prog_var_names … prog) fn) in
     53let coloured_graph ≝ build … fn after in
     54∀R : Register.
     55¬ lives (inr ? ? R) (livebefore  … fn l after) →
     56to_be_cleared_sb after coloured_graph l R.
     57 
    3158axiom sigma_sb_state: ertlptr_program → (block → label → list label) →
    32  (block → label → list register) → list register →
    33   state LTL_semantics → state ERTLptr_semantics.
     59 (block → label → list register) → clear_sb_type → state LTL_semantics → state ERTLptr_semantics.
    3460
    3561definition dummy_state : state ERTLptr_semantics ≝
     
    4167
    4268
    43 definition sigma_fb_state_pc : ertlptr_program → (block → label → list label) →
    44  (block → label → list register) →
    45  state_pc ERTLptr_semantics → state_pc ERTLptr_semantics ≝
    46 λprog,f_lbls,f_regs,st.
     69definition sigma_fb_state_pc : fixpoint_computer → ertlptr_program →
     70(block → label → list label) → (block → label → list register) →
     71state_pc ERTLptr_semantics → state_pc ERTLptr_semantics ≝
     72λfix_comp,prog,f_lbls,f_regs,st.
    4773let ge ≝ globalenv_noinit … prog in
    4874let globals ≝ prog_var_names … prog in
    4975match fetch_internal_function … ge (pc_block (pc … st)) with
    50   [ OK y ⇒ ?
     76  [ OK y ⇒
     77  let after ≝ (analyse_liveness fix_comp (prog_var_names … prog) (\snd y)) in
     78  mk_state_pc ? (sigma_fb_state prog f_lbls f_regs (to_be_cleared_fb after) st) (pc … st) 
     79                         (last_pop … st)
    5180  | Error e ⇒ dummy_state_pc
    5281  ].
    53 cases daemon qed.
    54 
    55 definition sigma_sb_state_pc : ertlptr_program → (block → label → list label) →
    56  (block → label → list register) → state_pc LTL_semantics → state_pc ERTLptr_semantics ≝
    57 λprog,f_lbls,f_regs,st.
     82
     83definition sigma_sb_state_pc :fixpoint_computer → coloured_graph_computer → 
     84ertlptr_program → (block → label → list label) →
     85(block → label → list register) → state_pc LTL_semantics → state_pc ERTLptr_semantics ≝
     86λfix_comp,build,prog,f_lbls,f_regs,st.
    5887let ge ≝ globalenv_noinit … prog in
    5988let globals ≝ prog_var_names … prog in
    6089match fetch_internal_function … ge (pc_block (pc … st)) with
    61   [ OK y ⇒ ?
     90  [ OK y ⇒ 
     91     let after ≝ (analyse_liveness fix_comp (prog_var_names … prog) (\snd y)) in
     92     let coloured_graph ≝ build … (\snd y) after in
     93     mk_state_pc ? (sigma_sb_state prog f_lbls f_regs
     94                          (to_be_cleared_sb after coloured_graph) st) (pc … st) 
     95                          (sigma_stored_pc prog f_lbls (last_pop … st))
    6296  | Error e ⇒ dummy_state_pc
    6397  ].
    64 cases daemon qed.
     98
     99axiom write_decision : decision → beval → state LTL_LIN_state →
     100state LTL_LIN_state.
     101
     102axiom read_arg_decision : arg_decision → state LTL_LIN_state → beval.
     103
     104axiom insensitive_to_be_cleared_sb : ∀prog. ∀f_lbls : (block → label → list label).
     105∀f_regs : (block → label → list register).∀tb : clear_sb_type.
     106∀st : state LTL_LIN_state.∀lab.
     107∀d : decision.∀bv.tb lab d →
     108sigma_sb_state prog f_lbls f_regs tb st =
     109sigma_sb_state prog f_lbls f_regs tb (write_decision d bv st).
    65110
    66111
     
    82127         (λs1:ERTLptr_status ? ?
    83128          .λs2:LTL_status ? ?
    84            .sigma_fb_state_pc prog f_lbls f_regs s1
    85             =sigma_sb_state_pc prog f_lbls f_regs s2)
     129           .sigma_fb_state_pc fix_comp prog f_lbls f_regs s1
     130            =sigma_sb_state_pc fix_comp colour prog f_lbls f_regs s2)
    86131    (* call_rel ≝ *) 
    87132       (λs1:Σs:ERTLptr_status ??.as_classifier ? s cl_call
     
    121166*)
    122167
    123 lemma set_no_pc_eta:
    124  ∀P.∀st1: state_pc P. set_no_pc P st1 st1 = st1.
    125 #P * //
    126 qed.
    127 
    128 lemma pc_of_label_eq :
    129   ∀p,p'.let pars ≝ mk_sem_graph_params p p' in
    130   ∀globals,ge,bl,i_fn,lbl.
    131   fetch_internal_function ? ge bl = return i_fn →
    132   pc_of_label pars globals ge bl lbl =
    133     OK ? (pc_of_point ERTL_semantics bl lbl).
    134 #p #p' #globals #ge #bl #i_fn #lbl #EQf
    135 whd in match pc_of_label;
    136 normalize nodelta >EQf >m_return_bind %
    137 qed.
    138168
    139169lemma eq_OK_OK_to_eq: ∀T,x,y. OK T x = OK T y → x=y.
     
    151181pc_block (pc … st1) = pc_block (pc … st2).
    152182
     183
    153184axiom pc_eq_sigma_commute : ∀fix_comp,colour.
    154185∀prog.∀ f_lbls,f_regs.∀f_bl_r.
    155186∀ good :b_graph_transform_program_props ERTLptr_semantics LTL_semantics
    156187     (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs.
    157 ∀st1,st2.
     188∀st1,st2,f,fn,stmt.
     189fetch_statement ERTLptr_semantics (prog_var_names … prog) (globalenv_noinit … prog)
     190                (pc … st1) = return 〈f,fn,stmt〉 →
    158191let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good) in
    159192R st1 st2 →
     
    184217include "joint/semantics_blocks.ma".
    185218include "ASM/Util.ma".
     219include "joint/StatusSimulationHelper.ma".
     220
     221
     222axiom hw_reg_retrieve_write_decision_hit : ∀r : Register.∀bv : beval.
     223∀st : state LTL_LIN_state.
     224hw_reg_retrieve (regs … (write_decision r bv st)) r = return bv.
     225
     226axiom move_spec : ∀prog.∀stack_size.∀localss : nat.
     227∀ carry_lives_after : bool.∀dest : decision.∀src : arg_decision.
     228∀f : ident.
     229∀s : state LTL_LIN_state.
     230repeat_eval_seq_no_pc (mk_prog_params LTL_semantics prog stack_size) f
     231   (move (prog_var_names … prog) localss carry_lives_after dest src) s =
     232   return write_decision dest (read_arg_decision src s) s.
     233
     234axiom sigma_beval : ertlptr_program → (block → label → list label) →
     235                    beval → beval.
     236 
     237
     238axiom ps_reg_retrieve_hw_reg_retrieve_commute :
     239∀fix_comp,colour,prog.
     240∀ f_lbls,f_regs.∀f_bl_r.
     241∀ good :b_graph_transform_program_props ERTLptr_semantics LTL_semantics
     242 (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs.
     243∀fn : joint_closed_internal_function ERTLptr (prog_var_names … prog).
     244let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good) in
     245let after ≝ (analyse_liveness fix_comp (prog_var_names … prog) fn) in
     246∀st1 : state_pc ERTL_state.
     247∀st2 : state_pc LTL_LIN_state.
     248∀bv.
     249∀r : register.R st1 st2 →
     250lives (inl ? ? r) (livebefore  … fn (point_of_pc ERTLptr_semantics (pc … st1)) after) →
     251ps_reg_retrieve (regs … st1) r = return bv →
     252∃bv'.bv = sigma_beval prog f_lbls bv' ∧
     253read_arg_decision (colouring after (colour (prog_var_names … prog) fn after)
     254                                            (inl register Register r))
     255                              st2 = bv'.
     256                             
     257axiom set_member_empty :∀A.∀DEC.∀a.¬set_member A DEC a (set_empty …).   
     258axiom set_member_singl : ∀A,DEC,a.set_member A DEC a (set_singleton … a).
     259axiom set_member_union1 : ∀A,DEC,x,y,a.set_member A DEC a x →
     260set_member A DEC a (set_union … x y).
     261axiom set_member_union2 : ∀A,DEC,x,y,a.set_member A DEC a y →
     262set_member A DEC a (set_union … x y).
     263axiom set_member_diff : ∀A,DEC,x,y,a.set_member A DEC a x →
     264¬set_member A DEC a y →
     265set_member A DEC a (set_diff … x y).
     266
     267
     268lemma all_used_are_live_before :
     269∀fix_comp.
     270∀prog : ertlptr_program.
     271∀fn : joint_closed_internal_function ERTLptr (prog_var_names … prog).
     272∀l,stmt.
     273stmt_at … (joint_if_code … fn) l = return stmt →
     274∀r : register. set_member ? (eq_identifier …) r (\fst (used ? stmt)) →
     275let after ≝ (analyse_liveness fix_comp (prog_var_names … prog) fn) in
     276eliminable ? (after l) stmt = None ? →
     277lives (inl ? ? r)  (livebefore  … fn l after).
     278#fix_comp #prog #fn #l *
     279[ * [#c|* [#c_id | #c_ptr] #args #dest | #a #lbl | *
     280[ #str
     281| * * [#r1 | #R1]  * [1,3: * [1,3: #r |2,4: #R] |2,4: #b]
     282| #a
     283| * [ #r | #b]
     284| #i #i_spec #dpl #dph
     285| #op #a #b * [#r | #by]  * [1,3: #r'|2,4: #by']
     286| #op #a #a'
     287| * #a #a' * [1,3,5,7,9,11: #r |2,4,6,8,10,12: #b]
     288|
     289|
     290| #a #dpl #dph
     291| #dpl #dph #a
     292| * [ * [|| #r] | #r #lbl | #r #lbl ]
     293]
     294] #nxt| * [ #lbl | | *] |*]
     295#EQstmt #r #H #H1 whd in match (lives ??); normalize  nodelta
     296whd in match (livebefore ????); whd in EQstmt : (??%?); >EQstmt
     297normalize nodelta -EQstmt whd in match (statement_semantics ???);
     298whd in match(\fst ?); try( @(set_member_union2) assumption) >H1
     299normalize nodelta whd in match(\fst ?); @(set_member_union2) assumption
     300qed.
     301
     302axiom bool_of_beval_sigma_commute :
     303∀prog.∀f_lbls.∀bv,b.
     304bool_of_beval (sigma_beval prog f_lbls bv) = return b →
     305bool_of_beval bv = return b.
     306
     307lemma map_eval_add_dummy_variance_id :
     308∀X,Y.∀l,x.map_eval X Y (add_dummy_variance X Y l) x =l.
     309#X #Y #l elim l [//] #hd #tl normalize #IH #x >IH %
     310qed.
     311
     312lemma state_pc_eq : ∀p.∀st1,st2 : state_pc p.
     313st1 = st2 → st_no_pc … st1 = st_no_pc … st2 ∧
     314pc … st1 = pc … st2 ∧ last_pop … st1 = last_pop … st2.
     315#p * #st1 #pc1 #lp1 * #st2 #pc2 #lp2 #EQ destruct(EQ)
     316%{(refl …)} %{(refl …)} %
     317qed.
     318(*
     319axiom dead_is_to_be_clear :
     320*)
     321
     322(* Cut&paste da un altro file con nome split_on_last_append, unificare*)
     323lemma split_on_last_append_singl : ∀A : Type[0]. ∀pre : list A.
     324∀ last : A. split_on_last ? (pre@[last]) = return 〈pre,last〉.
     325#A #pre elim pre [#last %] #a #tl #IH #last whd in ⊢ (??%?);lapply(IH last)
     326whd in ⊢ (??%? → ?); #EQ >EQ %
     327qed.
     328
     329lemma split_on_last_append : ∀A : Type[0]. ∀l1,l2: list A.
     330 OptPred True (λres.
     331  split_on_last ? (l1@l2) = return 〈l1 @ \fst res, \snd res〉)
     332  (split_on_last … l2).
     333#A #l1 #l2 lapply l1 -l1 @(list_elim_left … l2) //
     334#hd #tl #IH #l1 whd >split_on_last_append_singl whd
     335<associative_append @split_on_last_append_singl
     336qed.
     337
     338lemma make_ERTLptr_To_LTL_good_state_relation :
     339∀fix_comp,colour,prog.
     340let p_out ≝ (\fst (\fst (ertlptr_to_ltl fix_comp colour prog))) in
     341let m ≝ (\snd (\fst (ertlptr_to_ltl fix_comp colour prog))) in
     342let n ≝ \snd (ertlptr_to_ltl fix_comp colour prog) in
     343let stacksizes ≝ lookup_stack_cost … m in
     344∃init_regs : block → list register.
     345∃f_lbls : block → label → list label.
     346∃f_regs : block → label → list register.
     347∃good : b_graph_transform_program_props ERTLptr_semantics LTL_semantics
     348        (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)»)
     349        prog init_regs f_lbls f_regs.
     350good_state_relation ERTLptr_semantics LTL_semantics prog stacksizes
     351 (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)»)
     352 (sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good)).
     353#fix_comp #colour #prog
     354cases(make_b_graph_transform_program_props ERTLptr_semantics LTL_semantics
     355          (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog)
     356#init_regs * #f_lbls * #f_regs #good %{init_regs} %{f_lbls} %{f_regs} %{good}
     357%
     358[ #st1 #st2 #f #fn #stmt #Rst1st2 #EQstmt >(pc_eq_sigma_commute … good … EQstmt Rst1st2) %
     359| #st1 #st2 #f #fn #stmt #EQstmt #Rst1St2 >(as_label_ok … good … Rst1St2 EQstmt) %
     360| normalize nodelta whd in ⊢ (% → % → % → ?); #st1 #st1' #st2 #f #fn #a #ltrue #lfalse
     361  #EQfetch whd in match eval_state in ⊢ (% → ?); whd in match eval_statement_no_pc;
     362  normalize nodelta
     363  >EQfetch >m_return_bind normalize nodelta >m_return_bind
     364  whd in match eval_statement_advance; normalize nodelta
     365  change with (ps_reg_retrieve ??) in match (acca_retrieve ?????);
     366  #H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H
     367  #bv >set_no_pc_eta #EQbv #H @('bind_inversion H) -H * #EQbool normalize nodelta
     368  cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt
     369  [ whd in match goto; normalize nodelta >(pc_of_label_eq … EQfn)
     370    >m_return_bind ] whd in ⊢ (??%% → ?); #EQ destruct(EQ) #Rst1st2
     371  #t_fn1 #EQt_fn1 whd normalize nodelta
     372  letin trans_prog ≝ (b_graph_transform_program ????)
     373  letin stacksizes ≝ (lookup_stack_cost ?)
     374  letin prog_pars_in ≝ (mk_prog_params ERTLptr_semantics ??)
     375  letin prog_pars_out ≝ (mk_prog_params LTL_semantics ??) %{(refl …)}
     376  #mid #EQmid
     377  letin st2_pre_mid_no_pc ≝
     378  (write_decision RegisterA
     379          (read_arg_decision
     380              (colouring
     381                  (analyse_liveness fix_comp (globals prog_pars_in) fn)
     382                  (colour (globals prog_pars_in) fn
     383                  (analyse_liveness fix_comp (globals prog_pars_in) fn))
     384              (inl register Register a)) st2) st2)
     385  %{st2_pre_mid_no_pc}
     386  %
     387  [1,3: >map_eval_add_dummy_variance_id @move_spec]
     388  % [1,3: % %] %{(mk_state_pc ? st2_pre_mid_no_pc
     389                       (pc_of_point LTL_semantics (pc_block (pc … st2)) ?)
     390                        (last_pop … st2))} [@ltrue |3: @lfalse]
     391  change with prog_pars_out in match (mk_prog_params ???); %
     392  [1,3: whd in match eval_state; whd in match eval_statement_no_pc;
     393        whd in match fetch_statement; normalize nodelta
     394       >EQt_fn1 >m_return_bind >point_of_pc_of_point >EQmid >m_return_bind
     395        normalize nodelta >m_return_bind
     396        change with prog_pars_out in match (mk_prog_params ???);
     397        whd in match eval_statement_advance; normalize nodelta
     398        change with (hw_reg_retrieve ??) in match (acca_retrieve ?????);
     399        whd in match set_no_pc; normalize nodelta
     400        >hw_reg_retrieve_write_decision_hit >m_return_bind
     401        cases(ps_reg_retrieve_hw_reg_retrieve_commute fix_comp colour prog … good fn … Rst1st2 … EQbv)
     402        [2,4: @(all_used_are_live_before … EQstmt)
     403            [1,3: @set_member_singl |*: % ] ] #bv' * #EQbv' #EQbv1
     404        change with (prog_var_names … prog) in match (globals ?); >EQbv1
     405        >EQbv' in EQbool; #EQbool
     406        >(bool_of_beval_sigma_commute prog f_lbls … EQbool) >m_return_bind
     407        normalize nodelta [2: %] whd in match goto; normalize nodelta
     408        >(pc_of_label_eq … EQt_fn1) %
     409  |2,4: whd whd in match sigma_fb_state_pc; normalize nodelta
     410        whd in match sigma_sb_state_pc; normalize nodelta
     411        change with (pc_block (pc … st1)) in match (pc_block ?);
     412        cases(fetch_statement_inv … EQfetch) #EQfn #_ >EQfn
     413        normalize nodelta <(pc_eq_sigma_commute … good … EQfetch Rst1st2)
     414        change with (pc_block (pc … st1)) in ⊢ (???match (???%) with [_⇒ ? | _ ⇒ ?]);
     415        >EQfn normalize nodelta
     416        lapply Rst1st2 whd in ⊢ (% → ?); whd in match sigma_fb_state_pc;
     417         whd in match sigma_sb_state_pc; normalize nodelta >EQfn
     418         <(pc_eq_sigma_commute … good … EQfetch Rst1st2) >EQfn normalize nodelta
     419         #EQ cases(state_pc_eq … EQ) * #EQst1st2 #EQpc #EQlp @eq_f3
     420        [3,6:  assumption
     421        |2,5: %
     422        |*: <(insensitive_to_be_cleared_sb … prog f_lbls f_regs … st2 …
     423               (point_of_pc ERTLptr_semantics (pc … st2)))
     424            [2,4: @dead_registers_in_dead @acc_is_dead ]
     425            assumption
     426        ]
     427  ]
     428| letin p_in ≝ (mk_prog_params ERTLptr_semantics ??)
     429  letin p_out ≝ (mk_prog_params LTL_semantics ??)
     430  letin trans_prog ≝ (b_graph_transform_program ????)
     431  #st1 #st1' #st2 #f #fn *
     432  [7: #op1 #dest #src #nxt #EQfetch whd in match eval_state in ⊢ (% → ?);
     433      normalize nodelta >EQfetch >m_return_bind #H @('bind_inversion H) -H
     434      #st1_no_pc whd in match eval_statement_no_pc in ⊢ (% → ?); normalize nodelta
     435      whd in match eval_seq_no_pc; normalize  nodelta
     436      #H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H
     437      #bv #EQbv #H @('bind_inversion H) -H #bv_op1 #EQbv_op1 #EQst1_no_pc
     438      whd in match eval_statement_advance; normalize nodelta
     439      whd in ⊢ (??%% → ?); #EQ destruct(EQ)
     440      whd in ⊢ (% → ?); #Rst1st2 #t_fn #EQt_fn
     441      whd normalize nodelta whd in match translate_op1;
     442      normalize nodelta
     443      change with p_out in match p_out;
     444      change with p_in in match p_in;
     445      change with trans_prog in match trans_prog;
     446      #mid #mid1 #EQmid % [%]
     447      [ cases (andb ??) whd in match (preserve_carry_bit ???);
     448        whd in match ensure_step_block; normalize nodelta
     449        XXX
     450     
     451     
     452      whd normalize nodelta
     453      change with p_out in match p_out;
     454      change with p_in in match p_in;
     455      change with trans_prog in match trans_prog;
     456      letin coloured_dst ≝ (colouring ???)
     457      letin coloured_src ≝ (colouring ???)
     458      whd in match translate_op1; normalize nodelta
     459
     460
     461
     462      whd in match (translate_op1 ?????);
     463      change with (bind_new_P' ? (? × ?) ?
     464       (f_step ERTLptr_semantics ?????));
     465      whd in match (translate_data ????);
     466      change with (bind_new_P' ??? (f_step ??????));
     467      whd in match (f_step ??????);
     468      @(λH.H)
     469     
     470      whd in match (  #mid whd #
     471 
     472
     473qed.
     474
    186475
    187476lemma eval_cond_ok :
     
    209498bool_to_Prop (taaf_non_empty … taf).
    210499#fix_comp #colour #prog #f_lbls #f_regs #f_bl_r #good #st1 #st2 #st1' #f #fn #a
    211 #ltrue #lfalse #Rst1st2 #EQfetch
     500#ltrue #lfalse #Rst1st2 #EQfetch #EQeval
     501letin R ≝ (sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good))
     502@(general_eval_cond_ok … good … Rst1st2 EQfetch EQeval)
     503%
     504[ #st1 #st2 #Rst1St2 >(pc_eq_sigma_commute … good … Rst1St2) %
     505| #st1 #st2 #f #fn #stmt #EQstmt #Rst1St2 >(as_label_ok … good … Rst1St2 EQstmt) %
     506|
     507
     508
     509
    212510whd in match eval_state; normalize nodelta
    213511>EQfetch >m_return_bind
  • src/ERTLptr/liveness.ma

    r2700 r2883  
    2626    〈set_empty …, set_singleton … r〉.
    2727
    28 definition rl_join: register_lattice → register_lattice → register_lattice ≝
    29   λleft.
    30   λright.
    31   let 〈lp, lh〉 ≝ left in
    32   let 〈rp, rh〉 ≝ right in
    33     〈set_union … lp rp, set_union … lh rh〉.
     28definition pairwise : ∀A,B : Type[0]. ∀f : A → A → A. ∀g: B → B → B.
     29A × B → A × B → A × B≝
     30λA,B,f,g,c1,c2.〈f (\fst c1) (\fst c2) , g (\snd c1) (\snd c2)〉.
     31
     32definition rl_join: register_lattice → register_lattice → register_lattice ≝
     33pairwise ?? (set_union …) (set_union …).
    3434
    3535definition rl_diff: register_lattice → register_lattice → register_lattice ≝
    36   λleft.
    37   λright.
    38   let 〈lp, lh〉 ≝ left in
    39   let 〈rp, rh〉 ≝ right in
    40     〈set_diff … lp rp, set_diff … lh rh〉.
     36pairwise ?? (set_diff …) (set_diff …).
    4137
    4238definition defined ≝
  • src/joint/StatusSimulationHelper.ma

    r2863 r2883  
    4444 @Hr
    4545]
    46 qed.
    47 
    48 check joint_classify
    49 check as_label
     46qed.
     47
     48
     49definition step_to_seq : ∀p : prog_params.∀stmt : joint_step p (globals p).
     50joint_classify_step p stmt = cl_other →
     51(∀c.stmt ≠ COST_LABEL ?? c) → Σ seq.stmt = step_seq ?? seq ≝
     52λp,stmt,CL_OTHER,COST.
     53(match stmt return λx.x = stmt → ? with
     54[ COST_LABEL c ⇒ λprf.⊥
     55| CALL id args dest ⇒ λprf.⊥
     56| COND r lab ⇒ λprf.⊥
     57| step_seq seq ⇒ λprf.«seq,?»
     58])(refl …).
     59@hide_prf
     60[ lapply(COST c) * #H @H >prf %
     61|2,3: <prf in CL_OTHER; whd in match (joint_classify_step ??); #EQ destruct(EQ)
     62| >prf %
     63]
     64qed.
     65 
    5066
    5167record good_state_relation (P_in : sem_graph_params)
     
    5975                                stack_sizes)
    6076        → Prop) : Prop ≝
    61 { pc_eq_sigma_commute : ∀st1,st2.R st1 st2 → pc … st1 = pc … st2
     77{ pc_eq_sigma_commute : ∀st1,st2,f,fn,stmt.R st1 st2 →
     78                 fetch_statement ? (prog_var_names … prog)
     79                     (globalenv_noinit … prog) (pc … st1)  = return 〈f,fn,stmt〉 →
     80                 pc … st1 = pc … st2
    6281; as_label_ok : ∀st1 : joint_abstract_status (mk_prog_params P_in prog stack_sizes).
    6382                ∀st2 : joint_abstract_status ?.
     
    7089    ∀st1,st1' : joint_abstract_status (mk_prog_params P_in prog stack_sizes) .
    7190    ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes).
    72     ∀f,fn,a,ltrue,lfalse.
    73     eval_state P_in (prog_var_names … ℕ prog) (ev_genv … (mk_prog_params P_in prog stack_sizes))
    74     st1 = return st1' →
     91    ∀f,fn,a,ltrue,lfalse.
    7592    let cond ≝ (COND P_in ? a ltrue) in
    7693    fetch_statement P_in … (ev_genv … (mk_prog_params P_in prog stack_sizes)) (pc … st1) =
    77     return 〈f, fn,  sequential … cond lfalse〉 →
     94    return 〈f, fn,  sequential … cond lfalse〉 → 
     95    eval_state P_in (prog_var_names … ℕ prog) (ev_genv … (mk_prog_params P_in prog stack_sizes))
     96    st1 = return st1' →
    7897    R st1 st2 →
    7998    ∀t_fn.
     
    82101    bind_new_P' ??
    83102     (λregs1.λdata.bind_new_P' ??
    84      (λregs2.λblp.
    85         ∀mid,nxt1.
     103     (λregs2.λblp.(\snd blp) = [ ] ∧
     104        ∀mid.
    86105          stmt_at ? (prog_var_names … trans_prog) (joint_if_code ?? t_fn) mid
    87           = return sequential P_out ? ((\snd (\fst blp)) mid) nxt1
     106          = return sequential P_out ? ((\snd (\fst blp)) mid) lfalse
    88107         ∃st2_pre_mid_no_pc.
    89108            repeat_eval_seq_no_pc (mk_prog_params P_out trans_prog stack_sizes) f (map_eval ?? (\fst (\fst blp)) mid)
     
    95114                                ((\snd (\fst blp)) mid)  = cl_jump ∧
    96115            cost_label_of_stmt (mk_prog_params P_out trans_prog stack_sizes)
    97                                (sequential P_out ? ((\snd (\fst blp)) mid) nxt1) = None ? ∧
    98             (\snd blp) = [ ] ∧
     116                               (sequential P_out ? ((\snd (\fst blp)) mid) lfalse) = None ? ∧
    99117            ∃st2_mid .
    100118                eval_state P_out (prog_var_names … trans_prog)
     
    103121   )  (f_step … data (point_of_pc P_in (pc … st1)) cond)   
    104122  ) (init ? fn)
     123; seq_commutation :
     124  let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
     125  ∀st1,st1' : joint_abstract_status (mk_prog_params P_in prog stack_sizes) .
     126  ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes).
     127  ∀f,fn,stmt,nxt.
     128  let seq ≝ (step_seq P_in ? stmt) in
     129  fetch_statement P_in … (ev_genv … (mk_prog_params P_in prog stack_sizes)) (pc … st1) =
     130  return 〈f, fn,  sequential … seq nxt〉 → 
     131  eval_state P_in (prog_var_names … ℕ prog) (ev_genv … (mk_prog_params P_in prog stack_sizes))
     132  st1 = return st1' →
     133  R st1 st2 →
     134  ∀t_fn.
     135  fetch_internal_function … (globalenv_noinit … trans_prog) (pc_block (pc … st2)) =
     136  return 〈f,t_fn〉 →
     137  bind_new_P' ??
     138     (λregs1.λdata.bind_new_P' ??
     139     (λregs2.λblp.
     140           ∀mid,mid1.
     141            stmt_at ? (prog_var_names … trans_prog) (joint_if_code ?? t_fn) mid
     142            = return sequential P_out ? ((\snd (\fst blp)) mid) mid1→
     143            ∃CL_OTHER : joint_classify_step (mk_prog_params P_out trans_prog stack_sizes)
     144                          ((\snd (\fst blp)) mid)  = cl_other.
     145            ∃COST : cost_label_of_stmt (mk_prog_params P_out trans_prog stack_sizes)
     146                         (sequential P_out ? ((\snd (\fst blp)) mid) mid1) = None ?.
     147            ∃st2_fin_no_pc.
     148            let pre ≝ (map_eval ?? (\fst (\fst blp)) mid) in
     149            let middle ≝ [pi1 ?? (step_to_seq (mk_prog_params P_out trans_prog stack_sizes)
     150                                  ((\snd (\fst blp)) mid) CL_OTHER ?)] in
     151           repeat_eval_seq_no_pc (mk_prog_params P_out trans_prog stack_sizes) f
     152              (pre@ middle @ (\snd blp))  (st_no_pc … st2)= return st2_fin_no_pc ∧
     153           let st2_fin ≝
     154           mk_state_pc ? st2_fin_no_pc
     155                         (pc_of_point P_out (pc_block(pc … st2)) nxt)
     156                         (last_pop … st2) in
     157           R st1' st2_fin) (f_step ??? data (point_of_pc P_in (pc … st1)) seq)
     158      ) (init ? fn)         
    105159}.
    106 
     160@hide_prf #c % #EQ >EQ in COST; whd in ⊢ (??%% → ?); #EQ destruct(EQ)
     161qed.
    107162
    108163lemma general_eval_cond_ok : ∀ P_in , P_out: sem_graph_params.
     
    135190#f #fn #a #ltrue #lfalse #Rst1st2 #EQfetch #EQeval #n_costed
    136191cases(b_graph_transform_program_fetch_statement … good … EQfetch)
    137 #init_data * #t_fn1 **  >(pc_eq_sigma_commute … goodR … Rst1st2)
     192#init_data * #t_fn1 **  >(pc_eq_sigma_commute … goodR … Rst1st2 EQfetch)
    138193#EQt_fn1 whd in ⊢ (% → ?); #Hinit
    139194* #labs * #regs
     
    142197[ @eq_identifier_elim [2: #_ *] whd in match point_of_pc; normalize nodelta
    143198  whd in match (point_of_offset ??); #ABS #_ lapply(fetch_statement_inv … EQfetch)
    144   * #_ >(pc_eq_sigma_commute … goodR … Rst1st2) whd in match point_of_pc;
     199  * #_ >(pc_eq_sigma_commute … goodR … Rst1st2 EQfetch) whd in match point_of_pc;
    145200  normalize nodelta whd in match (point_of_offset ??); <ABS
    146201  cases(entry_is_cost … (pi2 ?? fn)) #nxt1 * #c #EQ >EQ #EQ1 destruct(EQ1)
    147202]
    148 #_ <(pc_eq_sigma_commute … goodR … Rst1st2) #EQbl whd in ⊢ (% → ?); * #l1 * #mid1
     203#_ <(pc_eq_sigma_commute … goodR … Rst1st2 EQfetch) #EQbl whd in ⊢ (% → ?); * #l1 * #mid1
    149204* #mid2 * #l2 *** #EQmid1 whd in ⊢ (% → ?); #seq_pre_l whd in ⊢ (% → ?); * #nxt1
    150205* #EQmid change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ)
    151 cases(bind_new_bind_new_instantiates … EQbl
    152             (bind_new_bind_new_instantiates … Hinit
    153                (cond_commutation … goodR … EQeval EQfetch Rst1st2 t_fn1 EQt_fn1))
    154             … EQmid)   
    155 #st_pre_mid_no_pc * #EQst_pre_mid_no_pc *** #CL_JUMP #COST #EQ destruct(EQ) *
    156 #st2_mid * #EQst2mid #Hst2_mid whd in ⊢(% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2)
    157 %{st2_mid} %{Hst2_mid}
    158 >(pc_eq_sigma_commute … goodR … Rst1st2) in seq_pre_l; #seq_pre_l
     206cases(bind_new_bind_new_instantiates … EQbl (bind_new_bind_new_instantiates … Hinit
     207               (cond_commutation … goodR … EQfetch EQeval Rst1st2 t_fn1 EQt_fn1)))
     208#EQ destruct(EQ) #APP whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2)
     209cases(APP … EQmid) -APP
     210#st_pre_mid_no_pc * #EQst_pre_mid_no_pc ** #CL_JUMP #COST *
     211#st2_mid * #EQst2mid #Hst2_mid %{st2_mid} %{Hst2_mid}
     212>(pc_eq_sigma_commute … goodR … Rst1st2 EQfetch) in seq_pre_l; #seq_pre_l
    159213lapply(taaf_to_taa ???
    160214           (produce_trace_any_any_free ? st2 f t_fn1 ??? st_pre_mid_no_pc EQt_fn1
     
    174228qed.
    175229
     230(*
     231let rec taa_to_taaf  S st1 st2 (taa : trace_any_any S st1 st2) on taa :
     232trace_any_any_free S st1 st2 ≝
     233(match taa in trace_any_any return λs1,s2.λx.st1 = s1 → st2 = s2 → taa ≃ x → trace_any_any_free S s1 s2 with
     234[taa_base st1' ⇒ λprf.?
     235|taa_step st1' st2' st3' H I J tl ⇒ λprf.?
     236]) (refl … st1) (refl … st2) (refl_jmeq ? taa).
     237*)
     238
     239lemma general_eval_seq_no_call_ok : ∀ P_in , P_out: sem_graph_params.
     240∀prog : joint_program P_in.
     241∀stack_sizes.
     242∀ f_lbls,f_regs.∀f_bl_r.∀init.
     243∀good : b_graph_transform_program_props P_in P_out init prog f_bl_r f_lbls f_regs.
     244let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in
     245let trans_prog  ≝ b_graph_transform_program P_in P_out init prog in
     246let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in
     247∀ R : joint_abstract_status prog_pars_in → joint_abstract_status prog_pars_out → Prop.
     248good_state_relation P_in P_out prog stack_sizes init R →
     249∀st1,st1' : joint_abstract_status prog_pars_in.
     250∀st2 : joint_abstract_status prog_pars_out.
     251∀f.
     252∀fn : joint_closed_internal_function P_in (prog_var_names … prog).
     253∀stmt,nxt.
     254R st1 st2 →
     255    let seq ≝ (step_seq P_in ? stmt) in
     256 fetch_statement P_in …
     257  (globalenv_noinit ? prog) (pc … st1) =
     258    return 〈f, fn,  sequential ?? seq nxt〉 →
     259 eval_state P_in (prog_var_names … ℕ prog) (ev_genv … prog_pars_in)
     260            st1 = return st1' →
     261∃st2'. R st1' st2' ∧           
     262∃taf : trace_any_any_free (joint_abstract_status prog_pars_out) st2 st2'.           
     263 if taaf_non_empty … taf then True else  (*IT CAN BE SIMPLIFIED *)
     264(¬as_costed (joint_abstract_status (mk_prog_params P_in prog stack_sizes)) st1 ∨
     265 ¬as_costed (joint_abstract_status (mk_prog_params P_in prog stack_sizes)) st1').
     266#P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_bl_r #init #good #R #goodR #st1 #st1'
     267#st2 #f #fn #stmt #nxt #Rst1st2 #EQfetch #EQeval
     268cases(b_graph_transform_program_fetch_statement … good … EQfetch)
     269#init_data * #t_fn ** >(pc_eq_sigma_commute … goodR … Rst1st2 EQfetch)
     270#EQt_fn #Hinit * #labs * #regs ** #EQlabs #EQregs normalize nodelta ***
     271#blp #blm #bls * @if_elim
     272[ @eq_identifier_elim [2: #_ *] whd in match point_of_pc; normalize nodelta
     273  whd in match (point_of_offset ??); #ABS #_ lapply(fetch_statement_inv … EQfetch)
     274  * #_ >(pc_eq_sigma_commute … goodR … Rst1st2 EQfetch) whd in match point_of_pc;
     275  normalize nodelta whd in match (point_of_offset ??); <ABS
     276  cases(entry_is_cost … (pi2 ?? fn)) #nxt1 * #c #EQ >EQ #EQ1 destruct(EQ1)
     277]
     278#_ <(pc_eq_sigma_commute … goodR … Rst1st2 EQfetch) #EQbl
     279>(pc_eq_sigma_commute … goodR … Rst1st2 EQfetch) #SBiC lapply SBiC
     280whd in ⊢ (% → ?); * #l1 * #mid1 * #mid2 * #l2 *** #EQmid1 whd in ⊢ (% → ?);
     281#_ whd in ⊢ (% → ?); * #nxt1 * #EQmid change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ)
     282#_
     283cases(bind_new_bind_new_instantiates … EQbl (bind_new_bind_new_instantiates … Hinit
     284               (seq_commutation … goodR … EQfetch EQeval Rst1st2 t_fn EQt_fn)))
     285[4: @EQmid |*:] #COST * #CL_OTHER * #st2_fin_no_pc normalize nodelta cases(step_to_seq ????)
     286    #seq_mid cases daemon (*TODO*)
     287    qed.
     288   
     289(*   
     290    cases(blm mid1) in
     291#stmt_at_middle #EQstmt_at_middle normalize nodelta * >EQstmt_at_middle in SBiC;  destruct(EQ) whd in ⊢ (??%% → ?);#EQ destruct(EQ)
     292
     293
     294* #EQst2_pre_mid_no_pc
     295* #st2_mid * #EQst2_mid * #st2_fin_no_pc * #EQst2_fin_no_pc #Hfin
     296%{(mk_state_pc ? st2_fin_no_pc (pc_of_point P_out (pc_block (pc … st2)) nxt) (last_pop … st2))}
     297%{Hfin}
     298lapply(taaf_to_taa ???
     299           (produce_trace_any_any_free ? st2 f t_fn ??? st2_pre_mid_no_pc EQt_fn
     300                                       seq_pre_l EQst2_pre_mid_no_pc) ?)
     301[ @if_elim #_ [2: @I] % whd in match as_costed; normalize nodelta
     302  whd in match (as_label ??); whd in match fetch_statement; normalize nodelta
     303  >EQt_fn >m_return_bind whd in match (as_pc_of ??); whd in match point_of_pc;
     304  normalize nodelta >point_of_offset_of_point >EQmid >m_return_bind
     305  normalize nodelta >COST * #H @H %]
     306#taa1
     307letin st2_mid_pc ≝ (mk_state_pc ? st2_mid
     308                                (pc_of_point P_out (pc_block (pc … st2)) mid2)
     309                                (last_pop … st2))
     310<(point_of_pc_of_point P_out (pc_block (pc … st2)) mid2) in seq_post_l;
     311#seq_post_l
     312lapply (produce_trace_any_any_free (mk_prog_params P_out ? stack_sizes)
     313                     st2_mid_pc f t_fn ??? st2_fin_no_pc EQt_fn
     314                                       (seq_post_l) EQst2_fin_no_pc)
     315* #taaf2 * #taaf2_prf1 #taaf2_prf2
     316%{(taaf_append_taaf ???? (taaf_step ???? taa1 ??) taaf2 ?)}
     317[ @hide_prf @if_elim [2: #_ %] @andb_elim @if_elim [2: #_ *] #H #_
     318  % whd in match (as_costed ??); whd in match (as_label ??);
     319  whd in match (as_pc_of ??); whd in match fetch_statement; normalize nodelta
     320  >EQt_fn >m_return_bind whd in match point_of_pc; normalize nodelta
     321  >point_of_offset_of_point lapply(taaf2_prf2 H) lapply seq_post_l cases bls
     322  [ #_ *] #stmt1 #tl * #lbl1 * #rest ** #EQ destruct(EQ) * #nxt1 * #EQstmt1
     323  >point_of_pc_of_point change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) #_ #_
     324  >point_of_pc_of_point in EQstmt1; #EQstmt1 >EQstmt1 >m_return_bind normalize nodelta
     325  * #H @H %
     326| @hide_prf whd whd in match eval_state; normalize nodelta whd in match fetch_statement;
     327  normalize nodelta >EQt_fn >m_return_bind >point_of_pc_of_point >EQmid
     328  >m_return_bind >EQst2_mid >m_return_bind whd in match eval_statement_advance;
     329  normalize nodelta lapply COST lapply CL_OTHER lapply EQmid cases(blm mid1)
     330  normalize nodelta
     331  [ #c #_ #_ whd in ⊢ (??%? → ?); #EQ destruct(EQ)
     332  | #id #args #dest #_ whd in ⊢ (??%? → ?); #EQ destruct(EQ)
     333  | #r #lbl #_ whd in ⊢ (??%? → ?); #EQ destruct(EQ)
     334  | #jseq #EQjseq #_ #_ %
     335  ]
     336| @hide_prf whd whd in ⊢ (??%?); whd in match fetch_statement; normalize nodelta >EQt_fn
     337  >m_return_bind >point_of_pc_of_point >EQmid >m_return_bind assumption
     338| @if_elim #_ [%] % % whd in ⊢ (% → ?); * #H @H -H whd in ⊢ (??%?); >EQfetch %
     339]
     340qed.
     341*)
  • src/joint/semantics_blocks.ma

    r2879 r2883  
    146146  seq_list_in_code … (joint_if_code … curr_fn) src b l dst →
    147147  repeat_eval_seq_no_pc p curr_id b st = return st' →
    148   trace_any_any_free (joint_abstract_status p) st
    149     (mk_state_pc ? st' (pc_of_point p (pc_block (pc … st)) dst) (last_pop … st)) ≝
     148  Σtaaf :trace_any_any_free (joint_abstract_status p) st
     149    (mk_state_pc ? st' (pc_of_point p (pc_block (pc … st)) dst) (last_pop … st)).
     150    (not_empty … b ↔ bool_to_Prop (taaf_non_empty … taaf)) ≝
    150151  λp,st,curr_id,curr_fn,b,l,dst,st',prf1,prf2,prf3.
    151152  produce_trace_any_any_free_aux p st curr_id curr_fn b l dst st' prf1 prf2 prf3.
     
    175176  #H #G
    176177  %2{(taa_base …)} assumption
    177 | #hd #tl #_ #EQ <EQ -hd -tl @produce_trace_any_any_free assumption
     178| #hd #tl #_ #EQ <EQ -hd -tl #H1 #H2 @(produce_trace_any_any_free …) assumption
    178179]
    179180qed.
Note: See TracChangeset for help on using the changeset viewer.