From eaa52ff64ff5dcb0598f5963069fd106218cac44 Mon Sep 17 00:00:00 2001 From: Brummel Date: Tue, 2 Jun 2026 11:27:53 +0200 Subject: [PATCH] docs(contracts): honesty-prose cleanup + ratifier integrity MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Second tranche of the contracts-against-code audit. Two threads, both applied conservatively under the over-correction guards in docs_honesty_pin.rs (the self-labelled tiebreaker in 0008 and the Diverge-reserved anchor in 0010 are deliberate honest content and were left untouched; design rationale that explains a present-state design principle — semantic-locality, the reuse-as-wrapper reasons — was also preserved). Honesty-rule (0007): demote clear change/deletion narration to present tense. - 0008: drop "they were promoted from ... to ... Recorded here so"; strip the "Iter A"/"Iter B" iteration labels (the descriptive titles carry the meaning); drop "(no longer a carve-out)". - 0001: "were rewired to use ... was deleted at the same time" -> present tense. (The substance was already correct: `pretty.rs` holds only the diagnostic helpers; an audit agent had misread the line as "pretty.rs was deleted" — the file exists, the printer code does not.) - 0012: drop "Per the tail-call survey of existing fixtures" and "Migration of existing fixtures is partial" -> present-state description of which corpus fixtures carry the tail marker. Ratifier integrity: a contract that names a test which does not ratify it is itself a form of the dishonesty this ledger forbids. - 0014 named `bench/architect_sweeps.sh`, which sweeps honesty-anchors and ratifies none of the six verification mechanisms; and claim 5 cited `tests/expected/`, which never existed (git log empty). Point claim 5 at the real golden mechanism (`crates/ail/tests/snapshots/` via `ir_snapshot.rs`) and the footer at each mechanism's actual test. - 0015's four constraints are guaranteed by absence (no thunk/`ref`/ `IORef` node, non-recursive `let`); the named uniqueness in-source tests only count RC consumes, never the constraints. State the by-construction guarantee and point the ratifier at `ast.rs` (the single source of truth for which nodes exist). - INDEX ratifying-test column updated for both to match. All ledger pins green (docs_honesty_pin, design_index_pin incl. every_contract_names_a_resolvable_ratifying_test, effect_doc_honesty_pin, carve_out_inventory); architect honesty sweep clean. Deferred, recommend-only: 0016-method-dispatch carries no invariant absent from 0013 (merge candidate), but a contract-file merge touches INDEX, the retired-counter convention, and cross-refs — a structural call left for explicit direction. Minor history phrasing in 0008's Type::Con.name hash-shift paragraph (§"FnDef.suppress") also left. --- design/INDEX.md | 4 ++-- design/contracts/0001-authoring-surface.md | 9 ++++----- design/contracts/0008-memory-model.md | 17 +++++++---------- design/contracts/0012-tail-calls.md | 14 ++++++-------- design/contracts/0014-verification.md | 11 +++++++++-- design/contracts/0015-language-constraints.md | 14 +++++++++----- 6 files changed, 37 insertions(+), 32 deletions(-) diff --git a/design/INDEX.md b/design/INDEX.md index a27fd0e..f891ff6 100644 --- a/design/INDEX.md +++ b/design/INDEX.md @@ -82,7 +82,7 @@ is the default. | feature-acceptance | brainstorm-gate / stable | CLAUDE.md | design/contracts/0004-feature-acceptance.md | | authoring-surface | LLM author / stable | crates/ailang-surface/tests/round_trip.rs | design/contracts/0001-authoring-surface.md | | roundtrip-invariant | every release / stable | crates/ailang-surface/tests/round_trip.rs | design/contracts/0009-roundtrip-invariant.md | -| language-constraints | LLM author / stable | crates/ailang-check/src/uniqueness.rs (in-source mod tests) | design/contracts/0015-language-constraints.md | +| language-constraints | LLM author / stable | crates/ailang-core/src/ast.rs (no thunk/ref/IORef node — by construction) | design/contracts/0015-language-constraints.md | | memory-model | LLM author / stable | crates/ailang-check/src/uniqueness.rs + linearity.rs (in-source mod tests) | design/contracts/0008-memory-model.md | | data-model | LLM author / stable | crates/ailang-core/tests/design_schema_drift.rs | design/contracts/0002-data-model.md | | mangling | codegen / stable | crates/ail/tests/eq_ord_e2e.rs | crates/ailang-codegen/src/lib.rs //! | @@ -98,7 +98,7 @@ is the default. | honesty-rule | architect+grounding / stable | crates/ailang-core/tests/docs_honesty_pin.rs | design/contracts/0007-honesty-rule.md | | embedding-abi | embedding host / stable | crates/ailang-codegen/tests/embed_record_layout_pin.rs | design/contracts/0003-embedding-abi.md | | scope-boundaries | architect+author / stable | crates/ailang-core/tests/effect_doc_honesty_pin.rs | design/contracts/0010-scope-boundaries.md | -| verification | architect / stable | bench/architect_sweeps.sh | design/contracts/0014-verification.md | +| verification | architect / stable | crates/ail/tests/ir_snapshot.rs (+ round_trip, hash_pin, e2e) | design/contracts/0014-verification.md | | check-codegen-boundary| architect / stable | crates/ailang-check/tests/lower_to_mir_ty.rs (callee_classification_builtin_and_static) | design/contracts/0018-check-codegen-boundary.md | ## Models diff --git a/design/contracts/0001-authoring-surface.md b/design/contracts/0001-authoring-surface.md index 938d88f..fd1c7e8 100644 --- a/design/contracts/0001-authoring-surface.md +++ b/design/contracts/0001-authoring-surface.md @@ -7,11 +7,10 @@ the `ailang-surface` crate (parser + printer). Form-A is gated against drift by `ailang-surface/tests/round_trip.rs`, which parses every `.ail` fixture, prints it back, re-parses, and demands canonical-byte equality. `ail render` and both branches -of `ail describe` were rewired to use `ailang_surface::print`, making -form (A) the **sole** text projection of a module — the legacy -non-round-tripping pretty-printer code in `pretty.rs` was deleted at -the same time, leaving only diagnostic helpers (`type_to_string`, -`pattern_to_string`, `manifest`) public. +of `ail describe` project through `ailang_surface::print`, so +form (A) is the **sole** text projection of a module. `pretty.rs` +carries no round-tripping printer — only the diagnostic helpers +(`type_to_string`, `pattern_to_string`, `manifest`) are public there. ## Architectural pin: data structure is the source of truth diff --git a/design/contracts/0008-memory-model.md b/design/contracts/0008-memory-model.md index 1783c42..d475bff 100644 --- a/design/contracts/0008-memory-model.md +++ b/design/contracts/0008-memory-model.md @@ -253,14 +253,11 @@ it is bench-only and never a production target. `param_modes` and `ret_mode` on `Type::Fn` are not merely typechecker metadata — codegen consults both to decide where to -emit drop calls. They were promoted from -"annotation that the typechecker enforces" to "annotation that -codegen reads to keep RC correct". Recorded here so the schema -metadata's role is explicit: +emit drop calls: **`param_modes` — drop-emission gates.** -- **Iter B: Own-param dec at fn return.** When a fn body +- **Own-param dec at fn return.** When a fn body fall-throughs to a `ret` (no tail-call), every parameter with `param_modes[i] == Own` is dec'd before the `ret` iff its uniqueness `consume_count == 0` and the ret value is not the @@ -268,7 +265,7 @@ metadata's role is explicit: the caller's ownership by contract. (There is no `Implicit` parameter any longer — every param is `Own` or `Borrow`.) -- **Iter A: arm-close pattern-binder dec.** When a match-arm's +- **Arm-close pattern-binder dec.** When a match-arm's body terminates without a tail-call, every ptr-typed pattern-bound binder pushed by the arm is dec'd at arm close iff its `consume_count == 0` and it is not the arm's tail @@ -278,8 +275,8 @@ metadata's role is explicit: the caller still references. - **Pre-tail-call shallow-dec.** When a match-arm's - body IS a tail call, both Iter A and Iter B are skipped (the - block is terminated). A separate seam in `lower_match` emits + body IS a tail call, both the own-param dec and the arm-close + pattern-binder dec are skipped (the block is terminated). A separate seam in `lower_match` emits a shallow `ailang_rc_dec` on the scrutinee outer cell BEFORE the tail call, gated identically on the scrutinee mode plus the requirement that every ptr-typed slot in the active @@ -423,8 +420,8 @@ twice (double-free under a hypothetical Consume + scope-close). subsequent work added codegen consumers, not new schema fields. - Does not introduce a new `Type` variant. Mode metadata stays flat on `Type::Fn` (see "Schema additions" above on why). -**Let-aliases of borrowed values are propagated** (no longer a -carve-out). A let-binder whose value is a bare `Term::Var` +**Let-aliases of borrowed values are propagated.** A let-binder +whose value is a bare `Term::Var` resolving to a tracked binder is treated as an alias of that source on both axes of the ownership analysis: diff --git a/design/contracts/0012-tail-calls.md b/design/contracts/0012-tail-calls.md index 0eb523d..e8b1b5b 100644 --- a/design/contracts/0012-tail-calls.md +++ b/design/contracts/0012-tail-calls.md @@ -46,9 +46,8 @@ Solution: explicit, verified tail calls. the constraint-1 budget (see [authoring surface](0001-authoring-surface.md)). -**What this does NOT promise.** Per the tail-call survey of existing fixtures, -many existing recursive calls are *not* in tail position -because they are arguments to constructor calls (e.g. +**What this does NOT promise.** Many recursive calls are *not* in +tail position because they are arguments to constructor calls (e.g. `Cons (f h) (map f t)`). The current pipeline adds annotation + verification; it does **not** add a CPS transform or accumulator-form rewrite. Programs whose recursion is constructor-blocked @@ -58,10 +57,9 @@ accumulator-form variant (`map_acc`, `fold_left`, etc.) explicitly. The stdlib ships both forms where relevant. -Migration of existing fixtures is partial: only -`print_list`-style terminal recursions get marked. The -constructor-blocked recursions in `map`, `sort`, `insert` -remain unmarked — they cannot benefit from `musttail` -without a source-level rewrite. +In the corpus, only terminal recursions (`print_list`-style) +carry the tail marker; the constructor-blocked recursions in +`map`, `sort`, `insert` are unmarked — they cannot benefit from +`musttail` without a source-level rewrite. Ratified by: `crates/ailang-check/src/lib.rs`. diff --git a/design/contracts/0014-verification.md b/design/contracts/0014-verification.md index 2d17968..f986895 100644 --- a/design/contracts/0014-verification.md +++ b/design/contracts/0014-verification.md @@ -9,9 +9,16 @@ 3. **End-to-end tests** for `examples/` with expected program output. 4. **Hash stability**: a test ensures the same def always produces the same hash. -5. **CI pin** of the outputs in `tests/expected/`. +5. **CI pin** of emitted output: the committed golden snapshots in + `crates/ail/tests/snapshots/` (driven by `ir_snapshot.rs`) are + byte-compared on every run. 6. **Rustdoc cleanliness**: `cargo doc --no-deps` runs warning-free. Fixing a rustdoc warning is part of the iteration that introduced it, not a follow-up. -Ratified by: `bench/architect_sweeps.sh`. +Ratified by: each mechanism's own test — the round-trip property +(`crates/ailang-surface/tests/round_trip.rs`), the golden snapshots +(`crates/ail/tests/ir_snapshot.rs`), hash stability +(`crates/ailang-core/tests/hash_pin.rs`), the `examples/` e2e suite +(`crates/ail/tests/e2e.rs`), and the warning-free +`cargo doc --no-deps` build. diff --git a/design/contracts/0015-language-constraints.md b/design/contracts/0015-language-constraints.md index bc1fb90..d386d04 100644 --- a/design/contracts/0015-language-constraints.md +++ b/design/contracts/0015-language-constraints.md @@ -3,10 +3,8 @@ ## Language-design constraints (binding) The four constraints below are necessary preconditions for RC to -be sound and complete *without* a cycle-collector backstop. They -are not new — AILang already satisfies all four — but the -[memory model](0008-memory-model.md) makes them load-bearing rather -than incidental: +be sound and complete *without* a cycle-collector backstop. The +[memory model](0008-memory-model.md) relies on all four: 1. **Strict evaluation.** Every `Term::App` (see [Data model](0002-data-model.md)) argument is fully @@ -38,4 +36,10 @@ load-bearing structural reason behind several rejections under the [feature-acceptance](0004-feature-acceptance.md) bug-class-reintroduction discriminator (notably iterated-mutable-state reasoning). -Ratified by: `crates/ailang-check/src/uniqueness.rs` (in-source mod tests). +Guaranteed by construction, not by a positive test: the AST has no +thunk, `ref`, or `IORef` node, and `(let x EXPR ...)` binds `x` only +in the body, never in `EXPR` — there is no construct that could +violate constraints 1–3, and constraint 4 follows from them. The +binding force is the design-time +[feature-acceptance](0004-feature-acceptance.md) gate, which rejects +any proposal that would reintroduce one of them.