Changeset 2891 for src/ERTL


Ignore:
Timestamp:
Mar 16, 2013, 10:42:43 AM (7 years ago)
Author:
piccolo
Message:

added precondition on seq statement and tested correct in the ERTl-ERTLptr passed

Location:
src/ERTL
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLtoERTLptrOK.ma

    r2883 r2891  
    160160
    161161include "joint/StatusSimulationHelper.ma".
     162include alias "basics/lists/listb.ma".
    162163
    163164lemma make_ERTL_To_ERTLptr_good_state_relation :
     
    209210  change with (pc_block (pc … st2)) in match (pc_block ?);
    210211  <(fetch_stmt_ok_sigma_pc_ok … EQfetch) >EQfn %
     212| #st1 #st1' #st2 #f #fn #stmt #nxt #EQfetch whd in match eval_state;
     213  whd in match eval_statement_no_pc; normalize nodelta >EQfetch >m_return_bind
     214  normalize nodelta #H @('bind_inversion H) -H #st1_no_pc' #EQst1_no_pc'
     215  whd in ⊢ (??%% → ?); #EQ destruct(EQ) whd in ⊢ (%→?); #EQ destruct(EQ)
     216  whd in match sigma_state_pc in EQst1_no_pc'; normalize  nodelta in EQst1_no_pc';
     217  cases(fetch_statement_inv … EQfetch) >(fetch_stmt_ok_sigma_pc_ok … EQfetch)
     218  #EQfn #EQstmt >EQfn in EQst1_no_pc'; normalize nodelta #EQst1_no_pc'
     219  #t_fn #EQt_fn whd % [2: %{(refl …)} |] lapply(err_eq_from_io ????? EQst1_no_pc')
     220  -EQst1_no_pc' #EQst1_no_pc'
     221  cases(eval_seq_no_pc_no_call_ok prog f_lbls f_regs ???????? EQst1_no_pc')
     222  [ #st2_no_pc' * #EQst2_no_pc' #EQ destruct(EQ)
     223  %{(mk_state_pc ? st2_no_pc'
     224     (pc_of_point ERTLptr_semantics (pc_block (pc … st2)) nxt)
     225     (last_pop … st2))} %
     226     [ whd in ⊢ (??%?); >EQst2_no_pc' %
     227     | whd whd in match sigma_state_pc; normalize nodelta >EQfn %
     228     ]
     229  |  #lbl whd in match code_has_label; whd in match code_has_point; normalize nodelta
     230  inversion(stmt_at ????) [#_ *] #stmt1 #EQstmt1 #_
     231  cut(fetch_statement ERTL_semantics (prog_var_names … prog) (globalenv_noinit … prog)
     232                      (pc_of_point ERTL_semantics (pc_block (pc … st2)) lbl) =
     233                 return 〈f,fn,stmt1〉)
     234   [ whd in ⊢ (??%?); >EQfn normalize nodelta >point_of_pc_of_point >EQstmt1 %] #EQf_stmt1
     235  cases(b_graph_transform_program_fetch_statement_plus … good … EQf_stmt1)
     236  #init * #t_fn' ** #EQt_fn' whd in ⊢ (% → ?); cases(init_regs ?) [2: #x #y *]
     237  normalize nodelta #EQ destruct(EQ) * #labels * #registers
     238  ******* #EQlabels >point_of_pc_of_point change with (pc_block (pc … st2)) in match (pc_block ?);
     239  #EQregisters #_ #_ #_ #_ #fresh_regs #_ >EQregisters
     240  cases(excluded_middle_list ? (λreg.bool_to_Prop(¬(reg∈registers)))
     241         (get_used_registers_from_seq … (functs ERTL) stmt) ?)
     242  [3: #a #_ cases(¬a∈registers) // |1: #H assumption] #H @⊥
     243  cases(Exists_All … H (regs_are_in_univers … (pi2 ?? fn) … EQstmt))
     244   #reg ** #H1 #H2 @H1 -H1 @notb_Prop % #H1 lapply(fresh_regs … lbl) >EQregisters
     245  #H3 lapply(All_memb … H3 H1) ** #H4 #_ @H4 assumption
     246  ]
    211247]
    212248qed.
  • src/ERTL/ERTLtoERTLptrUtils.ma

    r2845 r2891  
    413413     (be_op2 b op).
    414414#prog #sigma #b #op #bv #bv1 whd in match be_op2; normalize nodelta
    415 cases bv
     415cases daemon
     416qed. (*TODO*)
     417(*cases bv
    416418[ | | #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc1 #p1]
    417 normalize nodelta [@res_preserve_error1] whd in match sigma_beval;
     419normalize nodelta [cases op normalize nodelta @res_preserve_error1] whd in match sigma_beval;
    418420normalize nodelta
    419421cases bv1
     
    499501      ]
    500502]
    501 qed.
     503qed.*)
    502504
    503505lemma pointer_of_address_ok : ∀prog : ertl_program.∀f_lbls : lbl_funct.
     
    10491051        sigma_stored_pc prog f_lbls pc〉)
    10501052     (pop_ra ERTL_semantics)
    1051      (pop_ra ERTLptr_semantics).   
     1053     (pop_ra ERTLptr_semantics).
     1054cases daemon (*TODO*) qed.
     1055(*       
    10521056#prog #f_lbls #f_regs #restr1 #st whd in match pop_ra; normalize nodelta
    10531057@mfr_bind1
     
    10881092| #pc @mfr_return_eq1 %
    10891093]
    1090 qed.
     1094qed.*)
    10911095
    10921096lemma pc_block_eq : ∀prog : ertl_program. ∀f_lbls,pc.
Note: See TracChangeset for help on using the changeset viewer.