Commit 4832c173 authored by Dan Frumin's avatar Dan Frumin

Fix some tests

parent e05af4c4
......@@ -10,8 +10,9 @@ Section tests_vcg.
l C #42 -
AWP call (c_id, ∗ᶜ ♯ₗl) @ R {{ v, v = #42 l C #42 }}%I.
Proof.
iIntros "Hl". vcg_solver.
iIntros "Hl". awp_lam. vcg_solver. iIntros "?".
iIntros "Hl". vcg.
iIntros "Hl". iModIntro. iIntros "HR". iExists R. iFrame.
awp_lam. vcg. iIntros "Hl $".
vcg_continue. eauto.
Qed.
......@@ -23,9 +24,9 @@ Section tests_vcg.
Lemma test_invoke_2 R :
AWP call (plus_pair, 21 ||| 21) @ R {{ v, v = #42 }}%I.
Proof.
iIntros. vcg_solver. awp_lam.
do 2 (awp_proj; awp_let).
vcg_solver. by vcg_continue.
iIntros. vcg. iModIntro. iIntros "HR". iExists R. iFrame.
awp_lam. awp_pures. vcg.
iIntros "$". vcg_continue. done.
Qed.
Lemma test_invoke_3 (l : cloc) R :
......@@ -33,10 +34,9 @@ Section tests_vcg.
AWP call (plus_pair, (∗ᶜ ♯ₗl ||| ∗ᶜ ♯ₗl)) @ R
{{ v, v = #42 l C #21 }}%I.
Proof.
iIntros. vcg_solver. iIntros "Hl". awp_lam.
do 2 (awp_proj; awp_let).
vcg_solver. iIntros "Hl". vcg_continue.
rewrite Qp_half_half. eauto 42 with iFrame.
iIntros. vcg. iIntros "Hl".
iModIntro. iIntros "HR". iExists R. iFrame.
awp_lam. awp_pures. vcg.
iIntros "Hl $". vcg_continue. eauto.
Qed.
End tests_vcg.
......@@ -9,37 +9,31 @@ Section tests_vcg.
(a_ret "l2") = ∗ᶜ (a_ret "r") ;
().
Lemma swap_spec_by_vcg_opt (l1 l2 r : cloc) (v1 v2: val) R :
Lemma swap_spec (l1 l2 r : cloc) (v1 v2: val) R :
r C #0 - l1 C v1 l2 C v2 -
awp (swap (cloc_to_val l1) (cloc_to_val l2) (cloc_to_val r)) R (λ _, l2 C v1 l1 C v2).
Proof.
iIntros "Hr [Hl1 Hl2]". awp_lam; awp_pures. vcg.
vcg_solver. iIntros "!> !> !> **". eauto with iFrame.
iIntros "Hr [Hl1 Hl2]".
awp_lam. awp_pure _. awp_pure _. awp_pure _. awp_lam.
(* TODO: ^ if we do awp_pures here it unfolds too much!
Perhaps it unlocks something it shouldnt? *)
vcg. eauto with iFrame.
Qed.
Definition swap_with_alloc : val := λ: "l1" "l2",
"r" ←ᶜ alloc (1, 0);;
"r" ←ᶜ alloc (1, 0);
(a_ret "r") = ∗ᶜ (a_ret "l1") ;
(a_ret "l1") = ∗ᶜ (a_ret "l2") ;
(a_ret "l2") = ∗ᶜ (a_ret "r") ;
().
Lemma load_spec cl (v1 v2: val) R :
cl C v1 -
AWP ∗ᶜ (a_ret (cloc_to_val cl)) @ R {{ _, cl C v1 }}.
Proof.
iIntros "Hl".
vcg_solver. eauto.
Qed.
Lemma swap_spec (l1 l2 : cloc) (v1 v2: val) R :
Lemma swap_with_alloc_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.
vcg_solver.
iIntros "Hl2 Hl1". iIntros (l3) "[Hl3 _]". vcg_continue.
iIntros "!> !> !> **". eauto with iFrame.
iIntros "Hl1 Hl2". awp_lam.
awp_pure _. awp_pure _. vcg.
iIntros (l3) "? l1 l2 l3". eauto with iFrame.
Qed.
End tests_vcg.
......@@ -5,7 +5,7 @@ Local Open Scope Z_scope.
Section tests_vcg.
Context `{amonadG Σ}.
Lemma test1 (l k : cloc) (e: expr) `{Closed [] e}:
Lemma test1 (l k : cloc) (e: expr) :
( Φ v, k C v - (k C #12 - Φ v) - awp e True Φ) -
l C #1 -
k C #10 -
......@@ -14,20 +14,21 @@ Section tests_vcg.
♯ₗl = e
{{ _, True }}.
Proof.
iIntros "#He Hl Hk". vcg_solver.
iIntros "Hk".
iIntros "#He Hl Hk". vcg.
iIntros "Hl Hk".
iApply ("He" with "Hk"); iIntros "Hk".
vcg_continue. iIntros "!> Hk Hl".
vcg_continue.
iIntros "Hl Hk".
iApply ("He" with "Hk"); iIntros "Hk".
vcg_continue. eauto.
Qed.
Lemma test2 (k : cloc) :
k C #10 - AWP alloc (2,11) = ∗ᶜ♯ₗk + 2 {{ v, v = #12 }}.
k C #10 - AWP alloc (2,11) = ∗ᶜ♯ₗk + 2 {{ v, v = #12 k C #10}}.
Proof.
iIntros "Hk". vcg_solver. iIntros "Hk".
iIntros (l) "[Hl1 [Hl2 _]]".
vcg_continue. eauto 42 with iFrame.
iIntros "Hk". vcg.
iIntros (l) "Hl2 Hk Hl1".
eauto 42 with iFrame.
Qed.
(* TODO: should we even allow to alloc arrays of size zero?
......@@ -38,8 +39,9 @@ Section tests_vcg.
(AWP ∗ᶜ(alloc (n,m)) {{ v, v = #m }})%I.
Proof.
intros ?. iStartProof.
vcg_solver.
iIntros (l) "Hl". assert ( m, n = S m) as [k ->]. exists (pred n). omega.
vcg. iExists (n). repeat iSplit; eauto.
{ iPureIntro. lia. }
iIntros (l) "Hl". assert ( m, n = S m) as [k ->]. exists (pred n). lia.
iDestruct "Hl" as "[Hl Hls]". (* TODO: this looks ridiculous *)
vcg_continue. eauto 42 with iFrame.
Qed.
......@@ -49,14 +51,14 @@ Section tests_vcg.
(AWP ∗ᶜ(alloc (n,m)) {{ v, v = #m }})%I.
Proof.
intros ?. iStartProof.
vcg_solver.
vcg.
match goal with
| [ |- environments.envs_entails _
( n0 : nat, _)%I] => idtac
end.
Abort.
Lemma test6 (l k : cloc) (e1 e2 : expr) `{Closed [] e1, Closed [] e2}:
Lemma test6 (l k : cloc) (e1 e2 : expr) :
( Φ, Φ #11 - awp e1 True Φ) -
( Φ, Φ #12 - awp e2 True Φ) -
l C #1 -
......@@ -64,12 +66,12 @@ Section tests_vcg.
AWP (♯ₗl = 2) + (♯ₗk = e1; e2)
{{ v, l C[LLvl] #2 k C #11 v = #14 }}.
Proof.
iIntros "He1 He2 Hl Hk". vcg_solver.
iIntros "He1 He2 Hl Hk". vcg.
iIntros "Hk".
iApply "He1".
vcg_continue. iModIntro. iIntros "Hk".
vcg_continue. iIntros "Hk".
iApply "He2".
vcg_continue. iIntros "Hk Hl".
vcg_continue. iIntros "Hl Hk".
eauto with iFrame.
Qed.
End tests_vcg.
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