docs(contracts): honesty-prose cleanup + ratifier integrity

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

@@ -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

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
+of `ail describe` project through `ailang_surface::print`, so
-form (A) the **sole** text projection of a module — the legacy
+form (A) is the **sole** text projection of a module. `pretty.rs`
-non-round-tripping pretty-printer code in `pretty.rs` was deleted at
+carries no round-tripping printer — only the diagnostic helpers
-the same time, leaving only diagnostic helpers (`type_to_string`,
+(`type_to_string`, `pattern_to_string`, `manifest`) are public there.
-`pattern_to_string`, `manifest`) public.
 
 ## Architectural pin: data structure is the source of truth
 

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
+emit drop calls:
-"annotation that the typechecker enforces" to "annotation that
-codegen reads to keep RC correct". Recorded here so the schema
-metadata's role is explicit:
 
 **`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
+  body IS a tail call, both the own-param dec and the arm-close
-  block is terminated). A separate seam in `lower_match` emits
+  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
+**Let-aliases of borrowed values are propagated.** A let-binder
-carve-out). A let-binder whose value is a bare `Term::Var`
+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:
 

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,
+**What this does NOT promise.** Many recursive calls are *not* in
-many existing recursive calls are *not* in tail position
+tail position because they are arguments to constructor calls (e.g.
-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
+In the corpus, only terminal recursions (`print_list`-style)
-`print_list`-style terminal recursions get marked. The
+carry the tail marker; the constructor-blocked recursions in
-constructor-blocked recursions in `map`, `sort`, `insert`
+`map`, `sort`, `insert` are unmarked — they cannot benefit from
-remain unmarked — they cannot benefit from `musttail`
+`musttail` without a source-level rewrite.
-without a source-level rewrite.
 
 Ratified by: `crates/ailang-check/src/lib.rs`.

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.

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
+be sound and complete *without* a cycle-collector backstop. The
-are not new — AILang already satisfies all four — but the
+[memory model](0008-memory-model.md) relies on all four:
-[memory model](0008-memory-model.md) makes them load-bearing rather
-than incidental:
 
 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.