Changeset 3464 for LTS/Vm.ma


Ignore:
Timestamp:
Feb 21, 2014, 8:34:32 PM (6 years ago)
Author:
piccolo
Message:

static_dinamic in place

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Vm.ma

    r3463 r3464  
    3232{ instructions : list (AssemblerInstr p)
    3333; endmain : ℕ
    34 ; endmain_ok : endmain |instructions|
     34; endmain_ok : endmain < |instructions|
    3535}.
    3636
     
    510510qed.
    511511
     512(*
     513lemma labels_pc_bounded : ∀p.∀prog : AssemblerProgram p.∀lbl,pc.∀m.
     514mem ? 〈lbl,pc〉 (labels_pc p (instructions … prog) m) →
     515(m + pc) < (|(instructions … prog)|).
     516#p * #instr #endmain #_  #H1 #H2 elim instr
     517[ #H3 @⊥ /2/ ] #x #xs #IH #_ #lbl #pc #m whd in match (labels_pc ???);
     518#H cases(mem_append ???? H) -H
     519[ whd in match labels_pc_of_instr; normalize nodelta
     520  cases x normalize nodelta
     521  [ #seq * [|#lab]
     522  | #newpc
     523  | #cond #newpc #ltrue #lfalse
     524  | #lin #io #lout
     525  | #f
     526  |
     527  ]
     528  normalize [1,3,6,7: *] * [2,4,6: * [2,4:*] ]
     529  #EQ destruct
     530*) 
     531
    512532unification hint  0 ≔ ;
    513533    X ≟ DEQInitCostLabel
     
    592612static_analisys p abs_t instr_m mT prog = return map →
    593613mem … 〈lbl,pc〉 (labels_pc … (instructions … prog) O) →
    594 get_map … map lbl = block_cost … prog abs_t instr_m pc (S (|(instructions … prog)|)).
     614get_map … map lbl =
     615block_cost … prog abs_t instr_m pc (S (|(instructions … prog)|)) ∧
     616block_cost … prog abs_t instr_m pc (S (|(instructions … prog)|)) ≠ None ?.
    595617#p #abs_t #instr_m #mT * #prog whd in match static_analisys; normalize nodelta
    596618whd in match asm_no_duplicates; normalize nodelta lapply (labels_pc ???)
     
    600622cases(bind_inversion ????? H) -H #elem * #EQelem whd in ⊢ (??%% → ?); #EQ
    601623destruct *
    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
     624[ #EQ destruct % [ >get_set_hit >EQelem % | >EQelem % whd in ⊢ (??%% → ?); #EQ destruct]
     625| #H %
     626  [ >get_set_miss [ @(proj1 … (IH …)) //] inversion (? == ?) [2: #_ %]
     627    #ABS cases H1 -H1 #H1 @⊥ @H1 >(\P ABS) >mem_to_memb //
     628    cases(map_mem … \fst … H) #z1 * #Hz1 #EQ destruct @Hz1
     629  | @(proj2 … (IH …)) //
     630  ]
    606631]
    607632qed.
     
    741766qed.
    742767
    743 
    744 lemma static_dynamic : ∀p,p',prog.asm_no_duplicates p prog →
     768lemma labels_of_trace_are_in_code :
     769∀p,p',prog.∀st1,st2 :  vm_state p p'.∀t : raw_trace (asm_operational_semantics p p' prog) … st1 st2.
     770∀lbl.
     771mem … lbl (get_costlabels_of_trace … t) →
     772mem … (costlab lbl) (map ?? \fst … (labels_pc … (instructions p prog) O)).
     773#p #p' #prog #st1 #st2 #t elim t
     774[ #st #lbl *
     775| #st1 #st2 #st3 #l * #H1 #H2 #tl #IH #lbl whd in match (get_costlabels_of_trace ????);
     776  #H cases(mem_append ???? H) -H [2: #H @IH //]
     777  lapply(vm_step_to_eval … H2) whd in match eval_vmstate;
     778  normalize nodelta #H cases(bind_inversion ????? H) -H #i * #EQi #_
     779  inversion(emits_labels … i)
     780  [ #EQemit cases(step_emit … (vm_step_to_eval … H2)) // #x * #EQ1 #EQ2 >EQ1 *
     781    [2: *] #EQ destruct cases(map_mem … \fst … EQ2) #y * #H3 #EQ destruct //
     782  | #f #EQemit >(proj1 … (step_non_emit … EQi (vm_step_to_eval … H2) … EQemit))
     783    *
     784  ]
     785
     786qed.
     787
     788let rec dependent_map (A,B : Type[0]) (l : list A) (f : ∀a : A.mem … a l → B) on l : list B ≝
     789(match l return λx.l=x → ? with
     790[ nil ⇒ λ_.nil ?
     791| cons x xs ⇒ λprf.(f x ?) :: dependent_map A B xs (λx,prf1.f x ?)
     792])(refl …).
     793[ >prf %% | >prf %2 assumption]
     794qed.
     795
     796lemma dependent_map_append : ∀A,B,l1,l2,f.
     797dependent_map A B (l1 @ l2) (λa,prf.f a prf) =
     798(dependent_map A B l1 (λa,prf.f a ?)) @ (dependent_map A B l2 (λa,prf.f a ?)).
     799[2: @hide_prf /2/ | 3: @hide_prf /2/]
     800#A #B #l1 elim l1 normalize /2/
     801qed.
     802
     803lemma rewrite_in_dependent_map : ∀A,B,l1,l2,f.
     804        ∀EQ:l1 = l2.
     805         dependent_map A B l1 (λa,prf.f a prf) =
     806         dependent_map A B l2 (λa,prf.f a ?).
     807[2: >EQ // | #A #B #l1 #l2 #f #EQ >EQ in f; #f % ]
     808qed.
     809
     810
     811lemma static_dynamic : ∀p,p',prog.∀no_dup : asm_no_duplicates p prog.
    745812∀abs_t : abstract_transition_sys (m … p').∀instr_m.
    746813∀good : static_galois … (asm_static_analisys_data p p' prog abs_t instr_m).∀mT,map1.
    747 static_analisys p ? instr_m mT prog = return map1 →
     814∀EQmap : static_analisys p ? instr_m mT prog = return map1.
    748815∀st1,st2 : vm_state p p'.
    749816∀ter : terminated_trace (asm_operational_semantics p p' prog) st2.
     
    755822let stop_state ≝ match R_post_step … ter with [None ⇒ st2 | Some x ⇒ \snd x ] in
    756823∀costs.
    757 costs = map … (λlbl.(opt_safe … (get_map … map1 lbl) ?)) (get_costlabels_of_trace …  t) →
     824costs = dependent_map CostLabel ? (get_costlabels_of_trace …  t) (λlbl,prf.(opt_safe … (get_map … map1 lbl) ?)) →
    758825rel_galois … good stop_state (act_abs … abs_t (big_op … costs) (act_abs … abs_t k a1)).
    759 [2: @hide_prf cases daemon]
     826[2: @hide_prf
     827    cases(mem_map ????? (labels_of_trace_are_in_code … prf)) *
     828    #lbl' #pc * #Hmem #EQ destruct   
     829    >(proj1 … (static_analisys_ok … no_dup … EQmap … Hmem))
     830    @(proj2 … (static_analisys_ok … no_dup … EQmap … Hmem))
     831]
    760832#p #p' #prog #no_dup #abs_t #instr_m #good #mT #map1 #EQmap #st1 #st2 #ter #t
    761833lapply ter -ter elim t
     
    786858    [4,8: cases H1 [1,3: * |*: * #y #EQ destruct]]
    787859    >m_return_bind whd in ⊢ (??%% → ?); #EQ destruct
    788     #a1 #good_st_a1 whd in match (map ????); #costs #EQ >EQ >neutral_r
     860    #a1 #good_st_a1 whd in match (dependent_map ????); #costs #EQ >EQ >neutral_r
    789861    >act_neutral
    790862    @(instr_map_ok … good … EQfetch … good_st_a1) /2/
     
    792864| -st1 -st2 #st1 #st2 #st3 #l * #H3 #H4 #tl #IH #ter #k #H
    793865  #H2 #a1 #good_a1 whd in match (get_costlabels_of_trace ????);
    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
     866  whd #costs >dependent_map_append
     867  (*change with (list_cost_to_list_initcost ?) in match (list_cost_to_list_initcost ?);*) 
     868  #EQ destruct whd in H2 : (??%?); lapply H2 >H3 in ⊢ (% → ?); -H2
     869  normalize nodelta #H cases(bind_inversion ????? H) -H #i * #EQi
    799870  inversion(emits_labels ??)
    800871  [ #EQemits whd in ⊢ (??%% → ?); #EQ destruct  >big_op_associative >act_op @IH
     
    813884    |5,10: #s1 #s2 #s3 #s4 #s5 #l1 #l2 #exe1 #t1 #t2 #exe2 #noio1 #noio2 #H *
    814885    ] //
    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
     886  | cases(step_emit … EQi (vm_step_to_eval … H4) … EQemits) #x * #EQx #Hx
     887    >(rewrite_in_dependent_map … EQx)
     888 
     889    whd in match (dependent_map ????); whd in match (dependent_map ????); whd in match (big_op ??);
     890    >neutral_l @opt_safe_elim #elem #EQget
     891    cases (static_analisys_ok  … x … (pc … st2) … no_dup … EQmap) //
     892    #EQ #_ <EQ assumption
    819893  | >neutral_r  @(instr_map_ok … good … EQi … good_a1) /2/
    820894  | %
     
    822896    >(monotonicity_of_block_cost … EQk') //
    823897  | @(instr_map_ok … good … EQi … good_a1) /2/
    824   | >(proj1 … (step_non_emit … EQi (vm_step_to_eval … H4) … EQemits)) %
    825   ]
    826 ]
    827 qed.
    828 
    829 
    830 
    831 
     898  | lapply (proj1 … (step_non_emit … EQi (vm_step_to_eval … H4) … EQemits))
     899    #EQ >(rewrite_in_dependent_map … EQ) %
     900  ]
     901]
     902qed.
     903
     904
     905
     906
Note: See TracChangeset for help on using the changeset viewer.