Commit bb851ce8 authored by George Pîrlea's avatar George Pîrlea

Merge branch 'master' into gpirlea/pinning

This branch is in a badly broken state. Even before the
merge, the build did no go through, as we did not finish
propagating the change to places in the semantic type
system to all files.

Nonetheless, the changes from master have now been merged,
with the exception of the following files:

theories/typing/lib/cell.v
theories/typing/soundness.v

(which require fixing other files before they can be compiled)

For these two files, the merge conflict has been commented out
and left in the file.
parents aa93b381 c36ae2bd
*.v gitlab-language=coq
*.vo
*.vio
*.v.d
*.vos
*.vok
.coqdeps.d
.Makefile.coq.d
*.glob
*.cache
*.aux
......@@ -10,7 +13,7 @@
*~
*.bak
.coq-native/
build-dep/
builddep/
Makefile.coq
Makefile.coq.conf
_opam
......@@ -16,10 +16,10 @@ variables:
cache:
key: "$CI_JOB_NAME"
paths:
- opamroot/
- _opam/
only:
- master
- /^ci/
- /^master/@iris/lambda-rust
- /^ci/@iris/lambda-rust
except:
- triggers
- schedules
......@@ -27,30 +27,25 @@ variables:
## Build jobs
# We are in Coq's benchmark suite, so better make sure we keep working with Coq master.
build-coq.dev:
<<: *template
variables:
OCAML: "ocaml-base-compiler.4.07.0"
OPAM_PINS: "coq version dev"
build-coq.8.9.0:
build-coq.8.12.0:
<<: *template
variables:
OPAM_PINS: "coq version 8.9.0"
OPAM_PKG: "coq-lambda-rust"
TIMING_CONF: "coq-8.9.0"
OPAM_PINS: "coq version 8.12.0"
OPAM_PKG: "1"
DENY_WARNINGS: "1"
tags:
- fp-timing
build-coq.8.8.2:
<<: *template
variables:
OPAM_PINS: "coq version 8.8.2"
build-iris.dev:
<<: *template
variables:
OPAM_PINS: "coq version 8.9.0 coq-stdpp.dev git git+https://gitlab.mpi-sws.org/iris/stdpp.git#$STDPP_REV coq-iris.dev git git+https://gitlab.mpi-sws.org/iris/iris.git#$IRIS_REV"
OPAM_PINS: "coq version 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"
except:
only:
- triggers
......
All files in this development are distributed under the terms of the BSD
license, included below.
------------------------------------------------------------------------------
Copyright: lambdaRust developers and contributors
BSD LICENCE
------------------------------------------------------------------------------
Redistribution and use in source and binary forms, with or without
modification, are permitted provided that the following conditions are met:
......@@ -12,18 +12,17 @@ modification, are permitted provided that the following conditions are met:
* Redistributions in binary form must reproduce the above copyright
notice, this list of conditions and the following disclaimer in the
documentation and/or other materials provided with the distribution.
* Neither the name of the <organization> nor the
names of its contributors may be used to endorse or promote products
derived from this software without specific prior written permission.
* Neither the name of the copyright holder nor the names of its contributors
may be used to endorse or promote products derived from this software
without specific prior written permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND
ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT HOLDER> BE LIABLE FOR ANY
DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR
ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON
ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
# Forward most targets to Coq makefile (with some trick to make this phony)
%: Makefile.coq phony
+@make -f Makefile.coq $@
# Default target
all: Makefile.coq
+@make -f Makefile.coq all
+@$(MAKE) -f Makefile.coq all
.PHONY: all
# Permit local customization
-include Makefile.local
# Forward most targets to Coq makefile (with some trick to make this phony)
%: Makefile.coq phony
@#echo "Forwarding $@"
+@$(MAKE) -f Makefile.coq $@
phony: ;
.PHONY: phony
clean: Makefile.coq
+@make -f Makefile.coq clean
find theories tests \( -name "*.d" -o -name "*.vo" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete || true
rm -f Makefile.coq
+@$(MAKE) -f Makefile.coq clean
@# Make sure not to enter the `_opam` folder.
find [a-z]*/ \( -name "*.d" -o -name "*.vo" -o -name "*.vo[sk]" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete || true
rm -f Makefile.coq .lia.cache builddep/*
.PHONY: clean
# Create Coq Makefile.
Makefile.coq: _CoqProject Makefile
"$(COQBIN)coq_makefile" -f _CoqProject -o Makefile.coq
"$(COQBIN)coq_makefile" -f _CoqProject -o Makefile.coq $(EXTRA_COQFILES)
# Install build-dependencies
build-dep/opam: opam Makefile
@echo "# Creating build-dep package."
@mkdir -p build-dep
@sed <opam -E 's/^(build|install|remove):.*/\1: []/; s/^name: *"(.*)" */name: "\1-builddep"/' >build-dep/opam
@fgrep builddep build-dep/opam >/dev/null || (echo "sed failed to fix the package name" && exit 1) # sanity check
build-dep: build-dep/opam phony
@# We want opam to not just instal the build-deps now, but to also keep satisfying these
OPAMFILES=$(wildcard *.opam)
BUILDDEPFILES=$(addsuffix -builddep.opam, $(addprefix builddep/,$(basename $(OPAMFILES))))
builddep/%-builddep.opam: %.opam Makefile
@echo "# Creating builddep package for $<."
@mkdir -p builddep
@sed <$< -E 's/^(build|install|remove):.*/\1: []/; s/"(.*)"(.*= *version.*)$$/"\1-builddep"\2/;' >$@
builddep-opamfiles: $(BUILDDEPFILES)
.PHONY: builddep-opamfiles
builddep: builddep-opamfiles
@# We want opam to not just install the build-deps now, but to also keep satisfying these
@# constraints. Otherwise, `opam upgrade` may well update some packages to versions
@# that are incompatible with our build requirements.
@# To achieve this, we create a fake opam package that has our build-dependencies as
@# dependencies, but does not actually install anything itself.
@echo "# Pinning build-dep package." && \
if opam --version | grep "^1\." -q; then \
BUILD_DEP_PACKAGE="$$(egrep "^name:" build-dep/opam | sed 's/^name: *"\(.*\)" */\1/')" && \
opam pin add -k path $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE".dev build-dep && \
opam reinstall $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE"; \
else \
opam install $(OPAMFLAGS) build-dep/; \
fi
# Some files that do *not* need to be forwarded to Makefile.coq
Makefile: ;
_CoqProject: ;
opam: ;
# Phony wildcard targets
phony: ;
.PHONY: phony
@echo "# Installing builddep packages."
@opam install $(OPAMFLAGS) $(BUILDDEPFILES)
.PHONY: builddep
# Backwards compatibility target
build-dep: builddep
.PHONY: build-dep
# Some files that do *not* need to be forwarded to Makefile.coq.
# ("::" lets Makefile.local overwrite this.)
Makefile Makefile.local _CoqProject $(OPAMFILES):: ;
......@@ -5,6 +5,8 @@ Missing APIs from the types we cover (APIs have been added after this formalizat
* Structural conversion for slices. The matching operations in our model would be
`&mut Cell<(A, B)>` -> `&mut (Cell<A>, Cell<B>)` and
`&Cell<(A, B)>` -> `&(Cell<A>, Cell<B>)` (both being NOPs).
* Turns out to be very hard! The way we currently associate NA-masks with locations is in conflict with this.
The invariant for the entire cell gets allocated "on" the first location of the cell, so when we do splitting the 2nd projection has no way to access it...
# ZST
......
......@@ -6,12 +6,12 @@ This is the Coq development accompanying lambda-Rust.
This version is known to compile with:
- Coq 8.8.2 / 8.9.0
- Coq 8.12.0
- A development version of [Iris](https://gitlab.mpi-sws.org/iris/iris)
## Building from source
When building from source, we recommend to use opam (1.2.2 or newer) for
When building from source, we recommend to use opam (2.0.0 or newer) for
installing the dependencies. This requires the following two repositories:
opam repo add coq-released https://coq.inria.fr/opam/released
......@@ -91,7 +91,7 @@ borrows" in the Coq development.
| F-endlft | programs.v | type_endlft |
| F-call | function.v | type_call' |
Some of these lemmas are called `something'` because the version without the `'` is a derived, more speicalized form used together with our eauto-based `solve_typing` tactic. You can see this tactic in action in the [examples](theories/typing/examples) subfolder.
Some of these lemmas are called `something'` because the version without the `'` is a derived, more specialized form used together with our eauto-based `solve_typing` tactic. You can see this tactic in action in the [examples](theories/typing/examples) subfolder.
### Lifetime Logic Rules
......
-Q theories lrust
# 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
# non-canonical projections (https://github.com/coq/coq/pull/10076) do not exist yet in 8.9.
# Cannot use non-canonical projections as it causes massive unification failures
# (https://github.com/coq/coq/issues/6294).
-arg -w -arg -redundant-canonical-projection
# change_no_check does not exist yet in 8.9.
-arg -w -arg -convert_concl_no_check
theories/lifetime/model/definitions.v
theories/lifetime/model/faking.v
......
opam-version: "1.2"
name: "coq-lambda-rust"
version: "dev"
opam-version: "2.0"
maintainer: "Ralf Jung <jung@mpi-sws.org>"
authors: "The RustBelt Team"
license: "BSD"
homepage: "http://plv.mpi-sws.org/rustbelt/"
homepage: "https://plv.mpi-sws.org/rustbelt/"
bug-reports: "https://gitlab.mpi-sws.org/iris/lambda-rust/issues"
dev-repo: "https://gitlab.mpi-sws.org/iris/lambda-rust.git"
build: [make "-j%{jobs}%"]
install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/lrust'" ]
dev-repo: "git+https://gitlab.mpi-sws.org/iris/lambda-rust.git"
synopsis: "LambdaRust Coq formalization"
description: """
A formal model of a Rust core language and type system, a logical relation for
the type system, and safety proof for some Rust libraries.
"""
depends: [
"coq-iris" { (= "dev.2019-07-14.1.0cdad2cb") | (= "dev") }
"coq-iris" { (= "dev.2020-12-10.1.872fe77b") | (= "dev") }
]
build: [make "-j%{jobs}%"]
install: [make "install"]
A formal model of a Rust core langauge and type system, a logical relation for
the type system, and safety proof for some Rust libraries.
From Coq Require Import Min.
From stdpp Require Import coPset.
From iris.algebra Require Import big_op gmap frac agree.
From iris.algebra Require Import big_op gmap frac agree numbers.
From iris.algebra Require Import csum excl auth cmra_big_op.
From iris.bi Require Import fractional.
From iris.base_logic Require Export lib.own.
......@@ -118,7 +118,7 @@ Section heap.
Global Instance heap_mapsto_fractional l v: Fractional (λ q, l {q} v)%I.
Proof.
intros p q.
by rewrite heap_mapsto_eq -own_op -auth_frag_op op_singleton pair_op agree_idemp.
by rewrite heap_mapsto_eq -own_op -auth_frag_op singleton_op -pair_op agree_idemp.
Qed.
Global Instance heap_mapsto_as_fractional l q v:
AsFractional (l {q} v) (λ q, l {q} v)%I q.
......@@ -143,7 +143,7 @@ Section heap.
Proof.
rewrite heap_mapsto_eq -own_op -auth_frag_op own_valid discrete_valid.
eapply pure_elim; [done|]=> /auth_frag_valid /=.
rewrite op_singleton pair_op singleton_valid=> -[? /agree_op_invL'->]; eauto.
rewrite singleton_op -pair_op singleton_valid=> -[? /to_agree_op_inv_L->]; eauto.
Qed.
Lemma heap_mapsto_vec_nil l q : l ↦∗{q} [] True.
......@@ -174,7 +174,7 @@ Section heap.
{ rewrite !heap_mapsto_vec_nil. iIntros "_"; auto. }
rewrite !heap_mapsto_vec_cons. iIntros "[[Hv1 Hvl1] [Hv2 Hvl2]]".
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 %<-.
iSplit; first done. iFrame.
- by iIntros "[% [$ Hl2]]"; subst.
......@@ -272,7 +272,7 @@ Section heap.
{q1}ln {q2}l+n n' {q1+q2}l(n+n').
Proof.
by rewrite heap_freeable_eq /heap_freeable_def -own_op -auth_frag_op
op_singleton pair_op inter_op.
singleton_op -pair_op inter_op.
Qed.
(** Properties about heap_freeable_rel and heap_freeable *)
......@@ -406,8 +406,8 @@ Section heap.
Proof.
iDestruct 1 as (hF) "(Hvalσ & HhF & REL)"; iDestruct "REL" as %REL.
iIntros "Hmt Hf". rewrite heap_freeable_eq /heap_freeable_def.
iDestruct (own_valid_2 with "HhF Hf") as % [Hl Hv]%auth_both_valid.
move: Hl=> /singleton_included [[q qs] [/leibniz_equiv_iff Hl Hq]].
iDestruct (own_valid_2 with "HhF Hf") as % [Hl Hv]%auth_both_valid_discrete.
move: Hl=> /singleton_included_l [[q qs] [/leibniz_equiv_iff Hl Hq]].
apply (Some_included_exclusive _ _) in Hq as [=<-<-]%leibniz_equiv; last first.
{ move: (Hv (l.1)). rewrite Hl. by intros [??]. }
assert (vl []).
......@@ -429,8 +429,8 @@ Section heap.
σ !! l = Some (match ls with RSt n => RSt (n+n') | WSt => WSt end, v).
Proof.
iIntros "H● H◯".
iDestruct (own_valid_2 with "H● H◯") as %[Hl?]%auth_both_valid.
iPureIntro. move: Hl=> /singleton_included [[[q' ls'] dv]].
iDestruct (own_valid_2 with "H● H◯") as %[Hl?]%auth_both_valid_discrete.
iPureIntro. move: Hl=> /singleton_included_l [[[q' ls'] dv]].
rewrite /to_heap lookup_fmap fmap_Some_equiv.
move=> [[[ls'' v'] [?[[/=??]->]]]]; simplify_eq.
move=> /Some_pair_included_total_2
......@@ -446,8 +446,8 @@ Section heap.
⌜σ !! l = Some (ls, v).
Proof.
iIntros "H● H◯".
iDestruct (own_valid_2 with "H● H◯") as %[Hl?]%auth_both_valid.
iPureIntro. move: Hl=> /singleton_included [[[q' ls'] dv]].
iDestruct (own_valid_2 with "H● H◯") as %[Hl?]%auth_both_valid_discrete.
iPureIntro. move: Hl=> /singleton_included_l [[[q' ls'] dv]].
rewrite /to_heap lookup_fmap fmap_Some_equiv.
move=> [[[ls'' v'] [?[[/=??]->]]] Hincl]; simplify_eq.
apply (Some_included_exclusive _ _) in Hincl as [? Hval]; last by destruct ls''.
......
......@@ -9,6 +9,7 @@ Open Scope Z_scope.
Definition block : Set := positive.
Definition loc : Set := block * Z.
Declare Scope loc_scope.
Bind Scope loc_scope with loc.
Delimit Scope loc_scope with L.
Open Scope loc_scope.
......@@ -430,13 +431,13 @@ Qed.
Definition fresh_block (σ : state) : block :=
let loclst : list loc := elements (dom _ σ : gset loc) in
let blockset : gset block := foldr (λ l, ({[l.1]} )) loclst in
let blockset : gset block := foldr (λ l, ({[l.1]} .)) loclst in
fresh blockset.
Lemma is_fresh_block σ i : σ !! (fresh_block σ,i) = None.
Proof.
assert ( (l : loc) ls (X : gset block),
l ls l.1 foldr (λ l, ({[l.1]} )) X ls) as help.
l ls l.1 foldr (λ l, ({[l.1]} .)) X ls) as help.
{ induction 1; set_solver. }
rewrite /fresh_block /shift_loc /= -(not_elem_of_dom (D := gset loc)) -elem_of_elements.
move=> /(help _ _ ) /=. apply is_fresh.
......
From Coq.QArith Require Import Qcanon.
From iris.base_logic.lib Require Import invariants.
From iris.program_logic Require Import weakestpre.
From iris.proofmode Require Import tactics.
From iris.bi Require Import fractional.
From iris.algebra Require Import excl csum frac auth.
From iris.algebra Require Import excl csum frac auth numbers.
From lrust.lang Require Import lang proofmode notation new_delete.
Set Default Proof Using "Type".
......@@ -189,7 +188,7 @@ Section arc.
iIntros "Hl1 Hl2 [HP1 HP1']".
iMod (own_alloc (( (Some $ Cinl ((1/2)%Qp, xH, None), O)
(Some $ Cinl ((1/2)%Qp, xH, None), O))))
as (γ) "[H● H◯]"; first by apply auth_both_valid.
as (γ) "[H● H◯]"; first by apply auth_both_valid_discrete.
iExists _, _. iFrame. iApply inv_alloc. iExists _. iFrame. iExists _. iFrame.
rewrite Qp_div_2. auto.
Qed.
......@@ -199,7 +198,7 @@ Section arc.
Proof.
iIntros "Hl1 Hl2 HP2".
iMod (own_alloc (( (None, 1%nat) (None, 1%nat)))) as (γ) "[H● H◯]";
first by apply auth_both_valid.
first by apply auth_both_valid_discrete.
iExists _. iFrame. iApply inv_alloc. iExists _. iFrame.
Qed.
......@@ -210,7 +209,7 @@ Section arc.
else q'', q' = (q + q'')%Qp.
Proof.
iIntros "H● Htok". iDestruct (own_valid_2 with "H● Htok") as
%[[Hincl%option_included _]%prod_included [Hval _]]%auth_both_valid.
%[[Hincl%option_included _]%prod_included [Hval _]]%auth_both_valid_discrete.
destruct st, Hincl as [[=]|(?&?&[= <-]&?&[Hincl|Hincl%csum_included])];
simpl in *; subst.
- setoid_subst. iExists _, _, _, _. by iSplit.
......@@ -268,25 +267,24 @@ Section arc.
iModIntro. wp_let. wp_op. wp_bind (CAS _ _ _). iInv N as (st) "[>H● H]" "Hclose1".
iMod ("Hacc" with "HP") as (?) "[Hown Hclose2]".
iDestruct (arc_tok_auth_val with "H● Hown") as %(?&strong'&?&?&[-> _]).
iDestruct "H" as (q) "(>#Hq & [HP1 HP1'] & Hl & Hw)". iDestruct "Hq" as %Hq.
iDestruct "H" as (qq) "(>#Hq & [HP1 HP1'] & Hl & Hw)". iDestruct "Hq" as %Hq.
destruct (decide (strong = strong')) as [->|?].
- wp_apply (wp_cas_int_suc with "Hl"). iIntros "Hl".
iMod (own_update with "H●") as "[H● Hown']".
{ apply auth_update_alloc, prod_local_update_1,
(op_local_update_discrete _ _ (Some (Cinl ((q/2)%Qp, 1%positive, None))))
(op_local_update_discrete _ _ (Some (Cinl ((qq/2)%Qp, 1%positive, None))))
=>-[/= Hqa ?]. split;[split|]=>//=; last by rewrite left_id.
apply frac_valid'. rewrite -Hq comm_L -{2}(Qp_div_2 q).
apply Qcplus_le_mono_l. rewrite -{1}(Qcplus_0_l (_ / _)%Qp).
apply Qcplus_le_mono_r, Qp_ge_0. }
apply frac_valid'. rewrite -Hq comm_L.
by apply Qp_add_le_mono_l, Qp_div_le. }
iMod ("Hclose2" with "Hown") as "HP". iModIntro.
iMod ("Hclose1" with "[Hl Hw H● HP1']") as "_".
{ iExists _. iFrame. iExists _. rewrite /= [xH _]comm_L. iFrame.
rewrite [(q / 2)%Qp _]comm frac_op' -[(_ + _)%Qp]assoc Qp_div_2 left_id_L. auto. }
rewrite [(qq / 2)%Qp _]comm frac_op' -[(_ + _)%Qp]assoc Qp_div_2 left_id_L. auto. }
iModIntro. wp_case. iApply "HΦ". iFrame.
- wp_apply (wp_cas_int_fail with "Hl"); [congruence|]. iIntros "Hl".
iMod ("Hclose2" with "Hown") as "HP". iModIntro.
iMod ("Hclose1" with "[-HP HΦ]") as "_".
{ iExists _. iFrame. iExists q. auto with iFrame. }
{ iExists _. iFrame. iExists qq. auto with iFrame. }
iModIntro. wp_case. iApply ("IH" with "HP HΦ").
Qed.
......@@ -309,7 +307,7 @@ Section arc.
iApply fupd_wp. iMod ("Hacc" with "HP") as (?) "[Hown Hclose2]".
iDestruct (arc_tok_auth_val with "H● Hown") as %(?&?& wlock & weak' &[-> _]).
iMod ("Hclose2" with "Hown") as "HP". iModIntro.
iDestruct "H" as (q) "(>Heq & HP1 & Hl & Hl1)". iDestruct "Heq" as %Heq.
iDestruct "H" as (qq) "(>Heq & HP1 & Hl & Hl1)". iDestruct "Heq" as %Heq.
destruct (decide (weak = weak' wlock = None)) as [[<- ->]|Hw].
- wp_apply (wp_cas_int_suc with "Hl1"). iIntros "Hl1".
iMod (own_update with "H●") as "[H● Hown']".
......@@ -337,7 +335,7 @@ Section arc.
Proof.
iIntros "H● Htok". iDestruct (own_valid_2 with "H● Htok") as
%[[Hincl%option_included Hincl'%nat_included]%prod_included [Hval _]]
%auth_both_valid.
%auth_both_valid_discrete.
destruct st as [?[]], Hincl as [_|(?&?&[=]&?)]; simpl in *; try lia. eauto.
Qed.
......@@ -407,9 +405,8 @@ Section arc.
{ apply auth_update_alloc. rewrite -[(_,0%nat)]right_id.
apply op_local_update_discrete=>Hv. constructor; last done.
split; last by rewrite /= left_id; apply Hv. split=>[|//].
apply frac_valid'. rewrite -Heq comm_L -{2}(Qp_div_2 q).
apply Qcplus_le_mono_l. rewrite -{1}(Qcplus_0_l (_ / _)%Qp).
apply Qcplus_le_mono_r, Qp_ge_0. }
apply frac_valid'. rewrite /= -Heq comm_L.
by apply Qp_add_le_mono_l, Qp_div_le. }
iFrame. iApply "Hclose1". iExists _. iFrame. iExists _. iFrame.
rewrite /= [xH _]comm_L frac_op' [(_ + c)%Qp]comm -[(_ + _)%Qp]assoc
Qp_div_2 left_id_L. auto with iFrame.
......@@ -492,7 +489,7 @@ Section arc.
Proof.
iIntros "INV H◯ HP2". iInv N as ([st ?]) "[>H● H]" "Hclose".
iDestruct (own_valid_2 with "H● H◯")
as %[[[[=]|Hincl]%option_included _]%prod_included [? _]]%auth_both_valid.
as %[[[[=]|Hincl]%option_included _]%prod_included [? _]]%auth_both_valid_discrete.
simpl in Hincl. destruct Hincl as (?&?&[=<-]&->&[?|[]%exclusive_included]);
try done; try apply _. setoid_subst.
iMod (own_update_2 with "H● H◯") as "[H● $]".
......@@ -509,7 +506,7 @@ Section arc.
iIntros "#INV !# * [Hown HP1] HΦ". iLöb as "IH".
wp_rec. wp_bind (!ˢᶜ_)%E. iInv N as (st) "[>H● H]" "Hclose".
iDestruct (arc_tok_auth_val with "H● Hown") as %(?& s &?&?&[-> _]).
iDestruct "H" as (?) "(? & ? & ? & ?)". wp_read.
iDestruct "H" as (x') "(? & ? & ? & ?)". wp_read.
iMod ("Hclose" with "[-Hown HP1 HΦ]") as "_". { iExists _. auto with iFrame. }
iModIntro. wp_let. wp_op. wp_bind (CAS _ _ _). iInv N as (st) "[>H● H]" "Hclose".
iDestruct (arc_tok_auth_val with "H● Hown") as %(q' & s' & wl & w &[-> Hqq']).
......@@ -520,14 +517,14 @@ Section arc.
+ destruct Hqq' as [<- ->].
iMod (own_update_2 with "H● Hown") as "[H● H◯]".
{ apply auth_update, prod_local_update_1. rewrite -[x in (x, _)]right_id.
etrans; first apply cancel_local_update_unit, _.
etrans; first apply: cancel_local_update_unit.
by apply (op_local_update _ _ (Some (Cinr (Excl ())))). }
iMod ("Hclose" with "[H● Hs Hw]") as "_"; first by iExists _; do 2 iFrame.
iModIntro. wp_case. iApply wp_fupd. wp_op.
iApply ("HΦ"). rewrite -{2}Hq''. iFrame. by iApply close_last_strong.
+ destruct Hqq' as [? ->].
rewrite -[in (_, _)](Pos.succ_pred s) // -[wl in Cinl (_, wl)]left_id
-Pos.add_1_l -2!pair_op -Cinl_op Some_op.
-Pos.add_1_l 2!pair_op Cinl_op Some_op.
iMod (own_update_2 _ _ _ _ with "H● Hown") as "H●".
{ apply auth_update_dealloc, prod_local_update_1, @cancel_local_update_unit, _. }
iMod ("Hclose" with "[- HΦ]") as "_".
......@@ -553,7 +550,7 @@ Section arc.
- wp_apply (wp_cas_int_suc with "Hs"). iIntros "Hs".
destruct Hqq' as [<- ->]. iMod (own_update_2 with "H● Hown") as "[H● H◯]".
{ apply auth_update, prod_local_update_1. rewrite -[x in (x, _)]right_id.
etrans; first apply cancel_local_update_unit, _.
etrans; first apply: cancel_local_update_unit.
by apply (op_local_update _ _ (Some (Cinr (Excl ())))). }
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.
......@@ -589,7 +586,7 @@ Section arc.
iMod ("Hclose" with "[-HΦ HP1 H◯]") as "_"; first by iExists _; eauto with iFrame.
iModIntro. wp_case. wp_bind (!ˢᶜ_)%E. iInv N as ([st ?]) "[>H● H]" "Hclose".
iDestruct (own_valid_2 with "H● H◯") as
%[[[[=]|Hincl]%option_included _]%prod_included [? _]]%auth_both_valid.
%[[[[=]|Hincl]%option_included _]%prod_included [? _]]%auth_both_valid_discrete.
simpl in Hincl. destruct Hincl as (? & ? & [=<-] & -> & [|Hincl]); last first.
+ apply csum_included in Hincl. destruct Hincl as [->|[Hincl|(?&?&[=]&?)]]=>//.
destruct Hincl as (?&[[??]?]&[=<-]&->&[[_ Hlt]%prod_included _]%prod_included).
......@@ -599,7 +596,7 @@ Section arc.
iModIntro. wp_let. wp_op; case_bool_decide; [lia|]. wp_let. wp_op. wp_bind (_ <-ˢᶜ _)%E.
iInv N as ([st w]) "[>H● H]" "Hclose".
iDestruct (own_valid_2 with "H● H◯") as
%[[[[=]|Hincl]%option_included _]%prod_included [Hval _]]%auth_both_valid.
%[[[[=]|Hincl]%option_included _]%prod_included [Hval _]]%auth_both_valid_discrete.
simpl in Hincl. destruct Hincl as (? & ? & [=<-] & -> & Hincl); last first.
assert ( q p, x2 = Cinl (q, p, Excl' ())) as (? & ? & ->).
{ destruct Hincl as [|Hincl]; first by setoid_subst; eauto.
......@@ -644,14 +641,14 @@ Section arc.
- wp_apply (wp_cas_int_suc with "Hs")=>//. iIntros "Hs".
destruct Hqq' as [<- ->]. iMod (own_update_2 with "H● Hown") as "[H● H◯]".
{ apply auth_update, prod_local_update_1. rewrite -[x in (x, _)]right_id.
etrans; first apply cancel_local_update_unit, _.
etrans; first apply: cancel_local_update_unit.
by apply (op_local_update _ _ (Some (Cinr (Excl ())))). }
iCombine "HP1" "HP1'" as "HP1". rewrite Hq''. clear Hq'' q''.
iMod ("Hclose" with "[H● Hs Hw]") as "_"; first by iExists _; do 2 iFrame.
clear w. iModIntro. wp_case. wp_op. wp_bind (!ˢᶜ_)%E.
iInv N as ([st w']) "[>H● H]" "Hclose".
iDestruct (own_valid_2 with "H● H◯")
as %[[[[=]|Hincl]%option_included _]%prod_included [? _]]%auth_both_valid.
as %[[[[=]|Hincl]%option_included _]%prod_included [? _]]%auth_both_valid_discrete.
simpl in Hincl. destruct Hincl as (?&?&[=<-]&->&[?|[]%exclusive_included]);
[|by apply _|done]. setoid_subst. iDestruct "H" as "[Hl Hl1]".
wp_read. destruct w'.
......
......@@ -23,6 +23,8 @@ Section proof.
Global Instance lock_proto_ne l : NonExpansive (lock_proto l).