Distinguish two kinds of nonterminating behaviors: silent divergence

and reactive divergence.  As a consequence:
- Removed the Enilinf constructor from traceinf (values of traceinf
  type are always infinite traces).
- Traces are now uniquely defined.
- Adapted proofs big step -> small step for Clight and Cminor accordingly.
- Strengthened results in driver/Complements accordingly.
- Added common/Determinism to collect generic results about
  deterministic semantics.


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

1 files changed, 39 insertions, 537 deletions

diff --git a/driver/Complements.v b/driver/Complements.v
index dfd3c454..6fe50381 100644
--- a/driver/Complements.v
+++ b/driver/Complements.v
@@ -20,6 +20,7 @@ Require Import Values.
 Require Import Events.
 Require Import Globalenvs.
 Require Import Smallstep.
+Require Import Determinism.
 Require Import Csyntax.
 Require Import Csem.
 Require Import Asm.
@@ -29,159 +30,8 @@ Require Import Errors.
 (** * Determinism of Asm semantics *)
 
 (** In this section, we show that the semantics for the Asm language
-  are deterministic, in a sense to be made precise later.
-  There are two sources of apparent non-determinism:
-- The semantics leaves unspecified the results of calls to external 
-  functions.  Different results to e.g. a "read" operation can of
-  course lead to different behaviors for the program.
-  We address this issue by modeling a notion of deterministic
-  external world that uniquely determines the results of external calls.
-- For diverging executions, the trace of I/O events is not uniquely
-  determined: it can contain events that will never be performed
-  because the program diverges earlier.  We address this issue
-  by showing the existence of a minimal trace for diverging executions.
-
-*)
-
-(** ** Deterministic worlds *)
-
-(** An external world is a function that, given the name of an
-  external call and its arguments, returns either [None], meaning
-  that this external call gets stuck, or [Some(r,w)], meaning
-  that this external call succeeds, has result [r], and changes
-  the world to [w]. *)
-
-Inductive world: Type :=
-  World: (ident -> list eventval -> option (eventval * world)) -> world.
-
-Definition nextworld (w: world) (evname: ident) (evargs: list eventval) :
-                     option (eventval * world) :=
-  match w with World f => f evname evargs end.
-
-(** A trace is possible in a given world if all events correspond
-  to non-stuck external calls according to the given world.
-  Two predicates are defined, for finite and infinite traces respectively:
-- [possible_trace w t w'], where [w] is the initial state of the
-  world, [t] the finite trace of interest, and [w'] the state of the
-  world after performing trace [t].
-- [possible_traceinf w T], where [w] is the initial state of the
-  world and [T] the possibly infinite trace of interest.
-*)
-
-Inductive possible_trace: world -> trace -> world -> Prop :=
-  | possible_trace_nil: forall w,
-      possible_trace w E0 w
-  | possible_trace_cons: forall w0 evname evargs evres w1 t w2,
-      nextworld w0 evname evargs = Some (evres, w1) ->
-      possible_trace w1 t w2 ->
-      possible_trace w0 (mkevent evname evargs evres :: t) w2.
-
-Lemma possible_trace_app:
-  forall t2 w2 w0 t1 w1,
-  possible_trace w0 t1 w1 -> possible_trace w1 t2 w2 ->
-  possible_trace w0 (t1 ** t2) w2.
-Proof.
-  induction 1; simpl; intros.
-  auto.
-  econstructor; eauto.
-Qed.
-
-Lemma possible_trace_app_inv:
-  forall t2 w2 t1 w0,
-  possible_trace w0 (t1 ** t2) w2 ->
-  exists w1, possible_trace w0 t1 w1 /\ possible_trace w1 t2 w2.
-Proof.
-  induction t1; simpl; intros.
-  exists w0; split. constructor. auto.
-  inv H. exploit IHt1; eauto. intros [w1 [A B]]. 
-  exists w1; split. econstructor; eauto. auto.
-Qed.
-
-CoInductive possible_traceinf: world -> traceinf -> Prop :=
-  | possible_traceinf_nil: forall w0,
-      possible_traceinf w0 Enilinf
-  | possible_traceinf_cons: forall w0 evname evargs evres w1 T,
-      nextworld w0 evname evargs = Some (evres, w1) ->
-      possible_traceinf w1 T ->
-      possible_traceinf w0 (Econsinf (mkevent evname evargs evres) T).
-
-Lemma possible_traceinf_app:
-  forall t2 w0 t1 w1,
-  possible_trace w0 t1 w1 -> possible_traceinf w1 t2 ->
-  possible_traceinf w0 (t1 *** t2).
-Proof.
-  induction 1; simpl; intros.
-  auto.
-  econstructor; eauto.
-Qed.
-
-Lemma possible_traceinf_app_inv:
-  forall t2 t1 w0,
-  possible_traceinf w0 (t1 *** t2) ->
-  exists w1, possible_trace w0 t1 w1 /\ possible_traceinf w1 t2.
-Proof.
-  induction t1; simpl; intros.
-  exists w0; split. constructor. auto.
-  inv H. exploit IHt1; eauto. intros [w1 [A B]]. 
-  exists w1; split. econstructor; eauto. auto.
-Qed.
-
-Ltac possibleTraceInv :=
-  match goal with
-  | [H: possible_trace _ (_ ** _) _ |- _] =>
-      let P1 := fresh "P" in
-      let w := fresh "w" in
-      let P2 := fresh "P" in
-      elim (possible_trace_app_inv _ _ _ _ H); clear H;
-      intros w [P1 P2];
-      possibleTraceInv
-  | [H: possible_traceinf _ (_ *** _) |- _] =>
-      let P1 := fresh "P" in
-      let w := fresh "w" in
-      let P2 := fresh "P" in
-      elim (possible_traceinf_app_inv _ _ _ H); clear H;
-      intros w [P1 P2];
-      possibleTraceInv
-  | _ => idtac
-  end.
-
-(** Determinism properties of [event_match]. *)
-
-Remark eventval_match_deterministic:
-  forall ev1 ev2 ty v1 v2,
-  eventval_match ev1 ty v1 -> eventval_match ev2 ty v2 ->
-  (ev1 = ev2 <-> v1 = v2).
-Proof.
-  intros. inv H; inv H0; intuition congruence.
-Qed.
-
-Remark eventval_list_match_deterministic:
-  forall ev1 ty v, eventval_list_match ev1 ty v ->
-  forall ev2, eventval_list_match ev2 ty v -> ev1 = ev2.
-Proof.
-  induction 1; intros.
-  inv H. auto.
-  inv H1. decEq.
-  rewrite (eventval_match_deterministic _ _ _ _ _ H H6). auto.
-  eauto.
-Qed.
-
-Lemma event_match_deterministic:
-  forall w0 t1 w1 t2 w2 ef vargs vres1 vres2,
-  possible_trace w0 t1 w1 ->
-  possible_trace w0 t2 w2 ->
-  event_match ef vargs t1 vres1 ->
-  event_match ef vargs t2 vres2 ->
-  vres1 = vres2 /\ t1 = t2 /\ w1 = w2.
-Proof.
-  intros. inv H1. inv H2. 
-  assert (eargs = eargs0). eapply eventval_list_match_deterministic; eauto. subst eargs0.
-  inv H. inv H12. inv H0. inv H12.
-  rewrite H11 in H10. inv H10. intuition. 
-  rewrite <- (eventval_match_deterministic _ _ _ _ _ H4 H5). auto.
-Qed.
-
-(** ** Determinism of Asm transitions. *)
+  are deterministic, provided that the program is executed against a
+  deterministic world, as formalized in module [Determinism]. *)
 
 Remark extcall_arguments_deterministic:
   forall rs m sg args args',
@@ -199,22 +49,26 @@ Proof.
   unfold extcall_arguments; intros; eauto.
 Qed.
 
-Lemma step_deterministic:
-  forall ge s0 t1 s1 t2 s2 w0 w1 w2,
-  step ge s0 t1 s1 -> step ge s0 t2 s2 ->
-  possible_trace w0 t1 w1 -> possible_trace w0 t2 w2 ->
-  s1 = s2 /\ t1 = t2 /\ w1 = w2.
+Lemma step_internal_deterministic:
+  forall ge s t1 s1 t2 s2,
+  Asm.step ge s t1 s1 -> Asm.step ge s t2 s2 -> internal_determinism _ t1 s1 t2 s2.
 Proof.
   intros. inv H; inv H0.
-  assert (c0 = c) by congruence. subst c0.
-  assert (i0 = i) by congruence. subst i0.
-  split. congruence. split. auto. inv H1; inv H2; auto.
+  assert (c0 = c) by congruence.
+  assert (i0 = i) by congruence.
+  assert (rs'0 = rs') by congruence.
+  assert (m'0 = m') by congruence.
+  subst. constructor.
   congruence.
   congruence.
   assert (ef0 = ef) by congruence. subst ef0.
   assert (args0 = args). eapply extcall_arguments_deterministic; eauto. subst args0.
-  exploit event_match_deterministic. eexact H1. eexact H2. eauto. eauto.
-  intros [A [B C]]. intuition congruence.
+  inv H3; inv H8.
+  assert (eargs0 = eargs). eapply eventval_list_match_deterministic; eauto. subst eargs0.
+  constructor. intros.
+  exploit eventval_match_deterministic. eexact H0. eexact H5. intros. 
+  assert (res = res0). tauto. 
+  congruence.
 Qed.
 
 Lemma initial_state_deterministic:
@@ -224,10 +78,8 @@ Proof.
   intros. inv H; inv H0. reflexivity. 
 Qed.
 
-Definition nostep (ge: genv) (st: state) : Prop := forall t st', ~step ge st t st'.
-
 Lemma final_state_not_step:
-  forall ge st r, final_state st r -> nostep ge st.
+  forall ge st r, final_state st r -> nostep step ge st.
 Proof.
   unfold nostep. intros. red; intros. inv H. inv H0.
   unfold Vzero in H1. congruence.
@@ -240,373 +92,41 @@ Proof.
   intros. inv H; inv H0. congruence.
 Qed.
 
-(** ** Determinism for terminating executions. *)
-
-Lemma steps_deterministic:
-  forall ge s0 t1 s1, star step ge s0 t1 s1 -> 
-  forall t2 s2 w0 w1 w2, star step ge s0 t2 s2 -> 
-  nostep ge s1 -> nostep ge s2 ->
-  possible_trace w0 t1 w1 -> possible_trace w0 t2 w2 ->
-  t1 = t2 /\ s1 = s2.
-Proof.
-  induction 1; intros. 
-  inv H. auto. 
-  elim (H0 _ _ H4).
-  inv H2. elim (H4 _ _ H). 
-  possibleTraceInv.
-  exploit step_deterministic. eexact H. eexact H7. eauto. eauto. 
-  intros [A [B C]]. subst s5 t3 w3.
-  exploit IHstar; eauto. intros [A B]. split; congruence.
-Qed.
-
-(** ** Determinism for infinite transition sequences. *)
-
-Lemma forever_star_inv:
-  forall ge s t s', star step ge s t s' ->
-  forall T w w', forever step ge s T ->
-  possible_trace w t w' -> possible_traceinf w T ->
-  exists T',
-  forever step ge s' T' /\ possible_traceinf w' T' /\ T = t *** T'.
-Proof.
-  induction 1; intros.
-  inv H0. exists T; auto.
-  subst t. possibleTraceInv. 
-  inv H2. possibleTraceInv. 
-  exploit step_deterministic.
-    eexact H. eexact H1. eauto. eauto. intros [A [B C]]; subst s4 t1 w1.
-  exploit IHstar; eauto. intros [T' [A [B C]]]. 
-  exists T'; split. auto.
-  split. auto.
-  rewrite C. rewrite Eappinf_assoc; auto.
-Qed.
-
-Lemma star_final_not_forever:
-  forall ge s1 t s2 T w1 w2,
-  star step ge s1 t s2 ->
-  nostep ge s2 -> forever step ge s1 T ->
-  possible_trace w1 t w2 -> possible_traceinf w1 T ->
-  False.
-Proof.
-  intros. exploit forever_star_inv; eauto. intros [T' [A [B C]]]. 
-  inv A. elim (H0 _ _ H4). 
-Qed.
-
-(** ** Minimal traces for divergence. *)
-
-(** There are two mutually exclusive way in which a program can diverge.
-  It can diverge in a reactive fashion: it performs infinitely many
-  external calls, and the internal computations between two external
-  calls are always finite.  Or it can diverge silently: after a finite
-  number of external calls, it enters an infinite sequence of internal
-  computations. *)
-
-Definition reactive (ge: genv) (s: state) (w: world) :=
-  forall t s1 w1,
-  star step ge s t s1 -> possible_trace w t w1 ->
-  exists s2, exists t', exists s3, exists w2,
-  star step ge s1 E0 s2 
-  /\ step ge s2 t' s3
-  /\ possible_trace w1 t' w2
-  /\ t' <> E0.
-
-Definition diverges_silently (ge: genv) (s: state) :=
-  forall s2, star step ge s E0 s2 -> exists s3, step ge s2 E0 s3.
-
-Definition diverges_eventually (ge: genv) (s: state) (w: world) :=
-  exists t, exists s1, exists w1,
-  star step ge s t s1 /\ possible_trace w t w1 /\ diverges_silently ge s1.
-
-(** Using classical logic, we show that any infinite sequence of transitions
-  that is possible in a deterministic world is of one of the two forms 
-  described above. *)
-
-Lemma reactive_or_diverges:
-  forall ge s T w,
-  forever step ge s T -> possible_traceinf w T ->
-  reactive ge s w \/ diverges_eventually ge s w.
-Proof.
-  intros. elim (classic (diverges_eventually ge s w)); intro.
-  right; auto.
-  left. red; intros.
-  generalize (not_ex_all_not trace _ H1 t).
-  intro. clear H1.
-  generalize (not_ex_all_not state _ H4 s1).
-  intro. clear H4.
-  generalize (not_ex_all_not world _ H1 w1).
-  intro. clear H1.
-  elim (not_and_or _ _ H4); clear H4; intro.
-  contradiction.
-  elim (not_and_or _ _ H1); clear H1; intro.
-  contradiction.
-  generalize (not_all_ex_not state _ H1). intros [s2 A]. clear H1.
-  destruct (imply_to_and _ _ A). clear A.
-  exploit forever_star_inv.
-    eapply star_trans. eexact H2. eexact H1. reflexivity.
-    eauto. rewrite E0_right. eauto. eauto. 
-  intros [T' [A [B C]]]. 
-  inv A. possibleTraceInv. 
-  exists s2; exists t0; exists s3; exists w4. intuition.
-  subst t0. apply H4. exists s3; auto.
-Qed.
-
-(** Moreover, a program cannot be both reactive and silently diverging. *)
-
-Lemma reactive_not_diverges:
-  forall ge s w,
-  reactive ge s w -> diverges_eventually ge s w -> False.
-Proof.
-  intros. destruct H0 as [t [s1 [w1 [A [B C]]]]]. 
-  destruct (H _ _ _ A B) as [s2 [t' [s3 [w2 [P [Q [R S]]]]]]].
-  destruct (C _ P) as [s4 T].
-  assert (s3 = s4 /\ t' = E0 /\ w2 = w1).
-    eapply step_deterministic; eauto. constructor.
-  intuition congruence.
-Qed.
-
-(** A program that silently diverges can be given any finite or
-  infinite trace of events.  In particular, taking [T' = Enilinf],
-  it can be given the empty trace of events. *)
-
-Lemma diverges_forever:
-  forall ge s1 T w T',
-  diverges_silently ge s1 ->
-  forever step ge s1 T ->
-  possible_traceinf w T ->
-  forever step ge s1 T'.
-Proof.
-  cofix COINDHYP; intros. inv H0. possibleTraceInv. 
-  assert (exists s3, step ge s1 E0 s3). apply H. constructor.
-  destruct H0 as [s3 C]. 
-  assert (s2 = s3 /\ t = E0 /\ w0 = w). eapply step_deterministic; eauto. constructor.
-  destruct H0 as [Q [R S]]. subst s3 t w0. 
-  change T' with (E0 *** T'). econstructor. eassumption. 
-  eapply COINDHYP; eauto. 
-  red; intros. apply H. eapply star_left; eauto. 
-Qed.
-
-(** The trace of I/O events generated by a reactive diverging program
-  is uniquely determined up to bisimilarity. *)
-
-Lemma reactive_sim:
-  forall ge s w T1 T2,
-  reactive ge s w ->
-  forever step ge s T1 ->
-  forever step ge s T2 ->
-  possible_traceinf w T1 ->
-  possible_traceinf w T2 ->
-  traceinf_sim T1 T2.
-Proof.
-  cofix COINDHYP; intros.
-  elim (H E0 s w); try constructor. 
-  intros s2 [t' [s3 [w2 [A [B [C D]]]]]].
-  assert (star step ge s t' s3). eapply star_right; eauto. 
-  destruct (forever_star_inv _ _ _ _ H4 _ _ _ H0 C H2)
-  as [T1' [P [Q R]]].
-  destruct (forever_star_inv _ _ _ _ H4 _ _ _ H1 C H3)
-  as [T2' [S [T U]]].
-  destruct t'. unfold E0 in D. congruence.
-  assert (t' = nil). inversion B. inversion H7. auto. subst t'.
-  subst T1 T2. simpl. constructor.
-  apply COINDHYP with ge s3 w2; auto.
-  red; intros. eapply H. eapply star_trans; eauto.
-  eapply possible_trace_app; eauto. 
-Qed.
-
-(** A trace is minimal for a program if it is a prefix of all possible
-  traces. *)
-
-Definition minimal_trace (ge: genv) (s: state) (w: world) (T: traceinf) :=
-  forall T',
-  forever step ge s T' -> possible_traceinf w T' ->
-  traceinf_prefix T T'.
-
-(** For any program that diverges with some possible trace [T1],
-  the set of possible traces admits a minimal element [T].
-  If the program is reactive, this trace is [T1]. 
-  If the program silently diverges, this trace is the finite trace
-  of events performed prior to silent divergence. *)
-
-Lemma forever_minimal_trace:
-  forall ge s T1 w,
-  forever step ge s T1 -> possible_traceinf w T1 ->
-  exists T,
-     forever step ge s T
-  /\ possible_traceinf w T
-  /\ minimal_trace ge s w T.
+Theorem asm_exec_program_deterministic:
+  forall p w beh1 beh2,
+  Asm.exec_program p beh1 -> Asm.exec_program p beh2 ->
+  possible_behavior w beh1 -> possible_behavior w beh2 ->
+  beh1 = beh2.
 Proof.
   intros. 
-  destruct (reactive_or_diverges _ _ _ _ H H0).
-  (* reactive *)
-  exists T1; split. auto. split. auto. red; intros.
-  elim (reactive_or_diverges _ _ _ _ H2 H3); intro.
-  apply traceinf_sim_prefix. eapply reactive_sim; eauto. 
-  elimtype False. eapply reactive_not_diverges; eauto.
-  (* diverges *) 
-  elim H1. intros t [s1 [w1 [A [B C]]]].
-  exists (t *** Enilinf); split.
-  exploit forever_star_inv; eauto. intros [T' [P [Q R]]]. 
-  eapply star_forever. eauto. 
-  eapply diverges_forever; eauto.
-  split. eapply possible_traceinf_app. eauto. constructor. 
-  red; intros. exploit forever_star_inv. eauto. eexact H2. eauto. eauto.
-  intros [T2 [P [Q R]]].
-  subst T'. apply traceinf_prefix_app. constructor.
-Qed.
-
-(** ** Refined semantics for program executions. *)
-
-(** We now define the following variant [exec_program'] of the
-  [exec_program] predicate defined in module [Smallstep].
-  In the diverging case [Diverges T], the new predicate imposes that the
-  finite or infinite trace [T] is minimal. *)
-
-Inductive exec_program' (p: program) (w: world): program_behavior -> Prop :=
-  | program_terminates': forall s t s' w' r,
-      initial_state p s ->
-      star step (Genv.globalenv p) s t s' ->
-      possible_trace w t w' ->
-      final_state s' r ->
-      exec_program' p w (Terminates t r)
-  | program_diverges': forall s T,
-      initial_state p s ->
-      forever step (Genv.globalenv p) s T ->
-      possible_traceinf w T ->
-      minimal_trace (Genv.globalenv p) s w T ->
-      exec_program' p w (Diverges T)
-  | program_goes_wrong': forall s t s' w',
-      initial_state p s ->
-      star step (Genv.globalenv p) s t s' ->
-      possible_trace w t w' -> 
-      nostep (Genv.globalenv p) s' ->
-       (forall r, ~final_state s' r) ->
-      exec_program' p w (Goes_wrong t).
-
-(** We show that any [exec_program] execution corresponds to
-  an [exec_program'] execution. *)
-
-Definition possible_behavior (w: world) (b: program_behavior) : Prop :=
-  match b with
-  | Terminates t r => exists w', possible_trace w t w'
-  | Diverges T => possible_traceinf w T
-  | Goes_wrong t => exists w', possible_trace w t w'
-  end.
-
-Inductive matching_behaviors: program_behavior -> program_behavior -> Prop :=
-  | matching_behaviors_terminates: forall t r,
-      matching_behaviors (Terminates t r) (Terminates t r)
-  | matching_behaviors_diverges: forall T1 T2,
-      traceinf_prefix T2 T1 ->
-      matching_behaviors (Diverges T1) (Diverges T2)
-  | matching_behaviors_goeswrong: forall t ,
-      matching_behaviors (Goes_wrong t) (Goes_wrong t).
-
-Theorem exec_program_program':
-  forall p b w,
-  exec_program p b -> possible_behavior w b ->
-  exists b', exec_program' p w b' /\ matching_behaviors b b'.
-Proof.
-  intros. inv H; simpl in H0.
-  (* termination *)
-  destruct H0 as [w' A].
-  exists (Terminates t r).
-  split. econstructor; eauto. constructor.
-  (* divergence *)
-  exploit forever_minimal_trace; eauto. intros [T0 [A [B C]]].
-  exists (Diverges T0); split.
-  econstructor; eauto.
-  constructor. apply C; auto.
-  (* going wrong *)
-  destruct H0 as [w' A].
-  exists (Goes_wrong t).
-  split. econstructor; eauto. constructor.
-Qed.
-
-(** Moreover, [exec_program'] is deterministic, in that the behavior
-  associated with a given program and external world is uniquely
-  defined up to bisimilarity between infinite traces. *)
-
-Inductive same_behaviors: program_behavior -> program_behavior -> Prop :=
-  | same_behaviors_terminates: forall t r,
-      same_behaviors (Terminates t r) (Terminates t r)
-  | same_behaviors_diverges: forall T1 T2,
-      traceinf_sim T2 T1 ->
-      same_behaviors (Diverges T1) (Diverges T2)
-  | same_behaviors_goes_wrong: forall t,
-      same_behaviors (Goes_wrong t) (Goes_wrong t).
-
-Theorem exec_program'_deterministic:
-  forall p b1 b2 w,
-  exec_program' p w b1 -> exec_program' p w b2 ->
-  same_behaviors b1 b2.
-Proof.
-  intros. inv H; inv H0;
-  try (assert (s0 = s) by (eapply initial_state_deterministic; eauto); subst s0).
-  (* terminates, terminates *)
-  exploit steps_deterministic. eexact H2. eexact H5.
-  eapply final_state_not_step; eauto. eapply final_state_not_step; eauto. eauto. eauto.
-  intros [A B]. subst. 
-  exploit final_state_deterministic. eexact H4. eexact H7.
-  intro. subst. constructor.
-  (* terminates, diverges *)
-  byContradiction. eapply star_final_not_forever; eauto. eapply final_state_not_step; eauto.
-  (* terminates, goes wrong *)
-  exploit steps_deterministic. eexact H2. eexact H5.
-  eapply final_state_not_step; eauto. auto. eauto. eauto.
-  intros [A B]. subst. elim (H8 _ H4).
-  (* diverges, terminates *)
-  byContradiction. eapply star_final_not_forever; eauto. eapply final_state_not_step; eauto.
-  (* diverges, diverges *)
-  constructor. apply traceinf_prefix_2_sim; auto.
-  (* diverges, goes wrong *)
-  byContradiction. eapply star_final_not_forever; eauto.
-  (* goes wrong, terminates *)
-  exploit steps_deterministic. eexact H2. eexact H6. eauto. 
-  eapply final_state_not_step; eauto. eauto. eauto.
-  intros [A B]. subst. elim (H5 _ H8).
-  (* goes wrong, diverges *)
-  byContradiction. eapply star_final_not_forever; eauto.
-  (* goes wrong, goes wrong *)
-  exploit steps_deterministic. eexact H2. eexact H6.
-  eauto. eauto. eauto. eauto.
-  intros [A B]. subst. constructor.
-Qed.
-
-Lemma matching_behaviors_same:
-  forall b b1' b2',
-  matching_behaviors b b1' -> same_behaviors b1' b2' ->
-  matching_behaviors b b2'.
-Proof.
-  intros. inv H; inv H0. 
-  constructor.
-  constructor. apply traceinf_prefix_compat with T2 T1.
-  auto. apply traceinf_sim_sym; auto. apply traceinf_sim_refl.
-  constructor.
+  eapply (program_behaves_deterministic _ _ step (initial_state p) final_state); eauto.
+  exact step_internal_deterministic.
+  exact (initial_state_deterministic p).
+  exact final_state_deterministic.
+  exact final_state_not_step.
 Qed.
 
 (** * Additional semantic preservation property *)
 
-(** Combining the semantic preservation theorem from module [Main]
+(** Combining the semantic preservation theorem from module [Compiler]
   with the determinism of Asm executions, we easily obtain
   additional, stronger semantic preservation properties.
   The first property states that, when compiling a Clight
   program that has well-defined semantics, all possible executions
   of the resulting Asm code correspond to an execution of
-  the source Clight program, in the sense of the [matching_behaviors]
-  predicate. *)
+  the source Clight program. *)
 
-Theorem transf_c_program_correct_strong:
+Theorem transf_c_program_is_refinement:
   forall p tp w,
   transf_c_program p = OK tp ->
   (exists b, Csem.exec_program p b /\ possible_behavior w b /\ not_wrong b) ->
-  (forall b, exec_program' tp w b -> exists b0, Csem.exec_program p b0 /\ matching_behaviors b0 b).
+  (forall b, Asm.exec_program tp b -> possible_behavior w b -> Csem.exec_program p b).
 Proof.
   intros. destruct H0 as [b0 [A [B C]]]. 
   assert (Asm.exec_program tp b0).
     eapply transf_c_program_correct; eauto.
-  exploit exec_program_program'; eauto. 
-  intros [b1 [D E]].
-  assert (same_behaviors b1 b). eapply exec_program'_deterministic; eauto.
-  exists b0. split. auto. eapply matching_behaviors_same; eauto.
+  assert (b = b0). eapply asm_exec_program_deterministic; eauto.
+  subst b0. auto.
 Qed.
 
 Section SPECS_PRESERVED.
@@ -619,37 +139,19 @@ Section SPECS_PRESERVED.
 
 Variable spec: program_behavior -> Prop.
 
-(* Since the execution trace for a diverging Clight program
-   is not uniquely defined (the trace can contain events that
-   the program will never perform because it loops earlier),
-   this result holds only if the specification is closed under
-   prefixes in the case of diverging executions.  This is the
-   case for all safety properties (some undesirable event never
-   occurs), but not for liveness properties (some desirable event
-   always occurs). *)
-
-Hypothesis spec_safety:
-  forall T T', traceinf_prefix T T' -> spec (Diverges T') -> spec (Diverges T).
+Hypothesis spec_not_wrong: forall b, spec b -> not_wrong b.
 
 Theorem transf_c_program_preserves_spec:
   forall p tp w,
   transf_c_program p = OK tp ->
-  (exists b, Csem.exec_program p b /\ possible_behavior w b /\ not_wrong b) ->
-  (forall b, Csem.exec_program p b -> possible_behavior w b -> spec b) ->
-  (forall b, exec_program' tp w b -> not_wrong b /\ spec b).
+  (exists b, Csem.exec_program p b /\ possible_behavior w b /\ spec b) ->
+  (forall b, Asm.exec_program tp b -> possible_behavior w b -> spec b).
 Proof.
   intros. destruct H0 as [b1 [A [B C]]].
   assert (Asm.exec_program tp b1).
     eapply transf_c_program_correct; eauto.
-  exploit exec_program_program'; eauto. 
-  intros [b' [D E]].
-  assert (same_behaviors b b'). eapply exec_program'_deterministic; eauto.
-  inv E; inv H3. 
-  auto.
-  split. simpl. auto. apply spec_safety with T1. 
-  eapply traceinf_prefix_compat. eauto. auto. apply traceinf_sim_refl.
-  auto.
-  simpl in C. contradiction.
+  assert (b1 = b). eapply asm_exec_program_deterministic; eauto. 
+  subst b1. auto.
 Qed.
 
 End SPECS_PRESERVED.