Changeset 3457


Ignore:
Timestamp:
Feb 20, 2014, 7:14:53 PM (5 years ago)
Author:
piccolo
Message:
 
File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Vm.ma

    r3449 r3457  
    1 include "Traces.ma".
     1include "costs.ma".
    22include "basics/lists/list.ma".
    33include "../src/utilities/option.ma".
     
    1111%{a} %{(refl …)} //
    1212qed.
    13 
    14 record monoid: Type[1] ≝
    15  { carrier :> Type[0]
    16  ; op: carrier → carrier → carrier
    17  ; e: carrier
    18  ; neutral: ∀x. op … x e = x
    19  ; is_associative: ∀x,y,z. op … (op … x y) z = op … x (op … y z)
    20  }.
    2113
    2214record assembler_params : Type[1] ≝
     
    345337qed.
    346338
     339definition asm_concrete_trans_sys ≝
     340λp,p',prog.mk_concrete_transition_sys …
     341             (asm_operational_semantics p p' prog) (m … p') (cost …).
     342
    347343definition emits_labels ≝
    348344λp.λinstr : AssemblerInstr p.match instr with
     
    355351        ].
    356352
    357 
    358 let rec block_cost (p : assembler_params) (p' : sem_params p)
    359  (prog: AssemblerProgram p) (program_counter: ℕ)
     353definition fetch_state : ∀p,p'.AssemblerProgram p → vm_state p p' → option (AssemblerInstr p) ≝
     354λp,p',prog,st.fetch … prog (pc … st).
     355
     356definition asm_static_analisys_data ≝ λp,p',prog,abs_t,instr_m.
     357mk_static_analysis_data (asm_concrete_trans_sys p p' prog) abs_t
     358 … (fetch_state p p' prog) instr_m.
     359
     360
     361let rec block_cost (p : assembler_params)
     362 (prog: AssemblerProgram p) (abs_t : monoid)
     363 (instr_m : AssemblerInstr p → abs_t)
     364 (program_counter: ℕ)
    360365    (program_size: ℕ)
    361         on program_size: option (m … p')
     366        on program_size: option abs_t
    362367match program_size with
    363368  [ O ⇒ None ?
    364369  | S program_size' ⇒
    365370    if eqb program_counter (\snd prog) then
    366        return e … (m … p')
     371       return e … abs_t
    367372    else
    368373    ! instr ← fetch … prog program_counter;
    369374    ! n ← (match emits_labels … instr with
    370           [ Some f ⇒ block_cost … prog (f program_counter) program_size'
     375          [ Some f ⇒ block_cost … prog abs_t instr_m (f program_counter) program_size'
    371376          | None ⇒ return e …
    372377          ]);
    373     return (op … (m … p') (cost_of p p' instr) n)
     378    return (op … abs_t (instr_m … instr) n)
    374379  ].
    375380 
     
    405410].
    406411
    407 definition static_analisys : ∀p : assembler_params.∀ p' : sem_params p.
    408 ∀mT : cost_map_T DEQCostLabel (m … p').AssemblerProgram p → option mT ≝
    409 λp,p',mT,prog.
     412definition static_analisys : ∀p : assembler_params.∀abs_t : monoid.(AssemblerInstr p → abs_t) →
     413∀mT : cost_map_T DEQCostLabel abs_t.AssemblerProgram p → option mT ≝
     414λp,abs_t,instr_m,mT,prog.
    410415let 〈instrs,final〉 ≝ prog in
    411416let prog_size ≝ S (|instrs|) in
    412 m_fold Option ?? (λx,m.let 〈z,w〉≝ x in ! k ← block_cost … prog w prog_size; 
     417m_fold Option ?? (λx,m.let 〈z,w〉≝ x in ! k ← block_cost p prog abs_t instr_m w prog_size; 
    413418                               return set_map … m z k) (labels_pc … instrs O)
    414419      (empty_map ?? mT).
    415420
    416421(*falso: necessita di no_duplicates*)
    417 axiom static_analisys_ok : ∀p,p',mT,prog,lbl,pc,map.
    418 static_analisys p p' mT prog = return map →
     422axiom static_analisys_ok : ∀p,abs_t,instr_m,mT,prog,lbl,pc,map.
     423static_analisys p abs_t instr_m mT prog = return map →
    419424mem … 〈lbl,pc〉 (labels_pc … (\fst prog) O) →
    420 get_map … map lbl = block_cost … prog pc (S (|(\fst prog)|)). 
     425get_map … map lbl = block_cost … prog abs_t instr_m pc (S (|(\fst prog)|)). 
    421426
    422427include "Simulation.ma".
    423428
    424 record terminated_trace (S : abstract_status) (L_s1,R_s2) (trace: raw_trace S L_s1 R_s2)
    425  : Prop ≝
    426  { R_label : option ActionLabel
    427  ; R_post_state : option S
    428  ; R_fin_ok : match R_label with
    429                [ None ⇒ bool_to_Prop (as_final … R_s2) ∧ R_post_state = None ?
    430                | Some l ⇒ (is_costlabelled_act l ∨ is_unlabelled_ret_act l) ∧
     429record terminated_trace (S : abstract_status) (R_s2 : S) : Type[0] ≝
     430{  R_post_step : option (ActionLabel × S)
     431 ; R_fin_ok : match R_post_step with
     432               [ None ⇒ bool_to_Prop (as_final … R_s2)
     433               | Some x ⇒ let 〈l,R_post_state〉≝ x in
     434                          (is_costlabelled_act l ∨ is_labelled_ret_act l) ∧
    431435                          (is_call_act l → bool_to_Prop (is_call_post_label … R_s2)) ∧
    432                           ∃ s'.R_post_state = Some ? s' ∧ as_execute … l R_s2 s'
     436                          as_execute … l R_s2 R_post_state
    433437               ]
    434438 }.
    435439 
    436 lemma static_dynamic : ∀p,p',prog,k,mT,map.
    437 static_analisys p p' mT prog = return map →
    438 ∀st1,st2 : vm_state p p'.∀t : raw_trace (asm_operational_semantics p p' prog) … st1 st2.
    439 pre_measurable_trace … t → terminated_trace … t →
    440 block_cost … prog (pc … st1) (S (|(\fst prog)|)) = return k →
    441 op … (m … p') (cost … st1)
    442  (foldr ?? (λlbl,k1.op … (opt_safe … (get_map … map lbl) ?) k1)
    443      k (get_costlabels_of_trace … t)) = cost … st2.
    444 [2: cases daemon]
    445 #p #p' #prog #k #mT #map #EQmap #st1 #st2 #t elim t
    446 [ #st #_ ** [|#r_lab] normalize nodelta #opt_r_state
    447   [ * whd in ⊢ (?% → ?); #final_st #_ whd in ⊢ (??%? → ?); >final_st
     440axiom vm_step_to_eval : ∀p,p',prog,st1,st2,l.vmstep … prog l st1 st2 →
     441eval_vmstate p p' prog st1 = return 〈l,st2〉.
     442
     443coercion vm_step_to_eval.
     444
     445definition big_op: ∀M: monoid. list M → M ≝
     446 λM. foldl … (op … M) (e … M).
     447
     448lemma big_op_associative:
     449 ∀M:monoid. ∀l1,l2.
     450  big_op M (l1@l2) = op M (big_op … l1) (big_op … l2).
     451 #M #l1 whd in match big_op; normalize nodelta
     452 generalize in match (e M) in ⊢ (? → (??%(??%?))); elim l1
     453 [ #c #l2 whd in match (append ???); normalize lapply(neutral_r … c)
     454   generalize in match c in ⊢ (??%? → ???%); lapply c -c lapply(e M)
     455   elim l2 normalize
     456   [ #c #c1 #c2 #EQ @sym_eq //
     457   | #x #xs #IH #c1 #c2 #c3 #EQ <EQ <IH [% | <is_associative % |]
     458   ]
     459 | #x #xs #IH #c #l2 @IH
     460 ]
     461qed.
     462
     463lemma act_big_op : ∀M,B. ∀act : monoid_action M B.
     464 ∀l1,l2,x.
     465   act (big_op M (l1@l2)) x = act (big_op … l2) (act (big_op … l1) x).
     466 #M #B #act #l1 elim l1
     467 [ #l2 #x >act_neutral //
     468 | #hd #tl #IH #l2 #x change with ([?]@(tl@l2)) in match ([?]@(tl@l2));
     469   >big_op_associative >act_op >IH change with ([hd]@tl) in match ([hd]@tl);
     470   >big_op_associative >act_op in ⊢ (???%); %
     471 ]
     472qed.
     473
     474lemma static_dynamic : ∀p,p',prog.
     475∀abs_t : abstract_transition_sys (m … p').∀instr_m.
     476∀good : static_galois … (asm_static_analisys_data p p' prog abs_t instr_m).∀mT,map1.
     477static_analisys p ? instr_m mT prog = return map1 →
     478∀st1,st2 : vm_state p p'.
     479∀ter : terminated_trace (asm_operational_semantics p p' prog) st2.
     480∀t : raw_trace (asm_operational_semantics p p' prog) … st1 st2.
     481∀k.
     482pre_measurable_trace … t →
     483block_cost p prog … instr_m (pc … st1) (S (|(\fst prog)|)) = return k →
     484∀a1.rel_galois … good st1 a1 →
     485let stop_state ≝ match R_post_step … ter with [None ⇒ st2 | Some x ⇒ \snd x ] in
     486∀costs.
     487costs = map … (λlbl.(opt_safe … (get_map … map1 lbl) ?)) (get_costlabels_of_trace …  t) →
     488rel_galois … good stop_state (act_abs … abs_t (big_op … costs) (act_abs … abs_t k a1)).
     489[2: @hide_prf cases daemon]
     490#p #p' #prog #abs_t #instr_m #good #mT #map1 #EQmap #st1 #st2 #ter #t
     491lapply ter -ter elim t
     492[ #st #ter inversion(R_post_step … ter) normalize nodelta [| * #lbl #st3 ]
     493  #EQr_post #k #_ lapply(R_fin_ok … ter) >EQr_post normalize nodelta
     494  [ whd in ⊢ (?% → ?); #final_st whd in ⊢ (??%? → ?); >final_st
    448495    normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ)
    449     >neutral %
    450   | ** #H1 #H2 * #post_st * #EQ destruct * #H3 #H4 whd in ⊢ (??%? → ?);
    451     >H3 normalize nodelta #H cases(bind_inversion ????? H) -H
    452     #i * #EQi #H cases(bind_inversion ????? H) -H #el
     496    #a1 #rel_st_a1 whd in match (map ????); #costs #EQ >EQ >act_neutral >act_neutral assumption
     497  | ** #H1 #H2 * #H3 #H4 whd in ⊢ (??%% → ?); >H3 normalize nodelta
     498    #H cases(bind_inversion ????? H) -H *
     499    [ #seq * [|#lbl1]
     500    | #newpc
     501    | #cond #newpc #ltrue #lfalse
     502    | #lin #io #lout
     503    | #f
     504    |
     505    ]
     506    * #EQfetch lapply(vm_step_to_eval … H4) whd in match eval_vmstate;
     507    normalize nodelta >EQfetch >m_return_bind normalize nodelta
     508    cases(asm_is_io ??) normalize nodelta
     509    [1,3,5,7,11,13: whd in ⊢ (??%% → ?); #EQ destruct
     510    |2,4,8,9,12,14: #H cases(bind_inversion ????? H) -H #x * #_
     511      [3: cases x normalize nodelta
     512      |6: #H cases(bind_inversion ????? H) -H #y * #_
     513      ]
     514    ]
     515    whd in ⊢ (??%% → ?); #EQ destruct
     516    [4,8: cases H1 [1,3: * |*: * #y #EQ destruct]]
     517    >m_return_bind whd in ⊢ (??%% → ?); #EQ destruct
     518    #a1 #good_st_a1 whd in match (map ????); #costs #EQ >EQ >neutral_r
     519    >act_neutral
     520    @(instr_map_ok … good … EQfetch … good_st_a1) /2/
     521  ]
     522| -st1 -st2 #st1 #st2 #st3 #l * #H3 #H4 #tl #IH #ter #k #H
     523  #H2 #a1 #good_a1 whd in match (get_costlabels_of_trace ????);
     524  whd #costs <map_append #EQ destruct >big_op_associative >act_op @IH
     525  [   
     526  inversion H in ⊢ ?;
     527  [ #st #c #EQ1 #EQ2 #EQ3 #EQ4 destruct
     528  | #s1 #s2 #s3 #lbl #exe #tl1 #s1_noio * #opt_l #EQ destruct #pre_tl1 #_
     529    #EQ1 #EQ2 #EQ3 #EQ4 destruct
     530  | #s1 #s2 #s3 #lbl #s1_noio #exe #tl1 * #lbl1 #EQ destruct #pre_tl1 #_
     531    #EQ1 #EQ2 #EQ3 #EQ4 destruct
     532  | #s1 #s2 #s3 #lbl #exe #tl1 #s1_noio * #f * #lbl1 #EQ destruct
     533    * #pre_tl1 #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct
     534  | #s1 #s2 #s3 #s4 #s5 #l1 #l2 #exe1 #t1 #t2 #exe2 #noio1 #noio2 #H *
     535  ] //
     536  | whd in H2 : (??%?); >H3 in H2; normalize nodelta #H
     537    cases(bind_inversion ????? H) #i * #EQi whd in match (emits_labels ??);
     538 
     539  inversion l [#fn #lbl | * [|#lbl] | * [|#lbl] ] #EQlbl normalize nodelta
     540  inversion (R_post_step ???) [|2,4,6,8,10,12,14,16: * #post_lbl #post_state]
     541  #EQR_post_step normalize nodelta lapply (IH ter) -IH
     542  >EQR_post_step normalize nodelta #IH
     543  whd in match (foldl ?????);
     544  [ >act_op @IH
     545  try (> act_op)
     546
     547
     548
     549
     550
     551
     552  whd in ⊢ (??%% → ?); [ >H1 in ⊢ (% → ?); | >H1 in ⊢ (% → ?); | >H1 in ⊢ (% → ?);]
     553  normalize nodelta lapply(vm_step_to_eval … H2) whd in match eval_vmstate;
     554  normalize nodelta #H cases(bind_inversion ????? H) -H * normalize nodelta
     555  [1,7,13: #seq * [2,4,6: #lbl1]
     556  |2,8,14: #newpc
     557  |3,9,15: #cond #newpc #ltrue #lfalse
     558  |4,10,16: #lin #io #lout
     559  |5,11,17: #f
     560  |*:
     561  ] * normalize nodelta #EQfetch
     562  [13,14,15: whd in s1_noio : (?(??%?)); >EQfetch in s1_noio;
     563    normalize nodelta cases(asm_is_io ???) normalize nodelta
     564    [1,3,5: * #H @⊥ @H % ] #_
     565  |*: cases(asm_is_io ???) normalize nodelta
     566     [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35:
     567        whd in ⊢ (??%% → ?); #EQ destruct]
     568  [13   
     569   
     570     #i * #EQi #H cases(bind_inversion ????? H) -H #el
    453571    inversion H4
    454572    [ #s1 #s2 #i1 * [| #lbl] #EQfetch #no_io #EQstore #EQstack #EQio #EQpc
Note: See TracChangeset for help on using the changeset viewer.