.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,19 +28,21 @@ 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
 
 trigger-iris.timing:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.13.1   git+https://gitlab.mpi-sws.org/$IRIS_REPO#$IRIS_REV"
+    OPAM_PINS: "coq version 8.20.0   git+https://gitlab.mpi-sws.org/$IRIS_REPO#$IRIS_REV"
   tags:
   - fp-timing
   only:
@@ -55,7 +58,7 @@ trigger-iris.dev:
   variables:
     STDPP_REPO: "iris/stdpp"
     IRIS_REPO: "iris/iris"
-    OPAM_PINS: "coq version 8.13.dev   git+https://gitlab.mpi-sws.org/$STDPP_REPO#$STDPP_REV   git+https://gitlab.mpi-sws.org/$IRIS_REPO#$IRIS_REV"
+    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:

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-07-22.0.26ebf1ee") | (= "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,19 +2,19 @@ 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 lrustGpreS Σ := HeapGpreS {
-  lrustGpreS_irig :> invGpreS Σ;
-  lrustGpreS_heap :> inG Σ (authR heapUR);
-  lrustGpreS_heap_freeable :> inG Σ (authR heap_freeableUR)
+  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_lrustGpreS {Σ} : subG lrustΣ Σ → lrustGpreS Σ.
+Global Instance subG_lrustGpreS {Σ} : subG lrustΣ Σ → lrustGpreS Σ.
 Proof. solve_inG. Qed.
 
 Definition lrust_adequacy Σ `{!lrustGpreS Σ} e σ φ :

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,12 +151,12 @@ 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.
@@ -168,11 +168,8 @@ 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).
 
@@ -235,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)]>σ)
               []
@@ -284,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)]>σ)
               []
@@ -311,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.
@@ -347,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 :
@@ -358,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.
@@ -404,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.
@@ -432,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.
 
@@ -449,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.
 
@@ -473,10 +470,10 @@ 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; 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.
@@ -543,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 :=
@@ -597,27 +594,27 @@ Proof.
       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.
@@ -627,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
@@ -108,9 +108,9 @@ 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.
@@ -161,7 +161,7 @@ Section arc.
   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.
@@ -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"] :=
@@ -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"],
@@ -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,10 +28,10 @@ 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. *)
@@ -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"] :=
@@ -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 `{!lrustGS Σ}.

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 lrustGS Σ := LRustGS {
   lrustGS_invGS : invGS Σ;
-  lrustGS_heapGS :> heapGS Σ
+  lrustGS_heapGS :: heapGS Σ
 }.
 
-Instance lrustGS_irisGS `{!lrustGS Σ} : irisGS lrust_lang Σ := {
-  iris_invG := lrustGS_invGS;
+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,13 +51,13 @@ 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.
 
@@ -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.