Changeset 3490


Ignore:
Timestamp:
Sep 24, 2014, 5:15:02 PM (5 years ago)
Author:
piccolo
Message:
 
File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Vm.ma

    r3489 r3490  
    459459
    460460definition asm_static_analisys_data ≝ λp,p',prog,abs_t,instr_m.
    461 mk_static_analysis_data (asm_concrete_trans_sys p p' prog) abs_t
    462  … (λs.match s with [ STATE st ⇒ fetch_state p p' prog st | _ ⇒ None ? ]) instr_m.
     461mk_static_analysis_data (asm_concrete_trans_sys p p' prog) abs_t (option (AssemblerInstr p))
     462 (λs.match s with [ STATE st ⇒ ! x ← fetch_state p p' prog st; Some ? (Some ? x)
     463                  | INITIAL ⇒ Some ? (None ?)
     464                  | FINAL  ⇒ None ? ]) instr_m.
    463465
    464466definition non_empty_list : ∀A.list A → bool ≝
     
    655657
    656658definition terminated_trace : ∀S : abstract_status.∀s1,s3 : S.raw_trace … s1 s3 → Prop ≝
    657 λS,s1,s3,t.bool_to_Prop (as_final … s3) ∨
    658        ∃s2: S.∃t1 : raw_trace … s1 s2.∃ l,prf.t = t1 @ (t_ind ? s2 s3 s3 l prf … (t_base … s3))
     659λS,s1,s3,t.∃s2: S.∃t1 : raw_trace … s1 s2.∃ l,prf.t = t1 @ (t_ind ? s2 s3 s3 l prf … (t_base … s3))
    659660∧ ((is_costlabelled_act l ∨ is_labelled_ret_act l) ∧
    660661   (is_call_act l → bool_to_Prop (is_call_post_label … s2))).
     
    833834
    834835
     836lemma tbase_tind_append : ∀S : abstract_status.∀st1,st2,st3.∀t : raw_trace … st1 st2.
     837∀l,prf.∀t'.
     838t_base … st1 = t @ t_ind S st2 st3 st1 l prf t' → False.
     839#S #st1 #st2 #st3 *
     840[ #st #l #prf  #t' normalize #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct ]
     841#s1 #s2 #s3 #l1 #prf1 #t2 #l2 #prf2 #t3 normalize #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
     842qed.
     843
     844
     845
    835846lemma static_dynamic : ∀p,p',prog.
    836 ∀abs_t : abstract_transition_sys (m … p').∀instr_m.
    837 ∀good : static_galois … (asm_static_analisys_data p p' prog abs_t instr_m).∀mT,map1.
     847∀abs_t : abstract_transition_sys (m … p').∀instr_m : (AssemblerInstr p) → abs_instr … abs_t.
     848∀good : static_galois … (asm_static_analisys_data p p' prog abs_t
     849 (λi.match i with [None ⇒ e …
     850                  |Some x ⇒ instr_m x
     851                  ])) .∀mT,map1.
    838852∀EQmap : static_analisys p ? instr_m mT prog = return map1.
    839853∀st1,st2 : vm_ass_state p p'.
     
    853867    @(proj2 … (static_analisys_ok … EQmap … Hmem))
    854868]
    855 #p #p' #prog #abs_t #instr_m #good #mT #map1 #EQmap #st1 #st2 #t elim t
    856 [ #st * [| * #st3 * #t1 * #l * #prf * #ABS @⊥ cases t1 in ABS; ]
     869#p #p' #prog #abs_t #instr_m #good #mT #map1 #EQmap #st1 #st2 #t * #st3 * #t1 * #l1 * #prf1 * #EQ destruct
     870lapply prf1 -prf1 lapply l1 -l1 elim t1 -st3
     871[ * [3: #st] #l #prf * #H1 #H2 #k #_ whd in ⊢ (??%? → ?);
     872  [3: cases prf
     873  |2: whd in ⊢ (??%% → ?); #EQ destruct #a1 #rel_fin #labels whd in match (get_costlabels_of_trace ????);
     874      whd in match (get_costlabels_of_trace ????); cases st2 in prf; -st2 [3: #st2] *
     875      #EQpc_st2 #EQ destruct normalize nodelta whd in ⊢ (??%% → ?); @opt_safe_elim #k_init
     876      #EQk_init whd in ⊢ (??%% → ?); whd in match (dependent_map ????); #EQ destruct
     877      >act_neutral whd in match (big_op ??); >act_op >act_neutral
     878      @(instr_map_ok … good … rel_fin)
     879     
     880       #H >act_neutral whd in prf;
     881       
     882        cases l in prf H1 H2;
     883        [1,4: #f #lbl |2,5: * [2,4: #lbl] |*: * [2,4: #lbl] ] #prf
     884        ** [normalize in ⊢ (% → ?);
     885         ⊢ (??%% → ?);
     886
     887 #st * #st3 * #t1 * #l * #prf * #ABS cases(tbase_tind_append … ABS) ]
     888  cases st -st [3: #x] * #H #_ whd in ⊢ (??%% → ?); @eqb_elim [2: * #ABS @⊥ @ABS %]
     889   #_ normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct #a1 #rel_fin_a1
     890   #labels whd in ⊢ (???% → ?); #EQ destruct >act_neutral >act_neutral assumption
     891| -st1 -st2 * [3: #st1] * [3,6,9: #st2] #st3 #l whd in ⊢ (% → ?); *
     892  [ #no_final #Hstep #tl #IH whd in ⊢ (% → ?);
     893   (*
     894    #EQlabels
    857895  #EQr_post #k #_ lapply(R_fin_ok … ter) >EQr_post normalize nodelta
    858896  [ whd in ⊢ (?% → ?); #final_st whd in ⊢ (??%? → ?); >final_st
     
    883921    >act_neutral
    884922    @(instr_map_ok … good … EQfetch … good_st_a1) /2/
    885   ]
     923  ]*)
    886924| -st1 -st2 #st1 #st2 #st3 #l * #H3 #H4 #tl #IH #ter #k #H
    887925  #H2 #a1 #good_a1 whd in match (get_costlabels_of_trace ????);
Note: See TracChangeset for help on using the changeset viewer.