.gitlab-ci.yml

@@ -5,6 +5,7 @@ stages:
 
 variables:
   CPU_CORES: "10"
+  OCAML: "ocaml-variants.4.14.0+options ocaml-option-flambda"
 
 .template: &template
   stage: build
@@ -27,21 +28,42 @@ variables:
 
 ## Build jobs
 
-build-coq.8.13.1:
+build-coq.8.20.0:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.13.1"
-    OPAM_PKG: "1"
+    OPAM_PINS: "coq version 8.20.0"
     DENY_WARNINGS: "1"
+    MANGLE_NAMES: "1"
+    # Mostly to make the lifetime logic available
+    OPAM_PKG: "1"
   tags:
   - fp-timing
 
-build-iris.dev:
+trigger-iris.timing:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.13.dev   coq-stdpp.dev git git+https://gitlab.mpi-sws.org/iris/stdpp.git#$STDPP_REV   coq-iris.dev git git+https://gitlab.mpi-sws.org/iris/iris.git#$IRIS_REV"
-  except:
+    OPAM_PINS: "coq version 8.20.0   git+https://gitlab.mpi-sws.org/$IRIS_REPO#$IRIS_REV"
+  tags:
+  - fp-timing
   only:
   - triggers
   - schedules
   - api
+  except:
+    variables:
+    - $TIMING_AD_HOC_ID == null
+
+trigger-iris.dev:
+  <<: *template
+  variables:
+    STDPP_REPO: "iris/stdpp"
+    IRIS_REPO: "iris/iris"
+    OPAM_PINS: "coq version $NIGHTLY_COQ   git+https://gitlab.mpi-sws.org/$STDPP_REPO#$STDPP_REV   git+https://gitlab.mpi-sws.org/$IRIS_REPO#$IRIS_REV"
+  except:
+  only:
+    refs:
+    - triggers
+    - schedules
+    - api
+    variables:
+    - $TIMING_AD_HOC_ID == null

Makefile.coq.local

+# Run tests interleaved with main build.  They have to be in the same target for this.
+real-all: style
+
+style: $(VFILES) coq-lint.sh
+# Make sure everything imports the options, and all Instance/Argument/Hint are qualified.
+	$(SHOW)"COQLINT"
+	$(HIDE)for FILE in $(VFILES); do \
+	  if ! grep -F -q 'From iris.prelude Require Import options.' "$$FILE"; then echo "ERROR: $$FILE does not import 'options'."; echo; exit 1; fi ; \
+	  ./coq-lint.sh "$$FILE" || exit 1; \
+	done
+.PHONY: style

Missing.md

 Missing APIs from the types we cover (APIs have been added after this formalization was done)
 
+# Mutex
+
+* Might become covariant: https://github.com/rust-lang/rust/pull/96820
+
 # Cell
 
 * Structural conversion for slices.  The matching operations in our model would be

README.md

@@ -6,7 +6,7 @@ This is the Coq development accompanying lambda-Rust.
 
 This version is known to compile with:
 
- - Coq 8.13.1
+ - Coq 8.20.0
  - A development version of [Iris](https://gitlab.mpi-sws.org/iris/iris)
 
 ## Building from source

_CoqProject

--Q theories lrust
+# Search paths for all packages. They must all match the regex
+# `-Q $PACKAGE[/ ]` so that we can filter out the right ones for each package.
+-Q lifetime lrust.lifetime
+-Q lambda-rust/lang lrust.lang
+-Q lambda-rust/typing lrust.typing
 # We sometimes want to locally override notation, and there is no good way to do that with scopes.
 -arg -w -arg -notation-overridden
 # Cannot use non-canonical projections as it causes massive unification failures
 # (https://github.com/coq/coq/issues/6294).
 -arg -w -arg -redundant-canonical-projection
+# Warning is often incorrect, see https://gitlab.mpi-sws.org/iris/stdpp/-/issues/216
+-arg -w -arg -notation-incompatible-prefix
 
-theories/lifetime/model/definitions.v
-theories/lifetime/model/faking.v
-theories/lifetime/model/creation.v
-theories/lifetime/model/primitive.v
-theories/lifetime/model/accessors.v
-theories/lifetime/model/borrow.v
-theories/lifetime/model/borrow_sep.v
-theories/lifetime/model/reborrow.v
-theories/lifetime/lifetime_sig.v
-theories/lifetime/lifetime.v
-theories/lifetime/at_borrow.v
-theories/lifetime/na_borrow.v
-theories/lifetime/frac_borrow.v
-theories/lifetime/meta.v
-theories/lang/adequacy.v
-theories/lang/heap.v
-theories/lang/lang.v
-theories/lang/lifting.v
-theories/lang/notation.v
-theories/lang/proofmode.v
-theories/lang/races.v
-theories/lang/tactics.v
-theories/lang/lib/memcpy.v
-theories/lang/lib/swap.v
-theories/lang/lib/new_delete.v
-theories/lang/lib/spawn.v
-theories/lang/lib/lock.v
-theories/lang/lib/arc.v
-theories/lang/lib/tests.v
-theories/typing/base.v
-theories/typing/type.v
-theories/typing/util.v
-theories/typing/lft_contexts.v
-theories/typing/type_context.v
-theories/typing/cont_context.v
-theories/typing/uninit.v
-theories/typing/own.v
-theories/typing/uniq_bor.v
-theories/typing/shr_bor.v
-theories/typing/product.v
-theories/typing/product_split.v
-theories/typing/sum.v
-theories/typing/bool.v
-theories/typing/int.v
-theories/typing/function.v
-theories/typing/programs.v
-theories/typing/borrow.v
-theories/typing/cont.v
-theories/typing/fixpoint.v
-theories/typing/type_sum.v
-theories/typing/typing.v
-theories/typing/soundness.v
-theories/typing/lib/panic.v
-theories/typing/lib/option.v
-theories/typing/lib/fake_shared.v
-theories/typing/lib/cell.v
-theories/typing/lib/spawn.v
-theories/typing/lib/join.v
-theories/typing/lib/take_mut.v
-theories/typing/lib/rc/rc.v
-theories/typing/lib/rc/weak.v
-theories/typing/lib/arc.v
-theories/typing/lib/swap.v
-theories/typing/lib/diverging_static.v
-theories/typing/lib/brandedvec.v
-theories/typing/lib/ghostcell.v
-theories/typing/lib/mutex/mutex.v
-theories/typing/lib/mutex/mutexguard.v
-theories/typing/lib/refcell/refcell.v
-theories/typing/lib/refcell/ref.v
-theories/typing/lib/refcell/refmut.v
-theories/typing/lib/refcell/refcell_code.v
-theories/typing/lib/refcell/ref_code.v
-theories/typing/lib/refcell/refmut_code.v
-theories/typing/lib/rwlock/rwlock.v
-theories/typing/lib/rwlock/rwlockreadguard.v
-theories/typing/lib/rwlock/rwlockwriteguard.v
-theories/typing/lib/rwlock/rwlock_code.v
-theories/typing/lib/rwlock/rwlockreadguard_code.v
-theories/typing/lib/rwlock/rwlockwriteguard_code.v
-theories/typing/examples/get_x.v
-theories/typing/examples/rebor.v
-theories/typing/examples/unbox.v
-theories/typing/examples/init_prod.v
-theories/typing/examples/lazy_lft.v
-theories/typing/examples/nonlexical.v
+lifetime/model/definitions.v
+lifetime/model/faking.v
+lifetime/model/creation.v
+lifetime/model/primitive.v
+lifetime/model/accessors.v
+lifetime/model/borrow.v
+lifetime/model/borrow_sep.v
+lifetime/model/reborrow.v
+lifetime/lifetime_sig.v
+lifetime/lifetime.v
+lifetime/at_borrow.v
+lifetime/na_borrow.v
+lifetime/frac_borrow.v
+lifetime/meta.v
+lambda-rust/lang/adequacy.v
+lambda-rust/lang/heap.v
+lambda-rust/lang/lang.v
+lambda-rust/lang/lifting.v
+lambda-rust/lang/notation.v
+lambda-rust/lang/proofmode.v
+lambda-rust/lang/races.v
+lambda-rust/lang/tactics.v
+lambda-rust/lang/lib/memcpy.v
+lambda-rust/lang/lib/swap.v
+lambda-rust/lang/lib/new_delete.v
+lambda-rust/lang/lib/spawn.v
+lambda-rust/lang/lib/lock.v
+lambda-rust/lang/lib/arc.v
+lambda-rust/lang/lib/tests.v
+lambda-rust/typing/base.v
+lambda-rust/typing/type.v
+lambda-rust/typing/util.v
+lambda-rust/typing/lft_contexts.v
+lambda-rust/typing/type_context.v
+lambda-rust/typing/cont_context.v
+lambda-rust/typing/uninit.v
+lambda-rust/typing/own.v
+lambda-rust/typing/uniq_bor.v
+lambda-rust/typing/shr_bor.v
+lambda-rust/typing/product.v
+lambda-rust/typing/product_split.v
+lambda-rust/typing/sum.v
+lambda-rust/typing/bool.v
+lambda-rust/typing/int.v
+lambda-rust/typing/function.v
+lambda-rust/typing/programs.v
+lambda-rust/typing/borrow.v
+lambda-rust/typing/cont.v
+lambda-rust/typing/fixpoint.v
+lambda-rust/typing/type_sum.v
+lambda-rust/typing/typing.v
+lambda-rust/typing/soundness.v
+lambda-rust/typing/lib/panic.v
+lambda-rust/typing/lib/option.v
+lambda-rust/typing/lib/fake_shared.v
+lambda-rust/typing/lib/cell.v
+lambda-rust/typing/lib/spawn.v
+lambda-rust/typing/lib/join.v
+lambda-rust/typing/lib/take_mut.v
+lambda-rust/typing/lib/rc/rc.v
+lambda-rust/typing/lib/rc/weak.v
+lambda-rust/typing/lib/arc.v
+lambda-rust/typing/lib/swap.v
+lambda-rust/typing/lib/diverging_static.v
+lambda-rust/typing/lib/brandedvec.v
+lambda-rust/typing/lib/ghostcell.v
+lambda-rust/typing/lib/mutex/mutex.v
+lambda-rust/typing/lib/mutex/mutexguard.v
+lambda-rust/typing/lib/refcell/refcell.v
+lambda-rust/typing/lib/refcell/ref.v
+lambda-rust/typing/lib/refcell/refmut.v
+lambda-rust/typing/lib/refcell/refcell_code.v
+lambda-rust/typing/lib/refcell/ref_code.v
+lambda-rust/typing/lib/refcell/refmut_code.v
+lambda-rust/typing/lib/rwlock/rwlock.v
+lambda-rust/typing/lib/rwlock/rwlockreadguard.v
+lambda-rust/typing/lib/rwlock/rwlockwriteguard.v
+lambda-rust/typing/lib/rwlock/rwlock_code.v
+lambda-rust/typing/lib/rwlock/rwlockreadguard_code.v
+lambda-rust/typing/lib/rwlock/rwlockwriteguard_code.v
+lambda-rust/typing/examples/fixpoint.v
+lambda-rust/typing/examples/get_x.v
+lambda-rust/typing/examples/rebor.v
+lambda-rust/typing/examples/unbox.v
+lambda-rust/typing/examples/init_prod.v
+lambda-rust/typing/examples/lazy_lft.v
+lambda-rust/typing/examples/nonlexical.v

coq-lambda-rust.opam

 opam-version: "2.0"
 maintainer: "Ralf Jung <jung@mpi-sws.org>"
 authors: "The RustBelt Team"
-license: "BSD"
+license: "BSD-3-Clause"
 homepage: "https://plv.mpi-sws.org/rustbelt/"
 bug-reports: "https://gitlab.mpi-sws.org/iris/lambda-rust/issues"
 dev-repo: "git+https://gitlab.mpi-sws.org/iris/lambda-rust.git"
@@ -13,8 +13,8 @@ the type system, and safety proof for some Rust libraries.
 """
 
 depends: [
-  "coq-iris" { (= "dev.2021-05-05.0.6f18e8cd") | (= "dev") }
+  "coq-lifetime-logic" { = version }
 ]
 
-build: [make "-j%{jobs}%"]
-install: [make "install"]
+build: ["./make-package" "lambda-rust" "-j%{jobs}%"]
+install: ["./make-package" "lambda-rust" "install"]

coq-lifetime-logic.opam

+opam-version: "2.0"
+maintainer: "Ralf Jung <jung@mpi-sws.org>"
+authors: "The RustBelt Team"
+license: "BSD-3-Clause"
+homepage: "https://plv.mpi-sws.org/rustbelt/"
+bug-reports: "https://gitlab.mpi-sws.org/iris/lambda-rust/issues"
+dev-repo: "git+https://gitlab.mpi-sws.org/iris/lambda-rust.git"
+
+synopsis: "Lifetime Logic Coq formalization"
+description: """
+The lifetime logic extends Iris with a notion of "borrowing".
+"""
+
+depends: [
+  "coq-iris" { (= "dev.2025-03-28.0.fa344cbe") | (= "dev") }
+]
+
+build: ["./make-package" "lifetime" "-j%{jobs}%"]
+install: ["./make-package" "lifetime" "install"]

coq-lint.sh

+#!/bin/bash
+set -e
+## A simple shell script checking for some common Coq issues.
+
+FILE="$1"
+
+if grep -E -n '^\s*((Existing\s+|Program\s+|Declare\s+)?Instance|Arguments|Remove|Hint\s+(Extern|Constructors|Resolve|Immediate|Mode|Opaque|Transparent|Unfold)|(Open|Close)\s+Scope|Opaque|Transparent)\b' "$FILE"; then
+    echo "ERROR: $FILE contains 'Instance'/'Arguments'/'Hint' or another side-effect without locality (see above)."
+    echo "Please add 'Global' or 'Local' as appropriate."
+    echo
+    exit 1
+fi

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

@@ -2,23 +2,23 @@ From iris.program_logic Require Export adequacy weakestpre.
 From iris.algebra Require Import auth.
 From lrust.lang Require Export heap.
 From lrust.lang Require Import proofmode notation.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
 
-Class lrustPreG Σ := HeapPreG {
-  lrust_preG_irig :> invPreG Σ;
-  lrust_preG_heap :> inG Σ (authR heapUR);
-  lrust_preG_heap_freeable :> inG Σ (authR heap_freeableUR)
+Class lrustGpreS Σ := HeapGpreS {
+  lrustGpreS_irig :: invGpreS Σ;
+  lrustGpreS_heap :: inG Σ (authR heapUR);
+  lrustGpreS_heap_freeable :: inG Σ (authR heap_freeableUR)
 }.
 
 Definition lrustΣ : gFunctors :=
   #[invΣ;
     GFunctor (constRF (authR heapUR));
     GFunctor (constRF (authR heap_freeableUR))].
-Instance subG_heapPreG {Σ} : subG lrustΣ Σ → lrustPreG Σ.
+Global Instance subG_lrustGpreS {Σ} : subG lrustΣ Σ → lrustGpreS Σ.
 Proof. solve_inG. Qed.
 
-Definition lrust_adequacy Σ `{!lrustPreG Σ} e σ φ :
-  (∀ `{!lrustG Σ}, True ⊢ WP e {{ v, ⌜φ v⌝ }}) →
+Definition lrust_adequacy Σ `{!lrustGpreS Σ} e σ φ :
+  (∀ `{!lrustGS Σ}, True ⊢ WP e {{ v, ⌜φ v⌝ }}) →
   adequate NotStuck e σ (λ v _, φ v).
 Proof.
   intros Hwp; eapply (wp_adequacy _ _); iIntros (??).
@@ -26,8 +26,8 @@ Proof.
   { apply (auth_auth_valid (to_heap _)), to_heap_valid. }
   iMod (own_alloc (● (∅ : heap_freeableUR))) as (fγ) "Hfγ";
     first by apply auth_auth_valid.
-  set (Hheap := HeapG _ _ _ vγ fγ).
+  set (Hheap := HeapGS _ _ _ vγ fγ).
   iModIntro. iExists (λ σ _, heap_ctx σ), (λ _, True%I). iSplitL.
   { iExists ∅. by iFrame. }
-  by iApply (Hwp (LRustG _ _ Hheap)).
+  by iApply (Hwp (LRustGS _ _ Hheap)).
 Qed.

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

 From iris.program_logic Require Export language ectx_language ectxi_language.
 From stdpp Require Export strings binders.
 From stdpp Require Import gmap.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
 
-Open Scope Z_scope.
+Global Open Scope Z_scope.
 
 (** Expressions and vals. *)
 Definition block : Set := positive.
@@ -12,7 +12,7 @@ Definition loc : Set := block * Z.
 Declare Scope loc_scope.
 Bind Scope loc_scope with loc.
 Delimit Scope loc_scope with L.
-Open Scope loc_scope.
+Global Open Scope loc_scope.
 
 Inductive base_lit : Set :=
 | LitPoison | LitLoc (l : loc) | LitInt (n : Z).
@@ -43,8 +43,8 @@ Inductive expr :=
 | Case (e : expr) (el : list expr)
 | Fork (e : expr).
 
-Arguments App _%E _%E.
-Arguments Case _%E _%E.
+Global Arguments App _%_E _%_E.
+Global Arguments Case _%_E _%_E.
 
 Fixpoint is_closed (X : list string) (e : expr) : bool :=
   match e with
@@ -59,9 +59,9 @@ Fixpoint is_closed (X : list string) (e : expr) : bool :=
   end.
 
 Class Closed (X : list string) (e : expr) := closed : is_closed X e.
-Instance closed_proof_irrel env e : ProofIrrel (Closed env e).
+Global Instance closed_proof_irrel env e : ProofIrrel (Closed env e).
 Proof. rewrite /Closed. apply _. Qed.
-Instance closed_decision env e : Decision (Closed env e).
+Global Instance closed_decision env e : Decision (Closed env e).
 Proof. rewrite /Closed. apply _. Qed.
 
 Inductive val :=
@@ -151,27 +151,25 @@ Fixpoint subst_l (xl : list binder) (esl : list expr) (e : expr) : option expr :
   | x::xl, es::esl => subst' x es <$> subst_l xl esl e
   | _, _ => None
   end.
-Arguments subst_l _%binder _ _%E.
+Global Arguments subst_l _%_binder _ _%_E.
 
 Definition subst_v (xl : list binder) (vsl : vec val (length xl))
                    (e : expr) : expr :=
   Vector.fold_right2 (λ b, subst' b ∘ of_val) e _ (list_to_vec xl) vsl.
-Arguments subst_v _%binder _ _%E.
+Global Arguments subst_v _%_binder _ _%_E.
 
 Lemma subst_v_eq (xl : list binder) (vsl : vec val (length xl)) e :
   Some $ subst_v xl vsl e = subst_l xl (of_val <$> vec_to_list vsl) e.
 Proof.
-  revert vsl. induction xl=>/= vsl; inv_vec vsl=>//=v vsl. by rewrite -IHxl.
+  revert vsl. induction xl as [|x xl IHxl]=>/= vsl; inv_vec vsl=>//=v vsl.
+  by rewrite -IHxl.
 Qed.
 
 (** The stepping relation *)
 (* Be careful to make sure that poison is always stuck when used for anything
    except for reading from or writing to memory! *)
-Definition Z_of_bool (b : bool) : Z :=
-  if b then 1 else 0.
-
 Definition lit_of_bool (b : bool) : base_lit :=
-  LitInt $ Z_of_bool b.
+  LitInt $ Z.b2z b.
 
 Definition shift_loc (l : loc) (z : Z) : loc := (l.1, l.2 + z).
 
@@ -234,48 +232,48 @@ Inductive bin_op_eval (σ : state) : bin_op → base_lit → base_lit → base_l
 
 Definition stuck_term := App (Lit $ LitInt 0) [].
 
-Inductive head_step : expr → state → list Empty_set → expr → state → list expr → Prop :=
+Inductive base_step : expr → state → list Empty_set → expr → state → list expr → Prop :=
 | BinOpS op l1 l2 l' σ :
     bin_op_eval σ op l1 l2 l' →
-    head_step (BinOp op (Lit l1) (Lit l2)) σ [] (Lit l') σ []
+    base_step (BinOp op (Lit l1) (Lit l2)) σ [] (Lit l') σ []
 | BetaS f xl e e' el σ:
     Forall (λ ei, is_Some (to_val ei)) el →
     Closed (f :b: xl +b+ []) e →
     subst_l (f::xl) (Rec f xl e :: el) e = Some e' →
-    head_step (App (Rec f xl e) el) σ [] e' σ []
+    base_step (App (Rec f xl e) el) σ [] e' σ []
 | ReadScS l n v σ:
     σ !! l = Some (RSt n, v) →
-    head_step (Read ScOrd (Lit $ LitLoc l)) σ [] (of_val v) σ []
+    base_step (Read ScOrd (Lit $ LitLoc l)) σ [] (of_val v) σ []
 | ReadNa1S l n v σ:
     σ !! l = Some (RSt n, v) →
-    head_step (Read Na1Ord (Lit $ LitLoc l)) σ
+    base_step (Read Na1Ord (Lit $ LitLoc l)) σ
               []
               (Read Na2Ord (Lit $ LitLoc l)) (<[l:=(RSt $ S n, v)]>σ)
               []
 | ReadNa2S l n v σ:
     σ !! l = Some (RSt $ S n, v) →
-    head_step (Read Na2Ord (Lit $ LitLoc l)) σ
+    base_step (Read Na2Ord (Lit $ LitLoc l)) σ
               []
               (of_val v) (<[l:=(RSt n, v)]>σ)
               []
 | WriteScS l e v v' σ:
     to_val e = Some v →
     σ !! l = Some (RSt 0, v') →
-    head_step (Write ScOrd (Lit $ LitLoc l) e) σ
+    base_step (Write ScOrd (Lit $ LitLoc l) e) σ
               []
               (Lit LitPoison) (<[l:=(RSt 0, v)]>σ)
               []
 | WriteNa1S l e v v' σ:
     to_val e = Some v →
     σ !! l = Some (RSt 0, v') →
-    head_step (Write Na1Ord (Lit $ LitLoc l) e) σ
+    base_step (Write Na1Ord (Lit $ LitLoc l) e) σ
               []
               (Write Na2Ord (Lit $ LitLoc l) e) (<[l:=(WSt, v')]>σ)
               []
 | WriteNa2S l e v v' σ:
     to_val e = Some v →
     σ !! l = Some (WSt, v') →
-    head_step (Write Na2Ord (Lit $ LitLoc l) e) σ
+    base_step (Write Na2Ord (Lit $ LitLoc l) e) σ
               []
               (Lit LitPoison) (<[l:=(RSt 0, v)]>σ)
               []
@@ -283,12 +281,12 @@ Inductive head_step : expr → state → list Empty_set → expr → state → l
     to_val e1 = Some $ LitV lit1 → to_val e2 = Some $ LitV lit2 →
     σ !! l = Some (RSt n, LitV litl) →
     lit_neq lit1 litl →
-    head_step (CAS (Lit $ LitLoc l) e1 e2) σ [] (Lit $ lit_of_bool false) σ  []
+    base_step (CAS (Lit $ LitLoc l) e1 e2) σ [] (Lit $ lit_of_bool false) σ  []
 | CasSucS l e1 lit1 e2 lit2 litl σ :
     to_val e1 = Some $ LitV lit1 → to_val e2 = Some $ LitV lit2 →
     σ !! l = Some (RSt 0, LitV litl) →
     lit_eq σ lit1 litl →
-    head_step (CAS (Lit $ LitLoc l) e1 e2) σ
+    base_step (CAS (Lit $ LitLoc l) e1 e2) σ
               []
               (Lit $ lit_of_bool true) (<[l:=(RSt 0, LitV lit2)]>σ)
               []
@@ -310,30 +308,30 @@ Inductive head_step : expr → state → list Empty_set → expr → state → l
     to_val e1 = Some $ LitV lit1 → to_val e2 = Some $ LitV lit2 →
     σ !! l = Some (RSt n, LitV litl) → 0 < n →
     lit_eq σ lit1 litl →
-    head_step (CAS (Lit $ LitLoc l) e1 e2) σ
+    base_step (CAS (Lit $ LitLoc l) e1 e2) σ
               []
               stuck_term σ
               []
 | AllocS n l σ :
     0 < n →
     (∀ m, σ !! (l +ₗ m) = None) →
-    head_step (Alloc $ Lit $ LitInt n) σ
+    base_step (Alloc $ Lit $ LitInt n) σ
               []
               (Lit $ LitLoc l) (init_mem l (Z.to_nat n) σ)
               []
 | FreeS n l σ :
     0 < n →
     (∀ m, is_Some (σ !! (l +ₗ m)) ↔ 0 ≤ m < n) →
-    head_step (Free (Lit $ LitInt n) (Lit $ LitLoc l)) σ
+    base_step (Free (Lit $ LitInt n) (Lit $ LitLoc l)) σ
               []
               (Lit LitPoison) (free_mem l (Z.to_nat n) σ)
               []
 | CaseS i el e σ :
     0 ≤ i →
     el !! (Z.to_nat i) = Some e →
-    head_step (Case (Lit $ LitInt i) el) σ [] e σ []
+    base_step (Case (Lit $ LitInt i) el) σ [] e σ []
 | ForkS e σ:
-    head_step (Fork e) σ [] (Lit LitPoison) σ [e].
+    base_step (Fork e) σ [] (Lit LitPoison) σ [e].
 
 (** Basic properties about the language *)
 Lemma to_of_val v : to_val (of_val v) = Some v.
@@ -346,10 +344,10 @@ Proof.
   revert v; induction e; intros v ?; simplify_option_eq; auto with f_equal.
 Qed.
 
-Instance of_val_inj : Inj (=) (=) of_val.
+Global Instance of_val_inj : Inj (=) (=) of_val.
 Proof. by intros ?? Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed.
 
-Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
+Global Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
 Proof. destruct Ki; intros ???; simplify_eq/=; auto with f_equal. Qed.
 
 Lemma fill_item_val Ki e :
@@ -357,11 +355,11 @@ Lemma fill_item_val Ki e :
 Proof. intros [v ?]. destruct Ki; simplify_option_eq; eauto. Qed.
 
 Lemma val_stuck e1 σ1 κ e2 σ2 ef :
-  head_step e1 σ1 κ e2 σ2 ef → to_val e1 = None.
+  base_step e1 σ1 κ e2 σ2 ef → to_val e1 = None.
 Proof. destruct 1; naive_solver. Qed.
 
-Lemma head_ctx_step_val Ki e σ1 κ e2 σ2 ef :
-  head_step (fill_item Ki e) σ1 κ e2 σ2 ef → is_Some (to_val e).
+Lemma base_ctx_step_val Ki e σ1 κ e2 σ2 ef :
+  base_step (fill_item Ki e) σ1 κ e2 σ2 ef → is_Some (to_val e).
 Proof.
   destruct Ki; inversion_clear 1; decompose_Forall_hyps;
     simplify_option_eq; by eauto.
@@ -372,7 +370,8 @@ Lemma list_expr_val_eq_inv vl1 vl2 e1 e2 el1 el2 :
   map of_val vl1 ++ e1 :: el1 = map of_val vl2 ++ e2 :: el2 →
   vl1 = vl2 ∧ el1 = el2.
 Proof.
-  revert vl2; induction vl1; destruct vl2; intros H1 H2; inversion 1.
+  revert vl2; induction vl1 as [|? vl1 IHvl1];
+    intros vl2; destruct vl2 as [|? vl2]; intros H1 H2; inversion 1.
   - done.
   - subst. by rewrite to_of_val in H1.
   - subst. by rewrite to_of_val in H2.
@@ -402,8 +401,8 @@ Proof. rewrite /shift_loc /=. f_equal. lia. Qed.
 Lemma shift_loc_0_nat l : l +ₗ 0%nat = l.
 Proof. destruct l as [b o]. rewrite /shift_loc /=. f_equal. lia. Qed.
 
-Instance shift_loc_inj l : Inj (=) (=) (shift_loc l).
-Proof. destruct l as [b o]; intros n n' [=?]; lia. Qed.
+Global Instance shift_loc_inj l : Inj (=) (=) (shift_loc l).
+Proof. destruct l as [b o]; intros n n' [= ?]; lia. Qed.
 
 Lemma shift_loc_block l n : (l +ₗ n).1 = l.1.
 Proof. done. Qed.
@@ -430,7 +429,7 @@ Proof.
 Qed.
 
 Definition fresh_block (σ : state) : block :=
-  let loclst : list loc := elements (dom _ σ : gset loc) in
+  let loclst : list loc := elements (dom σ : gset loc) in
   let blockset : gset block := foldr (λ l, ({[l.1]} ∪.)) ∅ loclst in
   fresh blockset.
 
@@ -447,9 +446,9 @@ Lemma alloc_fresh n σ :
   let l := (fresh_block σ, 0) in
   let init := repeat (LitV $ LitInt 0) (Z.to_nat n) in
   0 < n →
-  head_step (Alloc $ Lit $ LitInt n) σ [] (Lit $ LitLoc l) (init_mem l (Z.to_nat n) σ) [].
+  base_step (Alloc $ Lit $ LitInt n) σ [] (Lit $ LitLoc l) (init_mem l (Z.to_nat n) σ) [].
 Proof.
-  intros l init Hn. apply AllocS. auto.
+  intros l init Hn. apply AllocS; first done.
   - intros i. apply (is_fresh_block _ i).
 Qed.
 
@@ -469,11 +468,13 @@ Qed.
 (** Closed expressions *)
 Lemma is_closed_weaken X Y e : is_closed X e → X ⊆ Y → is_closed Y e.
 Proof.
-  revert e X Y. fix FIX 1; destruct e=>X Y/=; try naive_solver.
+  revert e X Y. fix FIX 1; intros e; destruct e=>X Y/=; try naive_solver.
   - naive_solver set_solver.
-  - rewrite !andb_True. intros [He Hel] HXY. split. by eauto.
+  - rewrite !andb_True. intros [He Hel] HXY. split; first by eauto.
+    rename select (list expr) into el.
     induction el=>/=; naive_solver.
-  - rewrite !andb_True. intros [He Hel] HXY. split. by eauto.
+  - rewrite !andb_True. intros [He Hel] HXY. split; first by eauto.
+    rename select (list expr) into el.
     induction el=>/=; naive_solver.
 Qed.
 
@@ -482,12 +483,16 @@ Proof. intros. by apply is_closed_weaken with [], list_subseteq_nil. Qed.
 
 Lemma is_closed_subst X e x es : is_closed X e → x ∉ X → subst x es e = e.
 Proof.
-  revert e X. fix FIX 1; destruct e=> X /=; rewrite ?bool_decide_spec ?andb_True=> He ?;
+  revert e X. fix FIX 1; intros e; destruct e=> X /=; rewrite ?bool_decide_spec ?andb_True=> He ?;
     repeat case_bool_decide; simplify_eq/=; f_equal;
     try by intuition eauto with set_solver.
-  - case He=> _. clear He. induction el=>//=. rewrite andb_True=>?.
+  - case He=> _. clear He.
+    rename select (list expr) into el.
+    induction el=>//=. rewrite andb_True=>?.
     f_equal; intuition eauto with set_solver.
-  - case He=> _. clear He. induction el=>//=. rewrite andb_True=>?.
+  - case He=> _. clear He.
+    rename select (list expr) into el.
+    induction el=>//=. rewrite andb_True=>?.
     f_equal; intuition eauto with set_solver.
 Qed.
 
@@ -503,14 +508,18 @@ Proof. intros <-%of_to_val. apply is_closed_of_val. Qed.
 Lemma subst_is_closed X x es e :
   is_closed X es → is_closed (x::X) e → is_closed X (subst x es e).
 Proof.
-  revert e X. fix FIX 1; destruct e=>X //=; repeat (case_bool_decide=>//=);
+  revert e X. fix FIX 1; intros e; destruct e=>X //=; repeat (case_bool_decide=>//=);
     try naive_solver; rewrite ?andb_True; intros.
   - set_solver.
   - eauto using is_closed_weaken with set_solver.
   - eapply is_closed_weaken; first done.
+    rename select binder into f.
+    rename select (list binder) into xl.
     destruct (decide (BNamed x = f)), (decide (BNamed x ∈ xl)); set_solver.
-  - split; first naive_solver. induction el; naive_solver.
-  - split; first naive_solver. induction el; naive_solver.
+  - split; first naive_solver.
+    rename select (list expr) into el. induction el; naive_solver.
+  - split; first naive_solver.
+    rename select (list expr) into el. induction el; naive_solver.
 Qed.
 
 Lemma subst'_is_closed X b es e :
@@ -531,16 +540,16 @@ Proof.
 Qed.
 
 (* Misc *)
-Lemma stuck_not_head_step σ e' κ σ' ef :
-  ¬head_step stuck_term σ e' κ σ' ef.
+Lemma stuck_not_base_step σ e' κ σ' ef :
+  ¬base_step stuck_term σ e' κ σ' ef.
 Proof. inversion 1. Qed.
 
 (** Equality and other typeclass stuff *)
-Instance base_lit_dec_eq : EqDecision base_lit.
+Global Instance base_lit_dec_eq : EqDecision base_lit.
 Proof. solve_decision. Defined.
-Instance bin_op_dec_eq : EqDecision bin_op.
+Global Instance bin_op_dec_eq : EqDecision bin_op.
 Proof. solve_decision. Defined.
-Instance un_op_dec_eq : EqDecision order.
+Global Instance un_op_dec_eq : EqDecision order.
 Proof. solve_decision. Defined.
 
 Fixpoint expr_beq (e : expr) (e' : expr) : bool :=
@@ -571,41 +580,41 @@ Fixpoint expr_beq (e : expr) (e' : expr) : bool :=
   end.
 Lemma expr_beq_correct (e1 e2 : expr) : expr_beq e1 e2 ↔ e1 = e2.
 Proof.
-  revert e1 e2; fix FIX 1.
+  revert e1 e2; fix FIX 1. intros e1 e2.
     destruct e1 as [| | | |? el1| | | | | |? el1|],
              e2 as [| | | |? el2| | | | | |? el2|]; simpl; try done;
   rewrite ?andb_True ?bool_decide_spec ?FIX;
   try (split; intro; [destruct_and?|split_and?]; congruence).
   - match goal with |- context [?F el1 el2] => assert (F el1 el2 ↔ el1 = el2) end.
-    { revert el2. induction el1 as [|el1h el1q]; destruct el2; try done.
+    { revert el2. induction el1 as [|el1h el1q]; intros el2; destruct el2; try done.
       specialize (FIX el1h). naive_solver. }
     clear FIX. naive_solver.
   - match goal with |- context [?F el1 el2] => assert (F el1 el2 ↔ el1 = el2) end.
-    { revert el2. induction el1 as [|el1h el1q]; destruct el2; try done.
+    { revert el2. induction el1 as [|el1h el1q]; intros el2; destruct el2; try done.
       specialize (FIX el1h). naive_solver. }
     clear FIX. naive_solver.
 Qed.
-Instance expr_dec_eq : EqDecision expr.
+Global Instance expr_dec_eq : EqDecision expr.
 Proof.
  refine (λ e1 e2, cast_if (decide (expr_beq e1 e2))); by rewrite -expr_beq_correct.
 Defined.
-Instance val_dec_eq : EqDecision val.
+Global Instance val_dec_eq : EqDecision val.
 Proof.
  refine (λ v1 v2, cast_if (decide (of_val v1 = of_val v2))); abstract naive_solver.
 Defined.
 
-Instance expr_inhabited : Inhabited expr := populate (Lit LitPoison).
-Instance val_inhabited : Inhabited val := populate (LitV LitPoison).
+Global Instance expr_inhabited : Inhabited expr := populate (Lit LitPoison).
+Global Instance val_inhabited : Inhabited val := populate (LitV LitPoison).
 
 Canonical Structure stateO := leibnizO state.
 Canonical Structure valO := leibnizO val.
 Canonical Structure exprO := leibnizO expr.
 
 (** Language *)
-Lemma lrust_lang_mixin : EctxiLanguageMixin of_val to_val fill_item head_step.
+Lemma lrust_lang_mixin : EctxiLanguageMixin of_val to_val fill_item base_step.
 Proof.
   split; apply _ || eauto using to_of_val, of_to_val,
-    val_stuck, fill_item_val, fill_item_no_val_inj, head_ctx_step_val.
+    val_stuck, fill_item_val, fill_item_no_val_inj, base_ctx_step_val.
 Qed.
 Canonical Structure lrust_ectxi_lang := EctxiLanguage lrust_lang_mixin.
 Canonical Structure lrust_ectx_lang := EctxLanguageOfEctxi lrust_ectxi_lang.
@@ -615,7 +624,7 @@ Canonical Structure lrust_lang := LanguageOfEctx lrust_ectx_lang.
 Lemma stuck_irreducible K σ : irreducible (fill K stuck_term) σ.
 Proof.
   apply: (irreducible_fill (K:=ectx_language.fill K)); first done.
-  apply prim_head_irreducible; unfold stuck_term.
+  apply prim_base_irreducible; unfold stuck_term.
   - inversion 1.
   - apply ectxi_language_sub_redexes_are_values.
     intros [] ??; simplify_eq/=; eauto; discriminate_list.

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

 From iris.base_logic.lib Require Import invariants.
 From iris.program_logic Require Import weakestpre.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.bi Require Import fractional.
 From iris.algebra Require Import excl csum frac auth numbers.
 From lrust.lang Require Import lang proofmode notation new_delete.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
 
 (* JH: while working on Arc, I think figured that the "weak count
 locking" mechanism that Rust is using and that is verified below may
@@ -99,7 +99,7 @@ Definition try_unwrap_full : val :=
     else #2.
 
 (** The CMRA we need. *)
-(* Not bundling heapG, as it may be shared with other users. *)
+(* Not bundling heapGS, as it may be shared with other users. *)
 
 (* See rc.v for understanding the structure of this CMRA.
    The only additional thing is the [optionR (exclR unitO))], used to handle
@@ -108,13 +108,13 @@ Definition arc_stR :=
   prodUR (optionUR (csumR (prodR (prodR fracR positiveR) (optionR (exclR unitO)))
                           (exclR unitO))) natUR.
 Class arcG Σ :=
-  RcG :> inG Σ (authR arc_stR).
+  RcG :: inG Σ (authR arc_stR).
 Definition arcΣ : gFunctors := #[GFunctor (authR arc_stR)].
-Instance subG_arcΣ {Σ} : subG arcΣ Σ → arcG Σ.
+Global Instance subG_arcΣ {Σ} : subG arcΣ Σ → arcG Σ.
 Proof. solve_inG. Qed.
 
 Section def.
-  Context `{!lrustG Σ, !arcG Σ} (P1 : Qp → iProp Σ) (P2 : iProp Σ) (N : namespace).
+  Context `{!lrustGS Σ, !arcG Σ} (P1 : Qp → iProp Σ) (P2 : iProp Σ) (N : namespace).
 
   Definition arc_tok γ q : iProp Σ :=
     own γ (◯ (Some $ Cinl (q, 1%positive, None), 0%nat)).
@@ -158,10 +158,10 @@ Section arc.
      this is the lifetime token), and P2 is the thing that is owned by the
      protocol when only weak references are left (in practice, P2 is the
      ownership of the underlying memory incl. deallocation). *)
-  Context `{!lrustG Σ, !arcG Σ} (P1 : Qp → iProp Σ) {HP1:Fractional P1}
+  Context `{!lrustGS Σ, !arcG Σ} (P1 : Qp → iProp Σ) {HP1:Fractional P1}
           (P2 : iProp Σ) (N : namespace).
 
-  Instance P1_AsFractional q : AsFractional (P1 q) P1 q.
+  Local Instance P1_AsFractional q : AsFractional (P1 q) P1 q.
   Proof using HP1. done. Qed.
 
   Global Instance arc_inv_ne n :
@@ -189,8 +189,8 @@ Section arc.
     iMod (own_alloc ((● (Some $ Cinl ((1/2)%Qp, xH, None), O) ⋅
                       ◯ (Some $ Cinl ((1/2)%Qp, xH, None), O))))
       as (γ) "[H● H◯]"; first by apply auth_both_valid_discrete.
-    iExists _, _. iFrame. iApply inv_alloc. iExists _. iFrame. iExists _. iFrame.
-    rewrite Qp_div_2. auto.
+    iFrame. iApply inv_alloc. iExists _. iFrame.
+    rewrite Qp.div_2. auto.
   Qed.
 
   Lemma create_weak E l :
@@ -208,12 +208,12 @@ Section arc.
                              if decide (strong = xH) then q = q' ∧ wlock = None
                              else ∃ q'', q' = (q + q'')%Qp⌝.
   Proof.
-    iIntros "H● Htok". iDestruct (own_valid_2 with "H● Htok") as
+    iIntros "H● Htok". iCombine "H● Htok" gives
         %[[Hincl%option_included _]%prod_included [Hval _]]%auth_both_valid_discrete.
     destruct st, Hincl as [[=]|(?&?&[= <-]&?&[Hincl|Hincl%csum_included])];
       simpl in *; subst.
     - setoid_subst. iExists _, _, _, _. by iSplit.
-    - destruct Hincl as [->|[(?&[[??]?]&[=<-]&->&[[[??]%frac_included%Qp_lt_sum
+    - destruct Hincl as [->|[(?&[[??]?]&[=<-]&->&[[[??]%frac_included%Qp.lt_sum
         ?%pos_included]%prod_included _]%prod_included)|(?&?&[=]&?)]]; first done.
       iExists _, _, _, _. iSplit=>//. simpl in *. destruct decide; [subst;lia|eauto].
   Qed.
@@ -275,16 +275,16 @@ Section arc.
          (op_local_update_discrete _ _ (Some (Cinl ((qq/2)%Qp, 1%positive, None))))
            =>-[/= Hqa ?]. split;[split|]=>//=; last by rewrite left_id.
         apply frac_valid. rewrite -Hq comm_L.
-        by apply Qp_add_le_mono_l, Qp_div_le. }
+        by apply Qp.add_le_mono_l, Qp.div_le. }
       iMod ("Hclose2" with "Hown") as "HP". iModIntro.
       iMod ("Hclose1" with "[Hl Hw H● HP1']") as "_".
       { iExists _. iFrame. iExists _. rewrite /= [xH ⋅ _]comm_L. iFrame.
-        rewrite [(qq / 2)%Qp ⋅ _]comm frac_op -[(_ + _)%Qp]assoc Qp_div_2 left_id_L. auto. }
+        rewrite [(qq / 2)%Qp ⋅ _]comm frac_op -[(_ + _)%Qp]assoc Qp.div_2 left_id_L. auto. }
       iModIntro. wp_case. iApply "HΦ". iFrame.
     - wp_apply (wp_cas_int_fail with "Hl"); [congruence|]. iIntros "Hl".
       iMod ("Hclose2" with "Hown") as "HP". iModIntro.
       iMod ("Hclose1" with "[-HP HΦ]") as "_".
-      { iExists _. iFrame. iExists qq. auto with iFrame. }
+      { iExists _. iFrame. iExists qq. iCombine "HP1 HP1'" as "$". auto with iFrame. }
       iModIntro. wp_case. iApply ("IH" with "HP HΦ").
   Qed.
 
@@ -314,7 +314,7 @@ Section arc.
       { by apply auth_update_alloc, prod_local_update_2,
               (op_local_update_discrete _ _ (1%nat)). }
       iMod ("Hclose1" with "[-Hown' HP HΦ]") as "_".
-      { iExists _. iFrame. iExists _.
+      { iExists _. iFrame.
         rewrite Z.add_comm -(Nat2Z.inj_add 1) /=. auto with iFrame. }
       iModIntro. wp_case. iApply "HΦ". iFrame.
     - destruct wlock.
@@ -333,7 +333,7 @@ Section arc.
   Lemma weak_tok_auth_val γ st :
     own γ (● st) -∗ weak_tok γ -∗ ⌜∃ st' weak, st = (st', S weak) ∧ ✓ st'⌝.
   Proof.
-    iIntros "H● Htok". iDestruct (own_valid_2 with "H● Htok") as
+    iIntros "H● Htok". iCombine "H● Htok" gives
         %[[Hincl%option_included Hincl'%nat_included]%prod_included [Hval _]]
          %auth_both_valid_discrete.
     destruct st as [?[]], Hincl as [_|(?&?&[=]&?)]; simpl in *; try lia. eauto.
@@ -398,7 +398,7 @@ Section arc.
     { iIntros "!> HP". iInv N as (st) "[>H● H]" "Hclose1".
       iMod ("Hacc" with "HP") as "[Hown Hclose2]".
       iDestruct (weak_tok_auth_val with "H● Hown") as %(st' & weak & -> & Hval).
-      destruct st' as [[[[??]?]| |]|]; try done; iExists _.
+      destruct st' as [[[[q' c]?]| |]|]; try done; iExists _.
       - iDestruct "H" as (q) "(>Heq & [HP1 HP1'] & >$ & ?)". iDestruct "Heq" as %Heq.
         iIntros "!>"; iSplit; iMod ("Hclose2" with "Hown") as "HP".
         + iIntros "_ Hl". iExists (q/2)%Qp. iMod (own_update with "H●") as "[H● $]".
@@ -406,12 +406,12 @@ Section arc.
             apply op_local_update_discrete=>Hv. constructor; last done.
             split; last by rewrite /= left_id; apply Hv. split=>[|//].
             apply frac_valid. rewrite /= -Heq comm_L.
-            by apply Qp_add_le_mono_l, Qp_div_le. }
-          iFrame. iApply "Hclose1". iExists _. iFrame. iExists _. iFrame.
-          rewrite /= [xH ⋅ _]comm_L frac_op [(_ + c)%Qp]comm -[(_ + _)%Qp]assoc
-                  Qp_div_2 left_id_L. auto with iFrame.
+            by apply Qp.add_le_mono_l, Qp.div_le. }
+          iFrame. iApply "Hclose1". iExists _. iFrame.
+          rewrite /= [xH ⋅ _]comm_L frac_op [(_ + q')%Qp]comm -[(_ + _)%Qp]assoc
+                  Qp.div_2 left_id_L. auto with iFrame.
         + iIntros "Hl". iFrame. iApply ("Hclose1" with "[-]"). iExists _. iFrame.
-          iExists q. auto with iFrame.
+          iExists q. iCombine "HP1 HP1'" as "$". auto with iFrame.
       - iDestruct "H" as "[>$ ?]". iIntros "!>"; iSplit; first by auto with congruence.
         iIntros "Hl". iMod ("Hclose2" with "Hown") as "$". iApply "Hclose1".
         iExists _. auto with iFrame.
@@ -521,14 +521,16 @@ Section arc.
           by apply (op_local_update _ _ (Some (Cinr (Excl ())))). }
         iMod ("Hclose" with "[H● Hs Hw]") as "_"; first by iExists _; do 2 iFrame.
         iModIntro. wp_case. iApply wp_fupd. wp_op.
-        iApply ("HΦ"). rewrite -{2}Hq''. iFrame. by iApply close_last_strong.
+        iApply ("HΦ"). rewrite -{2}Hq''. iCombine "HP1 HP1'" as "$".
+        by iApply close_last_strong.
       + destruct Hqq' as [? ->].
         rewrite -[in (_, _)](Pos.succ_pred s) // -[wl in Cinl (_, wl)]left_id
                 -Pos.add_1_l 2!pair_op Cinl_op Some_op.
         iMod (own_update_2 _ _ _ _ with "H● Hown") as "H●".
         { apply auth_update_dealloc, prod_local_update_1, @cancel_local_update_unit, _. }
         iMod ("Hclose" with "[- HΦ]") as "_".
-        { iExists _. iFrame. iExists (q + q'')%Qp. iFrame. iSplit; last by destruct s.
+        { iExists _. iCombine "HP1 HP1'" as "HP". iFrame "H●". iFrame.
+          iSplit; last by destruct s.
           iIntros "!> !%". rewrite assoc -Hq''. f_equal. apply comm, _. }
         iModIntro. wp_case. wp_op; case_bool_decide; simplify_eq. by iApply "HΦ".
     - wp_apply (wp_cas_int_fail with "Hs"); [congruence|]. iIntros "Hs".
@@ -553,7 +555,8 @@ Section arc.
         etrans; first apply: cancel_local_update_unit.
         by apply (op_local_update _ _ (Some (Cinr (Excl ())))). }
       iMod ("Hclose" with "[H● Hs Hw]") as "_"; first by iExists _; do 2 iFrame.
-      iApply ("HΦ" $! true). rewrite -{1}Hq''. iFrame. by iApply close_last_strong.
+      iApply ("HΦ" $! true). rewrite -{1}Hq''. iCombine "HP1 HP1'" as "$".
+      by iApply close_last_strong.
     - wp_apply (wp_cas_int_fail with "Hs"); [congruence|]. iIntros "Hs".
       iMod ("Hclose" with "[-Hown HP1 HΦ]") as "_"; first by iExists _; auto with iFrame.
       iApply ("HΦ" $! false). by iFrame.
@@ -585,7 +588,7 @@ Section arc.
                  (alloc_option_local_update (Excl ())). }
       iMod ("Hclose" with "[-HΦ HP1 H◯]") as "_"; first by iExists _; eauto with iFrame.
       iModIntro. wp_case. wp_bind (!ˢᶜ_)%E. iInv N as ([st ?]) "[>H● H]" "Hclose".
-      iDestruct (own_valid_2 with "H● H◯") as
+      iCombine "H● H◯" gives
         %[[[[=]|Hincl]%option_included _]%prod_included [? _]]%auth_both_valid_discrete.
       simpl in Hincl. destruct Hincl as (? & ? & [=<-] & -> & [|Hincl]); last first.
       + apply csum_included in Hincl. destruct Hincl as [->|[Hincl|(?&?&[=]&?)]]=>//.
@@ -595,9 +598,9 @@ Section arc.
         iMod ("Hclose" with "[-HΦ H◯ HP1]") as "_"; first by iExists _; auto with iFrame.
         iModIntro. wp_let. wp_op; case_bool_decide; [lia|]. wp_let. wp_op. wp_bind (_ <-ˢᶜ _)%E.
         iInv N as ([st w]) "[>H● H]" "Hclose".
-        iDestruct (own_valid_2 with "H● H◯") as
+        iCombine "H● H◯" gives
            %[[[[=]|Hincl]%option_included _]%prod_included [Hval _]]%auth_both_valid_discrete.
-        simpl in Hincl. destruct Hincl as (? & ? & [=<-] & -> & Hincl); last first.
+        simpl in Hincl. destruct Hincl as (x1 & x2 & [=<-] & -> & Hincl); last first.
         assert (∃ q p, x2 = Cinl (q, p, Excl' ())) as (? & ? & ->).
         { destruct Hincl as [|Hincl]; first by setoid_subst; eauto.
           apply csum_included in Hincl. destruct Hincl as [->|[Hincl|(?&?&[=]&?)]]=>//.
@@ -610,13 +613,13 @@ Section arc.
           csum_local_update_l, prod_local_update_2, delete_option_local_update, _. }
         iMod ("Hclose" with "[-HΦ H◯ HP1]") as "_"; first by iExists _; auto with iFrame.
         iModIntro. wp_seq. iApply "HΦ". iFrame.
-      + setoid_subst. iDestruct "H" as (?) "(Hq & ? & ? & >? & >%)". subst. wp_read.
+      + setoid_subst. iDestruct "H" as (?) "(Hq & HP1' & ? & >? & >%)". subst. wp_read.
         iMod (own_update_2 with "H● H◯") as "H●".
         { apply auth_update_dealloc. rewrite -{1}[(_, 0%nat)]right_id.
           apply cancel_local_update_unit, _. }
         iMod ("Hclose" with "[H●]") as "_"; first by iExists _; iFrame.
         iModIntro. wp_seq. wp_op. wp_let. wp_op. wp_write. iApply "HΦ".
-        iDestruct "Hq" as %<-. iFrame.
+        iDestruct "Hq" as %<-. iCombine "HP1 HP1'" as "$". iFrame.
   Qed.
 
   Lemma try_unwrap_full_spec (γ : gname) (q: Qp) (l : loc) :
@@ -666,4 +669,4 @@ Section arc.
   Qed.
 End arc.
 
-Typeclasses Opaque is_arc arc_tok weak_tok.
+Global Typeclasses Opaque is_arc arc_tok weak_tok.

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

 From iris.program_logic Require Import weakestpre.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.algebra Require Import excl.
 From lrust.lang Require Import lang proofmode notation.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
 
 Definition mklock_unlocked : val := λ: ["l"], "l" <- #false.
 Definition mklock_locked : val := λ: ["l"], "l" <- #true.
@@ -16,7 +16,7 @@ Definition release : val := λ: ["l"], "l" <-ˢᶜ #false.
    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 `{!lrustG Σ}.
+  Context `{!lrustGS Σ}.
 
   Definition lock_proto (l : loc) (R : iProp Σ) : iProp Σ :=
     (∃ b : bool, l ↦ #b ∗ if b then True else R)%I.
@@ -109,4 +109,4 @@ Section proof.
   Qed.
 End proof.
 
-Typeclasses Opaque lock_proto.
+Global Typeclasses Opaque lock_proto.

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

 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"] :=
@@ -19,7 +19,7 @@ Notation "e1 <-{ n ',Σ' i } ! e2" :=
   (at level 80, n, i at next level,
    format "e1  <-{ n ,Σ  i }  ! e2") : expr_scope.
 
-Lemma wp_memcpy `{!lrustG Σ} E l1 l2 vl1 vl2 q (n : Z):
+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
@@ -30,7 +30,7 @@ Proof.
   - 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_mapsto_vec_cons. subst n.
+    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_write. do 3 wp_op. iApply ("IH" with "[%] [%] Hl1 Hl2"); [lia..|].

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

 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"],
@@ -13,7 +13,7 @@ Definition delete : val :=
     else Free "n" "loc".
 
 Section specs.
-  Context `{!lrustG Σ}.
+  Context `{!lrustGS Σ}.
 
   Lemma wp_new E n:
     0 ≤ n →
@@ -23,8 +23,8 @@ Section specs.
   Proof.
     iIntros (? Φ) "_ HΦ". wp_lam. wp_op; case_bool_decide.
     - wp_if. assert (n = 0) as -> by lia. iApply "HΦ".
-      rewrite heap_mapsto_vec_nil. auto.
-    - wp_if. wp_alloc l as "H↦" "H†". lia. iApply "HΦ". subst sz. iFrame.
+      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 :

theories/lang/lib/spawn.v → 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 tactics.
+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.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
 
 Definition spawn : val :=
   λ: ["f"],
@@ -28,15 +28,15 @@ Definition join : val :=
       "join" ["c"].
 
 (** The CMRA & functor we need. *)
-Class spawnG Σ := SpawnG { spawn_tokG :> inG Σ (exclR unitO) }.
+Class spawnG Σ := SpawnG { spawn_tokG :: inG Σ (exclR unitO) }.
 Definition spawnΣ : gFunctors := #[GFunctor (exclR unitO)].
 
-Instance subG_spawnΣ {Σ} : subG spawnΣ Σ → spawnG Σ.
+Global Instance subG_spawnΣ {Σ} : subG spawnΣ Σ → spawnG Σ.
 Proof. solve_inG. Qed.
 
 (** Now we come to the Iris part of the proof. *)
 Section proof.
-Context `{!lrustG Σ, !spawnG Σ} (N : namespace).
+Context `{!lrustGS Σ, !spawnG Σ} (N : namespace).
 
 Definition spawn_inv (γf γj : gname) (c : loc) (Ψ : val → iProp Σ) : iProp Σ :=
   (own γf (Excl ()) ∗ own γj (Excl ()) ∨
@@ -70,7 +70,7 @@ Proof.
   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_mapsto_vec_cons heap_mapsto_vec_singleton.
+  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. }
@@ -90,7 +90,7 @@ Proof.
     auto. }
   iDestruct "Hinv" as (b) "[>Hc _]". wp_write.
   iMod ("Hclose" with "[-HΦ]").
-  - iNext. iRight. iExists true. iFrame. iExists _. iFrame.
+  - iNext. iRight. iExists true. iFrame.
   - iModIntro. wp_seq. by iApply "HΦ".
 Qed.
 
@@ -111,7 +111,7 @@ Proof.
   { iNext. iLeft. iFrame. }
   iModIntro. wp_if. wp_op. wp_read. wp_let.
   iAssert (c ↦∗ [ #true; v])%I with "[Hc Hd]" as "Hc".
-  { rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton. iFrame. }
+  { rewrite heap_pointsto_vec_cons heap_pointsto_vec_singleton. iFrame. }
   wp_free; first done. iApply "HΦ". iApply "HΨ'". done.
 Qed.
 
@@ -125,4 +125,4 @@ Qed.
 
 End proof.
 
-Typeclasses Opaque finish_handle join_handle.
+Global Typeclasses Opaque finish_handle join_handle.

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

 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 swap : val :=
   rec: "swap" ["p1";"p2";"len"] :=
@@ -10,7 +10,7 @@ Definition swap : val :=
          "p2" <- "x";;
          "swap" ["p1" +ₗ #1 ; "p2" +ₗ #1 ; "len" - #1].
 
-Lemma wp_swap `{!lrustG Σ} E l1 l2 vl1 vl2 (n : Z):
+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
@@ -22,7 +22,7 @@ Proof.
   - 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_mapsto_vec_cons. subst n.
+    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.

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

 From iris.program_logic Require Import weakestpre.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From lrust.lang Require Import lang proofmode notation.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
 
 Section tests.
-  Context `{!lrustG Σ}.
+  Context `{!lrustGS Σ}.
 
   Lemma test_location_cmp E (l1 l2 : loc) q1 q2 v1 v2 :
     {{{ ▷ l1 ↦{q1} v1 ∗ ▷ l2 ↦{q2} v2 }}}

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

-From iris.proofmode Require Import tactics.
+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.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
 Import uPred.
 
-Class lrustG Σ := LRustG {
-  lrustG_invG : invG Σ;
-  lrustG_gen_heapG :> heapG Σ
+Class lrustGS Σ := LRustGS {
+  lrustGS_invGS : invGS Σ;
+  lrustGS_heapGS :: heapGS Σ
 }.
 
-Instance lrustG_irisG `{!lrustG Σ} : irisG lrust_lang Σ := {
-  iris_invG := lrustG_invG;
+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 _ _
 }.
-Global Opaque iris_invG.
 
 Ltac inv_lit :=
   repeat match goal with
@@ -32,16 +31,16 @@ Ltac inv_bin_op_eval :=
   end.
 
 Local Hint Extern 0 (atomic _) => solve_atomic : core.
-Local Hint Extern 0 (head_reducible _ _) => eexists _, _, _, _; simpl : core.
+Local Hint Extern 0 (base_reducible _ _) => eexists _, _, _, _; simpl : core.
 
-Local Hint Constructors head_step bin_op_eval lit_neq lit_eq : 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.
-Instance AsRec_rec f xl e : AsRec (Rec f xl e) f xl e := eq_refl.
-Instance AsRec_rec_locked_val v f xl e :
+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.
 
@@ -52,18 +51,18 @@ Global Hint Extern 0 (DoSubst _ _ _ _) =>
 
 Class DoSubstL (xl : list binder) (esl : list expr) (e er : expr) :=
   do_subst_l : subst_l xl esl e = Some er.
-Instance do_subst_l_nil e : DoSubstL [] [] e e.
+Global Instance do_subst_l_nil e : DoSubstL [] [] e e.
 Proof. done. Qed.
-Instance do_subst_l_cons x xl es esl e er er' :
+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.
-Instance do_subst_vec xl (vsl : vec val (length xl)) e :
+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 `{!lrustG Σ}.
+Context `{!lrustGS Σ}.
 Implicit Types P Q : iProp Σ.
 Implicit Types e : expr.
 Implicit Types ef : option expr.
@@ -72,9 +71,9 @@ Implicit Types ef : option expr.
 Lemma wp_fork E e :
   {{{ ▷ WP e {{ _, True }} }}} Fork e @ E {{{ RET LitV LitPoison; True }}}.
 Proof.
-  iIntros (?) "?HΦ". iApply wp_lift_atomic_head_step; [done|].
+  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_head_step. iFrame.
+  iNext; iIntros (v2 σ2 efs Hstep) "_"; inv_base_step. iFrame.
   iModIntro. by iApply "HΦ".
 Qed.
 
@@ -82,9 +81,9 @@ Qed.
 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_head_step; inv_bin_op_eval; inv_lit; done.
+  simpl; intros; destruct_and?; inv_base_step; inv_bin_op_eval; inv_lit; done.
 Local Ltac solve_pure_exec :=
-  intros ?; apply nsteps_once, pure_head_step_pure_step;
+  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 :
@@ -141,9 +140,9 @@ Lemma wp_alloc E (n : Z) :
   {{{ 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_head_step_no_fork; auto.
+  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_head_step.
+  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.
@@ -155,11 +154,11 @@ Lemma wp_free E (n:Z) l vl :
     Free (Lit $ LitInt n) (Lit $ LitLoc l) @ E
   {{{ RET LitV LitPoison; True }}}.
 Proof.
-  iIntros (? Φ) "[>Hmt >Hf] HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
+  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_head_step.
+  iNext; iIntros (v2 σ2 efs Hstep) "_"; inv_base_step.
   iModIntro; iSplit=> //. iFrame. iApply "HΦ"; auto.
 Qed.
 
@@ -167,10 +166,10 @@ 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_head_step_no_fork; auto.
+  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_head_step.
+  iNext; iIntros (v2 σ2 efs Hstep) "_"; inv_base_step.
   iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
 Qed.
 
@@ -178,17 +177,17 @@ 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_head_step; auto. iIntros (σ1 ? κ κs n) "Hσ".
+  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_head_step. iMod "Hclose" as "_".
+  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_head_step_no_fork; auto.
+  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_head_step.
+  iNext; iIntros (e2 σ2 efs Hstep) "_ !>"; inv_base_step.
   iFrame "Hσ". iSplit; [done|]. by iApply "HΦ".
 Qed.
 
@@ -197,11 +196,11 @@ Lemma wp_write_sc E l e v v' :
   {{{ ▷ l ↦ v' }}} Write ScOrd (Lit $ LitLoc l) e @ E
   {{{ RET LitV LitPoison; l ↦ v }}}.
 Proof.
-  iIntros (<- Φ) ">Hv HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
+  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_head_step.
+  iNext; iIntros (v2 σ2 efs Hstep) "_"; inv_base_step.
   iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
 Qed.
 
@@ -211,16 +210,16 @@ Lemma wp_write_na E l e v v' :
   {{{ RET LitV LitPoison; l ↦ v }}}.
 Proof.
   iIntros (<- Φ) ">Hv HΦ".
-  iApply wp_lift_head_step; auto. iIntros (σ1 ? κ κs n) "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_head_step. iMod "Hclose" as "_".
+  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_head_step_no_fork; auto.
+  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_head_step.
+  iNext; iIntros (e2 σ2 efs Hstep) "_ !>"; inv_base_step.
   iFrame "Hσ". iSplit; [done|]. by iApply "HΦ".
 Qed.
 
@@ -231,10 +230,10 @@ Lemma wp_cas_int_fail E l q z1 e2 lit2 zl :
   {{{ RET LitV $ LitInt 0; l ↦{q} LitV (LitInt zl) }}}.
 Proof.
   iIntros (<- ? Φ) ">Hv HΦ".
-  iApply wp_lift_atomic_head_step_no_fork; auto.
+  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_head_step; inv_lit.
+  iNext; iIntros (v2 σ2 efs Hstep) "_"; inv_base_step; inv_lit.
   iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
 Qed.
 
@@ -245,10 +244,10 @@ Lemma wp_cas_suc E l lit1 e2 lit2 :
   {{{ RET LitV (LitInt 1); l ↦ LitV lit2 }}}.
 Proof.
   iIntros (<- ? Φ) ">Hv HΦ".
-  iApply wp_lift_atomic_head_step_no_fork; auto.
+  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_head_step; [inv_lit|].
+  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.
@@ -275,12 +274,12 @@ Lemma wp_cas_loc_fail E l q q' q1 l1 v1' e2 lit2 l' vl' :
       l ↦{q} LitV (LitLoc l') ∗ l' ↦{q'} vl' ∗ l1 ↦{q1} v1' }}}.
 Proof.
   iIntros (<- ? Φ) "(>Hl & >Hl' & >Hl1) HΦ".
-  iApply wp_lift_atomic_head_step_no_fork; auto.
+  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_head_step; inv_lit.
+  iNext; iIntros (v2 σ2 efs Hstep) "_"; inv_base_step; inv_lit.
   iModIntro; iSplit=> //. iFrame. iApply "HΦ"; iFrame.
 Qed.
 
@@ -293,10 +292,10 @@ Lemma wp_cas_loc_nondet E l l1 e2 l2 ll :
       else ⌜l1 ≠ ll⌝ ∗ l ↦ LitV (LitLoc ll) }}}.
 Proof.
   iIntros (<- Φ) ">Hv HΦ".
-  iApply wp_lift_atomic_head_step_no_fork; auto.
+  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_head_step; last lia.
+  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]".
@@ -304,18 +303,19 @@ Proof.
 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 {{ Φ }}.
+  (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_head_step_no_fork';
+  - iApply wp_lift_pure_det_base_step_no_fork';
       [done|solve_exec_safe|solve_exec_puredet|].
-    iApply wp_value. by iApply Hpost.
-  - iApply wp_lift_atomic_head_step_no_fork; subst=>//.
-    iIntros (σ1 ? κ κs n') "Hσ1". iModIntro. inv_head_step.
+    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
@@ -325,8 +325,8 @@ Proof.
       + iExists _, _. by iApply Hl1.
       + iExists _, _. by iApply Hl2.
       + by iApply Hpost. }
-    clear Hl1 Hl2. iNext. iIntros (e2 σ2 efs Hs) "!>".
-    inv_head_step. iSplitR=>//. inv_bin_op_eval; inv_lit.
+    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.
@@ -351,7 +351,7 @@ Proof.
     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 "* Hvl". rewrite -assoc.
+    iApply (IH _ _ with "Hl"). iIntros "%vl Hvl". rewrite -assoc.
     iApply ("HΦ" $! (v:::vl)). iFrame.
 Qed.
 
@@ -374,6 +374,6 @@ 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 vec_to_list_length.
+  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 lang.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
 
 Coercion LitInt : Z >-> base_lit.
 Coercion LitLoc : loc >-> base_lit.