Merge of branch new-semantics: revised and strengthened top-level statements of semantic preservation.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1683 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

4 files changed, 2111 insertions, 660 deletions

diff --git a/common/Behaviors.v b/common/Behaviors.v
new file mode 100644
index 0000000..ccb5749
--- /dev/null
+++ b/common/Behaviors.v
@@ -0,0 +1,700 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Whole-program behaviors *)
+
+Require Import Classical.
+Require Import ClassicalEpsilon.
+Require Import Coqlib.
+Require Import AST.
+Require Import Events.
+Require Import Globalenvs.
+Require Import Integers.
+Require Import Smallstep.
+
+Set Implicit Arguments.
+
+(** * Behaviors for program executions *)
+
+(** The four possible outcomes for the execution of a program:
+- Termination, with a finite trace of observable events
+  and an integer value that stands for the process exit code
+  (the return value of the main function).
+- Divergence with a finite trace of observable events.
+  (At some point, the program runs forever without doing any I/O.)
+- Reactive divergence with an infinite trace of observable events.
+  (The program performs infinitely many I/O operations separated
+   by finite amounts of internal computations.)
+- Going wrong, with a finite trace of observable events
+  performed before the program gets stuck.
+*)
+
+Inductive program_behavior: Type :=
+  | Terminates: trace -> int -> program_behavior
+  | Diverges: trace -> program_behavior
+  | Reacts: traceinf -> program_behavior
+  | Goes_wrong: trace -> program_behavior.
+
+(** Operations and relations on behaviors *)
+
+Definition not_wrong (beh: program_behavior) : Prop :=
+  match beh with
+  | Terminates _ _ => True
+  | Diverges _ => True
+  | Reacts _ => True
+  | Goes_wrong _ => False
+  end.
+
+Definition behavior_app (t: trace) (beh: program_behavior): program_behavior :=
+  match beh with
+  | Terminates t1 r => Terminates (t ** t1) r
+  | Diverges t1 => Diverges (t ** t1)
+  | Reacts T => Reacts (t *** T)
+  | Goes_wrong t1 => Goes_wrong (t ** t1)
+  end.
+
+Lemma behavior_app_assoc:
+  forall t1 t2 beh,
+  behavior_app (t1 ** t2) beh = behavior_app t1 (behavior_app t2 beh).
+Proof.
+  intros. destruct beh; simpl; f_equal; traceEq. 
+Qed.
+
+Lemma behavior_app_E0:
+  forall beh, behavior_app E0 beh = beh.
+Proof.
+  destruct beh; auto.
+Qed.
+
+Definition behavior_prefix (t: trace) (beh: program_behavior) : Prop :=
+  exists beh', beh = behavior_app t beh'.
+
+Definition behavior_improves (beh1 beh2: program_behavior) : Prop :=
+  beh1 = beh2 \/ exists t, beh1 = Goes_wrong t /\ behavior_prefix t beh2.
+
+Lemma behavior_improves_refl:
+  forall beh, behavior_improves beh beh.
+Proof.
+  intros; red; auto.
+Qed.
+
+Lemma behavior_improves_trans:
+  forall beh1 beh2 beh3, 
+  behavior_improves beh1 beh2 -> behavior_improves beh2 beh3 ->
+  behavior_improves beh1 beh3.
+Proof.
+  intros. red. destruct H; destruct H0; subst; auto. 
+  destruct H as [t1 [EQ1 [beh2' EQ1']]].
+  destruct H0 as [t2 [EQ2 [beh3' EQ2']]].
+  subst. destruct beh2'; simpl in EQ2; try discriminate. inv EQ2. 
+  right. exists t1; split; auto. exists (behavior_app t beh3'). apply behavior_app_assoc.
+Qed.
+
+Lemma behavior_improves_bot:
+  forall beh, behavior_improves (Goes_wrong E0) beh.
+Proof.
+  intros. right. exists E0; split; auto. exists beh. rewrite behavior_app_E0; auto.
+Qed.
+
+Lemma behavior_improves_app:
+  forall t beh1 beh2,
+  behavior_improves beh1 beh2 ->
+  behavior_improves (behavior_app t beh1) (behavior_app t beh2).
+Proof.
+  intros. red; destruct H. left; congruence. 
+  destruct H as [t' [A [beh' B]]]. subst.
+  right; exists (t ** t'); split; auto. exists beh'. rewrite behavior_app_assoc; auto.
+Qed.
+
+(** Associating behaviors to programs. *)
+
+Section PROGRAM_BEHAVIORS.
+
+Variable L: semantics.
+
+Inductive state_behaves (s: state L): program_behavior -> Prop :=
+  | state_terminates: forall t s' r,
+      Star L s t s' ->
+      final_state L s' r ->
+      state_behaves s (Terminates t r)
+  | state_diverges: forall t s',
+      Star L s t s' -> Forever_silent L s' ->
+      state_behaves s (Diverges t)
+  | state_reacts: forall T,
+      Forever_reactive L s T ->
+      state_behaves s (Reacts T)
+  | state_goes_wrong: forall t s',
+      Star L s t s' ->
+      Nostep L s' ->
+      (forall r, ~final_state L s' r) ->
+      state_behaves s (Goes_wrong t).
+
+Inductive program_behaves: program_behavior -> Prop :=
+  | program_runs: forall s beh,
+      initial_state L s -> state_behaves s beh ->
+      program_behaves beh
+  | program_goes_initially_wrong:
+      (forall s, ~initial_state L s) ->
+      program_behaves (Goes_wrong E0).
+
+Lemma state_behaves_app:
+  forall s1 t s2 beh,
+  Star L s1 t s2 -> state_behaves s2 beh -> state_behaves s1 (behavior_app t beh).
+Proof.
+  intros. inv H0; simpl; econstructor; eauto; try (eapply star_trans; eauto). 
+  eapply star_forever_reactive; eauto.
+Qed.
+
+(** * Existence of behaviors *)
+
+(** We now show that any program admits at least one behavior.
+  The proof requires classical logic: the axiom of excluded middle
+  and an axiom of description. *)
+
+(** The most difficult part of the proof is to show the existence
+  of an infinite trace in the case of reactive divergence. *)
+
+Section TRACEINF_REACTS.
+
+Variable s0: state L.
+
+Hypothesis reacts:
+  forall s1 t1, Star L s0 t1 s1 ->
+  exists s2, exists t2, Star L s1 t2 s2 /\ t2 <> E0.
+
+Lemma reacts':
+  forall s1 t1, Star L s0 t1 s1 ->
+  { s2 : state L & { t2 : trace | Star L s1 t2 s2 /\ t2 <> E0 } }.
+Proof.
+  intros. 
+  destruct (constructive_indefinite_description _ (reacts H)) as [s2 A].
+  destruct (constructive_indefinite_description _ A) as [t2 [B C]].
+  exists s2; exists t2; auto.
+Qed.
+
+CoFixpoint build_traceinf' (s1: state L) (t1: trace) (ST: Star L s0 t1 s1) : traceinf' :=
+  match reacts' ST with
+  | existT s2 (exist t2 (conj A B)) =>
+      Econsinf' t2 
+                (build_traceinf' (star_trans ST A (refl_equal _)))
+                B
+  end.
+
+Lemma reacts_forever_reactive_rec:
+  forall s1 t1 (ST: Star L s0 t1 s1),
+  Forever_reactive L s1 (traceinf_of_traceinf' (build_traceinf' ST)).
+Proof.
+  cofix COINDHYP; intros.
+  rewrite (unroll_traceinf' (build_traceinf' ST)). simpl. 
+  destruct (reacts' ST) as [s2 [t2 [A B]]]. 
+  rewrite traceinf_traceinf'_app. 
+  econstructor. eexact A. auto. apply COINDHYP. 
+Qed.
+
+Lemma reacts_forever_reactive:
+  exists T, Forever_reactive L s0 T.
+Proof.
+  exists (traceinf_of_traceinf' (build_traceinf' (star_refl (step L) (globalenv L) s0))).
+  apply reacts_forever_reactive_rec.
+Qed.
+
+End TRACEINF_REACTS.
+
+Lemma diverges_forever_silent:
+  forall s0,
+  (forall s1 t1, Star L s0 t1 s1 -> exists s2, Step L s1 E0 s2) ->
+  Forever_silent L s0.
+Proof.
+  cofix COINDHYP; intros. 
+  destruct (H s0 E0) as [s1 ST]. constructor. 
+  econstructor. eexact ST. apply COINDHYP. 
+  intros. eapply H. eapply star_left; eauto.
+Qed.
+
+Lemma state_behaves_exists:
+  forall s, exists beh, state_behaves s beh.
+Proof.
+  intros s0.
+  destruct (classic (forall s1 t1, Star L s0 t1 s1 -> exists s2, exists t2, Step L s1 t2 s2)).
+(* 1 Divergence (silent or reactive) *)
+  destruct (classic (exists s1, exists t1, Star L s0 t1 s1 /\
+                       (forall s2 t2, Star L s1 t2 s2 ->
+                        exists s3, Step L s2 E0 s3))).
+(* 1.1 Silent divergence *)
+  destruct H0 as [s1 [t1 [A B]]].
+  exists (Diverges t1); econstructor; eauto. 
+  apply diverges_forever_silent; auto.
+(* 1.2 Reactive divergence *)
+  destruct (@reacts_forever_reactive s0) as [T FR].
+  intros.
+  generalize (not_ex_all_not _ _ H0 s1). intro A; clear H0.
+  generalize (not_ex_all_not _ _ A t1). intro B; clear A.
+  destruct (not_and_or _ _ B). contradiction. 
+  destruct (not_all_ex_not _ _ H0) as [s2 C]; clear H0. 
+  destruct (not_all_ex_not _ _ C) as [t2 D]; clear C.
+  destruct (imply_to_and _ _ D) as [E F]; clear D.
+  destruct (H s2 (t1 ** t2)) as [s3 [t3 G]]. eapply star_trans; eauto. 
+  exists s3; exists (t2 ** t3); split.
+  eapply star_right; eauto. 
+  red; intros. destruct (app_eq_nil t2 t3 H0). subst. elim F. exists s3; auto.
+  exists (Reacts T); econstructor; eauto.
+(* 2 Termination (normal or by going wrong) *)
+  destruct (not_all_ex_not _ _ H) as [s1 A]; clear H.
+  destruct (not_all_ex_not _ _ A) as [t1 B]; clear A.
+  destruct (imply_to_and _ _ B) as [C D]; clear B.
+  destruct (classic (exists r, final_state L s1 r)) as [[r FINAL] | NOTFINAL].
+(* 2.1 Normal termination *)
+  exists (Terminates t1 r); econstructor; eauto.
+(* 2.2 Going wrong *)
+  exists (Goes_wrong t1); econstructor; eauto. red. intros. 
+  generalize (not_ex_all_not _ _ D s'); intros. 
+  generalize (not_ex_all_not _ _ H t); intros. 
+  auto.
+Qed.
+
+Theorem program_behaves_exists:
+  exists beh, program_behaves beh.
+Proof.
+  destruct (classic (exists s, initial_state L s)) as [[s0 INIT] | NOTINIT].
+(* 1. Initial state is defined. *)
+  destruct (state_behaves_exists s0) as [beh SB].
+  exists beh; econstructor; eauto. 
+(* 2. Initial state is undefined *)
+  exists (Goes_wrong E0). apply program_goes_initially_wrong. 
+  intros. eapply not_ex_all_not; eauto. 
+Qed.
+
+End PROGRAM_BEHAVIORS.
+
+(** * Forward simulations and program behaviors *)
+
+Section FORWARD_SIMULATIONS.
+
+Variable L1: semantics.
+Variable L2: semantics.
+Variable S: forward_simulation L1 L2.
+
+Lemma forward_simulation_state_behaves:
+  forall i s1 s2 beh1,
+  S i s1 s2 -> state_behaves L1 s1 beh1 ->
+  exists beh2, state_behaves L2 s2 beh2 /\ behavior_improves beh1 beh2.
+Proof.
+  intros. inv H0. 
+(* termination *)
+  exploit simulation_star; eauto. intros [i' [s2' [A B]]].
+  exists (Terminates t r); split.
+  econstructor; eauto. eapply fsim_match_final_states; eauto.
+  apply behavior_improves_refl.
+(* silent divergence *)
+  exploit simulation_star; eauto. intros [i' [s2' [A B]]].
+  exists (Diverges t); split.
+  econstructor; eauto. eapply simulation_forever_silent; eauto.
+  apply behavior_improves_refl.
+(* reactive divergence *)
+  exists (Reacts T); split.
+  econstructor. eapply simulation_forever_reactive; eauto.
+  apply behavior_improves_refl.
+(* going wrong *)
+  exploit simulation_star; eauto. intros [i' [s2' [A B]]].
+  destruct (state_behaves_exists L2 s2') as [beh' SB].
+  exists (behavior_app t beh'); split. 
+  eapply state_behaves_app; eauto. 
+  replace (Goes_wrong t) with (behavior_app t (Goes_wrong E0)).
+  apply behavior_improves_app. apply behavior_improves_bot. 
+  simpl. decEq. traceEq.
+Qed.
+
+Theorem forward_simulation_behavior_improves:
+  forall beh1, program_behaves L1 beh1 ->
+  exists beh2, program_behaves L2 beh2 /\ behavior_improves beh1 beh2.
+Proof.
+  intros. inv H.
+(* initial state defined *)
+  exploit (fsim_match_initial_states S); eauto. intros [i [s' [INIT MATCH]]].
+  exploit forward_simulation_state_behaves; eauto. intros [beh2 [A B]].
+  exists beh2; split; auto. econstructor; eauto.
+(* initial state undefined *)
+  destruct (classic (exists s', initial_state L2 s')).
+  destruct H as [s' INIT]. 
+  destruct (state_behaves_exists L2 s') as [beh' SB].
+  exists beh'; split. econstructor; eauto. apply behavior_improves_bot.
+  exists (Goes_wrong E0); split.
+  apply program_goes_initially_wrong. 
+  intros; red; intros. elim H; exists s; auto.
+  apply behavior_improves_refl.
+Qed.
+
+Corollary forward_simulation_same_safe_behavior:
+  forall beh,
+  program_behaves L1 beh -> not_wrong beh ->
+  program_behaves L2 beh.
+Proof.
+  intros. exploit forward_simulation_behavior_improves; eauto. 
+  intros [beh' [A B]]. destruct B. 
+  congruence.
+  destruct H1 as [t [C D]]. subst. contradiction.
+Qed.
+
+End FORWARD_SIMULATIONS.
+
+(** * Backward simulations and program behaviors *)
+
+Section BACKWARD_SIMULATIONS.
+
+Variable L1: semantics.
+Variable L2: semantics.
+Variable S: backward_simulation L1 L2.
+
+Definition safe_along_behavior (s: state L1) (b: program_behavior) : Prop :=
+  forall t1 s' b2, Star L1 s t1 s' -> b = behavior_app t1 b2 ->
+     (exists r, final_state L1 s' r)
+  \/ (exists t2, exists s'', Step L1 s' t2 s'').
+
+Remark safe_along_safe:
+  forall s b, safe_along_behavior s b -> safe L1 s.
+Proof.
+  intros; red; intros. eapply H; eauto. symmetry; apply behavior_app_E0. 
+Qed.
+
+Remark star_safe_along:
+  forall s b t1 s' b2,
+  safe_along_behavior s b ->
+  Star L1 s t1 s' -> b = behavior_app t1 b2 ->
+  safe_along_behavior s' b2.
+Proof.
+  intros; red; intros. eapply H. eapply star_trans; eauto.
+  subst. rewrite behavior_app_assoc. eauto.
+Qed.
+
+Remark not_safe_along_behavior:
+  forall s b,
+  ~ safe_along_behavior s b ->
+  exists t, exists s',
+     behavior_prefix t b 
+  /\ Star L1 s t s'
+  /\ Nostep L1 s'
+  /\ (forall r, ~(final_state L1 s' r)).
+Proof.
+  intros. 
+  destruct (not_all_ex_not _ _ H) as [t1 A]; clear H.
+  destruct (not_all_ex_not _ _ A) as [s' B]; clear A.
+  destruct (not_all_ex_not _ _ B) as [b2 C]; clear B.
+  destruct (imply_to_and _ _ C) as [D E]; clear C.
+  destruct (imply_to_and _ _ E) as [F G]; clear E.
+  destruct (not_or_and _ _ G) as [P Q]; clear G.
+  exists t1; exists s'. 
+  split. exists b2; auto. 
+  split. auto. 
+  split. red; intros; red; intros. elim Q. exists t; exists s'0; auto.
+  intros; red; intros. elim P. exists r; auto.
+Qed.
+
+Lemma backward_simulation_star:
+  forall s2 t s2', Star L2 s2 t s2' ->
+  forall i s1 b, S i s1 s2 -> safe_along_behavior s1 (behavior_app t b) ->
+  exists i', exists s1', Star L1 s1 t s1' /\ S i' s1' s2'.
+Proof.
+  induction 1; intros.
+  exists i; exists s1; split; auto. apply star_refl.
+  exploit (bsim_simulation S); eauto. eapply safe_along_safe; eauto. 
+  intros [i' [s1' [A B]]].
+  assert (Star L1 s0 t1 s1'). intuition. apply plus_star; auto.
+  exploit IHstar; eauto. eapply star_safe_along; eauto.
+  subst t; apply behavior_app_assoc.
+  intros [i'' [s2'' [C D]]].
+  exists i''; exists s2''; split; auto. eapply star_trans; eauto.
+Qed.
+
+Lemma backward_simulation_forever_silent:
+  forall i s1 s2,
+  Forever_silent L2 s2 -> S i s1 s2 -> safe L1 s1 ->
+  Forever_silent L1 s1.
+Proof.
+  assert (forall i s1 s2,
+         Forever_silent L2 s2 -> S i s1 s2 -> safe L1 s1 ->
+         forever_silent_N (step L1) (bsim_order S) (globalenv L1) i s1).
+    cofix COINDHYP; intros.
+    inv H.  destruct (bsim_simulation S _ _ _ H2 _ H0 H1) as [i' [s2' [A B]]].
+    destruct A as [C | [C D]].
+    eapply forever_silent_N_plus; eauto. eapply COINDHYP; eauto.
+      eapply star_safe; eauto. apply plus_star; auto.
+    eapply forever_silent_N_star; eauto. eapply COINDHYP; eauto.
+      eapply star_safe; eauto.
+  intros. eapply forever_silent_N_forever; eauto. apply bsim_order_wf.
+Qed.
+
+Lemma backward_simulation_forever_reactive:
+  forall i s1 s2 T,
+  Forever_reactive L2 s2 T -> S i s1 s2 -> safe_along_behavior s1 (Reacts T) ->
+  Forever_reactive L1 s1 T.
+Proof.
+  cofix COINDHYP; intros. inv H. 
+  destruct (backward_simulation_star H2 _ (Reacts T0) H0) as [i' [s1' [A B]]]; eauto.
+  econstructor; eauto. eapply COINDHYP; eauto. eapply star_safe_along; eauto. 
+Qed.
+
+Lemma backward_simulation_state_behaves:
+  forall i s1 s2 beh2,
+  S i s1 s2 -> state_behaves L2 s2 beh2 ->
+  exists beh1, state_behaves L1 s1 beh1 /\ behavior_improves beh1 beh2.
+Proof.
+  intros. destruct (classic (safe_along_behavior s1 beh2)).
+(* 1. Safe along *)
+  exists beh2; split; [idtac|apply behavior_improves_refl].
+  inv H0. 
+(* termination *)
+  assert (Terminates t r = behavior_app t (Terminates E0 r)).
+    simpl. rewrite E0_right; auto.
+  rewrite H0 in H1. 
+  exploit backward_simulation_star; eauto.
+  intros [i' [s1' [A B]]].
+  exploit (bsim_match_final_states S); eauto.
+    eapply safe_along_safe. eapply star_safe_along; eauto. 
+  intros [s1'' [C D]].
+  econstructor. eapply star_trans; eauto. traceEq. auto.
+(* silent divergence *)
+  assert (Diverges t = behavior_app t (Diverges E0)).
+    simpl. rewrite E0_right; auto.
+  rewrite H0 in H1. 
+  exploit backward_simulation_star; eauto.
+  intros [i' [s1' [A B]]].
+  econstructor. eauto. eapply backward_simulation_forever_silent; eauto. 
+  eapply safe_along_safe. eapply star_safe_along; eauto. 
+(* reactive divergence *)
+  econstructor. eapply backward_simulation_forever_reactive; eauto. 
+(* goes wrong *)
+  assert (Goes_wrong t = behavior_app t (Goes_wrong E0)).
+    simpl. rewrite E0_right; auto.
+  rewrite H0 in H1. 
+  exploit backward_simulation_star; eauto.
+  intros [i' [s1' [A B]]].
+  exploit (bsim_progress S); eauto. eapply safe_along_safe. eapply star_safe_along; eauto. 
+  intros [[r FIN] | [t' [s2' STEP2]]]. 
+  elim (H4 _ FIN).
+  elim (H3 _ _ STEP2).
+
+(* 2. Not safe along *)
+  exploit not_safe_along_behavior; eauto. 
+  intros [t [s1' [PREF [STEPS [NOSTEP NOFIN]]]]].
+  exists (Goes_wrong t); split.
+  econstructor; eauto. 
+  right. exists t; auto.
+Qed.
+
+Theorem backward_simulation_behavior_improves:
+  forall beh2, program_behaves L2 beh2 ->
+  exists beh1, program_behaves L1 beh1 /\ behavior_improves beh1 beh2.
+Proof.
+  intros. inv H.
+(* L2's initial state is defined. *)
+  destruct (classic (exists s1, initial_state L1 s1)) as [[s1 INIT] | NOINIT].
+(* L1's initial state is defined too. *)
+  exploit (bsim_match_initial_states S); eauto. intros [i [s1' [INIT1' MATCH]]].
+  exploit backward_simulation_state_behaves; eauto. intros [beh1 [A B]].
+  exists beh1; split; auto. econstructor; eauto.
+(* L1 has no initial state *)
+  exists (Goes_wrong E0); split.
+  apply program_goes_initially_wrong. 
+  intros; red; intros. elim NOINIT; exists s0; auto.
+  apply behavior_improves_bot.
+(* L2 has no initial state *)
+  exists (Goes_wrong E0); split.
+  apply program_goes_initially_wrong. 
+  intros; red; intros.
+  exploit (bsim_initial_states_exist S); eauto. intros [s2 INIT2]. 
+  elim (H0 s2); auto.
+  apply behavior_improves_refl.
+Qed.
+
+Corollary backward_simulation_same_safe_behavior:
+  (forall beh, program_behaves L1 beh -> not_wrong beh) ->
+  (forall beh, program_behaves L2 beh -> program_behaves L1 beh).
+Proof.
+  intros. exploit backward_simulation_behavior_improves; eauto. 
+  intros [beh' [A B]]. destruct B. 
+  congruence.
+  destruct H1 as [t [C D]]. subst. elim (H (Goes_wrong t)). auto.
+Qed.
+
+End BACKWARD_SIMULATIONS.
+
+(** * Additional results about infinite reduction sequences *)
+
+(** We now show that any infinite sequence of reductions is either of
+  the "reactive" kind or of the "silent" kind (after a finite number
+  of non-silent transitions).  The proof necessitates the axiom of
+  excluded middle.  This result is used below to relate
+  the coinductive big-step semantics for divergence with the
+  small-step notions of divergence. *)
+
+Unset Implicit Arguments.
+
+Section INF_SEQ_DECOMP.
+
+Variable genv: Type.
+Variable state: Type.
+Variable step: genv -> state -> trace -> state -> Prop.
+
+Variable ge: genv.
+
+Inductive tstate: Type :=
+  ST: forall (s: state) (T: traceinf), forever step ge s T -> tstate.
+
+Definition state_of_tstate (S: tstate): state :=
+  match S with ST s T F => s end.
+Definition traceinf_of_tstate (S: tstate) : traceinf :=
+  match S with ST s T F => T end.
+
+Inductive tstep: trace -> tstate -> tstate -> Prop :=
+  | tstep_intro: forall s1 t T s2 S F,
+      tstep t (ST s1 (t *** T) (@forever_intro genv state step ge s1 t s2 T S F))
+              (ST s2 T F).
+
+Inductive tsteps: tstate -> tstate -> Prop :=
+  | tsteps_refl: forall S, tsteps S S
+  | tsteps_left: forall t S1 S2 S3, tstep t S1 S2 -> tsteps S2 S3 -> tsteps S1 S3.
+
+Remark tsteps_trans:
+  forall S1 S2, tsteps S1 S2 -> forall S3, tsteps S2 S3 -> tsteps S1 S3.
+Proof.
+  induction 1; intros. auto. econstructor; eauto.
+Qed.
+
+Let treactive (S: tstate) : Prop :=
+  forall S1, 
+  tsteps S S1 ->
+  exists S2, exists S3, exists t, tsteps S1 S2 /\ tstep t S2 S3 /\ t <> E0.
+
+Let tsilent (S: tstate) : Prop :=
+  forall S1 t S2, tsteps S S1 -> tstep t S1 S2 -> t = E0.
+
+Lemma treactive_or_tsilent:
+  forall S, treactive S \/ (exists S', tsteps S S' /\ tsilent S').
+Proof.
+  intros. destruct (classic (exists S', tsteps S S' /\ tsilent S')).
+  auto.
+  left. red; intros. 
+  generalize (not_ex_all_not _ _ H S1). intros.
+  destruct (not_and_or _ _ H1). contradiction. 
+  unfold tsilent in H2. 
+  generalize (not_all_ex_not _ _ H2). intros [S2 A].
+  generalize (not_all_ex_not _ _ A). intros [t B].
+  generalize (not_all_ex_not _ _ B). intros [S3 C].
+  generalize (imply_to_and _ _ C). intros [D F].
+  generalize (imply_to_and _ _ F). intros [G J].
+  exists S2; exists S3; exists t. auto.  
+Qed.
+
+Lemma tsteps_star:
+  forall S1 S2, tsteps S1 S2 ->
+  exists t, star step ge (state_of_tstate S1) t (state_of_tstate S2)
+         /\ traceinf_of_tstate S1 = t *** traceinf_of_tstate S2.
+Proof.
+  induction 1.
+  exists E0; split. apply star_refl. auto.
+  inv H. destruct IHtsteps as [t' [A B]].
+  exists (t ** t'); split.
+  simpl; eapply star_left; eauto.
+  simpl in *. subst T. traceEq.
+Qed.
+
+Lemma tsilent_forever_silent:
+  forall S,
+  tsilent S -> forever_silent step ge (state_of_tstate S).
+Proof.
+  cofix COINDHYP; intro S. case S. intros until f. simpl. case f. intros.
+  assert (tstep t (ST s1 (t *** T0) (forever_intro s1 t s0 f0))
+                  (ST s2 T0 f0)). 
+    constructor.
+  assert (t = E0). 
+    red in H. eapply H; eauto. apply tsteps_refl.
+  apply forever_silent_intro with (state_of_tstate (ST s2 T0 f0)).
+  rewrite <- H1. assumption. 
+  apply COINDHYP. 
+  red; intros. eapply H. eapply tsteps_left; eauto. eauto. 
+Qed.
+
+Lemma treactive_forever_reactive:
+  forall S,
+  treactive S -> forever_reactive step ge (state_of_tstate S) (traceinf_of_tstate S).
+Proof.
+  cofix COINDHYP; intros.
+  destruct (H S) as [S1 [S2 [t [A [B C]]]]]. apply tsteps_refl. 
+  destruct (tsteps_star _ _ A) as [t' [P Q]].
+  inv B. simpl in *. rewrite Q. rewrite <- Eappinf_assoc. 
+  apply forever_reactive_intro with s2. 
+  eapply star_right; eauto. 
+  red; intros. destruct (Eapp_E0_inv _ _ H0). contradiction.
+  change (forever_reactive step ge (state_of_tstate (ST s2 T F)) (traceinf_of_tstate (ST s2 T F))).
+  apply COINDHYP. 
+  red; intros. apply H.
+  eapply tsteps_trans. eauto.
+  eapply tsteps_left. constructor. eauto.
+Qed.
+
+Theorem forever_silent_or_reactive:
+  forall s T,
+  forever step ge s T ->
+  forever_reactive step ge s T \/
+  exists t, exists s', exists T',
+  star step ge s t s' /\ forever_silent step ge s' /\ T = t *** T'.
+Proof.
+  intros. 
+  destruct (treactive_or_tsilent (ST s T H)).
+  left. 
+  change (forever_reactive step ge (state_of_tstate (ST s T H)) (traceinf_of_tstate (ST s T H))).
+  apply treactive_forever_reactive. auto.
+  destruct H0 as [S' [A B]].
+  exploit tsteps_star; eauto. intros [t [C D]]. simpl in *.
+  right. exists t; exists (state_of_tstate S'); exists (traceinf_of_tstate S').
+  split. auto. 
+  split. apply tsilent_forever_silent. auto.
+  auto.
+Qed.
+
+End INF_SEQ_DECOMP.
+
+Set Implicit Arguments.
+
+(** * Big-step semantics and program behaviors *)
+
+Section BIGSTEP_BEHAVIORS.
+
+Variable B: bigstep_semantics.
+Variable L: semantics.
+Hypothesis sound: bigstep_sound B L.
+
+Lemma behavior_bigstep_terminates:
+  forall t r,
+  bigstep_terminates B t r -> program_behaves L (Terminates t r).
+Proof.
+  intros. exploit (bigstep_terminates_sound sound); eauto. 
+  intros [s1 [s2 [P [Q R]]]].
+  econstructor; eauto. econstructor; eauto.
+Qed.
+
+Lemma behavior_bigstep_diverges:
+  forall T,
+  bigstep_diverges B T ->
+  program_behaves L (Reacts T)
+  \/ exists t, program_behaves L (Diverges t) /\ traceinf_prefix t T.
+Proof.
+  intros. exploit (bigstep_diverges_sound sound); eauto. intros [s1 [P Q]].
+  exploit forever_silent_or_reactive; eauto. intros [X | [t [s' [T' [X [Y Z]]]]]].
+  left. econstructor; eauto. constructor; auto.
+  right. exists t; split. econstructor; eauto. econstructor; eauto. exists T'; auto.
+Qed.
+
+End BIGSTEP_BEHAVIORS.
diff --git a/common/Determinism.v b/common/Determinism.v
index 00d8855..16e8890 100644
--- a/common/Determinism.v
+++ b/common/Determinism.v
@@ -20,6 +20,7 @@ Require Import Values.
 Require Import Events.
 Require Import Globalenvs.
 Require Import Smallstep.
+Require Import Behaviors.
 
 (** This file uses classical logic (the axiom of excluded middle), as
   well as the following extensionality property over infinite
@@ -80,7 +81,9 @@ Inductive possible_event: world -> event -> world -> Prop :=
       possible_event w1 (Event_vload chunk id ofs evres) w2
   | possible_event_vstore: forall w1 chunk id ofs evarg w2,
       nextworld_vstore w1 chunk id ofs evarg = Some w2 ->
-      possible_event w1 (Event_vstore chunk id ofs evarg) w2.
+      possible_event w1 (Event_vstore chunk id ofs evarg) w2
+  | possible_event_annot: forall w1 id args,
+      possible_event w1 (Event_annot id args) w1.
 
 Inductive possible_trace: world -> trace -> world -> Prop :=
   | possible_trace_nil: forall w,
@@ -110,6 +113,20 @@ Proof.
   exists w1; split. econstructor; eauto. auto.
 Qed.
 
+Lemma match_possible_traces:
+  forall (F V: Type) (ge: Genv.t F V) t1 t2 w0 w1 w2,
+  match_traces ge t1 t2 -> possible_trace w0 t1 w1 -> possible_trace w0 t2 w2 ->
+  t1 = t2 /\ w1 = w2.
+Proof.
+  intros. inv H; inv H1; inv H0.
+  auto.
+  inv H7; inv H6. inv H9; inv H10. split; congruence.
+  inv H7; inv H6. inv H9; inv H10. split; congruence.
+  inv H4; inv H3. inv H6; inv H7. split; congruence. 
+  inv H4; inv H3. inv H7; inv H6. auto.
+Qed.
+
+(*
 Lemma possible_event_final_world:
   forall w ev w1 w2,
   possible_event w ev w1 -> possible_event w ev w2 -> w1 = w2.
@@ -126,6 +143,7 @@ Proof.
   inv H1. assert (w2 = w5) by (eapply possible_event_final_world; eauto). 
   subst; eauto.
 Qed.
+*)
 
 CoInductive possible_traceinf: world -> traceinf -> Prop :=
   | possible_traceinf_cons: forall w1 ev w2 T,
@@ -200,46 +218,38 @@ Proof.
   inv H3. simpl. auto. econstructor; eauto. econstructor; eauto. unfold E0; congruence.
 Qed.
 
-(** * Properties of deterministic semantics *)
-
-Section DETERM_SEM.
+(** * Definition and properties of deterministic semantics *)
 
-(** We assume given a semantics that is deterministic, in the following sense. *)
-
-Variable genv: Type.
-Variable state: Type.
-Variable step: genv -> state -> trace -> state -> Prop.
-Variable initial_state: state -> Prop.
-Variable final_state: state -> int -> Prop.
+Record sem_deterministic (L: semantics) := mk_deterministic {
+  det_step: forall s0 t1 s1 t2 s2,
+    L (genv L) s0 t1 s1 -> L (genv L) s0 t2 s2 -> s1 = s2 /\ t1 = t2;
+  det_initial_state: forall s1 s2,
+    initial_state L s1 -> initial_state L s2 -> s1 = s2;
+  det_final_state: forall s r1 r2,
+    final_state L s r1 -> final_state L s r2 -> r1 = r2;
+  det_final_nostep: forall s r,
+    final_state L s r -> nostep L (genv L) s
+}.
 
-Hypothesis step_deterministic:
-  forall ge s0 t1 s1 t2 s2,
-  step ge s0 t1 s1 -> step ge s0 t2 s2 ->
-  s1 = s2 /\ t1 = t2.
-
-Hypothesis initial_state_determ:
-  forall s1 s2, initial_state s1 -> initial_state s2 -> s1 = s2.
-
-Hypothesis final_state_determ:
-  forall st r1 r2, final_state st r1 -> final_state st r2 -> r1 = r2.
+Section DETERM_SEM.
 
-Hypothesis final_state_nostep:
-  forall ge st r, final_state st r -> nostep step ge st.
+Variable L: semantics.
+Hypothesis DET: sem_deterministic L.
 
 Ltac use_step_deterministic :=
   match goal with
-  | [ S1: step _ _ ?t1 _, S2: step _ _ ?t2 _ |- _ ] =>
-    destruct (step_deterministic _ _ _ _ _ _ S1 S2) as [EQ1 EQ2]; subst
+  | [ S1: step L (genv L) _ ?t1 _, S2: step L (genv L) _ ?t2 _ |- _ ] =>
+    destruct (det_step L DET _ _ _ _ _ S1 S2) as [EQ1 EQ2]; subst
   end.
 
 (** Determinism for finite transition sequences. *)
 
 Lemma star_step_diamond:
-  forall ge s0 t1 s1, star step ge s0 t1 s1 -> 
-  forall t2 s2, star step ge s0 t2 s2 -> 
+  forall s0 t1 s1, star L (genv L) s0 t1 s1 -> 
+  forall t2 s2, star L (genv L) s0 t2 s2 -> 
   exists t,
-     (star step ge s1 t s2 /\ t2 = t1 ** t)
-  \/ (star step ge s2 t s1 /\ t1 = t2 ** t).
+     (star L (genv L) s1 t s2 /\ t2 = t1 ** t)
+  \/ (star L (genv L) s2 t s1 /\ t1 = t2 ** t).
 Proof.
   induction 1; intros. 
   exists t2; auto. 
@@ -252,24 +262,24 @@ Qed.
 
 Ltac use_star_step_diamond :=
   match goal with
-  | [ S1: star step _ _ ?t1 _, S2: star step _ _ ?t2 _ |- _ ] =>
+  | [ S1: star (step L) (genv L) _ ?t1 _, S2: star (step L) (genv L) _ ?t2 _ |- _ ] =>
     let t := fresh "t" in let P := fresh "P" in let EQ := fresh "EQ" in
-    destruct (star_step_diamond _ _ _ _ S1 _ _ S2)
+    destruct (star_step_diamond _ _ _ S1 _ _ S2)
     as [t [ [P EQ] | [P EQ] ]]; subst
  end.
 
 Ltac use_nostep :=
   match goal with
-  | [ S: step _ ?s _ _, NO: nostep step _ ?s |- _ ] => elim (NO _ _ S)
+  | [ S: step L (genv L) ?s _ _, NO: nostep (step L) (genv L) ?s |- _ ] => elim (NO _ _ S)
   end.
 
 Lemma star_step_triangle:
-  forall ge s0 t1 s1 t2 s2,
-  star step ge s0 t1 s1 -> 
-  star step ge s0 t2 s2 -> 
-  nostep step ge s2 ->
+  forall s0 t1 s1 t2 s2,
+  star L (genv L) s0 t1 s1 -> 
+  star L (genv L) s0 t2 s2 -> 
+  nostep L (genv L) s2 ->
   exists t,
-  star step ge s1 t s2 /\ t2 = t1 ** t.
+  star L (genv L) s1 t s2 /\ t2 = t1 ** t.
 Proof.
   intros. use_star_step_diamond.
   exists t; auto.
@@ -279,17 +289,17 @@ Qed.
 
 Ltac use_star_step_triangle :=
   match goal with
-  | [ S1: star step _ _ ?t1 _, S2: star step _ _ ?t2 ?s2,
-      NO: nostep step _ ?s2 |- _ ] =>
+  | [ S1: star (step L) (genv L) _ ?t1 _, S2: star (step L) (genv L) _ ?t2 ?s2,
+      NO: nostep (step L) (genv L) ?s2 |- _ ] =>
     let t := fresh "t" in let P := fresh "P" in let EQ := fresh "EQ" in
-    destruct (star_step_triangle _ _ _ _ _ _ S1 S2 NO)
+    destruct (star_step_triangle _ _ _ _ _ S1 S2 NO)
     as [t [P EQ]]; subst
   end.
 
 Lemma steps_deterministic:
-  forall ge s0 t1 s1 t2 s2,
-  star step ge s0 t1 s1 -> star step ge s0 t2 s2 -> 
-  nostep step ge s1 -> nostep step ge s2 ->
+  forall s0 t1 s1 t2 s2,
+  star L (genv L) s0 t1 s1 -> star L (genv L) s0 t2 s2 -> 
+  nostep L (genv L) s1 -> nostep L (genv L) s2 ->
   t1 = t2 /\ s1 = s2.
 Proof.
   intros. use_star_step_triangle. inv P.
@@ -297,23 +307,23 @@ Proof.
 Qed.
 
 Lemma terminates_not_goes_wrong:
-  forall ge s t1 s1 r t2 s2,
-  star step ge s t1 s1 -> final_state s1 r ->
-  star step ge s t2 s2 -> nostep step ge s2 ->
-  (forall r, ~final_state s2 r) -> False.
+  forall s t1 s1 r t2 s2,
+  star L (genv L) s t1 s1 -> final_state L s1 r ->
+  star L (genv L) s t2 s2 -> nostep L (genv L) s2 ->
+  (forall r, ~final_state L s2 r) -> False.
 Proof.
   intros.
   assert (t1 = t2 /\ s1 = s2). 
-    eapply steps_deterministic; eauto. 
+    eapply steps_deterministic; eauto. eapply det_final_nostep; eauto. 
   destruct H4; subst. elim (H3 _ H0).
 Qed.
 
 (** Determinism for infinite transition sequences. *)
 
 Lemma star_final_not_forever_silent:
-  forall ge s t s', star step ge s t s' ->
-  nostep step ge s' ->
-  forever_silent step ge s -> False.
+  forall s t s', star L (genv L) s t s' ->
+  nostep L (genv L) s' ->
+  forever_silent L (genv L) s -> False.
 Proof.
   induction 1; intros. 
   inv H0. use_nostep. 
@@ -321,9 +331,9 @@ Proof.
 Qed.
 
 Lemma star2_final_not_forever_silent:
-  forall ge s t1 s1 t2 s2,
-  star step ge s t1 s1 -> nostep step ge s1 ->
-  star step ge s t2 s2 -> forever_silent step ge s2 ->
+  forall s t1 s1 t2 s2,
+  star L (genv L) s t1 s1 -> nostep L (genv L) s1 ->
+  star L (genv L) s t2 s2 -> forever_silent L (genv L) s2 ->
   False.
 Proof.
   intros. use_star_step_triangle.
@@ -331,8 +341,8 @@ Proof.
 Qed.
 
 Lemma star_final_not_forever_reactive:
-  forall ge s t s', star step ge s t s' -> 
-  forall T, nostep step ge s' -> forever_reactive step ge s T -> False.
+  forall s t s', star L (genv L) s t s' -> 
+  forall T, nostep L (genv L) s' -> forever_reactive L (genv L) s T -> False.
 Proof.
   induction 1; intros.
   inv H0. inv H1. congruence. use_nostep. 
@@ -343,9 +353,9 @@ Proof.
 Qed.
 
 Lemma star_forever_silent_inv:
-  forall ge s t s', star step ge s t s' ->
-  forever_silent step ge s -> 
-  t = E0 /\ forever_silent step ge s'.
+  forall s t s', star L (genv L) s t s' ->
+  forever_silent L (genv L) s -> 
+  t = E0 /\ forever_silent L (genv L) s'.
 Proof.
   induction 1; intros.
   auto.
@@ -353,24 +363,24 @@ Proof.
 Qed.
 
 Lemma forever_silent_reactive_exclusive:
-  forall ge s T,
-  forever_silent step ge s -> forever_reactive step ge s T -> False.
+  forall s T,
+  forever_silent L (genv L) s -> forever_reactive L (genv L) s T -> False.
 Proof.
   intros. inv H0. exploit star_forever_silent_inv; eauto. 
   intros [A B]. contradiction.
 Qed.
 
 Lemma forever_reactive_inv2:
-  forall ge s t1 s1, star step ge s t1 s1 ->
+  forall s t1 s1, star L (genv L) s t1 s1 ->
   forall t2 s2 T1 T2,
-  star step ge s t2 s2 ->
+  star L (genv L) s t2 s2 ->
   t1 <> E0 -> t2 <> E0 ->
-  forever_reactive step ge s1 T1 ->
-  forever_reactive step ge s2 T2 ->
+  forever_reactive L (genv L) s1 T1 ->
+  forever_reactive L (genv L) s2 T2 ->
   exists s', exists t, exists T1', exists T2',
   t <> E0 /\
-  forever_reactive step ge s' T1' /\
-  forever_reactive step ge s' T2' /\
+  forever_reactive L (genv L) s' T1' /\
+  forever_reactive L (genv L) s' T2' /\
   t1 *** T1 = t *** T1' /\
   t2 *** T2 = t *** T2'.
 Proof.
@@ -390,32 +400,32 @@ Proof.
 Qed.
 
 Lemma forever_reactive_determ':
-  forall ge s T1 T2,
-  forever_reactive step ge s T1 ->
-  forever_reactive step ge s T2 ->
+  forall s T1 T2,
+  forever_reactive L (genv L) s T1 ->
+  forever_reactive L (genv L) s T2 ->
   traceinf_sim' T1 T2.
 Proof.
   cofix COINDHYP; intros.
   inv H. inv H0.
-  destruct (forever_reactive_inv2 _ _ _ _ H t s2 T0 T)
+  destruct (forever_reactive_inv2 _ _ _ H t s2 T0 T)
   as [s' [t' [T1' [T2' [A [B [C [D E]]]]]]]]; auto.
   rewrite D; rewrite E. constructor. auto. 
   eapply COINDHYP; eauto. 
 Qed.
 
 Lemma forever_reactive_determ:
-  forall ge s T1 T2,
-  forever_reactive step ge s T1 ->
-  forever_reactive step ge s T2 ->
+  forall s T1 T2,
+  forever_reactive L (genv L) s T1 ->
+  forever_reactive L (genv L) s T2 ->
   traceinf_sim T1 T2.
 Proof.
   intros. apply traceinf_sim'_sim. eapply forever_reactive_determ'; eauto.
 Qed.
 
 Lemma star_forever_reactive_inv:
-  forall ge s t s', star step ge s t s' ->
-  forall T, forever_reactive step ge s T ->
-  exists T', forever_reactive step ge s' T' /\ T = t *** T'.
+  forall s t s', star L (genv L) s t s' ->
+  forall T, forever_reactive L (genv L) s T ->
+  exists T', forever_reactive L (genv L) s' T' /\ T = t *** T'.
 Proof.
   induction 1; intros. 
   exists T; auto.
@@ -426,9 +436,9 @@ Proof.
 Qed.
 
 Lemma forever_silent_reactive_exclusive2:
-  forall ge s t s' T,
-  star step ge s t s' -> forever_silent step ge s' ->
-  forever_reactive step ge s T ->
+  forall s t s' T,
+  star L (genv L) s t s' -> forever_silent L (genv L) s' ->
+  forever_reactive L (genv L) s T ->
   False.
 Proof.
   intros. exploit star_forever_reactive_inv; eauto. 
@@ -438,26 +448,16 @@ Qed.
 
 (** Determinism for program executions *)
 
-Ltac use_init_state :=
-  match goal with
-  | [ H1: (initial_state _), H2: (initial_state _) |- _ ] =>
-        generalize (initial_state_determ _ _ H1 H2); intro; subst; clear H2
-  | [ H1: (initial_state _), H2: (forall s, ~initial_state s) |- _ ] =>
-        elim (H2 _ H1)
-  | _ => idtac
-  end.
-
-Theorem program_behaves_deterministic:
-  forall ge beh1 beh2,
-  program_behaves step initial_state final_state ge beh1 ->
-  program_behaves step initial_state final_state ge beh2 ->
-  beh1 = beh2.
+Lemma state_behaves_deterministic:
+  forall s beh1 beh2,
+  state_behaves L s beh1 -> state_behaves L s beh2 -> beh1 = beh2.
 Proof.
+  generalize (det_final_nostep L DET); intro dfns.
   intros until beh2; intros BEH1 BEH2.
-  inv BEH1; inv BEH2; use_init_state.
+  inv BEH1; inv BEH2.
 (* terminates, terminates *)
   assert (t = t0 /\ s' = s'0). eapply steps_deterministic; eauto.
-  destruct H2. f_equal; auto. subst. eauto. 
+  destruct H3. f_equal; auto. subst. eapply det_final_state; eauto. 
 (* terminates, diverges *)
   byContradiction. eapply star2_final_not_forever_silent with (s1 := s') (s2 := s'0); eauto.
 (* terminates, reacts *)
@@ -493,9 +493,23 @@ Proof.
   byContradiction. eapply star_final_not_forever_reactive; eauto.
 (* goes wrong, goes wrong *)
   assert (t = t0 /\ s' = s'0). eapply steps_deterministic; eauto.
-  destruct H3. congruence.
-(* goes initially wrong, goes initially wrong *)
-  reflexivity.
+  destruct H5. congruence.
+Qed.
+
+Theorem program_behaves_deterministic:
+  forall beh1 beh2,
+  program_behaves L beh1 -> program_behaves L beh2 ->
+  beh1 = beh2.
+Proof.
+  intros until beh2; intros BEH1 BEH2. inv BEH1; inv BEH2.
+(* both initial states defined *)
+  assert (s = s0) by (eapply det_initial_state; eauto). subst s0. 
+  eapply state_behaves_deterministic; eauto.
+(* one initial state defined, the other undefined *)
+  elim (H1 _ H).
+  elim (H _ H0).
+(* both initial states undefined *)
+  auto.
 Qed.
 
 End DETERM_SEM.
@@ -508,6 +522,48 @@ End DETERM_SEM.
 
 Section WORLD_SEM.
 
+Variable L: semantics.
+Variable initial_world: world.
+
+Notation "s #1" := (fst s) (at level 9, format "s '#1'") : pair_scope.
+Notation "s #2" := (snd s) (at level 9, format "s '#2'") : pair_scope.
+Local Open Scope pair_scope.
+
+Definition world_sem : semantics := @mk_semantics
+  (state L * world)%type
+  (funtype L)
+  (vartype L)
+  (fun ge s t s' => L ge s#1 t s'#1 /\ possible_trace s#2 t s'#2)
+  (fun s => initial_state L s#1 /\ s#2 = initial_world)
+  (fun s r => final_state L s#1 r)
+  (genv L).
+
+(** If the original semantics is determinate, the world-aware semantics is deterministic. *)
+
+Hypothesis D: sem_determinate L.
+
+Theorem world_sem_deterministic: sem_deterministic world_sem.
+Proof.
+  constructor; simpl; intros.
+(* steps *)
+  destruct H; destruct H0.
+  exploit (sd_match D). eexact H. eexact H0. intros MT.
+  exploit match_possible_traces; eauto. intros [EQ1 EQ2]. subst t2.
+  exploit (sd_determ D). eexact H. eexact H0. intros EQ3. 
+  split; auto. rewrite (surjective_pairing s1). rewrite (surjective_pairing s2). congruence.
+(* initial states *)
+  destruct H; destruct H0.
+  rewrite (surjective_pairing s1). rewrite (surjective_pairing s2). decEq. 
+  eapply (sd_initial_determ D); eauto. 
+  congruence.
+(* final states *)
+  eapply (sd_final_determ D); eauto.
+(* final no step *)
+  red; simpl; intros. red; intros [A B]. exploit (sd_final_nostep D); eauto. 
+Qed.
+
+
+
 Variable genv: Type.
 Variable state: Type.
 Variable step: genv -> state -> trace -> state -> Prop.
@@ -517,9 +573,6 @@ Variable initial_world: world.
 
 Definition wstate : Type := (state * world)%type.
 
-Notation "s #1" := (fst s) (at level 9, format "s '#1'") : pair_scope.
-Notation "s #2" := (snd s) (at level 9, format "s '#2'") : pair_scope.
-Local Open Scope pair_scope.
 
 Definition wstep (ge: genv) (S: wstate) (t: trace) (S': wstate) :=
   step ge S#1 t S'#1 /\ possible_trace S#2 t S'#2.
diff --git a/common/Events.v b/common/Events.v
index 2e57922..3948640 100644
--- a/common/Events.v
+++ b/common/Events.v
@@ -177,26 +177,6 @@ Transparent E0.
   constructor. unfold E0; congruence. auto.
 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_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.
-
 (** An alternate presentation of infinite traces as
   infinite concatenations of nonempty finite traces. *)
 
@@ -248,6 +228,30 @@ Transparent Eappinf.
   simpl. f_equal. apply IHt. 
 Qed.
 
+(** Prefixes of traces. *)
+
+Definition trace_prefix (t1 t2: trace) :=
+  exists t3, t2 = t1 ** t3.
+
+Definition traceinf_prefix (t1: trace) (T2: traceinf) :=
+  exists T3, T2 = t1 *** T3.
+
+Lemma trace_prefix_app:
+  forall t1 t2 t,
+  trace_prefix t1 t2 ->
+  trace_prefix (t ** t1) (t ** t2).
+Proof.
+  intros. destruct H as [t3 EQ]. exists t3. traceEq. 
+Qed.
+
+Lemma traceinf_prefix_app:
+  forall t1 T2 t,
+  traceinf_prefix t1 T2 ->
+  traceinf_prefix (t ** t1) (t *** T2).
+Proof.
+  intros. destruct H as [T3 EQ]. exists T3. subst T2. traceEq.
+Qed.
+
 (** * Relating values and event values *)
 
 Set Implicit Arguments.
@@ -370,6 +374,39 @@ Proof.
   eapply eventval_match_determ_2; eauto.
 Qed.
 
+(** Validity *)
+
+Definition eventval_valid (ev: eventval) : Prop :=
+  match ev with
+  | EVint _ => True
+  | EVfloat _ => True
+  | EVptr_global id ofs => exists b, Genv.find_symbol ge id = Some b
+  end.
+
+Definition eventval_type (ev: eventval) : typ :=
+  match ev with
+  | EVint _ => Tint
+  | EVfloat _ => Tfloat
+  | EVptr_global id ofs => Tint
+  end.
+
+Lemma eventval_valid_match:
+  forall ev ty,
+  eventval_valid ev -> eventval_type ev = ty -> exists v, eventval_match ev ty v.
+Proof.
+  intros. subst ty. destruct ev; simpl in *.
+  exists (Vint i); constructor.
+  exists (Vfloat f0); constructor.
+  destruct H as [b A]. exists (Vptr b i0); constructor; auto.
+Qed.
+
+Lemma eventval_match_valid:
+  forall ev ty v,
+  eventval_match ev ty v -> eventval_valid ev /\ eventval_type ev = ty.
+Proof.
+  induction 1; simpl; auto. split; auto. exists b; auto.
+Qed.
+
 End EVENTVAL.
 
 (** Invariance under changes to the global environment *)
@@ -397,8 +434,62 @@ Proof.
   induction 1; constructor; auto. eapply eventval_match_preserved; eauto.
 Qed.
 
+Lemma eventval_valid_preserved:
+  forall ev, eventval_valid ge1 ev -> eventval_valid ge2 ev.
+Proof.
+  unfold eventval_valid; destruct ev; auto. 
+  intros [b A]. exists b; rewrite symbols_preserved; auto.
+Qed.
+
 End EVENTVAL_INV.
 
+(** * Matching traces. *)
+
+Section MATCH_TRACES.
+
+Variables F V: Type.
+Variable ge: Genv.t F V.
+
+(** Matching between traces corresponding to single transitions.
+  Arguments (provided by the program) must be equal.
+  Results (provided by the outside world) can vary as long as they
+  can be converted safely to values. *)
+
+Inductive match_traces: trace -> trace -> Prop :=
+  | match_traces_E0:
+      match_traces nil nil
+  | match_traces_syscall: forall id args res1 res2,
+      eventval_valid ge res1 -> eventval_valid ge res2 -> eventval_type res1 = eventval_type res2 ->
+      match_traces (Event_syscall id args res1 :: nil) (Event_syscall id args res2 :: nil)
+  | match_traces_vload: forall chunk id ofs res1 res2,
+      eventval_valid ge res1 -> eventval_valid ge res2 -> eventval_type res1 = eventval_type res2 ->
+      match_traces (Event_vload chunk id ofs res1 :: nil) (Event_vload chunk id ofs res2 :: nil)
+  | match_traces_vstore: forall chunk id ofs arg,
+      match_traces (Event_vstore chunk id ofs arg :: nil) (Event_vstore chunk id ofs arg :: nil)
+  | match_traces_annot: forall id args,
+      match_traces (Event_annot id args :: nil) (Event_annot id args :: nil).
+
+End MATCH_TRACES.
+
+(** Invariance by change of global environment *)
+
+Section MATCH_TRACES_INV.
+
+Variables F1 V1 F2 V2: Type.
+Variable ge1: Genv.t F1 V1.
+Variable ge2: Genv.t F2 V2.
+
+Hypothesis symbols_preserved:
+  forall id, Genv.find_symbol ge2 id = Genv.find_symbol ge1 id.
+
+Lemma match_traces_preserved:
+  forall t1 t2, match_traces ge1 t1 t2 -> match_traces ge2 t1 t2.
+Proof.
+  induction 1; constructor; auto; eapply eventval_valid_preserved; eauto.
+Qed.
+
+End MATCH_TRACES_INV.
+
 (** * Semantics of external functions *)
 
 (** For each external function, its behavior is defined by a predicate relating:
@@ -439,20 +530,6 @@ Definition inject_separated (f f': meminj) (m1 m2: mem): Prop :=
   f b1 = None -> f' b1 = Some(b2, delta) ->
   ~Mem.valid_block m1 b1 /\ ~Mem.valid_block m2 b2.
 
-Fixpoint matching_traces (t1 t2: trace) {struct t1} : Prop :=
-  match t1, t2 with
-  | Event_syscall name1 args1 res1 :: t1', Event_syscall name2 args2 res2 :: t2' =>
-      name1 = name2 /\ args1 = args2 -> res1 = res2 /\ matching_traces t1' t2'
-  | Event_vload chunk1 id1 ofs1 res1 :: t1', Event_vload chunk2 id2 ofs2 res2 :: t2' =>
-      chunk1 = chunk2 /\ id1 = id2 /\ ofs1 = ofs2 -> res1 = res2 /\ matching_traces t1' t2'
-  | Event_vstore chunk1 id1 ofs1 arg1 :: t1', Event_vstore chunk2 id2 ofs2 arg2 :: t2' =>
-      chunk1 = chunk2 /\ id1 = id2 /\ ofs1 = ofs2 /\ arg1 = arg2 -> matching_traces t1' t2'
-  | Event_annot txt1 args1 :: t1', Event_annot txt2 args2 :: t2' =>
-      txt1 = txt2 /\ args1 = args2 -> matching_traces t1' t2'
-  | _, _ =>
-      True
-  end.
-
 Definition block_is_volatile (F V: Type) (ge: Genv.t F V) (b: block) : bool :=
   match Genv.find_var_info ge b with
   | None => false
@@ -525,13 +602,22 @@ Record extcall_properties (sem: extcall_sem)
     /\ inject_incr f f'
     /\ inject_separated f f' m1 m1';
 
-(** External calls must be internally deterministic:
-  if the observable traces match, the return states must be
-  identical. *)
+(** External calls produce at most one event. *)
+  ec_trace_length:
+    forall F V ge vargs m t vres m',
+    sem F V ge vargs m t vres m' -> (length t <= 1)%nat;
+
+(** External calls must be receptive to changes of traces by another, matching trace. *)
+  ec_receptive:
+    forall F V ge vargs m t1 vres1 m1 t2,
+    sem F V ge vargs m t1 vres1 m1 -> match_traces ge t1 t2 ->
+    exists vres2, exists m2, sem F V ge vargs m t2 vres2 m2;
+
+(** External calls must be deterministic up to matching between traces. *)
   ec_determ:
     forall F V ge vargs m t1 vres1 m1 t2 vres2 m2,
     sem F V ge vargs m t1 vres1 m1 -> sem F V ge vargs m t2 vres2 m2 ->
-    matching_traces t1 t2 -> t1 = t2 /\ vres1 = vres2 /\ m1 = m2
+    match_traces ge t1 t2 /\ (t1 = t2 -> vres1 = vres2 /\ m1 = m2)
 }.
 
 (** ** Semantics of volatile loads *)
@@ -573,21 +659,21 @@ Lemma volatile_load_ok:
                      (mksignature (Tint :: nil) (Some (type_of_chunk chunk))).
 Proof.
   intros; constructor; intros.
-
+(* well typed *)
   unfold proj_sig_res; simpl. destruct H.
   destruct chunk; destruct v; simpl; constructor.
   eapply Mem.load_type; eauto. 
-
+(* arity *)
   destruct H; simpl; auto.
-
+(* symbols *)
   destruct H1. 
   econstructor; eauto. rewrite H; auto. eapply eventval_match_preserved; eauto. 
   econstructor; eauto.
-
+(* valid blocks *)
   destruct H; auto.
-
+(* bounds *)
   destruct H; auto.
-
+(* mem extends *)
   destruct H. 
   inv H1. inv H8. inv H6. 
   exists (Val.load_result chunk v); exists m1'; intuition.
@@ -598,7 +684,7 @@ Proof.
   exists v'; exists m1'; intuition.
   econstructor; eauto.
   red; auto.
-
+(* mem injects *)
   destruct H0.
   inv H2. inv H9. inv H7.
   generalize H; intros [P [Q R]].
@@ -618,13 +704,25 @@ Proof.
   red; auto.
   red; auto.
   red; intros. congruence.
-
+(* trace length *)
+  inv H; simpl; omega.
+(* receptive *)
+  inv H; inv H0.
+  exploit eventval_match_valid; eauto. intros [A B]. 
+  exploit eventval_valid_match. eexact H9. rewrite <- H10; eauto. 
+  intros [v' EVM]. exists (Val.load_result chunk v'); exists m1.
+  eapply volatile_load_sem_vol; eauto. 
+  exists vres1; exists m1; eapply volatile_load_sem_nonvol; eauto.
+(* determ *)
   inv H; inv H0; try congruence.
   assert (id = id0) by (eapply Genv.genv_vars_inj; eauto). subst id0.
-  assert (ev = ev0) by (red in H1; tauto). subst ev0.
+  exploit eventval_match_valid. eexact H3. intros [V1 T1].
+  exploit eventval_match_valid. eexact H11. intros [V2 T2].
+  split. constructor; auto. congruence.
+  intros EQ; inv EQ. 
   assert (v = v0) by (eapply eventval_match_determ_1; eauto). subst v0.
   auto.
-  intuition congruence.
+  split. constructor. intuition congruence.
 Qed.
 
 (** ** Semantics of volatile stores *)
@@ -652,19 +750,19 @@ Lemma volatile_store_ok:
                      (mksignature (Tint :: type_of_chunk chunk :: nil) None).
 Proof.
   intros; constructor; intros.
-
+(* well typed *)
   unfold proj_sig_res; simpl. inv H; constructor.
-
+(* arity *)
   inv H; simpl; auto.
-
+(* symbols preserved *)
   inv H1. 
   constructor. rewrite H; auto. rewrite H0; auto. eapply eventval_match_preserved; eauto.
   constructor; auto. rewrite H0; auto.
-
+(* valid block *)
   inv H. auto. eauto with mem.
-
+(* bounds *)
   inv H. auto. eapply Mem.bounds_store; eauto.
-
+(* mem extends*)
   inv H.
   inv H1. inv H6. inv H8. inv H7.
   exists Vundef; exists m1'; intuition.
@@ -687,7 +785,7 @@ Proof.
                               (Int.unsigned ofs, Int.unsigned ofs + size_chunk chunk)).
   red; intros. generalize (H x H5). unfold loc_out_of_bounds, Intv.In; simpl. omega.
   simpl; omega. simpl; omega.
-
+(* mem injects *)
   inv H0.
   inv H2. inv H7. inv H9. inv H10.
   generalize H; intros [P [Q R]].
@@ -724,12 +822,17 @@ Proof.
   red; intros. exploit (H2 x H8). eauto. unfold Intv.In; simpl. omega.
   simpl; omega. simpl; omega.
   red; intros; congruence.
-
+(* trace length *)
+  inv H; simpl; omega.
+(* receptive *)
+  assert (t1 = t2). inv H; inv H0; auto. 
+  exists vres1; exists m1; congruence.
+(* determ *)
   inv H; inv H0; try congruence.
   assert (id = id0) by (eapply Genv.genv_vars_inj; eauto). subst id0.
   assert (ev = ev0) by (eapply eventval_match_determ_2; eauto). subst ev0.
-  auto.
-  intuition congruence.
+  split. constructor. auto.
+  split. constructor. intuition congruence.
 Qed.
 
 (** ** Semantics of dynamic memory allocation (malloc) *)
@@ -758,20 +861,20 @@ Proof.
   eapply Mem.load_alloc_other; eauto. 
 
   constructor; intros.
-
+(* well typed *)
   inv H. unfold proj_sig_res; simpl. auto.
-
+(* arity *)
   inv H. auto.
-
+(* symbols preserved *)
   inv H1; econstructor; eauto.
-
+(* valid block *)
   inv H. eauto with mem.
-
+(* bounds *)
   inv H. transitivity (Mem.bounds m' b).
   eapply Mem.bounds_store; eauto.
   eapply Mem.bounds_alloc_other; eauto.
   apply Mem.valid_not_valid_diff with m1; eauto with mem.
-
+(* mem extends *)
   inv H. inv H1. inv H5. inv H7. 
   exploit Mem.alloc_extends; eauto. apply Zle_refl. apply Zle_refl.
   intros [m3' [A B]].
@@ -781,7 +884,7 @@ Proof.
   exists (Vptr b Int.zero); exists m2'; intuition.
   econstructor; eauto.
   eapply UNCHANGED; eauto.
-
+(* mem injects *)
   inv H0. inv H2. inv H6. inv H8.
   exploit Mem.alloc_parallel_inject; eauto. apply Zle_refl. apply Zle_refl. 
   intros [f' [m3' [b' [ALLOC [A [B [C D]]]]]]].
@@ -796,8 +899,13 @@ Proof.
   red; intros. destruct (eq_block b1 b). 
   subst b1. rewrite C in H2. inv H2. eauto with mem. 
   rewrite D in H2. congruence. auto. 
-
-  inv H; inv H0. intuition congruence. 
+(* trace length *)
+  inv H; simpl; omega.
+(* receptive *)
+  assert (t1 = t2). inv H; inv H0; auto. subst t2.
+  exists vres1; exists m1; auto.
+(* determ *)
+  inv H; inv H0. split. constructor. intuition congruence. 
 Qed.
 
 (** ** Semantics of dynamic memory deallocation (free) *)
@@ -830,17 +938,17 @@ Proof.
   simpl; omega.
 
   constructor; intros.
-
+(* well typed *)
   inv H. unfold proj_sig_res. simpl. auto.
-
+(* arity *)
   inv H. auto.
-
+(* symbols preserved *)
   inv H1; econstructor; eauto.
-
+(* valid block *)
   inv H. eauto with mem.
-
+(* bounds *)
   inv H. eapply Mem.bounds_free; eauto.
-
+(* mem extends *)
   inv H. inv H1. inv H8. inv H6. 
   exploit Mem.load_extends; eauto. intros [vsz [A B]]. inv B. 
   exploit Mem.free_parallel_extends; eauto. intros [m2' [C D]].
@@ -851,7 +959,7 @@ Proof.
   red in H.
   exploit Mem.range_perm_in_bounds. 
   eapply Mem.free_range_perm. eexact H4. omega. omega.
-
+(* mem inject *)
   inv H0. inv H2. inv H7. inv H9.
   exploit Mem.load_inject; eauto. intros [vsz [A B]]. inv B. 
   assert (Mem.range_perm m1 b (Int.unsigned lo - 4) (Int.unsigned lo + Int.unsigned sz) Freeable).
@@ -895,8 +1003,13 @@ Proof.
   exploit Mem.range_perm_in_bounds. eexact H0. omega. intros. omega.
 
   red; intros. congruence.
-
-  inv H; inv H0. intuition congruence.
+(* trace length *)
+  inv H; simpl; omega.
+(* receptive *)
+  assert (t1 = t2). inv H; inv H0; auto. subst t2.
+  exists vres1; exists m1; auto.
+(* determ *)
+  inv H; inv H0. split. constructor. intuition congruence.
 Qed.
 
 (** ** Semantics of [memcpy] operations. *)
@@ -1015,8 +1128,14 @@ Proof.
   omega.
   split. apply inject_incr_refl.
   red; intros; congruence.
-(* determinism *)
-  intros. inv H; inv H0. split. auto. split. auto. congruence.
+(* trace length *)
+  intros; inv H. simpl; omega.
+(* receptive *)
+  intros. 
+  assert (t1 = t2). inv H; inv H0; auto. subst t2.
+  exists vres1; exists m1; auto.
+(* determ *)
+  intros; inv H; inv H0. split. constructor. intros; split; congruence.
 Qed.
 
 (** ** Semantics of system calls. *)
@@ -1033,25 +1152,25 @@ Lemma extcall_io_ok:
   extcall_properties (extcall_io_sem name sg) sg.
 Proof.
   intros; constructor; intros.
-
+(* well typed *)
   inv H. eapply eventval_match_type; eauto.
-
+(* arity *)
   inv H. eapply eventval_list_match_length; eauto.
-
+(* symbols preserved *)
   inv H1. econstructor; eauto. 
   eapply eventval_list_match_preserved; eauto.
   eapply eventval_match_preserved; eauto. 
-
+(* valid block *)
   inv H; auto.
-
+(* bounds *)
   inv H; auto.
-
+(* mem extends *)
   inv H.
   exists vres; exists m1'; intuition.
   econstructor; eauto.
   eapply eventval_list_match_lessdef; eauto.
   red; auto.
-
+(* mem injects *)
   inv H0.
   exists f; exists vres; exists m1'; intuition.
   econstructor; eauto.
@@ -1060,11 +1179,20 @@ Proof.
   red; auto.
   red; auto.
   red; intros; congruence.
-
-  inv H; inv H0. simpl in H1.
+(* trace length *)
+  inv H; simpl; omega.
+(* receptive *)
+  inv H; inv H0.
+  exploit eventval_match_valid; eauto. intros [A B]. 
+  exploit eventval_valid_match. eexact H7. rewrite <- H8; eauto. 
+  intros [v' EVM]. exists v'; exists m1. econstructor; eauto. 
+(* determ *)
+  inv H; inv H0.
   assert (args = args0). eapply eventval_list_match_determ_2; eauto. subst args0.
-  assert (res = res0). tauto. subst res0.
-  intuition. eapply eventval_match_determ_1; eauto.
+  exploit eventval_match_valid. eexact H2. intros [V1 T1].
+  exploit eventval_match_valid. eexact H3. intros [V2 T2].
+  split. constructor; auto. congruence.
+  intros EQ; inv EQ. split; auto. eapply eventval_match_determ_1; eauto.
 Qed.
 
 (** ** Semantics of annotation. *)
@@ -1080,24 +1208,24 @@ Lemma extcall_annot_ok:
   extcall_properties (extcall_annot_sem text targs) (mksignature targs None).
 Proof.
   intros; constructor; intros.
-
+(* well typed *)
   inv H. simpl. auto.
-
+(* arity *)
   inv H. eapply eventval_list_match_length; eauto.
-
+(* symbols *)
   inv H1. econstructor; eauto. 
   eapply eventval_list_match_preserved; eauto.
-
+(* valid blocks *)
   inv H; auto.
-
+(* bounds *)
   inv H; auto.
-
+(* mem extends *)
   inv H.
   exists Vundef; exists m1'; intuition.
   econstructor; eauto.
   eapply eventval_list_match_lessdef; eauto.
   red; auto.
-
+(* mem injects *)
   inv H0.
   exists f; exists Vundef; exists m1'; intuition.
   econstructor; eauto.
@@ -1105,10 +1233,15 @@ Proof.
   red; auto.
   red; auto.
   red; intros; congruence.
-
-  inv H; inv H0. simpl in H1.
+(* trace length *)
+  inv H; simpl; omega.
+(* receptive *)
+  assert (t1 = t2). inv H; inv H0; auto. 
+  exists vres1; exists m1; congruence.
+(* determ *)
+  inv H; inv H0.
   assert (args = args0). eapply eventval_list_match_determ_2; eauto. subst args0.
-  intuition.
+  split. constructor. auto.
 Qed.
 
 Inductive extcall_annot_val_sem (text: ident) (targ: typ) (F V: Type) (ge: Genv.t F V):
@@ -1148,9 +1281,14 @@ Proof.
   red; auto.
   red; intros; congruence.
 
-  inv H; inv H0. simpl in H1.
+  inv H; simpl; omega.
+
+  assert (t1 = t2). inv H; inv H0; auto. subst t2.
+  exists vres1; exists m1; auto.
+
+  inv H; inv H0.
   assert (arg = arg0). eapply eventval_match_determ_2; eauto. subst arg0.
-  intuition.
+  split. constructor. auto.
 Qed.
 
 (** ** Combined semantics of external calls *)
@@ -1202,6 +1340,8 @@ Definition external_call_valid_block ef := ec_valid_block (external_call_spec ef
 Definition external_call_bounds ef := ec_bounds (external_call_spec ef).
 Definition external_call_mem_extends ef := ec_mem_extends (external_call_spec ef).
 Definition external_call_mem_inject ef := ec_mem_inject (external_call_spec ef).
+Definition external_call_trace_length ef := ec_trace_length (external_call_spec ef).
+Definition external_call_receptive ef := ec_receptive (external_call_spec ef).
 Definition external_call_determ ef := ec_determ (external_call_spec ef).
 
 (** Special cases of [external_call_symbols_preserved_gen]. *)
@@ -1251,3 +1391,24 @@ Proof.
   instantiate (1 := Mem.nextblock m1 - 1). red; omega.
   unfold Mem.valid_block. omega.
 Qed.
+
+(** Corollaries of [external_call_determ]. *)
+
+Lemma external_call_match_traces:
+  forall ef (F V : Type) (ge : Genv.t F V) vargs m t1 vres1 m1 t2 vres2 m2,
+  external_call ef ge vargs m t1 vres1 m1 ->
+  external_call ef ge vargs m t2 vres2 m2 ->
+  match_traces ge t1 t2.
+Proof.
+  intros. exploit external_call_determ. eexact H. eexact H0. tauto.
+Qed.
+
+Lemma external_call_deterministic:
+  forall ef (F V : Type) (ge : Genv.t F V) vargs m t vres1 m1 vres2 m2,
+  external_call ef ge vargs m t vres1 m1 ->
+  external_call ef ge vargs m t vres2 m2 ->
+  vres1 = vres2 /\ m1 = m2.
+Proof.
+  intros. exploit external_call_determ. eexact H. eexact H0. intuition.
+Qed.
+
diff --git a/common/Smallstep.v b/common/Smallstep.v
index 63426c1..63ab5ea 100644
--- a/common/Smallstep.v
+++ b/common/Smallstep.v
@@ -19,8 +19,8 @@
   the one-step transition relations that are used to specify
   operational semantics in small-step style. *)
 
-Require Import Wf.
-Require Import Wf_nat.
+Require Import Relations.
+Require Import Wellfounded.
 Require Import Coqlib.
 Require Import AST.
 Require Import Events.
@@ -114,6 +114,20 @@ Proof.
   intros. eapply star_trans. eauto. apply star_one. eauto. auto.
 Qed.
 
+Lemma star_E0_ind:
+  forall ge (P: state -> state -> Prop),
+  (forall s, P s s) ->
+  (forall s1 s2 s3, step ge s1 E0 s2 -> P s2 s3 -> P s1 s3) ->
+  forall s1 s2, star ge s1 E0 s2 -> P s1 s2.
+Proof.
+  intros ge P BASE REC. 
+  assert (forall s1 t s2, star ge s1 t s2 -> t = E0 -> P s1 s2).
+    induction 1; intros; subst.
+    auto.
+    destruct (Eapp_E0_inv _ _ H2). subst. eauto.
+  eauto.
+Qed. 
+
 (** One or several transitions.  Also known as the transitive closure. *)
 
 Inductive plus (ge: genv): state -> trace -> state -> Prop :=
@@ -232,6 +246,56 @@ Proof.
   intros. inv H. left; auto. right; econstructor; eauto.
 Qed.
 
+Lemma plus_ind2:
+  forall ge (P: state -> trace -> state -> Prop),
+  (forall s1 t s2, step ge s1 t s2 -> P s1 t s2) ->
+  (forall s1 t1 s2 t2 s3 t, 
+   step ge s1 t1 s2 -> plus ge s2 t2 s3 -> P s2 t2 s3 -> t = t1 ** t2 ->
+   P s1 t s3) ->
+  forall s1 t s2, plus ge s1 t s2 -> P s1 t s2.
+Proof.
+  intros ge P BASE IND.
+  assert (forall s1 t s2, star ge s1 t s2 ->
+         forall s0 t0, step ge s0 t0 s1 ->
+         P s0 (t0 ** t) s2).
+  induction 1; intros.
+  rewrite E0_right. apply BASE; auto.
+  eapply IND. eauto. econstructor; eauto. subst t. eapply IHstar; eauto. auto.
+
+  intros. inv H0. eauto. 
+Qed.
+
+Lemma plus_E0_ind:
+  forall ge (P: state -> state -> Prop),
+  (forall s1 s2 s3, step ge s1 E0 s2 -> star ge s2 E0 s3 -> P s1 s3) ->
+  forall s1 s2, plus ge s1 E0 s2 -> P s1 s2.
+Proof.
+  intros. inv H0. exploit Eapp_E0_inv; eauto. intros [A B]; subst. eauto.
+Qed.
+
+(** Counted sequences of transitions *)
+
+Inductive starN (ge: genv): nat -> state -> trace -> state -> Prop :=
+  | starN_refl: forall s,
+      starN ge O s E0 s
+  | starN_step: forall n s t t1 s' t2 s'',
+      step ge s t1 s' -> starN ge n s' t2 s'' -> t = t1 ** t2 ->
+      starN ge (S n) s t s''.
+
+Remark starN_star:
+  forall ge n s t s', starN ge n s t s' -> star ge s t s'.
+Proof.
+  induction 1; econstructor; eauto.
+Qed.
+
+Remark star_starN:
+  forall ge s t s', star ge s t s' -> exists n, starN ge n s t s'.
+Proof.
+  induction 1. 
+  exists O; constructor.
+  destruct IHstar as [n P]. exists (S n); econstructor; eauto.
+Qed.
+
 (** Infinitely many transitions *)
 
 CoInductive forever (ge: genv): state -> traceinf -> Prop :=
@@ -404,111 +468,101 @@ Proof.
   auto.
 Qed.
 
-(** * Outcomes for program executions *)
-
-(** The four possible outcomes for the execution of a program:
-- Termination, with a finite trace of observable events
-  and an integer value that stands for the process exit code
-  (the return value of the main function).
-- Divergence with a finite trace of observable events.
-  (At some point, the program runs forever without doing any I/O.)
-- Reactive divergence with an infinite trace of observable events.
-  (The program performs infinitely many I/O operations separated
-   by finite amounts of internal computations.)
-- Going wrong, with a finite trace of observable events
-  performed before the program gets stuck.
-*)
-
-Inductive program_behavior: Type :=
-  | Terminates: trace -> int -> program_behavior
-  | Diverges: trace -> program_behavior
-  | Reacts: traceinf -> program_behavior
-  | Goes_wrong: trace -> program_behavior.
-
-Definition not_wrong (beh: program_behavior) : Prop :=
-  match beh with
-  | Terminates _ _ => True
-  | Diverges _ => True
-  | Reacts _ => True
-  | Goes_wrong _ => False
-  end.
-
-(** Given a characterization of initial states and final states,
-  [program_behaves] relates a program behaviour with the 
-  sequences of transitions that can be taken from an initial state
-  to a final state. *)
-
-Variable initial_state: state -> Prop.
-Variable final_state: state -> int -> Prop.
-
-Inductive program_behaves (ge: genv): program_behavior -> Prop :=
-  | program_terminates: forall s t s' r,
-      initial_state s ->
-      star ge s t s' ->
-      final_state s' r ->
-      program_behaves ge (Terminates t r)
-  | program_diverges: forall s t s',
-      initial_state s ->
-      star ge s t s' -> forever_silent ge s' ->
-      program_behaves ge (Diverges t)
-  | program_reacts: forall s T,
-      initial_state s ->
-      forever_reactive ge s T ->
-      program_behaves ge (Reacts T)
-  | program_goes_wrong: forall s t s',
-      initial_state s ->
-      star ge s t s' ->
-      nostep ge s' ->
-      (forall r, ~final_state s' r) ->
-      program_behaves ge (Goes_wrong t)
-  | program_goes_initially_wrong:
-      (forall s, ~initial_state s) ->
-      program_behaves ge (Goes_wrong E0).
-
 End CLOSURES.
 
-(** * Simulations between two small-step semantics. *)
-
-(** In this section, we show that if two transition relations 
-  satisfy certain simulation diagrams, then every program behaviour
-  generated by the first transition relation can also occur
-  with the second transition relation. *)
-
-Section SIMULATION.
+(** * Transition semantics *)
+
+(** The general form of a transition semantics. *)
+
+Record semantics : Type := Semantics {
+  state: Type;
+  funtype: Type;
+  vartype: Type;
+  step : Genv.t funtype vartype -> state -> trace -> state -> Prop;
+  initial_state: state -> Prop;
+  final_state: state -> int -> Prop;
+  globalenv: Genv.t funtype vartype
+}.
+
+(** Handy notations. *)
+
+Notation " 'Step' L " := (step L (globalenv L)) (at level 1) : smallstep_scope.
+Notation " 'Star' L " := (star (step L) (globalenv L)) (at level 1) : smallstep_scope.
+Notation " 'Plus' L " := (plus (step L) (globalenv L)) (at level 1) : smallstep_scope.
+Notation " 'Forever_silent' L " := (forever_silent (step L) (globalenv L)) (at level 1) : smallstep_scope.
+Notation " 'Forever_reactive' L " := (forever_reactive (step L) (globalenv L)) (at level 1) : smallstep_scope.
+Notation " 'Nostep' L " := (nostep (step L) (globalenv L)) (at level 1) : smallstep_scope.
+
+Open Scope smallstep_scope.
+
+(** * Forward simulations between two transition semantics. *)
+
+(** The general form of a forward simulation. *)
+
+Record forward_simulation (L1 L2: semantics) : Type :=
+  Forward_simulation {
+    fsim_index: Type;
+    fsim_order: fsim_index -> fsim_index -> Prop;
+    fsim_order_wf: well_founded fsim_order;
+    fsim_match_states :> fsim_index -> state L1 -> state L2 -> Prop;
+    fsim_match_initial_states:
+      forall s1, initial_state L1 s1 ->
+      exists i, exists s2, initial_state L2 s2 /\ fsim_match_states i s1 s2;
+    fsim_match_final_states:
+      forall i s1 s2 r, 
+      fsim_match_states i s1 s2 -> final_state L1 s1 r -> final_state L2 s2 r;
+    fsim_simulation:
+      forall s1 t s1', Step L1 s1 t s1' ->
+      forall i s2, fsim_match_states i s1 s2 ->
+      exists i', exists s2',
+         (Plus L2 s2 t s2' \/ (Star L2 s2 t s2' /\ fsim_order i' i))
+      /\ fsim_match_states i' s1' s2';
+    fsim_symbols_preserved:
+      forall id, Genv.find_symbol (globalenv L2) id = Genv.find_symbol (globalenv L1) id
+  }.
+
+Implicit Arguments forward_simulation [].
+
+(** An alternate form of the simulation diagram *)
+
+Lemma fsim_simulation':
+  forall L1 L2 (S: forward_simulation L1 L2),
+  forall i s1 t s1', Step L1 s1 t s1' ->
+  forall s2, S i s1 s2 ->
+  (exists i', exists s2', Plus L2 s2 t s2' /\ S i' s1' s2')
+  \/ (exists i', fsim_order S i' i /\ t = E0 /\ S i' s1' s2).
+Proof.
+  intros. exploit fsim_simulation; eauto. 
+  intros [i' [s2' [A B]]]. intuition. 
+  left; exists i'; exists s2'; auto.
+  inv H2. 
+  right; exists i'; auto.
+  left; exists i'; exists s2'; split; auto. econstructor; eauto. 
+Qed.
 
-(** The first small-step semantics is axiomatized as follows. *)
+(** ** Forward simulation diagrams. *)
 
-Variable genv1: Type.
-Variable state1: Type.
-Variable step1: genv1 -> state1 -> trace -> state1 -> Prop.
-Variable initial_state1: state1 -> Prop.
-Variable final_state1: state1 -> int -> Prop.
-Variable ge1: genv1.
+(** Various simulation diagrams that imply forward simulation *)
 
-(** The second small-step semantics is also axiomatized. *)
+Section FORWARD_SIMU_DIAGRAMS.
 
-Variable genv2: Type.
-Variable state2: Type.
-Variable step2: genv2 -> state2 -> trace -> state2 -> Prop.
-Variable initial_state2: state2 -> Prop.
-Variable final_state2: state2 -> int -> Prop.
-Variable ge2: genv2.
+Variable L1: semantics.
+Variable L2: semantics.
 
-(** We assume given a matching relation between states of both semantics.
-  This matching relation must be compatible with initial states
-  and with final states. *)
+Hypothesis symbols_preserved:
+  forall id, Genv.find_symbol (globalenv L2) id = Genv.find_symbol (globalenv L1) id.
 
-Variable match_states: state1 -> state2 -> Prop.
+Variable match_states: state L1 -> state L2 -> Prop.
 
 Hypothesis match_initial_states:
-  forall st1, initial_state1 st1 ->
-  exists st2, initial_state2 st2 /\ match_states st1 st2.
+  forall s1, initial_state L1 s1 ->
+  exists s2, initial_state L2 s2 /\ match_states s1 s2.
 
 Hypothesis match_final_states:
-  forall st1 st2 r,
-  match_states st1 st2 ->
-  final_state1 st1 r ->
-  final_state2 st2 r.
+  forall s1 s2 r,
+  match_states s1 s2 ->
+  final_state L1 s1 r ->
+  final_state L2 s2 r.
 
 (** Simulation when one transition in the first program
     corresponds to zero, one or several transitions in the second program.
@@ -522,81 +576,27 @@ Section SIMULATION_STAR_WF.
   of the first semantics.  Stuttering steps must correspond
   to states that decrease w.r.t. [order]. *)
 
-Variable order: state1 -> state1 -> Prop.
+Variable order: state L1 -> state L1 -> Prop.
 Hypothesis order_wf: well_founded order.
 
 Hypothesis simulation:
-  forall st1 t st1', step1 ge1 st1 t st1' ->
-  forall st2, match_states st1 st2 ->
-  exists st2',
-  (plus step2 ge2 st2 t st2' \/ (star step2 ge2 st2 t st2' /\ order st1' st1))
-  /\ match_states st1' st2'.
+  forall s1 t s1', Step L1 s1 t s1' ->
+  forall s2, match_states s1 s2 ->
+  exists s2',
+  (Plus L2 s2 t s2' \/ (Star L2 s2 t s2' /\ order s1' s1))
+  /\ match_states s1' s2'.
 
-Lemma simulation_star_star:
-  forall st1 t st1', star step1 ge1 st1 t st1' ->
-  forall st2, match_states st1 st2 ->
-  exists st2', star step2 ge2 st2 t st2' /\ match_states st1' st2'.
+Lemma forward_simulation_star_wf: forward_simulation L1 L2.
 Proof.
-  induction 1; intros.
-  exists st2; split. apply star_refl. auto.
-  destruct (simulation H H2) as [st2' [A B]].
-  destruct (IHstar _ B) as [st3' [C D]].
-  exists st3'; split; auto.
-  apply star_trans with t1 st2' t2; auto. 
-  destruct A as [F | [F G]].
-  apply plus_star; auto.
+  apply Forward_simulation with
+    (fsim_order := order)
+    (fsim_match_states := fun idx s1 s2 => idx = s1 /\ match_states s1 s2);
   auto.
-Qed.
-
-Lemma simulation_star_forever_silent:
-  forall st1 st2,
-  forever_silent step1 ge1 st1 -> match_states st1 st2 ->
-  forever_silent step2 ge2 st2.
-Proof.
-  assert (forall st1 st2,
-    forever_silent step1 ge1 st1 -> match_states st1 st2 ->
-    forever_silent_N step2 order ge2 st1 st2).
-  cofix COINDHYP; intros.
-  inversion H; subst.
-  destruct (simulation H1 H0) as [st2' [A B]].
-  destruct A as [C | [C D]].
-  apply forever_silent_N_plus with st2' s2.
-  auto. apply COINDHYP. assumption. assumption.
-  apply forever_silent_N_star with st2' s2.
-  auto. auto. apply COINDHYP. assumption. auto.
-  intros. eapply forever_silent_N_forever; eauto.
-Qed.
-
-Lemma simulation_star_forever_reactive:
-  forall st1 st2 T,
-  forever_reactive step1 ge1 st1 T -> match_states st1 st2 ->
-  forever_reactive step2 ge2 st2 T.
-Proof.
-  cofix COINDHYP; intros.
-  inv H. 
-  destruct (simulation_star_star H1 H0) as [st2' [A B]].
-  econstructor. eexact A. auto. 
-  eapply COINDHYP. eauto. auto. 
-Qed.
-
-Lemma simulation_star_wf_preservation:
-  forall beh,
-  not_wrong beh ->
-  program_behaves step1 initial_state1 final_state1 ge1 beh ->
-  program_behaves step2 initial_state2 final_state2 ge2 beh.
-Proof.
-  intros. inv H0; simpl in H. 
-  destruct (match_initial_states H1) as [s2 [A B]].
-  destruct (simulation_star_star H2 B) as [s2' [C D]].
-  econstructor; eauto.
-  destruct (match_initial_states H1) as [s2 [A B]].
-  destruct (simulation_star_star H2 B) as [s2' [C D]].
-  econstructor; eauto.
-  eapply simulation_star_forever_silent; eauto.
-  destruct (match_initial_states H1) as [s2 [A B]].
-  econstructor; eauto. eapply simulation_star_forever_reactive; eauto.
-  contradiction.
-  contradiction.
+  intros. exploit match_initial_states; eauto. intros [s2 [A B]].
+    exists s1; exists s2; auto.
+  intros. destruct H. eapply match_final_states; eauto.
+  intros. destruct H0. subst i. exploit simulation; eauto. intros [s2' [A B]].
+  exists s1'; exists s2'; intuition.
 Qed.
 
 End SIMULATION_STAR_WF.
@@ -607,90 +607,61 @@ Section SIMULATION_STAR.
   associated with states of the first semantics.  It must decrease when we take 
   a stuttering step. *)
 
-Variable measure: state1 -> nat.
+Variable measure: state L1 -> nat.
 
 Hypothesis simulation:
-  forall st1 t st1', step1 ge1 st1 t st1' ->
-  forall st2, match_states st1 st2 ->
-  (exists st2', plus step2 ge2 st2 t st2' /\ match_states st1' st2')
-  \/ (measure st1' < measure st1 /\ t = E0 /\ match_states st1' st2)%nat.
+  forall s1 t s1', Step L1 s1 t s1' ->
+  forall s2, match_states s1 s2 ->
+  (exists s2', Plus L2 s2 t s2' /\ match_states s1' s2')
+  \/ (measure s1' < measure s1 /\ t = E0 /\ match_states s1' s2)%nat.
 
-Lemma simulation_star_preservation:
-  forall beh,
-  not_wrong beh ->
-  program_behaves step1 initial_state1 final_state1 ge1 beh ->
-  program_behaves step2 initial_state2 final_state2 ge2 beh.
+Lemma forward_simulation_star: forward_simulation L1 L2.
 Proof.
-  intros.
-  apply simulation_star_wf_preservation with (ltof _ measure).
-  apply well_founded_ltof. intros.
-  destruct (simulation H1 H2) as [[st2' [A B]] | [A [B C]]].
-  exists st2'; auto.
-  exists st2; split. right; split. rewrite B. apply star_refl. auto. auto.
-  auto. auto.
+  apply forward_simulation_star_wf with (ltof _ measure).
+  apply well_founded_ltof.
+  intros. exploit simulation; eauto. intros [[s2' [A B]] | [A [B C]]].
+  exists s2'; auto.
+  exists s2; split. right; split. rewrite B. apply star_refl. auto. auto.
 Qed.
 
 End SIMULATION_STAR.
 
-(** Lock-step simulation: each transition in the first semantics
-    corresponds to exactly one transition in the second semantics. *)
+(** Simulation when one transition in the first program corresponds
+    to one or several transitions in the second program. *)
 
-Section SIMULATION_STEP.
+Section SIMULATION_PLUS.
 
 Hypothesis simulation:
-  forall st1 t st1', step1 ge1 st1 t st1' ->
-  forall st2, match_states st1 st2 ->
-  exists st2', step2 ge2 st2 t st2' /\ match_states st1' st2'.
+  forall s1 t s1', Step L1 s1 t s1' ->
+  forall s2, match_states s1 s2 ->
+  exists s2', Plus L2 s2 t s2' /\ match_states s1' s2'.
 
-Lemma simulation_step_preservation:
-  forall beh,
-  not_wrong beh ->
-  program_behaves step1 initial_state1 final_state1 ge1 beh ->
-  program_behaves step2 initial_state2 final_state2 ge2 beh.
+Lemma forward_simulation_plus: forward_simulation L1 L2.
 Proof.
-  intros.
-  pose (measure := fun (st: state1) => 0%nat).
-  assert (simulation':
-  forall st1 t st1', step1 ge1 st1 t st1' ->
-  forall st2, match_states st1 st2 ->
-  (exists st2', plus step2 ge2 st2 t st2' /\ match_states st1' st2')
-  \/ (measure st1' < measure st1 /\ t = E0 /\ match_states st1' st2)%nat).
-  intros. destruct (simulation H1 H2) as [st2' [A B]].
-  left; exists st2'; split. apply plus_one; auto. auto.
-  eapply simulation_star_preservation; eauto.
+  apply forward_simulation_star with (measure := fun _ => O).
+  intros. exploit simulation; eauto.
 Qed.
 
-End SIMULATION_STEP.
+End SIMULATION_PLUS.
 
-(** Simulation when one transition in the first program corresponds
-    to one or several transitions in the second program. *)
+(** Lock-step simulation: each transition in the first semantics
+    corresponds to exactly one transition in the second semantics. *)
 
-Section SIMULATION_PLUS.
+Section SIMULATION_STEP.
 
 Hypothesis simulation:
-  forall st1 t st1', step1 ge1 st1 t st1' ->
-  forall st2, match_states st1 st2 ->
-  exists st2', plus step2 ge2 st2 t st2' /\ match_states st1' st2'.
+  forall s1 t s1', Step L1 s1 t s1' ->
+  forall s2, match_states s1 s2 ->
+  exists s2', Step L2 s2 t s2' /\ match_states s1' s2'.
 
-Lemma simulation_plus_preservation:
-  forall beh,
-  not_wrong beh ->
-  program_behaves step1 initial_state1 final_state1 ge1 beh ->
-  program_behaves step2 initial_state2 final_state2 ge2 beh.
+Lemma forward_simulation_step: forward_simulation L1 L2.
 Proof.
-  intros.
-  pose (measure := fun (st: state1) => 0%nat).
-  assert (simulation':
-  forall st1 t st1', step1 ge1 st1 t st1' ->
-  forall st2, match_states st1 st2 ->
-  (exists st2', plus step2 ge2 st2 t st2' /\ match_states st1' st2')
-  \/ (measure st1' < measure st1 /\ t = E0 /\ match_states st1' st2)%nat).
-  intros. destruct (simulation H1 H2) as [st2' [A B]].
-  left; exists st2'; auto.
-  eapply simulation_star_preservation; eauto.
+  apply forward_simulation_plus. 
+  intros. exploit simulation; eauto. intros [s2' [A B]].
+  exists s2'; split; auto. apply plus_one; auto.
 Qed.
 
-End SIMULATION_PLUS.
+End SIMULATION_STEP.
 
 (** Simulation when one transition in the first program
     corresponds to zero or one transitions in the second program.
@@ -700,294 +671,860 @@ End SIMULATION_PLUS.
 
 Section SIMULATION_OPT.
 
-Variable measure: state1 -> nat.
+Variable measure: state L1 -> nat.
 
 Hypothesis simulation:
-  forall st1 t st1', step1 ge1 st1 t st1' ->
-  forall st2, match_states st1 st2 ->
-  (exists st2', step2 ge2 st2 t st2' /\ match_states st1' st2')
-  \/ (measure st1' < measure st1 /\ t = E0 /\ match_states st1' st2)%nat.
-
-Lemma simulation_opt_preservation:
-  forall beh,
-  not_wrong beh ->
-  program_behaves step1 initial_state1 final_state1 ge1 beh ->
-  program_behaves step2 initial_state2 final_state2 ge2 beh.
-Proof.
-  assert (simulation':
-    forall st1 t st1', step1 ge1 st1 t st1' ->
-    forall st2, match_states st1 st2 ->
-    (exists st2', plus step2 ge2 st2 t st2' /\ match_states st1' st2')
-    \/ (measure st1' < measure st1 /\ t = E0 /\ match_states st1' st2)%nat).
-  intros. elim (simulation H H0). 
-  intros [st2' [A B]]. left. exists st2'; split. apply plus_one; auto. auto.
-  intros [A [B C]]. right. intuition.
-  intros. eapply simulation_star_preservation; eauto.
+  forall s1 t s1', Step L1 s1 t s1' ->
+  forall s2, match_states s1 s2 ->
+  (exists s2', Step L2 s2 t s2' /\ match_states s1' s2')
+  \/ (measure s1' < measure s1 /\ t = E0 /\ match_states s1' s2)%nat.
+
+Lemma forward_simulation_opt: forward_simulation L1 L2.
+Proof.
+  apply forward_simulation_star with measure.
+  intros. exploit simulation; eauto. intros [[s2' [A B]] | [A [B C]]].
+  left; exists s2'; split; auto. apply plus_one; auto.
+  right; auto.
 Qed.
 
 End SIMULATION_OPT.
 
-End SIMULATION.
+End FORWARD_SIMU_DIAGRAMS.
 
-(** * Existence of behaviors *)
+(** ** Forward simulation of transition sequences *)
 
-Require Import Classical.
-Require Import ClassicalEpsilon.
+Section SIMULATION_SEQUENCES.
 
-(** We now show that any program admits at least one behavior.
-  The proof requires classical logic: the axiom of excluded middle
-  and an axiom of description. *)
+Variable L1: semantics.
+Variable L2: semantics.
+Variable S: forward_simulation L1 L2.
 
-Section EXISTS_BEHAVIOR.
+Lemma simulation_star:
+  forall s1 t s1', Star L1 s1 t s1' ->
+  forall i s2, S i s1 s2 ->
+  exists i', exists s2', Star L2 s2 t s2' /\ S i' s1' s2'.
+Proof.
+  induction 1; intros.
+  exists i; exists s2; split; auto. apply star_refl.
+  exploit fsim_simulation; eauto. intros [i' [s2' [A B]]].
+  exploit IHstar; eauto. intros [i'' [s2'' [C D]]].
+  exists i''; exists s2''; split; auto. eapply star_trans; eauto.
+  intuition. apply plus_star; auto. 
+Qed.
 
-Variable genv: Type.
-Variable state: Type.
-Variable initial_state: state -> Prop.
-Variable final_state: state -> int -> Prop.
-Variable step: genv -> state -> trace -> state -> Prop.
+Lemma simulation_plus:
+  forall s1 t s1', Plus L1 s1 t s1' ->
+  forall i s2, S i s1 s2 ->
+  (exists i', exists s2', Plus L2 s2 t s2' /\ S i' s1' s2')
+  \/ (exists i', clos_trans _ (fsim_order S) i' i /\ t = E0 /\ S i' s1' s2).
+Proof.
+  induction 1 using plus_ind2; intros.
+(* base case *)
+  exploit fsim_simulation'; eauto. intros [A | [i' A]].
+  left; auto.
+  right; exists i'; intuition. 
+(* inductive case *)
+  exploit fsim_simulation'; eauto. intros [[i' [s2' [A B]]] | [i' [A [B C]]]].
+  exploit simulation_star. apply plus_star; eauto. eauto. 
+  intros [i'' [s2'' [P Q]]].
+  left; exists i''; exists s2''; split; auto. eapply plus_star_trans; eauto.
+  exploit IHplus; eauto. intros [[i'' [s2'' [P Q]]] | [i'' [P [Q R]]]].
+  subst. simpl. left; exists i''; exists s2''; auto.
+  subst. simpl. right; exists i''; intuition.
+  eapply t_trans; eauto. eapply t_step; eauto.
+Qed.
+
+Lemma simulation_forever_silent:
+  forall i s1 s2,
+  Forever_silent L1 s1 -> S i s1 s2 ->
+  Forever_silent L2 s2.
+Proof.
+  assert (forall i s1 s2,
+          Forever_silent L1 s1 -> S i s1 s2 ->
+          forever_silent_N (step L2) (fsim_order S) (globalenv L2) i s2).
+    cofix COINDHYP; intros.
+    inv H. destruct (fsim_simulation S _ _ _ H1 _ _ H0) as [i' [s2' [A B]]].
+    destruct A as [C | [C D]].
+    eapply forever_silent_N_plus; eauto.
+    eapply forever_silent_N_star; eauto.
+  intros. eapply forever_silent_N_forever; eauto. apply fsim_order_wf.
+Qed.
+
+Lemma simulation_forever_reactive:
+  forall i s1 s2 T,
+  Forever_reactive L1 s1 T -> S i s1 s2 ->
+  Forever_reactive L2 s2 T.
+Proof.
+  cofix COINDHYP; intros.
+  inv H. 
+  destruct (simulation_star H1 i _ H0) as [i' [st2' [A B]]].
+  econstructor; eauto.
+Qed.
+
+End SIMULATION_SEQUENCES.
 
-(** The most difficult part of the proof is to show the existence
-  of an infinite trace in the case of reactive divergence. *)
+(** ** Composing two forward simulations *)
 
-Section TRACEINF_REACTS.
+Section COMPOSE_SIMULATIONS.
 
-Variable ge: genv.
-Variable s0: state.
+Variable L1: semantics.
+Variable L2: semantics.
+Variable L3: semantics.
+Variable S12: forward_simulation L1 L2.
+Variable S23: forward_simulation L2 L3.
 
-Hypothesis reacts:
-  forall s1 t1, star step ge s0 t1 s1 ->
-  exists s2, exists t2, star step ge s1 t2 s2 /\ t2 <> E0.
+Let ff_index : Type := (fsim_index S23 * fsim_index S12)%type.
 
-Lemma reacts':
-  forall s1 t1, star step ge s0 t1 s1 ->
-  { s2 : state & { t2 : trace | star step ge s1 t2 s2 /\ t2 <> E0 } }.
+Let ff_order : ff_index -> ff_index -> Prop :=
+  lex_ord (clos_trans _ (fsim_order S23)) (fsim_order S12).
+
+Let ff_match_states (i: ff_index) (s1: state L1) (s3: state L3) : Prop :=
+  exists s2, S12 (snd i) s1 s2 /\ S23 (fst i) s2 s3.
+
+Lemma compose_forward_simulation: forward_simulation L1 L3.
 Proof.
-  intros. 
-  destruct (constructive_indefinite_description _ (reacts H)) as [s2 A].
-  destruct (constructive_indefinite_description _ A) as [t2 [B C]].
-  exists s2; exists t2; auto.
+  apply Forward_simulation with (fsim_order := ff_order) (fsim_match_states := ff_match_states).
+(* well founded *)
+  unfold ff_order. apply wf_lex_ord. apply wf_clos_trans. apply fsim_order_wf. apply fsim_order_wf.
+(* initial states *)
+  intros. exploit (fsim_match_initial_states S12); eauto. intros [i [s2 [A B]]].
+  exploit (fsim_match_initial_states S23); eauto. intros [i' [s3 [C D]]].
+  exists (i', i); exists s3; split; auto. exists s2; auto. 
+(* final states *)
+  intros. destruct H as [s3 [A B]].
+  eapply (fsim_match_final_states S23); eauto.
+  eapply (fsim_match_final_states S12); eauto.
+(* simulation *)
+  intros. destruct H0 as [s3 [A B]]. destruct i as [i2 i1]; simpl in *.
+  exploit (fsim_simulation' S12); eauto. intros [[i1' [s3' [C D]]] | [i1' [C [D E]]]].
+  (* L2 makes one or several steps. *)
+  exploit simulation_plus; eauto. intros [[i2' [s2' [P Q]]] | [i2' [P [Q R]]]].
+  (* L3 makes one or several steps *)
+  exists (i2', i1'); exists s2'; split. auto. exists s3'; auto.
+  (* L3 makes no step *)
+  exists (i2', i1'); exists s2; split. 
+  right; split. subst t; apply star_refl. red. left. auto.
+  exists s3'; auto. 
+  (* L2 makes no step *)
+  exists (i2, i1'); exists s2; split.
+  right; split. subst t; apply star_refl. red. right. auto. 
+  exists s3; auto.
+(* symbols *)
+  intros. transitivity (Genv.find_symbol (globalenv L2) id); apply fsim_symbols_preserved; auto.
 Qed.
 
-CoFixpoint build_traceinf' (s1: state) (t1: trace) (ST: star step ge s0 t1 s1) : traceinf' :=
-  match reacts' ST with
-  | existT s2 (exist t2 (conj A B)) =>
-      Econsinf' t2 
-                (build_traceinf' (star_trans ST A (refl_equal _)))
-                B
-  end.
+End COMPOSE_SIMULATIONS.
+
+(** * Receptiveness and determinacy *)
+
+Record receptive (L: semantics) : Prop :=
+  Receptive {
+    sr_receptive: forall s t1 s1 t2,
+      Step L s t1 s1 -> match_traces (globalenv L) t1 t2 -> exists s2, Step L s t2 s2;
+    sr_traces: forall s t s',
+      Step L s t s' -> (length t <= 1)%nat
+  }.
+
+Record determinate (L: semantics) : Prop :=
+  Determinate {
+    sd_determ: forall s t1 s1 t2 s2,
+      Step L s t1 s1 -> Step L s t2 s2 ->
+      match_traces (globalenv L) t1 t2 /\ (t1 = t2 -> s1 = s2);
+    sd_traces: forall s t s',
+      Step L s t s' -> (length t <= 1)%nat;
+    sd_initial_determ: forall s1 s2,
+      initial_state L s1 -> initial_state L s2 -> s1 = s2;
+    sd_final_nostep: forall s r,
+      final_state L s r -> Nostep L s;
+    sd_final_determ: forall s r1 r2,
+      final_state L s r1 -> final_state L s r2 -> r1 = r2
+  }.
+
+Section DETERMINACY.
+
+Variable L: semantics.
+Hypothesis DET: determinate L.
+
+Lemma sd_determ_1:
+  forall s t1 s1 t2 s2,
+  Step L s t1 s1 -> Step L s t2 s2 -> match_traces (globalenv L) t1 t2.
+Proof.
+  intros. eapply sd_determ; eauto.
+Qed. 
 
-Lemma reacts_forever_reactive_rec:
-  forall s1 t1 (ST: star step ge s0 t1 s1),
-  forever_reactive step ge s1 (traceinf_of_traceinf' (build_traceinf' ST)).
+Lemma sd_determ_2:
+  forall s t s1 s2,
+  Step L s t s1 -> Step L s t s2 -> s1 = s2.
 Proof.
-  cofix COINDHYP; intros.
-  rewrite (unroll_traceinf' (build_traceinf' ST)). simpl. 
-  destruct (reacts' ST) as [s2 [t2 [A B]]]. 
-  rewrite traceinf_traceinf'_app. 
-  econstructor. eexact A. auto. apply COINDHYP. 
+  intros. eapply sd_determ; eauto.
 Qed.
 
-Lemma reacts_forever_reactive:
-  exists T, forever_reactive step ge s0 T.
+Lemma star_determinacy:
+  forall s t s', Star L s t s' ->
+  forall s'', Star L s t s'' -> Star L s' E0 s'' \/ Star L s'' E0 s'.
 Proof.
-  exists (traceinf_of_traceinf' (build_traceinf' (star_refl step ge s0))).
-  apply reacts_forever_reactive_rec.
+  induction 1; intros. 
+  auto.
+  inv H2.
+  right. eapply star_step; eauto.
+  exploit sd_determ_1. eexact H. eexact H3. intros MT.
+  exploit (sd_traces DET). eexact H. intros L1.
+  exploit (sd_traces DET). eexact H3. intros L2.
+  assert (t1 = t0 /\ t2 = t3).
+    destruct t1. inv MT. auto. 
+    destruct t1; simpl in L1; try omegaContradiction. 
+    destruct t0. inv MT. destruct t0; simpl in L2; try omegaContradiction.
+    simpl in H5. split. congruence. congruence.
+  destruct H1; subst.
+  assert (s2 = s4) by (eapply sd_determ_2; eauto). subst s4. 
+  auto.
 Qed.
 
-End TRACEINF_REACTS.
+End DETERMINACY.
+
+(** * Backward simulations between two transition semantics. *)
+
+Definition safe (L: semantics) (s: state L) : Prop :=
+  forall s',
+  Star L s E0 s' -> 
+  (exists r, final_state L s' r)
+  \/ (exists t, exists s'', Step L s' t s'').
 
-Lemma diverges_forever_silent:
-  forall ge s0,
-  (forall s1 t1, star step ge s0 t1 s1 -> exists s2, step ge s1 E0 s2) ->
-  forever_silent step ge s0.
+Lemma star_safe:
+  forall (L: semantics) s s',
+  Star L s E0 s' -> safe L s -> safe L s'.
 Proof.
-  cofix COINDHYP; intros. 
-  destruct (H s0 E0) as [s1 ST]. constructor. 
-  econstructor. eexact ST. apply COINDHYP. 
-  intros. eapply H. eapply star_left; eauto.
+  intros; red; intros. apply H0. eapply star_trans; eauto.
+Qed. 
+
+(** The general form of a backward simulation. *)
+
+Record backward_simulation (L1 L2: semantics) : Type :=
+  Backward_simulation {
+    bsim_index: Type;
+    bsim_order: bsim_index -> bsim_index -> Prop;
+    bsim_order_wf: well_founded bsim_order;
+    bsim_match_states :> bsim_index -> state L1 -> state L2 -> Prop;
+    bsim_initial_states_exist:
+      forall s1, initial_state L1 s1 -> exists s2, initial_state L2 s2;
+    bsim_match_initial_states:
+      forall s1 s2, initial_state L1 s1 -> initial_state L2 s2 ->
+      exists i, exists s1', initial_state L1 s1' /\ bsim_match_states i s1' s2;
+    bsim_match_final_states:
+      forall i s1 s2 r, 
+      bsim_match_states i s1 s2 -> safe L1 s1 -> final_state L2 s2 r -> 
+      exists s1', Star L1 s1 E0 s1' /\ final_state L1 s1' r;
+    bsim_progress:
+      forall i s1 s2, 
+      bsim_match_states i s1 s2 -> safe L1 s1 ->
+      (exists r, final_state L2 s2 r) \/
+      (exists t, exists s2', Step L2 s2 t s2');
+    bsim_simulation:
+      forall s2 t s2', Step L2 s2 t s2' ->
+      forall i s1, bsim_match_states i s1 s2 -> safe L1 s1 ->
+      exists i', exists s1',
+         (Plus L1 s1 t s1' \/ (Star L1 s1 t s1' /\ bsim_order i' i))
+      /\ bsim_match_states i' s1' s2';
+    bsim_traces:
+      forall s2 t s2', Step L2 s2 t s2' -> (length t <= 1)%nat;
+    bsim_symbols_preserved:
+      forall id, Genv.find_symbol (globalenv L2) id = Genv.find_symbol (globalenv L1) id
+  }.
+
+(** An alternate form of the simulation diagram *)
+
+Lemma bsim_simulation':
+  forall L1 L2 (S: backward_simulation L1 L2),
+  forall i s2 t s2', Step L2 s2 t s2' ->
+  forall s1, S i s1 s2 -> safe L1 s1 ->
+  (exists i', exists s1', Plus L1 s1 t s1' /\ S i' s1' s2')
+  \/ (exists i', bsim_order S i' i /\ t = E0 /\ S i' s1 s2').
+Proof.
+  intros. exploit bsim_simulation; eauto. 
+  intros [i' [s1' [A B]]]. intuition. 
+  left; exists i'; exists s1'; auto.
+  inv H3. 
+  right; exists i'; auto.
+  left; exists i'; exists s1'; split; auto. econstructor; eauto. 
 Qed.
 
-Theorem program_behaves_exists:
-  forall ge, exists beh, program_behaves step initial_state final_state ge beh.
+(** ** Backward simulation diagrams. *)
+
+(** Various simulation diagrams that imply backward simulation. *)
+
+Section BACKWARD_SIMU_DIAGRAMS.
+
+Variable L1: semantics.
+Variable L2: semantics.
+
+Hypothesis symbols_preserved:
+  forall id, Genv.find_symbol (globalenv L2) id = Genv.find_symbol (globalenv L1) id.
+
+Hypothesis length_traces:
+  forall s2 t s2', Step L2 s2 t s2' -> (length t <= 1)%nat.
+
+Variable match_states: state L1 -> state L2 -> Prop.
+
+Hypothesis initial_states_exist:
+  forall s1, initial_state L1 s1 -> exists s2, initial_state L2 s2.
+
+Hypothesis match_initial_states:
+  forall s1 s2, initial_state L1 s1 -> initial_state L2 s2 ->
+  exists s1', initial_state L1 s1' /\ match_states s1' s2.
+
+Hypothesis match_final_states:
+  forall s1 s2 r, 
+  match_states s1 s2 -> final_state L2 s2 r -> final_state L1 s1 r.
+
+Hypothesis progress:
+  forall s1 s2, 
+  match_states s1 s2 -> safe L1 s1 ->
+  (exists r, final_state L2 s2 r) \/
+  (exists t, exists s2', Step L2 s2 t s2').
+
+Section BACKWARD_SIMULATION_PLUS.
+
+Hypothesis simulation:
+  forall s2 t s2', Step L2 s2 t s2' ->
+  forall s1, match_states s1 s2 -> safe L1 s1 ->
+  exists s1', Plus L1 s1 t s1' /\ match_states s1' s2'.
+
+Lemma backward_simulation_plus: backward_simulation L1 L2.
 Proof.
-  intros.
-  destruct (classic (exists s, initial_state s)) as [[s0 INIT] | NOTINIT].
-(* 1. Initial state is defined. *)
-  destruct (classic (forall s1 t1, star step ge s0 t1 s1 -> exists s2, exists t2, step ge s1 t2 s2)).
-(* 1.1 Divergence (silent or reactive) *)
-  destruct (classic (exists s1, exists t1, star step ge s0 t1 s1 /\
-                       (forall s2 t2, star step ge s1 t2 s2 ->
-                        exists s3, step ge s2 E0 s3))).
-(* 1.1.1 Silent divergence *)
-  destruct H0 as [s1 [t1 [A B]]].
-  exists (Diverges t1); econstructor; eauto. 
-  apply diverges_forever_silent; auto.
-(* 1.1.2 Reactive divergence *)
-  destruct (@reacts_forever_reactive ge s0) as [T FR].
-  intros.
-  generalize (not_ex_all_not _ _ H0 s1). intro A; clear H0.
-  generalize (not_ex_all_not _ _ A t1). intro B; clear A.
-  destruct (not_and_or _ _ B). contradiction. 
-  destruct (not_all_ex_not _ _ H0) as [s2 C]; clear H0. 
-  destruct (not_all_ex_not _ _ C) as [t2 D]; clear C.
-  destruct (imply_to_and _ _ D) as [E F]; clear D.
-  destruct (H s2 (t1 ** t2)) as [s3 [t3 G]]. eapply star_trans; eauto. 
-  exists s3; exists (t2 ** t3); split.
-  eapply star_right; eauto. 
-  red; intros. destruct (app_eq_nil t2 t3 H0). subst. elim F. exists s3; auto.
-  exists (Reacts T); econstructor; eauto.
-(* 1.2 Termination (normal or by going wrong) *)
-  destruct (not_all_ex_not _ _ H) as [s1 A]; clear H.
-  destruct (not_all_ex_not _ _ A) as [t1 B]; clear A.
-  destruct (imply_to_and _ _ B) as [C D]; clear B.
-  destruct (classic (exists r, final_state s1 r)) as [[r FINAL] | NOTFINAL].
-(* 1.2.1 Normal termination *)
-  exists (Terminates t1 r); econstructor; eauto.
-(* 1.2.2 Going wrong *)
-  exists (Goes_wrong t1); econstructor; eauto. red. intros. 
-  generalize (not_ex_all_not _ _ D s'); intros. 
-  generalize (not_ex_all_not _ _ H t); intros. 
+  apply Backward_simulation with
+    (bsim_order := fun (x y: unit) => False)
+    (bsim_match_states := fun (i: unit) s1 s2 => match_states s1 s2);
   auto.
-(* 2. Initial state is undefined *)
-  exists (Goes_wrong E0). apply program_goes_initially_wrong. 
-  intros. eapply not_ex_all_not; eauto. 
+  red; intros; constructor; intros. contradiction.
+  intros. exists tt; eauto.
+  intros. exists s1; split. apply star_refl. eauto. 
+  intros. exploit simulation; eauto. intros [s1' [A B]]. 
+  exists tt; exists s1'; auto.
 Qed.
 
-End EXISTS_BEHAVIOR.
+End BACKWARD_SIMULATION_PLUS.
 
-(** * Additional results about infinite reduction sequences *)
+End BACKWARD_SIMU_DIAGRAMS.
 
-(** We now show that any infinite sequence of reductions is either of
-  the "reactive" kind or of the "silent" kind (after a finite number
-  of non-silent transitions).  The proof necessitates the axiom of
-  excluded middle.  This result is used in [Csem] and [Cminor] to
-  relate the coinductive big-step semantics for divergence with the
-  small-step notions of divergence. *)
+(** ** Backward simulation of transition sequences *)
 
-Unset Implicit Arguments.
+Section BACKWARD_SIMULATION_SEQUENCES.
 
-Section INF_SEQ_DECOMP.
+Variable L1: semantics.
+Variable L2: semantics.
+Variable S: backward_simulation L1 L2.
 
-Variable genv: Type.
-Variable state: Type.
-Variable step: genv -> state -> trace -> state -> Prop.
+Lemma bsim_E0_star:
+  forall s2 s2', Star L2 s2 E0 s2' ->
+  forall i s1, S i s1 s2 -> safe L1 s1 ->
+  exists i', exists s1', Star L1 s1 E0 s1' /\ S i' s1' s2'.
+Proof.
+  intros s20 s20' STAR0. pattern s20, s20'. eapply star_E0_ind; eauto.
+(* base case *)
+  intros. exists i; exists s1; split; auto. apply star_refl.
+(* inductive case *)
+  intros. exploit bsim_simulation; eauto. intros [i' [s1' [A B]]].
+  assert (Star L1 s0 E0 s1'). intuition. apply plus_star; auto. 
+  exploit H0. eauto. eapply star_safe; eauto. intros [i'' [s1'' [C D]]].
+  exists i''; exists s1''; split; auto. eapply star_trans; eauto.
+Qed.
+
+Lemma bsim_safe:
+  forall i s1 s2,
+  S i s1 s2 -> safe L1 s1 -> safe L2 s2.
+Proof.
+  intros; red; intros. 
+  exploit bsim_E0_star; eauto. intros [i' [s1' [A B]]].
+  eapply bsim_progress; eauto. eapply star_safe; eauto.
+Qed.
+
+Lemma bsim_E0_plus:
+  forall s2 t s2', Plus L2 s2 t s2' -> t = E0 ->
+  forall i s1, S i s1 s2 -> safe L1 s1 ->
+     (exists i', exists s1', Plus L1 s1 E0 s1' /\ S i' s1' s2')
+  \/ (exists i', clos_trans _ (bsim_order S) i' i /\ S i' s1 s2').
+Proof.
+  induction 1 using plus_ind2; intros; subst t.
+(* base case *)
+  exploit bsim_simulation'; eauto. intros [[i' [s1' [A B]]] | [i' [A [B C]]]].
+  left; exists i'; exists s1'; auto.
+  right; exists i'; intuition.
+(* inductive case *)
+  exploit Eapp_E0_inv; eauto. intros [EQ1 EQ2]; subst.
+  exploit bsim_simulation'; eauto. intros [[i' [s1' [A B]]] | [i' [A [B C]]]].
+  exploit bsim_E0_star. apply plus_star; eauto. eauto. eapply star_safe; eauto. apply plus_star; auto.
+  intros [i'' [s1'' [P Q]]]. 
+  left; exists i''; exists s1''; intuition. eapply plus_star_trans; eauto. 
+  exploit IHplus; eauto. intros [P | [i'' [P Q]]].
+  left; auto.
+  right; exists i''; intuition. eapply t_trans; eauto. apply t_step; auto.
+Qed.
+
+Lemma star_non_E0_split:
+  forall s2 t s2', Star L2 s2 t s2' -> (length t = 1)%nat ->
+  exists s2x, exists s2y, Star L2 s2 E0 s2x /\ Step L2 s2x t s2y /\ Star L2 s2y E0 s2'.
+Proof.
+  induction 1; intros.
+  simpl in H; discriminate.
+  subst t.
+  assert (EITHER: t1 = E0 \/ t2 = E0). 
+    unfold Eapp in H2; rewrite app_length in H2. 
+    destruct t1; auto. destruct t2; auto. simpl in H2; omegaContradiction.
+  destruct EITHER; subst. 
+  exploit IHstar; eauto. intros [s2x [s2y [A [B C]]]]. 
+  exists s2x; exists s2y; intuition. eapply star_left; eauto. 
+  rewrite E0_right. exists s1; exists s2; intuition. apply star_refl.
+Qed.
+
+End BACKWARD_SIMULATION_SEQUENCES.
+
+(** ** Composing two backward simulations *)
+
+Section COMPOSE_BACKWARD_SIMULATIONS.
+
+Variable L1: semantics.
+Variable L2: semantics.
+Variable L3: semantics.
+Variable S12: backward_simulation L1 L2.
+Variable S23: backward_simulation L2 L3.
+
+Let bb_index : Type := (bsim_index S12 * bsim_index S23)%type.
+
+Let bb_order : bb_index -> bb_index -> Prop :=
+  lex_ord (clos_trans _ (bsim_order S12)) (bsim_order S23).
+
+Inductive bb_match_states: bb_index -> state L1 -> state L3 -> Prop :=
+  | bb_match_later: forall i1 i2 s1 s3 s2x s2y,
+      S12 i1 s1 s2x -> Star L2 s2x E0 s2y -> S23 i2 s2y s3 ->
+      bb_match_states (i1, i2) s1 s3.
+
+Lemma bb_match_at: forall i1 i2 s1 s3 s2,
+  S12 i1 s1 s2 -> S23 i2 s2 s3 ->
+  bb_match_states (i1, i2) s1 s3.
+Proof.
+  intros. econstructor; eauto. apply star_refl.
+Qed. 
+
+Lemma bb_simulation_base:
+  forall s3 t s3', Step L3 s3 t s3' ->
+  forall i1 s1 i2 s2, S12 i1 s1 s2 -> S23 i2 s2 s3 -> safe L1 s1 ->
+  exists i', exists s1',
+    (Plus L1 s1 t s1' \/ (Star L1 s1 t s1' /\ bb_order i' (i1, i2)))
+    /\ bb_match_states i' s1' s3'.
+Proof.
+  intros.
+  exploit (bsim_simulation' S23); eauto. eapply bsim_safe; eauto.
+  intros [ [i2' [s2' [PLUS2 MATCH2]]] | [i2' [ORD2 [EQ MATCH2]]]].
+  (* 1 L2 makes one or several transitions *)
+  assert (EITHER: t = E0 \/ (length t = 1)%nat).
+    exploit bsim_traces; eauto. 
+    destruct t; auto. destruct t; auto. simpl. intros. omegaContradiction.
+  destruct EITHER.
+  (* 1.1 these are silent transitions *)
+  subst t. exploit bsim_E0_plus; eauto. 
+  intros [ [i1' [s1' [PLUS1 MATCH1]]] | [i1' [ORD1 MATCH1]]].
+  (* 1.1.1 L1 makes one or several transitions *)
+  exists (i1', i2'); exists s1'; split. auto. eapply bb_match_at; eauto. 
+  (* 1.1.2 L1 makes no transitions *)
+  exists (i1', i2'); exists s1; split. 
+  right; split. apply star_refl. left; auto. 
+  eapply bb_match_at; eauto. 
+  (* 1.2 non-silent transitions *)
+  exploit star_non_E0_split. apply plus_star; eauto. auto. 
+  intros [s2x [s2y [P [Q R]]]].
+  exploit bsim_E0_star. eexact P. eauto. auto. intros [i1' [s1x [X Y]]].
+  exploit bsim_simulation'. eexact Q. eauto. eapply star_safe; eauto. 
+  intros [[i1'' [s1y [U V]]] | [i1'' [U [V W]]]]; try (subst t; discriminate).
+  exists (i1'', i2'); exists s1y; split.
+  left. eapply star_plus_trans; eauto. eapply bb_match_later; eauto.
+  (* 2. L2 makes no transitions *)
+  subst. exists (i1, i2'); exists s1; split.
+  right; split. apply star_refl. right; auto. 
+  eapply bb_match_at; eauto.
+Qed.
 
-Variable ge: genv.
+Lemma bb_simulation:
+  forall s3 t s3', Step L3 s3 t s3' ->
+  forall i s1, bb_match_states i s1 s3 -> safe L1 s1 ->
+  exists i', exists s1',
+    (Plus L1 s1 t s1' \/ (Star L1 s1 t s1' /\ bb_order i' i))
+    /\ bb_match_states i' s1' s3'.
+Proof.
+  intros. inv H0. 
+  exploit star_inv; eauto. intros [[EQ1 EQ2] | PLUS].
+  (* 1. match at *)
+  subst. eapply bb_simulation_base; eauto.
+  (* 2. match later *)
+  exploit bsim_E0_plus; eauto. 
+  intros [[i1' [s1' [A B]]] | [i1' [A B]]].
+  (* 2.1 one or several silent transitions *)
+  exploit bb_simulation_base. eauto. auto. eexact B. eauto.
+    eapply star_safe; eauto. eapply plus_star; eauto.
+  intros [i'' [s1'' [C D]]].
+  exists i''; exists s1''; split; auto.
+  left. eapply plus_star_trans; eauto.
+  destruct C as [P | [P Q]]. apply plus_star; eauto. eauto. 
+  traceEq.
+  (* 2.2 no silent transition *)
+  exploit bb_simulation_base. eauto. auto. eexact B. eauto. auto.
+  intros [i'' [s1'' [C D]]].
+  exists i''; exists s1''; split; auto.
+  intuition. right; intuition. 
+  inv H6. left. eapply t_trans; eauto. left; auto.
+Qed.
 
-Inductive State: Type :=
-  ST: forall (s: state) (T: traceinf), forever step ge s T -> State.
+Lemma compose_backward_simulation: backward_simulation L1 L3.
+Proof.
+  apply Backward_simulation with (bsim_order := bb_order) (bsim_match_states := bb_match_states).
+(* well founded *)
+  unfold bb_order. apply wf_lex_ord. apply wf_clos_trans. apply bsim_order_wf. apply bsim_order_wf.
+(* initial states exist *)
+  intros. exploit (bsim_initial_states_exist S12); eauto. intros [s2 A].
+  eapply (bsim_initial_states_exist S23); eauto.
+(* match initial states *)
+  intros s1 s3 INIT1 INIT3.
+  exploit (bsim_initial_states_exist S12); eauto. intros [s2 INIT2].
+  exploit (bsim_match_initial_states S23); eauto. intros [i2 [s2' [INIT2' M2]]].
+  exploit (bsim_match_initial_states S12); eauto. intros [i1 [s1' [INIT1' M1]]].
+  exists (i1, i2); exists s1'; intuition. eapply bb_match_at; eauto.
+(* match final states *)
+  intros i s1 s3 r MS SAFE FIN. inv MS.
+  exploit (bsim_match_final_states S23); eauto. 
+    eapply star_safe; eauto. eapply bsim_safe; eauto. 
+  intros [s2' [A B]].
+  exploit bsim_E0_star. eapply star_trans. eexact H0. eexact A. auto. eauto. auto.
+  intros [i1' [s1' [C D]]].
+  exploit (bsim_match_final_states S12); eauto. eapply star_safe; eauto. 
+  intros [s1'' [P Q]]. 
+  exists s1''; split; auto. eapply star_trans; eauto.
+(* progress *)
+  intros i s1 s3 MS SAFE. inv MS.
+  eapply (bsim_progress S23). eauto. eapply star_safe; eauto. eapply bsim_safe; eauto. 
+(* simulation *)
+  exact bb_simulation.
+(* trace length *)
+  exact (bsim_traces S23). 
+(* symbols *)
+  intros. transitivity (Genv.find_symbol (globalenv L2) id); apply bsim_symbols_preserved; auto.
+Qed.
 
-Definition state_of_State (S: State): state :=
-  match S with ST s T F => s end.
-Definition traceinf_of_State (S: State) : traceinf :=
-  match S with ST s T F => T end.
+End COMPOSE_BACKWARD_SIMULATIONS.
 
-Inductive Step: trace -> State -> State -> Prop :=
-  | Step_intro: forall s1 t T s2 S F,
-      Step t (ST s1 (t *** T) (@forever_intro genv state step ge s1 t s2 T S F))
-             (ST s2 T F).
+(** ** Converting a forward simulation to a backward simulation *)
 
-Inductive Steps: State -> State -> Prop :=
-  | Steps_refl: forall S, Steps S S
-  | Steps_left: forall t S1 S2 S3, Step t S1 S2 -> Steps S2 S3 -> Steps S1 S3.
+Section FORWARD_TO_BACKWARD.
 
-Remark Steps_trans:
-  forall S1 S2, Steps S1 S2 -> forall S3, Steps S2 S3 -> Steps S1 S3.
+Variable L1: semantics.
+Variable L2: semantics.
+Variable FS: forward_simulation L1 L2.
+
+Hypothesis receptive: receptive L1.
+Hypothesis determinate: determinate L2.
+
+(** Exploiting forward simulation *)
+
+Inductive f2b_transitions: state L1 -> state L2 -> Prop :=
+  | f2b_trans_final: forall s1 s2 s1' r,
+      Star L1 s1 E0 s1' ->
+      final_state L1 s1' r ->
+      final_state L2 s2 r ->
+      f2b_transitions s1 s2
+  | f2b_trans_step: forall s1 s2 s1' t s1'' s2' i' i'',
+      Star L1 s1 E0 s1' ->
+      Step L1 s1' t s1'' ->
+      Plus L2 s2 t s2' ->
+      FS i' s1' s2 -> 
+      FS i'' s1'' s2' ->
+      f2b_transitions s1 s2.
+
+Lemma f2b_progress:
+  forall i s1 s2, FS i s1 s2 -> safe L1 s1 -> f2b_transitions s1 s2.
 Proof.
-  induction 1; intros. auto. econstructor; eauto.
+  intros i0; pattern i0. apply well_founded_ind with (R := fsim_order FS). 
+  apply fsim_order_wf.
+  intros i REC s1 s2 MATCH SAFE.
+  destruct (SAFE s1) as [[r FINAL] | [t [s1' STEP1]]]. apply star_refl.
+  (* final state reached *)
+  eapply f2b_trans_final; eauto. 
+  apply star_refl.
+  eapply fsim_match_final_states; eauto. 
+  (* L1 can make one step *)
+  exploit (fsim_simulation FS); eauto. intros [i' [s2' [A MATCH']]].
+  assert (B: Plus L2 s2 t s2' \/ (s2' = s2 /\ t = E0 /\ fsim_order FS i' i)).
+    intuition.
+    destruct (star_inv H0); intuition.
+  clear A. destruct B as [PLUS2 | [EQ1 [EQ2 ORDER]]].
+  eapply f2b_trans_step; eauto. apply star_refl.
+  subst. exploit REC; eauto. eapply star_safe; eauto. apply star_one; auto.
+  intros TRANS; inv TRANS.
+  eapply f2b_trans_final; eauto. eapply star_left; eauto. 
+  eapply f2b_trans_step; eauto. eapply star_left; eauto.
 Qed.
 
-Let Reactive (S: State) : Prop :=
-  forall S1, 
-  Steps S S1 ->
-  exists S2, exists S3, exists t, Steps S1 S2 /\ Step t S2 S3 /\ t <> E0.
+Lemma fsim_simulation_not_E0:
+  forall s1 t s1', Step L1 s1 t s1' -> t <> E0 ->
+  forall i s2, FS i s1 s2 ->
+  exists i', exists s2', Plus L2 s2 t s2' /\ FS i' s1' s2'.
+Proof.
+  intros. exploit (fsim_simulation FS); eauto. intros [i' [s2' [A B]]].
+  exists i'; exists s2'; split; auto.
+  destruct A. auto. destruct H2. exploit star_inv; eauto. intros [[EQ1 EQ2] | P]; auto.
+  congruence.
+Qed.
 
-Let Silent (S: State) : Prop :=
-  forall S1 t S2, Steps S S1 -> Step t S1 S2 -> t = E0.
+(** Exploiting determinacy *)
 
-Lemma Reactive_or_Silent:
-  forall S, Reactive S \/ (exists S', Steps S S' /\ Silent S').
+Remark silent_or_not_silent:
+  forall t, t = E0 \/ t <> E0.
 Proof.
-  intros. destruct (classic (exists S', Steps S S' /\ Silent S')).
-  auto.
-  left. red; intros. 
-  generalize (not_ex_all_not _ _ H S1). intros.
-  destruct (not_and_or _ _ H1). contradiction. 
-  unfold Silent in H2. 
-  generalize (not_all_ex_not _ _ H2). intros [S2 A].
-  generalize (not_all_ex_not _ _ A). intros [t B].
-  generalize (not_all_ex_not _ _ B). intros [S3 C].
-  generalize (imply_to_and _ _ C). intros [D F].
-  generalize (imply_to_and _ _ F). intros [G J].
-  exists S2; exists S3; exists t. auto.  
-Qed.
-
-Lemma Steps_star:
-  forall S1 S2, Steps S1 S2 ->
-  exists t, star step ge (state_of_State S1) t (state_of_State S2)
-         /\ traceinf_of_State S1 = t *** traceinf_of_State S2.
-Proof.
-  induction 1.
-  exists E0; split. apply star_refl. auto.
-  inv H. destruct IHSteps as [t' [A B]].
-  exists (t ** t'); split.
-  simpl; eapply star_left; eauto.
-  simpl in *. subst T. traceEq.
-Qed.
-
-Lemma Silent_forever_silent:
-  forall S,
-  Silent S -> forever_silent step ge (state_of_State S).
-Proof.
-  cofix COINDHYP; intro S. case S. intros until f. simpl. case f. intros.
-  assert (Step t (ST s1 (t *** T0) (forever_intro s1 t s0 f0))
-                 (ST s2 T0 f0)). 
-    constructor.
-  assert (t = E0). 
-    red in H. eapply H; eauto. apply Steps_refl.
-  apply forever_silent_intro with (state_of_State (ST s2 T0 f0)).
-  rewrite <- H1. assumption. 
-  apply COINDHYP. 
-  red; intros. eapply H. eapply Steps_left; eauto. eauto. 
-Qed.
-
-Lemma Reactive_forever_reactive:
-  forall S,
-  Reactive S -> forever_reactive step ge (state_of_State S) (traceinf_of_State S).
+  intros; unfold E0; destruct t; auto; right; congruence.
+Qed.
+
+Remark not_silent_length:
+  forall t1 t2, (length (t1 ** t2) <= 1)%nat -> t1 = E0 \/ t2 = E0.
 Proof.
-  cofix COINDHYP; intros.
-  destruct (H S) as [S1 [S2 [t [A [B C]]]]]. apply Steps_refl. 
-  destruct (Steps_star _ _ A) as [t' [P Q]].
-  inv B. simpl in *. rewrite Q. rewrite <- Eappinf_assoc. 
-  apply forever_reactive_intro with s2. 
-  eapply star_right; eauto. 
-  red; intros. destruct (Eapp_E0_inv _ _ H0). contradiction.
-  change (forever_reactive step ge (state_of_State (ST s2 T F)) (traceinf_of_State (ST s2 T F))).
-  apply COINDHYP. 
-  red; intros. apply H.
-  eapply Steps_trans. eauto.
-  eapply Steps_left. constructor. eauto.
+  unfold Eapp, E0; intros. rewrite app_length in H. 
+  destruct t1; destruct t2; auto. simpl in H. omegaContradiction.
 Qed.
 
-Theorem forever_silent_or_reactive:
-  forall s T,
-  forever step ge s T ->
-  forever_reactive step ge s T \/
-  exists t, exists s', exists T',
-  star step ge s t s' /\ forever_silent step ge s' /\ T = t *** T'.
+Lemma f2b_determinacy_inv:
+  forall s2 t' s2' t'' s2'',
+  Step L2 s2 t' s2' -> Step L2 s2 t'' s2'' ->
+  (t' = E0 /\ t'' = E0 /\ s2' = s2'')
+  \/ (t' <> E0 /\ t'' <> E0 /\ match_traces (globalenv L1) t' t'').
 Proof.
   intros. 
-  destruct (Reactive_or_Silent (ST s T H)).
-  left. 
-  change (forever_reactive step ge (state_of_State (ST s T H)) (traceinf_of_State (ST s T H))).
-  apply Reactive_forever_reactive. auto.
-  destruct H0 as [S' [A B]].
-  exploit Steps_star; eauto. intros [t [C D]]. simpl in *.
-  right. exists t; exists (state_of_State S'); exists (traceinf_of_State S').
-  split. auto. 
-  split. apply Silent_forever_silent. auto.
-  auto.
+  assert (match_traces (globalenv L2) t' t'').
+    eapply sd_determ_1; eauto. 
+  destruct (silent_or_not_silent t').
+  subst. inv H1.  
+  left; intuition. eapply sd_determ_2; eauto.
+  destruct (silent_or_not_silent t'').
+  subst. inv H1. elim H2; auto. 
+  right; intuition. 
+  eapply match_traces_preserved with (ge1 := (globalenv L2)); auto. 
+  intros; symmetry; apply (fsim_symbols_preserved FS). 
+Qed.
+
+Lemma f2b_determinacy_star:
+  forall s s1, Star L2 s E0 s1 -> 
+  forall t s2 s3,
+  Step L2 s1 t s2 -> t <> E0 ->
+  Star L2 s t s3 ->
+  Star L2 s1 t s3.
+Proof.
+  intros s0 s01 ST0. pattern s0, s01. eapply star_E0_ind; eauto.
+  intros. inv H3. congruence.
+  exploit f2b_determinacy_inv. eexact H. eexact H4.
+  intros [[EQ1 [EQ2 EQ3]] | [NEQ1 [NEQ2 MT]]].
+  subst. simpl in *. eauto. 
+  congruence.
+Qed.
+
+(** Orders *)
+
+Inductive f2b_index : Type :=
+  | F2BI_before (n: nat)
+  | F2BI_after (n: nat).
+
+Inductive f2b_order: f2b_index -> f2b_index -> Prop :=
+  | f2b_order_before: forall n n',
+      (n' < n)%nat ->
+      f2b_order (F2BI_before n') (F2BI_before n)
+  | f2b_order_after: forall n n',
+      (n' < n)%nat ->
+      f2b_order (F2BI_after n') (F2BI_after n)
+  | f2b_order_switch: forall n n',
+      f2b_order (F2BI_before n') (F2BI_after n).
+
+Lemma wf_f2b_order:
+  well_founded f2b_order.
+Proof.
+  assert (ACC1: forall n, Acc f2b_order (F2BI_before n)).
+    intros n0; pattern n0; apply lt_wf_ind; intros.
+    constructor; intros. inv H0. auto. 
+  assert (ACC2: forall n, Acc f2b_order (F2BI_after n)).
+    intros n0; pattern n0; apply lt_wf_ind; intros.
+    constructor; intros. inv H0. auto. auto. 
+  red; intros. destruct a; auto.
+Qed.
+
+(** Constructing the backward simulation *)
+
+Inductive f2b_match_states: f2b_index -> state L1 -> state L2 -> Prop :=
+  | f2b_match_at: forall i s1 s2,
+      FS i s1 s2 ->
+      f2b_match_states (F2BI_after O) s1 s2
+  | f2b_match_before: forall s1 t s1' s2b s2 n s2a i,
+      Step L1 s1 t s1' ->  t <> E0 ->
+      Star L2 s2b E0 s2 ->
+      starN (step L2) (globalenv L2) n s2 t s2a ->
+      FS i s1 s2b ->
+      f2b_match_states (F2BI_before n) s1 s2
+  | f2b_match_after: forall n s2 s2a s1 i,
+      starN (step L2) (globalenv L2) (S n) s2 E0 s2a ->
+      FS i s1 s2a ->
+      f2b_match_states (F2BI_after (S n)) s1 s2.
+
+Remark f2b_match_after':
+  forall n s2 s2a s1 i,
+  starN (step L2) (globalenv L2) n s2 E0 s2a ->
+  FS i s1 s2a ->
+  f2b_match_states (F2BI_after n) s1 s2.
+Proof.
+  intros. inv H. 
+  econstructor; eauto.
+  econstructor; eauto. econstructor; eauto.
+Qed.
+
+(** Backward simulation of L2 steps *)
+
+Lemma f2b_simulation_step:
+  forall s2 t s2', Step L2 s2 t s2' ->
+  forall i s1, f2b_match_states i s1 s2 -> safe L1 s1 ->
+  exists i', exists s1',
+    (Plus L1 s1 t s1' \/ (Star L1 s1 t s1' /\ f2b_order i' i))
+     /\ f2b_match_states i' s1' s2'.
+Proof.
+  intros s2 t s2' STEP2 i s1 MATCH SAFE.
+  inv MATCH.
+(* 1. At matching states *)
+  exploit f2b_progress; eauto. intros TRANS; inv TRANS.
+  (* 1.1  L1 can reach final state and L2 is at final state: impossible! *)
+  exploit (sd_final_nostep determinate); eauto. contradiction.
+  (* 1.2  L1 can make 0 or several steps; L2 can make 1 or several matching steps. *)
+  inv H2. 
+  exploit f2b_determinacy_inv. eexact H5. eexact STEP2.
+  intros [[EQ1 [EQ2 EQ3]] | [NOT1 [NOT2 MT]]].
+  (* 1.2.1  L2 makes a silent transition *)
+  destruct (silent_or_not_silent t2).
+  (* 1.2.1.1  L1 makes a silent transition too: perform transition now and go to "after" state *)
+  subst. simpl in *. destruct (star_starN H6) as [n STEPS2].
+  exists (F2BI_after n); exists s1''; split.
+  left. eapply plus_right; eauto.
+  eapply f2b_match_after'; eauto.
+  (* 1.2.1.2 L1 makes a non-silent transition: keep it for later and go to "before" state *)
+  subst. simpl in *. destruct (star_starN H6) as [n STEPS2].
+  exists (F2BI_before n); exists s1'; split.
+  right; split. auto. constructor.
+  econstructor. eauto. auto. apply star_one; eauto. eauto. eauto. 
+  (* 1.2.2 L2 makes a non-silent transition, and so does L1 *)
+  exploit not_silent_length. eapply (sr_traces receptive); eauto. intros [EQ | EQ].
+  congruence.
+  subst t2. rewrite E0_right in H1. 
+  (* Use receptiveness to equate the traces *)
+  exploit (sr_receptive receptive); eauto. intros [s1''' STEP1].
+  exploit fsim_simulation_not_E0. eexact STEP1. auto. eauto. 
+  intros [i''' [s2''' [P Q]]]. inv P.
+  (* Exploit determinacy *)
+  exploit not_silent_length. eapply (sr_traces receptive); eauto. intros [EQ | EQ].
+  subst t0. simpl in *. exploit sd_determ_1. eauto. eexact STEP2. eexact H2. 
+  intros. elim NOT2. inv H8. auto.
+  subst t2. rewrite E0_right in *. 
+  assert (s4 = s2'). eapply sd_determ_2; eauto. subst s4. 
+  (* Perform transition now and go to "after" state *)
+  destruct (star_starN H7) as [n STEPS2]. exists (F2BI_after n); exists s1'''; split.
+  left. eapply plus_right; eauto. 
+  eapply f2b_match_after'; eauto.
+
+(* 2. Before *)
+  inv H2. congruence.
+  exploit f2b_determinacy_inv. eexact H4. eexact STEP2.
+  intros [[EQ1 [EQ2 EQ3]] | [NOT1 [NOT2 MT]]].
+  (* 2.1 L2 makes a silent transition: remain in "before" state *)
+  subst. simpl in *. exists (F2BI_before n0); exists s1; split.
+  right; split. apply star_refl. constructor. omega.
+  econstructor; eauto. eapply star_right; eauto. 
+  (* 2.2 L2 make a non-silent transition *)
+  exploit not_silent_length. eapply (sr_traces receptive); eauto. intros [EQ | EQ].
+  congruence.
+  subst. rewrite E0_right in *.
+  (* Use receptiveness to equate the traces *)
+  exploit (sr_receptive receptive); eauto. intros [s1''' STEP1].
+  exploit fsim_simulation_not_E0. eexact STEP1. auto. eauto. 
+  intros [i''' [s2''' [P Q]]].
+  (* Exploit determinacy *)
+  exploit f2b_determinacy_star. eauto. eexact STEP2. auto. apply plus_star; eauto. 
+  intro R. inv R. congruence. 
+  exploit not_silent_length. eapply (sr_traces receptive); eauto. intros [EQ | EQ].
+  subst. simpl in *. exploit sd_determ_1. eauto. eexact STEP2. eexact H2. 
+  intros. elim NOT2. inv H7; auto.  
+  subst. rewrite E0_right in *. 
+  assert (s3 = s2'). eapply sd_determ_2; eauto. subst s3.
+  (* Perform transition now and go to "after" state *)
+  destruct (star_starN H6) as [n STEPS2]. exists (F2BI_after n); exists s1'''; split.
+  left. apply plus_one; auto.
+  eapply f2b_match_after'; eauto.
+
+(* 3. After *)
+  inv H. exploit Eapp_E0_inv; eauto. intros [EQ1 EQ2]; subst. 
+  exploit f2b_determinacy_inv. eexact H2. eexact STEP2.
+  intros [[EQ1 [EQ2 EQ3]] | [NOT1 [NOT2 MT]]].
+  subst. exists (F2BI_after n); exists s1; split.
+  right; split. apply star_refl. constructor; omega.
+  eapply f2b_match_after'; eauto.
+  congruence.
+Qed.
+
+(** The backward simulation *)
+
+Lemma forward_to_backward_simulation: backward_simulation L1 L2.
+Proof.
+  apply Backward_simulation with (bsim_order := f2b_order) (bsim_match_states := f2b_match_states).
+  apply wf_f2b_order.
+(* initial states exist *)
+  intros. exploit (fsim_match_initial_states FS); eauto. intros [i [s2 [A B]]].
+  exists s2; auto.
+(* initial states *)
+  intros. exploit (fsim_match_initial_states FS); eauto. intros [i [s2' [A B]]].
+  assert (s2 = s2') by (eapply sd_initial_determ; eauto). subst s2'.
+  exists (F2BI_after O); exists s1; split; auto. econstructor; eauto.
+(* final states *)
+  intros. inv H.
+  exploit f2b_progress; eauto. intros TRANS; inv TRANS.
+  assert (r0 = r) by (eapply (sd_final_determ determinate); eauto). subst r0.
+  exists s1'; auto.
+  inv H4. exploit (sd_final_nostep determinate); eauto. contradiction.
+  inv H5. congruence. exploit (sd_final_nostep determinate); eauto. contradiction.
+  inv H2. exploit (sd_final_nostep determinate); eauto. contradiction.
+(* progress *)
+  intros. inv H. 
+  exploit f2b_progress; eauto. intros TRANS; inv TRANS. 
+  left; exists r; auto. 
+  inv H3. right; econstructor; econstructor; eauto.
+  inv H4. congruence. right; econstructor; econstructor; eauto.
+  inv H1. right; econstructor; econstructor; eauto.
+(* simulation *)
+  exact f2b_simulation_step.
+(* trace length *)
+  exact (sd_traces determinate).
+(* symbols preserved *)
+  exact (fsim_symbols_preserved FS).
 Qed.
 
-End INF_SEQ_DECOMP.
+End FORWARD_TO_BACKWARD.
+
+(** * Connections with big-step semantics *)
+
+(** The general form of a big-step semantics *)
+
+Record bigstep_semantics : Type :=
+  Bigstep_semantics {
+    bigstep_terminates: trace -> int -> Prop;
+    bigstep_diverges: traceinf -> Prop
+  }.
+
+(** Soundness with respect to a small-step semantics *)
+
+Record bigstep_sound (B: bigstep_semantics) (L: semantics) : Prop :=
+  Bigstep_sound {
+    bigstep_terminates_sound:
+      forall t r,
+      bigstep_terminates B t r ->
+      exists s1, exists s2, initial_state L s1 /\ Star L s1 t s2 /\ final_state L s2 r;
+    bigstep_diverges_sound:
+      forall T,
+      bigstep_diverges B T ->
+      exists s1, initial_state L s1 /\ forever (step L) (globalenv L) s1 T
+}.