From dd5b18378f58ef273de9d771a6b0d948a6589094 Mon Sep 17 00:00:00 2001 From: Brummel Date: Tue, 19 May 2026 11:22:25 +0200 Subject: [PATCH] =?UTF-8?q?docs:=20DESIGN.md=20=C2=A7Embedding=20ABI=20?= =?UTF-8?q?=E2=80=94=20current-state=20honesty=20(no=20general-ABI=20claim?= =?UTF-8?q?)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 | 25 +++++++++++++++++-------- 1 file changed, 17 insertions(+), 8 deletions(-) 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__`. The symbol is author-chosen and decoupled from the `ail__` 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