1 files changed, 109 insertions, 8 deletions

diff --git a/common/Events.v b/common/Events.v
index a0559fd0..e1a4729a 100644
--- a/common/Events.v
+++ b/common/Events.v
@@ -1,4 +1,4 @@
-(** Representation of (traces of) observable events. *)
+(** Representation of observable events and execution traces. *)
 
 Require Import Coqlib.
 Require Import AST.
@@ -6,23 +6,77 @@ Require Import Integers.
 Require Import Floats.
 Require Import Values.
 
+(** The observable behaviour of programs is stated in terms of
+  input/output events, which can also be thought of as system calls 
+  to the operating system.  An event is generated each time an
+  external function (see module AST) is invoked.  The event records
+  the name of the external function, the arguments to the function
+  invocation provided by the program, and the return value provided by
+  the outside world (e.g. the operating system).  Arguments and values
+  are either integers or floating-point numbers.  We currently do not
+  allow pointers to be exchanged between the program and the outside
+  world. *)
+
 Inductive eventval: Set :=
   | EVint: int -> eventval
   | EVfloat: float -> eventval.
 
-Parameter trace: Set.
-Parameter E0: trace.
-Parameter Eextcall: ident -> list eventval -> eventval -> trace.
-Parameter Eapp: trace -> trace -> trace.
+Record event : Set := mkevent {
+  ev_name: ident;
+  ev_args: list eventval;
+  ev_res: eventval
+}.
+
+(** The dynamic semantics for programs collect traces of events.
+  Traces are of two kinds: finite (type [trace]) 
+  or infinite (type [traceinf]). *)
+
+Definition trace := list event.
+
+Definition E0 : trace := nil.
+
+Definition Eextcall
+             (name: ident) (args: list eventval) (res: eventval) : trace :=
+  mkevent name args res :: nil.
+
+Definition Eapp (t1 t2: trace) : trace := t1 ++ t2.
+
+CoInductive traceinf : Set :=
+  | Econsinf: event -> traceinf -> traceinf.
+
+Fixpoint Eappinf (t: trace) (T: traceinf) {struct t} : traceinf :=
+  match t with
+  | nil => T
+  | ev :: t' => Econsinf ev (Eappinf t' T)
+  end.
+
+(** Concatenation of traces is written [**] in the finite case
+  or [***] in the infinite case. *)
 
 Infix "**" := Eapp (at level 60, right associativity).
+Infix "***" := Eappinf (at level 60, right associativity).
 
-Axiom E0_left: forall t, E0 ** t = t.
-Axiom E0_right: forall t, t ** E0 = t.
-Axiom Eapp_assoc: forall t1 t2 t3, (t1 ** t2) ** t3 = t1 ** (t2 ** t3).
+Lemma E0_left: forall t, E0 ** t = t.
+Proof. auto. Qed.
+
+Lemma E0_right: forall t, t ** E0 = t.
+Proof. intros. unfold E0, Eapp. rewrite <- app_nil_end. auto. Qed.
+
+Lemma Eapp_assoc: forall t1 t2 t3, (t1 ** t2) ** t3 = t1 ** (t2 ** t3).
+Proof. intros. unfold Eapp, trace. apply app_ass. Qed.
+
+Lemma Eappinf_assoc: forall t1 t2 T, (t1 ** t2) *** T = t1 *** (t2 *** T).
+Proof.
+  induction t1; intros; simpl. auto. decEq; auto.
+Qed.
 
 Hint Rewrite E0_left E0_right Eapp_assoc: trace_rewrite.
 
+Opaque trace E0 Eextcall Eapp.
+
+(** The following [traceEq] tactic proves equalities between traces
+  or infinite traces. *)
+
 Ltac substTraceHyp :=
   match goal with
   | [ H: (@eq trace ?x ?y) |- _ ] =>
@@ -40,6 +94,11 @@ Ltac decomposeTraceEq :=
 Ltac traceEq := 
   repeat substTraceHyp; autorewrite with trace_rewrite; decomposeTraceEq.
 
+(** The predicate [event_match ef vargs t vres] expresses that
+  the event [t] is generated when invoking external function [ef]
+  with arguments [vargs], and obtaining [vres] as a return value
+  from the operating system. *)
+
 Inductive eventval_match: eventval -> typ -> val -> Prop :=
   | ev_match_int:
       forall i, eventval_match (EVint i) Tint (Vint i)
@@ -63,6 +122,10 @@ Inductive event_match:
     eventval_match eres (proj_sig_res ef.(ef_sig)) vres ->
     event_match ef vargs (Eextcall ef.(ef_id) eargs eres) vres.
 
+(** The following section shows that [event_match] is stable under
+  relocation of pointer values, as performed by memory injections
+  (see module [Mem]). *)
+
 Require Import Mem.
 
 Section EVENT_MATCH_INJECT.
@@ -101,3 +164,41 @@ Proof.
 Qed.
 
 End EVENT_MATCH_INJECT.
+
+(** The following section shows that [event_match] is stable under
+  replacement of [Vundef] values by more defined values. *)
+
+Section EVENT_MATCH_LESSDEF.
+
+Remark eventval_match_lessdef:
+  forall ev ty v1,  eventval_match ev ty v1 ->
+  forall v2, Val.lessdef v1 v2 ->
+  eventval_match ev ty v2.
+Proof.
+  induction 1; intros; inv H; constructor.
+Qed.
+
+Remark eventval_list_match_moredef:
+  forall evl tyl vl1, eventval_list_match evl tyl vl1 ->
+  forall vl2, Val.lessdef_list vl1 vl2 ->
+  eventval_list_match evl tyl vl2.
+Proof.
+  induction 1; intros.
+  inversion H; constructor. 
+  inversion H1; constructor. 
+  eapply eventval_match_lessdef; eauto.
+  eauto.
+Qed.
+
+Lemma event_match_lessdef:
+  forall ef args1 t res1 args2,
+  event_match ef args1 t res1 ->
+  Val.lessdef_list args1 args2 ->
+  exists res2, event_match ef args2 t res2 /\ Val.lessdef res1 res2.
+Proof.
+  intros. inversion H; subst. exists res1; split. 
+  constructor. eapply eventval_list_match_moredef; eauto. auto.
+  auto.
+Qed.
+
+End EVENT_MATCH_LESSDEF.