Commit 4b59cf37 authored by Glen Mével's avatar Glen Mével

refactored implicit parameters of the translation (tick) and of tick...

refactored implicit parameters of the translation (tick) and of tick (runtime_error and the location); notations are now defined only once
parent ed7e0be2
From iris.heap_lang Require Import notation proofmode.
From iris.program_logic Require Import adequacy.
Require Import Misc Reduction Tactics.
Require Export Translation.
......@@ -13,20 +14,44 @@ Implicit Type m n : nat.
Section Tick.
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.
Context (runtime_error : val).
Context ( : loc).
Definition tick : val :=
rec: "tick" "x" :=
let: "k" := ! # in
if: "k" #0 then
runtime_error #()
else if: CAS # "k" ("k" - #1) then
"x"
else
"tick" "x".
Section Simulation. (* this whole file is parameterized by a runtime_error value *)
Context (runtime_error : val).
(*
* Definition of tick
*)
Definition tick {Hloc : TickCounter} : val :=
rec: "tick" "x" :=
let: "k" := ! # in
if: "k" #0 then
runtime_error #()
else if: CAS # "k" ("k" - #1) then
"x"
else
"tick" "x".
Local Instance Tick_tick (Hloc: TickCounter) : Tick :=
{| Translation.tick := tick |}.
(*
* Operational behavior of tick
*)
Section Tick_exec.
Context {Hloc : TickCounter}.
Lemma exec_tick_success n v σ :
prim_exec (tick v) (<[ := #(S n)]> σ) v (<[ := #n]> σ) [].
......@@ -114,17 +139,6 @@ Section Tick.
apply prim_exec_nil.
Qed.
End Tick.
Section Tick_aux.
Context (tick : val).
Definition tick_aux : val :=
(λ: "f" "x", "f" #() (tick "x"))%V.
Lemma exec_tick_aux e1 v2 σ :
is_closed [] e1
prim_exec (tick_aux (λ: <>, e1) v2)%E σ
......@@ -154,27 +168,22 @@ Section Tick_aux.
by prim_step.
}
Qed.
End Tick_aux.
End Tick_exec.
(*
* Simulation
* Simulation lemma
*)
Section Simulation.
Section SimulationLemma.
Context ( : loc).
Context (tick : val).
Context {Hloc : TickCounter}.
(* from a reduction of the source expression,
* deduce a reduction of the translated expression. *)
Context (exec_tick_success :
n v σ,
prim_exec (tick v) (<[ := #(S n)]> σ) v (<[ := #n]> σ) []
).
Lemma exec_tick_success' n e v σ :
to_val e = Some v
prim_exec (tick e) (<[ := #(S n)]> σ) e (<[ := #n]> σ) [].
......@@ -206,18 +215,6 @@ Section Simulation.
Local Ltac tick_then_step_then_stop :=
tick_then_step_then prim_exec_nil.
Local Notation "E« e »" := (translation tick e%E).
Local Notation "V« v »" := (translationV tick v%V).
Local Notation "Ki« ki »" := (translationKi tick ki).
Local Notation "K« K »" := (translationK tick K).
Local Notation "S« σ »" := (translationS tick σ%V).
Local Notation "S« σ , n »" := (<[ := LitV (LitInt n%nat)]> (translationS tick σ%V)).
Local Notation "T« t »" := (translation tick <$> t%E).
Local Notation "« e »" := (translation tick e%E).
Local Notation "« e »" := (translation tick e%E) : expr_scope.
Local Notation "« v »" := (translationV tick v%V) : val_scope.
Lemma simulation_head_step_success n e1 σ1 e2 σ2 efs :
σ2 !! = None
is_closed [] e1
......@@ -379,7 +376,7 @@ Section Simulation.
(* from a reduction of the translated expression,
* deduce a reduction of the source expression. *)
(* note: this does not depend on the operational semantics of `tick`. *)
(* note: this does not depend on the operational behavior of `tick`. *)
Local Ltac exhibit_prim_step e2 :=
eexists e2, _, _ ; simpl ; prim_step.
......@@ -466,7 +463,7 @@ Section Simulation.
(* CasFailS *)
- apply lookup_translationS_Some_inv in Hbound_l as (? & ? & ->).
exhibit_prim_step (#false)%E.
intros ? % (f_equal (translationV tick)). contradiction.
intros ? % (f_equal translationV). contradiction.
(* CasSucS *)
- apply lookup_translationS_Some_inv in Hbound_l as (? & ? & -> % translationV_injective).
exhibit_prim_step (#true)%E.
......@@ -560,8 +557,6 @@ Section Simulation.
(* assuming the adequacy of the translated expression,
* a proof that the original expression has m-adequate results. *)
From iris.program_logic Require Import adequacy.
Lemma adequate_translation__adequate_result m n (φ : val Prop) e σ t2 σ2 v2 :
is_closed [] e
σ2 !! = None
......@@ -572,7 +567,7 @@ From iris.program_logic Require Import adequacy.
Proof.
intros Hclosed Hfresh Hadq Hnsteps Inm.
assert (safe «e» S«σ, m») as Hsafe by by eapply safe_adequate.
replace (φ v2) with ((φ invtranslationV) (translationV tick v2))
replace (φ v2) with ((φ invtranslationV) (translationV v2))
by (simpl ; by rewrite invtranslationV_translationV).
eapply adequate_result ; first done.
change [«e»%E] with T«[e]».
......@@ -580,32 +575,9 @@ From iris.program_logic Require Import adequacy.
eapply simulation_exec_success' ; eauto.
Qed.
End Simulation.
Section StrongSimulation.
End SimulationLemma. (* we close the section here as we now want to quantify over all locations *)
Context (tick : loc val).
(* from a reduction of the source expression,
* deduce a reduction of the translated expression. *)
Context (exec_tick_success :
n v σ,
prim_exec (tick v) (<[ := #(S n)]> σ) v (<[ := #n]> σ) []
).
Local Notation "E{ ℓ }« e »" := (translation (tick ) e%E).
Local Notation "V{ ℓ }« v »" := (translationV (tick ) v%V).
Local Notation "Ki{ ℓ }« ki »" := (translationKi (tick ) ki).
Local Notation "K{ ℓ }« K »" := (translationK (tick ) K).
Local Notation "S{ ℓ }« σ »" := (translationS (tick ) σ%V).
Local Notation "S{ ℓ }« σ , n »" := (<[ := LitV (LitInt n%nat)]> (translationS (tick ) σ%V)).
Local Notation "T{ ℓ }« t »" := (translation (tick ) <$> t%E).
Local Notation "{ ℓ }« e »" := (translation (tick ) e%E).
Local Notation "{ ℓ }« e »" := (translation (tick ) e%E) : expr_scope.
Local Notation "{ ℓ }« v »" := (translationV (tick ) v%V) : val_scope.
(* now lets combine the two results. *)
(* now lets combine the two results. *)
Record adequate_n (s : stuckness) (n : nat) e1 σ1 (φ : val Prop) := {
adequate_n_result k t2 σ2 v2 :
......@@ -617,34 +589,34 @@ Record adequate_n (s : stuckness) (n : nat) e1 σ1 (φ : val → Prop) := {
e2 t2 (is_Some (to_val e2) reducible e2 σ2)
}.
Lemma adequate_translation__adequate m (φ : val Prop) e σ :
is_closed [] e
( (:loc), adequate NotStuck {}«e» S{}«σ, m» (φ invtranslationV))
adequate_n NotStuck m e σ φ.
Proof.
intros Hclosed Hadq.
split.
(* (1) adequate result: *)
- intros n t2 σ2 v2 Hnsteps Inm.
(* build a location which is not in the domain of σ2: *)
pose ( := fresh (dom (gset loc) σ2) : loc).
assert (σ2 !! = None)
by (simpl ; eapply not_elem_of_dom, is_fresh).
by eapply adequate_translation__adequate_result.
(* (2) safety: *)
- intros n t2 σ2 e2 _ Hnsteps Inm He2.
(* build a location which is fresh in e2 and in the domain of σ2: *)
pose (set1 := loc_set_of_expr e2 : gset loc).
pose (set2 := dom (gset loc) σ2 : gset loc).
pose ( := fresh (set1 set2) : loc).
eassert ( set1 set2) as [H1 H2] % not_elem_of_union
by (unfold ; apply is_fresh).
assert (loc_fresh_in_expr e2)
by by apply loc_not_in_set_is_fresh.
assert (σ2 !! = None)
by by (simpl ; eapply not_elem_of_dom).
specialize (Hadq ) as Hsafe % safe_adequate.
by eapply safe_translation__safe.
Qed.
End StrongSimulation.
\ No newline at end of file
Lemma adequate_translation__adequate m (φ : val Prop) e σ :
is_closed [] e
( {Hloc : TickCounter}, adequate NotStuck «e» S«σ, m» (φ invtranslationV))
adequate_n NotStuck m e σ φ.
Proof.
intros Hclosed Hadq.
split.
(* (1) adequate result: *)
- intros n t2 σ2 v2 Hnsteps Inm.
(* build a location which is not in the domain of σ2: *)
pose (Hloc := Build_TickCounter (fresh (dom (gset loc) σ2)) : TickCounter).
assert (σ2 !! = None)
by (simpl ; eapply not_elem_of_dom, is_fresh).
by eapply adequate_translation__adequate_result.
(* (2) safety: *)
- intros n t2 σ2 e2 _ Hnsteps Inm He2.
(* build a location which is fresh in e2 and in the domain of σ2: *)
pose (set1 := loc_set_of_expr e2 : gset loc).
pose (set2 := dom (gset loc) σ2 : gset loc).
pose (Hloc := Build_TickCounter (fresh (set1 set2)) : TickCounter).
eassert ( set1 set2) as [H1 H2] % not_elem_of_union
by (unfold ; apply is_fresh).
assert (loc_fresh_in_expr e2)
by by apply loc_not_in_set_is_fresh.
assert (σ2 !! = None)
by by (simpl ; eapply not_elem_of_dom).
specialize (Hadq Hloc) as Hsafe % safe_adequate.
by eapply safe_translation__safe.
Qed.
End Simulation.
\ No newline at end of file
......@@ -43,19 +43,15 @@ Class timeCreditHeapPreG Σ := {
timeCreditHeapPreG_inG :> inG Σ (authR natUR) ;
}.
Class timeCreditLoc := {
timeCreditLoc_loc : loc ;
}.
Class timeCreditHeapG Σ := {
timeCreditHeapG_heapG :> heapG Σ ;
timeCreditHeapG_inG :> inG Σ (authR natUR) ;
timeCreditHeapG_loc :> timeCreditLoc ;
timeCreditHeapG_loc :> TickCounter ;
timeCreditHeapG_name : gname ;
}.
Local Notation γ := timeCreditHeapG_name.
Local Notation := timeCreditLoc_loc.
Local Notation := tick_counter.
......@@ -63,19 +59,16 @@ Local Notation ℓ := timeCreditLoc_loc.
* Implementation and specification of `TC` and `tick`
*)
Section Tick.
Context `{timeCreditLoc}.
(* This code is irrelevant for tick_spec but has to be unsafe for proving
* the safety theorem: *)
Definition fail : val :=
λ: <>, #() #().
(* This code is irrelevant for tick_spec but has to be unsafe for proving
* the safety theorem: *)
Definition fail : val :=
λ: <>, #() #().
Definition tick {_:TickCounter} : val :=
tick fail.
Definition tick : val :=
tick fail .
End Tick.
Global Instance Tick_tick (Hloc : TickCounter) : Tick :=
{| Translation.tick := tick |}.
......@@ -201,7 +194,7 @@ End TickSpec.
Section Tick_lemmas.
Context `{timeCreditLoc}.
Context {Hloc : TickCounter}.
(* Semantics in the successful case. *)
......@@ -320,44 +313,14 @@ End Tick_lemmas.
* Simulation
*)
Notation tctranslation := (translation tick).
Notation tctranslationV := (translationV tick).
Notation tctranslationS := (translationS tick).
Notation tctranslationKi := (translationKi tick).
Notation tctranslationK := (translationK tick).
Notation "E« e »" := (tctranslation e%E).
Notation "V« v »" := (tctranslationV v%V).
Notation "Ki« ki »" := (tctranslationKi ki).
Notation "K« K »" := (tctranslationK K).
Notation "S« σ »" := (tctranslationS σ%V).
Notation "S« σ , n »" := (<[ := LitV (LitInt n%nat)]> (tctranslationS σ%V)).
Notation "T« t »" := (tctranslation <$> t%E).
Notation "« e »" := (tctranslation e%E).
Notation "« e »" := (tctranslation e%E) : expr_scope.
Notation "« v »" := (tctranslationV v%V) : val_scope.
(* for some reason, these notations make parsing fail,
* even if they only regard printing *)
(*
Notation "« e »" := (tctranslation e%E) (only printing).
Notation "« v »" := (tctranslationV v%V) (only printing).
Notation "« ki »" := (tctranslationKi ki) (only printing).
Notation "« K »" := (tctranslationK K) (only printing).
Notation "« σ »" := (tctranslationS σ%V) (only printing).
Notation "« σ , n »" := (<[ := LitV (LitInt n%nat)]> (tctranslationS σ%V)) (only printing).
Notation "« t »" := (tctranslation <$> t%E) (only printing).
*)
Section Simulation.
Context `{Hloc : timeCreditLoc}.
Context {Hloc : TickCounter}.
(* Simulation in the successful case. *)
Definition simulation_exec_success := simulation_exec_success _ tick exec_tick_success.
Definition simulation_exec_success' := simulation_exec_success' _ tick exec_tick_success.
Definition simulation_exec_success := simulation_exec_success fail.
Definition simulation_exec_success' := simulation_exec_success' fail.
(* Simulation in the failing case. *)
......@@ -445,7 +408,7 @@ Section Simulation.
apply simulation_exec_success ; assumption.
- by eapply simulation_exec_failure_now.
}
apply (elem_of_list_fmap_1 tctranslation) in E3.
apply (elem_of_list_fmap_1 translation) in E3.
eapply not_safe_exec ; eassumption.
Qed.
......@@ -465,7 +428,7 @@ Section Soundness.
Proof.
intro. exists (m - S n)%nat. lia.
Qed.
Lemma safe_tctranslation__bounded `{timeCreditLoc} m e σ t2 σ2 n :
Lemma safe_tctranslation__bounded {Hloc : TickCounter} m e σ t2 σ2 n :
is_closed [] e
σ2 !! = None
safe «e» S«σ, m»
......@@ -481,40 +444,28 @@ Section Soundness.
Lemma adequate_tctranslation__bounded m (φ : val Prop) e σ :
is_closed [] e
( `{timeCreditLoc}, adequate NotStuck «e» S«σ, m» (φ invtranslationV))
( `{TickCounter}, adequate NotStuck «e» S«σ, m» (φ invtranslationV))
bounded_time e σ m.
Proof.
intros Hclosed Hadq.
intros t2 σ2 k.
(* build a location which is not in the domain of σ2: *)
pose (Build_timeCreditLoc (fresh (dom (gset loc) σ2))) as Hloc.
pose (Build_TickCounter (fresh (dom (gset loc) σ2))) as Hloc.
assert (σ2 !! = None)
by (unfold ; eapply not_elem_of_dom, is_fresh).
specialize (Hadq Hloc) as Hsafe % safe_adequate.
by eapply safe_tctranslation__bounded.
Qed.
Lemma adequate_tctranslation__adequate m (φ : val Prop) e σ :
is_closed [] e
( `{timeCreditLoc}, adequate NotStuck «e» S«σ, m» (φ invtranslationV))
adequate_n NotStuck m e σ φ.
Proof.
intros.
apply (adequate_translation__adequate (λ 1, @tick {| timeCreditLoc_loc := 1 |})).
- intro 1.
rewrite (_ : 1 = @timeCreditLoc_loc {| timeCreditLoc_loc := 1 |}) ; last done.
apply exec_tick_success.
- done.
- intro 1.
rewrite (_ : 1 = @timeCreditLoc_loc {| timeCreditLoc_loc := 1 |}) ; last done.
done.
Qed.
Definition adequate_tctranslation__adequate := adequate_translation__adequate fail.
(* now lets combine the three results. *)
Lemma adequate_tctranslation__adequate_and_bounded m (φ : val Prop) e σ :
is_closed [] e
( (k : nat), (k m)%nat `{timeCreditLoc}, adequate NotStuck «e» S«σ, k» (φ invtranslationV))
( (k : nat), (k m)%nat
`{TickCounter}, adequate NotStuck «e» S«σ, k» (φ invtranslationV)
)
adequate NotStuck e σ φ bounded_time e σ m.
Proof.
intros Hclosed Hadq.
......@@ -540,7 +491,8 @@ Section Soundness.
TICKCTXT -
{{{ TC m }}} «e» {{{ v, RET v ; ⌜ψ v }}}
)
`{timeCreditHeapPreG Σ} `{timeCreditLoc} σ, (k : nat), (k m)%nat adequate NotStuck «e» S«σ,k» ψ.
`{timeCreditHeapPreG Σ} `{TickCounter} σ,
(k : nat), (k m)%nat adequate NotStuck «e» S«σ,k» ψ.
Proof.
intros Hspec HpreG Hloc σ k Ik.
(* apply the adequacy results. *)
......@@ -597,8 +549,9 @@ Section Soundness.
Theorem abstract_spec_tctranslation__adequate_and_bounded {Σ} m (φ : val Prop) e :
is_closed [] e
( `{heapG Σ} (TC : nat iProp Σ) (tick : val),
let _ := {| Translation.tick := tick |} in
TC_interface TC tick -
{{{ TC m }}} translation tick e {{{ v, RET v ; ⌜φ (invtranslationV v) }}}
{{{ TC m }}} «e» {{{ v, RET v ; ⌜φ (invtranslationV v) }}}
)
{_ : timeCreditHeapPreG Σ} σ,
adequate NotStuck e σ φ bounded_time e σ m.
......
......@@ -11,7 +11,7 @@ Implicit Type K : ectx heap_ectx_lang.
Implicit Type m n : nat.
Local Notation γ := timeCreditHeapG_name.
Local Notation := timeCreditLoc_loc.
Local Notation := tick_counter.
(* In general, one can prove:
* if the translated program with the counter initialized to m is safe,
......@@ -54,7 +54,7 @@ Local Notation ℓ := timeCreditLoc_loc.
(* assuming the safety of the translated expression,
* a proof that the original expression is safe. *)
Lemma safe_tctranslation__safe_here `{timeCreditLoc} m e σ :
Lemma safe_tctranslation__safe_here {Hloc : TickCounter} m e σ :
is_closed [] e
loc_fresh_in_expr e
safe «e» S«σ, m»
......@@ -105,7 +105,7 @@ Proof.
(* or «ki»[«v»] reduces to something: this is precisely what we need. *)
* exact Hred.
Qed.
Lemma safe_tctranslation__safe `{timeCreditLoc} m e σ t2 σ2 e2 :
Lemma safe_tctranslation__safe {Hloc : TickCounter} m e σ t2 σ2 e2 :
is_closed [] e
loc_fresh_in_expr e2
σ2 !! = None
......@@ -135,7 +135,7 @@ Qed.
(* assuming the adequacy of the translated expression,
* a proof that the original expression has adequate results. *)
Lemma adequate_tctranslation__adequate_result `{timeCreditLoc} m (φ : val Prop) e σ t2 σ2 v2 :
Lemma adequate_tctranslation__adequate_result {Hloc : TickCounter} m (φ : val Prop) e σ t2 σ2 v2 :
is_closed [] e
σ2 !! = None
adequate NotStuck «e» S«σ, m» (φ invtranslationV)
......@@ -145,7 +145,7 @@ Proof.
intros Hclosed Hfresh Hadq [n Hnsteps] % rtc_nsteps.
assert (safe «e» S«σ, m») as Hsafe by by eapply safe_adequate.
assert (n m)%nat by by eapply safe_tctranslation__bounded.
replace (φ v2) with ((φ invtranslationV) (tctranslationV v2))
replace (φ v2) with ((φ invtranslationV) (translationV v2))
by (simpl ; by rewrite invtranslationV_translationV).
eapply adequate_result ; first done.
change [«e»%E] with T«[e]».
......@@ -157,7 +157,7 @@ Qed.
Lemma adequate_tctranslation__adequate_alt m (φ : val Prop) e σ :
is_closed [] e
( `{timeCreditLoc}, adequate NotStuck «e» S«σ, m» (φ invtranslationV))
( `{TickCounter}, adequate NotStuck «e» S«σ, m» (φ invtranslationV))
adequate NotStuck e σ φ.
Proof.
intros Hclosed Hadq.
......@@ -165,7 +165,7 @@ Proof.
(* (1) adequate result: *)
- intros t2 σ2 v2 Hsteps.
(* build a location which is not in the domain of σ2: *)
pose (Build_timeCreditLoc (fresh (dom (gset loc) σ2))) as Hloc.
pose (Build_TickCounter (fresh (dom (gset loc) σ2))) as Hloc.
assert (σ2 !! = None)
by (simpl ; eapply not_elem_of_dom, is_fresh).
by eapply adequate_tctranslation__adequate_result.
......@@ -174,7 +174,7 @@ Proof.
(* build a location which is fresh in e2 and in the domain of σ2: *)
pose (set1 := loc_set_of_expr e2 : gset loc).
pose (set2 := dom (gset loc) σ2 : gset loc).
pose (Build_timeCreditLoc (fresh (set1 set2))) as Hloc.
pose (Build_TickCounter (fresh (set1 set2))) as Hloc.
eassert ( set1 set2) as [H1 H2] % not_elem_of_union
by (unfold ; apply is_fresh).
assert (loc_fresh_in_expr e2)
......@@ -246,7 +246,7 @@ Lemma spec_tctranslation__bounded {Σ} m (ψ : val → Prop) e :
TICKCTXT -
{{{ TC m }}} «e» {{{ v, RET v ; ⌜ψ v }}}
)
`{!timeCreditLoc} `{!timeCreditHeapPreG Σ} σ1 t2 σ2 (z : Z),
`{TickCounter} `{timeCreditHeapPreG Σ} σ1 t2 σ2 (z : Z),
rtc step ([«e»], S«σ1, m») (T«t2», S«σ2, z»)
0 z.
Proof.
......@@ -303,7 +303,7 @@ Proof.
Qed.
(* The simulation lemma with no assumption that m n. *)
Axiom simulation_exec_alt : `{timeCreditLoc} m n t1 σ1 t2 σ2,
Axiom simulation_exec_alt : {Hloc : TickCounter} m n t1 σ1 t2 σ2,
σ2 !! = None
Forall (is_closed []) t1
nsteps step m (t1, σ1) (t2, σ2)
......@@ -320,7 +320,7 @@ Lemma spec_tctranslation__bounded' {Σ} m (ψ : val → Prop) e :
Proof.
intros Hclosed Hspec HtcPreG σ t2 σ2 n Hnsteps.
(* build a location which is not in the domain of σ2: *)
pose (Build_timeCreditLoc (fresh (dom (gset loc) σ2))) as Hloc.
pose (Build_TickCounter (fresh (dom (gset loc) σ2))) as Hloc.
assert (σ2 !! = None)
by (unfold ; eapply not_elem_of_dom, is_fresh).
eapply simulation_exec_alt in Hnsteps ; auto.
......
......@@ -69,22 +69,18 @@ Class timeReceiptHeapPreG Σ := {
timeReceiptHeapPreG_inG2 :> inG Σ (authR mnatUR) ;
}.
Class timeReceiptLoc := {
timeReceiptLoc_loc : loc ;
}.
Class timeReceiptHeapG Σ := {
timeReceiptHeapG_heapG :> heapG Σ ;
timeReceiptHeapG_inG1 :> inG Σ (authR natUR) ;
timeReceiptHeapG_inG2 :> inG Σ (authR mnatUR) ;
timeReceiptHeapG_loc :> timeReceiptLoc ;
timeReceiptHeapG_loc :> TickCounter ;
timeReceiptHeapG_name1 : gname ;
timeReceiptHeapG_name2 : gname ;
}.
Local Notation γ1 := timeReceiptHeapG_name1.
Local Notation γ2 := timeReceiptHeapG_name2.
Local Notation := timeReceiptLoc_loc.
Local Notation := tick_counter.
......@@ -92,17 +88,14 @@ Local Notation ℓ := timeReceiptLoc_loc.
* Implementation and specification of `TR` and `tock`
*)
Section Tock.
Context `{timeReceiptLoc}.
Definition loop : val :=
rec: "f" <> := "f" #().
Definition loop : val :=
rec: "f" <> := "f" #().
Definition tock {_:TickCounter} : val :=
tick loop.
Definition tock : val :=
tick loop .
End Tock.
Global Instance Tick_tock (Hloc: TickCounter) : Tick :=
{| Translation.tick := tock |}.
......@@ -300,65 +293,19 @@ End TockSpec.
* Simulation
*)
Notation trtranslation := (translation tock).
Notation trtranslationV := (translationV tock).
Notation trtranslationS := (translationS tock).
Notation trtranslationKi := (translationKi tock).
Notation trtranslationK := (translationK tock).
Notation "E« e »" := (trtranslation e%E).
Notation "V« v »" := (trtranslationV v%V).
Notation "Ki« ki »" := (trtranslationKi ki).
Notation "K« K »" := (trtranslationK K).
Notation "S« σ »" := (trtranslationS σ%V).
Notation "S« σ , n »" := (<[ := LitV (LitInt n%nat)]> (trtranslationS σ%V)).
Notation "T« t »" := (trtranslation <$> t%E).
Notation "« e »" := (trtranslation e%E).
Notation "« e »" := (trtranslation e%E) : expr_scope.
Notation "« v »" := (trtranslationV v%V) : val_scope.
(* for some reason, these notations make parsing fail,
* even if they only regard printing *)
(*
Notation "« e »" := (trtranslation e%E) (only printing).
Notation "« v »" := (trtranslationV v%V) (only printing).
Notation "« ki »" := (trtranslationKi ki) (only printing).
Notation "« K »" := (trtranslationK K) (only printing).
Notation "« σ »" := (trtranslationS σ%V) (only printing).
Notation "« σ , n »" := (<[ := LitV (LitInt n%nat)]> (trtranslationS σ%V)) (only printing).
Notation "« t »" := (trtranslation <$> t%E) (only printing).
*)
Section Soundness.
Lemma adequate_trtranslation__adequate m (φ : val Prop) e σ :
is_closed [] e
( `{timeReceiptLoc}, adequate NotStuck «e» S«σ, m» (φ invtranslationV))
adequate_n NotStuck m e σ φ.
Proof.
intros.
apply (adequate_translation__adequate (λ 1, @tock {| timeReceiptLoc_loc := 1 |})).
- intro 1.
rewrite (_ : 1 = @timeReceiptLoc_loc {| timeReceiptLoc_loc := 1 |}) ; last done.
apply exec_tick_success.
- done.
- intro 1.
rewrite (_ : 1 = @timeReceiptLoc_loc {| timeReceiptLoc_loc := 1 |}) ; last done.
done.
Qed.
Definition adequate_trtranslation__adequate := adequate_translation__adequate loop.
(* derive the adequacy of the translated program from a Hoare triple in Iris. *)
Lemma spec_trtranslation__adequate_translation {Σ} (nmax : nat) (ψ : val Prop) e :
(0 < nmax)%nat
( `{!timeReceiptHeapG Σ},
( `{timeReceiptHeapG Σ},
TOCKCTXT nmax -
{{{ True }}} «e» {{{ v, RET v ; ⌜ψ v }}}
)
`{!timeReceiptHeapPreG Σ} `{!timeReceiptLoc} σ, adequate NotStuck «e» S«σ,nmax-1» ψ.
`{timeReceiptHeapPreG Σ} `{TickCounter} σ, adequate NotStuck «e» S«σ,nmax-1» ψ.
Proof.
intros Inmax Hspec HpreG Hloc σ.
(* apply the adequacy results. *)
......@@ -401,7 +348,7 @@ Section Soundness.
Lemma spec_trtranslation__adequate {Σ} (nmax : nat) (φ : val Prop) e :
(0 < nmax)%nat
is_closed [] e
( `{!timeReceiptHeapG Σ},
( `{timeReceiptHeapG Σ},
TOCKCTXT nmax -
{{{ True }}} «e» {{{ v, RET v ; ⌜φ (invtranslationV v) }}}
)
......@@ -416,9 +363,10 @@ Section Soundness.
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) }}}
( `{heapG Σ} (TR TRdup : nat iProp Σ) (tock : val),
let _ := {| Translation.tick := tock |} in
TR_interface nmax TR TRdup tock -
{{{ True }}} «e» {{{ v, RET v ; ⌜φ (invtranslationV v) }}}
)
{_ : timeReceiptHeapPreG Σ} σ,
adequate_n NotStuck (nmax-1) e σ φ.
......
......@@ -16,9 +16,14 @@ Implicit Type m n : nat.
* Translation with any arbitrary expression for [tick]
*)
Class Tick := { tick : val }.
Section Translation.
Variable tick : val.
Context {Htick : Tick}.
Definition tick_aux : val :=
(λ: "f" "x", "f" #() (tick "x"))%V.
Fixpoint translation (e : expr) : expr :=
match e with
......@@ -39,10 +44,9 @@ Section Translation.