Brummel
19dc42f5ca
The first formal-links milestone shipped clause-5 + 8 links across the
existing file layout. Browsing surfaced that file-only granularity is
only as precise as the file boundaries — three files mixed two or
three navigation targets under one address, so the 8 links could not
multiply without ambiguity. This commit fixes the substrate, then
applies the sweep the original milestone deferred.
Splits (each extracts an already-self-contained section into its own
file so links land on the topic, not the parent doc's TOC):
contracts/typeclasses.md
→ +contracts/prelude-classes.md (Eq/Ord/Show ships, polymorphic `print`)
→ +contracts/method-dispatch.md (5-step dispatch rule, candidate index)
contracts/memory-model.md
→ +contracts/language-constraints.md (the 4 binding constraints
making RC sound without a
cycle collector)
models/authoring-surface.md
→ +models/prose-projection.md (Form-B / `ail prose` / merge-prose)
Each new file enters design/INDEX.md as its own row (three contracts
share show_no_instance_e2e.rs / uniqueness.rs as ratifying tests;
prose-projection is a model). Two pre-existing links rebind to the
new topic-files (memory-model.md → method-dispatch.md;
float-semantics.md → prelude-classes.md).
Link sweep: 8 → 88 formal Markdown links over 23 files. Every file
in design/contracts/ + design/models/ now has at least one outgoing
link; the tree is fully connected. Links are file-relative
`[label](path)` per the established convention, fenced code blocks
are skipped (a `](` inside ```jsonc``` is literal text), the durable
tier (design/ + crates/ + runtime/) is enforced by clause-5.
Tests:
- design_index_pin.rs (5/5 clauses): clean-cut, INDEX resolution,
ratifying-test resolution, no decision-record prose in contracts/,
body links durable + resolving.
- docs_honesty_pin.rs (5/5): one assertion rebinds from typeclasses.md
to prelude-classes.md (where the gated sentence now lives);
design_corpus widens to include the 4 new files so the Wunschdenken
/ doc-archaeology sweeps continue to cover everything that used to
live in the parents.
No spec/plan/journal for this batch — interactive collaboration after
the milestone closed; the user gated the splits explicitly before the
sweep.
2.3 KiB
Frozen value layout (M3 — one-way commitment)
Frozen value layout (M3 — one-way commitment)
For a single-constructor data T whose n fields are each Int
or Float, a value of T crossing the
embedding C boundary is a
bare payload pointer p:
| bytes | content |
|---|---|
p - 8 .. p |
uint64_t refcount header (HEADER_SIZE = 8) |
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 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
payload pointer with the refcount header pre-set to 1, payload
zeroed), then write the tag (0) and the scalar fields at the
offsets above. A raw malloc is a contract violation:
own-consume and ailang_rc_dec both require the runtime's 8-byte
header at p - 8 initialised to 1.
Ownership follows the declared mode (the
Mode metadata is load-bearing for codegen
contract, as the C ABI): a (own (con T)) parameter transfers ownership in — the kernel consumes it
(Iter-B drop-at-return); the host MUST NOT touch or dec it after
the call. A (borrow (con T)) parameter is retained by the host —
the kernel does not consume it; the host frees it. The return value
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
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.
Ratified by: crates/ailang-codegen/tests/embed_record_layout_pin.rs.