Merge branch 'arrays'

_CoqProject

@@ -21,8 +21,7 @@ theories/vcgen/tests/unknowns.v
 theories/vcgen/tests/test.v
 theories/vcgen/tests/swap.v
 theories/vcgen/tests/fact.v
-theories/tests/test1.v
-theories/tests/test2.v
-theories/tests/fact.v
-theories/tests/gcd.v
-theories/tests/lists.v
+# theories/tests/test1.v
+# theories/tests/test2.v
+# theories/tests/gcd.v
+# theories/tests/lists.v

opam

@@ -7,5 +7,5 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris-c-monad"]
 depends: [
-  "coq-iris" { (= "branch.gen_proofmode.2018-06-18.3.33f0c279") | (= "dev") }
+  "coq-iris" { (= "branch.gen_proofmode.2018-06-30.2.29c965ba") | (= "dev") }
 ]

theories/c_translation/derived.v

@@ -4,35 +4,48 @@ From iris.algebra Require Import frac auth.
 From iris_c.lib Require Import locking_heap mset flock U.
 From iris_c.c_translation Require Import proofmode translation.
 
+Class ValToNat (v : val) (n : nat) :=
+  val_to_nat : v = #n.
+
+Global Instance val_to_nat_pos (o : positive) : ValToNat #(Zpos o) (Pos.to_nat o).
+Proof. rewrite /ValToNat. by rewrite -positive_nat_Z. Qed.
+
+Global Instance val_to_nat_zero : ValToNat #0 0%nat.
+Proof. done. Qed.
+
 Section derived.
   Context `{amonadG Σ}.
 
-  Lemma a_load_ret (l: loc) (q : Qp) (w: val) R Φ:
-    l ↦C{q} w ∗ (l ↦C{q} w -∗ Φ w) -∗
-    awp (a_load (a_ret (#l)%E)) R Φ.
+  Lemma a_load_ret (cl: cloc) (q : Qp) (w: val) R Φ:
+    cl ↦C{q} w ∗ (cl ↦C{q} w -∗ Φ w) -∗
+    awp (a_load (a_ret (cloc_to_val cl)%E)) R Φ.
   Proof.
     iIntros "H". iApply a_load_spec.
     iApply awp_ret. wp_value_head.
-    iExists l, w. by iFrame.
+    iExists cl, w. by iFrame.
   Qed.
 
-  Lemma a_alloc_ret (e: expr) (ev: val) R Φ:
-    IntoVal e ev →
-    (∀ l: loc, l ↦C ev -∗ Φ #l) -∗
-    awp (a_alloc (a_ret e)) R Φ.
+  Lemma a_alloc_ret (n: nat) (e1 e2: expr) (ev1 ev2: val) R Φ:
+    IntoVal e1 ev1 →
+    ValToNat ev1 n →
+    IntoVal e2 ev2 →
+    (∀ l: cloc, l ↦C∗ replicate n ev2 -∗ Φ (cloc_to_val l)) -∗
+    awp (a_alloc (a_ret e1) (a_ret e2)) R Φ.
   Proof.
-    iIntros (?) "H". iApply a_alloc_spec.
-    iApply awp_ret. by iApply wp_value.
+    iIntros (? ? ?) "H". iApply (a_alloc_spec _ _ (λ v, ⌜v = #n⌝)%I).
+    - iApply awp_ret. by iApply wp_value.
+    - iApply awp_ret. wp_value_head.
+      iNext. iIntros (? ->). iExists n; iSplit; eauto.
   Qed.
 
-  Lemma a_store_ret (l:loc) (e: expr) `{Closed [] e}  R Φ :
-    awp e R (λ w, ∃ v, l ↦C v ∗ (l ↦C[LLvl] w -∗ Φ w)) -∗
-    awp (a_store (a_ret #l) e) R Φ.
+  Lemma a_store_ret (cl:cloc) (e: expr) `{Closed [] e}  R Φ :
+    awp e R (λ w, ∃ v, cl ↦C v ∗ (cl ↦C[LLvl] w -∗ Φ w)) -∗
+    awp (a_store (a_ret (cloc_to_val cl)) e) R Φ.
   Proof.
     iIntros "H".
     iApply ((a_store_spec _ _
-               (λ l1, ⌜l1 = #l⌝)%I
-               (λ w, ∃ v, (l ↦C v ∗ (l ↦C[LLvl] w -∗ Φ w)))%I ) with "[] [$H] []").
+               (λ l1, ⌜l1 = cloc_to_val cl⌝)%I
+               (λ w, ∃ v, (cl ↦C v ∗ (cl ↦C[LLvl] w -∗ Φ w)))%I ) with "[] [$H] []").
     - iApply awp_ret; iApply wp_value; eauto.
     - iNext. iIntros (? w) "-> H".
       iDestruct "H" as (v) "H".
@@ -43,10 +56,10 @@ Section derived.
   Ltac awp_ret_value := iApply awp_ret; iApply wp_value; eauto.
   Ltac awp_alloc_ret r h := iApply a_alloc_ret; iIntros (r) h; awp_lam.
 
-  Lemma awp_bin_op_load_load op (l r : loc) (v1 v2: val) R Φ :
+  Lemma awp_bin_op_load_load op (l r : cloc) (v1 v2: val) R Φ :
     l ↦C v1 -∗ r ↦C v2 -∗
     (l ↦C v1 -∗ r ↦C v2 -∗ ∃ w : val, ⌜bin_op_eval op v1 v2 = Some w⌝ ∧ Φ w) -∗
-    awp (a_bin_op op (a_load (a_ret #l)) (a_load (a_ret #r))) R Φ.
+    awp (a_bin_op op (a_load (a_ret (cloc_to_val l))) (a_load (a_ret (cloc_to_val r)))) R Φ.
   Proof.
     iIntros "Hl Hr HΦ".
     iApply (a_bin_op_spec _ _
@@ -61,7 +74,7 @@ Section derived.
   Lemma a_pre_bin_op_spec' R Φ Ψ1 Ψ2 e1 e2 op v l :
     l ↦C v -∗
     AWP e1 @ R {{ Ψ1 }} -∗ AWP e2 @ R {{ Ψ2 }} -∗
-    ▷ (∀ v1 v2, Ψ1 v1 -∗ Ψ2 v2 -∗ ⌜v1 = #l⌝ ∗
+    ▷ (∀ v1 v2, Ψ1 v1 -∗ Ψ2 v2 -∗ ⌜v1 = cloc_to_val l⌝ ∗
           ∃ w, ⌜bin_op_eval op v v2 = Some w⌝
           ∗ (l ↦C[LLvl] w -∗ Φ v)) -∗
     AWP a_pre_bin_op op e1 e2 @ R {{ Φ }}.
@@ -76,7 +89,7 @@ Section derived.
 
   Lemma a_pre_incr R Φ e1 l (z : Z) :
     l ↦C #z -∗
-    AWP e1 @ R {{ v, ⌜v = #l⌝ ∗ (l ↦C[LLvl] #(z+1) -∗ Φ #z) }} -∗
+    AWP e1 @ R {{ v, ⌜v = cloc_to_val l⌝ ∗ (l ↦C[LLvl] #(z+1) -∗ Φ #z) }} -∗
     AWP e1 +=ᶜ ♯1 @ R {{ Φ }}.
   Proof.
     iIntros "Hl He1".
@@ -85,9 +98,9 @@ Section derived.
     iNext. iIntros (v1 v2) "[% HΦ] %". simplify_eq/=. eauto.
   Qed.
 
-  Lemma a_move_spec (s t :loc) (v w: val) R Φ :
+  Lemma a_move_spec (s t :cloc) (v w: val) R Φ :
     s ↦C v ∗ t ↦C w ∗ (t ↦C w -∗ s ↦C[LLvl] w -∗ Φ w) -∗
-    awp (a_store (a_ret #s) (a_load (a_ret #t))) R Φ.
+    awp (a_store (a_ret (cloc_to_val s)) (a_load (a_ret (cloc_to_val t)))) R Φ.
   Proof.
     iIntros "(Hs & Ht & H)".
     iApply a_store_ret. awp_load_ret t. iIntros "Ht".
@@ -119,6 +132,30 @@ Section derived.
     iSpecialize ("HΨ" with "HR").
     iApply (awp_wand with "HΨ"). eauto with iFrame.
   Qed.
+
+  Lemma a_ptr_add_ret R Φ Ψ2 e1 e2 :
+    AWP e2 @ R {{ Ψ2 }} -∗
+    AWP e1 @ R {{ v1, ▷ ∀ v2, Ψ2 v2 -∗ ∃ cl (n : nat),
+                         ⌜ v1 = cloc_to_val cl ⌝ ∗
+                         ⌜ v2 = #n ⌝ ∗
+                         Φ (cloc_to_val (cl.1, cl.2+n)%nat) }} -∗
+    AWP a_ptr_add e1 e2 @ R {{ Φ }}.
+  Proof.
+    iIntros "He2 HΦ". rewrite /a_ptr_add.
+    awp_apply (a_wp_awp with "HΦ"); iIntros (a1) "Ha1". awp_lam.
+    awp_apply (a_wp_awp with "He2"); iIntros (a2) "Ha2". awp_lam.
+    iApply awp_bind. iApply (awp_par with "Ha1 Ha2"). iNext.
+    iIntros (v1 v2) "Hv1 Hv2 !>". awp_let.
+    iDestruct ("Hv1" with "Hv2") as (cl n -> ->) "HΦ".
+    destruct cl as [l o]. simpl.
+    iApply awp_bind. iApply (a_bin_op_spec _ _ (λ v, ⌜v = #o⌝)%I (λ v, ⌜v = #n⌝)%I); repeat awp_proj;
+    try by (iApply awp_ret; wp_value_head).
+    iNext. iIntros (? ? -> ->). iExists #(o+n); iSplit; eauto.
+    awp_let. repeat awp_proj. iApply awp_ret; wp_value_head.
+    rewrite -Nat2Z.inj_add.
+    iApply "HΦ".
+  Qed.
+
 End derived.
 
 Ltac awp_load_ret l := iApply (a_load_ret l); iFrame; eauto.

theories/c_translation/monad.v

@@ -61,31 +61,27 @@ Class amonadG (Σ : gFunctors) := AMonadG {
 Section a_wp.
   Context `{amonadG Σ}.
 
-  (* X ⊆ σ^{-1}(L) *)
-  Definition correct_locks (X : gset val) (preσ : gset loc) : Prop :=
-    set_Forall (λ v, ∃ l : loc, v = #l ∧ l ∈ preσ) X.
-
   Definition env_inv (env : val) : iProp Σ :=
-    (∃ (X : gset val) (σ : gmap loc (lvl*val)),
-         is_mset env X
-       ∗ full_locking_heap σ
-       ∗ ⌜correct_locks X (locked_locs σ)⌝)%I.
+    (∃ (X : gset val) (σ : gmap cloc (lvl * val)),
+      ⌜ ∀ v, v ∈ X → ∃ cl, cloc_of_val v = Some cl ∧ cl ∈ locked_locs σ ⌝ ∧
+      is_mset env X ∗
+      full_locking_heap σ)%I.
 
   Definition flock_resources (γ : flock_name) (I : gmap prop_id (iProp Σ * frac)) :=
     ([∗ map] i ↦ p ∈ I, flock_res γ i p.1 p.2)%I.
 
   Definition awp (e : expr)
       (R : iProp Σ) (Φ : val → iProp Σ) : iProp Σ :=
-    tc_opaque (WP e {{ ev, ∀ (γ : flock_name) (env : val) (l : val) (I : gmap prop_id (iProp Σ * frac)),
-      is_flock amonadN γ l -∗
-      flock_resources γ I -∗
-      (([∗ map] p ∈ I, p.1) ≡ (env_inv env ∗ R)) -∗
-      WP ev env l {{ v, Φ v ∗ flock_resources γ I }}
+    tc_opaque (WP e {{ ev,
+      ∀ (γ : flock_name) (env : val) (l : val) (I : gmap prop_id (iProp Σ * frac)),
+        is_flock amonadN γ l -∗
+        flock_resources γ I -∗
+        ([∗ map] p ∈ I, p.1) ≡ (env_inv env ∗ R) -∗
+        WP ev env l {{ v, Φ v ∗ flock_resources γ I }}
     }})%I.
 
   Global Instance elim_bupd_awp p e Φ :
-   ElimModal True p false (|==> P) P
-     (awp e R Φ) (awp e R Φ).
+    ElimModal True p false (|==> P) P (awp e R Φ) (awp e R Φ).
   Proof.
     iIntros (P R _) "[HP HA]".
     rewrite /awp /tc_opaque /= bi.intuitionistically_if_elim.
@@ -234,8 +230,8 @@ Section a_wp_rules.
   Lemma awp_atomic_env (e : expr) (ev : val) R Φ :
     IntoVal e ev →
     (∀ env, env_inv env -∗ R -∗
-      WP ev env {{ w, ▷ env_inv env ∗ ▷ R ∗ ▷ Φ w }}) -∗
-    AWP (a_atomic_env e) @ R {{ Φ }}.
+      WP ev env {{ w, ▷ (env_inv env ∗ R ∗ Φ w) }}) -∗
+    AWP a_atomic_env e @ R {{ Φ }}.
   Proof.
     iIntros (<-) "Hwp". rewrite /awp /a_atomic_env /=. wp_lam.
     iIntros (γ env l I) "#Hlock Hres #Heq". do 2 wp_lam.
@@ -255,7 +251,7 @@ Section a_wp_rules.
     AWP e1 @ R {{ Ψ1 }} -∗
     ▷ AWP e2 @ R {{ Ψ2 }} -∗
     ▷ (∀ w1 w2, Ψ1 w1 -∗ Ψ2 w2 -∗ ▷ Φ (w1,w2)%V) -∗
-    AWP (a_par e1 e2) @ R {{ Φ }}.
+    AWP e1 |||ᶜ e2 @ R {{ Φ }}.
   Proof.
     iIntros "Hwp1 Hwp2 HΦ". rewrite /a_par /awp /=.
     wp_bind e1. iApply (wp_wand with "Hwp1").
@@ -303,8 +299,8 @@ Section a_wp_run.
     wp_apply (newlock_cancel_spec amonadN); first done.
     iIntros (k γ') "#Hlock". rewrite- wp_fupd.
     iMod (flock_res_single_alloc _ ∅ _ _ (env_inv env ∗ R)%I
-            with "Hlock [Henv Hσ $HR]") as (i) "[_ Hres]"; first done.
-    { iNext. iExists ∅, ∅. iFrame. eauto. }
+      with "Hlock [Henv Hσ $HR]") as (i) "[_ Hres]"; first done.
+    { iNext. iExists ∅, ∅. iFrame. iPureIntro; set_solver. }
     iSpecialize ("Hwp" $! amg).
     iMod (wp_value_inv with "Hwp") as "Hwp".
     wp_let. wp_bind (ev env k).

theories/c_translation/translation.v

 From iris.heap_lang Require Export proofmode notation.
-From iris.heap_lang Require Import spin_lock assert par.
+From iris.heap_lang Require Import assert par.
 From iris.algebra Require Import frac auth.
-From iris_c.lib Require Import locking_heap mset flock U.
+From iris_c.lib Require Import mset flock list.
+From iris_c.lib Require Export locking_heap U.
+From iris_c.c_translation Require Export monad.
 From iris_c.c_translation Require Import proofmode.
 
 Notation "♯ l" := (a_ret (LitV l%Z%V)) (at level 8, format "♯ l").
 Notation "♯ l" := (a_ret (Lit l%Z%V)) (at level 8, format "♯ l") : expr_scope.
+Notation "♯ₗ l" := (a_ret (cloc_to_val l)) (at level 8, format "♯ₗ l") : expr_scope.
 
-Definition a_alloc : val := λ: "x",
-  "v" ←ᶜ "x" ;;ᶜ
-  a_atomic_env (λ: <>, ref "v").
-Notation "'allocᶜ' e1" := (a_alloc e1%E) (at level 80) : expr_scope.
+Definition a_alloc : val := λ: "x1" "x2",
+  "vv" ←ᶜ "x1" |||ᶜ "x2" ;;ᶜ
+  let: "n" := Fst "vv" in
+  let: "v" := Snd "vv" in
+  a_atomic_env (λ: <>, (ref (lreplicate "n" "v"), #0)).
+Notation "'allocᶜ' ( e1 , e2 )" := (a_alloc e1%E e2%E) (at level 80) : expr_scope.
 
 Definition a_store : val := λ: "x1" "x2",
   "vv" ←ᶜ "x1" |||ᶜ "x2" ;;ᶜ
   a_atomic_env (λ: "env",
-    mset_add (Fst "vv") "env" ;;
-    Fst "vv" <- Snd "vv" ;;
-    Snd "vv"
+    let: "l" := Fst (Fst "vv") in
+    let: "i" := Snd (Fst "vv") in
+    let: "v" := Snd "vv" in
+    mset_add ("l", "i") "env" ;;
+    let: "ll" := !"l" in
+    "l" <- linsert "i" "v" "ll" ;;
+    "v"
   ).
 Notation "e1 =ᶜ e2" := (a_store e1%E e2%E) (at level 80) : expr_scope.
 
 Definition a_load : val := λ: "x",
   "v" ←ᶜ "x";;ᶜ
   a_atomic_env (λ: "env",
-    assert: (mset_member "v" "env" = #false);;
-    !"v"
+    let: "l" := Fst "v" in
+    let: "i" := Snd "v" in
+    assert: (mset_member ("l", "i") "env" = #false);;
+    let: "ll" := !"l" in
+    llookup "i" "ll"
   ).
 Notation "∗ᶜ e" :=
   (a_load e)%E (at level 9, right associativity) : expr_scope.
@@ -89,63 +101,58 @@ Notation "'whileᶜ' ( e1 ) { e2 }" := (a_while (λ:<>, e1)%E (λ:<>, e2)%E)
 
 Definition a_invoke: val := λ: "f" "arg",
   a_seq_bind (λ: "a", a_atomic (λ: <>, "f" "a")) "arg".
-
 Notation "f ❲ a ❳ " :=
   ( a_invoke f a)%E
   (at level 100, a at level 200,
    format "f ❲ a ❳") : expr_scope.
 
-
+Definition a_ptr_add : val := λ: "x" "y",
+  "lo" ←ᶜ ("x" |||ᶜ "y");;ᶜ
+  "o'" ←ᶜ ((a_ret (Snd (Fst "lo")) +ᶜ (a_ret (Snd "lo")))) ;;ᶜ
+  a_ret (Fst (Fst "lo"), "o'").
+
+Definition a_ptr_lt : val := λ: "x" "y",
+  "pq" ←ᶜ ("x" |||ᶜ "y");;ᶜ
+  let: "p" := Fst "pq" in
+  let: "q" := Snd "pq" in
+  ifᶜ ((a_ret (Fst "p")) ==ᶜ (a_ret (Fst "q")))
+  { (a_ret (Snd "p")) <ᶜ (a_ret (Snd "q")) }
+  elseᶜ { ♯false }.
+Notation "e1 +∗ᶜ e2" := (a_ptr_add e1%E e2%E) (at level 80) : expr_scope.
+Notation "e1 <∗ᶜ e2" := (a_ptr_lt e1%E e2%E)  (at level 80) : expr_scope.
 
 Section proofs.
   Context `{amonadG Σ}.
 
-  Lemma a_alloc_spec R Φ e :
-    AWP e @ R {{ v, ∀ l : loc, l ↦C v -∗ Φ #l }} -∗
-    AWP allocᶜ e @ R {{ Φ }}.
+  Lemma a_alloc_spec R Φ Ψ1 e1 e2 :
+    AWP e1 @ R {{ Ψ1 }} -∗
+    AWP e2 @ R {{ v2, ▷ (∀ v1, Ψ1 v1 -∗ ∃ n : nat,
+                          ⌜ v1 = #n ⌝ ∧
+                          ∀ l, l ↦C∗ replicate n v2 -∗ Φ (cloc_to_val l)) }} -∗
+    AWP allocᶜ(e1, e2) @ R {{ Φ }}.
   Proof.
-    iIntros "H". awp_apply (a_wp_awp with "H"); iIntros (v) "H". awp_lam.
-    iApply awp_bind.
-    iApply (awp_wand with "H"). clear v.
-    iIntros (v) "H". awp_lam.
+    iIntros "H1 HΦ".
+    awp_apply (a_wp_awp with "H1"); iIntros (v1) "H1". awp_lam.
+    awp_apply (a_wp_awp with "HΦ"); iIntros (v2) "H2". awp_lam.
+    iApply awp_bind. iApply (awp_par with "H1 H2").
+    iIntros "!>" (w1 w2) "H1 H2 !>". awp_let. do 2 (awp_proj; awp_let).
+    iDestruct ("H2" with "H1") as (n ->) "HΦ".
     iApply awp_atomic_env.
-    iIntros (env) "Henv HR".
-    rewrite {2}/env_inv.
-    iDestruct "Henv" as (X σ) "(HX & Hσ & Hlocks)".
-    iDestruct "Hlocks" as %Hlocks.
-    iApply wp_fupd.
-    wp_let. wp_alloc l as "Hl".
-    iAssert ⌜σ !! l = None⌝%I with "[Hl Hσ]" as %Hl.
-    { remember (σ !! l) as σl. destruct σl as [[? ?]|]; simplify_eq; eauto.
-      iDestruct "Hσ" as "[_ Hls]".
-      iExFalso. rewrite (big_sepM_lookup _ σ l _); last eauto.
-      by iDestruct (mapsto_valid_2 l with "Hl Hls") as %[]. }
-    iMod (locking_heap_alloc σ l ULvl v with "Hl Hσ") as "[Hσ Hl']"; eauto.
-    iModIntro. iFrame "HR". iSplitR "H Hl'".
-    - iExists X,(<[l:=(ULvl,v)]>σ). iFrame.
-      iPureIntro. by rewrite locked_locs_alloc_unlocked.
-    - iApply ("H" with "Hl'").
-  Qed.
-
-  (* DF TODO: move this somewhere else? *)
-  Lemma big_sepM_insert_overwrite `{Countable K, EqDecision K} {A : Type}
-        (Φ : K → A → iProp Σ) (m : gmap K A) i x x' :
-    m !! i = Some x →
-    ([∗ map] k↦y ∈ m, Φ k y) ⊢
-      Φ i x ∗ (Φ i x' -∗ ([∗ map] k↦y ∈ <[i:=x']> m, Φ k y)).
-  Proof.
-    intros ?.
-    rewrite {1}big_sepM_delete //. iIntros "[$ ?]".
-    rewrite -insert_delete big_sepM_insert ?lookup_delete //.
-    eauto with iFrame.
+    iIntros (env). iDestruct 1 as (X σ HX) "[Hlocks Hσ]". iIntros "$". wp_let.
+    wp_apply (lreplicate_spec with "[//]"); iIntros (ll Hll).
+    iApply wp_fupd. wp_alloc l as "Hl".
+    iMod (locking_heap_alloc with "Hσ Hl") as (?) "[Hσ Hl]"; first done.
+    iIntros "!> !>". iSplitL "Hlocks Hσ"; [|by iApply ("HΦ" $! (l, 0%nat))].
+    iExists X, _. iFrame.
+    iIntros "!%". intros w Hw. destruct (HX _ Hw) as (cl&Hcl&Hin).
+    exists cl; split; first done. by rewrite locked_locs_alloc_heap.
   Qed.
 
   Lemma a_store_spec R Φ Ψ1 Ψ2 e1 e2 :
     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)) -∗
+    ▷ (∀ v1 v2, Ψ1 v1 -∗ Ψ2 v2 -∗ ∃ cl w,
+                ⌜ v1 = cloc_to_val cl ⌝ ∧ cl ↦C w ∗ (cl ↦C[LLvl] v2 -∗ Φ v2)) -∗
     AWP e1 =ᶜ e2 @ R {{ Φ }}.
   Proof.
     iIntros "H1 H2 HΦ".
@@ -153,91 +160,61 @@ Section proofs.
     awp_apply (a_wp_awp with "H2"); iIntros (v2) "H2". awp_lam.
     iApply awp_bind. iApply (awp_par with "H1 H2").
     iIntros "!>" (w1 w2) "H1 H2 !>". awp_lam.
-    iDestruct ("HΦ" with "H1 H2") as (l w ->) "[Hl HΦ]".
+    iDestruct ("HΦ" with "H1 H2") as ([l i] w ->) "[Hl HΦ]".
     iApply awp_atomic_env.
-    iIntros (env) "Henv HR".
-    rewrite {2}/env_inv.
-    iDestruct "Henv" as (X σ) "(HX & Hσ & Hlocks)".
-    iDestruct "Hlocks" as %Hlocks.
-    iDestruct (locked_locs_unlocked with "Hl Hσ") as %Hl.
-    assert (#l ∉ X).
-    { 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"); first done.
-    iIntros "HX". wp_seq.
-    iDestruct (full_locking_heap_unlocked with "Hl Hσ") as %?.
-    do 2 wp_proj.
-    iDestruct "Hσ" as "[Hσ Hls]".
-    rewrite {1}mapsto_eq /mapsto_def.
-    iDestruct "Hl" as (b' Hb%lvl_included) "Hl".
-    assert (b' = ULvl) as -> by (destruct b'; naive_solver).
-    rewrite (big_sepM_insert_overwrite _ _ l _ (ULvl, w2)) ?lookup_insert //.
-    iDestruct "Hls" as "[Hl' Hls] /=".
-    wp_store.
-    iSpecialize ("Hls" with "Hl'").
-    iMod (own_update_2 with "Hσ Hl") as "[Hσ Hl]".
-    { apply (auth_update _ _ (to_locking_heap (<[l:=(ULvl,w2)]>σ)) {[l := (1%Qp, ULvl, agree.to_agree w2)]}).
-      rewrite !to_locking_heap_insert.
-      eapply (gmap.singleton_local_update (to_locking_heap σ)); first by apply to_locking_heap_lookup_Some.
-      by apply exclusive_local_update. }
-    iCombine "Hσ Hls" as "Hσ".
-    iMod (locking_heap_change_lock _ _ ULvl LLvl with "Hσ [Hl]") as "[Hσ Hl]".
-    { rewrite mapsto_eq /mapsto_def. eauto. }
-    wp_proj. iFrame "HR". iSplitR "HΦ Hl".
-    - iExists ({[#l]} ∪ X),(<[l:=(LLvl,w2)]> σ). iFrame. iSplitL.
-      + rewrite /full_locking_heap insert_insert //.
-      + (* TODO: a separate lemma somewhere *)
-        iPureIntro. rewrite locked_locs_lock.
-        revert Hlocks. rewrite /correct_locks /set_Forall. set_solver.
-    - by iApply "HΦ".
+    iIntros (env). iDestruct 1 as (X σ HX) "[Hlocks Hσ]". iIntros "HR".
+    iDestruct (locked_locs_unlocked with "Hl Hσ") as %Hw1.
+    assert ((#l, #i)%V ∉ X).
+    { intros Hcl. destruct (HX _ Hcl) as ([??]&[=]%cloc_to_of_val&?); naive_solver. }
+    iMod (locking_heap_store with "Hσ Hl") as (ll vs Hl Hi) "[Hl Hclose]".
+    wp_let. do 2 wp_proj; wp_let. do 2 wp_proj; wp_let. wp_proj; wp_let.
+    wp_apply (mset_add_spec with "[$]"); first done.
+    iIntros "Hlocks /="; wp_seq.
+    wp_load; wp_let.
+    wp_apply (linsert_spec with "[//]"); [eauto|]; iIntros (ll' Hl').
+    iApply wp_fupd. wp_store.
+    iMod ("Hclose" $! _ LLvl with "[//] Hl") as "[Hσ Hl]".
+    iIntros "!> !> {$HR}". iSplitL "Hlocks Hσ"; last by iApply "HΦ".
+    iExists ({[(#l, #i)%V]} ∪ X), _. iFrame "Hσ". rewrite locked_locs_lock.
+    iIntros "{$Hlocks} !%".
+    intros v [->%elem_of_singleton|?]%elem_of_union; last set_solver.
+    eexists; split; [apply (cloc_of_to_val (l,i))|set_solver].
   Qed.
 
   Lemma a_load_spec_exists_frac R Φ e :
-    AWP e @ R {{ v, ∃ (l : loc) (q : Qp) (w : val), ⌜v = #l⌝ ∗ l ↦C{q} w ∗ (l ↦C{q} w -∗ Φ w) }} -∗
+    AWP e @ R {{ v, ∃ cl q w, ⌜ v = cloc_to_val cl ⌝ ∧
+                              cl ↦C{q} w ∗ (cl ↦C{q} w -∗ Φ w) }} -∗
     AWP ∗ᶜe @ R {{ Φ }}.
   Proof.
     iIntros "H".
     awp_apply (a_wp_awp with "H"); iIntros (v) "H". awp_lam.
-    iApply awp_bind.
-    iApply (awp_wand with "H"). clear v.
-    iIntros (v). iDestruct 1 as (l q w) "(% & Hl & HΦ)". subst.
-    awp_lam.
-    iApply awp_atomic_env.
-    iIntros (env) "Henv HR".
-    rewrite {2}/env_inv.
-    iDestruct "Henv" as (X σ) "(HX & Hσ & Hlocks)".
-    iDestruct "Hlocks" as %Hlocks.
-    iDestruct (locked_locs_unlocked with "Hl Hσ") as %Hl.
-    assert (#l ∉ X).
-    { unfold correct_locks in *. intros Hx. apply Hl.
-      destruct (Hlocks _ Hx) as [l' [? Hl']]. by simplify_eq/=. }
-    wp_lam. wp_apply wp_assert.
-    wp_apply (mset_member_spec with "HX").
-    iIntros "Henv /=". case_decide; first by exfalso. simpl.
-    wp_op. iSplit; eauto. iNext. wp_seq.
-    iDestruct (full_locking_heap_unlocked with "Hl Hσ") as %Hσl.
-    rewrite mapsto_eq /mapsto_def.
-    iDestruct "Hl" as (b' Hb%lvl_included) "Hl".
-    assert (b' = ULvl) as -> by (destruct b'; naive_solver).
-    iDestruct "Hσ" as "[Hσ Hls]".
-    rewrite (big_sepM_lookup_acc _ _ l) //. iDestruct "Hls" as "[Hl' Hls] /=".
-    wp_load. iSpecialize ("Hls" with "Hl'").
-    iFrame "HR".
-    iSplitR "HΦ Hl".
-    - iExists X,σ. by iFrame.
-    - iApply "HΦ". eauto.
+    iApply awp_bind. iApply (awp_wand with "H"). clear v.
+    iIntros (v). iDestruct 1 as ([l i] q w ->) "[Hl HΦ]". awp_lam.
+    iApply awp_atomic_env. iIntros (env) "Henv HR".
+    iDestruct "Henv" as (X σ HX) "[Hlocks Hσ]".
+    iDestruct (locked_locs_unlocked with "Hl Hσ") as %Hv.
+    assert ((#l, #i)%V ∉ X).
+    { intros Hcl. destruct (HX _ Hcl) as ([??]&[=]%cloc_to_of_val&?); naive_solver. }
+    iMod (locking_heap_load with "Hσ Hl") as (ll vs Hl Hi) "[Hl Hclose]".
+    wp_let. wp_proj; wp_let. wp_proj; wp_let.
+    wp_apply wp_assert. wp_apply (mset_member_spec with "Hlocks"); iIntros "Hlocks /=".
+    rewrite bool_decide_false //.
+    wp_op. iSplit; first done. iNext; wp_seq.
+    wp_load; wp_let. wp_apply (llookup_spec with "[//]"); [done|]; iIntros "_".
+    iDestruct ("Hclose" with "Hl") as "[Hσ Hl]".
+    iIntros "!> {$HR}". iSplitL "Hlocks Hσ"; last by iApply "HΦ".
+    iExists X, _. by iFrame.
   Qed.
 
   Lemma a_load_spec R Φ q e :
-    AWP e @ R {{ v, ∃ (l : loc) (w : val), ⌜v = #l⌝ ∗ l ↦C{q} w ∗ (l ↦C{q} w -∗ Φ w) }} -∗
+    AWP e @ R {{ v, ∃ cl w,
+                    ⌜ v = cloc_to_val cl ⌝ ∧
+                    cl ↦C{q} w ∗ (cl ↦C{q} w -∗ Φ w) }} -∗
     AWP ∗ᶜe @ R {{ Φ }}.
   Proof.
-    iIntros "H".
-    iApply a_load_spec_exists_frac.
+    iIntros "H". iApply a_load_spec_exists_frac.
     awp_apply (awp_wand with "H").
-    iIntros (v) "H". iDestruct "H" as (l w ->) "[H1 H2]".
-    eauto with iFrame.
+    iIntros (v). iDestruct 1 as (cl w ->) "[H1 H2]"; eauto with iFrame.