Ignore:
Timestamp:
Jul 10, 2015, 4:08:09 PM (4 years ago)
Author:
piccolo
Message:
 
File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/variable_stack_pass.ma

    r3578 r3579  
    1313(**************************************************************************)
    1414
     15include "common_variable_stack.ma".
    1516include "stack.ma".
    1617
     
    7778include "Simulation.ma".
    7879
     80let rec divide_continuation_on_frames (l : list (ActionLabel flat_labels × frame_Instructions))
     81(to_append : list frame_Instructions) on l : list (list frame_Instructions) ≝
     82match l with
     83[ nil ⇒ [ to_append ]
     84| cons hd tl ⇒ let 〈act,code〉 ≝ hd in
     85               match act with
     86               [ ret_act _ ⇒ to_append :: divide_continuation_on_frames tl [code]
     87               |  _ ⇒ divide_continuation_on_frames tl (to_append @ [code])
     88               ]
     89].
     90
     91definition var_to_shift_ok ≝ λst : list activation_frame.
     92All … (λx.to_shift ≤ (|x|)) st.
     93
     94definition var_instr_bond_ok ≝ λst : list activation_frame.λcode : frame_Instructions.
     95λcont : list (ActionLabel flat_labels × frame_Instructions).
     96All2 ?? (λx,y.All … (λz.get_instr_bound z ≤ |x| - to_shift) y) st
     97 (divide_continuation_on_frames cont [code]).
     98
     99
     100definition frame_variable_sem_rel ≝
     101λs1 : state frame_state_params.
     102λs2 : state stack_state_params.
     103store … s1 = store … s2 ∧
     104code … s2 = trans_var_instr (code … s1) ∧
     105cont … s2 = foldr … (λx,tail. 〈(\fst x),trans_var_instr (\snd x)〉 :: tail) (nil ?) (cont … s1) ∧
     106io_info … s1 = io_info … s2 ∧ (code … s1 ≠ EMPTY … → io_info … s1 =false) ∧
     107var_to_shift_ok … (\fst (store … s1)) ∧ var_instr_bond_ok … (\fst (store … s1)) (code … s1) (cont … s1).
     108
    79109definition frame_variable_pass_rel :
    80110∀prog : Program frame_state_params frame_state_params frame_state_params.
    81111∀t_prog : Program stack_env_params stack_instr_params flat_labels.
    82112∀bound : ℕ.
    83 relations flat_labels (operational_semantics frame_state_params frame_sem_state_params prog)
     113relations flat_labels (operational_semantics frame_state_params (frame_sem_state_params bound) prog)
    84114(operational_semantics stack_state_params (stack_sem_state_params bound) t_prog) ≝
    85115λprog,t_prog,bound.
    86 (mk_relations flat_labels (operational_semantics frame_state_params frame_sem_state_params prog)
     116(mk_relations flat_labels (operational_semantics frame_state_params (frame_sem_state_params bound) prog)
    87117 (operational_semantics stack_state_params (stack_sem_state_params bound) t_prog)
    88  (λs1,s2.store … s1 = store … s2 ∧ code … s2 = trans_var_instr (code … s1) ∧
    89          cont … s2 = foldr … (λx,tail. 〈(\fst x),trans_var_instr (\snd x)〉 :: tail) (nil ?) (cont … s1))
     118 frame_variable_sem_rel
    90119 (λ_.λ_.True)).
    91120
     
    204233
    205234definition safe_cast : ∀A,B : Type[0].A = B → A → B ≝
    206 λA,B,prf.match prf with [refl ⇒ λx : A.x]. 
     235λA,B,prf.match prf with [refl ⇒ λx : A.x].
    207236
    208237let rec create_silent_trace_from_eval_combinators (prog : Program stack_env_params stack_instr_params flat_labels)
     
    211240 m_fold Option … eval_combinators l (store … st) = return (store … st') →
    212241  code … st = list_combinators_to_instructions l (code … st') →
    213   cont … st = cont … st' → io_info … st = io_info … st' →
     242  cont … st = cont … st' → io_info … st = false → io_info … st = io_info … st' →
    214243  raw_trace … (operational_semantics stack_state_params (stack_sem_state_params bound) prog) st st' ≝
    215244match l return λx.(m_fold Option … eval_combinators x ? = ? → ? = list_combinators_to_instructions x ? → ?) with
    216 [ nil ⇒ λprf1,prf2,prf3,prf4.safe_cast (raw_trace … (operational_semantics stack_state_params (stack_sem_state_params bound) prog) st st)
     245[ nil ⇒ λprf1,prf2,prf3,prf4,prf5.safe_cast (raw_trace … (operational_semantics stack_state_params (stack_sem_state_params bound) prog) st st)
    217246     (raw_trace … (operational_semantics stack_state_params (stack_sem_state_params bound) prog) st st') ? (t_base ?? st)
    218 | cons x xs ⇒ λprf1,prf2,prf3,prf4.
     247| cons x xs ⇒ λprf1,prf2,prf3,prf4,prf5.
    219248   let next_store ≝ (opt_safe … (eval_combinators x (store … st)) ?) in
    220249   let next_st ≝ mk_state stack_state_params (list_combinators_to_instructions xs (code … st')) (cont … st')
    221250                   next_store (io_info … st') in
    222    let tail ≝ create_silent_trace_from_eval_combinators prog bound next_st st' xs ? (refl …) (refl …) (refl …) in
     251   let tail ≝ create_silent_trace_from_eval_combinators prog bound next_st st' xs ? (refl …) (refl …) ? (refl …) in
    223252   t_ind … (cost_act … (None ?)) … tail
    224253].
    225254@hide_prf
    226 [ cases st in prf1 prf2 prf3 prf4; cases st' #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 whd in H9 : (??%%);
    227   whd in H10 : (??%%); destruct %
    228 |4: change with (m_bind ?????) in prf1 :(??%?); cases(bind_inversion ????? prf1) -prf1 #w * #EQw #_ >EQw %
     255[ cases st in prf1 prf2 prf3 prf4 prf5; cases st'  #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 whd in ⊢ (??%% → ??%% → ?);
     256 #H9 #H10 #H11 #H12 #H13 destruct %
     257|5: change with (m_bind ?????) in prf1 :(??%?); cases(bind_inversion ????? prf1) -prf1 #w * #EQw #_ >EQw %
    229258   whd in ⊢ (??%% → ?); #EQ destruct
    230259| whd @seq_sil
     
    234263  |6: %
    235264  |7: assumption
    236   |9,10: cases daemon (*io*)
     265  |9,10: // normalize nodelta <prf5 //
    237266  |*:
    238267  ]
    239268| normalize nodelta @opt_safe_elim #w #EQw change with (m_bind ?????) in prf1 :(??%?); >EQw in prf1;
    240269  >m_return_bind //
    241 ]
    242 qed.
    243 
    244 lemma create_silent_trace_from_eval_combinators_ok : ∀prog,bound,st,st',l,prf1,prf2,prf3,prf4,t.
    245 create_silent_trace_from_eval_combinators prog bound st st' l prf1 prf2 prf3 prf4 = t →
     270| normalize nodelta <prf5 //
     271]
     272qed.
     273
     274lemma create_silent_trace_from_eval_combinators_ok : ∀prog,bound,st,st',l,prf1,prf2,prf3,prf4,prf5,t.
     275create_silent_trace_from_eval_combinators prog bound st st' l prf1 prf2 prf3 prf4 prf5 = t →
    246276pre_silent_trace … t.
    247277#prog #bound #st #st' #l lapply st -st lapply st' -st' elim l
    248 [ * #code' #cont' #store' #io' * #code #cont #store #io whd in ⊢ (??%% → ??%% → ?); #EQ destruct #EQ1 #EQ2 #EQ3 destruct
    249   #t whd in ⊢ (??%% → ?); #EQ destruct % cases daemon (*io*)
     278[ * #code' #cont' #store' #io' * #code #cont #store #io whd in ⊢ (??%% → ??%% → ?); #EQ destruct #EQ1 #EQ2 #EQ3 #EQ4 destruct
     279  #t whd in ⊢ (??%% → ?); #EQ destruct % % whd in ⊢ (??%% → ?); cases code' -code' normalize nodelta
     280  [| #rt | #seq #opt_l #i | #cond #ltrue #i_true #lfalse #i_false #i | #cond #ltrue #i_true #lfalse #i | #f #act #opt_l #i |
     281    #lin *]
     282  #EQ destruct
    250283| #x #xs #IH #st' #st #H cases(bind_inversion ????? H) #w * #EQw #EQstore_st'
    251284  whd in ⊢ (???% → ?); change with (list_combinators_to_instructions ??) in match (foldr ?????);
    252   #prf2 #EQcont #EQio #t whd in ⊢ (??%? → ?); #EQ destruct %2 [cases daemon (* io *)] @IH [|*: %]
    253 ]
    254 qed.
    255 
     285  #prf2 #EQcont #Hio #EQio #t whd in ⊢ (??%? → ?); #EQ destruct %2
     286  [2: @IH try % (*?????? possibile baco!!!!!*) ]
     287  % whd in ⊢ (??%% → ?); cases(code … st)
     288  [| #rt | #seq #opt_l #i | #cond #ltrue #i_true #lfalse #i_false #i | #cond #ltrue #i_true #lfalse #i | #f #act #opt_l #i |
     289    #lin *] normalize nodelta [ >Hio normalize nodelta] #EQ destruct
     290]
     291qed.
    256292(*  [ @opt_safe_elim #w' >EQw whd in ⊢ (??%% → ?); #EQ destruct assumption
    257293  | %
    258294  | % c'e' un baco????*)
     295
     296
     297
     298lemma list_n_def : ∀A,n,a.(|list_n A a n|) = n.
     299#A #n elim n // #m #IH #a normalize @eq_f @IH
     300qed.
     301
     302
     303
     304lemma var_initial_stack_initial : ∀prog,bound.
     305get_instr_bound (main … prog) ≤ bound - to_shift →
     306∀s1.∀s2.
     307bool_to_Prop (lang_initial ? (frame_sem_state_params bound) prog s1) →
     308bool_to_Prop (lang_initial ? (stack_sem_state_params bound)  (trans_var_prog prog) s2) →
     309frame_variable_sem_rel s1 s2.
     310#prog #bound #Hbound #s1 #s2 #H cases(andb_Prop_true … H) -H #H cases(andb_Prop_true … H) -H
     311#H cases(andb_Prop_true … H) -H @eq_instructions_elim #EQcode_s1 * @eqb_list_elim #EQcont_s1 *
     312normalize in match (init_store ??); #EQstore_s1 #Hio1
     313#H cases(andb_Prop_true … H) -H #H cases(andb_Prop_true … H) -H #H cases(andb_Prop_true … H) -H
     314@eq_instructions_elim #EQcode_s2 * @eqb_list_elim #EQcont_s2 * normalize in match (init_store ??);
     315#EQstore_s2 #Hio2 %
     316[ % [ % [ % [ % [ % [ >(\P (bool_as_Prop_to_eq … EQstore_s1)) >(\P (bool_as_Prop_to_eq … EQstore_s2)) %
     317                    |  >EQcode_s1 >EQcode_s2 %
     318                    ]
     319                | >EQcont_s1 >EQcont_s2 %
     320                ]
     321            | >Hio1 >Hio2 %
     322            ]
     323        | >EQcode_s1 * #H cases H %
     324        ]
     325    | >(\P (bool_as_Prop_to_eq … EQstore_s1)) normalize % /2/
     326    ]
     327| >(\P (bool_as_Prop_to_eq … EQstore_s1)) >EQcode_s1 >EQcont_s1 whd %
     328  [ % // % [ @(transitive_le … Hbound) normalize >list_n_def <minus_n_O /2/]
     329  % normalize //
     330  ]
     331@I
     332]
     333qed.
     334
     335
     336lemma var_final_stack_final : ∀s1,s2.frame_variable_sem_rel s1 s2 →
     337bool_to_Prop(lang_final … s1) → bool_to_Prop (lang_final … s2).
     338#s1 #s2 ****** #EQstore #EQcode #EQcont #Hio1 #_ #_ #_ #H cases(andb_Prop_true … H) -H
     339@eq_instructions_elim #EQinstr * cases(cont … s1) in EQcont; [|#x #xs #_ *]
     340whd in ⊢ (??%% → ?); #EQcont_s2 #_ @andb_Prop [ >EQcode >EQinstr @I | >EQcont_s2 @I]
     341qed.
     342
     343lemma var_io_is_stack_io :∀s1,s2.frame_variable_sem_rel s1 s2 → lang_classify ? s2 = cl_io → lang_classify ? s1 = cl_io.
     344#s1 #s2 whd in match frame_variable_sem_rel; normalize nodelta ****** #_ #EQcode #_ #Hio1 #_ #_ #_
     345whd in match lang_classify; normalize nodelta cases (code … s2) in EQcode; normalize nodelta
     346[| #rt | #seq #opt_l #i | #cond #ltrue #i_true #lfalse #i_false #i | #cond #ltrue #i_true #lfalse #i | #f #act #opt_l #i |
     347    #lin *] [2,3,4,5,6: #_ #EQ destruct] cases (code … s1)
     348[| #rt | #seq #opt_l #i | #cond #ltrue #i_true #lfalse #i_false #i | #cond #ltrue #i_true #lfalse #i | #f #act #opt_l #i |
     349    #lin *]  whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
     350[2: cases(trans_expr rt) in EQ; [2: #x #xs] whd in ⊢ (????%→ ?); #EQ destruct
     351|3: cases seq in EQ; normalize nodelta [2: #v #EQ destruct] * #v #e normalize nodelta cases(trans_expr ?)
     352    [2: #x #xs] whd in ⊢ (????%→ ?); #EQ destruct
     353|4: cases(trans_cond ?) in EQ; [2: #x #xs] whd in ⊢ (????%→ ?); #EQ destruct
     354|5: cases(trans_expr act) in EQ; [2: #x #xs] whd in ⊢ (????%→ ?); #EQ destruct
     355]
     356normalize nodelta >Hio1 //
     357qed.
     358
     359lemma divide_continuation_on_frame_app : ∀ct,z,app.divide_continuation_on_frames ct (app @ z) =
     360match divide_continuation_on_frames ct z with
     361[ nil ⇒ [app @ z] | cons x xs ⇒ (app @ x) :: xs ].
     362#ct elim ct
     363[ #z #app whd in ⊢ (??%%); % ]
     364** [#f #lbl |*: #opt_l] #i #tl #IH #z #ap whd in ⊢ (??%%); // whd in match (divide_continuation_on_frames ??) in ⊢ (???%);
     365>associative_append >IH inversion(divide_continuation_on_frames …) // #ABS @⊥ lapply ABS -ABS lapply z -z lapply i -i
     366elim tl [1,3: #i #z whd in ⊢ (??%% → ?); #EQ destruct] * #y1 #y2 #ys #IH #i #z cases y1
     367[1,4: #f #lbl |*: #opt_l] whd in ⊢ (??%? → ?); try @IH #EQ destruct
     368qed.
     369
     370lemma divide_continuation_on_frame_app_nil_is_nil : ∀ct,app.divide_continuation_on_frames ct app = [ ] →
     371app = [ ].
     372#ct elim ct [ #app whd in ⊢ (??%% → ?); #H destruct]
     373* #x1 #x2 #xs #IH #app whd in ⊢ (??%% → ?); cases x1 [#f #lbl |*: #opt_l] normalize nodelta
     374#H destruct lapply(IH … H) elim app // #z #zs #_ whd in match (append ???); #EQ destruct
     375qed.
     376
     377lemma var_instr_bond_for_empty : ∀st,x,opt_l,cd,ct.
     378var_instr_bond_ok st x (〈cost_act … opt_l,cd〉::ct) →
     379var_instr_bond_ok st cd ct.
     380#st #x #opt_l #cd #ct whd in ⊢ (% → %); whd in match (divide_continuation_on_frames ??);
     381whd in match (divide_continuation_on_frames ??) in ⊢ (? → %); >divide_continuation_on_frame_app
     382inversion(divide_continuation_on_frames ??)
     383[ #ABS lapply(divide_continuation_on_frame_app_nil_is_nil … ABS) #EQ destruct]
     384#y #ys #_ #EQdivide normalize nodelta cases st -st [ *]
     385#z #zs * #H1 #H2 % // cases H1 //
     386qed.
     387
     388definition get_top_expression_from_instr : frame_Instructions → option expr ≝
     389λi.match i with
     390[ EMPTY ⇒ None ?
     391| RETURN exp ⇒ return exp
     392| SEQ seq opt_l instr ⇒
     393  match seq with
     394  [ Seq_i seq' ⇒
     395     match seq' with
     396     [ sAss v e ⇒ return e
     397     ]
     398  | PopReg v ⇒ None ?
     399  ]
     400| COND cond ltrue i_true lfalse i_false instr ⇒ None ?
     401| LOOP cond ltrue i_true lfalse instr ⇒ None ?
     402| CALL f act_p opt_l instr ⇒ return act_p
     403| IO lin io lout instr ⇒ ?
     404].
     405cases io
     406qed.
     407
     408lemma expr_bound_good_expr : ∀e,n.get_expr_bound e ≤ n →
     409good_expr n e.
     410#e elim e normalize /2/ #e1 #e2 #IH1 #IH2 #n #H @All_append try @IH1 try @IH2
     411change with (max (get_expr_bound e1) (get_expr_bound e2)) in H : (?%?);
     412@(transitive_le … H) /2 by le_maxl/
     413qed.
     414
     415lemma good_expr_for_var_instr_ok : ∀x,st,cd,ct,e.
     416var_instr_bond_ok (x :: st) cd ct →
     417get_top_expression_from_instr cd = return e →
     418good_expr (|x|-to_shift) e.
     419#x #st #cd #ct #e whd in ⊢ (% → ?); inversion(divide_continuation_on_frames ??)
     420[ #ABS lapply(divide_continuation_on_frame_app_nil_is_nil … ABS) #EQ destruct]
     421#y #ys #_ normalize nodelta <(append_nil … [cd]) >divide_continuation_on_frame_app
     422cases(divide_continuation_on_frames ??) [|#z #zs] normalize nodelta
     423[>append_nil | whd in match (append ???); whd in match (append ???); ]
     424#EQ destruct ** #H #_ #_ cases cd in H; -cd
     425[1,8: |2,9: #rt |3,10: * [1,3: * #v #exp |*: #v] #opt_l #i |4,11: #cond #ltrue #i_true #lfalse #i_false #i
     426|5,12: #cond #ltrue #i_true #lfalse #i |6,13: #f #act #opt_l #i |7,14: #lin *] #H1 whd in ⊢ (??%% → ?);
     427#EQ destruct @expr_bound_good_expr /2 by le_maxl/
     428qed.
     429
     430check frame_assign_var
     431
     432lemma var_to_shift_frame_assign_var_ok : ∀st,v,val,new_st.
     433var_to_shift_ok (\fst st) → frame_assign_var st v val = return new_st →
     434var_to_shift_ok (\fst new_st).
     435cases daemon
     436qed.
     437
     438lemma var_instr_bond_frame_assign_var_ok : ∀st,i,ct,v,val,new_st.
     439var_instr_bond_ok (\fst st) i ct →
     440frame_assign_var st v val = return new_st →
     441var_instr_bond_ok (\fst new_st) i ct.
     442cases daemon
     443qed.
     444
     445lemma var_instr_bond_seq_ok : ∀st.
     446∀i : frame_Instructions.∀seq,opt_l.∀ct.
     447var_instr_bond_ok st (SEQ … seq opt_l i) ct →
     448var_instr_bond_ok st i ct.
     449cases daemon
     450qed.
     451
     452
     453lemma var_stack_simulate_tau :
     454∀prog : Program frame_state_params frame_state_params frame_state_params.
     455∀bound : ℕ.
     456∀s1.∀s2.∀s1'.
     457execute_l … (frame_sem_state_params bound) (env … prog) (cost_act … (None ?))  s1 s1'→
     458frame_variable_sem_rel … s1 s2 → lang_classify … s1 ≠ cl_io → lang_classify … s1' ≠ cl_io →
     459∃s2'. ∃t: raw_trace … (operational_semantics … (stack_sem_state_params bound) (trans_var_prog prog)) s2 s2'.
     460frame_variable_sem_rel s1' s2' ∧ silent_trace … t.
     461#prog #bound #s1 #s2 #s1' #H inversion H
     462[ #st1 #st1' * #act_lbl #instr #tl #EQcode_st1 #EQcont_st1 #EQ1 #EQ2 destruct #EQstore_11' #Hio1 #Hio2 #no_ret
     463  #EQ1 #EQ2 #EQ3 #EQ4 destruct ****** #EQstore_12 >EQcode_st1 whd in ⊢ (???% → ?); #EQcode_s2
     464  >EQcont_st1 whd in match (foldr ?????); #EQcont_s2 #EQ_io_st1 #_ #Hstore1 #Hstore2
     465  #Hclass_st1 #Hclass_st1'
     466  %{(mk_state … (trans_var_instr (code … st1')) (foldr … (λx,tail.〈\fst x,trans_var_instr (\snd x)〉::tail) [ ] (cont … st1'))
     467      (store … st1') false)} %{(t_ind … (cost_act … (None ?)) … (t_base …))}
     468  [ @hide_prf whd applyS empty try assumption try %
     469    [ #ABS whd in match lang_classify in Hclass_st1; normalize nodelta in Hclass_st1; >EQcode_st1 in Hclass_st1;
     470      normalize nodelta >EQ_io_st1 >ABS normalize nodelta * #H cases H %
     471      | >EQstore_12 %
     472      ]
     473  | %
     474    [ % [ % [/5 by refl, conj/ | <EQstore_11' // ] | <EQstore_11' @(var_instr_bond_for_empty … Hstore2) ]
     475    | %1 %2
     476        [ % whd in ⊢ (??%? → ?); cases(code … s2)
     477          [| #rt | #seq #opt_l #i | #cond #ltrue #i_true #lfalse #i_false #i | #cond #ltrue #i_true #lfalse #i | #f #act #opt_l #i |
     478           #lin *] normalize nodelta [|*: #EQ destruct] inversion(io_info … s2) #ABS normalize nodelta #EQ destruct
     479            whd in match lang_classify in Hclass_st1; normalize nodelta in Hclass_st1; >EQcode_st1 in Hclass_st1;
     480            normalize nodelta >EQ_io_st1 >ABS normalize nodelta * #H cases H %
     481        | %1 % whd in ⊢ (??%? → ?); cases(trans_var_instr ?)
     482           [| #rt | #seq #opt_l #i | #cond #ltrue #i_true #lfalse #i_false #i | #cond #ltrue #i_true #lfalse #i | #f #act #opt_l #i |
     483            #lin *] normalize nodelta #EQ destruct
     484        ]
     485     ]
     486  ]
     487| #st1 #st1' * [ * #v #e | #v ] #instr #mem #opt_l #EQcode_st1
     488  [ change with (m_bind ?????) in ⊢ (??%? → ?);
     489    #H1 cases(bind_inversion ????? H1) #curr_env * (*inversion(store … st1) *
     490    [| #hd #tl] #fp #EQstore_st1 whd in ⊢ (??%% → ?); #EQ destruct*) #EQcurr_env  #H
     491    cases(bind_inversion ????? H) -H #sem_e * #EQsem_e
     492  | change with (frame_assign_var ???) in ⊢ (??%? → ?);
     493  ]
     494  #EQmem #EQ destruct #EQcont #EQ destruct #EQio_st1 #EQio_st1' #EQ1 #EQ2 #EQ3 #EQ4 destruct ******
     495  #EQstore_12 >EQcode_st1
     496  [change with (list_combinators_to_instructions ??) in ⊢ (???% → ?); | whd in ⊢ (???% → ?); ]
     497  #EQcode_s2 #EQcont_s2 #Hio1 #Hio2 #Hstore1 #Hstore2 #Hclass_st1 #Hclass_st1'
     498  %{(mk_state … (trans_var_instr (code … st1')) (cont … s2) (store … st1') false)}
     499  [ cases(eval_exp_ok … EQcurr_env … EQsem_e)
     500    [2,3: cases(bind_inversion ????? EQcurr_env) #c_env inversion(store … st1) *
     501        [2,4: #hd #tl] #fp #EQstore_st1 * whd in ⊢ (??%% → ??%% → ?); #EQ1 #EQ2 destruct
     502        [ >EQstore_st1 in Hstore1; * // |  >EQstore_st1 in Hstore2; #H @(good_expr_for_var_instr_ok … H) % ] ]
     503    #new_st * >EQstore_12 #EQnew_st #EQpop
     504    %{((create_silent_trace_from_eval_combinators (trans_var_prog prog) bound s2
     505          (mk_state … ? (cont … s2) new_st false)
     506          (trans_expr e) EQnew_st …) @ (t_ind … (cost_act … (None ?)) … (t_base …)))}
     507    try assumption try %
     508    [ whd applyS seq_sil try % whd in ⊢ (??%?); >EQpop normalize nodelta <EQstore_12 @EQmem
     509    |2,3: <Hio1 @Hio2 % #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
     510    | % [ % [ % // % // % // % //] @(var_to_shift_frame_assign_var_ok … EQmem) assumption ]
     511      @(var_instr_bond_frame_assign_var_ok … EQmem) <EQcont
     512      @(var_instr_bond_seq_ok … Hstore2)
     513    ]
     514    @append_silent [ % @create_silent_trace_from_eval_combinators_ok [7: % |*:] ]
     515    xxxx
     516   
     517 
     518  %{((create_silent_trace_from_eval_combinators …) @ (t_ind … (t_base …)))}
     519 
     520
     521 whd in ⊢ (??%? → ?); #H cases(bind_inversion ????? H)
     522   
     523       
     524qed.
    259525
    260526definition simulation_imp_frame :
     
    264530λprog,bound.
    265531mk_simulation_conditions ….
    266 cases daemon
    267 qed.
     532[ @var_initial_stack_initial | @var_final_stack_final | @var_io_is_stack_io
     533| @var_stack_simulate_tau
     534qed.
Note: See TracChangeset for help on using the changeset viewer.