Changeset 3372 for src

Timestamp:

Jul 1, 2013, 4:34:13 PM (7 years ago)

Author:

piccolo

Message:

Added new implementation of labelling approach based on LTS and emmission of costlabels during transitions

File:

• src/ERTL/ERTLToLTLProof.ma (modified) (11 diffs)

src/ERTL/ERTLToLTLProof.ma

@@ -66 +66 @@
      (beloadv m2) (beloadv m3). 
 
+(*
 definition callee_saved_remap :
 (Σb:block.block_region b=Code) → (block → list register) → 
@@ -87 +88 @@
   ]
 ].
+*)
+
 (*
 definition mem_relation : fixpoint_computer → coloured_graph_computer → 
@@ -97 +100 @@
      (λptr1,ptr2.ERTL_validate_pointer … ge f st ptr1 = return it ∧ ptr1 = ptr2) R 
      (beloadv m2) (beloadv m3).
+*)
 
 definition callee_saved_remap : fixpoint_computer → coloured_graph_computer → 
@@ -123 +127 @@
   | None ⇒ d
   ]
-]. *)
-
+].
+
+xxxxxxxxxxxxx
 
 let rec frames_relation_aux (prog : ertl_program) (stacksize : ident → option ℕ)
@@ -520 +525 @@
 qed.*)
 
-
 lemma ps_reg_retrieve_hw_reg_retrieve_commute : 
 ∀prog,stacksize,init,color_f,live_f,color_fun,live_fun.
@@ -1023 +1027 @@
 cases daemon qed.
 
+axiom BadVertexValue : ErrorMessage.
+
 definition ertl_vertex_retrieve :  ertl_reg_env → vertex → res beval ≝ 
-λregs,v.match v with [inl r ⇒ ps_reg_retrieve regs r | inr r ⇒ hw_reg_retrieve regs r ].
-
+λregs,v.match v with 
+[inl r ⇒ ps_reg_retrieve regs r 
+| inr r ⇒ match hwreg_retrieve (\snd regs) r with 
+   [ BVundef ⇒ Error ? [MSG BadVertexValue]
+   | _ ⇒ OK ? (hwreg_retrieve (\snd regs) r)
+   ]
+].
+  
 definition eq_decision : decision → decision → bool ≝ 
 λd1,d2.match d1 with 
@@ -1042 +1054 @@
 qed.
 
+lemma ertl_vertex_retrieve_ok_on_hw_regs : 
+∀regs,r,bv.ertl_vertex_retrieve regs (inr ?? r) = return bv → 
+hwreg_retrieve (\snd regs) r = bv.
+#regs #r #bv whd in match ertl_vertex_retrieve; normalize nodelta
+cases(hwreg_retrieve ??) normalize nodelta
+[|| #x #y #p | #b | #p | #ptr #p | #pc #p ]
+#EQ whd in EQ : (???%); destruct %
+qed.
 
 lemma vertex_retrieve_read_arg_decision_commute : 
@@ -1054 +1074 @@
      (λv,d.
       bool_to_Prop
-        (live_fun fn (point_of_pc ERTL_semantics pc) v) ∧
+        (live_fun fn (point_of_pc ERTL_semantics pc) v) ∧ 
       d = 
       (color_fun fn v))
-     (λbv,bv'.bv = sigma_beval prog stacksize init init_regs f_lbls f_regs bv') …
-     (λst1.ertl_vertex_retrieve (regs … st1)) 
-     (λst,d.m_map Res ?? (\fst …) 
-      (read_arg_decision (joint_if_local_stacksize ?? fn) st d)).
+     (λx,y.\fst x = sigma_beval prog stacksize init init_regs f_lbls f_regs (\fst y) ∧
+            gen_state_rel prog stacksize init color_f live_f color_fun 
+            live_fun init_regs f_lbls f_regs pc (\snd x) (\snd y)) …
+     (λst1,v.! bv ← ertl_vertex_retrieve (regs … st1) v;
+              return〈bv,st1〉) 
+     (λst,d.(read_arg_decision (joint_if_local_stacksize ?? fn) st d)).
 #prog #stacksize #init #color_f #live_f #color_fun #live_fun #init_regs #f_lbls #f_regs
 #f #fn #pc #EQfn #st1 #st2 * 
@@ -1066 +1088 @@
 ** >EQfn whd in ⊢ (??%% → ?); #EQ1 destruct(EQ1) #_ cases(st_frms ??) [*] #frames 
 normalize nodelta ***** #_ #H1 #_ #_ #_ #_ * #live_R #EQ destruct(EQ) #bv #EQbv 
-lapply((proj2 ?? H1 …) R live_R) cases(color_fun ??) normalize nodelta [#n1 | #R1 ]
-whd in EQbv : (??%%); destruct(EQbv)
+lapply((proj2 ?? H1 …) R live_R ?)
+[ % #ABS whd in match ertl_vertex_retrieve in EQbv; normalize nodelta in EQbv;
+  >ABS in EQbv; normalize nodelta whd in ⊢ (???% → ?); #EQ destruct(EQ) ]
+ cases(color_fun ??) normalize nodelta [#n1 | #R1 ] lapply(ertl_vertex_retrieve_ok_on_hw_regs … EQbv)
+ #EQ destruct(EQ)
 [ inversion (hwreg_retrieve_sp ?) normalize nodelta [2: #e #_ *] #sp #EQsp
   inversion(beloadv ??) normalize nodelta [ #_ *] #bv1 #EQbv1 #Hbv1 %{bv1}
@@ -1112 +1137 @@
 qed.
 
+(*
 lemma update_color_lemma : 
 ∀fix_comp,colour,prog,init.
@@ -1178 +1204 @@
      (update_fun ?? eq_vertex (live_fun fn (point_of_pc ERTL_semantics pc)) v new_live))
  init_regs f_lbls f_regs pc st1 st2.
-cases daemon qed.  
+cases daemon qed.  *)
 
 lemma move_preserve :