Commit add06828 authored by Léon Gondelman's avatar Léon Gondelman

using mutable sets operations (create, add, membership, clear) in the monad

parent ee50bc2e
-Q theories iris_c
-arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
theories/lib/env.v
theories/lib/mset.v
theories/lib/flock.v
theories/c_translation/monad.v
theories/c_translation/translation.v
\ No newline at end of file
......@@ -2,7 +2,7 @@ From iris.heap_lang Require Export proofmode notation.
From iris.heap_lang Require Import spin_lock assert par.
From iris.algebra Require Import frac.
From iris.base_logic.lib Require Import fractional.
From iris_c.lib Require Import env flock.
From iris_c.lib Require Import mset flock.
(* M A := ref (list loc) → Mutex → A *)
......@@ -16,7 +16,7 @@ Definition a_bind : val := λ: "f" "x" "env" "l",
(* M A → A *)
Definition a_run : val := λ: "x",
let: "env" := ref (newset #()) in
let: "env" := mset_create #() in
let: "l" := newlock #() in
"x" "env" "l".
......@@ -44,6 +44,9 @@ Definition amonadN := nroot .@ "amonad".
Section a_wp.
Context `{heapG Σ, flockG Σ, spawnG Σ}.
Definition env_inv `{heapG Σ} (env : val) : iProp Σ :=
( X, is_set_mut env X)%I.
Definition awp (e : expr)
(R : iProp Σ) (Φ : val iProp Σ) : iProp Σ :=
( (γ : flock_name) (π : frac) (env : val) (l : val),
......@@ -78,12 +81,10 @@ Section a_wp.
WP a_run v {{ Φ }}.
Proof.
iIntros "HR Hwp". rewrite /a_run /=. wp_let.
wp_bind (newset #()).
iApply set_newset_spec. done.
iNext. iIntros (v0) "%".
wp_alloc env as "H". wp_let.
wp_apply (newlock_cancel_spec amonadN (env_inv #env R)%I with "[H HR]").
iFrame. iExists . iExists env, v0. iFrame. done.
wp_bind (mset_create #()). iApply mset_create_spec; first done.
iNext. iIntros (env) "H". wp_let.
wp_apply (newlock_cancel_spec amonadN (env_inv env R)%I with "[H HR]");
first by iFrame; iExists .
iIntros (k γ') "[#Hlock Hunfl]". wp_let. rewrite- wp_fupd.
iApply (wp_wand with "[Hwp Hunfl]").
unfold awp. by iApply ("Hwp" with "Hlock").
......@@ -92,7 +93,6 @@ Section a_wp.
iMod (cancel_lock with "Hlock Hunfl") as "[HEnv HR]". done.
Qed.
Lemma awp_atomic (v : val) R Φ `{Timeless _ R} :
(R - R', Timeless R' R' awp v R' (λ w, R' - R Φ w)) -
awp (a_atomic v) R Φ.
......
......@@ -2,14 +2,14 @@ From iris.heap_lang Require Export proofmode notation.
From iris.heap_lang Require Import spin_lock assert par.
From iris.algebra Require Import frac.
From iris.base_logic.lib Require Import fractional.
From iris_c.lib Require Import env flock.
From iris_c.lib Require Import mset flock.
From iris_c.c_translation Require Import monad.
Definition a_store : val := λ: "x1" "x2",
a_bind (λ: "vv",
a_atomic_env (λ: "env",
"env" <- set_add (!"env") (!(Fst "vv")) ;;
mset_add (!(Fst "vv")) "env" ;;
Fst "vv" <- Snd "vv" ;;
Snd "vv"
)
......@@ -18,7 +18,7 @@ Definition a_store : val := λ: "x1" "x2",
Definition a_load : val := λ: "x",
a_bind (λ: "v",
a_atomic_env (λ: "env",
assert (set_member (!"env") "v" = #false);;
assert (mset_member "v" "env" = #false);;
!"v"
)
) "x".
......@@ -34,6 +34,4 @@ Definition a_bin_op (op : bin_op) : val := λ: "x1" "x2",
(* M () *)
(* The eta expansion is used to turn it into a value *)
Definition a_seq : val := λ: "env",
a_atomic_env (λ: "env",
"env" <- newset #()
) "env".
a_atomic_env (λ: "env", mset_clear "env") "env".
......@@ -4,7 +4,7 @@ From iris.algebra Require Import frac.
From iris.base_logic.lib Require Import fractional.
Section Env.
Section Sets.
Fixpoint is_list (hd : val) (xs : list val) : Prop :=
match xs with
......@@ -33,17 +33,33 @@ Section Env.
then assert #false
else SOME ("x", "xs").
End Sets.
Section MutableSet.
Definition is_set_mut `{heapG Σ} (v : val) (X : gset val) : iProp Σ
:= ( (l : loc) hd, v = #l l hd is_set hd X )%I.
Definition env_inv `{heapG Σ} (env : val) : iProp Σ :=
( X, is_set_mut env X)%I.
Definition mset_create : val := λ: <>, ref (newset #()).
Definition mset_member : val :=
λ: "x" "xs",
let: "v" := ! "xs" in
set_member "x" "v".
Definition mset_add : val :=
λ: "x" "xs",
let: "v" := ! "xs" in
"xs" <- set_add "x" "v".
Definition mset_clear : val :=
λ: "xs",
"xs" <- newset #().
End Env.
End MutableSet.
Section Env_wp.
Section Sets_wp.
Context `{heapG Σ}.
......@@ -55,7 +71,6 @@ Section Env_wp.
iSplit. iPureIntro. apply NoDup_nil_2. done.
Qed.
Lemma set_member_spec (x: val) (xs: val) (X: gset val):
{{{ is_set xs X }}}
set_member x xs
......@@ -84,28 +99,83 @@ Section Env_wp.
destruct a; iPureIntro; destruct H0; set_solver.
Admitted.
Lemma set_add_spec (x: val) (xs: val) (X: gset val):
Lemma set_add_spec (x: val) (xs: val) (X: gset val):
{{{ is_set xs X x X }}}
set_add x xs
{{{ v, RET v;
(is_set v ({[x]} X) )}}}.
Proof.
iIntros (Φ) "[% %] HPost".
do 2 wp_lam.
wp_bind ((set_member x) xs).
iApply (set_member_spec _ _ X); first done.
iNext. iIntros (v) "[[% %]|[% %]]".
simplify_eq /=.
- by destruct H1.
- simplify_eq. wp_if. iApply "HPost".
destruct H0 as [l [HL [HD HX]]].
unfold is_set; simplify_eq.
iPureIntro. exists (x :: l).
split. simpl. exists xs. done.
split. apply NoDup_cons_2.
by apply not_elem_of_of_list in H1.
done. done.
Qed.
End Env_wp.
\ No newline at end of file
{{{ v, RET v;
(is_set v ({[x]} X) )}}}.
Proof.
iIntros (Φ) "[% %] HPost".
do 2 wp_lam.
wp_bind ((set_member x) xs).
iApply (set_member_spec _ _ X); first done.
iNext. iIntros (v) "[[% %]|[% %]]".
simplify_eq /=.
- by destruct H1.
- simplify_eq. wp_if. iApply "HPost".
destruct H0 as [l [HL [HD HX]]].
unfold is_set; simplify_eq.
iPureIntro. exists (x :: l).
split. simpl. exists xs. done.
split. apply NoDup_cons_2.
by apply not_elem_of_of_list in H1.
done. done.
Qed.
End Sets_wp.
Section MutableSet_wp.
Context `{heapG Σ}.
Lemma mset_create_spec:
{{{ True }}} mset_create #() {{{ v, RET v; is_set_mut v }}}.
Proof.
iIntros (Φ) "_ H".
wp_lam. wp_bind (newset #()).
iApply set_newset_spec; first done.
iNext. iIntros (v) "%".
wp_alloc l as "Hl". iApply "H".
iExists l, v. by iFrame.
Qed.
Lemma mset_member_spec (x: val) (xs: val) (X: gset val):
{{{ is_set_mut xs X }}}
mset_member x xs
{{{ v, RET v; (v = #true x X) (v = #false x X) }}}.
Proof.
iIntros (Φ) "Hmut H".
iDestruct "Hmut" as (s hd) "[% [Hs Hset]]"; subst .
wp_lam. wp_let. wp_load. wp_let.
by iApply (set_member_spec with "[$Hset//]").
Qed.
Lemma mset_add_spec (x: val) (xs: val) (X: gset val):
{{{ is_set_mut xs X x X }}}
mset_add x xs
{{{ RET #() ; (is_set_mut xs ({[x]} X))}}}.
Proof.
iIntros (Φ) "[Hmut %] HPost".
iDestruct "Hmut" as (s hd) "[% [Hs Hset]]"; subst.
do 2 wp_lam; wp_load; wp_let.
wp_bind (set_add x hd).
iApply (set_add_spec with "[$Hset//]").
iNext. iIntros (v) "%". wp_store. iApply "HPost".
iExists s, v. by iFrame.
Qed.
Lemma mset_clear_spec (xs: val) (X: gset val):
{{{ is_set_mut xs X }}}
mset_clear xs
{{{ RET #() ; is_set_mut xs }}}.
Proof.
iIntros (Φ) "Hmut HPost".
iDestruct "Hmut" as (s hd) "[% [Hs Hset]]"; subst.
wp_lam. wp_bind (newset #()).
iApply set_newset_spec; first done.
iNext. iIntros (v) "%". wp_store.
iApply "HPost". iExists s, v. by iFrame.
Qed.
End MutableSet_wp.
\ 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