# Security Model

> What a proof establishes, what it assumes, what a verifier must hold for itself, which code soundness rests on, and the limits of version 1.0.0.

## What a proof establishes

A proof that verifies establishes that the program of a given identity, started at its entry pc over its image, with the public input in its input window and some advice of the prover's choosing, executes instruction by instruction to `EXIT` with a given status, having written a given journal. Nothing is claimed of the advice. Nothing is hidden.

## Assumptions

| Assumption | Where it enters |
| --- | --- |
| Knowledge soundness of Mercury and KZG in the algebraic group model under q-DLOG | every commitment opening |
| Poseidon2 as a random oracle for Fiat–Shamir | every challenge, in the base proof and in recursion |
| Groth16's own assumptions | the decider, the last step to the contract |
| One honest contributor to the PSE perpetual powers of tau | the SRS every commitment is under |
| One honest contributor per round of the decider's phase-2 ceremony | the decider's key |

BN254 gives about 100 bits of security. The statistical error of every protocol layer, from the sumchecks and the batched opening to the memory and lookup arguments, is far below that: under `2^14/|Fr|` for a circuit's whole GKR pass, below `2^−190` for every lookup channel, below `2^−220` for every Mercury instance.

## What a verifier must hold for itself

Two values, from a channel the prover does not control:

- **The program identity.** Against a prover-supplied identity a proof shows only that some program ran.
- **The ceremony's SRS digest.** A key loads under whatever digest its own points give, so a key built over a known `τ` is refused only by this comparison.

The verifying key itself may come from anyone. Loading it recomputes the identity and the SRS digest from its own contents and holds its circuits to the verifier's registry: the identity binds the program, the registry binds the circuits. The `verifier` command-line tool compares the identity only, taking the SRS digest from the key; `host::verify` compares neither, and leaves its caller to check the statement's input, journal and exit status too.

## Trusted code

Soundness is the verifier's alone. It rests on `constants`, `field`, `curve`, `transcript`, `poly`, `sumcheck`, `pcs-verify`, `pcs`, `gkr-verify`, `verifier-core`, `verifier`, and `constraints`, because the circuits are part of the statement and a missing gate is a soundness bug. Computing an identity from an ELF also trusts `loader`, `isa` and `program`. The last step to the chain adds the recursion programs, `groth16`, the decider's circuit and the contract.

The prover, the emulator, the trace builders and the proving half of the host SDK are **untrusted**. The prover validates nothing; a wrong input costs an honest prover a proof that fails, and a cheating prover runs none of this code anyway.

## Not constant-time, not zero-knowledge

Nothing in the code is constant-time: reductions, exponentiations, point additions and scalar ladders branch on their operands. That is harmless here because no proof is zero-knowledge, so proving keeps nothing secret. The one secret the code handles is a decider ceremony contributor's factor, which goes through the same variable-time ladder; run contributions on a machine you control.

## Limits of v1.0.0

| Limit | Detail |
| --- | --- |
| Not zero-knowledge | no blinding in Mercury, GKR or the decider |
| Advice is unbound | a guest checks it against something a proof binds |
| Public values | at most 16,380 bytes each of input and journal |
| `sc.w` always succeeds | the one deviation from RV32IMAC's semantics; there is no reservation state |
| Traps are not provable | a misaligned access, an access outside mapped memory, `ebreak`, or a pc with no instruction ends an execution with no proof |
| Code is static | the instruction stream is the image decoded at load; one undecodable word in executable code refuses the program |
| Code size | `.text` within a decoded table's reach, 7.94 MiB at `2^22`; the image within 4 MiB by default |
| Execution length | `2^36 − 1` cycles |
| Delegations are a fixed set | six in the base format; a delegation proves one step of its function, and composing steps, validating curve points among them, is the calling code's |
| Prover memory | set by the shards in flight: the measured block peaked at 174 GiB |
| Block witnesses | the stateless validator takes its input from an external witness producer |
| The decider's key | one per root shape, and only as trustworthy as its ceremony; the development key is forgeable |
| On-chain cost | about 3.6M gas for the measured block |

## Where the next version moves this

Every assumption above that involves BN254, from q-DLOG and the pairing to Groth16, falls to a large enough quantum computer. The [v2.0.0 trajectory](https://apogee.gweb3networks.com/docs/quantum-leap) is a proving core whose soundness rests on lattice problems instead.

For an auditor's view of the same model, crate by crate and argument by argument: [Audit guide](https://apogee.gweb3networks.com/docs/auditors), [Soundness map](https://apogee.gweb3networks.com/docs/auditors/soundness-map).