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
  • abstraction
  • 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/places
  • ci/pm_red
  • ci/ralf/const-rf
  • ci/ralf/exact_vm
  • ci/ralf/lia-experiment
  • 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/iprop_structures
  • ci/robbert/naive_solver
  • ci/robbert/pm_faster_alt
  • ci/weak_mem
  • coqbug/match
  • experiments
  • fast_string
  • fnlft
  • gen_big_op
  • gpirlea/pinning
  • 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
  • sharedrw
  • sharedrw2
  • simple
  • simulation
  • skiplist
  • stackedborrows
  • stackedborrows-20200517
  • strong_cas_fail
  • stuck
  • RBrlx-POPL20-artifact
  • popl18
  • popl18-aec
61 results
Show changes
Commits on Source (234)
134 additional commits have been omitted to prevent performance issues.
Hide whitespace changes
Inline Side-by-side
Showing
with 536 additions and 413 deletions
.gitignore
View file @ 0f4ebd6d
...@@ -13,7 +13,7 @@ ...@@ -13,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,25 +28,42 @@ variables: ...@@ -27,25 +28,42 @@ variables:
## Build jobs ## Build jobs
build-coq.dev: build-coq.9.0.0:
<<: *template <<: *template
variables: variables:
OPAM_PINS: "coq version dev" 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.11.2: trigger-iris.timing:
<<: *template <<: *template
variables: variables:
OPAM_PINS: "coq version 8.11.2" OPAM_PINS: "coq version 9.0.0 git+https://gitlab.mpi-sws.org/$IRIS_REPO#$IRIS_REV"
OPAM_PKG: "coq-lambda-rust"
tags: tags:
- fp-timing - 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.12.dev 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
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 exercises solutions \( -name "*.d" -o -name "*.vo" -o -name "*.vo[sk]" -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 .lia.cache 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 "# Installing build-dep package." @echo "# Installing builddep packages."
@opam install $(OPAMFLAGS) build-dep/ @opam install $(OPAMFLAGS) $(BUILDDEPFILES)
.PHONY: builddep
# Some files that do *not* need to be forwarded to Makefile.coq # Backwards compatibility target
Makefile: ; build-dep: builddep
_CoqProject: ; .PHONY: build-dep
opam: ;
# Phony wildcard targets # Some files that do *not* need to be forwarded to Makefile.coq.
phony: ; # ("::" lets Makefile.local overwrite this.)
.PHONY: phony 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) 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
......
README.md
View file @ 0f4ebd6d
...@@ -6,7 +6,7 @@ This is the Coq development accompanying lambda-Rust. ...@@ -6,7 +6,7 @@ This is the Coq development accompanying lambda-Rust.
This version is known to compile with: This version is known to compile with:
- Coq 8.11.2 - 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
...@@ -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
# `-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. # 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
# "Declare Scope" does not exist yet in 8.9.
-arg -w -arg -undeclared-scope
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
opam → coq-lambda-rust.opam
View file @ 0f4ebd6d
opam-version: "2.0" opam-version: "2.0"
name: "coq-lambda-rust"
maintainer: "Ralf Jung <jung@mpi-sws.org>" maintainer: "Ralf Jung <jung@mpi-sws.org>"
authors: "The RustBelt Team" authors: "The RustBelt Team"
license: "BSD" license: "BSD-3-Clause"
homepage: "https://plv.mpi-sws.org/rustbelt/" homepage: "https://plv.mpi-sws.org/rustbelt/"
bug-reports: "https://gitlab.mpi-sws.org/iris/lambda-rust/issues" bug-reports: "https://gitlab.mpi-sws.org/iris/lambda-rust/issues"
dev-repo: "git+https://gitlab.mpi-sws.org/iris/lambda-rust.git" dev-repo: "git+https://gitlab.mpi-sws.org/iris/lambda-rust.git"
...@@ -14,8 +13,8 @@ the type system, and safety proof for some Rust libraries. ...@@ -14,8 +13,8 @@ the type system, and safety proof for some Rust libraries.
""" """
depends: [ depends: [
"coq-iris" { (= "dev.2020-07-22.0.1e8432a9") | (= "dev") } "coq-lifetime-logic" { = version }
] ]
build: [make "-j%{jobs}%"] build: ["./make-package" "lambda-rust" "-j%{jobs}%"]
install: [make "install"] 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
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/heap.v → lambda-rust/lang/heap.v
View file @ 0f4ebd6d
From Coq Require Import Min.
From stdpp Require Import coPset. From stdpp Require Import coPset.
From iris.algebra Require Import big_op gmap frac agree numbers. From iris.algebra Require Import big_op gmap frac agree numbers.
From iris.algebra Require Import csum excl auth cmra_big_op. From iris.algebra Require Import csum excl auth cmra_big_op.
From iris.bi Require Import fractional. From iris.bi Require Import fractional.
From iris.base_logic Require Export lib.own. 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. From lrust.lang Require Export lang.
Set Default Proof Using "Type". From iris.prelude Require Import options.
Import uPred. Import uPred.
Definition lock_stateR : cmraT := Definition lock_stateR : cmra :=
csumR (exclR unitO) natR. 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)). 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))). gmapUR block (prodR fracR (gmapR Z (exclR unitO))).
Class heapG Σ := HeapG { Class heapGS Σ := HeapGS {
heap_inG :> inG Σ (authR heapUR); heap_inG :: inG Σ (authR heapUR);
heap_freeable_inG :> inG Σ (authR heap_freeableUR); heap_freeable_inG :: inG Σ (authR heap_freeableUR);
heap_name : gname; heap_name : gname;
heap_freeable_name : gname heap_freeable_name : gname
}. }.
...@@ -34,28 +34,28 @@ Definition heap_freeable_rel (σ : state) (hF : heap_freeableUR) : Prop := ...@@ -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). qs.2 ≠ ∅ ∧ ∀ i, is_Some (σ !! (blk, i)) ↔ is_Some (qs.2 !! i).
Section definitions. 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 Σ := (l : loc) (q : Qp) (v: val) : iProp Σ :=
own heap_name (◯ {[ l := (q, to_lock_stateR st, to_agree v) ]}). own heap_name (◯ {[ l := (q, to_lock_stateR st, to_agree v) ]}).
Definition heap_mapsto_def (l : loc) (q : Qp) (v: val) : iProp Σ := Definition heap_pointsto_def (l : loc) (q : Qp) (v: val) : iProp Σ :=
heap_mapsto_st (RSt 0) l q v. heap_pointsto_st (RSt 0) l q v.
Definition heap_mapsto_aux : seal (@heap_mapsto_def). by eexists. Qed. Definition heap_pointsto_aux : seal (@heap_pointsto_def). Proof. by eexists. Qed.
Definition heap_mapsto := unseal heap_mapsto_aux. Definition heap_pointsto := unseal heap_pointsto_aux.
Definition heap_mapsto_eq : @heap_mapsto = @heap_mapsto_def := Definition heap_pointsto_eq : @heap_pointsto = @heap_pointsto_def :=
seal_eq heap_mapsto_aux. seal_eq heap_pointsto_aux.
Definition heap_mapsto_vec (l : loc) (q : Qp) (vl : list val) : iProp Σ := Definition heap_pointsto_vec (l : loc) (q : Qp) (vl : list val) : iProp Σ :=
([∗ list] i ↦ v ∈ vl, heap_mapsto (l +ₗ i) q v)%I. ([∗ list] i ↦ v ∈ vl, heap_pointsto (l +ₗ i) q v)%I.
Fixpoint inter (i0 : Z) (n : nat) : gmapR Z (exclR unitO) := Fixpoint inter (i0 : Z) (n : nat) : gmapR Z (exclR unitO) :=
match n with O => ∅ | S n => <[i0 := Excl ()]>(inter (i0+1) n) end. match n with O => ∅ | S n => <[i0 := Excl ()]>(inter (i0+1) n) end.
Definition heap_freeable_def (l : loc) (q : Qp) (n: nat) : iProp Σ := Definition heap_freeable_def (l : loc) (q : Qp) (n: nat) : iProp Σ :=
own heap_freeable_name (◯ {[ l.1 := (q, inter (l.2) n) ]}). 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 := unseal heap_freeable_aux.
Definition heap_freeable_eq : @heap_freeable = @heap_freeable_def := Definition heap_freeable_eq : @heap_freeable = @heap_freeable_def :=
seal_eq heap_freeable_aux. seal_eq heap_freeable_aux.
...@@ -66,17 +66,17 @@ Section definitions. ...@@ -66,17 +66,17 @@ Section definitions.
∗ ⌜heap_freeable_rel σ hF⌝)%I. ∗ ⌜heap_freeable_rel σ hF⌝)%I.
End definitions. End definitions.
Typeclasses Opaque heap_mapsto heap_freeable heap_mapsto_vec. Global Typeclasses Opaque heap_pointsto_vec.
Instance: Params (@heap_mapsto) 4 := {}. Global Instance: Params (@heap_pointsto) 4 := {}.
Instance: Params (@heap_freeable) 5 := {}. 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. (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. (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 Notation "l ↦∗{ q }: P" := (∃ vl, l ↦∗{ q } vl ∗ P vl)%I
(at level 20, q at level 50, format "l ↦∗{ q }: P") : bi_scope. (at level 20, q at level 50, format "l ↦∗{ q }: P") : bi_scope.
...@@ -91,7 +91,7 @@ Section to_heap. ...@@ -91,7 +91,7 @@ Section to_heap.
Implicit Types σ : state. Implicit Types σ : state.
Lemma to_heap_valid σ : ✓ to_heap σ. 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. Lemma lookup_to_heap_None σ l : σ !! l = None → to_heap σ !! l = None.
Proof. by rewrite /to_heap lookup_fmap=> ->. Qed. Proof. by rewrite /to_heap lookup_fmap=> ->. Qed.
...@@ -106,81 +106,86 @@ Section to_heap. ...@@ -106,81 +106,86 @@ Section to_heap.
End to_heap. End to_heap.
Section heap. Section heap.
Context `{!heapG Σ}. Context `{!heapGS Σ}.
Implicit Types P Q : iProp Σ. Implicit Types P Q : iProp Σ.
Implicit Types σ : state. Implicit Types σ : state.
Implicit Types E : coPset. Implicit Types E : coPset.
(** General properties of mapsto and freeable *) (** General properties of pointsto and freeable *)
Global Instance heap_mapsto_timeless l q v : Timeless (l↦{q}v). Global Instance heap_pointsto_timeless l q v : Timeless (l↦{q}v).
Proof. rewrite heap_mapsto_eq /heap_mapsto_def. apply _. Qed. 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. Proof.
intros p q. intros p q.
by rewrite heap_mapsto_eq -own_op -auth_frag_op singleton_op -pair_op agree_idemp. by rewrite heap_pointsto_eq -own_op -auth_frag_op singleton_op -pair_op agree_idemp.
Qed. 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. 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). Global Instance frame_pointsto p l v q1 q2 q :
Proof. rewrite /heap_mapsto_vec. apply _. Qed. 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. 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). by setoid_rewrite (fractional (Φ := λ q, _ ↦{q} _)%I).
Qed. 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. 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). Global Instance heap_freeable_timeless q l n : Timeless (†{q}l…n).
Proof. rewrite heap_freeable_eq /heap_freeable_def. apply _. Qed. 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. 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 /=. eapply pure_elim; [done|]=> /auth_frag_valid /=.
rewrite singleton_op -pair_op singleton_valid=> -[? /agree_op_invL'->]; eauto. rewrite singleton_op -pair_op singleton_valid=> -[? /to_agree_op_inv_L->]; eauto.
Qed. Qed.
Lemma heap_mapsto_vec_nil l q : l ↦∗{q} [] ⊣⊢ True. Lemma heap_pointsto_vec_nil l q : l ↦∗{q} [] ⊣⊢ True.
Proof. by rewrite /heap_mapsto_vec. Qed. 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. l ↦∗{q} (vl1 ++ vl2) ⊣⊢ l ↦∗{q} vl1 ∗ (l +ₗ length vl1) ↦∗{q} vl2.
Proof. 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. do 2 f_equiv. intros k v. by rewrite shift_loc_assoc_nat.
Qed. Qed.
Lemma heap_mapsto_vec_singleton l q v : l ↦∗{q} [v] ⊣⊢ l ↦{q} v. Lemma heap_pointsto_vec_singleton l q v : l ↦∗{q} [v] ⊣⊢ l ↦{q} v.
Proof. by rewrite /heap_mapsto_vec /= shift_loc_0 right_id. Qed. 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. l ↦∗{q} (v :: vl) ⊣⊢ l ↦{q} v ∗ (l +ₗ 1) ↦∗{q} vl.
Proof. 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. 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 → length vl1 = length vl2 →
l ↦∗{q1} vl1 ∗ l ↦∗{q2} vl2 ⊣⊢ ⌜vl1 = vl2⌝ ∧ l ↦∗{q1+q2} vl1. l ↦∗{q1} vl1 ∗ l ↦∗{q2} vl2 ⊣⊢ ⌜vl1 = vl2⌝ ∧ l ↦∗{q1+q2} vl1.
Proof. Proof.
intros Hlen%Forall2_same_length. apply (anti_symm (⊢)). intros Hlen%Forall2_same_length. apply (anti_symm (⊢)).
- revert l. induction Hlen as [|v1 v2 vl1 vl2 _ _ IH]=> l. - revert l. induction Hlen as [|v1 v2 vl1 vl2 _ _ IH]=> l.
{ rewrite !heap_mapsto_vec_nil. iIntros "_"; auto. } { rewrite !heap_pointsto_vec_nil. iIntros "_"; auto. }
rewrite !heap_mapsto_vec_cons. iIntros "[[Hv1 Hvl1] [Hv2 Hvl2]]". rewrite !heap_pointsto_vec_cons. iIntros "[[Hv1 Hvl1] [Hv2 Hvl2]]".
iDestruct (IH (l +ₗ 1) with "[$Hvl1 $Hvl2]") as "[% $]"; subst. iDestruct (IH (l +ₗ 1) with "[$Hvl1 $Hvl2]") as "[% $]"; subst.
rewrite (inj_iff (.:: vl2)). rewrite (inj_iff (.:: vl2)).
iDestruct (heap_mapsto_agree with "[$Hv1 $Hv2]") as %<-. iDestruct (heap_pointsto_agree with "[$Hv1 $Hv2]") as %<-.
iSplit; first done. iFrame. iSplit; first done. iFrame.
- by iIntros "[% [$ Hl2]]"; subst. - by iIntros "[% [$ Hl2]]"; subst.
Qed. 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⌝) → (∀ vl, Φ vl -∗ ⌜length vl = n⌝) →
l ↦∗{q1}: Φ ∗ l ↦∗{q2}: (λ vl, ⌜length vl = n⌝) ⊣⊢ l ↦∗{q1+q2}: Φ. l ↦∗{q1}: Φ ∗ l ↦∗{q2}: (λ vl, ⌜length vl = n⌝) ⊣⊢ l ↦∗{q1+q2}: Φ.
Proof. Proof.
...@@ -188,37 +193,37 @@ Section heap. ...@@ -188,37 +193,37 @@ Section heap.
- iIntros "[Hmt1 Hmt2]". - iIntros "[Hmt1 Hmt2]".
iDestruct "Hmt1" as (vl) "[Hmt1 Hown]". iDestruct "Hmt2" as (vl') "[Hmt2 %]". iDestruct "Hmt1" as (vl) "[Hmt1 Hown]". iDestruct "Hmt2" as (vl') "[Hmt2 %]".
iDestruct (Hlen with "Hown") as %?. 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. iDestruct "Hmt" as "[_ Hmt]". iExists vl. by iFrame.
- iIntros "Hmt". iDestruct "Hmt" as (vl) "[[Hmt1 Hmt2] Hown]". - iIntros "Hmt". iDestruct "Hmt" as (vl) "[[Hmt1 Hmt2] Hown]".
iDestruct (Hlen with "Hown") as %?. iDestruct (Hlen with "Hown") as %?.
iSplitL "Hmt1 Hown"; iExists _; by iFrame. iSplitL "Hmt1 Hown"; iExists _; by iFrame.
Qed. 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. l ↦∗{q}: Φ1 -∗ (∀ vl, Φ1 vl -∗ Φ2 vl) -∗ l ↦∗{q}: Φ2.
Proof. Proof.
iIntros "Hm Hwand". iDestruct "Hm" as (vl) "[Hm HΦ]". iExists vl. iIntros "Hm Hwand". iDestruct "Hm" as (vl) "[Hm HΦ]". iExists vl.
iFrame "Hm". by iApply "Hwand". iFrame "Hm". by iApply "Hwand".
Qed. 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). □ (∀ vl, Φ1 vl ↔ Φ2 vl) -∗ □ (l ↦∗{q}: Φ1 ↔ l ↦∗{q}: Φ2).
Proof. 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Φ". iIntros; by iApply "HΦ".
Qed. Qed.
Lemma heap_mapsto_vec_combine l q vl : Lemma heap_pointsto_vec_combine l q vl :
vl ≠ [] → vl ≠ [] →
l ↦∗{q} vl ⊣⊢ own heap_name (◯ [^op list] i ↦ v ∈ vl, l ↦∗{q} vl ⊣⊢ own heap_name (◯ [^op list] i ↦ v ∈ vl,
{[l +ₗ i := (q, Cinr 0%nat, to_agree v)]}). {[l +ₗ i := (q, Cinr 0%nat, to_agree v)]}).
Proof. 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 //. rewrite (big_opL_commute auth_frag) big_opL_commute1 //.
Qed. 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. (∀ vl, Persistent (P vl)) → Fractional (λ q, l ↦∗{q}: P)%I.
Proof. Proof.
intros p q q'. iSplit. intros p q q'. iSplit.
...@@ -227,13 +232,13 @@ Section heap. ...@@ -227,13 +232,13 @@ Section heap.
- iIntros "[H1 H2]". iDestruct "H1" as (vl1) "[Hown1 #HP1]". - iIntros "[H1 H2]". iDestruct "H1" as (vl1) "[Hown1 #HP1]".
iDestruct "H2" as (vl2) "[Hown2 #HP2]". iDestruct "H2" as (vl2) "[Hown2 #HP2]".
set (ll := min (length vl1) (length vl2)). 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 _]". iDestruct "Hown1" as "[Hown1 _]". iDestruct "Hown2" as "[Hown2 _]".
iCombine "Hown1" "Hown2" as "Hown". rewrite heap_mapsto_vec_op; last first. iCombine "Hown1" "Hown2" as "Hown". rewrite heap_pointsto_vec_op; last first.
{ rewrite !firstn_length. subst ll. { rewrite !length_firstn. subst ll.
rewrite -!min_assoc min_idempotent min_comm -min_assoc min_idempotent min_comm. done. } 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. 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. + iClear "HP2". rewrite take_ge; last first.
{ rewrite -Heq /ll. done. } { rewrite -Heq /ll. done. }
rewrite drop_ge; first by rewrite app_nil_r. by rewrite -Heq. rewrite drop_ge; first by rewrite app_nil_r. by rewrite -Heq.
...@@ -241,9 +246,9 @@ Section heap. ...@@ -241,9 +246,9 @@ Section heap.
{ rewrite -Heq /ll. done. } { rewrite -Heq /ll. done. }
rewrite drop_ge; first by rewrite app_nil_r. by rewrite -Heq. rewrite drop_ge; first by rewrite app_nil_r. by rewrite -Heq.
Qed. 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. (∀ 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): Lemma inter_lookup_Some i j (n : nat):
i ≤ j < i+n → inter i n !! j = Excl' (). i ≤ j < i+n → inter i n !! j = Excl' ().
...@@ -266,10 +271,10 @@ Section heap. ...@@ -266,10 +271,10 @@ Section heap.
- by rewrite !inter_lookup_None; try lia. - by rewrite !inter_lookup_None; try lia.
Qed. Qed.
Lemma inter_valid i n : ✓ inter i n. 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' : 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. Proof.
by rewrite heap_freeable_eq /heap_freeable_def -own_op -auth_frag_op by rewrite heap_freeable_eq /heap_freeable_def -own_op -auth_frag_op
singleton_op -pair_op inter_op. singleton_op -pair_op inter_op.
...@@ -343,13 +348,13 @@ Section heap. ...@@ -343,13 +348,13 @@ Section heap.
∗ own heap_name (◯ [^op list] i ↦ v ∈ (repeat (LitV LitPoison) n), ∗ own heap_name (◯ [^op list] i ↦ v ∈ (repeat (LitV LitPoison) n),
{[l +ₗ i := (1%Qp, Cinr 0%nat, to_agree v)]}). {[l +ₗ i := (1%Qp, Cinr 0%nat, to_agree v)]}).
Proof. 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|]. revert l FREE. induction n as [|n IH]=> l FRESH; [done|].
rewrite (big_opL_consZ_l (λ k _, _ (_ k) _ )) /=. rewrite (big_opL_consZ_l (λ k _, _ (_ k) _ )) /=.
etrans; first apply (IH (l +ₗ 1)). etrans; first apply (IH (l +ₗ 1)).
{ intros. by rewrite shift_loc_assoc. } { intros. by rewrite shift_loc_assoc. }
rewrite shift_loc_0 -insert_singleton_op; last first. 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 lookup_singleton_None -{2}(shift_loc_0 l). apply not_inj; lia. }
rewrite to_heap_insert. setoid_rewrite shift_loc_assoc. rewrite to_heap_insert. setoid_rewrite shift_loc_assoc.
apply alloc_local_update; last done. apply lookup_to_heap_None. apply alloc_local_update; last done. apply lookup_to_heap_None.
...@@ -365,17 +370,18 @@ Section heap. ...@@ -365,17 +370,18 @@ Section heap.
Proof. Proof.
intros ??; iDestruct 1 as (hF) "(Hvalσ & HhF & %)". intros ??; iDestruct 1 as (hF) "(Hvalσ & HhF & %)".
assert (Z.to_nat n ≠ O). { rewrite -(Nat2Z.id 0)=>/Z2Nat.inj. lia. } 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]". iMod (own_update _ (● hF) with "HhF") as "[HhF Hfreeable]".
{ apply auth_update_alloc, { apply auth_update_alloc,
(alloc_singleton_local_update _ (l.1) (1%Qp, inter (l.2) (Z.to_nat n))). (alloc_singleton_local_update _ (l.1) (1%Qp, inter (l.2) (Z.to_nat n))).
- eauto using heap_freeable_rel_None. - eauto using heap_freeable_rel_None.
- split. done. apply inter_valid. } - split; first done. apply inter_valid. }
iModIntro. iSplitL "Hvalσ HhF". iModIntro. iSplitL "Hvalσ HhF".
{ iExists _. iFrame. iPureIntro. { iExists _. iFrame. iPureIntro.
auto using heap_freeable_rel_init_mem. } auto using heap_freeable_rel_init_mem. }
rewrite heap_freeable_eq /heap_freeable_def heap_mapsto_vec_combine //. rewrite heap_freeable_eq /heap_freeable_def heap_pointsto_vec_combine //; last first.
iFrame. destruct (Z.to_nat n); done. { destruct (Z.to_nat n); done. }
iFrame.
Qed. Qed.
Lemma heap_free_vs σ l vl : Lemma heap_free_vs σ l vl :
...@@ -383,14 +389,14 @@ Section heap. ...@@ -383,14 +389,14 @@ Section heap.
{[l +ₗ i := (1%Qp, Cinr 0%nat, to_agree v)]}) {[l +ₗ i := (1%Qp, Cinr 0%nat, to_agree v)]})
==∗ own heap_name (● to_heap (free_mem l (length vl) σ)). ==∗ own heap_name (● to_heap (free_mem l (length vl) σ)).
Proof. 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|]. revert σ l. induction vl as [|v vl IH]=> σ l; [done|].
rewrite (big_opL_consZ_l (λ k _, _ (_ k) _ )) /= shift_loc_0. rewrite (big_opL_consZ_l (λ k _, _ (_ k) _ )) /= shift_loc_0.
apply local_update_total_valid=> _ Hvalid _. apply local_update_total_valid=> _ Hvalid _.
assert (([^op list] k↦y ∈ vl, assert (([^op list] k↦y ∈ vl,
{[l +ₗ (1 + k) := (1%Qp, Cinr 0%nat, to_agree y)]} : heapUR) !! l = None). {[l +ₗ (1 + k) := (1%Qp, Cinr 0%nat, to_agree y)]} : heapUR) !! l = None).
{ move: (Hvalid l). rewrite lookup_op lookup_singleton. { 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. rewrite -insert_singleton_op //. etrans.
{ apply (delete_local_update _ _ l (1%Qp, Cinr 0%nat, to_agree v)). { apply (delete_local_update _ _ l (1%Qp, Cinr 0%nat, to_agree v)).
by rewrite lookup_insert. } by rewrite lookup_insert. }
...@@ -406,7 +412,7 @@ Section heap. ...@@ -406,7 +412,7 @@ Section heap.
Proof. Proof.
iDestruct 1 as (hF) "(Hvalσ & HhF & REL)"; iDestruct "REL" as %REL. iDestruct 1 as (hF) "(Hvalσ & HhF & REL)"; iDestruct "REL" as %REL.
iIntros "Hmt Hf". rewrite heap_freeable_eq /heap_freeable_def. iIntros "Hmt Hf". rewrite heap_freeable_eq /heap_freeable_def.
iDestruct (own_valid_2 with "HhF Hf") as % [Hl Hv]%auth_both_valid. iCombine "HhF Hf" gives % [Hl Hv]%auth_both_valid_discrete.
move: Hl=> /singleton_included_l [[q qs] [/leibniz_equiv_iff Hl Hq]]. move: Hl=> /singleton_included_l [[q qs] [/leibniz_equiv_iff Hl Hq]].
apply (Some_included_exclusive _ _) in Hq as [=<-<-]%leibniz_equiv; last first. apply (Some_included_exclusive _ _) in Hq as [=<-<-]%leibniz_equiv; last first.
{ move: (Hv (l.1)). rewrite Hl. by intros [??]. } { move: (Hv (l.1)). rewrite Hl. by intros [??]. }
...@@ -414,7 +420,7 @@ Section heap. ...@@ -414,7 +420,7 @@ Section heap.
{ intros ->. by destruct (REL (l.1) (1%Qp, ∅)) as [[] ?]. } { intros ->. by destruct (REL (l.1) (1%Qp, ∅)) as [[] ?]. }
assert (0 < n) by (subst n; by destruct vl). assert (0 < n) by (subst n; by destruct vl).
iMod (heap_free_vs with "[Hmt Hvalσ]") as "Hvalσ". 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". iMod (own_update_2 with "HhF Hf") as "HhF".
{ apply auth_update_dealloc, (delete_singleton_local_update _ _ _). } { apply auth_update_dealloc, (delete_singleton_local_update _ _ _). }
iModIntro; subst. repeat iSplit; eauto using heap_freeable_is_Some. iModIntro; subst. repeat iSplit; eauto using heap_freeable_is_Some.
...@@ -422,14 +428,14 @@ Section heap. ...@@ -422,14 +428,14 @@ Section heap.
eauto using heap_freeable_rel_free_mem. eauto using heap_freeable_rel_free_mem.
Qed. 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 (● to_heap σ) -∗
own heap_name (◯ {[ l := (q, to_lock_stateR ls, to_agree v) ]}) -∗ own heap_name (◯ {[ l := (q, to_lock_stateR ls, to_agree v) ]}) -∗
⌜∃ n' : nat, ⌜∃ n' : nat,
σ !! l = Some (match ls with RSt n => RSt (n+n') | WSt => WSt end, v)⌝. σ !! l = Some (match ls with RSt n => RSt (n+n') | WSt => WSt end, v)⌝.
Proof. Proof.
iIntros "H● H◯". iIntros "H● H◯".
iDestruct (own_valid_2 with "H● H◯") as %[Hl?]%auth_both_valid. iCombine "H● H◯" gives %[Hl?]%auth_both_valid_discrete.
iPureIntro. move: Hl=> /singleton_included_l [[[q' ls'] dv]]. iPureIntro. move: Hl=> /singleton_included_l [[[q' ls'] dv]].
rewrite /to_heap lookup_fmap fmap_Some_equiv. rewrite /to_heap lookup_fmap fmap_Some_equiv.
move=> [[[ls'' v'] [?[[/=??]->]]]]; simplify_eq. move=> [[[ls'' v'] [?[[/=??]->]]]]; simplify_eq.
...@@ -437,16 +443,18 @@ Section heap. ...@@ -437,16 +443,18 @@ Section heap.
[/Some_pair_included [_ Hincl] /to_agree_included->]. [/Some_pair_included [_ Hincl] /to_agree_included->].
destruct ls as [|n], ls'' as [|n''], destruct ls as [|n], ls'' as [|n''],
Hincl as [[[|n'|]|] [=]%leibniz_equiv]; subst. 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. 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 (● to_heap σ) -∗
own heap_name (◯ {[ l := (1%Qp, to_lock_stateR ls, to_agree v) ]}) -∗ own heap_name (◯ {[ l := (1%Qp, to_lock_stateR ls, to_agree v) ]}) -∗
⌜σ !! l = Some (ls, v)⌝. ⌜σ !! l = Some (ls, v)⌝.
Proof. Proof.
iIntros "H● H◯". iIntros "H● H◯".
iDestruct (own_valid_2 with "H● H◯") as %[Hl?]%auth_both_valid. iCombine "H● H◯" gives %[Hl?]%auth_both_valid_discrete.
iPureIntro. move: Hl=> /singleton_included_l [[[q' ls'] dv]]. iPureIntro. move: Hl=> /singleton_included_l [[[q' ls'] dv]].
rewrite /to_heap lookup_fmap fmap_Some_equiv. rewrite /to_heap lookup_fmap fmap_Some_equiv.
move=> [[[ls'' v'] [?[[/=??]->]]] Hincl]; simplify_eq. move=> [[[ls'' v'] [?[[/=??]->]]] Hincl]; simplify_eq.
...@@ -457,12 +465,12 @@ Section heap. ...@@ -457,12 +465,12 @@ Section heap.
Lemma heap_read_vs σ n1 n2 nf l q v: Lemma heap_read_vs σ n1 n2 nf l q v:
σ !! l = Some (RSt (n1 + nf), 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)]> σ)) ==∗ 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. Proof.
intros Hσv. apply wand_intro_r. rewrite -!own_op to_heap_insert. intros Hσv. apply entails_wand, wand_intro_r. rewrite -!own_op to_heap_insert.
eapply own_update, auth_update, singleton_local_update. iApply own_update. eapply auth_update, singleton_local_update.
{ by rewrite /to_heap lookup_fmap Hσv. } { by rewrite /to_heap lookup_fmap Hσv. }
apply prod_local_update_1, prod_local_update_2, csum_local_update_r. apply prod_local_update_1, prod_local_update_2, csum_local_update_r.
apply nat_local_update; lia. apply nat_local_update; lia.
...@@ -472,16 +480,16 @@ Section heap. ...@@ -472,16 +480,16 @@ Section heap.
heap_ctx σ -∗ l ↦{q} v -∗ ∃ n, ⌜σ !! l = Some (RSt n, v)⌝. heap_ctx σ -∗ l ↦{q} v -∗ ∃ n, ⌜σ !! l = Some (RSt n, v)⌝.
Proof. Proof.
iDestruct 1 as (hF) "(Hσ & HhF & REL)". iIntros "Hmt". iDestruct 1 as (hF) "(Hσ & HhF & REL)". iIntros "Hmt".
rewrite heap_mapsto_eq. rewrite heap_pointsto_eq.
iDestruct (heap_mapsto_lookup with "Hσ Hmt") as %[n Hσl]; eauto. iDestruct (heap_pointsto_lookup with "Hσ Hmt") as %[n Hσl]; eauto.
Qed. Qed.
Lemma heap_read_1 σ l v : Lemma heap_read_1 σ l v :
heap_ctx σ -∗ l ↦ v -∗ ⌜σ !! l = Some (RSt 0, v)⌝. heap_ctx σ -∗ l ↦ v -∗ ⌜σ !! l = Some (RSt 0, v)⌝.
Proof. Proof.
iDestruct 1 as (hF) "(Hσ & HhF & REL)". iIntros "Hmt". iDestruct 1 as (hF) "(Hσ & HhF & REL)". iIntros "Hmt".
rewrite heap_mapsto_eq. rewrite heap_pointsto_eq.
iDestruct (heap_mapsto_lookup_1 with "Hσ Hmt") as %?; auto. iDestruct (heap_pointsto_lookup_1 with "Hσ Hmt") as %?; auto.
Qed. Qed.
Lemma heap_read_na σ l q v : Lemma heap_read_na σ l q v :
...@@ -492,13 +500,13 @@ Section heap. ...@@ -492,13 +500,13 @@ Section heap.
heap_ctx (<[l:=(RSt n2, v)]> σ2) ∗ l ↦{q} v. heap_ctx (<[l:=(RSt n2, v)]> σ2) ∗ l ↦{q} v.
Proof. Proof.
iDestruct 1 as (hF) "(Hσ & HhF & %)"; iIntros "Hmt". iDestruct 1 as (hF) "(Hσ & HhF & %)"; iIntros "Hmt".
rewrite heap_mapsto_eq. rewrite heap_pointsto_eq.
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 _ 0 1 with "Hσ Hmt") as "[Hσ Hmt]"; first done. iMod (heap_read_vs _ 0 1 with "Hσ Hmt") as "[Hσ Hmt]"; first done.
iModIntro. iExists n; iSplit; [done|]. iSplitL "HhF Hσ". iModIntro. iExists n; iSplit; [done|]. iSplitL "HhF Hσ".
{ iExists hF. iFrame. eauto using heap_freeable_rel_stable. } { iExists hF. iFrame. eauto using heap_freeable_rel_stable. }
clear dependent n σ hF. iIntros (σ2). iDestruct 1 as (hF) "(Hσ & HhF & %)". 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. iMod (heap_read_vs _ 1 0 with "Hσ Hmt") as "[Hσ Hmt]"; first done.
iExists n; iModIntro; iSplit; [done|]. iFrame "Hmt". iExists n; iModIntro; iSplit; [done|]. iFrame "Hmt".
iExists hF. iFrame. eauto using heap_freeable_rel_stable. iExists hF. iFrame. eauto using heap_freeable_rel_stable.
...@@ -506,12 +514,12 @@ Section heap. ...@@ -506,12 +514,12 @@ Section heap.
Lemma heap_write_vs σ st1 st2 l v v': Lemma heap_write_vs σ st1 st2 l v v':
σ !! l = Some (st1, 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')]> σ)) ==∗ 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. Proof.
intros Hσv. apply wand_intro_r. rewrite -!own_op to_heap_insert. intros Hσv. apply entails_wand, wand_intro_r. rewrite -!own_op to_heap_insert.
eapply own_update, auth_update, singleton_local_update. iApply own_update. eapply auth_update, singleton_local_update.
{ by rewrite /to_heap lookup_fmap Hσv. } { by rewrite /to_heap lookup_fmap Hσv. }
apply exclusive_local_update. by destruct st2. apply exclusive_local_update. by destruct st2.
Qed. Qed.
...@@ -520,8 +528,8 @@ Section heap. ...@@ -520,8 +528,8 @@ Section heap.
heap_ctx σ -∗ l ↦ v ==∗ heap_ctx (<[l:=(RSt 0, v')]> σ) ∗ l ↦ v'. heap_ctx σ -∗ l ↦ v ==∗ heap_ctx (<[l:=(RSt 0, v')]> σ) ∗ l ↦ v'.
Proof. Proof.
iDestruct 1 as (hF) "(Hσ & HhF & %)". iIntros "Hmt". iDestruct 1 as (hF) "(Hσ & HhF & %)". iIntros "Hmt".
rewrite heap_mapsto_eq. rewrite heap_pointsto_eq.
iDestruct (heap_mapsto_lookup_1 with "Hσ Hmt") as %?; auto. iDestruct (heap_pointsto_lookup_1 with "Hσ Hmt") as %?; auto.
iMod (heap_write_vs with "Hσ Hmt") as "[Hσ $]"; first done. iMod (heap_write_vs with "Hσ Hmt") as "[Hσ $]"; first done.
iModIntro. iExists _. iFrame. eauto using heap_freeable_rel_stable. iModIntro. iExists _. iFrame. eauto using heap_freeable_rel_stable.
Qed. Qed.
...@@ -534,13 +542,13 @@ Section heap. ...@@ -534,13 +542,13 @@ Section heap.
heap_ctx (<[l:=(RSt 0, v')]> σ2) ∗ l ↦ v'. heap_ctx (<[l:=(RSt 0, v')]> σ2) ∗ l ↦ v'.
Proof. Proof.
iDestruct 1 as (hF) "(Hσ & HhF & %)"; iIntros "Hmt". iDestruct 1 as (hF) "(Hσ & HhF & %)"; iIntros "Hmt".
rewrite heap_mapsto_eq. rewrite heap_pointsto_eq.
iDestruct (heap_mapsto_lookup_1 with "Hσ Hmt") as %?; eauto. iDestruct (heap_pointsto_lookup_1 with "Hσ Hmt") as %?; eauto.
iMod (heap_write_vs with "Hσ Hmt") as "[Hσ Hmt]"; first done. iMod (heap_write_vs with "Hσ Hmt") as "[Hσ Hmt]"; first done.
iModIntro. iSplit; [done|]. iSplitL "HhF Hσ". iModIntro. iSplit; [done|]. iSplitL "HhF Hσ".
{ iExists hF. iFrame. eauto using heap_freeable_rel_stable. } { iExists hF. iFrame. eauto using heap_freeable_rel_stable. }
clear dependent σ hF. iIntros (σ2). iDestruct 1 as (hF) "(Hσ & HhF & %)". 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. iMod (heap_write_vs with "Hσ Hmt") as "[Hσ Hmt]"; first done.
iModIntro; iSplit; [done|]. iFrame "Hmt". iModIntro; iSplit; [done|]. iFrame "Hmt".
iExists hF. iFrame. eauto using heap_freeable_rel_stable. 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 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,7 +429,7 @@ Proof. ...@@ -429,7 +429,7 @@ 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.
...@@ -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/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.base_logic.lib Require Import invariants.
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.bi Require Import fractional. From iris.bi Require Import fractional.
From iris.algebra Require Import excl csum frac auth numbers. From iris.algebra Require Import excl csum frac auth numbers.
From lrust.lang Require Import lang proofmode notation new_delete. 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 (* JH: while working on Arc, I think figured that the "weak count
locking" mechanism that Rust is using and that is verified below may locking" mechanism that Rust is using and that is verified below may
...@@ -100,7 +99,7 @@ Definition try_unwrap_full : val := ...@@ -100,7 +99,7 @@ Definition try_unwrap_full : val :=
else #2. else #2.
(** The CMRA we need. *) (** 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. (* See rc.v for understanding the structure of this CMRA.
The only additional thing is the [optionR (exclR unitO))], used to handle The only additional thing is the [optionR (exclR unitO))], used to handle
...@@ -109,13 +108,13 @@ Definition arc_stR := ...@@ -109,13 +108,13 @@ Definition arc_stR :=
prodUR (optionUR (csumR (prodR (prodR fracR positiveR) (optionR (exclR unitO))) prodUR (optionUR (csumR (prodR (prodR fracR positiveR) (optionR (exclR unitO)))
(exclR unitO))) natUR. (exclR unitO))) natUR.
Class arcG Σ := Class arcG Σ :=
RcG :> inG Σ (authR arc_stR). RcG :: inG Σ (authR arc_stR).
Definition arcΣ : gFunctors := #[GFunctor (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. Proof. solve_inG. Qed.
Section def. 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 Σ := Definition arc_tok γ q : iProp Σ :=
own γ (◯ (Some $ Cinl (q, 1%positive, None), 0%nat)). own γ (◯ (Some $ Cinl (q, 1%positive, None), 0%nat)).
...@@ -159,10 +158,10 @@ Section arc. ...@@ -159,10 +158,10 @@ Section arc.
this is the lifetime token), and P2 is the thing that is owned by the 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 protocol when only weak references are left (in practice, P2 is the
ownership of the underlying memory incl. deallocation). *) 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). (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. Proof using HP1. done. Qed.
Global Instance arc_inv_ne n : Global Instance arc_inv_ne n :
...@@ -189,9 +188,9 @@ Section arc. ...@@ -189,9 +188,9 @@ Section arc.
iIntros "Hl1 Hl2 [HP1 HP1']". iIntros "Hl1 Hl2 [HP1 HP1']".
iMod (own_alloc ((● (Some $ Cinl ((1/2)%Qp, xH, None), O) ⋅ iMod (own_alloc ((● (Some $ Cinl ((1/2)%Qp, xH, None), O) ⋅
◯ (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. as (γ) "[H● H◯]"; first by apply auth_both_valid_discrete.
iExists _, _. iFrame. iApply inv_alloc. iExists _. iFrame. iExists _. iFrame. iFrame. iApply inv_alloc. iExists _. iFrame.
rewrite Qp_div_2. auto. rewrite Qp.div_2. auto.
Qed. Qed.
Lemma create_weak E l : Lemma create_weak E l :
...@@ -199,7 +198,7 @@ Section arc. ...@@ -199,7 +198,7 @@ Section arc.
Proof. Proof.
iIntros "Hl1 Hl2 HP2". iIntros "Hl1 Hl2 HP2".
iMod (own_alloc ((● (None, 1%nat) ⋅ ◯ (None, 1%nat)))) as (γ) "[H● H◯]"; 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. iExists _. iFrame. iApply inv_alloc. iExists _. iFrame.
Qed. Qed.
...@@ -209,12 +208,12 @@ Section arc. ...@@ -209,12 +208,12 @@ Section arc.
if decide (strong = xH) then q = q' ∧ wlock = None if decide (strong = xH) then q = q' ∧ wlock = None
else ∃ q'', q' = (q + q'')%Qp⌝. else ∃ q'', q' = (q + q'')%Qp⌝.
Proof. Proof.
iIntros "H● Htok". iDestruct (own_valid_2 with "H● Htok") as iIntros "H● Htok". iCombine "H● Htok" gives
%[[Hincl%option_included _]%prod_included [Hval _]]%auth_both_valid. %[[Hincl%option_included _]%prod_included [Hval _]]%auth_both_valid_discrete.
destruct st, Hincl as [[=]|(?&?&[= <-]&?&[Hincl|Hincl%csum_included])]; destruct st, Hincl as [[=]|(?&?&[= <-]&?&[Hincl|Hincl%csum_included])];
simpl in *; subst. simpl in *; subst.
- setoid_subst. iExists _, _, _, _. by iSplit. - 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. ?%pos_included]%prod_included _]%prod_included)|(?&?&[=]&?)]]; first done.
iExists _, _, _, _. iSplit=>//. simpl in *. destruct decide; [subst;lia|eauto]. iExists _, _, _, _. iSplit=>//. simpl in *. destruct decide; [subst;lia|eauto].
Qed. Qed.
...@@ -223,7 +222,7 @@ Section arc. ...@@ -223,7 +222,7 @@ Section arc.
is_arc P1 P2 N γ l -∗ arc_tok_acc γ P (⊤ ∖ ↑N) -∗ is_arc P1 P2 N γ l -∗ arc_tok_acc γ P (⊤ ∖ ↑N) -∗
{{{ P }}} strong_count [ #l] {{{ (c : nat), RET #c; P ∗ ⌜(c > 0)%nat⌝ }}}. {{{ P }}} strong_count [ #l] {{{ (c : nat), RET #c; P ∗ ⌜(c > 0)%nat⌝ }}}.
Proof using HP1. 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". iInv N as (st) "[>H● H]" "Hclose1".
iMod ("Hacc" with "HP") as (?) "[Hown Hclose2]". iMod ("Hacc" with "HP") as (?) "[Hown Hclose2]".
iDestruct (arc_tok_auth_val with "H● Hown") as %(?& strong &?&?&[-> _]). iDestruct (arc_tok_auth_val with "H● Hown") as %(?& strong &?&?&[-> _]).
...@@ -239,7 +238,7 @@ Section arc. ...@@ -239,7 +238,7 @@ Section arc.
is_arc P1 P2 N γ l -∗ arc_tok_acc γ P (⊤ ∖ ↑N) -∗ is_arc P1 P2 N γ l -∗ arc_tok_acc γ P (⊤ ∖ ↑N) -∗
{{{ P }}} weak_count [ #l] {{{ (c : Z), RET #c; P ∗ ⌜c >= -1⌝ }}}. {{{ P }}} weak_count [ #l] {{{ (c : Z), RET #c; P ∗ ⌜c >= -1⌝ }}}.
Proof using HP1. 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". iInv N as (st) "[>H● H]" "Hclose1".
iMod ("Hacc" with "HP") as (?) "[Hown Hclose2]". iMod ("Hacc" with "HP") as (?) "[Hown Hclose2]".
iDestruct (arc_tok_auth_val with "H● Hown") as %(?& strong &wl&?&[-> _]). iDestruct (arc_tok_auth_val with "H● Hown") as %(?& strong &wl&?&[-> _]).
...@@ -258,7 +257,7 @@ Section arc. ...@@ -258,7 +257,7 @@ Section arc.
{{{ P }}} clone_arc [ #l] {{{ P }}} clone_arc [ #l]
{{{ q', RET #☠; P ∗ arc_tok γ q' ∗ P1 q' }}}. {{{ q', RET #☠; P ∗ arc_tok γ q' ∗ P1 q' }}}.
Proof using HP1. 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". iInv N as (st) "[>H● H]" "Hclose1".
iMod ("Hacc" with "HP") as (?) "[Hown Hclose2]". iMod ("Hacc" with "HP") as (?) "[Hown Hclose2]".
iDestruct (arc_tok_auth_val with "H● Hown") as %(?& strong &?&?&[-> _]). iDestruct (arc_tok_auth_val with "H● Hown") as %(?& strong &?&?&[-> _]).
...@@ -275,18 +274,17 @@ Section arc. ...@@ -275,18 +274,17 @@ Section arc.
{ apply auth_update_alloc, prod_local_update_1, { apply auth_update_alloc, prod_local_update_1,
(op_local_update_discrete _ _ (Some (Cinl ((qq/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. =>-[/= Hqa ?]. split;[split|]=>//=; last by rewrite left_id.
apply frac_valid'. rewrite -Hq comm_L -{2}(Qp_div_2 qq). apply frac_valid. rewrite -Hq comm_L.
apply Qcplus_le_mono_l. rewrite -{1}(Qcplus_0_l (_ / _)%Qp). by apply Qp.add_le_mono_l, Qp.div_le. }
apply Qcplus_le_mono_r, Qp_ge_0. }
iMod ("Hclose2" with "Hown") as "HP". iModIntro. iMod ("Hclose2" with "Hown") as "HP". iModIntro.
iMod ("Hclose1" with "[Hl Hw H● HP1']") as "_". iMod ("Hclose1" with "[Hl Hw H● HP1']") as "_".
{ iExists _. iFrame. iExists _. rewrite /= [xH ⋅ _]comm_L. iFrame. { iExists _. iFrame. iExists _. rewrite /= [xH ⋅ _]comm_L. iFrame.
rewrite [(qq / 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. iModIntro. wp_case. iApply "HΦ". iFrame.
- wp_apply (wp_cas_int_fail with "Hl"); [congruence|]. iIntros "Hl". - wp_apply (wp_cas_int_fail with "Hl"); [congruence|]. iIntros "Hl".
iMod ("Hclose2" with "Hown") as "HP". iModIntro. iMod ("Hclose2" with "Hown") as "HP". iModIntro.
iMod ("Hclose1" with "[-HP HΦ]") as "_". iMod ("Hclose1" with "[-HP HΦ]") as "_".
{ iExists _. iFrame. iExists qq. auto with iFrame. } { iExists _. iFrame. iExists qq. iCombine "HP1 HP1'" as "$". auto with iFrame. }
iModIntro. wp_case. iApply ("IH" with "HP HΦ"). iModIntro. wp_case. iApply ("IH" with "HP HΦ").
Qed. Qed.
...@@ -294,7 +292,7 @@ Section arc. ...@@ -294,7 +292,7 @@ Section arc.
is_arc P1 P2 N γ l -∗ arc_tok_acc γ P (⊤ ∖ ↑N) -∗ is_arc P1 P2 N γ l -∗ arc_tok_acc γ P (⊤ ∖ ↑N) -∗
{{{ P }}} downgrade [ #l] {{{ RET #☠; P ∗ weak_tok γ }}}. {{{ P }}} downgrade [ #l] {{{ RET #☠; P ∗ weak_tok γ }}}.
Proof. 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". iInv N as (st) "[>H● H]" "Hclose1".
iApply fupd_wp. iMod ("Hacc" with "HP") as (?) "[Hown Hclose2]". iApply fupd_wp. iMod ("Hacc" with "HP") as (?) "[Hown Hclose2]".
iDestruct (arc_tok_auth_val with "H● Hown") as %(?&?& wlock & weak &[-> _]). iDestruct (arc_tok_auth_val with "H● Hown") as %(?&?& wlock & weak &[-> _]).
...@@ -316,7 +314,7 @@ Section arc. ...@@ -316,7 +314,7 @@ Section arc.
{ by apply auth_update_alloc, prod_local_update_2, { by apply auth_update_alloc, prod_local_update_2,
(op_local_update_discrete _ _ (1%nat)). } (op_local_update_discrete _ _ (1%nat)). }
iMod ("Hclose1" with "[-Hown' HP HΦ]") as "_". iMod ("Hclose1" with "[-Hown' HP HΦ]") as "_".
{ iExists _. iFrame. iExists _. { iExists _. iFrame.
rewrite Z.add_comm -(Nat2Z.inj_add 1) /=. auto with iFrame. } rewrite Z.add_comm -(Nat2Z.inj_add 1) /=. auto with iFrame. }
iModIntro. wp_case. iApply "HΦ". iFrame. iModIntro. wp_case. iApply "HΦ". iFrame.
- destruct wlock. - destruct wlock.
...@@ -335,9 +333,9 @@ Section arc. ...@@ -335,9 +333,9 @@ Section arc.
Lemma weak_tok_auth_val γ st : Lemma weak_tok_auth_val γ st :
own γ (● st) -∗ weak_tok γ -∗ ⌜∃ st' weak, st = (st', S weak) ∧ ✓ st'⌝. own γ (● st) -∗ weak_tok γ -∗ ⌜∃ st' weak, st = (st', S weak) ∧ ✓ st'⌝.
Proof. 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 _]] %[[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. destruct st as [?[]], Hincl as [_|(?&?&[=]&?)]; simpl in *; try lia. eauto.
Qed. Qed.
...@@ -345,11 +343,11 @@ Section arc. ...@@ -345,11 +343,11 @@ Section arc.
is_arc P1 P2 N γ l -∗ weak_tok_acc γ P (⊤ ∖ ↑N) -∗ is_arc P1 P2 N γ l -∗ weak_tok_acc γ P (⊤ ∖ ↑N) -∗
{{{ P }}} clone_weak [ #l] {{{ RET #☠; P ∗ weak_tok γ }}}. {{{ P }}} clone_weak [ #l] {{{ RET #☠; P ∗ weak_tok γ }}}.
Proof. 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 ∗ iAssert (□ (P ={⊤,⊤∖↑N}=∗ ∃ w : Z, (l +ₗ 1) ↦ #w ∗
((l +ₗ 1) ↦ #(w + 1) ={⊤∖↑N,⊤}=∗ P ∗ weak_tok γ) ∧ ((l +ₗ 1) ↦ #(w + 1) ={⊤∖↑N,⊤}=∗ P ∗ weak_tok γ) ∧
((l +ₗ 1) ↦ #w ={⊤∖↑N,⊤}=∗ P)))%I as "#Hproto". ((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]". iMod ("Hacc" with "HP") as "[Hown Hclose2]".
iDestruct (weak_tok_auth_val with "H● Hown") as %(st' & weak & -> & Hval). iDestruct (weak_tok_auth_val with "H● Hown") as %(st' & weak & -> & Hval).
iMod ("Hclose2" with "Hown") as "HP". iMod ("Hclose2" with "Hown") as "HP".
...@@ -393,28 +391,27 @@ Section arc. ...@@ -393,28 +391,27 @@ Section arc.
{{{ P }}} upgrade [ #l] {{{ P }}} upgrade [ #l]
{{{ (b : bool) q, RET #b; P ∗ if b then arc_tok γ q ∗ P1 q else True }}}. {{{ (b : bool) q, RET #b; P ∗ if b then arc_tok γ q ∗ P1 q else True }}}.
Proof using HP1. 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 ∗ iAssert (□ (P ={⊤,∅}=∗ ∃ s : Z, l ↦ #s ∗
(⌜s ≠ 0⌝ -∗ l ↦ #(s + 1) ={∅,⊤}=∗ ∃ q, P ∗ arc_tok γ q ∗ ▷ P1 q) ∧ (⌜s ≠ 0⌝ -∗ l ↦ #(s + 1) ={∅,⊤}=∗ ∃ q, P ∗ arc_tok γ q ∗ ▷ P1 q) ∧
(l ↦ #s ={∅,⊤}=∗ P)))%I as "#Hproto". (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]". iMod ("Hacc" with "HP") as "[Hown Hclose2]".
iDestruct (weak_tok_auth_val with "H● Hown") as %(st' & weak & -> & Hval). 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. - iDestruct "H" as (q) "(>Heq & [HP1 HP1'] & >$ & ?)". iDestruct "Heq" as %Heq.
iIntros "!>"; iSplit; iMod ("Hclose2" with "Hown") as "HP". iIntros "!>"; iSplit; iMod ("Hclose2" with "Hown") as "HP".
+ iIntros "_ Hl". iExists (q/2)%Qp. iMod (own_update with "H●") as "[H● $]". + iIntros "_ Hl". iExists (q/2)%Qp. iMod (own_update with "H●") as "[H● $]".
{ apply auth_update_alloc. rewrite -[(_,0%nat)]right_id. { apply auth_update_alloc. rewrite -[(_,0%nat)]right_id.
apply op_local_update_discrete=>Hv. constructor; last done. apply op_local_update_discrete=>Hv. constructor; last done.
split; last by rewrite /= left_id; apply Hv. split=>[|//]. split; last by rewrite /= left_id; apply Hv. split=>[|//].
apply frac_valid'. rewrite -Heq comm_L -{2}(Qp_div_2 q). apply frac_valid. rewrite /= -Heq comm_L.
apply Qcplus_le_mono_l. rewrite -{1}(Qcplus_0_l (_ / _)%Qp). by apply Qp.add_le_mono_l, Qp.div_le. }
apply Qcplus_le_mono_r, Qp_ge_0. } iFrame. iApply "Hclose1". iExists _. iFrame.
iFrame. iApply "Hclose1". iExists _. iFrame. iExists _. iFrame. rewrite /= [xH ⋅ _]comm_L frac_op [(_ + q')%Qp]comm -[(_ + _)%Qp]assoc
rewrite /= [xH ⋅ _]comm_L frac_op' [(_ + c)%Qp]comm -[(_ + _)%Qp]assoc Qp.div_2 left_id_L. auto with iFrame.
Qp_div_2 left_id_L. auto with iFrame.
+ iIntros "Hl". iFrame. iApply ("Hclose1" with "[-]"). iExists _. 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. - iDestruct "H" as "[>$ ?]". iIntros "!>"; iSplit; first by auto with congruence.
iIntros "Hl". iMod ("Hclose2" with "Hown") as "$". iApply "Hclose1". iIntros "Hl". iMod ("Hclose2" with "Hown") as "$". iApply "Hclose1".
iExists _. auto with iFrame. iExists _. auto with iFrame.
...@@ -440,12 +437,12 @@ Section arc. ...@@ -440,12 +437,12 @@ Section arc.
{{{ weak_tok γ }}} drop_weak [ #l] {{{ weak_tok γ }}} drop_weak [ #l]
{{{ (b : bool), RET #b ; if b then P2 ∗ l ↦ #0 ∗ (l +ₗ 1) ↦ #0 else True }}}. {{{ (b : bool), RET #b ; if b then P2 ∗ l ↦ #0 ∗ (l +ₗ 1) ↦ #0 else True }}}.
Proof. 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 ∗ iAssert (□ (weak_tok γ ={⊤,⊤ ∖ ↑N}=∗ ∃ w : Z, (l +ₗ 1) ↦ #w ∗
((l +ₗ 1) ↦ #(w - 1) ={⊤ ∖ ↑N,⊤}=∗ ⌜w ≠ 1⌝ ∨ ((l +ₗ 1) ↦ #(w - 1) ={⊤ ∖ ↑N,⊤}=∗ ⌜w ≠ 1⌝ ∨
▷ P2 ∗ l ↦ #0 ∗ (l +ₗ 1) ↦ #0) ∧ ▷ P2 ∗ l ↦ #0 ∗ (l +ₗ 1) ↦ #0) ∧
((l +ₗ 1) ↦ #w ={⊤ ∖ ↑N,⊤}=∗ weak_tok γ)))%I as "#Hproto". ((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). iDestruct (weak_tok_auth_val with "H● Hown") as %(st' & weak & -> & Hval).
destruct st' as [[[[??][?|]]| |]|]; try done; [|iExists _..]. destruct st' as [[[[??][?|]]| |]|]; try done; [|iExists _..].
- by iDestruct "H" as (?) "(_ & _ & _ & _ & >%)". - by iDestruct "H" as (?) "(_ & _ & _ & _ & >%)".
...@@ -492,7 +489,7 @@ Section arc. ...@@ -492,7 +489,7 @@ Section arc.
Proof. Proof.
iIntros "INV H◯ HP2". iInv N as ([st ?]) "[>H● H]" "Hclose". iIntros "INV H◯ HP2". iInv N as ([st ?]) "[>H● H]" "Hclose".
iDestruct (own_valid_2 with "H● H◯") 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]); simpl in Hincl. destruct Hincl as (?&?&[=<-]&->&[?|[]%exclusive_included]);
try done; try apply _. setoid_subst. try done; try apply _. setoid_subst.
iMod (own_update_2 with "H● H◯") as "[H● $]". iMod (own_update_2 with "H● H◯") as "[H● $]".
...@@ -506,7 +503,7 @@ Section arc. ...@@ -506,7 +503,7 @@ Section arc.
{{{ arc_tok γ q ∗ P1 q }}} drop_arc [ #l] {{{ arc_tok γ q ∗ P1 q }}} drop_arc [ #l]
{{{ (b : bool), RET #b ; if b then P1 1 ∗ (P2 ={⊤}=∗ weak_tok γ) else True }}}. {{{ (b : bool), RET #b ; if b then P1 1 ∗ (P2 ={⊤}=∗ weak_tok γ) else True }}}.
Proof using HP1. 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". wp_rec. wp_bind (!ˢᶜ_)%E. iInv N as (st) "[>H● H]" "Hclose".
iDestruct (arc_tok_auth_val with "H● Hown") as %(?& s &?&?&[-> _]). iDestruct (arc_tok_auth_val with "H● Hown") as %(?& s &?&?&[-> _]).
iDestruct "H" as (x') "(? & ? & ? & ?)". wp_read. iDestruct "H" as (x') "(? & ? & ? & ?)". wp_read.
...@@ -520,18 +517,20 @@ Section arc. ...@@ -520,18 +517,20 @@ Section arc.
+ destruct Hqq' as [<- ->]. + destruct Hqq' as [<- ->].
iMod (own_update_2 with "H● Hown") as "[H● H◯]". iMod (own_update_2 with "H● Hown") as "[H● H◯]".
{ apply auth_update, prod_local_update_1. rewrite -[x in (x, _)]right_id. { 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 ())))). } by apply (op_local_update _ _ (Some (Cinr (Excl ())))). }
iMod ("Hclose" with "[H● Hs Hw]") as "_"; first by iExists _; do 2 iFrame. iMod ("Hclose" with "[H● Hs Hw]") as "_"; first by iExists _; do 2 iFrame.
iModIntro. wp_case. iApply wp_fupd. wp_op. 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 [? ->]. + destruct Hqq' as [? ->].
rewrite -[in (_, _)](Pos.succ_pred s) // -[wl in Cinl (_, wl)]left_id 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●". iMod (own_update_2 _ _ _ _ with "H● Hown") as "H●".
{ apply auth_update_dealloc, prod_local_update_1, @cancel_local_update_unit, _. } { apply auth_update_dealloc, prod_local_update_1, @cancel_local_update_unit, _. }
iMod ("Hclose" with "[- HΦ]") as "_". 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, _. } iIntros "!> !%". rewrite assoc -Hq''. f_equal. apply comm, _. }
iModIntro. wp_case. wp_op; case_bool_decide; simplify_eq. by iApply "HΦ". iModIntro. wp_case. wp_op; case_bool_decide; simplify_eq. by iApply "HΦ".
- wp_apply (wp_cas_int_fail with "Hs"); [congruence|]. iIntros "Hs". - wp_apply (wp_cas_int_fail with "Hs"); [congruence|]. iIntros "Hs".
...@@ -546,17 +545,18 @@ Section arc. ...@@ -546,17 +545,18 @@ Section arc.
{{{ (b : bool), RET #b ; {{{ (b : bool), RET #b ;
if b then P1 1 ∗ (P2 ={⊤}=∗ weak_tok γ) else arc_tok γ q ∗ P1 q }}}. if b then P1 1 ∗ (P2 ={⊤}=∗ weak_tok γ) else arc_tok γ q ∗ P1 q }}}.
Proof using HP1. 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 (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''. iDestruct "H" as (q'') "(>Hq'' & HP1' & Hs & Hw)". iDestruct "Hq''" as %Hq''.
destruct (decide (s = xH)) as [->|?]. destruct (decide (s = xH)) as [->|?].
- wp_apply (wp_cas_int_suc with "Hs"). iIntros "Hs". - wp_apply (wp_cas_int_suc with "Hs"). iIntros "Hs".
destruct Hqq' as [<- ->]. iMod (own_update_2 with "H● Hown") as "[H● H◯]". 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. { 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 ())))). } by apply (op_local_update _ _ (Some (Cinr (Excl ())))). }
iMod ("Hclose" with "[H● Hs Hw]") as "_"; first by iExists _; do 2 iFrame. 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". - wp_apply (wp_cas_int_fail with "Hs"); [congruence|]. iIntros "Hs".
iMod ("Hclose" with "[-Hown HP1 HΦ]") as "_"; first by iExists _; auto with iFrame. iMod ("Hclose" with "[-Hown HP1 HΦ]") as "_"; first by iExists _; auto with iFrame.
iApply ("HΦ" $! false). by iFrame. iApply ("HΦ" $! false). by iFrame.
...@@ -569,7 +569,7 @@ Section arc. ...@@ -569,7 +569,7 @@ Section arc.
if b then l ↦ #1 ∗ (l +ₗ 1) ↦ #1 ∗ P1 1 if b then l ↦ #1 ∗ (l +ₗ 1) ↦ #1 ∗ P1 1
else arc_tok γ q ∗ P1 q }}}. else arc_tok γ q ∗ P1 q }}}.
Proof using HP1. 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". iInv N as (st) "[>H● H]" "Hclose".
iDestruct (arc_tok_auth_val with "H● Hown") as %(? & ? & wl & w &[-> _]). iDestruct (arc_tok_auth_val with "H● Hown") as %(? & ? & wl & w &[-> _]).
iDestruct "H" as (?) "(>Hq'' & HP1' & >Hs & >Hw)". iDestruct "H" as (?) "(>Hq'' & HP1' & >Hs & >Hw)".
...@@ -588,8 +588,8 @@ Section arc. ...@@ -588,8 +588,8 @@ Section arc.
(alloc_option_local_update (Excl ())). } (alloc_option_local_update (Excl ())). }
iMod ("Hclose" with "[-HΦ HP1 H◯]") as "_"; first by iExists _; eauto with iFrame. 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". iModIntro. wp_case. wp_bind (!ˢᶜ_)%E. iInv N as ([st ?]) "[>H● H]" "Hclose".
iDestruct (own_valid_2 with "H● H◯") as iCombine "H● H◯" gives
%[[[[=]|Hincl]%option_included _]%prod_included [? _]]%auth_both_valid. %[[[[=]|Hincl]%option_included _]%prod_included [? _]]%auth_both_valid_discrete.
simpl in Hincl. destruct Hincl as (? & ? & [=<-] & -> & [|Hincl]); last first. simpl in Hincl. destruct Hincl as (? & ? & [=<-] & -> & [|Hincl]); last first.
+ apply csum_included in Hincl. destruct Hincl as [->|[Hincl|(?&?&[=]&?)]]=>//. + apply csum_included in Hincl. destruct Hincl as [->|[Hincl|(?&?&[=]&?)]]=>//.
destruct Hincl as (?&[[??]?]&[=<-]&->&[[_ Hlt]%prod_included _]%prod_included). destruct Hincl as (?&[[??]?]&[=<-]&->&[[_ Hlt]%prod_included _]%prod_included).
...@@ -598,9 +598,9 @@ Section arc. ...@@ -598,9 +598,9 @@ Section arc.
iMod ("Hclose" with "[-HΦ H◯ HP1]") as "_"; first by iExists _; auto with iFrame. 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. iModIntro. wp_let. wp_op; case_bool_decide; [lia|]. wp_let. wp_op. wp_bind (_ <-ˢᶜ _)%E.
iInv N as ([st w]) "[>H● H]" "Hclose". iInv N as ([st w]) "[>H● H]" "Hclose".
iDestruct (own_valid_2 with "H● H◯") as iCombine "H● H◯" gives
%[[[[=]|Hincl]%option_included _]%prod_included [Hval _]]%auth_both_valid. %[[[[=]|Hincl]%option_included _]%prod_included [Hval _]]%auth_both_valid_discrete.
simpl in Hincl. destruct Hincl as (? & ? & [=<-] & -> & Hincl); last first. simpl in Hincl. destruct Hincl as (x1 & x2 & [=<-] & -> & Hincl); last first.
assert (∃ q p, x2 = Cinl (q, p, Excl' ())) as (? & ? & ->). assert (∃ q p, x2 = Cinl (q, p, Excl' ())) as (? & ? & ->).
{ destruct Hincl as [|Hincl]; first by setoid_subst; eauto. { destruct Hincl as [|Hincl]; first by setoid_subst; eauto.
apply csum_included in Hincl. destruct Hincl as [->|[Hincl|(?&?&[=]&?)]]=>//. apply csum_included in Hincl. destruct Hincl as [->|[Hincl|(?&?&[=]&?)]]=>//.
...@@ -613,13 +613,13 @@ Section arc. ...@@ -613,13 +613,13 @@ Section arc.
csum_local_update_l, prod_local_update_2, delete_option_local_update, _. } csum_local_update_l, prod_local_update_2, delete_option_local_update, _. }
iMod ("Hclose" with "[-HΦ H◯ HP1]") as "_"; first by iExists _; auto with iFrame. iMod ("Hclose" with "[-HΦ H◯ HP1]") as "_"; first by iExists _; auto with iFrame.
iModIntro. wp_seq. iApply "HΦ". 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●". iMod (own_update_2 with "H● H◯") as "H●".
{ apply auth_update_dealloc. rewrite -{1}[(_, 0%nat)]right_id. { apply auth_update_dealloc. rewrite -{1}[(_, 0%nat)]right_id.
apply cancel_local_update_unit, _. } apply cancel_local_update_unit, _. }
iMod ("Hclose" with "[H●]") as "_"; first by iExists _; iFrame. iMod ("Hclose" with "[H●]") as "_"; first by iExists _; iFrame.
iModIntro. wp_seq. wp_op. wp_let. wp_op. wp_write. iApply "HΦ". 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. Qed.
Lemma try_unwrap_full_spec (γ : gname) (q: Qp) (l : loc) : Lemma try_unwrap_full_spec (γ : gname) (q: Qp) (l : loc) :
...@@ -636,7 +636,7 @@ Section arc. ...@@ -636,7 +636,7 @@ Section arc.
| _ (* 2 *) => arc_tok γ q ∗ P1 q | _ (* 2 *) => arc_tok γ q ∗ P1 q
end }}}. end }}}.
Proof using HP1. 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". iInv N as (st) "[>H● H]" "Hclose".
iDestruct (arc_tok_auth_val with "H● Hown") as %(q' & s & wl & w &[-> Hqq']). 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''. iDestruct "H" as (q'') "(>Hq'' & HP1' & Hs & Hw)". iDestruct "Hq''" as %Hq''.
...@@ -644,14 +644,14 @@ Section arc. ...@@ -644,14 +644,14 @@ Section arc.
- wp_apply (wp_cas_int_suc with "Hs")=>//. iIntros "Hs". - wp_apply (wp_cas_int_suc with "Hs")=>//. iIntros "Hs".
destruct Hqq' as [<- ->]. iMod (own_update_2 with "H● Hown") as "[H● H◯]". 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. { 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 ())))). } by apply (op_local_update _ _ (Some (Cinr (Excl ())))). }
iCombine "HP1" "HP1'" as "HP1". rewrite Hq''. clear Hq'' q''. iCombine "HP1" "HP1'" as "HP1". rewrite Hq''. clear Hq'' q''.
iMod ("Hclose" with "[H● Hs Hw]") as "_"; first by iExists _; do 2 iFrame. iMod ("Hclose" with "[H● Hs Hw]") as "_"; first by iExists _; do 2 iFrame.
clear w. iModIntro. wp_case. wp_op. wp_bind (!ˢᶜ_)%E. clear w. iModIntro. wp_case. wp_op. wp_bind (!ˢᶜ_)%E.
iInv N as ([st w']) "[>H● H]" "Hclose". iInv N as ([st w']) "[>H● H]" "Hclose".
iDestruct (own_valid_2 with "H● H◯") 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]); simpl in Hincl. destruct Hincl as (?&?&[=<-]&->&[?|[]%exclusive_included]);
[|by apply _|done]. setoid_subst. iDestruct "H" as "[Hl Hl1]". [|by apply _|done]. setoid_subst. iDestruct "H" as "[Hl Hl1]".
wp_read. destruct w'. wp_read. destruct w'.
...@@ -669,4 +669,4 @@ Section arc. ...@@ -669,4 +669,4 @@ Section arc.
Qed. Qed.
End arc. 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.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,7 +36,7 @@ Section proof. ...@@ -34,7 +36,7 @@ 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.
- iModIntro; iSplit; iIntros; by iApply "HR". - iModIntro; iSplit; iIntros; by iApply "HR".
Qed. Qed.
...@@ -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 :
......
theories/lang/lib/spawn.v → lambda-rust/lang/lib/spawn.v
View file @ 0f4ebd6d
From iris.program_logic Require Import weakestpre. From iris.program_logic Require Import weakestpre.
From iris.base_logic.lib Require Import invariants. From iris.base_logic.lib Require Import invariants.
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 proofmode notation. From lrust.lang Require Import proofmode notation.
From lrust.lang Require Export lang. From lrust.lang Require Export lang.
Set Default Proof Using "Type". From iris.prelude Require Import options.
Definition spawn : val := Definition spawn : val :=
λ: ["f"], λ: ["f"],
...@@ -28,15 +28,15 @@ Definition join : val := ...@@ -28,15 +28,15 @@ Definition join : val :=
"join" ["c"]. "join" ["c"].
(** The CMRA & functor we need. *) (** The CMRA & functor we need. *)
Class spawnG Σ := SpawnG { spawn_tokG :> inG Σ (exclR unitO) }. Class spawnG Σ := SpawnG { spawn_tokG :: inG Σ (exclR unitO) }.
Definition spawnΣ : gFunctors := #[GFunctor (exclR unitO)]. Definition spawnΣ : gFunctors := #[GFunctor (exclR unitO)].
Instance subG_spawnΣ {Σ} : subG spawnΣ Σ → spawnG Σ. Global Instance subG_spawnΣ {Σ} : subG spawnΣ Σ → spawnG Σ.
Proof. solve_inG. Qed. Proof. solve_inG. Qed.
(** Now we come to the Iris part of the proof. *) (** Now we come to the Iris part of the proof. *)
Section proof. Section proof.
Context `{!lrustG Σ, !spawnG Σ} (N : namespace). Context `{!lrustGS Σ, !spawnG Σ} (N : namespace).
Definition spawn_inv (γf γj : gname) (c : loc) (Ψ : val → iProp Σ) : iProp Σ := Definition spawn_inv (γf γj : gname) (c : loc) (Ψ : val → iProp Σ) : iProp Σ :=
(own γf (Excl ()) ∗ own γj (Excl ()) ∨ (own γf (Excl ()) ∗ own γj (Excl ()) ∨
...@@ -70,7 +70,7 @@ Proof. ...@@ -70,7 +70,7 @@ Proof.
wp_let. wp_alloc l as "Hl" "H†". wp_let. wp_let. wp_alloc l as "Hl" "H†". wp_let.
iMod (own_alloc (Excl ())) as (γf) "Hγf"; first done. iMod (own_alloc (Excl ())) as (γf) "Hγf"; first done.
iMod (own_alloc (Excl ())) as (γj) "Hγj"; first done. iMod (own_alloc (Excl ())) as (γj) "Hγj"; first done.
rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton. rewrite heap_pointsto_vec_cons heap_pointsto_vec_singleton.
iDestruct "Hl" as "[Hc Hd]". wp_write. iDestruct "Hl" as "[Hc Hd]". wp_write.
iMod (inv_alloc N _ (spawn_inv γf γj l Ψ) with "[Hc]") as "#?". iMod (inv_alloc N _ (spawn_inv γf γj l Ψ) with "[Hc]") as "#?".
{ iNext. iRight. iExists false. auto. } { iNext. iRight. iExists false. auto. }
...@@ -90,7 +90,7 @@ Proof. ...@@ -90,7 +90,7 @@ Proof.
auto. } auto. }
iDestruct "Hinv" as (b) "[>Hc _]". wp_write. iDestruct "Hinv" as (b) "[>Hc _]". wp_write.
iMod ("Hclose" with "[-HΦ]"). iMod ("Hclose" with "[-HΦ]").
- iNext. iRight. iExists true. iFrame. iExists _. iFrame. - iNext. iRight. iExists true. iFrame.
- iModIntro. wp_seq. by iApply "HΦ". - iModIntro. wp_seq. by iApply "HΦ".
Qed. Qed.
...@@ -111,7 +111,7 @@ Proof. ...@@ -111,7 +111,7 @@ Proof.
{ iNext. iLeft. iFrame. } { iNext. iLeft. iFrame. }
iModIntro. wp_if. wp_op. wp_read. wp_let. iModIntro. wp_if. wp_op. wp_read. wp_let.
iAssert (c ↦∗ [ #true; v])%I with "[Hc Hd]" as "Hc". iAssert (c ↦∗ [ #true; v])%I with "[Hc Hd]" as "Hc".
{ rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton. iFrame. } { rewrite heap_pointsto_vec_cons heap_pointsto_vec_singleton. iFrame. }
wp_free; first done. iApply "HΦ". iApply "HΨ'". done. wp_free; first done. iApply "HΦ". iApply "HΨ'". done.
Qed. Qed.
...@@ -119,10 +119,10 @@ Lemma join_handle_impl (Ψ1 Ψ2 : val → iProp Σ) c : ...@@ -119,10 +119,10 @@ Lemma join_handle_impl (Ψ1 Ψ2 : val → iProp Σ) c :
□ (∀ v, Ψ1 v -∗ Ψ2 v) -∗ join_handle c Ψ1 -∗ join_handle c Ψ2. □ (∀ v, Ψ1 v -∗ Ψ2 v) -∗ join_handle c Ψ1 -∗ join_handle c Ψ2.
Proof. Proof.
iIntros "#HΨ Hhdl". iDestruct "Hhdl" as (γf γj Ψ') "(Hj & H† & #? & #HΨ')". iIntros "#HΨ Hhdl". iDestruct "Hhdl" as (γf γj Ψ') "(Hj & H† & #? & #HΨ')".
iExists γf, γj, Ψ'. iFrame "#∗". iIntros "!# * ?". iExists γf, γj, Ψ'. iFrame "#∗". iIntros "!> * ?".
iApply "HΨ". iApply "HΨ'". done. iApply "HΨ". iApply "HΨ'". done.
Qed. Qed.
End proof. End proof.
Typeclasses Opaque finish_handle join_handle. Global Typeclasses Opaque finish_handle join_handle.
theories/lang/lib/swap.v → lambda-rust/lang/lib/swap.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 swap : val := Definition swap : val :=
rec: "swap" ["p1";"p2";"len"] := rec: "swap" ["p1";"p2";"len"] :=
...@@ -10,7 +10,7 @@ Definition swap : val := ...@@ -10,7 +10,7 @@ Definition swap : val :=
"p2" <- "x";; "p2" <- "x";;
"swap" ["p1" +ₗ #1 ; "p2" +ₗ #1 ; "len" - #1]. "swap" ["p1" +ₗ #1 ; "p2" +ₗ #1 ; "len" - #1].
Lemma wp_swap `{!lrustG Σ} E l1 l2 vl1 vl2 (n : Z): Lemma wp_swap `{!lrustGS Σ} E l1 l2 vl1 vl2 (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 ↦∗ vl2 }}} {{{ l1 ↦∗ vl1 ∗ l2 ↦∗ vl2 }}}
swap [ #l1; #l2; #n] @ E swap [ #l1; #l2; #n] @ E
...@@ -22,7 +22,7 @@ Proof. ...@@ -22,7 +22,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_let; wp_read; do 2 wp_write. do 3 wp_op. wp_read; wp_let; wp_read; do 2 wp_write. do 3 wp_op.
......
theories/lang/lib/tests.v → lambda-rust/lang/lib/tests.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 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.
Section tests. Section tests.
Context `{!lrustG Σ}. Context `{!lrustGS Σ}.
Lemma test_location_cmp E (l1 l2 : loc) q1 q2 v1 v2 : Lemma test_location_cmp E (l1 l2 : loc) q1 q2 v1 v2 :
{{{ ▷ l1 ↦{q1} v1 ∗ ▷ l2 ↦{q2} v2 }}} {{{ ▷ l1 ↦{q1} v1 ∗ ▷ l2 ↦{q2} v2 }}}
......