Commit 1174a416 authored by Ralf Jung's avatar Ralf Jung
Browse files

delete Coq code; it moved to lambda-rust

parent 5f7402f6
Pipeline #44176 failed with stage
in 2 minutes and 32 seconds
# Forward most targets to Coq makefile (with some trick to make this phony)
%: Makefile.coq phony
+@make -f Makefile.coq $@
all: Makefile.coq
+@make -f Makefile.coq all
.PHONY: all
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 .lia.cache
.PHONY: clean
# Create Coq Makefile.
Makefile.coq: _CoqProject Makefile
"$(COQBIN)coq_makefile" -f _CoqProject -o Makefile.coq
# 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
@# constraints. Otherwise, `opam upgrade` may well update some packages to versions
@# that are incompatible with our build requirements.
@# To achieve this, we create a fake opam package that has our build-dependencies as
@# dependencies, but does not actually install anything itself.
@echo "# Installing build-dep package."
@opam install $(OPAMFLAGS) build-dep/
# Some files that do *not* need to be forwarded to Makefile.coq
Makefile: ;
_CoqProject: ;
opam: ;
# Phony wildcard targets
phony: ;
.PHONY: phony
......@@ -32,39 +32,13 @@ To run an example, use `cargo run --example branded_vec` from the [`ghostcell`]
# Coq proof
Our Coq proof is based on the [RustBelt formalization](https://gitlab.mpi-sws.org/iris/lambda-rust).
Our Coq proof is part of the [RustBelt formalization](https://gitlab.mpi-sws.org/iris/lambda-rust).
## Where to find the proofs
- The `BrandedVec` soundness proof (§4.3) is in [`theories/typing/lib/brandedvec.v`](theories/typing/lib/brandedvec.v).
- The `GhostCell` soundness proof (§4.4) is in [`theories/typing/lib/ghostcell.v`](theories/typing/lib/ghostcell.v).
- The new version of the "lifetime equalization" rule (§4.2) is `type_equivalize_lft` in [`theories/typing/programs.v`](theories/typing/programs.v).
The example that motivated the rule is [`theories/typing/examples/nonlexical.v`](theories/typing/examples/nonlexical.v).
## Prerequisites
This version is known to compile with:
- Coq 8.11.2
- A development version of [Iris](https://gitlab.mpi-sws.org/iris/iris) (see the [`opam`](opam) file for the exact version).
## Building from source
When building from source, we recommend to use opam (2.0.0 or newer) for
installing the dependencies. This requires the following two repositories:
opam repo add coq-released https://coq.inria.fr/opam/released
opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
Once you got opam set up, run `make build-dep` to install the right versions
of the dependencies.
Run `make -jN` to build the full development, where `N` is the number of your
CPU cores.
To update, do `git pull`. After an update, the development may fail to compile
because of outdated dependencies. To fix that, please run `opam update`
followed by `make build-dep`.
- The `BrandedVec` soundness proof (§4.3) is in [`theories/typing/lib/brandedvec.v`](https://gitlab.mpi-sws.org/iris/lambda-rust/-/tree/master/theories/typing/lib/brandedvec.v).
- The `GhostCell` soundness proof (§4.4) is in [`theories/typing/lib/ghostcell.v`](https://gitlab.mpi-sws.org/iris/lambda-rust/-/tree/master/theories/typing/lib/ghostcell.v).
- The new version of the "lifetime equalization" rule (§4.2) is `type_equivalize_lft` in [`theories/typing/programs.v`](https://gitlab.mpi-sws.org/iris/lambda-rust/-/tree/master/theories/typing/programs.v).
The example that motivated the rule is [`theories/typing/examples/nonlexical.v`](https://gitlab.mpi-sws.org/iris/lambda-rust/-/tree/master/theories/typing/examples/nonlexical.v).
[`ghostcell`]: ghostcell
-Q theories lrust
# We sometimes want to locally override notation (e.g. in proofmode/base.v, bi/embedding.v), 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.
-arg -w -arg -redundant-canonical-projection
# change_no_check does not exist yet in 8.9.
-arg -w -arg -convert_concl_no_check
# "Declare Scope" does not exist yet in 8.9.
-arg -w -arg -undeclared-scope
# We have ambiguous paths and so far it is not even clear what they are (https://gitlab.mpi-sws.org/iris/iris/issues/240).
-arg -w -arg -ambiguous-paths
theories/lifetime/model/definitions.v
theories/lifetime/model/faking.v
theories/lifetime/model/creation.v
theories/lifetime/model/primitive.v
theories/lifetime/model/accessors.v
theories/lifetime/model/borrow.v
theories/lifetime/model/borrow_sep.v
theories/lifetime/model/reborrow.v
theories/lifetime/lifetime_sig.v
theories/lifetime/lifetime.v
theories/lifetime/at_borrow.v
theories/lifetime/na_borrow.v
theories/lifetime/frac_borrow.v
theories/lang/adequacy.v
theories/lang/heap.v
theories/lang/lang.v
theories/lang/lifting.v
theories/lang/notation.v
theories/lang/proofmode.v
theories/lang/races.v
theories/lang/tactics.v
theories/lang/lib/memcpy.v
theories/lang/lib/swap.v
theories/lang/lib/new_delete.v
theories/lang/lib/spawn.v
theories/lang/lib/lock.v
theories/lang/lib/arc.v
theories/lang/lib/tests.v
theories/typing/base.v
theories/typing/type.v
theories/typing/util.v
theories/typing/lft_contexts.v
theories/typing/type_context.v
theories/typing/cont_context.v
theories/typing/uninit.v
theories/typing/own.v
theories/typing/uniq_bor.v
theories/typing/shr_bor.v
theories/typing/product.v
theories/typing/product_split.v
theories/typing/sum.v
theories/typing/bool.v
theories/typing/int.v
theories/typing/function.v
theories/typing/programs.v
theories/typing/borrow.v
theories/typing/cont.v
theories/typing/fixpoint.v
theories/typing/type_sum.v
theories/typing/typing.v
theories/typing/soundness.v
theories/typing/lib/panic.v
theories/typing/lib/option.v
theories/typing/lib/fake_shared.v
theories/typing/lib/cell.v
theories/typing/lib/spawn.v
theories/typing/lib/join.v
theories/typing/lib/diverging_static.v
theories/typing/lib/take_mut.v
theories/typing/lib/rc/rc.v
theories/typing/lib/rc/weak.v
theories/typing/lib/arc.v
theories/typing/lib/swap.v
theories/typing/lib/mutex/mutex.v
theories/typing/lib/mutex/mutexguard.v
theories/typing/lib/refcell/refcell.v
theories/typing/lib/refcell/ref.v
theories/typing/lib/refcell/refmut.v
theories/typing/lib/refcell/refcell_code.v
theories/typing/lib/refcell/ref_code.v
theories/typing/lib/refcell/refmut_code.v
theories/typing/lib/rwlock/rwlock.v
theories/typing/lib/rwlock/rwlockreadguard.v
theories/typing/lib/rwlock/rwlockwriteguard.v
theories/typing/lib/rwlock/rwlock_code.v
theories/typing/lib/rwlock/rwlockreadguard_code.v
theories/typing/lib/rwlock/rwlockwriteguard_code.v
theories/typing/lib/gsingleton.v
theories/typing/lib/brandedvec.v
theories/typing/lib/ghostcell.v
theories/typing/examples/get_x.v
theories/typing/examples/rebor.v
theories/typing/examples/unbox.v
theories/typing/examples/init_prod.v
theories/typing/examples/lazy_lft.v
theories/typing/examples/nonlexical.v
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.
opam-version: "2.0"
name: "coq-lambda-rust"
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.2020-02-14.2.a3cea59c") | (= "dev") }
]
build: [make "-j%{jobs}%"]
install: [make "install"]
From iris.program_logic Require Export adequacy weakestpre.
From iris.algebra Require Import auth.
From lrust.lang Require Export heap.
From lrust.lang Require Import proofmode notation.
Set Default Proof Using "Type".
Class lrustPreG Σ := HeapPreG {
lrust_preG_irig :> invPreG Σ;
lrust_preG_heap :> inG Σ (authR heapUR);
lrust_preG_heap_freeable :> inG Σ (authR heap_freeableUR)
}.
Definition lrustΣ : gFunctors :=
#[invΣ;
GFunctor (constRF (authR heapUR));
GFunctor (constRF (authR heap_freeableUR))].
Instance subG_heapPreG {Σ} : subG lrustΣ Σ lrustPreG Σ.
Proof. solve_inG. Qed.
Definition lrust_adequacy Σ `{!lrustPreG Σ} e σ φ :
( `{!lrustG Σ}, True WP e {{ v, ⌜φ v }})
adequate NotStuck e σ (λ v _, φ v).
Proof.
intros Hwp; eapply (wp_adequacy _ _); iIntros (??).
iMod (own_alloc ( to_heap σ)) as (vγ) "Hvγ".
{ apply (auth_auth_valid (to_heap _)), to_heap_valid. }
iMod (own_alloc ( ( : heap_freeableUR))) as (fγ) "Hfγ";
first by apply auth_auth_valid.
set (Hheap := HeapG _ _ _ vγ fγ).
iModIntro. iExists (λ σ _, heap_ctx σ), (λ _, True%I). iSplitL.
{ iExists . by iFrame. }
by iApply (Hwp (LRustG _ _ Hheap)).
Qed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
From iris.program_logic Require Import weakestpre.
From iris.proofmode Require Import tactics.
From iris.algebra Require Import excl.
From lrust.lang Require Import lang proofmode notation.
Set Default Proof Using "Type".
Definition mklock_unlocked : val := λ: ["l"], "l" <- #false.
Definition mklock_locked : val := λ: ["l"], "l" <- #true.
Definition try_acquire : val := λ: ["l"], CAS "l" #false #true.
Definition acquire : val :=
rec: "acquire" ["l"] := if: try_acquire ["l"] then # else "acquire" ["l"].
Definition release : val := λ: ["l"], "l" <-ˢᶜ #false.
(* It turns out that we need an accessor-based spec so that we can put the
protocol into shared borrows. Cancellable invariants don't work because
their cancelling view shift has a non-empty mask, and it would have to be
executed in the consequence view shift of a borrow. *)
Section proof.
Context `{!lrustG Σ}.
Definition lock_proto (l : loc) (R : iProp Σ) : iProp Σ :=
( b : bool, l #b if b then True else R)%I.
Global Instance lock_proto_ne l : NonExpansive (lock_proto l).
Proof. solve_proper. Qed.
Lemma lock_proto_iff l R R' :
(R R') - lock_proto l R - lock_proto l R'.
Proof.
iIntros "#HRR' Hlck". iDestruct "Hlck" as (b) "[Hl HR]". iExists b.
iFrame "Hl". destruct b; first done. by iApply "HRR'".
Qed.
Lemma lock_proto_iff_proper l R R' :
(R R') - (lock_proto l R lock_proto l R').
Proof.
iIntros "#HR !#". iSplit; iIntros "Hlck"; iApply (lock_proto_iff with "[HR] Hlck").
- done.
- iAlways; iSplit; iIntros; by iApply "HR".
Qed.
(** The main proofs. *)
Lemma lock_proto_create (R : iProp Σ) l (b : bool) :
l #b - (if b then True else R) == lock_proto l R.
Proof.
iIntros "Hl HR". iExists _. iFrame "Hl". destruct b; first done. by iFrame.
Qed.
Lemma lock_proto_destroy l R :
lock_proto l R - (b : bool), l #b if b then True else R.
Proof.
iIntros "Hlck". iDestruct "Hlck" as (b) "[Hl HR]". auto with iFrame.
Qed.
Lemma mklock_unlocked_spec (R : iProp Σ) (l : loc) v :
{{{ l v R }}} mklock_unlocked [ #l ] {{{ RET #; lock_proto l R }}}.
Proof.
iIntros (Φ) "[Hl HR] HΦ". wp_lam. rewrite -wp_fupd. wp_write.
iMod (lock_proto_create with "Hl HR") as "Hproto".
iApply "HΦ". by iFrame.
Qed.
Lemma mklock_locked_spec (R : iProp Σ) (l : loc) v :
{{{ l v }}} mklock_locked [ #l ] {{{ RET #; lock_proto l R }}}.
Proof.
iIntros (Φ) "Hl HΦ". wp_lam. rewrite -wp_fupd. wp_write.
iMod (lock_proto_create with "Hl [//]") as "Hproto".
iApply "HΦ". by iFrame.
Qed.
(* At this point, it'd be really nice to have some sugar for symmetric
accessors. *)
Lemma try_acquire_spec E l R P :
(P ={E,}= lock_proto l R ( lock_proto l R ={,E}= P)) -
{{{ P }}} try_acquire [ #l ] @ E
{{{ b, RET #b; (if b is true then R else True) P }}}.
Proof.
iIntros "#Hproto !# * HP HΦ".
wp_rec. iMod ("Hproto" with "HP") as "(Hinv & Hclose)".
iDestruct "Hinv" as ([]) "[Hl HR]".
- wp_apply (wp_cas_int_fail with "Hl"); [done..|]. iIntros "Hl".
iMod ("Hclose" with "[Hl]"); first (iExists true; by eauto).
iModIntro. iApply ("HΦ" $! false). auto.
- wp_apply (wp_cas_int_suc with "Hl"); [done..|]. iIntros "Hl".
iMod ("Hclose" with "[Hl]") as "HP"; first (iExists true; by eauto).
iModIntro. iApply ("HΦ" $! true); iFrame.
Qed.
Lemma acquire_spec E l R P :
(P ={E,}= lock_proto l R ( lock_proto l R ={,E}= P)) -
{{{ P }}} acquire [ #l ] @ E {{{ RET #; R P }}}.
Proof.
iIntros "#Hproto !# * HP HΦ". iLöb as "IH". wp_rec.
wp_apply (try_acquire_spec with "Hproto HP"). iIntros ([]).
- iIntros "[HR Hown]". wp_if. iApply "HΦ"; iFrame.
- iIntros "[_ Hown]". wp_if. iApply ("IH" with "Hown HΦ").
Qed.
Lemma release_spec E l R P :
(P ={E,}= lock_proto l R ( lock_proto l R ={,E}= P)) -
{{{ R P }}} release [ #l ] @ E {{{ RET #; P }}}.
Proof.
iIntros "#Hproto !# * (HR & HP) HΦ". wp_let.
iMod ("Hproto" with "HP") as "(Hinv & Hclose)".
iDestruct "Hinv" as (b) "[? _]". wp_write. iApply "HΦ".
iApply "Hclose". iExists false. by iFrame.
Qed.
End proof.
Typeclasses Opaque lock_proto.
From lrust.lang Require Export notation.
From lrust.lang Require Import heap proofmode.
Set Default Proof Using "Type".
Definition memcpy : val :=
rec: "memcpy" ["dst";"len";"src"] :=
if: "len" #0 then #
else "dst" <- !"src";;
"memcpy" ["dst" + #1 ; "len" - #1 ; "src" + #1].
Notation "e1 <-{ n } ! e2" :=
(memcpy (@cons expr e1%E
(@cons expr (Lit n)
(@cons expr e2%E nil))))
(at level 80, n at next level, format "e1 <-{ n } ! e2") : expr_scope.
Notation "e1 <-{ n ',Σ' i } ! e2" :=
(e1 <-{Σ i} () ;; e1+#1 <-{n} !e2)%E
(at level 80, n, i at next level,
format "e1 <-{ n ,Σ i } ! e2") : expr_scope.
Lemma wp_memcpy `{!lrustG Σ} E l1 l2 vl1 vl2 q (n : Z):
Z.of_nat (length vl1) = n Z.of_nat (length vl2) = n
{{{ l1 ↦∗ vl1 l2 ↦∗{q} vl2 }}}
#l1 <-{n} !#l2 @ E
{{{ RET #; l1 ↦∗ vl2 l2 ↦∗{q} vl2 }}}.
Proof.
iIntros (Hvl1 Hvl2 Φ) "(Hl1 & Hl2) HΦ".
iLöb as "IH" forall (n l1 l2 vl1 vl2 Hvl1 Hvl2). wp_rec. wp_op; case_bool_decide; wp_if.
- iApply "HΦ". assert (n = O) by lia; subst.
destruct vl1, vl2; try discriminate. by iFrame.
- destruct vl1 as [|v1 vl1], vl2 as [|v2 vl2], n as [|n|]; try (discriminate || lia).
revert Hvl1 Hvl2. intros [= Hvl1] [= Hvl2]; rewrite !heap_mapsto_vec_cons. subst n.
iDestruct "Hl1" as "[Hv1 Hl1]". iDestruct "Hl2" as "[Hv2 Hl2]".
Local Opaque Zminus.
wp_read; wp_write. do 3 wp_op. iApply ("IH" with "[%] [%] Hl1 Hl2"); [lia..|].
iIntros "!> [Hl1 Hl2]"; iApply "HΦ"; by iFrame.
Qed.
From lrust.lang Require Export notation.
From lrust.lang Require Import heap proofmode memcpy.
Set Default Proof Using "Type".
Definition new : val :=
λ: ["n"],
if: "n" #0 then #((42%positive, 1337):loc)
else Alloc "n".
Definition delete : val :=
λ: ["n"; "loc"],
if: "n" #0 then #
else Free "n" "loc".
Section specs.
Context `{!lrustG Σ}.
Lemma wp_new E n:
0 n
{{{ True }}} new [ #n ] @ E
{{{ l, RET LitV $ LitLoc l;
(l(Z.to_nat n) n = 0) l ↦∗ repeat (LitV LitPoison) (Z.to_nat n) }}}.
Proof.
iIntros (? Φ) "_ HΦ". wp_lam. wp_op; case_bool_decide.
- wp_if. assert (n = 0) as -> by lia. iApply "HΦ".
rewrite heap_mapsto_vec_nil. auto.
- wp_if. wp_alloc l as "H↦" "H†". lia. iApply "HΦ". subst sz. iFrame.
Qed.
Lemma wp_delete E (n:Z) l vl :
n = length vl
{{{ l ↦∗ vl (l(length vl) n = 0) }}}
delete [ #n; #l] @ E
{{{ RET #; True }}}.
Proof.
iIntros (? Φ) "(H↦ & [H†|%]) HΦ";
wp_lam; wp_op; case_bool_decide; try lia;
wp_if; try wp_free; by iApply "HΦ".
Qed.
End specs.
(* FIXME : why are these notations not pretty-printed? *)
Notation "'letalloc:' x <- e1 'in' e2" :=
((Lam (@cons binder x%E%E%E nil) (x <- e1 ;; e2)) [new [ #1]])%E
(at level 102, x at level 1, e1, e2 at level 150) : expr_scope.
Notation "'letalloc:' x <-{ n } ! e1 'in' e2" :=
((Lam (@cons binder x%E%E%E nil) (x <-{n%Z%V%L} !e1 ;; e2)) [new [ #n]])%E
(at level 102, x at level 1, e1, e2 at level 150) : expr_scope.
From iris.program_logic Require Import weakestpre.
From iris.base_logic.lib Require Import invariants.
From iris.proofmode Require Import tactics.
From iris.algebra Require Import excl.
From lrust.lang Require Import proofmode notation.
From lrust.lang Require Export lang.
Set Default Proof Using "Type".
Definition spawn : val :=
λ: ["f"],
let: "c" := Alloc #2 in
"c" <- #0;; (* Initialize "sent" field to 0 (non-atomically). *)
Fork ("f" ["c"]);;
"c".
Definition finish : val :=
λ: ["c"; "v"],
"c" + #1 <- "v";; (* Store data (non-atomically). *)
"c" <-ˢᶜ #1;; (* Signal that we finished (atomically!) *)
#.
Definition join : val :=
rec: "join" ["c"] :=
if: !ˢᶜ"c" then
(* The thread finished, we can non-atomically load the data. *)
let: "v" := !("c" + #1) in
Free #2 "c";;
"v"
else
"join" ["c"].
(** The CMRA & functor we need. *)
Class spawnG Σ := SpawnG { spawn_tokG :> inG Σ (exclR unitO) }.
Definition spawnΣ : gFunctors := #[GFunctor (exclR unitO)].
Instance subG_spawnΣ {Σ} : subG spawnΣ Σ spawnG Σ.
Proof. solve_inG. Qed.
(** Now we come to the Iris part of the proof. *)
Section proof.
Context `{!lrustG Σ, !spawnG Σ} (N : namespace).
Definition spawn_inv (γf γj : gname) (c : loc) (Ψ : val iProp Σ) : iProp Σ :=
(own γf (Excl ()) own γj (Excl ())
b, c #(lit_of_bool b)
if b then v, (c + 1) v Ψ v own γf (Excl ()) else True)%I.
Definition finish_handle (c : loc) (Ψ : val iProp Σ) : iProp Σ :=
( γf γj v, own γf (Excl ()) (c + 1) v inv N (spawn_inv γf γj c Ψ))%I.
Definition join_handle (c : loc) (Ψ : val iProp Σ) : iProp Σ :=
( γf γj Ψ', own γj (Excl ()) c 2 inv N (spawn_inv γf γj c Ψ')
( v, Ψ' v - Ψ v))%I.
Global Instance spawn_inv_ne n γf γj c :
Proper (pointwise_relation val (dist n) ==> dist n) (spawn_inv γf γj c).
Proof. solve_proper. Qed.
Global Instance finish_handle_ne n c :
Proper (pointwise_relation val (dist n) ==> dist n) (finish_handle c).
Proof. solve_proper. Qed.
Global Instance join_handle_ne n c :
Proper (pointwise_relation val (dist n) ==> dist n) (join_handle c).
Proof. solve_proper. Qed.
(** The main proofs. *)
Lemma spawn_spec (Ψ : val iProp Σ) e (f : val) :
IntoVal e f
{{{ c, finish_handle c Ψ - WP f [ #c] {{ _, True }} }}}
spawn [e] {{{ c, RET #c; join_handle c Ψ }}}.
Proof.
iIntros (<- Φ) "Hf HΦ". rewrite /spawn /=.
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 (γj) "Hγj"; first done.
rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
iDestruct "Hl" as "[Hc Hd]". wp_write.
iMod (inv_alloc N _ (spawn_inv γf γj l Ψ) with "[Hc]") as "#?".
{ iNext. iRight. iExists false. auto. }
wp_apply (wp_fork with "[Hγf Hf Hd]").
- iApply "Hf". iExists _, _, _. iFrame. auto.
- iIntros "_". wp_seq. iApply "HΦ". iExists _, _.
iFrame. auto.
Qed.
Lemma finish_spec (Ψ : val iProp Σ) c v :
{{{ finish_handle c Ψ Ψ v }}} finish [ #c; v] {{{ RET #; True }}}.
Proof.
iIntros (Φ) "[Hfin HΨ] HΦ". iDestruct "Hfin" as (γf γj v0) "(Hf & Hd & #?)".
wp_lam. wp_op. wp_write.
wp_bind (_ <-ˢᶜ _)%E. iInv N as "[[>Hf' _]|Hinv]" "Hclose".
{ iExFalso. iCombine "Hf" "Hf'" as "Hf". iDestruct (own_valid with "Hf") as "%".
auto. }
iDestruct "Hinv" as (b) "[>Hc _]". wp_write.
iMod ("Hclose" with "[-HΦ]").
- iNext. iRight. iExists true. iFrame. iExists _. iFrame.
- iModIntro. wp_seq. by iApply "HΦ".
Qed.
Lemma join_spec (Ψ : val iProp Σ) c :
{{{ join_handle c Ψ }}} join [ #c] {{{ v, RET v; Ψ v }}}.
Proof.
iIntros (Φ) "H HΦ". iDestruct "H" as (γf γj Ψ') "(Hj & H† & #? & #HΨ')".
iLöb as "IH". wp_rec.
wp_bind (!ˢᶜ _)%E. iInv N as "[[_ >Hj']|Hinv]" "Hclose".
{ iExFalso. iCombine "Hj" "Hj'" as "Hj". iDestruct (own_valid with "Hj") as "%".
auto. }
iDestruct "Hinv" as (b) "[>Hc Ho]". wp_read. destruct b; last first.
{ iMod ("Hclose" with "[Hc]").
- iNext. iRight. iExists _. iFrame.
- iModIntro. wp_if. iApply ("IH" with "Hj H†"). auto. }
iDestruct "Ho" as (v) "(Hd & HΨ & Hf)".
iMod ("Hclose" with "[Hj Hf]") as "_".
{ iNext. iLeft. iFrame. }
iModIntro. wp_if. wp_op. wp_read. wp_let.
iAssert (c ↦∗ [ #true; v])%I with "[Hc Hd]" as "Hc".
{ rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton. iFrame. }
wp_free; first done. iApply "HΦ". iApply "HΨ'". done.
Qed.
Lemma join_handle_impl (Ψ1 Ψ2