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

specification for environment operations done and a_run proof restored

parent bb6daa40
......@@ -77,6 +77,8 @@ Section a_wp.
WP a_run v {{ Φ }}.
Proof.
iIntros "HR Hwp". rewrite /a_run /=. wp_let.
wp_let. wp_alloc env. wp_let.
(*
wp_apply (newlock_cancel_spec R with "[$]").
iIntros (k γ') "Hlock". wp_let. iApply wp_fupd.
......
......@@ -4,30 +4,108 @@ From iris.algebra Require Import frac.
From iris.base_logic.lib Require Import fractional.
(* Make mutable versions *)
Fixpoint is_list (hd : val) (xs : list val) : Prop :=
match xs with
| [] => hd = NONEV
| x :: xs => hd', hd = SOMEV (x,hd') is_list hd' xs
Section Env.
Fixpoint is_list (hd : val) (xs : list val) : Prop :=
match xs with
| [] => hd = NONEV
| x :: xs => hd', hd = SOMEV (x,hd') is_list hd' xs
end.
Definition is_set (hd : val) (X : gset val) : Prop :=
l : list val, is_list hd l NoDup l of_list l X.
Definition is_set_mut `{heapG Σ} (v : val) (X : gset val) : iProp Σ :=
( (l : loc) hd,
v = #l l hd is_set hd X )%I.
Definition newset : val := λ: <>, NONEV.
Definition set_member : val :=
rec: "member" "x" "xs" :=
match: "xs" with
NONE => #false
| SOME "p" => if: Fst "p" = "x" then #true else "member" "x" (Snd "p")
end.
Definition set_add : val := λ: "x" "xs",
if: set_member "x" "xs"
then assert #false
else SOME ("x", "xs").
Definition is_set (hd : val) (X : gset val) : Prop :=
l : list val, is_list hd l NoDup l of_list l X.
Definition newset : val := λ: <>, NONEV.
Definition set_member : val :=
rec: "member" "x" "xs" :=
match: "xs" with
NONE => #false
| SOME "p" =>
if: Fst "p" = "x"
then #true else
let: "y" := (Snd "p") in "member" "x" "y"
end.
Definition set_add : val :=
λ: "x" "xs",
if: set_member "x" "xs"
then assert #false
else SOME ("x", "xs").
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.
\ No newline at end of file
( X, is_set_mut env X)%I.
End Env.
Section Env_wp.
Context `{heapG Σ}.
Lemma set_newset_spec:
{{{ True }}} newset #() {{{ v, RET v; is_set v ∅⌝ }}}.
Proof.
iIntros (Φ) "_ H". wp_lam.
iApply "H". iExists []. iSimpl. iSplit. done.
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
{{{ v, RET v;
(v = #true x X) (v = #false x X) }}}.
Proof.
iIntros (Φ) "% HPost".
unfold is_set in a.
destruct a as [l [HL [HDup HX]]].
iRevert (HL HX). iInduction l as [|hd tl] "IH" forall (xs X);
iIntros "% %"; simpl in a; subst; do 2 wp_lam.
- wp_case. wp_seq. iApply "HPost". iRight.
simplify_eq. done.
- destruct a as [hd' [HXs HL]].
rewrite of_list_cons in a0; simplify_eq /=.
wp_case. wp_let. wp_proj.
destruct (decide (hd = x)); simplify_eq /=.
+ assert (BinOp EqOp x x = #true) as ->. admit.
wp_if. iApply "HPost". iLeft. iSplit; first done.
iPureIntro. set_solver.
+ assert (BinOp EqOp hd x = #false) as ->. admit.
wp_if. wp_proj. wp_let. apply NoDup_cons_12 in HDup.
iApply ("IH" $! _ hd' (of_list tl) with "[HPost]");
[| done| done].
iNext; iIntros; iApply "HPost";
destruct a; iPureIntro; destruct H0; set_solver.
Admitted.
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
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