source: LTS/variable_stack_pass.ma @ 3579

Last change on this file since 3579 was 3579, checked in by piccolo, 4 years ago
File size: 25.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_pass_rel :
110∀prog : Program frame_state_params frame_state_params frame_state_params.
111∀t_prog : Program stack_env_params stack_instr_params flat_labels.
112∀bound : ℕ.
113relations flat_labels (operational_semantics frame_state_params (frame_sem_state_params bound) prog)
114(operational_semantics stack_state_params (stack_sem_state_params bound) t_prog) ≝
115λprog,t_prog,bound.
116(mk_relations flat_labels (operational_semantics frame_state_params (frame_sem_state_params bound) prog)
117 (operational_semantics stack_state_params (stack_sem_state_params bound) t_prog)
118 frame_variable_sem_rel
119 (λ_.λ_.True)).
120
121let rec expr_fv (e : expr) on e : list variable ≝
122match e with
123[ Var v ⇒ [v]
124| Const n ⇒ []
125| Plus e1 e2 ⇒ expr_fv e1 @ expr_fv e2
126| Minus e1 e2 ⇒ expr_fv e1 @ expr_fv e2
127].
128
129definition good_expr ≝  λbound : ℕ.λe : expr.All … (λv.v < bound) (expr_fv e).
130
131let rec cond_fv (c : condition) on c : list variable ≝
132match c with
133[ Eq e1 e2 ⇒ expr_fv e1 @ expr_fv e2
134| Not c1 ⇒ cond_fv c1
135].
136
137definition good_cond ≝ λbound : ℕ.λc : condition.All … (λv.v < bound) (cond_fv c).
138
139lemma good_expr_monotone : ∀n1,n2.∀e.n1 ≤ n2 → good_expr n1 e →
140good_expr n2 e.
141#n1 #n2 #e lapply n1 -n1 lapply n2 -n2 elim e //
142[ #v #n1 #n2 #H * #H1 * % /2/
143|*: #e1 #e2 #IH1 #IH2 #n1 #n2 #H #H1 cases(All_inv_append … H1) #H3 #H4 @All_append /2/
144]
145qed.
146
147lemma frame_sem_exp_cons : ∀env.∀e.∀n1,n2.
148to_shift ≤ |env| →
149good_expr (|env| - to_shift) e →
150frame_sem_expr env e = return n1 →
151frame_sem_expr (n2 :: env) e = return n1.
152#env #e lapply env -env elim e
153[ #v #env #n1 #n2 #prf1 * #Hv *
154 whd in ⊢ (??%% → ?); #H change with (nth_opt ???) in ⊢ (??%?);
155 change with ([?]@?) in match ([?]@?); >nth_second
156 [ >length_append whd in ⊢ (???%); <H @eq_f2 // normalize <minus_n_O <minus_n_O
157   >(eq_minus_S_pred ? O) <minus_n_O >(eq_minus_S_pred ? O) <minus_n_O
158   >(eq_minus_S_pred ? O) <minus_n_O @eq_f <(eq_minus_S_pred ? (S v)) %
159 | normalize <minus_n_O >minus_minus_comm @le_plus_to_minus_r
160   @(transitive_le … (monotonic_le_plus_r 1 ?? Hv)) normalize <(minus_Sn_m 2) //
161 ]
162| #n #env #n1 #n2 #prf1 * normalize //
163|*: #e1 #e2 #IH1 #IH2 #env #n1 #n2 #prf1 #H cases(All_inv_append … H) -H #H1 #H2
164  change with (m_bind ?????) in ⊢ (??%? → ?); #H cases(bind_inversion ????? H) -H
165  #n3 * #EQn3 #H cases(bind_inversion ????? H) -H #n4 * #EQn4 whd in ⊢ (??%% → ?);
166  #EQ destruct change with (m_bind ?????) in ⊢ (??%?); >(IH1 … EQn3) //
167  >(IH2 … EQn4) //
168]
169qed.
170
171
172lemma eval_exp_ok : ∀st.∀env:activation_frame.∀e: expr.∀n.
173to_shift ≤ |env| → good_expr (|env| - to_shift) e →
174frame_current_env … st = return env →
175frame_sem_expr env e = return n →
176∃st'.m_fold Option … eval_combinators (trans_expr e) st = return st' ∧
177pop st' = return 〈n,st〉.
178** [| #curr_env #rem] #sp_fp #env #e #n #H1 #H2 normalize in ⊢ (% → ?); #EQ destruct
179lapply n -n lapply H1 -H1 lapply H2 -H2 lapply env -env elim e
180[ #v #env #_ #_ #n whd in ⊢ (??%% → ?); #H %{(〈(n::env)::rem,sp_fp〉)} % try %
181  whd in ⊢ (??%?); whd in match eval_combinators; normalize nodelta
182  whd in match frame_current_env; normalize nodelta whd in match option_hd; normalize nodelta
183  >m_return_bind whd in match read_frame; normalize nodelta >H %
184| #n #env #_ #_ #m whd in ⊢ (??%% → ?); #EQ destruct %{(〈(m::env)::rem,sp_fp〉)} %%
185|*: #e1 #e2 #IH1 #IH2 #env #H1 #H2 #n change with (m_bind ?????) in ⊢ (??%? → ?);
186  #H cases(bind_inversion ????? H) -H #n1 * #EQn1
187  #H cases(bind_inversion ????? H) -H #n2 * #EQn2
188  whd in ⊢ (??%% → ?); #EQ destruct
189  [ %{(〈((n1 + n2)::env)::rem,sp_fp〉)} | %{(〈((n1 - n2)::env)::rem,sp_fp〉)} ]
190  >m_fold_append cases(IH1 … EQn1) // [2,4: cases(All_inv_append … H1) //] #st1 * #EQst1 #EQpop1 >EQst1
191  >m_return_bind >m_fold_append cases(IH2 … (n1 :: env))
192  [2,7: cases(All_inv_append … H1) #H1 #H2 @(good_expr_monotone … H2) normalize /2/
193  |3,8: normalize /2/
194  |5,10: @(frame_sem_exp_cons … EQn2) // cases(All_inv_append … H1) //
195  |4,9:
196  ]
197  #st2 * #EQst2 #EQpop2 cases st1 in EQst1 EQpop1; * [2,4: #env' #rem'] #fp_sp' #EQst1
198  [3,4: whd in ⊢ (??%% → ?); #EQ destruct ] cases env' in EQst1; [2,4: #val1 #env''] #EQst1
199  whd in ⊢ (??%% → ?); #EQ destruct >EQst2 >m_return_bind % [2,4: %] whd in ⊢ (??%?);
200  whd in match eval_combinators; normalize nodelta >EQpop2 %
201]
202qed.
203
204lemma eval_cond_ok :  ∀st.∀env:activation_frame.∀c: condition.∀b.
205to_shift ≤ |env| → good_cond (|env| - to_shift) c →
206frame_current_env … st = return env →
207frame_sem_condition env c = return b →
208∃st'.m_fold Option … eval_combinators (trans_cond c) st = return st' ∧
209pop st' = Some ? 〈if b then 1 else O,st〉.
210** [| #curr_env #rem] #sp_fp #env #c #b #H1 #H2 normalize in ⊢ (% → ?); #EQ destruct
211lapply b -b lapply H1 -H1 lapply H2 -H2 lapply env -env elim c
212[ #e1 #e2 #env #H #H1 #b change with (m_bind ?????) in ⊢ (??%? → ?); #H cases(bind_inversion ????? H) -H
213  #n * #EQn #H cases(bind_inversion ????? H) -H #m * #EQm whd in ⊢ (??%% → ?); #EQ destruct
214  %{(〈((if (eqb n m )then 1 else O) :: env)::rem,sp_fp〉)} >m_fold_append
215  cases(eval_exp_ok … EQn) //
216  [2: @(〈env::rem,sp_fp〉) |3: cases(All_inv_append … H) // |4: %]
217  #st1 * #EQst1 #EQpop1 >EQst1 >m_return_bind % // >m_fold_append
218  cases st1 in EQst1 EQpop1; * [| * [| #m' #env'] #rem'] #sp_fp' #EQst1 whd in ⊢ (??%% → ?);
219  #EQ destruct cases(eval_exp_ok … (frame_sem_exp_cons … EQm))
220  [2: @(〈(n::env)::rem,sp_fp〉) |5: % |3: @(transitive_le … H1) //
221  |4: @(good_expr_monotone … (|env| - to_shift)) [ /2/ | cases(All_inv_append … H) //]
222  |6: cases(All_inv_append … H) // |7: // |8:]
223  #st2 * #EQst2 #EQpop2 >EQst2 >m_return_bind change with (m_bind ?????) in ⊢ (??%?);
224  whd in match eval_combinators; normalize nodelta >EQpop2 %
225| #c1 #IH #env #H1 #H2 #b change with (m_bind ?????) in ⊢ (??%? → ?);
226  #H cases(bind_inversion ????? H) -H #b1 * #EQb1 whd in ⊢ (??%% → ?); #EQ destruct
227  %{(〈((if (if b1 then false else true) then 1 else O) :: env)::rem,sp_fp〉)} % //
228  >m_fold_append cases(IH … EQb1) // #st1 * #EQst1 #EQpop1 >EQst1 >m_return_bind
229  change with (m_bind ?????) in ⊢ (??%?); whd in match eval_combinators; normalize nodelta
230  >EQpop1 >m_return_bind whd in ⊢ (??%?); @eq_f @eq_f2 // cases b1 //
231]
232qed.
233
234definition safe_cast : ∀A,B : Type[0].A = B → A → B ≝
235λA,B,prf.match prf with [refl ⇒ λx : A.x].
236
237let rec create_silent_trace_from_eval_combinators (prog : Program stack_env_params stack_instr_params flat_labels)
238(bound : ℕ) (st,st' : state stack_state_params) (l : list guard_combinators) 
239on l :
240 m_fold Option … eval_combinators l (store … st) = return (store … st') →
241  code … st = list_combinators_to_instructions l (code … st') →
242  cont … st = cont … st' → io_info … st = false → io_info … st = io_info … st' →
243  raw_trace … (operational_semantics stack_state_params (stack_sem_state_params bound) prog) st st' ≝
244match l return λx.(m_fold Option … eval_combinators x ? = ? → ? = list_combinators_to_instructions x ? → ?) with
245[ nil ⇒ λprf1,prf2,prf3,prf4,prf5.safe_cast (raw_trace … (operational_semantics stack_state_params (stack_sem_state_params bound) prog) st st)
246     (raw_trace … (operational_semantics stack_state_params (stack_sem_state_params bound) prog) st st') ? (t_base ?? st)
247| cons x xs ⇒ λprf1,prf2,prf3,prf4,prf5.
248   let next_store ≝ (opt_safe … (eval_combinators x (store … st)) ?) in
249   let next_st ≝ mk_state stack_state_params (list_combinators_to_instructions xs (code … st')) (cont … st')
250                   next_store (io_info … st') in
251   let tail ≝ create_silent_trace_from_eval_combinators prog bound next_st st' xs ? (refl …) (refl …) ? (refl …) in
252   t_ind … (cost_act … (None ?)) … tail
253].
254@hide_prf
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 %
258   whd in ⊢ (??%% → ?); #EQ destruct
259| whd @seq_sil
260  [4: >prf2 in ⊢ (??%?); %
261  |8: %
262  |5: change with (eval_combinators ??) in ⊢ (??%?); normalize nodelta @opt_safe_elim #w #H assumption
263  |6: %
264  |7: assumption
265  |9,10: // normalize nodelta <prf5 //
266  |*:
267  ]
268| normalize nodelta @opt_safe_elim #w #EQw change with (m_bind ?????) in prf1 :(??%?); >EQw in prf1;
269  >m_return_bind //
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 →
276pre_silent_trace … t.
277#prog #bound #st #st' #l lapply st -st lapply st' -st' elim l
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
283| #x #xs #IH #st' #st #H cases(bind_inversion ????? H) #w * #EQw #EQstore_st'
284  whd in ⊢ (???% → ?); change with (list_combinators_to_instructions ??) in match (foldr ?????);
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.
292(*  [ @opt_safe_elim #w' >EQw whd in ⊢ (??%% → ?); #EQ destruct assumption
293  | %
294  | % 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.
525
526definition simulation_imp_frame :
527∀prog : Program frame_state_params frame_state_params frame_state_params.
528∀bound: ℕ.
529simulation_conditions … (frame_variable_pass_rel prog (trans_var_prog prog) bound) ≝
530λprog,bound.
531mk_simulation_conditions ….
532[ @var_initial_stack_initial | @var_final_stack_final | @var_io_is_stack_io
533| @var_stack_simulate_tau
534qed.
Note: See TracBrowser for help on using the repository browser.