Changeset 2849


Ignore:
Timestamp:
Mar 12, 2013, 1:41:46 PM (4 years ago)
Author:
piccolo
Message:

partial commit

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTLptr/ERTLptrToLTLProof.ma

    r2845 r2849  
    7070∀ prog : ertlptr_program.
    7171∀ f_lbls. ∀ f_regs. ∀f_bl_r.
    72 ∀p_out,m,n.
    73 ertlptr_to_ltl fix_comp colour prog = 〈p_out, m, n〉 →
    74 let stacksizes ≝ lookup_stack_cost … m in
    7572b_graph_transform_program_props ERTLptr_semantics LTL_semantics
    7673     (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs →
     74let p_out ≝ (\fst (\fst (ertlptr_to_ltl fix_comp colour prog))) in
     75let m ≝ (\snd (\fst (ertlptr_to_ltl fix_comp colour prog))) in
     76let n ≝ \snd (ertlptr_to_ltl fix_comp colour prog) in
     77let stacksizes ≝ lookup_stack_cost … m in 
    7778status_rel (ERTLptr_status prog stacksizes) (LTL_status p_out stacksizes) ≝
    78 λfix_comp,colour,prog,f_lbls,f_regs,f_bl_r,p_out,m,n,EQ.
    79 λgood.
     79λfix_comp,colour,prog,f_lbls,f_regs,f_bl_r.λgood.
    8080    mk_status_rel ??
    81     (* sem_rel ≝ *) (λs1:ERTLptr_status prog ?.
    82        λs2: LTL_status ? ?.
    83         sigma_fb_state_pc prog f_lbls f_regs s1 = sigma_sb_state_pc prog f_lbls f_regs s2)
     81    (* sem_rel ≝ *)
     82         (λs1:ERTLptr_status ? ?
     83          .λ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)
    8486    (* call_rel ≝ *) 
    85        (λs1:Σs.as_classifier … s cl_call.
    86         λs2:Σs.as_classifier … s cl_call.
    87          pc … s1 =sigma_stored_pc prog f_lbls (pc … s2))
     87       (λs1:Σs:ERTLptr_status ??.as_classifier ? s cl_call
     88          .λs2:Σs:LTL_status ??.as_classifier ? s cl_call
     89           .pc ? s1 =sigma_stored_pc prog f_lbls (pc ? s2))
    8890    (* sim_final ≝ *) ?.
    8991cases daemon
     
    9294axiom as_label_ok :
    9395∀fix_comp,colour.
    94 ∀prog.
    95 ∀p_out,m,n.
    96 ∀EQp_out: ertlptr_to_ltl fix_comp colour prog = 〈p_out, m, n〉.
    97 ∀f_lbls,f_regs.
    98 ∀f_bl_r.
     96∀prog.∀f_lbls,f_regs. ∀f_bl_r.
    9997∀ good :b_graph_transform_program_props ERTLptr_semantics LTL_semantics
    10098     (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs.
    10199∀st1,st2,fn,id,stmt.
    102 let stack_sizes ≝ lookup_stack_cost m in
    103 let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour … EQp_out … good) in
    104 R st1 st2 →
     100let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good) in
     101R st1 st2 → 
    105102fetch_statement ERTLptr_semantics (prog_var_names … prog)
    106103      (globalenv_noinit … prog) (pc … st1) = return 〈id,fn,stmt〉 →
    107 as_label (LTL_status p_out stack_sizes) st2 =
    108  as_label (ERTLptr_status prog stack_sizes) st1.
     104as_label ? st2 = as_label ? st1.
     105
    109106
    110107
     
    146143
    147144axiom pc_block_eq_sigma_commute : ∀fix_comp,colour.
    148 ∀prog.
    149 ∀p_out,m,n.
    150 ∀EQp_out: ertlptr_to_ltl fix_comp colour prog = 〈p_out, m, n〉.
    151 ∀ f_lbls,f_regs.
    152 ∀f_bl_r.
     145∀prog.∀ f_lbls,f_regs.∀f_bl_r.
    153146∀ good :b_graph_transform_program_props ERTLptr_semantics LTL_semantics
    154147     (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs.
    155148∀st1,st2.
    156 let stack_sizes ≝ lookup_stack_cost m in
    157 let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour … EQp_out … good) in
     149let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good) in
    158150R st1 st2 →
    159151pc_block (pc … st1) = pc_block (pc … st2).
    160152
    161 axiom change_pc_sigma_commute : ∀fix_comp,colour.
    162 ∀prog.
    163 ∀p_out,m,n.
    164 ∀EQp_out: ertlptr_to_ltl fix_comp colour prog = 〈p_out, m, n〉.
    165 ∀ f_lbls,f_regs.
    166 ∀f_bl_r.
     153axiom pc_eq_sigma_commute : ∀fix_comp,colour.
     154∀prog.∀ f_lbls,f_regs.∀f_bl_r.
    167155∀ good :b_graph_transform_program_props ERTLptr_semantics LTL_semantics
    168156     (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs.
    169157∀st1,st2.
    170 let stack_sizes ≝ lookup_stack_cost m in
    171 let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour … EQp_out … good) in
     158let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good) in
     159R st1 st2 →
     160(pc … st1) = (pc … st2).
     161
     162
     163axiom change_pc_sigma_commute : ∀fix_comp,colour.
     164∀prog.∀ f_lbls,f_regs.∀f_bl_r.
     165∀ good :b_graph_transform_program_props ERTLptr_semantics LTL_semantics
     166     (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs.
     167∀st1,st2.
     168let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good) in
    172169R st1 st2 →
    173170∀pc1,pc2.pc1 = pc2 →
    174171R (set_pc … pc1 st1) (set_pc … pc2 st2).
    175 
     172(*
    176173axiom globals_commute : ∀fix_comp,colour.
    177174∀prog.
    178175∀p_out,m,n.
    179176∀EQp_out: ertlptr_to_ltl fix_comp colour prog = 〈p_out, m, n〉.
    180 prog_var_names … prog = prog_var_names … p_out.
     177prog_var_names … prog = prog_var_names … p_out.*)
     178
     179lemma appoggio : (∀A,B,C : Type[0]. ∀a1,b1 : A.∀a2,b2 : B. ∀a3,b3 : C.
     180〈a1,a2,a3〉 = 〈b1,b2,b3〉 → a1 = b1 ∧ a2 = b2 ∧ a3 = b3).
     181#H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 destruct % [%] //
     182qed.
    181183
    182184include "joint/semantics_blocks.ma".
     
    186188∀fix_comp,colour.
    187189∀prog.
    188 ∀p_out,m,n.
    189 ∀EQp_out: ertlptr_to_ltl fix_comp colour prog = 〈p_out, m, n〉.
    190 ∀ f_lbls,f_regs.
    191 ∀f_bl_r.
     190∀ f_lbls,f_regs.∀f_bl_r.
    192191∀ good :b_graph_transform_program_props ERTLptr_semantics LTL_semantics
    193192     (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs.
    194193∀st1,st2,st1',f,fn,a,ltrue,lfalse.
    195 let stack_sizes ≝ lookup_stack_cost m in
    196 let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour … EQp_out … good) in
     194let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good) in
    197195R st1 st2 →
    198196 fetch_statement ERTLptr_semantics …
    199197  (globalenv_noinit ? prog) (pc … st1) =
    200198    return 〈f, fn,  sequential … (COND ERTLptr … a ltrue) lfalse〉 →
     199let stacksizes ≝ lookup_stack_cost …
     200                  (\snd (\fst (ertlptr_to_ltl fix_comp colour prog))) in 
    201201 eval_state ERTLptr_semantics
    202202   (prog_var_names … ℕ prog)
    203    (ev_genv … (mk_prog_params ERTLptr_semantics prog stack_sizes))
     203   (ev_genv … (mk_prog_params ERTLptr_semantics prog stacksizes))
    204204   st1 = return st1' →
    205 as_costed (ERTLptr_status prog stack_sizes) st1' →
     205as_costed (ERTLptr_status prog stacksizes) st1' →
    206206∃ st2'. R st1' st2' ∧
    207 ∃taf : trace_any_any_free (LTL_status p_out stack_sizes)
     207∃taf : trace_any_any_free (LTL_status ? ?)
    208208st2 st2'.
    209209bool_to_Prop (taaf_non_empty … taf).
    210 #fix_comp #colour #prog #transf_prog #stack_size #maxstack #EQtransf_prog
    211 #f_lbls #f_regs #f_bl_r #good #st1 #st2 #st1' #f #fn #a #ltrue #lfalse
    212 #Rst1st2
    213 #EQfetch whd in match eval_state; normalize nodelta >EQfetch >m_return_bind
     210#fix_comp #colour #prog #f_lbls #f_regs #f_bl_r #good #st1 #st2 #st1' #f #fn #a
     211#ltrue #lfalse #Rst1st2 #EQfetch whd in match eval_state; normalize nodelta
     212>EQfetch >m_return_bind
    214213whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
    215214whd in match eval_statement_advance; normalize nodelta
    216215change with (ps_reg_retrieve ??) in match (acca_retrieve ?????);
    217216#H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H
    218 #bv >set_no_pc_eta
    219 #EQbv #H @('bind_inversion H) -H * #EQbool normalize nodelta
    220  lapply(fetch_statement_inv … EQfetch) * #EQfn #_
     217#bv >set_no_pc_eta #EQbv #H @('bind_inversion H) -H * #EQbool normalize nodelta
     218lapply(fetch_statement_inv … EQfetch) * #EQfn #_
    221219[ whd in match goto; normalize nodelta >(pc_of_label_eq ??????? EQfn) >m_return_bind
    222220| whd in match next; normalize nodelta
    223221]
    224 whd in ⊢ (??%% → ?); #EQ <(eq_OK_OK_to_eq ??? EQ) -EQ -st1'
    225 #n_cost
     222whd in ⊢ (??%% → ?); #EQ <(eq_OK_OK_to_eq ??? EQ) -EQ -st1' #n_cost
    226223cases(b_graph_transform_program_fetch_statement … good … EQfetch)
    227224#init_data * #t_fn1 ** #EQt_fn1 whd in ⊢ (% → ?); cases (f_bl_r ?) normalize nodelta
    228225[2,4: #r #tl *] #EQ >EQ -init_data >if_merge_right in ⊢ (% → ?); [2,4: %] * #labs **
    229226[2,4: #hd #tl ** #_ #_ *** #pre #inst #post * whd in ⊢ (%→?); *] ** #EQlabs #EQf_regs
    230 whd in match translate_step; normalize nodelta * #bl *
    231 whd in ⊢ (% → ?); inversion (〈?,?〉) * #blp #blm #bls #EQ #EQbl >EQbl -bl
    232 letin p≝ (mk_prog_params LTL_semantics (\fst (\fst (ertlptr_to_ltl fix_comp colour prog))) (lookup_stack_cost stack_size))
    233 whd in ⊢ (% → ?); * #l1 * #mid1 * #mid2 * #l2 *** #EQmid1 whd in ⊢ (% → ?); #seq_pre_l
     227whd in match translate_step; normalize nodelta *** #blp #blm #bls *
     228whd in ⊢ (% → ?); #EQbl
     229whd in ⊢ (% → ?); * #l1 * #mid1 * #mid2 * #l2 *** #EQmid1 whd in ⊢ (% → ?);
     230#seq_pre_l
     231letin stacksizes ≝ (lookup_stack_cost …
     232                  (\snd (\fst (ertlptr_to_ltl fix_comp colour prog))))
     233letin p≝ (mk_prog_params LTL_semantics
     234                         (\fst (\fst (ertlptr_to_ltl fix_comp colour prog)))
     235                         stacksizes)
    234236cases(? : ∃st2'.repeat_eval_seq_no_pc p f (map_eval ?? blp mid1) (st_no_pc … st2) = return (st_no_pc … st2') ∧
    235237           pc … st2' = (pc_of_point ERTLptr_semantics (pc_block (pc … st2)) mid1) ∧
    236238           last_pop … st2' = last_pop … st2)
    237239   [2,4: cases daemon (* THE EXTENSIONAL PROOF *) ]
    238 #st2_pre_cond ** #res_st2_pre_cond #EQpc_st2_pre_cond #EQlast_pop_st2_pre_cond
    239 >(pc_block_eq_sigma_commute … EQtransf_prog … good … Rst1st2) in EQt_fn1; #EQt_fn1
    240 
    241 xxxxxxxxxxxxxxxxxxxxxxxxxxxx
    242 
     240#st2_pre_mid ** #res_st2_pre_mid #EQpc_st2_pre_mid #EQlast_pop_st2_pre_mid
     241>(pc_block_eq_sigma_commute … good … Rst1st2) in EQt_fn1; #EQt_fn1
     242>(pc_eq_sigma_commute … good … Rst1st2) in seq_pre_l; #seq_pre_l
     243whd in ⊢ (% → ?); * #nxt1 * #EQmid change with nxt1 in ⊢ (??%? → ?); #EQ
     244>EQ in EQmid ⊢ %; -nxt1 #EQmid
    243245lapply(taaf_to_taa ???
    244     (produce_trace_any_any_free p st2 f t_fn1 ??? st2_pre_cond EQt_fn1 seq_pre_l res_st2_pre_cond) ?)
    245  
    246    @(map_eval ??? mid1) lapply blp whd in match p; normalize nodelta
    247    whd in match (globals ?); whd in match prog_var_names; normalize nodelta
    248    change with (prog_var_names ??) in match (globals ??);
    249 
    250 lapply(produce_trace_any_any_free p st2 ?????
    251 
    252 
    253 %{(set_pc … (pc_of_point ERTLptr_semantics (pc_block (pc … st2)) ?) st2)}
     246           (produce_trace_any_any_free p st2 f t_fn1 ??? st2_pre_mid EQt_fn1
     247                                       seq_pre_l res_st2_pre_mid) ?)
     248[1,3: @if_elim #_ [2,4: @I] % whd in match as_costed; normalize nodelta
     249      whd in match (as_label ??); whd in match (as_pc_of ??);
     250      whd in match fetch_statement; normalize nodelta * #H @H -H >EQt_fn1
     251      >m_return_bind whd in match point_of_pc; normalize nodelta
     252      >point_of_offset_of_point >EQmid >m_return_bind normalize nodelta
     253      cases(appoggio ????????? EQbl) cases daemon (*PASSED DEPENDANT * #_ #EQ1 #_ >EQ1 % *) ]
     254#taa_pre_mid whd in ⊢ (% → ?);
     255cases(? : ∃st2_cond. eval_state LTL_semantics (globals p) (ev_genv … p) st2_pre_mid =
     256                     return st2_cond )
     257[2,4: cases daemon (*THE EXTENSIONAL PROOF *)]
     258#st2_mid #EQst2_mid
     259cut(bls = [ ] ∧ as_classify (joint_abstract_status p) st2_mid = cl_jump)
     260[1,3: cases daemon (*PASSED DEPENDANT *)] * #EQbls #CL_JUMP >EQbls whd in ⊢ (% → ?);
     261* #EQ1 #EQ2 destruct(EQ1 EQ2)
     262#seq_post_l   
     263lapply(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
     268cases(appoggio ????????? EQbl) * #_ #_ #EQ1 >EQ1 -EQ1
     269whd 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)}
    254272[ @ltrue |3: @lfalse]
    255 % [1,3: @(change_pc_sigma_commute … EQtransf_prog … good … Rst1st2)
    256         <(pc_block_eq_sigma_commute … EQtransf_prog … good … Rst1st2) %]
    257 
    258 
    259 
     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
    260285 -bl whd in ⊢ (% → ?); * #l1 * #mid1 * #mid2 * #l2
    261286*** #EQmid1 whd in ⊢ (% → ?); #seq_pre_l * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in ⊢ (% → ?); *
     
    322347∀colour : coloured_graph_computer.
    323348∀p_in : ertlptr_program.
    324 let 〈p_out, m, n〉 ≝ ertlptr_to_ltl fix_comp colour p_in in
     349let p_out ≝ (\fst (\fst (ertlptr_to_ltl fix_comp colour p_in))) in
     350let m ≝ (\snd (\fst (ertlptr_to_ltl fix_comp colour p_in))) in
     351let n ≝ \snd (ertlptr_to_ltl fix_comp colour p_in) in
    325352(* what should we do with n? *)
    326353let stacksizes ≝ lookup_stack_cost m in
     
    331358    R.
    332359#fix_comp #colour #p_in
    333 @pair_elim * #p_out #m #n #EQp_out whd
    334360cases(make_b_graph_transform_program_props ERTLptr_semantics LTL_semantics
    335361          (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») p_in)
    336362#fregs * #f_lbls * #f_bl_r #good
    337 %{(ERTLptr_to_LTL_StatusSimulation … EQp_out … good)}
     363%{(ERTLptr_to_LTL_StatusSimulation fix_comp colour p_in … good)}
    338364whd in match status_simulation; normalize nodelta
    339365whd in match ERTLptr_status; whd in match LTL_status; normalize nodelta
     
    367393| (*COND*) whd in match joint_classify; normalize nodelta >EQfetch
    368394          normalize nodelta #n_costed
    369           cases(eval_cond_ok … EQp_out … good … EQst2 … EQfetch EQeval … n_costed)
     395          cases(eval_cond_ok … good … EQst2 … EQfetch EQeval … n_costed)
    370396          #st2' * #EQst2' * #taf #tafne %{st2'} %{taf} >tafne % [% [@I|assumption]]
    371           whd >EQst2' >(as_label_ok fix_comp colour … EQp_out … good … EQst2') [%] cases daemon (*TODO*)
     397          whd >EQst2' >(as_label_ok fix_comp colour … good … EQst2') [%] cases daemon (*TODO*)
    372398| (*seq*) XXX whd in match joint_classify; normalize nodelta >EQfetch
    373399          normalize nodelta
Note: See TracChangeset for help on using the changeset viewer.