Commit fa84d536 authored by Ralf Jung's avatar Ralf Jung
Browse files

update dependencies

parent 482553f5
......@@ -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-05-07.0.5119ab8b") | (= "dev") }
"coq-iris" { (= "dev.2021-06-03.0.2959900d") | (= "dev") }
"coq-tlc" { (= "20200328") | (= "dev") }
]
......@@ -23,7 +23,7 @@ Implicit Type Σ : gFunctors.
(* Ideally, this would be represented as a record (or a typeclass), but it has
* to be an Iris proposition (iProp Σ) and not a Coq proposition (Prop). *)
Definition TCTR_interface `{irisG heap_lang Σ, Tick}
Definition TCTR_interface `{irisGS heap_lang Σ, Tick}
(TC : nat iProp Σ)
(max_tr : nat)
(TR : nat iProp Σ)
......@@ -52,7 +52,7 @@ Definition TCTR_interface `{irisG heap_lang Σ, Tick}
*)
Class tctrHeapPreG Σ := {
tctrHeapPreG_heapPreG :> heapPreG Σ ;
tctrHeapPreG_heapPreG :> heapGpreS Σ ;
tctrHeapPreG_inG_TC :> inG Σ (authR natUR) ;
tctrHeapPreG_inG_TR :> inG Σ (authR natUR) ;
tctrHeapPreG_inG_TRdup :> inG Σ (authR max_natUR) ;
......@@ -61,7 +61,7 @@ Class tctrHeapPreG Σ := {
Class UseTC := useTC : bool.
Class tctrHeapG Σ := {
tctrHeapG_heapG :> heapG Σ ;
tctrHeapG_heapG :> heapGS Σ ;
tctrHeapG_inG_TC :> inG Σ (authR natUR) ;
tctrHeapG_inG_TR :> inG Σ (authR natUR) ;
tctrHeapG_inG_TRdup :> inG Σ (authR max_natUR) ;
......@@ -837,7 +837,7 @@ Section Soundness.
iMod (auth_nat_alloc (max_tr-1-M)) as (γ1) "[Hγ1● _]".
iMod (auth_max_nat_alloc (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 Σ _ Hheap) _ _ _ _ γ γ1 γ2 _)
pose (Build_tctrHeapG Σ (HeapGS Σ _ Hheap) _ _ _ _ γ γ1 γ2 _)
as HtcHeapG.
(* create the invariant: *)
iAssert (|={}=> TCTR_invariant max_tr)%I with "[Hℓ◯ Hγ● Hγ1● Hγ2●]" as "> Hinv".
......@@ -880,7 +880,7 @@ Section Soundness.
(* abstract version of the theorem. *)
Theorem tctr_sound_abstract {Σ} max_tr m φ e :
(0 < max_tr)%nat
( `{heapG Σ, Tick} (TC TR TRdup : nat iProp Σ),
( `{heapGS Σ, Tick} (TC TR TRdup : nat iProp Σ),
TCTR_interface TC max_tr TR TRdup -
{{{ TC m }}} «e» {{{ v, RET v ; ⌜φ (invtranslationV v) }}}
)
......
......@@ -16,7 +16,7 @@ Definition sum_list : val :=
end.
(** Representation predicate in separation logic for a list of integers [l]: *)
Fixpoint is_list `{heapG Σ} (l : list Z) (v : val) : iProp Σ :=
Fixpoint is_list `{heapGS Σ} (l : list Z) (v : val) : iProp Σ :=
match l with
| [] => v = NONEV
| x :: l' => (p : loc), v = SOMEV #p
......@@ -100,7 +100,7 @@ Definition sum_list_coq (l : list Z) : Z :=
fold_right Z.add 0 l.
(** The proof using induction over [l]: *)
Lemma sum_list_spec `{!heapG Σ} (l : list Z) (v : val) :
Lemma sum_list_spec `{!heapGS Σ} (l : list Z) (v : val) :
{{{ is_list l v }}} sum_list v {{{ RET #(sum_list_coq l) ; is_list l v }}}.
Proof.
iIntros (Φ) "Hl Post".
......@@ -153,7 +153,7 @@ Fixpoint make_list_coq (n : nat) : list Z :=
end.
(** The proof using induction over [l]: *)
Lemma make_list_spec `{!heapG Σ} (n : nat) :
Lemma make_list_spec `{!heapGS Σ} (n : nat) :
{{{ True }}} make_list #n {{{ v, RET v ; is_list (make_list_coq n) v }}}.
Proof.
iIntros (Φ) "_ Post".
......@@ -217,7 +217,7 @@ Proof.
lia.
Qed.
Lemma prgm_spec `{!heapG Σ} (n : nat) :
Lemma prgm_spec `{!heapGS Σ} (n : nat) :
{{{ True }}} prgm n {{{ v, RET v ; v = #(n*(n+1)/2) }}}.
Proof.
iIntros (Φ) "_ Post".
......
......@@ -24,7 +24,7 @@ Implicit Type Σ : gFunctors.
(* Ideally, this would be represented as a record (or a typeclass), but it has
* to be an Iris proposition (iProp Σ) and not a Coq proposition (Prop). *)
Definition TC_interface `{!irisG heap_lang Σ, Tick}
Definition TC_interface `{!irisGS heap_lang Σ, Tick}
(TC : nat iProp Σ)
: iProp Σ := (
n, Timeless (TC n)
......@@ -40,12 +40,12 @@ Definition TC_interface `{!irisG heap_lang Σ, Tick}
*)
Class timeCreditHeapPreG Σ := {
timeCreditHeapPreG_heapPreG :> heapPreG Σ ;
timeCreditHeapPreG_heapPreG :> heapGpreS Σ ;
timeCreditHeapPreG_inG :> inG Σ (authR natUR) ;
}.
Class timeCreditHeapG Σ := {
timeCreditHeapG_heapG :> heapG Σ ;
timeCreditHeapG_heapG :> heapGS Σ ;
timeCreditHeapG_inG :> inG Σ (authR natUR) ;
timeCreditHeapG_loc :> TickCounter ;
timeCreditHeapG_name : gname ;
......@@ -424,7 +424,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 Σ _ Hheap) _ _ γ)
pose (Build_timeCreditHeapG Σ (HeapGS Σ _ Hheap) _ _ γ)
as HtcHeapG.
(* create the invariant: *)
iAssert (|={}=> TC_invariant)%I with "[Hℓ◯ Hγ●]" as "> Hinv".
......@@ -454,7 +454,7 @@ Section Soundness.
(* The abstract version of the theorem: *)
Theorem abstract_spec_tctranslation__adequate_and_bounded {Σ} m φ e :
( `{heapG Σ, Tick} (TC : nat iProp Σ),
( `{heapGS Σ, Tick} (TC : nat iProp Σ),
TC_interface TC -
{{{ TC m }}} «e» {{{ v, RET v ; ⌜φ (invtranslationV v) }}}
)
......@@ -525,7 +525,7 @@ Section Tactics.
(*
(* TODO: abstract version: *)
Lemma tac_wp_tick_abstr `{heapG Σ} (TC : nat → iProp Σ) (tick : val) Δ Δ' Δ'' s E i j n K e (v : val) Φ :
Lemma tac_wp_tick_abstr `{heapGS Σ} (TC : nat → iProp Σ) (tick : val) Δ Δ' Δ'' s E i j n K e (v : val) Φ :
MaybeIntoLaterNEnvs 1 Δ Δ' →
envs_lookup i Δ' = Some (true, ∀ (v : val), {{{ TC 1%nat }}} tick v @ s ; E {{{ RET v ; True }}})%I →
envs_lookup j Δ' = Some (false, TC (S n)) →
......
......@@ -253,7 +253,7 @@ 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 Hheap) HinG _ γ)
pose (Build_timeCreditHeapG Σ (HeapGS Σ HinvG Hheap) HinG _ γ)
as HtcHeapG.
(* create the invariant: *)
iAssert (|={}=> TC_invariant)%I with "[Hℓ◯ Hγ●]" as "> #Hinv".
......
......@@ -22,7 +22,7 @@ Implicit Type Σ : gFunctors.
(* Ideally, this would be represented as a record (or a typeclass), but it has
* to be an Iris proposition (iProp Σ) and not a Coq proposition (Prop). *)
Definition TR_interface `{irisG heap_lang Σ, Tick}
Definition TR_interface `{irisGS heap_lang Σ, Tick}
(nmax : nat)
(TR : nat iProp Σ)
(TRdup : nat iProp Σ)
......@@ -47,13 +47,13 @@ Definition TR_interface `{irisG heap_lang Σ, Tick}
*)
Class timeReceiptHeapPreG Σ := {
timeReceiptHeapPreG_heapPreG :> heapPreG Σ ;
timeReceiptHeapPreG_heapPreG :> heapGpreS Σ ;
timeReceiptHeapPreG_inG1 :> inG Σ (authR natUR) ;
timeReceiptHeapPreG_inG2 :> inG Σ (authR max_natUR) ;
}.
Class timeReceiptHeapG Σ := {
timeReceiptHeapG_heapG :> heapG Σ ;
timeReceiptHeapG_heapG :> heapGS Σ ;
timeReceiptHeapG_inG1 :> inG Σ (authR natUR) ;
timeReceiptHeapG_inG2 :> inG Σ (authR max_natUR) ;
timeReceiptHeapG_loc :> TickCounter ;
......@@ -313,7 +313,7 @@ Section Soundness.
iMod (auth_nat_alloc 0) as (γ1) "[Hγ1● _]".
iMod (auth_max_nat_alloc 0) as (γ2) "[Hγ2● _]".
(* packing all those bits, build the heap instance necessary to use time receipts: *)
pose (Build_timeReceiptHeapG Σ (HeapG Σ _ Hheap) _ _ _ γ1 γ2)
pose (Build_timeReceiptHeapG Σ (HeapGS Σ _ Hheap) _ _ _ γ1 γ2)
as HtrHeapG.
(* create the invariant: *)
iAssert (|={}=> TR_invariant nmax)%I with "[Hℓ◯ Hγ1● Hγ2●]" as "> Hinv".
......@@ -344,7 +344,7 @@ Section Soundness.
Theorem abstract_spec_trtranslation__nadequate {Σ} nmax φ e :
(0 < nmax)%nat
( `{heapG Σ, Tick} (TR TRdup : nat iProp Σ),
( `{heapGS Σ, Tick} (TR TRdup : nat iProp Σ),
TR_interface nmax TR TRdup -
{{{ True }}} «e» {{{ v, RET v ; ⌜φ (invtranslationV v) }}}
)
......
......@@ -4,22 +4,22 @@ From iris_time.heap_lang Require Import proofmode notation.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
Class heapPreG Σ := HeapPreG {
heap_preG_iris :> invPreG Σ;
heap_preG_heap :> gen_heapPreG loc val Σ
Class heapGpreS Σ := HeapGpreS {
heap_preG_iris :> invGpreS Σ;
heap_preG_heap :> gen_heapGpreS loc val Σ
}.
Definition heapΣ : gFunctors := #[invΣ; gen_heapΣ loc val].
Instance subG_heapPreG {Σ} : subG heapΣ Σ heapPreG Σ.
Instance subG_heapPreG {Σ} : subG heapΣ Σ heapGpreS Σ.
Proof. solve_inG. Qed.
Definition heap_adequacy Σ `{heapPreG Σ} s e σ φ :
( `{heapG Σ}, WP e @ s; {{ v, ⌜φ v }})
Definition heap_adequacy Σ `{heapGpreS Σ} s e σ φ :
( `{heapGS Σ}, WP e @ s; {{ v, ⌜φ v }})
adequate s e σ (λ v _, φ v).
Proof.
intros Hwp; eapply (wp_adequacy _ _); iIntros (??) "".
iMod (gen_heap_init σ) as (?) "[Hh _]".
iModIntro.
iExists (λ σ κs, (gen_heap_interp σ)%I), (λ _, True%I). iFrame.
iApply (Hwp (HeapG _ _ _)).
iApply (Hwp (HeapGS _ _ _)).
Qed.
......@@ -9,7 +9,7 @@ Definition assert : val :=
(* just below ;; *)
Notation "'assert:' e" := (assert (λ: <>, e))%E (at level 99) : expr_scope.
Lemma wp_assert `{heapG Σ} E (Φ : val iProp Σ) e :
Lemma wp_assert `{heapGS Σ} E (Φ : val iProp Σ) e :
WP e @ E {{ v, v = #true Φ #() }} -
WP assert (LamV BAnon e)%V @ E {{ Φ }}.
Proof.
......
......@@ -8,12 +8,12 @@ From iris.proofmode Require Import tactics.
From stdpp Require Import fin_maps.
Set Default Proof Using "Type".
Class heapG Σ := HeapG {
heapG_invG : invG Σ;
heapG_gen_heapG :> gen_heapG loc val Σ
Class heapGS Σ := HeapGS {
heapG_invG : invGS Σ;
heapG_gen_heapG :> gen_heapGS loc val Σ
}.
Instance heapG_irisG `{heapG Σ} : irisG heap_lang Σ := {
Instance heapG_irisG `{heapGS Σ} : irisGS heap_lang Σ := {
iris_invG := heapG_invG;
state_interp σ _ κs _ := gen_heap_interp σ;
num_laters_per_step _ := 0%nat;
......@@ -146,7 +146,7 @@ Global Instance pure_case_inr v e1 e2 :
Proof. solve_pure_exec. Qed.
Section lifting.
Context `{heapG Σ}.
Context `{heapGS Σ}.
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val iProp Σ.
Implicit Types efs : list expr.
......
......@@ -6,7 +6,7 @@ From iris_time.heap_lang Require Import notation.
Set Default Proof Using "Type".
Import uPred.
Lemma tac_wp_expr_eval `{heapG Σ} Δ s E Φ e e' :
Lemma tac_wp_expr_eval `{heapGS Σ} Δ s E Φ e e' :
( (e'':=e'), e = e'')
envs_entails Δ (WP e' @ s; E {{ Φ }}) envs_entails Δ (WP e @ s; E {{ Φ }}).
Proof. by intros ->. Qed.
......@@ -22,7 +22,7 @@ Tactic Notation "wp_expr_eval" tactic(t) :=
Ltac wp_expr_simpl := wp_expr_eval simpl.
Lemma tac_wp_pure `{heapG Σ} Δ Δ' s E K e1 e2 φ n Φ :
Lemma tac_wp_pure `{heapGS Σ} Δ Δ' s E K e1 e2 φ n Φ :
PureExec φ n e1 e2
φ
MaybeIntoLaterNEnvs n Δ Δ'
......@@ -35,7 +35,7 @@ Proof.
rewrite HΔ' -lifting.wp_pure_step_later //.
Qed.
Lemma tac_wp_value `{heapG Σ} Δ s E Φ v :
Lemma tac_wp_value `{heapGS Σ} Δ s E Φ v :
envs_entails Δ (Φ v) envs_entails Δ (WP (Val v) @ s; E {{ Φ }}).
Proof. rewrite envs_entails_eq=> ->. by apply wp_value. Qed.
......@@ -95,7 +95,7 @@ Tactic Notation "wp_inj" := wp_pure (InjL _) || wp_pure (InjR _).
Tactic Notation "wp_pair" := wp_pure (Pair _ _).
Tactic Notation "wp_closure" := wp_pure (Rec _ _ _).
Lemma tac_wp_bind `{heapG Σ} K Δ s E Φ e f :
Lemma tac_wp_bind `{heapGS Σ} K Δ s E Φ e f :
f = (λ e, fill K e) (* as an eta expanded hypothesis so that we can `simpl` it *)
envs_entails Δ (WP e @ s; E {{ v, WP f (Val v) @ s; E {{ Φ }} }})%I
envs_entails Δ (WP fill K e @ s; E {{ Φ }}).
......@@ -118,7 +118,7 @@ Tactic Notation "wp_bind" open_constr(efoc) :=
(** Heap tactics *)
Section heap.
Context `{WordSize, heapG Σ}.
Context `{WordSize, heapGS Σ}.
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val iProp Σ.
Implicit Types Δ : envs (uPredI (iResUR Σ)).
......
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