docs(contracts): finish the honesty pass (0003, 0008, 0013, 0017)

Third tranche, completing the honesty-rule sweep across the remaining
contracts. Same conservative bar: cut unbacked-verification claims,
change/deletion history, and forward-intent; keep present-state design
rationale.

- 0003: drop "sanitiser-verified" — no TSan/sanitiser test exists in
  the tree, so the claim asserts a verification that does not happen.
  The data-race-freedom property (argued from the non-atomic-but-never-
  shared hot path + atomic-relaxed shared counter) stays.
- 0008: the `Type::Con.name` hash paragraph ("the tightening shifted
  the hashes ... The new pins ... re-asserts the pre-tightening hashes")
  -> present-state: which fixtures carry which hash shape and which test
  pins each.
- 0013: drop "the former codegen-side fallback (at ..., and the
  now-deleted `synth_with_extras`) is retracted" (deletion history; the
  present fact is that codegen does not re-resolve, per the boundary);
  "A future refactor that loosens any one of the four breaks ..." ->
  present-tense statement that the four are load-bearing and each pinned.
- 0017: drop "a real cost surfaced by the `bench_closure_chain`
  regression at the operator-routing-eq-ord milestone" (history) and
  "the symmetric extensions are mechanical when the first such workload
  appears" (forward-intent); keep the present-state allocation cost, the
  pin, and the Int-only-asymmetry rationale.

All 18 contracts now reviewed against the code. Ledger pins green;
honesty sweep clean.

design/contracts/0003-embedding-abi.md

@@ -38,7 +38,7 @@ thread (`Ctx: !Send`) and each `ailang_ctx_t` is
 single-thread-per-ctx. The one datum a multi-threaded host shares
 is the global RC-stats fallback counter (used when no ctx is
 bound); it is atomic-relaxed so the swarm's leak accounting is
-exact. The swarm artefact is data-race-free, sanitiser-verified.
+exact. The swarm artefact is data-race-free by this split.
 The staticlib swarm artefact is **RC-only**:
 `ail build --emit=staticlib` rejects `--alloc=bump` (the bench
 stub is leak-only and not swarm-safe; `--alloc=gc` no longer

design/contracts/0008-memory-model.md

@@ -162,15 +162,12 @@ Skipped from serialisation when empty so existing fixtures keep
 bit-identical canonical-JSON hashes (regression-pinned by
 `iter19b_empty_suppress_preserves_pre_19b_hashes` and
 `iter19b_schema_extension_preserves_pre_19b_hashes`).
-The canonical-form tightening for `Type::Con.name` shifted the
+Two cross-module fixtures (`ordering_match.ail.json` and
-hashes of two cross-module fixtures (`ordering_match.ail.json` and
+`test_22b1_dup_a.ail.json`) carry canonical-form `Type::Con.name`
-`test_22b1_dup_a.ail.json`); all intra-module fixtures, including
+hashes, pinned by `ct4_migrated_fixtures_have_canonical_form_hashes`;
-the regression-pinned `sum.ail.json` and `list.ail.json`, remain
+all intra-module fixtures, including `sum.ail.json` and
-bit-identical. The new pins are
+`list.ail.json`, are pinned bit-identical by
-`ct4_migrated_fixtures_have_canonical_form_hashes` (locks the
+`ct4_unmigrated_fixtures_remain_bit_identical`.
-post-migration hashes) and
-`ct4_unmigrated_fixtures_remain_bit_identical` (re-asserts the
-pre-tightening hashes still hold).
 
 ## Advisory diagnostics
 

design/contracts/0013-typeclasses.md

@@ -115,10 +115,7 @@ Three invariants make this work:
    the callee against the workspace and emits
    `Callee::Static { module, fn_name, .. }` carrying the resolved owner.
    Codegen consumes that identity off the MIR `App` node and does
-   **not** re-resolve it — the former codegen-side
+   **not** re-resolve it, per the
-   `import_map`-then-`module_user_fns` fallback (at `resolve_top_level_fn`,
-   `lower_app`'s cross-module arm, and the now-deleted
-   `synth_with_extras`) is retracted, per the
    [check→codegen boundary](0018-check-codegen-boundary.md). Both ends
    were independently typechecked under their own module contexts before
    mono ran; the cross-module reference is a post-mono construct, not a
@@ -163,9 +160,8 @@ cross-module reference, invariant (2) makes codegen able to resolve
 post-mono references, invariant (3) makes the typecheck-time
 discharge fire correctly when no instance exists, invariant (4)
 makes bare prelude-fn names resolve from user modules at the source
-level. A future refactor that loosens any one of the four breaks
+level. Loosening any one breaks the user-ADT trajectory or the
-the user-ADT trajectory or the Float-named-fn surface; the test
+Float-named-fn surface, so each is pinned:
-pins at
 `crates/ail/tests/codegen_import_map_fallback_pin.rs` (invariant 2),
 `crates/ail/tests/polyfn_dot_qualified_branch_pin.rs` (invariant 3
 + lockstep), `crates/ail/tests/float_compare_smoke_e2e.rs`

design/contracts/0017-prelude-classes.md

@@ -25,15 +25,13 @@ codegen intercept short-circuits this indirection: `lt__Int`,
 overridden to emit `icmp slt i64` / `sle i64` / `sgt i64` /
 `sge i64` / `ne i64` directly, bypassing the `compare__Int` →
 `Ordering`-ctor → `match` path. Without this short-circuit the
-`Ordering` ctor allocates per call inside hot loops — a real
+`Ordering` ctor allocates per call inside hot loops; the
-cost surfaced by the `bench_closure_chain` regression at the
+short-circuit is pinned by
-operator-routing-eq-ord milestone and pinned by
+`crates/ail/tests/ord_int_intercept_ir_pin.rs`. It
-`crates/ail/tests/ord_int_intercept_ir_pin.rs`. The short-circuit
 is *Int-only* by deliberate asymmetry: no current bench or
 example fixture exercises Ord-`lt`/`le`/`gt`/`ge` at Bool or
 Str at sufficient call frequency to justify the intercept-arm
-maintenance; the symmetric extensions are mechanical when the
+maintenance.
-first such workload appears.
 
 Float has neither `Eq` nor `Ord` instance per [Float semantics](
 0005-float-semantics.md); a polymorphic helper invoked at Float fires