alkgen/tasks/implementation/w2-code-proof.md

---
id: w2-code-proof
name: "Wave 2: the code-shape proof (posture-A/C, ordering and determinism invariants)"
status: completed
depends_on: []
scope: narrow
risk: low
impact: component
level: 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

- [x] 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
- [x] byte-identical output across repeated renders within one
      registry
- [x] byte-identical output across independent registry rebuilds
      from the same assets, including a differing registration order
- [x] `render` and `render_to_write` produce byte-identical output
      for the same set and context
- [x] document order (not sort or hash order) drives rendered order
      on the new proof set
- [x] the DO-NOT-EDIT banner gap recorded honestly in Notes; tests
      assert nothing banner-related
- [x] `cargo test`, `cargo clippy --all-targets -- -D warnings`,
      `cargo fmt --check` pass
- [x] 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.