Finish a generative ADT example

From "State-Dependent Represenation Independence" by A. Ahmed, D. Dreyer, A. Rossberg.

theories/F_mu_ref_conc/rules.v

@@ -46,6 +46,15 @@ Section mapsto.
     by intros [_ ?%agree_op_invL'].
   Qed.
 
+  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.
+
 End mapsto.
 
 Section lang_rules.

theories/examples/symbol.v

+(** This is a generative ADT example from "State-Dependent
+Represenation Independence" by A. Ahmed, D. Dreyer, A. Rossberg.
+
+In this example we implement a symbol lookup table, where a symbol is
+an abstract data type. Because the only way to obtain a symbol is to
+insert something into the table, we can show that the dynamic check in
+the lookup function in `symbol2` is redundant. *)
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import auth.
-From iris_logrel Require Import logrel examples.lock.
+From iris_logrel Require Import logrel examples.lock examples.various.
+
+(** * Some stuff on lists *)
+Notation Conse h t := (Fold (SOME (Pair h t))).
+Notation ConseV h t := (FoldV (SOMEV (PairV h t))).
+Notation Nile := (Fold NONE).
+Notation NileV := (FoldV NONEV).
+
+Definition LIST τ :=
+  TRec (TSum TUnit (TProd τ.[ren (+1)] (TVar 0))).
+
+Lemma LIST_interp_nil τ `{logrelG Σ} :
+  ⟦ LIST τ ⟧ [] (NileV, NileV).
+Proof.
+  rewrite /= {1}fixpoint_unfold /=.
+  iExists (_,_).
+  iSplit; eauto.
+  iNext. iLeft. iExists (_,_). eauto.
+Qed.
+Lemma LIST_interp_cons (n : nat) ls1 ls2 `{logrelG Σ} :
+  ⟦ LIST TNat ⟧ [] (ls1,ls2) -∗
+  ⟦ LIST TNat ⟧ [] (ConseV #n ls1,ConseV #n ls2).
+Proof.
+  iIntros "#Hls".
+  rewrite /= {2}fixpoint_unfold /=.
+  iExists (_,_).
+  iSplit; eauto.
+  iNext. iRight. iExists (_,_).
+  iSplit; eauto.
+  iExists (_,_), (_,_). iSplit; eauto.
+Qed.
+Lemma LIST_interp_weaken `{logrelG Σ} Δ ls1 ls2 :
+  ⟦ LIST TNat ⟧ [] (ls1, ls2) -∗
+  ⟦ LIST TNat ⟧ Δ (ls1, ls2).
+Proof.
+  iRevert (ls1 ls2).
+  iLöb as "IH".
+  iIntros (ls1 ls2) "#Hls /=".
+  rewrite {2}(fixpoint_unfold (interp_rec1
+        (interp_sum interp_unit (interp_prod interp_nat (ctx_lookup 0))) Δ)) /=.
+  rewrite {2}(fixpoint_unfold (interp_rec1
+                (interp_sum interp_unit
+                   (interp_prod interp_nat (ctx_lookup 0))) [])) /=.
+  iDestruct "Hls" as ([? ?]) "[% #Hls]".
+  iExists (_,_).
+  iSplit; eauto.
+  iNext.
+  iDestruct "Hls" as "[Hls | Hls]".
+  - iLeft; eauto.
+  - iRight.
+    iDestruct "Hls" as ([? ?]) "[% Hls]".
+    iExists _. iSplit; eauto.
+    iDestruct "Hls" as ([? ?] [? ?]) "[% [Hn #Hls]]".
+    iExists _,_. iSplit; eauto.
+    iSplit; eauto.
+    iAlways.
+    by iApply "IH".
+Qed.
 
+(* `nth ls n` diverges if `n >= length ls` *)
+Definition nth : val := rec: "nth" "l" "n" :=
+  match: Unfold "l" with
+    NONE      => bot #()
+  | SOME "xs" => if: "n" = #0
+                 then Fst "xs"
+                 else "nth" (Snd "xs") ("n" - #1)
+  end.
+
+Lemma bot_typed Γ τ :
+  Γ ⊢ₜ bot : TArrow TUnit τ.
+Proof. solve_typed. Qed.
+Hint Resolve bot_typed : typeable.
+Lemma nth_typed Γ τ :
+  Γ ⊢ₜ nth : TArrow (LIST τ) (TArrow TNat τ).
+Proof.
+  unfold LIST.
+  solve_typed.
+  econstructor.
+  econstructor; cbn.
+  econstructor.
+  - solve_typed.
+  - asimpl. solve_typed.
+  - asimpl. solve_typed.
+Qed.
+Hint Resolve nth_typed : typeable.
+
+(** * Symbol table *)
+(* SYMBOL = ∃ α. (eq: α → α → bool)
+               × (insert: nat → α)
+               × (lookup: α → nat) *)
+Definition SYMBOL : type :=
+  TExists (TProd (TProd (TArrow (TVar 0) (TArrow (TVar 0) TBool))
+                        (TArrow TNat (TVar 0)))
+                        (TArrow (TVar 0) TNat)).
+
+Definition eqKey : val := λ: "n" "m", "n" = "m".
 Definition symbol1 : val := λ: <>,
   let: "size" := ref #0 in
+  let: "tbl" := ref Nile in
   let: "l" := newlock #() in
-  Pack (λ: "s", acquire "l";;
+  Pack (eqKey,
+        λ: "s", acquire "l";;
                 let: "n" := !"size" in
                 "size" <- "n"+#1;;
+                "tbl" <- Conse "s" (!"tbl");;
                 release "l";;
                 "n",
-        λ: "n", #0).
+        λ: "n", nth (!"tbl") (!"size" - "n")).
 Definition symbol2 : val := λ: <>,
   let: "size" := ref #0 in
+  let: "tbl" := ref Nile in
   let: "l" := newlock #() in
-  Pack (λ: "s", acquire "l";;
+  Pack (eqKey,
+        λ: "s", acquire "l";;
                 let: "n" := !"size" in
                 "size" <- "n"+#1;;
+                "tbl" <- Conse "s" (!"tbl");;
                 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 Γ :
+                if: "n" ≤ "m" then nth (!"tbl") (!"size" - "n") else #0).
+Lemma eqKey_typed Γ :
+  typed Γ eqKey (TArrow TNat (TArrow TNat TBool)).
+Proof. solve_typed. Qed.
+Hint Resolve eqKey_typed : typeable.
+Lemma symbol1_typed Γ :
   typed Γ symbol1 (TArrow TUnit SYMBOL).
 Proof.
   unfold SYMBOL.
   solve_typed.
+  econstructor. cbn.
+  econstructor; cbn. 2: solve_typed.
+  econstructor; cbn.
+  econstructor; cbn.
+  econstructor; cbn.
+  econstructor; cbn. 2: solve_typed.
+  econstructor; cbn.
+  econstructor; cbn.
+  econstructor; cbn.
+  econstructor; cbn.
+  apply eqKey_typed.
+  econstructor; cbn. 2: solve_typed.
+  all: solve_typed.
 Qed.
-Hint Resolve symbol1_type : typeable.
-Lemma symbol2_type Γ :
+Hint Resolve symbol1_typed : typeable.
+Lemma symbol2_typed Γ :
   typed Γ symbol2 (TArrow TUnit SYMBOL).
 Proof.
   unfold SYMBOL.
   solve_typed.
+  econstructor. cbn.
+  econstructor; cbn. 2: solve_typed.
+  econstructor; cbn.
+  econstructor; cbn.
+  econstructor; cbn.
+  econstructor; cbn. 2: solve_typed.
+  econstructor; cbn.
+  econstructor; cbn.
+  econstructor; cbn.
+  econstructor; cbn.
+  apply eqKey_typed.
+  econstructor; cbn. 2: solve_typed.
+  all: solve_typed.
 Qed.
-Hint Resolve symbol2_type : typeable.
-
+Hint Resolve symbol2_typed : typeable.
 
+(** * The actual refinement proof.
+      Requires monotonic state *)
 Class msizeG Σ := MSizeG { msize_inG :> inG Σ (authR mnatUR) }.
 Definition msizeΣ : gFunctors := #[GFunctor (authR mnatUR)].
 
@@ -100,33 +234,38 @@ Section rules.
   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.
+  Definition table_inv (size1 size2 tbl1 tbl2 : loc) : iProp Σ :=
+    (∃ (n : nat) (ls : val), own γ (● (n : mnat))
+                           ∗ size1 ↦ᵢ{1/2} #n ∗ size2 ↦ₛ{1/2} #n
+                           ∗ tbl1 ↦ᵢ{1/2} ls ∗ tbl2 ↦ₛ{1/2} ls
+                           ∗ ⟦ LIST TNat ⟧ [] (ls, ls))%I.
 
+  Definition lok_inv (size1 size2 tbl1 tbl2 l : loc) : iProp Σ :=
+    (∃ (n : nat) (ls : val), size1 ↦ᵢ{1/2} #n ∗ size2 ↦ₛ{1/2} #n
+                           ∗ tbl1 ↦ᵢ{1/2} ls ∗ tbl2 ↦ₛ{1/2} ls
+                           ∗ 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.
+  Lemma eqKey_refinement Δ Γ γ :
+    {⊤,⊤;tableR γ :: Δ;Autosubst_Classes.subst (ren (+1)) <$> Γ} ⊨
+      eqKey
+    ≤log≤
+      eqKey : TArrow (TVar 0) (TArrow (TVar 0) TBool).
   Proof.
-    iIntros "Hl1 Hl2".
-    iDestruct (threadpool.mapsto_agree with "Hl1 Hl2") as %?. simplify_eq.
-    iSplit; eauto.
-    iApply (fractional_half_2 with "Hl1 Hl2").
+    unlock eqKey.
+    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.
+    iApply bin_log_related_arrow_val; eauto.
+    iAlways. iIntros (k1 k2) "/= #Hk".
+    iDestruct "Hk" as (m) "(% & % & #Hm)"; simplify_eq.
+    rel_let_l. rel_let_r.
+    iApply bin_log_related_nat_binop; eauto;
+      iApply bin_log_related_nat.
   Qed.
 
   Lemma refinement1 Δ Γ :
@@ -138,19 +277,23 @@ Section proof.
     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.
+    rel_alloc_l as tbl1 "[Htbl1 Htbl1']"; rel_let_l.
+    rel_alloc_r as tbl2 "[Htbl2 Htbl2']"; 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. }
+    iMod (inv_alloc sizeN _ (table_inv γ size1 size2 tbl1 tbl2) with "[Hs1 Hs2 Htbl1 Htbl2 Ha]") as "#Hinv".
+    { iNext. iExists _,_. iFrame. iApply LIST_interp_nil. }
     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. }
+    rel_apply_l (bin_log_related_newlock_l N (lok_inv size1 size2 tbl1 tbl2 l2)%I with "[Hs1' Hs2' Htbl1' Htbl2' Hl2]").
+    { iExists 0,_. by iFrame. }
     iIntros (l1 γl) "#Hl1". rel_let_l.
     iApply (bin_log_related_pack _ (tableR γ)).
-    iApply bin_log_related_pair.
+    repeat iApply bin_log_related_pair.
+    (* Eq *)
+    - iApply eqKey_refinement.
     (* Insert *)
     - iApply bin_log_related_arrow_val; eauto.
       iAlways. iIntros (? ?). iDestruct 1 as (n) "[% %]"; simplify_eq/=.
@@ -158,26 +301,24 @@ Section proof.
       rel_apply_l (bin_log_related_acquire_l with "Hl1"); auto.
       iIntros "Hlk Htbl".
       rel_let_l.
-      iDestruct "Htbl" as (m) "(Hs1 & Hs2 & Hl2)".
+      iDestruct "Htbl" as (m ls) "(Hs1 & Hs2 & Htbl1 & Htbl2 & Hl2)".
       rel_load_l.
       rel_let_l.
       rel_op_l.
       rel_store_l_atomic.
-      iInv sizeN as (m') ">(Ha & Hs1' & Hs2')" "Hcl".
+      iInv sizeN as (m' ls') "(Ha & >Hs1' & >Hs2' & >Htbl1' & >Htbl2' & #Hls)" "Hcl".
       iDestruct (mapsto_half_combine with "Hs1 Hs1'") as "[% Hs1]"; simplify_eq.
+      iDestruct (mapsto_half_combine with "Htbl1 Htbl1'") as "[% [Htbl1 Htbl1']]"; 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.
+      iDestruct (threadpool.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".
@@ -186,10 +327,28 @@ Section proof.
       iModIntro.
       iDestruct "Hs2" as "[Hs2 Hs2']".
       rewrite Nat.add_1_r.
-      iMod ("Hcl" with "[Ha Hs1 Hs2]") as "_".
-      { iNext. iExists _. iFrame. }
+      iMod ("Hcl" with "[Ha Hs1 Hs2 Htbl1 Htbl2]") as "_".
+      { iNext. iExists _,_. by iFrame. }
+      rel_load_l.
+      rel_store_l_atomic.
+      iClear "Hls".
+      iInv sizeN as (m ls) "(Ha & >Hs1 & >Hs2 & >Htbl1 & >Htbl2 & #Hls)" "Hcl".
+      iDestruct (mapsto_half_combine with "Htbl1 Htbl1'") as "[% Htbl1]"; simplify_eq.
+      iModIntro. iExists _. iFrame. iNext. iIntros "[Htbl1 Htbl1']".
+      rel_let_l.
+      rel_load_r.
+      iDestruct (threadpool.mapsto_half_combine with "Htbl2 Htbl2'") as "[% Htbl2]"; simplify_eq.
+      rel_store_r.
+      rel_let_r.
+      rel_apply_r (bin_log_related_release_r with "Hl2"); first solve_ndisj.
+      iIntros "Hl2".
+      rel_let_r.
+      iDestruct "Htbl2" as "[Htbl2 Htbl2']".
+      iMod ("Hcl" with "[Ha Hs1 Hs2 Htbl1 Htbl2]") as "_".
+      { iNext. iExists _,_. iFrame.
+        by iApply LIST_interp_cons. }
       rel_apply_l (bin_log_related_release_l with "Hl1 Hlk [-]"); auto.
-      { iExists _. by iFrame. }
+      { iExists _,_. by iFrame. }
       rel_let_l.
       rel_vals. iModIntro. iAlways.
       iExists m'. eauto.
@@ -200,16 +359,35 @@ Section proof.
       rel_let_l.
       rel_let_r.
       rel_load_l_atomic.
-      iInv sizeN as (m') ">(Ha & Hs1' & Hs2')" "Hcl".
+      iInv sizeN as (m ls) "(Ha & Hs1' & >Hs2' & >Htbl1' & >Htbl2' & Hls)" "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. }
+      iMod ("Hcl" with "[Ha Hs1' Hs2' Htbl1' Htbl2' Hls]") as "_".
+      { iNext. iExists _,_. by iFrame. }
+      clear ls.
       rel_let_l.
       rel_op_l.
-      destruct (le_dec n m'); last congruence.
+      destruct (le_dec n m); last congruence.
       rel_if_l.
-      iApply bin_log_related_nat.
+      repeat iApply bin_log_related_app.
+      + iApply binary_fundamental; eauto with typeable.
+      + rel_load_l_atomic.
+        iInv sizeN as (m' ls) "(Ha & Hs1' & Hs2' & Htbl1' & Htbl2' & #Hls)" "Hcl".
+        iModIntro. iExists _. iFrame. iNext. iIntros "Htbl1'".
+        rel_load_r.
+        iMod ("Hcl" with "[Ha Hs1' Hs2' Htbl1' Htbl2']") as "_".
+        { iNext. iExists _,_. by iFrame. }
+        rel_vals; eauto.
+        iModIntro. by iApply LIST_interp_weaken.
+      + iApply bin_log_related_nat_binop; eauto;
+          last by iApply bin_log_related_nat.
+        rel_load_l_atomic.
+        iInv sizeN as (m' ls) "(Ha & Hs1' & Hs2' & Htbl1' & Htbl2' & Hls)" "Hcl".
+        iModIntro. iExists _. iFrame. iNext. iIntros "Hs1'".
+        rel_load_r.
+        iMod ("Hcl" with "[Ha Hs1' Hs2' Htbl1' Htbl2' Hls]") as "_".
+        { iNext. iExists _,_. by iFrame. }
+        iApply bin_log_related_nat.
   Qed.
 End proof.

theories/logrel/threadpool.v

 (* The threadpool RA *)
 From iris.algebra Require Import auth gmap agree list.
 From iris.base_logic Require Export gen_heap invariants fractional.
+From iris.proofmode Require Import tactics.
 From iris_logrel.F_mu_ref_conc Require Import lang.
 Import uPred.
 
@@ -141,4 +142,13 @@ Section mapsto.
     by intros [_ ?%agree_op_invL'].
   Qed.
 
+  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.
+
 End mapsto.