docs: DESIGN.md §Embedding ABI — current-state honesty (no general-ABI claim)

The §"Embedding ABI" prose presented the M3 contract as "the
embedding ABI" — a general boundary — and justified the layout
freeze with "this is what codegen emits today". Both overclaim:

- The accepted set (bare scalar | single-ctor all-scalar record)
  is the *whole* contract, narrow by construction. The host
  hand-constructs and hand-reads the box layout directly; there
  is no general value-marshalling layer. The text now says this
  plainly instead of framing the set as a subset of a wider ABI.
- The freeze is reframed as the consequence of that direct
  layout exposure (the host is the contract surface), not as
  "frozen because that is what lower_ctor emits".
- "MUST NOT move these offsets" is corrected to "for an exported
  type" — the prior wording overclaimed the freeze as binding
  every record layout; the commitment binds exported types and
  thereby constrains codegen repacking of exported records.

Present-tense Ist-state mirror only: no lockstep/wire-contract
design, no post-mortem, no aspirational "should become". Schema
section untouched. Verified green: design_schema_drift (8),
docs_honesty_pin (5), effect_doc_honesty_pin (4),
embed_record_layout_pin (1), embed_staticlib_lowering (3).

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
+The set that can cross the boundary is exactly: `Int` (lowered
-`double`), or a single-constructor record of those (crossing as a
+`i64`), `Float` (lowered `double`), or a single-constructor record
-bare `ptr` to the frozen box layout below); the fn's effect set must
+whose every field is one of those (crossing as a bare `ptr` to the
-be empty. **Frozen as of M3**: a future compiler change MUST NOT
+box layout below); the fn's effect set must be empty. There is no
-move the box offsets below or invert the host-free rule.
+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
+Total box payload size = `8 + n*8`. This is the same layout
-emits today (`match_lower.rs` `lower_ctor`); it is **frozen** — a
+`lower_ctor` (`match_lower.rs`) emits internally; for an exported
-future compiler change MUST NOT move these offsets.
+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