Changeset 3485 for LTS


Ignore:
Timestamp:
Sep 23, 2014, 4:47:59 PM (5 years ago)
Author:
piccolo
Message:

partial measurable static dynamic

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Vm.ma

    r3478 r3485  
    448448
    449449lemma labels_pc_ok : ∀p,prog,i,lbl,pc,m.
    450 fetch p prog pc = return i →
     450nth_opt ? pc prog = return i →
    451451mem ? lbl (labels_pc_of_instr … i (m+pc)) →
    452 mem ? lbl (labels_pc p (instructions … prog) m).
    453 #p * #instrs #end_main #Hend_main #i #lbl #pc
     452mem ? lbl (labels_pc p prog m).
     453#p #instrs #i #lbl #pc
    454454whd in match fetch; normalize nodelta lapply pc -pc
    455 -end_main elim instrs
     455elim instrs
    456456[ #pc #m whd in ⊢ (??%% → ?); #EQ destruct]
    457457#x #xs #IH * [|#pc'] #m whd in ⊢ (??%% → ?);
     
    465465 label_of_pc ReturnPostCostLabel (return_label_fun p) x1=return x2 →
    466466 ∀m.
    467    mem … 〈(a_return_post x2),x1〉 (labels_pc p (instructions p prog) m).
    468  #p * #l #endmain #_ whd in match (labels_pc ???); #x1 #x2 #H elim l
     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
    469469[ #m @mem_append_l2 @mem_append_l2 whd in H:(??%?);
    470470  elim (return_label_fun ?) in H; [ whd in ⊢ (??%% → ?); #EQ destruct]
     
    479479 label_of_pc CallCostLabel (call_label_fun p) x1=return x2 →
    480480 ∀m.
    481    mem … 〈(a_call x2),x1〉 (labels_pc p (instructions p prog) m).
    482  #p * #l #endmain #_ whd in match (labels_pc ???); #x1 #x2 #H elim l
     481   mem … 〈(a_call x2),x1〉 (labels_pc p prog m).
     482 #p #l whd in match (labels_pc ???); #x1 #x2 #H elim l
    483483[ #m @mem_append_l2 @mem_append_l1 whd in H:(??%?);
    484484  elim (call_label_fun ?) in H; [ whd in ⊢ (??%% → ?); #EQ destruct]
     
    883883 get_costlabels_of_trace … (trace … t).
    884884
     885lemma i_act_in_map :  ∀p,prog.
     886mem … 〈i_act,O〉 (labels_pc … (instructions p prog) O).
     887#p *#instr #n #_ generalize in match O in ⊢ (???%); elim instr
     888[ normalize /2/] #i #xs #IH #m whd in match (labels_pc ???);
     889@mem_append_l2 @IH
     890qed.
     891
     892
     893lemma as_execute_labelled_ok : ∀p,p',prog,c,l,st1,st2.
     894eval_vmstate p p' prog st1 = return 〈l,st2〉 → actionlabel_to_costlabel l = [c] →
     895∃n.
     896mem … 〈c,n〉 (labels_pc … (instructions p prog) O).
     897#p #p' * #instr #endmain #Hendmain #c #l #st1 #st2 #H2 lapply H2 whd in match eval_vmstate; normalize nodelta
     898#H cases(bind_inversion ????? H) -H #i * #EQfetch #_
     899 inversion(emits_labels … i)
     900 [ #EQemit cases(step_emit … H2) // #x * #EQ1 #EQ2 whd in match actionlabel_to_costlabel;
     901   normalize nodelta >EQ1 #EQ destruct /2 by ex_intro/
     902  | #f #EQemit whd in match actionlabel_to_costlabel; normalize nodelta  >(proj1 … (step_non_emit … EQfetch H2 … EQemit))
     903    #EQ destruct
     904 ]
     905qed.
     906 
     907
    885908(*get_costlabels_of_measurable_trace deve aggiungere la label iniziale.*)
    886909theorem static_dynamic_meas : ∀p,p',prog.∀no_dup : asm_no_duplicates p prog.
     
    889912∀EQmap : static_analisys p ? instr_m mT prog = return map1.
    890913∀t : measurable_trace (asm_operational_semantics p p' prog).
    891 ∀a1.rel_galois … good (L_s1 … t) a1 →
    892 let stop_state ≝ match R_post_state … t with [None ⇒ R_s2 … t | Some x ⇒ x ] in
     914let start_state ≝ match L_pre_state … t with [None ⇒ L_s1 … t | Some x ⇒ x ] in
     915∀a1.rel_galois … good start_state a1 →
    893916∀abs_trace.
    894917abs_trace = dependent_map CostLabel ? (get_costlabels_of_measurable_trace …  t) (λlbl,prf.(opt_safe … (get_map … map1 lbl) ?)) →
    895 rel_galois … good stop_state (act_abs … abs_t (big_op … abs_trace) a1).
     918rel_galois … good (R_s2 … t) (act_abs … abs_t (big_op … abs_trace) a1).
    896919[2: @hide_prf
    897920    whd in match get_costlabels_of_measurable_trace in prf; normalize nodelta in prf;
     
    902925        @(proj2 … (static_analisys_ok … no_dup … EQmap … Hmem))
    903926    | 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
     927      [ * [2: *] #EQ destruct >(proj1 … (static_analisys_ok … no_dup … EQmap … (i_act_in_map …)))
     928        @(proj2 … (static_analisys_ok … no_dup … EQmap … (i_act_in_map …)))
     929      | #H lapply(L_init_ok … t) inversion(L_pre_state … t) [ #_ normalize nodelta * #_ >EQleft #EQ destruct]
     930        #st_pre #EQst_pre normalize nodelta * #l' ** >EQleft #EQ destruct cases l' in H;
     931        [ #x1 #x2 | * [|#x1] | * [|#x1]] whd in ⊢ (% → %→ ?); * [2,4,6: *] #EQ destruct * * #_
     932        #H cases(as_execute_labelled_ok … H) [3,6,9:% |*:] #w #EQw
     933        >(proj1 … (static_analisys_ok … no_dup … EQmap … EQw))
     934       @(proj2 … (static_analisys_ok … no_dup … EQmap … EQw))
    906935      ]
    907936    ]
    908937]
    909938#p #p' #prog #no_dup #abs_t #instr_m #good #mT #map1 #EQmap1 #t #a1 #rel_galois #abs_trace #EQabs_trace
     939@(static_dynamic …)
     940
    910941xxxxxx
    911942lapply(static_dynamic … (trace …t) … abs_trace) try //
Note: See TracChangeset for help on using the changeset viewer.