diff --git a/opam b/opam
index 2c023bcbc23a9475dc7b6c7247fbcafaca429c54..ac688b5afd126f789fe01471cc7775f2611fc48f 100644
--- a/opam
+++ b/opam
@@ -11,5 +11,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/lrust'" ]
depends: [
- "coq-iris" { (= "dev.2017-10-29.1") | (= "dev") }
+ "coq-iris" { (= "dev.2017-11-02.0") | (= "dev") }
]
diff --git a/theories/lang/lang.v b/theories/lang/lang.v
index 5deef297cf567b1250dae28e4b6da2827dc673bb..bd1dc08479c9cf521c7baf0e7a6e87fe5344ea95 100644
--- a/theories/lang/lang.v
+++ b/theories/lang/lang.v
@@ -512,6 +512,9 @@ Proof. intros. apply is_closed_subst with []; set_solver. Qed.
Lemma is_closed_of_val X v : is_closed X (of_val v).
Proof. apply is_closed_weaken_nil. induction v; simpl; auto. Qed.
+Lemma is_closed_to_val X e v : to_val e = Some v → is_closed X e.
+Proof. intros <-%of_to_val. apply is_closed_of_val. Qed.
+
Lemma subst_is_closed X x es e :
is_closed X es → is_closed (x::X) e → is_closed X (subst x es e).
Proof.
diff --git a/theories/lang/lib/arc.v b/theories/lang/lib/arc.v
index 9755ee062493ec8c72947b8e2a57eb43b92290f6..88394b666c9cf6aa5322b6e4ab3077a1825d3ccf 100644
--- a/theories/lang/lib/arc.v
+++ b/theories/lang/lib/arc.v
@@ -269,7 +269,7 @@ Section arc.
iDestruct (arc_tok_auth_val with "Hâ— Hown") as %(?&strong'&?&?&[-> _]).
iDestruct "H" as (q) "(>#Hq & [HP1 HP1'] & Hl & Hw)". iDestruct "Hq" as %Hq.
destruct (decide (strong = strong')) as [->|?].
- - wp_apply (wp_cas_int_suc with "Hl"); first done. iIntros "Hl".
+ - wp_apply (wp_cas_int_suc with "Hl"). iIntros "Hl".
iMod (own_update with "Hâ—") as "[Hâ— Hown']".
{ apply auth_update_alloc, prod_local_update_1,
(op_local_update_discrete _ _ (Some (Cinl ((q/2)%Qp, 1%positive, None))))
@@ -282,7 +282,7 @@ Section arc.
{ iExists _. iFrame. iExists _. rewrite /= [xH â‹… _]comm_L. iFrame.
rewrite [(q / 2)%Qp â‹… _]comm frac_op' -[(_ + _)%Qp]assoc Qp_div_2 left_id_L. auto. }
iModIntro. wp_case. iApply "HΦ". iFrame.
- - wp_apply (wp_cas_int_fail with "Hl"); [done|congruence|]. iIntros "Hl".
+ - wp_apply (wp_cas_int_fail with "Hl"); [congruence|]. iIntros "Hl".
iMod ("Hclose2" with "Hown") as "HP". iModIntro.
iMod ("Hclose1" with "[-HP HΦ]") as "_".
{ iExists _. iFrame. iExists q. auto with iFrame. }
@@ -301,16 +301,16 @@ Section arc.
iDestruct "H" as (?) "(? & ? & ? & Hw)". destruct wlock.
{ iDestruct "Hw" as "(Hw & >%)". subst. wp_read.
iMod ("Hclose1" with "[-HP HΦ]") as "_"; first by iExists _; auto with iFrame.
- iModIntro. wp_let. wp_op=>[_|//]. wp_if. iApply ("IH" with "HP HΦ"). }
+ iModIntro. wp_let. wp_op. wp_if. iApply ("IH" with "HP HΦ"). }
wp_read. iMod ("Hclose1" with "[-HP HΦ]") as "_"; first by iExists _; auto with iFrame.
- iModIntro. wp_let. wp_op=>[//|_]. wp_if. wp_op. wp_op. wp_bind (CAS _ _ _).
+ iModIntro. wp_let. wp_op. wp_if. wp_op. wp_op. wp_bind (CAS _ _ _).
iInv N as (st) "[>Hâ— H]" "Hclose1".
iApply fupd_wp. iMod ("Hacc" with "HP") as (?) "[Hown Hclose2]".
iDestruct (arc_tok_auth_val with "Hâ— Hown") as %(?&?& wlock & weak' &[-> _]).
iMod ("Hclose2" with "Hown") as "HP". iModIntro.
iDestruct "H" as (q) "(>Heq & HP1 & Hl & Hl1)". iDestruct "Heq" as %Heq.
destruct (decide (weak = weak' ∧ wlock = None)) as [[<- ->]|Hw].
- - wp_apply (wp_cas_int_suc with "Hl1"); first done. iIntros "Hl1".
+ - wp_apply (wp_cas_int_suc with "Hl1"). iIntros "Hl1".
iMod (own_update with "Hâ—") as "[Hâ— Hown']".
{ by apply auth_update_alloc, prod_local_update_2,
(op_local_update_discrete _ _ (1%nat)). }
@@ -324,7 +324,7 @@ Section arc.
iIntros "Hl1". iMod ("Hclose1" with "[-HP HΦ]") as "_".
{ iExists _. auto with iFrame. }
iModIntro. wp_case. iApply ("IH" with "HP HΦ").
- + wp_apply (wp_cas_int_fail with "Hl1"); [done| |].
+ + wp_apply (wp_cas_int_fail with "Hl1").
{ contradict Hw. split=>//. apply SuccNat2Pos.inj. lia. }
iIntros "Hl1". iMod ("Hclose1" with "[-HP HΦ]") as "_".
{ iExists _. auto with iFrame. }
@@ -379,7 +379,7 @@ Section arc.
iMod ("Hclose" with "Hw") as "HP". iModIntro. wp_let. wp_op. wp_op.
wp_bind (CAS _ _ _). iMod ("Hproto" with "HP") as (w') "[H↦ Hclose]".
destruct (decide (w = w')) as [<-|].
- - wp_apply (wp_cas_int_suc with "H↦"); first done. iIntros "H↦".
+ - wp_apply (wp_cas_int_suc with "H↦"). iIntros "H↦".
iDestruct "Hclose" as "[Hclose _]". iMod ("Hclose" with "H↦"). iModIntro.
wp_case. by iApply "HΦ".
- wp_apply (wp_cas_int_fail with "H↦"); try done. iIntros "H↦".
@@ -421,11 +421,11 @@ Section arc.
iIntros "Hl". iMod ("Hclose2" with "Hown") as "$". iApply "Hclose1".
iExists _. auto with iFrame. }
iMod ("Hproto" with "HP") as (s) "[Hs [_ Hclose]]". wp_read.
- iMod ("Hclose" with "Hs") as "HP". iModIntro. wp_let. wp_op=>[->|?]; wp_if.
- - iApply ("HΦ" $! _ 1%Qp). auto.
+ iMod ("Hclose" with "Hs") as "HP". iModIntro. wp_let. wp_op; wp_if; case_bool_decide.
+ - iApply wp_value. iApply ("HΦ" $! _ 1%Qp). auto.
- wp_op. wp_bind (CAS _ _ _). iMod ("Hproto" with "HP") as (s') "[H↦ Hclose]".
destruct (decide (s = s')) as [<-|].
- + wp_apply (wp_cas_int_suc with "H↦"); first done. iIntros "H↦".
+ + wp_apply (wp_cas_int_suc with "H↦"). iIntros "H↦".
iDestruct "Hclose" as "[Hclose _]".
iMod ("Hclose" with "[//] H↦") as (q) "(?&?&?)". iModIntro.
wp_case. iApply "HΦ". iFrame.
@@ -476,9 +476,9 @@ Section arc.
iMod ("Hclose" with "Hw") as "Hown". iModIntro. wp_let. wp_op. wp_op.
wp_bind (CAS _ _ _).
iMod ("Hproto" with "Hown") as (w') "[Hw Hclose]". destruct (decide (w = w')) as [<-|?].
- - wp_apply (wp_cas_int_suc with "Hw"); first done. iIntros "Hw".
+ - wp_apply (wp_cas_int_suc with "Hw"). iIntros "Hw".
iDestruct "Hclose" as "[Hclose _]". iMod ("Hclose" with "Hw") as "HP2". iModIntro.
- wp_case. wp_op=>[->|?]; iApply "HΦ"=>//.
+ wp_case. wp_op; case_bool_decide; subst; iApply "HΦ"=>//.
by iDestruct "HP2" as "[%|$]".
- wp_apply (wp_cas_int_fail with "Hw"); try done. iIntros "Hw".
iDestruct "Hclose" as "[_ Hclose]". iMod ("Hclose" with "Hw") as "Hown".
@@ -514,7 +514,7 @@ Section arc.
iDestruct (arc_tok_auth_val with "Hâ— Hown") as %(q' & s' & wl & w &[-> Hqq']).
iDestruct "H" as (q'') "(>Hq'' & HP1' & Hs & Hw)". iDestruct "Hq''" as %Hq''.
destruct (decide (s = s')) as [<-|?].
- - wp_apply (wp_cas_int_suc with "Hs"); first done. iIntros "Hs".
+ - wp_apply (wp_cas_int_suc with "Hs"). iIntros "Hs".
destruct decide as [->|?].
+ destruct Hqq' as [<- ->].
iMod (own_update_2 with "Hâ— Hown") as "[Hâ— Hâ—¯]".
@@ -522,7 +522,7 @@ Section arc.
etrans; first apply cancel_local_update_unit, _.
by apply (op_local_update _ _ (Some (Cinr (Excl ())))). }
iMod ("Hclose" with "[Hâ— Hs Hw]") as "_"; first by iExists _; do 2 iFrame.
- iModIntro. wp_case. iApply wp_fupd. wp_op=>[_|//].
+ iModIntro. wp_case. iApply wp_fupd. wp_op.
iApply ("HΦ"). rewrite -{2}Hq''. iFrame. by iApply close_last_strong.
+ destruct Hqq' as [? ->].
rewrite -[in (_, _)](Pos.succ_pred s) // -[wl in Cinl (_, wl)]left_id
@@ -532,8 +532,8 @@ Section arc.
iMod ("Hclose" with "[- HΦ]") as "_".
{ iExists _. iFrame. iExists (q + q'')%Qp. iFrame. iSplit; last by destruct s.
iIntros "!> !%". rewrite assoc -Hq''. f_equal. apply comm, _. }
- iModIntro. wp_case. wp_op=>[|_]. by intros [=->]. by iApply "HΦ".
- - wp_apply (wp_cas_int_fail with "Hs"); [done|congruence|]. iIntros "Hs".
+ iModIntro. wp_case. wp_op; case_bool_decide; simplify_eq. by iApply "HΦ".
+ - wp_apply (wp_cas_int_fail with "Hs"); [congruence|]. iIntros "Hs".
iSpecialize ("IH" with "Hown HP1 HΦ").
iMod ("Hclose" with "[- IH]") as "_"; first by iExists _; auto with iFrame.
iModIntro. by wp_case.
@@ -549,14 +549,14 @@ Section arc.
iDestruct (arc_tok_auth_val with "Hâ— Hown") as %(q' & s & wl & w &[-> Hqq']).
iDestruct "H" as (q'') "(>Hq'' & HP1' & Hs & Hw)". iDestruct "Hq''" as %Hq''.
destruct (decide (s = xH)) as [->|?].
- - wp_apply (wp_cas_int_suc with "Hs"); first done. iIntros "Hs".
+ - wp_apply (wp_cas_int_suc with "Hs"). iIntros "Hs".
destruct Hqq' as [<- ->]. iMod (own_update_2 with "Hâ— Hown") as "[Hâ— Hâ—¯]".
{ apply auth_update, prod_local_update_1. rewrite -[x in (x, _)]right_id.
etrans; first apply cancel_local_update_unit, _.
by apply (op_local_update _ _ (Some (Cinr (Excl ())))). }
iMod ("Hclose" with "[Hâ— Hs Hw]") as "_"; first by iExists _; do 2 iFrame.
iApply ("HΦ" $! true). rewrite -{1}Hq''. iFrame. by iApply close_last_strong.
- - wp_apply (wp_cas_int_fail with "Hs"); [done|congruence|]. iIntros "Hs".
+ - wp_apply (wp_cas_int_fail with "Hs"); [congruence|]. iIntros "Hs".
iMod ("Hclose" with "[-Hown HP1 HΦ]") as "_"; first by iExists _; auto with iFrame.
iApply ("HΦ" $! false). by iFrame.
Qed.
@@ -577,7 +577,7 @@ Section arc.
iApply (wp_cas_int_fail with "Hw")=>//. iNext. iIntros "Hw".
iMod ("Hclose" with "[-HΦ Hown HP1]") as "_"; first by iExists _; eauto with iFrame.
iModIntro. wp_case. iApply "HΦ". iFrame.
- - iApply (wp_cas_int_fail with "Hw"); [done|lia|]. iNext. iIntros "Hw".
+ - iApply (wp_cas_int_fail with "Hw"); [lia|]. iNext. iIntros "Hw".
iMod ("Hclose" with "[-HΦ Hown HP1]") as "_"; first by iExists _; eauto with iFrame.
iModIntro. wp_case. iApply "HΦ". iFrame.
- iApply (wp_cas_int_suc with "Hw")=>//. iNext. iIntros "Hw".
@@ -595,7 +595,7 @@ Section arc.
simpl in Hlt. apply pos_included in Hlt.
iDestruct "H" as (?) "(? & ? & ? & ?)". wp_read.
iMod ("Hclose" with "[-HΦ H◯ HP1]") as "_"; first by iExists _; auto with iFrame.
- iModIntro. wp_let. wp_op; [lia|intros _]. wp_let. wp_op. wp_bind (_ <-ˢᶜ _)%E.
+ iModIntro. wp_let. wp_op; case_bool_decide; [lia|]. wp_let. wp_op. wp_bind (_ <-ˢᶜ _)%E.
iInv N as ([st w]) "[>Hâ— H]" "Hclose".
iDestruct (own_valid_2 with "Hâ— Hâ—¯") as
%[[[[=]|Hincl]%option_included _]%prod_included [Hval _]]%auth_valid_discrete_2.
@@ -617,7 +617,7 @@ Section arc.
{ apply auth_update_dealloc. rewrite -{1}[(_, 0%nat)]right_id.
apply cancel_local_update_unit, _. }
iMod ("Hclose" with "[Hâ—]") as "_"; first by iExists _; iFrame.
- iModIntro. wp_seq. wp_op=>[_|//]. wp_let. wp_op. wp_write. iApply "HΦ".
+ iModIntro. wp_seq. wp_op. wp_let. wp_op. wp_write. iApply "HΦ".
iDestruct "Hq" as %<-. iFrame.
Qed.
@@ -658,11 +658,11 @@ Section arc.
{ apply auth_update_dealloc, prod_local_update_1,
delete_option_local_update, _. }
iMod ("Hclose" with "[Hâ—]") as "_"; first by iExists _; iFrame. iModIntro.
- wp_op=>[_|//]. wp_if. wp_write. iApply ("HΦ" $! 0%fin). iFrame.
+ wp_op. wp_if. wp_write. iApply ("HΦ" $! 0%fin). iFrame.
+ iMod ("Hclose" with "[Hâ— Hl Hl1]") as "_"; first by iExists _; do 2 iFrame.
- iModIntro. wp_op; [lia|intros _]. wp_if. iApply ("HΦ" $! 1%fin). iFrame.
+ iModIntro. wp_op; case_bool_decide; [lia|]. wp_if. iApply ("HΦ" $! 1%fin). iFrame.
by iApply close_last_strong.
- - wp_apply (wp_cas_int_fail with "Hs"); [done|congruence|]. iIntros "Hs".
+ - wp_apply (wp_cas_int_fail with "Hs"); [congruence|]. iIntros "Hs".
iMod ("Hclose" with "[Hâ— Hs Hw HP1']") as "_"; first by iExists _; auto with iFrame.
iModIntro. wp_case. iApply ("HΦ" $! 2%fin). iFrame.
Qed.
diff --git a/theories/lang/lib/memcpy.v b/theories/lang/lib/memcpy.v
index 76a180b25c02016a328aff077705e85c966e592c..ecf05a0287ec6003686851ec868f8dccd14f9f0b 100644
--- a/theories/lang/lib/memcpy.v
+++ b/theories/lang/lib/memcpy.v
@@ -27,10 +27,10 @@ Lemma wp_memcpy `{lrustG Σ} E l1 l2 vl1 vl2 q (n : Z):
{{{ RET #☠; l1 ↦∗ vl2 ∗ l2 ↦∗{q} vl2 }}}.
Proof.
iIntros (Hvl1 Hvl2 Φ) "(Hl1 & Hl2) HΦ".
- iLöb as "IH" forall (n l1 l2 vl1 vl2 Hvl1 Hvl2). wp_rec. wp_op=> ?; wp_if.
+ iLöb as "IH" forall (n l1 l2 vl1 vl2 Hvl1 Hvl2). wp_rec. wp_op; case_bool_decide; wp_if.
- iApply "HΦ". assert (n = O) by lia; subst.
destruct vl1, vl2; try discriminate. by iFrame.
- - destruct vl1 as [|v1 vl1], vl2 as [|v2 vl2], n as [|n|]; try discriminate.
+ - destruct vl1 as [|v1 vl1], vl2 as [|v2 vl2], n as [|n|]; try (discriminate || omega).
revert Hvl1 Hvl2. intros [= Hvl1] [= Hvl2]; rewrite !heap_mapsto_vec_cons. subst n.
iDestruct "Hl1" as "[Hv1 Hl1]". iDestruct "Hl2" as "[Hv2 Hl2]".
Local Opaque Zminus.
diff --git a/theories/lang/lib/new_delete.v b/theories/lang/lib/new_delete.v
index 48957caade90fcd892e3a305b99cdac78bee7a57..da1d71e90b442861f50d6087cdf94253f4f5378d 100644
--- a/theories/lang/lib/new_delete.v
+++ b/theories/lang/lib/new_delete.v
@@ -22,10 +22,10 @@ Section specs.
{{{ l, RET LitV $ LitLoc l;
(†l…(Z.to_nat n) ∨ ⌜n = 0âŒ) ∗ l ↦∗ repeat (LitV LitPoison) (Z.to_nat n) }}}.
Proof.
- iIntros (? Φ) "_ HΦ". wp_lam. wp_op; intros ?.
+ iIntros (? Φ) "_ HΦ". wp_lam. wp_op; case_bool_decide.
- wp_if. assert (n = 0) as -> by lia. iApply "HΦ".
rewrite heap_mapsto_vec_nil. auto.
- - wp_if. wp_alloc l as "H↦" "H†". iApply "HΦ". subst sz.
+ - wp_if. wp_alloc l as "H↦" "H†". omega. iApply "HΦ". subst sz.
iFrame. auto.
Qed.
@@ -36,7 +36,7 @@ Section specs.
{{{ RET #☠; True }}}.
Proof.
iIntros (? Φ) "(H↦ & [H†|%]) HΦ";
- wp_lam; wp_op; intros ?; try lia; wp_if; try wp_free; by iApply "HΦ".
+ wp_lam; wp_op; case_bool_decide; try lia; wp_if; try wp_free; by iApply "HΦ".
Qed.
End specs.
diff --git a/theories/lang/lib/spawn.v b/theories/lang/lib/spawn.v
index 4090a683c277c215ee08beb1c55d7d43bbfaa709..81a8fbbe3a9dd7a34e3f26a7544559c633d35cda 100644
--- a/theories/lang/lib/spawn.v
+++ b/theories/lang/lib/spawn.v
@@ -105,12 +105,11 @@ Proof.
iDestruct "Hinv" as (b) "[>Hc Ho]". wp_read. destruct b; last first.
{ iMod ("Hclose" with "[Hc]").
- iNext. iRight. iExists _. iFrame.
- - iModIntro. iApply wp_if. iNext. iApply ("IH" with "Hj H†").
- auto. }
+ - iModIntro. wp_if. iApply ("IH" with "Hj H†"). auto. }
iDestruct "Ho" as (v) "(Hd & HΨ & Hf)".
iMod ("Hclose" with "[Hj Hf]") as "_".
{ iNext. iLeft. iFrame. }
- iModIntro. iApply wp_if. iNext. wp_op. wp_read. wp_let.
+ iModIntro. wp_if. wp_op. wp_read. wp_let.
iAssert (c ↦∗ [ #true; v])%I with "[Hc Hd]" as "Hc".
{ rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton. iFrame. }
wp_free; first done. iApply "HΦ". iApply "HΨ'". done.
diff --git a/theories/lang/lib/swap.v b/theories/lang/lib/swap.v
index 1d3f46fbecc2c68b26df2036220cfd275c4e5b8c..38d96b17f28d1a06de83a70cac958db553cb34e0 100644
--- a/theories/lang/lib/swap.v
+++ b/theories/lang/lib/swap.v
@@ -18,10 +18,11 @@ Lemma wp_swap `{lrustG Σ} E l1 l2 vl1 vl2 (n : Z):
{{{ RET #☠; l1 ↦∗ vl2 ∗ l2 ↦∗ vl1 }}}.
Proof.
iIntros (Hvl1 Hvl2 Φ) "(Hl1 & Hl2) HΦ".
- iLöb as "IH" forall (n l1 l2 vl1 vl2 Hvl1 Hvl2). wp_rec. wp_op=> ?; wp_if.
+ iLöb as "IH" forall (n l1 l2 vl1 vl2 Hvl1 Hvl2). wp_rec.
+ wp_op; case_bool_decide; wp_if.
- iApply "HΦ". assert (n = O) by lia; subst.
destruct vl1, vl2; try discriminate. by iFrame.
- - destruct vl1 as [|v1 vl1], vl2 as [|v2 vl2], n as [|n|]; try discriminate.
+ - destruct vl1 as [|v1 vl1], vl2 as [|v2 vl2], n as [|n|]; try (discriminate || omega).
revert Hvl1 Hvl2. intros [= Hvl1] [= Hvl2]; rewrite !heap_mapsto_vec_cons. subst n.
iDestruct "Hl1" as "[Hv1 Hl1]". iDestruct "Hl2" as "[Hv2 Hl2]".
Local Opaque Zminus.
diff --git a/theories/lang/lib/tests.v b/theories/lang/lib/tests.v
index 135f2fe7c2fe3e05db5ff831864a75b893f43093..8f414deb52aa61ec33e4e20b76385cd83febbc64 100644
--- a/theories/lang/lib/tests.v
+++ b/theories/lang/lib/tests.v
@@ -12,7 +12,7 @@ Section tests.
{{{ (b: bool), RET LitV (lit_of_bool b); (if b then ⌜l1 = l2⌠else ⌜l1 ≠l2âŒ) ∗
l1 ↦{q1} v1 ∗ l2 ↦{q2} v2 }}}.
Proof.
- iIntros (Φ) "[Hl1 Hl2] HΦ". wp_op; try (by eauto); [|];
- intros ?; iApply "HΦ"; by iFrame.
+ iIntros (Φ) "[Hl1 Hl2] HΦ". wp_op.
+ case_bool_decide; iApply "HΦ"; by iFrame.
Qed.
End tests.
diff --git a/theories/lang/lifting.v b/theories/lang/lifting.v
index d5b2a32c085ba1d0c0de51dbb719e672f3cfec01..7761b6edb39d01b6c4aeae016672e78bdbe6888e 100644
--- a/theories/lang/lifting.v
+++ b/theories/lang/lifting.v
@@ -5,8 +5,6 @@ From lrust.lang Require Import tactics.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
Import uPred.
-Local Hint Extern 0 (head_reducible _ _) => do_head_step eauto 2.
-Hint Constructors lit_neq lit_eq.
Class lrustG Σ := LRustG {
lrustG_invG : invG Σ;
@@ -25,9 +23,46 @@ Ltac inv_lit :=
| H : lit_neq _ ?x ?y |- _ => inversion H; clear H; simplify_eq/=
end.
+Ltac inv_bin_op_eval :=
+ repeat match goal with
+ | H : bin_op_eval _ ?c _ _ _ |- _ => is_constructor c; inversion H; clear H; simplify_eq/=
+ end.
+
+Local Hint Extern 0 (atomic _) => solve_atomic.
+Local Hint Extern 0 (head_reducible _ _) => eexists _, _, _; simpl.
+
+Local Hint Constructors head_step bin_op_eval lit_neq lit_eq.
+Local Hint Resolve alloc_fresh.
+Local Hint Resolve to_of_val.
+
+Class AsRec (e : expr) (f : binder) (xl : list binder) (erec : expr) :=
+ as_rec : e = Rec f xl erec.
+Instance AsRec_rec f xl e : AsRec (Rec f xl e) f xl e := eq_refl.
+Instance AsRec_rec_locked_val v f xl e :
+ AsRec (of_val v) f xl e → AsRec (of_val (locked v)) f xl e.
+Proof. by unlock. Qed.
+
+Class DoSubst (x : binder) (es : expr) (e er : expr) :=
+ do_subst : subst' x es e = er.
+Hint Extern 0 (DoSubst _ _ _ _) =>
+ rewrite /DoSubst; simpl_subst; reflexivity : typeclass_instances.
+
+Class DoSubstL (xl : list binder) (esl : list expr) (e er : expr) :=
+ do_subst_l : subst_l xl esl e = Some er.
+Instance do_subst_l_nil e : DoSubstL [] [] e e.
+Proof. done. Qed.
+Instance do_subst_l_cons x xl es esl e er er' :
+ DoSubstL xl esl e er' → DoSubst x es er' er →
+ DoSubstL (x :: xl) (es :: esl) e er.
+Proof. rewrite /DoSubstL /DoSubst /= => -> <- //. Qed.
+Instance do_subst_vec xl (vsl : vec val (length xl)) e :
+ DoSubstL xl (of_val <$> vec_to_list vsl) e (subst_v xl vsl e).
+Proof. by rewrite /DoSubstL subst_v_eq. Qed.
+
Section lifting.
Context `{lrustG Σ}.
Implicit Types P Q : iProp Σ.
+Implicit Types e : expr.
Implicit Types ef : option expr.
(** Bind. This bundles some arguments that wp_ectx_bind leaves as indices. *)
@@ -40,6 +75,68 @@ Lemma wp_bindi {E e} Ki Φ :
WP fill_item Ki e @ E {{ Φ }}.
Proof. exact: weakestpre.wp_bind. Qed.
+(** Base axioms for core primitives of the language: Stateless reductions *)
+Lemma wp_fork E e :
+ {{{ â–· WP e {{ _, True }} }}} Fork e @ E {{{ RET LitV LitPoison; True }}}.
+Proof.
+ iIntros (?) "?HΦ". iApply wp_lift_pure_det_head_step; eauto.
+ by intros; inv_head_step; eauto. iApply step_fupd_intro; first done. iNext.
+ rewrite big_sepL_singleton. iFrame. iApply wp_value. by iApply "HΦ".
+Qed.
+
+(** Pure reductions *)
+Local Ltac solve_exec_safe :=
+ intros; destruct_and?; subst; do 3 eexists; econstructor; simpl; eauto with omega.
+Local Ltac solve_exec_puredet :=
+ simpl; intros; destruct_and?; inv_head_step; inv_bin_op_eval; inv_lit; done.
+Local Ltac solve_pure_exec :=
+ apply det_head_step_pure_exec; [ solve_exec_safe | solve_exec_puredet ].
+
+Global Instance pure_rec e f xl erec erec' el :
+ AsRec e f xl erec →
+ TCForall AsVal el →
+ Closed (f :b: xl +b+ []) erec →
+ DoSubstL (f :: xl) (e :: el) erec erec' →
+ PureExec True (App e el) erec'.
+Proof. rewrite /AsRec /DoSubstL=> -> /TCForall_Forall ???. solve_pure_exec. Qed.
+
+Global Instance pure_le n1 n2 :
+ PureExec True (BinOp LeOp (Lit (LitInt n1)) (Lit (LitInt n2)))
+ (Lit (bool_decide (n1 ≤ n2))).
+Proof. solve_pure_exec. Qed.
+
+Global Instance pure_eq_int n1 n2 :
+ PureExec True (BinOp EqOp (Lit (LitInt n1)) (Lit (LitInt n2))) (Lit (bool_decide (n1 = n2))).
+Proof. case_bool_decide; solve_pure_exec. Qed.
+
+Global Instance pure_eq_loc_0_r l :
+ PureExec True (BinOp EqOp (Lit (LitLoc l)) (Lit (LitInt 0))) (Lit false).
+Proof. solve_pure_exec. Qed.
+
+Global Instance pure_eq_loc_0_l l :
+ PureExec True (BinOp EqOp (Lit (LitInt 0)) (Lit (LitLoc l))) (Lit false).
+Proof. solve_pure_exec. Qed.
+
+Global Instance pure_plus z1 z2 :
+ PureExec True (BinOp PlusOp (Lit $ LitInt z1) (Lit $ LitInt z2)) (Lit $ LitInt $ z1 + z2).
+Proof. solve_pure_exec. Qed.
+
+Global Instance pure_minus z1 z2 :
+ PureExec True (BinOp MinusOp (Lit $ LitInt z1) (Lit $ LitInt z2)) (Lit $ LitInt $ z1 - z2).
+Proof. solve_pure_exec. Qed.
+
+Global Instance pure_offset l z :
+ PureExec True (BinOp OffsetOp (Lit $ LitLoc l) (Lit $ LitInt z)) (Lit $ LitLoc $ l +â‚— z).
+Proof. solve_pure_exec. Qed.
+
+Global Instance pure_case i e el :
+ PureExec (0 ≤ i ∧ el !! (Z.to_nat i) = Some e) (Case (Lit $ LitInt i) el) e | 10.
+Proof. solve_pure_exec. Qed.
+
+Global Instance pure_if b e1 e2 :
+ PureExec True (If (Lit (lit_of_bool b)) e1 e2) (if b then e1 else e2) | 1.
+Proof. destruct b; solve_pure_exec. Qed.
+
(** Heap *)
Lemma wp_alloc E (n : Z) :
0 < n →
@@ -76,7 +173,7 @@ Proof.
iIntros (σ1) "Hσ". iDestruct (heap_read with "Hσ Hv") as %[n ?].
iModIntro; iSplit; first by eauto.
iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
- iModIntro; iSplit=> //. iFrame. rewrite to_of_val. iFrame. by iApply "HΦ".
+ iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
Lemma wp_read_na E l q v :
@@ -93,12 +190,12 @@ Proof.
iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1) "Hσ". iMod ("Hσclose" with "Hσ") as (n) "(% & Hσ & Hv)".
iModIntro; iSplit; first by eauto.
- iNext; iIntros (e2 σ2 efs Hstep) "!>"; inv_head_step. rewrite to_of_val /=.
+ iNext; iIntros (e2 σ2 efs Hstep) "!>"; inv_head_step.
iFrame "Hσ". iSplit; [done|]. by iApply "HΦ".
Qed.
Lemma wp_write_sc E l e v v' :
- to_val e = Some v →
+ IntoVal e v →
{{{ ▷ l ↦ v' }}} Write ScOrd (Lit $ LitLoc l) e @ E
{{{ RET LitV LitPoison; l ↦ v }}}.
Proof.
@@ -111,7 +208,7 @@ Proof.
Qed.
Lemma wp_write_na E l e v v' :
- to_val e = Some v →
+ IntoVal e v →
{{{ ▷ l ↦ v' }}} Write Na1Ord (Lit $ LitLoc l) e @ E
{{{ RET LitV LitPoison; l ↦ v }}}.
Proof.
@@ -130,7 +227,7 @@ Proof.
Qed.
Lemma wp_cas_int_fail E l q z1 e2 lit2 zl :
- to_val e2 = Some (LitV lit2) → z1 ≠zl →
+ IntoVal e2 (LitV lit2) → z1 ≠zl →
{{{ ▷ l ↦{q} LitV (LitInt zl) }}}
CAS (Lit $ LitLoc l) (Lit $ LitInt z1) e2 @ E
{{{ RET LitV $ LitInt 0; l ↦{q} LitV (LitInt zl) }}}.
@@ -144,7 +241,7 @@ Proof.
Qed.
Lemma wp_cas_suc E l lit1 e2 lit2 :
- to_val e2 = Some (LitV lit2) → lit1 ≠LitPoison →
+ IntoVal e2 (LitV lit2) → lit1 ≠LitPoison →
{{{ ▷ l ↦ LitV lit1 }}}
CAS (Lit $ LitLoc l) (Lit lit1) e2 @ E
{{{ RET LitV (LitInt 1); l ↦ LitV lit2 }}}.
@@ -159,21 +256,21 @@ Proof.
Qed.
Lemma wp_cas_int_suc E l z1 e2 lit2 :
- to_val e2 = Some (LitV lit2) →
+ IntoVal e2 (LitV lit2) →
{{{ ▷ l ↦ LitV (LitInt z1) }}}
CAS (Lit $ LitLoc l) (Lit $ LitInt z1) e2 @ E
{{{ RET LitV (LitInt 1); l ↦ LitV lit2 }}}.
Proof. intros ?. by apply wp_cas_suc. Qed.
Lemma wp_cas_loc_suc E l l1 e2 lit2 :
- to_val e2 = Some (LitV lit2) →
+ IntoVal e2 (LitV lit2) →
{{{ ▷ l ↦ LitV (LitLoc l1) }}}
CAS (Lit $ LitLoc l) (Lit $ LitLoc l1) e2 @ E
{{{ RET LitV (LitInt 1); l ↦ LitV lit2 }}}.
Proof. intros ?. by apply wp_cas_suc. Qed.
Lemma wp_cas_loc_fail E l q q' q1 l1 v1' e2 lit2 l' vl' :
- to_val e2 = Some (LitV lit2) → l1 ≠l' →
+ IntoVal e2 (LitV lit2) → l1 ≠l' →
{{{ ▷ l ↦{q} LitV (LitLoc l') ∗ ▷ l' ↦{q'} vl' ∗ ▷ l1 ↦{q1} v1' }}}
CAS (Lit $ LitLoc l) (Lit $ LitLoc l1) e2 @ E
{{{ RET LitV (LitInt 0);
@@ -190,7 +287,7 @@ Proof.
Qed.
Lemma wp_cas_loc_nondet E l l1 e2 l2 ll :
- to_val e2 = Some (LitV $ LitLoc l2) →
+ IntoVal e2 (LitV $ LitLoc l2) →
{{{ ▷ l ↦ LitV (LitLoc ll) }}}
CAS (Lit $ LitLoc l) (Lit $ LitLoc l1) e2 @ E
{{{ b, RET LitV (lit_of_bool b);
@@ -208,87 +305,18 @@ Proof.
iModIntro; iSplit; [done|]. iApply "HΦ"; iFrame.
Qed.
-(** Base axioms for core primitives of the language: Stateless reductions *)
-Lemma wp_fork E e :
- {{{ â–· WP e {{ _, True }} }}} Fork e @ E {{{ RET LitV LitPoison; True }}}.
-Proof.
- iIntros (?) "?HΦ". iApply wp_lift_pure_det_head_step; eauto.
- by intros; inv_head_step; eauto. iApply step_fupd_intro; first done. iNext.
- rewrite big_sepL_singleton. iFrame. iApply wp_value. by iApply "HΦ".
-Qed.
-
-Lemma wp_rec_step_fupd E E' e f xl erec erec' el Φ :
- e = Rec f xl erec →
- Forall (λ ei, is_Some (to_val ei)) el →
- Closed (f :b: xl +b+ []) erec →
- subst_l (f::xl) (e::el) erec = Some erec' →
- (|={E,E'}▷=> WP erec' @ E {{ Φ }}) -∗ WP App e el @ E {{ Φ }}.
-Proof.
- iIntros (-> ???) "H". iApply wp_lift_pure_det_head_step_no_fork; subst; eauto.
- by intros; inv_head_step; eauto.
-Qed.
-
-Lemma wp_rec E e f xl erec erec' el Φ :
- e = Rec f xl erec →
- Forall (λ ei, is_Some (to_val ei)) el →
- Closed (f :b: xl +b+ []) erec →
- subst_l (f::xl) (e::el) erec = Some erec' →
- ▷ WP erec' @ E {{ Φ }} -∗ WP App e el @ E {{ Φ }}.
-Proof.
- iIntros (-> ???) "?". iApply wp_rec_step_fupd; [done..|].
- iApply step_fupd_intro; done.
-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
- {{{ l'' σ, RET LitV l''; ⌜bin_op_eval σ op l1 l2 l''⌠}}}.
-Proof.
- iIntros (? Φ) "_ HΦ". iApply wp_lift_pure_head_step; eauto.
- { intros. by inv_head_step. }
- iApply step_fupd_intro; first done. iNext. iIntros (e2 efs σ Hs).
- inv_head_step; rewrite right_id.
- rewrite -wp_value. iApply "HΦ". eauto.
-Qed.
-
-Lemma wp_le E (n1 n2 : Z) P Φ :
- (n1 ≤ n2 → P -∗ ▷ Φ (LitV $ true)) →
- (n2 < n1 → P -∗ ▷ Φ (LitV false)) →
- P -∗ WP BinOp LeOp (Lit (LitInt n1)) (Lit (LitInt n2)) @ E {{ Φ }}.
-Proof.
- iIntros (Hl Hg) "HP".
- destruct (bool_decide_reflect (n1 ≤ n2)); [rewrite Hl //|rewrite Hg; last omega];
- clear Hl Hg; (iApply wp_bin_op_pure; first by econstructor); try done; iNext; iIntros (?? Heval);
- inversion_clear Heval; [rewrite bool_decide_true //|rewrite bool_decide_false //].
-Qed.
-
-Lemma wp_eq_int E (n1 n2 : Z) P Φ :
- (n1 = n2 → P -∗ ▷ Φ (LitV true)) →
- (n1 ≠n2 → P -∗ ▷ Φ (LitV false)) →
- P -∗ WP BinOp EqOp (Lit (LitInt n1)) (Lit (LitInt n2)) @ E {{ Φ }}.
-Proof.
- iIntros (Heq Hne) "HP".
- destruct (bool_decide_reflect (n1 = n2)); [rewrite Heq //|rewrite Hne //];
- clear Hne Heq; iApply wp_bin_op_pure; subst; try done.
- - intros. apply BinOpEqTrue. constructor.
- - iNext; iIntros (?? Heval). by inversion_clear Heval; inv_lit.
- - intros. apply BinOpEqFalse. by constructor.
- - iNext; iIntros (?? Heval). by inversion_clear Heval; inv_lit.
-Qed.
-
-Lemma wp_eq_loc E (l1 : loc) (l2: loc) P Φ :
- (P -∗ ∃ q v, ▷ l1 ↦{q} v) →
- (P -∗ ∃ q v, ▷ l2 ↦{q} v) →
- (l1 = l2 → P -∗ ▷ Φ (LitV true)) →
- (l1 ≠l2 → P -∗ ▷ Φ (LitV false)) →
+Lemma wp_eq_loc E (l1 : loc) (l2: loc) q1 q2 v1 v2 P Φ :
+ (P -∗ ▷ l1 ↦{q1} v1) →
+ (P -∗ ▷ l2 ↦{q2} v2) →
+ (P -∗ ▷ Φ (LitV (bool_decide (l1 = l2)))) →
P -∗ WP BinOp EqOp (Lit (LitLoc l1)) (Lit (LitLoc l2)) @ E {{ Φ }}.
Proof.
- iIntros (Hl1 Hl2 Heq Hne) "HP".
- destruct (bool_decide_reflect (l1 = l2)).
- - rewrite Heq // {Heq Hne}. iApply wp_bin_op_pure; subst; try done.
- + intros. apply BinOpEqTrue. constructor.
- + iNext. iIntros (?? Heval). by inversion_clear Heval; inv_lit.
- - clear Heq. iApply wp_lift_atomic_head_step_no_fork; subst=>//.
+ iIntros (Hl1 Hl2 Hpost) "HP".
+ destruct (bool_decide_reflect (l1 = l2)) as [->|].
+ - iApply wp_lift_pure_det_head_step_no_fork';
+ [done|solve_exec_safe|solve_exec_puredet|].
+ iApply wp_value. by iApply Hpost.
+ - iApply wp_lift_atomic_head_step_no_fork; subst=>//.
iIntros (σ1) "Hσ1". iModIntro. inv_head_step.
iSplitR.
{ iPureIntro. eexists _, _, _. constructor. apply BinOpEqFalse. by auto. }
@@ -296,85 +324,23 @@ Proof.
▷ but also have the ↦s. *)
iAssert ((▷ ∃ q v, l1 ↦{q} v) ∧ (▷ ∃ q v, l2 ↦{q} v) ∧ ▷ Φ (LitV false))%I with "[HP]" as "HP".
{ iSplit; last iSplit.
- - iDestruct (Hl1 with "HP") as (??) "?". iNext. eauto.
- - iDestruct (Hl2 with "HP") as (??) "?". iNext. eauto.
- - by iApply Hne. }
- clear Hne Hl1 Hl2. iNext.
- iIntros (e2 σ2 efs Hs) "!>".
- inv_head_step. iSplitR=>//.
- match goal with [ H : bin_op_eval _ _ _ _ _ |- _ ] => inversion H end;
- inv_lit=>//.
- * iExFalso. iDestruct "HP" as "[Hl1 _]".
+ + iExists _, _. by iApply Hl1.
+ + iExists _, _. by iApply Hl2.
+ + by iApply Hpost. }
+ clear Hl1 Hl2. iNext. iIntros (e2 σ2 efs Hs) "!>".
+ inv_head_step. iSplitR=>//. inv_bin_op_eval; inv_lit.
+ + iExFalso. iDestruct "HP" as "[Hl1 _]".
iDestruct "Hl1" as (??) "Hl1".
- iDestruct (heap_read σ2 with "Hσ1 Hl1") as (n') "%".
- simplify_eq.
- * iExFalso. iDestruct "HP" as "[_ [Hl2 _]]".
+ iDestruct (heap_read σ2 with "Hσ1 Hl1") as %[??]; simplify_eq.
+ + iExFalso. iDestruct "HP" as "[_ [Hl2 _]]".
iDestruct "Hl2" as (??) "Hl2".
- iDestruct (heap_read σ2 with "Hσ1 Hl2") as (n') "%".
- simplify_eq.
- * iDestruct "HP" as "[_ [_ $]]". done.
-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; try done.
- - 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; try done.
- - 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 $ l +ₗ z) -∗
- WP BinOp OffsetOp (Lit $ LitLoc l) (Lit $ LitInt z) @ E {{ Φ }}.
-Proof.
- iIntros "HP". iApply wp_bin_op_pure; first (by econstructor); first done.
- iNext. iIntros (?? Heval). inversion_clear Heval. done.
+ iDestruct (heap_read σ2 with "Hσ1 Hl2") as %[??]; simplify_eq.
+ + iDestruct "HP" as "[_ [_ $]]". done.
Qed.
-Lemma wp_plus E z1 z2 Φ :
- ▷ Φ (LitV $ LitInt $ z1 + z2) -∗
- WP BinOp PlusOp (Lit $ LitInt z1) (Lit $ LitInt z2) @ E {{ Φ }}.
-Proof.
- iIntros "HP". iApply wp_bin_op_pure; first (by econstructor); first done.
- iNext. iIntros (?? Heval). inversion_clear Heval. done.
-Qed.
-
-Lemma wp_minus E z1 z2 Φ :
- ▷ Φ (LitV $ LitInt $ z1 - z2) -∗
- WP BinOp MinusOp (Lit $ LitInt z1) (Lit $ LitInt z2) @ E {{ Φ }}.
-Proof.
- iIntros "HP". iApply (wp_bin_op_pure with "[//]"); first by econstructor.
- iNext. iIntros (?? Heval). inversion_clear Heval. done.
-Qed.
-
-Lemma wp_case E i e el Φ :
- 0 ≤ i →
- el !! (Z.to_nat i) = Some e →
- ▷ WP e @ E {{ Φ }} -∗ WP Case (Lit $ LitInt i) el @ E {{ Φ }}.
-Proof.
- iIntros (??) "?". iApply wp_lift_pure_det_head_step_no_fork'; eauto.
- by intros; inv_head_step; eauto.
-Qed.
-
-Lemma wp_if E (b : bool) e1 e2 Φ :
- (if b then ▷ WP e1 @ E {{ Φ }} else ▷ WP e2 @ E {{ Φ }})%I -∗
- WP If (Lit b) e1 e2 @ E {{ Φ }}.
-Proof. iIntros "?". by destruct b; iApply wp_case. Qed.
-
-
(** Proof rules for working on the n-ary argument list. *)
-Lemma wp_app_ind E f (el : list expr) (Ql : vec (val → iProp Σ) (length el)) vs Φ:
- is_Some (to_val f) →
+Lemma wp_app_ind E f (el : list expr) (Ql : vec (val → iProp Σ) (length el)) vs Φ :
+ AsVal f →
([∗ list] eQ ∈ zip el Ql, WP eQ.1 @ E {{ eQ.2 }}) -∗
(∀ vl : vec val (length el), ([∗ list] vQ ∈ zip vl Ql, vQ.2 $ vQ.1) -∗
WP App f (of_val <$> vs ++ vl) @ E {{ Φ }}) -∗
@@ -393,7 +359,7 @@ Proof.
Qed.
Lemma wp_app_vec E f el (Ql : vec (val → iProp Σ) (length el)) Φ :
- is_Some (to_val f) →
+ AsVal f →
([∗ list] eQ ∈ zip el Ql, WP eQ.1 @ E {{ eQ.2 }}) -∗
(∀ vl : vec val (length el), ([∗ list] vQ ∈ zip vl Ql, vQ.2 $ vQ.1) -∗
WP App f (of_val <$> (vl : list val)) @ E {{ Φ }}) -∗
@@ -401,7 +367,7 @@ Lemma wp_app_vec E f el (Ql : vec (val → iProp Σ) (length el)) Φ :
Proof. iIntros (Hf). by iApply (wp_app_ind _ _ _ _ []). Qed.
Lemma wp_app (Ql : list (val → iProp Σ)) E f el Φ :
- length Ql = length el → is_Some (to_val f) →
+ length Ql = length el → AsVal f →
([∗ list] eQ ∈ zip el Ql, WP eQ.1 @ E {{ eQ.2 }}) -∗
(∀ vl : list val, ⌜length vl = length el⌠-∗
([∗ list] k ↦ vQ ∈ zip vl Ql, vQ.2 $ vQ.1) -∗
@@ -410,42 +376,7 @@ Lemma wp_app (Ql : list (val → iProp Σ)) E f el Φ :
Proof.
iIntros (Hlen Hf) "Hel HΦ". rewrite -(vec_to_list_of_list Ql).
generalize (list_to_vec Ql). rewrite Hlen. clear Hlen Ql=>Ql.
- iApply (wp_app_vec with "Hel"); first done. iIntros (vl) "Hvl".
+ iApply (wp_app_vec with "Hel"). iIntros (vl) "Hvl".
iApply ("HΦ" with "[%] Hvl"). by rewrite vec_to_list_length.
Qed.
-
-
-(** Proof rules for the lam-related sugar *)
-Lemma wp_lam E xl e eb e' el Φ :
- e = Lam xl eb →
- Forall (λ ei, is_Some (to_val ei)) el →
- Closed (xl +b+ []) eb →
- subst_l xl el eb = Some e' →
- ▷ WP e' @ E {{ Φ }} -∗ WP App e el @ E {{ Φ }}.
-Proof.
- iIntros (-> ???) "?". iApply (wp_rec _ _ BAnon)=>//.
- by rewrite /= option_fmap_id.
-Qed.
-
-Lemma wp_let E x e1 e2 v Φ :
- to_val e1 = Some v →
- Closed (x :b: []) e2 →
- ▷ WP subst' x e1 e2 @ E {{ Φ }} -∗ WP Let x e1 e2 @ E {{ Φ }}.
-Proof. eauto using wp_lam. Qed.
-
-Lemma wp_let' E x e1 e2 v Φ :
- to_val e1 = Some v →
- Closed (x :b: []) e2 →
- ▷ WP subst' x (of_val v) e2 @ E {{ Φ }} -∗ WP Let x e1 e2 @ E {{ Φ }}.
-Proof. intros ?. rewrite (of_to_val e1) //. eauto using wp_let. Qed.
-
-Lemma wp_seq E e1 e2 v Φ :
- to_val e1 = Some v →
- Closed [] e2 →
- ▷ WP e2 @ E {{ Φ }} -∗ WP Seq e1 e2 @ E {{ Φ }}.
-Proof. iIntros (??) "?". by iApply (wp_let _ BAnon). Qed.
-
-Lemma wp_skip E Φ : ▷ Φ (LitV LitPoison) -∗ WP Skip @ E {{ Φ }}.
-Proof. iIntros. iApply wp_seq. done. iNext. by iApply wp_value. Qed.
-
End lifting.
diff --git a/theories/lang/proofmode.v b/theories/lang/proofmode.v
index b45f4217ca91c0dd5867860701f183d1c09f948e..e757c6dfb918da455f4c64e8a0f447fa4718a822 100644
--- a/theories/lang/proofmode.v
+++ b/theories/lang/proofmode.v
@@ -3,142 +3,87 @@ From iris.program_logic Require Export weakestpre.
From iris.proofmode Require Import coq_tactics.
From iris.proofmode Require Export tactics.
From lrust.lang Require Export tactics lifting.
+From iris.program_logic Require Import lifting.
Set Default Proof Using "Type".
Import uPred.
-(** wp-specific helper tactics *)
-Ltac wp_bind_core K :=
- lazymatch eval hnf in K with
- | [] => idtac
- | _ => etrans; [|fast_by apply (wp_bind K)]; simpl
- end.
+Lemma tac_wp_value `{lrustG Σ} Δ E Φ e v :
+ IntoVal e v →
+ envs_entails Δ (Φ v) → envs_entails Δ (WP e @ E {{ Φ }}).
+Proof. rewrite /envs_entails=> ? ->. by apply wp_value. Qed.
-(* Solves side-conditions generated by the wp tactics *)
-Ltac wp_done :=
- match goal with
- | |- Closed _ _ => solve_closed
- | |- is_Some (to_val _) => solve_to_val
- | |- to_val _ = Some _ => solve_to_val
- | |- language.to_val _ = Some _ => solve_to_val
- | |- Forall _ [] => fast_by apply List.Forall_nil
- | |- Forall _ (_ :: _) => apply List.Forall_cons; wp_done
- | |- _ ≤ _ => lia
- | _ => fast_done
- end.
-
-Ltac wp_value_head := etrans; [|eapply wp_value; apply _]; simpl.
-
-Ltac wp_seq_head :=
- lazymatch goal with
- | |- _ ⊢ wp ?E (Seq _ _) ?Q =>
- etrans; [|eapply wp_seq; wp_done]; iNext
- end.
+Ltac wp_value_head := eapply tac_wp_value; [apply _|lazy beta].
-Ltac wp_finish := intros_revert ltac:(
- rewrite /= ?to_of_val;
- try iNext;
- repeat lazymatch goal with
- | |- _ ⊢ wp ?E (Seq _ _) ?Q =>
- etrans; [|eapply wp_seq; wp_done]; iNext
- | |- _ ⊢ wp ?E _ ?Q => wp_value_head
- end).
+Lemma tac_wp_pure `{lrustG Σ} K Δ Δ' E e1 e2 φ Φ :
+ PureExec φ e1 e2 →
+ φ →
+ IntoLaterNEnvs 1 Δ Δ' →
+ envs_entails Δ' (WP fill K e2 @ E {{ Φ }}) →
+ envs_entails Δ (WP fill K e1 @ E {{ Φ }}).
+Proof.
+ rewrite /envs_entails=> ??? HΔ'. rewrite into_laterN_env_sound /=.
+ rewrite -lifting.wp_bind HΔ' -wp_pure_step_later //.
+ by rewrite -ectx_lifting.wp_ectx_bind_inv.
+Qed.
-Tactic Notation "wp_value" :=
+Tactic Notation "wp_pure" open_constr(efoc) :=
iStartProof;
lazymatch goal with
- | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
- wp_bind_core K; wp_value_head) || fail "wp_value: cannot find value in" e
- | _ => fail "wp_value: not a wp"
+ | |- envs_entails _ (wp ?E ?e ?Q) => reshape_expr e ltac:(fun K e' =>
+ unify e' efoc;
+ eapply (tac_wp_pure K);
+ [simpl; apply _ (* PureExec *)
+ |try done (* The pure condition for PureExec *)
+ |apply _ (* IntoLaters *)
+ |simpl_subst; try wp_value_head (* new goal *)])
+ || fail "wp_pure: cannot find" efoc "in" e "or" efoc "is not a reduct"
+ | _ => fail "wp_pure: not a 'wp'"
end.
-Lemma of_val_unlock v e : of_val v = e → of_val (locked v) = e.
-Proof. by unlock. Qed.
-
-(* Applied to goals that are equalities of expressions. Will try to unlock the
- LHS once if necessary, to get rid of the lock added by the syntactic sugar. *)
-Ltac solve_of_val_unlock := try apply of_val_unlock; reflexivity.
-
-Tactic Notation "wp_rec" :=
- iStartProof;
- lazymatch goal with
- | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
- match eval hnf in e' with App ?e1 _ =>
-(* hnf does not reduce through an of_val *)
-(* match eval hnf in e1 with Rec _ _ _ => *)
- wp_bind_core K; etrans;
- [|eapply wp_rec; [solve_of_val_unlock|wp_done..]]; simpl_subst; wp_finish
-(* end *) end) || fail "wp_rec: cannot find 'Rec' in" e
- | _ => fail "wp_rec: not a 'wp'"
- end.
+Lemma tac_wp_eq_loc `{lrustG Σ} K Δ Δ' E i1 i2 l1 l2 q1 q2 v1 v2 Φ :
+ IntoLaterNEnvs 1 Δ Δ' →
+ envs_lookup i1 Δ' = Some (false, l1 ↦{q1} v1)%I →
+ envs_lookup i2 Δ' = Some (false, l2 ↦{q2} v2)%I →
+ envs_entails Δ' (WP fill K (Lit (bool_decide (l1 = l2))) @ E {{ Φ }}) →
+ envs_entails Δ (WP fill K (BinOp EqOp (Lit (LitLoc l1)) (Lit (LitLoc l2))) @ E {{ Φ }}).
+Proof.
+ rewrite /envs_entails=> ? /envs_lookup_sound'. rewrite sep_elim_l=> ?.
+ move /envs_lookup_sound'; rewrite sep_elim_l=> ? HΔ. rewrite -wp_bind.
+ rewrite into_laterN_env_sound /=. eapply wp_eq_loc; eauto using later_mono.
+Qed.
-Tactic Notation "wp_lam" :=
+Tactic Notation "wp_eq_loc" :=
iStartProof;
lazymatch goal with
- | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
- match eval hnf in e' with App ?e1 _ =>
-(* match eval hnf in e1 with Rec BAnon _ _ => *)
- wp_bind_core K; etrans;
- [|eapply wp_lam; [solve_of_val_unlock|wp_done..]]; simpl_subst; wp_finish
-(* end *) end) || fail "wp_lam: cannot find 'Lam' in" e
- | _ => fail "wp_lam: not a 'wp'"
+ | |- envs_entails _ (wp ?E ?e ?Q) =>
+ reshape_expr e ltac:(fun K e' => eapply (tac_wp_eq_loc K));
+ [apply _|iAssumptionCore|iAssumptionCore|simpl; try wp_value_head]
+ | _ => fail "wp_pure: not a 'wp'"
end.
+Tactic Notation "wp_rec" := wp_pure (App _ _).
+Tactic Notation "wp_lam" := wp_rec.
Tactic Notation "wp_let" := wp_lam.
Tactic Notation "wp_seq" := wp_let.
+Tactic Notation "wp_op" := wp_pure (BinOp _ _ _) || wp_eq_loc.
+Tactic Notation "wp_if" := wp_pure (If _ _ _).
+Tactic Notation "wp_case" := wp_pure (Case _ _); try wp_value_head.
-Tactic Notation "wp_op" :=
- iStartProof;
- lazymatch goal with
- | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
- match eval hnf in e' with
- | BinOp LeOp _ _ => wp_bind_core K; apply wp_le; wp_finish
- | BinOp EqOp (Lit (LitInt _)) (Lit (LitInt _)) =>
- 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 _ _ =>
- wp_bind_core K; etrans; [|eapply wp_plus; try fast_done]; wp_finish
- | BinOp MinusOp _ _ =>
- wp_bind_core K; etrans; [|eapply wp_minus; try fast_done]; wp_finish
- end) || fail "wp_op: cannot find 'BinOp' in" e
- | _ => fail "wp_op: not a 'wp'"
- end.
-
-Tactic Notation "wp_if" :=
- iStartProof;
- lazymatch goal with
- | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
- match eval hnf in e' with
- | If _ _ _ =>
- wp_bind_core K;
- etrans; [|eapply wp_if]; wp_finish
- end) || fail "wp_if: cannot find 'If' in" e
- | _ => fail "wp_if: not a 'wp'"
- end.
+Lemma tac_wp_bind `{lrustG Σ} K Δ E Φ e :
+ envs_entails Δ (WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }})%I →
+ envs_entails Δ (WP fill K e @ E {{ Φ }}).
+Proof. rewrite /envs_entails=> ->. by apply wp_bind. Qed.
-Tactic Notation "wp_case" :=
- iStartProof;
- lazymatch goal with
- | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
- match eval hnf in e' with
- | Case _ _ =>
- wp_bind_core K;
- etrans; [|eapply wp_case; wp_done];
- simpl_subst; wp_finish
- end) || fail "wp_case: cannot find 'Case' in" e
- | _ => fail "wp_case: not a 'wp'"
+Ltac wp_bind_core K :=
+ lazymatch eval hnf in K with
+ | [] => idtac
+ | _ => apply (tac_wp_bind K); simpl
end.
Tactic Notation "wp_bind" open_constr(efoc) :=
iStartProof;
lazymatch goal with
- | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
+ | |- envs_entails _ (wp ?E ?e ?Q) => reshape_expr e ltac:(fun K e' =>
match e' with
| efoc => unify e' efoc; wp_bind_core K
end) || fail "wp_bind: cannot find" efoc "in" e
@@ -151,25 +96,26 @@ Implicit Types P Q : iProp Σ.
Implicit Types Φ : val → iProp Σ.
Implicit Types Δ : envs (iResUR Σ).
-Lemma tac_wp_alloc Δ Δ' E j1 j2 n Φ :
+Lemma tac_wp_alloc K Δ Δ' E j1 j2 n Φ :
0 < n →
IntoLaterNEnvs 1 Δ Δ' →
(∀ l (sz: nat), n = sz → ∃ Δ'',
envs_app false (Esnoc (Esnoc Enil j1 (l ↦∗ repeat (LitV LitPoison) sz)) j2 (†l…sz)) Δ'
= Some Δ'' ∧
- (Δ'' ⊢ Φ (LitV $ LitLoc l))) →
- Δ ⊢ WP Alloc (Lit $ LitInt n) @ E {{ Φ }}.
+ envs_entails Δ'' (WP fill K (Lit $ LitLoc l) @ E {{ Φ }})) →
+ envs_entails Δ (WP fill K (Alloc (Lit $ LitInt n)) @ E {{ Φ }}).
Proof.
- intros ?? HΔ. rewrite -wp_fupd. eapply wand_apply; first exact:wp_alloc.
- rewrite -and_sep_l. apply and_intro; first done.
+ rewrite /envs_entails=> ?? HΔ. rewrite -wp_bind.
+ eapply wand_apply; first exact:wp_alloc.
+ rewrite -and_sep_l. apply and_intro; first auto with I.
rewrite into_laterN_env_sound; apply later_mono, forall_intro=> l.
apply forall_intro=>sz. apply wand_intro_l. rewrite -assoc.
apply pure_elim_sep_l=> Hn. apply wand_elim_r'.
destruct (HΔ l sz) as (Δ''&?&HΔ'); first done.
- rewrite envs_app_sound //; simpl. by rewrite right_id HΔ' -fupd_intro.
+ rewrite envs_app_sound //; simpl. by rewrite right_id HΔ'.
Qed.
-Lemma tac_wp_free Δ Δ' Δ'' Δ''' E i1 i2 vl (n : Z) (n' : nat) l Φ :
+Lemma tac_wp_free K Δ Δ' Δ'' Δ''' E i1 i2 vl (n : Z) (n' : nat) l Φ :
n = length vl →
IntoLaterNEnvs 1 Δ Δ' →
envs_lookup i1 Δ' = Some (false, l ↦∗ vl)%I →
@@ -177,83 +123,84 @@ Lemma tac_wp_free Δ Δ' Δ'' Δ''' E i1 i2 vl (n : Z) (n' : nat) l Φ :
envs_lookup i2 Δ'' = Some (false, †l…n')%I →
envs_delete i2 false Δ'' = Δ''' →
n' = length vl →
- (Δ''' ⊢ Φ (LitV LitPoison)) →
- Δ ⊢ WP Free (Lit $ LitInt n) (Lit $ LitLoc l) @ E {{ Φ }}.
+ envs_entails Δ''' (WP fill K (Lit LitPoison) @ E {{ Φ }}) →
+ envs_entails Δ (WP fill K (Free (Lit $ LitInt n) (Lit $ LitLoc l)) @ E {{ Φ }}).
Proof.
- intros -> ?? <- ? <- -> HΔ. rewrite -wp_fupd.
+ rewrite /envs_entails; intros -> ?? <- ? <- -> HΔ. rewrite -wp_bind.
eapply wand_apply; first exact:wp_free; simpl.
rewrite into_laterN_env_sound -!later_sep; apply later_mono.
- do 2 (rewrite envs_lookup_sound' //).
- by rewrite HΔ wand_True -fupd_intro -assoc.
+ do 2 (rewrite envs_lookup_sound' //). by rewrite HΔ wand_True -assoc.
Qed.
-Lemma tac_wp_read Δ Δ' E i l q v o Φ :
+Lemma tac_wp_read K Δ Δ' E i l q v o Φ :
o = Na1Ord ∨ o = ScOrd →
IntoLaterNEnvs 1 Δ Δ' →
envs_lookup i Δ' = Some (false, l ↦{q} v)%I →
- (Δ' ⊢ Φ v) →
- Δ ⊢ WP Read o (Lit $ LitLoc l) @ E {{ Φ }}.
+ envs_entails Δ' (WP fill K (of_val v) @ E {{ Φ }}) →
+ envs_entails Δ (WP fill K (Read o (Lit $ LitLoc l)) @ E {{ Φ }}).
Proof.
- intros [->| ->] ???.
- - rewrite -wp_fupd. eapply wand_apply; first exact:wp_read_na.
+ rewrite /envs_entails; intros [->| ->] ???.
+ - rewrite -wp_bind. eapply wand_apply; first exact:wp_read_na.
rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
- rewrite -fupd_intro. by apply later_mono, sep_mono_r, wand_mono.
- - rewrite -wp_fupd. eapply wand_apply; first exact:wp_read_sc.
+ by apply later_mono, sep_mono_r, wand_mono.
+ - rewrite -wp_bind. eapply wand_apply; first exact:wp_read_sc.
rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
- rewrite -fupd_intro. by apply later_mono, sep_mono_r, wand_mono.
+ by apply later_mono, sep_mono_r, wand_mono.
Qed.
-Lemma tac_wp_write Δ Δ' Δ'' E i l v e v' o Φ :
- to_val e = Some v' →
+Lemma tac_wp_write K Δ Δ' Δ'' E i l v e v' o Φ :
+ IntoVal e v' →
o = Na1Ord ∨ o = ScOrd →
IntoLaterNEnvs 1 Δ Δ' →
envs_lookup i Δ' = Some (false, l ↦ v)%I →
envs_simple_replace i false (Esnoc Enil i (l ↦ v')) Δ' = Some Δ'' →
- (Δ'' ⊢ Φ (LitV LitPoison)) →
- Δ ⊢ WP Write o (Lit $ LitLoc l) e @ E {{ Φ }}.
+ envs_entails Δ'' (WP fill K (Lit LitPoison) @ E {{ Φ }}) →
+ envs_entails Δ (WP fill K (Write o (Lit $ LitLoc l) e) @ E {{ Φ }}).
Proof.
- intros ? [->| ->] ????.
- - rewrite -wp_fupd. eapply wand_apply; first by apply wp_write_na.
+ rewrite /envs_entails; intros ? [->| ->] ????.
+ - rewrite -wp_bind. eapply wand_apply; first by apply wp_write_na.
rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
- rewrite right_id -fupd_intro. by apply later_mono, sep_mono_r, wand_mono.
- - rewrite -wp_fupd. eapply wand_apply; first by apply wp_write_sc.
+ rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
+ - rewrite -wp_bind. eapply wand_apply; first by apply wp_write_sc.
rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
- rewrite right_id -fupd_intro. by apply later_mono, sep_mono_r, wand_mono.
+ rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
Qed.
End heap.
Tactic Notation "wp_apply" open_constr(lem) :=
- iStartProof;
- lazymatch goal with
- | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
- wp_bind_core K; iApply lem; try iNext; simpl)
- | _ => fail "wp_apply: not a 'wp'"
- end.
+ iPoseProofCore lem as false true (fun H =>
+ lazymatch goal with
+ | |- envs_entails _ (wp ?E ?e ?Q) =>
+ reshape_expr e ltac:(fun K e' =>
+ wp_bind_core K; iApplyHyp H; try iNext; simpl) ||
+ lazymatch iTypeOf H with
+ | Some (_,?P) => fail "wp_apply: cannot apply" P
+ end
+ | _ => fail "wp_apply: not a 'wp'"
+ end).
Tactic Notation "wp_alloc" ident(l) "as" constr(H) constr(Hf) :=
iStartProof;
lazymatch goal with
- | |- _ ⊢ wp ?E ?e ?Q =>
+ | |- envs_entails _ (wp ?E ?e ?Q) =>
first
- [reshape_expr e ltac:(fun K e' =>
- match eval hnf in e' with Alloc _ => wp_bind_core K end)
+ [reshape_expr e ltac:(fun K e' => eapply (tac_wp_alloc K _ _ _ H Hf))
|fail 1 "wp_alloc: cannot find 'Alloc' in" e];
- eapply tac_wp_alloc with _ H Hf;
- [try fast_done
- |apply _
- |let sz := fresh "sz" in let Hsz := fresh "Hsz" in
- first [intros l sz Hsz | fail 1 "wp_alloc:" l "not fresh"];
- (* If Hsz is "constant Z = nat", change that to an equation on nat and
- potentially substitute away the sz. *)
- try (match goal with Hsz : ?x = _ |- _ => rewrite <-(Z2Nat.id x) in Hsz; last done end;
- apply Nat2Z.inj in Hsz;
- try (cbv [Z.to_nat Pos.to_nat] in Hsz;
- simpl in Hsz;
- (* Substitute only if we have a literal nat. *)
- match goal with Hsz : S _ = _ |- _ => subst sz end));
- eexists; split;
- [env_cbv; reflexivity || fail "wp_alloc:" H "or" Hf "not fresh"
- |wp_finish]]
+ [try fast_done
+ |apply _
+ |let sz := fresh "sz" in let Hsz := fresh "Hsz" in
+ first [intros l sz Hsz | fail 1 "wp_alloc:" l "not fresh"];
+ (* If Hsz is "constant Z = nat", change that to an equation on nat and
+ potentially substitute away the sz. *)
+ try (match goal with Hsz : ?x = _ |- _ => rewrite <-(Z2Nat.id x) in Hsz; last done end;
+ apply Nat2Z.inj in Hsz;
+ try (cbv [Z.to_nat Pos.to_nat] in Hsz;
+ simpl in Hsz;
+ (* Substitute only if we have a literal nat. *)
+ match goal with Hsz : S _ = _ |- _ => subst sz end));
+ eexists; split;
+ [env_cbv; reflexivity || fail "wp_alloc:" H "or" Hf "not fresh"
+ |simpl; try wp_value_head]]
| _ => fail "wp_alloc: not a 'wp'"
end.
@@ -263,60 +210,52 @@ Tactic Notation "wp_alloc" ident(l) :=
Tactic Notation "wp_free" :=
iStartProof;
lazymatch goal with
- | |- _ ⊢ wp ?E ?e ?Q =>
+ | |- envs_entails _ (wp ?E ?e ?Q) =>
first
- [reshape_expr e ltac:(fun K e' =>
- match eval hnf in e' with Free _ _ => wp_bind_core K end)
+ [reshape_expr e ltac:(fun K e' => eapply (tac_wp_free K))
|fail 1 "wp_free: cannot find 'Free' in" e];
- eapply tac_wp_free;
- [try fast_done
- |apply _
- |let l := match goal with |- _ = Some (_, (?l ↦∗ _)%I) => l end in
- iAssumptionCore || fail "wp_free: cannot find" l "↦∗ ?"
- |env_cbv; reflexivity
- |let l := match goal with |- _ = Some (_, (†?l … _)%I) => l end in
- iAssumptionCore || fail "wp_free: cannot find †" l "… ?"
- |env_cbv; reflexivity
- |try fast_done
- |wp_finish]
+ [try fast_done
+ |apply _
+ |let l := match goal with |- _ = Some (_, (?l ↦∗ _)%I) => l end in
+ iAssumptionCore || fail "wp_free: cannot find" l "↦∗ ?"
+ |env_cbv; reflexivity
+ |let l := match goal with |- _ = Some (_, (†?l … _)%I) => l end in
+ iAssumptionCore || fail "wp_free: cannot find †" l "… ?"
+ |env_cbv; reflexivity
+ |try fast_done
+ |simpl; try first [wp_pure (Seq (Lit LitPoison) _)|wp_value_head]]
| _ => fail "wp_free: not a 'wp'"
end.
Tactic Notation "wp_read" :=
iStartProof;
lazymatch goal with
- | |- _ ⊢ wp ?E ?e ?Q =>
+ | |- envs_entails _ (wp ?E ?e ?Q) =>
first
- [reshape_expr e ltac:(fun K e' =>
- match eval hnf in e' with Read _ _ => wp_bind_core K end)
+ [reshape_expr e ltac:(fun K e' => eapply (tac_wp_read K))
|fail 1 "wp_read: cannot find 'Read' in" e];
- eapply tac_wp_read;
- [(right; fast_done) || (left; fast_done) ||
- fail "wp_read: order is neither Na2Ord nor ScOrd"
- |apply _
- |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
- iAssumptionCore || fail "wp_read: cannot find" l "↦ ?"
- |wp_finish]
+ [(right; fast_done) || (left; fast_done) ||
+ fail "wp_read: order is neither Na2Ord nor ScOrd"
+ |apply _
+ |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
+ iAssumptionCore || fail "wp_read: cannot find" l "↦ ?"
+ |simpl; try wp_value_head]
| _ => fail "wp_read: not a 'wp'"
end.
Tactic Notation "wp_write" :=
iStartProof;
lazymatch goal with
- | |- _ ⊢ wp ?E ?e ?Q =>
+ | |- envs_entails _ (wp ?E ?e ?Q) =>
first
- [reshape_expr e ltac:(fun K e' =>
- match eval hnf in e' with Write _ _ _ => wp_bind_core K end)
+ [reshape_expr e ltac:(fun K e' => eapply (tac_wp_write K); [apply _|..])
|fail 1 "wp_write: cannot find 'Write' in" e];
- eapply tac_wp_write;
- [let e' := match goal with |- to_val ?e' = _ => e' end in
- wp_done || fail "wp_write:" e' "not a value"
- |(right; fast_done) || (left; fast_done) ||
- fail "wp_write: order is neither Na2Ord nor ScOrd"
- |apply _
- |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
- iAssumptionCore || fail "wp_write: cannot find" l "↦ ?"
- |env_cbv; reflexivity
- |wp_finish]
+ [(right; fast_done) || (left; fast_done) ||
+ fail "wp_write: order is neither Na2Ord nor ScOrd"
+ |apply _
+ |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
+ iAssumptionCore || fail "wp_write: cannot find" l "↦ ?"
+ |env_cbv; reflexivity
+ |simpl; try first [wp_pure (Seq (Lit LitPoison) _)|wp_value_head]]
| _ => fail "wp_write: not a 'wp'"
end.
diff --git a/theories/lang/tactics.v b/theories/lang/tactics.v
index 11efdd22f157a236e15fe732e2083350baa18739..a4a69dbf8ca86cfd517cdca767bd9d55bbe46803 100644
--- a/theories/lang/tactics.v
+++ b/theories/lang/tactics.v
@@ -8,7 +8,7 @@ expressions into this type we can implement substitution, closedness
checking, atomic checking, and conversion into values, by computation. *)
Module W.
Inductive expr :=
-| Val (v : val)
+| Val (v : val) (e : lang.expr) (H : to_val e = Some v)
| ClosedExpr (e : lang.expr) `{!Closed [] e}
| Var (x : string)
| Lit (l : base_lit)
@@ -25,7 +25,7 @@ Inductive expr :=
Fixpoint to_expr (e : expr) : lang.expr :=
match e with
- | Val v => of_val v
+ | Val v e' _ => e'
| ClosedExpr e _ => e
| Var x => lang.Var x
| Lit l => lang.Lit l
@@ -66,13 +66,16 @@ Ltac of_expr e :=
| @cons lang.expr ?e ?el =>
let e := of_expr e in let el := of_expr el in constr:(e::el)
| to_expr ?e => e
- | of_val ?v => constr:(Val v)
- | _ => match goal with H : Closed [] e |- _ => constr:(@ClosedExpr e H) end
+ | of_val ?v => constr:(Val v (of_val v) (to_of_val v))
+ | _ => match goal with
+ | H : to_val e = Some ?v |- _ => constr:(Val v e H)
+ | H : Closed [] e |- _ => constr:(@ClosedExpr e H)
+ end
end.
Fixpoint is_closed (X : list string) (e : expr) : bool :=
match e with
- | Val _ | ClosedExpr _ _ => true
+ | Val _ _ _ | ClosedExpr _ _ => true
| Var x => bool_decide (x ∈ X)
| Lit _ => true
| Rec f xl e => is_closed (f :b: xl +b+ X) e
@@ -85,7 +88,7 @@ Fixpoint is_closed (X : list string) (e : expr) : bool :=
Lemma is_closed_correct X e : is_closed X e → lang.is_closed X (to_expr e).
Proof.
revert e X. fix 1; destruct e=>/=;
- try naive_solver eauto using is_closed_of_val, is_closed_weaken_nil.
+ try naive_solver eauto using is_closed_to_val, is_closed_weaken_nil.
- induction el=>/=; naive_solver.
- induction el=>/=; naive_solver.
Qed.
@@ -96,7 +99,7 @@ about apart from being closed. Notice that the reverse implication of
[to_val_Some] thus does not hold. *)
Definition to_val (e : expr) : option val :=
match e with
- | Val v => Some v
+ | Val v _ _ => Some v
| Rec f xl e =>
if decide (is_closed (f :b: xl +b+ []) e) is left H
then Some (@RecV f xl (to_expr e) (is_closed_correct _ _ H)) else None
@@ -116,7 +119,7 @@ Proof. intros [v ?]; exists v; eauto using to_val_Some. Qed.
Fixpoint subst (x : string) (es : expr) (e : expr) : expr :=
match e with
- | Val v => Val v
+ | Val v e H => Val v e H
| ClosedExpr e H => @ClosedExpr e H
| Var y => if bool_decide (y = x) then es else Var y
| Lit l => Lit l
@@ -136,7 +139,7 @@ Lemma to_expr_subst x er e :
to_expr (subst x er e) = lang.subst x (to_expr er) (to_expr e).
Proof.
revert e x er. fix 1; destruct e=>/= ? er; repeat case_bool_decide;
- f_equal; auto using is_closed_nil_subst, is_closed_of_val, eq_sym.
+ f_equal; eauto using is_closed_nil_subst, is_closed_to_val, eq_sym.
- induction el=>//=. f_equal; auto.
- induction el=>//=. f_equal; auto.
Qed.
@@ -174,7 +177,7 @@ Ltac solve_closed :=
Hint Extern 0 (Closed _ _) => solve_closed : typeclass_instances.
Ltac solve_to_val :=
- rewrite /IntoVal;
+ rewrite /IntoVal /AsVal;
try match goal with
| |- context E [language.to_val ?e] =>
let X := context E [to_val e] in change X
@@ -188,6 +191,7 @@ Ltac solve_to_val :=
apply W.to_val_is_Some, (bool_decide_unpack _); vm_compute; exact I
end.
Hint Extern 10 (IntoVal _ _) => solve_to_val : typeclass_instances.
+Hint Extern 10 (AsVal _) => solve_to_val : typeclass_instances.
Ltac solve_atomic :=
match goal with
@@ -270,16 +274,3 @@ Ltac reshape_expr e tac :=
| Case ?e ?el => go (CaseCtx el :: K) e
end
in go (@nil ectx_item) e.
-
-(** The tactic [do_head_step tac] solves goals of the shape [head_reducible] and
-[head_step] by performing a reduction step and uses [tac] to solve any
-side-conditions generated by individual steps. *)
-Tactic Notation "do_head_step" tactic3(tac) :=
- try match goal with |- head_reducible _ _ => eexists _, _, _ end;
- simpl;
- match goal with
- | |- head_step ?e1 ?σ1 ?e2 ?σ2 ?ef =>
- first [apply alloc_fresh|econstructor];
- (* solve [to_val] side-conditions *)
- first [rewrite ?to_of_val; reflexivity|simpl_subst; tac; fast_done]
- end.
diff --git a/theories/typing/base.v b/theories/typing/base.v
index c69fbf5f8648e6a3024411fdc6bdf77f6e3ed8e8..d892ae6159b834b9d89f456196a731372c396a5b 100644
--- a/theories/typing/base.v
+++ b/theories/typing/base.v
@@ -14,6 +14,9 @@ Ltac solve_typing :=
(typeclasses eauto with lrust_typing typeclass_instances core; fail) ||
(typeclasses eauto with lrust_typing lrust_typing_merge typeclass_instances core; fail).
+Lemma of_val_unlock v e : of_val v = e → of_val (locked v) = e.
+Proof. by unlock. Qed.
+
Hint Constructors Forall Forall2 elem_of_list : lrust_typing.
Hint Resolve
of_val_unlock
diff --git a/theories/typing/bool.v b/theories/typing/bool.v
index 2da29d43c387268357aacb02b2689a12031f2056..08784b1a57c986e030cbc44b531c438b0945a2be 100644
--- a/theories/typing/bool.v
+++ b/theories/typing/bool.v
@@ -27,7 +27,7 @@ Section typing.
Lemma type_bool_instr (b : Datatypes.bool) : typed_val #b bool.
Proof.
- iIntros (E L tid) "_ _ $ $ _". wp_value.
+ iIntros (E L tid) "_ _ $ $ _". iApply wp_value.
rewrite tctx_interp_singleton tctx_hasty_val' //. by destruct b.
Qed.
@@ -45,7 +45,7 @@ Section typing.
iIntros (Hp) "He1 He2". iIntros (tid) "#LFT #HE Htl HL HC HT".
iDestruct (big_sepL_elem_of _ _ _ Hp with "HT") as "#Hp".
wp_bind p. iApply (wp_hasty with "Hp").
- iIntros ([[| |[|[]|]]|]) "_ H1"; try done; (iApply wp_case; [done..|iNext]).
+ iIntros ([[| |[|[]|]]|]) "_ H1"; try done; wp_case.
- iApply ("He2" with "LFT HE Htl HL HC HT").
- iApply ("He1" with "LFT HE Htl HL HC HT").
Qed.
diff --git a/theories/typing/cont.v b/theories/typing/cont.v
index caa9284b8af969917dada052b791d6a349a81168..c25ab6b1b3ac3c6b99642ee1c091f6287de888d9 100644
--- a/theories/typing/cont.v
+++ b/theories/typing/cont.v
@@ -34,14 +34,12 @@ Section typing.
typed_body E L2 C T (letcont: kb argsb := econt in e2).
Proof.
iIntros (Hc1 Hc2) "He2 #Hecont". iIntros (tid) "#LFT #HE Htl HL HC HT".
- iApply wp_let'; first by rewrite /= decide_left.
- iModIntro. iApply ("He2" with "LFT HE Htl HL [HC] HT").
+ rewrite (_ : (rec: kb argsb := econt)%E = of_val (rec: kb argsb := econt)%V); last by unlock.
+ wp_let. iApply ("He2" with "LFT HE Htl HL [HC] HT").
iLöb as "IH". iIntros (x) "H".
iDestruct "H" as %[->|?]%elem_of_cons; last by iApply "HC".
- iIntros (args) "Htl HL HT". iApply wp_rec; try done.
- { rewrite Forall_fmap Forall_forall=>? _. rewrite /= to_of_val. eauto. }
- { by rewrite -(subst_v_eq (_ :: _) (RecV _ _ _ ::: _)). }
- iNext. iApply ("Hecont" with "LFT HE Htl HL [HC] HT"). by iApply "IH".
+ iIntros (args) "Htl HL HT". wp_rec.
+ iApply ("Hecont" with "LFT HE Htl HL [HC] HT"). by iApply "IH".
Qed.
Lemma type_cont_norec argsb L1 (T' : vec val (length argsb) → _) E L2 C T econt e2 kb :
@@ -52,13 +50,11 @@ Section typing.
typed_body E L2 C T (letcont: kb argsb := econt in e2).
Proof.
iIntros (Hc1 Hc2) "He2 Hecont". iIntros (tid) "#LFT #HE Htl HL HC HT".
- iApply wp_let'; first by rewrite /= decide_left.
- iModIntro. iApply ("He2" with "LFT HE Htl HL [HC Hecont] HT").
+ rewrite (_ : (rec: kb argsb := econt)%E = of_val (rec: kb argsb := econt)%V); last by unlock.
+ wp_let. iApply ("He2" with "LFT HE Htl HL [HC Hecont] HT").
iIntros (x) "H".
iDestruct "H" as %[->|?]%elem_of_cons; last by iApply "HC".
- iIntros (args) "Htl HL HT". iApply wp_rec; try done.
- { rewrite Forall_fmap Forall_forall=>? _. rewrite /= to_of_val. eauto. }
- { by rewrite -(subst_v_eq (_ :: _) (RecV _ _ _ ::: _)). }
- iNext. iApply ("Hecont" with "LFT HE Htl HL HC HT").
+ iIntros (args) "Htl HL HT". wp_rec.
+ iApply ("Hecont" with "LFT HE Htl HL HC HT").
Qed.
End typing.
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 0fe495160042d571aef8e023491bb6062f3b57e7..e1b8759108e841ed3e45d29c3877afaf8d9ecfb0 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -260,7 +260,7 @@ Section typing.
clear dependent k. wp_apply (wp_hasty with "Hf"). iIntros (v) "% Hf".
iApply (wp_app_vec _ _ (_::_) ((λ v, ⌜v = (λ: ["_r"], (#☠;; #☠) ;; k' ["_r"])%VâŒ):::
vmap (λ ty (v : val), tctx_elt_interp tid (v ◠box ty)) (fp x).(fp_tys))%I
- with "[Hargs]"); first wp_done.
+ with "[Hargs]").
- rewrite /=. iSplitR "Hargs".
{ simpl. iApply wp_value. by unlock. }
remember (fp_tys (fp x)) as tys. clear dependent k' p HE fp x.
@@ -270,13 +270,11 @@ Section typing.
+ iApply (wp_hasty with "HT"). iIntros (?). rewrite tctx_hasty_val. iIntros "? $".
+ iApply "IH". done.
- simpl. change (@length expr ps) with (length ps).
- iIntros (vl'). inv_vec vl'=>kv vl.
- iIntros "/= [% Hvl]". subst kv. iDestruct "Hf" as (fb kb xb e ?) "[EQ [EQl #Hf]]".
+ iIntros (vl'). inv_vec vl'=>kv vl; csimpl.
+ iIntros "[-> Hvl]". iDestruct "Hf" as (fb kb xb e ?) "[EQ [EQl #Hf]]".
iDestruct "EQ" as %[=->]. iDestruct "EQl" as %EQl.
- revert vl fp HE. rewrite <-EQl=>vl fp HE. iApply wp_rec; try done.
- { rewrite -fmap_cons Forall_fmap Forall_forall=>? _. rewrite /= to_of_val. eauto. }
- { rewrite -fmap_cons -(subst_v_eq (fb::kb::xb) (_:::_:::vl)) //. }
- iNext. iMod (lft_create with "LFT") as (Ï) "[Htk #Hinh]"; first done.
+ revert vl fp HE. rewrite /= -EQl=>vl fp HE. wp_rec.
+ iMod (lft_create with "LFT") as (Ï) "[Htk #Hinh]"; first done.
iSpecialize ("Hf" $! x Ï _ vl). iDestruct (HE Ï with "HL") as "#HE'".
iMod (bor_create _ Ï with "LFT Hκs") as "[Hκs HκsI]"; first done.
iDestruct (frac_bor_lft_incl with "LFT [>Hκs]") as "#Hκs".
diff --git a/theories/typing/int.v b/theories/typing/int.v
index 9643e8ba81e78888791bad5c6d35d251cd6ab458..5f94433c1935aec43dcbe14f62db55d93e8ef9c8 100644
--- a/theories/typing/int.v
+++ b/theories/typing/int.v
@@ -26,7 +26,7 @@ Section typing.
Lemma type_int_instr (z : Z) : typed_val #z int.
Proof.
- iIntros (E L tid) "_ _ $ $ _". wp_value.
+ iIntros (E L tid) "_ _ $ $ _". iApply wp_value.
by rewrite tctx_interp_singleton tctx_hasty_val' //.
Qed.
@@ -74,7 +74,7 @@ Section typing.
iIntros (tid) "_ _ $ $ [Hp1 [Hp2 _]]".
wp_apply (wp_hasty with "Hp1"). iIntros ([[]|]) "_ H1"; try done.
wp_apply (wp_hasty with "Hp2"). iIntros ([[]|]) "_ H2"; try done.
- wp_op; intros _; by rewrite tctx_interp_singleton tctx_hasty_val' //.
+ wp_op; case_bool_decide; by rewrite tctx_interp_singleton tctx_hasty_val' //.
Qed.
Lemma type_le E L C T T' p1 p2 x e :
diff --git a/theories/typing/lib/arc.v b/theories/typing/lib/arc.v
index 502c96e216005d06b8931619ce14240a4453318c..3e5a37217532faafb09a6f1e6db5d0052b54d38d 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -771,8 +771,8 @@ Section arc.
iDestruct "Hown" as (???) "(_ & Hlen & _)". wp_write. iIntros "(#Hν & Hown & H†)!>".
wp_seq. wp_op. wp_op. iDestruct "Hown" as (?) "[H↦ Hown]".
iDestruct (ty_size_eq with "Hown") as %?. rewrite Max.max_0_r.
- iDestruct "Hlen" as %[= ?]. iApply (wp_memcpy with "[$H↦1 $H↦]"); [congruence..|].
- iNext. iIntros "[? Hrc']". wp_seq. iMod ("Hdrop" with "[Hrc' H†]") as "Htok".
+ iDestruct "Hlen" as %[= ?]. wp_apply (wp_memcpy with "[$H↦1 $H↦]"); [congruence..|].
+ iIntros "[? Hrc']". wp_seq. iMod ("Hdrop" with "[Hrc' H†]") as "Htok".
{ unfold P2. auto with iFrame. }
wp_apply (drop_weak_spec with "[//] Htok"). unlock. iIntros ([]); last first.
{ iIntros "_". wp_if. unlock. iFrame. iExists (_::_). rewrite heap_mapsto_vec_cons.
@@ -780,7 +780,8 @@ Section arc.
auto 10 with iFrame. }
iIntros "([H†H1] & H2 & H3)". iDestruct "H1" as (vl') "[H1 Heq]".
iDestruct "Heq" as %<-. wp_if.
- wp_apply (wp_delete _ _ _ (_::_::vl') with "[H1 H2 H3 H†]"). lia.
+ wp_apply (wp_delete _ _ _ (_::_::vl') with "[H1 H2 H3 H†]").
+ { simpl. lia. }
{ rewrite 2!heap_mapsto_vec_cons shift_loc_assoc. auto with iFrame. }
iFrame. iIntros "_". iExists (_::_). rewrite heap_mapsto_vec_cons. iFrame.
iExists 1%nat, _, []. rewrite right_id_L. iFrame. iSplit; [by auto|simpl].
@@ -818,7 +819,7 @@ Section arc.
iApply (wp_wand _ _ (λ _, True)%I with "[Hdrop]").
{ destruct b; wp_if=>//. iDestruct "Hdrop" as "((? & H↦) & ? & ?)".
iDestruct "H↦" as (vl) "[? Heq]". iDestruct "Heq" as %<-.
- wp_apply (wp_delete _ _ _ (_::_::vl) with "[-]"); [lia| |done].
+ wp_apply (wp_delete _ _ _ (_::_::vl) with "[-]"); [simpl;lia| |done].
rewrite !heap_mapsto_vec_cons shift_loc_assoc. iFrame. auto. }
iIntros (?) "_". wp_seq.
(* Finish up the proof. *)
@@ -874,15 +875,15 @@ Section arc.
rewrite -(firstn_skipn ty.(ty_size) vl0) heap_mapsto_vec_app.
iDestruct "Hr1" as "[Hr1 Hr2]". iDestruct "Hown" as (vl) "[Hrc' Hown]".
iDestruct (ty_size_eq with "Hown") as %Hlen.
- iApply (wp_memcpy with "[$Hr1 $Hrc']"); rewrite ?firstn_length_le; try lia.
- iIntros "!> [Hr1 Hrc']". wp_seq. wp_bind (drop_weak _).
+ wp_apply (wp_memcpy with "[$Hr1 $Hrc']"); rewrite /= ?firstn_length_le; try lia.
+ iIntros "[Hr1 Hrc']". wp_seq. wp_bind (drop_weak _).
iMod ("Hend" with "[$H†Hrc']") as "Htok"; first by eauto.
iApply (drop_weak_spec with "Ha Htok").
iIntros "!> * Hdrop". wp_bind (if: _ then _ else _)%E.
iApply (wp_wand _ _ (λ _, True)%I with "[Hdrop]").
{ destruct b; wp_if=>//. iDestruct "Hdrop" as "((? & H↦) & ? & ?)".
iDestruct "H↦" as (vl') "[? Heq]". iDestruct "Heq" as %<-.
- wp_apply (wp_delete _ _ _ (_::_::vl') with "[-]"); [lia| |done].
+ wp_apply (wp_delete _ _ _ (_::_::vl') with "[-]"); [simpl; lia| |done].
rewrite !heap_mapsto_vec_cons shift_loc_assoc. iFrame. auto. }
iIntros (?) "_". wp_seq.
iApply (type_type _ _ _ [ rcx ◠box (uninit 1); #r ◠box (Σ[ ty; arc ty ]) ]
diff --git a/theories/typing/lib/fake_shared_box.v b/theories/typing/lib/fake_shared_box.v
index 99530965643368fbd0a1ebbd5abfcbaf346ec303..35c849e5b75840d0c9da4a59170bf619a942665e 100644
--- a/theories/typing/lib/fake_shared_box.v
+++ b/theories/typing/lib/fake_shared_box.v
@@ -27,7 +27,7 @@ Section fake_shared_box.
rewrite heap_mapsto_vec_singleton. iSplit; auto. }
iDestruct "H" as "#H". iIntros "!# * % $". iApply step_fupd_intro. set_solver.
by iApply ty_shr_mono. }
- wp_seq.
+ do 2 wp_seq.
iApply (type_type [] _ _ [ x ◠box (&shr{α}(box ty)) ]
with "[] LFT [] Hna HL Hk [HT]"); last first.
{ by rewrite tctx_interp_singleton tctx_hasty_val. }
diff --git a/theories/typing/lib/panic.v b/theories/typing/lib/panic.v
index 865e9a907c60c6a8ec853450ce209a1aac349e7e..9050768b6b96d769bf195edbb5d110bd52e70d34 100644
--- a/theories/typing/lib/panic.v
+++ b/theories/typing/lib/panic.v
@@ -20,6 +20,6 @@ Section panic.
Proof.
intros E L. iApply type_fn; [solve_typing..|]. iIntros "!# *".
inv_vec args. iIntros (tid) "LFT HE Hna HL Hk HT /=". simpl_subst.
- wp_value. done.
+ by iApply wp_value.
Qed.
End panic.
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index ff86be075f1b78f0eca381a1067af0c419c369a6..83548b9c44881ba74b85d029f4dd8bbb8f0fbe3f 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -692,7 +692,7 @@ Section code.
wp_apply (rc_check_unique with "[$Hna $Hrc']"); first solve_ndisj.
iIntros (strong) "[Hrc Hc]". wp_let.
iDestruct "Hc" as "[[% [_ Hproto]]|[% [Hproto _]]]".
- - subst strong. wp_op=>[_|?]; last done. wp_if. wp_op.
+ - subst strong. wp_op. wp_if. wp_op.
rewrite shift_loc_0. wp_write. wp_bind (#☠;;#☠)%E.
iApply (wp_step_fupd with "[Hproto Hrc]");
[| |by iApply ("Hproto" with "Hrc")|];
@@ -707,7 +707,7 @@ Section code.
iIntros (?) "(Hna & HL & [Hr [Hrc _]])". wp_seq.
iMod ("Hproto" with "Hna") as (weak) "[H↦weak Hproto]". wp_op. wp_read. wp_let.
iDestruct "Hproto" as "[(% & H↦strong & Hna)|[% Hproto]]".
- + subst. wp_op=>[_|[]//]. wp_if.
+ + subst. wp_op. wp_if.
iApply (type_type _ _ _
[ r ◠own_ptr (ty_size Σ[ ty; rc ty ]) (Σ[ ty; rc ty]);
rcx â— box (uninit 1);
@@ -722,7 +722,7 @@ Section code.
iApply (type_delete (Î [uninit 2;uninit ty.(ty_size)])); [solve_typing..|].
iApply type_jump; solve_typing.
+ rewrite (tctx_hasty_val' _ (#rc' +â‚— #2)); last done.
- iDestruct "Hrc" as "[Hrc H†2]". wp_op=>[?|_]. lia. wp_if. wp_op. wp_op. wp_write.
+ iDestruct "Hrc" as "[Hrc H†2]". wp_op; case_bool_decide; first lia. wp_if. wp_op. wp_op. wp_write.
iMod ("Hproto" with "[H†1 H†2] H↦weak Hrc") as "Hna".
{ rewrite -freeable_sz_full_S -(freeable_sz_split _ 2 ty.(ty_size)). iFrame. }
iApply (type_type _ _ _
@@ -731,7 +731,7 @@ Section code.
with "[] LFT HE Hna HL Hk [-]"); last first.
{ unlock. rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame. }
iApply type_jump; solve_typing.
- - wp_op; intros Hc; first lia. wp_if. iMod ("Hproto" with "Hrc") as "[Hna Hrc]".
+ - wp_op; case_bool_decide as Hc; first lia. wp_if. iMod ("Hproto" with "Hrc") as "[Hna Hrc]".
iApply (type_type _ _ _ [ r ◠own_ptr (ty_size Σ[ ty; rc ty ]) (uninit _);
rcx â— box (uninit 1); #rc' â— rc ty ]
with "[] LFT HE Hna HL Hk [-]"); last first.
@@ -791,7 +791,7 @@ Section code.
- subst strong. wp_bind (#1 = #1)%E.
iApply (wp_step_fupd with "[Hproto Hrc]");
[| |by iApply ("Hproto" with "Hrc")|];
- [done..|wp_op=>[_|//]; iIntros "(Hty&H†&Hna&Hproto) !>"; wp_if].
+ [done..|wp_op; iIntros "(Hty&H†&Hna&Hproto) !>"; wp_if].
rewrite <-freeable_sz_full_S, <-(freeable_sz_split _ 2 ty.(ty_size)).
iDestruct "H†" as "[H†1 H†2]". wp_bind (_<-_;;_)%E.
iApply (wp_wand with "[Hna HL Hty Hr H†2]").
@@ -802,7 +802,7 @@ Section code.
iIntros (?) "(Hna & HL & [Hr [Hrc _]])". wp_seq.
iMod ("Hproto" with "Hna") as (weak) "[H↦weak Hproto]". wp_op. wp_read. wp_let.
iDestruct "Hproto" as "[(% & H↦strong & Hna)|[% Hproto]]".
- + subst. wp_op=>[_|[]//]. wp_if.
+ + subst. wp_op. wp_if.
iApply (type_type _ _ _
[ r â— own_ptr (ty_size (option ty)) (option ty);
rcx â— box (uninit 1);
@@ -817,7 +817,7 @@ Section code.
iApply (type_delete (Î [uninit 2;uninit ty.(ty_size)])); [solve_typing..|].
iApply type_jump; solve_typing.
+ rewrite (tctx_hasty_val' _ (#rc' +â‚— #2)); last done.
- iDestruct "Hrc" as "[Hrc H†2]". wp_op=>[?|_]. lia. wp_if. wp_op. wp_op. wp_write.
+ iDestruct "Hrc" as "[Hrc H†2]". wp_op. case_bool_decide; first lia. wp_if. wp_op. wp_op. wp_write.
iMod ("Hproto" with "[H†1 H†2] H↦weak Hrc") as "Hna".
{ rewrite -freeable_sz_full_S -(freeable_sz_split _ 2 ty.(ty_size)). iFrame. }
iApply (type_type _ _ _
@@ -825,7 +825,7 @@ Section code.
with "[] LFT HE Hna HL Hk [-]"); last first.
{ unlock. rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame. }
iApply type_jump; solve_typing.
- - wp_op; intros Hc; first lia. wp_if. iMod ("Hproto" with "Hrc") as "Hna".
+ - wp_op; case_bool_decide as Hc; first lia. wp_if. iMod ("Hproto" with "Hrc") as "Hna".
iApply (type_type _ _ _ [ r â— own_ptr (ty_size (option ty)) (uninit _);
rcx â— box (uninit 1) ]
with "[] LFT HE Hna HL Hk [-]"); last first.
@@ -882,12 +882,12 @@ Section code.
wp_apply (rc_check_unique with "[$Hna Hrcown]"); first done.
{ (* Boy this is silly... *) iDestruct "Hrcown" as "[(?&?&?&?)|?]"; last by iRight.
iLeft. by iFrame. }
- iIntros (c) "(Hl1 & Hc)". wp_let. wp_op; intros Hc.
+ iIntros (c) "(Hl1 & Hc)". wp_let. wp_op; case_bool_decide as Hc.
- wp_if. iDestruct "Hc" as "[[% [Hc _]]|[% _]]"; last lia. subst.
iDestruct "Hc" as (weak) "[Hl2 Hweak]". wp_op. wp_read. wp_let.
iDestruct "Hweak" as "[[% Hrc]|[% [Hrc _]]]".
+ subst. wp_bind (#1 = #1)%E. iApply (wp_step_fupd with "Hrc"); [done..|].
- wp_op=>[_|//]. iIntros "(Hl†& Hty & Hna)!>". wp_if.
+ wp_op. iIntros "(Hl†& Hty & Hna)!>". wp_if.
iMod ("Hclose2" with "[Hrc' Hl1 Hl2 Hl†] [Hty]") as "[Hty Hα]"; [|iNext; iExact "Hty"|].
{ iIntros "!> Hty". iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame "Hrc'".
iLeft. by iFrame. }
@@ -899,7 +899,7 @@ Section code.
unlock. iFrame. }
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]".
+ + wp_op; case_bool_decide; first lia. wp_if. iMod ("Hrc" with "Hl1 Hl2") as "[Hna Hrc]".
iMod ("Hclose2" with "[] [Hrc' Hrc]") as "[Hrc' Hα]".
{ iIntros "!> HX". iModIntro. iExact "HX". }
{ iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame. auto. }
@@ -1014,12 +1014,12 @@ Section code.
wp_apply (rc_check_unique with "[$Hna Hrcown]"); first done.
{ (* Boy this is silly... *) iDestruct "Hrcown" as "[(?&?&?&?)|?]"; last by iRight.
iLeft. by iFrame. }
- iIntros (c) "(Hl1 & Hc)". wp_let. wp_op; intros Hc; wp_if.
+ iIntros (c) "(Hl1 & Hc)". wp_let. wp_op; case_bool_decide as Hc; wp_if.
- iDestruct "Hc" as "[[% [Hc _]]|[% _]]"; last lia. subst.
iDestruct "Hc" as (weak) "[Hl2 Hweak]". wp_op. wp_read. wp_let.
iDestruct "Hweak" as "[[% Hrc]|[% [_ Hrc]]]".
+ subst. wp_bind (#1 = #1)%E. iApply (wp_step_fupd with "Hrc"); [done..|].
- wp_op=>[_|//]. iIntros "(Hl†& Hty & Hna)!>". wp_if.
+ wp_op. iIntros "(Hl†& Hty & Hna)!>". wp_if.
iMod ("Hclose2" with "[Hrc' Hl1 Hl2 Hl†] [Hty]") as "[Hty Hα1]"; [|iNext; iExact "Hty"|].
{ iIntros "!> Hty". iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame "Hrc'".
iLeft. by iFrame. }
@@ -1031,7 +1031,7 @@ Section code.
tctx_hasty_val' //. unlock. iFrame. }
iApply type_assign; [solve_typing..|].
iApply type_jump; solve_typing.
- + wp_op; [lia|move=>_]. wp_if. wp_op. rewrite shift_loc_0. wp_write. wp_op.
+ + wp_op; case_bool_decide; first lia. wp_if. wp_op. rewrite shift_loc_0. wp_write. wp_op.
wp_op. wp_write. wp_bind (new _). iSpecialize ("Hrc" with "Hl1 Hl2").
iApply (wp_step_fupd with "Hrc"); [done..|]. iApply wp_new; first lia. done.
rewrite -!lock Nat2Z.id.
diff --git a/theories/typing/lib/rc/weak.v b/theories/typing/lib/rc/weak.v
index 992f8b234d9172dbeb80055298c31557be1e1771..ed05e2e2f3c60970549123aeb37b9777df7bb3d9 100644
--- a/theories/typing/lib/rc/weak.v
+++ b/theories/typing/lib/rc/weak.v
@@ -164,7 +164,7 @@ Section code.
- (* Success case. *)
iDestruct "Hrcst" as (qb) "(Hl'1 & Hl'2 & Hl'†& >Hq''q0 & [Hν1 Hν2] & Hν†)".
iDestruct "Hq''q0" as %Hq''q0.
- wp_read. wp_let. wp_op=>[//|_]. wp_if. wp_op. rewrite shift_loc_0. wp_op. wp_write.
+ wp_read. wp_let. wp_op. wp_if. wp_op. rewrite shift_loc_0. wp_op. wp_write.
(* Closing the invariant. *)
iMod (own_update with "Hrcâ—") as "[Hrcâ— Hrctok2]".
{ apply auth_update_alloc, prod_local_update_1,
@@ -192,7 +192,7 @@ Section code.
iApply type_jump; solve_typing.
- (* Failure : dropping *)
(* TODO : The two failure cases are almost identical. *)
- iDestruct "Hrcst" as "[Hl'1 Hl'2]". wp_read. wp_let. wp_op=>[_|//]. wp_if.
+ iDestruct "Hrcst" as "[Hl'1 Hl'2]". wp_read. wp_let. wp_op. wp_if.
(* Closing the invariant. *)
iMod ("Hclose3" with "[$Hwtok] Hna") as "[Hα1 Hna]".
iMod ("Hclose2" with "[Hrcâ— Hl'1 Hl'2 $Hna]") as "Hna".
@@ -208,7 +208,7 @@ Section code.
iApply type_jump; solve_typing.
- (* Failure : general case *)
destruct weakc as [|weakc]; first by simpl in *; lia.
- iDestruct "Hrcst" as "[Hl'1 Hrcst]". wp_read. wp_let. wp_op=>[_|//]. wp_if.
+ iDestruct "Hrcst" as "[Hl'1 Hrcst]". wp_read. wp_let. wp_op. wp_if.
(* Closing the invariant. *)
iMod ("Hclose3" with "[$Hwtok] Hna") as "[Hα1 Hna]".
iMod ("Hclose2" with "[Hrcâ— Hl'1 Hrcst $Hna]") as "Hna".
@@ -421,7 +421,7 @@ Section code.
+ iRight. iSplitR; first by auto with lia. iIntros "!>?". iApply "Hclose".
iFrame. iExists _. iFrame. simpl. destruct Pos.of_succ_nat; try done.
by rewrite /= Pos.pred_double_succ. }
- - subst. wp_read. wp_let. wp_op=>[_|//]. wp_if.
+ - subst. wp_read. wp_let. wp_op. wp_if.
iApply (type_type _ _ _ [ w â— box (uninit 1); #lw â— box (uninit (2 + ty.(ty_size))) ]
with "[] LFT HE Hna HL Hk [-]"); last first.
{ rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
@@ -431,7 +431,7 @@ Section code.
iIntros "!> !%". simpl. congruence. }
iApply type_delete; [try solve_typing..|].
iApply type_jump; solve_typing.
- - wp_read. wp_let. wp_op=>[|_]; first lia. wp_if. wp_op. wp_op. wp_write.
+ - wp_read. wp_let. wp_op; case_bool_decide; first lia. wp_if. wp_op. wp_op. wp_write.
iMod ("Hclose" with "Hlw") as "Hna".
iApply (type_type _ _ _ [ w â— box (uninit 1) ]
with "[] LFT HE Hna HL Hk [-]"); last first.
diff --git a/theories/typing/lib/refcell/refcell_code.v b/theories/typing/lib/refcell/refcell_code.v
index 1c06d34d0aa2cabdd5734721654d6b8913449973..b5c9942143058ddf57d8530e068f76a0fc570bd1 100644
--- a/theories/typing/lib/refcell/refcell_code.v
+++ b/theories/typing/lib/refcell/refcell_code.v
@@ -157,7 +157,7 @@ Section refcell_functions.
iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose)"; [solve_typing..|].
iMod (lft_incl_acc with "Hαβ Hα") as (qβ) "[[Hβtok1 Hβtok2] Hclose']". done.
iMod (na_bor_acc with "LFT Hinv Hβtok1 Hna") as "(INV & Hna & Hclose'')"; try done.
- iDestruct "INV" as (st) "(Hlx & Hownst & Hst)". wp_read. wp_let. wp_op=>?; wp_if.
+ iDestruct "INV" as (st) "(Hlx & Hownst & Hst)". wp_read. wp_let. wp_op; case_bool_decide; wp_if.
- iMod ("Hclose''" with "[Hlx Hownst Hst] Hna") as "[Hβtok1 Hna]";
first by iExists st; iFrame.
iMod ("Hclose'" with "[$Hβtok1 $Hβtok2]") as "Hα".
@@ -264,7 +264,7 @@ Section refcell_functions.
iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose)"; [solve_typing..|].
iMod (lft_incl_acc with "Hαβ Hα") as (qβ) "[Hβtok Hclose']". done.
iMod (na_bor_acc with "LFT Hinv Hβtok Hna") as "(INV & Hna & Hclose'')"; try done.
- iDestruct "INV" as (st) "(Hlx & Hownst & Hb)". wp_read. wp_let. wp_op=>?; wp_if.
+ iDestruct "INV" as (st) "(Hlx & Hownst & Hb)". wp_read. wp_let. wp_op; case_bool_decide; wp_if.
- wp_write. wp_apply wp_new; [done..|].
iIntros (lref) "(H†& Hlref)". wp_let.
rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index 50415055395e6c7abad309b74527c52cc1f126b4..130dff9ebd6878bb8c12ee63e5c36636551591af 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -166,7 +166,7 @@ Section rwlock_functions.
iMod (at_bor_acc_tok with "LFT Hinv Hβtok1") as "[INV Hclose'']"; try done.
iDestruct "INV" as (st) "(Hlx & INV)". wp_read.
iMod ("Hclose''" with "[Hlx INV]") as "Hβtok1"; first by iExists _; iFrame.
- iModIntro. wp_let. wp_op=>Hm1; wp_if.
+ iModIntro. wp_let. wp_op; case_bool_decide as Hm1; wp_if.
- iMod ("Hclose'" with "[$]") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
iApply (type_type _ _ _
[ x ◠box (&shr{α}(rwlock ty)); r ◠box (uninit 2) ]
@@ -179,7 +179,7 @@ Section rwlock_functions.
iMod (at_bor_acc_tok with "LFT Hinv Hβtok1") as "[INV Hclose'']"; try done.
iDestruct "INV" as (st') "(Hlx & Hownst & Hst)". revert Hm1.
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".
+ + iApply (wp_cas_int_suc with "Hlx"). iNext. iIntros "Hlx".
iAssert (∃ qν ν, (qβ / 2).[β] ∗ (qν).[ν] ∗
ty_shr ty (β ⊓ ν) tid (lx +ₗ 1) ∗
own γ (◯ reading_st qν ν) ∗ rwlock_inv tid lx γ β ty ∗
@@ -273,7 +273,7 @@ Section rwlock_functions.
wp_bind (CAS _ _ _).
iMod (at_bor_acc_tok with "LFT Hinv Hβtok") as "[INV Hclose'']"; try done.
iDestruct "INV" as (st) "(Hlx & >Hownst & Hst)". destruct st.
- - iApply (wp_cas_int_fail with "Hlx"). done. by destruct c as [|[[]]|].
+ - iApply (wp_cas_int_fail with "Hlx"). by destruct c as [|[[]]|].
iNext. iIntros "Hlx".
iMod ("Hclose''" with "[Hlx Hownst Hst]") as "Hβtok"; first by iExists _; iFrame.
iMod ("Hclose'" with "Hβtok") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
@@ -285,7 +285,7 @@ Section rwlock_functions.
iApply (type_sum_unit (option $ rwlockwriteguard α ty));
[solve_typing..|]; first last.
rewrite /option /=. iApply type_jump; solve_typing.
- - iApply (wp_cas_int_suc with "Hlx"). done. iIntros "!> Hlx".
+ - iApply (wp_cas_int_suc with "Hlx"). iIntros "!> Hlx".
iMod (own_update with "Hownst") as "[Hownst ?]".
{ by eapply auth_update_alloc, (op_local_update_discrete _ _ writing_st). }
iMod ("Hclose''" with "[Hlx Hownst]") as "Hβtok". { iExists _. iFrame. }
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index 9a6f357382380c9595adce8710acb92bd77be449..5bfcaccd25e7bd0b0bfc61a3a89cf1263e7f4681 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -123,7 +123,7 @@ Section rwlockreadguard_functions.
iApply (wp_cas_int_suc with "Hlx"); try done. iNext. iIntros "Hlx INV !>".
iMod ("INV" with "Hlx") as "INV". iMod ("Hcloseβ" with "[$INV]") as "Hβ".
iMod ("Hcloseα" with "Hβ") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
- iApply (wp_if _ true). iIntros "!>!>".
+ iModIntro. wp_if.
iApply (type_type _ _ _ [ x â— box (uninit 1)]
with "[] LFT HE Hna HL Hk"); first last.
{ rewrite tctx_interp_singleton tctx_hasty_val //. }
@@ -133,7 +133,7 @@ Section rwlockreadguard_functions.
+ iApply (wp_cas_int_fail with "Hlx"); try done. iNext. iIntros "Hlx".
iMod ("Hcloseβ" with "[Hlx H◠Hst]") as "Hβ". by iExists _; iFrame.
iMod ("Hcloseα" with "Hβ") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
- iApply (wp_if _ false). iIntros "!> !>".
+ iModIntro. wp_if.
iApply (type_type _ _ _ [ x ◠box (uninit 1); #lx' ◠rwlockreadguard α ty]
with "[] LFT HE Hna HL Hk"); first last.
{ rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val
diff --git a/theories/typing/lib/take_mut.v b/theories/typing/lib/take_mut.v
index 9edf93f09c3ebc85269789696af454f951373221..af60ddb097010f8731f52ea73d5040ab9861eaa5 100644
--- a/theories/typing/lib/take_mut.v
+++ b/theories/typing/lib/take_mut.v
@@ -49,8 +49,7 @@ Section code.
(* Prove the continuation of the function call. *)
iIntros (r) "Hna HÏ Hr". simpl.
iDestruct (ownptr_own with "Hr") as (lr rvl) "(% & Hlr & Hrvl & Hlr†)". subst r.
- iApply wp_rec; try (done || apply _).
- { repeat econstructor. } simpl_subst. iNext.
+ wp_rec.
rewrite (right_id static).
wp_apply (wp_memcpy with "[$Hx'↦ $Hlr]"); [by auto using vec_to_list_length..|].
iIntros "[Hlx' Hlr]". wp_seq.
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index 54469b366b36edd885040d25d28cac339b239ba9..5f0db23720e06e4935a9a252c42eeeccee297351 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -117,8 +117,8 @@ Section typing_rules.
iIntros (Hc) "He He'". iIntros (tid) "#LFT #HE Htl HL HC HT". rewrite tctx_interp_app.
iDestruct "HT" as "[HT1 HT]". wp_bind e. iApply (wp_wand with "[He HL HT1 Htl]").
{ iApply ("He" with "LFT HE Htl HL HT1"). }
- iIntros (v) "/= (Htl & HL & HT2)". iApply wp_let; first wp_done.
- iModIntro. iApply ("He'" with "LFT HE Htl HL HC [HT2 HT]").
+ iIntros (v) "/= (Htl & HL & HT2)". wp_let.
+ iApply ("He'" with "LFT HE Htl HL HC [HT2 HT]").
rewrite tctx_interp_app. by iFrame.
Qed.
diff --git a/theories/typing/soundness.v b/theories/typing/soundness.v
index b88d1123893b25a78e3cb9064628689ecca837a8..ea61633256764b05e2ebd91b426ec3c8fc74a003 100644
--- a/theories/typing/soundness.v
+++ b/theories/typing/soundness.v
@@ -47,10 +47,8 @@ Section type_soundness.
iDestruct "Hmain" as (?) "[EQ Hmain]".
rewrite eval_path_of_val. iDestruct "EQ" as %[= <-].
iDestruct "Hmain" as (f k x e ?) "(EQ & % & Hmain)". iDestruct "EQ" as %[= ->].
- destruct x; try done.
- iApply (wp_rec _ _ _ _ _ _ [exit_cont]%E); [done| |by simpl_subst|iNext].
- { repeat econstructor. apply to_of_val. }
- iMod (lft_create with "LFT") as (Ï) "HÏ". done.
+ destruct x; try done. wp_rec.
+ iMod (lft_create with "LFT") as (Ï) "HÏ"; first done.
iApply ("Hmain" $! () Ï exit_cont [#] tid with "LFT [] Htl [HÏ] []");
last by rewrite tctx_interp_nil.
{ by rewrite /elctx_interp /=. }
diff --git a/theories/typing/type_sum.v b/theories/typing/type_sum.v
index 35867764cea5cdd1b38bf8f026e764365a0fdb6f..3c5cabf5e577874ede0375bc173e26a23c566fea 100644
--- a/theories/typing/type_sum.v
+++ b/theories/typing/type_sum.v
@@ -29,7 +29,7 @@ Section case.
rewrite nth_lookup.
destruct (tyl !! i) as [ty|] eqn:EQty; last iDestruct "Hown" as ">[]".
edestruct @Forall2_lookup_l as (e & He & Hety); eauto.
- wp_read. iApply wp_case; [lia|by rewrite Nat2Z.id|]. iNext.
+ wp_read. wp_case; first (split; [lia|by rewrite Nat2Z.id]).
destruct Hety as [Hety|Hety]; iApply (Hety with "LFT HE Hna HL HC");
rewrite !tctx_interp_cons !tctx_hasty_val' /= ?Hv //=; iFrame "HT".
- rewrite /own_ptr /=. iDestruct (ty.(ty_size_eq) with "Hown") as %<-.
@@ -73,7 +73,7 @@ Section case.
iDestruct "H↦" as "(H↦i & H↦vl' & H↦vl'')".
destruct (tyl !! i) as [ty|] eqn:EQty; last iDestruct "Hown" as ">[]".
edestruct @Forall2_lookup_l as (e & He & Hety); eauto.
- wp_read. iApply wp_case; [lia|by rewrite Nat2Z.id|]. iNext.
+ wp_read. wp_case; first (split; [lia|by rewrite Nat2Z.id]).
iDestruct (ty.(ty_size_eq) with "Hown") as %EQlenvl'.
destruct Hety as [Hety|Hety].
- iMod ("Hclose'" $! ((l +ₗ 1) ↦∗: ty.(ty_own) tid)%I
@@ -123,7 +123,7 @@ Section case.
rewrite nth_lookup.
destruct (tyl !! i) as [ty|] eqn:EQty; last done.
edestruct @Forall2_lookup_l as (e & He & Hety); eauto.
- wp_read. iApply wp_case; [lia|by rewrite Nat2Z.id|]. iNext.
+ wp_read. wp_case; first (split; [lia|by rewrite Nat2Z.id]).
iMod ("Hclose'" with "[$H↦i $H↦vl'']") as "Htok".
iMod ("Hclose" with "Htok") as "HL".
destruct Hety as [Hety|Hety]; iApply (Hety with "LFT HE Hna HL HC");