Commit 8462798e authored by Glen Mével's avatar Glen Mével
Browse files

simply proof of zero_{TC,TR}: no need for the invariant

parent 72e838c7
......@@ -30,14 +30,14 @@ Definition TCTR_interface `{irisG heap_lang Σ, Tick}
(TRdup : nat iProp Σ)
: iProp Σ := (
n, Timeless (TC n)
(|={}=> TC 0%nat)
(|==> TC 0%nat)
m n, TC (m + n)%nat (TC m TC n)
n, Timeless (TR n)
n, Timeless (TRdup n)
n, Persistent (TRdup n)
( n, TR n ={}= TR n TRdup n)
(|={}=> TR 0%nat)
(* ∗ (|={⊤}=> TRdup 0%nat) *)
(|==> TR 0%nat)
(* ∗ (|==> TRdup 0%nat) *)
m n, TR (m + n)%nat (TR m TR n)
m n, TRdup (m `max` n)%nat (TRdup m TRdup n)
(* ∗ (TR max_tr ={⊤}=∗ False) *)
......@@ -103,6 +103,15 @@ Section Definitions.
Definition TC (n : nat) : iProp Σ :=
if useTC then own γ (nat n) else True%I.
(* Note: we can avoid the update modality by redefining TC like so:
Definition TC' n : iProp Σ := ⌜n = 0%nat⌝ ∨ TC n. *)
Lemma zero_TC :
|==> TC 0.
Proof using.
rewrite /TC ; destruct useTC.
- by apply own_unit.
- by iStartProof.
Qed.
Lemma TC_plus m n :
TC (m + n) (TC m TC n)%I.
Proof using.
......@@ -144,6 +153,11 @@ Section Definitions.
own γ2 (max_nat (MaxNat n)).
Arguments TRdup _%nat_scope.
(* Note: we can avoid the update modality by redefining TR like so:
Definition TR' n : iProp Σ := ⌜n = 0%nat⌝ ∨ TR n. *)
Lemma zero_TR :
|==> TR 0.
Proof using. apply own_unit. Qed.
Lemma TR_plus m n :
TR (m + n) (TR m TR n)%I.
Proof using. by rewrite /TR auth_frag_op own_op. Qed.
......@@ -170,6 +184,11 @@ Section Definitions.
Global Instance from_sep_TR_succ n : FromSep (TR (S n)) (TR 1) (TR n) | 100.
Proof using. by rewrite /FromSep [TR (S n)] TR_succ. Qed.
(* Note: we can avoid the update modality by redefining TRdup like so:
Definition TRdup' n : iProp Σ := ⌜n = 0%nat⌝ ∨ TRdup n. *)
Lemma zero_TRdup :
|==> TRdup 0.
Proof using. apply own_unit. Qed.
Lemma TRdup_max m n :
TRdup (m `max` n) (TRdup m TRdup n)%I.
Proof using. by rewrite /TRdup -own_op -auth_frag_op. Qed.
......@@ -204,37 +223,6 @@ Section Definitions.
own γ2 (max_nat (MaxNat (max_tr - 1 - m)))
)%I.
Lemma zero_TC E:
tctrN E
TCTR_invariant ={E}= TC 0.
Proof using.
rewrite /TC /TCTR_invariant ; destruct useTC ; last by auto.
iIntros (?) "#Htickinv".
iInv tctrN as (m) ">(? & ? & H● & ?)" "InvClose".
iDestruct (own_auth_nat_null with "H●") as "[H● $]".
iApply "InvClose" ; eauto with iFrame.
Qed.
Lemma zero_TR E:
tctrN E
TCTR_invariant ={E}= TR 0.
Proof using.
iIntros (?) "#Htickinv".
iInv tctrN as (m) "(>? & >? & ? & >Hγ1● & >?)" "InvClose".
iDestruct (own_auth_nat_null with "Hγ1●") as "[Hγ1● $]".
iApply "InvClose" ; eauto with iFrame.
Qed.
Lemma zero_TRdup E :
tctrN E
TCTR_invariant ={E}= TRdup 0.
Proof using.
iIntros (?) "#Htickinv".
iInv tctrN as (m) "(>? & >? & ? & >? & >Hγ2●)" "InvClose".
iDestruct (own_auth_max_nat_null with "Hγ2●") as "[Hγ2● $]".
iApply "InvClose" ; eauto with iFrame.
Qed.
Lemma TR_nmax_absurd (E : coPset) :
tctrN E
TCTR_invariant - TR max_tr ={E}= False.
......@@ -374,13 +362,13 @@ Section Definitions.
Proof using.
iIntros "#Hinv". repeat iSplitR.
- iPureIntro. by apply TC_timeless.
- by iApply (zero_TC with "Hinv").
- by iApply zero_TC.
- iPureIntro. by apply TC_plus.
- iPureIntro. by apply TR_timeless.
- iPureIntro. by apply TRdup_timeless.
- iPureIntro. by apply TRdup_persistent.
- iIntros (n). by iApply (TR_TRdup with "Hinv").
- by iApply (zero_TR with "Hinv").
- by iApply zero_TR.
- iPureIntro. by apply TR_plus.
- iPureIntro. by apply TRdup_max.
- by iApply (TRdup_nmax_absurd with "Hinv").
......@@ -433,7 +421,7 @@ Proof.
rewrite Nat.add_comm. iSpecialize ("HΔ3" with "[//]").
iDestruct (envs_simple_replace_singleton_sound with "HΔ3") as "[HTR' HΔ']"=>//=.
iCombine "HTR HTR'" as "HTR". iDestruct ("HΔ'" with "HTR") as "$".
- iMod (zero_TRdup with "Hinv") as "HTRdup"=>//.
- iMod zero_TRdup as "HTRdup".
iApply (tick_spec with "[//] [$HTC $HTRdup]")=>//. iIntros "!> [HTR _]". iApply HWP.
iDestruct (envs_simple_replace_singleton_sound with "HΔ2") as "[HTR' HΔ']"=>//=.
iCombine "HTR HTR'" as "HTR". iDestruct ("HΔ'" with "HTR") as "$".
......@@ -442,7 +430,7 @@ Proof.
iDestruct "HTRdup" as "#>HTRdup".
iApply (tick_spec with "[//] [$HTC $HTRdup]")=>//. iIntros "!> [_ #HTRdup']".
iApply HWP. rewrite Nat.add_comm. iDestruct ("HΔ'" with "[//]") as "$".
- iMod (zero_TRdup with "Hinv") as "HTRdup"=>//.
- iMod zero_TRdup as "HTRdup".
iApply (tick_spec with "[//] [$HTC $HTRdup]")=>//.
iIntros "!> [_ #HTRdup']". by iApply HWP.
Qed.
......
......@@ -92,7 +92,6 @@ Section Thunk.
{{{ (t : loc), RET #t ; Thunk p t nc φ }}}.
Proof.
iIntros "#Htickinv" (Φ) "!# [? Hf] Post".
iDestruct (zero_TC with "Htickinv") as ">Htc0".
iMod (auth_max_nat_alloc (MaxNat 0)) as (γ) "[Hγ● Hγ◯]".
iApply wp_fupd.
wp_tick_lam. wp_tick_inj. wp_tick_alloc t.
......
......@@ -28,7 +28,7 @@ Definition TC_interface `{!irisG heap_lang Σ, Tick}
(TC : nat iProp Σ)
: iProp Σ := (
n, Timeless (TC n)
(|={}=> TC 0%nat)
(|==> TC 0%nat)
m n, TC (m + n)%nat (TC m TC n)
( v, {{{ TC 1%nat }}} tick v {{{ RET v ; True }}})
)%I.
......@@ -77,6 +77,11 @@ Section TickSpec.
Definition TC (n : nat) : iProp Σ :=
own γ (nat n).
(* Note: we can avoid the update modality by redefining TC like so:
Definition TC' n : iProp Σ := ⌜n = 0%nat⌝ ∨ TC n. *)
Lemma zero_TC :
|==> TC 0.
Proof. apply own_unit. Qed.
Lemma TC_plus m n :
TC (m + n) (TC m TC n)%I.
Proof. by rewrite /TC auth_frag_op own_op. Qed.
......@@ -108,15 +113,6 @@ Section TickSpec.
Definition TC_invariant : iProp Σ :=
inv timeCreditN ( (m:nat), #m own γ (nat m))%I.
Lemma zero_TC :
TC_invariant ={}= TC 0.
Proof.
iIntros "#Htickinv".
iInv timeCreditN as (m) ">[Hcounter H●]" "Hclose".
iDestruct (own_auth_nat_null with "H●") as "[H● $]".
iApply "Hclose" ; eauto with iFrame.
Qed.
Theorem tick_spec s E (v : val) :
timeCreditN E
TC_invariant -
......@@ -177,7 +173,7 @@ Section TickSpec.
Proof.
iIntros "#Hinv". iSplit ; last iSplit ; last iSplit.
- iPureIntro. by apply TC_timeless.
- by iApply (zero_TC with "Hinv").
- by iApply zero_TC.
- iPureIntro. by apply TC_plus.
- iIntros (v). by iApply (tick_spec_simple with "Hinv").
Qed.
......
......@@ -31,8 +31,8 @@ Definition TR_interface `{irisG heap_lang Σ, Tick}
n, Timeless (TRdup n)
n, Persistent (TRdup n)
( n, TR n ={}= TR n TRdup n)
(|={}=> TR 0%nat)
(* ∗ (|={⊤}=> TRdup 0%nat) *)
(|==> TR 0%nat)
(* ∗ (|==> TRdup 0%nat) *)
m n, TR (m + n)%nat (TR m TR n)
m n, TRdup (m `max` n)%nat (TRdup m TRdup n)
(* ∗ (TR nmax ={⊤}=∗ False) *)
......@@ -88,6 +88,11 @@ Section TickSpec.
own γ2 (max_nat (MaxNat n)).
Arguments TRdup _%nat_scope.
(* Note: we can avoid the update modality by redefining TR like so:
Definition TR' n : iProp Σ := ⌜n = 0%nat⌝ ∨ TR n. *)
Lemma zero_TR :
|==> TR 0.
Proof. apply own_unit. Qed.
Lemma TR_plus m n :
TR (m + n) (TR m TR n)%I.
Proof. by rewrite /TR auth_frag_op own_op. Qed.
......@@ -112,6 +117,11 @@ Section TickSpec.
Global Instance from_sep_TR_succ n : FromSep (TR (S n)) (TR 1) (TR n).
Proof. by rewrite /FromSep [TR (S n)] TR_succ. Qed.
(* Note: we can avoid the update modality by redefining TRdup like so:
Definition TRdup' n : iProp Σ := ⌜n = 0%nat⌝ ∨ TRdup n. *)
Lemma zero_TRdup :
|==> TRdup 0.
Proof. apply own_unit. Qed.
Lemma TRdup_max m n :
TRdup (m `max` n) (TRdup m TRdup n)%I.
Proof. by rewrite /TRdup -own_op -auth_frag_op. Qed.
......@@ -137,26 +147,6 @@ Section TickSpec.
Definition TR_invariant : iProp Σ :=
inv timeReceiptN ( (n:nat), #(nmax-n-1) own γ1 (nat n) own γ2 (max_nat (MaxNat n)) (n < nmax)%nat)%I.
Lemma zero_TR E :
timeReceiptN E
TR_invariant ={E}= TR 0.
Proof.
iIntros (?) "#Htickinv".
iInv timeReceiptN as (m) ">(Hcounter & Hγ1● & H)" "Hclose".
iDestruct (own_auth_nat_null with "Hγ1●") as "[Hγ1● $]".
iApply "Hclose" ; eauto with iFrame.
Qed.
Lemma zero_TRdup E :
timeReceiptN E
TR_invariant ={E}= TRdup 0.
Proof.
iIntros (?) "#Htickinv".
iInv timeReceiptN as (m) ">(Hcounter & Hγ1● & Hγ2● & Im)" "Hclose".
iDestruct (own_auth_max_nat_null with "Hγ2●") as "[Hγ2● $]".
iApply "Hclose" ; eauto with iFrame.
Qed.
Lemma TR_nmax_absurd (E : coPset) :
timeReceiptN E
TR_invariant - TR nmax ={E}= False.
......@@ -283,7 +273,7 @@ Section TickSpec.
- iPureIntro. by apply TRdup_timeless.
- iPureIntro. by apply TRdup_persistent.
- iIntros (n). by iApply (TR_TRdup with "Hinv").
- by iApply (zero_TR with "Hinv").
- by iApply zero_TR.
- iPureIntro. by apply TR_plus.
- iPureIntro. by apply TRdup_max.
- by iApply (TRdup_nmax_absurd with "Hinv").
......@@ -410,7 +400,7 @@ Proof.
rewrite Nat.add_comm. iSpecialize ("HΔ2" with "[//]").
iDestruct (envs_simple_replace_singleton_sound with "HΔ2") as "[HTR' HΔ']"=>//=.
iCombine "HTR HTR'" as "HTR". iDestruct ("HΔ'" with "HTR") as "$".
- iMod (zero_TRdup with "Hinv") as "HTRdup"=>//.
- iMod zero_TRdup as "HTRdup".
iApply (tick_spec with "[//] HTRdup")=>//. iIntros "!> [HTR _]". iApply HWP.
iDestruct (envs_simple_replace_singleton_sound with "HΔ1") as "[HTR' HΔ']"=>//=.
iCombine "HTR HTR'" as "HTR". iDestruct ("HΔ'" with "HTR") as "$".
......@@ -419,7 +409,7 @@ Proof.
iDestruct "HTRdup" as "#>HTRdup".
iApply (tick_spec with "[//] HTRdup")=>//. iIntros "!> [_ #HTRdup']". iApply HWP.
rewrite Nat.add_comm. iDestruct ("HΔ'" with "[//]") as "$".
- iMod (zero_TRdup with "Hinv") as "HTRdup"=>//.
- iMod zero_TRdup as "HTRdup".
iApply (tick_spec with "[//] HTRdup")=>//. iIntros "!> [_ #HTRdup']". by iApply HWP.
Qed.
......
......@@ -731,7 +731,7 @@ Theorem make_spec : forall D R V v,
Proof using.
iIntros "* #?" (Φ) "!# [HF TC] HΦ".
wp_tick_rec. wp_tick_pair. wp_tick_inj.
iMod (zero_TR with "[//]") as "TR"=>//.
iMod zero_TR as "TR".
wp_tick. wp_alloc x as "Hx". iApply "HΦ".
iDestruct "HF" as (F K M HI HM) "(HM & TC' & TR')".
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment