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.
49 lines
2.3 KiB
Markdown
49 lines
2.3 KiB
Markdown
# 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](embedding-abi.md) 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](memory-model.md)
|
|
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`.
|