lambda-rust/lang/lib/lock.v

+From iris.program_logic Require Import weakestpre.
+From iris.proofmode Require Import proofmode.
+From iris.algebra Require Import excl.
+From lrust.lang Require Import lang proofmode notation.
+From iris.prelude Require Import options.
+
+Definition mklock_unlocked : val := λ: ["l"], "l" <- #false.
+Definition mklock_locked : val := λ: ["l"], "l" <- #true.
+Definition try_acquire : val := λ: ["l"], CAS "l" #false #true.
+Definition acquire : val :=
+  rec: "acquire" ["l"] := if: try_acquire ["l"] then #☠ else "acquire" ["l"].
+Definition release : val := λ: ["l"], "l" <-ˢᶜ #false.
+
+(* It turns out that we need an accessor-based spec so that we can put the
+   protocol into shared borrows.  Cancellable invariants don't work because
+   their cancelling view shift has a non-empty mask, and it would have to be
+   executed in the consequence view shift of a borrow. *)
+Section proof.
+  Context `{!lrustGS Σ}.
+
+  Definition lock_proto (l : loc) (R : iProp Σ) : iProp Σ :=
+    (∃ b : bool, l ↦ #b ∗ if b then True else R)%I.
+
+  Global Instance lock_proto_ne l : NonExpansive (lock_proto l).
+  Proof. solve_proper. Qed.
+  Global Instance lock_proto_proper l : Proper ((≡) ==> (≡)) (lock_proto l).
+  Proof. apply ne_proper, _. Qed.
+
+  Lemma lock_proto_iff l R R' :
+    □ (R ↔ R') -∗ lock_proto l R -∗ lock_proto l R'.
+  Proof.
+    iIntros "#HRR' Hlck". iDestruct "Hlck" as (b) "[Hl HR]". iExists b.
+    iFrame "Hl". destruct b; first done. by iApply "HRR'".
+  Qed.
+
+  Lemma lock_proto_iff_proper l R R' :
+    □ (R ↔ R') -∗ □ (lock_proto l R ↔ lock_proto l R').
+  Proof.
+    iIntros "#HR !>". iSplit; iIntros "Hlck"; iApply (lock_proto_iff with "[HR] Hlck").
+    - done.
+    - iModIntro; iSplit; iIntros; by iApply "HR".
+  Qed.
+
+  (** The main proofs. *)
+  Lemma lock_proto_create (R : iProp Σ) l (b : bool) :
+    l ↦ #b -∗ (if b then True else ▷ R) ==∗ ▷ lock_proto l R.
+  Proof.
+    iIntros "Hl HR". iExists _. iFrame "Hl". destruct b; first done. by iFrame.
+  Qed.
+
+  Lemma lock_proto_destroy l R :
+    lock_proto l R -∗ ∃ (b : bool), l ↦ #b ∗ if b then True else R.
+  Proof.
+    iIntros "Hlck". iDestruct "Hlck" as (b) "[Hl HR]". auto with iFrame.
+  Qed.
+
+  Lemma mklock_unlocked_spec (R : iProp Σ) (l : loc) v :
+    {{{ l ↦ v ∗ ▷ R }}} mklock_unlocked [ #l ] {{{ RET #☠; ▷ lock_proto l R }}}.
+  Proof.
+    iIntros (Φ) "[Hl HR] HΦ". wp_lam. rewrite -wp_fupd. wp_write.
+    iMod (lock_proto_create with "Hl HR") as "Hproto".
+    iApply "HΦ". by iFrame.
+  Qed.
+
+  Lemma mklock_locked_spec (R : iProp Σ) (l : loc) v :
+    {{{ l ↦ v }}} mklock_locked [ #l ] {{{ RET #☠; ▷ lock_proto l R }}}.
+  Proof.
+    iIntros (Φ) "Hl HΦ". wp_lam. rewrite -wp_fupd. wp_write.
+    iMod (lock_proto_create with "Hl [//]") as "Hproto".
+    iApply "HΦ". by iFrame.
+  Qed.
+
+  (* At this point, it'd be really nice to have some sugar for symmetric
+     accessors. *)
+  Lemma try_acquire_spec E l R P :
+    □ (P ={E,∅}=∗ ▷ lock_proto l R ∗ (▷ lock_proto l R ={∅,E}=∗ P)) -∗
+    {{{ P }}} try_acquire [ #l ] @ E
+    {{{ b, RET #b; (if b is true then R else True) ∗ P }}}.
+  Proof.
+    iIntros "#Hproto !> * HP HΦ".
+    wp_rec. iMod ("Hproto" with "HP") as "(Hinv & Hclose)".
+    iDestruct "Hinv" as ([]) "[Hl HR]".
+    - wp_apply (wp_cas_int_fail with "Hl"); [done..|]. iIntros "Hl".
+      iMod ("Hclose" with "[Hl]"); first (iExists true; by eauto).
+      iModIntro. iApply ("HΦ" $! false). auto.
+    - wp_apply (wp_cas_int_suc with "Hl"); [done..|]. iIntros "Hl".
+      iMod ("Hclose" with "[Hl]") as "HP"; first (iExists true; by eauto).
+      iModIntro. iApply ("HΦ" $! true); iFrame.
+  Qed.
+
+  Lemma acquire_spec E l R P :
+    □ (P ={E,∅}=∗ ▷ lock_proto l R ∗ (▷ lock_proto l R ={∅,E}=∗ P)) -∗
+    {{{ P }}} acquire [ #l ] @ E {{{ RET #☠; R ∗ P }}}.
+  Proof.
+    iIntros "#Hproto !> * HP HΦ". iLöb as "IH". wp_rec.
+    wp_apply (try_acquire_spec with "Hproto HP"). iIntros ([]).
+    - iIntros "[HR Hown]". wp_if. iApply "HΦ"; iFrame.
+    - iIntros "[_ Hown]". wp_if. iApply ("IH" with "Hown HΦ").
+  Qed.
+
+  Lemma release_spec E l R P :
+    □ (P ={E,∅}=∗ ▷ lock_proto l R ∗ (▷ lock_proto l R ={∅,E}=∗ P)) -∗
+    {{{ R ∗ P }}} release [ #l ] @ E {{{ RET #☠; P }}}.
+  Proof.
+    iIntros "#Hproto !> * (HR & HP) HΦ". wp_let.
+    iMod ("Hproto" with "HP") as "(Hinv & Hclose)".
+    iDestruct "Hinv" as (b) "[? _]". wp_write. iApply "HΦ".
+    iApply "Hclose". iExists false. by iFrame.
+  Qed.
+End proof.
+
+Global Typeclasses Opaque lock_proto.

theories/lang/memcpy.v → lambda-rust/lang/lib/memcpy.v

-From iris.base_logic.lib Require Import namespaces.
 From lrust.lang Require Export notation.
 From lrust.lang Require Import heap proofmode.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
 
 Definition memcpy : val :=
   rec: "memcpy" ["dst";"len";"src"] :=
-    if: "len" ≤ #0 then #()
+    if: "len" ≤ #0 then #☠
     else "dst" <- !"src";;
          "memcpy" ["dst" +ₗ #1 ; "len" - #1 ; "src" +ₗ #1].
-Global Opaque memcpy.
 
-Notation "e1 <⋯ !{ n } e2" :=
+Notation "e1 <-{ n } ! e2" :=
   (memcpy (@cons expr e1%E
           (@cons expr (Lit n)
           (@cons expr e2%E nil))))
-  (at level 80, n at next level, format "e1  <⋯  !{ n } e2") : expr_scope.
+  (at level 80, n at next level, format "e1  <-{ n }  ! e2") : expr_scope.
 
-Notation "e1 <⋯{ i } !{ n } e2" :=
-  (e1 <-{i} ☇ ;; e1+ₗ#1 <⋯ !{n}e2)%E
+Notation "e1 <-{ n ',Σ' i } ! e2" :=
+  (e1 <-{Σ i} () ;; e1+ₗ#1 <-{n} !e2)%E
   (at level 80, n, i at next level,
-   format "e1  <⋯{ i }  !{ n } e2") : expr_scope.
+   format "e1  <-{ n ,Σ  i }  ! e2") : expr_scope.
 
-Lemma wp_memcpy `{heapG Σ} E l1 l2 vl1 vl2 q n:
-  ↑heapN ⊆ E →
-  length vl1 = n → length vl2 = n →
-  {{{ heap_ctx ∗ l1 ↦∗ vl1 ∗ l2 ↦∗{q} vl2 }}}
-    #l1 <⋯ !{n}#l2 @ E
-  {{{ RET #(); l1 ↦∗ vl2 ∗ l2 ↦∗{q} vl2 }}}.
+Lemma wp_memcpy `{!lrustGS Σ} E l1 l2 vl1 vl2 q (n : Z):
+  Z.of_nat (length vl1) = n → Z.of_nat (length vl2) = n →
+  {{{ l1 ↦∗ vl1 ∗ l2 ↦∗{q} vl2 }}}
+    #l1 <-{n} !#l2 @ E
+  {{{ RET #☠; l1 ↦∗ vl2 ∗ l2 ↦∗{q} vl2 }}}.
 Proof.
-  iIntros (? Hvl1 Hvl2 Φ) "(#Hinv & Hl1 & Hl2) HΦ".
-  iLöb as "IH" forall (n l1 l2 vl1 vl2 Hvl1 Hvl2). wp_rec. wp_op=> ?; wp_if.
+  iIntros (Hvl1 Hvl2 Φ) "(Hl1 & Hl2) HΦ".
+  iLöb as "IH" forall (n l1 l2 vl1 vl2 Hvl1 Hvl2). wp_rec. wp_op; case_bool_decide; wp_if.
   - iApply "HΦ". assert (n = O) by lia; subst.
     destruct vl1, vl2; try discriminate. by iFrame.
-  - destruct vl1 as [|v1 vl1], vl2 as [|v2 vl2], n as [|n]; try discriminate.
-    revert Hvl1 Hvl2. intros [= Hvl1] [= Hvl2]; rewrite !heap_mapsto_vec_cons.
+  - destruct vl1 as [|v1 vl1], vl2 as [|v2 vl2], n as [|n|]; try (discriminate || lia).
+    revert Hvl1 Hvl2. intros [= Hvl1] [= Hvl2]; rewrite !heap_pointsto_vec_cons. subst n.
     iDestruct "Hl1" as "[Hv1 Hl1]". iDestruct "Hl2" as "[Hv2 Hl2]".
-    wp_read; wp_write. replace (Z.pos (Pos.of_succ_nat n)) with (n+1) by lia.
-    do 3 wp_op. rewrite Z.add_simpl_r.
-    iApply ("IH" with "[%] [%] Hl1 Hl2"); try done.
+    Local Opaque Zminus.
+    wp_read; wp_write. do 3 wp_op. iApply ("IH" with "[%] [%] Hl1 Hl2"); [lia..|].
     iIntros "!> [Hl1 Hl2]"; iApply "HΦ"; by iFrame.
 Qed.

theories/lang/new_delete.v → lambda-rust/lang/lib/new_delete.v

-From iris.base_logic.lib Require Import namespaces.
 From lrust.lang Require Export notation.
 From lrust.lang Require Import heap proofmode memcpy.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
 
 Definition new : val :=
   λ: ["n"],
     if: "n" ≤ #0 then #((42%positive, 1337):loc)
     else Alloc "n".
-Global Opaque new.
 
 Definition delete : val :=
   λ: ["n"; "loc"],
-    if: "n" ≤ #0 then #()
+    if: "n" ≤ #0 then #☠
     else Free "n" "loc".
-Global Opaque delete.
 
 Section specs.
-  Context `{heapG Σ}.
+  Context `{!lrustGS Σ}.
 
   Lemma wp_new E n:
-    ↑heapN ⊆ E → 0 ≤ n →
-    {{{ heap_ctx }}} new [ #n ] @ E
-    {{{ l vl, RET LitV $ LitLoc l;
-        ⌜n = length vl⌝ ∗ (†l…(Z.to_nat n) ∨ ⌜n = 0⌝) ∗ l ↦∗ vl }}}.
+    0 ≤ n →
+    {{{ True }}} new [ #n ] @ E
+    {{{ l, RET LitV $ LitLoc l;
+        (†l…(Z.to_nat n) ∨ ⌜n = 0⌝) ∗ l ↦∗ repeat (LitV LitPoison) (Z.to_nat n) }}}.
   Proof.
-    iIntros (? ? Φ) "#Hinv HΦ". wp_lam. wp_op; intros ?.
-    - wp_if. assert (n = 0) as -> by lia. iApply ("HΦ" $! _ []).
-      rewrite heap_mapsto_vec_nil. auto.
-    - wp_if. wp_alloc l vl as "H↦" "H†". iApply  "HΦ". iFrame. auto.
+    iIntros (? Φ) "_ HΦ". wp_lam. wp_op; case_bool_decide.
+    - wp_if. assert (n = 0) as -> by lia. iApply "HΦ".
+      rewrite heap_pointsto_vec_nil. auto.
+    - wp_if. wp_alloc l as "H↦" "H†"; first lia. iApply "HΦ". subst. iFrame.
   Qed.
 
   Lemma wp_delete E (n:Z) l vl :
-    ↑heapN ⊆ E → n = length vl →
-    {{{ heap_ctx ∗ l ↦∗ vl ∗ (†l…(length vl) ∨ ⌜n = 0⌝) }}}
+    n = length vl →
+    {{{ l ↦∗ vl ∗ (†l…(length vl) ∨ ⌜n = 0⌝) }}}
       delete [ #n; #l] @ E
-    {{{ RET LitV LitUnit; True }}}.
+    {{{ RET #☠; True }}}.
   Proof.
-    iIntros (? ? Φ) "(#Hinv & H↦ & [H†|%]) HΦ";
-      wp_lam; wp_op; intros ?; try lia; wp_if; try wp_free; by iApply "HΦ".
+    iIntros (? Φ) "(H↦ & [H†|%]) HΦ";
+      wp_lam; wp_op; case_bool_decide; try lia;
+      wp_if; try wp_free; by iApply "HΦ".
   Qed.
 End specs.
 
 (* FIXME : why are these notations not pretty-printed? *)
 Notation "'letalloc:' x <- e1 'in' e2" :=
   ((Lam (@cons binder x%E%E%E nil) (x <- e1 ;; e2)) [new [ #1]])%E
-  (at level 102, x at level 1, e1, e2 at level 200) : expr_scope.
-Notation "'letalloc:' x <⋯ !{ n } e1 'in' e2" :=
-  ((Lam (@cons binder x%E%E%E nil) (x <⋯ !{n%Z%V}e1 ;; e2)) [new [ #n]])%E
-  (at level 102, x at level 1, e1, e2 at level 200) : expr_scope.
+  (at level 102, x at level 1, e1, e2 at level 150) : expr_scope.
+Notation "'letalloc:' x <-{ n } ! e1 'in' e2" :=
+  ((Lam (@cons binder x%E%E%E nil) (x <-{n%Z%V%L} !e1 ;; e2)) [new [ #n]])%E
+  (at level 102, x at level 1, e1, e2 at level 150) : expr_scope.

lambda-rust/lang/lib/spawn.v

+From iris.program_logic Require Import weakestpre.
+From iris.base_logic.lib Require Import invariants.
+From iris.proofmode Require Import proofmode.
+From iris.algebra Require Import excl.
+From lrust.lang Require Import proofmode notation.
+From lrust.lang Require Export lang.
+From iris.prelude Require Import options.
+
+Definition spawn : val :=
+  λ: ["f"],
+    let: "c" := Alloc #2 in
+    "c" <- #0;; (* Initialize "sent" field to 0 (non-atomically). *)
+    Fork ("f" ["c"]);;
+    "c".
+Definition finish : val :=
+  λ: ["c"; "v"],
+    "c" +ₗ #1 <- "v";; (* Store data (non-atomically). *)
+    "c" <-ˢᶜ #1;; (* Signal that we finished (atomically!) *)
+    #☠.
+Definition join : val :=
+  rec: "join" ["c"] :=
+    if: !ˢᶜ"c" then
+      (* The thread finished, we can non-atomically load the data. *)
+      let: "v" := !("c" +ₗ #1) in
+      Free #2 "c";;
+      "v"
+    else
+      "join" ["c"].
+
+(** The CMRA & functor we need. *)
+Class spawnG Σ := SpawnG { spawn_tokG :: inG Σ (exclR unitO) }.
+Definition spawnΣ : gFunctors := #[GFunctor (exclR unitO)].
+
+Global Instance subG_spawnΣ {Σ} : subG spawnΣ Σ → spawnG Σ.
+Proof. solve_inG. Qed.
+
+(** Now we come to the Iris part of the proof. *)
+Section proof.
+Context `{!lrustGS Σ, !spawnG Σ} (N : namespace).
+
+Definition spawn_inv (γf γj : gname) (c : loc) (Ψ : val → iProp Σ) : iProp Σ :=
+  (own γf (Excl ()) ∗ own γj (Excl ()) ∨
+   ∃ b, c ↦ #(lit_of_bool b) ∗
+        if b then ∃ v, (c +ₗ 1) ↦ v ∗ Ψ v ∗ own γf (Excl ()) else True)%I.
+
+Definition finish_handle (c : loc) (Ψ : val → iProp Σ) : iProp Σ :=
+  (∃ γf γj v, own γf (Excl ()) ∗ (c +ₗ 1) ↦ v ∗ inv N (spawn_inv γf γj c Ψ))%I.
+
+Definition join_handle (c : loc) (Ψ : val → iProp Σ) : iProp Σ :=
+  (∃ γf γj Ψ', own γj (Excl ()) ∗ † c … 2 ∗ inv N (spawn_inv γf γj c Ψ') ∗
+   □ (∀ v, Ψ' v -∗ Ψ v))%I.
+
+Global Instance spawn_inv_ne n γf γj c :
+  Proper (pointwise_relation val (dist n) ==> dist n) (spawn_inv γf γj c).
+Proof. solve_proper. Qed.
+Global Instance finish_handle_ne n c :
+  Proper (pointwise_relation val (dist n) ==> dist n) (finish_handle c).
+Proof. solve_proper. Qed.
+Global Instance join_handle_ne n c :
+  Proper (pointwise_relation val (dist n) ==> dist n) (join_handle c).
+Proof. solve_proper. Qed.
+
+(** The main proofs. *)
+Lemma spawn_spec (Ψ : val → iProp Σ) e (f : val) :
+  IntoVal e f →
+  {{{ ∀ c, finish_handle c Ψ -∗ WP f [ #c] {{ _, True }} }}}
+    spawn [e] {{{ c, RET #c; join_handle c Ψ }}}.
+Proof.
+  iIntros (<- Φ) "Hf HΦ". rewrite /spawn /=.
+  wp_let. wp_alloc l as "Hl" "H†". wp_let.
+  iMod (own_alloc (Excl ())) as (γf) "Hγf"; first done.
+  iMod (own_alloc (Excl ())) as (γj) "Hγj"; first done.
+  rewrite heap_pointsto_vec_cons heap_pointsto_vec_singleton.
+  iDestruct "Hl" as "[Hc Hd]". wp_write.
+  iMod (inv_alloc N _ (spawn_inv γf γj l Ψ) with "[Hc]") as "#?".
+  { iNext. iRight. iExists false. auto. }
+  wp_apply (wp_fork with "[Hγf Hf Hd]").
+  - iApply "Hf". iExists _, _, _. iFrame. auto.
+  - iIntros "_". wp_seq. iApply "HΦ". iExists _, _.
+    iFrame. auto.
+Qed.
+
+Lemma finish_spec (Ψ : val → iProp Σ) c v :
+  {{{ finish_handle c Ψ ∗ Ψ v }}} finish [ #c; v] {{{ RET #☠; True }}}.
+Proof.
+  iIntros (Φ) "[Hfin HΨ] HΦ". iDestruct "Hfin" as (γf γj v0) "(Hf & Hd & #?)".
+  wp_lam. wp_op. wp_write.
+  wp_bind (_ <-ˢᶜ _)%E. iInv N as "[[>Hf' _]|Hinv]" "Hclose".
+  { iExFalso. iCombine "Hf" "Hf'" as "Hf". iDestruct (own_valid with "Hf") as "%".
+    auto. }
+  iDestruct "Hinv" as (b) "[>Hc _]". wp_write.
+  iMod ("Hclose" with "[-HΦ]").
+  - iNext. iRight. iExists true. iFrame.
+  - iModIntro. wp_seq. by iApply "HΦ".
+Qed.
+
+Lemma join_spec (Ψ : val → iProp Σ) c :
+  {{{ join_handle c Ψ }}} join [ #c] {{{ v, RET v; Ψ v }}}.
+Proof.
+  iIntros (Φ) "H HΦ". iDestruct "H" as (γf γj Ψ') "(Hj & H† & #? & #HΨ')".
+  iLöb as "IH". wp_rec.
+  wp_bind (!ˢᶜ _)%E. iInv N as "[[_ >Hj']|Hinv]" "Hclose".
+  { iExFalso. iCombine "Hj" "Hj'" as "Hj". iDestruct (own_valid with "Hj") as "%".
+    auto. }
+  iDestruct "Hinv" as (b) "[>Hc Ho]". wp_read. destruct b; last first.
+  { iMod ("Hclose" with "[Hc]").
+    - iNext. iRight. iExists _. iFrame.
+    - iModIntro. wp_if. iApply ("IH" with "Hj H†"). auto. }
+  iDestruct "Ho" as (v) "(Hd & HΨ & Hf)".
+  iMod ("Hclose" with "[Hj Hf]") as "_".
+  { iNext. iLeft. iFrame. }
+  iModIntro. wp_if. wp_op. wp_read. wp_let.
+  iAssert (c ↦∗ [ #true; v])%I with "[Hc Hd]" as "Hc".
+  { rewrite heap_pointsto_vec_cons heap_pointsto_vec_singleton. iFrame. }
+  wp_free; first done. iApply "HΦ". iApply "HΨ'". done.
+Qed.
+
+Lemma join_handle_impl (Ψ1 Ψ2 : val → iProp Σ) c :
+  □ (∀ v, Ψ1 v -∗ Ψ2 v) -∗ join_handle c Ψ1 -∗ join_handle c Ψ2.
+Proof.
+  iIntros "#HΨ Hhdl". iDestruct "Hhdl" as (γf γj Ψ') "(Hj & H† & #? & #HΨ')".
+  iExists γf, γj, Ψ'. iFrame "#∗". iIntros "!> * ?".
+  iApply "HΨ". iApply "HΨ'". done.
+Qed.
+
+End proof.
+
+Global Typeclasses Opaque finish_handle join_handle.

lambda-rust/lang/lib/swap.v

+From lrust.lang Require Export notation.
+From lrust.lang Require Import heap proofmode.
+From iris.prelude Require Import options.
+
+Definition swap : val :=
+  rec: "swap" ["p1";"p2";"len"] :=
+    if: "len" ≤ #0 then #☠
+    else let: "x" := !"p1" in
+         "p1" <- !"p2";;
+         "p2" <- "x";;
+         "swap" ["p1" +ₗ #1 ; "p2" +ₗ #1 ; "len" - #1].
+
+Lemma wp_swap `{!lrustGS Σ} E l1 l2 vl1 vl2 (n : Z):
+  Z.of_nat (length vl1) = n → Z.of_nat (length vl2) = n →
+  {{{ l1 ↦∗ vl1 ∗ l2 ↦∗ vl2 }}}
+    swap [ #l1; #l2; #n] @ E
+  {{{ RET #☠; l1 ↦∗ vl2 ∗ l2 ↦∗ vl1 }}}.
+Proof.
+  iIntros (Hvl1 Hvl2 Φ) "(Hl1 & Hl2) HΦ".
+  iLöb as "IH" forall (n l1 l2 vl1 vl2 Hvl1 Hvl2). wp_rec.
+  wp_op; case_bool_decide; wp_if.
+  - iApply "HΦ". assert (n = O) by lia; subst.
+    destruct vl1, vl2; try discriminate. by iFrame.
+  - destruct vl1 as [|v1 vl1], vl2 as [|v2 vl2], n as [|n|]; try (discriminate || lia).
+    revert Hvl1 Hvl2. intros [= Hvl1] [= Hvl2]; rewrite !heap_pointsto_vec_cons. subst n.
+    iDestruct "Hl1" as "[Hv1 Hl1]". iDestruct "Hl2" as "[Hv2 Hl2]".
+    Local Opaque Zminus.
+    wp_read; wp_let; wp_read; do 2 wp_write. do 3 wp_op.
+    iApply ("IH" with "[%] [%] Hl1 Hl2"); [lia..|].
+    iIntros "!> [Hl1 Hl2]"; iApply "HΦ"; by iFrame.
+Qed.

lambda-rust/lang/lib/tests.v

+From iris.program_logic Require Import weakestpre.
+From iris.proofmode Require Import proofmode.
+From lrust.lang Require Import lang proofmode notation.
+From iris.prelude Require Import options.
+
+Section tests.
+  Context `{!lrustGS Σ}.
+
+  Lemma test_location_cmp E (l1 l2 : loc) q1 q2 v1 v2 :
+    {{{ ▷ l1 ↦{q1} v1 ∗ ▷ l2 ↦{q2} v2 }}}
+      #l1 = #l2 @ E
+    {{{ (b: bool), RET LitV (lit_of_bool b); (if b then ⌜l1 = l2⌝ else ⌜l1 ≠ l2⌝) ∗
+                                     l1 ↦{q1} v1 ∗ l2 ↦{q2} v2 }}}.
+  Proof.
+    iIntros (Φ) "[Hl1 Hl2] HΦ". wp_op.
+    case_bool_decide; iApply "HΦ"; by iFrame.
+  Qed.
+End tests.

lambda-rust/lang/lifting.v

+From iris.proofmode Require Import proofmode.
+From iris.program_logic Require Export weakestpre.
+From iris.program_logic Require Import ectx_lifting.
+From lrust.lang Require Export lang heap.
+From lrust.lang Require Import tactics.
+From iris.prelude Require Import options.
+Import uPred.
+
+Class lrustGS Σ := LRustGS {
+  lrustGS_invGS : invGS Σ;
+  lrustGS_heapGS :: heapGS Σ
+}.
+
+Global Instance lrustGS_irisGS `{!lrustGS Σ} : irisGS lrust_lang Σ := {
+  iris_invGS := lrustGS_invGS;
+  state_interp σ _ κs _ := heap_ctx σ;
+  fork_post _ := True%I;
+  num_laters_per_step _ := 0%nat;
+  state_interp_mono _ _ _ _ := fupd_intro _ _
+}.
+
+Ltac inv_lit :=
+  repeat match goal with
+  | H : lit_eq _ ?x ?y |- _ => inversion H; clear H; simplify_map_eq/=
+  | H : lit_neq ?x ?y |- _ => inversion H; clear H; simplify_map_eq/=
+  end.
+
+Ltac inv_bin_op_eval :=
+  repeat match goal with
+  | H : bin_op_eval _ ?c _ _ _ |- _ => is_constructor c; inversion H; clear H; simplify_eq/=
+  end.
+
+Local Hint Extern 0 (atomic _) => solve_atomic : core.
+Local Hint Extern 0 (base_reducible _ _) => eexists _, _, _, _; simpl : core.
+
+Local Hint Constructors base_step bin_op_eval lit_neq lit_eq : core.
+Local Hint Resolve alloc_fresh : core.
+Local Hint Resolve to_of_val : core.
+
+Class AsRec (e : expr) (f : binder) (xl : list binder) (erec : expr) :=
+  as_rec : e = Rec f xl erec.
+Global Instance AsRec_rec f xl e : AsRec (Rec f xl e) f xl e := eq_refl.
+Global Instance AsRec_rec_locked_val v f xl e :
+  AsRec (of_val v) f xl e → AsRec (of_val (locked v)) f xl e.
+Proof. by unlock. Qed.
+
+Class DoSubst (x : binder) (es : expr) (e er : expr) :=
+  do_subst : subst' x es e = er.
+Global Hint Extern 0 (DoSubst _ _ _ _) =>
+  rewrite /DoSubst; simpl_subst; reflexivity : typeclass_instances.
+
+Class DoSubstL (xl : list binder) (esl : list expr) (e er : expr) :=
+  do_subst_l : subst_l xl esl e = Some er.
+Global Instance do_subst_l_nil e : DoSubstL [] [] e e.
+Proof. done. Qed.
+Global Instance do_subst_l_cons x xl es esl e er er' :
+  DoSubstL xl esl e er' → DoSubst x es er' er →
+  DoSubstL (x :: xl) (es :: esl) e er.
+Proof. rewrite /DoSubstL /DoSubst /= => -> <- //. Qed.
+Global Instance do_subst_vec xl (vsl : vec val (length xl)) e :
+  DoSubstL xl (of_val <$> vec_to_list vsl) e (subst_v xl vsl e).
+Proof. by rewrite /DoSubstL subst_v_eq. Qed.
+
+Section lifting.
+Context `{!lrustGS Σ}.
+Implicit Types P Q : iProp Σ.
+Implicit Types e : expr.
+Implicit Types ef : option expr.
+
+(** Base axioms for core primitives of the language: Stateless reductions *)
+Lemma wp_fork E e :
+  {{{ ▷ WP e {{ _, True }} }}} Fork e @ E {{{ RET LitV LitPoison; True }}}.
+Proof.
+  iIntros (?) "?HΦ". iApply wp_lift_atomic_base_step; [done|].
+  iIntros (σ1 κ ? κs n) "Hσ !>"; iSplit; first by eauto.
+  iNext; iIntros (v2 σ2 efs Hstep) "_"; inv_base_step. iFrame.
+  iModIntro. by iApply "HΦ".
+Qed.
+
+(** Pure reductions *)
+Local Ltac solve_exec_safe :=
+  intros; destruct_and?; subst; do 3 eexists; econstructor; simpl; eauto with lia.
+Local Ltac solve_exec_puredet :=
+  simpl; intros; destruct_and?; inv_base_step; inv_bin_op_eval; inv_lit; done.
+Local Ltac solve_pure_exec :=
+  intros ?; apply nsteps_once, pure_base_step_pure_step;
+    constructor; [solve_exec_safe | solve_exec_puredet].
+
+Global Instance pure_rec e f xl erec erec' el :
+  AsRec e f xl erec →
+  TCForall AsVal el →
+  Closed (f :b: xl +b+ []) erec →
+  DoSubstL (f :: xl) (e :: el) erec erec' →
+  PureExec True 1 (App e el) erec'.
+Proof.
+  rewrite /AsRec /DoSubstL=> -> /TCForall_Forall Hel ??. solve_pure_exec.
+  eapply Forall_impl; [exact Hel|]. intros e' [v <-]. rewrite to_of_val; eauto.
+Qed.
+
+Global Instance pure_le n1 n2 :
+  PureExec True 1 (BinOp LeOp (Lit (LitInt n1)) (Lit (LitInt n2)))
+                  (Lit (bool_decide (n1 ≤ n2))).
+Proof. solve_pure_exec. Qed.
+
+Global Instance pure_eq_int n1 n2 :
+  PureExec True 1 (BinOp EqOp (Lit (LitInt n1)) (Lit (LitInt n2))) (Lit (bool_decide (n1 = n2))).
+Proof. case_bool_decide; solve_pure_exec. Qed.
+
+Global Instance pure_eq_loc_0_r l :
+  PureExec True 1 (BinOp EqOp (Lit (LitLoc l)) (Lit (LitInt 0))) (Lit false).
+Proof. solve_pure_exec. Qed.
+
+Global Instance pure_eq_loc_0_l l :
+  PureExec True 1 (BinOp EqOp (Lit (LitInt 0)) (Lit (LitLoc l))) (Lit false).
+Proof. solve_pure_exec. Qed.
+
+Global Instance pure_plus z1 z2 :
+  PureExec True 1 (BinOp PlusOp (Lit $ LitInt z1) (Lit $ LitInt z2)) (Lit $ LitInt $ z1 + z2).
+Proof. solve_pure_exec. Qed.
+
+Global Instance pure_minus z1 z2 :
+  PureExec True 1 (BinOp MinusOp (Lit $ LitInt z1) (Lit $ LitInt z2)) (Lit $ LitInt $ z1 - z2).
+Proof. solve_pure_exec. Qed.
+
+Global Instance pure_offset l z  :
+  PureExec True 1 (BinOp OffsetOp (Lit $ LitLoc l) (Lit $ LitInt z)) (Lit $ LitLoc $ l +ₗ z).
+Proof. solve_pure_exec. Qed.
+
+Global Instance pure_case i e el :
+  PureExec (0 ≤ i ∧ el !! (Z.to_nat i) = Some e) 1 (Case (Lit $ LitInt i) el) e | 10.
+Proof. solve_pure_exec. Qed.
+
+Global Instance pure_if b e1 e2 :
+  PureExec True 1 (If (Lit (lit_of_bool b)) e1 e2) (if b then e1 else e2) | 1.
+Proof. destruct b; solve_pure_exec. Qed.
+
+(** Heap *)
+Lemma wp_alloc E (n : Z) :
+  0 < n →
+  {{{ True }}} Alloc (Lit $ LitInt n) @ E
+  {{{ l (sz: nat), RET LitV $ LitLoc l; ⌜n = sz⌝ ∗ †l…sz ∗ l ↦∗ repeat (LitV LitPoison) sz }}}.
+Proof.
+  iIntros (? Φ) "_ HΦ". iApply wp_lift_atomic_base_step_no_fork; auto.
+  iIntros (σ1 ? κ κs n') "Hσ !>"; iSplit; first by auto.
+  iNext; iIntros (v2 σ2 efs Hstep) "_"; inv_base_step.
+  iMod (heap_alloc with "Hσ") as "[Hσ Hl]"; [done..|].
+  iModIntro; iSplit=> //. iFrame.
+  iApply ("HΦ" $! _ (Z.to_nat n)). iFrame. iPureIntro. rewrite Z2Nat.id; lia.
+Qed.
+
+Lemma wp_free E (n:Z) l vl :
+  n = length vl →
+  {{{ ▷ l ↦∗ vl ∗ ▷ †l…(length vl) }}}
+    Free (Lit $ LitInt n) (Lit $ LitLoc l) @ E
+  {{{ RET LitV LitPoison; True }}}.
+Proof.
+  iIntros (? Φ) "[>Hmt >Hf] HΦ". iApply wp_lift_atomic_base_step_no_fork; auto.
+  iIntros (σ1 ? κ κs n') "Hσ".
+  iMod (heap_free _ _ _ n with "Hσ Hmt Hf") as "(% & % & Hσ)"=>//.
+  iModIntro; iSplit; first by auto.
+  iNext; iIntros (v2 σ2 efs Hstep) "_"; inv_base_step.
+  iModIntro; iSplit=> //. iFrame. iApply "HΦ"; auto.
+Qed.
+
+Lemma wp_read_sc E l q v :
+  {{{ ▷ l ↦{q} v }}} Read ScOrd (Lit $ LitLoc l) @ E
+  {{{ RET v; l ↦{q} v }}}.
+Proof.
+  iIntros (?) ">Hv HΦ". iApply wp_lift_atomic_base_step_no_fork; auto.
+  iIntros (σ1 ? κ κs n) "Hσ". iDestruct (heap_read with "Hσ Hv") as %[m ?].
+  iModIntro; iSplit; first by eauto.
+  iNext; iIntros (v2 σ2 efs Hstep) "_"; inv_base_step.
+  iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
+Qed.
+
+Lemma wp_read_na E l q v :
+  {{{ ▷ l ↦{q} v }}} Read Na1Ord (Lit $ LitLoc l) @ E
+  {{{ RET v; l ↦{q} v }}}.
+Proof.
+  iIntros (Φ) ">Hv HΦ". iApply wp_lift_base_step; auto. iIntros (σ1 ? κ κs n) "Hσ".
+  iMod (heap_read_na with "Hσ Hv") as (m) "(% & Hσ & Hσclose)".
+  iMod (fupd_mask_subseteq ∅) as "Hclose"; first set_solver.
+  iModIntro; iSplit; first by eauto.
+  iNext; iIntros (e2 σ2 efs Hstep) "_"; inv_base_step. iMod "Hclose" as "_".
+  iModIntro. iFrame "Hσ". iSplit; last done.
+  clear dependent σ1 n.
+  iApply wp_lift_atomic_base_step_no_fork; auto.
+  iIntros (σ1 ? κ' κs' n') "Hσ". iMod ("Hσclose" with "Hσ") as (n) "(% & Hσ & Hv)".
+  iModIntro; iSplit; first by eauto.
+  iNext; iIntros (e2 σ2 efs Hstep) "_ !>"; inv_base_step.
+  iFrame "Hσ". iSplit; [done|]. by iApply "HΦ".
+Qed.
+
+Lemma wp_write_sc E l e v v' :
+  IntoVal e v →
+  {{{ ▷ l ↦ v' }}} Write ScOrd (Lit $ LitLoc l) e @ E
+  {{{ RET LitV LitPoison; l ↦ v }}}.
+Proof.
+  iIntros (<- Φ) ">Hv HΦ". iApply wp_lift_atomic_base_step_no_fork; auto.
+  iIntros (σ1 ? κ κs n) "Hσ". iDestruct (heap_read_1 with "Hσ Hv") as %?.
+  iMod (heap_write _ _ _  v with "Hσ Hv") as "[Hσ Hv]".
+  iModIntro; iSplit; first by eauto.
+  iNext; iIntros (v2 σ2 efs Hstep) "_"; inv_base_step.
+  iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
+Qed.
+
+Lemma wp_write_na E l e v v' :
+  IntoVal e v →
+  {{{ ▷ l ↦ v' }}} Write Na1Ord (Lit $ LitLoc l) e @ E
+  {{{ RET LitV LitPoison; l ↦ v }}}.
+Proof.
+  iIntros (<- Φ) ">Hv HΦ".
+  iApply wp_lift_base_step; auto. iIntros (σ1 ? κ κs n) "Hσ".
+  iMod (heap_write_na with "Hσ Hv") as "(% & Hσ & Hσclose)".
+  iMod (fupd_mask_subseteq ∅) as "Hclose"; first set_solver.
+  iModIntro; iSplit; first by eauto.
+  iNext; iIntros (e2 σ2 efs Hstep) "_"; inv_base_step. iMod "Hclose" as "_".
+  iModIntro. iFrame "Hσ". iSplit; last done.
+  clear dependent σ1. iApply wp_lift_atomic_base_step_no_fork; auto.
+  iIntros (σ1 ? κ' κs' n') "Hσ". iMod ("Hσclose" with "Hσ") as "(% & Hσ & Hv)".
+  iModIntro; iSplit; first by eauto.
+  iNext; iIntros (e2 σ2 efs Hstep) "_ !>"; inv_base_step.
+  iFrame "Hσ". iSplit; [done|]. by iApply "HΦ".
+Qed.
+
+Lemma wp_cas_int_fail E l q z1 e2 lit2 zl :
+  IntoVal e2 (LitV lit2) → z1 ≠ zl →
+  {{{ ▷ l ↦{q} LitV (LitInt zl) }}}
+    CAS (Lit $ LitLoc l) (Lit $ LitInt z1) e2 @ E
+  {{{ RET LitV $ LitInt 0; l ↦{q} LitV (LitInt zl) }}}.
+Proof.
+  iIntros (<- ? Φ) ">Hv HΦ".
+  iApply wp_lift_atomic_base_step_no_fork; auto.
+  iIntros (σ1 ? κ κs n) "Hσ". iDestruct (heap_read with "Hσ Hv") as %[m ?].
+  iModIntro; iSplit; first by eauto.
+  iNext; iIntros (v2 σ2 efs Hstep) "_"; inv_base_step; inv_lit.
+  iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
+Qed.
+
+Lemma wp_cas_suc E l lit1 e2 lit2 :
+  IntoVal e2 (LitV lit2) → lit1 ≠ LitPoison →
+  {{{ ▷ l ↦ LitV lit1 }}}
+    CAS (Lit $ LitLoc l) (Lit lit1) e2 @ E
+  {{{ RET LitV (LitInt 1); l ↦ LitV lit2 }}}.
+Proof.
+  iIntros (<- ? Φ) ">Hv HΦ".
+  iApply wp_lift_atomic_base_step_no_fork; auto.
+  iIntros (σ1 ? κ κs n) "Hσ". iDestruct (heap_read_1 with "Hσ Hv") as %?.
+  iModIntro; iSplit; first (destruct lit1; by eauto).
+  iNext; iIntros (v2 σ2 efs Hstep) "_"; inv_base_step; [inv_lit|].
+  iMod (heap_write with "Hσ Hv") as "[$ Hv]".
+  iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
+Qed.
+
+Lemma wp_cas_int_suc E l z1 e2 lit2 :
+  IntoVal e2 (LitV lit2) →
+  {{{ ▷ l ↦ LitV (LitInt z1) }}}
+    CAS (Lit $ LitLoc l) (Lit $ LitInt z1) e2 @ E
+  {{{ RET LitV (LitInt 1); l ↦ LitV lit2 }}}.
+Proof. intros ?. by apply wp_cas_suc. Qed.
+
+Lemma wp_cas_loc_suc E l l1 e2 lit2 :
+  IntoVal e2 (LitV lit2) →
+  {{{ ▷ l ↦ LitV (LitLoc l1) }}}
+    CAS (Lit $ LitLoc l) (Lit $ LitLoc l1) e2 @ E
+  {{{ RET LitV (LitInt 1); l ↦ LitV lit2 }}}.
+Proof. intros ?. by apply wp_cas_suc. Qed.
+
+Lemma wp_cas_loc_fail E l q q' q1 l1 v1' e2 lit2 l' vl' :
+  IntoVal e2 (LitV lit2) → l1 ≠ l' →
+  {{{ ▷ l ↦{q} LitV (LitLoc l') ∗ ▷ l' ↦{q'} vl' ∗ ▷ l1 ↦{q1} v1' }}}
+    CAS (Lit $ LitLoc l) (Lit $ LitLoc l1) e2 @ E
+  {{{ RET LitV (LitInt 0);
+      l ↦{q} LitV (LitLoc l') ∗ l' ↦{q'} vl' ∗ l1 ↦{q1} v1' }}}.
+Proof.
+  iIntros (<- ? Φ) "(>Hl & >Hl' & >Hl1) HΦ".
+  iApply wp_lift_atomic_base_step_no_fork; auto.
+  iIntros (σ1 ? κ κs n) "Hσ". iDestruct (heap_read with "Hσ Hl") as %[nl ?].
+  iDestruct (heap_read with "Hσ Hl'") as %[nl' ?].
+  iDestruct (heap_read with "Hσ Hl1") as %[nl1 ?].
+  iModIntro; iSplit; first by eauto.
+  iNext; iIntros (v2 σ2 efs Hstep) "_"; inv_base_step; inv_lit.
+  iModIntro; iSplit=> //. iFrame. iApply "HΦ"; iFrame.
+Qed.
+
+Lemma wp_cas_loc_nondet E l l1 e2 l2 ll :
+  IntoVal e2 (LitV $ LitLoc l2) →
+  {{{ ▷ l ↦ LitV (LitLoc ll) }}}
+    CAS (Lit $ LitLoc l) (Lit $ LitLoc l1) e2 @ E
+  {{{ b, RET LitV (lit_of_bool b);
+      if b is true then l ↦ LitV (LitLoc l2)
+      else ⌜l1 ≠ ll⌝ ∗ l ↦ LitV (LitLoc ll) }}}.
+Proof.
+  iIntros (<- Φ) ">Hv HΦ".
+  iApply wp_lift_atomic_base_step_no_fork; auto.
+  iIntros (σ1 ? κ κs n) "Hσ". iDestruct (heap_read_1 with "Hσ Hv") as %?.
+  iModIntro; iSplit; first (destruct (decide (ll = l1)) as [->|]; by eauto).
+  iNext; iIntros (v2 σ2 efs Hstep) "_"; inv_base_step; last lia.
+  - inv_lit. iModIntro; iSplit; [done|]; iFrame "Hσ".
+    iApply "HΦ"; simpl; auto.
+  - iMod (heap_write with "Hσ Hv") as "[$ Hv]".
+    iModIntro; iSplit; [done|]. iApply "HΦ"; iFrame.
+Qed.
+
+Lemma wp_eq_loc E (l1 : loc) (l2: loc) q1 q2 v1 v2 P Φ :
+  (P ⊢ ▷ l1 ↦{q1} v1) →
+  (P ⊢ ▷ l2 ↦{q2} v2) →
+  (P ⊢ ▷ Φ (LitV (bool_decide (l1 = l2)))) →
+  P ⊢ WP BinOp EqOp (Lit (LitLoc l1)) (Lit (LitLoc l2)) @ E {{ Φ }}.
+Proof.
+  iIntros (Hl1 Hl2 Hpost) "HP".
+  destruct (bool_decide_reflect (l1 = l2)) as [->|].
+  - iApply wp_lift_pure_det_base_step_no_fork';
+      [done|solve_exec_safe|solve_exec_puredet|].
+    iPoseProof (Hpost with "HP") as "?".
+    iIntros "!> _". by iApply wp_value.
+  - iApply wp_lift_atomic_base_step_no_fork; subst=>//.
+    iIntros (σ1 ? κ κs n') "Hσ1". iModIntro. inv_base_step.
+    iSplitR.
+    { iPureIntro. repeat eexists. econstructor. eapply BinOpEqFalse. by auto. }
+    (* We need to do a little gymnastics here to apply Hne now and strip away a
+       ▷ but also have the ↦s. *)
+    iAssert ((▷ ∃ q v, l1 ↦{q} v) ∧ (▷ ∃ q v, l2 ↦{q} v) ∧ ▷ Φ (LitV false))%I with "[HP]" as "HP".
+    { iSplit; last iSplit.
+      + iExists _, _. by iApply Hl1.
+      + iExists _, _. by iApply Hl2.
+      + by iApply Hpost. }
+    clear Hl1 Hl2. iNext. iIntros (e2 σ2 efs Hs) "_ !>".
+    inv_base_step. iSplitR=>//. inv_bin_op_eval; inv_lit.
+    + iExFalso. iDestruct "HP" as "[Hl1 _]".
+      iDestruct "Hl1" as (??) "Hl1".
+      iDestruct (heap_read σ2 with "Hσ1 Hl1") as %[??]; simplify_eq.
+    + iExFalso. iDestruct "HP" as "[_ [Hl2 _]]".
+      iDestruct "Hl2" as (??) "Hl2".
+      iDestruct (heap_read σ2 with "Hσ1 Hl2") as %[??]; simplify_eq.
+    + iDestruct "HP" as "[_ [_ $]]". done.
+Qed.
+
+(** Proof rules for working on the n-ary argument list. *)
+Lemma wp_app_ind E f (el : list expr) (Ql : vec (val → iProp Σ) (length el)) vs Φ :
+  AsVal f →
+  ([∗ list] eQ ∈ zip el Ql, WP eQ.1 @ E {{ eQ.2 }}) -∗
+    (∀ vl : vec val (length el), ([∗ list] vQ ∈ zip vl Ql, vQ.2 $ vQ.1) -∗
+                    WP App f (of_val <$> vs ++ vl) @ E {{ Φ }}) -∗
+    WP App f ((of_val <$> vs) ++ el) @ E {{ Φ }}.
+Proof.
+  intros [vf <-]. revert vs Ql.
+  induction el as [|e el IH]=>/= vs Ql; inv_vec Ql; simpl.
+  - iIntros "_ H". iSpecialize ("H" $! [#]). rewrite !app_nil_r /=. by iApply "H".
+  - iIntros (Q Ql) "[He Hl] HΦ".
+    change (App (of_val vf) ((of_val <$> vs) ++ e :: el)) with (fill_item (AppRCtx vf vs el) e).
+    iApply wp_bind. iApply (wp_wand with "He"). iIntros (v) "HQ /=".
+    rewrite cons_middle (assoc app) -(fmap_app _ _ [v]).
+    iApply (IH _ _ with "Hl"). iIntros "%vl Hvl". rewrite -assoc.
+    iApply ("HΦ" $! (v:::vl)). iFrame.
+Qed.
+
+Lemma wp_app_vec E f el (Ql : vec (val → iProp Σ) (length el)) Φ :
+  AsVal f →
+  ([∗ list] eQ ∈ zip el Ql, WP eQ.1 @ E {{ eQ.2 }}) -∗
+    (∀ vl : vec val (length el), ([∗ list] vQ ∈ zip vl Ql, vQ.2 $ vQ.1) -∗
+                    WP App f (of_val <$> (vl : list val)) @ E {{ Φ }}) -∗
+    WP App f el @ E {{ Φ }}.
+Proof. iIntros (Hf). by iApply (wp_app_ind _ _ _ _ []). Qed.
+
+Lemma wp_app (Ql : list (val → iProp Σ)) E f el Φ :
+  length Ql = length el → AsVal f →
+  ([∗ list] eQ ∈ zip el Ql, WP eQ.1 @ E {{ eQ.2 }}) -∗
+    (∀ vl : list val, ⌜length vl = length el⌝ -∗
+            ([∗ list] k ↦ vQ ∈ zip vl Ql, vQ.2 $ vQ.1) -∗
+             WP App f (of_val <$> (vl : list val)) @ E {{ Φ }}) -∗
+    WP App f el @ E {{ Φ }}.
+Proof.
+  iIntros (Hlen Hf) "Hel HΦ". rewrite -(vec_to_list_to_vec Ql).
+  generalize (list_to_vec Ql). rewrite Hlen. clear Hlen Ql=>Ql.
+  iApply (wp_app_vec with "Hel"). iIntros (vl) "Hvl".
+  iApply ("HΦ" with "[%] Hvl"). by rewrite length_vec_to_list.
+Qed.
+End lifting.

theories/lang/notation.v → lambda-rust/lang/notation.v

-From lrust.lang Require Export derived.
-Set Default Proof Using "Type".
+From lrust.lang Require Export lang.
+From iris.prelude Require Import options.
 
 Coercion LitInt : Z >-> base_lit.
 Coercion LitLoc : loc >-> base_lit.
@@ -9,9 +9,7 @@ Coercion of_val : val >-> expr.
 
 Coercion Var : string >-> expr.
 
-Coercion BNamed : string >-> binder.
-Notation "<>" := BAnon : lrust_binder_scope.
-
+Notation "[ ]" := (@nil expr) : expr_scope.
 Notation "[ x ]" := (@cons expr x%E (@nil expr)) : expr_scope.
 Notation "[ x1 ; x2 ; .. ; xn ]" :=
   (@cons expr x1%E (@cons expr x2%E
@@ -19,16 +17,16 @@ Notation "[ x1 ; x2 ; .. ; xn ]" :=
 
 (* No scope for the values, does not conflict and scope is often not inferred
 properly. *)
-Notation "# l" := (LitV l%Z%V) (at level 8, format "# l").
-Notation "# l" := (Lit l%Z%V) (at level 8, format "# l") : expr_scope.
+Notation "# l" := (LitV l%Z%V%L) (at level 8, format "# l").
+Notation "# l" := (Lit l%Z%V%L) (at level 8, format "# l") : expr_scope.
 
 (** Syntax inspired by Coq/Ocaml. Constructions with higher precedence come
     first. *)
 Notation "'case:' e0 'of' el" := (Case e0%E el%E)
   (at level 102, e0, el at level 150) : expr_scope.
 Notation "'if:' e1 'then' e2 'else' e3" := (If e1%E e2%E e3%E)
-  (only parsing, at level 200, e1, e2, e3 at level 150) : expr_scope.
-Notation "()" := LitUnit : val_scope.
+  (only parsing, at level 102, e1, e2, e3 at level 150) : expr_scope.
+Notation "☠" := LitPoison : val_scope.
 Notation "! e" := (Read Na1Ord e%E) (at level 9, format "! e") : expr_scope.
 Notation "!ˢᶜ e" := (Read ScOrd e%E) (at level 9, format "!ˢᶜ e") : expr_scope.
 Notation "e1 + e2" := (BinOp PlusOp e1%E e2%E)
@@ -37,14 +35,18 @@ Notation "e1 - e2" := (BinOp MinusOp e1%E e2%E)
   (at level 50, left associativity) : expr_scope.
 Notation "e1 ≤ e2" := (BinOp LeOp e1%E e2%E)
   (at level 70) : expr_scope.
+Notation "e1 < e2" := (e1+#1 ≤ e2)%E
+  (at level 70) : expr_scope.
+Notation "e1 = e2" := (BinOp EqOp e1%E e2%E)
+  (at level 70) : expr_scope.
 (* The unicode ← is already part of the notation "_ ← _; _" for bind. *)
 Notation "e1 <-ˢᶜ e2" := (Write ScOrd e1%E e2%E)
   (at level 80) : expr_scope.
 Notation "e1 <- e2" := (Write Na1Ord e1%E e2%E)
   (at level 80) : expr_scope.
-Notation "'rec:' f xl := e" := (Rec f%RustB xl%RustB e%E)
+Notation "'rec:' f xl := e" := (Rec f%binder xl%binder e%E)
   (at level 102, f, xl at level 1, e at level 200) : expr_scope.
-Notation "'rec:' f xl := e" := (RecV f%RustB xl%RustB e%E)
+Notation "'rec:' f xl := e" := (locked (RecV f%binder xl%binder e%E))
   (at level 102, f, xl at level 1, e at level 200) : val_scope.
 Notation "e1 +ₗ e2" := (BinOp OffsetOp e1%E e2%E)
   (at level 50, left associativity) : expr_scope.
@@ -54,38 +56,50 @@ explicitly instead of relying on the Notations Let and Seq as defined
 above. This is needed because App is now a coercion, and these
 notations are otherwise not pretty printed back accordingly. *)
 
-Notation "λ: xl , e" := (Lam xl%RustB e%E)
+Notation "λ: xl , e" := (Lam xl%binder e%E)
   (at level 102, xl at level 1, e at level 200) : expr_scope.
-Notation "λ: xl , e" := (LamV xl%RustB e%E)
+Notation "λ: xl , e" := (locked (LamV xl%binder e%E))
   (at level 102, xl at level 1, e at level 200) : val_scope.
-Notation "'funrec:' f xl := e" := (rec: f ("return"::xl) := e)%E
-  (only parsing, at level 102, f, xl at level 1, e at level 200) : expr_scope.
-Notation "'funrec:' f xl := e" := (rec: f ("return"::xl) := e)%V
-  (only parsing, at level 102, f, xl at level 1, e at level 200) : val_scope.
+
+Notation "'fnrec:' f xl := e" := (rec: f (BNamed "return"::xl) := e)%E
+  (at level 102, f, xl at level 1, e at level 200) : expr_scope.
+Notation "'fnrec:' f xl := e" := (rec: f (BNamed "return"::xl) := e)%V
+  (at level 102, f, xl at level 1, e at level 200) : val_scope.
+Notation "'fn:' xl := e" := (fnrec: <> xl := e)%E
+  (at level 102, xl at level 1, e at level 200) : expr_scope.
+Notation "'fn:' xl := e" := (fnrec: <> xl := e)%V
+  (at level 102, xl at level 1, e at level 200) : val_scope.
+Notation "'return:'" := "return" : expr_scope.
 
 Notation "'let:' x := e1 'in' e2" :=
-  ((Lam (@cons binder x%RustB nil) e2%E) (@cons expr e1%E nil))
+  ((Lam (@cons binder x%binder nil) e2%E) (@cons expr e1%E nil))
   (at level 102, x at level 1, e1, e2 at level 150) : expr_scope.
 Notation "e1 ;; e2" := (let: <> := e1 in e2)%E
-  (at level 100, e2 at level 150, format "e1  ;;  e2") : expr_scope.
+  (at level 100, e2 at level 200, format "e1  ;;  e2") : expr_scope.
 (* These are not actually values, but we want them to be pretty-printed. *)
 Notation "'let:' x := e1 'in' e2" :=
-  (LamV (@cons binder x%RustB nil) e2%E (@cons expr e1%E nil))
+  (LamV (@cons binder x%binder nil) e2%E (@cons expr e1%E nil))
   (at level 102, x at level 1, e1, e2 at level 150) : val_scope.
 Notation "e1 ;; e2" := (let: <> := e1 in e2)%V
-  (at level 100, e2 at level 150, format "e1  ;;  e2") : val_scope.
+  (at level 100, e2 at level 200, format "e1  ;;  e2") : val_scope.
 
-Notation "e1 'cont:' k xl := e2" :=
-  ((Lam (@cons binder k%RustB nil) e1%E) [Rec k%RustB xl%RustB e2%E])
-  (only parsing, at level 151, k, xl at level 1, e2 at level 150) : expr_scope.
+Notation "'letcont:' k xl := e1 'in' e2" :=
+  ((Lam (@cons binder k%binder nil) e2%E) [Rec k%binder xl%binder e1%E])
+  (at level 102, k, xl at level 1, e1, e2 at level 150) : expr_scope.
+Notation "'withcont:' k1 ':' e1 'cont:' k2 xl := e2" :=
+  ((Lam (@cons binder k1%binder nil) e1%E) [Rec k2%binder ((fun _ : eq k1%binder k2%binder => xl%binder) eq_refl) e2%E])
+  (only parsing, at level 151, k1, k2, xl at level 1, e2 at level 150) : expr_scope.
 
-Notation "'call:' f args → k" := (f (@cons expr k args))%E
+Notation "'call:' f args → k" := (f (@cons expr (λ: ["_r"], k ["_r"]) args))%E
   (only parsing, at level 102, f, args, k at level 1) : expr_scope.
 Notation "'letcall:' x := f args 'in' e" :=
-  (call: f args → "_k" cont: "_k" [ x ] := e)%E
+  (letcont: "_k" [ x ] := e in call: f args → "_k")%E
   (at level 102, x, f, args at level 1, e at level 150) : expr_scope.
 
-Notation "e1 <-{ i } '☇'" := (e1 <- #i)%E
+(* These notations unfortunately do not print.  Also, I don't think
+   we would even want them to print in general.
+   TODO: Introduce a Definition. *)
+Notation "e1 '<-{Σ' i } '()'" := (e1 <- #i)%E
   (only parsing, at level 80) : expr_scope.
-Notation "e1 <-{ i } e2" := (e1 <-{i} ☇ ;; e1+ₗ#1 <- e2)%E
-  (at level 80) : expr_scope.
+Notation "e1 '<-{Σ' i } e2" := (e1 <-{Σ i} () ;; e1+ₗ#1 <- e2)%E
+  (at level 80, format "e1 <-{Σ  i }  e2") : expr_scope.

lambda-rust/lang/proofmode.v

+From iris.proofmode Require Import coq_tactics reduction.
+From iris.proofmode Require Export proofmode.
+From iris.program_logic Require Export weakestpre.
+From iris.program_logic Require Import lifting.
+From lrust.lang Require Export tactics lifting.
+From iris.prelude Require Import options.
+Import uPred.
+
+Lemma tac_wp_value `{!lrustGS Σ} Δ E Φ e v :
+  IntoVal e v →
+  envs_entails Δ (Φ v) → envs_entails Δ (WP e @ E {{ Φ }}).
+Proof. rewrite envs_entails_unseal=> ? ->. by apply wp_value. Qed.
+
+Ltac wp_value_head := eapply tac_wp_value; [tc_solve|reduction.pm_prettify].
+
+Lemma tac_wp_pure `{!lrustGS Σ} K Δ Δ' E e1 e2 φ n Φ :
+  PureExec φ n e1 e2 →
+  φ →
+  MaybeIntoLaterNEnvs n Δ Δ' →
+  envs_entails Δ' (WP fill K e2 @ E {{ Φ }}) →
+  envs_entails Δ (WP fill K e1 @ E {{ Φ }}).
+Proof.
+  rewrite envs_entails_unseal=> ??? HΔ'. rewrite into_laterN_env_sound /=.
+  rewrite -wp_bind HΔ' -wp_pure_step_later //. rewrite -wp_bind_inv.
+  f_equiv. apply wand_intro_l. by rewrite sep_elim_r.
+Qed.
+
+Tactic Notation "wp_pure" open_constr(efoc) :=
+  iStartProof;
+  lazymatch goal with
+  | |- envs_entails _ (wp ?s ?E ?e ?Q) => reshape_expr e ltac:(fun K e' =>
+    unify e' efoc;
+    eapply (tac_wp_pure K);
+    [simpl; tc_solve                (* PureExec *)
+    |try done                       (* The pure condition for PureExec *)
+    |tc_solve                       (* IntoLaters *)
+    |simpl_subst; try wp_value_head (* new goal *)])
+   || fail "wp_pure: cannot find" efoc "in" e "or" efoc "is not a reduct"
+  | _ => fail "wp_pure: not a 'wp'"
+  end.
+
+Lemma tac_wp_eq_loc `{!lrustGS Σ} K Δ Δ' E i1 i2 l1 l2 q1 q2 v1 v2 Φ :
+  MaybeIntoLaterNEnvs 1 Δ Δ' →
+  envs_lookup i1 Δ' = Some (false, l1 ↦{q1} v1)%I →
+  envs_lookup i2 Δ' = Some (false, l2 ↦{q2} v2)%I →
+  envs_entails Δ' (WP fill K (Lit (bool_decide (l1 = l2))) @ E {{ Φ }}) →
+  envs_entails Δ (WP fill K (BinOp EqOp (Lit (LitLoc l1)) (Lit (LitLoc l2))) @ E {{ Φ }}).
+Proof.
+  rewrite envs_entails_unseal=> ? /envs_lookup_sound /=. rewrite sep_elim_l=> ?.
+  move /envs_lookup_sound; rewrite sep_elim_l=> ? HΔ. rewrite -wp_bind.
+  rewrite into_laterN_env_sound /=. eapply wp_eq_loc; eauto using later_mono.
+Qed.
+
+Tactic Notation "wp_eq_loc" :=
+  iStartProof;
+  lazymatch goal with
+  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
+     reshape_expr e ltac:(fun K e' => eapply (tac_wp_eq_loc K));
+       [tc_solve|iAssumptionCore|iAssumptionCore|simpl; try wp_value_head]
+  | _ => fail "wp_pure: not a 'wp'"
+  end.
+
+Tactic Notation "wp_rec" := wp_pure (App _ _).
+Tactic Notation "wp_lam" := wp_rec.
+Tactic Notation "wp_let" := wp_lam.
+Tactic Notation "wp_seq" := wp_let.
+Tactic Notation "wp_op" := wp_pure (BinOp _ _ _) || wp_eq_loc.
+Tactic Notation "wp_if" := wp_pure (If _ _ _).
+Tactic Notation "wp_case" := wp_pure (Case _ _); try wp_value_head.
+
+Lemma tac_wp_bind `{!lrustGS Σ} K Δ E Φ e :
+  envs_entails Δ (WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }})%I →
+  envs_entails Δ (WP fill K e @ E {{ Φ }}).
+Proof. rewrite envs_entails_unseal=> ->. apply: wp_bind. Qed.
+
+Ltac wp_bind_core K :=
+  lazymatch eval hnf in K with
+  | [] => idtac
+  | _ => apply (tac_wp_bind K); simpl
+  end.
+
+Tactic Notation "wp_bind" open_constr(efoc) :=
+  iStartProof;
+  lazymatch goal with
+  | |- envs_entails _ (wp ?s ?E ?e ?Q) => reshape_expr e ltac:(fun K e' =>
+    match e' with
+    | efoc => unify e' efoc; wp_bind_core K
+    end) || fail "wp_bind: cannot find" efoc "in" e
+  | _ => fail "wp_bind: not a 'wp'"
+  end.
+
+Section heap.
+Context `{!lrustGS Σ}.
+Implicit Types P Q : iProp Σ.
+Implicit Types Φ : val → iProp Σ.
+Implicit Types Δ : envs (uPredI (iResUR Σ)).
+
+Lemma tac_wp_alloc K Δ Δ' E j1 j2 n Φ :
+  0 < n →
+  MaybeIntoLaterNEnvs 1 Δ Δ' →
+  (∀ l (sz: nat), n = sz → ∃ Δ'',
+    envs_app false (Esnoc (Esnoc Enil j1 (l ↦∗ repeat (LitV LitPoison) sz)) j2 (†l…sz)) Δ'
+      = Some Δ'' ∧
+    envs_entails Δ'' (WP fill K (Lit $ LitLoc l) @ E {{ Φ }})) →
+  envs_entails Δ (WP fill K (Alloc (Lit $ LitInt n)) @ E {{ Φ }}).
+Proof.
+  rewrite envs_entails_unseal=> ?? HΔ. rewrite -wp_bind.
+  eapply wand_apply; first by apply wand_entails, wp_alloc.
+  rewrite -persistent_and_sep. apply and_intro; first by auto.
+  rewrite into_laterN_env_sound; apply later_mono, forall_intro=> l.
+  apply forall_intro=>sz. apply wand_intro_l. rewrite -assoc.
+  rewrite sep_and. apply pure_elim_l=> Hn. apply wand_elim_r'.
+  destruct (HΔ l sz) as (Δ''&?&HΔ'); first done.
+  rewrite envs_app_sound //; simpl. by rewrite right_id HΔ'.
+Qed.
+
+Lemma tac_wp_free K Δ Δ' Δ'' Δ''' E i1 i2 vl (n : Z) (n' : nat) l Φ :
+  n = length vl →
+  MaybeIntoLaterNEnvs 1 Δ Δ' →
+  envs_lookup i1 Δ' = Some (false, l ↦∗ vl)%I →
+  envs_delete false i1 false Δ' = Δ'' →
+  envs_lookup i2 Δ'' = Some (false, †l…n')%I →
+  envs_delete false i2 false Δ'' = Δ''' →
+  n' = length vl →
+  envs_entails Δ''' (WP fill K (Lit LitPoison) @ E {{ Φ }}) →
+  envs_entails Δ (WP fill K (Free (Lit $ LitInt n) (Lit $ LitLoc l)) @ E {{ Φ }}).
+Proof.
+  rewrite envs_entails_unseal; intros -> ?? <- ? <- -> HΔ. rewrite -wp_bind.
+  eapply wand_apply; first by apply wand_entails, wp_free; simpl.
+  rewrite into_laterN_env_sound -!later_sep; apply later_mono.
+  do 2 (rewrite envs_lookup_sound //). by rewrite HΔ True_emp emp_wand -assoc.
+Qed.
+
+Lemma tac_wp_read K Δ Δ' E i l q v o Φ :
+  o = Na1Ord ∨ o = ScOrd →
+  MaybeIntoLaterNEnvs 1 Δ Δ' →
+  envs_lookup i Δ' = Some (false, l ↦{q} v)%I →
+  envs_entails Δ' (WP fill K (of_val v) @ E {{ Φ }}) →
+  envs_entails Δ (WP fill K (Read o (Lit $ LitLoc l)) @ E {{ Φ }}).
+Proof.
+  rewrite envs_entails_unseal; intros [->| ->] ???.
+  - rewrite -wp_bind. eapply wand_apply; first by apply wand_entails, wp_read_na.
+    rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
+    by apply later_mono, sep_mono_r, wand_mono.
+  - rewrite -wp_bind. eapply wand_apply; first by apply wand_entails, wp_read_sc.
+    rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
+    by apply later_mono, sep_mono_r, wand_mono.
+Qed.
+
+Lemma tac_wp_write K Δ Δ' Δ'' E i l v e v' o Φ :
+  IntoVal e v' →
+  o = Na1Ord ∨ o = ScOrd →
+  MaybeIntoLaterNEnvs 1 Δ Δ' →
+  envs_lookup i Δ' = Some (false, l ↦ v)%I →
+  envs_simple_replace i false (Esnoc Enil i (l ↦ v')) Δ' = Some Δ'' →
+  envs_entails Δ'' (WP fill K (Lit LitPoison) @ E {{ Φ }}) →
+  envs_entails Δ (WP fill K (Write o (Lit $ LitLoc l) e) @ E {{ Φ }}).
+Proof.
+  rewrite envs_entails_unseal; intros ? [->| ->] ????.
+  - rewrite -wp_bind. eapply wand_apply; first by apply wand_entails, wp_write_na.
+    rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
+    rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
+  - rewrite -wp_bind. eapply wand_apply; first by apply wand_entails, wp_write_sc.
+    rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
+    rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
+Qed.
+End heap.
+
+Tactic Notation "wp_apply" open_constr(lem) :=
+  iPoseProofCore lem as false (fun H =>
+    lazymatch goal with
+    | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
+      reshape_expr e ltac:(fun K e' =>
+        wp_bind_core K; iApplyHyp H; try iNext; simpl) ||
+      lazymatch iTypeOf H with
+      | Some (_,?P) => fail "wp_apply: cannot apply" P
+      end
+    | _ => fail "wp_apply: not a 'wp'"
+    end).
+
+Tactic Notation "wp_alloc" ident(l) "as" constr(H) constr(Hf) :=
+  iStartProof;
+  lazymatch goal with
+  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
+    first
+      [reshape_expr e ltac:(fun K e' => eapply (tac_wp_alloc K _ _ _ H Hf))
+      |fail 1 "wp_alloc: cannot find 'Alloc' in" e];
+    [try fast_done
+    |tc_solve
+    |let sz := fresh "sz" in let Hsz := fresh "Hsz" in
+     first [intros l sz Hsz | fail 1 "wp_alloc:" l "not fresh"];
+     (* If Hsz is "constant Z = nat", change that to an equation on nat and
+        potentially substitute away the sz. *)
+     try (match goal with Hsz : ?x = _ |- _ => rewrite <-(Z2Nat.id x) in Hsz; last done end;
+          apply Nat2Z.inj in Hsz;
+          try (cbv [Z.to_nat Pos.to_nat] in Hsz;
+               simpl in Hsz;
+               (* Substitute only if we have a literal nat. *)
+               match goal with Hsz : S _ = _ |- _ => subst sz end));
+      eexists; split;
+        [pm_reflexivity || fail "wp_alloc:" H "or" Hf "not fresh"
+        |simpl; try wp_value_head]]
+  | _ => fail "wp_alloc: not a 'wp'"
+  end.
+
+Tactic Notation "wp_alloc" ident(l) :=
+  let H := iFresh in let Hf := iFresh in wp_alloc l as H Hf.
+
+Tactic Notation "wp_free" :=
+  iStartProof;
+  lazymatch goal with
+  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
+    first
+      [reshape_expr e ltac:(fun K e' => eapply (tac_wp_free K))
+      |fail 1 "wp_free: cannot find 'Free' in" e];
+    [try fast_done
+    |tc_solve
+    |let l := match goal with |- _ = Some (_, (?l ↦∗ _)%I) => l end in
+     iAssumptionCore || fail "wp_free: cannot find" l "↦∗ ?"
+    |pm_reflexivity
+    |let l := match goal with |- _ = Some (_, († ?l … _)%I) => l end in
+     iAssumptionCore || fail "wp_free: cannot find †" l "… ?"
+    |pm_reflexivity
+    |try fast_done
+    |simpl; try first [wp_pure (Seq (Lit LitPoison) _)|wp_value_head]]
+  | _ => fail "wp_free: not a 'wp'"
+  end.
+
+Tactic Notation "wp_read" :=
+  iStartProof;
+  lazymatch goal with
+  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
+    first
+      [reshape_expr e ltac:(fun K e' => eapply (tac_wp_read K))
+      |fail 1 "wp_read: cannot find 'Read' in" e];
+    [(right; fast_done) || (left; fast_done) ||
+     fail "wp_read: order is neither Na2Ord nor ScOrd"
+    |tc_solve
+    |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
+     iAssumptionCore || fail "wp_read: cannot find" l "↦ ?"
+    |simpl; try wp_value_head]
+  | _ => fail "wp_read: not a 'wp'"
+  end.
+
+Tactic Notation "wp_write" :=
+  iStartProof;
+  lazymatch goal with
+  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
+    first
+      [reshape_expr e ltac:(fun K e' => eapply (tac_wp_write K); [tc_solve|..])
+      |fail 1 "wp_write: cannot find 'Write' in" e];
+    [(right; fast_done) || (left; fast_done) ||
+     fail "wp_write: order is neither Na2Ord nor ScOrd"
+    |tc_solve
+    |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
+     iAssumptionCore || fail "wp_write: cannot find" l "↦ ?"
+    |pm_reflexivity
+    |simpl; try first [wp_pure (Seq (Lit LitPoison) _)|wp_value_head]]
+  | _ => fail "wp_write: not a 'wp'"
+  end.

theories/lang/races.v → lambda-rust/lang/races.v

-From iris.prelude Require Import gmap.
-From iris.program_logic Require Export hoare.
+From stdpp Require Import gmap.
 From iris.program_logic Require Import adequacy.
 From lrust.lang Require Import tactics.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
 
 Inductive access_kind : Type := ReadAcc | WriteAcc | FreeAcc.
 
-(* This is a crucial definition; if we forget to sync it with head_step,
+(* This is a crucial definition; if we forget to sync it with base_step,
    the results proven here are worthless. *)
 Inductive next_access_head : expr → state → access_kind * order → loc → Prop :=
 | Access_read ord l σ :
@@ -15,40 +14,40 @@ Inductive next_access_head : expr → state → access_kind * order → loc →
     is_Some (to_val e) →
     next_access_head (Write ord (Lit $ LitLoc l) e) σ (WriteAcc, ord) l
 | Access_cas_fail l st e1 lit1 e2 lit2 litl σ :
-    to_val e1 = Some $ LitV lit1 → to_val e2 = Some $ LitV lit2 →
-    lit_neq σ lit1 litl → σ !! l = Some (st, LitV litl) →
+    to_val e1 = Some (LitV lit1) → to_val e2 = Some (LitV lit2) →
+    lit_neq lit1 litl → σ !! l = Some (st, LitV litl) →
     next_access_head (CAS (Lit $ LitLoc l) e1 e2) σ (ReadAcc, ScOrd) l
 | Access_cas_suc l st e1 lit1 e2 lit2 litl σ :
-    to_val e1 = Some $ LitV lit1 → to_val e2 = Some $ LitV lit2 →
+    to_val e1 = Some (LitV lit1) → to_val e2 = Some (LitV lit2) →
     lit_eq σ lit1 litl → σ !! l = Some (st, LitV litl) →
     next_access_head (CAS (Lit $ LitLoc l) e1 e2) σ (WriteAcc, ScOrd) l
 | Access_free n l σ i :
     0 ≤ i < n →
     next_access_head (Free (Lit $ LitInt n) (Lit $ LitLoc l))
-                     σ (FreeAcc, Na2Ord) (shift_loc l i).
+                     σ (FreeAcc, Na2Ord) (l +ₗ i).
 
 (* Some sanity checks to make sure the definition above is not entirely insensible. *)
-Goal ∀ e1 e2 e3 σ, head_reducible (CAS e1 e2 e3) σ →
+Goal ∀ e1 e2 e3 σ, base_reducible (CAS e1 e2 e3) σ →
                    ∃ a l, next_access_head (CAS e1 e2 e3) σ a l.
 Proof.
-  intros ??? σ (?&?&?&?). inversion H; do 2 eexists;
+  intros ??? σ (?&?&?&?&H). inversion H; do 2 eexists;
     (eapply Access_cas_fail; done) || eapply Access_cas_suc; done.
 Qed.
-Goal ∀ o e σ, head_reducible (Read o e) σ →
+Goal ∀ o e σ, base_reducible (Read o e) σ →
               ∃ a l, next_access_head (Read o e) σ a l.
 Proof.
-  intros ?? σ (?&?&?&?). inversion H; do 2 eexists; eapply Access_read; done.
+  intros ?? σ (?&?&?&?&H). inversion H; do 2 eexists; eapply Access_read; done.
 Qed.
-Goal ∀ o e1 e2 σ, head_reducible (Write o e1 e2) σ →
+Goal ∀ o e1 e2 σ, base_reducible (Write o e1 e2) σ →
               ∃ a l, next_access_head (Write o e1 e2) σ a l.
 Proof.
-  intros ??? σ (?&?&?&?). inversion H; do 2 eexists;
+  intros ??? σ (?&?&?&?&H). inversion H; do 2 eexists;
     eapply Access_write; try done; eexists; done.
 Qed.
-Goal ∀ e1 e2 σ, head_reducible (Free e1 e2) σ →
+Goal ∀ e1 e2 σ, base_reducible (Free e1 e2) σ →
               ∃ a l, next_access_head (Free e1 e2) σ a l.
 Proof.
-  intros ?? σ (?&?&?&?). inversion H; do 2 eexists; eapply Access_free; done.
+  intros ?? σ (?&?&?&?&H). inversion H; do 2 eexists; eapply Access_free; done.
 Qed.
 
 Definition next_access_thread (e: expr) (σ : state)
@@ -67,229 +66,219 @@ Definition nonracing_accesses (a1 a2 : access_kind * order) : Prop :=
   | _, _ => False
   end.
 
-Definition nonracing_threadpool (el : list expr) σ : Prop :=
+Definition nonracing_threadpool (el : list expr) (σ : state) : Prop :=
   ∀ l a1 a2, next_accesses_threadpool el σ a1 a2 l →
              nonracing_accesses a1 a2.
 
-Lemma next_access_head_head K e σ a l:
-  next_access_head (fill_item K e) σ a l → is_Some (to_val e).
+Lemma next_access_base_reductible_ctx e σ σ' a l K :
+  next_access_head e σ' a l → reducible (fill K e) σ → base_reducible e σ.
 Proof.
-  destruct K; inversion 1; eauto.
+  intros Hhead Hred. apply prim_base_reducible.
+  - eapply (reducible_fill_inv (K:=ectx_language.fill K)), Hred. destruct Hhead; eauto.
+  - apply ectxi_language_sub_redexes_are_values. intros [] ? ->; inversion Hhead; eauto.
 Qed.
 
-Lemma next_access_head_reductible_ctx e σ σ' a l K :
-  next_access_head e σ' a l → reducible (fill K e) σ → head_reducible e σ.
-Proof.
-  intros Ha. apply step_is_head.
-  - by destruct Ha.
-  - clear -Ha. intros Ki K e' Heq (?&?&?&Hstep).
-    subst e. apply next_access_head_head in Ha.
-    change to_val with ectxi_language.to_val in Ha.
-    rewrite fill_not_val in Ha. by eapply is_Some_None. by eapply val_stuck.
-Qed.
+Definition base_reduce_not_to_stuck (e : expr) (σ : state) :=
+  ∀ κ e' σ' efs, ectx_language.base_step e σ κ e' σ' efs → e' ≠ App (Lit $ LitInt 0) [].
 
-Definition head_reduce_not_to_stuck e σ :=
-  ∀ e' σ' efs, ectx_language.head_step e σ e' σ' efs → e' ≠ App (Lit $ LitInt 0) [].
-
-Lemma next_access_head_reducible_state e σ a l :
-  next_access_head e σ a l → head_reducible e σ →
-  head_reduce_not_to_stuck e σ →
+Lemma next_access_base_reducible_state e σ a l :
+  next_access_head e σ a l → base_reducible e σ →
+  base_reduce_not_to_stuck e σ →
   match a with
-  | (ReadAcc, ScOrd | Na1Ord) => ∃ v n, σ !! l = Some (RSt n, v)
+  | (ReadAcc, (ScOrd | Na1Ord)) => ∃ v n, σ !! l = Some (RSt n, v)
   | (ReadAcc, Na2Ord) => ∃ v n, σ !! l = Some (RSt (S n), v)
-  | (WriteAcc, ScOrd | Na1Ord) => ∃ v, σ !! l = Some (RSt 0, v)
+  | (WriteAcc, (ScOrd | Na1Ord)) => ∃ v, σ !! l = Some (RSt 0, v)
   | (WriteAcc, Na2Ord) => ∃ v, σ !! l = Some (WSt, v)
   | (FreeAcc, _) => ∃ v ls, σ !! l = Some (ls, v)
   end.
 Proof.
-(*  assert (Hrefl : ∀ l, ~lit_neq σ l l).
-    { intros ? Hneq. inversion Hneq; done. } *)
-  intros Ha (e'&σ'&ef&Hstep) Hrednonstuck. destruct Ha; inv_head_step; eauto.
-  - destruct n; first by eexists. exfalso. eapply Hrednonstuck; last done.
-    eapply CasStuckS; done.
+  intros Ha (κ&e'&σ'&ef&Hstep) Hrednonstuck. destruct Ha; inv_base_step; eauto.
+  - rename select nat into n.
+    destruct n; first by eexists. exfalso. eapply Hrednonstuck; last done.
+    by eapply CasStuckS.
   - exfalso. eapply Hrednonstuck; last done.
     eapply CasStuckS; done.
-  - match goal with H : ∀ m, _ |- _ => destruct (H i) as [_ [[]?]] end; eauto.
+  - match goal with H : ∀ m, _ |- context[_ +ₗ ?i] => destruct (H i) as [_ [[]?]] end; eauto.
 Qed.
 
-Lemma next_access_head_Na1Ord_step e1 e2 ef σ1 σ2 a l :
+Lemma next_access_base_Na1Ord_step e1 e2 ef σ1 σ2 κ a l :
   next_access_head e1 σ1 (a, Na1Ord) l →
-  head_step e1 σ1 e2 σ2 ef →
+  base_step e1 σ1 κ e2 σ2 ef →
   next_access_head e2 σ2 (a, Na2Ord) l.
 Proof.
-  intros Ha Hstep. inversion Ha; subst; clear Ha; inv_head_step; constructor.
-  by rewrite to_of_val.
+  intros Ha Hstep. inversion Ha; subst; clear Ha; inv_base_step; constructor; by rewrite to_of_val.
 Qed.
 
-Lemma next_access_head_Na1Ord_concurent_step e1 e1' e2 e'f σ σ' a1 a2 l :
+Lemma next_access_base_Na1Ord_concurent_step e1 e1' e2 e'f σ σ' κ a1 a2 l :
   next_access_head e1 σ (a1, Na1Ord) l →
-  head_step e1 σ e1' σ' e'f →
+  base_step e1 σ κ e1' σ' e'f →
   next_access_head e2 σ a2 l →
   next_access_head e2 σ' a2 l.
 Proof.
-  intros Ha1 Hstep Ha2. inversion Ha1; subst; clear Ha1; inv_head_step;
+  intros Ha1 Hstep Ha2. inversion Ha1; subst; clear Ha1; inv_base_step;
   destruct Ha2; simplify_eq; econstructor; eauto; try apply lookup_insert.
-  (* Oh my. FIXME RJ. *)
-  - eapply lit_neq_state; last done.
-    setoid_rewrite <-not_elem_of_dom. rewrite dom_insert_L.
-    cut (is_Some (σ !! l)); last by eexists. rewrite -elem_of_dom. set_solver+.
+  (* Oh my. FIXME. *)
   - eapply lit_eq_state; last done.
     setoid_rewrite <-not_elem_of_dom. rewrite dom_insert_L.
-    cut (is_Some (σ !! l)); last by eexists. rewrite -elem_of_dom. set_solver+.
-  - eapply lit_neq_state; last done.
-    setoid_rewrite <-not_elem_of_dom. rewrite dom_insert_L.
+    rename select loc into l.
+    rename select state into σ.
     cut (is_Some (σ !! l)); last by eexists. rewrite -elem_of_dom. set_solver+.
   - eapply lit_eq_state; last done.
     setoid_rewrite <-not_elem_of_dom. rewrite dom_insert_L.
+    rename select loc into l.
+    rename select state into σ.
     cut (is_Some (σ !! l)); last by eexists. rewrite -elem_of_dom. set_solver+.
 Qed.
 
-Lemma next_access_head_Free_concurent_step e1 e1' e2 e'f σ σ' o1 a2 l :
-  next_access_head e1 σ (FreeAcc, o1) l → head_step e1 σ e1' σ' e'f →
-  next_access_head e2 σ a2 l → head_reducible e2 σ' →
+Lemma next_access_base_Free_concurent_step e1 e1' e2 e'f σ σ' κ o1 a2 l :
+  next_access_head e1 σ (FreeAcc, o1) l → base_step e1 σ κ e1' σ' e'f →
+  next_access_head e2 σ a2 l → base_reducible e2 σ' →
   False.
 Proof.
   intros Ha1 Hstep Ha2 Hred2.
-  assert (FREE : ∀ l n i, 0 ≤ i ∧ i < n → free_mem l (Z.to_nat n) σ !! shift_loc l i = None).
+  assert (FREE : ∀ l n i, 0 ≤ i ∧ i < n → free_mem l (Z.to_nat n) σ !! (l +ₗ i) = None).
   { clear. intros l n i Hi.
     replace n with (Z.of_nat (Z.to_nat n)) in Hi by (apply Z2Nat.id; lia).
-    revert l i Hi. induction (Z.to_nat n) as [|? IH]=>/=l i Hi. lia.
+    revert l i Hi. induction (Z.to_nat n) as [|? IH]=>/=l i Hi; first lia.
     destruct (decide (i = 0)).
     - subst. by rewrite /shift_loc Z.add_0_r -surjective_pairing lookup_delete.
     - replace i with (1+(i-1)) by lia.
-      rewrite lookup_delete_ne -shift_loc_assoc ?IH //. lia.
-      destruct l; intros [=?]. lia. }
+      rewrite lookup_delete_ne -shift_loc_assoc ?IH //; first lia.
+      destruct l; intros [= ?]. lia. }
   assert (FREE' : σ' !! l = None).
-  { inversion Ha1; clear Ha1; inv_head_step. auto. }
-  destruct Hred2 as (e2'&σ''&ef&?).
-  inversion Ha2; clear Ha2; inv_head_step.
+  { inversion Ha1; clear Ha1; inv_base_step. auto. }
+  destruct Hred2 as (κ'&e2'&σ''&ef&?).
+  inversion Ha2; clear Ha2; inv_base_step.
   eapply (@is_Some_None (lock_state * val)). rewrite -FREE'. naive_solver.
 Qed.
 
-Lemma safe_step_not_reduce_to_stuck el σ K e e' σ' ef :
-  (∀ el' σ' e', rtc step (el, σ) (el', σ') →
+Lemma safe_step_not_reduce_to_stuck el σ K e e' σ' ef κ :
+  (∀ el' σ' e', rtc erased_step (el, σ) (el', σ') →
                 e' ∈ el' → to_val e' = None → reducible e' σ') →
-  fill K e ∈ el → head_step e σ e' σ' ef → head_reduce_not_to_stuck e' σ'.
+  fill K e ∈ el → base_step e σ κ e' σ' ef → base_reduce_not_to_stuck e' σ'.
 Proof.
-  intros Hsafe Hi Hstep e1 σ1 ? Hstep1 Hstuck.
+  intros Hsafe Hi Hstep κ1 e1 σ1 ? Hstep1 Hstuck.
   cut (reducible (fill K e1) σ1).
-  { subst. intros (?&?&?&?). eapply stuck_irreducible. done. }
+  { subst. intros (?&?&?&?&?). by eapply stuck_irreducible. }
   destruct (elem_of_list_split _ _ Hi) as (?&?&->).
   eapply Hsafe; last by (apply: fill_not_val; subst).
   - eapply rtc_l, rtc_l, rtc_refl.
-    + econstructor. done. done. econstructor; done.
-    + econstructor. done. done. econstructor; done.
+    + eexists. econstructor; [done..|]. econstructor; done.
+    + eexists. econstructor; [done..|]. econstructor; done.
   - subst. set_solver+.
 Qed.
 
 (* TODO: Unify this and the above. *)
 Lemma safe_not_reduce_to_stuck el σ K e :
-  (∀ el' σ' e', rtc step (el, σ) (el', σ') →
+  (∀ el' σ' e', rtc erased_step (el, σ) (el', σ') →
                 e' ∈ el' → to_val e' = None → reducible e' σ') →
-  fill K e ∈ el → head_reduce_not_to_stuck e σ.
+  fill K e ∈ el → base_reduce_not_to_stuck e σ.
 Proof.
-  intros Hsafe Hi e1 σ1 ? Hstep1 Hstuck.
+  intros Hsafe Hi κ e1 σ1 ? Hstep1 Hstuck.
   cut (reducible (fill K e1) σ1).
-  { subst. intros (?&?&?&?). eapply stuck_irreducible. done. }
+  { subst. intros (?&?&?&?&?). by eapply stuck_irreducible. }
   destruct (elem_of_list_split _ _ Hi) as (?&?&->).
   eapply Hsafe; last by (apply: fill_not_val; subst).
   - eapply rtc_l, rtc_refl.
-    + econstructor. done. done. econstructor; done.
+    + eexists. econstructor; [done..|]. econstructor; done.
   - subst. set_solver+.
 Qed.
 
 Theorem safe_nonracing el σ :
-  (∀ el' σ' e', rtc step (el, σ) (el', σ') →
+  (∀ el' σ' e', rtc erased_step (el, σ) (el', σ') →
                 e' ∈ el' → to_val e' = None → reducible e' σ') →
   nonracing_threadpool el σ.
 Proof.
-  change to_val with ectxi_language.to_val.
   intros Hsafe l a1 a2 (t1&?&t2&?&t3&->&(K1&e1&Ha1&->)&(K2&e2&Ha2&->)).
 
-  assert (to_val e1 = None). by destruct Ha1.
-  assert (Hrede1:head_reducible e1 σ).
-  { eapply (next_access_head_reductible_ctx e1 σ σ a1 l K1), Hsafe, fill_not_val=>//.
+  assert (to_val e1 = None) by by destruct Ha1.
+  assert (Hrede1:base_reducible e1 σ).
+  { eapply (next_access_base_reductible_ctx e1 σ σ a1 l K1), Hsafe, fill_not_val=>//.
     abstract set_solver. }
-  assert (Hnse1:head_reduce_not_to_stuck e1 σ).
-  { eapply safe_not_reduce_to_stuck with (K:=K1); first done. set_solver+. }
-  assert (Hσe1:=next_access_head_reducible_state _ _ _ _ Ha1 Hrede1 Hnse1).
-  destruct Hrede1 as (e1'&σ1'&ef1&Hstep1). clear Hnse1.
+  assert (Hnse1:base_reduce_not_to_stuck e1 σ).
+  { eapply (safe_not_reduce_to_stuck _ _ K1); first done. set_solver+. }
+  assert (Hσe1:=next_access_base_reducible_state _ _ _ _ Ha1 Hrede1 Hnse1).
+  destruct Hrede1 as (κ1'&e1'&σ1'&ef1&Hstep1). clear Hnse1.
   assert (Ha1' : a1.2 = Na1Ord → next_access_head e1' σ1' (a1.1, Na2Ord) l).
-  { intros. eapply next_access_head_Na1Ord_step, Hstep1.
+  { intros. eapply next_access_base_Na1Ord_step, Hstep1.
     by destruct a1; simpl in *; subst. }
   assert (Hrtc_step1:
-    rtc step (t1 ++ fill K1 e1 :: t2 ++ fill K2 e2 :: t3, σ)
+    rtc erased_step (t1 ++ fill K1 e1 :: t2 ++ fill K2 e2 :: t3, σ)
         (t1 ++ fill K1 e1' :: t2 ++ fill K2 e2 :: t3 ++ ef1, σ1')).
-  { eapply rtc_l, rtc_refl. eapply step_atomic, Ectx_step, Hstep1; try  done.
+  { eapply rtc_l, rtc_refl. eexists. eapply step_atomic, Ectx_step, Hstep1; try  done.
     by rewrite -assoc. }
-  assert (Hrede1: a1.2 = Na1Ord → head_reducible e1' σ1').
+  assert (Hrede1: a1.2 = Na1Ord → base_reducible e1' σ1').
   { destruct a1 as [a1 []]=>// _.
-    eapply (next_access_head_reductible_ctx e1' σ1' σ1' (a1, Na2Ord) l K1), Hsafe,
+    eapply (next_access_base_reductible_ctx e1' σ1' σ1' (a1, Na2Ord) l K1), Hsafe,
            fill_not_val=>//.
-    by auto. abstract set_solver. by destruct Hstep1; inversion Ha1. }
-  assert (Hnse1: head_reduce_not_to_stuck e1' σ1').
-  { eapply safe_step_not_reduce_to_stuck with (K:=K1); first done; last done. set_solver+. }
+    - by auto.
+    - abstract set_solver.
+    - by destruct Hstep1; inversion Ha1. }
+  assert (Hnse1: base_reduce_not_to_stuck e1' σ1').
+  { eapply (safe_step_not_reduce_to_stuck _ _ K1); first done; last done. set_solver+. }
 
-  assert (to_val e2 = None). by destruct Ha2.
-  assert (Hrede2:head_reducible e2 σ).
-  { eapply (next_access_head_reductible_ctx e2 σ σ a2 l K2), Hsafe, fill_not_val=>//.
+  assert (to_val e2 = None) by by destruct Ha2.
+  assert (Hrede2:base_reducible e2 σ).
+  { eapply (next_access_base_reductible_ctx e2 σ σ a2 l K2), Hsafe, fill_not_val=>//.
     abstract set_solver. }
-  assert (Hnse2:head_reduce_not_to_stuck e2 σ).
-  { eapply safe_not_reduce_to_stuck with (K:=K2); first done. set_solver+. }
-  assert (Hσe2:=next_access_head_reducible_state _ _ _ _ Ha2 Hrede2 Hnse2).
-  destruct Hrede2 as (e2'&σ2'&ef2&Hstep2).
+  assert (Hnse2:base_reduce_not_to_stuck e2 σ).
+  { eapply (safe_not_reduce_to_stuck _ _ K2); first done. set_solver+. }
+  assert (Hσe2:=next_access_base_reducible_state _ _ _ _ Ha2 Hrede2 Hnse2).
+  destruct Hrede2 as (κ2'&e2'&σ2'&ef2&Hstep2).
   assert (Ha2' : a2.2 = Na1Ord → next_access_head e2' σ2' (a2.1, Na2Ord) l).
-  { intros. eapply next_access_head_Na1Ord_step, Hstep2.
+  { intros. eapply next_access_base_Na1Ord_step, Hstep2.
     by destruct a2; simpl in *; subst. }
   assert (Hrtc_step2:
-    rtc step (t1 ++ fill K1 e1 :: t2 ++ fill K2 e2 :: t3, σ)
+    rtc erased_step (t1 ++ fill K1 e1 :: t2 ++ fill K2 e2 :: t3, σ)
         (t1 ++ fill K1 e1 :: t2 ++ fill K2 e2' :: t3 ++ ef2, σ2')).
-  { eapply rtc_l, rtc_refl. rewrite app_comm_cons assoc.
+  { eapply rtc_l, rtc_refl. rewrite app_comm_cons assoc. eexists.
     eapply step_atomic, Ectx_step, Hstep2; try done. by rewrite -assoc. }
-  assert (Hrede2: a2.2 = Na1Ord → head_reducible e2' σ2').
+  assert (Hrede2: a2.2 = Na1Ord → base_reducible e2' σ2').
   { destruct a2 as [a2 []]=>// _.
-    eapply (next_access_head_reductible_ctx e2' σ2' σ2' (a2, Na2Ord) l K2), Hsafe,
+    eapply (next_access_base_reductible_ctx e2' σ2' σ2' (a2, Na2Ord) l K2), Hsafe,
            fill_not_val=>//.
-    by auto. abstract set_solver. by destruct Hstep2; inversion Ha2. }
-  assert (Hnse2':head_reduce_not_to_stuck e2' σ2').
-  { eapply safe_step_not_reduce_to_stuck with (K:=K2); first done; last done. set_solver+. }
+    - by auto.
+    - abstract set_solver.
+    - by destruct Hstep2; inversion Ha2. }
+  assert (Hnse2':base_reduce_not_to_stuck e2' σ2').
+  { eapply (safe_step_not_reduce_to_stuck _ _ K2); first done; last done. set_solver+. }
 
   assert (Ha1'2 : a1.2 = Na1Ord → next_access_head e2 σ1' a2 l).
-  { intros HNa. eapply next_access_head_Na1Ord_concurent_step=>//.
+  { intros HNa. eapply next_access_base_Na1Ord_concurent_step=>//.
     by rewrite <-HNa, <-surjective_pairing. }
-  assert (Hrede1_2: head_reducible e2 σ1').
-  { intros. eapply (next_access_head_reductible_ctx e2 σ1' σ  a2 l K2), Hsafe, fill_not_val=>//.
+  assert (Hrede1_2: base_reducible e2 σ1').
+  { intros. eapply (next_access_base_reductible_ctx e2 σ1' σ  a2 l K2), Hsafe, fill_not_val=>//.
     abstract set_solver. }
-  assert (Hnse1_2:head_reduce_not_to_stuck e2 σ1').
-  { eapply safe_not_reduce_to_stuck with (K:=K2).
-    - intros. eapply Hsafe. etrans; last done. done. done. done.
+  assert (Hnse1_2:base_reduce_not_to_stuck e2 σ1').
+  { eapply (safe_not_reduce_to_stuck _ _ K2).
+    - intros. eapply Hsafe; [|done..]. etrans; last done. done.
     - set_solver+. }
   assert (Hσe1'1:=
-    λ Hord, next_access_head_reducible_state _ _ _ _ (Ha1' Hord) (Hrede1 Hord) Hnse1).
+    λ Hord, next_access_base_reducible_state _ _ _ _ (Ha1' Hord) (Hrede1 Hord) Hnse1).
   assert (Hσe1'2:=
-    λ Hord, next_access_head_reducible_state _ _ _ _ (Ha1'2 Hord) Hrede1_2 Hnse1_2).
+    λ Hord, next_access_base_reducible_state _ _ _ _ (Ha1'2 Hord) Hrede1_2 Hnse1_2).
 
   assert (Ha2'1 : a2.2 = Na1Ord → next_access_head e1 σ2' a1 l).
-  { intros HNa. eapply next_access_head_Na1Ord_concurent_step=>//.
+  { intros HNa. eapply next_access_base_Na1Ord_concurent_step=>//.
     by rewrite <-HNa, <-surjective_pairing. }
-  assert (Hrede2_1: head_reducible e1 σ2').
-  { intros. eapply (next_access_head_reductible_ctx e1 σ2' σ a1 l K1), Hsafe, fill_not_val=>//.
+  assert (Hrede2_1: base_reducible e1 σ2').
+  { intros. eapply (next_access_base_reductible_ctx e1 σ2' σ a1 l K1), Hsafe, fill_not_val=>//.
     abstract set_solver. }
-  assert (Hnse2_1:head_reduce_not_to_stuck e1 σ2').
-  { eapply safe_not_reduce_to_stuck with (K:=K1).
-    - intros. eapply Hsafe. etrans; last done. done. done. done.
+  assert (Hnse2_1:base_reduce_not_to_stuck e1 σ2').
+  { eapply (safe_not_reduce_to_stuck _ _ K1).
+    - intros. eapply Hsafe; [|done..]. etrans; last done. done.
     - set_solver+. }
   assert (Hσe2'1:=
-    λ Hord, next_access_head_reducible_state _ _ _ _ (Ha2'1 Hord) Hrede2_1 Hnse2_1).
+    λ Hord, next_access_base_reducible_state _ _ _ _ (Ha2'1 Hord) Hrede2_1 Hnse2_1).
   assert (Hσe2'2:=
-    λ Hord, next_access_head_reducible_state _ _ _ _ (Ha2' Hord) (Hrede2 Hord) Hnse2').
+    λ Hord, next_access_base_reducible_state _ _ _ _ (Ha2' Hord) (Hrede2 Hord) Hnse2').
 
   assert (a1.1 = FreeAcc → False).
   { destruct a1 as [[]?]; inversion 1.
-    eauto using next_access_head_Free_concurent_step. }
+    eauto using next_access_base_Free_concurent_step. }
   assert (a2.1 = FreeAcc → False).
   { destruct a2 as [[]?]; inversion 1.
-    eauto using next_access_head_Free_concurent_step. }
+    eauto using next_access_base_Free_concurent_step. }
 
   destruct Ha1 as [[]|[]| | |], Ha2 as [[]|[]| | |]=>//=; simpl in *;
     repeat match goal with
@@ -299,19 +288,21 @@ Proof.
     end;
     try congruence.
 
-  clear e2' Hnse2' Hnse2_1 Hstep2 σ2' Hrtc_step2 Hrede2_1. destruct Hrede1_2 as (e2'&σ'&ef&?).
-  inv_head_step.
+  clear κ2' e2' Hnse2' Hnse2_1 Hstep2 σ2' Hrtc_step2 Hrede2_1.
+  destruct Hrede1_2 as (κ2'&e2'&σ'&ef&?).
+  inv_base_step.
   match goal with
-  | H : <[l:=_]> σ !! l = _ |- _ => by rewrite lookup_insert in H
+  | H : <[?l:=_]> ?σ !! ?l = _ |- _ => by rewrite lookup_insert in H
   end.
 Qed.
 
 Corollary adequate_nonracing e1 t2 σ1 σ2 φ :
-  adequate e1 σ1 φ →
-  rtc step ([e1], σ1) (t2, σ2) →
+  adequate NotStuck e1 σ1 φ →
+  rtc erased_step ([e1], σ1) (t2, σ2) →
   nonracing_threadpool t2 σ2.
 Proof.
   intros [_ Had] Hrtc. apply safe_nonracing. intros el' σ' e' ?? He'.
-  edestruct (Had el' σ' e') as [He''|]; try done. etrans; eassumption.
-  rewrite /language.to_val /= He' in He''. by edestruct @is_Some_None.
+  edestruct (Had el' σ' e') as [He''|]; try done.
+  - etrans; eassumption.
+  - rewrite /language.to_val /= He' in He''. by edestruct @is_Some_None.
 Qed.

theories/lang/tactics.v → lambda-rust/lang/tactics.v

-From iris.prelude Require Import fin_maps.
+From stdpp Require Import fin_maps.
 From lrust.lang Require Export lang.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
 
 (** We define an alternative representation of expressions in which the
 embedding of values and closed expressions is explicit. By reification of
@@ -8,7 +8,7 @@ expressions into this type we can implement substitution, closedness
 checking, atomic checking, and conversion into values, by computation. *)
 Module W.
 Inductive expr :=
-| Val (v : val)
+| Val (v : val) (e : lang.expr) (H : to_val e = Some v)
 | ClosedExpr (e : lang.expr) `{!Closed [] e}
 | Var (x : string)
 | Lit (l : base_lit)
@@ -25,8 +25,8 @@ Inductive expr :=
 
 Fixpoint to_expr (e : expr) : lang.expr :=
   match e with
-  | Val v => of_val v
-  | ClosedExpr e _ => e
+  | Val v e' _ => e'
+  | ClosedExpr e => e
   | Var x => lang.Var x
   | Lit l => lang.Lit l
   | Rec f xl e => lang.Rec f xl (to_expr e)
@@ -66,14 +66,16 @@ Ltac of_expr e :=
   | @cons lang.expr ?e ?el =>
     let e := of_expr e in let el := of_expr el in constr:(e::el)
   | to_expr ?e => e
-  | of_val ?v => constr:(Val v)
-  | _ => constr:(ltac:(
-     match goal with H : Closed [] e |- _ => exact (@ClosedExpr e H) end))
+  | of_val ?v => constr:(Val v (of_val v) (to_of_val v))
+  | _ => match goal with
+         | H : to_val e = Some ?v |- _ => constr:(Val v e H)
+         | H : Closed [] e |- _ => constr:(@ClosedExpr e H)
+         end
   end.
 
 Fixpoint is_closed (X : list string) (e : expr) : bool :=
   match e with
-  | Val _ | ClosedExpr _ _ => true
+  | Val _ _ _ | ClosedExpr _ => true
   | Var x => bool_decide (x ∈ X)
   | Lit _ => true
   | Rec f xl e => is_closed (f :b: xl +b+ X) e
@@ -85,10 +87,10 @@ Fixpoint is_closed (X : list string) (e : expr) : bool :=
   end.
 Lemma is_closed_correct X e : is_closed X e → lang.is_closed X (to_expr e).
 Proof.
-  revert e X. fix 1; destruct e=>/=;
-    try naive_solver eauto using is_closed_of_val, is_closed_weaken_nil.
-  - induction el=>/=; naive_solver.
-  - induction el=>/=; naive_solver.
+  revert e X. fix FIX 1; intros e; destruct e=>/=;
+    try naive_solver eauto using is_closed_to_val, is_closed_weaken_nil.
+  - rename select (list expr) into el. induction el=>/=; naive_solver.
+  - rename select (list expr) into el. induction el=>/=; naive_solver.
 Qed.
 
 (* We define [to_val (ClosedExpr _)] to be [None] since [ClosedExpr]
@@ -97,7 +99,7 @@ about apart from being closed. Notice that the reverse implication of
 [to_val_Some] thus does not hold. *)
 Definition to_val (e : expr) : option val :=
   match e with
-  | Val v => Some v
+  | Val v _ _ => Some v
   | Rec f xl e =>
     if decide (is_closed (f :b: xl +b+ []) e) is left H
     then Some (@RecV f xl (to_expr e) (is_closed_correct _ _ H)) else None
@@ -105,20 +107,21 @@ Definition to_val (e : expr) : option val :=
   | _ => None
   end.
 Lemma to_val_Some e v :
-  to_val e = Some v → lang.to_val (to_expr e) = Some v.
+  to_val e = Some v → of_val v = W.to_expr e.
 Proof.
-  revert v. induction e; intros; simplify_option_eq; rewrite ?to_of_val; auto.
-  - do 2 f_equal. apply proof_irrel.
-  - exfalso. unfold Closed in *; eauto using is_closed_correct.
+  revert v. induction e; intros; simplify_option_eq; auto using of_to_val.
 Qed.
 Lemma to_val_is_Some e :
-  is_Some (to_val e) → is_Some (lang.to_val (to_expr e)).
+  is_Some (to_val e) → ∃ v, of_val v = to_expr e.
 Proof. intros [v ?]; exists v; eauto using to_val_Some. Qed.
+Lemma to_val_is_Some' e :
+  is_Some (to_val e) → is_Some (lang.to_val (to_expr e)).
+Proof. intros [v ?]%to_val_is_Some. exists v. rewrite -to_of_val. by f_equal. Qed.
 
 Fixpoint subst (x : string) (es : expr) (e : expr)  : expr :=
   match e with
-  | Val v => Val v
-  | ClosedExpr e H => @ClosedExpr e H
+  | Val v e H => Val v e H
+  | ClosedExpr e => ClosedExpr e
   | Var y => if bool_decide (y = x) then es else Var y
   | Lit l => Lit l
   | Rec f xl e =>
@@ -136,13 +139,13 @@ Fixpoint subst (x : string) (es : expr) (e : expr)  : expr :=
 Lemma to_expr_subst x er e :
   to_expr (subst x er e) = lang.subst x (to_expr er) (to_expr e).
 Proof.
-  revert e x er. fix 1; destruct e=>/= ? er; repeat case_bool_decide;
-    f_equal; auto using is_closed_nil_subst, is_closed_of_val, eq_sym.
-  - induction el=>//=. f_equal; auto.
-  - induction el=>//=. f_equal; auto.
+  revert e x er. fix FIX 1; intros e; destruct e=>/= ? er; repeat case_bool_decide;
+    f_equal; eauto using is_closed_nil_subst, is_closed_to_val, eq_sym.
+  - rename select (list expr) into el. induction el=>//=. f_equal; auto.
+  - rename select (list expr) into el. induction el=>//=. f_equal; auto.
 Qed.
 
-Definition atomic (e: expr) : bool :=
+Definition is_atomic (e: expr) : bool :=
   match e with
   | Read (ScOrd | Na2Ord) e | Alloc e => bool_decide (is_Some (to_val e))
   | Write (ScOrd | Na2Ord) e1 e2 | Free e1 e2 =>
@@ -151,19 +154,18 @@ Definition atomic (e: expr) : bool :=
     bool_decide (is_Some (to_val e0) ∧ is_Some (to_val e1) ∧ is_Some (to_val e2))
   | _ => false
   end.
-Lemma atomic_correct e : atomic e → language.atomic (to_expr e).
+Lemma is_atomic_correct e : is_atomic e → Atomic WeaklyAtomic (to_expr e).
 Proof.
   intros He. apply ectx_language_atomic.
-  - intros σ e' σ' ef.
+  - intros σ ef e' σ'.
     destruct e; simpl; try done; repeat (case_match; try done);
     inversion 1; try (apply val_irreducible; rewrite ?language.to_of_val; naive_solver eauto); [].
     rewrite -[stuck_term](fill_empty). apply stuck_irreducible.
-  - intros [|Ki K] e' Hfill Hnotval; [done|exfalso].
-    apply (fill_not_val K), eq_None_not_Some in Hnotval. apply Hnotval. simpl.
+  - apply ectxi_language_sub_redexes_are_values=> /= Ki e' Hfill.
     revert He. destruct e; simpl; try done; repeat (case_match; try done);
     rewrite ?bool_decide_spec;
     destruct Ki; inversion Hfill; subst; clear Hfill;
-    try naive_solver eauto using to_val_is_Some.
+    try naive_solver eauto using to_val_is_Some'.
 Qed.
 End W.
 
@@ -173,31 +175,49 @@ Ltac solve_closed :=
      let e' := W.of_expr e in change (Closed X (W.to_expr e'));
      apply W.is_closed_correct; vm_compute; exact I
   end.
-Hint Extern 0 (Closed _ _) => solve_closed : typeclass_instances.
+Global Hint Extern 0 (Closed _ _) => solve_closed : typeclass_instances.
 
-Ltac solve_to_val :=
-  try match goal with
-  | |- context E [language.to_val ?e] =>
-     let X := context E [to_val e] in change X
-  end;
+Ltac solve_into_val :=
+  match goal with
+  | |- IntoVal ?e ?v =>
+     let e' := W.of_expr e in change (of_val v = W.to_expr e');
+     apply W.to_val_Some; simpl; unfold W.to_expr;
+     ((unlock; exact eq_refl) || (idtac; exact eq_refl))
+  end.
+Global Hint Extern 10 (IntoVal _ _) => solve_into_val : typeclass_instances.
+
+Ltac solve_as_val :=
   match goal with
-  | |- to_val ?e = Some ?v =>
-     let e' := W.of_expr e in change (to_val (W.to_expr e') = Some v);
-     apply W.to_val_Some; simpl; unfold W.to_expr; reflexivity
-  | |- is_Some (to_val ?e) =>
-     let e' := W.of_expr e in change (is_Some (to_val (W.to_expr e')));
+  | |- AsVal ?e =>
+     let e' := W.of_expr e in change (∃ v, of_val v = W.to_expr e');
      apply W.to_val_is_Some, (bool_decide_unpack _); vm_compute; exact I
   end.
+Global Hint Extern 10 (AsVal _) => solve_as_val : typeclass_instances.
 
 Ltac solve_atomic :=
   match goal with
-  | |- language.atomic ?e =>
-     let e' := W.of_expr e in change (language.atomic (W.to_expr e'));
-     apply W.atomic_correct; vm_compute; exact I
+  | |- Atomic ?s ?e =>
+     let e' := W.of_expr e in change (Atomic s (W.to_expr e'));
+     apply W.is_atomic_correct; vm_compute; exact I
   end.
-Hint Extern 0 (language.atomic _) => solve_atomic.
-(* For the side-condition of elim_vs_pvs_wp_atomic *)
-Hint Extern 0 (language.atomic _) => solve_atomic : typeclass_instances.
+Global Hint Extern 0 (Atomic _ _) => solve_atomic : typeclass_instances.
+
+Global Instance skip_atomic : Atomic WeaklyAtomic Skip.
+Proof.
+  apply strongly_atomic_atomic, ectx_language_atomic.
+  - inversion 1. naive_solver.
+  - apply ectxi_language_sub_redexes_are_values. intros [] * Hskip; try naive_solver.
+    + inversion Hskip. simpl. rewrite decide_True_pi. eauto.
+    + inversion Hskip. rename select ([Lit _] = _) into Hargs.
+      assert (length [Lit LitPoison] = 1%nat) as Hlen by done. move:Hlen.
+      rewrite Hargs. rewrite length_app length_fmap /=.
+      rename select (list val) into vl. rename select (list expr) into el.
+      destruct vl; last first.
+      { simpl. intros. exfalso. lia. }
+      destruct el; last first.
+      { simpl. intros. exfalso. lia. }
+      simpl in *. intros _. inversion Hargs. eauto.
+Qed.
 
 (** Substitution *)
 Ltac simpl_subst :=
@@ -209,15 +229,15 @@ Ltac simpl_subst :=
       rewrite <-(W.to_expr_subst x); simpl (* ssr rewrite is slower *)
   end;
   unfold W.to_expr; simpl.
-Arguments W.to_expr : simpl never.
-Arguments subst : simpl never.
+Global Arguments W.to_expr : simpl never.
+Global Arguments subst : simpl never.
 
-(** The tactic [inv_head_step] performs inversion on hypotheses of the
-shape [head_step]. The tactic will discharge head-reductions starting
+(** The tactic [inv_base_step] performs inversion on hypotheses of the
+shape [base_step]. The tactic will discharge head-reductions starting
 from values, and simplifies hypothesis related to conversions from and
 to values, and finite map operations. This tactic is slightly ad-hoc
 and tuned for proving our lifting lemmas. *)
-Ltac inv_head_step :=
+Ltac inv_base_step :=
   repeat match goal with
   | _ => progress simplify_map_eq/= (* simplify memory stuff *)
   | H : to_val _ = Some _ |- _ => apply of_to_val in H
@@ -225,7 +245,7 @@ Ltac inv_head_step :=
     apply (f_equal (to_val)) in H; rewrite to_of_val in H;
     injection H; clear H; intro
   | H : context [to_val (of_val _)] |- _ => rewrite to_of_val in H
-  | H : head_step ?e _ _ _ _ |- _ =>
+  | H : base_step ?e _ _ _ _ _ |- _ =>
      try (is_var e; fail 1); (* inversion yields many goals if [e] is a variable
      and can thus better be avoided. *)
      inversion H; subst; clear H
@@ -250,7 +270,7 @@ Ltac reshape_expr e tac :=
     end
   with go K e :=
   match e with
-  | _ => tac (reverse K) e
+  | _ => tac K e
   | BinOp ?op ?e1 ?e2 =>
      reshape_val e1 ltac:(fun v1 => go (BinOpRCtx op v1 :: K) e2)
   | BinOp ?op ?e1 ?e2 => go (BinOpLCtx op e2 :: K) e1
@@ -270,16 +290,3 @@ Ltac reshape_expr e tac :=
   | Case ?e ?el => go (CaseCtx el :: K) e
   end
   in go (@nil ectx_item) e.
-
-(** The tactic [do_head_step tac] solves goals of the shape [head_reducible] and
-[head_step] by performing a reduction step and uses [tac] to solve any
-side-conditions generated by individual steps. *)
-Tactic Notation "do_head_step" tactic3(tac) :=
-  try match goal with |- head_reducible _ _ => eexists _, _, _ end;
-  simpl;
-  match goal with
-  | |- head_step ?e1 ?σ1 ?e2 ?σ2 ?ef =>
-     first [apply alloc_fresh|econstructor];
-       (* solve [to_val] side-conditions *)
-       first [rewrite ?to_of_val; reflexivity|simpl_subst; tac; fast_done]
-  end.

lambda-rust/typing/base.v

+From stdpp Require Import namespaces.
+From lrust.lang Require Export proofmode.
+From iris.prelude Require Import options.
+
+(* Last, so that we make sure we shadow the defintion of delete for
+   sets coming from the prelude. *)
+From lrust.lang.lib Require Export new_delete.
+
+Global Open Scope Z_scope.
+
+Definition lft_userN : namespace := nroot .@ "lft_usr".
+
+(* The "user mask" of the lifetime logic. This needs to be disjoint with ↑lftN.
+
+   If a client library desires to put invariants in lft_userE, then it is
+   encouraged to place it in the already defined lft_userN. On the other hand,
+   extensions to the model of RustBelt itself (such as gpfsl for
+   the weak-mem extension) can require extending [lft_userE] with the relevant
+   namespaces. In that case all client libraries need to be re-checked to
+   ensure disjointness of [lft_userE] with their masks is maintained where
+   necessary. *)
+Definition lft_userE : coPset := ↑lft_userN.
+
+Create HintDb lrust_typing.
+Create HintDb lrust_typing_merge.
+
+(* We first try to solve everything without the merging rules, and
+   then start from scratch with them.
+
+   The reason is that we want we want the search proof search for
+   [tctx_extract_hasty] to suceed even if the type is an evar, and
+   merging makes it diverge in this case. *)
+Ltac solve_typing :=
+  (typeclasses eauto with lrust_typing typeclass_instances core; fail) ||
+  (typeclasses eauto with lrust_typing lrust_typing_merge typeclass_instances core; fail).
+
+Global Hint Constructors Forall Forall2 elem_of_list : lrust_typing.
+Global Hint Resolve submseteq_cons submseteq_inserts_l submseteq_inserts_r
+  : lrust_typing.
+
+Global Hint Extern 1 (@eq nat _ (Z.to_nat _)) =>
+  (etrans; [symmetry; exact: Nat2Z.id | reflexivity]) : lrust_typing.
+Global Hint Extern 1 (@eq nat (Z.to_nat _) _) =>
+  (etrans; [exact: Nat2Z.id | reflexivity]) : lrust_typing.
+
+Global Hint Resolve <- elem_of_app : lrust_typing.
+
+(* done is there to handle equalities with constants *)
+Global Hint Extern 100 (_ ≤ _) => simpl; first [done|lia] : lrust_typing.
+Global Hint Extern 100 (@eq Z _ _) => simpl; first [done|lia] : lrust_typing.
+Global Hint Extern 100 (@eq nat _ _) => simpl; first [done|lia] : lrust_typing.

theories/typing/bool.v → lambda-rust/typing/bool.v

-From iris.base_logic Require Import big_op.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From lrust.typing Require Export type.
 From lrust.typing Require Import programs.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
 
 Section bool.
-  Context `{typeG Σ}.
+  Context `{!typeGS Σ}.
 
   Program Definition bool : type :=
-    {| st_own tid vl := (∃ z:bool, ⌜vl = [ #z ]⌝)%I |}.
-  Next Obligation. iIntros (tid vl) "H". iDestruct "H" as (z) "%". by subst. Qed.
+    {| st_own tid vl :=
+         match vl return _ with
+         | [ #(LitInt (0|1))] => True
+         | _ => False
+         end%I |}.
+  Next Obligation. intros ? [|[[| |[|[]|]]|] []]; auto. Qed.
+  Next Obligation. intros ? [|[[| |[|[]|]]|] []]; apply _. Qed.
+
+  Global Instance bool_wf : TyWf bool := { ty_lfts := []; ty_wf_E := [] }.
 
   Global Instance bool_send : Send bool.
-  Proof. iIntros (tid1 tid2 vl). done. Qed.
+  Proof. done. Qed.
 End bool.
 
 Section typing.
-  Context `{typeG Σ}.
+  Context `{!typeGS Σ}.
 
-  Lemma type_bool_instr (b : Datatypes.bool) E L :
-    typed_instruction_ty E L [] #b bool.
+  Lemma type_bool_instr (b : Datatypes.bool) : typed_val #b bool.
   Proof.
-    iAlways. iIntros (tid qE) "_ _ $ $ $ _". wp_value.
-    rewrite tctx_interp_singleton tctx_hasty_val. iExists _. done.
+    iIntros (E L tid ?) "_ _ $ $ _". iApply wp_value.
+    rewrite tctx_interp_singleton tctx_hasty_val' //. by destruct b.
   Qed.
 
   Lemma type_bool (b : Datatypes.bool) E L C T x e :
     Closed (x :b: []) e →
-    (∀ (v : val), typed_body E L C ((v ◁ bool) :: T) (subst' x v e)) →
+    (∀ (v : val), typed_body E L C ((v ◁ bool) :: T) (subst' x v e)) -∗
     typed_body E L C T (let: x := #b in e).
-  Proof.
-    intros. eapply type_let; [done|apply type_bool_instr|solve_typing|done].
-  Qed.
+  Proof. iIntros. iApply type_let; [apply type_bool_instr|solve_typing|done]. Qed.
 
   Lemma type_if E L C T e1 e2 p:
-    (p ◁ bool)%TC ∈ T →
-    typed_body E L C T e1 → typed_body E L C T e2 →
+    p ◁ bool ∈ T →
+    typed_body E L C T e1 -∗ typed_body E L C T e2 -∗
     typed_body E L C T (if: p then e1 else e2).
   Proof.
-    iIntros (Hp He1 He2) "!#". iIntros (tid qE) "#HEAP #LFT Htl HE HL HC HT".
+    iIntros (Hp) "He1 He2". iIntros (tid qmax) "#LFT #HE Htl HL HC HT".
     iDestruct (big_sepL_elem_of _ _ _ Hp with "HT") as "#Hp".
-    wp_bind p. iApply (wp_hasty with "Hp"). iIntros (v) "_ Hown".
-    iDestruct "Hown" as (b) "Hv". iDestruct "Hv" as %[=->].
-    destruct b; wp_if.
-    - iApply (He1 with "HEAP LFT Htl HE HL HC HT").
-    - iApply (He2 with "HEAP LFT Htl HE HL HC HT").
+    wp_bind p. iApply (wp_hasty with "Hp").
+    iIntros ([[| |[|[]|]]|]) "_ H1"; try done; wp_case.
+    - iApply ("He2" with "LFT HE Htl HL HC HT").
+    - iApply ("He1" with "LFT HE Htl HL HC HT").
   Qed.
 End typing.

theories/typing/borrow.v → lambda-rust/typing/borrow.v

-From iris.proofmode Require Import tactics.
-From iris.base_logic Require Import big_op.
+From iris.proofmode Require Import proofmode.
 From lrust.lang Require Import proofmode.
 From lrust.typing Require Export uniq_bor shr_bor own.
 From lrust.typing Require Import lft_contexts type_context programs.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
 
 (** The rules for borrowing and derferencing borrowed non-Copy pointers are in
   a separate file so make sure that own.v and uniq_bor.v can be compiled
   concurrently. *)
 
 Section borrow.
-  Context `{typeG Σ}.
+  Context `{!typeGS Σ}.
 
   Lemma tctx_borrow E L p n ty κ :
     tctx_incl E L [p ◁ own_ptr n ty] [p ◁ &uniq{κ}ty; p ◁{κ} own_ptr n ty].
   Proof.
-    iIntros (tid ??) "#LFT $ $ H".
-    rewrite /tctx_interp big_sepL_singleton big_sepL_cons big_sepL_singleton.
-    iDestruct "H" as (v) "[% Hown]". iDestruct "Hown" as (l) "(EQ & Hmt & ?)".
-    iDestruct "EQ" as %[=->]. iMod (bor_create with "LFT Hmt") as "[Hbor Hext]". done.
-    iModIntro. iSplitL "Hbor".
-    - iExists _. iSplit. done. iExists _, _. erewrite <-uPred.iff_refl. eauto.
-    - iExists _. iSplit. done. iIntros "H†". iExists _. iFrame. iSplitR. by eauto.
-        by iMod ("Hext" with "H†") as "$".
+    iIntros (tid ??)  "#LFT _ $ [H _]".
+    iDestruct "H" as ([[]|]) "[% Hown]"; try done. iDestruct "Hown" as "[Hmt ?]".
+    iMod (bor_create with "LFT Hmt") as "[Hbor Hext]"; first done.
+    iModIntro. rewrite /tctx_interp /=. iSplitL "Hbor"; last iSplit; last done.
+    - iExists _. auto.
+    - iExists _. iSplit; first done. by iFrame.
+  Qed.
+
+  Lemma tctx_share E L p κ ty :
+    lctx_lft_alive E L κ → tctx_incl E L [p ◁ &uniq{κ}ty] [p ◁ &shr{κ}ty].
+  Proof.
+    iIntros (Hκ ???) "#LFT #HE HL Huniq".
+    iMod (Hκ with "HE HL") as (q) "[Htok Hclose]"; [try done..|].
+    rewrite !tctx_interp_singleton /=.
+    iDestruct "Huniq" as ([[]|]) "[% Huniq]"; try done.
+    iMod (ty.(ty_share) with "LFT Huniq Htok") as "[Hown Htok]"; [solve_ndisj|].
+    iMod ("Hclose" with "Htok") as "[$ $]". iExists _. by iFrame "%∗".
+  Qed.
+
+  (* When sharing during extraction, we do the (arbitrary) choice of
+     sharing at the lifetime requested (κ). In some cases, we could
+     actually desire a longer lifetime and then use subtyping, because
+     then we get, in the environment, a shared borrow at this longer
+     lifetime.
+
+     In the case the user wants to do the sharing at a longer
+     lifetime, she has to manually perform the extraction herself at
+     the desired lifetime. *)
+  Lemma tctx_extract_hasty_share E L p ty ty' κ κ' T :
+    lctx_lft_alive E L κ → lctx_lft_incl E L κ κ' → subtype E L ty' ty →
+    tctx_extract_hasty E L p (&shr{κ}ty) ((p ◁ &uniq{κ'}ty')::T)
+                       ((p ◁ &shr{κ}ty')::(p ◁{κ} &uniq{κ'}ty')::T).
+  Proof.
+    intros. apply (tctx_incl_frame_r _ [_] [_;_;_]).
+    rewrite tctx_reborrow_uniq //. apply (tctx_incl_frame_r _ [_] [_;_]).
+    rewrite tctx_share // {1}copy_tctx_incl.
+    by apply (tctx_incl_frame_r _ [_] [_]), subtype_tctx_incl, shr_mono'.
+  Qed.
+
+  Lemma tctx_extract_hasty_share_samelft E L p ty ty' κ T :
+    lctx_lft_alive E L κ → subtype E L ty' ty →
+    tctx_extract_hasty E L p (&shr{κ}ty) ((p ◁ &uniq{κ}ty')::T)
+                                         ((p ◁ &shr{κ}ty')::T).
+  Proof.
+    intros. apply (tctx_incl_frame_r _ [_] [_;_]).
+    rewrite tctx_share // {1}copy_tctx_incl.
+    by apply (tctx_incl_frame_r _ [_] [_]), subtype_tctx_incl, shr_mono'.
   Qed.
 
   Lemma tctx_extract_hasty_borrow E L p n ty ty' κ T :
@@ -31,10 +69,11 @@ Section borrow.
                        ((p ◁{κ} own_ptr n ty)::T).
   Proof.
     intros. apply (tctx_incl_frame_r _ [_] [_;_]). rewrite subtype_tctx_incl.
-    by apply tctx_borrow. by f_equiv.
+    - by apply tctx_borrow.
+    - by f_equiv.
   Qed.
 
-  (* See the comment above [tctx_extract_hasty_share] in [uniq_bor.v]. *)
+  (* See the comment above [tctx_extract_hasty_share]. *)
   Lemma tctx_extract_hasty_borrow_share E L p ty ty' κ n T :
     lctx_lft_alive E L κ → subtype E L ty' ty →
     tctx_extract_hasty E L p (&shr{κ}ty) ((p ◁ own_ptr n ty')::T)
@@ -46,142 +85,135 @@ Section borrow.
 
   Lemma type_deref_uniq_own_instr {E L} κ p n ty :
     lctx_lft_alive E L κ →
-    typed_instruction_ty E L [p ◁ &uniq{κ} own_ptr n ty] (!p) (&uniq{κ} ty).
+    ⊢ typed_instruction_ty E L [p ◁ &uniq{κ}(own_ptr n ty)] (!p) (&uniq{κ} ty).
   Proof.
-    iIntros (Hκ) "!#". iIntros (tid qE) "#HEAP #LFT $ HE HL Hp".
+    iIntros (Hκ tid qmax) "#LFT HE $ HL Hp".
     rewrite tctx_interp_singleton.
-    iMod (Hκ with "HE HL") as (q) "[Htok Hclose]"; first set_solver.
-    wp_bind p. iApply (wp_hasty with "Hp"). iIntros (v) "_ Hown".
-    iDestruct "Hown" as (l P) "[[Heq #HPiff] HP]". iDestruct "Heq" as %[=->].
-    iMod (bor_iff with "LFT [] HP") as "H↦". set_solver. by eauto.
-    iMod (bor_acc_cons with "LFT H↦ Htok") as "[H↦ Hclose']". done.
-    iDestruct "H↦" as (vl) "[>H↦ Hown]". iDestruct "Hown" as (l') "(>% & Hown & H†)".
-    subst. rewrite heap_mapsto_vec_singleton. wp_read.
-    iMod ("Hclose'" with "*[H↦ Hown H†][]") as "[Hbor Htok]"; last 1 first.
-    - iMod (bor_sep with "LFT Hbor") as "[_ Hbor]". done.
-      iMod (bor_sep _ _ _ (l' ↦∗: ty_own ty tid) with "LFT Hbor") as "[_ Hbor]". done.
-      iMod ("Hclose" with "Htok") as "($ & $)".
-      rewrite tctx_interp_singleton tctx_hasty_val' //. iExists _, _.
-      iFrame. iSplitR. done. rewrite -uPred.iff_refl. auto.
-    - iFrame "H↦ H† Hown".
+    iDestruct (llctx_interp_acc_noend with "HL") as "[HL HLclose]".
+    iMod (Hκ with "HE HL") as (q) "[Htok Hclose]"; first solve_ndisj.
+    wp_apply (wp_hasty with "Hp"). iIntros ([[|l|]|]) "_ Hown"; try done.
+    iMod (bor_acc_cons with "LFT Hown Htok") as "[H↦ Hclose']"; first done.
+    iDestruct "H↦" as ([|[[|l'|]|][]]) "[>H↦ Hown]"; try iDestruct "Hown" as ">[]".
+      iDestruct "Hown" as "[Hown H†]". rewrite heap_pointsto_vec_singleton -wp_fupd. wp_read.
+    iMod ("Hclose'" $! (l↦#l' ∗ freeable_sz n (ty_size ty) l' ∗ _)%I
+          with "[] [H↦ Hown H†]") as "[Hbor Htok]"; last 1 first.
+    - iMod (bor_sep with "LFT Hbor") as "[_ Hbor]"; first done.
+      iMod (bor_sep with "LFT Hbor") as "[_ Hbor]"; first done.
+      iMod ("Hclose" with "Htok") as "HL".
+      iDestruct ("HLclose" with "HL") as "$".
+      by rewrite tctx_interp_singleton tctx_hasty_val' //=.
     - iIntros "!>(?&?&?)!>". iNext. iExists _.
-      rewrite -heap_mapsto_vec_singleton. iFrame. iExists _. by iFrame.
+      rewrite -heap_pointsto_vec_singleton. iFrame. by iFrame.
+    - iFrame.
   Qed.
 
   Lemma type_deref_uniq_own {E L} κ x p e n ty C T T' :
     Closed (x :b: []) e →
-    tctx_extract_hasty E L p (&uniq{κ} own_ptr n ty) T T' →
+    tctx_extract_hasty E L p (&uniq{κ}(own_ptr n ty)) T T' →
     lctx_lft_alive E L κ →
-    (∀ (v:val), typed_body E L C ((v ◁ &uniq{κ} ty) :: T') (subst' x v e)) →
+    (∀ (v:val), typed_body E L C ((v ◁ &uniq{κ}ty) :: T') (subst' x v e)) -∗
     typed_body E L C T (let: x := !p in e).
-  Proof.
-    intros. eapply type_let; [done|by apply type_deref_uniq_own_instr|solve_typing|done].
-  Qed.
+  Proof. iIntros. iApply type_let; [by apply type_deref_uniq_own_instr|solve_typing|done]. Qed.
 
   Lemma type_deref_shr_own_instr {E L} κ p n ty :
     lctx_lft_alive E L κ →
-    typed_instruction_ty E L [p ◁ &shr{κ} own_ptr n ty] (!p) (&shr{κ} ty).
+    ⊢ typed_instruction_ty E L [p ◁ &shr{κ}(own_ptr n ty)] (!p) (&shr{κ} ty).
   Proof.
-    iIntros (Hκ) "!#". iIntros (tid qE) "#HEAP #LFT $ HE HL Hp".
+    iIntros (Hκ tid qmax) "#LFT HE $ HL Hp".
     rewrite tctx_interp_singleton.
-    iMod (Hκ with "HE HL") as (q) "[[Htok1 Htok2] Hclose]"; first set_solver.
-    wp_bind p. iApply (wp_hasty with "Hp"). iIntros (v) "_ Hown".
-    iDestruct "Hown" as (l) "[Heq #H↦]". iDestruct "Heq" as %[=->].
-    iDestruct "H↦" as (vl) "[H↦b #Hown]".
-    iMod (frac_bor_acc with "LFT H↦b Htok1") as (q''') "[>H↦ Hclose']". done.
-    iApply (wp_fupd_step _ (_∖_) with "[Hown Htok2]"); try done.
-    - iApply ("Hown" with "* [%] Htok2"). set_solver+.
-    - wp_read. iIntros "!>[#Hshr Htok2]".
+    iDestruct (llctx_interp_acc_noend with "HL") as "[HL HLclose]".
+    iMod (Hκ with "HE HL") as (q) "[[Htok1 Htok2] Hclose]"; first solve_ndisj.
+    wp_apply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hown"; try done.
+    iDestruct "Hown" as (l') "#[H↦b #Hown]".
+    iMod (frac_bor_acc with "LFT H↦b Htok1") as (q''') "[>H↦ Hclose']"; first done.
+    iApply (wp_step_fupd _ _ (_∖_) with "[Hown Htok2]"); try done.
+    - iApply ("Hown" with "[%] Htok2"); first solve_ndisj.
+    - iApply wp_fupd. wp_read. iIntros "!>[#Hshr Htok2]".
       iMod ("Hclose'" with "[H↦]") as "Htok1"; first by auto.
-      iMod ("Hclose" with "[Htok1 Htok2]") as "($ & $)"; first by iFrame.
-      rewrite tctx_interp_singleton tctx_hasty_val' //. iExists _. auto.
+      iMod ("Hclose" with "[Htok1 Htok2]") as "HL"; first by iFrame.
+      iDestruct ("HLclose" with "HL") as "$".
+      rewrite tctx_interp_singleton tctx_hasty_val' //. auto.
   Qed.
 
   Lemma type_deref_shr_own {E L} κ x p e n ty C T T' :
     Closed (x :b: []) e →
-    tctx_extract_hasty E L p (&shr{κ} own_ptr n ty) T T' →
+    tctx_extract_hasty E L p (&shr{κ}(own_ptr n ty)) T T' →
     lctx_lft_alive E L κ →
-    (∀ (v:val), typed_body E L C ((v ◁ &shr{κ} ty) :: T') (subst' x v e)) →
+    (∀ (v:val), typed_body E L C ((v ◁ &shr{κ} ty) :: T') (subst' x v e)) -∗
     typed_body E L C T (let: x := !p in e).
-  Proof.
-    intros. eapply type_let; [done|by apply type_deref_shr_own_instr|solve_typing|done].
-  Qed.
+  Proof. iIntros. iApply type_let; [by apply type_deref_shr_own_instr|solve_typing|done]. Qed.
 
   Lemma type_deref_uniq_uniq_instr {E L} κ κ' p ty :
     lctx_lft_alive E L κ → lctx_lft_incl E L κ κ' →
-    typed_instruction_ty E L [p ◁ &uniq{κ} &uniq{κ'} ty] (!p) (&uniq{κ} ty).
+    ⊢ typed_instruction_ty E L [p ◁ &uniq{κ}(&uniq{κ'}ty)] (!p) (&uniq{κ} ty).
   Proof.
-    iIntros (Hκ Hincl) "!#". iIntros (tid qE) "#HEAP #LFT $ HE HL Hp".
+    iIntros (Hκ Hincl tid qmax) "#LFT #HE $ HL Hp".
     rewrite tctx_interp_singleton.
-    iPoseProof (Hincl with "[#] [#]") as "Hincl".
-    { by iApply elctx_interp_persist. } { by iApply llctx_interp_persist. }
-    iMod (Hκ with "HE HL") as (q) "[Htok Hclose]"; first set_solver.
-    wp_bind p. iApply (wp_hasty with "Hp"). iIntros (v) "_ Hown".
-    iDestruct "Hown" as (l P) "[[Heq #HPiff] HP]". iDestruct "Heq" as %[=->].
-    iMod (bor_iff with "LFT [] HP") as "H↦". set_solver. by eauto.
-    iMod (bor_exists with "LFT H↦") as (vl) "Hbor". done.
-    iMod (bor_sep with "LFT Hbor") as "[H↦ Hbor]". done.
-    iMod (bor_exists with "LFT Hbor") as (l') "Hbor". done.
-    iMod (bor_exists with "LFT Hbor") as (P') "Hbor". done.
-    iMod (bor_sep with "LFT Hbor") as "[H Hbor]". done.
-    iMod (bor_persistent_tok with "LFT H Htok") as "[[>% #HP'iff] Htok]". done. subst.
-    iMod (bor_acc with "LFT H↦ Htok") as "[>H↦ Hclose']". done.
-    rewrite heap_mapsto_vec_singleton.
-    iApply (wp_fupd_step  _ (⊤∖↑lftN) with "[Hbor]"); try done.
-      by iApply (bor_unnest with "LFT Hbor").
-    wp_read. iIntros "!> Hbor". iFrame "#".
+    iDestruct (llctx_interp_acc_noend with "HL") as "[HL HLclose]".
+    iDestruct (Hincl with "HL HE") as "%".
+    iMod (Hκ with "HE HL") as (q) "[Htok Hclose]"; first solve_ndisj.
+    wp_apply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hown"; try done.
+    iMod (bor_exists with "LFT Hown") as (vl) "Hbor"; first done.
+    iMod (bor_sep with "LFT Hbor") as "[H↦ Hbor]"; first done.
+    destruct vl as [|[[]|][]];
+      try by iMod (bor_persistent with "LFT Hbor Htok") as "[>[] _]".
+    iMod (bor_acc with "LFT H↦ Htok") as "[>H↦ Hclose']"; first done.
+    rewrite heap_pointsto_vec_singleton.
+    iMod (bor_unnest with "LFT Hbor") as "Hbor"; [done|].
+    iApply wp_fupd. wp_read.
     iMod ("Hclose'" with "[H↦]") as "[H↦ Htok]"; first by auto.
-    iMod ("Hclose" with "Htok") as "($ & $)".
+    iMod ("Hclose" with "Htok") as "HL".
+    iDestruct ("HLclose" with "HL") as "$".
     rewrite tctx_interp_singleton tctx_hasty_val' //.
-    iExists _, _. iSplitR; first by auto.
     iApply (bor_shorten with "[] Hbor").
-    iApply (lft_incl_glb with "Hincl"). iApply lft_incl_refl.
+    iApply lft_incl_glb; first by iApply lft_incl_syn_sem. iApply lft_incl_refl.
   Qed.
 
   Lemma type_deref_uniq_uniq {E L} κ κ' x p e ty C T T' :
     Closed (x :b: []) e →
-    tctx_extract_hasty E L p (&uniq{κ} &uniq{κ'} ty) T T' →
+    tctx_extract_hasty E L p (&uniq{κ}(&uniq{κ'}ty))%T T T' →
     lctx_lft_alive E L κ → lctx_lft_incl E L κ κ' →
-    (∀ (v:val), typed_body E L C ((v ◁ &uniq{κ} ty) :: T') (subst' x v e)) →
+    (∀ (v:val), typed_body E L C ((v ◁ &uniq{κ}ty) :: T') (subst' x v e)) -∗
     typed_body E L C T (let: x := !p in e).
-  Proof.
-    intros. eapply type_let; [done|by apply type_deref_uniq_uniq_instr|solve_typing|done].
-  Qed.
+  Proof. iIntros. iApply type_let; [by apply type_deref_uniq_uniq_instr|solve_typing|done]. Qed.
 
   Lemma type_deref_shr_uniq_instr {E L} κ κ' p ty :
     lctx_lft_alive E L κ → lctx_lft_incl E L κ κ' →
-    typed_instruction_ty E L [p ◁ &shr{κ} &uniq{κ'} ty] (!p) (&shr{κ} ty).
+    ⊢ typed_instruction_ty E L [p ◁ &shr{κ}(&uniq{κ'}ty)] (!p) (&shr{κ}ty).
   Proof.
-    iIntros (Hκ Hincl) "!# * #HEAP #LFT $ HE HL Hp". rewrite tctx_interp_singleton.
-    iPoseProof (Hincl with "[#] [#]") as "Hincl".
-    { by iApply elctx_interp_persist. } { by iApply llctx_interp_persist. }
-    iMod (Hκ with "HE HL") as (q) "[[Htok1 Htok2] Hclose]"; first set_solver.
-    wp_bind p. iApply (wp_hasty with "Hp"). iIntros (v) "_ Hown".
-    iDestruct "Hown" as (l) "[Heq Hshr]".
-    iDestruct "Heq" as %[=->]. iDestruct "Hshr" as (l') "[H↦ Hown]".
-    iMod (frac_bor_acc with "LFT H↦ Htok1") as (q'') "[>H↦ Hclose']". done.
-    iAssert (κ ⊑ κ' ∪ κ)%I as "#Hincl'".
-    { iApply (lft_incl_glb with "Hincl []"). iApply lft_incl_refl. }
-    iMod (lft_incl_acc with "Hincl' Htok2") as (q2) "[Htok2 Hclose'']". solve_ndisj.
-    iApply (wp_fupd_step _ (_∖_) with "[Hown Htok2]"); try done.
-    - iApply ("Hown" with "* [%] Htok2"). set_solver+.
-    - wp_read. iIntros "!>[#Hshr Htok2]". iMod ("Hclose''" with "Htok2") as "Htok2".
-      iMod ("Hclose'" with "[H↦]") as "Htok1"; first by auto.
-      iMod ("Hclose" with "[Htok1 Htok2]") as "($ & $)"; first by iFrame.
-      rewrite tctx_interp_singleton tctx_hasty_val' //.
-      iExists _. iSplitR. done. by iApply (ty_shr_mono with "LFT Hincl' Hshr").
+    iIntros (Hκ Hincl tid qmax) "#LFT HE $ HL Hp". rewrite tctx_interp_singleton.
+    iDestruct (llctx_interp_acc_noend with "HL") as "[HL HLclose]".
+    iDestruct (Hincl with "HL HE") as "%".
+    iMod (Hκ with "HE HL") as (q) "[[Htok1 Htok2] Hclose]"; first solve_ndisj.
+    wp_apply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hshr"; try done.
+    iDestruct "Hshr" as (l') "[H↦ Hown]".
+    iMod (frac_bor_acc with "LFT H↦ Htok1") as (q'') "[>H↦ Hclose']"; first done.
+    iAssert (κ ⊑ κ' ⊓ κ)%I as "#Hincl'".
+    { iApply lft_incl_glb.
+      + by iApply lft_incl_syn_sem.
+      + by iApply lft_incl_refl. }
+    iMod (lft_incl_acc with "Hincl' Htok2") as (q2) "[Htok2 Hclose'']"; first solve_ndisj.
+    iApply (wp_step_fupd _ _ (_∖_) with "[Hown Htok2]"); try done.
+    { iApply ("Hown" with "[%] Htok2"); first solve_ndisj. }
+    iApply wp_fupd. wp_read. iIntros "!>[#Hshr Htok2]".
+    iMod ("Hclose''" with "Htok2") as "Htok2".
+    iMod ("Hclose'" with "[H↦]") as "Htok1"; first by auto.
+    iMod ("Hclose" with "[Htok1 Htok2]") as "HL"; first by iFrame.
+    iDestruct ("HLclose" with "HL") as "$".
+    rewrite tctx_interp_singleton tctx_hasty_val' //.
+    by iApply (ty_shr_mono with "Hincl' Hshr").
   Qed.
 
   Lemma type_deref_shr_uniq {E L} κ κ' x p e ty C T T' :
     Closed (x :b: []) e →
-    tctx_extract_hasty E L p (&shr{κ} &uniq{κ'} ty) T T' →
+    tctx_extract_hasty E L p (&shr{κ}(&uniq{κ'}ty))%T T T' →
     lctx_lft_alive E L κ → lctx_lft_incl E L κ κ' →
-    (∀ (v:val), typed_body E L C ((v ◁ &shr{κ} ty) :: T') (subst' x v e)) →
+    (∀ (v:val), typed_body E L C ((v ◁ &shr{κ}ty) :: T') (subst' x v e)) -∗
     typed_body E L C T (let: x := !p in e).
-  Proof.
-    intros. eapply type_let; [done|by apply type_deref_shr_uniq_instr|solve_typing|done].
-  Qed.
+  Proof. iIntros. iApply type_let; [by apply type_deref_shr_uniq_instr|solve_typing|done]. Qed.
 End borrow.
 
-Hint Resolve tctx_extract_hasty_borrow tctx_extract_hasty_borrow_share
+Global Hint Resolve tctx_extract_hasty_borrow tctx_extract_hasty_borrow_share
                | 10 : lrust_typing.
+Global Hint Resolve tctx_extract_hasty_share | 10 : lrust_typing.
+Global Hint Resolve tctx_extract_hasty_share_samelft | 9 : lrust_typing.

lambda-rust/typing/cont.v

+From iris.proofmode Require Import proofmode.
+From lrust.typing Require Export type.
+From lrust.typing Require Import programs.
+From iris.prelude Require Import options.
+
+Section typing.
+  Context `{!typeGS Σ}.
+
+  (** Jumping to and defining a continuation. *)
+  Lemma type_jump args argsv E L C T k T' :
+    (* We use this rather complicated way to state that
+         args = of_val <$> argsv, only because then solve_typing
+         is able to prove it easily. *)
+    Forall2 (λ a av, to_val a = Some av ∨ a = of_val av) args argsv →
+    k ◁cont(L, T') ∈ C →
+    tctx_incl E L T (T' (list_to_vec argsv)) →
+    ⊢ typed_body E L C T (k args).
+  Proof.
+    iIntros (Hargs HC Hincl tid qmax) "#LFT #HE Hna HL HC HT".
+    iDestruct (llctx_interp_acc_noend with "HL") as "[HL HLclose]".
+    iMod (Hincl with "LFT HE HL HT") as "(HL & HT)".
+    iSpecialize ("HC" with "[]"); first done.
+    iDestruct ("HLclose" with "HL") as "HL".
+    assert (args = of_val <$> argsv) as ->.
+    { clear -Hargs. induction Hargs as [|a av ?? [<-%of_to_val| ->] _ ->]=>//=. }
+    rewrite -{3}(vec_to_list_to_vec argsv). iApply ("HC" with "Hna HL HT").
+  Qed.
+
+  Lemma type_cont argsb L1 (T' : vec val (length argsb) → _) E L2 C T econt e2 kb :
+    Closed (kb :b: argsb +b+ []) econt → Closed (kb :b: []) e2 →
+    (∀ k, typed_body E L2 (k ◁cont(L1, T') :: C) T (subst' kb k e2)) -∗
+    □ (∀ k (args : vec val (length argsb)),
+          typed_body E L1 (k ◁cont(L1, T') :: C) (T' args)
+                     (subst_v (kb::argsb) (k:::args) econt)) -∗
+    typed_body E L2 C T (letcont: kb argsb := econt in e2).
+  Proof.
+    iIntros (Hc1 Hc2) "He2 #Hecont". iIntros (tid qmax) "#LFT #HE Htl HL HC HT".
+    rewrite (_ : (rec: kb argsb := econt)%E = of_val (rec: kb argsb := econt)%V); last by unlock.
+    wp_let. iApply ("He2" with "LFT HE Htl HL [HC] HT").
+    iLöb as "IH". iIntros (x) "H".
+    iDestruct "H" as %[->|?]%elem_of_cons; last by iApply "HC".
+    iIntros (args) "Htl HL HT". wp_rec.
+    iApply ("Hecont" with "LFT HE Htl HL [HC] HT"). by iApply "IH".
+  Qed.
+
+  Lemma type_cont_norec argsb L1 (T' : vec val (length argsb) → _) E L2 C T econt e2 kb :
+    Closed (kb :b: argsb +b+ []) econt → Closed (kb :b: []) e2 →
+    (∀ k, typed_body E L2 (k ◁cont(L1, T') :: C) T (subst' kb k e2)) -∗
+    (∀ k (args : vec val (length argsb)),
+          typed_body E L1 C (T' args) (subst_v (kb :: argsb) (k:::args) econt)) -∗
+    typed_body E L2 C T (letcont: kb argsb := econt in e2).
+  Proof.
+    iIntros (Hc1 Hc2) "He2 Hecont". iIntros (tid qmax) "#LFT #HE Htl HL HC HT".
+    rewrite (_ : (rec: kb argsb := econt)%E = of_val (rec: kb argsb := econt)%V); last by unlock.
+    wp_let. iApply ("He2" with "LFT HE Htl HL [HC Hecont] HT").
+    iIntros (x) "H".
+    iDestruct "H" as %[->|?]%elem_of_cons; last by iApply "HC".
+    iIntros (args) "Htl HL HT". wp_rec.
+    iApply ("Hecont" with "LFT HE Htl HL HC HT").
+  Qed.
+End typing.

theories/typing/cont_context.v → lambda-rust/typing/cont_context.v

-From iris.proofmode Require Import tactics.
-From iris.base_logic Require Import big_op.
+From iris.proofmode Require Import proofmode.
 From lrust.lang Require Import notation.
 From lrust.typing Require Import type lft_contexts type_context.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
 
 Section cont_context_def.
-  Context `{typeG Σ}.
+  Context `{!typeGS Σ}.
 
   Definition cont_postcondition : iProp Σ := True%I.
 
@@ -17,35 +16,25 @@ Add Printing Constructor cctx_elt.
 
 Notation cctx := (list cctx_elt).
 
-Delimit Scope lrust_cctx_scope with CC.
-Bind Scope lrust_cctx_scope with cctx_elt.
-
-Notation "k ◁cont( L , T )" := (CCtx_iscont k L _ T%TC)
-  (at level 70, format "k  ◁cont( L ,  T )") : lrust_cctx_scope.
-Notation "a :: b" := (@cons cctx_elt a%CC b%CC)
-  (at level 60, right associativity) : lrust_cctx_scope.
-Notation "[ x1 ; x2 ; .. ; xn ]" :=
-  (@cons cctx_elt x1%CC (@cons cctx_elt x2%CC
-        (..(@cons cctx_elt xn%CC (@nil cctx_elt))..))) : lrust_cctx_scope.
-Notation "[ x ]" := (@cons cctx_elt x%CC (@nil cctx_elt)) : lrust_cctx_scope.
+Notation "k ◁cont( L , T )" := (CCtx_iscont k L _ T)
+  (at level 70, format "k  ◁cont( L ,  T )").
 
 Section cont_context.
-  Context `{typeG Σ}.
+  Context `{!typeGS Σ}.
 
-  Definition cctx_elt_interp (tid : thread_id) (x : cctx_elt) : iProp Σ :=
-    let '(k ◁cont(L, T))%CC := x in
-    (∀ args, na_own tid ⊤ -∗ llctx_interp L 1 -∗ tctx_interp tid (T args) -∗
+  Definition cctx_elt_interp (tid : thread_id) (qmax: Qp) (x : cctx_elt) : iProp Σ :=
+    let '(k ◁cont(L, T)) := x in
+    (∀ args, na_own tid top -∗ llctx_interp qmax L -∗ tctx_interp tid (T args) -∗
          WP k (of_val <$> (args : list _)) {{ _, cont_postcondition }})%I.
-  Definition cctx_interp (tid : thread_id) (C : cctx) : iProp Σ :=
-    (∀ (x : cctx_elt), ⌜x ∈ C⌝ -∗ cctx_elt_interp tid x)%I.
-  Global Arguments cctx_interp _ _%CC.
+  Definition cctx_interp (tid : thread_id) (qmax: Qp) (C : cctx) : iProp Σ :=
+    (∀ (x : cctx_elt), ⌜x ∈ C⌝ -∗ cctx_elt_interp tid qmax x)%I.
 
-  Global Instance cctx_interp_permut tid:
-    Proper ((≡ₚ) ==> (⊣⊢)) (cctx_interp tid).
+  Global Instance cctx_interp_permut tid qmax :
+    Proper ((≡ₚ) ==> (⊣⊢)) (cctx_interp tid qmax).
   Proof. solve_proper. Qed.
 
-  Lemma cctx_interp_cons tid x T :
-    cctx_interp tid (x :: T) ≡ (cctx_elt_interp tid x ∧ cctx_interp tid T)%I.
+  Lemma cctx_interp_cons tid qmax x T :
+    cctx_interp tid qmax (x :: T) ≡ (cctx_elt_interp tid qmax x ∧ cctx_interp tid qmax T)%I.
   Proof.
     iSplit.
     - iIntros "H". iSplit; [|iIntros (??)]; iApply "H"; rewrite elem_of_cons; auto.
@@ -54,78 +43,77 @@ Section cont_context.
       + iDestruct "H" as "[_ H]". by iApply "H".
   Qed.
 
-  Lemma cctx_interp_nil tid : cctx_interp tid [] ≡ True%I.
+  Lemma cctx_interp_nil tid qmax : cctx_interp tid qmax [] ≡ True%I.
   Proof. iSplit; first by auto. iIntros "_". iIntros (? Hin). inversion Hin. Qed.
 
-  Lemma cctx_interp_app tid T1 T2 :
-    cctx_interp tid (T1 ++ T2) ≡ (cctx_interp tid T1 ∧ cctx_interp tid T2)%I.
+  Lemma cctx_interp_app tid qmax T1 T2 :
+    cctx_interp tid qmax (T1 ++ T2) ≡ (cctx_interp tid qmax T1 ∧ cctx_interp tid qmax T2)%I.
   Proof.
     induction T1 as [|?? IH]; first by rewrite /= cctx_interp_nil left_id.
     by rewrite /= !cctx_interp_cons IH assoc.
   Qed.
 
-  Lemma cctx_interp_singleton tid x :
-    cctx_interp tid [x] ≡ cctx_elt_interp tid x.
+  Lemma cctx_interp_singleton tid qmax x :
+    cctx_interp tid qmax [x] ≡ cctx_elt_interp tid qmax x.
   Proof. rewrite cctx_interp_cons cctx_interp_nil right_id //. Qed.
 
-  Lemma fupd_cctx_interp tid C :
-    (|={⊤}=> cctx_interp tid C) -∗ cctx_interp tid C.
+  Lemma fupd_cctx_interp tid qmax C :
+    (|={⊤}=> cctx_interp tid qmax C) -∗ cctx_interp tid qmax C.
   Proof.
     rewrite /cctx_interp. iIntros "H". iIntros ([k L n T]) "%".
     iIntros (args) "HL HT". iMod "H".
-    by iApply ("H" $! (k ◁cont(L, T)%CC) with "[%] * HL HT").
+    by iApply ("H" $! (k ◁cont(L, T)) with "[%] HL HT").
   Qed.
 
   Definition cctx_incl (E : elctx) (C1 C2 : cctx): Prop :=
-    ∀ tid q, lft_ctx -∗ (elctx_interp E q -∗ cctx_interp tid C1) -∗
-                       (elctx_interp E q -∗ cctx_interp tid C2).
-  Global Arguments cctx_incl _%EL _%CC _%CC.
+    ∀ tid qmax, lft_ctx -∗ elctx_interp E -∗ cctx_interp tid qmax C1 -∗ cctx_interp tid qmax C2.
 
   Global Instance cctx_incl_preorder E : PreOrder (cctx_incl E).
   Proof.
     split.
-    - iIntros (???) "_ $".
-    - iIntros (??? H1 H2 ??) "#LFT HE".
-      iApply (H2 with "LFT"). by iApply (H1 with "LFT").
+    - iIntros (???) "_ _ $".
+    - iIntros (??? H1 H2 ??) "#LFT #HE HC".
+      iApply (H2 with "LFT HE"). by iApply (H1 with "LFT HE").
   Qed.
 
   Lemma incl_cctx_incl E C1 C2 : C1 ⊆ C2 → cctx_incl E C2 C1.
   Proof.
-    rewrite /cctx_incl /cctx_interp. iIntros (HC1C2 tid ?) "_ H HE * %".
-    iApply ("H" with "HE * [%]"). by apply HC1C2.
+    rewrite /cctx_incl /cctx_interp. iIntros (HC1C2 tid ?) "_ #HE H * %".
+    iApply ("H" with "[%]"). by apply HC1C2.
   Qed.
 
-  Lemma cctx_incl_cons_match E k L n (T1 T2 : vec val n → tctx) C1 C2 :
+  Lemma cctx_incl_cons E k L n (T1 T2 : vec val n → tctx) C1 C2 :
     cctx_incl E C1 C2 → (∀ args, tctx_incl E L (T2 args) (T1 args)) →
     cctx_incl E (k ◁cont(L, T1) :: C1) (k ◁cont(L, T2) :: C2).
   Proof.
-    iIntros (HC1C2 HT1T2 ??) "#LFT H HE". rewrite /cctx_interp.
+    iIntros (HC1C2 HT1T2 ??) "#LFT #HE H". rewrite /cctx_interp.
     iIntros (x) "Hin". iDestruct "Hin" as %[->|Hin]%elem_of_cons.
     - iIntros (args) "Htl HL HT".
-      iMod (HT1T2 with "LFT HE HL HT") as "(HE & HL & HT)".
-      iSpecialize ("H" with "HE").
-      iApply ("H" $! (_ ◁cont(_, _))%CC with "[%] * Htl HL HT").
+      iDestruct (llctx_interp_acc_noend with "HL") as "[HL HLclose]".
+      iMod (HT1T2 with "LFT HE HL HT") as "(HL & HT)".
+      iDestruct ("HLclose" with "HL") as "HL".
+      iApply ("H" $! (_ ◁cont(_, _)) with "[%] Htl HL HT").
       constructor.
-    - iApply (HC1C2 with "LFT [H] HE * [%]"); last done.
-      iIntros "HE". iIntros (x') "%".
-      iApply ("H" with "HE * [%]"). by apply elem_of_cons; auto.
+    - iApply (HC1C2 with "LFT HE [H] [%]"); last done.
+      iIntros (x') "%". iApply ("H" with "[%]"). by apply elem_of_cons; auto.
   Qed.
 
   Lemma cctx_incl_nil E C : cctx_incl E C [].
   Proof. apply incl_cctx_incl. by set_unfold. Qed.
 
-  Lemma cctx_incl_cons E k L n (T1 T2 : vec val n → tctx) C1 C2 :
-    (k ◁cont(L, T1))%CC ∈ C1 →
+  (* Extra strong cctx inclusion rule that we do not have on paper. *)
+  Lemma cctx_incl_cons_dup E k L n (T1 T2 : vec val n → tctx) C1 C2 :
+    k ◁cont(L, T1) ∈ C1 →
     (∀ args, tctx_incl E L (T2 args) (T1 args)) →
     cctx_incl E C1 C2 →
     cctx_incl E C1 (k ◁cont(L, T2) :: C2).
   Proof.
-    intros Hin ??. rewrite <-cctx_incl_cons_match; try done.
-    iIntros (??) "_ HC HE". iSpecialize ("HC" with "HE").
+    intros Hin ??. rewrite <-cctx_incl_cons; try done.
+    clear -Hin. iIntros (??) "_ #HE HC".
     rewrite cctx_interp_cons. iSplit; last done. clear -Hin.
     iInduction Hin as [] "IH"; rewrite cctx_interp_cons;
       [iDestruct "HC" as "[$ _]" | iApply "IH"; iDestruct "HC" as "[_ $]"].
   Qed.
 End cont_context.
 
-Hint Resolve cctx_incl_nil cctx_incl_cons : lrust_typing.
+Global Hint Resolve cctx_incl_nil cctx_incl_cons : lrust_typing.

lambda-rust/typing/examples/fixpoint.v

+From iris.proofmode Require Import proofmode.
+From lrust.typing Require Import typing.
+From iris.prelude Require Import options.
+
+Section fixpoint.
+  Context `{!typeGS Σ}.
+
+  Local Definition my_list_pre l : type := sum [ unit; box l].
+
+  Local Instance my_list_contractive : TypeContractive my_list_pre.
+  Proof.
+    (* FIXME: solve_type_proper should handle this. *)
+    intros n l1 l2 Hl. rewrite /my_list_pre.
+    f_equiv. constructor; last constructor; last by constructor.
+    - done.
+    - f_equiv. done.
+  Qed.
+
+  Definition my_list := type_fixpoint my_list_pre.
+
+  Local Lemma my_list_unfold :
+    my_list ≡ my_list_pre my_list.
+  Proof. apply type_fixpoint_unfold. Qed.
+
+  Lemma my_list_size : my_list.(ty_size) = 2%nat.
+  Proof. rewrite my_list_unfold. done. Qed.
+End fixpoint.

lambda-rust/typing/examples/get_x.v

+From iris.proofmode Require Import proofmode.
+From lrust.typing Require Import typing.
+From iris.prelude Require Import options.
+
+Section get_x.
+  Context `{!typeGS Σ}.
+
+  Definition get_x : val :=
+    fn: ["p"] :=
+       let: "p'" := !"p" in
+       letalloc: "r" <- "p'" +ₗ #0 in
+       delete [ #1; "p"] ;; return: ["r"].
+
+  Lemma get_x_type :
+    typed_val get_x (fn(∀ α, ∅; &uniq{α}(Π[int; int])) → &shr{α}int).
+  Proof.
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>". iIntros (α ϝ ret p).
+    inv_vec p=>p. simpl_subst.
+    iApply type_deref; [solve_typing..|]. iIntros (p'); simpl_subst.
+    iApply (type_letalloc_1 (&shr{α}int)); [solve_typing..|]. iIntros (r). simpl_subst.
+    iApply type_delete; [solve_typing..|].
+    iApply type_jump; solve_typing.
+  Qed.
+End get_x.

lambda-rust/typing/examples/init_prod.v

+From iris.proofmode Require Import proofmode.
+From lrust.typing Require Import typing.
+From iris.prelude Require Import options.
+
+Section init_prod.
+  Context `{!typeGS Σ}.
+
+  Definition init_prod : val :=
+    fn: ["x"; "y"] :=
+       let: "x'" := !"x" in let: "y'" := !"y" in
+       let: "r" := new [ #2] in
+       "r" +ₗ #0 <- "x'";; "r" +ₗ #1 <- "y'";;
+       delete [ #1; "x"] ;; delete [ #1; "y"] ;; return: ["r"].
+
+  Lemma init_prod_type : typed_val init_prod (fn(∅; int, int) → Π[int;int]).
+  Proof.
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
+      iIntros ([] ϝ ret p). inv_vec p=>x y. simpl_subst.
+    iApply type_deref; [solve_typing..|]. iIntros (x'). simpl_subst.
+    iApply type_deref; [solve_typing..|]. iIntros (y'). simpl_subst.
+    iApply (type_new_subtype (Π[uninit 1; uninit 1])); [solve_typing..|].
+      iIntros (r). simpl_subst. unfold Z.to_nat, Pos.to_nat; simpl.
+    iApply (type_assign (own_ptr 2 (uninit 1))); [solve_typing..|].
+    iApply type_assign; [solve_typing..|].
+    iApply type_delete; [solve_typing..|].
+    iApply type_delete; [solve_typing..|].
+    iApply type_jump; solve_typing.
+  Qed.
+End init_prod.

lambda-rust/typing/examples/lazy_lft.v

+From iris.proofmode Require Import proofmode.
+From lrust.typing Require Import typing.
+From iris.prelude Require Import options.
+
+Section lazy_lft.
+  Context `{!typeGS Σ}.
+
+  Definition lazy_lft : val :=
+    fn: [] :=
+      Newlft;;
+      let: "t" := new [ #2] in let: "f" := new [ #1] in let: "g" := new [ #1] in
+      let: "42" := #42 in "f" <- "42";;
+      "t" +ₗ #0 <- "f";; "t" +ₗ #1 <- "f";;
+      let: "t0'" := !("t" +ₗ #0) in "t0'";;
+      let: "23" := #23 in "g" <- "23";;
+      "t" +ₗ #1 <- "g";;
+      let: "r" := new [ #0] in
+      Endlft;; delete [ #2; "t"];; delete [ #1; "f"];; delete [ #1; "g"];; return: ["r"].
+
+  Lemma lazy_lft_type : typed_val lazy_lft (fn(∅) → unit).
+  Proof.
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
+      iIntros ([] ϝ ret p). inv_vec p. simpl_subst.
+    iApply (type_newlft []). iIntros (α).
+    iApply (type_new_subtype (Π[uninit 1;uninit 1])); [solve_typing..|].
+      iIntros (t). simpl_subst.
+    iApply type_new; [solve_typing..|]. iIntros (f). simpl_subst.
+    iApply type_new; [solve_typing..|]. iIntros (g). simpl_subst.
+    iApply type_int. iIntros (v42). simpl_subst.
+    iApply type_assign; [solve_typing..|].
+    iApply (type_assign _ (&shr{α}_)); [solve_typing..|].
+    iApply type_assign; [solve_typing..|].
+    iApply type_deref; [solve_typing..|]. iIntros (t0'). simpl_subst.
+    iApply type_letpath; [solve_typing|]. iIntros (dummy). simpl_subst.
+    iApply type_int. iIntros (v23). simpl_subst.
+    iApply type_assign; [solve_typing..|].
+    iApply (type_assign _ (&shr{α}int)); [solve_typing..|].
+    iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
+    iApply type_endlft; [solve_typing..|].
+    iApply (type_delete (Π[&shr{α}_;&shr{α}_])%T); [solve_typing..|].
+    iApply type_delete; [solve_typing..|].
+    iApply type_delete; [solve_typing..|].
+    iApply type_jump; solve_typing.
+  Qed.
+End lazy_lft.