.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.

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.