From b6eeb952ae81d3365467fe1f08ebc67482c0117c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?L=C3=A9o=20Stefanesco?= <leo.lveb@gmail.com>
Date: Tue, 31 May 2022 17:38:38 +0200
Subject: [PATCH] Add graceful shutdown of threads for termination
A thread can be associated to a non-live role, in which case it can take
silent steps until it finishes, but it cannot take observable steps.
This allows to prove the yes-no example using the ``right'' model, that
is, the model we showed in the figure in the paper!
---
fairness/examples/yesno.v | 553 +++++++++----------
fairness/examples/yesno_adequacy.v | 185 +++----
fairness/fairness.v | 241 ++++-----
fairness/fairness_finiteness.v | 91 ++--
fairness/heap_lang/lifting.v | 239 ++++++---
fairness/resources.v | 821 ++++++++++++++++++-----------
trillium/prelude/finitary.v | 55 ++
trillium/program_logic/adequacy.v | 122 +++++
8 files changed, 1335 insertions(+), 972 deletions(-)
diff --git a/fairness/examples/yesno.v b/fairness/examples/yesno.v
index 7f3f3e3..3cc148d 100644
--- a/fairness/examples/yesno.v
+++ b/fairness/examples/yesno.v
@@ -68,39 +68,39 @@ Qed.
#[global] Instance YN_inhabited: Inhabited YN.
Proof. exact (populate Y). Qed.
-Inductive yntrans: nat*bool*bool*bool -> option YN -> nat*bool*bool*bool -> Prop :=
-| yes_trans n: (n > 0)%nat ->yntrans (n, true, true, true) (Some Y) (n, false, true, true) (* < *)
-| yes_fail n: (n > 0)%nat ->yntrans (n, false, true, true) (Some Y) (n, false, true, true) (* ≤ *)
-| no_trans n: yntrans (S n, false, true, true) (Some No) (n, true, true, true) (* < *)
-| no_trans_end yf: yntrans (1, false, yf, true) (Some No) (0, true, yf, true) (* < *)
-| no_fail n: yntrans (n, true, true, true) (Some No) (n, true, true, true) (* ≤ *)
-| yes_finish N B nf: (N ≤ 1) -> yntrans (N, B, true, nf) (Some Y) (N, B, false, nf) (* < *)
-| no_finish B yf: yntrans (0, B, yf, true) (Some No) (0, B, yf, false). (* < *)
+Inductive yntrans: nat*bool -> option YN -> nat*bool -> Prop :=
+| yes_trans n: (n > 0)%nat -> yntrans (n, true) (Some Y) (n, false) (* < *)
+| yes_fail n: (n > 1)%nat -> yntrans (n, false) (Some Y) (n, false) (* ≤ *)
+| no_trans n: yntrans (S n, false) (Some No) (n, true) (* < *)
+| no_fail n: (n > 0)%nat → yntrans (n, true) (Some No) (n, true) (* ≤ *)
+.
+
+Definition yn_live_roles nb : gset YN :=
+ match nb with
+ | (0, _) => ∅
+ | (1, false) => {[ No ]}
+ | _ => {[ No; Y ]}
+ end.
Lemma live_spec_holds:
- forall s Ï s', yntrans s (Some Ï) s' -> Ï âˆˆ (match s with
- | (_, _, yf, nf) => (if yf then {[ Y ]} else ∅) ∪ (if nf then {[ No ]} else ∅)
- end: gset YN).
+ forall s Ï s', yntrans s (Some Ï) s' -> Ï âˆˆ yn_live_roles s.
Proof.
- intros [[[n ?] yf] nf] yn [[[??] ?] ?] Htrans.
- inversion Htrans; set_solver.
+ intros [n b] yn [n' ?] Htrans. rewrite /yn_live_roles.
+ inversion Htrans; simplify_eq; destruct n'; try set_solver; try lia; destruct n'; try set_solver; lia.
Qed.
Definition the_model: FairModel.
Proof.
refine({|
- fmstate := nat * bool * bool * bool;
+ fmstate := nat * bool;
fmrole := YN;
fmtrans := yntrans;
- live_roles nb :=
- match nb with
- | (_, _, yf, nf) => (if yf then {[ Y ]} else ∅) ∪ (if nf then {[ No ]} else ∅)
- end;
- fuel_limit _ := 45%nat;
+ live_roles nb := yn_live_roles nb;
+ fuel_limit _ := 61%nat;
fm_live_spec := live_spec_holds;
|}).
- intros Ï' [[[? ?] ?] ?] Ï [[[? ?] ?] ?] Htrans Hin Hneq.
- inversion Htrans; destruct Ï; try set_solver.
+ intros Ï' [? ?] Ï [n' ?] Htrans Hin Hneq; rewrite /yn_live_roles.
+ inversion Htrans; destruct Ï; simplify_eq; destruct n'; try set_solver; try lia; destruct n'; try set_solver; lia.
Defined.
@@ -108,8 +108,6 @@ Defined.
Class yesnoG Σ := YesnoG {
yes_name: gname;
no_name: gname;
- yes_f_name: gname;
- no_f_name: gname;
yesno_n_G :> inG Σ (excl_authR natO);
yesno_f_G :> inG Σ (excl_authR boolO);
}.
@@ -133,12 +131,6 @@ Section proof.
Definition auth_yes_at (n: nat) := own yes_name (â—E n).
Definition auth_no_at (n: nat) := own no_name (â—E n).
- Definition yes_finished (b: bool) := own yes_f_name (â—¯E b).
- Definition no_finished (b: bool) := own no_f_name (â—¯E b).
-
- Definition auth_yes_finished (b: bool) := own yes_f_name (â—E b).
- Definition auth_no_finished (b: bool) := own no_f_name (â—E b).
-
Lemma they_agree γ (N M: nat):
own γ (â—¯E N) -∗ own γ (â—E M) -∗ ⌜ M = N âŒ.
Proof.
@@ -153,20 +145,6 @@ Section proof.
no_at N -∗ auth_no_at M -∗ ⌜ M = N âŒ.
Proof. apply they_agree. Qed.
- Lemma they_finished_agree γ (N M: bool):
- own γ (â—¯E N) -∗ own γ (â—E M) -∗ ⌜ M = N âŒ.
- Proof.
- iIntros "HA HB". iCombine "HB HA" as "H".
- iDestruct (own_valid with "H") as "%Hval".
- iPureIntro. by apply excl_auth_agree_L.
- Qed.
- Lemma yes_finished_agree N M:
- yes_finished N -∗ auth_yes_finished M -∗ ⌜ M = N âŒ.
- Proof. apply they_finished_agree. Qed.
- Lemma no_finished_agree N M:
- no_finished N -∗ auth_no_finished M -∗ ⌜ M = N âŒ.
- Proof. apply they_finished_agree. Qed.
-
Lemma they_update γ (N M P: nat):
own γ (â—E N) ∗ own γ (â—¯E M) ==∗ own γ (â—E P) ∗ own γ (â—¯E P).
Proof.
@@ -184,63 +162,125 @@ Section proof.
Proof.
rewrite -!own_op. iApply own_update. apply excl_auth_update.
Qed.
- Lemma yes_finished_update P N M:
- auth_yes_finished M ∗ yes_finished N ==∗ auth_yes_finished P ∗ yes_finished P.
- Proof. apply they_finished_update. Qed.
- Lemma no_finished_update P N M:
- auth_no_finished M ∗ no_finished N ==∗ auth_no_finished P ∗ no_finished P.
- Proof. apply they_finished_update. Qed.
Definition yesno_inv_inner b :=
- (∃ N B yf nf,
- ⌜((N > 1 ∨ (N > 0 ∧ B = true)) -> yf = true) ∧ (N > 0 -> nf = true)⌠∗
- auth_yes_finished yf ∗ auth_no_finished nf ∗
- frag_model_is (N, B, yf, nf) ∗ b ↦ #B ∗
- if B
- then auth_yes_at N ∗ auth_no_at N
- else auth_yes_at (N-1)%nat ∗ auth_no_at N)%I.
+ (∃ N B,
+ frag_free_roles_are ∅ ∗
+ frag_model_is (N, B) ∗ b ↦ #B ∗
+ (if B
+ then auth_yes_at N ∗ auth_no_at N
+ else auth_yes_at (N-1) ∗ auth_no_at N) ∗
+ ⌜(N, B) ≠(0, false)âŒ
+ )%I.
Definition yesno_inv b := inv Ns (yesno_inv_inner b).
- Lemma yes_go_spec tid n b (N: nat) f (Hf: f > 17):
- {{{ yesno_inv b ∗ has_fuel tid Y f ∗ n ↦ #N ∗ ⌜N > 0⌠∗ yes_at N ∗ yes_finished true }}}
+ Lemma yes_go_spec tid n b (N: nat) f (Hf: f > 40):
+ {{{ yesno_inv b ∗ has_fuel tid Y f ∗ n ↦ #N ∗ ⌜N > 0âŒ%nat ∗ yes_at N }}}
yes_go #n #b @ tid
{{{ RET #(); tid ↦M ∅ }}}.
Proof.
iLöb as "Hg" forall (N f Hf).
- iIntros (Φ) "(#Hinv & Hf & HnN & %HN & Hyes & Hyesf) Hk". unfold yes_go.
+ iIntros (Φ) "(#Hinv & Hf & HnN & %HN & Hyes) Hk". unfold yes_go.
wp_pures.
wp_bind (CmpXchg _ _ _).
- assert (∀ s, Atomic s (CmpXchg #b #true #false)).
- { apply _. }
+ assert (∀ s, Atomic s (CmpXchg #b #true #false)) by apply _.
iApply wp_atomic.
- iInv Ns as (M B yf nf) "(>[%Htrue %Htrue'] & >Hayesf & >Hanof & >Hmod & >Bb & Hauths)" "Hclose".
- iDestruct (yes_finished_agree with "Hyesf Hayesf") as %->.
+ iInv Ns as (M B) "(>HFR & >Hmod & >Bb & Hauths & >%Hnever)" "Hclose".
destruct B; iDestruct "Hauths" as "[>Hay >Han]".
- - iDestruct (yes_agree with "Hyes Hay") as "%Heq". rewrite -> Heq in *. clear Heq.
- rewrite (Htrue' HN).
+ - iDestruct (yes_agree with "Hyes Hay") as "%Heq".
+
(* 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)
+
+ destruct (decide (M = 0)) as [->|Nneq]; first lia.
+ destruct (decide (M = 1)) as [->|Nneq1].
+ + iApply (wp_cmpxchg_suc_step_singlerole_keep_dead _ tid (Y: fmrole the_model) _ 30%nat _
+ (1, true) (1, false)
+ with "[$]") =>//.
+ { set_solver. }
+ { lia. }
+ { econstructor. lia. }
+ { set_solver. }
+ iModIntro.
+ iIntros "!> (Hb & Hmod & HFR & Hf)".
+ iMod (yes_update 0 with "[$]") as "[Hay Hyes]".
+ iMod ("Hclose" with "[Hmod Hb Hay Han HFR]").
+ { iNext. iExists _, _. iFrame. simpl. iFrame. by iPureIntro. }
+
+ iModIntro.
+
+ rewrite has_fuel_fuels.
+ wp_pures.
+ wp_load.
+ wp_pures.
+ wp_store.
+ wp_pures.
+ wp_load.
+
+ wp_pure _.
+ simplify_eq. simpl.
+
+ iApply wp_atomic.
+
+ iInv Ns as (M B) "(>HFR & >Hmod & >Hb & Hauths & >%Hbever')" "Hclose".
+
+ destruct B.
+ * iApply (wp_lift_pure_step_no_fork_remove_role {[ Y ]} ((0, true): fmstate the_model) _ _ _ _ _ _ {[ Y := _ ]}) =>//.
+ { apply map_non_empty_singleton. }
+ { rewrite dom_singleton. set_solver. }
+ { simpl. set_solver. }
+
+ repeat iModIntro.
+
+ iDestruct "Hauths" as "[Hay Han]". iDestruct (yes_agree with "Hyes Hay") as %Heq.
+ assert (M = 0) by lia. simplify_eq. iFrame "Hmod". iSplitL "Hf".
+ { rewrite /has_fuels_S fmap_insert fmap_empty //. }
+ iIntros "Hmod Hf".
+
+ wp_pures. repeat iModIntro.
+ iMod ("Hclose" with "[Hmod Hay Han Hb HFR]").
+ { iNext. iExists _, _. iFrame. done. }
+ iModIntro. iApply "Hk".
+ rewrite map_filter_singleton_False; last set_solver. rewrite /has_fuels dom_empty_L.
+ iDestruct "Hf" as "[??]". iFrame.
+ * iDestruct "Hauths" as "[>Hay >Han]". iDestruct (yes_agree with "Hyes Hay") as %Heq.
+ assert (M = 1) by (destruct M; [done|lia]). simplify_eq.
+
+ iApply (wp_lift_pure_step_no_fork_remove_role {[ Y ]} ((1, false): fmstate the_model) _ _ _ _ _ _ {[ Y := _ ]}) =>//.
+ { apply map_non_empty_singleton. }
+ { rewrite dom_singleton. set_solver. }
+ { simpl. set_solver. }
+
+ repeat iModIntro.
+
+ iFrame "Hmod". iSplitL "Hf".
+ { rewrite /has_fuels_S fmap_insert fmap_empty //. }
+ iIntros "Hmod Hf".
+
+ wp_pures. repeat iModIntro.
+ iMod ("Hclose" with "[Hmod Hay Han Hb HFR]").
+ { iNext. iExists _, _. iFrame. done. }
+ iModIntro. iApply "Hk".
+ rewrite map_filter_singleton_False; last set_solver. rewrite /has_fuels dom_empty_L.
+ iDestruct "Hf" as "[??]". iFrame.
+ + assert (N = N) by lia. simplify_eq. iApply (wp_cmpxchg_suc_step_singlerole _ tid (Y: fmrole the_model) _ 55%nat _
+ (M, true) (M, false)
with "[$]"); eauto.
{ simpl. lia. }
{ econstructor. lia. }
+ { simpl. destruct M; [set_solver | destruct M; set_solver]. }
iModIntro.
- iIntros "!> (Hb & Hmod & Hf)".
- iMod (yes_update (N-1) with "[$]") as "[Hay Hyes]".
- iMod ("Hclose" with "[Hmod Hb Hay Han Hanof Hayesf]").
- { iNext. iExists N, false, true, true. iFrame. iPureIntro; intros; lia. }
- simpl.
-
- destruct N as [|N]; first lia. rewrite decide_True; last first.
- { destruct N; set_solver. }
-
- iModIntro.
+ iIntros "!> (Hb & Hmod & HFR & Hf)".
+ iMod (yes_update (M-1) with "[$]") as "[Hay Hyes]".
+ iMod ("Hclose" with "[Hmod Hay Han Hb HFR]").
+ { iNext. iExists _, _. iFrame. iPureIntro. intro contra. simplify_eq. }
+ iModIntro. rewrite decide_True; last first.
+ { do 2 (destruct M; try done). set_solver. }
rewrite has_fuel_fuels.
wp_pures.
@@ -251,115 +291,57 @@ Section proof.
wp_load.
wp_pures.
- destruct (decide (0 < S N - 1)) as [Heq|Heq].
- + rewrite bool_decide_eq_true_2 //; last lia.
+ destruct (decide (0 < S M - 1)) as [Heq|Heq].
+ * rewrite bool_decide_eq_true_2 //; last lia.
wp_pure _.
rewrite -has_fuel_fuels.
- iApply ("Hg" with "[] [Hyes HnN Hf Hyesf] [$]"); last first.
- { iFrame "∗#". iSplit; last (iPureIntro; lia).
- 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.
- have ->: N = 0 by lia. simpl.
+ iApply ("Hg" with "[] [Hyes HnN Hf] [$]"); last first.
+ { iFrame "∗#". iSplit; last by iPureIntro; lia.
+ iClear "Hg Hinv". Set Printing Implicit.
- clear M. clear Htrue Htrue' nf.
-
- iApply wp_atomic.
- iInv Ns as (M B yf nf) "(>[%Htrue %Htrue'] & >Hayesf & >Hanof & >Hmod & >Hb & Hauths)" "Hclose".
-
- destruct B as [|].
- * iDestruct "Hauths" as "[>Hay >Hano]".
- iDestruct (yes_agree with "Hyes Hay") as %->.
- iDestruct (yes_finished_agree with "Hyesf Hayesf") as %->.
-
- iApply (wp_lift_pure_step_no_fork_singlerole_take_step
- ((0, true, true, nf): fmstate the_model) (0, true, false, nf) _ _ _ _ 0
- ); eauto.
- { set_solver. }
- { lia. }
- { econstructor. lia. }
-
- rewrite -has_fuel_fuels.
- iFrame. iModIntro.
- iMod (yes_finished_update false with "[$]") as "[Hayesf Hyesf]".
- iModIntro. iNext. iModIntro.
- iIntros "Hmod".
-
- rewrite -wp_value.
- have Hnotin: Y ∉ live_roles the_model (0, true, false, nf).
- { destruct nf; simpl; set_solver. }
- rewrite decide_False //. iIntros "Hccl".
-
- iMod ("Hclose" with "[Hmod Hb Hay Hano Hanof Hayesf]").
- { iNext. iExists 0, true, false, nf. iFrame. iPureIntro; lia. }
- iModIntro. iApply ("Hk" with "Hccl").
-
- * iDestruct "Hauths" as "[>Hay >Hano]".
- iDestruct (yes_agree with "Hyes Hay") as %Heq'.
- iDestruct (yes_finished_agree with "Hyesf Hayesf") as %->.
-
- iApply (wp_lift_pure_step_no_fork_singlerole_take_step
- ((M, false, true, nf): fmstate the_model) (M, false, false, nf) _ _ _ _ 0
- ); eauto.
- { set_solver. }
- { lia. }
- { econstructor. lia. }
-
- rewrite -has_fuel_fuels.
- iFrame. iModIntro.
- iMod (yes_finished_update false with "[$]") as "[Hayesf Hyesf]".
- iModIntro. iNext. iModIntro.
- iIntros "Hmod".
-
- rewrite -wp_value.
- have Hnotin: Y ∉ live_roles the_model (0, true, false, nf).
- { destruct nf; simpl; set_solver. }
- rewrite decide_False //. iIntros "Hccl".
-
- iMod ("Hclose" with "[Hmod Hb Hay Hano Hanof Hayesf]").
- { iNext. iExists M, false, false, nf. iFrame. iPureIntro; split; intros. { lia. }
- apply Htrue'. lia. }
- iModIntro. iApply ("Hk" with "Hccl").
+ assert (∀ l v v', v = v' → l ↦ v ⊣⊢ l ↦ v') as pointsto_proper.
+ { intros ??? ->. done. }
+ iApply (pointsto_proper with "HnN"). do 2 f_equiv. destruct M; [done|]. lia. }
+ iPureIntro; lia.
+ * rewrite bool_decide_eq_false_2 //; last lia.
+ have ->: M = 0 by lia. simpl. lia.
- 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)
+ iApply (wp_cmpxchg_fail_step_singlerole _ tid (Y: fmrole the_model) _ 50%nat _
+ (M, false) (M, false)
with "[$]"); eauto.
{ simpl. lia. }
{ econstructor. lia. }
- iIntros "!>!> (Hb & Hmod & Hf)".
+ iIntros "!>!> (Hb & Hmod & HFR & Hf)".
(* iMod (yes_update (N-1) with "[$]") as "[Hay Hyes]". *)
- iMod ("Hclose" with "[Hmod Hb Hay Han Hanof Hayesf]").
- { iNext. iExists M, false, true, true. rewrite Heq. iFrame. iPureIntro; intros; lia. }
- simpl.
+ iMod ("Hclose" with "[Hmod Hb Hay Han HFR]").
+ { iNext. simplify_eq. iExists _, _. iFrame. iSplit; [iFrame|done]. }
- destruct N as [|N]; first lia. rewrite decide_True; last first.
- { destruct N; set_solver. }
+ rewrite decide_True; last first.
+ { destruct M; [done|destruct M; [lia|set_solver]]. }
- rewrite has_fuel_fuels.
iModIntro.
wp_pures.
wp_load.
- do 2 wp_pure _.
+ wp_pure _. rewrite bool_decide_eq_true_2; last lia.
+ wp_pure _.
rewrite -has_fuel_fuels.
- iApply ("Hg" with "[] [Hyes HnN Hf Hyesf] [$]"); last first.
+ iApply ("Hg" with "[] [Hyes HnN Hf] [$]"); last first.
{ iFrame "∗#". iPureIntro; lia. }
iPureIntro; lia.
Qed.
- Lemma yes_spec tid b (N: nat) f (Hf: f > 25):
- {{{ yesno_inv b ∗ has_fuel tid Y f ∗ ⌜N > 0⌠∗ yes_at N ∗ yes_finished true }}}
+ Lemma yes_spec tid b (N: nat) f (Hf: f > 50):
+ {{{ yesno_inv b ∗ has_fuel tid Y f ∗ ⌜N > 0⌠∗ yes_at N }}}
yes #N #b @ tid
{{{ RET #(); tid ↦M ∅ }}}.
Proof.
- iIntros (Φ) "(#Hinv & Hf & %HN & Hyes & Hyesf) Hk". unfold yes.
+ iIntros (Φ) "(#Hinv & Hf & %HN & Hyes) Hk". unfold yes.
wp_pures.
wp_bind (Alloc _).
@@ -378,159 +360,155 @@ Section proof.
iApply (yes_go_spec with "[-Hk]"); try iFrame.
{ lia. }
- { iFrame "Hinv". done. }
+ { iFrame "Hinv". iPureIntro; lia. }
Qed.
- Lemma no_go_spec tid n b (N: nat) f (Hf: f > 17):
- {{{ yesno_inv b ∗ has_fuel tid No f ∗ n ↦ #N ∗ ⌜N > 0⌠∗ no_at N ∗ no_finished true }}}
+ Lemma no_go_spec tid n b (N: nat) f (Hf: f > 40):
+ {{{ yesno_inv b ∗ has_fuel tid No f ∗ n ↦ #N ∗ ⌜N > 0⌠∗ no_at N }}}
no_go #n #b @ tid
{{{ RET #(); tid ↦M ∅ }}}.
Proof.
iLöb as "Hg" forall (N f Hf).
- iIntros (Φ) "(#Hinv & Hf & HnN & %HN & Hno & Hnof) Hk". unfold no_go.
+ iIntros (Φ) "(#Hinv & Hf & HnN & %HN & Hno) Hk". unfold no_go.
wp_pures.
-
wp_bind (CmpXchg _ _ _).
- rewrite -has_fuel_fuels.
+ assert (∀ s, Atomic s (CmpXchg #b #true #false)) by apply _.
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 %->.
- destruct B; iDestruct "Hauths" as "[>Hay >Han]"; last first.
- - iDestruct (no_agree with "Hno Han") as "%H". rewrite -> H in *. clear H.
- iApply (wp_cmpxchg_suc_step_singlerole _ tid (No: fmrole the_model) _ 30%nat
- (N, false, yf, true) (N-1, true, yf, true)
- with "[$]"); eauto.
- { simpl. lia. }
- { simpl. destruct N as [|N]; first lia. rewrite /= Nat.sub_0_r.
- destruct yf; first econstructor. destruct N as [|N]; try econstructor.
- by have ?: false = true by lia. }
- iModIntro.
- iIntros "!> (Hb & Hmod & Hf)".
- iMod (no_update (N-1) with "[$]") as "[Han Hno]".
- iMod ("Hclose" with "[Hmod Hb Hay Han Hanof Hayesf]").
- { iNext. iExists (N-1), true, yf, true. iFrame. iPureIntro; intros; split; last lia.
- intros. apply Htrue. lia. }
- simpl.
-
- destruct N as [|N]; first lia. rewrite decide_True; last first.
- { destruct N; set_solver. }
+ iInv Ns as (M B) "(>HFR & >Hmod & >Bb & Hauths & >%Hnever)" "Hclose".
+ destruct B; iDestruct "Hauths" as "[>Hay >Han]"; last first.
+ - iDestruct (no_agree with "Hno Han") as "%Heq".
- iModIntro.
- wp_pures.
- wp_load.
- wp_pures.
- wp_store.
- wp_pures.
- wp_load.
- wp_pures.
+ (* TODO *)
+ rewrite -has_fuel_fuels.
- destruct (decide (0 < S N - 1)) as [Heq|Heq].
- + rewrite bool_decide_eq_true_2 //; last lia.
+ destruct (decide (M = 0)) as [->|Nneq]; first lia.
+ destruct (decide (M = 1)) as [->|Nneq1].
+ + iApply (wp_cmpxchg_suc_step_singlerole_keep_dead _ tid (No: fmrole the_model) _ 30%nat _
+ (1, false) (0, true)
+ with "[$]") =>//.
+ { lia. }
+ { econstructor. }
+ iModIntro.
+ iIntros "!> (Hb & Hmod & HFR & Hf)".
+ iMod (no_update 0 with "[$]") as "[Han Hno]".
+ iMod ("Hclose" with "[Hmod Hb Hay Han HFR]").
+ { iNext. iExists _, _. iFrame. simpl. iFrame. by iPureIntro. }
+
+ iModIntro.
+
+ rewrite has_fuel_fuels.
+ wp_pures.
+ wp_load.
+ wp_pures.
+ wp_store.
+ wp_pures.
+ wp_load.
wp_pure _.
-
- rewrite -has_fuel_fuels.
- iApply ("Hg" with "[] [Hno HnN Hf Hnof] [$]"); last first.
- { iFrame "∗#". iSplit; last (iPureIntro; lia).
- 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.
- have ->: N = 0 by lia. simpl.
-
- clear M. clear Htrue Htrue' yf.
+ simplify_eq. simpl.
iApply wp_atomic.
- iInv Ns as (M B yf nf) "(>[%Htrue %Htrue'] & >Hayesf & >Hanof & >Hmod & >Hb & Hauths)" "Hclose".
-
- destruct B as [|].
- * iDestruct "Hauths" as "[>Hay >Han]".
- 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.
- { set_solver. }
- { lia. }
- { econstructor. }
- iFrame. iModIntro.
- iMod (no_finished_update false with "[$]") as "[Hanof Hnof]".
- iModIntro. iNext. iModIntro.
- rewrite -wp_value.
-
- have Hnotin: No ∉ live_roles the_model (0, true, yf, false).
- { destruct yf; simpl; set_solver. }
- rewrite decide_False //. iIntros "Hmod".
-
- iMod ("Hclose" with "[- Hk]").
- { iNext. iExists 0, true, yf, false. iFrame. iPureIntro; lia. }
- iIntros "Hccl". iModIntro. iApply ("Hk" with "Hccl").
- * iDestruct "Hauths" as "[>Hay >Hano]".
- 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.
- { set_solver. }
- { lia. }
- { econstructor. }
- iFrame. iModIntro.
-
- iMod (no_finished_update false with "[$]") as "[Hanof Hnof]".
- iModIntro. iNext. iModIntro. iIntros "Hmod".
-
- have Hnotin: No ∉ live_roles the_model (0, false, yf, false).
- { destruct yf; simpl; set_solver. }
- rewrite decide_False //. iIntros "Hccl".
-
- rewrite -wp_value.
- iMod ("Hclose" with "[-Hk Hccl]").
- { iNext. iExists 0, false, yf, false. iFrame. iPureIntro; split; intros; lia. }
- iModIntro. iApply ("Hk" with "Hccl").
-
- - iDestruct (no_agree with "Hno Han") as "%H". rewrite -> H in *.
+
+ iInv Ns as (M B) "(>HFR & >Hmod & >Hb & Hauths & >%Hbever')" "Hclose".
+
+ destruct B.
+ * iApply (wp_lift_pure_step_no_fork_remove_role {[ No ]} ((0, true): fmstate the_model) _ _ _ _ _ _ {[ No := _ ]}) =>//.
+ { apply map_non_empty_singleton. }
+ { rewrite dom_singleton. set_solver. }
+ { simpl. set_solver. }
+
+ repeat iModIntro.
+
+ iDestruct "Hauths" as "[Hay Han]". iDestruct (no_agree with "Hno Han") as %Heq.
+ assert (M = 0) by lia. simplify_eq. iFrame "Hmod". iSplitL "Hf".
+ { rewrite /has_fuels_S fmap_insert fmap_empty //. }
+ iIntros "Hmod Hf".
+
+ wp_pures. repeat iModIntro.
+ iMod ("Hclose" with "[Hmod Hay Han Hb HFR]").
+ { iNext. iExists _, _. iFrame. done. }
+ iModIntro. iApply "Hk".
+ rewrite map_filter_singleton_False; last set_solver. rewrite /has_fuels dom_empty_L.
+ iDestruct "Hf" as "[??]". iFrame.
+ * iDestruct "Hauths" as "[>Hay >Han]". iDestruct (no_agree with "Hno Han") as %Heq.
+ assert (M = 0) by lia. simplify_eq.
+ + assert (N = N) by lia. simplify_eq.
+ destruct M; first done.
+
+ iApply (wp_cmpxchg_suc_step_singlerole _ tid (No: fmrole the_model) _ 55%nat _
+ (S M, false) (M, true)
+ with "[$]"); eauto.
+ { simpl. lia. }
+ { econstructor. }
+ { simpl. destruct M; [set_solver | destruct M; set_solver]. }
+ iModIntro.
+ iIntros "!> (Hb & Hmod & HFR & Hf)".
+ iMod (no_update (M) with "[$]") as "[Han Hno]".
+ iMod ("Hclose" with "[Hmod Hay Han Hb HFR]").
+ { iNext. iExists _, _. iFrame. iSplit; last by iPureIntro.
+ iApply (own_proper with "Hay"). f_equiv. apply leibniz_equiv_iff. lia. }
+
+ iModIntro. rewrite decide_True; last first.
+ { do 2 (destruct M; try done); set_solver. }
+
+ rewrite has_fuel_fuels.
+ wp_pures.
+ wp_load.
+ wp_pures.
+ wp_store.
+ wp_pures.
+ wp_load.
+ wp_pures.
+
+ destruct (decide (0 < S M - 1)) as [Heq|Heq].
+ * rewrite bool_decide_eq_true_2 //; last lia.
+ wp_pure _.
+
+ rewrite -has_fuel_fuels.
+ iApply ("Hg" with "[] [Hno HnN Hf] [$]"); last first.
+ { iFrame "∗#". assert ((S M - 1)%Z = M)%nat as -> by lia. iFrame. iPureIntro; lia. }
+ iPureIntro; lia.
+ * rewrite bool_decide_eq_false_2 //; last lia.
+ have ->: M = 0 by lia. simpl. lia.
+ - iDestruct (no_agree with "Hno Han") as "%Heq". rewrite -> Heq in *.
have HM: M > 0 by lia.
- (* rewrite (Htrue' HM). *)
- iApply (wp_cmpxchg_fail_step_singlerole _ tid (No: fmrole the_model) _ 30%nat
- (N, true, yf, true) (N, true, yf, true)
+
+ rewrite -has_fuel_fuels. assert (M = N) by lia. simplify_eq.
+ iApply (wp_cmpxchg_fail_step_singlerole _ tid (No: fmrole the_model) _ 50%nat _
+ (N, true) (N, true)
with "[$]"); eauto.
{ simpl. lia. }
- { rewrite Htrue; last by right; lia. econstructor. }
- iModIntro. iIntros "!> (Hb & Hmod & Hf)".
- (* iMod (yes_update (N-1) with "[$]") as "[Hay Hyes]". *)
- iMod ("Hclose" with "[Hmod Hb Hay Han Hanof Hayesf]").
- { iNext. iExists N, true, yf, true. iFrame. iPureIntro; intros. split=>//. }
- simpl.
+ { econstructor. lia. }
+ iIntros "!>!> (Hb & Hmod & HFR & Hf)".
+ iMod ("Hclose" with "[Hmod Hb Hay Han HFR]").
+ { iNext. simplify_eq. iExists _, _. iFrame. iSplit; [iFrame|done]. }
- destruct N as [|N]; first lia. rewrite decide_True; last first.
- { destruct N; set_solver. }
+ rewrite decide_True; last first.
+ { destruct N; [lia|destruct N; set_solver]. }
iModIntro.
wp_pures.
wp_load.
- do 2 wp_pure _.
+ wp_pure _. rewrite bool_decide_eq_true_2; last lia.
+ wp_pure _.
rewrite -has_fuel_fuels.
- iApply ("Hg" with "[] [-Hk] [$]"); last first.
+ iApply ("Hg" with "[] [Hno HnN Hf] [$]"); last first.
{ iFrame "∗#". iPureIntro; lia. }
iPureIntro; lia.
Qed.
- Lemma no_spec tid b (N: nat) f (Hf: f > 25):
- {{{ yesno_inv b ∗ has_fuel tid No f ∗ ⌜N > 0⌠∗ no_at N ∗ no_finished true }}}
+ Lemma no_spec tid b (N: nat) f (Hf: f > 50):
+ {{{ yesno_inv b ∗ has_fuel tid No f ∗ ⌜N > 0⌠∗ no_at N }}}
no #N #b @ tid
{{{ RET #(); tid ↦M ∅ }}}.
Proof.
- iIntros (Φ) "(#Hinv & Hf & %HN & Hyes & Hyesf) Hk". unfold no.
+ iIntros (Φ) "(#Hinv & Hf & %HN & Hyes) Hk". unfold no.
wp_pures.
wp_bind (Alloc _).
@@ -558,13 +536,13 @@ Section proof_start.
Context `{!heapGS Σ the_model, !yesnoPreG Σ}.
Let Ns := nroot .@ "yes_no".
- Lemma start_spec tid (N: nat) f (Hf: f > 40):
- {{{ frag_model_is (N, true, true, true) ∗
+ Lemma start_spec tid (N: nat) f (Hf: f > 60):
+ {{{ frag_model_is (N, true) ∗ frag_free_roles_are ∅ ∗
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.
+ iIntros (Φ) "[Hst [HFR [Hf %HN]]] Hkont". unfold start.
wp_pures.
@@ -579,32 +557,25 @@ Section proof_start.
wp_pures.
(* Allocate the invariant. *)
- iMod (own_alloc (â—E N â‹… â—¯E N)) as (γ_yes_at) "[Hyes_at_auth Hyes_at]".
- { apply auth_both_valid_2; eauto. by compute. }
- iMod (own_alloc (â—E N â‹… â—¯E N)) as (γ_no_at) "[Hno_at_auth Hno_at]".
- { apply auth_both_valid_2; eauto. by compute. }
- iMod (own_alloc (â—E true â‹… â—¯E true)) as (γ_yes_fin) "[Hyes_fin_auth Hyes_fin]".
+ iMod (own_alloc (â—E N â‹… â—¯E N))%nat as (γ_yes_at) "[Hyes_at_auth Hyes_at]".
{ apply auth_both_valid_2; eauto. by compute. }
- iMod (own_alloc (â—E true â‹… â—¯E true)) as (γ_no_fin) "[Hno_fin_auth Hno_fin]".
+ iMod (own_alloc (â—E N â‹… â—¯E N))%nat as (γ_no_at) "[Hno_at_auth Hno_at]".
{ apply auth_both_valid_2; eauto. by compute. }
pose (the_names := {|
yes_name := γ_yes_at;
- yes_f_name := γ_yes_fin;
no_name := γ_no_at;
- no_f_name := γ_no_fin;
|}).
iApply fupd_wp.
- iMod (inv_alloc Ns _ (yesno_inv_inner l) with "[-Hkont Hf Hyes_at Hno_at Hyes_fin Hno_fin]") as "#Hinv".
- { iNext. unfold yesno_inv_inner. iExists N, true, true, true.
- iSplit; first done. iFrame. }
+ iMod (inv_alloc Ns _ (yesno_inv_inner l) with "[-Hkont Hf Hyes_at Hno_at]") as "#Hinv".
+ { iNext. unfold yesno_inv_inner. iExists N, true. iFrame. done. }
iModIntro.
wp_bind (Fork _).
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]");
+ with "[Hyes_at] [- 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.
@@ -624,7 +595,7 @@ Section proof_start.
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]");
+ iApply (wp_fork_nostep _ tid _ _ _ ∅ {[ No ]} {[No := _]} with "[Hno_at] [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.
diff --git a/fairness/examples/yesno_adequacy.v b/fairness/examples/yesno_adequacy.v
index c8533d3..b09f1bd 100644
--- a/fairness/examples/yesno_adequacy.v
+++ b/fairness/examples/yesno_adequacy.v
@@ -83,69 +83,47 @@ Section unstrict_order.
x = y ∨ lt x y.
End unstrict_order.
-Definition the_order (s1 s2: the_model): Prop :=
- match s1, s2 with
- | (N1, B1, yf1, nf1), (N2, B2, yf2, nf2) =>
- prod_relation
- (unstrict (lexprod _ _ (strict Nat.le) (strict bool_le)))
- (prod_relation bool_le bool_le)
- (N1, B1, (yf1, nf1))
- (N2, B2, (yf2, nf2))
- end.
+Definition the_order := unstrict (lexprod _ _ (strict Nat.le) (strict bool_le)).
Ltac inv_lexs :=
repeat match goal with
[ H: lexprod _ _ _ _ _ _ |- _ ] => inversion H; clear H; simplify_eq
end.
+Lemma lexprod_lexico x y:
+ lexprod _ _ (strict Nat.le) (strict bool_le) x y <-> lexico x y.
+Proof.
+ split.
+ - intros [???? H|x' y' z' H].
+ + left =>/=. compute. compute in H. lia.
+ + right =>/=. compute; split=>//. compute in H. destruct y'; destruct z' =>//; intuition.
+ - destruct x as [x1 x2]. destruct y as [y1 y2]. intros [H|[Heq H]]; simpl in *.
+ + left =>/=. compute. compute in H. lia.
+ + rewrite Heq. right =>/=. destruct x2; destruct y2 =>//; intuition. constructor =>//. eauto.
+Qed.
#[local] Instance the_order_po: PartialOrder the_order.
Proof.
constructor.
- constructor.
- + intros x. destruct x as [[[??]?]?]. simpl.
- unfold prod_relation. simpl. split; last done.
- by econstructor.
- + intros [[[??]?]?] [[[??]?]?] [[[??]?]?]. simpl.
- unfold prod_relation. simpl. intros (Hlex1&?&?) (Hlex2&?&?). split; last first.
- * split; etransitivity =>//.
- * inversion Hlex1; inversion Hlex2; simplify_eq;
- try (econstructor 1; try (etransitivity; done); inv_lexs; f_equal; done);
- try (econstructor 2; try done).
- inv_lexs.
- ** econstructor. by etransitivity.
- ** econstructor 1 =>//.
- ** econstructor => //.
- ** econstructor 2. by etransitivity.
- - intros [[[??]?]?] [[[??]?]?]. simpl.
- unfold prod_relation. simpl. intros (Hlex1&?&?) (Hlex2&?&?).
- do 3 f_equal; try (by eapply anti_symm =>//).
- + inversion Hlex1; inversion Hlex2; simplify_eq; try (eapply anti_symm =>//; done);
- inv_lexs; eauto. exfalso; eapply (strict_anti_symm (R := strict Nat.le)) =>//; eapply _.
- + inversion Hlex1; inversion Hlex2; simplify_eq; try (eapply anti_symm =>//; done);
- inv_lexs; eauto; try by eapply anti_symm;
- exfalso; eapply (strict_anti_symm (R := strict Nat.le)); eauto.
- exfalso; eapply (strict_anti_symm (R := strict bool_le)); eauto.
- + eapply anti_symm =>//; apply _.
- + eapply anti_symm =>//; apply _.
- Unshelve. all: exact eq.
+ + intros ?. by left.
+ + unfold the_order. intros [x1 x2] [y1 y2] [z1 z2] [|H1] [|H2]; simplify_eq; try (by left); right; eauto.
+ rewrite -> lexprod_lexico in *. etransitivity =>//.
+ - intros [x1 x2] [y1 y2] [|H1] [|H2]; simplify_eq =>//.
+ inversion H1; inversion H2; simplify_eq; try (compute in *; lia).
+ destruct x2; destruct y2; compute in *; intuition.
Qed.
Definition the_decreasing_role (s: the_model): YN :=
match s with
- | (0%nat, false, true, false) => Y
- | (0%nat, true, false, true) => No
- | (1%nat, false, true, false) => Y
- | (_, true, _, _) => Y
- | (_, false, _, _) => No
+ | (0%nat, false) => Y
+ | (_, true) => Y
+ | (_, false) => No
end.
#[local] Instance eq_antisymm A: Antisymmetric A eq eq.
Proof. by intros ??. Qed.
-Definition same: the_model -> (nat * bool * (bool * bool)) :=
- λ '(N, B, yf, nf), (N, B, (yf, nf)).
-
Lemma strict_unstrict {A} (R: relation A):
forall x y, strict (unstrict R) x y -> R x y.
Proof.
@@ -171,95 +149,63 @@ Proof.
- constructor 2. etransitivity =>//.
Qed.
-#[local] Instance test1 `{Transitive A R}: Transitive (unstrict R).
-Proof.
- intros x y z [?|?] [?|?]; simplify_eq; ((left; done) || right; eauto).
-Qed.
-
-Lemma the_model_almost_wf:
- wf (strict $
- prod_relation
- (unstrict (lexprod _ _ (strict Nat.le) (strict bool_le)))
- (prod_relation bool_le bool_le)).
-Proof.
- apply wf_prod_strict.
- - apply _.
- - assert (H: wf (lexprod nat bool (strict Nat.le) (strict bool_le))).
- + apply wf_lexprod; last apply wf_bool_le.
- eapply (wf_projected _ id); last apply Nat.lt_wf_0.
- intros ??[??]. simpl. lia.
- + eapply (wf_projected _ id); last exact H.
- intros ???. apply strict_unstrict => //.
- - apply wf_prod_strict; eauto using wf_bool_le.
- apply _.
-Qed.
-
-
-
#[local] Program Instance the_model_terminates: FairTerminatingModel the_model :=
{|
ftm_leq := the_order;
ftm_decreasing_role := the_decreasing_role;
|}.
Next Obligation.
- eapply (wf_projected _ same); last exact the_model_almost_wf.
- intros [[[? ?] ?] ?] [[[? ?] ? ]?] ?. eauto.
+ unfold the_order.
+ assert (H: wf (lexprod nat bool (strict Nat.le) (strict bool_le))).
+ + apply wf_lexprod; last apply wf_bool_le.
+ eapply (wf_projected _ id); last apply Nat.lt_wf_0.
+ intros ??[??]. simpl. lia.
+ + eapply (wf_projected _ id); last exact H.
+ intros ???. apply strict_unstrict => //.
Qed.
Next Obligation.
- intros [[[N B] yf] nf] Hex.
+ intros [N B] Hex.
destruct B.
- split.
- + simpl. destruct yf.
- * do 2 (destruct N; try set_solver).
+ + simpl. destruct N.
* destruct Hex as [Ï' [s' Hex]].
- inversion Hex; subst. set_solver.
- + intros [[[N' B'] yf'] nf'] Htrans.
- inversion Htrans; simplify_eq; rewrite strict_spec_alt; (split; [| try done; do 2 (destruct N'; eauto)]);
- (constructor; [simpl; eauto; unfold unstrict; (try by left) |]).
- { right. constructor 2. constructor; eauto. constructor. }
- all: simpl; by constructor.
+ inversion Hex; subst; lia.
+ * destruct N; set_solver.
+ + intros [??] H. inversion H; simplify_eq.
+ * split; [right; right; compute; done| compute; intros [?|contra] =>//].
+ inversion contra; simplify_eq; intuition.
+ * destruct n =>//.
- split.
- + simpl. destruct nf.
- * destruct N; simpl; destruct yf; try set_solver; destruct N; set_solver.
+ + destruct N; simpl.
* destruct Hex as [Ï' [s' Hex]].
- inversion Hex; subst. destruct N; try set_solver.
- destruct N; try set_solver. lia.
- + intros [[[N' B'] yf'] nf'] Htrans.
- inversion Htrans; simplify_eq; rewrite strict_spec_alt; (split; [| try done; do 2 (destruct N'; eauto)]);
- (constructor ; [simpl; eauto; unfold unstrict; (try by left) |]).
- all: simpl; try by constructor.
- all: right; constructor 1; split; lia.
+ inversion Hex; subst; lia.
+ * destruct N; set_solver.
+ + intros [[|?] ?] H.
+ * inversion H; simplify_eq; [lia|]. unfold strict, the_order; split.
+ ** right; left. compute. lia.
+ ** intros [|contra] =>//. inversion contra; simplify_eq. compute in *. lia.
+ * inversion H; simplify_eq. split; [right;left; compute; lia|].
+ intros [|contra] =>//; inversion contra; simplify_eq; last lia. compute in *. lia.
Qed.
Next Obligation.
- intros [[[N B] yf] nf] [[[N' B'] yf'] nf'] Ï Htrans Hnex.
+ intros [N B] [N' B'] Ï Htrans Hnex.
inversion Htrans ; simplify_eq; eauto; simpl in *;
try (destruct N'; eauto); try lia; (try (destruct N'; done)); try done.
- - destruct yf'; done.
- - destruct B'; try done. destruct nf'; done.
- - have ?: N' = 0%nat by lia. subst. destruct B' =>//.
- destruct nf'=>//.
- - destruct B' =>//; destruct yf' =>//.
Qed.
Next Obligation.
- intros [[[N B] yf] nf] Ï [[[N' B'] yf'] nf'] Htrans.
+ intros [N B] Ï [N' B'] Htrans.
destruct Ï; last by inversion Htrans.
- inversion Htrans; simplify_eq; simpl.
- all: constructor; [((left; done) || right; (constructor 1; constructor; done) || (try constructor 2)); simpl | simpl; try reflexivity].
- - constructor. constructor. eauto.
- - constructor 1; split; lia.
- - constructor 1; split; lia.
- - constructor. constructor. eauto. done.
- - constructor; done.
+ inversion Htrans; simplify_eq; simpl; try reflexivity.
+ - right; constructor 2; by compute.
+ - right; constructor 1; compute. lia.
Qed.
(* The model is finitely branching *)
-Definition steppable '(n, w, yf, nf): list ((nat * bool * bool * bool) * option YN) :=
+Definition steppable '(n, w): list ((nat * bool) * option YN) :=
n' ↠[n; (n-1)%nat];
w' ↠[w; negb w];
- yf' ↠[yf; negb yf];
- nf' ↠[nf; negb nf];
ℓ ↠[Some Y; Some No];
- mret ((n', w', yf', nf'), â„“).
+ mret ((n', w'), â„“).
#[local] Instance proof_irrel_trans s x:
ProofIrrel ((let '(s', â„“) := x in yntrans s â„“ s'): Prop).
@@ -270,14 +216,14 @@ Lemma model_finitary s:
Proof.
assert (H: forall A (y x: A) xs, (y = x ∨ y ∈ xs) -> y ∈ x::xs) by set_solver.
eapply (in_list_finite (steppable s)).
- intros [[[n w] yf] nf] Htrans.
+ intros [n w] Htrans.
inversion Htrans; try (repeat (rewrite ?Nat.sub_0_r; simpl;
eapply H; try (by left); right); done).
Qed.
Theorem yesno_terminates
(N : nat)
- (HN: N > 0)
+ (HN: N > 1)
(extr : extrace)
(Hvex : extrace_valid extr)
(Hexfirst : (trfirst extr).1 = [start #N]):
@@ -285,22 +231,21 @@ Theorem yesno_terminates
Proof.
assert (heapGpreS yesnoΣ the_model) as HPreG.
{ apply _. }
- eapply (simulation_adequacy_terminate_ftm (Mdl := the_model) yesnoΣ NotStuck _ (N, true, true, true)) =>//.
+ eapply (simulation_adequacy_terminate_ftm (Mdl := the_model) yesnoΣ NotStuck _ (N, true) ∅) =>//.
- eapply valid_state_evolution_finitary_fairness.
intros ?. simpl. apply (model_finitary s1).
- - set_solver.
- - intros ?. iStartProof. iIntros "!> Hm Hf !>". simpl.
- iApply (start_spec _ _ 45 with "[Hm Hf]"); eauto.
- + lia.
- + iSplitL "Hm"; eauto. iSplit; last done.
- assert ({[Y := 45%nat; No := 45%nat]} = gset_to_gmap 45 {[Y; No]}) as <-; last done.
+ - destruct N; [lia|destruct N; set_solver].
+ - intros ?. iStartProof. iIntros "!> Hm HFR Hf !>". simpl.
+ iApply (start_spec _ _ 61 with "[Hm Hf HFR]"); eauto.
+ + iSplitL "Hm"; eauto. do 2 (destruct N; first lia).
+ assert (∅ ∖ {[ No; Y ]} = ∅) as -> by set_solver. iFrame. iSplit; last (iPureIntro; lia).
+ assert ({[Y := 61%nat; No := 61%nat]} = gset_to_gmap 61 {[No;Y]}) as <-; last done.
rewrite -leibniz_equiv_iff. intros Ï.
- destruct (gset_to_gmap 45 {[Y; No]} !! Ï) as [f|] eqn:Heq.
+ destruct (gset_to_gmap 61 {[Y; No]} !! Ï) as [f|] eqn:Heq.
* apply lookup_gset_to_gmap_Some in Heq as [Heq ->].
destruct (decide (Ï = Y)) as [-> |].
- ** rewrite lookup_insert //.
+ ** rewrite lookup_insert //. rewrite lookup_gset_to_gmap option_guard_True //. set_solver.
** rewrite lookup_insert_ne //. assert (Ï = No) as -> by set_solver.
- rewrite lookup_insert //.
- * apply lookup_gset_to_gmap_None in Heq.
- repeat (rewrite lookup_insert_ne //; last set_solver).
+ rewrite lookup_insert // lookup_gset_to_gmap option_guard_True //. set_solver.
+ * apply lookup_gset_to_gmap_None in Heq. destruct Ï; set_solver.
Qed.
diff --git a/fairness/fairness.v b/fairness/fairness.v
index 832985c..c0c4390 100644
--- a/fairness/fairness.v
+++ b/fairness/fairness.v
@@ -27,83 +27,6 @@ Record FairModel : Type := {
}.
Arguments fuel_limit {_}.
-Section from_locale.
- Context {Λ: language}.
- Context `{ EqDecision (locale Λ)}.
-
- Fixpoint from_locale_from tp0 tp ζ :=
- match tp with
- | [] => None
- | e::tp' => if decide (locale_of tp0 e = ζ) then Some e else from_locale_from (tp0 ++ [e]) tp' ζ
- end.
-
- Definition from_locale tp ζ := from_locale_from [] tp ζ.
-
- (* Other possibility is:
- Definition from_locale tp ζ := list_find (λ '(tp, e), locale_of tp e = ζ) (prefixes tp).*)
-
- Lemma from_locale_from_Some_app tp0 tp tp' ζ e :
- from_locale_from tp0 tp ζ = Some e ->
- from_locale_from tp0 (tp ++ tp') ζ = Some e.
- Proof.
- revert tp0 tp'. induction tp as [|e' tp IH]; first by list_simplifier.
- simpl. intros tp0 tp' Hfl.
- destruct (decide (locale_of tp0 e' = ζ)) =>//.
- apply IH =>//.
- Qed.
-
- Lemma from_locale_from_is_Some_app tp0 tp tp' ζ :
- is_Some (from_locale_from tp0 tp ζ) ->
- is_Some (from_locale_from tp0 (tp ++ tp') ζ).
- Proof.
- intros [? HS]. eapply from_locale_from_Some_app in HS. eauto.
- Qed.
-
- Lemma from_locale_from_equiv tp0 tp0' tp tp' ζ :
- locales_equiv tp0 tp0' ->
- locales_equiv_from tp0 tp0' tp tp' ->
- is_Some (from_locale_from tp0 tp ζ) ->
- is_Some (from_locale_from tp0' tp' ζ).
- Proof.
- revert tp0 tp0' tp'. induction tp as [|e tp IH]; intros tp0 tp0' tp' Heq0 Heq [eζ Heζ];
- destruct tp' as [|e' tp']; try by apply Forall2_length in Heq.
- simpl in *.
- destruct (decide (locale_of tp0 e' = ζ)).
- - rewrite decide_True //; eauto. erewrite <-locale_equiv =>//.
- - rewrite decide_False; last by erewrite <-locale_equiv.
- apply Forall2_cons_1 in Heq as [Hlocs ?].
- rewrite decide_False // in Heζ; last by erewrite Hlocs, <-locale_equiv =>//.
- apply (IH (tp0 ++ [e])); eauto.
- apply locales_equiv_snoc =>//. constructor.
- Qed.
-
- Lemma from_locale_step tp1 tp2 ζ oζ σ1 σ2 :
- locale_step (tp1, σ1) oζ (tp2, σ2) →
- is_Some(from_locale tp1 ζ) →
- is_Some(from_locale tp2 ζ).
- Proof.
- intros Hstep. inversion Hstep; simplify_eq=>//.
- intros HiS. replace (t1 ++ e2 :: t2 ++ efs) with ((t1 ++ e2 :: t2) ++ efs);
- last by list_simplifier.
- apply from_locale_from_is_Some_app.
- eapply from_locale_from_equiv; eauto; [constructor|].
- apply locales_equiv_from_middle. list_simplifier. by eapply locale_step_preserve.
- Qed.
-
- Lemma from_locale_from_Some tp0 tp1 tp e :
- (tp, e) ∈ prefixes_from tp0 tp1 →
- from_locale_from tp0 tp1 (locale_of tp e) = Some e.
- Proof.
- revert tp0 tp e; induction tp1 as [| e1 tp1 IH]; intros tp0 tp e Hin; first set_solver.
- apply elem_of_cons in Hin as [Heq|Hin].
- { simplify_eq. rewrite /= decide_True //. }
- rewrite /= decide_False; first by apply IH.
- fold (prefixes_from (A := expr Λ)) in Hin.
- by eapply locale_injective.
- Qed.
-
-End from_locale.
-
#[global] Existing Instance fmrole_eqdec.
#[global] Existing Instance fmrole_countable.
#[global] Existing Instance fmrole_inhabited.
@@ -117,17 +40,22 @@ Section fairness.
ls_under:> M.(fmstate);
ls_fuel: gmap M.(fmrole) nat;
- ls_fuel_dom: dom ls_fuel = M.(live_roles) ls_under;
+ ls_fuel_dom: M.(live_roles) ls_under ⊆ dom ls_fuel;
ls_mapping: gmap M.(fmrole) (locale Λ); (* maps roles to thread id *)
- ls_mapping_dom: dom ls_mapping = M.(live_roles) ls_under;
+
+ ls_same_doms: dom ls_mapping = dom ls_fuel;
}.
Arguments ls_under {_}.
Arguments ls_fuel {_}.
Arguments ls_fuel_dom {_}.
Arguments ls_mapping {_}.
- Arguments ls_mapping_dom {_}.
+ Arguments ls_same_doms {_}.
+
+ Lemma ls_mapping_dom M (m: LiveState M):
+ M.(live_roles) m.(ls_under) ⊆ dom m.(ls_mapping).
+ Proof. rewrite ls_same_doms. apply ls_fuel_dom. Qed.
Inductive FairLabel {Roles} :=
| Take_step: Roles -> locale Λ -> FairLabel
@@ -147,8 +75,10 @@ Section fairness.
must_decrease Ï' oÏ a b (Some tid)
| Change_tid otid (Hneqtid: a.(ls_mapping) !! Ï' ≠b.(ls_mapping) !! Ï')
(Hissome: is_Some (b.(ls_mapping) !! Ï')):
- must_decrease Ï' oÏ a b otid.
-
+ must_decrease Ï' oÏ a b otid
+ | Zombie otid (Hismainrole: oÏ = Some Ï') (Hnotalive: Ï' ∉ live_roles _ b) (Hnotdead: Ï' ∈ dom b.(ls_fuel)):
+ must_decrease Ï' oÏ a b otid
+ .
Definition oleq a b :=
match a, b with
@@ -168,12 +98,14 @@ Section fairness.
Qed.
Definition fuel_decr {M: FairModel} (tid: olocale Λ) (oÏ: option M.(fmrole)) (a b: LiveState M) :=
- forall Ï', Ï' ∈ M.(live_roles) a.(ls_under) ->
+ forall Ï', Ï' ∈ dom a.(ls_fuel) -> Ï' ∈ dom b.(ls_fuel) →
must_decrease Ï' oÏ a b tid
-> oless (b.(ls_fuel) !! Ï') (a.(ls_fuel) !! Ï').
Definition fuel_must_not_incr {M: FairModel} oÏ (a b: LiveState M) :=
- ∀ Ï', Ï' ∈ live_roles _ a -> Some Ï' ≠oÏ -> oleq ((ls_fuel b) !! Ï') ((ls_fuel a) !! Ï').
+ ∀ Ï', Ï' ∈ dom a.(ls_fuel) -> Some Ï' ≠oÏ ->
+ (oleq ((ls_fuel b) !! Ï') ((ls_fuel a) !! Ï')
+ ∨ (Ï' ∉ dom b.(ls_fuel) ∧ Ï' ∉ M.(live_roles) a.(ls_under))).
Definition ls_trans {M} (a: LiveState M) â„“ (b: LiveState M): Prop :=
match â„“ with
@@ -183,17 +115,20 @@ Section fairness.
∧ fuel_decr (Some tid) (Some Ï) a b
∧ fuel_must_not_incr (Some Ï) a b
∧ (Ï âˆˆ live_roles _ b -> oleq (b.(ls_fuel) !! Ï) (Some (fuel_limit b)))
- ∧ ∀ Ï, Ï âˆˆ M.(live_roles) b ∖ M.(live_roles) a -> oleq (b.(ls_fuel) !! Ï) (Some (fuel_limit b))
+ ∧ (∀ Ï, Ï âˆˆ dom b.(ls_fuel) ∖ dom a.(ls_fuel) -> oleq (b.(ls_fuel) !! Ï) (Some (fuel_limit b)))
+ ∧ dom b.(ls_fuel) ∖ dom a.(ls_fuel) ⊆ live_roles _ b ∖ live_roles _ a
| Silent_step tid =>
- (∃ Ï, a.(ls_mapping) !! Ï = Some tid) ∧
- fuel_decr (Some tid) None a b
+ (∃ Ï, a.(ls_mapping) !! Ï = Some tid)
+ ∧ fuel_decr (Some tid) None a b
∧ fuel_must_not_incr None a b
+ ∧ dom b.(ls_fuel) ⊆ dom a.(ls_fuel)
∧ a.(ls_under) = b.(ls_under)
| Config_step =>
M.(fmtrans) a None b
∧ fuel_decr None None a b
∧ fuel_must_not_incr None a b
- ∧ ∀ Ï, Ï âˆˆ M.(live_roles) b ∖ M.(live_roles) a -> oleq (b.(ls_fuel) !! Ï) (Some (fuel_limit b))
+ ∧ (∀ Ï, Ï âˆˆ M.(live_roles) b ∖ M.(live_roles) a -> oleq (b.(ls_fuel) !! Ï) (Some (fuel_limit b)))
+ ∧ False (* TODO: add support for config steps later! *)
end.
Definition fair_model M: Model := {|
@@ -210,8 +145,8 @@ Section fairness.
ls_fuel := gset_to_gmap (fuel_limit s0) (M.(live_roles) s0);
ls_mapping := gset_to_gmap ζ0 (M.(live_roles) s0);
|}.
- Next Obligation. eauto using dom_gset_to_gmap. Qed.
- Next Obligation. eauto using dom_gset_to_gmap. Qed.
+ Next Obligation. intros ???. apply reflexive_eq. rewrite dom_gset_to_gmap //. Qed.
+ Next Obligation. intros ???. apply reflexive_eq. rewrite !dom_gset_to_gmap //. Qed.
Definition labels_match {M} (oζ : olocale Λ) (ℓ : @FairLabel (M.(fmrole))) :=
match oζ, ℓ with
@@ -646,6 +581,11 @@ Section lex_ind.
End lex_ind.
+Ltac SS :=
+ epose proof ls_fuel_dom;
+ (* epose proof ls_mapping_dom; *)
+ set_solver.
+
Section fairness_preserved.
Context {M: FairModel}.
Context {Λ: language}.
@@ -705,11 +645,11 @@ Section fairness_preserved.
Lemma mapping_live_role (δ: LiveState M) Ï:
Ï âˆˆ M.(live_roles) δ ->
is_Some (ls_mapping (Λ := Λ) δ !! Ï).
- Proof. rewrite -elem_of_dom. rewrite (δ.(ls_mapping_dom)). done. Qed.
+ Proof. rewrite -elem_of_dom ls_same_doms. SS. Qed.
Lemma fuel_live_role (δ: LiveState M) Ï:
Ï âˆˆ M.(live_roles) δ ->
is_Some (ls_fuel (Λ := Λ) δ !! Ï).
- Proof. rewrite -elem_of_dom. rewrite (δ.(ls_fuel_dom)). done. Qed.
+ Proof. rewrite -elem_of_dom. SS. Qed.
Local Hint Resolve mapping_live_role: core.
Local Hint Resolve fuel_live_role: core.
@@ -760,7 +700,7 @@ Section fairness_preserved.
strict lt_lex m0 (f, m)
→ ∀ (f m: nat) (ζ: locale Λ) (extr : extrace) (auxtr : auxtrace)
(δ : LiveState M) (c : cfg Λ), fairness_induction_stmt Ï m0 f m ζ extr auxtr δ c) ->
- oless (ls_fuel (trfirst auxtr') !! Ï) (ls_fuel δ !! Ï) ->
+ (Ï âˆˆ dom (ls_fuel (trfirst auxtr')) → oless (ls_fuel (trfirst auxtr') !! Ï) (ls_fuel δ !! Ï)) ->
exaux_traces_match extr' auxtr' ->
infinite_trace extr' ->
ls_fuel δ !! Ï = Some f ->
@@ -775,21 +715,25 @@ Section fairness_preserved.
unfold oless in Hdec.
simpl in *.
rewrite -> Hsome in *.
- destruct (ls_fuel (trfirst auxtr') !! Ï) as [f'|] eqn:Heq; last done.
- destruct (decide (Ï âˆˆ live_roles M (trfirst auxtr'))) as [HÏlive'|]; last first.
- { exists 1. left. unfold pred_at. simpl. destruct auxtr'; eauto. }
- have [ζ' Hζ'] : is_Some (ls_mapping (trfirst auxtr') !! Ï) by eauto.
-
- have Hloc'en: pred_at extr' 0 (λ (c : cfg Λ) (_ : option (olocale Λ)),
- locale_enabled ζ' c).
- { rewrite /pred_at /= pred_first_ex. eauto. }
-
- have [p Hp] := (Hfair ζ' 0 Hloc'en).
- have [P Hind] : ∃ M0 : nat, pred_at auxtr' M0 (λ (δ0 : LiveState M) _, ¬ role_enabled Ï Î´0)
- ∨ pred_at auxtr' M0 (λ (_ : LiveState M) â„“, ∃ ζ0, â„“ = Some (Take_step Ï Î¶0)).
- { eapply (IH _ _ _ p _ extr'); eauto.
- Unshelve. unfold strict, lt_lex. lia. }
- exists (1+P). rewrite !pred_at_sum. simpl. done.
+ destruct (ls_fuel (trfirst auxtr') !! Ï) as [f'|] eqn:Heq.
+ - destruct (decide (Ï âˆˆ live_roles M (trfirst auxtr'))) as [HÏlive'|]; last first.
+ { exists 1. left. unfold pred_at. simpl. destruct auxtr'; eauto. }
+ have [ζ' Hζ'] : is_Some (ls_mapping (trfirst auxtr') !! Ï) by eauto.
+
+ have Hloc'en: pred_at extr' 0 (λ (c : cfg Λ) (_ : option (olocale Λ)),
+ locale_enabled ζ' c).
+ { rewrite /pred_at /= pred_first_ex. eauto. }
+
+ have [p Hp] := (Hfair ζ' 0 Hloc'en).
+ have [P Hind] : ∃ M0 : nat, pred_at auxtr' M0 (λ (δ0 : LiveState M) _, ¬ role_enabled Ï Î´0)
+ ∨ pred_at auxtr' M0 (λ (_ : LiveState M) â„“, ∃ ζ0, â„“ = Some (Take_step Ï Î¶0)).
+ { eapply (IH _ _ _ p _ extr'); eauto.
+ Unshelve. unfold strict, lt_lex. specialize (Hdec ltac:(by eapply elem_of_dom_2)). lia. }
+ exists (1+P). rewrite !pred_at_sum. simpl. done.
+ - exists 1. left. rewrite /pred_at /=. rewrite /role_enabled.
+ destruct auxtr' =>/=.
+ + apply not_elem_of_dom in Heq; eapply not_elem_of_weaken; last (by apply ls_fuel_dom); set_solver.
+ + apply not_elem_of_dom in Heq; eapply not_elem_of_weaken; last (by apply ls_fuel_dom); set_solver.
Qed.
Lemma fairness_preserved_ind Ï:
@@ -814,8 +758,9 @@ Section fairness_preserved.
unfold fuel_decr in Hlsdec.
have Hmustdec: must_decrease Ï None δ (trfirst auxtr') (Some ζ).
{ constructor; eauto. }
- specialize (Hlsdec Ï HÏlive Hmustdec).
- eapply case1 =>//; last by eauto using infinite_cons.
+ eapply case1 =>//.
+ * move=> Hinfuel; apply Hlsdec => //; first set_solver.
+ * eapply infinite_cons =>//.
+ (* Three cases:
(1) Ï' = Ï and we are done
(2) Ï' â‰ Ï but they share the same Ï -> Ï decreases
@@ -829,8 +774,8 @@ Section fairness_preserved.
have Hmustdec: must_decrease Ï (Some Ï') δ (trfirst auxtr') (Some ζ).
{ constructor; eauto; congruence. }
(* Copy and paste begins here *)
- specialize (Hdec Ï HÏlive Hmustdec).
eapply case1 =>//; last by eauto using infinite_cons.
+ intros Hinfuels. apply Hdec =>//. SS.
- (* Another thread is taking a step. *)
destruct (decide (Ï âˆˆ live_roles M (trfirst auxtr'))) as [HÏlive'|]; last first.
{ exists 1. left. unfold pred_at. simpl. destruct auxtr'; eauto. }
@@ -841,23 +786,29 @@ Section fairness_preserved.
- inversion Htm as [|s1 â„“1 r1 s2 â„“2 r2 Hl Hs Hts Hls Hmatchrest]; simplify_eq.
simpl in *. destruct â„“; try done. destruct Hls as [_ [_ [Hnoninc _]]].
have HnotNone: Some Ï â‰ None by congruence.
- specialize (Hnoninc Ï HÏlive HnotNone).
+ specialize (Hnoninc Ï ltac:(SS) HnotNone).
unfold oleq in Hnoninc. rewrite Hfuel in Hnoninc.
- destruct (ls_fuel (trfirst auxtr') !! Ï) as [f'|] eqn:Heq; [by eexists|done].
+ destruct (ls_fuel (trfirst auxtr') !! Ï) as [f'|] eqn:Heq; [|set_solver].
+ eexists; split =>//. destruct Hnoninc as [Hnoninc|Hnoninc]=>//.
+ apply elem_of_dom_2 in Heq. set_solver.
- inversion Htm as [|s1 â„“1 r1 s2 â„“2 r2 Hl Hs Hts Hls Hmatchrest]; simplify_eq.
simpl in *. destruct â„“ as [Ï0 ζ0| ζ0|]; try done.
+ destruct Hls as (?&?&?&Hnoninc&?).
unfold fuel_must_not_incr in Hnoninc.
have Hneq: Some Ï â‰ Some Ï0 by congruence.
- specialize (Hnoninc Ï HÏlive Hneq).
+ specialize (Hnoninc Ï ltac:(SS) Hneq).
unfold oleq in Hnoninc. rewrite Hfuel in Hnoninc.
- destruct (ls_fuel (trfirst auxtr') !! Ï) as [f'|] eqn:Heq; [by eexists|done].
+ destruct (ls_fuel (trfirst auxtr') !! Ï) as [f'|] eqn:Heq; [|set_solver].
+ eexists; split =>//. destruct Hnoninc as [Hnoninc|Hnoninc]=>//.
+ apply elem_of_dom_2 in Heq. set_solver.
+ destruct Hls as (?&?&Hnoninc&?).
unfold fuel_must_not_incr in Hnoninc.
have Hneq: Some Ï â‰ None by congruence.
- specialize (Hnoninc Ï HÏlive Hneq).
+ specialize (Hnoninc Ï ltac:(SS) Hneq).
unfold oleq in Hnoninc. rewrite Hfuel in Hnoninc.
- destruct (ls_fuel (trfirst auxtr') !! Ï) as [f'|] eqn:Heq; [by eexists|done]. }
+ destruct (ls_fuel (trfirst auxtr') !! Ï) as [f'|] eqn:Heq; [|set_solver].
+ eexists; split =>//. destruct Hnoninc as [Hnoninc|Hnoninc]=>//.
+ apply elem_of_dom_2 in Heq. set_solver. }
unfold fair_ex in *.
have Hζ'en: pred_at extr' 0 (λ (c : cfg Λ) _, locale_enabled ζ c).
@@ -879,23 +830,23 @@ Section fairness_preserved.
unfold fuel_decr in Hdec.
have Hmd: must_decrease Ï None δ (trfirst auxtr') None.
{ econstructor. congruence. rewrite Hζ''. eauto. }
- specialize (Hdec Ï HÏlive Hmd).
+ specialize (Hdec Ï ltac:(SS) ltac:(SS) Hmd).
unfold oleq in Hdec. rewrite Hfuel in Hdec.
destruct (ls_fuel (trfirst auxtr') !! Ï) as [f'|] eqn:Heq; [by eexists|done].
- inversion Htm as [|s1 â„“1 r1 s2 â„“2 r2 Hl Hs Hts Hls Hmatchrest]; simplify_eq.
- simpl in *. destruct â„“ as [Ï0 ζ0| ζ0|]; try done.
+ simpl in *. destruct â„“ as [Ï0 ζ0| ζ0|]; try done.
+ destruct Hls as (?&?&Hdec&?&?).
unfold fuel_decr in Hdec. simplify_eq.
have Hmd: must_decrease Ï (Some Ï0) δ (trfirst auxtr') (Some ζ0).
{ econstructor 2. congruence. rewrite Hζ''; eauto. }
- specialize (Hdec Ï HÏlive Hmd).
+ specialize (Hdec Ï ltac:(SS) ltac:(SS) Hmd).
unfold oleq in Hdec. rewrite Hfuel in Hdec.
destruct (ls_fuel (trfirst auxtr') !! Ï) as [f'|] eqn:Heq; [by eexists|done].
+ destruct Hls as (?&Hdec&_).
unfold fuel_decr in Hdec. simplify_eq.
have Hmd: must_decrease Ï None δ (trfirst auxtr') (Some ζ0).
{ econstructor 2. congruence. rewrite Hζ''; eauto. }
- specialize (Hdec Ï HÏlive Hmd).
+ specialize (Hdec Ï ltac:(SS) ltac:(SS) Hmd).
unfold oleq in Hdec. rewrite Hfuel in Hdec.
destruct (ls_fuel (trfirst auxtr') !! Ï) as [f'|] eqn:Heq; [by eexists|done]. }
@@ -1064,7 +1015,7 @@ Section fuel_dec_unless.
end.
Definition Ψ (δ: LiveState Mdl) :=
- [^ Nat.add map] Ï â†¦ f ∈ δ.(ls_fuel (Λ := Λ)), f.
+ size δ.(ls_fuel) + [^ Nat.add map] Ï â†¦ f ∈ δ.(ls_fuel (Λ := Λ)), f.
Lemma fuel_dec_unless (extr: extrace) (auxtr: auxtrace) :
(∀ c c', locale_step (Λ := Λ) c None c' -> False) ->
@@ -1083,22 +1034,38 @@ Section fuel_dec_unless.
inversion Hval as [|c tid extr' ?? ? Hlm Hsteps Hstep Htrans Hmatch]; simplify_eq =>//.
destruct â„“ as [| tid' |];
[left; eexists; done| right |destruct tid; by [| exfalso; eapply Hcl]].
- destruct Htrans as (Hne&Hdec&Hni&Heq). rewrite -> Heq in *. split; last done.
+ destruct Htrans as (Hne&Hdec&Hni&Hincl&Heq). rewrite -> Heq in *. split; last done.
destruct tid as [tid|]; last done.
- rewrite <- Hlm in *. destruct Hne as [Ï HÏtid].
- have Hless: oless (ls_fuel (trfirst auxtr') !! Ï) (ls_fuel δ !! Ï).
- { apply Hdec; last by econstructor.
- rewrite -ls_mapping_dom. by eapply elem_of_dom_2. }
- unfold oless in Hless.
- destruct (ls_fuel (trfirst auxtr')!!Ï) as [f2|] eqn:Hf2;
- destruct (ls_fuel δ!!Ï) as [f1|] eqn:Hf1 =>//.
- rewrite /Ψ (big_opM_delete (λ _ f, f) (ls_fuel (trfirst _)) Ï) //.
- rewrite (big_opM_delete (λ _ f, f) (ls_fuel δ) Ï) //.
- apply Nat.add_lt_le_mono =>//. apply big_addM_leq_forall => Ï' HÏ'.
- rewrite dom_delete_L in HÏ'.
- have HÏneqÏ' : Ï â‰ Ï' by set_solver.
- rewrite !lookup_delete_ne //. apply Hni => //.
- rewrite Heq. rewrite -ls_fuel_dom. set_solver.
+ rewrite <- Hlm in *.
+
+ destruct (decide (dom $ ls_fuel δ = dom $ ls_fuel (trfirst auxtr'))) as [Hdomeq|Hdomneq].
+ - destruct Hne as [Ï HÏtid].
+
+ assert (Ï âˆˆ dom $ ls_fuel δ) as Hin by rewrite -ls_same_doms elem_of_dom //.
+ pose proof Hin as Hin'. pose proof Hin as Hin''.
+ apply elem_of_dom in Hin as [f Hf].
+ rewrite Hdomeq in Hin'. apply elem_of_dom in Hin' as [f' Hf'].
+ rewrite /Ψ -!size_dom Hdomeq.
+ apply Nat.add_lt_mono_l.
+
+ rewrite /Ψ (big_opM_delete (λ _ f, f) (ls_fuel (trfirst _)) Ï) //.
+ rewrite (big_opM_delete (λ _ f, f) (ls_fuel δ) Ï) //.
+ apply Nat.add_lt_le_mono.
+ { rewrite /fuel_decr in Hdec. specialize (Hdec Ï). rewrite Hf Hf' /= in Hdec.
+ apply Hdec; [set_solver | set_solver | by econstructor]. }
+
+ apply big_addM_leq_forall => Ï' HÏ'.
+ rewrite dom_delete_L in HÏ'.
+ have HÏneqÏ' : Ï â‰ Ï' by set_solver.
+ rewrite !lookup_delete_ne //.
+ destruct (decide (Ï' ∈ dom δ.(ls_fuel))) as [Hin|Hnotin]; last set_solver.
+ rewrite /fuel_must_not_incr in Hni.
+ destruct (Hni Ï' ltac:(done) ltac:(done)); [done|set_solver].
+ - assert (size $ ls_fuel (trfirst auxtr') < size $ ls_fuel δ).
+ { rewrite -!size_dom. apply subset_size. set_solver. }
+ apply Nat.add_lt_le_mono =>//.
+ apply big_addM_leq_forall => Ï' HÏ'.
+ destruct (Hni Ï' ltac:(set_solver) ltac:(done)); [done|set_solver].
Qed.
End fuel_dec_unless.
diff --git a/fairness/fairness_finiteness.v b/fairness/fairness_finiteness.v
index e3a8656..3c07fa8 100644
--- a/fairness/fairness_finiteness.v
+++ b/fairness/fairness_finiteness.v
@@ -1,4 +1,4 @@
-From trillium.fairness Require Import fairness resources.
+From trillium.fairness Require Import fairness.
From trillium.prelude Require Import finitary quantifiers classical_instances.
From stdpp Require Import finite.
@@ -42,8 +42,9 @@ Section finitary.
Program Definition enumerate_next (δ1: (fair_model (Λ := Λ) M)) (oζ : olocale Λ) (c': cfg Λ):
list (fair_model M * @mlabel (fair_model (Λ := Λ) M)) :=
'(s2, ℓ) ↠(δ1.(ls_under), None) :: enum_inner δ1.(ls_under);
- fs ↠enum_gmap_bounded' (live_roles _ s2) (max_gmap δ1.(ls_fuel) `max` fuel_limit s2);
- ms ↠enum_gmap_range_bounded' (live_roles _ s2) (locales_of_list c'.1);
+ d ↠enumerate_dom_gsets' (dom δ1.(ls_fuel) ∪ live_roles _ s2);
+ fs ↠enum_gmap_bounded' (live_roles _ s2 ∪ d) (max_gmap δ1.(ls_fuel) `max` fuel_limit s2);
+ ms ↠enum_gmap_range_bounded' (live_roles _ s2 ∪ d) (locales_of_list c'.1);
let â„“' := match â„“ with
| None => match oζ with
Some ζ => Silent_step ζ
@@ -58,10 +59,13 @@ Section finitary.
ls_fuel := `fs;
(* ls_fuel_dom := proj2_sig fs; *) (* TODO: why this does not work?*)
ls_mapping := `ms ;
- ls_mapping_dom := proj2_sig ms
|}, â„“').
Next Obligation.
- intros ??????????. destruct fs as [??]. by simpl.
+ intros ??????????. destruct fs as [? Heq]. rewrite /= Heq //. set_solver.
+ Qed.
+ Next Obligation.
+ intros ??????????. destruct fs as [? Heq]. destruct ms as [? Heq'].
+ rewrite /= Heq //.
Qed.
Lemma valid_state_evolution_finitary_fairness (φ: execution_trace Λ -> auxiliary_trace (fair_model M) -> Prop) :
@@ -76,43 +80,60 @@ Section finitary.
split; last first.
{ destruct â„“ as [Ï tid' | |].
- inversion Htrans as [Htrans']. apply elem_of_cons; right. by apply enum_inner_spec.
- - apply elem_of_cons; left. f_equal. inversion Htrans as (?&?&?&?); done.
+ - apply elem_of_cons; left. f_equal. inversion Htrans as (?&?&?&?&?); done.
- apply elem_of_cons; right. inversion Htrans as (?&?). by apply enum_inner_spec. }
- apply elem_of_list_bind. eexists (δ2.(ls_fuel) ↾ (ls_fuel_dom _)); split; last first.
- { eapply enum_gmap_bounded'_spec; split; first by apply ls_fuel_dom.
+ apply elem_of_list_bind. eexists (dom $ δ2.(ls_fuel)). split; last first.
+ { apply enumerate_dom_gsets'_spec. destruct â„“ as [Ï tid' | |].
+ - inversion Htrans as (?&?&?&?&?&?&?). intros Ï' Hin. destruct (decide (Ï' ∈ live_roles _ δ2)); first set_solver.
+ destruct (decide (Ï' ∈ dom $ ls_fuel (trace_last auxtr))); first set_solver. set_solver.
+ - inversion Htrans as (?&?&?&?&?). set_solver.
+ - inversion Htrans as (?&?&?&?&?). done. }
+ apply elem_of_list_bind.
+ assert (Hfueldom: dom δ2.(ls_fuel) = live_roles M δ2 ∪ dom (ls_fuel δ2)).
+ { rewrite subseteq_union_1_L //. apply ls_fuel_dom. }
+
+ eexists (δ2.(ls_fuel) ↾ Hfueldom); split; last first.
+ { eapply enum_gmap_bounded'_spec; split =>//.
intros Ï f Hsome. destruct â„“ as [Ï' tid' | |].
- destruct (decide (Ï = Ï')) as [-> | Hneq].
- + inversion Htrans as [? Hbig]. destruct Hbig as (?&?&?&Hlim&?).
- rewrite Hsome /= in Hlim.
- assert (Hlive: Ï' ∈ live_roles _ δ2).
- { rewrite -ls_fuel_dom elem_of_dom. eauto. }
- specialize (Hlim Hlive). lia.
- + inversion Htrans as [? Hbig]. destruct Hbig as (?&?&Hleq&?&Hnew).
- destruct (decide (Ï âˆˆ live_roles _ (trace_last auxtr))) as [Hin|Hnotin].
+ + inversion Htrans as [? Hbig]. destruct Hbig as (Hmap&Hleq&?&Hlim&?&?).
+ destruct (decide (Ï' ∈ live_roles _ δ2)).
+ * rewrite Hsome /= in Hlim.
+ assert (Hlive: Ï' ∈ live_roles _ δ2) by set_solver.
+ specialize (Hlim Hlive). lia.
+ * unfold fuel_decr in Hleq.
+ apply elem_of_dom_2 in Hmap. rewrite ls_same_doms in Hmap.
+ pose proof Hsome as Hsome'. apply elem_of_dom_2 in Hsome'.
+ specialize (Hleq Ï' ltac:(done) ltac:(done)).
+ assert(must_decrease Ï' (Some Ï') (trace_last auxtr) δ2 (Some tid')) as Hmd; first by constructor 3.
+ specialize (Hleq Hmd). rewrite Hsome /= in Hleq.
+ apply elem_of_dom in Hmap as [? Heq]. rewrite Heq in Hleq.
+ pose proof (max_gmap_spec _ _ _ Heq). simpl in *. lia.
+ + inversion Htrans as [? Hbig]. destruct Hbig as (Hmap&?&Hleq'&?&Hnew&?).
+ destruct (decide (Ï âˆˆ dom $ ls_fuel (trace_last auxtr))) as [Hin|Hnotin].
* assert (Hok: oleq (ls_fuel δ2 !! Ï) (ls_fuel (trace_last auxtr) !! Ï)).
- { apply Hleq =>//. congruence. }
+ { unfold fuel_must_not_incr in *.
+ assert (Ï âˆˆ dom $ ls_fuel (trace_last auxtr)) by SS.
+ specialize (Hleq' Ï ltac:(done) ltac:(congruence)) as [Hleq'|Hleq'] =>//. apply elem_of_dom_2 in Hsome. set_solver. }
rewrite Hsome in Hok. destruct (ls_fuel (trace_last auxtr) !! Ï) as [f'|] eqn:Heqn; last done.
- rewrite <-ls_fuel_dom, elem_of_dom in Hin.
pose proof (max_gmap_spec _ _ _ Heqn). simpl in *. lia.
* assert (Hok: oleq (ls_fuel δ2 !! Ï) (Some (fuel_limit δ2))).
- { apply Hnew. apply elem_of_dom_2 in Hsome. rewrite -ls_fuel_dom. set_solver. }
- rewrite Hsome in Hok. simpl in *. lia.
- - inversion Htrans as [? [? [Hleq Heq]]]. specialize (Hleq Ï).
- assert (Hok: oleq (ls_fuel δ2 !! Ï) (ls_fuel (trace_last auxtr) !! Ï)).
- { apply Hleq; last done. rewrite Heq -ls_fuel_dom elem_of_dom Hsome. by eauto. }
- rewrite Hsome in Hok. destruct (ls_fuel (trace_last auxtr) !! Ï) as [f'|] eqn:Heqn; last done.
- pose proof (max_gmap_spec _ _ _ Heqn). simpl in *. lia.
- - inversion Htrans as [? [? [Hleq Hnew]]]. specialize (Hleq Ï).
- destruct (decide (Ï âˆˆ live_roles _ (trace_last auxtr))).
- + assert (Hok: oleq (ls_fuel δ2 !! Ï) (ls_fuel (trace_last auxtr) !! Ï)).
- { apply Hleq; done. }
- rewrite Hsome in Hok. destruct (ls_fuel (trace_last auxtr) !! Ï) as [f'|] eqn:Heqn; last done.
+ { apply Hnew. apply elem_of_dom_2 in Hsome. set_solver. }
+ rewrite Hsome in Hok. simpl in Hok. lia.
+ - inversion Htrans as [? [? [Hleq [Hincl Heq]]]]. specialize (Hleq Ï).
+ assert (Ï âˆˆ dom $ ls_fuel (trace_last auxtr)) as Hin.
+ { apply elem_of_dom_2 in Hsome. set_solver. }
+ specialize (Hleq Hin ltac:(done)) as [Hleq|Hleq].
+ + rewrite Hsome in Hleq. destruct (ls_fuel (trace_last auxtr) !! Ï) as [f'|] eqn:Heqn; last done.
pose proof (max_gmap_spec _ _ _ Heqn). simpl in *. lia.
- + assert (Hok: oleq (ls_fuel δ2 !! Ï) (Some (fuel_limit δ2))).
- { apply Hnew. apply elem_of_dom_2 in Hsome. rewrite -ls_fuel_dom. set_solver. }
- rewrite Hsome in Hok. simpl in *. lia. }
- apply elem_of_list_bind. exists (δ2.(ls_mapping) ↾ (ls_mapping_dom _)); split; last first.
- { eapply enum_gmap_range_bounded'_spec; split; first by apply ls_mapping_dom.
+ + apply elem_of_dom_2 in Hsome. set_solver.
+ - inversion Htrans as [? [? [Hleq [Hnew Hfalse]]]]. done. }
+ apply elem_of_list_bind.
+ assert (Hmappingdom: dom δ2.(ls_mapping) = live_roles M δ2 ∪ dom (ls_fuel δ2)).
+ { rewrite -Hfueldom ls_same_doms //. }
+
+ exists (δ2.(ls_mapping) ↾ Hmappingdom); split; last first.
+ { eapply enum_gmap_range_bounded'_spec; split=>//.
intros Ï' tid' Hsome. unfold tids_smaller in *.
apply locales_of_list_from_locale_from. eauto. }
rewrite elem_of_list_singleton; f_equal.
@@ -121,5 +142,7 @@ Section finitary.
Unshelve.
+ intros ??. apply make_decision.
+ intros. apply make_proof_irrel.
+ + done.
+ + done.
Qed.
End finitary.
diff --git a/fairness/heap_lang/lifting.v b/fairness/heap_lang/lifting.v
index b87d31a..0121b4a 100644
--- a/fairness/heap_lang/lifting.v
+++ b/fairness/heap_lang/lifting.v
@@ -120,7 +120,7 @@ Definition sim_rel (M : FairModel) (ex : execution_trace heap_lang)
valid_state_evolution_fairness ex aux ∧ live_rel M ex aux.
-Theorem simulation_adequacy Σ {Mdl: FairModel} `{!heapGpreS Σ Mdl} (s: stuckness) (e1 : expr) σ1 (s1: Mdl):
+Theorem simulation_adequacy Σ {Mdl: FairModel} `{!heapGpreS Σ Mdl} (s: stuckness) (e1 : expr) σ1 (s1: Mdl) (FR: gset _):
(* The model has finite branching *)
rel_finitary (sim_rel Mdl) →
live_roles Mdl s1 ≠∅ ->
@@ -130,7 +130,8 @@ Theorem simulation_adequacy Σ {Mdl: FairModel} `{!heapGpreS Σ Mdl} (s: stuckne
(∀ `{!heapGS Σ Mdl},
⊢ |={⊤}=>
frag_model_is s1 -∗
- has_fuels (Σ := Σ) 0%nat (gset_to_gmap (fuel_limit s1) (Mdl.(live_roles) s1))
+ frag_free_roles_are (FR ∖ 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 *)
@@ -148,17 +149,19 @@ Proof.
iMod (model_state_init s1) as (γmod) "[Hmoda Hmodf]".
iMod (model_mapping_init s1) as (γmap) "[Hmapa Hmapf]".
iMod (model_fuel_init s1) as (γfuel) "[Hfuela Hfuelf]".
+ iMod (model_free_roles_init s1 (FR ∖ live_roles _ s1)) as (γfr) "[HFR Hfr]".
set (distG :=
{|
heap_fairnessGS := {|
fairness_model_name := γmod;
fairness_model_mapping_name := γmap;
fairness_model_fuel_name := γfuel;
+ fairness_model_free_roles_name := γfr;
|}
|}).
iMod (H distG) as "Hwp". clear H.
- iSpecialize ("Hwp" with "Hmodf [Hmapf Hfuelf]").
+ iSpecialize ("Hwp" with "Hmodf Hfr [Hmapf Hfuelf]").
{ rewrite /has_fuels /frag_mapping_is /= map_fmap_singleton. iFrame.
iAssert ([∗ set] Ï âˆˆ live_roles Mdl s1, Ï â†¦F (fuel_limit s1))%I with "[Hfuelf]" as "H".
- unfold frag_fuel_is. setoid_rewrite map_fmap_singleton.
@@ -172,16 +175,17 @@ Proof.
iSplitR.
{ unfold config_wp. iIntros "!>" (???????) "?". done. }
iFrame.
- iSplitL "Hmapa Hfuela".
- { iExists {[ 0%nat := (live_roles Mdl s1) ]}. iSplitL "Hfuela".
+ iSplitL "Hmapa Hfuela HFR".
+ { iExists {[ 0%nat := (live_roles Mdl s1) ]}, _.
+ iSplitL "Hfuela"; [|iSplitL "Hmapa"; repeat iSplit; try iPureIntro].
- rewrite /auth_fuel_is /= fmap_gset_to_gmap //.
- rewrite /auth_mapping_is /ls_mapping /= map_fmap_singleton. iFrame; iPureIntro.
- split.
- + intros Ï tid. rewrite lookup_gset_to_gmap_Some.
- setoid_rewrite lookup_singleton_Some.
- split; naive_solver.
- + intros tid Hlocs. rewrite lookup_singleton_ne //.
- unfold locales_of_list in Hlocs. simpl in Hlocs. set_solver. }
+ - rewrite /auth_free_roles_are. iFrame.
+ - intros Ï tid. rewrite lookup_gset_to_gmap_Some.
+ setoid_rewrite lookup_singleton_Some. split; naive_solver.
+ - intros tid Hlocs. rewrite lookup_singleton_ne //.
+ unfold locales_of_list in Hlocs. simpl in Hlocs. set_solver.
+ - rewrite dom_gset_to_gmap. set_solver. }
iIntros (ex atr c3 Hval Hexst Hauxst Hexend Hbig).
iIntros (Hns) "[%Hvalid Hsi] Hposts".
@@ -209,7 +213,7 @@ Proof.
iAssert (0%nat ↦M ∅) with "[Hposts]" as "Hem".
{ rewrite /= Heq /fmap /=. by iDestruct "Hposts" as "[??]". }
iDestruct "Hsi" as "(_&Hsi)".
- iDestruct "Hsi" as "(%M&Hfuela&Hmapa&%Hinvmap&%Hsmall&Hmodel)".
+ iDestruct "Hsi" as "(%M&%FR'&Hfuela&Hmapa&HFR&%Hinvmap&%Hsmall&Hmodel&HfrFR)".
iDestruct (frag_mapping_same 0%nat M with "[Hmapa] Hem") as "%H"; first done.
iPureIntro. by eapply no_locale_empty.
+ iSplit; iPureIntro.
@@ -238,12 +242,12 @@ Proof.
{ destruct (to_val e') as [?|] eqn:Heq; last done.
iApply posts_of_empty_mapping => //.
apply from_locale_lookup =>//. }
- iDestruct "Hsi" as "(_&Hsi)". iDestruct "Hsi" as "(%M&Hfuela&Hmapa&%Hinvmap&%Hsmall&Hmodel)".
+ iDestruct "Hsi" as "(_&Hsi)". iDestruct "Hsi" as "(%M&%&Hfuela&Hmapa&?&%Hinvmap&%Hsmall&Hmodel&?)".
iDestruct (frag_mapping_same tid' M with "Hmapa H") as "%Hlk".
{ rewrite /auth_mapping_is. iPureIntro. by eapply no_locale_empty. }
Qed.
-Theorem simulation_adequacy_inftraces Σ (Mdl : FairModel) `{!heapGpreS Σ Mdl} (s: stuckness)
+Theorem simulation_adequacy_inftraces Σ (Mdl : FairModel) `{!heapGpreS Σ Mdl} (s: stuckness) FR
e1 σ1 (s1: Mdl)
(iex : inf_execution_trace heap_lang)
(Hvex : valid_inf_exec (trace_singleton ([e1], σ1)) iex)
@@ -253,7 +257,8 @@ Theorem simulation_adequacy_inftraces Σ (Mdl : FairModel) `{!heapGpreS Σ Mdl}
live_roles Mdl s1 ≠∅ ->
(∀ `{!heapGS Σ Mdl},
⊢ |={⊤}=>
- frag_model_is s1 -∗
+ frag_model_is s1 -∗
+ frag_free_roles_are (FR ∖ 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 ∅ }}
) ->
@@ -274,7 +279,7 @@ Proof.
eapply produced_inf_aux_trace_valid_inf.
Unshelve.
- econstructor.
- - apply (simulation_adequacy Σ s) => //.
+ - apply (simulation_adequacy Σ s _ _ _ FR) => //.
- done.
Qed.
@@ -290,7 +295,7 @@ Notation exaux_traces_match Mdl :=
ls_trans
).
-Theorem simulation_adequacy_traces Σ (Mdl : FairModel) `{!heapGpreS Σ Mdl} (s: stuckness)
+Theorem simulation_adequacy_traces Σ (Mdl : FairModel) `{!heapGpreS Σ Mdl} (s: stuckness) FR
e1 (s1: Mdl)
(extr : extrace)
(Hvex : extrace_valid extr)
@@ -302,6 +307,7 @@ Theorem simulation_adequacy_traces Σ (Mdl : FairModel) `{!heapGpreS Σ Mdl} (s:
(∀ `{!heapGS Σ Mdl},
⊢ |={⊤}=>
frag_model_is s1 -∗
+ frag_free_roles_are (FR ∖ 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 ∅ }}
) ->
@@ -320,7 +326,7 @@ Proof.
(trace_singleton (initial_ls s1 0%nat))
(from_trace extr)
iatr.
- { apply (simulation_adequacy_inftraces Σ Mdl s); eauto.
+ { apply (simulation_adequacy_inftraces Σ Mdl s FR); eauto.
eapply from_trace_preserves_validity; eauto; first econstructor.
simpl. destruct (trfirst extr) eqn:Heq.
simpl in Hexfirst. rewrite -Hexfirst Heq //. }
@@ -333,7 +339,7 @@ Proof.
- apply to_trace_spec.
Qed.
-Theorem simulation_adequacy_model_trace Σ (Mdl : FairModel) `{!heapGpreS Σ Mdl} (s: stuckness)
+Theorem simulation_adequacy_model_trace Σ (Mdl : FairModel) `{!heapGpreS Σ Mdl} (s: stuckness) FR
e1 (s1: Mdl)
(extr : extrace)
(Hvex : extrace_valid extr)
@@ -345,6 +351,7 @@ Theorem simulation_adequacy_model_trace Σ (Mdl : FairModel) `{!heapGpreS Σ Mdl
(∀ `{!heapGS Σ Mdl},
⊢ |={⊤}=>
frag_model_is s1 -∗
+ frag_free_roles_are (FR ∖ 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 ∅ }}
) ->
@@ -354,14 +361,14 @@ Theorem simulation_adequacy_model_trace Σ (Mdl : FairModel) `{!heapGpreS Σ Mdl
Proof.
intros Hfb Hlr Hwp.
destruct (simulation_adequacy_traces
- Σ Mdl _ e1 s1 extr Hvex Hexfirst Hfb Hlr Hwp) as [auxtr Hmatch].
+ Σ Mdl _ FR e1 s1 extr Hvex Hexfirst Hfb Hlr Hwp) as [auxtr Hmatch].
destruct (can_destutter_auxtr extr auxtr) as [mtr Hupto] =>//.
{ intros ?? contra. inversion contra. done. }
eauto.
Qed.
Theorem simulation_adequacy_terminate Σ Mdl `{!heapGpreS Σ Mdl} (s: stuckness)
- e1 (s1: Mdl)
+ e1 (s1: Mdl) FR
(extr : extrace)
(Hvex : extrace_valid extr)
(Hexfirst : (trfirst extr).1 = [e1])
@@ -373,6 +380,7 @@ Theorem simulation_adequacy_terminate Σ Mdl `{!heapGpreS Σ Mdl} (s: stuckness)
(∀ `{!heapGS Σ Mdl},
⊢ |={⊤}=>
frag_model_is s1 -∗
+ frag_free_roles_are (FR ∖ 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 ∅ }}
) ->
@@ -381,7 +389,7 @@ Theorem simulation_adequacy_terminate Σ Mdl `{!heapGpreS Σ Mdl} (s: stuckness)
Proof.
intros Hterm Hfb Hlr Hwp Hfair.
destruct (simulation_adequacy_model_trace
- Σ Mdl _ e1 s1 extr Hvex Hexfirst Hfb Hlr Hwp) as (auxtr&mtr&Hmatch&Hupto).
+ Σ Mdl _ FR e1 s1 extr Hvex Hexfirst Hfb Hlr Hwp) as (auxtr&mtr&Hmatch&Hupto).
destruct (infinite_or_finite extr) as [Hinf|] =>//.
have Hfairaux := fairness_preserved extr auxtr Hinf Hmatch Hfair.
have Hvalaux := exaux_preserves_validity extr auxtr Hmatch.
@@ -393,7 +401,7 @@ Proof.
Qed.
Theorem simulation_adequacy_terminate_ftm Σ `{FairTerminatingModel Mdl} `{!heapGpreS Σ Mdl} (s: stuckness)
- e1 (s1: Mdl)
+ e1 (s1: Mdl) FR
(extr : extrace)
(Hvex : extrace_valid extr)
(Hexfirst : (trfirst extr).1 = [e1])
@@ -404,7 +412,8 @@ Theorem simulation_adequacy_terminate_ftm Σ `{FairTerminatingModel Mdl} `{!heap
(∀ `{!heapGS Σ Mdl},
⊢ |={⊤}=>
frag_model_is s1 -∗
- has_fuels (Σ := Σ) 0%nat (gset_to_gmap (fuel_limit s1) (Mdl.(live_roles) s1))
+ frag_free_roles_are (FR ∖ 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 *)
@@ -625,9 +634,10 @@ Proof.
simplify_eq. iMod "Hclose" as "_". iMod "H" as "[Hfuels Hkont]".
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. }
+ (* iDestruct "Hmi" as (??) "(?&?&?&?&?&?&%)". *)
+
+ iMod (update_no_step_enough_fuel _ _ ∅ with "Hfuels Hmi") as "H"; eauto;
+ [by intros X%dom_empty_inv_L | set_solver | set_solver | econstructor =>//; by apply fill_step |].
iModIntro.
iDestruct ("H") as (δ2 ℓ [Hlabels Hvse]) "[Hfuels Hmi]".
iExists δ2, ℓ.
@@ -637,7 +647,47 @@ Proof.
- iPureIntro. destruct â„“ =>//.
- iPureIntro. destruct Hvse as (?&?&? )=>//.
- iPureIntro. destruct Hvse as (?&?&? )=>//.
- - by iApply "Hkont".
+ - iApply "Hkont". iApply (has_fuels_proper with "Hfuels") =>//.
+ rewrite map_filter_id //. intros ?? ?%elem_of_dom_2; set_solver.
+Qed.
+
+Lemma wp_lift_pure_step_no_fork_remove_role rem s tid E E' Φ e1 e2 fs ϕ:
+ fs ≠∅ ->
+ rem ⊆ dom fs →
+ rem ∩ live_roles _ s = ∅ →
+ PureExec Ï• 1 e1 e2 ->
+ Ï• ->
+ (|={E}[E']▷=> frag_model_is s ∗ has_fuels_S tid fs ∗
+ (frag_model_is s -∗ (has_fuels tid (fs ⇂ (dom fs ∖ rem))) -∗ WP e2 @ tid; E {{ Φ }}))
+ ⊢ WP e1 @ tid; E {{ Φ }}.
+Proof.
+ intros NnO Hincl Hdisj Hpe HÏ•.
+ have Hps: pure_step e1 e2.
+ { specialize (Hpe HÏ•). by apply nsteps_once_inv in Hpe. }
+ iIntros "H". iApply wp_lift_step; eauto.
+ { destruct Hps as [Hred _]. specialize (Hred inhabitant). eapply reducible_not_val; eauto. }
+ iIntros (extr auxtr K tp1 tp2 σ1 Hvalex Hexend Hloc) "Hsi".
+ iMod "H". iMod fupd_mask_subseteq as "Hclose"; last iModIntro; first by set_solver.
+ iSplit; first by destruct Hps as [Hred _].
+ iNext. iIntros (e2' σ2 efs Hpstep).
+ destruct Hps as [? Hdet]. specialize (Hdet _ _ _ _ Hpstep) as (?&?&?).
+ simplify_eq. iMod "Hclose" as "_". iMod "H" as "(Hmod & Hfuels & Hkont)".
+ rewrite !app_nil_r.
+ iDestruct "Hsi" as "(%&Hgh&Hmi)".
+ iDestruct (model_agree' with "Hmi Hmod") as %Heq.
+
+ iMod (update_no_step_enough_fuel _ _ rem with "Hfuels Hmi") as "H"; eauto;
+ [by intros X%dom_empty_inv_L | set_solver | econstructor =>//; by apply fill_step |].
+ iModIntro.
+ iDestruct ("H") as (δ2 ℓ [Hlabels Hvse]) "[Hfuels Hmi]".
+ iExists δ2, ℓ.
+ rewrite /state_interp /=.
+ rewrite Hexend /=. list_simplifier. iFrame "Hgh Hmi".
+ repeat iSplit; last done.
+ - iPureIntro. destruct â„“ =>//.
+ - iPureIntro. destruct Hvse as (?&?&? )=>//.
+ - iPureIntro. destruct Hvse as (?&?&? )=>//.
+ - iApply ("Hkont" with "Hmod"). iApply (has_fuels_proper with "Hfuels") =>//.
Qed.
(* Lemma wp_lift_pure_step_no_fork_2 tid E E' Φ e1 e2 (fs: gmap (fmrole Mdl) nat) R ϕ: *)
@@ -668,15 +718,17 @@ Proof.
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 Ï Ï†:
+Lemma wp_lift_pure_step_no_fork_take_step s1 s2 tid E E' fs1 fs2 fr1 Φ e1 e2 Ï Ï†:
PureExec φ 1 e1 e2 -> φ ->
valid_new_fuelmap fs1 fs2 s1 s2 Ï ->
+ live_roles Mdl s2 ∖ live_roles Mdl s1 ⊆ fr1 →
Mdl.(fmtrans) s1 (Some Ï) s2 ->
- (|={E}[E']▷=> frag_model_is s1 ∗ has_fuels tid fs1 ∗
- (frag_model_is s2 -∗ (has_fuels tid fs2 -∗ WP e2 @ tid; E {{ Φ }})))
+ (|={E}[E']▷=> frag_model_is s1 ∗ has_fuels tid fs1 ∗ frag_free_roles_are fr1 ∗
+ (frag_model_is s2 -∗ frag_free_roles_are (fr1 ∖ (live_roles Mdl s2 ∖ live_roles Mdl s1))
+ -∗ (has_fuels tid fs2 -∗ WP e2 @ tid; E {{ Φ }})))
⊢ WP e1 @ tid; E {{ Φ }}.
Proof.
- iIntros (Hpe Hφ Hval Htrans).
+ iIntros (Hpe Hφ Hval Hfr Htrans).
have Hps: pure_step e1 e2.
{ specialize (Hpe Hφ). by apply nsteps_once_inv in Hpe. }
iIntros "Hkont".
@@ -688,52 +740,56 @@ Proof.
iSplit; first by destruct Hps as [Hred _].
iNext. iIntros (e2' σ2 efs Hpstep).
destruct Hps as [? Hdet]. specialize (Hdet _ _ _ _ Hpstep) as (?&?&?).
- simplify_eq. iMod "Hclose" as "_". iMod "Hkont" as "(Hmod&Hfuels&Hkont)".
+ simplify_eq. iMod "Hclose" as "_". iMod "Hkont" as "(Hmod&Hfuels&Hfr&Hkont)".
rewrite !app_nil_r.
iDestruct "Hsi" as "(%&Hgh&Hmi)". simpl.
iDestruct (model_agree' with "Hmi Hmod") as %Hmeq.
- iMod (update_step_still_alive _ _ _ _ σ1 σ1 with "Hfuels Hmod Hmi") as "H"; eauto.
+ iMod (update_step_still_alive _ _ _ _ σ1 σ1 with "Hfuels Hmod Hmi Hfr") as "H"; eauto.
{ rewrite Hexend. eauto. }
{ econstructor =>//.
- rewrite Hexend //=.
- by apply fill_step. }
{ rewrite Hmeq. apply Hval. }
- iModIntro. iDestruct "H" as (δ2 ℓ [Hlabels Hvse]) "(Hfuels&Hmod&Hmi)".
+ iModIntro. iDestruct "H" as (δ2 ℓ [Hlabels Hvse]) "(Hfuels&Hmod&Hmi&Hfr)".
iExists δ2, ℓ.
rewrite Hexend /=. list_simplifier. iFrame "Hgh Hmi".
repeat iSplit; last done.
- iPureIntro. destruct â„“ =>//.
- iPureIntro. destruct Hvse as (?&?&? )=>//.
- iPureIntro. destruct Hvse as (?&?&? )=>//.
- - by iSpecialize ("Hkont" with "Hmod Hfuels").
+ - by iSpecialize ("Hkont" with "Hmod Hfr Hfuels").
Qed.
-Lemma wp_lift_pure_step_no_fork_singlerole_take_step s1 s2 tid E E' (f1 f2: nat) Φ e1 e2 Ï Ï†:
+Lemma wp_lift_pure_step_no_fork_singlerole_take_step s1 s2 tid E E' (f1 f2: nat) fr Φ e1 e2 Ï Ï†:
PureExec φ 1 e1 e2 -> φ ->
live_roles _ s2 ⊆ live_roles _ s1 ->
(f2 ≤ fuel_limit s2)%nat -> Mdl.(fmtrans) s1 (Some Ï) s2 ->
- ( |={E}[E']â–·=> frag_model_is s1 ∗ has_fuel tid Ï f1 ∗
- (frag_model_is s2 -∗ (if decide (Ï âˆˆ live_roles Mdl s2) then has_fuel tid Ï f2 else tid ↦M ∅) -∗
- WP e2 @ tid; E {{ Φ }}))
+ (|={E}[E']â–·=> frag_model_is s1 ∗ frag_free_roles_are fr ∗ has_fuel tid Ï f1 ∗
+ (frag_model_is s2 -∗ frag_free_roles_are fr -∗ (if decide (Ï âˆˆ live_roles Mdl s2) then has_fuel tid Ï f2 else tid ↦M ∅) -∗
+ WP e2 @ tid; E {{ Φ }}))
⊢ WP e1 @ tid; E {{ Φ }}.
Proof.
iIntros (Hpe Hφ Hroles Hfl Hmdl).
rewrite has_fuel_fuels.
iIntros "H".
iApply (wp_lift_pure_step_no_fork_take_step _ _ _ _ _ {[Ï := f1]}
- (if decide (Ï âˆˆ live_roles Mdl s2) then {[Ï := f2]} else ∅) with "[H]"); eauto.
+ (if decide (Ï âˆˆ live_roles Mdl s2) then {[Ï := f2]} else ∅) fr with "[H]"); eauto.
- repeat split.
+ intros ?. rewrite decide_True //. rewrite lookup_singleton //=.
+ + destruct (decide (Ï âˆˆ live_roles _ s2)); set_solver.
+ set_solver.
+ intros Ï' Hdom. destruct (decide (Ï âˆˆ live_roles Mdl s2)); set_solver.
+ intros Ï' Hneq Hin. destruct (decide (Ï âˆˆ live_roles Mdl s2)); set_solver.
+ destruct (decide (Ï âˆˆ live_roles Mdl s2)); set_solver.
- - 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 -has_fuel_fuels //.
- + iDestruct "Hfuels" as "[Hf _]". rewrite dom_empty_L //.
+ + destruct (decide (Ï âˆˆ live_roles Mdl s2)); set_solver.
+ - set_solver.
+ - iMod "H". do 2 iModIntro. iMod "H" as "(Hmod&Hfr&Hfuels&Hkont)". iModIntro.
+ iFrame "Hmod Hfr Hfuels". iIntros "Hmod Hfr Hfuels". iApply ("Hkont" with "Hmod [Hfr] [Hfuels]").
+ + replace (fr ∖ (live_roles Mdl s2 ∖ live_roles Mdl s1)) with fr; [done|set_solver].
+ + destruct (decide (Ï âˆˆ live_roles Mdl s2)).
+ * rewrite -has_fuel_fuels //.
+ * iDestruct "Hfuels" as "[Hf _]". rewrite dom_empty_L //.
Qed.
Lemma wp_lift_pure_step_no_fork_singlerole' tid E E' Φ e1 e2 Ï f:
@@ -825,13 +881,17 @@ Proof.
as "(Hsi & Hl & Hm)".
{ 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)" =>//.
+ iMod (update_no_step_enough_fuel _ _ ∅ with "HfuelS Hmi") as (δ2 ℓ) "([%Hlabel %Hvse] & Hfuel & Hmi)" =>//.
{ by intros ?%dom_empty_inv_L. }
+ { set_solver. }
{ rewrite Hexend. apply head_locale_step. by econstructor. }
iModIntro; iExists δ2, ℓ.
rewrite Hexend //=. iFrame "Hmi Hsi".
repeat iSplit =>//.
- iApply "HΦ". iFrame "Hfuel". iApply big_sepL_sep. iSplitL "Hl".
+ iApply "HΦ". iSplitL "Hfuel".
+ { iApply (has_fuels_proper with "Hfuel") =>//.
+ rewrite map_filter_id //. intros ???%elem_of_dom_2; set_solver. }
+ iApply big_sepL_sep. iSplitL "Hl".
+ by iApply heap_array_to_seq_mapsto.
+ iApply (heap_array_to_seq_meta with "Hm"). by rewrite replicate_length.
Qed.
@@ -853,13 +913,15 @@ Proof.
iDestruct (@gen_heap_valid with "Hsi Hl") as %Hheap.
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)" =>//.
+ iMod (update_no_step_enough_fuel _ _ ∅ with "HfuelS Hmi") as (δ2 ℓ) "([%Hlabels %Hvse] & Hfuel & Hmod)" =>//.
{ by intros ?%dom_empty_inv_L. }
+ { set_solver. }
{ rewrite Hexend. apply head_locale_step. by econstructor. }
iModIntro; iExists _,_.
rewrite Hexend //=. iFrame "Hsi Hmod".
do 2 (iSplit=>//).
- iApply "HΦ". iFrame.
+ iApply "HΦ". iFrame. iApply (has_fuels_proper with "Hfuel") =>//.
+ rewrite map_filter_id //. intros ???%elem_of_dom_2; set_solver.
Qed.
Lemma wp_store_nostep s tid E l v' v fs:
@@ -874,23 +936,25 @@ Proof.
iSplit; first by rewrite Hexend // in Hheap; eauto. iIntros "!>" (e2 σ2 efs Hstep).
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)" =>//.
+ iMod (update_no_step_enough_fuel _ _ ∅ with "HfuelS Hmi") as (δ2 ℓ) "([%Hlabels %Hvse] & Hfuel & Hmod)" =>//.
{ by intros ?%dom_empty_inv_L. }
+ { set_solver. }
{ rewrite Hexend. apply head_locale_step. by econstructor. }
iModIntro; iExists _,_.
rewrite Hexend //=. iFrame "Hsi Hmod".
do 2 (iSplit=>//).
- iApply "HΦ". iFrame.
+ iApply "HΦ". iFrame. iApply (has_fuels_proper with "Hfuel") =>//.
+ rewrite map_filter_id //. intros ???%elem_of_dom_2; set_solver.
Qed.
-Lemma wp_cmpxchg_fail_step_singlerole s tid Ï (f1 f2: nat) s1 s2 E l q v' v1 v2:
+Lemma wp_cmpxchg_fail_step_singlerole s tid Ï (f1 f2: nat) fr s1 s2 E l q v' v1 v2:
v' ≠v1 → vals_compare_safe v' v1 → f2 ≤ fuel_limit s2 -> Mdl.(fmtrans) s1 (Some Ï) s2 ->
live_roles _ s2 ⊆ live_roles _ s1 ->
- {{{ â–· l ↦{q} v' ∗ â–· frag_model_is s1 ∗ â–· has_fuel tid Ï f1 }}} CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; tid; E
- {{{ RET PairV v' (LitV $ LitBool false); l ↦{q} v' ∗ frag_model_is s2 ∗
+ {{{ â–· l ↦{q} v' ∗ â–· frag_model_is s1 ∗ â–· has_fuel tid Ï f1 ∗ â–· frag_free_roles_are fr }}} CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; tid; E
+ {{{ RET PairV v' (LitV $ LitBool false); l ↦{q} v' ∗ frag_model_is s2 ∗ frag_free_roles_are fr ∗
(if decide (Ï âˆˆ live_roles Mdl s2) then has_fuel tid Ï f2 else tid ↦M ∅ ) }}}.
Proof.
- iIntros (?? Hfl Htrans ? Φ) "(>Hl & >Hst & >Hfuel1) HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
+ iIntros (?? Hfl Htrans ? Φ) "(>Hl & >Hst & >Hfuel1 & > Hfr) HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (extr atr K tp1 tp2 σ1 Hval Hexend Hloc) "(% & Hsi & Hmi) !>".
iDestruct (@gen_heap_valid with "Hsi Hl") as %Hheap.
iSplit; first by rewrite Hexend // in Hheap; eauto. iIntros "!>" (e2 σ2 efs Hstep).
@@ -900,34 +964,72 @@ Proof.
rewrite has_fuel_fuels Hexend.
iMod (update_step_still_alive _ _ _ _ _ _ _ _ _
(if decide (Ï âˆˆ live_roles Mdl s2) then {[ Ï := f2 ]} else ∅)
- with "Hfuel1 Hst Hmi") as
- (δ2 ℓ) "([%Hlab %Hvse] & Hfuel & Hst & Hmod)"; eauto.
+ with "Hfuel1 Hst Hmi Hfr") as
+ (δ2 ℓ) "([%Hlab %Hvse] & Hfuel & Hst & Hfr & Hmod)"; eauto.
+ - set_solver.
- destruct (decide (Ï âˆˆ live_roles Mdl s2)); apply head_locale_step; econstructor =>//.
- destruct (decide (Ï âˆˆ live_roles Mdl s2)).
+ split; first by intros _; rewrite lookup_singleton /=; lia.
split; first set_solver.
- split.
- { intros Ï' Hin. exfalso. rewrite dom_singleton_L Hmeq in Hin. set_solver. }
+ split; first set_solver.
+ split; first (intros Ï' Hin; set_solver).
split; set_solver.
+ repeat (split; set_solver).
- rewrite -> bool_decide_eq_false_2 in *; eauto.
iModIntro; iExists δ2, ℓ. iSplit.
{ iPureIntro. simpl in *. split =>//. }
iFrame. iSplit; first done. iApply "HΦ". iFrame.
+ replace (fr ∖ (live_roles Mdl s2 ∖ live_roles Mdl s1)) with fr; [iFrame|set_solver].
destruct (decide (Ï âˆˆ live_roles Mdl s2)).
+ rewrite has_fuel_fuels //.
+ iDestruct "Hfuel" as "[?_]". rewrite dom_empty_L //.
Qed.
-Lemma wp_cmpxchg_suc_step_singlerole s tid Ï (f1 f2: nat) s1 s2 E l v' v1 v2:
+Lemma wp_cmpxchg_suc_step_singlerole_keep_dead s tid Ï (f1 f2: nat) fr s1 s2 E l v' v1 v2:
+ Ï âˆ‰ live_roles _ s2 →
+ v' = v1 → vals_compare_safe v' v1 → f2 < f1 -> Mdl.(fmtrans) s1 (Some Ï) s2 ->
+ live_roles _ s2 ⊆ live_roles _ s1 ->
+ {{{ â–· l ↦ v' ∗ â–· frag_model_is s1 ∗ â–· has_fuel tid Ï f1 ∗ â–· frag_free_roles_are fr }}}
+ CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; tid; E
+ {{{ RET PairV v' (LitV $ LitBool true); l ↦ v2 ∗ frag_model_is s2 ∗ frag_free_roles_are fr ∗
+ has_fuel tid Ï f2 }}}.
+Proof.
+ iIntros (??? Hfl Htrans ? Φ) "(>Hl & >Hst & >Hfuel1 & >Hfr) HΦ".
+ iApply wp_lift_atomic_head_step_no_fork; auto.
+ iIntros (extr atr K tp1 tp2 σ1 Hval Hexend Hloc) "(% & Hsi & Hmi) !>".
+ iDestruct (@gen_heap_valid with "Hsi Hl") as %Hheap.
+ iSplit; first by rewrite Hexend // in Hheap; eauto. iIntros "!>" (e2 σ2 efs Hstep).
+ rewrite Hexend in Hheap. inv_head_step.
+ iDestruct (model_agree' with "Hmi Hst") as %Hmeq.
+ rewrite bool_decide_true //.
+ iMod (@gen_heap_update with "Hsi Hl") as "[Hsi Hl]".
+ rewrite has_fuel_fuels Hexend.
+ iMod (update_step_still_alive _ _ _ _ _ _ _ _ _ {[ Ï := f2 ]} with "Hfuel1 Hst Hmi Hfr") as
+ (δ2 ℓ) "([%Hlab %Hvse] & Hfuel & Hst & Hfr & Hmod)"; eauto.
+ - set_solver.
+ - apply head_locale_step; econstructor =>//.
+ - repeat (split; try done); [|set_solver|set_solver|set_solver| set_solver |].
+ + intros ??. rewrite !lookup_singleton /=. lia.
+ + rewrite dom_singleton singleton_subseteq_l. simplify_eq.
+ destruct (decide (Ï âˆˆ live_roles _ (trace_last atr))); set_solver.
+ - rewrite -> bool_decide_eq_true_2 in *; eauto.
+ iModIntro; iExists δ2, ℓ. iSplit.
+ { iPureIntro. simpl in *. split =>//. }
+ iFrame. iSplit; first done. iApply "HΦ". iFrame.
+ replace (fr ∖ (live_roles Mdl s2 ∖ live_roles Mdl s1)) with fr; [iFrame|set_solver].
+ by rewrite has_fuel_fuels.
+Qed.
+
+Lemma wp_cmpxchg_suc_step_singlerole s tid Ï (f1 f2: nat) fr s1 s2 E l v' v1 v2:
v' = v1 → vals_compare_safe v' v1 → f2 ≤ fuel_limit s2 -> Mdl.(fmtrans) s1 (Some Ï) s2 ->
live_roles _ s2 ⊆ live_roles _ s1 ->
- {{{ â–· l ↦ v' ∗ â–· frag_model_is s1 ∗ â–· has_fuel tid Ï f1 }}}
+ {{{ â–· l ↦ v' ∗ â–· frag_model_is s1 ∗ â–· has_fuel tid Ï f1 ∗ â–· frag_free_roles_are fr }}}
CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; tid; E
- {{{ RET PairV v' (LitV $ LitBool true); l ↦ v2 ∗ frag_model_is s2 ∗
+ {{{ RET PairV v' (LitV $ LitBool true); l ↦ v2 ∗ frag_model_is s2 ∗ frag_free_roles_are fr ∗
(if decide (Ï âˆˆ live_roles Mdl s2) then has_fuel tid Ï f2 else tid ↦M ∅ ) }}}.
Proof.
- iIntros (?? Hfl Htrans ? Φ) "(>Hl & >Hst & >Hfuel1) HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
+ iIntros (?? Hfl Htrans ? Φ) "(>Hl & >Hst & >Hfuel1 & >Hfr) HΦ".
+ iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (extr atr K tp1 tp2 σ1 Hval Hexend Hloc) "(% & Hsi & Hmi) !>".
iDestruct (@gen_heap_valid with "Hsi Hl") as %Hheap.
iSplit; first by rewrite Hexend // in Hheap; eauto. iIntros "!>" (e2 σ2 efs Hstep).
@@ -938,20 +1040,21 @@ Proof.
rewrite has_fuel_fuels Hexend.
iMod (update_step_still_alive _ _ _ _ _ _ _ _ _
(if decide (Ï âˆˆ live_roles Mdl s2) then {[ Ï := f2 ]} else ∅)
- with "Hfuel1 Hst Hmi") as
- (δ2 ℓ) "([%Hlab %Hvse] & Hfuel & Hst & Hmod)"; eauto.
+ with "Hfuel1 Hst Hmi Hfr") as
+ (δ2 ℓ) "([%Hlab %Hvse] & Hfuel & Hst & Hfr & Hmod)"; eauto.
+ - set_solver.
- destruct (decide (Ï âˆˆ live_roles Mdl s2)); apply head_locale_step; econstructor =>//.
- destruct (decide (Ï âˆˆ live_roles Mdl s2)).
+ split; first by intros _; rewrite lookup_singleton /=; lia.
split; first set_solver.
- split.
- { intros Ï' Hin. exfalso. rewrite dom_singleton_L Hmeq in Hin. set_solver. }
+ split; first set_solver.
split; set_solver.
+ repeat (split; set_solver).
- rewrite -> bool_decide_eq_true_2 in *; eauto.
iModIntro; iExists δ2, ℓ. iSplit.
{ iPureIntro. simpl in *. split =>//. }
iFrame. iSplit; first done. iApply "HΦ". iFrame.
+ replace (fr ∖ (live_roles Mdl s2 ∖ live_roles Mdl s1)) with fr; [iFrame|set_solver].
destruct (decide (Ï âˆˆ live_roles Mdl s2)).
+ rewrite has_fuel_fuels //.
+ iDestruct "Hfuel" as "[?_]". rewrite dom_empty_L //.
diff --git a/fairness/resources.v b/fairness/resources.v
index 58a4d79..e088b73 100644
--- a/fairness/resources.v
+++ b/fairness/resources.v
@@ -11,6 +11,7 @@ Class fairnessGpreS (Mdl : FairModel) Λ Σ `{Countable (locale Λ)} := {
fairnessGpreS_model :> inG Σ (authUR (optionUR (exclR (ModelO Mdl))));
fairnessGpreS_model_mapping :> inG Σ (authUR (gmapUR (localeO Λ) (exclR (gsetR (RoleO Mdl)))));
fairnessGpreS_model_fuel :> inG Σ (authUR (gmapUR (RoleO Mdl) (exclR natO)));
+ fairnessGpreS_model_free_roles :> inG Σ (authUR (gset_disjUR (RoleO Mdl)));
}.
Class fairnessGS (Mdl: FairModel) Λ Σ `{Countable (locale Λ)} := FairnessGS {
@@ -21,17 +22,21 @@ Class fairnessGS (Mdl: FairModel) Λ Σ `{Countable (locale Λ)} := FairnessGS {
fairness_model_mapping_name : gname;
(** Mapping of roles to fuel *)
fairness_model_fuel_name : gname;
+ (** Set of free/availble roles *)
+ fairness_model_free_roles_name : gname;
}.
Global Arguments FairnessGS Mdl Λ Σ {_ _ _} _ _ _.
Global Arguments fairness_model_name {Mdl Λ Σ _ _} _.
Global Arguments fairness_model_mapping_name {Mdl Λ Σ _ _} _ : assert.
Global Arguments fairness_model_fuel_name {Mdl Λ Σ _ _} _ : assert.
+Global Arguments fairness_model_free_roles_name {Mdl Λ Σ _ _} _ : assert.
Definition fairnessΣ (Mdl: FairModel) Λ `{Countable (locale Λ)} : gFunctors := #[
GFunctor (authUR (optionUR (exclR (ModelO Mdl))));
GFunctor (authUR (gmapUR (localeO Λ) (exclR (gsetR (RoleO Mdl)))));
- GFunctor (authUR (gmapUR (RoleO Mdl) (exclR natO)))
+ GFunctor (authUR (gmapUR (RoleO Mdl) (exclR natO)));
+ GFunctor (authUR (gset_disjUR (RoleO Mdl)))
].
Global Instance subG_fairnessGpreS {Σ Λ Mdl} `{Countable (locale Λ)} :
@@ -159,50 +164,6 @@ Section map_imap.
Qed.
End map_imap.
-Section locales_utils.
- Context {Λ: language}.
-
- Definition locales_of_list_from tp0 (tp: list $ expr Λ): list $ locale Λ :=
- (λ '(t, e), locale_of t e) <$> (prefixes_from tp0 tp).
- Notation locales_of_list tp := (locales_of_list_from [] tp).
-
- Lemma locales_of_list_equiv tp0 tp0' tp1 tp2:
- locales_equiv_from tp0 tp0' tp1 tp2 →
- locales_of_list_from tp0 tp1 = locales_of_list_from tp0' tp2.
- Proof.
- revert tp0 tp0' tp1. induction tp2; intros tp0 tp0' tp1 H;
- destruct tp1 as [|e1 tp1]; try by apply Forall2_length in H.
- unfold locales_of_list_from. simpl.
- simpl in H. apply Forall2_cons_1 in H as [??]. f_equal =>//.
- apply IHtp2 =>//.
- Qed.
-
- Lemma locales_of_list_step_incl σ1 σ2 oζ tp1 tp2 :
- locale_step (tp1, σ1) oζ (tp2, σ2) ->
- locales_of_list tp1 ⊆ locales_of_list tp2.
- Proof.
- intros H. inversion H; simplify_eq=>//.
- replace (t1 ++ e2 :: t2 ++ efs) with ((t1 ++ e2 :: t2) ++ efs); last by list_simplifier.
- rewrite /locales_of_list_from. rewrite [in X in _ ⊆ X]prefixes_from_app /= fmap_app.
- assert ((λ '(t, e), locale_of t e) <$> prefixes (t1 ++ e1 :: t2) = (λ '(t, e), locale_of t e) <$> prefixes (t1 ++ e2 :: t2))
- as ->; last set_solver.
- apply locales_of_list_equiv, locales_equiv_middle. by eapply locale_step_preserve.
- Qed.
-
- Lemma locales_of_list_from_locale_from `{EqDecision (locale Λ)} tp0 tp1 ζ:
- is_Some (from_locale_from tp0 tp1 ζ) ->
- ζ ∈ locales_of_list_from tp0 tp1.
- Proof.
- revert tp0; induction tp1 as [|e1 tp1 IH]; intros tp0.
- { simpl. intros H. inversion H. congruence. }
- simpl. intros [e Hsome]. rewrite /locales_of_list_from /=.
- destruct (decide (locale_of tp0 e1 = ζ)); simplify_eq; first set_solver.
- apply elem_of_cons; right. apply IH. eauto.
- Qed.
-
-End locales_utils.
-Notation locales_of_list tp := (locales_of_list_from [] tp).
-
Section model_state_interp.
Context {Mdl: FairModel}.
Context `{fG: fairnessGS Mdl Λ Σ}.
@@ -235,16 +196,22 @@ Section model_state_interp.
Definition frag_model_is (M: Mdl): iProp Σ :=
own (fairness_model_name fG) (â—¯ Excl' M).
+ Definition auth_free_roles_are (FR: gset Role): iProp Σ :=
+ own (fairness_model_free_roles_name fG) (â— (GSet FR)).
+
+ Definition frag_free_roles_are (FR: gset Role): iProp Σ :=
+ own (fairness_model_free_roles_name fG) (â—¯ (GSet FR)).
+
Definition model_state_interp (tp: list $ expr Λ) (δ: LiveState Mdl): iProp Σ :=
- ∃ M, auth_fuel_is δ.(ls_fuel) ∗
- auth_mapping_is M ∗ ⌜maps_inverse_match δ.(ls_mapping) M⌠∗
+ ∃ M FR, auth_fuel_is δ.(ls_fuel) ∗ auth_mapping_is M ∗ auth_free_roles_are FR ∗
+ ⌜maps_inverse_match δ.(ls_mapping) M⌠∗
⌜ ∀ ζ, ζ ∉ locales_of_list tp → M !! ζ = None ⌠∗
- auth_model_is δ.
+ auth_model_is δ ∗ ⌜ FR ∩ dom δ.(ls_fuel) = ∅ âŒ.
Lemma model_state_interp_tids_smaller δ tp :
model_state_interp tp δ -∗ ⌜ tids_smaller tp δ âŒ.
Proof.
- iIntros "(%M&_&_&%Hminv&%Hbig&_)". iPureIntro.
+ iIntros "(%M&%FR&_&_&_&%Hminv&%Hbig&_)". iPureIntro.
intros Ï Î¶ Hin.
assert (¬ (ζ ∉ locales_of_list tp)).
- intros contra.
@@ -397,6 +364,14 @@ Section adequacy.
iExists _. by iSplitL "H1".
Qed.
+ Lemma model_free_roles_init `{fairnessGpreS Mdl Λ Σ} (s0: Mdl) (FR: gset _):
+ ⊢ |==> ∃ γ,
+ own (A := authUR (gset_disjUR (RoleO Mdl))) γ (◠GSet FR ⋅ ◯ GSet FR).
+ Proof.
+ iMod (own_alloc (◠GSet FR ⋅ ◯ GSet FR)) as (γ) "[H1 H2]".
+ { apply auth_both_valid_2 =>//. }
+ iExists _. by iSplitL "H1".
+ Qed.
End adequacy.
Section model_state_lemmas.
@@ -413,6 +388,43 @@ Section model_state_lemmas.
- iModIntro. iFrame.
Qed.
+ Lemma free_roles_inclusion FR fr:
+ auth_free_roles_are FR -∗
+ frag_free_roles_are fr -∗
+ ⌜fr ⊆ FRâŒ.
+ Proof.
+ iIntros "HFR Hfr".
+ iDestruct (own_valid_2 with "HFR Hfr") as %Hval. iPureIntro.
+ apply auth_both_valid_discrete in Hval as [??].
+ by apply gset_disj_included.
+ Qed.
+
+ Lemma update_free_roles rem FR fr1:
+ rem ⊆ fr1 ->
+ auth_free_roles_are FR -∗
+ frag_free_roles_are fr1 ==∗
+ auth_free_roles_are (FR ∖ rem) ∗
+ frag_free_roles_are (fr1 ∖ rem).
+ Proof.
+ iIntros (?) "HFR Hfr1".
+
+ iDestruct (free_roles_inclusion with "HFR Hfr1") as %Hincl.
+
+ replace FR with ((FR ∖ rem) ∪ rem); last first.
+ { rewrite difference_union_L. set_solver. }
+ replace fr1 with ((fr1 ∖ rem) ∪ rem); last first.
+ { rewrite difference_union_L. set_solver. }
+
+ iAssert (frag_free_roles_are (fr1 ∖ rem) ∗ frag_free_roles_are rem)%I with "[Hfr1]" as "[Hfr2 Hrem]".
+ { rewrite /frag_free_roles_are -own_op -auth_frag_op gset_disj_union //. set_solver. }
+
+ iCombine "HFR Hrem" as "H".
+ iMod (own_update with "H") as "[??]" ; eauto.
+ - apply auth_update, gset_disj_dealloc_local_update.
+ - iModIntro. iFrame. iApply (own_proper with "Hfr2").
+ do 2 f_equiv. set_solver.
+ Qed.
+
Lemma model_agree s1 s2:
auth_model_is s1 -∗ frag_model_is s2 -∗ ⌜ s1 = s2 âŒ.
Proof.
@@ -424,7 +436,7 @@ Section model_state_lemmas.
Lemma model_agree' δ1 s2 n:
model_state_interp n δ1 -∗ frag_model_is s2 -∗ ⌜ ls_under δ1 = s2 âŒ.
Proof.
- iIntros "Hsi Hs2". iDestruct "Hsi" as (?) "(_&_&_&_&Hs1)".
+ iIntros "Hsi Hs2". iDestruct "Hsi" as (??) "(_&_&_&_&_&Hs1&_)".
iApply (model_agree with "Hs1 Hs2").
Qed.
@@ -450,9 +462,9 @@ Section model_state_lemmas.
| right _ => F !! Ï
end) (gset_to_gmap (0%nat) LR).
- Definition update_fuel_resource (δ1: LiveState Mdl) (fs2: gmap (fmrole Mdl) nat) (s2: Mdl):
+ Definition update_fuel_resource (δ1: LiveState Mdl) (fs1 fs2: gmap (fmrole Mdl) nat) (s2: Mdl):
gmap (fmrole Mdl) nat :=
- fuel_apply fs2 (δ1.(ls_fuel (Λ := Λ))) (live_roles _ s2).
+ fuel_apply fs2 (δ1.(ls_fuel (Λ := Λ))) (((dom $ ls_fuel δ1) ∪ dom fs2) ∖ (dom fs1 ∖ dom fs2)).
Lemma elem_of_frame_excl_map
(fs F: gmap (fmrole Mdl) nat)
@@ -664,6 +676,24 @@ Section model_state_lemmas.
Qed.
Lemma update_has_fuels_no_step ζ fs fs' F M:
+ let LR := (dom F ∪ dom fs') ∖ (dom fs ∖ dom fs') in
+ (fs ≠∅) ->
+ (dom fs' ⊆ dom fs) ->
+ has_fuels ζ fs -∗
+ auth_fuel_is F -∗
+ auth_mapping_is M ==∗
+ auth_fuel_is (fuel_apply fs' F LR) ∗
+ has_fuels ζ fs' ∗
+ auth_mapping_is (<[ ζ := dom fs' ]> M).
+ Proof.
+ iIntros (LR Hfs Hdom) "Hfuels Hafuels Hamapping".
+ rewrite !has_fuels_equiv. iDestruct "Hfuels" as "[Hmapping Hfuels]".
+ iMod (update_fuel fs fs' with "Hafuels Hfuels") as "[Hafuels Hfuels]"; [done|set_solver|].
+ iMod (update_mapping with "Hamapping Hmapping") as "[Hamapping Hmapping]".
+ iModIntro. iFrame.
+ Qed.
+
+ Lemma update_has_fuels_no_step_no_change ζ fs fs' F M:
let LR := (dom F ∪ dom fs') ∖ (dom fs ∖ dom fs') in
(fs ≠∅) ->
(dom fs' = dom fs) ->
@@ -686,7 +716,7 @@ Section model_state_lemmas.
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ζ Hfuels] (%M&Hafuel&Hamapping&%Hmapinv&Hamod) %Ï".
+ iIntros "[Hζ Hfuels] (%M&%FR&Hafuel&Hamapping &HFR&%Hmapinv&Hamod&Hfr) %Ï".
iCombine "Hamapping Hζ" as "H".
iDestruct (own_valid with "H") as %Hval. iPureIntro.
apply auth_both_valid_discrete in Hval as [Hval ?].
@@ -703,7 +733,7 @@ Section model_state_lemmas.
has_fuels ζ fs -∗ model_state_interp n δ -∗ ⌜ ∀ Ï, Ï âˆˆ dom fs -> ls_fuel δ !! Ï = fs !! Ï âŒ.
Proof.
unfold has_fuels, model_state_interp, auth_fuel_is.
- iIntros "[Hζ Hfuels] (%M&Hafuel&Hamapping&%Hmapinv&Hamod)" (Ï HÏ).
+ iIntros "[Hζ Hfuels] (%M&%FR&Hafuel&Hamapping&HFR&%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.
@@ -715,93 +745,159 @@ Section model_state_lemmas.
rewrite HfuelÏ Hfs //.
Qed.
- Lemma update_no_step_enough_fuel extr (auxtr : auxiliary_trace (fair_model Mdl)) c2 fs ζ:
+ Lemma update_no_step_enough_fuel extr (auxtr : auxiliary_trace (fair_model Mdl)) rem c2 fs ζ:
(dom fs ≠∅) ->
+ (live_roles _ (trace_last auxtr)) ∩ rem = ∅ →
+ rem ⊆ dom fs →
locale_step (trace_last extr) (Some ζ) c2 ->
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 ζ fs ∗ model_state_interp c2.1 δ2.
+ ∗ has_fuels ζ (fs ⇂ (dom fs ∖ rem)) ∗ model_state_interp c2.1 δ2.
Proof.
- iIntros "%HnotO %Hstep Hf Hmod".
+ iIntros "%HnotO %Holdroles %Hincl %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 "%Hfuel"; eauto.
iDestruct (model_state_interp_tids_smaller with "Hmod") as %Hζs.
- iDestruct "Hmod" as "(%M & Hfuel & Hamapping & %Hminv & %Hlocssmall & Hmodel)".
+ iDestruct "Hmod" as "(%M & %FR & Hfuel & Hamapping & HFR & %Hminv & %Hlocssmall & Hmodel & %HFR)".
unfold has_fuels_S.
simpl in *.
- iMod (update_has_fuels_no_step ζ (S <$> fs) fs with "[Hf] [Hfuel] [Hamapping]") as "(Hafuels&Hfuels&Hamapping)" =>//.
- { rewrite -dom_empty_iff_L. set_solver. }
- { set_solver. }
- iModIntro.
- assert (Hfueldom: dom (fuel_apply fs (ls_fuel (trace_last auxtr))
- ((dom (ls_fuel (trace_last auxtr)) ∪ dom fs) ∖ (dom fs ∖ dom fs))) =
- live_roles Mdl (trace_last auxtr)).
- { unfold fuel_apply.
- assert (dom fs ⊆ live_roles Mdl (trace_last auxtr)).
- { intros Ï Hin. rewrite -ls_fuel_dom elem_of_dom Hfuel; last set_solver.
+ set new_dom := ((dom (ls_fuel (trace_last auxtr)) ∪ dom fs) ∖ rem).
+ set new_mapping := ls_mapping (trace_last auxtr) ⇂ new_dom.
+
+ assert (dom (fuel_apply (filter (λ '(k, _), k ∈ dom fs ∖ rem) fs) (ls_fuel (trace_last auxtr))
+ ((dom (ls_fuel (trace_last auxtr)) ∪ dom fs) ∖ rem)) = new_dom) as Hnewdom.
+ { rewrite /fuel_apply map_imap_dom_eq ?dom_gset_to_gmap //.
+ intros Ï0 _ Hindom.
+ destruct (decide (Ï0 ∈ dom (filter (λ '(k, _), k ∈ dom fs ∖ rem) fs))) as [Hinf|Hninf];
+ first by apply elem_of_dom.
+ apply elem_of_difference in Hindom as [Hin1 ?].
+ apply elem_of_union in Hin1 as [?|Hin2]; first by apply elem_of_dom.
+ exfalso. apply Hninf. apply elem_of_dom in Hin2 as [f ?].
+ eapply elem_of_dom_2. rewrite map_filter_lookup_Some. split =>//.
+ apply elem_of_difference; split =>//. by eapply elem_of_dom_2. }
+
+ assert (Hsamedoms: dom new_mapping =
+ dom (fuel_apply (fs ⇂ (dom fs ∖ rem))
+ (ls_fuel (trace_last auxtr))
+ ((dom (ls_fuel (trace_last auxtr)) ∪ dom fs) ∖ rem))).
+ { rewrite /new_mapping /new_dom. unfold fuel_apply.
+ assert (dom fs ⊆ dom (trace_last auxtr).(ls_fuel)).
+ { intros Ï Hin. rewrite elem_of_dom Hfuel; last set_solver.
apply elem_of_dom in Hin as [? Hin]. rewrite lookup_fmap Hin //=. }
- rewrite (ls_fuel_dom (trace_last auxtr)) map_imap_dom_eq.
- + rewrite dom_gset_to_gmap. set_solver.
- + intros Ï _ Hin. rewrite dom_gset_to_gmap in Hin.
- destruct (decide (Ï âˆˆ dom fs)) as [Hin'|_].
+ rewrite map_imap_dom_eq; last first.
+ { intros Ï _ Hin. rewrite dom_gset_to_gmap in Hin.
+ destruct (decide (Ï âˆˆ dom $ fs ⇂ (dom fs ∖ rem))) as [Hin'|_].
* by apply elem_of_dom.
- * apply elem_of_dom. rewrite ls_fuel_dom. set_solver. }
- assert (Hmappingdom: dom (ls_mapping (trace_last auxtr)) = live_roles _ (trace_last auxtr)).
- { apply ls_mapping_dom. }
+ * apply elem_of_dom. set_solver. }
+ rewrite dom_domain_restrict ?dom_gset_to_gmap ?ls_same_doms //. set_solver. }
+ assert (Hfueldom: live_roles _ (trace_last auxtr) ⊆
+ dom (fuel_apply (fs ⇂ (dom fs ∖ rem))
+ (ls_fuel (trace_last auxtr))
+ ((dom (ls_fuel (trace_last auxtr)) ∪ dom fs) ∖ rem))).
+ { rewrite /fuel_apply Hnewdom.
+ intros Ï Hin. apply elem_of_difference; split;
+ [apply ls_fuel_dom in Hin; set_solver | set_solver]. }
+
+ iMod (update_has_fuels_no_step ζ (S <$> fs) (fs ⇂ (dom fs ∖ rem)) with "[Hf] [Hfuel] [Hamapping]") as "(Hafuels&Hfuels&Hamapping)" =>//.
+ { rewrite -dom_empty_iff_L. set_solver. }
+ { rewrite dom_domain_restrict; set_solver. }
+
+ iModIntro.
iExists {|
ls_under := (trace_last auxtr).(ls_under);
ls_fuel := _;
ls_fuel_dom := Hfueldom;
- ls_mapping := (trace_last auxtr).(ls_mapping);
- ls_mapping_dom := Hmappingdom;
+ ls_same_doms := Hsamedoms;
|}.
iExists (Silent_step ζ). simpl.
iSplit; last first.
- { rewrite (dom_fmap_L _ fs). iFrame "Hfuels". iExists M. rewrite /maps_inverse_match //=. iFrame.
- iPureIntro. split; first set_solver.
- unfold tids_smaller; simpl. intros ζ0 Hin.
- unfold tids_smaller in Hζs.
- apply Hlocssmall.
- destruct (trace_last extr).
- have ? := locales_of_list_step_incl _ _ _ _ _ Hstep. simpl.
- clear Hfueldom Hmappingdom. set_solver. }
- iSplit =>//. iSplit; first done. iSplit; last first.
- { iPureIntro.
- unfold tids_smaller; simpl. intros Ï Î¶0 Hsome.
- specialize (Hζs _ _ Hsome).
- destruct (trace_last extr); eapply from_locale_step =>//. }
- iSplit.
- { iPureIntro. eexists. apply Hxdom. by rewrite dom_fmap. }
- iSplit.
- { unfold fuel_decr. simpl.
- iIntros "!%" (Ï' HÏ'live Hmustdec).
+ { rewrite (dom_fmap_L _ fs). iFrame "Hfuels". iExists _, FR. rewrite /maps_inverse_match //=. iFrame.
+ assert (dom fs ⊆ dom (ls_fuel $ trace_last auxtr)).
+ { intros Ï Hin. setoid_rewrite dom_fmap in Hxdom.
+ specialize (Hxdom Ï). rewrite -ls_same_doms. apply elem_of_dom. exists ζ.
+ by apply Hxdom. }
+ iSplit.
+ { iApply (auth_fuel_is_proper with "Hafuels"). f_equiv.
+ rewrite dom_domain_restrict; last set_solver.
+ replace (dom fs ∖ (dom fs ∖ rem)) with rem; [set_solver|].
+ rewrite -leibniz_equiv_iff. intros Ï. split; [set_solver|].
+ intros [? [?|?]%not_elem_of_difference]%elem_of_difference =>//. }
+ iPureIntro. split; last split.
+ - intros Ï Î¶'. rewrite /new_mapping dom_domain_restrict; last set_solver. split.
+ + intros [Hlk Hin]%map_filter_lookup_Some. destruct (decide (ζ' = ζ)) as [->|Hneq].
+ * rewrite lookup_insert. eexists; split=>//. set_solver.
+ * rewrite lookup_insert_ne //. by apply Hminv.
+ + intros Hin. destruct (decide (ζ' = ζ)) as [->|Hneq].
+ * rewrite lookup_insert in Hin. apply map_filter_lookup_Some.
+ destruct Hin as (?&?&?). simplify_eq. split; last set_solver.
+ apply Hxdom. rewrite dom_fmap. set_solver.
+ * rewrite lookup_insert_ne // -Hminv in Hin. apply map_filter_lookup_Some; split=>//.
+ rewrite /new_dom. apply elem_of_difference; split.
+ ** apply elem_of_dom_2 in Hin. rewrite ls_same_doms in Hin. set_solver.
+ ** assert (Ï âˆ‰ dom fs); last set_solver. rewrite dom_fmap_L in Hxdom.
+ intros contra%Hxdom. congruence.
+ - intros ζ0 Hnotin. apply lookup_insert_None; split.
+ + apply Hlocssmall.
+ destruct (trace_last extr).
+ have ? := locales_of_list_step_incl _ _ _ _ _ Hstep. simpl.
+ clear Hfueldom Hsamedoms. set_solver.
+ + intros <-.
+ destruct (trace_last extr).
+ have ? := locales_of_list_step_incl _ _ _ _ _ Hstep. simpl.
+ clear Hfueldom Hsamedoms. inversion Hstep. simplify_eq.
+ assert (locale_of t1 e1 ∈ locales_of_list (t1 ++ e1 :: t2)); last set_solver.
+ apply locales_of_list_from_locale_from.
+ rewrite from_locale_from_Some // prefixes_from_spec. eexists _,_. by list_simplifier.
+ - rewrite Hnewdom /new_dom. apply elem_of_equiv_empty_L. intros Ï [Hin1 Hin2]%elem_of_intersection.
+ assert (Ï âˆˆ dom (ls_fuel (trace_last auxtr))) by set_solver. set_solver. }
+ iPureIntro.
+ do 2 split; first done. split; [split; [|split; [|split; [|split]]]|] =>//.
+ - eexists. apply Hxdom. by rewrite dom_fmap.
+ - unfold fuel_decr. simpl.
+ intros Ï' Hin Hin' Hmustdec.
+ rewrite Hnewdom in Hin'.
+
inversion Hmustdec; simplify_eq.
- 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.
- destruct (fs!!Ï') as [f'|]=> //=.
- simpl in Heq. injection Heq=>Heq'. rewrite -Heq'.
- rewrite lookup_gset_to_gmap option_guard_True /=; last by set_solver. lia.
- + have: Ï' ∉ dom (S <$> fs).
- { apply not_elem_of_dom. rewrite lookup_fmap //. }
- set_solver. }
- iPureIntro. split=>//. intros Ï' Hin _.
- rewrite map_lookup_imap. rewrite -ls_fuel_dom in Hin.
- apply elem_of_dom in Hin as [f Hf]. rewrite Hf /=.
- destruct (decide (Ï' ∈ dom fs)).
- + rewrite lookup_gset_to_gmap option_guard_True /=; last by set_solver.
- rewrite -Hf Hfuel; last set_solver. rewrite lookup_fmap.
- destruct (fs!!Ï') as [f'|] eqn:Heq'; first (simpl; lia).
- rewrite Hfuel in Hf; last set_solver. rewrite lookup_fmap Heq' // in Hf.
- + assert (Ï' ∈ dom (ls_fuel (trace_last auxtr))).
- { apply elem_of_dom. eexists _; done. }
- rewrite lookup_gset_to_gmap option_guard_True /=; [lia | set_solver].
+ + have Hinfs: Ï' ∈ dom (S <$> fs) by set_solver.
+ rewrite map_lookup_imap Hfuel // lookup_fmap. rewrite dom_fmap in Hinfs.
+ rewrite lookup_gset_to_gmap option_guard_True //=.
+
+ pose proof Hinfs as Hinfs'. apply elem_of_dom in Hinfs' as [f Heqf].
+ assert (filter (λ '(k, _), k ∈ dom fs ∖ rem) fs !! Ï' = Some f) as Heqfilter.
+ { rewrite map_filter_lookup Heqf /= option_guard_True //. set_solver. }
+ rewrite decide_True // ?Heqfilter ?lookup_fmap ?Heqf /=; last by eapply elem_of_dom_2. lia.
+ + rewrite /= /new_mapping map_filter_lookup in Hneqtid.
+ pose proof Hin as Hin2. rewrite -ls_same_doms in Hin2. apply elem_of_dom in Hin2 as [f Hf].
+ rewrite Hf /= option_guard_True // in Hneqtid.
+ - intros Ï' Hin _. simpl. destruct (decide (Ï' ∈ rem)) as [Hin'|Hnin'].
+ + right; split; last set_solver. rewrite /fuel_apply map_imap_dom_eq ?dom_gset_to_gmap; first set_solver.
+ intros Ï0 _ Hin0. destruct (decide (Ï0 ∈ dom (filter (λ '(k, _), k ∈ dom fs ∖ rem) fs))) as [?|Hnin];
+ first by apply elem_of_dom.
+ apply elem_of_difference in Hin0 as [Hin1 ?].
+ apply elem_of_union in Hin1 as [?|Hin2]; first by apply elem_of_dom.
+ exfalso. apply Hnin. apply elem_of_dom in Hin2 as [f ?].
+ eapply elem_of_dom_2. rewrite map_filter_lookup_Some. split =>//.
+ apply elem_of_difference; split =>//. by eapply elem_of_dom_2.
+ + left. rewrite map_lookup_imap lookup_gset_to_gmap option_guard_True //=; last set_solver.
+ apply elem_of_dom in Hin as [f Hf].
+ destruct (decide (Ï' ∈ dom (filter (λ '(k, _), k ∈ dom fs ∖ rem) fs))) as [Hin|?];
+ last by rewrite !Hf //=.
+ apply elem_of_dom in Hin as [f' Hf']. rewrite Hf'.
+ apply map_filter_lookup_Some in Hf' as [Hfs Hf'].
+ rewrite Hfuel ?lookup_fmap ?Hfs /=; [lia |]. rewrite dom_fmap; set_solver.
+ - rewrite Hnewdom. assert (dom fs ⊆ dom $ ls_fuel (trace_last auxtr)); last set_solver.
+ intros Ï Hin. apply elem_of_dom. rewrite Hfuel ?dom_fmap // -elem_of_dom dom_fmap //.
+ - unfold tids_smaller; simpl. intros Ï Î¶0 Hin.
+ destruct (trace_last extr); destruct (trace_last extr).
+ eapply from_locale_step =>//.
+ rewrite /tids_smaller /= in Hζs. eapply Hζs.
+ rewrite /new_mapping map_filter_lookup_Some in Hin.
+ by destruct Hin.
Qed.
Lemma update_fork_split R1 R2 tp1 tp2 fs (extr : execution_trace Λ)
@@ -822,11 +918,11 @@ Section model_state_lemmas.
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 "Hmod" as (M FR) "(Haf&Ham&HFR&%Hminv&%Hsmall&Hamod&%HFR)".
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)".
+ iMod (update_has_fuels_no_step_no_change ζ (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 //. }
@@ -846,29 +942,33 @@ Section model_state_lemmas.
apply prefixes_from_spec.
exists t0, []. split =>//. by list_simplifier. }
- iMod (update_mapping_new_locale ζ _ _ R1 R2 with "Ham Hf") as "(Ham&HR1&HR2)"; eauto.
+ iMod (update_mapping_new_locale ζ (locale_of tp1 efork) _ R1 R2 with "Ham Hf") as "(Ham&HR1&HR2)"; eauto.
pose δ1 := trace_last auxtr.
- assert (Hfueldom: dom (map_imap
- (λ Ï o,
- if decide (Ï âˆˆ R1 ∪ R2) then Some (o - 1)%nat else Some o)
- (ls_fuel δ1)) = live_roles Mdl δ1).
- { rewrite map_imap_dom_eq; first rewrite ls_fuel_dom //.
- intros Ï f Hin. destruct (decide (Ï âˆˆ R1 ∪ R2)); eauto. }
- assert (Hmappingdom: dom (map_imap
+ assert (Hsamedoms: dom (map_imap
(λ Ï o,
if decide (Ï âˆˆ R2) then Some $ locale_of tp1 efork else Some o)
- (ls_mapping δ1)) = live_roles Mdl δ1).
- { rewrite map_imap_dom_eq; first rewrite ls_mapping_dom //.
- intros Ï f Hin. destruct (decide (Ï âˆˆ R2)); eauto. }
+ (ls_mapping δ1)) =
+ dom (map_imap
+ (λ Ï o,
+ if decide (Ï âˆˆ R1 ∪ R2) then Some (o - 1)%nat else Some o)
+ (ls_fuel δ1))
+ ).
+ { rewrite !map_imap_dom_eq; first by rewrite ls_same_doms.
+ - by intros Ï??; destruct (decide (Ï âˆˆ R1 ∪ R2)).
+ - by intros Ï??; destruct (decide (Ï âˆˆ R2)). }
+ assert (Hfueldom: live_roles _ δ1 ⊆ dom (map_imap
+ (λ Ï o,
+ if decide (Ï âˆˆ R1 ∪ R2) then Some (o - 1)%nat else Some o)
+ (ls_fuel δ1))).
+ { rewrite map_imap_dom_eq; first by apply ls_fuel_dom.
+ - by intros Ï??; destruct (decide (Ï âˆˆ R1 ∪ R2)). }
iExists {|
ls_under := δ1.(ls_under);
- ls_fuel :=
- map_imap (λ Ï o, if (decide (Ï âˆˆ R1 ∪ R2)) then Some (o-1)%nat else Some o) (ls_fuel δ1);
+ ls_fuel := _;
ls_fuel_dom := Hfueldom;
- ls_mapping :=
- map_imap (λ Ï o, if (decide (Ï âˆˆ R2)) then Some $ locale_of tp1 efork else Some o) (ls_mapping δ1);
- ls_mapping_dom := Hmappingdom;
+ ls_mapping := _;
+ ls_same_doms := Hsamedoms;
|}.
iModIntro.
assert (Hdomincl: dom fs ⊆ dom (ls_fuel δ1)).
@@ -884,8 +984,8 @@ Section model_state_lemmas.
{ 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".
+ iSplitL "Ham Haf Hamod HFR".
+ { iExists _, FR; simpl. iFrame "Ham Hamod HFR".
iSplit.
- iApply (auth_fuel_is_proper with "Haf"). unfold fuel_apply.
rewrite -leibniz_equiv_iff. intros Ï. rewrite !map_lookup_imap.
@@ -907,10 +1007,10 @@ Section model_state_lemmas.
+ rewrite option_guard_False //=.
rewrite -> not_elem_of_union in Hin. destruct Hin as [Hin ?].
rewrite -> not_elem_of_dom in Hin. rewrite Hin //.
- - iPureIntro. split; last first.
+ - iPureIntro. split; first last; [split|].
{ intros ζ' Hζ'. rewrite lookup_insert_ne; last first.
{ pose proof (locales_of_list_step_incl _ _ _ _ _ Hstep).
- clear Hfueldom Hmappingdom.
+ clear Hfueldom Hsamedoms.
assert (ζ' ∉ locales_of_list tp1); first by set_solver.
intros contra. simplify_eq.
destruct Htlen as [tp1' [-> Hlen]].
@@ -930,7 +1030,7 @@ Section model_state_lemmas.
rewrite lookup_insert_ne; last first.
{ intros <-. rewrite Hsmall in Hmapping; [congruence | set_solver]. }
apply Hsmall; set_solver. }
-
+ { rewrite map_imap_dom_eq // => Ï f Hin. by destruct (decide (Ï âˆˆ R1 ∪ R2)). }
intros Ï Î¶'. rewrite map_lookup_imap.
destruct (decide (Ï âˆˆ dom (ls_mapping δ1))) as [Hin|Hin].
+ apply elem_of_dom in Hin as [ζ'' HÏ]. rewrite HÏ. simpl.
@@ -971,7 +1071,7 @@ Section model_state_lemmas.
{ eapply Hminv. eexists _. split; eauto. }
congruence.
+ apply not_elem_of_dom in Hin. rewrite Hin /=. split; first done.
- intros (?&Hin'&?). rewrite ls_fuel_dom -ls_mapping_dom in Hdomincl.
+ intros (?&Hin'&?). rewrite -ls_same_doms in Hdomincl.
apply not_elem_of_dom in Hin.
destruct (decide (ζ' = locale_of tp1 efork)).
{ simplify_eq. rewrite lookup_insert in Hin'. simplify_eq. set_solver. }
@@ -983,14 +1083,39 @@ Section model_state_lemmas.
{ eapply Hminv. eauto. }
apply not_elem_of_dom in Hin. congruence. }
iSplit; first done.
- iSplit; [iSplit|].
+ iSplit; last first.
+ { iPureIntro. intros Ï Î¶'. simpl. rewrite map_lookup_imap.
+ destruct (ls_mapping δ1 !!Ï) eqn:Heq; last done. simpl.
+ destruct (decide (Ï âˆˆ R2)); first (intros ?; simplify_eq).
+ - destruct Htlen as [tp1' [-> Hlen]].
+ inversion Hstep as [? ? e1 ? e2 ? efs t1 t2 Hf1 YY Hprimstep |]. simplify_eq.
+ assert (efs = [efork]) as ->.
+ { symmetry. assert (length tp1' = length (t1 ++ e2 :: t2)).
+ rewrite app_length //=; rewrite app_length //= in Hlen.
+ clear Hlen. eapply app_inj_1 =>//. by list_simplifier. }
+ assert (is_Some (from_locale (t1 ++ e1 :: t2 ++ [efork]) (locale_of (t1 ++ e1 :: t2) efork))).
+ + unfold from_locale. erewrite from_locale_from_Some; eauto.
+ apply prefixes_from_spec. list_simplifier. eexists _, []. split=>//.
+ by list_simplifier.
+ + eapply from_locale_from_equiv =>//; [constructor |]. rewrite H1.
+ replace (t1 ++ e1 :: t2 ++ [efork]) with ((t1 ++ e1 :: t2) ++ [efork]);
+ last by list_simplifier.
+ replace (t1 ++ e2 :: t2 ++ [efork]) with ((t1 ++ e2 :: t2) ++ [efork]);
+ last by list_simplifier.
+ assert (locales_equiv (t1 ++ e1 :: t2) (t1 ++ e2 :: t2)).
+ { apply locales_equiv_middle. eapply locale_step_preserve =>//. }
+ apply locales_equiv_from_app =>//. by eapply locales_from_equiv_refl.
+ - intros ?; simplify_eq.
+ assert (is_Some (from_locale tp1 ζ')) by eauto.
+ eapply from_locale_step =>//. }
+ iSplit.
{ iPureIntro. destruct (map_choose _ Hnemp) as [Ï[??]]. exists Ï.
apply Hminv. eexists _. split; eauto. apply elem_of_dom. eauto. }
iSplit.
- { iPureIntro. intros Ï Hlive Hmd. simpl. inversion Hmd; simplify_eq.
+ { iPureIntro. intros Ï Hlive Hlive' Hmd. simpl. inversion Hmd; simplify_eq.
- rewrite map_lookup_imap.
assert (Hin: Ï âˆˆ dom (ls_fuel δ1)).
- { rewrite ls_fuel_dom -ls_mapping_dom elem_of_dom. eauto. }
+ { rewrite -ls_same_doms elem_of_dom. eauto. }
apply elem_of_dom in Hin. destruct Hin as [f' Hin'].
rewrite Hin' /=.
destruct (decide (Ï âˆˆ R1 ∪ R2)) as [Hin''|Hin''].
@@ -1008,257 +1133,309 @@ Section model_state_lemmas.
rewrite Hfuels; last set_solver. rewrite lookup_fmap.
assert (Hindom: Ï âˆˆ dom fs); first by set_solver.
apply elem_of_dom in Hindom as [f Hindom]. rewrite Hindom /= decide_True /=; [lia|set_solver]. }
- iSplit; last done.
- { iPureIntro. intros Ï' HÏ' _. simpl.
- rewrite map_lookup_imap. rewrite <-ls_fuel_dom, elem_of_dom in HÏ'.
+ iSplit.
+ { iPureIntro. intros Ï' HÏ' _. simpl. left.
+ rewrite map_lookup_imap. rewrite elem_of_dom in HÏ'.
destruct HÏ' as [f Hf]. rewrite Hf /=. destruct (decide ((Ï' ∈ R1 ∪ R2))); simpl; lia. }
- iPureIntro. intros Ï Î¶'. simpl. rewrite map_lookup_imap.
- destruct (ls_mapping δ1 !!Ï) eqn:Heq; last done. simpl.
- destruct (decide (Ï âˆˆ R2)); first (intros ?; simplify_eq).
- - destruct Htlen as [tp1' [-> Hlen]].
- inversion Hstep as [? ? e1 ? e2 ? efs t1 t2 Hf1 YY Hprimstep |]. simplify_eq.
- assert (efs = [efork]) as ->.
- { symmetry. assert (length tp1' = length (t1 ++ e2 :: t2)).
- rewrite app_length //=; rewrite app_length //= in Hlen.
- clear Hlen. eapply app_inj_1 =>//. by list_simplifier. }
- assert (is_Some (from_locale (t1 ++ e1 :: t2 ++ [efork]) (locale_of (t1 ++ e1 :: t2) efork))).
- + unfold from_locale. erewrite from_locale_from_Some; eauto.
- apply prefixes_from_spec. list_simplifier. eexists _, []. split=>//.
- by list_simplifier.
- + eapply from_locale_from_equiv =>//; [constructor |]. rewrite H1.
- replace (t1 ++ e1 :: t2 ++ [efork]) with ((t1 ++ e1 :: t2) ++ [efork]);
- last by list_simplifier.
- replace (t1 ++ e2 :: t2 ++ [efork]) with ((t1 ++ e2 :: t2) ++ [efork]);
- last by list_simplifier.
- assert (locales_equiv (t1 ++ e1 :: t2) (t1 ++ e2 :: t2)).
- { apply locales_equiv_middle. eapply locale_step_preserve =>//. }
- apply locales_equiv_from_app =>//. by eapply locales_from_equiv_refl.
- - intros ?; simplify_eq.
- assert (is_Some (from_locale tp1 ζ')) by eauto.
- eapply from_locale_step =>//.
+ iSplit; [simpl| done]. rewrite map_imap_dom_eq //.
+ by intros Ï??; destruct (decide (Ï âˆˆ R1 ∪ R2)).
Qed.
Definition valid_new_fuelmap (fs1 fs2: gmap (fmrole Mdl) nat) (s1 s2: Mdl) (Ï: fmrole Mdl) :=
(Ï âˆˆ live_roles _ s2 -> oleq (fs2 !! Ï) (Some (fuel_limit s2))) ∧
+ (Ï âˆ‰ live_roles _ s2 -> Ï âˆˆ dom fs1 ∩ dom fs2 -> oless (fs2 !! Ï) (fs1 !! Ï)) ∧
Ï âˆˆ dom fs1 ∧
- (forall Ï', Ï' ∈ dom fs2 ∖ live_roles _ s1 -> oleq (fs2 !! Ï') (Some $ fuel_limit s2)) ∧
+ (forall Ï', Ï' ∈ dom fs2 ∖ dom fs1 -> oleq (fs2 !! Ï') (Some $ fuel_limit s2)) ∧
(forall Ï', Ï â‰ Ï' -> Ï' ∈ dom fs1 ∩ dom fs2 -> oless (fs2 !! Ï') (fs1 !! Ï')) ∧
- dom fs2 = (dom fs1 ∩ live_roles _ s2) ∪ (live_roles _ s2 ∖ live_roles _ s1).
+ (dom fs1 ∖ {[ Ï ]}) ∪ (live_roles _ s2 ∖ live_roles _ s1) ⊆ dom fs2 ∧
+ dom fs2 ⊆
+ (* new roles *) (live_roles _ s2 ∖ live_roles _ s1) ∪
+ (* surviving roles *) (live_roles _ s2 ∩ live_roles _ s1 ∩ dom fs1) ∪
+ (* already dead *) (dom fs1 ∖ live_roles _ s1) ∪
+ (* new deads *) ((live_roles _ s1 ∖ live_roles _ s2) ∩ dom fs1).
+
+ Ltac by_contradiction :=
+ match goal with
+ | |- ?goal => destruct_decide (decide (goal)); first done; exfalso
+ end.
Lemma update_step_still_alive
(extr : execution_trace Λ)
(auxtr: auxiliary_trace (fair_model Mdl))
- tp1 tp2 σ1 σ2 s1 s2 fs1 fs2 Ï (δ1 : fair_model Mdl) ζ:
+ tp1 tp2 σ1 σ2 s1 s2 fs1 fs2 Ï (δ1 : fair_model Mdl) ζ fr1:
+ (live_roles _ s2 ∖ live_roles _ s1) ⊆ fr1 ->
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 ζ fs1 -∗ frag_model_is s1 -∗ model_state_interp tp1 δ1
+ has_fuels ζ fs1 -∗ frag_model_is s1 -∗ model_state_interp tp1 δ1 -∗
+ frag_free_roles_are fr1
==∗ ∃ (δ2: fair_model Mdl) ℓ,
⌜labels_match (Some ζ) ℓ
∧ valid_state_evolution_fairness (extr :tr[Some ζ]: (tp2, σ2)) (auxtr :tr[â„“]: δ2)âŒ
- ∗ has_fuels ζ fs2 ∗ frag_model_is s2 ∗ model_state_interp tp2 δ2.
+ ∗ has_fuels ζ fs2 ∗ frag_model_is s2 ∗ model_state_interp tp2 δ2 ∗
+ frag_free_roles_are (fr1 ∖ (live_roles _ s2 ∖ live_roles _ s1)).
Proof.
- iIntros (Htrlast Hauxtrlast Hstep Htrans Hfuelsval) "Hfuel Hmod Hsi".
+ iIntros (Hfr_new Htrlast Hauxtrlast Hstep Htrans Hfuelsval) "Hfuel Hmod Hsi Hfr1".
assert (Hfsne: fs1 ≠∅).
- { destruct Hfuelsval as (_&?&_). intros ->. set_solver. }
+ { destruct Hfuelsval as (_&_&?&_). intros ->. set_solver. }
iDestruct (has_fuel_in with "Hfuel Hsi") as "%Hxdom"; 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 "Hsi" as "(%M&%FR&Hafuel&Hamapping&HFR&%Hinv&%Hsmall&Hamod&%HFR)".
iDestruct (model_agree with "Hamod Hmod") as "%Heq".
- assert (Hfueldom: dom (update_fuel_resource δ1 fs2 s2) = live_roles Mdl s2).
+ iDestruct (free_roles_inclusion with "HFR Hfr1") as %HfrFR.
+
+ assert (Hsamedoms:
+ dom (map_imap
+ (λ Ï' _, if decide (Ï' ∈ dom $ ls_fuel δ1) then ls_mapping δ1 !! Ï' else Some ζ)
+ (gset_to_gmap 333 ((dom (ls_fuel δ1) ∪ dom fs2) ∖ (dom fs1 ∖ dom fs2)))) =
+ dom (update_fuel_resource δ1 fs1 fs2 s2)).
{ unfold update_fuel_resource, fuel_apply. rewrite -leibniz_equiv_iff.
intros Ï'; split.
- - intros [f Hin]%elem_of_dom. rewrite map_lookup_imap in Hin.
- destruct (decide (Ï' ∈ live_roles _ s2)); first done.
- rewrite lookup_gset_to_gmap option_guard_False // in Hin.
- intros Hin. destruct (decide (Ï' ∈ dom fs2)) as [[f Hin1]%elem_of_dom|Hin1].
+ apply elem_of_dom. eexists f. rewrite map_lookup_imap lookup_gset_to_gmap option_guard_True //=.
rewrite decide_True //. apply elem_of_dom. rewrite Hin1; eauto.
- + apply elem_of_dom. rewrite map_lookup_imap lookup_gset_to_gmap option_guard_True //=.
- rewrite decide_False //. apply elem_of_dom. rewrite ls_fuel_dom.
- destruct Hfuelsval as (?&?&?&?&Hdomeq). rewrite Hdomeq in Hin1. set_solver. }
-
- assert (Hmappingdom: dom (map_imap
- (λ Ï' _, if decide (Ï' ∈ live_roles Mdl δ1) then ls_mapping δ1 !! Ï' else Some ζ)
- (gset_to_gmap 333 (live_roles Mdl s2))) = live_roles Mdl s2).
- { rewrite -leibniz_equiv_iff. intros Ï'; split.
+ rewrite map_imap_dom_eq dom_gset_to_gmap in Hin; first set_solver.
+ intros Ï0??. destruct (decide (Ï0 ∈ dom $ ls_fuel δ1)); [|done].
+ apply elem_of_dom. rewrite ls_same_doms. SS.
+ + rewrite map_imap_dom_eq dom_gset_to_gmap; last first.
+ { intros Ï0 ? Hin0. destruct (decide (Ï0 ∈ dom fs2)) as [|Hnotin]; apply elem_of_dom; first done.
+ unfold valid_new_fuelmap in Hfuelsval.
+ destruct Hfuelsval as (_&_&_&_& Hdomfs2). set_solver. }
+
+ rewrite map_imap_dom_eq dom_gset_to_gmap in Hin; first set_solver.
+ intros Ï0??. destruct (decide (Ï0 ∈ dom $ ls_fuel δ1)); [|done].
+ apply elem_of_dom. rewrite ls_same_doms. SS.
- intros [f Hin]%elem_of_dom. rewrite map_lookup_imap in Hin.
- destruct (decide (Ï' ∈ live_roles _ s2)); first done.
- rewrite lookup_gset_to_gmap option_guard_False // in Hin.
- - intros Hin. destruct (decide (Ï' ∈ live_roles _ δ1)) as [Hin1|Hin1].
- + apply elem_of_dom. rewrite map_lookup_imap lookup_gset_to_gmap option_guard_True //=.
- rewrite decide_True //. apply elem_of_dom. rewrite ls_mapping_dom //.
- + apply elem_of_dom. rewrite map_lookup_imap lookup_gset_to_gmap option_guard_True //=.
- rewrite decide_False //. }
+ rewrite map_imap_dom_eq dom_gset_to_gmap.
+ + by_contradiction. rewrite lookup_gset_to_gmap option_guard_False // in Hin.
+ + intros Ï0??. destruct (decide (Ï0 ∈ dom $ ls_fuel δ1)); [|done].
+ apply elem_of_dom. rewrite ls_same_doms. SS. }
+
+ assert (Hnewdom: dom (update_fuel_resource δ1 fs1 fs2 s2) =
+ (dom (ls_fuel δ1) ∪ dom fs2) ∖ (dom fs1 ∖ dom fs2)).
+ { unfold update_fuel_resource, fuel_apply. rewrite map_imap_dom_eq ?dom_gset_to_gmap //.
+ intros Ï' _ Hin. destruct (decide (Ï' ∈ dom fs2)); apply elem_of_dom =>//. set_solver. }
+
+ assert (Hfueldom: live_roles _ s2 ⊆ dom $ update_fuel_resource δ1 fs1 fs2 s2).
+ { rewrite -Hsamedoms map_imap_dom_eq dom_gset_to_gmap //.
+ { epose proof ls_fuel_dom. intros Ï' Hin.
+ destruct Hfuelsval as (?&?&?&?&?&?).
+ destruct (decide (Ï' ∈ live_roles _ δ1)).
+ - apply elem_of_difference; split; [set_solver|].
+ intros [? Habs]%elem_of_difference.
+ destruct (decide (Ï' = Ï)).
+ + simplify_eq. apply not_elem_of_dom in Habs.
+ rewrite -> Habs in *. simpl in *. eauto.
+ + apply Habs. assert (Ï' ∈ dom fs1 ∖ {[Ï]}); set_solver.
+ - apply elem_of_difference; split; [apply elem_of_union; right; set_solver|set_solver]. }
+ intros Ï0??. destruct (decide (Ï0 ∈ dom $ ls_fuel δ1)); [|done].
+ apply elem_of_dom. rewrite ls_same_doms. SS. }
iExists {|
ls_under := s2;
- ls_fuel := update_fuel_resource δ1 fs2 s2;
+ ls_fuel := _;
ls_fuel_dom := Hfueldom;
- ls_mapping := map_imap
- (λ Ï' fold, if decide (Ï' ∈ live_roles _ δ1)
- then δ1.(ls_mapping) !! Ï'
- else Some ζ)
- (gset_to_gmap 333 (live_roles _ s2));
- ls_mapping_dom := Hmappingdom;
+ ls_mapping := _;
+ ls_same_doms := Hsamedoms;
|}, (Take_step Ï Î¶).
Unshelve.
iMod (update_has_fuels _ fs1 fs2 with "Hfuel Hafuel Hamapping") as "(Hafuel & Hfuel & Hmapping)".
{ set_solver. }
{ unfold valid_new_fuelmap in Hfuelsval.
- destruct Hfuelsval as (_&_&?&?&->). rewrite !Heq.
- rewrite ls_fuel_dom. set_solver. }
+ destruct Hfuelsval as (_&_&?&?& Hfs2_inf&Hfs2_sup).
+
+ apply elem_of_equiv_empty_L => Ï0 Hin.
+ apply elem_of_intersection in Hin as [Hin1 Hin2].
+ apply elem_of_difference in Hin1 as [Hin11 Hin12].
+
+ assert (Ï0 ∈ live_roles _ s2 ∖ live_roles _ s1) by set_solver.
+ assert (Ï0 ∈ fr1) by set_solver.
+ assert (Ï0 ∈ FR) by set_solver.
+ assert (Ï0 ∉ dom (ls_fuel δ1)) by set_solver.
+ done. }
iMod (update_model s2 with "Hamod Hmod") as "[Hamod Hmod]".
+ iMod (update_free_roles (live_roles Mdl s2 ∖ live_roles Mdl s1)
+ with "HFR Hfr1") as "[HFR Hfr2]"; [set_solver|].
iModIntro. iSplit.
{ iSplit; first done. iPureIntro.
- destruct Hfuelsval as (Hlim&Hinfs1m&Hnewlim&Hdec&Hdomeq).
+ destruct Hfuelsval as (Hlim&Hzombie&Hinfs1m&Hnewlim&Hdec&Hinf&Hsup).
constructor =>//; split.
- constructor; simpl; first by rewrite Hauxtrlast Heq //.
split; first by rewrite Hauxtrlast; apply Hxdom; set_solver.
split.
- { intros ?? Hmd. inversion Hmd; clear Hmd; simplify_eq.
+ { intros ??? Hmd. inversion Hmd; clear Hmd; simplify_eq.
+ symmetry in Hsametid. rewrite -> Hxdom in Hsametid. simpl.
unfold update_fuel_resource, fuel_apply.
rewrite map_lookup_imap lookup_gset_to_gmap.
- destruct (decide (Ï' ∈ live_roles Mdl s2)) as [Hin|Hin].
+ destruct (decide (Ï' ∈ live_roles Mdl s2 ∪ dom fs2)) as [Hin|Hin].
* rewrite option_guard_True //=.
{ destruct (decide (Ï' ∈ dom fs2)) as [Hin2|Hin2].
** rewrite Hfuel; last set_solver. apply Hdec; [congruence|set_solver].
** exfalso. set_solver. }
+ apply elem_of_difference; split; [set_solver|].
+ apply not_elem_of_difference; right.
+ apply elem_of_union in Hin as [|]; [|done].
+ destruct (decide (Ï' = Ï)); simplify_eq.
+ apply Hinf; set_solver.
* rewrite option_guard_False //=.
- eapply Hin, fm_live_preserved; [done| | congruence].
- rewrite <-Hxdom in Hsametid. rewrite -ls_mapping_dom elem_of_dom. by eauto.
+ ** assert (Ï' ∈ dom fs2); set_solver.
+ ** apply not_elem_of_difference; right; set_solver.
+ simpl in *. unfold update_fuel_resource, fuel_apply.
rewrite map_lookup_imap lookup_gset_to_gmap.
- destruct (decide (Ï' ∈ live_roles Mdl s2)) as [Hin|Hin].
- * rewrite option_guard_True //=.
- { destruct (decide (Ï' ∈ dom fs2)) as [Hin2|Hin2].
- ** rewrite Hfuel; last set_solver.
- rewrite Hdomeq in Hin2. exfalso.
- assert (Hin3: Ï' ∈ dom fs1).
- { set_solver. }
- rewrite map_lookup_imap in Hneqtid.
- rewrite <-Hxdom in Hin3.
- rewrite Hin3 /= in Hneqtid.
- rewrite lookup_gset_to_gmap option_guard_True //= in Hneqtid.
- rewrite decide_True // in Hneqtid.
- ** rewrite map_lookup_imap in Hneqtid.
- assert (is_Some (ls_mapping (trace_last auxtr) !! Ï')) as [ζ' Hζ'].
- { apply elem_of_dom. rewrite ls_mapping_dom //. }
- rewrite lookup_gset_to_gmap option_guard_True //= in Hneqtid.
- rewrite Hζ' /= decide_True // in Hneqtid. }
- * rewrite option_guard_False //=.
- rewrite map_lookup_imap in Hissome.
- assert (is_Some (ls_mapping (trace_last auxtr) !! Ï')) as [ζ' Hζ'].
- { apply elem_of_dom. rewrite ls_mapping_dom //. }
- rewrite lookup_gset_to_gmap option_guard_False //= in Hissome.
- by inversion Hissome. }
+
+ destruct (decide (Ï' ∈ (dom (ls_fuel (trace_last auxtr)) ∪ dom fs2) ∖ (dom fs1 ∖ dom fs2))) as [Hin|Hin].
+ * rewrite map_lookup_imap lookup_gset_to_gmap option_guard_True //= decide_True //= in Hneqtid.
+ * apply not_elem_of_difference in Hin as [?|Hin]; [set_solver|].
+ apply elem_of_difference in Hin as [??].
+ rewrite map_lookup_imap lookup_gset_to_gmap /= option_guard_False /= in Hissome;
+ [inversion Hissome; congruence|set_solver].
+ + simpl in *. rewrite Hfuel; last set_solver. unfold update_fuel_resource, fuel_apply.
+ rewrite Hnewdom in Hnotdead. rewrite map_lookup_imap lookup_gset_to_gmap option_guard_True //=.
+ assert (Ï' ∈ dom fs2) by set_solver.
+ rewrite decide_True; [apply Hzombie =>//; set_solver | done]. }
split.
+ intros ? Hin ?. simplify_eq; simpl.
unfold update_fuel_resource, fuel_apply.
rewrite map_lookup_imap lookup_gset_to_gmap.
- destruct (decide (Ï' ∈ live_roles _ s2)) as [Hlive|Hlive].
+ destruct (decide (Ï' ∈ (dom (ls_fuel (trace_last auxtr)) ∪ dom fs2) ∖ (dom fs1 ∖ dom fs2))) as [Hlive|Hlive].
* rewrite option_guard_True //=.
+ apply elem_of_difference in Hlive as [Hin1 Hnin].
+ apply not_elem_of_difference in Hnin.
+
destruct (decide (Ï' ∈ dom fs2)) as [Hin2|Hin2].
- ** rewrite Hfuel; last set_solver. apply oleq_oless, Hdec; [congruence|set_solver].
- ** rewrite <-ls_fuel_dom, elem_of_dom in Hin. destruct Hin as [? ->]. simpl;lia.
- * rewrite option_guard_False //=.
- eapply Hlive, fm_live_preserved =>//. congruence.
+ ** destruct (decide (Ï' ∈ live_roles _ (trace_last auxtr)));left.
+ *** destruct (decide (Ï' ∈ dom fs1)).
+ { rewrite Hfuel //. apply oleq_oless, Hdec; [congruence|set_solver]. }
+ { exfalso. set_solver. }
+ *** assert (Ï' ∉ live_roles _ s2).
+ { by_contradiction. assert (Ï' ∈ fr1); [eapply elem_of_subseteq; eauto; set_solver|].
+ assert (Ï' ∈ FR); [eapply elem_of_subseteq; eauto; set_solver|set_solver]. }
+ assert (Ï' ∈ dom fs1). set_solver.
+ rewrite Hfuel //. apply oleq_oless, Hdec; [congruence|set_solver].
+ ** left. rewrite elem_of_dom in Hin. destruct Hin as [? ->]. simpl;lia.
+ * right; split.
+ ** eapply not_elem_of_weaken; [|by apply map_imap_dom_inclusion; rewrite dom_gset_to_gmap].
+ rewrite dom_gset_to_gmap //.
+ ** apply not_elem_of_difference in Hlive as [?|Hlive]; [set_solver|].
+ apply elem_of_difference in Hlive as [? Habs].
+ exfalso. apply Habs. set_solver.
+ split.
{ intros Hlive. unfold update_fuel_resource, fuel_apply.
- rewrite map_lookup_imap lookup_gset_to_gmap option_guard_True //=.
- rewrite decide_True; [by apply Hlim | set_solver]. }
- intros ??. unfold update_fuel_resource, fuel_apply.
- rewrite map_lookup_imap lookup_gset_to_gmap option_guard_True //=; last set_solver.
- rewrite decide_True; first apply Hnewlim; set_solver.
+ destruct (decide (Ï âˆˆ (dom (ls_fuel (trace_last auxtr)) ∪ dom fs2) ∖ (dom fs1 ∖ dom fs2))) as [Hin|Hnin].
+ - rewrite map_lookup_imap lookup_gset_to_gmap option_guard_True //=; last set_solver.
+ rewrite decide_True; [by apply Hlim |set_solver].
+ - exfalso; apply not_elem_of_difference in Hnin as [Hnin|Hnin].
+ + assert (Ï âˆ‰ live_roles _ (trace_last auxtr)).
+ eapply not_elem_of_weaken => //.
+ { epose proof ls_fuel_dom. set_solver. }
+ assert (Ï âˆˆ dom fs2) by set_solver. set_solver.
+ + apply elem_of_difference in Hnin as [? Hnin].
+ apply not_elem_of_dom in Hnin. rewrite Hnin /= in Hlim.
+ by apply Hlim. }
+ split.
+ { intros Ï'. unfold update_fuel_resource, fuel_apply => Hin.
+ rewrite map_imap_dom_eq in Hin; last first.
+ { intros Ï0 _ Hin'. destruct (decide (Ï0 ∈ dom fs2)); [by apply elem_of_dom|].
+ rewrite dom_gset_to_gmap elem_of_difference in Hin'.
+ destruct Hin' as [Hin' ?]. apply elem_of_union in Hin' as [?|?]; [by apply elem_of_dom|done]. }
+ rewrite dom_gset_to_gmap in Hin. rewrite map_lookup_imap lookup_gset_to_gmap option_guard_True /=; last set_solver.
+ assert (Ï' ∈ dom fs2) by set_solver. rewrite decide_True //. apply Hnewlim. apply elem_of_difference; split =>//.
+ intros contra%Hxdom%elem_of_dom_2. rewrite ls_same_doms in contra. simplify_eq. set_solver. }
+ intros Ï0 Hin.
+ assert (Ï0 ∉ live_roles _ (trace_last auxtr)).
+ { eapply not_elem_of_weaken; last apply ls_fuel_dom. set_solver. }
+ apply elem_of_difference in Hin as [Hin1 Hnin].
+ assert (Ï0 ∈ live_roles _ s2).
+ { by_contradiction.
+ assert (Ï0 ∈ dom fs2).
+ { unfold update_fuel_resource, fuel_apply in Hin1.
+ eapply elem_of_subseteq in Hin1; last apply map_imap_dom_inclusion.
+ rewrite dom_gset_to_gmap in Hin1. set_solver. }
+ exfalso. assert (Hinabs: Ï0 ∈ dom fs1) by set_solver.
+ apply not_elem_of_dom in Hnin. rewrite Hauxtrlast Hfuel // in Hnin.
+ apply elem_of_dom in Hinabs. rewrite Hnin in Hinabs. simpl in Hinabs.
+ by inversion Hinabs. }
+ set_solver.
- simplify_eq. unfold tids_smaller; simpl.
intros Ï' ? Hmim.
- rewrite map_lookup_imap in Hmim.
- destruct (decide (Ï' ∈ live_roles _ s2)).
- + rewrite lookup_gset_to_gmap option_guard_True //= in Hmim.
- destruct (ls_mapping (trace_last auxtr) !! Ï') eqn:Heq.
- * simpl in H. destruct (decide (Ï' ∈ live_roles _ (trace_last auxtr))) as [|Hnotin].
- ** rewrite decide_True // in Hmim.
- inversion Hstep; simplify_eq.
- eapply from_locale_step =>//. by eapply Hless.
- ** rewrite <- ls_mapping_dom in Hnotin. apply not_elem_of_dom in Hnotin. congruence.
- * simpl in H. destruct (decide (Ï' ∈ live_roles _ (trace_last auxtr))) as [|Hnotin].
- ** rewrite decide_True // in Hmim.
- inversion Hstep; simplify_eq. eapply from_locale_step =>//.
- by eapply Hless.
- ** rewrite decide_False // in Hmim. simplify_eq.
- inversion Hstep; simplify_eq. eapply from_locale_step =>//.
- eapply Hless. eapply Hxdom. set_solver.
- + rewrite lookup_gset_to_gmap option_guard_False //= in Hmim. }
-
- iFrame "Hfuel Hmod". iExists _. iFrame.
- iSplitL "Hafuel".
- { simpl. unfold update_fuel_resource.
- destruct Hfuelsval as (?&?&?&?&Hdomeq).
- iApply (own_proper with "Hafuel"). do 3 f_equiv.
- rewrite !ls_fuel_dom !Hdomeq !Heq.
- assert (live_roles _ s1 ∖ dom fs1 = live_roles _ s2 ∖ dom fs2).
- { rewrite Hdomeq -leibniz_equiv_iff.
- eapply set_subseteq_antisymm.
- - intros Ï' [Hin Hnotin]%elem_of_difference.
- apply elem_of_difference. split; last set_solver.
- eapply fm_live_preserved; eauto. set_solver.
- - intros Ï' [Hin Hnotin]%elem_of_difference. apply elem_of_difference.
- split; [set_solver | set_solver]. }
- rewrite -leibniz_equiv_iff.
- eapply set_subseteq_antisymm; first set_solver.
- intros Ï' Hin. apply elem_of_difference; split; [| set_solver].
- apply elem_of_union.
- destruct (decide (Ï' ∈ live_roles _ s1)); set_solver. }
- iPureIntro. split; last first.
- { intros ζ' ?. pose proof (locales_of_list_step_incl _ _ _ _ _ Hstep).
+ rewrite map_lookup_imap in Hmim. rewrite lookup_gset_to_gmap in Hmim.
+ destruct (decide (Ï' ∈ (dom (ls_fuel (trace_last auxtr)) ∪ dom fs2) ∖ (dom fs1 ∖ dom fs2)));
+ last by rewrite option_guard_False in Hmim.
+ rewrite option_guard_True //= in Hmim.
+ destruct (decide (Ï' ∈ dom (ls_fuel (trace_last auxtr)))).
+ + rewrite decide_True // in Hmim.
+ inversion Hstep; simplify_eq.
+ eapply from_locale_step =>//. by eapply Hless.
+ + rewrite decide_False // in Hmim. simplify_eq.
+ inversion Hstep; simplify_eq.
+ eapply from_locale_step =>//. unfold from_locale. rewrite from_locale_from_Some //.
+ apply prefixes_from_spec. exists t1, t2. by list_simplifier. }
+
+ iFrame "Hfuel Hmod Hfr2". iExists _, _. iFrame. all: eauto. (* TODO: find source... *)
+ iPureIntro; split.
+
+ { intros Ï' ζ'. simpl. rewrite map_lookup_imap.
+ rewrite lookup_gset_to_gmap //=.
+ destruct (decide (Ï' ∈ (dom (ls_fuel δ1) ∪ dom fs2) ∖ (dom fs1 ∖ dom fs2))) as [Hin|Hnotin].
+ - rewrite option_guard_True //=. destruct (decide (Ï' ∈ dom (ls_fuel δ1))).
+ + destruct (decide (ζ' = ζ)) as [->|Hneq].
+ * rewrite lookup_insert. split.
+ { eexists; split =>//. apply elem_of_difference in Hin as [? Hin].
+ apply not_elem_of_difference in Hin as [?|?]; [|done].
+ set_solver. }
+ { intros (?&?&?). simplify_eq. apply Hxdom.
+ destruct Hfuelsval as (?&?&?&?&?). by_contradiction.
+ assert (Ï' ∈ live_roles Mdl s2 ∖ live_roles Mdl (trace_last auxtr)) by set_solver.
+ assert (Ï' ∈ fr1) by set_solver.
+ assert (Ï' ∈ FR) by set_solver.
+ assert (Ï' ∉ dom $ ls_fuel (trace_last auxtr)) by set_solver.
+ done. }
+ * rewrite lookup_insert_ne //.
+ + split.
+ * intros Htid. simplify_eq. rewrite lookup_insert. eexists; split=>//.
+ set_solver.
+ * assert (Ï' ∈ dom fs2) by set_solver. intros Hm. by_contradiction.
+ rewrite lookup_insert_ne in Hm; last congruence.
+ rewrite -Hinv in Hm. apply elem_of_dom_2 in Hm. rewrite ls_same_doms // in Hm.
+ - destruct Hfuelsval as (?&?&?&?&Hinf&?). rewrite option_guard_False //=. split; first done.
+ destruct (decide (ζ' = ζ)) as [->|Hneq].
+ { rewrite lookup_insert //. intros (?&?&?). simplify_eq. set_solver. }
+ rewrite lookup_insert_ne //.
+ rewrite -Hinv. intros Habs.
+
+ apply not_elem_of_difference in Hnotin as [Hnin|Hin].
+ + apply elem_of_dom_2 in Habs. rewrite ls_same_doms in Habs. set_solver.
+ + apply elem_of_difference in Hin as [Hin Hnin].
+ apply Hxdom in Hin. congruence. }
+ split.
+ { intros ζ' ?. pose proof (locales_of_list_step_incl _ _ _ _ _ Hstep). simpl.
rewrite lookup_insert_ne; first by apply Hsmall; set_solver.
- intros <-. destruct Hfuelsval as (_&Hfs1&_).
+ intros <-. destruct Hfuelsval as (_&_&Hfs1&_).
rewrite <-Hxdom in Hfs1. apply Hinv in Hfs1 as (?&HM&?).
rewrite Hsmall // in HM. set_solver. }
-
- intros Ï' ζ'. simpl. rewrite map_lookup_imap.
- destruct (decide (Ï' ∈ live_roles _ s2)) as [Hin|Hnotin].
- - rewrite lookup_gset_to_gmap option_guard_True //=.
- destruct (decide (Ï' ∈ live_roles _ δ1)) as [Hlive|Hlive].
- + destruct (decide (ζ = ζ')) as [<-|Hneq]; last by rewrite lookup_insert_ne //.
- rewrite lookup_insert. split.
- * rewrite Hinv. intros (ks&HM&Hks). eexists. split; first done.
- destruct Hfuelsval as (?&?&?&?&->). apply elem_of_union.
- left. apply elem_of_intersection. split; last done. apply Hxdom.
- apply Hinv. eexists; split; done.
- * intros (ks&HM&Hks). simplify_eq. apply Hxdom.
- destruct Hfuelsval as (?&?&?&?&Hdomeq). rewrite Hdomeq in Hks.
- set_solver.
- + split.
- * intros ?. simplify_eq. rewrite lookup_insert. eexists; split; first done.
- destruct Hfuelsval as (?&?&?&?&->). set_solver.
- * intros (ks&HM&Hks). simplify_eq.
- destruct Hfuelsval as (?&?&?&?&Hdomeq).
- assert (ζ = ζ'); last congruence.
- destruct (decide (ζ = ζ')) as [|Hneq]; first done. exfalso.
- rewrite lookup_insert_ne // in HM. unfold maps_inverse_match in Hinv.
- assert (ls_mapping (trace_last auxtr) !! Ï' = Some ζ').
- { apply Hinv. eexists; done. }
- rewrite -ls_mapping_dom in Hlive. apply not_elem_of_dom in Hlive. set_solver.
- - rewrite lookup_gset_to_gmap option_guard_False //=. split; first done.
- intros (ks & HM & Hks). exfalso.
- destruct (decide (ζ = ζ')) as [Heq'|Heq'].
- + subst ζ'. rewrite lookup_insert in HM. simplify_eq.
- destruct Hfuelsval as (_&_&_&_&Hdomeq). rewrite Hdomeq in Hks.
- set_solver.
- + rewrite lookup_insert_ne // in HM. unfold maps_inverse_match in Hinv.
- assert (ls_mapping δ1 !! Ï' = Some ζ').
- { apply Hinv. eexists _; eauto. }
- eapply Hnotin, fm_live_preserved; eauto.
- * rewrite -Heq -ls_mapping_dom. apply elem_of_dom. eauto.
- * intros <-. destruct Hfuelsval as (?&?&?&?&_). set_solver.
- Qed.
+ { simpl. rewrite /update_fuel_resource /fuel_apply.
+ rewrite map_imap_dom_eq ?dom_gset_to_gmap.
+ + apply elem_of_equiv_empty_L. intros Ï' [Hin1 Hin2]%elem_of_intersection.
+ apply elem_of_difference in Hin1 as [Hin11 Hin12].
+ apply not_elem_of_difference in Hin12.
+ apply elem_of_difference in Hin2 as [Hin21 Hin22].
+ apply not_elem_of_difference in Hin22.
+ assert (Ï' ∉ dom $ ls_fuel δ1) by set_solver.
+ assert (Ï' ∈ dom fs2) by set_solver.
+ destruct Hin12 as [Hin12|Hin12]; last by (epose proof ls_fuel_dom; set_solver).
+ destruct Hfuelsval as (?&?&?&?&?&?).
+ assert (Ï' ∉ dom fs1); last set_solver.
+ intros contra. pose proof (Hfuel _ contra) as Habs. apply elem_of_dom in contra as [? contra].
+ rewrite contra in Habs. apply elem_of_dom_2 in Habs. done.
+ + intros Ï' _ Hin. destruct (decide (Ï' ∈ dom fs2)) as [Hin'|].
+ * apply elem_of_dom in Hin' as [? ->]. done.
+ * assert (Ï' ∈ dom (ls_fuel δ1)) as Hin' by set_solver. apply elem_of_dom in Hin' as [? ->]. done. }
+Qed.
End model_state_lemmas.
diff --git a/trillium/prelude/finitary.v b/trillium/prelude/finitary.v
index 47696da..76196ae 100644
--- a/trillium/prelude/finitary.v
+++ b/trillium/prelude/finitary.v
@@ -573,3 +573,58 @@ Section finite_range_gmap.
Qed.
End finite_range_gmap.
+
+
+Section enumerate_gsets.
+ Context {A : Type}.
+ Context `{!EqDecision A, !Countable A}.
+
+ Fixpoint enumerate_dom_gsets (D: list A) : list (gset A) :=
+ match D with
+ | [] => [ ∅ ]
+ | k::ks =>
+ s_wo ↠enumerate_dom_gsets ks;
+ b ↠[ true; false];
+ if (b : bool) then mret s_wo else mret $ {[ k ]} ∪ s_wo
+ end.
+
+ Definition enumerate_dom_gsets' (D: gset A) : list (gset A) :=
+ enumerate_dom_gsets (elements D).
+
+ Local Instance all_the_range_instances' B (P: B -> Prop) : ∀ x, Decision (P x).
+ Proof. intros ?; apply make_decision. Qed.
+
+ Lemma enumerate_gsets_spec D l m :
+ elements D ≡ₚ l ∧ m ⊆ D → m ∈ enumerate_dom_gsets l.
+ Proof.
+ revert l D m.
+ induction l; intros D m.
+
+ { simpl. intros (Hel&Hl). eapply list.Permutation_nil_r in Hel. apply elements_empty_inv in Hel.
+ rewrite leibniz_equiv_iff in Hel. rewrite Hel in *. assert (m = ∅); set_solver. }
+ simpl. intros (Hel & Hl).
+
+ assert (Hdecomp: ∃ m1 m2, m = m1 ∪ m2 ∧ m1 ⊆ {[a]} ∧ m2 ⊆ list_to_set l).
+ { assert (list_to_set (elements D) = (list_to_set (a :: l): gset _)).
+ { by rewrite Hel. }
+ rewrite list_to_set_elements_L in H. simpl in H. exists (m ∩ {[a]}), (m ∩ list_to_set l).
+ split; last split; [set_solver|set_solver|set_solver]. }
+
+ destruct Hdecomp as (m1&m2&Hunion&Hdom1&Hdom2). rewrite Hunion in *.
+ assert (Hanotin: a ∉ m2).
+ { intros contra. eapply elem_of_subseteq in contra; eauto. rewrite elem_of_list_to_set in contra.
+ assert (a ∉ l); last done. apply NoDup_cons_1_1. rewrite <-Hel. apply NoDup_elements. }
+ apply elem_of_list_bind. exists m2; split; last first.
+ - apply (IHl (list_to_set l)). split; last set_solver. apply elements_list_to_set.
+ eapply (NoDup_cons_1_2 a). rewrite <-Hel. apply NoDup_elements.
+ - destruct (decide (a ∈ m1)).
+ + assert (m1 = {[a]}) by set_solver. simplify_eq. set_solver.
+ + assert (m1 = ∅) by set_solver. simplify_eq. rewrite union_empty_l_L. set_solver.
+ Qed.
+
+ Lemma enumerate_dom_gsets'_spec D s:
+ s ⊆ D → s ∈ enumerate_dom_gsets' D.
+ Proof.
+ intros H. unfold enumerate_dom_gsets'. eapply (enumerate_gsets_spec D). split; set_solver.
+ Qed.
+End enumerate_gsets.
diff --git a/trillium/program_logic/adequacy.v b/trillium/program_logic/adequacy.v
index 13f01b6..502493c 100644
--- a/trillium/program_logic/adequacy.v
+++ b/trillium/program_logic/adequacy.v
@@ -291,6 +291,128 @@ Section locales_helpers.
End locales_helpers.
+Section from_locale.
+ Context {Λ: language}.
+ Context `{ EqDecision (locale Λ)}.
+
+ Fixpoint from_locale_from tp0 tp ζ :=
+ match tp with
+ | [] => None
+ | e::tp' => if decide (locale_of tp0 e = ζ) then Some e else from_locale_from (tp0 ++ [e]) tp' ζ
+ end.
+
+ Definition from_locale tp ζ := from_locale_from [] tp ζ.
+
+ (* Other possibility is:
+ Definition from_locale tp ζ := list_find (λ '(tp, e), locale_of tp e = ζ) (prefixes tp).*)
+
+ Lemma from_locale_from_Some_app tp0 tp tp' ζ e :
+ from_locale_from tp0 tp ζ = Some e ->
+ from_locale_from tp0 (tp ++ tp') ζ = Some e.
+ Proof.
+ revert tp0 tp'. induction tp as [|e' tp IH]; first by list_simplifier.
+ simpl. intros tp0 tp' Hfl.
+ destruct (decide (locale_of tp0 e' = ζ)) =>//.
+ apply IH =>//.
+ Qed.
+
+ Lemma from_locale_from_is_Some_app tp0 tp tp' ζ :
+ is_Some (from_locale_from tp0 tp ζ) ->
+ is_Some (from_locale_from tp0 (tp ++ tp') ζ).
+ Proof.
+ intros [? HS]. eapply from_locale_from_Some_app in HS. eauto.
+ Qed.
+
+ Lemma from_locale_from_equiv tp0 tp0' tp tp' ζ :
+ locales_equiv tp0 tp0' ->
+ locales_equiv_from tp0 tp0' tp tp' ->
+ is_Some (from_locale_from tp0 tp ζ) ->
+ is_Some (from_locale_from tp0' tp' ζ).
+ Proof.
+ revert tp0 tp0' tp'. induction tp as [|e tp IH]; intros tp0 tp0' tp' Heq0 Heq [eζ Heζ];
+ destruct tp' as [|e' tp']; try by apply Forall2_length in Heq.
+ simpl in *.
+ destruct (decide (locale_of tp0 e' = ζ)).
+ - rewrite decide_True //; eauto. erewrite <-locale_equiv =>//.
+ - rewrite decide_False; last by erewrite <-locale_equiv.
+ apply Forall2_cons_1 in Heq as [Hlocs ?].
+ rewrite decide_False // in Heζ; last by erewrite Hlocs, <-locale_equiv =>//.
+ apply (IH (tp0 ++ [e])); eauto.
+ apply locales_equiv_snoc =>//. constructor.
+ Qed.
+
+ Lemma from_locale_step tp1 tp2 ζ oζ σ1 σ2 :
+ locale_step (tp1, σ1) oζ (tp2, σ2) →
+ is_Some(from_locale tp1 ζ) →
+ is_Some(from_locale tp2 ζ).
+ Proof.
+ intros Hstep. inversion Hstep; simplify_eq=>//.
+ intros HiS. replace (t1 ++ e2 :: t2 ++ efs) with ((t1 ++ e2 :: t2) ++ efs);
+ last by list_simplifier.
+ apply from_locale_from_is_Some_app.
+ eapply from_locale_from_equiv; eauto; [constructor|].
+ apply locales_equiv_from_middle. list_simplifier. by eapply locale_step_preserve.
+ Qed.
+
+ Lemma from_locale_from_Some tp0 tp1 tp e :
+ (tp, e) ∈ prefixes_from tp0 tp1 →
+ from_locale_from tp0 tp1 (locale_of tp e) = Some e.
+ Proof.
+ revert tp0 tp e; induction tp1 as [| e1 tp1 IH]; intros tp0 tp e Hin; first set_solver.
+ apply elem_of_cons in Hin as [Heq|Hin].
+ { simplify_eq. rewrite /= decide_True //. }
+ rewrite /= decide_False; first by apply IH.
+ fold (prefixes_from (A := expr Λ)) in Hin.
+ by eapply locale_injective.
+ Qed.
+
+End from_locale.
+
+Section locales_utils.
+ Context {Λ: language}.
+
+ Definition locales_of_list_from tp0 (tp: list $ expr Λ): list $ locale Λ :=
+ (λ '(t, e), locale_of t e) <$> (prefixes_from tp0 tp).
+ Notation locales_of_list tp := (locales_of_list_from [] tp).
+
+ Lemma locales_of_list_equiv tp0 tp0' tp1 tp2:
+ locales_equiv_from tp0 tp0' tp1 tp2 →
+ locales_of_list_from tp0 tp1 = locales_of_list_from tp0' tp2.
+ Proof.
+ revert tp0 tp0' tp1. induction tp2; intros tp0 tp0' tp1 H;
+ destruct tp1 as [|e1 tp1]; try by apply Forall2_length in H.
+ unfold locales_of_list_from. simpl.
+ simpl in H. apply Forall2_cons_1 in H as [??]. f_equal =>//.
+ apply IHtp2 =>//.
+ Qed.
+
+ Lemma locales_of_list_step_incl σ1 σ2 oζ tp1 tp2 :
+ locale_step (tp1, σ1) oζ (tp2, σ2) ->
+ locales_of_list tp1 ⊆ locales_of_list tp2.
+ Proof.
+ intros H. inversion H; simplify_eq=>//.
+ replace (t1 ++ e2 :: t2 ++ efs) with ((t1 ++ e2 :: t2) ++ efs); last by list_simplifier.
+ rewrite /locales_of_list_from. rewrite [in X in _ ⊆ X]prefixes_from_app /= fmap_app.
+ assert ((λ '(t, e), locale_of t e) <$> prefixes (t1 ++ e1 :: t2) = (λ '(t, e), locale_of t e) <$> prefixes (t1 ++ e2 :: t2))
+ as ->; last set_solver.
+ apply locales_of_list_equiv, locales_equiv_middle. by eapply locale_step_preserve.
+ Qed.
+
+ Lemma locales_of_list_from_locale_from `{EqDecision (locale Λ)} tp0 tp1 ζ:
+ is_Some (from_locale_from tp0 tp1 ζ) ->
+ ζ ∈ locales_of_list_from tp0 tp1.
+ Proof.
+ revert tp0; induction tp1 as [|e1 tp1 IH]; intros tp0.
+ { simpl. intros H. inversion H. congruence. }
+ simpl. intros [e Hsome]. rewrite /locales_of_list_from /=.
+ destruct (decide (locale_of tp0 e1 = ζ)); simplify_eq; first set_solver.
+ apply elem_of_cons; right. apply IH. eauto.
+ Qed.
+
+End locales_utils.
+Notation locales_of_list tp := (locales_of_list_from [] tp).
+
+
Section adequacy_helper_lemmas.
Context `{!irisG Λ M Σ}.
--
GitLab