Commit 6d372842 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Fix build, bump Iris.

parent d2e5a8c0
......@@ -11,6 +11,6 @@ install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iris_time" ]
depends: [
"coq" { (>= "8.10.2" & < "8.13~") | (= "dev") }
"coq-iris" { (= "dev.2020-12-18.3.e7bfdf12") | (= "dev") }
"coq-iris" { (= "dev.2021-01-08.0.51cc75f3") | (= "dev") }
"coq-tlc" { (= "20200328") | (= "dev") }
]
......@@ -856,7 +856,7 @@ Section Soundness.
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● _]".
(* packing all those bits, build the heap instance necessary to use time credits: *)
pose (Build_tctrHeapG Σ (HeapG Σ _ (GenHeapG _ _ Σ _ _ _ _ _ h γmeta)) _ _ _ _ γ γ1 γ2 _)
pose (Build_tctrHeapG Σ (HeapG Σ _ (GenHeapG _ _ Σ h γmeta)) _ _ _ _ γ γ1 γ2 _)
as HtcHeapG.
(* create the invariant: *)
iAssert (|={}=> TCTR_invariant max_tr)%I with "[Hℓ◯ Hγ● Hγ1● Hγ2●]" as "> Hinv".
......
......@@ -433,7 +433,7 @@ Section Soundness.
(* allocate the ghost state associated with ℓ: *)
iMod (auth_nat_alloc k) as (γ) "[Hγ● Hγ◯]".
(* packing all those bits, build the heap instance necessary to use time credits: *)
pose (Build_timeCreditHeapG Σ (HeapG Σ _ (GenHeapG _ _ Σ _ _ _ _ _ h γmeta)) _ _ γ)
pose (Build_timeCreditHeapG Σ (HeapG Σ _ (GenHeapG _ _ Σ h γmeta)) _ _ γ)
as HtcHeapG.
(* create the invariant: *)
iAssert (|={}=> TC_invariant)%I with "[Hℓ◯ Hγ●]" as "> Hinv".
......
......@@ -258,7 +258,8 @@ Proof.
iMod (auth_nat_alloc m) as (γ) "[Hγ● Hγ◯]".
(* packing all those bits, build the heap instance necessary to use time credits: *)
destruct HtcPreG as [[HinvPreG [HgenHeapPreInG]] HinG] ; simpl ; clear HinvPreG.
pose (Build_timeCreditHeapG Σ (HeapG Σ HinvG (GenHeapG _ _ Σ _ _ _ _ _ h γmeta)) HinG _ γ)
pose (Build_timeCreditHeapG Σ (HeapG Σ HinvG
(@GenHeapG _ _ Σ _ _ {| gen_heap_preG_inG := _ |} h γmeta)) HinG _ γ)
as HtcHeapG.
(* create the invariant: *)
iAssert (|={}=> TC_invariant)%I with "[Hℓ◯ Hγ●]" as "> #Hinv".
......
......@@ -331,7 +331,7 @@ Section Soundness.
iMod (auth_nat_alloc 0) as (γ1) "[Hγ1● _]".
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)
pose (Build_timeReceiptHeapG Σ (HeapG Σ _ (GenHeapG _ _ Σ h γmeta)) _ _ _ γ1 γ2)
as HtrHeapG.
(* create the invariant: *)
iAssert (|={}=> TR_invariant nmax)%I with "[Hℓ◯ Hγ1● Hγ2●]" as "> Hinv".
......
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