Commit 21f2b119 authored by MEVEL Glen's avatar MEVEL Glen

Renamings

parent e3611719
...@@ -404,7 +404,7 @@ Section SimulationLemma. ...@@ -404,7 +404,7 @@ Section SimulationLemma.
(* assuming the safety of the translated expression, (* assuming the safety of the translated expression,
* a proof that the original expression is m-safe. *) * a proof that the original expression is m-safe. *)
Lemma safe_translation__safe_here m e σ : Lemma safe_translation__nsafe_here m e σ :
loc_fresh_in_expr e loc_fresh_in_expr e
(m > 0)%nat (m > 0)%nat
safe «e» S«σ, m» safe «e» S«σ, m»
...@@ -468,7 +468,7 @@ Section SimulationLemma. ...@@ -468,7 +468,7 @@ Section SimulationLemma.
(* — or «ki»[«v»] reduces to something: this is precisely what we need. *) (* — or «ki»[«v»] reduces to something: this is precisely what we need. *)
* exact Hred. * exact Hred.
Qed. Qed.
Lemma safe_translation__safe m n e σ t2 σ2 e2 : Lemma safe_translation__nsafe m n e σ t2 σ2 e2 :
loc_fresh_in_expr e2 loc_fresh_in_expr e2
σ2 !! = None σ2 !! = None
safe «e» S«σ, m» safe «e» S«σ, m»
...@@ -486,7 +486,7 @@ Section SimulationLemma. ...@@ -486,7 +486,7 @@ Section SimulationLemma.
- change [«e»] with T«[e]». apply simulation_exec_success' ; [ assumption | lia | assumption ]. - change [«e»] with T«[e]». apply simulation_exec_success' ; [ assumption | lia | assumption ].
} }
assert (m - n > 0)%nat by lia. assert (m - n > 0)%nat by lia.
by eapply safe_translation__safe_here. by eapply safe_translation__nsafe_here.
Qed. Qed.
(* assuming the adequacy of the translated expression, (* assuming the adequacy of the translated expression,
...@@ -494,7 +494,7 @@ Section SimulationLemma. ...@@ -494,7 +494,7 @@ Section SimulationLemma.
(* FIXME : this is a weaker result than the adequacy result of Iris, (* FIXME : this is a weaker result than the adequacy result of Iris,
where the predicate can also speak about the final state. *) where the predicate can also speak about the final state. *)
Lemma adequate_translation__adequate_result m n φ e σ t2 σ2 v2 : Lemma adequate_translation__nadequate_result m n φ e σ t2 σ2 v2 :
σ2 !! = None σ2 !! = None
adequate NotStuck «e» S«σ, m» (λ v σ, φ (invtranslationV v)) adequate NotStuck «e» S«σ, m» (λ v σ, φ (invtranslationV v))
nsteps erased_step n ([e], σ) (Val v2 :: t2, σ2) nsteps erased_step n ([e], σ) (Val v2 :: t2, σ2)
...@@ -515,7 +515,7 @@ End SimulationLemma. (* we close the section here as we now want to quantify ove ...@@ -515,7 +515,7 @@ End SimulationLemma. (* we close the section here as we now want to quantify ove
(* now let’s combine the two results. *) (* now let’s combine the two results. *)
Lemma adequate_translation__adequate m φ e σ : Lemma adequate_translation__nadequate m φ e σ :
( {Hloc : TickCounter}, adequate NotStuck «e» S«σ, m» (λ v σ, φ (invtranslationV v))) ( {Hloc : TickCounter}, adequate NotStuck «e» S«σ, m» (λ v σ, φ (invtranslationV v)))
nadequate NotStuck m e σ φ. nadequate NotStuck m e σ φ.
Proof. Proof.
...@@ -527,7 +527,7 @@ Proof. ...@@ -527,7 +527,7 @@ Proof.
pose (Hloc := Build_TickCounter (fresh (dom (gset loc) σ2)) : TickCounter). pose (Hloc := Build_TickCounter (fresh (dom (gset loc) σ2)) : TickCounter).
assert (σ2 !! = None) assert (σ2 !! = None)
by (simpl ; eapply not_elem_of_dom, is_fresh). by (simpl ; eapply not_elem_of_dom, is_fresh).
by eapply adequate_translation__adequate_result. by eapply adequate_translation__nadequate_result.
(* (2) safety: *) (* (2) safety: *)
- intros n t2 σ2 e2 _ Hnsteps Inm He2. - intros n t2 σ2 e2 _ Hnsteps Inm He2.
(* build a location ℓ which is fresh in e2 and in the domain of σ2: *) (* build a location ℓ which is fresh in e2 and in the domain of σ2: *)
...@@ -541,7 +541,7 @@ Proof. ...@@ -541,7 +541,7 @@ Proof.
assert (σ2 !! = None) assert (σ2 !! = None)
by by (simpl ; eapply not_elem_of_dom). by by (simpl ; eapply not_elem_of_dom).
specialize (Hadq Hloc) as Hsafe % safe_adequate. specialize (Hadq Hloc) as Hsafe % safe_adequate.
by eapply safe_translation__safe. by eapply safe_translation__nsafe.
Qed. Qed.
End Simulation. End Simulation.
...@@ -380,7 +380,7 @@ Section Soundness. ...@@ -380,7 +380,7 @@ Section Soundness.
by eapply safe_tctranslation__bounded. by eapply safe_tctranslation__bounded.
Qed. Qed.
Definition adequate_tctranslation__adequate := adequate_translation__adequate fail. Definition adequate_tctranslation__nadequate := adequate_translation__nadequate fail.
(* now let’s combine the three results. *) (* now let’s combine the three results. *)
...@@ -394,7 +394,7 @@ Section Soundness. ...@@ -394,7 +394,7 @@ Section Soundness.
assert (bounded_time e σ m) as Hbounded assert (bounded_time e σ m) as Hbounded
by (eapply adequate_tctranslation__bounded, Hadq ; lia). by (eapply adequate_tctranslation__bounded, Hadq ; lia).
assert (nadequate NotStuck (m + 1) e σ φ) as Hadqm assert (nadequate NotStuck (m + 1) e σ φ) as Hadqm
by (apply adequate_tctranslation__adequate, Hadq ; lia). by (apply adequate_tctranslation__nadequate, Hadq ; lia).
clear Hadq. clear Hadq.
split ; last done. split ; last done.
split. split.
...@@ -408,7 +408,7 @@ Section Soundness. ...@@ -408,7 +408,7 @@ Section Soundness.
(* finally, derive the adequacy assumption from a Hoare triple in Iris. *) (* finally, derive the adequacy assumption from a Hoare triple in Iris. *)
Lemma spec_tctranslation__adequate {Σ} m ψ e : Lemma spec_tctranslation__adequate_translation {Σ} m ψ e :
( `{timeCreditHeapG Σ}, ( `{timeCreditHeapG Σ},
TC_invariant - TC_invariant -
{{{ TC m }}} «e» {{{ v, RET v ; ⌜ψ v }}} {{{ TC m }}} «e» {{{ v, RET v ; ⌜ψ v }}}
...@@ -464,7 +464,7 @@ Section Soundness. ...@@ -464,7 +464,7 @@ Section Soundness.
Proof. Proof.
intros Hspec HpreG σ. intros Hspec HpreG σ.
apply adequate_tctranslation__adequate_and_bounded. apply adequate_tctranslation__adequate_and_bounded.
intros k Ik Hloc. by eapply spec_tctranslation__adequate. intros k Ik Hloc. by eapply spec_tctranslation__adequate_translation.
Qed. Qed.
(* The abstract version of the theorem: *) (* The abstract version of the theorem: *)
......
...@@ -35,7 +35,7 @@ Local Notation ℓ := tick_counter. ...@@ -35,7 +35,7 @@ Local Notation ℓ := tick_counter.
* if the Hoare triple { TC m } «e» { φ } holds, * if the Hoare triple { TC m } «e» { φ } holds,
* then FOR ALL m' ≥ m, * then FOR ALL m' ≥ m,
* the translated program with the counter initialized to m' is safe. * the translated program with the counter initialized to m' is safe.
* This is lemma [<spec_tctranslation__adequate_tctranslation>] in `TimeCredits.v`. * This is lemma [spec_tctranslation__adequate_translation] in `TimeCredits.v`.
* *
* Hence from the Hoare triple we can deduce that the source program * Hence from the Hoare triple we can deduce that the source program
* (1) computes in at most m steps (by taking m' = m), and * (1) computes in at most m steps (by taking m' = m), and
......
...@@ -295,12 +295,12 @@ End TickSpec. ...@@ -295,12 +295,12 @@ End TickSpec.
(* (*
* Simulation * Soundness
*) *)
Section Soundness. Section Soundness.
Definition adequate_trtranslation__adequate := adequate_translation__adequate loop. Definition adequate_trtranslation__nadequate := adequate_translation__nadequate loop.
(* derive the adequacy of the translated program from a Hoare triple in Iris. *) (* derive the adequacy of the translated program from a Hoare triple in Iris. *)
...@@ -351,7 +351,7 @@ Section Soundness. ...@@ -351,7 +351,7 @@ Section Soundness.
iApply (Hspec with "Hinv") ; auto. iApply (Hspec with "Hinv") ; auto.
Qed. Qed.
Theorem spec_trtranslation__adequate {Σ} nmax φ e : Theorem spec_trtranslation__nadequate {Σ} nmax φ e :
(0 < nmax)%nat (0 < nmax)%nat
( `{timeReceiptHeapG Σ}, ( `{timeReceiptHeapG Σ},
TR_invariant nmax - TR_invariant nmax -
...@@ -361,11 +361,11 @@ Section Soundness. ...@@ -361,11 +361,11 @@ Section Soundness.
nadequate NotStuck (nmax-1) e σ φ. nadequate NotStuck (nmax-1) e σ φ.
Proof. Proof.
intros Inmax Hspec HpreG σ. intros Inmax Hspec HpreG σ.
eapply adequate_trtranslation__adequate. eapply adequate_trtranslation__nadequate.
intros Hloc. by eapply spec_trtranslation__adequate_translation. intros Hloc. by eapply spec_trtranslation__adequate_translation.
Qed. Qed.
Theorem abstract_spec_trtranslation__adequate {Σ} nmax φ e : Theorem abstract_spec_trtranslation__nadequate {Σ} nmax φ e :
(0 < nmax)%nat (0 < nmax)%nat
( `{heapG Σ, Tick} (TR TRdup : nat iProp Σ), ( `{heapG Σ, Tick} (TR TRdup : nat iProp Σ),
TR_interface nmax TR TRdup - TR_interface nmax TR TRdup -
...@@ -375,7 +375,7 @@ Section Soundness. ...@@ -375,7 +375,7 @@ Section Soundness.
nadequate NotStuck (nmax-1) e σ φ. nadequate NotStuck (nmax-1) e σ φ.
Proof. Proof.
intros Inmax Hspec HpreG σ. intros Inmax Hspec HpreG σ.
eapply spec_trtranslation__adequate; try done. eapply spec_trtranslation__nadequate; try done.
clear HpreG. iIntros (HtrHeapG) "#Hinv". clear HpreG. iIntros (HtrHeapG) "#Hinv".
iApply Hspec. by iApply TR_implementation. iApply Hspec. by iApply TR_implementation.
Qed. Qed.
......
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