(** 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 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 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 (eqKey, λ: "s", acquire "l";; let: "n" := !"size" in "size" <- "n"+#1;; "tbl" <- Conse "s" (!"tbl");; release "l";; "n", λ: "n", nth (!"tbl") (!"size" - "n")). Definition symbol2 : val := λ: <>, let: "size" := ref #0 in let: "tbl" := ref Nile in let: "l" := newlock #() in 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 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_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_typed : typeable. (** * The actual refinement proof. Requires monotonic state *) 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 : Persistent (tableR ww). Proof. apply _. Qed. 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 eqKey_refinement Δ Γ γ : {tableR γ :: Δ;⤉Γ} ⊨ eqKey ≤log≤ eqKey : TArrow (TVar 0) (TArrow (TVar 0) TBool). Proof. 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 Δ Γ : {Δ;Γ} ⊨ 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. rel_alloc_l as tbl1 "[Htbl1 Htbl1']"; rel_let_l. rel_alloc_r as tbl2 "[Htbl2 Htbl2']"; rel_let_r. iMod (own_alloc (● (0 : mnat))) as (γ) "Ha"; first done. 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. } 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 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 γ)). 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/=. 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 ls) "(Hs1 & Hs2 & Htbl1 & Htbl2 & Hl2)". rel_load_l. rel_let_l. rel_op_l. rel_store_l_atomic. 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 (threadpool.mapsto_half_combine with "Hs2 Hs2'") as "[% Hs2]"; simplify_eq. rel_load_r. repeat (rel_pure_r _). rel_store_r. rel_let_r. (* Before we close the lock, we need to gather some evidence *) iMod (conjure_0 γ) as "Hf". iMod (same_size with "[\$Ha \$Hf]") as "[Ha #Hf]". iMod (inc_size with "Ha") as "Ha". iDestruct "Hs2" as "[Hs2 Hs2']". rewrite Nat.add_1_r. 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. } 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 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' Htbl1' Htbl2' Hls]") as "_". { iNext. iExists _,_. by iFrame. } clear ls. rel_let_l. rel_op_l. destruct (le_dec n m); last congruence. rel_if_l. 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.