Spartan PIOP: R1CS reduction and Eq-shaped F2Z handoff

# S2 - Spartan PIOP: outer sumcheck, inner sumcheck, and F2Z handoff

Implement a Spartan-style R1CS PIOP over `F_q` that reduces relation
satisfaction to an Eq-shaped linear claim consumable by F2Z.

This issue owns:

1. Projection of the SHA relation into `F_q`.
2. The R1CS assignment, padding, and MLE layout.
3. Prover and verifier orchestration for the cubic outer sumcheck.
4. The terminal `Az/Bz/Cz` evaluations and fresh batching challenge.
5. Prover-side row binding and verifier-side sparse matrix-MLE evaluation.
6. Prover and verifier orchestration for the quadratic inner sumcheck.
7. Reduction of the inner terminal claim to `EqShapedVirtualClaim<Q>`.
8. Transcript binding, proof types, and positive and negative tests.

The completed protocol must reduce

```text
(AZ) ∘ (BZ) = CZ
```

to a verifier-derived claim

```text
kappa * H~(r_H) = target
```

that is subsequently authenticated by F2Z.

To avoid collision with the SHA relation's existing notation
`z = M_mix f`, this issue uses `Z` for the complete padded R1CS assignment
and `H` for the private binary oracle authenticated by F2Z.

The Spartan verifier is a reduction verifier. It MUST NOT report final
acceptance after the inner sumcheck. Overall acceptance requires successful
F2Z verification of the returned Eq-shaped claim.

## Source of truth

Use:

- the F2Z protocol specification from #2 for transcript and claim semantics
- the SHA-256 relation from #17
- Spartan2 as an algorithmic reference for the R1CS reduction
- the repository's shared polynomial, transcript, and sumcheck abstractions

The local F2Z specification is normative. Spartan2 is an implementation
reference; its field, PCS, transcript, assignment ordering, and MLE variable
ordering must not be copied without adapting them to this repository.

## Relation and field profile

The PIOP proves the R1CS relation

```text
(AZ) ∘ (BZ) = CZ
```

over the configured prime field

```text
F_q, q = 2^100 - 15.
```

For the initial SHA integration, lower each exact-integer linear row

```text
L(H) = 0
```

as the degenerate R1CS constraint

```text
L(H) * 1 = 0.
```

The generic outer sumcheck must accept individual degree at most three. The
linear SHA instance may degenerate to degree two and must not be rejected for
having degree below the maximum.

Projection of signed integer coefficients into `F_q` must be checked and must
preserve #17's no-modular-aliasing bound. Do not reinterpret signed
coefficients using unchecked integer casts.

Every coordinate ultimately authenticated by F2Z must be binary. Supporting
general R1CS witnesses containing arbitrary `F_q` values is out of scope unless
those values are explicitly bit-encoded and linked to the binary assignment.

## 1. Assignment layout and padding

Define one canonical layout for the R1CS assignment and its row and column
domains.

The layout must pin:

- fixed-one, public-input, and private-witness coordinate ordering
- live and padded row and column dimensions
- deterministic zero padding
- MLE variable and index-bit ordering
- multi-compression ordering

All R1CS matrices, prover tables, sparse verifier evaluations, and F2Z
reductions must use the same layout metadata. Bind that metadata into the
public statement and add golden tests for representative indices and padded
coordinates.

## 2. Spartan prover-verifier protocol

The Spartan PIOP consists of:

1. A degree-at-most-three outer sumcheck.
2. Three terminal MLE evaluations and a fresh batching challenge.
3. A degree-at-most-two inner sumcheck.
4. An Eq-shaped reduction to F2Z.

All verifier challenges are derived through Fiat-Shamir from the shared
transcript.

### 2.1 Outer sumcheck

Let the padded constraint-row domain have size `2^m_x`. The verifier samples

```text
tau <- F_q^m_x
```

from the transcript.

Define

```text
G(x) =
    eq(tau, x)
    (Az~(x) Bz~(x) - Cz~(x)).
```

For a satisfying assignment,

```text
sum_{x in {0,1}^m_x} G(x) = 0.
```

The prover and verifier run a degree-at-most-three sumcheck for this claim.

In each round:

1. The prover sends the current univariate round polynomial `g_i(X)`.
2. The verifier checks

   ```text
   g_i(0) + g_i(1) = current_claim.
   ```

3. The verifier absorbs the round message.
4. The verifier samples the next challenge `r_x[i]`.
5. Both parties update

   ```text
   current_claim = g_i(r_x[i]).
   ```

After `m_x` rounds, the protocol has a transcript-derived point `r_x` and
terminal value

```text
sigma_outer = G(r_x).
```

The prover then sends

```text
a = Az~(r_x)
b = Bz~(r_x)
c = Cz~(r_x).
```

The verifier checks

```text
sigma_outer
= eq(tau, r_x) (a b - c).
```

The values `(a, b, c)` are then absorbed into the transcript.

### 2.2 Batched MLE claim and row binding

After absorbing `(a, b, c)`, the verifier samples a fresh challenge

```text
rho <- F_q.
```

The parties derive

```text
v = a + rho b + rho^2 c.
```

For each assignment coordinate `y`, define

```text
D(y) =
    A~(r_x, y)
  + rho B~(r_x, y)
  + rho^2 C~(r_x, y).
```

The three terminal MLE claims are thereby reduced to the single claim

```text
v = sum_{y in {0,1}^m_y} D(y) Z[y].
```

The prover constructs the row-bound table

```text
D[j] =
    sum_i eq(i, r_x)
    (A[i,j] + rho B[i,j] + rho^2 C[i,j]).
```

This table is prover-local and is not included in the proof.

The verifier does not construct `D[j]` at this stage. It retains `r_x`,
`rho`, and `v`. After the inner sumcheck produces `r_y`, the verifier evaluates
`D~(r_y)` directly from the public sparse matrices.

The fresh `rho` must be sampled after all three values `(a, b, c)` have been
absorbed.

### 2.3 Inner sumcheck

The prover and verifier run a degree-at-most-two sumcheck for

```text
v = sum_{y in {0,1}^m_y} D(y) Z[y].
```

In each round:

1. The prover sends the quadratic round polynomial.
2. The verifier checks

   ```text
   g_i(0) + g_i(1) = current_claim.
   ```

3. The verifier absorbs the round message.
4. The verifier samples the next challenge `r_y[i]`.
5. Both parties update the running claim.

After `m_y` rounds, the protocol derives a point `r_y` and terminal value

```text
sigma_inner = D~(r_y) Z~(r_y).
```

The verifier evaluates the public sparse matrices at `(r_x, r_y)`:

```text
A_xy =
    sum_(i,j) A[i,j] eq(i, r_x) eq(j, r_y)

B_xy =
    sum_(i,j) B[i,j] eq(i, r_x) eq(j, r_y)

C_xy =
    sum_(i,j) C[i,j] eq(i, r_x) eq(j, r_y).
```

It then computes

```text
lambda =
    A_xy
  + rho B_xy
  + rho^2 C_xy.
```

By construction,

```text
D~(r_y) = lambda,
```

so the remaining terminal claim is

```text
sigma_inner = lambda Z~(r_y).
```

The matrix evaluations and `lambda` are verifier-derived. They are not prover
messages.

### 2.4 Assignment split and F2Z handoff

For the terminal reduction, interpret the canonical assignment as

```text
Z = H || P,
```

where `H` is the private binary oracle authenticated by F2Z and `P` is
verifier-known.

Split the inner point as

```text
r_y = (r_H, s)
```

according to the pinned MLE ordering. With contiguous halves under the
repository's little-endian convention, `s` is the high-bit selector and is
folded last.

Then

```text
Z~(r_H, s)
= (1 - s) H~(r_H) + s P~(r_H).
```

The verifier computes

```text
p_eval = P~(r_H)
```

and derives, without division,

```text
kappa = lambda (1 - s)

target =
    sigma_inner
  - lambda s p_eval.
```

This yields the Eq-shaped claim

```text
kappa H~(r_H) = target.
```

The claim is returned as

```rust
EqShapedVirtualClaim::new(
    MlePoint::new(r_H),
    kappa,
    target,
)
```

and subsequently verified by F2Z.

Do not divide by `lambda` or `1 - s`.

A zero `kappa` is not an automatic success. The resulting relation still
requires `target = 0`, which must be enforced by F2Z.

## 3. Verifier algorithm

### Inputs

The verifier receives:

- the public R1CS statement `(A, B, C)`
- public inputs and assignment-layout metadata
- the F2Z commitment
- the Spartan proof:

  ```text
  outer sumcheck proof
  (a, b, c)
  inner sumcheck proof
  ```

- the F2Z proof
- the shared transcript

The verifier does not receive:

- `tau`
- `r_x`
- `sigma_outer`
- `rho`
- `v`
- `r_y`
- `sigma_inner`
- either Eq table
- matrix evaluations
- `lambda`
- the final Eq-shaped claim

These values are all derived locally.

### Algorithm

1. Validate:

   - the field profile
   - R1CS matrix dimensions
   - CSR matrix structure
   - live and padded dimensions
   - assignment layout
   - public-input length
   - deterministic padding

2. Bind to the transcript:

   - protocol and wire version
   - field profile
   - R1CS matrix and shape digest
   - public input
   - dimensions and padding
   - assignment and MLE layout
   - virtual-map digest
   - F2Z parameters
   - F2Z commitment root

3. Sample

   ```text
   tau <- F_q^m_x.
   ```

4. Verify the degree-at-most-three outer sumcheck with initial claim zero,
   obtaining

   ```text
   (r_x, sigma_outer).
   ```

5. Read `(a, b, c)` from the proof and reject unless

   ```text
   sigma_outer
   = eq(tau, r_x) (a b - c).
   ```

6. Absorb `(a, b, c)` in canonical order and sample

   ```text
   rho <- F_q.
   ```

7. Derive

   ```text
   v = a + rho b + rho^2 c.
   ```

8. Verify the degree-at-most-two inner sumcheck with initial claim `v`,
   obtaining

   ```text
   (r_y, sigma_inner).
   ```

9. Construct

   ```text
   T_x = eq_table(r_x)
   T_y = eq_table(r_y).
   ```

10. Evaluate the public sparse matrices:

    ```text
    A_xy = A~(r_x, r_y)
    B_xy = B~(r_x, r_y)
    C_xy = C~(r_x, r_y).
    ```

11. Compute

    ```text
    lambda =
        A_xy
      + rho B_xy
      + rho^2 C_xy.
    ```

12. Split `r_y = (r_H, s)` according to the pinned assignment and MLE
    ordering.

13. Compute

    ```text
    p_eval = P~(r_H)

    kappa = lambda (1 - s)

    target =
        sigma_inner
      - lambda s p_eval.
    ```

14. Construct

    ```text
    claim =
        EqShapedVirtualClaim(r_H, kappa, target).
    ```

15. Bind the Spartan-to-F2Z handoff:

    - protocol and handoff version
    - `r_H`
    - `kappa`
    - `target`

16. Invoke the F2Z verifier on `claim`.

17. Accept if and only if:

    - both sumchecks verified
    - the outer terminal identity verified
    - all statement and layout checks passed
    - F2Z verified the derived Eq-shaped claim

    Otherwise reject.

### Shared sumcheck verification requirements

For both sumchecks, the verifier must:

- require exactly the statement-derived number of rounds
- reject missing and trailing rounds
- enforce individual degree at most the declared bound
- reconstruct omitted coefficients according to the shared proof encoding
- check `g_i(0) + g_i(1) = current_claim`
- absorb the canonical round message before sampling its challenge
- derive every challenge from the transcript
- reject malformed or non-canonical field encodings
- use distinct outer and inner transcript domains

If the proof encodes each round as

```text
[c_0, c_2, ..., c_D],
```

the verifier reconstructs

```text
c_1 =
    current_claim
  - 2 c_0
  - sum_{j=2}^D c_j.
```

This guarantees

```text
g_i(0) + g_i(1) = current_claim.
```

### Sparse matrix-MLE evaluation

Given

```text
T_x[i] = eq(i, r_x)
T_y[j] = eq(j, r_y),
```

evaluate each sparse matrix as

```text
M_xy =
    sum_(i,j,M_ij != 0)
    T_x[i] M_ij T_y[j].
```

Expose the equivalent of:

```rust
fn evaluate_abc_mles<const Q: u128>(
    relation: &R1csRelation<Fq<Q>>,
    row_weights: &[Fq<Q>],
    column_weights: &[Fq<Q>],
) -> Result<MatrixEvals<Fq<Q>>, SpartanError>;
```

The correctness-first implementation may evaluate `A`, `B`, and `C`
separately. The optimized implementation should fuse the three CSR traversals
to reuse row and column weights.

Verifier work must be linear in

```text
nnz(A) + nnz(B) + nnz(C)
```

plus construction of the two Eq tables. Production code must not materialize
a dense bivariate matrix MLE.

## 4. Proof and API shape

The Spartan proof should contain only prover messages:

```rust
pub struct SpartanR1csProof<const Q: u128> {
    pub outer: SumcheckProof<Fq<Q>, 3>,
    pub outer_evaluations: OuterEvaluations<Fq<Q>>,
    pub inner: SumcheckProof<Fq<Q>, 2>,
}

pub struct OuterEvaluations<F> {
    pub az: F,
    pub bz: F,
    pub cz: F,
}
```

Challenges, running claims, terminal points, matrix evaluations, and the
Eq-shaped claim must not be independently serialized.

Expose a reduction API equivalent to:

```rust
fn prove<const Q: u128>(
    statement: &SpartanR1csStatement<Q>,
    witness: &SpartanR1csWitness<Q>,
    transcript: &mut impl F2zTranscript<Q>,
) -> Result<(SpartanR1csProof<Q>, EqShapedVirtualClaim<Q>), SpartanError>;

fn verify<const Q: u128>(
    statement: &SpartanR1csStatement<Q>,
    proof: &SpartanR1csProof<Q>,
    transcript: &mut impl F2zTranscript<Q>,
) -> Result<EqShapedVirtualClaim<Q>, SpartanError>;
```

The composed proof should have the equivalent shape:

```rust
pub struct R1csF2zProof<const Q: u128> {
    pub spartan: SpartanR1csProof<Q>,
    pub f2z: F2zOpeningProof<Q>,
}
```

The top-level verifier performs:

```text
claim = SpartanR1csReduction::verify(...)
F2z::verify_eq(commitment, virtual_map, claim, ...)
```

and accepts only if both calls succeed.

Use a return type or naming convention that makes it impossible to mistake
successful Spartan reduction for final proof acceptance.

## 5. Transcript order and statement binding

Pin the following transcript order:

1. Domain separator and protocol version.
2. Field and R1CS profile.
3. R1CS matrix and shape digest.
4. Public input.
5. Assignment and padding metadata.
6. Virtual-map digest.
7. F2Z parameters and commitment root.
8. Outer point `tau`.
9. Outer sumcheck rounds.
10. Outer evaluations `(a, b, c)`.
11. Batching challenge `rho`.
12. Inner sumcheck rounds.
13. Spartan-to-F2Z handoff.
14. F2Z proof.

Add an audit mode or golden transcript test recording every absorb and squeeze.
Prover and verifier logs must match byte for byte.

## 6. Expected prover and verifier cost

For padded row dimension `2^m_x` and assignment dimension `2^m_y`, the
Spartan verifier performs:

```text
m_x degree-3 sumcheck rounds
m_y degree-2 sumcheck rounds
two Eq-table constructions
one fused sparse evaluation of A, B, and C
one public-table MLE evaluation
one Eq-shaped reduction
one F2Z verification
```

The issue must document the concrete SHA profile after the assignment layout
is frozen, including:

- live and padded row counts
- live and padded assignment lengths
- outer and inner round counts
- combined matrix nonzero count
- Spartan proof field-element count
- verifier sparse-evaluation cost
- F2Z handoff dimension

## Out of scope

- SHA witness synthesis and `M_mix/A_x` construction from #17
- rewriting SHA as a conventional nonlinear R1CS circuit
- arbitrary non-binary R1CS witness elements
- dense production matrix representations
- matrix commitments for sublinear verifier time
- zero-knowledge masking of the two sumchecks
- downstream F2Z bounded lifting
- product arguments and merged GKR
- characteristic-two adjoint
- ring switching
- Flock/Ligerito implementation
- a new optimized F2Z wire version that skips the v1 input-shaping sumcheck

The optimized native Eq-shaped F2Z wire profile should be tracked separately.
This issue owns the stable Eq-shaped reduction boundary.

## Validation

Done when all of the following hold:

- Tiny hand-built satisfiable R1CS instances prove and verify.
- Unsatisfied R1CS instances are rejected.
- The SHA linear relation is correctly lowered to degenerate R1CS.
- Signed coefficients project into `F_q` without modular aliasing.
- Outer verification rejects incorrect round counts and degrees.
- Outer verification rejects mutations to `a`, `b`, or `c`.
- The batching challenge is sampled only after `(a, b, c)` are absorbed.
- Inner verification rejects incorrect round counts and degrees.
- Sparse `A/B/C` evaluations match an independent dense reference.
- Fused and separate matrix evaluators return identical values.
- The verifier never consumes a prover-supplied matrix evaluation.
- The derived `lambda` matches direct evaluation of the row-bound `D` table.
- The final Eq-shaped claim matches direct witness-MLE evaluation.
- Edge tests cover `lambda = 0`, `kappa = 0`, and selector values zero and one.
- A zero-scale claim with nonzero target is rejected.
- Mutating the public table changes or invalidates the handoff claim.
- Mutating the R1CS digest, layout, padding, public input, commitment root, or
  virtual map causes rejection.
- Golden tests pin assignment order and MLE variable order.
- Golden transcript tests pin every absorb and squeeze.
- The composed verifier cannot accept without successful F2Z verification.
- Production code does not allocate a dense bivariate matrix MLE.
- The workspace passes:

  ```text
  cargo test --workspace --all-features
  cargo clippy --workspace --all-targets --all-features -- -D warnings
  cargo fmt --all --check
  ```

## Dependencies

- #17 for the executable SHA relation and shape metadata.
- #2 for the normative F2Z statement and transcript semantics.
- #3 for the transcript layer.
- #4 for MLE and Eq-table support.
- #5 for the shared sumcheck verifier and commitment integration.
- #7 for the shared sumcheck prover.

Effort L.


Navigation Menu

Spartan PIOP: R1CS reduction and Eq-shaped F2Z handoff #19

S2 - Spartan PIOP: outer sumcheck, inner sumcheck, and F2Z handoff

Source of truth

Relation and field profile

1. Assignment layout and padding

2. Spartan prover-verifier protocol

2.1 Outer sumcheck

2.2 Batched MLE claim and row binding

2.3 Inner sumcheck

2.4 Assignment split and F2Z handoff

3. Verifier algorithm

Inputs

Algorithm

Shared sumcheck verification requirements

Sparse matrix-MLE evaluation

4. Proof and API shape

5. Transcript order and statement binding

6. Expected prover and verifier cost

Out of scope

Validation

Dependencies

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Spartan PIOP: R1CS reduction and Eq-shaped F2Z handoff #19

Description

S2 - Spartan PIOP: outer sumcheck, inner sumcheck, and F2Z handoff

Source of truth

Relation and field profile

1. Assignment layout and padding

2. Spartan prover-verifier protocol

2.1 Outer sumcheck

2.2 Batched MLE claim and row binding

2.3 Inner sumcheck

2.4 Assignment split and F2Z handoff

3. Verifier algorithm

Inputs

Algorithm

Shared sumcheck verification requirements

Sparse matrix-MLE evaluation

4. Proof and API shape

5. Transcript order and statement binding

6. Expected prover and verifier cost

Out of scope

Validation

Dependencies

Activity

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions