Commit d592e2f2 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Update wrt Iris.

parent 0da70c19
......@@ -51,7 +51,7 @@ To create an archive of the project:
Important modules are highlighted.
* `Misc`: some basic things
* `Auth_nat`, `Auth_mnat`: simple lemmas about the authoritative resources on
* `Auth_nat`, `Auth_max_nat`: simple lemmas about the authoritative resources on
(ℕ, +) and (ℕ, max)
* `heap_lang/` directory: the toy language under study
* `Reduction`: generic lemmas about reduction, safety, closedness, fresh
......
......@@ -14,7 +14,7 @@ theories/heap_lang/proofmode.v
theories/heap_lang/tactics.v
theories/heap_lang/lib/assert.v
theories/Auth_mnat.v
theories/Auth_max_nat.v
theories/Auth_nat.v
theories/Base.v
theories/ClockIntegers.v
......
......@@ -11,6 +11,6 @@ install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iris_time" ]
depends: [
"coq" { (>= "8.9.1" & < "8.11~") | (= "dev") }
"coq-iris" { (= "dev.2020-05-24.1.76bec8b7") | (= "dev") }
"coq-iris" { (= "dev.2020-06-19.1.3091e4d4") | (= "dev") }
"coq-tlc" { (= "20181116") | (= "dev") }
]
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) 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).
Proof.
iMod (own_alloc (max_nat n max_nat 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) -
(n m)%nat.
Proof.
iIntros "H● H◯".
iDestruct (own_valid_2 with "H● H◯") as % [[k ->] _] % auth_both_valid.
iPureIntro. apply Max.le_max_l.
Qed.
Lemma own_auth_max_nat_weaken (γ : gname) (n n : max_nat) :
(n n)%nat
own γ (max_nat n) -
own γ (max_nat n).
Proof.
iIntros (I) "H".
rewrite (_ : n = n n)%nat.
- iDestruct "H" as "[_$]".
- destruct n, n. rewrite max_nat_op_max. f_equal. simpl in I. lia.
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)).
Proof.
by rewrite - own_op.
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).
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.
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))).
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.
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))).
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_max. f_equal. lia.
Qed.
Global Arguments auth_max_nat_update_incr' _ (_ _ _)%nat_scope.
End Auth_max_nat.
From iris Require Export algebra.auth.
From iris Require Import algebra.excl base_logic.lib.own proofmode.tactics.
Notation "'●mnat' n" := (auth_auth (A:=mnatUR) 1%Qp n%nat) (at level 20).
Notation "'◯mnat' n" := (auth_frag (A:=mnatUR) n%nat) (at level 20).
Section Auth_mnat.
Context `{inG Σ (authR mnatUR)}.
Lemma auth_mnat_alloc (n : mnat) :
|==> γ, own γ (mnat n) own γ (mnat n).
Proof.
iMod (own_alloc (mnat n mnat n)) as (γ) "[? ?]".
- by apply auth_both_valid_2.
- by auto with iFrame.
Qed.
Global Arguments auth_mnat_alloc _%nat.
Lemma own_auth_mnat_le (γ : gname) (m n : mnat) :
own γ (mnat m) -
own γ (mnat n) -
(n m)%nat.
Proof.
iIntros "H● H◯".
iDestruct (own_valid_2 with "H● H◯") as % [[k ->] _] % auth_both_valid.
iPureIntro. apply Max.le_max_l.
Qed.
Lemma own_auth_mnat_weaken (γ : gname) (n n : mnat) :
(n n)%nat
own γ (mnat n) -
own γ (mnat n).
Proof.
iIntros (I) "H".
rewrite (_ : n = n `max` n)%nat ; last (by rewrite max_l).
iDestruct "H" as "[_$]".
Qed.
Global Arguments own_auth_mnat_weaken _ (_ _ _)%nat_scope.
Lemma own_auth_mnat_null (γ : gname) (m : mnat) :
own γ (mnat m) -
own γ (mnat m) own γ (mnat 0).
Proof.
by rewrite - own_op.
Qed.
Global Arguments own_auth_mnat_null _ _%nat_scope.
Lemma auth_mnat_update_read_auth (γ : gname) (m : mnat) :
own γ (mnat m) -
|==> own γ (mnat m) own γ (mnat m).
Proof.
iIntros "H●".
iDestruct (own_auth_mnat_null with "H●") as "[H● H◯]".
(iMod (own_update_2 with "H● H◯") as "[$ $]" ; last done).
apply auth_update, mnat_local_update. lia.
Qed.
Global Arguments auth_mnat_update_read_auth _ _%nat_scope.
Lemma auth_mnat_update_incr (γ : gname) (m k : mnat) :
own γ (mnat m) -
|==> own γ (mnat (m + k : mnat)).
Proof.
iIntros "H●". iDestruct (own_auth_mnat_null with "H●") as "[H● H◯]".
iMod (own_update_2 with "H● H◯") as "[$ _]" ; last done.
apply auth_update, mnat_local_update. lia.
Qed.
Global Arguments auth_mnat_update_incr _ (_ _)%nat_scope.
Lemma auth_mnat_update_incr' (γ : gname) (m n k : mnat) :
own γ (mnat m) -
own γ (mnat n) -
|==> own γ (mnat (m + k : mnat)) own γ (mnat (n + k : mnat)).
Proof.
iIntros "H● H◯".
iDestruct (own_auth_mnat_le with "H● H◯") as %I. iClear "H◯".
iDestruct (auth_mnat_update_incr _ _ k with "H●") as ">H●".
iDestruct (auth_mnat_update_read_auth with "H●") as ">[$ H◯]".
iModIntro.
rewrite (_ : m + k = (n + k) `max` (m + k))%nat ; last lia.
iDestruct "H◯" as "[$ _]".
Qed.
Global Arguments auth_mnat_update_incr' _ (_ _ _)%nat_scope.
End Auth_mnat.
From iris Require Export algebra.auth.
From iris Require Import base_logic.lib.own proofmode.tactics.
From iris Require Export algebra.auth algebra.numbers.
From iris Require Import base_logic.lib.own proofmode.tactics.
......
......@@ -2,7 +2,7 @@ From iris_time Require Import Base.
From iris.base_logic Require Import invariants.
From iris.proofmode Require Import coq_tactics.
From iris_time.heap_lang Require Import proofmode notation adequacy lang.
From iris_time Require Import Auth_nat Auth_mnat Reduction Tactics.
From iris_time Require Import Auth_nat Auth_max_nat Reduction Tactics.
From iris_time Require Export Simulation.
Implicit Type e : expr.
......@@ -54,7 +54,7 @@ Class tctrHeapPreG Σ := {
tctrHeapPreG_heapPreG :> heapPreG Σ ;
tctrHeapPreG_inG_TC :> inG Σ (authR natUR) ;
tctrHeapPreG_inG_TR :> inG Σ (authR natUR) ;
tctrHeapPreG_inG_TRdup :> inG Σ (authR mnatUR) ;
tctrHeapPreG_inG_TRdup :> inG Σ (authR max_natUR) ;
}.
Class UseTC := useTC : bool.
......@@ -63,7 +63,7 @@ Class tctrHeapG Σ := {
tctrHeapG_heapG :> heapG Σ ;
tctrHeapG_inG_TC :> inG Σ (authR natUR) ;
tctrHeapG_inG_TR :> inG Σ (authR natUR) ;
tctrHeapG_inG_TRdup :> inG Σ (authR mnatUR) ;
tctrHeapG_inG_TRdup :> inG Σ (authR max_natUR) ;
tctrHeapG_loc :> TickCounter ;
tctrHeapG_name_TC : gname ;
tctrHeapG_name_TR : gname ;
......@@ -139,8 +139,8 @@ Section Definitions.
Definition TR (n : nat) : iProp Σ :=
own γ1 (nat n).
Definition TRdup (n : mnat) : iProp Σ :=
own γ2 (mnat n).
Definition TRdup (n : nat) : iProp Σ :=
own γ2 (max_nat (MaxNat n)).
Arguments TRdup _%nat_scope.
Lemma TR_plus m n :
......@@ -171,11 +171,11 @@ Section Definitions.
Lemma TRdup_max m n :
TRdup (m `max` n) (TRdup m TRdup n)%I.
Proof using. by rewrite /TRdup auth_frag_op own_op. Qed.
Proof using. by rewrite /TRdup -own_op -auth_frag_op. Qed.
Lemma TRdup_weaken (n n : nat) :
(n n)%nat
TRdup n - TRdup n.
Proof using. apply own_auth_mnat_weaken. Qed.
Proof using. apply (own_auth_max_nat_weaken _ (MaxNat _) (MaxNat _)). Qed.
Lemma TRdup_timeless n :
Timeless (TRdup n).
......@@ -200,7 +200,7 @@ Section Definitions.
#m
(if useTC then own γ (nat m) else True)
own γ1 (nat (max_tr - 1 - m))
own γ2 (mnat (max_tr - 1 - m))
own γ2 (max_nat (MaxNat (max_tr - 1 - m)))
)%I.
Lemma zero_TC E:
......@@ -230,7 +230,7 @@ Section Definitions.
Proof using.
iIntros (?) "#Htickinv".
iInv tctrN as (m) "(>? & >? & ? & >? & >Hγ2●)" "InvClose".
iDestruct (own_auth_mnat_null with "Hγ2●") as "[Hγ2● $]".
iDestruct (own_auth_max_nat_null with "Hγ2●") as "[Hγ2● $]".
iApply "InvClose" ; eauto with iFrame.
Qed.
......@@ -260,8 +260,8 @@ Section Definitions.
Proof using.
iIntros (?) "#Inv Hγ2◯".
iInv tctrN as (m) "(>I & _ & _ & _ & >Hγ2●)" "InvClose" ; iDestruct "I" as %I.
iDestruct (own_auth_mnat_le with "Hγ2● Hγ2◯") as %I'.
exfalso ; lia.
iDestruct (own_auth_max_nat_le with "Hγ2● Hγ2◯") as %I'.
simpl in I'. exfalso ; lia.
Qed.
Lemma TRdup_lt_nmax n (E : coPset) :
tctrN E
......@@ -281,7 +281,7 @@ Section Definitions.
iIntros (?) "#Inv Hγ1◯".
iInv tctrN as (m) "(>I & >Hℓ & Hγ● & >Hγ1● & >Hγ2●)" "InvClose".
iDestruct (own_auth_nat_le with "Hγ1● Hγ1◯") as %I'.
iDestruct (auth_mnat_update_read_auth with "Hγ2●") as ">[Hγ2● Hγ2◯]".
iDestruct (auth_max_nat_update_read_auth with "Hγ2●") as ">[Hγ2● Hγ2◯]".
iAssert (TR n TRdup n)%I with "[$Hγ1◯ Hγ2◯]" as "$". {
rewrite (_ : (max_tr-1-m) = (max_tr-1-m) `max` n)%nat ; last lia.
iDestruct "Hγ2◯" as "[_ $]".
......@@ -344,7 +344,7 @@ Section Definitions.
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_mnat_update_incr' _ _ _ 1 with "Hγ2● Hγ2◯") as "[Hγ2● Hγ2◯]" ; simpl.
iMod (auth_max_nat_update_incr' _ _ _ (MaxNat 1) with "Hγ2● Hγ2◯") as "[Hγ2● Hγ2◯]" ; simpl.
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.
......@@ -859,7 +859,7 @@ Section Soundness.
}
iMod "Hγalloc" as (γ) "[Hγ● Hγ◯]".
iMod (auth_nat_alloc (max_tr-1-M)) as (γ1) "[Hγ1● _]".
iMod (auth_mnat_alloc (max_tr-1-M)) as (γ2) "[Hγ2● _]".
iMod (auth_max_nat_alloc (MaxNat (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 Σ _ (GenHeapG _ _ Σ _ _ _ _ _ h γmeta)) _ _ _ _ γ γ1 γ2 _)
as HtcHeapG.
......
From stdpp Require Import namespaces.
From iris.base_logic.lib Require Import na_invariants.
From iris_time.heap_lang Require Import proofmode notation.
From iris_time Require Import TimeCredits Auth_mnat.
From iris_time Require Import TimeCredits Auth_max_nat.
Section Thunk.
Context `{timeCreditHeapG Σ}.
Context `{inG Σ (authR mnatUR)}.
Context `{inG Σ (authR max_natUR)}.
Context `{na_invG Σ}.
Implicit Type t : loc.
......@@ -30,7 +30,7 @@ Section Thunk.
Definition ThunkInv t γ nc φ : iProp Σ := (
(ac : nat),
own γ (mnat ac)
own γ (max_nat (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 γ (mnat (nc-n))
own γ (max_nat (MaxNat (nc-n)))
)%I.
Lemma thunk_persistent p t n φ :
......@@ -66,7 +66,8 @@ Section Thunk.
Proof.
iIntros (I) "H". iDestruct "H" as (γ nc) "[Hinv Hγ◯]".
iExists γ, nc. iFrame "Hinv".
iDestruct (own_auth_mnat_weaken _ (nc-n)%nat (nc-n)%nat with "Hγ◯") as "$" ; lia.
iDestruct (own_auth_max_nat_weaken _ (MaxNat (nc-n))%nat (MaxNat (nc-n))%nat with "Hγ◯") as "$".
simpl. lia.
Qed.
Definition create : val :=
......@@ -92,7 +93,7 @@ Section Thunk.
Proof.
iIntros "#Htickinv" (Φ) "!# [? Hf] Post".
iDestruct (zero_TC with "Htickinv") as ">Htc0".
iMod (auth_mnat_alloc 0) as (γ) "[Hγ● Hγ◯]".
iMod (auth_max_nat_alloc (MaxNat 0)) as (γ) "[Hγ● Hγ◯]".
iApply wp_fupd.
wp_tick_lam. wp_tick_inj. wp_tick_alloc t.
iApply "Post".
......@@ -125,7 +126,7 @@ Section Thunk.
(* (1) if it is UNEVALUATED, we evaluate it: *)
{
wp_tick_load. wp_tick_match.
iDestruct (own_auth_mnat_le with "Hγ● Hγ◯") as %I.
iDestruct (own_auth_max_nat_le with "Hγ● Hγ◯") as %I.
iDestruct (TC_weaken _ _ I with "Htc") as "Htc".
wp_apply ("Hf" with "Htc") ; iIntros (v) "Hv".
wp_tick_let. wp_tick_inj. wp_tick_store. wp_tick_seq.
......@@ -160,7 +161,7 @@ Section Thunk.
{
iAssert (TC (ac + k)) with "[Htc Htc_k]" as "Htc" ;
first by iSplitL "Htc".
iDestruct (auth_mnat_update_incr' _ _ _ k with "Hγ● Hγ◯") as ">[Hγ●' #Hγ◯']" ;
iDestruct (auth_max_nat_update_incr' _ _ _ (MaxNat k) with "Hγ● Hγ◯") as ">[Hγ●' #Hγ◯']" ;
iClear "Hγ◯".
iMod ("Hclose" with "[-Hγ◯']") as "$". {
iFrame "Hp".
......@@ -168,11 +169,11 @@ Section Thunk.
}
iModIntro.
iExists γ, nc. iFrame "Hthunkinv".
iDestruct (own_auth_mnat_weaken _ ((nc-n)+k) (nc-(n-k)) with "Hγ◯'") as "$" ; lia.
iDestruct (own_auth_max_nat_weaken _ (MaxNat ((nc-n)+k)) (MaxNat (nc-(n-k))) with "Hγ◯'") as "$" ; simpl; lia.
}
(* (2) if it is EVALUATED, then we do nothing: *)
{
iDestruct (auth_mnat_update_incr' _ _ _ k with "Hγ● Hγ◯") as ">[Hγ●' #Hγ◯']" ;
iDestruct (auth_max_nat_update_incr' _ _ _ (MaxNat k) with "Hγ● Hγ◯") as ">[Hγ●' #Hγ◯']" ;
iClear "Hγ◯".
iMod ("Hclose" with "[-Hγ◯']") as "$". {
iFrame "Hp".
......@@ -180,7 +181,7 @@ Section Thunk.
}
iModIntro.
iExists γ, nc. iFrame "Hthunkinv".
iDestruct (own_auth_mnat_weaken _ ((nc-n)+k) (nc-(n-k)) with "Hγ◯'") as "$" ; lia.
iDestruct (own_auth_max_nat_weaken _ (MaxNat ((nc-n)+k)) (MaxNat (nc-(n-k))) with "Hγ◯'") as "$" ; simpl; lia.
}
Qed.
......
From iris.base_logic Require Import invariants.
From iris.proofmode Require Import coq_tactics.
From iris_time.heap_lang Require Import proofmode notation adequacy lang.
From iris_time Require Import Auth_nat Auth_mnat Reduction Tactics.
From iris_time Require Import Auth_nat Auth_max_nat Reduction Tactics.
From iris_time Require Export Simulation.
Implicit Type e : expr.
......@@ -48,13 +48,13 @@ Definition TR_interface `{irisG heap_lang Σ, Tick}
Class timeReceiptHeapPreG Σ := {
timeReceiptHeapPreG_heapPreG :> heapPreG Σ ;
timeReceiptHeapPreG_inG1 :> inG Σ (authR natUR) ;
timeReceiptHeapPreG_inG2 :> inG Σ (authR mnatUR) ;
timeReceiptHeapPreG_inG2 :> inG Σ (authR max_natUR) ;
}.
Class timeReceiptHeapG Σ := {
timeReceiptHeapG_heapG :> heapG Σ ;
timeReceiptHeapG_inG1 :> inG Σ (authR natUR) ;
timeReceiptHeapG_inG2 :> inG Σ (authR mnatUR) ;
timeReceiptHeapG_inG2 :> inG Σ (authR max_natUR) ;
timeReceiptHeapG_loc :> TickCounter ;
timeReceiptHeapG_name1 : gname ;
timeReceiptHeapG_name2 : gname ;
......@@ -83,8 +83,8 @@ Section TickSpec.
Definition TR (n : nat) : iProp Σ :=
own γ1 (nat n).
Definition TRdup (n : mnat) : iProp Σ :=
own γ2 (mnat n).
Definition TRdup (n : nat) : iProp Σ :=
own γ2 (max_nat (MaxNat n)).
Arguments TRdup _%nat_scope.
Lemma TR_plus m n :
......@@ -113,11 +113,11 @@ Section TickSpec.
Lemma TRdup_max m n :
TRdup (m `max` n) (TRdup m TRdup n)%I.
Proof. by rewrite /TRdup auth_frag_op own_op. Qed.
Proof. by rewrite /TRdup -own_op -auth_frag_op. Qed.
Lemma TRdup_weaken (n n : nat) :
(n n)%nat
TRdup n - TRdup n.
Proof. apply own_auth_mnat_weaken. Qed.
Proof. apply (own_auth_max_nat_weaken _ (MaxNat _) (MaxNat _)). Qed.
Lemma TRdup_timeless n :
Timeless (TRdup n).
......@@ -134,7 +134,7 @@ Section TickSpec.
Definition timeReceiptN := nroot .@ "timeReceipt".
Definition TR_invariant : iProp Σ :=
inv timeReceiptN ( (n:nat), #(nmax-n-1) own γ1 (nat n) own γ2 (mnat n) (n < nmax)%nat)%I.
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
......@@ -152,7 +152,7 @@ Section TickSpec.
Proof.
iIntros (?) "#Htickinv".
iInv timeReceiptN as (m) ">(Hcounter & Hγ1● & Hγ2● & Im)" "Hclose".
iDestruct (own_auth_mnat_null with "Hγ2●") as "[Hγ2● $]".
iDestruct (own_auth_max_nat_null with "Hγ2●") as "[Hγ2● $]".
iApply "Hclose" ; eauto with iFrame.
Qed.
......@@ -182,8 +182,8 @@ 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_mnat_le with "Hγ2● Hγ2◯") as %In'.
exfalso ; lia.
iDestruct (own_auth_max_nat_le with "Hγ2● Hγ2◯") as %In'.
simpl in In'. exfalso ; lia.
Qed.
Lemma TRdup_lt_nmax n (E : coPset) :
timeReceiptN E
......@@ -203,7 +203,7 @@ Section TickSpec.
iIntros (?) "#Inv Hγ1◯".
iInv timeReceiptN as (m) ">(Hℓ & Hγ1● & Hγ2● & Im)" "InvClose".
iDestruct (own_auth_nat_le with "Hγ1● Hγ1◯") as %In.
iDestruct (auth_mnat_update_read_auth with "Hγ2●") as ">[Hγ2● Hγ2◯]".
iDestruct (auth_max_nat_update_read_auth with "Hγ2●") as ">[Hγ2● Hγ2◯]".
iAssert (TR n TRdup n)%I with "[$Hγ1◯ Hγ2◯]" as "$". {
rewrite (_ : m = m `max` n)%nat ; last lia.
iDestruct "Hγ2◯" as "[_ $]".
......@@ -251,8 +251,8 @@ Section TickSpec.
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_mnat_update_incr _ _ 1 with "Hγ2●") as "Hγ2●" ; simpl. *)
iMod (auth_mnat_update_incr' _ _ _ 1 with "Hγ2● Hγ2◯") as "[Hγ2● Hγ2◯]" ; 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.
assert ((n+1) < nmax)%nat by lia.
(* close the invariant: *)
iMod ("InvClose" with "[ Hℓ Hγ1● Hγ2● ]") as "_" ; [ by auto with iFrame | iModIntro ].
......@@ -334,7 +334,7 @@ Section Soundness.
first by apply auth_auth_valid, to_gen_meta_valid.
(* allocate the ghost state associated with ℓ: *)
iMod (auth_nat_alloc 0) as (γ1) "[Hγ1● _]".
iMod (auth_mnat_alloc 0) as (γ2) "[Hγ2● _]".
iMod (auth_max_nat_alloc (MaxNat 0)) as (γ2) "[Hγ2● _]".
(* packing all those bits, build the heap instance necessary to use time receipts: *)
pose (Build_timeReceiptHeapG Σ (HeapG Σ _ (GenHeapG _ _ Σ _ _ _ _ _ h γmeta)) _ _ _ γ1 γ2)
as HtrHeapG.
......
Markdown is supported
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