Changeset 3463


Ignore:
Timestamp:
Feb 21, 2014, 6:15:38 PM (6 years ago)
Author:
piccolo
Message:
 
File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Vm.ma

    r3457 r3463  
    2929| Iret: AssemblerInstr p.
    3030
    31 definition AssemblerProgram ≝λp.list (AssemblerInstr p) × ℕ.
     31record AssemblerProgram (p : assembler_params) : Type[0] ≝
     32{ instructions : list (AssemblerInstr p)
     33; endmain : ℕ
     34; endmain_ok : endmain ≤ |instructions|
     35}.
    3236
    3337definition fetch: ∀p.AssemblerProgram p → ℕ → option (AssemblerInstr p) ≝
    34  λp,l,n. nth_opt ? n (\fst l).
     38 λp,l,n. nth_opt ? n (instructions … l).
    3539
    3640definition stackT: Type[0] ≝ list (nat).
     
    4347; eval_asm_io : io_instr p → asm_store_type → option asm_store_type
    4448; cost_of_io : io_instr p → asm_store_type → m
    45 ; cost_of : AssemblerInstr p → m
     49; cost_of : AssemblerInstr p → asm_store_type →  m
    4650}.
    4751
     
    7377           asm_is_io … st1 = asm_is_io … st2 →
    7478           S (pc … st1) = pc … st2 →
    75            op … (cost … st1) (cost_of p p' (Seq p i l)) = cost … st2 →
     79           op … (cost … st1) (cost_of p p' (Seq p i l) (asm_store … st1)) = cost … st2 →
    7680           vmstep … (cost_act l) st1 st2
    7781| vm_ijump : ∀st1,st2 : vm_state p p'.∀new_pc : ℕ.
     
    8286           asm_is_io … st1 = asm_is_io … st2 →
    8387           new_pc = pc … st2 →
    84            op … (cost … st1) (cost_of p p' (Ijmp … new_pc)) = cost … st2 →
     88           op … (cost … st1) (cost_of p p' (Ijmp … new_pc) (asm_store … st1)) = cost … st2 →
    8589           vmstep … (cost_act (None ?)) st1 st2
    8690| vm_cjump_true :
     
    9397           asm_is_io … st1 = asm_is_io … st2 →
    9498           pc … st2 = new_pc →
    95            op … (cost … st1) (cost_of p p' (CJump p cond new_pc ltrue lfalse)) = cost … st2 →
     99           op … (cost … st1) (cost_of p p' (CJump p cond new_pc ltrue lfalse) (asm_store … st1)) = cost … st2 →
    96100           vmstep … (cost_act (Some ? ltrue)) st1 st2
    97101| vm_cjump_false :
     
    104108           asm_is_io … st1 = asm_is_io … st2 →
    105109           S (pc … st1) = pc … st2 →
    106            op … (cost … st1) (cost_of p p' (CJump … cond new_pc ltrue lfalse)) = cost … st2 →
     110           op … (cost … st1) (cost_of p p' (CJump … cond new_pc ltrue lfalse) (asm_store … st1)) = cost … st2 →
    107111           vmstep … (cost_act (Some ? lfalse)) st1 st2
    108112| vm_io_in : 
     
    134138           asm_is_io … st1 = asm_is_io … st2 →
    135139           entry_of_function p  f = pc … st2 →
    136            op … (cost … st1) (cost_of p p' (Icall p f)) = cost … st2 →
     140           op … (cost … st1) (cost_of p p' (Icall p f) (asm_store … st1)) = cost … st2 →
    137141           label_of_pc ? (call_label_fun p) (entry_of_function p f) = return lbl →
    138142           vmstep … (call_act f lbl) st1 st2
     
    146150           newpc = pc … st2 →
    147151           label_of_pc ? (return_label_fun p) newpc = return lbl →
    148            op … (cost … st1) (cost_of p p' (Iret p)) = cost … st2 →
     152           op … (cost … st1) (cost_of p p' (Iret p) (asm_store … st1)) = cost … st2 →
    149153           vmstep … (ret_act (Some ? lbl)) st1 st2.
    150154
     
    161165     return 〈cost_act opt_l,
    162166             mk_vm_state ?? (S (pc … st)) (asm_stack … st) new_store false
    163                 (op … (cost … st) (cost_of p p' (Seq p x opt_l)))〉
     167                (op … (cost … st) (cost_of p p' (Seq p x opt_l) (asm_store … st)))〉
    164168| Ijmp newpc ⇒
    165169   if asm_is_io … st then
     
    168172     return 〈cost_act (None ?),
    169173             mk_vm_state ?? newpc (asm_stack … st) (asm_store … st) false
    170                 (op … (cost … st) (cost_of p p' (Ijmp … newpc)))〉
     174                (op … (cost … st) (cost_of p p' (Ijmp … newpc) (asm_store … st)))〉
    171175| CJump cond newpc ltrue lfalse ⇒
    172176   if asm_is_io … st then
     
    177181       return 〈cost_act (Some ? ltrue),
    178182               mk_vm_state ?? newpc (asm_stack … st) (asm_store … st) false
    179                 (op … (cost … st) (cost_of p p' (CJump … cond newpc ltrue lfalse)))〉
     183                (op … (cost … st) (cost_of p p' (CJump … cond newpc ltrue lfalse) (asm_store … st)))〉
    180184     else
    181185       return 〈cost_act (Some ? lfalse),
    182186               mk_vm_state ?? (S (pc … st)) (asm_stack … st) (asm_store … st) false
    183                 (op … (cost … st) (cost_of p p' (CJump … cond newpc ltrue lfalse)))〉
     187                (op … (cost … st) (cost_of p p' (CJump … cond newpc ltrue lfalse) (asm_store … st)))〉
    184188| Iio lin io lout ⇒
    185189              if asm_is_io … st then
     
    203207                             ((S (pc … st)) :: (asm_stack … st))
    204208                             (asm_store … st) false
    205                              (op … (cost … st) (cost_of p p' (Icall p f)))〉
     209                             (op … (cost … st) (cost_of p p' (Icall p f) (asm_store … st)))〉
    206210| Iret ⇒ if asm_is_io … st then
    207211            None ?
     
    211215            return 〈ret_act (Some ? lbl),
    212216                    mk_vm_state ?? newpc tl (asm_store … st) false   
    213                      (op … (cost … st) (cost_of p p' (Iret p)))〉
     217                     (op … (cost … st) (cost_of p p' (Iret p) (asm_store … st)))〉
    214218].
    215219
     
    245249qed.
    246250
     251 
     252lemma vm_step_to_eval : ∀p,p',prog,st1,st2,l.vmstep … prog l st1 st2 →
     253eval_vmstate p p' prog st1 = return 〈l,st2〉.
     254#p #p' #prog * #pc1 #stack1 #store1 #io1 #cost1
     255* #pc2 #stack2 #store2 #io2 #cost2 #l #H inversion H
     256[ #s1 #s2 #i #opt_l #EQfetch #EQio #EQstore #EQstack #EQio1 #EQpc #EQcost
     257  #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in match eval_vmstate; normalize nodelta   
     258  >EQfetch >m_return_bind normalize nodelta >EQio normalize nodelta >EQstore
     259  >m_return_bind <EQio1 >EQio <EQpc >EQstack >EQcost %
     260| #s1 #s2 #newpc #EQfetch #EQio1 #EQstore #EQstack #EQio2 #EQnewpc #EQcost
     261  #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in match eval_vmstate; normalize nodelta
     262  >EQfetch >m_return_bind normalize nodelta >EQio1 normalize nodelta <EQio2 >EQio1
     263  >EQstore >EQstack <EQcost >EQstore %
     264|3,4: #s1 #s2 #cond #newoc #ltrue #lfalse #EQev_cond #EQfetch #EQio1 #EQstore
     265  #EQstack #EQio2 #EQnewoc #EQcost #EQ1 #EQ2 #EQ3 #EQ4 destruct
     266  whd in match eval_vmstate; normalize nodelta >EQfetch >m_return_bind
     267  normalize nodelta >EQio1 normalize nodelta >EQev_cond >m_return_bind
     268  normalize nodelta <EQio1 >EQio2 >EQstore >EQstack <EQcost >EQstore [%] >EQnewoc %
     269|5,6: #s1 #s2 #lin #io #lout #EQfetch #EQio1 #EQstore #EQstack #EQio2 #EQpc
     270   #EQcost #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in match eval_vmstate;
     271   normalize nodelta >EQfetch >m_return_bind normalize nodelta >EQio1
     272   normalize nodelta >EQstack <EQpc >EQcost [ >EQstore <EQio2 %]
     273   >EQstore >m_return_bind <EQpc <EQio2 %
     274| #s1 #s2 #f #lbl #EQfetch #EQio1 #EQstore #EQstack #EQio2 #EQentry
     275  #EQcost #EQlab_pc #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in match eval_vmstate;
     276  normalize nodelta >EQfetch >m_return_bind normalize nodelta >EQio1
     277  normalize nodelta >EQlab_pc >m_return_bind >EQentry >EQcost <EQio2 >EQio1
     278  <EQstack >EQstore %
     279| #s1 #s2 #newpc #lbl #EQfetch #EQio1 #EQstore #EQstack #EQio2 #EQnewpc
     280  #EQlab_pc #EQcosts #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in match eval_vmstate;
     281  normalize nodelta >EQfetch >m_return_bind normalize nodelta >EQio1 normalize nodelta
     282  >EQstack whd in match option_pop; normalize nodelta >m_return_bind
     283  >EQlab_pc >m_return_bind >EQcosts >EQstore  <EQio2 >EQio1 %
     284]
     285qed.
     286
     287coercion vm_step_to_eval.
     288
    247289include "../src/utilities/hide.ma".
    248290
     
    252294λp,p',prog.mk_abstract_status
    253295                (vm_state p p')
    254                 (λl.λst1,st2 : vm_state p p'.(eqb (pc ?? st1) (\snd prog)) = false ∧
     296                (λl.λst1,st2 : vm_state p p'.(eqb (pc ?? st1) (endmain … prog)) = false ∧
    255297                               vmstep p p' prog l st1 st2)
    256298                (λ_.λ_.True)
     
    269311                (λ_.true)
    270312                (λs.eqb (pc ?? s) O)
    271                 (λs.eqb (pc … s) (\snd prog))
     313                (λs.eqb (pc … s) (endmain … prog))
    272314                ???.
    273 @hide_prf cases daemon (*
     315@hide_prf
    274316[ #s1 #s2 #l inversion(fetch ???) normalize nodelta
    275317  [ #_ #EQ destruct] * normalize nodelta
     
    281323  | #_
    282324  ]
    283   #EQ destruct * #_ #H inversion H in ⊢ ?;
    284   [ #st1 #st2 #i #lbl #EQ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11
    285   | #st1 #st2 #new_pc #EQ #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23
    286   | #st1 #st2 #cond1 #new_pc1 #ltrue1 #lfalse1 #ev_c #EQ #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35
    287   | #st1 #st2 #cond1 #new_pc1 #ltrue1 #lfalse1 #ev_c #EQ #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47
    288   | #st1 #st2 #lin #io #lout #EQ #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59
    289   | #st1 #st2 #lin #io #lout #EQ #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 #H71
    290   | #st1 #st2 #f #EQ #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83
    291   | #st1 #st2 #new_pc #EQ #H85 #H86 #H87 #H88 #H89 #H90 #H91 #H92 #H93 #H94 #H95
    292   ]   
    293   destruct >EQfetch in EQ; whd in ⊢ (??%% → ?); #EQ
    294   lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct % //
     325  #EQ destruct * #_ #H lapply(vm_step_to_eval … H) whd in match eval_vmstate;
     326  normalize nodelta >EQfetch >m_return_bind normalize nodelta cases(asm_is_io ??)
     327  normalize nodelta [ whd in ⊢ (??%% → ?); #EQ destruct] #H cases(bind_inversion ????? H) -H
     328  * * #_ normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct % //
    295329| #s1 #s2 #l inversion(fetch ???) normalize nodelta
    296330  [ #_ #EQ destruct] * normalize nodelta
     
    302336  | #_
    303337  ]
    304   #EQ destruct * #_ #H inversion H in ⊢ ?;
    305   [ #st1 #st2 #i #lbl #EQf #EQio1 #H2 #H3 #H4 #EQio2 #H6 #H7 #H8 #H9 #H10 #H11
    306   | #st1 #st2 #new_pc #EQf #EQio1 #H13 #H14 #H15 #EQio2 #H17 #H18 #H19 #H20 #H21 #H22
    307   | #st1 #st2 #cond1 #new_pc1 #ltrue1 #lfalse1 #ev_c #EQf #EQio1 #H26 #H27 #H28 #EQio2 #H30 #H31 #H32 #H33 #H34 #H35
    308   | #st1 #st2 #cond1 #new_pc1 #ltrue1 #lfalse1 #ev_c #EQf #EQio1 #H38 #H39 #H40 #EQio2 #H42 #H43 #H44 #H45 #H46 #H47
    309   | #st1 #st2 #lin #io #lout #EQf #EQio1 #H50 #H51 #H52 #EQio2 #H54 #H55 #H56 #H57 #H58 #H59
    310   | #st1 #st2 #lin #io #lout #EQf #EQio1 #H61 #H62 #H63 #EQio2 #H65 #H66 #H67 #H68 #H69 #H70
    311   | #st1 #st2 #f #EQf #EQio1 #H74 #H75 #H76 #EQio2 #H78 #H79 #H80 #H81 #H82 #H83
    312   | #st1 #st2 #new_pc #EQf #EQio1 #H86 #H87 #H88 #EQio2 #H90 #H91 #H92 #H93 #H94 #H95
    313   ]   
    314   destruct >EQio in EQio2; >EQio1 #EQ destruct %{lin} //
     338  #EQ destruct * #_ #H lapply(vm_step_to_eval … H) whd in match eval_vmstate;
     339  normalize nodelta #H cases(bind_inversion ????? H) -H *
     340  [ #seq1 #lbl1
     341  | #n1
     342  | #cond1 #newpc1 #ltrue1 #lfalse1
     343  | #lin1 #io1 #lout1
     344  | #f
     345  |
     346  ]
     347  normalize nodelta * #_ cases(asm_is_io ??) normalize nodelta
     348  [1,3,5,9,11: whd in ⊢ (??%% → ?); #EQ destruct
     349  |2,6,7,10,12: #H cases(bind_inversion ????? H) -H #x * #_
     350    [2: cases x normalize nodelta
     351    |5: #H cases(bind_inversion ????? H) -H #y * #_
     352    ]
     353  ]
     354  whd in ⊢ (??%% → ?); #EQ destruct destruct % //
    315355|  #s1 #s2 #l inversion(fetch ???) normalize nodelta
    316356  [ #_ #EQ destruct] * normalize nodelta
    317357  [ #seq #lbl #_
    318358  | #n #_
    319   | #cond #newpc #ltrue #lfalse #EQfetch
    320   | #lin #io #lout #EQfetch cases (asm_is_io ??) normalize nodelta
     359  | #cond #newpc #ltrue #lfalse #_
     360  | #lin #io #lout #EQfetch inversion(asm_is_io ??) normalize nodelta #EQio
    321361  | #f #_
    322362  | #_
    323363  ]
    324   #EQ destruct * #_ #H inversion H in ⊢ ?;
    325   [ #st1 #st2 #i #lbl #EQ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11
    326   | #st1 #st2 #new_pc #EQ #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23
    327   | #st1 #st2 #cond1 #new_pc1 #ltrue1 #lfalse1 #ev_c #EQ #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35
    328   | #st1 #st2 #cond1 #new_pc1 #ltrue1 #lfalse1 #ev_c #EQ #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47
    329   | #st1 #st2 #lin1 #io1 #lout1 #EQ #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59
    330   | #st1 #st2 #lin1 #io1 #lout1 #EQ #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 #H71
    331   | #st1 #st2 #f #EQ #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83
    332   | #st1 #st2 #new_pc #EQ #H85 #H86 #H87 #H88 #H89 #H90 #H91 #H92 #H93 #H94 #H95
    333   ]   
    334   destruct >EQfetch in EQ; whd in ⊢ (??%% → ?); #EQ
    335   lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct % //
    336 ]*)
     364  #EQ destruct * #_ #H lapply(vm_step_to_eval … H) whd in match eval_vmstate;
     365  normalize nodelta  >EQfetch >m_return_bind normalize nodelta >EQio
     366  normalize nodelta #H cases(bind_inversion ????? H) -H #x * #_
     367  whd in ⊢ (??%% → ?); #EQ destruct % //
    337368qed.
    338369
     
    358389 … (fetch_state p p' prog) instr_m.
    359390
     391definition non_empty_list : ∀A.list A → bool ≝
     392λA,l.match l with [ nil ⇒ false | _ ⇒  true ].
    360393
    361394let rec block_cost (p : assembler_params)
     
    368401  [ O ⇒ None ?
    369402  | S program_size' ⇒
    370     if eqb program_counter (\snd prog) then
     403    if eqb program_counter (endmain … prog) then
    371404       return e … abs_t
    372405    else
     
    379412  ].
    380413 
    381 axiom initial_act : CostLabel.
     414inductive InitCostLabel : Type[0] ≝
     415  costlab : CostLabel → InitCostLabel
     416| initial_act : InitCostLabel.
     417
     418definition 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
     423definition 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 …)) %]
     426qed.
     427
     428coercion costlab.
     429
     430definition list_cost_to_list_initcost : list CostLabel → list InitCostLabel ≝
     431map … costlab.
     432
     433coercion list_cost_to_list_initcost.
    382434 
    383435record cost_map_T (dom : DeqSet) (codom : Type[0]) : Type[1] ≝
     
    390442}.
    391443
    392 let rec labels_pc (p : assembler_params)
    393 (prog : list (AssemblerInstr p)) (program_counter : ℕ) on prog : list (CostLabel × ℕ) ≝
    394 match prog with
    395 [ nil ⇒ [〈initial_act,O〉] @
    396         map … (λx.let〈y,z〉 ≝ x in 〈a_call z,y〉) (call_label_fun … p) @
    397         map … (λx.let〈y,z〉 ≝ x in 〈a_return_post z,y〉) (return_label_fun … p)
    398 | cons i is ⇒
    399   match i with
     444definition labels_pc_of_instr : ∀p.AssemblerInstr p → ℕ → list (InitCostLabel × ℕ) ≝
     445λp,i,program_counter.
     446match i with
    400447  [ Seq _ opt_l ⇒ match opt_l with
    401                   [ Some lbl ⇒ [〈a_non_functional_label lbl,S program_counter〉]
     448                  [ Some lbl ⇒ [〈costlab (a_non_functional_label lbl),S program_counter〉]
    402449                  | None ⇒ [ ]
    403450                  ]
    404451  | Ijmp _ ⇒ [ ]
    405   | CJump _ newpc ltrue lfalse ⇒ [〈a_non_functional_label ltrue,newpc〉;〈a_non_functional_label lfalse,S program_counter〉]
    406   | Iio lin _ lout ⇒ [〈a_non_functional_label lout,S program_counter〉]
     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〉]
    407456  | Icall f ⇒ [ ]
    408457  | Iret ⇒ [ ]
    409   ] @ labels_pc p is (S program_counter)             
     458  ].
     459
     460let rec labels_pc (p : assembler_params)
     461(prog : list (AssemblerInstr p)) (program_counter : ℕ) on prog : list (InitCostLabel × ℕ) ≝
     462match 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)
     466| cons i is ⇒ (labels_pc_of_instr … i program_counter)@labels_pc p is (S program_counter)
    410467].
    411468
     469lemma labels_pc_ok : ∀p,prog,i,lbl,pc,m.
     470fetch p prog pc = return i →
     471mem ? lbl (labels_pc_of_instr … i (m+pc)) →
     472mem ? lbl (labels_pc p (instructions … prog) m).
     473#p * #instrs #end_main #Hend_main #i #lbl #pc
     474whd in match fetch; normalize nodelta lapply pc -pc
     475-end_main elim instrs
     476[ #pc #m whd in ⊢ (??%% → ?); #EQ destruct]
     477#x #xs #IH * [|#pc'] #m whd in ⊢ (??%% → ?);
     478[ #EQ destruct #lbl_addr whd in match (labels_pc ???);
     479  /2 by mem_append_l1/
     480| #EQ #H2 whd in match (labels_pc ???); @mem_append_l2 @(IH … EQ) //
     481]
     482qed.
     483
     484lemma labels_pc_return: ∀p,prog,x1,x2.
     485 label_of_pc ReturnPostCostLabel (return_label_fun p) x1=return x2 →
     486 ∀m.
     487   mem … 〈costlab (a_return_post x2),x1〉 (labels_pc p (instructions p prog) m).
     488 #p * #l #endmain #_ whd in match (labels_pc ???); #x1 #x2 #H elim l
     489[ #m @mem_append_l2 @mem_append_l2 whd in H:(??%?);
     490  elim (return_label_fun ?) in H; [ whd in ⊢ (??%% → ?); #EQ destruct]
     491  * #x #y #tl #IH whd in ⊢ (??%? → %); normalize nodelta @eqb_elim
     492  normalize nodelta
     493  [ #EQ whd in ⊢ (??%% → ?); #EQ2 destruct /2/
     494  | #NEQ #H2 %2 @IH // ]
     495| #hd #tl #IH #m @mem_append_l2 @IH ]
     496qed.
     497
     498lemma labels_pc_call: ∀p,prog,x1,x2.
     499 label_of_pc CallCostLabel (call_label_fun p) x1=return x2 →
     500 ∀m.
     501   mem … 〈costlab (a_call x2),x1〉 (labels_pc p (instructions p prog) m).
     502 #p * #l #endmain #_ whd in match (labels_pc ???); #x1 #x2 #H elim l
     503[ #m @mem_append_l2 @mem_append_l1 whd in H:(??%?);
     504  elim (call_label_fun ?) in H; [ whd in ⊢ (??%% → ?); #EQ destruct]
     505  * #x #y #tl #IH whd in ⊢ (??%? → %); normalize nodelta @eqb_elim
     506  normalize nodelta
     507  [ #EQ whd in ⊢ (??%% → ?); #EQ2 destruct /2/
     508  | #NEQ #H2 %2 @IH // ]
     509| #hd #tl #IH #m @mem_append_l2 @IH ]
     510qed.
     511
     512unification hint  0 ≔ ;
     513    X ≟ DEQInitCostLabel
     514(* ---------------------------------------- *) ⊢
     515    InitCostLabel ≡ carr X.
     516
     517
     518unification hint  0 ≔ p1,p2;
     519    X ≟ DEQInitCostLabel
     520(* ---------------------------------------- *) ⊢
     521    eq_init_costlabel p1 p2 ≡ eqb X p1 p2.
     522   
     523
     524let rec m_foldr (M : Monad) (X,Y : Type[0]) (f : X→Y→M Y) (l : list X) (y : Y) on l : M Y ≝
     525match l with
     526[ nil ⇒ return y
     527| cons x xs ⇒ ! z ← m_foldr M X Y f xs y; f x z
     528].
     529
    412530definition static_analisys : ∀p : assembler_params.∀abs_t : monoid.(AssemblerInstr p → abs_t) →
    413 ∀mT : cost_map_T DEQCostLabel abs_t.AssemblerProgram p → option mT ≝
     531∀mT : cost_map_T DEQInitCostLabel abs_t.AssemblerProgram p → option mT ≝
    414532λp,abs_t,instr_m,mT,prog.
    415 let 〈instrs,final〉 ≝ prog in
    416 let prog_size ≝ S (|instrs|) in
    417 m_fold Option ?? (λx,m.let 〈z,w〉≝ x in ! k ← block_cost p prog abs_t instr_m w prog_size; 
    418                                return set_map … m z k) (labels_pc … instrs O)
    419       (empty_map ?? mT).
     533let prog_size ≝ S (|instructions … prog|) in
     534m_foldr Option ?? (λx,m.let 〈z,w〉≝ x in ! k ← block_cost p prog abs_t instr_m w prog_size; 
     535                               return set_map … m z k) (labels_pc … (instructions … prog) O)
     536      (empty_map ?? mT).
     537     
     538
     539include "basics/lists/listb.ma".
     540
     541(*doppione da mettere a posto*)
     542let rec no_duplicates (A : DeqSet) (l : list A) on l : Prop ≝
     543match l with
     544[ nil ⇒ True
     545| cons x xs ⇒ ¬ (bool_to_Prop (x ∈ xs)) ∧ no_duplicates … xs
     546].
     547
     548definition asm_no_duplicates ≝
     549λp,prog.no_duplicates … (map ?? \fst … (labels_pc … (instructions p prog) O)).
    420550
    421551(*falso: necessita di no_duplicates*)
    422 axiom static_analisys_ok : ∀p,abs_t,instr_m,mT,prog,lbl,pc,map.
     552
     553definition eq_deq_prod : ∀D1,D2 : DeqSet.D1 × D2 → D1 × D2 → bool ≝
     554λD1,D2,x,y.\fst x == \fst y ∧ \snd x == \snd y.
     555
     556definition DeqProd ≝ λD1 : DeqSet.λD2 : DeqSet.
     557mk_DeqSet (D1 × D2) (eq_deq_prod D1 D2) ?.
     558@hide_prf
     559* #x1 #x2 * #y1 #y2 whd in match eq_deq_prod; normalize nodelta
     560% [2: #EQ destruct @andb_Prop >(\b (refl …)) %]
     561inversion (? ==?) #EQ1 whd in match (andb ??); #EQ2 destruct
     562>(\P EQ1) >(\P EQ2) %
     563qed.
     564(*
     565unification hint  0 ≔ D1,D2 ;
     566    X ≟ DeqProd D1 D2
     567(* ---------------------------------------- *) ⊢
     568    D1 × D2 ≡ carr X.
     569
     570
     571unification hint  0 ≔ D1,D2,p1,p2;
     572    X ≟ DeqProd D1 D2
     573(* ---------------------------------------- *) ⊢
     574    eq_deq_prod D1 D2 p1 p2 ≡ eqb X p1 p2.
     575   
     576definition deq_prod_to_prod : ∀D1,D2 : DeqSet.DeqProd D1 D2 → D1 × D2 ≝
     577λD1,D2,x.x.
     578
     579coercion deq_prod_to_prod.
     580*)
     581
     582lemma map_mem : ∀A,B,f,l,a.mem A a l → ∃b : B.mem B b (map A B f l)
     583∧ b = f a.
     584#A #B #f #l elim l [ #a *] #x #xs #IH #a *
     585[ #EQ destruct %{(f x)} % // % // | #H cases(IH … H)
     586  #b * #H1 #EQ destruct %{(f a)} % // %2 //
     587]
     588qed.
     589
     590lemma static_analisys_ok : ∀p,abs_t,instr_m,mT,prog,lbl,pc,map.
     591asm_no_duplicates p prog →
    423592static_analisys p abs_t instr_m mT prog = return map →
    424 mem … 〈lbl,pc〉 (labels_pc … (\fst prog) O) →
    425 get_map … map lbl = block_cost … prog abs_t instr_m pc (S (|(\fst prog)|)). 
     593mem … 〈lbl,pc〉 (labels_pc … (instructions … prog) O) →
     594get_map … map lbl = block_cost … prog abs_t instr_m pc (S (|(instructions … prog)|)).
     595#p #abs_t #instr_m #mT * #prog whd in match static_analisys; normalize nodelta
     596whd in match asm_no_duplicates; normalize nodelta lapply (labels_pc ???)
     597#l #endmain #Hendmain elim l [ #x #y #z #w #h * ]
     598* #hd1 #hd2 #tl #IH #lbl #pc #map * #H1 #H2 #H
     599cases(bind_inversion ????? H) -H #map1 * #EQmap1 normalize nodelta #H
     600cases(bind_inversion ????? H) -H #elem * #EQelem whd in ⊢ (??%% → ?); #EQ
     601destruct *
     602[ #EQ destruct >get_set_hit >EQelem %
     603| #H >get_set_miss [ @IH //] inversion (? == ?) [2: #_ %]
     604  #ABS cases H1 -H1 #H1 @⊥ @H1 >(\P ABS) >mem_to_memb //
     605  cases(map_mem … \fst … H) #z1 * #Hz1 #EQ destruct @Hz1
     606]
     607qed.
    426608
    427609include "Simulation.ma".
     
    437619               ]
    438620 }.
    439  
    440 axiom vm_step_to_eval : ∀p,p',prog,st1,st2,l.vmstep … prog l st1 st2 →
    441 eval_vmstate p p' prog st1 = return 〈l,st2〉.
    442 
    443 coercion vm_step_to_eval.
    444621
    445622definition big_op: ∀M: monoid. list M → M ≝
     
    472649qed.
    473650
    474 lemma static_dynamic : ∀p,p',prog.
     651lemma monotonicity_of_block_cost : ∀p,prog,abs_t,instr_m,pc,size,k.
     652block_cost p prog abs_t instr_m pc size = return k →
     653∀size'.size ≤ size' →
     654block_cost p prog abs_t instr_m pc size' = return k.
     655#p #prog #abs_t #instr_m #pc #size lapply pc elim size
     656[ #pc #k whd in ⊢ (??%% → ?); #EQ destruct]
     657#n #IH #pc #k whd in ⊢ (??%% → ?); @eqb_elim
     658[ #EQ destruct normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct
     659  #size' * [2: #m #_] whd in ⊢ (??%%); @eqb_elim try( #_ %) * #H @⊥ @H %
     660| #Hpc normalize nodelta #H cases(bind_inversion ????? H) -H #i
     661  * #EQi #H cases(bind_inversion ????? H) -H #elem * #EQelem whd in ⊢ (??%% → ?);
     662  #EQ destruct #size' *
     663  [ whd in ⊢ (??%?); @eqb_elim
     664    [ #EQ @⊥ @(absurd ?? Hpc) assumption ]
     665    #_ normalize nodelta >EQi >m_return_bind >EQelem %
     666  | #m #Hm whd in ⊢ (??%?); @eqb_elim
     667    [ #EQ @⊥ @(absurd ?? Hpc) assumption ]
     668    #_ normalize nodelta >EQi >m_return_bind
     669    cases (emits_labels ??) in EQelem; normalize nodelta
     670    [ whd in ⊢ (??%%→ ??%%); #EQ destruct %]
     671    #f #EQelem >(IH … EQelem) [2: /2/ ] %
     672  ]
     673]
     674qed.
     675
     676lemma step_emit : ∀p,p',prog,st1,st2,l,i.
     677fetch p prog (pc … st1) = return i →
     678eval_vmstate p p' … prog st1 = return 〈l,st2〉 → 
     679emits_labels … i = None ? → ∃x.
     680match l in ActionLabel return λ_:ActionLabel.(list CostLabel) with 
     681[call_act f c ⇒ [a_call c]
     682|ret_act x ⇒
     683   match x with [None⇒[]|Some c⇒[a_return_post c]]
     684|cost_act x ⇒
     685   match x with [None⇒[]|Some c⇒[a_non_functional_label c]]
     686|init_act⇒[ ]
     687] = [x] ∧
     688 (mem … 〈costlab x,pc … st2〉 (labels_pc p (instructions … prog) O)).
     689#p #p' #prog #st1 #st2 #l #i #EQi whd in match eval_vmstate; normalize nodelta
     690>EQi >m_return_bind normalize nodelta cases i in EQi; -i normalize nodelta
     691[ #seq * [|#lab]
     692| #newpc
     693| #cond #newpc #ltrue #lfalse
     694| #lin #io #lout
     695| #f
     696|
     697]
     698#EQi cases(asm_is_io ???) normalize nodelta
     699[1,3,5,7,11,13: whd in ⊢ (??%% → ?); #EQ destruct
     700|2,4,8,9,12,14: #H cases(bind_inversion ????? H) -H #x1 * #EQx1
     701  [3: cases x1 in EQx1; -x1 #EQx1 normalize nodelta
     702  |6: #H cases(bind_inversion ????? H) -H #x2 * #EQx2
     703  ]
     704]
     705whd in ⊢ (??%% → ?); #EQ destruct whd in match emits_labels;
     706normalize nodelta #EQ destruct % [2,4,6,8,10,12,14: % try % |*:]
     707[1,2,4,5,7: @(labels_pc_ok … EQi) normalize /3 by or_introl,or_intror/ ]
     708/2 by labels_pc_return, labels_pc_call/
     709qed.
     710
     711lemma step_non_emit : ∀p,p',prog,st1,st2,l,i,f.
     712fetch p prog (pc … st1) = return i →
     713eval_vmstate p p' … prog st1 = return 〈l,st2〉 → 
     714emits_labels … i = Some ? f →
     715match l in ActionLabel return λ_:ActionLabel.(list CostLabel) with 
     716[call_act f c ⇒ [a_call c]
     717|ret_act x ⇒
     718   match x with [None⇒[]|Some c⇒[a_return_post c]]
     719|cost_act x ⇒
     720   match x with [None⇒[]|Some c⇒[a_non_functional_label c]]
     721|init_act⇒[ ]
     722] = [ ] ∧ pc … st2 = f (pc … st1).
     723#p #p' #prog #st1 #st2 #l #i #f #EQi whd in match eval_vmstate; normalize nodelta
     724>EQi >m_return_bind normalize nodelta cases i in EQi; -i normalize nodelta
     725[ #seq * [|#lab]
     726| #newpc
     727| #cond #newpc #ltrue #lfalse
     728| #lin #io #lout
     729| #f
     730|
     731]
     732#EQi cases(asm_is_io ???) normalize nodelta
     733[1,3,5,7,11,13: whd in ⊢ (??%% → ?); #EQ destruct
     734|2,4,8,9,12,14: #H cases(bind_inversion ????? H) -H #x1 * #EQx1
     735  [3: cases x1 in EQx1; -x1 #EQx1 normalize nodelta
     736  |6: #H cases(bind_inversion ????? H) -H #x2 * #EQx2
     737  ]
     738]
     739whd in ⊢ (??%% → ?); #EQ destruct whd in match emits_labels;
     740normalize nodelta #EQ destruct /2 by refl, conj/
     741qed.
     742
     743
     744lemma static_dynamic : ∀p,p',prog.asm_no_duplicates p prog →
    475745∀abs_t : abstract_transition_sys (m … p').∀instr_m.
    476746∀good : static_galois … (asm_static_analisys_data p p' prog abs_t instr_m).∀mT,map1.
     
    481751∀k.
    482752pre_measurable_trace … t →
    483 block_cost p prog … instr_m (pc … st1) (S (|(\fst prog)|)) = return k →
     753block_cost p prog … instr_m (pc … st1) (S (|(instructions … prog)|)) = return k →
    484754∀a1.rel_galois … good st1 a1 →
    485755let stop_state ≝ match R_post_step … ter with [None ⇒ st2 | Some x ⇒ \snd x ] in
     
    488758rel_galois … good stop_state (act_abs … abs_t (big_op … costs) (act_abs … abs_t k a1)).
    489759[2: @hide_prf cases daemon]
    490 #p #p' #prog #abs_t #instr_m #good #mT #map1 #EQmap #st1 #st2 #ter #t
     760#p #p' #prog #no_dup #abs_t #instr_m #good #mT #map1 #EQmap #st1 #st2 #ter #t
    491761lapply ter -ter elim t
    492762[ #st #ter inversion(R_post_step … ter) normalize nodelta [| * #lbl #st3 ]
     
    522792| -st1 -st2 #st1 #st2 #st3 #l * #H3 #H4 #tl #IH #ter #k #H
    523793  #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
    571     inversion H4
    572     [ #s1 #s2 #i1 * [| #lbl] #EQfetch #no_io #EQstore #EQstack #EQio #EQpc
    573       #EQcost #EQ1 #EQ2 #EQ3 #EQ4 destruct >EQi in EQfetch; whd in ⊢ (??%% → ?);
    574       #EQ destruct whd in match emits_labels; normalize nodelta
    575       [ cases H1 whd in ⊢ (% → ?); [ * |  #EQ destruct]]
    576       * whd in ⊢ (??%% → ?); #EQ destruct >neutral whd in ⊢ (??%% → ?);
    577       #EQ destruct whd in match (foldr ?????);
    578 
    579 
    580 
    581 
     794  whd #costs whd in match list_cost_to_list_initcost; normalize nodelta
     795  <map_append <map_append
     796  change with (list_cost_to_list_initcost ?) in match (list_cost_to_list_initcost ?); 
     797  #EQ destruct whd in H2 : (??%?); >H3 in H2; normalize nodelta #H
     798  cases(bind_inversion ????? H) -H #i * #EQi
     799  inversion(emits_labels ??)
     800  [ #EQemits whd in ⊢ (??%% → ?); #EQ destruct  >big_op_associative >act_op @IH
     801  | #f #EQemits normalize nodelta #H
     802    cases(bind_inversion ????? H) -H #k' * #EQk' whd in ⊢ (??%% → ?);
     803    #EQ destruct(EQ) >act_op whd in match (append ???); @IH
     804  ]
     805  [1,5: inversion H in ⊢ ?;
     806    [1,6: #st #c #EQ1 #EQ2 #EQ3 #EQ4 destruct
     807    |2,7: #s1 #s2 #s3 #lbl #exe #tl1 #s1_noio * #opt_l #EQ destruct #pre_tl1 #_
     808      #EQ1 #EQ2 #EQ3 #EQ4 destruct
     809    |3,8: #s1 #s2 #s3 #lbl #s1_noio #exe #tl1 * #lbl1 #EQ destruct #pre_tl1 #_
     810      #EQ1 #EQ2 #EQ3 #EQ4 destruct
     811    |4,9: #s1 #s2 #s3 #lbl #exe #tl1 #s1_noio * #f * #lbl1 #EQ destruct
     812      * #pre_tl1 #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct
     813    |5,10: #s1 #s2 #s3 #s4 #s5 #l1 #l2 #exe1 #t1 #t2 #exe2 #noio1 #noio2 #H *
     814    ] //
     815  | cases(step_emit … EQi (vm_step_to_eval … H4) … EQemits) #x * #EQx #Hx >EQx
     816    whd in match (map ????); whd in match (map ????); whd in match (big_op ??);
     817    >neutral_l @opt_safe_elim #elem #EQget <(static_analisys_ok  … x … (pc … st2) … EQmap)
     818    assumption
     819  | >neutral_r  @(instr_map_ok … good … EQi … good_a1) /2/
     820  | %
     821  | >(proj2 … (step_non_emit … EQi (vm_step_to_eval … H4) … EQemits))
     822    >(monotonicity_of_block_cost … EQk') //
     823  | @(instr_map_ok … good … EQi … good_a1) /2/
     824  | >(proj1 … (step_non_emit … EQi (vm_step_to_eval … H4) … EQemits)) %
     825  ]
     826]
     827qed.
     828
     829
     830
     831
Note: See TracChangeset for help on using the changeset viewer.