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

2 files changed, 250 insertions, 233 deletions

diff --git a/driver/Compiler.v b/driver/Compiler.v
index d8810a4..a51cd8f 100644
--- a/driver/Compiler.v
+++ b/driver/Compiler.v
@@ -171,15 +171,19 @@ Definition transf_cminor_program (p: Cminor.program) : res Asm.program :=
    @@ Selection.sel_program
   @@@ transform_partial_program transf_cminorsel_fundef.
 
-Definition transf_c_program (p: Csyntax.program) : res Asm.program :=
+Definition transf_clight_program (p: Clight.program) : res Asm.program :=
   OK p 
-   @@ print print_Csyntax
-  @@@ SimplExpr.transl_program
    @@ print print_Clight
   @@@ Cshmgen.transl_program
   @@@ Cminorgen.transl_program
   @@@ transf_cminor_program.
 
+Definition transf_c_program (p: Csyntax.program) : res Asm.program :=
+  OK p 
+   @@ print print_Csyntax
+  @@@ SimplExpr.transl_program
+  @@@ transf_clight_program.
+
 (** Force [Initializers] to be extracted as well. *)
 
 Definition transl_init := Initializers.transl_init.
@@ -199,16 +203,18 @@ Lemma map_partial_compose:
          (f1: A -> res B) (f2: B -> res C)
          (pa: list (X * A)) (pc: list (X * C)),
   map_partial ctx (fun f => f1 f @@@ f2) pa = OK pc ->
-  exists pb, map_partial ctx f1 pa = OK pb /\ map_partial ctx f2 pb = OK pc.
+  { pb | map_partial ctx f1 pa = OK pb /\ map_partial ctx f2 pb = OK pc }.
 Proof.
   induction pa; simpl.
   intros. inv H. econstructor; eauto.
   intro pc. destruct a as [x a].
-  caseEq (f1 a); simpl; try congruence. intros b F1.
-  caseEq (f2 b); simpl; try congruence. intros c F2 EQ.
-  monadInv EQ. exploit IHpa; eauto. intros [pb [P Q]]. 
+  destruct (f1 a) as [] _eqn; simpl; try congruence.
+  destruct (f2 b) as [] _eqn; simpl; try congruence.
+  destruct (map_partial ctx (fun f => f1 f @@@ f2) pa) as [] _eqn; simpl; try congruence.
+  intros. inv H.
+  destruct (IHpa l) as [pb [P Q]]; auto.
   rewrite P; simpl.
-  exists ((x, b) :: pb); split. auto. simpl. rewrite F2. rewrite Q. auto. 
+  econstructor; split. eauto. simpl. rewrite Heqr0. rewrite Q. auto.
 Qed.
 
 Lemma transform_partial_program_compose:
@@ -216,11 +222,13 @@ Lemma transform_partial_program_compose:
          (f1: A -> res B) (f2: B -> res C)
          (pa: program A V) (pc: program C V),
   transform_partial_program (fun f => f1 f @@@ f2) pa = OK pc ->
-  exists pb, transform_partial_program f1 pa = OK pb /\
-             transform_partial_program f2 pb = OK pc.
+  { pb | transform_partial_program f1 pa = OK pb /\
+         transform_partial_program f2 pb = OK pc }.
 Proof.
-  intros. monadInv H. 
-  exploit map_partial_compose; eauto. intros [xb [P Q]].
+  intros. unfold transform_partial_program in H. 
+  destruct (map_partial prefix_name (fun f : A => f1 f @@@ f2) (prog_funct pa)) as [] _eqn;
+  simpl in H; inv H.
+  destruct (map_partial_compose _ _ _ _ _ _ _ _ _ Heqr) as [xb [P Q]].
   exists (mkprogram xb (prog_main pa) (prog_vars pa)); split.
   unfold transform_partial_program. rewrite P; auto. 
   unfold transform_partial_program. simpl. rewrite Q; auto.
@@ -240,14 +248,14 @@ Lemma transform_program_compose:
          (f1: A -> res B) (f2: B -> C)
          (pa: program A V) (pc: program C V),
   transform_partial_program (fun f => f1 f @@ f2) pa = OK pc ->
-  exists pb, transform_partial_program f1 pa = OK pb /\
-             transform_program f2 pb = pc.
+  { pb | transform_partial_program f1 pa = OK pb /\
+         transform_program f2 pb = pc }.
 Proof.
   intros. 
   replace (fun f : A => f1 f @@ f2)
      with (fun f : A => f1 f @@@ (fun x => OK (f2 x))) in H.
-  exploit transform_partial_program_compose; eauto.
-  intros [pb [X Y]]. exists pb; split. auto. 
+  destruct (transform_partial_program_compose _ _ _ _ _ _ _  _ H) as [pb [X Y]].
+  exists pb; split. auto. 
   apply transform_program_partial_program. auto. 
   apply extensionality; intro. destruct(f1 x); auto. 
 Qed.
@@ -283,9 +291,17 @@ Qed.
 
 (** * Semantic preservation *)
 
-(** We prove that the [transf_program] translations preserve semantics.
-  The proof composes the semantic preservation results for each pass.
-  This establishes the correctness of the whole compiler! *)
+(** We prove that the [transf_program] translations preserve semantics
+  by constructing the following simulations:
+- Forward simulations from [Cstrategy] / [Cminor] / [RTL] to [Asm]
+  (composition of the forward simulations for each pass).
+- Backward simulations for the same languages
+  (derived from the forward simulation, using receptiveness of the source
+  language and determinacy of [Asm]).
+- Backward simulation from [Csem] to [Asm]
+  (composition of two backward simulations).
+
+These results establish the correctness of the whole compiler! *)
 
 Ltac TransfProgInv :=
   match goal with
@@ -300,16 +316,17 @@ Ltac TransfProgInv :=
   end.
 
 Theorem transf_rtl_program_correct:
-  forall p tp beh,
+  forall p tp,
   transf_rtl_program p = OK tp ->
-  not_wrong beh ->
-  RTL.exec_program p beh ->
-  Asm.exec_program tp beh.
+  forward_simulation (RTL.semantics p) (Asm.semantics tp)
+  * backward_simulation (RTL.semantics p) (Asm.semantics tp).
 Proof.
-  intros. unfold transf_rtl_program, transf_rtl_fundef in H.
+  intros.
+  assert (F: forward_simulation (RTL.semantics p) (Asm.semantics tp)).
+  unfold transf_rtl_program, transf_rtl_fundef in H.
   repeat TransfProgInv. 
   repeat rewrite transform_program_print_identity in *. subst. 
-  exploit transform_partial_program_identity; eauto. intro EQ. subst.
+  generalize (transform_partial_program_identity _ _ _ _ X0). intro EQ. subst.
 
   generalize Alloctyping.program_typing_preserved
              Tunnelingtyping.program_typing_preserved
@@ -318,49 +335,93 @@ Proof.
              Reloadtyping.program_typing_preserved
              Stackingtyping.program_typing_preserved; intros.
 
-  eapply Asmgenproof.transf_program_correct; eauto 8.
-  eapply Stackingproof.transf_program_correct; eauto 6.
-  eapply Reloadproof.transf_program_correct; eauto.
-  eapply CleanupLabelsproof.transf_program_correct; eauto.
-  eapply Linearizeproof.transf_program_correct; eauto.
-  eapply Tunnelingproof.transf_program_correct; eauto.
-  eapply Allocproof.transf_program_correct; eauto.
-  eapply CSEproof.transf_program_correct; eauto.
-  eapply Constpropproof.transf_program_correct; eauto.
-  eapply CastOptimproof.transf_program_correct; eauto.
-  eapply Tailcallproof.transf_program_correct; eauto.
+  eapply compose_forward_simulation. apply Tailcallproof.transf_program_correct. 
+  eapply compose_forward_simulation. apply CastOptimproof.transf_program_correct.
+  eapply compose_forward_simulation. apply Constpropproof.transf_program_correct. 
+  eapply compose_forward_simulation. apply CSEproof.transf_program_correct.
+  eapply compose_forward_simulation. apply Allocproof.transf_program_correct. eassumption.
+  eapply compose_forward_simulation. apply Tunnelingproof.transf_program_correct.
+  eapply compose_forward_simulation. apply Linearizeproof.transf_program_correct. eassumption. eauto. 
+  eapply compose_forward_simulation. apply CleanupLabelsproof.transf_program_correct. 
+  eapply compose_forward_simulation. apply Reloadproof.transf_program_correct. eauto.
+  eapply compose_forward_simulation. apply Stackingproof.transf_program_correct. eassumption. eauto 8.
+  apply Asmgenproof.transf_program_correct; eauto 10.
+  split. auto. 
+  apply forward_to_backward_simulation. auto. 
+  apply RTL.semantics_receptive.
+  apply Asm.semantics_determinate.
 Qed.
 
 Theorem transf_cminor_program_correct:
-  forall p tp beh,
+  forall p tp,
   transf_cminor_program p = OK tp ->
-  not_wrong beh ->
-  Cminor.exec_program p beh ->
-  Asm.exec_program tp beh.
+  forward_simulation (Cminor.semantics p) (Asm.semantics tp)
+  * backward_simulation (Cminor.semantics p) (Asm.semantics tp).
 Proof.
-  intros. unfold transf_cminor_program, transf_cminorsel_fundef in H.
+  intros.
+  assert (F: forward_simulation (Cminor.semantics p) (Asm.semantics tp)).
+  unfold transf_cminor_program, transf_cminorsel_fundef in H.
   simpl in H. repeat TransfProgInv.
-  eapply transf_rtl_program_correct; eauto.
-  eapply RTLgenproof.transf_program_correct; eauto.
-  eapply Selectionproof.transf_program_correct; eauto.
+  eapply compose_forward_simulation. apply Selectionproof.transf_program_correct.
+  eapply compose_forward_simulation. apply RTLgenproof.transf_program_correct. eassumption.
+  exact (fst (transf_rtl_program_correct _ _ P)).
+
+  split. auto. 
+  apply forward_to_backward_simulation. auto. 
+  apply Cminor.semantics_receptive.
+  apply Asm.semantics_determinate.
 Qed.
 
-Theorem transf_c_program_correct:
-  forall p tp beh,
-  transf_c_program p = OK tp ->
-  not_wrong beh ->
-  Cstrategy.exec_program p beh ->
-  Asm.exec_program tp beh.
+Theorem transf_clight_program_correct:
+  forall p tp,
+  transf_clight_program p = OK tp ->
+  forward_simulation (Clight.semantics p) (Asm.semantics tp)
+  * backward_simulation (Clight.semantics p) (Asm.semantics tp).
 Proof.
-  intros until beh; unfold transf_c_program; simpl.
-  rewrite print_identity.
-  caseEq (SimplExpr.transl_program p); simpl; try congruence; intros p0 EQ0.
+  intros. 
+  assert (F: forward_simulation (Clight.semantics p) (Asm.semantics tp)).
+  revert H; unfold transf_clight_program; simpl.
   rewrite print_identity.
-  caseEq (Cshmgen.transl_program p0); simpl; try congruence; intros p1 EQ1.
+  caseEq (Cshmgen.transl_program p); simpl; try congruence; intros p1 EQ1.
   caseEq (Cminorgen.transl_program p1); simpl; try congruence; intros p2 EQ2.
-  intros EQ3 NOTW SEM.
-  eapply transf_cminor_program_correct; eauto.
-  eapply Cminorgenproof.transl_program_correct; eauto. 
-  eapply Cshmgenproof.transl_program_correct; eauto.
-  eapply SimplExprproof.transl_program_correct; eauto.
+  intros EQ3.
+  eapply compose_forward_simulation. apply Cshmgenproof.transl_program_correct. eauto.
+  eapply compose_forward_simulation. apply Cminorgenproof.transl_program_correct. eauto.
+  exact (fst (transf_cminor_program_correct _ _ EQ3)). 
+
+  split. auto. 
+  apply forward_to_backward_simulation. auto. 
+  apply Clight.semantics_receptive.
+  apply Asm.semantics_determinate.
+Qed.
+
+Theorem transf_cstrategy_program_correct:
+  forall p tp,
+  transf_c_program p = OK tp ->
+  forward_simulation (Cstrategy.semantics p) (Asm.semantics tp)
+  * backward_simulation (Cstrategy.semantics p) (Asm.semantics tp).
+Proof.
+  intros.
+  assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics tp)).
+  revert H; unfold transf_c_program; simpl. rewrite print_identity.
+  caseEq (SimplExpr.transl_program p); simpl; try congruence; intros p0 EQ0.
+  intros EQ1.
+  eapply compose_forward_simulation. apply SimplExprproof.transl_program_correct. eauto.
+  exact (fst (transf_clight_program_correct _ _ EQ1)). 
+
+  split. auto. 
+  apply forward_to_backward_simulation. auto. 
+  apply Cstrategy.semantics_receptive.
+  apply Asm.semantics_determinate.
+Qed.
+
+Theorem transf_c_program_correct:
+  forall p tp,
+  transf_c_program p = OK tp ->
+  backward_simulation (Csem.semantics p) (Asm.semantics tp).
+Proof.
+  intros. 
+  eapply compose_backward_simulation.
+  apply Cstrategy.strategy_simulation.
+  exact (snd (transf_cstrategy_program_correct _ _ H)).
 Qed.
diff --git a/driver/Complements.v b/driver/Complements.v
index e6b0095..1b7e974 100644
--- a/driver/Complements.v
+++ b/driver/Complements.v
@@ -20,223 +20,179 @@ Require Import Values.
 Require Import Events.
 Require Import Globalenvs.
 Require Import Smallstep.
-Require Import Determinism.
+Require Import Behaviors.
 Require Import Csyntax.
 Require Import Csem.
 Require Import Cstrategy.
+Require Import Clight.
+Require Import Cminor.
+Require Import RTL.
 Require Import Asm.
 Require Import Compiler.
 Require Import Errors.
 
-(** * Integrating a deterministic external world *)
+(** * Preservation of whole-program behaviors *)
 
-(** We now integrate a deterministic external world in the semantics
-  of Compcert C and Asm. *)
+(** From the simulation diagrams proved in file [Compiler]. it follows that
+  whole-program observable behaviors are preserved in the following sense.
+  First, every behavior of the generated assembly code is matched by
+  a behavior of the source C code. *)
 
-Section WORLD.
-
-Variable initial_world: world.
-
-Definition exec_C_program (p: Csyntax.program) (beh: program_behavior) : Prop :=
-  wprogram_behaves _ _
-      Csem.step (Csem.initial_state p) Csem.final_state
-      initial_world (Genv.globalenv p) beh.
-
-Definition exec_asm_program (p: Asm.program) (beh: program_behavior) : Prop :=
-  wprogram_behaves _ _
-      Asm.step (Asm.initial_state p) Asm.final_state
-      initial_world (Genv.globalenv p) beh.
-
-(** ** Safety of C programs. *)
+Theorem transf_c_program_preservation:
+  forall p tp beh,
+  transf_c_program p = OK tp ->
+  program_behaves (Asm.semantics tp) beh ->
+  exists beh', program_behaves (Csem.semantics p) beh' /\ behavior_improves beh' beh.
+Proof.
+  intros. eapply backward_simulation_behavior_improves; eauto. 
+  apply transf_c_program_correct; auto.
+Qed.
 
-(** We show that a C program is safe (in the sense of [Cstrategy.safeprog])
-  if it cannot go wrong in the world-aware semantics. *)
+(** As a corollary, if the source C code cannot go wrong, the behavior of the
+  generated assembly code is one of the possible behaviors of the source C code. *)
 
-Lemma notwrong_safeprog:
-  forall p,
-  (forall beh, exec_C_program p beh -> not_wrong beh) ->
-  Cstrategy.safeprog p initial_world.
+Theorem transf_c_program_is_refinement:
+  forall p tp,
+  transf_c_program p = OK tp ->
+  (forall beh, program_behaves (Csem.semantics p) beh -> not_wrong beh) ->
+  (forall beh, program_behaves (Asm.semantics tp) beh -> program_behaves (Csem.semantics p) beh).
 Proof.
-  intros; red.
-  assert (exists beh1, exec_C_program p beh1).
-    unfold exec_C_program. apply program_behaves_exists. 
-  destruct H0 as [beh1 A].
-  assert (B: not_wrong beh1) by auto.
-  split.
-  inv A; simpl in B.
-  destruct H0. exists (fst s); auto.
-  destruct H0. exists (fst s); auto.
-  destruct H0. exists (fst s); auto.
-  contradiction.
-  contradiction.
-  intros; red; intros.
-  destruct (classic (exists r, Csem.final_state s' r)).
-  (* 1. Final state.  This is immsafe. *)
-  destruct H3 as [r F]. eapply immsafe_final; eauto. 
-  (* 2. Not a final state. *)
-  destruct (classic (nostep (wstep _ _ Csem.step) (Genv.globalenv p) (s', w'))).
-  (* 2.1 No step possible -> going wrong *)
-  elim (H (Goes_wrong t)). 
-  eapply program_goes_wrong.
-  instantiate (1 := (s, initial_world)). split; auto.
-  instantiate (1 := (s', w')). apply Determinism.inject_star; auto. 
-  auto.
-  intros; red; intros. elim H3. exists r; auto. 
-  (* 2.2 One step possible -> this is immsafe *)
-  unfold nostep in H4. 
-  generalize (not_all_ex_not _ _ H4). clear H4. intros [t' P].
-  generalize (not_all_ex_not _ _ P). clear P. intros [s'' Q].
-  generalize (NNPP _ Q). clear Q. intros R. destruct R as [R1 R2]. simpl in *.
-  eapply immsafe_step. eauto. eauto. 
+  intros. eapply backward_simulation_same_safe_behavior; eauto.
+  apply transf_c_program_correct; auto.
 Qed.
 
-(** ** Determinism of Asm semantics *)
+(** If we consider the C evaluation strategy implemented by the compiler,
+  we get stronger preservation results. *)
 
-Remark extcall_arguments_deterministic:
-  forall rs m sg args args',
-  extcall_arguments rs m sg args ->
-  extcall_arguments rs m sg args' -> args = args'.
+Theorem transf_cstrategy_program_preservation:
+  forall p tp,
+  transf_c_program p = OK tp ->
+  (forall beh, program_behaves (Cstrategy.semantics p) beh ->
+     exists beh', program_behaves (Asm.semantics tp) beh' /\ behavior_improves beh beh')
+/\(forall beh, program_behaves (Asm.semantics tp) beh ->
+     exists beh', program_behaves (Cstrategy.semantics p) beh' /\ behavior_improves beh' beh)
+/\(forall beh, not_wrong beh ->
+     program_behaves (Cstrategy.semantics p) beh -> program_behaves (Asm.semantics tp) beh)
+/\(forall beh,
+     (forall beh', program_behaves (Cstrategy.semantics p) beh' -> not_wrong beh') ->
+     program_behaves (Asm.semantics tp) beh ->
+     program_behaves (Cstrategy.semantics p) beh).
 Proof.
-  unfold extcall_arguments; intros. 
-  revert args H args' H0. generalize (Conventions1.loc_arguments sg); induction 1; intros.
-  inv H0; auto.
-  inv H1; decEq; auto. inv H; inv H4; congruence. 
+  intros. intuition.
+  eapply forward_simulation_behavior_improves; eauto. 
+    apply (fst (transf_cstrategy_program_correct _ _ H)).
+  eapply backward_simulation_behavior_improves; eauto. 
+    apply (snd (transf_cstrategy_program_correct _ _ H)).
+  eapply forward_simulation_same_safe_behavior; eauto.
+    apply (fst (transf_cstrategy_program_correct _ _ H)).
+  eapply backward_simulation_same_safe_behavior; eauto.
+    apply (snd (transf_cstrategy_program_correct _ _ H)).
 Qed.
 
-Remark annot_arguments_deterministic:
-  forall rs m pl args args',
-  annot_arguments rs m pl args ->
-  annot_arguments rs m pl args' -> args = args'.
+(** We can also use the alternate big-step semantics for [Cstrategy]
+  to establish behaviors of the generated assembly code. *)
+
+Theorem bigstep_cstrategy_preservation:
+  forall p tp,
+  transf_c_program p = OK tp ->
+  (forall t r,
+     Cstrategy.bigstep_program_terminates p t r ->
+     program_behaves (Asm.semantics tp) (Terminates t r))
+/\(forall T,
+     Cstrategy.bigstep_program_diverges p T ->
+       program_behaves (Asm.semantics tp) (Reacts T)
+    \/ exists t, program_behaves (Asm.semantics tp) (Diverges t) /\ traceinf_prefix t T).
 Proof.
-  unfold annot_arguments; intros. 
-  revert pl args H args' H0. induction 1; intros.
-  inv H0; auto.
-  inv H1; decEq; auto. inv H; inv H4; congruence. 
+  intuition.
+  apply transf_cstrategy_program_preservation with p; auto. red; auto.
+  apply behavior_bigstep_terminates with (Cstrategy.bigstep_semantics p); auto.
+  apply Cstrategy.bigstep_semantics_sound.
+  exploit (behavior_bigstep_diverges (Cstrategy.bigstep_semantics_sound p)). eassumption.
+  intros [A | [t [A B]]]. 
+  left. apply transf_cstrategy_program_preservation with p; auto. red; auto.
+  right; exists t; split; auto. apply transf_cstrategy_program_preservation with p; auto. red; auto.
 Qed.
 
-Lemma step_internal_deterministic:
-  forall ge s t1 s1 t2 s2,
-  Asm.step ge s t1 s1 -> Asm.step ge s t2 s2 -> matching_traces t1 t2 ->
-  s1 = s2 /\ t1 = t2.
-Proof.
+(** * Satisfaction of specifications *)
 
-Ltac InvEQ :=
-  match goal with
-  | [ H1: ?x = ?y, H2: ?x = ?z |- _ ] => rewrite H1 in H2; inv H2; InvEQ
-  | _ => idtac
-  end.
-
-  intros. inv H; inv H0; InvEQ.
-(* regular, regular *)
-  split; congruence.
-(* regular, builtin *)
-  simpl in H5; inv H5.
-(* regular, annot *)
-  simpl in H5; inv H5.
-(* builtin, regular *)
-  simpl in H12; inv H12.
-(* builtin, builtin *)
-  exploit external_call_determ. eexact H5. eexact H12. auto. intros [A [B C]]. subst.
-  auto.
-(* annot, regular *)
-  simpl in H13. inv H13.
-(* annot, annot *)
-  exploit annot_arguments_deterministic. eexact H5. eexact H11. intros EQ; subst. 
-  exploit external_call_determ. eexact H6. eexact H14. auto. intros [A [B C]]. subst.
-  auto.
-(* extcall, extcall *)
-  exploit extcall_arguments_deterministic. eexact H5. eexact H10. intros EQ; subst.
-  exploit external_call_determ. eexact H4. eexact H9. auto. intros [A [B C]]. subst.
-  auto.
-Qed.
+(** The second additional results shows that if all executions
+  of the source C program satisfies a given specification
+  (a predicate on the observable behavior of the program),
+  then all executions of the produced Asm program satisfy
+  this specification as well.  
 
-Lemma initial_state_deterministic:
-  forall p s1 s2,
-  initial_state p s1 -> initial_state p s2 -> s1 = s2.
-Proof.
-  intros. inv H; inv H0. f_equal. congruence.
-Qed.
+  We first show this result for specifications that are stable
+  under the [behavior_improves] relation. *) 
 
-Lemma final_state_not_step:
-  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.
-Qed.
+Section SPECS_PRESERVED.
 
-Lemma final_state_deterministic:
-  forall st r1 r2, final_state st r1 -> final_state st r2 -> r1 = r2.
-Proof.
-  intros. inv H; inv H0. congruence.
-Qed.
+Variable spec: program_behavior -> Prop.
+
+Hypothesis spec_stable:
+  forall beh1 beh2, behavior_improves beh1 beh2 -> spec beh1 -> spec beh2.
 
-Theorem asm_exec_program_deterministic:
-  forall p beh1 beh2,
-  exec_asm_program p beh1 -> exec_asm_program p beh2 ->
-  beh1 = beh2.
+Theorem transf_c_program_preserves_spec:
+  forall p tp,
+  transf_c_program p = OK tp ->
+  (forall beh, program_behaves (Csem.semantics p) beh -> spec beh) ->
+  (forall beh, program_behaves (Asm.semantics tp) beh -> spec beh).
 Proof.
-  intros. hnf in H; hnf in H0.
-  eapply (program_behaves_deterministic _ _
-             (wstep _ _ step)
-             (winitial_state _ (initial_state p) initial_world)
-             (wfinal_state _ final_state));
-  eauto.
-  apply wstep_deterministic. apply step_internal_deterministic.
-  apply winitial_state_determ. apply initial_state_deterministic.
-  apply wfinal_state_determ. apply final_state_deterministic.
-  apply wfinal_state_nostep. apply final_state_not_step.
+  intros.
+  exploit transf_c_program_preservation; eauto. intros [beh' [A B]].
+  apply spec_stable with beh'; auto. 
 Qed.
 
-(** * Additional semantic preservation property *)
+End SPECS_PRESERVED.
+
+(** As a corollary, we obtain preservation of safety specifications:
+  specifications that exclude "going wrong" behaviors. *)
 
-(** 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 Compcert C
-  program that has well-defined semantics, all possible executions
-  of the resulting Asm code correspond to an execution of
-  the source program. *)
+Section SAFETY_PRESERVED.
 
-Theorem transf_c_program_is_refinement:
+Variable spec: program_behavior -> Prop.
+
+Hypothesis spec_safety:
+  forall beh, spec beh -> not_wrong beh.
+
+Theorem transf_c_program_preserves_safety_spec:
   forall p tp,
   transf_c_program p = OK tp ->
-  (forall beh, exec_C_program p beh -> not_wrong beh) ->
-  (forall beh, exec_asm_program tp beh -> exec_C_program p beh).
+  (forall beh, program_behaves (Csem.semantics p) beh -> spec beh) ->
+  (forall beh, program_behaves (Asm.semantics tp) beh -> spec beh).
 Proof.
-  intros. 
-  exploit Cstrategy.strategy_behavior.
-  apply notwrong_safeprog. eauto. 
-  intros [beh1 [A [B [C D]]]].
-  assert (Asm.exec_program tp beh1).
-    eapply transf_c_program_correct; eauto.
-  assert (exec_asm_program tp beh1).
-    red. apply inject_behaviors; auto.
-  assert (beh = beh1). eapply asm_exec_program_deterministic; eauto.
-  subst beh.
-  red. apply inject_behaviors; auto.
+  intros. eapply transf_c_program_preserves_spec; eauto. 
+  intros. destruct H2. congruence. destruct H2 as [t [EQ1 EQ2]]. 
+  subst beh1. elim (spec_safety _ H3). 
 Qed.
 
-Section SPECS_PRESERVED.
+End SAFETY_PRESERVED.
 
-(** The second additional results shows that if one execution
-  of the source C program satisfies a given specification
-  (a predicate on the observable behavior of the program),
-  then all executions of the produced Asm program satisfy
-  this specification as well.  *) 
+(** We also have preservation of liveness specifications:
+  specifications that assert the existence of a prefix of the observable
+  trace satisfying some conditions. *)
 
-Variable spec: program_behavior -> Prop.
+Section LIVENESS_PRESERVED.
 
-Hypothesis spec_not_wrong: forall b, spec b -> not_wrong b.
+Variable spec: trace -> Prop.
 
-Theorem transf_c_program_preserves_spec:
+Definition liveness_spec_satisfied (b: program_behavior) : Prop :=
+  exists t, behavior_prefix t b /\ spec t.
+
+Theorem transf_c_program_preserves_liveness_spec:
   forall p tp,
   transf_c_program p = OK tp ->
-  (forall beh, exec_C_program p beh -> spec beh) ->
-  (forall beh, exec_asm_program tp beh -> spec beh).
+  (forall beh, program_behaves (Csem.semantics p) beh -> liveness_spec_satisfied beh) ->
+  (forall beh, program_behaves (Asm.semantics tp) beh -> liveness_spec_satisfied beh).
 Proof.
-  intros. apply H0. apply transf_c_program_is_refinement with tp; auto. 
+  intros. eapply transf_c_program_preserves_spec; eauto.
+  intros. destruct H3 as [t1 [A B]]. destruct H2.
+  subst. exists t1; auto.
+  destruct H2 as [t [C D]]. subst.
+  destruct A as [b1 E]. destruct D as [b2 F].
+  destruct b1; simpl in E; inv E.
+  exists t1; split; auto. 
+  exists (behavior_app t0 b2); apply behavior_app_assoc. 
 Qed.
 
-End SPECS_PRESERVED.
-
-End WORLD.
+End LIVENESS_PRESERVED.