.gitattributes

+*.v gitlab-language=coq

.gitignore

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

.gitlab-ci.yml

+image: ralfjung/opam-ci:opam2
+
+stages:
+  - build
+
+variables:
+  CPU_CORES: "10"
+  OCAML: "ocaml-variants.4.14.0+options ocaml-option-flambda"
+
+.template: &template
+  stage: build
+  tags:
+  - fp
+  script:
+  - git clone https://gitlab.mpi-sws.org/iris/ci.git ci -b opam2
+  - ci/buildjob
+  cache:
+    key: "$CI_JOB_NAME"
+    paths:
+    - _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:
+    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

-# Makefile originally taken from coq-club
+# Default target
+all: Makefile.coq
+	+@$(MAKE) -f Makefile.coq all
+.PHONY: all
 
-%: Makefile.coq
-	+make -f Makefile.coq $@
+# Permit local customization
+-include Makefile.local
 
-all: Makefile.coq
-	+make -f Makefile.coq all
+# Forward most targets to Coq makefile (with some trick to make this phony)
+%: Makefile.coq phony
+	@#echo "Forwarding $@"
+	+@$(MAKE) -f Makefile.coq $@
+phony: ;
+.PHONY: phony
 
 clean: Makefile.coq
-	+make -f Makefile.coq clean
-	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.
 Makefile.coq: _CoqProject Makefile
-	coq_makefile -f _CoqProject | sed 's/$$(COQCHK) $$(COQCHKFLAGS) $$(COQLIBS)/$$(COQCHK) $$(COQCHKFLAGS) $$(subst -Q,-R,$$(COQLIBS))/' > Makefile.coq
+	"$(COQBIN)coq_makefile" -f _CoqProject -o Makefile.coq $(EXTRA_COQFILES)
+
+# Install build-dependencies
+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
 
-_CoqProject: ;
+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
 
-Makefile: ;
+# Backwards compatibility target
+build-dep: builddep
+.PHONY: build-dep
 
-.PHONY: all clean
+# 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 development accompanying lambda-Rust.
+
+## Prerequisites
+
+This version is known to compile with:
+
+ - Coq 8.20.0
+ - A development version of [Iris](https://gitlab.mpi-sws.org/iris/iris)
+
+## Building from source
+
+When building from source, we recommend to use opam (2.0.0 or newer) for
+installing the dependencies.  This requires the following two repositories:
+
+    opam repo add coq-released https://coq.inria.fr/opam/released
+    opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
+
+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 . lrust
-adequacy.v
-derived.v
-heap.v
-lang.v
-lifting.v
-memcpy.v
-notation.v
-proofmode.v
-races.v
-tactics.v
-wp_tactics.v
-lifetime.v
-type.v
-type_incl.v
-perm.v
-perm_incl.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

adequacy.v

-From iris.program_logic Require Export weakestpre adequacy.
-From lrust Require Export heap.
-From iris.program_logic Require Import auth ownership.
-From lrust Require Import proofmode notation.
-From iris.proofmode Require Import tactics weakestpre.
-From iris.prelude Require Import fin_maps.
-
-Definition heap_adequacy Σ `{irisPreG lrust_lang Σ, authG Σ heapValUR, authG Σ heapFreeableUR} e σ φ :
-  (∀ `{heapG Σ}, heap_ctx ⊢ WP e {{ v, ■ φ v }}) →
-  adequate e σ φ.
-Proof.
-  intros Hwp; eapply (wp_adequacy Σ); iIntros (?) "Hσ".
-  iVs (own_alloc (● to_heapVal σ)) as (vγ) "Hvγ".
-  { split; last apply to_heap_valid. intro. simpl. refine (ucmra_unit_leastN _ _). }
-  iVs (own_alloc (● (∅ : heapFreeableUR))) as (fγ) "Hfγ".
-  { split. intro. refine (ucmra_unit_leastN _ _). exact ucmra_unit_valid. }
-  set (h:=HeapG _ _ _ _ vγ fγ).
-  iVs (inv_alloc heapN _ heap_inv with "[-]") as "HN";
-    last by iApply (Hwp h); rewrite /heap_ctx.
-  iNext. iExists _, _. iFrame. iPureIntro. intros ??. rewrite lookup_empty.
-  inversion 1.
-Qed.

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-03-28.0.fa344cbe") | (= "dev") }
+]
+
+build: ["./make-package" "lifetime" "-j%{jobs}%"]
+install: ["./make-package" "lifetime" "install"]

coq-lint.sh

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

derived.v

-From lrust Require Export lifting.
-From iris.proofmode Require Import weakestpre.
-Import uPred.
-
-(** Define some derived forms, and derived lemmas about them. *)
-Notation Lam xl e := (Rec BAnon xl e).
-Notation Let x e1 e2 := (App (Lam [x] e2) [e1]).
-Notation Seq e1 e2 := (Let BAnon e1 e2).
-Notation LamV xl e := (RecV BAnon xl e).
-Notation LetCtx x e2 := (AppRCtx (LamV [x] e2) [] []).
-Notation SeqCtx e2 := (LetCtx BAnon e2).
-Notation Skip := (Seq (Lit LitUnit) (Lit LitUnit)).
-Coercion lit_of_bool : bool >-> base_lit.
-Notation If e0 e1 e2 := (Case e0 [e2;e1]).
-Notation Newlft := (Lit LitUnit) (only parsing).
-Notation Endlft := (Seq Skip Skip) (only parsing).
-
-Section derived.
-Context `{irisG lrust_lang Σ}.
-Implicit Types P Q : iProp Σ.
-Implicit Types Φ : val → iProp Σ.
-
-(** Proof rules for the sugar *)
-Lemma wp_lam E xl e e' el Φ :
-  Forall (λ ei, is_Some (to_val ei)) el →
-  Closed (xl +b+ []) e →
-  subst_l xl el e = Some e' →
-  ▷ WP e' @ E {{ Φ }} ⊢ WP App (Lam xl e) el @ E {{ Φ }}.
-Proof. iIntros (???) "?". by iApply (wp_rec _ _ BAnon). Qed.
-
-Lemma wp_let E x e1 e2 v Φ :
-  to_val e1 = Some v →
-  Closed (x :b: []) e2 →
-  ▷ WP subst' x e1 e2 @ E {{ Φ }} ⊢ WP Let x e1 e2 @ E {{ Φ }}.
-Proof. eauto using wp_lam. Qed.
-
-Lemma wp_seq E e1 e2 v Φ :
-  to_val e1 = Some v →
-  Closed [] e2 →
-  ▷ WP e2 @ E {{ Φ }} ⊢ WP Seq e1 e2 @ E {{ Φ }}.
-Proof. iIntros (??) "?". by iApply (wp_let _ BAnon). Qed.
-
-Lemma wp_skip E Φ : ▷ Φ (LitV LitUnit) ⊢ WP Skip @ E {{ Φ }}.
-Proof. iIntros. iApply wp_seq. done. iNext. by iApply wp_value. Qed.
-
-Lemma wp_le E (n1 n2 : Z) P Φ :
-  (n1 ≤ n2 → P ⊢ ▷ |={E}=> Φ (LitV true)) →
-  (n2 < n1 → P ⊢ ▷ |={E}=> Φ (LitV false)) →
-  P ⊢ WP BinOp LeOp (Lit (LitInt n1)) (Lit (LitInt n2)) @ E {{ Φ }}.
-Proof.
-  intros. rewrite -wp_bin_op //; [].
-  destruct (bool_decide_reflect (n1 ≤ n2)); by eauto with omega.
-Qed.
-
-Lemma wp_if E (b : bool) e1 e2 Φ :
-  (if b then ▷ WP e1 @ E {{ Φ }} else ▷ WP e2 @ E {{ Φ }})%I
-  ⊢ WP If (Lit b) e1 e2 @ E {{ Φ }}.
-Proof. iIntros "?". by destruct b; iApply wp_case. Qed.
-End derived.

lambda-rust/lang/adequacy.v

+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 lrustGpreS Σ := HeapGpreS {
+  lrustGpreS_irig :: invGpreS Σ;
+  lrustGpreS_heap :: inG Σ (authR heapUR);
+  lrustGpreS_heap_freeable :: inG Σ (authR heap_freeableUR)
+}.
+
+Definition lrustΣ : gFunctors :=
+  #[invΣ;
+    GFunctor (constRF (authR heapUR));
+    GFunctor (constRF (authR heap_freeableUR))].
+Global Instance subG_lrustGpreS {Σ} : subG lrustΣ Σ → lrustGpreS Σ.
+Proof. solve_inG. Qed.
+
+Definition lrust_adequacy Σ `{!lrustGpreS Σ} e σ φ :
+  (∀ `{!lrustGS Σ}, True ⊢ WP e {{ v, ⌜φ v⌝ }}) →
+  adequate NotStuck e σ (λ v _, φ v).
+Proof.
+  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 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.