Changeset 2930


Ignore:
Timestamp:
Mar 21, 2013, 7:14:38 PM (4 years ago)
Author:
sacerdot
Message:

More progress. Some useless parameters have been removed from the axioms.
Axiom's parameters fixed (they were not inhabited before).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTLptr/ERTLptrToLTLProof.ma

    r2922 r2930  
    2222joint_abstract_status (mk_prog_params LTL_semantics prog stack_sizes).
    2323
    24 definition clear_sb_type ≝ label → decision → bool.
     24definition local_clear_sb_type ≝ decision → bool.
     25definition clear_sb_type ≝ label → local_clear_sb_type.
    2526 
    2627axiom to_be_cleared_sb : 
    2728∀after : valuation register_lattice. coloured_graph after → clear_sb_type.
    2829
    29 definition clear_fb_type ≝ label → vertex → bool.
     30definition local_clear_fb_type ≝ vertex → bool.
     31definition clear_fb_type ≝ label → local_clear_fb_type.
    3032
    3133axiom to_be_cleared_fb :
    3234∀after : valuation register_lattice.clear_fb_type.
    3335
    34 axiom sigma_fb_state: ertlptr_program → (block → label → list label) →
    35  (block → label → list register) →
    36  clear_fb_type → state ERTLptr_semantics → state ERTLptr_semantics.
     36axiom sigma_fb_state:
     37 ertlptr_program → local_clear_fb_type →
     38  state ERTLptr_semantics → state ERTLptr_semantics.
    3739
    3840axiom acc_is_dead : ∀fix_comp.∀prog : ertlptr_program.
     
    4244¬ lives (inr ? ? RegisterA) (livebefore  … fn l after).
    4345
    44 axiom dead_registers_in_dead :  ∀fix_comp.∀build : coloured_graph_computer.
    45 ∀prog : ertlptr_program.
    46 ∀fn : joint_closed_internal_function ERTLptr (prog_var_names … prog).
    47 ∀l.
    48 let after ≝ (analyse_liveness fix_comp (prog_var_names … prog) fn) in
    49 let coloured_graph ≝ build … fn after in
    50 ∀R : Register.
    51 ¬ lives (inr ? ? R) (livebefore  … fn l after) →
    52 to_be_cleared_sb after coloured_graph l R.
    53  
    54 axiom sigma_sb_state: ertlptr_program → (block → label → list label) →
    55  (block → label → list register) → clear_sb_type → state LTL_semantics → state ERTLptr_semantics.
     46axiom dead_registers_in_dead :
     47 ∀fix_comp.∀build : coloured_graph_computer.
     48 ∀prog : ertlptr_program.
     49 ∀fn : joint_closed_internal_function ERTLptr (prog_var_names … prog).
     50 ∀l.
     51 let after ≝ (analyse_liveness fix_comp (prog_var_names … prog) fn) in
     52 let coloured_graph ≝ build … fn after in
     53 ∀R : Register.
     54  ¬ lives (inr ? ? R) (livebefore  … fn l after) →
     55   to_be_cleared_sb after coloured_graph l R.
     56
     57axiom sigma_sb_state:
     58 ertlptr_program → local_clear_sb_type → state LTL_semantics → state ERTLptr_semantics.
    5659
    5760definition dummy_state : state ERTLptr_semantics ≝
     
    6366
    6467
    65 definition sigma_fb_state_pc : fixpoint_computer → ertlptr_program →
    66 (block → label → list label) → (block → label → list register)
    67 state_pc ERTLptr_semantics → state_pc ERTLptr_semantics ≝
    68 λfix_comp,prog,f_lbls,f_regs,st.
    69 let ge ≝ globalenv_noinit … prog in
    70 let globals ≝ prog_var_names … prog in
    71 match fetch_internal_function … ge (pc_block (pc … st)) with
     68definition sigma_fb_state_pc :
     69 fixpoint_computer → ertlptr_program
     70  state_pc ERTLptr_semantics → state_pc ERTLptr_semantics ≝
     71 λfix_comp,prog,st.
     72 let ge ≝ globalenv_noinit … prog in
     73 let globals ≝ prog_var_names … prog in
     74 match fetch_internal_function … ge (pc_block (pc … st)) with
    7275  [ OK y ⇒
    73   let after ≝ (analyse_liveness fix_comp (prog_var_names … prog) (\snd y)) in
    74   mk_state_pc ? (sigma_fb_state prog f_lbls f_regs (to_be_cleared_fb after) st) (pc … st) 
    75                          (last_pop … st)
     76     let pt ≝ point_of_pc ERTLptr_semantics (pc ? st) in
     77     let after ≝ (analyse_liveness fix_comp (prog_var_names … prog) (\snd y)) in
     78     mk_state_pc ? (sigma_fb_state prog (to_be_cleared_fb after pt) st) (pc … st) 
     79      (last_pop … st)
    7680  | Error e ⇒ dummy_state_pc
    7781  ].
     
    7983include "joint/StatusSimulationHelper.ma".
    8084
    81 definition sigma_sb_state_pc :fixpoint_computer → coloured_graph_computer → 
    82 ertlptr_program → (block → label → list label) →
    83 (block → label → list register) → state_pc LTL_semantics → state_pc ERTLptr_semantics ≝
    84 λfix_comp,build,prog,f_lbls,f_regs,st.
    85 let ge ≝ globalenv_noinit … prog in
    86 let globals ≝ prog_var_names … prog in
    87 match fetch_internal_function … ge (pc_block (pc … st)) with
     85definition sigma_sb_state_pc:
     86 fixpoint_computer → coloured_graph_computer → 
     87  ertlptr_program → lbl_funct → state_pc LTL_semantics → state_pc ERTLptr_semantics ≝
     88 λfix_comp,build,prog,f_lbls,st.
     89  let ge ≝ globalenv_noinit … prog in
     90  let globals ≝ prog_var_names … prog in
     91  match fetch_internal_function … ge (pc_block (pc … st)) with
    8892  [ OK y ⇒ 
     93     let pt ≝ point_of_pc ERTLptr_semantics (pc ? st) in
    8994     let after ≝ (analyse_liveness fix_comp (prog_var_names … prog) (\snd y)) in
    9095     let coloured_graph ≝ build … (\snd y) after in
    91      mk_state_pc ? (sigma_sb_state prog f_lbls f_regs
    92                        (to_be_cleared_sb after coloured_graph) st) (pc … st) 
     96     mk_state_pc ? (sigma_sb_state prog
     97                       (to_be_cleared_sb after coloured_graph pt) st) (pc … st) 
    9398                   (sigma_stored_pc ERTLptr_semantics LTL_semantics
    9499                                    prog f_lbls (last_pop … st))
     
    97102
    98103definition state_rel : fixpoint_computer → coloured_graph_computer →
    99 ertlptr_program → (block → label → list label) → (block → label → list register) →
    100 (Σb:block.block_region b = Code) → state ERTL_state → state LTL_LIN_state → Prop ≝
    101 λfix_comp,build,prog,f_lbls,f_regs,bl,st1,st2.
     104ertlptr_program → (Σb:block.block_region b = Code) → label →
     105 state ERTL_state → state LTL_LIN_state → Prop ≝
     106λfix_comp,build,prog,bl,pc,st1,st2.
    102107∃f,fn.fetch_internal_function ? (globalenv_noinit … prog) bl = return 〈f,fn〉 ∧
    103108let after ≝ (analyse_liveness fix_comp (prog_var_names … prog) fn) in
    104109let coloured_graph ≝ build … fn after in
    105 (sigma_fb_state prog f_lbls f_regs (to_be_cleared_fb after) st1) =
    106 (sigma_sb_state prog f_lbls f_regs
    107                        (to_be_cleared_sb after coloured_graph) st2).
    108 
    109 axiom write_decision : decision → beval → state LTL_LIN_state →
    110 state LTL_LIN_state.
     110(sigma_fb_state prog (to_be_cleared_fb after pc) st1) =
     111(sigma_sb_state prog (to_be_cleared_sb after coloured_graph pc) st2).
     112
     113axiom write_decision :
     114 decision → beval → state LTL_LIN_state → state LTL_LIN_state.
    111115
    112116axiom read_arg_decision : arg_decision → state LTL_LIN_state → beval.
    113117
    114 axiom insensitive_to_be_cleared_sb : ∀prog. ∀f_lbls : (block → label → list label).
    115 ∀f_regs : (block → label → list register).∀tb : clear_sb_type.
    116 ∀st : state LTL_LIN_state.∀lab.
    117 ∀d : decision.∀bv.tb lab d →
    118 sigma_sb_state prog f_lbls f_regs tb st =
    119 sigma_sb_state prog f_lbls f_regs tb (write_decision d bv st).
     118axiom insensitive_to_be_cleared_sb :
     119 ∀prog. ∀tb : local_clear_sb_type. ∀st : state LTL_LIN_state.
     120  ∀d : decision.∀bv.tb d →
     121   sigma_sb_state prog tb st =
     122    sigma_sb_state prog tb (write_decision d bv st).
    120123
    121124
     
    124127∀colour : coloured_graph_computer.
    125128∀ prog : ertlptr_program.
    126 ∀ f_lbls. ∀ f_regs. ∀f_bl_r.
     129∀ f_lbls, f_regs. ∀f_bl_r.
    127130b_graph_transform_program_props ERTLptr_semantics LTL_semantics
    128131     (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs →
     
    137140         (λs1:ERTLptr_status ? ?
    138141          .λs2:LTL_status ? ?
    139            .sigma_fb_state_pc fix_comp prog f_lbls f_regs s1
    140             =sigma_sb_state_pc fix_comp colour prog f_lbls f_regs s2)
     142           .sigma_fb_state_pc fix_comp prog s1
     143            =sigma_sb_state_pc fix_comp colour prog f_lbls s2)
    141144    (* call_rel ≝ *) 
    142145       (λs1:Σs:ERTLptr_status ??.as_classifier ? s cl_call
     
    159162      (globalenv_noinit … prog) (pc … st1) = return 〈id,fn,stmt〉 →
    160163as_label ? st2 = as_label ? st1.
    161 
    162 
    163 
    164164
    165165(*
     
    177177*)
    178178
    179 
    180 
    181179axiom pc_block_eq_sigma_commute : ∀fix_comp,colour.
    182180∀prog.∀ f_lbls,f_regs.∀f_bl_r.
     
    187185R st1 st2 →
    188186pc_block (pc … st1) = pc_block (pc … st2).
    189 
    190187
    191188axiom pc_eq_sigma_commute : ∀fix_comp,colour.
     
    237234   return write_decision dest (read_arg_decision src s) s.
    238235
    239 axiom sigma_beval : ertlptr_program → (block → label → list label) →
    240                    beval → beval.
     236axiom sigma_beval:
     237 ertlptr_program → (block → label → list label) → beval → beval.
    241238 
    242239
     
    269266¬set_member A DEC a y →
    270267set_member A DEC a (set_diff … x y).
    271 
    272268
    273269lemma all_used_are_live_before :
     
    351347
    352348axiom sigma_fb_state_insensitive_to_dead_reg:
    353  ∀fix_comp,colour,prog.
    354  let p_in ≝
    355    mk_prog_params ERTLptr_semantics prog
    356    (lookup_stack_cost (\snd  (\fst  (ertlptr_to_ltl fix_comp colour prog)))) in
    357  ∀fn,f_lbls,f_regs,bv.
    358  ∀st: joint_abstract_status p_in.
     349 ∀fix_comp,prog,fn,bv. ∀st: state ERTLptr_semantics. ∀l:label.
    359350 ∀r: register.
    360351 let live ≝
    361   analyse_liveness fix_comp (prog_var_names (joint_function ERTLptr) ℕ prog) fn
    362  in
     352  analyse_liveness fix_comp (prog_var_names (joint_function ERTLptr) ℕ prog) fn in
    363353  set_member (identifier RegisterTag) (eq_identifier RegisterTag) r
    364    (\fst  (live (point_of_pc ERTLptr_semantics (pc p_in st)))) = false →
    365   sigma_fb_state prog f_lbls f_regs
    366    (to_be_cleared_fb live)
     354   (\fst  (live l)) = false →
     355  sigma_fb_state prog
     356   (to_be_cleared_fb live l)
    367357   (set_regs ERTLptr_semantics
    368     〈reg_store r bv (\fst  (regs ERTLptr_semantics (st_no_pc … st))),
    369     \snd  (regs ERTLptr_semantics (st_no_pc … st))〉 (st_no_pc … st))
    370   = sigma_fb_state prog f_lbls f_regs (to_be_cleared_fb live) (st_no_pc … st).
     358    〈reg_store r bv (\fst  (regs ERTLptr_semantics st)),
     359    \snd  (regs ERTLptr_semantics st)〉 st)
     360  = sigma_fb_state prog (to_be_cleared_fb live l) st.
    371361
    372362axiom sigma_fb_state_insensitive_to_dead_Reg:
    373  ∀fix_comp,colour,prog.
    374  let p_in ≝
    375    mk_prog_params ERTLptr_semantics prog
    376    (lookup_stack_cost (\snd  (\fst  (ertlptr_to_ltl fix_comp colour prog)))) in
    377  ∀fn,f_lbls,f_regs,bv.
    378  ∀st: joint_abstract_status p_in.
     363 ∀fix_comp,prog,fn,bv. ∀st: state ERTLptr_semantics. ∀l:label.
    379364 ∀r: Register.
    380365 let live ≝
    381366  analyse_liveness fix_comp (prog_var_names (joint_function ERTLptr) ℕ prog) fn
    382367 in
    383   set_member Register eq_Register r
    384    (\snd  (live (point_of_pc ERTLptr_semantics (pc p_in st)))) = false →
    385   sigma_fb_state prog f_lbls f_regs
    386    (to_be_cleared_fb live)
     368  set_member Register eq_Register r (\snd  (live l)) = false →
     369  sigma_fb_state prog
     370   (to_be_cleared_fb live l)
    387371   (set_regs ERTLptr_semantics
    388      〈\fst  (regs ERTLptr_semantics (st_no_pc … st)),
    389       hwreg_store r bv (\snd  (regs ERTLptr_semantics (st_no_pc … st)))〉
    390       (st_no_pc … st))
    391   = sigma_fb_state prog f_lbls f_regs
    392    (to_be_cleared_fb live) (st_no_pc … st).
     372     〈\fst  (regs ERTLptr_semantics st),
     373      hwreg_store r bv (\snd  (regs ERTLptr_semantics st))〉
     374      st)
     375  = sigma_fb_state prog (to_be_cleared_fb live l) st.
    393376
    394377axiom sigma_fb_state_insensitive_to_dead_carry:
    395  ∀fix_comp,colour,prog.
    396  let p_in ≝
    397    mk_prog_params ERTLptr_semantics prog
    398    (lookup_stack_cost (\snd  (\fst  (ertlptr_to_ltl fix_comp colour prog)))) in
    399  ∀fn,f_lbls,f_regs,bv.
    400  ∀st: joint_abstract_status p_in.
     378 ∀fix_comp,prog,fn,bv. ∀st: state ERTLptr_semantics. ∀l:label.
    401379 let live ≝
    402380  analyse_liveness fix_comp (prog_var_names (joint_function ERTLptr) ℕ prog) fn
    403381 in
    404   set_member Register eq_Register RegisterCarry
    405    (\snd  (live (point_of_pc ERTLptr_semantics (pc p_in st)))) = false →
    406   sigma_fb_state prog f_lbls f_regs
    407   (to_be_cleared_fb live)
    408   (set_carry ERTLptr_semantics bv (st_no_pc … st))
    409   = sigma_fb_state prog f_lbls f_regs (to_be_cleared_fb live) (st_no_pc … st).
     382  set_member Register eq_Register RegisterCarry (\snd (live l)) = false →
     383   sigma_fb_state prog (to_be_cleared_fb live l) (set_carry ERTLptr_semantics bv st) =
     384   sigma_fb_state prog (to_be_cleared_fb live l) st.
    410385
    411386lemma split_orb_false: ∀a,b:bool. orb a b = false → a = false ∧ b = false.
     
    420395   mk_prog_params ERTLptr_semantics prog
    421396   (lookup_stack_cost (\snd  (\fst  (ertlptr_to_ltl fix_comp colour prog)))) in
    422  ∀f,fn,f_lbls,f_regs.
     397 ∀f,fn.
    423398 ∀st1 : joint_abstract_status p_in.
     399 let pt ≝ point_of_pc ERTLptr_semantics (pc ? st1) in
    424400 ∀st1_no_pc,stms.
    425401 ∀Heval_seq_no_pc:
     
    436412    (point_of_pc ERTLptr_semantics (pc p_in st1))) stms
    437413   =true.
    438  (sigma_fb_state prog f_lbls f_regs
     414 (sigma_fb_state prog
    439415  (to_be_cleared_fb
    440416   (analyse_liveness fix_comp (prog_var_names (joint_function ERTLptr) ℕ prog)
    441     fn))
     417    fn) pt)
    442418  st1_no_pc
    443   =sigma_fb_state prog f_lbls f_regs
     419  =sigma_fb_state prog
    444420   (to_be_cleared_fb
    445421    (analyse_liveness fix_comp (prog_var_names (joint_function ERTLptr) ℕ prog)
    446      fn))
     422     fn) pt)
    447423   (st_no_pc … st1)).
    448 #fix_comp #colour #prog letin p_in ≝ (mk_prog_params ???) #f #fn #f_lbls #f_regs
     424#fix_comp #colour #prog letin p_in ≝ (mk_prog_params ???) #f #fn
    449425#st1 #st1' *
    450426try (#arg1 #arg2 #arg3 #arg4 #arg5 #Heval #Helim)
     
    493469try (@sigma_fb_state_insensitive_to_dead_Reg assumption)
    494470try (@sigma_fb_state_insensitive_to_dead_carry assumption)
    495 [ <(injective_OK ??? Hst1'') XXX
    496   >sigma_fb_state_insensitive_to_dead_carry assumption
    497  @sigma_fb_state_insensitive_to_dead_carry
     471[1,2,3,4,5,6,7: <(injective_OK ??? Hst1'') ]
     472[1,2,3:
     473  >sigma_fb_state_insensitive_to_dead_carry try assumption
     474  @sigma_fb_state_insensitive_to_dead_reg assumption
     475|4,5,6: (* BUG! *)
     476|7: >sigma_fb_state_insensitive_to_dead_reg try assumption
    498477
    499478lemma make_ERTLptr_To_LTL_good_state_relation :
Note: See TracChangeset for help on using the changeset viewer.