Changeset 3566
- Timestamp:
- Jun 17, 2015, 4:23:08 PM (6 years ago)
- Location:
- LTS
- Files:
-
- 1 added
- 3 edited
Legend:
- Unmodified
- Added
- Removed
-
LTS/stack.ma
r3565 r3566 81 81 @hide_prf ** % // qed. 82 82 83 definition stack_env_params ≝ mk_env_params ℕ. 84 83 85 definition stack_state_params:state_params≝ 84 mk_state_params stack_instr_params frame_env_params flat_labels frame_store_t (*DeqEnv*).86 mk_state_params stack_instr_params stack_env_params flat_labels frame_store_t (*DeqEnv*). 85 87 86 88 definition push : (store_type stack_state_params) → DeqNat → option (store_type stack_state_params) ≝ … … 125 127 126 128 129 let rec list_n (A :Type[0]) (a : A) (n :ℕ) on n : list A ≝ 130 match n with 131 [ O ⇒ nil ? 132 | S m ⇒ a :: list_n … a m 133 ]. 134 127 135 definition stack_eval_call:(signature stack_state_params stack_state_params)→ act_params_type stack_state_params → 128 136 frame_store_t → (option frame_store_t)≝ 129 λsgn,var,st. 130 match sgn with 131 [ mk_signature fun fpt rt ⇒ 132 !〈n,st1〉 ← pop st; 133 frame_assign_var 〈(〈(nil ?),var〉::(\fst st1)),(\snd st1)〉 O n 134 ]. 137 λsgn.λvar,st. 138 !〈n,st1〉 ← pop st; 139 frame_assign_var 〈(〈list_n … O (pred (to_shift + (f_pars … sgn))),var〉::(\fst st1)),(\snd st1)〉 to_shift n. 135 140 136 141 definition stack_return_call:frame_store_t→ (option frame_store_t)≝ … … 142 147 ]. 143 148 149 definition stack_init_store ≝ λn : ℕ.〈[〈list_n … O (to_shift + n),O〉],〈O,O〉〉. 144 150 145 151 146 definition stack_sem_state_params : sem_state_params stack_state_params ≝ mk_sem_state_params stack_state_params stack_eval_seq frame_eval_io 147 (λ_.stack_eval_cond_cond (nil ?)) stack_eval_cond_cond stack_eval_call (λ_.stack_return_call) frame_init_store. 152 definition stack_sem_state_params : ℕ → sem_state_params stack_state_params ≝ 153 λn.mk_sem_state_params stack_state_params stack_eval_seq frame_eval_io 154 (λ_.stack_eval_cond_cond (nil ?)) stack_eval_cond_cond stack_eval_call (λ_.stack_return_call) (stack_init_store n). 148 155 149 156 (* Abitare tipo Instructions *) … … 154 161 155 162 156 definition stack_envitem≝ (env_item frame_env_params stack_instr_params flat_labels).163 definition stack_envitem≝ (env_item stack_env_params stack_instr_params flat_labels). -
LTS/variable.ma
r3562 r3566 52 52 53 53 54 definition frame_store_t≝ DeqProd (DeqSet_List (DeqProd activation_frame variable)) (DeqProd DeqNat DeqNat). (*frame_pointer e stack_pointer*)54 definition frame_store_t≝ DeqProd (DeqSet_List activation_frame) (DeqProd DeqNat DeqNat). (*frame_pointer e return register*) 55 55 56 56 definition frame_env_params ≝ mk_env_params unit. 57 57 58 inductive frame_seq_i : Type[0] ≝ 59 | Seq_i : seq_i → frame_seq_i 60 | PopReg : variable → frame_seq_i. 61 62 definition eq_frame_seq_i : frame_seq_i → frame_seq_i → bool ≝ 63 λx,y. 64 match x with 65 [ Seq_i s ⇒ match y with [Seq_i s' ⇒ seq_i_eq s s' | _ ⇒ false ] 66 | PopReg v ⇒ match y with [PopReg v' ⇒ eqb v v' | _ ⇒ false] 67 ]. 68 69 definition DeqFrameSeqI ≝ mk_DeqSet frame_seq_i eq_frame_seq_i ?. 70 @hide_prf cases daemon qed. 71 72 definition frame_instr_params : instr_params ≝ 73 mk_instr_params ? ? ? ? ? ?. 74 [ @DeqFrameSeqI 75 |@(mk_DeqSet io_i io_i_eq io_i_eq_equality) 76 |@(mk_DeqSet cond_i cond_i_eq cond_i_eq_equality) 77 |@(mk_DeqSet loop_i loop_i_eq loop_i_eq_equality) 78 |@(DeqProd variable DeqExpr) 79 |@DeqExpr].qed. 80 58 81 definition frame_state_params:state_params≝ 59 mk_state_params imp_instr_params frame_env_params flat_labels frame_store_t (*DeqEnv*).82 mk_state_params frame_instr_params frame_env_params flat_labels frame_store_t (*DeqEnv*). 60 83 61 definition frame_current_env:store_type frame_state_params→ option ?≝λs.!hd ← option_hd … (\fst s); return \fsthd.84 definition frame_current_env:store_type frame_state_params→ option ?≝λs.!hd ← option_hd … (\fst s); return hd. 62 85 63 86 definition frame_assign_var ≝ λenv:frame_store_t.λv:variable.λn:DeqNat. 64 87 match \fst env with 65 88 [ nil ⇒ None ? 66 | cons hd tl ⇒ let 〈e,var〉 ≝ hd in return 〈(〈assign_frame e v (\fst (\snd env)) n,var〉:: tl),\snd env〉89 | cons hd tl ⇒ return 〈(assign_frame hd v (\fst (\snd env)) n :: tl),\snd env〉 67 90 ]. 68 91 69 92 definition frame_eval_seq:(seq_instr frame_state_params)→(store_type frame_state_params)→ option (store_type frame_state_params)≝ 70 93 λi,s.match i with 71 [sNop ⇒ Some ? s 72 |sAss v e ⇒ !env ← frame_current_env … s; 73 ! n ← frame_sem_expr env e; 74 frame_assign_var s v n 94 [ Seq_i instr ⇒ 95 match instr with 96 [sNop ⇒ Some ? s 97 |sAss v e ⇒ !env ← frame_current_env … s; 98 ! n ← frame_sem_expr env e; 99 frame_assign_var s v n 100 ] 101 | PopReg v ⇒ frame_assign_var s v (\snd (\snd s)) 75 102 ]. 76 103 … … 88 115 frame_eval_cond_cond. 89 116 90 definition frame_eval_call:(signature frame_state_params imp_state_params)→ act_params_type frame_state_params → frame_store_t → (option frame_store_t)≝117 definition frame_eval_call:(signature frame_state_params frame_state_params)→ act_params_type frame_state_params → frame_store_t → (option frame_store_t)≝ 91 118 λsgn,e,st. 92 119 let 〈var,act_exp〉 ≝ e in 93 120 !env ← frame_current_env … st; 94 121 !n ← frame_sem_expr env act_exp; 95 frame_assign_var 〈( 〈(nil ?),var〉::(\fst st)),(\snd st)〉 On.122 frame_assign_var 〈((nil ?)::(\fst st)),(\snd st)〉 to_shift n. 96 123 97 124 definition frame_return_call:(return_type frame_state_params)→ frame_store_t→ (option frame_store_t)≝ 98 125 λr,s.match (\fst s) with 99 126 [nil⇒ None ? 100 |cons hd tl⇒ let 〈env,v〉≝ hd in 101 !n ← frame_sem_expr env r; 102 frame_assign_var 〈tl,\snd s〉 v n 127 |cons hd tl⇒ !n ← frame_sem_expr hd r; 128 return 〈tl,〈(\fst (\snd s)),n〉〉 103 129 ]. 104 130 105 106 definition frame_init_store: (store_type frame_state_params)≝ 〈[〈(nil ?),O〉],〈O,O〉〉. 131 definition frame_init_store: (store_type frame_state_params)≝ 〈[(nil ?)],〈O,O〉〉. 107 132 108 133 … … 117 142 118 143 119 definition frame_envitem≝ (env_item frame_env_params imp_instr_params flat_labels).144 definition frame_envitem≝ (env_item frame_env_params frame_instr_params flat_labels). -
LTS/variable_stack_pass.ma
r3565 r3566 32 32 λl,i.foldr … (λc,instr.SEQ stack_state_params flat_labels (push c) (None ?) instr) i l. 33 33 34 let rec trans_var_instr (i : frame_Instructions) on i : stack_Instructions ≝ 34 let rec get_expr_bound (e : expr) on e : ℕ ≝ 35 match e with 36 [ Var v ⇒ S v 37 | Const n ⇒ O 38 | Plus e1 e2 ⇒ max (get_expr_bound e1) (get_expr_bound e2) 39 | Minus e1 e2 ⇒ max (get_expr_bound e1) (get_expr_bound e2) 40 ]. 41 42 let rec get_cond_bound (c : condition) on c : ℕ ≝ 43 match c with 44 [Eq e1 e2 ⇒ max (get_expr_bound e1) (get_expr_bound e2) 45 | Not c ⇒ get_cond_bound c 46 ]. 47 48 let rec trans_var_instr (i : frame_Instructions) on i : (stack_Instructions × ℕ) ≝ 35 49 match i with 36 [ EMPTY ⇒ EMPTY …37 | RETURN exp ⇒ list_combinators_to_instructions (trans_expr exp) (RETURN … it)50 [ EMPTY ⇒ 〈EMPTY …,O〉 51 | RETURN exp ⇒ 〈list_combinators_to_instructions (trans_expr exp) (RETURN … it),get_expr_bound exp〉 38 52 | SEQ seq opt_l instr ⇒ 53 let 〈t_instr,c_bound〉 ≝ trans_var_instr … instr in 39 54 match seq with 40 [ sNop ⇒ trans_var_instr … instr 41 | sAss v e ⇒ list_combinators_to_instructions (trans_expr e) (SEQ … (pop_Ass v) opt_l (trans_var_instr … instr)) 55 [ sNop ⇒ 〈t_instr,c_bound〉 56 | sAss v e ⇒ 〈list_combinators_to_instructions (trans_expr e) (SEQ … (pop_Ass v) opt_l t_instr), 57 max (get_expr_bound e) c_bound〉 42 58 ] 43 | COND cond ltrue i_true lfalse i_false instr ⇒ 44 list_combinators_to_instructions (trans_cond cond) 45 (COND … it ltrue (trans_var_instr … i_true) lfalse (trans_var_instr … i_false) (trans_var_instr … instr)) 59 | COND cond ltrue i_true lfalse i_false instr ⇒ 60 let 〈t_i_true,i_true_bound〉 ≝ trans_var_instr … i_true in 61 let 〈t_i_false,i_false_bound〉 ≝ trans_var_instr … i_false in 62 let 〈t_instr,c_bound〉 ≝ trans_var_instr … instr in 63 〈list_combinators_to_instructions (trans_cond cond) (COND … it ltrue t_i_true lfalse t_i_false t_instr), 64 max (get_cond_bound cond) (max i_true_bound (max i_false_bound c_bound))〉 46 65 | LOOP cond ltrue i_true lfalse instr ⇒ 47 LOOP stack_state_params flat_labels (trans_cond … cond) ltrue (trans_var_instr … i_true) lfalse (trans_var_instr … instr) 66 let 〈t_i_true,i_true_bound〉 ≝ trans_var_instr … i_true in 67 let 〈t_instr,c_bound〉 ≝ trans_var_instr … instr in 68 〈LOOP stack_state_params flat_labels (trans_cond … cond) ltrue t_i_true lfalse t_instr, 69 max (get_cond_bound cond) (max i_true_bound c_bound)〉 48 70 | CALL f act_p opt_l instr ⇒ 49 list_combinators_to_instructions (trans_expr (\snd act_p)) (CALL … f (\fst act_p) opt_l (trans_var_instr … instr)) 71 let 〈t_instr,c_bound〉 ≝ trans_var_instr … instr in 72 〈list_combinators_to_instructions (trans_expr (\snd act_p)) (CALL … f (\fst act_p) opt_l t_instr), 73 max (get_expr_bound (\snd act_p)) c_bound〉 50 74 | IO lin io lout instr ⇒ ? 51 75 ]. … … 54 78 55 79 definition trans_var_prog : Program frame_env_params imp_instr_params flat_labels → 56 Program frame_env_params stack_instr_params flat_labels ≝ λprog. 57 mk_Program … 58 (foldr … (λx,tail.(mk_env_item … 59 (mk_signature ? stack_instr_params (f_name … (f_sig … x)) (f_pars … (f_sig … x)) it) (f_lab … x) 60 (trans_var_instr … (f_body … x)) ) :: tail) (nil ?) (env … prog)) 61 (trans_var_instr … (main … prog)). 80 (Program stack_env_params stack_instr_params flat_labels × ℕ) ≝ 81 λprog. 82 let 〈t_main,m_bound〉 ≝ trans_var_instr … (main … prog) in 83 〈(mk_Program … 84 (foldr … 85 (λx,tail.(let 〈t_body,bound〉 ≝ trans_var_instr … (f_body … x) in 86 mk_env_item … 87 (mk_signature stack_env_params stack_instr_params (f_name … (f_sig … x)) bound it) (f_lab … x) t_body) :: tail) 88 (nil ?) (env … prog)) 89 t_main),m_bound〉. 62 90 63 91 include "Simulation.ma". 64 92 65 definition frame_variable_pass_rel ≝ 66 λprog : Program frame_state_params frame_state_params frame_state_params. 67 let t_prog ≝ trans_var_prog prog in 68 mk_relations flat_labels (operational_semantics frame_state_params frame_sem_state_params prog) 69 (operational_semantics stack_state_params stack_sem_state_params t_prog) 70 (λs1,s2.store … s1 = store … s2 ∧ code … s2 = trans_var_instr (code … s1) ∧ 71 cont … s2 = foldr … (λx,tail. 〈(\fst x),trans_var_instr (\snd x)〉 :: tail) (nil ?) (cont … s1)) 72 (λ_.λ_.True). 93 definition frame_variable_pass_rel : 94 ∀prog : Program frame_state_params frame_state_params frame_state_params. 95 ∀t_prog : Program stack_env_params stack_instr_params flat_labels. 96 ∀bound : ℕ. 97 relations flat_labels (operational_semantics frame_state_params frame_sem_state_params prog) 98 (operational_semantics stack_state_params (stack_sem_state_params bound) t_prog) ≝ 99 λprog,t_prog,bound. 100 (mk_relations flat_labels (operational_semantics frame_state_params frame_sem_state_params prog) 101 (operational_semantics stack_state_params (stack_sem_state_params bound) t_prog) 102 (λs1,s2.store … s1 = store … s2 ∧ code … s2 = (\fst (trans_var_instr (code … s1))) ∧ 103 cont … s2 = foldr … (λx,tail. 〈(\fst x),(\fst (trans_var_instr (\snd x)))〉 :: tail) (nil ?) (cont … s1)) 104 (λ_.λ_.True)). 105 73 106 74 107 let rec expr_fv (e : expr) on e : list variable ≝ … … 81 114 82 115 definition good_expr ≝ λbound : ℕ.λe : expr.All … (λv.v < bound) (expr_fv e). 116 117 let rec cond_fv (c : condition) on c : list variable ≝ 118 match c with 119 [ Eq e1 e2 ⇒ expr_fv e1 @ expr_fv e2 120 | Not c1 ⇒ cond_fv c1 121 ]. 122 123 definition good_cond ≝ λbound : ℕ.λc : condition.All … (λv.v < bound) (cond_fv c). 83 124 84 125 lemma good_expr_monotone : ∀n1,n2.∀e.n1 ≤ n2 → good_expr n1 e → … … 155 196 qed. 156 197 157 198 lemma eval_cond_ok : ∀st.∀env:activation_frame.∀c: condition.∀b. 199 to_shift ≤ |env| → good_cond (|env| - to_shift) c → 200 frame_current_env … st = return env → 201 frame_sem_condition env c = return b → 202 ∃st'.m_fold Option … eval_combinators (trans_cond c) st = return st' ∧ 203 pop st' = Some ? 〈if b then 1 else O,st〉. 204 ** [| * #curr_env #var #rem] #sp_fp #env #c #b #H1 #H2 normalize in ⊢ (% → ?); #EQ destruct 205 lapply b -b lapply H1 -H1 lapply H2 -H2 lapply env -env elim c 206 [ #e1 #e2 #env #H #H1 #b change with (m_bind ?????) in ⊢ (??%? → ?); #H cases(bind_inversion ????? H) -H 207 #n * #EQn #H cases(bind_inversion ????? H) -H #m * #EQm whd in ⊢ (??%% → ?); #EQ destruct 208 %{(〈〈(if (eqb n m )then 1 else O) :: env,var〉::rem,sp_fp〉)} >m_fold_append 209 cases(eval_exp_ok … EQn) // 210 [2: @(〈〈env,var〉::rem,sp_fp〉) |3: cases(All_inv_append … H) // |4: %] 211 #st1 * #EQst1 #EQpop1 >EQst1 >m_return_bind % // >m_fold_append 212 cases st1 in EQst1 EQpop1; * [| * * [| #m' #env'] #var #rem'] #sp_fp' #EQst1 whd in ⊢ (??%% → ?); 213 #EQ destruct cases(eval_exp_ok … (frame_sem_exp_cons … EQm)) 214 [2: @(〈〈n::env,var〉::rem,sp_fp〉) |5: % |3: @(transitive_le … H1) // 215 |4: @(good_expr_monotone … (|env| - to_shift)) [ /2/ | cases(All_inv_append … H) //] 216 |6: cases(All_inv_append … H) // |7: // |8:] 217 #st2 * #EQst2 #EQpop2 >EQst2 >m_return_bind change with (m_bind ?????) in ⊢ (??%?); 218 whd in match eval_combinators; normalize nodelta >EQpop2 % 219 | #c1 #IH #env #H1 #H2 #b change with (m_bind ?????) in ⊢ (??%? → ?); 220 #H cases(bind_inversion ????? H) -H #b1 * #EQb1 whd in ⊢ (??%% → ?); #EQ destruct 221 %{(〈〈(if (if b1 then false else true) then 1 else O) :: env,var〉::rem,sp_fp〉)} % // 222 >m_fold_append cases(IH … EQb1) // #st1 * #EQst1 #EQpop1 >EQst1 >m_return_bind 223 change with (m_bind ?????) in ⊢ (??%?); whd in match eval_combinators; normalize nodelta 224 >EQpop1 >m_return_bind whd in ⊢ (??%?); @eq_f @eq_f2 // cases b1 // 225 ] 226 qed. 227 228 (* 229 let rec create_silent_trace_from_eval_combinators (st : (l : list guard_combinators) 230 (prf: m_fold Option … eval_combinators l st = return st') 231 *) 232 233 definition simulation_imp_frame : 234 ∀prog : Program frame_state_params frame_state_params frame_state_params. 235 ∀t_prog,bound.〈t_prog,bound〉 = trans_var_prog prog → 236 simulation_conditions … (frame_variable_pass_rel prog t_prog bound) ≝ 237 λprog,t_prog,bound,good_trans. 238 mk_simulation_conditions …. 239 cases daemon 240 qed. 158 241 159 definition simulation_imp_frame ≝160 λprog : Program frame_state_params frame_state_params frame_state_params.161 mk_simulation_conditions … (frame_variable_pass_rel prog) ???????????.162 cases daemon163 qed.164
Note: See TracChangeset
for help on using the changeset viewer.