Commit 676af6f9 authored by Glen Mével's avatar Glen Mével

more proof-mode tactics for time credits; the spec of thunk operations now gives their cost

parent 36d2a361
......@@ -127,20 +127,19 @@ Proof.
- simpl.
rewrite !translation_of_val.
iDestruct "Hl" as %->.
wp_tick ; unlock sum_list ; wp_rec.
wp_tick ; wp_match ; do 2 wp_lam ; wp_tick.
wp_tick_rec. wp_tick_match.
by iApply "Post".
- replace (3 + 10 * length (x :: l))%nat with (13 + 10 * length l)%nat by (simpl ; lia).
simpl.
rewrite !translation_of_val. setoid_rewrite translation_of_val.
iDestruct "Hl" as (p) "[-> Hl]" ; iDestruct "Hl" as (v) "[Hp Hl]".
wp_tick ; unlock sum_list ; wp_rec.
wp_tick ; wp_match ; do 2 wp_lam ; wp_tick ; wp_lam.
wp_tick ; wp_load. wp_tick ; wp_proj. wp_tick ; wp_let.
wp_tick ; wp_load. wp_tick ; wp_proj. wp_tick ; wp_let.
wp_tick_rec.
wp_tick_match ; wp_lam.
wp_tick_load. wp_tick_proj. wp_tick_let.
wp_tick_load. wp_tick_proj. wp_tick_let.
iDestruct "Htc" as "[Htc1 Htc]".
wp_apply ("IH" with "Hl Htc"). iIntros "Hl".
wp_tick ; wp_op.
wp_tick_op.
iApply "Post". eauto with iFrame.
Qed.
......@@ -181,18 +180,18 @@ Proof.
iInduction n as [|n'] "IH" forall (Φ).
- simpl.
rewrite !translation_of_val.
wp_tick ; unlock make_list ; wp_rec. wp_tick ; wp_op. wp_tick ; wp_if.
wp_tick_rec. wp_tick_op. wp_tick_if.
by iApply "Post".
- replace (3 + 5 * S n')%nat with (8 + 5 * n')%nat by lia.
simpl.
rewrite !translation_of_val.
wp_tick ; unlock make_list ; wp_rec. wp_tick ; wp_op. wp_tick ; wp_if.
wp_tick ; wp_op.
wp_tick_rec. wp_tick_op. wp_tick_if.
wp_tick_op.
assert (Z.of_nat n' = Z.of_nat (S n') - 1) as Eq by lia ; simpl in Eq ; destruct Eq.
iDestruct "Htc" as "[Htc1 Htc]".
wp_apply ("IH" with "Htc"). iIntros (v') "Hl".
change (Z.pos $ Pos.of_succ_nat n') with (Z.of_nat $ S n').
wp_tick ; wp_alloc p.
wp_tick_alloc p.
iApply "Post". eauto with iFrame.
Qed.
......@@ -279,6 +278,7 @@ 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.
......@@ -287,6 +287,7 @@ Proof.
iApply ("Post" with "[%]"). done.
- assumption.
Restart.
*)
apply (spec_tctranslation__adequate_and_bounded' (Σ:=Σ)).
- by intros _ ->.
- rewrite !andb_True ; repeat split ; apply is_closed_of_val.
......
......@@ -88,15 +88,15 @@ Section Thunk.
Lemma create_spec p nc φ f :
TICKCTXT -
{{{ ( {{{ TC nc }}} f #() {{{ v, RET v ; φ v }}} ) }}}
create f
{{{ TC 1 ( {{{ TC nc }}} f #() {{{ v, RET v ; φ v }}} ) }}}
«create» f
{{{ (t : loc), RET #t ; Thunk p t nc φ }}}.
Proof.
iIntros "#Htickinv" (Φ) "!# Hf Post".
iIntros "#Htickinv" (Φ) "!# [? Hf] Post".
iDestruct (zero_TC with "Htickinv") as ">Htc0".
iMod (auth_mnat_alloc 0) as (γ) "[Hγ● Hγ◯]".
iApply wp_fupd.
wp_lam. wp_alloc t.
unlock create ; wp_lam. wp_tick_alloc t.
iApply "Post".
iExists γ, nc ; rewrite (_ : nc - nc = 0)%nat ; last lia.
iFrame "Hγ◯".
......@@ -107,15 +107,17 @@ Section Thunk.
Lemma force_spec p F t φ :
(thunkN t) F
( (v : val), φ v - φ v φ v)
{{{ Thunk p t 0 φ na_own p F }}}
force #t
TICKCTXT -
{{{ TC 7 Thunk p t 0 φ na_own p F }}}
«force» #t
{{{ v, RET v ; φ v na_own p F }}}.
Proof.
iIntros (? Hφdup Φ) "[#Hthunk Hp] Post".
iIntros (? Hφdup).
iIntros "#Htickinv" (Φ) "!# (? & #Hthunk & Hp) Post".
iDestruct "Hthunk" as (γ nc) "#[Hthunkinv Hγ◯]".
rewrite (_ : nc - 0 = nc)%nat ; last lia.
iApply wp_fupd.
wp_rec.
unlock force ; wp_rec.
(* reading the thunk *)
iDestruct (na_inv_open p F (thunkN t) with "Hthunkinv Hp")
as ">(Hthunk & Hp & Hclose)" ; [done|done|] ;
......@@ -124,11 +126,11 @@ Section Thunk.
| iDestruct "Hevaluated" as (v) "(>Ht & Hv & >%)" ].
(* (1) if it is UNEVALUATED, we evaluate it: *)
{
wp_load. wp_match.
wp_tick_load. wp_tick_match ; wp_let.
iDestruct (own_auth_mnat_le with "Hγ● Hγ◯") as %I.
iDestruct (TC_weaken _ _ I with "Htc") as "Htc".
wp_apply ("Hf" with "Htc") ; iIntros (v) "Hv".
wp_let. wp_store.
wp_tick ; wp_apply ("Hf" with "Htc") ; iIntros (v) "Hv".
wp_tick_let. wp_tick_store. wp_tick_seq.
iApply "Post".
iDestruct (Hφdup with "Hv") as "[Hv $]".
iApply "Hclose". iFrame "Hp".
......@@ -136,7 +138,7 @@ Section Thunk.
}
(* (2) if it is EVALUATED, we get the result which is already memoized: *)
{
wp_load. wp_match.
wp_tick_load. wp_tick_match ; wp_let.
iApply "Post".
iDestruct (Hφdup with "Hv") as "[Hv $]".
iApply "Hclose". iFrame "Hp".
......
......@@ -640,4 +640,27 @@ Ltac wp_tick :=
| |- envs_entails _ (twp ?s ?E ?e ?Q) =>
fail "wp_tick is not implemented for twp"
| _ => fail "wp_tick: not a 'wp'"
end.
\ No newline at end of file
end.
Ltac wp_tick_rec :=
wp_tick ; first
[ wp_rec
| match goal with
| |-context [ App ?f _ ] =>
unlock f ; wp_rec
| |-context [ App (translation ?f) _ ] =>
unlock f ; wp_rec
| |-context [ App (of_val (translationV ?f)) _ ] =>
unlock f ; wp_rec
end
| fail ].
Ltac wp_tick_lam := wp_tick_rec.
Ltac wp_tick_let := wp_tick ; wp_let.
Ltac wp_tick_seq := wp_tick.
Ltac wp_tick_op := wp_tick ; wp_op.
Ltac wp_tick_if := wp_tick ; wp_if.
Ltac wp_tick_match := wp_tick ; wp_match ; do 2 wp_lam ; wp_tick.
Ltac wp_tick_proj := wp_tick ; wp_proj.
Ltac wp_tick_alloc loc := wp_tick ; wp_alloc loc.
Ltac wp_tick_load := wp_tick ; wp_load.
Ltac wp_tick_store := wp_tick ; wp_store.
\ No newline at end of file
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