Changeset 2898 for src/ERTLptr


Ignore:
Timestamp:
Mar 18, 2013, 10:03:37 AM (8 years ago)
Author:
piccolo
Message:

1) simplification of cond and seq case for StatusSimulationHelper? which has
been tested correct in ERTL to ERTlptr correctness proof.

2) the cond case for ERTLptr to LTL correctenss proof has been adapted to the
new specification

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTLptr/ERTLptrToLTLProof.ma

    r2889 r2898  
    2121λprog : ltl_program.λstack_sizes.
    2222joint_abstract_status (mk_prog_params LTL_semantics prog stack_sizes).
    23 
    24 axiom sigma_stored_pc : ertlptr_program → (block → label → list label) → 
    25 program_counter → program_counter.
    26 
    2723
    2824definition clear_sb_type ≝ label → decision → bool.
     
    8177  ].
    8278
     79include "joint/StatusSimulationHelper.ma".
     80
    8381definition sigma_sb_state_pc :fixpoint_computer → coloured_graph_computer → 
    8482ertlptr_program → (block → label → list label) →
     
    9290     let coloured_graph ≝ build … (\snd y) after in
    9391     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))
     92                       (to_be_cleared_sb after coloured_graph) st) (pc … st) 
     93                   (sigma_stored_pc ERTLptr_semantics LTL_semantics
     94                                    prog f_lbls (last_pop … st))
    9695  | Error e ⇒ dummy_state_pc
    9796  ].
     97
     98definition state_rel : fixpoint_computer → coloured_graph_computer →
     99ertlptr_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.
     102∃f,fn.fetch_internal_function ? (globalenv_noinit … prog) bl = return 〈f,fn〉 ∧
     103let after ≝ (analyse_liveness fix_comp (prog_var_names … prog) fn) in
     104let 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).
    98108
    99109axiom write_decision : decision → beval → state LTL_LIN_state →
     
    132142       (λs1:Σs:ERTLptr_status ??.as_classifier ? s cl_call
    133143          .λs2:Σs:LTL_status ??.as_classifier ? s cl_call
    134            .pc ? s1 =sigma_stored_pc prog f_lbls (pc ? s2))
     144           .pc ? s1 =sigma_stored_pc ERTLptr_semantics LTL_semantics
     145                                                          prog f_lbls (pc ? s2))
    135146    (* sim_final ≝ *) ?.
    136147cases daemon
     
    167178
    168179
    169 lemma eq_OK_OK_to_eq: ∀T,x,y. OK T x = OK T y → x=y.
    170  #T #x #y #EQ destruct %
    171 qed.
    172 
    173180
    174181axiom pc_block_eq_sigma_commute : ∀fix_comp,colour.
     
    186193∀ good :b_graph_transform_program_props ERTLptr_semantics LTL_semantics
    187194     (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs.
    188 ∀st1,st2,f,fn,stmt.
    189 fetch_statement ERTLptr_semantics (prog_var_names … prog) (globalenv_noinit … prog)
    190                 (pc … st1) = return 〈f,fn,stmt〉 →
     195∀st1,st2,f,fn.
     196fetch_internal_function ? (globalenv_noinit … prog)
     197                (pc_block (pc … st1)) = return 〈f,fn〉 →
    191198let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good) in
    192199R st1 st2 →
    193200(pc … st1) = (pc … st2).
    194201
    195 
     202(*
    196203axiom change_pc_sigma_commute : ∀fix_comp,colour.
    197204∀prog.∀ f_lbls,f_regs.∀f_bl_r.
     
    203210∀pc1,pc2.pc1 = pc2 →
    204211R (set_pc … pc1 st1) (set_pc … pc2 st2).
    205 (*
     212
    206213axiom globals_commute : ∀fix_comp,colour.
    207214∀prog.
    208215∀p_out,m,n.
    209216∀EQp_out: ertlptr_to_ltl fix_comp colour prog = 〈p_out, m, n〉.
    210 prog_var_names … prog = prog_var_names … p_out.*)
     217prog_var_names … prog = prog_var_names … p_out.
    211218
    212219lemma appoggio : (∀A,B,C : Type[0]. ∀a1,b1 : A.∀a2,b2 : B. ∀a3,b3 : C.
    213220〈a1,a2,a3〉 = 〈b1,b2,b3〉 → a1 = b1 ∧ a2 = b2 ∧ a3 = b3).
    214221#H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 destruct % [%] //
    215 qed.
     222qed.*)
    216223
    217224include "joint/semantics_blocks.ma".
    218225include "ASM/Util.ma".
    219 include "joint/StatusSimulationHelper.ma".
    220 
    221226
    222227axiom hw_reg_retrieve_write_decision_hit : ∀r : Register.∀bv : beval.
     
    350355good_state_relation ERTLptr_semantics LTL_semantics prog stacksizes
    351356 (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)»)
     357 init_regs f_lbls f_regs good (state_rel fix_comp colour prog f_lbls f_regs)
    352358 (sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good)).
    353359#fix_comp #colour #prog
     
    356362#init_regs * #f_lbls * #f_regs #good %{init_regs} %{f_lbls} %{f_regs} %{good}
    357363%
    358 [ #st1 #st2 #f #fn #stmt #Rst1st2 #EQstmt >(pc_eq_sigma_commute … good … EQstmt Rst1st2) %
     364[ #st1 #st2 #f #fn whd in ⊢ (% → ?); #REL lapply REL whd in match sigma_fb_state_pc;
     365  whd in match sigma_sb_state_pc; normalize nodelta #EQ #EQfn >EQfn in EQ;
     366  normalize nodelta <(pc_eq_sigma_commute  … good … EQfn REL) >EQfn
     367  normalize nodelta #H cases(state_pc_eq … H) * #H1 #_ #_ whd %{f} %{fn} %{EQfn}
     368  assumption
     369| #st1 #st2 #f #fn #Rst1st2 #EQfetcn >(pc_eq_sigma_commute … good … EQfetcn Rst1st2) %
     370| #st1 #st2 #f #fn whd in ⊢ (% → ?); #REL lapply REL whd in match sigma_fb_state_pc;
     371  whd in match sigma_sb_state_pc; normalize nodelta #EQ #EQfn >EQfn in EQ;
     372  normalize nodelta <(pc_eq_sigma_commute  … good … EQfn REL) >EQfn normalize nodelta
     373   #H cases(state_pc_eq … H) * #_ #_ //
     374| #st1 #st2 #pc #lp1 #lp2 #f #fn #EQfn * #f1 * #fn1 * >EQfn whd in ⊢ (??%% → ?);
     375  #EQ destruct(EQ) normalize nodelta #state_rel #EQ destruct(EQ) whd
     376  whd in match sigma_fb_state_pc; whd in match sigma_sb_state_pc; normalize nodelta
     377  >EQfn >EQfn normalize nodelta //
    359378| #st1 #st2 #f #fn #stmt #EQstmt #Rst1St2 >(as_label_ok … good … Rst1St2 EQstmt) %
    360379| normalize nodelta whd in ⊢ (% → % → % → ?); #st1 #st1' #st2 #f #fn #a #ltrue #lfalse
    361380  #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
     381  normalize nodelta >EQfetch >m_return_bind normalize nodelta >m_return_bind
    364382  whd in match eval_statement_advance; normalize nodelta
    365383  change with (ps_reg_retrieve ??) in match (acca_retrieve ?????);
     
    385403  %{st2_pre_mid_no_pc}
    386404  %
    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)
     405  [1,3: >map_eval_add_dummy_variance_id %
     406       [1,3: %
     407            [1,3: %
     408                 [1,3: @move_spec
     409                 |*: lapply Rst1st2 whd in ⊢ (% → ?); whd in match sigma_fb_state_pc;
     410                     whd in match sigma_sb_state_pc; normalize nodelta >EQfn
     411                     <(pc_eq_sigma_commute … good … EQfn Rst1st2) >EQfn
     412                     normalize nodelta #EQ cases(state_pc_eq … EQ) *
     413                     #EQst1st2 #_ #_ whd %{f} %{fn} %{EQfn}
     414                     <(insensitive_to_be_cleared_sb … prog f_lbls f_regs … st2 …
     415                                          (point_of_pc ERTLptr_semantics (pc … st2)))
     416                     [2,4: @dead_registers_in_dead @acc_is_dead ]
     417                     assumption
     418                 ]
     419            |*: %
     420            ]
     421       |*: %
     422       ]
     423  |*: change with (hw_reg_retrieve ??) in match (acca_retrieve ?????);
     424      >hw_reg_retrieve_write_decision_hit >m_return_bind
     425      cases(ps_reg_retrieve_hw_reg_retrieve_commute fix_comp colour prog …
     426                                                        good fn … Rst1st2 … EQbv)
    402427        [2,4: @(all_used_are_live_before … EQstmt)
    403428            [1,3: @set_member_singl |*: % ] ] #bv' * #EQbv' #EQbv1
     
    405430        >EQbv' in EQbool; #EQbool
    406431        >(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         ]
     432        normalize nodelta
     433        [2: <(pc_eq_sigma_commute … good … EQfn Rst1st2) %]
     434        whd in match goto; normalize nodelta
     435        >(pc_of_label_eq … EQt_fn1) <(pc_eq_sigma_commute … good … EQfn Rst1st2) %
    427436  ]
    428 | letin p_in ≝ (mk_prog_params ERTLptr_semantics ??)
     437| xxxxxxxxxxxx
     438 letin p_in ≝ (mk_prog_params ERTLptr_semantics ??)
    429439  letin p_out ≝ (mk_prog_params LTL_semantics ??)
    430440  letin trans_prog ≝ (b_graph_transform_program ????)
Note: See TracChangeset for help on using the changeset viewer.