source: C-semantics/Events.ma @ 3

Last change on this file since 3 was 3, checked in by campbell, 10 years ago

Import work-in-progress port of the CompCert? C semantics to matita.

File size: 9.0 KB
Line 
1(* *********************************************************************)
2(*                                                                     *)
3(*              The Compcert verified compiler                         *)
4(*                                                                     *)
5(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
6(*                                                                     *)
7(*  Copyright Institut National de Recherche en Informatique et en     *)
8(*  Automatique.  All rights reserved.  This file is distributed       *)
9(*  under the terms of the GNU General Public License as published by  *)
10(*  the Free Software Foundation, either version 2 of the License, or  *)
11(*  (at your option) any later version.  This file is also distributed *)
12(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
13(*                                                                     *)
14(* *********************************************************************)
15
16(* * Representation of observable events and execution traces. *)
17(*
18Require Import Coqlib.
19*)
20include "AST.ma".
21include "Integers.ma".
22include "Floats.ma".
23include "Values.ma".
24include "datatypes/list.ma".
25include "extralib.ma".
26
27(* * The observable behaviour of programs is stated in terms of
28  input/output events, which can also be thought of as system calls
29  to the operating system.  An event is generated each time an
30  external function (see module AST) is invoked.  The event records
31  the name of the external function, the arguments to the function
32  invocation provided by the program, and the return value provided by
33  the outside world (e.g. the operating system).  Arguments and values
34  are either integers or floating-point numbers.  We currently do not
35  allow pointers to be exchanged between the program and the outside
36  world. *)
37
38ninductive eventval: Type :=
39  | EVint: int -> eventval
40  | EVfloat: float -> eventval.
41
42nrecord event : Type := {
43  ev_name: ident;
44  ev_args: list eventval;
45  ev_res: eventval
46}.
47
48(* * The dynamic semantics for programs collect traces of events.
49  Traces are of two kinds: finite (type [trace]) or infinite (type [traceinf]). *)
50
51ndefinition trace := list event.
52
53ndefinition E0 : trace := nil ?.
54
55ndefinition Eextcall : ident → list eventval → eventval → trace ≝
56             λname: ident. λargs: list eventval. λres: eventval.
57  mk_event name args res :: (nil ?).
58
59ndefinition Eapp : trace → trace → trace ≝ λt1,t2. t1 @ t2.
60
61ncoinductive traceinf : Type :=
62  | Econsinf: event -> traceinf -> traceinf.
63
64nlet rec Eappinf (t: trace) (T: traceinf) on t : traceinf :=
65  match t with
66  [ nil => T
67  | cons ev t' => Econsinf ev (Eappinf t' T)
68  ].
69
70(* * Concatenation of traces is written [**] in the finite case
71  or [***] in the infinite case. *)
72
73notation "hvbox(l1 break ⧺ l2)"
74  right associative with precedence 47
75  for @{'doubleplus $l1 $l2 }.
76
77notation "hvbox(l1 break ⧻ l2)"
78  right associative with precedence 47
79  for @{'tripleplus $l1 $l2 }.
80
81interpretation "trace concatenation" 'doubleplus l1 l2 = (Eapp l1 l2).
82interpretation "infinite trace concatenation" 'tripleplus l1 l2 = (Eappinf l1 l2).
83(*
84Infix "**" := Eapp (at level 60, right associativity).
85Infix "***" := Eappinf (at level 60, right associativity).
86*)
87nlemma E0_left: ∀t. E0 ⧺ t = t.
88//; nqed.
89
90nlemma E0_right: ∀t. t ⧺ E0 = t.
91napply append_nil; nqed.
92
93nlemma Eapp_assoc: ∀t1,t2,t3. (t1 ⧺ t2) ⧺ t3 = t1 ⧺ (t2 ⧺ t3).
94napply associative_append; nqed.
95
96nlemma Eapp_E0_inv: ∀t1,t2. t1 ⧺ t2 = E0 → t1 = E0 ∧ t2 = E0.
97napply nil_append_nil_both; nqed.
98 
99nlemma E0_left_inf: ∀T. E0 ⧻ T = T.
100//; nqed.
101
102nlemma Eappinf_assoc: ∀t1,t2,T. (t1 ⧺ t2) ⧻ T = t1 ⧻ (t2 ⧻ T).
103#t1; nelim t1; #t2 T; nnormalize; //; nqed.
104
105(*
106Hint Rewrite E0_left E0_right Eapp_assoc
107             E0_left_inf Eappinf_assoc: trace_rewrite.
108
109Opaque trace E0 Eextcall Eapp Eappinf.
110
111(** The following [traceEq] tactic proves equalities between traces
112  or infinite traces. *)
113
114Ltac substTraceHyp :=
115  match goal with
116  | [ H: (@eq trace ?x ?y) |- _ ] =>
117       subst x || clear H
118  end.
119
120Ltac decomposeTraceEq :=
121  match goal with
122  | [ |- (_ ** _) = (_ ** _) ] =>
123      apply (f_equal2 Eapp); auto; decomposeTraceEq
124  | _ =>
125      auto
126  end.
127
128Ltac traceEq :=
129  repeat substTraceHyp; autorewrite with trace_rewrite; decomposeTraceEq.
130*)
131(* * The predicate [event_match ef vargs t vres] expresses that
132  the event [t] is generated when invoking external function [ef]
133  with arguments [vargs], and obtaining [vres] as a return value
134  from the operating system. *)
135
136ninductive eventval_match: eventval -> typ -> val -> Prop :=
137  | ev_match_int:
138      ∀i. eventval_match (EVint i) Tint (Vint i)
139  | ev_match_float:
140      ∀f. eventval_match (EVfloat f) Tfloat (Vfloat f).
141
142ninductive eventval_list_match: list eventval -> list typ -> list val -> Prop :=
143  | evl_match_nil:
144      eventval_list_match (nil ?) (nil ?) (nil ?)
145  | evl_match_cons:
146      ∀ev1,evl,ty1,tyl,v1,vl.
147      eventval_match ev1 ty1 v1 ->
148      eventval_list_match evl tyl vl ->
149      eventval_list_match (ev1::evl) (ty1::tyl) (v1::vl).
150
151ninductive event_match:
152         external_function -> list val -> trace -> val -> Prop :=
153  event_match_intro:
154    ∀ef,vargs,vres,eargs,eres.
155    eventval_list_match eargs (sig_args (ef_sig ef)) vargs ->
156    eventval_match eres (proj_sig_res (ef_sig ef)) vres ->
157    event_match ef vargs (Eextcall (ef_id ef) eargs eres) vres.
158(*
159(** The following section shows that [event_match] is stable under
160  relocation of pointer values, as performed by memory injections
161  (see module [Mem]). *)
162
163Require Import Mem.
164
165Section EVENT_MATCH_INJECT.
166
167Variable f: meminj.
168
169Remark eventval_match_inject:
170  forall ev ty v1,  eventval_match ev ty v1 ->
171  forall v2, val_inject f v1 v2 ->
172  eventval_match ev ty v2.
173Proof.
174  induction 1; intros; inversion H; constructor.
175Qed.
176
177Remark eventval_list_match_inject:
178  forall evl tyl vl1,  eventval_list_match evl tyl vl1 ->
179  forall vl2, val_list_inject f vl1 vl2 ->
180  eventval_list_match evl tyl vl2.
181Proof.
182  induction 1; intros.
183  inversion H; constructor.
184  inversion H1; constructor.
185  eapply eventval_match_inject; eauto.
186  eauto.
187Qed.
188
189Lemma event_match_inject:
190  forall ef args1 t res args2,
191  event_match ef args1 t res ->
192  val_list_inject f args1 args2 ->
193  event_match ef args2 t res /\ val_inject f res res.
194Proof.
195  intros. inversion H; subst.
196  split. constructor. eapply eventval_list_match_inject; eauto. auto.
197  inversion H2; constructor.
198Qed.
199
200End EVENT_MATCH_INJECT.
201
202(** The following section shows that [event_match] is stable under
203  replacement of [Vundef] values by more defined values. *)
204
205Section EVENT_MATCH_LESSDEF.
206
207Remark eventval_match_lessdef:
208  forall ev ty v1,  eventval_match ev ty v1 ->
209  forall v2, Val.lessdef v1 v2 ->
210  eventval_match ev ty v2.
211Proof.
212  induction 1; intros; inv H; constructor.
213Qed.
214
215Remark eventval_list_match_moredef:
216  forall evl tyl vl1, eventval_list_match evl tyl vl1 ->
217  forall vl2, Val.lessdef_list vl1 vl2 ->
218  eventval_list_match evl tyl vl2.
219Proof.
220  induction 1; intros.
221  inversion H; constructor.
222  inversion H1; constructor.
223  eapply eventval_match_lessdef; eauto.
224  eauto.
225Qed.
226
227Lemma event_match_lessdef:
228  forall ef args1 t res1 args2,
229  event_match ef args1 t res1 ->
230  Val.lessdef_list args1 args2 ->
231  exists res2, event_match ef args2 t res2 /\ Val.lessdef res1 res2.
232Proof.
233  intros. inversion H; subst. exists res1; split.
234  constructor. eapply eventval_list_match_moredef; eauto. auto.
235  auto.
236Qed.
237
238End EVENT_MATCH_LESSDEF.
239
240(** Bisimilarity between infinite traces. *)
241
242CoInductive traceinf_sim: traceinf -> traceinf -> Prop :=
243  | traceinf_sim_cons: forall e T1 T2,
244      traceinf_sim T1 T2 ->
245      traceinf_sim (Econsinf e T1) (Econsinf e T2).
246
247Lemma traceinf_sim_refl:
248  forall T, traceinf_sim T T.
249Proof.
250  cofix COINDHYP; intros.
251  destruct T. constructor. apply COINDHYP.
252Qed.
253 
254Lemma traceinf_sim_sym:
255  forall T1 T2, traceinf_sim T1 T2 -> traceinf_sim T2 T1.
256Proof.
257  cofix COINDHYP; intros. inv H; constructor; auto.
258Qed.
259
260Lemma traceinf_sim_trans:
261  forall T1 T2 T3,
262  traceinf_sim T1 T2 -> traceinf_sim T2 T3 -> traceinf_sim T1 T3.
263Proof.
264  cofix COINDHYP;intros. inv H; inv H0; constructor; eauto.
265Qed.
266
267(** The "is prefix of" relation between a finite and an infinite trace. *)
268
269Inductive traceinf_prefix: trace -> traceinf -> Prop :=
270  | traceinf_prefix_nil: forall T,
271      traceinf_prefix nil T
272  | traceinf_prefix_cons: forall e t1 T2,
273      traceinf_prefix t1 T2 ->
274      traceinf_prefix (e :: t1) (Econsinf e T2).
275
276(*
277Lemma traceinf_prefix_compat:
278  forall T1 T2 T1' T2',
279  traceinf_prefix T1 T2 -> traceinf_sim T1 T1' -> traceinf_sim T2 T2' ->
280  traceinf_prefix T1' T2'.
281Proof.
282  cofix COINDHYP; intros.
283  inv H; inv H0; inv H1; constructor; eapply COINDHYP; eauto.
284Qed.
285
286Transparent trace E0 Eapp Eappinf.
287*)
288
289Lemma traceinf_prefix_app:
290  forall t1 T2 t,
291  traceinf_prefix t1 T2 ->
292  traceinf_prefix (t ** t1) (t *** T2).
293Proof.
294  induction t; simpl; intros. auto.
295  change ((a :: t) ** t1) with (a :: (t ** t1)).
296  change ((a :: t) *** T2) with (Econsinf a (t *** T2)).
297  constructor. auto.
298Qed.
299
300*)
Note: See TracBrowser for help on using the repository browser.