iter embedding-abi-m5.tidy (DONE 3/3): milestone-close doc-honesty drift — pin-safe, doc/comment-only

Resolves the M5 milestone-close audit DRIFT (audit journal
28ab56a). Single cohesive commit, M2.tidy a80d495 / M3.tidy
63d7d60 precedent (pins are the coverage, no RED, no
audit/fieldtest gate).

- docs/DESIGN.md edit-1 §"Free (host side)": dropped the retired-M4
  forward-reference ("an additive M4 concern, not a contradiction
  of this freeze"; M4 retired 2026-05-18) -> present-tense current
  fact (a boxed-field record is not an M3 embedding type,
  export-gate-rejected; the freeze covers exactly the all-scalar
  single-ctor record).
- docs/DESIGN.md edit-2 §"Embedding ABI": reconciled the now-
  inaccurate "(no shared mutable runtime state - ... data-race-free,
  sanitiser-verified)" blanket with the real post-7bfa11e state:
  the per-allocation hot path (per-ctx counters + per-object
  refcount header) is non-atomic by design and never shared
  (Ctx:!Send, single-thread-per-ctx); the one shared datum is the
  atomic-relaxed global RC-stats fallback counter; "data-race-free,
  sanitiser-verified" retained (still true).
- runtime/rc.c:88 comment-only: stale "two unconditional ++
  operations" -> accurate "one counter bump per alloc/free ...
  relaxed atomic add on the global null-ctx fallback, a plain ++
  on the per-ctx path" (consistent with the adjacent already-
  correct :93-106 atomic block + :45-55 Threading header).

Boss-verified independently: all pins green (design_schema_drift
8/0, docs_honesty_pin 5/0, effect_doc_honesty_pin 4/0,
embed_record_layout_pin 1/0) = mechanical proof no pinned/hashed
byte moved; the adjacent separately-pinned bare-scalar sentence is
byte-identical (shifted 2299->2305 by net-added lines; substring
pin, passes); rc.c strictly comment-only (filter empty);
cargo build --workspace Finished; git scope = only docs/DESIGN.md
+ runtime/rc.c + journal/stats. Clears the M5-audit doc-honesty
debt; no new debt.

FINAL M5 iteration. The M1-M5 Embedding ABI arc is functionally
complete, audited, ratified, and doc-honest. Includes the per-iter
journal, stats, and INDEX line.
This commit is contained in:
2026-05-19 03:07:40 +02:00
parent e81fb90d88
commit 70f2a318e0
5 changed files with 111 additions and 9 deletions
+13 -7
View File
@@ -2288,9 +2288,15 @@ typecheck*. Every exported entrypoint takes a mandatory leading `ailang_ctx_t*`
(M2): a per-thread embedding context created by `ailang_ctx_new()`
and released by `ailang_ctx_free()`, owned by the calling thread for
its lifetime. The host links one `ailang_ctx_t` per OS worker thread
and the runtime accounts RC alloc/free into it (no shared mutable
runtime state — the swarm artefact is data-race-free, sanitiser-
verified). The staticlib swarm artefact is **RC-only**:
and the runtime accounts RC alloc/free into it: the per-allocation
hot path (the per-ctx counters and the per-object refcount header)
is non-atomic by design and never shared — a box never crosses a
thread (`Ctx: !Send`) and each `ailang_ctx_t` is
single-thread-per-ctx. The one datum a multi-threaded host shares
is the global RC-stats fallback counter (used when no ctx is
bound); it is atomic-relaxed so the swarm's leak accounting is
exact. The swarm artefact is data-race-free, sanitiser-verified.
The staticlib swarm artefact is **RC-only**:
`ail build --emit=staticlib` rejects `--alloc=gc`/`--alloc=bump`
(the shared Boehm collector is not swarm-safe). The value/record
layout is **frozen as of M3** (see "Frozen value layout" below); the
@@ -2354,10 +2360,10 @@ is always owned by the host.
**Free (host side).** `ailang_rc_dec(payload)`. Leak-free for an M3
record because every field is a scalar — `ailang_rc_dec` is
header-only and an M3 record has no boxed children. A record with
boxed fields (`Str`/`List`/nested record) is **not** an M3 type
(rejected by the export gate); a recursive typed-free for that
shape is an additive M4 concern, not a contradiction of this
freeze.
boxed fields (`Str`/`List`/nested record) is **not** an M3
embedding type — the export gate rejects it, so the boundary
never crosses a value that would need a recursive typed-free. The
freeze covers exactly the all-scalar single-constructor record.
## Data model