source: src/common/Events.ma @ 748

(* *********************************************************************)
(*                                                                     *)
(*              The Compcert verified compiler                         *)
(*                                                                     *)
(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
(*                                                                     *)
(*  Copyright Institut National de Recherche en Informatique et en     *)
(*  Automatique.  All rights reserved.  This file is distributed       *)
(*  under the terms of the GNU General Public License as published by  *)
(*  the Free Software Foundation, either version 2 of the License, or  *)
(*  (at your option) any later version.  This file is also distributed *)
(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
(*                                                                     *)
(* *********************************************************************)

(* * Representation of observable events and execution traces. *)
(*
Require Import Coqlib.
*)
(*include "AST.ma".*)
(*include "Integers.ma".*)
(*include "Floats.ma".*)
include "common/Values.ma".
include "basics/list.ma".
include "utilities/extralib.ma".
include "common/CostLabel.ma".

(* * 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: Type[0] :=
  | EVint: int -> eventval
  | EVfloat: float -> eventval.

inductive event : Type[0] ≝
  | EVcost: costlabel → event
  | EVextcall: ∀ev_name: ident. ∀ev_args: list eventval. ∀ev_res: eventval. event.

(* * 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 Echarge : costlabel → trace ≝
λlabel. EVcost label :: (nil ?).

definition Eextcall : ident → list eventval → eventval → trace ≝
             λname: ident. λargs: list eventval. λres: eventval.
  EVextcall name args res :: (nil ?).

definition Eapp : trace → trace → trace ≝ λt1,t2. t1 @ t2.

coinductive traceinf : Type[0] :=
  | Econsinf: event -> traceinf -> traceinf.

let rec Eappinf (t: trace) (T: traceinf) on t : traceinf :=
  match t with
  [ nil => T
  | cons ev t' => Econsinf ev (Eappinf t' T)
  ].

(* * Concatenation of traces is written [**] in the finite case
  or [***] in the infinite case. *)

notation "hvbox(l1 break ⧺ l2)"
  right associative with precedence 47
  for @{'doubleplus $l1 $l2 }.

notation "hvbox(l1 break ⧻ l2)"
  right associative with precedence 47
  for @{'tripleplus $l1 $l2 }.

interpretation "trace concatenation" 'doubleplus l1 l2 = (Eapp l1 l2).
interpretation "infinite trace concatenation" 'tripleplus l1 l2 = (Eappinf l1 l2).
(*
Infix "**" := Eapp (at level 60, right associativity).
Infix "***" := Eappinf (at level 60, right associativity).
*)
lemma E0_left: ∀t. E0 ⧺ t = t.
//; qed.

lemma E0_right: ∀t. t ⧺ E0 = t.
@append_nil qed.

lemma Eapp_assoc: ∀t1,t2,t3. (t1 ⧺ t2) ⧺ t3 = t1 ⧺ (t2 ⧺ t3).
@associative_append qed.

lemma Eapp_E0_inv: ∀t1,t2. t1 ⧺ t2 = E0 → t1 = E0 ∧ t2 = E0.
@nil_append_nil_both qed.
  
lemma E0_left_inf: ∀T. E0 ⧻ T = T.
//; qed. 

lemma Eappinf_assoc: ∀t1,t2,T. (t1 ⧺ t2) ⧻ T = t1 ⧻ (t2 ⧻ T).
#t1 elim t1; #t2 #T normalize; //; qed.

(*
Hint Rewrite E0_left E0_right Eapp_assoc
             E0_left_inf Eappinf_assoc: trace_rewrite.

Opaque trace E0 Eextcall Eapp Eappinf.

(** The following [traceEq] tactic proves equalities between traces
  or infinite traces. *)

Ltac substTraceHyp :=
  match goal with
  | [ H: (@eq trace ?x ?y) |- _ ] =>
       subst x || clear H
  end.

Ltac decomposeTraceEq :=
  match goal with
  | [ |- (_ ** _) = (_ ** _) ] =>
      apply (f_equal2 Eapp); auto; decomposeTraceEq
  | _ =>
      auto
  end.

Ltac traceEq := 
  repeat substTraceHyp; autorewrite with trace_rewrite; decomposeTraceEq.
*)

(* Ported from CompCert 1.7.1 >>> *)

(* * An alternate presentation of infinite traces as
  infinite concatenations of nonempty finite traces. *)

coinductive traceinf': Type[0] ≝
  | Econsinf': ∀t: trace. ∀T: traceinf'. t ≠ E0 → traceinf'.

definition split_traceinf' : ∀t:trace. traceinf' → t ≠ E0 → event × traceinf' ≝
λt,T.
  match t return λt0.t0 ≠ E0 → ? with
  [ nil ⇒ ?
  | cons e t' ⇒ λ_.
     (match t' return λt0. t' = t0 → ? with 
     [ nil ⇒ λ_.〈e, T〉
     | cons e' t'' ⇒ λE.〈e, Econsinf' t' T ?〉
     ]) (refl ? t')
  ].
[ *; #NE @False_rect_Type0 @NE @refl
| % #E' >E' in E #E whd in E:(??%%); destruct (E);
] qed.

let corec traceinf_of_traceinf' (T': traceinf') : traceinf ≝
  match T' with
  [ Econsinf' t T'' NOTEMPTY ⇒
      match split_traceinf' t T'' NOTEMPTY with [ pair e tl ⇒
      Econsinf e (traceinf_of_traceinf' tl) ]
  ].

lemma unroll_traceinf':
  ∀T. T = match T with [ Econsinf' t T' NE ⇒ Econsinf' t T' NE ].
#T cases T; //; qed.

lemma unroll_traceinf:
  ∀T. T = match T with [ Econsinf t T' ⇒ Econsinf t T' ].
#T cases T #ev #tr @refl (* XXX //; *)
qed.

lemma traceinf_traceinfp_app:
  ∀t,T,NE.
  traceinf_of_traceinf' (Econsinf' t T NE) = t ⧻ traceinf_of_traceinf' T.
#t elim t;
[ #T #NE cases NE; #NE' @False_ind @NE' @refl
| #h #t' cases t'; [ 2: #h' #t'' ] #IH #T #NE
    >(unroll_traceinf (traceinf_of_traceinf' ?))
    whd in ⊢ (??%?); //; >(IH …) @refl
] qed.

(* <<< *)

(* * 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:
      ∀i. eventval_match (EVint i) ASTint (Vint i)
  | ev_match_float:
      ∀f. eventval_match (EVfloat f) ASTfloat (Vfloat f).

inductive eventval_list_match: list eventval -> list typ -> list val -> Prop :=
  | evl_match_nil:
      eventval_list_match (nil ?) (nil ?) (nil ?)
  | evl_match_cons:
      ∀ev1,evl,ty1,tyl,v1,vl.
      eventval_match ev1 ty1 v1 ->
      eventval_list_match evl tyl vl ->
      eventval_list_match (ev1::evl) (ty1::tyl) (v1::vl).

inductive event_match:
         external_function -> list val -> trace -> val -> Prop :=
  event_match_intro:
    ∀ef,vargs,vres,eargs,eres.
    eventval_list_match eargs (sig_args (ef_sig ef)) vargs ->
    eventval_match eres (proj_sig_res (ef_sig ef)) vres ->
    event_match ef vargs (Eextcall (ef_id ef) 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.

Variable f: meminj.

Remark eventval_match_inject:
  forall ev ty v1,  eventval_match ev ty v1 ->
  forall v2, val_inject f v1 v2 ->
  eventval_match ev ty v2.
Proof.
  induction 1; intros; inversion H; constructor.
Qed.

Remark eventval_list_match_inject:
  forall evl tyl vl1,  eventval_list_match evl tyl vl1 ->
  forall vl2, val_list_inject f vl1 vl2 ->
  eventval_list_match evl tyl vl2.
Proof.
  induction 1; intros.
  inversion H; constructor. 
  inversion H1; constructor. 
  eapply eventval_match_inject; eauto.
  eauto.
Qed.

Lemma event_match_inject:
  forall ef args1 t res args2,
  event_match ef args1 t res ->
  val_list_inject f args1 args2 ->
  event_match ef args2 t res /\ val_inject f res res.
Proof.
  intros. inversion H; subst. 
  split. constructor. eapply eventval_list_match_inject; eauto. auto.
  inversion H2; constructor.
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.

(** Bisimilarity between infinite traces. *)

CoInductive traceinf_sim: traceinf -> traceinf -> Prop :=
  | traceinf_sim_cons: forall e T1 T2,
      traceinf_sim T1 T2 ->
      traceinf_sim (Econsinf e T1) (Econsinf e T2).

Lemma traceinf_sim_refl:
  forall T, traceinf_sim T T.
Proof.
  cofix COINDHYP; intros.
  destruct T. constructor. apply COINDHYP.
Qed.
 
Lemma traceinf_sim_sym:
  forall T1 T2, traceinf_sim T1 T2 -> traceinf_sim T2 T1.
Proof.
  cofix COINDHYP; intros. inv H; constructor; auto.
Qed.

Lemma traceinf_sim_trans:
  forall T1 T2 T3, 
  traceinf_sim T1 T2 -> traceinf_sim T2 T3 -> traceinf_sim T1 T3.
Proof.
  cofix COINDHYP;intros. inv H; inv H0; constructor; eauto.
Qed.

(** The "is prefix of" relation between a finite and an infinite trace. *)

Inductive traceinf_prefix: trace -> traceinf -> Prop :=
  | traceinf_prefix_nil: forall T,
      traceinf_prefix nil T
  | traceinf_prefix_cons: forall e t1 T2,
      traceinf_prefix t1 T2 ->
      traceinf_prefix (e :: t1) (Econsinf e T2).

(*
Lemma traceinf_prefix_compat:
  forall T1 T2 T1' T2',
  traceinf_prefix T1 T2 -> traceinf_sim T1 T1' -> traceinf_sim T2 T2' ->
  traceinf_prefix T1' T2'.
Proof.
  cofix COINDHYP; intros.
  inv H; inv H0; inv H1; constructor; eapply COINDHYP; eauto.
Qed.

Transparent trace E0 Eapp Eappinf.
*)

Lemma traceinf_prefix_app:
  forall t1 T2 t,
  traceinf_prefix t1 T2 ->
  traceinf_prefix (t ** t1) (t *** T2).
Proof.
  induction t; simpl; intros. auto.
  change ((a :: t) ** t1) with (a :: (t ** t1)).
  change ((a :: t) *** T2) with (Econsinf a (t *** T2)).
  constructor. auto.
Qed.

*)