Changeset 3503


Ignore:
Timestamp:
Sep 26, 2014, 2:40:35 PM (5 years ago)
Author:
piccolo
Message:
 
File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Vm.ma

    r3502 r3503  
    11031103
    11041104definition measurable :
    1105  ∀S: abstract_status. ∀s1,s2,s4 : S. raw_trace … s1 s4 → Prop ≝
    1106 λS,s1,s2,s4,t.
     1105 ∀S: abstract_status. ∀si,s1,s3,sn : S. raw_trace … si sn → Prop ≝
     1106λS,si,s1,s3,sn,t.
    11071107 pre_measurable_trace … t ∧
    1108  ∃s3:S. ∃t' : raw_trace … s2 s3. ∃l1,l2,prf1,prf2.
    1109   t = t_ind ? s1 s2 s4 l1 prf1 … (t' @ (t_ind ? s3 s4 s4 l2 prf2 … (t_base … s4)))
    1110  ∧ is_costlabelled_act l1 ∧ is_costlabelled_act l2.
    1111 
     1108 ∃s0,s2:S. ∃ti0 : raw_trace … si s0.∃t12 : raw_trace … s1 s2.∃t3n : raw_trace … s3 sn.
     1109 ∃l1,l2,prf1,prf2.
     1110  t = ti0 @  t_ind ? s0 s1 sn l1 prf1 … (t12 @ (t_ind ? s2 s3 sn l2 prf2 … t3n))
     1111 ∧ is_costlabelled_act l1 ∧ is_costlabelled_act l2 ∧ silent_trace … ti0 ∧ silent_trace … t3n.
     1112 
     1113lemma chop_cons : ∀A : Type[0].∀x : A.∀xs: list A. xs ≠ [ ] → chop … (x :: xs) = x :: (chop … xs).
     1114#A #x * [ #H cases(absurd ?? H) % ] // qed.
     1115 
    11121116(*
    11131117lemma measurable_terminated:
     
    11171121qed. *)
    11181122
     1123lemma execute_mem_label_pc :∀p,p',prog.∀st0,st1 :vm_state p p'.∀l1,c1.
     1124actionlabel_to_costlabel l1 = [c1] →
     1125vmstep p p' prog l1 st0 st1 →
     1126 mem … 〈c1,pc p p' st1〉
     1127  (labels_pc … (instructions … prog) (call_label_fun … prog)
     1128   (return_label_fun … prog) (in_act … prog) O).
    11191129theorem static_dynamic :
    11201130(* Given an assembly program *)
     
    11291139(* For every measurable trace whose second state is st1 or, equivalently,
    11301140   whose first state after the initial labelled transition is st1 *)
    1131 ∀st0,st1,stn. ∀t: raw_trace (asm_operational_semantics … prog) … st0 stn.
    1132  measurable … st1 … t →
     1141∀si,s1,s2,sn. ∀t: raw_trace (asm_operational_semantics … prog) … si sn.
     1142 measurable … s1 s2 … t →
    11331143
    11341144(* Let labels be the costlabels observed in the trace (last one excluded) *)
     
    11421152
    11431153(* Given an abstract state in relation with the second state of the trace *)
    1144 ∀a1.R st1 a1 →
     1154∀a1.R s1 a1 →
    11451155
    11461156(* The final state of the trace is in relation with the one obtained by
    11471157   applying every semantics in abs_trace. *)
    1148 R stn (〚abs_actions〛 a1).
    1149 [2: @hide_prf cases daemon
    1150 | #p #p' #prog #R #mT #map1 #EQmap #st0 #st1 #stn #t #measurable
    1151   cases measurable #premeas * #st3 * #t' * #l1 * #l2 * #prf1 * #prf2 ** #EQ destruct
    1152   #Hl1 #Hl2 #acts #EQacts #a1 #HR
    1153   cut (∃act.∃actstl. acts = act::actstl)
    1154   [ cases daemon (* usare measurable *) ]
    1155   * #act * #actstl #EQacts2 >EQacts2
    1156   cut (〚act::actstl〛 a1 = (〚actstl〛 (〚act〛 a1)))
    1157   [ cases daemon (* true *) ]
    1158   #EQ >EQ -EQ >EQacts2 in EQacts; #EQacts
    1159   @(static_dynamic_inv … EQmap … (t' @ t_ind … prf2 (t_base …)) … actstl … HR)
     1158R s2 (〚abs_actions〛 a1).
     1159[2: @hide_prf
     1160    cases(mem_map ????? (labels_of_trace_are_in_code … (chop_mem … prf))) *
     1161    #lbl' #pc * #Hmem #EQ destruct   
     1162    >(proj1 … (static_analisys_ok … EQmap … Hmem))
     1163    @(proj2 … (static_analisys_ok … EQmap … Hmem))
     1164]
     1165#p #p' #prog #R #mT #map1 #EQmap #si #s1 #s2 #sn #t #measurable
     1166cases measurable #premeas * #s0 * #s3 * #ti0 * #t12 * #t3n *  #l1 * #l2 * #prf1 * #prf2
     1167**** #EQ destruct #Hl1 #Hl2 #silent_ti0 #silent_t3n #acts cases(actionlabel_ok … Hl1)
     1168#c1 #EQc1 >rewrite_in_dependent_map
     1169[2: >get_cost_label_append in ⊢ (??%?); >(get_cost_label_silent_is_empty … silent_ti0) in ⊢ (??%?);
     1170     >get_cost_label_of_trace_tind in ⊢ (??%?); >get_cost_label_append in ⊢ (??%?);
     1171      >get_cost_label_of_trace_tind in ⊢ (??%?);
     1172     >(get_cost_label_silent_is_empty … silent_t3n) in ⊢ (??%?);
     1173     >append_nil in ⊢ (??%?); >EQc1 in ⊢ (??%?); whd in ⊢ (??(??%)?);
     1174     whd in ⊢ (??(??(???%))?); >chop_cons in ⊢ (??%?); [2: cases daemon] % |3:
     1175 ]
     1176 whd in ⊢ (???% → ?); @opt_safe_elim #act #EQact #EQacts2 >EQacts2
     1177 >(big_op_associative ? [?]) #a1 >act_op #HR
     1178letin actsl ≝ (dependent_map ????);
     1179@(static_dynamic_inv … EQmap … (t12 @ t_ind … prf2 (t_base …)) … actsl … HR)
    11601180  [ /6 width=6 by conj, ex_intro/
    11611181  | cases daemon (* true *)
    1162   | cases daemon (* true *)
    1163   | cases daemon (* true *) ]]
    1164 qed.
     1182  | cases s1 in prf1 t12; [3: #st1] cases s0 [3,6,9: #st0] *
     1183    [2: #H #EQ lapply(refl ? (FINAL p p')) generalize in match (FINAL p p') in ⊢ (??%? → %);
     1184        #st' #EQst' #tr lapply prf2 lapply EQst' -EQst' cases tr
     1185        [ #st'' #EQ2 >EQ2 *
     1186        | #st'' #st''' #st'''' #l3 #ABS #_ #EQ2 >EQ2 in ABS; *
     1187        ]
     1188    | #H1 #H2 #_ whd in match get_pc; normalize nodelta
     1189      <(proj1 ?? (static_analisys_ok … EQmap …))
     1190      [ normalize in ⊢ (??%%); >neutral_l @EQact
     1191      |
     1192      | check nth_opt
     1193 
     1194  cases daemon
     1195  | >rewrite_in_dependent_map
     1196     [2: >get_cost_label_append in ⊢ (??%?); >get_cost_label_of_trace_tind in ⊢ (??%?);
     1197         >append_nil in ⊢ (??%?); % |3:]
     1198     %
     1199   ]
     1200qed.
Note: See TracChangeset for help on using the changeset viewer.