Changeset 3579
 Timestamp:
 Jul 10, 2015, 4:08:09 PM (4 years ago)
 Location:
 LTS
 Files:

 6 edited
Legend:
 Unmodified
 Added
 Removed

LTS/Language.ma
r3576 r3579 348 348 eq_instructions … (code … st) (EMPTY …) ∧ 349 349 eqb_list … (cont … st) [〈spec_act,(main … prog)〉 ; 〈spec_act,EMPTY …〉] ∧ 350 store … st == init_store … p' ∧ io_info … st. 350 store … st == init_store … p' ∧ 351 io_info … st. 351 352 352 353 definition lang_final : ∀p.state p → bool ≝ … … 354 355 eq_instructions … (code … st) (EMPTY …) ∧ isnilb … (cont … st). 355 356 357 definition lang_classify : ∀p.state p → ? ≝ 358 (λp,s.match (code … s) with 359 [ COND _ _ _ _ _ _ ⇒ cl_jump 360  LOOP _ _ _ _ _ ⇒ cl_jump 361  EMPTY ⇒ if io_info … s then cl_io else cl_other 362  _ ⇒ cl_other 363 ]). 364 356 365 definition operational_semantics : ∀p : state_params.sem_state_params p → Program p p p → abstract_status p ≝ 357 366 λp,p',prog.mk_abstract_status ? … … 359 368 (execute_l ? p' (env … prog)) 360 369 (is_synt_succ …) 361 (λs.match (code … s) with 362 [ COND _ _ _ _ _ _ ⇒ cl_jump 363  LOOP _ _ _ _ _ ⇒ cl_jump 364  EMPTY ⇒ if io_info … s then cl_io else cl_other 365  _ ⇒ cl_other 366 ]) 370 (lang_classify p) 367 371 (λs.match (code … s) with 368 372 [CALL _ _ m _ ⇒ match m with [ Some _ ⇒ true  None ⇒ false ] … … 393 397  #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8 #EQ9 #EQ10 394 398 ] 395 #_ destruct >EQcode in H; normalize nodelta /2 by ex_intro/ 399 #_ destruct whd in match lang_classify in H ⊢ %; normalize nodelta in H ⊢ %; 400 >EQcode in H; whd in match lang_classify; normalize nodelta /2 by ex_intro/ 396 401 [ cases(io_info ??) normalize nodelta] #EQ destruct 397 402  #s1 #s2 #l #H #H1 inversion H1 #st #st' … … 415 420  #EQ1 #EQ2 #EQ3 #EQiost' #EQ5 #EQ6 #EQ7 #EQ8 #EQ9 #EQ10 416 421 ] 417 #_ destruct 418 cases(code ? st') in H; normalize nodelta >EQiost' normalize nodelta422 #_ destruct whd in match lang_classify in H ⊢ %; normalize nodelta in H ⊢ %; 423 cases(code ? st') in H; whd in match lang_classify; normalize nodelta >EQiost' normalize nodelta 419 424 #eq destruct try (#eq1 destruct) try (#eq2 destruct) try (#eq3 destruct) 420 425 try (#eq4 destruct) try (#eq5 destruct) try (#eq6 destruct) %{lin} % … … 439 444  #EQ1 #EQ2 #EQiost #EQiost' #EQ5 #EQ6 #EQ7 #EQ8 #EQ9 #EQ10 440 445 ] 441 #_ destruct >EQcode in H; normalize nodelta [*: #EQ destruct] 446 #_ destruct whd in match lang_classify in H ⊢ %; normalize nodelta in H ⊢ %; 447 >EQcode in H; normalize nodelta [*: #EQ destruct] 442 448 cases(io_info … st) in x; normalize nodelta [2: #_ #EQ destruct] 443 449 #H3 #_ @H3 % 
LTS/Simulation.ma
r3549 r3579 15 15 (rel : relations …S1 S2) : Prop ≝ 16 16 { initial_is_initial : 17 ∀s1,s2. Srel … rel s1 s2 → (bool_to_Prop (as_initial … s1) → bool_to_Prop (as_initial … s2))18 ; final_is_final : 19 ∀s1,s2. Srel … rel s1 s2 → (bool_to_Prop(as_final … s1) → bool_to_Prop (as_final … s2))17 ∀s1,s2.(bool_to_Prop (as_initial … s1) → bool_to_Prop (as_initial … s2)) → Srel … rel s1 s2 18 ; final_is_final : 19 ∀s1,s2.bool_to_Prop (as_final … s1) → Srel … rel s1 s2 → bool_to_Prop (as_final … s2) 20 20 ; io_is_io : 21 21 ∀s1,s2.Srel … rel s1 s2 → as_classify … s2 = cl_io → as_classify … s1 = cl_io 
LTS/frame_variable_pass.ma
r3577 r3579 14 14 15 15 include "Simulation.ma". 16 include "variable.ma". 17 include alias "arithmetics/nat.ma". 16 include "common_variable_stack.ma". 18 17 19 18 definition update_fun : ∀A : DeqSet.∀B : Type[0].(A → B) → A → B → A → B ≝ 20 19 λA,B,f,a,b,x.if x == a then b else f x. 21 20 22 let rec get_expr_bound (e : expr) on e : ℕ ≝ 23 match e with 24 [ Var v ⇒ S v 25  Const n ⇒ O 26  Plus e1 e2 ⇒ max (get_expr_bound e1) (get_expr_bound e2) 27  Minus e1 e2 ⇒ max (get_expr_bound e1) (get_expr_bound e2) 28 ]. 29 30 let rec get_cond_bound (c : condition) on c : ℕ ≝ 31 match c with 32 [Eq e1 e2 ⇒ max (get_expr_bound e1) (get_expr_bound e2) 33  Not c ⇒ get_cond_bound c 34 ]. 35 36 let rec get_instr_bound (i : frame_Instructions) ≝ 37 match i with 38 [ EMPTY ⇒ O 39  RETURN exp ⇒ get_expr_bound exp 40  SEQ seq opt_l instr ⇒ 41 let c_bound ≝ get_instr_bound instr in 42 match seq with 43 [ Seq_i seq' ⇒ 44 match seq' with [ sAss v e ⇒ max (get_expr_bound e) c_bound ] 45  PopReg v ⇒ max (S v) c_bound 46 ] 47  COND cond ltrue i_true lfalse i_false instr ⇒ 48 let i_true_bound ≝ get_instr_bound i_true in 49 let i_false_bound ≝ get_instr_bound i_false in 50 let c_bound ≝ get_instr_bound instr in 51 max (get_cond_bound cond) (max i_true_bound (max i_false_bound c_bound)) 52  LOOP cond ltrue i_true lfalse instr ⇒ 53 let i_true_bound ≝ get_instr_bound i_true in 54 let c_bound ≝ get_instr_bound instr in 55 max (get_cond_bound cond) (max i_true_bound c_bound) 56  CALL f act_p opt_l instr ⇒ 57 let c_bound ≝ get_instr_bound instr in 58 max (get_expr_bound act_p) c_bound 59  IO lin io lout instr ⇒ ? 60 ]. 61 cases io 62 qed. 21 63 22 64 23 let rec map_exp (e : expr) (map : variable → variable) on e : expr ≝ … … 100 59 cases io qed. 101 60 102 103 let rec All2 (A,B : Type[0]) (f : A → B → Prop) (l1 : list A) (l2 : list B) on l1 : Prop ≝104 match l1 with105 [ nil ⇒ match l2 with [nil ⇒ True  cons _ _ ⇒ False]106  cons x xs ⇒ match l2 with [nil ⇒ False  cons y ys ⇒ f x y ∧ All2 … f xs ys]107 ].108 61 109 62 definition environment_rel : (variable → variable) → environment → activation_frame → Prop ≝ 
LTS/utils.ma
r3575 r3579 159 159 ]. 160 160 161 lemma eqb_list_elim : ∀P : bool → Prop. 162 ∀D,l1,l2.(l1 = l2 → P true) → (l1 ≠ l2 → P false) → P (eqb_list D l1 l2). 163 #P #D #l1 lapply P P elim l1 164 [ #P * /2/ #x #xs #H1 #H2 @H2 % #EQ destruct] 165 #x #xs #IH #P * /2/ #y #ys #H1 #H2 normalize 166 inversion(?==?) #EQ normalize [2: @H2 % #EQ1 destruct >(\b (refl …)) in EQ; #EQ destruct] 167 @IH [ #EQ1 destruct @H1 >(\P EQ) %  * #H @H2 % #EQ1 destruct @H %] 168 qed. 169 161 170 definition DeqSet_List : DeqSet → DeqSet ≝ 162 171 λX.mk_DeqSet (list X) (eqb_list …) ?. … … 381 390 #A #l1 elim l1 [normalize //] #x #xs #IH #l2 * [ normalize #H @⊥ /2/] #n #H normalize @IH /2/ 382 391 qed. 392 393 (* All2 *) 394 395 let rec All2 (A,B : Type[0]) (f : A → B → Prop) (l1 : list A) (l2 : list B) on l1 : Prop ≝ 396 match l1 with 397 [ nil ⇒ match l2 with [nil ⇒ True  cons _ _ ⇒ False] 398  cons x xs ⇒ match l2 with [nil ⇒ False  cons y ys ⇒ f x y ∧ All2 … f xs ys] 399 ]. 
LTS/variable.ma
r3577 r3579 156 156 match \fst env with 157 157 [ nil ⇒ None ? 158  cons hd tl ⇒ ! x ← (assign_frame hd v(\fst (\snd env)) n); return ((〈x::tl,\snd env〉))158  cons hd tl ⇒ ! x ← (assign_frame hd (to_shift + v) (\fst (\snd env)) n); return ((〈x::tl,\snd env〉)) 159 159 ]. 160 160 … … 165 165 [sAss v e ⇒ !env ← frame_current_env … s; 166 166 ! n ← frame_sem_expr env e; 167 frame_assign_var s vn167 frame_assign_var s (to_shift + v) n 168 168 ] 169  PopReg v ⇒ frame_assign_var s v(\snd (\snd s))169  PopReg v ⇒ frame_assign_var s (to_shift + v) (\snd (\snd s)) 170 170 ]. 171 171 … … 204 204 ]. 205 205 206 definition frame_init_store: frame_store_t≝ 〈[(nil ?)],〈O,O〉〉. 207 208 209 definition frame_sem_state_params : sem_state_params frame_state_params ≝ mk_sem_state_params frame_state_params frame_eval_seq frame_eval_io 210 frame_eval_cond_cond frame_eval_loop_cond frame_eval_call frame_return_call frame_init_store. 206 definition frame_init_store: ℕ → frame_store_t≝ λn.〈[list_n … O (to_shift + n)],〈O,O〉〉. 207 208 209 definition frame_sem_state_params : ℕ → sem_state_params frame_state_params ≝ 210 λn.mk_sem_state_params frame_state_params frame_eval_seq frame_eval_io 211 frame_eval_cond_cond frame_eval_loop_cond frame_eval_call frame_return_call (frame_init_store n). 211 212 212 213 (* Abitare tipo Instructions *) 
LTS/variable_stack_pass.ma
r3578 r3579 13 13 (**************************************************************************) 14 14 15 include "common_variable_stack.ma". 15 16 include "stack.ma". 16 17 … … 77 78 include "Simulation.ma". 78 79 80 let rec divide_continuation_on_frames (l : list (ActionLabel flat_labels × frame_Instructions)) 81 (to_append : list frame_Instructions) on l : list (list frame_Instructions) ≝ 82 match 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 91 definition var_to_shift_ok ≝ λst : list activation_frame. 92 All … (λx.to_shift ≤ (x)) st. 93 94 definition var_instr_bond_ok ≝ λst : list activation_frame.λcode : frame_Instructions. 95 λcont : list (ActionLabel flat_labels × frame_Instructions). 96 All2 ?? (λx,y.All … (λz.get_instr_bound z ≤ x  to_shift) y) st 97 (divide_continuation_on_frames cont [code]). 98 99 100 definition frame_variable_sem_rel ≝ 101 λs1 : state frame_state_params. 102 λs2 : state stack_state_params. 103 store … s1 = store … s2 ∧ 104 code … s2 = trans_var_instr (code … s1) ∧ 105 cont … s2 = foldr … (λx,tail. 〈(\fst x),trans_var_instr (\snd x)〉 :: tail) (nil ?) (cont … s1) ∧ 106 io_info … s1 = io_info … s2 ∧ (code … s1 ≠ EMPTY … → io_info … s1 =false) ∧ 107 var_to_shift_ok … (\fst (store … s1)) ∧ var_instr_bond_ok … (\fst (store … s1)) (code … s1) (cont … s1). 108 79 109 definition frame_variable_pass_rel : 80 110 ∀prog : Program frame_state_params frame_state_params frame_state_params. 81 111 ∀t_prog : Program stack_env_params stack_instr_params flat_labels. 82 112 ∀bound : ℕ. 83 relations flat_labels (operational_semantics frame_state_params frame_sem_state_paramsprog)113 relations flat_labels (operational_semantics frame_state_params (frame_sem_state_params bound) prog) 84 114 (operational_semantics stack_state_params (stack_sem_state_params bound) t_prog) ≝ 85 115 λprog,t_prog,bound. 86 (mk_relations flat_labels (operational_semantics frame_state_params frame_sem_state_paramsprog)116 (mk_relations flat_labels (operational_semantics frame_state_params (frame_sem_state_params bound) prog) 87 117 (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)) 118 frame_variable_sem_rel 90 119 (λ_.λ_.True)). 91 120 … … 204 233 205 234 definition safe_cast : ∀A,B : Type[0].A = B → A → B ≝ 206 λA,B,prf.match prf with [refl ⇒ λx : A.x]. 235 λA,B,prf.match prf with [refl ⇒ λx : A.x]. 207 236 208 237 let rec create_silent_trace_from_eval_combinators (prog : Program stack_env_params stack_instr_params flat_labels) … … 211 240 m_fold Option … eval_combinators l (store … st) = return (store … st') → 212 241 code … st = list_combinators_to_instructions l (code … st') → 213 cont … st = cont … st' → io_info … st = io_info … st' →242 cont … st = cont … st' → io_info … st = false → io_info … st = io_info … st' → 214 243 raw_trace … (operational_semantics stack_state_params (stack_sem_state_params bound) prog) st st' ≝ 215 244 match 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)245 [ nil ⇒ λprf1,prf2,prf3,prf4,prf5.safe_cast (raw_trace … (operational_semantics stack_state_params (stack_sem_state_params bound) prog) st st) 217 246 (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 .247  cons x xs ⇒ λprf1,prf2,prf3,prf4,prf5. 219 248 let next_store ≝ (opt_safe … (eval_combinators x (store … st)) ?) in 220 249 let next_st ≝ mk_state stack_state_params (list_combinators_to_instructions xs (code … st')) (cont … st') 221 250 next_store (io_info … st') in 222 let tail ≝ create_silent_trace_from_eval_combinators prog bound next_st st' xs ? (refl …) (refl …) (refl …) in251 let tail ≝ create_silent_trace_from_eval_combinators prog bound next_st st' xs ? (refl …) (refl …) ? (refl …) in 223 252 t_ind … (cost_act … (None ?)) … tail 224 253 ]. 225 254 @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 %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 % 229 258 whd in ⊢ (??%% → ?); #EQ destruct 230 259  whd @seq_sil … … 234 263 6: % 235 264 7: assumption 236 9,10: cases daemon (*io*)265 9,10: // normalize nodelta <prf5 // 237 266 *: 238 267 ] 239 268  normalize nodelta @opt_safe_elim #w #EQw change with (m_bind ?????) in prf1 :(??%?); >EQw in prf1; 240 269 >m_return_bind // 241 ] 242 qed. 243 244 lemma create_silent_trace_from_eval_combinators_ok : ∀prog,bound,st,st',l,prf1,prf2,prf3,prf4,t. 245 create_silent_trace_from_eval_combinators prog bound st st' l prf1 prf2 prf3 prf4 = t → 270  normalize nodelta <prf5 // 271 ] 272 qed. 273 274 lemma create_silent_trace_from_eval_combinators_ok : ∀prog,bound,st,st',l,prf1,prf2,prf3,prf4,prf5,t. 275 create_silent_trace_from_eval_combinators prog bound st st' l prf1 prf2 prf3 prf4 prf5 = t → 246 276 pre_silent_trace … t. 247 277 #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*) 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 250 283  #x #xs #IH #st' #st #H cases(bind_inversion ????? H) #w * #EQw #EQstore_st' 251 284 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 ] 254 qed. 255 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 ] 291 qed. 256 292 (* [ @opt_safe_elim #w' >EQw whd in ⊢ (??%% → ?); #EQ destruct assumption 257 293  % 258 294  % c'e' un baco????*) 295 296 297 298 lemma list_n_def : ∀A,n,a.(list_n A a n) = n. 299 #A #n elim n // #m #IH #a normalize @eq_f @IH 300 qed. 301 302 303 304 lemma var_initial_stack_initial : ∀prog,bound. 305 get_instr_bound (main … prog) ≤ bound  to_shift → 306 ∀s1.∀s2. 307 bool_to_Prop (lang_initial ? (frame_sem_state_params bound) prog s1) → 308 bool_to_Prop (lang_initial ? (stack_sem_state_params bound) (trans_var_prog prog) s2) → 309 frame_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 * 312 normalize 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 ] 333 qed. 334 335 336 lemma var_final_stack_final : ∀s1,s2.frame_variable_sem_rel s1 s2 → 337 bool_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 #_ *] 340 whd in ⊢ (??%% → ?); #EQcont_s2 #_ @andb_Prop [ >EQcode >EQinstr @I  >EQcont_s2 @I] 341 qed. 342 343 lemma 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 #_ #_ #_ 345 whd 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 ] 356 normalize nodelta >Hio1 // 357 qed. 358 359 lemma divide_continuation_on_frame_app : ∀ct,z,app.divide_continuation_on_frames ct (app @ z) = 360 match 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 366 elim 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 368 qed. 369 370 lemma divide_continuation_on_frame_app_nil_is_nil : ∀ct,app.divide_continuation_on_frames ct app = [ ] → 371 app = [ ]. 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 375 qed. 376 377 lemma var_instr_bond_for_empty : ∀st,x,opt_l,cd,ct. 378 var_instr_bond_ok st x (〈cost_act … opt_l,cd〉::ct) → 379 var_instr_bond_ok st cd ct. 380 #st #x #opt_l #cd #ct whd in ⊢ (% → %); whd in match (divide_continuation_on_frames ??); 381 whd in match (divide_continuation_on_frames ??) in ⊢ (? → %); >divide_continuation_on_frame_app 382 inversion(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 // 386 qed. 387 388 definition 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 ]. 405 cases io 406 qed. 407 408 lemma expr_bound_good_expr : ∀e,n.get_expr_bound e ≤ n → 409 good_expr n e. 410 #e elim e normalize /2/ #e1 #e2 #IH1 #IH2 #n #H @All_append try @IH1 try @IH2 411 change with (max (get_expr_bound e1) (get_expr_bound e2)) in H : (?%?); 412 @(transitive_le … H) /2 by le_maxl/ 413 qed. 414 415 lemma good_expr_for_var_instr_ok : ∀x,st,cd,ct,e. 416 var_instr_bond_ok (x :: st) cd ct → 417 get_top_expression_from_instr cd = return e → 418 good_expr (xto_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 422 cases(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/ 428 qed. 429 430 check frame_assign_var 431 432 lemma var_to_shift_frame_assign_var_ok : ∀st,v,val,new_st. 433 var_to_shift_ok (\fst st) → frame_assign_var st v val = return new_st → 434 var_to_shift_ok (\fst new_st). 435 cases daemon 436 qed. 437 438 lemma var_instr_bond_frame_assign_var_ok : ∀st,i,ct,v,val,new_st. 439 var_instr_bond_ok (\fst st) i ct → 440 frame_assign_var st v val = return new_st → 441 var_instr_bond_ok (\fst new_st) i ct. 442 cases daemon 443 qed. 444 445 lemma var_instr_bond_seq_ok : ∀st. 446 ∀i : frame_Instructions.∀seq,opt_l.∀ct. 447 var_instr_bond_ok st (SEQ … seq opt_l i) ct → 448 var_instr_bond_ok st i ct. 449 cases daemon 450 qed. 451 452 453 lemma var_stack_simulate_tau : 454 ∀prog : Program frame_state_params frame_state_params frame_state_params. 455 ∀bound : ℕ. 456 ∀s1.∀s2.∀s1'. 457 execute_l … (frame_sem_state_params bound) (env … prog) (cost_act … (None ?)) s1 s1'→ 458 frame_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'. 460 frame_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 524 qed. 259 525 260 526 definition simulation_imp_frame : … … 264 530 λprog,bound. 265 531 mk_simulation_conditions …. 266 cases daemon 267 qed. 532 [ @var_initial_stack_initial  @var_final_stack_final  @var_io_is_stack_io 533  @var_stack_simulate_tau 534 qed.
Note: See TracChangeset
for help on using the changeset viewer.