Commit 544400fd authored by Marianna Rapoport's avatar Marianna Rapoport Committed by Ralf Jung

Simpler proof

parent 5c51c26c
...@@ -93,26 +93,27 @@ Section prophecy. ...@@ -93,26 +93,27 @@ Section prophecy.
(* -- predicates -- *) (* -- predicates -- *)
is_prophecy : proph -> val -> iProp Σ; is_prophecy : proph -> val -> iProp Σ;
(* -- general properties -- *) (* -- general properties -- *)
new_prophecy_spec : new_prophecy_spec:
{{{ True }}} new_prophecy #() {{{ p, RET #p; v, is_prophecy p #v }}}; {{{ True }}} new_prophecy #() {{{ p, RET #p; v, is_prophecy p v }}};
resolve_prophecy_spec p v w : resolve_prophecy_spec p v e w:
{{{ is_prophecy p v }}} resolve_prophecy #p w {{{ RET w; v = w }}} IntoVal e w ->
{{{ is_prophecy p v }}} resolve_prophecy #p e {{{ RET w; v = w }}}
}. }.
Context `{pr: prophecy}. Context `{pr: prophecy}.
Definition val_to_bool v : bool :=
match v with
| LitV (LitBool b) => b
| _ => true
end.
Definition lateChoice_proph: val := Definition lateChoice_proph: val :=
λ: "x", λ: "x",
let: "p" := new_prophecy pr #() in let: "p" := new_prophecy pr #() in
"x" <- #0 ;; "x" <- #0 ;;
let: "r" := rand #() in let: "r" := rand #() in
resolve_prophecy pr "p" "r". resolve_prophecy pr "p" "r".
Definition val_to_bool v :=
match v with
| LitBool b => Some b
| _ => None
end.
Lemma lateChoice_proph_spec (x: loc) : Lemma lateChoice_proph_spec (x: loc) :
<<< x - >>> <<< x - >>>
...@@ -128,24 +129,11 @@ Section prophecy. ...@@ -128,24 +129,11 @@ Section prophecy.
iMod "AU" as "[Hl [_ Hclose]]". iMod "AU" as "[Hl [_ Hclose]]".
iDestruct "Hl" as (v') "Hl". iDestruct "Hl" as (v') "Hl".
wp_store. wp_store.
destruct (val_to_bool v) eqn:Heq. iMod ("Hclose" $! (val_to_bool v) with "[Hl]") as "HΦ"; first by eauto.
- iMod ("Hclose" $! b with "[Hl]") as "HΦ"; first by eauto. iModIntro. wp_seq. wp_apply rand_spec; try done.
iModIntro. wp_seq. wp_apply rand_spec; try done. iIntros (b') "_". wp_let.
iIntros (b') "_". wp_let. iApply (resolve_prophecy_spec with "Hp").
iDestruct (resolve_prophecy_spec with "Hp") as "Hs". iNext. iIntros (->). done.
iAssert ((#v = #b' - Φ #b'))%I with "[HΦ]" as "Hb". {
iNext. iIntros "Heq". destruct v; inversion Heq; subst. iDestruct "Heq" as %->. done.
}
iSpecialize ("Hs" with "Hb"). done.
- iMod ("Hclose" $! true with "[Hl]") as "HΦ"; first by eauto.
iModIntro. wp_seq. wp_apply rand_spec; try done.
iIntros (b') "_". wp_let.
iDestruct (resolve_prophecy_spec with "Hp") as "Hs".
iAssert ((#v = #b' - Φ #b'))%I with "[HΦ]" as "Hb". {
iNext. iIntros "Heq". iDestruct "Heq" as %[=Heq'].
destruct v; inversion Heq; inversion Heq'.
}
iSpecialize ("Hs" with "Hb"). done.
Qed. Qed.
End prophecy. End prophecy.
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