diff --git a/docs/DESIGN.md b/docs/DESIGN.md
index 8ebc7d9..a6ae73b 100644
--- a/docs/DESIGN.md
+++ b/docs/DESIGN.md
@@ -2277,11 +2277,17 @@ the internal `@ail_<module>_<fn>`. The symbol is author-chosen and
 decoupled from the `ail_<module>_<def>` mangling so a module/fn
 rename does not move the C symbol.
 
-The embedding ABI accepts `Int` (lowered `i64`), `Float` (lowered
-`double`), or a single-constructor record of those (crossing as a
-bare `ptr` to the frozen box layout below); the fn's effect set must
-be empty. **Frozen as of M3**: a future compiler change MUST NOT
-move the box offsets below or invert the host-free rule.
+The set that can cross the boundary is exactly: `Int` (lowered
+`i64`), `Float` (lowered `double`), or a single-constructor record
+whose every field is one of those (crossing as a bare `ptr` to the
+box layout below); the fn's effect set must be empty. There is no
+general value-marshalling layer — the host hand-constructs and
+hand-reads that box layout directly, so the enumerated set *is* the
+whole contract, narrow by construction, not a subset of a wider
+embedding ABI. Because the box layout is the host's contract
+surface with no accessor indirection, it is a **one-way commitment
+frozen as of M3**: a compiler change MUST NOT move the box offsets
+below for an exported type, nor invert the host-free rule.
 These are enforced at `ail check` (`export-non-scalar-signature`,
 `export-has-effects`) — an effectful or non-scalar export *fails to
 typecheck*. Every exported entrypoint takes a mandatory leading `ailang_ctx_t*`
@@ -2337,9 +2343,12 @@ bare payload pointer `p`:
 | `p + 0 .. p + 8` | `int64_t` constructor tag (written; `0` for the single ctor — no elision) |
 | `p + 8 + i*8` | field `i`, declaration order: `int64_t` for `Int`, IEEE-754 `double` bit-pattern for `Float` |
 
-Total box payload size = `8 + n*8`. This is the layout codegen
-emits today (`match_lower.rs` `lower_ctor`); it is **frozen** — a
-future compiler change MUST NOT move these offsets.
+Total box payload size = `8 + n*8`. This is the same layout
+`lower_ctor` (`match_lower.rs`) emits internally; for an exported
+type the host encodes and decodes these exact offsets itself, so
+they are **frozen** — a compiler change MUST NOT move them for an
+exported type, which permanently constrains codegen's freedom to
+repack exported records.
 
 **Construction (host → kernel input).** The host MUST obtain an
 input record's storage from `ailang_rc_alloc(8 + n*8)` (returns the