Changeset 3486
- Timestamp:
- Sep 24, 2014, 2:49:14 PM (6 years ago)
- Location:
- LTS
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
LTS/Simulation.ma
r3484 r3486 1 1 include "Traces.ma". 2 2 3 record relations (S 1,S2: abstract_status) : Type[0] ≝4 { Srel: S 1 → S2→ Prop5 ; Crel: S 1 → S2→ Prop3 record relations (S : abstract_status) : Type[0] ≝ 4 { Srel: S → S → Prop 5 ; Crel: S → S → Prop 6 6 }. 7 7 8 definition Rrel ≝ λS 1,S2 : abstract_status.λrel : relations S1 S2.λs,s'.9 ∀s1,s1'. as_syntactical_succ S 1 s1 s → Crel … rel s1 s1' → as_syntactical_succ S2s1' s'.10 11 record simulation_conditions (S 1,S2 : abstract_status) (rel : relations S1 S2) : Prop ≝8 definition Rrel ≝ λS : abstract_status.λrel : relations S.λs,s' : S. 9 ∀s1,s1'. as_syntactical_succ S s1 s → Crel … rel s1 s1' → as_syntactical_succ S s1' s'. 10 11 record simulation_conditions (S : abstract_status) (rel : relations S) : Prop ≝ 12 12 { initial_is_initial : 13 ∀s1,s2 .Srel … rel s1 s2 → (bool_to_Prop (as_initial … s1) → bool_to_Prop (as_initial … s2))13 ∀s1,s2 : S.Srel … rel s1 s2 → (bool_to_Prop (as_initial … s1) → bool_to_Prop (as_initial … s2)) 14 14 ; final_is_final : 15 ∀s1,s2 .Srel … rel s1 s2 → (bool_to_Prop(as_final … s1) → bool_to_Prop (as_final … s2))15 ∀s1,s2 : S.Srel … rel s1 s2 → (bool_to_Prop(as_final … s1) → bool_to_Prop (as_final … s2)) 16 16 ; simulate_tau: 17 ∀s1 :S1.∀s2:S2.∀s1':S1.17 ∀s1,s2,s1' : S. 18 18 as_execute … (cost_act (None ?)) s1 s1'→ 19 19 Srel … rel s1 s2 → as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io → 20 ∃s2'. ∃t: raw_trace S 2s2 s2'.20 ∃s2'. ∃t: raw_trace S s2 s2'. 21 21 Srel … rel s1' s2' ∧ silent_trace … t 22 22 ; simulate_label: 23 ∀s1 :S1.∀s2:S2.∀l.∀s1':S1.24 as_execute S 1(cost_act (Some ? l)) s1 s1' →23 ∀s1,s2,l,s1'. 24 as_execute S (cost_act (Some ? l)) s1 s1' → 25 25 as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io → 26 26 Srel … rel s1 s2 → 27 27 ∃s2',s2'',s2'''. 28 ∃t1: raw_trace S 2s2 s2'.28 ∃t1: raw_trace S s2 s2'. 29 29 as_execute … (cost_act (Some ? l)) s2' s2'' ∧ 30 ∃t3: raw_trace …s2'' s2'''.30 ∃t3: raw_trace S s2'' s2'''. 31 31 Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ pre_silent_trace … t3 32 32 ; simulate_call_pl: 33 ∀s1 :S1.∀s2:S2.∀s1':S1.∀f,l.33 ∀s1,s2,s1' : S.∀f,l. 34 34 is_call_post_label … s1 → 35 35 as_execute … (call_act f l) s1 s1' → … … 37 37 Srel … rel s1 s2 → 38 38 ∃s2',s2'',s2'''. 39 ∃t1: raw_trace S 2s2 s2'.39 ∃t1: raw_trace S s2 s2'. 40 40 as_execute … (call_act f l) s2' s2'' ∧ 41 41 bool_to_Prop(is_call_post_label … s2') ∧ 42 ∃t3: raw_trace S 2s2'' s2'''.42 ∃t3: raw_trace S s2'' s2'''. 43 43 Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ pre_silent_trace … t3 44 44 ; simulate_ret_l: 45 ∀s1 :S1.∀s2:S2.∀s1':S1.∀l.46 as_execute S 1(ret_act (Some ? l)) s1 s1' →45 ∀s1,s2,s1' : S.∀l. 46 as_execute S (ret_act (Some ? l)) s1 s1' → 47 47 as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io → 48 48 Srel … rel s1 s2 → 49 49 ∃s2',s2'',s2'''. 50 ∃t1: raw_trace S 2s2 s2'.50 ∃t1: raw_trace S s2 s2'. 51 51 as_execute … (ret_act (Some ? l)) s2' s2'' ∧ 52 ∃t3: raw_trace S 2s2'' s2'''.52 ∃t3: raw_trace S s2'' s2'''. 53 53 Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ pre_silent_trace … t3 54 54 ; simulate_call_n: 55 ∀s1 :S1.∀s2:S2.∀s1':S1.∀f,l.55 ∀s1,s2,s1' : S.∀f,l. 56 56 as_execute … (call_act f l) s1 s1' → 57 57 ¬ is_call_post_label … s1 → … … 59 59 Srel … rel s1 s2 → 60 60 ∃s2',s2'',s2'''. 61 ∃t1: raw_trace S 2s2 s2'.61 ∃t1: raw_trace S s2 s2'. 62 62 bool_to_Prop (¬ is_call_post_label … s2') ∧ 63 63 as_execute … (call_act f l) s2' s2'' ∧ 64 ∃t3: raw_trace S 2s2'' s2'''.64 ∃t3: raw_trace S s2'' s2'''. 65 65 Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ pre_silent_trace … t3 66 66 ∧ Crel … rel s1 s2' 67 67 ; simulate_ret_n: 68 ∀s1 :S1.∀s2:S2.∀s1':S1.68 ∀s1,s2,s1' : S. 69 69 as_execute … (ret_act (None ?)) s1 s1' → 70 70 as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io → 71 71 Srel … rel s1 s2 → 72 ∃s2',s2'',s2''' : S2.73 ∃t1: raw_trace S 2s2 s2'.72 ∃s2',s2'',s2'''. 73 ∃t1: raw_trace S s2 s2'. 74 74 as_execute … (ret_act (None ?)) s2' s2'' ∧ 75 ∃t3: raw_trace S 2s2'' s2'''.75 ∃t3: raw_trace S s2'' s2'''. 76 76 Srel … rel s1' s2''' ∧ pre_silent_trace … t1 ∧ pre_silent_trace … t3 77 77 ∧ Rrel … rel s1' s2'' 78 78 ; simulate_io_in : 79 ∀s1 :S1.∀s2:S2.∀s1':S1.∀l.79 ∀s1,s2,s1' : S.∀l. 80 80 as_execute … (cost_act … (Some ? l)) s1 s1' → 81 81 as_classify … s1 ≠ cl_io → as_classify … s1' = cl_io → 82 82 Srel … rel s1 s2 → 83 ∃s2',s2'' .∃t: raw_trace … s2 s2'.83 ∃s2',s2'' : S.∃t: raw_trace … s2 s2'. 84 84 pre_silent_trace … t ∧ as_execute … (cost_act … (Some ? l)) s2' s2'' ∧ 85 85 as_classify … s2'' = cl_io ∧ Srel … rel s1' s2'' 86 86 ; simulate_io_out : 87 ∀s1:S1.∀s2:S2.∀s1':S1.∀l.87 ∀s1,s2,s1' : S.∀l. 88 88 as_execute … (cost_act … (Some ? l)) s1 s1' → 89 89 as_classify … s1 = cl_io → as_classify … s1' ≠ cl_io → 90 90 Srel … rel s1 s2 → 91 ∃s2',s2'' .∃t : raw_trace … s2' s2''.91 ∃s2',s2'' : S.∃t : raw_trace … s2' s2''. 92 92 pre_silent_trace … t ∧ as_execute … (cost_act … (Some ? l)) s2 s2' ∧ 93 93 as_classify … s2 = cl_io ∧ Srel … rel s1' s2'' … … 261 261 qed. 262 262 263 263 264 theorem simulates_pre_mesurable: 264 ∀S 1,S2 : abstract_status.∀rel : relations S1 S2.265 ∀s1,s1' : S 1. ∀t1: raw_trace S1s1 s1'.266 simulation_conditions …rel →265 ∀S : abstract_status.∀rel : relations S. 266 ∀s1,s1' : S. ∀t1: raw_trace S s1 s1'. 267 simulation_conditions S rel → 267 268 pre_measurable_trace … t1 → 268 ∀s2 : S 2.269 ∀s2 : S. 269 270 as_classify … s2 ≠ cl_io → Srel … rel s1 s2 → 270 271 ∃s2'. ∃t2: raw_trace … s2 s2'. … … 272 273 get_costlabels_of_trace … t1 = get_costlabels_of_trace … t2 ∧ 273 274 Srel … rel s1' s2'. 274 #S 1 #S2#rel #s1 #s1' #t1 #good #pre_measurable elim pre_measurable275 #S #rel #s1 #s1' #t1 #good #pre_measurable elim pre_measurable 275 276 [ #st #H1 #s2 #REL #Hs2 %{s2} %{(t_base …)} 276 277 /8 by refl, silent_empty, conj, pre_silent_is_premeasurable/ … … 401 402 402 403 record measurable_trace (S : abstract_status) : Type[0] ≝ 403 { L_label: option ActionLabel 404 ; R_label : option ActionLabel 405 ; L_pre_state : option S 406 ; L_s1 : S 404 { L_s1 : S 407 405 ; R_s2: S 408 ; R_post_state : option S409 406 ; trace : raw_trace S L_s1 R_s2 410 407 ; pre_meas : pre_measurable_trace … trace 411 ; L_init_ok : match L_pre_state with 412 [ None ⇒ bool_to_Prop(as_initial … L_s1) ∧ L_label = None ? 413 | Some s ⇒ ∃l. L_label = Some ? l ∧ is_costlabelled_act l ∧ 414 as_execute … l s L_s1 415 ] 416 ; R_fin_ok : match R_label with 417 [ None ⇒ bool_to_Prop (as_final … R_s2) ∧ R_post_state = None ? 418 | Some l ⇒ (is_costlabelled_act l ∨ is_unlabelled_ret_act l) ∧ 419 (is_call_act l → bool_to_Prop (is_call_post_label … R_s2)) ∧ 420 ∃ s'.R_post_state = Some ? s' ∧ as_execute … l R_s2 s' 421 ] 422 }. 408 }. 423 409 424 410 lemma cl_io_case : ∀P : status_class → Prop. P cl_io → (∀x.x≠cl_io → P x) → ∀s.P s. … … 450 436 qed. 451 437 452 lemma instr_execute_commute : ∀S 1,S2:abstract_status.453 ∀rel : relations S 1 S2.438 lemma instr_execute_commute : ∀S :abstract_status. 439 ∀rel : relations S. 454 440 simulation_conditions … rel → 455 ∀s1,s1': S 1.∀l.l ≠ cost_act (None ?) → as_execute …l s1 s1' →441 ∀s1,s1': S.∀l.l ≠ cost_act (None ?) → as_execute S l s1 s1' → 456 442 (as_classify … s1 ≠ cl_io ∨ as_classify … s1' ≠ cl_io) → 457 443 ∀s2. 458 444 Srel … rel s1 s2 → 459 ∃s2' : S 2.∃tr : raw_trace …s2 s2'.silent_trace … tr ∧460 ∃s2'' : S 2.as_execute … l s2' s2'' ∧ ∃s2''' : S2.461 ∃tr' : raw_trace …s2'' s2'''. silent_trace … tr' ∧ Srel … rel s1' s2''' ∧445 ∃s2' : S.∃tr : raw_trace S s2 s2'.silent_trace … tr ∧ 446 ∃s2'' : S.as_execute S l s2' s2'' ∧ ∃s2''' : S. 447 ∃tr' : raw_trace S s2'' s2'''. silent_trace … tr' ∧ Srel … rel s1' s2''' ∧ 462 448 (is_call_act l → is_call_post_label … s1 → is_call_post_label … s2') ∧ 463 449 (as_classify … s1' ≠ cl_io → as_classify … s2'' ≠ cl_io). 464 #S 1 #S2#rel #good #s1 #s1' #l #l_notau #prf #HIO #s2 #REL cases(case_cl_io … (as_classify … s1))450 #S #rel #good #s1 #s1' #l #l_notau #prf #HIO #s2 #REL cases(case_cl_io … (as_classify … s1)) 465 451 [ #EQs1_io cases(io_exiting … EQs1_io … prf) #lab #EQ destruct(EQ) 466 452 cases HIO [ >EQs1_io * #EQ @⊥ @EQ % ] #Hio_s1' … … 513 499 qed. 514 500 501 (* 515 502 theorem simulate_LR_trace : 516 ∀S 1,S2: abstract_status.517 ∀t : measurable_trace S 1.518 ∀rel : relations S 1 S2.503 ∀S : abstract_status. 504 ∀t : measurable_trace S. 505 ∀rel : relations S. 519 506 simulation_conditions … rel → 520 ∀s2 : S 2.507 ∀s2 : S. 521 508 match L_pre_state … t with 522 509 [ None ⇒ … … 524 511 Srel … rel (L_s1 … t) s2 525 512 | Some s1 ⇒ Srel … rel s1 s2 ] → 526 ∃t' : measurable_trace S 2.513 ∃t' : measurable_trace S. 527 514 L_label … t = L_label … t' ∧ R_label … t = R_label … t' ∧ 528 515 get_costlabels_of_trace … (trace … t) = … … 531 518 [ None ⇒ L_s1 … t' = s2 532 519 | Some s1 ⇒ 533 ∃ pre_state : S 2.520 ∃ pre_state : S. 534 521 L_pre_state … t' = Some ? pre_state ∧ 535 ∃tr_i : raw_trace …s2 pre_state. silent_trace … tr_i522 ∃tr_i : raw_trace S s2 pre_state. silent_trace … tr_i 536 523 ] ∧ 537 524 match R_post_state … t with 538 525 [ None ⇒ Srel … rel (R_s2 … t) (R_s2 … t') 539 526 | Some s1' ⇒ 540 ∃s2' : S 2. Srel … rel s1' s2' ∧541 ∃ post_state : S 2.527 ∃s2' : S. Srel … rel s1' s2' ∧ 528 ∃ post_state : S. 542 529 R_post_state … t' = Some ? post_state ∧ 543 ∃tr : raw_trace …post_state s2'. silent_trace … tr530 ∃tr : raw_trace S post_state s2'. silent_trace … tr 544 531 ]. 545 #S 1 #S2#t #rel #good #s2 inversion(L_pre_state … t) [| #pre_s1] #EQpre normalize nodelta [* #Hclass_s2 ]532 #S #t #rel #good #s2 inversion(L_pre_state … t) [| #pre_s1] #EQpre normalize nodelta [* #Hclass_s2 ] 546 533 [2: #REL_pre 547 534 cut 548 (∃pre_state .∃ l.549 ∃tr_i : raw_trace …s2 pre_state. silent_trace … tr_i ∧550 ∃middle_state .L_label … t = Some ? l ∧535 (∃pre_state: S.∃ l. 536 ∃tr_i : raw_trace S s2 pre_state. silent_trace … tr_i ∧ 537 ∃middle_state: S.L_label … t = Some ? l ∧ 551 538 as_execute … l pre_state middle_state ∧ 552 ∃final_state .553 ∃tr_i2: raw_trace …middle_state final_state. silent_trace … tr_i2 ∧539 ∃final_state: S. 540 ∃tr_i2: raw_trace S middle_state final_state. silent_trace … tr_i2 ∧ 554 541 as_classify … final_state ≠ cl_io ∧ 555 542 Srel … rel (L_s1 … t) final_state) … … 566 553 * #final_state * #tr_i2 ** #silent_i2 #final_not_io #REL 567 554 | #REL 568 cut(bool_to_Prop (as_initial … s2)∧L_label …t=None ?)555 cut(bool_to_Prop (as_initial S s2)∧L_label S t=None ?) 569 556 [ lapply(L_init_ok … t) >EQpre normalize nodelta * #H1 #H2 % [2: //] 570 557 @(initial_is_initial … good … H1) assumption ] * #initial_s2 #init_label … … 573 560 #fin_s2 * #t' ** #pre_meas_t' #EQcost #REL' inversion(R_post_state … t) 574 561 [2,4: #post_s2] #EQpost normalize nodelta 575 [3,4: cut (match R_label …t in option return λ_:(option ActionLabel).Prop with576 [None⇒bool_to_Prop (as_final … fin_s2)∧None S2=None S2562 [3,4: cut (match R_label S t in option return λ_:(option ActionLabel).Prop with 563 [None⇒bool_to_Prop (as_final S fin_s2)∧None S=None S 577 564 |Some (l:ActionLabel)⇒ 578 565 (is_costlabelled_act l∨is_unlabelled_ret_act l) 579 ∧(is_call_act l→is_call_post_label …fin_s2)580 ∧(∃s' .None S2=Some … s'∧as_execute …l fin_s2 s')])566 ∧(is_call_act l→is_call_post_label S fin_s2) 567 ∧(∃s':S.None S=Some S s'∧as_execute S l fin_s2 s')]) 581 568 [1,3: lapply(R_fin_ok … t) cases(R_label … t) normalize nodelta 582 569 [1,3: * #H1 #H2 % [2,4: //] @(final_is_final … good … H1) assumption … … 588 575 #a #_ %{a} % ] * #final_label #EQfinal_label 589 576 cut 590 (∃middle_state .591 ∃tr : raw_trace …fin_s2 middle_state. silent_trace … tr ∧592 ∃post_state .577 (∃middle_state: S. 578 ∃tr : raw_trace S fin_s2 middle_state. silent_trace … tr ∧ 579 ∃post_state : S. 593 580 as_execute … final_label middle_state post_state ∧ 594 581 (is_call_act final_label → bool_to_Prop (is_call_post_label … middle_state)) ∧ 595 ∃final_state .596 ∃tr_f2: raw_trace …post_state final_state. silent_trace … tr_f2 ∧582 ∃final_state: S. 583 ∃tr_f2: raw_trace S post_state final_state. silent_trace … tr_f2 ∧ 597 584 Srel … rel post_s2 final_state) 598 585 [1,3: lapply(R_fin_ok … t) >EQfinal_label normalize nodelta ** #H1 #H2 * #sfin … … 846 833 ] 847 834 *) 835 *) -
LTS/Vm.ma
r3485 r3486 15 15 { seq_instr : Type[0] 16 16 ; jump_condition : Type[0] 17 ; io_instr : Type[0] 18 ; entry_of_function : FunctionName → ℕ 19 ; call_label_fun : list (ℕ × CallCostLabel) 20 ; return_label_fun : list (ℕ × ReturnPostCostLabel) 21 }. 17 ; io_instr : Type[0] }. 22 18 23 19 inductive AssemblerInstr (p : assembler_params) : Type[0] ≝ … … 29 25 | Iret: AssemblerInstr p. 30 26 27 definition labels_pc_of_instr : ∀p.AssemblerInstr p → ℕ → list (CostLabel × ℕ) ≝ 28 λp,i,program_counter. 29 match i with 30 [ Seq _ opt_l ⇒ match opt_l with 31 [ Some lbl ⇒ [〈(a_non_functional_label lbl),S program_counter〉] 32 | None ⇒ [ ] 33 ] 34 | Ijmp _ ⇒ [ ] 35 | CJump _ newpc ltrue lfalse ⇒ [〈(a_non_functional_label ltrue),newpc〉; 36 〈(a_non_functional_label lfalse),S program_counter〉] 37 | Iio lin _ lout ⇒ [〈(a_non_functional_label lin),program_counter〉; 38 〈(a_non_functional_label lout),S program_counter〉] 39 | Icall f ⇒ [ ] 40 | Iret ⇒ [ ] 41 ]. 42 43 let rec labels_pc (p : assembler_params) 44 (prog : list (AssemblerInstr p)) (call_label_fun : list (ℕ × CallCostLabel)) 45 (return_label_fun : list (ℕ × ReturnPostCostLabel)) (i_act : NonFunctionalLabel) 46 (program_counter : ℕ) on prog : list (CostLabel × ℕ) ≝ 47 match prog with 48 [ nil ⇒ [〈a_non_functional_label (i_act),O〉] @ 49 map … (λx.let〈y,z〉 ≝ x in 〈(a_call z),y〉) (call_label_fun) @ 50 map … (λx.let〈y,z〉 ≝ x in 〈(a_return_post z),y〉) (return_label_fun) 51 | cons i is ⇒ (labels_pc_of_instr … i program_counter)@labels_pc p is call_label_fun return_label_fun i_act (S program_counter) 52 ]. 53 54 include "basics/lists/listb.ma". 55 56 (*doppione da mettere a posto*) 57 let rec no_duplicates (A : DeqSet) (l : list A) on l : Prop ≝ 58 match l with 59 [ nil ⇒ True 60 | cons x xs ⇒ ¬ (bool_to_Prop (x ∈ xs)) ∧ no_duplicates … xs 61 ]. 62 63 31 64 record AssemblerProgram (p : assembler_params) : Type[0] ≝ 32 65 { instructions : list (AssemblerInstr p) 33 66 ; endmain : ℕ 34 67 ; endmain_ok : endmain < |instructions| 68 ; entry_of_function : FunctionName → ℕ 69 ; call_label_fun : list (ℕ × CallCostLabel) 70 ; return_label_fun : list (ℕ × ReturnPostCostLabel) 71 ; in_act : NonFunctionalLabel 72 ; asm_no_duplicates : no_duplicates … (map ?? \fst … (labels_pc … instructions call_label_fun return_label_fun in_act O)) 35 73 }. 74 36 75 37 76 definition fetch: ∀p.AssemblerProgram p → ℕ → option (AssemblerInstr p) ≝ … … 137 176 S (pc … st1) :: asm_stack … st1 = asm_stack … st2 → 138 177 asm_is_io … st1 = asm_is_io … st2 → 139 entry_of_function pf = pc … st2 →178 entry_of_function … prog f = pc … st2 → 140 179 op … (cost … st1) (cost_of p p' (Icall p f) (asm_store … st1)) = cost … st2 → 141 label_of_pc ? (call_label_fun p) (entry_of_function pf) = return lbl →180 label_of_pc ? (call_label_fun … prog) (entry_of_function … prog f) = return lbl → 142 181 vmstep … (call_act f lbl) st1 st2 143 182 | vm_ret : … … 149 188 asm_is_io … st1 = asm_is_io … st2 → 150 189 newpc = pc … st2 → 151 label_of_pc ? (return_label_fun p) newpc = return lbl →190 label_of_pc ? (return_label_fun … prog) newpc = return lbl → 152 191 op … (cost … st1) (cost_of p p' (Iret p) (asm_store … st1)) = cost … st2 → 153 192 vmstep … (ret_act (Some ? lbl)) st1 st2. … … 202 241 None ? 203 242 else 204 ! lbl ← label_of_pc ? (call_label_fun p) (entry_of_function pf);243 ! lbl ← label_of_pc ? (call_label_fun … prog) (entry_of_function … prog f); 205 244 return 〈call_act f lbl, 206 mk_vm_state ?? (entry_of_function pf)245 mk_vm_state ?? (entry_of_function … prog f) 207 246 ((S (pc … st)) :: (asm_stack … st)) 208 247 (asm_store … st) false … … 212 251 else 213 252 ! 〈newpc,tl〉 ← option_pop … (asm_stack … st); 214 ! lbl ← label_of_pc ? (return_label_fun p) newpc;253 ! lbl ← label_of_pc ? (return_label_fun … prog) newpc; 215 254 return 〈ret_act (Some ? lbl), 216 255 mk_vm_state ?? newpc tl (asm_store … st) false … … 291 330 discriminator option. 292 331 332 inductive vm_ass_state (p : assembler_params) (p' : sem_params p) : Type[0] ≝ 333 | INITIAL : vm_ass_state p p' 334 | FINAL : vm_ass_state p p' 335 | STATE : vm_state p p' → vm_ass_state p p'. 336 293 337 definition asm_operational_semantics : ∀p.sem_params p → AssemblerProgram p → abstract_status ≝ 294 λp,p',prog.mk_abstract_status 295 (vm_state p p') 296 (λl.λst1,st2 : vm_state p p'.(eqb (pc ?? st1) (endmain … prog)) = false ∧ 297 vmstep p p' prog l st1 st2) 338 λp,p',prog.let init_act ≝ cost_act (Some ? (in_act … prog)) in 339 let end_act ≝ cost_act (Some ? (in_act … prog)) in 340 mk_abstract_status 341 (vm_ass_state p p') 342 (λl.λs1,s2 : vm_ass_state p p'. 343 match s1 with 344 [ STATE st1 ⇒ 345 match s2 with 346 [ STATE st2 ⇒ 347 (eqb (pc ?? st1) (endmain … prog)) = false ∧ vmstep p p' prog l st1 st2 348 | INITIAL ⇒ False 349 | FINAL ⇒ eqb (pc … st1) (endmain … prog) = true ∧ l = end_act 350 ] 351 | INITIAL ⇒ match s2 with 352 [ STATE st2 ⇒ eqb (pc … st2) O = true ∧ l = init_act 353 | _ ⇒ False 354 ] 355 | FINAL ⇒ False 356 ]) 298 357 (λ_.λ_.True) 299 (λs.match fetch … prog (pc … s) with 300 [ Some i ⇒ match i with 358 (λst.match st with 359 [ INITIAL ⇒ cl_other | FINAL ⇒ cl_other | 360 STATE s ⇒ 361 match fetch … prog (pc … s) with 362 [ Some i ⇒ match i with 301 363 [ Seq _ _ ⇒ cl_other 302 364 | Ijmp _ ⇒ cl_other … … 306 368 | Iret ⇒ cl_other 307 369 ] 308 | None ⇒ cl_other 370 | None ⇒ cl_other 371 ] 309 372 ] 310 373 ) 311 374 (λ_.true) 312 (λs. eqb (pc ?? s) O)313 (λs. eqb (pc … s) (endmain … prog))375 (λs.match s with [ INITIAL ⇒ true | _ ⇒ false]) 376 (λs.match s with [ FINAL ⇒ true | _ ⇒ false]) 314 377 ???. 315 @hide_prf 378 @hide_prf cases daemon qed. (* 316 379 [ #s1 #s2 #l inversion(fetch ???) normalize nodelta 317 380 [ #_ #EQ destruct] * normalize nodelta … … 366 429 normalize nodelta #H cases(bind_inversion ????? H) -H #x * #_ 367 430 whd in ⊢ (??%% → ?); #EQ destruct % // 368 qed. 431 qed.*) 369 432 370 433 definition asm_concrete_trans_sys ≝ 371 434 λp,p',prog.mk_concrete_transition_sys … 372 (asm_operational_semantics p p' prog) (m … p') (cost …). 435 (asm_operational_semantics p p' prog) (m … p') 436 (λs.match s with [STATE st ⇒ cost … st | _ ⇒ e …] ). 373 437 374 438 definition emits_labels ≝ … … 387 451 definition asm_static_analisys_data ≝ λp,p',prog,abs_t,instr_m. 388 452 mk_static_analysis_data (asm_concrete_trans_sys p p' prog) abs_t 389 … ( fetch_state p p' prog) instr_m.453 … (λs.match s with [ STATE st ⇒ fetch_state p p' prog st | _ ⇒ None ? ]) instr_m. 390 454 391 455 definition non_empty_list : ∀A.list A → bool ≝ … … 395 459 (prog: AssemblerProgram p) (abs_t : monoid) 396 460 (instr_m : AssemblerInstr p → abs_t) 397 (prog ram_counter:ℕ)461 (prog_c: option ℕ) 398 462 (program_size: ℕ) 399 463 on program_size: option abs_t ≝ 400 match program_size with 401 [ O ⇒ None ? 402 | S program_size' ⇒ 403 if eqb program_counter (endmain … prog) then 404 return e … abs_t 405 else 406 ! instr ← fetch … prog program_counter; 407 ! n ← (match emits_labels … instr with 408 [ Some f ⇒ block_cost … prog abs_t instr_m (f program_counter) program_size' 409 | None ⇒ return e … 410 ]); 411 return (op … abs_t (instr_m … instr) n) 412 ]. 464 match prog_c with 465 [ None ⇒ return e … abs_t 466 | Some program_counter ⇒ 467 match program_size with 468 [ O ⇒ None ? 469 | S program_size' ⇒ 470 if eqb program_counter (endmain … prog) then 471 return e … abs_t 472 else 473 ! instr ← fetch … prog program_counter; 474 ! n ← (match emits_labels … instr with 475 [ Some f ⇒ block_cost … prog abs_t instr_m (Some ? (f program_counter)) program_size' 476 | None ⇒ return e … 477 ]); 478 return (op … abs_t (instr_m … instr) n) 479 ] 480 ]. 413 481 414 482 … … 422 490 }. 423 491 424 definition labels_pc_of_instr : ∀p.AssemblerInstr p → ℕ → list (CostLabel × ℕ) ≝ 425 λp,i,program_counter. 426 match i with 427 [ Seq _ opt_l ⇒ match opt_l with 428 [ Some lbl ⇒ [〈(a_non_functional_label lbl),S program_counter〉] 429 | None ⇒ [ ] 430 ] 431 | Ijmp _ ⇒ [ ] 432 | CJump _ newpc ltrue lfalse ⇒ [〈(a_non_functional_label ltrue),newpc〉; 433 〈(a_non_functional_label lfalse),S program_counter〉] 434 | Iio lin _ lout ⇒ [〈(a_non_functional_label lin),program_counter〉; 435 〈(a_non_functional_label lout),S program_counter〉] 436 | Icall f ⇒ [ ] 437 | Iret ⇒ [ ] 438 ]. 439 440 let rec labels_pc (p : assembler_params) 441 (prog : list (AssemblerInstr p)) (program_counter : ℕ) on prog : list (CostLabel × ℕ) ≝ 442 match prog with 443 [ nil ⇒ [〈i_act,O〉] @ 444 map … (λx.let〈y,z〉 ≝ x in 〈(a_call z),y〉) (call_label_fun … p) @ 445 map … (λx.let〈y,z〉 ≝ x in 〈(a_return_post z),y〉) (return_label_fun … p) 446 | cons i is ⇒ (labels_pc_of_instr … i program_counter)@labels_pc p is (S program_counter) 447 ]. 448 449 lemma labels_pc_ok : ∀p,prog,i,lbl,pc,m. 492 493 494 lemma labels_pc_ok : ∀p,prog,l1,l2,i_act,i,lbl,pc,m. 450 495 nth_opt ? pc prog = return i → 451 496 mem ? lbl (labels_pc_of_instr … i (m+pc)) → 452 mem ? lbl (labels_pc p prog m).453 #p #instrs # i #lbl #pc497 mem ? lbl (labels_pc p prog l1 l2 i_act m). 498 #p #instrs #l1 #l2 #iact #i #lbl #pc 454 499 whd in match fetch; normalize nodelta lapply pc -pc 455 500 elim instrs 456 501 [ #pc #m whd in ⊢ (??%% → ?); #EQ destruct] 457 #x #xs #IH * [|#pc'] #m whd in ⊢ (??%% → ?);502 #x #xs #IH * [|#pc'] #m whd in ⊢ (??%% → ?); 458 503 [ #EQ destruct #lbl_addr whd in match (labels_pc ???); 459 504 /2 by mem_append_l1/ … … 462 507 qed. 463 508 464 lemma labels_pc_return: ∀p,prog, x1,x2.465 label_of_pc ReturnPostCostLabel (return_label_fun p)x1=return x2 →509 lemma labels_pc_return: ∀p,prog,l1,l2,iact,x1,x2. 510 label_of_pc ReturnPostCostLabel l2 x1=return x2 → 466 511 ∀m. 467 mem … 〈(a_return_post x2),x1〉 (labels_pc p prog m).468 #p #l whd in match (labels_pc ???); #x1 #x2 #H elim l512 mem … 〈(a_return_post x2),x1〉 (labels_pc p prog l1 l2 iact m). 513 #p #l #l1 #l2 #iact whd in match (labels_pc ???); #x1 #x2 #H elim l 469 514 [ #m @mem_append_l2 @mem_append_l2 whd in H:(??%?); 470 elim (return_label_fun ?)in H; [ whd in ⊢ (??%% → ?); #EQ destruct]515 elim l2 in H; [ whd in ⊢ (??%% → ?); #EQ destruct] 471 516 * #x #y #tl #IH whd in ⊢ (??%? → %); normalize nodelta @eqb_elim 472 517 normalize nodelta … … 476 521 qed. 477 522 478 lemma labels_pc_call: ∀p,prog, x1,x2.479 label_of_pc CallCostLabel (call_label_fun p)x1=return x2 →523 lemma labels_pc_call: ∀p,prog,l1,l2,iact,x1,x2. 524 label_of_pc CallCostLabel l1 x1=return x2 → 480 525 ∀m. 481 mem … 〈(a_call x2),x1〉 (labels_pc p prog m).482 #p #l whd in match (labels_pc ???); #x1 #x2 #H elim l526 mem … 〈(a_call x2),x1〉 (labels_pc p prog l1 l2 iact m). 527 #p #l #l1 #l2 #iact whd in match (labels_pc ???); #x1 #x2 #H elim l 483 528 [ #m @mem_append_l2 @mem_append_l1 whd in H:(??%?); 484 elim (call_label_fun ?)in H; [ whd in ⊢ (??%% → ?); #EQ destruct]529 elim l1 in H; [ whd in ⊢ (??%% → ?); #EQ destruct] 485 530 * #x #y #tl #IH whd in ⊢ (??%? → %); normalize nodelta @eqb_elim 486 531 normalize nodelta … … 520 565 λp,abs_t,instr_m,mT,prog. 521 566 let prog_size ≝ S (|instructions … prog|) in 522 m_foldr Option ?? (λx,m.let 〈z,w〉≝ x in ! k ← block_cost p prog abs_t instr_m w prog_size; 523 return set_map … m z k) (labels_pc … (instructions … prog) O) 567 m_foldr Option ?? (λx,m.let 〈z,w〉≝ x in ! k ← block_cost p prog abs_t instr_m (Some ? w) prog_size; 568 return set_map … m z k) (labels_pc … (instructions … prog) 569 (call_label_fun … prog) (return_label_fun … prog) (in_act … prog) O) 524 570 (empty_map ?? mT). 525 571 526 527 include "basics/lists/listb.ma".528 529 (*doppione da mettere a posto*)530 let rec no_duplicates (A : DeqSet) (l : list A) on l : Prop ≝531 match l with532 [ nil ⇒ True533 | cons x xs ⇒ ¬ (bool_to_Prop (x ∈ xs)) ∧ no_duplicates … xs534 ].535 536 definition asm_no_duplicates ≝537 λp,prog.no_duplicates … (map ?? \fst … (labels_pc … (instructions p prog) O)).538 572 539 573 (*falso: necessita di no_duplicates*) … … 577 611 578 612 lemma static_analisys_ok : ∀p,abs_t,instr_m,mT,prog,lbl,pc,map. 579 asm_no_duplicates p prog →580 613 static_analisys p abs_t instr_m mT prog = return map → 581 mem … 〈lbl,pc〉 (labels_pc … (instructions … prog) O) → 614 mem … 〈lbl,pc〉 (labels_pc … (instructions … prog) (call_label_fun … prog) 615 (return_label_fun … prog) (in_act … prog) O) → 582 616 get_map … map lbl = 583 block_cost … prog abs_t instr_m pc(S (|(instructions … prog)|)) ∧584 block_cost … prog abs_t instr_m pc(S (|(instructions … prog)|)) ≠ None ?.617 block_cost … prog abs_t instr_m (Some ? pc) (S (|(instructions … prog)|)) ∧ 618 block_cost … prog abs_t instr_m (Some ? pc) (S (|(instructions … prog)|)) ≠ None ?. 585 619 #p #abs_t #instr_m #mT * #prog whd in match static_analisys; normalize nodelta 586 whd in match asm_no_duplicates; normalize nodelta lapply (labels_pc ???) 587 #l #endmain #Hendmain elim l [ #x #y #z #w #h * ] 588 * #hd1 #hd2 #tl #IH #lbl #pc #map * #H1 #H2 #H 620 #endmain #Hendmain #entry_fun #call_label_fun #return_label_fun #inact 621 #nodup generalize in match nodup in ⊢ (∀_.∀_.∀_. (??(????%??)?) → %); #Hnodup lapply nodup -nodup 622 lapply (labels_pc ??????) #l elim l [ #x #y #z #w #h * ] 623 * #hd1 #hd2 #tl #IH * #H1 #H2 #lbl #pc #map #H 589 624 cases(bind_inversion ????? H) -H #map1 * #EQmap1 normalize nodelta #H 590 625 cases(bind_inversion ????? H) -H #elem * #EQelem whd in ⊢ (??%% → ?); #EQ … … 602 637 include "Simulation.ma". 603 638 604 record terminated_trace (S : abstract_status) (R_s2 : S) : Type[0] ≝ 605 { R_post_step : option (ActionLabel × S) 606 ; R_fin_ok : match R_post_step with 607 [ None ⇒ bool_to_Prop (as_final … R_s2) 608 | Some x ⇒ let 〈l,R_post_state〉≝ x in 609 (is_costlabelled_act l ∨ is_labelled_ret_act l) ∧ 610 (is_call_act l → bool_to_Prop (is_call_post_label … R_s2)) ∧ 611 as_execute … l R_s2 R_post_state 612 ] 613 }. 639 definition terminated_trace : ∀S : abstract_status.∀s1,s3 : S.raw_trace … s1 s3 → Prop ≝ 640 λS,s1,s3,t.bool_to_Prop (as_final … s3) ∨ 641 ∃s2: S.∃t1 : raw_trace … s1 s2.∃ l,prf.t = t1 @ (t_ind ? s2 s3 s3 l prf … (t_base … s3)) 642 ∧ ((is_costlabelled_act l ∨ is_labelled_ret_act l) ∧ 643 (is_call_act l → bool_to_Prop (is_call_post_label … s2))). 614 644 615 645 definition big_op: ∀M: monoid. list M → M ≝ … … 643 673 644 674 lemma monotonicity_of_block_cost : ∀p,prog,abs_t,instr_m,pc,size,k. 645 block_cost p prog abs_t instr_m pcsize = return k →675 block_cost p prog abs_t instr_m (Some ? pc) size = return k → 646 676 ∀size'.size ≤ size' → 647 block_cost p prog abs_t instr_m pcsize' = return k.677 block_cost p prog abs_t instr_m (Some ? pc) size' = return k. 648 678 #p #prog #abs_t #instr_m #pc #size lapply pc elim size 649 679 [ #pc #k whd in ⊢ (??%% → ?); #EQ destruct] … … 678 708 match x with [None⇒[]|Some c⇒[a_non_functional_label c]] 679 709 ] = [x] ∧ 680 (mem … 〈x,pc … st2〉 (labels_pc p (instructions … prog) O)).710 (mem … 〈x,pc … st2〉 (labels_pc p (instructions … prog) (call_label_fun … prog) (return_label_fun … prog) (in_act … prog) O)). 681 711 #p #p' #prog #st1 #st2 #l #i #EQi whd in match eval_vmstate; normalize nodelta 682 712 >EQi >m_return_bind normalize nodelta cases i in EQi; -i normalize nodelta … … 733 763 734 764 lemma labels_of_trace_are_in_code : 735 ∀p,p',prog.∀st1,st2 : vm_ state p p'.∀t : raw_trace (asm_operational_semantics p p' prog) … st1 st2.765 ∀p,p',prog.∀st1,st2 : vm_ass_state p p'.∀t : raw_trace (asm_operational_semantics p p' prog) … st1 st2. 736 766 ∀lbl. 737 767 mem … lbl (get_costlabels_of_trace … t) → 738 mem … (lbl) (map ?? \fst … (labels_pc … (instructions p prog) O)). 768 mem … (lbl) (map ?? \fst … (labels_pc … (instructions p prog) (call_label_fun … prog) (return_label_fun … prog) (in_act … prog) O)). 769 cases daemon (* 739 770 #p #p' #prog #st1 #st2 #t elim t 740 771 [ #st #lbl * … … 749 780 * 750 781 ] 751 ] 782 ] *) 752 783 qed. 753 784 … … 774 805 qed. 775 806 776 777 lemma static_dynamic : ∀p,p',prog.∀no_dup : asm_no_duplicates p prog. 807 definition get_pc : ∀p,p'.vm_ass_state p p' → ℕ → option ℕ ≝ 808 λp,p',st,endmain.match st with 809 [ STATE s ⇒ Some ? (pc … s) 810 | INITIAL ⇒ None ? 811 | FINAL ⇒ Some ? endmain 812 ]. 813 814 815 lemma static_dynamic : ∀p,p',prog. 778 816 ∀abs_t : abstract_transition_sys (m … p').∀instr_m. 779 817 ∀good : static_galois … (asm_static_analisys_data p p' prog abs_t instr_m).∀mT,map1. 780 818 ∀EQmap : static_analisys p ? instr_m mT prog = return map1. 781 ∀st1,st2 : vm_state p p'. 782 ∀ter : terminated_trace (asm_operational_semantics p p' prog) st2. 819 ∀st1,st2 : vm_ass_state p p'. 783 820 ∀t : raw_trace (asm_operational_semantics p p' prog) … st1 st2. 821 terminated_trace … t → 784 822 ∀k. 785 823 pre_measurable_trace … t → 786 block_cost p prog … instr_m ( pc … st1) (S (|(instructions … prog)|)) = return k →824 block_cost p prog … instr_m (get_pc … st1 (endmain … prog)) (S (|(instructions … prog)|)) = return k → 787 825 ∀a1.rel_galois … good st1 a1 → 788 let stop_state ≝ match R_post_step … ter with [None ⇒ st2 | Some x ⇒ \snd x ] in 789 ∀costs. 790 costs = dependent_map CostLabel ? (get_costlabels_of_trace … t) (λlbl,prf.(opt_safe … (get_map … map1 lbl) ?)) → 791 rel_galois … good stop_state (act_abs … abs_t (big_op … costs) (act_abs … abs_t k a1)). 826 ∀labels. 827 labels = dependent_map CostLabel ? (get_costlabels_of_trace … t) (λlbl,prf.(opt_safe … (get_map … map1 lbl) ?)) → 828 rel_galois … good st2 (act_abs … abs_t (big_op … labels) (act_abs … abs_t k a1)). 792 829 [2: @hide_prf 793 830 cases(mem_map ????? (labels_of_trace_are_in_code … prf)) * 794 831 #lbl' #pc * #Hmem #EQ destruct 795 >(proj1 … (static_analisys_ok … no_dup … EQmap … Hmem)) 796 @(proj2 … (static_analisys_ok … no_dup … EQmap … Hmem)) 797 ] 798 #p #p' #prog #no_dup #abs_t #instr_m #good #mT #map1 #EQmap #st1 #st2 #ter #t 799 lapply ter -ter elim t 800 [ #st #ter inversion(R_post_step … ter) normalize nodelta [| * #lbl #st3 ] 832 >(proj1 … (static_analisys_ok … EQmap … Hmem)) 833 @(proj2 … (static_analisys_ok … EQmap … Hmem)) 834 ] 835 #p #p' #prog #abs_t #instr_m #good #mT #map1 #EQmap #st1 #st2 #t elim t 836 [ #st * [| * #st3 * #t1 * #l * #prf * #ABS @⊥ cases t1 in ABS; ] 801 837 #EQr_post #k #_ lapply(R_fin_ok … ter) >EQr_post normalize nodelta 802 838 [ whd in ⊢ (?% → ?); #final_st whd in ⊢ (??%? → ?); >final_st
Note: See TracChangeset
for help on using the changeset viewer.