zorch.spartan

Separately deployable Spartan roles and their shared R1CS data model.

R1CS dataclass

A dense R1CS instance (A·z) ∘ (B·z) = C·z.

a, b, c are (m, n) dense matrices over the field; m = num_cons is a power of two and n = 2·num_vars_padded is a power of two with the witness in the low half (z = (W, 1, X)). num_io is the public-input count. The class holds no witness — an assignment z is passed to the product helpers, so one instance serves many assignments.

Source code in zorch/spartan/r1cs.py

@dataclass(frozen=True)
class R1CS:
    """A dense R1CS instance `(A·z) ∘ (B·z) = C·z`.

    `a`, `b`, `c` are `(m, n)` dense matrices over the field; `m = num_cons` is a
    power of two and `n = 2·num_vars_padded` is a power of two with the witness in
    the low half (`z = (W, 1, X)`). `num_io` is the public-input count. The class
    holds no witness — an assignment `z` is passed to the product helpers, so one
    instance serves many assignments.
    """

    a: Array
    b: Array
    c: Array
    num_io: int

    def __post_init__(self) -> None:
        if self.a.shape != self.b.shape or self.a.shape != self.c.shape:
            raise ValueError("A, B, C must share shape")
        m, n = self.a.shape
        # power-of-two guards (log2_strict_usize raises on a non-power-of-two).
        log2_strict_usize(m)
        log2_strict_usize(n)
        if n % 2 != 0:
            raise ValueError("column count must be even (witness fills the low half)")
        if self.num_io >= n // 2:
            raise ValueError("num_io must fit in the high half after the constant 1")

    @property
    def num_cons(self) -> int:
        return self.a.shape[0]

    @property
    def num_cols(self) -> int:
        return self.a.shape[1]

    @property
    def num_vars_padded(self) -> int:
        """`|W|` slot count — the low half of `z`."""
        return self.num_cols // 2

    @property
    def s_x(self) -> int:
        """Outer-sumcheck variable count `log2(num_cons)`."""
        return log2_strict_usize(self.num_cons)

    @property
    def s_y(self) -> int:
        """Inner-sumcheck variable count `log2(num_cols)` (= `log2(|W|)+1`)."""
        return log2_strict_usize(self.num_cols)

    def matvecs(self, z: Array) -> tuple[Array, Array, Array]:
        """`(A·z, B·z, C·z)`, each length `num_cons` — the outer-sumcheck MLEs."""
        return self.a @ z, self.b @ z, self.c @ z

    def is_satisfied(self, z: Array) -> Array:
        """Row-wise `(A·z)∘(B·z) == C·z` for all rows (scalar bool)."""
        az, bz, cz = self.matvecs(z)
        return fnp.all(az * bz == cz)

    def combined_row_mle(self, r_x: Array, r_batch: Array) -> Array:
        """`M(y) = Σ_i eq(r_x)_i · (A + r·B + r²·C)_{i,y}`, length `num_cols`.

        The inner-sumcheck operand: the three matrices batched by powers of `r`,
        then bound on the row variables at `r_x`. MSB-first row order matches the
        outer sumcheck's bind and `expand_eq_to_hypercube`.
        """
        combined = self.a + r_batch * self.b + r_batch * r_batch * self.c
        eq_rows = expand_eq_to_hypercube(r_x, fnp.ones((), self.a.dtype))
        return eq_rows @ combined

    def eval_combined_matrix(self, r_x: Array, r_y: Array, r_batch: Array) -> Array:
        """`Ã(r_x,r_y) + r·B̃ + r²·C̃` as `eq(r_x)·M·eq(r_y)` — the verifier's
        `eval_ABC`. Dense here; a succinct scheme opens it from a SPARK commitment.
        """
        combined = self.a + r_batch * self.b + r_batch * r_batch * self.c
        eq_rows = expand_eq_to_hypercube(r_x, fnp.ones((), self.a.dtype))
        eq_cols = expand_eq_to_hypercube(r_y, fnp.ones((), self.a.dtype))
        return eq_rows @ combined @ eq_cols

num_vars_padded property

num_vars_padded: int

|W| slot count — the low half of z.

s_x property

s_x: int

Outer-sumcheck variable count log2(num_cons).

s_y property

s_y: int

Inner-sumcheck variable count log2(num_cols) (= log2(|W|)+1).

matvecs

matvecs(z: Array) -> tuple[Array, Array, Array]

(A·z, B·z, C·z), each length num_cons — the outer-sumcheck MLEs.

Source code in zorch/spartan/r1cs.py

def matvecs(self, z: Array) -> tuple[Array, Array, Array]:
    """`(A·z, B·z, C·z)`, each length `num_cons` — the outer-sumcheck MLEs."""
    return self.a @ z, self.b @ z, self.c @ z

is_satisfied

is_satisfied(z: Array) -> Array

Row-wise (A·z)∘(B·z) == C·z for all rows (scalar bool).

Source code in zorch/spartan/r1cs.py

def is_satisfied(self, z: Array) -> Array:
    """Row-wise `(A·z)∘(B·z) == C·z` for all rows (scalar bool)."""
    az, bz, cz = self.matvecs(z)
    return fnp.all(az * bz == cz)

combined_row_mle

combined_row_mle(r_x: Array, r_batch: Array) -> Array

M(y) = Σ_i eq(r_x)_i · (A + r·B + r²·C)_{i,y}, length num_cols.

The inner-sumcheck operand: the three matrices batched by powers of r, then bound on the row variables at r_x. MSB-first row order matches the outer sumcheck's bind and expand_eq_to_hypercube.

Source code in zorch/spartan/r1cs.py

def combined_row_mle(self, r_x: Array, r_batch: Array) -> Array:
    """`M(y) = Σ_i eq(r_x)_i · (A + r·B + r²·C)_{i,y}`, length `num_cols`.

    The inner-sumcheck operand: the three matrices batched by powers of `r`,
    then bound on the row variables at `r_x`. MSB-first row order matches the
    outer sumcheck's bind and `expand_eq_to_hypercube`.
    """
    combined = self.a + r_batch * self.b + r_batch * r_batch * self.c
    eq_rows = expand_eq_to_hypercube(r_x, fnp.ones((), self.a.dtype))
    return eq_rows @ combined

eval_combined_matrix

eval_combined_matrix(
    r_x: Array, r_y: Array, r_batch: Array
) -> Array

Ã(r_x,r_y) + r·B̃ + r²·C̃ as eq(r_x)·M·eq(r_y) — the verifier's eval_ABC. Dense here; a succinct scheme opens it from a SPARK commitment.

Source code in zorch/spartan/r1cs.py

def eval_combined_matrix(self, r_x: Array, r_y: Array, r_batch: Array) -> Array:
    """`Ã(r_x,r_y) + r·B̃ + r²·C̃` as `eq(r_x)·M·eq(r_y)` — the verifier's
    `eval_ABC`. Dense here; a succinct scheme opens it from a SPARK commitment.
    """
    combined = self.a + r_batch * self.b + r_batch * r_batch * self.c
    eq_rows = expand_eq_to_hypercube(r_x, fnp.ones((), self.a.dtype))
    eq_cols = expand_eq_to_hypercube(r_y, fnp.ones((), self.a.dtype))
    return eq_rows @ combined @ eq_cols

SpartanClaim dataclass

Public R1CS satisfiability claim.

Source code in zorch/spartan/spartan.py

@dataclass(frozen=True)
class SpartanClaim:
    """Public R1CS satisfiability claim."""

    instance: R1CS
    public_inputs: Array

    def __post_init__(self) -> None:
        if self.public_inputs.shape != (self.instance.num_io,):
            raise ValueError(
                f"expected {self.instance.num_io} public inputs, "
                f"got shape {self.public_inputs.shape}"
            )

SpartanProof dataclass

One named reduction-proof section per coarse protocol phase.

Source code in zorch/spartan/spartan.py

@dataclass(frozen=True)
class SpartanProof:
    """One named reduction-proof section per coarse protocol phase."""

    commitment: Array
    outer: OuterProof
    inner: InnerProof
    witness_open: WitnessOpenProof

SpartanProver

Bases: ProverStage[SpartanClaim, SpartanWitness, TrivialClaim, SpartanProof]

The Spartan prover role; owns the PCS proving capability only.

Source code in zorch/spartan/spartan.py

class SpartanProver(
    ProverStage[SpartanClaim, SpartanWitness, TrivialClaim, SpartanProof]
):
    """The Spartan prover role; owns the PCS proving capability only."""

    def __init__(
        self,
        pcs_prover: CommittingOpener[Any, Any, Any],
        *,
        outer: (
            ProverStage[
                ZerocheckClaim, ZerocheckWitness, RowEvaluationClaim, OuterProof
            ]
            | None
        ) = None,
        inner: (
            ProverStage[
                LincheckClaim, LincheckWitness, ColumnEvaluationClaim, InnerProof
            ]
            | None
        ) = None,
        witness_open: (
            ProverStage[
                WitnessOpeningClaim,
                WitnessOpeningWitness,
                TrivialClaim,
                WitnessOpenProof,
            ]
            | None
        ) = None,
        challenges: ChallengePolicy,
    ) -> None:
        self.challenges = challenges
        self.pcs_prover = pcs_prover
        self.outer = outer or OuterProver(challenges=challenges)
        self.inner = inner or InnerProver(challenges=challenges)
        self.witness_open = witness_open or WitnessOpenProver(
            cast(
                ProverStage[
                    OpeningClaim[Any],
                    OpeningWitness[Any],
                    TrivialClaim,
                    OpeningProof[Any],
                ],
                pcs_prover,
            )
        )

    def prove(
        self,
        claim: SpartanClaim,
        witness: SpartanWitness,
        transcript: Transcript,
    ) -> ProveResult[TrivialClaim, SpartanProof]:
        instance = claim.instance
        assignment = witness.assignment
        if assignment.shape != (instance.num_cols,):
            raise ValueError(
                f"expected assignment shape {(instance.num_cols,)}, "
                f"got {assignment.shape}"
            )
        witness_poly = assignment[: instance.num_vars_padded]
        commitment, prover_data = self.pcs_prover.commit([witness_poly])
        transcript = _absorb_claim(transcript, claim, commitment)

        az, bz, cz = instance.matvecs(assignment)
        outer = self.outer.prove(
            ZerocheckClaim(instance.s_x),
            ZerocheckWitness(az, bz, cz),
            transcript,
        )
        batch, transcript = batch_claims(
            outer.reduced_claim.values, outer.transcript, self.challenges
        )
        inner = self.inner.prove(
            LincheckClaim(instance, outer.reduced_claim, batch),
            LincheckWitness(assignment),
            transcript,
        )
        opening_claim = witness_opening_claim(
            commitment,
            instance,
            claim.public_inputs,
            outer.reduced_claim,
            batch,
            inner.reduced_claim,
        )
        opening = self.witness_open.prove(
            opening_claim,
            WitnessOpeningWitness(prover_data),
            inner.transcript,
        )
        return ProveResult(
            TrivialClaim(),
            SpartanProof(
                commitment,
                outer.reduction_proof,
                inner.reduction_proof,
                opening.reduction_proof,
            ),
            opening.transcript,
        )

SpartanVerifier

Bases: VerifierStage[SpartanClaim, TrivialClaim, SpartanProof]

The Spartan verifier role; owns the PCS verification capability only.

Source code in zorch/spartan/spartan.py

class SpartanVerifier(VerifierStage[SpartanClaim, TrivialClaim, SpartanProof]):
    """The Spartan verifier role; owns the PCS verification capability only."""

    def __init__(
        self,
        pcs_verifier: VerifierStage[
            OpeningClaim[Any], TrivialClaim, OpeningProof[Any], Any
        ],
        *,
        outer: (
            VerifierStage[ZerocheckClaim, RowEvaluationClaim, OuterProof] | None
        ) = None,
        inner: (
            VerifierStage[LincheckClaim, ColumnEvaluationClaim, InnerProof] | None
        ) = None,
        witness_open: (
            VerifierStage[WitnessOpeningClaim, TrivialClaim, WitnessOpenProof] | None
        ) = None,
        challenges: ChallengePolicy,
    ) -> None:
        self.challenges = challenges
        self.outer = outer or OuterVerifier(challenges=challenges)
        self.inner = inner or InnerVerifier(challenges=challenges)
        self.witness_open = witness_open or WitnessOpenVerifier(pcs_verifier)

    def verify(
        self,
        claim: SpartanClaim,
        reduction_proof: SpartanProof,
        transcript: Transcript,
    ) -> VerifyResult[TrivialClaim]:
        transcript = _absorb_claim(transcript, claim, reduction_proof.commitment)
        outer = self.outer.verify(
            ZerocheckClaim(claim.instance.s_x),
            reduction_proof.outer,
            transcript,
        )
        batch, transcript = batch_claims(
            outer.reduced_claim.values, outer.transcript, self.challenges
        )
        inner = self.inner.verify(
            LincheckClaim(claim.instance, outer.reduced_claim, batch),
            reduction_proof.inner,
            transcript,
        )
        opening = self.witness_open.verify(
            witness_opening_claim(
                reduction_proof.commitment,
                claim.instance,
                claim.public_inputs,
                outer.reduced_claim,
                batch,
                inner.reduced_claim,
            ),
            reduction_proof.witness_open,
            inner.transcript,
        )
        return VerifyResult(
            TrivialClaim(), opening.transcript, outer.ok & inner.ok & opening.ok
        )

SpartanWitness dataclass

Private assignment witnessing a SpartanClaim.

Source code in zorch/spartan/spartan.py

@dataclass(frozen=True)
class SpartanWitness:
    """Private assignment witnessing a ``SpartanClaim``."""

    assignment: Array

assignment

assignment(
    witness: Array,
    io: Array,
    num_vars_padded: int,
    num_io: int,
) -> Array

Assemble z = (W, 1, X) from the witness and public inputs.

W is padded into the low half [0, num_vars_padded); the high half holds the constant 1 at its first slot, then the public inputs X, then zero padding. Length is 2·num_vars_padded.

Source code in zorch/spartan/r1cs.py

def assignment(witness: Array, io: Array, num_vars_padded: int, num_io: int) -> Array:
    """Assemble `z = (W, 1, X)` from the witness and public inputs.

    `W` is padded into the low half `[0, num_vars_padded)`; the high half holds
    the constant `1` at its first slot, then the public inputs `X`, then zero
    padding. Length is `2·num_vars_padded`.
    """
    if witness.shape[0] > num_vars_padded:
        raise ValueError("witness longer than the padded low half")
    if io.shape[0] != num_io:
        raise ValueError(f"expected {num_io} public inputs, got {io.shape[0]}")
    dtype = witness.dtype
    low = fnp.zeros((num_vars_padded,), dtype).at[: witness.shape[0]].set(witness)
    high = fnp.zeros((num_vars_padded,), dtype).at[0].set(fnp.ones((), dtype))
    high = high.at[1 : 1 + num_io].set(io)
    return fnp.concatenate([low, high])