Section Toy. Require Import Utf8. Parameter mem: Type. Parameter base: Type. Parameter sem_base: mem → base → mem → Prop. Inductive prog: Type := | pskip | pbreak | pbase (b: base): prog | pseq (p1 p2: prog): prog | palt (p1 p2: prog): prog | ploop (p: prog): prog . Inductive cont: Type := | kstop | kseq (p: prog) (k: cont) | kloop (p: prog) (k: cont) . Definition config: Type := (mem * prog * cont) %type. Definition memof (c: config) := fst (fst c). Reserved Notation "a ↦ b" (at level 60). Inductive step: config → config → Prop := | sbase b m1 m2 k (BASE: sem_base m1 b m2) : (m1, pbase b, k) ↦ (m2, pskip, k) | sseq1 p1 p2 m k : (m, pseq p1 p2, k) ↦ (m, p1, kseq p2 k) | sseq2 p m k : (m, pskip, kseq p k) ↦ (m, p, k) | sseq3 p m k : (m, pbreak, kseq p k) ↦ (m, pbreak, k) | salt1 p1 p2 m k : (m, palt p1 p2, k) ↦ (m, p1, k) | salt2 p1 p2 m k : (m, palt p1 p2, k) ↦ (m, p2, k) | sloop1 p m k : (m, ploop p, k) ↦ (m, p, kloop p k) | sloop2 p m k : (m, pskip, kloop p k) ↦ (m, ploop p, k) | sloop3 p m k : (m, pbreak, kloop p k) ↦ (m, pskip, k) where "a ↦ b" := (step a b). Definition assn: Type := mem → Prop. Definition bottom: assn := λ _, False. (* I is an invariant *) Parameter I: assn. Inductive triple: assn → prog → assn → assn → Prop := | tskip (A: assn) : triple (A) (pskip) (A) (bottom) | tbreak (B: assn) : triple (B) (pbreak) (bottom) (B) | tbase b (A: assn) : triple (λ m, ∀ m', sem_base m b m' → A m' ∧ I m') (pbase b) (A) (bottom) | tseq p1 p2 (A1 A2 A3 B: assn) (P1: triple A1 p1 A2 B) (P2: triple A2 p2 A3 B) : triple (A1) (pseq p1 p2) (A3) (B) | talt p1 p2 (A1 A2 B: assn) (P1: triple A1 p1 A2 B) (P2: triple A1 p2 A2 B) : triple (A1) (palt p1 p2) (A2) (B) | tloop p (A1 A2: assn) (P: triple A1 p A1 A2) : triple (A1) (ploop p) (A2) (bottom) | tweak p (A1 A2 B A1' A2' B': assn) (P: triple A1 p A2 B) (PRE: ∀ m, A1' m → A1 m) (PST: ∀ m, A2 m → A2' m) (BRK: ∀ m, B m → B' m) : triple (A1') p (A2') (B') . (* Safety of configurations. *) Definition spec: Type := nat → config → Prop. Inductive safe: spec := | safe0 c: safe 0 c | safeN n c (SAFE: ∀ c' (STEP: c ↦ c') (INV: I (memof c)), safe n c' ∧ I (memof c')) : safe (S n) c . Require Import Arith. Require Import Omega. Section SafeRemarks. Inductive multi: config → config → Prop := | multi0 c: multi c c | multiN c c₁ c₂: c ↦ c₁ → multi c₁ c₂ → multi c c₂ . (* safety expresses the preservation of * invariants, during a given number of * steps *) Theorem safe_preserve: ∀ c c₁ (MULT: multi c c₁) (IINI: I (memof c)) (SAFE: ∀ n, safe n c), I (memof c₁). Proof. induction 1; intros. - assumption. - apply IHMULT. + generalize (SAFE 1). clear SAFE. inversion_clear 1. apply SAFE; assumption. + intros. generalize (SAFE (S n)). clear SAFE. inversion_clear 1. apply SAFE; assumption. Qed. (* safe is downward closed *) Lemma safe_le: ∀ n c (SAFE: safe n c) n' (LE: n' ≤ n), safe n' c. Proof. induction n as [|n IND]; intros. - inversion_clear LE. apply safe0. - destruct n' as [|n']. + apply safe0. + inversion SAFE; subst. apply safeN. intros. split. * apply IND; auto with arith. apply SAFE0; assumption. * apply SAFE0; assumption. Qed. End SafeRemarks. Definition valid (A1: assn) p (A2 B: assn) := ∀ n k (SAFES: ∀ m, A2 m → safe n (m, pskip, k)) (SAFEB: ∀ m, B m → safe n (m, pbreak, k)) m (MOK: A1 m), safe n (m, p, k). (* Soundness: triple → valid *) Lemma valid_skip (A: assn): valid (A) (pskip) (A) (bottom). Proof. unfold valid; intros. apply SAFES, MOK. Qed. Lemma valid_break (B: assn): valid (B) (pbreak) (bottom) (B). Proof. unfold valid; intros. apply SAFEB, MOK. Qed. Ltac step := match goal with | [ |- safe ?n _ ] => destruct n; [ apply safe0 | apply safeN; inversion_clear 1; intros; split; try assumption ] end. Ltac ale H := eapply safe_le; [apply H|]; try omega. Lemma valid_base b (A: assn): valid (λ m, ∀ m', sem_base m b m' → A m' ∧ I m') (pbase b) (A) (bottom). Proof. unfold valid; intros. step. - ale SAFES. apply MOK, BASE. - apply MOK, BASE. Qed. Lemma valid_seq p1 p2 A1 A2 A3 B (VALID1: valid (A1) (p1) (A2) (B)) (VALID2: valid (A2) (p2) (A3) (B)): valid (A1) (pseq p1 p2) (A3) (B). Proof with (omega || eauto); intros. unfold valid; intros. step. apply VALID1... - step. apply VALID2... + ale SAFES; assumption. + ale SAFEB; assumption. - step. ale SAFEB; assumption. Qed. Lemma valid_alt p1 p2 A1 A2 B (VALID1: valid (A1) (p1) (A2) (B)) (VALID2: valid (A1) (p2) (A2) (B)): valid (A1) (palt p1 p2) (A2) (B). Proof with (omega || eauto). unfold valid; intros. step. - ale VALID1... - ale VALID2... Qed. Lemma valid_loop p A1 A2 (VALID: valid (A1) (p) (A1) (A2)): valid (A1) (ploop p) (A2) (bottom). Proof. red. induction n as [n IND] using lt_wf_rec. intros. step. apply VALID; (omega || eauto). - intros. step. clear INV0. eapply (IND n); (omega || eauto). intros; ale SAFES; assumption. intros; ale SAFEB; assumption. - intros. step. ale SAFES; eauto. Qed. Lemma valid_weak p (A1 A2 B A1' A2' B': assn) (P: valid (A1) (p) (A2) (B)) (PRE: ∀ m, A1' m → A1 m) (PST: ∀ m, A2 m → A2' m) (BRK: ∀ m, B m → B' m): valid (A1') (p) (A2') (B'). Proof. unfold valid; intros. apply P; (omega || eauto). Qed. Theorem soundness A1 p A2 B: triple (A1) (p) (A2) (B) → valid (A1) (p) (A2) (B). Proof. induction 1; intros; eauto using valid_skip, valid_break, valid_base, valid_seq, valid_alt, valid_loop, valid_weak. Qed. (* Completeness: safe → triple *) Ltac pets H := (* step, inverted *) match goal with | [ |- safe ?n _ ] => generalize (H (S n)); clear H; inversion 1 as [|n__ c__ SAFE]; subst; apply SAFE; [ constructor | assumption ] end. Definition mgt p := ∀ k, triple (λ m, I m ∧ ∀ n, safe n (m, p, k)) (p) (λ m, I m ∧ ∀ n, safe n (m, pskip, k)) (λ m, I m ∧ ∀ n, safe n (m, pbreak, k)). Lemma mgt_skip: mgt (pskip). Proof. intro. eapply tweak; eauto using tskip. - intros. exact H. - eauto. - firstorder. Qed. Lemma mgt_break: mgt (pbreak). Proof. intro. eapply tweak; eauto using tbreak. - intros. exact H. - firstorder. - eauto. Qed. Lemma mgt_base b: mgt (pbase b). Proof. intro. eapply tweak; eauto using tbase. - instantiate (1 := (λ m, I m ∧ ∀ n, safe n (m, pskip, k))). simpl. intros. assert (I m'). { replace m' with (memof (m', pskip, k)) by reflexivity. destruct H. apply (safe_preserve (m, pbase b, k) (m', pskip, k)); repeat (eauto; econstructor). } intuition. pets H3; assumption. - simpl; eauto. - firstorder. Qed. Lemma mgt_seq p1 p2 (MGT1: mgt p1) (MGT2: mgt p2): mgt (pseq p1 p2). Proof. intro. eapply tseq. - generalize (MGT1 (kseq p2 k)). clear MGT1 MGT2. intro MGT1. eapply tweak; eauto. + simpl. intuition. pets H1. + simpl. intuition. pets H1. - generalize (MGT2 k). clear MGT1 MGT2. intro MGT2. eapply tweak; eauto; simpl; eauto. simpl. intuition. pets H1. Qed. Lemma mgt_alt p1 p2 (MGT1: mgt p1) (MGT2: mgt p2): mgt (palt p1 p2). Proof. intro. eapply talt. - generalize (MGT1 k). clear MGT1 MGT2. intro MGT. eapply tweak; eauto. simpl. intuition. pets H1. - (* same proof *) generalize (MGT2 k). clear MGT1 MGT2. intro MGT. eapply tweak; eauto. simpl. intuition. pets H1. Qed. Lemma mgt_loop p (MGT: mgt p): mgt (ploop p). Proof. intro. eapply tweak. apply tloop. generalize (MGT (kloop p k)). clear MGT. intro MGT. eapply tweak; eauto. - simpl. intuition. assert (∀ n, safe n (m, ploop p, k)) by (intro; pets H1). pets H. - simpl. intuition. pets H1. - simpl. intuition. pets H1. - firstorder. Qed. Lemma key0: ∀ p, mgt p. Proof. induction p; eauto using mgt_skip, mgt_break, mgt_base, mgt_seq, mgt_alt, mgt_loop. Qed. Lemma key1 p (X: assn) (MGT: mgt p): (∀ m, X m → I m ∧ ∀ n, safe n (m, p, kstop)) → triple (X) p (λ _, True) (λ _, True). Proof. unfold mgt. intros VALIDX. eapply tweak; eauto. intuition. Qed. Theorem completeness p (X: assn): (∀ m, X m → I m ∧ ∀ n, safe n (m, p, kstop)) → triple (X) p (λ _, True) (λ _, True). Proof. eauto using key0, key1. Qed. End Toy.