Commit 72e838c7 authored by Ralf Jung's avatar Ralf Jung
Browse files

update dependencies

parent 515d13eb
......@@ -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.2021-03-06.3.b0708b01") | (= "dev") }
"coq-iris" { (= "dev.2021-03-08.2.5380a1d7") | (= "dev") }
"coq-tlc" { (= "20200328") | (= "dev") }
]
......@@ -833,21 +833,16 @@ Section Soundness.
(* … now we have to prove a WP. *)
set σ' := S«σ».
(* allocate the heap, including cell ℓ (on which we need to keep an eye): *)
iMod (own_alloc (gmap_view_auth 1 (<[ := #M]> σ') gmap_view_frag (DfracOwn 1) #M))
as (h) "[Hh● Hℓ◯]".
{ apply gmap_view_both_valid_L. split; first done.
rewrite lookup_insert. done.
}
(* allocate the meta-heap: *)
iMod (own_alloc (gmap_view_auth 1 (V:=gnameO) )) as (γmeta) "H" ;
first by apply gmap_view_auth_valid.
iMod (gen_heap_init (<[ := #M]> σ')) as (Hheap) "(Hh● & Hℓ◯ & _)".
iDestruct (big_sepM_lookup _ _ with "Hℓ◯") as "Hℓ◯".
{ by rewrite lookup_insert. }
(* allocate the ghost state associated with ℓ: *)
iAssert (|==> γ,
(if useTC then own γ ( M) else True)
(if useTC then own γ ( m) else True)
)%I as "Hγalloc".
{
rewrite /useTC ; case_bool_decide ; last done.
rewrite /useTC ; case_bool_decide ; last by iExists inhabitant.
rewrite (_ : M = m) ; last by (rewrite /M ; lia).
iMod (auth_nat_alloc m) as (γ) "[Hγ● Hγ◯]".
auto with iFrame.
......@@ -856,20 +851,18 @@ 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 Σ _ Hheap) _ _ _ _ γ γ1 γ2 _)
as HtcHeapG.
(* create the invariant: *)
iAssert (|={}=> TCTR_invariant max_tr)%I with "[Hℓ◯ Hγ● Hγ1● Hγ2●]" as "> Hinv".
{
iApply inv_alloc.
iExists M.
unfold mapsto ; destruct mapsto_aux as [_ ->] ; simpl. by iFrame.
iExists M. by iFrame.
}
iIntros (?) "!>".
(* finally, use the user-given specification: *)
iExists (λ σ _, gen_heap_interp σ), (λ _, True%I). iSplitL "H Hh●".
- iExists . auto with iFrame.
- iApply (Hspec $ HtcHeapG with "Hinv Hγ◯") ; auto.
iExists (λ σ _, gen_heap_interp σ), (λ _, True%I). iFrame.
iApply (Hspec $ HtcHeapG with "Hinv Hγ◯") ; auto.
Qed.
(* the final soundness theorem. *)
......
......@@ -422,32 +422,25 @@ Section Soundness.
(* … now we have to prove a WP. *)
set σ' := S«σ».
(* allocate the heap, including cell ℓ (on which we need to keep an eye): *)
iMod (own_alloc (gmap_view_auth 1 (<[ := #k]> σ') gmap_view_frag (DfracOwn 1) #k))
as (h) "[Hh● Hℓ◯]".
{ apply gmap_view_both_valid_L. split; first done.
rewrite lookup_insert. done.
}
(* allocate the meta-heap: *)
iMod (own_alloc (gmap_view_auth 1 (V:=gnameO) )) as (γmeta) "H" ;
first by apply gmap_view_auth_valid.
iMod (gen_heap_init (<[ := #k]> σ')) as (Hheap) "(Hh● & Hℓ◯ & _)".
iDestruct (big_sepM_lookup _ _ with "Hℓ◯") as "Hℓ◯".
{ by rewrite lookup_insert. }
(* 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 Σ _ Hheap) _ _ γ)
as HtcHeapG.
(* create the invariant: *)
iAssert (|={}=> TC_invariant)%I with "[Hℓ◯ Hγ●]" as "> Hinv".
{
iApply inv_alloc.
iExists k.
unfold mapsto ; destruct mapsto_aux as [_ ->] ; simpl. by iFrame.
iExists k. iFrame.
}
iIntros (?) "!>".
(* finally, use the user-given specification: *)
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.
iExists (λ σ _, gen_heap_interp σ), (λ _, True%I). iFrame.
iDestruct (own_auth_nat_weaken _ _ _ Ik with "Hγ◯") as "Hγ◯".
iApply (Hspec with "Hinv Hγ◯") ; auto.
Qed.
Theorem spec_tctranslation__adequate_and_bounded {Σ} m φ e :
......
......@@ -246,32 +246,24 @@ Proof.
* we settle the needed invariant TC_invariant. *)
set σ' := S«σ1».
(* allocate the heap, including cell ℓ (on which we need to keep an eye): *)
iMod (own_alloc (gmap_view_auth 1 (<[ := #m]> σ') gmap_view_frag (DfracOwn 1) #m))
as (h) "[Hh● Hℓ◯]".
{ apply gmap_view_both_valid_L. split; first done.
rewrite lookup_insert. done.
}
(* allocate the meta-heap: *)
iMod (own_alloc (gmap_view_auth 1 (V:=gnameO) )) as (γmeta) "H" ;
first by apply gmap_view_auth_valid.
iMod (gen_heap_init (<[ := #m]> σ')) as (Hheap) "(Hh● & Hℓ◯ & _)".
iDestruct (big_sepM_lookup _ _ with "Hℓ◯") as "Hℓ◯".
{ by rewrite lookup_insert. }
(* allocate the ghost state associated with ℓ: *)
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 _ _ Σ _ _ {| gen_heap_preG_inG := _ |} h γmeta)) HinG _ γ)
pose (Build_timeCreditHeapG Σ (HeapG Σ HinvG Hheap) HinG _ γ)
as HtcHeapG.
(* create the invariant: *)
iAssert (|={}=> TC_invariant)%I with "[Hℓ◯ Hγ●]" as "> #Hinv".
{
iApply inv_alloc.
iExists m.
unfold mapsto ; destruct mapsto_aux as [_ ->] ; simpl. by iFrame.
iExists m. by iFrame.
}
(* finally, use the user-given specification: *)
iModIntro.
iExists (λ σ _ _, gen_heap_interp σ), (λ _, True%I). iSplitL "H Hh●" ;
first by (iExists ; auto with iFrame).
iExists (λ σ _ _, gen_heap_interp σ), (λ _, True%I). iFrame.
iSplitL ; first (iApply (Hspec with "Hinv Hγ◯") ; auto).
(* it remains to prove that the interpretation of the final state, along
* with the invariant, implies the inequality… *)
......
......@@ -319,32 +319,26 @@ Section Soundness.
(* … now we have to prove a WP. *)
set σ' := S«σ».
(* allocate the heap, including cell ℓ (on which we need to keep an eye): *)
iMod (own_alloc (gmap_view_auth 1 (<[ := #(nmax-1)%nat]> σ') gmap_view_frag (DfracOwn 1) #(nmax-1)%nat))
as (h) "[Hh● Hℓ◯]".
{ apply gmap_view_both_valid_L. split; first done.
rewrite lookup_insert. done.
}
(* allocate the meta-heap: *)
iMod (own_alloc (gmap_view_auth 1 (V:=gnameO) )) as (γmeta) "H" ;
first by apply gmap_view_auth_valid.
iMod (gen_heap_init (<[ := #(nmax-1)%nat]> σ')) as (Hheap) "(Hh● & Hℓ◯ & _)".
iDestruct (big_sepM_lookup _ _ with "Hℓ◯") as "Hℓ◯".
{ 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● _]".
(* 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 Σ _ Hheap) _ _ _ γ1 γ2)
as HtrHeapG.
(* create the invariant: *)
iAssert (|={}=> TR_invariant nmax)%I with "[Hℓ◯ Hγ1● Hγ2●]" as "> Hinv".
{
iApply inv_alloc.
iExists 0%nat. rewrite (_ : nmax - 0 - 1 = Z.of_nat (nmax - 1)) ; last lia.
unfold mapsto ; destruct mapsto_aux as [_ ->] ; simpl. by iFrame.
by iFrame.
}
iModIntro.
(* finally, use the user-given specification: *)
iExists (λ σ _, gen_heap_interp σ), (λ _, True%I). iSplitL "H Hh●".
- iExists . auto with iFrame.
- iApply (Hspec with "Hinv") ; auto.
iExists (λ σ _, gen_heap_interp σ), (λ _, True%I). iFrame.
iApply (Hspec with "Hinv") ; auto.
Qed.
Theorem spec_trtranslation__nadequate {Σ} nmax φ e :
......
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