Changeset 3478 for LTS/Vm.ma


Ignore:
Timestamp:
Sep 22, 2014, 4:50:21 PM (5 years ago)
Author:
piccolo
Message:

fixed costlabels

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Vm.ma

    r3465 r3478  
    411411    return (op … abs_t (instr_m … instr) n)
    412412  ].
    413  
    414 inductive InitCostLabel : Type[0] ≝
    415   costlab : CostLabel → InitCostLabel
    416 | initial_act : InitCostLabel.
    417 
    418 definition eq_init_costlabel ≝ (λi1,i2.match i1 with
    419  [ initial_act ⇒ match i2 with [initial_act ⇒ true | _ ⇒ false ]
    420  | costlab c ⇒ match i2 with [costlab c1 ⇒ c == c1 | _ ⇒ false ]
    421  ]).
    422 
    423 definition DEQInitCostLabel ≝ mk_DeqSet InitCostLabel eq_init_costlabel ?.
    424 * [#c] * [1,3: #c1] whd in match eq_init_costlabel; normalize nodelta
    425 [4: /2/ | 2,3: % #EQ destruct] % [ #H >(\P H) % | #EQ destruct >(\b (refl …)) %]
    426 qed.
    427 
    428 coercion costlab.
    429 
    430 definition list_cost_to_list_initcost : list CostLabel → list InitCostLabel ≝
    431 map … costlab.
    432 
    433 coercion list_cost_to_list_initcost.
    434  
     413
     414
    435415record cost_map_T (dom : DeqSet) (codom : Type[0]) : Type[1] ≝
    436416{ map_type :> Type[0]
     
    442422}.
    443423
    444 definition labels_pc_of_instr : ∀p.AssemblerInstr p → ℕ → list (InitCostLabel × ℕ) ≝
     424definition labels_pc_of_instr : ∀p.AssemblerInstr p → ℕ → list (CostLabel × ℕ) ≝
    445425λp,i,program_counter.
    446426match i with
    447427  [ Seq _ opt_l ⇒ match opt_l with
    448                   [ Some lbl ⇒ [〈costlab (a_non_functional_label lbl),S program_counter〉]
     428                  [ Some lbl ⇒ [〈(a_non_functional_label lbl),S program_counter〉]
    449429                  | None ⇒ [ ]
    450430                  ]
    451431  | Ijmp _ ⇒ [ ]
    452   | CJump _ newpc ltrue lfalse ⇒ [〈costlab (a_non_functional_label ltrue),newpc〉;
    453                                   〈costlab (a_non_functional_label lfalse),S program_counter〉]
    454   | Iio lin _ lout ⇒ [〈costlab (a_non_functional_label lin),program_counter〉;
    455                       〈costlab (a_non_functional_label lout),S program_counter〉]
     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〉]
    456436  | Icall f ⇒ [ ]
    457437  | Iret ⇒ [ ]
     
    459439
    460440let rec labels_pc (p : assembler_params)
    461 (prog : list (AssemblerInstr p)) (program_counter : ℕ) on prog : list (InitCostLabel × ℕ) ≝
     441(prog : list (AssemblerInstr p)) (program_counter : ℕ) on prog : list (CostLabel × ℕ) ≝
    462442match prog with
    463 [ nil ⇒ [〈initial_act,O〉] @
    464         map … (λx.let〈y,z〉 ≝ x in 〈costlab (a_call z),y〉) (call_label_fun … p) @
    465         map … (λx.let〈y,z〉 ≝ x in 〈costlab (a_return_post z),y〉) (return_label_fun … p)
     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)
    466446| cons i is ⇒ (labels_pc_of_instr … i program_counter)@labels_pc p is (S program_counter)
    467447].
     
    485465 label_of_pc ReturnPostCostLabel (return_label_fun p) x1=return x2 →
    486466 ∀m.
    487    mem … 〈costlab (a_return_post x2),x1〉 (labels_pc p (instructions p prog) m).
     467   mem … 〈(a_return_post x2),x1〉 (labels_pc p (instructions p prog) m).
    488468 #p * #l #endmain #_ whd in match (labels_pc ???); #x1 #x2 #H elim l
    489469[ #m @mem_append_l2 @mem_append_l2 whd in H:(??%?);
     
    499479 label_of_pc CallCostLabel (call_label_fun p) x1=return x2 →
    500480 ∀m.
    501    mem … 〈costlab (a_call x2),x1〉 (labels_pc p (instructions p prog) m).
     481   mem … 〈(a_call x2),x1〉 (labels_pc p (instructions p prog) m).
    502482 #p * #l #endmain #_ whd in match (labels_pc ???); #x1 #x2 #H elim l
    503483[ #m @mem_append_l2 @mem_append_l1 whd in H:(??%?);
     
    530510*) 
    531511
    532 unification hint  0 ≔ ;
    533     X ≟ DEQInitCostLabel
    534 (* ---------------------------------------- *) ⊢
    535     InitCostLabel ≡ carr X.
    536 
    537 
    538 unification hint  0 ≔ p1,p2;
    539     X ≟ DEQInitCostLabel
    540 (* ---------------------------------------- *) ⊢
    541     eq_init_costlabel p1 p2 ≡ eqb X p1 p2.
    542    
    543 
    544512let rec m_foldr (M : Monad) (X,Y : Type[0]) (f : X→Y→M Y) (l : list X) (y : Y) on l : M Y ≝
    545513match l with
     
    549517
    550518definition static_analisys : ∀p : assembler_params.∀abs_t : monoid.(AssemblerInstr p → abs_t) →
    551 ∀mT : cost_map_T DEQInitCostLabel abs_t.AssemblerProgram p → option mT ≝
     519∀mT : cost_map_T DEQCostLabel abs_t.AssemblerProgram p → option mT ≝
    552520λp,abs_t,instr_m,mT,prog.
    553521let prog_size ≝ S (|instructions … prog|) in
     
    709677|cost_act x ⇒
    710678   match x with [None⇒[]|Some c⇒[a_non_functional_label c]]
    711 |init_act⇒[ ]
    712679] = [x] ∧
    713  (mem … 〈costlab x,pc … st2〉 (labels_pc p (instructions … prog) O)).
     680 (mem … 〈x,pc … st2〉 (labels_pc p (instructions … prog) O)).
    714681#p #p' #prog #st1 #st2 #l #i #EQi whd in match eval_vmstate; normalize nodelta
    715682>EQi >m_return_bind normalize nodelta cases i in EQi; -i normalize nodelta
     
    744711|cost_act x ⇒
    745712   match x with [None⇒[]|Some c⇒[a_non_functional_label c]]
    746 |init_act⇒[ ]
    747713] = [ ] ∧ pc … st2 = f (pc … st1).
    748714#p #p' #prog #st1 #st2 #l #i #f #EQi whd in match eval_vmstate; normalize nodelta
     
    770736∀lbl.
    771737mem … lbl (get_costlabels_of_trace … t) →
    772 mem … (costlab lbl) (map ?? \fst … (labels_pc … (instructions p prog) O)).
     738mem … (lbl) (map ?? \fst … (labels_pc … (instructions p prog) O)).
    773739#p #p' #prog #st1 #st2 #t elim t
    774740[ #st #lbl *
     
    902868qed.
    903869
     870definition actionlabel_to_costlabel : ActionLabel → list CostLabel ≝
     871λa.match a with
     872[ call_act f l ⇒ [a_call l]
     873| ret_act opt_l ⇒ match opt_l with [None ⇒ [ ] | Some l ⇒ [a_return_post l]]
     874| cost_act opt_l ⇒ match opt_l with [None ⇒ [ ] | Some l ⇒ [a_non_functional_label l]]
     875].
     876
     877definition get_costlabels_of_measurable_trace : ∀S : abstract_status.measurable_trace S → list CostLabel ≝
     878λS,t.
     879 match L_label … t with
     880 [ None ⇒ [i_act]
     881 | Some l ⇒ actionlabel_to_costlabel l
     882 ] @
     883 get_costlabels_of_trace … (trace … t).
     884
    904885(*get_costlabels_of_measurable_trace deve aggiungere la label iniziale.*)
    905 theorem static_dynamic : ∀p,p',prog.∀no_dup : asm_no_duplicates p prog.
     886theorem static_dynamic_meas : ∀p,p',prog.∀no_dup : asm_no_duplicates p prog.
    906887∀abs_t : abstract_transition_sys (m … p').∀instr_m.
    907888∀good : static_galois … (asm_static_analisys_data p p' prog abs_t instr_m).∀mT,map1.
    908889∀EQmap : static_analisys p ? instr_m mT prog = return map1.
    909890∀t : measurable_trace (asm_operational_semantics p p' prog).
    910 ∀a1.rel_galois … good st1 (L_s1 … t)
     891∀a1.rel_galois … good (L_s1 … t) a1
    911892let stop_state ≝ match R_post_state … t with [None ⇒ R_s2 … t | Some x ⇒ x ] in
    912 ∀costs.
    913 costs = dependent_map CostLabel ? (get_costlabels_of_measurable_trace …  t) (λlbl,prf.(opt_safe … (get_map … map1 lbl) ?)) →
    914 rel_galois … good stop_state (act_abs … abs_t (big_op … costs) a1).
    915 
    916 
    917 
     893∀abs_trace.
     894abs_trace = dependent_map CostLabel ? (get_costlabels_of_measurable_trace …  t) (λlbl,prf.(opt_safe … (get_map … map1 lbl) ?)) →
     895rel_galois … good stop_state (act_abs … abs_t (big_op … abs_trace) a1).
     896[2: @hide_prf
     897    whd in match get_costlabels_of_measurable_trace in prf; normalize nodelta in prf;
     898    cases(mem_append ???? prf) -prf
     899    [2: #prf cases(mem_map ????? (labels_of_trace_are_in_code … prf)) *
     900        #lbl' #pc * #Hmem #EQ destruct   
     901        >(proj1 … (static_analisys_ok … no_dup … EQmap … Hmem))
     902        @(proj2 … (static_analisys_ok … no_dup … EQmap … Hmem))
     903    | inversion(L_label … t) normalize nodelta [| #lbl'] #EQleft
     904      [ * [2: *] #EQ destruct cases daemon (* i_act sta sempre nel codice *)
     905      | (* per inversione su as_execute *) cases daemon
     906      ]
     907    ]
     908]
     909#p #p' #prog #no_dup #abs_t #instr_m #good #mT #map1 #EQmap1 #t #a1 #rel_galois #abs_trace #EQabs_trace
     910xxxxxx
     911lapply(static_dynamic … (trace …t) … abs_trace) try //
     912
     913
Note: See TracChangeset for help on using the changeset viewer.