Changeset 3582 for LTS


Ignore:
Timestamp:
Jul 16, 2015, 4:02:53 PM (4 years ago)
Author:
piccolo
Message:

pass variable to stack in place

Location:
LTS
Files:
6 edited

Legend:

Unmodified
Added
Removed
  • LTS/Lang_corr.ma

    r3549 r3582  
    7272    [ #x #y #_ (*#_ #_ #_ #H*) *****
    7373    | #x #_ cases (ret_costed_abs ??) normalize nodelta [|#c] ******[|*] #EQ @⊥ >EQ in Hl1;
    74       normalize * /2/ ] *
     74      normalize * ] *
    7575    [ #EQconts1' normalize nodelta ****** #EQ destruct(EQ)
    7676      #HH1 #EQ destruct(EQ) >EQcode11 in ⊢ (% → ?); inversion(code … s1')
  • LTS/Language.ma

    r3579 r3582  
    247247| empty : ∀st,st',hd,tl.(code ? st) = (EMPTY p p)→ (cont ? st) = hd :: tl →
    248248           (code ? st') = \snd hd → (cont … st') = tl → (store … st) = (store … st') →
    249            (io_info … st = true → is_non_silent_cost_act … (\fst hd)) →  (io_info … st') = false → ¬ is_ret_call_act … (\fst hd) →  execute_l … (\fst hd) st st'
     249           (io_info … st = true → is_non_silent_cost_act … (\fst hd)) →  (io_info … st') = false → is_cost_label … (\fst hd) →  execute_l … (\fst hd) st st'
    250250| seq_sil : ∀st,st',i,cd,s,opt_l.(code ? st) = SEQ … i opt_l cd →
    251251             eval_seq … p' i (store … st) = return s → (code ? st') = cd →
  • LTS/Simulation.ma

    r3579 r3582  
    1515(rel : relations …S1 S2) : Prop ≝
    1616 { initial_is_initial :
    17    ∀s1,s2.(bool_to_Prop (as_initial … s1) →  bool_to_Prop (as_initial … s2)) → Srel … rel s1 s2
     17   ∀s1,s2.bool_to_Prop (as_initial … s1) →  bool_to_Prop (as_initial … s2) → Srel … rel s1 s2
    1818 ; final_is_final :
    1919   ∀s1,s2.bool_to_Prop (as_final … s1) → Srel … rel s1 s2 → bool_to_Prop (as_final … s2)
  • LTS/stack.ma

    r3577 r3582  
    136136λsgn.λst.
    137137    !〈n,st1〉 ← pop st; 
    138     frame_assign_var 〈(list_n … O (pred (to_shift + (f_pars … sgn))))::(\fst st1),(\snd st1)〉 to_shift n.
     138    frame_assign_var 〈(list_n … O (to_shift + (f_pars … sgn)))::(\fst st1),(\snd st1)〉 to_shift n.
    139139
    140140definition stack_return_call:frame_store_t→ (option frame_store_t)≝
  • LTS/variable.ma

    r3579 r3582  
    195195    !env ← frame_current_env … st;
    196196    !n ← frame_sem_expr env e;
    197     frame_assign_var 〈((list_n … O (pred (to_shift + (f_pars … sgn))))::(\fst st)),(\snd st)〉 to_shift n.
     197    frame_assign_var 〈((list_n … O (to_shift + (f_pars … sgn)))::(\fst st)),(\snd st)〉 to_shift n.
    198198
    199199definition frame_return_call:expr→ frame_store_t→ (option frame_store_t)≝
  • LTS/variable_stack_pass.ma

    r3581 r3582  
    107107var_to_shift_ok … (\fst (store … s1)) ∧ var_instr_bond_ok … (\fst (store … s1)) (code … s1) (cont … s1).
    108108
     109definition frame_variable_call_rel ≝
     110(λs1 : state frame_state_params.λs2 : state stack_state_params.
     111 cont … s2 = foldr … (λx,tail. 〈(\fst x),trans_var_instr (\snd x)〉 :: tail) (nil ?) (cont … s1) ∧
     112    ∃f,act_p,opt_l,instr.code … s1 =  CALL … f act_p opt_l instr ∧ code … s2 = CALL … f it opt_l (trans_var_instr instr)).
     113   
    109114definition frame_variable_pass_rel :
    110115∀prog : Program frame_state_params frame_state_params frame_state_params.
     
    117122 (operational_semantics stack_state_params (stack_sem_state_params bound) t_prog)
    118123 frame_variable_sem_rel
    119  (λ_.λ_.True)).
     124 frame_variable_call_rel).
    120125
    121126let rec expr_fv (e : expr) on e : list variable ≝
     
    412417@(transitive_le … H) /2 by le_maxl/
    413418qed.
     419
     420lemma cond_bound_good_cond : ∀e,n.get_cond_bound e ≤ n →
     421good_cond n e.
     422#e elim e /2/ #e1 #e2 #n change with (max (get_expr_bound ?) (get_expr_bound ?)) in ⊢ (?%? → ?);
     423#H normalize @All_append @expr_bound_good_expr /2 by le_maxl/
     424qed.
    414425
    415426lemma good_expr_for_var_instr_ok : ∀x,st,cd,ct,e.
     
    536547qed.
    537548
     549include alias "arithmetics/nat.ma".
     550
    538551lemma var_stack_simulate_label :
    539552∀prog : Program frame_state_params frame_state_params frame_state_params.
     
    611624            #lin *] normalize nodelta #EQ destruct
    612625   ]
    613 |*: cases daemon (*todo*)
    614 ]
    615 qed.
    616  
     626|3,4: #st1 #st1' #exp #ltrue #i_true #lfalse #i_false #instr #new_m #EQcode_st1
     627      [ change with (m_bind ?????) in ⊢ (??%? → ?); | change with (m_bind ?????) in ⊢ (??%? → ?);]
     628      #EQeval cases(bind_inversion ????? EQeval) #curr_env * #EQcurr_env #H
     629      cases(bind_inversion ????? H) -H #b * #EQb whd in ⊢ (??%% → ?); #EQ destruct #EQcont_st1'
     630      #EQ1 #EQstore destruct #Hio1 #Hio2 #EQ1 #EQ2 #EQ3 #EQ4 destruct #Hclass1 #Hclass2 ****** #EQstore_12
     631      >EQcode_st1
     632      [change with (list_combinators_to_instructions ??) in ⊢ (???% → ?); |
     633       change with (list_combinators_to_instructions ??) in ⊢ (???% → ?);
     634      ]
     635      #EQcode_s2 #EQcont_s2 #EQ_io #Hio3 #Hstore1 #Hstore2
     636      cases(eval_cond_ok … EQcurr_env EQb)
     637      [2,5: cases (store … st1) in EQcurr_env Hstore1; *
     638            [1,3: #fp whd in ⊢ (??%% → ?); #EQ destruct]
     639            #hd #tl #fp whd in ⊢ (??%% → ?); #EQ destruct * //
     640      |3,6: @cond_bound_good_cond cases(store … st1) in EQcurr_env Hstore2; *
     641            [2,4: #hd #tl] #fp whd in ⊢ (??%% → ?); #EQ destruct whd in ⊢ (% → ?);
     642            inversion(divide_continuation_on_frames ??) [1,3: #_ *] #x #xs #_
     643            change with ([?] @ ?) in match ([?] @ ?);
     644            >divide_continuation_on_frame_app cases(divide_continuation_on_frames ??)
     645            normalize nodelta [2,4: #y #ys] whd in ⊢ (??%% → ?); #EQ destruct
     646            ** /2 by le_maxl/
     647      ]
     648      #new_mem * #EQnew_mem normalize nodelta #EQpop
     649      %{(mk_state … (COND … it ltrue ? lfalse ? (trans_var_instr instr))
     650                    (cont … s2) new_mem false)}
     651      [3,6: %{(mk_state … (trans_var_instr … (code … st1'))
     652              (〈cost_act … (None ?),trans_var_instr … instr〉::cont … s2) (store … st1) false)}
     653            %{(mk_state … (trans_var_instr … (code … st1'))
     654              (〈cost_act … (None ?),trans_var_instr … instr〉::cont … s2) (store … st1) false)}
     655      [ %{(create_silent_trace_from_eval_combinators (trans_var_prog prog) bound s2
     656          (mk_state … (COND … it ltrue ? lfalse ? (trans_var_instr instr))
     657                    (cont … s2) new_mem false)
     658          (trans_cond exp) …)} try assumption try %
     659          [1,2: <EQ_io @Hio3 % #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
     660          | <EQstore_12 assumption
     661          | @cond_true [7,9,10,11,12,13: % |8: whd in ⊢ (??%?); >EQpop % |*:]
     662          ]
     663      | %{(create_silent_trace_from_eval_combinators (trans_var_prog prog) bound s2
     664          (mk_state … (COND … it ltrue ? lfalse ? (trans_var_instr instr))
     665                    (cont … s2) new_mem false)
     666          (trans_cond exp) …)} try assumption try %
     667          [1,2: <EQ_io @Hio3 % #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
     668          | <EQstore_12 assumption
     669          | @cond_false [7,9,10,11,12,13: % |8: whd in ⊢ (??%?); >EQpop % |*:]
     670          ]
     671      ]
     672      %{(t_base …)} %
     673      [2,4: % % whd in ⊢ (??%? → ?); cases(trans_var_instr ?)
     674         [1,8: |2,9: #rt |3,10: #seq #opt_l #i |4,11: #cond #ltrue #i_true #lfalse #i_false #i
     675         |5,12: #cond #ltrue #i_true #lfalse #i |6,13: #f #act #opt_l #i |7,14: #lin *] normalize nodelta #EQ destruct ]
     676      % [2,4: %  @(create_silent_trace_from_eval_combinators_ok … (refl …)) ]
     677      % [1,3: % [1,3: % // % // % [2,4: >EQcont_st1' @eq_f2 // ] % // ] <EQstore // ]
     678              >EQstore >EQcont_st1' change with ([?] @ ?) in match ([?] @ ?); whd
     679              cases(store … st1) in Hstore2; * [2,4: #x #xs] #fp whd in ⊢ (% → ?);
     680              inversion(divide_continuation_on_frames …)
     681              [1,3,5,7: #ABS * lapply(divide_continuation_on_frame_app_nil_is_nil … ABS) #EQ destruct]
     682              #y #ys #_ normalize nodelta [3,4: #_ *] change with ([?] @ ?) in match ([?] @ ?);
     683              >divide_continuation_on_frame_app inversion(divide_continuation_on_frames …)
     684              [2,4: #z #zs #_ ] normalize nodelta #EQdivide whd in ⊢ (??%% → ?); #EQ destruct
     685              ** change with (max (get_cond_bound ?) ?) in ⊢ (?%? → ?); #cond_bound
     686              [1,2: #Hz |*: *] #Hxs_ys whd in match (divide_continuation_on_frames ??);
     687              whd in match (append ???); whd in match (append ???); whd in match (append ???);
     688              <(append_nil … [ ? ; ?]) in ⊢ (?????%); >divide_continuation_on_frame_app
     689              >EQdivide normalize nodelta % // %
     690              [1,3,5,7: @(transitive_le … cond_bound)
     691                 [ >commutative_max @(max_1 flat_labels) @(max_1 flat_labels) //
     692                 | @(max_2 flat_labels) @(max_2 flat_labels) @(max_1 flat_labels) //
     693                 | @(max_2 flat_labels) @(max_1 flat_labels) //
     694                 | @(max_2 flat_labels) @(max_2 flat_labels) @(max_1 flat_labels) //
     695                 ]
     696              |*: @All_append // % // @(transitive_le … cond_bound)
     697                  @(max_2 flat_labels) @(max_2 flat_labels) @(max_2 flat_labels) //
     698              ]
     699        |*:
     700        ]
     701|5,6: #st1 #st1' #exp #ltrue #i_true #lfalse #i_false #new_m #EQcode_st1 change with (m_bind ?????) in ⊢ (??%? → ?);
     702      #EQeval cases(bind_inversion ????? EQeval) #curr_env * #EQcurr_env #H cases(bind_inversion ????? H) -H #b * #EQb
     703      whd in ⊢ (??%% → ?); #EQ destruct #EQcont_st1' #EQ destruct #EQstore #Hio1 #Hio2 #EQ1 #EQ2 #EQ3 #EQ4 destruct
     704      #Hclass_st1 #Hclass_st2 ****** #EQstore_12 >EQcode_st1 whd in ⊢ (???% → ?); #EQcode_s2 #EQcont_s2 #Hio2 #Hio3
     705      #Hstore1 #Hstore2 %{s2}
     706      [ %{(mk_state … (trans_var_instr … (code … st1'))
     707            (〈cost_act … (None ?),LOOP … (trans_cond exp) ltrue (trans_var_instr (code … st1')) lfalse (trans_var_instr i_false)〉::cont … s2)
     708            (store … st1') false)}
     709        %{(mk_state … (trans_var_instr … (code … st1'))
     710            (〈cost_act … (None ?),LOOP … (trans_cond exp) ltrue (trans_var_instr (code … st1')) lfalse (trans_var_instr i_false)〉::cont … s2)
     711            (store … st1') false)}   
     712     | %{(mk_state … (trans_var_instr … (code … st1')) (cont … s2) (store … st1') false)}
     713       %{(mk_state … (trans_var_instr … (code … st1')) (cont … s2) (store … st1') false)}
     714     ]
     715     %{(t_base …)} %
     716     [ @loop_true try assumption try % [2: <Hio2 @Hio3 % #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct]
     717     |3: @loop_false [6: @EQcode_s2 |*:] try assumption try % [2: <Hio2 @Hio3 % #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct]
     718     |*: %{(t_base …)} % [2,4: % % whd in ⊢ (??%? → ?); cases(trans_var_instr ?)
     719         [1,8: |2,9: #rt |3,10: #seq #opt_l #i |4,11: #cond #ltrue #i_true #lfalse #i_false #i
     720         |5,12: #cond #ltrue #i_true #lfalse #i |6,13: #f #act #opt_l #i |7,14: #lin *] normalize nodelta #EQ destruct ]
     721         % [2,4: %2 % * ]
     722         % [1,3: % [1,3: % // % // % [2,4: >EQcont_s2 >EQcont_st1' %] % //] <EQstore //
     723           |*: >EQstore >EQcont_st1' whd whd in match (divide_continuation_on_frames ??); whd in match (append ???);
     724               whd in match (append ???); [ <(append_nil … [?;?]) | <(append_nil … [?]) ]
     725               >divide_continuation_on_frame_app inversion(divide_continuation_on_frames ??) normalize nodelta
     726               [2,4: #x #xs #_] #EQdivide cases(store … st1) in Hstore2; * [2,4,6,8: #y #ys] #fp whd in ⊢ (% → ?);
     727               <(append_nil … [?])  >divide_continuation_on_frame_app >EQdivide normalize nodelta **
     728               change with (max (get_cond_bound ?) ?) in ⊢ (?%? → ?); #cond_bound whd in match (append ???);
     729               #H1 #H2 % // % // try (% //) @(transitive_le … cond_bound) @(max_2 flat_labels)
     730               [1,3: @(max_1 flat_labels) |*: @(max_2 flat_labels)] //
     731          ]
     732       ]
     733      cases(eval_cond_ok … EQcurr_env EQb)
     734      [2,5: cases (store … st1) in EQcurr_env Hstore1; *
     735            [1,3: #fp whd in ⊢ (??%% → ?); #EQ destruct]
     736            #hd #tl #fp whd in ⊢ (??%% → ?); #EQ destruct * //
     737      |3,6: @cond_bound_good_cond cases(store … st1) in EQcurr_env Hstore2; *
     738            [2,4: #hd #tl] #fp whd in ⊢ (??%% → ?); #EQ destruct whd in ⊢ (% → ?);
     739            inversion(divide_continuation_on_frames ??) [1,3: #_ *] #x #xs #_
     740            change with ([?] @ ?) in match ([?] @ ?);
     741            >divide_continuation_on_frame_app cases(divide_continuation_on_frames ??)
     742            normalize nodelta [2,4: #y #ys] whd in ⊢ (??%% → ?); #EQ destruct
     743            ** /2 by le_maxl/
     744      ] 
     745      #new_m * #EQnew_m #EQpop  whd in ⊢ (??%?); <EQstore_12  >EQnew_m normalize nodelta 
     746      >EQpop %
     747| #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 destruct cases H4
     748| #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 destruct
     749| #H46 #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 #H60 #H61 #H62 #H63 #H64 #H65 #H66 #H67 destruct
     750]
     751qed.
     752
     753definition var_stack_good_prog : Program frame_state_params frame_state_params frame_state_params → Prop ≝
     754λprog.All … (λx.get_instr_bound (f_body … x) ≤ f_pars frame_env_params … (f_sig … x)) (env … prog).
     755
     756lemma lookup_trans_ok : ∀prog : Program frame_state_params frame_state_params frame_state_params.∀f,env_it.
     757lookup … (env … prog) f = return env_it →
     758lookup … (env … (trans_var_prog prog)) f = return (mk_env_item …       
     759         (mk_signature stack_env_params stack_instr_params (f_name … (f_sig … env_it)) (f_pars … env_it) it)
     760         (f_lab … env_it)
     761         (trans_var_instr (f_body … env_it))).
     762* #en #main #init_lab #f * lapply f -f elim en -en
     763[ #f #sig #c_lab #body whd in ⊢ (??%% → ?); #EQ destruct]
     764* #sig #c_lab #body #xs #IH #f #sig' #c_lab' #body' whd in ⊢ (??%? → ?); @eq_function_name_elim
     765[ #EQ destruct normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct whd in ⊢ (??%?); @eq_function_name_elim // normalize nodelta
     766  * #ABS cases ABS %
     767| #DIFF normalize nodelta #H whd in ⊢ (??%?); normalize nodelta @eq_function_name_elim
     768  [ #EQ destruct cases DIFF * %] #_ normalize nodelta
     769  change with (env … (trans_var_prog (mk_Program ??? ? main init_lab))) in ⊢ (??(????%?)?); @IH //
     770]
     771qed.
     772
     773lemma lookup_prop_ok : ∀prog : Program frame_state_params frame_state_params frame_state_params.∀P,f,env_it.
     774lookup … (env … prog) f = return env_it → All … P (env … prog) →
     775P env_it.
     776* #en #main #init elim en -en
     777[ #P #f #env_it whd in ⊢ (??%% → ?); #EQ destruct ]
     778#x #xs #IH #P #f #env_it whd in ⊢ (??%? → ?); @eq_function_name_elim
     779[ #EQ destruct normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct] * //
     780#DIFF normalize nodelta #H1 * #_ @IH //
     781qed.
     782
     783lemma var_stack_simulate_call_general :
     784∀prog : Program frame_state_params frame_state_params frame_state_params.
     785∀bound : ℕ.
     786var_stack_good_prog prog →
     787∀s1.∀s2.∀s1'.∀f,l.
     788execute_l … (frame_sem_state_params bound) (env … prog) (call_act … f l) s1 s1' →
     789lang_classify … s1 ≠ cl_io → lang_classify … s1' ≠ cl_io →
     790frame_variable_sem_rel s1 s2 →
     791∃s2',s2'',s2'''.
     792∃t1: raw_trace … (operational_semantics … (stack_sem_state_params bound) (trans_var_prog prog)) s2 s2'.
     793execute_l … (stack_sem_state_params bound) (env … (trans_var_prog prog)) (call_act … f l) s2' s2'' ∧
     794∃t3: raw_trace … (operational_semantics … (stack_sem_state_params bound) (trans_var_prog prog)) s2'' s2'''.
     795frame_variable_sem_rel s1' s2''' ∧ silent_trace … t1 ∧ pre_silent_trace … t3 ∧
     796is_call_post_label …  (operational_semantics … (frame_sem_state_params bound) prog) s1 =
     797  is_call_post_label … (operational_semantics … (stack_sem_state_params bound) (trans_var_prog prog)) s2' ∧
     798  frame_variable_call_rel s1 s2'.
     799#prog #bound #good_prog #s1 #s2 #s1' #f #lab #H inversion H
     800[ #H1 #H2 * #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 destruct cases H11
     801| #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 destruct
     802|#H41 #H42 #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 #H60 #H61 #H62 #H63 destruct
     803| #H65 #H66 #H67 #H68 #H69 #H70 #H71 #H72 #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83 #H84 #H85 #H86 #H87 destruct
     804| #H89 #H90 #H91 #H92 #H93 #H94 #H95 #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107 #H108 #H109 #H110 destruct
     805| #H112 #H113 #H114 #H115 #H116 #H117 #H118 #H119 #H120 #H121 #H122 #H123 #H124 #H125 #H126 #H127 #H128 #H129 #H130 #H131 #H132 #H133 destruct
     806| #H135 #H136 #H137 #H138 #H139 #H140 #H141 #H142 #H143 #H144 #H145 #H146 #H147 #H148 #H149 #H150 #H151 #H152 #H153 #H154 destruct
     807|9: #H156 #H157 #H158 #H159 #H160 #H161 #H162 #H163 #H164 #H165 #H166 #H167 #H168 #H169 #H170 #H171 #H172 #H173 #H174 #H175 #H176 #H177 destruct
     808]
     809#st1 #st1' #f' #act_p #r_lb #i #mem #env_it #EQcode_st1 #EQenv_it change with (m_bind ?????) in ⊢ (??%? → ?);
     810#EQmem cases(bind_inversion ????? EQmem) #curr_env * #EQcurr_env #H cases(bind_inversion ????? H) -H #val * #EQval
     811#EQassign #EQ destruct #EQcode_st1' #EQcont_st1' #Hio1 #Hio2 #EQ1 #EQ2 #EQ3 #EQ4 destruct #Hclass1 #Hclass2 ******
     812#EQstore_12 >EQcode_st1 change with (list_combinators_to_instructions ??) in ⊢ (???% → ?); #EQcode_s2 #EQcont_s2
     813#Hio3 #Hio4 #Hstore1 #Hstore2
     814cases(eval_exp_ok … EQcurr_env EQval)
     815[2: cases (store … st1) in EQcurr_env Hstore1; *
     816   [1,3: #fp whd in ⊢ (??%% → ?); #EQ destruct]
     817   #hd #tl #fp whd in ⊢ (??%% → ?); #EQ destruct * //
     818|3,6: @expr_bound_good_expr cases(store … st1) in EQcurr_env Hstore2; *
     819      [2,4: #hd #tl] #fp whd in ⊢ (??%% → ?); #EQ destruct whd in ⊢ (% → ?);
     820      inversion(divide_continuation_on_frames ??) [1,3: #_ *] #x #xs #_
     821      change with ([?] @ ?) in match ([?] @ ?);
     822      >divide_continuation_on_frame_app cases(divide_continuation_on_frames ??)
     823      normalize nodelta [2,4: #y #ys] whd in ⊢ (??%% → ?); #EQ destruct
     824      ** /2 by le_maxl/
     825]
     826#new_st * #EQnew_st #EQpop %{(mk_state … (CALL … f' it r_lb (trans_var_instr i)) (cont … s2) new_st false)}
     827%{(mk_state … (trans_var_instr (f_body … env_it)) (〈ret_act … r_lb,trans_var_instr i〉 :: (cont … s2))
     828     (store … st1') false)}
     829%{(mk_state … (trans_var_instr (f_body … env_it)) (〈ret_act … r_lb,trans_var_instr i〉 :: (cont … s2))
     830     (store … st1') false)}
     831%{(create_silent_trace_from_eval_combinators (trans_var_prog prog) bound s2
     832          (mk_state … (CALL … f' it r_lb (trans_var_instr i)) (cont … s2) new_st false)
     833          (trans_expr act_p) …)}
     834try assumption
     835[1,2: <Hio3 @Hio4 % #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
     836| %
     837| <EQstore_12 assumption
     838]
     839%
     840[ @(call stack_state_params (stack_sem_state_params bound) (env … (trans_var_prog prog))
     841     (mk_state … (CALL … f' it r_lb (trans_var_instr i)) (cont … s2) new_st false)
     842     (mk_state … (trans_var_instr (f_body … env_it)) (〈ret_act … r_lb,trans_var_instr i〉 :: (cont … s2))
     843        (store … st1') false)
     844       f' it r_lb (trans_var_instr i) ?
     845       (mk_env_item …       
     846         (mk_signature stack_env_params stack_instr_params (f_name … (f_sig … env_it)) (f_pars … env_it) it)
     847         (f_lab … env_it)
     848         (trans_var_instr (f_body … env_it))) (refl …))
     849  [3: whd in ⊢ (??%?); >EQpop in ⊢ (??%?); normalize nodelta assumption |] try assumption try %
     850  @lookup_trans_ok //
     851]
     852%{(t_base …)} %
     853[ %
     854[2: whd in ⊢ (??%%); >EQcode_st1 % ] %
     855[2: % % whd in ⊢ (??%? → ?); cases(trans_var_instr ?)
     856    [| #rt | #seq #opt_l #i | #cond #ltrue #i_true #lfalse #i_false #i | #cond #ltrue #i_true #lfalse #i | #f #act #opt_l #i |
     857            #lin *] normalize nodelta #EQ destruct ] %
     858[2: % @(create_silent_trace_from_eval_combinators_ok … (refl …)) ]
     859% [ % [ % // % // % [2: >EQcont_s2 >EQcont_st1' % ] % // ] @(var_to_shift_frame_assign_var_ok … EQassign) % // ]
     860@(var_instr_bond_frame_assign_var_ok … EQassign) >EQcont_st1' %
     861[ % // >list_n_def >EQcode_st1' @(transitive_le … (lookup_prop_ok … EQenv_it good_prog)) /2 by le_plus_to_minus/ ]
     862<(append_nil … [i]) >divide_continuation_on_frame_app inversion(divide_continuation_on_frames …) normalize nodelta
     863[2: #y #ys #_] #EQdivide cases(store … st1) in Hstore2; *
     864[2,4: #z #zs] #fp whd in ⊢ (% → ?); <(append_nil … [?]) >divide_continuation_on_frame_app
     865>EQdivide normalize nodelta ** change with (max ??) in ⊢ (?%? → ?); #act_bound #H1 #H2 % //
     866% /2 by le_maxl/
     867]
     868% // %{f'} %{act_p} %{r_lb} %{i} % //
     869qed.
     870
     871lemma var_stack_simulate_return_general :
     872∀prog : Program frame_state_params frame_state_params frame_state_params.
     873∀bound : ℕ.
     874∀s1.∀s2.∀s1'.∀l.
     875execute_l … (frame_sem_state_params bound) (env … prog) (ret_act … l) s1 s1' →
     876lang_classify … s1 ≠ cl_io → lang_classify … s1' ≠ cl_io →
     877frame_variable_sem_rel s1 s2 →
     878∃s2',s2'',s2'''.
     879∃t1: raw_trace … (operational_semantics … (stack_sem_state_params bound) (trans_var_prog prog)) s2 s2'.
     880execute_l … (stack_sem_state_params bound) (env … (trans_var_prog prog)) (ret_act … l) s2' s2'' ∧
     881∃t3: raw_trace … (operational_semantics … (stack_sem_state_params bound) (trans_var_prog prog)) s2'' s2'''.
     882frame_variable_sem_rel s1' s2''' ∧ pre_silent_trace … t1 ∧ pre_silent_trace … t3
     883∧ Rrel … (frame_variable_pass_rel prog (trans_var_prog prog) bound) s1' s2''.
     884#prog #bound #s1 #s2 #s1' #l #H inversion H
     885[ #H1 #H2 * #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 destruct
     886  cases H31
     887| #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 destruct
     888| #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 #H71 #H72 #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83 destruct
     889| #H85 #H86 #H87 #H88 #H89 #H90 #H91 #H92 #H93 #H94 #H95 #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107 destruct
     890| #H109 #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 #H119 #H120 #H121 #H122 #H123 #H124 #H125 #H126 #H127 #H128 #H129 #H130 destruct
     891| #H132 #H133 #H134 #H135 #H136 #H137 #H138 #H139 #H140 #H141 #H142 #H143 #H144 #H145 #H146 #H147 #H148 #H149 #H150 #H151 #H152 #H153 destruct
     892| #H155 #H156 #H157 #H158 #H159 #H160 #H161 #H162 #H163 #H164 #H165 #H166 #H167 #H168 #H169 #H170 #H171 #H172 #H173 #H174 destruct
     893| #H176 #H177 #H178 #H179 #H180 #H181 #H182 #H183 #H184 #H185 #H186 #H187 #H188 #H189 #H190 #H191 #H192 #H193 #H194 #H195 #H196 #H197 #H198 destruct
     894]
     895* #code_st1 #cont_st1 #store_st1 #io_info_st1 #st1' #r_t #new_st #tail #rb #instr #EQcode_st1 #EQcont_st1 #EQ destruct #Hio1 #Hio2 destruct
     896whd in ⊢ (??%? → ?); cases(store_st1) -store_st1 * [ #fp whd in ⊢ (??%% → ?); #EQ destruct] #curr_env #tail * #fp1 #fp2 normalize nodelta
     897#EQnew_st cases(bind_inversion ????? EQnew_st) #val * #EQval whd in ⊢ (??%% → ?); #EQ destruct #EQ destruct #EQstore_st1' #EQ1 #EQ2 #EQ3 #EQ4
     898destruct #Hclass1 #Hclass2 ****** #EQstore_12 change with (list_combinators_to_instructions ??) in ⊢ (???% → ?); #EQcode_s2
     899whd in ⊢ (???% → ?); #EQcont_s2 #Hio1 #_ * #H1 #Hstore1 ** whd in ⊢ (?%? → ?); #rt_good * #Hstore2
     900cases(eval_exp_ok … 〈curr_env::tail,〈fp1,fp2〉〉 … (refl …) EQval) [2,3: /2 by expr_bound_good_expr/]
     901#mem * #EQmem #EQpop
     902%{(mk_state … (RETURN … it) (cont … s2) mem false)}
     903%{(mk_state … (trans_var_instr (code … st1')) (foldr … (λx,tail.〈\fst x,trans_var_instr (\snd x)〉::tail) [ ] (cont … st1')) (store … st1') false)}
     904%{(mk_state … (trans_var_instr (code … st1')) (foldr … (λx,tail.〈\fst x,trans_var_instr (\snd x)〉::tail) [ ] (cont … st1')) (store … st1') false)}
     905%{(create_silent_trace_from_eval_combinators (trans_var_prog prog) bound s2 …)} try assumption try %
     906[1,2: //
     907| <EQstore_12 assumption
     908| @(ret_instr … it … (refl …) … (refl …) … (refl …)) // try assumption
     909  whd in ⊢ (??%?); >EQpop whd in EQpop : (??%%); cases mem in EQpop; * [2: * [2: #w #ws] #zs] #fp normalize nodelta
     910  whd in ⊢ (??%% → ?); #EQ destruct >m_return_bind >EQstore_st1' %
     911]
     912%{(t_base …)} %
     913[ % [2: % %  whd in ⊢ (??%? → ?); cases(trans_var_instr ?)
     914    [| #rt | #seq #opt_l #i | #cond #ltrue #i_true #lfalse #i_false #i | #cond #ltrue #i_true #lfalse #i | #f #act #opt_l #i |
     915            #lin *] normalize nodelta #EQ destruct]
     916% [2: @(create_silent_trace_from_eval_combinators_ok … (refl …))]
     917% [ % [ % // % // % // % //] ] >EQstore_st1' assumption
     918]
     919#s3 #s3' * #EQcont_s31' inversion(code …)
     920  [| #rt | #seq #opt_l #i #_ | #cond #ltrue #i_true #lfalse #i_false #i #_ #_ #_ | #cond #ltrue #i_true #lfalse #i #_ #_ | #f #act #opt_l #i #_ |
     921            #lin *] #EQcode_s3 normalize nodelta [6: |*: *] #EQ destruct * #EQcont_s3' * #f' * #act' * #opt_l' * #i' *
     922  #H >H in EQcode_s3; #EQ destruct #EQcode_s3' % [ >EQcont_s3' <EQcont_s31' % | >EQcode_s3' %]
     923qed.
     924
    617925
    618926
     
    620928∀prog : Program frame_state_params frame_state_params frame_state_params.
    621929∀bound: ℕ.
     930var_stack_good_prog prog → get_instr_bound (main … prog) ≤ bound - to_shift →
    622931simulation_conditions … (frame_variable_pass_rel prog (trans_var_prog prog) bound) ≝
    623 λprog,bound.
     932λprog,bound,good_prog,good_main.
    624933mk_simulation_conditions ….
    625 [ @var_initial_stack_initial | @var_final_stack_final | @var_io_is_stack_io
    626 | @var_stack_simulate_tau
    627 qed.
     934[ @var_initial_stack_initial // | #H1 #H2 #H3 #H4 @var_final_stack_final //
     935| @var_io_is_stack_io | @var_stack_simulate_tau
     936| @var_stack_simulate_label
     937| #s1 #s2 #s1' #f #lbl #post #exe #class1 #class2 #rel
     938  cases(var_stack_simulate_call_general … exe class1 class2 rel) //
     939  #s2' * #s2'' * #s2''' * #t1 * #exe' *#t3 **** #rel' #sil1 #sil2 #Hpost #_
     940  %{s2'} %{s2''} %{s2'''} %{t1} % [ %{exe'} <Hpost assumption] %{t3}
     941  % [ %{rel'} ]  assumption
     942| #s1 #s2 #s1' #lbl #exe #class1 #class2 #rel
     943  cases(var_stack_simulate_return_general … exe class1 class2 rel)
     944  #s2' * #s2'' * #s2''' * #t1 * #exe' * #t3 *** #rel' #sil1 #sil2 #_
     945  %{s2'} %{s2''} %{s2'''} %{t1} %{exe'} %{t3} % [% ] try assumption  % assumption
     946| #s1 #s2 #s1' #f #lbl #exe #post #class1 #class2 #rel
     947  cases(var_stack_simulate_call_general … exe class1 class2 rel) //
     948  #s2' * #s2'' * #s2''' * #t1 * #exe' *#t3 **** #rel' #sil1 #sil2 #Hpost #Hcall
     949  %{s2'} %{s2''} %{s2'''} %{t1} % [ % // <Hpost assumption ] %{t3}
     950  % // % [%] assumption
     951| #s1 #s2 #s1' #exe #class1 #class2 #rel
     952  cases(var_stack_simulate_return_general … exe class1 class2 rel)
     953  #s2' * #s2'' * #s2''' * #t1 * #exe' * #t3 *** #rel' #sil1 #sil2 #HR
     954  %{s2'} %{s2''} %{s2'''} %{t1} %{exe'} %{t3} % [ % [%] ] assumption
     955|*: cases daemon (*todo per giulio*)
     956]
     957qed.
Note: See TracChangeset for help on using the changeset viewer.