Commit 397fbe27 authored by Glen Mével's avatar Glen Mével

code cleanup

parent 0c8d2f7f
......@@ -119,7 +119,7 @@ Proof.
iApply "Post". eauto with iFrame.
Qed.
Lemma sum_list_translation_spec `{!timeCreditHeapG Σ} (l : list Z) (v : val) :
TICKCTXT -
TC_invariant -
{{{ is_list_tr l v TC (3 + 10 * length l) }}} « sum_list v » {{{ RET #(sum_list_coq l) ; is_list_tr l v }}}.
Proof.
iIntros "#Htickinv !#" (Φ) "[Hl Htc] Post".
......@@ -173,7 +173,7 @@ Proof.
iApply "Post". eauto with iFrame.
Qed.
Lemma make_list_translation_spec `{!timeCreditHeapG Σ} (n : nat) :
TICKCTXT -
TC_invariant -
{{{ TC (3+5*n) }}} «make_list #n» {{{ v', RET v' ; is_list (make_list_coq n) v' }}}.
Proof.
iIntros "#Htickinv !#" (Φ) "Htc Post".
......@@ -235,7 +235,7 @@ Proof.
iApply ("Post" with "[%]"). repeat f_equal. apply sum_list_coq_make_list_coq.
Qed.
Lemma prgm_translation_spec `{!timeCreditHeapG Σ} (n : nat) :
TICKCTXT -
TC_invariant -
{{{ TC (6+15*n) }}} «prgm n» {{{ v, RET v ; v = #(n*(n+1)/2) }}}.
Proof.
iIntros "#Htickinv !#" (Φ) "Htc Post".
......@@ -255,39 +255,10 @@ Proof.
iApply ("Post" with "[%]"). repeat f_equal. apply sum_list_coq_make_list_coq.
Qed.
Theorem spec_tctranslation__adequate_and_bounded' {Σ} m (φ : val Prop) e :
( v, φ v closure_free v)
is_closed [] e
( `{timeCreditHeapG Σ},
TICKCTXT -
{{{ TC m }}} «e» {{{ v, RET v ; ⌜φ v }}}
)
{_ : timeCreditHeapPreG Σ} σ,
adequate NotStuck e σ φ bounded_time e σ m.
Proof.
intros Hφ Hclosed Hspec HpreG σ.
apply (spec_tctranslation__adequate_and_bounded (Σ:=Σ)) ; try assumption.
intros HtcHeapG.
iIntros "#Htickinv !#" (Φ) "Htc Post".
wp_apply (Hspec with "Htickinv Htc"). iIntros (v Hv).
iApply ("Post" with "[%]").
by apply closure_free_predicate.
Qed.
Lemma prgm_timed_spec (n : nat) (σ : state) `{!timeCreditHeapPreG Σ} :
adequate NotStuck (prgm n) σ (λ v, v = #(n*(n+1)/2))
bounded_time (prgm n) σ (6 + 15 * n)%nat.
Proof.
(*
apply (spec_tctranslation__adequate_and_bounded (Σ:=Σ)).
- rewrite !andb_True ; repeat split ; apply is_closed_of_val.
- intros HtcHeapG.
iIntros "#Htickinv !#". iIntros (Φ) "Htc Post".
wp_apply (prgm_translation_spec with "Htickinv Htc"). iIntros (v ->).
iApply ("Post" with "[%]"). done.
- assumption.
Restart.
*)
apply (spec_tctranslation__adequate_and_bounded' (Σ:=Σ)).
- by intros _ ->.
- rewrite !andb_True ; repeat split ; apply is_closed_of_val.
......
......@@ -767,4 +767,19 @@ Section Safety.
intros <-. apply not_safe_fill.
Qed.
(* n-adequacy: *)
Record nadequate (s : stuckness) (n : nat) e1 σ1 (φ : val Prop) : Prop := {
nadequate_result k t2 σ2 v2 :
nsteps step k ([e1], σ1) (of_val v2 :: t2, σ2) (k n)%nat φ v2;
nadequate_not_stuck k t2 σ2 e2 :
s = NotStuck
nsteps step k ([e1], σ1) (t2, σ2)
(k < n)%nat
e2 t2 (is_Some (to_val e2) reducible e2 σ2)
}.
(* n-safety: *)
Definition nsafe n e σ : Prop :=
nadequate NotStuck n e σ (λ _, True).
End Safety.
\ No newline at end of file
......@@ -11,17 +11,20 @@ Implicit Type t : list expr.
Implicit Type K : ectx heap_ectx_lang.
Implicit Type : loc.
Implicit Type m n : nat.
Implicit Type φ : val Prop.
(* Our definition of tick will depend on a location. This is made a typeclass
* so as to be inferred automatically. *)
Class TickCounter := { tick_counter : loc }.
Notation "S« σ , n »" := (<[tick_counter := LitV (LitInt n%nat)]> (translationS σ%V)).
(* Notation "« σ , n »" := (<[ := LitV (LitInt n%nat)]> (translationS σ%V)) (only printing). *)
Local Notation := tick_counter.
Section Simulation. (* this whole file is parameterized by a runtime_error value *)
(* This whole file is parameterized by a runtime_error value: *)
Section Simulation.
Context (runtime_error : val).
......@@ -139,13 +142,12 @@ Section Tick_exec.
apply prim_exec_nil.
Qed.
Lemma exec_tick_aux e1 v2 σ :
Lemma exec_tick_case_branch e1 v2 σ :
is_closed [] e1
prim_exec (tick_aux (λ: <>, e1) v2)%E σ
(e1 (tick v2) ) σ [].
prim_exec (tick_case_branch (λ: <>, e1) v2)%E σ (e1 (tick v2)) σ [].
Proof.
intros ; assert (Closed [] e1) by exact.
unfold tick_aux ; unlock.
unfold tick_case_branch ; unlock.
eapply prim_exec_cons_nofork.
{
prim_step.
......@@ -265,13 +267,13 @@ Section SimulationLemma.
(* SndS e1 v1 e2 v2 σ : *)
- tick_then_step_then_stop.
(* CaseLS e0 v0 e1 e2 σ : *)
- tick_then_step_then exec_tick_aux.
- tick_then_step_then exec_tick_case_branch.
(* this is the only place where we need the term to be closed (because
* the reduction rules for Case are adhoc somehow: *)
simpl in Hclosed ; repeat (apply andb_True in Hclosed as [ Hclosed ? ]).
by apply is_closed_translation.
(* CaseRS e0 v0 e1 e2 σ : *)
- tick_then_step_then exec_tick_aux.
- tick_then_step_then exec_tick_case_branch.
(* this is the only place where we need the term to be closed (because
* the reduction rules for Case are adhoc somehow: *)
simpl in Hclosed ; repeat (apply andb_True in Hclosed as [ Hclosed ? ]).
......@@ -557,7 +559,7 @@ Section SimulationLemma.
(* assuming the adequacy of the translated expression,
* a proof that the original expression has m-adequate results. *)
Lemma adequate_translation__adequate_result m n (φ : val Prop) e σ t2 σ2 v2 :
Lemma adequate_translation__adequate_result m n φ e σ t2 σ2 v2 :
is_closed [] e
σ2 !! = None
adequate NotStuck «e» S«σ, m» (φ invtranslationV)
......@@ -579,20 +581,10 @@ End SimulationLemma. (* we close the section here as we now want to quantify ove
(* now lets combine the two results. *)
Record adequate_n (s : stuckness) (n : nat) e1 σ1 (φ : val Prop) := {
adequate_n_result k t2 σ2 v2 :
nsteps step k ([e1], σ1) (of_val v2 :: t2, σ2) (k n)%nat φ v2;
adequate_n_not_stuck k t2 σ2 e2 :
s = NotStuck
nsteps step k ([e1], σ1) (t2, σ2)
(k < n)%nat
e2 t2 (is_Some (to_val e2) reducible e2 σ2)
}.
Lemma adequate_translation__adequate m (φ : val Prop) e σ :
Lemma adequate_translation__adequate m φ e σ :
is_closed [] e
( {Hloc : TickCounter}, adequate NotStuck «e» S«σ, m» (φ invtranslationV))
adequate_n NotStuck m e σ φ.
nadequate NotStuck m e σ φ.
Proof.
intros Hclosed Hadq.
split.
......
......@@ -87,7 +87,7 @@ Section Thunk.
end.
Lemma create_spec p nc φ f :
TICKCTXT -
TC_invariant -
{{{ TC 1 ( {{{ TC nc }}} f #() {{{ v, RET v ; φ v }}} ) }}}
«create» f
{{{ (t : loc), RET #t ; Thunk p t nc φ }}}.
......@@ -107,7 +107,7 @@ Section Thunk.
Lemma force_spec p F t φ :
(thunkN t) F
( (v : val), φ v - φ v φ v)
TICKCTXT -
TC_invariant -
{{{ TC 7 Thunk p t 0 φ na_own p F }}}
«force» #t
{{{ v, RET v ; φ v na_own p F }}}.
......@@ -187,6 +187,4 @@ Section Thunk.
}
Qed.
(* TODO: prove these specifications on the translation of create, force *)
End Thunk.
\ No newline at end of file
From iris.heap_lang Require Import proofmode notation adequacy.
From iris.algebra Require Import auth.
From iris.base_logic Require Import invariants.
From iris.proofmode Require Import classes.
From stdpp Require Import namespaces.
Require Import Auth_nat Misc Reduction Tactics.
Require Export Translation Simulation.
From iris.proofmode Require Import coq_tactics.
Import uPred.
Implicit Type e : expr.
Implicit Type v : val.
Implicit Type σ : state.
Implicit Type t : list expr.
Implicit Type K : ectx heap_ectx_lang.
Implicit Type m n : nat.
Implicit Type φ ψ : val Prop.
Implicit Type Σ : gFunctors.
......@@ -106,11 +108,11 @@ Section TickSpec.
Definition timeCreditN := nroot .@ "timeCredit".
Definition TICKCTXT : iProp Σ :=
Definition TC_invariant : iProp Σ :=
inv timeCreditN ( (m:nat), #m own γ (nat m))%I.
Lemma zero_TC :
TICKCTXT ={}= TC 0.
TC_invariant ={}= TC 0.
Proof.
iIntros "#Htickinv".
iInv timeCreditN as (m) ">[Hcounter H●]" "Hclose".
......@@ -121,7 +123,7 @@ Section TickSpec.
Theorem tick_spec s E e v :
timeCreditN E
IntoVal e v
TICKCTXT -
TC_invariant -
{{{ TC 1 }}} tick e @ s ; E {{{ RET v ; True }}}.
Proof.
intros ? <- % of_to_val. iIntros "#Inv" (Ψ) "!# Hγ◯ HΨ".
......@@ -168,14 +170,14 @@ Section TickSpec.
Qed.
Theorem tick_spec_simple v :
TICKCTXT -
TC_invariant -
{{{ TC 1 }}} tick v {{{ RET v ; True }}}.
Proof.
iIntros "#Hinv" (Ψ) "!# HTC HΨ".
by iApply (tick_spec with "Hinv [HTC//] HΨ").
Qed.
Lemma TC_implementation : TICKCTXT - TC_interface TC tick.
Lemma TC_implementation : TC_invariant - TC_interface TC tick.
Proof.
iIntros "#Hinv". iSplit ; last iSplit ; last iSplit.
- iPureIntro. by apply TC_timeless.
......@@ -442,7 +444,7 @@ Section Soundness.
by eapply simulation_exec_failure.
Qed.
Lemma adequate_tctranslation__bounded m (φ : val Prop) e σ :
Lemma adequate_tctranslation__bounded m φ e σ :
is_closed [] e
( `{TickCounter}, adequate NotStuck «e» S«σ, m» (φ invtranslationV))
bounded_time e σ m.
......@@ -461,7 +463,7 @@ Section Soundness.
(* now lets combine the three results. *)
Lemma adequate_tctranslation__adequate_and_bounded m (φ : val Prop) e σ :
Lemma adequate_tctranslation__adequate_and_bounded m φ e σ :
is_closed [] e
( (k : nat), (k m)%nat
`{TickCounter}, adequate NotStuck «e» S«σ, k» (φ invtranslationV)
......@@ -471,24 +473,24 @@ Section Soundness.
intros Hclosed Hadq.
assert (bounded_time e σ m) as Hbounded
by (eapply adequate_tctranslation__bounded, Hadq ; [ assumption | lia ]).
assert (adequate_n NotStuck (m + 1) e σ φ) as Hadqm
assert (nadequate NotStuck (m + 1) e σ φ) as Hadqm
by (apply adequate_tctranslation__adequate, Hadq ; [ assumption | lia ]).
clear Hadq.
split ; last done.
split.
- intros t2 σ2 v2 [n Hnsteps] % rtc_nsteps.
assert (n m)%nat as Inm by by eapply Hbounded.
eapply adequate_n_result ; try done ; lia.
eapply nadequate_result ; try done ; lia.
- intros t2 σ2 e2 _ [n Hnsteps] % rtc_nsteps He2.
assert (n m)%nat as Inm by by eapply Hbounded.
eapply adequate_n_not_stuck ; try done ; lia.
eapply nadequate_not_stuck ; try done ; lia.
Qed.
(* finally, derive the adequacy assumption from a Hoare triple in Iris. *)
Lemma spec_tctranslation__adequate {Σ} m (ψ : val Prop) e :
Lemma spec_tctranslation__adequate {Σ} m ψ e :
( `{timeCreditHeapG Σ},
TICKCTXT -
TC_invariant -
{{{ TC m }}} «e» {{{ v, RET v ; ⌜ψ v }}}
)
`{timeCreditHeapPreG Σ} `{TickCounter} σ,
......@@ -517,7 +519,7 @@ Section Soundness.
pose (Build_timeCreditHeapG Σ (HeapG Σ _ (GenHeapG _ _ Σ _ _ _ h)) _ _ γ)
as HtcHeapG.
(* create the invariant: *)
iAssert (|={}=> TICKCTXT)%I with "[Hℓ◯ Hγ●]" as "> Hinv".
iAssert (|={}=> TC_invariant)%I with "[Hℓ◯ Hγ●]" as "> Hinv".
{
iApply inv_alloc.
iExists k.
......@@ -532,10 +534,10 @@ Section Soundness.
iApply (Hspec with "Hinv Hγ◯") ; auto.
Qed.
Theorem spec_tctranslation__adequate_and_bounded {Σ} m (φ : val Prop) e :
Theorem spec_tctranslation__adequate_and_bounded {Σ} m φ e :
is_closed [] e
( `{timeCreditHeapG Σ},
TICKCTXT -
TC_invariant -
{{{ TC m }}} «e» {{{ v, RET v ; ⌜φ (invtranslationV v) }}}
)
{_ : timeCreditHeapPreG Σ} σ,
......@@ -546,7 +548,8 @@ Section Soundness.
intros k Ik Hloc. by eapply spec_tctranslation__adequate.
Qed.
Theorem abstract_spec_tctranslation__adequate_and_bounded {Σ} m (φ : val Prop) e :
(* The abstract version of the theorem: *)
Theorem abstract_spec_tctranslation__adequate_and_bounded {Σ} m φ e :
is_closed [] e
( `{heapG Σ} (TC : nat iProp Σ) (tick : val),
let _ := {| Translation.tick := tick |} in
......@@ -562,6 +565,28 @@ Section Soundness.
iApply Hspec. by iApply TC_implementation.
Qed.
(* A simplification for common use-cases: when the return value does not
* contain a closure, there is no need to compose the postcondition φ with
* the translation: *)
Theorem spec_tctranslation__adequate_and_bounded' {Σ} m (φ : val Prop) e :
( v, φ v closure_free v)
is_closed [] e
( `{timeCreditHeapG Σ},
TC_invariant -
{{{ TC m }}} «e» {{{ v, RET v ; ⌜φ v }}}
)
{_ : timeCreditHeapPreG Σ} σ,
adequate NotStuck e σ φ bounded_time e σ m.
Proof.
intros Hφ Hclosed Hspec HpreG σ.
apply (spec_tctranslation__adequate_and_bounded (Σ:=Σ)) ; try assumption.
intros HtcHeapG.
iIntros "#Htickinv !#" (Φ) "Htc Post".
wp_apply (Hspec with "Htickinv Htc"). iIntros (v Hv).
iApply ("Post" with "[%]").
by apply closure_free_predicate.
Qed.
End Soundness.
......@@ -572,20 +597,17 @@ End Soundness.
Section Tactics.
From iris.proofmode Require Import coq_tactics tactics.
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export tactics lifting.
Import uPred.
Context {Σ : gFunctors}.
Implicit Types Φ : val iProp Σ.
Implicit Types Δ : envs (iResUR Σ).
Context {Σ : gFunctors}.
Implicit Types Φ : val iProp Σ.
Implicit Types Δ : envs (iResUR Σ).
(* concrete version: *)
Lemma tac_wp_tick `{timeCreditHeapG Σ} Δ Δ' Δ'' s E i j n K e v Φ :
timeCreditN E
IntoVal e v
MaybeIntoLaterNEnvs 1 Δ Δ'
envs_lookup i Δ = Some (true, TICKCTXT)
envs_lookup i Δ = Some (true, TC_invariant)
envs_lookup j Δ' = Some (false, TC (S n))
envs_simple_replace j false (Esnoc Enil j (TC n)) Δ' = Some Δ''
envs_entails Δ'' (WP fill K v @ s; E {{ Φ }})
......@@ -602,7 +624,7 @@ Implicit Types Δ : envs (iResUR Σ).
Qed.
(*
(* abstract version: *)
(* TODO: abstract version: *)
Lemma tac_wp_tick_abstr `{heapG Σ} (TC : nat iProp Σ) (tick : val) Δ Δ' Δ'' s E i j n K e v Φ :
IntoVal e v
MaybeIntoLaterNEnvs 1 Δ Δ'
......@@ -618,7 +640,7 @@ End Tactics.
Ltac wp_tick :=
let solve_TICKCTXT _ :=
iAssumptionCore || fail "wp_tick: cannot find TICKCTXT" in
iAssumptionCore || fail "wp_tick: cannot find TC_invariant" in
let solve_TC _ :=
iAssumptionCore || fail "wp_tick: cannot find TC (S _)" in
let finish _ :=
......
......@@ -9,6 +9,8 @@ Implicit Type σ : state.
Implicit Type t : list expr.
Implicit Type K : ectx heap_ectx_lang.
Implicit Type m n : nat.
Implicit Type φ ψ : val Prop.
Implicit Type Σ : gFunctors.
Local Notation γ := timeCreditHeapG_name.
Local Notation := tick_counter.
......@@ -16,7 +18,7 @@ Local Notation ℓ := tick_counter.
(* In general, one can prove:
* if the translated program with the counter initialized to m is safe,
* then the source program is m-safe.
* This is lemma [adequate_translation__adequate] in `Simulation.v`.
* This is lemma [adequate_translation__nadequate] in `Simulation.v`.
*
* Moreover, for time credits, we can prove:
* if the translated program with the counter initialized to m is safe,
......@@ -33,7 +35,7 @@ Local Notation ℓ := tick_counter.
* if the Hoare triple { TC m } «e» { φ } holds,
* then FOR ALL m' m,
* the translated program with the counter initialized to m' is safe.
* This is lemma [spec_tctranslation__adequate] in `TimeCredits.v`.
* This is lemma [<spec_tctranslation__adequate_tctranslation>] in `TimeCredits.v`.
*
* Hence from the Hoare triple we can deduce that the source program
* (1) computes in at most m steps (by taking m' = m), and
......@@ -47,7 +49,7 @@ Local Notation ℓ := tick_counter.
* if the translated program with the counter initialized to m is safe,
* then the source program is safe.
* The proof is given below. It is mostly a copy-paste of the general proof
* of [adequate_translation__adequate] in `Simulation.v`, with additional calls
* of [adequate_translation__nadequate] in `Simulation.v`, with additional calls
* to [safe_tctranslation__bounded] and one call to [not_safe_tick].
*)
......@@ -135,7 +137,7 @@ Qed.
(* assuming the adequacy of the translated expression,
* a proof that the original expression has adequate results. *)
Lemma adequate_tctranslation__adequate_result {Hloc : TickCounter} m (φ : val Prop) e σ t2 σ2 v2 :
Lemma adequate_tctranslation__adequate_result {Hloc : TickCounter} m φ e σ t2 σ2 v2 :
is_closed [] e
σ2 !! = None
adequate NotStuck «e» S«σ, m» (φ invtranslationV)
......@@ -155,7 +157,7 @@ Qed.
(* now lets combine the two results. *)
Lemma adequate_tctranslation__adequate_alt m (φ : val Prop) e σ :
Lemma adequate_tctranslation__adequate m φ e σ :
is_closed [] e
( `{TickCounter}, adequate NotStuck «e» S«σ, m» (φ invtranslationV))
adequate NotStuck e σ φ.
......@@ -241,9 +243,9 @@ Proof.
pose proof (eq_stepl Hσ H) as E. by injection E.
Qed.
Lemma spec_tctranslation__bounded {Σ} m (ψ : val Prop) e :
Lemma spec_tctranslation__bounded {Σ} m ψ e :
( `{timeCreditHeapG Σ},
TICKCTXT -
TC_invariant -
{{{ TC m }}} «e» {{{ v, RET v ; ⌜ψ v }}}
)
`{TickCounter} `{timeCreditHeapPreG Σ} σ1 t2 σ2 (z : Z),
......@@ -255,7 +257,7 @@ Proof.
apply (wp_invariance Σ _ NotStuck «e» S«σ1,m» T«t2» S«σ2,z») ; simpl ; last assumption.
intros HinvG.
(* now we have to prove a WP for some state interpretation, for which
* we settle the needed invariant TICKCTXT. *)
* 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]}))
......@@ -276,7 +278,7 @@ Proof.
pose (Build_timeCreditHeapG Σ (HeapG Σ HinvG (GenHeapG _ _ Σ _ _ HgenHeapPreInG h)) HinG _ γ)
as HtcHeapG.
(* create the invariant: *)
iAssert (|={}=> TICKCTXT)%I with "[Hℓ◯ Hγ●]" as "> #Hinv".
iAssert (|={}=> TC_invariant)%I with "[Hℓ◯ Hγ●]" as "> #Hinv".
{
iApply inv_alloc.
iExists m.
......@@ -309,10 +311,10 @@ Axiom simulation_exec_alt : ∀ {Hloc : TickCounter} m n t1 σ1 t2 σ2,
nsteps step m (t1, σ1) (t2, σ2)
rtc step (T«t1», S«σ1, n») (T«t2», S«σ2, (n-m)%Z»).
Lemma spec_tctranslation__bounded' {Σ} m (ψ : val Prop) e :
Lemma spec_tctranslation__bounded' {Σ} m ψ e :
is_closed [] e
( `{timeCreditHeapG Σ},
TICKCTXT -
TC_invariant -
{{{ TC m }}} «e» {{{ v, RET v ; ⌜ψ v }}}
)
`{!timeCreditHeapPreG Σ} σ,
......
From iris.heap_lang Require Import proofmode notation adequacy.
From iris.algebra Require Import auth.
From iris.base_logic Require Import invariants.
From iris.proofmode Require Import classes.
From stdpp Require Import namespaces.
Require Import Auth_nat Auth_mnat Misc Reduction Tactics.
Require Export Translation Simulation.
(* Require Import TimeCredits. *)
Implicit Type e : expr.
Implicit Type v : val.
Implicit Type σ : state.
Implicit Type t : list expr.
Implicit Type K : ectx heap_ectx_lang.
Implicit Type m n : nat.
(* rem: Unicode notations?
* medals: 🏅🥇🎖
* gears: ⚙⛭
* shields:
* florettes: ✿❀
* squares:
* circles:
* pentagons:
* hexagons:
* shogi pieces:
* sandglasses:
* other:
*)
Implicit Type m n nmax : nat.
Implicit Type φ ψ : val Prop.
Implicit Type Σ : gFunctors.
......@@ -38,7 +21,7 @@ Implicit Type m n : nat.
(* 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 Σ}
Definition TR_interface `{irisG heap_lang Σ}
(nmax : nat)
(TR : nat iProp Σ)
(TRdup : nat iProp Σ)
......@@ -102,6 +85,7 @@ Global Instance Tick_tock (Hloc: TickCounter) : Tick :=
Section TockSpec.
Context `{timeReceiptHeapG Σ}.
Context (nmax : nat).
Definition TR (n : nat) : iProp Σ :=
own γ1 (nat n).
......@@ -150,11 +134,11 @@ Section TockSpec.
Definition timeReceiptN := nroot .@ "timeReceipt".
Definition TOCKCTXT (nmax : nat) : iProp Σ :=
Definition TR_invariant : 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.
Lemma zero_TR :
TR_invariant ={}= TR 0.
Proof.
iIntros "#Htockinv".
iInv timeReceiptN as (m) ">(Hcounter & Hγ1● & H)" "Hclose".
......@@ -162,8 +146,8 @@ Section TockSpec.
iApply "Hclose" ; eauto with iFrame.
Qed.
Lemma zero_TRdup (nmax : nat) :
TOCKCTXT nmax ={}= TRdup 0.
Lemma zero_TRdup :
TR_invariant ={}= TRdup 0.
Proof.
iIntros "#Htockinv".
iInv timeReceiptN as (m) ">(Hcounter & Hγ1● & Hγ2● & Im)" "Hclose".
......@@ -171,9 +155,9 @@ Section TockSpec.
iApply "Hclose" ; eauto with iFrame.
Qed.
Lemma TR_nmax_absurd (nmax : nat) (E : coPset) :
Lemma TR_nmax_absurd (E : coPset) :
timeReceiptN E
TOCKCTXT nmax - TR nmax ={E}= False.
TR_invariant - TR nmax ={E}= False.
Proof.
iIntros (?) "#Inv Hγ1◯".
iInv timeReceiptN as (n) ">(Hℓ & Hγ1● & Hγ2● & In)" "InvClose" ; iDestruct "In" as %In.
......@@ -181,9 +165,9 @@ Section TockSpec.
exfalso ; lia.
Qed.
Lemma TRdup_nmax_absurd (nmax : nat) (E : coPset) :
Lemma TRdup_nmax_absurd (E : coPset) :
timeReceiptN E
TOCKCTXT nmax - TRdup nmax ={E}= False.
TR_invariant - TRdup nmax ={E}= False.
Proof.
iIntros (?) "#Inv Hγ2◯".
iInv timeReceiptN as (n) ">(Hℓ & Hγ1● & Hγ2● & In)" "InvClose" ; iDestruct "In" as %In.
......@@ -191,9 +175,9 @@ Section TockSpec.
exfalso ; lia.
Qed.
Lemma TR_TRdup (nmax : nat) (E : coPset) (n : nat) :
Lemma TR_TRdup (E : coPset) n :
timeReceiptN E
TOCKCTXT nmax - TR n ={E}= TR n TRdup n.
TR_invariant - TR n ={E}= TR n TRdup n.
Proof.
iIntros (?) "#Inv Hγ1◯".
iInv timeReceiptN as (m) ">(Hℓ & Hγ1● & Hγ2● & Im)" "InvClose".
......@@ -212,10 +196,10 @@ Section TockSpec.
iLöb as "IH". wp_rec. iExact "IH".
Qed.
Theorem tock_spec (nmax : nat) s E e v m :
Theorem tock_spec s E e v m :
timeReceiptN E
IntoVal e v
TOCKCTXT nmax -
TR_invariant -
{{{ TRdup m }}} tock e @ s ; E {{{ RET v ; TR 1 TRdup (m+1) }}}.
Proof.
intros ? <- % of_to_val. iIntros "#Inv" (Ψ) "!# Hγ2◯ HΨ".
......@@ -263,15 +247,15 @@ Section TockSpec.
iApply ("IH" with "Hγ2◯ HΨ").
Qed.
Theorem tock_spec_simple (nmax : nat) v (n : nat) :
TOCKCTXT nmax -
Theorem tock_spec_simple v n :
TR_invariant -
{{{ 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.
Lemma TR_implementation : TR_invariant - TR_interface nmax TR TRdup tock.
Proof.
iIntros "#Hinv". repeat iSplitR.
- iPureIntro. by apply TR_timeless.
......@@ -299,10 +283,10 @@ Section Soundness.
(* derive the adequacy of the translated program from a Hoare triple in Iris. *)
Lemma spec_trtranslation__adequate_translation {Σ} (nmax : nat) (ψ : val Prop) e :
Lemma spec_trtranslation__adequate_translation {Σ} nmax ψ e :
(0 < nmax)%nat
( `{timeReceiptHeapG Σ},
TOCKCTXT nmax -
TR_invariant nmax -
{{{ True }}} «e» {{{ v, RET v ; ⌜ψ v }}}
)
`{timeReceiptHeapPreG Σ} `{TickCounter} σ, adequate NotStuck «e» S«σ,nmax-1» ψ.
......@@ -331,7 +315,7 @@ Section Soundness.
pose (Build_timeReceiptHeapG Σ (HeapG Σ _ (GenHeapG _ _ Σ _ _ _ h)) _ _ _ γ1 γ2)
as HtrHeapG.
(* create the invariant: *)
iAssert (|={}=> TOCKCTXT nmax)%I with "[Hℓ◯ Hγ1● Hγ2●]" as "> Hinv".
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.
......@@ -345,22 +329,22 @@ Section Soundness.
iApply (Hspec with "Hinv") ; auto.
Qed.
Lemma spec_trtranslation__adequate {Σ} (nmax : nat) (φ : val Prop) e :
Theorem spec_trtranslation__adequate {Σ} nmax φ e :
(0 < nmax)%nat
is_closed [] e
( `{timeReceiptHeapG Σ},
TOCKCTXT nmax -
TR_invariant nmax -
{{{ True }}} «e» {{{ v, RET v ; ⌜φ (invtranslationV v) }}}
)
`{!timeReceiptHeapPreG Σ} σ,
adequate_n NotStuck (nmax-1) e σ φ.
nadequate NotStuck (nmax-1) e σ φ.
Proof.
intros Inmax Hclosed Hspec HpreG σ.
eapply adequate_trtranslation__adequate ; first done.
intros Hloc. by eapply spec_trtranslation__adequate_translation.
Qed.
Lemma abstract_spec_trtranslation__adequate {Σ} (nmax : nat) (φ : val Prop) e :
Theorem abstract_spec_trtranslation__adequate {Σ} nmax φ e :
(0 < nmax)%nat
is_closed [] e
( `{heapG Σ} (TR TRdup : nat iProp Σ) (tock : val),
......@@ -369,7 +353,7 @@ Section Soundness.
{{{ True }}} «e» {{{ v, RET v ; ⌜φ (invtranslationV v) }}}
)
{_ : timeReceiptHeapPreG Σ} σ,
adequate_n NotStuck (nmax-1) e σ φ.
nadequate NotStuck (nmax-1) e σ φ.
Proof.
intros Inmax Hclosed Hspec HpreG σ.
eapply spec_trtranslation__adequate ; try done.
......
This diff is collapsed.