source: Deliverables/D3.1/C-semantics/Events.ma @ 535

Last change on this file since 535 was 487, checked in by campbell, 9 years ago

Port Clight semantics to the new-new matita syntax.

File size: 10.6 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*)
20(*include "AST.ma".*)
21(*include "Integers.ma".*)
22(*include "Floats.ma".*)
23include "Values.ma".
24include "basics/list.ma".
25include "extralib.ma".
26include "CostLabel.ma".
27
28(* * The observable behaviour of programs is stated in terms of
29  input/output events, which can also be thought of as system calls
30  to the operating system.  An event is generated each time an
31  external function (see module AST) is invoked.  The event records
32  the name of the external function, the arguments to the function
33  invocation provided by the program, and the return value provided by
34  the outside world (e.g. the operating system).  Arguments and values
35  are either integers or floating-point numbers.  We currently do not
36  allow pointers to be exchanged between the program and the outside
37  world. *)
38
39inductive eventval: Type[0] :=
40  | EVint: int -> eventval
41  | EVfloat: float -> eventval.
42
43inductive event : Type[0] ≝
44  | EVcost: costlabel → event
45  | EVextcall: ∀ev_name: ident. ∀ev_args: list eventval. ∀ev_res: eventval. event.
46
47(* * The dynamic semantics for programs collect traces of events.
48  Traces are of two kinds: finite (type [trace]) or infinite (type [traceinf]). *)
49
50definition trace := list event.
51
52definition E0 : trace := nil ?.
53
54definition Echarge : costlabel → trace ≝
55λlabel. EVcost label :: (nil ?).
56
57definition Eextcall : ident → list eventval → eventval → trace ≝
58             λname: ident. λargs: list eventval. λres: eventval.
59  EVextcall name args res :: (nil ?).
60
61definition Eapp : trace → trace → trace ≝ λt1,t2. t1 @ t2.
62
63coinductive traceinf : Type[0] :=
64  | Econsinf: event -> traceinf -> traceinf.
65
66let rec Eappinf (t: trace) (T: traceinf) on t : traceinf :=
67  match t with
68  [ nil => T
69  | cons ev t' => Econsinf ev (Eappinf t' T)
70  ].
71
72(* * Concatenation of traces is written [**] in the finite case
73  or [***] in the infinite case. *)
74
75notation "hvbox(l1 break ⧺ l2)"
76  right associative with precedence 47
77  for @{'doubleplus $l1 $l2 }.
78
79notation "hvbox(l1 break ⧻ l2)"
80  right associative with precedence 47
81  for @{'tripleplus $l1 $l2 }.
82
83interpretation "trace concatenation" 'doubleplus l1 l2 = (Eapp l1 l2).
84interpretation "infinite trace concatenation" 'tripleplus l1 l2 = (Eappinf l1 l2).
85(*
86Infix "**" := Eapp (at level 60, right associativity).
87Infix "***" := Eappinf (at level 60, right associativity).
88*)
89lemma E0_left: ∀t. E0 ⧺ t = t.
90//; qed.
91
92lemma E0_right: ∀t. t ⧺ E0 = t.
93@append_nil qed.
94
95lemma Eapp_assoc: ∀t1,t2,t3. (t1 ⧺ t2) ⧺ t3 = t1 ⧺ (t2 ⧺ t3).
96@associative_append qed.
97
98lemma Eapp_E0_inv: ∀t1,t2. t1 ⧺ t2 = E0 → t1 = E0 ∧ t2 = E0.
99@nil_append_nil_both qed.
100 
101lemma E0_left_inf: ∀T. E0 ⧻ T = T.
102//; qed.
103
104lemma Eappinf_assoc: ∀t1,t2,T. (t1 ⧺ t2) ⧻ T = t1 ⧻ (t2 ⧻ T).
105#t1 elim t1; #t2 #T normalize; //; qed.
106
107(*
108Hint Rewrite E0_left E0_right Eapp_assoc
109             E0_left_inf Eappinf_assoc: trace_rewrite.
110
111Opaque trace E0 Eextcall Eapp Eappinf.
112
113(** The following [traceEq] tactic proves equalities between traces
114  or infinite traces. *)
115
116Ltac substTraceHyp :=
117  match goal with
118  | [ H: (@eq trace ?x ?y) |- _ ] =>
119       subst x || clear H
120  end.
121
122Ltac decomposeTraceEq :=
123  match goal with
124  | [ |- (_ ** _) = (_ ** _) ] =>
125      apply (f_equal2 Eapp); auto; decomposeTraceEq
126  | _ =>
127      auto
128  end.
129
130Ltac traceEq :=
131  repeat substTraceHyp; autorewrite with trace_rewrite; decomposeTraceEq.
132*)
133
134(* Ported from CompCert 1.7.1 >>> *)
135
136(* * An alternate presentation of infinite traces as
137  infinite concatenations of nonempty finite traces. *)
138
139coinductive traceinf': Type[0] ≝
140  | Econsinf': ∀t: trace. ∀T: traceinf'. t ≠ E0 → traceinf'.
141
142definition split_traceinf' : ∀t:trace. traceinf' → t ≠ E0 → event × traceinf' ≝
143λt,T.
144  match t return λt0.t0 ≠ E0 → ? with
145  [ nil ⇒ ?
146  | cons e t' ⇒ λ_.
147     (match t' return λt0. t' = t0 → ? with
148     [ nil ⇒ λ_.〈e, T〉
149     | cons e' t'' ⇒ λE.〈e, Econsinf' t' T ?〉
150     ]) (refl ? t')
151  ].
152[ *; #NE @False_rect_Type0 @NE @refl
153| % #E' >E' in E #E whd in E:(??%%); destruct (E);
154] qed.
155
156let corec traceinf_of_traceinf' (T': traceinf') : traceinf ≝
157  match T' with
158  [ Econsinf' t T'' NOTEMPTY ⇒
159      match split_traceinf' t T'' NOTEMPTY with [ pair e tl ⇒
160      Econsinf e (traceinf_of_traceinf' tl) ]
161  ].
162
163lemma unroll_traceinf':
164  ∀T. T = match T with [ Econsinf' t T' NE ⇒ Econsinf' t T' NE ].
165#T cases T; //; qed.
166
167lemma unroll_traceinf:
168  ∀T. T = match T with [ Econsinf t T' ⇒ Econsinf t T' ].
169#T cases T #ev #tr @refl (* XXX //; *)
170qed.
171
172lemma traceinf_traceinfp_app:
173  ∀t,T,NE.
174  traceinf_of_traceinf' (Econsinf' t T NE) = t ⧻ traceinf_of_traceinf' T.
175#t elim t;
176[ #T #NE cases NE; #NE' @False_ind @NE' @refl
177| #h #t' cases t'; [ 2: #h' #t'' ] #IH #T #NE
178    >(unroll_traceinf (traceinf_of_traceinf' ?))
179    whd in ⊢ (??%?); //; >(IH …) @refl
180] qed.
181
182(* <<< *)
183
184(* * The predicate [event_match ef vargs t vres] expresses that
185  the event [t] is generated when invoking external function [ef]
186  with arguments [vargs], and obtaining [vres] as a return value
187  from the operating system. *)
188
189inductive eventval_match: eventval -> typ -> val -> Prop :=
190  | ev_match_int:
191      ∀i. eventval_match (EVint i) ASTint (Vint i)
192  | ev_match_float:
193      ∀f. eventval_match (EVfloat f) ASTfloat (Vfloat f).
194
195inductive eventval_list_match: list eventval -> list typ -> list val -> Prop :=
196  | evl_match_nil:
197      eventval_list_match (nil ?) (nil ?) (nil ?)
198  | evl_match_cons:
199      ∀ev1,evl,ty1,tyl,v1,vl.
200      eventval_match ev1 ty1 v1 ->
201      eventval_list_match evl tyl vl ->
202      eventval_list_match (ev1::evl) (ty1::tyl) (v1::vl).
203
204inductive event_match:
205         external_function -> list val -> trace -> val -> Prop :=
206  event_match_intro:
207    ∀ef,vargs,vres,eargs,eres.
208    eventval_list_match eargs (sig_args (ef_sig ef)) vargs ->
209    eventval_match eres (proj_sig_res (ef_sig ef)) vres ->
210    event_match ef vargs (Eextcall (ef_id ef) eargs eres) vres.
211(*
212(** The following section shows that [event_match] is stable under
213  relocation of pointer values, as performed by memory injections
214  (see module [Mem]). *)
215
216Require Import Mem.
217
218Section EVENT_MATCH_INJECT.
219
220Variable f: meminj.
221
222Remark eventval_match_inject:
223  forall ev ty v1,  eventval_match ev ty v1 ->
224  forall v2, val_inject f v1 v2 ->
225  eventval_match ev ty v2.
226Proof.
227  induction 1; intros; inversion H; constructor.
228Qed.
229
230Remark eventval_list_match_inject:
231  forall evl tyl vl1,  eventval_list_match evl tyl vl1 ->
232  forall vl2, val_list_inject f vl1 vl2 ->
233  eventval_list_match evl tyl vl2.
234Proof.
235  induction 1; intros.
236  inversion H; constructor.
237  inversion H1; constructor.
238  eapply eventval_match_inject; eauto.
239  eauto.
240Qed.
241
242Lemma event_match_inject:
243  forall ef args1 t res args2,
244  event_match ef args1 t res ->
245  val_list_inject f args1 args2 ->
246  event_match ef args2 t res /\ val_inject f res res.
247Proof.
248  intros. inversion H; subst.
249  split. constructor. eapply eventval_list_match_inject; eauto. auto.
250  inversion H2; constructor.
251Qed.
252
253End EVENT_MATCH_INJECT.
254
255(** The following section shows that [event_match] is stable under
256  replacement of [Vundef] values by more defined values. *)
257
258Section EVENT_MATCH_LESSDEF.
259
260Remark eventval_match_lessdef:
261  forall ev ty v1,  eventval_match ev ty v1 ->
262  forall v2, Val.lessdef v1 v2 ->
263  eventval_match ev ty v2.
264Proof.
265  induction 1; intros; inv H; constructor.
266Qed.
267
268Remark eventval_list_match_moredef:
269  forall evl tyl vl1, eventval_list_match evl tyl vl1 ->
270  forall vl2, Val.lessdef_list vl1 vl2 ->
271  eventval_list_match evl tyl vl2.
272Proof.
273  induction 1; intros.
274  inversion H; constructor.
275  inversion H1; constructor.
276  eapply eventval_match_lessdef; eauto.
277  eauto.
278Qed.
279
280Lemma event_match_lessdef:
281  forall ef args1 t res1 args2,
282  event_match ef args1 t res1 ->
283  Val.lessdef_list args1 args2 ->
284  exists res2, event_match ef args2 t res2 /\ Val.lessdef res1 res2.
285Proof.
286  intros. inversion H; subst. exists res1; split.
287  constructor. eapply eventval_list_match_moredef; eauto. auto.
288  auto.
289Qed.
290
291End EVENT_MATCH_LESSDEF.
292
293(** Bisimilarity between infinite traces. *)
294
295CoInductive traceinf_sim: traceinf -> traceinf -> Prop :=
296  | traceinf_sim_cons: forall e T1 T2,
297      traceinf_sim T1 T2 ->
298      traceinf_sim (Econsinf e T1) (Econsinf e T2).
299
300Lemma traceinf_sim_refl:
301  forall T, traceinf_sim T T.
302Proof.
303  cofix COINDHYP; intros.
304  destruct T. constructor. apply COINDHYP.
305Qed.
306 
307Lemma traceinf_sim_sym:
308  forall T1 T2, traceinf_sim T1 T2 -> traceinf_sim T2 T1.
309Proof.
310  cofix COINDHYP; intros. inv H; constructor; auto.
311Qed.
312
313Lemma traceinf_sim_trans:
314  forall T1 T2 T3,
315  traceinf_sim T1 T2 -> traceinf_sim T2 T3 -> traceinf_sim T1 T3.
316Proof.
317  cofix COINDHYP;intros. inv H; inv H0; constructor; eauto.
318Qed.
319
320(** The "is prefix of" relation between a finite and an infinite trace. *)
321
322Inductive traceinf_prefix: trace -> traceinf -> Prop :=
323  | traceinf_prefix_nil: forall T,
324      traceinf_prefix nil T
325  | traceinf_prefix_cons: forall e t1 T2,
326      traceinf_prefix t1 T2 ->
327      traceinf_prefix (e :: t1) (Econsinf e T2).
328
329(*
330Lemma traceinf_prefix_compat:
331  forall T1 T2 T1' T2',
332  traceinf_prefix T1 T2 -> traceinf_sim T1 T1' -> traceinf_sim T2 T2' ->
333  traceinf_prefix T1' T2'.
334Proof.
335  cofix COINDHYP; intros.
336  inv H; inv H0; inv H1; constructor; eapply COINDHYP; eauto.
337Qed.
338
339Transparent trace E0 Eapp Eappinf.
340*)
341
342Lemma traceinf_prefix_app:
343  forall t1 T2 t,
344  traceinf_prefix t1 T2 ->
345  traceinf_prefix (t ** t1) (t *** T2).
346Proof.
347  induction t; simpl; intros. auto.
348  change ((a :: t) ** t1) with (a :: (t ** t1)).
349  change ((a :: t) *** T2) with (Econsinf a (t *** T2)).
350  constructor. auto.
351Qed.
352
353*)
Note: See TracBrowser for help on using the repository browser.