note some design choices

theories/heap_lang/lang.v

@@ -15,6 +15,13 @@ Noteworthy design choices:
   [b] are evaluated.  With left-to-right evaluation, that triple is basically
   useless unless the user let-expands [b].
 
+- Even after deallocating a location, the heap remembers that these locations
+  were previously allocated and makes sure they do not get reused. This is
+  necessary to ensure soundness of the [meta] feature provided by [gen_heap].
+  Also, unlike in langauges like C, allocated and deallocated "blocks" do not
+  have to match up: you can allocate a large array of locations and then
+  deallocate a hole out of it in the middle.
+
 - 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