From 79989f27598de94144598008e0684b10693501ab Mon Sep 17 00:00:00 2001
From: Yusuke Matsushita <y.skm24t@gmail.com>
Date: Thu, 21 Apr 2022 01:57:24 +0900
Subject: [PATCH] Bump up Iris and Coq
---
.gitlab-ci.yml | 6 +--
README.md | 4 +-
coq-lambda-rust.opam | 3 +-
theories/lang/adequacy.v | 20 ++++----
theories/lang/heap.v | 47 ++++++++++++-------
theories/lang/lib/arc.v | 41 ++++++++--------
theories/lang/lib/lock.v | 4 +-
theories/lang/lib/memcpy.v | 2 +-
theories/lang/lib/new_delete.v | 2 +-
theories/lang/lib/spawn.v | 4 +-
theories/lang/lib/swap.v | 2 +-
theories/lang/lib/tests.v | 4 +-
theories/lang/lifting.v | 18 +++----
theories/lang/proofmode.v | 12 ++---
theories/lang/time.v | 36 +++++++-------
theories/lifetime/at_borrow.v | 6 +--
theories/lifetime/frac_borrow.v | 15 +++---
theories/lifetime/lifetime.v | 4 +-
theories/lifetime/lifetime_sig.v | 42 ++++++++++-------
theories/lifetime/model/accessors.v | 6 +--
theories/lifetime/model/borrow.v | 2 +-
theories/lifetime/model/borrow_sep.v | 2 +-
theories/lifetime/model/creation.v | 8 ++--
theories/lifetime/model/definitions.v | 16 +++----
theories/lifetime/model/faking.v | 2 +-
theories/lifetime/model/primitive.v | 22 +++++++--
theories/lifetime/model/reborrow.v | 8 ++--
theories/lifetime/na_borrow.v | 4 +-
theories/prophecy/prophecy.v | 23 ++++++---
theories/prophecy/syn_type.v | 2 +-
theories/typing/array.v | 6 +--
theories/typing/array_util.v | 8 ++--
theories/typing/cont_context.v | 2 +-
theories/typing/examples/get_x.v | 2 +-
theories/typing/examples/inc_vec.v | 2 +-
theories/typing/examples/init_prod.v | 2 +-
theories/typing/examples/lazy_lft.v | 2 +-
theories/typing/examples/nonlexical.v | 2 +-
theories/typing/examples/projection_toggle.v | 2 +-
theories/typing/examples/rebor.v | 2 +-
theories/typing/examples/unbox.v | 2 +-
theories/typing/fixpoint.v | 4 +-
theories/typing/function.v | 2 +-
theories/typing/lft_contexts.v | 13 +++--
theories/typing/lib/arc.v | 10 ++--
theories/typing/lib/diverging_static.v | 2 +-
theories/typing/lib/fake_shared.v | 2 +-
theories/typing/lib/join.v | 2 +-
theories/typing/lib/mutex/mutex.v | 4 +-
theories/typing/lib/mutex/mutexguard.v | 11 +++--
theories/typing/lib/panic.v | 2 +-
theories/typing/lib/rc/rc.v | 4 +-
theories/typing/lib/rc/weak.v | 2 +-
theories/typing/lib/refcell/ref.v | 2 +-
theories/typing/lib/refcell/ref_code.v | 2 +-
theories/typing/lib/refcell/refcell.v | 4 +-
theories/typing/lib/refcell/refcell_code.v | 2 +-
theories/typing/lib/refcell/refmut.v | 4 +-
theories/typing/lib/refcell/refmut_code.v | 2 +-
theories/typing/lib/rwlock/rwlock.v | 4 +-
theories/typing/lib/rwlock/rwlock_code.v | 2 +-
theories/typing/lib/rwlock/rwlockreadguard.v | 2 +-
.../typing/lib/rwlock/rwlockreadguard_code.v | 2 +-
theories/typing/lib/rwlock/rwlockwriteguard.v | 4 +-
.../typing/lib/rwlock/rwlockwriteguard_code.v | 2 +-
theories/typing/lib/slice/slice.v | 5 +-
theories/typing/lib/slice/slice_basic.v | 4 +-
theories/typing/lib/spawn.v | 2 +-
theories/typing/lib/swap.v | 2 +-
theories/typing/lib/take_mut.v | 2 +-
theories/typing/lib/vec/vec_basic.v | 4 +-
theories/typing/own.v | 6 +--
theories/typing/product.v | 6 +--
theories/typing/product_split.v | 2 +-
theories/typing/soundness.v | 6 +--
theories/typing/sum.v | 2 +-
theories/typing/type.v | 38 +++++++--------
theories/typing/type_context.v | 6 +--
theories/typing/type_sum.v | 2 +-
theories/typing/uniq_array_util.v | 6 +--
theories/typing/uniq_bor.v | 6 +--
theories/typing/uniq_cmra.v | 10 ++--
theories/typing/uniq_util.v | 6 +--
theories/util/basic.v | 2 +-
theories/util/fancy_lists.v | 6 +--
theories/util/update.v | 2 +-
theories/util/vector.v | 6 +--
87 files changed, 334 insertions(+), 286 deletions(-)
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 63aecda5..6c8cdc89 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -27,10 +27,10 @@ variables:
## Build jobs
-build-coq.8.13.0:
+build-coq.8.15.0:
<<: *template
variables:
- OPAM_PINS: "coq version 8.13.0"
+ OPAM_PINS: "coq version 8.15.0"
OPAM_PKG: "1"
DENY_WARNINGS: "1"
tags:
@@ -39,7 +39,7 @@ build-coq.8.13.0:
build-iris.dev:
<<: *template
variables:
- OPAM_PINS: "coq version 8.13.dev coq-stdpp.dev git git+https://gitlab.mpi-sws.org/iris/stdpp.git#$STDPP_REV"
+ OPAM_PINS: "coq version 8.15.dev coq-stdpp.dev git git+https://gitlab.mpi-sws.org/iris/stdpp.git#$STDPP_REV"
only:
- triggers
- schedules
diff --git a/README.md b/README.md
index 5fa668ee..d84f87cd 100644
--- a/README.md
+++ b/README.md
@@ -7,9 +7,9 @@ Functional Verification of Rust Programs with Unsafe Code".
This version is known to compile with:
-- Coq 8.13.0
+- Coq 8.15.0
- A development version of [Iris](https://gitlab.mpi-sws.org/iris/iris)
- (the version `dev.2021-03-27.0.f1484b2b`)
+ (the version `dev.2022-04-12.0.a3bed7ea`)
## Building from source
diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index 932a7b90..aa37621f 100644
--- a/coq-lambda-rust.opam
+++ b/coq-lambda-rust.opam
@@ -13,8 +13,7 @@ it possible to easily prove the functionnal correctness of well-typed program.
"""
depends: [
- "coq-iris" { (= "dev.2021-03-27.0.f1484b2b") | (= "dev") }
- "coq" { (>= "8.13.0") }
+ "coq-iris" { (= "dev.2022-04-12.0.a3bed7ea") | (= "dev") }
]
build: [make "-j%{jobs}%"]
diff --git a/theories/lang/adequacy.v b/theories/lang/adequacy.v
index 84eda49a..152c5a6a 100644
--- a/theories/lang/adequacy.v
+++ b/theories/lang/adequacy.v
@@ -5,22 +5,22 @@ From lrust.lang Require Export heap.
From lrust.lang Require Import proofmode notation.
Set Default Proof Using "Type".
-Class lrustPreG Σ := HeapPreG {
- lrust_preG_iris :> invPreG Σ;
- lrust_preG_heap :> inG Σ (authR heapUR);
- lrust_preG_heap_freeable :> inG Σ (authR heap_freeableUR);
- lrust_preG_time :> timePreG Σ
+Class lrustGpreS Σ := HeapGpreS {
+ lrustGpreS_iris :> invGpreS Σ;
+ lrustGpreS_heap :> inG Σ (authR heapUR);
+ lrustGpreS_heap_freeable :> inG Σ (authR heap_freeableUR);
+ lrustGpreS_time :> timePreG Σ
}.
Definition lrustΣ : gFunctors :=
#[invΣ; timeΣ;
GFunctor (constRF (authR heapUR));
GFunctor (constRF (authR heap_freeableUR))].
-Instance subG_heapPreG {Σ} : subG lrustΣ Σ → lrustPreG Σ.
+Instance subG_heapPreG {Σ} : subG lrustΣ Σ → lrustGpreS Σ.
Proof. solve_inG. Qed.
-Definition lrust_adequacy Σ `{!lrustPreG Σ} e σ φ :
- (∀ `{!lrustG Σ}, time_ctx -∗ WP e {{ v, ⌜φ v⌝ }}) →
+Definition lrust_adequacy Σ `{!lrustGpreS Σ} e σ φ :
+ (∀ `{!lrustGS Σ}, time_ctx -∗ WP e {{ v, ⌜φ v⌝ }}) →
adequate NotStuck e σ (λ v _, φ v).
Proof.
intros Hwp. apply adequate_alt. intros t2 σ2 [n [κs ?]]%erased_steps_nsteps.
@@ -30,9 +30,9 @@ Proof.
iMod (own_alloc (● (∅ : heap_freeableUR))) as (fγ) "Hfγ";
first by apply auth_auth_valid.
iMod time_init as (Htime) "[TIME Htime]"; [done|].
- set (Hheap := HeapG _ _ _ vγ fγ).
+ set (Hheap := HeapGS _ _ _ vγ fγ).
iModIntro. iExists NotStuck, _, [_], _, _. simpl.
- iDestruct (Hwp (LRustG _ _ Hheap Htime) with "TIME") as "$".
+ iDestruct (Hwp (LRustGS _ _ Hheap Htime) with "TIME") as "$".
iSplitL; first by auto with iFrame. iIntros ([|e' [|]]? -> ??) "//".
iIntros "[??] [?_] _". iApply fupd_mask_weaken; [|iIntros "_ !>"]; [done|].
iSplit; [|done]. iIntros (v2 t2'' [= -> <-]). by rewrite to_of_val.
diff --git a/theories/lang/heap.v b/theories/lang/heap.v
index 19b0c821..5fe4d602 100644
--- a/theories/lang/heap.v
+++ b/theories/lang/heap.v
@@ -4,9 +4,9 @@ From iris.algebra Require Import big_op gmap frac agree numbers.
From iris.algebra Require Import csum excl auth cmra_big_op.
From iris.bi Require Import fractional.
From iris.base_logic Require Export lib.own.
-From iris.proofmode Require Export tactics.
+From iris.proofmode Require Export proofmode.
From lrust.lang Require Export lang.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Import uPred.
Definition lock_stateR : cmra :=
@@ -18,7 +18,7 @@ Definition heapUR : ucmra :=
Definition heap_freeableUR : ucmra :=
gmapUR block (prodR fracR (gmapR Z (exclR unitO))).
-Class heapG Σ := HeapG {
+Class heapGS Σ := HeapGS {
heap_inG :> inG Σ (authR heapUR);
heap_freeable_inG :> inG Σ (authR heap_freeableUR);
heap_name : gname;
@@ -34,7 +34,7 @@ Definition heap_freeable_rel (σ : state) (hF : heap_freeableUR) : Prop :=
qs.2 ≠ ∅ ∧ ∀ i, is_Some (σ !! (blk, i)) ↔ is_Some (qs.2 !! i).
Section definitions.
- Context `{!heapG Σ}.
+ Context `{!heapGS Σ}.
Definition heap_mapsto_st (st : lock_state)
(l : loc) (q : Qp) (v: val) : iProp Σ :=
@@ -42,7 +42,7 @@ Section definitions.
Definition heap_mapsto_def (l : loc) (q : Qp) (v: val) : iProp Σ :=
heap_mapsto_st (RSt 0) l q v.
- Definition heap_mapsto_aux : seal (@heap_mapsto_def). by eexists. Qed.
+ Definition heap_mapsto_aux : seal (@heap_mapsto_def). Proof. by eexists. Qed.
Definition heap_mapsto := unseal heap_mapsto_aux.
Definition heap_mapsto_eq : @heap_mapsto = @heap_mapsto_def :=
seal_eq heap_mapsto_aux.
@@ -55,7 +55,7 @@ Section definitions.
Definition heap_freeable_def (l : loc) (q : Qp) (n: nat) : iProp Σ :=
own heap_freeable_name (◯ {[ l.1 := (q, inter (l.2) n) ]}).
- Definition heap_freeable_aux : seal (@heap_freeable_def). by eexists. Qed.
+ Definition heap_freeable_aux : seal (@heap_freeable_def). Proof. by eexists. Qed.
Definition heap_freeable := unseal heap_freeable_aux.
Definition heap_freeable_eq : @heap_freeable = @heap_freeable_def :=
seal_eq heap_freeable_aux.
@@ -67,8 +67,8 @@ Section definitions.
End definitions.
Typeclasses Opaque heap_mapsto heap_freeable heap_mapsto_vec.
-Instance: Params (@heap_mapsto) 4 := {}.
-Instance: Params (@heap_freeable) 5 := {}.
+Global Instance: Params (@heap_mapsto) 4 := {}.
+Global Instance: Params (@heap_freeable) 5 := {}.
Notation "l ↦{ q } v" := (heap_mapsto l q v)
(at level 20, q at level 50, format "l ↦{ q } v") : bi_scope.
@@ -106,7 +106,7 @@ Section to_heap.
End to_heap.
Section heap.
- Context `{!heapG Σ}.
+ Context `{!heapGS Σ}.
Implicit Types P Q : iProp Σ.
Implicit Types σ : state.
Implicit Types E : coPset.
@@ -122,7 +122,11 @@ Section heap.
Qed.
Global Instance heap_mapsto_as_fractional l q v:
AsFractional (l ↦{q} v) (λ q, l ↦{q} v)%I q.
- Proof. split. done. apply _. Qed.
+ Proof. split; first done. apply _. Qed.
+ Global Instance frame_heap_mapsto p l v q1 q2 RES :
+ FrameFractionalHyps p (l ↦{q1} v) (λ q, l ↦{q} v)%I RES q1 q2 →
+ Frame p (l ↦{q1} v) (l ↦{q2} v) RES | 5.
+ Proof. apply: frame_fractional. Qed.
Global Instance heap_mapsto_vec_timeless l q vl : Timeless (l ↦∗{q} vl).
Proof. rewrite /heap_mapsto_vec. apply _. Qed.
@@ -134,7 +138,11 @@ Section heap.
Qed.
Global Instance heap_mapsto_vec_as_fractional l q vl:
AsFractional (l ↦∗{q} vl) (λ q, l ↦∗{q} vl)%I q.
- Proof. split. done. apply _. Qed.
+ Proof. split; first done. apply _. Qed.
+ Global Instance frame_heap_mapsto_vec p l vl q1 q2 RES :
+ FrameFractionalHyps p (l ↦∗{q1} vl) (λ q, l ↦∗{q} vl)%I RES q1 q2 →
+ Frame p (l ↦∗{q1} vl) (l ↦∗{q2} vl) RES | 5.
+ Proof. apply: frame_fractional. Qed.
Global Instance heap_freeable_timeless q l n : Timeless (†{q}l…n).
Proof. rewrite heap_freeable_eq /heap_freeable_def. apply _. Qed.
@@ -243,7 +251,7 @@ Section heap.
Qed.
Global Instance heap_mapsto_pred_as_fractional l q (P : list val → iProp Σ):
(∀ vl, Persistent (P vl)) → AsFractional (l ↦∗{q}: P) (λ q, l ↦∗{q}: P)%I q.
- Proof. split. done. apply _. Qed.
+ Proof. split; first done. apply _. Qed.
Lemma inter_lookup_Some i j (n : nat):
i ≤ j < i+n → inter i n !! j = Excl' ().
@@ -266,7 +274,7 @@ Section heap.
- by rewrite !inter_lookup_None; try lia.
Qed.
Lemma inter_valid i n : ✓ inter i n.
- Proof. revert i. induction n as [|n IH]=>i. done. by apply insert_valid. Qed.
+ Proof. revert i. induction n as [|n IH]=>i; first done. by apply insert_valid. Qed.
Lemma heap_freeable_op_eq l q1 q2 n n' :
†{q1}l…n ∗ †{q2}l+ₗn … n' ⊣⊢ †{q1+q2}l…(n+n').
@@ -349,7 +357,7 @@ Section heap.
etrans; first apply (IH (l +ₗ 1)).
{ intros. by rewrite shift_loc_assoc. }
rewrite shift_loc_0 -insert_singleton_op; last first.
- { rewrite -equiv_None big_opL_commute equiv_None big_opL_None=> l' v' ?.
+ { rewrite -None_equiv_eq big_opL_commute None_equiv_eq big_opL_None=> l' v' ?.
rewrite lookup_singleton_None -{2}(shift_loc_0 l). apply not_inj; lia. }
rewrite to_heap_insert. setoid_rewrite shift_loc_assoc.
apply alloc_local_update; last done. apply lookup_to_heap_None.
@@ -370,12 +378,13 @@ Section heap.
{ apply auth_update_alloc,
(alloc_singleton_local_update _ (l.1) (1%Qp, inter (l.2) (Z.to_nat n))).
- eauto using heap_freeable_rel_None.
- - split. done. apply inter_valid. }
+ - split; first done. apply inter_valid. }
iModIntro. iSplitL "Hvalσ HhF".
{ iExists _. iFrame. iPureIntro.
auto using heap_freeable_rel_init_mem. }
- rewrite heap_freeable_eq /heap_freeable_def heap_mapsto_vec_combine //.
- iFrame. destruct (Z.to_nat n); done.
+ rewrite heap_freeable_eq /heap_freeable_def heap_mapsto_vec_combine //; last first.
+ { destruct (Z.to_nat n); done. }
+ iFrame.
Qed.
Lemma heap_free_vs σ l vl :
@@ -437,7 +446,9 @@ Section heap.
[/Some_pair_included [_ Hincl] /to_agree_included->].
destruct ls as [|n], ls'' as [|n''],
Hincl as [[[|n'|]|] [=]%leibniz_equiv]; subst.
- by exists O. eauto. exists O. by rewrite Nat.add_0_r.
+ - by exists O.
+ - eauto.
+ - exists O. by rewrite Nat.add_0_r.
Qed.
Lemma heap_mapsto_lookup_1 σ l ls v :
diff --git a/theories/lang/lib/arc.v b/theories/lang/lib/arc.v
index 86c49cb6..8c897d67 100644
--- a/theories/lang/lib/arc.v
+++ b/theories/lang/lib/arc.v
@@ -1,12 +1,12 @@
From iris.base_logic.lib Require Import invariants.
From iris.program_logic Require Import weakestpre.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
From iris.bi Require Import fractional.
From iris.algebra Require Import excl csum frac auth numbers.
From lrust.lang Require Import lang proofmode notation new_delete.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
-(* A: 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
not be necessary.
@@ -24,7 +24,7 @@ What's wrong with this protocol? The "only" problem I can see is that if
someone tries to upgrade a weak after we did the CAS, then this will
fail even though this could be possible.
-B: Upgrade failing spuriously sounds like a problem severe enough to
+RJ: Upgrade failing spuriously sounds like a problem severe enough to
justify the locking protocol.
*)
@@ -99,7 +99,7 @@ Definition try_unwrap_full : val :=
else #2.
(** The CMRA we need. *)
-(* Not bundling heapG, as it may be shared with other users. *)
+(* Not bundling heapGS, as it may be shared with other users. *)
(* See rc.v for understanding the structure of this CMRA.
The only additional thing is the [optionR (exclR unitO))], used to handle
@@ -110,11 +110,11 @@ Definition arc_stR :=
Class arcG Σ :=
RcG :> inG Σ (authR arc_stR).
Definition arcΣ : gFunctors := #[GFunctor (authR arc_stR)].
-Instance subG_arcΣ {Σ} : subG arcΣ Σ → arcG Σ.
+Global Instance subG_arcΣ {Σ} : subG arcΣ Σ → arcG Σ.
Proof. solve_inG. Qed.
Section def.
- Context `{!lrustG Σ, !arcG Σ} (P1 : Qp → iProp Σ) (P2 : iProp Σ) (N : namespace).
+ Context `{!lrustGS Σ, !arcG Σ} (P1 : Qp → iProp Σ) (P2 : iProp Σ) (N : namespace).
Definition arc_tok γ q : iProp Σ :=
own γ (◯ (Some $ Cinl (q, 1%positive, None), 0%nat)).
@@ -158,10 +158,10 @@ Section arc.
this is the lifetime token), and P2 is the thing that is owned by the
protocol when only weak references are left (in practice, P2 is the
ownership of the underlying memory incl. deallocation). *)
- Context `{!lrustG Σ, !arcG Σ} (P1 : Qp → iProp Σ) {HP1:Fractional P1}
+ Context `{!lrustGS Σ, !arcG Σ} (P1 : Qp → iProp Σ) {HP1:Fractional P1}
(P2 : iProp Σ) (N : namespace).
- Instance P1_AsFractional q : AsFractional (P1 q) P1 q.
+ Local Instance P1_AsFractional q : AsFractional (P1 q) P1 q.
Proof using HP1. done. Qed.
Global Instance arc_inv_ne n :
@@ -284,7 +284,7 @@ Section arc.
- 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 qq. auto with iFrame. }
+ { iExists _. iFrame. iExists qq. iCombine "HP1 HP1'" as "$". auto with iFrame. }
iModIntro. wp_case. iApply ("IH" with "HP HΦ").
Qed.
@@ -398,7 +398,7 @@ Section arc.
{ iIntros "!> HP". iInv N as (st) "[>H● H]" "Hclose1".
iMod ("Hacc" with "HP") as "[Hown Hclose2]".
iDestruct (weak_tok_auth_val with "H● Hown") as %(st' & weak & -> & Hval).
- destruct st' as [[[[??]?]| |]|]; try done; iExists _.
+ destruct st' as [[[[q' c]?]| |]|]; try done; iExists _.
- iDestruct "H" as (q) "(>Heq & [HP1 HP1'] & >$ & ?)". iDestruct "Heq" as %Heq.
iIntros "!>"; iSplit; iMod ("Hclose2" with "Hown") as "HP".
+ iIntros "_ Hl". iExists (q/2)%Qp. iMod (own_update with "H●") as "[H● $]".
@@ -408,10 +408,10 @@ Section arc.
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
+ rewrite /= [xH ⋅ _]comm_L frac_op [(_ + q')%Qp]comm -[(_ + _)%Qp]assoc
Qp_div_2 left_id_L. auto with iFrame.
+ iIntros "Hl". iFrame. iApply ("Hclose1" with "[-]"). iExists _. iFrame.
- iExists q. auto with iFrame.
+ iExists q. iCombine "HP1 HP1'" as "$". auto with iFrame.
- iDestruct "H" as "[>$ ?]". iIntros "!>"; iSplit; first by auto with congruence.
iIntros "Hl". iMod ("Hclose2" with "Hown") as "$". iApply "Hclose1".
iExists _. auto with iFrame.
@@ -521,14 +521,16 @@ Section arc.
by apply (op_local_update _ _ (Some (Cinr (Excl ())))). }
iMod ("Hclose" with "[H● Hs Hw]") as "_"; first by iExists _; do 2 iFrame.
iModIntro. wp_case. iApply wp_fupd. wp_op.
- iApply ("HΦ"). rewrite -{2}Hq''. iFrame. by iApply close_last_strong.
+ iApply ("HΦ"). rewrite -{2}Hq''. iCombine "HP1 HP1'" as "$".
+ by iApply close_last_strong.
+ destruct Hqq' as [? ->].
rewrite -[in (_, _)](Pos.succ_pred s) // -[wl in Cinl (_, wl)]left_id
-Pos.add_1_l 2!pair_op Cinl_op Some_op.
iMod (own_update_2 _ _ _ _ with "H● Hown") as "H●".
{ apply auth_update_dealloc, prod_local_update_1, @cancel_local_update_unit, _. }
iMod ("Hclose" with "[- HΦ]") as "_".
- { iExists _. iFrame. iExists (q + q'')%Qp. iFrame. iSplit; last by destruct s.
+ { iExists _. iFrame. iExists (q + q'')%Qp. iCombine "HP1 HP1'" as "$".
+ iSplit; last by destruct s.
iIntros "!> !%". rewrite assoc -Hq''. f_equal. apply comm, _. }
iModIntro. wp_case. wp_op; case_bool_decide; simplify_eq. by iApply "HΦ".
- wp_apply (wp_cas_int_fail with "Hs"); [congruence|]. iIntros "Hs".
@@ -553,7 +555,8 @@ Section arc.
etrans; first apply: cancel_local_update_unit.
by apply (op_local_update _ _ (Some (Cinr (Excl ())))). }
iMod ("Hclose" with "[H● Hs Hw]") as "_"; first by iExists _; do 2 iFrame.
- iApply ("HΦ" $! true). rewrite -{1}Hq''. iFrame. by iApply close_last_strong.
+ iApply ("HΦ" $! true). rewrite -{1}Hq''. iCombine "HP1 HP1'" as "$".
+ by iApply close_last_strong.
- wp_apply (wp_cas_int_fail with "Hs"); [congruence|]. iIntros "Hs".
iMod ("Hclose" with "[-Hown HP1 HΦ]") as "_"; first by iExists _; auto with iFrame.
iApply ("HΦ" $! false). by iFrame.
@@ -597,7 +600,7 @@ Section arc.
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_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 (? & ? & ->).
{ destruct Hincl as [|Hincl]; first by setoid_subst; eauto.
apply csum_included in Hincl. destruct Hincl as [->|[Hincl|(?&?&[=]&?)]]=>//.
@@ -610,13 +613,13 @@ Section arc.
csum_local_update_l, prod_local_update_2, delete_option_local_update, _. }
iMod ("Hclose" with "[-HΦ H◯ HP1]") as "_"; first by iExists _; auto with iFrame.
iModIntro. wp_seq. iApply "HΦ". iFrame.
- + setoid_subst. iDestruct "H" as (?) "(Hq & ? & ? & >? & >%)". subst. wp_read.
+ + setoid_subst. iDestruct "H" as (?) "(Hq & HP1' & ? & >? & >%)". subst. wp_read.
iMod (own_update_2 with "H● H◯") as "H●".
{ apply auth_update_dealloc. rewrite -{1}[(_, 0%nat)]right_id.
apply cancel_local_update_unit, _. }
iMod ("Hclose" with "[H●]") as "_"; first by iExists _; iFrame.
iModIntro. wp_seq. wp_op. wp_let. wp_op. wp_write. iApply "HΦ".
- iDestruct "Hq" as %<-. iFrame.
+ iDestruct "Hq" as %<-. iCombine "HP1 HP1'" as "$". iFrame.
Qed.
Lemma try_unwrap_full_spec (γ : gname) (q: Qp) (l : loc) :
diff --git a/theories/lang/lib/lock.v b/theories/lang/lib/lock.v
index ae421b61..2ab7a9f3 100644
--- a/theories/lang/lib/lock.v
+++ b/theories/lang/lib/lock.v
@@ -1,5 +1,5 @@
From iris.program_logic Require Import weakestpre.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
From iris.algebra Require Import excl.
From lrust.lang Require Import lang proofmode notation.
Set Default Proof Using "Type".
@@ -16,7 +16,7 @@ Definition release : val := λ: ["l"], "l" <-ˢᶜ #false.
their cancelling view shift has a non-empty mask, and it would have to be
executed in the consequence view shift of a borrow. *)
Section proof.
- Context `{!lrustG Σ}.
+ Context `{!lrustGS Σ}.
Definition lock_proto (l : loc) (R : iProp Σ) : iProp Σ :=
(∃ b : bool, l ↦ #b ∗ if b then True else R)%I.
diff --git a/theories/lang/lib/memcpy.v b/theories/lang/lib/memcpy.v
index 59272fd5..cdb8058e 100644
--- a/theories/lang/lib/memcpy.v
+++ b/theories/lang/lib/memcpy.v
@@ -16,7 +16,7 @@ Notation "e1 <-{ n ',Σ' i } ! e2" :=
(e1%E%E <- #(LitInt i);; e1 +ₗ #(LitInt 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):
+Lemma wp_memcpy `{!lrustGS Σ} E l1 l2 vl1 vl2 q (n : Z):
Z.of_nat (length vl1) = n → Z.of_nat (length vl2) = n →
{{{ l1 ↦∗ vl1 ∗ l2 ↦∗{q} vl2 }}}
#l1 <-{n} !#l2 @ E
diff --git a/theories/lang/lib/new_delete.v b/theories/lang/lib/new_delete.v
index d1db9df5..4d4dbd69 100644
--- a/theories/lang/lib/new_delete.v
+++ b/theories/lang/lib/new_delete.v
@@ -13,7 +13,7 @@ Definition delete : val :=
else Free "n" "loc".
Section specs.
- Context `{!lrustG Σ}.
+ Context `{!lrustGS Σ}.
Lemma wp_new E n:
0 ≤ n →
diff --git a/theories/lang/lib/spawn.v b/theories/lang/lib/spawn.v
index 55feed47..66ad5d22 100644
--- a/theories/lang/lib/spawn.v
+++ b/theories/lang/lib/spawn.v
@@ -1,6 +1,6 @@
From iris.program_logic Require Import weakestpre.
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 lrust.lang Require Import proofmode notation.
From lrust.lang Require Export lang.
@@ -36,7 +36,7 @@ Proof. solve_inG. Qed.
(** Now we come to the Iris part of the proof. *)
Section proof.
-Context `{!lrustG Σ, !spawnG Σ} (N : namespace).
+Context `{!lrustGS Σ, !spawnG Σ} (N : namespace).
Definition spawn_inv (γf γj : gname) (c : loc) (Ψ : val → iProp Σ) : iProp Σ :=
(own γf (Excl ()) ∗ own γj (Excl ()) ∨
diff --git a/theories/lang/lib/swap.v b/theories/lang/lib/swap.v
index d182c900..e6997bbe 100644
--- a/theories/lang/lib/swap.v
+++ b/theories/lang/lib/swap.v
@@ -10,7 +10,7 @@ Definition swap : val :=
"p2" <- "x";;
"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 →
{{{ l1 ↦∗ vl1 ∗ l2 ↦∗ vl2 }}}
swap [ #l1; #l2; #n] @ E
diff --git a/theories/lang/lib/tests.v b/theories/lang/lib/tests.v
index 8f414deb..7f6ebbaa 100644
--- a/theories/lang/lib/tests.v
+++ b/theories/lang/lib/tests.v
@@ -1,10 +1,10 @@
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.
Set Default Proof Using "Type".
Section tests.
- Context `{!lrustG Σ}.
+ Context `{!lrustGS Σ}.
Lemma test_location_cmp E (l1 l2 : loc) q1 q2 v1 v2 :
{{{ ▷ l1 ↦{q1} v1 ∗ ▷ l2 ↦{q2} v2 }}}
diff --git a/theories/lang/lifting.v b/theories/lang/lifting.v
index 1ccf972c..844d971d 100644
--- a/theories/lang/lifting.v
+++ b/theories/lang/lifting.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
From iris.program_logic Require Export weakestpre.
From iris.program_logic Require Import ectx_lifting.
From lrust.lang Require Export lang heap time.
@@ -6,14 +6,14 @@ From lrust.lang Require Import tactics.
Set Default Proof Using "Type".
Import uPred.
-Class lrustG Σ := LRustG {
- lrustG_invG : invG Σ;
- lrustG_gen_heapG :> heapG Σ;
- lrustG_gen_timeG :> timeG Σ
+Class lrustGS Σ := LRustGS {
+ lrustGS_invGS : invGS Σ;
+ lrustGS_gen_heapGS :> heapGS Σ;
+ lrustGS_gen_timeGS :> timeGS Σ
}.
-Program Instance lrustG_irisG `{!lrustG Σ} : irisG lrust_lang Σ := {
- iris_invG := lrustG_invG;
+Program Instance lrustGS_irisGS `{!lrustGS Σ} : irisGS lrust_lang Σ := {
+ iris_invGS := lrustGS_invGS;
state_interp σ stepcnt κs _ := (heap_ctx σ ∗ time_interp stepcnt)%I;
fork_post _ := True%I;
num_laters_per_step n := n
@@ -22,7 +22,7 @@ Next Obligation.
intros. iIntros "/= [$ H]". by iMod (time_interp_step with "H") as "$".
Qed.
-Global Opaque iris_invG.
+Global Opaque iris_invGS.
Ltac inv_lit :=
repeat match goal with
@@ -67,7 +67,7 @@ Instance do_subst_vec xl (vsl : vec val (length xl)) e :
Proof. by rewrite /DoSubstL subst_v_eq. Qed.
Section lifting.
-Context `{!lrustG Σ}.
+Context `{!lrustGS Σ}.
Implicit Types P Q : iProp Σ.
Implicit Types e : expr.
Implicit Types ef : option expr.
diff --git a/theories/lang/proofmode.v b/theories/lang/proofmode.v
index 386756f2..14b227b6 100644
--- a/theories/lang/proofmode.v
+++ b/theories/lang/proofmode.v
@@ -6,14 +6,14 @@ From lrust.lang Require Export tactics lifting.
Set Default Proof Using "Type".
Import uPred.
-Lemma tac_wp_value `{!lrustG Σ} Δ E Φ e v :
+Lemma tac_wp_value `{!lrustGS Σ} Δ E Φ e v :
IntoVal e v →
envs_entails Δ (Φ v) → envs_entails Δ (WP e @ E {{ Φ }}).
Proof. rewrite envs_entails_eq=> ? ->. by apply wp_value. Qed.
Ltac wp_value_head := eapply tac_wp_value; [iSolveTC|reduction.pm_prettify].
-Lemma tac_wp_pure `{!lrustG Σ} K Δ Δ' E e1 e2 φ n Φ :
+Lemma tac_wp_pure `{!lrustGS Σ} K Δ Δ' E e1 e2 φ n Φ :
PureExec φ n e1 e2 →
φ →
MaybeIntoLaterNEnvs n Δ Δ' →
@@ -38,7 +38,7 @@ Tactic Notation "wp_pure" open_constr(efoc) :=
| _ => fail "wp_pure: not a 'wp'"
end.
-Lemma tac_wp_eq_loc `{!lrustG Σ} K Δ Δ' E i1 i2 l1 l2 q1 q2 v1 v2 Φ :
+Lemma tac_wp_eq_loc `{!lrustGS Σ} K Δ Δ' E i1 i2 l1 l2 q1 q2 v1 v2 Φ :
MaybeIntoLaterNEnvs 1 Δ Δ' →
envs_lookup i1 Δ' = Some (false, l1 ↦{q1} v1)%I →
envs_lookup i2 Δ' = Some (false, l2 ↦{q2} v2)%I →
@@ -67,7 +67,7 @@ Tactic Notation "wp_op" := wp_pure (BinOp _ _ _) || wp_eq_loc.
Tactic Notation "wp_if" := wp_pure (If _ _ _).
Tactic Notation "wp_case" := wp_pure (Case _ _); try wp_value_head.
-Lemma tac_wp_bind `{!lrustG Σ} K Δ E Φ e :
+Lemma tac_wp_bind `{!lrustGS Σ} K Δ E Φ e :
envs_entails Δ (WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }})%I →
envs_entails Δ (WP fill K e @ E {{ Φ }}).
Proof. rewrite envs_entails_eq=> ->. apply: wp_bind. Qed.
@@ -89,12 +89,12 @@ Tactic Notation "wp_bind" open_constr(efoc) :=
end.
Section heap.
-Context `{!lrustG Σ}.
+Context `{!lrustGS Σ}.
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val → iProp Σ.
Implicit Types Δ : envs (uPredI (iResUR Σ)).
-Lemma tac_wp_nd_int `{!lrustG Σ} K Δ Δ' E Φ :
+Lemma tac_wp_nd_int `{!lrustGS Σ} K Δ Δ' E Φ :
MaybeIntoLaterNEnvs 1 Δ Δ' →
(∀z, envs_entails Δ' (WP fill K (Lit (LitInt z)) @ E {{ Φ }})) →
envs_entails Δ (WP fill K NdInt @ E {{ Φ }}).
diff --git a/theories/lang/time.v b/theories/lang/time.v
index f7532a6a..3e26718a 100644
--- a/theories/lang/time.v
+++ b/theories/lang/time.v
@@ -1,12 +1,12 @@
From iris.algebra Require Import lib.mono_nat numbers.
From iris.base_logic Require Import lib.own.
From iris.base_logic.lib Require Export invariants.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
From lrust.lang Require Export lang.
Set Default Proof Using "Type".
Import uPred.
-Class timeG Σ := TimeG {
+Class timeGS Σ := TimeG {
time_mono_nat_inG :> inG Σ mono_natR;
time_nat_inG :> inG Σ (authR natUR);
time_global_name : gname;
@@ -27,7 +27,7 @@ Proof. solve_inG. Qed.
Definition timeN : namespace := nroot .@ "lft_usr" .@ "time".
Section definitions.
- Context `{!timeG Σ}.
+ Context `{!timeGS Σ}.
(** persistent time receipt *)
Definition persistent_time_receipt (n : nat) :=
@@ -36,19 +36,19 @@ Section definitions.
Definition cumulative_time_receipt (n : nat) :=
own time_cumulative_name (◯ n).
(** invariant *)
- Definition time_ctx `{!invG Σ} :=
+ Definition time_ctx `{!invGS Σ} :=
inv timeN (∃ n m,
own time_global_name (mono_nat_lb (n + m)) ∗
own time_cumulative_name (● n) ∗
- own time_persistent_name (mono_nat_auth 1 m)).
+ own time_persistent_name (●MN m)).
(** authority *)
Definition time_interp (n: nat) : iProp Σ :=
- own time_global_name (mono_nat_auth 1 n).
+ own time_global_name (●MN n).
End definitions.
-Typeclasses Opaque persistent_time_receipt cumulative_time_receipt.
-Instance: Params (@persistent_time_receipt) 2 := {}.
-Instance: Params (@cumulative_time_receipt) 2 := {}.
+Global Typeclasses Opaque persistent_time_receipt cumulative_time_receipt.
+Global Instance: Params (@persistent_time_receipt) 2 := {}.
+Global Instance: Params (@cumulative_time_receipt) 2 := {}.
Notation "⧖ n" := (persistent_time_receipt n)
(at level 1, format "⧖ n") : bi_scope.
@@ -56,7 +56,7 @@ Notation "⧗ n" := (cumulative_time_receipt n)
(at level 1, format "⧗ n") : bi_scope.
Section time.
- Context `{!timeG Σ}.
+ Context `{!timeGS Σ}.
Implicit Types P Q : iProp Σ.
Global Instance persistent_time_receipt_timeless n : Timeless (⧖n).
@@ -83,7 +83,7 @@ Section time.
Qed.
Lemma persistent_time_receipt_sep n m : ⧖(n `max` m) ⊣⊢ ⧖n ∗ ⧖m.
- Proof. by rewrite /persistent_time_receipt -mono_nat_lb_op own_op. Qed.
+ Proof. by rewrite /persistent_time_receipt mono_nat_lb_op own_op. Qed.
Lemma cumulative_time_receipt_sep n m : ⧗(n + m) ⊣⊢ ⧗n ∗ ⧗m.
Proof. by rewrite /cumulative_time_receipt -nat_op auth_frag_op own_op. Qed.
@@ -101,7 +101,7 @@ Section time.
Lemma cumulative_time_receipt_0 : ⊢ |==> ⧗0.
Proof. rewrite /cumulative_time_receipt. apply own_unit. Qed.
- Lemma cumulative_persistent_time_receipt `{!invG Σ} E n m :
+ Lemma cumulative_persistent_time_receipt `{!invGS Σ} E n m :
↑timeN ⊆ E → time_ctx -∗ ⧗n -∗ ⧖m ={E}=∗ ⧖(n + m).
Proof.
iIntros (?) "#TIME Hn #Hm".
@@ -121,7 +121,7 @@ Section time.
rewrite (_:(n'+m')%nat = ((n'-n) + (m'+n))%nat); [done|lia].
Qed.
- Lemma step_cumulative_time_receipt `{!invG Σ} E n :
+ Lemma step_cumulative_time_receipt `{!invGS Σ} E n :
↑timeN ⊆ E →
time_ctx -∗ time_interp n ={E, E∖↑timeN}=∗ time_interp n ∗
(time_interp (S n) ={E∖↑timeN, E}=∗ time_interp (S n) ∗ ⧗1).
@@ -137,7 +137,7 @@ Section time.
iApply (own_mono with "H'Sn"). apply mono_nat_lb_mono. lia.
Qed.
- Lemma time_receipt_le `{!invG Σ} E n m m' :
+ Lemma time_receipt_le `{!invGS Σ} E n m m' :
↑timeN ⊆ E →
time_ctx -∗ time_interp n -∗ ⧖m -∗ ⧗m' ={E}=∗
⌜m+m' ≤ n⌝%nat ∗ time_interp n ∗ ⧗m'.
@@ -151,13 +151,13 @@ Section time.
Qed.
End time.
-Lemma time_init `{!invG Σ, !timePreG Σ} E : ↑timeN ⊆ E →
- ⊢ |={E}=> ∃ _ : timeG Σ, time_ctx ∗ time_interp 0.
+Lemma time_init `{!invGS Σ, !timePreG Σ} E : ↑timeN ⊆ E →
+ ⊢ |={E}=> ∃ _ : timeGS Σ, time_ctx ∗ time_interp 0.
Proof.
intros ?.
- iMod (own_alloc (mono_nat_auth 1 0 ⋅ mono_nat_lb 0)) as (time_global_name) "[??]";
+ iMod (own_alloc (●MN 0 ⋅ mono_nat_lb 0)) as (time_global_name) "[??]";
[by apply mono_nat_both_valid|].
- iMod (own_alloc (mono_nat_auth 1 0)) as (time_persistent_name) "?";
+ iMod (own_alloc (●MN 0)) as (time_persistent_name) "?";
[by apply mono_nat_auth_valid|].
iMod (own_alloc (● 0%nat)) as (time_cumulative_name) "?"; [by apply auth_auth_valid|].
iExists (TimeG _ _ _ time_global_name time_persistent_name time_cumulative_name).
diff --git a/theories/lifetime/at_borrow.v b/theories/lifetime/at_borrow.v
index 0c9d3409..091ab883 100644
--- a/theories/lifetime/at_borrow.v
+++ b/theories/lifetime/at_borrow.v
@@ -5,14 +5,14 @@ Set Default Proof Using "Type".
(** Atomic persistent bors *)
(* TODO : update the TEX with the fact that we can choose the namespace. *)
-Definition at_bor `{!invG Σ, !lftG Σ} κ N (P : iProp Σ) :=
+Definition at_bor `{!invGS Σ, !lftGS Σ} κ N (P : iProp Σ) :=
(∃ i, &{κ,i}P ∗
(⌜N ## lftN⌝ ∗ inv N (idx_bor_own 1 i) ∨
⌜N = lftN⌝ ∗ inv N (∃ q, idx_bor_own q i)))%I.
Notation "&at{ κ , N }" := (at_bor κ N) (format "&at{ κ , N }") : bi_scope.
Section atomic_bors.
- Context `{!invG Σ, !lftG Σ} (P : iProp Σ) (N : namespace).
+ Context `{!invGS Σ, !lftGS Σ} (P : iProp Σ) (N : namespace).
Global Instance at_bor_ne κ n : Proper (dist n ==> dist n) (at_bor κ N).
Proof. solve_proper. Qed.
@@ -97,7 +97,7 @@ Section atomic_bors.
Qed.
End atomic_bors.
-Lemma at_bor_acc_lftN `{!invG Σ, !lftG Σ} (P : iProp Σ) E κ :
+Lemma at_bor_acc_lftN `{!invGS Σ, !lftGS Σ} (P : iProp Σ) E κ :
↑lftN ⊆ E →
lft_ctx -∗ &at{κ,lftN}P ={E,E∖↑lftN}=∗ ▷P ∗ (▷P ={E∖↑lftN,E}=∗ True) ∨
[†κ] ∗ |={E∖↑lftN,E}=> True.
diff --git a/theories/lifetime/frac_borrow.v b/theories/lifetime/frac_borrow.v
index 8936fa11..d0475952 100644
--- a/theories/lifetime/frac_borrow.v
+++ b/theories/lifetime/frac_borrow.v
@@ -6,15 +6,15 @@ Set Default Proof Using "Type".
Class frac_borG Σ := frac_borG_inG :> inG Σ fracR.
-Local Definition frac_bor_inv `{!invG Σ, !lftG Σ, !frac_borG Σ} (φ : Qp → iProp Σ) γ κ' :=
+Local Definition frac_bor_inv `{!invGS Σ, !lftGS Σ, !frac_borG Σ} (φ : Qp → iProp Σ) γ κ' :=
(∃ q, φ q ∗ own γ q ∗ (⌜q = 1%Qp⌝ ∨ ∃ q', ⌜(q + q' = 1)%Qp⌝ ∗ q'.[κ']))%I.
-Definition frac_bor `{!invG Σ, !lftG Σ, !frac_borG Σ} κ (φ : Qp → iProp Σ) :=
+Definition frac_bor `{!invGS Σ, !lftGS Σ, !frac_borG Σ} κ (φ : Qp → iProp Σ) :=
(∃ γ κ', κ ⊑ κ' ∗ &at{κ',lftN} (frac_bor_inv φ γ κ'))%I.
Notation "&frac{ κ }" := (frac_bor κ) (format "&frac{ κ }") : bi_scope.
Section frac_bor.
- Context `{!invG Σ, !lftG Σ, !frac_borG Σ} (φ : Qp → iProp Σ).
+ Context `{!invGS Σ, !lftGS Σ, !frac_borG Σ} (φ : Qp → iProp Σ).
Implicit Types E : coPset.
Global Instance frac_bor_contractive κ n :
@@ -108,8 +108,8 @@ Section frac_bor.
- iRight. iExists qq. iFrame. iPureIntro.
by rewrite (comm _ qφ0).
- iDestruct "Hq" as (q') "[% Hq'κ]". iRight. iExists (qq + q')%Qp.
- iFrame. iPureIntro.
- rewrite assoc (comm _ _ qq). done.
+ iSplitR; last first. { iApply fractional_split. iFrame. }
+ iPureIntro. rewrite assoc (comm _ _ qq). done.
Qed.
Lemma frac_bor_acc' E q κ :
@@ -129,7 +129,8 @@ Section frac_bor.
iMod (at_bor_acc_tok with "LFT Hshr Hκ1") as "[H Hclose']"; try done.
iDestruct (frac_bor_trade1 with "Hφ [$H $Hown $Hqφ]") as "[H >Hκ3]".
iMod ("Hclose'" with "H") as "Hκ1".
- iApply "Hclose". iFrame "Hκ1". rewrite Hq. iFrame.
+ iApply "Hclose". iApply fractional_half. iFrame "Hκ1". rewrite Hq.
+ iApply fractional_split. iFrame.
Qed.
Lemma frac_bor_acc E q κ `{!Fractional φ} :
@@ -154,7 +155,7 @@ Section frac_bor.
Qed.
End frac_bor.
-Lemma frac_bor_lft_incl `{!invG Σ, !lftG Σ, !frac_borG Σ} κ κ' q:
+Lemma frac_bor_lft_incl `{!invGS Σ, !lftGS Σ, !frac_borG Σ} κ κ' q:
lft_ctx -∗ &frac{κ}(λ q', (q * q').[κ']) -∗ κ ⊑ κ'.
Proof.
iIntros "#LFT#Hbor". iApply lft_incl_intro. iModIntro. iSplitR.
diff --git a/theories/lifetime/lifetime.v b/theories/lifetime/lifetime.v
index 47b85f69..a184733f 100644
--- a/theories/lifetime/lifetime.v
+++ b/theories/lifetime/lifetime.v
@@ -30,12 +30,12 @@ Instance lft_inhabited : Inhabited lft := populate static.
Canonical lftO := leibnizO lft.
-Definition lft_equiv `{!invG Σ, !lftG Σ} (κ κ':lft) : iProp Σ :=
+Definition lft_equiv `{!invGS Σ, !lftGS Σ} (κ κ':lft) : iProp Σ :=
κ ⊑ κ' ∗ κ' ⊑ κ.
Infix "≡ₗ" := lft_equiv (at level 70) : bi_scope.
Section derived.
-Context `{!invG Σ, !lftG Σ}.
+Context `{!invGS Σ, !lftGS Σ}.
Implicit Types κ : lft.
(* Deriving this just to prove that it can be derived.
diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index 36cff762..5f94a63c 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -3,6 +3,7 @@ From stdpp Require Export gmultiset strings.
From iris.base_logic.lib Require Export invariants.
From iris.base_logic.lib Require Import boxes.
From iris.bi Require Import fractional.
+From iris.proofmode Require Import proofmode.
Set Default Proof Using "Type".
Definition lftN : namespace := nroot .@ "lft".
@@ -14,29 +15,29 @@ Module Type lifetime_sig.
(** CMRAs needed by the lifetime logic *)
(* We can't instantie the module parameters with inductive types, so we
have aliases here. *)
- Parameter lftG' : gFunctors → Set.
- Global Notation lftG := lftG'.
- Existing Class lftG'.
- Parameter lftPreG' : gFunctors → Set.
- Global Notation lftPreG := lftPreG'.
- Existing Class lftPreG'.
+ Parameter lftGS' : gFunctors → Set.
+ Global Notation lftGS := lftGS'.
+ Existing Class lftGS'.
+ Parameter lftGpreS' : gFunctors → Set.
+ Global Notation lftGpreS := lftGpreS'.
+ Existing Class lftGpreS'.
(** Definitions *)
Parameter lft : Type.
Parameter static : lft.
Declare Instance lft_intersect : Meet lft.
- Parameter lft_ctx : ∀ `{!invG Σ, !lftG Σ}, iProp Σ.
+ Parameter lft_ctx : ∀ `{!invGS Σ, !lftGS Σ}, iProp Σ.
- Parameter lft_tok : ∀ `{!lftG Σ} (q : Qp) (κ : lft), iProp Σ.
- Parameter lft_dead : ∀ `{!lftG Σ} (κ : lft), iProp Σ.
+ Parameter lft_tok : ∀ `{!lftGS Σ} (q : Qp) (κ : lft), iProp Σ.
+ Parameter lft_dead : ∀ `{!lftGS Σ} (κ : lft), iProp Σ.
- Parameter lft_incl : ∀ `{!invG Σ, !lftG Σ} (κ κ' : lft), iProp Σ.
- Parameter bor : ∀ `{!invG Σ, !lftG Σ} (κ : lft) (P : iProp Σ), iProp Σ.
+ Parameter lft_incl : ∀ `{!invGS Σ, !lftGS Σ} (κ κ' : lft), iProp Σ.
+ Parameter bor : ∀ `{!invGS Σ, !lftGS Σ} (κ : lft) (P : iProp Σ), iProp Σ.
Parameter bor_idx : Type.
- Parameter idx_bor_own : ∀ `{!lftG Σ} (q : frac) (i : bor_idx), iProp Σ.
- Parameter idx_bor : ∀ `{!invG Σ, !lftG Σ} (κ : lft) (i : bor_idx) (P : iProp Σ), iProp Σ.
+ Parameter idx_bor_own : ∀ `{!lftGS Σ} (q : frac) (i : bor_idx), iProp Σ.
+ Parameter idx_bor : ∀ `{!invGS Σ, !lftGS Σ} (κ : lft) (i : bor_idx) (P : iProp Σ), iProp Σ.
(** Notation *)
Notation "q .[ κ ]" := (lft_tok q κ)
@@ -49,7 +50,7 @@ Module Type lifetime_sig.
Infix "⊑" := lft_incl (at level 70) : bi_scope.
Section properties.
- Context `{!invG Σ, !lftG Σ}.
+ Context `{!invGS Σ, !lftGS Σ}.
(** Instances *)
Global Declare Instance lft_inhabited : Inhabited lft.
@@ -84,9 +85,16 @@ Module Type lifetime_sig.
Global Declare Instance lft_tok_fractional κ : Fractional (λ q, q.[κ])%I.
Global Declare Instance lft_tok_as_fractional κ q :
AsFractional q.[κ] (λ q, q.[κ])%I q.
+ Global Declare Instance frame_lft_tok p κ q1 q2 RES :
+ FrameFractionalHyps p q1.[κ] (λ q, q.[κ])%I RES q1 q2 →
+ Frame p q1.[κ] q2.[κ] RES | 5.
+
Global Declare Instance idx_bor_own_fractional i : Fractional (λ q, idx_bor_own q i)%I.
Global Declare Instance idx_bor_own_as_fractional i q :
AsFractional (idx_bor_own q i) (λ q, idx_bor_own q i)%I q.
+ Global Declare Instance frame_idx_bor_own p i q1 q2 RES :
+ FrameFractionalHyps p (idx_bor_own q1 i) (λ q, idx_bor_own q i)%I RES q1 q2 →
+ Frame p (idx_bor_own q1 i) (idx_bor_own q2 i) RES | 5.
(** Laws *)
Parameter lft_tok_sep : ∀ q κ1 κ2, q.[κ1] ∗ q.[κ2] ⊣⊢ q.[κ1 ⊓ κ2].
@@ -158,8 +166,8 @@ Module Type lifetime_sig.
End properties.
Parameter lftΣ : gFunctors.
- Global Declare Instance subG_lftPreG Σ : subG lftΣ Σ → lftPreG Σ.
+ Global Declare Instance subG_lftGpreS Σ : subG lftΣ Σ → lftGpreS Σ.
- Parameter lft_init : ∀ `{!invG Σ, !lftPreG Σ} E, ↑lftN ⊆ E →
- ⊢ |={E}=> ∃ _ : lftG Σ, lft_ctx.
+ Parameter lft_init : ∀ `{!invGS Σ, !lftGpreS Σ} E, ↑lftN ⊆ E →
+ ⊢ |={E}=> ∃ _ : lftGS Σ, lft_ctx.
End lifetime_sig.
diff --git a/theories/lifetime/model/accessors.v b/theories/lifetime/model/accessors.v
index dab4be3c..ff73ee32 100644
--- a/theories/lifetime/model/accessors.v
+++ b/theories/lifetime/model/accessors.v
@@ -5,7 +5,7 @@ From iris.base_logic.lib Require Import boxes.
Set Default Proof Using "Type".
Section accessors.
-Context `{!invG Σ, !lftG Σ}.
+Context `{!invGS Σ, !lftGS Σ}.
Implicit Types κ : lft.
(* Helper internal lemmas *)
@@ -28,7 +28,7 @@ Proof.
by apply (exclusive_local_update _ (1%Qp, to_agree (Bor_open q))). }
rewrite own_bor_op -fmap_insert. iDestruct "Hbor" as "[Hown $]".
iExists _. iFrame "∗".
- rewrite -insert_delete big_sepM_insert ?lookup_delete // big_sepM_delete /=; last done.
+ rewrite -insert_delete_insert big_sepM_insert ?lookup_delete // big_sepM_delete /=; last done.
iDestruct "HB" as "[_ $]". auto.
Qed.
@@ -51,7 +51,7 @@ Proof.
rewrite own_bor_op -fmap_insert. iDestruct "Hbor" as "[Hown $]".
rewrite big_sepM_delete //. simpl. iDestruct "HB" as "[>$ HB]".
iExists _. iFrame "Hbox Hown".
- rewrite -insert_delete big_sepM_insert ?lookup_delete //. simpl. by iFrame.
+ rewrite -insert_delete_insert big_sepM_insert ?lookup_delete //. simpl. by iFrame.
Qed.
Lemma add_vs Pb Pb' P Q Pi κ :
diff --git a/theories/lifetime/model/borrow.v b/theories/lifetime/model/borrow.v
index 03ff321d..d12f215b 100644
--- a/theories/lifetime/model/borrow.v
+++ b/theories/lifetime/model/borrow.v
@@ -6,7 +6,7 @@ From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
Section borrow.
-Context `{!invG Σ, !lftG Σ}.
+Context `{!invGS Σ, !lftGS Σ}.
Implicit Types κ : lft.
Lemma raw_bor_create E κ P :
diff --git a/theories/lifetime/model/borrow_sep.v b/theories/lifetime/model/borrow_sep.v
index 3a4348e8..c961c617 100644
--- a/theories/lifetime/model/borrow_sep.v
+++ b/theories/lifetime/model/borrow_sep.v
@@ -6,7 +6,7 @@ From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
Section borrow.
-Context `{!invG Σ, !lftG Σ}.
+Context `{!invGS Σ, !lftGS Σ}.
Implicit Types κ : lft.
Lemma bor_sep E κ P Q :
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index bf215b53..f6e00a1b 100644
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -6,7 +6,7 @@ From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
Section creation.
-Context `{!invG Σ, !lftG Σ}.
+Context `{!invGS Σ, !lftGS Σ}.
Implicit Types κ : lft.
Lemma lft_kill (I : gmap lft lft_names) (K K' : gset lft) (κ : lft) :
@@ -125,7 +125,7 @@ Proof.
iModIntro. rewrite /lft_inv. iIntros (κ ?) "[[Hκ %]|[Hκ %]]".
- iLeft. iFrame "Hκ". iPureIntro. by apply lft_alive_in_insert.
- iRight. iFrame "Hκ". iPureIntro. by apply lft_dead_in_insert. }
- iModIntro; iExists {[ Λ ]}.
+ iModIntro; iExists {[+ Λ +]}.
rewrite {1}/lft_tok big_sepMS_singleton. iFrame "HΛ".
clear I A HΛ. iIntros "!> HΛ".
iApply (step_fupd_mask_mono (↑lftN ∪ ↑lft_userN) _ ((↑lftN ∪ ↑lft_userN)∖↑mgmtN)).
@@ -134,8 +134,6 @@ Proof.
set_solver. }
{ done. }
iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
- { (* FIXME solve_ndisj should really handle this... *)
- assert (↑mgmtN ⊆ ↑lftN) by solve_ndisj. set_solver. }
rewrite /lft_tok big_sepMS_singleton.
iDestruct (own_valid_2 with "HA HΛ")
as %[[s [?%leibniz_equiv ?]]%singleton_included_l _]%auth_both_valid_discrete.
@@ -172,7 +170,7 @@ Proof.
split; last done. by eapply gmultiset_elem_of_subseteq. }
{ intros κ ???. rewrite elem_of_difference elem_of_filter elem_of_dom. auto. }
iModIntro. iMod ("Hclose" with "[-]") as "_"; last first.
- { iModIntro. rewrite /lft_dead. iExists Λ. rewrite elem_of_singleton. auto. }
+ { iModIntro. rewrite /lft_dead. iExists Λ. rewrite gmultiset_elem_of_singleton. auto. }
iNext. iExists (<[Λ:=false]>A), I.
rewrite /own_alft_auth /to_alftUR fmap_insert. iFrame "HA HI".
rewrite HI !big_sepS_union //.
diff --git a/theories/lifetime/model/definitions.v b/theories/lifetime/model/definitions.v
index bbd57d69..fcb5f0fc 100644
--- a/theories/lifetime/model/definitions.v
+++ b/theories/lifetime/model/definitions.v
@@ -38,7 +38,7 @@ Definition ilftUR := gmapUR lft (agreeR lft_namesO).
Definition borUR := gmapUR slice_name (prodR fracR (agreeR bor_stateO)).
Definition inhUR := gset_disjUR slice_name.
-Class lftG Σ := LftG {
+Class lftGS Σ := LftG {
lft_box :> boxG Σ;
alft_inG :> inG Σ (authR alftUR);
alft_name : gname;
@@ -48,9 +48,9 @@ Class lftG Σ := LftG {
lft_cnt_inG :> inG Σ (authR natUR);
lft_inh_inG :> inG Σ (authR inhUR);
}.
-Definition lftG' := lftG.
+Definition lftGS' := lftGS.
-Class lftPreG Σ := LftPreG {
+Class lftGpreS Σ := LftGPreS {
lft_preG_box :> boxG Σ;
alft_preG_inG :> inG Σ (authR alftUR);
ilft_preG_inG :> inG Σ (authR ilftUR);
@@ -58,13 +58,13 @@ Class lftPreG Σ := LftPreG {
lft_preG_cnt_inG :> inG Σ (authR natUR);
lft_preG_inh_inG :> inG Σ (authR inhUR);
}.
-Definition lftPreG' := lftPreG.
+Definition lftGpreS' := lftGpreS.
Definition lftΣ : gFunctors :=
#[ boxΣ; GFunctor (authR alftUR); GFunctor (authR ilftUR);
GFunctor (authR borUR); GFunctor (authR natUR); GFunctor (authR inhUR) ].
-Instance subG_lftPreG Σ :
- subG lftΣ Σ → lftPreG Σ.
+Instance subG_lftGpreS Σ :
+ subG lftΣ Σ → lftGpreS Σ.
Proof. solve_inG. Qed.
Definition bor_filled (s : bor_state) : bool :=
@@ -77,7 +77,7 @@ Definition to_ilftUR : gmap lft lft_names → ilftUR := fmap to_agree.
Definition to_borUR : gmap slice_name bor_state → borUR := fmap ((1%Qp,.) ∘ to_agree).
Section defs.
- Context `{!invG Σ, !lftG Σ}.
+ Context `{!invGS Σ, !lftGS Σ}.
Definition lft_tok (q : Qp) (κ : lft) : iProp Σ :=
([∗ mset] Λ ∈ κ, own alft_name (◯ {[ Λ := Cinl q ]}))%I.
@@ -221,7 +221,7 @@ Typeclasses Opaque lft_tok lft_dead bor_cnt lft_bor_alive lft_bor_dead
idx_bor_own idx_bor raw_bor bor.
Section basic_properties.
-Context `{!invG Σ, !lftG Σ}.
+Context `{!invGS Σ, !lftGS Σ}.
Implicit Types κ : lft.
(* Unfolding lemmas *)
diff --git a/theories/lifetime/model/faking.v b/theories/lifetime/model/faking.v
index 101ca0ee..94b0f796 100644
--- a/theories/lifetime/model/faking.v
+++ b/theories/lifetime/model/faking.v
@@ -5,7 +5,7 @@ From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
Section faking.
-Context `{!invG Σ, !lftG Σ}.
+Context `{!invGS Σ, !lftGS Σ}.
Implicit Types κ : lft.
Lemma ilft_create A I κ :
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index a5c38259..547d293a 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -7,7 +7,7 @@ Set Default Proof Using "Type".
Import uPred.
Section primitive.
-Context `{!invG Σ, !lftG Σ}.
+Context `{!invGS Σ, !lftGS Σ}.
Implicit Types κ : lft.
Lemma to_borUR_included (B : gmap slice_name bor_state) i s q :
@@ -18,8 +18,8 @@ Proof.
by move=> /Some_pair_included [_] /Some_included_total /to_agree_included=>->.
Qed.
-Lemma lft_init `{!lftPreG Σ} E :
- ↑lftN ⊆ E → ⊢ |={E}=> ∃ _ : lftG Σ, lft_ctx.
+Lemma lft_init `{!lftGpreS Σ} E :
+ ↑lftN ⊆ E → ⊢ |={E}=> ∃ _ : lftGS Σ, lft_ctx.
Proof.
iIntros (?). rewrite /lft_ctx.
iMod (own_alloc (● ∅ : authR alftUR)) as (γa) "Ha"; first by apply auth_auth_valid.
@@ -300,9 +300,18 @@ Proof.
intros p q. rewrite /idx_bor_own -own_bor_op /own_bor. f_equiv=>?.
rewrite -auth_frag_op singleton_op -pair_op agree_idemp. done.
Qed.
+Global Instance frame_lft_tok p κ q1 q2 RES :
+ FrameFractionalHyps p q1.[κ] (λ q, q.[κ])%I RES q1 q2 →
+ Frame p q1.[κ] q2.[κ] RES | 5.
+Proof. apply: frame_fractional. Qed.
+
Global Instance idx_bor_own_as_fractional i q :
AsFractional (idx_bor_own q i) (λ q, idx_bor_own q i)%I q.
Proof. split. done. apply _. Qed.
+Global Instance frame_idx_bor_own p i q1 q2 RES :
+ FrameFractionalHyps p (idx_bor_own q1 i) (λ q, idx_bor_own q i)%I RES q1 q2 →
+ Frame p (idx_bor_own q1 i) (idx_bor_own q2 i) RES | 5.
+Proof. apply: frame_fractional. Qed.
(** Lifetime inclusion *)
Lemma lft_incl_acc E κ κ' q :
@@ -357,7 +366,8 @@ Proof.
iIntros "Hκ Hκ'".
destruct (Qp_lower_bound q q') as (qq & q0 & q'0 & -> & ->).
iExists qq. rewrite -lft_tok_sep.
- iDestruct "Hκ" as "[$$]". iDestruct "Hκ'" as "[$$]". auto.
+ iDestruct "Hκ" as "[$ Hκ]". iDestruct "Hκ'" as "[$ Hκ']".
+ iIntros "[Hκ+ Hκ'+]". iSplitL "Hκ Hκ+"; iApply fractional_split; iFrame.
Qed.
Lemma lft_incl_glb κ κ' κ'' : κ ⊑ κ' -∗ κ ⊑ κ'' -∗ κ ⊑ κ' ⊓ κ''.
@@ -369,7 +379,9 @@ Proof.
iDestruct (lft_intersect_acc with "Hκ' Hκ''") as (qq) "[Hqq Hclose]".
iExists qq. iFrame. iIntros "!> Hqq".
iDestruct ("Hclose" with "Hqq") as "[Hκ' Hκ'']".
- iMod ("Hclose'" with "Hκ'") as "$". by iApply "Hclose''".
+ iMod ("Hclose'" with "Hκ'") as "?".
+ iMod ("Hclose''" with "Hκ''") as "?". iModIntro.
+ iApply fractional_half. iFrame.
- rewrite -lft_dead_or. iIntros "[H†|H†]". by iApply "H1†". by iApply "H2†".
Qed.
diff --git a/theories/lifetime/model/reborrow.v b/theories/lifetime/model/reborrow.v
index 721a53a4..d8f6d63e 100644
--- a/theories/lifetime/model/reborrow.v
+++ b/theories/lifetime/model/reborrow.v
@@ -5,7 +5,7 @@ From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
Section reborrow.
-Context `{!invG Σ, !lftG Σ}.
+Context `{!invGS Σ, !lftGS Σ}.
Implicit Types κ : lft.
(* Notice that taking lft_inv for both κ and κ' already implies
@@ -49,7 +49,7 @@ Proof.
rewrite /to_borUR !fmap_insert. iFrame "Hbox HB●".
iDestruct (@big_sepM_delete with "HB") as "[_ HB]"; first done.
rewrite (big_sepM_delete _ (<[_:=_]>_) i); last by rewrite lookup_insert.
- rewrite -insert_delete delete_insert ?lookup_delete //=. iFrame; auto. }
+ rewrite -insert_delete_insert delete_insert ?lookup_delete //=. iFrame; auto. }
clear B HB Pb' Pi'.
rewrite {1}/lft_bor_alive. iDestruct "Hκalive'" as (B) "(Hbox & >HB● & HB)".
iMod (slice_insert_full _ _ true with "HP Hbox")
@@ -93,7 +93,7 @@ Proof.
iIntros (_). rewrite lft_inv_alive_unfold.
iExists Pb', Pi'. iFrame "Hvs' Hinh". rewrite /lft_bor_alive.
iExists (<[i:=Bor_in]>B'). rewrite /to_borUR !fmap_insert. iFrame.
- rewrite -insert_delete big_sepM_insert ?lookup_delete //=. by iFrame. }
+ rewrite -insert_delete_insert big_sepM_insert ?lookup_delete //=. by iFrame. }
iModIntro. rewrite -[S n]Nat.add_1_l -nat_op auth_frag_op own_cnt_op.
by iFrame.
Qed.
@@ -135,7 +135,7 @@ Proof.
as (Pb'') "HH"; [solve_ndisj|done|done| | |].
{ rewrite /lft_bor_alive (big_sepM_delete _ B i') //. iDestruct "HB" as "[_ HB]".
iExists (delete i' B). rewrite -fmap_delete. iFrame.
- rewrite fmap_delete -insert_delete delete_insert ?lookup_delete //=. }
+ rewrite fmap_delete -insert_delete_insert delete_insert ?lookup_delete //=. }
{ iNext. iApply (lft_vs_cons with "[] Hvs"). iIntros "[??] _ !>". iNext.
iRewrite "HeqPb'". iFrame. by iApply "HP'". }
iDestruct "HH" as "([HI Hinvκ] & $ & Halive & Hvs)".
diff --git a/theories/lifetime/na_borrow.v b/theories/lifetime/na_borrow.v
index 81816c74..f9b5932e 100644
--- a/theories/lifetime/na_borrow.v
+++ b/theories/lifetime/na_borrow.v
@@ -3,7 +3,7 @@ From iris.base_logic.lib Require Export na_invariants.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
-Definition na_bor `{!invG Σ, !lftG Σ, !na_invG Σ}
+Definition na_bor `{!invGS Σ, !lftGS Σ, !na_invG Σ}
(κ : lft) (tid : na_inv_pool_name) (N : namespace) (P : iProp Σ) :=
(∃ i, &{κ,i}P ∗ na_inv tid N (idx_bor_own 1 i))%I.
@@ -11,7 +11,7 @@ Notation "&na{ κ , tid , N }" := (na_bor κ tid N)
(format "&na{ κ , tid , N }") : bi_scope.
Section na_bor.
- Context `{!invG Σ, !lftG Σ, !na_invG Σ}
+ Context `{!invGS Σ, !lftGS Σ, !na_invG Σ}
(tid : na_inv_pool_name) (N : namespace) (P : iProp Σ).
Global Instance na_bor_ne κ n : Proper (dist n ==> dist n) (na_bor κ tid N).
diff --git a/theories/prophecy/prophecy.v b/theories/prophecy/prophecy.v
index 00b9dae5..6c4ac900 100644
--- a/theories/prophecy/prophecy.v
+++ b/theories/prophecy/prophecy.v
@@ -2,7 +2,7 @@ Import EqNotations.
From stdpp Require Import strings.
From iris.algebra Require Import auth cmra functions gmap csum frac agree.
From iris.bi Require Import fractional.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
From iris.base_logic Require Import invariants.
From lrust.util Require Import basic vector discrete_fun.
From lrust.prophecy Require Export syn_type.
@@ -201,7 +201,7 @@ Local Definition proph_sim (S: proph_smryUR) (L: proph_log) :=
Local Notation "S :~ L" := (proph_sim S L) (at level 70, format "S :~ L").
Section defs.
-Context `{!invG Σ, !prophG Σ}.
+Context `{!invGS Σ, !prophG Σ}.
(** Prophecy Context *)
Local Definition proph_inv: iProp Σ :=
@@ -231,7 +231,7 @@ Notation "⟨ π , φ ⟩" := (proph_obs (λ π, φ%type%stdpp))
(** * Iris Lemmas *)
Section proph.
-Context `{!invG Σ, !prophG Σ}.
+Context `{!invGS Σ, !prophG Σ}.
(** Instances *)
@@ -245,9 +245,17 @@ Proof.
Qed.
Global Instance proph_tok_as_fractional q ξ : AsFractional q:[ξ] (λ q, q:[ξ]%I) q.
Proof. split; by [|apply _]. Qed.
+Global Instance frame_proph_tok p ξ q1 q2 RES :
+ FrameFractionalHyps p q1:[ξ] (λ q, q:[ξ])%I RES q1 q2 →
+ Frame p q1:[ξ] q2:[ξ] RES | 5.
+Proof. apply: frame_fractional. Qed.
Global Instance proph_toks_as_fractional q ξl : AsFractional q:+[ξl] (λ q, q:+[ξl]%I) q.
Proof. split; by [|apply _]. Qed.
+Global Instance frame_proph_toks p ξl q1 q2 RES :
+ FrameFractionalHyps p q1:+[ξl] (λ q, q:+[ξl])%I RES q1 q2 →
+ Frame p q1:+[ξl] q2:+[ξl] RES | 5.
+Proof. apply: frame_fractional. Qed.
Global Instance proph_obs_persistent φπ : Persistent .⟨φπ⟩ := _.
Global Instance proph_obs_timeless φπ : Timeless .⟨φπ⟩ := _.
@@ -272,8 +280,9 @@ Lemma proph_tok_combine ξl ζl q q' :
q:+[ξl] -∗ q':+[ζl] -∗
∃q'', q'':+[ξl ++ ζl] ∗ (q'':+[ξl ++ ζl] -∗ q:+[ξl] ∗ q':+[ζl]).
Proof.
- case (Qp_lower_bound q q')=> [q''[?[?[->->]]]]. iIntros "[ξl $][ζl $]".
- iExists q''. iIntros "{$ξl $ζl}[$$]".
+ case (Qp_lower_bound q q')=> [q''[?[?[->->]]]]. iIntros "[ξl ξl'][ζl ζl']".
+ iExists q''. iFrame "ξl ζl". iIntros "[ξl ζl]".
+ iSplitL "ξl ξl'"; iApply fractional_split; iFrame.
Qed.
(** Initialization *)
@@ -425,13 +434,13 @@ Global Opaque proph_ctx proph_tok proph_obs.
(** * Prophecy Equalizer *)
-Definition proph_eqz `{!invG Σ, !prophG Σ} {A} (uπ vπ: proph A) : iProp Σ :=
+Definition proph_eqz `{!invGS Σ, !prophG Σ} {A} (uπ vπ: proph A) : iProp Σ :=
∀E ξl q, ⌜↑prophN ⊆ E ∧ vπ ./ ξl⌝ -∗ q:+[ξl] ={E}=∗ ⟨π, uπ π = vπ π⟩ ∗ q:+[ξl].
Notation "uπ :== vπ" := (proph_eqz uπ vπ) (at level 70, format "uπ :== vπ") : bi_scope.
Section proph_eqz.
-Context `{!invG Σ, !prophG Σ}.
+Context `{!invGS Σ, !prophG Σ}.
(** ** Constructing Prophecy Equalizers *)
diff --git a/theories/prophecy/syn_type.v b/theories/prophecy/syn_type.v
index d4a75ce7..bad469b8 100644
--- a/theories/prophecy/syn_type.v
+++ b/theories/prophecy/syn_type.v
@@ -62,7 +62,7 @@ Proof.
try (by split; [move=> ->|move=> [=]]);
by split; [move=> [->->]|move=> [=]].
Qed.
-Instance syn_type_beq_dec: EqDecision syn_type.
+Global Instance syn_type_beq_dec: EqDecision syn_type.
Proof.
refine (λ 𝔄 𝔅, cast_if (decide (syn_type_beq 𝔄 𝔅)));
by rewrite -syn_type_eq_correct.
diff --git a/theories/typing/array.v b/theories/typing/array.v
index c0b3da4e..9fbe383c 100644
--- a/theories/typing/array.v
+++ b/theories/typing/array.v
@@ -156,12 +156,12 @@ Section typing.
Qed.
Lemma array_plus_prod {𝔄} m n (ty: type 𝔄) E L :
- eqtype E L [ty;^ m + n] ([ty;^ m] * [ty;^ n]) (vsepat m) (curry vapp).
+ eqtype E L [ty;^ m + n] ([ty;^ m] * [ty;^ n]) (vsepat m) (uncurry vapp).
Proof.
apply eqtype_symm, eqtype_unfold; [apply _|]. iIntros (?) "_!>_".
iSplit; [iPureIntro=>/=; lia|]. iSplit.
{ rewrite/= lft_intersect_list_app. iApply lft_intersect_equiv_idemp. }
- have Eq: ∀vπ: proph (vec 𝔄 _ * _), vfunsep (curry vapp ∘ vπ) =
+ have Eq: ∀vπ: proph (vec 𝔄 _ * _), vfunsep (uncurry vapp ∘ vπ) =
vfunsep (fst ∘ vπ) +++ vfunsep (snd ∘ vπ).
{ move=> ?? vπ. have {1}<-: pair ∘ vapply (vfunsep $ fst ∘ vπ) ⊛
vapply (vfunsep $ snd ∘ vπ) = vπ by rewrite !semi_iso' -surjective_pairing_fun.
@@ -179,7 +179,7 @@ Section typing.
Qed.
Lemma array_succ_prod {𝔄} n (ty: type 𝔄) E L :
- eqtype E L [ty;^ S n] (ty * [ty;^ n]) (λ v, (vhd v, vtl v)) (curry (λ x, vcons x)).
+ eqtype E L [ty;^ S n] (ty * [ty;^ n]) (λ v, (vhd v, vtl v)) (uncurry (λ x, vcons x)).
Proof.
eapply eqtype_eq.
- eapply eqtype_trans; [apply (array_plus_prod 1)|].
diff --git a/theories/typing/array_util.v b/theories/typing/array_util.v
index 398bfbdc..093beb94 100644
--- a/theories/typing/array_util.v
+++ b/theories/typing/array_util.v
@@ -47,7 +47,7 @@ Section array_util.
Qed.
Lemma ty_share_big_sepL {𝔄} (ty: type 𝔄) E aπl d κ l tid q :
- ↑lftN ⊆ E → lft_ctx -∗ κ ⊑ ty.(ty_lft) -∗
+ ↑lftN ⊆ E → lft_ctx -∗ κ ⊑ ty_lft ty -∗
&{κ} ([∗ list] i ↦ aπ ∈ aπl, (l +ₗ[ty] i) ↦∗: ty.(ty_own) aπ d tid) -∗ q.[κ]
={E}=∗ |={E}▷=>^d |={E}=>
([∗ list] i ↦ aπ ∈ aπl, ty.(ty_shr) aπ d κ tid (l +ₗ[ty] i)) ∗ q.[κ].
@@ -64,7 +64,7 @@ Section array_util.
Qed.
Lemma ty_own_proph_big_sepL {𝔄} (ty: type 𝔄) n E (aπl: vec _ n) wll d tid κ q :
- ↑lftN ⊆ E → lft_ctx -∗ κ ⊑ ty.(ty_lft) -∗
+ ↑lftN ⊆ E → lft_ctx -∗ κ ⊑ ty_lft ty -∗
([∗ list] i ↦ aπwl ∈ vzip aπl wll, ty.(ty_own) aπwl.1 d tid aπwl.2) -∗ q.[κ]
={E}=∗ |={E}▷=>^d |={E}=> ∃ξl q', ⌜vapply aπl ./ ξl⌝ ∗ q':+[ξl] ∗
(q':+[ξl] ={E}=∗
@@ -85,7 +85,7 @@ Section array_util.
Qed.
Lemma ty_own_proph_big_sepL_mt {𝔄} (ty: type 𝔄) n E (aπl: vec _ n) l d tid κ q :
- ↑lftN ⊆ E → lft_ctx -∗ κ ⊑ ty.(ty_lft) -∗
+ ↑lftN ⊆ E → lft_ctx -∗ κ ⊑ ty_lft ty -∗
([∗ list] i ↦ aπ ∈ aπl, (l +ₗ[ty] i) ↦∗: ty.(ty_own) aπ d tid) -∗ q.[κ]
={E}=∗ |={E}▷=>^d |={E}=> ∃ξl q', ⌜vapply aπl ./ ξl⌝ ∗ q':+[ξl] ∗
(q':+[ξl] ={E}=∗
@@ -100,7 +100,7 @@ Section array_util.
Qed.
Lemma ty_shr_proph_big_sepL {𝔄} (ty: type 𝔄) n E (aπl: vec _ n) d κ tid l κ' q :
- ↑lftN ⊆ E → lft_ctx -∗ κ' ⊑ κ -∗ κ' ⊑ ty.(ty_lft) -∗
+ ↑lftN ⊆ E → lft_ctx -∗ κ' ⊑ κ -∗ κ' ⊑ ty_lft ty -∗
([∗ list] i ↦ aπ ∈ aπl, ty.(ty_shr) aπ d κ tid (l +ₗ[ty] i)) -∗ q.[κ']
={E}▷=∗ |={E}▷=>^d |={E}=> ∃ξl q', ⌜vapply aπl ./ ξl⌝ ∗ q':+[ξl] ∗
(q':+[ξl] ={E}=∗ q.[κ']).
diff --git a/theories/typing/cont_context.v b/theories/typing/cont_context.v
index fac14295..a431a62d 100644
--- a/theories/typing/cont_context.v
+++ b/theories/typing/cont_context.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
From lrust.lang Require Import notation.
From lrust.typing Require Import type lft_contexts type_context.
Set Default Proof Using "Type".
diff --git a/theories/typing/examples/get_x.v b/theories/typing/examples/get_x.v
index 94e8665e..c8348721 100644
--- a/theories/typing/examples/get_x.v
+++ b/theories/typing/examples/get_x.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
From lrust.typing Require Import typing.
Set Default Proof Using "Type".
diff --git a/theories/typing/examples/inc_vec.v b/theories/typing/examples/inc_vec.v
index 5f806925..3fb3fb67 100644
--- a/theories/typing/examples/inc_vec.v
+++ b/theories/typing/examples/inc_vec.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
From lrust.typing Require Export type.
From lrust.typing Require Import typing.
From lrust.typing.lib.vec Require Import vec vec_slice.
diff --git a/theories/typing/examples/init_prod.v b/theories/typing/examples/init_prod.v
index 53268f2c..b4a50aaa 100644
--- a/theories/typing/examples/init_prod.v
+++ b/theories/typing/examples/init_prod.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
From lrust.typing Require Import typing.
Set Default Proof Using "Type".
diff --git a/theories/typing/examples/lazy_lft.v b/theories/typing/examples/lazy_lft.v
index f0b562f2..4a177600 100644
--- a/theories/typing/examples/lazy_lft.v
+++ b/theories/typing/examples/lazy_lft.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
From lrust.typing Require Import typing.
Set Default Proof Using "Type".
diff --git a/theories/typing/examples/nonlexical.v b/theories/typing/examples/nonlexical.v
index 9759813c..a543759a 100644
--- a/theories/typing/examples/nonlexical.v
+++ b/theories/typing/examples/nonlexical.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
From lrust.typing Require Import typing lib.option.
(* Typing "problem case #3" from:
diff --git a/theories/typing/examples/projection_toggle.v b/theories/typing/examples/projection_toggle.v
index 80c2cf7d..a3b72ae0 100644
--- a/theories/typing/examples/projection_toggle.v
+++ b/theories/typing/examples/projection_toggle.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
From lrust.typing Require Export type.
From lrust.typing Require Import typing.
Set Default Proof Using "Type".
diff --git a/theories/typing/examples/rebor.v b/theories/typing/examples/rebor.v
index f8a7eb7a..e23c30c4 100644
--- a/theories/typing/examples/rebor.v
+++ b/theories/typing/examples/rebor.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
From lrust.typing Require Import typing.
Set Default Proof Using "Type".
diff --git a/theories/typing/examples/unbox.v b/theories/typing/examples/unbox.v
index 82e11937..9b46ac8b 100644
--- a/theories/typing/examples/unbox.v
+++ b/theories/typing/examples/unbox.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
From lrust.typing Require Import typing.
Set Default Proof Using "Type".
diff --git a/theories/typing/fixpoint.v b/theories/typing/fixpoint.v
index b94ed7cf..db14e95c 100644
--- a/theories/typing/fixpoint.v
+++ b/theories/typing/fixpoint.v
@@ -13,9 +13,9 @@ Section S.
Definition Tn n := Nat.iter (S n) T base.
- Lemma Tn_ty_lft_const n n' : ⊢ (Tn n).(ty_lft) ≡ₗ (Tn n').(ty_lft).
+ Lemma Tn_ty_lft_const n n' : ⊢ ty_lft (Tn n) ≡ₗ ty_lft (Tn n').
Proof using HT.
- have Eq: ∀n, ⊢ (Tn n).(ty_lft) ≡ₗ (Tn 0).(ty_lft); last first.
+ have Eq: ∀n, ⊢ ty_lft (Tn n) ≡ₗ ty_lft (Tn 0); last first.
{ iApply lft_equiv_trans; [|iApply lft_equiv_sym]; iApply Eq. }
clear n n'=> n. case type_contractive_type_lft_morphism=> [> Hα ?|> Hα ?]; last first.
{ iApply lft_equiv_trans; [iApply Hα|]. iApply lft_equiv_sym. iApply Hα. }
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 7bab016a..cbabd1f0 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -383,7 +383,7 @@ Section typing.
move: Cl. rewrite Into. iIntros (? Body ?????) "_ _ _ _ _ $$ _ Obs".
iMod persistent_time_receipt_0 as "#⧖". iApply wp_value. iExists -[const tr].
iFrame "Obs". iSplit; [|done]. iLöb as "IH". iExists _, 0%nat.
- iSplit; [by rewrite/= decide_left|]. iFrame "⧖". iExists tr.
+ iSplit; [by rewrite/= decide_True_pi|]. iFrame "⧖". iExists tr.
iSplit; [done|]. iExists fb, "return", bl', e, _. iSplit; [done|].
iIntros "!>!> *%%% LFT TIME PROPH UNIQ Efp Na L C T ?".
iApply (Body _ _ (RecV _ _ _) $! _ (_-::_) with
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index 6e1ef5b3..685830cd 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -24,12 +24,12 @@ Notation llctx := (list llctx_elt).
Notation "κ ⊑ₗ κl" := (@pair lft (list lft) κ κl) (at level 55).
(* External lifetime context. *)
-Definition elctx_elt_interp `{!invG Σ, !lftG Σ} (x : elctx_elt) : iProp Σ :=
+Definition elctx_elt_interp `{!invGS Σ, !lftGS Σ} (x : elctx_elt) : iProp Σ :=
(x.1 ⊑ x.2)%I.
Notation elctx_interp := (big_sepL (λ _, elctx_elt_interp)).
Section lft_contexts.
- Context `{!invG Σ, !lftG Σ}.
+ Context `{!invGS Σ, !lftGS Σ}.
Implicit Type (κ: lft).
Global Instance elctx_interp_permut :
@@ -56,7 +56,7 @@ Section lft_contexts.
iDestruct "Hq" as (κ0) "(% & Hq & #?)".
iDestruct "Hq'" as (κ0') "(% & Hq' & #?)". simpl in *.
rewrite (inj ((lft_intersect_list κs) ⊓.) κ0' κ0); last congruence.
- iExists κ0. by iFrame "∗%".
+ iExists κ0. iFrame "∗%". done.
Qed.
Definition llctx_interp (L : llctx) (q : Qp) : iProp Σ :=
@@ -68,6 +68,11 @@ Section lft_contexts.
Global Instance llctx_interp_as_fractional L q :
AsFractional (llctx_interp L q) (llctx_interp L) q.
Proof. split. done. apply _. Qed.
+ Global Instance frame_llctx_interp p L q1 q2 RES :
+ FrameFractionalHyps p (llctx_interp L q1) (llctx_interp L) RES q1 q2 →
+ Frame p (llctx_interp L q1) (llctx_interp L q2) RES | 5.
+ Proof. apply: frame_fractional. Qed.
+
Global Instance llctx_interp_permut :
Proper ((≡ₚ) ==> eq ==> (⊣⊢)) llctx_interp.
Proof. intros ????? ->. by apply big_opL_permutation. Qed.
@@ -347,7 +352,7 @@ Arguments elctx_sat {_ _ _} _ _ _.
Arguments lctx_lft_incl_incl {_ _ _ _ _} _ _.
Arguments lctx_lft_alive_tok {_ _ _ _ _} _ _ _.
-Lemma elctx_sat_submseteq `{!invG Σ, !lftG Σ} E E' L :
+Lemma elctx_sat_submseteq `{!invGS Σ, !lftGS Σ} E E' L :
E' ⊆+ E → elctx_sat E L E'.
Proof. iIntros (HE' ?) "_ !> H". by iApply big_sepL_submseteq. Qed.
diff --git a/theories/typing/lib/arc.v b/theories/typing/lib/arc.v
index b89618e3..b6c1510d 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -25,7 +25,7 @@ Section arc.
(* We use this disjunction, and not simply [ty_shr] here, *)
(* because [weak_new] cannot prove ty_shr, even for a dead *)
(* lifetime. *)
- (ty.(ty_shr) (ν ⊓ ty.(ty_lft)) tid (l +ₗ 2) ∨ [†ν]) ∗
+ (ty.(ty_shr) (ν ⊓ ty_lft ty) tid (l +ₗ 2) ∨ [†ν]) ∗
□ (1.[ν] ={↑lftN ∪ ↑lft_userN ∪ ↑arc_endN}[↑lft_userN]▷=∗
[†ν] ∗ ▷ (l +ₗ 2) ↦∗: ty.(ty_own) tid ∗ † l…(2 + ty.(ty_size))))%I.
@@ -63,8 +63,8 @@ Section arc.
(∃ γ ν q, arc_persist tid ν γ l ty ∗ arc_tok γ q ∗ q.[ν])%I.
Lemma arc_own_share E l ty tid q :
↑lftN ⊆ E →
- lft_ctx -∗ (q).[ty.(ty_lft)] -∗ full_arc_own l ty tid
- ={E}=∗ (q).[ty.(ty_lft)] ∗ shared_arc_own l ty tid.
+ lft_ctx -∗ (q).[ty_lft ty] -∗ full_arc_own l ty tid
+ ={E}=∗ (q).[ty_lft ty] ∗ shared_arc_own l ty tid.
Proof.
iIntros (?) "#LFT Htok (Hl1 & Hl2 & H† & Hown)".
iMod (lft_create with "LFT") as (ν) "[Hν #Hν†]"=>//.
@@ -806,7 +806,7 @@ Section arc.
iAssert (shared_arc_own rc' ty tid ∗ llctx_interp [ϝ ⊑ₗ []] 1)%I
with "[>Hrc' HL]" as "[Hrc' HL]".
{ iDestruct "Hrc'" as "[?|$]"; last done.
- iMod (lctx_lft_alive_tok ty.(ty_lft) with "HE HL")
+ iMod (lctx_lft_alive_tok ty_lft ty with "HE HL")
as (?) "(Htok & HL & Hclose)"; [done| |].
{ change (ty_outlives_E (arc ty)) with (ty_outlives_E ty).
eapply (lctx_lft_alive_incl _ _ ϝ); first solve_typing.
@@ -921,7 +921,7 @@ Section arc.
iAssert (shared_arc_own rc' ty tid ∗ llctx_interp [ϝ ⊑ₗ []] 1)%I
with "[>Hrc' HL]" as "[Hrc' HL]".
{ iDestruct "Hrc'" as "[?|$]"; last done.
- iMod (lctx_lft_alive_tok ty.(ty_lft) with "HE HL")
+ iMod (lctx_lft_alive_tok ty_lft ty with "HE HL")
as (?) "(Htok & HL & Hclose)"; [done| |].
{ change (ty_outlives_E (arc ty)) with (ty_outlives_E ty).
eapply (lctx_lft_alive_incl _ _ ϝ); first solve_typing.
diff --git a/theories/typing/lib/diverging_static.v b/theories/typing/lib/diverging_static.v
index 1d09e83c..ccfd10c9 100644
--- a/theories/typing/lib/diverging_static.v
+++ b/theories/typing/lib/diverging_static.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
From lrust.typing Require Export type.
From lrust.typing Require Import typing.
Set Default Proof Using "Type".
diff --git a/theories/typing/lib/fake_shared.v b/theories/typing/lib/fake_shared.v
index ebaa3764..55c03115 100644
--- a/theories/typing/lib/fake_shared.v
+++ b/theories/typing/lib/fake_shared.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
From lrust.typing Require Import typing.
Set Default Proof Using "Type".
diff --git a/theories/typing/lib/join.v b/theories/typing/lib/join.v
index 8516d2db..321c75a9 100644
--- a/theories/typing/lib/join.v
+++ b/theories/typing/lib/join.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
From lrust.lang Require Import spawn.
From lrust.typing Require Export type.
From lrust.typing Require Import typing.
diff --git a/theories/typing/lib/mutex/mutex.v b/theories/typing/lib/mutex/mutex.v
index 146ffcdd..bbfc0d5b 100644
--- a/theories/typing/lib/mutex/mutex.v
+++ b/theories/typing/lib/mutex/mutex.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
From iris.algebra Require Import auth csum frac agree.
From lrust.lang.lib Require Import memcpy lock.
From lrust.lifetime Require Import na_borrow.
@@ -63,7 +63,7 @@ Section mutex.
ty_own Φπ _ tid vl := ∃Φ (b: bool) vl' (vπ: proph 𝔄) d,
⌜vl = #b :: vl' ∧ Φπ = const Φ⌝ ∗
⟨π, Φ (vπ π)⟩ ∗ ⧖(S d) ∗ ty.(ty_own) vπ d tid vl';
- ty_shr Φπ _ κ tid l := ∃Φ κ', ⌜Φπ = const Φ⌝ ∗ κ ⊑ κ' ∗ κ' ⊑ ty.(ty_lft) ∗
+ ty_shr Φπ _ κ tid l := ∃Φ κ', ⌜Φπ = const Φ⌝ ∗ κ ⊑ κ' ∗ κ' ⊑ ty_lft ty ∗
&at{κ, mutexN} (lock_proto l (mutex_body ty Φ κ' l tid));
|}%I.
Next Obligation.
diff --git a/theories/typing/lib/mutex/mutexguard.v b/theories/typing/lib/mutex/mutexguard.v
index 3f225436..4903e427 100644
--- a/theories/typing/lib/mutex/mutexguard.v
+++ b/theories/typing/lib/mutex/mutexguard.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
From iris.algebra Require Import auth csum frac agree.
From lrust.lang.lib Require Import memcpy lock.
From lrust.lifetime Require Import na_borrow.
@@ -46,11 +46,11 @@ Section mutexguard.
ty_size := 1; ty_lfts := κ :: ty.(ty_lfts); ty_E := ty.(ty_E) ++ ty_outlives_E ty κ;
(* One logical step is required for [ty_share] *)
ty_own Φπ d tid vl := ⌜d > 0⌝ ∗ [loc[l] := vl] ∃Φ κ',
- ⌜Φπ = const Φ⌝ ∗ κ ⊑ κ' ∗ κ' ⊑ ty.(ty_lft) ∗
+ ⌜Φπ = const Φ⌝ ∗ κ ⊑ κ' ∗ κ' ⊑ ty_lft ty ∗
&at{κ, mutexN} (lock_proto l (mutex_body ty Φ κ' l tid)) ∗
mutex_body ty Φ κ' l tid;
ty_shr Φπ _ κ' tid l := ∃Φ (l': loc) κᵢ (vπ: proph 𝔄) d,
- ⌜Φπ = const Φ⌝ ∗ κ' ⊑ κᵢ ∗ κᵢ ⊑ ty.(ty_lft) ∗
+ ⌜Φπ = const Φ⌝ ∗ κ' ⊑ κᵢ ∗ κᵢ ⊑ ty_lft ty ∗
&frac{κ'}(λ q', l ↦{q'} #l') ∗ ⟨π, Φ (vπ π)⟩ ∗ ⧖(S d) ∗
□ ∀E q, ⌜↑lftN ∪ ↑shrN ⊆ E⌝ -∗ q.[κᵢ]
={E,E∖↑shrN}=∗ |={E∖↑shrN}▷=>^(S d) |={E∖↑shrN,E}=>
@@ -87,7 +87,7 @@ Section mutexguard.
iMod (inv_alloc shrN _ (_ ∨ ty.(ty_shr) _ _ _ _ _)%I with "[Bor]") as "#inv".
{ iLeft. iNext. iExact "Bor". }
iModIntro. iFrame "κ'". iExists _, _, κᵢ, _, _. iSplit; [done|].
- iFrame "Bor↦ Obs ⧖ κ'⊑κᵢ". iAssert (κᵢ ⊑ ty.(ty_lft))%I as "#?".
+ iFrame "Bor↦ Obs ⧖ κ'⊑κᵢ". iAssert (κᵢ ⊑ ty_lft ty)%I as "#?".
{ iApply lft_incl_trans; [iApply lft_intersect_incl_l|done]. }
iSplit; [done|]. iIntros "!>" (???) "κᵢ".
iInv shrN as "[Bor|#ty]" "Close"; iIntros "/=!>!>!>"; last first.
@@ -131,7 +131,8 @@ Section mutexguard.
Global Instance mutexguard_send {𝔄} κ (ty: type 𝔄) :
Send ty → Send (mutexguard κ ty).
Proof.
- move=> ?>/=. rewrite /mutex_body. do 21 f_equiv; [|done]. by do 2 f_equiv.
+ move=> ?>/=. rewrite /mutex_body. do 21 (f_equiv || move=>?); [|done].
+ by do 2 f_equiv.
Qed.
(* In order to prove [mutexguard_resolve] with a non-trivial postcondition,
diff --git a/theories/typing/lib/panic.v b/theories/typing/lib/panic.v
index 972529d0..d5407276 100644
--- a/theories/typing/lib/panic.v
+++ b/theories/typing/lib/panic.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
From lrust.typing Require Import typing.
Set Default Proof Using "Type".
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index ccd2608e..989138bd 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
From iris.algebra Require Import auth csum frac agree excl numbers.
From lrust.lang.lib Require Import memcpy.
From lrust.lifetime Require Import na_borrow.
@@ -77,7 +77,7 @@ Section rc.
(* We use this disjunction, and not simply [ty_shr] here,
because [weak_new] cannot prove ty_shr, even for a dead
lifetime. *)
- (ty.(ty_shr) (ν ⊓ ty.(ty_lft)) tid (l +ₗ 2) ∨ [†ν]) ∗
+ (ty.(ty_shr) (ν ⊓ ty_lft ty) tid (l +ₗ 2) ∨ [†ν]) ∗
□ (1.[ν] ={↑lftN ∪ ↑lft_userN}[↑lft_userN]▷=∗ [†ν]))%I.
Global Instance rc_persist_persistent tid ν γ l ty : Persistent (rc_persist tid ν γ l ty).
diff --git a/theories/typing/lib/rc/weak.v b/theories/typing/lib/rc/weak.v
index 77e40214..b800f535 100644
--- a/theories/typing/lib/rc/weak.v
+++ b/theories/typing/lib/rc/weak.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
From iris.algebra Require Import auth csum frac agree numbers.
From lrust.lang.lib Require Import memcpy.
From lrust.lifetime Require Import na_borrow.
diff --git a/theories/typing/lib/refcell/ref.v b/theories/typing/lib/refcell/ref.v
index ae10f43d..220b915c 100644
--- a/theories/typing/lib/refcell/ref.v
+++ b/theories/typing/lib/refcell/ref.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
From iris.algebra Require Import auth csum frac agree.
From iris.bi Require Import fractional.
From lrust.lifetime Require Import na_borrow.
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index 1af1e8dc..befa9dbc 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
From iris.algebra Require Import auth csum frac agree numbers.
From iris.bi Require Import fractional.
From lrust.lifetime Require Import lifetime na_borrow.
diff --git a/theories/typing/lib/refcell/refcell.v b/theories/typing/lib/refcell/refcell.v
index e7f5e657..5573e83f 100644
--- a/theories/typing/lib/refcell/refcell.v
+++ b/theories/typing/lib/refcell/refcell.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
From iris.algebra Require Import auth csum frac agree numbers.
From iris.bi Require Import fractional.
From lrust.lifetime Require Import na_borrow.
@@ -101,7 +101,7 @@ Section refcell.
| _ => False
end%I;
ty_shr κ tid l :=
- (∃ α γ, κ ⊑ α ∗ α ⊑ ty.(ty_lft) ∗
+ (∃ α γ, κ ⊑ α ∗ α ⊑ ty_lft ty ∗
&na{α, tid, refcell_invN}(refcell_inv tid l γ α ty))%I |}.
Next Obligation.
iIntros (??[|[[]|]]); try iIntros "[]". rewrite ty_size_eq /=. by iIntros (->).
diff --git a/theories/typing/lib/refcell/refcell_code.v b/theories/typing/lib/refcell/refcell_code.v
index af7face2..d5070402 100644
--- a/theories/typing/lib/refcell/refcell_code.v
+++ b/theories/typing/lib/refcell/refcell_code.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
From iris.algebra Require Import auth csum frac agree.
From iris.bi Require Import fractional.
From lrust.lang.lib Require Import memcpy.
diff --git a/theories/typing/lib/refcell/refmut.v b/theories/typing/lib/refcell/refmut.v
index 7332c953..8e634a2e 100644
--- a/theories/typing/lib/refcell/refmut.v
+++ b/theories/typing/lib/refcell/refmut.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
From iris.algebra Require Import auth csum frac agree.
From iris.bi Require Import fractional.
From lrust.lifetime Require Import na_borrow.
@@ -27,7 +27,7 @@ Section refmut.
match vl return _ with
| [ #(LitLoc lv); #(LitLoc lrc) ] =>
∃ ν q γ β ty', &{α ⊓ ν}(lv ↦∗: ty.(ty_own) tid) ∗
- α ⊑ β ∗ α ⊓ ν ⊑ ty.(ty_lft) ∗
+ α ⊑ β ∗ α ⊓ ν ⊑ ty_lft ty ∗
&na{β, tid, refcell_invN}(refcell_inv tid lrc γ β ty') ∗
q.[ν] ∗ own γ (◯ writing_stR q ν)
| _ => False
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index 4ba81432..b23d8fa6 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
From iris.algebra Require Import auth csum frac agree numbers.
From iris.bi Require Import fractional.
From lrust.lifetime Require Import na_borrow.
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index 961cd95f..736d26ed 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
From iris.algebra Require Import auth csum frac agree excl numbers.
From iris.bi Require Import fractional.
From lrust.lifetime Require Import at_borrow.
@@ -108,7 +108,7 @@ Section rwlock.
| _ => False
end%I;
ty_shr κ tid l :=
- (∃ α γ, κ ⊑ α ∗ α ⊑ ty.(ty_lft) ∗
+ (∃ α γ, κ ⊑ α ∗ α ⊑ ty_lft ty ∗
&at{α,rwlockN}(rwlock_inv tid tid l γ α ty))%I |}.
Next Obligation.
iIntros (??[|[[]|]]); try iIntros "[]". rewrite ty_size_eq.
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index 3b21c2d8..b8ab832b 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
From iris.algebra Require Import auth csum frac agree.
From iris.bi Require Import fractional.
From lrust.lang.lib Require Import memcpy.
diff --git a/theories/typing/lib/rwlock/rwlockreadguard.v b/theories/typing/lib/rwlock/rwlockreadguard.v
index 4d162190..83b652e1 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
From iris.algebra Require Import auth csum frac agree.
From iris.bi Require Import fractional.
From lrust.lifetime Require Import na_borrow.
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index 6bfda63d..acd7ae81 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
From iris.algebra Require Import auth csum frac agree numbers.
From iris.bi Require Import fractional.
From lrust.lifetime Require Import lifetime na_borrow.
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard.v b/theories/typing/lib/rwlock/rwlockwriteguard.v
index 7c96791a..69620a05 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
From iris.algebra Require Import auth csum frac agree.
From iris.bi Require Import fractional.
From lrust.lifetime Require Import na_borrow.
@@ -23,7 +23,7 @@ Section rwlockwriteguard.
match vl return _ with
| [ #(LitLoc l) ] =>
∃ γ β tid_shr, &{β}((l +ₗ 1) ↦∗: ty.(ty_own) tid) ∗
- α ⊑ β ∗ β ⊑ ty.(ty_lft) ∗
+ α ⊑ β ∗ β ⊑ ty_lft ty ∗
&at{β,rwlockN}(rwlock_inv tid tid_shr l γ β ty) ∗
own γ (◯ writing_st)
| _ => False
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard_code.v b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
index 797ad601..9539be53 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
From iris.algebra Require Import auth csum frac agree.
From iris.bi Require Import fractional.
From lrust.lifetime Require Import na_borrow.
diff --git a/theories/typing/lib/slice/slice.v b/theories/typing/lib/slice/slice.v
index 3cb66a63..f8b91edf 100644
--- a/theories/typing/lib/slice/slice.v
+++ b/theories/typing/lib/slice/slice.v
@@ -82,7 +82,7 @@ Section slice.
(* Rust's &'a mut [T] *)
Program Definition uniq_slice {𝔄} (κ: lft) (ty: type 𝔄) : type (listₛ (𝔄 * 𝔄)) := {|
ty_size := 2; ty_lfts := κ :: ty.(ty_lfts); ty_E := ty.(ty_E) ++ ty_outlives_E ty κ;
- ty_own vπ d tid vl := κ ⊑ ty.(ty_lft) ∗
+ ty_own vπ d tid vl := κ ⊑ ty_lft ty ∗
∃(l: loc) (n d': nat) (aπξil: vec (proph 𝔄 * positive) n),
let aaπl := vmap
(λ aπξi π, (aπξi.1 π, π (PrVar (𝔄 ↾ prval_to_inh aπξi.1) aπξi.2): 𝔄)) aπξil in
@@ -122,7 +122,8 @@ Section slice.
iMod (bor_fracture (λ q, q:+[_])%I with "LFT Borξl") as "Borξl"; [done|].
iModIntro. case d as [|]; [lia|]. iExists _, _, _, _. iFrame "Bor↦ Borξl".
iSplit; last first.
- { iClear "#". iNext. iStopProof. do 3 f_equiv. iApply ty_shr_depth_mono. lia. }
+ { iClear "#". iNext. iStopProof. do 3 f_equiv; [|done].
+ iApply ty_shr_depth_mono. lia. }
iPureIntro. split.
- fun_ext=>/= ?. by elim aπξil; [done|]=>/= ???->.
- rewrite /ξl. elim aπξil; [done|]=>/= ????.
diff --git a/theories/typing/lib/slice/slice_basic.v b/theories/typing/lib/slice/slice_basic.v
index 9574c97b..6aec9578 100644
--- a/theories/typing/lib/slice/slice_basic.v
+++ b/theories/typing/lib/slice/slice_basic.v
@@ -19,7 +19,7 @@ Section slice_basic.
Qed.
Global Instance shr_slice_send {𝔄} κ (ty: type 𝔄) : Sync ty → Send (shr_slice κ ty).
- Proof. move=> >/=. by do 12 f_equiv. Qed.
+ Proof. move=> >/=. by do 12 (f_equiv || move=>?). Qed.
Lemma shr_slice_resolve {𝔄} κ (ty: type 𝔄) E L : resolve E L (shr_slice κ ty) (const True).
Proof. apply resolve_just. Qed.
@@ -76,7 +76,7 @@ Section slice_basic.
Proof. move=> >/=. rewrite /uniq_body. by do 24 f_equiv. Qed.
Global Instance uniq_slice_sync {𝔄} κ (ty: type 𝔄) : Sync ty → Sync (uniq_slice κ ty).
- Proof. move=> >/=. by do 17 f_equiv. Qed.
+ Proof. move=> >/=. by do 17 (f_equiv || move=>?). Qed.
Lemma uniq_slice_resolve {𝔄} κ (ty: type 𝔄) E L :
lctx_lft_alive E L κ →
diff --git a/theories/typing/lib/spawn.v b/theories/typing/lib/spawn.v
index 56e6ad5a..54f4b4f5 100644
--- a/theories/typing/lib/spawn.v
+++ b/theories/typing/lib/spawn.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
From lrust.lang Require Import spawn.
From lrust.typing Require Export type.
From lrust.typing Require Import typing.
diff --git a/theories/typing/lib/swap.v b/theories/typing/lib/swap.v
index 253fc315..0ab8ef55 100644
--- a/theories/typing/lib/swap.v
+++ b/theories/typing/lib/swap.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
From lrust.lang.lib Require Import swap.
From lrust.typing Require Import typing.
Set Default Proof Using "Type".
diff --git a/theories/typing/lib/take_mut.v b/theories/typing/lib/take_mut.v
index c5af236f..0b71a85d 100644
--- a/theories/typing/lib/take_mut.v
+++ b/theories/typing/lib/take_mut.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
From lrust.lang.lib Require Import memcpy.
From lrust.lifetime Require Import na_borrow.
From lrust.typing Require Export type.
diff --git a/theories/typing/lib/vec/vec_basic.v b/theories/typing/lib/vec/vec_basic.v
index da20c4f2..af9dd03d 100644
--- a/theories/typing/lib/vec/vec_basic.v
+++ b/theories/typing/lib/vec/vec_basic.v
@@ -17,10 +17,10 @@ Section vec_basic.
Qed.
Global Instance vec_send {𝔄} (ty: type 𝔄) : Send ty → Send (vec_ty ty).
- Proof. move=> ?>/=. by do 19 f_equiv. Qed.
+ Proof. move=> ?>/=. by do 19 (f_equiv || move=>?). Qed.
Global Instance vec_sync {𝔄} (ty: type 𝔄) : Sync ty → Sync (vec_ty ty).
- Proof. move=> ?>/=. by do 16 f_equiv. Qed.
+ Proof. move=> ?>/=. by do 16 (f_equiv || move=>?). Qed.
Lemma vec_resolve {𝔄} (ty: type 𝔄) Φ E L :
resolve E L ty Φ → resolve E L (vec_ty ty) (lforall Φ).
diff --git a/theories/typing/own.v b/theories/typing/own.v
index e42de1a4..d06e2d1b 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -36,7 +36,7 @@ Section own.
- by rewrite left_id shift_loc_0.
- by rewrite right_id Nat.add_0_r.
- iSplit; by [iIntros "[??]"|iIntros].
- - rewrite heap_freeable_op_eq. f_equiv.
+ - rewrite heap_freeable_op_eq. f_equiv; [|done].
by rewrite -Qp_div_add_distr pos_to_Qp_add -Nat2Pos.inj_add.
Qed.
@@ -108,10 +108,10 @@ Section own.
Qed.
Global Instance own_send {𝔄} n (ty: type 𝔄) : Send ty → Send (own_ptr n ty).
- Proof. move=> >/=. by do 9 f_equiv. Qed.
+ Proof. move=> >/=. by do 9 (f_equiv || move=>?). Qed.
Global Instance own_sync {𝔄} n (ty: type 𝔄) : Sync ty → Sync (own_ptr n ty).
- Proof. move=> >/=. by do 6 f_equiv. Qed.
+ Proof. move=> >/=. by do 6 (f_equiv || move=>?). Qed.
Global Instance own_just_loc {𝔄} n (ty: type 𝔄) : JustLoc (own_ptr n ty).
Proof. iIntros (?[|]?[|[[]|][]]) "? //". by iExists _. Qed.
diff --git a/theories/typing/product.v b/theories/typing/product.v
index 37a9c6ba..0cb50dac 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
From iris.algebra Require Import list numbers.
From lrust.typing Require Import lft_contexts.
From lrust.typing Require Export type.
@@ -290,7 +290,7 @@ Section typing.
Hint Resolve prod_resolve : lrust_typing.
Lemma xprod_resolve {𝔄l} (tyl: typel 𝔄l) Φl E L :
resolvel E L tyl Φl →
- resolve E L (Π! tyl) (λ al, pforall (λ _, curry ($)) (pzip Φl al)).
+ resolve E L (Π! tyl) (λ al, pforall (λ _, uncurry ($)) (pzip Φl al)).
Proof.
elim; [eapply resolve_impl; [apply resolve_just|done]|]=>/= *.
by eapply resolve_impl; [solve_typing|]=>/= [[??][??]].
@@ -424,7 +424,7 @@ Section typing.
Qed.
Lemma xprod_ty_app_prod {𝔄l 𝔅l} E L (tyl: typel 𝔄l) (tyl': typel 𝔅l) :
- eqtype E L (Π! (tyl h++ tyl')) (Π! tyl * Π! tyl') psep (curry papp).
+ eqtype E L (Π! (tyl h++ tyl')) (Π! tyl * Π! tyl') psep (uncurry papp).
Proof.
elim: tyl=> [|> Eq].
- eapply eqtype_eq.
diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v
index a941995d..707e54ac 100644
--- a/theories/typing/product_split.v
+++ b/theories/typing/product_split.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
From lrust.typing Require Export type.
From lrust.typing Require Import type_context lft_contexts product own uniq_bor.
From lrust.typing Require Import shr_bor mod_ty uninit.
diff --git a/theories/typing/soundness.v b/theories/typing/soundness.v
index 9fe2981c..c86c4f30 100644
--- a/theories/typing/soundness.v
+++ b/theories/typing/soundness.v
@@ -1,14 +1,14 @@
From iris.algebra Require Import frac.
From iris.base_logic.lib Require Import na_invariants.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
From lrust.lang Require Import races adequacy proofmode notation.
From lrust.lifetime Require Import lifetime frac_borrow.
From lrust.typing Require Import typing.
Set Default Proof Using "Type".
Class typePreG Σ := PreTypeG {
- type_preG_lrustG :> lrustPreG Σ;
- type_preG_lftG :> lftPreG Σ;
+ type_preG_lrustGS :> lrustGpreS Σ;
+ type_preG_lftGS :> lftGpreS Σ;
type_preG_na_invG :> na_invG Σ;
type_preG_frac_borG :> frac_borG Σ;
type_preG_prophG:> prophPreG Σ;
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index 20445026..0d0f09f9 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
From lrust.typing Require Import lft_contexts mod_ty.
From lrust.typing Require Export type.
Set Default Proof Using "Type".
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 01e735e5..401d5979 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -11,10 +11,10 @@ Set Default Proof Using "Type".
Implicit Type (𝔄 𝔅 ℭ: syn_type) (𝔄l 𝔅l: syn_typel).
Class typeG Σ := TypeG {
- type_lrustG :> lrustG Σ;
+ type_lrustGS :> lrustGS Σ;
type_prophG :> prophG Σ;
type_uniqG :> uniqG Σ;
- type_lftG :> lftG Σ;
+ type_lftGS :> lftGS Σ;
type_na_invG :> na_invG Σ;
type_frac_borG :> frac_borG Σ;
}.
@@ -121,7 +121,7 @@ Proof.
Qed.
Lemma elctx_interp_ty_outlives_E `{!typeG Σ} {𝔄} (ty: type 𝔄) α :
- elctx_interp (ty_outlives_E ty α) ⊣⊢ α ⊑ ty.(ty_lft).
+ elctx_interp (ty_outlives_E ty α) ⊣⊢ α ⊑ ty_lft ty.
Proof.
rewrite /ty_outlives_E /elctx_elt_interp big_sepL_fmap /=.
elim ty.(ty_lfts)=>/= [|κ l ->].
@@ -453,12 +453,12 @@ Ltac solve_ne_type :=
Inductive TypeLftMorphism `{!typeG Σ} {𝔄 𝔅} (T: type 𝔄 → type 𝔅) : Prop :=
| type_lft_morphism_add α βs E :
- (∀ty, ⊢ (T ty).(ty_lft) ≡ₗ α ⊓ ty.(ty_lft)) →
+ (∀ty, ⊢ ty_lft (T ty) ≡ₗ α ⊓ ty_lft ty) →
(∀ty, elctx_interp (T ty).(ty_E) ⊣⊢
- elctx_interp E ∗ elctx_interp ty.(ty_E) ∗ [∗ list] β ∈ βs, β ⊑ ty.(ty_lft)) →
+ elctx_interp E ∗ elctx_interp ty.(ty_E) ∗ [∗ list] β ∈ βs, β ⊑ ty_lft ty) →
TypeLftMorphism T
| type_lft_morphism_const α E :
- (∀ty, ⊢ (T ty).(ty_lft) ≡ₗ α) →
+ (∀ty, ⊢ ty_lft (T ty) ≡ₗ α) →
(∀ty, elctx_interp (T ty).(ty_E) ⊣⊢ elctx_interp E) →
TypeLftMorphism T.
Existing Class TypeLftMorphism.
@@ -516,7 +516,7 @@ Qed.
Lemma type_lft_morphism_lft_equiv_proper {𝔄 𝔅} (T: type 𝔄 → type 𝔅)
{HT: TypeLftMorphism T} ty ty' :
- ty.(ty_lft) ≡ₗ ty'.(ty_lft) -∗ (T ty).(ty_lft) ≡ₗ (T ty').(ty_lft).
+ ty_lft ty ≡ₗ ty_lft ty' -∗ ty_lft (T ty) ≡ₗ ty_lft (T ty').
Proof.
iIntros "#?". case HT=> [α βs E Hα HE|α E Hα HE].
- iApply lft_equiv_trans; [|iApply lft_equiv_sym; iApply Hα].
@@ -528,7 +528,7 @@ Qed.
Lemma type_lft_morphism_elctx_interp_proper {𝔄 𝔅} (T: type 𝔄 → type 𝔅)
{HT: TypeLftMorphism T} ty ty' :
- elctx_interp ty.(ty_E) ≡ elctx_interp ty'.(ty_E) → (⊢ ty.(ty_lft) ≡ₗ ty'.(ty_lft)) →
+ elctx_interp ty.(ty_E) ≡ elctx_interp ty'.(ty_E) → (⊢ ty_lft ty ≡ₗ ty_lft ty') →
elctx_interp (T ty).(ty_E) ≡ elctx_interp (T ty').(ty_E).
Proof.
move=> EqvE EqvLft. move: HT=> [|] > ? HE; [|by rewrite !HE].
@@ -541,13 +541,13 @@ Class TypeNonExpansive `{!typeG Σ} {𝔄 𝔅} (T: type 𝔄 → type 𝔅) : P
type_ne_ty_size ty ty' :
ty.(ty_size) = ty'.(ty_size) → (T ty).(ty_size) = (T ty').(ty_size);
type_ne_ty_own n ty ty' :
- ty.(ty_size) = ty'.(ty_size) → (⊢ ty.(ty_lft) ≡ₗ ty'.(ty_lft)) →
+ ty.(ty_size) = ty'.(ty_size) → (⊢ ty_lft ty ≡ₗ ty_lft ty') →
elctx_interp ty.(ty_E) ≡ elctx_interp ty'.(ty_E) →
(∀vπ d tid vl, ty.(ty_own) vπ d tid vl ≡{n}≡ ty'.(ty_own) vπ d tid vl) →
(∀vπ d κ tid l, ty.(ty_shr) vπ d κ tid l ≡{S n}≡ ty'.(ty_shr) vπ d κ tid l) →
(∀vπ d tid vl, (T ty).(ty_own) vπ d tid vl ≡{n}≡ (T ty').(ty_own) vπ d tid vl);
type_ne_ty_shr n ty ty' :
- ty.(ty_size) = ty'.(ty_size) → (⊢ ty.(ty_lft) ≡ₗ ty'.(ty_lft)) →
+ ty.(ty_size) = ty'.(ty_size) → (⊢ ty_lft ty ≡ₗ ty_lft ty') →
elctx_interp ty.(ty_E) ≡ elctx_interp ty'.(ty_E) →
(∀vπ d tid vl,
dist_later n (ty.(ty_own) vπ d tid vl) (ty'.(ty_own) vπ d tid vl)) →
@@ -559,13 +559,13 @@ Class TypeContractive `{!typeG Σ} {𝔄 𝔅} (T: type 𝔄 → type 𝔅) : Pr
type_contractive_type_lft_morphism : TypeLftMorphism T;
type_contractive_ty_size ty ty' : (T ty).(ty_size) = (T ty').(ty_size);
type_contractive_ty_own n ty ty' :
- ty.(ty_size) = ty'.(ty_size) → (⊢ ty.(ty_lft) ≡ₗ ty'.(ty_lft)) →
+ ty.(ty_size) = ty'.(ty_size) → (⊢ ty_lft ty ≡ₗ ty_lft ty') →
elctx_interp ty.(ty_E) ≡ elctx_interp ty'.(ty_E) →
(∀vπ d tid vl, dist_later n (ty.(ty_own) vπ d tid vl) (ty'.(ty_own) vπ d tid vl)) →
(∀vπ d κ tid l, ty.(ty_shr) vπ d κ tid l ≡{n}≡ ty'.(ty_shr) vπ d κ tid l) →
(∀vπ d tid vl, (T ty).(ty_own) vπ d tid vl ≡{n}≡ (T ty').(ty_own) vπ d tid vl);
type_contractive_ty_shr n ty ty' :
- ty.(ty_size) = ty'.(ty_size) → (⊢ ty.(ty_lft) ≡ₗ ty'.(ty_lft)) →
+ ty.(ty_size) = ty'.(ty_size) → (⊢ ty_lft ty ≡ₗ ty_lft ty') →
elctx_interp ty.(ty_E) ≡ elctx_interp ty'.(ty_E) →
(∀vπ d tid vl, match n with S (S n) =>
ty.(ty_own) vπ d tid vl ≡{n}≡ ty'.(ty_own) vπ d tid vl | _ => True end) →
@@ -867,7 +867,7 @@ End real.
Definition type_incl `{!typeG Σ} {𝔄 𝔅} (ty: type 𝔄) (ty': type 𝔅) (f: 𝔄 → 𝔅)
: iProp Σ :=
- ⌜ty.(ty_size) = ty'.(ty_size)⌝ ∗ (ty'.(ty_lft) ⊑ ty.(ty_lft)) ∗
+ ⌜ty.(ty_size) = ty'.(ty_size)⌝ ∗ (ty_lft ty' ⊑ ty_lft ty) ∗
(□ ∀vπ d tid vl, ty.(ty_own) vπ d tid vl -∗ ty'.(ty_own) (f ∘ vπ) d tid vl) ∗
(□ ∀vπ d κ tid l, ty.(ty_shr) vπ d κ tid l -∗ ty'.(ty_shr) (f ∘ vπ) d κ tid l).
Instance: Params (@type_incl) 4 := {}.
@@ -900,7 +900,7 @@ Section subtyping.
Lemma eqtype_unfold {𝔄 𝔅} E L f g `{!Iso f g} (ty : type 𝔄) (ty' : type 𝔅) :
eqtype E L ty ty' f g ↔
∀qL, llctx_interp L qL -∗ □ (elctx_interp E -∗
- ⌜ty.(ty_size) = ty'.(ty_size)⌝ ∗ ty.(ty_lft) ≡ₗ ty'.(ty_lft) ∗
+ ⌜ty.(ty_size) = ty'.(ty_size)⌝ ∗ ty_lft ty ≡ₗ ty_lft ty' ∗
(□ ∀vπ d tid vl, ty.(ty_own) vπ d tid vl ↔ ty'.(ty_own) (f ∘ vπ) d tid vl) ∗
(□ ∀vπ d κ tid l, ty.(ty_shr) vπ d κ tid l ↔ ty'.(ty_shr) (f ∘ vπ) d κ tid l)).
Proof.
@@ -924,7 +924,7 @@ Section subtyping.
Lemma eqtype_id_unfold {𝔄} E L (ty ty': type 𝔄) :
eqtype E L ty ty' id id ↔
∀qL, llctx_interp L qL -∗ □ (elctx_interp E -∗
- ⌜ty.(ty_size) = ty'.(ty_size)⌝ ∗ ty.(ty_lft) ≡ₗ ty'.(ty_lft) ∗
+ ⌜ty.(ty_size) = ty'.(ty_size)⌝ ∗ ty_lft ty ≡ₗ ty_lft ty' ∗
(□ ∀vπ d tid vl, ty.(ty_own) vπ d tid vl ↔ ty'.(ty_own) vπ d tid vl) ∗
(□ ∀vπ d κ tid l, ty.(ty_shr) vπ d κ tid l ↔ ty'.(ty_shr) vπ d κ tid l)).
Proof. by rewrite eqtype_unfold. Qed.
@@ -1058,7 +1058,7 @@ Section subtyping.
(** Simple Type *)
Lemma type_incl_simple_type {𝔄 𝔅} f (st: simple_type 𝔄) (st': simple_type 𝔅):
- st.(st_size) = st'.(st_size) → st'.(ty_lft) ⊑ st.(ty_lft) -∗
+ st.(st_size) = st'.(st_size) → ty_lft st' ⊑ ty_lft st -∗
□ (∀vπ d tid vl, st.(st_own) vπ d tid vl -∗ st'.(st_own) (f ∘ vπ) d tid vl) -∗
type_incl st st' f.
Proof.
@@ -1069,7 +1069,7 @@ Section subtyping.
Lemma subtype_simple_type {𝔄 𝔅} E L f (st: simple_type 𝔄) (st': simple_type 𝔅) :
(∀qL, llctx_interp L qL -∗ □ (elctx_interp E -∗
- ⌜st.(st_size) = st'.(st_size)⌝ ∗ st'.(ty_lft) ⊑ st.(ty_lft) ∗
+ ⌜st.(st_size) = st'.(st_size)⌝ ∗ ty_lft st' ⊑ ty_lft st ∗
(∀vπ d tid vl, st.(st_own) vπ d tid vl -∗ st'.(st_own) (f ∘ vπ) d tid vl))) →
subtype E L st st' f.
Proof.
@@ -1081,7 +1081,7 @@ Section subtyping.
(** Plain Type *)
Lemma type_incl_plain_type {𝔄 𝔅} f (pt: plain_type 𝔄) (pt': plain_type 𝔅):
- pt.(pt_size) = pt'.(pt_size) → pt'.(ty_lft) ⊑ pt.(ty_lft) -∗
+ pt.(pt_size) = pt'.(pt_size) → ty_lft pt' ⊑ ty_lft pt -∗
□ (∀v tid vl, pt.(pt_own) v tid vl -∗ pt'.(pt_own) (f v) tid vl) -∗
type_incl pt pt' f.
Proof.
@@ -1093,7 +1093,7 @@ Section subtyping.
Lemma subtype_plain_type {𝔄 𝔅} E L f (pt: plain_type 𝔄) (pt': plain_type 𝔅) :
(∀qL, llctx_interp L qL -∗ □ (elctx_interp E -∗
- ⌜pt.(pt_size) = pt'.(pt_size)⌝ ∗ pt'.(ty_lft) ⊑ pt.(ty_lft) ∗
+ ⌜pt.(pt_size) = pt'.(pt_size)⌝ ∗ ty_lft pt' ⊑ ty_lft pt ∗
(∀v tid vl, pt.(pt_own) v tid vl -∗ pt'.(pt_own) (f v) tid vl))) →
subtype E L pt pt' f.
Proof.
diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v
index 02623ad5..a643d732 100644
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
From lrust.typing Require Import type lft_contexts.
Set Default Proof Using "Type".
@@ -64,7 +64,7 @@ Section type_context.
| e => to_val e end.
Lemma eval_path_of_val (v: val) : eval_path v = Some v.
- Proof. case v; [done|]=>/= *. by rewrite (decide_left _). Qed.
+ Proof. case v; [done|]=>/= *. by rewrite (decide_True_pi _). Qed.
Lemma wp_eval_path E p v :
eval_path p = Some v → ⊢ WP p @ E {{ v', ⌜v' = v⌝ }}.
@@ -538,7 +538,7 @@ Section lemmas.
Qed.
Lemma unblock_tctx_cons_unblock {𝔄 𝔄l} p (ty: type 𝔄) (T T': tctx 𝔄l) κ E L :
- lctx_lft_alive E L ty.(ty_lft) → unblock_tctx E L κ T T' →
+ lctx_lft_alive E L (ty_lft ty) → unblock_tctx E L κ T T' →
unblock_tctx E L κ (p ◁{κ} ty +:: T) (p ◁ ty +:: T').
Proof.
iIntros (Alv Un ??[??]) "#LFT #E [L L'] #†κ /=[(%v &%& Upd) T]".
diff --git a/theories/typing/type_sum.v b/theories/typing/type_sum.v
index 2d66c2b6..464e99b6 100644
--- a/theories/typing/type_sum.v
+++ b/theories/typing/type_sum.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
From lrust.lang Require Import memcpy.
From lrust.typing Require Import int uninit uniq_bor shr_bor own sum.
From lrust.typing Require Import lft_contexts type_context programs product.
diff --git a/theories/typing/uniq_array_util.v b/theories/typing/uniq_array_util.v
index 702f3ff4..0fd1dfe3 100644
--- a/theories/typing/uniq_array_util.v
+++ b/theories/typing/uniq_array_util.v
@@ -8,7 +8,7 @@ Section uniq_array_util.
Lemma ty_share_big_sepL_uniq_body {𝔄} (ty: type 𝔄) n (vπξil: vec _ n)
d κ tid l κ' q E :
- ↑lftN ⊆ E → lft_ctx -∗ κ' ⊑ κ -∗ κ' ⊑ ty.(ty_lft) -∗
+ ↑lftN ⊆ E → lft_ctx -∗ κ' ⊑ κ -∗ κ' ⊑ ty_lft ty -∗
&{κ'} ([∗ list] i ↦ vπξi ∈ vπξil, uniq_body ty vπξi.1 vπξi.2 d κ tid (l +ₗ[ty] i)) -∗
q.[κ'] ={E}=∗ |={E}▷=>^(S d) |={E}=>
let ξl := vmap (λ vπξi, PrVar (𝔄 ↾ prval_to_inh vπξi.1) vπξi.2) vπξil in
@@ -31,7 +31,7 @@ Section uniq_array_util.
Lemma ty_own_proph_big_sepL_uniq_body {𝔄} (ty: type 𝔄) n (vπξil: vec _ n)
d κ tid l κ' q E :
- ↑lftN ⊆ E → lft_ctx -∗ κ' ⊑ κ -∗ κ' ⊑ ty.(ty_lft) -∗
+ ↑lftN ⊆ E → lft_ctx -∗ κ' ⊑ κ -∗ κ' ⊑ ty_lft ty -∗
([∗ list] i ↦ vπξi ∈ vπξil, uniq_body ty vπξi.1 vπξi.2 d κ tid (l +ₗ[ty] i)) -∗
q.[κ'] ={E}=∗ |={E}▷=>^(S d) |={E}=>
let ξl := vmap (λ vπξi, PrVar (𝔄 ↾ prval_to_inh vπξi.1) vπξi.2) vπξil in
@@ -61,7 +61,7 @@ Section uniq_array_util.
Lemma resolve_big_sepL_uniq_body {𝔄} (ty: type 𝔄) n (vπξil: vec _ n) d κ tid l E L q F :
lctx_lft_alive E L κ → ↑lftN ∪ ↑prophN ⊆ F →
- lft_ctx -∗ proph_ctx -∗ κ ⊑ ty.(ty_lft) -∗ elctx_interp E -∗ llctx_interp L q -∗
+ lft_ctx -∗ proph_ctx -∗ κ ⊑ ty_lft ty -∗ elctx_interp E -∗ llctx_interp L q -∗
([∗ list] i ↦ vπξi ∈ vπξil, uniq_body ty vπξi.1 vπξi.2 d κ tid (l +ₗ[ty] i))
={F}=∗ |={F}▷=>^(S d) |={F}=>
let φπ π := lforall (λ vπξi,
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index e183599a..458c9517 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -21,7 +21,7 @@ Section uniq_bor.
Program Definition uniq_bor {𝔄} (κ: lft) (ty: type 𝔄) : type (𝔄 * 𝔄) := {|
ty_size := 1; ty_lfts := κ :: ty.(ty_lfts); ty_E := ty.(ty_E) ++ ty_outlives_E ty κ;
- ty_own vπ d tid vl := κ ⊑ ty.(ty_lft) ∗ [loc[l] := vl] ∃d' ξi,
+ ty_own vπ d tid vl := κ ⊑ ty_lft ty ∗ [loc[l] := vl] ∃d' ξi,
let ξ := PrVar (𝔄 ↾ prval_to_inh (fst ∘ vπ)) ξi in
⌜(S d' ≤ d)%nat ∧ snd ∘ vπ = (.$ ξ)⌝ ∗ uniq_body ty (fst ∘ vπ) ξi d' κ tid l;
ty_shr vπ d κ' tid l := [S(d') := d] ∃(l': loc) ξ, ⌜snd ∘ vπ ./ [ξ]⌝ ∗
@@ -107,10 +107,10 @@ Section typing.
Qed.
Global Instance uniq_send {𝔄} κ (ty: type 𝔄) : Send ty → Send (&uniq{κ} ty).
- Proof. move=> >/=. rewrite /uniq_body. by do 19 f_equiv. Qed.
+ Proof. move=> >/=. rewrite /uniq_body. by do 19 (f_equiv || move=>?). Qed.
Global Instance uniq_sync {𝔄} κ (ty: type 𝔄) : Sync ty → Sync (&uniq{κ} ty).
- Proof. move=> >/=. by do 10 f_equiv. Qed.
+ Proof. move=> >/=. by do 10 (f_equiv || move=>?). Qed.
Global Instance uniq_just_loc {𝔄} κ (ty: type 𝔄) : JustLoc (&uniq{κ} ty).
Proof. iIntros (???[|[[]|][]]) "[_ ?] //". by iExists _. Qed.
diff --git a/theories/typing/uniq_cmra.v b/theories/typing/uniq_cmra.v
index 841f0c90..33dc2fb5 100644
--- a/theories/typing/uniq_cmra.v
+++ b/theories/typing/uniq_cmra.v
@@ -1,5 +1,5 @@
-From iris.algebra Require Import auth cmra functions gmap frac_agree.
-From iris.proofmode Require Import tactics.
+From iris.algebra Require Import auth cmra functions gmap dfrac_agree.
+From iris.proofmode Require Import proofmode.
From iris.base_logic Require Import invariants.
From lrust.util Require Import discrete_fun.
From lrust.prophecy Require Import prophecy.
@@ -9,7 +9,7 @@ Implicit Type (𝔄i: syn_typei) (𝔄: syn_type).
(** * Camera for Unique Borrowing *)
-Local Definition uniq_itemR 𝔄i := frac_agreeR (leibnizO (proph 𝔄i * nat)).
+Local Definition uniq_itemR 𝔄i := dfrac_agreeR (leibnizO (proph 𝔄i * nat)).
Local Definition uniq_gmapUR 𝔄i := gmapUR positive (uniq_itemR 𝔄i).
Local Definition uniq_smryUR := discrete_funUR uniq_gmapUR.
Definition uniqUR: ucmra := authUR uniq_smryUR.
@@ -32,7 +32,7 @@ Definition uniqN: namespace := lft_userN .@ "uniq".
(** * Iris Propositions *)
Section defs.
-Context `{!invG Σ, !prophG Σ, !uniqG Σ}.
+Context `{!invGS Σ, !prophG Σ, !uniqG Σ}.
(** Unique Reference Context *)
Definition uniq_inv: iProp Σ := ∃S, own uniq_name (● S).
@@ -62,7 +62,7 @@ Definition prval_to_inh {𝔄} (vπ: proph 𝔄) : inh_syn_type 𝔄 :=
to_inh_syn_type (vπ inhabitant).
Section lemmas.
-Context `{!invG Σ, !prophG Σ, !uniqG Σ}.
+Context `{!invGS Σ, !prophG Σ, !uniqG Σ}.
Global Instance uniq_ctx_persistent : Persistent uniq_ctx := _.
Global Instance val_obs_timeless ξ vπ d : Timeless (.VO[ξ] vπ d) := _.
diff --git a/theories/typing/uniq_util.v b/theories/typing/uniq_util.v
index f1182cfd..71ec5c50 100644
--- a/theories/typing/uniq_util.v
+++ b/theories/typing/uniq_util.v
@@ -13,7 +13,7 @@ Section uniq_util.
&{κ} (∃vπ' d', ⧖(S d') ∗ .PC[ξ] vπ' d' ∗ l ↦∗: ty.(ty_own) vπ' d' tid).
Lemma ty_share_uniq_body {𝔄} (ty: type 𝔄) vπ ξi d κ tid l κ' q E :
- ↑lftN ⊆ E → lft_ctx -∗ κ' ⊑ κ -∗ κ' ⊑ ty.(ty_lft) -∗
+ ↑lftN ⊆ E → lft_ctx -∗ κ' ⊑ κ -∗ κ' ⊑ ty_lft ty -∗
&{κ'} (uniq_body ty vπ ξi d κ tid l) -∗ q.[κ'] ={E}=∗ |={E}▷=>^(S d) |={E}=>
&{κ'} 1:[PrVar (𝔄 ↾ prval_to_inh vπ) ξi] ∗ ty.(ty_shr) vπ d κ' tid l ∗ q.[κ'].
Proof.
@@ -37,7 +37,7 @@ Section uniq_util.
Qed.
Lemma ty_own_proph_uniq_body {𝔄} (ty: type 𝔄) vπ ξi d κ tid l κ' q E :
- ↑lftN ⊆ E → lft_ctx -∗ κ' ⊑ κ -∗ κ' ⊑ ty.(ty_lft) -∗
+ ↑lftN ⊆ E → lft_ctx -∗ κ' ⊑ κ -∗ κ' ⊑ ty_lft ty -∗
uniq_body ty vπ ξi d κ tid l -∗ q.[κ'] ={E}=∗ |={E}▷=>^(S d) |={E}=>
let ξ := PrVar (𝔄 ↾ prval_to_inh vπ) ξi in
∃ζl q', ⌜vπ ./ ζl⌝ ∗ q':+[ζl ++ [ξ]] ∗
@@ -64,7 +64,7 @@ Section uniq_util.
Lemma resolve_uniq_body {𝔄} (ty: type 𝔄) vπ ξi d κ tid l E L q F :
lctx_lft_alive E L κ → ↑lftN ∪ ↑prophN ⊆ F →
- lft_ctx -∗ proph_ctx -∗ κ ⊑ ty.(ty_lft) -∗ elctx_interp E -∗ llctx_interp L q -∗
+ lft_ctx -∗ proph_ctx -∗ κ ⊑ ty_lft ty -∗ elctx_interp E -∗ llctx_interp L q -∗
uniq_body ty vπ ξi d κ tid l ={F}=∗ |={F}▷=>^(S d) |={F}=>
⟨π, π (PrVar (𝔄 ↾ prval_to_inh vπ) ξi) = vπ π⟩ ∗ llctx_interp L q.
Proof.
diff --git a/theories/util/basic.v b/theories/util/basic.v
index 0d4258d5..2249a47e 100644
--- a/theories/util/basic.v
+++ b/theories/util/basic.v
@@ -1,6 +1,6 @@
Require Export Equality FunctionalExtensionality.
From iris.algebra Require Import ofe.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
(** * Utility for Point-Free Style *)
diff --git a/theories/util/fancy_lists.v b/theories/util/fancy_lists.v
index eecfa382..2f09d759 100644
--- a/theories/util/fancy_lists.v
+++ b/theories/util/fancy_lists.v
@@ -1,5 +1,5 @@
From iris.algebra Require Import ofe.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
From lrust.util Require Import basic.
(** * Heterogeneous List *)
@@ -154,7 +154,7 @@ Fixpoint plookup {Xl} (xl: plist Xl) : ∀i, F (Xl !!ₗ i) :=
end.
Global Instance papp_psep_iso {Xl Yl}
- : Iso (curry (@papp Xl Yl)) (λ xl, (psepl xl, psepr xl)).
+ : Iso (uncurry (@papp Xl Yl)) (λ xl, (psepl xl, psepr xl)).
Proof.
split; fun_ext.
- case=>/= [??]. by rewrite papp_sepl papp_sepr.
@@ -704,7 +704,7 @@ Lemma big_sepHL_2_big_sepN {F G H: A → Type} {Xl}
[∗ nat] i < length Xl, Φ _ (xl +!! i) (yl -!! i) (zl -!! i).
Proof.
move: Φ. induction Xl; inv_hlist xl; case yl; case zl; [done|]=>/= *.
- f_equiv. apply IHXl.
+ f_equiv; [done|apply IHXl].
Qed.
Lemma big_sepHL_2_lookup {F G H: A → Type} {Xl}
diff --git a/theories/util/update.v b/theories/util/update.v
index 92338ce2..6b4e1911 100644
--- a/theories/util/update.v
+++ b/theories/util/update.v
@@ -1,5 +1,5 @@
From iris.bi Require Import updates.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
From lrust.util Require Import basic.
(* TODO : move all that to Iris *)
diff --git a/theories/util/vector.v b/theories/util/vector.v
index 01f4ef89..95107ddf 100644
--- a/theories/util/vector.v
+++ b/theories/util/vector.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
From lrust.util Require Import basic.
(* TODO : move all that to stdpp *)
@@ -25,7 +25,7 @@ Global Instance vhd_vsingleton_iso {A} : Iso vhd (λ x: A, [#x]).
Proof. split; [|done]. fun_ext=> v. by inv_vec v. Qed.
Global Instance vhd_vtl_vcons_iso {A n} :
- Iso (λ v: vec A (S n), (vhd v, vtl v)) (curry vcons').
+ Iso (λ v: vec A (S n), (vhd v, vtl v)) (uncurry vcons').
Proof. split; fun_ext; [|by case]=> v. by inv_vec v. Qed.
Global Instance vec_to_list_inj' {A n} : Inj (=) (=) (@vec_to_list A n).
@@ -52,7 +52,7 @@ Qed.
Lemma vapp_ex {A m n} (xl: _ A (m + n)) : ∃yl zl, xl = yl +++ zl.
Proof. eexists _, _. apply vsepat_app. Qed.
-Global Instance vapp_vsepat_iso {A} m n : Iso (curry vapp) (@vsepat A m n).
+Global Instance vapp_vsepat_iso {A} m n : Iso (uncurry vapp) (@vsepat A m n).
Proof.
split; fun_ext.
- move=> [xl ?]. by elim xl; [done|]=>/= ???->.
--
GitLab