Skip to content

zorch.spartan.r1cs

R1CS instance (A·z) ∘ (B·z) = C·z and the products the Spartan PIOP reduces.

The assignment is witness-first z = (W, 1, X): W fills the low half, the high half holds the constant 1 then the public inputs X. That layout is what makes r_y[0] (the inner sumcheck's first-bound variable) the half-selector between W and (1, X), so W opens at r_y[1:]. Matrices are dense (a sparse SPARK form would plug the same matvecs / combined-row interface). Field is the caller's dtype.

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 
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
@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 
74
75
76
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 
78
79
80
81
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 
83
84
85
86
87
88
89
90
91
92
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 
 94
 95
 96
 97
 98
 99
100
101
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

eval_eq 

eval_eq(w: Array, x: Array) -> Array

eq(w, x) = Π_i (1 - w_i - x_i + 2·w_i·x_i) for two equal-length points, in O(len) time and O(1) memory.

The closed form of the equality polynomial evaluated at a pair of points -- equals (expand_eq_to_hypercube(x, 1) · expand_eq_to_hypercube(w, 1)).sum() but without materializing either 2^len vector, so a verifier evaluating eq at a bound point stays succinct. Symmetric in w/x and order-agnostic (a product over coordinates), so MSB/LSB indexing does not matter.

Source code in zorch/poly/eq.py 
43
44
45
46
47
48
49
50
51
52
def eval_eq(w: Array, x: Array) -> Array:
    """eq(w, x) = Π_i (1 - w_i - x_i + 2·w_i·x_i) for two equal-length points, in
    O(len) time and O(1) memory.

    The closed form of the equality polynomial evaluated at a pair of points --
    equals ``(expand_eq_to_hypercube(x, 1) · expand_eq_to_hypercube(w, 1)).sum()``
    but without materializing either 2^len vector, so a verifier evaluating eq at
    a bound point stays succinct. Symmetric in ``w``/``x`` and order-agnostic (a
    product over coordinates), so MSB/LSB indexing does not matter."""
    return fnp.prod(eq_factor(w, x), axis=-1)

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 
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
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])

eval_public_half 

eval_public_half(
    io: Array, r_y_rest: Array, num_vars_padded: int
) -> Array

MLE of the public high half (1, X, 0…) at r_y[1:].

The verifier evaluates the (1, X) part of z̃ itself; combined with the witness opening eval_W it reconstructs z̃(r_y) — see pcs_glue.

Source code in zorch/spartan/r1cs.py 
122
123
124
125
126
127
128
129
130
131
def eval_public_half(io: Array, r_y_rest: Array, num_vars_padded: int) -> Array:
    """MLE of the public high half `(1, X, 0…)` at `r_y[1:]`.

    The verifier evaluates the `(1, X)` part of `z̃` itself; combined with the
    witness opening `eval_W` it reconstructs `z̃(r_y)` — see `pcs_glue`.
    """
    dtype = io.dtype
    high = fnp.zeros((num_vars_padded,), dtype).at[0].set(fnp.ones((), dtype))
    high = high.at[1 : 1 + io.shape[0]].set(io)
    return (high * expand_eq_to_hypercube(r_y_rest, fnp.ones((), dtype))).sum()

recombine_z_eval 

recombine_z_eval(
    eval_w: Array, eval_pub: Array, r_y0: Array
) -> Array

z̃(r_y) from the two half-openings: (1−r_y0)·eval_W + r_y0·eval_pub.

r_y0 (the MSB inner challenge) selects between the witness low half and the public high half; the multilinear bind on that top variable is this affine combination.

Source code in zorch/spartan/r1cs.py 
134
135
136
137
138
139
140
141
142
def recombine_z_eval(eval_w: Array, eval_pub: Array, r_y0: Array) -> Array:
    """`z̃(r_y)` from the two half-openings: `(1−r_y0)·eval_W + r_y0·eval_pub`.

    `r_y0` (the MSB inner challenge) selects between the witness low half and the
    public high half; the multilinear bind on that top variable is this affine
    combination.
    """
    one = fnp.ones((), eval_w.dtype)
    return (one - r_y0) * eval_w + r_y0 * eval_pub