Files

T

Brummel eaa52ff64f 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.

2026-06-02 11:27:53 +02:00

1.1 KiB

Raw Permalink Blame History

Verification and correctness (across cycles)

Snapshot tests for the pretty-printer and IR emit. The diff makes regressions visible immediately.
Property tests for the JSON ↔ pretty-print roundtrip.
End-to-end tests for examples/ with expected program output.
Hash stability: a test ensures the same def always produces the same hash.
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.
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: 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.

1.1 KiB Raw Permalink Blame History

Verification and correctness (across cycles)

Verification and correctness (across cycles)

1.1 KiB

Raw Permalink Blame History