symbol.v 13 KB
Newer Older
1 2 3 4 5 6 7
(** 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. *)
8 9
From iris.proofmode Require Import tactics.
From iris.algebra Require Import auth.
10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67
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.
68

69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101
(* `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".
102 103
Definition symbol1 : val := λ: <>,
  let: "size" := ref #0 in
104
  let: "tbl" := ref Nile in
105
  let: "l" := newlock #() in
106 107
  Pack (eqKey,
        λ: "s", acquire "l";;
108 109
                let: "n" := !"size" in
                "size" <- "n"+#1;;
110
                "tbl" <- Conse "s" (!"tbl");;
111 112
                release "l";;
                "n",
113
        λ: "n", nth (!"tbl") (!"size" - "n")).
114 115
Definition symbol2 : val := λ: <>,
  let: "size" := ref #0 in
116
  let: "tbl" := ref Nile in
117
  let: "l" := newlock #() in
118 119
  Pack (eqKey,
        λ: "s", acquire "l";;
120 121
                let: "n" := !"size" in
                "size" <- "n"+#1;;
122
                "tbl" <- Conse "s" (!"tbl");;
123 124 125
                release "l";;
                "n",
        λ: "n", let: "m" := !"size" in
126 127 128 129 130 131
                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 Γ :
132 133 134 135
  typed Γ symbol1 (TArrow TUnit SYMBOL).
Proof.
  unfold SYMBOL.
  solve_typed.
136 137 138 139 140 141 142 143 144 145 146 147 148
  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.
149
Qed.
150 151
Hint Resolve symbol1_typed : typeable.
Lemma symbol2_typed Γ :
152 153 154 155
  typed Γ symbol2 (TArrow TUnit SYMBOL).
Proof.
  unfold SYMBOL.
  solve_typed.
156 157 158 159 160 161 162 163 164 165 166 167 168
  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.
169
Qed.
170
Hint Resolve symbol2_typed : typeable.
171

172 173
(** * The actual refinement proof.
      Requires monotonic state *)
174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229
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.

Dan Frumin's avatar
Dan Frumin committed
230
  Instance tableR_persistent ww : Persistent (tableR ww).
231 232
  Proof. apply _. Qed.

233 234 235 236 237
  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.
238

239 240 241 242
  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.
243 244 245 246 247
End rules.

Section proof.
  Context `{!logrelG Σ, !msizeG Σ, !lockG Σ}.

248
  Lemma eqKey_refinement Δ Γ γ :
249
    {,;tableR γ :: Δ;⤉Γ} 
250 251 252
      eqKey
    log
      eqKey : TArrow (TVar 0) (TArrow (TVar 0) TBool).
253
  Proof.
254 255 256 257 258 259 260 261 262 263 264
    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.
265 266 267 268 269 270 271 272 273 274 275
  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.
276 277
    rel_alloc_l as tbl1 "[Htbl1 Htbl1']"; rel_let_l.
    rel_alloc_r as tbl2 "[Htbl2 Htbl2']"; rel_let_r.
278
    iMod (own_alloc ( (0 : mnat))) as (γ) "Ha"; first done.
279 280
    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. }
281 282 283
    rel_apply_r bin_log_related_newlock_r; first done.
    iIntros (l2) "Hl2". rel_let_r.
    pose (N:=(logrelN.@"lock1")).
284 285
    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. }
286 287
    iIntros (l1 γl) "#Hl1". rel_let_l.
    iApply (bin_log_related_pack _ (tableR γ)).
288 289 290
    repeat iApply bin_log_related_pair.
    (* Eq *)
    - iApply eqKey_refinement.
291 292 293 294 295 296 297
    (* 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.
298
      iDestruct "Htbl" as (m ls) "(Hs1 & Hs2 & Htbl1 & Htbl2 & Hl2)".
299 300 301 302
      rel_load_l.
      rel_let_l.
      rel_op_l.
      rel_store_l_atomic.
303
      iInv sizeN as (m' ls') "(Ha & >Hs1' & >Hs2' & >Htbl1' & >Htbl2' & #Hls)" "Hcl".
304
      iDestruct (mapsto_half_combine with "Hs1 Hs1'") as "[% Hs1]"; simplify_eq.
305
      iDestruct (mapsto_half_combine with "Htbl1 Htbl1'") as "[% [Htbl1 Htbl1']]"; simplify_eq.
306 307 308 309 310
      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.
311
      iDestruct (threadpool.mapsto_half_combine with "Hs2 Hs2'") as "[% Hs2]"; simplify_eq.
312 313 314 315 316 317 318 319 320 321
      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.
322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341
      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. }
342
      rel_apply_l (bin_log_related_release_l with "Hl1 Hlk [-]"); auto.
343
      { iExists _,_. by iFrame. }
344 345 346 347 348 349 350 351 352 353
      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.
354
      iInv sizeN as (m ls) "(Ha & Hs1' & >Hs2' & >Htbl1' & >Htbl2' & Hls)" "Hcl".
355 356 357
      iModIntro. iExists _. iFrame. iNext. iIntros "Hs1'".
      iDestruct (own_valid_2 with "Ha Hn")
        as %[?%mnat_included _]%auth_valid_discrete_2.
358 359 360
      iMod ("Hcl" with "[Ha Hs1' Hs2' Htbl1' Htbl2' Hls]") as "_".
      { iNext. iExists _,_. by iFrame. }
      clear ls.
361 362
      rel_let_l.
      rel_op_l.
363
      destruct (le_dec n m); last congruence.
364
      rel_if_l.
365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383
      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.
384 385
  Qed.
End proof.