From 3dc789f297d19d71dedaddb5968a5fe9e919706e Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 4 Oct 2018 19:23:10 +0200
Subject: [PATCH] document some heap_lang design choices

---
 theories/heap_lang/lang.v | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index 7a7f28361..9242baac2 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -12,8 +12,14 @@ Set Default Proof Using "Type".
   [b] are evaluated.  With left-to-right evaluation, that triple is basically
   useless the user let-expands [b].
 
-*)
+- For prophecy variables, we annotate the reduction steps with an "observation"
+  and tweak adequacy such that WP knows all future observations.  There is
+  another possible choice: Use non-deterministic choice when creating a prophecy
+  variable ([NewProph]), and when resolving it ([ResolveProph]) make the
+  program diverge unless the variable matches.  That, however, requires an
+  erasure proof that this endless loop does not make specifications useless.
 
+*)
 
 Delimit Scope expr_scope with E.
 Delimit Scope val_scope with V.
-- 
GitLab