Commit 36e4c4a1 authored by Marianna Rapoport's avatar Marianna Rapoport Committed by Ralf Jung

splitting up prophecy into separate file

parent 544400fd
...@@ -4,6 +4,7 @@ From iris.program_logic Require Export atomic. ...@@ -4,6 +4,7 @@ From iris.program_logic Require Export atomic.
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation par. From iris.heap_lang Require Import proofmode notation par.
From iris.bi.lib Require Import fractional. From iris.bi.lib Require Import fractional.
From iris.heap_lang Require Import prophecy.
Set Default Proof Using "Type". Set Default Proof Using "Type".
(** Nondeterminism and Speculation: (** Nondeterminism and Speculation:
...@@ -82,25 +83,9 @@ Section coinflip. ...@@ -82,25 +83,9 @@ Section coinflip.
End coinflip. End coinflip.
Section prophecy. Section coinflip_with_prophecy.
Context `{!heapG Σ} (N: namespace). Context `{!heapG Σ} `{pr: prophecy} (N: namespace).
Record prophecy {Σ} `{!heapG Σ} := Prophecy {
(* -- operations -- *)
new_prophecy : val;
resolve_prophecy : val;
(* -- predicates -- *)
is_prophecy : proph -> val -> iProp Σ;
(* -- general properties -- *)
new_prophecy_spec:
{{{ True }}} new_prophecy #() {{{ p, RET #p; v, is_prophecy p v }}};
resolve_prophecy_spec p v e w:
IntoVal e w ->
{{{ is_prophecy p v }}} resolve_prophecy #p e {{{ RET w; v = w }}}
}.
Context `{pr: prophecy}.
Definition val_to_bool v : bool := Definition val_to_bool v : bool :=
match v with match v with
...@@ -136,4 +121,4 @@ Section prophecy. ...@@ -136,4 +121,4 @@ Section prophecy.
iNext. iIntros (->). done. iNext. iIntros (->). done.
Qed. Qed.
End prophecy. End coinflip_with_prophecy.
From iris.heap_lang Require Export lifting notation.
From iris.base_logic.lib Require Export invariants.
From iris.program_logic Require Export atomic.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation par.
From iris.bi.lib Require Import fractional.
Set Default Proof Using "Type".
Section prophecy.
Context `{!heapG Σ} (N: namespace).
Record prophecy {Σ} `{!heapG Σ} := Prophecy {
(* -- operations -- *)
new_prophecy : val;
resolve_prophecy : val;
(* -- predicates -- *)
is_prophecy : proph -> val -> iProp Σ;
(* -- general properties -- *)
new_prophecy_spec:
{{{ True }}} new_prophecy #() {{{ p, RET #p; v, is_prophecy p v }}};
resolve_prophecy_spec p v e w:
IntoVal e w ->
{{{ is_prophecy p v }}} resolve_prophecy #p e {{{ RET w; v = w }}}
}.
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