Changeset 3503

Timestamp:

Sep 26, 2014, 2:40:35 PM (5 years ago)

Author:

piccolo

Message:

 

File:

• LTS/Vm.ma (modified) (4 diffs)

LTS/Vm.ma

@@ -1103 +1103 @@
 
 definition measurable :
- ∀S: abstract_status. ∀s1,s2,s4 : S. raw_trace … s1 s4 → Prop ≝ 
-λS,s1,s2,s4,t.
+ ∀S: abstract_status. ∀si,s1,s3,sn : S. raw_trace … si sn → Prop ≝ 
+λS,si,s1,s3,sn,t.
  pre_measurable_trace … t ∧
- ∃s3:S. ∃t' : raw_trace … s2 s3. ∃l1,l2,prf1,prf2.
-  t = t_ind ? s1 s2 s4 l1 prf1 … (t' @ (t_ind ? s3 s4 s4 l2 prf2 … (t_base … s4)))
- ∧ is_costlabelled_act l1 ∧ is_costlabelled_act l2.
-
+ ∃s0,s2:S. ∃ti0 : raw_trace … si s0.∃t12 : raw_trace … s1 s2.∃t3n : raw_trace … s3 sn.
+ ∃l1,l2,prf1,prf2.
+  t = ti0 @  t_ind ? s0 s1 sn l1 prf1 … (t12 @ (t_ind ? s2 s3 sn l2 prf2 … t3n))
+ ∧ is_costlabelled_act l1 ∧ is_costlabelled_act l2 ∧ silent_trace … ti0 ∧ silent_trace … t3n.
+ 
+lemma chop_cons : ∀A : Type[0].∀x : A.∀xs: list A. xs ≠ [ ] → chop … (x :: xs) = x :: (chop … xs).
+#A #x * [ #H cases(absurd ?? H) % ] // qed.
+ 
 (*
 lemma measurable_terminated:
@@ -1117 +1121 @@
 qed. *)
 
+lemma execute_mem_label_pc :∀p,p',prog.∀st0,st1 :vm_state p p'.∀l1,c1.
+actionlabel_to_costlabel l1 = [c1] → 
+vmstep p p' prog l1 st0 st1 → 
+ mem … 〈c1,pc p p' st1〉
+  (labels_pc … (instructions … prog) (call_label_fun … prog)
+   (return_label_fun … prog) (in_act … prog) O).
 theorem static_dynamic :
 (* Given an assembly program *)
@@ -1129 +1139 @@
 (* For every measurable trace whose second state is st1 or, equivalently,
    whose first state after the initial labelled transition is st1 *)
-∀st0,st1,stn. ∀t: raw_trace (asm_operational_semantics … prog) … st0 stn.
- measurable … st1 … t →
+∀si,s1,s2,sn. ∀t: raw_trace (asm_operational_semantics … prog) … si sn.
+ measurable … s1 s2 … t →
 
 (* Let labels be the costlabels observed in the trace (last one excluded) *)
@@ -1142 +1152 @@
 
 (* Given an abstract state in relation with the second state of the trace *)
-∀a1.R st1 a1 →
+∀a1.R s1 a1 →
 
 (* The final state of the trace is in relation with the one obtained by
    applying every semantics in abs_trace. *) 
-R stn (〚abs_actions〛 a1).
-[2: @hide_prf cases daemon
-| #p #p' #prog #R #mT #map1 #EQmap #st0 #st1 #stn #t #measurable
-  cases measurable #premeas * #st3 * #t' * #l1 * #l2 * #prf1 * #prf2 ** #EQ destruct
-  #Hl1 #Hl2 #acts #EQacts #a1 #HR
-  cut (∃act.∃actstl. acts = act::actstl)
-  [ cases daemon (* usare measurable *) ]
-  * #act * #actstl #EQacts2 >EQacts2
-  cut (〚act::actstl〛 a1 = (〚actstl〛 (〚act〛 a1)))
-  [ cases daemon (* true *) ]
-  #EQ >EQ -EQ >EQacts2 in EQacts; #EQacts
-  @(static_dynamic_inv … EQmap … (t' @ t_ind … prf2 (t_base …)) … actstl … HR)
+R s2 (〚abs_actions〛 a1).
+[2: @hide_prf 
+    cases(mem_map ????? (labels_of_trace_are_in_code … (chop_mem … prf))) *
+    #lbl' #pc * #Hmem #EQ destruct    
+    >(proj1 … (static_analisys_ok … EQmap … Hmem))
+    @(proj2 … (static_analisys_ok … EQmap … Hmem))
+]
+#p #p' #prog #R #mT #map1 #EQmap #si #s1 #s2 #sn #t #measurable
+cases measurable #premeas * #s0 * #s3 * #ti0 * #t12 * #t3n *  #l1 * #l2 * #prf1 * #prf2 
+**** #EQ destruct #Hl1 #Hl2 #silent_ti0 #silent_t3n #acts cases(actionlabel_ok … Hl1)
+#c1 #EQc1 >rewrite_in_dependent_map
+[2: >get_cost_label_append in ⊢ (??%?); >(get_cost_label_silent_is_empty … silent_ti0) in ⊢ (??%?);
+     >get_cost_label_of_trace_tind in ⊢ (??%?); >get_cost_label_append in ⊢ (??%?);
+      >get_cost_label_of_trace_tind in ⊢ (??%?);
+     >(get_cost_label_silent_is_empty … silent_t3n) in ⊢ (??%?);
+     >append_nil in ⊢ (??%?); >EQc1 in ⊢ (??%?); whd in ⊢ (??(??%)?);
+     whd in ⊢ (??(??(???%))?); >chop_cons in ⊢ (??%?); [2: cases daemon] % |3:
+ ]
+ whd in ⊢ (???% → ?); @opt_safe_elim #act #EQact #EQacts2 >EQacts2
+ >(big_op_associative ? [?]) #a1 >act_op #HR
+letin actsl ≝ (dependent_map ????);
+@(static_dynamic_inv … EQmap … (t12 @ t_ind … prf2 (t_base …)) … actsl … HR)
   [ /6 width=6 by conj, ex_intro/
   | cases daemon (* true *)
-  | cases daemon (* true *)
-  | cases daemon (* true *) ]]
-qed.
+  | cases s1 in prf1 t12; [3: #st1] cases s0 [3,6,9: #st0] *
+    [2: #H #EQ lapply(refl ? (FINAL p p')) generalize in match (FINAL p p') in ⊢ (??%? → %);
+        #st' #EQst' #tr lapply prf2 lapply EQst' -EQst' cases tr
+        [ #st'' #EQ2 >EQ2 *
+        | #st'' #st''' #st'''' #l3 #ABS #_ #EQ2 >EQ2 in ABS; *
+        ]
+    | #H1 #H2 #_ whd in match get_pc; normalize nodelta
+      <(proj1 ?? (static_analisys_ok … EQmap …)) 
+      [ normalize in ⊢ (??%%); >neutral_l @EQact
+      |
+      | check nth_opt
+  
+  cases daemon
+  | >rewrite_in_dependent_map
+     [2: >get_cost_label_append in ⊢ (??%?); >get_cost_label_of_trace_tind in ⊢ (??%?);
+         >append_nil in ⊢ (??%?); % |3:]
+     %
+   ]
+qed.