Initial Commit - Implemented new chan, send and recv

.gitignore

+*.vo
+*.vio
+*.v.d
+.coqdeps.d
+*.glob
+*.cache
+*.aux
+\#*\#
+.\#*
+*~
+*.bak
+.coqdeps.d
+.coq-native/
+build-dep/
+Makefile.coq
+Makefile.coq.conf
+*.crashcoqide

Makefile

+# Forward most targets to Coq makefile (with some trick to make this phony)
+%: Makefile.coq phony
+	+@make -f Makefile.coq $@
+
+all: Makefile.coq
+	+@make -f Makefile.coq all
+.PHONY: all
+
+clean: Makefile.coq
+	+@make -f Makefile.coq clean
+	find theories tests \( -name "*.d" -o -name "*.vo" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete || true
+	rm -f Makefile.coq
+.PHONY: clean
+
+# Create Coq Makefile.
+Makefile.coq: _CoqProject Makefile
+	"$(COQBIN)coq_makefile" -f _CoqProject -o Makefile.coq
+
+# Install build-dependencies
+build-dep/opam: opam Makefile
+	@echo "# Creating build-dep package."
+	@mkdir -p build-dep
+	@sed <opam -E 's/^(build|install|remove):.*/\1: []/; s/^name: *"(.*)" */name: "\1-builddep"/' >build-dep/opam
+	@fgrep builddep build-dep/opam >/dev/null || (echo "sed failed to fix the package name" && exit 1) # sanity check
+
+build-dep: build-dep/opam phony
+	@# We want opam to not just instal the build-deps now, but to also keep satisfying these
+	@# constraints.  Otherwise, `opam upgrade` may well update some packages to versions
+	@# that are incompatible with our build requirements.
+	@# To achieve this, we create a fake opam package that has our build-dependencies as
+	@# dependencies, but does not actually install anything itself.
+	@echo "# Pinning build-dep package." && \
+	  if opam --version | grep "^1\." -q; then \
+	    BUILD_DEP_PACKAGE="$$(egrep "^name:" build-dep/opam | sed 's/^name: *"\(.*\)" */\1/')" && \
+	    opam pin add -k path $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE".dev build-dep && \
+	    opam reinstall $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE"; \
+	  else \
+	    opam install $(OPAMFLAGS) build-dep/; \
+	  fi
+
+# Some files that do *not* need to be forwarded to Makefile.coq
+Makefile: ;
+_CoqProject: ;
+opam: ;
+
+# Phony wildcard targets
+phony: ;
+.PHONY: phony

_CoqProject

+-Q theories osiris
+-arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
+theories/list.v
+theories/channel.v

theories/channel.v

+From iris.program_logic Require Export weakestpre.
+From iris.heap_lang Require Export lang.
+From iris.proofmode Require Import tactics.
+From iris.heap_lang Require Import proofmode notation.
+From iris.algebra Require Import excl.
+From iris.heap_lang.lib Require Import lock.
+From iris.heap_lang.lib Require Import spin_lock.
+From osiris Require Import list.
+Set Default Proof Using "Type".
+
+Definition new_list : val :=
+  λ: <>, lnil #().
+
+Definition new_chan : val := 
+  λ: <>,
+     let l := ref new_list #() in
+     let r := ref new_list #() in
+     let lk := newlock #() in
+     ((l,r),lk).
+
+Notation left := (#true) (only parsing).
+Notation right := (#false) (only parsing).
+
+Definition get_buffs c := Fst c.
+Definition get_left c := Fst (get_buffs c).
+Definition get_right c := Snd (get_buffs c).
+Definition get_lock c := Snd c.
+
+Definition dual_side s :=
+  (if: s = left then right else left)%E.
+
+Definition get_side c s :=
+  (if: s = left then (get_left c) else (get_right c))%E.
+
+Definition send : val :=
+  λ: "c" "s" "v",
+    let lk := get_lock "c" in
+    acquire lk;;
+    let l := get_side "c" "s" in
+    l <- lsnoc !l "v";;
+    release lk.
+
+Definition try_recv : val :=
+  λ: "c" "s",
+    let lk := get_lock "c" in
+    acquire lk;;
+    let l := (get_side "c" (dual_side "s")) in
+    let v :=
+        match: !l with
+          SOME "p" => l <- Snd "p";; SOME (Fst "p")
+        | NONE => NONE
+        end in
+    release lk;;
+    v.
+
+Definition recv : val :=
+  rec: "go" "c" "s" :=
+    match: try_recv "c" "s" with
+      SOME "p" => "p"
+    | NONE => "go" "c" "s"
+    end.
+
+Section channel.
+  Context `{!heapG Σ, !lockG Σ} (N : namespace).
+  
+  Definition is_list_ref (l : val) (xs : list val) : iProp Σ :=
+    (∃ l':loc, ⌜l = #l'⌝ ∧ ∃ hd : val, l' ↦ hd ∗ ⌜is_list hd xs⌝)%I.
+
+  Definition is_side (s : val) : Prop :=
+    s = left ∨ s = right.
+    
+  Definition is_chan (γ : gname) (c : val) (ls rs : list val) (R : iProp Σ) : iProp Σ :=
+    (∃ l r lk : val, ⌜c = ((l, r), lk)%V⌝ ∧ is_lock N γ lk R ∗ is_list_ref l ls ∗ is_list_ref r rs)%I.
+
+  Lemma new_chan_spec (R : iProp Σ) :
+    {{{ R }}}
+      new_chan #()
+    {{{ c γ, RET c; is_chan γ c [] [] R }}}.
+  Proof. 
+    iIntros (Φ) "HR HΦ". rewrite -wp_fupd /newlock /new_list /=.
+    repeat wp_lam. 
+    wp_alloc lk as "Hlk".
+    repeat wp_lam. 
+    wp_alloc r as "Hr".
+    repeat wp_lam. 
+    wp_alloc l as "Hl".
+    wp_pures.
+    iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done.
+    iMod (inv_alloc N _ (lock_inv γ lk R) with "[-Hl Hr HΦ]") as "#?".
+    { iIntros "!>". iExists false. by iFrame. }
+    iModIntro.
+    iApply "HΦ".
+    iExists _, _, _.
+    iSplit=> //.
+    iSplitR.
+    - unfold is_lock. iExists _. iSplit=> //.
+    - iSplitL "Hl".
+      + iExists l. iSplit=> //. iExists (InjLV #()). iSplit => //.
+      + iExists r. iSplit=> //. iExists (InjLV #()). iSplit => //.
+  Qed.
+
+  Definition send_upd γ c ls rs R s v : iProp Σ :=
+    match s with
+    | #true  => is_chan γ c (ls ++ [v]) rs R
+    | #false => is_chan γ c ls (rs ++ [v]) R
+    | _ => ⌜False⌝%I
+    end.
+
+  Lemma send_spec (γ : gname) (c v : val) (ls rs : list val) (s : val) (R : iProp Σ) :
+    {{{ is_chan γ c ls rs R ∗ ⌜is_side s⌝%I }}}
+      send c s v
+    {{{ RET #(); send_upd γ c ls rs R s v }}}.
+  Proof.
+    iIntros (Φ) "[Hc #Hs] HΦ". 
+    iRevert "Hs". iIntros (Hs).
+    rewrite -wp_fupd /send /=.
+    iDestruct "Hc" as (l r lk Hc) "[#Hlk [Hl Hr]]".
+    wp_lam.
+    wp_pures.
+    subst.
+    wp_bind (Snd _). 
+    wp_pures.
+    wp_bind (acquire lk).
+    iApply acquire_spec=> //.
+    iNext.
+    iIntros "[Hlocked HR]".
+    wp_seq.
+    wp_pures.
+    inversion Hs. 
+    - iDestruct "Hl" as (ll Hl lhd) "[Hl #Hlhd]".
+      subst.
+      wp_pures.
+      wp_bind (lsnoc (Load #ll) v).
+      wp_load.
+      iApply lsnoc_spec=> //.
+      iIntros (hd' Hhd').
+      iNext.
+      wp_store.
+      wp_pures.
+      iApply (release_spec N γ lk R with "[Hlocked HR]") => //.
+      iFrame. eauto. 
+      iModIntro.
+      iIntros (_).
+      iModIntro.
+      iApply "HΦ".
+      iExists _, _, _.
+      iSplitR.
+      eauto.
+      iSplitL "Hlk"=> //.
+      iSplitL "Hl"=> //.
+      iExists _.
+      iSplitR.
+      eauto.
+      iExists _.
+      iSplitL=>//.      
+    - iDestruct "Hr" as (rl Hr rhd) "[Hr #Hrhd]".
+      subst.
+      wp_pures. 
+      wp_bind (lsnoc (Load #rl) v).
+      wp_load.
+      iApply lsnoc_spec=> //.
+      iIntros (hd' Hhd').
+      iNext.
+      wp_store.
+      wp_pures.
+      iApply (release_spec N γ lk R with "[Hlocked HR]") => //.
+      iFrame. eauto. 
+      iModIntro.
+      iIntros (_).
+      iModIntro.
+      iApply "HΦ".
+      iExists _, _, _.
+      iSplitR.
+      eauto.
+      iSplitL "Hlk"=> //.
+      iSplitL "Hl"=> //.
+      iExists _.
+      iSplitR.
+      eauto.
+      iExists _.
+      iSplitL=>//.
+  Qed.
+
+  (* Definition try_recv_upd γ c ls rs R s v : iProp Σ := *)
+  (*   match s with *)
+  (*   | left   => is_chan γ c ls rs R ∧ (∃ w rs', v = SOMEV w ∧ rs' = w::rs) ∨ (v = NONE ∧ rs = []) *)
+  (*   | right  => is_chan γ c ls rs R ∧ (∃ w ls', v = SOMEV w ∧ ls' = w::ls) ∨ (v = NONE ∧ ls = []) *)
+  (*   . *)
+
+  (*                         match v with *)
+  (*               | NONE => is_chan γ c ls rs R *)
+  (*               | SOMEV w => ∃ ls', ls = w::ls' ∧ is_chan γ c ls rs R *)
+  (*               end *)
+  (*   | right => match rs with *)
+  (*               | [] => is_chan γ c ls rs R *)
+  (*               | r::rs => is_chan γ c ls rs R *)
+  (*               end *)
+  (*   | _ => ⌜False⌝%I *)
+  (*   end. *)
+
+  Definition try_recv_upd γ c ls rs R s v : iProp Σ :=
+    match s with
+    | left => match v with
+              | NONEV => (is_chan γ c ls rs R ∧ ⌜rs = []⌝)%I
+              | SOMEV w => (∃ rs', is_chan γ c ls rs' R ∧ ⌜rs = w::rs'⌝)%I
+              | _ => ⌜False⌝%I
+              end
+    | right => match v with
+               | NONEV => (is_chan γ c ls rs R ∧ ⌜ls = []⌝)%I
+               | SOMEV w => (∃ ls', is_chan γ c ls' rs R ∧ ⌜ls = w::ls'⌝)%I
+               | _ => ⌜False⌝%I
+               end 
+    | _ => ⌜False⌝%I
+    end.
+
+  Lemma try_recv_spec (γ : gname) (c v s : val) (ls rs : list val) (R : iProp Σ) :
+    {{{ is_chan γ c ls rs R ∗ ⌜is_side s⌝%I }}}
+      try_recv c s
+    {{{ v, RET v;  try_recv_upd γ c ls rs R s v }}}.
+  Proof.
+    iIntros (Φ) "[Hc #Hs] HΦ". 
+    iRevert "Hs". iIntros (Hs).
+    rewrite -wp_fupd /send /=.
+    iDestruct "Hc" as (l r lk Hc) "[#Hlk [Hl Hr]]".
+    subst.
+    wp_lam.
+    wp_pures.
+    wp_bind (acquire _).
+    iApply acquire_spec=> //.
+    iNext.
+    iIntros "[Hlocked HR]".
+    wp_seq.
+    wp_bind (release _).
+    wp_bind (Snd _).
+    wp_pures.
+    iApply (release_spec N γ lk R with "[Hlocked HR]") => //.
+    iFrame. eauto.
+    iNext. iIntros (_).
+    wp_pures.
+    inversion Hs; subst.
+    - wp_pures.
+      iDestruct "Hr" as (rl Hr rhd) "[Hr #Hrhd]".
+      wp_pures.
+      subst.
+      wp_load.
+      iRevert "Hrhd". iIntros (Hrhd).
+      unfold is_list in Hrhd.
+      destruct rs.
+      + subst.
+        wp_pures.
+        iModIntro.
+        iApply "HΦ".
+        iSplit=> //.
+        iExists _, _, _.
+        iSplit=> //.
+        iFrame.
+        iSplitR. eauto.
+        iExists _.
+        iSplit=> //.
+        iExists _.
+        iSplit=> //.
+      + subst.
+        destruct Hrhd as [hd' [Hrhd Hrhd']].
+        subst.
+        wp_pures.
+        wp_store. wp_pures. iModIntro.
+        iApply "HΦ".
+        iExists _.
+        iSplit=> //.
+        iExists _, _, _.
+        iSplit=> //.
+        iSplit=> //.
+        iFrame. 
+        iExists _.
+        iSplit=>//.
+        iExists _.
+        iSplit=> //.
+    - wp_pures.
+      iDestruct "Hl" as (ll Hl lhd) "[Hl #Hlhd]".
+      wp_pures.
+      subst.
+      wp_load.
+      iRevert "Hlhd". iIntros (Hlhd).
+      unfold is_list in Hlhd.
+      destruct ls.
+      + subst.
+        wp_pures.
+        iModIntro.
+        iApply "HΦ".
+        iSplit=> //.
+        iExists _, _, _.
+        iSplit=> //.
+        iFrame.
+        iSplitR. eauto.
+        iExists _.
+        iSplit=> //.
+        iExists _.
+        iSplit=> //.
+      + subst.
+        destruct Hlhd as [hd' [Hlhd Hlhd']].
+        subst.
+        wp_pures.
+        wp_store. wp_pures. iModIntro.
+        iApply "HΦ".
+        iExists _.
+        iSplit=> //.
+        iExists _, _, _.
+        iSplit=> //.
+        iSplit=> //.
+        iFrame. 
+        iExists _.
+        iSplit=>//.
+        iExists _.
+        iSplit=> //.
+  Qed.
+
+  (* Lemma recv_spec (γ : gname) (c v s : val) (ls rs : list val) (R : iProp Σ) : *)
+  (*   {{{ is_chan γ c ls rs R ∗ ⌜is_side s⌝%I }}} *)
+  (*     recv c s *)
+  (*   {{{ v, RET v; *)
+  (*       match s with *)
+  (*       | left => match v with *)
+  (*                 | NONEV => is_chan γ c ls rs R ∧ ⌜rs = []⌝%I *)
+  (*                 | SOMEV w => ∃ rs', is_chan γ c ls rs' R ∧ ⌜rs = w::rs'⌝%I *)
+  (*                 | _ => False *)
+  (*                 end  *)
+  (*       | right => match v with *)
+  (*                 | NONEV => is_chan γ c ls rs R ∧ ⌜ls = []⌝%I *)
+  (*                 | SOMEV w => ∃ ls', is_chan γ c ls' rs R ∧ ⌜ls = w::ls'⌝%I *)
+  (*                 | _ => False *)
+  (*                 end  *)
+  (*       | _ => False *)
+  (*       end }}}. *)
+  (* Proof. *)
+  
+
+End channel.
\ No newline at end of file

theories/list.v

+From iris.heap_lang Require Export proofmode notation.
+From iris.heap_lang Require Import assert.
+
+(** Immutable ML-style functional lists *)
+Fixpoint is_list (hd : val) (xs : list val) : Prop :=
+  match xs with
+  | [] => hd = NONEV
+  | x :: xs => ∃ hd', hd = SOMEV (x,hd') ∧ is_list hd' xs
+  end.
+
+Definition lnil : val := λ: <>, NONEV.
+Definition lcons : val := λ: "x" "l", SOME ("x", "l").
+
+Definition lhead : val := λ: "l",
+  match: "l" with
+    SOME "p" => Fst "p"
+  | NONE => assert: #false
+  end.
+Definition ltail : val := λ: "l",
+  match: "l" with
+    SOME "p" => Snd "p"
+  | NONE => assert: #false
+  end.
+
+Definition llookup : val :=
+  rec: "go" "n" "l" :=
+    if: "n" = #0 then lhead "l" else
+    let: "l" := ltail "l" in "go" ("n" - #1) "l".
+
+Definition linsert : val :=
+  rec: "go" "n" "x" "l" :=
+    if: "n" = #0 then let: "l" := ltail "l" in lcons "x" "l" else
+    let: "k" := ltail "l" in
+    let: "k" := "go" ("n" - #1) "x" "k" in
+    lcons (lhead "l") "k".
+
+Definition lreplicate : val :=
+  rec: "go" "n" "x" :=
+    if: "n" = #0 then lnil #() else
+    let: "l" := "go" ("n" - #1) "x" in lcons "x" "l".
+
+Definition llist_member : val :=
+  rec: "go" "x" "l" :=
+    match: "l" with
+      NONE => #false
+    | SOME "p" =>
+      if: Fst "p" = "x" then #true
+      else let: "l" := (Snd "p")  in "go" "x" "l"
+    end.
+
+Definition llength : val :=
+  rec: "go" "l" :=
+    match: "l" with
+      NONE => #0
+    | SOME "p" => #1 + "go" (Snd "p")
+    end.
+
+Definition lsnoc : val :=
+  rec: "go" "l" "x" :=
+    match: "l" with
+      SOME "p" => (lcons (Fst "p") ("go" (Snd "p") "x"))
+    | NONE => lcons "x" NONE
+    end.
+
+Section lists.
+Context `{heapG Σ}.
+Implicit Types i : nat.
+Implicit Types v : val.
+
+Lemma lnil_spec : {{{ True }}} lnil #() {{{ hd, RET hd; ⌜ is_list hd [] ⌝ }}}.
+Proof. iIntros (Φ _) "HΦ". wp_lam. by iApply "HΦ". Qed.
+
+Lemma lcons_spec hd vs v :
+  {{{ ⌜ is_list hd vs ⌝ }}} lcons v hd {{{ hd', RET hd'; ⌜ is_list hd' (v :: vs) ⌝ }}}.
+Proof.
+  iIntros (Φ ?) "HΦ". wp_lam. wp_pures.
+  iApply "HΦ". simpl; eauto.
+Qed.
+
+Lemma lhead_spec hd vs v :
+  {{{ ⌜ is_list hd (v :: vs) ⌝ }}} lhead hd {{{ RET v; True }}}.
+Proof. iIntros (Φ (hd'&->&?)) "HΦ". wp_lam. wp_pures. by iApply "HΦ". Qed.
+
+Lemma ltail_spec hd vs v :
+  {{{ ⌜ is_list hd (v :: vs) ⌝ }}} ltail hd {{{ hd', RET hd'; ⌜ is_list hd' vs ⌝ }}}.
+Proof. iIntros (Φ (hd'&->&?)) "HΦ". wp_lam. wp_pures. by iApply "HΦ". Qed.
+
+Lemma llookup_spec i hd vs v :
+  vs !! i = Some v →
+  {{{ ⌜ is_list hd vs ⌝ }}} llookup #i hd {{{ RET v; True }}}.
+Proof.
+  iIntros (Hi Φ Hl) "HΦ".
+  iInduction vs as [|v' vs] "IH" forall (hd i Hi Hl); destruct i as [|i]=> //; simplify_eq/=.
+  { wp_lam. wp_pures. by iApply (lhead_spec with "[//]"). }
+  wp_lam. wp_pures.
+  wp_apply (ltail_spec with "[//]"); iIntros (hd' ?). wp_let.
+  wp_op. rewrite Nat2Z.inj_succ -Z.add_1_l Z.add_simpl_l. by iApply "IH".
+Qed.
+
+Lemma linsert_spec i hd vs v :
+  is_Some (vs !! i) →
+  {{{ ⌜ is_list hd vs ⌝ }}} linsert #i v hd {{{ hd', RET hd'; ⌜ is_list hd' (<[i:=v]> vs) ⌝ }}}.
+Proof.
+  iIntros ([w Hi] Φ Hl) "HΦ".
+  iInduction vs as [|v' vs] "IH" forall (hd i Hi Hl Φ); destruct i as [|i]=> //; simplify_eq/=.
+  { wp_lam. wp_pures. wp_apply (ltail_spec with "[//]"). iIntros (hd' ?).
+    wp_let. by iApply (lcons_spec with "[//]"). }
+  wp_lam; wp_pures.
+  wp_apply (ltail_spec with "[//]"); iIntros (hd' ?). wp_let.
+  wp_op. rewrite Nat2Z.inj_succ -Z.add_1_l Z.add_simpl_l.
+  wp_apply ("IH" with "[//] [//]"). iIntros (hd'' ?). wp_let.
+  wp_apply (lhead_spec with "[//]"); iIntros "_".
+  by wp_apply (lcons_spec with "[//]").
+Qed.
+
+Lemma llist_member_spec hd vs v :
+  {{{ ⌜ is_list hd vs ⌝ }}} llist_member v hd {{{ RET #(bool_decide (v ∈ vs)); True }}}.
+Proof.
+  iIntros (Φ Hl) "HΦ".
+  iInduction vs as [|v' vs] "IH" forall (hd Hl); simplify_eq/=.
+  { wp_lam; wp_pures. by iApply "HΦ". }
+  destruct Hl as (hd'&->&?). wp_lam; wp_pures.
+  destruct (bool_decide_reflect (v' = v)) as [->|?]; wp_if.
+  { rewrite (bool_decide_true (_ ∈ _ :: _)); last by left. by iApply "HΦ". }
+  wp_proj. wp_let. iApply ("IH" with "[//]"). destruct (bool_decide_reflect (v ∈ vs)).
+  - by rewrite bool_decide_true; last by right.
+  - by rewrite bool_decide_false ?elem_of_cons; last naive_solver.
+Qed.
+
+Lemma lreplicate_spec i v :
+  {{{ True }}} lreplicate #i v {{{ hd, RET hd; ⌜ is_list hd (replicate i v) ⌝ }}}.
+Proof.
+  iIntros (Φ _) "HΦ". iInduction i as [|i] "IH" forall (Φ); simpl.
+  { wp_lam; wp_pures.
+    iApply (lnil_spec with "[//]"). iApply "HΦ". }
+  wp_lam; wp_pures.
+  rewrite Nat2Z.inj_succ -Z.add_1_l Z.add_simpl_l.
+  wp_apply "IH"; iIntros (hd' Hl). wp_let. by iApply (lcons_spec with "[//]").
+Qed.
+
+Lemma llength_spec hd vs :
+  {{{ ⌜ is_list hd vs ⌝ }}} llength hd {{{ RET #(length vs); True }}}.
+Proof.
+  iIntros (Φ Hl) "HΦ".
+  iInduction vs as [|v' vs] "IH" forall (hd Hl Φ); simplify_eq/=.
+  { wp_lam. wp_match. by iApply "HΦ". }
+  destruct Hl as (hd'&->&?). wp_lam. wp_match. wp_proj.
+  wp_apply ("IH" $! hd' with "[//]"); iIntros "_ /=". wp_op.
+  rewrite (Nat2Z.inj_add 1). by iApply "HΦ".
+Qed.
+
+Lemma lsnoc_spec hd vs v :
+  {{{ ⌜ is_list hd vs ⌝ }}} lsnoc hd v {{{ hd', RET hd'; ⌜ is_list hd' (vs++[v]) ⌝ }}}.
+Proof.
+  iIntros (Φ Hvs) "HΦ".
+  iInduction vs as [|v' vs] "IH" forall (hd Hvs Φ).
+  - inversion Hvs.
+    subst.
+    wp_rec.
+    wp_pures.
+    wp_lam.
+    wp_pures.
+    iApply "HΦ". simpl. eauto.
+  - inversion Hvs as [vs' [Hhd Hvs']]; subst.
+    eauto.
+    wp_rec.
+    wp_pures.
+    wp_bind (lsnoc vs' v).
+    iApply "IH".
+    eauto.
+    iNext.
+    iIntros (hd' Hhd').
+    wp_pures.
+    iApply lcons_spec.
+    eauto.
+    iApply "HΦ". 
+Qed.
+
+End lists.
\ No newline at end of file