diff --git a/.gitignore b/.gitignore
index 30ee28f867d2d16d405af4eade8415803f0ba55d..ecdc2641c856c3f94f1daa3e1fb9d99b9c8c9fa1 100644
--- a/.gitignore
+++ b/.gitignore
@@ -10,5 +10,5 @@
*.bak
.coq-native/
iris-enabled
-Makefile.coq
+Makefile.coq*
opamroot
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 62420da59d7cff04cb8871c418baaaa484566e94..28d985125fb44ac8f61e385a9f19237fb2699fd0 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -3,24 +3,38 @@ image: ralfjung/opam-ci:latest
variables:
CPU_CORES: "9"
-lrust-coq8.6:
+.template: &template
tags:
- fp-timing
script:
# prepare
- - . build/opam-ci.sh coq 8.6 coq-mathcomp-ssreflect 1.6.1
+ - . build/opam-ci.sh coq "$COQ_VERSION" coq-mathcomp-ssreflect "$SSR_VERSION"
- env | egrep '^(CI_BUILD_REF|CI_RUNNER)' > build-env.txt
# build
- 'time make -k -j$CPU_CORES TIMED=y 2>&1 | tee build-log.txt'
- 'if fgrep Axiom build-log.txt >/dev/null; then exit 1; fi'
- - 'cat build-log.txt | egrep "[a-zA-Z0-9_/-]+ \(user: [0-9]" | tee build-time.txt'
+ - 'cat build-log.txt | egrep "[a-zA-Z0-9_/-]+ \((real|user): [0-9]" | tee build-time.txt'
+ - 'if test -n "$VALIDATE" && (( RANDOM % 10 == 0 )); then make validate; fi'
cache:
- key: "coq8.6"
+ key: "coq$COQ_VERSION-ssr$SSR_VERSION"
paths:
- opamroot/
only:
- master
- /^ci/
+
+lrust-coq8.7:
+ <<: *template
+ variables:
+ COQ_VERSION: "8.7.dev"
+ SSR_VERSION: "dev"
+
+lrust-coq8.6.1:
+ <<: *template
+ variables:
+ COQ_VERSION: "8.6.1"
+ SSR_VERSION: "1.6.1"
+ VALIDATE: 1
artifacts:
paths:
- build-time.txt
diff --git a/_CoqProject b/_CoqProject
index 6655f65e692c5824ad66ed962987d2b870bb8056..c447a2bc4de6f5956033a7623b3c76c39d83309d 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -56,6 +56,7 @@ theories/typing/lib/fake_shared_box.v
theories/typing/lib/cell.v
theories/typing/lib/spawn.v
theories/typing/lib/join.v
+theories/typing/lib/diverging_static.v
theories/typing/lib/take_mut.v
theories/typing/lib/rc/rc.v
theories/typing/lib/rc/weak.v
diff --git a/opam.pins b/opam.pins
index 9087d1ed13556140819293adf4d9c13459b4c69d..2c200453f67a9f2301754445d21ca0e7403bc5a6 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 398bae9d092b6568cf8d504ca98d8810979eea33
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 2e2c5c25aea886acc7d0925d435fe856ffa6ac14
diff --git a/theories/lang/heap.v b/theories/lang/heap.v
index 58df7d54b0d9d06533e39ccdddde442c389ef280..6523f643d5d7398f4eeb5f8b5e5e9cad64bc1017 100644
--- a/theories/lang/heap.v
+++ b/theories/lang/heap.v
@@ -48,7 +48,7 @@ Section definitions.
seal_eq heap_mapsto_aux.
Definition heap_mapsto_vec (l : loc) (q : Qp) (vl : list val) : iProp Σ :=
- ([∗ list] i ↦ v ∈ vl, heap_mapsto (shift_loc l i) q v)%I.
+ ([∗ list] i ↦ v ∈ vl, heap_mapsto (l +ₗ i) q v)%I.
Fixpoint inter (i0 : Z) (n : nat) : gmapR Z (exclR unitC) :=
match n with O => ∅ | S n => <[i0 := Excl ()]>(inter (i0+1) n) end.
@@ -150,7 +150,7 @@ Section heap.
Proof. by rewrite /heap_mapsto_vec. Qed.
Lemma heap_mapsto_vec_app l q vl1 vl2 :
- l ↦∗{q} (vl1 ++ vl2) ⊣⊢ l ↦∗{q} vl1 ∗ shift_loc l (length vl1) ↦∗{q} vl2.
+ l ↦∗{q} (vl1 ++ vl2) ⊣⊢ l ↦∗{q} vl1 ∗ (l +ₗ length vl1) ↦∗{q} vl2.
Proof.
rewrite /heap_mapsto_vec big_sepL_app.
do 2 f_equiv. intros k v. by rewrite shift_loc_assoc_nat.
@@ -160,7 +160,7 @@ Section heap.
Proof. by rewrite /heap_mapsto_vec /= shift_loc_0 right_id. Qed.
Lemma heap_mapsto_vec_cons l q v vl:
- l ↦∗{q} (v :: vl) ⊣⊢ l ↦{q} v ∗ shift_loc l 1 ↦∗{q} vl.
+ l ↦∗{q} (v :: vl) ⊣⊢ l ↦{q} v ∗ (l +ₗ 1) ↦∗{q} vl.
Proof.
by rewrite (heap_mapsto_vec_app l q [v] vl) heap_mapsto_vec_singleton.
Qed.
@@ -173,7 +173,7 @@ Section heap.
- revert l. induction Hlen as [|v1 v2 vl1 vl2 _ _ IH]=> l.
{ rewrite !heap_mapsto_vec_nil. iIntros "_"; auto. }
rewrite !heap_mapsto_vec_cons. iIntros "[[Hv1 Hvl1] [Hv2 Hvl2]]".
- iDestruct (IH (shift_loc l 1) with "[$Hvl1 $Hvl2]") as "[% $]"; subst.
+ iDestruct (IH (l +ₗ 1) with "[$Hvl1 $Hvl2]") as "[% $]"; subst.
rewrite (inj_iff (:: vl2)).
iDestruct (heap_mapsto_agree with "[$Hv1 $Hv2]") as %<-.
iSplit; first done. iFrame.
@@ -212,7 +212,7 @@ Section heap.
Lemma heap_mapsto_vec_combine l q vl :
vl ≠ [] →
l ↦∗{q} vl ⊣⊢ own heap_name (◯ [^op list] i ↦ v ∈ vl,
- {[shift_loc l i := (q, Cinr 0%nat, to_agree v)]}).
+ {[l +ₗ i := (q, Cinr 0%nat, to_agree v)]}).
Proof.
rewrite /heap_mapsto_vec heap_mapsto_eq /heap_mapsto_def /heap_mapsto_st=>?.
by rewrite (big_opL_commute (Auth None)) big_opL_commute1 //.
@@ -269,7 +269,7 @@ Section heap.
Proof. revert i. induction n as [|n IH]=>i. done. by apply insert_valid. Qed.
Lemma heap_freeable_op_eq l q1 q2 n n' :
- †{q1}l…n ∗ †{q2}shift_loc l n…n' ⊣⊢ †{q1+q2}l…(n+n').
+ †{q1}l…n ∗ †{q2}l+ₗn … n' ⊣⊢ †{q1+q2}l…(n+n').
Proof.
by rewrite heap_freeable_eq /heap_freeable_def -own_op -auth_frag_op
op_singleton pair_op inter_op.
@@ -277,7 +277,7 @@ Section heap.
(** Properties about heap_freeable_rel and heap_freeable *)
Lemma heap_freeable_rel_None σ l hF :
- (∀ m : Z, σ !! shift_loc l m = None) → heap_freeable_rel σ hF →
+ (∀ m : Z, σ !! (l +ₗ m) = None) → heap_freeable_rel σ hF →
hF !! l.1 = None.
Proof.
intros FRESH REL. apply eq_None_not_Some. intros [[q s] [Hsne REL']%REL].
@@ -288,7 +288,7 @@ Section heap.
Lemma heap_freeable_is_Some σ hF l n i :
heap_freeable_rel σ hF →
hF !! l.1 = Some (1%Qp, inter (l.2) n) →
- is_Some (σ !! shift_loc l i) ↔ 0 ≤ i ∧ i < n.
+ is_Some (σ !! (l +ₗ i)) ↔ 0 ≤ i ∧ i < n.
Proof.
destruct l as [b j]; rewrite /shift_loc /=. intros REL Hl.
destruct (REL b (1%Qp, inter j n)) as [_ ->]; simpl in *; auto.
@@ -299,7 +299,7 @@ Section heap.
Lemma heap_freeable_rel_init_mem l h vl σ:
vl ≠ [] →
- (∀ m : Z, σ !! shift_loc l m = None) →
+ (∀ m : Z, σ !! (l +ₗ m) = None) →
heap_freeable_rel σ h →
heap_freeable_rel (init_mem l vl σ)
(<[l.1 := (1%Qp, inter (l.2) (length vl))]> h).
@@ -311,8 +311,7 @@ Section heap.
+ rewrite inter_lookup_Some //.
destruct (lookup_init_mem_Some σ l (l.1, i) vl); naive_solver.
+ rewrite inter_lookup_None; last lia. rewrite lookup_init_mem_ne /=; last lia.
- replace (l.1,i) with (shift_loc l (i - l.2))
- by (rewrite /shift_loc; f_equal; lia).
+ replace (l.1,i) with (l +ₗ (i - l.2)) by (rewrite /shift_loc; f_equal; lia).
by rewrite FRESH !is_Some_alt.
- destruct (REL blk qs) as [? Hs]; auto.
split; [done|]=> i. by rewrite -Hs lookup_init_mem_ne; last auto.
@@ -339,16 +338,16 @@ Section heap.
(** Weakest precondition *)
Lemma heap_alloc_vs σ l vl :
- (∀ m : Z, σ !! shift_loc l m = None) →
+ (∀ m : Z, σ !! (l +ₗ m) = None) →
own heap_name (● to_heap σ)
==∗ own heap_name (● to_heap (init_mem l vl σ))
∗ own heap_name (◯ [^op list] i ↦ v ∈ vl,
- {[shift_loc l i := (1%Qp, Cinr 0%nat, to_agree v)]}).
+ {[l +ₗ i := (1%Qp, Cinr 0%nat, to_agree v)]}).
Proof.
intros FREE. rewrite -own_op. apply own_update, auth_update_alloc.
revert l FREE. induction vl as [|v vl IH]=> l FRESH; [done|].
rewrite (big_opL_consZ_l (λ k _, _ (_ k) _ )) /=.
- etrans; first apply (IH (shift_loc l 1)).
+ 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' ?.
@@ -360,7 +359,7 @@ Section heap.
Lemma heap_alloc σ l n vl :
0 < n →
- (∀ m, σ !! shift_loc l m = None) →
+ (∀ m, σ !! (l +ₗ m) = None) →
Z.of_nat (length vl) = n →
heap_ctx σ ==∗
heap_ctx (init_mem l vl σ) ∗ †l…(Z.to_nat n) ∗ l ↦∗ vl.
@@ -382,7 +381,7 @@ Section heap.
Lemma heap_free_vs σ l vl :
own heap_name (● to_heap σ) ∗ own heap_name (◯ [^op list] i ↦ v ∈ vl,
- {[shift_loc l i := (1%Qp, Cinr 0%nat, to_agree v)]})
+ {[l +ₗ i := (1%Qp, Cinr 0%nat, to_agree v)]})
==∗ own heap_name (● to_heap (free_mem l (length vl) σ)).
Proof.
rewrite -own_op. apply own_update, auth_update_dealloc.
@@ -390,7 +389,7 @@ Section heap.
rewrite (big_opL_consZ_l (λ k _, _ (_ k) _ )) /= shift_loc_0.
apply local_update_total_valid=> _ Hvalid _.
assert (([^op list] k↦y ∈ vl,
- {[shift_loc l (1 + k) := (1%Qp, Cinr 0%nat, to_agree y)]} : heapUR) !! l = None).
+ {[l +ₗ (1 + k) := (1%Qp, Cinr 0%nat, to_agree y)]} : heapUR) !! l = None).
{ move: (Hvalid l). rewrite lookup_op lookup_singleton.
by move=> /(cmra_discrete_valid_iff 0) /exclusiveN_Some_l. }
rewrite -insert_singleton_op //. etrans.
@@ -403,7 +402,7 @@ Section heap.
Lemma heap_free σ l vl (n : Z) :
n = length vl →
heap_ctx σ -∗ l ↦∗ vl -∗ †l…(length vl)
- ==∗ ⌜0 < n⌝ ∗ ⌜∀ m, is_Some (σ !! (shift_loc l m)) ↔ (0 ≤ m < n)⌝ ∗
+ ==∗ ⌜0 < n⌝ ∗ ⌜∀ m, is_Some (σ !! (l +ₗ m)) ↔ (0 ≤ m < n)⌝ ∗
heap_ctx (free_mem l (Z.to_nat n) σ).
Proof.
iDestruct 1 as (hF) "(Hvalσ & HhF & REL)"; iDestruct "REL" as %REL.
diff --git a/theories/lang/lang.v b/theories/lang/lang.v
index 1dbd8ee6e64cac86914d30947093d9475bc8a10f..b7abe7f678e8492149cc635690fb515d1cced230 100644
--- a/theories/lang/lang.v
+++ b/theories/lang/lang.v
@@ -9,6 +9,10 @@ Open Scope Z_scope.
Definition block : Set := positive.
Definition loc : Set := block * Z.
+Bind Scope loc_scope with loc.
+Delimit Scope loc_scope with L.
+Open Scope loc_scope.
+
Inductive base_lit : Set :=
| LitUnit | LitLoc (l : loc) | LitInt (n : Z).
Inductive bin_op : Set :=
@@ -194,16 +198,19 @@ Definition lit_of_bool (b : bool) : base_lit :=
Definition shift_loc (l : loc) (z : Z) : loc := (l.1, l.2 + z).
+Notation "l +ₗ z" := (shift_loc l%L z%Z)
+ (at level 50, left associativity) : loc_scope.
+
Fixpoint init_mem (l:loc) (init:list val) (σ:state) : state :=
match init with
| [] => σ
- | inith :: initq => <[l:=(RSt 0, inith)]>(init_mem (shift_loc l 1) initq σ)
+ | inith :: initq => <[l:=(RSt 0, inith)]>(init_mem (l +ₗ 1) initq σ)
end.
Fixpoint free_mem (l:loc) (n:nat) (σ:state) : state :=
match n with
| O => σ
- | S n => delete l (free_mem (shift_loc l 1) n σ)
+ | S n => delete l (free_mem (l +ₗ 1) n σ)
end.
Inductive lit_eq (σ : state) : base_lit → base_lit → Prop :=
@@ -220,7 +227,11 @@ Inductive lit_neq (σ : state) : base_lit → base_lit → Prop :=
| IntNeq z1 z2 :
z1 ≠ z2 → lit_neq σ (LitInt z1) (LitInt z2)
| LocNeq l1 l2 :
- l1 ≠ l2 → lit_neq σ (LitLoc l1) (LitLoc l2).
+ l1 ≠ l2 → lit_neq σ (LitLoc l1) (LitLoc l2)
+| LocNeqNullR l :
+ lit_neq σ (LitLoc l) (LitInt 0)
+| LocNeqNullL l :
+ lit_neq σ (LitInt 0) (LitLoc l).
Inductive bin_op_eval (σ : state) : bin_op → base_lit → base_lit → base_lit → Prop :=
| BinOpPlus z1 z2 :
@@ -234,7 +245,7 @@ Inductive bin_op_eval (σ : state) : bin_op → base_lit → base_lit → base_l
| BinOpEqFalse l1 l2 :
lit_neq σ l1 l2 → bin_op_eval σ EqOp l1 l2 (lit_of_bool false)
| BinOpOffset l z :
- bin_op_eval σ OffsetOp (LitLoc l) (LitInt z) (LitLoc $ shift_loc l z).
+ bin_op_eval σ OffsetOp (LitLoc l) (LitInt z) (LitLoc $ l +ₗ z).
Definition stuck_term := App (Lit $ LitInt 0) [].
@@ -299,13 +310,13 @@ Inductive head_step : expr → state → expr → state → list expr → Prop :
[]
| AllocS n l init σ :
0 < n →
- (∀ m, σ !! shift_loc l m = None) →
+ (∀ m, σ !! (l +ₗ m) = None) →
Z.of_nat (length init) = n →
head_step (Alloc $ Lit $ LitInt n) σ
(Lit $ LitLoc l) (init_mem l init σ) []
| FreeS n l σ :
0 < n →
- (∀ m, is_Some (σ !! shift_loc l m) ↔ 0 ≤ m < n) →
+ (∀ m, is_Some (σ !! (l +ₗ m)) ↔ 0 ≤ m < n) →
head_step (Free (Lit $ LitInt n) (Lit $ LitLoc l)) σ
(Lit LitUnit) (free_mem l (Z.to_nat n) σ)
[]
@@ -373,22 +384,20 @@ Proof.
destruct (list_expr_val_eq_inv vl1 vl2 e1 e2 el1 el2); auto. congruence.
Qed.
-Lemma shift_loc_assoc l n n' :
- shift_loc (shift_loc l n) n' = shift_loc l (n+n').
+Lemma shift_loc_assoc l n n' : l +ₗ n +ₗ n' = l +ₗ (n + n').
Proof. rewrite /shift_loc /=. f_equal. lia. Qed.
-Lemma shift_loc_0 l : shift_loc l 0 = l.
+Lemma shift_loc_0 l : l +ₗ 0 = l.
Proof. destruct l as [b o]. rewrite /shift_loc /=. f_equal. lia. Qed.
-Lemma shift_loc_assoc_nat l (n n' : nat) :
- shift_loc (shift_loc l n) n' = shift_loc l (n+n')%nat.
+Lemma shift_loc_assoc_nat l (n n' : nat) : l +ₗ n +ₗ n' = l +ₗ (n + n')%nat.
Proof. rewrite /shift_loc /=. f_equal. lia. Qed.
-Lemma shift_loc_0_nat l : shift_loc l 0%nat = l.
+Lemma shift_loc_0_nat l : l +ₗ 0%nat = l.
Proof. destruct l as [b o]. rewrite /shift_loc /=. f_equal. lia. Qed.
Instance shift_loc_inj l : Inj (=) (=) (shift_loc l).
Proof. destruct l as [b o]; intros n n' [=?]; lia. Qed.
-Lemma shift_loc_block l n : (shift_loc l n).1 = l.1.
+Lemma shift_loc_block l n : (l +ₗ n).1 = l.1.
Proof. done. Qed.
Lemma lookup_init_mem σ (l l' : loc) vl :
@@ -420,7 +429,7 @@ Lemma lookup_init_mem_ne σ (l l' : loc) vl :
init_mem l vl σ !! l' = σ !! l'.
Proof.
revert l. induction vl as [|v vl IH]=> /= l Hl; auto.
- rewrite -(IH (shift_loc l 1)); last (simpl; intuition lia).
+ rewrite -(IH (l +ₗ 1)); last (simpl; intuition lia).
apply lookup_insert_ne. intros ->; intuition lia.
Qed.
@@ -629,6 +638,6 @@ Notation LetCtx x e2 := (AppRCtx (LamV [x] e2) [] []).
Notation SeqCtx e2 := (LetCtx BAnon e2).
Notation Skip := (Seq (Lit LitUnit) (Lit LitUnit)).
Coercion lit_of_bool : bool >-> base_lit.
-Notation If e0 e1 e2 := (Case e0 [e2;e1]).
+Notation If e0 e1 e2 := (Case e0 (@cons expr e2 (@cons expr e1 (@nil expr)))).
Notation Newlft := (Lit LitUnit) (only parsing).
Notation Endlft := Skip (only parsing).
diff --git a/theories/lang/lib/arc.v b/theories/lang/lib/arc.v
index 0baed576cf670c8d8d33f37b74fa67c9c0ccdbd9..166130461bcf6fb15192e93f21872af20dcb247d 100644
--- a/theories/lang/lib/arc.v
+++ b/theories/lang/lib/arc.v
@@ -130,12 +130,12 @@ Section def.
match st with
| (Some (Cinl (q, strong, wlock)), weak) =>
∃ q', ⌜(q + q')%Qp = 1%Qp⌝ ∗ P1 q' ∗ l ↦ #(Zpos strong) ∗
- if wlock then shift_loc l 1 ↦ #(-1) ∗ ⌜weak = 0%nat⌝
- else shift_loc l 1 ↦ #(S weak)
+ if wlock then (l +ₗ 1) ↦ #(-1) ∗ ⌜weak = 0%nat⌝
+ else (l +ₗ 1) ↦ #(S weak)
| (Some (Cinr _), weak) =>
- l ↦ #0 ∗ shift_loc l 1 ↦ #(S weak)
+ l ↦ #0 ∗ (l +ₗ 1) ↦ #(S weak)
| (None, (S _) as weak) =>
- l ↦ #0 ∗ shift_loc l 1 ↦ #weak ∗ P2
+ l ↦ #0 ∗ (l +ₗ 1) ↦ #weak ∗ P2
| _ => True
end)%I.
@@ -183,7 +183,7 @@ Section arc.
Proof. solve_proper. Qed.
Lemma create_arc E l :
- l ↦ #1 -∗ shift_loc l 1 ↦ #1 -∗ P1 1%Qp ={E}=∗
+ l ↦ #1 -∗ (l +ₗ 1) ↦ #1 -∗ P1 1%Qp ={E}=∗
∃ γ q, is_arc P1 P2 N γ l ∗ P1 q ∗ arc_tok γ q.
Proof using HP1.
iIntros "Hl1 Hl2 [HP1 HP1']".
@@ -195,7 +195,7 @@ Section arc.
Qed.
Lemma create_weak E l :
- l ↦ #0 -∗ shift_loc l 1 ↦ #1 -∗ P2 ={E}=∗ ∃ γ, is_arc P1 P2 N γ l ∗ weak_tok γ.
+ l ↦ #0 -∗ (l +ₗ 1) ↦ #1 -∗ P2 ={E}=∗ ∃ γ, is_arc P1 P2 N γ l ∗ weak_tok γ.
Proof.
iIntros "Hl1 Hl2 HP2".
iMod (own_alloc ((● (None, 1%nat) ⋅ ◯ (None, 1%nat)))) as (γ) "[H● H◯]"; first done.
@@ -345,9 +345,9 @@ Section arc.
{{{ P }}} clone_weak [ #l] {{{ RET #(); P ∗ weak_tok γ }}}.
Proof.
iIntros "#INV #Hacc !# * HP HΦ". iLöb as "IH". wp_rec. wp_op. wp_bind (!ˢᶜ_)%E.
- iAssert (□ (P ={⊤,⊤∖↑N}=∗ ∃ w : Z, shift_loc l 1 ↦ #w ∗
- (shift_loc l 1 ↦ #(w + 1) ={⊤∖↑N,⊤}=∗ P ∗ weak_tok γ) ∧
- (shift_loc l 1 ↦ #w ={⊤∖↑N,⊤}=∗ P)))%I as "#Hproto".
+ iAssert (□ (P ={⊤,⊤∖↑N}=∗ ∃ w : Z, (l +ₗ 1) ↦ #w ∗
+ ((l +ₗ 1) ↦ #(w + 1) ={⊤∖↑N,⊤}=∗ P ∗ weak_tok γ) ∧
+ ((l +ₗ 1) ↦ #w ={⊤∖↑N,⊤}=∗ P)))%I as "#Hproto".
{ iIntros "!# HP". iInv N as (st) "[>H● H]" "Hclose1".
iMod ("Hacc" with "HP") as "[Hown Hclose2]".
iDestruct (weak_tok_auth_val with "H● Hown") as %(st' & weak & -> & Hval).
@@ -437,13 +437,13 @@ Section arc.
Lemma drop_weak_spec (γ : gname) (l : loc) :
is_arc P1 P2 N γ l -∗
{{{ weak_tok γ }}} drop_weak [ #l]
- {{{ (b : bool), RET #b ; if b then P2 ∗ l ↦ #0 ∗ shift_loc l 1 ↦ #0 else True }}}.
+ {{{ (b : bool), RET #b ; if b then P2 ∗ l ↦ #0 ∗ (l +ₗ 1) ↦ #0 else True }}}.
Proof.
iIntros "#INV !# * Hown HΦ". iLöb as "IH". wp_rec. wp_op. wp_bind (!ˢᶜ_)%E.
- iAssert (□ (weak_tok γ ={⊤,⊤ ∖ ↑N}=∗ ∃ w : Z, shift_loc l 1 ↦ #w ∗
- (shift_loc l 1 ↦ #(w - 1) ={⊤ ∖ ↑N,⊤}=∗ ⌜w ≠ 1⌝ ∨
- ▷ P2 ∗ l ↦ #0 ∗ shift_loc l 1 ↦ #0) ∧
- (shift_loc l 1 ↦ #w ={⊤ ∖ ↑N,⊤}=∗ weak_tok γ)))%I as "#Hproto".
+ iAssert (□ (weak_tok γ ={⊤,⊤ ∖ ↑N}=∗ ∃ w : Z, (l +ₗ 1) ↦ #w ∗
+ ((l +ₗ 1) ↦ #(w - 1) ={⊤ ∖ ↑N,⊤}=∗ ⌜w ≠ 1⌝ ∨
+ ▷ P2 ∗ l ↦ #0 ∗ (l +ₗ 1) ↦ #0) ∧
+ ((l +ₗ 1) ↦ #w ={⊤ ∖ ↑N,⊤}=∗ weak_tok γ)))%I as "#Hproto".
{ iIntros "!# Hown". iInv N as (st) "[>H● H]" "Hclose1".
iDestruct (weak_tok_auth_val with "H● Hown") as %(st' & weak & -> & Hval).
destruct st' as [[[[??][?|]]| |]|]; try done; [|iExists _..].
@@ -565,7 +565,7 @@ Section arc.
is_arc P1 P2 N γ l -∗
{{{ arc_tok γ q ∗ P1 q }}} is_unique [ #l]
{{{ (b : bool), RET #b ;
- if b then l ↦ #1 ∗ shift_loc l 1 ↦ #1 ∗ P1 1
+ if b then l ↦ #1 ∗ (l +ₗ 1) ↦ #1 ∗ P1 1
else arc_tok γ q ∗ P1 q }}}.
Proof using HP1.
iIntros "#INV !# * [Hown HP1] HΦ". wp_rec. wp_bind (CAS _ _ _). wp_op.
@@ -627,7 +627,7 @@ Section arc.
{{{ (x : fin 3), RET #x ;
match x : nat with
(* No other reference : we get everything. *)
- | 0%nat => l ↦ #1 ∗ shift_loc l 1 ↦ #1 ∗ P1 1
+ | 0%nat => l ↦ #1 ∗ (l +ₗ 1) ↦ #1 ∗ P1 1
(* No other strong, but there are weaks : we get P1,
plus the option to get a weak if we pay P2. *)
| 1%nat => P1 1 ∗ (P2 ={⊤}=∗ weak_tok γ)
diff --git a/theories/lang/lib/lock.v b/theories/lang/lib/lock.v
index 446804dd553e52135cb910c9840394951e459da1..3832cceb397aec08844896d6e0ebc26d86ce272b 100644
--- a/theories/lang/lib/lock.v
+++ b/theories/lang/lib/lock.v
@@ -73,7 +73,7 @@ Section proof.
Lemma try_acquire_spec E l R P :
□ (P ={E,∅}=∗ ▷ lock_proto l R ∗ (▷ lock_proto l R ={∅,E}=∗ P)) -∗
{{{ P }}} try_acquire [ #l ] @ E
- {{{ b, RET #b; (if b is true then ▷ R else True) ∗ P }}}.
+ {{{ b, RET #b; (if b is true then R else True) ∗ P }}}.
Proof.
iIntros "#Hproto !# * HP HΦ".
wp_rec. iMod ("Hproto" with "HP") as "(Hinv & Hclose)".
@@ -88,7 +88,7 @@ Section proof.
Lemma acquire_spec E l R P :
□ (P ={E,∅}=∗ ▷ lock_proto l R ∗ (▷ lock_proto l R ={∅,E}=∗ P)) -∗
- {{{ P }}} acquire [ #l ] @ E {{{ RET #(); ▷ R ∗ P }}}.
+ {{{ P }}} acquire [ #l ] @ E {{{ RET #(); R ∗ P }}}.
Proof.
iIntros "#Hproto !# * HP HΦ". iLöb as "IH". wp_rec.
wp_apply (try_acquire_spec with "Hproto HP"). iIntros ([]).
diff --git a/theories/lang/lib/new_delete.v b/theories/lang/lib/new_delete.v
index c78267bc645c26dfecbbbda6405529bb0457d01c..dfe6bc79bc4bb09c41b0b2a06b7f02e555621689 100644
--- a/theories/lang/lib/new_delete.v
+++ b/theories/lang/lib/new_delete.v
@@ -45,5 +45,5 @@ Notation "'letalloc:' x <- e1 'in' e2" :=
((Lam (@cons binder x%E%E%E nil) (x <- e1 ;; e2)) [new [ #1]])%E
(at level 102, x at level 1, e1, e2 at level 150) : expr_scope.
Notation "'letalloc:' x <-{ n } ! e1 'in' e2" :=
- ((Lam (@cons binder x%E%E%E nil) (x <-{n%Z%V} !e1 ;; e2)) [new [ #n]])%E
+ ((Lam (@cons binder x%E%E%E nil) (x <-{n%Z%V%L} !e1 ;; e2)) [new [ #n]])%E
(at level 102, x at level 1, e1, e2 at level 150) : expr_scope.
diff --git a/theories/lang/lib/spawn.v b/theories/lang/lib/spawn.v
index 2716c48b70bcb8537c1aea9583b383c765add0d9..34a1ef5269a778f88c62114d868dac7f74b01cfc 100644
--- a/theories/lang/lib/spawn.v
+++ b/theories/lang/lib/spawn.v
@@ -41,10 +41,10 @@ Context `{!lrustG Σ, !spawnG Σ} (N : namespace).
Definition spawn_inv (γf γj : gname) (c : loc) (Ψ : val → iProp Σ) : iProp Σ :=
(own γf (Excl ()) ∗ own γj (Excl ()) ∨
∃ b, c ↦ #(lit_of_bool b) ∗
- if b then ∃ v, shift_loc c 1 ↦ v ∗ Ψ v ∗ own γf (Excl ()) else True)%I.
+ if b then ∃ v, (c +ₗ 1) ↦ v ∗ Ψ v ∗ own γf (Excl ()) else True)%I.
Definition finish_handle (c : loc) (Ψ : val → iProp Σ) : iProp Σ :=
- (∃ γf γj v, own γf (Excl ()) ∗ shift_loc c 1 ↦ v ∗ inv N (spawn_inv γf γj c Ψ))%I.
+ (∃ γf γj v, own γf (Excl ()) ∗ (c +ₗ 1) ↦ v ∗ inv N (spawn_inv γf γj c Ψ))%I.
Definition join_handle (c : loc) (Ψ : val → iProp Σ) : iProp Σ :=
(∃ γf γj Ψ', own γj (Excl ()) ∗ † c … 2 ∗ inv N (spawn_inv γf γj c Ψ') ∗
diff --git a/theories/lang/lifting.v b/theories/lang/lifting.v
index 2d5be6071012b5d70ec241328bd8642fc4d5d272..0f3f69a7b78dd96b4486c6afcbd04627d7254f42 100644
--- a/theories/lang/lifting.v
+++ b/theories/lang/lifting.v
@@ -240,19 +240,6 @@ Proof.
iApply step_fupd_intro; done.
Qed.
-(*
-Lemma wp_bin_op_heap E σ op l1 l2 l' :
- bin_op_eval σ op l1 l2 l' →
- {{{ ▷ ownP σ }}} BinOp op (Lit l1) (Lit l2) @ E
- {{{ l'', RET LitV l''; ⌜bin_op_eval σ op l1 l2 l''⌝ ∗ ownP σ }}}.
-Proof.
- iIntros (? Φ) "HP HΦ". iApply ownP_lift_atomic_head_step; eauto.
- iFrame "HP". iNext. iIntros (e2 σ2 efs Hs) "Ho".
- inv_head_step; rewrite big_sepL_nil right_id.
- iApply "HΦ". eauto.
-Qed.
-*)
-
Lemma wp_bin_op_pure E op l1 l2 l' :
(∀ σ, bin_op_eval σ op l1 l2 l') →
{{{ True }}} BinOp op (Lit l1) (Lit l2) @ E
@@ -320,8 +307,24 @@ Proof.
* by iFrame.
Qed.
+Lemma wp_eq_loc_0_r E (l : loc) P Φ :
+ (P -∗ ▷ Φ (LitV false)) →
+ P -∗ WP BinOp EqOp (Lit (LitLoc l)) (Lit (LitInt 0)) @ E {{ Φ }}.
+Proof.
+ iIntros (HΦ) "HP". iApply wp_bin_op_pure. by intros; do 2 constructor.
+ rewrite HΦ. iNext. iIntros (?? Heval). by inversion_clear Heval; inv_lit.
+Qed.
+
+Lemma wp_eq_loc_0_l E (l : loc) P Φ :
+ (P -∗ ▷ Φ (LitV false)) →
+ P -∗ WP BinOp EqOp (Lit (LitInt 0)) (Lit (LitLoc l)) @ E {{ Φ }}.
+Proof.
+ iIntros (HΦ) "HP". iApply wp_bin_op_pure. by intros; do 2 constructor.
+ rewrite HΦ. iNext. iIntros (?? Heval). by inversion_clear Heval; inv_lit.
+Qed.
+
Lemma wp_offset E l z Φ :
- ▷ Φ (LitV $ LitLoc $ shift_loc l z) -∗
+ ▷ Φ (LitV $ LitLoc $ l +ₗ z) -∗
WP BinOp OffsetOp (Lit $ LitLoc l) (Lit $ LitInt z) @ E {{ Φ }}.
Proof.
iIntros "HP". iApply wp_bin_op_pure; first by econstructor.
diff --git a/theories/lang/notation.v b/theories/lang/notation.v
index 01f305780a99ae4f6fba2f60f8aae67c0263702c..46f57ef61ac424a0360e85228b79a48c20a3b8ab 100644
--- a/theories/lang/notation.v
+++ b/theories/lang/notation.v
@@ -20,8 +20,8 @@ Notation "[ x1 ; x2 ; .. ; xn ]" :=
(* No scope for the values, does not conflict and scope is often not inferred
properly. *)
-Notation "# l" := (LitV l%Z%V) (at level 8, format "# l").
-Notation "# l" := (Lit l%Z%V) (at level 8, format "# l") : expr_scope.
+Notation "# l" := (LitV l%Z%V%L) (at level 8, format "# l").
+Notation "# l" := (Lit l%Z%V%L) (at level 8, format "# l") : expr_scope.
(** Syntax inspired by Coq/Ocaml. Constructions with higher precedence come
first. *)
diff --git a/theories/lang/proofmode.v b/theories/lang/proofmode.v
index 843c7a55275dbf4fc5c0c91a01cf59b40be2adb2..6ed7298bad4ccf3d97298e9569a4de78b6a8fd25 100644
--- a/theories/lang/proofmode.v
+++ b/theories/lang/proofmode.v
@@ -96,6 +96,10 @@ Tactic Notation "wp_op" :=
wp_bind_core K; apply wp_eq_int; wp_finish
| BinOp EqOp (Lit (LitLoc _)) (Lit (LitLoc _)) =>
wp_bind_core K; apply wp_eq_loc; wp_finish
+ | BinOp EqOp (Lit (LitLoc _)) (Lit (LitInt 0)) =>
+ wp_bind_core K; apply wp_eq_loc_0_r; wp_finish
+ | BinOp EqOp (Lit (LitInt 0)) (Lit (LitLoc _)) =>
+ wp_bind_core K; apply wp_eq_loc_0_l; wp_finish
| BinOp OffsetOp _ _ =>
wp_bind_core K; etrans; [|eapply wp_offset; try fast_done]; wp_finish
| BinOp PlusOp _ _ =>
diff --git a/theories/lang/races.v b/theories/lang/races.v
index 647f112b95a7e8cd4c6d5829cd8c5e361852b21a..5baaf0a70cd1da881274fae33a7745668689dbc9 100644
--- a/theories/lang/races.v
+++ b/theories/lang/races.v
@@ -25,7 +25,7 @@ Inductive next_access_head : expr → state → access_kind * order → loc →
| Access_free n l σ i :
0 ≤ i < n →
next_access_head (Free (Lit $ LitInt n) (Lit $ LitLoc l))
- σ (FreeAcc, Na2Ord) (shift_loc l i).
+ σ (FreeAcc, Na2Ord) (l +ₗ i).
(* Some sanity checks to make sure the definition above is not entirely insensible. *)
Goal ∀ e1 e2 e3 σ, head_reducible (CAS e1 e2 e3) σ →
@@ -139,7 +139,7 @@ Lemma next_access_head_Free_concurent_step e1 e1' e2 e'f σ σ' o1 a2 l :
False.
Proof.
intros Ha1 Hstep Ha2 Hred2.
- assert (FREE : ∀ l n i, 0 ≤ i ∧ i < n → free_mem l (Z.to_nat n) σ !! shift_loc l i = None).
+ assert (FREE : ∀ l n i, 0 ≤ i ∧ i < n → free_mem l (Z.to_nat n) σ !! (l +ₗ i) = None).
{ clear. intros l n i Hi.
replace n with (Z.of_nat (Z.to_nat n)) in Hi by (apply Z2Nat.id; lia).
revert l i Hi. induction (Z.to_nat n) as [|? IH]=>/=l i Hi. lia.
diff --git a/theories/lifetime/at_borrow.v b/theories/lifetime/at_borrow.v
index 01e19df60714cbab72b5e43de6d7615cae58cf23..4148b93e8c6817f8e368232fc1ad9cc64d80877f 100644
--- a/theories/lifetime/at_borrow.v
+++ b/theories/lifetime/at_borrow.v
@@ -9,8 +9,7 @@ Definition at_bor `{invG Σ, lftG Σ} κ 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 } P" := (at_bor κ N P)
- (format "&at{ κ , N } P", at level 20, right associativity) : uPred_scope.
+Notation "&at{ κ , N }" := (at_bor κ N) (format "&at{ κ , N }") : uPred_scope.
Section atomic_bors.
Context `{invG Σ, lftG Σ} (P : iProp Σ) (N : namespace).
@@ -31,9 +30,9 @@ Section atomic_bors.
Global Instance at_bor_persistent : PersistentP (&at{κ, N} P) := _.
Lemma bor_share E κ :
- ↑lftN ⊆ E → N ⊥ lftN → &{κ}P ={E}=∗ &at{κ, N}P.
+ N ⊥ lftN → &{κ}P ={E}=∗ &at{κ, N}P.
Proof.
- iIntros (? HN) "HP". rewrite bor_unfold_idx. iDestruct "HP" as (i) "(#?&Hown)".
+ iIntros (HN) "HP". rewrite bor_unfold_idx. iDestruct "HP" as (i) "(#?&Hown)".
iExists i. iFrame "#".
iLeft. iSplitR. done. by iMod (inv_alloc with "[Hown]") as "$"; auto.
Qed.
diff --git a/theories/lifetime/frac_borrow.v b/theories/lifetime/frac_borrow.v
index 6ff33ee6c813f5d4a09c9ad48e92f85b0350809b..d700003cc32b5fe38a0d9873350941e2e06db6c8 100644
--- a/theories/lifetime/frac_borrow.v
+++ b/theories/lifetime/frac_borrow.v
@@ -8,10 +8,9 @@ Set Default Proof Using "Type".
Class frac_borG Σ := frac_borG_inG :> inG Σ fracR.
Definition frac_bor `{invG Σ, lftG Σ, frac_borG Σ} κ (φ : Qp → iProp Σ) :=
- (∃ γ κ', κ ⊑ κ' ∗ &at{κ',lftN} ∃ q, φ q ∗ own γ q ∗
- (⌜q = 1%Qp⌝ ∨ ∃ q', ⌜(q + q' = 1)%Qp⌝ ∗ q'.[κ']))%I.
-Notation "&frac{ κ } P" := (frac_bor κ P)
- (format "&frac{ κ } P", at level 20, right associativity) : uPred_scope.
+ (∃ γ κ', κ ⊑ κ' ∗ &at{κ',lftN} (∃ q, φ q ∗ own γ q ∗
+ (⌜q = 1%Qp⌝ ∨ ∃ q', ⌜(q + q' = 1)%Qp⌝ ∗ q'.[κ'])))%I.
+Notation "&frac{ κ }" := (frac_bor κ) (format "&frac{ κ }") : uPred_scope.
Section frac_bor.
Context `{invG Σ, lftG Σ, frac_borG Σ} (φ : Qp → iProp Σ).
diff --git a/theories/lifetime/lifetime.v b/theories/lifetime/lifetime.v
index e5cbde2ad42defea9c5918c0724793871cecbb84..e5c15254f70b1af38916ca4e0a67ef4889f1fb26 100644
--- a/theories/lifetime/lifetime.v
+++ b/theories/lifetime/lifetime.v
@@ -26,6 +26,21 @@ Section derived.
Context `{invG Σ, lftG Σ}.
Implicit Types κ : lft.
+Lemma bor_acc_atomic_cons E κ P :
+ ↑lftN ⊆ E →
+ lft_ctx -∗ &{κ} P ={E,E∖↑lftN}=∗
+ (▷ P ∗ ∀ Q, ▷ (▷ Q ={∅}=∗ ▷ P) -∗ ▷ Q ={E∖↑lftN,E}=∗ &{κ} Q) ∨
+ ([†κ] ∗ |={E∖↑lftN,E}=> True).
+Proof.
+ iIntros (?) "#LFT HP".
+ iMod (bor_acc_atomic_strong with "LFT HP") as "[H|[??]]"; first done.
+ - iLeft. iDestruct "H" as (κ') "(#Hκκ' & $ & Hclose)". iIntros "!>* HPQ HQ".
+ iMod ("Hclose" with "[HPQ] HQ") as "Hb".
+ + iNext. iIntros "? _". by iApply "HPQ".
+ + iApply (bor_shorten with "Hκκ' Hb").
+ - iRight. by iFrame.
+Qed.
+
Lemma bor_acc_atomic E κ P :
↑lftN ⊆ E →
lft_ctx -∗ &{κ}P ={E,E∖↑lftN}=∗
@@ -60,7 +75,7 @@ Qed.
Lemma bor_exists {A} (Φ : A → iProp Σ) `{!Inhabited A} E κ :
↑lftN ⊆ E →
- lft_ctx -∗ &{κ}(∃ x, Φ x) ={E}=∗ ∃ x, &{κ}Φ x.
+ lft_ctx -∗ &{κ}(∃ x, Φ x) ={E}=∗ ∃ x, &{κ}(Φ x).
Proof.
iIntros (?) "#LFT Hb".
iMod (bor_acc_atomic_cons with "LFT Hb") as "[H|[H† >_]]"; first done.
@@ -95,6 +110,34 @@ Proof.
- iIntros "!> !>". iMod "Hclose" as "_". by iApply (bor_fake with "LFT").
Qed.
+Lemma bor_later_tok E q κ P :
+ ↑lftN ⊆ E →
+ lft_ctx -∗ &{κ}(▷ P) -∗ q.[κ] ={E}▷=∗ &{κ}P ∗ q.[κ].
+Proof.
+ iIntros (?) "#LFT Hb Htok".
+ iMod (bor_acc_cons with "LFT Hb Htok") as "[HP Hclose]"; first done.
+ iModIntro. iNext. iApply ("Hclose" with "[] HP"). by iIntros "!> $".
+Qed.
+
+Lemma bor_persistent P `{!PersistentP P} E κ :
+ ↑lftN ⊆ E →
+ lft_ctx -∗ &{κ}P ={E}=∗ ▷ P ∨ [†κ].
+Proof.
+ iIntros (?) "#LFT Hb".
+ iMod (bor_acc_atomic with "LFT Hb") as "[[#HP Hob]|[#H† Hclose]]"; first done.
+ - iMod ("Hob" with "HP") as "_". auto.
+ - iMod "Hclose" as "_". auto.
+Qed.
+
+Lemma bor_persistent_tok P `{!PersistentP P} E κ q :
+ ↑lftN ⊆ E →
+ lft_ctx -∗ &{κ}P -∗ q.[κ] ={E}=∗ ▷ P ∗ q.[κ].
+Proof.
+ iIntros (?) "#LFT Hb Htok".
+ iMod (bor_acc with "LFT Hb Htok") as "[#HP Hob]"; first done.
+ by iMod ("Hob" with "HP") as "[_ $]".
+Qed.
+
Lemma later_bor_static E P :
↑lftN ⊆ E →
lft_ctx -∗ ▷ P ={E}=∗ &{static} P.
@@ -110,15 +153,6 @@ Proof.
iApply lft_tok_static.
Qed.
-Lemma bor_later_tok E q κ P :
- ↑lftN ⊆ E →
- lft_ctx -∗ &{κ}(▷ P) -∗ q.[κ] ={E}▷=∗ &{κ}P ∗ q.[κ].
-Proof.
- iIntros (?) "#LFT Hb Htok".
- iMod (bor_acc_cons with "LFT Hb Htok") as "[HP Hclose]"; first done.
- iModIntro. iNext. iApply ("Hclose" with "[] HP"). by iIntros "!> $".
-Qed.
-
Lemma rebor E κ κ' P :
↑lftN ⊆ E →
lft_ctx -∗ κ' ⊑ κ -∗ &{κ}P ={E}=∗ &{κ'}P ∗ ([†κ'] ={E}=∗ &{κ}P).
@@ -134,36 +168,15 @@ Qed.
Lemma bor_unnest E κ κ' P :
↑lftN ⊆ E →
- lft_ctx -∗ &{κ'} &{κ} P ={E}▷=∗ &{κ ⊓ κ'} P.
+ lft_ctx -∗ &{κ'} (&{κ} P) ={E}▷=∗ &{κ ⊓ κ'} P.
Proof.
iIntros (?) "#LFT Hbor".
- iMod (bor_acc_atomic_cons with "LFT Hbor") as
- "[[Hbor Hclose]|[H† Hclose]]"; first done.
- - rewrite ->bor_unfold_idx. iDestruct "Hbor" as (i) "[#Hidx Hbor]".
- iMod ("Hclose" with "[] Hbor") as "Hbor".
- { iIntros "!> H". rewrite bor_unfold_idx. auto with iFrame. }
- iIntros "!>"; iNext. by iApply (idx_bor_unnest with "LFT Hidx Hbor").
- - iMod "Hclose" as "_". iApply (bor_fake with "LFT"); first done.
- rewrite -lft_dead_or. auto.
-Qed.
-
-Lemma bor_persistent P `{!PersistentP P} E κ :
- ↑lftN ⊆ E →
- lft_ctx -∗ &{κ}P ={E}=∗ ▷ P ∨ [†κ].
-Proof.
- iIntros (?) "#LFT Hb".
- iMod (bor_acc_atomic with "LFT Hb") as "[[#HP Hob]|[#H† Hclose]]"; first done.
- - iMod ("Hob" with "HP") as "_". auto.
- - iMod "Hclose" as "_". auto.
-Qed.
-
-Lemma bor_persistent_tok P `{!PersistentP P} E κ q :
- ↑lftN ⊆ E →
- lft_ctx -∗ &{κ}P -∗ q.[κ] ={E}=∗ ▷ P ∗ q.[κ].
-Proof.
- iIntros (?) "#LFT Hb Htok".
- iMod (bor_acc with "LFT Hb Htok") as "[#HP Hob]"; first done.
- by iMod ("Hob" with "HP") as "[_ $]".
+ rewrite ->(bor_unfold_idx _ P).
+ iMod (bor_exists with "LFT Hbor") as (i) "Hbor"; [done|].
+ iMod (bor_sep with "LFT Hbor") as "[Hidx Hbor]"; [done|].
+ iMod (bor_persistent with "LFT Hidx") as "#[Hidx|H†]"; [done| |].
+ - iIntros "!>". iNext. by iApply (idx_bor_unnest with "LFT Hidx Hbor").
+ - iApply (bor_fake with "LFT"); [done|]. rewrite -lft_dead_or. auto.
Qed.
Lemma lft_incl_static κ : (κ ⊑ static)%I.
@@ -181,4 +194,18 @@ Proof.
- iApply lft_incl_trans; last iApply IH. (* FIXME: Why does "done" not do this? Looks like "assumption" to me. *)
iApply lft_intersect_incl_r.
Qed.
+
+Lemma lft_eternalize E q κ :
+ q.[κ] ={E}=∗ static ⊑ κ.
+Proof.
+ iIntros "Hκ". iMod (inv_alloc lftN _ (∃ q, q.[κ])%I with "[Hκ]") as "#Hnv".
+ { iExists _. done. }
+ iApply lft_incl_intro. iIntros "!> !#". iSplitL.
+ - iIntros (q') "$". iInv lftN as ">Hκ" "Hclose". iDestruct "Hκ" as (q'') "[Hκ1 Hκ2]".
+ iMod ("Hclose" with "[Hκ2]") as "_". { iExists _. done. }
+ iModIntro. iExists _. iFrame. iIntros "_". done.
+ - iIntros "H†". iInv lftN as ">Hκ" "_". iDestruct "Hκ" as (q'') "Hκ".
+ iDestruct (lft_tok_dead with "Hκ H†") as "[]".
+Qed.
+
End derived.
diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index 22f12192c9d38d48c101d9ca345effa079700d76..af69eaed4e0503b63a0d2553d041b8b8602979e3 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -5,9 +5,6 @@ From iris.base_logic.lib Require Import boxes fractional.
Set Default Proof Using "Type".
Definition lftN : namespace := nroot .@ "lft".
-Definition borN : namespace := lftN .@ "bor".
-Definition inhN : namespace := lftN .@ "inh".
-Definition mgmtN : namespace := lftN .@ "mgmt".
Module Type lifetime_sig.
(** CMRAs needed by the lifetime logic *)
@@ -42,10 +39,8 @@ Module Type lifetime_sig.
(format "q .[ κ ]", at level 0) : uPred_scope.
Notation "[† κ ]" := (lft_dead κ) (format "[† κ ]"): uPred_scope.
- Notation "&{ κ } P" := (bor κ P)
- (format "&{ κ } P", at level 20, right associativity) : uPred_scope.
- Notation "&{ κ , i } P" := (idx_bor κ i P)
- (format "&{ κ , i } P", at level 20, right associativity) : uPred_scope.
+ Notation "&{ κ }" := (bor κ) (format "&{ κ }") : uPred_scope.
+ Notation "&{ κ , i }" := (idx_bor κ i) (format "&{ κ , i }") : uPred_scope.
Infix "⊑" := lft_incl (at level 70) : uPred_scope.
Infix "⊓" := lft_intersect (at level 40) : C_scope.
@@ -65,12 +60,12 @@ Module Type lifetime_sig.
Global Declare Instance lft_intersect_right_id : RightId eq static lft_intersect.
Global Declare Instance lft_ctx_persistent : PersistentP lft_ctx.
- Global Declare Instance lft_dead_persistent κ : PersistentP (lft_dead κ).
+ Global Declare Instance lft_dead_persistent κ : PersistentP ([†κ]).
Global Declare Instance lft_incl_persistent κ κ' : PersistentP (κ ⊑ κ').
- Global Declare Instance idx_bor_persistent κ i P : PersistentP (idx_bor κ i P).
+ Global Declare Instance idx_bor_persistent κ i P : PersistentP (&{κ,i} P).
- Global Declare Instance lft_tok_timeless q κ : TimelessP (lft_tok q κ).
- Global Declare Instance lft_dead_timeless κ : TimelessP (lft_dead κ).
+ Global Declare Instance lft_tok_timeless q κ : TimelessP (q.[κ]).
+ Global Declare Instance lft_dead_timeless κ : TimelessP ([†κ]).
Global Declare Instance idx_bor_own_timeless q i : TimelessP (idx_bor_own q i).
Global Instance idx_bor_params : Params (@idx_bor) 5.
@@ -118,7 +113,7 @@ Module Type lifetime_sig.
Parameter idx_bor_iff : ∀ κ i P P', ▷ □ (P ↔ P') -∗ &{κ,i}P -∗ &{κ,i}P'.
Parameter idx_bor_unnest : ∀ E κ κ' i P,
- ↑lftN ⊆ E → lft_ctx -∗ &{κ,i} P -∗ &{κ'} idx_bor_own 1 i ={E}=∗ &{κ ⊓ κ'} P.
+ ↑lftN ⊆ E → lft_ctx -∗ &{κ,i} P -∗ &{κ'}(idx_bor_own 1 i) ={E}=∗ &{κ ⊓ κ'} P.
Parameter idx_bor_acc : ∀ E q κ i P, ↑lftN ⊆ E →
lft_ctx -∗ &{κ,i}P -∗ idx_bor_own 1 i -∗ q.[κ] ={E}=∗
@@ -151,14 +146,8 @@ Module Type lifetime_sig.
↑lftN ⊆ E → κ ⊑ κ' -∗ q.[κ] ={E}=∗ ∃ q', q'.[κ'] ∗ (q'.[κ'] ={E}=∗ q.[κ]).
Parameter lft_incl_dead : ∀ E κ κ', ↑lftN ⊆ E → κ ⊑ κ' -∗ [†κ'] ={E}=∗ [†κ].
Parameter lft_incl_intro : ∀ κ κ',
- □ ((∀ q, lft_tok q κ ={↑lftN}=∗ ∃ q',
- lft_tok q' κ' ∗ (lft_tok q' κ' ={↑lftN}=∗ lft_tok q κ)) ∗
- (lft_dead κ' ={↑lftN}=∗ lft_dead κ)) -∗ κ ⊑ κ'.
- (* Same for some of the derived lemmas. *)
- Parameter bor_acc_atomic_cons : ∀ E κ P,
- ↑lftN ⊆ E → lft_ctx -∗ &{κ} P ={E,E∖↑lftN}=∗
- (▷ P ∗ ∀ Q, ▷ (▷ Q ={∅}=∗ ▷ P) -∗ ▷ Q ={E∖↑lftN,E}=∗ &{κ} Q) ∨
- ([†κ] ∗ |={E∖↑lftN,E}=> True).
+ □ ((∀ q, q.[κ] ={↑lftN}=∗ ∃ q', q'.[κ'] ∗ (q'.[κ'] ={↑lftN}=∗ q.[κ])) ∗
+ ([†κ'] ={↑lftN}=∗ [†κ])) -∗ κ ⊑ κ'.
End properties.
diff --git a/theories/lifetime/model/accessors.v b/theories/lifetime/model/accessors.v
index 053a65ce864f967aae570d6f37d2b7c67da88832..1dbe120693d240af40513016a8e528b6c35122a1 100644
--- a/theories/lifetime/model/accessors.v
+++ b/theories/lifetime/model/accessors.v
@@ -262,20 +262,4 @@ Proof.
+ iMod (lft_incl_dead with "Hle H†") as "$". done.
iApply fupd_intro_mask'. solve_ndisj.
Qed.
-
-(* These derived lemmas are needed inside the model. *)
-Lemma bor_acc_atomic_cons E κ P :
- ↑lftN ⊆ E →
- lft_ctx -∗ &{κ} P ={E,E∖↑lftN}=∗
- (▷ P ∗ ∀ Q, ▷ (▷ Q ={∅}=∗ ▷ P) -∗ ▷ Q ={E∖↑lftN,E}=∗ &{κ} Q) ∨
- ([†κ] ∗ |={E∖↑lftN,E}=> True).
-Proof.
- iIntros (?) "#LFT HP".
- iMod (bor_acc_atomic_strong with "LFT HP") as "[H|[??]]"; first done.
- - iLeft. iDestruct "H" as (κ') "(#Hκκ' & $ & Hclose)". iIntros "!>* HPQ HQ".
- iMod ("Hclose" with "[HPQ] HQ") as "Hb".
- + iNext. iIntros "? _". by iApply "HPQ".
- + iApply (bor_shorten with "Hκκ' Hb").
- - iRight. by iFrame.
-Qed.
End accessors.
diff --git a/theories/lifetime/model/borrow_sep.v b/theories/lifetime/model/borrow_sep.v
index 20be9317c7988774a7ccfdb04f234a333a62d84f..fd37a3f7913483041b27cd3e4d9c849183448995 100644
--- a/theories/lifetime/model/borrow_sep.v
+++ b/theories/lifetime/model/borrow_sep.v
@@ -78,9 +78,9 @@ Lemma bor_combine E κ P Q :
Proof.
iIntros (?) "#LFT HP HQ". rewrite {1 2}/bor.
iDestruct "HP" as (κ1) "[#Hκ1 Hbor1]". iDestruct "HQ" as (κ2) "[#Hκ2 Hbor2]".
- iMod (raw_rebor _ _ (κ1 ⊓ κ2) with "LFT Hbor1") as "[Hbor1 _]".
+ iMod (raw_bor_shorten _ _ (κ1 ⊓ κ2) with "LFT Hbor1") as "Hbor1".
done. by apply gmultiset_union_subseteq_l.
- iMod (raw_rebor _ _ (κ1 ⊓ κ2) with "LFT Hbor2") as "[Hbor2 _]".
+ iMod (raw_bor_shorten _ _ (κ1 ⊓ κ2) with "LFT Hbor2") as "Hbor2".
done. by apply gmultiset_union_subseteq_r.
iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose". unfold raw_bor, idx_bor_own.
iDestruct "Hbor1" as (j1) "[Hbor1 Hslice1]". iDestruct "Hbor2" as (j2) "[Hbor2 Hslice2]".
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index f4a620bcf1041a21ac4ee38c3bb20de01bdfac8c..befd40f28d4c8ee8d84a3d866cec362051e34427 100644
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -13,13 +13,13 @@ Implicit Types κ : lft.
Lemma lft_kill (I : gmap lft lft_names) (K K' : gset lft) (κ : lft) :
let Iinv := (
own_ilft_auth I ∗
- ([∗ set] κ' ∈ K, lft_inv_alive κ') ∗
- ([∗ set] κ' ∈ K', lft_inv_dead κ'))%I in
- (∀ κ', is_Some (I !! κ') → κ' ⊂ κ → κ' ∈ K) →
- (∀ κ', is_Some (I !! κ') → κ ⊂ κ' → κ' ∈ K') →
+ ([∗ set] κ' ∈ K, lft_inv_dead κ') ∗
+ ([∗ set] κ' ∈ K', lft_inv_alive κ'))%I in
+ (∀ κ', is_Some (I !! κ') → κ ⊂ κ' → κ' ∈ K) →
+ (∀ κ', is_Some (I !! κ') → κ' ⊂ κ → κ' ∈ K') →
Iinv -∗ lft_inv_alive κ -∗ [†κ] ={↑borN ∪ ↑inhN}=∗ Iinv ∗ lft_inv_dead κ.
Proof.
- iIntros (Iinv HK HK') "(HI & Halive & Hdead) Hlalive Hκ".
+ iIntros (Iinv HK HK') "(HI & Hdead & Halive) Hlalive Hκ".
rewrite lft_inv_alive_unfold;
iDestruct "Hlalive" as (P Q) "(Hbor & Hvs & Hinh)".
rewrite /lft_bor_alive; iDestruct "Hbor" as (B) "(Hbox & Hbor & HB)".
@@ -57,14 +57,14 @@ Qed.
Lemma lfts_kill A (I : gmap lft lft_names) (K K' : gset lft) :
let Iinv K' := (own_ilft_auth I ∗ [∗ set] κ' ∈ K', lft_inv_alive κ')%I in
+ K ⊥ K' →
(∀ κ κ', κ ∈ K → is_Some (I !! κ') → κ ⊆ κ' → κ' ∈ K) →
- (∀ κ κ', κ ∈ K → lft_alive_in A κ → is_Some (I !! κ') →
- κ' ∉ K → κ' ⊂ κ → κ' ∈ K') →
+ (∀ κ, lft_alive_in A κ → is_Some (I !! κ) → κ ∉ K → κ ∈ K') →
Iinv K' -∗ ([∗ set] κ ∈ K, lft_inv A κ ∗ [†κ])
={↑borN ∪ ↑inhN}=∗ Iinv K' ∗ [∗ set] κ ∈ K, lft_inv_dead κ.
Proof.
intros Iinv. revert K'.
- induction (collection_wf K) as [K _ IH]=> K' HK HK'.
+ induction (collection_wf K) as [K _ IH]=> K' HKK' HK HK'.
iIntros "[HI Halive] HK".
pose (Kalive := filter (lft_alive_in A) K).
destruct (decide (Kalive = ∅)) as [HKalive|].
@@ -75,31 +75,28 @@ Proof.
as (κ & [Hκalive HκK]%elem_of_filter & Hκmin); first done.
iDestruct (@big_sepS_delete with "HK") as "[[Hκinv Hκ] HK]"; first done.
iDestruct (lft_inv_alive_in with "Hκinv") as "Hκalive"; first done.
- iAssert ⌜κ ∉ K'⌝%I with "[#]" as %HκK'.
- { iIntros (Hκ). iApply (lft_inv_alive_twice κ with "Hκalive").
- by iApply (@big_sepS_elem_of with "Halive"). }
+ assert (κ ∉ K') as HκK' by set_solver +HκK HKK'.
specialize (IH (K ∖ {[ κ ]})). feed specialize IH; [set_solver +HκK|].
iMod (IH ({[ κ ]} ∪ K') with "[HI Halive Hκalive] HK") as "[[HI Halive] Hdead]".
+ { set_solver +HKK'. }
{ intros κ' κ''.
rewrite !elem_of_difference !elem_of_singleton=> -[? Hneq] ??.
split; [by eauto|]; intros ->.
eapply (minimal_strict_1 _ _ κ' Hκmin), strict_spec_alt; eauto.
apply elem_of_filter; eauto using lft_alive_in_subseteq. }
- { intros κ' κ'' Hκ' ? [γs'' ?].
- destruct (decide (κ'' = κ)) as [->|]; [set_solver +|].
- move: Hκ'; rewrite not_elem_of_difference elem_of_difference
- elem_of_union not_elem_of_singleton elem_of_singleton.
- intros [??] [?|?]; eauto. }
+ { intros κ' Hκ'. destruct (decide (κ' = κ)) as [->|Hκκ']; [set_solver +|].
+ specialize (HK' _ Hκ'). set_solver +Hκκ' HK'. }
{ rewrite /Iinv big_sepS_insert //. iFrame. }
iDestruct (@big_sepS_insert with "Halive") as "[Hκalive Halive]"; first done.
iMod (lft_kill with "[$HI $Halive $Hdead] Hκalive Hκ")
as "[(HI&Halive&Hdead) Hκdead]".
- { intros κ' ??. eapply (HK' κ); eauto.
- intros ?. eapply (minimal_strict_1 _ _ _ Hκmin); eauto.
- apply elem_of_filter; split; last done.
- eapply lft_alive_in_subseteq, gmultiset_subset_subseteq; eauto. }
{ intros κ' ? [??]%strict_spec_alt.
rewrite elem_of_difference elem_of_singleton; eauto. }
+ { intros κ' ??. eapply HK'; [|done|].
+ - by eapply lft_alive_in_subseteq, gmultiset_subset_subseteq.
+ - intros ?. eapply (minimal_strict_1 _ _ _ Hκmin); eauto.
+ apply elem_of_filter; split; last done.
+ eapply lft_alive_in_subseteq, gmultiset_subset_subseteq; eauto. }
iModIntro. rewrite /Iinv (big_sepS_delete _ K) //. iFrame.
Qed.
@@ -108,28 +105,6 @@ Definition kill_set (I : gmap lft lft_names) (Λ : atomic_lft) : gset lft :=
Lemma elem_of_kill_set I Λ κ : κ ∈ kill_set I Λ ↔ Λ ∈ κ ∧ is_Some (I !! κ).
Proof. by rewrite /kill_set elem_of_filter elem_of_dom. Qed.
-Lemma kill_set_subseteq I Λ : kill_set I Λ ⊆ dom (gset lft) I.
-Proof. intros κ [??]%elem_of_kill_set. by apply elem_of_dom. Qed.
-
-Definition down_close (A : gmap atomic_lft bool)
- (I : gmap lft lft_names) (K : gset lft) : gset lft :=
- filter (λ κ, κ ∉ K ∧
- set_Exists (λ κ', κ ⊂ κ' ∧ lft_alive_in A κ') K) (dom (gset lft) I).
-Lemma elem_of_down_close A I K κ :
- κ ∈ down_close A I K ↔
- is_Some (I !! κ) ∧ κ ∉ K ∧ ∃ κ', κ' ∈ K ∧ κ ⊂ κ' ∧ lft_alive_in A κ'.
-Proof. rewrite /down_close elem_of_filter elem_of_dom /set_Exists. tauto. Qed.
-
-Lemma down_close_lft_alive_in A I K κ : κ ∈ down_close A I K → lft_alive_in A κ.
-Proof.
- rewrite elem_of_down_close; intros (?&?&?&?&?&?).
- eapply lft_alive_in_subseteq, gmultiset_subset_subseteq; eauto.
-Qed.
-Lemma down_close_disjoint A I K : K ⊥ down_close A I K.
-Proof. intros κ. rewrite elem_of_down_close. naive_solver. Qed.
-Lemma down_close_subseteq A I K :
- down_close A I K ⊆ dom (gset lft) I.
-Proof. intros κ [??]%elem_of_down_close. by apply elem_of_dom. Qed.
Lemma lft_create E :
↑lftN ⊆ E →
@@ -160,28 +135,28 @@ Proof.
{ by eapply auth_update, singleton_local_update,
(exclusive_local_update _ (Cinr ())). }
iDestruct "HΛ" as "#HΛ". iModIntro; iNext.
- pose (K := kill_set I Λ); pose (K' := down_close A I K).
- assert (K ⊥ K') by (by apply down_close_disjoint).
- destruct (proj1 (subseteq_disjoint_union_L (K ∪ K')
- (dom (gset lft) I))) as (K''&HI&?).
- { apply union_least. apply kill_set_subseteq. apply down_close_subseteq. }
+ pose (K := kill_set I Λ).
+ pose (K' := filter (lft_alive_in A) (dom (gset lft) I) ∖ K).
+ destruct (proj1 (subseteq_disjoint_union_L (K ∪ K') (dom (gset lft) I))) as (K''&HI&HK'').
+ { set_solver+. }
+ assert (K ⊥ K') by set_solver+.
rewrite HI !big_sepS_union //. iDestruct "Hinv" as "[[HinvK HinvD] Hinv]".
iAssert ([∗ set] κ ∈ K', lft_inv_alive κ)%I with "[HinvD]" as "HinvD".
{ iApply (@big_sepS_impl with "[$HinvD]"); iIntros "!#".
- iIntros (κ Hκ) "?". iApply lft_inv_alive_in; last done.
- eauto using down_close_lft_alive_in. }
+ iIntros (κ [[Hκ _]%elem_of_filter _]%elem_of_difference) "?".
+ by iApply lft_inv_alive_in. }
iAssert ([∗ set] κ ∈ K, lft_inv A κ ∗ [† κ])%I with "[HinvK]" as "HinvK".
{ iApply (@big_sepS_impl with "[$HinvK]"); iIntros "!#".
iIntros (κ [? _]%elem_of_kill_set) "$". rewrite /lft_dead. eauto. }
iApply fupd_trans. iApply (fupd_mask_mono (↑borN ∪ ↑inhN));
first by apply union_least; solve_ndisj.
iMod (lfts_kill A I K K' with "[$HI $HinvD] HinvK") as "[[HI HinvD] HinvK]".
+ { done. }
{ intros κ κ' [??]%elem_of_kill_set ??. apply elem_of_kill_set.
split; last done. by eapply gmultiset_elem_of_subseteq. }
- { intros κ κ' ?????. apply elem_of_down_close; eauto 10. }
+ { 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 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 //.
@@ -190,19 +165,16 @@ Proof.
iIntros (κ [? _]%elem_of_kill_set) "Hdead". rewrite /lft_inv.
iRight. iFrame. iPureIntro. by apply lft_dead_in_insert_false'.
- iApply (@big_sepS_impl with "[$HinvD]"); iIntros "!#".
- iIntros (κ Hκ) "Halive". rewrite /lft_inv.
- iLeft. iFrame "Halive". iPureIntro.
- assert (lft_alive_in A κ) as Halive by (by eapply down_close_lft_alive_in).
+ iIntros (κ [[Hκ HκI]%elem_of_filter HκK]%elem_of_difference) "Halive".
+ rewrite /lft_inv. iLeft. iFrame "Halive". iPureIntro.
apply lft_alive_in_insert_false; last done.
- apply elem_of_down_close in Hκ as (?&HFOO&_).
- move: HFOO. rewrite elem_of_kill_set. tauto.
+ move: HκK. rewrite elem_of_kill_set -elem_of_dom. set_solver +HκI.
- iApply (@big_sepS_impl with "[$Hinv]"); iIntros "!#".
rewrite /lft_inv. iIntros (κ Hκ) "[[? %]|[? %]]".
+ iLeft. iFrame. iPureIntro.
- apply lft_alive_in_insert_false; last done.
- assert (κ ∉ K). intros ?. eapply H5. 2: eauto. rewrite elem_of_union. eauto.
- move: H7. rewrite elem_of_kill_set not_and_l. intros [?|?]. done.
- contradict H7. apply elem_of_dom. set_solver +HI Hκ.
+ apply lft_alive_in_insert_false; last done. intros ?.
+ assert (κ ∈ K) by (rewrite elem_of_kill_set -elem_of_dom HI elem_of_union; auto).
+ eapply HK'', Hκ. rewrite elem_of_union. auto.
+ iRight. iFrame. iPureIntro. by apply lft_dead_in_insert_false.
Qed.
End creation.
diff --git a/theories/lifetime/model/definitions.v b/theories/lifetime/model/definitions.v
index 7ee2738816323458d685fedf126842a133d8fe6d..41545ef98b54bc8f0c1e275d85cc79005c57b4a1 100644
--- a/theories/lifetime/model/definitions.v
+++ b/theories/lifetime/model/definitions.v
@@ -1,11 +1,14 @@
From iris.algebra Require Import csum auth frac gmap agree gset.
-From iris.algebra Require Import csum auth frac agree gset.
From iris.base_logic Require Import big_op.
From iris.base_logic.lib Require Import boxes.
From lrust.lifetime Require Export lifetime_sig.
Set Default Proof Using "Type".
Import uPred.
+Definition borN : namespace := lftN .@ "bor".
+Definition inhN : namespace := lftN .@ "inh".
+Definition mgmtN : namespace := lftN .@ "mgmt".
+
Definition atomic_lft := positive.
(* HACK : We need to make sure this is not in the top-level context,
so that it does not conflict with the *definition* of [lft] that we
@@ -23,8 +26,6 @@ Inductive bor_state :=
| Bor_in
| Bor_open (q : frac)
| Bor_rebor (κ : lft).
-Instance bor_state_eq_dec : EqDecision bor_state.
-Proof. solve_decision. Defined.
Canonical bor_stateC := leibnizC bor_state.
Record lft_names := LftNames {
@@ -32,8 +33,6 @@ Record lft_names := LftNames {
cnt_name : gname;
inh_name : gname
}.
-Instance lft_names_eq_dec : EqDecision lft_names.
-Proof. solve_decision. Defined.
Canonical lft_namesC := leibnizC lft_names.
Definition lft_stateR := csumR fracR unitR.
@@ -213,10 +212,8 @@ Notation "q .[ κ ]" := (lft_tok q κ)
(format "q .[ κ ]", at level 0) : uPred_scope.
Notation "[† κ ]" := (lft_dead κ) (format "[† κ ]"): uPred_scope.
-Notation "&{ κ } P" := (bor κ P)
- (format "&{ κ } P", at level 20, right associativity) : uPred_scope.
-Notation "&{ κ , i } P" := (idx_bor κ i P)
- (format "&{ κ , i } P", at level 20, right associativity) : uPred_scope.
+Notation "&{ κ }" := (bor κ) (format "&{ κ }") : uPred_scope.
+Notation "&{ κ , i }" := (idx_bor κ i) (format "&{ κ , i }") : uPred_scope.
Infix "⊑" := lft_incl (at level 70) : uPred_scope.
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index 5f77eea264f6416e2bf28b5377e72d86789894f2..54daebe3797c2d929dab3e1c3bc355d7e1066126 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -242,14 +242,6 @@ Proof.
by rewrite HAinsert.
Qed.
-Lemma lft_inv_alive_twice κ : lft_inv_alive κ -∗ lft_inv_alive κ -∗ False.
-Proof.
- rewrite lft_inv_alive_unfold /lft_inh.
- iDestruct 1 as (P Q) "(_&_&Hinh)"; iDestruct 1 as (P' Q') "(_&_&Hinh')".
- iDestruct "Hinh" as (E) "[HE _]"; iDestruct "Hinh'" as (E') "[HE' _]".
- by iDestruct (own_inh_valid_2 with "HE HE'") as %?.
-Qed.
-
Lemma lft_inv_alive_in A κ : lft_alive_in A κ → lft_inv A κ -∗ lft_inv_alive κ.
Proof.
rewrite /lft_inv. iIntros (?) "[[$ _]|[_ %]]".
@@ -330,9 +322,8 @@ Proof.
Qed.
Lemma lft_incl_intro κ κ' :
- □ ((∀ q, lft_tok q κ ={↑lftN}=∗ ∃ q',
- lft_tok q' κ' ∗ (lft_tok q' κ' ={↑lftN}=∗ lft_tok q κ)) ∗
- (lft_dead κ' ={↑lftN}=∗ lft_dead κ)) -∗ κ ⊑ κ'.
+ □ ((∀ q, q.[κ] ={↑lftN}=∗ ∃ q', q'.[κ'] ∗ (q'.[κ'] ={↑lftN}=∗ q.[κ])) ∗
+ ([†κ'] ={↑lftN}=∗ [†κ])) -∗ κ ⊑ κ'.
Proof. reflexivity. Qed.
Lemma lft_intersect_incl_l κ κ': (κ ⊓ κ' ⊑ κ)%I.
diff --git a/theories/lifetime/model/reborrow.v b/theories/lifetime/model/reborrow.v
index e4707eccda1faa7be8fcc9e8b1c3dcb0bf5d7f71..2e7d4d9af3a6f9a6e70a5b304f89c1706070f168 100644
--- a/theories/lifetime/model/reborrow.v
+++ b/theories/lifetime/model/reborrow.v
@@ -60,10 +60,8 @@ Proof.
{ apply auth_update_alloc,
(alloc_singleton_local_update _ j (1%Qp, to_agree Bor_in)); last done.
rewrite /to_borUR lookup_fmap. by rewrite HBj. }
- iModIntro. iExists (P ∗ Pb)% I. rewrite /Iinv. iFrame "HI". iFrame.
- iSplitL "Hj".
- { rewrite /raw_bor /idx_bor_own. iExists j. iFrame. iExists P.
- rewrite -uPred.iff_refl. auto. }
+ iModIntro. iExists (P ∗ Pb)%I. rewrite /Iinv. iFrame "HI Hκ". iSplitL "Hj".
+ { iExists j. iFrame. iExists P. rewrite -uPred.iff_refl. auto. }
iSplitL "Hbox HB● HB".
{ rewrite /lft_bor_alive. iNext. iExists (<[j:=Bor_in]> B).
rewrite /to_borUR !fmap_insert big_sepM_insert //. iFrame.
@@ -75,7 +73,7 @@ Proof.
iDestruct (own_bor_auth with "HI Hi") as %?%elem_of_dom.
iDestruct (@big_sepS_delete with "Hinv") as "[Hκalive Hinv]"; first done.
rewrite lft_inv_alive_unfold.
- iDestruct ("Hκalive" with "[%]") as (Pb' Pi') "(Hκalive&Hvs'&Hinh)"; first done.
+ iDestruct ("Hκalive" with "[//]") as (Pb' Pi') "(Hκalive&Hvs'&Hinh)".
rewrite /lft_bor_alive; iDestruct "Hκalive" as (B') "(Hbox & HB● & HB)".
iDestruct (own_bor_valid_2 with "HB● Hi")
as %[HB%to_borUR_included _]%auth_valid_discrete_2.
@@ -89,14 +87,13 @@ Proof.
iDestruct (@big_sepM_delete with "HB") as "[Hcnt HB]"; first done.
rewrite /=. iDestruct "Hcnt" as "[% H1◯]".
iMod ("Hvs" $! I with "[Hκdead' HI Hinv Hvs' Hinh HB● Hbox HB]
- [$HPb Hi] Hκ†") as "($ & $ & Hcnt')".
+ [$HPb $Hi] Hκ†") as "($ & $ & Hcnt')".
{ rewrite lft_vs_inv_unfold. iFrame "Hκdead' HI".
iApply (big_sepS_delete _ (dom (gset lft) I) with "[- $Hinv]"); first done.
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 /raw_bor /idx_bor_own /=. auto. }
iModIntro. rewrite -[S n]Nat.add_1_l -nat_op_plus auth_frag_op own_cnt_op.
by iFrame.
Qed.
@@ -126,8 +123,7 @@ Proof.
iMod (slice_empty _ _ true with "Hs' Hbox") as "[Hidx Hbox]".
solve_ndisj. by rewrite lookup_fmap EQB.
iAssert (▷ idx_bor_own 1 (κ, i))%I with "[Hidx]" as ">Hidx"; [by iApply "HP'"|].
- iDestruct (raw_bor_inI _ _ P with "HI [Hidx]") as %HI;
- first by rewrite /raw_bor; auto 10 with I.
+ iDestruct (own_bor_auth with "HI [Hidx]") as %HI; [by rewrite /idx_bor_own|].
iDestruct (big_sepS_elem_of_acc _ _ κ with "Hinv") as "[Hinvκ Hclose']";
first by rewrite elem_of_difference elem_of_dom not_elem_of_singleton;
eauto using strict_ne.
@@ -149,25 +145,22 @@ Proof.
rewrite /lft_inv lft_inv_alive_unfold. auto 10 with iFrame.
Qed.
-Lemma raw_rebor E κ κ' P :
+Lemma raw_bor_shorten E κ κ' P :
↑lftN ⊆ E → κ ⊆ κ' →
- lft_ctx -∗ raw_bor κ P ={E}=∗ raw_bor κ' P ∗ ([†κ'] ={E}=∗ raw_bor κ P).
+ lft_ctx -∗ raw_bor κ P ={E}=∗ raw_bor κ' P.
Proof.
iIntros (? Hκκ') "#LFT Hbor".
- destruct (decide (κ = κ')) as [<-|Hκneq].
- { iFrame. iIntros "!> H†". by iApply raw_bor_fake'. }
+ destruct (decide (κ = κ')) as [<-|Hκneq]; [by iFrame|].
assert (κ ⊂ κ') by (by apply strict_spec_alt).
rewrite [_ κ P]/raw_bor. iDestruct "Hbor" as (s) "[Hbor Hs]".
iDestruct "Hs" as (P') "[#HP'P #Hs]".
- iMod (raw_bor_create _ κ' with "LFT Hbor") as "[Hbor Hinh]"; first done.
- iSplitR "Hinh"; first last.
- { iIntros "!> #H†". iExists _. iMod ("Hinh" with "H†") as ">$". auto with iFrame. }
+ iMod (raw_bor_create _ κ' with "LFT Hbor") as "[Hbor _]"; [done|].
iApply (raw_bor_iff with "HP'P"). by iApply raw_idx_bor_unnest.
Qed.
Lemma idx_bor_unnest E κ κ' i P :
↑lftN ⊆ E →
- lft_ctx -∗ &{κ,i} P -∗ &{κ'} idx_bor_own 1 i ={E}=∗ &{κ ⊓ κ'} P.
+ lft_ctx -∗ &{κ,i} P -∗ &{κ'}(idx_bor_own 1 i) ={E}=∗ &{κ ⊓ κ'} P.
Proof.
iIntros (?) "#LFT #HP Hbor".
rewrite [(&{κ'}_)%I]/bor. iDestruct "Hbor" as (κ'0) "[#Hκ'κ'0 Hbor]".
@@ -180,7 +173,7 @@ Proof.
iApply lft_intersect_incl_l. }
rewrite /idx_bor /bor. destruct i as [κ0 i].
iDestruct "HP" as "[Hκκ0 HP]". iDestruct "HP" as (P') "[HPP' HP']".
- iMod (raw_rebor _ _ (κ0 ⊓ κ'0) with "LFT Hbor") as "[Hbor _]";
+ iMod (raw_bor_shorten _ _ (κ0 ⊓ κ'0) with "LFT Hbor") as "Hbor";
[done|by apply gmultiset_union_subseteq_r|].
iMod (raw_idx_bor_unnest with "LFT HP' Hbor") as "Hbor";
[done|by apply gmultiset_union_subset_l|].
diff --git a/theories/lifetime/na_borrow.v b/theories/lifetime/na_borrow.v
index 5d17cd6ef7c8f3f689fed1a1322ddd086626bd5b..64adfc2cfaae777f01219abe30ef10a7951fe46d 100644
--- a/theories/lifetime/na_borrow.v
+++ b/theories/lifetime/na_borrow.v
@@ -7,8 +7,8 @@ Definition na_bor `{invG Σ, lftG Σ, 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.
-Notation "&na{ κ , tid , N } P" := (na_bor κ tid N P)
- (format "&na{ κ , tid , N } P", at level 20, right associativity) : uPred_scope.
+Notation "&na{ κ , tid , N }" := (na_bor κ tid N)
+ (format "&na{ κ , tid , N }") : uPred_scope.
Section na_bor.
Context `{invG Σ, lftG Σ, na_invG Σ}
diff --git a/theories/typing/borrow.v b/theories/typing/borrow.v
index 5f13cdd3a842578530eacbdc12369bbee9a57c1b..1fe107e0e624d58166b6a108ab445f429569b2a0 100644
--- a/theories/typing/borrow.v
+++ b/theories/typing/borrow.v
@@ -44,7 +44,7 @@ Section borrow.
Lemma type_deref_uniq_own_instr {E L} κ p n ty :
lctx_lft_alive E L κ →
- typed_instruction_ty E L [p ◁ &uniq{κ} own_ptr n ty] (!p) (&uniq{κ} ty).
+ typed_instruction_ty E L [p ◁ &uniq{κ}(own_ptr n ty)] (!p) (&uniq{κ} ty).
Proof.
iIntros (Hκ tid) "#LFT HE $ HL Hp".
rewrite tctx_interp_singleton.
@@ -66,15 +66,15 @@ Section borrow.
Lemma type_deref_uniq_own {E L} κ x p e n ty C T T' :
Closed (x :b: []) e →
- tctx_extract_hasty E L p (&uniq{κ} own_ptr n ty) T T' →
+ tctx_extract_hasty E L p (&uniq{κ}(own_ptr n ty)) T T' →
lctx_lft_alive E L κ →
- (∀ (v:val), typed_body E L C ((v ◁ &uniq{κ} ty) :: T') (subst' x v e)) -∗
+ (∀ (v:val), typed_body E L C ((v ◁ &uniq{κ}ty) :: T') (subst' x v e)) -∗
typed_body E L C T (let: x := !p in e).
Proof. iIntros. iApply type_let; [by apply type_deref_uniq_own_instr|solve_typing|done]. Qed.
Lemma type_deref_shr_own_instr {E L} κ p n ty :
lctx_lft_alive E L κ →
- typed_instruction_ty E L [p ◁ &shr{κ} own_ptr n ty] (!p) (&shr{κ} ty).
+ typed_instruction_ty E L [p ◁ &shr{κ}(own_ptr n ty)] (!p) (&shr{κ} ty).
Proof.
iIntros (Hκ tid) "#LFT HE $ HL Hp".
rewrite tctx_interp_singleton.
@@ -92,7 +92,7 @@ Section borrow.
Lemma type_deref_shr_own {E L} κ x p e n ty C T T' :
Closed (x :b: []) e →
- tctx_extract_hasty E L p (&shr{κ} own_ptr n ty) T T' →
+ tctx_extract_hasty E L p (&shr{κ}(own_ptr n ty)) T T' →
lctx_lft_alive E L κ →
(∀ (v:val), typed_body E L C ((v ◁ &shr{κ} ty) :: T') (subst' x v e)) -∗
typed_body E L C T (let: x := !p in e).
@@ -100,7 +100,7 @@ Section borrow.
Lemma type_deref_uniq_uniq_instr {E L} κ κ' p ty :
lctx_lft_alive E L κ → lctx_lft_incl E L κ κ' →
- typed_instruction_ty E L [p ◁ &uniq{κ} &uniq{κ'} ty] (!p) (&uniq{κ} ty).
+ typed_instruction_ty E L [p ◁ &uniq{κ}(&uniq{κ'}ty)] (!p) (&uniq{κ} ty).
Proof.
iIntros (Hκ Hincl tid) "#LFT #HE $ HL Hp".
rewrite tctx_interp_singleton.
@@ -124,15 +124,15 @@ Section borrow.
Lemma type_deref_uniq_uniq {E L} κ κ' x p e ty C T T' :
Closed (x :b: []) e →
- tctx_extract_hasty E L p (&uniq{κ} &uniq{κ'} ty) T T' →
+ tctx_extract_hasty E L p (&uniq{κ}(&uniq{κ'}ty))%T T T' →
lctx_lft_alive E L κ → lctx_lft_incl E L κ κ' →
- (∀ (v:val), typed_body E L C ((v ◁ &uniq{κ} ty) :: T') (subst' x v e)) -∗
+ (∀ (v:val), typed_body E L C ((v ◁ &uniq{κ}ty) :: T') (subst' x v e)) -∗
typed_body E L C T (let: x := !p in e).
Proof. iIntros. iApply type_let; [by apply type_deref_uniq_uniq_instr|solve_typing|done]. Qed.
Lemma type_deref_shr_uniq_instr {E L} κ κ' p ty :
lctx_lft_alive E L κ → lctx_lft_incl E L κ κ' →
- typed_instruction_ty E L [p ◁ &shr{κ} &uniq{κ'} ty] (!p) (&shr{κ} ty).
+ typed_instruction_ty E L [p ◁ &shr{κ}(&uniq{κ'}ty)] (!p) (&shr{κ}ty).
Proof.
iIntros (Hκ Hincl tid) "#LFT HE $ HL Hp". rewrite tctx_interp_singleton.
iDestruct (Hincl with "HL HE") as "#Hincl".
@@ -155,9 +155,9 @@ Section borrow.
Lemma type_deref_shr_uniq {E L} κ κ' x p e ty C T T' :
Closed (x :b: []) e →
- tctx_extract_hasty E L p (&shr{κ} &uniq{κ'} ty) T T' →
+ tctx_extract_hasty E L p (&shr{κ}(&uniq{κ'}ty))%T T T' →
lctx_lft_alive E L κ → lctx_lft_incl E L κ κ' →
- (∀ (v:val), typed_body E L C ((v ◁ &shr{κ} ty) :: T') (subst' x v e)) -∗
+ (∀ (v:val), typed_body E L C ((v ◁ &shr{κ}ty) :: T') (subst' x v e)) -∗
typed_body E L C T (let: x := !p in e).
Proof. iIntros. iApply type_let; [by apply type_deref_shr_uniq_instr|solve_typing|done]. Qed.
End borrow.
diff --git a/theories/typing/examples/get_x.v b/theories/typing/examples/get_x.v
index 66fef27d074343423ea84d867079909a2a7fabdd..3052ba5a7a8f0be9d049654bb3f02baa2939c751 100644
--- a/theories/typing/examples/get_x.v
+++ b/theories/typing/examples/get_x.v
@@ -12,7 +12,7 @@ Section get_x.
delete [ #1; "p"] ;; return: ["r"].
Lemma get_x_type :
- typed_val get_x (fn(∀ α, ∅; &uniq{α} Π[int; int]) → &shr{α} int).
+ typed_val get_x (fn(∀ α, ∅; &uniq{α}(Π[int; int])) → &shr{α}int).
Proof.
intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ϝ ret p).
inv_vec p=>p. simpl_subst.
diff --git a/theories/typing/examples/rebor.v b/theories/typing/examples/rebor.v
index 4efa575329c5b7342a9457c0d3636ba428bd9d5b..c8b0b12783079550d086e9b1006c0f88b73314bc 100644
--- a/theories/typing/examples/rebor.v
+++ b/theories/typing/examples/rebor.v
@@ -22,10 +22,10 @@ Section rebor.
intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros ([] ϝ ret p). inv_vec p=>t1 t2. simpl_subst.
iApply (type_newlft []). iIntros (α).
- iApply (type_letalloc_1 (&uniq{α}Π[int; int])); [solve_typing..|]. iIntros (x). simpl_subst.
+ iApply (type_letalloc_1 (&uniq{α}(Π[int; int]))); [solve_typing..|]. iIntros (x). simpl_subst.
iApply type_deref; [solve_typing..|]. iIntros (x'). simpl_subst.
iApply (type_letpath (&uniq{α}int)); [solve_typing|]. iIntros (y). simpl_subst.
- iApply (type_assign _ (&uniq{α}Π [int; int])); [solve_typing..|].
+ iApply (type_assign _ (&uniq{α}(Π[int; int]))); [solve_typing..|].
iApply type_deref; [solve_typing..|]. iIntros (y'). simpl_subst.
iApply type_letalloc_1; [solve_typing..|]. iIntros (r). simpl_subst.
iApply type_endlft.
diff --git a/theories/typing/examples/unbox.v b/theories/typing/examples/unbox.v
index 7b19d4be356eed375d7f2c8cade36aa1ed4f5092..cb63526d34ebc2b63732a86702ea240a95562378 100644
--- a/theories/typing/examples/unbox.v
+++ b/theories/typing/examples/unbox.v
@@ -12,7 +12,7 @@ Section unbox.
delete [ #1; "b"] ;; return: ["r"].
Lemma ubox_type :
- typed_val unbox (fn(∀ α, ∅; &uniq{α}box (Π[int; int])) → &uniq{α} int).
+ typed_val unbox (fn(∀ α, ∅; &uniq{α}(box(Π[int; int]))) → &uniq{α}int).
Proof.
intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros (α ϝ ret b). inv_vec b=>b. simpl_subst.
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index 3cf52a41af1e07000c1aac5c4c1104685f1e2d51..4c81124ff4f7a64dffd03e0647ad9d9ac6299d56 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -74,16 +74,13 @@ Section lft_contexts.
elctx_elt_interp (κ1 ⊑ₑ κ2) ∗ elctx_elt_interp (κ2 ⊑ₑ κ1).
Proof.
iIntros "#LFT". iDestruct 1 as (κ) "(% & Hκ & _)"; simplify_eq/=.
- iMod (bor_create _ κ2 (qL).[κ] with "LFT [Hκ]") as "[Hκ _]";
- first done; first by iFrame.
- iMod (bor_fracture (λ q, (qL * q).[_])%I with "LFT [Hκ]") as "#Hκ"; first done.
- { rewrite Qp_mult_1_r. done. }
+ iMod (lft_eternalize with "Hκ") as "#Hincl".
iModIntro. iSplit.
- iApply lft_incl_trans; iApply lft_intersect_incl_l.
- iApply (lft_incl_glb with "[]"); first iApply (lft_incl_glb with "[]").
+ iApply lft_incl_refl.
+ iApply lft_incl_static.
- + iApply (frac_bor_lft_incl with "LFT"). done.
+ + iApply lft_incl_trans; last done. iApply lft_incl_static.
Qed.
Context (E : elctx) (L : llctx).
diff --git a/theories/typing/lib/arc.v b/theories/typing/lib/arc.v
index 0e4bb55b8ef08fbc888f34df531d73ac1275b507..290ec5e953a234e1356afc6acc63e36cd1ceaf81 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -20,15 +20,15 @@ Section arc.
Let P1 ν q := (q.[ν])%I.
Instance P1_fractional ν : Fractional (P1 ν).
Proof. unfold P1. apply _. Qed.
- Let P2 l n := († l…(2 + n) ∗ shift_loc l 2 ↦∗: λ vl, ⌜length vl = n⌝)%I.
+ Let P2 l n := († l…(2 + n) ∗ (l +ₗ 2) ↦∗: λ vl, ⌜length vl = n⌝)%I.
Definition arc_persist tid ν (γ : gname) (l : loc) (ty : type) : iProp Σ :=
(is_arc (P1 ν) (P2 l ty.(ty_size)) arc_invN γ l ∗
(* 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) ν tid (shift_loc l 2) ∨ [†ν]) ∗
+ (ty.(ty_shr) ν tid (l +ₗ 2) ∨ [†ν]) ∗
□ (1.[ν] ={↑lftN ∪ ↑arc_endN,∅}▷=∗
- [†ν] ∗ ▷ shift_loc l 2 ↦∗: ty.(ty_own) tid ∗ † l…(2 + ty.(ty_size))))%I.
+ [†ν] ∗ ▷ (l +ₗ 2) ↦∗: ty.(ty_own) tid ∗ † l…(2 + ty.(ty_size))))%I.
Global Instance arc_persist_ne tid ν γ l n :
Proper (type_dist2 n ==> dist n) (arc_persist tid ν γ l).
@@ -64,8 +64,8 @@ Section arc.
content. The reason is that get_mut does not have the
masks to rebuild the invariants. *)
Definition full_arc_own l ty tid : iProp Σ:=
- (l ↦ #1 ∗ shift_loc l 1 ↦ #1 ∗ † l…(2 + ty.(ty_size)) ∗
- ▷ shift_loc l 2 ↦∗: ty.(ty_own) tid)%I.
+ (l ↦ #1 ∗ (l +ₗ 1) ↦ #1 ∗ † l…(2 + ty.(ty_size)) ∗
+ ▷ (l +ₗ 2) ↦∗: ty.(ty_own) tid)%I.
Definition shared_arc_own l ty tid : iProp Σ:=
(∃ γ ν q, arc_persist tid ν γ l ty ∗ arc_tok γ q ∗ q.[ν])%I.
Lemma arc_own_share E l ty tid :
@@ -418,7 +418,7 @@ Section arc.
delete [ #1; "arc" ];; return: ["x"].
Lemma arc_deref_type ty `{!TyWf ty} :
- typed_val arc_deref (fn(∀ α, ∅; &shr{α} arc ty) → &shr{α} ty).
+ typed_val arc_deref (fn(∀ α, ∅; &shr{α}(arc ty)) → &shr{α}ty).
Proof.
intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros (α ϝ ret arg). inv_vec arg=>rcx. simpl_subst.
@@ -443,7 +443,7 @@ Section arc.
iDestruct (lft_tok_dead with "Hα1 Hα†") as "[]". }
wp_op. wp_write. iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL".
(* Finish up the proof. *)
- iApply (type_type _ _ _ [ rcx ◁ box (&shr{α} arc ty); #lrc2 ◁ box (&shr{α} ty)]
+ iApply (type_type _ _ _ [ rcx ◁ box (&shr{α}(arc ty)); #lrc2 ◁ box (&shr{α}ty)]
with "[] LFT HE Hna HL Hk [-]"); last first.
{ rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val tctx_hasty_val' //.
unlock. iFrame "Hrcx". iFrame "Hx†". iExists [_]. rewrite heap_mapsto_vec_singleton.
@@ -462,7 +462,7 @@ Section arc.
delete [ #1; "arc" ];; return: ["r"].
Lemma arc_strong_count_type ty `{!TyWf ty} :
- typed_val arc_strong_count (fn(∀ α, ∅; &shr{α} arc ty) → int).
+ typed_val arc_strong_count (fn(∀ α, ∅; &shr{α}(arc ty)) → int).
Proof.
intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
@@ -487,7 +487,7 @@ Section arc.
iIntros "Htok". iMod "Hclose2" as "_". by iApply "Hclose1". }
iIntros (c) "[Hα _]". iMod ("Hclose1" with "Hα HL") as "HL".
(* Finish up the proof. *)
- iApply (type_type _ _ _ [ x ◁ box (&shr{α} arc ty); #c ◁ int; r ◁ box (uninit 1)]
+ iApply (type_type _ _ _ [ x ◁ box (&shr{α}(arc ty)); #c ◁ int; r ◁ box (uninit 1)]
with "[] LFT HE Hna HL Hk [-]"); last first.
{ rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val tctx_hasty_val' //.
unlock. iFrame. }
@@ -505,7 +505,7 @@ Section arc.
delete [ #1; "arc" ];; return: ["r"].
Lemma arc_weak_count_type ty `{!TyWf ty} :
- typed_val arc_weak_count (fn(∀ α, ∅; &shr{α} arc ty) → int).
+ typed_val arc_weak_count (fn(∀ α, ∅; &shr{α}(arc ty)) → int).
Proof.
intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
@@ -530,7 +530,7 @@ Section arc.
iIntros "Htok". iMod "Hclose2" as "_". by iApply "Hclose1". }
iIntros (c) "[Hα _]". iMod ("Hclose1" with "Hα HL") as "HL".
(* Finish up the proof. *)
- iApply (type_type _ _ _ [ x ◁ box (&shr{α} arc ty); #c ◁ int; r ◁ box (uninit 1)]
+ iApply (type_type _ _ _ [ x ◁ box (&shr{α}(arc ty)); #c ◁ int; r ◁ box (uninit 1)]
with "[] LFT HE Hna HL Hk [-]"); last first.
{ rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val tctx_hasty_val' //.
unlock. iFrame. }
@@ -550,7 +550,7 @@ Section arc.
delete [ #1; "arc" ];; return: ["r"].
Lemma arc_clone_type ty `{!TyWf ty} :
- typed_val arc_clone (fn(∀ α, ∅; &shr{α} arc ty) → arc ty).
+ typed_val arc_clone (fn(∀ α, ∅; &shr{α}(arc ty)) → arc ty).
Proof.
intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
@@ -575,7 +575,7 @@ Section arc.
iIntros "Htok". iMod "Hclose2" as "_". by iApply "Hclose1". }
iIntros (q'') "[Hα Hown]". wp_seq. iMod ("Hclose1" with "Hα HL") as "HL".
(* Finish up the proof. *)
- iApply (type_type _ _ _ [ x ◁ box (&shr{α} arc ty); #l' ◁ arc ty; r ◁ box (uninit 1)]
+ iApply (type_type _ _ _ [ x ◁ box (&shr{α}(arc ty)); #l' ◁ arc ty; r ◁ box (uninit 1)]
with "[] LFT HE Hna HL Hk [-]"); last first.
{ rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val tctx_hasty_val' //.
unlock. iFrame. simpl. unfold shared_arc_own. auto 10 with iFrame. }
@@ -594,7 +594,7 @@ Section arc.
delete [ #1; "w" ];; return: ["r"].
Lemma weak_clone_type ty `{!TyWf ty} :
- typed_val weak_clone (fn(∀ α, ∅; &shr{α} weak ty) → weak ty).
+ typed_val weak_clone (fn(∀ α, ∅; &shr{α}(weak ty)) → weak ty).
Proof.
intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
@@ -619,7 +619,7 @@ Section arc.
iIntros "Htok". iMod "Hclose2" as "_". by iApply "Hclose1". }
iIntros "[Hα Hown]". wp_seq. iMod ("Hclose1" with "Hα HL") as "HL".
(* Finish up the proof. *)
- iApply (type_type _ _ _ [ x ◁ box (&shr{α} weak ty); #l' ◁ weak ty; r ◁ box (uninit 1) ]
+ iApply (type_type _ _ _ [ x ◁ box (&shr{α}(weak ty)); #l' ◁ weak ty; r ◁ box (uninit 1) ]
with "[] LFT HE Hna HL Hk [-]"); last first.
{ rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val tctx_hasty_val' //.
unlock. iFrame. simpl. eauto 10 with iFrame. }
@@ -638,7 +638,7 @@ Section arc.
delete [ #1; "arc" ];; return: ["r"].
Lemma downgrade_type ty `{!TyWf ty} :
- typed_val downgrade (fn(∀ α, ∅; &shr{α} arc ty) → weak ty).
+ typed_val downgrade (fn(∀ α, ∅; &shr{α}(arc ty)) → weak ty).
Proof.
intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
@@ -663,7 +663,7 @@ Section arc.
iIntros "Htok". iMod "Hclose2" as "_". by iApply "Hclose1". }
iIntros "[Hα Hown]". wp_seq. iMod ("Hclose1" with "Hα HL") as "HL".
(* Finish up the proof. *)
- iApply (type_type _ _ _ [ x ◁ box (&shr{α} arc ty); #l' ◁ weak ty; r ◁ box (uninit 1) ]
+ iApply (type_type _ _ _ [ x ◁ box (&shr{α}(arc ty)); #l' ◁ weak ty; r ◁ box (uninit 1) ]
with "[] LFT HE Hna HL Hk [-]"); last first.
{ rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val tctx_hasty_val' //.
unlock. iFrame. simpl. eauto 10 with iFrame. }
@@ -685,7 +685,7 @@ Section arc.
delete [ #1; "w" ];; return: ["r"].
Lemma upgrade_type ty `{!TyWf ty} :
- typed_val upgrade (fn(∀ α, ∅; &shr{α} weak ty) → option (arc ty)).
+ typed_val upgrade (fn(∀ α, ∅; &shr{α}(weak ty)) → option (arc ty)).
Proof.
intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
@@ -710,7 +710,7 @@ Section arc.
iIntros "Htok". iMod "Hclose2" as "_". by iApply "Hclose1". }
iIntros ([] q') "[Hα Hown]"; wp_if; iMod ("Hclose1" with "Hα HL") as "HL".
- (* Finish up the proof (sucess). *)
- iApply (type_type _ _ _ [ x ◁ box (&shr{α} weak ty); #l' ◁ arc ty;
+ iApply (type_type _ _ _ [ x ◁ box (&shr{α}(weak ty)); #l' ◁ arc ty;
r ◁ box (uninit 2) ]
with "[] LFT HE Hna HL Hk [-]"); last first.
{ rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val tctx_hasty_val' //.
@@ -719,7 +719,7 @@ Section arc.
iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing.
- (* Finish up the proof (fail). *)
- iApply (type_type _ _ _ [ x ◁ box (&shr{α} weak ty); r ◁ box (uninit 2) ]
+ iApply (type_type _ _ _ [ x ◁ box (&shr{α}(weak ty)); r ◁ box (uninit 2) ]
with "[] LFT HE Hna HL Hk [-]"); last first.
{ rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
unlock. iFrame. }
@@ -889,7 +889,7 @@ Section arc.
with "[] LFT HE Hna HL Hk [-]"); last first.
{ rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val. unlock.
iFrame. iCombine "Hr1" "Hr2" as "Hr1". iCombine "Hr0" "Hr1" as "Hr".
- rewrite -[in shift_loc _ ty.(ty_size)]Hlen -heap_mapsto_vec_app
+ rewrite -[in _ +ₗ ty.(ty_size)]Hlen -heap_mapsto_vec_app
-heap_mapsto_vec_cons tctx_hasty_val' //. iFrame. iExists _. iFrame.
iExists O, _, _. iSplit; first by auto. iFrame. iIntros "!> !% /=".
rewrite app_length drop_length. lia. }
@@ -920,7 +920,7 @@ Section arc.
delete [ #1; "arc"];; return: ["r"].
Lemma arc_get_mut_type ty `{!TyWf ty} :
- typed_val arc_get_mut (fn(∀ α, ∅; &uniq{α} arc ty) → option (&uniq{α}ty)).
+ typed_val arc_get_mut (fn(∀ α, ∅; &uniq{α}(arc ty)) → option (&uniq{α}ty)).
Proof.
intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros (α ϝ ret arg). inv_vec arg=>rcx. simpl_subst.
@@ -1006,8 +1006,8 @@ Section arc.
]).
Lemma arc_make_mut_type ty `{!TyWf ty} clone :
- typed_val clone (fn(∀ α, ∅; &shr{α} ty) → ty) →
- typed_val (arc_make_mut ty clone) (fn(∀ α, ∅; &uniq{α} arc ty) → &uniq{α} ty).
+ typed_val clone (fn(∀ α, ∅; &shr{α}ty) → ty) →
+ typed_val (arc_make_mut ty clone) (fn(∀ α, ∅; &uniq{α}(arc ty)) → &uniq{α} ty).
Proof.
intros Hclone E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros (α ϝ ret arg). inv_vec arg=>rcx. simpl_subst.
@@ -1034,7 +1034,7 @@ Section arc.
{ iIntros "!> Hrc2". iExists [_]. rewrite heap_mapsto_vec_singleton.
iFrame. iLeft. by iFrame. }
iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL".
- iApply (type_type _ _ _ [ rcx ◁ box (uninit 1); #(shift_loc rc 2) ◁ &uniq{α}ty;
+ iApply (type_type _ _ _ [ rcx ◁ box (uninit 1); #(rc +ₗ 2) ◁ &uniq{α}ty;
r ◁ box (uninit 1) ]
with "[] LFT HE Hna HL Hk [-]"); last first.
{ rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val
@@ -1052,7 +1052,7 @@ Section arc.
iDestruct (ty_size_eq with "Hown") as %Hlen'.
wp_apply (wp_memcpy with "[$Hrc2 $H↦]"); [lia..|].
iIntros "[H↦ H↦']". wp_seq. wp_write.
- iMod ("Hclose2" $! (shift_loc l 2 ↦∗: ty_own ty tid)%I
+ iMod ("Hclose2" $! ((l +ₗ 2) ↦∗: ty_own ty tid)%I
with "[Hrc'↦ Hrc0 Hrc1 H†] [H↦ Hown]") as "[Hb Hα1]"; [|by auto with iFrame|].
{ iIntros "!> H↦". iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame.
iLeft. iFrame. iDestruct "H†" as "[?|%]"=>//.
@@ -1094,7 +1094,7 @@ Section arc.
wp_apply (wp_delete with "[$Hcl↦ Hcl†]");
[lia|by replace (length vl) with (ty.(ty_size))|].
iIntros "_". wp_seq. wp_write.
- iMod ("Hclose2" $! (shift_loc l' 2 ↦∗: ty_own ty tid)%I with
+ iMod ("Hclose2" $! ((l' +ₗ 2) ↦∗: ty_own ty tid)%I with
"[Hrc'↦ Hl' Hl'1 Hl'†] [Hl'2 Hown]") as "[Hl' Hα1]".
{ iIntros "!> H". iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame.
iLeft. iFrame. iDestruct "Hl'†" as "[?|%]"=>//.
diff --git a/theories/typing/lib/cell.v b/theories/typing/lib/cell.v
index 42fb6805fe9ffc69b380bc5142e77b65e69a7038..025d2ef1f61753f39da343304002909783a85454 100644
--- a/theories/typing/lib/cell.v
+++ b/theories/typing/lib/cell.v
@@ -12,7 +12,7 @@ Section cell.
Program Definition cell (ty : type) :=
{| ty_size := ty.(ty_size);
ty_own := ty.(ty_own);
- ty_shr κ tid l := (&na{κ, tid, shrN.@l}l ↦∗: ty.(ty_own) tid)%I |}.
+ ty_shr κ tid l := (&na{κ, tid, shrN.@l}(l ↦∗: ty.(ty_own) tid))%I |}.
Next Obligation. apply ty_size_eq. Qed.
Next Obligation.
iIntros (ty E κ l tid q ?) "#LFT Hown $". by iApply (bor_na with "Hown").
@@ -146,7 +146,7 @@ Section typing.
delete [ #1; "c"] ;; delete [ #ty.(ty_size); "x"] ;; return: ["r"].
Lemma cell_replace_type ty `{!TyWf ty} :
- typed_val (cell_replace ty) (fn(∀ α, ∅; &shr{α} cell ty, ty) → ty).
+ typed_val (cell_replace ty) (fn(∀ α, ∅; &shr{α}(cell ty), ty) → ty).
Proof.
intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros (α ϝ ret arg). inv_vec arg=>c x. simpl_subst.
@@ -178,7 +178,7 @@ Section typing.
iMod ("Hclose1" with "Htok HL") as "HL".
(* Now go back to typing level. *)
iApply (type_type _ _ _
- [c ◁ box (&shr{α} cell ty); #x ◁ box (uninit ty.(ty_size)); #r ◁ box ty]
+ [c ◁ box (&shr{α}(cell ty)); #x ◁ box (uninit ty.(ty_size)); #r ◁ box ty]
with "[] LFT HE Htl HL HC"); last first.
{ rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
iFrame "Hc". rewrite !tctx_hasty_val' //. iSplitL "Hx↦ Hx†".
@@ -198,17 +198,17 @@ Section typing.
delete [ #1; "x"];; return: ["r"].
Lemma fake_shared_cell_type ty `{!TyWf ty} :
- typed_val fake_shared_cell (fn(∀ α, ∅; &uniq{α} ty) → &shr{α} cell ty).
+ typed_val fake_shared_cell (fn(∀ α, ∅; &uniq{α} ty) → &shr{α}(cell ty)).
Proof.
intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
iIntros (tid) "#LFT #HE Hna HL Hk HT".
rewrite tctx_interp_singleton tctx_hasty_val.
- iApply (type_type _ _ _ [ x ◁ box (&uniq{α}cell ty) ]
+ iApply (type_type _ _ _ [ x ◁ box (&uniq{α}(cell ty)) ]
with "[] LFT HE Hna HL Hk [HT]"); last first.
{ by rewrite tctx_interp_singleton tctx_hasty_val. }
iApply type_deref; [solve_typing..|]. iIntros (x'). simpl_subst.
- iApply (type_letalloc_1 (&shr{α}cell ty)); [solve_typing..|]. iIntros (r). simpl_subst.
+ iApply (type_letalloc_1 (&shr{α}(cell ty))); [solve_typing..|]. iIntros (r). simpl_subst.
iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing.
Qed.
diff --git a/theories/typing/lib/diverging_static.v b/theories/typing/lib/diverging_static.v
new file mode 100644
index 0000000000000000000000000000000000000000..e34687af30abf1dd95cde4b8b7d95c2b15c507cd
--- /dev/null
+++ b/theories/typing/lib/diverging_static.v
@@ -0,0 +1,59 @@
+From iris.proofmode Require Import tactics.
+From iris.base_logic Require Import big_op.
+From lrust.typing Require Export type.
+From lrust.typing Require Import typing.
+Set Default Proof Using "Type".
+
+Section diverging_static.
+ Context `{!typeG Σ}.
+
+ (* Show that we can convert any live borrow to 'static with an infinite
+ loop. *)
+ Definition diverging_static_loop (call_once : val) : val :=
+ funrec: <> ["x"; "f"] :=
+ let: "call_once" := call_once in
+ letcall: "ret" := "call_once" ["f"; "x"]%E in
+ withcont: "loop":
+ "loop" []
+ cont: "loop" [] :=
+ "loop" [].
+
+ Lemma diverging_static_loop_type T F call_once
+ `{!TyWf T, !TyWf F} :
+ (* F : FnOnce(&'static T), as witnessed by the impl call_once *)
+ typed_val call_once (fn(∅; F, &shr{static} T) → unit) →
+ typed_val (diverging_static_loop call_once)
+ (fn(∀ α, λ ϝ, T.(ty_outlives_E) static; &shr{α} T, F) → emp).
+ Proof.
+ intros Hf E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ iIntros (α ϝ ret arg). inv_vec arg=>x f. simpl_subst.
+ iApply type_let; [apply Hf|solve_typing|]. iIntros (call); simpl_subst.
+ (* Drop to Iris *)
+ iIntros (tid) "#LFT #HE Hna HL Hk (Hcall & Hx & Hf & _)".
+ (* We need a ϝ token to show that we can call F despite it being non-'static. *)
+ iMod (lctx_lft_alive_tok ϝ with "HE HL") as (qϝ) "(Hϝ & HL & _)";
+ [solve_typing..|].
+ iMod (lctx_lft_alive_tok α with "HE HL") as (q) "(Hα & _ & _)";
+ [solve_typing..|].
+ iMod (lft_eternalize with "Hα") as "#Hα".
+ iAssert (type_incl (box (&shr{α} T)) (box (&shr{static} T))) as "#[_ [Hincl _]]".
+ { iApply box_type_incl. iNext. iApply shr_type_incl; first done.
+ iApply type_incl_refl. }
+ wp_let. rewrite tctx_hasty_val.
+ iApply (type_call_iris _ [ϝ] () [_; _] with "LFT HE Hna [Hϝ] Hcall [Hx Hf]").
+ - solve_typing.
+ - solve_to_val.
+ - by rewrite /= (right_id static).
+ - simpl. iFrame. iSplit; last done. rewrite !tctx_hasty_val.
+ iApply "Hincl". done.
+ - iClear "Hα Hincl". iIntros (r) "Htl Hϝ1 Hret". wp_rec.
+ (* Go back to the type system. *)
+ iApply (type_type _ [] _ [] with "[] LFT HE Htl [] Hk [-]"); last first.
+ { rewrite /tctx_interp /=. done. }
+ { rewrite /llctx_interp /=. done. }
+ iApply (type_cont [] [] (λ _, [])).
+ + iIntros (?). simpl_subst. iApply type_jump; solve_typing.
+ + iIntros "!#" (? args). inv_vec args. simpl_subst. iApply type_jump; solve_typing.
+ Qed.
+
+End diverging_static.
diff --git a/theories/typing/lib/fake_shared_box.v b/theories/typing/lib/fake_shared_box.v
index 768aabdd2a1787edb6c50fa44ea71bb0e2118474..99530965643368fbd0a1ebbd5abfcbaf346ec303 100644
--- a/theories/typing/lib/fake_shared_box.v
+++ b/theories/typing/lib/fake_shared_box.v
@@ -11,14 +11,14 @@ Section fake_shared_box.
Lemma fake_shared_box_type ty `{!TyWf ty} :
typed_val fake_shared_box
- (fn(∀ '(α, β), ∅; &shr{α} &shr{β} ty) → &shr{α} box ty).
+ (fn(∀ '(α, β), ∅; &shr{α}(&shr{β} ty)) → &shr{α}(box ty)).
Proof.
intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros ([α β] ϝ ret arg). inv_vec arg=>x. simpl_subst.
iIntros (tid) "#LFT #HE Hna HL Hk HT".
rewrite tctx_interp_singleton tctx_hasty_val.
iDestruct (lctx_lft_incl_incl α β with "HL HE") as "#Hαβ"; [solve_typing..|].
- iAssert (▷ ty_own (own_ptr 1 (&shr{α} box ty)) tid [x])%I with "[HT]" as "HT".
+ iAssert (▷ ty_own (own_ptr 1 (&shr{α}(box ty))) tid [x])%I with "[HT]" as "HT".
{ destruct x as [[|l|]|]=>//=. iDestruct "HT" as "[H $]".
iNext. iDestruct "H" as ([|[[]|][]]) "[H↦ H]"; try done.
iExists _. iFrame. iDestruct "H" as (vl) "[#Hf H]".
@@ -28,7 +28,7 @@ Section fake_shared_box.
iDestruct "H" as "#H". iIntros "!# * % $". iApply step_fupd_intro. set_solver.
by iApply ty_shr_mono. }
wp_seq.
- iApply (type_type [] _ _ [ x ◁ box (&shr{α}box ty) ]
+ iApply (type_type [] _ _ [ x ◁ box (&shr{α}(box ty)) ]
with "[] LFT [] Hna HL Hk [HT]"); last first.
{ by rewrite tctx_interp_singleton tctx_hasty_val. }
{ by rewrite /elctx_interp. }
diff --git a/theories/typing/lib/mutex/mutex.v b/theories/typing/lib/mutex/mutex.v
index 12ae9140af592ffa6742885e22ed364d405843fe..58e43755ed86cddb56ed305a54c871d9f9d66149 100644
--- a/theories/typing/lib/mutex/mutex.v
+++ b/theories/typing/lib/mutex/mutex.v
@@ -34,7 +34,7 @@ Section mutex.
⌜∃ b, z = Z_of_bool b⌝ ∗ ty.(ty_own) tid vl'
| _ => False end;
ty_shr κ tid l := ∃ κ', κ ⊑ κ' ∗
- &at{κ, mutexN} (lock_proto l (&{κ'} shift_loc l 1 ↦∗: ty.(ty_own) tid))
+ &at{κ, mutexN} (lock_proto l (&{κ'}((l +ₗ 1) ↦∗: ty.(ty_own) tid)))
|}%I.
Next Obligation.
iIntros (??[|[[]|]]); try iIntros "[]". rewrite ty_size_eq.
@@ -48,7 +48,7 @@ Section mutex.
iDestruct "H" as "[>EQ Hown]". iDestruct "EQ" as %[b ->].
(* We need to turn the ohne borrow into two, so we close it -- and then
we open one of them again. *)
- iMod ("Hclose" $! ((∃ b, l ↦ #(Z_of_bool b)) ∗ (shift_loc l 1 ↦∗: ty_own ty tid))%I
+ iMod ("Hclose" $! ((∃ b, l ↦ #(Z_of_bool b)) ∗ ((l +ₗ 1) ↦∗: ty_own ty tid))%I
with "[] [Hl H↦ Hown]") as "[Hbor Htok]".
{ clear. iNext. iIntros "[Hl Hown] !>". iNext. iDestruct "Hl" as (b) "Hl".
iDestruct "Hown" as (vl) "[H↦ Hown]". iExists (#(Z_of_bool b) :: vl).
@@ -125,7 +125,6 @@ Section mutex.
iApply heap_mapsto_pred_iff_proper.
iAlways; iIntros; iSplit; iIntros; by iApply send_change_tid.
Qed.
-
End mutex.
Section code.
@@ -217,7 +216,7 @@ Section code.
return: ["m"].
Lemma mutex_get_mut_type ty `{!TyWf ty} :
- typed_val mutex_get_mut (fn(∀ α, ∅; &uniq{α} mutex ty) → &uniq{α} ty).
+ typed_val mutex_get_mut (fn(∀ α, ∅; &uniq{α}(mutex ty)) → &uniq{α} ty).
Proof.
intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros (α ϝ ret arg); inv_vec arg=>m; simpl_subst.
@@ -233,13 +232,13 @@ Section code.
destruct vl as [|[[|m'|]|] vl]; try done. simpl.
iDestruct (heap_mapsto_vec_cons with "H↦") as "[H↦1 H↦2]".
iDestruct "Hm'" as "[% Hvl]".
- iMod ("Hclose2" $! (shift_loc lm' 1 ↦∗: ty_own ty tid)%I with "[H↦1] [H↦2 Hvl]") as "[Hbor Hα]".
+ iMod ("Hclose2" $! ((lm' +ₗ 1) ↦∗: ty_own ty tid)%I with "[H↦1] [H↦2 Hvl]") as "[Hbor Hα]".
{ iIntros "!> Hlm' !>". iNext. clear vl. iDestruct "Hlm'" as (vl) "[H↦ Hlm']".
iExists (_ :: _). rewrite heap_mapsto_vec_cons. do 2 iFrame. done. }
{ iExists vl. iFrame. }
iMod ("Hclose1" with "Hα HL") as "HL".
(* Switch back to typing mode. *)
- iApply (type_type _ _ _ [ m ◁ own_ptr _ _; #(shift_loc lm' 1) ◁ &uniq{α} ty]
+ iApply (type_type _ _ _ [ m ◁ own_ptr _ _; #(lm' +ₗ 1) ◁ &uniq{α} ty]
with "[] LFT HE Hna HL Hk"); last first.
{ rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
unlock. iFrame. }
diff --git a/theories/typing/lib/mutex/mutexguard.v b/theories/typing/lib/mutex/mutexguard.v
index c2b4b68cd9804ceab9a243db7a680b1c019fcb84..d28626c93aecdd86075a58787c0c2e581616a48d 100644
--- a/theories/typing/lib/mutex/mutexguard.v
+++ b/theories/typing/lib/mutex/mutexguard.v
@@ -35,13 +35,13 @@ Section mguard.
match vl return _ with
| [ #(LitLoc l) ] =>
∃ β, α ⊑ β ∗
- &at{α, mutexN} (lock_proto l (&{β} shift_loc l 1 ↦∗: ty.(ty_own) tid)) ∗
- &{β} (shift_loc l 1 ↦∗: ty.(ty_own) tid)
+ &at{α, mutexN} (lock_proto l (&{β} ((l +ₗ 1) ↦∗: ty.(ty_own) tid))) ∗
+ &{β} ((l +ₗ 1) ↦∗: ty.(ty_own) tid)
| _ => False end;
ty_shr κ tid l :=
∃ (l':loc), &frac{κ}(λ q', l ↦{q'} #l') ∗
□ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ q.[α⊓κ]
- ={F, F∖↑shrN}▷=∗ ty.(ty_shr) (α⊓κ) tid (shift_loc l' 1) ∗ q.[α⊓κ]
+ ={F, F∖↑shrN}▷=∗ ty.(ty_shr) (α⊓κ) tid (l' +ₗ 1) ∗ q.[α⊓κ]
|}%I.
Next Obligation. by iIntros (? ty tid [|[[]|][]]) "H". Qed.
(* This is to a large extend copy-pasted from RWLock's write guard. *)
@@ -136,8 +136,8 @@ Section code.
Lemma mutex_acc E l ty tid q α κ :
↑lftN ⊆ E → ↑mutexN ⊆ E →
- let R := (&{κ} shift_loc l 1 ↦∗: ty_own ty tid)%I in
- lft_ctx -∗ &at{α,mutexN} lock_proto l R -∗ α ⊑ κ -∗
+ let R := (&{κ}((l +ₗ 1) ↦∗: ty_own ty tid))%I in
+ lft_ctx -∗ &at{α,mutexN}(lock_proto l R) -∗ α ⊑ κ -∗
□ ((q).[α] ={E,∅}=∗ ▷ lock_proto l R ∗ (▷ lock_proto l R ={∅,E}=∗ (q).[α])).
Proof.
(* FIXME: This should work: iIntros (?? R). *) intros ?? R.
@@ -157,7 +157,7 @@ Section code.
delete [ #1; "mutex" ];; return: ["guard"].
Lemma mutex_lock_type ty `{!TyWf ty} :
- typed_val mutex_lock (fn(∀ α, ∅; &shr{α} mutex ty) → mutexguard α ty).
+ typed_val mutex_lock (fn(∀ α, ∅; &shr{α}(mutex ty)) → mutexguard α ty).
Proof.
intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index a42269279bde1fe05bdeda90ac772a0c810a2d07..123029972f8c15f41b31ecf44f6ad81cf3400138 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -60,16 +60,16 @@ Section rc.
(∃ st : rc_stR, own γ (● st) ∗
match st with
| (Some (Cinl (q, strong)), weak) => ∃ q',
- l ↦ #(Zpos strong) ∗ shift_loc l 1 ↦ #(S weak) ∗ † l…(2 + ty.(ty_size)) ∗
+ l ↦ #(Zpos strong) ∗ (l +ₗ 1) ↦ #(S weak) ∗ † l…(2 + ty.(ty_size)) ∗
⌜(q + q')%Qp = 1%Qp⌝ ∗ q'.[ν] ∗
(* We keep this view shift decomposed because we store the persistent
part in ty_own, to make it available with one step less. *)
- ([†ν] ={↑lftN}=∗ ▷ shift_loc l 2 ↦∗: ty.(ty_own) tid)
+ ([†ν] ={↑lftN}=∗ ▷ (l +ₗ 2) ↦∗: ty.(ty_own) tid)
| (Some (Cinr _), weak) =>
- l ↦ #0 ∗ shift_loc l 1 ↦ #(S weak)
+ l ↦ #0 ∗ (l +ₗ 1) ↦ #(S weak)
| (None, (S _) as weak) =>
- l ↦ #0 ∗ shift_loc l 1 ↦ #weak ∗ † l…(2 + ty.(ty_size)) ∗
- shift_loc l 2 ↦∗: λ vl, ⌜length vl = ty.(ty_size)⌝
+ l ↦ #0 ∗ (l +ₗ 1) ↦ #weak ∗ † l…(2 + ty.(ty_size)) ∗
+ (l +ₗ 2) ↦∗: λ vl, ⌜length vl = ty.(ty_size)⌝
| _ => True
end)%I.
@@ -85,7 +85,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) ν tid (shift_loc l 2) ∨ [†ν]) ∗
+ (ty.(ty_shr) ν tid (l +ₗ 2) ∨ [†ν]) ∗
□ (1.[ν] ={↑lftN,∅}▷=∗ [†ν]))%I.
Global Instance rc_persist_ne ν γ l n :
@@ -114,8 +114,8 @@ Section rc.
shared protocol or the full ownership of the
content. The reason is that get_mut does not have the
masks to rebuild the invariants. *)
- (l ↦ #1 ∗ shift_loc l 1 ↦ #1 ∗ † l…(2 + ty.(ty_size)) ∗
- ▷ shift_loc l 2 ↦∗: ty.(ty_own) tid) ∨
+ (l ↦ #1 ∗ (l +ₗ 1) ↦ #1 ∗ † l…(2 + ty.(ty_size)) ∗
+ ▷ (l +ₗ 2) ↦∗: ty.(ty_own) tid) ∨
(∃ γ ν q, rc_persist tid ν γ l ty ∗ own γ (rc_tok q) ∗ q.[ν])
| _ => False end;
ty_shr κ tid l :=
@@ -241,25 +241,25 @@ Section code.
!#l
{{{ strong, RET #(Zpos strong); l ↦ #(Zpos strong) ∗
(((⌜strong = 1%positive⌝ ∗
- (∃ weak : Z, shift_loc l 1 ↦ #weak ∗
+ (∃ weak : Z, (l +ₗ 1) ↦ #weak ∗
((⌜weak = 1⌝ ∗
|={⊤,∅}▷=> † l…(2 + ty.(ty_size)) ∗
- ▷ shift_loc l 2 ↦∗: ty.(ty_own) tid ∗ na_own tid F) ∨
+ ▷ (l +ₗ 2) ↦∗: ty.(ty_own) tid ∗ na_own tid F) ∨
(⌜weak > 1⌝ ∗
- ((l ↦ #1 -∗ shift_loc l 1 ↦ #weak
+ ((l ↦ #1 -∗ (l +ₗ 1) ↦ #weak
={⊤}=∗ na_own tid F ∗ ty_own (rc ty) tid [ #l ]) ∧
- (l ↦ #0 -∗ shift_loc l 1 ↦ #(weak - 1)
- ={⊤,∅}▷=∗ ▷ shift_loc l 2 ↦∗: ty.(ty_own) tid ∗
- (shift_loc l 2 ↦∗: (λ vl, ⌜length vl = ty.(ty_size)⌝)
+ (l ↦ #0 -∗ (l +ₗ 1) ↦ #(weak - 1)
+ ={⊤,∅}▷=∗ ▷ (l +ₗ 2) ↦∗: ty.(ty_own) tid ∗
+ ((l +ₗ 2) ↦∗: (λ vl, ⌜length vl = ty.(ty_size)⌝)
={⊤}=∗ na_own tid F)))))) ∧
(l ↦ #0 ={⊤,∅}▷=∗
- ▷ shift_loc l 2 ↦∗: ty.(ty_own) tid ∗ † l…(2 + ty.(ty_size)) ∗ na_own tid F ∗
+ ▷ (l +ₗ 2) ↦∗: ty.(ty_own) tid ∗ † l…(2 + ty.(ty_size)) ∗ na_own tid F ∗
(na_own tid F ={⊤}=∗ ∃ weak : Z,
- shift_loc l 1 ↦ #weak ∗
+ (l +ₗ 1) ↦ #weak ∗
((⌜weak = 1⌝ ∗ l ↦ #0 ∗ na_own tid F) ∨
(⌜weak > 1⌝ ∗
- († l…(2 + ty.(ty_size)) -∗ shift_loc l 1 ↦ #(weak-1) -∗
- shift_loc l 2 ↦∗: (λ vl, ⌜length vl = ty.(ty_size)⌝)
+ († l…(2 + ty.(ty_size)) -∗ (l +ₗ 1) ↦ #(weak-1) -∗
+ (l +ₗ 2) ↦∗: (λ vl, ⌜length vl = ty.(ty_size)⌝)
={⊤}=∗ na_own tid F))))))
) ∨
(⌜(1 < strong)%positive⌝ ∗
@@ -379,7 +379,7 @@ Section code.
delete [ #1; "rc" ];; return: ["r"].
Lemma rc_strong_count_type ty `{!TyWf ty} :
- typed_val rc_strong_count (fn(∀ α, ∅; &shr{α} rc ty) → int).
+ typed_val rc_strong_count (fn(∀ α, ∅; &shr{α}(rc ty)) → int).
Proof.
intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
@@ -415,7 +415,7 @@ Section code.
{ iExists _. iFrame "Hrc●". iExists _. auto with iFrame. }
iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL".
(* Finish up the proof. *)
- iApply (type_type _ _ _ [ x ◁ box (&shr{α} rc ty); r ◁ box (uninit 1);
+ iApply (type_type _ _ _ [ x ◁ box (&shr{α}(rc ty)); r ◁ box (uninit 1);
#(Z.pos s0) ◁ int ]
with "[] LFT HE Hna HL Hk [-]"); last first.
{ unlock.
@@ -438,7 +438,7 @@ Section code.
delete [ #1; "rc" ];; return: ["r"].
Lemma rc_weak_count_type ty `{!TyWf ty} :
- typed_val rc_weak_count (fn(∀ α, ∅; &shr{α} rc ty) → int).
+ typed_val rc_weak_count (fn(∀ α, ∅; &shr{α}(rc ty)) → int).
Proof.
intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
@@ -474,7 +474,7 @@ Section code.
{ iExists _. iFrame "Hrc●". iExists _. auto with iFrame. }
iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL".
(* Finish up the proof. *)
- iApply (type_type _ _ _ [ x ◁ box (&shr{α} rc ty); r ◁ box (uninit 1);
+ iApply (type_type _ _ _ [ x ◁ box (&shr{α}(rc ty)); r ◁ box (uninit 1);
#(S weak) ◁ int ]
with "[] LFT HE Hna HL Hk [-]"); last first.
{ unlock.
@@ -541,7 +541,7 @@ Section code.
delete [ #1; "rc" ];; return: ["r"].
Lemma rc_clone_type ty `{!TyWf ty} :
- typed_val rc_clone (fn(∀ α, ∅; &shr{α} rc ty) → rc ty).
+ typed_val rc_clone (fn(∀ α, ∅; &shr{α}(rc ty)) → rc ty).
Proof.
intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
@@ -587,7 +587,7 @@ Section code.
rewrite [_ ⋅ _]comm frac_op' -[(_ + _)%Qp]assoc Qp_div_2. auto. }
iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL".
(* Finish up the proof. *)
- iApply (type_type _ _ _ [ x ◁ box (&shr{α} rc ty); #lr ◁ box (rc ty)]
+ iApply (type_type _ _ _ [ x ◁ box (&shr{α}(rc ty)); #lr ◁ box (rc ty)]
with "[] LFT HE Hna HL Hk [-]"); last first.
{ rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
unlock. iFrame "Hx". iFrame "Hr†". iExists [# #l'].
@@ -604,7 +604,7 @@ Section code.
delete [ #1; "rc" ];; return: ["x"].
Lemma rc_deref_type ty `{!TyWf ty} :
- typed_val rc_deref (fn(∀ α, ∅; &shr{α} rc ty) → &shr{α} ty).
+ typed_val rc_deref (fn(∀ α, ∅; &shr{α}(rc ty)) → &shr{α}ty).
Proof.
intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros (α ϝ ret arg). inv_vec arg=>rcx. simpl_subst.
@@ -629,7 +629,7 @@ Section code.
iDestruct (lft_tok_dead with "Hα1 Hα†") as "[]". }
wp_op. wp_write. iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL".
(* Finish up the proof. *)
- iApply (type_type _ _ _ [ rcx ◁ box (&shr{α} rc ty); #lrc2 ◁ box (&shr{α} ty)]
+ iApply (type_type _ _ _ [ rcx ◁ box (&shr{α}(rc ty)); #lrc2 ◁ box (&shr{α}ty)]
with "[] LFT HE Hna HL Hk [-]"); last first.
{ rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val tctx_hasty_val' //.
unlock. iFrame "Hrcx". iFrame "Hx†". iExists [_]. rewrite heap_mapsto_vec_singleton.
@@ -852,13 +852,13 @@ Section code.
delete [ #1; "rc"];; return: ["r"].
Lemma rc_get_mut_type ty `{!TyWf ty} :
- typed_val rc_get_mut (fn(∀ α, ∅; &uniq{α} rc ty) → option (&uniq{α} ty)).
+ typed_val rc_get_mut (fn(∀ α, ∅; &uniq{α}(rc ty)) → option (&uniq{α}ty)).
Proof.
intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros (α ϝ ret arg). inv_vec arg=>rcx. simpl_subst.
iApply (type_new 2); [solve_typing..|]; iIntros (r); simpl_subst.
iApply (type_cont [] [ϝ ⊑ₗ []]
- (λ _, [rcx ◁ box (uninit 1); r ◁ box (option $ &uniq{α} ty)]));
+ (λ _, [rcx ◁ box (uninit 1); r ◁ box (option $ &uniq{α}ty)]));
[solve_typing..| |]; last first.
{ simpl. iAlways. iIntros (k arg). inv_vec arg. simpl_subst.
iApply type_delete; [solve_typing..|].
@@ -887,12 +887,12 @@ Section code.
{ iIntros "!> Hty". iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame "Hrc'".
iLeft. by iFrame. }
iMod ("Hclose1" with "Hα HL") as "HL".
- iApply (type_type _ _ _ [ r ◁ box (uninit 2); #l +ₗ #2 ◁ &uniq{α} ty;
+ iApply (type_type _ _ _ [ r ◁ box (uninit 2); #l +ₗ #2 ◁ &uniq{α}ty;
rcx ◁ box (uninit 1)]
with "[] LFT HE Hna HL Hk [-]"); last first.
{ rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val tctx_hasty_val' //.
unlock. iFrame. }
- iApply (type_sum_assign (option (&uniq{_} _))); [solve_typing..|].
+ iApply (type_sum_assign (option (&uniq{_}_))); [solve_typing..|].
iApply type_jump; solve_typing.
+ wp_op=>[?|_]; first lia. wp_if. iMod ("Hrc" with "Hl1 Hl2") as "[Hna Hrc]".
iMod ("Hclose2" with "[] [Hrc' Hrc]") as "[Hrc' Hα]".
@@ -903,7 +903,7 @@ Section code.
with "[] LFT HE Hna HL Hk [-]"); last first.
{ rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
unlock. iFrame. }
- iApply (type_sum_unit (option (&uniq{_} _))); [solve_typing..|].
+ iApply (type_sum_unit (option (&uniq{_}_))); [solve_typing..|].
iApply type_jump; solve_typing.
- wp_if. iDestruct "Hc" as "[[% _]|[% [Hproto _]]]"; first lia.
iMod ("Hproto" with "Hl1") as "[Hna Hrc]".
@@ -915,7 +915,7 @@ Section code.
with "[] LFT HE Hna HL Hk [-]"); last first.
{ rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
unlock. iFrame. }
- iApply (type_sum_unit (option (&uniq{_} _))); [solve_typing..|].
+ iApply (type_sum_unit (option (&uniq{_}_))); [solve_typing..|].
iApply type_jump; solve_typing.
Qed.
@@ -982,14 +982,14 @@ Section code.
Lemma rc_make_mut_type ty `{!TyWf ty} clone :
(* ty : Clone, as witnessed by the impl clone *)
- typed_val clone (fn(∀ α, ∅; &shr{α} ty) → ty) →
- typed_val (rc_make_mut ty clone) (fn(∀ α, ∅; &uniq{α} rc ty) → &uniq{α} ty).
+ typed_val clone (fn(∀ α, ∅; &shr{α}ty) → ty) →
+ typed_val (rc_make_mut ty clone) (fn(∀ α, ∅; &uniq{α}(rc ty)) → &uniq{α}ty).
Proof.
intros Hclone E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros (α ϝ ret arg). inv_vec arg=>rcx. simpl_subst.
iApply (type_new 1); [solve_typing..|]; iIntros (r); simpl_subst.
iApply (type_cont [] [ϝ ⊑ₗ []]
- (λ _, [rcx ◁ box (uninit 1); r ◁ box (&uniq{α} ty)]));
+ (λ _, [rcx ◁ box (uninit 1); r ◁ box (&uniq{α}ty)]));
[solve_typing..| |]; last first.
{ simpl. iAlways. iIntros (k arg). inv_vec arg. simpl_subst.
iApply type_delete; [solve_typing..|].
@@ -1018,7 +1018,7 @@ Section code.
{ iIntros "!> Hty". iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame "Hrc'".
iLeft. by iFrame. }
iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL".
- iApply (type_type _ _ _ [ r ◁ box (uninit 1); #l +ₗ #2 ◁ &uniq{α} ty;
+ iApply (type_type _ _ _ [ r ◁ box (uninit 1); #l +ₗ #2 ◁ &uniq{α}ty;
rcx ◁ box (uninit 1)]
with "[] LFT HE Hna HL Hk [-]"); last first.
{ rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val
@@ -1035,13 +1035,13 @@ Section code.
iDestruct (ty_size_eq with "Hty") as %?.
wp_apply (wp_memcpy with "[$Hlr3 $H↦vlr]"); [lia..|]. iIntros "[Hlr3 Hvlr]".
wp_seq. wp_write. wp_op. iMod ("Hproto" with "[Hvlr]") as "Hna"; first by eauto.
- iMod ("Hclose2" $! (shift_loc lr 2 ↦∗: ty_own ty tid)%I
+ iMod ("Hclose2" $! ((lr +ₗ 2) ↦∗: ty_own ty tid)%I
with "[Hrc' Hlr1 Hlr2 H†] [Hlr3 Hty]") as "[Hb Hα1]".
{ iIntros "!> H !>". iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame.
iLeft. iFrame. rewrite Z2Nat.inj_pos Pos2Nat.inj_succ SuccNat2Pos.id_succ //. }
{ iExists _. iFrame. }
iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL".
- iApply (type_type _ _ _ [ r ◁ box (uninit 1); #(shift_loc lr 2) ◁ &uniq{α} ty;
+ iApply (type_type _ _ _ [ r ◁ box (uninit 1); #(lr +ₗ 2) ◁ &uniq{α}ty;
rcx ◁ box (uninit 1)]
with "[] LFT HE Hna HL Hk [-]"); last first.
{ rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val
@@ -1092,14 +1092,14 @@ Section code.
wp_apply (wp_delete with "[$Hcl↦ Hcl†]");
[lia|by replace (length vl) with (ty.(ty_size))|].
iIntros "_". wp_seq. wp_write.
- iMod ("Hclose2" $! (shift_loc l' 2 ↦∗: ty_own ty tid)%I with
+ iMod ("Hclose2" $! ((l' +ₗ 2) ↦∗: ty_own ty tid)%I with
"[Hrc' Hl' Hl'1 Hl'†] [Hl'2 Hown]") as "[Hl' Hα1]".
{ iIntros "!> H". iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame.
iLeft. iFrame. iDestruct "Hl'†" as "[?|%]"=>//.
by rewrite /Z.to_nat Pos2Nat.inj_succ SuccNat2Pos.id_succ. }
{ iExists _. iFrame. }
iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL".
- iApply (type_type _ _ _ [ #l ◁ rc ty; #l' +ₗ #2 ◁ &uniq{α} ty;
+ iApply (type_type _ _ _ [ #l ◁ rc ty; #l' +ₗ #2 ◁ &uniq{α}ty;
r ◁ box (uninit 1); rcx ◁ box (uninit 1) ]
with "[] LFT HE Hna HL Hk [-]"); last first.
{ rewrite 3!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val
diff --git a/theories/typing/lib/rc/weak.v b/theories/typing/lib/rc/weak.v
index 34417e1cd5f7f8cbd6535e4551c91ee1de538f2a..4e50af06d3d9102ed2c852ca1cfcbfc93ae9d2c5 100644
--- a/theories/typing/lib/rc/weak.v
+++ b/theories/typing/lib/rc/weak.v
@@ -125,13 +125,13 @@ Section code.
delete [ #1; "w" ];; return: ["r"].
Lemma rc_upgrade_type ty `{!TyWf ty} :
- typed_val rc_upgrade (fn(∀ α, ∅; &shr{α} weak ty) → option (rc ty)).
+ typed_val rc_upgrade (fn(∀ α, ∅; &shr{α}(weak ty)) → option (rc ty)).
Proof.
intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros (α ϝ ret arg). inv_vec arg=>w. simpl_subst.
iApply (type_new 2); [solve_typing..|]; iIntros (r); simpl_subst.
iApply (type_cont [] [ϝ ⊑ₗ []]
- (λ _, [w ◁ box (&shr{α} weak ty); r ◁ box (option (rc ty))])) ;
+ (λ _, [w ◁ box (&shr{α}(weak ty)); r ◁ box (option (rc ty))])) ;
[solve_typing..| |]; last first.
{ simpl. iAlways. iIntros (k arg). inv_vec arg. simpl_subst.
iApply type_delete; [solve_typing..|].
@@ -180,7 +180,7 @@ Section code.
rewrite [_ ⋅ _]comm frac_op' -[(_ + _)%Qp]assoc Qp_div_2. auto. }
iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL".
(* Finish up the proof. *)
- iApply (type_type _ _ _ [ w ◁ box (&shr{α} weak ty); #lr ◁ box (uninit 2);
+ iApply (type_type _ _ _ [ w ◁ box (&shr{α}(weak ty)); #lr ◁ box (uninit 2);
#l' ◁ rc ty ]
with "[] LFT HE Hna HL Hk [-]"); last first.
{ rewrite 2!tctx_interp_cons tctx_interp_singleton tctx_hasty_val !tctx_hasty_val' //.
@@ -199,7 +199,7 @@ Section code.
{ iExists _. auto with iFrame. }
iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL".
(* Finish up the proof. *)
- iApply (type_type _ _ _ [ w ◁ box (&shr{α} weak ty); #lr ◁ box (uninit 2) ]
+ iApply (type_type _ _ _ [ w ◁ box (&shr{α}(weak ty)); #lr ◁ box (uninit 2) ]
with "[] LFT HE Hna HL Hk [-]"); last first.
{ rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
unlock. iFrame. iExists [_;_].
@@ -215,7 +215,7 @@ Section code.
{ iExists _. auto with iFrame. }
iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL".
(* Finish up the proof. *)
- iApply (type_type _ _ _ [ w ◁ box (&shr{α} weak ty); #lr ◁ box (uninit 2) ]
+ iApply (type_type _ _ _ [ w ◁ box (&shr{α}(weak ty)); #lr ◁ box (uninit 2) ]
with "[] LFT HE Hna HL Hk [-]"); last first.
{ rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
unlock. iFrame. iExists [_;_].
@@ -235,7 +235,7 @@ Section code.
delete [ #1; "rc" ];; return: ["r"].
Lemma rc_downgrade_type ty `{!TyWf ty} :
- typed_val rc_downgrade (fn(∀ α, ∅; &shr{α} rc ty) → weak ty).
+ typed_val rc_downgrade (fn(∀ α, ∅; &shr{α}(rc ty)) → weak ty).
Proof.
(* TODO : this is almost identical to rc_clone *)
intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
@@ -276,7 +276,7 @@ Section code.
{ iExists _. iFrame "Hrc●". iExists _. rewrite /Z.add Pos.add_1_r. iFrame. }
iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL".
(* Finish up the proof. *)
- iApply (type_type _ _ _ [ x ◁ box (&shr{α} rc ty); #lr ◁ box (weak ty)]
+ iApply (type_type _ _ _ [ x ◁ box (&shr{α}(rc ty)); #lr ◁ box (weak ty)]
with "[] LFT HE Hna HL Hk [-]"); last first.
{ rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
unlock. iFrame "Hx". iFrame "Hr†". iExists [# #l'].
@@ -297,7 +297,7 @@ Section code.
delete [ #1; "w" ];; return: ["r"].
Lemma weak_clone_type ty `{!TyWf ty} :
- typed_val weak_clone (fn(∀ α, ∅; &shr{α} weak ty) → weak ty).
+ typed_val weak_clone (fn(∀ α, ∅; &shr{α}(weak ty)) → weak ty).
Proof.
(* TODO : this is almost identical to rc_clone *)
intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
@@ -320,7 +320,7 @@ Section code.
iModIntro. wp_let. wp_op.
(* Finally, finally... opening the thread-local Rc protocol. *)
iPoseProof "Hpersist" as (ty') "(_ & Hinv & _ & _)".
- iAssert (∃ wv : Z, shift_loc l' 1 ↦ #wv ∗ (shift_loc l' 1 ↦ #(wv + 1) ={⊤}=∗
+ iAssert (∃ wv : Z, (l' +ₗ 1) ↦ #wv ∗ ((l' +ₗ 1) ↦ #(wv + 1) ={⊤}=∗
na_own tid ⊤ ∗ (q / 2).[α] ∗ own γ weak_tok))%I
with "[> Hna Hα1]" as (wv) "[Hwv Hclose2]".
{ iMod (na_inv_open with "Hinv Hna") as "(Hrcproto & Hna & Hclose2)"; [solve_ndisj..|].
@@ -349,7 +349,7 @@ Section code.
iMod ("Hclose2" with "Hwv") as "(Hna & Hα1 & Hwtok)".
iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL". wp_write.
(* Finish up the proof. *)
- iApply (type_type _ _ _ [ x ◁ box (&shr{α} weak ty); #lr ◁ box (weak ty)]
+ iApply (type_type _ _ _ [ x ◁ box (&shr{α}(weak ty)); #lr ◁ box (weak ty)]
with "[] LFT HE Hna HL Hk [-]"); last first.
{ rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
unlock. iFrame. iExists [# #l']. rewrite heap_mapsto_vec_singleton /=.
@@ -389,11 +389,11 @@ Section code.
iIntros (tid) "#LFT #HE Hna HL Hk [Hw [Hw' _]]".
rewrite !tctx_hasty_val [[w]]lock. destruct w' as [[|lw|]|]; try done. wp_op.
iDestruct "Hw'" as (γ ν) "[#Hpersist Hwtok]".
- iAssert (∃ wv : Z, shift_loc lw 1 ↦ #wv ∗
+ iAssert (∃ wv : Z, (lw +ₗ 1) ↦ #wv ∗
((⌜wv = 1⌝ ∗ na_own tid ⊤ ∗
- ∃ s, lw ↦ s ∗ (shift_loc lw 2 ↦∗: λ vl, ⌜length vl = ty.(ty_size)⌝) ∗
+ ∃ s, lw ↦ s ∗ ((lw +ₗ 2) ↦∗: λ vl, ⌜length vl = ty.(ty_size)⌝) ∗
† lw … (2 + ty_size ty)) ∨
- (⌜wv > 1⌝ ∗ (shift_loc lw 1 ↦ #(wv - 1) ={⊤}=∗ na_own tid ⊤))))%I
+ (⌜wv > 1⌝ ∗ ((lw +ₗ 1) ↦ #(wv - 1) ={⊤}=∗ na_own tid ⊤))))%I
with "[>Hna Hwtok]" as (wv) "[Hlw [(% & Hna & H)|[% Hclose]]]".
{ iPoseProof "Hpersist" as (ty') "([>Hszeq _] & Hinv & _ & _)".
iDestruct "Hszeq" as %Hszeq.
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index 7bceb0176a798d81140aa6ab69f8e1bbaca9a91d..87012a873bb7fa74f639dc196f6e91b4d0766d1f 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -15,8 +15,8 @@ Section ref_functions.
own γ (◯ reading_st q ν) -∗
∃ (q' : Qp) n, l ↦ #(Zpos n) ∗ ⌜(q ≤ q')%Qc⌝ ∗
own γ (● Some (to_agree ν, Cinr (q', n)) ⋅ ◯ reading_st q ν) ∗
- ty.(ty_shr) (α ⊓ ν) tid (shift_loc l 1) ∗
- ((1).[ν] ={↑lftN,∅}▷=∗ &{α} shift_loc l 1 ↦∗: ty_own ty tid) ∗
+ ty.(ty_shr) (α ⊓ ν) tid (l +ₗ 1) ∗
+ ((1).[ν] ={↑lftN,∅}▷=∗ &{α}((l +ₗ 1) ↦∗: ty_own ty tid)) ∗
∃ q'', ⌜(q' + q'' = 1)%Qp⌝ ∗ q''.[ν].
Proof.
iIntros "INV H◯".
@@ -99,7 +99,7 @@ Section ref_functions.
iMod ("Hcloseβ" with "Hδ") as "Hβ". iMod ("Hcloseα1" with "[$H↦]") as "Hα2".
iMod ("Hclose'" with "[$Hα1 $Hα2] HL") as "HL". iMod ("Hclose" with "Hβ HL") as "HL".
iApply (type_type _ _ _
- [ x ◁ box (&shr{α} ref β ty); #lr ◁ box(ref β ty)]
+ [ x ◁ box (&shr{α}(ref β ty)); #lr ◁ box(ref β ty)]
with "[] LFT HE Hna HL Hk"); first last.
{ rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
rewrite /= freeable_sz_full. iFrame. iExists _. iFrame. iExists _, _, _, _, _.
@@ -134,7 +134,7 @@ Section ref_functions.
iMod ("Hcloseα" with "[$H↦1 $H↦2]") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
iDestruct (lctx_lft_incl_incl α β with "HL HE") as "#Hαβ"; [solve_typing..|].
iApply (type_type _ _ _
- [ x ◁ box (&shr{α} ref β ty); #lv ◁ &shr{α}ty]
+ [ x ◁ box (&shr{α}(ref β ty)); #lv ◁ &shr{α}ty]
with "[] LFT HE Hna HL Hk"); first last.
{ rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
iFrame. iApply (ty_shr_mono with "[] Hshr"). by iApply lft_incl_glb. }
diff --git a/theories/typing/lib/refcell/refcell.v b/theories/typing/lib/refcell/refcell.v
index f34f6305b309983871d49fd916a7307be9773522..5b7d94c9dc913621f104355ed2e00c22429e901c 100644
--- a/theories/typing/lib/refcell/refcell.v
+++ b/theories/typing/lib/refcell/refcell.v
@@ -36,14 +36,14 @@ Section refcell_inv.
match st return _ with
| None =>
(* Not borrowed. *)
- &{α}(shift_loc l 1 ↦∗: ty.(ty_own) tid)
+ &{α}((l +ₗ 1) ↦∗: ty.(ty_own) tid)
| Some (agν, st) =>
∃ ν, agν ≡ to_agree ν ∗
- (1.[ν] ={↑lftN,∅}▷=∗ &{α}(shift_loc l 1 ↦∗: ty.(ty_own) tid)) ∗
+ (1.[ν] ={↑lftN,∅}▷=∗ &{α}((l +ₗ 1) ↦∗: ty.(ty_own) tid)) ∗
match st with
| Cinr (q, n) =>
(* Immutably borrowed. *)
- ty.(ty_shr) (α ⊓ ν) tid (shift_loc l 1) ∗
+ ty.(ty_shr) (α ⊓ ν) tid (l +ₗ 1) ∗
∃ q', ⌜(q + q')%Qp = 1%Qp⌝ ∗ q'.[ν]
| _ => (* Mutably borrowed. *) True
end
@@ -72,8 +72,8 @@ Section refcell_inv.
rewrite eqtype_unfold. iIntros (Hty) "HL".
iDestruct (Hty with "HL") as "#Hty". iIntros "* !# #HE H".
iDestruct ("Hty" with "HE") as "(% & #Hown & #Hshr)".
- iAssert (□ (&{α} shift_loc l 1 ↦∗: ty_own ty1 tid -∗
- &{α} shift_loc l 1 ↦∗: ty_own ty2 tid))%I as "#Hb".
+ iAssert (□ (&{α}((l +ₗ 1) ↦∗: ty_own ty1 tid) -∗
+ &{α}((l +ₗ 1) ↦∗: ty_own ty2 tid)))%I as "#Hb".
{ iIntros "!# H". iApply bor_iff; last done.
iSplit; iIntros "!>!#H"; iDestruct "H" as (vl) "[Hf H]"; iExists vl;
iFrame; by iApply "Hown". }
@@ -116,7 +116,7 @@ Section refcell.
iDestruct "H" as ([|[[| |n]|]vl]) "[H↦ H]"; try iDestruct "H" as ">[]".
iDestruct "H" as "[>% Hown]".
iMod ("Hclose" $! ((∃ n:Z, l ↦ #n ∗ ⌜-1 ≤ n⌝) ∗
- shift_loc l 1 ↦∗: ty.(ty_own) tid) with "[] [-]")%I as "[H [Htok Htok']]".
+ (l +ₗ 1) ↦∗: ty.(ty_own) tid) with "[] [-]")%I as "[H [Htok Htok']]".
{ iIntros "!> [Hn Hvl] !>". iDestruct "Hn" as (n') "[Hn >%]".
iDestruct "Hvl" as (vl') "[H↦ Hvl]".
iExists (#n'::vl'). rewrite heap_mapsto_vec_cons. iFrame "∗%". }
diff --git a/theories/typing/lib/refcell/refcell_code.v b/theories/typing/lib/refcell/refcell_code.v
index e596aca90194bf294feed5389c3d3c12cb1a559f..9f1f4b40f4c5aef8589cf21b09b9082ee9db68b9 100644
--- a/theories/typing/lib/refcell/refcell_code.v
+++ b/theories/typing/lib/refcell/refcell_code.v
@@ -97,7 +97,7 @@ Section refcell_functions.
rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
iDestruct "HT" as "[Hx Hx']". destruct x' as [[|lx'|]|]; try iDestruct "Hx'" as "[]".
iAssert (&{α} (∃ (z : Z), lx' ↦ #z ∗ ⌜-1 ≤ z⌝) ∗
- (&uniq{α} ty).(ty_own) tid [ #(shift_loc lx' 1)])%I with "[> Hx']" as "[_ Hx']".
+ (&uniq{α} ty).(ty_own) tid [ #(lx' +ₗ 1)])%I with "[> Hx']" as "[_ Hx']".
{ iApply bor_sep; [done..|]. iApply (bor_proper with "Hx'"). iSplit.
- iIntros "[H1 H2]". iDestruct "H1" as (z) "[??]". iDestruct "H2" as (vl) "[??]".
iExists (_::_). rewrite heap_mapsto_vec_cons. iFrame. iFrame.
@@ -108,7 +108,7 @@ Section refcell_functions.
destruct x as [[|lx|]|]; try done. iDestruct "Hx" as "[Hx Hx†]".
iDestruct "Hx" as (vl) "[Hx↦ Hx]". rewrite uninit_own. wp_op.
iApply (type_type _ _ _
- [ #lx ◁ box (uninit 1); #(shift_loc lx' 1) ◁ &uniq{α}ty]
+ [ #lx ◁ box (uninit 1); #(lx' +ₗ 1) ◁ &uniq{α}ty]
with "[] LFT HE Hna HL HC [-]"); last first.
{ rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //. iFrame.
iNext. iExists _. rewrite uninit_own. iFrame. }
@@ -144,7 +144,7 @@ Section refcell_functions.
intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
- iApply (type_cont [] [ϝ ⊑ₗ []] (λ _, [x ◁ box (&shr{α} refcell ty);
+ iApply (type_cont [] [ϝ ⊑ₗ []] (λ _, [x ◁ box (&shr{α}(refcell ty));
r ◁ box (option (ref α ty))]));
[iIntros (k)|iIntros "/= !#"; iIntros (k arg); inv_vec arg]; simpl_subst; last first.
{ iApply type_delete; [solve_typing..|].
@@ -174,7 +174,7 @@ Section refcell_functions.
rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
iDestruct "Hlref" as "[Hlref0 Hlref1]". wp_op. wp_write. wp_op. wp_write.
iAssert (∃ qν ν, (qβ / 2).[β] ∗ (qν).[ν] ∗
- ty_shr ty (β ⊓ ν) tid (shift_loc lx 1) ∗
+ ty_shr ty (β ⊓ ν) tid (lx +ₗ 1) ∗
own γ (◯ reading_st qν ν) ∗ refcell_inv tid lx γ β ty)%I
with "[> Hlx Hownst Hst Hβtok2]" as (q' ν) "(Hβtok2 & Hν & Hshr & Hreading & INV)".
{ destruct st as [[agν [|[q n]|]]|]; try done.
@@ -251,7 +251,7 @@ Section refcell_functions.
intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
- iApply (type_cont [] [ϝ ⊑ₗ []] (λ _, [x ◁ box (&shr{α} refcell ty);
+ iApply (type_cont [] [ϝ ⊑ₗ []] (λ _, [x ◁ box (&shr{α}(refcell ty));
r ◁ box (option (refmut α ty))]));
[iIntros (k)|iIntros "/= !#"; iIntros (k arg); inv_vec arg];
simpl_subst; last first.
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index c372114653cd1a2226065c0abc708940dcdca1fb..acc5cc5b6b0ab94d273889a6b75b1ecccb36c787 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -43,7 +43,7 @@ Section refmut_functions.
iMod ("Hcloseα1" with "[$H↦1 $H↦2]") as "Hα1".
iMod ("Hclose''" with "Hβ HL") as "HL". iMod ("Hclose'" with "[$] HL") as "HL".
iDestruct (lctx_lft_incl_incl α β with "HL HE") as "#Hαβ"; [solve_typing..|].
- iApply (type_type _ _ _ [ x ◁ box (&shr{α} refmut β ty); #lv ◁ &shr{α}ty]
+ iApply (type_type _ _ _ [ x ◁ box (&shr{α}(refmut β ty)); #lv ◁ &shr{α}ty]
with "[] LFT HE Hna HL Hk"); last first.
{ rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
iFrame. iApply (ty_shr_mono with "[] Hshr'").
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index 7b68f9925db04305aac5a4a3d2ce1a3144e2c8f3..6b42693d15983748259cfc2ac43edf72cb27233e 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -35,13 +35,13 @@ Section rwlock_inv.
match st return _ with
| None =>
(* Not locked. *)
- &{α}(shift_loc l 1 ↦∗: ty.(ty_own) tid)
+ &{α}((l +ₗ 1) ↦∗: ty.(ty_own) tid)
| Some (Cinr (agν, q, n)) =>
(* Locked for read. *)
∃ (ν : lft) q', agν ≡ to_agree ν ∗
□ (1.[ν] ={↑lftN,∅}▷=∗ [†ν]) ∗
- ([†ν] ={↑lftN}=∗ &{α}(shift_loc l 1 ↦∗: ty.(ty_own) tid)) ∗
- ty.(ty_shr) (α ⊓ ν) tid (shift_loc l 1) ∗
+ ([†ν] ={↑lftN}=∗ &{α}((l +ₗ 1) ↦∗: ty.(ty_own) tid)) ∗
+ ty.(ty_shr) (α ⊓ ν) tid (l +ₗ 1) ∗
⌜(q + q')%Qp = 1%Qp⌝ ∗ q'.[ν]
| _ => (* Locked for write. *) True
end)%I.
@@ -68,8 +68,8 @@ Section rwlock_inv.
rewrite eqtype_unfold. iIntros (Hty) "HL".
iDestruct (Hty with "HL") as "#Hty". iIntros "* !# #HE H".
iDestruct ("Hty" with "HE") as "(% & #Hown & #Hshr)".
- iAssert (□ (&{α} shift_loc l 1 ↦∗: ty_own ty1 tid -∗
- &{α} shift_loc l 1 ↦∗: ty_own ty2 tid))%I as "#Hb".
+ iAssert (□ (&{α}((l +ₗ 1) ↦∗: ty_own ty1 tid) -∗
+ &{α}((l +ₗ 1) ↦∗: ty_own ty2 tid)))%I as "#Hb".
{ iIntros "!# H". iApply bor_iff; last done.
iSplit; iIntros "!>!#H"; iDestruct "H" as (vl) "[Hf H]"; iExists vl;
iFrame; by iApply "Hown". }
@@ -111,7 +111,7 @@ Section rwlock.
iDestruct "H" as ([|[[| |n]|]vl]) "[H↦ H]"; try iDestruct "H" as ">[]".
iDestruct "H" as "[>% Hown]".
iMod ("Hclose" $! ((∃ n:Z, l ↦ #n ∗ ⌜-1 ≤ n⌝) ∗
- shift_loc l 1 ↦∗: ty.(ty_own) tid) with "[] [-]")%I as "[H [Htok Htok']]".
+ (l +ₗ 1) ↦∗: ty.(ty_own) tid) with "[] [-]")%I as "[H [Htok Htok']]".
{ iIntros "!> [Hn Hvl] !>". iDestruct "Hn" as (n') "[Hn >%]".
iDestruct "Hvl" as (vl') "[H↦ Hvl]".
iExists (#n'::vl'). rewrite heap_mapsto_vec_cons. iFrame "∗%". }
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index 1df9e471c467720beb870c236caf03a96ac35f2a..50415055395e6c7abad309b74527c52cc1f126b4 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -97,7 +97,7 @@ Section rwlock_functions.
rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
iDestruct "HT" as "[Hx Hx']". destruct x' as [[|lx'|]|]; try iDestruct "Hx'" as "[]".
iAssert (&{α} (∃ (z : Z), lx' ↦ #z ∗ ⌜-1 ≤ z⌝) ∗
- (&uniq{α} ty).(ty_own) tid [ #(shift_loc lx' 1)])%I with "[> Hx']" as "[_ Hx']".
+ (&uniq{α} ty).(ty_own) tid [ #(lx' +ₗ 1)])%I with "[> Hx']" as "[_ Hx']".
{ iApply bor_sep; [done..|]. iApply (bor_proper with "Hx'"). iSplit.
- iIntros "[H1 H2]". iDestruct "H1" as (z) "[??]". iDestruct "H2" as (vl) "[??]".
iExists (_::_). rewrite heap_mapsto_vec_cons. iFrame. iFrame.
@@ -108,7 +108,7 @@ Section rwlock_functions.
destruct x as [[|lx|]|]; try done. iDestruct "Hx" as "[Hx Hx†]".
iDestruct "Hx" as (vl) "[Hx↦ Hx]". rewrite uninit_own. wp_op.
iApply (type_type _ _ _
- [ #lx ◁ box (uninit 1); #(shift_loc lx' 1) ◁ &uniq{α}ty]
+ [ #lx ◁ box (uninit 1); #(lx' +ₗ 1) ◁ &uniq{α}ty]
with "[] LFT HE Hna HL HC [-]"); last first.
{ rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //. iFrame.
iNext. iExists _. rewrite uninit_own. iFrame. }
@@ -145,7 +145,7 @@ Section rwlock_functions.
iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
iApply type_deref; [solve_typing..|]. iIntros (x'). simpl_subst.
- iApply (type_cont [] [ϝ ⊑ₗ []] (λ _, [x ◁ box (&shr{α} rwlock ty);
+ iApply (type_cont [] [ϝ ⊑ₗ []] (λ _, [x ◁ box (&shr{α}(rwlock ty));
r ◁ box (option (rwlockreadguard α ty))]));
[iIntros (k)|iIntros "/= !#"; iIntros (k arg); inv_vec arg];
simpl_subst; last first.
@@ -181,7 +181,7 @@ Section rwlock_functions.
destruct (decide (Z_of_rwlock_st st = Z_of_rwlock_st st')) as [->|?]=>?.
+ iApply (wp_cas_int_suc with "Hlx"); first done. iNext. iIntros "Hlx".
iAssert (∃ qν ν, (qβ / 2).[β] ∗ (qν).[ν] ∗
- ty_shr ty (β ⊓ ν) tid (shift_loc lx 1) ∗
+ ty_shr ty (β ⊓ ν) tid (lx +ₗ 1) ∗
own γ (◯ reading_st qν ν) ∗ rwlock_inv tid lx γ β ty ∗
((1).[ν] ={↑lftN,∅}▷=∗ [†ν]))%I
with "[> Hlx Hownst Hst Hβtok2]"
@@ -257,7 +257,7 @@ Section rwlock_functions.
Proof.
intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
- iApply (type_cont [_] [ϝ ⊑ₗ []] (λ r, [x ◁ box (&shr{α} rwlock ty);
+ iApply (type_cont [_] [ϝ ⊑ₗ []] (λ r, [x ◁ box (&shr{α}(rwlock ty));
r!!!0 ◁ box (option (rwlockwriteguard α ty))]));
[iIntros (k)|iIntros "/= !#"; iIntros (k arg); inv_vec arg=>r];
simpl_subst; last first.
diff --git a/theories/typing/lib/rwlock/rwlockreadguard.v b/theories/typing/lib/rwlock/rwlockreadguard.v
index 6bbcfe1da774a26999f5134711a3a9cba080aab4..1beca19de117fbf603e802b726bf8ee0352f217b 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard.v
@@ -20,7 +20,7 @@ Section rwlockreadguard.
ty_own tid vl :=
match vl return _ with
| [ #(LitLoc l) ] =>
- ∃ ν q γ β, ty.(ty_shr) (α ⊓ ν) tid (shift_loc l 1) ∗
+ ∃ ν q γ β, ty.(ty_shr) (α ⊓ ν) tid (l +ₗ 1) ∗
α ⊑ β ∗ &at{β,rwlockN}(rwlock_inv tid l γ β ty) ∗
q.[ν] ∗ own γ (◯ reading_st q ν) ∗
(1.[ν] ={↑lftN,∅}▷=∗ [†ν])
@@ -29,7 +29,7 @@ Section rwlockreadguard.
ty_shr κ tid l :=
∃ (l' : loc),
&frac{κ} (λ q, l↦∗{q} [ #l']) ∗
- ▷ ty.(ty_shr) (α ⊓ κ) tid (shift_loc l' 1) |}%I.
+ ▷ ty.(ty_shr) (α ⊓ κ) tid (l' +ₗ 1) |}%I.
Next Obligation. intros α ty tid [|[[]|] []]; auto. Qed.
Next Obligation.
iIntros (α ty E κ l tid q ?) "#LFT Hb Htok".
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index a746c7a10632317ec7b1845d9c4c96bc847bba4f..5e3905c02b1e40ffe984b2579285943403b53631 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -20,7 +20,7 @@ Section rwlockreadguard_functions.
Lemma rwlockreadguard_deref_type ty `{!TyWf ty} :
typed_val rwlockreadguard_deref
- (fn(∀ '(α, β), ∅; &shr{α} rwlockreadguard β ty) → &shr{α} ty).
+ (fn(∀ '(α, β), ∅; &shr{α}(rwlockreadguard β ty)) → &shr{α} ty).
Proof.
intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros ([α β] ϝ ret arg). inv_vec arg=>x. simpl_subst.
@@ -34,8 +34,8 @@ Section rwlockreadguard_functions.
rewrite heap_mapsto_vec_singleton. wp_read. wp_op. wp_let.
iMod ("Hcloseα" with "[$H↦]") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
iDestruct (lctx_lft_incl_incl α β with "HL HE") as "#Hαβ"; [solve_typing..|].
- iApply (type_type _ _ _ [ x ◁ box (&shr{α} rwlockreadguard β ty);
- #(shift_loc l' 1) ◁ &shr{α}ty]
+ iApply (type_type _ _ _ [ x ◁ box (&shr{α}(rwlockreadguard β ty));
+ #(l' +ₗ 1) ◁ &shr{α}ty]
with "[] LFT HE Hna HL Hk"); first last.
{ rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
iFrame. iApply (ty_shr_mono with "[] Hshr"). iApply lft_incl_glb; first done.
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard.v b/theories/typing/lib/rwlock/rwlockwriteguard.v
index 9ba6c32700a9205dcd8e397224e04848dadb0be8..1d2f6512b3dbbb5065e481c80fdc3ed300ac20cd 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard.v
@@ -21,7 +21,7 @@ Section rwlockwriteguard.
ty_own tid vl :=
match vl return _ with
| [ #(LitLoc l) ] =>
- ∃ γ β, &{β}(shift_loc l 1 ↦∗: ty.(ty_own) tid) ∗
+ ∃ γ β, &{β}((l +ₗ 1) ↦∗: ty.(ty_own) tid) ∗
α ⊑ β ∗ &at{β,rwlockN}(rwlock_inv tid l γ β ty) ∗
own γ (◯ writing_st)
| _ => False
@@ -30,7 +30,7 @@ Section rwlockwriteguard.
∃ (l' : loc),
&frac{κ} (λ q, l↦∗{q} [ #l']) ∗
□ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ q.[α ⊓ κ] ={F, F∖↑shrN}▷=∗
- ty.(ty_shr) (α ⊓ κ) tid (shift_loc l' 1) ∗ q.[α ⊓ κ] |}%I.
+ ty.(ty_shr) (α ⊓ κ) tid (l' +ₗ 1) ∗ q.[α ⊓ κ] |}%I.
Next Obligation. by iIntros (???[|[[]|][]]) "?". Qed.
Next Obligation.
iIntros (α ty E κ l tid q HE) "#LFT Hb Htok".
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard_code.v b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
index c19d95e4f4a874c42ce8b14124b876fb86205432..548fe054bf5a19e9073dcf9fdbbc0ea22c17f6ca 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
@@ -20,7 +20,7 @@ Section rwlockwriteguard_functions.
Lemma rwlockwriteguard_deref_type ty `{!TyWf ty} :
typed_val rwlockwriteguard_deref
- (fn(∀ '(α, β), ∅; &shr{α} rwlockwriteguard β ty) → &shr{α} ty).
+ (fn(∀ '(α, β), ∅; &shr{α}(rwlockwriteguard β ty)) → &shr{α} ty).
Proof.
intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros ([α β] ϝ ret arg). inv_vec arg=>x. simpl_subst.
@@ -43,8 +43,8 @@ Section rwlockwriteguard_functions.
iMod ("Hcloseα1" with "[$H↦1 $H↦2]") as "Hα1". iMod ("Hclose'" with "Hβ HL") as "HL".
iMod ("Hclose" with "[$] HL") as "HL".
iDestruct (lctx_lft_incl_incl α β with "HL HE") as "#Hαβ"; [solve_typing..|].
- iApply (type_type _ _ _ [ x ◁ box (&shr{α} rwlockwriteguard β ty);
- #(shift_loc l' 1) ◁ &shr{α}ty]
+ iApply (type_type _ _ _ [ x ◁ box (&shr{α}(rwlockwriteguard β ty));
+ #(l' +ₗ 1) ◁ &shr{α}ty]
with "[] LFT HE Hna HL Hk"); last first.
{ rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
iFrame. iApply (ty_shr_mono with "[] Hshr'"). iApply lft_incl_glb; first done.
@@ -64,7 +64,7 @@ Section rwlockwriteguard_functions.
Lemma rwlockwriteguard_derefmut_type ty `{!TyWf ty} :
typed_val rwlockwriteguard_derefmut
- (fn(∀ '(α, β), ∅; &uniq{α} rwlockwriteguard β ty) → &uniq{α} ty).
+ (fn(∀ '(α, β), ∅; &uniq{α}(rwlockwriteguard β ty)) → &uniq{α}ty).
Proof.
intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros ([α β] ϝ ret arg). inv_vec arg=>x. simpl_subst.
@@ -88,7 +88,7 @@ Section rwlockwriteguard_functions.
wp_read. wp_op. wp_let. iMod "Hb".
iMod ("Hcloseα" with "[$H↦]") as "[_ Hα]". iMod ("Hclose" with "Hα HL") as "HL".
iDestruct (lctx_lft_incl_incl α β with "HL HE") as "#Hαβ"; [solve_typing..|].
- iApply (type_type _ _ _ [ x ◁ box (uninit 1); #(shift_loc l 1) ◁ &uniq{α}ty]
+ iApply (type_type _ _ _ [ x ◁ box (uninit 1); #(l +ₗ 1) ◁ &uniq{α}ty]
with "[] LFT HE Hna HL Hk"); last first.
{ rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
iFrame. iApply (bor_shorten with "[] Hb"). iApply lft_incl_glb.
diff --git a/theories/typing/own.v b/theories/typing/own.v
index 47db32f457251651d7f7e3e2d0e19aea48648ebd..d1b7551dfdab0a973f5d5343cb9f11a5de508aef 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -32,7 +32,7 @@ Section own.
Proof. rewrite freeable_sz_full. iSplit; auto. iIntros "[$|%]"; done. Qed.
Lemma freeable_sz_split n sz1 sz2 l :
- freeable_sz n sz1 l ∗ freeable_sz n sz2 (shift_loc l sz1) ⊣⊢
+ freeable_sz n sz1 l ∗ freeable_sz n sz2 (l +ₗ sz1) ⊣⊢
freeable_sz n (sz1 + sz2) l.
Proof.
destruct sz1; [|destruct sz2;[|rewrite /freeable_sz plus_Sn_m; destruct n]].
diff --git a/theories/typing/product.v b/theories/typing/product.v
index 6fab9f41432f7e536f210e25ac06312e5b17d3a4..f69b987372f6d43b2e54bbbbfae4f8f5fa8dcf74 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -38,7 +38,7 @@ Section product.
Lemma split_prod_mt tid ty1 ty2 q l :
(l ↦∗{q}: λ vl,
∃ vl1 vl2, ⌜vl = vl1 ++ vl2⌝ ∗ ty1.(ty_own) tid vl1 ∗ ty2.(ty_own) tid vl2)%I
- ⊣⊢ l ↦∗{q}: ty1.(ty_own) tid ∗ shift_loc l ty1.(ty_size) ↦∗{q}: ty2.(ty_own) tid.
+ ⊣⊢ l ↦∗{q}: ty1.(ty_own) tid ∗ (l +ₗ ty1.(ty_size)) ↦∗{q}: ty2.(ty_own) tid.
Proof.
iSplit; iIntros "H".
- iDestruct "H" as (vl) "[H↦ H]". iDestruct "H" as (vl1 vl2) "(% & H1 & H2)".
@@ -57,7 +57,7 @@ Section product.
⌜vl = vl1 ++ vl2⌝ ∗ ty1.(ty_own) tid vl1 ∗ ty2.(ty_own) tid vl2)%I;
ty_shr κ tid l :=
(ty1.(ty_shr) κ tid l ∗
- ty2.(ty_shr) κ tid (shift_loc l ty1.(ty_size)))%I |}.
+ ty2.(ty_shr) κ tid (l +ₗ ty1.(ty_size)))%I |}.
Next Obligation.
iIntros (ty1 ty2 tid vl) "H". iDestruct "H" as (vl1 vl2) "(% & H1 & H2)".
subst. rewrite app_length !ty_size_eq.
@@ -116,7 +116,7 @@ Section product.
{ rewrite <-HF. apply shr_locsE_subseteq. simpl. clear. omega. }
iMod (@copy_shr_acc with "LFT H2 Htl Htok2") as (q2) "(Htl & H2 & Hclose2)"; first solve_ndisj.
{ move: HF. rewrite /= -plus_assoc shr_locsE_shift.
- assert (shr_locsE l (ty_size ty1) ⊥ shr_locsE (shift_loc l (ty_size ty1)) (ty_size ty2 + 1))
+ assert (shr_locsE l (ty_size ty1) ⊥ shr_locsE (l +ₗ (ty_size ty1)) (ty_size ty2 + 1))
by exact: shr_locsE_disj.
set_solver. }
iDestruct (na_own_acc with "Htl") as "[$ Htlclose]".
diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v
index 3d1a4eb29e9fed14c33b7b17dff64c5368115b76..525c039cd1d73a3dd84550cb50ad670556d2b45e 100644
--- a/theories/typing/product_split.v
+++ b/theories/typing/product_split.v
@@ -139,7 +139,7 @@ Section product_split.
(** Unique borrows *)
Lemma tctx_split_uniq_prod2 E L p κ ty1 ty2 :
- tctx_incl E L [p ◁ &uniq{κ} product2 ty1 ty2]
+ tctx_incl E L [p ◁ &uniq{κ}(product2 ty1 ty2)]
[p ◁ &uniq{κ} ty1; p +ₗ #ty1.(ty_size) ◁ &uniq{κ} ty2].
Proof.
iIntros (tid q) "#LFT _ $ H".
@@ -152,7 +152,7 @@ Section product_split.
Lemma tctx_merge_uniq_prod2 E L p κ ty1 ty2 :
tctx_incl E L [p ◁ &uniq{κ} ty1; p +ₗ #ty1.(ty_size) ◁ &uniq{κ} ty2]
- [p ◁ &uniq{κ} product2 ty1 ty2].
+ [p ◁ &uniq{κ}(product2 ty1 ty2)].
Proof.
iIntros (tid q) "#LFT _ $ H".
rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
@@ -163,11 +163,11 @@ Section product_split.
Qed.
Lemma uniq_is_ptr κ ty tid (vl : list val) :
- ty_own (&uniq{κ} ty) tid vl -∗ ⌜∃ l : loc, vl = [(#l) : val]⌝.
+ ty_own (&uniq{κ}ty) tid vl -∗ ⌜∃ l : loc, vl = [(#l) : val]⌝.
Proof. iIntros "H". destruct vl as [|[[]|][]]; eauto. Qed.
Lemma tctx_split_uniq_prod E L κ tyl p :
- tctx_incl E L [p ◁ &uniq{κ} product tyl]
+ tctx_incl E L [p ◁ &uniq{κ}(product tyl)]
(hasty_ptr_offsets p (uniq_bor κ) tyl 0).
Proof.
apply tctx_split_ptr_prod.
@@ -178,7 +178,7 @@ Section product_split.
Lemma tctx_merge_uniq_prod E L κ tyl :
tyl ≠ [] →
∀ p, tctx_incl E L (hasty_ptr_offsets p (uniq_bor κ) tyl 0)
- [p ◁ &uniq{κ} product tyl].
+ [p ◁ &uniq{κ}(product tyl)].
Proof.
intros. apply tctx_merge_ptr_prod; try done.
- apply _.
@@ -188,7 +188,7 @@ Section product_split.
(** Shared borrows *)
Lemma tctx_split_shr_prod2 E L p κ ty1 ty2 :
- tctx_incl E L [p ◁ &shr{κ} product2 ty1 ty2]
+ tctx_incl E L [p ◁ &shr{κ}(product2 ty1 ty2)]
[p ◁ &shr{κ} ty1; p +ₗ #ty1.(ty_size) ◁ &shr{κ} ty2].
Proof.
iIntros (tid q) "#LFT _ $ H".
@@ -200,7 +200,7 @@ Section product_split.
Lemma tctx_merge_shr_prod2 E L p κ ty1 ty2 :
tctx_incl E L [p ◁ &shr{κ} ty1; p +ₗ #ty1.(ty_size) ◁ &shr{κ} ty2]
- [p ◁ &shr{κ} product2 ty1 ty2].
+ [p ◁ &shr{κ}(product2 ty1 ty2)].
Proof.
iIntros (tid q) "#LFT _ $ H".
rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
@@ -214,7 +214,7 @@ Section product_split.
Proof. iIntros "H". destruct vl as [|[[]|][]]; eauto. Qed.
Lemma tctx_split_shr_prod E L κ tyl p :
- tctx_incl E L [p ◁ &shr{κ} product tyl]
+ tctx_incl E L [p ◁ &shr{κ}(product tyl)]
(hasty_ptr_offsets p (shr_bor κ) tyl 0).
Proof.
apply tctx_split_ptr_prod.
@@ -225,7 +225,7 @@ Section product_split.
Lemma tctx_merge_shr_prod E L κ tyl :
tyl ≠ [] →
∀ p, tctx_incl E L (hasty_ptr_offsets p (shr_bor κ) tyl 0)
- [p ◁ &shr{κ} product tyl].
+ [p ◁ &shr{κ}(product tyl)].
Proof.
intros. apply tctx_merge_ptr_prod; try done.
- apply _.
@@ -247,14 +247,14 @@ Section product_split.
Lemma tctx_extract_split_uniq_prod E L p p' κ ty tyl T T' :
tctx_extract_hasty E L p' ty (hasty_ptr_offsets p (uniq_bor κ) tyl 0) T' →
- tctx_extract_hasty E L p' ty ((p ◁ &uniq{κ} Π tyl) :: T) (T' ++ T).
+ tctx_extract_hasty E L p' ty ((p ◁ &uniq{κ}(Π tyl)) :: T) (T' ++ T).
Proof.
intros. apply (tctx_incl_frame_r T [_] (_::_)). by rewrite tctx_split_uniq_prod.
Qed.
Lemma tctx_extract_split_shr_prod E L p p' κ ty tyl T T' :
tctx_extract_hasty E L p' ty (hasty_ptr_offsets p (shr_bor κ) tyl 0) T' →
- tctx_extract_hasty E L p' ty ((p ◁ &shr{κ} Π tyl) :: T) ((p ◁ &shr{κ} Π tyl) :: T).
+ tctx_extract_hasty E L p' ty ((p ◁ &shr{κ}(Π tyl)) :: T) ((p ◁ &shr{κ}(Π tyl)) :: T).
Proof.
intros. apply (tctx_incl_frame_r _ [_] [_;_]).
rewrite {1}copy_tctx_incl. apply (tctx_incl_frame_r _ [_] [_]).
@@ -291,13 +291,13 @@ Section product_split.
Lemma tctx_extract_merge_uniq_prod E L p κ tyl T T' :
tyl ≠ [] →
extract_tyl E L p (uniq_bor κ) tyl 0 T T' →
- tctx_extract_hasty E L p (&uniq{κ}Π tyl) T T'.
+ tctx_extract_hasty E L p (&uniq{κ}(Π tyl)) T T'.
Proof. auto using tctx_extract_merge_ptr_prod, tctx_merge_uniq_prod. Qed.
Lemma tctx_extract_merge_shr_prod E L p κ tyl T T' :
tyl ≠ [] →
extract_tyl E L p (shr_bor κ) tyl 0 T T' →
- tctx_extract_hasty E L p (&shr{κ}Π tyl) T T'.
+ tctx_extract_hasty E L p (&shr{κ}(Π tyl)) T T'.
Proof. auto using tctx_extract_merge_ptr_prod, tctx_merge_shr_prod. Qed.
End product_split.
diff --git a/theories/typing/shr_bor.v b/theories/typing/shr_bor.v
index 66e76ea8403a3802e82b5455a46b61ebf915a0f5..3d4bfc702d53d650ca1e5b93221ccd02a722fe52 100644
--- a/theories/typing/shr_bor.v
+++ b/theories/typing/shr_bor.v
@@ -19,16 +19,23 @@ Section shr_bor.
Global Instance shr_bor_wf κ ty `{!TyWf ty} : TyWf (shr_bor κ ty) :=
{ ty_lfts := [κ]; ty_wf_E := ty.(ty_wf_E) ++ ty.(ty_outlives_E) κ }.
+ Lemma shr_type_incl κ1 κ2 ty1 ty2 :
+ κ2 ⊑ κ1 -∗ type_incl ty1 ty2 -∗ type_incl (shr_bor κ1 ty1) (shr_bor κ2 ty2).
+ Proof.
+ iIntros "#Hκ #[_ [_ Hty]]". iApply type_incl_simple_type. simpl.
+ iIntros "!#" (tid [|[[]|][]]) "H"; try done. iApply "Hty".
+ iApply (ty1.(ty_shr_mono) with "Hκ"). done.
+ Qed.
+
Global Instance shr_mono E L :
Proper (flip (lctx_lft_incl E L) ==> subtype E L ==> subtype E L) shr_bor.
Proof.
- intros κ1 κ2 Hκ ty1 ty2 Hty. apply subtype_simple_type.
+ intros κ1 κ2 Hκ ty1 ty2 Hty.
iIntros (?) "/= HL". iDestruct (Hκ with "HL") as "#Hincl".
iDestruct (Hty with "HL") as "#Hty". iIntros "!# #HE".
- iIntros (? [|[[]|][]]) "H"; try done. iDestruct ("Hincl" with "HE") as "#Hκ".
- iApply (ty2.(ty_shr_mono) with "Hκ").
- iDestruct ("Hty" with "HE") as "(_ & _ & #Hs1)"; [done..|clear Hty].
- by iApply "Hs1".
+ iApply shr_type_incl.
+ - by iApply "Hincl".
+ - by iApply "Hty".
Qed.
Global Instance shr_mono_flip E L :
Proper (lctx_lft_incl E L ==> flip (subtype E L) ==> flip (subtype E L)) shr_bor.
@@ -51,18 +58,17 @@ Section shr_bor.
Proof. by iIntros (Hsync tid1 tid2 [|[[]|][]]) "H"; try iApply Hsync. Qed.
End shr_bor.
-Notation "&shr{ κ } ty" := (shr_bor κ ty)
- (format "&shr{ κ } ty", at level 20, right associativity) : lrust_type_scope.
+Notation "&shr{ κ }" := (shr_bor κ) (format "&shr{ κ }") : lrust_type_scope.
Section typing.
Context `{typeG Σ}.
Lemma shr_mono' E L κ1 κ2 ty1 ty2 :
lctx_lft_incl E L κ2 κ1 → subtype E L ty1 ty2 →
- subtype E L (&shr{κ1} ty1) (&shr{κ2} ty2).
+ subtype E L (&shr{κ1}ty1) (&shr{κ2}ty2).
Proof. by intros; apply shr_mono. Qed.
Lemma shr_proper' E L κ ty1 ty2 :
- eqtype E L ty1 ty2 → eqtype E L (&shr{κ} ty1) (&shr{κ} ty2).
+ eqtype E L ty1 ty2 → eqtype E L (&shr{κ}ty1) (&shr{κ}ty2).
Proof. by intros; apply shr_proper. Qed.
Lemma tctx_reborrow_shr E L p ty κ κ' :
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index 585a95e4e258eb9bf712a961af0e3ecd433f1987..6ad1ecb4c9aeb13f5213f47413d3414a6a30abe3 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -32,8 +32,8 @@ Section sum.
⌜length vl = S (max_list_with ty_size tyl)⌝ ∗
ty_own (nth i tyl emp0) tid vl')%I
⊣⊢ ∃ (i : nat), (l ↦{q} #i ∗
- shift_loc l (S $ (nth i tyl emp0).(ty_size)) ↦∗{q}: is_pad i tyl) ∗
- shift_loc l 1 ↦∗{q}: (nth i tyl emp0).(ty_own) tid.
+ (l +ₗ (S $ (nth i tyl emp0).(ty_size))) ↦∗{q}: is_pad i tyl) ∗
+ (l +ₗ 1) ↦∗{q}: (nth i tyl emp0).(ty_own) tid.
Proof.
iSplit; iIntros "H".
- iDestruct "H" as (vl) "[Hmt Hown]". iDestruct "Hown" as (i vl' vl'') "(% & % & Hown)".
@@ -60,9 +60,9 @@ Section sum.
(nth i tyl emp0).(ty_own) tid vl')%I;
ty_shr κ tid l :=
(∃ (i : nat),
- (&frac{κ} λ q, l ↦{q} #i ∗
- shift_loc l (S $ (nth i tyl emp0).(ty_size)) ↦∗{q}: is_pad i tyl) ∗
- (nth i tyl emp0).(ty_shr) κ tid (shift_loc l 1))%I
+ &frac{κ} (λ q, l ↦{q} #i ∗
+ (l +ₗ (S $ (nth i tyl emp0).(ty_size))) ↦∗{q}: is_pad i tyl) ∗
+ (nth i tyl emp0).(ty_shr) κ tid (l +ₗ 1))%I
|}.
Next Obligation.
iIntros (tyl tid vl) "Hown". iDestruct "Hown" as (i vl' vl'') "(%&%&_)".
@@ -197,7 +197,7 @@ Section sum.
apply shr_locsE_subseteq. omega. }
iDestruct (na_own_acc with "Htl") as "[$ Htlclose]".
{ apply difference_mono_l.
- trans (shr_locsE (shift_loc l 1) (max_list_with ty_size tyl)).
+ trans (shr_locsE (l +ₗ 1) (max_list_with ty_size tyl)).
- apply shr_locsE_subseteq. omega.
- set_solver+. }
destruct (Qp_lower_bound q'1 q'2) as (q' & q'01 & q'02 & -> & ->).
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 7adb46bcc1a35be23e443e5ad2d6a600222a0500..21cefb195c8614ce417505f2cdd6e70b58792d49 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -126,18 +126,15 @@ Program Definition ty_of_st `{typeG Σ} (st : simple_type) : type :=
borrow, otherwise I do not know how to prove the shr part of
[subtype_shr_mono]. *)
ty_shr := λ κ tid l,
- (∃ vl, (&frac{κ} λ q, l ↦∗{q} vl) ∗
- ▷ st.(st_own) tid vl)%I
+ (∃ vl, &frac{κ} (λ q, l ↦∗{q} vl) ∗ ▷ st.(st_own) tid vl)%I
|}.
Next Obligation. intros. apply st_size_eq. Qed.
Next Obligation.
iIntros (?? st E κ l tid ??) "#LFT Hmt Hκ".
iMod (bor_exists with "LFT Hmt") as (vl) "Hmt"; first solve_ndisj.
iMod (bor_sep with "LFT Hmt") as "[Hmt Hown]"; first solve_ndisj.
- iMod (bor_persistent with "LFT Hown") as "[Hown|#H†]"; first solve_ndisj.
- - iFrame "Hκ".
- iMod (bor_fracture with "LFT [Hmt]") as "Hfrac"; by eauto with iFrame.
- - iExFalso. by iApply (lft_tok_dead with "Hκ").
+ iMod (bor_persistent_tok with "LFT Hown Hκ") as "[Hown $]"; first solve_ndisj.
+ iMod (bor_fracture with "LFT [Hmt]") as "Hfrac"; by eauto with iFrame.
Qed.
Next Obligation.
iIntros (?? st κ κ' tid l) "#Hord H".
@@ -378,7 +375,7 @@ End type_contractive.
(* Tactic automation. *)
Ltac f_type_equiv :=
first [ ((eapply ty_size_type_dist || eapply ty_shr_type_dist || eapply ty_own_type_dist); try reflexivity) |
- match goal with | |- @dist_later ?A ?n ?x ?y =>
+ match goal with | |- @dist_later ?A _ ?n ?x ?y =>
destruct n as [|n]; [exact I|change (@dist A _ n x y)]
end ].
Ltac solve_type_proper :=
@@ -389,7 +386,7 @@ Ltac solve_type_proper :=
Fixpoint shr_locsE (l : loc) (n : nat) : coPset :=
match n with
| 0%nat => ∅
- | S n => ↑shrN.@l ∪ shr_locsE (shift_loc l 1%nat) n
+ | S n => ↑shrN.@l ∪ shr_locsE (l +ₗ 1%nat) n
end.
Class Copy `{typeG Σ} (t : type) := {
@@ -436,7 +433,7 @@ Section type.
(** Copy types *)
Lemma shr_locsE_shift l n m :
- shr_locsE l (n + m) = shr_locsE l n ∪ shr_locsE (shift_loc l n) m.
+ shr_locsE l (n + m) = shr_locsE l n ∪ shr_locsE (l +ₗ n) m.
Proof.
revert l; induction n; intros l.
- rewrite shift_loc_0. set_solver+.
@@ -445,7 +442,7 @@ Section type.
Qed.
Lemma shr_locsE_disj l n m :
- shr_locsE l n ⊥ shr_locsE (shift_loc l n) m.
+ shr_locsE l n ⊥ shr_locsE (l +ₗ n) m.
Proof.
revert l; induction n; intros l.
- simpl. set_solver+.
@@ -473,7 +470,7 @@ Section type.
Lemma shr_locsE_split_tok l n m tid :
na_own tid (shr_locsE l (n + m)) ⊣⊢
- na_own tid (shr_locsE l n) ∗ na_own tid (shr_locsE (shift_loc l n) m).
+ na_own tid (shr_locsE l n) ∗ na_own tid (shr_locsE (l +ₗ n) m).
Proof.
rewrite shr_locsE_shift na_own_union //. apply shr_locsE_disj.
Qed.
@@ -642,16 +639,24 @@ Section subtyping.
- intros ??? H1 H2. split; etrans; (apply H1 || apply H2).
Qed.
+ Lemma type_incl_simple_type (st1 st2 : simple_type) :
+ □ (∀ tid vl, st1.(st_own) tid vl -∗ st2.(st_own) tid vl) -∗
+ type_incl st1 st2.
+ Proof.
+ iIntros "#Hst". iSplit; first done. iSplit; iAlways.
+ - iIntros. iApply "Hst"; done.
+ - iIntros (???). iDestruct 1 as (vl) "[Hf Hown]". iExists vl. iFrame "Hf".
+ by iApply "Hst".
+ Qed.
+
Lemma subtype_simple_type E L (st1 st2 : simple_type) :
(∀ qL, llctx_interp L qL -∗ □ (elctx_interp E -∗
∀ tid vl, st1.(st_own) tid vl -∗ st2.(st_own) tid vl)) →
subtype E L st1 st2.
Proof.
intros Hst. iIntros (qL) "HL". iDestruct (Hst with "HL") as "#Hst".
- iClear "∗". iIntros "!# #HE". iSplit; first done. iSplit; iAlways.
- - iIntros. iApply "Hst"; done.
- - iIntros (???). iDestruct 1 as (vl) "[Hf Hown]". iExists vl. iFrame "Hf".
- by iApply "Hst".
+ iClear "∗". iIntros "!# #HE". iApply type_incl_simple_type.
+ iIntros "!#" (??) "?". by iApply "Hst".
Qed.
Lemma subtype_weaken E1 E2 L1 L2 ty1 ty2 :
diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v
index 7b1b47e91406a47c494f70229b5aabf86f54ff9d..aec79f460df6a8511cd8e2d623a1dafdc2e0886d 100644
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
@@ -26,7 +26,7 @@ Section type_context.
match p with
| BinOp OffsetOp e (Lit (LitInt n)) =>
match eval_path e with
- | Some (#(LitLoc l)) => Some (#(shift_loc l n))
+ | Some (#(LitLoc l)) => Some (#(l +ₗ n))
| _ => None
end
| e => to_val e
diff --git a/theories/typing/type_sum.v b/theories/typing/type_sum.v
index b642ba7499cf1824e5d7a42c0eee3345a5151c95..35867764cea5cdd1b38bf8f026e764365a0fdb6f 100644
--- a/theories/typing/type_sum.v
+++ b/theories/typing/type_sum.v
@@ -58,8 +58,8 @@ Section case.
lctx_lft_alive E L κ →
Forall2 (λ ty e,
typed_body E L C ((p +ₗ #1 ◁ &uniq{κ}ty) :: T) e ∨
- typed_body E L C ((p ◁ &uniq{κ}sum tyl) :: T) e) tyl el →
- typed_body E L C ((p ◁ &uniq{κ}sum tyl) :: T) (case: !p of el).
+ typed_body E L C ((p ◁ &uniq{κ}(sum tyl)) :: T) e) tyl el →
+ typed_body E L C ((p ◁ &uniq{κ}(sum tyl)) :: T) (case: !p of el).
Proof.
iIntros (Halive Hel tid) "#LFT #HE Hna HL HC HT". wp_bind p.
rewrite tctx_interp_cons. iDestruct "HT" as "[Hp HT]".
@@ -76,7 +76,7 @@ Section case.
wp_read. iApply wp_case; [lia|by rewrite Nat2Z.id|]. iNext.
iDestruct (ty.(ty_size_eq) with "Hown") as %EQlenvl'.
destruct Hety as [Hety|Hety].
- - iMod ("Hclose'" $! (shift_loc l 1 ↦∗: ty.(ty_own) tid)%I
+ - iMod ("Hclose'" $! ((l +ₗ 1) ↦∗: ty.(ty_own) tid)%I
with "[H↦i H↦vl''] [H↦vl' Hown]") as "[Hb Htok]".
{ iIntros "!>Hown". iDestruct "Hown" as (vl'2) "[H↦ Hown]".
iExists (#i::vl'2++vl''). iIntros "!>". iNext.
@@ -99,11 +99,11 @@ Section case.
Qed.
Lemma type_case_uniq E L C T T' p κ tyl el :
- tctx_extract_hasty E L p (&uniq{κ}sum tyl) T T' →
+ tctx_extract_hasty E L p (&uniq{κ}(sum tyl)) T T' →
lctx_lft_alive E L κ →
Forall2 (λ ty e,
typed_body E L C ((p +ₗ #1 ◁ &uniq{κ}ty) :: T') e ∨
- typed_body E L C ((p ◁ &uniq{κ}sum tyl) :: T') e) tyl el →
+ typed_body E L C ((p ◁ &uniq{κ}(sum tyl)) :: T') e) tyl el →
typed_body E L C T (case: !p of el).
Proof. unfold tctx_extract_hasty=>->. apply type_case_uniq'. Qed.
@@ -111,8 +111,8 @@ Section case.
lctx_lft_alive E L κ →
Forall2 (λ ty e,
typed_body E L C ((p +ₗ #1 ◁ &shr{κ}ty) :: T) e ∨
- typed_body E L C ((p ◁ &shr{κ}sum tyl) :: T) e) tyl el →
- typed_body E L C ((p ◁ &shr{κ}sum tyl) :: T) (case: !p of el).
+ typed_body E L C ((p ◁ &shr{κ}(sum tyl)) :: T) e) tyl el →
+ typed_body E L C ((p ◁ &shr{κ}(sum tyl)) :: T) (case: !p of el).
Proof.
iIntros (Halive Hel tid) "#LFT #HE Hna HL HC HT". wp_bind p.
rewrite tctx_interp_cons. iDestruct "HT" as "[Hp HT]".
@@ -132,7 +132,7 @@ Section case.
Qed.
Lemma type_case_shr E L C T p κ tyl el :
- p ◁ &shr{κ}sum tyl ∈ T →
+ p ◁ &shr{κ}(sum tyl) ∈ T →
lctx_lft_alive E L κ →
Forall2 (λ ty e, typed_body E L C ((p +ₗ #1 ◁ &shr{κ}ty) :: T) e) tyl el →
typed_body E L C T (case: !p of el).
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index 5a3a55433fa462651d1216023c52d1f8482f793a..baafe6bacb95cfc6bace8ff198720d1c357fa8da 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -12,7 +12,7 @@ Section uniq_bor.
{| ty_size := 1;
ty_own tid vl :=
match vl return _ with
- | [ #(LitLoc l) ] => &{κ} l ↦∗: ty.(ty_own) tid
+ | [ #(LitLoc l) ] => &{κ} (l ↦∗: ty.(ty_own) tid)
| _ => False
end;
ty_shr κ' tid l :=
@@ -96,18 +96,17 @@ Section uniq_bor.
Qed.
End uniq_bor.
-Notation "&uniq{ κ } ty" := (uniq_bor κ ty)
- (format "&uniq{ κ } ty", at level 20, right associativity) : lrust_type_scope.
+Notation "&uniq{ κ }" := (uniq_bor κ) (format "&uniq{ κ }") : lrust_type_scope.
Section typing.
Context `{typeG Σ}.
Lemma uniq_mono' E L κ1 κ2 ty1 ty2 :
lctx_lft_incl E L κ2 κ1 → eqtype E L ty1 ty2 →
- subtype E L (&uniq{κ1} ty1) (&uniq{κ2} ty2).
+ subtype E L (&uniq{κ1}ty1) (&uniq{κ2}ty2).
Proof. by intros; apply uniq_mono. Qed.
Lemma uniq_proper' E L κ ty1 ty2 :
- eqtype E L ty1 ty2 → eqtype E L (&uniq{κ} ty1) (&uniq{κ} ty2).
+ eqtype E L ty1 ty2 → eqtype E L (&uniq{κ}ty1) (&uniq{κ}ty2).
Proof. by intros; apply uniq_proper. Qed.
Lemma tctx_share E L p κ ty :
diff --git a/theories/typing/util.v b/theories/typing/util.v
index fec9517556eb9deb80d3bf19fc0573801bd822f8..1b907a641b09243d71b38c29790f423482ca339f 100644
--- a/theories/typing/util.v
+++ b/theories/typing/util.v
@@ -27,7 +27,7 @@ Section util.
Lemma delay_sharing_later N κ l ty tid :
lftE ⊆ N →
- lft_ctx -∗ &{κ} ▷ l ↦∗: ty_own ty tid ={N}=∗
+ lft_ctx -∗ &{κ}(▷ l ↦∗: ty_own ty tid) ={N}=∗
□ ∀ (F : coPset) (q : Qp),
⌜↑shrN ∪ lftE ⊆ F⌝ -∗ (q).[κ] ={F,F ∖ ↑shrN}▷=∗ ty.(ty_shr) κ tid l ∗ (q).[κ].
Proof.
@@ -49,7 +49,7 @@ Section util.
Lemma delay_sharing_nested N κ κ' κ'' l ty tid :
lftE ⊆ N →
- lft_ctx -∗ ▷ (κ'' ⊑ κ ⊓ κ') -∗ &{κ'} &{κ} l ↦∗: ty_own ty tid ={N}=∗
+ lft_ctx -∗ ▷ (κ'' ⊑ κ ⊓ κ') -∗ &{κ'}(&{κ}(l ↦∗: ty_own ty tid)) ={N}=∗
□ ∀ (F : coPset) (q : Qp),
⌜↑shrN ∪ lftE ⊆ F⌝ -∗ (q).[κ''] ={F,F ∖ ↑shrN}▷=∗ ty.(ty_shr) κ'' tid l ∗ (q).[κ''].
Proof.