Commit c6057c67 authored by Glen Mével's avatar Glen Mével

abstract interfaces for time credits and time receipts

parent 4a6c8d5f
......@@ -16,6 +16,24 @@ Implicit Type m n : nat.
(*
* Abstract interface of time credits
*)
(* 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 Σ}
(TC : nat iProp Σ)
(tick : val)
: iProp Σ := (
⌜∀ n, Timeless (TC n)
(|={}=> TC 0%nat)
⌜∀ m n, TC (m + n)%nat (TC m TC n)
( v, {{{ TC 1%nat }}} tick v {{{ RET v ; True }}})
)%I.
(*
* Prerequisites on the global monoid Σ
*)
......@@ -54,10 +72,6 @@ Section Tick.
Definition fail : val :=
λ: <>, #() #().
(*
Definition tick : val :=
λ: "x", if: ! # < #1 then fail #() else (FAA # (- #1) ;; "x").
*)
Definition tick : val :=
tick fail .
......@@ -87,7 +101,7 @@ Section TickSpec.
Timeless (TC n).
Proof. exact _. Qed.
(* note: IntoAnd false will become IntoSep *)
(* note: IntoAnd false will become IntoSep in a future version of Iris *)
Global Instance into_sep_TC_plus m n p : IntoAnd p (TC (m + n)) (TC m) (TC n).
Proof. rewrite /IntoAnd TC_plus ; iIntros "[Hm Hn]". destruct p ; iFrame. Qed.
Global Instance from_sep_TC_plus m n : FromAnd false (TC (m + n)) (TC m) (TC n).
......@@ -168,6 +182,15 @@ Section TickSpec.
by iApply (tick_spec with "Hinv [HTC//] HΨ").
Qed.
Lemma TC_implementation : TICKCTXT - TC_interface TC tick.
Proof.
iIntros "#Hinv". iSplit ; last iSplit ; last iSplit.
- iPureIntro. by apply TC_timeless.
- by iApply (zero_TC with "Hinv").
- iPureIntro. by apply TC_plus.
- iIntros (v). by iApply (tick_spec_simple with "Hinv").
Qed.
End TickSpec.
......@@ -563,7 +586,7 @@ Section Soundness.
TICKCTXT -
{{{ TC m }}} «e» {{{ v, RET v ; ⌜φ (invtranslationV v) }}}
)
`{timeCreditHeapPreG Σ} σ,
{_ : timeCreditHeapPreG Σ} σ,
adequate NotStuck e σ φ bounded_time e σ m.
Proof.
intros Hclosed Hspec HpreG σ.
......@@ -574,24 +597,16 @@ Section Soundness.
Theorem abstract_spec_tctranslation__adequate_and_bounded {Σ} m (φ : val Prop) e :
is_closed [] e
( `{heapG Σ} (TC : nat iProp Σ) (tick : val),
( m n, TC (m + n)%nat (TC m TC n)%I)
( n, Timeless (TC n))
( v, {{{ TC 1%nat }}} tick v {{{ RET v ; True }}}) -
TC_interface TC tick -
{{{ TC m }}} translation tick e {{{ v, RET v ; ⌜φ (invtranslationV v) }}}
)
{_ : heapPreG Σ} {_ : inG Σ (authR natUR)} σ,
{_ : timeCreditHeapPreG Σ} σ,
adequate NotStuck e σ φ bounded_time e σ m.
Proof.
intros Hclosed Hspec HpreG HinG σ.
(* a record of type (timeCreditHeapPreG Σ) is inferred from HpreG and HinG: *)
intros Hclosed Hspec HpreG σ.
eapply spec_tctranslation__adequate_and_bounded ; try done.
clear HpreG HinG.
intros HtcHeapG.
specialize (Hspec _ TC tick).
iIntros "#Hinv".
iApply Hspec.
- exact TC_plus.
- iIntros (v). iApply (tick_spec_simple with "Hinv").
clear HpreG. iIntros (HtcHeapG) "#Hinv".
iApply Hspec. by iApply TC_implementation.
Qed.
End Soundness.
......
......@@ -32,6 +32,33 @@ Implicit Type m n : nat.
(*
* Abstract interface of time receipts
*)
(* 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 Σ}
(nmax : nat)
(TR : nat iProp Σ)
(TRdup : nat iProp Σ)
(tick : val)
: iProp Σ := (
⌜∀ n, Timeless (TR n)
⌜∀ n, Timeless (TRdup n)
⌜∀ n, Persistent (TRdup n)
( n, TR n ={}= TR n TRdup n)
(|={}=> TR 0%nat)
(* (|={}=> TRdup 0%nat) *)
⌜∀ m n, TR (m + n)%nat (TR m TR n)
⌜∀ m n, TRdup (m `max` n) (TRdup m TRdup n)
(* (TR nmax ={}= False) *)
(TRdup nmax ={}= False)
( v n, {{{ TRdup n }}} tick v {{{ RET v ; TR 1%nat TRdup (n+1)%nat }}})
)%I.
(*
* Prerequisites on the global monoid Σ
*)
......@@ -118,6 +145,9 @@ Section TockSpec.
Lemma TRdup_timeless n :
Timeless (TRdup n).
Proof. exact _. Qed.
Lemma TRdup_persistent n :
Persistent (TRdup n).
Proof. exact _. Qed.
(* note: IntoAnd false will become IntoSep in a future version of Iris *)
Global Instance into_sep_TRdup_max m n p : IntoAnd p (TRdup (m `max` n)) (TRdup m) (TRdup n).
......@@ -130,6 +160,24 @@ Section TockSpec.
Definition TOCKCTXT (nmax : nat) : iProp Σ :=
inv timeReceiptN ( (n:nat), #(nmax-n-1) own γ1 (nat n) own γ2 (mnat n) (n < nmax)%nat)%I.
Lemma zero_TR (nmax : nat) :
TOCKCTXT nmax ={}= TR 0.
Proof.
iIntros "#Htockinv".
iInv timeReceiptN as (m) ">(Hcounter & Hγ1● & H)" "Hclose".
iDestruct (own_auth_nat_null with "Hγ1●") as "[Hγ1● $]".
iApply "Hclose" ; eauto with iFrame.
Qed.
Lemma zero_TRdup (nmax : nat) :
TOCKCTXT nmax ={}= TRdup 0.
Proof.
iIntros "#Htockinv".
iInv timeReceiptN as (m) ">(Hcounter & Hγ1● & Hγ2● & Im)" "Hclose".
iDestruct (own_auth_mnat_null with "Hγ2●") as "[Hγ2● $]".
iApply "Hclose" ; eauto with iFrame.
Qed.
Lemma TR_nmax_absurd (nmax : nat) (E : coPset) :
timeReceiptN E
TOCKCTXT nmax - TR nmax ={E}= False.
......@@ -140,6 +188,16 @@ Section TockSpec.
exfalso ; lia.
Qed.
Lemma TRdup_nmax_absurd (nmax : nat) (E : coPset) :
timeReceiptN E
TOCKCTXT nmax - TRdup nmax ={E}= False.
Proof.
iIntros (?) "#Inv Hγ2◯".
iInv timeReceiptN as (n) ">(Hℓ & Hγ1● & Hγ2● & In)" "InvClose" ; iDestruct "In" as %In.
iDestruct (own_auth_mnat_le with "Hγ2● Hγ2◯") as %In'.
exfalso ; lia.
Qed.
Lemma TR_TRdup (nmax : nat) (E : coPset) (n : nat) :
timeReceiptN E
TOCKCTXT nmax - TR n ={E}= TR n TRdup n.
......@@ -161,13 +219,13 @@ Section TockSpec.
iLöb as "IH". wp_rec. iExact "IH".
Qed.
Theorem tock_spec (nmax : nat) s E e v :
Theorem tock_spec (nmax : nat) s E e v m :
timeReceiptN E
IntoVal e v
TOCKCTXT nmax -
{{{ True }}} tock e @ s ; E {{{ RET v ; TR 1 }}}.
{{{ TRdup m }}} tock e @ s ; E {{{ RET v ; TR 1 TRdup (m+1) }}}.
Proof.
intros ? <- % of_to_val. iIntros "#Inv" (Ψ) "!# _ HΨ".
intros ? <- % of_to_val. iIntros "#Inv" (Ψ) "!# Hγ2◯ HΨ".
iLöb as "IH".
wp_lam.
(* open the invariant, in order to read the value k = nmaxn1 of location : *)
......@@ -196,29 +254,44 @@ Section TockSpec.
receipt produced: *)
replace (nmax - n - 1 - 1) with (nmax - (n+1)%nat - 1) by lia.
iMod (auth_nat_update_incr _ _ 1 with "Hγ1●") as "[Hγ1● Hγ1◯]" ; simpl.
iMod (auth_mnat_update_incr _ _ 1 with "Hγ2●") as "Hγ2●" ; simpl.
(* iMod (auth_mnat_update_incr _ _ 1 with "Hγ2●") as "Hγ2●" ; simpl. *)
iMod (auth_mnat_update_incr' _ _ _ 1 with "Hγ2● Hγ2◯") as "[Hγ2● Hγ2◯]" ; simpl.
assert ((n+1) < nmax)%nat by lia.
(* close the invariant: *)
iMod ("InvClose" with "[ Hℓ Hγ1● Hγ2● ]") as "_" ; [ by auto with iFrame | iModIntro ].
(* finish: *)
wp_if. iApply "HΨ" ; iExact "Hγ1◯".
wp_if. iApply "HΨ" ; by iFrame.
(* otherwise, CAS fails and is unchanged: *)
+ wp_cas_fail ; first (injection ; lia).
(* close the invariant as is: *)
iMod ("InvClose" with "[ Hℓ Hγ1● Hγ2● ]") as "_" ; [ by auto with iFrame | iModIntro ] ; clear dependent n.
wp_if.
(* conclude using the induction hypothesis: *)
iApply ("IH" with "HΨ").
iApply ("IH" with "Hγ2◯ HΨ").
Qed.
Theorem tock_spec_simple (nmax : nat) v :
Theorem tock_spec_simple (nmax : nat) v (n : nat) :
TOCKCTXT nmax -
{{{ True }}} tock v {{{ RET v ; TR 1 }}}.
{{{ TRdup n }}} tock v {{{ RET v ; TR 1 TRdup (n+1) }}}.
Proof.
iIntros "#Inv" (Ψ) "!# H HΨ".
by iApply (tock_spec with "Inv H HΨ").
Qed.
Lemma TR_implementation (nmax : nat) : TOCKCTXT nmax - TR_interface nmax TR TRdup tock.
Proof.
iIntros "#Hinv". repeat iSplitR.
- iPureIntro. by apply TR_timeless.
- iPureIntro. by apply TRdup_timeless.
- iPureIntro. by apply TRdup_persistent.
- iIntros (n). by iApply (TR_TRdup with "Hinv").
- by iApply (zero_TR with "Hinv").
- iPureIntro. by apply TR_plus.
- iPureIntro. by apply TRdup_max.
- by iApply (TRdup_nmax_absurd with "Hinv").
- iIntros (v n). by iApply (tock_spec_simple with "Hinv").
Qed.
End TockSpec.
......@@ -347,6 +420,22 @@ Section Soundness.
intros Hloc. by eapply spec_trtranslation__adequate_translation.
Qed.
Lemma abstract_spec_trtranslation__adequate {Σ} (nmax : nat) (φ : val Prop) e :
(0 < nmax)%nat
is_closed [] e
( `{!heapG Σ} (TR TRdup : nat iProp Σ) (tick : val),
TR_interface nmax TR TRdup tick -
{{{ True }}} translation tick e {{{ v, RET v ; ⌜φ (invtranslationV v) }}}
)
{_ : timeReceiptHeapPreG Σ} σ,
adequate_n NotStuck (nmax-1) e σ φ.
Proof.
intros Inmax Hclosed Hspec HpreG σ.
eapply spec_trtranslation__adequate ; try done.
clear HpreG. iIntros (HtrHeapG) "#Hinv".
iApply Hspec. by iApply TR_implementation.
Qed.
End Soundness.
......
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