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
  • ci/ike/frame_exist
  • ci/janno/reduction_no_check
  • ci/janno/strict-tc-resolution
  • ci/pinning
  • ci/places
  • ci/pm_red
  • ci/ralf/const-rf
  • ci/ralf/sections
  • ci/weak_mem
  • coqbug/match
  • ghostcell
  • gpirlea/pin_semantic
  • gpirlea/pinning
  • jh/closures
  • jh/dynamic_masks
  • jh/lifetime_no_dead_trade
  • jh/typecheck_foo
  • master
  • masters/rusthornbelt
  • masters/weak_mem
  • msammler/new-contractive
  • msammler/rustverify_talk
  • notations
  • ralf/acc
  • ralf/prop-level-wand
  • refmut_sync
  • robbert/Z_of_nat
  • robbert/sprop
  • rusthornbelt
  • skiplist
  • step_indexing_controlled_by_ghosts
  • strong_cas_fail
  • xldenis/option
  • xldenis/pldi-submission
  • xldenis/smallvec-push
  • xldenis/type-sum
  • yusuke/tlist_for_prophecy
  • RBrlx-POPL20-artifact
  • popl18
  • popl18-aec
40 results

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
  • ci/debug
  • ci/gen_proofmode
  • ci/iris-dev-performance
  • ci/janno/reduction_no_check
  • ci/joe/compact_ipm
  • ci/joe/compact_ipm_remaining
  • ci/joe/compact_ipm_simple
  • ci/pm_red
  • ci/ralf/const-rf
  • ci/ralf/exact_vm
  • ci/ralf/sections
  • ci/ralf/weak_mem
  • ci/robbert/faster_iDestruct
  • ci/robbert/faster_iDestruct2
  • ci/robbert/faster_iFresh
  • ci/robbert/faster_iFresh_joe
  • ci/robbert/naive_solver
  • ci/robbert/pm_faster_alt
  • ci/weak_mem
  • coqbug/match
  • fast_string
  • feature/ty_own_loc
  • fnlft
  • gen_big_op
  • iris-update
  • jh/bug
  • jh/closures
  • jh/dynamic_masks
  • jh/lifetime_no_dead_trade
  • jh/ofe_problems
  • jh/popl_submission
  • jh/typecheck_foo
  • jh/undiscriminated_hintdb
  • jh_nondependent_expr
  • master
  • new_lifetime_logic
  • no-opaque
  • notations
  • ralf/acc
  • ralf/anomaly
  • ralf/call
  • ralf/old-asval
  • ralf/prophecy
  • ralf/sections-open
  • skiplist
  • strong_cas_fail
  • stuck
  • popl18
  • popl18-aec
49 results
Show changes
Commits on Source (309)
209 additional commits have been omitted to prevent performance issues.
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
*.vio
*.v.d
*.vos
*.vok
.coqdeps.d
.Makefile.coq.d
*.glob
*.cache
*.aux
......@@ -10,7 +13,7 @@
*~
*.bak
.coq-native/
build-dep/
builddep/
Makefile.coq
Makefile.coq.conf
_opam
.gitlab-ci.yml
View file @ 0f4ebd6d
......@@ -5,6 +5,7 @@ stages:
variables:
CPU_CORES: "10"
OCAML: "ocaml-variants.4.14.0+options ocaml-option-flambda"
.template: &template
stage: build
......@@ -16,10 +17,10 @@ variables:
cache:
key: "$CI_JOB_NAME"
paths:
- opamroot/
- _opam/
only:
- master
- /^ci/
- /^master/@iris/lambda-rust
- /^ci/@iris/lambda-rust
except:
- triggers
- schedules
......@@ -27,32 +28,42 @@ variables:
## Build jobs
build-coq.dev:
build-coq.9.0.0:
<<: *template
variables:
OCAML: "ocaml-base-compiler.4.07.0"
OPAM_PINS: "coq version dev"
build-coq.8.9.0:
<<: *template
variables:
OPAM_PINS: "coq version 8.9.0"
OPAM_PKG: "coq-lambda-rust"
TIMING_CONF: "coq-8.9.0"
OPAM_PINS: "coq version 9.0.0"
DENY_WARNINGS: "1"
MANGLE_NAMES: "1"
# Mostly to make the lifetime logic available
OPAM_PKG: "1"
tags:
- fp-timing
build-coq.8.8.2:
trigger-iris.timing:
<<: *template
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
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:
only:
- triggers
- schedules
- api
refs:
- triggers
- 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
license, included below.
------------------------------------------------------------------------------
Copyright: lambdaRust developers and contributors
BSD LICENCE
------------------------------------------------------------------------------
Redistribution and use in source and binary forms, with or without
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
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 <organization> nor the
names of its contributors may be used to endorse or promote products
derived from this software without specific prior written permission.
* 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 <COPYRIGHT HOLDER> BE LIABLE FOR ANY
DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
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
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
View file @ 0f4ebd6d
# Forward most targets to Coq makefile (with some trick to make this phony)
%: Makefile.coq phony
+@make -f Makefile.coq $@
# Default target
all: Makefile.coq
+@make -f Makefile.coq all
+@$(MAKE) -f Makefile.coq all
.PHONY: all
# Permit local customization
-include Makefile.local
# Forward most targets to Coq makefile (with some trick to make this phony)
%: Makefile.coq phony
@#echo "Forwarding $@"
+@$(MAKE) -f Makefile.coq $@
phony: ;
.PHONY: phony
clean: Makefile.coq
+@make -f Makefile.coq clean
find theories tests \( -name "*.d" -o -name "*.vo" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete || true
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
"$(COQBIN)coq_makefile" -f _CoqProject -o Makefile.coq
"$(COQBIN)coq_makefile" -f _CoqProject -o Makefile.coq $(EXTRA_COQFILES)
# Install build-dependencies
build-dep/opam: opam Makefile
@echo "# Creating build-dep package."
@mkdir -p build-dep
@sed <opam -E 's/^(build|install|remove):.*/\1: []/; s/^name: *"(.*)" */name: "\1-builddep"/' >build-dep/opam
@fgrep builddep build-dep/opam >/dev/null || (echo "sed failed to fix the package name" && exit 1) # sanity check
build-dep: build-dep/opam phony
@# We want opam to not just instal the build-deps now, but to also keep satisfying these
OPAMFILES=$(wildcard *.opam)
BUILDDEPFILES=$(addsuffix -builddep.opam, $(addprefix builddep/,$(basename $(OPAMFILES))))
builddep/%-builddep.opam: %.opam Makefile
@echo "# Creating builddep package for $<."
@mkdir -p builddep
@sed <$< -E 's/^(build|install|remove):.*/\1: []/; s/"(.*)"(.*= *version.*)$$/"\1-builddep"\2/;' >$@
builddep-opamfiles: $(BUILDDEPFILES)
.PHONY: builddep-opamfiles
builddep: builddep-opamfiles
@# We want opam to not just install the build-deps now, but to also keep satisfying these
@# constraints. Otherwise, `opam upgrade` may well update some packages to versions
@# that are incompatible with our build requirements.
@# To achieve this, we create a fake opam package that has our build-dependencies as
@# dependencies, but does not actually install anything itself.
@echo "# Pinning build-dep package." && \
if opam --version | grep "^1\." -q; then \
BUILD_DEP_PACKAGE="$$(egrep "^name:" build-dep/opam | sed 's/^name: *"\(.*\)" */\1/')" && \
opam pin add -k path $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE".dev build-dep && \
opam reinstall $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE"; \
else \
opam install $(OPAMFLAGS) build-dep/; \
fi
# Some files that do *not* need to be forwarded to Makefile.coq
Makefile: ;
_CoqProject: ;
opam: ;
# Phony wildcard targets
phony: ;
.PHONY: phony
@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 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)
# 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
......
README.md
View file @ 0f4ebd6d
......@@ -6,12 +6,12 @@ This is the Coq development accompanying lambda-Rust.
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)
## 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:
opam repo add coq-released https://coq.inria.fr/opam/released
......@@ -52,6 +52,26 @@ followed by `make build-dep`.
`thread::spawn`, `take_mut::take`, `alias::once` as well as converting `&&T`
to `&Box<T>`.
## Changes since original RustBelt publication
In this section we list fundamental changes to the model that were done since
the publication of the
[original RustBelt paper](https://plv.mpi-sws.org/rustbelt/popl18/).
### Support for branding
As part of the [GhostCell paper](http://plv.mpi-sws.org/rustbelt/ghostcell/),
the model was adjusted to support branding.
* The semantic interpretation of external lifetime contexts had to be changed to use a *syntactic* form of lifetime inclusion.
* This changed interpretation broke the proof of "lifetime equalization".
Instead we prove a weaker rule that only substitutes lifetimes on positions that are compatible with *semantic* lifetime inclusion.
This is good enough for [the example](theories/typing/examples/nonlexical.v).
* Furthermore, we had to redo the proof of `type_call_iris'`, a key lemma involved in calling functions and ensuring that their assumptions about lifetime parameters do indeed hold.
The old proof exploited *semantic* lifetime inclusion in external lifetime contexts in a crucial step.
The proof was fixed by adjusting the semantic interpretation of the local lifetime context.
In particular there is a new parameter `qmax` here that has to be threaded through everywhere.
## Where to Find the Proof Rules From the Paper
### Type System Rules
......@@ -91,7 +111,7 @@ borrows" in the Coq development.
| F-endlft | programs.v | type_endlft |
| F-call | function.v | type_call' |
Some of these lemmas are called `something'` because the version without the `'` is a derived, more speicalized form used together with our eauto-based `solve_typing` tactic. You can see this tactic in action in the [examples](theories/typing/examples) subfolder.
Some of these lemmas are called `something'` because the version without the `'` is a derived, more specialized form used together with our eauto-based `solve_typing` tactic. You can see this tactic in action in the [examples](theories/typing/examples) subfolder.
### Lifetime Logic Rules
......
_CoqProject
View file @ 0f4ebd6d
-Q theories lrust
# We sometimes want to locally override notation and there is no good way to do that with scopes.
# Search paths for all packages. They must all match the regex
# `-Q $PACKAGE[/ ]` so that we can filter out the right ones for each package.
-Q lifetime lrust.lifetime
-Q lambda-rust/lang lrust.lang
-Q lambda-rust/typing lrust.typing
# We sometimes want to locally override notation, and there is no good way to do that with scopes.
-arg -w -arg -notation-overridden
# non-canonical projections (https://github.com/coq/coq/pull/10076) do not exist yet in 8.9.
# Cannot use non-canonical projections as it causes massive unification failures
# (https://github.com/coq/coq/issues/6294).
-arg -w -arg -redundant-canonical-projection
# change_no_check does not exist yet in 8.9.
-arg -w -arg -convert_concl_no_check
# Warning is often incorrect, see https://gitlab.mpi-sws.org/iris/stdpp/-/issues/216
-arg -w -arg -notation-incompatible-prefix
theories/lifetime/model/definitions.v
theories/lifetime/model/faking.v
theories/lifetime/model/creation.v
theories/lifetime/model/primitive.v
theories/lifetime/model/accessors.v
theories/lifetime/model/borrow.v
theories/lifetime/model/borrow_sep.v
theories/lifetime/model/reborrow.v
theories/lifetime/lifetime_sig.v
theories/lifetime/lifetime.v
theories/lifetime/at_borrow.v
theories/lifetime/na_borrow.v
theories/lifetime/frac_borrow.v
theories/lang/adequacy.v
theories/lang/heap.v
theories/lang/lang.v
theories/lang/lifting.v
theories/lang/notation.v
theories/lang/proofmode.v
theories/lang/races.v
theories/lang/tactics.v
theories/lang/lib/memcpy.v
theories/lang/lib/swap.v
theories/lang/lib/new_delete.v
theories/lang/lib/spawn.v
theories/lang/lib/lock.v
theories/lang/lib/arc.v
theories/lang/lib/tests.v
theories/typing/base.v
theories/typing/type.v
theories/typing/util.v
theories/typing/lft_contexts.v
theories/typing/type_context.v
theories/typing/cont_context.v
theories/typing/uninit.v
theories/typing/own.v
theories/typing/uniq_bor.v
theories/typing/shr_bor.v
theories/typing/product.v
theories/typing/product_split.v
theories/typing/sum.v
theories/typing/bool.v
theories/typing/int.v
theories/typing/function.v
theories/typing/programs.v
theories/typing/borrow.v
theories/typing/cont.v
theories/typing/fixpoint.v
theories/typing/type_sum.v
theories/typing/typing.v
theories/typing/soundness.v
theories/typing/lib/panic.v
theories/typing/lib/option.v
theories/typing/lib/fake_shared.v
theories/typing/lib/cell.v
theories/typing/lib/spawn.v
theories/typing/lib/join.v
theories/typing/lib/diverging_static.v
theories/typing/lib/take_mut.v
theories/typing/lib/rc/rc.v
theories/typing/lib/rc/weak.v
theories/typing/lib/arc.v
theories/typing/lib/swap.v
theories/typing/lib/mutex/mutex.v
theories/typing/lib/mutex/mutexguard.v
theories/typing/lib/refcell/refcell.v
theories/typing/lib/refcell/ref.v
theories/typing/lib/refcell/refmut.v
theories/typing/lib/refcell/refcell_code.v
theories/typing/lib/refcell/ref_code.v
theories/typing/lib/refcell/refmut_code.v
theories/typing/lib/rwlock/rwlock.v
theories/typing/lib/rwlock/rwlockreadguard.v
theories/typing/lib/rwlock/rwlockwriteguard.v
theories/typing/lib/rwlock/rwlock_code.v
theories/typing/lib/rwlock/rwlockreadguard_code.v
theories/typing/lib/rwlock/rwlockwriteguard_code.v
theories/typing/examples/get_x.v
theories/typing/examples/rebor.v
theories/typing/examples/unbox.v
theories/typing/examples/init_prod.v
theories/typing/examples/lazy_lft.v
theories/typing/examples/nonlexical.v
lifetime/model/definitions.v
lifetime/model/faking.v
lifetime/model/creation.v
lifetime/model/primitive.v
lifetime/model/accessors.v
lifetime/model/borrow.v
lifetime/model/borrow_sep.v
lifetime/model/reborrow.v
lifetime/lifetime_sig.v
lifetime/lifetime.v
lifetime/at_borrow.v
lifetime/na_borrow.v
lifetime/frac_borrow.v
lifetime/meta.v
lambda-rust/lang/adequacy.v
lambda-rust/lang/heap.v
lambda-rust/lang/lang.v
lambda-rust/lang/lifting.v
lambda-rust/lang/notation.v
lambda-rust/lang/proofmode.v
lambda-rust/lang/races.v
lambda-rust/lang/tactics.v
lambda-rust/lang/lib/memcpy.v
lambda-rust/lang/lib/swap.v
lambda-rust/lang/lib/new_delete.v
lambda-rust/lang/lib/spawn.v
lambda-rust/lang/lib/lock.v
lambda-rust/lang/lib/arc.v
lambda-rust/lang/lib/tests.v
lambda-rust/typing/base.v
lambda-rust/typing/type.v
lambda-rust/typing/util.v
lambda-rust/typing/lft_contexts.v
lambda-rust/typing/type_context.v
lambda-rust/typing/cont_context.v
lambda-rust/typing/uninit.v
lambda-rust/typing/own.v
lambda-rust/typing/uniq_bor.v
lambda-rust/typing/shr_bor.v
lambda-rust/typing/product.v
lambda-rust/typing/product_split.v
lambda-rust/typing/sum.v
lambda-rust/typing/bool.v
lambda-rust/typing/int.v
lambda-rust/typing/function.v
lambda-rust/typing/programs.v
lambda-rust/typing/borrow.v
lambda-rust/typing/cont.v
lambda-rust/typing/fixpoint.v
lambda-rust/typing/type_sum.v
lambda-rust/typing/typing.v
lambda-rust/typing/soundness.v
lambda-rust/typing/lib/panic.v
lambda-rust/typing/lib/option.v
lambda-rust/typing/lib/fake_shared.v
lambda-rust/typing/lib/cell.v
lambda-rust/typing/lib/spawn.v
lambda-rust/typing/lib/join.v
lambda-rust/typing/lib/take_mut.v
lambda-rust/typing/lib/rc/rc.v
lambda-rust/typing/lib/rc/weak.v
lambda-rust/typing/lib/arc.v
lambda-rust/typing/lib/swap.v
lambda-rust/typing/lib/diverging_static.v
lambda-rust/typing/lib/brandedvec.v
lambda-rust/typing/lib/ghostcell.v
lambda-rust/typing/lib/mutex/mutex.v
lambda-rust/typing/lib/mutex/mutexguard.v
lambda-rust/typing/lib/refcell/refcell.v
lambda-rust/typing/lib/refcell/ref.v
lambda-rust/typing/lib/refcell/refmut.v
lambda-rust/typing/lib/refcell/refcell_code.v
lambda-rust/typing/lib/refcell/ref_code.v
lambda-rust/typing/lib/refcell/refmut_code.v
lambda-rust/typing/lib/rwlock/rwlock.v
lambda-rust/typing/lib/rwlock/rwlockreadguard.v
lambda-rust/typing/lib/rwlock/rwlockwriteguard.v
lambda-rust/typing/lib/rwlock/rwlock_code.v
lambda-rust/typing/lib/rwlock/rwlockreadguard_code.v
lambda-rust/typing/lib/rwlock/rwlockwriteguard_code.v
lambda-rust/typing/examples/fixpoint.v
lambda-rust/typing/examples/get_x.v
lambda-rust/typing/examples/rebor.v
lambda-rust/typing/examples/unbox.v
lambda-rust/typing/examples/init_prod.v
lambda-rust/typing/examples/lazy_lft.v
lambda-rust/typing/examples/nonlexical.v
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.
From iris.algebra Require Import auth.
From lrust.lang Require Export heap.
From lrust.lang Require Import proofmode notation.
Set Default Proof Using "Type".
From iris.prelude Require Import options.
Class lrustPreG Σ := HeapPreG {
lrust_preG_irig :> invPreG Σ;
lrust_preG_heap :> inG Σ (authR heapUR);
lrust_preG_heap_freeable :> inG Σ (authR heap_freeableUR)
Class lrustGpreS Σ := HeapGpreS {
lrustGpreS_irig :: invGpreS Σ;
lrustGpreS_heap :: inG Σ (authR heapUR);
lrustGpreS_heap_freeable :: inG Σ (authR heap_freeableUR)
}.
Definition lrustΣ : gFunctors :=
#[invΣ;
GFunctor (constRF (authR heapUR));
GFunctor (constRF (authR heap_freeableUR))].
Instance subG_heapPreG {Σ} : subG lrustΣ Σ → lrustPreG Σ.
Global Instance subG_lrustGpreS {Σ} : subG lrustΣ Σ → lrustGpreS Σ.
Proof. solve_inG. Qed.
Definition lrust_adequacy Σ `{!lrustPreG Σ} e σ φ :
(∀ `{!lrustG Σ}, True ⊢ WP e {{ v, ⌜φ v⌝ }}) →
Definition lrust_adequacy Σ `{!lrustGpreS Σ} e σ φ :
(∀ `{!lrustGS Σ}, True ⊢ WP e {{ v, ⌜φ v⌝ }}) →
adequate NotStuck e σ (λ v _, φ v).
Proof.
intros Hwp; eapply (wp_adequacy _ _); iIntros (??).
......@@ -26,8 +26,8 @@ Proof.
{ apply (auth_auth_valid (to_heap _)), to_heap_valid. }
iMod (own_alloc (● (∅ : heap_freeableUR))) as (fγ) "Hfγ";
first by apply auth_auth_valid.
set (Hheap := HeapG _ _ _ vγ fγ).
set (Hheap := HeapGS _ _ _ vγ fγ).
iModIntro. iExists (λ σ _, heap_ctx σ), (λ _, True%I). iSplitL.
{ iExists ∅. by iFrame. }
by iApply (Hwp (LRustG _ _ Hheap)).
by iApply (Hwp (LRustGS _ _ Hheap)).
Qed.
theories/lang/heap.v → lambda-rust/lang/heap.v
View file @ 0f4ebd6d
From Coq Require Import Min.
From stdpp Require Import coPset.
From iris.algebra Require Import big_op gmap frac agree.
From iris.algebra Require Import big_op gmap frac agree numbers.
From iris.algebra Require Import csum excl auth cmra_big_op.
From iris.bi Require Import fractional.
From iris.base_logic Require Export lib.own.
From iris.proofmode Require Export tactics.
From iris.proofmode Require Export proofmode.
From lrust.lang Require Export lang.
Set Default Proof Using "Type".
From iris.prelude Require Import options.
Import uPred.
Definition lock_stateR : cmraT :=
Definition lock_stateR : cmra :=
csumR (exclR unitO) natR.
Definition heapUR : ucmraT :=
(* These days this could use gmap_view, but this code predates that. *)
Definition heapUR : ucmra :=
gmapUR loc (prodR (prodR fracR lock_stateR) (agreeR valO)).
Definition heap_freeableUR : ucmraT :=
Definition heap_freeableUR : ucmra :=
gmapUR block (prodR fracR (gmapR Z (exclR unitO))).
Class heapG Σ := HeapG {
heap_inG :> inG Σ (authR heapUR);
heap_freeable_inG :> inG Σ (authR heap_freeableUR);
Class heapGS Σ := HeapGS {
heap_inG :: inG Σ (authR heapUR);
heap_freeable_inG :: inG Σ (authR heap_freeableUR);
heap_name : gname;
heap_freeable_name : gname
}.
......@@ -34,28 +34,28 @@ Definition heap_freeable_rel (σ : state) (hF : heap_freeableUR) : Prop :=
qs.2 ≠ ∅ ∧ ∀ i, is_Some (σ !! (blk, i)) ↔ is_Some (qs.2 !! i).
Section definitions.
Context `{!heapG Σ}.
Context `{!heapGS Σ}.
Definition heap_mapsto_st (st : lock_state)
Definition heap_pointsto_st (st : lock_state)
(l : loc) (q : Qp) (v: val) : iProp Σ :=
own heap_name (◯ {[ l := (q, to_lock_stateR st, to_agree v) ]}).
Definition heap_mapsto_def (l : loc) (q : Qp) (v: val) : iProp Σ :=
heap_mapsto_st (RSt 0) l q v.
Definition heap_mapsto_aux : seal (@heap_mapsto_def). by eexists. Qed.
Definition heap_mapsto := unseal heap_mapsto_aux.
Definition heap_mapsto_eq : @heap_mapsto = @heap_mapsto_def :=
seal_eq heap_mapsto_aux.
Definition heap_pointsto_def (l : loc) (q : Qp) (v: val) : iProp Σ :=
heap_pointsto_st (RSt 0) l q v.
Definition heap_pointsto_aux : seal (@heap_pointsto_def). Proof. by eexists. Qed.
Definition heap_pointsto := unseal heap_pointsto_aux.
Definition heap_pointsto_eq : @heap_pointsto = @heap_pointsto_def :=
seal_eq heap_pointsto_aux.
Definition heap_mapsto_vec (l : loc) (q : Qp) (vl : list val) : iProp Σ :=
([∗ list] i ↦ v ∈ vl, heap_mapsto (l +ₗ i) q v)%I.
Definition heap_pointsto_vec (l : loc) (q : Qp) (vl : list val) : iProp Σ :=
([∗ list] i ↦ v ∈ vl, heap_pointsto (l +ₗ i) q v)%I.
Fixpoint inter (i0 : Z) (n : nat) : gmapR Z (exclR unitO) :=
match n with O => ∅ | S n => <[i0 := Excl ()]>(inter (i0+1) n) end.
Definition heap_freeable_def (l : loc) (q : Qp) (n: nat) : iProp Σ :=
own heap_freeable_name (◯ {[ l.1 := (q, inter (l.2) n) ]}).
Definition heap_freeable_aux : seal (@heap_freeable_def). by eexists. Qed.
Definition heap_freeable_aux : seal (@heap_freeable_def). Proof. by eexists. Qed.
Definition heap_freeable := unseal heap_freeable_aux.
Definition heap_freeable_eq : @heap_freeable = @heap_freeable_def :=
seal_eq heap_freeable_aux.
......@@ -66,17 +66,17 @@ Section definitions.
∗ ⌜heap_freeable_rel σ hF⌝)%I.
End definitions.
Typeclasses Opaque heap_mapsto heap_freeable heap_mapsto_vec.
Instance: Params (@heap_mapsto) 4 := {}.
Instance: Params (@heap_freeable) 5 := {}.
Global Typeclasses Opaque heap_pointsto_vec.
Global Instance: Params (@heap_pointsto) 4 := {}.
Global Instance: Params (@heap_freeable) 5 := {}.
Notation "l ↦{ q } v" := (heap_mapsto l q v)
Notation "l ↦{ q } v" := (heap_pointsto l q v)
(at level 20, q at level 50, format "l ↦{ q } v") : bi_scope.
Notation "l ↦ v" := (heap_mapsto l 1 v) (at level 20) : bi_scope.
Notation "l ↦ v" := (heap_pointsto l 1 v) (at level 20) : bi_scope.
Notation "l ↦∗{ q } vl" := (heap_mapsto_vec l q vl)
Notation "l ↦∗{ q } vl" := (heap_pointsto_vec l q vl)
(at level 20, q at level 50, format "l ↦∗{ q } vl") : bi_scope.
Notation "l ↦∗ vl" := (heap_mapsto_vec l 1 vl) (at level 20) : bi_scope.
Notation "l ↦∗ vl" := (heap_pointsto_vec l 1 vl) (at level 20) : bi_scope.
Notation "l ↦∗{ q }: P" := (∃ vl, l ↦∗{ q } vl ∗ P vl)%I
(at level 20, q at level 50, format "l ↦∗{ q }: P") : bi_scope.
......@@ -91,7 +91,7 @@ Section to_heap.
Implicit Types σ : state.
Lemma to_heap_valid σ : ✓ to_heap σ.
Proof. intros l. rewrite lookup_fmap. case (σ !! l)=> [[[|n] v]|] //=. Qed.
Proof. intros l. rewrite lookup_fmap. destruct (σ !! l) as [[[|n] v]|] eqn:EQ; rewrite EQ //. Qed.
Lemma lookup_to_heap_None σ l : σ !! l = None → to_heap σ !! l = None.
Proof. by rewrite /to_heap lookup_fmap=> ->. Qed.
......@@ -106,81 +106,86 @@ Section to_heap.
End to_heap.
Section heap.
Context `{!heapG Σ}.
Context `{!heapGS Σ}.
Implicit Types P Q : iProp Σ.
Implicit Types σ : state.
Implicit Types E : coPset.
(** General properties of mapsto and freeable *)
Global Instance heap_mapsto_timeless l q v : Timeless (l↦{q}v).
Proof. rewrite heap_mapsto_eq /heap_mapsto_def. apply _. Qed.
(** General properties of pointsto and freeable *)
Global Instance heap_pointsto_timeless l q v : Timeless (l↦{q}v).
Proof. rewrite heap_pointsto_eq /heap_pointsto_def. apply _. Qed.
Global Instance heap_mapsto_fractional l v: Fractional (λ q, l ↦{q} v)%I.
Global Instance heap_pointsto_fractional l v: Fractional (λ q, l ↦{q} v)%I.
Proof.
intros p q.
by rewrite heap_mapsto_eq -own_op -auth_frag_op op_singleton pair_op agree_idemp.
by rewrite heap_pointsto_eq -own_op -auth_frag_op singleton_op -pair_op agree_idemp.
Qed.
Global Instance heap_mapsto_as_fractional l q v:
Global Instance heap_pointsto_as_fractional l q v:
AsFractional (l ↦{q} v) (λ q, l ↦{q} v)%I q.
Proof. split. done. apply _. Qed.
Proof. split; first done. apply _. Qed.
Global Instance heap_mapsto_vec_timeless l q vl : Timeless (l ↦∗{q} vl).
Proof. rewrite /heap_mapsto_vec. apply _. Qed.
Global Instance frame_pointsto p l v q1 q2 q :
FrameFractionalQp q1 q2 q →
Frame p (l ↦{q1} v) (l ↦{q2} v) (l ↦{q} v) | 5.
Proof. apply: frame_fractional. Qed.
Global Instance heap_mapsto_vec_fractional l vl: Fractional (λ q, l ↦∗{q} vl)%I.
Global Instance heap_pointsto_vec_timeless l q vl : Timeless (l ↦∗{q} vl).
Proof. rewrite /heap_pointsto_vec. apply _. Qed.
Global Instance heap_pointsto_vec_fractional l vl: Fractional (λ q, l ↦∗{q} vl)%I.
Proof.
intros p q. rewrite /heap_mapsto_vec -big_sepL_sep.
intros p q. rewrite /heap_pointsto_vec -big_sepL_sep.
by setoid_rewrite (fractional (Φ := λ q, _ ↦{q} _)%I).
Qed.
Global Instance heap_mapsto_vec_as_fractional l q vl:
Global Instance heap_pointsto_vec_as_fractional l q vl:
AsFractional (l ↦∗{q} vl) (λ q, l ↦∗{q} vl)%I q.
Proof. split. done. apply _. Qed.
Proof. split; first done. apply _. Qed.
Global Instance heap_freeable_timeless q l n : Timeless (†{q}l…n).
Proof. rewrite heap_freeable_eq /heap_freeable_def. apply _. Qed.
Lemma heap_mapsto_agree l q1 q2 v1 v2 : l ↦{q1} v1 ∗ l ↦{q2} v2 ⊢ ⌜v1 = v2⌝.
Lemma heap_pointsto_agree l q1 q2 v1 v2 : l ↦{q1} v1 ∗ l ↦{q2} v2 ⊢ ⌜v1 = v2⌝.
Proof.
rewrite heap_mapsto_eq -own_op -auth_frag_op own_valid discrete_valid.
rewrite heap_pointsto_eq -own_op -auth_frag_op own_valid discrete_valid.
eapply pure_elim; [done|]=> /auth_frag_valid /=.
rewrite op_singleton pair_op singleton_valid=> -[? /agree_op_invL'->]; eauto.
rewrite singleton_op -pair_op singleton_valid=> -[? /to_agree_op_inv_L->]; eauto.
Qed.
Lemma heap_mapsto_vec_nil l q : l ↦∗{q} [] ⊣⊢ True.
Proof. by rewrite /heap_mapsto_vec. Qed.
Lemma heap_pointsto_vec_nil l q : l ↦∗{q} [] ⊣⊢ True.
Proof. by rewrite /heap_pointsto_vec. Qed.
Lemma heap_mapsto_vec_app l q vl1 vl2 :
Lemma heap_pointsto_vec_app l q vl1 vl2 :
l ↦∗{q} (vl1 ++ vl2) ⊣⊢ l ↦∗{q} vl1 ∗ (l +ₗ length vl1) ↦∗{q} vl2.
Proof.
rewrite /heap_mapsto_vec big_sepL_app.
rewrite /heap_pointsto_vec big_sepL_app.
do 2 f_equiv. intros k v. by rewrite shift_loc_assoc_nat.
Qed.
Lemma heap_mapsto_vec_singleton l q v : l ↦∗{q} [v] ⊣⊢ l ↦{q} v.
Proof. by rewrite /heap_mapsto_vec /= shift_loc_0 right_id. Qed.
Lemma heap_pointsto_vec_singleton l q v : l ↦∗{q} [v] ⊣⊢ l ↦{q} v.
Proof. by rewrite /heap_pointsto_vec /= shift_loc_0 right_id. Qed.
Lemma heap_mapsto_vec_cons l q v vl:
Lemma heap_pointsto_vec_cons l q v vl:
l ↦∗{q} (v :: vl) ⊣⊢ l ↦{q} v ∗ (l +ₗ 1) ↦∗{q} vl.
Proof.
by rewrite (heap_mapsto_vec_app l q [v] vl) heap_mapsto_vec_singleton.
by rewrite (heap_pointsto_vec_app l q [v] vl) heap_pointsto_vec_singleton.
Qed.
Lemma heap_mapsto_vec_op l q1 q2 vl1 vl2 :
Lemma heap_pointsto_vec_op l q1 q2 vl1 vl2 :
length vl1 = length vl2 →
l ↦∗{q1} vl1 ∗ l ↦∗{q2} vl2 ⊣⊢ ⌜vl1 = vl2⌝ ∧ l ↦∗{q1+q2} vl1.
Proof.
intros Hlen%Forall2_same_length. apply (anti_symm (⊢)).
- revert l. induction Hlen as [|v1 v2 vl1 vl2 _ _ IH]=> l.
{ rewrite !heap_mapsto_vec_nil. iIntros "_"; auto. }
rewrite !heap_mapsto_vec_cons. iIntros "[[Hv1 Hvl1] [Hv2 Hvl2]]".
{ rewrite !heap_pointsto_vec_nil. iIntros "_"; auto. }
rewrite !heap_pointsto_vec_cons. iIntros "[[Hv1 Hvl1] [Hv2 Hvl2]]".
iDestruct (IH (l +ₗ 1) with "[$Hvl1 $Hvl2]") as "[% $]"; subst.
rewrite (inj_iff (:: vl2)).
iDestruct (heap_mapsto_agree with "[$Hv1 $Hv2]") as %<-.
rewrite (inj_iff (.:: vl2)).
iDestruct (heap_pointsto_agree with "[$Hv1 $Hv2]") as %<-.
iSplit; first done. iFrame.
- by iIntros "[% [$ Hl2]]"; subst.
Qed.
Lemma heap_mapsto_pred_op l q1 q2 n (Φ : list val → iProp Σ) :
Lemma heap_pointsto_pred_op l q1 q2 n (Φ : list val → iProp Σ) :
(∀ vl, Φ vl -∗ ⌜length vl = n⌝) →
l ↦∗{q1}: Φ ∗ l ↦∗{q2}: (λ vl, ⌜length vl = n⌝) ⊣⊢ l ↦∗{q1+q2}: Φ.
Proof.
......@@ -188,37 +193,37 @@ Section heap.
- iIntros "[Hmt1 Hmt2]".
iDestruct "Hmt1" as (vl) "[Hmt1 Hown]". iDestruct "Hmt2" as (vl') "[Hmt2 %]".
iDestruct (Hlen with "Hown") as %?.
iCombine "Hmt1" "Hmt2" as "Hmt". rewrite heap_mapsto_vec_op; last congruence.
iCombine "Hmt1" "Hmt2" as "Hmt". rewrite heap_pointsto_vec_op; last congruence.
iDestruct "Hmt" as "[_ Hmt]". iExists vl. by iFrame.
- iIntros "Hmt". iDestruct "Hmt" as (vl) "[[Hmt1 Hmt2] Hown]".
iDestruct (Hlen with "Hown") as %?.
iSplitL "Hmt1 Hown"; iExists _; by iFrame.
Qed.
Lemma heap_mapsto_pred_wand l q Φ1 Φ2 :
Lemma heap_pointsto_pred_wand l q Φ1 Φ2 :
l ↦∗{q}: Φ1 -∗ (∀ vl, Φ1 vl -∗ Φ2 vl) -∗ l ↦∗{q}: Φ2.
Proof.
iIntros "Hm Hwand". iDestruct "Hm" as (vl) "[Hm HΦ]". iExists vl.
iFrame "Hm". by iApply "Hwand".
Qed.
Lemma heap_mapsto_pred_iff_proper l q Φ1 Φ2 :
Lemma heap_pointsto_pred_iff_proper l q Φ1 Φ2 :
□ (∀ vl, Φ1 vl ↔ Φ2 vl) -∗ □ (l ↦∗{q}: Φ1 ↔ l ↦∗{q}: Φ2).
Proof.
iIntros "#HΦ !#". iSplit; iIntros; iApply (heap_mapsto_pred_wand with "[-]"); try done; [|];
iIntros "#HΦ !>". iSplit; iIntros; iApply (heap_pointsto_pred_wand with "[-]"); try done; [|];
iIntros; by iApply "HΦ".
Qed.
Lemma heap_mapsto_vec_combine l q vl :
Lemma heap_pointsto_vec_combine l q vl :
vl ≠ [] →
l ↦∗{q} vl ⊣⊢ own heap_name (◯ [^op list] i ↦ v ∈ vl,
{[l +ₗ i := (q, Cinr 0%nat, to_agree v)]}).
Proof.
rewrite /heap_mapsto_vec heap_mapsto_eq /heap_mapsto_def /heap_mapsto_st=>?.
rewrite /heap_pointsto_vec heap_pointsto_eq /heap_pointsto_def /heap_pointsto_st=>?.
rewrite (big_opL_commute auth_frag) big_opL_commute1 //.
Qed.
Global Instance heap_mapsto_pred_fractional l (P : list val → iProp Σ):
Global Instance heap_pointsto_pred_fractional l (P : list val → iProp Σ):
(∀ vl, Persistent (P vl)) → Fractional (λ q, l ↦∗{q}: P)%I.
Proof.
intros p q q'. iSplit.
......@@ -227,13 +232,13 @@ Section heap.
- iIntros "[H1 H2]". iDestruct "H1" as (vl1) "[Hown1 #HP1]".
iDestruct "H2" as (vl2) "[Hown2 #HP2]".
set (ll := min (length vl1) (length vl2)).
rewrite -[vl1](firstn_skipn ll) -[vl2](firstn_skipn ll) 2!heap_mapsto_vec_app.
rewrite -[vl1](firstn_skipn ll) -[vl2](firstn_skipn ll) 2!heap_pointsto_vec_app.
iDestruct "Hown1" as "[Hown1 _]". iDestruct "Hown2" as "[Hown2 _]".
iCombine "Hown1" "Hown2" as "Hown". rewrite heap_mapsto_vec_op; last first.
{ rewrite !firstn_length. subst ll.
rewrite -!min_assoc min_idempotent min_comm -min_assoc min_idempotent min_comm. done. }
iCombine "Hown1" "Hown2" as "Hown". rewrite heap_pointsto_vec_op; last first.
{ rewrite !length_firstn. subst ll.
rewrite -!Nat.min_assoc Nat.min_idempotent Nat.min_comm -Nat.min_assoc Nat.min_idempotent Nat.min_comm. done. }
iDestruct "Hown" as "[H Hown]". iDestruct "H" as %Hl. iExists (take ll vl1). iFrame.
destruct (min_spec (length vl1) (length vl2)) as [[Hne Heq]|[Hne Heq]].
destruct (Nat.min_spec (length vl1) (length vl2)) as [[Hne Heq]|[Hne Heq]].
+ iClear "HP2". rewrite take_ge; last first.
{ rewrite -Heq /ll. done. }
rewrite drop_ge; first by rewrite app_nil_r. by rewrite -Heq.
......@@ -241,9 +246,9 @@ Section heap.
{ rewrite -Heq /ll. done. }
rewrite drop_ge; first by rewrite app_nil_r. by rewrite -Heq.
Qed.
Global Instance heap_mapsto_pred_as_fractional l q (P : list val → iProp Σ):
Global Instance heap_pointsto_pred_as_fractional l q (P : list val → iProp Σ):
(∀ vl, Persistent (P vl)) → AsFractional (l ↦∗{q}: P) (λ q, l ↦∗{q}: P)%I q.
Proof. split. done. apply _. Qed.
Proof. split; first done. apply _. Qed.
Lemma inter_lookup_Some i j (n : nat):
i ≤ j < i+n → inter i n !! j = Excl' ().
......@@ -266,13 +271,13 @@ Section heap.
- by rewrite !inter_lookup_None; try lia.
Qed.
Lemma inter_valid i n : ✓ inter i n.
Proof. revert i. induction n as [|n IH]=>i. done. by apply insert_valid. Qed.
Proof. revert i. induction n as [|n IH]=>i; first done. by apply insert_valid. Qed.
Lemma heap_freeable_op_eq l q1 q2 n n' :
†{q1}l…n ∗ †{q2}l+ₗn … n' ⊣⊢ †{q1+q2}l…(n+n').
†{q1}l…n ∗ †{q2}l +ₗ n … n' ⊣⊢ †{q1+q2}l…(n+n').
Proof.
by rewrite heap_freeable_eq /heap_freeable_def -own_op -auth_frag_op
op_singleton pair_op inter_op.
singleton_op -pair_op inter_op.
Qed.
(** Properties about heap_freeable_rel and heap_freeable *)
......@@ -343,13 +348,13 @@ Section heap.
∗ own heap_name (◯ [^op list] i ↦ v ∈ (repeat (LitV LitPoison) n),
{[l +ₗ i := (1%Qp, Cinr 0%nat, to_agree v)]}).
Proof.
intros FREE. rewrite -own_op. apply own_update, auth_update_alloc.
intros FREE. rewrite -own_op. apply entails_wand, own_update, auth_update_alloc.
revert l FREE. induction n as [|n IH]=> l FRESH; [done|].
rewrite (big_opL_consZ_l (λ k _, _ (_ k) _ )) /=.
etrans; first apply (IH (l +ₗ 1)).
{ intros. by rewrite shift_loc_assoc. }
rewrite shift_loc_0 -insert_singleton_op; last first.
{ rewrite -equiv_None big_opL_commute equiv_None big_opL_None=> l' v' ?.
{ rewrite -None_equiv_eq big_opL_commute None_equiv_eq big_opL_None=> l' v' ?.
rewrite lookup_singleton_None -{2}(shift_loc_0 l). apply not_inj; lia. }
rewrite to_heap_insert. setoid_rewrite shift_loc_assoc.
apply alloc_local_update; last done. apply lookup_to_heap_None.
......@@ -365,17 +370,18 @@ Section heap.
Proof.
intros ??; iDestruct 1 as (hF) "(Hvalσ & HhF & %)".
assert (Z.to_nat n ≠ O). { rewrite -(Nat2Z.id 0)=>/Z2Nat.inj. lia. }
iMod (heap_alloc_vs _ _ (Z.to_nat n) with "[$Hvalσ]") as "[Hvalσ Hmapsto]"; first done.
iMod (heap_alloc_vs _ _ (Z.to_nat n) with "[$Hvalσ]") as "[Hvalσ ?]"; first done.
iMod (own_update _ (● hF) with "HhF") as "[HhF Hfreeable]".
{ apply auth_update_alloc,
(alloc_singleton_local_update _ (l.1) (1%Qp, inter (l.2) (Z.to_nat n))).
- eauto using heap_freeable_rel_None.
- split. done. apply inter_valid. }
- split; first done. apply inter_valid. }
iModIntro. iSplitL "Hvalσ HhF".
{ iExists _. iFrame. iPureIntro.
auto using heap_freeable_rel_init_mem. }
rewrite heap_freeable_eq /heap_freeable_def heap_mapsto_vec_combine //.
iFrame. destruct (Z.to_nat n); done.
rewrite heap_freeable_eq /heap_freeable_def heap_pointsto_vec_combine //; last first.
{ destruct (Z.to_nat n); done. }
iFrame.
Qed.
Lemma heap_free_vs σ l vl :
......@@ -383,14 +389,14 @@ Section heap.
{[l +ₗ i := (1%Qp, Cinr 0%nat, to_agree v)]})
==∗ own heap_name (● to_heap (free_mem l (length vl) σ)).
Proof.
rewrite -own_op. apply own_update, auth_update_dealloc.
rewrite -own_op. apply entails_wand, own_update, auth_update_dealloc.
revert σ l. induction vl as [|v vl IH]=> σ l; [done|].
rewrite (big_opL_consZ_l (λ k _, _ (_ k) _ )) /= shift_loc_0.
apply local_update_total_valid=> _ Hvalid _.
assert (([^op list] k↦y ∈ vl,
{[l +ₗ (1 + k) := (1%Qp, Cinr 0%nat, to_agree y)]} : heapUR) !! l = None).
{ move: (Hvalid l). rewrite lookup_op lookup_singleton.
by move=> /(cmra_discrete_valid_iff 0) /exclusiveN_Some_l. }
by move=> /(cmra_discrete_valid_iff 0ᵢ) /exclusiveN_Some_l. }
rewrite -insert_singleton_op //. etrans.
{ apply (delete_local_update _ _ l (1%Qp, Cinr 0%nat, to_agree v)).
by rewrite lookup_insert. }
......@@ -406,15 +412,15 @@ Section heap.
Proof.
iDestruct 1 as (hF) "(Hvalσ & HhF & REL)"; iDestruct "REL" as %REL.
iIntros "Hmt Hf". rewrite heap_freeable_eq /heap_freeable_def.
iDestruct (own_valid_2 with "HhF Hf") as % [Hl Hv]%auth_both_valid.
move: Hl=> /singleton_included [[q qs] [/leibniz_equiv_iff Hl Hq]].
iCombine "HhF Hf" gives % [Hl Hv]%auth_both_valid_discrete.
move: Hl=> /singleton_included_l [[q qs] [/leibniz_equiv_iff Hl Hq]].
apply (Some_included_exclusive _ _) in Hq as [=<-<-]%leibniz_equiv; last first.
{ move: (Hv (l.1)). rewrite Hl. by intros [??]. }
assert (vl ≠ []).
{ intros ->. by destruct (REL (l.1) (1%Qp, ∅)) as [[] ?]. }
assert (0 < n) by (subst n; by destruct vl).
iMod (heap_free_vs with "[Hmt Hvalσ]") as "Hvalσ".
{ rewrite heap_mapsto_vec_combine //. iFrame. }
{ rewrite heap_pointsto_vec_combine //. iFrame. }
iMod (own_update_2 with "HhF Hf") as "HhF".
{ apply auth_update_dealloc, (delete_singleton_local_update _ _ _). }
iModIntro; subst. repeat iSplit; eauto using heap_freeable_is_Some.
......@@ -422,32 +428,34 @@ Section heap.
eauto using heap_freeable_rel_free_mem.
Qed.
Lemma heap_mapsto_lookup σ l ls q v :
Lemma heap_pointsto_lookup σ l ls q v :
own heap_name (● to_heap σ) -∗
own heap_name (◯ {[ l := (q, to_lock_stateR ls, to_agree v) ]}) -∗
⌜∃ n' : nat,
σ !! l = Some (match ls with RSt n => RSt (n+n') | WSt => WSt end, v)⌝.
Proof.
iIntros "H● H◯".
iDestruct (own_valid_2 with "H● H◯") as %[Hl?]%auth_both_valid.
iPureIntro. move: Hl=> /singleton_included [[[q' ls'] dv]].
iCombine "H● H◯" gives %[Hl?]%auth_both_valid_discrete.
iPureIntro. move: Hl=> /singleton_included_l [[[q' ls'] dv]].
rewrite /to_heap lookup_fmap fmap_Some_equiv.
move=> [[[ls'' v'] [?[[/=??]->]]]]; simplify_eq.
move=> /Some_pair_included_total_2
[/Some_pair_included [_ Hincl] /to_agree_included->].
destruct ls as [|n], ls'' as [|n''],
Hincl as [[[|n'|]|] [=]%leibniz_equiv]; subst.
by exists O. eauto. exists O. by rewrite Nat.add_0_r.
- by exists O.
- eauto.
- exists O. by rewrite Nat.add_0_r.
Qed.
Lemma heap_mapsto_lookup_1 σ l ls v :
Lemma heap_pointsto_lookup_1 σ l ls v :
own heap_name (● to_heap σ) -∗
own heap_name (◯ {[ l := (1%Qp, to_lock_stateR ls, to_agree v) ]}) -∗
⌜σ !! l = Some (ls, v)⌝.
Proof.
iIntros "H● H◯".
iDestruct (own_valid_2 with "H● H◯") as %[Hl?]%auth_both_valid.
iPureIntro. move: Hl=> /singleton_included [[[q' ls'] dv]].
iCombine "H● H◯" gives %[Hl?]%auth_both_valid_discrete.
iPureIntro. move: Hl=> /singleton_included_l [[[q' ls'] dv]].
rewrite /to_heap lookup_fmap fmap_Some_equiv.
move=> [[[ls'' v'] [?[[/=??]->]]] Hincl]; simplify_eq.
apply (Some_included_exclusive _ _) in Hincl as [? Hval]; last by destruct ls''.
......@@ -457,12 +465,12 @@ Section heap.
Lemma heap_read_vs σ n1 n2 nf l q v:
σ !! l = Some (RSt (n1 + nf), v) →
own heap_name (● to_heap σ) -∗ heap_mapsto_st (RSt n1) l q v
own heap_name (● to_heap σ) -∗ heap_pointsto_st (RSt n1) l q v
==∗ own heap_name (● to_heap (<[l:=(RSt (n2 + nf), v)]> σ))
∗ heap_mapsto_st (RSt n2) l q v.
∗ heap_pointsto_st (RSt n2) l q v.
Proof.
intros Hσv. apply wand_intro_r. rewrite -!own_op to_heap_insert.
eapply own_update, auth_update, singleton_local_update.
intros Hσv. apply entails_wand, wand_intro_r. rewrite -!own_op to_heap_insert.
iApply own_update. eapply auth_update, singleton_local_update.
{ by rewrite /to_heap lookup_fmap Hσv. }
apply prod_local_update_1, prod_local_update_2, csum_local_update_r.
apply nat_local_update; lia.
......@@ -472,16 +480,16 @@ Section heap.
heap_ctx σ -∗ l ↦{q} v -∗ ∃ n, ⌜σ !! l = Some (RSt n, v)⌝.
Proof.
iDestruct 1 as (hF) "(Hσ & HhF & REL)". iIntros "Hmt".
rewrite heap_mapsto_eq.
iDestruct (heap_mapsto_lookup with "Hσ Hmt") as %[n Hσl]; eauto.
rewrite heap_pointsto_eq.
iDestruct (heap_pointsto_lookup with "Hσ Hmt") as %[n Hσl]; eauto.
Qed.
Lemma heap_read_1 σ l v :
heap_ctx σ -∗ l ↦ v -∗ ⌜σ !! l = Some (RSt 0, v)⌝.
Proof.
iDestruct 1 as (hF) "(Hσ & HhF & REL)". iIntros "Hmt".
rewrite heap_mapsto_eq.
iDestruct (heap_mapsto_lookup_1 with "Hσ Hmt") as %?; auto.
rewrite heap_pointsto_eq.
iDestruct (heap_pointsto_lookup_1 with "Hσ Hmt") as %?; auto.
Qed.
Lemma heap_read_na σ l q v :
......@@ -492,13 +500,13 @@ Section heap.
heap_ctx (<[l:=(RSt n2, v)]> σ2) ∗ l ↦{q} v.
Proof.
iDestruct 1 as (hF) "(Hσ & HhF & %)"; iIntros "Hmt".
rewrite heap_mapsto_eq.
iDestruct (heap_mapsto_lookup with "Hσ Hmt") as %[n Hσl]; eauto.
rewrite heap_pointsto_eq.
iDestruct (heap_pointsto_lookup with "Hσ Hmt") as %[n Hσl]; eauto.
iMod (heap_read_vs _ 0 1 with "Hσ Hmt") as "[Hσ Hmt]"; first done.
iModIntro. iExists n; iSplit; [done|]. iSplitL "HhF Hσ".
{ iExists hF. iFrame. eauto using heap_freeable_rel_stable. }
clear dependent n σ hF. iIntros (σ2). iDestruct 1 as (hF) "(Hσ & HhF & %)".
iDestruct (heap_mapsto_lookup with "Hσ Hmt") as %[n Hσl]; eauto.
iDestruct (heap_pointsto_lookup with "Hσ Hmt") as %[n Hσl]; eauto.
iMod (heap_read_vs _ 1 0 with "Hσ Hmt") as "[Hσ Hmt]"; first done.
iExists n; iModIntro; iSplit; [done|]. iFrame "Hmt".
iExists hF. iFrame. eauto using heap_freeable_rel_stable.
......@@ -506,12 +514,12 @@ Section heap.
Lemma heap_write_vs σ st1 st2 l v v':
σ !! l = Some (st1, v) →
own heap_name (● to_heap σ) -∗ heap_mapsto_st st1 l 1%Qp v
own heap_name (● to_heap σ) -∗ heap_pointsto_st st1 l 1%Qp v
==∗ own heap_name (● to_heap (<[l:=(st2, v')]> σ))
∗ heap_mapsto_st st2 l 1%Qp v'.
∗ heap_pointsto_st st2 l 1%Qp v'.
Proof.
intros Hσv. apply wand_intro_r. rewrite -!own_op to_heap_insert.
eapply own_update, auth_update, singleton_local_update.
intros Hσv. apply entails_wand, wand_intro_r. rewrite -!own_op to_heap_insert.
iApply own_update. eapply auth_update, singleton_local_update.
{ by rewrite /to_heap lookup_fmap Hσv. }
apply exclusive_local_update. by destruct st2.
Qed.
......@@ -520,8 +528,8 @@ Section heap.
heap_ctx σ -∗ l ↦ v ==∗ heap_ctx (<[l:=(RSt 0, v')]> σ) ∗ l ↦ v'.
Proof.
iDestruct 1 as (hF) "(Hσ & HhF & %)". iIntros "Hmt".
rewrite heap_mapsto_eq.
iDestruct (heap_mapsto_lookup_1 with "Hσ Hmt") as %?; auto.
rewrite heap_pointsto_eq.
iDestruct (heap_pointsto_lookup_1 with "Hσ Hmt") as %?; auto.
iMod (heap_write_vs with "Hσ Hmt") as "[Hσ $]"; first done.
iModIntro. iExists _. iFrame. eauto using heap_freeable_rel_stable.
Qed.
......@@ -534,13 +542,13 @@ Section heap.
heap_ctx (<[l:=(RSt 0, v')]> σ2) ∗ l ↦ v'.
Proof.
iDestruct 1 as (hF) "(Hσ & HhF & %)"; iIntros "Hmt".
rewrite heap_mapsto_eq.
iDestruct (heap_mapsto_lookup_1 with "Hσ Hmt") as %?; eauto.
rewrite heap_pointsto_eq.
iDestruct (heap_pointsto_lookup_1 with "Hσ Hmt") as %?; eauto.
iMod (heap_write_vs with "Hσ Hmt") as "[Hσ Hmt]"; first done.
iModIntro. iSplit; [done|]. iSplitL "HhF Hσ".
{ iExists hF. iFrame. eauto using heap_freeable_rel_stable. }
clear dependent σ hF. iIntros (σ2). iDestruct 1 as (hF) "(Hσ & HhF & %)".
iDestruct (heap_mapsto_lookup with "Hσ Hmt") as %[n Hσl]; eauto.
iDestruct (heap_pointsto_lookup with "Hσ Hmt") as %[n Hσl]; eauto.
iMod (heap_write_vs with "Hσ Hmt") as "[Hσ Hmt]"; first done.
iModIntro; iSplit; [done|]. iFrame "Hmt".
iExists hF. iFrame. eauto using heap_freeable_rel_stable.
......
theories/lang/lang.v → lambda-rust/lang/lang.v
View file @ 0f4ebd6d
From iris.program_logic Require Export language ectx_language ectxi_language.
From stdpp Require Export strings binders.
From stdpp Require Import gmap.
Set Default Proof Using "Type".
From iris.prelude Require Import options.
Open Scope Z_scope.
Global Open Scope Z_scope.
(** Expressions and vals. *)
Definition block : Set := positive.
Definition loc : Set := block * Z.
Declare Scope loc_scope.
Bind Scope loc_scope with loc.
Delimit Scope loc_scope with L.
Open Scope loc_scope.
Global Open Scope loc_scope.
Inductive base_lit : Set :=
| LitPoison | LitLoc (l : loc) | LitInt (n : Z).
......@@ -42,8 +43,8 @@ Inductive expr :=
| Case (e : expr) (el : list expr)
| Fork (e : expr).
Arguments App _%E _%E.
Arguments Case _%E _%E.
Global Arguments App _%_E _%_E.
Global Arguments Case _%_E _%_E.
Fixpoint is_closed (X : list string) (e : expr) : bool :=
match e with
......@@ -58,9 +59,9 @@ Fixpoint is_closed (X : list string) (e : expr) : bool :=
end.
Class Closed (X : list string) (e : expr) := closed : is_closed X e.
Instance closed_proof_irrel env e : ProofIrrel (Closed env e).
Global Instance closed_proof_irrel env e : ProofIrrel (Closed env e).
Proof. rewrite /Closed. apply _. Qed.
Instance closed_decision env e : Decision (Closed env e).
Global Instance closed_decision env e : Decision (Closed env e).
Proof. rewrite /Closed. apply _. Qed.
Inductive val :=
......@@ -150,27 +151,25 @@ Fixpoint subst_l (xl : list binder) (esl : list expr) (e : expr) : option expr :
| x::xl, es::esl => subst' x es <$> subst_l xl esl e
| _, _ => None
end.
Arguments subst_l _%binder _ _%E.
Global Arguments subst_l _%_binder _ _%_E.
Definition subst_v (xl : list binder) (vsl : vec val (length xl))
(e : expr) : expr :=
Vector.fold_right2 (λ b, subst' b ∘ of_val) e _ (list_to_vec xl) vsl.
Arguments subst_v _%binder _ _%E.
Global Arguments subst_v _%_binder _ _%_E.
Lemma subst_v_eq (xl : list binder) (vsl : vec val (length xl)) e :
Some $ subst_v xl vsl e = subst_l xl (of_val <$> vec_to_list vsl) e.
Proof.
revert vsl. induction xl=>/= vsl; inv_vec vsl=>//=v vsl. by rewrite -IHxl.
revert vsl. induction xl as [|x xl IHxl]=>/= vsl; inv_vec vsl=>//=v vsl.
by rewrite -IHxl.
Qed.
(** The stepping relation *)
(* Be careful to make sure that poison is always stuck when used for anything
except for reading from or writing to memory! *)
Definition Z_of_bool (b : bool) : Z :=
if b then 1 else 0.
Definition lit_of_bool (b : bool) : base_lit :=
LitInt $ Z_of_bool b.
LitInt $ Z.b2z b.
Definition shift_loc (l : loc) (z : Z) : loc := (l.1, l.2 + z).
......@@ -233,48 +232,48 @@ Inductive bin_op_eval (σ : state) : bin_op → base_lit → base_lit → base_l
Definition stuck_term := App (Lit $ LitInt 0) [].
Inductive head_step : expr → state → list Empty_set → expr → state → list expr → Prop :=
Inductive base_step : expr → state → list Empty_set → expr → state → list expr → Prop :=
| BinOpS op l1 l2 l' σ :
bin_op_eval σ op l1 l2 l' →
head_step (BinOp op (Lit l1) (Lit l2)) σ [] (Lit l') σ []
base_step (BinOp op (Lit l1) (Lit l2)) σ [] (Lit l') σ []
| BetaS f xl e e' el σ:
Forall (λ ei, is_Some (to_val ei)) el →
Closed (f :b: xl +b+ []) e →
subst_l (f::xl) (Rec f xl e :: el) e = Some e' →
head_step (App (Rec f xl e) el) σ [] e' σ []
base_step (App (Rec f xl e) el) σ [] e' σ []
| ReadScS l n v σ:
σ !! l = Some (RSt n, v) →
head_step (Read ScOrd (Lit $ LitLoc l)) σ [] (of_val v) σ []
base_step (Read ScOrd (Lit $ LitLoc l)) σ [] (of_val v) σ []
| ReadNa1S l n v σ:
σ !! l = Some (RSt n, v) →
head_step (Read Na1Ord (Lit $ LitLoc l)) σ
base_step (Read Na1Ord (Lit $ LitLoc l)) σ
[]
(Read Na2Ord (Lit $ LitLoc l)) (<[l:=(RSt $ S n, v)]>σ)
[]
| ReadNa2S l n v σ:
σ !! l = Some (RSt $ S n, v) →
head_step (Read Na2Ord (Lit $ LitLoc l)) σ
base_step (Read Na2Ord (Lit $ LitLoc l)) σ
[]
(of_val v) (<[l:=(RSt n, v)]>σ)
[]
| WriteScS l e v v' σ:
to_val e = Some v →
σ !! l = Some (RSt 0, v') →
head_step (Write ScOrd (Lit $ LitLoc l) e) σ
base_step (Write ScOrd (Lit $ LitLoc l) e) σ
[]
(Lit LitPoison) (<[l:=(RSt 0, v)]>σ)
[]
| WriteNa1S l e v v' σ:
to_val e = Some v →
σ !! l = Some (RSt 0, v') →
head_step (Write Na1Ord (Lit $ LitLoc l) e) σ
base_step (Write Na1Ord (Lit $ LitLoc l) e) σ
[]
(Write Na2Ord (Lit $ LitLoc l) e) (<[l:=(WSt, v')]>σ)
[]
| WriteNa2S l e v v' σ:
to_val e = Some v →
σ !! l = Some (WSt, v') →
head_step (Write Na2Ord (Lit $ LitLoc l) e) σ
base_step (Write Na2Ord (Lit $ LitLoc l) e) σ
[]
(Lit LitPoison) (<[l:=(RSt 0, v)]>σ)
[]
......@@ -282,12 +281,12 @@ Inductive head_step : expr → state → list Empty_set → expr → state → l
to_val e1 = Some $ LitV lit1 → to_val e2 = Some $ LitV lit2 →
σ !! l = Some (RSt n, LitV litl) →
lit_neq lit1 litl →
head_step (CAS (Lit $ LitLoc l) e1 e2) σ [] (Lit $ lit_of_bool false) σ []
base_step (CAS (Lit $ LitLoc l) e1 e2) σ [] (Lit $ lit_of_bool false) σ []
| CasSucS l e1 lit1 e2 lit2 litl σ :
to_val e1 = Some $ LitV lit1 → to_val e2 = Some $ LitV lit2 →
σ !! l = Some (RSt 0, LitV litl) →
lit_eq σ lit1 litl →
head_step (CAS (Lit $ LitLoc l) e1 e2) σ
base_step (CAS (Lit $ LitLoc l) e1 e2) σ
[]
(Lit $ lit_of_bool true) (<[l:=(RSt 0, LitV lit2)]>σ)
[]
......@@ -309,30 +308,30 @@ Inductive head_step : expr → state → list Empty_set → expr → state → l
to_val e1 = Some $ LitV lit1 → to_val e2 = Some $ LitV lit2 →
σ !! l = Some (RSt n, LitV litl) → 0 < n →
lit_eq σ lit1 litl →
head_step (CAS (Lit $ LitLoc l) e1 e2) σ
base_step (CAS (Lit $ LitLoc l) e1 e2) σ
[]
stuck_term σ
[]
| AllocS n l σ :
0 < n →
(∀ m, σ !! (l +ₗ m) = None) →
head_step (Alloc $ Lit $ LitInt n) σ
base_step (Alloc $ Lit $ LitInt n) σ
[]
(Lit $ LitLoc l) (init_mem l (Z.to_nat n) σ)
[]
| FreeS n l σ :
0 < n →
(∀ m, is_Some (σ !! (l +ₗ m)) ↔ 0 ≤ m < n) →
head_step (Free (Lit $ LitInt n) (Lit $ LitLoc l)) σ
base_step (Free (Lit $ LitInt n) (Lit $ LitLoc l)) σ
[]
(Lit LitPoison) (free_mem l (Z.to_nat n) σ)
[]
| CaseS i el e σ :
0 ≤ i →
el !! (Z.to_nat i) = Some e →
head_step (Case (Lit $ LitInt i) el) σ [] e σ []
base_step (Case (Lit $ LitInt i) el) σ [] e σ []
| ForkS e σ:
head_step (Fork e) σ [] (Lit LitPoison) σ [e].
base_step (Fork e) σ [] (Lit LitPoison) σ [e].
(** Basic properties about the language *)
Lemma to_of_val v : to_val (of_val v) = Some v.
......@@ -345,10 +344,10 @@ Proof.
revert v; induction e; intros v ?; simplify_option_eq; auto with f_equal.
Qed.
Instance of_val_inj : Inj (=) (=) of_val.
Global Instance of_val_inj : Inj (=) (=) of_val.
Proof. by intros ?? Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed.
Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
Global Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
Proof. destruct Ki; intros ???; simplify_eq/=; auto with f_equal. Qed.
Lemma fill_item_val Ki e :
......@@ -356,11 +355,11 @@ Lemma fill_item_val Ki e :
Proof. intros [v ?]. destruct Ki; simplify_option_eq; eauto. Qed.
Lemma val_stuck e1 σ1 κ e2 σ2 ef :
head_step e1 σ1 κ e2 σ2 ef → to_val e1 = None.
base_step e1 σ1 κ e2 σ2 ef → to_val e1 = None.
Proof. destruct 1; naive_solver. Qed.
Lemma head_ctx_step_val Ki e σ1 κ e2 σ2 ef :
head_step (fill_item Ki e) σ1 κ e2 σ2 ef → is_Some (to_val e).
Lemma base_ctx_step_val Ki e σ1 κ e2 σ2 ef :
base_step (fill_item Ki e) σ1 κ e2 σ2 ef → is_Some (to_val e).
Proof.
destruct Ki; inversion_clear 1; decompose_Forall_hyps;
simplify_option_eq; by eauto.
......@@ -371,7 +370,8 @@ Lemma list_expr_val_eq_inv vl1 vl2 e1 e2 el1 el2 :
map of_val vl1 ++ e1 :: el1 = map of_val vl2 ++ e2 :: el2 →
vl1 = vl2 ∧ el1 = el2.
Proof.
revert vl2; induction vl1; destruct vl2; intros H1 H2; inversion 1.
revert vl2; induction vl1 as [|? vl1 IHvl1];
intros vl2; destruct vl2 as [|? vl2]; intros H1 H2; inversion 1.
- done.
- subst. by rewrite to_of_val in H1.
- subst. by rewrite to_of_val in H2.
......@@ -401,8 +401,8 @@ Proof. rewrite /shift_loc /=. f_equal. lia. Qed.
Lemma shift_loc_0_nat l : l +ₗ 0%nat = l.
Proof. destruct l as [b o]. rewrite /shift_loc /=. f_equal. lia. Qed.
Instance shift_loc_inj l : Inj (=) (=) (shift_loc l).
Proof. destruct l as [b o]; intros n n' [=?]; lia. Qed.
Global Instance shift_loc_inj l : Inj (=) (=) (shift_loc l).
Proof. destruct l as [b o]; intros n n' [= ?]; lia. Qed.
Lemma shift_loc_block l n : (l +ₗ n).1 = l.1.
Proof. done. Qed.
......@@ -429,14 +429,14 @@ Proof.
Qed.
Definition fresh_block (σ : state) : block :=
let loclst : list loc := elements (dom _ σ : gset loc) in
let blockset : gset block := foldr (λ l, ({[l.1]} ∪)) ∅ loclst in
let loclst : list loc := elements (dom σ : gset loc) in
let blockset : gset block := foldr (λ l, ({[l.1]} ∪.)) ∅ loclst in
fresh blockset.
Lemma is_fresh_block σ i : σ !! (fresh_block σ,i) = None.
Proof.
assert (∀ (l : loc) ls (X : gset block),
l ∈ ls → l.1 ∈ foldr (λ l, ({[l.1]} ∪)) X ls) as help.
l ∈ ls → l.1 ∈ foldr (λ l, ({[l.1]} ∪.)) X ls) as help.
{ induction 1; set_solver. }
rewrite /fresh_block /shift_loc /= -(not_elem_of_dom (D := gset loc)) -elem_of_elements.
move=> /(help _ _ ∅) /=. apply is_fresh.
......@@ -446,9 +446,9 @@ Lemma alloc_fresh n σ :
let l := (fresh_block σ, 0) in
let init := repeat (LitV $ LitInt 0) (Z.to_nat n) in
0 < n →
head_step (Alloc $ Lit $ LitInt n) σ [] (Lit $ LitLoc l) (init_mem l (Z.to_nat n) σ) [].
base_step (Alloc $ Lit $ LitInt n) σ [] (Lit $ LitLoc l) (init_mem l (Z.to_nat n) σ) [].
Proof.
intros l init Hn. apply AllocS. auto.
intros l init Hn. apply AllocS; first done.
- intros i. apply (is_fresh_block _ i).
Qed.
......@@ -468,11 +468,13 @@ Qed.
(** Closed expressions *)
Lemma is_closed_weaken X Y e : is_closed X e → X ⊆ Y → is_closed Y e.
Proof.
revert e X Y. fix FIX 1; destruct e=>X Y/=; try naive_solver.
revert e X Y. fix FIX 1; intros e; destruct e=>X Y/=; try naive_solver.
- naive_solver set_solver.
- rewrite !andb_True. intros [He Hel] HXY. split. by eauto.
- rewrite !andb_True. intros [He Hel] HXY. split; first by eauto.
rename select (list expr) into el.
induction el=>/=; naive_solver.
- rewrite !andb_True. intros [He Hel] HXY. split. by eauto.
- rewrite !andb_True. intros [He Hel] HXY. split; first by eauto.
rename select (list expr) into el.
induction el=>/=; naive_solver.
Qed.
......@@ -481,12 +483,16 @@ Proof. intros. by apply is_closed_weaken with [], list_subseteq_nil. Qed.
Lemma is_closed_subst X e x es : is_closed X e → x ∉ X → subst x es e = e.
Proof.
revert e X. fix FIX 1; destruct e=> X /=; rewrite ?bool_decide_spec ?andb_True=> He ?;
revert e X. fix FIX 1; intros e; destruct e=> X /=; rewrite ?bool_decide_spec ?andb_True=> He ?;
repeat case_bool_decide; simplify_eq/=; f_equal;
try by intuition eauto with set_solver.
- case He=> _. clear He. induction el=>//=. rewrite andb_True=>?.
- case He=> _. clear He.
rename select (list expr) into el.
induction el=>//=. rewrite andb_True=>?.
f_equal; intuition eauto with set_solver.
- case He=> _. clear He. induction el=>//=. rewrite andb_True=>?.
- case He=> _. clear He.
rename select (list expr) into el.
induction el=>//=. rewrite andb_True=>?.
f_equal; intuition eauto with set_solver.
Qed.
......@@ -502,14 +508,18 @@ Proof. intros <-%of_to_val. apply is_closed_of_val. Qed.
Lemma subst_is_closed X x es e :
is_closed X es → is_closed (x::X) e → is_closed X (subst x es e).
Proof.
revert e X. fix FIX 1; destruct e=>X //=; repeat (case_bool_decide=>//=);
revert e X. fix FIX 1; intros e; destruct e=>X //=; repeat (case_bool_decide=>//=);
try naive_solver; rewrite ?andb_True; intros.
- set_solver.
- eauto using is_closed_weaken with set_solver.
- eapply is_closed_weaken; first done.
rename select binder into f.
rename select (list binder) into xl.
destruct (decide (BNamed x = f)), (decide (BNamed x ∈ xl)); set_solver.
- split; first naive_solver. induction el; naive_solver.
- split; first naive_solver. induction el; naive_solver.
- split; first naive_solver.
rename select (list expr) into el. induction el; naive_solver.
- split; first naive_solver.
rename select (list expr) into el. induction el; naive_solver.
Qed.
Lemma subst'_is_closed X b es e :
......@@ -530,16 +540,16 @@ Proof.
Qed.
(* Misc *)
Lemma stuck_not_head_step σ e' κ σ' ef :
¬head_step stuck_term σ e' κ σ' ef.
Lemma stuck_not_base_step σ e' κ σ' ef :
¬base_step stuck_term σ e' κ σ' ef.
Proof. inversion 1. Qed.
(** Equality and other typeclass stuff *)
Instance base_lit_dec_eq : EqDecision base_lit.
Global Instance base_lit_dec_eq : EqDecision base_lit.
Proof. solve_decision. Defined.
Instance bin_op_dec_eq : EqDecision bin_op.
Global Instance bin_op_dec_eq : EqDecision bin_op.
Proof. solve_decision. Defined.
Instance un_op_dec_eq : EqDecision order.
Global Instance un_op_dec_eq : EqDecision order.
Proof. solve_decision. Defined.
Fixpoint expr_beq (e : expr) (e' : expr) : bool :=
......@@ -570,41 +580,41 @@ Fixpoint expr_beq (e : expr) (e' : expr) : bool :=
end.
Lemma expr_beq_correct (e1 e2 : expr) : expr_beq e1 e2 ↔ e1 = e2.
Proof.
revert e1 e2; fix FIX 1.
revert e1 e2; fix FIX 1. intros e1 e2.
destruct e1 as [| | | |? el1| | | | | |? el1|],
e2 as [| | | |? el2| | | | | |? el2|]; simpl; try done;
rewrite ?andb_True ?bool_decide_spec ?FIX;
try (split; intro; [destruct_and?|split_and?]; congruence).
- match goal with |- context [?F el1 el2] => assert (F el1 el2 ↔ el1 = el2) end.
{ revert el2. induction el1 as [|el1h el1q]; destruct el2; try done.
{ revert el2. induction el1 as [|el1h el1q]; intros el2; destruct el2; try done.
specialize (FIX el1h). naive_solver. }
clear FIX. naive_solver.
- match goal with |- context [?F el1 el2] => assert (F el1 el2 ↔ el1 = el2) end.
{ revert el2. induction el1 as [|el1h el1q]; destruct el2; try done.
{ revert el2. induction el1 as [|el1h el1q]; intros el2; destruct el2; try done.
specialize (FIX el1h). naive_solver. }
clear FIX. naive_solver.
Qed.
Instance expr_dec_eq : EqDecision expr.
Global Instance expr_dec_eq : EqDecision expr.
Proof.
refine (λ e1 e2, cast_if (decide (expr_beq e1 e2))); by rewrite -expr_beq_correct.
Defined.
Instance val_dec_eq : EqDecision val.
Global Instance val_dec_eq : EqDecision val.
Proof.
refine (λ v1 v2, cast_if (decide (of_val v1 = of_val v2))); abstract naive_solver.
Defined.
Instance expr_inhabited : Inhabited expr := populate (Lit LitPoison).
Instance val_inhabited : Inhabited val := populate (LitV LitPoison).
Global Instance expr_inhabited : Inhabited expr := populate (Lit LitPoison).
Global Instance val_inhabited : Inhabited val := populate (LitV LitPoison).
Canonical Structure stateO := leibnizO state.
Canonical Structure valO := leibnizO val.
Canonical Structure exprO := leibnizO expr.
(** Language *)
Lemma lrust_lang_mixin : EctxiLanguageMixin of_val to_val fill_item head_step.
Lemma lrust_lang_mixin : EctxiLanguageMixin of_val to_val fill_item base_step.
Proof.
split; apply _ || eauto using to_of_val, of_to_val,
val_stuck, fill_item_val, fill_item_no_val_inj, head_ctx_step_val.
val_stuck, fill_item_val, fill_item_no_val_inj, base_ctx_step_val.
Qed.
Canonical Structure lrust_ectxi_lang := EctxiLanguage lrust_lang_mixin.
Canonical Structure lrust_ectx_lang := EctxLanguageOfEctxi lrust_ectxi_lang.
......@@ -614,7 +624,7 @@ Canonical Structure lrust_lang := LanguageOfEctx lrust_ectx_lang.
Lemma stuck_irreducible K σ : irreducible (fill K stuck_term) σ.
Proof.
apply: (irreducible_fill (K:=ectx_language.fill K)); first done.
apply prim_head_irreducible; unfold stuck_term.
apply prim_base_irreducible; unfold stuck_term.
- inversion 1.
- apply ectxi_language_sub_redexes_are_values.
intros [] ??; simplify_eq/=; eauto; discriminate_list.
......
theories/lang/lib/arc.v → lambda-rust/lang/lib/arc.v
View file @ 0f4ebd6d
From Coq.QArith Require Import Qcanon.
From iris.base_logic.lib Require Import invariants.
From iris.program_logic Require Import weakestpre.
From iris.proofmode Require Import tactics.
From iris.proofmode Require Import proofmode.
From iris.bi Require Import fractional.
From iris.algebra Require Import excl csum frac auth.
From iris.algebra Require Import excl csum frac auth numbers.
From lrust.lang Require Import lang proofmode notation new_delete.
Set Default Proof Using "Type".
From iris.prelude Require Import options.
(* JH: while working on Arc, I think figured that the "weak count
locking" mechanism that Rust is using and that is verified below may
......@@ -100,7 +99,7 @@ Definition try_unwrap_full : val :=
else #2.
(** The CMRA we need. *)
(* Not bundling heapG, as it may be shared with other users. *)
(* Not bundling heapGS, as it may be shared with other users. *)
(* See rc.v for understanding the structure of this CMRA.
The only additional thing is the [optionR (exclR unitO))], used to handle
......@@ -109,13 +108,13 @@ Definition arc_stR :=
prodUR (optionUR (csumR (prodR (prodR fracR positiveR) (optionR (exclR unitO)))
(exclR unitO))) natUR.
Class arcG Σ :=
RcG :> inG Σ (authR arc_stR).
RcG :: inG Σ (authR arc_stR).
Definition arcΣ : gFunctors := #[GFunctor (authR arc_stR)].
Instance subG_arcΣ {Σ} : subG arcΣ Σ → arcG Σ.
Global Instance subG_arcΣ {Σ} : subG arcΣ Σ → arcG Σ.
Proof. solve_inG. Qed.
Section def.
Context `{!lrustG Σ, !arcG Σ} (P1 : Qp → iProp Σ) (P2 : iProp Σ) (N : namespace).
Context `{!lrustGS Σ, !arcG Σ} (P1 : Qp → iProp Σ) (P2 : iProp Σ) (N : namespace).
Definition arc_tok γ q : iProp Σ :=
own γ (◯ (Some $ Cinl (q, 1%positive, None), 0%nat)).
......@@ -159,10 +158,10 @@ Section arc.
this is the lifetime token), and P2 is the thing that is owned by the
protocol when only weak references are left (in practice, P2 is the
ownership of the underlying memory incl. deallocation). *)
Context `{!lrustG Σ, !arcG Σ} (P1 : Qp → iProp Σ) {HP1:Fractional P1}
Context `{!lrustGS Σ, !arcG Σ} (P1 : Qp → iProp Σ) {HP1:Fractional P1}
(P2 : iProp Σ) (N : namespace).
Instance P1_AsFractional q : AsFractional (P1 q) P1 q.
Local Instance P1_AsFractional q : AsFractional (P1 q) P1 q.
Proof using HP1. done. Qed.
Global Instance arc_inv_ne n :
......@@ -189,9 +188,9 @@ Section arc.
iIntros "Hl1 Hl2 [HP1 HP1']".
iMod (own_alloc ((● (Some $ Cinl ((1/2)%Qp, xH, None), O) ⋅
◯ (Some $ Cinl ((1/2)%Qp, xH, None), O))))
as (γ) "[H● H◯]"; first by apply auth_both_valid.
iExists _, _. iFrame. iApply inv_alloc. iExists _. iFrame. iExists _. iFrame.
rewrite Qp_div_2. auto.
as (γ) "[H● H◯]"; first by apply auth_both_valid_discrete.
iFrame. iApply inv_alloc. iExists _. iFrame.
rewrite Qp.div_2. auto.
Qed.
Lemma create_weak E l :
......@@ -199,7 +198,7 @@ Section arc.
Proof.
iIntros "Hl1 Hl2 HP2".
iMod (own_alloc ((● (None, 1%nat) ⋅ ◯ (None, 1%nat)))) as (γ) "[H● H◯]";
first by apply auth_both_valid.
first by apply auth_both_valid_discrete.
iExists _. iFrame. iApply inv_alloc. iExists _. iFrame.
Qed.
......@@ -209,12 +208,12 @@ Section arc.
if decide (strong = xH) then q = q' ∧ wlock = None
else ∃ q'', q' = (q + q'')%Qp⌝.
Proof.
iIntros "H● Htok". iDestruct (own_valid_2 with "H● Htok") as
%[[Hincl%option_included _]%prod_included [Hval _]]%auth_both_valid.
iIntros "H● Htok". iCombine "H● Htok" gives
%[[Hincl%option_included _]%prod_included [Hval _]]%auth_both_valid_discrete.
destruct st, Hincl as [[=]|(?&?&[= <-]&?&[Hincl|Hincl%csum_included])];
simpl in *; subst.
- setoid_subst. iExists _, _, _, _. by iSplit.
- destruct Hincl as [->|[(?&[[??]?]&[=<-]&->&[[[??]%frac_included%Qp_lt_sum
- destruct Hincl as [->|[(?&[[??]?]&[=<-]&->&[[[??]%frac_included%Qp.lt_sum
?%pos_included]%prod_included _]%prod_included)|(?&?&[=]&?)]]; first done.
iExists _, _, _, _. iSplit=>//. simpl in *. destruct decide; [subst;lia|eauto].
Qed.
......@@ -223,7 +222,7 @@ Section arc.
is_arc P1 P2 N γ l -∗ arc_tok_acc γ P (⊤ ∖ ↑N) -∗
{{{ P }}} strong_count [ #l] {{{ (c : nat), RET #c; P ∗ ⌜(c > 0)%nat⌝ }}}.
Proof using HP1.
iIntros "#INV #Hacc !# * HP HΦ". iLöb as "IH". wp_rec.
iIntros "#INV #Hacc !> * HP HΦ". iLöb as "IH". wp_rec.
iInv N as (st) "[>H● H]" "Hclose1".
iMod ("Hacc" with "HP") as (?) "[Hown Hclose2]".
iDestruct (arc_tok_auth_val with "H● Hown") as %(?& strong &?&?&[-> _]).
......@@ -239,7 +238,7 @@ Section arc.
is_arc P1 P2 N γ l -∗ arc_tok_acc γ P (⊤ ∖ ↑N) -∗
{{{ P }}} weak_count [ #l] {{{ (c : Z), RET #c; P ∗ ⌜c >= -1⌝ }}}.
Proof using HP1.
iIntros "#INV #Hacc !# * HP HΦ". iLöb as "IH". wp_rec. wp_op.
iIntros "#INV #Hacc !> * HP HΦ". iLöb as "IH". wp_rec. wp_op.
iInv N as (st) "[>H● H]" "Hclose1".
iMod ("Hacc" with "HP") as (?) "[Hown Hclose2]".
iDestruct (arc_tok_auth_val with "H● Hown") as %(?& strong &wl&?&[-> _]).
......@@ -258,7 +257,7 @@ Section arc.
{{{ P }}} clone_arc [ #l]
{{{ q', RET #☠; P ∗ arc_tok γ q' ∗ P1 q' }}}.
Proof using HP1.
iIntros "#INV #Hacc !# * HP HΦ". iLöb as "IH". wp_rec. wp_bind (!ˢᶜ_)%E.
iIntros "#INV #Hacc !> * HP HΦ". iLöb as "IH". wp_rec. wp_bind (!ˢᶜ_)%E.
iInv N as (st) "[>H● H]" "Hclose1".
iMod ("Hacc" with "HP") as (?) "[Hown Hclose2]".
iDestruct (arc_tok_auth_val with "H● Hown") as %(?& strong &?&?&[-> _]).
......@@ -268,25 +267,24 @@ Section arc.
iModIntro. wp_let. wp_op. wp_bind (CAS _ _ _). iInv N as (st) "[>H● H]" "Hclose1".
iMod ("Hacc" with "HP") as (?) "[Hown Hclose2]".
iDestruct (arc_tok_auth_val with "H● Hown") as %(?&strong'&?&?&[-> _]).
iDestruct "H" as (q) "(>#Hq & [HP1 HP1'] & Hl & Hw)". iDestruct "Hq" as %Hq.
iDestruct "H" as (qq) "(>#Hq & [HP1 HP1'] & Hl & Hw)". iDestruct "Hq" as %Hq.
destruct (decide (strong = strong')) as [->|?].
- wp_apply (wp_cas_int_suc with "Hl"). iIntros "Hl".
iMod (own_update with "H●") as "[H● Hown']".
{ apply auth_update_alloc, prod_local_update_1,
(op_local_update_discrete _ _ (Some (Cinl ((q/2)%Qp, 1%positive, None))))
(op_local_update_discrete _ _ (Some (Cinl ((qq/2)%Qp, 1%positive, None))))
=>-[/= Hqa ?]. split;[split|]=>//=; last by rewrite left_id.
apply frac_valid'. rewrite -Hq comm_L -{2}(Qp_div_2 q).
apply Qcplus_le_mono_l. rewrite -{1}(Qcplus_0_l (_ / _)%Qp).
apply Qcplus_le_mono_r, Qp_ge_0. }
apply frac_valid. rewrite -Hq comm_L.
by apply Qp.add_le_mono_l, Qp.div_le. }
iMod ("Hclose2" with "Hown") as "HP". iModIntro.
iMod ("Hclose1" with "[Hl Hw H● HP1']") as "_".
{ iExists _. iFrame. iExists _. rewrite /= [xH ⋅ _]comm_L. iFrame.
rewrite [(q / 2)%Qp ⋅ _]comm frac_op' -[(_ + _)%Qp]assoc Qp_div_2 left_id_L. auto. }
rewrite [(qq / 2)%Qp ⋅ _]comm frac_op -[(_ + _)%Qp]assoc Qp.div_2 left_id_L. auto. }
iModIntro. wp_case. iApply "HΦ". iFrame.
- wp_apply (wp_cas_int_fail with "Hl"); [congruence|]. iIntros "Hl".
iMod ("Hclose2" with "Hown") as "HP". iModIntro.
iMod ("Hclose1" with "[-HP HΦ]") as "_".
{ iExists _. iFrame. iExists q. auto with iFrame. }
{ iExists _. iFrame. iExists qq. iCombine "HP1 HP1'" as "$". auto with iFrame. }
iModIntro. wp_case. iApply ("IH" with "HP HΦ").
Qed.
......@@ -294,7 +292,7 @@ Section arc.
is_arc P1 P2 N γ l -∗ arc_tok_acc γ P (⊤ ∖ ↑N) -∗
{{{ P }}} downgrade [ #l] {{{ RET #☠; P ∗ weak_tok γ }}}.
Proof.
iIntros "#INV #Hacc !# * HP HΦ". iLöb as "IH". wp_rec. wp_op. wp_bind (!ˢᶜ_)%E.
iIntros "#INV #Hacc !> * HP HΦ". iLöb as "IH". wp_rec. wp_op. wp_bind (!ˢᶜ_)%E.
iInv N as (st) "[>H● H]" "Hclose1".
iApply fupd_wp. iMod ("Hacc" with "HP") as (?) "[Hown Hclose2]".
iDestruct (arc_tok_auth_val with "H● Hown") as %(?&?& wlock & weak &[-> _]).
......@@ -309,14 +307,14 @@ Section arc.
iApply fupd_wp. iMod ("Hacc" with "HP") as (?) "[Hown Hclose2]".
iDestruct (arc_tok_auth_val with "H● Hown") as %(?&?& wlock & weak' &[-> _]).
iMod ("Hclose2" with "Hown") as "HP". iModIntro.
iDestruct "H" as (q) "(>Heq & HP1 & Hl & Hl1)". iDestruct "Heq" as %Heq.
iDestruct "H" as (qq) "(>Heq & HP1 & Hl & Hl1)". iDestruct "Heq" as %Heq.
destruct (decide (weak = weak' ∧ wlock = None)) as [[<- ->]|Hw].
- wp_apply (wp_cas_int_suc with "Hl1"). iIntros "Hl1".
iMod (own_update with "H●") as "[H● Hown']".
{ by apply auth_update_alloc, prod_local_update_2,
(op_local_update_discrete _ _ (1%nat)). }
iMod ("Hclose1" with "[-Hown' HP HΦ]") as "_".
{ iExists _. iFrame. iExists _.
{ iExists _. iFrame.
rewrite Z.add_comm -(Nat2Z.inj_add 1) /=. auto with iFrame. }
iModIntro. wp_case. iApply "HΦ". iFrame.
- destruct wlock.
......@@ -335,9 +333,9 @@ Section arc.
Lemma weak_tok_auth_val γ st :
own γ (● st) -∗ weak_tok γ -∗ ⌜∃ st' weak, st = (st', S weak) ∧ ✓ st'⌝.
Proof.
iIntros "H● Htok". iDestruct (own_valid_2 with "H● Htok") as
iIntros "H● Htok". iCombine "H● Htok" gives
%[[Hincl%option_included Hincl'%nat_included]%prod_included [Hval _]]
%auth_both_valid.
%auth_both_valid_discrete.
destruct st as [?[]], Hincl as [_|(?&?&[=]&?)]; simpl in *; try lia. eauto.
Qed.
......@@ -345,11 +343,11 @@ Section arc.
is_arc P1 P2 N γ l -∗ weak_tok_acc γ P (⊤ ∖ ↑N) -∗
{{{ P }}} clone_weak [ #l] {{{ RET #☠; P ∗ weak_tok γ }}}.
Proof.
iIntros "#INV #Hacc !# * HP HΦ". iLöb as "IH". wp_rec. wp_op. wp_bind (!ˢᶜ_)%E.
iIntros "#INV #Hacc !> * HP HΦ". iLöb as "IH". wp_rec. wp_op. wp_bind (!ˢᶜ_)%E.
iAssert (□ (P ={⊤,⊤∖↑N}=∗ ∃ w : Z, (l +ₗ 1) ↦ #w ∗
((l +ₗ 1) ↦ #(w + 1) ={⊤∖↑N,⊤}=∗ P ∗ weak_tok γ) ∧
((l +ₗ 1) ↦ #w ={⊤∖↑N,⊤}=∗ P)))%I as "#Hproto".
{ iIntros "!# HP". iInv N as (st) "[>H● H]" "Hclose1".
{ iIntros "!> HP". iInv N as (st) "[>H● H]" "Hclose1".
iMod ("Hacc" with "HP") as "[Hown Hclose2]".
iDestruct (weak_tok_auth_val with "H● Hown") as %(st' & weak & -> & Hval).
iMod ("Hclose2" with "Hown") as "HP".
......@@ -393,28 +391,27 @@ Section arc.
{{{ P }}} upgrade [ #l]
{{{ (b : bool) q, RET #b; P ∗ if b then arc_tok γ q ∗ P1 q else True }}}.
Proof using HP1.
iIntros "#INV #Hacc !# * HP HΦ". iLöb as "IH". wp_rec. wp_bind (!ˢᶜ_)%E.
iIntros "#INV #Hacc !> * HP HΦ". iLöb as "IH". wp_rec. wp_bind (!ˢᶜ_)%E.
iAssert (□ (P ={⊤,∅}=∗ ∃ s : Z, l ↦ #s ∗
(⌜s ≠ 0⌝ -∗ l ↦ #(s + 1) ={∅,⊤}=∗ ∃ q, P ∗ arc_tok γ q ∗ ▷ P1 q) ∧
(l ↦ #s ={∅,⊤}=∗ P)))%I as "#Hproto".
{ iIntros "!# HP". iInv N as (st) "[>H● H]" "Hclose1".
{ iIntros "!> HP". iInv N as (st) "[>H● H]" "Hclose1".
iMod ("Hacc" with "HP") as "[Hown Hclose2]".
iDestruct (weak_tok_auth_val with "H● Hown") as %(st' & weak & -> & Hval).
destruct st' as [[[[??]?]| |]|]; try done; iExists _.
destruct st' as [[[[q' c]?]| |]|]; try done; iExists _.
- iDestruct "H" as (q) "(>Heq & [HP1 HP1'] & >$ & ?)". iDestruct "Heq" as %Heq.
iIntros "!>"; iSplit; iMod ("Hclose2" with "Hown") as "HP".
+ iIntros "_ Hl". iExists (q/2)%Qp. iMod (own_update with "H●") as "[H● $]".
{ apply auth_update_alloc. rewrite -[(_,0%nat)]right_id.
apply op_local_update_discrete=>Hv. constructor; last done.
split; last by rewrite /= left_id; apply Hv. split=>[|//].
apply frac_valid'. rewrite -Heq comm_L -{2}(Qp_div_2 q).
apply Qcplus_le_mono_l. rewrite -{1}(Qcplus_0_l (_ / _)%Qp).
apply Qcplus_le_mono_r, Qp_ge_0. }
iFrame. iApply "Hclose1". iExists _. iFrame. iExists _. iFrame.
rewrite /= [xH ⋅ _]comm_L frac_op' [(_ + c)%Qp]comm -[(_ + _)%Qp]assoc
Qp_div_2 left_id_L. auto with iFrame.
apply frac_valid. rewrite /= -Heq comm_L.
by apply Qp.add_le_mono_l, Qp.div_le. }
iFrame. iApply "Hclose1". iExists _. iFrame.
rewrite /= [xH ⋅ _]comm_L frac_op [(_ + q')%Qp]comm -[(_ + _)%Qp]assoc
Qp.div_2 left_id_L. auto with iFrame.
+ iIntros "Hl". iFrame. iApply ("Hclose1" with "[-]"). iExists _. iFrame.
iExists q. auto with iFrame.
iExists q. iCombine "HP1 HP1'" as "$". auto with iFrame.
- iDestruct "H" as "[>$ ?]". iIntros "!>"; iSplit; first by auto with congruence.
iIntros "Hl". iMod ("Hclose2" with "Hown") as "$". iApply "Hclose1".
iExists _. auto with iFrame.
......@@ -440,12 +437,12 @@ Section arc.
{{{ weak_tok γ }}} drop_weak [ #l]
{{{ (b : bool), RET #b ; if b then P2 ∗ l ↦ #0 ∗ (l +ₗ 1) ↦ #0 else True }}}.
Proof.
iIntros "#INV !# * Hown HΦ". iLöb as "IH". wp_rec. wp_op. wp_bind (!ˢᶜ_)%E.
iIntros "#INV !> * Hown HΦ". iLöb as "IH". wp_rec. wp_op. wp_bind (!ˢᶜ_)%E.
iAssert (□ (weak_tok γ ={⊤,⊤ ∖ ↑N}=∗ ∃ w : Z, (l +ₗ 1) ↦ #w ∗
((l +ₗ 1) ↦ #(w - 1) ={⊤ ∖ ↑N,⊤}=∗ ⌜w ≠ 1⌝ ∨
▷ P2 ∗ l ↦ #0 ∗ (l +ₗ 1) ↦ #0) ∧
((l +ₗ 1) ↦ #w ={⊤ ∖ ↑N,⊤}=∗ weak_tok γ)))%I as "#Hproto".
{ iIntros "!# Hown". iInv N as (st) "[>H● H]" "Hclose1".
{ iIntros "!> Hown". iInv N as (st) "[>H● H]" "Hclose1".
iDestruct (weak_tok_auth_val with "H● Hown") as %(st' & weak & -> & Hval).
destruct st' as [[[[??][?|]]| |]|]; try done; [|iExists _..].
- by iDestruct "H" as (?) "(_ & _ & _ & _ & >%)".
......@@ -492,7 +489,7 @@ Section arc.
Proof.
iIntros "INV H◯ HP2". iInv N as ([st ?]) "[>H● H]" "Hclose".
iDestruct (own_valid_2 with "H● H◯")
as %[[[[=]|Hincl]%option_included _]%prod_included [? _]]%auth_both_valid.
as %[[[[=]|Hincl]%option_included _]%prod_included [? _]]%auth_both_valid_discrete.
simpl in Hincl. destruct Hincl as (?&?&[=<-]&->&[?|[]%exclusive_included]);
try done; try apply _. setoid_subst.
iMod (own_update_2 with "H● H◯") as "[H● $]".
......@@ -506,10 +503,10 @@ Section arc.
{{{ arc_tok γ q ∗ P1 q }}} drop_arc [ #l]
{{{ (b : bool), RET #b ; if b then P1 1 ∗ (P2 ={⊤}=∗ weak_tok γ) else True }}}.
Proof using HP1.
iIntros "#INV !# * [Hown HP1] HΦ". iLöb as "IH".
iIntros "#INV !> * [Hown HP1] HΦ". iLöb as "IH".
wp_rec. wp_bind (!ˢᶜ_)%E. iInv N as (st) "[>H● H]" "Hclose".
iDestruct (arc_tok_auth_val with "H● Hown") as %(?& s &?&?&[-> _]).
iDestruct "H" as (?) "(? & ? & ? & ?)". wp_read.
iDestruct "H" as (x') "(? & ? & ? & ?)". wp_read.
iMod ("Hclose" with "[-Hown HP1 HΦ]") as "_". { iExists _. auto with iFrame. }
iModIntro. wp_let. wp_op. wp_bind (CAS _ _ _). iInv N as (st) "[>H● H]" "Hclose".
iDestruct (arc_tok_auth_val with "H● Hown") as %(q' & s' & wl & w &[-> Hqq']).
......@@ -520,18 +517,20 @@ Section arc.
+ destruct Hqq' as [<- ->].
iMod (own_update_2 with "H● Hown") as "[H● H◯]".
{ apply auth_update, prod_local_update_1. rewrite -[x in (x, _)]right_id.
etrans; first apply cancel_local_update_unit, _.
etrans; first apply: cancel_local_update_unit.
by apply (op_local_update _ _ (Some (Cinr (Excl ())))). }
iMod ("Hclose" with "[H● Hs Hw]") as "_"; first by iExists _; do 2 iFrame.
iModIntro. wp_case. iApply wp_fupd. wp_op.
iApply ("HΦ"). rewrite -{2}Hq''. iFrame. by iApply close_last_strong.
iApply ("HΦ"). rewrite -{2}Hq''. iCombine "HP1 HP1'" as "$".
by iApply close_last_strong.
+ destruct Hqq' as [? ->].
rewrite -[in (_, _)](Pos.succ_pred s) // -[wl in Cinl (_, wl)]left_id
-Pos.add_1_l -2!pair_op -Cinl_op Some_op.
-Pos.add_1_l 2!pair_op Cinl_op Some_op.
iMod (own_update_2 _ _ _ _ with "H● Hown") as "H●".
{ apply auth_update_dealloc, prod_local_update_1, @cancel_local_update_unit, _. }
iMod ("Hclose" with "[- HΦ]") as "_".
{ iExists _. iFrame. iExists (q + q'')%Qp. iFrame. iSplit; last by destruct s.
{ iExists _. iCombine "HP1 HP1'" as "HP". iFrame "H●". iFrame.
iSplit; last by destruct s.
iIntros "!> !%". rewrite assoc -Hq''. f_equal. apply comm, _. }
iModIntro. wp_case. wp_op; case_bool_decide; simplify_eq. by iApply "HΦ".
- wp_apply (wp_cas_int_fail with "Hs"); [congruence|]. iIntros "Hs".
......@@ -546,17 +545,18 @@ Section arc.
{{{ (b : bool), RET #b ;
if b then P1 1 ∗ (P2 ={⊤}=∗ weak_tok γ) else arc_tok γ q ∗ P1 q }}}.
Proof using HP1.
iIntros "#INV !# * [Hown HP1] HΦ". wp_rec. iInv N as (st) "[>H● H]" "Hclose".
iIntros "#INV !> * [Hown HP1] HΦ". wp_rec. iInv N as (st) "[>H● H]" "Hclose".
iDestruct (arc_tok_auth_val with "H● Hown") as %(q' & s & wl & w &[-> Hqq']).
iDestruct "H" as (q'') "(>Hq'' & HP1' & Hs & Hw)". iDestruct "Hq''" as %Hq''.
destruct (decide (s = xH)) as [->|?].
- wp_apply (wp_cas_int_suc with "Hs"). iIntros "Hs".
destruct Hqq' as [<- ->]. iMod (own_update_2 with "H● Hown") as "[H● H◯]".
{ apply auth_update, prod_local_update_1. rewrite -[x in (x, _)]right_id.
etrans; first apply cancel_local_update_unit, _.
etrans; first apply: cancel_local_update_unit.
by apply (op_local_update _ _ (Some (Cinr (Excl ())))). }
iMod ("Hclose" with "[H● Hs Hw]") as "_"; first by iExists _; do 2 iFrame.
iApply ("HΦ" $! true). rewrite -{1}Hq''. iFrame. by iApply close_last_strong.
iApply ("HΦ" $! true). rewrite -{1}Hq''. iCombine "HP1 HP1'" as "$".
by iApply close_last_strong.
- wp_apply (wp_cas_int_fail with "Hs"); [congruence|]. iIntros "Hs".
iMod ("Hclose" with "[-Hown HP1 HΦ]") as "_"; first by iExists _; auto with iFrame.
iApply ("HΦ" $! false). by iFrame.
......@@ -569,7 +569,7 @@ Section arc.
if b then l ↦ #1 ∗ (l +ₗ 1) ↦ #1 ∗ P1 1
else arc_tok γ q ∗ P1 q }}}.
Proof using HP1.
iIntros "#INV !# * [Hown HP1] HΦ". wp_rec. wp_bind (CAS _ _ _). wp_op.
iIntros "#INV !> * [Hown HP1] HΦ". wp_rec. wp_bind (CAS _ _ _). wp_op.
iInv N as (st) "[>H● H]" "Hclose".
iDestruct (arc_tok_auth_val with "H● Hown") as %(? & ? & wl & w &[-> _]).
iDestruct "H" as (?) "(>Hq'' & HP1' & >Hs & >Hw)".
......@@ -588,8 +588,8 @@ Section arc.
(alloc_option_local_update (Excl ())). }
iMod ("Hclose" with "[-HΦ HP1 H◯]") as "_"; first by iExists _; eauto with iFrame.
iModIntro. wp_case. wp_bind (!ˢᶜ_)%E. iInv N as ([st ?]) "[>H● H]" "Hclose".
iDestruct (own_valid_2 with "H● H◯") as
%[[[[=]|Hincl]%option_included _]%prod_included [? _]]%auth_both_valid.
iCombine "H● H◯" gives
%[[[[=]|Hincl]%option_included _]%prod_included [? _]]%auth_both_valid_discrete.
simpl in Hincl. destruct Hincl as (? & ? & [=<-] & -> & [|Hincl]); last first.
+ apply csum_included in Hincl. destruct Hincl as [->|[Hincl|(?&?&[=]&?)]]=>//.
destruct Hincl as (?&[[??]?]&[=<-]&->&[[_ Hlt]%prod_included _]%prod_included).
......@@ -598,9 +598,9 @@ Section arc.
iMod ("Hclose" with "[-HΦ H◯ HP1]") as "_"; first by iExists _; auto with iFrame.
iModIntro. wp_let. wp_op; case_bool_decide; [lia|]. wp_let. wp_op. wp_bind (_ <-ˢᶜ _)%E.
iInv N as ([st w]) "[>H● H]" "Hclose".
iDestruct (own_valid_2 with "H● H◯") as
%[[[[=]|Hincl]%option_included _]%prod_included [Hval _]]%auth_both_valid.
simpl in Hincl. destruct Hincl as (? & ? & [=<-] & -> & Hincl); last first.
iCombine "H● H◯" gives
%[[[[=]|Hincl]%option_included _]%prod_included [Hval _]]%auth_both_valid_discrete.
simpl in Hincl. destruct Hincl as (x1 & x2 & [=<-] & -> & Hincl); last first.
assert (∃ q p, x2 = Cinl (q, p, Excl' ())) as (? & ? & ->).
{ destruct Hincl as [|Hincl]; first by setoid_subst; eauto.
apply csum_included in Hincl. destruct Hincl as [->|[Hincl|(?&?&[=]&?)]]=>//.
......@@ -613,13 +613,13 @@ Section arc.
csum_local_update_l, prod_local_update_2, delete_option_local_update, _. }
iMod ("Hclose" with "[-HΦ H◯ HP1]") as "_"; first by iExists _; auto with iFrame.
iModIntro. wp_seq. iApply "HΦ". iFrame.
+ setoid_subst. iDestruct "H" as (?) "(Hq & ? & ? & >? & >%)". subst. wp_read.
+ setoid_subst. iDestruct "H" as (?) "(Hq & HP1' & ? & >? & >%)". subst. wp_read.
iMod (own_update_2 with "H● H◯") as "H●".
{ apply auth_update_dealloc. rewrite -{1}[(_, 0%nat)]right_id.
apply cancel_local_update_unit, _. }
iMod ("Hclose" with "[H●]") as "_"; first by iExists _; iFrame.
iModIntro. wp_seq. wp_op. wp_let. wp_op. wp_write. iApply "HΦ".
iDestruct "Hq" as %<-. iFrame.
iDestruct "Hq" as %<-. iCombine "HP1 HP1'" as "$". iFrame.
Qed.
Lemma try_unwrap_full_spec (γ : gname) (q: Qp) (l : loc) :
......@@ -636,7 +636,7 @@ Section arc.
| _ (* 2 *) => arc_tok γ q ∗ P1 q
end }}}.
Proof using HP1.
iIntros "#INV !# * [Hown HP1] HΦ". wp_rec. wp_bind (CAS _ _ _).
iIntros "#INV !> * [Hown HP1] HΦ". wp_rec. wp_bind (CAS _ _ _).
iInv N as (st) "[>H● H]" "Hclose".
iDestruct (arc_tok_auth_val with "H● Hown") as %(q' & s & wl & w &[-> Hqq']).
iDestruct "H" as (q'') "(>Hq'' & HP1' & Hs & Hw)". iDestruct "Hq''" as %Hq''.
......@@ -644,14 +644,14 @@ Section arc.
- wp_apply (wp_cas_int_suc with "Hs")=>//. iIntros "Hs".
destruct Hqq' as [<- ->]. iMod (own_update_2 with "H● Hown") as "[H● H◯]".
{ apply auth_update, prod_local_update_1. rewrite -[x in (x, _)]right_id.
etrans; first apply cancel_local_update_unit, _.
etrans; first apply: cancel_local_update_unit.
by apply (op_local_update _ _ (Some (Cinr (Excl ())))). }
iCombine "HP1" "HP1'" as "HP1". rewrite Hq''. clear Hq'' q''.
iMod ("Hclose" with "[H● Hs Hw]") as "_"; first by iExists _; do 2 iFrame.
clear w. iModIntro. wp_case. wp_op. wp_bind (!ˢᶜ_)%E.
iInv N as ([st w']) "[>H● H]" "Hclose".
iDestruct (own_valid_2 with "H● H◯")
as %[[[[=]|Hincl]%option_included _]%prod_included [? _]]%auth_both_valid.
as %[[[[=]|Hincl]%option_included _]%prod_included [? _]]%auth_both_valid_discrete.
simpl in Hincl. destruct Hincl as (?&?&[=<-]&->&[?|[]%exclusive_included]);
[|by apply _|done]. setoid_subst. iDestruct "H" as "[Hl Hl1]".
wp_read. destruct w'.
......@@ -669,4 +669,4 @@ Section arc.
Qed.
End arc.
Typeclasses Opaque is_arc arc_tok weak_tok.
Global Typeclasses Opaque is_arc arc_tok weak_tok.
theories/lang/lib/lock.v → lambda-rust/lang/lib/lock.v
View file @ 0f4ebd6d
From iris.program_logic Require Import weakestpre.
From iris.proofmode Require Import tactics.
From iris.proofmode Require Import proofmode.
From iris.algebra Require Import excl.
From lrust.lang Require Import lang proofmode notation.
Set Default Proof Using "Type".
From iris.prelude Require Import options.
Definition mklock_unlocked : val := λ: ["l"], "l" <- #false.
Definition mklock_locked : val := λ: ["l"], "l" <- #true.
......@@ -16,13 +16,15 @@ Definition release : val := λ: ["l"], "l" <-ˢᶜ #false.
their cancelling view shift has a non-empty mask, and it would have to be
executed in the consequence view shift of a borrow. *)
Section proof.
Context `{!lrustG Σ}.
Context `{!lrustGS Σ}.
Definition lock_proto (l : loc) (R : iProp Σ) : iProp Σ :=
(∃ b : bool, l ↦ #b ∗ if b then True else R)%I.
Global Instance lock_proto_ne l : NonExpansive (lock_proto l).
Proof. solve_proper. Qed.
Global Instance lock_proto_proper l : Proper ((≡) ==> (≡)) (lock_proto l).
Proof. apply ne_proper, _. Qed.
Lemma lock_proto_iff l R R' :
□ (R ↔ R') -∗ lock_proto l R -∗ lock_proto l R'.
......@@ -34,9 +36,9 @@ Section proof.
Lemma lock_proto_iff_proper l R R' :
□ (R ↔ R') -∗ □ (lock_proto l R ↔ lock_proto l R').
Proof.
iIntros "#HR !#". iSplit; iIntros "Hlck"; iApply (lock_proto_iff with "[HR] Hlck").
iIntros "#HR !>". iSplit; iIntros "Hlck"; iApply (lock_proto_iff with "[HR] Hlck").
- done.
- iAlways; iSplit; iIntros; by iApply "HR".
- iModIntro; iSplit; iIntros; by iApply "HR".
Qed.
(** The main proofs. *)
......@@ -75,7 +77,7 @@ Section proof.
{{{ P }}} try_acquire [ #l ] @ E
{{{ b, RET #b; (if b is true then R else True) ∗ P }}}.
Proof.
iIntros "#Hproto !# * HP HΦ".
iIntros "#Hproto !> * HP HΦ".
wp_rec. iMod ("Hproto" with "HP") as "(Hinv & Hclose)".
iDestruct "Hinv" as ([]) "[Hl HR]".
- wp_apply (wp_cas_int_fail with "Hl"); [done..|]. iIntros "Hl".
......@@ -90,7 +92,7 @@ Section proof.
□ (P ={E,∅}=∗ ▷ lock_proto l R ∗ (▷ lock_proto l R ={∅,E}=∗ P)) -∗
{{{ P }}} acquire [ #l ] @ E {{{ RET #☠; R ∗ P }}}.
Proof.
iIntros "#Hproto !# * HP HΦ". iLöb as "IH". wp_rec.
iIntros "#Hproto !> * HP HΦ". iLöb as "IH". wp_rec.
wp_apply (try_acquire_spec with "Hproto HP"). iIntros ([]).
- iIntros "[HR Hown]". wp_if. iApply "HΦ"; iFrame.
- iIntros "[_ Hown]". wp_if. iApply ("IH" with "Hown HΦ").
......@@ -100,11 +102,11 @@ Section proof.
□ (P ={E,∅}=∗ ▷ lock_proto l R ∗ (▷ lock_proto l R ={∅,E}=∗ P)) -∗
{{{ R ∗ P }}} release [ #l ] @ E {{{ RET #☠; P }}}.
Proof.
iIntros "#Hproto !# * (HR & HP) HΦ". wp_let.
iIntros "#Hproto !> * (HR & HP) HΦ". wp_let.
iMod ("Hproto" with "HP") as "(Hinv & Hclose)".
iDestruct "Hinv" as (b) "[? _]". wp_write. iApply "HΦ".
iApply "Hclose". iExists false. by iFrame.
Qed.
End proof.
Typeclasses Opaque lock_proto.
Global Typeclasses Opaque lock_proto.
theories/lang/lib/memcpy.v → lambda-rust/lang/lib/memcpy.v
View file @ 0f4ebd6d
From lrust.lang Require Export notation.
From lrust.lang Require Import heap proofmode.
Set Default Proof Using "Type".
From iris.prelude Require Import options.
Definition memcpy : val :=
rec: "memcpy" ["dst";"len";"src"] :=
......@@ -19,7 +19,7 @@ Notation "e1 <-{ n ',Σ' i } ! e2" :=
(at level 80, n, i at next level,
format "e1 <-{ n ,Σ i } ! e2") : expr_scope.
Lemma wp_memcpy `{!lrustG Σ} E l1 l2 vl1 vl2 q (n : Z):
Lemma wp_memcpy `{!lrustGS Σ} E l1 l2 vl1 vl2 q (n : Z):
Z.of_nat (length vl1) = n → Z.of_nat (length vl2) = n →
{{{ l1 ↦∗ vl1 ∗ l2 ↦∗{q} vl2 }}}
#l1 <-{n} !#l2 @ E
......@@ -30,7 +30,7 @@ Proof.
- iApply "HΦ". assert (n = O) by lia; subst.
destruct vl1, vl2; try discriminate. by iFrame.
- destruct vl1 as [|v1 vl1], vl2 as [|v2 vl2], n as [|n|]; try (discriminate || lia).
revert Hvl1 Hvl2. intros [= Hvl1] [= Hvl2]; rewrite !heap_mapsto_vec_cons. subst n.
revert Hvl1 Hvl2. intros [= Hvl1] [= Hvl2]; rewrite !heap_pointsto_vec_cons. subst n.
iDestruct "Hl1" as "[Hv1 Hl1]". iDestruct "Hl2" as "[Hv2 Hl2]".
Local Opaque Zminus.
wp_read; wp_write. do 3 wp_op. iApply ("IH" with "[%] [%] Hl1 Hl2"); [lia..|].
......
theories/lang/lib/new_delete.v → lambda-rust/lang/lib/new_delete.v
View file @ 0f4ebd6d
From lrust.lang Require Export notation.
From lrust.lang Require Import heap proofmode memcpy.
Set Default Proof Using "Type".
From iris.prelude Require Import options.
Definition new : val :=
λ: ["n"],
......@@ -13,7 +13,7 @@ Definition delete : val :=
else Free "n" "loc".
Section specs.
Context `{!lrustG Σ}.
Context `{!lrustGS Σ}.
Lemma wp_new E n:
0 ≤ n →
......@@ -23,8 +23,8 @@ Section specs.
Proof.
iIntros (? Φ) "_ HΦ". wp_lam. wp_op; case_bool_decide.
- wp_if. assert (n = 0) as -> by lia. iApply "HΦ".
rewrite heap_mapsto_vec_nil. auto.
- wp_if. wp_alloc l as "H↦" "H†". lia. iApply "HΦ". subst sz. iFrame.
rewrite heap_pointsto_vec_nil. auto.
- wp_if. wp_alloc l as "H↦" "H†"; first lia. iApply "HΦ". subst. iFrame.
Qed.
Lemma wp_delete E (n:Z) l vl :
......