Commit 04bfd18c authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Compat with Iris, bump version.

parent 872a1cb1
......@@ -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-10-13.1.5558d66d") | (= "dev") }
"coq-iris" { (= "dev.2020-10-14.0.dc793c10") | (= "dev") }
"coq-tlc" { (= "20181116") | (= "dev") }
]
......@@ -867,7 +867,7 @@ Section Soundness.
}
iIntros (?) "!>".
(* finally, use the user-given specification: *)
iExists (λ σ _, gen_heap_ctx σ), (λ _, True%I). iSplitL "H Hh●".
iExists (λ σ _, gen_heap_interp σ), (λ _, True%I). iSplitL "H Hh●".
- iExists . auto with iFrame.
- iApply (Hspec $ HtcHeapG with "Hinv Hγ◯") ; auto.
Qed.
......
......@@ -444,7 +444,7 @@ Section Soundness.
}
iIntros (?) "!>".
(* finally, use the user-given specification: *)
iExists (λ σ _, gen_heap_ctx σ), (λ _, True%I). iSplitL "H Hh●".
iExists (λ σ _, gen_heap_interp σ), (λ _, True%I). iSplitL "H Hh●".
- iExists . auto with iFrame.
- iDestruct (own_auth_nat_weaken _ _ _ Ik with "Hγ◯") as "Hγ◯".
iApply (Hspec with "Hinv Hγ◯") ; auto.
......
......@@ -229,9 +229,9 @@ Qed.
* said, n ≤ m.
*)
Lemma gen_heap_ctx_mapsto {Σ : gFunctors} {Hgen : gen_heapG loc val Σ} (σ : state) (l : loc) (v v' : val) :
Lemma gen_heap_interp_mapsto {Σ : gFunctors} {Hgen : gen_heapG loc val Σ} (σ : state) (l : loc) (v v' : val) :
σ !! l = Some v
gen_heap_ctx σ -
gen_heap_interp σ -
l v' -
v = v'.
Proof.
......@@ -282,7 +282,7 @@ Proof.
}
(* finally, use the user-given specification: *)
iModIntro.
iExists (λ σ _ _, gen_heap_ctx σ), (λ _, True%I). iSplitL "H Hh●" ;
iExists (λ σ _ _, gen_heap_interp σ), (λ _, True%I). iSplitL "H Hh●" ;
first by (iExists ; auto with iFrame).
iSplitL ; first (iApply (Hspec with "Hinv Hγ◯") ; auto).
(* it remains to prove that the interpretation of the final state, along
......@@ -291,7 +291,7 @@ Proof.
(* open the invariant: *)
iInv timeCreditN as (m') ">[Hc Hγ●]" "InvClose".
(* derive that z = m' (that is, the relative integer is in fact a natural integer): *)
iDestruct (gen_heap_ctx_mapsto with "Hheap2 Hc") as %Eq ; first (by apply lookup_insert) ;
iDestruct (gen_heap_interp_mapsto with "Hheap2 Hc") as %Eq ; first (by apply lookup_insert) ;
injection Eq as ->.
(* close the invariant (in fact, this is not required): *)
iMod ("InvClose" with "[-]") as "_" ; first by auto with iFrame.
......
......@@ -342,7 +342,7 @@ Section Soundness.
}
iModIntro.
(* finally, use the user-given specification: *)
iExists (λ σ _, gen_heap_ctx σ), (λ _, True%I). iSplitL "H Hh●".
iExists (λ σ _, gen_heap_interp σ), (λ _, True%I). iSplitL "H Hh●".
- iExists . auto with iFrame.
- iApply (Hspec with "Hinv") ; auto.
Qed.
......
......@@ -20,6 +20,6 @@ Proof.
intros Hwp; eapply (wp_adequacy _ _); iIntros (??) "".
iMod (gen_heap_init σ) as (?) "Hh".
iModIntro.
iExists (λ σ κs, (gen_heap_ctx σ)%I), (λ _, True%I). iFrame.
iExists (λ σ κs, (gen_heap_interp σ)%I), (λ _, True%I). iFrame.
iApply (Hwp (HeapG _ _ _)).
Qed.
......@@ -15,7 +15,7 @@ Class heapG Σ := HeapG {
Instance heapG_irisG `{heapG Σ} : irisG heap_lang Σ := {
iris_invG := heapG_invG;
state_interp σ κs _ := gen_heap_ctx σ;
state_interp σ κs _ := gen_heap_interp σ;
fork_post _ := True%I
}.
......
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