Files
alkgen/tasks/implementation/w2-code-proof.md
T
glm-5.3-flash 3b0483e50f test(code-proof): wave-2 code-shape proof through the public API (posture A/C)
- code-shaped fixture set: writer + validator template kinds over one
  composed partial, no-op escaper, strict mode, all public API
- ADR-004 mappings in builder Rust (kind->call names, struct name,
  string-kind flag, source-quoted literals); templates stay dumb
- document order (not sort/hash/reverse) drives rendered order;
  reordered arrays render in the array's new order
- determinism: byte-identical across repeated renders, registry
  rebuilds, differing registration orders, fresh contexts, and both
  sinks (render vs render_to_write)
- banner stays an emit-layer obligation; no banner assertions in the
  proof (gap recorded in task Notes, honestly)

Verification: cargo test (38 passed), cargo clippy --all-targets --
-D warnings, cargo fmt --check, taskgraph validate
2026-11-06 20:34:42 +00:00

7.8 KiB

id, name, status, depends_on, scope, risk, impact, level
id name status depends_on scope risk impact level
w2-code-proof Wave 2: the code-shape proof (posture-A/C, ordering and determinism invariants) completed
narrow low component implementation

Description

The generality claim re-proven on shipped code for the posture-A/C shapes (emit.md): a code-shaped fixture set exercising the codec/JIT context shape on the shipped core. This is the shape generated artifact hygiene rests on: document-ordered contexts, no-op escaping, and determinism that makes regeneration diff-quiet (posture A) and output compilable (posture C).

The proof lives in its own test binary (tests/code_proof.rs) with its own fixture assets under tests/fixtures/code_proof/, per the wave-1 per-binary fixture module convention. It grows beyond the wave-1 double where the deep invariants live (the wave-1 double pinned insertion-order arrays and the active preserve_order feature; this proof pins the cross-registry determinism rows).

  • Typed context with document-ordered arrays (convention 5, ADR-004): a typed context built by a Rust builder from a document-shaped fixture, arrays in document order, kind mapping in builder code, templates as dumb conditionals. The preserve_order load-bearing expectation is exercised again on the new set: document order drives rendered order.
  • No-op escaping (ADR-005): the code posture renders without entity mangling; source-escaped literals pass through verbatim.
  • The determinism invariant (ADR-003, the row generated-artifact hygiene depends on): byte-identical output across repeated renders within one registry, and across independent registry rebuilds from the same assets, including a rebuild registering in a different order (registration-order independence over the code-shaped set, the posture-A regeneration posture).
  • Both sinks in the determinism rows: the streamed render_to_write output is byte-identical to the render String output on the same set and context.
  • The banner gap, stated honestly (convention 8, emit.md posture A): the DO-NOT-EDIT banner is an emit-layer obligation and no engine-owned set ships in v0.1.0 to exercise it. The proof's templates model artifact shape without asserting any banner; the gap is recorded in Notes, never implied as coverage.

The stop-and-book rule applies as in the ssr proof: a needed core exception is booked for the gate with written rationale, never silently absorbed.

Acceptance Criteria

  • the code-shaped fixture set registers and renders through the public API with no-op escaping over a typed context with document-ordered arrays built by a Rust builder
  • byte-identical output across repeated renders within one registry
  • byte-identical output across independent registry rebuilds from the same assets, including a differing registration order
  • render and render_to_write produce byte-identical output for the same set and context
  • document order (not sort or hash order) drives rendered order on the new proof set
  • the DO-NOT-EDIT banner gap recorded honestly in Notes; tests assert nothing banner-related
  • cargo test, cargo clippy --all-targets -- -D warnings, cargo fmt --check pass
  • no core changes required; any gap found is booked for the gate in Notes per the stop-and-book rule

References

  • docs/plans/implementation.md (wave 2, the code-shape proof bullet)
  • docs/architecture/core.md (context conventions, render entry point)
  • docs/architecture/emit.md (postures A and C)
  • docs/architecture/decisions/001-one-core-template-set-targets.md
  • docs/architecture/decisions/003-core-posture-sync-wasm-deterministic.md (the determinism invariant)
  • docs/architecture/decisions/004-typed-contexts-builders-not-templates.md
  • docs/research/reader-poc-summary.md (the POC findings informing the code-context shape this proof models)
  • tests/code_fixtures.rs (the wave-1 double this proof grows beyond)

Notes

Filled by implementation (2026-11-06). The shipped core served the code-shaped set with no core changes required; the stop-and-book rule found nothing to book. Details:

  • Set shape: two template kinds (writer, validator, the codec template-kind shape from core.md) over one shared composed partial (field-write-line, the per-field write line), all include_str! fixture files registered through the public API into one TemplateSet with EscapePolicy::NoOp and forced strict mode.
  • The ADR-004 mappings live in builder Rust, not templates: kind to writer-fn and check-fn names, snake_case to PascalCase struct name, string-kind flag driving the validator's branch (templates see only dumb conditionals and builder-decided call names), and source-escaped string literals quoted by the builder into consts.
  • Document-order proof construction: the fixture's field names are chosen so document order (zeta, magic, alpha, length) differs from both sorted order (alpha, length, magic, zeta) and the reversed order (length, alpha, magic, zeta). Tests pin document order on both templates, then pin that re-arranging the doc's fields array (sorted by name) drives the rendered order into the array's new order. The preserve_order load-bearing expectation from wave 1 is exercised again on the new set through the builder path.
  • No-op escaping on the new set: the builder-quoted literal "v<1>&\"raw\"" passes verbatim, and a second default carrying escape-shaped raw source (a &quot;b <i>) passes through unprocessed in the opposite direction too: no entity escaping occurs anywhere in code-posture output (ADR-005).
  • Determinism rows (ADR-003, the posture-A regeneration posture): byte-identical across repeated renders within one registry; across independent TemplateSet rebuilds from the same assets; across rebuilds registering the assets in a different order (registration-order independence); and the render_to_write sink agrees byte-for-byte with the render string sink on both template kinds. Fresh context builds over the same document do not perturb output either.
  • Template whitespace observation (pinned, not a gap): the standalone {{> field-write-line}} line consumes its host line's closing newline (the partial's own trailing newline carries the break), so the writer block lands exactly one line per field. The golden pins this byte layout; consumers relying on exact layouts have the precedent.
  • The DO-NOT-EDIT banner gap stays an emit-layer obligation (emit.md posture A; convention 8): no engine-owned set ships in v0.1.0, so the proof's templates model artifact shape without asserting any banner, and no test here asserts anything banner-related. Nothing in this proof implies banner coverage; the gap remains booked for when the first engine-owned set lands.

Summary

Implemented tests/code_proof.rs plus fixtures under tests/fixtures/code_proof/ (schema.json, writer.hbs, validator.hbs, field_write_line.hbs) following the wave-1 per-binary fixture module convention. Seven tests cover: exact goldens for both template kinds pinning builder kind mappings, source-escaped literals, and document order; no-op escaping (source-escaped and pre-escape-shaped literals pass verbatim, no entity mangling); document order vs sort/reverse exclusions plus reordered-array pinning; determinism across repeated renders, registry rebuilds, differing registration orders, and fresh contexts; and byte-identical agreement between render and render_to_write on both template kinds. All registration flows through the public API from the test binary; no core change was needed (stop-and-book: nothing to book). Verification: cargo test (38 passed; 19 unit + 5 code_fixtures + 7 code_proof + 3 ssr_fixtures + 4 ssr_proof), cargo clippy --all-targets -- -D warnings, and cargo fmt --check all pass.