From 1e50fc8746b74d27a6fbe7aee62f765ce4ed809e Mon Sep 17 00:00:00 2001
From: Dan Frumin
Date: Thu, 11 Oct 2018 19:12:53 +0200
Subject: [PATCH] Some comments
---
theories/c_translation/monad.v | 7 +++++++
theories/c_translation/translation.v | 6 ++++++
2 files changed, 13 insertions(+)
diff --git a/theories/c_translation/monad.v b/theories/c_translation/monad.v
index db63921..3f1c77c 100644
--- a/theories/c_translation/monad.v
+++ b/theories/c_translation/monad.v
@@ -70,6 +70,13 @@ Section a_wp.
Definition flock_resources (γ : flock_name) (I : gmap prop_id (iProp Σ * frac)) :=
([∗ map] i ↦ p ∈ I, flock_res γ i p.1 p.2)%I.
+ (** DF: The outer `WP` here is needed to be able to preform some reductions inside a heap_lang context.
+ Without this, the `a_wp_awp` rule is not provable.
+
+ My intuitive explanation: we want to preform some reductions to `e` until it is actually a value that is a monadic computation.
+ In some sense it is a form of CPSing on a logical level.
+ But I still cannot precisely state why is it needed.
+ *)
Definition awp (e : expr)
(R : iProp Σ) (Φ : val → iProp Σ) : iProp Σ :=
tc_opaque (WP e {{ ev,
diff --git a/theories/c_translation/translation.v b/theories/c_translation/translation.v
index ab6b775..5077fb6 100644
--- a/theories/c_translation/translation.v
+++ b/theories/c_translation/translation.v
@@ -24,6 +24,12 @@ Definition a_free_check : val :=
"go" "env" "l" (#1 + "i") "n"
else #().
+
+(* DF: following the discussion with Robbert, it seems that we cannot
+ prove this function right now, because our ghost state cannot
+ account that we hold permission for the *whole* array.
+
+ See the RustBelt paper for the trick to make it work. *)
Definition a_free : val := λ: "x",
"v" ←ᶜ "x";;ᶜ
a_atomic_env (λ: "env",
--
GitLab