Skip to content
Snippets Groups Projects

Compare revisions

Changes are shown as if the source revision was being merged into the target revision. Learn more about comparing revisions.

Source

Select target project
No results found
Select Git revision

Target

Select target project
  • Villetaneuse/lambda-rust
  • iris/lambda-rust
  • maximedenes/LambdaRust-coq
  • msammler/lambda-rust
  • daniel.louwrink/lambda-rust
  • simonspies/lambda-rust
  • xldenis/lambda-rust
  • lgaeher/lambda-rust
  • JasonHuZS/lambda-rust
  • snyke7/lambda-rust
  • ivanbakel/lambda-rust
  • HumamAlhusaini/lambda-rust
12 results
Select Git revision
Show changes
Commits on Source (309)
209 additional commits have been omitted to prevent performance issues.
Expand all Hide whitespace changes
Inline Side-by-side
Showing
with 570 additions and 434 deletions
.gitattributes 0 → 100644
View file @ 0f4ebd6d
*.v gitlab-language=coq
.gitignore
View file @ 0f4ebd6d
*.vo *.vo
*.vio *.vio
*.v.d *.v.d
*.vos
*.vok
.coqdeps.d .coqdeps.d
.Makefile.coq.d
*.glob *.glob
*.cache *.cache
*.aux *.aux
...@@ -10,7 +13,7 @@ ...@@ -10,7 +13,7 @@
*~ *~
*.bak *.bak
.coq-native/ .coq-native/
build-dep/ builddep/
Makefile.coq Makefile.coq
Makefile.coq.conf Makefile.coq.conf
_opam _opam
.gitlab-ci.yml
View file @ 0f4ebd6d
...@@ -5,6 +5,7 @@ stages: ...@@ -5,6 +5,7 @@ stages:
variables: variables:
CPU_CORES: "10" CPU_CORES: "10"
OCAML: "ocaml-variants.4.14.0+options ocaml-option-flambda"
.template: &template .template: &template
stage: build stage: build
...@@ -16,10 +17,10 @@ variables: ...@@ -16,10 +17,10 @@ variables:
cache: cache:
key: "$CI_JOB_NAME" key: "$CI_JOB_NAME"
paths: paths:
- opamroot/ - _opam/
only: only:
- master - /^master/@iris/lambda-rust
- /^ci/ - /^ci/@iris/lambda-rust
except: except:
- triggers - triggers
- schedules - schedules
...@@ -27,32 +28,42 @@ variables: ...@@ -27,32 +28,42 @@ variables:
## Build jobs ## Build jobs
build-coq.dev: build-coq.9.0.0:
<<: *template <<: *template
variables: variables:
OCAML: "ocaml-base-compiler.4.07.0" OPAM_PINS: "coq version 9.0.0"
OPAM_PINS: "coq version dev" DENY_WARNINGS: "1"
MANGLE_NAMES: "1"
build-coq.8.9.0: # Mostly to make the lifetime logic available
<<: *template OPAM_PKG: "1"
variables:
OPAM_PINS: "coq version 8.9.0"
OPAM_PKG: "coq-lambda-rust"
TIMING_CONF: "coq-8.9.0"
tags: tags:
- fp-timing - fp-timing
build-coq.8.8.2: trigger-iris.timing:
<<: *template <<: *template
variables: variables:
OPAM_PINS: "coq version 8.8.2" OPAM_PINS: "coq version 9.0.0 git+https://gitlab.mpi-sws.org/$IRIS_REPO#$IRIS_REV"
tags:
- fp-timing
only:
- triggers
- schedules
- api
except:
variables:
- $TIMING_AD_HOC_ID == null
build-iris.dev: trigger-iris.dev:
<<: *template <<: *template
variables: variables:
OPAM_PINS: "coq version 8.9.0 coq-stdpp.dev git git+https://gitlab.mpi-sws.org/iris/stdpp.git#$STDPP_REV coq-iris.dev git git+https://gitlab.mpi-sws.org/iris/iris.git#$IRIS_REV" STDPP_REPO: "iris/stdpp"
IRIS_REPO: "iris/iris"
OPAM_PINS: "coq version $NIGHTLY_COQ git+https://gitlab.mpi-sws.org/$STDPP_REPO#$STDPP_REV git+https://gitlab.mpi-sws.org/$IRIS_REPO#$IRIS_REV"
except: except:
only: only:
- triggers refs:
- schedules - triggers
- api - schedules
- api
variables:
- $TIMING_AD_HOC_ID == null
LICENSE
View file @ 0f4ebd6d
All files in this development are distributed under the terms of the BSD All files in this development are distributed under the terms of the BSD
license, included below. license, included below.
------------------------------------------------------------------------------ Copyright: lambdaRust developers and contributors
BSD LICENCE ------------------------------------------------------------------------------
Redistribution and use in source and binary forms, with or without Redistribution and use in source and binary forms, with or without
modification, are permitted provided that the following conditions are met: modification, are permitted provided that the following conditions are met:
...@@ -12,18 +12,17 @@ modification, are permitted provided that the following conditions are met: ...@@ -12,18 +12,17 @@ modification, are permitted provided that the following conditions are met:
* Redistributions in binary form must reproduce the above copyright * Redistributions in binary form must reproduce the above copyright
notice, this list of conditions and the following disclaimer in the notice, this list of conditions and the following disclaimer in the
documentation and/or other materials provided with the distribution. documentation and/or other materials provided with the distribution.
* Neither the name of the <organization> nor the * Neither the name of the copyright holder nor the names of its contributors
names of its contributors may be used to endorse or promote products may be used to endorse or promote products derived from this software
derived from this software without specific prior written permission. without specific prior written permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND 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 ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT HOLDER> BE LIABLE FOR ANY DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR
DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON
ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT 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 (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
Makefile
View file @ 0f4ebd6d
# Forward most targets to Coq makefile (with some trick to make this phony) # Default target
%: Makefile.coq phony
+@make -f Makefile.coq $@
all: Makefile.coq all: Makefile.coq
+@make -f Makefile.coq all +@$(MAKE) -f Makefile.coq all
.PHONY: all .PHONY: all
# Permit local customization
-include Makefile.local
# Forward most targets to Coq makefile (with some trick to make this phony)
%: Makefile.coq phony
@#echo "Forwarding $@"
+@$(MAKE) -f Makefile.coq $@
phony: ;
.PHONY: phony
clean: Makefile.coq clean: Makefile.coq
+@make -f Makefile.coq clean +@$(MAKE) -f Makefile.coq clean
find theories tests \( -name "*.d" -o -name "*.vo" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete || true @# Make sure not to enter the `_opam` folder.
rm -f Makefile.coq 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 .PHONY: clean
# Create Coq Makefile. # Create Coq Makefile.
Makefile.coq: _CoqProject Makefile Makefile.coq: _CoqProject Makefile
"$(COQBIN)coq_makefile" -f _CoqProject -o Makefile.coq "$(COQBIN)coq_makefile" -f _CoqProject -o Makefile.coq $(EXTRA_COQFILES)
# Install build-dependencies # Install build-dependencies
build-dep/opam: opam Makefile OPAMFILES=$(wildcard *.opam)
@echo "# Creating build-dep package." BUILDDEPFILES=$(addsuffix -builddep.opam, $(addprefix builddep/,$(basename $(OPAMFILES))))
@mkdir -p build-dep
@sed <opam -E 's/^(build|install|remove):.*/\1: []/; s/^name: *"(.*)" */name: "\1-builddep"/' >build-dep/opam builddep/%-builddep.opam: %.opam Makefile
@fgrep builddep build-dep/opam >/dev/null || (echo "sed failed to fix the package name" && exit 1) # sanity check @echo "# Creating builddep package for $<."
@mkdir -p builddep
build-dep: build-dep/opam phony @sed <$< -E 's/^(build|install|remove):.*/\1: []/; s/"(.*)"(.*= *version.*)$$/"\1-builddep"\2/;' >$@
@# We want opam to not just instal the build-deps now, but to also keep satisfying these
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 @# constraints. Otherwise, `opam upgrade` may well update some packages to versions
@# that are incompatible with our build requirements. @# that are incompatible with our build requirements.
@# To achieve this, we create a fake opam package that has our build-dependencies as @# To achieve this, we create a fake opam package that has our build-dependencies as
@# dependencies, but does not actually install anything itself. @# dependencies, but does not actually install anything itself.
@echo "# Pinning build-dep package." && \ @echo "# Installing builddep packages."
if opam --version | grep "^1\." -q; then \ @opam install $(OPAMFLAGS) $(BUILDDEPFILES)
BUILD_DEP_PACKAGE="$$(egrep "^name:" build-dep/opam | sed 's/^name: *"\(.*\)" */\1/')" && \ .PHONY: builddep
opam pin add -k path $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE".dev build-dep && \
opam reinstall $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE"; \ # Backwards compatibility target
else \ build-dep: builddep
opam install $(OPAMFLAGS) build-dep/; \ .PHONY: build-dep
fi
# Some files that do *not* need to be forwarded to Makefile.coq.
# Some files that do *not* need to be forwarded to Makefile.coq # ("::" lets Makefile.local overwrite this.)
Makefile: ; Makefile Makefile.local _CoqProject $(OPAMFILES):: ;
_CoqProject: ;
opam: ;
# Phony wildcard targets
phony: ;
.PHONY: phony
Makefile.coq.local 0 → 100644
View file @ 0f4ebd6d
# 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
View file @ 0f4ebd6d
Missing APIs from the types we cover (APIs have been added after this formalization was done) 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 # Cell
* Structural conversion for slices. The matching operations in our model would be * Structural conversion for slices. The matching operations in our model would be
`&mut Cell<(A, B)>` -> `&mut (Cell<A>, Cell<B>)` and `&mut Cell<(A, B)>` -> `&mut (Cell<A>, Cell<B>)` and
`&Cell<(A, B)>` -> `&(Cell<A>, Cell<B>)` (both being NOPs). `&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 # ZST
......
README.md
View file @ 0f4ebd6d
...@@ -6,12 +6,12 @@ This is the Coq development accompanying lambda-Rust. ...@@ -6,12 +6,12 @@ This is the Coq development accompanying lambda-Rust.
This version is known to compile with: This version is known to compile with:
- Coq 8.8.2 / 8.9.0 - Rocq 9.0.0
- A development version of [Iris](https://gitlab.mpi-sws.org/iris/iris) - A development version of [Iris](https://gitlab.mpi-sws.org/iris/iris)
## Building from source ## Building from source
When building from source, we recommend to use opam (1.2.2 or newer) for When building from source, we recommend to use opam (2.0.0 or newer) for
installing the dependencies. This requires the following two repositories: installing the dependencies. This requires the following two repositories:
opam repo add coq-released https://coq.inria.fr/opam/released opam repo add coq-released https://coq.inria.fr/opam/released
...@@ -52,6 +52,26 @@ followed by `make build-dep`. ...@@ -52,6 +52,26 @@ followed by `make build-dep`.
`thread::spawn`, `take_mut::take`, `alias::once` as well as converting `&&T` `thread::spawn`, `take_mut::take`, `alias::once` as well as converting `&&T`
to `&Box<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 ## Where to Find the Proof Rules From the Paper
### Type System Rules ### Type System Rules
...@@ -91,7 +111,7 @@ borrows" in the Coq development. ...@@ -91,7 +111,7 @@ borrows" in the Coq development.
| F-endlft | programs.v | type_endlft | | F-endlft | programs.v | type_endlft |
| F-call | function.v | type_call' | | F-call | function.v | type_call' |
Some of these lemmas are called `something'` because the version without the `'` is a derived, more speicalized form used together with our eauto-based `solve_typing` tactic. You can see this tactic in action in the [examples](theories/typing/examples) subfolder. Some of these lemmas are called `something'` because the version without the `'` is a derived, more specialized form used together with our eauto-based `solve_typing` tactic. You can see this tactic in action in the [examples](theories/typing/examples) subfolder.
### Lifetime Logic Rules ### Lifetime Logic Rules
......
_CoqProject
View file @ 0f4ebd6d
-Q theories lrust # Search paths for all packages. They must all match the regex
# We sometimes want to locally override notation and there is no good way to do that with scopes. # `-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 -arg -w -arg -notation-overridden
# non-canonical projections (https://github.com/coq/coq/pull/10076) do not exist yet in 8.9. # Cannot use non-canonical projections as it causes massive unification failures
# (https://github.com/coq/coq/issues/6294).
-arg -w -arg -redundant-canonical-projection -arg -w -arg -redundant-canonical-projection
# change_no_check does not exist yet in 8.9. # Warning is often incorrect, see https://gitlab.mpi-sws.org/iris/stdpp/-/issues/216
-arg -w -arg -convert_concl_no_check -arg -w -arg -notation-incompatible-prefix
theories/lifetime/model/definitions.v lifetime/model/definitions.v
theories/lifetime/model/faking.v lifetime/model/faking.v
theories/lifetime/model/creation.v lifetime/model/creation.v
theories/lifetime/model/primitive.v lifetime/model/primitive.v
theories/lifetime/model/accessors.v lifetime/model/accessors.v
theories/lifetime/model/borrow.v lifetime/model/borrow.v
theories/lifetime/model/borrow_sep.v lifetime/model/borrow_sep.v
theories/lifetime/model/reborrow.v lifetime/model/reborrow.v
theories/lifetime/lifetime_sig.v lifetime/lifetime_sig.v
theories/lifetime/lifetime.v lifetime/lifetime.v
theories/lifetime/at_borrow.v lifetime/at_borrow.v
theories/lifetime/na_borrow.v lifetime/na_borrow.v
theories/lifetime/frac_borrow.v lifetime/frac_borrow.v
theories/lang/adequacy.v lifetime/meta.v
theories/lang/heap.v lambda-rust/lang/adequacy.v
theories/lang/lang.v lambda-rust/lang/heap.v
theories/lang/lifting.v lambda-rust/lang/lang.v
theories/lang/notation.v lambda-rust/lang/lifting.v
theories/lang/proofmode.v lambda-rust/lang/notation.v
theories/lang/races.v lambda-rust/lang/proofmode.v
theories/lang/tactics.v lambda-rust/lang/races.v
theories/lang/lib/memcpy.v lambda-rust/lang/tactics.v
theories/lang/lib/swap.v lambda-rust/lang/lib/memcpy.v
theories/lang/lib/new_delete.v lambda-rust/lang/lib/swap.v
theories/lang/lib/spawn.v lambda-rust/lang/lib/new_delete.v
theories/lang/lib/lock.v lambda-rust/lang/lib/spawn.v
theories/lang/lib/arc.v lambda-rust/lang/lib/lock.v
theories/lang/lib/tests.v lambda-rust/lang/lib/arc.v
theories/typing/base.v lambda-rust/lang/lib/tests.v
theories/typing/type.v lambda-rust/typing/base.v
theories/typing/util.v lambda-rust/typing/type.v
theories/typing/lft_contexts.v lambda-rust/typing/util.v
theories/typing/type_context.v lambda-rust/typing/lft_contexts.v
theories/typing/cont_context.v lambda-rust/typing/type_context.v
theories/typing/uninit.v lambda-rust/typing/cont_context.v
theories/typing/own.v lambda-rust/typing/uninit.v
theories/typing/uniq_bor.v lambda-rust/typing/own.v
theories/typing/shr_bor.v lambda-rust/typing/uniq_bor.v
theories/typing/product.v lambda-rust/typing/shr_bor.v
theories/typing/product_split.v lambda-rust/typing/product.v
theories/typing/sum.v lambda-rust/typing/product_split.v
theories/typing/bool.v lambda-rust/typing/sum.v
theories/typing/int.v lambda-rust/typing/bool.v
theories/typing/function.v lambda-rust/typing/int.v
theories/typing/programs.v lambda-rust/typing/function.v
theories/typing/borrow.v lambda-rust/typing/programs.v
theories/typing/cont.v lambda-rust/typing/borrow.v
theories/typing/fixpoint.v lambda-rust/typing/cont.v
theories/typing/type_sum.v lambda-rust/typing/fixpoint.v
theories/typing/typing.v lambda-rust/typing/type_sum.v
theories/typing/soundness.v lambda-rust/typing/typing.v
theories/typing/lib/panic.v lambda-rust/typing/soundness.v
theories/typing/lib/option.v lambda-rust/typing/lib/panic.v
theories/typing/lib/fake_shared.v lambda-rust/typing/lib/option.v
theories/typing/lib/cell.v lambda-rust/typing/lib/fake_shared.v
theories/typing/lib/spawn.v lambda-rust/typing/lib/cell.v
theories/typing/lib/join.v lambda-rust/typing/lib/spawn.v
theories/typing/lib/diverging_static.v lambda-rust/typing/lib/join.v
theories/typing/lib/take_mut.v lambda-rust/typing/lib/take_mut.v
theories/typing/lib/rc/rc.v lambda-rust/typing/lib/rc/rc.v
theories/typing/lib/rc/weak.v lambda-rust/typing/lib/rc/weak.v
theories/typing/lib/arc.v lambda-rust/typing/lib/arc.v
theories/typing/lib/swap.v lambda-rust/typing/lib/swap.v
theories/typing/lib/mutex/mutex.v lambda-rust/typing/lib/diverging_static.v
theories/typing/lib/mutex/mutexguard.v lambda-rust/typing/lib/brandedvec.v
theories/typing/lib/refcell/refcell.v lambda-rust/typing/lib/ghostcell.v
theories/typing/lib/refcell/ref.v lambda-rust/typing/lib/mutex/mutex.v
theories/typing/lib/refcell/refmut.v lambda-rust/typing/lib/mutex/mutexguard.v
theories/typing/lib/refcell/refcell_code.v lambda-rust/typing/lib/refcell/refcell.v
theories/typing/lib/refcell/ref_code.v lambda-rust/typing/lib/refcell/ref.v
theories/typing/lib/refcell/refmut_code.v lambda-rust/typing/lib/refcell/refmut.v
theories/typing/lib/rwlock/rwlock.v lambda-rust/typing/lib/refcell/refcell_code.v
theories/typing/lib/rwlock/rwlockreadguard.v lambda-rust/typing/lib/refcell/ref_code.v
theories/typing/lib/rwlock/rwlockwriteguard.v lambda-rust/typing/lib/refcell/refmut_code.v
theories/typing/lib/rwlock/rwlock_code.v lambda-rust/typing/lib/rwlock/rwlock.v
theories/typing/lib/rwlock/rwlockreadguard_code.v lambda-rust/typing/lib/rwlock/rwlockreadguard.v
theories/typing/lib/rwlock/rwlockwriteguard_code.v lambda-rust/typing/lib/rwlock/rwlockwriteguard.v
theories/typing/examples/get_x.v lambda-rust/typing/lib/rwlock/rwlock_code.v
theories/typing/examples/rebor.v lambda-rust/typing/lib/rwlock/rwlockreadguard_code.v
theories/typing/examples/unbox.v lambda-rust/typing/lib/rwlock/rwlockwriteguard_code.v
theories/typing/examples/init_prod.v lambda-rust/typing/examples/fixpoint.v
theories/typing/examples/lazy_lft.v lambda-rust/typing/examples/get_x.v
theories/typing/examples/nonlexical.v lambda-rust/typing/examples/rebor.v
lambda-rust/typing/examples/unbox.v
lambda-rust/typing/examples/init_prod.v
lambda-rust/typing/examples/lazy_lft.v
lambda-rust/typing/examples/nonlexical.v
coq-lambda-rust.opam 0 → 100644
View file @ 0f4ebd6d
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 0 → 100644
View file @ 0f4ebd6d
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 0 → 100755
View file @ 0f4ebd6d
#!/bin/sh
set -e
## A simple shell script checking for some common Coq issues.
FILE="$1"
if grep -E -n '^\s*((Existing\s+|Program\s+|Declare\s+)?Instance|Arguments|Remove|Hint\s+(Extern|Constructors|Resolve|Immediate|Mode|Opaque|Transparent|Unfold)|(Open|Close)\s+Scope|Opaque|Transparent)\b' "$FILE"; then
echo "ERROR: $FILE contains 'Instance'/'Arguments'/'Hint' or another side-effect without locality (see above)."
echo "Please add 'Global' or 'Local' as appropriate."
echo
exit 1
fi
descr deleted 100644 → 0
View file @ 1b485b6e
A formal model of a Rust core langauge and type system, a logical relation for
the type system, and safety proof for some Rust libraries.
theories/lang/adequacy.v → lambda-rust/lang/adequacy.v
View file @ 0f4ebd6d
...@@ -2,23 +2,23 @@ From iris.program_logic Require Export adequacy weakestpre. ...@@ -2,23 +2,23 @@ From iris.program_logic Require Export adequacy weakestpre.
From iris.algebra Require Import auth. From iris.algebra Require Import auth.
From lrust.lang Require Export heap. From lrust.lang Require Export heap.
From lrust.lang Require Import proofmode notation. From lrust.lang Require Import proofmode notation.
Set Default Proof Using "Type". From iris.prelude Require Import options.
Class lrustPreG Σ := HeapPreG { Class lrustGpreS Σ := HeapGpreS {
lrust_preG_irig :> invPreG Σ; lrustGpreS_irig :: invGpreS Σ;
lrust_preG_heap :> inG Σ (authR heapUR); lrustGpreS_heap :: inG Σ (authR heapUR);
lrust_preG_heap_freeable :> inG Σ (authR heap_freeableUR) lrustGpreS_heap_freeable :: inG Σ (authR heap_freeableUR)
}. }.
Definition lrustΣ : gFunctors := Definition lrustΣ : gFunctors :=
#[invΣ; #[invΣ;
GFunctor (constRF (authR heapUR)); GFunctor (constRF (authR heapUR));
GFunctor (constRF (authR heap_freeableUR))]. GFunctor (constRF (authR heap_freeableUR))].
Instance subG_heapPreG {Σ} : subG lrustΣ Σ → lrustPreG Σ. Global Instance subG_lrustGpreS {Σ} : subG lrustΣ Σ → lrustGpreS Σ.
Proof. solve_inG. Qed. Proof. solve_inG. Qed.
Definition lrust_adequacy Σ `{!lrustPreG Σ} e σ φ : Definition lrust_adequacy Σ `{!lrustGpreS Σ} e σ φ :
(∀ `{!lrustG Σ}, True ⊢ WP e {{ v, ⌜φ v⌝ }}) → (∀ `{!lrustGS Σ}, True ⊢ WP e {{ v, ⌜φ v⌝ }}) →
adequate NotStuck e σ (λ v _, φ v). adequate NotStuck e σ (λ v _, φ v).
Proof. Proof.
intros Hwp; eapply (wp_adequacy _ _); iIntros (??). intros Hwp; eapply (wp_adequacy _ _); iIntros (??).
...@@ -26,8 +26,8 @@ Proof. ...@@ -26,8 +26,8 @@ Proof.
{ apply (auth_auth_valid (to_heap _)), to_heap_valid. } { apply (auth_auth_valid (to_heap _)), to_heap_valid. }
iMod (own_alloc (● (∅ : heap_freeableUR))) as (fγ) "Hfγ"; iMod (own_alloc (● (∅ : heap_freeableUR))) as (fγ) "Hfγ";
first by apply auth_auth_valid. first by apply auth_auth_valid.
set (Hheap := HeapG _ _ _ vγ fγ). set (Hheap := HeapGS _ _ _ vγ fγ).
iModIntro. iExists (λ σ _, heap_ctx σ), (λ _, True%I). iSplitL. iModIntro. iExists (λ σ _, heap_ctx σ), (λ _, True%I). iSplitL.
{ iExists ∅. by iFrame. } { iExists ∅. by iFrame. }
by iApply (Hwp (LRustG _ _ Hheap)). by iApply (Hwp (LRustGS _ _ Hheap)).
Qed. Qed.
theories/lang/lang.v → lambda-rust/lang/lang.v
View file @ 0f4ebd6d
From iris.program_logic Require Export language ectx_language ectxi_language. From iris.program_logic Require Export language ectx_language ectxi_language.
From stdpp Require Export strings binders. From stdpp Require Export strings binders.
From stdpp Require Import gmap. From stdpp Require Import gmap.
Set Default Proof Using "Type". From iris.prelude Require Import options.
Open Scope Z_scope. Global Open Scope Z_scope.
(** Expressions and vals. *) (** Expressions and vals. *)
Definition block : Set := positive. Definition block : Set := positive.
Definition loc : Set := block * Z. Definition loc : Set := block * Z.
Declare Scope loc_scope.
Bind Scope loc_scope with loc. Bind Scope loc_scope with loc.
Delimit Scope loc_scope with L. Delimit Scope loc_scope with L.
Open Scope loc_scope. Global Open Scope loc_scope.
Inductive base_lit : Set := Inductive base_lit : Set :=
| LitPoison | LitLoc (l : loc) | LitInt (n : Z). | LitPoison | LitLoc (l : loc) | LitInt (n : Z).
...@@ -42,8 +43,8 @@ Inductive expr := ...@@ -42,8 +43,8 @@ Inductive expr :=
| Case (e : expr) (el : list expr) | Case (e : expr) (el : list expr)
| Fork (e : expr). | Fork (e : expr).
Arguments App _%E _%E. Global Arguments App _%_E _%_E.
Arguments Case _%E _%E. Global Arguments Case _%_E _%_E.
Fixpoint is_closed (X : list string) (e : expr) : bool := Fixpoint is_closed (X : list string) (e : expr) : bool :=
match e with match e with
...@@ -58,9 +59,9 @@ Fixpoint is_closed (X : list string) (e : expr) : bool := ...@@ -58,9 +59,9 @@ Fixpoint is_closed (X : list string) (e : expr) : bool :=
end. end.
Class Closed (X : list string) (e : expr) := closed : is_closed X e. 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. 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. Proof. rewrite /Closed. apply _. Qed.
Inductive val := Inductive val :=
...@@ -150,27 +151,25 @@ Fixpoint subst_l (xl : list binder) (esl : list expr) (e : expr) : option expr : ...@@ -150,27 +151,25 @@ Fixpoint subst_l (xl : list binder) (esl : list expr) (e : expr) : option expr :
| x::xl, es::esl => subst' x es <$> subst_l xl esl e | x::xl, es::esl => subst' x es <$> subst_l xl esl e
| _, _ => None | _, _ => None
end. end.
Arguments subst_l _%binder _ _%E. Global Arguments subst_l _%_binder _ _%_E.
Definition subst_v (xl : list binder) (vsl : vec val (length xl)) Definition subst_v (xl : list binder) (vsl : vec val (length xl))
(e : expr) : expr := (e : expr) : expr :=
Vector.fold_right2 (λ b, subst' b ∘ of_val) e _ (list_to_vec xl) vsl. Vector.fold_right2 (λ b, subst' b ∘ of_val) e _ (list_to_vec xl) vsl.
Arguments subst_v _%binder _ _%E. Global Arguments subst_v _%_binder _ _%_E.
Lemma subst_v_eq (xl : list binder) (vsl : vec val (length xl)) e : 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. Some $ subst_v xl vsl e = subst_l xl (of_val <$> vec_to_list vsl) e.
Proof. Proof.
revert vsl. induction xl=>/= vsl; inv_vec vsl=>//=v vsl. by rewrite -IHxl. revert vsl. induction xl as [|x xl IHxl]=>/= vsl; inv_vec vsl=>//=v vsl.
by rewrite -IHxl.
Qed. Qed.
(** The stepping relation *) (** The stepping relation *)
(* Be careful to make sure that poison is always stuck when used for anything (* Be careful to make sure that poison is always stuck when used for anything
except for reading from or writing to memory! *) except for reading from or writing to memory! *)
Definition Z_of_bool (b : bool) : Z :=
if b then 1 else 0.
Definition lit_of_bool (b : bool) : base_lit := Definition lit_of_bool (b : bool) : base_lit :=
LitInt $ Z_of_bool b. LitInt $ Z.b2z b.
Definition shift_loc (l : loc) (z : Z) : loc := (l.1, l.2 + z). Definition shift_loc (l : loc) (z : Z) : loc := (l.1, l.2 + z).
...@@ -233,48 +232,48 @@ Inductive bin_op_eval (σ : state) : bin_op → base_lit → base_lit → base_l ...@@ -233,48 +232,48 @@ Inductive bin_op_eval (σ : state) : bin_op → base_lit → base_lit → base_l
Definition stuck_term := App (Lit $ LitInt 0) []. Definition stuck_term := App (Lit $ LitInt 0) [].
Inductive head_step : expr → state → list Empty_set → expr → state → list expr → Prop := Inductive base_step : expr → state → list Empty_set → expr → state → list expr → Prop :=
| BinOpS op l1 l2 l' σ : | BinOpS op l1 l2 l' σ :
bin_op_eval σ 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 σ: | BetaS f xl e e' el σ:
Forall (λ ei, is_Some (to_val ei)) el → Forall (λ ei, is_Some (to_val ei)) el →
Closed (f :b: xl +b+ []) e → Closed (f :b: xl +b+ []) e →
subst_l (f::xl) (Rec f xl e :: el) e = Some e' → subst_l (f::xl) (Rec f xl e :: el) e = Some e' →
head_step (App (Rec f xl e) el) σ [] e' σ [] base_step (App (Rec f xl e) el) σ [] e' σ []
| ReadScS l n v σ: | ReadScS l n v σ:
σ !! l = Some (RSt 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 σ: | ReadNa1S l n v σ:
σ !! l = Some (RSt 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)]>σ) (Read Na2Ord (Lit $ LitLoc l)) (<[l:=(RSt $ S n, v)]>σ)
[] []
| ReadNa2S l n v σ: | ReadNa2S l n v σ:
σ !! l = Some (RSt $ S 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)]>σ) (of_val v) (<[l:=(RSt n, v)]>σ)
[] []
| WriteScS l e v v' σ: | WriteScS l e v v' σ:
to_val e = Some v → to_val e = Some v →
σ !! l = Some (RSt 0, v') → σ !! l = Some (RSt 0, v') →
head_step (Write ScOrd (Lit $ LitLoc l) e) σ base_step (Write ScOrd (Lit $ LitLoc l) e) σ
[] []
(Lit LitPoison) (<[l:=(RSt 0, v)]>σ) (Lit LitPoison) (<[l:=(RSt 0, v)]>σ)
[] []
| WriteNa1S l e v v' σ: | WriteNa1S l e v v' σ:
to_val e = Some v → to_val e = Some v →
σ !! l = Some (RSt 0, 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')]>σ) (Write Na2Ord (Lit $ LitLoc l) e) (<[l:=(WSt, v')]>σ)
[] []
| WriteNa2S l e v v' σ: | WriteNa2S l e v v' σ:
to_val e = Some v → to_val e = Some v →
σ !! l = Some (WSt, v') → σ !! l = Some (WSt, v') →
head_step (Write Na2Ord (Lit $ LitLoc l) e) σ base_step (Write Na2Ord (Lit $ LitLoc l) e) σ
[] []
(Lit LitPoison) (<[l:=(RSt 0, v)]>σ) (Lit LitPoison) (<[l:=(RSt 0, v)]>σ)
[] []
...@@ -282,12 +281,12 @@ Inductive head_step : expr → state → list Empty_set → expr → state → l ...@@ -282,12 +281,12 @@ Inductive head_step : expr → state → list Empty_set → expr → state → l
to_val e1 = Some $ LitV lit1 → to_val e2 = Some $ LitV lit2 → to_val e1 = Some $ LitV lit1 → to_val e2 = Some $ LitV lit2 →
σ !! l = Some (RSt n, LitV litl) → σ !! l = Some (RSt n, LitV litl) →
lit_neq lit1 litl → lit_neq lit1 litl →
head_step (CAS (Lit $ LitLoc l) e1 e2) σ [] (Lit $ lit_of_bool false) σ [] base_step (CAS (Lit $ LitLoc l) e1 e2) σ [] (Lit $ lit_of_bool false) σ []
| CasSucS l e1 lit1 e2 lit2 litl σ : | CasSucS l e1 lit1 e2 lit2 litl σ :
to_val e1 = Some $ LitV lit1 → to_val e2 = Some $ LitV lit2 → to_val e1 = Some $ LitV lit1 → to_val e2 = Some $ LitV lit2 →
σ !! l = Some (RSt 0, LitV litl) → σ !! l = Some (RSt 0, LitV litl) →
lit_eq σ lit1 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)]>σ) (Lit $ lit_of_bool true) (<[l:=(RSt 0, LitV lit2)]>σ)
[] []
...@@ -309,30 +308,30 @@ Inductive head_step : expr → state → list Empty_set → expr → state → l ...@@ -309,30 +308,30 @@ Inductive head_step : expr → state → list Empty_set → expr → state → l
to_val e1 = Some $ LitV lit1 → to_val e2 = Some $ LitV lit2 → to_val e1 = Some $ LitV lit1 → to_val e2 = Some $ LitV lit2 →
σ !! l = Some (RSt n, LitV litl) → 0 < n → σ !! l = Some (RSt n, LitV litl) → 0 < n →
lit_eq σ lit1 litl → lit_eq σ lit1 litl →
head_step (CAS (Lit $ LitLoc l) e1 e2) σ base_step (CAS (Lit $ LitLoc l) e1 e2) σ
[] []
stuck_term σ stuck_term σ
[] []
| AllocS n l σ : | AllocS n l σ :
0 < n → 0 < n →
(∀ m, σ !! (l +ₗ m) = None) → (∀ m, σ !! (l +ₗ m) = None) →
head_step (Alloc $ Lit $ LitInt n) σ base_step (Alloc $ Lit $ LitInt n) σ
[] []
(Lit $ LitLoc l) (init_mem l (Z.to_nat n) σ) (Lit $ LitLoc l) (init_mem l (Z.to_nat n) σ)
[] []
| FreeS n l σ : | FreeS n l σ :
0 < n → 0 < n →
(∀ m, is_Some (σ !! (l +ₗ m)) ↔ 0 ≤ m < n) → (∀ m, is_Some (σ !! (l +ₗ m)) ↔ 0 ≤ m < n) →
head_step (Free (Lit $ LitInt n) (Lit $ LitLoc l)) σ base_step (Free (Lit $ LitInt n) (Lit $ LitLoc l)) σ
[] []
(Lit LitPoison) (free_mem l (Z.to_nat n) σ) (Lit LitPoison) (free_mem l (Z.to_nat n) σ)
[] []
| CaseS i el e σ : | CaseS i el e σ :
0 ≤ i → 0 ≤ i →
el !! (Z.to_nat i) = Some e → el !! (Z.to_nat i) = Some e →
head_step (Case (Lit $ LitInt i) el) σ [] e σ [] base_step (Case (Lit $ LitInt i) el) σ [] e σ []
| ForkS e σ: | ForkS e σ:
head_step (Fork e) σ [] (Lit LitPoison) σ [e]. base_step (Fork e) σ [] (Lit LitPoison) σ [e].
(** Basic properties about the language *) (** Basic properties about the language *)
Lemma to_of_val v : to_val (of_val v) = Some v. Lemma to_of_val v : to_val (of_val v) = Some v.
...@@ -345,10 +344,10 @@ Proof. ...@@ -345,10 +344,10 @@ Proof.
revert v; induction e; intros v ?; simplify_option_eq; auto with f_equal. revert v; induction e; intros v ?; simplify_option_eq; auto with f_equal.
Qed. 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. 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. Proof. destruct Ki; intros ???; simplify_eq/=; auto with f_equal. Qed.
Lemma fill_item_val Ki e : Lemma fill_item_val Ki e :
...@@ -356,11 +355,11 @@ Lemma fill_item_val Ki e : ...@@ -356,11 +355,11 @@ Lemma fill_item_val Ki e :
Proof. intros [v ?]. destruct Ki; simplify_option_eq; eauto. Qed. Proof. intros [v ?]. destruct Ki; simplify_option_eq; eauto. Qed.
Lemma val_stuck e1 σ1 κ e2 σ2 ef : Lemma val_stuck e1 σ1 κ e2 σ2 ef :
head_step e1 σ1 κ e2 σ2 ef → to_val e1 = None. base_step e1 σ1 κ e2 σ2 ef → to_val e1 = None.
Proof. destruct 1; naive_solver. Qed. Proof. destruct 1; naive_solver. Qed.
Lemma head_ctx_step_val Ki e σ1 κ e2 σ2 ef : Lemma base_ctx_step_val Ki e σ1 κ e2 σ2 ef :
head_step (fill_item Ki e) σ1 κ e2 σ2 ef → is_Some (to_val e). base_step (fill_item Ki e) σ1 κ e2 σ2 ef → is_Some (to_val e).
Proof. Proof.
destruct Ki; inversion_clear 1; decompose_Forall_hyps; destruct Ki; inversion_clear 1; decompose_Forall_hyps;
simplify_option_eq; by eauto. simplify_option_eq; by eauto.
...@@ -371,7 +370,8 @@ Lemma list_expr_val_eq_inv vl1 vl2 e1 e2 el1 el2 : ...@@ -371,7 +370,8 @@ Lemma list_expr_val_eq_inv vl1 vl2 e1 e2 el1 el2 :
map of_val vl1 ++ e1 :: el1 = map of_val vl2 ++ e2 :: el2 → map of_val vl1 ++ e1 :: el1 = map of_val vl2 ++ e2 :: el2 →
vl1 = vl2 ∧ el1 = el2. vl1 = vl2 ∧ el1 = el2.
Proof. 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. - done.
- subst. by rewrite to_of_val in H1. - subst. by rewrite to_of_val in H1.
- subst. by rewrite to_of_val in H2. - subst. by rewrite to_of_val in H2.
...@@ -401,8 +401,8 @@ Proof. rewrite /shift_loc /=. f_equal. lia. Qed. ...@@ -401,8 +401,8 @@ Proof. rewrite /shift_loc /=. f_equal. lia. Qed.
Lemma shift_loc_0_nat l : 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. Proof. destruct l as [b o]. rewrite /shift_loc /=. f_equal. lia. Qed.
Instance shift_loc_inj l : Inj (=) (=) (shift_loc l). Global Instance shift_loc_inj l : Inj (=) (=) (shift_loc l).
Proof. destruct l as [b o]; intros n n' [=?]; lia. Qed. Proof. destruct l as [b o]; intros n n' [= ?]; lia. Qed.
Lemma shift_loc_block l n : (l +ₗ n).1 = l.1. Lemma shift_loc_block l n : (l +ₗ n).1 = l.1.
Proof. done. Qed. Proof. done. Qed.
...@@ -429,14 +429,14 @@ Proof. ...@@ -429,14 +429,14 @@ Proof.
Qed. Qed.
Definition fresh_block (σ : state) : block := Definition fresh_block (σ : state) : block :=
let loclst : list loc := elements (dom _ σ : gset loc) in let loclst : list loc := elements (dom σ : gset loc) in
let blockset : gset block := foldr (λ l, ({[l.1]} ∪)) ∅ loclst in let blockset : gset block := foldr (λ l, ({[l.1]} ∪.)) ∅ loclst in
fresh blockset. fresh blockset.
Lemma is_fresh_block σ i : σ !! (fresh_block σ,i) = None. Lemma is_fresh_block σ i : σ !! (fresh_block σ,i) = None.
Proof. Proof.
assert (∀ (l : loc) ls (X : gset block), 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. } { induction 1; set_solver. }
rewrite /fresh_block /shift_loc /= -(not_elem_of_dom (D := gset loc)) -elem_of_elements. rewrite /fresh_block /shift_loc /= -(not_elem_of_dom (D := gset loc)) -elem_of_elements.
move=> /(help _ _ ∅) /=. apply is_fresh. move=> /(help _ _ ∅) /=. apply is_fresh.
...@@ -446,9 +446,9 @@ Lemma alloc_fresh n σ : ...@@ -446,9 +446,9 @@ Lemma alloc_fresh n σ :
let l := (fresh_block σ, 0) in let l := (fresh_block σ, 0) in
let init := repeat (LitV $ LitInt 0) (Z.to_nat n) in let init := repeat (LitV $ LitInt 0) (Z.to_nat n) in
0 < n → 0 < n →
head_step (Alloc $ Lit $ LitInt n) σ [] (Lit $ LitLoc l) (init_mem l (Z.to_nat n) σ) []. base_step (Alloc $ Lit $ LitInt n) σ [] (Lit $ LitLoc l) (init_mem l (Z.to_nat n) σ) [].
Proof. Proof.
intros l init Hn. apply AllocS. auto. intros l init Hn. apply AllocS; first done.
- intros i. apply (is_fresh_block _ i). - intros i. apply (is_fresh_block _ i).
Qed. Qed.
...@@ -468,11 +468,13 @@ Qed. ...@@ -468,11 +468,13 @@ Qed.
(** Closed expressions *) (** Closed expressions *)
Lemma is_closed_weaken X Y e : is_closed X e → X ⊆ Y → is_closed Y e. Lemma is_closed_weaken X Y e : is_closed X e → X ⊆ Y → is_closed Y e.
Proof. Proof.
revert e X Y. fix FIX 1; destruct e=>X Y/=; try naive_solver. revert e X Y. fix FIX 1; intros e; destruct e=>X Y/=; try naive_solver.
- naive_solver set_solver. - 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. 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. induction el=>/=; naive_solver.
Qed. Qed.
...@@ -481,12 +483,16 @@ Proof. intros. by apply is_closed_weaken with [], list_subseteq_nil. Qed. ...@@ -481,12 +483,16 @@ Proof. intros. by apply is_closed_weaken with [], list_subseteq_nil. Qed.
Lemma is_closed_subst X e x es : is_closed X e → x ∉ X → subst x es e = e. Lemma is_closed_subst X e x es : is_closed X e → x ∉ X → subst x es e = e.
Proof. Proof.
revert e X. fix FIX 1; destruct e=> X /=; rewrite ?bool_decide_spec ?andb_True=> He ?; revert e X. fix FIX 1; intros e; destruct e=> X /=; rewrite ?bool_decide_spec ?andb_True=> He ?;
repeat case_bool_decide; simplify_eq/=; f_equal; repeat case_bool_decide; simplify_eq/=; f_equal;
try by intuition eauto with set_solver. 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. 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. f_equal; intuition eauto with set_solver.
Qed. Qed.
...@@ -502,14 +508,18 @@ Proof. intros <-%of_to_val. apply is_closed_of_val. Qed. ...@@ -502,14 +508,18 @@ Proof. intros <-%of_to_val. apply is_closed_of_val. Qed.
Lemma subst_is_closed X x es e : Lemma subst_is_closed X x es e :
is_closed X es → is_closed (x::X) e → is_closed X (subst x es e). is_closed X es → is_closed (x::X) e → is_closed X (subst x es e).
Proof. Proof.
revert e X. fix FIX 1; destruct e=>X //=; repeat (case_bool_decide=>//=); revert e X. fix FIX 1; intros e; destruct e=>X //=; repeat (case_bool_decide=>//=);
try naive_solver; rewrite ?andb_True; intros. try naive_solver; rewrite ?andb_True; intros.
- set_solver. - set_solver.
- eauto using is_closed_weaken with set_solver. - eauto using is_closed_weaken with set_solver.
- eapply is_closed_weaken; first done. - 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. destruct (decide (BNamed x = f)), (decide (BNamed x ∈ xl)); set_solver.
- split; first naive_solver. induction el; naive_solver. - split; first naive_solver.
- split; first naive_solver. induction el; 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. Qed.
Lemma subst'_is_closed X b es e : Lemma subst'_is_closed X b es e :
...@@ -530,16 +540,16 @@ Proof. ...@@ -530,16 +540,16 @@ Proof.
Qed. Qed.
(* Misc *) (* Misc *)
Lemma stuck_not_head_step σ e' κ σ' ef : Lemma stuck_not_base_step σ e' κ σ' ef :
¬head_step stuck_term σ e' κ σ' ef. ¬base_step stuck_term σ e' κ σ' ef.
Proof. inversion 1. Qed. Proof. inversion 1. Qed.
(** Equality and other typeclass stuff *) (** 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. 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. Proof. solve_decision. Defined.
Instance un_op_dec_eq : EqDecision order. Global Instance un_op_dec_eq : EqDecision order.
Proof. solve_decision. Defined. Proof. solve_decision. Defined.
Fixpoint expr_beq (e : expr) (e' : expr) : bool := Fixpoint expr_beq (e : expr) (e' : expr) : bool :=
...@@ -570,41 +580,41 @@ Fixpoint expr_beq (e : expr) (e' : expr) : bool := ...@@ -570,41 +580,41 @@ Fixpoint expr_beq (e : expr) (e' : expr) : bool :=
end. end.
Lemma expr_beq_correct (e1 e2 : expr) : expr_beq e1 e2 ↔ e1 = e2. Lemma expr_beq_correct (e1 e2 : expr) : expr_beq e1 e2 ↔ e1 = e2.
Proof. Proof.
revert e1 e2; fix FIX 1. revert e1 e2; fix FIX 1. intros e1 e2.
destruct e1 as [| | | |? el1| | | | | |? el1|], destruct e1 as [| | | |? el1| | | | | |? el1|],
e2 as [| | | |? el2| | | | | |? el2|]; simpl; try done; e2 as [| | | |? el2| | | | | |? el2|]; simpl; try done;
rewrite ?andb_True ?bool_decide_spec ?FIX; rewrite ?andb_True ?bool_decide_spec ?FIX;
try (split; intro; [destruct_and?|split_and?]; congruence). try (split; intro; [destruct_and?|split_and?]; congruence).
- match goal with |- context [?F el1 el2] => assert (F el1 el2 ↔ el1 = el2) end. - match goal with |- context [?F el1 el2] => assert (F el1 el2 ↔ el1 = el2) end.
{ revert el2. induction el1 as [|el1h el1q]; destruct el2; try done. { revert el2. induction el1 as [|el1h el1q]; intros el2; destruct el2; try done.
specialize (FIX el1h). naive_solver. } specialize (FIX el1h). naive_solver. }
clear FIX. naive_solver. clear FIX. naive_solver.
- match goal with |- context [?F el1 el2] => assert (F el1 el2 ↔ el1 = el2) end. - match goal with |- context [?F el1 el2] => assert (F el1 el2 ↔ el1 = el2) end.
{ revert el2. induction el1 as [|el1h el1q]; destruct el2; try done. { revert el2. induction el1 as [|el1h el1q]; intros el2; destruct el2; try done.
specialize (FIX el1h). naive_solver. } specialize (FIX el1h). naive_solver. }
clear FIX. naive_solver. clear FIX. naive_solver.
Qed. Qed.
Instance expr_dec_eq : EqDecision expr. Global Instance expr_dec_eq : EqDecision expr.
Proof. Proof.
refine (λ e1 e2, cast_if (decide (expr_beq e1 e2))); by rewrite -expr_beq_correct. refine (λ e1 e2, cast_if (decide (expr_beq e1 e2))); by rewrite -expr_beq_correct.
Defined. Defined.
Instance val_dec_eq : EqDecision val. Global Instance val_dec_eq : EqDecision val.
Proof. Proof.
refine (λ v1 v2, cast_if (decide (of_val v1 = of_val v2))); abstract naive_solver. refine (λ v1 v2, cast_if (decide (of_val v1 = of_val v2))); abstract naive_solver.
Defined. Defined.
Instance expr_inhabited : Inhabited expr := populate (Lit LitPoison). Global Instance expr_inhabited : Inhabited expr := populate (Lit LitPoison).
Instance val_inhabited : Inhabited val := populate (LitV LitPoison). Global Instance val_inhabited : Inhabited val := populate (LitV LitPoison).
Canonical Structure stateO := leibnizO state. Canonical Structure stateO := leibnizO state.
Canonical Structure valO := leibnizO val. Canonical Structure valO := leibnizO val.
Canonical Structure exprO := leibnizO expr. Canonical Structure exprO := leibnizO expr.
(** Language *) (** Language *)
Lemma lrust_lang_mixin : EctxiLanguageMixin of_val to_val fill_item head_step. Lemma lrust_lang_mixin : EctxiLanguageMixin of_val to_val fill_item base_step.
Proof. Proof.
split; apply _ || eauto using to_of_val, of_to_val, split; apply _ || eauto using to_of_val, of_to_val,
val_stuck, fill_item_val, fill_item_no_val_inj, head_ctx_step_val. val_stuck, fill_item_val, fill_item_no_val_inj, base_ctx_step_val.
Qed. Qed.
Canonical Structure lrust_ectxi_lang := EctxiLanguage lrust_lang_mixin. Canonical Structure lrust_ectxi_lang := EctxiLanguage lrust_lang_mixin.
Canonical Structure lrust_ectx_lang := EctxLanguageOfEctxi lrust_ectxi_lang. Canonical Structure lrust_ectx_lang := EctxLanguageOfEctxi lrust_ectxi_lang.
...@@ -614,7 +624,7 @@ Canonical Structure lrust_lang := LanguageOfEctx lrust_ectx_lang. ...@@ -614,7 +624,7 @@ Canonical Structure lrust_lang := LanguageOfEctx lrust_ectx_lang.
Lemma stuck_irreducible K σ : irreducible (fill K stuck_term) σ. Lemma stuck_irreducible K σ : irreducible (fill K stuck_term) σ.
Proof. Proof.
apply: (irreducible_fill (K:=ectx_language.fill K)); first done. apply: (irreducible_fill (K:=ectx_language.fill K)); first done.
apply prim_head_irreducible; unfold stuck_term. apply prim_base_irreducible; unfold stuck_term.
- inversion 1. - inversion 1.
- apply ectxi_language_sub_redexes_are_values. - apply ectxi_language_sub_redexes_are_values.
intros [] ??; simplify_eq/=; eauto; discriminate_list. intros [] ??; simplify_eq/=; eauto; discriminate_list.
......
theories/lang/lib/lock.v → lambda-rust/lang/lib/lock.v
View file @ 0f4ebd6d
From iris.program_logic Require Import weakestpre. From iris.program_logic Require Import weakestpre.
From iris.proofmode Require Import tactics. From iris.proofmode Require Import proofmode.
From iris.algebra Require Import excl. From iris.algebra Require Import excl.
From lrust.lang Require Import lang proofmode notation. From lrust.lang Require Import lang proofmode notation.
Set Default Proof Using "Type". From iris.prelude Require Import options.
Definition mklock_unlocked : val := λ: ["l"], "l" <- #false. Definition mklock_unlocked : val := λ: ["l"], "l" <- #false.
Definition mklock_locked : val := λ: ["l"], "l" <- #true. Definition mklock_locked : val := λ: ["l"], "l" <- #true.
...@@ -16,13 +16,15 @@ Definition release : val := λ: ["l"], "l" <-ˢᶜ #false. ...@@ -16,13 +16,15 @@ Definition release : val := λ: ["l"], "l" <-ˢᶜ #false.
their cancelling view shift has a non-empty mask, and it would have to be their cancelling view shift has a non-empty mask, and it would have to be
executed in the consequence view shift of a borrow. *) executed in the consequence view shift of a borrow. *)
Section proof. Section proof.
Context `{!lrustG Σ}. Context `{!lrustGS Σ}.
Definition lock_proto (l : loc) (R : iProp Σ) : iProp Σ := Definition lock_proto (l : loc) (R : iProp Σ) : iProp Σ :=
(∃ b : bool, l ↦ #b ∗ if b then True else R)%I. (∃ b : bool, l ↦ #b ∗ if b then True else R)%I.
Global Instance lock_proto_ne l : NonExpansive (lock_proto l). Global Instance lock_proto_ne l : NonExpansive (lock_proto l).
Proof. solve_proper. Qed. 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' : Lemma lock_proto_iff l R R' :
□ (R ↔ R') -∗ lock_proto l R -∗ lock_proto l R'. □ (R ↔ R') -∗ lock_proto l R -∗ lock_proto l R'.
...@@ -34,9 +36,9 @@ Section proof. ...@@ -34,9 +36,9 @@ Section proof.
Lemma lock_proto_iff_proper l R R' : Lemma lock_proto_iff_proper l R R' :
□ (R ↔ R') -∗ □ (lock_proto l R ↔ lock_proto l R'). □ (R ↔ R') -∗ □ (lock_proto l R ↔ lock_proto l R').
Proof. Proof.
iIntros "#HR !#". iSplit; iIntros "Hlck"; iApply (lock_proto_iff with "[HR] Hlck"). iIntros "#HR !>". iSplit; iIntros "Hlck"; iApply (lock_proto_iff with "[HR] Hlck").
- done. - done.
- iAlways; iSplit; iIntros; by iApply "HR". - iModIntro; iSplit; iIntros; by iApply "HR".
Qed. Qed.
(** The main proofs. *) (** The main proofs. *)
...@@ -75,7 +77,7 @@ Section proof. ...@@ -75,7 +77,7 @@ Section proof.
{{{ P }}} try_acquire [ #l ] @ E {{{ P }}} try_acquire [ #l ] @ E
{{{ b, RET #b; (if b is true then R else True) ∗ P }}}. {{{ b, RET #b; (if b is true then R else True) ∗ P }}}.
Proof. Proof.
iIntros "#Hproto !# * HP HΦ". iIntros "#Hproto !> * HP HΦ".
wp_rec. iMod ("Hproto" with "HP") as "(Hinv & Hclose)". wp_rec. iMod ("Hproto" with "HP") as "(Hinv & Hclose)".
iDestruct "Hinv" as ([]) "[Hl HR]". iDestruct "Hinv" as ([]) "[Hl HR]".
- wp_apply (wp_cas_int_fail with "Hl"); [done..|]. iIntros "Hl". - wp_apply (wp_cas_int_fail with "Hl"); [done..|]. iIntros "Hl".
...@@ -90,7 +92,7 @@ Section proof. ...@@ -90,7 +92,7 @@ Section proof.
□ (P ={E,∅}=∗ ▷ lock_proto l R ∗ (▷ lock_proto l R ={∅,E}=∗ P)) -∗ □ (P ={E,∅}=∗ ▷ lock_proto l R ∗ (▷ lock_proto l R ={∅,E}=∗ P)) -∗
{{{ P }}} acquire [ #l ] @ E {{{ RET #☠; R ∗ P }}}. {{{ P }}} acquire [ #l ] @ E {{{ RET #☠; R ∗ P }}}.
Proof. Proof.
iIntros "#Hproto !# * HP HΦ". iLöb as "IH". wp_rec. iIntros "#Hproto !> * HP HΦ". iLöb as "IH". wp_rec.
wp_apply (try_acquire_spec with "Hproto HP"). iIntros ([]). wp_apply (try_acquire_spec with "Hproto HP"). iIntros ([]).
- iIntros "[HR Hown]". wp_if. iApply "HΦ"; iFrame. - iIntros "[HR Hown]". wp_if. iApply "HΦ"; iFrame.
- iIntros "[_ Hown]". wp_if. iApply ("IH" with "Hown HΦ"). - iIntros "[_ Hown]". wp_if. iApply ("IH" with "Hown HΦ").
...@@ -100,11 +102,11 @@ Section proof. ...@@ -100,11 +102,11 @@ Section proof.
□ (P ={E,∅}=∗ ▷ lock_proto l R ∗ (▷ lock_proto l R ={∅,E}=∗ P)) -∗ □ (P ={E,∅}=∗ ▷ lock_proto l R ∗ (▷ lock_proto l R ={∅,E}=∗ P)) -∗
{{{ R ∗ P }}} release [ #l ] @ E {{{ RET #☠; P }}}. {{{ R ∗ P }}} release [ #l ] @ E {{{ RET #☠; P }}}.
Proof. Proof.
iIntros "#Hproto !# * (HR & HP) HΦ". wp_let. iIntros "#Hproto !> * (HR & HP) HΦ". wp_let.
iMod ("Hproto" with "HP") as "(Hinv & Hclose)". iMod ("Hproto" with "HP") as "(Hinv & Hclose)".
iDestruct "Hinv" as (b) "[? _]". wp_write. iApply "HΦ". iDestruct "Hinv" as (b) "[? _]". wp_write. iApply "HΦ".
iApply "Hclose". iExists false. by iFrame. iApply "Hclose". iExists false. by iFrame.
Qed. Qed.
End proof. End proof.
Typeclasses Opaque lock_proto. Global Typeclasses Opaque lock_proto.
theories/lang/lib/memcpy.v → lambda-rust/lang/lib/memcpy.v
View file @ 0f4ebd6d
From lrust.lang Require Export notation. From lrust.lang Require Export notation.
From lrust.lang Require Import heap proofmode. From lrust.lang Require Import heap proofmode.
Set Default Proof Using "Type". From iris.prelude Require Import options.
Definition memcpy : val := Definition memcpy : val :=
rec: "memcpy" ["dst";"len";"src"] := rec: "memcpy" ["dst";"len";"src"] :=
...@@ -19,7 +19,7 @@ Notation "e1 <-{ n ',Σ' i } ! e2" := ...@@ -19,7 +19,7 @@ Notation "e1 <-{ n ',Σ' i } ! e2" :=
(at level 80, n, i at next level, (at level 80, n, i at next level,
format "e1 <-{ n ,Σ i } ! e2") : expr_scope. format "e1 <-{ n ,Σ i } ! e2") : expr_scope.
Lemma wp_memcpy `{!lrustG Σ} E l1 l2 vl1 vl2 q (n : Z): Lemma wp_memcpy `{!lrustGS Σ} E l1 l2 vl1 vl2 q (n : Z):
Z.of_nat (length vl1) = n → Z.of_nat (length vl2) = n → Z.of_nat (length vl1) = n → Z.of_nat (length vl2) = n →
{{{ l1 ↦∗ vl1 ∗ l2 ↦∗{q} vl2 }}} {{{ l1 ↦∗ vl1 ∗ l2 ↦∗{q} vl2 }}}
#l1 <-{n} !#l2 @ E #l1 <-{n} !#l2 @ E
...@@ -30,7 +30,7 @@ Proof. ...@@ -30,7 +30,7 @@ Proof.
- iApply "HΦ". assert (n = O) by lia; subst. - iApply "HΦ". assert (n = O) by lia; subst.
destruct vl1, vl2; try discriminate. by iFrame. destruct vl1, vl2; try discriminate. by iFrame.
- destruct vl1 as [|v1 vl1], vl2 as [|v2 vl2], n as [|n|]; try (discriminate || lia). - destruct vl1 as [|v1 vl1], vl2 as [|v2 vl2], n as [|n|]; try (discriminate || lia).
revert Hvl1 Hvl2. intros [= Hvl1] [= Hvl2]; rewrite !heap_mapsto_vec_cons. subst n. revert Hvl1 Hvl2. intros [= Hvl1] [= Hvl2]; rewrite !heap_pointsto_vec_cons. subst n.
iDestruct "Hl1" as "[Hv1 Hl1]". iDestruct "Hl2" as "[Hv2 Hl2]". iDestruct "Hl1" as "[Hv1 Hl1]". iDestruct "Hl2" as "[Hv2 Hl2]".
Local Opaque Zminus. Local Opaque Zminus.
wp_read; wp_write. do 3 wp_op. iApply ("IH" with "[%] [%] Hl1 Hl2"); [lia..|]. wp_read; wp_write. do 3 wp_op. iApply ("IH" with "[%] [%] Hl1 Hl2"); [lia..|].
......
theories/lang/lib/new_delete.v → lambda-rust/lang/lib/new_delete.v
View file @ 0f4ebd6d
From lrust.lang Require Export notation. From lrust.lang Require Export notation.
From lrust.lang Require Import heap proofmode memcpy. From lrust.lang Require Import heap proofmode memcpy.
Set Default Proof Using "Type". From iris.prelude Require Import options.
Definition new : val := Definition new : val :=
λ: ["n"], λ: ["n"],
...@@ -13,7 +13,7 @@ Definition delete : val := ...@@ -13,7 +13,7 @@ Definition delete : val :=
else Free "n" "loc". else Free "n" "loc".
Section specs. Section specs.
Context `{!lrustG Σ}. Context `{!lrustGS Σ}.
Lemma wp_new E n: Lemma wp_new E n:
0 ≤ n → 0 ≤ n →
...@@ -23,8 +23,8 @@ Section specs. ...@@ -23,8 +23,8 @@ Section specs.
Proof. Proof.
iIntros (? Φ) "_ HΦ". wp_lam. wp_op; case_bool_decide. iIntros (? Φ) "_ HΦ". wp_lam. wp_op; case_bool_decide.
- wp_if. assert (n = 0) as -> by lia. iApply "HΦ". - wp_if. assert (n = 0) as -> by lia. iApply "HΦ".
rewrite heap_mapsto_vec_nil. auto. rewrite heap_pointsto_vec_nil. auto.
- wp_if. wp_alloc l as "H↦" "H†". lia. iApply "HΦ". subst sz. iFrame. - wp_if. wp_alloc l as "H↦" "H†"; first lia. iApply "HΦ". subst. iFrame.
Qed. Qed.
Lemma wp_delete E (n:Z) l vl : Lemma wp_delete E (n:Z) l vl :
......