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.
+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].
-Opaque memcpy.
 
-Notation "e1 <-{ n } ! e2" := (App memcpy [e1%E ; Lit (LitInt n) ; e2%E])
+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.
 
-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") : lrust_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 }}}
+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 }}}.
+  {{{ 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.

lambda-rust/lang/lib/new_delete.v

+From lrust.lang Require Export notation.
+From lrust.lang Require Import heap proofmode memcpy.
+From iris.prelude Require Import options.
+
+Definition new : val :=
+  λ: ["n"],
+    if: "n" ≤ #0 then #((42%positive, 1337):loc)
+    else Alloc "n".
+
+Definition delete : val :=
+  λ: ["n"; "loc"],
+    if: "n" ≤ #0 then #☠
+    else Free "n" "loc".
+
+Section specs.
+  Context `{!lrustGS Σ}.
+
+  Lemma wp_new E n:
+    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 (? Φ) "_ 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 :
+    n = length vl →
+    {{{ l ↦∗ vl ∗ (†l…(length vl) ∨ ⌜n = 0⌝) }}}
+      delete [ #n; #l] @ E
+    {{{ RET #☠; True }}}.
+  Proof.
+    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 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.

lambda-rust/lang/notation.v

+From lrust.lang Require Export lang.
+From iris.prelude Require Import options.
+
+Coercion LitInt : Z >-> base_lit.
+Coercion LitLoc : loc >-> base_lit.
+
+Coercion App : expr >-> Funclass.
+Coercion of_val : val >-> expr.
+
+Coercion Var : string >-> expr.
+
+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
+        (..(@cons expr xn%E (@nil expr))..))) : expr_scope.
+
+(* No scope for the values, does not conflict and scope is often not inferred
+properly. *)
+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 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)
+  (at level 50, left associativity) : expr_scope.
+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%binder xl%binder e%E)
+  (at level 102, f, xl at level 1, e at level 200) : expr_scope.
+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.
+
+(** Derived notions. The notations for let and seq are stated
+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%binder e%E)
+  (at level 102, xl at level 1, e at level 200) : expr_scope.
+Notation "λ: xl , e" := (locked (LamV xl%binder e%E))
+  (at level 102, 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%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 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%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 200, format "e1  ;;  e2") : val_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 (λ: ["_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" :=
+  (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.
+
+(* 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, 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/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.
+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
-expressions into this type we can implementation substitution, closedness
+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)
@@ -24,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)
@@ -65,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
@@ -84,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]
@@ -96,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
@@ -104,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 =>
@@ -135,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 =>
@@ -150,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.
 
@@ -172,51 +175,69 @@ 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 :=
-  simpl;
+  unfold subst_v; simpl;
   repeat match goal with
   | |- context [subst ?x ?er ?e] =>
       let er' := W.of_expr er in let e' := W.of_expr e in
       change (subst x er e) with (subst x (W.to_expr er') (W.to_expr e'));
       rewrite <-(W.to_expr_subst x); simpl (* ssr rewrite is slower *)
   end;
-  unfold W.to_expr.
-Arguments W.to_expr : simpl never.
-Arguments subst : simpl never.
+  unfold W.to_expr; simpl.
+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
@@ -224,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
@@ -239,7 +260,7 @@ Ltac reshape_val e tac :=
   | of_val ?v => v
   | Lit ?l => constr:(LitV l)
   | Rec ?f ?xl ?e => constr:(RecV f xl e)
-  end in let v := go e in first [tac v | fail 2].
+  end in let v := go e in tac v.
 
 Ltac reshape_expr e tac :=
   let rec go_fun K f vs es :=
@@ -249,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
@@ -269,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.

lambda-rust/typing/bool.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 bool.
+  Context `{!typeGS Σ}.
+
+  Program Definition bool : type :=
+    {| 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. done. Qed.
+End bool.
+
+Section typing.
+  Context `{!typeGS Σ}.
+
+  Lemma type_bool_instr (b : Datatypes.bool) : typed_val #b bool.
+  Proof.
+    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)) -∗
+    typed_body E L C T (let: x := #b in e).
+  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 ∈ 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 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 ([[| |[|[]|]]|]) "_ 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.

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.

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.