Changeset 3486


Ignore:
Timestamp:
Sep 24, 2014, 2:49:14 PM (6 years ago)
Author:
piccolo
Message:
 
Location:
LTS
Files:
2 edited

Legend:

Unmodified
Added
Removed

  • LTS/Simulation.ma

    r3484 r3486  
    11include "Traces.ma".
    22
    3 record relations (S1,S2 : abstract_status) : Type[0] ≝
    4  { Srel: S1 → S2 → Prop
    5  ; Crel: S1 → S2 → Prop
     3record relations (S : abstract_status) : Type[0] ≝
     4 { Srel: S → S → Prop
     5 ; Crel: S → S → Prop
    66 }.
    77
    8 definition Rrel ≝ λS1,S2 : abstract_status.λrel : relations S1 S2.λs,s'.
    9  ∀s1,s1'. as_syntactical_succ S1 s1 s → Crel … rel s1 s1' → as_syntactical_succ S2 s1' s'.
    10 
    11 record simulation_conditions (S1,S2 : abstract_status) (rel : relations S1 S2) : Prop ≝
     8definition 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
     11record simulation_conditions (S : abstract_status) (rel : relations S) : Prop ≝
    1212 { 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))
    1414 ; 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))
    1616 ; simulate_tau:
    17      ∀s1:S1.∀s2:S2.∀s1':S1.
     17     ∀s1,s2,s1' : S.
    1818      as_execute … (cost_act (None ?))  s1 s1'→
    1919      Srel … rel s1 s2 → as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io →
    20       ∃s2'. ∃t: raw_trace S2 s2 s2'.
     20      ∃s2'. ∃t: raw_trace S s2 s2'.
    2121        Srel … rel s1' s2' ∧ silent_trace … t
    2222 ; simulate_label:
    23      ∀s1:S1.∀s2:S2.∀l.∀s1':S1.
    24       as_execute S1 (cost_act (Some ? l)) s1 s1' →
     23     ∀s1,s2,l,s1'.
     24      as_execute S (cost_act (Some ? l)) s1 s1' →
    2525      as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io →
    2626      Srel … rel s1 s2 →
    2727      ∃s2',s2'',s2'''.
    28        ∃t1: raw_trace S2 s2 s2'.
     28       ∃t1: raw_trace S s2 s2'.
    2929       as_execute … (cost_act (Some ? l)) s2' s2'' ∧
    30        ∃t3: raw_trace … s2'' s2'''.
     30       ∃t3: raw_trace S s2'' s2'''.
    3131        Srel … rel  s1' s2''' ∧ silent_trace … t1 ∧ pre_silent_trace … t3
    3232 ; simulate_call_pl:
    33      ∀s1:S1.∀s2:S2.∀s1':S1.∀f,l.
     33     ∀s1,s2,s1' : S.∀f,l.
    3434      is_call_post_label … s1 →
    3535      as_execute … (call_act f l) s1 s1' →
    … …  
    3737      Srel … rel s1 s2 →
    3838      ∃s2',s2'',s2'''.
    39        ∃t1: raw_trace S2 s2 s2'.
     39       ∃t1: raw_trace S s2 s2'.
    4040       as_execute … (call_act f l) s2' s2'' ∧
    4141       bool_to_Prop(is_call_post_label … s2') ∧
    42        ∃t3: raw_trace S2 s2'' s2'''.
     42       ∃t3: raw_trace S s2'' s2'''.
    4343        Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ pre_silent_trace … t3
    4444 ; simulate_ret_l:
    45      ∀s1:S1.∀s2:S2.∀s1':S1.∀l.
    46       as_execute S1 (ret_act (Some ? l)) s1 s1' →
     45     ∀s1,s2,s1' : S.∀l.
     46      as_execute S (ret_act (Some ? l)) s1 s1' →
    4747      as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io →
    4848      Srel  … rel s1 s2 →
    4949      ∃s2',s2'',s2'''.
    50        ∃t1: raw_trace S2 s2 s2'.
     50       ∃t1: raw_trace S s2 s2'.
    5151       as_execute … (ret_act (Some ? l)) s2' s2'' ∧
    52        ∃t3: raw_trace S2 s2'' s2'''.
     52       ∃t3: raw_trace S s2'' s2'''.
    5353        Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ pre_silent_trace … t3
    5454 ; simulate_call_n:
    55      ∀s1:S1.∀s2:S2.∀s1':S1.∀f,l.
     55     ∀s1,s2,s1' : S.∀f,l.
    5656      as_execute … (call_act f l) s1 s1' →
    5757      ¬ is_call_post_label … s1 →
    … …  
    5959      Srel … rel s1 s2 →
    6060      ∃s2',s2'',s2'''.
    61        ∃t1: raw_trace S2 s2 s2'.
     61       ∃t1: raw_trace S s2 s2'.
    6262       bool_to_Prop (¬ is_call_post_label … s2') ∧
    6363       as_execute … (call_act f l) s2' s2'' ∧
    64        ∃t3: raw_trace S2 s2'' s2'''.
     64       ∃t3: raw_trace S s2'' s2'''.
    6565        Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ pre_silent_trace … t3
    6666        ∧ Crel … rel s1 s2'
    6767 ; simulate_ret_n:
    68      ∀s1:S1.∀s2:S2.∀s1':S1.
     68     ∀s1,s2,s1' : S.
    6969      as_execute … (ret_act (None ?)) s1 s1' →
    7070      as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io →
    7171      Srel … rel s1 s2 →
    72       ∃s2',s2'',s2''': S2.
    73        ∃t1: raw_trace S2 s2 s2'.
     72      ∃s2',s2'',s2'''.
     73       ∃t1: raw_trace S s2 s2'.
    7474       as_execute … (ret_act (None ?)) s2' s2''  ∧
    75        ∃t3: raw_trace S2 s2'' s2'''.
     75       ∃t3: raw_trace S s2'' s2'''.
    7676        Srel … rel s1' s2''' ∧ pre_silent_trace … t1 ∧ pre_silent_trace … t3
    7777        ∧ Rrel … rel s1' s2''
    7878 ; simulate_io_in :
    79    ∀s1:S1.∀s2:S2.∀s1':S1.∀l.
     79   ∀s1,s2,s1' : S.∀l.
    8080   as_execute … (cost_act … (Some ? l)) s1 s1' →
    8181   as_classify … s1 ≠ cl_io → as_classify … s1' = cl_io →
    8282   Srel … rel s1 s2 →
    83    ∃s2',s2''.∃t: raw_trace … s2 s2'.
     83   ∃s2',s2'' : S.∃t: raw_trace … s2 s2'.
    8484   pre_silent_trace … t ∧ as_execute … (cost_act … (Some ? l)) s2' s2'' ∧
    8585   as_classify … s2'' = cl_io ∧ Srel … rel s1' s2''
    8686; simulate_io_out :
    87    ∀s1:S1.∀s2:S2.∀s1':S1.∀l.
     87  ∀s1,s2,s1' : S.∀l.
    8888   as_execute … (cost_act … (Some ? l)) s1 s1' →
    8989   as_classify … s1 = cl_io → as_classify … s1' ≠ cl_io →
    9090   Srel … rel s1 s2 →
    91    ∃s2',s2''.∃t : raw_trace … s2' s2''.
     91   ∃s2',s2'' : S.∃t : raw_trace … s2' s2''.
    9292   pre_silent_trace … t ∧ as_execute … (cost_act … (Some ? l)) s2 s2' ∧
    9393   as_classify … s2 = cl_io ∧ Srel … rel s1' s2''
    … …  
    261261qed.
    262262
     263
    263264theorem simulates_pre_mesurable:
    264  ∀S1,S2 : abstract_status.∀rel : relations S1 S2.
    265  ∀s1,s1' : S1. ∀t1: raw_trace S1 s1 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 →
    267268  pre_measurable_trace … t1 →
    268   ∀s2 : S2.
     269  ∀s2 : S.
    269270 as_classify … s2 ≠ cl_io →   Srel … rel s1 s2 →
    270271  ∃s2'. ∃t2: raw_trace … s2 s2'.
    … …  
    272273    get_costlabels_of_trace … t1 = get_costlabels_of_trace … t2 ∧
    273274    Srel … rel s1' s2'.
    274 #S1 #S2 #rel #s1 #s1' #t1 #good #pre_measurable elim pre_measurable
     275#S #rel #s1 #s1' #t1 #good #pre_measurable elim pre_measurable
    275276[ #st #H1 #s2 #REL #Hs2 %{s2} %{(t_base …)}
    276277  /8 by refl, silent_empty, conj, pre_silent_is_premeasurable/
    … …  
    401402
    402403record 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
    407405 ; R_s2: S
    408  ; R_post_state : option S
    409406 ; trace : raw_trace S L_s1 R_s2
    410407 ; 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 }.
    423409
    424410lemma cl_io_case : ∀P : status_class → Prop. P cl_io → (∀x.x≠cl_io → P x) → ∀s.P s.
    … …  
    450436qed.
    451437
    452 lemma instr_execute_commute : ∀S1,S2 :abstract_status.
    453 ∀rel : relations S1 S2.
     438lemma instr_execute_commute : ∀S :abstract_status.
     439∀rel : relations S.
    454440simulation_conditions … rel →
    455 ∀s1,s1': S1.∀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' →
    456442(as_classify … s1 ≠ cl_io ∨ as_classify … s1' ≠ cl_io) →
    457443∀s2.
    458444Srel … rel s1 s2 →
    459 ∃s2' : S2.∃tr : raw_trace … s2 s2'.silent_trace … tr ∧
    460 ∃s2'' : S2.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''' ∧
    462448(is_call_act l → is_call_post_label … s1 → is_call_post_label … s2') ∧
    463449(as_classify … s1' ≠ cl_io → as_classify … s2'' ≠ cl_io).
    464 #S1 #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))
    465451[ #EQs1_io cases(io_exiting … EQs1_io … prf) #lab #EQ destruct(EQ)
    466452  cases HIO [ >EQs1_io * #EQ @⊥ @EQ % ] #Hio_s1'
    … …  
    513499qed.
    514500
     501(*
    515502theorem simulate_LR_trace :
    516 ∀S1,S2 : abstract_status.
    517 ∀t : measurable_trace S1.
    518 ∀rel : relations S1 S2.
     503∀S : abstract_status.
     504∀t : measurable_trace S.
     505∀rel : relations S.
    519506simulation_conditions … rel →
    520 ∀s2 : S2.
     507∀s2 : S.
    521508match L_pre_state … t with
    522509[ None ⇒
    … …  
    524511   Srel … rel (L_s1 … t) s2 
    525512| Some s1 ⇒ Srel … rel s1 s2 ] →
    526 ∃t' : measurable_trace S2.
     513∃t' : measurable_trace S.
    527514 L_label … t = L_label … t' ∧ R_label … t = R_label … t' ∧
    528515 get_costlabels_of_trace … (trace … t) =
    … …  
    531518[ None ⇒ L_s1 … t' = s2
    532519| Some s1 ⇒
    533          ∃ pre_state : S2.
     520         ∃ pre_state : S.
    534521         L_pre_state … t' = Some ? pre_state ∧
    535          ∃tr_i : raw_trace … s2 pre_state. silent_trace … tr_i
     522         ∃tr_i : raw_trace S s2 pre_state. silent_trace … tr_i
    536523] ∧
    537524match R_post_state … t with         
    538525[ None ⇒ Srel … rel (R_s2 … t) (R_s2 … t')
    539526| Some s1' ⇒
    540           ∃s2' : S2. Srel … rel s1' s2' ∧
    541           ∃ post_state : S2.
     527          ∃s2' : S. Srel … rel s1' s2' ∧
     528          ∃ post_state : S.
    542529          R_post_state … t' = Some ? post_state ∧
    543           ∃tr : raw_trace … post_state s2'. silent_trace … tr
     530          ∃tr : raw_trace S post_state s2'. silent_trace … tr
    544531].
    545 #S1 #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 ]
    546533[2: #REL_pre
    547534    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 ∧
    551538       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 ∧
    554541       as_classify … final_state ≠ cl_io ∧
    555542       Srel … rel (L_s1 … t) final_state)
    … …  
    566553    * #final_state * #tr_i2 ** #silent_i2 #final_not_io #REL
    567554| #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 ?)
    569556      [ lapply(L_init_ok … t) >EQpre normalize nodelta * #H1 #H2 % [2: //]
    570557        @(initial_is_initial … good … H1) assumption ] * #initial_s2 #init_label
    … …  
    573560#fin_s2 * #t' ** #pre_meas_t' #EQcost #REL' inversion(R_post_state … t)
    574561[2,4: #post_s2] #EQpost normalize nodelta
    575 [3,4: cut (match R_label … t in option return λ_:(option ActionLabel).Prop with 
    576  [None⇒bool_to_Prop (as_final … fin_s2)∧None S2=None S2
     562[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
    577564 |Some (l:ActionLabel)⇒
    578565  (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')])
    581568  [1,3: lapply(R_fin_ok … t) cases(R_label … t) normalize nodelta
    582569      [1,3: * #H1 #H2 % [2,4: //] @(final_is_final … good … H1) assumption
    … …  
    588575          #a #_ %{a} % ] * #final_label #EQfinal_label
    589576     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.
    593580       as_execute … final_label middle_state post_state ∧
    594581       (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 ∧
    597584       Srel … rel post_s2 final_state)
    598585     [1,3: lapply(R_fin_ok … t) >EQfinal_label normalize nodelta ** #H1 #H2 * #sfin
    … …  
    846833    ]
    847834    *)
     835*)

  • LTS/Vm.ma

    r3485 r3486  
    1515{ seq_instr : Type[0]
    1616; 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] }.
    2218
    2319inductive AssemblerInstr (p : assembler_params) : Type[0] ≝
    … …  
    2925| Iret: AssemblerInstr p.
    3026
     27definition labels_pc_of_instr : ∀p.AssemblerInstr p → ℕ → list (CostLabel × ℕ) ≝
     28λp,i,program_counter.
     29match 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
     43let 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 × ℕ) ≝
     47match 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
     54include "basics/lists/listb.ma".
     55
     56(*doppione da mettere a posto*)
     57let rec no_duplicates (A : DeqSet) (l : list A) on l : Prop ≝
     58match l with
     59[ nil ⇒ True
     60| cons x xs ⇒ ¬ (bool_to_Prop (x ∈ xs)) ∧ no_duplicates … xs
     61].
     62
     63
    3164record AssemblerProgram (p : assembler_params) : Type[0] ≝
    3265{ instructions : list (AssemblerInstr p)
    3366; endmain : ℕ
    3467; 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))
    3573}.
     74
    3675
    3776definition fetch: ∀p.AssemblerProgram p → ℕ → option (AssemblerInstr p) ≝
    … …  
    137176           S (pc … st1) ::  asm_stack … st1 = asm_stack … st2 →
    138177           asm_is_io … st1 = asm_is_io … st2 →
    139            entry_of_function p f = pc … st2 →
     178           entry_of_function … prog f = pc … st2 →
    140179           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 p f) = return lbl →
     180           label_of_pc ? (call_label_fun … prog) (entry_of_function … prog f) = return lbl →
    142181           vmstep … (call_act f lbl) st1 st2
    143182| vm_ret :
    … …  
    149188           asm_is_io … st1 = asm_is_io … st2 →
    150189           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 →
    152191           op … (cost … st1) (cost_of p p' (Iret p) (asm_store … st1)) = cost … st2 →
    153192           vmstep … (ret_act (Some ? lbl)) st1 st2.
    … …  
    202241      None ?
    203242    else
    204       ! lbl ← label_of_pc ? (call_label_fun p) (entry_of_function p f);
     243      ! lbl ← label_of_pc ? (call_label_fun … prog) (entry_of_function … prog f);
    205244      return 〈call_act f lbl,
    206               mk_vm_state ?? (entry_of_function p f)
     245              mk_vm_state ?? (entry_of_function … prog f)
    207246                             ((S (pc … st)) :: (asm_stack … st))
    208247                             (asm_store … st) false
    … …  
    212251         else
    213252            ! 〈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;
    215254            return 〈ret_act (Some ? lbl),
    216255                    mk_vm_state ?? newpc tl (asm_store … st) false   
    … …  
    291330discriminator option.
    292331
     332inductive 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
    293337definition 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                    ])
    298357                (λ_.λ_.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
    301363                               [ Seq _ _ ⇒ cl_other
    302364                               | Ijmp _ ⇒ cl_other
    … …  
    306368                               | Iret ⇒ cl_other
    307369                               ]
    308                     | None ⇒ cl_other
     370                     | None ⇒ cl_other
     371                     ]
    309372                    ]
    310373                )
    311374                (λ_.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])
    314377                ???.
    315 @hide_prf
     378@hide_prf cases daemon qed. (*
    316379[ #s1 #s2 #l inversion(fetch ???) normalize nodelta
    317380  [ #_ #EQ destruct] * normalize nodelta
    … …  
    366429  normalize nodelta #H cases(bind_inversion ????? H) -H #x * #_
    367430  whd in ⊢ (??%% → ?); #EQ destruct % //
    368 qed.
     431qed.*)
    369432
    370433definition asm_concrete_trans_sys ≝
    371434λ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 …] ).
    373437
    374438definition emits_labels ≝
    … …  
    387451definition asm_static_analisys_data ≝ λp,p',prog,abs_t,instr_m.
    388452mk_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.
    390454
    391455definition non_empty_list : ∀A.list A → bool ≝
    … …  
    395459 (prog: AssemblerProgram p) (abs_t : monoid)
    396460 (instr_m : AssemblerInstr p → abs_t)
    397  (program_counter: ℕ)
     461 (prog_c: option ℕ)
    398462    (program_size: ℕ)
    399463        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   ].
     464match 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].
    413481
    414482
    … …  
    422490}.
    423491
    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
     494lemma labels_pc_ok : ∀p,prog,l1,l2,i_act,i,lbl,pc,m.
    450495nth_opt ? pc prog = return i →
    451496mem ? lbl (labels_pc_of_instr … i (m+pc)) →
    452 mem ? lbl (labels_pc p prog m).
    453 #p #instrs #i #lbl #pc
     497mem ? lbl (labels_pc p prog l1 l2 i_act m).
     498#p #instrs #l1 #l2 #iact #i #lbl #pc
    454499whd in match fetch; normalize nodelta lapply pc -pc
    455500elim instrs
    456501[ #pc #m whd in ⊢ (??%% → ?); #EQ destruct]
    457 #x #xs #IH * [|#pc'] #m whd in ⊢ (??%% → ?);
     502#x #xs #IH * [|#pc'] #m  whd in ⊢ (??%% → ?);
    458503[ #EQ destruct #lbl_addr whd in match (labels_pc ???);
    459504  /2 by mem_append_l1/
    … …  
    462507qed.
    463508
    464 lemma labels_pc_return: ∀p,prog,x1,x2.
    465  label_of_pc ReturnPostCostLabel (return_label_fun p) x1=return x2 →
     509lemma labels_pc_return: ∀p,prog,l1,l2,iact,x1,x2.
     510 label_of_pc ReturnPostCostLabel l2 x1=return x2 →
    466511 ∀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 l
     512   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
    469514[ #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]
    471516  * #x #y #tl #IH whd in ⊢ (??%? → %); normalize nodelta @eqb_elim
    472517  normalize nodelta
    … …  
    476521qed.
    477522
    478 lemma labels_pc_call: ∀p,prog,x1,x2.
    479  label_of_pc CallCostLabel (call_label_fun p) x1=return x2 →
     523lemma labels_pc_call: ∀p,prog,l1,l2,iact,x1,x2.
     524 label_of_pc CallCostLabel l1 x1=return x2 →
    480525 ∀m.
    481    mem … 〈(a_call x2),x1〉 (labels_pc p prog m).
    482  #p #l whd in match (labels_pc ???); #x1 #x2 #H elim l
     526   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
    483528[ #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]
    485530  * #x #y #tl #IH whd in ⊢ (??%? → %); normalize nodelta @eqb_elim
    486531  normalize nodelta
    … …  
    520565λp,abs_t,instr_m,mT,prog.
    521566let 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)
     567m_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)
    524570      (empty_map ?? mT).
    525571     
    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 with
    532 [ nil ⇒ True
    533 | cons x xs ⇒ ¬ (bool_to_Prop (x ∈ xs)) ∧ no_duplicates … xs
    534 ].
    535 
    536 definition asm_no_duplicates ≝
    537 λp,prog.no_duplicates … (map ?? \fst … (labels_pc … (instructions p prog) O)).
    538572
    539573(*falso: necessita di no_duplicates*)
    … …  
    577611
    578612lemma static_analisys_ok : ∀p,abs_t,instr_m,mT,prog,lbl,pc,map.
    579 asm_no_duplicates p prog →
    580613static_analisys p abs_t instr_m mT prog = return map →
    581 mem … 〈lbl,pc〉 (labels_pc … (instructions … prog) O) →
     614mem … 〈lbl,pc〉 (labels_pc … (instructions … prog) (call_label_fun … prog)
     615                   (return_label_fun … prog) (in_act … prog) O) →
    582616get_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 ?.
     617block_cost … prog abs_t instr_m (Some ? pc) (S (|(instructions … prog)|)) ∧
     618block_cost … prog abs_t instr_m (Some ? pc) (S (|(instructions … prog)|)) ≠ None ?.
    585619#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
     622lapply (labels_pc ??????) #l elim l [ #x #y #z #w #h * ]
     623* #hd1 #hd2 #tl #IH * #H1 #H2 #lbl #pc #map #H
    589624cases(bind_inversion ????? H) -H #map1 * #EQmap1 normalize nodelta #H
    590625cases(bind_inversion ????? H) -H #elem * #EQelem whd in ⊢ (??%% → ?); #EQ
    … …  
    602637include "Simulation.ma".
    603638
    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  }.
     639definition 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))).
    614644
    615645definition big_op: ∀M: monoid. list M → M ≝
    … …  
    643673
    644674lemma monotonicity_of_block_cost : ∀p,prog,abs_t,instr_m,pc,size,k.
    645 block_cost p prog abs_t instr_m pc size = return k →
     675block_cost p prog abs_t instr_m (Some ? pc) size = return k →
    646676∀size'.size ≤ size' →
    647 block_cost p prog abs_t instr_m pc size' = return k.
     677block_cost p prog abs_t instr_m (Some ? pc) size' = return k.
    648678#p #prog #abs_t #instr_m #pc #size lapply pc elim size
    649679[ #pc #k whd in ⊢ (??%% → ?); #EQ destruct]
    … …  
    678708   match x with [None⇒[]|Some c⇒[a_non_functional_label c]]
    679709] = [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)).
    681711#p #p' #prog #st1 #st2 #l #i #EQi whd in match eval_vmstate; normalize nodelta
    682712>EQi >m_return_bind normalize nodelta cases i in EQi; -i normalize nodelta
    … …  
    733763
    734764lemma 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.
    736766∀lbl.
    737767mem … lbl (get_costlabels_of_trace … t) →
    738 mem … (lbl) (map ?? \fst … (labels_pc … (instructions p prog) O)).
     768mem … (lbl) (map ?? \fst … (labels_pc … (instructions p prog) (call_label_fun … prog) (return_label_fun … prog) (in_act … prog) O)).
     769cases daemon (*
    739770#p #p' #prog #st1 #st2 #t elim t
    740771[ #st #lbl *
    … …  
    749780    *
    750781  ]
    751 ] 
     782]  *)
    752783qed.
    753784
    … …  
    774805qed.
    775806
    776 
    777 lemma static_dynamic : ∀p,p',prog.∀no_dup : asm_no_duplicates p prog.
     807definition 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
     815lemma static_dynamic : ∀p,p',prog.
    778816∀abs_t : abstract_transition_sys (m … p').∀instr_m.
    779817∀good : static_galois … (asm_static_analisys_data p p' prog abs_t instr_m).∀mT,map1.
    780818∀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'.
    783820∀t : raw_trace (asm_operational_semantics p p' prog) … st1 st2.
     821terminated_trace … t →
    784822∀k.
    785823pre_measurable_trace … t →
    786 block_cost p prog … instr_m (pc … st1) (S (|(instructions … prog)|)) = return k →
     824block_cost p prog … instr_m (get_pc … st1 (endmain … prog)) (S (|(instructions … prog)|)) = return k →
    787825∀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.
     827labels = dependent_map CostLabel ? (get_costlabels_of_trace …  t) (λlbl,prf.(opt_safe … (get_map … map1 lbl) ?)) →
     828rel_galois … good st2 (act_abs … abs_t (big_op … labels) (act_abs … abs_t k a1)).
    792829[2: @hide_prf
    793830    cases(mem_map ????? (labels_of_trace_are_in_code … prf)) *
    794831    #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; ]
    801837  #EQr_post #k #_ lapply(R_fin_ok … ter) >EQr_post normalize nodelta
    802838  [ whd in ⊢ (?% → ?); #final_st whd in ⊢ (??%? → ?); >final_st
Note: See TracChangeset for help on using the changeset viewer.