Commit 34c8f154 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Use tick only via its type class. Notation for tickmatch and ticklet.

parent 1090f98c
...@@ -62,11 +62,11 @@ Section snapclock_int. ...@@ -62,11 +62,11 @@ Section snapclock_int.
Lemma snapclock_int_incr_spec n1 : Lemma snapclock_int_incr_spec n1 :
TR_invariant nmax - TR_invariant nmax -
{{{ is_snapclock_int n1 }}} {{{ is_snapclock_int n1 }}}
tock #() ;; machine_int_add #n1 #1 tick #() ;; machine_int_add #n1 #1
{{{ RET #(n1+1) ; is_snapclock_int (n1+1) }}}. {{{ RET #(n1+1) ; is_snapclock_int (n1+1) }}}.
Proof. Proof.
iIntros "#Htrinv" (Φ) "!# H1 Post". iIntros "#Htrinv" (Φ) "!# H1 Post".
wp_apply (tock_spec_simple nmax #() with "Htrinv H1"). iIntros "(_ & H)". wp_apply (tick_spec_simple nmax #() with "Htrinv H1"). iIntros "(_ & H)".
iDestruct (TRdup_lt_nmax with "Htrinv H") as ">(H & %)" ; first done. iDestruct (TRdup_lt_nmax with "Htrinv H") as ">(H & %)" ; first done.
wp_seq. wp_seq.
wp_apply (machine_int_add_spec n1 1 with "[] [H Post]") . wp_apply (machine_int_add_spec n1 1 with "[] [H Post]") .
...@@ -98,4 +98,4 @@ Section snapclock_int. ...@@ -98,4 +98,4 @@ Section snapclock_int.
} }
Qed. Qed.
End snapclock_int. End snapclock_int.
\ No newline at end of file
...@@ -33,19 +33,15 @@ Context (runtime_error : val). ...@@ -33,19 +33,15 @@ Context (runtime_error : val).
* Definition of tick * Definition of tick
*) *)
Definition tick {Hloc : TickCounter} : val := Local Instance generic_tick {Hloc : TickCounter} : Tick :=
rec: "tick" "x" := (rec: "tick" "x" :=
let: "k" := ! # in let: "k" := ! # in
if: "k" #0 then if: "k" #0 then
runtime_error #() runtime_error #()
else if: CAS # "k" ("k" - #1) then else if: CAS # "k" ("k" - #1) then
"x" "x"
else else
"tick" "x". "tick" "x")%V.
Local Instance Tick_tick (Hloc: TickCounter) : Tick :=
{| Translation.tick := tick |}.
(* (*
...@@ -59,7 +55,7 @@ Section Tick_exec. ...@@ -59,7 +55,7 @@ Section Tick_exec.
Lemma exec_tick_success n v σ : Lemma exec_tick_success n v σ :
prim_exec (tick v) (<[ := #(S n)]> σ) v (<[ := #n]> σ) []. prim_exec (tick v) (<[ := #(S n)]> σ) v (<[ := #n]> σ) [].
Proof. Proof.
unlock tick. unlock tick generic_tick.
apply prim_exec_cons_nofork apply prim_exec_cons_nofork
with ( with (
let: "k" := ! # in let: "k" := ! # in
...@@ -72,7 +68,7 @@ Section Tick_exec. ...@@ -72,7 +68,7 @@ Section Tick_exec.
)%E (<[ := #(S n)]> σ). )%E (<[ := #(S n)]> σ).
{ {
prim_step ; first exact _. simpl_subst. repeat f_equal. prim_step ; first exact _. simpl_subst. repeat f_equal.
unfold tick. by unlock. } unfold tick, generic_tick. by unlock. }
apply prim_exec_cons_nofork apply prim_exec_cons_nofork
with ( with (
let: "k" := #(S n) in let: "k" := #(S n) in
......
...@@ -2,7 +2,7 @@ From iris.heap_lang Require Import proofmode notation adequacy lang. ...@@ -2,7 +2,7 @@ From iris.heap_lang Require Import proofmode notation adequacy lang.
From iris.base_logic Require Import invariants. From iris.base_logic Require Import invariants.
From iris_time Require Import Auth_nat Misc Reduction Tactics. From iris_time Require Import Auth_nat Misc Reduction Tactics.
From iris_time Require Export Translation Simulation. From iris_time Require Export Simulation.
From iris.proofmode Require Import coq_tactics. From iris.proofmode Require Import coq_tactics.
Import uPred. Import uPred.
...@@ -24,9 +24,8 @@ Implicit Type Σ : gFunctors. ...@@ -24,9 +24,8 @@ Implicit Type Σ : gFunctors.
(* Ideally, this would be represented as a record (or a typeclass), but it has (* 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). *) * to be an Iris proposition (iProp Σ) and not a Coq proposition (Prop). *)
Definition TC_interface `{!irisG heap_lang Σ} Definition TC_interface `{!irisG heap_lang Σ, Tick}
(TC : nat iProp Σ) (TC : nat iProp Σ)
(tick : val)
: iProp Σ := ( : iProp Σ := (
⌜∀ n, Timeless (TC n) ⌜∀ n, Timeless (TC n)
(|={}=> TC 0%nat) (|={}=> TC 0%nat)
...@@ -66,11 +65,8 @@ Local Notation ℓ := tick_counter. ...@@ -66,11 +65,8 @@ Local Notation ℓ := tick_counter.
Definition fail : val := Definition fail : val :=
λ: <>, #() #(). λ: <>, #() #().
Definition tick {_:TickCounter} : val := Global Instance credits_tick {_:TickCounter} : Tick :=
tick fail. generic_tick fail.
Global Instance Tick_tick (Hloc : TickCounter) : Tick :=
{| Translation.tick := tick |}.
...@@ -176,7 +172,7 @@ Section TickSpec. ...@@ -176,7 +172,7 @@ Section TickSpec.
by iApply (tick_spec with "Hinv [HTC//] HΨ"). by iApply (tick_spec with "Hinv [HTC//] HΨ").
Qed. Qed.
Lemma TC_implementation : TC_invariant - TC_interface TC tick. Lemma TC_implementation : TC_invariant - TC_interface TC.
Proof. Proof.
iIntros "#Hinv". iSplit ; last iSplit ; last iSplit. iIntros "#Hinv". iSplit ; last iSplit ; last iSplit.
- iPureIntro. by apply TC_timeless. - iPureIntro. by apply TC_timeless.
...@@ -221,7 +217,7 @@ Section Tick_lemmas. ...@@ -221,7 +217,7 @@ Section Tick_lemmas.
Proof. Proof.
assert (prim_exec (tick v) (<[ := #0]> σ) (#() #()) (<[ := #0]> σ) []) as Hexec. assert (prim_exec (tick v) (<[ := #0]> σ) (#() #()) (<[ := #0]> σ) []) as Hexec.
{ {
unlock tick Simulation.tick. unlock credits_tick generic_tick. simpl.
apply prim_exec_cons_nofork apply prim_exec_cons_nofork
with ( with (
let: "k" := ! # in let: "k" := ! # in
...@@ -234,7 +230,8 @@ Section Tick_lemmas. ...@@ -234,7 +230,8 @@ Section Tick_lemmas.
)%E (<[ := #0]> σ). )%E (<[ := #0]> σ).
{ {
prim_step ; first exact _. prim_step ; first exact _.
replace (rec: "tick" "x" := _)%E with (of_val tick) by by unlock tick Simulation.tick. replace (rec: "tick" "x" := _)%E with (of_val tick)
by by unfold tick, credits_tick, generic_tick; unlock.
unfold subst ; simpl ; fold subst. unfold subst ; simpl ; fold subst.
rewrite ! subst_is_closed_nil // ; apply is_closed_of_val. rewrite ! subst_is_closed_nil // ; apply is_closed_of_val.
} }
...@@ -552,9 +549,8 @@ Section Soundness. ...@@ -552,9 +549,8 @@ Section Soundness.
(* The abstract version of the theorem: *) (* The abstract version of the theorem: *)
Theorem abstract_spec_tctranslation__adequate_and_bounded {Σ} m φ e : Theorem abstract_spec_tctranslation__adequate_and_bounded {Σ} m φ e :
is_closed [] e is_closed [] e
( `{heapG Σ} (TC : nat iProp Σ) (tick : val), ( `{heapG Σ, Tick} (TC : nat iProp Σ),
let _ := {| Translation.tick := tick |} in TC_interface TC -
TC_interface TC tick -
{{{ TC m }}} «e» {{{ v, RET v ; ⌜φ (invtranslationV v) }}} {{{ TC m }}} «e» {{{ v, RET v ; ⌜φ (invtranslationV v) }}}
) )
{_ : timeCreditHeapPreG Σ} σ, {_ : timeCreditHeapPreG Σ} σ,
......
...@@ -21,11 +21,10 @@ Implicit Type Σ : gFunctors. ...@@ -21,11 +21,10 @@ Implicit Type Σ : gFunctors.
(* Ideally, this would be represented as a record (or a typeclass), but it has (* 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). *) * to be an Iris proposition (iProp Σ) and not a Coq proposition (Prop). *)
Definition TR_interface `{irisG heap_lang Σ} Definition TR_interface `{irisG heap_lang Σ, Tick}
(nmax : nat) (nmax : nat)
(TR : nat iProp Σ) (TR : nat iProp Σ)
(TRdup : nat iProp Σ) (TRdup : nat iProp Σ)
(tick : val)
: iProp Σ := ( : iProp Σ := (
⌜∀ n, Timeless (TR n) ⌜∀ n, Timeless (TR n)
⌜∀ n, Timeless (TRdup n) ⌜∀ n, Timeless (TRdup n)
...@@ -68,21 +67,16 @@ Local Notation ℓ := tick_counter. ...@@ -68,21 +67,16 @@ Local Notation ℓ := tick_counter.
(* (*
* Implementation and specification of `TR` and `tock` * Implementation and specification of `TR` and `tick`
*) *)
Definition loop : val := Definition loop : val :=
rec: "f" <> := "f" #(). rec: "f" <> := "f" #().
Definition tock {_:TickCounter} : val := Global Instance receipts_tick {_:TickCounter} : Tick :=
tick loop. generic_tick loop.
Global Instance Tick_tock (Hloc: TickCounter) : Tick := Section TickSpec.
{| Translation.tick := tock |}.
Section TockSpec.
Context `{timeReceiptHeapG Σ}. Context `{timeReceiptHeapG Σ}.
Context (nmax : nat). Context (nmax : nat).
...@@ -146,7 +140,7 @@ Section TockSpec. ...@@ -146,7 +140,7 @@ Section TockSpec.
Lemma zero_TR : Lemma zero_TR :
TR_invariant ={}= TR 0. TR_invariant ={}= TR 0.
Proof. Proof.
iIntros "#Htockinv". iIntros "#Htickinv".
iInv timeReceiptN as (m) ">(Hcounter & Hγ1● & H)" "Hclose". iInv timeReceiptN as (m) ">(Hcounter & Hγ1● & H)" "Hclose".
iDestruct (own_auth_nat_null with "Hγ1●") as "[Hγ1● $]". iDestruct (own_auth_nat_null with "Hγ1●") as "[Hγ1● $]".
iApply "Hclose" ; eauto with iFrame. iApply "Hclose" ; eauto with iFrame.
...@@ -155,7 +149,7 @@ Section TockSpec. ...@@ -155,7 +149,7 @@ Section TockSpec.
Lemma zero_TRdup : Lemma zero_TRdup :
TR_invariant ={}= TRdup 0. TR_invariant ={}= TRdup 0.
Proof. Proof.
iIntros "#Htockinv". iIntros "#Htickinv".
iInv timeReceiptN as (m) ">(Hcounter & Hγ1● & Hγ2● & Im)" "Hclose". iInv timeReceiptN as (m) ">(Hcounter & Hγ1● & Hγ2● & Im)" "Hclose".
iDestruct (own_auth_mnat_null with "Hγ2●") as "[Hγ2● $]". iDestruct (own_auth_mnat_null with "Hγ2●") as "[Hγ2● $]".
iApply "Hclose" ; eauto with iFrame. iApply "Hclose" ; eauto with iFrame.
...@@ -222,11 +216,11 @@ Section TockSpec. ...@@ -222,11 +216,11 @@ Section TockSpec.
iLöb as "IH". wp_rec. iExact "IH". iLöb as "IH". wp_rec. iExact "IH".
Qed. Qed.
Theorem tock_spec s E e v m : Theorem tick_spec s E e v m :
timeReceiptN E timeReceiptN E
IntoVal e v IntoVal e v
TR_invariant - TR_invariant -
{{{ TRdup m }}} tock e @ s ; E {{{ RET v ; TR 1 TRdup (m+1) }}}. {{{ TRdup m }}} tick e @ s ; E {{{ RET v ; TR 1 TRdup (m+1) }}}.
Proof. Proof.
intros ? <-. iIntros "#Inv" (Ψ) "!# Hγ2◯ HΨ". intros ? <-. iIntros "#Inv" (Ψ) "!# Hγ2◯ HΨ".
iLöb as "IH". iLöb as "IH".
...@@ -273,15 +267,15 @@ Section TockSpec. ...@@ -273,15 +267,15 @@ Section TockSpec.
iApply ("IH" with "Hγ2◯ HΨ"). iApply ("IH" with "Hγ2◯ HΨ").
Qed. Qed.
Theorem tock_spec_simple v n : Theorem tick_spec_simple v n :
TR_invariant - TR_invariant -
{{{ TRdup n }}} tock v {{{ RET v ; TR 1 TRdup (n+1) }}}. {{{ TRdup n }}} tick v {{{ RET v ; TR 1 TRdup (n+1) }}}.
Proof. Proof.
iIntros "#Inv" (Ψ) "!# H HΨ". iIntros "#Inv" (Ψ) "!# H HΨ".
by iApply (tock_spec with "Inv H HΨ"). by iApply (tick_spec with "Inv H HΨ").
Qed. Qed.
Lemma TR_implementation : TR_invariant - TR_interface nmax TR TRdup tock. Lemma TR_implementation : TR_invariant - TR_interface nmax TR TRdup.
Proof. Proof.
iIntros "#Hinv". repeat iSplitR. iIntros "#Hinv". repeat iSplitR.
- iPureIntro. by apply TR_timeless. - iPureIntro. by apply TR_timeless.
...@@ -292,10 +286,10 @@ Section TockSpec. ...@@ -292,10 +286,10 @@ Section TockSpec.
- iPureIntro. by apply TR_plus. - iPureIntro. by apply TR_plus.
- iPureIntro. by apply TRdup_max. - iPureIntro. by apply TRdup_max.
- by iApply (TRdup_nmax_absurd with "Hinv"). - by iApply (TRdup_nmax_absurd with "Hinv").
- iIntros (v n). by iApply (tock_spec_simple with "Hinv"). - iIntros (v n). by iApply (tick_spec_simple with "Hinv").
Qed. Qed.
End TockSpec. End TickSpec.
...@@ -315,7 +309,7 @@ Section Soundness. ...@@ -315,7 +309,7 @@ Section Soundness.
TR_invariant nmax - TR_invariant nmax -
{{{ True }}} «e» {{{ v, RET v ; ⌜ψ v }}} {{{ True }}} «e» {{{ v, RET v ; ⌜ψ v }}}
) )
`{timeReceiptHeapPreG Σ} `{TickCounter} σ, `{timeReceiptHeapPreG Σ, TickCounter} σ,
adequate NotStuck «e» S«σ,nmax-1» (λ v σ, ψ v). adequate NotStuck «e» S«σ,nmax-1» (λ v σ, ψ v).
Proof. Proof.
intros Inmax Hspec HpreG Hloc σ. intros Inmax Hspec HpreG Hloc σ.
...@@ -374,9 +368,8 @@ Section Soundness. ...@@ -374,9 +368,8 @@ Section Soundness.
Theorem abstract_spec_trtranslation__adequate {Σ} nmax φ e : Theorem abstract_spec_trtranslation__adequate {Σ} nmax φ e :
(0 < nmax)%nat (0 < nmax)%nat
is_closed [] e is_closed [] e
( `{heapG Σ} (TR TRdup : nat iProp Σ) (tock : val), ( `{heapG Σ, Tick} (TR TRdup : nat iProp Σ),
let _ := {| Translation.tick := tock |} in TR_interface nmax TR TRdup -
TR_interface nmax TR TRdup tock -
{{{ True }}} «e» {{{ v, RET v ; ⌜φ (invtranslationV v) }}} {{{ True }}} «e» {{{ v, RET v ; ⌜φ (invtranslationV v) }}}
) )
{_ : timeReceiptHeapPreG Σ} σ, {_ : timeReceiptHeapPreG Σ} σ,
......
From iris.heap_lang Require Import notation. From iris.heap_lang Require Export notation.
From stdpp Require Import fin_maps. From stdpp Require Import fin_maps.
From iris_time Require Import Reduction. From iris_time Require Import Reduction.
...@@ -17,8 +17,9 @@ Implicit Type m n : nat. ...@@ -17,8 +17,9 @@ Implicit Type m n : nat.
*) *)
(* tick is a typeclass so that it can be made an implicit argument of the (* tick is a typeclass so that it can be made an implicit argument of the
* translation and be inferred automatically from the context: *) * translation and be inferred automatically from the context.
Class Tick := { tick : val }. This also make it possible to share notations. *)
Class Tick := tick : val.
Section Translation. Section Translation.
...@@ -494,6 +495,22 @@ Notation "« σ »" := (translationS σ%V) (only printing). ...@@ -494,6 +495,22 @@ Notation "« σ »" := (translationS σ%V) (only printing).
Notation "« t »" := (translation <$> t%E) (only printing). Notation "« t »" := (translation <$> t%E) (only printing).
*) *)
Notation "'lettick:' x := e1 'in' e2" :=
((tick (Lam x%bind e2%E)) e1%E)
(at level 200, x at level 1, e1, e2 at level 200,
format "'[' 'lettick:' x := '[' e1 ']' 'in' '/' e2 ']'") : expr_scope.
Notation "e1 ;tick; e2" :=
((tick (Lam BAnon e2%E)) e1%E)
(at level 100, e2 at level 200,
format "'[' '[hv' '[' e1 ']' ;tick; ']' '/' e2 ']'") : expr_scope.
Notation "'tickmatch:' e0 'with' 'InjL' x1 => e1 | 'InjR' x2 => e2 'end'" :=
(Case (App (of_val tick) e0) (App (of_val tick_case_branch) (λ: <> x1, e1)%E)
(App (of_val tick_case_branch) (λ: <> x2, e2)%E))
(e0, x1, e1, x2, e2 at level 200,
format "'[hv' 'tickmatch:' e0 'with' '/ ' '[' 'InjL' x1 => '/ ' e1 ']' '/' '[' | 'InjR' x2 => '/ ' e2 ']' '/' 'end' ']'") : expr_scope.
(* (*
......
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