SKIP TO CONTENT
STRATA
04 · VERIFICATION
5 CHECKS · RUN LOCALLY · NO AUDIT CLAIMED

Five checks,
and none of them
is the same check twice.

The arithmetic is checked against the same arithmetic built out of the primitive. The machine is checked against a second interpreter that shares no execution code with it. The encoding is checked by disassembling a word and reassembling the text. Randomised execution is checked for architectural validity at every phase. And the replay property the contract would depend on is checked by running the same program twice.

The fifth exists because a machine that agrees with itself is not evidence. It compares the sequence of state commitments produced by two independently constructed machines running the same program with the same inputs, digit for digit.

No third party has audited anything. Every figure below is produced by code in this page: a full CHECK 01 sweep runs 1,048,576 vectors through the machine and compares each one against the gate level model.

VERIFICATION RUNNER0 PASS · 0 FAIL · 5 NOT RUN
CHECK 01
IDLE

THE ARITHMETIC

Every arithmetic, logic and shift instruction produces the same result and the same four flags as the same operation built out of the primitive.

METHOD
Deterministic vectors are driven through the machine one instruction at a time. The expected value is computed by the gate level model in gates.ts, which composes NAND cells into a ripple carry adder, a logic unit and a four stage barrel shifter.
A PASS DOES NOT ESTABLISH
A sampled sweep covers the operand space it visits. The full sweep is exhaustive over its own vector schedule, not over all 2³² operand pairs.
0VECTORS · OF 4,096

QUICK 4,096 · FULL 1,048,576 VECTORS

CHECK 02
IDLE

AN INDEPENDENT MODEL

A second interpreter, sharing no execution code with the machine, reaches identical architectural state after every retired instruction.

METHOD
Both models execute the reference programs and a set of generated programs. After each retirement the program counter, instruction register, stack pointer, register file, flags and the whole store are compared.
A PASS DOES NOT ESTABLISH
Agreement between two models is not a proof of correctness. It is a proof that a single mistake would have to occur twice, in two different implementations, in the same way.
0RETIREMENTS · OF 20,000

QUICK 20,000 · FULL 400,000 RETIREMENTS

CHECK 03
IDLE

THE SHIPPED PATH

The encoding is canonical and the text path is closed: an instruction word disassembles to text that reassembles to the identical word.

METHOD
Words are constructed across the opcode, destination, source and immediate fields, decoded, disassembled, and passed back through the assembler used by the editor. Reserved bits are checked to reject non canonical words.
A PASS DOES NOT ESTABLISH
This checks the representation, not the semantics. A closed encoding with a wrong opcode assignment would still pass.
0WORDS · OF 8,192

QUICK 8,192 · FULL 131,072 WORDS

CHECK 04
IDLE

LIVENESS

Randomised execution never reaches an undefined architectural state. It either runs, halts, or raises one of the declared faults.

METHOD
Generated programs are executed for a phase budget. Every phase is checked for register width, stack pointer range, program counter range, phase list validity and monotonic cycle count.
A PASS DOES NOT ESTABLISH
Randomised execution samples the state space. It does not enumerate it.
0PHASES · OF 60,000

QUICK 60,000 · FULL 1,200,000 PHASES

CHECK 05
IDLE

THE COMMITMENT

A machine replayed from its program and its inputs produces the identical sequence of state commitments. This is the property the contract requires.

METHOD
A machine is run and its per cycle commitments recorded. A second machine is constructed from the same program and driven with the same inputs, and the two commitment sequences are compared digit for digit.
A PASS DOES NOT ESTABLISH
No contract is deployed. This check verifies the replay property that an on-chain execution would depend on, on this machine, in this browser.
0COMMITMENTS · OF 8,000

QUICK 8,000 · FULL 120,000 COMMITMENTS

04.6 · THE REFERENCE MODEL
92 GATE EVALUATIONS PER INSTRUCTION

The expectation is
built from the
primitive.

A check is only as good as what it compares against. The expected value in CHECK 01 is not a second copy of the same arithmetic: it is computed by composing NAND cells into a ripple carry adder, a bitwise logic unit and a four stage barrel shifter, and then reading the result off the bits.

That model is slow — around 92 primitive evaluations for every instruction it retires — and that is the point. The machine’s fast path and the model’s slow path have almost nothing in common except the architecture they both claim to implement.

The carry and overflow flags are taken from the chain rather than from a formula: the carry out of bit fifteen, and that carry differing from the carry into bit fifteen. The machine computes the same two bits arithmetically. CHECK 01 is where those two definitions have to agree, on every vector.

WHAT EACH CHECK CANNOT SHOWSTATED, NOT OMITTED
  • CHECK 01THE ARITHMETICA sampled sweep covers the operand space it visits. The full sweep is exhaustive over its own vector schedule, not over all 2³² operand pairs.
  • CHECK 02AN INDEPENDENT MODELAgreement between two models is not a proof of correctness. It is a proof that a single mistake would have to occur twice, in two different implementations, in the same way.
  • CHECK 03THE SHIPPED PATHThis checks the representation, not the semantics. A closed encoding with a wrong opcode assignment would still pass.
  • CHECK 04LIVENESSRandomised execution samples the state space. It does not enumerate it.
  • CHECK 05THE COMMITMENTNo contract is deployed. This check verifies the replay property that an on-chain execution would depend on, on this machine, in this browser.