Commit 7b3e515e authored by Dan Frumin's avatar Dan Frumin

Fix the rest of the tests wrt new alloc rule

parent 3216e98d
......@@ -22,6 +22,11 @@ Definition factorial : val := λ: "n",
Section factorial_spec.
Context `{amonadG Σ}.
Ltac etaprod l :=
compute[cloc_add];
rewrite ?Nat.add_0_r;
assert ((l.1, l.2) = l) as -> by (destruct l; auto).
Lemma incr_spec (l : cloc) (n : Z) R Φ :
l C #n - (l C[LLvl] #(n+1) - Φ #(n+1)) -
AWP incr (cloc_to_val l) @ R {{ Φ }}.
......@@ -56,24 +61,24 @@ Section factorial_spec.
AWP factorial #n @ R {{ v, v = #(fact n) }}%I.
Proof.
awp_lam.
iApply awp_bind. awp_alloc_ret r "[Hr _]".
iApply awp_bind. awp_alloc_ret c "[Hc _]".
iApply awp_bind. awp_alloc_ret r "[Hr _]". etaprod r.
iApply awp_bind. awp_alloc_ret c "[Hc _]". etaprod c.
iApply a_sequence_spec'. iNext.
iApply (awp_wand _ (λ _, (c,O) C #n (r,O) C #(fact n))%I with "[Hr Hc]").
- iApply ((factorial_body_spec n 0 (c,O) (r,O)) with "[$Hr $Hc]"); eauto with lia.
iApply (awp_wand _ (λ _, c C #n r C #(fact n))%I with "[Hr Hc]").
- iApply ((factorial_body_spec n 0 c r) with "[$Hr $Hc]"); eauto with lia.
- iIntros (?) "[Hc Hr]". iModIntro.
awp_load_ret (r,O).
awp_load_ret r.
Qed.
Lemma factorial_spec_with_inv (n: nat) R :
awp (factorial #n) R (λ v, v = #(fact n))%I.
Proof.
awp_lam.
iApply awp_bind. awp_alloc_ret r "[Hr _]".
iApply awp_bind. awp_alloc_ret c "[Hc _]".
iApply awp_bind. awp_alloc_ret r "[Hr _]". etaprod r.
iApply awp_bind. awp_alloc_ret c "[Hc _]". etaprod c.
iApply a_sequence_spec'. iNext. do 3 awp_lam.
iApply (a_while_inv_spec
(k:nat, k n (c,O) C #k (r,O) C #(fact k))%I with "[Hr Hc]").
(k:nat, k n c C #k r C #(fact k))%I with "[Hr Hc]").
- iExists O. eauto with iFrame lia.
- iModIntro. iIntros "H". iDestruct "H" as (k) "(H & Hc & Hr)".
vcg_solver. iIntros "Hr Hc".
......@@ -89,6 +94,6 @@ Section factorial_spec.
iExists (k+1)%nat. eauto with iFrame lia.
+ iLeft. iSplit; eauto. do 2 iModIntro.
iRevert "H". iIntros "%". assert (k = n) as -> by lia.
awp_load_ret (r,O).
awp_load_ret r.
Qed.
End factorial_spec.
......@@ -38,13 +38,17 @@ Section tests_vcg.
vcg_solver. eauto.
Qed.
Ltac etaprod l :=
compute[cloc_add];
rewrite ?Nat.add_0_r;
assert ((l.1, l.2) = l) as -> by (destruct l; auto).
Lemma swap_spec (l1 l2 : cloc) (v1 v2: val) R :
l1 C v1 - l2 C v2 -
awp (swap_with_alloc (cloc_to_val l1) (cloc_to_val l2)) R (λ _, l1 C v2 l2 C v1).
Proof.
iIntros "Hl1 Hl2".
do 2 awp_lam. iApply awp_bind. awp_alloc_ret r "[Hr _]".
progress compute[cloc_add]. simpl.
do 2 awp_lam. iApply awp_bind. awp_alloc_ret r "[Hr _]". etaprod r.
vcg_solver. iIntros "!> !> !>". eauto with iFrame.
Qed.
......
......@@ -24,12 +24,17 @@ Section tests_vcg.
vcg_continue. eauto.
Qed.
Ltac etaprod l :=
compute[cloc_add];
rewrite ?Nat.add_0_r;
assert ((l.1, l.2) = l) as -> by (destruct l; auto).
Lemma test2 (k : cloc) :
k C #10 - awp (alloc (2,11) = ∗ᶜ♯ₗk + 2) True (λ v, v = #12).
Proof.
iIntros "Hk". vcg_solver.
iIntros "Hk". iApply (a_alloc_ret 2).
iIntros (l) "[Hl1 [Hl2 _]]". compute[cloc_add]. simpl.
iIntros (l) "[Hl1 [Hl2 _]]". etaprod l.
vcg_continue. eauto 42 with iFrame.
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