Changeset 3498

Timestamp:

Sep 25, 2014, 3:49:58 PM (6 years ago)

Author:

sacerdot

Message:

Much nicer statement.

File:

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

LTS/Vm.ma

@@ -1 @@
- include "costs.ma".
+include "costs.ma".
 include "basics/lists/list.ma".
 include "../src/utilities/option.ma".
@@ -876 +876 @@
 qed.
 
-check labels_pc
-
 lemma i_act_in_map :  ∀p,prog,iact,l1,l2.
 mem ? 〈a_non_functional_label iact,O〉 (labels_pc p prog l1 l2 iact O).
@@ -885 +883 @@
 qed.
 
-lemma static_dynamic : ∀p,p',prog.
-∀abs_t : abstract_transition_sys (m … p').∀instr_m : (AssemblerInstr p) → abs_instr … abs_t.
-∀good : static_galois … (asm_static_analisys_data p p' prog abs_t 
+notation "〚 term 19 C 〛 term 90 A" with precedence 10 for @{ 'sem $C $A }.
+interpretation "act_abs" 'sem f x = (act ?? (act_abs ??) f x).
+
+coercion big_op : ∀M:monoid. ∀l: list M. M ≝ big_op on _l: list ? to ?.
+
+lemma static_dynamic :
+(* Given an assembly program *)
+∀p,p',prog.
+
+(* Given a Galois connection to an abstract transition system *)
+∀abs_t : abstract_transition_sys (m … p').
+∀instr_m : (AssemblerInstr p) → abs_instr … abs_t.
+∀R : static_galois … (asm_static_analisys_data … prog …
  (λi.match i with [None ⇒ e … 
                   |Some x ⇒ instr_m x
-                  ])) .∀mT,map1.
-∀EQmap : static_analisys p ? instr_m mT prog = return map1.
-∀st1,st2 : vm_ass_state p p'.
-∀t : raw_trace (asm_operational_semantics p p' prog) … st1 st2.
-terminated_trace … t → 
-∀k.
-pre_measurable_trace … t → 
-block_cost p prog … instr_m (get_pc … st1 (endmain … prog)) (S (|(instructions … prog)|)) = return k → 
-∀a1.rel_galois … good st1 a1 → 
-∀labels.
-labels = dependent_map CostLabel ? (chop … (get_costlabels_of_trace …  t)) (λlbl,prf.(opt_safe … (get_map … map1 lbl) ?)) →
-rel_galois … good st2 (act_abs … abs_t (big_op … labels) (act_abs … abs_t k a1)).
+                  ])).
+
+(* If the static analysis does not fail *)
+∀mT,map1. ∀EQmap : static_analisys … instr_m mT prog = return map1.
+
+(* For every pre_measurable, terminated trace *)
+∀st1,st2. ∀t: raw_trace (asm_operational_semantics … prog) … st1 st2.
+ terminated_trace … t → pre_measurable_trace … t → 
+
+(* Let k be the statically computed abstract action of the prefix of the trace
+   up to the first label *)
+∀k.block_cost p prog … instr_m (get_pc … st1 (endmain … prog)) (S (|(instructions … prog)|)) = return k →
+
+(* Given an abstract state in relation with the first state of the trace *)
+∀a1.R st1 a1 →
+
+(* Let labels be the costlabels observed in the trace, excluding the last one *)
+let labels ≝ chop … (get_costlabels_of_trace …  t) in
+
+(* Let abs_actions be the list of statically computed abstract actions
+   associated to each label in labels. *)
+∀abs_actions.
+ abs_actions =
+  dependent_map … labels (λlbl,prf.(opt_safe … (get_map … map1 lbl) …)) →
+
+(* The final state of the trace is in relation with the one obtained by
+   first applying k to a1, and then applying every semantics in abs_trace. *) 
+R st2 (〚abs_actions〛 (〚k〛 a1)).
+
 [2: @hide_prf 
     cases(mem_map ????? (labels_of_trace_are_in_code … (chop_mem … prf))) *
@@ -914 +939 @@
 ]   
 lapply Hlabelled lapply prf1 -prf1 lapply l1 -l1 elim t1 -st3
-[ * [3: #st] #l #prf #H1 #k #_ whd in ⊢ (??%? → ?);
+[ * [3: #st] #l #prf #H1 #_ #k whd in ⊢ (??%? → ?);
   [3: cases prf
   |2: whd in ⊢ (??%% → ?); #EQ destruct #a1 #rel_fin #labels whd in ⊢ (??%% → ?);
       lapply(instr_map_ok … good … prf … rel_fin) [ %|] cases st2 in prf; -st2 [3: #st2] *
       #EQpc #EQ destruct #H #EQ destruct >act_neutral >act_neutral normalize in H;
-      <(act_neutral ?? (act_abs ? abs_t) a1) @H
+      <(act_neutral … (act_abs …) a1) @H
   | @eqb_elim normalize nodelta
     [ #EQpc whd in ⊢(??%% → ?); #EQ destruct #a1 #good_st_a1 #labels whd in ⊢ (??%% → ?);
@@ -974 +999 @@
     ]
   ]
-  #st3 #exe_st1_st3 #tl #IH #l1 #exe_st4_st2 #l1_lab #k #pre_meas whd in ⊢ (??%? → ?); 
+  #st3 #exe_st1_st3 #tl #IH #l1 #exe_st4_st2 #l1_lab #pre_meas #k whd in ⊢ (??%? → ?); 
   >rewrite_in_dependent_map [2,5: @get_cost_label_of_trace_tind |3,6: ]
   >dependent_map_append