source: LTS/variable_stack_pass.ma @ 3578

Last change on this file since 3578 was 3578, checked in by piccolo, 4 years ago

baco

File size: 13.1 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 "stack.ma".
16
17let rec trans_expr (e : expr) on e : list guard_combinators ≝
18match e with
19[ Var v ⇒ [push_var v]
20| Const n ⇒ [push_const n]
21| Plus e1 e2 ⇒ trans_expr e1 @ trans_expr e2 @ [push_plus]
22| Minus e1 e2 ⇒ trans_expr e1 @ trans_expr e2 @ [push_minus]
23].
24
25let rec trans_cond  (c : condition) on c : list guard_combinators ≝
26match c with
27[ Eq e1 e2 ⇒ trans_expr e1 @ trans_expr e2 @ [push_eq]
28| Not c ⇒ trans_cond c @ [push_not]
29].
30
31definition list_combinators_to_instructions : list guard_combinators → stack_Instructions → stack_Instructions ≝
32λl,i.foldr … (λc,instr.SEQ stack_state_params flat_labels (push c) (None ?) instr) i l.
33
34let rec trans_var_instr (i : frame_Instructions) on i : stack_Instructions ≝
35match i with
36[ EMPTY ⇒ EMPTY …
37| RETURN exp ⇒ list_combinators_to_instructions (trans_expr exp) (RETURN … it)
38| SEQ seq opt_l instr ⇒
39  let t_instr ≝ trans_var_instr … instr in
40  match seq with
41  [ Seq_i seq' ⇒
42     match seq' with
43     [ sAss v e ⇒ list_combinators_to_instructions (trans_expr e) (SEQ … (pop_Ass v) opt_l t_instr)
44     ]
45  | PopReg v ⇒ SEQ stack_instr_params ? (popreg v) opt_l t_instr
46  ]
47| COND cond ltrue i_true lfalse i_false instr ⇒
48  let t_i_true ≝ trans_var_instr … i_true in
49  let t_i_false ≝ trans_var_instr … i_false in
50  let t_instr ≝ trans_var_instr … instr in
51  list_combinators_to_instructions (trans_cond cond) (COND … it ltrue t_i_true lfalse t_i_false t_instr)
52| LOOP cond ltrue i_true lfalse instr ⇒
53  let t_i_true ≝ trans_var_instr … i_true in
54  let t_instr ≝ trans_var_instr … instr in
55   LOOP stack_state_params flat_labels (trans_cond … cond) ltrue t_i_true lfalse t_instr
56| CALL f act_p opt_l instr ⇒
57  let t_instr ≝ trans_var_instr … instr in
58  list_combinators_to_instructions (trans_expr act_p) (CALL … f it opt_l t_instr)
59| IO lin io lout instr ⇒ ?
60].
61cases io
62qed.
63
64definition trans_var_prog :
65 Program frame_env_params frame_instr_params flat_labels →
66 Program stack_env_params stack_instr_params flat_labels ≝
67λprog.
68let t_main ≝ trans_var_instr … (main … prog) in
69 (mk_Program …
70  (foldr …
71   (λx,tail.(let t_body ≝ trans_var_instr … (f_body … x) in
72     mk_env_item …       
73     (mk_signature stack_env_params stack_instr_params (f_name … (f_sig … x)) (f_pars … x) it) (f_lab … x) t_body) :: tail)
74   (nil ?) (env … prog))
75  t_main (initial_act … prog)).
76
77include "Simulation.ma".
78
79definition frame_variable_pass_rel :
80∀prog : Program frame_state_params frame_state_params frame_state_params.
81∀t_prog : Program stack_env_params stack_instr_params flat_labels.
82∀bound : ℕ.
83relations flat_labels (operational_semantics frame_state_params frame_sem_state_params prog)
84(operational_semantics stack_state_params (stack_sem_state_params bound) t_prog) ≝
85λprog,t_prog,bound.
86(mk_relations flat_labels (operational_semantics frame_state_params frame_sem_state_params prog)
87 (operational_semantics stack_state_params (stack_sem_state_params bound) t_prog)
88 (λs1,s2.store … s1 = store … s2 ∧ code … s2 = trans_var_instr (code … s1) ∧
89         cont … s2 = foldr … (λx,tail. 〈(\fst x),trans_var_instr (\snd x)〉 :: tail) (nil ?) (cont … s1))
90 (λ_.λ_.True)).
91
92let rec expr_fv (e : expr) on e : list variable ≝
93match e with
94[ Var v ⇒ [v]
95| Const n ⇒ []
96| Plus e1 e2 ⇒ expr_fv e1 @ expr_fv e2
97| Minus e1 e2 ⇒ expr_fv e1 @ expr_fv e2
98].
99
100definition good_expr ≝  λbound : ℕ.λe : expr.All … (λv.v < bound) (expr_fv e).
101
102let rec cond_fv (c : condition) on c : list variable ≝
103match c with
104[ Eq e1 e2 ⇒ expr_fv e1 @ expr_fv e2
105| Not c1 ⇒ cond_fv c1
106].
107
108definition good_cond ≝ λbound : ℕ.λc : condition.All … (λv.v < bound) (cond_fv c).
109
110lemma good_expr_monotone : ∀n1,n2.∀e.n1 ≤ n2 → good_expr n1 e →
111good_expr n2 e.
112#n1 #n2 #e lapply n1 -n1 lapply n2 -n2 elim e //
113[ #v #n1 #n2 #H * #H1 * % /2/
114|*: #e1 #e2 #IH1 #IH2 #n1 #n2 #H #H1 cases(All_inv_append … H1) #H3 #H4 @All_append /2/
115]
116qed.
117
118lemma frame_sem_exp_cons : ∀env.∀e.∀n1,n2.
119to_shift ≤ |env| →
120good_expr (|env| - to_shift) e →
121frame_sem_expr env e = return n1 →
122frame_sem_expr (n2 :: env) e = return n1.
123#env #e lapply env -env elim e
124[ #v #env #n1 #n2 #prf1 * #Hv *
125 whd in ⊢ (??%% → ?); #H change with (nth_opt ???) in ⊢ (??%?);
126 change with ([?]@?) in match ([?]@?); >nth_second
127 [ >length_append whd in ⊢ (???%); <H @eq_f2 // normalize <minus_n_O <minus_n_O
128   >(eq_minus_S_pred ? O) <minus_n_O >(eq_minus_S_pred ? O) <minus_n_O
129   >(eq_minus_S_pred ? O) <minus_n_O @eq_f <(eq_minus_S_pred ? (S v)) %
130 | normalize <minus_n_O >minus_minus_comm @le_plus_to_minus_r
131   @(transitive_le … (monotonic_le_plus_r 1 ?? Hv)) normalize <(minus_Sn_m 2) //
132 ]
133| #n #env #n1 #n2 #prf1 * normalize //
134|*: #e1 #e2 #IH1 #IH2 #env #n1 #n2 #prf1 #H cases(All_inv_append … H) -H #H1 #H2
135  change with (m_bind ?????) in ⊢ (??%? → ?); #H cases(bind_inversion ????? H) -H
136  #n3 * #EQn3 #H cases(bind_inversion ????? H) -H #n4 * #EQn4 whd in ⊢ (??%% → ?);
137  #EQ destruct change with (m_bind ?????) in ⊢ (??%?); >(IH1 … EQn3) //
138  >(IH2 … EQn4) //
139]
140qed.
141
142
143lemma eval_exp_ok : ∀st.∀env:activation_frame.∀e: expr.∀n.
144to_shift ≤ |env| → good_expr (|env| - to_shift) e →
145frame_current_env … st = return env →
146frame_sem_expr env e = return n →
147∃st'.m_fold Option … eval_combinators (trans_expr e) st = return st' ∧
148pop st' = return 〈n,st〉.
149** [| #curr_env #rem] #sp_fp #env #e #n #H1 #H2 normalize in ⊢ (% → ?); #EQ destruct
150lapply n -n lapply H1 -H1 lapply H2 -H2 lapply env -env elim e
151[ #v #env #_ #_ #n whd in ⊢ (??%% → ?); #H %{(〈(n::env)::rem,sp_fp〉)} % try %
152  whd in ⊢ (??%?); whd in match eval_combinators; normalize nodelta
153  whd in match frame_current_env; normalize nodelta whd in match option_hd; normalize nodelta
154  >m_return_bind whd in match read_frame; normalize nodelta >H %
155| #n #env #_ #_ #m whd in ⊢ (??%% → ?); #EQ destruct %{(〈(m::env)::rem,sp_fp〉)} %%
156|*: #e1 #e2 #IH1 #IH2 #env #H1 #H2 #n change with (m_bind ?????) in ⊢ (??%? → ?);
157  #H cases(bind_inversion ????? H) -H #n1 * #EQn1
158  #H cases(bind_inversion ????? H) -H #n2 * #EQn2
159  whd in ⊢ (??%% → ?); #EQ destruct
160  [ %{(〈((n1 + n2)::env)::rem,sp_fp〉)} | %{(〈((n1 - n2)::env)::rem,sp_fp〉)} ]
161  >m_fold_append cases(IH1 … EQn1) // [2,4: cases(All_inv_append … H1) //] #st1 * #EQst1 #EQpop1 >EQst1
162  >m_return_bind >m_fold_append cases(IH2 … (n1 :: env))
163  [2,7: cases(All_inv_append … H1) #H1 #H2 @(good_expr_monotone … H2) normalize /2/
164  |3,8: normalize /2/
165  |5,10: @(frame_sem_exp_cons … EQn2) // cases(All_inv_append … H1) //
166  |4,9:
167  ]
168  #st2 * #EQst2 #EQpop2 cases st1 in EQst1 EQpop1; * [2,4: #env' #rem'] #fp_sp' #EQst1
169  [3,4: whd in ⊢ (??%% → ?); #EQ destruct ] cases env' in EQst1; [2,4: #val1 #env''] #EQst1
170  whd in ⊢ (??%% → ?); #EQ destruct >EQst2 >m_return_bind % [2,4: %] whd in ⊢ (??%?);
171  whd in match eval_combinators; normalize nodelta >EQpop2 %
172]
173qed.
174
175lemma eval_cond_ok :  ∀st.∀env:activation_frame.∀c: condition.∀b.
176to_shift ≤ |env| → good_cond (|env| - to_shift) c →
177frame_current_env … st = return env →
178frame_sem_condition env c = return b →
179∃st'.m_fold Option … eval_combinators (trans_cond c) st = return st' ∧
180pop st' = Some ? 〈if b then 1 else O,st〉.
181** [| #curr_env #rem] #sp_fp #env #c #b #H1 #H2 normalize in ⊢ (% → ?); #EQ destruct
182lapply b -b lapply H1 -H1 lapply H2 -H2 lapply env -env elim c
183[ #e1 #e2 #env #H #H1 #b change with (m_bind ?????) in ⊢ (??%? → ?); #H cases(bind_inversion ????? H) -H
184  #n * #EQn #H cases(bind_inversion ????? H) -H #m * #EQm whd in ⊢ (??%% → ?); #EQ destruct
185  %{(〈((if (eqb n m )then 1 else O) :: env)::rem,sp_fp〉)} >m_fold_append
186  cases(eval_exp_ok … EQn) //
187  [2: @(〈env::rem,sp_fp〉) |3: cases(All_inv_append … H) // |4: %]
188  #st1 * #EQst1 #EQpop1 >EQst1 >m_return_bind % // >m_fold_append
189  cases st1 in EQst1 EQpop1; * [| * [| #m' #env'] #rem'] #sp_fp' #EQst1 whd in ⊢ (??%% → ?);
190  #EQ destruct cases(eval_exp_ok … (frame_sem_exp_cons … EQm))
191  [2: @(〈(n::env)::rem,sp_fp〉) |5: % |3: @(transitive_le … H1) //
192  |4: @(good_expr_monotone … (|env| - to_shift)) [ /2/ | cases(All_inv_append … H) //]
193  |6: cases(All_inv_append … H) // |7: // |8:]
194  #st2 * #EQst2 #EQpop2 >EQst2 >m_return_bind change with (m_bind ?????) in ⊢ (??%?);
195  whd in match eval_combinators; normalize nodelta >EQpop2 %
196| #c1 #IH #env #H1 #H2 #b change with (m_bind ?????) in ⊢ (??%? → ?);
197  #H cases(bind_inversion ????? H) -H #b1 * #EQb1 whd in ⊢ (??%% → ?); #EQ destruct
198  %{(〈((if (if b1 then false else true) then 1 else O) :: env)::rem,sp_fp〉)} % //
199  >m_fold_append cases(IH … EQb1) // #st1 * #EQst1 #EQpop1 >EQst1 >m_return_bind
200  change with (m_bind ?????) in ⊢ (??%?); whd in match eval_combinators; normalize nodelta
201  >EQpop1 >m_return_bind whd in ⊢ (??%?); @eq_f @eq_f2 // cases b1 //
202]
203qed.
204
205definition safe_cast : ∀A,B : Type[0].A = B → A → B ≝
206λA,B,prf.match prf with [refl ⇒ λx : A.x].
207
208let rec create_silent_trace_from_eval_combinators (prog : Program stack_env_params stack_instr_params flat_labels)
209(bound : ℕ) (st,st' : state stack_state_params) (l : list guard_combinators) 
210on l :
211 m_fold Option … eval_combinators l (store … st) = return (store … st') →
212  code … st = list_combinators_to_instructions l (code … st') →
213  cont … st = cont … st' → io_info … st = io_info … st' →
214  raw_trace … (operational_semantics stack_state_params (stack_sem_state_params bound) prog) st st' ≝
215match l return λx.(m_fold Option … eval_combinators x ? = ? → ? = list_combinators_to_instructions x ? → ?) with
216[ nil ⇒ λprf1,prf2,prf3,prf4.safe_cast (raw_trace … (operational_semantics stack_state_params (stack_sem_state_params bound) prog) st st)
217     (raw_trace … (operational_semantics stack_state_params (stack_sem_state_params bound) prog) st st') ? (t_base ?? st)
218| cons x xs ⇒ λprf1,prf2,prf3,prf4.
219   let next_store ≝ (opt_safe … (eval_combinators x (store … st)) ?) in
220   let next_st ≝ mk_state stack_state_params (list_combinators_to_instructions xs (code … st')) (cont … st')
221                   next_store (io_info … st') in
222   let tail ≝ create_silent_trace_from_eval_combinators prog bound next_st st' xs ? (refl …) (refl …) (refl …) in
223   t_ind … (cost_act … (None ?)) … tail
224].
225@hide_prf
226[ cases st in prf1 prf2 prf3 prf4; cases st' #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 whd in H9 : (??%%);
227  whd in H10 : (??%%); destruct %
228|4: change with (m_bind ?????) in prf1 :(??%?); cases(bind_inversion ????? prf1) -prf1 #w * #EQw #_ >EQw %
229   whd in ⊢ (??%% → ?); #EQ destruct
230| whd @seq_sil
231  [4: >prf2 in ⊢ (??%?); %
232  |8: %
233  |5: change with (eval_combinators ??) in ⊢ (??%?); normalize nodelta @opt_safe_elim #w #H assumption
234  |6: %
235  |7: assumption
236  |9,10: cases daemon (*io*)
237  |*:
238  ]
239| normalize nodelta @opt_safe_elim #w #EQw change with (m_bind ?????) in prf1 :(??%?); >EQw in prf1;
240  >m_return_bind //
241]
242qed.
243
244lemma create_silent_trace_from_eval_combinators_ok : ∀prog,bound,st,st',l,prf1,prf2,prf3,prf4,t.
245create_silent_trace_from_eval_combinators prog bound st st' l prf1 prf2 prf3 prf4 = t →
246pre_silent_trace … t.
247#prog #bound #st #st' #l lapply st -st lapply st' -st' elim l
248[ * #code' #cont' #store' #io' * #code #cont #store #io whd in ⊢ (??%% → ??%% → ?); #EQ destruct #EQ1 #EQ2 #EQ3 destruct
249  #t whd in ⊢ (??%% → ?); #EQ destruct % cases daemon (*io*)
250| #x #xs #IH #st' #st #H cases(bind_inversion ????? H) #w * #EQw #EQstore_st'
251  whd in ⊢ (???% → ?); change with (list_combinators_to_instructions ??) in match (foldr ?????);
252  #prf2 #EQcont #EQio #t whd in ⊢ (??%? → ?); #EQ destruct %2 [cases daemon (* io *)] @IH [|*: %]
253]
254qed.
255
256(*  [ @opt_safe_elim #w' >EQw whd in ⊢ (??%% → ?); #EQ destruct assumption
257  | %
258  | % c'e' un baco????*)
259
260definition simulation_imp_frame :
261∀prog : Program frame_state_params frame_state_params frame_state_params.
262∀bound: ℕ.
263simulation_conditions … (frame_variable_pass_rel prog (trans_var_prog prog) bound) ≝
264λprog,bound.
265mk_simulation_conditions ….
266cases daemon
267qed.
Note: See TracBrowser for help on using the repository browser.