# Verifying the Implementation

> How the code is checked against something other than itself. Each layer's independent oracle, the second implementation of the circuit rules, the tamper twins that prove forgeries are refused, and what no check covers.

No component of Apogee is checked against a second implementation of the whole system. Instead each layer has an oracle of its own, chosen so that the check shares as little code as possible with what it checks.

## Each layer and its oracle

| Layer | Checked against |
| --- | --- |
| Fields, curve, pairing, MSM | known-answer vectors generated from arkworks, which the tests also run live; the tests re-derive every arithmetic constant the crates read |
| Poseidon2 and the transcript | `tools/transcript-ref`: Plonky3's Poseidon2 keyed with zkhash's round constants, and a transcription of the specification run beside Plonky3's duplex challenger, agreeing on every squeeze |
| The decoder | all `2^30` 32-bit words with low bits `11`, against accepted counts derived from the ISA's tables and against an independent encoder; `llvm-objdump` over the committed guests |
| RVC expansion | LLVM's own encoder, over a guest assembled both compressed and not |
| Circuits as data | `checker`: the four laws, the lookup rules and the padding contract re-implemented without `constraints`' code, sharing only the gate kernel |
| Each family's gates | row suites that build rows with Rust's own integer arithmetic and evaluate them through the checker; the arithmetic cores exhaustively at reduced word widths |
| The memory and lookup arguments | native evaluators in `checker`, run over executed traces |
| The executor | its own trace's self-check and the arguments above; there is no second executor |
| The revm guest | native revm, built from unpatched upstream crates |
| The stateless validator | a committed subset of `tests-zkevm` v21.0.1 natively in CI; the whole release natively and the subset through the guest binary by hand; `tools/stateless-ref` for the input encoding |
| The decider | the proof checked natively, and the contract executed in revm |

## Exhaustive checks at small widths

Several arithmetic cores are written with their word width as a parameter, so that the encoding can be checked over every input at a width small enough to enumerate:

- the comparison gadget at 6 bits, over every operand pair, signed and unsigned, finding exactly one `(lt, gap)`, the ISA's;
- `MUL_DIV`'s arithmetic at 4 bits, over every dividend and divisor and each division kind, admitting exactly one `(q, r)`, RV32M's;
- `MEM_SUBWORD`'s splice at a 4-bit word, admitting exactly one `(high, sub, low)` for every word, offset and width.

## The circuit rules, twice

`CircuitArtifact::validate` and the memory and lookup construction rules run wherever an artifact is built or a key is loaded. `crates/checker` enforces the same rules a second time with code of its own, never calling `validate`, and evaluates gates only through `gkr_verify::eval_gate`, the one kernel both sides treat as the semantic authority. Its validators check the laws by evaluation at sampled points where `validate` compares normalized expansions, recompute every channel's sum row by row rather than by a tree and name any tuple no table row holds, and rebuild an execution family's memory columns from the event log rather than from a shard's rows.

```sh
cargo run -p checker -- laws <artifact>       # Laws 1–4, then the lookup rules
cargo run -p checker -- padding <artifact>    # the padding contract
cargo run -p checker -- dump <artifact>       # the circuit, readably
```

## Tamper twins

A **tamper twin** is a forgery proved exactly as an honest prover would prove it. The tamper suite (`checker::TamperHarness`) re-proves a statement with witness cells or boundary scalars changed: each channel's multiplicities recounted, changed memory columns recommitted in a fresh global commit phase, every shard re-proved. Then it verifies a shard or the block and asserts the refusal's class, `Constraint`, `Lookup` with its channel, or `MemoryArgument`, or asserts that a change breaking nothing verifies.

The twins rely on the prover checking nothing, which is the design: a forged witness gets the best proof an honest prover could make of it, and the verifier must refuse it in the expected class. The suite also carries the delegation anchor's forgeries, and on the mainnet mini-block it shows the other side of the advice rule: a corrupted advice cell is refused by the memory argument, and a consistently corrupted one verifies, because advice is bound to nothing.

```sh
cargo test --release -p checker --test tamper -- --include-ignored --test-threads=1
```

## Fixtures that regenerate

`kat-gen` writes every committed known-answer vector, listing, circuit artifact and identity, each with its SHA-256, which the tests reading it pin. CI regenerates the default groups and both reference oracles and fails on any difference in the vector directories:

```sh
cargo run -p kat-gen && git diff --exit-code
```

A guest ELF is not reproducible across machines, because rustc embeds absolute paths in panic-location strings; two clean builds on one machine agree. So the guest ELFs are regenerated by hand on one machine, and CI regenerates only what derives from them.

## What no check covers

- **There is no second executor.** The emulator is held to a restatement of its own frame table and to the memory and lookup arguments, not to an independent RISC-V implementation, and no executor here takes a delegation shim's software fallback.
- **The construction rules the checker does not repeat**: the memory construction rules, the copower rule, and `validate`'s remaining construction rules, the degree ceiling among them, are enforced once.
- **The prover is not checked for correctness**, only for completeness through the suites that prove real shards, which run outside CI because each needs tens of GiB.
- **Osaka-family stateless inputs have no end-to-end oracle.** The release fills only Amsterdam; the Electra/Fulu layout is held to `eth-act/ere-guests` and the header rules to two mainnet blocks.
