Files

T

Brummel 625fe849be docs(contracts): reconcile contracts + honesty-pin with shipped reality

First tranche of a contracts-against-code audit (the inverse of the
usual direction: testing the ledger's claims against the code). Each
fix here is a verified factual divergence between a contract and the
code; the direction of the fix follows which side actually drifted.

Code drifted from the stated goal -> fix the code:

- 0014's claim 6 ("`cargo doc --no-deps` runs warning-free") was the
  design goal; reality had 6 warnings. Demote the offending intra-doc
  links to plain code spans so the docs match the goal:
  - ailang-core: `[`load_workspace`]` cannot resolve from core (the
    fn lives in ailang-surface, which core may not depend on) — three
    sites in workspace.rs.
  - ailang-check: three public-item docs linked the `pub(crate)`
    helpers `qualify_local_types` / `qualify_workspace_types`.
  `cargo doc --no-deps --workspace` is now warning-free.

Contract stale, code legitimately advanced -> fix the contract:

- 0011 stated `float_to_str` "codegen is reserved and not yet
  shipped". It is shipped: lowers to `@ailang_float_to_str(double)`,
  green under the codegen `float_to_str_no_longer_errors_internal`
  unit test and the e2e `float_to_str_smoke`. The docs_honesty_pin
  anchor that protected the stale "reserved" wording moved in lockstep
  to assert the present-tense lowering instead — the pin had been
  guarding a claim the code already falsified.
- 0013 named the diagnostic `ConstraintReferencesUnboundTypeVar`; the
  variant is `UnboundConstraintTypeVar` (workspace.rs), and its scope
  is a class-method signature whose constraint mentions a tyvar bound
  neither by the method's `forall` nor by the class `param`.
- 0017 called the primitive Eq/Ord bodies "placeholder lambdas"; they
  carry the `(intrinsic)` marker — the lockstep partner to the
  INTERCEPTS registry, not a placeholder.
- 0009 said "seven" `.ail.json` carve-outs and described the inventory
  test as pinning seven; the test pins twelve (7 subject-matter + 4
  recur + 1 loop-binder, per carve_out_inventory.rs).

Verified separately: 0001's "pretty-printer code in pretty.rs was
deleted, leaving only diagnostic helpers" is factually correct (an
audit agent misread it as "pretty.rs was deleted"); its only issue is
history phrasing, deferred to the honesty-prose tranche.

Deferred to later tranches: honesty-rule prose (history/rationale that
is not a protected honest-reserved/tiebreaker anchor), stale/mislinked
ratifying-tests (0014's `architect_sweeps.sh`, 0015's uniqueness
in-source tests), 0014's never-existent `tests/expected/`, 0012's
non-exhaustive tail-context list, and the 0016<->0013 redundancy.

2026-06-02 11:14:01 +02:00

4.8 KiB

Raw Blame History

Roundtrip Invariant

Every well-formed AILang module has a canonical .ail.json representation (the hashable, content-addressed JSON-AST) and a hand-authored .ail representation (Form A, the authoring projection). The JSON-AST is derived from .ail in-process by consumers that need it; the round-trip is now the property of that derivation, not the byte-level agreement of two on-disk forms.

Concretely:

Parse-determinism. For every well-formed .ail text t, ailang_surface::parse(t) produces a unique AST. The parser is a pure function of input — no randomness, no time dependence, no environment leak. Hashing canonical::to_bytes(parse(t)) is therefore well-defined for any .ail source.
Idempotency under print. For every well-formed .ail text t, canonical(parse(t)) == canonical(parse(print(parse(t)))). The printer is a left-inverse of the parser modulo canonical form: print-then-parse is a no-op on the canonical bytes.
CLI-pipeline idempotency. For every .ail fixture, the public CLI pipeline ail parse | ail render | ail parse is byte-identical to direct ail parse of the source .ail. Pins drift that crate-internal tests cannot see.
Carve-out anchor. Twelve .ail.json-only fixtures (canonical-form / negative-typecheck rejection tests) survive in the corpus by structural necessity. They participate in their own dedicated rejection-shape tests, not in the round-trip gate. (The prelude is embedded as examples/prelude.ail in ailang-surface and parsed at compile time via ailang_surface::parse_prelude.)

Hashing is the consequence the language depends on: BLAKE3 of the canonical bytes is well-defined for any .ail source via parse- determinism. An LLM author writes .ail; the build derives the canonical hash without ambiguity.

Float literals are inside the invariant

Float literals carry an IEEE-754 bit pattern, not a decimal approximation. The canonical encoding is {"kind":"float","bits":"<16-lowercase-hex>"} and the surface emits the same bits-hex string. NaN, ±Inf, signed zero, and subnormals all round-trip exactly because the JSON-number path is bypassed (see Float semantics, "Form-A serialisation"). Floats are not an exception to the invariant — the bits-hex encoding is the mechanism that keeps them inside it.

Enforcement

The invariant is workspace-CI-enforced by five tests, each operating on the examples/ corpus via dynamic read_dir collection (no hardcoded fixture list, so newly added fixtures inherit the gate automatically):

crates/ailang-surface/tests/round_trip.rs::parse_is_deterministic_over_every_ail_fixture — for every .ail, parse twice and assert canonical-byte equality between the two ASTs. Direction 1 above.
crates/ailang-surface/tests/round_trip.rs::parse_then_print_then_parse_is_idempotent_on_every_ail_fixture — for every .ail text t, parse(t) and parse(print(parse(t))) produce canonical-byte-equal AST. Direction 2 above.
crates/ail/tests/roundtrip_cli.rs::cli_parse_then_render_then_parse_is_idempotent — for every .ail, the public CLI pipeline ail parse | ail render | ail parse reproduces canonical bytes byte-identical to direct ail parse. Pins drift internal tests cannot see.
crates/ailang-core/tests/schema_coverage.rs::every_ast_variant_is_observed_in_the_fixture_corpus — every variant of Def, Term, Pattern, Literal, Type, and ParamMode appears in at least one .ail fixture. New AST variants fail compile until the visitor and corpus are extended in lockstep.
crates/ailang-core/tests/carve_out_inventory.rs::examples_ail_json_inventory_matches_carve_outs — exactly the twelve named carve-out files exist under examples/*.ail.json at any commit. A new .ail.json or a missing carve-out fails the test.

A new fixture or a new AST variant that violates the invariant fails one of these tests; the fix is in render or parse code, never by relaxing the test.

Why this is anchored at top level

The invariant is a property of the language identity, not of any one surface-design choice. The authoring surface introduces the .ail surface and lists round-trip-as-property as one of its constraints, but the property is load-bearing for every downstream concern that treats the two forms as exchangeable: content-addressed hashing, the LLM-author's choice of authoring form, the integrity of fixture cross-references, and the prerequisite for empirical cross-model authoring-form studies. Lifting it out of the authoring-surface contract makes the property quotable on its own and reviewable by the architect agent at every milestone close.

Ratified by: crates/ailang-surface/tests/round_trip.rs.

4.8 KiB Raw Blame History

Roundtrip Invariant