iter rt.2: DESIGN.md anchor — Roundtrip Invariant lifted to top-level
New top-level section '## Roundtrip Invariant' between Decision 11 and '## Mangling scheme'. States both directions of the .ail.json ↔ .ailx bijection, names Float-bits-hex encoding as the in- invariant mechanism (not an exception), lists the four enforcement tests by path, and explains why the property is top-level (load-bearing on language identity, not on Decision 6's surface- design rationale). Decision 6 Constraint 2 rewritten as upward cross-reference to the new section; the substantive content now lives at the anchor. Direct boss edit (no planner/implement dispatch): spec Architecture #1 fully specified the content, no design judgement deferred to execution. The iter is a deterministic projection of the spec onto DESIGN.md prose.
This commit is contained in:
+88
-4
@@ -247,10 +247,14 @@ the AST and remain projection-agnostic.
|
||||
semantic indentation, maximal-munch lexing, context-sensitive
|
||||
reductions.
|
||||
2. **AST-isomorphic.** Every surface form maps to exactly one AST
|
||||
shape. Round-trip surface → AST → canonical JSON → AST → surface
|
||||
is the identity (modulo formatting). Hashes computed via the
|
||||
round-tripped JSON must equal hashes of the same module written
|
||||
directly in JSON.
|
||||
shape. The full bijection between `.ail.json` and `.ailx` (both
|
||||
directions, BLAKE3-stable hashing, Float-bits-hex encoding,
|
||||
workspace-CI enforcement points) is anchored as the top-level
|
||||
§"Roundtrip Invariant" — this constraint records that Decision
|
||||
6's surface-design choice must satisfy that invariant; the
|
||||
invariant itself lives at top level because the property is
|
||||
load-bearing on the language identity, not on this Decision's
|
||||
surface-design rationale.
|
||||
3. **No external symbols.** ASCII only. No Greek (`∀`), no arrows
|
||||
(`→`), no subscripts. Reasoning: I substitute mojibake for
|
||||
non-ASCII characters under context pressure; foreign LLMs vary
|
||||
@@ -1750,6 +1754,86 @@ would invoke literal-defaulting which axis-7 already excluded.
|
||||
Prelude). A future Prelude milestone gates class additions on
|
||||
the Feature-acceptance criterion at the time of proposal.
|
||||
|
||||
## Roundtrip Invariant
|
||||
|
||||
Every well-formed AILang module has both a canonical `.ail.json`
|
||||
representation and a textual `.ailx` representation, and the two
|
||||
are exact projections of the same AST. Concretely, both directions
|
||||
of the bijection hold:
|
||||
|
||||
1. **JSON → text → JSON.** For every valid `.ail.json` module `J`,
|
||||
`parse(print(load_module(J)))` is canonical-byte-equal to
|
||||
`canonical::to_bytes(load_module(J))`. The textual surface is
|
||||
the inverse of the loader composed with the printer; no
|
||||
information is lost across the round-trip.
|
||||
2. **text → JSON → text.** For every well-formed `.ailx` text `t`,
|
||||
`parse(t)` is a complete AST, and re-printing `print(parse(t))`
|
||||
produces a text that re-parses to the same AST (modulo
|
||||
formatting). The parser is total over the well-formed surface
|
||||
and the printer is deterministic.
|
||||
|
||||
Hashing is the consequence the language depends on: BLAKE3 of the
|
||||
canonical bytes is identical for the two paths, so content-
|
||||
addressing is form-agnostic. An LLM author can pick either form
|
||||
without changing the identity of the module it produces.
|
||||
|
||||
### 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-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 four 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::print_then_parse_round_trips_every_fixture`
|
||||
— for every `.ail.json`, `print` then `parse` produces canonical-
|
||||
byte-equal output. Direction 1 above.
|
||||
- `crates/ailang-surface/tests/round_trip.rs::every_ailx_fixture_matches_its_json_counterpart`
|
||||
— for every `.ailx` with a same-stem `.ail.json` counterpart,
|
||||
`parse` of the text yields canonical bytes equal to the JSON
|
||||
counterpart. Pins the hand-authored `.ailx` corpus against
|
||||
drift between the two forms at the fixture level.
|
||||
- `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 fixture. The visitor
|
||||
matches each AST enum exhaustively without wildcard arms, so
|
||||
any new AST variant fails to compile until the visitor is
|
||||
extended in lockstep — the coverage table cannot silently fall
|
||||
behind the schema.
|
||||
- `crates/ail/tests/roundtrip_cli.rs::cli_render_then_parse_preserves_canonical_bytes_on_every_fixture`
|
||||
— for every `.ail.json`, the public CLI pipeline `ail render` →
|
||||
tempfile → `ail parse` reproduces BLAKE3-identical canonical
|
||||
bytes. Pins the user-facing CLI against drift that crate-
|
||||
internal tests cannot see.
|
||||
|
||||
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 Decision. Decision 6 introduces the `.ailx`
|
||||
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 Decision 6 makes the property quotable on its
|
||||
own and reviewable by the architect agent at every milestone
|
||||
close.
|
||||
|
||||
## Mangling scheme
|
||||
|
||||
All AILang functions are mangled to `@ail_<module>_<def>` — even in the
|
||||
|
||||
Reference in New Issue
Block a user