Changeset 2202

Timestamp:

Jul 17, 2012, 6:57:39 PM (6 years ago)

Author:

campbell

Message:

Start defining equivalent executions.

Location:

src

Files:

• Clight/labelSimulation.ma (modified) (8 diffs)
• Clight/labelSpecification.ma (modified) (5 diffs)
• common/Executions.ma (added)
• common/SmallstepExec.ma (modified) (1 diff)

src/Clight/labelSimulation.ma

@@ -1189 +1189 @@
 
 lemma not_wrong_init : ∀p.
-  not_wrong (exec_inf … clight_fullexec p) →
+  not_wrong state (exec_inf … clight_fullexec p) →
   ∃s. make_initial_state … p = OK ? s.
-#p whd in ⊢ (?% → ?); change with (make_initial_state p) in match (make_initial_state ??? p);
+#p whd in ⊢ (??% → ?); change with (make_initial_state p) in match (make_initial_state ??? p);
 cases (make_initial_state p)
 [ /2/
@@ -1225 +1225 @@
   plus ge s tr s' →
   is_final s' = None ? →
-  steps tr (exec_inf_aux … clight_fullexec ge (exec_step ge s))
-           (exec_inf_aux … clight_fullexec ge (exec_step ge s')).
+  steps state tr
+    (exec_inf_aux … clight_fullexec ge (exec_step ge s))
+    (exec_inf_aux … clight_fullexec ge (exec_step ge s')).
 #ge #s0 #tr0 #s0' #P elim P
 [ #s1 #tr #s2 #EX #NF >EX >exec_inf_aux_unfold
-  whd in ⊢ (??%?);
+  whd in ⊢ (???%?);
   whd in match (is_final ?????); >NF
   %2
 | #s1 #tr #s2 #tr' #s3 #EX1 #P2 #IH #NF
   >exec_inf_aux_unfold >EX1
-  whd in ⊢ (??%?);
+  whd in ⊢ (???%?);
   whd in match (is_final ?????); >(plus_not_final … P2)
   %3 @IH //
@@ -1242 +1243 @@
   plus ge s tr s' →
   is_final s' = Some ? r →
-  ∃tr'. steps tr (exec_inf_aux … clight_fullexec ge (exec_step ge s))
-                 (e_stop … tr' r s').
+  ∃tr'. steps state tr
+          (exec_inf_aux … clight_fullexec ge (exec_step ge s))
+          (e_stop … tr' r s').
 #ge #s0 #tr0 #s0' #r #P elim P
 [ #s1 #tr #s2 #EX #F >EX >exec_inf_aux_unfold
-  %{tr} whd in ⊢ (??%?);
+  %{tr} whd in ⊢ (???%?);
   whd in match (is_final ?????); >F
   %1
@@ -1253 +1255 @@
   #tr' #S' %{tr'}
   >exec_inf_aux_unfold >EX1
-  whd in ⊢ (??%?);
+  whd in ⊢ (???%?);
   whd in match (is_final ?????); >(plus_not_final … P2)
   %3 @S'
@@ -1263 +1265 @@
   (s1,s2:state)
   (S:state_with_labels s1 s2)
-  (NW:not_wrong (exec_inf_aux … clight_fullexec ge1 (exec_step ge1 s1)))
+  (NW:not_wrong state (exec_inf_aux … clight_fullexec ge1 (exec_step ge1 s1)))
 : sim_with_labels (exec_inf_aux … clight_fullexec ge1 (exec_step ge1 s1)) (exec_inf_aux … clight_fullexec ge2 (exec_step ge2 s2)) ≝ 
 match NW return λe,NW. exec_inf_aux … clight_fullexec ?? = e → sim_with_labels e ? with
@@ -1299 +1301 @@
   #i cases (H2 i) #tr1 * #s1' * #K1 * #tr2 * #s2' * * #K2 #TR #S'
   lapply (NWk i)
-  @(match sym_eq … K1 with [refl ⇒ ?]) @(match sym_eq … (exec_inf_aux_unfold …) with [refl ⇒ ?]) whd in ⊢ (?% → ?%%); whd in match (is_final ?????); @(match sym_eq … (final_related … S') with [refl ⇒ ?])
+  @(match sym_eq … K1 with [refl ⇒ ?]) @(match sym_eq … (exec_inf_aux_unfold …) with [refl ⇒ ?]) whd in ⊢ (??% → ?%%); whd in match (is_final ?????); @(match sym_eq … (final_related … S') with [refl ⇒ ?])
   @(match sym_eq … K2 with [refl ⇒ ?]) @(match sym_eq … (exec_inf_aux_unfold ?? clight_fullexec ge2 …) with [refl ⇒ ?]) whd in ⊢ (? → ??%); whd in match (is_final ?????);
   cases (is_final s2')
-  [ whd in ⊢ (?% → ?%%); #NW' @(swl_steps … (steps_step …)) // @build_exec //
+  [ whd in ⊢ (??% → ?%%); #NW' @(swl_steps … (steps_step …)) // @build_exec //
     inversion NW'
     [ #H1 #H2 #H3 #H4 #H5 destruct
@@ -1308 +1310 @@
     | #H14 #H15 #H16 #H17 #H18 destruct
     ]
-  | #r whd in ⊢ (?% → ?%%); #NW' @(swl_stop … (steps_stop …)) //
+  | #r whd in ⊢ (??% → ?%%); #NW' @(swl_stop … (steps_stop …)) //
   ]
 ] qed.
@@ -1343 +1345 @@
 >I2
 
-whd in ⊢ (?% → ? → ?%%);
+whd in ⊢ (??% → ? → ?%%);
 >exec_inf_aux_unfold
 >exec_inf_aux_unfold
-whd in ⊢ (?% → ? → ?%%);
+whd in ⊢ (??% → ? → ?%%);
 whd in match (is_final ?????);
 >(initial_state_is_not_final … I1)
 whd in match (is_final ?????);
 >(initial_state_is_not_final … I2)
-whd in ⊢ (?% → ? → ?%%);
+whd in ⊢ (??% → ? → ?%%);
 
 #NW #S

src/Clight/labelSpecification.ma

@@ -1 +1 @@
 include "Clight/Cexec.ma".
 include "Clight/label.ma".
+include "common/Executions.ma".
 
 (* Formalise the notion of a trace with extra cost labels added.  Note that
@@ -9 +10 @@
 | twel_new : ∀c,t1,t2. trace_with_extra_labels t1 t2 → trace_with_extra_labels t1 (EVcost c::t2).
 
-(* A finite trace is produced by some prefix of an execution. *)
-
-inductive steps : trace → execution state io_out io_in → execution state io_out io_in → Prop ≝
-| steps_stop : ∀tr,s,r. steps tr (e_stop … tr s r) (e_stop … tr s r)
-| steps_step : ∀tr,s,e. steps tr (e_step … tr s e) e
-| steps_steps : ∀tr,s,e,tr',e'. steps tr e e' → steps (tr'⧺tr) (e_step … tr' s e) e'.
-
 (* One execution is simulated by another, but possibly using more steps and
    introducing some cost labels. *)
@@ -21 +15 @@
 coinductive sim_with_labels : execution state io_out io_in → execution state io_out io_in → Prop ≝
 | swl_stop : ∀tr1,tr2,tr2',r,s1,s2,e2.
-    steps tr2 e2 (e_stop … tr2' r s2) →
+    steps state tr2 e2 (e_stop … tr2' r s2) →
     trace_with_extra_labels tr1 tr2 →
     sim_with_labels (e_stop … tr1 r s1) e2
 | swl_steps : ∀tr1,tr2,s1,e1,e2,e2'.
-    steps tr2 e2 e2' →
+    steps state tr2 e2 e2' →
     trace_with_extra_labels tr1 tr2 →
     sim_with_labels e1 e2' →
@@ -33 +27 @@
     sim_with_labels (e_interact … o k1) (e_interact … o k2).
 
-(* We do not consider wrong executions. *)
-
-coinductive not_wrong : execution state io_out io_in → Prop ≝
-| nw_stop : ∀tr,i,s. not_wrong (e_stop … tr i s)
-| nw_step : ∀tr,s,e. not_wrong e → not_wrong (e_step … tr s e)
-| nw_interact : ∀o,k. (∀i. not_wrong (k i)) → not_wrong (e_interact … o k).
-
 (* Desired result *)
 
@@ -46 +33 @@
   let e1 ≝ exec_inf … clight_fullexec p in
   let e2 ≝ exec_inf … clight_fullexec (clight_label p) in
-  not_wrong e1 →
+  not_wrong state e1 →
   sim_with_labels e1 e2.

src/common/SmallstepExec.ma

@@ -155 +155 @@
   ].
 
-(* Some preliminary simulation stuff that's not been used yet.
-record execstep' (outty:Type[0]) (inty:outty → Type[0]) : Type[1] ≝
-{ es0 :> execstep outty inty
-; initial : state ?? es0 → Prop
-}.
 
-
-alias symbol "and" (instance 2) = "logical and".
-record related_semantics : Type[1] ≝
-{ output : Type[0]
-; input : output → Type[0]
-; sem1 : execstep' output input
-; sem2 : execstep' output input
-; ge1 : genv ?? sem1
-; ge2 : genv ?? sem2
-; match_states : state ?? sem1 → state ?? sem2 → Prop
-; match_initial_states : ∀st1. (initial ?? sem1) st1 → ∃st2. (initial ?? sem2) st2 ∧ match_states st1 st2
-; match_final_states : ∀st1,st2,r. match_states st1 st2 → (is_final ?? sem1) st1 = Some ? r → (is_final ?? sem2) st2 = Some ? r
-}.
-
-
-
-record simulation : Type[1] ≝ 
-{ sems :> related_semantics
-; sim : ∀st1,st2,t,st1'.
-        P_io' ?? (trace × (state ?? (sem1 sems))) (λr. r = 〈t,st1'〉) (step ?? (sem1 sems) (ge1 sems) st1) →
-        match_states sems st1 st2 → 
-        ∃st2':(state ?? (sem2 sems)).(∃n:nat.P_io' ?? (trace × (state ?? (sem2 sems))) (λr. r = 〈t,st2'〉) (repeat n ?? (sem2 sems) (ge2 sems) st2)) ∧
-          match_states sems st1' st2'
-}.
-*)