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/Smallstep.v | 1451 +++++++++++++++++++++++++++++++++++----------------- 1 file changed, 994 insertions(+), 457 deletions(-) (limited to 'common/Smallstep.v') 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