Attention une mise à jour du serveur va être effectuée le vendredi 16 avril entre 12h et 12h30. Cette mise à jour va générer une interruption du service de quelques minutes.

Commit 872a1cb1 authored by Ralf Jung's avatar Ralf Jung

update dependencies; fix for gen_heap internal changes

parent 983e44bd
......@@ -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-10.0.cb8e35b8") | (= "dev") }
"coq-iris" { (= "dev.2020-10-13.1.5558d66d") | (= "dev") }
"coq-tlc" { (= "20181116") | (= "dev") }
]
From iris_time Require Import Base.
From iris.base_logic Require Import invariants.
From iris.algebra Require Import lib.gmap_view.
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_max_nat Reduction Tactics.
......@@ -832,20 +833,14 @@ 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 ( to_gen_heap (<[ := #M]> σ') to_gen_heap {[ := #M]}))
iMod (own_alloc (gmap_view_auth (<[ := #M]> σ') gmap_view_frag (DfracOwn 1) #M))
as (h) "[Hh● Hℓ◯]".
{
apply auth_both_valid ; split.
- rewrite - insert_delete ; set σ'' := delete σ'.
unfold to_gen_heap ; rewrite 2! fmap_insert fmap_empty insert_empty.
exists (to_gen_heap σ'').
rewrite (@gmap.insert_singleton_op _ _ _ _ (to_gen_heap σ'')) //.
rewrite lookup_fmap ; apply fmap_None, lookup_delete.
- apply to_gen_heap_valid.
{ apply gmap_view_both_valid_L. split; first done.
rewrite lookup_insert. done.
}
(* allocate the meta-heap: *)
iMod (own_alloc ( to_gen_meta )) as (γmeta) "H" ;
first by apply auth_auth_valid, to_gen_meta_valid.
iMod (own_alloc (gmap_view_auth (V:=gnameO) )) as (γmeta) "H" ;
first by apply gmap_view_auth_valid.
(* allocate the ghost state associated with ℓ: *)
iAssert (|==> γ,
(if useTC then own γ ( M) else True)
......@@ -868,9 +863,7 @@ Section Soundness.
{
iApply inv_alloc.
iExists M.
unfold mapsto ; destruct mapsto_aux as [_ ->] ; simpl.
unfold to_gen_heap ; rewrite fmap_insert fmap_empty insert_empty.
by iFrame.
unfold mapsto ; destruct mapsto_aux as [_ ->] ; simpl. by iFrame.
}
iIntros (?) "!>".
(* finally, use the user-given specification: *)
......
From iris_time Require Import Base.
From iris.base_logic Require Import invariants.
From iris.algebra Require Import lib.gmap_view.
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 Reduction Tactics.
......@@ -421,20 +422,14 @@ 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 ( to_gen_heap (<[ := #k]> σ') to_gen_heap {[ := #k]}))
iMod (own_alloc (gmap_view_auth (<[ := #k]> σ') gmap_view_frag (DfracOwn 1) #k))
as (h) "[Hh● Hℓ◯]".
{
apply auth_both_valid ; split.
- rewrite - insert_delete ; set σ'' := delete σ'.
unfold to_gen_heap ; rewrite 2! fmap_insert fmap_empty insert_empty.
exists (to_gen_heap σ'').
rewrite (@gmap.insert_singleton_op _ _ _ _ (to_gen_heap σ'')) //.
rewrite lookup_fmap ; apply fmap_None, lookup_delete.
- apply to_gen_heap_valid.
{ apply gmap_view_both_valid_L. split; first done.
rewrite lookup_insert. done.
}
(* allocate the meta-heap: *)
iMod (own_alloc ( to_gen_meta )) as (γmeta) "H" ;
first by apply auth_auth_valid, to_gen_meta_valid.
iMod (own_alloc (gmap_view_auth (V:=gnameO) )) as (γmeta) "H" ;
first by apply gmap_view_auth_valid.
(* 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: *)
......@@ -445,9 +440,7 @@ Section Soundness.
{
iApply inv_alloc.
iExists k.
unfold mapsto ; destruct mapsto_aux as [_ ->] ; simpl.
unfold to_gen_heap ; rewrite fmap_insert fmap_empty insert_empty.
by iFrame.
unfold mapsto ; destruct mapsto_aux as [_ ->] ; simpl. by iFrame.
}
iIntros (?) "!>".
(* finally, use the user-given specification: *)
......
From iris.base_logic Require Import invariants.
From iris.algebra Require Import lib.gmap_view.
From iris_time.heap_lang Require Import proofmode notation adequacy lang.
From iris_time Require Import Auth_nat Reduction.
From iris_time Require Export TimeCredits.
......@@ -236,12 +237,9 @@ Lemma gen_heap_ctx_mapsto {Σ : gFunctors} {Hgen : gen_heapG loc val Σ} (σ : s
Proof.
iIntros (Hσ) "Hheap Hl". iDestruct "Hheap" as (hmeta) "(_ & Hheap & _)".
unfold mapsto ; destruct mapsto_aux as [_->] ; rewrite /mapsto_def /=.
iDestruct (own_valid_2 with "Hheap Hl") as %H.
iPureIntro.
assert (CmraDiscrete (gen_heapUR loc val)) as Hdiscrete by apply _.
apply auth_both_valid_discrete in H as [H _].
apply gen_heap_singleton_included in H.
pose proof (eq_stepl Hσ H) as E. by injection E.
iDestruct (own_valid_2 with "Hheap Hl") as %H%gmap_view_both_valid_L.
iPureIntro. rewrite Hσ in H.
destruct H as [_ [= ->]]. done.
Qed.
Lemma spec_tctranslation__bounded {Σ} m ψ e :
......@@ -261,20 +259,14 @@ 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 ( to_gen_heap (<[ := #m]> σ') to_gen_heap {[ := #m]}))
iMod (own_alloc (gmap_view_auth (<[ := #m]> σ') gmap_view_frag (DfracOwn 1) #m))
as (h) "[Hh● Hℓ◯]".
{
apply auth_both_valid ; split.
- rewrite - insert_delete ; set σ'' := delete σ'.
unfold to_gen_heap ; rewrite 2! fmap_insert fmap_empty insert_empty.
exists (to_gen_heap σ'').
rewrite (@gmap.insert_singleton_op _ _ _ _ (to_gen_heap σ'')) //.
rewrite lookup_fmap ; apply fmap_None, lookup_delete.
- apply to_gen_heap_valid.
{ apply gmap_view_both_valid_L. split; first done.
rewrite lookup_insert. done.
}
(* allocate the meta-heap: *)
iMod (own_alloc ( to_gen_meta )) as (γmeta) "H" ;
first by apply auth_auth_valid, to_gen_meta_valid.
iMod (own_alloc (gmap_view_auth (V:=gnameO) )) as (γmeta) "H" ;
first by apply gmap_view_auth_valid.
(* 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: *)
......@@ -286,9 +278,7 @@ Proof.
{
iApply inv_alloc.
iExists m.
unfold mapsto ; destruct mapsto_aux as [_ ->] ; simpl.
unfold to_gen_heap ; rewrite fmap_insert fmap_empty insert_empty.
by iFrame.
unfold mapsto ; destruct mapsto_aux as [_ ->] ; simpl. by iFrame.
}
(* finally, use the user-given specification: *)
iModIntro.
......
From iris.base_logic Require Import invariants.
From iris.proofmode Require Import coq_tactics.
From iris.algebra Require Import lib.gmap_view.
From iris_time.heap_lang Require Import proofmode notation adequacy lang.
From iris_time Require Import Auth_nat Auth_max_nat Reduction Tactics.
From iris_time Require Export Simulation.
......@@ -318,20 +319,14 @@ 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 ( to_gen_heap (<[ := #(nmax-1)%nat]> σ') to_gen_heap {[ := #(nmax-1)%nat]}))
iMod (own_alloc (gmap_view_auth (<[ := #(nmax-1)%nat]> σ') gmap_view_frag (DfracOwn 1) #(nmax-1)%nat))
as (h) "[Hh● Hℓ◯]".
{
apply auth_both_valid ; split.
- rewrite - insert_delete ; set σ'' := delete σ'.
unfold to_gen_heap ; rewrite 2! fmap_insert fmap_empty insert_empty.
exists (to_gen_heap σ'').
rewrite (@gmap.insert_singleton_op _ _ _ _ (to_gen_heap σ'')) //.
rewrite lookup_fmap ; apply fmap_None, lookup_delete.
- apply to_gen_heap_valid.
{ apply gmap_view_both_valid_L. split; first done.
rewrite lookup_insert. done.
}
(* allocate the meta-heap: *)
iMod (own_alloc ( to_gen_meta )) as (γmeta) "H" ;
first by apply auth_auth_valid, to_gen_meta_valid.
iMod (own_alloc (gmap_view_auth (V:=gnameO) )) as (γmeta) "H" ;
first by apply gmap_view_auth_valid.
(* 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● _]".
......@@ -343,9 +338,7 @@ Section Soundness.
{
iApply inv_alloc.
iExists 0%nat. rewrite (_ : nmax - 0 - 1 = Z.of_nat (nmax - 1)) ; last lia.
unfold mapsto ; destruct mapsto_aux as [_ ->] ; simpl.
unfold to_gen_heap ; rewrite fmap_insert fmap_empty insert_empty.
by iFrame.
unfold mapsto ; destruct mapsto_aux as [_ ->] ; simpl. by iFrame.
}
iModIntro.
(* finally, use the user-given specification: *)
......
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