Changeset 2851


Ignore:
Timestamp:
Mar 12, 2013, 4:13:21 PM (4 years ago)
Author:
piccolo
Message:

partial commit

Location:
src
Files:
1 added
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTLptr/ERTLptrToLTLProof.ma

    r2849 r2851  
    220220| whd in match next; normalize nodelta
    221221]
    222 whd in ⊢ (??%% → ?); #EQ <(eq_OK_OK_to_eq ??? EQ) -EQ -st1' #n_cost
     222whd in ⊢ (??%% → ?); #EQ lapply(eq_OK_OK_to_eq ??? EQ) -EQ #EQst1' #n_cost
    223223cases(b_graph_transform_program_fetch_statement … good … EQfetch)
    224224#init_data * #t_fn1 ** #EQt_fn1 whd in ⊢ (% → ?); cases (f_bl_r ?) normalize nodelta
     
    235235                         stacksizes)
    236236cases(? : ∃st2'.repeat_eval_seq_no_pc p f (map_eval ?? blp mid1) (st_no_pc … st2) = return (st_no_pc … st2') ∧
    237            pc … st2' = (pc_of_point ERTLptr_semantics (pc_block (pc … st2)) mid1) ∧
     237           pc … st2' = (pc_of_point LTL_semantics (pc_block (pc … st2)) mid1) ∧
    238238           last_pop … st2' = last_pop … st2)
    239239   [2,4: cases daemon (* THE EXTENSIONAL PROOF *) ]
     
    257257[2,4: cases daemon (*THE EXTENSIONAL PROOF *)]
    258258#st2_mid #EQst2_mid
    259 cut(bls = [ ] ∧ as_classify (joint_abstract_status p) st2_mid = cl_jump)
     259cut(bls = [ ] ∧ as_classify (joint_abstract_status p) st2_pre_mid = cl_jump)
    260260[1,3: cases daemon (*PASSED DEPENDANT *)] * #EQbls #CL_JUMP >EQbls whd in ⊢ (% → ?);
    261 * #EQ1 #EQ2 destruct(EQ1 EQ2)
    262 #seq_post_l   
    263 lapply(taaf_to_taa ???
    264            (produce_trace_any_any_free p st2_cond f t_fn1 ??? st2_pre_mid EQt_fn1
    265                                        seq_pre_l res_st2_pre_mid) ?)
    266                  
    267 
    268 cases(appoggio ????????? EQbl) * #_ #_ #EQ1 >EQ1 -EQ1
    269 whd in ⊢ (% →  ?); * #EQ2 #EQ3 >EQ3 in seq_pre_l EQcond; -mid2 #se_pre_l #EQcond 
    270 >EQ2 in EQmid1; #EQmid1 -l2
    271 %{(set_pc … (pc_of_point ERTLptr_semantics (pc_block (pc … st2)) ?) st2_pre_cond)}
    272 [ @ltrue |3: @lfalse]
    273 % [1,3: @(change_pc_sigma_commute … good … Rst1st2) % ]
    274 %{(taaf_step_jump ? ??? taa_pre_cond ???) I}
    275 [2,5:  whd whd in ⊢ (??%?); whd in match fetch_statement; normalize nodelta
    276        >EQt_fn1  >m_return_bind >point_of_pc_of_point >EQcond >m_return_bind
    277        cases(appoggio ????????? EQbl) cases daemon (*PASSED DEPENDENT * #_ #EQ #_ >EQ -EQ % *)
    278 |3,6: whd whd in match eval_state; whd in match fetch_statement; normalize nodelta
    279        >EQt_fn1  >m_return_bind >point_of_pc_of_point >EQcond >m_return_bind
    280        cases(appoggio ????????? EQbl) * #_ #EQ #_ >EQ -EQ
    281        whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
    282        whd in match eval_statement_advance; normalize nodelta
    283        change with (hw_reg_retrieve ??) in match (acca_retrieve ?????);
    284        cases
    285  -bl whd in ⊢ (% → ?); * #l1 * #mid1 * #mid2 * #l2
    286 *** #EQmid1 whd in ⊢ (% → ?); #seq_pre_l * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in ⊢ (% → ?); *
    287 #nxt1 * #EQcond #EQ destruct(EQ) whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2)
    288 whd in EQmid1 : (??%%); destruct(EQmid1)
    289 %{(taaf_step_jump … (taa_base …) …) I}
    290 [2,5: whd whd in ⊢ (??%?); whd in match fetch_statement; normalize nodelta 
    291       <(fetch_stmt_ok_sigma_pc_ok … EQfetch) >EQt_fn1 >m_return_bind
    292       >EQcond %
    293 |3,6: whd whd in match eval_state; normalize nodelta whd in match eval_statement_no_pc;
    294       normalize nodelta whd in match fetch_statement; normalize nodelta
    295       <(fetch_stmt_ok_sigma_pc_ok … EQfetch) >EQt_fn1 >m_return_bind
    296       >EQcond >m_return_bind normalize nodelta >m_return_bind
    297       whd in match eval_statement_advance; normalize nodelta
    298       change with (ps_reg_retrieve ??) in match (acca_retrieve ?????);
    299       cases(ps_reg_retrieve_ok … EQbv) #bv1 * #EQbv1 #EQsem >EQbv1
    300       >m_return_bind >EQsem in EQbool; #EQbool cases(bool_of_beval_ok … EQbool)
    301       #bool1 * #EQbool1 #EQ destruct(EQ) >EQbool1 >m_return_bind normalize nodelta
    302       >(fetch_stmt_ok_sigma_pc_ok … EQfetch) [2: %] whd in match goto;
    303       normalize nodelta >(fetch_stmt_ok_sigma_pc_ok … EQfetch) in EQt_fn1; #EQt_fn1
    304       >(pc_of_label_eq … EQt_fn1) >m_return_bind %
    305 |*: lapply n_cost whd in match as_costed; normalize nodelta
    306     [ cut((mk_state_pc ERTL_semantics
    307    (sigma_state prog f_lbls f_regs
    308     (added_registers ERTL (prog_var_names (joint_function ERTL) ℕ prog) fn
    309      (f_regs (pc_block (pc ERTLptr_semantics st2)))) st2)
    310    (pc_of_point ERTL_semantics (pc_block (pc ERTLptr_semantics st2)) ltrue)
    311    (sigma_stored_pc prog f_lbls (last_pop ERTLptr_semantics st2))) =
    312    sigma_state_pc prog f_lbls f_regs (mk_state_pc ERTLptr_semantics st2
    313     (pc_of_point ERTLptr_semantics (pc_block (pc ERTLptr_semantics st2)) ltrue)
    314     (last_pop ERTLptr_semantics st2))) [ whd in match sigma_state_pc; normalize  nodelta
    315     >(fetch_stmt_ok_sigma_pc_ok … EQfetch) in EQfn; #EQfn >EQfn %]
    316     #EQ >EQ >(as_label_ok … good … (mk_state_pc ERTLptr_semantics st2
    317     (pc_of_point ERTLptr_semantics (pc_block (pc ERTLptr_semantics st2)) ltrue)
    318     (last_pop ERTLptr_semantics st2))) [#H @H] cases daemon (*needs lemma see below *)
    319     | cut((mk_state_pc ERTL_semantics
    320    (sigma_state prog f_lbls f_regs
    321     (added_registers ERTL (prog_var_names (joint_function ERTL) ℕ prog) fn
    322      (f_regs (pc_block (pc ERTLptr_semantics st2)))) st2)
    323    (succ_pc ERTL_semantics (pc ERTLptr_semantics st2)
    324     (point_of_succ ERTLptr_semantics
    325      (point_of_pc ERTLptr_semantics
    326       (pc ERTL_semantics (sigma_state_pc prog f_lbls f_regs st2))) nxt1))
    327    (sigma_stored_pc prog f_lbls (last_pop ERTLptr_semantics st2))) =
    328    sigma_state_pc prog f_lbls f_regs (mk_state_pc ERTLptr_semantics st2
    329     (pc_of_point ERTLptr_semantics (pc_block (pc ERTLptr_semantics st2))
    330      (point_of_succ ERTLptr_semantics
    331       (point_of_pc ERTLptr_semantics
    332        (pc ERTL_semantics (sigma_state_pc prog f_lbls f_regs st2))) nxt1))
    333     (last_pop ERTLptr_semantics st2))) [ whd in match sigma_state_pc; normalize  nodelta
    334     >(fetch_stmt_ok_sigma_pc_ok … EQfetch) in EQfn; #EQfn >EQfn %] #EQ >EQ
    335     >(as_label_ok … good … (mk_state_pc ERTLptr_semantics st2
    336     (pc_of_point ERTLptr_semantics (pc_block (pc ERTLptr_semantics st2))
    337      (point_of_succ ERTLptr_semantics
    338       (point_of_pc ERTLptr_semantics
    339        (pc ERTL_semantics (sigma_state_pc prog f_lbls f_regs st2))) nxt1))
    340     (last_pop ERTLptr_semantics st2))) [#H @H] cases daemon (*needs lemma see below ! *)
     261* #EQ1 #EQ2 >EQ1 in EQmid1; #EQmid1 -l2 >EQ2 in seq_pre_l EQmid; -mid2 #seq_pre_l #EQmid
     262letin R ≝ (sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good))
     263cut(R st1' st2_mid) [1,3: cases daemon (*PASSED DEPENDANT*)] #Rst1_st2_mid
     264%{st2_mid} % [1,3: assumption ] %{(taaf_step_jump ? ??? taa_pre_mid ???) I}
     265[1,4: whd >(as_label_ok … fix_comp colour … good … Rst1_st2_mid) [1,6: assumption]
     266     cases daemon (*TODO see also ERTL_to_ERTLptrOK proof! *)
     267|*: <EQpc_st2_pre_mid <EQlast_pop_st2_pre_mid assumption
    341268]
    342 qed.*)
     269qed.
    343270
    344271
Note: See TracChangeset for help on using the changeset viewer.