From 9a2e4b47521fb5cfd7f7b5915f64580a303d0b90 Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Wed, 27 Jan 2016 16:31:51 +0100
Subject: [PATCH] prove the very first Coq-verified iris Hoare Triple :)

---
 barrier/lifting.v | 47 ++++++++++++++++++++++++++++++---------------
 barrier/tests.v   | 49 ++++++++++++++++++++++++++++++++++++++---------
 2 files changed, 72 insertions(+), 24 deletions(-)

diff --git a/barrier/lifting.v b/barrier/lifting.v
index 9a1811ab9..43a1f3c3e 100644
--- a/barrier/lifting.v
+++ b/barrier/lifting.v
@@ -1,5 +1,5 @@
 Require Import prelude.gmap iris.lifting.
-Require Export barrier.parameter.
+Require Export iris.weakestpre barrier.parameter.
 Import uPred.
 
 (* TODO RJ: Figure out a way to to always use our Σ. *)
@@ -43,19 +43,20 @@ Qed.
 
 (* TODO RJ: Figure out some better way to make the
    postcondition a predicate over a *location* *)
-Lemma wp_alloc E σ v:
-  ownP (Σ:=Σ) σ ⊑ wp (Σ:=Σ) E (Alloc (v2e v))
+Lemma wp_alloc E σ e v:
+  e2v e = Some v →
+  ownP (Σ:=Σ) σ ⊑ wp (Σ:=Σ) E (Alloc e)
        (λ v', ∃ l, ■(v' = LocV l ∧ σ !! l = None) ∧ ownP (Σ:=Σ) (<[l:=v]>σ)).
 Proof.
   (* RJ FIXME (also for most other lemmas in this file): rewrite would be nicer... *)
-  etransitivity; last eapply wp_lift_step with (σ1 := σ)
+  intros Hvl. etransitivity; last eapply wp_lift_step with (σ1 := σ)
     (φ := λ e' σ', ∃ l, e' = Loc l ∧ σ' = <[l:=v]>σ ∧ σ !! l = None);
     last first.
   - intros e2 σ2 ef Hstep. inversion_clear Hstep. split; first done.
-    rewrite v2v in Hv. inversion_clear Hv.
+    rewrite Hv in Hvl. inversion_clear Hvl.
     eexists; split_ands; done.
   - set (l := fresh $ dom (gset loc) σ).
-    exists (Loc l), ((<[l:=v]>)σ), None. eapply AllocS; first by rewrite v2v.
+    exists (Loc l), ((<[l:=v]>)σ), None. eapply AllocS; first done.
     apply (not_elem_of_dom (D := gset loc)). apply is_fresh.
   - reflexivity.
   - reflexivity.
@@ -79,7 +80,7 @@ Proof.
     (φ := λ e' σ', e' = v2e v ∧ σ' = σ); last first.
   - intros e2 σ2 ef Hstep. move: Hl. inversion_clear Hstep=>{σ}.
     rewrite Hlookup. case=>->. done.
-  - do 3 eexists. eapply LoadS; eassumption.
+  - do 3 eexists. econstructor; eassumption.
   - reflexivity.
   - reflexivity.
   - rewrite -pvs_intro. rewrite -{1}[ownP σ](@right_id _ _ _ _ uPred.sep_True).
@@ -92,16 +93,17 @@ Proof.
     + done.
 Qed.
 
-Lemma wp_store E σ l v v':
+Lemma wp_store E σ l e v v':
+  e2v e = Some v →
   σ !! l = Some v' →
-  ownP (Σ:=Σ) σ ⊑ wp (Σ:=Σ) E (Store (Loc l) (v2e v))
-       (λ v', ■(v' = LitVUnit) ∧ ownP (Σ:=Σ) (<[l:=v]>σ)).
+  ownP (Σ:=Σ) σ ⊑ wp (Σ:=Σ) E (Store (Loc l) e)
+       (λ v', ■(v' = LitUnitV) ∧ ownP (Σ:=Σ) (<[l:=v]>σ)).
 Proof.
-  intros Hl. etransitivity; last eapply wp_lift_step with (σ1 := σ)
+  intros Hvl Hl. etransitivity; last eapply wp_lift_step with (σ1 := σ)
     (φ := λ e' σ', e' = LitUnit ∧ σ' = <[l:=v]>σ); last first.
   - intros e2 σ2 ef Hstep. move: Hl. inversion_clear Hstep=>{σ2}.
-    rewrite v2v in Hv. inversion_clear Hv. done.
-  - do 3 eexists. eapply StoreS; last (eexists; eassumption). by rewrite v2v.
+    rewrite Hvl in Hv. inversion_clear Hv. done.
+  - do 3 eexists. eapply StoreS; last (eexists; eassumption). eassumption.
   - reflexivity.
   - reflexivity.
   - rewrite -pvs_intro. rewrite -{1}[ownP σ](@right_id _ _ _ _ uPred.sep_True).
@@ -117,7 +119,7 @@ Qed.
 (** Base axioms for core primitives of the language: Stateless reductions *)
 
 Lemma wp_fork E e :
-  ▷ wp (Σ:=Σ) coPset_all e (λ _, True) ⊑ wp (Σ:=Σ) E (Fork e) (λ _, True).
+  ▷ wp (Σ:=Σ) coPset_all e (λ _, True) ⊑ wp (Σ:=Σ) E (Fork e) (λ v, ■(v = LitUnitV)).
 Proof.
   etransitivity; last eapply wp_lift_pure_step with
     (φ := λ e' ef, e' = LitUnit ∧ ef = Some e);
@@ -136,7 +138,8 @@ Proof.
     transitivity (True ★ wp coPset_all e (λ _ : ival Σ, True))%I;
       first by rewrite left_id.
     apply sep_mono; last reflexivity.
-    rewrite -wp_value'; reflexivity.
+    rewrite -wp_value'; last reflexivity.
+    by apply const_intro.
 Qed.
 
 Lemma wp_lift_pure_step E (φ : expr → Prop) Q e1 :
@@ -185,3 +188,17 @@ Proof.
   by asimpl.
 Qed.
 
+Lemma wp_plus n1 n2 E P Q :
+  P ⊑ Q (LitNatV (n1 + n2)) →
+  ▷P ⊑ wp (Σ:=Σ) E (Plus (LitNat n1) (LitNat n2)) Q.
+Proof.
+  intros HP.
+  etransitivity; last eapply wp_lift_pure_step with
+    (φ := λ e', e' = LitNat (n1 + n2)); last first.
+  - intros ? ? ? ? Hstep. inversion_clear Hstep; done.
+  - intros ?. do 3 eexists. econstructor.
+  - reflexivity.
+  - apply later_mono, forall_intro=>e2. apply impl_intro_l.
+    apply const_elim_l=>->.
+    rewrite -wp_value'; last reflexivity; done.
+Qed.
diff --git a/barrier/tests.v b/barrier/tests.v
index 1cf752f2a..f00b22461 100644
--- a/barrier/tests.v
+++ b/barrier/tests.v
@@ -1,25 +1,25 @@
 (** This file is essentially a bunch of testcases. *)
-Require Import modures.base.
-Require Import barrier.parameter.
+Require Import modures.logic.
+Require Import barrier.lifting.
+Import uPred.
 
 Module LangTests.
-  Definition add := Op2 plus (Lit 21) (Lit 21).
-
-  Goal ∀ σ, prim_step add σ (Lit 42) σ None.
+  Definition add :=  Plus (LitNat 21) (LitNat 21).
+  Goal ∀ σ, prim_step add σ (LitNat 42) σ None.
   Proof.
-    apply Op2S.
+    constructor.
   Qed.
 
   Definition rec := Rec (App (Var 0) (Var 1)). (* fix f x => f x *)
-  Definition rec_app := App rec (Lit 0).
+  Definition rec_app := App rec (LitNat 0).
   Goal ∀ σ, prim_step rec_app σ rec_app σ None.
   Proof.
     move=>?. eapply BetaS.
     reflexivity.
   Qed.
 
-  Definition lam := Lam (Op2 plus (Var 0) (Lit 21)).
-  Goal ∀ σ, prim_step (App lam (Lit 21)) σ add σ None.
+  Definition lam := Lam (Plus (Var 0) (LitNat 21)).
+  Goal ∀ σ, prim_step (App lam (LitNat 21)) σ add σ None.
   Proof.
     move=>?. eapply BetaS. reflexivity.
   Qed.
@@ -28,3 +28,34 @@ End LangTests.
 Module ParamTests.
   Print Assumptions Σ.
 End ParamTests.
+
+Module LiftingTests.
+  (* TODO RJ: Some syntactic sugar for language expressions would be nice. *)
+  Definition e3 := Load (Var 0).
+  Definition e2 := Seq (Store (Var 0) (Plus (Load (Var 0)) (LitNat 1))) e3.
+  Definition e := Let (Alloc (LitNat 1)) e2.
+  Goal ∀ σ E, (ownP (Σ:=Σ) σ) ⊑ (wp (Σ:=Σ) E e (λ v, ■(v = LitNatV 2))).
+  Proof.
+    move=> σ E. rewrite /e.
+    rewrite -(wp_bind _ _ (LetCtx EmptyCtx e2)). rewrite -wp_mono.
+    { eapply wp_alloc; done. }
+    move=>v; apply exist_elim=>l. apply const_elim_l; move=>[-> _] {v}.
+    rewrite (later_intro (ownP _)); apply wp_lam. asimpl.
+    rewrite -(wp_bind _ _ (SeqCtx (StoreRCtx (LocV _)
+                                   (PlusLCtx EmptyCtx _)) (Load (Loc _)))).
+    rewrite -wp_mono.
+    { eapply wp_load. apply: lookup_insert. } (* RJ TODO: figure out why apply and eapply fail. *)
+    move=>v; apply const_elim_l; move=>-> {v}.
+    rewrite -(wp_bind _ _ (SeqCtx (StoreRCtx (LocV _) EmptyCtx) (Load (Loc _)))).
+    rewrite (later_intro (ownP _)); apply wp_plus.
+    rewrite -(wp_bind _ _ (SeqCtx EmptyCtx (Load (Loc _)))).
+    rewrite -wp_mono.
+    { eapply wp_store; first reflexivity. apply: lookup_insert. }
+    move=>v; apply const_elim_l; move=>-> {v}.
+    rewrite (later_intro (ownP _)); apply wp_lam. asimpl.
+    rewrite -wp_mono.
+    { eapply wp_load. apply: lookup_insert. }
+    move=>v; apply const_elim_l; move=>-> {v}.
+    by apply const_intro.
+  Qed.
+End LiftingTests.
-- 
GitLab