.gitattributes

+*.v gitlab-language=coq

.gitignore

 *.vo
 *.vio
 *.v.d
+*.vos
+*.vok
+.coqdeps.d
+.Makefile.coq.d
 *.glob
 *.cache
 *.aux
@@ -9,6 +13,7 @@
 *~
 *.bak
 .coq-native/
-iris-enabled
+builddep/
 Makefile.coq
-opamroot
+Makefile.coq.conf
+_opam

.gitlab-ci.yml

-image: opam
+image: ralfjung/opam-ci:opam2
 
-lrust-coq8.5.3:
+stages:
+  - build
+
+variables:
+  CPU_CORES: "10"
+  OCAML: "ocaml-variants.4.14.0+options ocaml-option-flambda"
+
+.template: &template
+  stage: build
   tags:
-  - coq
+  - fp
   script:
-  # prepare
-  - . build/opam-ci.sh 'coq 8.5.3' 'coq-mathcomp-ssreflect 1.6'
-  # build
-  - 'time make -j8'
+  - git clone https://gitlab.mpi-sws.org/iris/ci.git ci -b opam2
+  - ci/buildjob
   cache:
-    key: "coq8.5.3-2"
+    key: "$CI_JOB_NAME"
     paths:
-    - opamroot/
+    - _opam/
+  only:
+  - /^master/@iris/lambda-rust
+  - /^ci/@iris/lambda-rust
+  except:
+  - triggers
+  - schedules
+  - api
+
+## Build jobs
+
+build-coq.8.20.0:
+  <<: *template
+  variables:
+    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.20.0   git+https://gitlab.mpi-sws.org/$IRIS_REPO#$IRIS_REV"
+  tags:
+  - fp-timing
+  only:
+  - triggers
+  - schedules
+  - api
+  except:
+    variables:
+    - $TIMING_AD_HOC_ID == null
+
+trigger-iris.dev:
+  <<: *template
+  variables:
+    STDPP_REPO: "iris/stdpp"
+    IRIS_REPO: "iris/iris"
+    OPAM_PINS: "coq version $NIGHTLY_COQ   git+https://gitlab.mpi-sws.org/$STDPP_REPO#$STDPP_REV   git+https://gitlab.mpi-sws.org/$IRIS_REPO#$IRIS_REV"
+  except:
   only:
-  - master
-  - ci
+    refs:
+    - triggers
+    - schedules
+    - api
+    variables:
+    - $TIMING_AD_HOC_ID == null

LICENSE

+All files in this development are distributed under the terms of the BSD
+license, included below.
+
+Copyright: lambdaRust developers and contributors
+
+------------------------------------------------------------------------------
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+    * Redistributions in binary form must reproduce the above copyright
+      notice, this list of conditions and the following disclaimer in the
+      documentation and/or other materials provided with the distribution.
+    * Neither the name of the copyright holder nor the names of its contributors
+      may be used to endorse or promote products derived from this software
+      without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND
+ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
+WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR
+ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
+(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
+LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON
+ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

Makefile

-# Process flags
-ifeq ($(Y), 1)
-	YFLAG=-y
-endif
-
-# Determine Coq version
-COQ_VERSION=$(shell coqc --version | egrep -o 'version 8.[0-9]' | egrep -o '8.[0-9]')
-COQ_MAKEFILE_FLAGS ?=
+# Default target
+all: Makefile.coq
+	+@$(MAKE) -f Makefile.coq all
+.PHONY: all
 
-ifeq ($(COQ_VERSION), 8.6)
-	COQ_MAKEFILE_FLAGS += -arg -w -arg -notation-overridden,-redundant-canonical-projection
-endif
+# Permit local customization
+-include Makefile.local
 
 # Forward most targets to Coq makefile (with some trick to make this phony)
 %: Makefile.coq phony
-	+@make -f Makefile.coq $@
-
-all: Makefile.coq
-	+@make -f Makefile.coq all
+	@#echo "Forwarding $@"
+	+@$(MAKE) -f Makefile.coq $@
+phony: ;
+.PHONY: phony
 
 clean: Makefile.coq
-	+@make -f Makefile.coq clean
-	find \( -name "*.v.d" -o -name "*.vo" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete
-	rm -f Makefile.coq
+	+@$(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
+# Create Coq Makefile.
 Makefile.coq: _CoqProject Makefile
-	@# we want to pass the correct name to coq_makefile or it will be confused.
-	coq_makefile $(COQ_MAKEFILE_FLAGS) -f _CoqProject -o Makefile.coq
-	mv Makefile.coq Makefile.coq.tmp
-	@# The sed script is for Coq 8.5 only, it fixes 'make verify'.
-	@# The awk script fixes 'make uninstall'.
-	sed 's/$$(COQCHK) $$(COQCHKFLAGS) $$(COQLIBS)/$$(COQCHK) $$(COQCHKFLAGS) $$(subst -Q,-R,$$(COQLIBS))/' < Makefile.coq.tmp \
-	  | awk '/^uninstall:/{print "uninstall:";print "\tif [ -d \"$$(DSTROOT)\"$$(COQLIBINSTALL)/iris/ ]; then find \"$$(DSTROOT)\"$$(COQLIBINSTALL)/iris/ -name \"*.vo\" -print -delete; fi";getline;next}1' > Makefile.coq
-	rm Makefile.coq.tmp
+	"$(COQBIN)coq_makefile" -f _CoqProject -o Makefile.coq $(EXTRA_COQFILES)
 
 # Install build-dependencies
-build-dep:
-	build/opam-pins.sh < opam.pins
-	opam upgrade $(YFLAG) # it is not nice that we upgrade *all* packages here, but I found no nice way to upgrade only those that we pinned
-	opam pin add coq-lambda-rust "$$(pwd)#HEAD" -k git -n -y
-	opam install coq-lambda-rust --deps-only $(YFLAG)
-	opam pin remove coq-lambda-rust
-
-# some fiels that do *not* need to be forwarded to Makefile.coq
-Makefile: ;
-_CoqProject: ;
-
-# Phony targets (i.e. targets that should be run no matter the timestamps of the involved files)
-phony: ;
-.PHONY: all clean phony
+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 builddep packages."
+	@opam install $(OPAMFLAGS) $(BUILDDEPFILES)
+.PHONY: builddep
+
+# Backwards compatibility target
+build-dep: builddep
+.PHONY: build-dep
+
+# 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
+  `&mut Cell<(A, B)>` -> `&mut (Cell<A>, Cell<B>)` and
+  `&Cell<(A, B)>` -> `&(Cell<A>, Cell<B>)` (both being NOPs).
+  * Turns out to be very hard!  The way we currently associate NA-masks with locations is in conflict with this.
+    The invariant for the entire cell gets allocated "on" the first location of the cell, so when we do splitting the 2nd projection has no way to access it...
+
+# ZST
+
+* Something like the example from <https://github.com/rust-lang/unsafe-code-guidelines/issues/168#issuecomment-512528361>

README.md

 # LAMBDA-RUST COQ DEVELOPMENT
 
-This is the Coq formalization of lambda-Rust.
+This is the Coq development accompanying lambda-Rust.
 
 ## Prerequisites
 
 This version is known to compile with:
 
- - Coq 8.5pl3
- - Ssreflect 1.6
- - A development version of [Iris](https://gitlab.mpi-sws.org/FP/iris-coq/)
+ - Coq 8.20.0
+ - A development version of [Iris](https://gitlab.mpi-sws.org/iris/iris)
 
-The easiest way to install the correct versions of the dependencies is through
-opam.  Once you got opam set up, just run `make build-dep` to install the right
-versions of the dependencies.  When the dependencies change (e.g., a newer
-version of Iris is needed), just run `make build-dep` again.
+## Building from source
 
-Alternatively, you can manually determine the required Iris commit by consulting
-the `opam.pins` file.
+When building from source, we recommend to use opam (2.0.0 or newer) for
+installing the dependencies.  This requires the following two repositories:
 
-## Building Instructions
+    opam repo add coq-released https://coq.inria.fr/opam/released
+    opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
 
-Run `make` to build the full development.
+Once you got opam set up, run `make build-dep` to install the right versions
+of the dependencies.
+
+Run `make -jN` to build the full development, where `N` is the number of your
+CPU cores.
+
+To update, do `git pull`.  After an update, the development may fail to compile
+because of outdated dependencies.  To fix that, please run `opam update`
+followed by `make build-dep`.
+
+## Structure
+
+* The folder [lang](theories/lang) contains the formalization of the lambda-Rust
+  core language, including the theorem showing that programs with data races get
+  stuck.
+* The folder [lifetime](theories/lifetime) proves the rules of the lifetime
+  logic, including derived constructions like (non-)atomic persistent borrows.
+  * The subfolder [model](theories/lifetime/model) proves the core rules, which
+    are then sealed behind a module signature in
+    [lifetime.v](theories/lifetime/lifetime.v).
+* The folder [typing](theories/typing) defines the domain of semantic types,
+  interpretations of all the judgments, as well as proofs of all typing rules.
+  * [type.v](theories/typing/type.v) contains the definition of a semantic type.
+  * [programs.v](theories/typing/programs.v) defines the typing judgements for
+    instructions and function bodies.
+  * [soundness.v](theories/typing/soundness.v) contains the main soundness
+    theorem of the type system.
+  * The subfolder [examples](theories/typing/examples) shows how the examples
+    from the technical appendix can be type-checked in Coq.
+  * The subfolder [lib](theories/typing/lib) contains proofs of safety of some
+    unsafely implement types from the Rust standard library and some user
+    crates: `Cell`, `RefCell`, `Rc`, `Arc`, `Mutex`, `RwLock`, `mem::swap`,
+    `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
+
+The files in [typing](theories/typing) prove semantic versions of the proof
+rules given in the paper.  Notice that mutable borrows are called "unique
+borrows" in the Coq development.
+
+| Proof Rule            | File            | Lemma                 |
+|-----------------------|-----------------|-----------------------|
+| T-bor-lft (for shr)   | shr_bor.v       | shr_mono              |
+| T-bor-lft (for mut)   | uniq_bor.v      | uniq_mono             |
+| C-subtype             | type_context.v  | subtype_tctx_incl     |
+| C-copy                | type_context.v  | copy_tctx_incl        |
+| C-split-bor (for shr) | product_split.v | tctx_split_shr_prod2  |
+| C-split-bor (for mut) | product_split.v | tctx_split_uniq_prod2 |
+| C-share               | borrow.v        | tctx_share            |
+| C-borrow              | borrow.v        | tctx_borrow           |
+| C-reborrow            | uniq_bor.v      | tctx_reborrow_uniq    |
+| Tread-own-copy        | own.v           | read_own_copy         |
+| Tread-own-move        | own.v           | read_own_move         |
+| Tread-bor (for shr)   | shr_bor.v       | read_shr              |
+| Tread-bor (for mut)   | uniq_bor.v      | read_uniq             |
+| Twrite-own            | own.v           | write_own             |
+| Twrite-bor            | uniq_bor.v      | write_uniq            |
+| S-num                 | int.v           | type_int_instr        |
+| S-nat-leq             | int.v           | type_le_instr         |
+| S-new                 | own.v           | type_new_instr        |
+| S-delete              | own.v           | type_delete_instr     |
+| S-deref               | programs.v      | type_deref_instr      |
+| S-assign              | programs.v      | type_assign_instr     |
+| F-consequence         | programs.v      | typed_body_mono       |
+| F-let                 | programs.v      | type_let'             |
+| F-letcont             | cont.v          | type_cont             |
+| F-jump                | cont.v          | type_jump             |
+| F-newlft              | programs.v      | type_newlft           |
+| 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 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
+
+The files in [lifetime](theories/lifetime) prove the lifetime logic, with the
+core rules being proven in the [model](theories/lifetime/model) subfolder and
+then sealed behind a module signature in
+[lifetime.v](theories/lifetime/lifetime.v).
+
+
+| Proof Rule        | File                | Lemma                |
+|-------------------|---------------------|----------------------|
+| LftL-begin        | model/creation.v    | lft_create           |
+| LftL-tok-fract    | model/primitive.v   | lft_tok_fractional   |
+| LftL-not-own-end  | model/primitive.v   | lft_tok_dead         |
+| LftL-end-persist  | model/definitions.v | lft_dead_persistent  |
+| LftL-borrow       | model/borrow.v      | bor_create           |
+| LftL-bor-split    | model/bor_sep.v     | bor_sep              |
+| LftL-bor-acc      | lifetime.v          | bor_acc              |
+| LftL-bor-shorten  | model/primitive.v   | bor_shorten          |
+| LftL-incl-isect   | model/primitive.v   | lft_intersect_incl_l |
+| LftL-incl-glb     | model/primitive.v   | lft_incl_glb         |
+| LftL-tok-inter    | model/primitive.v   | lft_tok_sep          |
+| LftL-end-inter    | model/primitive.v   | lft_dead_or          |
+| LftL-tok-unit     | model/primitive.v   | lft_tok_static       |
+| LftL-end-unit     | model/primitive.v   | lft_dead_static      |
+| LftL-reborrow     | lifetime.v          | rebor                |
+| LftL-bor-fracture | frac_borrow.v       | bor_fracture         |
+| LftL-fract-acc    | frac_borrow.v       | frac_bor_atomic_acc  |
+| LftL-bor-na       | na_borrow.v         | bor_na               |
+| LftL-na-acc       | na_borrow.v         | na_bor_acc           |
+
+## For Developers: How to update the Iris dependency
+
+* Do the change in Iris, push it.
+* Wait for CI to publish a new Iris version on the opam archive, then run
+  `opam update iris-dev`.
+* In lambdaRust, change the `opam` file to depend on the new version.
+* Run `make build-dep` (in lambdaRust) to install the new version of Iris.
+  You may have to do `make clean` as Coq will likely complain about .vo file
+  mismatches.

_CoqProject

--Q theories lrust
-theories/lifetime/definitions.v
-theories/lifetime/derived.v
-theories/lifetime/faking.v
-theories/lifetime/creation.v
-theories/lifetime/primitive.v
-theories/lifetime/accessors.v
-theories/lifetime/raw_reborrow.v
-theories/lifetime/borrow.v
-theories/lifetime/reborrow.v
-theories/lifetime/shr_borrow.v
-theories/lifetime/frac_borrow.v
-theories/lifetime/na_borrow.v
-theories/lang/adequacy.v
-theories/lang/derived.v
-theories/lang/heap.v
-theories/lang/lang.v
-theories/lang/lifting.v
-theories/lang/memcpy.v
-theories/lang/new_delete.v
-theories/lang/notation.v
-theories/lang/proofmode.v
-theories/lang/races.v
-theories/lang/tactics.v
-theories/lang/wp_tactics.v
-theories/typing/type.v
-theories/typing/type_incl.v
-theories/typing/perm.v
-theories/typing/typing.v
-theories/typing/lft_contexts.v
-theories/typing/type_context.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
+# 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
+
+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

build/opam-ci.sh

-#!/bin/bash
-set -e
-# This script installs the build dependencies for CI builds.
-
-# Prepare OPAM configuration
-export OPAMROOT="$(pwd)/opamroot"
-export OPAMJOBS=16
-export OPAM_EDITOR="$(which false)"
-
-# Make sure we got a good OPAM
-test -d "$OPAMROOT" || (mkdir "$OPAMROOT" && opam init --no-setup -y)
-eval `opam conf env`
-test -d "$OPAMROOT/repo/coq-extra-dev" || opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev -p 5
-test -d "$OPAMROOT/repo/coq-core-dev" || opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev -p 5
-test -d "$OPAMROOT/repo/coq-released" || opam repo add coq-released https://coq.inria.fr/opam/released -p 10
-opam update
-opam install ocamlfind -y # Remove this once the Coq crew fixed their package...
-
-# Install fixed versions of some dependencies
-echo
-for PIN in "${@}"
-do
-    echo "Applying pin: $PIN"
-    opam pin add $PIN -k version -y
-done
-
-# Install build-dependencies
-echo
-make build-dep Y=1
-
-# done
-echo
-coqc -v

build/opam-pins.sh

-#!/bin/bash
-set -e
-## Process an opam.pins file from stdin: Add all the given pins, but don't install anything.
-## Usage:
-##   ./opam-pins.sh < opam.pins
-
-# Process stdin
-while read PACKAGE URL HASH; do
-    if echo "$URL" | egrep '^https://gitlab\.mpi-sws\.org' > /dev/null; then
-        echo "[opam-pins] Recursing into $URL"
-        # an MPI URL -- try doing recursive pin processing
-        curl -f "$URL/raw/$HASH" 2> /dev/null | "$0"
-    fi
-    echo "[opam-pins] Applying pin: $PACKAGE -> $URL#$HASH"
-    opam pin add "$PACKAGE.dev.$HASH" "$URL#$HASH" -k git -y -n
-    echo
-done

coq-lambda-rust.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: "LambdaRust Coq formalization"
+description: """
+A formal model of a Rust core language and type system, a logical relation for
+the type system, and safety proof for some Rust libraries.
+"""
+
+depends: [
+  "coq-lifetime-logic" { = version }
+]
+
+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-01-25.1.8a8f05fb") | (= "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

-From iris.program_logic Require Export hoare adequacy.
+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.
+From iris.prelude Require Import options.
 
-Class heapPreG Σ := HeapPreG {
-  heap_preG_ownP :> ownPPreG lrust_lang Σ;
-  heap_preG_heap :> inG Σ (authR heapUR);
-  heap_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 heapΣ : gFunctors :=
-  #[ownPΣ state;
+Definition lrustΣ : gFunctors :=
+  #[invΣ;
     GFunctor (constRF (authR heapUR));
     GFunctor (constRF (authR heap_freeableUR))].
-Instance subG_heapPreG {Σ} : subG heapΣ Σ → heapPreG Σ.
-Proof. intros [? [?%subG_inG ?%subG_inG]%subG_inv]%subG_inv. split; apply _. Qed.
+Global Instance subG_lrustGpreS {Σ} : subG lrustΣ Σ → lrustGpreS Σ.
+Proof. solve_inG. Qed.
 
-Definition heap_adequacy Σ `{heapPreG Σ} e σ φ :
-  (∀ `{heapG Σ}, {{ heap_ctx }} e {{ v, ⌜φ v⌝ }}) →
-  adequate e σ φ.
+Definition lrust_adequacy Σ `{!lrustGpreS Σ} e σ φ :
+  (∀ `{!lrustGS Σ}, True ⊢ WP e {{ v, ⌜φ v⌝ }}) →
+  adequate NotStuck e σ (λ v _, φ v).
 Proof.
-  intros Hwp; eapply (ownP_adequacy Σ _). iIntros (?) "Hσ".
+  intros Hwp; eapply (wp_adequacy _ _); iIntros (??).
   iMod (own_alloc (● to_heap σ)) as (vγ) "Hvγ".
   { apply (auth_auth_valid (to_heap _)), to_heap_valid. }
-  iMod (own_alloc (● (∅ : heap_freeableUR))) as (fγ) "Hfγ"; first done.
-  set (Hheap := HeapG _ _ _ _ vγ fγ).
-  iMod (inv_alloc heapN _ heap_inv with "[-]"); [iNext; iExists σ, ∅; by iFrame|].
-  iApply (Hwp _). by rewrite /heap_ctx.
+  iMod (own_alloc (● (∅ : heap_freeableUR))) as (fγ) "Hfγ";
+    first by apply auth_auth_valid.
+  set (Hheap := HeapGS _ _ _ vγ fγ).
+  iModIntro. iExists (λ σ _, heap_ctx σ), (λ _, True%I). iSplitL.
+  { iExists ∅. by iFrame. }
+  by iApply (Hwp (LRustGS _ _ Hheap)).
 Qed.

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

-From iris.algebra Require Import cmra_big_op gmap frac agree.
-From iris.algebra Require Import csum excl auth.
-From iris.base_logic Require Import big_op lib.invariants lib.fractional.
-From iris.proofmode Require Export tactics.
-From lrust.lang Require Export lifting.
+From stdpp Require Import coPset.
+From iris.algebra Require Import big_op gmap frac agree numbers.
+From iris.algebra Require Import csum excl auth cmra_big_op.
+From iris.bi Require Import fractional.
+From iris.base_logic Require Export lib.own.
+From iris.proofmode Require Export proofmode.
+From lrust.lang Require Export lang.
+From iris.prelude Require Import options.
 Import uPred.
 
-Definition heapN : namespace := nroot .@ "heap".
+Definition lock_stateR : cmra :=
+  csumR (exclR unitO) natR.
 
-Definition lock_stateR : cmraT :=
-  csumR (exclR unitC) natR.
+(* These days this could use gmap_view, but this code predates that. *)
+Definition heapUR : ucmra :=
+  gmapUR loc (prodR (prodR fracR lock_stateR) (agreeR valO)).
 
-Definition heapUR : ucmraT :=
-  gmapUR loc (prodR (prodR fracR lock_stateR) (agreeR valC)).
+Definition heap_freeableUR : ucmra :=
+  gmapUR block (prodR fracR (gmapR Z (exclR unitO))).
 
-Definition heap_freeableUR : ucmraT :=
-  gmapUR block (prodR fracR (gmapR Z (exclR unitC))).
-
-Class heapG Σ := HeapG {
-  heapG_ownP_inG :> ownPG lrust_lang Σ;
-  heap_inG :> inG Σ (authR heapUR);
-  heap_freeable_inG :> inG Σ (authR heap_freeableUR);
+Class heapGS Σ := HeapGS {
+  heap_inG :: inG Σ (authR heapUR);
+  heap_freeable_inG :: inG Σ (authR heap_freeableUR);
   heap_name : gname;
   heap_freeable_name : gname
 }.
@@ -30,75 +31,67 @@ Definition to_heap : state → heapUR :=
   fmap (λ v, (1%Qp, to_lock_stateR (v.1), to_agree (v.2))).
 Definition heap_freeable_rel (σ : state) (hF : heap_freeableUR) : Prop :=
   ∀ blk qs, hF !! blk = Some qs →
-  qs.2 ≠ ∅ ∧ ∀ i, is_Some (σ !! (blk, i)) ↔ is_Some (qs.2 !! i).
+    qs.2 ≠ ∅ ∧ ∀ i, is_Some (σ !! (blk, i)) ↔ is_Some (qs.2 !! i).
 
 Section definitions.
-  Context `{heapG Σ}.
+  Context `{!heapGS Σ}.
 
-  Definition heap_mapsto_st (st : lock_state)
+  Definition heap_pointsto_st (st : lock_state)
              (l : loc) (q : Qp) (v: val) : iProp Σ :=
     own heap_name (◯ {[ l := (q, to_lock_stateR st, to_agree v) ]}).
 
-  Definition heap_mapsto_def (l : loc) (q : Qp) (v: val) : iProp Σ :=
-    heap_mapsto_st (RSt 0) l q v.
-  Definition heap_mapsto_aux : { x | x = @heap_mapsto_def }. by eexists. Qed.
-  Definition heap_mapsto := proj1_sig heap_mapsto_aux.
-  Definition heap_mapsto_eq : @heap_mapsto = @heap_mapsto_def :=
-    proj2_sig heap_mapsto_aux.
+  Definition heap_pointsto_def (l : loc) (q : Qp) (v: val) : iProp Σ :=
+    heap_pointsto_st (RSt 0) l q v.
+  Definition heap_pointsto_aux : seal (@heap_pointsto_def). Proof. by eexists. Qed.
+  Definition heap_pointsto := unseal heap_pointsto_aux.
+  Definition heap_pointsto_eq : @heap_pointsto = @heap_pointsto_def :=
+    seal_eq heap_pointsto_aux.
 
-  Definition heap_mapsto_vec (l : loc) (q : Qp) (vl : list val) : iProp Σ :=
-    ([∗ list] i ↦ v ∈ vl, heap_mapsto (shift_loc l i) q v)%I.
+  Definition heap_pointsto_vec (l : loc) (q : Qp) (vl : list val) : iProp Σ :=
+    ([∗ list] i ↦ v ∈ vl, heap_pointsto (l +ₗ i) q v)%I.
 
-  Fixpoint inter (i0 : Z) (n : nat) : gmapR Z (exclR unitC) :=
+  Fixpoint inter (i0 : Z) (n : nat) : gmapR Z (exclR unitO) :=
     match n with O => ∅ | S n => <[i0 := Excl ()]>(inter (i0+1) n) end.
 
   Definition heap_freeable_def (l : loc) (q : Qp) (n: nat) : iProp Σ :=
     own heap_freeable_name (◯ {[ l.1 := (q, inter (l.2) n) ]}).
-  Definition heap_freeable_aux : { x | x = @heap_freeable_def }. by eexists. Qed.
-  Definition heap_freeable := proj1_sig heap_freeable_aux.
+  Definition heap_freeable_aux : seal (@heap_freeable_def). Proof. by eexists. Qed.
+  Definition heap_freeable := unseal heap_freeable_aux.
   Definition heap_freeable_eq : @heap_freeable = @heap_freeable_def :=
-    proj2_sig heap_freeable_aux.
-
-  Definition heap_inv : iProp Σ :=
-    (∃ (σ:state) hF, ownP σ ∗ own heap_name (● to_heap σ)
-                            ∗ own heap_freeable_name (● hF)
-                            ∗ ⌜heap_freeable_rel σ hF⌝)%I.
-  Definition heap_ctx : iProp Σ := inv heapN heap_inv.
+    seal_eq heap_freeable_aux.
 
-  Global Instance heap_ctx_persistent : PersistentP heap_ctx.
-  Proof. apply _. Qed.
+  Definition heap_ctx (σ:state) : iProp Σ :=
+    (∃ hF, own heap_name (● to_heap σ)
+         ∗ own heap_freeable_name (● hF)
+         ∗ ⌜heap_freeable_rel σ hF⌝)%I.
 End definitions.
 
-Typeclasses Opaque heap_ctx heap_mapsto heap_freeable heap_mapsto_vec.
-Instance: Params (@heap_mapsto) 4.
-Instance: Params (@heap_freeable) 5.
+Global Typeclasses Opaque heap_pointsto_vec.
+Global Instance: Params (@heap_pointsto) 4 := {}.
+Global Instance: Params (@heap_freeable) 5 := {}.
 
-Notation "l ↦{ q } v" := (heap_mapsto l q v)
-  (at level 20, q at level 50, format "l  ↦{ q }  v") : uPred_scope.
-Notation "l ↦ v" := (heap_mapsto l 1 v) (at level 20) : uPred_scope.
+Notation "l ↦{ q } v" := (heap_pointsto l q v)
+  (at level 20, q at level 50, format "l  ↦{ q }  v") : bi_scope.
+Notation "l ↦ v" := (heap_pointsto l 1 v) (at level 20) : bi_scope.
 
-Notation "l ↦∗{ q } vl" := (heap_mapsto_vec l q vl)
-  (at level 20, q at level 50, format "l  ↦∗{ q }  vl") : uPred_scope.
-Notation "l ↦∗ vl" := (heap_mapsto_vec l 1 vl) (at level 20) : uPred_scope.
+Notation "l ↦∗{ q } vl" := (heap_pointsto_vec l q vl)
+  (at level 20, q at level 50, format "l  ↦∗{ q }  vl") : bi_scope.
+Notation "l ↦∗ vl" := (heap_pointsto_vec l 1 vl) (at level 20) : bi_scope.
 
 Notation "l ↦∗{ q }: P" := (∃ vl, l ↦∗{ q } vl ∗ P vl)%I
-  (at level 20, q at level 50, format "l  ↦∗{ q }:  P") : uPred_scope.
+  (at level 20, q at level 50, format "l  ↦∗{ q }:  P") : bi_scope.
 Notation "l ↦∗: P " := (∃ vl, l ↦∗ vl ∗ P vl)%I
-  (at level 20, format "l  ↦∗:  P") : uPred_scope.
+  (at level 20, format "l  ↦∗:  P") : bi_scope.
 
 Notation "†{ q } l … n" := (heap_freeable l q n)
-  (at level 20, q at level 50, format "†{ q } l … n") : uPred_scope.
-Notation "† l … n" := (heap_freeable l 1 n) (at level 20) : uPred_scope.
+  (at level 20, q at level 50, format "†{ q } l … n") : bi_scope.
+Notation "† l … n" := (heap_freeable l 1 n) (at level 20) : bi_scope.
 
-Section heap.
-  Context {Σ : gFunctors}.
-  Implicit Types P Q : iProp Σ.
+Section to_heap.
   Implicit Types σ : state.
-  Implicit Types E : coPset.
 
-  (** Allocation *)
   Lemma to_heap_valid σ : ✓ to_heap σ.
-  Proof. intros l. rewrite lookup_fmap. case (σ !! l)=> [[[|n] v]|] //=. Qed.
+  Proof. intros l. rewrite lookup_fmap. destruct (σ !! l) as [[[|n] v]|] eqn:EQ; rewrite EQ //. Qed.
 
   Lemma lookup_to_heap_None σ l : σ !! l = None → to_heap σ !! l = None.
   Proof. by rewrite /to_heap lookup_fmap=> ->. Qed.
@@ -110,82 +103,89 @@ Section heap.
 
   Lemma to_heap_delete σ l : to_heap (delete l σ) = delete l (to_heap σ).
   Proof. by rewrite /to_heap fmap_delete. Qed.
+End to_heap.
 
-  Context `{heapG Σ}.
+Section heap.
+  Context `{!heapGS Σ}.
+  Implicit Types P Q : iProp Σ.
+  Implicit Types σ : state.
+  Implicit Types E : coPset.
 
-  (** General properties of mapsto and freeable *)
-  Global Instance heap_mapsto_timeless l q v : TimelessP (l↦{q}v).
-  Proof. rewrite heap_mapsto_eq /heap_mapsto_def. apply _. Qed.
+  (** General properties of pointsto and freeable *)
+  Global Instance heap_pointsto_timeless l q v : Timeless (l↦{q}v).
+  Proof. rewrite heap_pointsto_eq /heap_pointsto_def. apply _. Qed.
 
-  Global Instance heap_mapsto_fractional l v: Fractional (λ q, l ↦{q} v)%I.
+  Global Instance heap_pointsto_fractional l v: Fractional (λ q, l ↦{q} v)%I.
   Proof.
     intros p q.
-    by rewrite heap_mapsto_eq -own_op -auth_frag_op op_singleton pair_op agree_idemp.
+    by rewrite heap_pointsto_eq -own_op -auth_frag_op singleton_op -pair_op agree_idemp.
   Qed.
-  Global Instance heap_mapsto_as_fractional l q v:
+  Global Instance heap_pointsto_as_fractional l q v:
     AsFractional (l ↦{q} v) (λ q, l ↦{q} v)%I q.
-  Proof. done. Qed.
+  Proof. split; first done. apply _. Qed.
+
+  Global Instance frame_pointsto p l v q1 q2 q :
+    FrameFractionalQp q1 q2 q →
+    Frame p (l ↦{q1} v) (l ↦{q2} v) (l ↦{q} v) | 5.
+  Proof. apply: frame_fractional. Qed.
 
-  Global Instance heap_mapsto_vec_timeless l q vl : TimelessP (l ↦∗{q} vl).
-  Proof. rewrite /heap_mapsto_vec. apply _. Qed.
+  Global Instance heap_pointsto_vec_timeless l q vl : Timeless (l ↦∗{q} vl).
+  Proof. rewrite /heap_pointsto_vec. apply _. Qed.
 
-  Global Instance heap_mapsto_vec_fractional l vl: Fractional (λ q, l ↦∗{q} vl)%I.
+  Global Instance heap_pointsto_vec_fractional l vl: Fractional (λ q, l ↦∗{q} vl)%I.
   Proof.
-    intros p q. rewrite /heap_mapsto_vec -big_sepL_sepL.
+    intros p q. rewrite /heap_pointsto_vec -big_sepL_sep.
     by setoid_rewrite (fractional (Φ := λ q, _ ↦{q} _)%I).
   Qed.
-  Global Instance heap_mapsto_vec_as_fractional l q vl:
+  Global Instance heap_pointsto_vec_as_fractional l q vl:
     AsFractional (l ↦∗{q} vl) (λ q, l ↦∗{q} vl)%I q.
-  Proof. done. Qed.
+  Proof. split; first done. apply _. Qed.
 
-  Global Instance heap_freeable_timeless q l n : TimelessP (†{q}l…n).
+  Global Instance heap_freeable_timeless q l n : Timeless (†{q}l…n).
   Proof. rewrite heap_freeable_eq /heap_freeable_def. apply _. Qed.
 
-  Lemma heap_mapsto_agree l q1 q2 v1 v2 :
-    l ↦{q1} v1 ∗ l ↦{q2} v2 ⊢ ⌜v1 = v2⌝.
+  Lemma heap_pointsto_agree l q1 q2 v1 v2 : l ↦{q1} v1 ∗ l ↦{q2} v2 ⊢ ⌜v1 = v2⌝.
   Proof.
-    rewrite heap_mapsto_eq -own_op -auth_frag_op own_valid discrete_valid.
-    eapply pure_elim; [done|]=> /auth_own_valid /=.
-    rewrite op_singleton pair_op singleton_valid. case.
-    rewrite /= to_agree_comp_valid=>? Heq. fold_leibniz. eauto.
+    rewrite heap_pointsto_eq -own_op -auth_frag_op own_valid discrete_valid.
+    eapply pure_elim; [done|]=> /auth_frag_valid /=.
+    rewrite singleton_op -pair_op singleton_valid=> -[? /to_agree_op_inv_L->]; eauto.
   Qed.
 
-  Lemma heap_mapsto_vec_nil l q : l ↦∗{q} [] ⊣⊢ True.
-  Proof. by rewrite /heap_mapsto_vec big_sepL_nil. Qed.
+  Lemma heap_pointsto_vec_nil l q : l ↦∗{q} [] ⊣⊢ True.
+  Proof. by rewrite /heap_pointsto_vec. Qed.
 
-  Lemma heap_mapsto_vec_app l q vl1 vl2 :
-    l ↦∗{q} (vl1 ++ vl2) ⊣⊢ l ↦∗{q} vl1 ∗ shift_loc l (length vl1) ↦∗{q} vl2.
+  Lemma heap_pointsto_vec_app l q vl1 vl2 :
+    l ↦∗{q} (vl1 ++ vl2) ⊣⊢ l ↦∗{q} vl1 ∗ (l +ₗ length vl1) ↦∗{q} vl2.
   Proof.
-    rewrite /heap_mapsto_vec big_sepL_app.
+    rewrite /heap_pointsto_vec big_sepL_app.
     do 2 f_equiv. intros k v. by rewrite shift_loc_assoc_nat.
   Qed.
 
-  Lemma heap_mapsto_vec_singleton l q v : l ↦∗{q} [v] ⊣⊢ l ↦{q} v.
-  Proof. by rewrite /heap_mapsto_vec big_sepL_singleton /= shift_loc_0. Qed.
+  Lemma heap_pointsto_vec_singleton l q v : l ↦∗{q} [v] ⊣⊢ l ↦{q} v.
+  Proof. by rewrite /heap_pointsto_vec /= shift_loc_0 right_id. Qed.
 
-  Lemma heap_mapsto_vec_cons l q v vl:
-    l ↦∗{q} (v :: vl) ⊣⊢ l ↦{q} v ∗ shift_loc l 1 ↦∗{q} vl.
+  Lemma heap_pointsto_vec_cons l q v vl:
+    l ↦∗{q} (v :: vl) ⊣⊢ l ↦{q} v ∗ (l +ₗ 1) ↦∗{q} vl.
   Proof.
-    by rewrite (heap_mapsto_vec_app l q [v] vl) heap_mapsto_vec_singleton.
+    by rewrite (heap_pointsto_vec_app l q [v] vl) heap_pointsto_vec_singleton.
   Qed.
 
-  Lemma heap_mapsto_vec_op l q1 q2 vl1 vl2 :
+  Lemma heap_pointsto_vec_op l q1 q2 vl1 vl2 :
     length vl1 = length vl2 →
     l ↦∗{q1} vl1 ∗ l ↦∗{q2} vl2 ⊣⊢ ⌜vl1 = vl2⌝ ∧ l ↦∗{q1+q2} vl1.
   Proof.
     intros Hlen%Forall2_same_length. apply (anti_symm (⊢)).
     - revert l. induction Hlen as [|v1 v2 vl1 vl2 _ _ IH]=> l.
-      { rewrite !heap_mapsto_vec_nil. iIntros "_"; auto. }
-      rewrite !heap_mapsto_vec_cons. iIntros "[[Hv1 Hvl1] [Hv2 Hvl2]]".
-      iDestruct (IH (shift_loc l 1) with "[Hvl1 Hvl2]") as "[% $]";
-        subst; first by iFrame.
-      rewrite (inj_iff (:: vl2)).
-      iDestruct (heap_mapsto_agree with "[$Hv1 $Hv2]") as %<-.
+      { rewrite !heap_pointsto_vec_nil. iIntros "_"; auto. }
+      rewrite !heap_pointsto_vec_cons. iIntros "[[Hv1 Hvl1] [Hv2 Hvl2]]".
+      iDestruct (IH (l +ₗ 1) with "[$Hvl1 $Hvl2]") as "[% $]"; subst.
+      rewrite (inj_iff (.:: vl2)).
+      iDestruct (heap_pointsto_agree with "[$Hv1 $Hv2]") as %<-.
       iSplit; first done. iFrame.
     - by iIntros "[% [$ Hl2]]"; subst.
   Qed.
 
-  Lemma heap_mapsto_vec_prop_op l q1 q2 n (Φ : list val → iProp Σ) :
+  Lemma heap_pointsto_pred_op l q1 q2 n (Φ : list val → iProp Σ) :
     (∀ vl, Φ vl -∗ ⌜length vl = n⌝) →
     l ↦∗{q1}: Φ ∗ l ↦∗{q2}: (λ vl, ⌜length vl = n⌝) ⊣⊢ l ↦∗{q1+q2}: Φ.
   Proof.
@@ -193,22 +193,63 @@ Section heap.
     - iIntros "[Hmt1 Hmt2]".
       iDestruct "Hmt1" as (vl) "[Hmt1 Hown]". iDestruct "Hmt2" as (vl') "[Hmt2 %]".
       iDestruct (Hlen with "Hown") as %?.
-      iCombine "Hmt1" "Hmt2" as "Hmt". rewrite heap_mapsto_vec_op; last congruence.
+      iCombine "Hmt1" "Hmt2" as "Hmt". rewrite heap_pointsto_vec_op; last congruence.
       iDestruct "Hmt" as "[_ Hmt]". iExists vl. by iFrame.
     - iIntros "Hmt". iDestruct "Hmt" as (vl) "[[Hmt1 Hmt2] Hown]".
       iDestruct (Hlen with "Hown") as %?.
       iSplitL "Hmt1 Hown"; iExists _; by iFrame.
   Qed.
 
-  Lemma heap_mapsto_vec_combine l q vl :
-    vl ≠ [] →
-    l ↦∗{q} vl ⊣⊢ own heap_name (◯ [⋅ list] i ↦ v ∈ vl,
-      {[shift_loc l i := (q, Cinr 0%nat, to_agree v)]}).
+  Lemma heap_pointsto_pred_wand l q Φ1 Φ2 :
+    l ↦∗{q}: Φ1 -∗ (∀ vl, Φ1 vl -∗ Φ2 vl) -∗ l ↦∗{q}: Φ2.
   Proof.
-    rewrite /heap_mapsto_vec heap_mapsto_eq /heap_mapsto_def /heap_mapsto_st=>?.
-    by rewrite (big_opL_commute (Auth None)) big_opL_commute1 //.
+    iIntros "Hm Hwand". iDestruct "Hm" as (vl) "[Hm HΦ]". iExists vl.
+    iFrame "Hm". by iApply "Hwand".
   Qed.
 
+  Lemma heap_pointsto_pred_iff_proper l q Φ1 Φ2 :
+    □ (∀ vl, Φ1 vl ↔ Φ2 vl) -∗ □ (l ↦∗{q}: Φ1 ↔ l ↦∗{q}: Φ2).
+  Proof.
+    iIntros "#HΦ !>". iSplit; iIntros; iApply (heap_pointsto_pred_wand with "[-]"); try done; [|];
+    iIntros; by iApply "HΦ".
+  Qed.
+
+  Lemma heap_pointsto_vec_combine l q vl :
+    vl ≠ [] →
+    l ↦∗{q} vl ⊣⊢ own heap_name (◯ [^op list] i ↦ v ∈ vl,
+      {[l +ₗ i := (q, Cinr 0%nat, to_agree v)]}).
+  Proof.
+    rewrite /heap_pointsto_vec heap_pointsto_eq /heap_pointsto_def /heap_pointsto_st=>?.
+    rewrite (big_opL_commute auth_frag) big_opL_commute1 //.
+  Qed.
+
+  Global Instance heap_pointsto_pred_fractional l (P : list val → iProp Σ):
+    (∀ vl, Persistent (P vl)) → Fractional (λ q, l ↦∗{q}: P)%I.
+  Proof.
+    intros p q q'. iSplit.
+    - iIntros "H". iDestruct "H" as (vl) "[[Hown1 Hown2] #HP]".
+      iSplitL "Hown1"; eauto.
+    - iIntros "[H1 H2]". iDestruct "H1" as (vl1) "[Hown1 #HP1]".
+      iDestruct "H2" as (vl2) "[Hown2 #HP2]".
+      set (ll := min (length vl1) (length vl2)).
+      rewrite -[vl1](firstn_skipn ll) -[vl2](firstn_skipn ll) 2!heap_pointsto_vec_app.
+      iDestruct "Hown1" as "[Hown1 _]". iDestruct "Hown2" as "[Hown2 _]".
+      iCombine "Hown1" "Hown2" as "Hown". rewrite heap_pointsto_vec_op; last first.
+      { rewrite !length_firstn. subst ll.
+        rewrite -!Nat.min_assoc Nat.min_idempotent Nat.min_comm -Nat.min_assoc Nat.min_idempotent Nat.min_comm. done. }
+      iDestruct "Hown" as "[H Hown]". iDestruct "H" as %Hl. iExists (take ll vl1). iFrame.
+      destruct (Nat.min_spec (length vl1) (length vl2)) as [[Hne Heq]|[Hne Heq]].
+      + iClear "HP2". rewrite take_ge; last first.
+        { rewrite -Heq /ll. done. }
+        rewrite drop_ge; first by rewrite app_nil_r. by rewrite -Heq.
+      + iClear "HP1". rewrite Hl take_ge; last first.
+        { rewrite -Heq /ll. done. }
+        rewrite drop_ge; first by rewrite app_nil_r. by rewrite -Heq.
+  Qed.
+  Global Instance heap_pointsto_pred_as_fractional l q (P : list val → iProp Σ):
+    (∀ vl, Persistent (P vl)) → AsFractional (l ↦∗{q}: P) (λ q, l ↦∗{q}: P)%I q.
+  Proof. split; first done. apply _. Qed.
+
   Lemma inter_lookup_Some i j (n : nat):
     i ≤ j < i+n → inter i n !! j = Excl' ().
   Proof.
@@ -230,18 +271,18 @@ Section heap.
     - by rewrite !inter_lookup_None; try lia.
   Qed.
   Lemma inter_valid i n : ✓ inter i n.
-  Proof. revert i. induction n as [|n IH]=>i. done. by apply insert_valid. Qed.
+  Proof. revert i. induction n as [|n IH]=>i; first done. by apply insert_valid. Qed.
 
   Lemma heap_freeable_op_eq l q1 q2 n n' :
-    †{q1}l…n ∗ †{q2}shift_loc l n…n' ⊣⊢ †{q1+q2}l…(n+n').
+    †{q1}l…n ∗ †{q2}l +ₗ n … n' ⊣⊢ †{q1+q2}l…(n+n').
   Proof.
     by rewrite heap_freeable_eq /heap_freeable_def -own_op -auth_frag_op
-      op_singleton pair_op inter_op.
+      singleton_op -pair_op inter_op.
   Qed.
 
   (** Properties about heap_freeable_rel and heap_freeable *)
   Lemma heap_freeable_rel_None σ l hF :
-    (∀ m : Z, σ !! shift_loc l m = None) → heap_freeable_rel σ hF →
+    (∀ m : Z, σ !! (l +ₗ m) = None) → heap_freeable_rel σ hF →
     hF !! l.1 = None.
   Proof.
     intros FRESH REL. apply eq_None_not_Some. intros [[q s] [Hsne REL']%REL].
@@ -252,7 +293,7 @@ Section heap.
   Lemma heap_freeable_is_Some σ hF l n i :
     heap_freeable_rel σ hF →
     hF !! l.1 = Some (1%Qp, inter (l.2) n) →
-    is_Some (σ !! shift_loc l i) ↔ 0 ≤ i ∧ i < n.
+    is_Some (σ !! (l +ₗ i)) ↔ 0 ≤ i ∧ i < n.
   Proof.
     destruct l as [b j]; rewrite /shift_loc /=. intros REL Hl.
     destruct (REL b (1%Qp, inter j n)) as [_ ->]; simpl in *; auto.
@@ -261,22 +302,20 @@ Section heap.
     - rewrite is_Some_alt inter_lookup_None; lia.
   Qed.
 
-  Lemma heap_freeable_rel_init_mem l h vl σ:
-    vl ≠ [] →
-    (∀ m : Z, σ !! shift_loc l m = None) →
+  Lemma heap_freeable_rel_init_mem l h n σ:
+    n ≠ O →
+    (∀ m : Z, σ !! (l +ₗ m) = None) →
     heap_freeable_rel σ h →
-    heap_freeable_rel (init_mem l vl σ)
-                      (<[l.1 := (1%Qp, inter (l.2) (length vl))]> h).
+    heap_freeable_rel (init_mem l n σ)
+                      (<[l.1 := (1%Qp, inter (l.2) n)]> h).
   Proof.
     move=> Hvlnil FRESH REL blk qs /lookup_insert_Some [[<- <-]|[??]].
     - split.
-      { destruct vl as [|v vl]; simpl in *; [done|]. apply: insert_non_empty. }
-      intros i. destruct (decide (l.2 ≤ i ∧ i < l.2 + length vl)).
-      + rewrite inter_lookup_Some //.
-        destruct (lookup_init_mem_Some σ l (l.1, i) vl); naive_solver.
+      { destruct n as [|n]; simpl in *; [done|]. apply: insert_non_empty. }
+      intros i. destruct (decide (l.2 ≤ i ∧ i < l.2 + n)).
+      + rewrite inter_lookup_Some // lookup_init_mem; naive_solver.
       + rewrite inter_lookup_None; last lia. rewrite lookup_init_mem_ne /=; last lia.
-        replace (l.1,i) with (shift_loc l (i - l.2))
-          by (rewrite /shift_loc; f_equal; lia).
+        replace (l.1,i) with (l +ₗ (i - l.2)) by (rewrite /shift_loc; f_equal; lia).
         by rewrite FRESH !is_Some_alt.
     - destruct (REL blk qs) as [? Hs]; auto.
       split; [done|]=> i. by rewrite -Hs lookup_init_mem_ne; last auto.
@@ -302,62 +341,60 @@ Section heap.
   Qed.
 
   (** Weakest precondition *)
-  Lemma heap_alloc_vs σ l vl:
-    (∀ m : Z, σ !! shift_loc l m = None) →
+  Lemma heap_alloc_vs σ l n :
+    (∀ m : Z, σ !! (l +ₗ m) = None) →
     own heap_name (● to_heap σ)
-    ==∗ own heap_name (● to_heap (init_mem l vl σ))
-       ∗ own heap_name (◯ [⋅ list] i ↦ v ∈ vl,
-           {[shift_loc l i := (1%Qp, Cinr 0%nat, to_agree v)]}).
+    ==∗ own heap_name (● to_heap (init_mem l n σ))
+       ∗ own heap_name (◯ [^op list] i ↦ v ∈ (repeat (LitV LitPoison) n),
+           {[l +ₗ i := (1%Qp, Cinr 0%nat, to_agree v)]}).
   Proof.
-    intros FREE. rewrite -own_op. apply own_update, auth_update_alloc.
-    revert l FREE. induction vl as [|v vl IH]=> l FRESH; [done|].
+    intros FREE. rewrite -own_op. apply entails_wand, own_update, auth_update_alloc.
+    revert l FREE. induction n as [|n IH]=> l FRESH; [done|].
     rewrite (big_opL_consZ_l (λ k _, _ (_ k) _ )) /=.
-    etrans; first apply (IH (shift_loc l 1)).
+    etrans; first apply (IH (l +ₗ 1)).
     { intros. by rewrite shift_loc_assoc. }
     rewrite shift_loc_0 -insert_singleton_op; last first.
-    { rewrite -equiv_None big_opL_commute equiv_None big_opL_None=> l' v' ?.
+    { rewrite -None_equiv_eq big_opL_commute None_equiv_eq big_opL_None=> l' v' ?.
       rewrite lookup_singleton_None -{2}(shift_loc_0 l). apply not_inj; lia. }
     rewrite to_heap_insert. setoid_rewrite shift_loc_assoc.
     apply alloc_local_update; last done. apply lookup_to_heap_None.
     rewrite lookup_init_mem_ne /=; last lia. by rewrite -(shift_loc_0 l) FRESH.
   Qed.
 
-  Lemma wp_alloc E n:
-    ↑heapN ⊆ E → 0 < n →
-    {{{ heap_ctx }}} Alloc (Lit $ LitInt n) @ E
-    {{{ l vl, RET LitV $ LitLoc l; ⌜n = length vl⌝ ∗ †l…(Z.to_nat n) ∗ l ↦∗ vl }}}.
+  Lemma heap_alloc σ l n :
+    0 < n →
+    (∀ m, σ !! (l +ₗ m) = None) →
+    heap_ctx σ ==∗
+      heap_ctx (init_mem l (Z.to_nat n) σ) ∗ †l…(Z.to_nat n) ∗
+      l ↦∗ repeat (LitV LitPoison) (Z.to_nat n).
   Proof.
-    iIntros (???) "#Hinv HΦ". rewrite /heap_ctx /heap_inv.
-    iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
-    iApply (wp_alloc_pst with "[$Hσ]")=> //.
-    iNext. iIntros (l σ') "(% & #Hσσ' & Hσ')".
-    iDestruct "Hσσ'" as %(vl & HvlLen & Hvl).
-    assert (vl ≠ []) by (intros ->; simpl in *; lia).
-    iMod (heap_alloc_vs with "[$Hvalσ]") as "[Hvalσ' Hmapsto]"; first done.
+    intros ??; iDestruct 1 as (hF) "(Hvalσ & HhF & %)".
+    assert (Z.to_nat n ≠ O). { rewrite -(Nat2Z.id 0)=>/Z2Nat.inj. lia. }
+    iMod (heap_alloc_vs _ _ (Z.to_nat n) with "[$Hvalσ]") as "[Hvalσ ?]"; first done.
     iMod (own_update _ (● hF) with "HhF") as "[HhF Hfreeable]".
     { apply auth_update_alloc,
         (alloc_singleton_local_update _ (l.1) (1%Qp, inter (l.2) (Z.to_nat n))).
       - eauto using heap_freeable_rel_None.
-      - split. done. apply inter_valid. }
-    iMod ("Hclose" with "[Hσ' Hvalσ' HhF]") as "_".
-    - iNext. iExists σ', _. subst σ'. iFrame. iPureIntro.
-      rewrite HvlLen Nat2Z.id. auto using heap_freeable_rel_init_mem.
-    - rewrite heap_freeable_eq /heap_freeable_def. iApply "HΦ".
-      iSplit; first auto. iFrame. by rewrite heap_mapsto_vec_combine.
-  Qed.
-
-  Lemma heap_free_vs l vl σ :
-    own heap_name (● to_heap σ) ∗ own heap_name (◯ [⋅ list] i ↦ v ∈ vl,
-      {[shift_loc l i := (1%Qp, Cinr 0%nat, to_agree v)]})
+      - split; first done. apply inter_valid. }
+    iModIntro. iSplitL "Hvalσ HhF".
+    { iExists _. iFrame. iPureIntro.
+      auto using heap_freeable_rel_init_mem. }
+    rewrite heap_freeable_eq /heap_freeable_def heap_pointsto_vec_combine //; last first.
+    { destruct (Z.to_nat n); done. }
+    iFrame. 
+  Qed.
+
+  Lemma heap_free_vs σ l vl :
+    own heap_name (● to_heap σ) ∗ own heap_name (◯ [^op list] i ↦ v ∈ vl,
+      {[l +ₗ i := (1%Qp, Cinr 0%nat, to_agree v)]})
     ==∗ own heap_name (● to_heap (free_mem l (length vl) σ)).
   Proof.
-    rewrite -own_op. apply own_update, auth_update_dealloc.
+    rewrite -own_op. apply entails_wand, own_update, auth_update_dealloc.
     revert σ l. induction vl as [|v vl IH]=> σ l; [done|].
     rewrite (big_opL_consZ_l (λ k _, _ (_ k) _ )) /= shift_loc_0.
     apply local_update_total_valid=> _ Hvalid _.
-    assert (([⋅ list] k↦y ∈ vl,
-      {[shift_loc l (1 + k) := (1%Qp, Cinr 0%nat, to_agree y)]}) !! l
-      = @None (frac * lock_stateR * agree valC)).
+    assert (([^op list] k↦y ∈ vl,
+      {[l +ₗ (1 + k) := (1%Qp, Cinr 0%nat, to_agree y)]} : heapUR) !! l = None).
     { move: (Hvalid l). rewrite lookup_op lookup_singleton.
       by move=> /(cmra_discrete_valid_iff 0) /exclusiveN_Some_l. }
     rewrite -insert_singleton_op //. etrans.
@@ -367,59 +404,58 @@ Section heap.
     setoid_rewrite <-shift_loc_assoc. apply IH.
   Qed.
 
-  Lemma wp_free E (n:Z) l vl :
-    ↑heapN ⊆ E → n = length vl →
-    {{{ heap_ctx ∗ ▷ l ↦∗ vl ∗ ▷ †l…(length vl) }}}
-      Free (Lit $ LitInt n) (Lit $ LitLoc l) @ E
-    {{{ RET LitV LitUnit; True }}}.
+  Lemma heap_free σ l vl (n : Z) :
+    n = length vl →
+    heap_ctx σ -∗ l ↦∗ vl -∗ †l…(length vl)
+    ==∗ ⌜0 < n⌝ ∗ ⌜∀ m, is_Some (σ !! (l +ₗ m)) ↔ (0 ≤ m < n)⌝ ∗
+        heap_ctx (free_mem l (Z.to_nat n) σ).
   Proof.
-    iIntros (???Φ) "(#Hinv & >Hmt & >Hf) HΦ". rewrite /heap_ctx /heap_inv.
-    iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & REL)" "Hclose". iDestruct "REL" as %REL.
-    rewrite heap_freeable_eq /heap_freeable_def.
-    iDestruct (own_valid_2 with "HhF Hf") as % [Hl Hv]%auth_valid_discrete_2.
-    move: Hl=> /singleton_included [[q qs] [/leibniz_equiv_iff Hl Hq]].
+    iDestruct 1 as (hF) "(Hvalσ & HhF & REL)"; iDestruct "REL" as %REL.
+    iIntros "Hmt Hf". rewrite heap_freeable_eq /heap_freeable_def.
+    iCombine "HhF Hf" gives % [Hl Hv]%auth_both_valid_discrete.
+    move: Hl=> /singleton_included_l [[q qs] [/leibniz_equiv_iff Hl Hq]].
     apply (Some_included_exclusive _ _) in Hq as [=<-<-]%leibniz_equiv; last first.
     { move: (Hv (l.1)). rewrite Hl. by intros [??]. }
     assert (vl ≠ []).
     { intros ->. by destruct (REL (l.1) (1%Qp, ∅)) as [[] ?]. }
     assert (0 < n) by (subst n; by destruct vl).
-    iApply (wp_free_pst _ σ with "[$Hσ]"). by auto.
-    { intros i. subst n. eauto using heap_freeable_is_Some. }
-    iNext. iIntros "Hσ". iMod (heap_free_vs with "[Hmt Hvalσ]") as "Hvalσ".
-    { rewrite heap_mapsto_vec_combine //. iFrame. }
+    iMod (heap_free_vs with "[Hmt Hvalσ]") as "Hvalσ".
+    { rewrite heap_pointsto_vec_combine //. iFrame. }
     iMod (own_update_2 with "HhF Hf") as "HhF".
     { apply auth_update_dealloc, (delete_singleton_local_update _ _ _). }
-    iMod ("Hclose" with "[-HΦ]") as "_"; last by iApply "HΦ".
-    iNext. iExists _, _. subst. rewrite Nat2Z.id. iFrame.
+    iModIntro; subst. repeat iSplit;  eauto using heap_freeable_is_Some.
+    iExists _. subst. rewrite Nat2Z.id. iFrame.
     eauto using heap_freeable_rel_free_mem.
   Qed.
 
-  Lemma heap_mapsto_lookup l ls q v σ:
+  Lemma heap_pointsto_lookup σ l ls q v :
     own heap_name (● to_heap σ) -∗
     own heap_name (◯ {[ l := (q, to_lock_stateR ls, to_agree v) ]}) -∗
     ⌜∃ n' : nat,
         σ !! l = Some (match ls with RSt n => RSt (n+n') | WSt => WSt end, v)⌝.
   Proof.
     iIntros "H● H◯".
-    iDestruct (own_valid_2 with "H● H◯") as %[Hl?]%auth_valid_discrete_2.
-    iPureIntro. move: Hl=> /singleton_included [[[q' ls'] dv]].
+    iCombine "H● H◯" gives %[Hl?]%auth_both_valid_discrete.
+    iPureIntro. move: Hl=> /singleton_included_l [[[q' ls'] dv]].
     rewrite /to_heap lookup_fmap fmap_Some_equiv.
     move=> [[[ls'' v'] [?[[/=??]->]]]]; simplify_eq.
     move=> /Some_pair_included_total_2
       [/Some_pair_included [_ Hincl] /to_agree_included->].
     destruct ls as [|n], ls'' as [|n''],
        Hincl as [[[|n'|]|] [=]%leibniz_equiv]; subst.
-    by exists O. eauto. exists O. by rewrite Nat.add_0_r.
+    - by exists O.
+    - eauto.
+    - exists O. by rewrite Nat.add_0_r.
   Qed.
 
-  Lemma heap_mapsto_lookup_1 l ls v σ:
+  Lemma heap_pointsto_lookup_1 σ l ls v :
     own heap_name (● to_heap σ) -∗
     own heap_name (◯ {[ l := (1%Qp, to_lock_stateR ls, to_agree v) ]}) -∗
     ⌜σ !! l = Some (ls, v)⌝.
   Proof.
     iIntros "H● H◯".
-    iDestruct (own_valid_2 with "H● H◯") as %[Hl?]%auth_valid_discrete_2.
-    iPureIntro. move: Hl=> /singleton_included [[[q' ls'] dv]].
+    iCombine "H● H◯" gives %[Hl?]%auth_both_valid_discrete.
+    iPureIntro. move: Hl=> /singleton_included_l [[[q' ls'] dv]].
     rewrite /to_heap lookup_fmap fmap_Some_equiv.
     move=> [[[ls'' v'] [?[[/=??]->]]] Hincl]; simplify_eq.
     apply (Some_included_exclusive _ _) in Hincl as [? Hval]; last by destruct ls''.
@@ -427,210 +463,94 @@ Section heap.
     destruct ls, ls''; rewrite ?Nat.add_0_r; naive_solver.
   Qed.
 
-  Lemma wp_read_sc E l q v :
-    ↑heapN ⊆ E →
-    {{{ heap_ctx ∗ ▷ l ↦{q} v }}} Read ScOrd (Lit $ LitLoc l) @ E
-    {{{ RET v; l ↦{q} v }}}.
-  Proof.
-    iIntros (??) "[#Hinv >Hv] HΦ".
-    rewrite /heap_ctx /heap_inv heap_mapsto_eq /heap_mapsto_def.
-    iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
-    iDestruct (heap_mapsto_lookup with "Hvalσ Hv") as %[n Hσl].
-    iApply (wp_read_sc_pst with "[$Hσ]"); first done. iNext. iIntros "Hσ".
-    iMod ("Hclose" with "[-Hv HΦ]"); last by iApply "HΦ".
-    iNext. iExists σ, hF. iFrame. eauto.
-  Qed.
-
   Lemma heap_read_vs σ n1 n2 nf l q v:
     σ !! l = Some (RSt (n1 + nf), v) →
-    own heap_name (● to_heap σ) ∗ heap_mapsto_st (RSt n1) l q v
+    own heap_name (● to_heap σ) -∗ heap_pointsto_st (RSt n1) l q v
     ==∗ own heap_name (● to_heap (<[l:=(RSt (n2 + nf), v)]> σ))
-        ∗ heap_mapsto_st (RSt n2) l q v.
+        ∗ heap_pointsto_st (RSt n2) l q v.
   Proof.
-    intros Hσv. rewrite -!own_op to_heap_insert.
-    eapply own_update, auth_update, singleton_local_update.
+    intros Hσv. apply entails_wand, wand_intro_r. rewrite -!own_op to_heap_insert.
+    iApply own_update. eapply auth_update, singleton_local_update.
     { by rewrite /to_heap lookup_fmap Hσv. }
     apply prod_local_update_1, prod_local_update_2, csum_local_update_r.
     apply nat_local_update; lia.
   Qed.
 
-  Lemma wp_read_na E l q v :
-    ↑heapN ⊆ E →
-    {{{ heap_ctx ∗ ▷ l ↦{q} v }}} Read Na1Ord (Lit $ LitLoc l) @ E
-    {{{ RET v; l ↦{q} v }}}.
-  Proof.
-    iIntros (??Φ) "[#Hinv >Hv] HΦ".
-    rewrite /heap_ctx /heap_inv heap_mapsto_eq /heap_mapsto_def.
-    iApply (wp_read_na1_pst E).
-    iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
-    iDestruct (heap_mapsto_lookup with "Hvalσ Hv") as %[n Hσl].
-    iMod (heap_read_vs _ 0 1 with "[$Hvalσ $Hv]") as "[Hvalσ Hv]"; first done.
-    iMod (fupd_intro_mask' (E∖↑heapN) ∅) as "Hclose'"; first set_solver.
-    iModIntro. iExists σ, n, v. iFrame. iSplit; [done|]. iIntros "!> Hσ".
-    iMod "Hclose'" as "_". iMod ("Hclose" with "[Hσ Hvalσ HhF]") as "_".
-    { iNext. iExists _, _. iFrame. eauto using heap_freeable_rel_stable. }
-    iModIntro. clear dependent n σ hF.
-    iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
-    iDestruct (heap_mapsto_lookup with "Hvalσ Hv") as %[n Hσl].
-    iApply (wp_read_na2_pst with "[$Hσ]"); first done. iNext. iIntros "Hσ".
-    iMod (heap_read_vs with "[$Hvalσ $Hv]") as "[Hvalσ Hv]"; first done.
-    iMod ("Hclose" with "[-Hv HΦ]") as "_"; last by iApply "HΦ".
-    iNext. iExists _, hF. iFrame. eauto using heap_freeable_rel_stable.
+  Lemma heap_read σ l q v :
+    heap_ctx σ -∗ l ↦{q} v -∗ ∃ n, ⌜σ !! l = Some (RSt n, v)⌝.
+  Proof.
+    iDestruct 1 as (hF) "(Hσ & HhF & REL)". iIntros "Hmt".
+    rewrite heap_pointsto_eq.
+    iDestruct (heap_pointsto_lookup with "Hσ Hmt") as %[n Hσl]; eauto.
+  Qed.
+
+  Lemma heap_read_1 σ l v :
+    heap_ctx σ -∗ l ↦ v -∗ ⌜σ !! l = Some (RSt 0, v)⌝.
+  Proof.
+    iDestruct 1 as (hF) "(Hσ & HhF & REL)". iIntros "Hmt".
+    rewrite heap_pointsto_eq.
+    iDestruct (heap_pointsto_lookup_1 with "Hσ Hmt") as %?; auto.
+  Qed.
+
+  Lemma heap_read_na σ l q v :
+    heap_ctx σ -∗ l ↦{q} v ==∗ ∃ n,
+      ⌜σ !! l = Some (RSt n, v)⌝ ∗
+      heap_ctx (<[l:=(RSt (S n), v)]> σ) ∗
+      ∀ σ2, heap_ctx σ2 ==∗ ∃ n2, ⌜σ2 !! l = Some (RSt (S n2), v)⌝ ∗
+        heap_ctx (<[l:=(RSt n2, v)]> σ2) ∗ l ↦{q} v.
+  Proof.
+    iDestruct 1 as (hF) "(Hσ & HhF & %)"; iIntros "Hmt".
+    rewrite heap_pointsto_eq.
+    iDestruct (heap_pointsto_lookup with "Hσ Hmt") as %[n Hσl]; eauto.
+    iMod (heap_read_vs _ 0 1 with "Hσ Hmt") as "[Hσ Hmt]"; first done.
+    iModIntro. iExists n; iSplit; [done|]. iSplitL "HhF Hσ".
+    { iExists hF. iFrame. eauto using heap_freeable_rel_stable. }
+    clear dependent n σ hF. iIntros (σ2). iDestruct 1 as (hF) "(Hσ & HhF & %)".
+    iDestruct (heap_pointsto_lookup with "Hσ Hmt") as %[n Hσl]; eauto.
+    iMod (heap_read_vs _ 1 0 with "Hσ Hmt") as "[Hσ Hmt]"; first done.
+    iExists n; iModIntro; iSplit; [done|]. iFrame "Hmt".
+    iExists hF. iFrame. eauto using heap_freeable_rel_stable.
   Qed.
 
   Lemma heap_write_vs σ st1 st2 l v v':
     σ !! l = Some (st1, v) →
-    own heap_name (● to_heap σ) ∗ heap_mapsto_st st1 l 1%Qp v
+    own heap_name (● to_heap σ) -∗ heap_pointsto_st st1 l 1%Qp v
     ==∗ own heap_name (● to_heap (<[l:=(st2, v')]> σ))
-        ∗ heap_mapsto_st st2 l 1%Qp v'.
+        ∗ heap_pointsto_st st2 l 1%Qp v'.
   Proof.
-    intros Hσv. rewrite -!own_op to_heap_insert.
-    eapply own_update, auth_update, singleton_local_update.
+    intros Hσv. apply entails_wand, wand_intro_r. rewrite -!own_op to_heap_insert.
+    iApply own_update. eapply auth_update, singleton_local_update.
     { by rewrite /to_heap lookup_fmap Hσv. }
     apply exclusive_local_update. by destruct st2.
   Qed.
 
-  Lemma wp_write_sc E l e v v' :
-    ↑heapN ⊆ E → to_val e = Some v →
-    {{{ heap_ctx ∗ ▷ l ↦ v' }}} Write ScOrd (Lit $ LitLoc l) e @ E
-    {{{ RET LitV LitUnit; l ↦ v }}}.
-  Proof.
-    iIntros (? <-%of_to_val?) "[#Hinv >Hv] HΦ".
-    rewrite /heap_ctx /heap_inv heap_mapsto_eq /heap_mapsto_def.
-    iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
-    iDestruct (heap_mapsto_lookup_1 with "Hvalσ Hv") as %?.
-    iApply (wp_write_sc_pst with "[$Hσ]"); [done|]. iNext. iIntros "Hσ".
-    iMod (heap_write_vs with "[$Hvalσ $Hv]") as "[Hvalσ Hv]"; first done.
-    iMod ("Hclose" with "[-Hv HΦ]") as "_"; last by iApply "HΦ".
-    iNext. iExists _, hF. iFrame. eauto using heap_freeable_rel_stable.
-  Qed.
-
-  Lemma wp_write_na E l e v v' :
-    ↑heapN ⊆ E → to_val e = Some v →
-    {{{ heap_ctx ∗ ▷ l ↦ v' }}} Write Na1Ord (Lit $ LitLoc l) e @ E
-    {{{ RET LitV LitUnit; l ↦ v }}}.
-  Proof.
-    iIntros (? <-%of_to_val?) "[#Hinv >Hv] HΦ".
-    rewrite /heap_ctx /heap_inv heap_mapsto_eq /heap_mapsto_def.
-    iApply (wp_write_na1_pst E).
-    iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
-    iDestruct (heap_mapsto_lookup_1 with "Hvalσ Hv") as %?.
-    iMod (heap_write_vs with "[$Hvalσ $Hv]") as "[Hvalσ Hv]"; first done.
-    iMod (fupd_intro_mask' (E∖↑heapN) ∅) as "Hclose'"; first set_solver.
-    iModIntro. iExists σ, v'. iSplit; [done|]. iIntros "{$Hσ} !> Hσ".
-    iMod "Hclose'" as "_". iMod ("Hclose" with "[Hσ Hvalσ HhF]") as "_".
-    { iNext. iExists _, _. iFrame. eauto using heap_freeable_rel_stable. }
-    iModIntro. clear dependent σ hF.
-    iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
-    iDestruct (heap_mapsto_lookup_1 with "Hvalσ Hv") as %?.
-    iApply (wp_write_na2_pst with "[$Hσ]"); [done|]. iNext. iIntros "Hσ".
-    iMod (heap_write_vs with "[$Hvalσ $Hv]") as "[Hvalσ Hv]"; first done.
-    iMod ("Hclose" with "[-Hv HΦ]"); last by iApply "HΦ".
-    iNext. iExists _, hF. iFrame. eauto using heap_freeable_rel_stable.
-  Qed.
-
-  Lemma wp_cas_int_fail E l q z1 e2 lit2 zl :
-    ↑heapN ⊆ E → to_val e2 = Some $ LitV lit2 → z1 ≠ zl →
-    {{{ heap_ctx ∗ ▷ l ↦{q} (LitV $ LitInt zl) }}}
-      CAS (Lit $ LitLoc l) (Lit $ LitInt z1) e2 @ E
-    {{{ RET LitV $ LitInt 0; l ↦{q} (LitV $ LitInt zl) }}}.
-  Proof.
-    iIntros (? <-%of_to_val ??) "[#Hinv >Hv] HΦ".
-    rewrite /heap_ctx /heap_inv heap_mapsto_eq /heap_mapsto_def.
-    iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
-    iDestruct (heap_mapsto_lookup with "Hvalσ Hv") as %[n Hσl].
-    iApply (wp_cas_pst with "[$Hσ]"); eauto.
-    { right. by constructor. }
-    { inversion 1. done. }
-    iNext. iIntros ([|]).
-    { iIntros "[Heq _]". iDestruct "Heq" as %Heq. inversion Heq. done. }
-    iIntros "[_ Hσ]". iMod ("Hclose" with "[-Hv HΦ]") as "_"; last by iApply "HΦ".
-    iNext. iExists _, hF. iFrame. eauto using heap_freeable_rel_stable.
-  Qed.
-
-  Lemma wp_cas_int_suc E l z1 e2 lit2 :
-    ↑heapN ⊆ E → to_val e2 = Some $ LitV lit2 →
-    {{{ heap_ctx ∗ ▷ l ↦ (LitV $ LitInt z1) }}}
-      CAS (Lit $ LitLoc l) (Lit $ LitInt z1) e2 @ E
-    {{{ RET LitV $ LitInt 1; l ↦ LitV lit2 }}}.
-  Proof.
-    iIntros (? <-%of_to_val?) "[#Hinv >Hv] HΦ".
-    rewrite /heap_ctx /heap_inv heap_mapsto_eq /heap_mapsto_def.
-    iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
-    iDestruct (heap_mapsto_lookup_1 with "Hvalσ Hv") as %?.
-    iApply (wp_cas_pst with "[$Hσ]"); eauto.
-    { left. by constructor. }
-    iNext. iIntros ([|]); last first.
-    { iIntros "[Hneq _]". iDestruct "Hneq" as %Hneq. inversion Hneq. done. }
-    iIntros "[_ Hσ]". iMod (heap_write_vs with "[$Hvalσ $Hv]") as "[Hvalσ Hv]"; first done.
-    iMod ("Hclose" with "[-Hv HΦ]"); last by iApply "HΦ"; iFrame.
-    iNext. iExists _, hF. iFrame. eauto using  heap_freeable_rel_stable.
-  Qed.
-
-  Lemma wp_cas_loc_fail E l q q' q1 l1 v1' e2 lit2 l' vl' :
-    ↑heapN ⊆ E → to_val e2 = Some $ LitV lit2 → l1 ≠ l' →
-    {{{ heap_ctx ∗ ▷ l ↦{q} (LitV $ LitLoc l') ∗ ▷ l' ↦{q'} vl' ∗ ▷ l1 ↦{q1} v1' }}}
-      CAS (Lit $ LitLoc l) (Lit $ LitLoc l1) e2 @ E
-    {{{ RET LitV $ LitInt 0;
-        l ↦{q} (LitV $ LitLoc l') ∗ l' ↦{q'} vl' ∗ l1 ↦{q1} v1' }}}.
-  Proof.
-    iIntros (? <-%of_to_val ??) "(#Hinv & >Hl & >Hl' & >Hl1) HΦ".
-    rewrite /heap_ctx /heap_inv heap_mapsto_eq /heap_mapsto_def.
-    iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
-    iDestruct (heap_mapsto_lookup with "Hvalσ Hl") as %[n Hσl].
-    iDestruct (heap_mapsto_lookup with "Hvalσ Hl'") as %[n' Hσl'].
-    iDestruct (heap_mapsto_lookup with "Hvalσ Hl1") as %[n1 Hσl1].
-    iApply (wp_cas_pst with "[$Hσ]"); eauto.
-    { right. by constructor. }
-    { inversion 1; subst; (by destruct (σ !! l1)) || by destruct (σ !! l'). }
-    iNext. iIntros ([|]).
-    { iIntros "[Heq _]". iDestruct "Heq" as %Heq. inversion Heq; subst.
-      done. by destruct (σ !! l1). by destruct (σ !! l'). }
-    iIntros "[_ Hσ]". iMod ("Hclose" with "[-Hl Hl' Hl1 HΦ]") as "_"; last by iApply "HΦ"; iFrame.
-    iNext. iExists _, hF. by iFrame.
-  Qed.
-
-  Lemma wp_cas_loc_suc E l l1 e2 lit2 :
-    ↑heapN ⊆ E → to_val e2 = Some $ LitV lit2 →
-    {{{ heap_ctx ∗ ▷ l ↦ (LitV $ LitLoc l1) }}}
-      CAS (Lit $ LitLoc l) (Lit $ LitLoc l1) e2 @ E
-    {{{ RET LitV $ LitInt 1; l ↦ LitV lit2 }}}.
-  Proof.
-    iIntros (? <-%of_to_val?) "[#Hinv >Hv] HΦ".
-    rewrite /heap_ctx /heap_inv heap_mapsto_eq /heap_mapsto_def.
-    iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
-    iDestruct (heap_mapsto_lookup_1 with "Hvalσ Hv") as %?.
-    iApply (wp_cas_pst with "[$Hσ]"); eauto.
-    { left. by constructor. }
-    iNext. iIntros ([|]); last first.
-    { iIntros "[Hneq _]". iDestruct "Hneq" as %Hneq. inversion Hneq. done. }
-    iIntros "[_ Hσ]". iMod (heap_write_vs with "[$Hvalσ $Hv]") as "[Hvalσ Hv]"; first done.
-    iMod ("Hclose" with "[-Hv HΦ]"); last by iApply "HΦ"; iFrame.
-    iNext. iExists _, hF. iFrame. eauto using  heap_freeable_rel_stable.
-  Qed.
-
-  Lemma wp_cas_loc_nondet E l l1 e2 l2 ll :
-    ↑heapN ⊆ E → to_val e2 = Some $ LitV $ LitLoc l2 →
-    {{{ heap_ctx ∗ ▷ l ↦ (LitV $ LitLoc ll) }}}
-      CAS (Lit $ LitLoc l) (Lit $ LitLoc l1) e2 @ E
-    {{{ b, RET LitV $ lit_of_bool b;
-        if b is true then l ↦ LitV (LitLoc l2)
-        else ⌜l1 ≠ ll⌝ ∗ l ↦ LitV (LitLoc ll) }}}.
-  Proof.
-    iIntros (? <-%of_to_val?) "[#Hinv >Hv] HΦ".
-    rewrite /heap_ctx /heap_inv heap_mapsto_eq /heap_mapsto_def.
-    iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
-    iDestruct (heap_mapsto_lookup_1 with "Hvalσ Hv") as %?.
-    iApply (wp_cas_pst with "[$Hσ]"); eauto.
-    { destruct (decide (l1 = ll)) as [->|Hne].
-      - left. by constructor.
-      - right. by constructor. }
-    iNext. iIntros ([|]).
-    - iIntros "[_ Hσ]". iMod (heap_write_vs with "[$Hvalσ $Hv]") as "[Hvalσ Hv]"; first done.
-      iMod ("Hclose" with "[-Hv HΦ]"); last by iApply "HΦ"; iFrame.
-      iNext. iExists _, hF. iFrame. eauto using  heap_freeable_rel_stable.
-    - iIntros "[Hneq Hσ]". iDestruct "Hneq" as %Hneq. inversion_clear Hneq.
-      iMod ("Hclose" with "[-Hv HΦ]"); last by iApply ("HΦ" $! false); iFrame.
-      iNext. iExists _, hF. iFrame. eauto using  heap_freeable_rel_stable.
+  Lemma heap_write σ l v v' :
+    heap_ctx σ -∗ l ↦ v ==∗ heap_ctx (<[l:=(RSt 0, v')]> σ) ∗ l ↦ v'.
+  Proof.
+    iDestruct 1 as (hF) "(Hσ & HhF & %)". iIntros "Hmt".
+    rewrite heap_pointsto_eq.
+    iDestruct (heap_pointsto_lookup_1 with "Hσ Hmt") as %?; auto.
+    iMod (heap_write_vs with "Hσ Hmt") as "[Hσ $]"; first done.
+    iModIntro. iExists _. iFrame. eauto using heap_freeable_rel_stable.
+  Qed.
+
+  Lemma heap_write_na σ l v v' :
+    heap_ctx σ -∗ l ↦ v ==∗
+      ⌜σ !! l = Some (RSt 0, v)⌝ ∗
+      heap_ctx (<[l:=(WSt, v)]> σ) ∗
+      ∀ σ2, heap_ctx σ2 ==∗ ⌜σ2 !! l = Some (WSt, v)⌝ ∗
+        heap_ctx (<[l:=(RSt 0, v')]> σ2) ∗ l ↦ v'.
+  Proof.
+    iDestruct 1 as (hF) "(Hσ & HhF & %)"; iIntros "Hmt".
+    rewrite heap_pointsto_eq.
+    iDestruct (heap_pointsto_lookup_1 with "Hσ Hmt") as %?; eauto.
+    iMod (heap_write_vs with "Hσ Hmt") as "[Hσ Hmt]"; first done.
+    iModIntro. iSplit; [done|]. iSplitL "HhF Hσ".
+    { iExists hF. iFrame. eauto using heap_freeable_rel_stable. }
+    clear dependent σ hF. iIntros (σ2). iDestruct 1 as (hF) "(Hσ & HhF & %)".
+    iDestruct (heap_pointsto_lookup with "Hσ Hmt") as %[n Hσl]; eauto.
+    iMod (heap_write_vs with "Hσ Hmt") as "[Hσ Hmt]"; first done.
+    iModIntro; iSplit; [done|]. iFrame "Hmt".
+    iExists hF. iFrame. eauto using heap_freeable_rel_stable.
   Qed.
 End heap.

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

 From iris.program_logic Require Export language ectx_language ectxi_language.
-From iris.prelude Require Export strings.
-From iris.prelude Require Import gmap.
+From stdpp Require Export strings binders.
+From stdpp Require Import gmap.
+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.
+Global Open Scope loc_scope.
+
 Inductive base_lit : Set :=
-| LitUnit | LitLoc (l : loc) | LitInt (n : Z).
+| LitPoison | LitLoc (l : loc) | LitInt (n : Z).
 Inductive bin_op : Set :=
 | PlusOp | MinusOp | LeOp | EqOp | OffsetOp.
 Inductive order : Set :=
 | ScOrd | Na1Ord | Na2Ord.
 
-Inductive binder := BAnon | BNamed : string → binder.
-Delimit Scope lrust_binder_scope with RustB.
-Bind Scope lrust_binder_scope with binder.
-
-Definition cons_binder (mx : binder) (X : list string) : list string :=
-  match mx with BAnon => X | BNamed x => x :: X end.
-Infix ":b:" := cons_binder (at level 60, right associativity).
-Fixpoint app_binder (mxl : list binder) (X : list string) : list string :=
-  match mxl with [] => X | b :: mxl => b :b: app_binder mxl X end.
-Infix "+b+" := app_binder (at level 60, right associativity).
-Instance binder_dec_eq : EqDecision binder.
-Proof. solve_decision. Defined.
-
-Instance set_unfold_cons_binder x mx X P :
-  SetUnfold (x ∈ X) P → SetUnfold (x ∈ mx :b: X) (BNamed x = mx ∨ P).
-Proof.
-  constructor. rewrite -(set_unfold (x ∈ X) P).
-  destruct mx; rewrite /= ?elem_of_cons; naive_solver.
-Qed.
-Instance set_unfold_app_binder x mxl X P :
-  SetUnfold (x ∈ X) P → SetUnfold (x ∈ mxl +b+ X) (BNamed x ∈ mxl ∨ P).
-Proof.
-  constructor. rewrite -(set_unfold (x ∈ X) P).
-  induction mxl as [|?? IH]; set_solver.
-Qed.
+Notation "[ ]" := (@nil binder) : binder_scope.
+Notation "a :: b" := (@cons binder a%binder b%binder)
+  (at level 60, right associativity) : binder_scope.
+Notation "[ x1 ; x2 ; .. ; xn ]" :=
+  (@cons binder x1%binder (@cons binder x2%binder
+        (..(@cons binder xn%binder (@nil binder))..))) : binder_scope.
+Notation "[ x ]" := (@cons binder x%binder (@nil binder)) : binder_scope.
 
 Inductive expr :=
 | Var (x : string)
@@ -55,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
@@ -71,20 +59,20 @@ 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 :=
 | LitV (l : base_lit)
-| RecV (f : binder) (xl : list binder) (e : expr) `{Closed (f :b: xl +b+ []) e}.
+| RecV (f : binder) (xl : list binder) (e : expr) `{!Closed (f :b: xl +b+ []) e}.
 
 Bind Scope val_scope with val.
 
 Definition of_val (v : val) : expr :=
   match v with
-  | RecV f x e _ => Rec f x e
+  | RecV f x e => Rec f x e
   | LitV l => Lit l
   end.
 
@@ -123,7 +111,7 @@ Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
   | BinOpLCtx op e2 => BinOp op e e2
   | BinOpRCtx op v1 => BinOp op (of_val v1) e
   | AppLCtx e2 => App e e2
-  | AppRCtx v vl el => App (of_val v) (map of_val vl ++ e :: el)
+  | AppRCtx v vl el => App (of_val v) ((of_val <$> vl) ++ e :: el)
   | ReadCtx o => Read o e
   | WriteLCtx o e2 => Write o e e2
   | WriteRCtx o v1 => Write o (of_val v1) e
@@ -156,34 +144,61 @@ Fixpoint subst (x : string) (es : expr) (e : expr)  : expr :=
 
 Definition subst' (mx : binder) (es : expr) : expr → expr :=
   match mx with BNamed x => subst x es | BAnon => id end.
+
 Fixpoint subst_l (xl : list binder) (esl : list expr) (e : expr) : option expr :=
   match xl, esl with
   | [], [] => Some e
-  | x::xl, es::esl => subst_l xl esl (subst' x es e)
+  | x::xl, es::esl => subst' x es <$> subst_l xl esl e
   | _, _ => None
   end.
+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.
+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 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 lit_of_bool (b : bool) : base_lit :=
-  LitInt (if b then 1 else 0).
+  LitInt $ Z.b2z b.
 
 Definition shift_loc (l : loc) (z : Z) : loc := (l.1, l.2 + z).
 
-Fixpoint init_mem (l:loc) (init:list val) (σ:state) : state :=
-  match init with
-  | [] => σ
-  | inith :: initq => <[l:=(RSt 0, inith)]>(init_mem (shift_loc l 1) initq σ)
+Notation "l +ₗ z" := (shift_loc l%L z%Z)
+  (at level 50, left associativity) : loc_scope.
+
+Fixpoint init_mem (l:loc) (n:nat) (σ:state) : state :=
+  match n with
+  | O => σ
+  | S n => <[l:=(RSt 0, LitV LitPoison)]>(init_mem (l +ₗ 1) n σ)
   end.
 
 Fixpoint free_mem (l:loc) (n:nat) (σ:state) : state :=
   match n with
   | O => σ
-  | S n => delete l (free_mem (shift_loc l 1) n σ)
+  | S n => delete l (free_mem (l +ₗ 1) n σ)
   end.
 
 Inductive lit_eq (σ : state) : base_lit → base_lit → Prop :=
+(* No refl case for poison *)
 | IntRefl z : lit_eq σ (LitInt z) (LitInt z)
 | LocRefl l : lit_eq σ (LitLoc l) (LitLoc l)
+(* Comparing unallocated pointers can non-deterministically say they are equal
+   even if they are not.  Given that our `free` actually makes addresses
+   re-usable, this may not be strictly necessary, but it is the most
+   conservative choice that avoids UB (and we cannot use UB as this operation is
+   possible in safe Rust).  See
+   <https://internals.rust-lang.org/t/comparing-dangling-pointers/3019> for some
+   more background. *)
 | LocUnallocL l1 l2 :
     σ !! l1 = None →
     lit_eq σ (LitLoc l1) (LitLoc l2)
@@ -191,11 +206,15 @@ Inductive lit_eq (σ : state) : base_lit → base_lit → Prop :=
     σ !! l2 = None →
     lit_eq σ (LitLoc l1) (LitLoc l2).
 
-Inductive lit_neq (σ : state) : base_lit → base_lit → Prop :=
+Inductive lit_neq : base_lit → base_lit → Prop :=
 | IntNeq z1 z2 :
-    z1 ≠ z2 → lit_neq σ (LitInt z1) (LitInt z2)
+    z1 ≠ z2 → lit_neq (LitInt z1) (LitInt z2)
 | LocNeq l1 l2 :
-    l1 ≠ l2 → lit_neq σ (LitLoc l1) (LitLoc l2).
+    l1 ≠ l2 → lit_neq (LitLoc l1) (LitLoc l2)
+| LocNeqNullR l :
+    lit_neq (LitLoc l) (LitInt 0)
+| LocNeqNullL l :
+    lit_neq (LitInt 0) (LitLoc l).
 
 Inductive bin_op_eval (σ : state) : bin_op → base_lit → base_lit → base_lit → Prop :=
 | BinOpPlus z1 z2 :
@@ -207,89 +226,112 @@ Inductive bin_op_eval (σ : state) : bin_op → base_lit → base_lit → base_l
 | BinOpEqTrue l1 l2 :
     lit_eq σ l1 l2 → bin_op_eval σ EqOp l1 l2 (lit_of_bool true)
 | BinOpEqFalse l1 l2 :
-    lit_neq σ l1 l2 → bin_op_eval σ EqOp l1 l2 (lit_of_bool false)
+    lit_neq l1 l2 → bin_op_eval σ EqOp l1 l2 (lit_of_bool false)
 | BinOpOffset l z :
-    bin_op_eval σ OffsetOp (LitLoc l) (LitInt z) (LitLoc $ shift_loc l z).
+    bin_op_eval σ OffsetOp (LitLoc l) (LitInt z) (LitLoc $ l +ₗ z).
 
 Definition stuck_term := App (Lit $ LitInt 0) [].
 
-Inductive head_step : expr → state → 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 xl el e = Some e' →
-    head_step (App (Rec f xl e) el) σ (subst' f (Rec f xl e) e') σ []
+    subst_l (f::xl) (Rec f xl e :: el) e = Some 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) σ
-              (Lit LitUnit) (<[l:=(RSt 0, v)]>σ)
+    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) σ
-              (Lit LitUnit) (<[l:=(RSt 0, v)]>σ)
+    base_step (Write Na2Ord (Lit $ LitLoc l) e) σ
+              []
+              (Lit LitPoison) (<[l:=(RSt 0, v)]>σ)
               []
 | CasFailS l n e1 lit1 e2 lit2 litl σ :
     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) σ  []
+    lit_neq lit1 litl →
+    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)]>σ)
               []
+(* A succeeding CAS has to detect concurrent non-atomic read accesses, and
+   trigger UB if there is one.  In lambdaRust, succeeding and failing CAS are
+   not mutually exclusive, so it could happen that a CAS can both fail (and
+   hence not be stuck) but also succeed (and hence be racing with a concurrent
+   non-atomic read).  In that case, we have to explicitly reduce to a stuck
+   state; due to the possibility of failing CAS, we cannot rely on the current
+   state being stuck like we could in a language where failing and succeeding
+   CAS are mutually exclusive.
+
+   This means that CAS is atomic (it always reducs to an irreducible
+   expression), but not strongly atomic (it does not always reduce to a value).
+
+   If there is a concurrent non-atomic write, the CAS itself is stuck: All its
+   reductions are blocked.  *)
 | CasStuckS l n e1 lit1 e2 lit2 litl σ :
     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 init σ :
+| AllocS n l σ :
     0 < n →
-    (∀ m, σ !! shift_loc l m = None) →
-    Z.of_nat (length init) = n →
-    head_step (Alloc $ Lit $ LitInt n) σ
-              (Lit $ LitLoc l) (init_mem l init σ) []
+    (∀ m, σ !! (l +ₗ m) = None) →
+    base_step (Alloc $ Lit $ LitInt n) σ
+              []
+              (Lit $ LitLoc l) (init_mem l (Z.to_nat n) σ)
+              []
 | FreeS n l σ :
     0 < n →
-    (∀ m, is_Some (σ !! shift_loc l m) ↔ 0 ≤ m < n) →
-    head_step (Free (Lit $ LitInt n) (Lit $ LitLoc l)) σ
-              (Lit LitUnit) (free_mem l (Z.to_nat n) σ)
+    (∀ m, is_Some (σ !! (l +ₗ m)) ↔ 0 ≤ m < n) →
+    base_step (Free (Lit $ LitInt n) (Lit $ LitLoc l)) σ
+              []
+              (Lit LitPoison) (free_mem l (Z.to_nat n) σ)
               []
 | CaseS i el e σ :
     0 ≤ i →
-    nth_error el (Z.to_nat i) = Some e →
-    head_step (Case (Lit $ LitInt i) el) σ e σ []
+    el !! (Z.to_nat i) = Some e →
+    base_step (Case (Lit $ LitInt i) el) σ [] e σ []
 | ForkS e σ:
-    head_step (Fork e) σ (Lit LitUnit) σ [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.
@@ -302,22 +344,22 @@ 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 :
   is_Some (to_val (fill_item Ki e)) → is_Some (to_val 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.
+Lemma val_stuck e1 σ1 κ e2 σ2 ef :
+  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.
@@ -328,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.
@@ -348,68 +391,54 @@ Proof.
   destruct (list_expr_val_eq_inv vl1 vl2 e1 e2 el1 el2); auto. congruence.
 Qed.
 
-Lemma shift_loc_assoc l n n' :
-  shift_loc (shift_loc l n) n' = shift_loc l (n+n').
+Lemma shift_loc_assoc l n n' : l +ₗ n +ₗ n' = l +ₗ (n + n').
 Proof. rewrite /shift_loc /=. f_equal. lia. Qed.
-Lemma shift_loc_0 l : shift_loc l 0 = l.
+Lemma shift_loc_0 l : l +ₗ 0 = l.
 Proof. destruct l as [b o]. rewrite /shift_loc /=. f_equal. lia. Qed.
 
-Lemma shift_loc_assoc_nat l (n n' : nat) :
-  shift_loc (shift_loc l n) n' = shift_loc l (n+n')%nat.
+Lemma shift_loc_assoc_nat l (n n' : nat) : l +ₗ n +ₗ n' = l +ₗ (n + n')%nat.
 Proof. rewrite /shift_loc /=. f_equal. lia. Qed.
-Lemma shift_loc_0_nat l : shift_loc l 0%nat = l.
+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 : (shift_loc l n).1 = l.1.
+Lemma shift_loc_block l n : (l +ₗ n).1 = l.1.
 Proof. done. Qed.
 
-Lemma lookup_init_mem σ (l l' : loc) vl :
-  l.1 = l'.1 → l.2 ≤ l'.2 < l.2 + length vl →
-  init_mem l vl σ !! l' = (RSt 0,) <$> vl !! Z.to_nat (l'.2 - l.2).
+Lemma lookup_init_mem σ (l l' : loc) (n : nat) :
+  l.1 = l'.1 → l.2 ≤ l'.2 < l.2 + n →
+  init_mem l n σ !! l' = Some (RSt 0, LitV LitPoison).
 Proof.
-  intros ?. destruct l' as [? n]; simplify_eq/=.
-  revert n l. induction vl as [|v vl IH]=> /= n l Hl; [lia|].
-  assert (n = l.2 ∨ l.2 + 1 ≤ n) as [->|?] by lia.
-  { by rewrite -surjective_pairing lookup_insert Z.sub_diag. }
+  intros ?. destruct l' as [? l']; simplify_eq/=.
+  revert l. induction n as [|n IH]=> /= l Hl; [lia|].
+  assert (l' = l.2 ∨ l.2 + 1 ≤ l') as [->|?] by lia.
+  { by rewrite -surjective_pairing lookup_insert. }
   rewrite lookup_insert_ne; last by destruct l; intros ?; simplify_eq/=; lia.
-  rewrite -(shift_loc_block l 1) IH /=; last lia.
-  cut (Z.to_nat (n - l.2) = S (Z.to_nat (n - (l.2 + 1)))); [by intros ->|].
-  rewrite -Z2Nat.inj_succ; last lia. f_equal; lia.
-Qed.
-
-Lemma lookup_init_mem_Some σ (l l' : loc) vl :
-  l.1 = l'.1 → l.2 ≤ l'.2 < l.2 + length vl → ∃ v,
-  vl !! Z.to_nat (l'.2 - l.2) = Some v ∧
-  init_mem l vl σ !! l' = Some (RSt 0,v).
-Proof.
-  intros. destruct (lookup_lt_is_Some_2 vl (Z.to_nat (l'.2 - l.2))) as [v Hv].
-  { rewrite -(Nat2Z.id (length vl)). apply Z2Nat.inj_lt; lia. }
-  exists v. by rewrite lookup_init_mem ?Hv.
+  rewrite -(shift_loc_block l 1) IH /=; last lia. done.
 Qed.
 
-Lemma lookup_init_mem_ne σ (l l' : loc) vl :
-  l.1 ≠ l'.1 ∨ l'.2 < l.2 ∨ l.2 + length vl ≤ l'.2 →
-  init_mem l vl σ !! l' = σ !! l'.
+Lemma lookup_init_mem_ne σ (l l' : loc) (n : nat) :
+  l.1 ≠ l'.1 ∨ l'.2 < l.2 ∨ l.2 + n ≤ l'.2 →
+  init_mem l n σ !! l' = σ !! l'.
 Proof.
-  revert l. induction vl as [|v vl IH]=> /= l Hl; auto.
-  rewrite -(IH (shift_loc l 1)); last (simpl; intuition lia).
+  revert l. induction n as [|n IH]=> /= l Hl; auto.
+  rewrite -(IH (l +ₗ 1)); last (simpl; intuition lia).
   apply lookup_insert_ne. intros ->; intuition lia.
 Qed.
 
 Definition fresh_block (σ : state) : block :=
-  let loclst : list loc := elements (dom _ σ : gset loc) in
-  let blockset : gset block := foldr (λ l, ({[l.1]} ∪)) ∅ loclst in
+  let loclst : list loc := elements (dom σ : gset loc) in
+  let blockset : gset block := foldr (λ l, ({[l.1]} ∪.)) ∅ loclst in
   fresh blockset.
 
 Lemma is_fresh_block σ i : σ !! (fresh_block σ,i) = None.
 Proof.
   assert (∀ (l : loc) ls (X : gset block),
-    l ∈ ls → l.1 ∈ foldr (λ l, ({[l.1]} ∪)) X ls) as help.
+    l ∈ ls → l.1 ∈ foldr (λ l, ({[l.1]} ∪.)) X ls) as help.
   { induction 1; set_solver. }
-  rewrite /fresh_block /shift_loc /= -not_elem_of_dom -elem_of_elements.
+  rewrite /fresh_block /shift_loc /= -(not_elem_of_dom (D := gset loc)) -elem_of_elements.
   move=> /(help _ _ ∅) /=. apply is_fresh.
 Qed.
 
@@ -417,11 +446,10 @@ 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 init σ) [].
+  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).
-  - rewrite repeat_length Z2Nat.id; lia.
 Qed.
 
 Lemma lookup_free_mem_ne σ l l' n : l.1 ≠ l'.1 → free_mem l n σ !! l' = σ !! l'.
@@ -440,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 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.
 
@@ -453,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 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.
 
@@ -468,35 +502,54 @@ Proof. intros. apply is_closed_subst with []; set_solver. Qed.
 Lemma is_closed_of_val X v : is_closed X (of_val v).
 Proof. apply is_closed_weaken_nil. induction v; simpl; auto. Qed.
 
+Lemma is_closed_to_val X e v : to_val e = Some v → is_closed X e.
+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; 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.
+    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 :
+  is_closed X es → is_closed (b:b:X) e → is_closed X (subst' b es e).
+Proof. destruct b; first done. apply subst_is_closed. Qed.
+
 (* Operations on literals *)
 Lemma lit_eq_state σ1 σ2 l1 l2 :
   (∀ l, σ1 !! l = None ↔ σ2 !! l = None) →
   lit_eq σ1 l1 l2 → lit_eq σ2 l1 l2.
 Proof. intros Heq. inversion 1; econstructor; eauto; eapply Heq; done. Qed.
 
-Lemma lit_neq_state σ1 σ2 l1 l2 :
-  (∀ l, σ1 !! l = None ↔ σ2 !! l = None) →
-  lit_neq σ1 l1 l2 → lit_neq σ2 l1 l2.
-Proof. intros Heq. inversion 1; econstructor; eauto; eapply Heq; done. Qed.
-
 Lemma bin_op_eval_state σ1 σ2 op l1 l2 l' :
   (∀ l, σ1 !! l = None ↔ σ2 !! l = None) →
   bin_op_eval σ1 op l1 l2 l' → bin_op_eval σ2 op l1 l2 l'.
 Proof.
-  intros Heq. inversion 1; econstructor; eauto using lit_eq_state, lit_neq_state.
+  intros Heq. inversion 1; econstructor; eauto using lit_eq_state.
 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 :=
@@ -527,56 +580,65 @@ 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 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 ?expr_beq_correct;
+  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.
-      specialize (expr_beq_correct el1h). naive_solver. }
-    clear expr_beq_correct. naive_solver.
+    { 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.
-      specialize (expr_beq_correct el1h). naive_solver. }
-    clear expr_beq_correct. naive_solver.
+    { 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 LitUnit).
-Instance val_inhabited : Inhabited val := populate (LitV LitUnit).
+Global Instance expr_inhabited : Inhabited expr := populate (Lit LitPoison).
+Global Instance val_inhabited : Inhabited val := populate (LitV LitPoison).
 
-Canonical Structure stateC := leibnizC state.
-Canonical Structure valC := leibnizC val.
-Canonical Structure exprC := leibnizC expr.
+Canonical Structure stateO := leibnizO state.
+Canonical Structure valO := leibnizO val.
+Canonical Structure exprO := leibnizO expr.
 
 (** Language *)
-Program Instance lrust_ectxi_lang: EctxiLanguage expr val ectx_item state :=
-  {| ectxi_language.of_val := of_val;
-     ectxi_language.to_val := to_val;
-     ectxi_language.fill_item := fill_item;
-     ectxi_language.head_step := head_step |}.
-Solve Obligations with eauto using to_of_val, of_to_val,
-  val_stuck, fill_item_val, fill_item_no_val_inj, head_ctx_step_val.
-
-Canonical Structure lrust_lang := ectx_lang expr.
+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, base_ctx_step_val.
+Qed.
+Canonical Structure lrust_ectxi_lang := EctxiLanguage lrust_lang_mixin.
+Canonical Structure lrust_ectx_lang := EctxLanguageOfEctxi lrust_ectxi_lang.
+Canonical Structure lrust_lang := LanguageOfEctx lrust_ectx_lang.
 
 (* Lemmas about the language. *)
 Lemma stuck_irreducible K σ : irreducible (fill K stuck_term) σ.
 Proof.
-  intros ??? Hstep. edestruct step_is_head as (?&?&?&?); [..|by do 3 eexists|].
-  - done.
-  - clear. intros Ki K e' Heq (?&?&? & Hstep). destruct Ki; inversion Heq.
-    + destruct K as [|Ki K].
-      * simpl in *. subst. inversion Hstep.
-      * destruct Ki; simpl in *; done.
-    + destruct (map of_val vl); last done. destruct (fill K e'); done.
-  - by eapply stuck_not_head_step.
+  apply: (irreducible_fill (K:=ectx_language.fill K)); first done.
+  apply prim_base_irreducible; unfold stuck_term.
+  - inversion 1.
+  - apply ectxi_language_sub_redexes_are_values.
+    intros [] ??; simplify_eq/=; eauto; discriminate_list.
 Qed.
+
+(* Define some derived forms *)
+Notation Lam xl e := (Rec BAnon xl e) (only parsing).
+Notation Let x e1 e2 := (App (Lam [x] e2) [e1]) (only parsing).
+Notation Seq e1 e2 := (Let BAnon e1 e2) (only parsing).
+Notation LamV xl e := (RecV BAnon xl e) (only parsing).
+Notation LetCtx x e2 := (AppRCtx (LamV [x] e2) [] []).
+Notation SeqCtx e2 := (LetCtx BAnon e2).
+Notation Skip := (Seq (Lit LitPoison) (Lit LitPoison)).
+Coercion lit_of_bool : bool >-> base_lit.
+Notation If e0 e1 e2 := (Case e0 (@cons expr e2 (@cons expr e1 (@nil expr)))) (only parsing).
+Notation Newlft := (Lit LitPoison) (only parsing).
+Notation Endlft := Skip (only parsing).

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 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.
+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
+not be necessary.
+
+Instead, what can be done in get_mut is the following:
+  - First, do a CAS on the strong count to put it to 0 from the expected
+value 1. This has the effect, at the same time, of ensuring that no one
+else has a strong reference, and of forbidding other weak references to
+be upgraded (since the strong count is now at 0). If the CAS fail,
+simply return None.
+  - Second, check the weak count. If it is at 1, then we are sure that
+we are the only owner.
+  - Third, in any case write 1 in the strong count to cancel the CAS.
+
+What's wrong with this protocol? The "only" problem I can see is that if
+someone tries to upgrade a weak after we did the CAS, then this will
+fail even though this could be possible.
+
+RJ: Upgrade failing spuriously sounds like a problem severe enough to
+justify the locking protocol.
+*)
+
+Definition strong_count : val :=
+  λ: ["l"], !ˢᶜ"l".
+
+Definition weak_count : val :=
+  λ: ["l"], !ˢᶜ("l" +ₗ #1).
+
+Definition clone_arc : val :=
+  rec: "clone" ["l"] :=
+    let: "strong" := !ˢᶜ"l" in
+    if: CAS "l" "strong" ("strong" + #1) then #☠ else "clone" ["l"].
+
+Definition clone_weak : val :=
+  rec: "clone" ["l"] :=
+    let: "weak" := !ˢᶜ("l" +ₗ #1) in
+    if: CAS ("l" +ₗ #1) "weak" ("weak" + #1) then #☠ else "clone" ["l"].
+
+Definition downgrade : val :=
+  rec: "downgrade" ["l"] :=
+    let: "weak" := !ˢᶜ("l" +ₗ #1) in
+    if: "weak" = #(-1) then
+      (* -1 in weak indicates that somebody locked the counts; let's spin. *)
+      "downgrade" ["l"]
+    else
+      if: CAS ("l" +ₗ #1) "weak" ("weak" + #1) then #☠
+      else "downgrade" ["l"].
+
+Definition upgrade : val :=
+  rec: "upgrade" ["l"] :=
+    let: "strong" := !ˢᶜ"l" in
+    if: "strong" = #0 then #false
+    else
+      if: CAS "l" "strong" ("strong" + #1) then #true
+      else "upgrade" ["l"].
+
+Definition drop_weak : val :=
+  rec: "drop" ["l"] :=
+    (* This can ignore the lock because the lock is only held when there
+       are no other weak refs in existence, so this code will never be called
+       with the lock held. *)
+    let: "weak" := !ˢᶜ("l" +ₗ #1) in
+    if: CAS ("l" +ₗ #1) "weak" ("weak" - #1) then "weak" = #1
+    else "drop" ["l"].
+
+Definition drop_arc : val :=
+  rec: "drop" ["l"] :=
+    let: "strong" := !ˢᶜ"l" in
+    if: CAS "l" "strong" ("strong" - #1) then "strong" = #1
+    else "drop" ["l"].
+
+Definition try_unwrap : val :=
+  λ: ["l"], CAS "l" #1 #0.
+
+Definition is_unique : val :=
+  λ: ["l"],
+    (* Try to acquire the lock for the last ref by CASing weak count from 1 to -1. *)
+    if: CAS ("l" +ₗ #1) #1 #(-1) then
+      let: "strong" := !ˢᶜ"l" in
+      let: "unique" := "strong" = #1 in
+      "l" +ₗ #1 <-ˢᶜ #1;;
+      "unique"
+    else
+      #false.
+
+Definition try_unwrap_full : val :=
+  λ: ["l"],
+    if: CAS "l" #1 #0 then
+      if: !ˢᶜ("l" +ₗ #1) = #1 then "l" <- #1;; #0
+      else #1
+    else #2.
+
+(** The CMRA we need. *)
+(* Not bundling heapGS, as it may be shared with other users. *)
+
+(* See rc.v for understanding the structure of this CMRA.
+   The only additional thing is the [optionR (exclR unitO))], used to handle
+   properly the locking mechanisme for the weak count. *)
+Definition arc_stR :=
+  prodUR (optionUR (csumR (prodR (prodR fracR positiveR) (optionR (exclR unitO)))
+                          (exclR unitO))) natUR.
+Class arcG Σ :=
+  RcG :: inG Σ (authR arc_stR).
+Definition arcΣ : gFunctors := #[GFunctor (authR arc_stR)].
+Global Instance subG_arcΣ {Σ} : subG arcΣ Σ → arcG Σ.
+Proof. solve_inG. Qed.
+
+Section def.
+  Context `{!lrustGS Σ, !arcG Σ} (P1 : Qp → iProp Σ) (P2 : iProp Σ) (N : namespace).
+
+  Definition arc_tok γ q : iProp Σ :=
+    own γ (◯ (Some $ Cinl (q, 1%positive, None), 0%nat)).
+  Definition weak_tok γ : iProp Σ :=
+    own γ (◯ (None, 1%nat)).
+
+  Global Instance arc_tok_timeless γ q : Timeless (arc_tok γ q) := _.
+  Global Instance weak_tok_timeless γ : Timeless (weak_tok γ) := _.
+
+  Definition arc_inv (γ : gname) (l : loc) : iProp Σ :=
+    (∃ st : arc_stR, own γ (● st) ∗
+      match st with
+      | (Some (Cinl (q, strong, wlock)), weak) =>
+         ∃ q', ⌜(q + q')%Qp = 1%Qp⌝ ∗ P1 q' ∗ l ↦ #(Zpos strong) ∗
+           if wlock then (l +ₗ 1) ↦ #(-1) ∗ ⌜weak = 0%nat⌝
+           else (l +ₗ 1) ↦ #(S weak)
+      | (Some (Cinr _), weak) =>
+        l ↦ #0 ∗ (l +ₗ 1) ↦ #(S weak)
+      | (None, (S _) as weak) =>
+        l ↦ #0 ∗ (l +ₗ 1) ↦ #weak ∗ P2
+      | _ => True
+      end)%I.
+
+  Definition is_arc (γ : gname) (l : loc) : iProp Σ :=
+    inv N (arc_inv γ l).
+
+  Global Instance is_arc_persistent γ l : Persistent (is_arc γ l) := _.
+
+  Definition arc_tok_acc (γ : gname) P E : iProp Σ :=
+    (□ (P ={E,∅}=∗ ∃ q, arc_tok γ q ∗ (arc_tok γ q ={∅,E}=∗ P)))%I.
+
+  Definition weak_tok_acc (γ : gname) P E : iProp Σ :=
+    (□ (P ={E,∅}=∗ weak_tok γ ∗ (weak_tok γ ={∅,E}=∗ P)))%I.
+
+  Definition drop_spec (drop : val) P : iProp Σ :=
+    ({{{ P ∗ P1 1 }}} drop [] {{{ RET #☠; P ∗ P2 }}})%I.
+End def.
+
+Section arc.
+  (* P1 is the thing that is shared by strong reference owners (in practice,
+     this is the lifetime token), and P2 is the thing that is owned by the
+     protocol when only weak references are left (in practice, P2 is the
+     ownership of the underlying memory incl. deallocation). *)
+  Context `{!lrustGS Σ, !arcG Σ} (P1 : Qp → iProp Σ) {HP1:Fractional P1}
+          (P2 : iProp Σ) (N : namespace).
+
+  Local Instance P1_AsFractional q : AsFractional (P1 q) P1 q.
+  Proof using HP1. done. Qed.
+
+  Global Instance arc_inv_ne n :
+    Proper (pointwise_relation _ (dist n) ==> dist n ==> eq ==> eq ==> dist n)
+           arc_inv.
+  Proof. solve_proper. Qed.
+  Global Instance arc_inv_proper :
+    Proper (pointwise_relation _ (≡) ==> (≡) ==> eq ==> eq ==> (≡))
+           arc_inv.
+  Proof. solve_proper. Qed.
+
+  Global Instance is_arc_contractive n :
+    Proper (pointwise_relation _ (dist_later n) ==> dist_later n ==> eq ==> eq ==> eq ==> dist n)
+           is_arc.
+  Proof. solve_contractive. Qed.
+  Global Instance is_arc_proper :
+    Proper (pointwise_relation _ (≡) ==> (≡) ==> eq ==> eq ==> eq ==> (≡)) is_arc.
+  Proof. solve_proper. Qed.
+
+  Lemma create_arc E l :
+    l ↦ #1 -∗ (l +ₗ 1) ↦ #1 -∗ P1 1%Qp ={E}=∗
+      ∃ γ q, is_arc P1 P2 N γ l ∗ P1 q ∗ arc_tok γ q.
+  Proof using HP1.
+    iIntros "Hl1 Hl2 [HP1 HP1']".
+    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.
+    iFrame. iApply inv_alloc. iExists _. iFrame.
+    rewrite Qp.div_2. auto.
+  Qed.
+
+  Lemma create_weak E l :
+    l ↦ #0 -∗ (l +ₗ 1) ↦ #1 -∗ P2 ={E}=∗ ∃ γ, is_arc P1 P2 N γ l ∗ weak_tok γ.
+  Proof.
+    iIntros "Hl1 Hl2 HP2".
+    iMod (own_alloc ((● (None, 1%nat) ⋅ ◯ (None, 1%nat)))) as (γ) "[H● H◯]";
+      first by apply auth_both_valid_discrete.
+    iExists _. iFrame. iApply inv_alloc. iExists _. iFrame.
+  Qed.
+
+  Lemma arc_tok_auth_val st γ q :
+    own γ (● st) -∗ arc_tok γ q -∗
+    ⌜∃ q' strong wlock weak, st = (Some $ Cinl (q', strong, wlock), weak) ∧
+                             if decide (strong = xH) then q = q' ∧ wlock = None
+                             else ∃ q'', q' = (q + q'')%Qp⌝.
+  Proof.
+    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
+        ?%pos_included]%prod_included _]%prod_included)|(?&?&[=]&?)]]; first done.
+      iExists _, _, _, _. iSplit=>//. simpl in *. destruct decide; [subst;lia|eauto].
+  Qed.
+
+  Lemma strong_count_spec (γ : gname) (l : loc) (P : iProp Σ) :
+    is_arc P1 P2 N γ l -∗ arc_tok_acc γ P (⊤ ∖ ↑N) -∗
+    {{{ P }}} strong_count [ #l] {{{ (c : nat), RET #c; P ∗ ⌜(c > 0)%nat⌝ }}}.
+  Proof using HP1.
+    iIntros "#INV #Hacc !> * HP HΦ". iLöb as "IH". wp_rec.
+    iInv N as (st) "[>H● H]" "Hclose1".
+    iMod ("Hacc" with "HP") as (?) "[Hown Hclose2]".
+    iDestruct (arc_tok_auth_val with "H● Hown") as %(?& strong &?&?&[-> _]).
+    iDestruct "H" as (?) "(Hq & HP1 & H↦ & Hw)". wp_read.
+    iMod ("Hclose2" with "Hown") as "HP". iModIntro.
+    iMod ("Hclose1" with "[-HP HΦ]") as "_"; [iExists _; auto with iFrame|].
+    iModIntro. rewrite -positive_nat_Z. iApply "HΦ". auto with iFrame lia.
+  Qed.
+
+  (* FIXME : in the case the weak count is locked, we can possibly
+     return -1. This problem already exists in Rust. *)
+  Lemma weak_count_spec (γ : gname) (l : loc) (P : iProp Σ) :
+    is_arc P1 P2 N γ l -∗ arc_tok_acc γ P (⊤ ∖ ↑N) -∗
+    {{{ P }}} weak_count [ #l] {{{ (c : Z), RET #c; P ∗ ⌜c >= -1⌝ }}}.
+  Proof using HP1.
+    iIntros "#INV #Hacc !> * HP HΦ". iLöb as "IH". wp_rec. wp_op.
+    iInv N as (st) "[>H● H]" "Hclose1".
+    iMod ("Hacc" with "HP") as (?) "[Hown Hclose2]".
+    iDestruct (arc_tok_auth_val with "H● Hown") as %(?& strong &wl&?&[-> _]).
+    iDestruct "H" as (?) "(Hq & HP1 & H↦ & Hw)". destruct wl.
+    - iDestruct "Hw" as ">[Hw %]". wp_read.
+      iMod ("Hclose2" with "Hown") as "HP". iModIntro.
+      iMod ("Hclose1" with "[-HP HΦ]") as "_"; [iExists _; auto with iFrame|].
+      iApply "HΦ". auto with iFrame lia.
+    - wp_read. iMod ("Hclose2" with "Hown") as "HP". iModIntro.
+      iMod ("Hclose1" with "[-HP HΦ]") as "_"; [iExists _; auto with iFrame|].
+      iApply "HΦ". auto with iFrame lia.
+  Qed.
+
+  Lemma clone_arc_spec (γ : gname) (l : loc) (P : iProp Σ) :
+    is_arc P1 P2 N γ l -∗ arc_tok_acc γ P (⊤ ∖ ↑N) -∗
+    {{{ P }}} clone_arc [ #l]
+    {{{ q', RET #☠; P ∗ arc_tok γ q' ∗ P1 q' }}}.
+  Proof using HP1.
+    iIntros "#INV #Hacc !> * HP HΦ". iLöb as "IH". wp_rec. wp_bind (!ˢᶜ_)%E.
+    iInv N as (st) "[>H● H]" "Hclose1".
+    iMod ("Hacc" with "HP") as (?) "[Hown Hclose2]".
+    iDestruct (arc_tok_auth_val with "H● Hown") as %(?& strong &?&?&[-> _]).
+    iDestruct "H" as (?) "(Hq & HP1 & H↦ & Hw)". wp_read.
+    iMod ("Hclose2" with "Hown") as "HP". iModIntro.
+    iMod ("Hclose1" with "[-HP HΦ]") as "_"; [iExists _; auto with iFrame|].
+    iModIntro. wp_let. wp_op. wp_bind (CAS _ _ _). iInv N as (st) "[>H● H]" "Hclose1".
+    iMod ("Hacc" with "HP") as (?) "[Hown Hclose2]".
+    iDestruct (arc_tok_auth_val with "H● Hown") as %(?&strong'&?&?&[-> _]).
+    iDestruct "H" as (qq) "(>#Hq & [HP1 HP1'] & Hl & Hw)". iDestruct "Hq" as %Hq.
+    destruct (decide (strong = strong')) as [->|?].
+    - wp_apply (wp_cas_int_suc with "Hl"). iIntros "Hl".
+      iMod (own_update with "H●") as "[H● Hown']".
+      { apply auth_update_alloc, prod_local_update_1,
+         (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. }
+      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. }
+      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. iCombine "HP1 HP1'" as "$". auto with iFrame. }
+      iModIntro. wp_case. iApply ("IH" with "HP HΦ").
+  Qed.
+
+  Lemma downgrade_spec (γ : gname) (l : loc) (P : iProp Σ) :
+    is_arc P1 P2 N γ l -∗ arc_tok_acc γ P (⊤ ∖ ↑N) -∗
+    {{{ P }}} downgrade [ #l] {{{ RET #☠; P ∗ weak_tok γ }}}.
+  Proof.
+    iIntros "#INV #Hacc !> * HP HΦ". iLöb as "IH". wp_rec. wp_op. wp_bind (!ˢᶜ_)%E.
+    iInv N as (st) "[>H● H]" "Hclose1".
+    iApply fupd_wp. iMod ("Hacc" with "HP") as (?) "[Hown Hclose2]".
+    iDestruct (arc_tok_auth_val with "H● Hown") as %(?&?& wlock & weak &[-> _]).
+    iMod ("Hclose2" with "Hown") as "HP". iModIntro.
+    iDestruct "H" as (?) "(? & ? & ? & Hw)". destruct wlock.
+    { iDestruct "Hw" as "(Hw & >%)". subst. wp_read.
+      iMod ("Hclose1" with "[-HP HΦ]") as "_"; first by iExists _; auto with iFrame.
+      iModIntro. wp_let. wp_op. wp_if. iApply ("IH" with "HP HΦ"). }
+    wp_read. iMod ("Hclose1" with "[-HP HΦ]") as "_"; first by iExists _; auto with iFrame.
+    iModIntro. wp_let. wp_op. wp_if. wp_op. wp_op. wp_bind (CAS _ _ _).
+    iInv N as (st) "[>H● H]" "Hclose1".
+    iApply fupd_wp. iMod ("Hacc" with "HP") as (?) "[Hown Hclose2]".
+    iDestruct (arc_tok_auth_val with "H● Hown") as %(?&?& wlock & weak' &[-> _]).
+    iMod ("Hclose2" with "Hown") as "HP". iModIntro.
+    iDestruct "H" as (qq) "(>Heq & HP1 & Hl & Hl1)". iDestruct "Heq" as %Heq.
+    destruct (decide (weak = weak' ∧ wlock = None)) as [[<- ->]|Hw].
+    - wp_apply (wp_cas_int_suc with "Hl1"). iIntros "Hl1".
+      iMod (own_update with "H●") as "[H● Hown']".
+      { by apply auth_update_alloc, prod_local_update_2,
+              (op_local_update_discrete _ _ (1%nat)). }
+      iMod ("Hclose1" with "[-Hown' HP HΦ]") as "_".
+      { iExists _. iFrame.
+        rewrite Z.add_comm -(Nat2Z.inj_add 1) /=. auto with iFrame. }
+      iModIntro. wp_case. iApply "HΦ". iFrame.
+    - destruct wlock.
+      + iDestruct "Hl1" as "[Hl1 >%]". subst.
+        wp_apply (wp_cas_int_fail with "Hl1"); [done..|].
+        iIntros "Hl1". iMod ("Hclose1" with "[-HP HΦ]") as "_".
+        { iExists _. auto with iFrame. }
+        iModIntro. wp_case. iApply ("IH" with "HP HΦ").
+      + wp_apply (wp_cas_int_fail with "Hl1").
+        { contradict Hw. split=>//. apply SuccNat2Pos.inj. lia. }
+        iIntros "Hl1". iMod ("Hclose1" with "[-HP HΦ]") as "_".
+        { iExists _. auto with iFrame. }
+        iModIntro. wp_case. iApply ("IH" with "HP HΦ").
+  Qed.
+
+  Lemma weak_tok_auth_val γ st :
+    own γ (● st) -∗ weak_tok γ -∗ ⌜∃ st' weak, st = (st', S weak) ∧ ✓ st'⌝.
+  Proof.
+    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.
+  Qed.
+
+  Lemma clone_weak_spec (γ : gname) (l : loc) (P : iProp Σ) :
+    is_arc P1 P2 N γ l -∗ weak_tok_acc γ P (⊤ ∖ ↑N) -∗
+    {{{ P }}} clone_weak [ #l] {{{ RET #☠; P ∗ weak_tok γ }}}.
+  Proof.
+    iIntros "#INV #Hacc !> * HP HΦ". iLöb as "IH". wp_rec. wp_op. wp_bind (!ˢᶜ_)%E.
+    iAssert (□ (P ={⊤,⊤∖↑N}=∗ ∃ w : Z, (l +ₗ 1) ↦ #w ∗
+              ((l +ₗ 1) ↦ #(w + 1) ={⊤∖↑N,⊤}=∗ P ∗ weak_tok γ) ∧
+              ((l +ₗ 1) ↦ #w ={⊤∖↑N,⊤}=∗ P)))%I as "#Hproto".
+    { 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).
+      iMod ("Hclose2" with "Hown") as "HP".
+      destruct st' as [[[[??][?|]]| |]|]; try done; [|iExists _..].
+      - by iDestruct "H" as (?) "(_ & _ & _ & _ & >%)".
+      - iDestruct "H" as (?) "(? & ? & ? & >$)". iIntros "!>"; iSplit; iIntros "?".
+        + iMod (own_update with "H●") as "[H● $]".
+          { by apply auth_update_alloc, prod_local_update_2,
+                  (op_local_update_discrete _ _ (1%nat)). }
+          rewrite Z.add_comm -(Nat2Z.inj_add 1). iFrame.
+          iApply "Hclose1". iExists _. auto with iFrame.
+        + iFrame. iApply ("Hclose1" with "[-]"). iExists _. auto with iFrame.
+      - iDestruct "H" as "[? >$]". iIntros "!>"; iSplit; iIntros "?".
+        + iMod (own_update with "H●") as "[H● $]".
+          { by apply auth_update_alloc, prod_local_update_2,
+                  (op_local_update_discrete _ _ (1%nat)). }
+          rewrite Z.add_comm -(Nat2Z.inj_add 1). iFrame. iApply "Hclose1".
+          iExists _. auto with iFrame.
+        + iFrame. iApply ("Hclose1" with "[-]"). iExists _. auto with iFrame.
+      - iDestruct "H" as "(? & >$ & ?)". iIntros "!>"; iSplit; iIntros "?".
+        + iMod (own_update with "H●") as "[H● $]".
+          { by apply auth_update_alloc, prod_local_update_2,
+                  (op_local_update_discrete _ _ (1%nat)). }
+          rewrite Z.add_comm -(Nat2Z.inj_add 1). iFrame. iApply "Hclose1".
+          iExists _. auto with iFrame.
+        + iFrame. iApply ("Hclose1" with "[-]"). iExists _. auto with iFrame. }
+    iMod ("Hproto" with "HP") as (w) "[Hw [_ Hclose]]". wp_read.
+    iMod ("Hclose" with "Hw") as "HP". iModIntro. wp_let. wp_op. wp_op.
+    wp_bind (CAS _ _ _). iMod ("Hproto" with "HP") as (w') "[H↦ Hclose]".
+    destruct (decide (w = w')) as [<-|].
+    - wp_apply (wp_cas_int_suc with "H↦"). iIntros "H↦".
+      iDestruct "Hclose" as "[Hclose _]". iMod ("Hclose" with "H↦"). iModIntro.
+      wp_case. by iApply "HΦ".
+    - wp_apply (wp_cas_int_fail with "H↦"); try done. iIntros "H↦".
+      iDestruct "Hclose" as "[_ Hclose]". iMod ("Hclose" with "H↦") as "Hown".
+      iModIntro. wp_case. by iApply ("IH" with "Hown").
+  Qed.
+
+  Lemma upgrade_spec (γ : gname) (l : loc) (P : iProp Σ) :
+    is_arc P1 P2 N γ l -∗ weak_tok_acc γ P (⊤ ∖ ↑N) -∗
+    {{{ P }}} upgrade [ #l]
+    {{{ (b : bool) q, RET #b; P ∗ if b then arc_tok γ q ∗ P1 q else True }}}.
+  Proof using HP1.
+    iIntros "#INV #Hacc !> * HP HΦ". iLöb as "IH". wp_rec. wp_bind (!ˢᶜ_)%E.
+    iAssert (□ (P ={⊤,∅}=∗ ∃ s : Z, l ↦ #s ∗
+              (⌜s ≠ 0⌝ -∗ l ↦ #(s + 1) ={∅,⊤}=∗ ∃ q, P ∗ arc_tok γ q ∗ ▷ P1 q) ∧
+              (l ↦ #s ={∅,⊤}=∗ P)))%I as "#Hproto".
+    { 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 [[[[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● $]".
+          { apply auth_update_alloc. rewrite -[(_,0%nat)]right_id.
+            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.
+          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. 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.
+      - iDestruct "H" as "[>$ ?]". iIntros "!>"; iSplit; first by auto with congruence.
+        iIntros "Hl". iMod ("Hclose2" with "Hown") as "$". iApply "Hclose1".
+        iExists _. auto with iFrame. }
+    iMod ("Hproto" with "HP") as (s) "[Hs [_ Hclose]]". wp_read.
+    iMod ("Hclose" with "Hs") as "HP". iModIntro. wp_let. wp_op; wp_if; case_bool_decide.
+    - iApply wp_value. iApply ("HΦ" $! _ 1%Qp). auto.
+    - wp_op. wp_bind (CAS _ _ _). iMod ("Hproto" with "HP") as (s') "[H↦ Hclose]".
+      destruct (decide (s = s')) as [<-|].
+      + wp_apply (wp_cas_int_suc with "H↦"). iIntros "H↦".
+        iDestruct "Hclose" as "[Hclose _]".
+        iMod ("Hclose" with "[//] H↦") as (q) "(?&?&?)". iModIntro.
+        wp_case. iApply "HΦ". iFrame.
+      + wp_apply (wp_cas_int_fail with "H↦"); try done. iIntros "H↦".
+        iDestruct "Hclose" as "[_ Hclose]". iMod ("Hclose" with "H↦") as "Hown".
+        iModIntro. wp_case. by iApply ("IH" with "Hown").
+  Qed.
+
+  Lemma drop_weak_spec (γ : gname) (l : loc) :
+    is_arc P1 P2 N γ l -∗
+    {{{ weak_tok γ }}} drop_weak [ #l]
+    {{{ (b : bool), RET #b ; if b then P2 ∗ l ↦ #0 ∗ (l +ₗ 1) ↦ #0 else True }}}.
+  Proof.
+    iIntros "#INV !> * Hown HΦ". iLöb as "IH". wp_rec. wp_op. wp_bind (!ˢᶜ_)%E.
+    iAssert (□ (weak_tok γ ={⊤,⊤ ∖ ↑N}=∗ ∃ w : Z, (l +ₗ 1) ↦ #w ∗
+              ((l +ₗ 1) ↦ #(w - 1) ={⊤ ∖ ↑N,⊤}=∗ ⌜w ≠ 1⌝ ∨
+               ▷ P2 ∗ l ↦ #0 ∗ (l +ₗ 1) ↦ #0) ∧
+              ((l +ₗ 1) ↦ #w ={⊤ ∖ ↑N,⊤}=∗ weak_tok γ)))%I as "#Hproto".
+    { iIntros "!> Hown". iInv N as (st) "[>H● H]" "Hclose1".
+      iDestruct (weak_tok_auth_val with "H● Hown") as %(st' & weak & -> & Hval).
+      destruct st' as [[[[??][?|]]| |]|]; try done; [|iExists _..].
+      - by iDestruct "H" as (?) "(_ & _ & _ & _ & >%)".
+      - iDestruct "H" as (q) "(>Heq & HP1 & ? & >$)". iIntros "!>"; iSplit; iIntros "Hl1".
+        + iMod ("Hclose1" with "[>-]") as "_"; last iLeft; auto with lia.
+          iExists _. iMod (own_update_2 with "H● Hown") as "$".
+          { apply auth_update_dealloc, prod_local_update_2,
+                  (cancel_local_update_unit 1%nat), _. }
+          iExists _. iFrame. by replace (S (S weak) - 1) with (S weak:Z) by lia.
+        + iFrame. iApply "Hclose1". iExists _. auto with iFrame.
+      - iDestruct "H" as "[? >$]". iIntros "!>"; iSplit; iIntros "Hl1".
+        + iMod ("Hclose1" with "[>-]") as "_"; last iLeft; auto with lia.
+          iExists _. iMod (own_update_2 with "H● Hown") as "$".
+          { apply auth_update_dealloc, prod_local_update_2,
+                  (cancel_local_update_unit 1%nat), _. }
+          iFrame. by replace (S (S weak) - 1) with (S weak:Z) by lia.
+        + iFrame. iApply "Hclose1". iExists _. auto with iFrame.
+      - iDestruct "H" as "(>? & >$ & HP2)". iIntros "!>"; iSplit; iIntros "Hl1".
+        + iMod (own_update_2 with "H● Hown") as "H●".
+          { apply auth_update_dealloc, prod_local_update_2,
+                  (cancel_local_update_unit 1%nat), _. }
+          destruct weak as [|weak].
+          * iMod ("Hclose1" with "[H●]") as "_"; last by auto with iFrame.
+            iExists _. iFrame.
+          * iMod ("Hclose1" with "[>-]") as "_"; last iLeft; auto with lia.
+            iExists _. iFrame. by replace (S (S weak) - 1) with (S weak:Z) by lia.
+        + iFrame. iApply "Hclose1". iExists _. auto with iFrame. }
+    iMod ("Hproto" with "Hown") as (w) "[Hw [_ Hclose]]". wp_read.
+    iMod ("Hclose" with "Hw") as "Hown". iModIntro. wp_let. wp_op. wp_op.
+    wp_bind (CAS _ _ _).
+    iMod ("Hproto" with "Hown") as (w') "[Hw Hclose]". destruct (decide (w = w')) as [<-|?].
+    - wp_apply (wp_cas_int_suc with "Hw"). iIntros "Hw".
+      iDestruct "Hclose" as "[Hclose _]". iMod ("Hclose" with "Hw") as "HP2". iModIntro.
+      wp_case. wp_op; case_bool_decide; subst; iApply "HΦ"=>//.
+      by iDestruct "HP2" as "[%|$]".
+    - wp_apply (wp_cas_int_fail with "Hw"); try done. iIntros "Hw".
+      iDestruct "Hclose" as "[_ Hclose]". iMod ("Hclose" with "Hw") as "Hown".
+      iModIntro. wp_case. by iApply ("IH" with "Hown").
+  Qed.
+
+  Lemma close_last_strong γ l :
+    is_arc P1 P2 N γ l -∗ own γ (◯ (Some (Cinr (Excl ())), 0%nat)) -∗ P2
+    ={⊤}=∗ weak_tok γ.
+  Proof.
+    iIntros "INV H◯ HP2". iInv N as ([st ?]) "[>H● H]" "Hclose".
+    iDestruct (own_valid_2 with "H● H◯")
+      as %[[[[=]|Hincl]%option_included _]%prod_included [? _]]%auth_both_valid_discrete.
+    simpl in Hincl. destruct Hincl as (?&?&[=<-]&->&[?|[]%exclusive_included]);
+        try done; try apply _. setoid_subst.
+    iMod (own_update_2 with "H● H◯") as "[H● $]".
+    { apply auth_update, prod_local_update', (op_local_update _ _ 1%nat)=>//.
+      apply delete_option_local_update, _. }
+    iApply "Hclose". iExists _. by iFrame.
+  Qed.
+
+  Lemma drop_arc_spec (γ : gname) (q: Qp) (l : loc) :
+    is_arc P1 P2 N γ l -∗
+    {{{ arc_tok γ q ∗ P1 q }}} drop_arc  [ #l]
+    {{{ (b : bool), RET #b ; if b then P1 1 ∗ (P2 ={⊤}=∗ weak_tok γ) else True }}}.
+  Proof using HP1.
+    iIntros "#INV !> * [Hown HP1] HΦ". iLöb as "IH".
+    wp_rec. wp_bind (!ˢᶜ_)%E. iInv N as (st) "[>H● H]" "Hclose".
+    iDestruct (arc_tok_auth_val with "H● Hown") as %(?& s &?&?&[-> _]).
+    iDestruct "H" as (x') "(? & ? & ? & ?)". wp_read.
+    iMod ("Hclose" with "[-Hown HP1 HΦ]") as "_". { iExists _. auto with iFrame. }
+    iModIntro. wp_let. wp_op. wp_bind (CAS _ _ _). iInv N as (st) "[>H● H]" "Hclose".
+    iDestruct (arc_tok_auth_val with "H● Hown") as %(q' & s' & wl & w &[-> Hqq']).
+    iDestruct "H" as (q'') "(>Hq'' & HP1' & Hs & Hw)". iDestruct "Hq''" as %Hq''.
+    destruct (decide (s = s')) as [<-|?].
+    - wp_apply (wp_cas_int_suc with "Hs"). iIntros "Hs".
+      destruct decide as [->|?].
+      + destruct Hqq' as [<- ->].
+        iMod (own_update_2 with "H● Hown") as "[H● H◯]".
+        { apply auth_update, prod_local_update_1. rewrite -[x in (x, _)]right_id.
+          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.
+        iModIntro. wp_case. iApply wp_fupd. wp_op.
+        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 _. 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".
+      iSpecialize ("IH" with "Hown HP1 HΦ").
+      iMod ("Hclose" with "[- IH]") as "_"; first by iExists _; auto with iFrame.
+      iModIntro. by wp_case.
+  Qed.
+
+  Lemma try_unwrap_spec (γ : gname) (q: Qp) (l : loc) :
+    is_arc P1 P2 N γ l -∗
+    {{{ arc_tok γ q ∗ P1 q }}} try_unwrap [ #l]
+    {{{ (b : bool), RET #b ;
+        if b then P1 1 ∗ (P2 ={⊤}=∗ weak_tok γ) else arc_tok γ q ∗ P1 q }}}.
+  Proof using HP1.
+    iIntros "#INV !> * [Hown HP1] HΦ". wp_rec. iInv N as (st) "[>H● H]" "Hclose".
+    iDestruct (arc_tok_auth_val with "H● Hown") as %(q' & s & wl & w &[-> Hqq']).
+    iDestruct "H" as (q'') "(>Hq'' & HP1' & Hs & Hw)". iDestruct "Hq''" as %Hq''.
+    destruct (decide (s = xH)) as [->|?].
+    - wp_apply (wp_cas_int_suc with "Hs"). iIntros "Hs".
+      destruct Hqq' as [<- ->]. iMod (own_update_2 with "H● Hown") as "[H● H◯]".
+      { apply auth_update, prod_local_update_1. rewrite -[x in (x, _)]right_id.
+        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''. 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.
+  Qed.
+
+  Lemma is_unique_spec (γ : gname) (q: Qp) (l : loc) :
+    is_arc P1 P2 N γ l -∗
+    {{{ arc_tok γ q ∗ P1 q }}} is_unique [ #l]
+    {{{ (b : bool), RET #b ;
+        if b then l ↦ #1 ∗ (l +ₗ 1) ↦ #1 ∗ P1 1
+        else arc_tok γ q ∗ P1 q }}}.
+  Proof using HP1.
+    iIntros "#INV !> * [Hown HP1] HΦ". wp_rec. wp_bind (CAS _ _ _). wp_op.
+    iInv N as (st) "[>H● H]" "Hclose".
+    iDestruct (arc_tok_auth_val with "H● Hown") as %(? & ? & wl & w &[-> _]).
+    iDestruct "H" as (?) "(>Hq'' & HP1' & >Hs & >Hw)".
+    destruct wl; last (destruct w; last first).
+    - iDestruct "Hw" as "[Hw %]". subst.
+      iApply (wp_cas_int_fail with "Hw")=>//. iNext. iIntros "Hw".
+      iMod ("Hclose" with "[-HΦ Hown HP1]") as "_"; first by iExists _; eauto with iFrame.
+      iModIntro. wp_case. iApply "HΦ". iFrame.
+    - iApply (wp_cas_int_fail with "Hw"); [lia|]. iNext. iIntros "Hw".
+      iMod ("Hclose" with "[-HΦ Hown HP1]") as "_"; first by iExists _; eauto with iFrame.
+      iModIntro. wp_case. iApply "HΦ". iFrame.
+    - iApply (wp_cas_int_suc with "Hw")=>//. iNext. iIntros "Hw".
+      iMod (own_update_2 with "H● Hown") as "[H● H◯]".
+      { by apply auth_update, prod_local_update_1, option_local_update,
+                 csum_local_update_l, prod_local_update_2,
+                 (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".
+      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|(?&?&[=]&?)]]=>//.
+        destruct Hincl as (?&[[??]?]&[=<-]&->&[[_ Hlt]%prod_included _]%prod_included).
+        simpl in Hlt. apply pos_included in Hlt.
+        iDestruct "H" as (?) "(? & ? & ? & ?)". wp_read.
+        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".
+        iCombine "H● H◯" gives
+           %[[[[=]|Hincl]%option_included _]%prod_included [Hval _]]%auth_both_valid_discrete.
+        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|(?&?&[=]&?)]]=>//.
+          destruct Hincl as (?&[[??]?]&[=<-]&->&[_ Hincl%option_included]%prod_included).
+          simpl in Hincl. destruct Hincl as [[=]|(?&?&[=<-]&->&[?|[]%exclusive_included])];
+            [|by apply _|by apply Hval]. setoid_subst. eauto. }
+        iDestruct "H" as (?) "(? & ? & ? & >? & >%)". subst. wp_write.
+        iMod (own_update_2 with "H● H◯") as "[H● H◯]".
+        { apply auth_update, prod_local_update_1, option_local_update,
+          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 & 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 %<-. iCombine "HP1 HP1'" as "$". iFrame.
+  Qed.
+
+  Lemma try_unwrap_full_spec (γ : gname) (q: Qp) (l : loc) :
+    is_arc P1 P2 N γ l -∗
+    {{{ arc_tok γ q ∗ P1 q }}} try_unwrap_full [ #l]
+    {{{ (x : fin 3), RET #x ;
+        match x : nat with
+        (* No other reference : we get everything. *)
+        | 0%nat => l ↦ #1 ∗ (l +ₗ 1) ↦ #1 ∗ P1 1
+        (* No other strong, but there are weaks : we get P1,
+           plus the option to get a weak if we pay P2. *)
+        | 1%nat => P1 1 ∗ (P2 ={⊤}=∗ weak_tok γ)
+        (* There are other strong : we get back what we gave at the first place. *)
+        | _ (* 2 *) => arc_tok γ q ∗ P1 q
+        end }}}.
+  Proof using HP1.
+    iIntros "#INV !> * [Hown HP1] HΦ". wp_rec. wp_bind (CAS _ _ _).
+    iInv N as (st) "[>H● H]" "Hclose".
+    iDestruct (arc_tok_auth_val with "H● Hown") as %(q' & s & wl & w &[-> Hqq']).
+    iDestruct "H" as (q'') "(>Hq'' & HP1' & Hs & Hw)". iDestruct "Hq''" as %Hq''.
+    destruct (decide (s = xH)) as [->|?].
+    - wp_apply (wp_cas_int_suc with "Hs")=>//. iIntros "Hs".
+      destruct Hqq' as [<- ->]. iMod (own_update_2 with "H● Hown") as "[H● H◯]".
+      { apply auth_update, prod_local_update_1. rewrite -[x in (x, _)]right_id.
+        etrans; first apply: cancel_local_update_unit.
+        by apply (op_local_update _ _ (Some (Cinr (Excl ())))). }
+      iCombine "HP1" "HP1'" as "HP1". rewrite Hq''. clear Hq'' q''.
+      iMod ("Hclose" with "[H● Hs Hw]") as "_"; first by iExists _; do 2 iFrame.
+      clear w. iModIntro. wp_case. wp_op. wp_bind (!ˢᶜ_)%E.
+      iInv N as ([st w']) "[>H● H]" "Hclose".
+      iDestruct (own_valid_2 with "H● H◯")
+        as %[[[[=]|Hincl]%option_included _]%prod_included [? _]]%auth_both_valid_discrete.
+      simpl in Hincl. destruct Hincl as (?&?&[=<-]&->&[?|[]%exclusive_included]);
+        [|by apply _|done]. setoid_subst. iDestruct "H" as "[Hl Hl1]".
+      wp_read. destruct w'.
+      + iMod (own_update_2 with "H● H◯") as "H●".
+        { apply auth_update_dealloc, prod_local_update_1,
+                delete_option_local_update, _. }
+        iMod ("Hclose" with "[H●]") as "_"; first by iExists _; iFrame. iModIntro.
+        wp_op. wp_if. wp_write. iApply ("HΦ" $! 0%fin). iFrame.
+      + iMod ("Hclose" with "[H● Hl Hl1]") as "_"; first by iExists _; do 2 iFrame.
+        iModIntro. wp_op; case_bool_decide; [lia|]. wp_if. iApply ("HΦ" $! 1%fin). iFrame.
+        by iApply close_last_strong.
+    - wp_apply (wp_cas_int_fail with "Hs"); [congruence|]. iIntros "Hs".
+      iMod ("Hclose" with "[H● Hs Hw HP1']") as "_"; first by iExists _; auto with iFrame.
+      iModIntro. wp_case. iApply ("HΦ" $! 2%fin). iFrame.
+  Qed.
+End arc.
+
+Global Typeclasses Opaque is_arc arc_tok weak_tok.

lambda-rust/lang/lib/lock.v

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