Commit 170d93f5 authored by Glen Mével's avatar Glen Mével
Browse files

max_nat is Iris now: simplify Auth_max_nat and remove custom notation

parent 8462798e
From iris Require Export algebra.auth algebra.numbers.
From iris Require Import algebra.excl base_logic.lib.own proofmode.tactics.
Notation "'●max_nat' n" := (auth_auth (A:=max_natUR) (DfracOwn 1%Qp) n%nat) (at level 20).
Notation "'◯max_nat' n" := (auth_frag (A:=max_natUR) n%nat) (at level 20).
Local Coercion max_nat_car : max_nat >-> nat.
Section Auth_max_nat.
Context `{inG Σ (authR max_natUR)}.
Lemma auth_max_nat_alloc (n : max_nat) :
|==> γ, own γ (max_nat n) own γ (max_nat n).
Lemma auth_max_nat_alloc (n : nat) :
|==> γ, own γ ( MaxNat n) own γ ( MaxNat n).
Proof.
iMod (own_alloc (max_nat n max_nat n)) as (γ) "[? ?]".
iMod (own_alloc ( MaxNat n MaxNat n)) as (γ) "[? ?]".
- by apply auth_both_valid_2.
- by auto with iFrame.
Qed.
Global Arguments auth_max_nat_alloc _%nat.
Lemma own_auth_max_nat_le (γ : gname) (m n : max_nat) :
own γ (max_nat m) -
own γ (max_nat n) -
Lemma own_auth_max_nat_le (γ : gname) (m n : nat) :
own γ ( MaxNat m) -
own γ ( MaxNat n) -
(n m)%nat.
Proof.
iIntros "H● H◯".
iDestruct (own_valid_2 with "H● H◯") as % [[k ->] _] % auth_both_valid_discrete.
iPureIntro. apply Max.le_max_l.
iDestruct (own_valid_2 with "H● H◯") as % [?%max_nat_included _] % auth_both_valid_discrete.
iPureIntro. assumption.
Qed.
Lemma own_auth_max_nat_weaken (γ : gname) (n n : max_nat) :
Lemma own_auth_max_nat_weaken (γ : gname) (n n : nat) :
(n n)%nat
own γ (max_nat n) -
own γ (max_nat n).
own γ ( MaxNat n) -
own γ ( MaxNat n).
Proof.
iIntros (I) "H".
rewrite (_ : n = n n)%nat.
- rewrite auth_frag_op. iDestruct "H" as "[_$]".
- destruct n, n. rewrite max_nat_op. f_equal. simpl in I. lia.
rewrite (_ : n = n `max` n)%nat ; last lia.
rewrite -max_nat_op auth_frag_op. iDestruct "H" as "[_$]".
Qed.
Global Arguments own_auth_max_nat_weaken _ (_ _ _)%nat_scope.
Lemma own_auth_max_nat_null (γ : gname) (m : max_nat) :
own γ (max_nat m) -
own γ (max_nat m) own γ (max_nat (MaxNat 0)).
Lemma own_auth_max_nat_zero (γ : gname) :
|==> own γ ( MaxNat 0).
Proof.
by rewrite - own_op.
by apply own_unit.
Qed.
Global Arguments own_auth_max_nat_null _ _%nat_scope.
Lemma auth_max_nat_update_read_auth (γ : gname) (m : max_nat) :
own γ (max_nat m) -
|==> own γ (max_nat m) own γ (max_nat m).
Lemma auth_max_nat_update_read_auth (γ : gname) (m : nat) :
own γ ( MaxNat m) -
|==> own γ ( MaxNat m) own γ ( MaxNat m).
Proof.
iIntros "H●".
iDestruct (own_auth_max_nat_null with "H●") as "[H● H◯]".
(iMod (own_update_2 with "H● H◯") as "[$ $]" ; last done).
apply auth_update, max_nat_local_update. lia.
iIntros "H●". rewrite -own_op. iApply (own_update with "H●").
by apply auth_update_alloc, max_nat_local_update.
Qed.
Global Arguments auth_max_nat_update_read_auth _ _%nat_scope.
Lemma auth_max_nat_update_incr (γ : gname) (m k : max_nat) :
own γ (max_nat m) -
|==> own γ (max_nat (MaxNat (m + k))).
Lemma auth_max_nat_update_incr (γ : gname) (m k : nat) :
own γ ( MaxNat m) -
|==> own γ ( MaxNat (m + k)).
Proof.
iIntros "H●". iDestruct (own_auth_max_nat_null with "H●") as "[H● H◯]".
iMod (own_update_2 with "H● H◯") as "[$ _]" ; last done.
apply auth_update, max_nat_local_update. destruct m. simpl. lia.
iIntros "H●". iApply (own_update with "H●").
eapply auth_update_auth, max_nat_local_update. cbn. lia.
Qed.
Global Arguments auth_max_nat_update_incr _ (_ _)%nat_scope.
Lemma auth_max_nat_update_incr' (γ : gname) (m n k : max_nat) :
own γ (max_nat m) -
own γ (max_nat n) -
|==> own γ (max_nat (MaxNat (m + k))) own γ (max_nat (MaxNat (n + k))).
Lemma auth_max_nat_update_incr' (γ : gname) (m n k : nat) :
own γ ( MaxNat m) -
own γ ( MaxNat n) -
|==> own γ ( MaxNat (m + k)) own γ ( MaxNat (n + k)).
Proof.
iIntros "H● H◯".
iDestruct (own_auth_max_nat_le with "H● H◯") as %I. iClear "H◯".
iDestruct (auth_max_nat_update_incr _ _ k with "H●") as ">H●".
iDestruct (auth_max_nat_update_read_auth with "H●") as ">[$ H◯]".
iModIntro.
rewrite (_ : MaxNat (m + k) = MaxNat (n + k) MaxNat (m + k))%nat.
- iDestruct "H◯" as "[$ _]".
- rewrite max_nat_op. f_equal. lia.
iApply (own_auth_max_nat_weaken with "H◯"). lia.
Qed.
Global Arguments auth_max_nat_update_incr' _ (_ _ _)%nat_scope.
End Auth_max_nat.
......@@ -150,8 +150,7 @@ Section Definitions.
own γ1 (nat n).
Definition TRdup (n : nat) : iProp Σ :=
own γ2 (max_nat (MaxNat n)).
Arguments TRdup _%nat_scope.
own γ2 ( MaxNat n).
(* Note: we can avoid the update modality by redefining TR like so:
Definition TR' n : iProp Σ := ⌜n = 0%nat⌝ ∨ TR n. *)
......@@ -195,7 +194,7 @@ Section Definitions.
Lemma TRdup_weaken (n n : nat) :
(n n)%nat
TRdup n - TRdup n.
Proof using. apply (own_auth_max_nat_weaken _ (MaxNat _) (MaxNat _)). Qed.
Proof using. apply own_auth_max_nat_weaken. Qed.
Lemma TRdup_timeless n :
Timeless (TRdup n).
......@@ -220,7 +219,7 @@ Section Definitions.
#m
(if useTC then own γ (nat m) else True)
own γ1 (nat (max_tr - 1 - m))
own γ2 (max_nat (MaxNat (max_tr - 1 - m)))
own γ2 ( MaxNat (max_tr - 1 - m))
)%I.
Lemma TR_nmax_absurd (E : coPset) :
......@@ -249,8 +248,7 @@ Section Definitions.
Proof using.
iIntros (?) "#Inv Hγ2◯".
iInv tctrN as (m) "(>I & _ & _ & _ & >Hγ2●)" "InvClose" ; iDestruct "I" as %I.
iDestruct (own_auth_max_nat_le with "Hγ2● Hγ2◯") as %I'.
simpl in I'. exfalso ; lia.
iDestruct (own_auth_max_nat_le with "Hγ2● Hγ2◯") as %I'. exfalso ; lia.
Qed.
Lemma TRdup_lt_nmax n (E : coPset) :
tctrN E
......@@ -332,8 +330,8 @@ Section Definitions.
rewrite /TC ; destruct useTC ; last done.
by iMod (auth_nat_update_decr _ _ _ 1 with "Hγ● Hγ◯") as "[$ _]".
}
iMod (auth_nat_update_incr _ _ 1 with "Hγ1●") as "[Hγ1● Hγ1◯]" ; simpl.
iMod (auth_max_nat_update_incr' _ _ _ (MaxNat 1) with "Hγ2● Hγ2◯") as "[Hγ2● Hγ2◯]" ; simpl.
iMod (auth_nat_update_incr _ _ 1 with "Hγ1●") as "[Hγ1● Hγ1◯]".
iMod (auth_max_nat_update_incr' _ _ _ 1 with "Hγ2● Hγ2◯") as "[Hγ2● Hγ2◯]".
iDestruct "I" as %I.
replace (max_tr - 1 - m + 1)%nat with (max_tr - 1 - (m - 1))%nat by lia.
assert ((m-1) < max_tr)%nat by lia.
......@@ -837,7 +835,7 @@ Section Soundness.
}
iMod "Hγalloc" as (γ) "[Hγ● Hγ◯]".
iMod (auth_nat_alloc (max_tr-1-M)) as (γ1) "[Hγ1● _]".
iMod (auth_max_nat_alloc (MaxNat (max_tr-1-M))) as (γ2) "[Hγ2● _]".
iMod (auth_max_nat_alloc (max_tr-1-M)) as (γ2) "[Hγ2● _]".
(* packing all those bits, build the heap instance necessary to use time credits: *)
pose (Build_tctrHeapG Σ (HeapG Σ _ Hheap) _ _ _ _ γ γ1 γ2 _)
as HtcHeapG.
......
......@@ -30,7 +30,7 @@ Section Thunk.
Definition ThunkInv t γ nc φ : iProp Σ := (
(ac : nat),
own γ (max_nat (MaxNat ac))
own γ ( MaxNat ac)
(
( (f : val),
t UNEVALUATEDV « f »
......@@ -46,7 +46,7 @@ Section Thunk.
Definition Thunk p t n φ : iProp Σ := (
(γ : gname) (nc : nat),
na_inv p (thunkN t) (ThunkInv t γ nc φ)
own γ (max_nat (MaxNat (nc-n)))
own γ ( MaxNat (nc-n))
)%I.
Lemma thunk_persistent p t n φ :
......@@ -66,8 +66,7 @@ Section Thunk.
Proof.
iIntros (I) "H". iDestruct "H" as (γ nc) "[Hinv Hγ◯]".
iExists γ, nc. iFrame "Hinv".
iDestruct (own_auth_max_nat_weaken _ (MaxNat (nc-n))%nat (MaxNat (nc-n))%nat with "Hγ◯") as "$".
simpl. lia.
iDestruct (own_auth_max_nat_weaken _ (nc-n) (nc-n) with "Hγ◯") as "$". lia.
Qed.
Definition create : val :=
......@@ -92,7 +91,7 @@ Section Thunk.
{{{ (t : loc), RET #t ; Thunk p t nc φ }}}.
Proof.
iIntros "#Htickinv" (Φ) "!# [? Hf] Post".
iMod (auth_max_nat_alloc (MaxNat 0)) as (γ) "[Hγ● Hγ◯]".
iMod (auth_max_nat_alloc 0) as (γ) "[Hγ● Hγ◯]".
iApply wp_fupd.
wp_tick_lam. wp_tick_inj. wp_tick_alloc t.
iApply "Post".
......@@ -160,7 +159,7 @@ Section Thunk.
{
iAssert (TC (ac + k)) with "[Htc Htc_k]" as "Htc" ;
first by iSplitL "Htc".
iDestruct (auth_max_nat_update_incr' _ _ _ (MaxNat k) with "Hγ● Hγ◯") as ">[Hγ●' #Hγ◯']" ;
iDestruct (auth_max_nat_update_incr' _ _ _ k with "Hγ● Hγ◯") as ">[Hγ●' #Hγ◯']" ;
iClear "Hγ◯".
iMod ("Hclose" with "[-Hγ◯']") as "$". {
iFrame "Hp".
......@@ -168,11 +167,11 @@ Section Thunk.
}
iModIntro.
iExists γ, nc. iFrame "Hthunkinv".
iDestruct (own_auth_max_nat_weaken _ (MaxNat ((nc-n)+k)) (MaxNat (nc-(n-k))) with "Hγ◯'") as "$" ; simpl; lia.
iDestruct (own_auth_max_nat_weaken _ ((nc-n)+k) (nc-(n-k)) with "Hγ◯'") as "$" ; lia.
}
(* (2) if it is EVALUATED, then we do nothing: *)
{
iDestruct (auth_max_nat_update_incr' _ _ _ (MaxNat k) with "Hγ● Hγ◯") as ">[Hγ●' #Hγ◯']" ;
iDestruct (auth_max_nat_update_incr' _ _ _ k with "Hγ● Hγ◯") as ">[Hγ●' #Hγ◯']" ;
iClear "Hγ◯".
iMod ("Hclose" with "[-Hγ◯']") as "$". {
iFrame "Hp".
......@@ -180,7 +179,7 @@ Section Thunk.
}
iModIntro.
iExists γ, nc. iFrame "Hthunkinv".
iDestruct (own_auth_max_nat_weaken _ (MaxNat ((nc-n)+k)) (MaxNat (nc-(n-k))) with "Hγ◯'") as "$" ; simpl; lia.
iDestruct (own_auth_max_nat_weaken _ ((nc-n)+k) (nc-(n-k)) with "Hγ◯'") as "$" ; lia.
}
Qed.
......
......@@ -85,8 +85,7 @@ Section TickSpec.
own γ1 (nat n).
Definition TRdup (n : nat) : iProp Σ :=
own γ2 (max_nat (MaxNat n)).
Arguments TRdup _%nat_scope.
own γ2 ( MaxNat n).
(* Note: we can avoid the update modality by redefining TR like so:
Definition TR' n : iProp Σ := ⌜n = 0%nat⌝ ∨ TR n. *)
......@@ -128,7 +127,7 @@ Section TickSpec.
Lemma TRdup_weaken (n n : nat) :
(n n)%nat
TRdup n - TRdup n.
Proof. apply (own_auth_max_nat_weaken _ (MaxNat _) (MaxNat _)). Qed.
Proof. apply own_auth_max_nat_weaken. Qed.
Lemma TRdup_timeless n :
Timeless (TRdup n).
......@@ -145,7 +144,7 @@ Section TickSpec.
Definition timeReceiptN := nroot .@ "timeReceipt".
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.
inv timeReceiptN ( (n:nat), #(nmax-n-1) own γ1 (nat n) own γ2 ( MaxNat n) (n < nmax)%nat)%I.
Lemma TR_nmax_absurd (E : coPset) :
timeReceiptN E
......@@ -173,8 +172,7 @@ Section TickSpec.
Proof.
iIntros (?) "#Inv Hγ2◯".
iInv timeReceiptN as (n) ">(Hℓ & Hγ1● & Hγ2● & In)" "InvClose" ; iDestruct "In" as %In.
iDestruct (own_auth_max_nat_le with "Hγ2● Hγ2◯") as %In'.
simpl in In'. exfalso ; lia.
iDestruct (own_auth_max_nat_le with "Hγ2● Hγ2◯") as %In'. exfalso ; lia.
Qed.
Lemma TRdup_lt_nmax n (E : coPset) :
timeReceiptN E
......@@ -241,9 +239,8 @@ Section TickSpec.
(* reform the invariant with n+1 instead of n, and an additional time
receipt produced: *)
replace (nmax - n - 1 - 1) with (nmax - (n+1)%nat - 1) by lia.
iMod (auth_nat_update_incr _ _ 1 with "Hγ1●") as "[Hγ1● Hγ1◯]" ; simpl.
(* iMod (auth_max_nat_update_incr _ _ 1 with "Hγ2●") as "Hγ2●" ; simpl. *)
iMod (auth_max_nat_update_incr' _ _ _ (MaxNat 1) with "Hγ2● Hγ2◯") as "[Hγ2● Hγ2◯]" ; simpl.
iMod (auth_nat_update_incr _ _ 1 with "Hγ1●") as "[Hγ1● Hγ1◯]".
iMod (auth_max_nat_update_incr' _ _ _ 1 with "Hγ2● Hγ2◯") as "[Hγ2● Hγ2◯]".
assert ((n+1) < nmax)%nat by lia.
(* close the invariant: *)
iMod ("InvClose" with "[ Hℓ Hγ1● Hγ2● ]") as "_" ; [ by auto with iFrame | iModIntro ].
......@@ -314,7 +311,7 @@ Section Soundness.
{ by rewrite lookup_insert. }
(* allocate the ghost state associated with ℓ: *)
iMod (auth_nat_alloc 0) as (γ1) "[Hγ1● _]".
iMod (auth_max_nat_alloc (MaxNat 0)) as (γ2) "[Hγ2● _]".
iMod (auth_max_nat_alloc 0) as (γ2) "[Hγ2● _]".
(* packing all those bits, build the heap instance necessary to use time receipts: *)
pose (Build_timeReceiptHeapG Σ (HeapG Σ _ Hheap) _ _ _ γ1 γ2)
as HtrHeapG.
......
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