diff --git a/docs/specs/2026-05-19-design-md-rolesplit.md b/docs/specs/2026-05-19-design-md-rolesplit.md index dd19999..f5a5912 100644 --- a/docs/specs/2026-05-19-design-md-rolesplit.md +++ b/docs/specs/2026-05-19-design-md-rolesplit.md @@ -155,16 +155,19 @@ header when the code is the single source of truth. | feature-acceptance | brainstorm-gate / stable | skills/brainstorm/SKILL.md Step 4 | contracts/feature-acceptance.md | | authoring-surface | LLM author / stable | crates/ailang-surface round_trip.rs | contracts/authoring-surface.md | | roundtrip-invariant | every release / stable | crates/ailang-surface round_trip.rs | contracts/roundtrip-invariant.md | -| memory-model | LLM author / stable | crates/ailang-check uniqueness/mode tests | contracts/memory-model.md | -| data-model | LLM author / stable | crates/ailang-core design_schema_drift.rs | contracts/data-model.md | -| mangling | codegen / stable | crates/ail eq_ord_e2e.rs | crates/ailang-codegen/src/lib.rs //! | -| env-construction | codegen / stable | crates/ailang-codegen duplicate_ctor_pin.rs | crates/ailang-codegen/src/lib.rs //! | -| frozen-value-layout | embedding ABI / one-way-frozen| crates/ailang-codegen embed_record_layout_pin.rs | contracts/frozen-value-layout.md + runtime/rc.c §layout | -| float-semantics | LLM author / stable | crates/ail eq_float_noinstance.rs | contracts/float-semantics.md | -| typeclasses | LLM author / stable | crates/ail show_no_instance_e2e.rs | contracts/typeclasses.md | -| tail-calls | codegen / stable | crates/ailang-check tail-call tests | contracts/tail-calls.md | -| honesty-rule | architect+grounding / stable | crates/ailang-core docs_honesty_pin.rs | contracts/honesty-rule.md | -| embedding-abi | embedding host / stable | crates/ailang-codegen embed_record_layout_pin.rs | contracts/embedding-abi.md | +| memory-model | LLM author / stable | crates/ailang-check/src/uniqueness.rs (in-source mod tests) | contracts/memory-model.md | +| data-model | LLM author / stable | crates/ailang-core/tests/design_schema_drift.rs | contracts/data-model.md | +| mangling | codegen / stable | crates/ail/tests/eq_ord_e2e.rs | crates/ailang-codegen/src/lib.rs //! | +| env-construction | codegen / stable | crates/ailang-check/tests/duplicate_ctor_pin.rs | crates/ailang-codegen/src/lib.rs //! | +| qualified-xref | codegen / stable | crates/ail/tests/codegen_import_map_fallback_pin.rs | crates/ail/src/main.rs //! | +| frozen-value-layout | embedding ABI / one-way-frozen| crates/ailang-codegen/tests/embed_record_layout_pin.rs | contracts/frozen-value-layout.md + runtime/rc.c §layout | +| float-semantics | LLM author / stable | crates/ail/tests/eq_float_noinstance.rs | contracts/float-semantics.md | +| typeclasses | LLM author / stable | crates/ail/tests/show_no_instance_e2e.rs | contracts/typeclasses.md | +| str-abi | runtime ABI / stable | crates/ail/tests/e2e.rs (Str path) | contracts/str-abi.md + runtime/str.c §heap-Str | +| tail-calls | codegen / stable | crates/ailang-check/src/lib.rs (in-source tail_call_in_non_tail_position_is_rejected) | contracts/tail-calls.md | +| honesty-rule | architect+grounding / stable | crates/ailang-core/tests/docs_honesty_pin.rs | contracts/honesty-rule.md | +| embedding-abi | embedding host / stable | crates/ailang-codegen/tests/embed_record_layout_pin.rs | contracts/embedding-abi.md | +| scope-boundaries | architect+author / stable | crates/ailang-core/tests/effect_doc_honesty_pin.rs | contracts/scope-boundaries.md | | verification | architect / stable | bench/architect_sweeps.sh | contracts/verification.md | ## Models @@ -177,11 +180,16 @@ header when the code is the single source of truth. | pipeline | onboarding / evolves | models/pipeline.md | ``` -The `ratifying-test` column above shows illustrative tokens. The -planner resolves each to an exact, recon-verified file path (the -`design_index_pin.rs` clause-2 check requires every token to resolve -to a real file); the spec owns the *shape and the disposition*, the -planner owns the exact bytes per the planner Iron Law. +The `ratifying-test` column above is now **Boss-resolved to exact +recon-verified paths** (plan-recon confirmed each file exists; the +`design_index_pin.rs` clause-2 check, widened to accept +`crates/**/src/*.rs` in-source `#[cfg(test)] mod tests`, requires +every token to resolve to a real file). The full per-`###` +relocation map and the adjudication rationale for the three +ledger additions (`qualified-xref`, `str-abi`, `scope-boundaries`) +are in the **Appendix — Boss-adjudicated relocation map** at the +end of this spec; that appendix is the authoritative, +placeholder-free map the planner consumes. **A sample contract file** — `design/contracts/float-semantics.md` (content moved verbatim from DESIGN.md:2700–2838, header re-levelled @@ -233,7 +241,9 @@ fn every_index_link_resolves() { #[test] fn every_contract_names_a_resolvable_ratifying_test() { // clause 2 — every kind=contract row's ratifying-test token - // resolves to a real file under crates/**/tests, bench/, or + // resolves to a real file under crates/**/tests, crates/**/src + // (in-source `#[cfg(test)] mod tests` are first-class ratifiers + // in this project — see Boss adjudication OQ1/OQ2), bench/, or // skills/**/SKILL.md. } @@ -510,3 +520,141 @@ All failure modes fail closed: contract still instructs reading a file that does not exist. 11. The milestone landed in a build-atomic shape (no commit leaves the workspace non-compiling). +12. Every `##`/`###` of the former DESIGN.md maps to exactly one + destination in the Appendix table; the three ledger additions + (`qualified-xref`, `str-abi`, `scope-boundaries`) have INDEX + rows and resolvable ratifiers; the `crates/ailang-codegen/src/lib.rs:103` + "Iter 13b" dangling cite is rewritten to drop the unresolvable + reference (keeping it would itself violate the honesty rule). + +## Appendix — Boss-adjudicated relocation map (authoritative, placeholder-free) + +This appendix supersedes any ambiguity in §Components. It is the +map the planner consumes. Every `##`/`###` of DESIGN.md (3020 +lines; no `## Decision 7` — numbering gap, not drift) has exactly +one destination. `D` = `docs/journals/2026-05-19-design-decision-records.md` +(decision-record archive). `IX` = `design/INDEX.md` preamble. + +**Bucketing principle.** *Contract* = prescriptive + obeyed/checked +by an author, the architect, or a green test (binding, schema, +enforcement, honesty-pinned, present-tense scope claim). *Model* = +explanatory narrative; reading it is optional for correctness; no +test pins it. *Decision-record* = why-X-chosen / why-Y-rejected / +"deliberately does not do" / rollback / empirical addendum / +how-the-doc-reached-its-wording. + +| `##` / `###` | Lines | Destination | +|---|---|---| +| `## Goal` | 6–18 | IX preamble | +| `## Project ecosystem` (intro) | 19–55 | IX preamble | +| ` ### What this document is — honesty rule` | 56–82 | `contracts/honesty-rule.md` (**rewritten**; pins `docs_honesty_pin.rs:70,72`) | +| `## Project language: English` | 83–92 | IX preamble | +| `## Feature-acceptance criterion` | 93–164 | `contracts/feature-acceptance.md` | +| `## Decision 1: source = data` | 165–176 | D | +| `## Decision 2: content-addressed` | 177–189 | D | +| `## Decision 3: pure core + effects` | 190–204 | `models/effects.md` (pins `effect_doc_honesty_pin.rs` present-anchors — pin reads this file) | +| `## Decision 4: HM + refinements` | 205–213 | D | +| `## Decision 5: emit LLVM IR as text` | 214–229 | D | +| `## Decision 6` intro | 230–240 | `contracts/authoring-surface.md` | +| ` (Decision 6 :241–243 audit-trail sentence)` | 241–243 | D (retired, no successor pin — §Architecture-4) | +| ` ### Why this is opening up` | 245–267 | D | +| ` ### Architectural pin: data structure is SoT` | 268–297 | `contracts/authoring-surface.md` | +| ` ### Constraints (hard, in priority order)` | 298–331 | `contracts/authoring-surface.md` | +| ` ### Candidate notations` | 332–471 | `models/authoring-surface.md` | +| ` ### First choice and rollback plan` | 472–486 | D | +| ` ### Implementation outline` | 487–519 | D | +| ` ### What this Decision deliberately does not do` | 520–536 | D | +| ` ### Form refinements during implementation` | 537–589 | D | +| ` ### Form (B) — human prose projection` | 590–674 | `models/authoring-surface.md` (the Form-B placeholder present-anchor in `docs_honesty_pin.rs` re-points here) | +| ` ### Empirical addendum` | 675–730 | D | +| `## Decision 8: explicit verified tail calls` | 731–787 | `contracts/tail-calls.md` | +| `## Decision 9` intro | 788–852 | `models/rc-uniqueness.md` | +| ` ### Per-fn arena via stack alloca` | 853–913 | `models/rc-uniqueness.md` | +| `## Decision 10` intro | 914–977 | `models/rc-uniqueness.md` | +| ` ### Why not other memory models` | 978–1014 | D | +| ` ### The LLM-aware sharpening` | 1015–1122 | `models/rc-uniqueness.md` | +| ` ### Language-design constraints (binding)` | 1123–1150 | `contracts/memory-model.md` | +| ` ### Schema additions` | 1151–1312 | `contracts/memory-model.md` | +| ` ### Advisory diagnostics` | 1313–1351 | `contracts/memory-model.md` | +| ` ### Why advisory + suppress instead of inference` | 1352–1377 | D | +| ` ### Inference algorithm` | 1378–1393 | `models/rc-uniqueness.md` | +| ` ### Codegen contract` | 1394–1412 | `contracts/memory-model.md` | +| ` ### Mode metadata is load-bearing for codegen` | 1413–1509 | `contracts/memory-model.md` | +| ` ### Adjacent extensions for mutability (out of scope)` | 1510–1519 | D | +| ` ### What this Decision deliberately does not do` | 1520–1535 | D | +| `## Decision 11` intro | 1536–1577 | `models/typeclasses.md` | +| ` ### Form-A schema (JSON authoring surface)` | 1578–1639 | `contracts/typeclasses.md` | +| ` ### Resolution and monomorphisation` | 1640–1752 | `models/typeclasses.md` | +| ` ### Cross-module references in synthesised bodies` | 1753–1823 | `contracts/typeclasses.md` (pins `codegen_import_map_fallback_pin.rs:2`, `polyfn_dot_qualified_branch_pin.rs:2`) | +| ` ### Defaults and superclasses` | 1824–1855 | `contracts/typeclasses.md` | +| ` ### Diagnostic categories` | 1856–1917 | `contracts/typeclasses.md` | +| ` ### Method dispatch` | 1918–1964 | `contracts/typeclasses.md` | +| ` ### What the typeclass design explicitly does NOT support` | 1965–2000 | D | +| ` ### Prelude (built-in) classes` | 2001–2042 | `contracts/typeclasses.md` (pins `show_no_instance_e2e.rs:47`; Show diagnostic target) | +| ` ### Heap-Str primitives` | 2043–2088 | `contracts/str-abi.md` (ledger addition — see below) | +| ` ### What this decision does NOT commit to` | 2089–2112 | D | +| `## Roundtrip Invariant` (+ 3 `###`s 2152–2208) | 2113–2208 | `contracts/roundtrip-invariant.md` (whole block kept together — pins `round_trip.rs:10,72`) | +| `## Mangling scheme` | 2209–2218 | **source-link only** (no prose file): behaviour → dropped (code is SoT); any "why" sentence → D | +| `## Convention: qualified cross-module references` | 2219–2236 | **source-link only** `qualified-xref` (ledger addition): behaviour → dropped; rationale → D | +| `## Env construction` | 2237–2265 | **source-link only** (no prose file): behaviour → dropped (code is SoT); any "why" sentence → D | +| `## Embedding ABI` intro | 2266–2333 | `contracts/embedding-abi.md` (pins `docs_honesty_pin.rs:135`) | +| ` ### Frozen value layout (M3 — one-way commitment)` | 2334–2376 | `contracts/frozen-value-layout.md` + source-link `runtime/rc.c §layout` (dual; pins `embed_record_layout_pin.rs:1`) | +| `## Data model` (+ 4 `###`s) | 2377–2615 | `contracts/data-model.md` (whole; `design_schema_drift.rs` `include_str!`s it) | +| `## Pipeline` | 2616–2662 | `models/pipeline.md` | +| `## CLI` | 2663–2686 | `models/pipeline.md` | +| `## Verification and correctness (across cycles)` | 2687–2699 | `contracts/verification.md` | +| `## Float semantics` | 2700–2838 | `contracts/float-semantics.md` (the inline `**Str ABI.**` para at 2802 is **moved to `contracts/str-abi.md`** — the one sentence-level exception, justified below) | +| `## What is not (yet) supported` | 2839–3020 | `contracts/scope-boundaries.md` (ledger addition — present-tense, honesty-pinned by `effect_doc_honesty_pin.rs:28`) | + +### Ledger additions — rationale (the brainstorm's 12-list under-counted) + +Plan-recon's exhaustive live-xref sweep proved three genuine, +distinct, currently-referenced contracts the 12-row first pass +missed. Forcing them into ill-fitting existing files would +re-create the conflation this milestone exists to end; the +ledger's purpose is per-contract addressability, so a genuine +distinct contract earns a row. + +- **`qualified-xref`** (13th, source-link only). `## Convention: + qualified cross-module references` is code-SoT per §Architecture + commitment 1 ("qualified-cross-module-ref resolution"). No prose + file; INDEX row links the resolution `//!`; ratifier + `codegen_import_map_fallback_pin.rs`. `crates/ail/src/main.rs:1393` + retargets to this row. +- **`str-abi`** (14th, prose + source-link). `### Heap-Str + primitives` (2043–2088) + the inline `**Str ABI.**` para (2802) + are one runtime-ABI contract, SoT `runtime/str.c`. Three live + xrefs name `§"Str ABI"`/`§"Heap-Str primitives"` + (`runtime/str.c:172,198`, `crates/ail/tests/e2e.rs:2843`) — they + would dangle with no destination. The 2802 para is the **single + sanctioned sentence-level move** (it is one inline bold-paragraph, + not a `###`; leaving it in `float-semantics.md` would mis-file a + Str contract under Float). Recorded as the explicit, bounded + exception to §Architecture commitment 2. +- **`scope-boundaries`** (15th, prose). `## What is not (yet) + supported` is present-tense scope assertion, honesty-pinned by + `effect_doc_honesty_pin.rs:28` (absent-string `"the built-in IO + and Diverge ops"`). A present-tense "what the language does not + do, now" claim is a contract (a checked promise), not a + decision-record; the pin already reads it, so its ratifier is + `effect_doc_honesty_pin.rs`. + +Net ledger: **15 contracts** (12 spec + 3 additions), 5 models, +one decision-record journal. The `design_index_pin.rs` clause-2 +resolution set is widened to accept `crates/**/src/*.rs` so the +in-source `memory-model` (`uniqueness.rs`) and `tail-calls` +(`lib.rs tail_call_in_non_tail_position_is_rejected`) ratifiers +resolve honestly rather than being mapped to a wrong tests/-level +file. + +### OQ7 — the dangling "Iter 13b" cite + +`crates/ailang-codegen/src/lib.rs:103` cites "Iter 13b notes in +`DESIGN.md`" — that prose was relocated out of DESIGN.md long ago; +no forward target exists in the tree. Per the honesty rule a +reference to non-existent content is itself a violation. The +comment is rewritten to drop the cite (state the behaviour +directly; no `design/` or journal pointer, because the referenced +notes no longer exist anywhere — inventing a pointer would be +fiction). This is the one reference in bucket (e) that is *deleted, +not retargeted*.