From 93b89122000e42ac57abc39734fdf05d3a89e83c Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Fri, 15 Jul 2011 08:26:16 +0000
Subject: 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
---
 common/Determinism.v | 257 +++++++++++++++++++++++++++++++--------------------
 1 file changed, 155 insertions(+), 102 deletions(-)

(limited to 'common/Determinism.v')

diff --git a/common/Determinism.v b/common/Determinism.v
index 00d88559..16e88902 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.
-- 
cgit