add English explanation of mbox_spec

GaloisInc · Oct 19, 2021 · 6a3e269 · 6a3e269
1 parent 09294b3
commit 6a3e269
Showing 1 changed file with 8 additions and 0 deletions.
diff --git a/heapster-saw/examples/mbox_proofs.v b/heapster-saw/examples/mbox_proofs.v
@@ -135,6 +135,14 @@ Proof.
     vm_compute in e_if0; discriminate e_if0.
 Qed.
 
+(*
+  In English, the spec for `mbox_randomize m` is:
+  - If `m` is non-null, the function returns `SUCCESS` and `m->data` is set to
+    some `data'` such that `m->data[i] = data'[i]` for all `i` such that
+    `i < m->strt` or `i >= m->len`.
+  - Otherwise, the function returns MBOX_NULL_ERROR.
+*)
+
 Definition SUCCESS         := intToBv 32 0.
 Definition MBOX_NULL_ERROR := intToBv 32 23.