--- id: w2-code-proof name: "Wave 2: the code-shape proof (posture-A/C, ordering and determinism invariants)" status: pending 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 - [ ] 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 > To be filled by implementation agent ## Summary > To be filled on completion