Debug80 Docs

Nucleus Z80 Runtime and Backend Contract 0.110

← 9. Generated-code integrity · Contents

10. Conformance and measurement ​

10.1 Required evidence ​

The active proof suite assembles the compiler and generated program with AZM, runs the result through Debug80, and checks source-level observations. It must cover the accepted and rejected Chapter 18 programs as implementation stages make them available, including normal output, static data, alias-visible mutation, recursion, recoverable failure, every reachable trap, exact diagnostic positions, and capacity boundaries.

A module or boundary proof may test a smaller path. It must identify the language or contract rule it establishes and may not substitute a fixed program template for a claimed general compiler feature.

Object-stream producer, materializer, and storage proofs cover the required cases in the NOBJ format separately from source-language execution. They include runtime-provider identity, link-context, helper-layout, and length mismatch, execution at two distinct linked layouts including runtime base $8003 with changed writable-state addresses, deferred MAP.usedLength validation, direct flat wire loading, and stored banked materialization without private backing for every bank.

10.2 Measurement reports ​

Every target size or timing claim comes from fresh assembled output and names the proof that produced it. Reports separate compiler code, compiler immutable data, peak workspace, generated program, target runtime, fixed runtime state, activation storage, instruction count, and T-states. A projection states its measured basis; an untested expectation is labelled a hypothesis.

test/nobj.test.ts assembles runtime identity $0009 under defaultRuntimeLinkContext and measures a 731-byte canonical linked helper image. This identity includes checked four-way integer conversion, signed comparison, signed division and modulo, signed loop continuation, and mixed u8/i8 promotion in addition to the existing unsigned and aggregate helpers. Its 36-byte vector appends the target-specific packet gateway, and its final 42-byte helper validates the native result and enters the ordinary terminal trap dispatcher with the original root frame restored. proofs/stage9-conformance-z80-slice-proof.json includes the historical direct service adapters and measures 921 bytes; proofs/chapter21-target-z80-slice-proof.json selects an 899-byte proof form.