Library with list stuff, and refactor mset based on that.

_CoqProject

 -Q theories iris_c
 -arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
 
+theories/lib/list.v
 theories/lib/mset.v
 theories/lib/flock.v
 theories/lib/locking_heap.v

theories/c_translation/monad.v

@@ -63,7 +63,7 @@ Section a_wp.
 
   Definition env_inv (env : val) : iProp Σ :=
     (∃ (X : gset val) (σ : gmap loc lvl),
-         is_set_mut env X
+         is_mset env X
        ∗ full_locking_heap σ
        ∗ ([∗ map] l ↦ _ ∈ σ, ∃ v', l ↦{1/2} v')
        ∗ ⌜correct_locks X (locked_locs σ)⌝)%I.

theories/c_translation/translation.v

@@ -111,12 +111,12 @@ Section proofs.
   Qed.
 
   Lemma a_store_spec R Φ Ψ1 Ψ2 e1 e2 :
-    awp e1 R Ψ1 -∗
-    awp e2 R Ψ2 -∗
+    AWP e1 @ R {{ Ψ1 }} -∗
+    AWP e2 @ R {{ Ψ2 }} -∗
     ▷ (∀ v1 v2,
         Ψ1 v1 -∗ Ψ2 v2 -∗ ∃ (l : loc) w,
         ⌜ v1 = #l ⌝ ∧ l ↦C w ∗ (l ↦C[LLvl] v2 -∗ Φ v2)) -∗
-    awp (a_store e1 e2) R Φ.
+    AWP e1 =ᶜ e2 @ R {{ Φ }}.
   Proof.
     iIntros "H1 H2 HΦ".
     awp_apply (a_wp_awp with "H1"); iIntros (v1) "H1". awp_lam.
@@ -134,7 +134,7 @@ Section proofs.
     { unfold correct_locks in *. intros Hx. apply Hl.
       destruct (Hlocks _ Hx) as [l' [? Hl']]. by simplify_eq/=. }
     wp_let. wp_proj.
-    wp_apply (mset_add_spec with "[$HX]"); eauto.
+    wp_apply (mset_add_spec with "HX"); first done.
     iIntros "HX". wp_seq.
     iDestruct (full_locking_heap_unlocked with "Hl Hσ") as %?.
     iMod (locking_heap_change_lock _ _ ULvl LLvl with "Hσ Hl") as "[Hσ Hl]".
@@ -180,7 +180,7 @@ Section proofs.
       destruct (Hlocks _ Hx) as [l' [? Hl']]. by simplify_eq/=. }
     wp_let.
     wp_apply wp_assert.
-    wp_apply (mset_member_spec #l env with "HX").
+    wp_apply (mset_member_spec with "HX").
     iIntros "Henv /=". case_decide; first by exfalso. simpl.
     wp_op. iSplit; eauto. iNext. wp_seq.
     rewrite mapsto_eq /mapsto_def.

theories/lib/list.v

+From iris.heap_lang Require Export proofmode notation.
+From iris.heap_lang Require Import assert.
+
+Opaque Z.of_nat.
+
+(** 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.
+
+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Φ". do 2 wp_lam. 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Φ". repeat wp_pure _. 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Φ". repeat wp_pure _. by iApply "HΦ". Qed.
+
+Lemma llookup_spec_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/=.
+  { do 2 wp_lam. wp_op; wp_if. by iApply (lhead_spec with "[//]"). }
+  do 2 wp_lam. wp_op; case_bool_decide=> [//|]. wp_if.
+  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_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/=.
+  { do 3 wp_lam. wp_op; wp_if. wp_apply (ltail_spec with "[//]"). iIntros (hd' ?).
+    wp_let. by iApply (lcons_spec with "[//]"). }
+  do 3 wp_lam. wp_op; case_bool_decide=> [//|]. wp_if.
+  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/=.
+  { do 2 wp_lam. wp_match. by iApply "HΦ". }
+  destruct Hl as (hd'&->&?). do 2 wp_lam. wp_match. wp_proj.
+  wp_op. 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.
+  { do 2 wp_lam. wp_op; case_bool_decide=> //=; wp_if.
+    iApply (lnil_spec with "[//]"). iApply "HΦ". }
+  do 2 wp_lam; wp_op; case_bool_decide=> [//|]; wp_if.
+  wp_op. 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.
+End lists.

theories/lib/mset.v

 From iris.heap_lang Require Export proofmode notation.
 From iris.heap_lang Require Import assert.
+From iris_c.lib Require Import list.
 
-Section Sets.
-  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 is_mset `{heapG Σ} (v : val) (X : gset val) : iProp Σ :=
+  (∃ (l : loc) hd vs,
+    ⌜ v = #l ∧ X = of_list vs ∧ is_list hd vs ∧ NoDup vs ⌝ ∗ l ↦ hd)%I.
 
-  Definition is_set (hd : val) (X : gset val) : Prop :=
-    ∃ l : list val, is_list hd l ∧ NoDup l ∧ of_list l = X.
+Definition mset_create : val := λ: <>, ref (lnil #()).
 
-  Definition newset : val := λ: <>, NONEV.
+Definition mset_member : val := λ: "x" "xs",
+  let: "l" := !"xs" in
+  llist_member "x" "l".
 
-  Definition set_member : val :=
-    rec: "member" "x" "xs" :=
-      match: "xs" with
-        NONE => #false
-      | SOME "p" =>
-        if: Fst "p" = "x" then #true
-        else let: "y" := (Snd "p")  in "member" "x" "y"
-      end.
+Definition mset_add : val := λ: "x" "xs",
+  let: "l" := !"xs" in
+  assert: (llist_member "x" "l" = #false);;
+  "xs" <- lcons "x" "l".
 
-  Definition set_add : val := λ: "x" "xs",
-    if: set_member "x" "xs"
-    then assert #false
-    else SOME ("x", "xs").
-End Sets.
+Definition mset_clear : val := λ: "xs",
+  "xs" <- lnil #().
 
-Section MutableSet.
-  Definition is_set_mut `{heapG Σ} (v : val) (X : gset val) : iProp Σ
-    := (∃ (l : loc) hd, ⌜ v = #l ⌝ ∗ l ↦ hd ∗ ⌜ is_set hd X ⌝)%I.
-
-  Definition mset_create : val := λ: <>, ref (newset #()).
-
-  Definition mset_member : val := λ: "x" "xs",
-    let: "v" := ! "xs" in
-    set_member "x" "v".
-
-  Definition mset_add : val := λ: "x" "xs",
-    let: "v" := ! "xs" in
-    "xs" <- set_add "x" "v".
-
-  Definition mset_clear : val := λ: "xs",
-    "xs" <-  newset #().
-End MutableSet.
-
-Section Sets_wp.
-  Context `{heapG Σ}.
-
-  Lemma set_newset_spec:
-    {{{ True }}} newset #() {{{ v, RET v; ⌜is_set v ∅⌝ }}}.
-  Proof.
-    iIntros (Φ) "_ HΦ". wp_lam.
-    iApply "HΦ". iExists []. simpl; eauto using NoDup_nil_2.
-  Qed.
-
-  Lemma set_member_spec (x: val) (xs: val) (X:  gset val):
-    {{{ ⌜is_set xs X⌝ }}}
-      set_member x xs
-    {{{ RET #(bool_decide (x ∈ X)); True }}}.
-  Proof.
-    iIntros (Φ (l & Hl & _ & HX)) "HΦ".
-    iRevert (Hl HX). iInduction l as [|hd tl] "IH" forall (xs X); simpl.
-    - iIntros (-> <-) "/=". do 2 wp_lam. wp_case. wp_seq.
-      rewrite bool_decide_false; last by set_solver. by iApply "HΦ".
-    - iIntros ([hd' [-> Hl]] <-) "/=". do 2 wp_lam. wp_case. wp_let. wp_proj.
-      wp_op. destruct (bool_decide_reflect (hd = x)) as [->|?]; wp_if.
-      + rewrite bool_decide_true; last set_solver. by iApply "HΦ".
-      + wp_proj. wp_let.
-        iApply ("IH" $! hd' (of_list tl) with "[HΦ] [//] [//]").
-        iNext; iIntros. case_bool_decide.
-        * rewrite bool_decide_true; last set_solver. by iApply "HΦ".
-        * rewrite bool_decide_false; last set_solver. by iApply "HΦ".
-  Qed.
-
-  Lemma set_add_spec (x: val) (xs: val) (X:  gset val):
-    {{{ ⌜is_set xs X⌝ ∧ ⌜x ∉ X⌝ }}}
-      set_add x xs
-    {{{ v, RET v; ⌜is_set v ({[x]} ∪ X) ⌝ }}}.
-  Proof.
-    iIntros (Φ [Hset ?]) "HΦ". do 2 wp_lam.
-    wp_bind (set_member x xs).
-    iApply (set_member_spec _ _ X with "[//]").
-    iNext. iIntros "_". case_bool_decide; first by set_solver.
-    wp_if. iApply "HΦ". iPureIntro.
-    destruct Hset as (l & Hl & ? & <-). exists (x :: l).
-    split_and!; [|constructor|]; set_solver.
-  Qed.
-End Sets_wp.
-
-Section MutableSet_wp.
+Section mset.
   Context `{heapG Σ}.
+  Implicit Types x v : val.
 
-  Lemma mset_create_spec:
-    {{{ True }}} mset_create #() {{{ v, RET v; is_set_mut v ∅ }}}.
+  Lemma mset_create_spec :
+    {{{ True }}} mset_create #() {{{ x, RET x; is_mset x ∅ }}}.
   Proof.
-    iIntros (Φ) "_ H".
-    wp_lam. wp_apply (set_newset_spec with "[//]").
-    iIntros (v ?). wp_alloc l as "Hl". iApply "H".
-    iExists l, v. by iFrame.
+    iIntros (Φ) "_ HΦ". wp_lam. wp_apply (lnil_spec with "[//]").
+    iIntros (hd ?); simplify_eq/=. wp_alloc l as "Hl". iApply "HΦ".
+    iExists l, _, []. iFrame "Hl". by rewrite /= NoDup_nil.
   Qed.
 
-  Lemma mset_member_spec (x: val) (xs: val) (X:  gset val):
-    {{{ is_set_mut xs X }}}
-      mset_member x xs
-    {{{ RET #(bool_decide (x ∈ X)); is_set_mut xs X }}}.
+  Lemma mset_member_spec x e v X :
+    IntoVal e v →
+    {{{ is_mset x X }}}
+      mset_member e x
+    {{{ RET #(bool_decide (v ∈ X)); is_mset x X }}}.
   Proof.
-    iIntros (Φ) "Hmut H".
-    iDestruct "Hmut" as (s hd ->) "[Hs #Hset]".
-    wp_lam. wp_let. wp_load. wp_let.
-    wp_apply (set_member_spec with "Hset"). iIntros (v).
-    iApply ("H" with "[Hset Hs]").
-    iExists s, hd. eauto.
+    iIntros (<- Φ) "Hmut HΦ". iDestruct "Hmut" as (l hd vs (->&->&?&?)) "Hl".
+    do 2 wp_lam. wp_load. wp_let.
+    wp_apply (llist_member_spec with "[//]"). iIntros "_".
+    rewrite (bool_decide_iff _ (v ∈ vs)); last set_solver.
+    iApply "HΦ". iExists l, hd, vs; auto.
   Qed.
 
-  Lemma mset_add_spec (xe xse: expr) (x xs: val) (X:  gset val):
-    IntoVal xe x →
-    IntoVal xse xs →
-    {{{ is_set_mut xs X ∧ ⌜x ∉ X⌝ }}}
-      mset_add xe xse
-    {{{ RET #() ; (is_set_mut xs ({[x]} ∪ X))}}}.
+  Lemma mset_add_spec x e v X :
+    IntoVal e v →
+    v ∉ X →
+    {{{ is_mset x X }}}
+      mset_add e x
+    {{{ RET #(); is_mset x ({[v]} ∪ X) }}}.
   Proof.
-    iIntros (<- <- Φ) "[Hmut %] HPost".
-    iDestruct "Hmut" as (s hd) "[% [Hs Hset]]"; subst.
-    do 2 wp_lam; wp_load; wp_let.
-    wp_apply (set_add_spec with "[$Hset//]").
-    iIntros (v ?). wp_store. iApply "HPost".
-    iExists s, v. by iFrame.
+    iIntros (<- Φ ?) "Hmut HΦ". iDestruct "Hmut" as (l hd vs (->&->&?&?)) "Hl".
+    do 2 wp_lam. wp_load. wp_lam. wp_apply wp_assert.
+    wp_apply (llist_member_spec with "[//]"); iIntros "_".
+    rewrite bool_decide_false /=; last set_solver. wp_op; iSplit=> //; iIntros "!>".
+    wp_seq. wp_apply (lcons_spec with "[//]"); iIntros (hd' ?). wp_store.
+    iApply "HΦ". iExists l, hd', (v :: vs). iFrame "Hl".
+    rewrite NoDup_cons. iPureIntro; set_solver.
   Qed.
 
-  Lemma mset_clear_spec (xs: val) (X:  gset val):
-    {{{ is_set_mut xs X }}}
-      mset_clear xs
-    {{{ RET #() ; is_set_mut xs ∅}}}.
+  Lemma mset_clear_spec x X :
+    {{{ is_mset x X }}} mset_clear x {{{ RET #(); is_mset x ∅}}}.
   Proof.
-    iIntros (Φ) "Hmut HPost".
-    iDestruct "Hmut" as (s hd) "[% [Hs Hset]]"; subst.
-    wp_lam. wp_apply (set_newset_spec with "[//]").
-    iIntros (v ?). wp_store.
-    iApply "HPost". iExists s, v. by iFrame.
+    iIntros (Φ) "Hmut HΦ". iDestruct "Hmut" as (l hd vs (->&->&?&?)) "Hl".
+    wp_lam. wp_apply (lnil_spec with "[//]").
+    iIntros (hd' ?); simplify_eq/=. wp_store. iApply "HΦ".
+    iExists l, _, []. iFrame "Hl". by rewrite /= NoDup_nil.
   Qed.
-End MutableSet_wp.
+End mset.