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

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

Minimal integration of bitvectors into Clight semantics

  • does a "round trip" through Z for most operations (slow)
  • a few extra bits for equality on vectors
  • version of reverse that doesn't make matita fall over on size 32 vectors during disambiguation and automation
File size: 27.7 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(* * Tools for small-step operational semantics *)
17
18(* * This module defines generic operations and theorems over
19  the one-step transition relations that are used to specify
20  operational semantics in small-step style. *)
21
22(*
23Require Import Wf.
24Require Import Wf_nat.
25Require Import Classical.
26Require Import Coqlib.
27Require Import AST.
28*)
29include "Events.ma".
30(*
31Require Import Globalenvs.
32Require Import Integers.
33
34Set Implicit Arguments.
35*)
36(* * * Closures of transitions relations *)
37
38record transrel : Type[1] ≝ {
39  genv : Type[0];
40  state: Type[0];
41  step : genv → state → trace → state → Prop
42}.
43
44(*Section CLOSURES.
45
46Variable genv: Type.
47Variable state: Type.
48
49(* * A one-step transition relation has the following signature.
50  It is parameterized by a global environment, which does not
51  change during the transition.  It relates the initial state
52  of the transition with its final state.  The [trace] parameter
53  captures the observable events possibly generated during the
54  transition. *)
55
56Variable step: genv -> state -> trace -> state -> Prop.
57*)
58(* * No transitions: stuck state *)
59
60definition nostep ≝ λtr:transrel. λge: genv tr. λs: state tr.
61  ∀t,s'. ¬((step tr) ge s t s').
62
63(* * Zero, one or several transitions.  Also known as Kleene closure,
64    or reflexive transitive closure. *)
65
66inductive star (tr:transrel) (ge: genv tr): state tr -> trace -> state tr -> Prop :=
67  | star_refl: ∀s.
68      star tr ge s E0 s
69  | star_step: ∀s1,t1,s2,t2,s3,t.
70      (step tr) ge s1 t1 s2 -> star tr ge s2 t2 s3 -> t = t1 ⧺ t2 ->
71      star tr ge s1 t s3.
72
73lemma star_one:
74  ∀tr,ge,s1,t,s2. (step tr) ge s1 t s2 -> star tr ge s1 t s2.
75#tr #ge #s1 #t #s2 #H @(star_step … H (star_refl …))
76>(E0_right …) //;
77qed.
78
79lemma star_trans:
80  ∀tr,ge,s1,t1,s2. star tr ge s1 t1 s2 ->
81  ∀t2,s3,t. star tr ge s2 t2 s3 -> t = t1 ⧺ t2 -> star tr ge s1 t s3.
82#tr #ge #s1 #t1 #s2 #H elim H;
83[ #s #t2 #s3 #t #H0 #H1 >H1 normalize; //;
84| #s #t #s' #t' #s'' #t'' #H0 #H1 #H2 #H3
85    #t2 #s3 #t3 #H4 #H5
86    @(star_step … H0 (H3 … H4 …) ?)
87    [ @(t'⧺t2)
88    | //
89    | <(Eapp_assoc …) <H2 @H5
90    ]
91]
92qed.
93
94lemma star_left:
95  ∀tr,ge,s1,t1,s2,t2,s3,t.
96  (step tr) ge s1 t1 s2 -> star tr ge s2 t2 s3 -> t = t1 ⧺ t2 ->
97  star tr ge s1 t s3.
98@star_step
99qed.
100
101lemma star_right:
102  ∀tr,ge,s1,t1,s2,t2,s3,t.
103  star tr ge s1 t1 s2 -> (step tr) ge s2 t2 s3 -> t = t1 ⧺ t2 ->
104  star tr ge s1 t s3.
105#tr #ge #s1 #t1 #s2 #t2 #s3 #t #H1 #H2 #H3
106@(star_trans … H1 … (star_one … H2)) @H3
107qed.
108
109(* * One or several transitions.  Also known as the transitive closure. *)
110
111inductive plus (tr:transrel) (ge: genv tr): state tr → trace → state tr → Prop ≝
112  | plus_left: ∀s1,t1,s2,t2,s3,t.
113      step tr ge s1 t1 s2 -> star tr ge s2 t2 s3 -> t = t1 ⧺ t2 ->
114      plus tr ge s1 t s3.
115
116lemma plus_one:
117  ∀tr,ge,s1,t,s2.
118  step tr ge s1 t s2 -> plus tr ge s1 t s2.
119#tr #ge #s1 #t #s2 #H @(plus_left … H (star_refl …))
120>(E0_right …) //;
121qed.
122
123lemma plus_star:
124  ∀tr,ge,s1,t,s2. plus tr ge s1 t s2 -> star tr ge s1 t s2.
125#tr #ge #s1 #t #s2 #H elim H; #s1' #t1' #s2' #t2' #s3' #t3' #H1 #H2 #e1
126@(star_step … H1 H2 …) @e1;
127qed.
128
129lemma plus_right:
130  ∀tr,ge,s1,t1,s2,t2,s3,t.
131  star tr ge s1 t1 s2 -> step tr ge s2 t2 s3 -> t = t1 ⧺ t2 ->
132  plus tr ge s1 t s3.
133#tr #ge #s1 #t1 #s2 #t2 #s3 #t3 #Hstar #Hstep #e1 inversion Hstar;
134[ #s2' #e2 #e3 #e4 destruct; @plus_one //;
135| #s1' #t1' #s1'' #t1'' #s2' #t2' #H1 #H2 #e2 #foo #e3 #e4 #e5 destruct;
136    >(Eapp_assoc …) @(plus_left … H1)
137    [ 2: @(star_right … H2 Hstep) //;
138    | skip;
139    | //
140    ]
141]
142qed.
143(*
144Lemma plus_left':
145  forall ge s1 t1 s2 t2 s3 t,
146  step ge s1 t1 s2 -> plus ge s2 t2 s3 -> t = t1 ** t2 ->
147  plus ge s1 t s3.
148Proof.
149  intros. eapply plus_left; eauto. apply plus_star; auto.
150Qed.
151
152Lemma plus_right':
153  forall ge s1 t1 s2 t2 s3 t,
154  plus ge s1 t1 s2 -> step ge s2 t2 s3 -> t = t1 ** t2 ->
155  plus ge s1 t s3.
156Proof.
157  intros. eapply plus_right; eauto. apply plus_star; auto.
158Qed.
159
160Lemma plus_star_trans:
161  forall ge s1 t1 s2 t2 s3 t,
162  plus ge s1 t1 s2 -> star ge s2 t2 s3 -> t = t1 ** t2 -> plus ge s1 t s3.
163Proof.
164  intros. inversion H; subst.
165  econstructor; eauto. eapply star_trans; eauto.
166  traceEq.
167Qed.
168
169Lemma star_plus_trans:
170  forall ge s1 t1 s2 t2 s3 t,
171  star ge s1 t1 s2 -> plus ge s2 t2 s3 -> t = t1 ** t2 -> plus ge s1 t s3.
172Proof.
173  intros. inversion H; subst.
174  simpl; auto.
175  rewrite Eapp_assoc.
176  econstructor. eauto. eapply star_trans. eauto.
177  apply plus_star. eauto. eauto. auto.
178Qed.
179
180Lemma plus_trans:
181  forall ge s1 t1 s2 t2 s3 t,
182  plus ge s1 t1 s2 -> plus ge s2 t2 s3 -> t = t1 ** t2 -> plus ge s1 t s3.
183Proof.
184  intros. eapply plus_star_trans. eauto. apply plus_star. eauto. auto.
185Qed.
186
187Lemma plus_inv:
188  forall ge s1 t s2,
189  plus ge s1 t s2 ->
190  step ge s1 t s2 \/ exists s', exists t1, exists t2, step ge s1 t1 s' /\ plus ge s' t2 s2 /\ t = t1 ** t2.
191Proof.
192  intros. inversion H; subst. inversion H1; subst.
193  left. rewrite E0_right. auto.
194  right. exists s3; exists t1; exists (t0 ** t3); split. auto.
195  split. econstructor; eauto. auto.
196Qed.
197
198Lemma star_inv:
199  forall ge s1 t s2,
200  star ge s1 t s2 ->
201  (s2 = s1 /\ t = E0) \/ plus ge s1 t s2.
202Proof.
203  intros. inv H. left; auto. right; econstructor; eauto.
204Qed.
205*)
206(* * Infinitely many transitions *)
207
208coinductive forever (tr:transrel) (ge: genv tr): state tr -> traceinf -> Prop :=
209  | forever_intro: ∀s1,t,s2,T.
210      step tr ge s1 t s2 -> forever tr ge s2 T ->
211      forever tr ge s1 (t ⧻ T).
212
213lemma star_forever:
214  ∀tr,ge,s1,t,s2. star tr ge s1 t s2 ->
215  ∀T. forever tr ge s2 T ->
216  forever tr ge s1 (t ⧻ T).
217#tr #ge #s1 #t1 #s2 #H elim H;
218[ #s' #T #H2 @H2
219| #s1' #t1 #s0 #t0 #s2' #t2' #H1 #H2 #e1 #IH #T #H3
220    >e1 >(Eappinf_assoc …)
221    % /2/;
222] qed.
223(*
224(** An alternate, equivalent definition of [forever] that is useful
225    for coinductive reasoning. *)
226
227Variable A: Type.
228Variable order: A -> A -> Prop.
229
230CoInductive forever_N (ge: genv) : A -> state -> traceinf -> Prop :=
231  | forever_N_star: forall s1 t s2 a1 a2 T1 T2,
232      star ge s1 t s2 ->
233      order a2 a1 ->
234      forever_N ge a2 s2 T2 ->
235      T1 = t *** T2 ->
236      forever_N ge a1 s1 T1
237  | forever_N_plus: forall s1 t s2 a1 a2 T1 T2,
238      plus ge s1 t s2 ->
239      forever_N ge a2 s2 T2 ->
240      T1 = t *** T2 ->
241      forever_N ge a1 s1 T1.
242
243Hypothesis order_wf: well_founded order.
244
245Lemma forever_N_inv:
246  forall ge a s T,
247  forever_N ge a s T ->
248  exists t, exists s', exists a', exists T',
249  step ge s t s' /\ forever_N ge a' s' T' /\ T = t *** T'.
250Proof.
251  intros ge a0. pattern a0. apply (well_founded_ind order_wf).
252  intros. inv H0.
253  (* star case *)
254  inv H1.
255  (* no transition *)
256  change (E0 *** T2) with T2. apply H with a2. auto. auto.
257  (* at least one transition *)
258  exists t1; exists s0; exists x; exists (t2 *** T2).
259  split. auto. split. eapply forever_N_star; eauto.
260  apply Eappinf_assoc.
261  (* plus case *)
262  inv H1.
263  exists t1; exists s0; exists a2; exists (t2 *** T2).
264  split. auto.
265  split. inv H3. auto. 
266  eapply forever_N_plus. econstructor; eauto. eauto. auto.
267  apply Eappinf_assoc.
268Qed.
269
270Lemma forever_N_forever:
271  forall ge a s T, forever_N ge a s T -> forever ge s T.
272Proof.
273  cofix COINDHYP; intros.
274  destruct (forever_N_inv H) as [t [s' [a' [T' [P [Q R]]]]]].
275  rewrite R. apply forever_intro with s'. auto.
276  apply COINDHYP with a'; auto.
277Qed.
278
279(** Yet another alternative definition of [forever]. *)
280
281CoInductive forever_plus (ge: genv) : state -> traceinf -> Prop :=
282  | forever_plus_intro: forall s1 t s2 T1 T2,
283      plus ge s1 t s2 ->
284      forever_plus ge s2 T2 ->
285      T1 = t *** T2 ->
286      forever_plus ge s1 T1.
287
288Lemma forever_plus_inv:
289  forall ge s T,
290  forever_plus ge s T ->
291  exists s', exists t, exists T',
292  step ge s t s' /\ forever_plus ge s' T' /\ T = t *** T'.
293Proof.
294  intros. inv H. inv H0. exists s0; exists t1; exists (t2 *** T2).
295  split. auto.
296  split. exploit star_inv; eauto. intros [[P Q] | R].
297    subst. simpl. auto. econstructor; eauto.
298  traceEq.
299Qed.
300
301Lemma forever_plus_forever:
302  forall ge s T, forever_plus ge s T -> forever ge s T.
303Proof.
304  cofix COINDHYP; intros.
305  destruct (forever_plus_inv H) as [s' [t [T' [P [Q R]]]]].
306  subst. econstructor; eauto.
307Qed.
308*)
309(* * Infinitely many silent transitions *)
310
311coinductive forever_silent (tr:transrel) (ge: genv tr): state tr → Prop ≝
312  | forever_silent_intro: ∀s1,s2.
313      step tr ge s1 E0 s2 → forever_silent tr ge s2 →
314      forever_silent tr ge s1.
315(*
316(** An alternate definition. *)
317
318CoInductive forever_silent_N (ge: genv) : A -> state -> Prop :=
319  | forever_silent_N_star: forall s1 s2 a1 a2,
320      star ge s1 E0 s2 ->
321      order a2 a1 ->
322      forever_silent_N ge a2 s2 ->
323      forever_silent_N ge a1 s1
324  | forever_silent_N_plus: forall s1 s2 a1 a2,
325      plus ge s1 E0 s2 ->
326      forever_silent_N ge a2 s2 ->
327      forever_silent_N ge a1 s1.
328
329Lemma forever_silent_N_inv:
330  forall ge a s,
331  forever_silent_N ge a s ->
332  exists s', exists a',
333  step ge s E0 s' /\ forever_silent_N ge a' s'.
334Proof.
335  intros ge a0. pattern a0. apply (well_founded_ind order_wf).
336  intros. inv H0.
337  (* star case *)
338  inv H1.
339  (* no transition *)
340  apply H with a2. auto. auto.
341  (* at least one transition *)
342  exploit Eapp_E0_inv; eauto. intros [P Q]. subst.
343  exists s0; exists x.
344  split. auto. eapply forever_silent_N_star; eauto.
345  (* plus case *)
346  inv H1. exploit Eapp_E0_inv; eauto. intros [P Q]. subst.
347  exists s0; exists a2.
348  split. auto. inv H3. auto. 
349  eapply forever_silent_N_plus. econstructor; eauto. eauto.
350Qed.
351
352Lemma forever_silent_N_forever:
353  forall ge a s, forever_silent_N ge a s -> forever_silent ge s.
354Proof.
355  cofix COINDHYP; intros.
356  destruct (forever_silent_N_inv H) as [s' [a' [P Q]]].
357  apply forever_silent_intro with s'. auto.
358  apply COINDHYP with a'; auto.
359Qed.
360*)
361(* * Infinitely many non-silent transitions *)
362
363coinductive forever_reactive (tr:transrel) (ge: genv tr): state tr → traceinf → Prop ≝
364  | forever_reactive_intro: ∀s1,s2,t,T.
365      star tr ge s1 t s2 → t ≠ E0 → forever_reactive tr ge s2 T →
366      forever_reactive tr ge s1 (t ⧻ T).
367(*
368lemma star_forever_reactive:
369  ∀tr,ge,s1,t,s2,T.
370  star tr ge s1 t s2 → forever_reactive tr ge s2 T →
371  forever_reactive tr ge s1 (t ⧻ T).
372#tr #ge #s1 #t #s2 #T #H1 #H2 inversion H2;
373Proof.
374  intros. inv H0. rewrite <- Eappinf_assoc. econstructor.
375  eapply star_trans; eauto.
376  red; intro. exploit Eapp_E0_inv; eauto. intros [P Q]. contradiction.
377  auto.
378Qed.
379*)
380(* * * Outcomes for program executions *)
381
382(* * The four possible outcomes for the execution of a program:
383- Termination, with a finite trace of observable events
384  and an integer value that stands for the process exit code
385  (the return value of the main function).
386- Divergence with a finite trace of observable events.
387  (At some point, the program runs forever without doing any I/O.)
388- Reactive divergence with an infinite trace of observable events.
389  (The program performs infinitely many I/O operations separated
390   by finite amounts of internal computations.)
391- Going wrong, with a finite trace of observable events
392  performed before the program gets stuck.
393*)
394
395inductive program_behavior: Type[0] :=
396  | Terminates: trace -> int -> program_behavior
397  | Diverges: trace -> program_behavior
398  | Reacts: traceinf -> program_behavior
399  | Goes_wrong: trace -> program_behavior.
400
401definition not_wrong : program_behavior → Prop ≝ λbeh.
402  match beh with
403  [ Terminates _ _ => True
404  | Diverges _ => True
405  | Reacts _ => True
406  | Goes_wrong _ => False
407  ].
408
409(* * Given a characterization of initial states and final states,
410  [program_behaves] relates a program behaviour with the
411  sequences of transitions that can be taken from an initial state
412  to a final state. *)
413(*
414Variable initial_state: state -> Prop.
415Variable final_state: state -> int -> Prop.
416*)
417inductive program_behaves (tr:transrel)
418                           (initial_state:state tr → Prop)
419                           (final_state : state tr → int → Prop)
420                           (ge: genv tr) : program_behavior -> Prop ≝
421  | program_terminates: ∀s,t,s',r.
422      initial_state s ->
423      star tr ge s t s' ->
424      final_state s' r ->
425      program_behaves tr initial_state final_state ge (Terminates t r)
426  | program_diverges: ∀s,t,s'.
427      initial_state s ->
428      star tr ge s t s' -> forever_silent tr ge s' ->
429      program_behaves tr initial_state final_state ge (Diverges t)
430  | program_reacts: ∀s,T.
431      initial_state s ->
432      forever_reactive tr ge s T ->
433      program_behaves tr initial_state final_state ge (Reacts T)
434  | program_goes_wrong: ∀s,t,s'.
435      initial_state s ->
436      star tr ge s t s' ->
437      nostep tr ge s' ->
438      (∀r. ¬final_state s' r) ->
439      program_behaves tr initial_state final_state ge (Goes_wrong t)
440  | program_goes_initially_wrong:
441      (∀s. ¬initial_state s) ->
442      program_behaves tr initial_state final_state ge (Goes_wrong E0).
443
444(*End CLOSURES.*)
445(*
446(** * Simulations between two small-step semantics. *)
447
448(** In this section, we show that if two transition relations
449  satisfy certain simulation diagrams, then every program behaviour
450  generated by the first transition relation can also occur
451  with the second transition relation. *)
452
453Section SIMULATION.
454
455(** The first small-step semantics is axiomatized as follows. *)
456
457Variable genv1: Type.
458Variable state1: Type.
459Variable step1: genv1 -> state1 -> trace -> state1 -> Prop.
460Variable initial_state1: state1 -> Prop.
461Variable final_state1: state1 -> int -> Prop.
462Variable ge1: genv1.
463*)
464
465record semantics : Type[1] ≝
466{ trans :> transrel
467; initial : (state trans) → Prop
468; final : (state trans) → int → Prop
469; ge : (genv trans)
470}.
471
472(*
473(** The second small-step semantics is also axiomatized. *)
474
475Variable genv2: Type[0].
476Variable state2: Type[0].
477Variable step2: genv2 -> state2 -> trace -> state2 -> Prop.
478Variable initial_state2: state2 -> Prop.
479Variable final_state2: state2 -> int -> Prop.
480Variable ge2: genv2.
481
482(** We assume given a matching relation between states of both semantics.
483  This matching relation must be compatible with initial states
484  and with final states. *)
485
486Variable match_states: state1 -> state2 -> Prop.
487
488Hypothesis match_initial_states:
489  forall st1, initial_state1 st1 ->
490  exists st2, initial_state2 st2 /\ match_states st1 st2.
491
492Hypothesis match_final_states:
493  forall st1 st2 r,
494  match_states st1 st2 ->
495  final_state1 st1 r ->
496  final_state2 st2 r.
497*)
498
499record related_semantics : Type[1] ≝
500{ sem1 : semantics
501; sem2 : semantics
502; match_states : state sem1 → state sem2 → Prop
503; match_initial_states : ∀st1. (initial sem1) st1 → ∃st2. (initial sem2) st2 ∧ match_states st1 st2
504; match_final_states : ∀st1,st2,r. match_states st1 st2 → (final sem1) st1 r → (final sem2) st2 r
505}.
506
507(*
508(** Simulation when one transition in the first program
509    corresponds to zero, one or several transitions in the second program.
510    However, there is no stuttering: infinitely many transitions
511    in the source program must correspond to infinitely many
512    transitions in the second program. *)
513
514Section SIMULATION_STAR_WF.
515
516(** [order] is a well-founded ordering associated with states
517  of the first semantics.  Stuttering steps must correspond
518  to states that decrease w.r.t. [order]. *)
519
520Variable order: state1 -> state1 -> Prop.
521Hypothesis order_wf: well_founded order.
522
523Hypothesis simulation:
524  forall st1 t st1', step1 ge1 st1 t st1' ->
525  forall st2, match_states st1 st2 ->
526  exists st2',
527  (plus step2 ge2 st2 t st2' \/ (star step2 ge2 st2 t st2' /\ order st1' st1))
528  /\ match_states st1' st2'.
529*)
530record order_sim : Type[1] ≝
531{ sem :> related_semantics
532; order : state (sem1 sem) → state (sem1 sem) → Prop
533(* ; order_wf  ? *)
534; simulation : ∀st1,t,st1'. step (sem1 sem) (ge (sem1 sem)) st1 t st1' →
535               ∀st2. match_states sem st1 st2 →
536               ∃st2'. (plus (sem2 sem) (ge (sem2 sem)) st2 t st2' ∨               
537                       (star (sem2 sem) (ge (sem2 sem)) st2 t st2' ∧
538                        order st1' st1))
539                      ∧ match_states sem st1' st2'
540}.
541
542lemma simulation_star_star: ∀sim:order_sim.
543  ∀st1,t,st1'. star (sem1 sim) (ge (sem1 sim)) st1 t st1' →
544  ∀st2. match_states sim st1 st2 →
545  ∃st2'. star (sem2 sim) (ge (sem2 sim)) st2 t st2' ∧ match_states sim st1' st2'.
546#sim #st1 #t #st1' #H elim H;
547[ #st1'' #st2 #Hmatch
548    %{ st2} % //;
549| #st1 #tA #st1A #tB #st1B #t #Hstep #Hstar #Ht #IH #st2 #Hmatch
550    elim (simulation sim ??? Hstep ? Hmatch); #st2' *; #A #B
551    elim (IH ? B); #st3' *; #C #D
552    %{ st3'} % //;
553    @(star_trans ??? tA st2' ? tB ?? C Ht)
554    elim A /2/ * //
555] qed.
556
557(*
558Lemma simulation_star_forever_silent:
559  forall st1 st2,
560  forever_silent step1 ge1 st1 -> match_states st1 st2 ->
561  forever_silent step2 ge2 st2.
562Proof.
563  assert (forall st1 st2,
564    forever_silent step1 ge1 st1 -> match_states st1 st2 ->
565    forever_silent_N step2 order ge2 st1 st2).
566  cofix COINDHYP; intros.
567  inversion H; subst.
568  destruct (simulation H1 H0) as [st2' [A B]].
569  destruct A as [C | [C D]].
570  apply forever_silent_N_plus with st2' s2.
571  auto. apply COINDHYP. assumption. assumption.
572  apply forever_silent_N_star with st2' s2.
573  auto. auto. apply COINDHYP. assumption. auto.
574  intros. eapply forever_silent_N_forever; eauto.
575Qed.
576
577Lemma simulation_star_forever_reactive:
578  forall st1 st2 T,
579  forever_reactive step1 ge1 st1 T -> match_states st1 st2 ->
580  forever_reactive step2 ge2 st2 T.
581Proof.
582  cofix COINDHYP; intros.
583  inv H.
584  destruct (simulation_star_star H1 H0) as [st2' [A B]].
585  econstructor. eexact A. auto.
586  eapply COINDHYP. eauto. auto.
587Qed.
588
589Lemma simulation_star_wf_preservation:
590  forall beh,
591  not_wrong beh ->
592  program_behaves step1 initial_state1 final_state1 ge1 beh ->
593  program_behaves step2 initial_state2 final_state2 ge2 beh.
594Proof.
595  intros. inv H0; simpl in H.
596  destruct (match_initial_states H1) as [s2 [A B]].
597  destruct (simulation_star_star H2 B) as [s2' [C D]].
598  econstructor; eauto.
599  destruct (match_initial_states H1) as [s2 [A B]].
600  destruct (simulation_star_star H2 B) as [s2' [C D]].
601  econstructor; eauto.
602  eapply simulation_star_forever_silent; eauto.
603  destruct (match_initial_states H1) as [s2 [A B]].
604  econstructor; eauto. eapply simulation_star_forever_reactive; eauto.
605  contradiction.
606  contradiction.
607Qed.
608
609End SIMULATION_STAR_WF.
610
611Section SIMULATION_STAR.
612
613(** We now consider the case where we have a nonnegative integer measure
614  associated with states of the first semantics.  It must decrease when we take
615  a stuttering step. *)
616
617Variable measure: state1 -> nat.
618
619Hypothesis simulation:
620  forall st1 t st1', step1 ge1 st1 t st1' ->
621  forall st2, match_states st1 st2 ->
622  (exists st2', plus step2 ge2 st2 t st2' /\ match_states st1' st2')
623  \/ (measure st1' < measure st1 /\ t = E0 /\ match_states st1' st2)%nat.
624
625Lemma simulation_star_preservation:
626  forall beh,
627  not_wrong beh ->
628  program_behaves step1 initial_state1 final_state1 ge1 beh ->
629  program_behaves step2 initial_state2 final_state2 ge2 beh.
630Proof.
631  intros.
632  apply simulation_star_wf_preservation with (ltof _ measure).
633  apply well_founded_ltof. intros.
634  destruct (simulation H1 H2) as [[st2' [A B]] | [A [B C]]].
635  exists st2'; auto.
636  exists st2; split. right; split. rewrite B. apply star_refl. auto. auto.
637  auto. auto.
638Qed.
639
640End SIMULATION_STAR.
641
642(** Lock-step simulation: each transition in the first semantics
643    corresponds to exactly one transition in the second semantics. *)
644
645Section SIMULATION_STEP.
646
647Hypothesis simulation:
648  forall st1 t st1', step1 ge1 st1 t st1' ->
649  forall st2, match_states st1 st2 ->
650  exists st2', step2 ge2 st2 t st2' /\ match_states st1' st2'.
651
652Lemma simulation_step_preservation:
653  forall beh,
654  not_wrong beh ->
655  program_behaves step1 initial_state1 final_state1 ge1 beh ->
656  program_behaves step2 initial_state2 final_state2 ge2 beh.
657Proof.
658  intros.
659  pose (measure := fun (st: state1) => 0%nat).
660  assert (simulation':
661  forall st1 t st1', step1 ge1 st1 t st1' ->
662  forall st2, match_states st1 st2 ->
663  (exists st2', plus step2 ge2 st2 t st2' /\ match_states st1' st2')
664  \/ (measure st1' < measure st1 /\ t = E0 /\ match_states st1' st2)%nat).
665  intros. destruct (simulation H1 H2) as [st2' [A B]].
666  left; exists st2'; split. apply plus_one; auto. auto.
667  eapply simulation_star_preservation; eauto.
668Qed.
669
670End SIMULATION_STEP.
671
672(** Simulation when one transition in the first program corresponds
673    to one or several transitions in the second program. *)
674
675Section SIMULATION_PLUS.
676
677Hypothesis simulation:
678  forall st1 t st1', step1 ge1 st1 t st1' ->
679  forall st2, match_states st1 st2 ->
680  exists st2', plus step2 ge2 st2 t st2' /\ match_states st1' st2'.
681
682Lemma simulation_plus_preservation:
683  forall beh,
684  not_wrong beh ->
685  program_behaves step1 initial_state1 final_state1 ge1 beh ->
686  program_behaves step2 initial_state2 final_state2 ge2 beh.
687Proof.
688  intros.
689  pose (measure := fun (st: state1) => 0%nat).
690  assert (simulation':
691  forall st1 t st1', step1 ge1 st1 t st1' ->
692  forall st2, match_states st1 st2 ->
693  (exists st2', plus step2 ge2 st2 t st2' /\ match_states st1' st2')
694  \/ (measure st1' < measure st1 /\ t = E0 /\ match_states st1' st2)%nat).
695  intros. destruct (simulation H1 H2) as [st2' [A B]].
696  left; exists st2'; auto.
697  eapply simulation_star_preservation; eauto.
698Qed.
699
700End SIMULATION_PLUS.
701
702(** Simulation when one transition in the first program
703    corresponds to zero or one transitions in the second program.
704    However, there is no stuttering: infinitely many transitions
705    in the source program must correspond to infinitely many
706    transitions in the second program. *)
707
708Section SIMULATION_OPT.
709
710Variable measure: state1 -> nat.
711
712Hypothesis simulation:
713  forall st1 t st1', step1 ge1 st1 t st1' ->
714  forall st2, match_states st1 st2 ->
715  (exists st2', step2 ge2 st2 t st2' /\ match_states st1' st2')
716  \/ (measure st1' < measure st1 /\ t = E0 /\ match_states st1' st2)%nat.
717
718Lemma simulation_opt_preservation:
719  forall beh,
720  not_wrong beh ->
721  program_behaves step1 initial_state1 final_state1 ge1 beh ->
722  program_behaves step2 initial_state2 final_state2 ge2 beh.
723Proof.
724  assert (simulation':
725    forall st1 t st1', step1 ge1 st1 t st1' ->
726    forall st2, match_states st1 st2 ->
727    (exists st2', plus step2 ge2 st2 t st2' /\ match_states st1' st2')
728    \/ (measure st1' < measure st1 /\ t = E0 /\ match_states st1' st2)%nat).
729  intros. elim (simulation H H0).
730  intros [st2' [A B]]. left. exists st2'; split. apply plus_one; auto. auto.
731  intros [A [B C]]. right. intuition.
732  intros. eapply simulation_star_preservation; eauto.
733Qed.
734
735End SIMULATION_OPT.
736
737End SIMULATION.
738
739(** * Additional results about infinite reduction sequences *)
740
741(** We now show that any infinite sequence of reductions is either of
742  the "reactive" kind or of the "silent" kind (after a finite number
743  of non-silent transitions).  The proof necessitates the axiom of
744  excluded middle.  This result is used in [Csem] and [Cminor] to
745  relate the coinductive big-step semantics for divergence with the
746  small-step notions of divergence. *)
747
748Require Import Classical.
749Unset Implicit Arguments.
750
751Section INF_SEQ_DECOMP.
752
753Variable genv: Type.
754Variable state: Type.
755Variable step: genv -> state -> trace -> state -> Prop.
756
757Variable ge: genv.
758
759Inductive State: Type :=
760  ST: forall (s: state) (T: traceinf), forever step ge s T -> State.
761
762Definition state_of_State (S: State): state :=
763  match S with ST s T F => s end.
764Definition traceinf_of_State (S: State) : traceinf :=
765  match S with ST s T F => T end.
766
767Inductive Step: trace -> State -> State -> Prop :=
768  | Step_intro: forall s1 t T s2 S F,
769      Step t (ST s1 (t *** T) (@forever_intro genv state step ge s1 t s2 T S F))
770             (ST s2 T F).
771
772Inductive Steps: State -> State -> Prop :=
773  | Steps_refl: forall S, Steps S S
774  | Steps_left: forall t S1 S2 S3, Step t S1 S2 -> Steps S2 S3 -> Steps S1 S3.
775
776Remark Steps_trans:
777  forall S1 S2, Steps S1 S2 -> forall S3, Steps S2 S3 -> Steps S1 S3.
778Proof.
779  induction 1; intros. auto. econstructor; eauto.
780Qed.
781
782Let Reactive (S: State) : Prop :=
783  forall S1,
784  Steps S S1 ->
785  exists S2, exists S3, exists t, Steps S1 S2 /\ Step t S2 S3 /\ t <> E0.
786
787Let Silent (S: State) : Prop :=
788  forall S1 t S2, Steps S S1 -> Step t S1 S2 -> t = E0.
789
790Lemma Reactive_or_Silent:
791  forall S, Reactive S \/ (exists S', Steps S S' /\ Silent S').
792Proof.
793  intros. destruct (classic (exists S', Steps S S' /\ Silent S')).
794  auto.
795  left. red; intros.
796  generalize (not_ex_all_not _ _ H S1). intros.
797  destruct (not_and_or _ _ H1). contradiction.
798  unfold Silent in H2.
799  generalize (not_all_ex_not _ _ H2). intros [S2 A].
800  generalize (not_all_ex_not _ _ A). intros [t B].
801  generalize (not_all_ex_not _ _ B). intros [S3 C].
802  generalize (imply_to_and _ _ C). intros [D F].
803  generalize (imply_to_and _ _ F). intros [G J].
804  exists S2; exists S3; exists t. auto. 
805Qed.
806
807Lemma Steps_star:
808  forall S1 S2, Steps S1 S2 ->
809  exists t, star step ge (state_of_State S1) t (state_of_State S2)
810         /\ traceinf_of_State S1 = t *** traceinf_of_State S2.
811Proof.
812  induction 1.
813  exists E0; split. apply star_refl. auto.
814  inv H. destruct IHSteps as [t' [A B]].
815  exists (t ** t'); split.
816  simpl; eapply star_left; eauto.
817  simpl in *. subst T. traceEq.
818Qed.
819
820Lemma Silent_forever_silent:
821  forall S,
822  Silent S -> forever_silent step ge (state_of_State S).
823Proof.
824  cofix COINDHYP; intro S. case S. intros until f. simpl. case f. intros.
825  assert (Step t (ST s1 (t *** T0) (forever_intro s1 t s0 f0))
826                 (ST s2 T0 f0)).
827    constructor.
828  assert (t = E0).
829    red in H. eapply H; eauto. apply Steps_refl.
830  apply forever_silent_intro with (state_of_State (ST s2 T0 f0)).
831  rewrite <- H1. assumption.
832  apply COINDHYP.
833  red; intros. eapply H. eapply Steps_left; eauto. eauto.
834Qed.
835
836Lemma Reactive_forever_reactive:
837  forall S,
838  Reactive S -> forever_reactive step ge (state_of_State S) (traceinf_of_State S).
839Proof.
840  cofix COINDHYP; intros.
841  destruct (H S) as [S1 [S2 [t [A [B C]]]]]. apply Steps_refl.
842  destruct (Steps_star _ _ A) as [t' [P Q]].
843  inv B. simpl in *. rewrite Q. rewrite <- Eappinf_assoc.
844  apply forever_reactive_intro with s2.
845  eapply star_right; eauto.
846  red; intros. destruct (Eapp_E0_inv _ _ H0). contradiction.
847  change (forever_reactive step ge (state_of_State (ST s2 T F)) (traceinf_of_State (ST s2 T F))).
848  apply COINDHYP.
849  red; intros. apply H.
850  eapply Steps_trans. eauto.
851  eapply Steps_left. constructor. eauto.
852Qed.
853
854Theorem forever_silent_or_reactive:
855  forall s T,
856  forever step ge s T ->
857  forever_reactive step ge s T \/
858  exists t, exists s', exists T',
859  star step ge s t s' /\ forever_silent step ge s' /\ T = t *** T'.
860Proof.
861  intros.
862  destruct (Reactive_or_Silent (ST s T H)).
863  left.
864  change (forever_reactive step ge (state_of_State (ST s T H)) (traceinf_of_State (ST s T H))).
865  apply Reactive_forever_reactive. auto.
866  destruct H0 as [S' [A B]].
867  exploit Steps_star; eauto. intros [t [C D]]. simpl in *.
868  right. exists t; exists (state_of_State S'); exists (traceinf_of_State S').
869  split. auto.
870  split. apply Silent_forever_silent. auto.
871  auto.
872Qed.
873
874End INF_SEQ_DECOMP.
875
876*)
Note: See TracBrowser for help on using the repository browser.