# Soundness Map

> Every claim a verified proof makes, the argument that carries it, and the exact specification sections where that argument is stated and justified.

A verified block establishes one sentence: *the program of this identity, started at its entry pc over its image, with this public input and some advice, executes instruction by instruction to `EXIT` with this status, having written this journal.* This page breaks that sentence into the claims it is made of and carries each one to the argument that proves it.

## The program

| Claim | Argument | Specification |
| --- | --- | --- |
| The key describes the registered program | loading a key recomputes the identity from its own config, entry pc and setup commitments; the verifier compares it with its own copy | [proof §7.2](https://apogee.gweb3networks.com/docs/auditors/spec/proof#s7-2), [program §8](https://apogee.gweb3networks.com/docs/auditors/spec/program#s8) |
| The tables a proof reads are the ones the identity commits | every shard's batched opening takes its setup commitments from the key | [proof §5](https://apogee.gweb3networks.com/docs/auditors/spec/proof#s5) |
| Each executed row is the program's instruction at its pc | the decoder lookup, keyed by the row's own pc read, into a table whose live rows are one-hot and whose padding rows are `−1` | [lookup §10](https://apogee.gweb3networks.com/docs/auditors/spec/lookup#s10), [program §5](https://apogee.gweb3networks.com/docs/auditors/spec/program#s5), [§6](https://apogee.gweb3networks.com/docs/auditors/spec/program#s6) |
| Memory starts from the program's image | `INIT_TEARDOWN`'s init column is a setup column the identity commits; no file-backed byte lies outside window 0 | [memory §6.2](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s6-2), [§3.4](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s3-4) |
| Execution starts at the entry pc | the pc's initial tuple uses the key's entry pc, which the identity binds | [memory §4.2](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s4-2), [§6.2](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s6-2) |
| The circuits are the right ones | a key's circuits must equal the verifier's registry at its heights and pass the laws, the memory rules and the discharge rule | [proof §7.2](https://apogee.gweb3networks.com/docs/auditors/spec/proof#s7-2), [circuits §1](https://apogee.gweb3networks.com/docs/auditors/spec/circuits#s1), [gkr §4.2](https://apogee.gweb3networks.com/docs/auditors/spec/gkr#s4-2) |

## Each row

| Claim | Argument | Specification |
| --- | --- | --- |
| A row obeys its instruction | the family's enforcing gates, zero on every row, each family's soundness argument | [add-sub §4](https://apogee.gweb3networks.com/docs/auditors/spec/add-sub#s4), [jump-branch-slt §5](https://apogee.gweb3networks.com/docs/auditors/spec/jump-branch-slt#s5), [shift-bitwise §5](https://apogee.gweb3networks.com/docs/auditors/spec/shift-bitwise#s5), [mul-div §5](https://apogee.gweb3networks.com/docs/auditors/spec/mul-div#s5), [memory-ops §3–§6](https://apogee.gweb3networks.com/docs/auditors/spec/memory-ops#s3) |
| A row makes exactly its instruction's queries | each mask pinned to `m_pc` times the kinds that make that query | [memory §2.1](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s2-1) |
| `x0` reads and writes 0 | the x0 gadget and write-backs | [memory §2.4](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s2-4) |
| Register and RAM values are words | every register write bounded on its own row; every RAM write of an execution family a word; initial values words except advice, which no family relies on | [memory-ops §5](https://apogee.gweb3networks.com/docs/auditors/spec/memory-ops#s5) |
| A padding row adds no memory event | every mask of a padding row is 0, so its leaves are 1 | [memory §2.3](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s2-3), [gkr §4.3](https://apogee.gweb3networks.com/docs/auditors/spec/gkr#s4-3) |

## Memory and order

| Claim | Argument | Specification |
| --- | --- | --- |
| Every read returns the last write | one read/write multiset over every shard, reconciled once against the register and pc boundary | [memory §4](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s4), [§9](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s9) |
| A read strictly follows the write it consumes | each query's timestamp gap is two 19-bit `TIMESTAMP` chunks | [memory §2.4](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s2-4), [§7](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s7) |
| Every address has exactly one initial value | the window rules: one height, disjoint windows, one shard each of the fixed windows | [memory §3.5](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s3-5), [§9](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s9) |
| The multiset cannot close by a loop | timestamps are integers on bounded paths: a loop would need more than `2^215` edges | [memory §4.2](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s4-2) |
| The rows form one path from the entry to the exit, in program order | the pc is a memory cell written at least four timestamps after it is read | [memory §5](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s5), [§9](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s9) |
| The execution ends at the exit row | `HALT_PC = 1` is odd; only the exit row writes it; `JUMP_BRANCH_SLT` range-checks its `next_pc` even | [memory §5](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s5), [jump-branch-slt §5](https://apogee.gweb3networks.com/docs/auditors/spec/jump-branch-slt#s5), [add-sub §4](https://apogee.gweb3networks.com/docs/auditors/spec/add-sub#s4) |
| A shard's time window adds nothing | time windows are checked for shape only; order comes from the multiset alone | [proof §8](https://apogee.gweb3networks.com/docs/auditors/spec/proof#s8) |

## Values and lookups

| Claim | Argument | Specification |
| --- | --- | --- |
| Every gated tuple is a row of its table | one LogUp identity per channel, summed by a fraction tree in the GKR pass; root numerator 0 and denominator nonzero | [lookup §1](https://apogee.gweb3networks.com/docs/auditors/spec/lookup#s1), [§6](https://apogee.gweb3networks.com/docs/auditors/spec/lookup#s6), [§8](https://apogee.gweb3networks.com/docs/auditors/spec/lookup#s8) |
| Selectors are boolean | every lookup's selector is held to `s − s²` by an enforcing gate of list 0 | [lookup §2](https://apogee.gweb3networks.com/docs/auditors/spec/lookup#s2) |
| A lookup answers from its own sub-table | one width per channel, disjoint key ranges with the `+1` offset, and each family's bound on its key | [lookup §4](https://apogee.gweb3networks.com/docs/auditors/spec/lookup#s4), [§9](https://apogee.gweb3networks.com/docs/auditors/spec/lookup#s9), [§11](https://apogee.gweb3networks.com/docs/auditors/spec/lookup#s11) |
| The tables are the intended ones | virtual tables are the verifier's closed forms; the generic table is bound by the SRS digest; decoded tables by the identity | [lookup §3](https://apogee.gweb3networks.com/docs/auditors/spec/lookup#s3), [§12](https://apogee.gweb3networks.com/docs/auditors/spec/lookup#s12) |
| Every declared obligation is discharged | the discharge rule at assembly and at every key load | [lookup §11](https://apogee.gweb3networks.com/docs/auditors/spec/lookup#s11) |

## Public values

| Claim | Argument | Specification |
| --- | --- | --- |
| The input window held the statement's input | `PUBLIC_INPUT`'s initial column equals the input's words at a random point, after G7 fixes the bytes | [public values §5](https://apogee.gweb3networks.com/docs/auditors/spec/public-values#s5) |
| The journal is what the guest's stores left | `PUBLIC_OUTPUT`'s final column equals the journal's words; the window has no initial column a prover could fill | [public values §5](https://apogee.gweb3networks.com/docs/auditors/spec/public-values#s5) |
| The exit status is `x10`'s final value | the exit row writes back the `a0` it read; the verifier holds `v_10` to the statement's status | [add-sub §4](https://apogee.gweb3networks.com/docs/auditors/spec/add-sub#s4), [memory §4.1](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s4-1), [proof §6](https://apogee.gweb3networks.com/docs/auditors/spec/proof#s6) |

## Delegations

| Claim | Argument | Specification |
| --- | --- | --- |
| Each request is executed exactly once | the anchor: requests and invocations pair one to one through the multiset in the type's own space | [delegation §5](https://apogee.gweb3networks.com/docs/auditors/spec/delegation#s5) |
| An invocation computes its function | each circuit's soundness argument, frame and canonicity chains included | [delegation circuits §2–§7](https://apogee.gweb3networks.com/docs/auditors/spec/delegation-circuits#s2) |
| A multi-call operation is the composition of its steps | RAM glue: each step reads the previous step's writes on one memory history; the order is the calling code's | [delegation circuits §1](https://apogee.gweb3networks.com/docs/auditors/spec/delegation-circuits#s1) |

## The proof system

| Claim | Argument | Specification |
| --- | --- | --- |
| A shard's outputs are its circuit evaluated on its committed columns | the GKR backward pass, each challenge drawn after what it protects | [gkr §5.4](https://apogee.gweb3networks.com/docs/auditors/spec/gkr#s5-4) |
| The claimed column values are the committed polynomials' | one batched Mercury opening at the pass's point | [mercury §5](https://apogee.gweb3networks.com/docs/auditors/spec/mercury#s5), [§7](https://apogee.gweb3networks.com/docs/auditors/spec/mercury#s7) |
| A statement is verified only by all of its shards | shard-set exactness at decode and in `verify_block`; the reconciliation reads every shard's roots | [proof §1.3](https://apogee.gweb3networks.com/docs/auditors/spec/proof#s1-3), [§6](https://apogee.gweb3networks.com/docs/auditors/spec/proof#s6) |
| Challenges follow every commitment they protect | the global transcript G1–G11 and the shard transcript S1–S6 | [proof §2](https://apogee.gweb3networks.com/docs/auditors/spec/proof#s2), [§4](https://apogee.gweb3networks.com/docs/auditors/spec/proof#s4), [transcript §3](https://apogee.gweb3networks.com/docs/auditors/spec/transcript#s3) |
| The setup is the ceremony's | the SRS digest, compared by the verifier with the ceremony's | [proof §3](https://apogee.gweb3networks.com/docs/auditors/spec/proof#s3), [srs §3](https://apogee.gweb3networks.com/docs/auditors/spec/srs#s3) |

## Recursion and the contract

| Claim | Argument | Specification |
| --- | --- | --- |
| A node ran exactly the base verifier's checks | the checks are compiled into tapes in the node program's image, which its identity binds | [recursion §7](https://apogee.gweb3networks.com/docs/auditors/spec/recursion#s7), [§8.1](https://apogee.gweb3networks.com/docs/auditors/spec/recursion#s8-1) |
| The tree covers one base statement, every shard, in order | the transcript chain across nodes, adjacent shard ranges, and each node's checks on its children | [recursion §8.1](https://apogee.gweb3networks.com/docs/auditors/spec/recursion#s8-1), [§8.2](https://apogee.gweb3networks.com/docs/auditors/spec/recursion#s8-2) |
| Every deferred opening holds | each folded under weights drawn after everything it weights, discharged by one pairing in the contract | [recursion §8.3](https://apogee.gweb3networks.com/docs/auditors/spec/recursion#s8-3), [mercury §6](https://apogee.gweb3networks.com/docs/auditors/spec/mercury#s6) |
| The decider binds what the contract holds | bound wires committed before their challenge; the circuit holds the journal to the whole base range | [recursion §9](https://apogee.gweb3networks.com/docs/auditors/spec/recursion#s9) |
| The decider key has no known trapdoor | a two-phase ceremony with one honest contributor per round, rounds in order | [recursion §9](https://apogee.gweb3networks.com/docs/auditors/spec/recursion#s9), [srs §7](https://apogee.gweb3networks.com/docs/auditors/spec/srs#s7) |

## Deliberately not claimed

- **Anything about advice.** Advice is bound to nothing by design; a guest checks it.
- **Zero knowledge.** Nothing is blinded.
- **`sc.w` failure semantics.** `sc.w` always succeeds; a program relying on its failure is outside the claim.
- **Traps.** A run that traps has no proof at all.
- **That the prover is correct.** The prover is untrusted; only the verifier's crates carry soundness.
- **That a ceremony file is the ceremony's**, or that a key's `τ` is unknown, without the verifier's own comparison of the SRS digest.