Commit e9f37915 authored by Ralf Jung's avatar Ralf Jung
Browse files

change prophecy notation

parent d2cb8da5
...@@ -24,11 +24,11 @@ Definition earlyChoice: val := ...@@ -24,11 +24,11 @@ Definition earlyChoice: val :=
Definition lateChoice: val := Definition lateChoice: val :=
λ: "x", λ: "x",
let: "p" := new prophecy in let: "p" := NewProph in
"x" <- #0 ;; "x" <- #0 ;;
let: "r" := rand #() in let: "r" := rand #() in
resolve "p" to "r" ;; resolve_proph: "p" to: "r" ;;
"r". "r".
Section coinflip. Section coinflip.
Context `{!heapG Σ} (N: namespace). Context `{!heapG Σ} (N: namespace).
...@@ -84,9 +84,9 @@ Section coinflip. ...@@ -84,9 +84,9 @@ Section coinflip.
wp_store. wp_store.
iMod ("Hclose" $! (val_to_bool v) with "[Hl]") as "HΦ"; first by eauto. iMod ("Hclose" $! (val_to_bool v) 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. wp_bind (resolve _ to _)%E. iIntros (b') "_". wp_let.
iApply (wp_resolve_proph with "Hp"). wp_apply (wp_resolve_proph with "Hp").
iNext. iIntros (->). wp_seq. done. iIntros (->). wp_seq. done.
Qed. Qed.
End coinflip. End coinflip.
...@@ -158,5 +158,4 @@ Notation "'match:' e0 'with' 'SOME' x => e2 | 'NONE' => e1 'end'" := ...@@ -158,5 +158,4 @@ Notation "'match:' e0 'with' 'SOME' x => e2 | 'NONE' => e1 'end'" :=
(Match e0 BAnon e1 x%bind e2) (Match e0 BAnon e1 x%bind e2)
(e0, e1, x, e2 at level 200, only parsing) : expr_scope. (e0, e1, x, e2 at level 200, only parsing) : expr_scope.
Notation "'new' 'prophecy'" := NewProph (at level 100) : expr_scope. Notation "'resolve_proph:' p 'to:' v" := (ResolveProph p v) (at level 100) : expr_scope.
Notation "'resolve' p 'to' v" := (ResolveProph p v) (at level 100) : expr_scope.
...@@ -5,8 +5,9 @@ Section language_mixin. ...@@ -5,8 +5,9 @@ Section language_mixin.
Context {expr val state observation : Type}. Context {expr val state observation : Type}.
Context (of_val : val expr). Context (of_val : val expr).
Context (to_val : expr option val). Context (to_val : expr option val).
(** We annotate the reduction relation with observations [κ], which we will use in the definition (** We annotate the reduction relation with observations [κ], which we will
of weakest preconditions to keep track of creating and resolving prophecy variables. *) use in the definition of weakest preconditions to predict future
observations and assert correctness of the predictions. *)
Context (prim_step : expr state option observation expr state list expr Prop). Context (prim_step : expr state option observation expr state list expr Prop).
Record LanguageMixin := { Record LanguageMixin := {
......
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