source: LTS/variable_stack_pass.ma @ 3586

Last change on this file since 3586 was 3586, checked in by pellitta, 4 years ago
File size: 56.9 KB
Line 
1(**************************************************************************)
2(*       ___                                                              *)
3(*      ||M||                                                             *)
4(*      ||A||       A project by Andrea Asperti                           *)
5(*      ||T||                                                             *)
6(*      ||I||       Developers:                                           *)
7(*      ||T||         The HELM team.                                      *)
8(*      ||A||         http://helm.cs.unibo.it                             *)
9(*      \   /                                                             *)
10(*       \ /        This file is distributed under the terms of the       *)
11(*        v         GNU General Public License Version 2                  *)
12(*                                                                        *)
13(**************************************************************************)
14
15include "common_variable_stack.ma".
16include "stack.ma".
17
18let rec trans_expr (e : expr) on e : list guard_combinators ≝
19match e with
20[ Var v ⇒ [push_var v]
21| Const n ⇒ [push_const n]
22| Plus e1 e2 ⇒ trans_expr e1 @ trans_expr e2 @ [push_plus]
23| Minus e1 e2 ⇒ trans_expr e1 @ trans_expr e2 @ [push_minus]
24].
25
26let rec trans_cond  (c : condition) on c : list guard_combinators ≝
27match c with
28[ Eq e1 e2 ⇒ trans_expr e1 @ trans_expr e2 @ [push_eq]
29| Not c ⇒ trans_cond c @ [push_not]
30].
31
32definition list_combinators_to_instructions : list guard_combinators → stack_Instructions → stack_Instructions ≝
33λl,i.foldr … (λc,instr.SEQ stack_state_params flat_labels (push c) (None ?) instr) i l.
34
35let rec trans_var_instr (i : frame_Instructions) on i : stack_Instructions ≝
36match i with
37[ EMPTY ⇒ EMPTY …
38| RETURN exp ⇒ list_combinators_to_instructions (trans_expr exp) (RETURN … it)
39| SEQ seq opt_l instr ⇒
40  let t_instr ≝ trans_var_instr … instr in
41  match seq with
42  [ Seq_i seq' ⇒
43     match seq' with
44     [ sAss v e ⇒ list_combinators_to_instructions (trans_expr e) (SEQ … (pop_Ass v) opt_l t_instr)
45     ]
46  | PopReg v ⇒ SEQ stack_instr_params ? (popreg v) opt_l t_instr
47  ]
48| COND cond ltrue i_true lfalse i_false instr ⇒
49  let t_i_true ≝ trans_var_instr … i_true in
50  let t_i_false ≝ trans_var_instr … i_false in
51  let t_instr ≝ trans_var_instr … instr in
52  list_combinators_to_instructions (trans_cond cond) (COND … it ltrue t_i_true lfalse t_i_false t_instr)
53| LOOP cond ltrue i_true lfalse instr ⇒
54  let t_i_true ≝ trans_var_instr … i_true in
55  let t_instr ≝ trans_var_instr … instr in
56   LOOP stack_state_params flat_labels (trans_cond … cond) ltrue t_i_true lfalse t_instr
57| CALL f act_p opt_l instr ⇒
58  let t_instr ≝ trans_var_instr … instr in
59  list_combinators_to_instructions (trans_expr act_p) (CALL … f it opt_l t_instr)
60| IO lin io lout instr ⇒ ?
61].
62cases io
63qed.
64
65definition trans_var_prog :
66 Program frame_env_params frame_instr_params flat_labels →
67 Program stack_env_params stack_instr_params flat_labels ≝
68λprog.
69let t_main ≝ trans_var_instr … (main … prog) in
70 (mk_Program …
71  (foldr …
72   (λx,tail.(let t_body ≝ trans_var_instr … (f_body … x) in
73     mk_env_item …       
74     (mk_signature stack_env_params stack_instr_params (f_name … (f_sig … x)) (f_pars … x) it) (f_lab … x) t_body) :: tail)
75   (nil ?) (env … prog))
76  t_main (initial_act … prog)).
77
78include "Simulation.ma".
79
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
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   
114definition frame_variable_pass_rel :
115∀prog : Program frame_state_params frame_state_params frame_state_params.
116∀t_prog : Program stack_env_params stack_instr_params flat_labels.
117∀bound : ℕ.
118relations flat_labels (operational_semantics frame_state_params (frame_sem_state_params bound) prog)
119(operational_semantics stack_state_params (stack_sem_state_params bound) t_prog) ≝
120λprog,t_prog,bound.
121(mk_relations flat_labels (operational_semantics frame_state_params (frame_sem_state_params bound) prog)
122 (operational_semantics stack_state_params (stack_sem_state_params bound) t_prog)
123 frame_variable_sem_rel
124 frame_variable_call_rel).
125
126let rec expr_fv (e : expr) on e : list variable ≝
127match e with
128[ Var v ⇒ [v]
129| Const n ⇒ []
130| Plus e1 e2 ⇒ expr_fv e1 @ expr_fv e2
131| Minus e1 e2 ⇒ expr_fv e1 @ expr_fv e2
132].
133
134definition good_expr ≝  λbound : ℕ.λe : expr.All … (λv.v < bound) (expr_fv e).
135
136let rec cond_fv (c : condition) on c : list variable ≝
137match c with
138[ Eq e1 e2 ⇒ expr_fv e1 @ expr_fv e2
139| Not c1 ⇒ cond_fv c1
140].
141
142definition good_cond ≝ λbound : ℕ.λc : condition.All … (λv.v < bound) (cond_fv c).
143
144lemma good_expr_monotone : ∀n1,n2.∀e.n1 ≤ n2 → good_expr n1 e →
145good_expr n2 e.
146#n1 #n2 #e lapply n1 -n1 lapply n2 -n2 elim e //
147[ #v #n1 #n2 #H * #H1 * % /2/
148|*: #e1 #e2 #IH1 #IH2 #n1 #n2 #H #H1 cases(All_inv_append … H1) #H3 #H4 @All_append /2/
149]
150qed.
151
152lemma frame_sem_exp_cons : ∀env.∀e.∀n1,n2.
153to_shift ≤ |env| →
154good_expr (|env| - to_shift) e →
155frame_sem_expr env e = return n1 →
156frame_sem_expr (n2 :: env) e = return n1.
157#env #e lapply env -env elim e
158[ #v #env #n1 #n2 #prf1 * #Hv *
159 whd in ⊢ (??%% → ?); #H change with (nth_opt ???) in ⊢ (??%?);
160 change with ([?]@?) in match ([?]@?); >nth_second
161 [ >length_append whd in ⊢ (???%); <H @eq_f2 // normalize <minus_n_O <minus_n_O
162   >(eq_minus_S_pred ? O) <minus_n_O >(eq_minus_S_pred ? O) <minus_n_O
163   >(eq_minus_S_pred ? O) <minus_n_O @eq_f <(eq_minus_S_pred ? (S v)) %
164 | normalize <minus_n_O >minus_minus_comm @le_plus_to_minus_r
165   @(transitive_le … (monotonic_le_plus_r 1 ?? Hv)) normalize <(minus_Sn_m 2) //
166 ]
167| #n #env #n1 #n2 #prf1 * normalize //
168|*: #e1 #e2 #IH1 #IH2 #env #n1 #n2 #prf1 #H cases(All_inv_append … H) -H #H1 #H2
169  change with (m_bind ?????) in ⊢ (??%? → ?); #H cases(bind_inversion ????? H) -H
170  #n3 * #EQn3 #H cases(bind_inversion ????? H) -H #n4 * #EQn4 whd in ⊢ (??%% → ?);
171  #EQ destruct change with (m_bind ?????) in ⊢ (??%?); >(IH1 … EQn3) //
172  >(IH2 … EQn4) //
173]
174qed.
175
176
177lemma eval_exp_ok : ∀st.∀env:activation_frame.∀e: expr.∀n.
178to_shift ≤ |env| → good_expr (|env| - to_shift) e →
179frame_current_env … st = return env →
180frame_sem_expr env e = return n →
181∃st'.m_fold Option … eval_combinators (trans_expr e) st = return st' ∧
182pop st' = return 〈n,st〉.
183** [| #curr_env #rem] #sp_fp #env #e #n #H1 #H2 normalize in ⊢ (% → ?); #EQ destruct
184lapply n -n lapply H1 -H1 lapply H2 -H2 lapply env -env elim e
185[ #v #env #_ #_ #n whd in ⊢ (??%% → ?); #H %{(〈(n::env)::rem,sp_fp〉)} % try %
186  whd in ⊢ (??%?); whd in match eval_combinators; normalize nodelta
187  whd in match frame_current_env; normalize nodelta whd in match option_hd; normalize nodelta
188  >m_return_bind whd in match read_frame; normalize nodelta >H %
189| #n #env #_ #_ #m whd in ⊢ (??%% → ?); #EQ destruct %{(〈(m::env)::rem,sp_fp〉)} %%
190|*: #e1 #e2 #IH1 #IH2 #env #H1 #H2 #n change with (m_bind ?????) in ⊢ (??%? → ?);
191  #H cases(bind_inversion ????? H) -H #n1 * #EQn1
192  #H cases(bind_inversion ????? H) -H #n2 * #EQn2
193  whd in ⊢ (??%% → ?); #EQ destruct
194  [ %{(〈((n1 + n2)::env)::rem,sp_fp〉)} | %{(〈((n1 - n2)::env)::rem,sp_fp〉)} ]
195  >m_fold_append cases(IH1 … EQn1) // [2,4: cases(All_inv_append … H1) //] #st1 * #EQst1 #EQpop1 >EQst1
196  >m_return_bind >m_fold_append cases(IH2 … (n1 :: env))
197  [2,7: cases(All_inv_append … H1) #H1 #H2 @(good_expr_monotone … H2) normalize /2/
198  |3,8: normalize /2/
199  |5,10: @(frame_sem_exp_cons … EQn2) // cases(All_inv_append … H1) //
200  |4,9:
201  ]
202  #st2 * #EQst2 #EQpop2 cases st1 in EQst1 EQpop1; * [2,4: #env' #rem'] #fp_sp' #EQst1
203  [3,4: whd in ⊢ (??%% → ?); #EQ destruct ] cases env' in EQst1; [2,4: #val1 #env''] #EQst1
204  whd in ⊢ (??%% → ?); #EQ destruct >EQst2 >m_return_bind % [2,4: %] whd in ⊢ (??%?);
205  whd in match eval_combinators; normalize nodelta >EQpop2 %
206]
207qed.
208
209lemma eval_cond_ok :  ∀st.∀env:activation_frame.∀c: condition.∀b.
210to_shift ≤ |env| → good_cond (|env| - to_shift) c →
211frame_current_env … st = return env →
212frame_sem_condition env c = return b →
213∃st'.m_fold Option … eval_combinators (trans_cond c) st = return st' ∧
214pop st' = Some ? 〈if b then 1 else O,st〉.
215** [| #curr_env #rem] #sp_fp #env #c #b #H1 #H2 normalize in ⊢ (% → ?); #EQ destruct
216lapply b -b lapply H1 -H1 lapply H2 -H2 lapply env -env elim c
217[ #e1 #e2 #env #H #H1 #b change with (m_bind ?????) in ⊢ (??%? → ?); #H cases(bind_inversion ????? H) -H
218  #n * #EQn #H cases(bind_inversion ????? H) -H #m * #EQm whd in ⊢ (??%% → ?); #EQ destruct
219  %{(〈((if (eqb n m )then 1 else O) :: env)::rem,sp_fp〉)} >m_fold_append
220  cases(eval_exp_ok … EQn) //
221  [2: @(〈env::rem,sp_fp〉) |3: cases(All_inv_append … H) // |4: %]
222  #st1 * #EQst1 #EQpop1 >EQst1 >m_return_bind % // >m_fold_append
223  cases st1 in EQst1 EQpop1; * [| * [| #m' #env'] #rem'] #sp_fp' #EQst1 whd in ⊢ (??%% → ?);
224  #EQ destruct cases(eval_exp_ok … (frame_sem_exp_cons … EQm))
225  [2: @(〈(n::env)::rem,sp_fp〉) |5: % |3: @(transitive_le … H1) //
226  |4: @(good_expr_monotone … (|env| - to_shift)) [ /2/ | cases(All_inv_append … H) //]
227  |6: cases(All_inv_append … H) // |7: // |8:]
228  #st2 * #EQst2 #EQpop2 >EQst2 >m_return_bind change with (m_bind ?????) in ⊢ (??%?);
229  whd in match eval_combinators; normalize nodelta >EQpop2 %
230| #c1 #IH #env #H1 #H2 #b change with (m_bind ?????) in ⊢ (??%? → ?);
231  #H cases(bind_inversion ????? H) -H #b1 * #EQb1 whd in ⊢ (??%% → ?); #EQ destruct
232  %{(〈((if (if b1 then false else true) then 1 else O) :: env)::rem,sp_fp〉)} % //
233  >m_fold_append cases(IH … EQb1) // #st1 * #EQst1 #EQpop1 >EQst1 >m_return_bind
234  change with (m_bind ?????) in ⊢ (??%?); whd in match eval_combinators; normalize nodelta
235  >EQpop1 >m_return_bind whd in ⊢ (??%?); @eq_f @eq_f2 // cases b1 //
236]
237qed.
238
239definition safe_cast : ∀A,B : Type[0].A = B → A → B ≝
240λA,B,prf.match prf with [refl ⇒ λx : A.x].
241
242let rec create_silent_trace_from_eval_combinators (prog : Program stack_env_params stack_instr_params flat_labels)
243(bound : ℕ) (st,st' : state stack_state_params) (l : list guard_combinators) 
244on l :
245 m_fold Option … eval_combinators l (store … st) = return (store … st') →
246  code … st = list_combinators_to_instructions l (code … st') →
247  cont … st = cont … st' → io_info … st = false → io_info … st = io_info … st' →
248  raw_trace … (operational_semantics stack_state_params (stack_sem_state_params bound) prog) st st' ≝
249match l return λx.(m_fold Option … eval_combinators x ? = ? → ? = list_combinators_to_instructions x ? → ?) with
250[ nil ⇒ λprf1,prf2,prf3,prf4,prf5.safe_cast (raw_trace … (operational_semantics stack_state_params (stack_sem_state_params bound) prog) st st)
251     (raw_trace … (operational_semantics stack_state_params (stack_sem_state_params bound) prog) st st') ? (t_base ?? st)
252| cons x xs ⇒ λprf1,prf2,prf3,prf4,prf5.
253   let next_store ≝ (opt_safe … (eval_combinators x (store … st)) ?) in
254   let next_st ≝ mk_state stack_state_params (list_combinators_to_instructions xs (code … st')) (cont … st')
255                   next_store (io_info … st') in
256   let tail ≝ create_silent_trace_from_eval_combinators prog bound next_st st' xs ? (refl …) (refl …) ? (refl …) in
257   t_ind … (cost_act … (None ?)) … tail
258].
259@hide_prf
260[ cases st in prf1 prf2 prf3 prf4 prf5; cases st'  #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 whd in ⊢ (??%% → ??%% → ?);
261 #H9 #H10 #H11 #H12 #H13 destruct %
262|5: change with (m_bind ?????) in prf1 :(??%?); cases(bind_inversion ????? prf1) -prf1 #w * #EQw #_ >EQw %
263   whd in ⊢ (??%% → ?); #EQ destruct
264| whd @seq_sil
265  [4: >prf2 in ⊢ (??%?); %
266  |8: %
267  |5: change with (eval_combinators ??) in ⊢ (??%?); normalize nodelta @opt_safe_elim #w #H assumption
268  |6: %
269  |7: assumption
270  |9,10: // normalize nodelta <prf5 //
271  |*:
272  ]
273| normalize nodelta @opt_safe_elim #w #EQw change with (m_bind ?????) in prf1 :(??%?); >EQw in prf1;
274  >m_return_bind //
275| normalize nodelta <prf5 //
276]
277qed.
278
279lemma create_silent_trace_from_eval_combinators_ok : ∀prog,bound,st,st',l,prf1,prf2,prf3,prf4,prf5,t.
280create_silent_trace_from_eval_combinators prog bound st st' l prf1 prf2 prf3 prf4 prf5 = t →
281pre_silent_trace … t.
282#prog #bound #st #st' #l lapply st -st lapply st' -st' elim l
283[ * #code' #cont' #store' #io' * #code #cont #store #io whd in ⊢ (??%% → ??%% → ?); #EQ destruct #EQ1 #EQ2 #EQ3 #EQ4 destruct
284  #t whd in ⊢ (??%% → ?); #EQ destruct % % whd in ⊢ (??%% → ?); cases code' -code' normalize nodelta
285  [| #rt | #seq #opt_l #i | #cond #ltrue #i_true #lfalse #i_false #i | #cond #ltrue #i_true #lfalse #i | #f #act #opt_l #i |
286    #lin *]
287  #EQ destruct
288| #x #xs #IH #st' #st #H cases(bind_inversion ????? H) #w * #EQw #EQstore_st'
289  whd in ⊢ (???% → ?); change with (list_combinators_to_instructions ??) in match (foldr ?????);
290  #prf2 #EQcont #Hio #EQio #t whd in ⊢ (??%? → ?); #EQ destruct %2
291  [2: @IH try % (*?????? possibile baco!!!!!*) ]
292  % whd in ⊢ (??%% → ?); cases(code … st)
293  [| #rt | #seq #opt_l #i | #cond #ltrue #i_true #lfalse #i_false #i | #cond #ltrue #i_true #lfalse #i | #f #act #opt_l #i |
294    #lin *] normalize nodelta [ >Hio normalize nodelta] #EQ destruct
295]
296qed.
297(*  [ @opt_safe_elim #w' >EQw whd in ⊢ (??%% → ?); #EQ destruct assumption
298  | %
299  | % c'e' un baco????*)
300
301
302
303lemma list_n_def : ∀A,n,a.(|list_n A a n|) = n.
304#A #n elim n // #m #IH #a normalize @eq_f @IH
305qed.
306
307
308
309lemma var_initial_stack_initial : ∀prog,bound.
310get_instr_bound (main … prog) ≤ bound - to_shift →
311∀s1.∀s2.
312bool_to_Prop (lang_initial ? (frame_sem_state_params bound) prog s1) →
313bool_to_Prop (lang_initial ? (stack_sem_state_params bound)  (trans_var_prog prog) s2) →
314frame_variable_sem_rel s1 s2.
315#prog #bound #Hbound #s1 #s2 #H cases(andb_Prop_true … H) -H #H cases(andb_Prop_true … H) -H
316#H cases(andb_Prop_true … H) -H @eq_instructions_elim #EQcode_s1 * @eqb_list_elim #EQcont_s1 *
317normalize in match (init_store ??); #EQstore_s1 #Hio1
318#H cases(andb_Prop_true … H) -H #H cases(andb_Prop_true … H) -H #H cases(andb_Prop_true … H) -H
319@eq_instructions_elim #EQcode_s2 * @eqb_list_elim #EQcont_s2 * normalize in match (init_store ??);
320#EQstore_s2 #Hio2 %
321[ % [ % [ % [ % [ % [ >(\P (bool_as_Prop_to_eq … EQstore_s1)) >(\P (bool_as_Prop_to_eq … EQstore_s2)) %
322                    |  >EQcode_s1 >EQcode_s2 %
323                    ]
324                | >EQcont_s1 >EQcont_s2 %
325                ]
326            | >Hio1 >Hio2 %
327            ]
328        | >EQcode_s1 * #H cases H %
329        ]
330    | >(\P (bool_as_Prop_to_eq … EQstore_s1)) normalize % /2/
331    ]
332| >(\P (bool_as_Prop_to_eq … EQstore_s1)) >EQcode_s1 >EQcont_s1 whd %
333  [ % // % [ @(transitive_le … Hbound) normalize >list_n_def <minus_n_O /2/]
334  % normalize //
335  ]
336@I
337]
338qed.
339
340
341lemma var_final_stack_final : ∀s1,s2.frame_variable_sem_rel s1 s2 →
342bool_to_Prop(lang_final … s1) → bool_to_Prop (lang_final … s2).
343#s1 #s2 ****** #EQstore #EQcode #EQcont #Hio1 #_ #_ #_ #H cases(andb_Prop_true … H) -H
344@eq_instructions_elim #EQinstr * cases(cont … s1) in EQcont; [|#x #xs #_ *]
345whd in ⊢ (??%% → ?); #EQcont_s2 #_ @andb_Prop [ >EQcode >EQinstr @I | >EQcont_s2 @I]
346qed.
347
348lemma var_io_is_stack_io :∀s1,s2.frame_variable_sem_rel s1 s2 → lang_classify ? s2 = cl_io → lang_classify ? s1 = cl_io.
349#s1 #s2 whd in match frame_variable_sem_rel; normalize nodelta ****** #_ #EQcode #_ #Hio1 #_ #_ #_
350whd in match lang_classify; normalize nodelta cases (code … s2) in EQcode; normalize nodelta
351[| #rt | #seq #opt_l #i | #cond #ltrue #i_true #lfalse #i_false #i | #cond #ltrue #i_true #lfalse #i | #f #act #opt_l #i |
352    #lin *] [2,3,4,5,6: #_ #EQ destruct] cases (code … s1)
353[| #rt | #seq #opt_l #i | #cond #ltrue #i_true #lfalse #i_false #i | #cond #ltrue #i_true #lfalse #i | #f #act #opt_l #i |
354    #lin *]  whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
355[2: cases(trans_expr rt) in EQ; [2: #x #xs] whd in ⊢ (????%→ ?); #EQ destruct
356|3: cases seq in EQ; normalize nodelta [2: #v #EQ destruct] * #v #e normalize nodelta cases(trans_expr ?)
357    [2: #x #xs] whd in ⊢ (????%→ ?); #EQ destruct
358|4: cases(trans_cond ?) in EQ; [2: #x #xs] whd in ⊢ (????%→ ?); #EQ destruct
359|5: cases(trans_expr act) in EQ; [2: #x #xs] whd in ⊢ (????%→ ?); #EQ destruct
360]
361normalize nodelta >Hio1 //
362qed.
363
364lemma divide_continuation_on_frame_app : ∀ct,z,app.divide_continuation_on_frames ct (app @ z) =
365match divide_continuation_on_frames ct z with
366[ nil ⇒ [app @ z] | cons x xs ⇒ (app @ x) :: xs ].
367#ct elim ct
368[ #z #app whd in ⊢ (??%%); % ]
369** [#f #lbl |*: #opt_l] #i #tl #IH #z #ap whd in ⊢ (??%%); // whd in match (divide_continuation_on_frames ??) in ⊢ (???%);
370>associative_append >IH inversion(divide_continuation_on_frames …) // #ABS @⊥ lapply ABS -ABS lapply z -z lapply i -i
371elim tl [1,3: #i #z whd in ⊢ (??%% → ?); #EQ destruct] * #y1 #y2 #ys #IH #i #z cases y1
372[1,4: #f #lbl |*: #opt_l] whd in ⊢ (??%? → ?); try @IH #EQ destruct
373qed.
374
375lemma divide_continuation_on_frame_app_nil_is_nil : ∀ct,app.divide_continuation_on_frames ct app = [ ] →
376app = [ ].
377#ct elim ct [ #app whd in ⊢ (??%% → ?); #H destruct]
378* #x1 #x2 #xs #IH #app whd in ⊢ (??%% → ?); cases x1 [#f #lbl |*: #opt_l] normalize nodelta
379#H destruct lapply(IH … H) elim app // #z #zs #_ whd in match (append ???); #EQ destruct
380qed.
381
382lemma var_instr_bond_for_empty : ∀st,x,opt_l,cd,ct.
383var_instr_bond_ok st x (〈cost_act … opt_l,cd〉::ct) →
384var_instr_bond_ok st cd ct.
385#st #x #opt_l #cd #ct whd in ⊢ (% → %); whd in match (divide_continuation_on_frames ??);
386whd in match (divide_continuation_on_frames ??) in ⊢ (? → %); >divide_continuation_on_frame_app
387inversion(divide_continuation_on_frames ??)
388[ #ABS lapply(divide_continuation_on_frame_app_nil_is_nil … ABS) #EQ destruct]
389#y #ys #_ #EQdivide normalize nodelta cases st -st [ *]
390#z #zs * #H1 #H2 % // cases H1 //
391qed.
392
393definition get_top_expression_from_instr : frame_Instructions → option expr ≝
394λi.match i with
395[ EMPTY ⇒ None ?
396| RETURN exp ⇒ return exp
397| SEQ seq opt_l instr ⇒
398  match seq with
399  [ Seq_i seq' ⇒
400     match seq' with
401     [ sAss v e ⇒ return e
402     ]
403  | PopReg v ⇒ None ?
404  ]
405| COND cond ltrue i_true lfalse i_false instr ⇒ None ?
406| LOOP cond ltrue i_true lfalse instr ⇒ None ?
407| CALL f act_p opt_l instr ⇒ return act_p
408| IO lin io lout instr ⇒ ?
409].
410cases io
411qed.
412
413lemma expr_bound_good_expr : ∀e,n.get_expr_bound e ≤ n →
414good_expr n e.
415#e elim e normalize /2/ #e1 #e2 #IH1 #IH2 #n #H @All_append try @IH1 try @IH2
416change with (max (get_expr_bound e1) (get_expr_bound e2)) in H : (?%?);
417@(transitive_le … H) /2 by le_maxl/
418qed.
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.
425
426lemma good_expr_for_var_instr_ok : ∀x,st,cd,ct,e.
427var_instr_bond_ok (x :: st) cd ct →
428get_top_expression_from_instr cd = return e →
429good_expr (|x|-to_shift) e.
430#x #st #cd #ct #e whd in ⊢ (% → ?); inversion(divide_continuation_on_frames ??)
431[ #ABS lapply(divide_continuation_on_frame_app_nil_is_nil … ABS) #EQ destruct]
432#y #ys #_ normalize nodelta <(append_nil … [cd]) >divide_continuation_on_frame_app
433cases(divide_continuation_on_frames ??) [|#z #zs] normalize nodelta
434[>append_nil | whd in match (append ???); whd in match (append ???); ]
435#EQ destruct ** #H #_ #_ cases cd in H; -cd
436[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
437|5,12: #cond #ltrue #i_true #lfalse #i |6,13: #f #act #opt_l #i |7,14: #lin *] #H1 whd in ⊢ (??%% → ?);
438#EQ destruct @expr_bound_good_expr /2 by le_maxl/
439qed.
440
441lemma var_to_shift_frame_assign_var_ok : ∀st,v,val,new_st.var_to_shift_ok (\fst st) → frame_assign_var st v val = return new_st →
442var_to_shift_ok (\fst new_st).
443** [|#x #xs] #fp #v #val #new_st * [| #H1 #H2] whd in ⊢ (??%% → ?); [ #EQ destruct]
444whd in match assign_frame; normalize nodelta inversion(update  …) normalize nodelta
445[ #_ #EQ destruct] #new_frm #EQnew_frm whd in ⊢ (??%% → ?); #EQ destruct % //
446@(transitive_le … H1) >(len_update … x … EQnew_frm) //
447qed.
448(*
449#st inversion st #l #p #IHst #v #val inversion l [#IHl #new_st inversion new_st #l' #p'
450inversion l' [#IHl' #IHnew_st #H #H18 @H|#ln #lln whd in match(var_to_shift_ok ?); whd in match(var_to_shift_ok ?); whd in match(var_to_shift_ok ?); #H #IHl' destruct
451#H2 #_ destruct
452whd in match (frame_assign_var ???);
453#H2 whd in match(var_to_shift_ok ?); % /3 by _/
454*)
455
456lemma var_instr_bond_frame_assign_var_ok : ∀st,i,ct,v,val,new_st.
457var_instr_bond_ok (\fst st) i ct →
458frame_assign_var st v val = return new_st →
459var_instr_bond_ok (\fst new_st) i ct.
460** [|#x #xs] #fp #i #ct #v #val #new_st whd in ⊢(%→?→?);
461inversion(divide_continuation_on_frames ct [i])
462#IH normalize nodelta whd in ⊢(?→%→%); [#_|3:#ABS cases ABS]
463[>IH whd in match (frame_assign_var ???); inversion(new_st)
464#l #p #Hns #HN]
465cases daemon
466qed.
467
468lemma var_instr_bond_seq_ok : ∀st.
469∀i : frame_Instructions.∀seq,opt_l.∀ct.
470var_instr_bond_ok st (SEQ … seq opt_l i) ct →
471var_instr_bond_ok st i ct.
472* [|#x #xs] #i #seq #ol #ct whd in ⊢(%→?); inversion(divide_continuation_on_frames ct ?)
473normalize nodelta [2: #H1 #H2 #H3 #H4|3:#H] [1,2:#ABS cases ABS]
474cases i whd in match(var_instr_bond_ok ??); inversion(ct)
475[1,3,5,7: whd in match(var_instr_bond_ok ???);]
476[#_ whd in match(divide_continuation_on_frames ??);
477#ABS destruct| #H1 #H2 whd in match (divide_continuation_on_frames ??);
478#ABS destruct| #H1 #H2 #H3 #H4 whd in match (divide_continuation_on_frames ??); #ABS destruct
479|#H8 #H9 #H10 #H11 #H12 #H13 #H14 whd in match (divide_continuation_on_frames ??); #ABS destruct
480|* #fl #fi #H10 cases fl [#fn #ccl|2,3:#op] #H20 [2,3:#H21 whd in match (divide_continuation_on_frames ??);
481#ABS destruct|whd in match (divide_continuation_on_frames ??);
482#H29 cases H10 [2:#al #l] whd in match (divide_continuation_on_frames ??);
483[2:#ABS destruct
484|1: whd in match(var_instr_bond_ok …);
485]
486]
487]
488
489cases daemon
490qed.
491
492
493lemma var_stack_simulate_tau :
494∀prog : Program frame_state_params frame_state_params frame_state_params.
495∀bound : ℕ.
496∀s1.∀s2.∀s1'.
497execute_l … (frame_sem_state_params bound) (env … prog) (cost_act … (None ?))  s1 s1'→
498frame_variable_sem_rel … s1 s2 → lang_classify … s1 ≠ cl_io → lang_classify … s1' ≠ cl_io →
499∃s2'. ∃t: raw_trace … (operational_semantics … (stack_sem_state_params bound) (trans_var_prog prog)) s2 s2'.
500frame_variable_sem_rel s1' s2' ∧ silent_trace … t.
501#prog #bound #s1 #s2 #s1' #H inversion H
502[ #st1 #st1' * #act_lbl #instr #tl #EQcode_st1 #EQcont_st1 #EQ1 #EQ2 destruct #EQstore_11' #Hio1 #Hio2 #no_ret
503  #EQ1 #EQ2 #EQ3 #EQ4 destruct ****** #EQstore_12 >EQcode_st1 whd in ⊢ (???% → ?); #EQcode_s2
504  >EQcont_st1 whd in match (foldr ?????); #EQcont_s2 #EQ_io_st1 #_ #Hstore1 #Hstore2
505  #Hclass_st1 #Hclass_st1'
506  %{(mk_state … (trans_var_instr (code … st1')) (foldr … (λx,tail.〈\fst x,trans_var_instr (\snd x)〉::tail) [ ] (cont … st1'))
507      (store … st1') false)} %{(t_ind … (cost_act … (None ?)) … (t_base …))}
508  [ @hide_prf whd applyS empty try assumption try %
509    [ #ABS whd in match lang_classify in Hclass_st1; normalize nodelta in Hclass_st1; >EQcode_st1 in Hclass_st1;
510      normalize nodelta >EQ_io_st1 >ABS normalize nodelta * #H cases H %
511      | >EQstore_12 %
512      ]
513  | %
514    [ % [ % [/5 by refl, conj/ | <EQstore_11' // ] | <EQstore_11' @(var_instr_bond_for_empty … Hstore2) ]
515    | %1 %2
516        [ % whd in ⊢ (??%? → ?); cases(code … s2)
517          [| #rt | #seq #opt_l #i | #cond #ltrue #i_true #lfalse #i_false #i | #cond #ltrue #i_true #lfalse #i | #f #act #opt_l #i |
518           #lin *] normalize nodelta [|*: #EQ destruct] inversion(io_info … s2) #ABS normalize nodelta #EQ destruct
519            whd in match lang_classify in Hclass_st1; normalize nodelta in Hclass_st1; >EQcode_st1 in Hclass_st1;
520            normalize nodelta >EQ_io_st1 >ABS normalize nodelta * #H cases H %
521        | %1 % whd in ⊢ (??%? → ?); cases(trans_var_instr ?)
522           [| #rt | #seq #opt_l #i | #cond #ltrue #i_true #lfalse #i_false #i | #cond #ltrue #i_true #lfalse #i | #f #act #opt_l #i |
523            #lin *] normalize nodelta #EQ destruct
524        ]
525     ]
526  ]
527| #st1 #st1' * [ * #v #e | #v ] #instr #mem #opt_l #EQcode_st1
528  [ change with (m_bind ?????) in ⊢ (??%? → ?);
529    #H1 cases(bind_inversion ????? H1) #curr_env * (*inversion(store … st1) *
530    [| #hd #tl] #fp #EQstore_st1 whd in ⊢ (??%% → ?); #EQ destruct*) #EQcurr_env  #H
531    cases(bind_inversion ????? H) -H #sem_e * #EQsem_e
532  | change with (frame_assign_var ???) in ⊢ (??%? → ?);
533  ]
534  #EQmem #EQ destruct #EQcont #EQ destruct #EQio_st1 #EQio_st1' #EQ1 #EQ2 #EQ3 #EQ4 destruct ******
535  #EQstore_12 >EQcode_st1
536  [change with (list_combinators_to_instructions ??) in ⊢ (???% → ?); | whd in ⊢ (???% → ?); ]
537  #EQcode_s2 #EQcont_s2 #Hio1 #Hio2 #Hstore1 #Hstore2 #Hclass_st1 #Hclass_st1'
538  %{(mk_state … (trans_var_instr (code … st1')) (cont … s2) (store … st1') false)}
539  [ cases(eval_exp_ok … EQcurr_env … EQsem_e)
540    [2,3: cases(bind_inversion ????? EQcurr_env) #c_env inversion(store … st1) *
541        [2,4: #hd #tl] #fp #EQstore_st1 * whd in ⊢ (??%% → ??%% → ?); #EQ1 #EQ2 destruct
542        [ >EQstore_st1 in Hstore1; * // |  >EQstore_st1 in Hstore2; #H @(good_expr_for_var_instr_ok … H) % ] ]
543    #new_st * >EQstore_12 #EQnew_st #EQpop
544    %{((create_silent_trace_from_eval_combinators (trans_var_prog prog) bound s2
545          (mk_state … ? (cont … s2) new_st false)
546          (trans_expr e) EQnew_st …) @ (t_ind … (cost_act … (None ?)) … (t_base …)))}
547    try assumption try %
548    [ whd applyS seq_sil try % whd in ⊢ (??%?); >EQpop normalize nodelta <EQstore_12 @EQmem
549    |2,3: <Hio1 @Hio2 % #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
550    | % [ % [ % // % // % // % //] @(var_to_shift_frame_assign_var_ok … EQmem) assumption ]
551      @(var_instr_bond_frame_assign_var_ok … EQmem) <EQcont
552      @(var_instr_bond_seq_ok … Hstore2)
553    ]
554    @append_silent [ % @create_silent_trace_from_eval_combinators_ok [7: % |*:] ]
555      % %2 [ % #EQ normalize in EQ; destruct ] % % whd in ⊢ (??%? → ?); cases(trans_var_instr ?)
556    [| #rt | #seq #opt_l #i | #cond #ltrue #i_true #lfalse #i_false #i | #cond #ltrue #i_true #lfalse #i | #f #act #opt_l #i |
557            #lin *] normalize nodelta #EQ destruct
558  | %{(t_ind … (cost_act … (None ?)) … (t_base …))}
559    [ whd applyS seq_sil try assumption try % [ <Hio1 @Hio2 % #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct]
560      change with (frame_assign_var ???) in ⊢ (??%?); <EQstore_12 assumption
561    | % [ % [2: <EQcont @(var_instr_bond_seq_ok … (var_instr_bond_frame_assign_var_ok … Hstore2 … EQmem)) ]
562          % [2: @(var_to_shift_frame_assign_var_ok … EQmem) assumption]
563          % // % // % // % // ]
564      % %2 [ % whd in ⊢ (??%?→ ?); >EQcode_s2 normalize nodelta #EQ destruct] %
565      % whd in ⊢ (??%? → ?); cases(trans_var_instr ?)
566    [| #rt | #seq #opt_l #i | #cond #ltrue #i_true #lfalse #i_false #i | #cond #ltrue #i_true #lfalse #i | #f #act #opt_l #i |
567            #lin *] normalize nodelta #EQ destruct
568   ]
569 ]
570| #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 destruct
571| #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47 destruct
572| #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 #H60 #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 destruct
573| #H72 #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83 #H84 #H85 #H86 #H87 #H88 #H89 #H90 #H91 #H92 #H93 destruct
574| #H95 #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107 #H108 #H109 #H110 #H111 #H112 #H113 #H114 destruct
575| #H116 #H117 #H118 #H119 #H120 #H121 #H122 #H123 #H124 #H125 #H126 #H127 #H128 #H129 #H130 #H131 #H132 #H133 #H134 #H135 #H136 #H137 #H138 destruct
576| #H140 #H141 #H142 #H143 #H144 #H145 #H146 #H147 #H148 #H149 #H150 #H151 #H152 #H153 #H154 #H155 #H156 #H157 #H158 #H159 #H160 #H161 destruct
577]
578qed.
579
580include alias "arithmetics/nat.ma".
581
582lemma var_stack_simulate_label :
583∀prog : Program frame_state_params frame_state_params frame_state_params.
584∀bound : ℕ.
585∀s1.∀s2.∀l.∀s1'.
586execute_l … (frame_sem_state_params bound) (env … prog) (cost_act … (Some ? l)) s1 s1' →
587lang_classify … s1 ≠ cl_io → lang_classify … s1' ≠ cl_io →
588frame_variable_sem_rel s1 s2 →
589∃s2',s2'',s2'''.
590∃t1: raw_trace … (operational_semantics … (stack_sem_state_params bound) (trans_var_prog prog)) s2 s2'.
591execute_l … (stack_sem_state_params bound) (env … (trans_var_prog prog)) (cost_act … (Some ? l)) s2' s2'' ∧
592∃t3: raw_trace … (operational_semantics … (stack_sem_state_params bound) (trans_var_prog prog)) s2'' s2'''.
593frame_variable_sem_rel  s1' s2''' ∧ silent_trace … t1 ∧ pre_silent_trace … t3.
594#prog #bound #s1 #s2 #lbl #s1' #H inversion H
595[ #st1 #st1' * #lab #instr #tail #EQcode_st1 #EQcont_st1 #EQ1 #EQ2 destruct #EQstore #Hio1 #Hio2 #no_ret
596  #EQ1 #EQ2 #EQ3 #EQ4 destruct #Hclass1 #Hclass2 ****** #EQstore_12 >EQcode_st1 whd in ⊢ (???% → ?);
597  #EQcode_s2 >EQcont_st1 whd in ⊢ (???% → ?); #EQcont_s2 #Hio3 #_ #Hstore1 #Hstore2 %{s2}
598  %{(mk_state … (trans_var_instr (code … st1')) (foldr … (λx,tail.〈\fst x,trans_var_instr (\snd x)〉::tail) [ ] (cont … st1'))
599      (store … st1') false)}
600  %{(mk_state … (trans_var_instr (code … st1')) (foldr … (λx,tail.〈\fst x,trans_var_instr (\snd x)〉::tail) [ ] (cont … st1'))
601      (store … st1') false)} %{(t_base …)} 
602 %
603 [ whd applyS empty try assumption try % [ #_ whd %{lbl} % | <EQstore_12 % ] ]
604 %{(t_base …)} %
605 [ % [ % [ % [ /5 by refl, conj/ | <EQstore // ] | <EQstore @(var_instr_bond_for_empty … Hstore2) ] ]
606 %2 % * ] % % whd in ⊢ (??%? → ?); cases(trans_var_instr ?)
607 [| #rt | #seq #opt_l #i | #cond #ltrue #i_true #lfalse #i_false #i | #cond #ltrue #i_true #lfalse #i | #f #act #opt_l #i |
608           #lin *] normalize nodelta #EQ destruct
609| #st1 #st1' * [ * #v #e | #v ] #instr #mem #opt_l #EQcode_st1
610  [ change with (m_bind ?????) in ⊢ (??%? → ?);
611    #H1 cases(bind_inversion ????? H1) #curr_env * (*inversion(store … st1) *
612    [| #hd #tl] #fp #EQstore_st1 whd in ⊢ (??%% → ?); #EQ destruct*) #EQcurr_env  #H
613    cases(bind_inversion ????? H) -H #sem_e * #EQsem_e
614  | change with (frame_assign_var ???) in ⊢ (??%? → ?);
615  ]
616  #EQmem #EQ destruct #EQcont #EQ destruct #EQio_st1 #EQio_st1' #EQ1 #EQ2 #EQ3 #EQ4 destruct #Hclass1 #Hclass2 ******
617  #EQstore_12 >EQcode_st1
618  [change with (list_combinators_to_instructions ??) in ⊢ (???% → ?); | whd in ⊢ (???% → ?); ]
619  #EQcode_s2 #EQcont_s2 #Hio1 #Hio2 #Hstore1 #Hstore2
620  [ cases(eval_exp_ok … EQcurr_env … EQsem_e)
621    [2,3: cases(bind_inversion ????? EQcurr_env) #c_env inversion(store … st1) *
622        [2,4: #hd #tl] #fp #EQstore_st1 * whd in ⊢ (??%% → ??%% → ?); #EQ1 #EQ2 destruct
623        [ >EQstore_st1 in Hstore1; * // |  >EQstore_st1 in Hstore2; #H @(good_expr_for_var_instr_ok … H) % ] ]
624    #new_st * >EQstore_12 #EQnew_st #EQpop
625    %{(mk_state … ? (cont … s2) new_st false)}
626    [2: %{(mk_state … (trans_var_instr (code … st1')) (cont … s2) (store … st1') false)}
627        %{(mk_state … (trans_var_instr (code … st1')) (cont … s2) (store … st1') false)}
628        %{(create_silent_trace_from_eval_combinators (trans_var_prog prog) bound s2
629          (mk_state … ? (cont … s2) new_st false)
630          (trans_expr e) EQnew_st …)} try assumption try %
631         [1,2: <Hio1 @Hio2 % #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
632         | whd @seq_sil [4,6,7,8,9,10: % |1,2,3:] whd in ⊢ (??%?); >EQpop normalize nodelta <EQstore_12 @EQmem
633         ]
634         %{(t_base …)} %
635         [ % [ % [ % [ % // % // % // % //] @(var_to_shift_frame_assign_var_ok … EQmem) assumption ]
636               @(var_instr_bond_frame_assign_var_ok … EQmem) <EQcont
637               @(var_instr_bond_seq_ok … Hstore2)
638             ] % @create_silent_trace_from_eval_combinators_ok [7: % |*:] ]
639         % % whd in ⊢ (??%? → ?); cases(trans_var_instr ?)
640    [| #rt | #seq #opt_l #i | #cond #ltrue #i_true #lfalse #i_false #i | #cond #ltrue #i_true #lfalse #i | #f #act #opt_l #i |
641            #lin *] normalize nodelta #EQ destruct
642   |]
643 | %{s2} %{(mk_state … (trans_var_instr (code … st1')) (cont … s2) (store … st1') false)}
644   %{(mk_state … (trans_var_instr (code … st1')) (cont … s2) (store … st1') false)} %{(t_base …)}
645   %
646   [ whd @seq_sil try assumption [3,4,5,7: % |6: <Hio1 @Hio2 % #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
647      |2: change with (frame_assign_var ???) in ⊢ (??%?); <EQstore_12 assumption |] ]
648   %{(t_base …)} % [ %
649    [ % [2: <EQcont @(var_instr_bond_seq_ok … (var_instr_bond_frame_assign_var_ok … Hstore2 … EQmem)) ]
650          % [2: @(var_to_shift_frame_assign_var_ok … EQmem) assumption]
651          % // % // % // % // ]
652    %2 % *]
653    % % whd in ⊢ (??%? → ?); cases(trans_var_instr ?)
654    [| #rt | #seq #opt_l #i | #cond #ltrue #i_true #lfalse #i_false #i | #cond #ltrue #i_true #lfalse #i | #f #act #opt_l #i |
655            #lin *] normalize nodelta #EQ destruct
656   ]
657|3,4: #st1 #st1' #exp #ltrue #i_true #lfalse #i_false #instr #new_m #EQcode_st1
658      [ change with (m_bind ?????) in ⊢ (??%? → ?); | change with (m_bind ?????) in ⊢ (??%? → ?);]
659      #EQeval cases(bind_inversion ????? EQeval) #curr_env * #EQcurr_env #H
660      cases(bind_inversion ????? H) -H #b * #EQb whd in ⊢ (??%% → ?); #EQ destruct #EQcont_st1'
661      #EQ1 #EQstore destruct #Hio1 #Hio2 #EQ1 #EQ2 #EQ3 #EQ4 destruct #Hclass1 #Hclass2 ****** #EQstore_12
662      >EQcode_st1
663      [change with (list_combinators_to_instructions ??) in ⊢ (???% → ?); |
664       change with (list_combinators_to_instructions ??) in ⊢ (???% → ?);
665      ]
666      #EQcode_s2 #EQcont_s2 #EQ_io #Hio3 #Hstore1 #Hstore2
667      cases(eval_cond_ok … EQcurr_env EQb)
668      [2,5: cases (store … st1) in EQcurr_env Hstore1; *
669            [1,3: #fp whd in ⊢ (??%% → ?); #EQ destruct]
670            #hd #tl #fp whd in ⊢ (??%% → ?); #EQ destruct * //
671      |3,6: @cond_bound_good_cond cases(store … st1) in EQcurr_env Hstore2; *
672            [2,4: #hd #tl] #fp whd in ⊢ (??%% → ?); #EQ destruct whd in ⊢ (% → ?);
673            inversion(divide_continuation_on_frames ??) [1,3: #_ *] #x #xs #_
674            change with ([?] @ ?) in match ([?] @ ?);
675            >divide_continuation_on_frame_app cases(divide_continuation_on_frames ??)
676            normalize nodelta [2,4: #y #ys] whd in ⊢ (??%% → ?); #EQ destruct
677            ** /2 by le_maxl/
678      ]
679      #new_mem * #EQnew_mem normalize nodelta #EQpop
680      %{(mk_state … (COND … it ltrue ? lfalse ? (trans_var_instr instr))
681                    (cont … s2) new_mem false)}
682      [3,6: %{(mk_state … (trans_var_instr … (code … st1'))
683              (〈cost_act … (None ?),trans_var_instr … instr〉::cont … s2) (store … st1) false)}
684            %{(mk_state … (trans_var_instr … (code … st1'))
685              (〈cost_act … (None ?),trans_var_instr … instr〉::cont … s2) (store … st1) false)}
686      [ %{(create_silent_trace_from_eval_combinators (trans_var_prog prog) bound s2
687          (mk_state … (COND … it ltrue ? lfalse ? (trans_var_instr instr))
688                    (cont … s2) new_mem false)
689          (trans_cond exp) …)} try assumption try %
690          [1,2: <EQ_io @Hio3 % #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
691          | <EQstore_12 assumption
692          | @cond_true [7,9,10,11,12,13: % |8: whd in ⊢ (??%?); >EQpop % |*:]
693          ]
694      | %{(create_silent_trace_from_eval_combinators (trans_var_prog prog) bound s2
695          (mk_state … (COND … it ltrue ? lfalse ? (trans_var_instr instr))
696                    (cont … s2) new_mem false)
697          (trans_cond exp) …)} try assumption try %
698          [1,2: <EQ_io @Hio3 % #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
699          | <EQstore_12 assumption
700          | @cond_false [7,9,10,11,12,13: % |8: whd in ⊢ (??%?); >EQpop % |*:]
701          ]
702      ]
703      %{(t_base …)} %
704      [2,4: % % whd in ⊢ (??%? → ?); cases(trans_var_instr ?)
705         [1,8: |2,9: #rt |3,10: #seq #opt_l #i |4,11: #cond #ltrue #i_true #lfalse #i_false #i
706         |5,12: #cond #ltrue #i_true #lfalse #i |6,13: #f #act #opt_l #i |7,14: #lin *] normalize nodelta #EQ destruct ]
707      % [2,4: %  @(create_silent_trace_from_eval_combinators_ok … (refl …)) ]
708      % [1,3: % [1,3: % // % // % [2,4: >EQcont_st1' @eq_f2 // ] % // ] <EQstore // ]
709              >EQstore >EQcont_st1' change with ([?] @ ?) in match ([?] @ ?); whd
710              cases(store … st1) in Hstore2; * [2,4: #x #xs] #fp whd in ⊢ (% → ?);
711              inversion(divide_continuation_on_frames …)
712              [1,3,5,7: #ABS * lapply(divide_continuation_on_frame_app_nil_is_nil … ABS) #EQ destruct]
713              #y #ys #_ normalize nodelta [3,4: #_ *] change with ([?] @ ?) in match ([?] @ ?);
714              >divide_continuation_on_frame_app inversion(divide_continuation_on_frames …)
715              [2,4: #z #zs #_ ] normalize nodelta #EQdivide whd in ⊢ (??%% → ?); #EQ destruct
716              ** change with (max (get_cond_bound ?) ?) in ⊢ (?%? → ?); #cond_bound
717              [1,2: #Hz |*: *] #Hxs_ys whd in match (divide_continuation_on_frames ??);
718              whd in match (append ???); whd in match (append ???); whd in match (append ???);
719              <(append_nil … [ ? ; ?]) in ⊢ (?????%); >divide_continuation_on_frame_app
720              >EQdivide normalize nodelta % // %
721              [1,3,5,7: @(transitive_le … cond_bound)
722                 [ >commutative_max @(max_1 flat_labels) @(max_1 flat_labels) //
723                 | @(max_2 flat_labels) @(max_2 flat_labels) @(max_1 flat_labels) //
724                 | @(max_2 flat_labels) @(max_1 flat_labels) //
725                 | @(max_2 flat_labels) @(max_2 flat_labels) @(max_1 flat_labels) //
726                 ]
727              |*: @All_append // % // @(transitive_le … cond_bound)
728                  @(max_2 flat_labels) @(max_2 flat_labels) @(max_2 flat_labels) //
729              ]
730        |*:
731        ]
732|5,6: #st1 #st1' #exp #ltrue #i_true #lfalse #i_false #new_m #EQcode_st1 change with (m_bind ?????) in ⊢ (??%? → ?);
733      #EQeval cases(bind_inversion ????? EQeval) #curr_env * #EQcurr_env #H cases(bind_inversion ????? H) -H #b * #EQb
734      whd in ⊢ (??%% → ?); #EQ destruct #EQcont_st1' #EQ destruct #EQstore #Hio1 #Hio2 #EQ1 #EQ2 #EQ3 #EQ4 destruct
735      #Hclass_st1 #Hclass_st2 ****** #EQstore_12 >EQcode_st1 whd in ⊢ (???% → ?); #EQcode_s2 #EQcont_s2 #Hio2 #Hio3
736      #Hstore1 #Hstore2 %{s2}
737      [ %{(mk_state … (trans_var_instr … (code … st1'))
738            (〈cost_act … (None ?),LOOP … (trans_cond exp) ltrue (trans_var_instr (code … st1')) lfalse (trans_var_instr i_false)〉::cont … s2)
739            (store … st1') false)}
740        %{(mk_state … (trans_var_instr … (code … st1'))
741            (〈cost_act … (None ?),LOOP … (trans_cond exp) ltrue (trans_var_instr (code … st1')) lfalse (trans_var_instr i_false)〉::cont … s2)
742            (store … st1') false)}   
743     | %{(mk_state … (trans_var_instr … (code … st1')) (cont … s2) (store … st1') false)}
744       %{(mk_state … (trans_var_instr … (code … st1')) (cont … s2) (store … st1') false)}
745     ]
746     %{(t_base …)} %
747     [ @loop_true try assumption try % [2: <Hio2 @Hio3 % #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct]
748     |3: @loop_false [6: @EQcode_s2 |*:] try assumption try % [2: <Hio2 @Hio3 % #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct]
749     |*: %{(t_base …)} % [2,4: % % whd in ⊢ (??%? → ?); cases(trans_var_instr ?)
750         [1,8: |2,9: #rt |3,10: #seq #opt_l #i |4,11: #cond #ltrue #i_true #lfalse #i_false #i
751         |5,12: #cond #ltrue #i_true #lfalse #i |6,13: #f #act #opt_l #i |7,14: #lin *] normalize nodelta #EQ destruct ]
752         % [2,4: %2 % * ]
753         % [1,3: % [1,3: % // % // % [2,4: >EQcont_s2 >EQcont_st1' %] % //] <EQstore //
754           |*: >EQstore >EQcont_st1' whd whd in match (divide_continuation_on_frames ??); whd in match (append ???);
755               whd in match (append ???); [ <(append_nil … [?;?]) | <(append_nil … [?]) ]
756               >divide_continuation_on_frame_app inversion(divide_continuation_on_frames ??) normalize nodelta
757               [2,4: #x #xs #_] #EQdivide cases(store … st1) in Hstore2; * [2,4,6,8: #y #ys] #fp whd in ⊢ (% → ?);
758               <(append_nil … [?])  >divide_continuation_on_frame_app >EQdivide normalize nodelta **
759               change with (max (get_cond_bound ?) ?) in ⊢ (?%? → ?); #cond_bound whd in match (append ???);
760               #H1 #H2 % // % // try (% //) @(transitive_le … cond_bound) @(max_2 flat_labels)
761               [1,3: @(max_1 flat_labels) |*: @(max_2 flat_labels)] //
762          ]
763       ]
764      cases(eval_cond_ok … EQcurr_env EQb)
765      [2,5: cases (store … st1) in EQcurr_env Hstore1; *
766            [1,3: #fp whd in ⊢ (??%% → ?); #EQ destruct]
767            #hd #tl #fp whd in ⊢ (??%% → ?); #EQ destruct * //
768      |3,6: @cond_bound_good_cond cases(store … st1) in EQcurr_env Hstore2; *
769            [2,4: #hd #tl] #fp whd in ⊢ (??%% → ?); #EQ destruct whd in ⊢ (% → ?);
770            inversion(divide_continuation_on_frames ??) [1,3: #_ *] #x #xs #_
771            change with ([?] @ ?) in match ([?] @ ?);
772            >divide_continuation_on_frame_app cases(divide_continuation_on_frames ??)
773            normalize nodelta [2,4: #y #ys] whd in ⊢ (??%% → ?); #EQ destruct
774            ** /2 by le_maxl/
775      ] 
776      #new_m * #EQnew_m #EQpop  whd in ⊢ (??%?); <EQstore_12  >EQnew_m normalize nodelta 
777      >EQpop %
778| #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 destruct cases H4
779| #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 destruct
780| #H46 #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 #H60 #H61 #H62 #H63 #H64 #H65 #H66 #H67 destruct
781]
782qed.
783
784definition var_stack_good_prog : Program frame_state_params frame_state_params frame_state_params → Prop ≝
785λprog.All … (λx.get_instr_bound (f_body … x) ≤ f_pars frame_env_params … (f_sig … x)) (env … prog).
786
787lemma lookup_trans_ok : ∀prog : Program frame_state_params frame_state_params frame_state_params.∀f,env_it.
788lookup … (env … prog) f = return env_it →
789lookup … (env … (trans_var_prog prog)) f = return (mk_env_item …       
790         (mk_signature stack_env_params stack_instr_params (f_name … (f_sig … env_it)) (f_pars … env_it) it)
791         (f_lab … env_it)
792         (trans_var_instr (f_body … env_it))).
793* #en #main #init_lab #f * lapply f -f elim en -en
794[ #f #sig #c_lab #body whd in ⊢ (??%% → ?); #EQ destruct]
795* #sig #c_lab #body #xs #IH #f #sig' #c_lab' #body' whd in ⊢ (??%? → ?); @eq_function_name_elim
796[ #EQ destruct normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct whd in ⊢ (??%?); @eq_function_name_elim // normalize nodelta
797  * #ABS cases ABS %
798| #DIFF normalize nodelta #H whd in ⊢ (??%?); normalize nodelta @eq_function_name_elim
799  [ #EQ destruct cases DIFF * %] #_ normalize nodelta
800  change with (env … (trans_var_prog (mk_Program ??? ? main init_lab))) in ⊢ (??(????%?)?); @IH //
801]
802qed.
803
804lemma lookup_prop_ok : ∀prog : Program frame_state_params frame_state_params frame_state_params.∀P,f,env_it.
805lookup … (env … prog) f = return env_it → All … P (env … prog) →
806P env_it.
807* #en #main #init elim en -en
808[ #P #f #env_it whd in ⊢ (??%% → ?); #EQ destruct ]
809#x #xs #IH #P #f #env_it whd in ⊢ (??%? → ?); @eq_function_name_elim
810[ #EQ destruct normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct] * //
811#DIFF normalize nodelta #H1 * #_ @IH //
812qed.
813
814lemma var_stack_simulate_call_general :
815∀prog : Program frame_state_params frame_state_params frame_state_params.
816∀bound : ℕ.
817var_stack_good_prog prog →
818∀s1.∀s2.∀s1'.∀f,l.
819execute_l … (frame_sem_state_params bound) (env … prog) (call_act … f l) s1 s1' →
820lang_classify … s1 ≠ cl_io → lang_classify … s1' ≠ cl_io →
821frame_variable_sem_rel s1 s2 →
822∃s2',s2'',s2'''.
823∃t1: raw_trace … (operational_semantics … (stack_sem_state_params bound) (trans_var_prog prog)) s2 s2'.
824execute_l … (stack_sem_state_params bound) (env … (trans_var_prog prog)) (call_act … f l) s2' s2'' ∧
825∃t3: raw_trace … (operational_semantics … (stack_sem_state_params bound) (trans_var_prog prog)) s2'' s2'''.
826frame_variable_sem_rel s1' s2''' ∧ silent_trace … t1 ∧ pre_silent_trace … t3 ∧
827is_call_post_label …  (operational_semantics … (frame_sem_state_params bound) prog) s1 =
828  is_call_post_label … (operational_semantics … (stack_sem_state_params bound) (trans_var_prog prog)) s2' ∧
829  frame_variable_call_rel s1 s2'.
830#prog #bound #good_prog #s1 #s2 #s1' #f #lab #H inversion H
831[ #H1 #H2 * #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 destruct cases H11
832| #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 destruct
833|#H41 #H42 #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 #H60 #H61 #H62 #H63 destruct
834| #H65 #H66 #H67 #H68 #H69 #H70 #H71 #H72 #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83 #H84 #H85 #H86 #H87 destruct
835| #H89 #H90 #H91 #H92 #H93 #H94 #H95 #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107 #H108 #H109 #H110 destruct
836| #H112 #H113 #H114 #H115 #H116 #H117 #H118 #H119 #H120 #H121 #H122 #H123 #H124 #H125 #H126 #H127 #H128 #H129 #H130 #H131 #H132 #H133 destruct
837| #H135 #H136 #H137 #H138 #H139 #H140 #H141 #H142 #H143 #H144 #H145 #H146 #H147 #H148 #H149 #H150 #H151 #H152 #H153 #H154 destruct
838|9: #H156 #H157 #H158 #H159 #H160 #H161 #H162 #H163 #H164 #H165 #H166 #H167 #H168 #H169 #H170 #H171 #H172 #H173 #H174 #H175 #H176 #H177 destruct
839]
840#st1 #st1' #f' #act_p #r_lb #i #mem #env_it #EQcode_st1 #EQenv_it change with (m_bind ?????) in ⊢ (??%? → ?);
841#EQmem cases(bind_inversion ????? EQmem) #curr_env * #EQcurr_env #H cases(bind_inversion ????? H) -H #val * #EQval
842#EQassign #EQ destruct #EQcode_st1' #EQcont_st1' #Hio1 #Hio2 #EQ1 #EQ2 #EQ3 #EQ4 destruct #Hclass1 #Hclass2 ******
843#EQstore_12 >EQcode_st1 change with (list_combinators_to_instructions ??) in ⊢ (???% → ?); #EQcode_s2 #EQcont_s2
844#Hio3 #Hio4 #Hstore1 #Hstore2
845cases(eval_exp_ok … EQcurr_env EQval)
846[2: cases (store … st1) in EQcurr_env Hstore1; *
847   [1,3: #fp whd in ⊢ (??%% → ?); #EQ destruct]
848   #hd #tl #fp whd in ⊢ (??%% → ?); #EQ destruct * //
849|3,6: @expr_bound_good_expr cases(store … st1) in EQcurr_env Hstore2; *
850      [2,4: #hd #tl] #fp whd in ⊢ (??%% → ?); #EQ destruct whd in ⊢ (% → ?);
851      inversion(divide_continuation_on_frames ??) [1,3: #_ *] #x #xs #_
852      change with ([?] @ ?) in match ([?] @ ?);
853      >divide_continuation_on_frame_app cases(divide_continuation_on_frames ??)
854      normalize nodelta [2,4: #y #ys] whd in ⊢ (??%% → ?); #EQ destruct
855      ** /2 by le_maxl/
856]
857#new_st * #EQnew_st #EQpop %{(mk_state … (CALL … f' it r_lb (trans_var_instr i)) (cont … s2) new_st false)}
858%{(mk_state … (trans_var_instr (f_body … env_it)) (〈ret_act … r_lb,trans_var_instr i〉 :: (cont … s2))
859     (store … st1') false)}
860%{(mk_state … (trans_var_instr (f_body … env_it)) (〈ret_act … r_lb,trans_var_instr i〉 :: (cont … s2))
861     (store … st1') false)}
862%{(create_silent_trace_from_eval_combinators (trans_var_prog prog) bound s2
863          (mk_state … (CALL … f' it r_lb (trans_var_instr i)) (cont … s2) new_st false)
864          (trans_expr act_p) …)}
865try assumption
866[1,2: <Hio3 @Hio4 % #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
867| %
868| <EQstore_12 assumption
869]
870%
871[ @(call stack_state_params (stack_sem_state_params bound) (env … (trans_var_prog prog))
872     (mk_state … (CALL … f' it r_lb (trans_var_instr i)) (cont … s2) new_st false)
873     (mk_state … (trans_var_instr (f_body … env_it)) (〈ret_act … r_lb,trans_var_instr i〉 :: (cont … s2))
874        (store … st1') false)
875       f' it r_lb (trans_var_instr i) ?
876       (mk_env_item …       
877         (mk_signature stack_env_params stack_instr_params (f_name … (f_sig … env_it)) (f_pars … env_it) it)
878         (f_lab … env_it)
879         (trans_var_instr (f_body … env_it))) (refl …))
880  [3: whd in ⊢ (??%?); >EQpop in ⊢ (??%?); normalize nodelta assumption |] try assumption try %
881  @lookup_trans_ok //
882]
883%{(t_base …)} %
884[ %
885[2: whd in ⊢ (??%%); >EQcode_st1 % ] %
886[2: % % whd in ⊢ (??%? → ?); cases(trans_var_instr ?)
887    [| #rt | #seq #opt_l #i | #cond #ltrue #i_true #lfalse #i_false #i | #cond #ltrue #i_true #lfalse #i | #f #act #opt_l #i |
888            #lin *] normalize nodelta #EQ destruct ] %
889[2: % @(create_silent_trace_from_eval_combinators_ok … (refl …)) ]
890% [ % [ % // % // % [2: >EQcont_s2 >EQcont_st1' % ] % // ] @(var_to_shift_frame_assign_var_ok … EQassign) % // ]
891@(var_instr_bond_frame_assign_var_ok … EQassign) >EQcont_st1' %
892[ % // >list_n_def >EQcode_st1' @(transitive_le … (lookup_prop_ok … EQenv_it good_prog)) /2 by le_plus_to_minus/ ]
893<(append_nil … [i]) >divide_continuation_on_frame_app inversion(divide_continuation_on_frames …) normalize nodelta
894[2: #y #ys #_] #EQdivide cases(store … st1) in Hstore2; *
895[2,4: #z #zs] #fp whd in ⊢ (% → ?); <(append_nil … [?]) >divide_continuation_on_frame_app
896>EQdivide normalize nodelta ** change with (max ??) in ⊢ (?%? → ?); #act_bound #H1 #H2 % //
897% /2 by le_maxl/
898]
899% // %{f'} %{act_p} %{r_lb} %{i} % //
900qed.
901
902lemma var_stack_simulate_return_general :
903∀prog : Program frame_state_params frame_state_params frame_state_params.
904∀bound : ℕ.
905∀s1.∀s2.∀s1'.∀l.
906execute_l … (frame_sem_state_params bound) (env … prog) (ret_act … l) s1 s1' →
907lang_classify … s1 ≠ cl_io → lang_classify … s1' ≠ cl_io →
908frame_variable_sem_rel s1 s2 →
909∃s2',s2'',s2'''.
910∃t1: raw_trace … (operational_semantics … (stack_sem_state_params bound) (trans_var_prog prog)) s2 s2'.
911execute_l … (stack_sem_state_params bound) (env … (trans_var_prog prog)) (ret_act … l) s2' s2'' ∧
912∃t3: raw_trace … (operational_semantics … (stack_sem_state_params bound) (trans_var_prog prog)) s2'' s2'''.
913frame_variable_sem_rel s1' s2''' ∧ pre_silent_trace … t1 ∧ pre_silent_trace … t3
914∧ Rrel … (frame_variable_pass_rel prog (trans_var_prog prog) bound) s1' s2''.
915#prog #bound #s1 #s2 #s1' #l #H inversion H
916[ #H1 #H2 * #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 destruct
917  cases H31
918| #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 destruct
919| #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 #H71 #H72 #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83 destruct
920| #H85 #H86 #H87 #H88 #H89 #H90 #H91 #H92 #H93 #H94 #H95 #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107 destruct
921| #H109 #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 #H119 #H120 #H121 #H122 #H123 #H124 #H125 #H126 #H127 #H128 #H129 #H130 destruct
922| #H132 #H133 #H134 #H135 #H136 #H137 #H138 #H139 #H140 #H141 #H142 #H143 #H144 #H145 #H146 #H147 #H148 #H149 #H150 #H151 #H152 #H153 destruct
923| #H155 #H156 #H157 #H158 #H159 #H160 #H161 #H162 #H163 #H164 #H165 #H166 #H167 #H168 #H169 #H170 #H171 #H172 #H173 #H174 destruct
924| #H176 #H177 #H178 #H179 #H180 #H181 #H182 #H183 #H184 #H185 #H186 #H187 #H188 #H189 #H190 #H191 #H192 #H193 #H194 #H195 #H196 #H197 #H198 destruct
925]
926* #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
927whd in ⊢ (??%? → ?); cases(store_st1) -store_st1 * [ #fp whd in ⊢ (??%% → ?); #EQ destruct] #curr_env #tail * #fp1 #fp2 normalize nodelta
928#EQnew_st cases(bind_inversion ????? EQnew_st) #val * #EQval whd in ⊢ (??%% → ?); #EQ destruct #EQ destruct #EQstore_st1' #EQ1 #EQ2 #EQ3 #EQ4
929destruct #Hclass1 #Hclass2 ****** #EQstore_12 change with (list_combinators_to_instructions ??) in ⊢ (???% → ?); #EQcode_s2
930whd in ⊢ (???% → ?); #EQcont_s2 #Hio1 #_ * #H1 #Hstore1 ** whd in ⊢ (?%? → ?); #rt_good * #Hstore2
931cases(eval_exp_ok … 〈curr_env::tail,〈fp1,fp2〉〉 … (refl …) EQval) [2,3: /2 by expr_bound_good_expr/]
932#mem * #EQmem #EQpop
933%{(mk_state … (RETURN … it) (cont … s2) mem false)}
934%{(mk_state … (trans_var_instr (code … st1')) (foldr … (λx,tail.〈\fst x,trans_var_instr (\snd x)〉::tail) [ ] (cont … st1')) (store … st1') false)}
935%{(mk_state … (trans_var_instr (code … st1')) (foldr … (λx,tail.〈\fst x,trans_var_instr (\snd x)〉::tail) [ ] (cont … st1')) (store … st1') false)}
936%{(create_silent_trace_from_eval_combinators (trans_var_prog prog) bound s2 …)} try assumption try %
937[1,2: //
938| <EQstore_12 assumption
939| @(ret_instr … it … (refl …) … (refl …) … (refl …)) // try assumption
940  whd in ⊢ (??%?); >EQpop whd in EQpop : (??%%); cases mem in EQpop; * [2: * [2: #w #ws] #zs] #fp normalize nodelta
941  whd in ⊢ (??%% → ?); #EQ destruct >m_return_bind >EQstore_st1' %
942]
943%{(t_base …)} %
944[ % [2: % %  whd in ⊢ (??%? → ?); cases(trans_var_instr ?)
945    [| #rt | #seq #opt_l #i | #cond #ltrue #i_true #lfalse #i_false #i | #cond #ltrue #i_true #lfalse #i | #f #act #opt_l #i |
946            #lin *] normalize nodelta #EQ destruct]
947% [2: @(create_silent_trace_from_eval_combinators_ok … (refl …))]
948% [ % [ % // % // % // % //] ] >EQstore_st1' assumption
949]
950#s3 #s3' * #EQcont_s31' inversion(code …)
951  [| #rt | #seq #opt_l #i #_ | #cond #ltrue #i_true #lfalse #i_false #i #_ #_ #_ | #cond #ltrue #i_true #lfalse #i #_ #_ | #f #act #opt_l #i #_ |
952            #lin *] #EQcode_s3 normalize nodelta [6: |*: *] #EQ destruct * #EQcont_s3' * #f' * #act' * #opt_l' * #i' *
953  #H >H in EQcode_s3; #EQ destruct #EQcode_s3' % [ >EQcont_s3' <EQcont_s31' % | >EQcode_s3' %]
954qed.
955
956
957
958definition simulation_imp_frame :
959∀prog : Program frame_state_params frame_state_params frame_state_params.
960∀bound: ℕ.
961var_stack_good_prog prog → get_instr_bound (main … prog) ≤ bound - to_shift →
962simulation_conditions … (frame_variable_pass_rel prog (trans_var_prog prog) bound) ≝
963λprog,bound,good_prog,good_main.
964mk_simulation_conditions ….
965[ @var_initial_stack_initial // | #H1 #H2 #H3 #H4 @var_final_stack_final //
966| @var_io_is_stack_io | @var_stack_simulate_tau
967| @var_stack_simulate_label
968| #s1 #s2 #s1' #f #lbl #post #exe #class1 #class2 #rel
969  cases(var_stack_simulate_call_general … exe class1 class2 rel) //
970  #s2' * #s2'' * #s2''' * #t1 * #exe' *#t3 **** #rel' #sil1 #sil2 #Hpost #_
971  %{s2'} %{s2''} %{s2'''} %{t1} % [ %{exe'} <Hpost assumption] %{t3}
972  % [ %{rel'} ]  assumption
973| #s1 #s2 #s1' #lbl #exe #class1 #class2 #rel
974  cases(var_stack_simulate_return_general … exe class1 class2 rel)
975  #s2' * #s2'' * #s2''' * #t1 * #exe' * #t3 *** #rel' #sil1 #sil2 #_
976  %{s2'} %{s2''} %{s2'''} %{t1} %{exe'} %{t3} % [% ] try assumption  % assumption
977| #s1 #s2 #s1' #f #lbl #exe #post #class1 #class2 #rel
978  cases(var_stack_simulate_call_general … exe class1 class2 rel) //
979  #s2' * #s2'' * #s2''' * #t1 * #exe' *#t3 **** #rel' #sil1 #sil2 #Hpost #Hcall
980  %{s2'} %{s2''} %{s2'''} %{t1} % [ % // <Hpost assumption ] %{t3}
981  % // % [%] assumption
982| #s1 #s2 #s1' #exe #class1 #class2 #rel
983  cases(var_stack_simulate_return_general … exe class1 class2 rel)
984  #s2' * #s2'' * #s2''' * #t1 * #exe' * #t3 *** #rel' #sil1 #sil2 #HR
985  %{s2'} %{s2''} %{s2'''} %{t1} %{exe'} %{t3} % [ % [%] ] assumption
986|*: cases daemon (*todo per giulio*)
987]
988qed.
Note: See TracBrowser for help on using the repository browser.