diff options
42 files changed, 3307 insertions, 1848 deletions
@@ -19,7 +19,7 @@ common/Memtype.vo common/Memtype.glob: common/Memtype.v lib/Coqlib.vo common/AST common/Memory.vo common/Memory.glob: common/Memory.v lib/Axioms.vo lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memdata.vo common/Memtype.vo common/Values.vo common/Values.glob: common/Values.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Smallstep.vo common/Smallstep.glob: common/Smallstep.v lib/Coqlib.vo common/AST.vo common/Events.vo common/Globalenvs.vo lib/Integers.vo -common/Determinism.vo common/Determinism.glob: common/Determinism.v lib/Coqlib.vo common/AST.vo lib/Integers.vo common/Values.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo +common/Behaviors.vo common/Behaviors.glob: common/Behaviors.v lib/Coqlib.vo common/AST.vo common/Events.vo common/Globalenvs.vo lib/Integers.vo common/Smallstep.vo common/Switch.vo common/Switch.glob: common/Switch.v lib/Coqlib.vo lib/Integers.vo lib/Ordered.vo backend/Cminor.vo backend/Cminor.glob: backend/Cminor.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Events.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Smallstep.vo common/Switch.vo $(ARCH)/Op.vo $(ARCH)/Op.glob: $(ARCH)/Op.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memdata.vo common/Memory.vo common/Globalenvs.vo common/Events.vo @@ -89,12 +89,12 @@ $(ARCH)/Asmgenproof1.vo $(ARCH)/Asmgenproof1.glob: $(ARCH)/Asmgenproof1.v lib/Co $(ARCH)/Asmgenproof.vo $(ARCH)/Asmgenproof.glob: $(ARCH)/Asmgenproof.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo backend/Machsem.vo backend/Machtyping.vo backend/Conventions.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo $(ARCH)/Asmgenretaddr.vo $(ARCH)/Asmgenproof1.vo cfrontend/Csyntax.vo cfrontend/Csyntax.glob: cfrontend/Csyntax.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo cfrontend/Csem.vo cfrontend/Csem.glob: cfrontend/Csem.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Events.vo common/Globalenvs.vo cfrontend/Csyntax.vo common/Smallstep.vo -cfrontend/Cstrategy.vo cfrontend/Cstrategy.glob: cfrontend/Cstrategy.v lib/Axioms.vo lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo common/Determinism.vo cfrontend/Csyntax.vo cfrontend/Csem.vo +cfrontend/Cstrategy.vo cfrontend/Cstrategy.glob: cfrontend/Cstrategy.v lib/Axioms.vo lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Initializers.vo cfrontend/Initializers.glob: cfrontend/Initializers.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Initializersproof.vo cfrontend/Initializersproof.glob: cfrontend/Initializersproof.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Globalenvs.vo common/Events.vo common/Smallstep.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Initializers.vo cfrontend/SimplExpr.vo cfrontend/SimplExpr.glob: cfrontend/SimplExpr.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo cfrontend/Csyntax.vo cfrontend/Clight.vo cfrontend/SimplExprspec.vo cfrontend/SimplExprspec.glob: cfrontend/SimplExprspec.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/AST.vo cfrontend/Csyntax.vo cfrontend/Clight.vo cfrontend/SimplExpr.vo -cfrontend/SimplExprproof.vo cfrontend/SimplExprproof.glob: cfrontend/SimplExprproof.v lib/Axioms.vo lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Errors.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Smallstep.vo common/Globalenvs.vo common/Determinism.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo cfrontend/Clight.vo cfrontend/SimplExpr.vo cfrontend/SimplExprspec.vo +cfrontend/SimplExprproof.vo cfrontend/SimplExprproof.glob: cfrontend/SimplExprproof.v lib/Axioms.vo lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Errors.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Smallstep.vo common/Globalenvs.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo cfrontend/Clight.vo cfrontend/SimplExpr.vo cfrontend/SimplExprspec.vo cfrontend/Clight.vo cfrontend/Clight.glob: cfrontend/Clight.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cshmgen.vo cfrontend/Cshmgen.glob: cfrontend/Cshmgen.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/AST.vo cfrontend/Csyntax.vo cfrontend/Clight.vo backend/Cminor.vo cfrontend/Csharpminor.vo cfrontend/Cshmgenproof.vo cfrontend/Cshmgenproof.glob: cfrontend/Cshmgenproof.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/AST.vo common/Values.vo common/Events.vo common/Memory.vo common/Globalenvs.vo common/Smallstep.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Clight.vo backend/Cminor.vo cfrontend/Csharpminor.vo cfrontend/Cshmgen.vo @@ -102,4 +102,4 @@ cfrontend/Csharpminor.vo cfrontend/Csharpminor.glob: cfrontend/Csharpminor.v lib cfrontend/Cminorgen.vo cfrontend/Cminorgen.glob: cfrontend/Cminorgen.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Ordered.vo common/AST.vo lib/Integers.vo common/Memdata.vo cfrontend/Csharpminor.vo backend/Cminor.vo cfrontend/Cminorgenproof.vo cfrontend/Cminorgenproof.glob: cfrontend/Cminorgenproof.v lib/Coqlib.vo lib/Intv.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memdata.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo common/Switch.vo cfrontend/Csharpminor.vo backend/Cminor.vo cfrontend/Cminorgen.vo driver/Compiler.vo driver/Compiler.glob: driver/Compiler.v lib/Axioms.vo lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo common/Values.vo common/Smallstep.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo cfrontend/Clight.vo cfrontend/Csharpminor.vo backend/Cminor.vo backend/CminorSel.vo backend/RTL.vo backend/LTL.vo backend/LTLin.vo backend/Linear.vo backend/Mach.vo backend/Machsem.vo $(ARCH)/Asm.vo cfrontend/Initializers.vo cfrontend/SimplExpr.vo cfrontend/Cshmgen.vo cfrontend/Cminorgen.vo backend/Selection.vo backend/RTLgen.vo backend/Tailcall.vo backend/CastOptim.vo backend/Constprop.vo backend/CSE.vo backend/Allocation.vo backend/Tunneling.vo backend/Linearize.vo backend/CleanupLabels.vo backend/Reload.vo backend/Stacking.vo $(ARCH)/Asmgen.vo backend/RTLtyping.vo backend/LTLtyping.vo backend/LTLintyping.vo backend/Lineartyping.vo backend/Machtyping.vo cfrontend/SimplExprproof.vo cfrontend/Cshmgenproof.vo cfrontend/Cminorgenproof.vo backend/Selectionproof.vo backend/RTLgenproof.vo backend/Tailcallproof.vo backend/CastOptimproof.vo backend/Constpropproof.vo backend/CSEproof.vo backend/Allocproof.vo backend/Alloctyping.vo backend/Tunnelingproof.vo backend/Tunnelingtyping.vo backend/Linearizeproof.vo backend/Linearizetyping.vo backend/CleanupLabelsproof.vo backend/CleanupLabelstyping.vo backend/Reloadproof.vo backend/Reloadtyping.vo backend/Stackingproof.vo backend/Stackingtyping.vo $(ARCH)/Asmgenproof.vo -driver/Complements.vo driver/Complements.glob: driver/Complements.v lib/Coqlib.vo common/AST.vo lib/Integers.vo common/Values.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo common/Determinism.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo $(ARCH)/Asm.vo driver/Compiler.vo common/Errors.vo +driver/Complements.vo driver/Complements.glob: driver/Complements.v lib/Coqlib.vo common/AST.vo lib/Integers.vo common/Values.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo common/Behaviors.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo cfrontend/Clight.vo backend/Cminor.vo backend/RTL.vo $(ARCH)/Asm.vo driver/Compiler.vo common/Errors.vo @@ -1,3 +1,11 @@ +- Revised and strengthened the top-level statements of semantic preservation. + In particular, we now show: + . backward simulation for the whole compiler without assuming + a deterministic external world; + . if the source program goes wrong after performing some I/O, + the compiled code performs at least these I/O before continuing + with an arbitrary behavior. + - Revised handling of annotation statements. Now they come in two forms: 1. __builtin_annot("format", x1, ..., xN) (arbitrarily many arguments; no code generated, even if some @@ -39,7 +39,8 @@ LIB=Axioms.v Coqlib.v Intv.v Maps.v Heaps.v Lattice.v Ordered.v \ # Parts common to the front-ends and the back-end (in common/) COMMON=Errors.v AST.v Events.v Globalenvs.v Memdata.v Memtype.v Memory.v Values.v \ - Smallstep.v Determinism.v Switch.v + Smallstep.v Behaviors.v Switch.v +# Determinism.v # Back-end modules (in backend/, $(ARCH)/, $(ARCH)/$(VARIANT)) @@ -670,5 +670,69 @@ Inductive final_state: state -> int -> Prop := rs#IR0 = Vint r -> final_state (State rs m) r. -Definition exec_program (p: program) (beh: program_behavior) : Prop := - program_behaves step (initial_state p) final_state (Genv.globalenv p) beh. +Definition semantics (p: program) := + Semantics step (initial_state p) final_state (Genv.globalenv p). + +(** Determinacy of the [Asm] semantics. *) + +Remark extcall_arguments_determ: + forall rs m sg args1 args2, + extcall_arguments rs m sg args1 -> extcall_arguments rs m sg args2 -> args1 = args2. +Proof. + intros until m. + assert (forall ll vl1, list_forall2 (extcall_arg rs m) ll vl1 -> + forall vl2, list_forall2 (extcall_arg rs m) ll vl2 -> vl1 = vl2). + induction 1; intros vl2 EA; inv EA. + auto. + f_equal; auto. + inv H; inv H3; congruence. + intros. red in H0; red in H1. eauto. +Qed. + +Remark annot_arguments_determ: + forall rs m params args1 args2, + annot_arguments rs m params args1 -> annot_arguments rs m params args2 -> args1 = args2. +Proof. + unfold annot_arguments. intros. revert params args1 H args2 H0. + induction 1; intros. + inv H0; auto. + inv H1. decEq; eauto. inv H; inv H4. auto. congruence. +Qed. + +Lemma semantics_determinate: forall p, determinate (semantics p). +Proof. +Ltac Equalities := + match goal with + | [ H1: ?a = ?b, H2: ?a = ?c |- _ ] => + rewrite H1 in H2; inv H2; Equalities + | _ => idtac + end. + intros; constructor; simpl; intros. +(* determ *) + inv H; inv H0; Equalities. + split. constructor. auto. + discriminate. + discriminate. + inv H11. + exploit external_call_determ. eexact H4. eexact H11. intros [A B]. + split. auto. intros. destruct B; auto. subst. auto. + inv H12. + assert (vargs0 = vargs) by (eapply annot_arguments_determ; eauto). subst vargs0. + exploit external_call_determ. eexact H5. eexact H13. intros [A B]. + split. auto. intros. destruct B; auto. subst. auto. + assert (args0 = args) by (eapply extcall_arguments_determ; eauto). subst args0. + exploit external_call_determ. eexact H3. eexact H8. intros [A B]. + split. auto. intros. destruct B; auto. subst. auto. +(* trace length *) + inv H; simpl. + omega. + eapply external_call_trace_length; eauto. + eapply external_call_trace_length; eauto. + eapply external_call_trace_length; eauto. +(* initial states *) + inv H; inv H0. f_equal. congruence. +(* final no step *) + inv H. unfold Vzero in H0. red; intros; red; intros. inv H; congruence. +(* final states *) + inv H; inv H0. congruence. +Qed. diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v index 82e54c8..0e2bdca 100644 --- a/arm/Asmgenproof.v +++ b/arm/Asmgenproof.v @@ -1404,11 +1404,10 @@ Proof. Qed. Theorem transf_program_correct: - forall (beh: program_behavior), not_wrong beh -> - Machsem.exec_program prog beh -> Asm.exec_program tprog beh. + forward_simulation (Machsem.semantics prog) (Asm.semantics tprog). Proof. - unfold Machsem.exec_program, Asm.exec_program; intros. - eapply simulation_star_preservation with (measure := measure); eauto. + eapply forward_simulation_star with (measure := measure). + eexact symbols_preserved. eexact transf_initial_states. eexact transf_final_states. exact transf_instr_correct. diff --git a/backend/Allocproof.v b/backend/Allocproof.v index e7d9995..ae86ee8 100644 --- a/backend/Allocproof.v +++ b/backend/Allocproof.v @@ -797,11 +797,10 @@ Proof. Qed. Theorem transf_program_correct: - forall (beh: program_behavior), not_wrong beh -> - RTL.exec_program prog beh -> LTL.exec_program tprog beh. + forward_simulation (RTL.semantics prog) (LTL.semantics tprog). Proof. - unfold RTL.exec_program, LTL.exec_program; intros. - eapply simulation_step_preservation; eauto. + eapply forward_simulation_step. + eexact symbols_preserved. eexact transf_initial_states. eexact transf_final_states. exact transl_step_correct. diff --git a/backend/CSEproof.v b/backend/CSEproof.v index 53576ad..77da538 100644 --- a/backend/CSEproof.v +++ b/backend/CSEproof.v @@ -968,11 +968,10 @@ Proof. Qed. Theorem transf_program_correct: - forall (beh: program_behavior), not_wrong beh -> - exec_program prog beh -> exec_program tprog beh. + forward_simulation (RTL.semantics prog) (RTL.semantics tprog). Proof. - unfold exec_program; intros. - eapply simulation_step_preservation; eauto. + eapply forward_simulation_step. + eexact symbols_preserved. eexact transf_initial_states. eexact transf_final_states. exact transf_step_correct. diff --git a/backend/CastOptimproof.v b/backend/CastOptimproof.v index ab04d0e..0afc208 100644 --- a/backend/CastOptimproof.v +++ b/backend/CastOptimproof.v @@ -560,15 +560,13 @@ Proof. Qed. (** The preservation of the observable behavior of the program then - follows, using the generic preservation theorem - [Smallstep.simulation_step_preservation]. *) + follows. *) Theorem transf_program_correct: - forall (beh: program_behavior), not_wrong beh -> - exec_program prog beh -> exec_program tprog beh. + forward_simulation (RTL.semantics prog) (RTL.semantics tprog). Proof. - unfold exec_program; intros. - eapply simulation_step_preservation; eauto. + eapply forward_simulation_step. + eexact symbols_preserved. eexact transf_initial_states. eexact transf_final_states. exact transf_step_correct. diff --git a/backend/CleanupLabelsproof.v b/backend/CleanupLabelsproof.v index abd2581..a7a60f6 100644 --- a/backend/CleanupLabelsproof.v +++ b/backend/CleanupLabelsproof.v @@ -324,11 +324,10 @@ Proof. Qed. Theorem transf_program_correct: - forall (beh: program_behavior), not_wrong beh -> - exec_program prog beh -> LTLin.exec_program tprog beh. + forward_simulation (LTLin.semantics prog) (LTLin.semantics tprog). Proof. - unfold exec_program; intros. - eapply simulation_opt_preservation; eauto. + eapply forward_simulation_opt. + eexact symbols_preserved. eexact transf_initial_states. eexact transf_final_states. eexact transf_step_correct. diff --git a/backend/Cminor.v b/backend/Cminor.v index 45e060d..45efdf9 100644 --- a/backend/Cminor.v +++ b/backend/Cminor.v @@ -529,13 +529,26 @@ Inductive final_state: state -> int -> Prop := | final_state_intro: forall r m, final_state (Returnstate (Vint r) Kstop m) r. -(** Execution of a whole program: [exec_program p beh] - holds if the application of [p]'s main function to no arguments - in the initial memory state for [p] has [beh] as observable - behavior. *) +(** The corresponding small-step semantics. *) -Definition exec_program (p: program) (beh: program_behavior) : Prop := - program_behaves step (initial_state p) final_state (Genv.globalenv p) beh. +Definition semantics (p: program) := + Semantics step (initial_state p) final_state (Genv.globalenv p). + +(** This semantics is receptive to changes in events. *) + +Lemma semantics_receptive: + forall (p: program), receptive (semantics p). +Proof. + intros. constructor; simpl; intros. +(* receptiveness *) + assert (t1 = E0 -> exists s2, step (Genv.globalenv p) s t2 s2). + intros. subst. inv H0. exists s1; auto. + inversion H; subst; auto. + exploit external_call_receptive; eauto. intros [vres2 [m2 EC2]]. + exists (Returnstate vres2 k m2). econstructor; eauto. +(* trace length *) + inv H; simpl; try omega. eapply external_call_trace_length; eauto. +Qed. (** * Alternate operational semantics (big-step) *) @@ -697,17 +710,6 @@ Scheme eval_funcall_ind2 := Minimality for eval_funcall Sort Prop Combined Scheme eval_funcall_exec_stmt_ind2 from eval_funcall_ind2, exec_stmt_ind2. -(* -Definition eval_funcall_exec_stmt_ind2 - (P1: mem -> fundef -> list val -> trace -> mem -> val -> Prop) - (P2: val -> env -> mem -> stmt -> trace -> - env -> mem -> outcome -> Prop) := - fun a b c d e f g h i j k l m n o p q => - conj - (eval_funcall_ind2 ge P1 P2 a b c d e f g h i j k l m n o p q) - (exec_stmt_ind2 ge P1 P2 a b c d e f g h i j k l m n o p q). -*) - (** Coinductive semantics for divergence. [evalinf_funcall ge m f args t] means that the function [f] diverges when applied to the arguments [args] in @@ -804,6 +806,9 @@ Inductive bigstep_program_diverges (p: program): traceinf -> Prop := evalinf_funcall ge m0 f nil t -> bigstep_program_diverges p t. +Definition bigstep_semantics (p: program) := + Bigstep_semantics (bigstep_program_terminates p) (bigstep_program_diverges p). + (** ** Correctness of the big-step semantics with respect to the transition semantics *) Section BIGSTEP_TO_TRANSITION. @@ -1102,32 +1107,20 @@ Proof. traceEq. Qed. -Theorem bigstep_program_terminates_exec: - forall t r, bigstep_program_terminates prog t r -> exec_program prog (Terminates t r). +Theorem bigstep_semantics_sound: + bigstep_sound (bigstep_semantics prog) (semantics prog). Proof. - intros. inv H. - econstructor. - econstructor; eauto. - apply eval_funcall_steps. eauto. red; auto. + constructor; intros. +(* termination *) + inv H. econstructor; econstructor. + split. econstructor; eauto. + split. apply eval_funcall_steps. eauto. red; auto. econstructor. -Qed. - -Theorem bigstep_program_diverges_exec: - forall T, bigstep_program_diverges prog T -> - exec_program prog (Reacts T) \/ - exists t, exec_program prog (Diverges t) /\ traceinf_prefix t T. -Proof. - intros. inv H. - set (st := Callstate f nil Kstop m0). - assert (forever step ge0 st T). - eapply forever_plus_forever. - eapply evalinf_funcall_forever; eauto. - destruct (forever_silent_or_reactive _ _ _ _ _ _ H) - as [A | [t [s' [T' [B [C D]]]]]]. - left. econstructor. econstructor; eauto. auto. - right. exists t. split. - econstructor. econstructor; eauto. eauto. auto. - subst T. rewrite <- (E0_right t) at 1. apply traceinf_prefix_app. constructor. +(* divergence *) + inv H. econstructor. + split. econstructor; eauto. + eapply forever_plus_forever. + eapply evalinf_funcall_forever; eauto. Qed. End BIGSTEP_TO_TRANSITION. diff --git a/backend/CminorSel.v b/backend/CminorSel.v index 8a82c42..84b47f3 100644 --- a/backend/CminorSel.v +++ b/backend/CminorSel.v @@ -384,8 +384,8 @@ Inductive final_state: state -> int -> Prop := | final_state_intro: forall r m, final_state (Returnstate (Vint r) Kstop m) r. -Definition exec_program (p: program) (beh: program_behavior) : Prop := - program_behaves step (initial_state p) final_state (Genv.globalenv p) beh. +Definition semantics (p: program) := + Semantics step (initial_state p) final_state (Genv.globalenv p). Hint Constructors eval_expr eval_condexpr eval_exprlist: evalexpr. diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v index d534c75..058d68e 100644 --- a/backend/Constpropproof.v +++ b/backend/Constpropproof.v @@ -468,15 +468,13 @@ Proof. Qed. (** The preservation of the observable behavior of the program then - follows, using the generic preservation theorem - [Smallstep.simulation_step_preservation]. *) + follows. *) Theorem transf_program_correct: - forall (beh: program_behavior), not_wrong beh -> - exec_program prog beh -> exec_program tprog beh. + forward_simulation (RTL.semantics prog) (RTL.semantics tprog). Proof. - unfold exec_program; intros. - eapply simulation_step_preservation; eauto. + eapply forward_simulation_step. + eexact symbols_preserved. eexact transf_initial_states. eexact transf_final_states. exact transf_step_correct. diff --git a/backend/LTL.v b/backend/LTL.v index 6e3effd..5ed0a8f 100644 --- a/backend/LTL.v +++ b/backend/LTL.v @@ -267,8 +267,8 @@ Inductive final_state: state -> int -> Prop := | final_state_intro: forall n m, final_state (Returnstate nil (Vint n) m) n. -Definition exec_program (p: program) (beh: program_behavior) : Prop := - program_behaves step (initial_state p) final_state (Genv.globalenv p) beh. +Definition semantics (p: program) := + Semantics step (initial_state p) final_state (Genv.globalenv p). (** * Operations over LTL *) diff --git a/backend/LTLin.v b/backend/LTLin.v index 5f12390..390c4cf 100644 --- a/backend/LTLin.v +++ b/backend/LTLin.v @@ -254,8 +254,8 @@ Inductive final_state: state -> int -> Prop := | final_state_intro: forall n m, final_state (Returnstate nil (Vint n) m) n. -Definition exec_program (p: program) (beh: program_behavior) : Prop := - program_behaves step (initial_state p) final_state (Genv.globalenv p) beh. +Definition semantics (p: program) := + Semantics step (initial_state p) final_state (Genv.globalenv p). (** * Properties of the operational semantics *) diff --git a/backend/Linear.v b/backend/Linear.v index 23f0324..3553ced 100644 --- a/backend/Linear.v +++ b/backend/Linear.v @@ -367,5 +367,5 @@ Inductive final_state: state -> int -> Prop := rs (R (loc_result (mksignature nil (Some Tint)))) = Vint r -> final_state (Returnstate nil rs m) r. -Definition exec_program (p: program) (beh: program_behavior) : Prop := - program_behaves step (initial_state p) final_state (Genv.globalenv p) beh. +Definition semantics (p: program) := + Semantics step (initial_state p) final_state (Genv.globalenv p). diff --git a/backend/Linearizeproof.v b/backend/Linearizeproof.v index abc497e..2f96a09 100644 --- a/backend/Linearizeproof.v +++ b/backend/Linearizeproof.v @@ -743,11 +743,10 @@ Proof. Qed. Theorem transf_program_correct: - forall (beh: program_behavior), not_wrong beh -> - LTL.exec_program prog beh -> LTLin.exec_program tprog beh. + forward_simulation (LTL.semantics prog) (LTLin.semantics tprog). Proof. - unfold LTL.exec_program, exec_program; intros. - eapply simulation_plus_preservation; eauto. + eapply forward_simulation_plus. + eexact symbols_preserved. eexact transf_initial_states. eexact transf_final_states. eexact transf_step_correct. diff --git a/backend/Machsem.v b/backend/Machsem.v index fe0ec37..853e8a7 100644 --- a/backend/Machsem.v +++ b/backend/Machsem.v @@ -272,5 +272,5 @@ Inductive final_state: state -> int -> Prop := rs (loc_result (mksignature nil (Some Tint))) = Vint r -> final_state (Returnstate nil rs m) r. -Definition exec_program (p: program) (beh: program_behavior) : Prop := - program_behaves step (initial_state p) final_state (Genv.globalenv p) beh. +Definition semantics (p: program) := + Semantics step (initial_state p) final_state (Genv.globalenv p). diff --git a/backend/RTL.v b/backend/RTL.v index 2cb2719..10d4a3f 100644 --- a/backend/RTL.v +++ b/backend/RTL.v @@ -345,8 +345,30 @@ Inductive final_state: state -> int -> Prop := | final_state_intro: forall r m, final_state (Returnstate nil (Vint r) m) r. -Definition exec_program (p: program) (beh: program_behavior) : Prop := - program_behaves step (initial_state p) final_state (Genv.globalenv p) beh. +(** The small-step semantics for a program. *) + +Definition semantics (p: program) := + Semantics step (initial_state p) final_state (Genv.globalenv p). + +(** This semantics is receptive to changes in events. *) + +Lemma semantics_receptive: + forall (p: program), receptive (semantics p). +Proof. + intros. constructor; simpl; intros. +(* receptiveness *) + assert (t1 = E0 -> exists s2, step (Genv.globalenv p) s t2 s2). + intros. subst. inv H0. exists s1; auto. + inversion H; subst; auto. + exploit external_call_receptive; eauto. intros [vres2 [m2 EC2]]. + exists (State s0 f sp pc' (rs#res <- vres2) m2). eapply exec_Ibuiltin; eauto. + exploit external_call_receptive; eauto. intros [vres2 [m2 EC2]]. + exists (Returnstate s0 vres2 m2). econstructor; eauto. +(* trace length *) + inv H; simpl; try omega. + eapply external_call_trace_length; eauto. + eapply external_call_trace_length; eauto. +Qed. (** * Operations on RTL abstract syntax *) diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v index e72b000..55cdd6b 100644 --- a/backend/RTLgenproof.v +++ b/backend/RTLgenproof.v @@ -906,21 +906,12 @@ Fixpoint size_cont (k: cont) : nat := Definition measure_state (S: CminorSel.state) := match S with - | CminorSel.State _ s k _ _ _ => - existS (fun (x: nat) => nat) - (size_stmt s + size_cont k) - (size_stmt s) - | _ => - existS (fun (x: nat) => nat) 0 0 + | CminorSel.State _ s k _ _ _ => (size_stmt s + size_cont k, size_stmt s) + | _ => (0, 0) end. -Require Import Relations. -Require Import Wellfounded. - Definition lt_state (S1 S2: CminorSel.state) := - lexprod nat (fun (x: nat) => nat) - lt (fun (x: nat) => lt) - (measure_state S1) (measure_state S2). + lex_ord lt lt (measure_state S1) (measure_state S2). Lemma lt_state_intro: forall f1 s1 k1 sp1 e1 m1 f2 s2 k2 sp2 e2 m2, @@ -931,20 +922,20 @@ Lemma lt_state_intro: (CminorSel.State f2 s2 k2 sp2 e2 m2). Proof. intros. unfold lt_state. simpl. destruct H as [A | [A B]]. - apply left_lex. auto. - rewrite A. apply right_lex. auto. + left. auto. + rewrite A. right. auto. Qed. Ltac Lt_state := apply lt_state_intro; simpl; try omega. -Require Import Wf_nat. +Require Import Wellfounded. Lemma lt_state_wf: well_founded lt_state. Proof. unfold lt_state. apply wf_inverse_image with (f := measure_state). - apply wf_lexprod. apply lt_wf. intros. apply lt_wf. + apply wf_lex_ord. apply lt_wf. apply lt_wf. Qed. (** ** Semantic preservation for the translation of statements *) @@ -1345,11 +1336,10 @@ Proof. Qed. Theorem transf_program_correct: - forall (beh: program_behavior), not_wrong beh -> - CminorSel.exec_program prog beh -> RTL.exec_program tprog beh. + forward_simulation (CminorSel.semantics prog) (RTL.semantics tprog). Proof. - unfold CminorSel.exec_program, RTL.exec_program; intros. - eapply simulation_star_wf_preservation with (order := lt_state); eauto. + eapply forward_simulation_star_wf with (order := lt_state). + eexact symbols_preserved. eexact transl_initial_states. eexact transl_final_states. apply lt_state_wf. diff --git a/backend/Reloadproof.v b/backend/Reloadproof.v index 49640a3..f0a0b97 100644 --- a/backend/Reloadproof.v +++ b/backend/Reloadproof.v @@ -1431,11 +1431,10 @@ Proof. Qed. Theorem transf_program_correct: - forall (beh: program_behavior), not_wrong beh -> - LTLin.exec_program prog beh -> Linear.exec_program tprog beh. + forward_simulation (LTLin.semantics prog) (Linear.semantics tprog). Proof. - unfold LTLin.exec_program, Linear.exec_program; intros. - eapply simulation_star_preservation; eauto. + eapply forward_simulation_star. + eexact symbols_preserved. eexact transf_initial_states. eexact transf_final_states. eexact transf_step_correct. diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index d475f26..d6c850a 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -565,11 +565,10 @@ Proof. Qed. Theorem transf_program_correct: - forall (beh: program_behavior), not_wrong beh -> - Cminor.exec_program prog beh -> CminorSel.exec_program tprog beh. + forward_simulation (Cminor.semantics prog) (CminorSel.semantics tprog). Proof. - unfold CminorSel.exec_program, Cminor.exec_program; intros. - eapply simulation_opt_preservation; eauto. + eapply forward_simulation_opt. + eexact symbols_preserved. eexact sel_initial_states. eexact sel_final_states. eexact sel_step_correct. diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index fbe8882..a2c8ecd 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -2701,11 +2701,10 @@ Proof. Qed. Theorem transf_program_correct: - forall (beh: program_behavior), not_wrong beh -> - Linear.exec_program prog beh -> Machsem.exec_program tprog beh. + forward_simulation (Linear.semantics prog) (Machsem.semantics tprog). Proof. - unfold Linear.exec_program, Machsem.exec_program; intros. - eapply simulation_plus_preservation; eauto. + eapply forward_simulation_plus. + eexact symbols_preserved. eexact transf_initial_states. eexact transf_final_states. eexact transf_step_correct. diff --git a/backend/Tailcallproof.v b/backend/Tailcallproof.v index ca8e915..f3dd9ed 100644 --- a/backend/Tailcallproof.v +++ b/backend/Tailcallproof.v @@ -616,15 +616,13 @@ Qed. (** The preservation of the observable behavior of the program then - follows, using the generic preservation theorem - [Smallstep.simulation_opt_preservation]. *) + follows. *) Theorem transf_program_correct: - forall (beh: program_behavior), not_wrong beh -> - exec_program prog beh -> exec_program tprog beh. + forward_simulation (RTL.semantics prog) (RTL.semantics tprog). Proof. - unfold exec_program; intros. - eapply simulation_opt_preservation with (measure := measure); eauto. + eapply forward_simulation_opt with (measure := measure); eauto. + eexact symbols_preserved. eexact transf_initial_states. eexact transf_final_states. exact transf_step_correct. diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v index 9a14158..8ff7347 100644 --- a/backend/Tunnelingproof.v +++ b/backend/Tunnelingproof.v @@ -138,31 +138,31 @@ Qed. Section PRESERVATION. -Variable p: program. -Let tp := tunnel_program p. -Let ge := Genv.globalenv p. -Let tge := Genv.globalenv tp. +Variable prog: program. +Let tprog := tunnel_program prog. +Let ge := Genv.globalenv prog. +Let tge := Genv.globalenv tprog. Lemma functions_translated: forall v f, Genv.find_funct ge v = Some f -> Genv.find_funct tge v = Some (tunnel_fundef f). -Proof (@Genv.find_funct_transf _ _ _ tunnel_fundef p). +Proof (@Genv.find_funct_transf _ _ _ tunnel_fundef prog). Lemma function_ptr_translated: forall v f, Genv.find_funct_ptr ge v = Some f -> Genv.find_funct_ptr tge v = Some (tunnel_fundef f). -Proof (@Genv.find_funct_ptr_transf _ _ _ tunnel_fundef p). +Proof (@Genv.find_funct_ptr_transf _ _ _ tunnel_fundef prog). Lemma symbols_preserved: forall id, Genv.find_symbol tge id = Genv.find_symbol ge id. -Proof (@Genv.find_symbol_transf _ _ _ tunnel_fundef p). +Proof (@Genv.find_symbol_transf _ _ _ tunnel_fundef prog). Lemma varinfo_preserved: forall b, Genv.find_var_info tge b = Genv.find_var_info ge b. -Proof (@Genv.find_var_info_transf _ _ _ tunnel_fundef p). +Proof (@Genv.find_var_info_transf _ _ _ tunnel_fundef prog). Lemma sig_preserved: forall f, funsig (tunnel_fundef f) = funsig f. @@ -358,14 +358,14 @@ Proof. Qed. Lemma transf_initial_states: - forall st1, initial_state p st1 -> - exists st2, initial_state tp st2 /\ match_states st1 st2. + forall st1, initial_state prog st1 -> + exists st2, initial_state tprog st2 /\ match_states st1 st2. Proof. intros. inversion H. exists (Callstate nil (tunnel_fundef f) nil m0); split. econstructor; eauto. apply Genv.init_mem_transf; auto. - change (prog_main tp) with (prog_main p). + change (prog_main tprog) with (prog_main prog). rewrite symbols_preserved. eauto. apply function_ptr_translated; auto. rewrite <- H3. apply sig_preserved. @@ -380,11 +380,10 @@ Proof. Qed. Theorem transf_program_correct: - forall (beh: program_behavior), not_wrong beh -> - exec_program p beh -> exec_program tp beh. + forward_simulation (LTL.semantics prog) (LTL.semantics tprog). Proof. - unfold exec_program; intros. - eapply simulation_opt_preservation; eauto. + eapply forward_simulation_opt. + eexact symbols_preserved. eexact transf_initial_states. eexact transf_final_states. eexact tunnel_step_correct. diff --git a/cfrontend/Clight.v b/cfrontend/Clight.v index da8f668..a61d706 100644 --- a/cfrontend/Clight.v +++ b/cfrontend/Clight.v @@ -906,13 +906,26 @@ Inductive final_state: state -> int -> Prop := | final_state_intro: forall r m, final_state (Returnstate (Vint r) Kstop m) r. -(** Execution of a whole program: [exec_program p beh] - holds if the application of [p]'s main function to no arguments - in the initial memory state for [p] has [beh] as observable - behavior. *) +(** Wrapping up these definitions in a small-step semantics. *) -Definition exec_program (p: program) (beh: program_behavior) : Prop := - program_behaves step (initial_state p) final_state (Genv.globalenv p) beh. +Definition semantics (p: program) := + Semantics step (initial_state p) final_state (Genv.globalenv p). + +(** This semantics is receptive to changes in events. *) + +Lemma semantics_receptive: + forall (p: program), receptive (semantics p). +Proof. + intros. constructor; simpl; intros. +(* receptiveness *) + assert (t1 = E0 -> exists s2, step (Genv.globalenv p) s t2 s2). + intros. subst. inv H0. exists s1; auto. + inversion H; subst; auto. + exploit external_call_receptive; eauto. intros [vres2 [m2 EC2]]. + exists (Returnstate vres2 k m2). econstructor; eauto. +(* trace length *) + inv H; simpl; try omega. eapply external_call_trace_length; eauto. +Qed. (** Big-step execution of a whole program. *) @@ -936,6 +949,9 @@ Inductive bigstep_program_diverges (p: program): traceinf -> Prop := evalinf_funcall ge m0 f nil t -> bigstep_program_diverges p t. +Definition bigstep_semantics (p: program) := + Bigstep_semantics (bigstep_program_terminates p) (bigstep_program_diverges p). + (** * Implication from big-step semantics to transition semantics *) Section BIGSTEP_TO_TRANSITIONS. @@ -1352,33 +1368,21 @@ Proof. traceEq. Qed. -Theorem bigstep_program_terminates_exec: - forall t r, bigstep_program_terminates prog t r -> exec_program prog (Terminates t r). +Theorem bigstep_semantics_sound: + bigstep_sound (bigstep_semantics prog) (semantics prog). Proof. - intros. inv H. + constructor; simpl; intros. +(* termination *) + inv H. econstructor; econstructor. + split. econstructor; eauto. + split. eapply eval_funcall_steps. eauto. red; auto. econstructor. - econstructor. eauto. eauto. eauto. auto. - eapply eval_funcall_steps. eauto. red; auto. - econstructor. -Qed. - -Theorem bigstep_program_diverges_exec: - forall T, bigstep_program_diverges prog T -> - exec_program prog (Reacts T) \/ - exists t, exec_program prog (Diverges t) /\ traceinf_prefix t T. -Proof. - intros. inv H. - set (st := Callstate f nil Kstop m0). - assert (forever step ge0 st T). - eapply forever_N_forever with (order := order). - red; intros. constructor; intros. red in H. elim H. - eapply evalinf_funcall_forever; eauto. - destruct (forever_silent_or_reactive _ _ _ _ _ _ H) - as [A | [t [s' [T' [B [C D]]]]]]. - left. econstructor. econstructor; eauto. eauto. - right. exists t. split. - econstructor. econstructor; eauto. eauto. auto. - subst T. rewrite <- (E0_right t) at 1. apply traceinf_prefix_app. constructor. +(* divergence *) + inv H. econstructor. + split. econstructor; eauto. + eapply forever_N_forever with (order := order). + red; intros. constructor; intros. red in H. elim H. + eapply evalinf_funcall_forever; eauto. Qed. End BIGSTEP_TO_TRANSITIONS. diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v index ba51310..0590a60 100644 --- a/cfrontend/Cminorgenproof.v +++ b/cfrontend/Cminorgenproof.v @@ -3021,12 +3021,10 @@ Proof. Qed. Theorem transl_program_correct: - forall (beh: program_behavior), - not_wrong beh -> Csharpminor.exec_program prog beh -> - Cminor.exec_program tprog beh. + forward_simulation (Csharpminor.semantics prog) (Cminor.semantics tprog). Proof. - unfold Csharpminor.exec_program, Cminor.exec_program; intros. - eapply simulation_star_preservation; eauto. + eapply forward_simulation_star; eauto. + eexact symbols_preserved. eexact transl_initial_states. eexact transl_final_states. eexact transl_step_correct. diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v index 33d8e53..21dd57e 100644 --- a/cfrontend/Csem.v +++ b/cfrontend/Csem.v @@ -1183,11 +1183,8 @@ Inductive final_state: state -> int -> Prop := | final_state_intro: forall r m, final_state (Returnstate (Vint r) Kstop m) r. -(** Execution of a whole program: [exec_program p beh] - holds if the application of [p]'s main function to no arguments - in the initial memory state for [p] has [beh] as observable - behavior. *) +(** Wrapping up these definitions in a small-step semantics. *) -Definition exec_program (p: program) (beh: program_behavior) : Prop := - program_behaves step (initial_state p) final_state (Genv.globalenv p) beh. +Definition semantics (p: program) := + Semantics step (initial_state p) final_state (Genv.globalenv p). diff --git a/cfrontend/Csharpminor.v b/cfrontend/Csharpminor.v index d2eb3c1..c192e46 100644 --- a/cfrontend/Csharpminor.v +++ b/cfrontend/Csharpminor.v @@ -557,13 +557,7 @@ Inductive final_state: state -> int -> Prop := | final_state_intro: forall r m, final_state (Returnstate (Vint r) Kstop m) r. -(** Execution of a whole program: [exec_program p beh] - holds if the application of [p]'s main function to no arguments - in the initial memory state for [p] has [beh] as observable - behavior. *) - -Definition exec_program (p: program) (beh: program_behavior) : Prop := - program_behaves step (initial_state p) final_state - (Genv.globalenv p) beh. - +(** Wrapping up these definitions in a small-step semantics. *) +Definition semantics (p: program) := + Semantics step (initial_state p) final_state (Genv.globalenv p). diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v index 49d3ff3..28e6dad 100644 --- a/cfrontend/Cshmgenproof.v +++ b/cfrontend/Cshmgenproof.v @@ -1846,14 +1846,14 @@ Proof. Qed. Lemma transl_initial_states: - forall S t S', Clight.initial_state prog S -> Clight.step ge S t S' -> + forall S, Clight.initial_state prog S -> exists R, initial_state tprog R /\ match_states S R. Proof. intros. inv H. exploit function_ptr_translated; eauto. intros [tf [A B]]. assert (C: Genv.find_symbol tge (prog_main tprog) = Some b). rewrite symbols_preserved. replace (prog_main tprog) with (prog_main prog). - exact H2. symmetry. unfold transl_program in TRANSL. + auto. symmetry. unfold transl_program in TRANSL. eapply transform_partial_program2_main; eauto. assert (funsig tf = signature_of_type Tnil (Tint I32 Signed)). eapply transl_fundef_sig2; eauto. @@ -1870,46 +1870,13 @@ Proof. Qed. Theorem transl_program_correct: - forall (beh: program_behavior), - not_wrong beh -> Clight.exec_program prog beh -> - Csharpminor.exec_program tprog beh. -Proof. - set (order := fun (S1 S2: Clight.state) => False). - assert (WF: well_founded order). - unfold order; red. intros. constructor; intros. contradiction. - assert (transl_step': - forall S1 t S2, Clight.step ge S1 t S2 -> - forall T1, match_states S1 T1 -> - exists T2, - (plus step tge T1 t T2 \/ star step tge T1 t T2 /\ order S2 S1) - /\ match_states S2 T2). - intros. exploit transl_step; eauto. intros [T2 [A B]]. - exists T2; split. auto. auto. - intros. inv H0. -(* Terminates *) - assert (exists t1, exists s1, Clight.step (Genv.globalenv prog) s t1 s1). - inv H3. inv H2. inv H1. exists t1; exists s2; auto. - destruct H0 as [t1 [s1 ST]]. - exploit transl_initial_states; eauto. intros [R [A B]]. - exploit simulation_star_star; eauto. intros [R' [C D]]. - econstructor; eauto. eapply transl_final_states; eauto. -(* Diverges *) - assert (exists t1, exists s1, Clight.step (Genv.globalenv prog) s t1 s1). - inv H2. inv H3. exists E0; exists s2; auto. exists t1; exists s2; auto. - destruct H0 as [t1 [s1 ST]]. - exploit transl_initial_states; eauto. intros [R [A B]]. - exploit simulation_star_star; eauto. intros [R' [C D]]. - econstructor; eauto. eapply simulation_star_forever_silent; eauto. -(* Reacts *) - assert (exists t1, exists s1, Clight.step (Genv.globalenv prog) s t1 s1). - inv H2. inv H0. congruence. exists t1; exists s0; auto. - destruct H0 as [t1 [s1 ST]]. - exploit transl_initial_states; eauto. intros [R [A B]]. - exploit simulation_star_forever_reactive; eauto. - intro C. - econstructor; eauto. -(* Goes wrong *) - contradiction. contradiction. + forward_simulation (Clight.semantics prog) (Csharpminor.semantics tprog). +Proof. + eapply forward_simulation_plus. + eexact symbols_preserved. + eexact transl_initial_states. + eexact transl_final_states. + eexact transl_step. Qed. End CORRECTNESS. diff --git a/cfrontend/Cstrategy.v b/cfrontend/Cstrategy.v index 8dbf586..c0dd3a3 100644 --- a/cfrontend/Cstrategy.v +++ b/cfrontend/Cstrategy.v @@ -28,7 +28,6 @@ Require Import Memory. Require Import Events. Require Import Globalenvs. Require Import Smallstep. -Require Import Determinism. Require Import Csyntax. Require Import Csem. @@ -299,39 +298,59 @@ Inductive estep: state -> trace -> state -> Prop := Definition step (S: state) (t: trace) (S': state) : Prop := estep S t S' \/ sstep ge S t S'. -(** * Safe executions. *) +(** Properties of contexts *) -(** A C program is safe (in the nondeterministic strategy) - if it cannot get stuck. The definition is parameterized by - an external world (cf. file [Determinism]) to constrain the behavior - of external functions. *) +Lemma context_compose: + forall k2 k3 C2, context k2 k3 C2 -> + forall k1 C1, context k1 k2 C1 -> + context k1 k3 (fun x => C2(C1 x)) +with contextlist_compose: + forall k2 C2, contextlist k2 C2 -> + forall k1 C1, context k1 k2 C1 -> + contextlist k1 (fun x => C2(C1 x)). +Proof. + induction 1; intros; try (constructor; eauto). + replace (fun x => C1 x) with C1. auto. apply extensionality; auto. + induction 1; intros; constructor; eauto. +Qed. + +Hint Constructors context contextlist. +Hint Resolve context_compose contextlist_compose. + +(** * Safe executions. *) -Inductive immsafe: world -> state -> Prop := - | immsafe_final: forall w s r, - final_state s r -> - immsafe w s - | immsafe_step: forall w s t s' w', - Csem.step ge s t s' -> possible_trace w t w' -> - immsafe w s. +(** A state is safe according to the nondeterministic semantics + if it cannot get stuck by doing silent transitions only. *) -Definition safe (w: world) (s: Csem.state) : Prop := - forall t s' w', star Csem.step ge s t s' -> possible_trace w t w' -> immsafe w' s'. +Definition safe (s: Csem.state) : Prop := + forall s', star Csem.step ge s E0 s' -> + (exists r, final_state s' r) \/ (exists t, exists s'', Csem.step ge s' t s''). Lemma safe_steps: - forall w s t s' w', - safe w s -> star Csem.step ge s t s' -> possible_trace w t w' -> safe w' s'. + forall s s', + safe s -> star Csem.step ge s E0 s' -> safe s'. Proof. intros; red; intros. - eapply H. eapply star_trans; eauto. eapply possible_trace_app; eauto. + eapply H. eapply star_trans; eauto. +Qed. + +Lemma star_safe: + forall s1 s2 s3, + safe s1 -> star Csem.step ge s1 E0 s2 -> (safe s2 -> star Csem.step ge s2 E0 s3) -> + star Csem.step ge s1 E0 s3. +Proof. + intros. eapply star_trans; eauto. apply H1. eapply safe_steps; eauto. auto. Qed. -Lemma safe_imm: - forall w s, safe w s -> immsafe w s. +Lemma plus_safe: + forall s1 s2 s3, + safe s1 -> star Csem.step ge s1 E0 s2 -> (safe s2 -> plus Csem.step ge s2 E0 s3) -> + plus Csem.step ge s1 E0 s3. Proof. - intros. eapply H. apply star_refl. constructor. + intros. eapply star_plus_trans; eauto. apply H1. eapply safe_steps; eauto. auto. Qed. -Lemma not_stuck_val: +Remark not_stuck_val: forall e v ty m, not_stuck ge e (Eval v ty) m. Proof. @@ -339,18 +358,22 @@ Proof. Qed. Lemma safe_not_stuck: - forall w f a k e m, - safe w (ExprState f a k e m) -> + forall f a k e m, + safe (ExprState f a k e m) -> not_stuck ge e a m. Proof. - intros. exploit safe_imm; eauto; intro IS; inv IS. - inv H0. - inv H0. inv H2; auto; apply not_stuck_val. inv H2; apply not_stuck_val. + intros. exploit H. apply star_refl. intros [[r FIN] | [t [s' STEP]]]. + inv FIN. + inv STEP. + inv H0; auto; apply not_stuck_val. + inv H0; apply not_stuck_val. Qed. +Hint Resolve safe_not_stuck. + Lemma safe_not_imm_stuck: - forall k C w f a K e m, - safe w (ExprState f (C a) K e m) -> + forall k C f a K e m, + safe (ExprState f (C a) K e m) -> context k RV C -> not_imm_stuck ge e k a m. Proof. @@ -360,20 +383,6 @@ Qed. (** Simple, non-stuck expressions are well-formed with respect to l-values and r-values. *) -Lemma context_compose: - forall k2 k3 C2, context k2 k3 C2 -> - forall k1 C1, context k1 k2 C1 -> - context k1 k3 (fun x => C2(C1 x)) -with contextlist_compose: - forall k2 C2, contextlist k2 C2 -> - forall k1 C1, context k1 k2 C1 -> - contextlist k1 (fun x => C2(C1 x)). -Proof. - induction 1; intros; try (constructor; eauto). - replace (fun x => C1 x) with C1. auto. apply extensionality; auto. - induction 1; intros; constructor; eauto. -Qed. - Definition expr_kind (a: expr) : kind := match a with | Eloc _ _ _ => LV @@ -419,9 +428,9 @@ Proof. Qed. Lemma safe_expr_kind: - forall from C w f a k e m, + forall from C f a k e m, context from RV C -> - safe w (ExprState f (C a) k e m) -> + safe (ExprState f (C a) k e m) -> expr_kind a = from. Proof. intros. eapply not_imm_stuck_kind. eapply safe_not_imm_stuck; eauto. @@ -544,31 +553,28 @@ Lemma invert_expr_context: invert_expr_prop a m -> ~exprlist_all_values (C a)). Proof. - apply context_contextlist_ind; intros; try (exploit H0; [eauto|intros]). + apply context_contextlist_ind; intros; try (exploit H0; [eauto|intros]); simpl. auto. - simpl. destruct (C a); auto. contradiction. - simpl. destruct (C a); auto. contradiction. - simpl. destruct (C a); auto. contradiction. - simpl. auto. - simpl. destruct (C a); auto. contradiction. - simpl. destruct (C a); auto. contradiction. - simpl. - destruct e1; auto. destruct (C a); auto. contradiction. - simpl. destruct (C a); auto. contradiction. - simpl. destruct (C a); auto. contradiction. - simpl. destruct (C a); auto. contradiction. - simpl. - destruct e1; auto. destruct (C a); auto. contradiction. - simpl. destruct (C a); auto. contradiction. - simpl. - destruct e1; auto. destruct (C a); auto. contradiction. - simpl. destruct (C a); auto. contradiction. - simpl. destruct (C a); auto. contradiction. - simpl. destruct e1; auto. intros. elim (H0 a m); auto. - simpl. destruct (C a); auto. contradiction. - simpl. destruct (C a); auto. contradiction. - simpl. red; intros. destruct (C a); auto. - simpl; red; intros. destruct e1; auto. elim (H0 a m); auto. + destruct (C a); auto; contradiction. + destruct (C a); auto; contradiction. + destruct (C a); auto; contradiction. + destruct (C a); auto; contradiction. + destruct (C a); auto; contradiction. + destruct (C a); auto; contradiction. + destruct e1; auto; destruct (C a); auto; contradiction. + destruct (C a); auto; contradiction. + destruct (C a); auto; contradiction. + destruct (C a); auto; contradiction. + destruct e1; auto; destruct (C a); auto; contradiction. + destruct (C a); auto; contradiction. + destruct e1; auto; destruct (C a); auto; contradiction. + destruct (C a); auto; contradiction. + destruct (C a); auto; contradiction. + destruct e1; auto. intros. elim (H0 a m); auto. + destruct (C a); auto; contradiction. + destruct (C a); auto; contradiction. + red; intros. destruct (C a); auto. + red; intros. destruct e1; auto. elim (H0 a m); auto. Qed. Lemma not_imm_stuck_inv: @@ -595,6 +601,19 @@ Proof. red in H. destruct (C e0); auto; contradiction. Qed. +Lemma safe_inv: + forall k C f a K m, + safe (ExprState f (C a) K e m) -> + context k RV C -> + match a with + | Eloc _ _ _ => True + | Eval _ _ => True + | _ => invert_expr_prop a m + end. +Proof. + intros. eapply not_imm_stuck_inv; eauto. eapply safe_not_imm_stuck; eauto. +Qed. + End INVERSION_LEMMAS. (** * Correctness of the strategy. *) @@ -605,180 +624,170 @@ Variable f: function. Variable k: cont. Variable e: env. Variable m: mem. -Variable w: world. -Lemma simple_eval: +Lemma eval_simple_steps: + (forall a v, eval_simple_rvalue e m a v -> + forall C, context RV RV C -> safe (ExprState f (C a) k e m) -> + star Csem.step ge (ExprState f (C a) k e m) + E0 (ExprState f (C (Eval v (typeof a))) k e m)) +/\ (forall a b ofs, eval_simple_lvalue e m a b ofs -> + forall C, context LV RV C -> safe (ExprState f (C a) k e m) -> + star Csem.step ge (ExprState f (C a) k e m) + E0 (ExprState f (C (Eloc b ofs (typeof a))) k e m)). +Proof. + +Ltac Steps REC C' := eapply star_safe; eauto; [apply (REC C'); eauto | intros]. +Ltac FinishR := apply star_one; left; apply step_rred; eauto; simpl; try (econstructor; eauto; fail). +Ltac FinishL := apply star_one; left; apply step_lred; eauto; simpl; try (econstructor; eauto; fail). + + apply eval_simple_rvalue_lvalue_ind; intros. +(* val *) + apply star_refl. +(* valof *) + Steps H0 (fun x => C(Evalof x ty)). rewrite <- H1 in *. FinishR. +(* addrof *) + Steps H0 (fun x => C(Eaddrof x ty)). FinishR. +(* unop *) + Steps H0 (fun x => C(Eunop op x ty)). FinishR. +(* binop *) + Steps H0 (fun x => C(Ebinop op x r2 ty)). + Steps H2 (fun x => C(Ebinop op (Eval v1 (typeof r1)) x ty)). + FinishR. +(* cast *) + Steps H0 (fun x => C(Ecast x ty)). FinishR. +(* sizeof *) + FinishR. +(* loc *) + apply star_refl. +(* var local *) + FinishL. +(* var global *) + FinishL. apply red_var_global; auto. +(* deref *) + Steps H0 (fun x => C(Ederef x ty)). FinishL. +(* field struct *) + Steps H0 (fun x => C(Efield x f0 ty)). rewrite H1 in *. FinishL. +(* field union *) + Steps H0 (fun x => C(Efield x f0 ty)). rewrite H1 in *. FinishL. +Qed. + +Lemma eval_simple_rvalue_steps: + forall a v, eval_simple_rvalue e m a v -> + forall C, context RV RV C -> safe (ExprState f (C a) k e m) -> + star Csem.step ge (ExprState f (C a) k e m) + E0 (ExprState f (C (Eval v (typeof a))) k e m). +Proof (proj1 eval_simple_steps). + +Lemma eval_simple_lvalue_steps: + forall a b ofs, eval_simple_lvalue e m a b ofs -> + forall C, context LV RV C -> safe (ExprState f (C a) k e m) -> + star Csem.step ge (ExprState f (C a) k e m) + E0 (ExprState f (C (Eloc b ofs (typeof a))) k e m). +Proof (proj2 eval_simple_steps). + +Corollary eval_simple_rvalue_safe: + forall C a v, + eval_simple_rvalue e m a v -> + context RV RV C -> safe (ExprState f (C a) k e m) -> + safe (ExprState f (C (Eval v (typeof a))) k e m). +Proof. + intros. eapply safe_steps; eauto. eapply eval_simple_rvalue_steps; eauto. +Qed. + +Corollary eval_simple_lvalue_safe: + forall C a b ofs, + eval_simple_lvalue e m a b ofs -> + context LV RV C -> safe (ExprState f (C a) k e m) -> + safe (ExprState f (C (Eloc b ofs (typeof a))) k e m). +Proof. + intros. eapply safe_steps; eauto. eapply eval_simple_lvalue_steps; eauto. +Qed. + +Lemma simple_can_eval: forall a from C, - simple a -> context from RV C -> safe w (ExprState f (C a) k e m) -> + simple a -> context from RV C -> safe (ExprState f (C a) k e m) -> match from with - | LV => - exists b, exists ofs, - eval_simple_lvalue e m a b ofs - /\ star Csem.step ge (ExprState f (C a) k e m) - E0 (ExprState f (C (Eloc b ofs (typeof a))) k e m) - | RV => - exists v, - eval_simple_rvalue e m a v - /\ star Csem.step ge (ExprState f (C a) k e m) - E0 (ExprState f (C (Eval v (typeof a))) k e m) + | LV => exists b, exists ofs, eval_simple_lvalue e m a b ofs + | RV => exists v, eval_simple_rvalue e m a v end. Proof. +Ltac StepL REC C' a := + let b := fresh "b" in let ofs := fresh "ofs" in + let E := fresh "E" in let S := fresh "SAFE" in + exploit (REC LV C'); eauto; intros [b [ofs E]]; + assert (S: safe (ExprState f (C' (Eloc b ofs (typeof a))) k e m)) by + (eapply (eval_simple_lvalue_safe C'); eauto); + simpl in S. +Ltac StepR REC C' a := + let v := fresh "v" in let E := fresh "E" in let S := fresh "SAFE" in + exploit (REC RV C'); eauto; intros [v E]; + assert (S: safe (ExprState f (C' (Eval v (typeof a))) k e m)) by + (eapply (eval_simple_rvalue_safe C'); eauto); + simpl in S. + induction a; intros from C S CTX SAFE; - generalize (safe_expr_kind _ _ _ _ _ _ _ _ CTX SAFE); intro K; subst; + generalize (safe_expr_kind _ _ _ _ _ _ _ CTX SAFE); intro K; subst; simpl in S; try contradiction; simpl. (* val *) - exists v; split. constructor. apply star_refl. + exists v; constructor. (* var *) - exploit not_imm_stuck_inv. eapply safe_not_imm_stuck; eauto. - simpl. intros [b A]. - exists b; exists Int.zero; split. + exploit safe_inv; eauto; simpl. intros [b A]. + exists b; exists Int.zero. intuition. apply esl_var_local; auto. apply esl_var_global; auto. - apply star_one. left; apply step_lred. - intuition. apply red_var_local; auto. apply red_var_global; auto. - eapply safe_not_stuck; eauto. auto. (* field *) - set (C1 := fun x => Efield x f0 ty). - set (C2 := fun x => C(C1 x)). - exploit (IHa LV C2); auto. eapply context_compose; eauto. repeat constructor. - unfold C2, C1; intros [b [ofs [A B]]]. - exploit not_imm_stuck_inv. - eapply safe_not_imm_stuck. eapply safe_steps; eauto. constructor. eauto. - simpl. - case_eq (typeof a); intros; try contradiction. - destruct H0 as [delta EQ]. - exists b; econstructor; split. - eapply esl_field_struct; eauto. - eapply star_right. eauto. left; apply step_lred. - rewrite H. constructor; auto. - eapply safe_not_stuck. eapply safe_steps; eauto. constructor. auto. - traceEq. - exists b; exists ofs; split. - eapply esl_field_union; eauto. - eapply star_right. eauto. left; apply step_lred. - rewrite H. constructor; auto. - eapply safe_not_stuck. eapply safe_steps; eauto. constructor. auto. - traceEq. + StepL IHa (fun x => C(Efield x f0 ty)) a. + exploit safe_inv. eexact SAFE0. eauto. simpl. case_eq (typeof a); intros; try contradiction. + destruct H0 as [delta OFS]. exists b; exists (Int.add ofs (Int.repr delta)); econstructor; eauto. + exists b; exists ofs; econstructor; eauto. (* valof *) - set (C1 := fun x => Evalof x ty). - set (C2 := fun x => C(C1 x)). - exploit (IHa LV C2); auto. eapply context_compose; eauto. repeat constructor. - unfold C2, C1; intros [b [ofs [A B]]]. - exploit not_imm_stuck_inv. - eapply safe_not_imm_stuck. eapply safe_steps; eauto. constructor. eauto. - simpl. intros [D [v E]]. - exists v; split. - econstructor; eauto. - eapply star_right. eauto. left; apply step_rred. - simpl. rewrite D. constructor. auto. - eapply safe_not_stuck. eapply safe_steps; eauto. constructor. auto. - traceEq. + StepL IHa (fun x => C(Evalof x ty)) a. + exploit safe_inv. eexact SAFE0. eauto. simpl. intros [TY [v LOAD]]. + exists v; econstructor; eauto. (* deref *) - set (C1 := fun x => Ederef x ty). - set (C2 := fun x => C(C1 x)). - exploit (IHa RV C2); auto. eapply context_compose; eauto. repeat constructor. - unfold C2, C1; intros [v1 [A B]]. - exploit not_imm_stuck_inv. - eapply safe_not_imm_stuck. eapply safe_steps; eauto. constructor. eauto. - simpl. intros [b [ofs D]]. subst v1. - exists b; exists ofs; split. - econstructor; eauto. - eapply star_right. eauto. left; apply step_lred. - simpl. constructor. - eapply safe_not_stuck. eapply safe_steps; eauto. constructor. auto. - traceEq. + StepR IHa (fun x => C(Ederef x ty)) a. + exploit safe_inv. eexact SAFE0. eauto. simpl. intros [b [ofs EQ]]. + subst v. exists b; exists ofs; econstructor; eauto. (* addrof *) - set (C1 := fun x => Eaddrof x ty). - set (C2 := fun x => C(C1 x)). - exploit (IHa LV C2); auto. eapply context_compose; eauto. repeat constructor. - unfold C2, C1; intros [b [ofs [A B]]]. - exists (Vptr b ofs); split. - econstructor; eauto. - eapply star_right. eauto. left; apply step_rred. - simpl. constructor. - eapply safe_not_stuck. eapply safe_steps; eauto. constructor. auto. - traceEq. + StepL IHa (fun x => C(Eaddrof x ty)) a. + exists (Vptr b ofs); econstructor; eauto. (* unop *) - set (C1 := fun x => Eunop op x ty). - set (C2 := fun x => C(C1 x)). - exploit (IHa RV C2); auto. eapply context_compose; eauto. repeat constructor. - unfold C2, C1; intros [v1 [A B]]. - exploit not_imm_stuck_inv. - eapply safe_not_imm_stuck. eapply safe_steps; eauto. constructor. eauto. - simpl. intros [v E]. - exists v; split. - econstructor; eauto. - eapply star_right. eauto. left; apply step_rred. - simpl. constructor. auto. - eapply safe_not_stuck. eapply safe_steps; eauto. constructor. auto. - traceEq. + StepR IHa (fun x => C(Eunop op x ty)) a. + exploit safe_inv. eexact SAFE0. eauto. simpl. intros [v' EQ]. + exists v'; econstructor; eauto. (* binop *) - set (C1 := fun x => Ebinop op x a2 ty). - set (C2 := fun x => C(C1 x)). - exploit (IHa1 RV C2). tauto. eapply context_compose; eauto. repeat constructor. auto. - unfold C2, C1; intros [v1 [A B]]. - assert (safe w (ExprState f (C (Ebinop op (Eval v1 (typeof a1)) a2 ty)) k e m)). - eapply safe_steps; eauto. constructor. - set (C3 := fun x => Ebinop op (Eval v1 (typeof a1)) x ty). - set (C4 := fun x => C(C3 x)). - exploit (IHa2 RV C4). tauto. eapply context_compose; eauto. repeat constructor. auto. - unfold C4, C3; intros [v2 [D E]]. - assert (safe w (ExprState f (C (Ebinop op (Eval v1 (typeof a1)) (Eval v2 (typeof a2)) ty)) k e m)). - eapply safe_steps; eauto. constructor. - exploit not_imm_stuck_inv. - eapply safe_not_imm_stuck. eexact H0. eauto. - simpl. intros [v F]. - exists v; split. - econstructor; eauto. - eapply star_right. eapply star_trans; eauto. left; apply step_rred. - simpl. constructor. auto. - eapply safe_not_stuck. eauto. - auto. - traceEq. + destruct S. + StepR IHa1 (fun x => C(Ebinop op x a2 ty)) a1. + StepR IHa2 (fun x => C(Ebinop op (Eval v (typeof a1)) x ty)) a2. + exploit safe_inv. eexact SAFE1. eauto. simpl. intros [v' EQ]. + exists v'; econstructor; eauto. (* cast *) - set (C1 := fun x => Ecast x ty). - set (C2 := fun x => C(C1 x)). - exploit (IHa RV C2); auto. eapply context_compose; eauto. repeat constructor. - unfold C2, C1; intros [v1 [A B]]. - exploit not_imm_stuck_inv. - eapply safe_not_imm_stuck. eapply safe_steps; eauto. constructor. eauto. - simpl. intros [v E]. - exists v; split. - econstructor; eauto. - eapply star_right. eauto. left; apply step_rred. - simpl. constructor. auto. - eapply safe_not_stuck. eapply safe_steps; eauto. constructor. auto. - traceEq. + StepR IHa (fun x => C(Ecast x ty)) a. + exploit safe_inv. eexact SAFE0. eauto. simpl. intros [v' CAST]. + exists v'; econstructor; eauto. (* sizeof *) - econstructor; split. constructor. - apply star_one. left; apply step_rred. constructor. - eapply safe_not_stuck; eauto. - auto. + econstructor; econstructor. (* loc *) - exploit not_imm_stuck_inv. eapply safe_not_imm_stuck; eauto. - simpl. intros. - exists b; exists ofs; split. constructor. apply star_refl. + exists b; exists ofs; constructor. Qed. -Lemma simple_eval_r: - forall r C, - simple r -> context RV RV C -> safe w (ExprState f (C r) k e m) -> - exists v, - eval_simple_rvalue e m r v - /\ star Csem.step ge (ExprState f (C r) k e m) - E0 (ExprState f (C (Eval v (typeof r))) k e m). +Lemma simple_can_eval_rval: + forall r C, + simple r -> context RV RV C -> safe (ExprState f (C r) k e m) -> + exists v, eval_simple_rvalue e m r v + /\ safe (ExprState f (C (Eval v (typeof r))) k e m). Proof. - intros. apply (simple_eval r RV); auto. + intros. exploit (simple_can_eval r RV); eauto. intros [v A]. + exists v; split; auto. eapply eval_simple_rvalue_safe; eauto. Qed. -Lemma simple_eval_l: - forall l C, - simple l -> context LV RV C -> safe w (ExprState f (C l) k e m) -> - exists b, exists ofs, - eval_simple_lvalue e m l b ofs - /\ star Csem.step ge (ExprState f (C l) k e m) - E0 (ExprState f (C (Eloc b ofs (typeof l))) k e m). +Lemma simple_can_eval_lval: + forall l C, + simple l -> context LV RV C -> safe (ExprState f (C l) k e m) -> + exists b, exists ofs, eval_simple_lvalue e m l b ofs + /\ safe (ExprState f (C (Eloc b ofs (typeof l))) k e m). Proof. - intros. apply (simple_eval l LV); auto. + intros. exploit (simple_can_eval l LV); eauto. intros [b [ofs A]]. + exists b; exists ofs; split; auto. eapply eval_simple_lvalue_safe; eauto. Qed. Fixpoint rval_list (vl: list val) (rl: exprlist) : exprlist := @@ -795,6 +804,29 @@ Inductive eval_simple_list': exprlist -> list val -> Prop := eval_simple_list' rl vl -> eval_simple_list' (Econs r rl) (v :: vl). +Lemma eval_simple_list_implies: + forall rl tyl vl, + eval_simple_list e m rl tyl vl -> + exists vl', cast_arguments (rval_list vl' rl) tyl vl /\ eval_simple_list' rl vl'. +Proof. + induction 1. + exists (@nil val); split. constructor. constructor. + destruct IHeval_simple_list as [vl' [A B]]. + exists (v' :: vl'); split. constructor; auto. constructor; auto. +Qed. + +Lemma can_eval_simple_list: + forall rl vl, + eval_simple_list' rl vl -> + forall tyl vl', + cast_arguments (rval_list vl rl) tyl vl' -> + eval_simple_list e m rl tyl vl'. +Proof. + induction 1; simpl; intros. + inv H. constructor. + inv H1. econstructor; eauto. +Qed. + Fixpoint exprlist_app (rl1 rl2: exprlist) : exprlist := match rl1 with | Enil => rl2 @@ -847,29 +879,39 @@ Proof. apply extensionality; intros. f_equal. f_equal. apply exprlist_app_assoc. Qed. -Lemma simple_eval_rlist: +Hint Resolve contextlist'_head contextlist'_tail. + +Lemma eval_simple_list_steps: + forall rl vl, eval_simple_list' rl vl -> + forall C, contextlist' C -> safe (ExprState f (C rl) k e m) -> + star Csem.step ge (ExprState f (C rl) k e m) + E0 (ExprState f (C (rval_list vl rl)) k e m). +Proof. + induction 1; intros. +(* nil *) + apply star_refl. +(* cons *) + eapply star_safe. eauto. + eapply eval_simple_rvalue_steps with (C := fun x => C(Econs x rl)); eauto. + intros. apply IHeval_simple_list' with (C := fun x => C(Econs (Eval v (typeof r)) x)); auto. +Qed. + +Lemma simple_list_can_eval: forall rl C, simplelist rl -> contextlist' C -> - safe w (ExprState f (C rl) k e m) -> - exists vl, - eval_simple_list' rl vl - /\ star Csem.step ge (ExprState f (C rl) k e m) - E0 (ExprState f (C (rval_list vl rl)) k e m). + safe (ExprState f (C rl) k e m) -> + exists vl, eval_simple_list' rl vl. Proof. - induction rl; intros. - econstructor; split. constructor. simpl. apply star_refl. - simpl in H; destruct H. - set (C1 := fun x => C (Econs x rl)). - exploit (simple_eval_r r1 C1). auto. apply contextlist'_head. auto. auto. - unfold C1; intros [v [X Y]]. - assert (safe w (ExprState f (C (Econs (Eval v (typeof r1)) rl)) k e m)). - eapply safe_steps; eauto. constructor. - set (C2 := fun x => C (Econs (Eval v (typeof r1)) x)). - destruct (IHrl C2) as [vl [U V]]. auto. apply contextlist'_tail. auto. auto. - unfold C2 in V. - exists (v :: vl); split. constructor; auto. - simpl. eapply star_trans; eauto. + induction rl; intros. + econstructor; constructor. + simpl in H; destruct H. + exploit (simple_can_eval r1 RV (fun x => C(Econs x rl))); eauto. + intros [v1 EV1]. + exploit (IHrl (fun x => C(Econs (Eval v1 (typeof r1)) x))); eauto. + apply (eval_simple_rvalue_safe (fun x => C(Econs x rl))); eauto. + intros [vl EVl]. + exists (v1 :: vl); constructor; auto. Qed. Lemma rval_list_all_values: @@ -879,18 +921,6 @@ Proof. destruct rl; simpl; auto. Qed. -Lemma can_eval_simple_list: - forall rl vl, - eval_simple_list' rl vl -> - forall tyl vl', - cast_arguments (rval_list vl rl) tyl vl' -> - eval_simple_list e m rl tyl vl'. -Proof. - induction 1; simpl; intros. - inv H. constructor. - inv H1. econstructor; eauto. -Qed. - End SIMPLE_EVAL. (** Decomposition *) @@ -901,7 +931,6 @@ Variable f: function. Variable k: cont. Variable e: env. Variable m: mem. -Variable w: world. Definition simple_side_effect (r: expr) : Prop := match r with @@ -919,155 +948,76 @@ Scheme expr_ind2 := Induction for expr Sort Prop with exprlist_ind2 := Induction for exprlist Sort Prop. Combined Scheme expr_expr_list_ind from expr_ind2, exprlist_ind2. +Hint Constructors leftcontext leftcontextlist. + Lemma decompose_expr: (forall a from C, - context from RV C -> safe w (ExprState f (C a) k e m) -> + context from RV C -> safe (ExprState f (C a) k e m) -> simple a - \/ exists C', exists a', simple_side_effect a' /\ leftcontext RV from C' /\ a = C' a') + \/ exists C', exists a', a = C' a' /\ simple_side_effect a' /\ leftcontext RV from C') /\(forall rl C, - contextlist' C -> safe w (ExprState f (C rl) k e m) -> + contextlist' C -> safe (ExprState f (C rl) k e m) -> simplelist rl - \/ exists C', exists a', simple_side_effect a' /\ leftcontextlist RV C' /\ rl = C' a'). + \/ exists C', exists a', rl = C' a' /\ simple_side_effect a' /\ leftcontextlist RV C'). Proof. apply expr_expr_list_ind; intros; simpl; auto. + +Ltac Kind := + exploit safe_expr_kind; eauto; simpl; intros X; rewrite <- X in *; clear X. +Ltac Rec HR kind C C' := + destruct (HR kind (fun x => C(C' x))) as [? | [C'' [a' [D [A B]]]]]; + [eauto | eauto | auto | + right; exists (fun x => C'(C'' x)); exists a'; rewrite D; auto]. +Ltac Base := + right; exists (fun x => x); econstructor; split; [eauto | simpl; auto]. + (* field *) - exploit safe_expr_kind; eauto; simpl; intros. subst. - destruct (H LV (fun x => C (Efield x f0 ty))) as [A | [C' [a' [A [B D]]]]]. - eapply context_compose; eauto. repeat constructor. auto. - auto. - right; exists (fun x => Efield (C' x) f0 ty); exists a'. - split. auto. split. constructor; auto. rewrite D; auto. + Kind. Rec H LV C (fun x => Efield x f0 ty). (* rvalof *) - exploit safe_expr_kind; eauto; simpl; intros. subst. - destruct (H LV (fun x => C (Evalof x ty))) as [A | [C' [a' [A [B D]]]]]. - eapply context_compose; eauto. repeat constructor. auto. - auto. - right; exists (fun x => Evalof (C' x) ty); exists a'. - split. auto. split. constructor; auto. rewrite D; auto. + Kind. Rec H LV C (fun x => Evalof x ty). (* deref *) - exploit safe_expr_kind; eauto; simpl; intros. subst. - subst. destruct (H RV (fun x => C (Ederef x ty))) as [A | [C' [a' [A [B D]]]]]. - eapply context_compose; eauto. repeat constructor. auto. - auto. - right; exists (fun x => Ederef (C' x) ty); exists a'. - split. auto. split. constructor; auto. rewrite D; auto. + Kind. Rec H RV C (fun x => Ederef x ty). (* addrof *) - exploit safe_expr_kind; eauto; simpl; intros. subst. - destruct (H LV (fun x => C (Eaddrof x ty))) as [A | [C' [a' [A [B D]]]]]. - eapply context_compose; eauto. repeat constructor. auto. - auto. - right; exists (fun x => Eaddrof (C' x) ty); exists a'. - split. auto. split. constructor; auto. rewrite D; auto. + Kind. Rec H LV C (fun x => Eaddrof x ty). (* unop *) - exploit safe_expr_kind; eauto; simpl; intros. subst. - destruct (H RV (fun x => C (Eunop op x ty))) as [A | [C' [a' [A [B D]]]]]. - eapply context_compose; eauto. repeat constructor. auto. - auto. - right; exists (fun x => Eunop op (C' x) ty); exists a'. - split. auto. split. constructor; auto. rewrite D; auto. + Kind. Rec H RV C (fun x => Eunop op x ty). (* binop *) - exploit safe_expr_kind; eauto; simpl; intros. subst. - destruct (H RV (fun x => C (Ebinop op x r2 ty))) as [A | [C' [a' [A [B D]]]]]. - eapply context_compose; eauto. repeat constructor. auto. - destruct (H0 RV (fun x => C (Ebinop op r1 x ty))) as [A' | [C' [a' [A' [B D]]]]]. - eapply context_compose; eauto. repeat constructor. auto. - auto. - right; exists (fun x => Ebinop op r1 (C' x) ty); exists a'. - split. auto. split. constructor; auto. rewrite D; auto. - right; exists (fun x => Ebinop op (C' x) r2 ty); exists a'. - split. auto. split. constructor; auto. rewrite D; auto. + Kind. Rec H RV C (fun x => Ebinop op x r2 ty). Rec H0 RV C (fun x => Ebinop op r1 x ty). (* cast *) - exploit safe_expr_kind; eauto; simpl; intros. subst. - destruct (H RV (fun x => C (Ecast x ty))) as [A | [C' [a' [A [B D]]]]]. - eapply context_compose; eauto. repeat constructor. auto. - auto. - right; exists (fun x => Ecast (C' x) ty); exists a'. - split. auto. split. constructor; auto. rewrite D; auto. + Kind. Rec H RV C (fun x => Ecast x ty). (* condition *) - exploit safe_expr_kind; eauto; simpl; intros. subst. - destruct (H RV (fun x => C(Econdition x r2 r3 ty))) as [A | [C' [a' [A [B D]]]]]. - eapply context_compose; eauto. repeat constructor. auto. - right. exists (fun x => x); exists (Econdition r1 r2 r3 ty). - split. red; auto. split. constructor. auto. - right; exists (fun x => Econdition (C' x) r2 r3 ty); exists a'. - split. auto. split. constructor; auto. rewrite D; auto. + Kind. Rec H RV C (fun x => Econdition x r2 r3 ty). Base. (* assign *) - exploit safe_expr_kind; eauto; simpl; intros. subst. - destruct (H LV (fun x => C (Eassign x r ty))) as [A | [C' [a' [A [B D]]]]]. - eapply context_compose; eauto. repeat constructor. auto. - destruct (H0 RV (fun x => C (Eassign l x ty))) as [A' | [C' [a' [A' [B D]]]]]. - eapply context_compose; eauto. repeat constructor. auto. - right. exists (fun x => x); exists (Eassign l r ty). - split. red; auto. split. constructor. auto. - right; exists (fun x => Eassign l (C' x) ty); exists a'. - split. auto. split. constructor; auto. rewrite D; auto. - right; exists (fun x => Eassign (C' x) r ty); exists a'. - split. auto. split. constructor; auto. rewrite D; auto. + Kind. Rec H LV C (fun x => Eassign x r ty). Rec H0 RV C (fun x => Eassign l x ty). Base. (* assignop *) - exploit safe_expr_kind; eauto; simpl; intros. subst. - destruct (H LV (fun x => C (Eassignop op x r tyres ty))) as [A | [C' [a' [A [B D]]]]]. - eapply context_compose; eauto. repeat constructor. auto. - destruct (H0 RV (fun x => C (Eassignop op l x tyres ty))) as [A' | [C' [a' [A' [B D]]]]]. - eapply context_compose; eauto. repeat constructor. auto. - right. exists (fun x => x); exists (Eassignop op l r tyres ty). - split. red; auto. split. constructor. auto. - right; exists (fun x => Eassignop op l (C' x) tyres ty); exists a'. - split. auto. split. constructor; auto. rewrite D; auto. - right; exists (fun x => Eassignop op (C' x) r tyres ty); exists a'. - split. auto. split. constructor; auto. rewrite D; auto. + Kind. Rec H LV C (fun x => Eassignop op x r tyres ty). Rec H0 RV C (fun x => Eassignop op l x tyres ty). Base. (* postincr *) - exploit safe_expr_kind; eauto; simpl; intros. subst. - destruct (H LV (fun x => C(Epostincr id x ty))) as [A | [C' [a' [A [B D]]]]]. - eapply context_compose; eauto. repeat constructor. auto. - right. exists (fun x => x); exists (Epostincr id l ty). - split. red; auto. split. constructor. auto. - right; exists (fun x => Epostincr id (C' x) ty); exists a'. - split. auto. split. econstructor; eauto. rewrite D; auto. + Kind. Rec H LV C (fun x => Epostincr id x ty). Base. (* comma *) - exploit safe_expr_kind; eauto; simpl; intros. subst. - destruct (H RV (fun x => C(Ecomma x r2 ty))) as [A | [C' [a' [A [B D]]]]]. - eapply context_compose; eauto. repeat constructor. auto. - right. exists (fun x => x); exists (Ecomma r1 r2 ty). - split. red; auto. split. constructor. auto. - right; exists (fun x => Ecomma (C' x) r2 ty); exists a'. - split. auto. split. econstructor; eauto. rewrite D; auto. + Kind. Rec H RV C (fun x => Ecomma x r2 ty). Base. (* call *) - exploit safe_expr_kind; eauto; simpl; intros. subst. - destruct (H RV (fun x => C (Ecall x rargs ty))) as [A | [C' [a' [A [B D]]]]]. - eapply context_compose; eauto. repeat constructor. auto. - destruct (H0 (fun x => C (Ecall r1 x ty))) as [A' | [C' [a' [A' [B D]]]]]. + Kind. Rec H RV C (fun x => Ecall x rargs ty). + destruct (H0 (fun x => C (Ecall r1 x ty))) as [A | [C' [a' [D [A B]]]]]. eapply contextlist'_intro with (C := C) (rl0 := Enil). auto. auto. - right. exists (fun x => x); exists (Ecall r1 rargs ty). - split. red; auto. split. constructor. auto. - right; exists (fun x => Ecall r1 (C' x) ty); exists a'. - split. auto. split. constructor; auto. rewrite D; auto. - right; exists (fun x => Ecall (C' x) rargs ty); exists a'. - split. auto. split. constructor; auto. rewrite D; auto. + Base. + right; exists (fun x => Ecall r1 (C' x) ty); exists a'. rewrite D; simpl; auto. (* rparen *) - exploit safe_expr_kind; eauto; simpl; intros. subst. - destruct (H RV (fun x => C (Eparen x ty))) as [A | [C' [a' [A [B D]]]]]. - eapply context_compose; eauto. repeat constructor. auto. - right. exists (fun x => x); exists (Eparen r ty). - split. red; auto. split. constructor. auto. - right; exists (fun x => Eparen (C' x) ty); exists a'. - split. auto. split. econstructor; eauto. rewrite D; auto. + Kind. Rec H RV C (fun x => (Eparen x ty)). Base. (* cons *) destruct (H RV (fun x => C (Econs x rl))) as [A | [C' [a' [A [B D]]]]]. eapply contextlist'_head; eauto. auto. destruct (H0 (fun x => C (Econs r1 x))) as [A' | [C' [a' [A' [B D]]]]]. eapply contextlist'_tail; eauto. auto. auto. - right; exists (fun x => Econs r1 (C' x)); exists a'. - split. auto. split. constructor; auto. rewrite D; auto. - right; exists (fun x => Econs (C' x) rl); exists a'. - split. auto. split. constructor; auto. rewrite D; auto. + right; exists (fun x => Econs r1 (C' x)); exists a'. rewrite A'; eauto. + right; exists (fun x => Econs (C' x) rl); exists a'. rewrite A; eauto. Qed. Lemma decompose_topexpr: forall a, - safe w (ExprState f a k e m) -> + safe (ExprState f a k e m) -> simple a - \/ exists C, exists a', simple_side_effect a' /\ leftcontext RV RV C /\ a = C a'. + \/ exists C, exists a', a = C a' /\ simple_side_effect a' /\ leftcontext RV RV C. Proof. intros. eapply (proj1 decompose_expr). apply ctx_top. auto. Qed. @@ -1076,341 +1026,207 @@ End DECOMPOSITION. (** Simulation for expressions. *) +Lemma estep_simulation: + forall S t S', + estep S t S' -> safe S -> plus Csem.step ge S t S'. +Proof. + intros. inv H. +(* simple *) + exploit eval_simple_rvalue_steps; eauto. simpl; intros STEPS. + exploit star_inv; eauto. intros [[EQ1 EQ2] | A]; auto. + inversion EQ1. rewrite <- H3 in H2; contradiction. +(* condition true *) + eapply plus_safe; eauto. + eapply eval_simple_rvalue_steps with (C := fun x => C(Econdition x r2 r3 (typeof r2))); eauto. + intros. apply plus_one. left; apply step_rred; eauto. apply red_condition_true; auto. +(* condition false *) + eapply plus_safe; eauto. + eapply eval_simple_rvalue_steps with (C := fun x => C(Econdition x r2 r3 (typeof r3))); eauto. + intros. apply plus_one. left; apply step_rred; eauto. apply red_condition_false; auto. +(* assign *) + eapply plus_safe; eauto. + eapply eval_simple_lvalue_steps with (C := fun x => C(Eassign x r (typeof l))); eauto. + intros. eapply plus_safe; eauto. + eapply eval_simple_rvalue_steps with (C := fun x => C(Eassign (Eloc b ofs (typeof l)) x (typeof l))); eauto. + intros. apply plus_one; left; apply step_rred; eauto. econstructor; eauto. +(* assignop *) + eapply plus_safe; eauto. + eapply eval_simple_lvalue_steps with (C := fun x => C(Eassignop op x r tyres (typeof l))); eauto. + intros. eapply plus_safe; eauto. + eapply eval_simple_rvalue_steps with (C := fun x => C(Eassignop op (Eloc b ofs (typeof l)) x tyres (typeof l))); eauto. + intros. apply plus_one; left; apply step_rred; eauto. econstructor; eauto. +(* postincr *) + eapply plus_safe; eauto. + eapply eval_simple_lvalue_steps with (C := fun x => C(Epostincr id x (typeof l))); eauto. + intros. apply plus_one; left; apply step_rred; eauto. econstructor; eauto. +(* comma *) + eapply plus_safe; eauto. + eapply eval_simple_rvalue_steps with (C := fun x => C(Ecomma x r2 (typeof r2))); eauto. + intros. apply plus_one; left; apply step_rred; eauto. econstructor; eauto. +(* paren *) + eapply plus_safe; eauto. + eapply eval_simple_rvalue_steps with (C := fun x => C(Eparen x (typeof r))); eauto. + intros. apply plus_one; left; apply step_rred; eauto. econstructor; eauto. +(* call *) + exploit eval_simple_list_implies; eauto. intros [vl' [A B]]. + eapply plus_safe; eauto. + eapply eval_simple_rvalue_steps with (C := fun x => C(Ecall x rargs ty)); eauto. + intros. eapply plus_safe; eauto. + eapply eval_simple_list_steps with (C := fun x => C(Ecall (Eval vf (typeof rf)) x ty)); eauto. + eapply contextlist'_intro with (rl0 := Enil); auto. + intros. apply plus_one; left; apply Csem.step_call; eauto. + econstructor; eauto. +Qed. + Lemma can_estep: - forall w f a k e m, - safe w (ExprState f a k e m) -> + forall f a k e m, + safe (ExprState f a k e m) -> match a with Eval _ _ => False | _ => True end -> - exists S, - estep (ExprState f a k e m) E0 S - /\ plus Csem.step ge (ExprState f a k e m) E0 S. + exists S, estep (ExprState f a k e m) E0 S. Proof. - intros. destruct (decompose_topexpr f k e m w a H) as [A | [C [b [P [Q R]]]]]. -(* expr *) - exploit (simple_eval_r f k e m w a (fun x => x)); auto. constructor. - intros [v [S T]]. - econstructor; split. - eapply step_expr; eauto. - inversion T. rewrite H2 in H0. contradiction. econstructor; eauto. + intros. destruct (decompose_topexpr f k e m a H) as [A | [C [b [P [Q R]]]]]. +(* simple expr *) + exploit (simple_can_eval f k e m a RV (fun x => x)); auto. intros [v P]. + econstructor; eapply step_expr; eauto. (* side effect *) - clear H0. subst a. red in P. destruct b; try contradiction. + clear H0. subst a. red in Q. destruct b; try contradiction. (* condition *) - set (C1 := fun x => Econdition x b2 b3 ty). - exploit (simple_eval_r f k e m w b1 (fun x => C(C1 x))). auto. - eapply context_compose; eauto. repeat constructor. auto. - unfold C1; intros [v [A B]]. - exploit not_imm_stuck_inv. - eapply safe_not_imm_stuck. eapply safe_steps; eauto. constructor. eauto. - simpl. intros [[X Y] | [X Y]]. - econstructor; split. eapply step_condition_true; eauto. - eapply plus_right. eauto. left; eapply step_rred. constructor; auto. - eapply safe_not_stuck. eapply safe_steps; eauto. constructor. apply leftcontext_context; auto. - traceEq. - econstructor; split. eapply step_condition_false; eauto. - eapply plus_right. eauto. left; eapply step_rred. constructor; auto. - eapply safe_not_stuck. eapply safe_steps; eauto. constructor. apply leftcontext_context; auto. - traceEq. + exploit (simple_can_eval_rval f k e m b1 (fun x => C(Econdition x b2 b3 ty))); eauto. + intros [v1 [E1 S1]]. + exploit safe_inv. eexact S1. eauto. simpl. intros [[T TY] | [F TY]]. + econstructor; eapply step_condition_true; eauto. + econstructor; eapply step_condition_false; eauto. (* assign *) - destruct P. - set (C1 := fun x => Eassign x b2 ty). - exploit (simple_eval_l f k e m w b1 (fun x => C(C1 x))). auto. - eapply context_compose; eauto. repeat constructor. auto. - unfold C1; intros [blk [ofs [A B]]]. - assert (S1: safe w (ExprState f (C (Eassign (Eloc blk ofs (typeof b1)) b2 ty)) k e m)). - eapply safe_steps; eauto. constructor. - set (C2 := fun x => Eassign (Eloc blk ofs (typeof b1)) x ty). - exploit (simple_eval_r f k e m w b2 (fun x => C(C2 x))). auto. - eapply context_compose; eauto. repeat constructor. auto. - unfold C2; intros [v [E F]]. - assert (S2: safe w (ExprState f - (C (Eassign (Eloc blk ofs (typeof b1)) (Eval v (typeof b2)) ty)) k e - m)). - eapply safe_steps; eauto. constructor. - exploit not_imm_stuck_inv. eapply safe_not_imm_stuck. eexact S2. eauto. - simpl. intros [v' [m' [X [Y Z]]]]. - econstructor; split. - eapply step_assign with (C := C); eauto. - eapply star_plus_trans. eapply star_trans; eauto. - apply plus_one. left. apply step_rred. rewrite X. econstructor; eauto. - eapply safe_not_stuck; eauto. apply leftcontext_context; auto. - traceEq. + destruct Q. + exploit (simple_can_eval_lval f k e m b1 (fun x => C(Eassign x b2 ty))); eauto. + intros [b [ofs [E1 S1]]]. + exploit (simple_can_eval_rval f k e m b2 (fun x => C(Eassign (Eloc b ofs (typeof b1)) x ty))); eauto. + intros [v [E2 S2]]. + exploit safe_inv. eexact S2. eauto. simpl. intros [v' [m' [A [B D]]]]. + econstructor; eapply step_assign; eauto. (* assignop *) - destruct P. - set (C1 := fun x => Eassignop op x b2 tyres ty). - exploit (simple_eval_l f k e m w b1 (fun x => C(C1 x))). auto. - eapply context_compose; eauto. repeat constructor. auto. - unfold C1; intros [blk [ofs [A B]]]. - assert (S1: safe w (ExprState f (C (Eassignop op (Eloc blk ofs (typeof b1)) b2 tyres ty)) k e m)). - eapply safe_steps; eauto. constructor. - set (C2 := fun x => Eassignop op (Eloc blk ofs (typeof b1)) x tyres ty). - exploit (simple_eval_r f k e m w b2 (fun x => C(C2 x))). auto. - eapply context_compose; eauto. repeat constructor. auto. - unfold C2; intros [v [E F]]. - assert (S2: safe w (ExprState f - (C - (Eassignop op (Eloc blk ofs (typeof b1)) (Eval v (typeof b2)) - tyres ty)) k e m)). - eapply safe_steps; eauto. constructor. - exploit not_imm_stuck_inv. eapply safe_not_imm_stuck. eexact S2. eauto. - simpl. intros [v1 [v2 [v3 [m' [U [V [W [X Y]]]]]]]]. - econstructor; split. - eapply step_assignop with (C := C); eauto. - eapply star_plus_trans. eapply star_trans; eauto. - apply plus_one. left. apply step_rred. rewrite U. econstructor; eauto. - eapply safe_not_stuck; eauto. apply leftcontext_context; auto. - traceEq. + destruct Q. + exploit (simple_can_eval_lval f k e m b1 (fun x => C(Eassignop op x b2 tyres ty))); eauto. + intros [b [ofs [E1 S1]]]. + exploit (simple_can_eval_rval f k e m b2 (fun x => C(Eassignop op (Eloc b ofs (typeof b1)) x tyres ty))); eauto. + intros [v [E2 S2]]. + exploit safe_inv. eexact S2. eauto. simpl. intros [v1 [v2 [v3 [m' [A [B [D [E F]]]]]]]]. + econstructor; eapply step_assignop; eauto. (* postincr *) - set (C1 := fun x => Epostincr id x ty). - exploit (simple_eval_l f k e m w b (fun x => C(C1 x))). auto. - eapply context_compose; eauto. repeat constructor. auto. - unfold C1; intros [blk [ofs [A B]]]. - assert (S1: safe w (ExprState f (C (Epostincr id (Eloc blk ofs (typeof b)) ty)) k e m)). - eapply safe_steps; eauto. constructor. - exploit not_imm_stuck_inv. eapply safe_not_imm_stuck. eexact S1. eauto. - simpl. intros [v1 [v2 [v3 [m' [U [V [W [X Y]]]]]]]]. - econstructor; split. - eapply step_postincr with (C := C); eauto. - eapply star_plus_trans. eauto. - apply plus_one. left. apply step_rred. subst ty. econstructor; eauto. - eapply safe_not_stuck; eauto. apply leftcontext_context; auto. - traceEq. + exploit (simple_can_eval_lval f k e m b (fun x => C(Epostincr id x ty))); eauto. + intros [b1 [ofs [E1 S1]]]. + exploit safe_inv. eexact S1. eauto. simpl. intros [v1 [v2 [v3 [m' [A [B [D [E F]]]]]]]]. + econstructor; eapply step_postincr; eauto. (* comma *) - set (C1 := fun x => Ecomma x b2 ty). - exploit (simple_eval_r f k e m w b1 (fun x => C(C1 x))). auto. - eapply context_compose; eauto. repeat constructor. auto. - unfold C1; intros [v1 [A B]]. - assert (S1: safe w (ExprState f (C (Ecomma (Eval v1 (typeof b1)) b2 ty)) k e m)). - eapply safe_steps; eauto. constructor. - exploit not_imm_stuck_inv. eapply safe_not_imm_stuck. eexact S1. eauto. - simpl. intro X. - econstructor; split. - eapply step_comma with (C := C); eauto. - eapply star_plus_trans. eauto. - apply plus_one. left. apply step_rred. subst ty. econstructor; eauto. - eapply safe_not_stuck; eauto. apply leftcontext_context; auto. - traceEq. + exploit (simple_can_eval_rval f k e m b1 (fun x => C(Ecomma x b2 ty))); eauto. + intros [v1 [E1 S1]]. + exploit safe_inv. eexact S1. eauto. simpl. intros EQ. + econstructor; eapply step_comma; eauto. (* call *) - destruct P. - set (C1 := fun x => Ecall x rargs ty). - exploit (simple_eval_r f k e m w b (fun x => C(C1 x))). auto. - eapply context_compose; eauto. repeat constructor. auto. - unfold C1; intros [vf [A B]]. - assert (S1: safe w (ExprState f (C (Ecall (Eval vf (typeof b)) rargs ty)) k e m)). - eapply safe_steps; eauto. constructor. - exploit (simple_eval_rlist f k e m w rargs (fun x => C(Ecall (Eval vf (typeof b)) x ty))). - auto. eapply contextlist'_intro with (rl0 := Enil). auto. auto. - intros [vl [E F]]. - assert (S2: safe w (ExprState f (C (Ecall (Eval vf (typeof b)) (rval_list vl rargs) ty)) - k e m)). - eapply safe_steps; eauto. constructor. - exploit not_imm_stuck_inv. eapply safe_not_imm_stuck. eexact S2. eauto. - simpl. intros X. - destruct X as [tyargs [tyres [fd [vl' [U [V [W X]]]]]]]. - apply rval_list_all_values. - econstructor; split. - eapply step_call with (C := C); eauto. eapply can_eval_simple_list; eauto. - eapply plus_right. eapply star_trans; eauto. - left. econstructor. econstructor; eauto. - eapply safe_not_stuck; eauto. apply leftcontext_context; auto. - traceEq. -(* rparen *) - set (C1 := fun x => Eparen x ty). - exploit (simple_eval_r f k e m w b (fun x => C(C1 x))). auto. - eapply context_compose; eauto. repeat constructor. auto. - unfold C1; intros [v [A B]]. - assert (S1: safe w (ExprState f (C (Eparen (Eval v (typeof b)) ty)) k e m)). - eapply safe_steps; eauto. constructor. - exploit not_imm_stuck_inv. eapply safe_not_imm_stuck. eexact S1. eauto. - simpl. intros EQ. subst ty. - econstructor; split. - eapply step_paren with (C := C); eauto. - eapply star_plus_trans. eauto. - apply plus_one. left. apply step_rred. econstructor; eauto. - eapply safe_not_stuck; eauto. apply leftcontext_context; auto. - traceEq. + destruct Q. + exploit (simple_can_eval_rval f k e m b (fun x => C(Ecall x rargs ty))); eauto. + intros [vf [E1 S1]]. + pose (C' := fun x => C(Ecall (Eval vf (typeof b)) x ty)). + assert (contextlist' C'). unfold C'; eapply contextlist'_intro with (rl0 := Enil); auto. + exploit (simple_list_can_eval f k e m rargs C'); eauto. + intros [vl E2]. + exploit safe_inv. 2: eapply leftcontext_context; eexact R. + eapply safe_steps. eexact S1. + apply (eval_simple_list_steps f k e m rargs vl E2 C'); auto. + simpl. intros X. exploit X. eapply rval_list_all_values. + intros [tyargs [tyres [fd [vargs [P [Q [U V]]]]]]]. + econstructor; eapply step_call; eauto. eapply can_eval_simple_list; eauto. +(* paren *) + exploit (simple_can_eval_rval f k e m b (fun x => C(Eparen x ty))); eauto. + intros [v1 [E1 S1]]. + exploit safe_inv. eexact S1. eauto. simpl. intros EQ. + econstructor; eapply step_paren; eauto. Qed. -(** The main simulation result. *) +(** Simulation for all states *) -Theorem strategy_simulation: - forall w S, - safe w S -> - (exists r, final_state S r) - \/ (exists t, exists S', exists w', - step S t S' - /\ plus Csem.step ge S t S' - /\ possible_trace w t w'). +Theorem step_simulation: + forall S1 t S2, + step S1 t S2 -> safe S1 -> plus Csem.step ge S1 t S2. Proof. - intros. exploit safe_imm; eauto. intros IS; inv IS. -(* terminated *) - left; exists r; auto. - destruct H0. -(* expression step *) - inv H0. - (* lred *) - exploit can_estep; eauto. inv H4; auto. - intros [S [A B]]. right. exists E0; exists S; exists w. - split. left; auto. split. auto. constructor. - (* rred *) - exploit can_estep; eauto. inv H4; auto. inv H2; auto. - intros [S [A B]]. right. exists E0; exists S; exists w. - split. left; auto. split. auto. constructor. - (* callred *) - exploit can_estep; eauto. inv H4; auto. inv H2; auto. - intros [S [A B]]. right. exists E0; exists S; exists w. - split. left; auto. split. auto. constructor. -(* other step *) - right. exists t; exists s'; exists w'. - split. right. auto. - split. apply plus_one. right. auto. - auto. -Qed. - -End STRATEGY. - -(** * Whole-program behaviors *) - -Definition exec_program (p: program) (beh: program_behavior) : Prop := - program_behaves step (initial_state p) final_state (Genv.globalenv p) beh. - -Definition safeprog (p: program) (w: world) : Prop := - (exists s, initial_state p s) - /\ (forall s, initial_state p s -> safe (Genv.globalenv p) w s). - -(** We now show the existence of a safe behavior for the strategy, - which is also an acceptable behavior for the nondeterministic semantics. *) - -Section BEHAVIOR. - -Variable prog: program. -Variable initial_world: world. - -(** We define a transition semantics that combines -- one strategy step; -- one or several nondeterministic steps; -- the state of the external world. -*) - -Local Open Scope pair_scope. - -Definition comb_state := (state * world)%type. - -Definition comb_step (ge: genv) (s: comb_state) (t: trace) (s': comb_state) : Prop := - (step ge s#1 t s'#1 /\ plus Csem.step ge s#1 t s'#1) - /\ possible_trace s#2 t s'#2. - -Definition comb_initial_state (s: comb_state) : Prop := - initial_state prog s#1 /\ s#2 = initial_world. - -Definition comb_final_state (s: comb_state) (r: int) : Prop := - final_state s#1 r. - -Definition comb_program_behaves (beh: program_behavior) : Prop := - program_behaves comb_step comb_initial_state comb_final_state (Genv.globalenv prog) beh. - -(** If the source program is safe, the combined semantics cannot go wrong. *) - -Remark proj_star_comb_step: - forall ge s t s', - star comb_step ge s t s' -> - star Csem.step ge s#1 t s'#1 /\ possible_trace s#2 t s'#2. -Proof. - induction 1. split; constructor. - destruct H as [[A B] C]. destruct IHstar. - split. eapply star_trans. apply plus_star; eauto. eauto. auto. - subst t. eapply possible_trace_app; eauto. + intros. inv H. + apply estep_simulation; auto. + apply plus_one. right. auto. Qed. -Lemma comb_behavior_not_wrong: - forall beh, - safeprog prog initial_world -> comb_program_behaves beh -> not_wrong beh. +Theorem progress: + forall S, + safe S -> (exists r, final_state S r) \/ (exists t, exists S', step S t S'). Proof. - intros. destruct H. inv H0; simpl; auto. -(* Goes wrong after some steps *) - destruct H2. exploit proj_star_comb_step; eauto. intros [A B]. - assert (C: safe (Genv.globalenv prog) s'#2 s'#1). - eapply safe_steps. apply H1. eauto. eauto. congruence. - exploit strategy_simulation. eexact C. - intros [[r P] | [t' [s'' [w'' [P [Q R]]]]]]. - elim (H5 r). auto. - elim (H4 t' (s'', w'')). red. auto. -(* Goes initiall wrong *) - destruct H as [s A]. elim (H2 (s, initial_world)). red; auto. + intros. exploit H. apply star_refl. intros [FIN | [t [S' STEP]]]. + (* 1. Finished. *) + auto. + right. destruct STEP. + (* 2. Expression step. *) + assert (exists S', estep S E0 S'). + inv H0. + (* lred *) + eapply can_estep; eauto. inv H3; auto. + (* rred *) + eapply can_estep; eauto. inv H3; auto. inv H1; auto. + (* callred *) + eapply can_estep; eauto. inv H3; auto. inv H1; auto. + destruct H1 as [S'' ESTEP]. + exists E0; exists S''; left; auto. + (* 3. Other step. *) + exists t; exists S'; right; auto. Qed. -(** Any non-wrong behavior of the combined semantics is a behavior - for the nondeterministic semantics. *) - -Lemma proj1_comb_behavior: - forall beh, - not_wrong beh -> - comb_program_behaves beh -> - Csem.exec_program prog beh. -Proof. - intros. red in H0. red. - eapply simulation_plus_preservation with - (match_states := fun (S1: comb_state) (S2: state) => S2 = S1#1); eauto. - intros. destruct H1. exists (st1#1); auto. - intros. red in H2. congruence. - intros. destruct H1 as [[A B] D]. subst st2. exists (st1'#1); auto. -Qed. +End STRATEGY. -(** Likewise, any non-wrong behavior of the combined semantics is a behavior - for the strategy. *) +(** The semantics that follows the strategy. *) -Lemma proj2_comb_behavior: - forall beh, - not_wrong beh -> - comb_program_behaves beh -> - exec_program prog beh. -Proof. - intros. red in H0. red. - eapply simulation_step_preservation with - (match_states := fun (S1: comb_state) (S2: state) => S2 = S1#1); eauto. - intros. destruct H1. exists (st1#1); auto. - intros. red in H2. congruence. - intros. destruct H1 as [[A B] D]. subst st2. exists (st1'#1); auto. -Qed. +Definition semantics (p: program) := + Semantics step (initial_state p) final_state (Genv.globalenv p). -(** Finally, any behavior of the combined semantics is possible in the - initial world. *) +(** This semantics is receptive to changes in events. *) -Lemma possible_comb_behavior: - forall beh, - comb_program_behaves beh -> - possible_behavior initial_world beh. +Lemma semantics_receptive: + forall p, receptive (semantics p). Proof. - intros. - apply (project_behaviors_trace _ _ - (fun ge s t s' => step ge s t s' /\ plus Csem.step ge s t s') - (initial_state prog) - final_state - initial_world (Genv.globalenv prog)). - exact H. + intros. constructor; simpl; intros. +(* receptiveness *) + assert (t1 = E0 -> exists s2, step (Genv.globalenv p) s t2 s2). + intros. subst. inv H0. exists s1; auto. + inversion H; subst. + inv H2; auto. + inv H2; auto. + exploit external_call_receptive; eauto. intros [vres2 [m2 EC2]]. + exists (Returnstate vres2 k m2). right; econstructor; eauto. +(* trace length *) + inv H. + inv H0; simpl; omega. + inv H0; simpl; try omega. eapply external_call_trace_length; eauto. Qed. -(** It follows that a safe C program has a non-wrong behavior that - follows the strategy. *) +(** The main simulation result. *) -Theorem strategy_behavior: - safeprog prog initial_world -> - exists beh, not_wrong beh - /\ Csem.exec_program prog beh - /\ exec_program prog beh - /\ possible_behavior initial_world beh. +Theorem strategy_simulation: + forall p, backward_simulation (Csem.semantics p) (semantics p). Proof. intros. - assert (exists beh, comb_program_behaves beh). - unfold comb_program_behaves. apply program_behaves_exists. - destruct H0 as [beh CPB]. - assert (not_wrong beh). eapply comb_behavior_not_wrong; eauto. - exists beh. split. auto. - split. apply proj1_comb_behavior; auto. - split. apply proj2_comb_behavior; auto. - apply possible_comb_behavior; auto. + apply backward_simulation_plus with (match_states := fun (S1 S2: state) => S1 = S2); simpl. +(* symbols *) + auto. +(* trace length *) + intros. eapply sr_traces. apply semantics_receptive. simpl. eauto. +(* initial states exist *) + intros. exists s1; auto. +(* initial states match *) + intros. exists s2; auto. +(* final states match *) + intros. subst s2. auto. +(* progress *) + intros. subst s2. apply progress. auto. +(* simulation *) + intros. subst s1. exists s2'; split; auto. apply step_simulation; auto. Qed. -End BEHAVIOR. - (** * A big-step semantics implementing the reduction strategy. *) Section BIGSTEP. @@ -2778,34 +2594,22 @@ Inductive bigstep_program_diverges (p: program): traceinf -> Prop := evalinf_funcall ge m0 f nil t -> bigstep_program_diverges p t. -Theorem bigstep_program_terminates_exec: - forall prog t r, - bigstep_program_terminates prog t r -> exec_program prog (Terminates t r). -Proof. - intros. inv H. - econstructor. - econstructor; eauto. - apply eval_funcall_to_steps. eauto. red; auto. - econstructor. -Qed. +Definition bigstep_semantics (p: program) := + Bigstep_semantics (bigstep_program_terminates p) (bigstep_program_diverges p). -Theorem bigstep_program_diverges_exec: - forall prog T, - bigstep_program_diverges prog T -> - exec_program prog (Reacts T) \/ - exists t, exec_program prog (Diverges t) /\ traceinf_prefix t T. +Theorem bigstep_semantics_sound: + forall p, bigstep_sound (bigstep_semantics p) (semantics p). Proof. - intros. inv H. - set (st := Callstate f nil Kstop m0). - assert (forever step ge st T). - eapply forever_N_forever with (order := lt). - apply lt_wf. - eapply evalinf_funcall_steps; eauto. - destruct (forever_silent_or_reactive _ _ _ _ _ _ H) - as [A | [t [s' [T' [B [C D]]]]]]. - left. econstructor. econstructor; eauto. eauto. - right. exists t. split. - econstructor. econstructor; eauto. eauto. auto. - subst T. rewrite <- (E0_right t) at 1. apply traceinf_prefix_app. constructor. + intros; constructor; intros. +(* termination *) + inv H. econstructor; econstructor. + split. econstructor; eauto. + split. apply eval_funcall_to_steps. eauto. red; auto. + econstructor. +(* divergence *) + inv H. econstructor. + split. econstructor; eauto. + eapply forever_N_forever with (order := lt). + apply lt_wf. + eapply evalinf_funcall_steps; eauto. Qed. - diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v index cff182d..ca45b4d 100644 --- a/cfrontend/SimplExprproof.v +++ b/cfrontend/SimplExprproof.v @@ -24,7 +24,6 @@ Require Import Memory. Require Import Events. Require Import Smallstep. Require Import Globalenvs. -Require Import Determinism. Require Import Csyntax. Require Import Csem. Require Import Cstrategy. @@ -1835,15 +1834,13 @@ Proof. Qed. Theorem transl_program_correct: - forall (beh: program_behavior), - not_wrong beh -> Cstrategy.exec_program prog beh -> - Clight.exec_program tprog beh. + forward_simulation (Cstrategy.semantics prog) (Clight.semantics tprog). Proof. - unfold Cstrategy.exec_program, Clight.exec_program. intros. - eapply simulation_star_wf_preservation; eauto. + eapply forward_simulation_star_wf with (order := ltof _ measure). + eexact symbols_preserved. eexact transl_initial_states. eexact transl_final_states. - instantiate (1 := ltof _ measure). apply well_founded_ltof. + apply well_founded_ltof. exact simulation. Qed. 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 +}. diff --git a/driver/Compiler.v b/driver/Compiler.v index d8810a4..a51cd8f 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -171,15 +171,19 @@ Definition transf_cminor_program (p: Cminor.program) : res Asm.program := @@ Selection.sel_program @@@ transform_partial_program transf_cminorsel_fundef. -Definition transf_c_program (p: Csyntax.program) : res Asm.program := +Definition transf_clight_program (p: Clight.program) : res Asm.program := OK p - @@ print print_Csyntax - @@@ SimplExpr.transl_program @@ print print_Clight @@@ Cshmgen.transl_program @@@ Cminorgen.transl_program @@@ transf_cminor_program. +Definition transf_c_program (p: Csyntax.program) : res Asm.program := + OK p + @@ print print_Csyntax + @@@ SimplExpr.transl_program + @@@ transf_clight_program. + (** Force [Initializers] to be extracted as well. *) Definition transl_init := Initializers.transl_init. @@ -199,16 +203,18 @@ Lemma map_partial_compose: (f1: A -> res B) (f2: B -> res C) (pa: list (X * A)) (pc: list (X * C)), map_partial ctx (fun f => f1 f @@@ f2) pa = OK pc -> - exists pb, map_partial ctx f1 pa = OK pb /\ map_partial ctx f2 pb = OK pc. + { pb | map_partial ctx f1 pa = OK pb /\ map_partial ctx f2 pb = OK pc }. Proof. induction pa; simpl. intros. inv H. econstructor; eauto. intro pc. destruct a as [x a]. - caseEq (f1 a); simpl; try congruence. intros b F1. - caseEq (f2 b); simpl; try congruence. intros c F2 EQ. - monadInv EQ. exploit IHpa; eauto. intros [pb [P Q]]. + destruct (f1 a) as [] _eqn; simpl; try congruence. + destruct (f2 b) as [] _eqn; simpl; try congruence. + destruct (map_partial ctx (fun f => f1 f @@@ f2) pa) as [] _eqn; simpl; try congruence. + intros. inv H. + destruct (IHpa l) as [pb [P Q]]; auto. rewrite P; simpl. - exists ((x, b) :: pb); split. auto. simpl. rewrite F2. rewrite Q. auto. + econstructor; split. eauto. simpl. rewrite Heqr0. rewrite Q. auto. Qed. Lemma transform_partial_program_compose: @@ -216,11 +222,13 @@ Lemma transform_partial_program_compose: (f1: A -> res B) (f2: B -> res C) (pa: program A V) (pc: program C V), transform_partial_program (fun f => f1 f @@@ f2) pa = OK pc -> - exists pb, transform_partial_program f1 pa = OK pb /\ - transform_partial_program f2 pb = OK pc. + { pb | transform_partial_program f1 pa = OK pb /\ + transform_partial_program f2 pb = OK pc }. Proof. - intros. monadInv H. - exploit map_partial_compose; eauto. intros [xb [P Q]]. + intros. unfold transform_partial_program in H. + destruct (map_partial prefix_name (fun f : A => f1 f @@@ f2) (prog_funct pa)) as [] _eqn; + simpl in H; inv H. + destruct (map_partial_compose _ _ _ _ _ _ _ _ _ Heqr) as [xb [P Q]]. exists (mkprogram xb (prog_main pa) (prog_vars pa)); split. unfold transform_partial_program. rewrite P; auto. unfold transform_partial_program. simpl. rewrite Q; auto. @@ -240,14 +248,14 @@ Lemma transform_program_compose: (f1: A -> res B) (f2: B -> C) (pa: program A V) (pc: program C V), transform_partial_program (fun f => f1 f @@ f2) pa = OK pc -> - exists pb, transform_partial_program f1 pa = OK pb /\ - transform_program f2 pb = pc. + { pb | transform_partial_program f1 pa = OK pb /\ + transform_program f2 pb = pc }. Proof. intros. replace (fun f : A => f1 f @@ f2) with (fun f : A => f1 f @@@ (fun x => OK (f2 x))) in H. - exploit transform_partial_program_compose; eauto. - intros [pb [X Y]]. exists pb; split. auto. + destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H) as [pb [X Y]]. + exists pb; split. auto. apply transform_program_partial_program. auto. apply extensionality; intro. destruct(f1 x); auto. Qed. @@ -283,9 +291,17 @@ Qed. (** * Semantic preservation *) -(** We prove that the [transf_program] translations preserve semantics. - The proof composes the semantic preservation results for each pass. - This establishes the correctness of the whole compiler! *) +(** We prove that the [transf_program] translations preserve semantics + by constructing the following simulations: +- Forward simulations from [Cstrategy] / [Cminor] / [RTL] to [Asm] + (composition of the forward simulations for each pass). +- Backward simulations for the same languages + (derived from the forward simulation, using receptiveness of the source + language and determinacy of [Asm]). +- Backward simulation from [Csem] to [Asm] + (composition of two backward simulations). + +These results establish the correctness of the whole compiler! *) Ltac TransfProgInv := match goal with @@ -300,16 +316,17 @@ Ltac TransfProgInv := end. Theorem transf_rtl_program_correct: - forall p tp beh, + forall p tp, transf_rtl_program p = OK tp -> - not_wrong beh -> - RTL.exec_program p beh -> - Asm.exec_program tp beh. + forward_simulation (RTL.semantics p) (Asm.semantics tp) + * backward_simulation (RTL.semantics p) (Asm.semantics tp). Proof. - intros. unfold transf_rtl_program, transf_rtl_fundef in H. + intros. + assert (F: forward_simulation (RTL.semantics p) (Asm.semantics tp)). + unfold transf_rtl_program, transf_rtl_fundef in H. repeat TransfProgInv. repeat rewrite transform_program_print_identity in *. subst. - exploit transform_partial_program_identity; eauto. intro EQ. subst. + generalize (transform_partial_program_identity _ _ _ _ X0). intro EQ. subst. generalize Alloctyping.program_typing_preserved Tunnelingtyping.program_typing_preserved @@ -318,49 +335,93 @@ Proof. Reloadtyping.program_typing_preserved Stackingtyping.program_typing_preserved; intros. - eapply Asmgenproof.transf_program_correct; eauto 8. - eapply Stackingproof.transf_program_correct; eauto 6. - eapply Reloadproof.transf_program_correct; eauto. - eapply CleanupLabelsproof.transf_program_correct; eauto. - eapply Linearizeproof.transf_program_correct; eauto. - eapply Tunnelingproof.transf_program_correct; eauto. - eapply Allocproof.transf_program_correct; eauto. - eapply CSEproof.transf_program_correct; eauto. - eapply Constpropproof.transf_program_correct; eauto. - eapply CastOptimproof.transf_program_correct; eauto. - eapply Tailcallproof.transf_program_correct; eauto. + eapply compose_forward_simulation. apply Tailcallproof.transf_program_correct. + eapply compose_forward_simulation. apply CastOptimproof.transf_program_correct. + eapply compose_forward_simulation. apply Constpropproof.transf_program_correct. + eapply compose_forward_simulation. apply CSEproof.transf_program_correct. + eapply compose_forward_simulation. apply Allocproof.transf_program_correct. eassumption. + eapply compose_forward_simulation. apply Tunnelingproof.transf_program_correct. + eapply compose_forward_simulation. apply Linearizeproof.transf_program_correct. eassumption. eauto. + eapply compose_forward_simulation. apply CleanupLabelsproof.transf_program_correct. + eapply compose_forward_simulation. apply Reloadproof.transf_program_correct. eauto. + eapply compose_forward_simulation. apply Stackingproof.transf_program_correct. eassumption. eauto 8. + apply Asmgenproof.transf_program_correct; eauto 10. + split. auto. + apply forward_to_backward_simulation. auto. + apply RTL.semantics_receptive. + apply Asm.semantics_determinate. Qed. Theorem transf_cminor_program_correct: - forall p tp beh, + forall p tp, transf_cminor_program p = OK tp -> - not_wrong beh -> - Cminor.exec_program p beh -> - Asm.exec_program tp beh. + forward_simulation (Cminor.semantics p) (Asm.semantics tp) + * backward_simulation (Cminor.semantics p) (Asm.semantics tp). Proof. - intros. unfold transf_cminor_program, transf_cminorsel_fundef in H. + intros. + assert (F: forward_simulation (Cminor.semantics p) (Asm.semantics tp)). + unfold transf_cminor_program, transf_cminorsel_fundef in H. simpl in H. repeat TransfProgInv. - eapply transf_rtl_program_correct; eauto. - eapply RTLgenproof.transf_program_correct; eauto. - eapply Selectionproof.transf_program_correct; eauto. + eapply compose_forward_simulation. apply Selectionproof.transf_program_correct. + eapply compose_forward_simulation. apply RTLgenproof.transf_program_correct. eassumption. + exact (fst (transf_rtl_program_correct _ _ P)). + + split. auto. + apply forward_to_backward_simulation. auto. + apply Cminor.semantics_receptive. + apply Asm.semantics_determinate. Qed. -Theorem transf_c_program_correct: - forall p tp beh, - transf_c_program p = OK tp -> - not_wrong beh -> - Cstrategy.exec_program p beh -> - Asm.exec_program tp beh. +Theorem transf_clight_program_correct: + forall p tp, + transf_clight_program p = OK tp -> + forward_simulation (Clight.semantics p) (Asm.semantics tp) + * backward_simulation (Clight.semantics p) (Asm.semantics tp). Proof. - intros until beh; unfold transf_c_program; simpl. - rewrite print_identity. - caseEq (SimplExpr.transl_program p); simpl; try congruence; intros p0 EQ0. + intros. + assert (F: forward_simulation (Clight.semantics p) (Asm.semantics tp)). + revert H; unfold transf_clight_program; simpl. rewrite print_identity. - caseEq (Cshmgen.transl_program p0); simpl; try congruence; intros p1 EQ1. + caseEq (Cshmgen.transl_program p); simpl; try congruence; intros p1 EQ1. caseEq (Cminorgen.transl_program p1); simpl; try congruence; intros p2 EQ2. - intros EQ3 NOTW SEM. - eapply transf_cminor_program_correct; eauto. - eapply Cminorgenproof.transl_program_correct; eauto. - eapply Cshmgenproof.transl_program_correct; eauto. - eapply SimplExprproof.transl_program_correct; eauto. + intros EQ3. + eapply compose_forward_simulation. apply Cshmgenproof.transl_program_correct. eauto. + eapply compose_forward_simulation. apply Cminorgenproof.transl_program_correct. eauto. + exact (fst (transf_cminor_program_correct _ _ EQ3)). + + split. auto. + apply forward_to_backward_simulation. auto. + apply Clight.semantics_receptive. + apply Asm.semantics_determinate. +Qed. + +Theorem transf_cstrategy_program_correct: + forall p tp, + transf_c_program p = OK tp -> + forward_simulation (Cstrategy.semantics p) (Asm.semantics tp) + * backward_simulation (Cstrategy.semantics p) (Asm.semantics tp). +Proof. + intros. + assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics tp)). + revert H; unfold transf_c_program; simpl. rewrite print_identity. + caseEq (SimplExpr.transl_program p); simpl; try congruence; intros p0 EQ0. + intros EQ1. + eapply compose_forward_simulation. apply SimplExprproof.transl_program_correct. eauto. + exact (fst (transf_clight_program_correct _ _ EQ1)). + + split. auto. + apply forward_to_backward_simulation. auto. + apply Cstrategy.semantics_receptive. + apply Asm.semantics_determinate. +Qed. + +Theorem transf_c_program_correct: + forall p tp, + transf_c_program p = OK tp -> + backward_simulation (Csem.semantics p) (Asm.semantics tp). +Proof. + intros. + eapply compose_backward_simulation. + apply Cstrategy.strategy_simulation. + exact (snd (transf_cstrategy_program_correct _ _ H)). Qed. diff --git a/driver/Complements.v b/driver/Complements.v index e6b0095..1b7e974 100644 --- a/driver/Complements.v +++ b/driver/Complements.v @@ -20,223 +20,179 @@ Require Import Values. Require Import Events. Require Import Globalenvs. Require Import Smallstep. -Require Import Determinism. +Require Import Behaviors. Require Import Csyntax. Require Import Csem. Require Import Cstrategy. +Require Import Clight. +Require Import Cminor. +Require Import RTL. Require Import Asm. Require Import Compiler. Require Import Errors. -(** * Integrating a deterministic external world *) +(** * Preservation of whole-program behaviors *) -(** We now integrate a deterministic external world in the semantics - of Compcert C and Asm. *) +(** From the simulation diagrams proved in file [Compiler]. it follows that + whole-program observable behaviors are preserved in the following sense. + First, every behavior of the generated assembly code is matched by + a behavior of the source C code. *) -Section WORLD. - -Variable initial_world: world. - -Definition exec_C_program (p: Csyntax.program) (beh: program_behavior) : Prop := - wprogram_behaves _ _ - Csem.step (Csem.initial_state p) Csem.final_state - initial_world (Genv.globalenv p) beh. - -Definition exec_asm_program (p: Asm.program) (beh: program_behavior) : Prop := - wprogram_behaves _ _ - Asm.step (Asm.initial_state p) Asm.final_state - initial_world (Genv.globalenv p) beh. - -(** ** Safety of C programs. *) +Theorem transf_c_program_preservation: + forall p tp beh, + transf_c_program p = OK tp -> + program_behaves (Asm.semantics tp) beh -> + exists beh', program_behaves (Csem.semantics p) beh' /\ behavior_improves beh' beh. +Proof. + intros. eapply backward_simulation_behavior_improves; eauto. + apply transf_c_program_correct; auto. +Qed. -(** We show that a C program is safe (in the sense of [Cstrategy.safeprog]) - if it cannot go wrong in the world-aware semantics. *) +(** As a corollary, if the source C code cannot go wrong, the behavior of the + generated assembly code is one of the possible behaviors of the source C code. *) -Lemma notwrong_safeprog: - forall p, - (forall beh, exec_C_program p beh -> not_wrong beh) -> - Cstrategy.safeprog p initial_world. +Theorem transf_c_program_is_refinement: + forall p tp, + transf_c_program p = OK tp -> + (forall beh, program_behaves (Csem.semantics p) beh -> not_wrong beh) -> + (forall beh, program_behaves (Asm.semantics tp) beh -> program_behaves (Csem.semantics p) beh). Proof. - intros; red. - assert (exists beh1, exec_C_program p beh1). - unfold exec_C_program. apply program_behaves_exists. - destruct H0 as [beh1 A]. - assert (B: not_wrong beh1) by auto. - split. - inv A; simpl in B. - destruct H0. exists (fst s); auto. - destruct H0. exists (fst s); auto. - destruct H0. exists (fst s); auto. - contradiction. - contradiction. - intros; red; intros. - destruct (classic (exists r, Csem.final_state s' r)). - (* 1. Final state. This is immsafe. *) - destruct H3 as [r F]. eapply immsafe_final; eauto. - (* 2. Not a final state. *) - destruct (classic (nostep (wstep _ _ Csem.step) (Genv.globalenv p) (s', w'))). - (* 2.1 No step possible -> going wrong *) - elim (H (Goes_wrong t)). - eapply program_goes_wrong. - instantiate (1 := (s, initial_world)). split; auto. - instantiate (1 := (s', w')). apply Determinism.inject_star; auto. - auto. - intros; red; intros. elim H3. exists r; auto. - (* 2.2 One step possible -> this is immsafe *) - unfold nostep in H4. - generalize (not_all_ex_not _ _ H4). clear H4. intros [t' P]. - generalize (not_all_ex_not _ _ P). clear P. intros [s'' Q]. - generalize (NNPP _ Q). clear Q. intros R. destruct R as [R1 R2]. simpl in *. - eapply immsafe_step. eauto. eauto. + intros. eapply backward_simulation_same_safe_behavior; eauto. + apply transf_c_program_correct; auto. Qed. -(** ** Determinism of Asm semantics *) +(** If we consider the C evaluation strategy implemented by the compiler, + we get stronger preservation results. *) -Remark extcall_arguments_deterministic: - forall rs m sg args args', - extcall_arguments rs m sg args -> - extcall_arguments rs m sg args' -> args = args'. +Theorem transf_cstrategy_program_preservation: + forall p tp, + transf_c_program p = OK tp -> + (forall beh, program_behaves (Cstrategy.semantics p) beh -> + exists beh', program_behaves (Asm.semantics tp) beh' /\ behavior_improves beh beh') +/\(forall beh, program_behaves (Asm.semantics tp) beh -> + exists beh', program_behaves (Cstrategy.semantics p) beh' /\ behavior_improves beh' beh) +/\(forall beh, not_wrong beh -> + program_behaves (Cstrategy.semantics p) beh -> program_behaves (Asm.semantics tp) beh) +/\(forall beh, + (forall beh', program_behaves (Cstrategy.semantics p) beh' -> not_wrong beh') -> + program_behaves (Asm.semantics tp) beh -> + program_behaves (Cstrategy.semantics p) beh). Proof. - unfold extcall_arguments; intros. - revert args H args' H0. generalize (Conventions1.loc_arguments sg); induction 1; intros. - inv H0; auto. - inv H1; decEq; auto. inv H; inv H4; congruence. + intros. intuition. + eapply forward_simulation_behavior_improves; eauto. + apply (fst (transf_cstrategy_program_correct _ _ H)). + eapply backward_simulation_behavior_improves; eauto. + apply (snd (transf_cstrategy_program_correct _ _ H)). + eapply forward_simulation_same_safe_behavior; eauto. + apply (fst (transf_cstrategy_program_correct _ _ H)). + eapply backward_simulation_same_safe_behavior; eauto. + apply (snd (transf_cstrategy_program_correct _ _ H)). Qed. -Remark annot_arguments_deterministic: - forall rs m pl args args', - annot_arguments rs m pl args -> - annot_arguments rs m pl args' -> args = args'. +(** We can also use the alternate big-step semantics for [Cstrategy] + to establish behaviors of the generated assembly code. *) + +Theorem bigstep_cstrategy_preservation: + forall p tp, + transf_c_program p = OK tp -> + (forall t r, + Cstrategy.bigstep_program_terminates p t r -> + program_behaves (Asm.semantics tp) (Terminates t r)) +/\(forall T, + Cstrategy.bigstep_program_diverges p T -> + program_behaves (Asm.semantics tp) (Reacts T) + \/ exists t, program_behaves (Asm.semantics tp) (Diverges t) /\ traceinf_prefix t T). Proof. - unfold annot_arguments; intros. - revert pl args H args' H0. induction 1; intros. - inv H0; auto. - inv H1; decEq; auto. inv H; inv H4; congruence. + intuition. + apply transf_cstrategy_program_preservation with p; auto. red; auto. + apply behavior_bigstep_terminates with (Cstrategy.bigstep_semantics p); auto. + apply Cstrategy.bigstep_semantics_sound. + exploit (behavior_bigstep_diverges (Cstrategy.bigstep_semantics_sound p)). eassumption. + intros [A | [t [A B]]]. + left. apply transf_cstrategy_program_preservation with p; auto. red; auto. + right; exists t; split; auto. apply transf_cstrategy_program_preservation with p; auto. red; auto. Qed. -Lemma step_internal_deterministic: - forall ge s t1 s1 t2 s2, - Asm.step ge s t1 s1 -> Asm.step ge s t2 s2 -> matching_traces t1 t2 -> - s1 = s2 /\ t1 = t2. -Proof. +(** * Satisfaction of specifications *) -Ltac InvEQ := - match goal with - | [ H1: ?x = ?y, H2: ?x = ?z |- _ ] => rewrite H1 in H2; inv H2; InvEQ - | _ => idtac - end. - - intros. inv H; inv H0; InvEQ. -(* regular, regular *) - split; congruence. -(* regular, builtin *) - simpl in H5; inv H5. -(* regular, annot *) - simpl in H5; inv H5. -(* builtin, regular *) - simpl in H12; inv H12. -(* builtin, builtin *) - exploit external_call_determ. eexact H5. eexact H12. auto. intros [A [B C]]. subst. - auto. -(* annot, regular *) - simpl in H13. inv H13. -(* annot, annot *) - exploit annot_arguments_deterministic. eexact H5. eexact H11. intros EQ; subst. - exploit external_call_determ. eexact H6. eexact H14. auto. intros [A [B C]]. subst. - auto. -(* extcall, extcall *) - exploit extcall_arguments_deterministic. eexact H5. eexact H10. intros EQ; subst. - exploit external_call_determ. eexact H4. eexact H9. auto. intros [A [B C]]. subst. - auto. -Qed. +(** The second additional results shows that if all executions + of the source C program satisfies a given specification + (a predicate on the observable behavior of the program), + then all executions of the produced Asm program satisfy + this specification as well. -Lemma initial_state_deterministic: - forall p s1 s2, - initial_state p s1 -> initial_state p s2 -> s1 = s2. -Proof. - intros. inv H; inv H0. f_equal. congruence. -Qed. + We first show this result for specifications that are stable + under the [behavior_improves] relation. *) -Lemma final_state_not_step: - forall ge st r, final_state st r -> nostep step ge st. -Proof. - unfold nostep. intros. red; intros. inv H. inv H0; unfold Vzero in H1; congruence. -Qed. +Section SPECS_PRESERVED. -Lemma final_state_deterministic: - forall st r1 r2, final_state st r1 -> final_state st r2 -> r1 = r2. -Proof. - intros. inv H; inv H0. congruence. -Qed. +Variable spec: program_behavior -> Prop. + +Hypothesis spec_stable: + forall beh1 beh2, behavior_improves beh1 beh2 -> spec beh1 -> spec beh2. -Theorem asm_exec_program_deterministic: - forall p beh1 beh2, - exec_asm_program p beh1 -> exec_asm_program p beh2 -> - beh1 = beh2. +Theorem transf_c_program_preserves_spec: + forall p tp, + transf_c_program p = OK tp -> + (forall beh, program_behaves (Csem.semantics p) beh -> spec beh) -> + (forall beh, program_behaves (Asm.semantics tp) beh -> spec beh). Proof. - intros. hnf in H; hnf in H0. - eapply (program_behaves_deterministic _ _ - (wstep _ _ step) - (winitial_state _ (initial_state p) initial_world) - (wfinal_state _ final_state)); - eauto. - apply wstep_deterministic. apply step_internal_deterministic. - apply winitial_state_determ. apply initial_state_deterministic. - apply wfinal_state_determ. apply final_state_deterministic. - apply wfinal_state_nostep. apply final_state_not_step. + intros. + exploit transf_c_program_preservation; eauto. intros [beh' [A B]]. + apply spec_stable with beh'; auto. Qed. -(** * Additional semantic preservation property *) +End SPECS_PRESERVED. + +(** As a corollary, we obtain preservation of safety specifications: + specifications that exclude "going wrong" behaviors. *) -(** Combining the semantic preservation theorem from module [Compiler] - with the determinism of Asm executions, we easily obtain - additional, stronger semantic preservation properties. - The first property states that, when compiling a Compcert C - program that has well-defined semantics, all possible executions - of the resulting Asm code correspond to an execution of - the source program. *) +Section SAFETY_PRESERVED. -Theorem transf_c_program_is_refinement: +Variable spec: program_behavior -> Prop. + +Hypothesis spec_safety: + forall beh, spec beh -> not_wrong beh. + +Theorem transf_c_program_preserves_safety_spec: forall p tp, transf_c_program p = OK tp -> - (forall beh, exec_C_program p beh -> not_wrong beh) -> - (forall beh, exec_asm_program tp beh -> exec_C_program p beh). + (forall beh, program_behaves (Csem.semantics p) beh -> spec beh) -> + (forall beh, program_behaves (Asm.semantics tp) beh -> spec beh). Proof. - intros. - exploit Cstrategy.strategy_behavior. - apply notwrong_safeprog. eauto. - intros [beh1 [A [B [C D]]]]. - assert (Asm.exec_program tp beh1). - eapply transf_c_program_correct; eauto. - assert (exec_asm_program tp beh1). - red. apply inject_behaviors; auto. - assert (beh = beh1). eapply asm_exec_program_deterministic; eauto. - subst beh. - red. apply inject_behaviors; auto. + intros. eapply transf_c_program_preserves_spec; eauto. + intros. destruct H2. congruence. destruct H2 as [t [EQ1 EQ2]]. + subst beh1. elim (spec_safety _ H3). Qed. -Section SPECS_PRESERVED. +End SAFETY_PRESERVED. -(** The second additional results shows that if one execution - of the source C program satisfies a given specification - (a predicate on the observable behavior of the program), - then all executions of the produced Asm program satisfy - this specification as well. *) +(** We also have preservation of liveness specifications: + specifications that assert the existence of a prefix of the observable + trace satisfying some conditions. *) -Variable spec: program_behavior -> Prop. +Section LIVENESS_PRESERVED. -Hypothesis spec_not_wrong: forall b, spec b -> not_wrong b. +Variable spec: trace -> Prop. -Theorem transf_c_program_preserves_spec: +Definition liveness_spec_satisfied (b: program_behavior) : Prop := + exists t, behavior_prefix t b /\ spec t. + +Theorem transf_c_program_preserves_liveness_spec: forall p tp, transf_c_program p = OK tp -> - (forall beh, exec_C_program p beh -> spec beh) -> - (forall beh, exec_asm_program tp beh -> spec beh). + (forall beh, program_behaves (Csem.semantics p) beh -> liveness_spec_satisfied beh) -> + (forall beh, program_behaves (Asm.semantics tp) beh -> liveness_spec_satisfied beh). Proof. - intros. apply H0. apply transf_c_program_is_refinement with tp; auto. + intros. eapply transf_c_program_preserves_spec; eauto. + intros. destruct H3 as [t1 [A B]]. destruct H2. + subst. exists t1; auto. + destruct H2 as [t [C D]]. subst. + destruct A as [b1 E]. destruct D as [b2 F]. + destruct b1; simpl in E; inv E. + exists t1; split; auto. + exists (behavior_app t0 b2); apply behavior_app_assoc. Qed. -End SPECS_PRESERVED. - -End WORLD. +End LIVENESS_PRESERVED. @@ -788,6 +788,69 @@ Inductive final_state: state -> int -> Prop := rs#EAX = Vint r -> final_state (State rs m) r. -Definition exec_program (p: program) (beh: program_behavior) : Prop := - program_behaves step (initial_state p) final_state (Genv.globalenv p) beh. +Definition semantics (p: program) := + Semantics step (initial_state p) final_state (Genv.globalenv p). +(** Determinacy of the [Asm] semantics. *) + +Remark extcall_arguments_determ: + forall rs m sg args1 args2, + extcall_arguments rs m sg args1 -> extcall_arguments rs m sg args2 -> args1 = args2. +Proof. + intros until m. + assert (forall ll vl1, list_forall2 (extcall_arg rs m) ll vl1 -> + forall vl2, list_forall2 (extcall_arg rs m) ll vl2 -> vl1 = vl2). + induction 1; intros vl2 EA; inv EA. + auto. + f_equal; auto. + inv H; inv H3; congruence. + intros. red in H0; red in H1. eauto. +Qed. + +Remark annot_arguments_determ: + forall rs m params args1 args2, + annot_arguments rs m params args1 -> annot_arguments rs m params args2 -> args1 = args2. +Proof. + unfold annot_arguments. intros. revert params args1 H args2 H0. + induction 1; intros. + inv H0; auto. + inv H1. decEq; eauto. inv H; inv H4. auto. congruence. +Qed. + +Lemma semantics_determinate: forall p, determinate (semantics p). +Proof. +Ltac Equalities := + match goal with + | [ H1: ?a = ?b, H2: ?a = ?c |- _ ] => + rewrite H1 in H2; inv H2; Equalities + | _ => idtac + end. + intros; constructor; simpl; intros. +(* determ *) + inv H; inv H0; Equalities. + split. constructor. auto. + discriminate. + discriminate. + inv H11. + exploit external_call_determ. eexact H4. eexact H11. intros [A B]. + split. auto. intros. destruct B; auto. subst. auto. + inv H12. + assert (vargs0 = vargs) by (eapply annot_arguments_determ; eauto). subst vargs0. + exploit external_call_determ. eexact H5. eexact H13. intros [A B]. + split. auto. intros. destruct B; auto. subst. auto. + assert (args0 = args) by (eapply extcall_arguments_determ; eauto). subst args0. + exploit external_call_determ. eexact H3. eexact H8. intros [A B]. + split. auto. intros. destruct B; auto. subst. auto. +(* trace length *) + inv H; simpl. + omega. + eapply external_call_trace_length; eauto. + eapply external_call_trace_length; eauto. + eapply external_call_trace_length; eauto. +(* initial states *) + inv H; inv H0. f_equal. congruence. +(* final no step *) + inv H. unfold Vzero in H0. red; intros; red; intros. inv H; congruence. +(* final states *) + inv H; inv H0. congruence. +Qed. diff --git a/ia32/Asmgenproof.v b/ia32/Asmgenproof.v index a9b9f3b..d049737 100644 --- a/ia32/Asmgenproof.v +++ b/ia32/Asmgenproof.v @@ -1294,11 +1294,10 @@ Proof. Qed. Theorem transf_program_correct: - forall (beh: program_behavior), not_wrong beh -> - Machsem.exec_program prog beh -> Asm.exec_program tprog beh. + forward_simulation (Machsem.semantics prog) (Asm.semantics tprog). Proof. - unfold Machsem.exec_program, Asm.exec_program; intros. - eapply simulation_star_preservation with (measure := measure); eauto. + eapply forward_simulation_star with (measure := measure). + eexact symbols_preserved. eexact transf_initial_states. eexact transf_final_states. exact transf_instr_correct. diff --git a/lib/Coqlib.v b/lib/Coqlib.v index f4d50e8..87b19ca 100644 --- a/lib/Coqlib.v +++ b/lib/Coqlib.v @@ -1285,3 +1285,46 @@ Qed. End DECIDABLE_PREDICATE. +(** * Well-founded orderings *) + +Require Import Relations. + +(** A non-dependent version of lexicographic ordering. *) + +Section LEX_ORDER. + +Variable A: Type. +Variable B: Type. +Variable ordA: A -> A -> Prop. +Variable ordB: B -> B -> Prop. + +Inductive lex_ord: A*B -> A*B -> Prop := + | lex_ord_left: forall a1 b1 a2 b2, + ordA a1 a2 -> lex_ord (a1,b1) (a2,b2) + | lex_ord_right: forall a b1 b2, + ordB b1 b2 -> lex_ord (a,b1) (a,b2). + +Lemma wf_lex_ord: + well_founded ordA -> well_founded ordB -> well_founded lex_ord. +Proof. + intros Awf Bwf. + assert (forall a, Acc ordA a -> forall b, Acc ordB b -> Acc lex_ord (a, b)). + induction 1. induction 1. constructor; intros. inv H3. + apply H0. auto. apply Bwf. + apply H2; auto. + red; intros. destruct a as [a b]. apply H; auto. +Qed. + +Lemma transitive_lex_ord: + transitive _ ordA -> transitive _ ordB -> transitive _ lex_ord. +Proof. + intros trA trB; red; intros. + inv H; inv H0. + left; eapply trA; eauto. + left; auto. + left; auto. + right; eapply trB; eauto. +Qed. + +End LEX_ORDER. + diff --git a/powerpc/Asm.v b/powerpc/Asm.v index 7ae5112..321b074 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -914,6 +914,69 @@ Inductive final_state: state -> int -> Prop := rs#GPR3 = Vint r -> final_state (State rs m) r. -Definition exec_program (p: program) (beh: program_behavior) : Prop := - program_behaves step (initial_state p) final_state (Genv.globalenv p) beh. +Definition semantics (p: program) := + Semantics step (initial_state p) final_state (Genv.globalenv p). +(** Determinacy of the [Asm] semantics. *) + +Remark extcall_arguments_determ: + forall rs m sg args1 args2, + extcall_arguments rs m sg args1 -> extcall_arguments rs m sg args2 -> args1 = args2. +Proof. + intros until m. + assert (forall ll vl1, list_forall2 (extcall_arg rs m) ll vl1 -> + forall vl2, list_forall2 (extcall_arg rs m) ll vl2 -> vl1 = vl2). + induction 1; intros vl2 EA; inv EA. + auto. + f_equal; auto. + inv H; inv H3; congruence. + intros. red in H0; red in H1. eauto. +Qed. + +Remark annot_arguments_determ: + forall rs m params args1 args2, + annot_arguments rs m params args1 -> annot_arguments rs m params args2 -> args1 = args2. +Proof. + unfold annot_arguments. intros. revert params args1 H args2 H0. + induction 1; intros. + inv H0; auto. + inv H1. decEq; eauto. inv H; inv H4. auto. congruence. +Qed. + +Lemma semantics_determinate: forall p, determinate (semantics p). +Proof. +Ltac Equalities := + match goal with + | [ H1: ?a = ?b, H2: ?a = ?c |- _ ] => + rewrite H1 in H2; inv H2; Equalities + | _ => idtac + end. + intros; constructor; simpl; intros. +(* determ *) + inv H; inv H0; Equalities. + split. constructor. auto. + discriminate. + discriminate. + inv H11. + exploit external_call_determ. eexact H4. eexact H11. intros [A B]. + split. auto. intros. destruct B; auto. subst. auto. + inv H12. + assert (vargs0 = vargs) by (eapply annot_arguments_determ; eauto). subst vargs0. + exploit external_call_determ. eexact H5. eexact H13. intros [A B]. + split. auto. intros. destruct B; auto. subst. auto. + assert (args0 = args) by (eapply extcall_arguments_determ; eauto). subst args0. + exploit external_call_determ. eexact H3. eexact H8. intros [A B]. + split. auto. intros. destruct B; auto. subst. auto. +(* trace length *) + inv H; simpl. + omega. + eapply external_call_trace_length; eauto. + eapply external_call_trace_length; eauto. + eapply external_call_trace_length; eauto. +(* initial states *) + inv H; inv H0. f_equal. congruence. +(* final no step *) + inv H. unfold Vzero in H0. red; intros; red; intros. inv H; congruence. +(* final states *) + inv H; inv H0. congruence. +Qed. diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v index 1d270e5..d22bc3d 100644 --- a/powerpc/Asmgenproof.v +++ b/powerpc/Asmgenproof.v @@ -1514,11 +1514,10 @@ Proof. Qed. Theorem transf_program_correct: - forall (beh: program_behavior), not_wrong beh -> - Machsem.exec_program prog beh -> Asm.exec_program tprog beh. + forward_simulation (Machsem.semantics prog) (Asm.semantics tprog). Proof. - unfold Machsem.exec_program, Asm.exec_program; intros. - eapply simulation_star_preservation with (measure := measure); eauto. + eapply forward_simulation_star with (measure := measure). + eexact symbols_preserved. eexact transf_initial_states. eexact transf_final_states. exact transf_instr_correct. |