Add a basic symbol table example

_CoqProject

@@ -38,6 +38,7 @@ theories/examples/stack/mailbox.v
 theories/examples/stack/helping.v
 theories/examples/various.v
 theories/examples/or.v
+theories/examples/symbol.v
 theories/tests/typetest.v
 theories/tests/tactics.v
 theories/tests/tactics2.v

theories/examples/symbol.v

+From iris.proofmode Require Import tactics.
+From iris.algebra Require Import auth.
+From iris_logrel Require Import logrel examples.lock.
+
+Definition symbol1 : val := λ: <>,
+  let: "size" := ref #0 in
+  let: "l" := newlock #() in
+  Pack (λ: "s", acquire "l";;
+                let: "n" := !"size" in
+                "size" <- "n"+#1;;
+                release "l";;
+                "n",
+        λ: "n", #0).
+Definition symbol2 : val := λ: <>,
+  let: "size" := ref #0 in
+  let: "l" := newlock #() in
+  Pack (λ: "s", acquire "l";;
+                let: "n" := !"size" in
+                "size" <- "n"+#1;;
+                release "l";;
+                "n",
+        λ: "n", let: "m" := !"size" in
+                if: "n" ≤ "m" then #0 else #1).
+
+Definition SYMBOL : type := TExists (TProd (TArrow TNat (TVar 0))
+                                           (TArrow (TVar 0) TNat)).
+
+Lemma symbol1_type Γ :
+  typed Γ symbol1 (TArrow TUnit SYMBOL).
+Proof.
+  unfold SYMBOL.
+  solve_typed.
+Qed.
+Hint Resolve symbol1_type : typeable.
+Lemma symbol2_type Γ :
+  typed Γ symbol2 (TArrow TUnit SYMBOL).
+Proof.
+  unfold SYMBOL.
+  solve_typed.
+Qed.
+Hint Resolve symbol2_type : typeable.
+
+
+Class msizeG Σ := MSizeG { msize_inG :> inG Σ (authR mnatUR) }.
+Definition msizeΣ : gFunctors := #[GFunctor (authR mnatUR)].
+
+Instance subG_mcounterΣ {Σ} : subG msizeΣ Σ → msizeG Σ.
+Proof. solve_inG. Qed.
+
+Section rules.
+  Definition sizeN := logrelN .@ "size".
+  Context `{!logrelG Σ, !msizeG Σ}.
+  Context (γ : gname).
+
+  Lemma size_le (n m : nat) :
+    own γ (● (n : mnat)) -∗
+    own γ (◯ (m : mnat)) -∗
+    ⌜m ≤ n⌝.
+  Proof.
+    iIntros "Hn Hm".
+    by iDestruct (own_valid_2 with "Hn Hm")
+      as %[?%mnat_included _]%auth_valid_discrete_2.
+  Qed.
+
+  Lemma same_size (n m : nat) :
+    own γ (● (n : mnat)) ∗ own γ (◯ (m : mnat))
+    ==∗ own γ (● (n : mnat)) ∗ own γ (◯ (n : mnat)).
+  Proof.
+    iIntros "[Hn Hm]".
+    iMod (own_update_2 γ _ _ (● (n : mnat) ⋅ ◯ (n : mnat)) with "Hn Hm")
+      as "[$ $]"; last done.
+    apply auth_update, (mnat_local_update _ _ n); auto.
+  Qed.
+
+  Lemma inc_size' (n m : nat) :
+    own γ (● (n : mnat)) ∗ own γ (◯ (m : mnat))
+    ==∗ own γ (● (S n : mnat)).
+  Proof.
+    iIntros "[Hn #Hm]".
+    iMod (own_update_2 γ _ _ (● (S n : mnat) ⋅ ◯ (S n : mnat)) with "Hn Hm") as "[$ _]"; last done.
+    apply auth_update, (mnat_local_update _ _ (S n)); auto.
+  Qed.
+
+  Lemma conjure_0 :
+    (|==> own γ (◯ (0 : mnat)))%I.
+  Proof. by apply own_unit. Qed.
+
+  Lemma inc_size (n : nat) :
+    own γ (● (n : mnat)) ==∗ own γ (● (S n : mnat)).
+  Proof.
+    iIntros "Hn".
+    iMod (conjure_0) as "Hz".
+    iApply inc_size'; by iFrame.
+  Qed.
+
+  Program Definition tableR : prodC valC valC -n> iProp Σ := λne vv,
+    (∃ n : nat, ⌜vv.1 = #n⌝ ∗ ⌜vv.2 = #n⌝ ∗ own γ (◯ (n : mnat)))%I.
+  Next Obligation. solve_proper. Qed.
+
+  Instance tableR_persistent ww : PersistentP (tableR ww).
+  Proof. apply _. Qed.
+
+  Definition table_inv (size1 size2 : loc) : iProp Σ :=
+    (∃ (n : nat), own γ (● (n : mnat)) ∗ size1 ↦ᵢ{1/2} #n ∗ size2 ↦ₛ{1/2} #n)%I.
+
+  Definition lok_inv (size1 size2 l : loc) : iProp Σ :=
+    (∃ (n : nat), size1 ↦ᵢ{1/2} #n ∗ size2 ↦ₛ{1/2} #n ∗ l ↦ₛ #false)%I.
+
+End rules.
+
+Section proof.
+  Context `{!logrelG Σ, !msizeG Σ, !lockG Σ}.
+
+  Lemma mapsto_half_combine l v1 v2 :
+    l ↦ᵢ{1/2} v1 -∗ l ↦ᵢ{1/2} v2 -∗ ⌜v1 = v2⌝ ∗ l ↦ᵢ v1.
+  Proof.
+    iIntros "Hl1 Hl2".
+    iDestruct (mapsto_agree with "Hl1 Hl2") as %?. simplify_eq.
+    iSplit; eauto.
+    iApply (fractional_half_2 with "Hl1 Hl2").
+  Qed.
+
+  Lemma heapS_mapsto_half_combine l v1 v2 :
+    l ↦ₛ{1/2} v1 -∗ l ↦ₛ{1/2} v2 -∗ ⌜v1 = v2⌝ ∗ l ↦ₛ v1.
+  Proof.
+    iIntros "Hl1 Hl2".
+    iDestruct (threadpool.mapsto_agree with "Hl1 Hl2") as %?. simplify_eq.
+    iSplit; eauto.
+    iApply (fractional_half_2 with "Hl1 Hl2").
+  Qed.
+
+  Lemma refinement1 Δ Γ :
+    {⊤,⊤;Δ;Γ} ⊨ symbol2 ≤log≤ symbol1 : TArrow TUnit SYMBOL.
+  Proof.
+    unlock symbol1 symbol2.
+    iApply bin_log_related_arrow_val; eauto.
+    iAlways. iIntros (? ?) "[% %]"; simplify_eq/=.
+    rel_let_l. rel_let_r.
+    rel_alloc_l as size1 "[Hs1 Hs1']"; rel_let_l.
+    rel_alloc_r as size2 "[Hs2 Hs2']"; rel_let_r.
+    iApply fupd_logrel'.
+    iMod (own_alloc (● (0 : mnat))) as (γ) "Ha"; first done.
+    iMod (inv_alloc sizeN _ (table_inv γ size1 size2) with "[Hs1 Hs2 Ha]") as "#Hinv".
+    { iNext. iExists _. by iFrame. }
+    iModIntro.
+    rel_apply_r bin_log_related_newlock_r; first done.
+    iIntros (l2) "Hl2". rel_let_r.
+    pose (N:=(logrelN.@"lock1")).
+    rel_apply_l (bin_log_related_newlock_l N (lok_inv size1 size2 l2)%I with "[Hs1' Hs2' Hl2]").
+    { iExists 0. by iFrame. }
+    iIntros (l1 γl) "#Hl1". rel_let_l.
+    iApply (bin_log_related_pack _ (tableR γ)).
+    iApply bin_log_related_pair.
+    (* Insert *)
+    - iApply bin_log_related_arrow_val; eauto.
+      iAlways. iIntros (? ?). iDestruct 1 as (n) "[% %]"; simplify_eq/=.
+      rel_let_l. rel_let_r.
+      rel_apply_l (bin_log_related_acquire_l with "Hl1"); auto.
+      iIntros "Hlk Htbl".
+      rel_let_l.
+      iDestruct "Htbl" as (m) "(Hs1 & Hs2 & Hl2)".
+      rel_load_l.
+      rel_let_l.
+      rel_op_l.
+      rel_store_l_atomic.
+      iInv sizeN as (m') ">(Ha & Hs1' & Hs2')" "Hcl".
+      iDestruct (mapsto_half_combine with "Hs1 Hs1'") as "[% Hs1]"; simplify_eq.
+      iModIntro. iExists _. iFrame. iNext. iIntros "[Hs1 Hs1']".
+      rel_let_l.
+      rel_apply_r (bin_log_related_acquire_r with "Hl2"); first solve_ndisj.
+      iIntros "Hl2".
+      rel_let_r.
+      iDestruct (heapS_mapsto_half_combine with "Hs2 Hs2'") as "[% Hs2]"; simplify_eq.
+      rel_load_r.
+      repeat (rel_pure_r _).
+      rel_store_r.
+      rel_let_r.
+      rel_apply_r (bin_log_related_release_r with "Hl2"); first solve_ndisj.
+      iIntros "Hl2".
+      rel_let_r.
+      (* Before we close the lock, we need to gather some evidence *)
+      iApply fupd_logrel'.
+      iMod (conjure_0 γ) as "Hf".
+      iMod (same_size with "[$Ha $Hf]") as "[Ha #Hf]".
+      iMod (inc_size with "Ha") as "Ha".
+      iModIntro.
+      iDestruct "Hs2" as "[Hs2 Hs2']".
+      rewrite Nat.add_1_r.
+      iMod ("Hcl" with "[Ha Hs1 Hs2]") as "_".
+      { iNext. iExists _. iFrame. }
+      rel_apply_l (bin_log_related_release_l with "Hl1 Hlk [-]"); auto.
+      { iExists _. by iFrame. }
+      rel_let_l.
+      rel_vals. iModIntro. iAlways.
+      iExists m'. eauto.
+    (* Lookup *)
+    - iApply bin_log_related_arrow_val; eauto.
+      iAlways. iIntros (k1 k2) "/= #Hk".
+      iDestruct "Hk" as (n) "(% & % & #Hn)"; simplify_eq.
+      rel_let_l.
+      rel_let_r.
+      rel_load_l_atomic.
+      iInv sizeN as (m') ">(Ha & Hs1' & Hs2')" "Hcl".
+      iModIntro. iExists _. iFrame. iNext. iIntros "Hs1'".
+      iDestruct (own_valid_2 with "Ha Hn")
+        as %[?%mnat_included _]%auth_valid_discrete_2.
+      iMod ("Hcl" with "[Ha Hs1' Hs2']") as "_".
+      { iNext. iExists _. by iFrame. }
+      rel_let_l.
+      rel_op_l.
+      destruct (le_dec n m'); last congruence.
+      rel_if_l.
+      iApply bin_log_related_nat.
+  Qed.
+End proof.