diff --git a/theories/c_translation/monad.v b/theories/c_translation/monad.v
index db6392186d188b1df6be529f6245c0080e2f3d18..3f1c77c50b808f8e5fa8d6e2c60c8cdd93e72577 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 ab6b775e0f866a9196928c493313b05ec6363b82..5077fb6cc9df4a1920abeb1c23aab0f92f3bd41c 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",