From 93b89122000e42ac57abc39734fdf05d3a89e83c Mon Sep 17 00:00:00 2001 From: xleroy 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/Behaviors.v | 700 ++++++++++++++++++++++++ common/Determinism.v | 257 +++++---- common/Events.v | 363 +++++++++---- common/Smallstep.v | 1451 ++++++++++++++++++++++++++++++++++---------------- 4 files changed, 2111 insertions(+), 660 deletions(-) create mode 100644 common/Behaviors.v (limited to 'common') 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 +}. -- cgit v1.2.3