Commit f0967467 authored by Dan Frumin's avatar Dan Frumin

Uncurry the swap function

parent 4832c173
......@@ -3,7 +3,10 @@ From iris_c.vcgen Require Import proofmode.
Section tests_vcg.
Context `{amonadG Σ}.
Definition swap : val := λ: "l1" "l2" "r",
Definition swap : val := λ: "a",
let: "l1" := Fst "a" in
let: "l2" := Fst (Snd "a") in
let: "r" := Snd (Snd "a") in
(a_ret "r") = ∗ᶜ (a_ret "l1") ;
(a_ret "l1") = ∗ᶜ (a_ret "l2") ;
(a_ret "l2") = ∗ᶜ (a_ret "r") ;
......@@ -11,16 +14,17 @@ Section tests_vcg.
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).
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_pure _. awp_pure _. awp_pure _. awp_lam.
(* TODO: ^ if we do awp_pures here it unfolds too much!
Perhaps it unlocks something it shouldnt? *)
awp_pures. awp_lam. do 11 (awp_pure _).
vcg. eauto with iFrame.
Qed.
Definition swap_with_alloc : val := λ: "l1" "l2",
Definition swap_with_alloc : val := λ: "a",
let: "l1" := Fst "a" in
let: "l2" := Snd "a" in
"r" ←ᶜ alloc (1, 0);
(a_ret "r") = ∗ᶜ (a_ret "l1") ;
(a_ret "l1") = ∗ᶜ (a_ret "l2") ;
......@@ -29,11 +33,11 @@ Section tests_vcg.
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 }}.
AWP swap_with_alloc (cloc_to_val l1, cloc_to_val l2) @ R {{ _, l1 C v2 l2 C v1 }}.
Proof.
iIntros "Hl1 Hl2". awp_lam.
awp_pure _. awp_pure _. vcg.
iIntros (l3) "? l1 l2 l3". eauto with iFrame.
iIntros "Hl1 Hl2".
awp_pures. awp_lam. do 6 (awp_pure _).
vcg. iIntros (l3) "? l1 l2 l3". 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