.gitignore

@@ -13,7 +13,7 @@
 *~
 *.bak
 .coq-native/
-build-dep/
+builddep/
 Makefile.coq
 Makefile.coq.conf
 _opam

.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
@@ -16,10 +17,10 @@ variables:
   cache:
     key: "$CI_JOB_NAME"
     paths:
-    - opamroot/
+    - _opam/
   only:
-  - master
-  - /^ci/
+  - /^master/@iris/lambda-rust
+  - /^ci/@iris/lambda-rust
   except:
   - triggers
   - schedules
@@ -27,25 +28,42 @@ variables:
 
 ## Build jobs
 
-build-coq.dev:
+build-coq.8.20.0:
   <<: *template
   variables:
-    OPAM_PINS: "coq version dev"
+    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-coq.8.11.2:
+trigger-iris.timing:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.11.2"
-    OPAM_PKG: "coq-lambda-rust"
+    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
 
-build-iris.dev:
+trigger-iris.dev:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.12.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"
+    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:
-  - triggers
-  - schedules
-  - api
+    refs:
+    - triggers
+    - schedules
+    - api
+    variables:
+    - $TIMING_AD_HOC_ID == null

Makefile

-# Forward most targets to Coq makefile (with some trick to make this phony)
-%: Makefile.coq phony
-	+@make -f Makefile.coq $@
-
+# Default target
 all: Makefile.coq
-	+@make -f Makefile.coq all
+	+@$(MAKE) -f Makefile.coq all
 .PHONY: all
 
+# Permit local customization
+-include Makefile.local
+
+# Forward most targets to Coq makefile (with some trick to make this phony)
+%: Makefile.coq phony
+	@#echo "Forwarding $@"
+	+@$(MAKE) -f Makefile.coq $@
+phony: ;
+.PHONY: phony
+
 clean: Makefile.coq
-	+@make -f Makefile.coq clean
-	find theories tests exercises solutions \( -name "*.d" -o -name "*.vo" -o -name "*.vo[sk]" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete || true
-	rm -f Makefile.coq .lia.cache
+	+@$(MAKE) -f Makefile.coq clean
+	@# Make sure not to enter the `_opam` folder.
+	find [a-z]*/ \( -name "*.d" -o -name "*.vo" -o -name "*.vo[sk]" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete || true
+	rm -f Makefile.coq .lia.cache builddep/*
 .PHONY: clean
 
 # Create Coq Makefile.
 Makefile.coq: _CoqProject Makefile
-	"$(COQBIN)coq_makefile" -f _CoqProject -o Makefile.coq
+	"$(COQBIN)coq_makefile" -f _CoqProject -o Makefile.coq $(EXTRA_COQFILES)
 
 # Install build-dependencies
-build-dep/opam: opam Makefile
-	@echo "# Creating build-dep package."
-	@mkdir -p build-dep
-	@sed <opam -E 's/^(build|install|remove):.*/\1: []/; s/^name: *"(.*)" */name: "\1-builddep"/' >build-dep/opam
-	@fgrep builddep build-dep/opam >/dev/null || (echo "sed failed to fix the package name" && exit 1) # sanity check
-
-build-dep: build-dep/opam phony
-	@# We want opam to not just instal the build-deps now, but to also keep satisfying these
+OPAMFILES=$(wildcard *.opam)
+BUILDDEPFILES=$(addsuffix -builddep.opam, $(addprefix builddep/,$(basename $(OPAMFILES))))
+
+builddep/%-builddep.opam: %.opam Makefile
+	@echo "# Creating builddep package for $<."
+	@mkdir -p builddep
+	@sed <$< -E 's/^(build|install|remove):.*/\1: []/; s/"(.*)"(.*= *version.*)$$/"\1-builddep"\2/;' >$@
+
+builddep-opamfiles: $(BUILDDEPFILES)
+.PHONY: builddep-opamfiles
+
+builddep: builddep-opamfiles
+	@# We want opam to not just install the build-deps now, but to also keep satisfying these
 	@# constraints.  Otherwise, `opam upgrade` may well update some packages to versions
 	@# that are incompatible with our build requirements.
 	@# To achieve this, we create a fake opam package that has our build-dependencies as
 	@# dependencies, but does not actually install anything itself.
-	@echo "# Installing build-dep package."
-	@opam install $(OPAMFLAGS) build-dep/
+	@echo "# Installing builddep packages."
+	@opam install $(OPAMFLAGS) $(BUILDDEPFILES)
+.PHONY: builddep
 
-# Some files that do *not* need to be forwarded to Makefile.coq
-Makefile: ;
-_CoqProject: ;
-opam: ;
+# Backwards compatibility target
+build-dep: builddep
+.PHONY: build-dep
 
-# Phony wildcard targets
-phony: ;
-.PHONY: phony
+# Some files that do *not* need to be forwarded to Makefile.coq.
+# ("::" lets Makefile.local overwrite this.)
+Makefile Makefile.local _CoqProject $(OPAMFILES):: ;

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.11.2
+ - Coq 8.20.0
  - A development version of [Iris](https://gitlab.mpi-sws.org/iris/iris)
 
 ## Building from source
@@ -52,6 +52,26 @@ followed by `make build-dep`.
     `thread::spawn`, `take_mut::take`, `alias::once` as well as converting `&&T`
     to `&Box<T>`.
 
+## Changes since original RustBelt publication
+
+In this section we list fundamental changes to the model that were done since
+the publication of the
+[original RustBelt paper](https://plv.mpi-sws.org/rustbelt/popl18/).
+
+### Support for branding
+
+As part of the [GhostCell paper](http://plv.mpi-sws.org/rustbelt/ghostcell/),
+the model was adjusted to support branding.
+
+* The semantic interpretation of external lifetime contexts had to be changed to use a *syntactic* form of lifetime inclusion.
+* This changed interpretation broke the proof of "lifetime equalization".
+    Instead we prove a weaker rule that only substitutes lifetimes on positions that are compatible with *semantic* lifetime inclusion.
+    This is good enough for [the example](theories/typing/examples/nonlexical.v).
+* Furthermore, we had to redo the proof of `type_call_iris'`, a key lemma involved in calling functions and ensuring that their assumptions about lifetime parameters do indeed hold.
+    The old proof exploited *semantic* lifetime inclusion in external lifetime contexts in a crucial step.
+    The proof was fixed by adjusting the semantic interpretation of the local lifetime context.
+    In particular there is a new parameter `qmax` here that has to be threaded through everywhere.
+
 ## Where to Find the Proof Rules From the Paper
 
 ### Type System Rules
@@ -91,7 +111,7 @@ borrows" in the Coq development.
 | F-endlft              | programs.v      | type_endlft           |
 | F-call                | function.v      | type_call'            |
 
-Some of these lemmas are called `something'` because the version without the `'` is a derived, more speicalized form used together with our eauto-based `solve_typing` tactic.  You can see this tactic in action in the [examples](theories/typing/examples) subfolder.
+Some of these lemmas are called `something'` because the version without the `'` is a derived, more specialized form used together with our eauto-based `solve_typing` tactic.  You can see this tactic in action in the [examples](theories/typing/examples) subfolder.
 
 ### Lifetime Logic Rules
 

_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
-# non-canonical projections (https://github.com/coq/coq/pull/10076) do not exist yet in 8.9.
+# Cannot use non-canonical projections as it causes massive unification failures
+# (https://github.com/coq/coq/issues/6294).
 -arg -w -arg -redundant-canonical-projection
-# change_no_check does not exist yet in 8.9.
--arg -w -arg -convert_concl_no_check
-# "Declare Scope" does not exist yet in 8.9.
--arg -w -arg -undeclared-scope
+# 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/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/diverging_static.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/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

opam → coq-lambda-rust.opam

 opam-version: "2.0"
-name: "coq-lambda-rust"
 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"
@@ -14,8 +13,8 @@ the type system, and safety proof for some Rust libraries.
 """
 
 depends: [
-  "coq-iris" { (= "dev.2020-07-22.0.1e8432a9") | (= "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/sh
+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.
 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).
@@ -42,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
@@ -58,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 :=
@@ -150,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).
 
@@ -233,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)]>σ)
               []
@@ -282,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)]>σ)
               []
@@ -309,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.
@@ -345,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 :
@@ -356,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.
@@ -371,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.
@@ -401,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.
@@ -429,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.
 
@@ -446,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.
 
@@ -468,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.
 
@@ -481,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.
 
@@ -502,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 :
@@ -530,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 :=
@@ -570,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.
@@ -614,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/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,13 +16,15 @@ 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.
 
   Global Instance lock_proto_ne l : NonExpansive (lock_proto l).
   Proof. solve_proper. Qed.
+  Global Instance lock_proto_proper l : Proper ((≡) ==> (≡)) (lock_proto l).
+  Proof. apply ne_proper, _. Qed.
 
   Lemma lock_proto_iff l R R' :
     □ (R ↔ R') -∗ lock_proto l R -∗ lock_proto l R'.
@@ -34,7 +36,7 @@ Section proof.
   Lemma lock_proto_iff_proper l R R' :
     □ (R ↔ R') -∗ □ (lock_proto l R ↔ lock_proto l R').
   Proof.
-    iIntros "#HR !#". iSplit; iIntros "Hlck"; iApply (lock_proto_iff with "[HR] Hlck").
+    iIntros "#HR !>". iSplit; iIntros "Hlck"; iApply (lock_proto_iff with "[HR] Hlck").
     - done.
     - iModIntro; iSplit; iIntros; by iApply "HR".
   Qed.
@@ -75,7 +77,7 @@ Section proof.
     {{{ P }}} try_acquire [ #l ] @ E
     {{{ b, RET #b; (if b is true then R else True) ∗ P }}}.
   Proof.
-    iIntros "#Hproto !# * HP HΦ".
+    iIntros "#Hproto !> * HP HΦ".
     wp_rec. iMod ("Hproto" with "HP") as "(Hinv & Hclose)".
     iDestruct "Hinv" as ([]) "[Hl HR]".
     - wp_apply (wp_cas_int_fail with "Hl"); [done..|]. iIntros "Hl".
@@ -90,7 +92,7 @@ Section proof.
     □ (P ={E,∅}=∗ ▷ lock_proto l R ∗ (▷ lock_proto l R ={∅,E}=∗ P)) -∗
     {{{ P }}} acquire [ #l ] @ E {{{ RET #☠; R ∗ P }}}.
   Proof.
-    iIntros "#Hproto !# * HP HΦ". iLöb as "IH". wp_rec.
+    iIntros "#Hproto !> * HP HΦ". iLöb as "IH". wp_rec.
     wp_apply (try_acquire_spec with "Hproto HP"). iIntros ([]).
     - iIntros "[HR Hown]". wp_if. iApply "HΦ"; iFrame.
     - iIntros "[_ Hown]". wp_if. iApply ("IH" with "Hown HΦ").
@@ -100,11 +102,11 @@ Section proof.
     □ (P ={E,∅}=∗ ▷ lock_proto l R ∗ (▷ lock_proto l R ={∅,E}=∗ P)) -∗
     {{{ R ∗ P }}} release [ #l ] @ E {{{ RET #☠; P }}}.
   Proof.
-    iIntros "#Hproto !# * (HR & HP) HΦ". wp_let.
+    iIntros "#Hproto !> * (HR & HP) HΦ". wp_let.
     iMod ("Hproto" with "HP") as "(Hinv & Hclose)".
     iDestruct "Hinv" as (b) "[? _]". wp_write. iApply "HΦ".
     iApply "Hclose". iExists false. by iFrame.
   Qed.
 End proof.
 
-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.
 
@@ -119,10 +119,10 @@ Lemma join_handle_impl (Ψ1 Ψ2 : val → iProp Σ) c :
   □ (∀ v, Ψ1 v -∗ Ψ2 v) -∗ join_handle c Ψ1 -∗ join_handle c Ψ2.
 Proof.
   iIntros "#HΨ Hhdl". iDestruct "Hhdl" as (γf γj Ψ') "(Hj & H† & #? & #HΨ')".
-  iExists γf, γj, Ψ'. iFrame "#∗". iIntros "!# * ?".
+  iExists γf, γj, Ψ'. iFrame "#∗". iIntros "!> * ?".
   iApply "HΨ". iApply "HΨ'". done.
 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 }}}