soundness-review-checklist

# Soundness Review Checklist ## Canonical Theory Sources - `.agents/papers/llm/INDEX.llm.md` — first stop to map concepts and notation - `.agents/papers/llm/Circle_STARKs.llm.md` — circle-FFT/FRI/AIR math anchors - `.agents/papers/llm/Stwo_Whitepaper.llm.md` — STWO protocol/soundness/parameter anchors ## When to Run Run this checklist for ANY change touching: - `crates/stwo/src/core/fri.rs` or `crates/stwo/src/prover/fri.rs` - `crates/stwo/src/core/verifier.rs` - `crates/stwo/src/core/pcs/` - `crates/stwo/src/core/fields/` - `crates/stwo/src/core/constraints.rs` - `crates/stwo/src/core/channel/` - `crates/stwo/src/core/proof.rs` - `crates/stwo/src/prover/mod.rs` (prove functions) - `crates/constraint-framework/src/logup.rs` - Any file tagged [SOUNDNESS-CRITICAL] ## Pre-Review: Context Loading - [ ] Read the divergence log: `.claude/skills/paper-implementation-divergence-log.md` - [ ] Identify which distilled-file anchor governs the modified code - [ ] Load the relevant mathematical skill (circle-stark-mathematics, finite-field-arithmetic, etc.) ## 1. Mathematical Correctness - [ ] **Invariant identification**: What mathematical invariant does this code maintain? State it explicitly. - [ ] **Theory grounding**: Can the modified logic be traced to a specific definition, theorem, or algorithm in `Circle_STARKs.llm.md` or `Stwo_Whitepaper.llm.md`? - [ ] **Divergence check**: Does this change introduce a new paper-implementation divergence? If yes, document in the divergence log before proceeding. ## 2. Constraint System Integrity - [ ] **No constraint removal**: No constraint has been removed or weakened - [ ] **Degree preservation**: Constraint degree bounds are unchanged or correctly updated - [ ] **LogUp balance**: If logup interactions are modified, verify they still balance - [ ] **Completeness**: Valid witnesses still satisfy all constraints - [ ] **Soundness**: Invalid witnesses are still rejected (no new under-constraint) ## 3. FRI Protocol Correctness - [ ] **Folding chain**: FRI folding operations are mathematically correct (challenge mixing, domain halving, polynomial splitting) - [ ] **Layer verification**: All FRI layers are verified (none skipped) - [ ] **Last layer check**: Last layer polynomial degree bound is enforced - [ ] **Query consistency**: Query positions are consistently mapped across layers - [ ] **Domain chain**: Each folded domain is correctly derived from the previous one ## 4. Fiat-Shamir Transcript - [ ] **Ordering preserved**: Commitments are mixed BEFORE challenges are drawn - [ ] **No reordering**: The sequence of mix/draw operations is identical in prover and verifier - [ ] **Complete binding**: All proof elements are mixed into the transcript (no unbound values that an adversary could vary) - [ ] **Channel state**: Channel state is deterministic given the same inputs ## 5. Field Arithmetic - [ ] **Reduction correctness**: All arithmetic results are properly reduced - [ ] **No overflow**: Intermediate computations do not overflow their integer types - [ ] **Extension field**: Extension field operations use correct irreducible polynomials - [ ] **SIMD parity**: SIMD implementations match scalar reference behavior ## 6. Verifier Completeness - [ ] **All checks present**: The verifier performs ALL required verification steps - [ ] **Error propagation**: Verification failures are properly propagated (not swallowed) - [ ] **OODS evaluation**: Composition polynomial OODS eval is correctly extracted - [ ] **Proof of work**: PoW nonce is verified - [ ] **Merkle verification**: Decommitments are verified against commitments ## 7. Security Parameters - [ ] **No parameter weakening**: log_blowup_factor, n_queries, pow_bits are not reduced - [ ] **Parameter validation**: FriConfig::new() range checks are preserved - [ ] **Security bits**: Total security_bits() >= target (document what target is) ## 8. Test Coverage - [ ] **Existing tests pass**: All tests in the modified module still pass - [ ] **New test for change**: A test specifically exercises the modified behavior - [ ] **Negative tests**: There are tests that verify rejection of invalid inputs - [ ] **Edge cases**: Boundary conditions are tested (zero, maximum, single-element) ## 9. Unsafe Code (if applicable) - [ ] **Justified**: The unsafe block has a documented safety argument - [ ] **Minimal scope**: The unsafe block is as small as possible - [ ] **Invariant preserved**: The unsafe code does not violate any field/type invariants - [ ] **No UB**: There is no undefined behavior under any valid input ## Post-Review Actions - [ ] Update divergence log if new divergence found - [ ] Flag any coverage gaps found during review - [ ] If confidence < 90%: ESCALATE with SOUNDNESS-ESCALATION tag ## Escalation Protocol If ANY of the following are true, escalate to human review: 1. The change modifies a mathematical identity and you cannot prove equivalence 2. The change affects security parameters 3. You find an undocumented divergence from the distilled references 4. A soundness-critical component has zero test coverage for the modified path 5. The change introduces or modifies `unsafe` code in a soundness-critical file 6. You are not confident the change preserves all invariants listed above **Format**: ``` SOUNDNESS-ESCALATION: File: [path] Change: [description] Invariant at risk: [which invariant] Paper reference: [Circle_STARKs.llm.md anchor / Stwo_Whitepaper.llm.md anchor] Confidence: [percentage] Reason for escalation: [why] ```