diff --git a/theories/heap_lang/lib/coin-flip.v b/theories/heap_lang/lib/coin-flip.v index 2cd4780ce2fbc1f1140030fa64e04ca68e0071d6..af0bf13cc1e05409f0a57aec105c6b9b78a9870b 100644 --- a/theories/heap_lang/lib/coin-flip.v +++ b/theories/heap_lang/lib/coin-flip.v @@ -4,6 +4,7 @@ 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. +From iris.heap_lang Require Import prophecy. Set Default Proof Using "Type". (** Nondeterminism and Speculation: @@ -82,25 +83,9 @@ Section coinflip. End coinflip. -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⌝ }}} - }. +Section coinflip_with_prophecy. - Context `{pr: prophecy}. + Context `{!heapG Σ} `{pr: prophecy} (N: namespace). Definition val_to_bool v : bool := match v with @@ -136,4 +121,4 @@ Section prophecy. iNext. iIntros (->). done. Qed. -End prophecy. +End coinflip_with_prophecy. diff --git a/theories/heap_lang/prophecy.v b/theories/heap_lang/prophecy.v new file mode 100644 index 0000000000000000000000000000000000000000..2e7af6544383bbbc21afc555c0a69abc914e9510 --- /dev/null +++ b/theories/heap_lang/prophecy.v @@ -0,0 +1,27 @@ +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.