Commit 70242f9c authored by Léon Gondelman's avatar Léon Gondelman

attempt to prove swap

parent 0a87ae99
......@@ -5,6 +5,7 @@ From iris.base_logic.lib Require Import fractional.
From iris_c.lib Require Import locking_heap mset flock U.
From iris_c.c_translation Require Import monad lifting proofmode translation.
Section test.
Context `{locking_heapG Σ, heapG Σ, flockG Σ, spawnG Σ}.
......@@ -34,4 +35,27 @@ Section test.
awp_lam.
iApply (a_load_spec with "Hl"). iIntros "Hl". eauto.
Qed.
Definition swap (l1 l2 : loc) : val := λ: <>,
a_bind (λ: "r",
a_sequence
(a_store (a_ret "r") (a_load (a_ret #l1)))
(a_sequence
(a_store (a_ret #l1) (a_load (a_ret #l2)))
(a_store (a_ret #l2) (a_load (a_ret "r")))))
(a_alloc (a_ret #0%V)).
Lemma swap_spec (l1 l2 : loc) (v1 v2: val) R :
l1 U v1 - l2 U v2 -
awp (swap l1 l2 #()) R (λ _, l1 U v2 l2 U v1).
Proof.
iIntros "Hl1 Hl2".
awp_lam.
iApply awp_bind.
iApply (a_alloc_spec R #0 ).
iIntros (r) "Hr".
awp_lam.
Admitted.
End test.
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