From 7678645fecc5576055d8b4fe8dbc802697511b54 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?L=C3=A9o=20Stefanesco?= <leo.lveb@gmail.com>
Date: Wed, 25 May 2022 18:47:06 +0200
Subject: [PATCH] [Fairness] add program logic tactics, and general cleanups
---
fairness/examples/yesno.v | 272 ++++-----
fairness/heap_lang/lifting.v | 90 +--
fairness/heap_lang/proofmode.v | 1023 ++++++++++++++++++++++++++++++++
fairness/resources.v | 244 ++++----
4 files changed, 1299 insertions(+), 330 deletions(-)
create mode 100644 fairness/heap_lang/proofmode.v
diff --git a/fairness/examples/yesno.v b/fairness/examples/yesno.v
index 05c8ad5..7f3f3e3 100644
--- a/fairness/examples/yesno.v
+++ b/fairness/examples/yesno.v
@@ -4,7 +4,7 @@ From trillium.fairness Require Import fairness fair_termination.
From trillium.prelude Require Export finitary quantifiers sigma classical_instances.
Require Import stdpp.decidable.
-From trillium.fairness.heap_lang Require Export lang lifting tactics.
+From trillium.fairness.heap_lang Require Export lang lifting tactics proofmode.
From trillium.fairness.heap_lang Require Import notation.
From iris.base_logic.lib Require Import invariants.
From iris.prelude Require Import options.
@@ -15,61 +15,6 @@ Import derived_laws_later.bi.
Set Default Proof Using "Type".
-(* Make it less ridiculous later... *)
-Ltac solve_vals_compare_safe :=
- (* The first branch is for when we have [vals_compare_safe] in the context.
- The other two branches are for when either one of the branches reduces to
- [True] or we have it in the context. *)
- fast_done || (left; fast_done) || (right; fast_done).
-
-Tactic Notation "solve_pure_exec" :=
- lazymatch goal with
- | |- PureExec _ _ ?e _ =>
- let e := eval simpl in e in
- reshape_expr e ltac:(fun K e' =>
- eapply (pure_exec_fill K _ _ e');
- [iSolveTC (* PureExec *)
- (* |try solve_vals_compare_safe (* The pure condition for PureExec -- handles trivial goals, including [vals_compare_safe] *) *)
- ])
- || fail "failed :("
- end.
-
-
-Tactic Notation "wp_bind" open_constr(efoc) :=
- lazymatch goal with
- | |- context[(wp ?s ?E ?tid ?e ?Q)] =>
- reshape_expr e ltac:(fun K e' => unify e' efoc;
- iApply (wp_bind K); simpl
- )
- || fail "wp_bind: cannot find" efoc "in" e
- | _ => fail "wp_bind: not a 'wp'"
- end.
-
-
-Ltac my_pure Hf :=
- iApply wp_lift_pure_step_no_fork_singlerole; eauto;
- do 3 iModIntro; iFrame; try iModIntro;
- iIntros Hf; simpl.
-
-Ltac my_pures Hf :=
- repeat (my_pure Hf).
-
-Ltac my_ld Hpthf :=
- wp_bind (Load _);
- iApply (wp_load_nostep with Hpthf); (try set_solver);
- [| iFrame; by rewrite has_fuel_fuels_S | (* TODO: one role versions! *)
- iModIntro; iIntros Hpthf; rewrite -has_fuel_fuels]; first set_solver.
-
-Ltac my_st Hpthf :=
- wp_bind (Store _ _);
- iApply (wp_store_nostep with Hpthf);(try set_solver);
- [| iFrame; by rewrite has_fuel_fuels_S |
- iModIntro; iIntros Hpthf; rewrite -has_fuel_fuels]; first set_solver.
-
-
-Global Hint Extern 0 (PureExec _ _ _ _) => solve_pure_exec: core.
-Global Hint Extern 0 (vals_compare_safe _ _) => solve_vals_compare_safe: core.
-
Definition yes_go : val :=
rec: "yes_go" "n" "b" :=
(if: CAS "b" #true #false
@@ -265,10 +210,7 @@ Section proof.
iIntros (Φ) "(#Hinv & Hf & HnN & %HN & Hyes & Hyesf) Hk". unfold yes_go.
- destruct f as [|f]; first lia. my_pure "Hf".
- destruct f as [|f]; first lia. my_pure "Hf".
- destruct f as [|f]; first lia. my_pure "Hf".
-
+ wp_pures.
wp_bind (CmpXchg _ _ _).
assert (∀ s, Atomic s (CmpXchg #b #true #false)).
@@ -281,6 +223,8 @@ Section proof.
destruct B; iDestruct "Hauths" as "[>Hay >Han]".
- iDestruct (yes_agree with "Hyes Hay") as "%Heq". rewrite -> Heq in *. clear Heq.
rewrite (Htrue' HN).
+ (* TODO *)
+ rewrite -has_fuel_fuels.
iApply (wp_cmpxchg_suc_step_singlerole _ tid (Y: fmrole the_model) _ 30%nat
(N, true, true, true) (N, false, true, true)
with "[$]"); eauto.
@@ -296,23 +240,25 @@ Section proof.
destruct N as [|N]; first lia. rewrite decide_True; last first.
{ destruct N; set_solver. }
- my_pures "Hf".
+ iModIntro.
- my_ld "[HnN Hf]".
- my_pures "Hf".
- my_st "[HnN Hf]".
- my_pures "Hf".
- my_ld "[HnN Hf]".
- my_pures "Hf".
+ rewrite has_fuel_fuels.
+ wp_pures.
+ wp_load.
+ wp_pures.
+ wp_store.
+ wp_pures.
+ wp_load.
+ wp_pures.
destruct (decide (0 < S N - 1)) as [Heq|Heq].
+ rewrite bool_decide_eq_true_2 //; last lia.
+ wp_pure _.
- my_pure "Hf".
-
+ rewrite -has_fuel_fuels.
iApply ("Hg" with "[] [Hyes HnN Hf Hyesf] [$]"); last first.
{ iFrame "∗#". iSplit; last (iPureIntro; lia).
- replace (#(N - 0)%nat) with (#(S N - 1)); first done.
+ replace (#(S N - 1)%nat) with (#(S N - 1)); first done.
do 2 f_equal. lia. }
iPureIntro; lia.
+ rewrite bool_decide_eq_false_2 //; last lia.
@@ -334,6 +280,8 @@ Section proof.
{ set_solver. }
{ lia. }
{ econstructor. lia. }
+
+ rewrite -has_fuel_fuels.
iFrame. iModIntro.
iMod (yes_finished_update false with "[$]") as "[Hayesf Hyesf]".
iModIntro. iNext. iModIntro.
@@ -359,6 +307,7 @@ Section proof.
{ lia. }
{ econstructor. lia. }
+ rewrite -has_fuel_fuels.
iFrame. iModIntro.
iMod (yes_finished_update false with "[$]") as "[Hayesf Hyesf]".
iModIntro. iNext. iModIntro.
@@ -377,6 +326,8 @@ Section proof.
- iDestruct (yes_agree with "Hyes Hay") as "%Heq". rewrite -> Heq in *.
have HM: M > 0 by lia.
rewrite (Htrue' HM).
+
+ rewrite -has_fuel_fuels.
iApply (wp_cmpxchg_fail_step_singlerole _ tid (Y: fmrole the_model) _ 30%nat
(M, false, true, true) (M, false, true, true)
with "[$]"); eauto.
@@ -391,11 +342,13 @@ Section proof.
destruct N as [|N]; first lia. rewrite decide_True; last first.
{ destruct N; set_solver. }
- my_pures "Hf".
- my_ld "[HnN Hf]".
-
- do 2 (my_pure "Hf").
+ rewrite has_fuel_fuels.
+ iModIntro.
+ wp_pures.
+ wp_load.
+ do 2 wp_pure _.
+ rewrite -has_fuel_fuels.
iApply ("Hg" with "[] [Hyes HnN Hf Hyesf] [$]"); last first.
{ iFrame "∗#". iPureIntro; lia. }
iPureIntro; lia.
@@ -408,20 +361,20 @@ Section proof.
Proof.
iIntros (Φ) "(#Hinv & Hf & %HN & Hyes & Hyesf) Hk". unfold yes.
- destruct f as [|f]; first lia. my_pure "Hf".
- destruct f as [|f]; first lia. my_pure "Hf".
- destruct f as [|f]; first lia. my_pure "Hf".
-
- destruct f as [|f]; first lia.
+ wp_pures.
wp_bind (Alloc _).
- iApply (wp_alloc_nostep _ _ _ _ {[Y]} with "[Hf]"); first set_solver.
- { by rewrite has_fuel_fuels_S. }
+ rewrite has_fuels_gt_1; last by solve_fuel_positive.
+
+ iApply (wp_alloc_nostep _ _ _ _ {[Y := _]}%nat with "[Hf]").
+ { apply map_non_empty_singleton. }
+ { rewrite fmap_insert fmap_empty. done. }
iNext. iIntros (n) "(HnN & _ & Hf)".
rewrite -has_fuel_fuels.
- destruct f as [|f]; first lia. my_pure "Hf".
- destruct f as [|f]; first lia. my_pure "Hf".
+ wp_pures.
+
+ rewrite -has_fuel_fuels.
iApply (yes_go_spec with "[-Hk]"); try iFrame.
{ lia. }
@@ -437,12 +390,12 @@ Section proof.
iIntros (Φ) "(#Hinv & Hf & HnN & %HN & Hno & Hnof) Hk". unfold no_go.
- destruct f as [|f]; first lia. my_pure "Hf".
- destruct f as [|f]; first lia. my_pure "Hf".
- destruct f as [|f]; first lia. my_pure "Hf".
+ wp_pures.
wp_bind (CmpXchg _ _ _).
+ rewrite -has_fuel_fuels.
+
iApply wp_atomic.
iInv Ns as (M B yf nf) "(>[%Htrue %Htrue'] & >Hayesf & >Hanof & >Hmod & >Bb & Hauths)" "Hclose".
iDestruct (no_finished_agree with "Hnof Hanof") as %->.
@@ -467,22 +420,24 @@ Section proof.
destruct N as [|N]; first lia. rewrite decide_True; last first.
{ destruct N; set_solver. }
- my_pures "Hf".
- my_ld "[HnN Hf]".
- my_pures "Hf".
- my_st "[HnN Hf]".
- my_pures "Hf".
- my_ld "[HnN Hf]".
- my_pures "Hf".
+ iModIntro.
+ wp_pures.
+ wp_load.
+ wp_pures.
+ wp_store.
+ wp_pures.
+ wp_load.
+ wp_pures.
destruct (decide (0 < S N - 1)) as [Heq|Heq].
+ rewrite bool_decide_eq_true_2 //; last lia.
- my_pure "Hf".
+ wp_pure _.
+ rewrite -has_fuel_fuels.
iApply ("Hg" with "[] [Hno HnN Hf Hnof] [$]"); last first.
{ iFrame "∗#". iSplit; last (iPureIntro; lia).
- replace (#(N - 0)%nat) with (#(S N - 1)); first done.
+ replace (#(S N - 1)%nat) with (#(S N - 1)); first done.
do 2 f_equal. lia. }
iPureIntro; lia.
+ rewrite bool_decide_eq_false_2 //; last lia.
@@ -498,6 +453,7 @@ Section proof.
iDestruct (no_agree with "Hno Han") as %->.
iDestruct (no_finished_agree with "Hnof Hanof") as %->.
+ rewrite -has_fuel_fuels.
iApply (wp_lift_pure_step_no_fork_singlerole_take_step
((0, true, yf, true): fmstate the_model) (0, true, yf, false) _ _ _ _ 0
); eauto.
@@ -520,6 +476,7 @@ Section proof.
iDestruct (no_agree with "Hno Hano") as %->.
iDestruct (no_finished_agree with "Hnof Hanof") as %->.
+ rewrite -has_fuel_fuels.
iApply (wp_lift_pure_step_no_fork_singlerole_take_step
((0, false, yf, true): fmstate the_model) (0, false, yf, false) _ _ _ _ 0
); eauto.
@@ -557,11 +514,12 @@ Section proof.
destruct N as [|N]; first lia. rewrite decide_True; last first.
{ destruct N; set_solver. }
- my_pures "Hf".
- my_ld "[HnN Hf]".
-
- do 2 (my_pure "Hf").
+ iModIntro.
+ wp_pures.
+ wp_load.
+ do 2 wp_pure _.
+ rewrite -has_fuel_fuels.
iApply ("Hg" with "[] [-Hk] [$]"); last first.
{ iFrame "∗#". iPureIntro; lia. }
iPureIntro; lia.
@@ -572,25 +530,22 @@ Section proof.
no #N #b @ tid
{{{ RET #(); tid ↦M ∅ }}}.
Proof.
- iIntros (Φ) "(#Hinv & Hf & %HN & Hno & Hnof) Hk". unfold no.
-
- destruct f as [|f]; first lia. my_pure "Hf".
- destruct f as [|f]; first lia. my_pure "Hf".
- destruct f as [|f]; first lia. my_pure "Hf".
+ iIntros (Φ) "(#Hinv & Hf & %HN & Hyes & Hyesf) Hk". unfold no.
- destruct f as [|f]; first lia.
+ wp_pures.
wp_bind (Alloc _).
- iApply (wp_alloc_nostep _ _ _ _ {[No]} with "[Hf]"); first set_solver.
- { by rewrite has_fuel_fuels_S. }
+ rewrite has_fuels_gt_1; last by solve_fuel_positive.
+
+ iApply (wp_alloc_nostep _ _ _ _ {[No := _]}%nat with "[Hf]").
+ { apply map_non_empty_singleton. }
+ { rewrite fmap_insert fmap_empty. done. }
iNext. iIntros (n) "(HnN & _ & Hf)".
rewrite -has_fuel_fuels.
- destruct f as [|f]; first lia.
-
+ wp_pures.
- my_pure "Hf".
- destruct f as [|f]; first lia. my_pure "Hf".
+ rewrite -has_fuel_fuels.
iApply (no_go_spec with "[-Hk]"); try iFrame.
{ lia. }
@@ -605,39 +560,23 @@ Section proof_start.
Lemma start_spec tid (N: nat) f (Hf: f > 40):
{{{ frag_model_is (N, true, true, true) ∗
- has_fuels tid {[ Y; No ]} {[ Y := f; No := f ]} ∗ ⌜N > 0⌠}}}
+ has_fuels tid {[ Y := f; No := f ]} ∗ ⌜N > 0⌠}}}
start #N @ tid
{{{ RET #(); tid ↦M ∅ }}}.
Proof using All.
iIntros (Φ) "[Hst [Hf %HN]] Hkont". unfold start.
- destruct f as [|f]; first lia.
- iApply (wp_lift_pure_step_no_fork tid _ _ _ _ _ {[Y := f; No := f]} {[Y; No]});
- [set_solver | eauto |].
- do 3 iModIntro. iSplitL "Hf".
- { unfold has_fuels_S. eauto. rewrite !fmap_insert fmap_empty //=. }
- iIntros "Hf". simpl.
+ wp_pures.
- destruct f as [|f]; first lia.
wp_bind (Alloc _).
- iApply (wp_alloc_nostep _ _ _ _ {[Y; No]} {[Y := f; No := f]} with "[Hf]");
- [set_solver | eauto |].
- { unfold has_fuels_S. eauto. rewrite !fmap_insert fmap_empty //=. }
- iIntros "!>" (l) "(Hl & _ & Hf)".
-
+ iApply (wp_alloc_nostep _ _ _ _ {[Y := _; No := _]} with "[Hf]").
+ { apply insert_non_empty. }
+ { rewrite has_fuels_gt_1; last solve_fuel_positive.
+ rewrite !fmap_insert fmap_empty //. }
- destruct f as [|f]; first lia.
- iApply (wp_lift_pure_step_no_fork tid _ _ _ _ _ {[Y := f; No := f]} {[Y; No]} True) ;
- [set_solver | eauto | eauto |].
- do 3 iModIntro. iSplitL "Hf".
- { unfold has_fuels_S. eauto. rewrite !fmap_insert fmap_empty //=. }
- iIntros "Hf". simpl.
+ iIntros "!>" (l) "(Hl & _ & Hf)".
- destruct f as [|f]; first lia.
- iApply (wp_lift_pure_step_no_fork tid _ _ _ _ _ {[Y := f; No := f]} {[Y; No]} True) ; eauto; first set_solver.
- do 3 iModIntro. iSplitL "Hf".
- { unfold has_fuels_S. eauto. rewrite !fmap_insert fmap_empty //=. }
- iIntros "Hf". simpl.
+ wp_pures.
(* Allocate the invariant. *)
iMod (own_alloc (â—E N â‹… â—¯E N)) as (γ_yes_at) "[Hyes_at_auth Hyes_at]".
@@ -663,48 +602,41 @@ Section proof_start.
iModIntro.
wp_bind (Fork _).
- destruct f as [|f]; first lia.
- iApply (wp_fork_nostep _ tid _ _ _ {[ No ]} {[ Y ]} {[Y := f; No := f]} with "[Hyes_at Hyes_fin] [- Hf] [Hf]").
- all: cycle 4.
- { unfold has_fuels_S. eauto. rewrite !fmap_insert fmap_empty //=.
- rewrite insert_commute // union_comm_L //. }
- { set_solver. }
- { apply insert_non_empty. }
- { iIntros (tid') "!> Hf". iApply (yes_spec _ _ _ f with "[-]"); eauto; first lia.
- rewrite map_filter_insert_True; last set_solver.
- rewrite map_filter_insert_not; last set_solver.
- rewrite map_filter_empty insert_empty.
- rewrite has_fuel_fuels. by iFrame "#∗". }
+ rewrite has_fuels_gt_1; last solve_fuel_positive.
+ iApply (wp_fork_nostep _ tid _ _ _ {[ No ]} {[ Y ]} {[Y := _; No := _]}
+ with "[Hyes_at Hyes_fin] [- Hf] [Hf]");
+ [ set_solver | by apply insert_non_empty | | | | rewrite !fmap_insert fmap_empty // ];
+ [set_solver | |].
+ { iIntros (tid') "!> Hf". iApply (yes_spec with "[-]"); last first.
+ + by eauto.
+ + rewrite map_filter_insert_True; last set_solver.
+ rewrite map_filter_insert_not; last set_solver.
+ rewrite map_filter_empty insert_empty.
+ rewrite has_fuel_fuels. by iFrame "#∗".
+ + lia. }
iIntros "!> Hf".
rewrite map_filter_insert_not; last set_solver.
rewrite map_filter_insert_True; last set_solver.
rewrite map_filter_empty insert_empty.
- destruct f as [|f]; first lia.
- iApply (wp_lift_pure_step_no_fork tid _ _ _ _ _ {[No := f]} {[No]} True) ; eauto; first set_solver.
- do 3 iModIntro. iSplitL "Hf".
- { unfold has_fuels_S. eauto. rewrite !fmap_insert fmap_empty //=. }
- iModIntro. iIntros "Hf". simpl.
-
- destruct f as [|f]; first lia.
- iApply (wp_lift_pure_step_no_fork tid _ _ _ _ _ {[No := f]} {[No]} True) ; eauto; first set_solver.
- do 3 iModIntro. iSplitL "Hf".
- { unfold has_fuels_S. eauto. rewrite !fmap_insert fmap_empty //=. }
- iIntros "Hf". simpl.
-
- destruct f as [|f]; first lia.
- iApply (wp_fork_nostep _ tid _ _ _ ∅ {[ No ]} {[No := f]} with "[Hno_at Hno_fin] [Hkont] [Hf]").
- all: cycle 4.
- { unfold has_fuels_S. eauto. rewrite union_empty_l_L !fmap_insert fmap_empty //=. }
- { set_solver. }
- { apply insert_non_empty. }
- { iIntros (tid') "!> Hf". iApply (no_spec _ _ _ f with "[-]"); eauto; first lia.
- rewrite map_filter_insert_True; last set_solver.
- rewrite map_filter_empty insert_empty.
- rewrite has_fuel_fuels. by iFrame "#∗". }
+ iModIntro.
+ wp_pures.
+
+ rewrite has_fuels_gt_1; last solve_fuel_positive.
+ iApply (wp_fork_nostep _ tid _ _ _ ∅ {[ No ]} {[No := _]} with "[Hno_at Hno_fin] [Hkont] [Hf]");
+ [ set_solver | by apply insert_non_empty | | | | rewrite !fmap_insert fmap_empty // ];
+ [set_solver | |].
+ { iIntros (tid') "!> Hf". iApply (no_spec with "[-]"); last first.
+ + by eauto.
+ + rewrite map_filter_insert_True; last set_solver.
+ rewrite map_filter_empty insert_empty.
+ rewrite has_fuel_fuels. by iFrame "#∗".
+ + lia. }
iNext. iIntros "[Hf _]".
- by iApply "Hkont".
+ iApply "Hkont". iModIntro. iApply (equiv_wand with "Hf"). do 2 f_equiv.
+ rewrite dom_empty_iff_L map_filter_empty_iff.
+ intros ???. set_solver.
Qed.
End proof_start.
diff --git a/fairness/heap_lang/lifting.v b/fairness/heap_lang/lifting.v
index e4e0cc8..b87d31a 100644
--- a/fairness/heap_lang/lifting.v
+++ b/fairness/heap_lang/lifting.v
@@ -130,7 +130,7 @@ Theorem simulation_adequacy Σ {Mdl: FairModel} `{!heapGpreS Σ Mdl} (s: stuckne
(∀ `{!heapGS Σ Mdl},
⊢ |={⊤}=>
frag_model_is s1 -∗
- has_fuels (Σ := Σ) 0%nat (Mdl.(live_roles) s1) (gset_to_gmap (fuel_limit s1) (Mdl.(live_roles) s1))
+ has_fuels (Σ := Σ) 0%nat (gset_to_gmap (fuel_limit s1) (Mdl.(live_roles) s1))
={⊤}=∗ WP e1 @ s; 0%nat; ⊤ {{ v, 0%nat ↦M ∅ }}
) ->
(* The coinductive pure coq proposition given by adequacy *)
@@ -164,7 +164,7 @@ Proof.
- unfold frag_fuel_is. setoid_rewrite map_fmap_singleton.
rewrite -big_opS_own //. iApply (own_proper with "Hfuelf").
rewrite -big_opS_auth_frag. f_equiv. rewrite gset_to_gmap_singletons //.
- - iSplit; first by (iPureIntro; rewrite dom_gset_to_gmap).
+ - rewrite dom_gset_to_gmap. iFrame.
iApply (big_sepS_mono with "H"). iIntros (Ï Hin) "H".
iExists _. iFrame. iPureIntro. apply lookup_gset_to_gmap_Some. done. }
iMod "Hwp". iModIntro.
@@ -254,7 +254,7 @@ Theorem simulation_adequacy_inftraces Σ (Mdl : FairModel) `{!heapGpreS Σ Mdl}
(∀ `{!heapGS Σ Mdl},
⊢ |={⊤}=>
frag_model_is s1 -∗
- has_fuels (Σ := Σ) 0%nat (Mdl.(live_roles) s1) (gset_to_gmap (fuel_limit s1) (Mdl.(live_roles) s1))
+ has_fuels (Σ := Σ) 0%nat (gset_to_gmap (fuel_limit s1) (Mdl.(live_roles) s1))
={⊤}=∗ WP e1 @ s; 0%nat; ⊤ {{ v, 0%nat ↦M ∅ }}
) ->
(* The coinductive pure coq proposition given by adequacy *)
@@ -302,7 +302,7 @@ Theorem simulation_adequacy_traces Σ (Mdl : FairModel) `{!heapGpreS Σ Mdl} (s:
(∀ `{!heapGS Σ Mdl},
⊢ |={⊤}=>
frag_model_is s1 -∗
- has_fuels (Σ := Σ) 0%nat (Mdl.(live_roles) s1) (gset_to_gmap (fuel_limit s1) (Mdl.(live_roles) s1))
+ has_fuels (Σ := Σ) 0%nat (gset_to_gmap (fuel_limit s1) (Mdl.(live_roles) s1))
={⊤}=∗ WP e1 @ s; 0%nat; ⊤ {{ v, 0%nat ↦M ∅ }}
) ->
(* The coinductive pure coq proposition given by adequacy *)
@@ -345,7 +345,7 @@ Theorem simulation_adequacy_model_trace Σ (Mdl : FairModel) `{!heapGpreS Σ Mdl
(∀ `{!heapGS Σ Mdl},
⊢ |={⊤}=>
frag_model_is s1 -∗
- has_fuels (Σ := Σ) 0%nat (Mdl.(live_roles) s1) (gset_to_gmap (fuel_limit s1) (Mdl.(live_roles) s1))
+ has_fuels (Σ := Σ) 0%nat (gset_to_gmap (fuel_limit s1) (Mdl.(live_roles) s1))
={⊤}=∗ WP e1 @ s; 0%nat; ⊤ {{ v, 0%nat ↦M ∅ }}
) ->
(* The coinductive pure coq proposition given by adequacy *)
@@ -373,7 +373,7 @@ Theorem simulation_adequacy_terminate Σ Mdl `{!heapGpreS Σ Mdl} (s: stuckness)
(∀ `{!heapGS Σ Mdl},
⊢ |={⊤}=>
frag_model_is s1 -∗
- has_fuels (Σ := Σ) 0%nat (Mdl.(live_roles) s1) (gset_to_gmap (fuel_limit s1) (Mdl.(live_roles) s1))
+ has_fuels (Σ := Σ) 0%nat (gset_to_gmap (fuel_limit s1) (Mdl.(live_roles) s1))
={⊤}=∗ WP e1 @ s; 0%nat; ⊤ {{ v, 0%nat ↦M ∅ }}
) ->
(* The coinductive pure coq proposition given by adequacy *)
@@ -404,7 +404,7 @@ Theorem simulation_adequacy_terminate_ftm Σ `{FairTerminatingModel Mdl} `{!heap
(∀ `{!heapGS Σ Mdl},
⊢ |={⊤}=>
frag_model_is s1 -∗
- has_fuels (Σ := Σ) 0%nat (Mdl.(live_roles) s1) (gset_to_gmap (fuel_limit s1) (Mdl.(live_roles) s1))
+ has_fuels (Σ := Σ) 0%nat (gset_to_gmap (fuel_limit s1) (Mdl.(live_roles) s1))
={⊤}=∗ WP e1 @ s; 0%nat; ⊤ {{ v, 0%nat ↦M ∅ }}
) ->
(* The coinductive pure coq proposition given by adequacy *)
@@ -605,11 +605,11 @@ Implicit Types l : loc.
Implicit Types tid : nat.
-Lemma wp_lift_pure_step_no_fork tid E E' Φ e1 e2 fs R ϕ:
- R ≠∅ ->
+Lemma wp_lift_pure_step_no_fork tid E E' Φ e1 e2 fs ϕ:
+ fs ≠∅ ->
PureExec Ï• 1 e1 e2 ->
Ï• ->
- (|={E}[E']▷=> has_fuels_S tid R fs ∗ ((has_fuels tid R fs) -∗ WP e2 @ tid; E {{ Φ }}))
+ (|={E}[E']▷=> has_fuels_S tid fs ∗ ((has_fuels tid fs) -∗ WP e2 @ tid; E {{ Φ }}))
⊢ WP e1 @ tid; E {{ Φ }}.
Proof.
intros NnO Hpe HÏ•.
@@ -626,6 +626,7 @@ Proof.
rewrite !app_nil_r.
iDestruct "Hsi" as "(%&Hgh&Hmi)".
iMod (update_no_step_enough_fuel with "Hfuels Hmi") as "H"; eauto.
+ { by intros X%dom_empty_inv_L. }
{ econstructor =>//. by apply fill_step. }
iModIntro.
iDestruct ("H") as (δ2 ℓ [Hlabels Hvse]) "[Hfuels Hmi]".
@@ -648,10 +649,10 @@ Qed.
(* ⊢ WP e1 @ tid; E {{ Φ }}. *)
(* Proof. *)
-Lemma wp_lift_pure_step_no_fork' fs R tid E E' Φ e1 e2:
- R ≠∅ ->
+Lemma wp_lift_pure_step_no_fork' fs tid E E' Φ e1 e2:
+ fs ≠∅ ->
PureExec True 1 e1 e2 ->
- (|={E}[E']▷=> has_fuels_S tid R fs ∗ ((has_fuels tid R fs) -∗ WP e2 @ tid; E {{ Φ }}))
+ (|={E}[E']▷=> has_fuels_S tid fs ∗ ((has_fuels tid fs) -∗ WP e2 @ tid; E {{ Φ }}))
⊢ WP e1 @ tid; E {{ Φ }}.
Proof.
intros. by iApply wp_lift_pure_step_no_fork.
@@ -664,15 +665,15 @@ Lemma wp_lift_pure_step_no_fork_singlerole tid E E' Φ e1 e2 Ï f φ:
Proof.
iIntros (??) "H". rewrite has_fuel_fuels_S.
iApply (wp_lift_pure_step_no_fork {[ Ï := f ]} {[Ï]}); eauto; last first.
- rewrite has_fuel_fuels //. set_solver.
+ rewrite has_fuel_fuels //. apply map_non_empty_singleton.
Qed.
Lemma wp_lift_pure_step_no_fork_take_step s1 s2 tid E E' fs1 fs2 Φ e1 e2 Ï Ï†:
PureExec φ 1 e1 e2 -> φ ->
valid_new_fuelmap fs1 fs2 s1 s2 Ï ->
Mdl.(fmtrans) s1 (Some Ï) s2 ->
- (|={E}[E']▷=> frag_model_is s1 ∗ has_fuels tid (dom fs1) fs1 ∗
- (frag_model_is s2 -∗ (has_fuels tid (dom fs2) fs2 -∗ WP e2 @ tid; E {{ Φ }})))
+ (|={E}[E']▷=> frag_model_is s1 ∗ has_fuels tid fs1 ∗
+ (frag_model_is s2 -∗ (has_fuels tid fs2 -∗ WP e2 @ tid; E {{ Φ }})))
⊢ WP e1 @ tid; E {{ Φ }}.
Proof.
iIntros (Hpe Hφ Hval Htrans).
@@ -700,11 +701,11 @@ Proof.
{ rewrite Hmeq. apply Hval. }
iModIntro. iDestruct "H" as (δ2 ℓ [Hlabels Hvse]) "(Hfuels&Hmod&Hmi)".
iExists δ2, ℓ.
- rewrite Hexend /=. list_simplifier. iFrame "Hgh Hmi".
- repeat iSplit; last done.
+ rewrite Hexend /=. list_simplifier. iFrame "Hgh Hmi".
+ repeat iSplit; last done.
- iPureIntro. destruct â„“ =>//.
- iPureIntro. destruct Hvse as (?&?&? )=>//.
- - iPureIntro. destruct Hvse as (?&?&? )=>//.
+ - iPureIntro. destruct Hvse as (?&?&? )=>//.
- by iSpecialize ("Hkont" with "Hmod Hfuels").
Qed.
@@ -720,7 +721,6 @@ Proof.
iIntros (Hpe Hφ Hroles Hfl Hmdl).
rewrite has_fuel_fuels.
iIntros "H".
- replace ({[Ï]}) with (dom ({[Ï := f1]}: gmap _ _)); last by set_solver.
iApply (wp_lift_pure_step_no_fork_take_step _ _ _ _ _ {[Ï := f1]}
(if decide (Ï âˆˆ live_roles Mdl s2) then {[Ï := f2]} else ∅) with "[H]"); eauto.
- repeat split.
@@ -732,7 +732,7 @@ Proof.
- iMod "H". do 2 iModIntro. iMod "H" as "(Hmod&Hfuels&Hkont)". iModIntro.
iFrame "Hmod Hfuels". iIntros "Hmod Hfuels". iApply ("Hkont" with "Hmod [Hfuels]").
destruct (decide (Ï âˆˆ live_roles Mdl s2)).
- + rewrite dom_singleton_L. rewrite -has_fuel_fuels //.
+ + rewrite -has_fuel_fuels //.
+ iDestruct "Hfuels" as "[Hf _]". rewrite dom_empty_L //.
Qed.
@@ -743,16 +743,17 @@ Lemma wp_lift_pure_step_no_fork_singlerole' tid E E' Φ e1 e2 Ï f:
Proof.
iIntros (?) "H". rewrite has_fuel_fuels_S.
iApply (wp_lift_pure_step_no_fork' {[ Ï := f ]} {[Ï]}); last first.
- rewrite has_fuel_fuels //. set_solver.
+ rewrite has_fuel_fuels //. apply map_non_empty_singleton.
Qed.
(** Fork: Not using Texan triples to avoid some unnecessary [True] *)
Lemma wp_fork_nostep s tid E e Φ R1 R2 fs (Hdisj: R1 ## R2) (Hnemp: fs ≠∅):
- (∀ tid', ▷ (has_fuels tid' R2 (fs ⇂ R2) -∗ WP e @ s; tid'; ⊤ {{ _, tid' ↦M ∅ }})) -∗
- ▷ (has_fuels tid R1 (fs ⇂ R1) ={E}=∗ Φ (LitV LitUnit)) -∗
- has_fuels_S tid (R1 ∪ R2) fs -∗ WP Fork e @ s; tid; E {{ Φ }}.
+ R1 ∪ R2 = dom fs ->
+ (∀ tid', ▷ (has_fuels tid' (fs ⇂ R2) -∗ WP e @ s; tid'; ⊤ {{ _, tid' ↦M ∅ }})) -∗
+ ▷ (has_fuels tid (fs ⇂ R1) ={E}=∗ Φ (LitV LitUnit)) -∗
+ has_fuels_S tid fs -∗ WP Fork e @ s; tid; E {{ Φ }}.
Proof.
- iIntros "He HΦ Htid". iApply wp_lift_atomic_head_step; [done|].
+ iIntros (Hunioneq) "He HΦ Htid". iApply wp_lift_atomic_head_step; [done|].
iIntros (extr auxtr K tp1 tp2 σ1 Hvalex Hexend Hloc) "(% & Hsi & Hmi)".
iMod (update_fork_split R1 R2 _
(tp1 ++ ectx_language.fill K (Val $ LitV LitUnit) :: tp2 ++ [e]) fs _ _ _ e _ σ1 with "Htid Hmi") as
@@ -808,11 +809,11 @@ Qed.
(* TODO *)
-Lemma wp_allocN_seq_nostep s tid E v n R fs:
- R ≠∅ ->
+Lemma wp_allocN_seq_nostep s tid E v n fs:
+ fs ≠∅ ->
0 < n →
- {{{ has_fuels_S tid R fs }}} AllocN (Val $ LitV $ LitInt $ n) (Val v) @ s; tid; E
- {{{ l, RET LitV (LitLoc l); has_fuels tid R fs ∗ [∗ list] i ∈ seq 0 (Z.to_nat n),
+ {{{ has_fuels_S tid fs }}} AllocN (Val $ LitV $ LitInt $ n) (Val v) @ s; tid; E
+ {{{ l, RET LitV (LitLoc l); has_fuels tid fs ∗ [∗ list] i ∈ seq 0 (Z.to_nat n),
(l +ₗ (i : nat)) ↦ v ∗ meta_token (l +ₗ (i : nat)) ⊤ }}}.
Proof.
iIntros (HnO Hn Φ) "HfuelS HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
@@ -825,6 +826,7 @@ Proof.
{ apply heap_array_map_disjoint.
rewrite replicate_length Z2Nat.id ?Hexend; auto with lia. }
iMod (update_no_step_enough_fuel _ _ with "HfuelS Hmi") as (δ2 ℓ) "([%Hlabel %Hvse] & Hfuel & Hmi)" =>//.
+ { by intros ?%dom_empty_inv_L. }
{ rewrite Hexend. apply head_locale_step. by econstructor. }
iModIntro; iExists δ2, ℓ.
rewrite Hexend //=. iFrame "Hmi Hsi".
@@ -834,17 +836,17 @@ Proof.
+ iApply (heap_array_to_seq_meta with "Hm"). by rewrite replicate_length.
Qed.
-Lemma wp_alloc_nostep s tid E v R fs :
- R ≠∅ ->
- {{{ has_fuels_S tid R fs }}} Alloc (Val v) @ s; tid; E {{{ l, RET LitV (LitLoc l); l ↦ v ∗ meta_token l ⊤ ∗ has_fuels tid R fs }}}.
+Lemma wp_alloc_nostep s tid E v fs :
+ fs ≠∅ ->
+ {{{ has_fuels_S tid fs }}} Alloc (Val v) @ s; tid; E {{{ l, RET LitV (LitLoc l); l ↦ v ∗ meta_token l ⊤ ∗ has_fuels tid fs }}}.
Proof.
iIntros (? Φ) "HfuelS HΦ". iApply (wp_allocN_seq_nostep with "HfuelS"); auto with lia.
iIntros "!>" (l) "/= (? & ? & _)". rewrite loc_add_0. by iApply "HΦ"; iFrame.
Qed.
-Lemma wp_load_nostep s tid E l q v R fs:
- R ≠∅ ->
- {{{ ▷ l ↦{q} v ∗ has_fuels_S tid R fs }}} Load (Val $ LitV $ LitLoc l) @ s; tid; E {{{ RET v; l ↦{q} v ∗ has_fuels tid R fs }}}.
+Lemma wp_load_nostep s tid E l q v fs:
+ fs ≠∅ ->
+ {{{ ▷ l ↦{q} v ∗ has_fuels_S tid fs }}} Load (Val $ LitV $ LitLoc l) @ s; tid; E {{{ RET v; l ↦{q} v ∗ has_fuels tid fs }}}.
Proof.
iIntros (? Φ) "[>Hl HfuelS] HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (extr atr K tp1 tp2 σ1 Hval Hexend Hloc) "(% & Hsi & Hmi) !>".
@@ -852,6 +854,7 @@ Proof.
iSplit; first by rewrite Hexend // in Hheap; eauto. iIntros "!>" (e2 σ2 efs Hstep).
rewrite Hexend in Hheap. inv_head_step.
iMod (update_no_step_enough_fuel with "HfuelS Hmi") as (δ2 ℓ) "([%Hlabels %Hvse] & Hfuel & Hmod)" =>//.
+ { by intros ?%dom_empty_inv_L. }
{ rewrite Hexend. apply head_locale_step. by econstructor. }
iModIntro; iExists _,_.
rewrite Hexend //=. iFrame "Hsi Hmod".
@@ -859,10 +862,10 @@ Proof.
iApply "HΦ". iFrame.
Qed.
-Lemma wp_store_nostep s tid E l v' v R fs:
- R ≠∅ ->
- {{{ ▷ l ↦ v' ∗ has_fuels_S tid R fs }}} Store (Val $ LitV (LitLoc l)) (Val v) @ s; tid; E
- {{{ RET LitV LitUnit; l ↦ v ∗ has_fuels tid R fs }}}.
+Lemma wp_store_nostep s tid E l v' v fs:
+ fs ≠∅ ->
+ {{{ ▷ l ↦ v' ∗ has_fuels_S tid fs }}} Store (Val $ LitV (LitLoc l)) (Val v) @ s; tid; E
+ {{{ RET LitV LitUnit; l ↦ v ∗ has_fuels tid fs }}}.
Proof.
iIntros (? Φ) "[>Hl HfuelS] HΦ".
iApply wp_lift_atomic_head_step_no_fork; auto.
@@ -872,11 +875,12 @@ Proof.
rewrite Hexend in Hheap. inv_head_step.
iMod (@gen_heap_update with "Hsi Hl") as "[Hsi Hl]".
iMod (update_no_step_enough_fuel with "HfuelS Hmi") as (δ2 ℓ) "([%Hlabels %Hvse] & Hfuel & Hmod)" =>//.
+ { by intros ?%dom_empty_inv_L. }
{ rewrite Hexend. apply head_locale_step. by econstructor. }
iModIntro; iExists _,_.
rewrite Hexend //=. iFrame "Hsi Hmod".
do 2 (iSplit=>//).
- iApply "HΦ". iFrame.
+ iApply "HΦ". iFrame.
Qed.
Lemma wp_cmpxchg_fail_step_singlerole s tid Ï (f1 f2: nat) s1 s2 E l q v' v1 v2:
@@ -911,7 +915,7 @@ Proof.
{ iPureIntro. simpl in *. split =>//. }
iFrame. iSplit; first done. iApply "HΦ". iFrame.
destruct (decide (Ï âˆˆ live_roles Mdl s2)).
- + rewrite has_fuel_fuels dom_singleton_L //.
+ + rewrite has_fuel_fuels //.
+ iDestruct "Hfuel" as "[?_]". rewrite dom_empty_L //.
Qed.
@@ -949,7 +953,7 @@ Proof.
{ iPureIntro. simpl in *. split =>//. }
iFrame. iSplit; first done. iApply "HΦ". iFrame.
destruct (decide (Ï âˆˆ live_roles Mdl s2)).
- + rewrite has_fuel_fuels dom_singleton_L //.
+ + rewrite has_fuel_fuels //.
+ iDestruct "Hfuel" as "[?_]". rewrite dom_empty_L //.
Qed.
diff --git a/fairness/heap_lang/proofmode.v b/fairness/heap_lang/proofmode.v
new file mode 100644
index 0000000..aeaac0a
--- /dev/null
+++ b/fairness/heap_lang/proofmode.v
@@ -0,0 +1,1023 @@
+From iris.proofmode Require Import coq_tactics reduction spec_patterns.
+From iris.proofmode Require Export tactics.
+From trillium.program_logic Require Import atomic.
+From trillium.fairness.heap_lang Require Export tactics lifting. (* derived_laws. *)
+From trillium.fairness.heap_lang Require Import notation.
+From iris.prelude Require Import options.
+Import uPred.
+
+Lemma tac_wp_expr_eval `{!heapGS Σ Mdl} Δ tid E Φ e e' :
+ (∀ (e'':=e'), e = e'') →
+ envs_entails Δ (WP e' @ tid; E {{ Φ }}) → envs_entails Δ (WP e @ tid; E {{ Φ }}).
+Proof. by intros ->. Qed.
+
+Tactic Notation "wp_expr_eval" tactic3(t) :=
+ iStartProof;
+ lazymatch goal with
+ | |- envs_entails _ (wp ?s ?E ?locale ?e ?Q) =>
+ notypeclasses refine (tac_wp_expr_eval _ _ _ _ e _ _ _);
+ [let x := fresh in intros x; t; unfold x; notypeclasses refine eq_refl|]
+ | _ => fail "wp_expr_eval: not a 'wp'"
+ end.
+Ltac wp_expr_simpl := wp_expr_eval simpl.
+
+Lemma tac_wp_pure_helper `{!heapGS Σ Mdl} tid E K e1 e2 fs φ n Φ :
+ fs ≠∅ ->
+ PureExec φ n e1 e2 →
+ φ →
+ ( ▷^n (has_fuels tid fs -∗ WP (fill K e2) @ tid; E {{ Φ }})) -∗
+ has_fuels_plus n tid fs -∗
+ WP (fill K e1) @ tid; E {{ Φ }}.
+Proof.
+ intros Hne HPE Hφ. specialize (HPE Hφ).
+ revert e1 e2 fs Hne HPE. induction n; intros e1 e2 fs Hne HPE.
+ { inversion HPE. rewrite has_fuel_fuels_plus_0. by simplify_eq. }
+
+ inversion HPE; simplify_eq.
+
+ iIntros "H Hf".
+ rewrite has_fuels_plus_split_S.
+
+ iApply (wp_lift_pure_step_no_fork _ _ _ _ _ _ ((λ m : nat, (n + m)%nat) <$> fs)) =>//.
+ { by intros ?%fmap_empty_inv. }
+ { econstructor =>//; [ by eapply pure_step_ctx | constructor ]. }
+ iModIntro; iFrame. do 2 iModIntro.
+ iIntros "Hf".
+ iApply (IHn _ _ _ with "[H] [Hf]") => //.
+Qed.
+
+Lemma equiv_wand {Σ} (P Q: iProp Σ):
+ P ≡ Q ->
+ P -∗ Q.
+Proof. by intros ->. Qed.
+
+Lemma maps_gt_n {Mdl} (fs: gmap (fmrole Mdl) _) n:
+ (∀ Ï f, fs !! Ï = Some f -> f >= n)%nat ->
+ fs = (λ m, n + m)%nat <$> ((λ m, m - n)%nat <$> fs).
+Proof.
+ intros Hgt.
+ rewrite -leibniz_equiv_iff => Ï.
+ rewrite -map_fmap_compose !lookup_fmap.
+ destruct (fs !! Ï) as [f|] eqn:? =>//=. f_equiv.
+ assert (f >= n)%nat by eauto.
+ apply leibniz_equiv_iff. lia.
+Qed.
+
+Lemma has_fuels_gt_n `{!heapGS Σ Mdl} (fs: gmap (fmrole Mdl) _) n tid:
+ (∀ Ï f, fs !! Ï = Some f -> f >= n)%nat ->
+ has_fuels tid fs ⊣⊢ has_fuels tid ((λ m, n + m)%nat <$> ((λ m, m - n)%nat <$> fs)).
+Proof. intros ?. rewrite {1}(maps_gt_n fs n) //. Qed.
+
+Lemma has_fuels_gt_1 `{!heapGS Σ Mdl} (fs: gmap (fmrole Mdl) _) tid:
+ (∀ Ï f, fs !! Ï = Some f -> f >= 1)%nat ->
+ has_fuels tid fs ⊣⊢ has_fuels_S tid (((λ m, m - 1)%nat <$> fs)).
+Proof. intros ?. by rewrite has_fuels_gt_n //. Qed.
+
+Lemma tac_wp_pure_helper_2 `{!heapGS Σ Mdl} tid E K e1 e2 fs φ n Φ :
+ (∀ Ï f, fs !! Ï = Some f -> f >= n)%nat ->
+ fs ≠∅ ->
+ PureExec φ n e1 e2 →
+ φ →
+ ( ▷^n ((has_fuels tid ((λ m, m - n)%nat <$> fs)) -∗ WP (fill K e2) @ tid; E {{ Φ }})) -∗
+ has_fuels tid fs -∗
+ WP (fill K e1) @ tid; E {{ Φ }}.
+Proof.
+ iIntros (Hfs Hne Hpe Hphi) "H Hf".
+ rewrite (has_fuels_gt_n fs n) //.
+ iApply (tac_wp_pure_helper with "H [Hf]") =>//.
+ by intros ?%fmap_empty_inv.
+Qed.
+
+(* Upstream? *)
+Lemma maybe_into_latersN_envs_dom {PROP} (Γ Δ: envs PROP) n i:
+ MaybeIntoLaterNEnvs n Γ Δ →
+ envs_lookup i Γ = None →
+ envs_lookup i Δ = None.
+Proof.
+ intros [??] ?. destruct Γ as [Γp Γs]. destruct Δ as [Δp Δs].
+ simpl.
+ destruct (env_lookup i Δp) eqn:Hlk.
+ - assert (HnN: env_lookup i Γp ≠None).
+ { intros contra%transform_intuitionistic_env_dom.
+ rewrite /= in contra. simplify_eq. }
+ rewrite not_eq_None_Some in HnN. destruct HnN as [? Hlk'].
+ by rewrite /= Hlk' in H.
+ - rewrite /= in H.
+ destruct (env_lookup i Γp); [simplify_eq|].
+ destruct (env_lookup i Γs) eqn:Heq =>//.
+ apply transform_spatial_env_dom in Heq.
+ by rewrite Heq.
+Qed.
+
+Lemma maybe_into_latersN_envs_wf {PROP} (Γ Δ: envs PROP) n:
+ MaybeIntoLaterNEnvs n Γ Δ →
+ envs_wf Γ →
+ envs_wf Δ.
+Proof.
+ intros [??] [? ? Hdisj]. destruct Γ as [Γp Γs]. destruct Δ as [Δp Δs]. constructor.
+ - by apply transform_intuitionistic_env_wf.
+ - by apply transform_spatial_env_wf.
+ - intros i. destruct (Hdisj i);
+ [ by left; apply transform_intuitionistic_env_dom |
+ by right; apply transform_spatial_env_dom].
+Qed.
+
+Lemma envs_delete_wf {PROP} i p (Δ: envs PROP) : envs_wf Δ → envs_wf (envs_delete true i p Δ).
+Proof.
+ intros [?? Hdisj]; destruct Δ. constructor.
+ - destruct p; simpl; [by apply env_delete_wf|done].
+ - destruct p; simpl; [done|by apply env_delete_wf].
+ - intro j. destruct (Hdisj j).
+ + left. destruct p; [|done]. simpl in *.
+ destruct (decide (i = j)) as [->|?].
+ * rewrite env_lookup_env_delete //.
+ * rewrite env_lookup_env_delete_ne //.
+ + right. destruct p; [done|].
+ destruct (decide (i = j)) as [->|?].
+ * rewrite env_lookup_env_delete //.
+ * rewrite env_lookup_env_delete_ne //.
+Qed.
+
+Lemma tac_wp_pure `{!heapGS Σ Mdl} Δ Δ'other tid E i K e1 e2 φ n Φ fs :
+ (∀ (Ï : fmrole Mdl) (f : nat), fs !! Ï = Some f → (f ≥ n)%nat) ->
+ fs ≠∅ ->
+ PureExec φ n e1 e2 →
+ φ →
+ envs_lookup i Δ = Some (false, has_fuels tid fs)%I →
+ let Δother := envs_delete true i false Δ in
+ MaybeIntoLaterNEnvs n Δother Δ'other →
+ let Δ' := envs_snoc Δ'other false i (has_fuels tid ((λ m, m - n)%nat <$> fs)) in
+ envs_entails Δ' (WP (fill K e2) @ tid; E {{ Φ }}) →
+ envs_entails Δ (WP (fill K e1) @ tid; E {{ Φ }}).
+Proof.
+ rewrite envs_entails_unseal=> ???.
+ intros ?? Δother Hlater Δ' Hccl.
+ iIntros "H".
+ iAssert (⌜envs_wf ΔâŒ)%I as %Hwf.
+ { unfold of_envs, of_envs', envs_wf. iDestruct "H" as "[%H1 _]". by iPureIntro. }
+
+ rewrite envs_lookup_sound // /= -/Δother. iDestruct "H" as "[H1 H2]".
+ rewrite into_laterN_env_sound.
+
+ iApply (tac_wp_pure_helper_2 with "[H2] [H1]") =>//.
+ iNext. simpl. iIntros "H". iApply Hccl.
+ rewrite /Δ' /= (envs_snoc_sound Δ'other false i); first by iApply "H2".
+ eapply maybe_into_latersN_envs_dom =>//. rewrite /Δother.
+ eapply envs_lookup_envs_delete =>//.
+Qed.
+
+
+Lemma tac_wp_value_nofupd `{!heapGS Σ Mdl} Δ tid E Φ v :
+ envs_entails Δ (Φ v) → envs_entails Δ (WP (Val v) @ tid; E {{ Φ }}).
+Proof. rewrite envs_entails_unseal=> ->. by apply wp_value. Qed.
+
+Lemma tac_wp_value `{!heapGS Σ Mdl} Δ tid E (Φ : val → iPropI Σ) v :
+ envs_entails Δ (|={E}=> Φ v) → envs_entails Δ (WP (Val v) @ tid; E {{ Φ }}).
+Proof. rewrite envs_entails_unseal=> ->. iIntros "?". by iApply wp_value_fupd. Qed.
+
+(** Simplify the goal if it is [WP] of a value.
+ If the postcondition already allows a fupd, do not add a second one.
+ But otherwise, *do* add a fupd. This ensures that all the lemmas applied
+ here are bidirectional, so we never will make a goal unprovable. *)
+Ltac wp_value_head :=
+ lazymatch goal with
+ | |- envs_entails _ (wp ?s ?E (Val _) (λ _, fupd ?E _ _)) =>
+ eapply tac_wp_value_nofupd
+ | |- envs_entails _ (wp ?s ?E (Val _) (λ _, wp _ ?E _ _ _)) =>
+ eapply tac_wp_value_nofupd
+ | |- envs_entails _ (wp ?s ?E _ (Val _) _) =>
+ eapply tac_wp_value
+ end.
+
+Ltac wp_finish :=
+ wp_expr_simpl; (* simplify occurences of subst/fill *)
+ try wp_value_head; (* in case we have reached a value, get rid of the WP *)
+ pm_prettify. (* prettify â–·s caused by [MaybeIntoLaterNEnvs] and
+ λs caused by wp_value *)
+
+Ltac solve_vals_compare_safe :=
+ (* The first branch is for when we have [vals_compare_safe] in the context. *)
+(* The other two branches are for when either one of the branches reduces to *)
+(* [True] or we have it in the context. *)
+ fast_done || (left; fast_done) || (right; fast_done).
+
+Tactic Notation "solve_pure_exec" :=
+ lazymatch goal with
+ | |- PureExec _ _ ?e _ =>
+ let e := eval simpl in e in
+ reshape_expr e ltac:(fun K e' =>
+ eapply (pure_exec_fill K _ _ e');
+ [iSolveTC (* PureExec *)
+ (* |try solve_vals_compare_safe (* The pure condition for PureExec -- handles trivial goals, including [vals_compare_safe] *) *)
+ ])
+ || fail "failed :("
+ end.
+
+
+Global Hint Extern 0 (PureExec _ _ _ _) => solve_pure_exec: core.
+Global Hint Extern 0 (vals_compare_safe _ _) => solve_vals_compare_safe: core.
+
+
+Ltac solve_fuel_positive :=
+ unfold singletonM, map_singleton; intros ??;
+ repeat progress match goal with
+ | [|- <[ ?x := _ ]> _ !! ?r = Some _ -> _] =>
+ destruct (decide (x = r)) as [->| ?];
+ [rewrite lookup_insert; intros ?; simplify_eq; lia |
+ rewrite lookup_insert_ne; [ try done | done]]
+ end.
+Tactic Notation "wp_pure" open_constr(efoc) :=
+ let solve_fuel _ :=
+ let fs := match goal with |- _ = Some (_, has_fuels _ ?fs) => fs end in
+ iAssumptionCore || fail "wp_pure: cannot find" fs in
+ iStartProof;
+ rewrite ?has_fuel_fuels;
+ lazymatch goal with
+ | |- envs_entails _ (wp ?s ?E ?locale ?e ?Q) =>
+ let e := eval simpl in e in
+ reshape_expr e ltac:(fun K e' =>
+ unify e' efoc;
+ eapply (tac_wp_pure _ _ _ _ _ K e');
+ [
+ |
+ | iSolveTC
+ | trivial
+ | let fs := match goal with |- _ = Some (_, has_fuels _ ?fs) => fs end in
+ iAssumptionCore || fail "wp_pures: cannot find" fs
+ |iSolveTC
+ | pm_reduce;
+ rewrite ?[in has_fuels _ _]fmap_insert [in has_fuels _ _]/= ?[in has_fuels _ _]fmap_empty;
+ wp_finish
+ ] ; [ solve_fuel_positive
+ | try apply map_non_empty_singleton; try apply insert_non_empty; try done
+ |])
+ || fail "wp_pure: cannot find" efoc "in" e "or" efoc "is not a redex"
+ | _ => fail "wp_pure: not a 'wp'"
+ end.
+
+(* TODO: do this in one go, without [repeat]. *)
+Ltac wp_pures :=
+ iStartProof;
+ first [ (* The `;[]` makes sure that no side-condition magically spawns. *)
+ progress repeat (wp_pure _; [])
+ | wp_finish (* In case wp_pure never ran, make sure we do the usual cleanup. *)
+ ].
+
+(** Unlike [wp_pures], the tactics [wp_rec] and [wp_lam] should also reduce
+lambdas/recs that are hidden behind a definition, i.e. they should use
+[AsRecV_recv] as a proper instance instead of a [Hint Extern].
+
+We achieve this by putting [AsRecV_recv] in the current environment so that it
+can be used as an instance by the typeclass resolution system. We then perform
+the reduction, and finally we clear this new hypothesis. *)
+Tactic Notation "wp_rec" :=
+ let H := fresh in
+ assert (H := AsRecV_recv);
+ wp_pure (App _ _);
+ clear H.
+
+Tactic Notation "wp_if" := wp_pure (If _ _ _).
+Tactic Notation "wp_if_true" := wp_pure (If (LitV (LitBool true)) _ _).
+Tactic Notation "wp_if_false" := wp_pure (If (LitV (LitBool false)) _ _).
+Tactic Notation "wp_unop" := wp_pure (UnOp _ _).
+Tactic Notation "wp_binop" := wp_pure (BinOp _ _ _).
+Tactic Notation "wp_op" := wp_unop || wp_binop.
+Tactic Notation "wp_lam" := wp_rec.
+Tactic Notation "wp_let" := wp_pure (Rec BAnon (BNamed _) _); wp_lam.
+Tactic Notation "wp_seq" := wp_pure (Rec BAnon BAnon _); wp_lam.
+Tactic Notation "wp_proj" := wp_pure (Fst _) || wp_pure (Snd _).
+Tactic Notation "wp_case" := wp_pure (Case _ _ _).
+Tactic Notation "wp_match" := wp_case; wp_pure (Rec _ _ _); wp_lam.
+Tactic Notation "wp_inj" := wp_pure (InjL _) || wp_pure (InjR _).
+Tactic Notation "wp_pair" := wp_pure (Pair _ _).
+Tactic Notation "wp_closure" := wp_pure (Rec _ _ _).
+
+Lemma tac_wp_bind `{!heapGS Σ Mdl} K Δ s E Φ e f :
+ f = (λ e, fill K e) → (* as an eta expanded hypothesis so that we can `simpl` it *)
+ envs_entails Δ (WP e @ s; E {{ v, WP f (Val v) @ s; E {{ Φ }} }})%I →
+ envs_entails Δ (WP fill K e @ s; E {{ Φ }}).
+Proof. rewrite envs_entails_unseal=> -> ->. by apply: wp_bind. Qed.
+
+Ltac wp_bind_core K :=
+ lazymatch eval hnf in K with
+ | [] => idtac
+ | _ => eapply (tac_wp_bind K); [simpl; reflexivity|reduction.pm_prettify]
+ end.
+
+Tactic Notation "wp_bind" open_constr(efoc) :=
+ iStartProof;
+ lazymatch goal with
+ | |- envs_entails _ (wp ?s ?E ?locale ?e ?Q) =>
+ first [ reshape_expr e ltac:(fun K e' => unify e' efoc; wp_bind_core K)
+ | fail 1 "wp_bind: cannot find" efoc "in" e ]
+ | _ => fail "wp_bind: not a 'wp'"
+ end.
+
+(** Heap tactics *)
+Section heap.
+Context `{!heapGS Σ Mdl}.
+Implicit Types P Q : iProp Σ.
+Implicit Types Φ : val → iProp Σ.
+Implicit Types Δ : envs (uPredI (iResUR Σ)).
+Implicit Types v : val.
+Implicit Types tid : locale heap_lang.
+
+(* Lemma tac_wp_allocN Δ Δ' s E j K v n Φ : *)
+(* (0 < n)%Z → *)
+(* MaybeIntoLaterNEnvs 1 Δ Δ' → *)
+(* (∀ l, *)
+(* match envs_app false (Esnoc Enil j (heap_array l (DfracOwn 1) (replicate (Z.to_nat n) v))) Δ' with *)
+(* | Some Δ'' => *)
+(* envs_entails Δ'' (WP fill K (Val $ LitV $ LitLoc l) @ s; E {{ Φ }}) *)
+(* | None => False *)
+(* end) → *)
+(* envs_entails Δ (WP fill K (AllocN (Val $ LitV $ LitInt n) (Val v)) @ s; E {{ Φ }}). *)
+(* Proof. *)
+(* rewrite envs_entails_eq=> ? ? HΔ. *)
+(* rewrite -wp_bind. eapply wand_apply; first exact: wp_allocN. *)
+(* rewrite left_id into_laterN_env_sound; apply later_mono, forall_intro=> l. *)
+(* specialize (HΔ l). *)
+(* destruct (envs_app _ _ _) as [Δ''|] eqn:HΔ'; [ | contradiction ]. *)
+(* rewrite envs_app_sound //; simpl. *)
+(* apply wand_intro_l. by rewrite (sep_elim_l (l ↦∗ _)%I) right_id wand_elim_r. *)
+(* Qed. *)
+(* Lemma tac_twp_allocN Δ s E j K v n Φ : *)
+(* (0 < n)%Z → *)
+(* (∀ l, *)
+(* match envs_app false (Esnoc Enil j (array l (DfracOwn 1) (replicate (Z.to_nat n) v))) Δ with *)
+(* | Some Δ' => *)
+(* envs_entails Δ' (WP fill K (Val $ LitV $ LitLoc l) @ s; E [{ Φ }]) *)
+(* | None => False *)
+(* end) → *)
+(* envs_entails Δ (WP fill K (AllocN (Val $ LitV $ LitInt n) (Val v)) @ s; E [{ Φ }]). *)
+(* Proof. *)
+(* rewrite envs_entails_eq=> ? HΔ. *)
+(* rewrite -twp_bind. eapply wand_apply; first exact: twp_allocN. *)
+(* rewrite left_id. apply forall_intro=> l. *)
+(* specialize (HΔ l). *)
+(* destruct (envs_app _ _ _) as [Δ'|] eqn:HΔ'; [ | contradiction ]. *)
+(* rewrite envs_app_sound //; simpl. *)
+(* apply wand_intro_l. by rewrite (sep_elim_l (l ↦∗ _)%I) right_id wand_elim_r. *)
+(* Qed. *)
+
+(* Lemma tac_wp_alloc Δ Δ' s E j K v Φ : *)
+(* MaybeIntoLaterNEnvs 1 Δ Δ' → *)
+(* (∀ l, *)
+(* match envs_app false (Esnoc Enil j (l ↦ v)) Δ' with *)
+(* | Some Δ'' => *)
+(* envs_entails Δ'' (WP fill K (Val $ LitV l) @ s; E {{ Φ }}) *)
+(* | None => False *)
+(* end) → *)
+(* envs_entails Δ (WP fill K (Alloc (Val v)) @ s; E {{ Φ }}). *)
+(* Proof. *)
+(* rewrite envs_entails_eq=> ? HΔ. *)
+(* rewrite -wp_bind. eapply wand_apply; first exact: wp_alloc. *)
+(* rewrite left_id into_laterN_env_sound; apply later_mono, forall_intro=> l. *)
+(* specialize (HΔ l). *)
+(* destruct (envs_app _ _ _) as [Δ''|] eqn:HΔ'; [ | contradiction ]. *)
+(* rewrite envs_app_sound //; simpl. *)
+(* apply wand_intro_l. by rewrite (sep_elim_l (l ↦ v)%I) right_id wand_elim_r. *)
+(* Qed. *)
+(* Lemma tac_twp_alloc Δ s E j K v Φ : *)
+(* (∀ l, *)
+(* match envs_app false (Esnoc Enil j (l ↦ v)) Δ with *)
+(* | Some Δ' => *)
+(* envs_entails Δ' (WP fill K (Val $ LitV $ LitLoc l) @ s; E [{ Φ }]) *)
+(* | None => False *)
+(* end) → *)
+(* envs_entails Δ (WP fill K (Alloc (Val v)) @ s; E [{ Φ }]). *)
+(* Proof. *)
+(* rewrite envs_entails_eq=> HΔ. *)
+(* rewrite -twp_bind. eapply wand_apply; first exact: twp_alloc. *)
+(* rewrite left_id. apply forall_intro=> l. *)
+(* specialize (HΔ l). *)
+(* destruct (envs_app _ _ _) as [Δ''|] eqn:HΔ'; [ | contradiction ]. *)
+(* rewrite envs_app_sound //; simpl. *)
+(* apply wand_intro_l. by rewrite (sep_elim_l (l ↦ v)%I) right_id wand_elim_r. *)
+(* Qed. *)
+
+(* Lemma tac_wp_free Δ Δ' s E i K l v Φ : *)
+(* MaybeIntoLaterNEnvs 1 Δ Δ' → *)
+(* envs_lookup i Δ' = Some (false, l ↦ v)%I → *)
+(* (let Δ'' := envs_delete false i false Δ' in *)
+(* envs_entails Δ'' (WP fill K (Val $ LitV LitUnit) @ s; E {{ Φ }})) → *)
+(* envs_entails Δ (WP fill K (Free (LitV l)) @ s; E {{ Φ }}). *)
+(* Proof. *)
+(* rewrite envs_entails_eq=> ? Hlk Hfin. *)
+(* rewrite -wp_bind. eapply wand_apply; first exact: wp_free. *)
+(* rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl. *)
+(* rewrite -Hfin wand_elim_r (envs_lookup_sound' _ _ _ _ _ Hlk). *)
+(* apply later_mono, sep_mono_r, wand_intro_r. rewrite right_id //. *)
+(* Qed. *)
+(* Lemma tac_twp_free Δ s E i K l v Φ : *)
+(* envs_lookup i Δ = Some (false, l ↦ v)%I → *)
+(* (let Δ' := envs_delete false i false Δ in *)
+(* envs_entails Δ' (WP fill K (Val $ LitV LitUnit) @ s; E [{ Φ }])) → *)
+(* envs_entails Δ (WP fill K (Free (LitV l)) @ s; E [{ Φ }]). *)
+(* Proof. *)
+(* rewrite envs_entails_eq=> Hlk Hfin. *)
+(* rewrite -twp_bind. eapply wand_apply; first exact: twp_free. *)
+(* rewrite envs_lookup_split //; simpl. *)
+(* rewrite -Hfin wand_elim_r (envs_lookup_sound' _ _ _ _ _ Hlk). *)
+(* apply sep_mono_r, wand_intro_r. rewrite right_id //. *)
+(* Qed. *)
+
+Lemma tac_wp_load K fs tid Δ Δ'other E i j l q v Φ :
+ (∀ (Ï : fmrole Mdl) (f : nat), fs !! Ï = Some f → (f ≥ 1)%nat) ->
+ fs ≠∅ ->
+ i ≠j ->
+ envs_lookup i Δ = Some (false, has_fuels tid fs)%I →
+ let Δother := envs_delete true i false Δ in
+ MaybeIntoLaterNEnvs 1 Δother Δ'other →
+ envs_lookup j Δ'other = Some (false, l ↦{q} v)%I →
+ let Δ' := envs_snoc Δ'other false i (has_fuels tid ((λ m, m - 1)%nat <$> fs)) in
+ envs_entails Δ' (WP fill K (Val v) @ tid; E {{ Φ }}) →
+ envs_entails Δ (WP fill K (Load (LitV l)) @ tid; E {{ Φ }}).
+Proof.
+ intros ?? Hij ?.
+ rewrite envs_entails_unseal=> Δother ?? Δ' Hccl.
+ rewrite -wp_bind.
+ iIntros "H".
+ iAssert (⌜envs_wf ΔâŒ)%I as %Hwf.
+ { unfold of_envs, of_envs', envs_wf. iDestruct "H" as "[% _]". by iPureIntro. }
+
+ rewrite (envs_lookup_sound _ i) // /= -/Δother. iDestruct "H" as "[H1 H2]".
+ rewrite into_laterN_env_sound /=.
+
+ rewrite (envs_lookup_sound _ j) // /=.
+ pose Δ'' := envs_delete true j false Δ'other. rewrite -/Δ''.
+ iDestruct "H2" as "[H2 H3]".
+
+ rewrite has_fuels_gt_1 //.
+ iApply (wp_load_nostep with "[H1 H2]"); [| iFrame |]; [by intros ?%fmap_empty_inv|].
+ iIntros "!> [Hl Hf]". iApply Hccl. rewrite /Δ' /=.
+ iApply (envs_snoc_sound Δ'other false i with "[H3 Hl] [Hf]") =>//.
+ - rewrite maybe_into_latersN_envs_dom // /Δother.
+ erewrite envs_lookup_envs_delete =>//.
+ - iApply (envs_lookup_sound_2 Δ'other) =>//; [| by iFrame].
+ eapply maybe_into_latersN_envs_wf =>//.
+ rewrite /Δother. by apply envs_delete_wf.
+Qed.
+
+
+Lemma tac_wp_store K fs tid Δ Δ'other E i j l v v' Φ :
+ (∀ (Ï : fmrole Mdl) (f : nat), fs !! Ï = Some f → (f ≥ 1)%nat) ->
+ fs ≠∅ ->
+ i ≠j ->
+ envs_lookup i Δ = Some (false, has_fuels tid fs)%I →
+ let Δother := envs_delete true i false Δ in
+ MaybeIntoLaterNEnvs 1 Δother Δ'other →
+ envs_lookup j Δ'other = Some (false, (l ↦ v)%I) ->
+ match envs_simple_replace j false (Esnoc Enil j (l ↦ v')%I) Δ'other with
+ | Some Δ'other2 =>
+ let Δ' := envs_snoc Δ'other2 false i (has_fuels tid ((λ m, m - 1)%nat <$> fs)) in
+ envs_lookup i Δ'other2 = None (* redondent but easier than proving it. *) ∧
+ envs_entails Δ' (WP fill K (Val $ LitV LitUnit) @ tid; E {{ Φ }})
+ | None => False
+ end →
+ envs_entails Δ (WP fill K (Store (LitV l) (Val v')) @ tid; E {{ Φ }}).
+Proof.
+ intros ?? Hij ?.
+ rewrite envs_entails_unseal=> Δother ??.
+ destruct (envs_simple_replace j false (Esnoc Enil j (l ↦ v'))%I Δ'other) as [Δ'other2|] eqn:Heq; last done.
+ move=> /= [Hhack Hccl].
+
+ rewrite -wp_bind.
+ iIntros "H".
+ iAssert (⌜envs_wf ΔâŒ)%I as %Hwf.
+ { unfold of_envs, of_envs', envs_wf. iDestruct "H" as "[% _]". by iPureIntro. }
+
+ rewrite (envs_lookup_sound _ i) // /= -/Δother. iDestruct "H" as "[H1 H2]".
+ rewrite into_laterN_env_sound /=.
+
+ rewrite (envs_lookup_sound _ j) //.
+ pose Δ'' := envs_delete true j false Δ'other. rewrite -/Δ''.
+ iDestruct "H2" as "[H2 H3]".
+
+ rewrite has_fuels_gt_1 //.
+ iApply (wp_store_nostep with "[H1 H2]"); [| iFrame |]; [by intros ?%fmap_empty_inv|].
+ iIntros "!> [Hl Hf]".
+ set Δ' := envs_snoc Δ'other2 false i (has_fuels tid ((λ m, m - 1)%nat <$> fs)).
+ fold Δ' in Hccl.
+
+ iApply Hccl. unfold Δ'.
+ iApply (envs_snoc_sound Δ'other2 false i with "[H3 Hl] [Hf]") =>//.
+ rewrite envs_simple_replace_sound' //=. simpl.
+ iApply "H3". iFrame.
+Qed.
+
+End heap.
+
+Tactic Notation "wp_load" :=
+ let solve_fuel _ :=
+ let fs := match goal with |- _ = Some (_, has_fuels _ ?fs) => fs end in
+ iAssumptionCore || fail "wp_load: cannot find" fs in
+ let solve_mapsto _ :=
+ let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
+ iAssumptionCore || fail "wp_load: cannot find" l "↦ ?" in
+ wp_pures;
+ lazymatch goal with
+ | |- envs_entails _ (wp ?s ?E ?locale ?e ?Q) =>
+ first
+ [reshape_expr e ltac:(fun K e' => eapply (tac_wp_load K))
+ |fail 1 "wp_load: cannot find 'Load' in" e];
+ [ (* dealt with later *)
+ |
+ |
+ | let fs := match goal with |- _ = Some (_, has_fuels _ ?fs) => fs end in
+ iAssumptionCore || fail "wp_load: cannot find" fs
+ | iSolveTC
+ | let fs := match goal with |- _ = Some (_, ?l ↦{_} _)%I => l end in
+ iAssumptionCore || fail "wp_load: cannot find" fs
+ | pm_reduce;
+ rewrite ?[in has_fuels _ _]fmap_insert [in has_fuels _ _]/= ?[in has_fuels _ _]fmap_empty;
+ wp_finish
+ ]; [ solve_fuel_positive
+ | try apply map_non_empty_singleton; try apply insert_non_empty; try done
+ | intros ?; by simplify_eq
+ |
+ ]
+ | _ => fail "wp_load: not a 'wp'"
+ end.
+
+Tactic Notation "wp_store" :=
+ let solve_fuel _ :=
+ let fs := match goal with |- _ = Some (_, has_fuels _ ?fs) => fs end in
+ iAssumptionCore || fail "wp_store: cannot find" fs in
+ let solve_mapsto _ :=
+ let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
+ iAssumptionCore || fail "wp_store: cannot find" l "↦ ?" in
+ wp_pures;
+ lazymatch goal with
+ | |- envs_entails _ (wp ?s ?E ?locale ?e ?Q) =>
+ first
+ [reshape_expr e ltac:(fun K e' => eapply (tac_wp_store K))
+ |fail 1 "wp_load: cannot find 'Load' in" e];
+ [ (* dealt with later *)
+ |
+ |
+ | let fs := match goal with |- _ = Some (_, has_fuels _ ?fs) => fs end in
+ iAssumptionCore || fail "wp_store: cannot find" fs
+ | iSolveTC
+ | let fs := match goal with |- _ = Some (_, ?l ↦{_} _)%I => l end in
+ iAssumptionCore || fail "wp_store: cannot find" fs
+ | split; [done | pm_reduce;
+ rewrite ?[in has_fuels _ _]fmap_insert [in has_fuels _ _]/= ?[in has_fuels _ _]fmap_empty;
+ wp_finish]
+ ]; [ solve_fuel_positive
+ | try apply map_non_empty_singleton; try apply insert_non_empty; try done
+ | intros ?; by simplify_eq
+ |
+ ]
+ | _ => fail "wp_store: not a 'wp'"
+ end.
+(*
+Lemma tac_wp_xchg Δ Δ' s E i K l v v' Φ :
+ MaybeIntoLaterNEnvs 1 Δ Δ' →
+ envs_lookup i Δ' = Some (false, l ↦ v)%I →
+ match envs_simple_replace i false (Esnoc Enil i (l ↦ v')) Δ' with
+ | Some Δ'' => envs_entails Δ'' (WP fill K (Val $ v) @ s; E {{ Φ }})
+ | None => False
+ end →
+ envs_entails Δ (WP fill K (Xchg (LitV l) (Val v')) @ s; E {{ Φ }}).
+Proof.
+ rewrite envs_entails_eq=> ???.
+ destruct (envs_simple_replace _ _ _) as [Δ''|] eqn:HΔ''; [ | contradiction ].
+ rewrite -wp_bind. eapply wand_apply; first by eapply wp_xchg.
+ rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
+ rewrite right_id.
+ by apply later_mono, sep_mono_r, wand_mono.
+Qed.
+Lemma tac_twp_xchg Δ s E i K l v v' Φ :
+ envs_lookup i Δ = Some (false, l ↦ v)%I →
+ match envs_simple_replace i false (Esnoc Enil i (l ↦ v')) Δ with
+ | Some Δ' => envs_entails Δ' (WP fill K (Val $ v) @ s; E [{ Φ }])
+ | None => False
+ end →
+ envs_entails Δ (WP fill K (Xchg (LitV l) v') @ s; E [{ Φ }]).
+Proof.
+ rewrite envs_entails_eq. intros.
+ destruct (envs_simple_replace _ _ _) as [Δ''|] eqn:HΔ''; [ | contradiction ].
+ rewrite -twp_bind. eapply wand_apply; first by eapply twp_xchg.
+ rewrite envs_simple_replace_sound //; simpl.
+ rewrite right_id. by apply sep_mono_r, wand_mono.
+Qed.
+
+Lemma tac_wp_cmpxchg Δ Δ' s E i K l v v1 v2 Φ :
+ MaybeIntoLaterNEnvs 1 Δ Δ' →
+ envs_lookup i Δ' = Some (false, l ↦ v)%I →
+ vals_compare_safe v v1 →
+ match envs_simple_replace i false (Esnoc Enil i (l ↦ v2)) Δ' with
+ | Some Δ'' =>
+ v = v1 →
+ envs_entails Δ'' (WP fill K (Val $ PairV v (LitV $ LitBool true)) @ s; E {{ Φ }})
+ | None => False
+ end →
+ (v ≠v1 →
+ envs_entails Δ' (WP fill K (Val $ PairV v (LitV $ LitBool false)) @ s; E {{ Φ }})) →
+ envs_entails Δ (WP fill K (CmpXchg (LitV l) (Val v1) (Val v2)) @ s; E {{ Φ }}).
+Proof.
+ rewrite envs_entails_eq=> ??? Hsuc Hfail.
+ destruct (envs_simple_replace _ _ _ _) as [Δ''|] eqn:HΔ''; [ | contradiction ].
+ destruct (decide (v = v1)) as [Heq|Hne].
+ - rewrite -wp_bind. eapply wand_apply.
+ { eapply wp_cmpxchg_suc; eauto. }
+ rewrite into_laterN_env_sound -later_sep /= {1}envs_simple_replace_sound //; simpl.
+ apply later_mono, sep_mono_r. rewrite right_id. apply wand_mono; auto.
+ - rewrite -wp_bind. eapply wand_apply.
+ { eapply wp_cmpxchg_fail; eauto. }
+ rewrite into_laterN_env_sound -later_sep /= {1}envs_lookup_split //; simpl.
+ apply later_mono, sep_mono_r. apply wand_mono; auto.
+Qed.
+Lemma tac_twp_cmpxchg Δ s E i K l v v1 v2 Φ :
+ envs_lookup i Δ = Some (false, l ↦ v)%I →
+ vals_compare_safe v v1 →
+ match envs_simple_replace i false (Esnoc Enil i (l ↦ v2)) Δ with
+ | Some Δ' =>
+ v = v1 →
+ envs_entails Δ' (WP fill K (Val $ PairV v (LitV $ LitBool true)) @ s; E [{ Φ }])
+ | None => False
+ end →
+ (v ≠v1 →
+ envs_entails Δ (WP fill K (Val $ PairV v (LitV $ LitBool false)) @ s; E [{ Φ }])) →
+ envs_entails Δ (WP fill K (CmpXchg (LitV l) v1 v2) @ s; E [{ Φ }]).
+Proof.
+ rewrite envs_entails_eq=> ?? Hsuc Hfail.
+ destruct (envs_simple_replace _ _ _ _) as [Δ''|] eqn:HΔ''; [ | contradiction ].
+ destruct (decide (v = v1)) as [Heq|Hne].
+ - rewrite -twp_bind. eapply wand_apply.
+ { eapply twp_cmpxchg_suc; eauto. }
+ rewrite /= {1}envs_simple_replace_sound //; simpl.
+ apply sep_mono_r. rewrite right_id. apply wand_mono; auto.
+ - rewrite -twp_bind. eapply wand_apply.
+ { eapply twp_cmpxchg_fail; eauto. }
+ rewrite /= {1}envs_lookup_split //; simpl.
+ apply sep_mono_r. apply wand_mono; auto.
+Qed.
+
+Lemma tac_wp_cmpxchg_fail Δ Δ' s E i K l q v v1 v2 Φ :
+ MaybeIntoLaterNEnvs 1 Δ Δ' →
+ envs_lookup i Δ' = Some (false, l ↦{q} v)%I →
+ v ≠v1 → vals_compare_safe v v1 →
+ envs_entails Δ' (WP fill K (Val $ PairV v (LitV $ LitBool false)) @ s; E {{ Φ }}) →
+ envs_entails Δ (WP fill K (CmpXchg (LitV l) v1 v2) @ s; E {{ Φ }}).
+Proof.
+ rewrite envs_entails_eq=> ?????.
+ rewrite -wp_bind. eapply wand_apply; first exact: wp_cmpxchg_fail.
+ rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
+ by apply later_mono, sep_mono_r, wand_mono.
+Qed.
+Lemma tac_twp_cmpxchg_fail Δ s E i K l q v v1 v2 Φ :
+ envs_lookup i Δ = Some (false, l ↦{q} v)%I →
+ v ≠v1 → vals_compare_safe v v1 →
+ envs_entails Δ (WP fill K (Val $ PairV v (LitV $ LitBool false)) @ s; E [{ Φ }]) →
+ envs_entails Δ (WP fill K (CmpXchg (LitV l) v1 v2) @ s; E [{ Φ }]).
+Proof.
+ rewrite envs_entails_eq. intros. rewrite -twp_bind.
+ eapply wand_apply; first exact: twp_cmpxchg_fail.
+ (* [//] solves some evars and enables further simplification. *)
+ rewrite envs_lookup_split /= // /=. by do 2 f_equiv.
+Qed.
+
+Lemma tac_wp_cmpxchg_suc Δ Δ' s E i K l v v1 v2 Φ :
+ MaybeIntoLaterNEnvs 1 Δ Δ' →
+ envs_lookup i Δ' = Some (false, l ↦ v)%I →
+ v = v1 → vals_compare_safe v v1 →
+ match envs_simple_replace i false (Esnoc Enil i (l ↦ v2)) Δ' with
+ | Some Δ'' =>
+ envs_entails Δ'' (WP fill K (Val $ PairV v (LitV $ LitBool true)) @ s; E {{ Φ }})
+ | None => False
+ end →
+ envs_entails Δ (WP fill K (CmpXchg (LitV l) v1 v2) @ s; E {{ Φ }}).
+Proof.
+ rewrite envs_entails_eq=> ?????; subst.
+ destruct (envs_simple_replace _ _ _) as [Δ''|] eqn:HΔ''; [ | contradiction ].
+ rewrite -wp_bind. eapply wand_apply.
+ { eapply wp_cmpxchg_suc; eauto. }
+ rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
+ rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
+Qed.
+Lemma tac_twp_cmpxchg_suc Δ s E i K l v v1 v2 Φ :
+ envs_lookup i Δ = Some (false, l ↦ v)%I →
+ v = v1 → vals_compare_safe v v1 →
+ match envs_simple_replace i false (Esnoc Enil i (l ↦ v2)) Δ with
+ | Some Δ' =>
+ envs_entails Δ' (WP fill K (Val $ PairV v (LitV $ LitBool true)) @ s; E [{ Φ }])
+ | None => False
+ end →
+ envs_entails Δ (WP fill K (CmpXchg (LitV l) v1 v2) @ s; E [{ Φ }]).
+Proof.
+ rewrite envs_entails_eq=>????; subst.
+ destruct (envs_simple_replace _ _ _) as [Δ''|] eqn:HΔ''; [ | contradiction ].
+ rewrite -twp_bind. eapply wand_apply.
+ { eapply twp_cmpxchg_suc; eauto. }
+ rewrite envs_simple_replace_sound //; simpl.
+ rewrite right_id. by apply sep_mono_r, wand_mono.
+Qed.
+
+Lemma tac_wp_faa Δ Δ' s E i K l z1 z2 Φ :
+ MaybeIntoLaterNEnvs 1 Δ Δ' →
+ envs_lookup i Δ' = Some (false, l ↦ LitV z1)%I →
+ match envs_simple_replace i false (Esnoc Enil i (l ↦ LitV (LitInt (z1 + z2)))) Δ' with
+ | Some Δ'' => envs_entails Δ'' (WP fill K (Val $ LitV z1) @ s; E {{ Φ }})
+ | None => False
+ end →
+ envs_entails Δ (WP fill K (FAA (LitV l) (LitV z2)) @ s; E {{ Φ }}).
+Proof.
+ rewrite envs_entails_eq=> ???.
+ destruct (envs_simple_replace _ _ _) as [Δ''|] eqn:HΔ''; [ | contradiction ].
+ rewrite -wp_bind. eapply wand_apply; first exact: (wp_faa _ _ _ z1 z2).
+ rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
+ rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
+Qed.
+Lemma tac_twp_faa Δ s E i K l z1 z2 Φ :
+ envs_lookup i Δ = Some (false, l ↦ LitV z1)%I →
+ match envs_simple_replace i false (Esnoc Enil i (l ↦ LitV (LitInt (z1 + z2)))) Δ with
+ | Some Δ' => envs_entails Δ' (WP fill K (Val $ LitV z1) @ s; E [{ Φ }])
+ | None => False
+ end →
+ envs_entails Δ (WP fill K (FAA (LitV l) (LitV z2)) @ s; E [{ Φ }]).
+Proof.
+ rewrite envs_entails_eq=> ??.
+ destruct (envs_simple_replace _ _ _) as [Δ'|] eqn:HΔ'; [ | contradiction ].
+ rewrite -twp_bind. eapply wand_apply; first exact: (twp_faa _ _ _ z1 z2).
+ rewrite envs_simple_replace_sound //; simpl.
+ rewrite right_id. by apply sep_mono_r, wand_mono.
+Qed.
+End heap.
+
+(** The tactic [wp_apply_core lem tac_suc tac_fail] evaluates [lem] to a
+hypothesis [H] that can be applied, and then runs [wp_bind_core K; tac_suc H]
+for every possible evaluation context [K].
+
+- The tactic [tac_suc] should do [iApplyHyp H] to actually apply the hypothesis,
+ but can perform other operations in addition (see [wp_apply] and [awp_apply]
+ below).
+- The tactic [tac_fail cont] is called when [tac_suc H] fails for all evaluation
+ contexts [K], and can perform further operations before invoking [cont] to
+ try again.
+
+TC resolution of [lem] premises happens *after* [tac_suc H] got executed. *)
+Ltac wp_apply_core lem tac_suc tac_fail := first
+ [iPoseProofCore lem as false (fun H =>
+ lazymatch goal with
+ | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
+ reshape_expr e ltac:(fun K e' =>
+ wp_bind_core K; tac_suc H)
+ | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
+ reshape_expr e ltac:(fun K e' =>
+ twp_bind_core K; tac_suc H)
+ | _ => fail 1 "wp_apply: not a 'wp'"
+ end)
+ |tac_fail ltac:(fun _ => wp_apply_core lem tac_suc tac_fail)
+ |let P := type of lem in
+ fail "wp_apply: cannot apply" lem ":" P ].
+
+Tactic Notation "wp_apply" open_constr(lem) :=
+ wp_apply_core lem ltac:(fun H => iApplyHyp H; try iNext; try wp_expr_simpl)
+ ltac:(fun cont => fail).
+Tactic Notation "wp_smart_apply" open_constr(lem) :=
+ wp_apply_core lem ltac:(fun H => iApplyHyp H; try iNext; try wp_expr_simpl)
+ ltac:(fun cont => wp_pure _; []; cont ()).
+
+(** Tactic tailored for atomic triples: the first, simple one just runs
+[iAuIntro] on the goal, as atomic triples always have an atomic update as their
+premise. The second one additionaly does some framing: it gets rid of [Hs] from
+the context, which is intended to be the non-laterable assertions that iAuIntro
+would choke on. You get them all back in the continuation of the atomic
+operation. *)
+Tactic Notation "awp_apply" open_constr(lem) :=
+ wp_apply_core lem ltac:(fun H => iApplyHyp H) ltac:(fun cont => fail);
+ last iAuIntro.
+Tactic Notation "awp_apply" open_constr(lem) "without" constr(Hs) :=
+ (* Convert "list of hypothesis" into specialization pattern. *)
+ let Hs := words Hs in
+ let Hs := eval vm_compute in (INamed <$> Hs) in
+ wp_apply_core lem
+ ltac:(fun H =>
+ iApply (wp_frame_wand with
+ [SGoal $ SpecGoal GSpatial false [] Hs false]); [iAccu|iApplyHyp H])
+ ltac:(fun cont => fail);
+ last iAuIntro.
+
+Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
+ let Htmp := iFresh in
+ let finish _ :=
+ first [intros l | fail 1 "wp_alloc:" l "not fresh"];
+ pm_reduce;
+ lazymatch goal with
+ | |- False => fail 1 "wp_alloc:" H "not fresh"
+ | _ => iDestructHyp Htmp as H; wp_finish
+ end in
+ wp_pures;
+ (** The code first tries to use allocation lemma for a single reference,
+ ie, [tac_wp_alloc] (respectively, [tac_twp_alloc]).
+ If that fails, it tries to use the lemma [tac_wp_allocN]
+ (respectively, [tac_twp_allocN]) for allocating an array.
+ Notice that we could have used the array allocation lemma also for single
+ references. However, that would produce the resource l ↦∗ [v] instead of
+ l ↦ v for single references. These are logically equivalent assertions
+ but are not equal. *)
+ lazymatch goal with
+ | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
+ let process_single _ :=
+ first
+ [reshape_expr e ltac:(fun K e' => eapply (tac_wp_alloc _ _ _ _ Htmp K))
+ |fail 1 "wp_alloc: cannot find 'Alloc' in" e];
+ [iSolveTC
+ |finish ()]
+ in
+ let process_array _ :=
+ first
+ [reshape_expr e ltac:(fun K e' => eapply (tac_wp_allocN _ _ _ _ Htmp K))
+ |fail 1 "wp_alloc: cannot find 'Alloc' in" e];
+ [idtac|iSolveTC
+ |finish ()]
+ in (process_single ()) || (process_array ())
+ | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
+ let process_single _ :=
+ first
+ [reshape_expr e ltac:(fun K e' => eapply (tac_twp_alloc _ _ _ Htmp K))
+ |fail 1 "wp_alloc: cannot find 'Alloc' in" e];
+ finish ()
+ in
+ let process_array _ :=
+ first
+ [reshape_expr e ltac:(fun K e' => eapply (tac_twp_allocN _ _ _ Htmp K))
+ |fail 1 "wp_alloc: cannot find 'Alloc' in" e];
+ [idtac
+ |finish ()]
+ in (process_single ()) || (process_array ())
+ | _ => fail "wp_alloc: not a 'wp'"
+ end.
+
+Tactic Notation "wp_alloc" ident(l) :=
+ wp_alloc l as "?".
+
+Tactic Notation "wp_free" :=
+ let solve_mapsto _ :=
+ let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
+ iAssumptionCore || fail "wp_free: cannot find" l "↦ ?" in
+ wp_pures;
+ lazymatch goal with
+ | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
+ first
+ [reshape_expr e ltac:(fun K e' => eapply (tac_wp_free _ _ _ _ _ K))
+ |fail 1 "wp_free: cannot find 'Free' in" e];
+ [iSolveTC
+ |solve_mapsto ()
+ |pm_reduce; wp_finish]
+ | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
+ first
+ [reshape_expr e ltac:(fun K e' => eapply (tac_twp_free _ _ _ _ K))
+ |fail 1 "wp_free: cannot find 'Free' in" e];
+ [solve_mapsto ()
+ |pm_reduce; wp_finish]
+ | _ => fail "wp_free: not a 'wp'"
+ end.
+
+Tactic Notation "wp_store" :=
+ let solve_mapsto _ :=
+ let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
+ iAssumptionCore || fail "wp_store: cannot find" l "↦ ?" in
+ wp_pures;
+ lazymatch goal with
+ | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
+ first
+ [reshape_expr e ltac:(fun K e' => eapply (tac_wp_store _ _ _ _ _ K))
+ |fail 1 "wp_store: cannot find 'Store' in" e];
+ [iSolveTC
+ |solve_mapsto ()
+ |pm_reduce; first [wp_seq|wp_finish]]
+ | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
+ first
+ [reshape_expr e ltac:(fun K e' => eapply (tac_twp_store _ _ _ _ K))
+ |fail 1 "wp_store: cannot find 'Store' in" e];
+ [solve_mapsto ()
+ |pm_reduce; first [wp_seq|wp_finish]]
+ | _ => fail "wp_store: not a 'wp'"
+ end.
+
+Tactic Notation "wp_xchg" :=
+ let solve_mapsto _ :=
+ let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
+ iAssumptionCore || fail "wp_xchg: cannot find" l "↦ ?" in
+ wp_pures;
+ lazymatch goal with
+ | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
+ first
+ [reshape_expr e ltac:(fun K e' => eapply (tac_wp_xchg _ _ _ _ _ K))
+ |fail 1 "wp_xchg: cannot find 'Xchg' in" e];
+ [iSolveTC
+ |solve_mapsto ()
+ |pm_reduce; first [wp_seq|wp_finish]]
+ | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
+ first
+ [reshape_expr e ltac:(fun K e' => eapply (tac_twp_xchg _ _ _ _ K))
+ |fail 1 "wp_xchg: cannot find 'Xchg' in" e];
+ [solve_mapsto ()
+ |pm_reduce; first [wp_seq|wp_finish]]
+ | _ => fail "wp_xchg: not a 'wp'"
+ end.
+
+Tactic Notation "wp_cmpxchg" "as" simple_intropattern(H1) "|" simple_intropattern(H2) :=
+ let solve_mapsto _ :=
+ let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
+ iAssumptionCore || fail "wp_cmpxchg: cannot find" l "↦ ?" in
+ wp_pures;
+ lazymatch goal with
+ | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
+ first
+ [reshape_expr e ltac:(fun K e' => eapply (tac_wp_cmpxchg _ _ _ _ _ K))
+ |fail 1 "wp_cmpxchg: cannot find 'CmpXchg' in" e];
+ [iSolveTC
+ |solve_mapsto ()
+ |try solve_vals_compare_safe
+ |pm_reduce; intros H1; wp_finish
+ |intros H2; wp_finish]
+ | |- envs_entails _ (twp ?E ?e ?Q) =>
+ first
+ [reshape_expr e ltac:(fun K e' => eapply (tac_twp_cmpxchg _ _ _ _ K))
+ |fail 1 "wp_cmpxchg: cannot find 'CmpXchg' in" e];
+ [solve_mapsto ()
+ |try solve_vals_compare_safe
+ |pm_reduce; intros H1; wp_finish
+ |intros H2; wp_finish]
+ | _ => fail "wp_cmpxchg: not a 'wp'"
+ end.
+
+Tactic Notation "wp_cmpxchg_fail" :=
+ let solve_mapsto _ :=
+ let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
+ iAssumptionCore || fail "wp_cmpxchg_fail: cannot find" l "↦ ?" in
+ wp_pures;
+ lazymatch goal with
+ | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
+ first
+ [reshape_expr e ltac:(fun K e' => eapply (tac_wp_cmpxchg_fail _ _ _ _ _ K))
+ |fail 1 "wp_cmpxchg_fail: cannot find 'CmpXchg' in" e];
+ [iSolveTC
+ |solve_mapsto ()
+ |try (simpl; congruence) (* value inequality *)
+ |try solve_vals_compare_safe
+ |wp_finish]
+ | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
+ first
+ [reshape_expr e ltac:(fun K e' => eapply (tac_twp_cmpxchg_fail _ _ _ _ K))
+ |fail 1 "wp_cmpxchg_fail: cannot find 'CmpXchg' in" e];
+ [solve_mapsto ()
+ |try (simpl; congruence) (* value inequality *)
+ |try solve_vals_compare_safe
+ |wp_finish]
+ | _ => fail "wp_cmpxchg_fail: not a 'wp'"
+ end.
+
+Tactic Notation "wp_cmpxchg_suc" :=
+ let solve_mapsto _ :=
+ let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
+ iAssumptionCore || fail "wp_cmpxchg_suc: cannot find" l "↦ ?" in
+ wp_pures;
+ lazymatch goal with
+ | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
+ first
+ [reshape_expr e ltac:(fun K e' => eapply (tac_wp_cmpxchg_suc _ _ _ _ _ K))
+ |fail 1 "wp_cmpxchg_suc: cannot find 'CmpXchg' in" e];
+ [iSolveTC
+ |solve_mapsto ()
+ |try (simpl; congruence) (* value equality *)
+ |try solve_vals_compare_safe
+ |pm_reduce; wp_finish]
+ | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
+ first
+ [reshape_expr e ltac:(fun K e' => eapply (tac_twp_cmpxchg_suc _ _ _ _ K))
+ |fail 1 "wp_cmpxchg_suc: cannot find 'CmpXchg' in" e];
+ [solve_mapsto ()
+ |try (simpl; congruence) (* value equality *)
+ |try solve_vals_compare_safe
+ |pm_reduce; wp_finish]
+ | _ => fail "wp_cmpxchg_suc: not a 'wp'"
+ end.
+
+Tactic Notation "wp_faa" :=
+ let solve_mapsto _ :=
+ let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
+ iAssumptionCore || fail "wp_faa: cannot find" l "↦ ?" in
+ wp_pures;
+ lazymatch goal with
+ | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
+ first
+ [reshape_expr e ltac:(fun K e' => eapply (tac_wp_faa _ _ _ _ _ K))
+ |fail 1 "wp_faa: cannot find 'FAA' in" e];
+ [iSolveTC
+ |solve_mapsto ()
+ |pm_reduce; wp_finish]
+ | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
+ first
+ [reshape_expr e ltac:(fun K e' => eapply (tac_twp_faa _ _ _ _ K))
+ |fail 1 "wp_faa: cannot find 'FAA' in" e];
+ [solve_mapsto ()
+ |pm_reduce; wp_finish]
+ | _ => fail "wp_faa: not a 'wp'"
+ end.
+
+*)
diff --git a/fairness/resources.v b/fairness/resources.v
index a40f5c2..58a4d79 100644
--- a/fairness/resources.v
+++ b/fairness/resources.v
@@ -40,6 +40,29 @@ Proof. solve_inG. Qed.
Notation "f ⇂ R" := (filter (λ '(k,v), k ∈ R) f) (at level 30).
+Lemma dom_domain_restrict `{Countable X} {A} (f: gmap X A) (R: gset X):
+ R ⊆ dom f ->
+ dom (f ⇂ R) = R.
+Proof.
+ intros ?. apply dom_filter_L.
+ intros i; split; [|set_solver].
+ intros Hin. assert (Hin': i ∈ dom f) by set_solver.
+ apply elem_of_dom in Hin' as [??]. set_solver.
+Qed.
+
+Lemma dom_domain_restrict_union_l `{Countable X} {A} (f: gmap X A) R1 R2:
+ R1 ∪ R2 ⊆ dom f ->
+ dom (f ⇂ R1) = R1.
+Proof.
+ intros ?. apply dom_domain_restrict. set_solver.
+Qed.
+Lemma dom_domain_restrict_union_r `{Countable X} {A} (f: gmap X A) R1 R2:
+ R1 ∪ R2 ⊆ dom f ->
+ dom (f ⇂ R2) = R2.
+Proof.
+ intros ?. apply dom_domain_restrict. set_solver.
+Qed.
+
Section bigop_utils.
Context `{Monoid M o}.
Context `{Countable K}.
@@ -47,10 +70,10 @@ Section bigop_utils.
Lemma big_opMS (g: gset K) (P: K -> M):
([^ o set] x ∈ g, P x) ≡ [^ o map] x ↦ y ∈ (mapset_car g), P x.
Proof.
- rewrite big_op.big_opS_unseal /big_op.big_opS_def /elements /gset_elements /mapset_elements.
- rewrite big_op.big_opM_unseal /big_op.big_opM_def.
+ rewrite big_opS_elements /elements /gset_elements /mapset_elements.
+ rewrite big_opM_map_to_list.
destruct g as [g]. simpl. rewrite big_opL_fmap.
- f_equiv. by intros x [y ?].
+ f_equiv.
Qed.
End bigop_utils.
@@ -256,30 +279,63 @@ Section model_state_lemmas.
Definition has_fuel (ζ: locale Λ) (Ï: Role) (f: nat): iProp Σ :=
ζ ↦m Ï âˆ— Ï â†¦F f.
- Definition has_fuels (ζ: locale Λ) (R: gset Role) (fs: gmap Role nat): iProp Σ :=
- ζ ↦M R ∗ ⌜R = dom fs⌠∗ [∗ set] Ï âˆˆ R, ∃ f, ⌜fs !! Ï = Some f⌠∧ Ï â†¦F f.
+ Definition has_fuels (ζ: locale Λ) (fs: gmap Role nat): iProp Σ :=
+ ζ ↦M dom fs ∗ [∗ set] Ï âˆˆ dom fs, ∃ f, ⌜fs !! Ï = Some f⌠∧ Ï â†¦F f.
+
+ #[global] Instance has_fuels_proper :
+ Proper ((≡) ==> (≡) ==> (≡)) (has_fuels).
+ Proof. solve_proper. Qed.
+
+ #[global] Instance has_fuels_timeless (ζ: locale Λ) (fs: gmap Role nat):
+ Timeless (has_fuels ζ fs).
+ Proof. rewrite /has_fuels. apply _. Qed.
Lemma has_fuel_fuels (ζ: locale Λ) (Ï: Role) (f: nat):
- has_fuel ζ Ï f ⊣⊢ has_fuels ζ {[ Ï ]} {[ Ï := f ]}.
+ has_fuel ζ Ï f ⊣⊢ has_fuels ζ {[ Ï := f ]}.
Proof.
rewrite /has_fuel /has_fuels. iSplit.
- - iIntros "[Hζ HÏ]". rewrite big_sepS_singleton. iFrame.
- iSplit; first (iPureIntro; set_solver).
+ - iIntros "[Hζ HÏ]". rewrite dom_singleton_L big_sepS_singleton. iFrame.
iExists f. iFrame. iPureIntro. by rewrite lookup_singleton.
- - iIntros "(?&H)". rewrite big_sepS_singleton. iFrame.
+ - iIntros "(?&H)". rewrite dom_singleton_L big_sepS_singleton. iFrame.
iDestruct "H" as (?) "H". rewrite lookup_singleton.
- iDestruct "H" as "[% [% ?]]". by simplify_eq.
+ iDestruct "H" as "[% ?]". by simplify_eq.
Qed.
- Definition has_fuels_S (ζ: locale Λ) (R: gset Role) (fs: gmap Role nat): iProp Σ :=
- has_fuels ζ R (fmap S fs).
+ Definition has_fuels_S (ζ: locale Λ) (fs: gmap Role nat): iProp Σ :=
+ has_fuels ζ (fmap S fs).
+
+ Definition has_fuels_plus (n: nat) (ζ: locale Λ) (fs: gmap Role nat): iProp Σ :=
+ has_fuels ζ (fmap (fun m => n+m) fs).
Lemma has_fuel_fuels_S (ζ: locale Λ) (Ï: Role) (f: nat):
- has_fuel ζ Ï (S f) ⊣⊢ has_fuels_S ζ {[ Ï ]} {[ Ï := f ]}.
+ has_fuel ζ Ï (S f) ⊣⊢ has_fuels_S ζ {[ Ï := f ]}.
Proof.
rewrite has_fuel_fuels /has_fuels_S map_fmap_singleton //.
Qed.
+ Lemma has_fuel_fuels_plus_1 (ζ: locale Λ) fs:
+ has_fuels_plus 1 ζ fs ⊣⊢ has_fuels_S ζ fs.
+ Proof.
+ rewrite /has_fuels_plus /has_fuels_S. do 2 f_equiv.
+ intros m m' ->. apply leibniz_equiv_iff. lia.
+ Qed.
+
+ Lemma has_fuel_fuels_plus_0 (ζ: locale Λ) fs:
+ has_fuels_plus 0 ζ fs ⊣⊢ has_fuels ζ fs.
+ Proof.
+ rewrite /has_fuels_plus /=. f_equiv. intros ?.
+ rewrite lookup_fmap. apply leibniz_equiv_iff.
+ destruct (fs !! i) eqn:Heq; rewrite Heq //.
+ Qed.
+
+ Lemma has_fuels_plus_split_S n (ζ: locale Λ) fs:
+ has_fuels_plus (S n) ζ fs ⊣⊢ has_fuels_S ζ ((λ m, n + m) <$> fs).
+ Proof.
+ rewrite /has_fuels_plus /has_fuels_S. f_equiv.
+ rewrite -map_fmap_compose /= => Ï.
+ rewrite !lookup_fmap //.
+ Qed.
+
Lemma frag_mapping_same ζ M R:
auth_mapping_is M -∗ ζ ↦M R -∗ ⌜ M !! ζ = Some R âŒ.
Proof.
@@ -349,9 +405,7 @@ Section model_state_lemmas.
Context `{EqDecision (expr Λ)}.
Lemma update_model δ δ1 δ2:
- auth_model_is δ1 -∗
- frag_model_is δ2 ==∗
- auth_model_is δ ∗ frag_model_is δ.
+ auth_model_is δ1 -∗ frag_model_is δ2 ==∗ auth_model_is δ ∗ frag_model_is δ.
Proof.
iIntros "H1 H2". iCombine "H1 H2" as "H".
iMod (own_update with "H") as "[??]" ; eauto.
@@ -360,9 +414,7 @@ Section model_state_lemmas.
Qed.
Lemma model_agree s1 s2:
- auth_model_is s1 -∗
- frag_model_is s2 -∗
- ⌜ s1 = s2 âŒ.
+ auth_model_is s1 -∗ frag_model_is s2 -∗ ⌜ s1 = s2 âŒ.
Proof.
iIntros "Ha Hf".
by iDestruct (own_valid_2 with "Ha Hf") as
@@ -370,18 +422,14 @@ Section model_state_lemmas.
Qed.
Lemma model_agree' δ1 s2 n:
- model_state_interp n δ1 -∗
- frag_model_is s2 -∗
- ⌜ ls_under δ1 = s2 âŒ.
+ model_state_interp n δ1 -∗ frag_model_is s2 -∗ ⌜ ls_under δ1 = s2 âŒ.
Proof.
iIntros "Hsi Hs2". iDestruct "Hsi" as (?) "(_&_&_&_&Hs1)".
iApply (model_agree with "Hs1 Hs2").
Qed.
Lemma update_fuel_delete Ï f F:
- auth_fuel_is F -∗
- Ï â†¦F f ==∗
- auth_fuel_is (delete Ï F).
+ auth_fuel_is F -∗ Ï â†¦F f ==∗ auth_fuel_is (delete Ï F).
Proof.
iIntros "Hafuel Hfuel".
iCombine "Hafuel Hfuel" as "H".
@@ -420,7 +468,8 @@ Section model_state_lemmas.
specialize (Heq Ï). rewrite lookup_op Hlk !lookup_fmap in Heq.
destruct (decide (Ï âˆˆ dom F)) as [HF|HF]; last first.
{ exfalso. apply not_elem_of_dom in HF. rewrite HF //= in Heq.
- destruct (fs !! Ï) eqn:Hfs; rewrite Hfs in Heq; inversion Heq. }
+ destruct (fs !! Ï) eqn:Hfs; inversion Heq as [A S D G Habs|A Habs];
+ setoid_rewrite -> Hfs in Habs; by compute in Habs. }
destruct (decide (Ï âˆˆ dom fs)) as [Hfs|Hfs].
{ exfalso. apply elem_of_dom in Hfs as [f' Hlk'].
rewrite Hlk' /= in Heq.
@@ -437,9 +486,9 @@ Section model_state_lemmas.
(fs ≠∅) ->
(dom fs' ∖ dom fs ∩ dom F = ∅) ->
auth_fuel_is F -∗
- ([∗ map] Ï â†¦ f ∈ fs, Ï â†¦F f) ==∗
- auth_fuel_is (fuel_apply fs' F LR) ∗
- ([∗ map] Ï â†¦ f ∈ fs', Ï â†¦F f).
+ ([∗ map] Ï â†¦ f ∈ fs, Ï â†¦F f) ==∗
+ auth_fuel_is (fuel_apply fs' F LR) ∗
+ ([∗ map] Ï â†¦ f ∈ fs', Ï â†¦F f).
Proof.
iIntros (? Hnotemp Hdisj) "Hafuel Hfuel".
rewrite {1}/frag_fuel_is -big_opM_own //.
@@ -512,10 +561,7 @@ Section model_state_lemmas.
Qed.
Lemma update_mapping ζ (R' : gset $ fmrole Mdl) (R: gset (fmrole Mdl)) M:
- auth_mapping_is M -∗
- ζ ↦M R ==∗
- auth_mapping_is (<[ ζ := R' ]> M) ∗
- ζ ↦M R'.
+ auth_mapping_is M -∗ ζ ↦M R ==∗ auth_mapping_is (<[ ζ := R' ]> M) ∗ ζ ↦M R'.
Proof.
iIntros "Hamap Hmap".
iCombine "Hamap Hmap" as "H".
@@ -527,9 +573,7 @@ Section model_state_lemmas.
Qed.
Lemma mapping_lookup ζ M R:
- auth_mapping_is M -∗
- ζ ↦M R -∗
- ⌜ ζ ∈ dom M âŒ.
+ auth_mapping_is M -∗ ζ ↦M R -∗ ⌜ ζ ∈ dom M âŒ.
Proof.
unfold auth_mapping_is, frag_mapping_is.
iIntros "Ham Hm".
@@ -577,32 +621,25 @@ Section model_state_lemmas.
Qed.
Lemma update_mapping_delete ζ (Rrem : gset $ fmrole Mdl) (R: gset (fmrole Mdl)) M:
- auth_mapping_is M -∗
- ζ ↦M R ==∗
- auth_mapping_is (<[ ζ := R ∖ Rrem ]> M) ∗
- ζ ↦M (R ∖ Rrem).
+ auth_mapping_is M -∗ ζ ↦M R ==∗ auth_mapping_is (<[ ζ := R ∖ Rrem ]> M) ∗ ζ ↦M (R ∖ Rrem).
Proof.
eauto using update_mapping.
Qed.
Lemma update_mapping_add ζ (Radd : gset $ fmrole Mdl) (R: gset (fmrole Mdl)) M:
- auth_mapping_is M -∗
- ζ ↦M R ==∗
- auth_mapping_is (<[ ζ := R ∪ Radd ]> M) ∗
- ζ ↦M (R ∪ Radd).
+ auth_mapping_is M -∗ ζ ↦M R ==∗ auth_mapping_is (<[ ζ := R ∪ Radd ]> M) ∗ ζ ↦M (R ∪ Radd).
Proof.
eauto using update_mapping.
Qed.
Lemma has_fuels_equiv fs ζ:
- has_fuels ζ (dom fs) fs ⊣⊢
- ζ ↦M (dom fs) ∗ ([∗ map] Ï â†¦ f ∈ fs, Ï â†¦F f).
+ has_fuels ζ fs ⊣⊢ ζ ↦M (dom fs) ∗ ([∗ map] Ï â†¦ f ∈ fs, Ï â†¦F f).
Proof.
rewrite /has_fuels -big_opM_dom. iSplit.
- - iIntros "($ & _ & H)". iApply (big_sepM_impl with "H").
+ - iIntros "($ & H)". iApply (big_sepM_impl with "H").
iIntros "!#" (Ï f Hin) "(%f' & %Hin' & ?)".
by simplify_eq.
- - iIntros "($&H)". iSplit; first done.
+ - iIntros "($&H)".
iApply (big_sepM_impl with "H").
iIntros "!#" (Ï f Hin) "?". iExists f. iSplit; done.
Qed.
@@ -611,11 +648,11 @@ Section model_state_lemmas.
let LR := (dom F ∪ dom fs') ∖ (dom fs ∖ dom fs') in
(fs ≠∅) ->
(dom fs' ∖ dom fs ∩ dom F = ∅) ->
- has_fuels ζ (dom fs) fs -∗
+ has_fuels ζ fs -∗
auth_fuel_is F -∗
auth_mapping_is M ==∗
auth_fuel_is (fuel_apply fs' F LR) ∗
- has_fuels ζ (dom fs') fs' ∗
+ has_fuels ζ fs' ∗
auth_mapping_is (<[ ζ := dom fs' ]> M).
Proof.
iIntros (LR Hfs Hdom) "Hfuels Hafuels Hamapping".
@@ -630,11 +667,11 @@ Section model_state_lemmas.
let LR := (dom F ∪ dom fs') ∖ (dom fs ∖ dom fs') in
(fs ≠∅) ->
(dom fs' = dom fs) ->
- has_fuels ζ (dom fs) fs -∗
+ has_fuels ζ fs -∗
auth_fuel_is F -∗
auth_mapping_is M ==∗
auth_fuel_is (fuel_apply fs' F LR) ∗
- has_fuels ζ (dom fs') fs' ∗
+ has_fuels ζ fs' ∗
auth_mapping_is M.
Proof.
iIntros (LR Hfs Hdom) "Hfuels Hafuels Hamapping".
@@ -645,13 +682,11 @@ Section model_state_lemmas.
iFrame. rewrite Hdom //.
Qed.
- Lemma has_fuel_in ζ R δ fs n:
- has_fuels ζ R fs -∗
- model_state_interp n δ -∗
- ⌜ ∀ Ï, ls_mapping δ !! Ï = Some ζ <-> Ï âˆˆ R âŒ.
+ Lemma has_fuel_in ζ δ fs n:
+ has_fuels ζ fs -∗ model_state_interp n δ -∗ ⌜ ∀ Ï, ls_mapping δ !! Ï = Some ζ <-> Ï âˆˆ dom fs âŒ.
Proof.
unfold model_state_interp, has_fuels, auth_mapping_is, frag_mapping_is.
- iIntros "[Hζ [%HRdom Hfuels]] (%M&Hafuel&Hamapping&%Hmapinv&Hamod) %Ï".
+ iIntros "[Hζ Hfuels] (%M&Hafuel&Hamapping&%Hmapinv&Hamod) %Ï".
iCombine "Hamapping Hζ" as "H".
iDestruct (own_valid with "H") as %Hval. iPureIntro.
apply auth_both_valid_discrete in Hval as [Hval ?].
@@ -664,15 +699,12 @@ Section model_state_lemmas.
- intros ?. eexists. split; eauto.
Qed.
- Lemma has_fuel_fuel ζ R δ fs n:
- has_fuels ζ R fs -∗
- model_state_interp n δ -∗
- ⌜ dom fs = R ∧ ∀ Ï, Ï âˆˆ R -> ls_fuel δ !! Ï = fs !! Ï âŒ.
+ Lemma has_fuel_fuel ζ δ fs n:
+ has_fuels ζ fs -∗ model_state_interp n δ -∗ ⌜ ∀ Ï, Ï âˆˆ dom fs -> ls_fuel δ !! Ï = fs !! Ï âŒ.
Proof.
unfold has_fuels, model_state_interp, auth_fuel_is.
- iIntros "[Hζ [%HRdom Hfuels]] (%M&Hafuel&Hamapping&%Hmapinv&Hamod)".
- iSplit; first done. iIntros (Ï HÏ).
- iDestruct (big_sepS_delete _ R Ï with "Hfuels") as "[(%f&%Hfs&Hfuel) _]" =>//.
+ iIntros "[Hζ Hfuels] (%M&Hafuel&Hamapping&%Hmapinv&Hamod)" (Ï HÏ).
+ iDestruct (big_sepS_delete _ _ Ï with "Hfuels") as "[(%f&%Hfs&Hfuel) _]" =>//.
iCombine "Hafuel Hfuel" as "H".
iDestruct (own_valid with "H") as %Hval. iPureIntro.
apply auth_both_valid_discrete in Hval as [Hval ?].
@@ -683,33 +715,24 @@ Section model_state_lemmas.
rewrite HfuelÏ Hfs //.
Qed.
- Lemma has_fuels_dom ζ fs R :
- has_fuels ζ R fs -∗ ⌜ R = dom fs âŒ.
- Proof. iIntros "(_&%&_)". iPureIntro. set_solver. Qed.
-
- Lemma has_fuels_S_dom ζ fs R :
- has_fuels_S ζ R fs -∗ ⌜ R = dom fs âŒ.
- Proof. iIntros "(_&%&_)". iPureIntro. set_solver. Qed.
-
- Lemma update_no_step_enough_fuel extr (auxtr : auxiliary_trace (fair_model Mdl)) c2 fs R ζ:
- (R ≠∅) ->
+ Lemma update_no_step_enough_fuel extr (auxtr : auxiliary_trace (fair_model Mdl)) c2 fs ζ:
+ (dom fs ≠∅) ->
locale_step (trace_last extr) (Some ζ) c2 ->
- has_fuels_S ζ R fs -∗ model_state_interp (trace_last extr).1 (trace_last auxtr)
+ has_fuels_S ζ fs -∗ model_state_interp (trace_last extr).1 (trace_last auxtr)
==∗ ∃ δ2 (ℓ : mlabel $ fair_model Mdl),
⌜labels_match (Some ζ) ℓ
∧ valid_state_evolution_fairness (extr :tr[Some ζ]: c2) (auxtr :tr[â„“]: δ2)âŒ
- ∗ has_fuels ζ R fs ∗ model_state_interp c2.1 δ2.
+ ∗ has_fuels ζ fs ∗ model_state_interp c2.1 δ2.
Proof.
iIntros "%HnotO %Hstep Hf Hmod".
destruct c2 as [tp2 σ2].
destruct (set_choose_L _ HnotO) as [??].
iDestruct (has_fuel_in with "Hf Hmod") as %Hxdom; eauto.
- iDestruct (has_fuel_fuel with "Hf Hmod") as %[HRdom Hfuel]; eauto.
+ iDestruct (has_fuel_fuel with "Hf Hmod") as "%Hfuel"; eauto.
iDestruct (model_state_interp_tids_smaller with "Hmod") as %Hζs.
iDestruct "Hmod" as "(%M & Hfuel & Hamapping & %Hminv & %Hlocssmall & Hmodel)".
unfold has_fuels_S.
simpl in *.
- iDestruct (has_fuels_dom with "Hf") as %->.
iMod (update_has_fuels_no_step ζ (S <$> fs) fs with "[Hf] [Hfuel] [Hamapping]") as "(Hafuels&Hfuels&Hamapping)" =>//.
{ rewrite -dom_empty_iff_L. set_solver. }
@@ -753,12 +776,12 @@ Section model_state_lemmas.
specialize (Hζs _ _ Hsome).
destruct (trace_last extr); eapply from_locale_step =>//. }
iSplit.
- { iPureIntro. eexists. by apply Hxdom. }
+ { iPureIntro. eexists. apply Hxdom. by rewrite dom_fmap. }
iSplit.
{ unfold fuel_decr. simpl.
iIntros "!%" (Ï' HÏ'live Hmustdec).
inversion Hmustdec; simplify_eq.
- have Hin: Ï' ∈ dom (S <$> fs) by set_solver.
+ have Hin: Ï' ∈ dom (S <$> fs) by set_solver.
rewrite map_lookup_imap Hfuel // lookup_fmap.
destruct (S <$> fs !! Ï') as [f|] eqn:Heq; simpl.
+ rewrite decide_True //; last by set_solver.
@@ -784,32 +807,30 @@ Section model_state_lemmas.
Lemma update_fork_split R1 R2 tp1 tp2 fs (extr : execution_trace Λ)
(auxtr: auxiliary_trace (fair_model Mdl)) ζ efork σ1 σ2 (Hdisj: R1 ## R2):
fs ≠∅ ->
+ R1 ∪ R2 = dom fs ->
trace_last extr = (tp1, σ1) ->
locale_step (tp1, σ1) (Some ζ) (tp2, σ2) ->
(∃ tp1', tp2 = tp1' ++ [efork] ∧ length tp1' = length tp1) ->
- has_fuels_S ζ (R1 ∪ R2) fs -∗ model_state_interp (trace_last extr).1 (trace_last auxtr) ==∗
- ∃ δ2, has_fuels (locale_of tp1 efork) R2 (fs ⇂ R2) ∗ has_fuels ζ R1 (fs ⇂ R1) ∗ model_state_interp tp2 δ2
+ has_fuels_S ζ fs -∗ model_state_interp (trace_last extr).1 (trace_last auxtr) ==∗
+ ∃ δ2, has_fuels (locale_of tp1 efork) (fs ⇂ R2) ∗ has_fuels ζ (fs ⇂ R1) ∗ model_state_interp tp2 δ2
∧ ⌜valid_state_evolution_fairness (extr :tr[Some ζ]: (tp2, σ2)) (auxtr :tr[Silent_step ζ]: δ2)âŒ.
Proof.
- iIntros (Hnemp -> Hstep Htlen) "Hf Hmod".
+ iIntros (Hnemp Hunioneq -> Hstep Htlen) "Hf Hmod".
unfold has_fuels_S.
simpl in *.
- iDestruct (has_fuel_fuel with "Hf Hmod") as %[HdomS Hfuels].
+ iDestruct (has_fuel_fuel with "Hf Hmod") as %Hfuels.
iDestruct (model_state_interp_tids_smaller with "Hmod") as %Hts.
iDestruct "Hmod" as (M) "(Haf&Ham&%Hminv&%Hsmall&Hamod)".
- iDestruct (has_fuels_dom with "Hf") as %Hdomeq.
- rewrite Hdomeq.
-
pose Hlocincl := locales_of_list_step_incl _ _ _ _ _ Hstep.
iMod (update_has_fuels_no_step ζ (S <$> fs) fs with "Hf Haf Ham") as "(Haf&Hf&Ham)".
{ intros contra. apply fmap_empty_inv in contra. set_solver. }
{ rewrite dom_fmap_L //. }
- iDestruct "Hf" as "(Hf & %Hdom & Hfuels)".
+ iDestruct "Hf" as "(Hf & Hfuels)".
iDestruct (frag_mapping_same with "Ham Hf") as %Hmapping.
assert (Hnewζ: (locale_of tp1 efork) ∉ dom M).
@@ -849,34 +870,26 @@ Section model_state_lemmas.
map_imap (λ Ï o, if (decide (Ï âˆˆ R2)) then Some $ locale_of tp1 efork else Some o) (ls_mapping δ1);
ls_mapping_dom := Hmappingdom;
|}.
- iModIntro. rewrite dom_fmap_L in Hdomeq.
+ iModIntro.
assert (Hdomincl: dom fs ⊆ dom (ls_fuel δ1)).
{ intros Ï' Hin'. rewrite elem_of_dom Hfuels; last first.
- { rewrite Hdomeq //. }
+ { rewrite dom_fmap_L //. }
rewrite lookup_fmap fmap_is_Some. by apply elem_of_dom. }
- rewrite -{3}Hdomeq big_sepS_union //. iDestruct "Hfuels" as "[Hf1 Hf2]".
+ rewrite -Hunioneq big_sepS_union //. iDestruct "Hfuels" as "[Hf1 Hf2]".
iSplitL "Hf2 HR2".
- { unfold has_fuels. iFrame. iSplit.
- - iPureIntro. symmetry. eapply dom_filter_L. intros Ï. split.
- + intros Hin. assert (Hindom: Ï âˆˆ dom fs); first set_solver.
- apply elem_of_dom in Hindom as [??]. eauto.
- + by intros (?&?&?).
- - iApply (big_sepS_impl with "Hf2"). iIntros "!#" (x Hin) "(%f&%&?)".
- iExists _; iFrame. iPureIntro. rewrite map_filter_lookup_Some //. }
+ { unfold has_fuels. rewrite dom_domain_restrict; [|set_solver]. iFrame.
+ iApply (big_sepS_impl with "Hf2"). iIntros "!#" (x Hin) "(%f&%&?)".
+ iExists _; iFrame. iPureIntro. rewrite map_filter_lookup_Some //. }
iSplitL "Hf1 HR1".
- { unfold has_fuels. iFrame. iSplit.
- - iPureIntro. symmetry. eapply dom_filter_L. intros Ï. split.
- + intros Hin. assert (Hindom: Ï âˆˆ dom fs); first set_solver.
- apply elem_of_dom in Hindom as [??]. eauto.
- + by intros (?&?&?).
- - iApply (big_sepS_impl with "Hf1"). iIntros "!#" (x Hin) "(%f&%&?)".
- iExists _; iFrame. iPureIntro. rewrite map_filter_lookup_Some //. }
+ { unfold has_fuels. rewrite dom_domain_restrict; [|set_solver]. iFrame.
+ iApply (big_sepS_impl with "Hf1"). iIntros "!#" (x Hin) "(%f&%&?)".
+ iExists _; iFrame. iPureIntro. rewrite map_filter_lookup_Some //. }
iSplitL "Ham Haf Hamod".
{ iExists _; simpl. iFrame "Ham Hamod".
iSplit.
- iApply (auth_fuel_is_proper with "Haf"). unfold fuel_apply.
rewrite -leibniz_equiv_iff. intros Ï. rewrite !map_lookup_imap.
- rewrite dom_fmap_L difference_diag_L difference_empty_L.
+ rewrite Hunioneq dom_fmap_L difference_diag_L difference_empty_L.
rewrite lookup_gset_to_gmap.
destruct (decide (Ï âˆˆ dom (ls_fuel δ1) ∪ dom fs)) as [Hin|Hin].
+ rewrite option_guard_True //=.
@@ -886,12 +899,11 @@ Section model_state_lemmas.
destruct (decide (Ï âˆˆ dom fs)) as [Hinfs|Hinfs].
* apply elem_of_dom in Hmap as [? Hinfuels]. rewrite Hinfuels /=.
- rewrite decide_True; last set_solver.
rewrite Hfuels in Hinfuels; last set_solver. rewrite lookup_fmap in Hinfuels.
destruct (fs !! Ï); last done. f_equiv. simpl in Hinfuels. injection Hinfuels. intros ?.
rewrite leibniz_equiv_iff. lia.
* apply elem_of_dom in Hmap as [? Hinfuels].
- rewrite Hinfuels /= decide_False //; last set_solver.
+ rewrite Hinfuels //.
+ rewrite option_guard_False //=.
rewrite -> not_elem_of_union in Hin. destruct Hin as [Hin ?].
rewrite -> not_elem_of_dom in Hin. rewrite Hin //.
@@ -982,11 +994,11 @@ Section model_state_lemmas.
apply elem_of_dom in Hin. destruct Hin as [f' Hin'].
rewrite Hin' /=.
destruct (decide (Ï âˆˆ R1 ∪ R2)) as [Hin''|Hin''].
- { specialize (Hfuels _ Hin''). rewrite lookup_fmap Hin' in Hfuels.
+ { rewrite dom_fmap_L -Hunioneq in Hfuels.
+ specialize (Hfuels _ Hin''). rewrite lookup_fmap Hin' in Hfuels.
destruct (fs !! Ï); simplify_eq. simpl in Hfuels. injection Hfuels.
intros ->. simpl. lia. }
- symmetry in Hsametid. apply Hminv in Hsametid as (?&?&?).
- rewrite Hdomeq in Hin''. set_solver.
+ symmetry in Hsametid. apply Hminv in Hsametid as (?&?&?). set_solver.
- rewrite map_lookup_imap. simpl in *. clear Hmd.
destruct (decide (Ï âˆˆ dom (ls_mapping δ1))) as [Hin|Hin]; last first.
{ apply not_elem_of_dom in Hin. rewrite map_lookup_imap Hin //= in Hissome. by inversion Hissome. }
@@ -1036,16 +1048,16 @@ Section model_state_lemmas.
Lemma update_step_still_alive
(extr : execution_trace Λ)
(auxtr: auxiliary_trace (fair_model Mdl))
- tp1 tp2 σ1 σ2 s1 s2 fs1 fs2 R1 Ï (δ1 : fair_model Mdl) ζ:
+ tp1 tp2 σ1 σ2 s1 s2 fs1 fs2 Ï (δ1 : fair_model Mdl) ζ:
trace_last extr = (tp1, σ1) →
trace_last auxtr = δ1 ->
locale_step (tp1, σ1) (Some ζ) (tp2, σ2) ->
fmtrans _ s1 (Some Ï) s2 -> valid_new_fuelmap fs1 fs2 δ1 s2 Ï ->
- has_fuels ζ R1 fs1 -∗ frag_model_is s1 -∗ model_state_interp tp1 δ1
+ has_fuels ζ fs1 -∗ frag_model_is s1 -∗ model_state_interp tp1 δ1
==∗ ∃ (δ2: fair_model Mdl) ℓ,
⌜labels_match (Some ζ) ℓ
∧ valid_state_evolution_fairness (extr :tr[Some ζ]: (tp2, σ2)) (auxtr :tr[â„“]: δ2)âŒ
- ∗ has_fuels ζ (dom fs2) fs2 ∗ frag_model_is s2 ∗ model_state_interp tp2 δ2.
+ ∗ has_fuels ζ fs2 ∗ frag_model_is s2 ∗ model_state_interp tp2 δ2.
Proof.
iIntros (Htrlast Hauxtrlast Hstep Htrans Hfuelsval) "Hfuel Hmod Hsi".
@@ -1053,14 +1065,12 @@ Section model_state_lemmas.
{ destruct Hfuelsval as (_&?&_). intros ->. set_solver. }
iDestruct (has_fuel_in with "Hfuel Hsi") as "%Hxdom"; eauto.
- iDestruct (has_fuel_fuel with "Hfuel Hsi") as %[HRdom Hfuel]; eauto.
+ iDestruct (has_fuel_fuel with "Hfuel Hsi") as %Hfuel; eauto.
iDestruct (model_state_interp_tids_smaller with "Hsi") as %Hless.
iDestruct "Hsi" as "(%M&Hafuel&Hamapping&%Hinv&%Hsmall&Hamod)".
iDestruct (model_agree with "Hamod Hmod") as "%Heq".
- iDestruct (has_fuels_dom with "Hfuel") as %->.
-
assert (Hfueldom: dom (update_fuel_resource δ1 fs2 s2) = live_roles Mdl s2).
{ unfold update_fuel_resource, fuel_apply. rewrite -leibniz_equiv_iff.
intros Ï'; split.
--
GitLab