"""SimpleLeft AIR constraint evaluation.
This module implements the constraint polynomial for SimpleLeft AIR exactly as
the PIL compiler generates it. The constraint structure was reverse-engineered
from SimpleLeft.expressionsinfo.json.
Constraint structure (8 constraints combined with std_vc powers):
- 6 im_cluster constraints (each verifies: im * prod(denoms) = sum_cross)
- 1 gsum recurrence constraint
- 1 boundary constraint at last row
The compress formula is: ((col2*α + col1)*α + busid) + γ for 2 columns,
or (col1*α + busid) + γ for 1 column.
"""
import numpy as np
from primitives.field import FF3, GOLDILOCKS_PRIME, FF3Poly
from .base import ConstraintContext, ConstraintModule, compress_2col
[docs]
class SimpleLeftConstraints(ConstraintModule):
"""Constraint evaluation for SimpleLeft AIR.
This implementation matches the exact constraint structure generated by the
PIL compiler as found in SimpleLeft.expressionsinfo.json.
"""
[docs]
def constraint_polynomial(self, ctx: ConstraintContext) -> FF3Poly | FF3:
"""Evaluate combined constraint polynomial.
For prover: returns polynomial over evaluation domain
For verifier: returns single FF3 value at evaluation point xi
"""
# Get challenges
alpha = ctx.challenge('std_alpha')
gamma = ctx.challenge('std_gamma')
vc = ctx.challenge('std_vc')
# Get witness columns (stage 1) - need conversion for prover/verifier compat
a = ctx.col('a')
b = ctx.col('b')
c = ctx.col('c')
d = ctx.col('d')
e = ctx.col('e')
f = ctx.col('f')
g = ctx.col('g')
h = ctx.col('h')
k = [ctx.col('k', i) for i in range(7)]
# Get intermediate columns (stage 2)
gsum = ctx.col('gsum')
prev_gsum = ctx.prev_col('gsum') # gsum at row-1 (used in constraint 6)
im = [ctx.col('im_cluster', i) for i in range(6)]
# Get constant L1 (selector for first row: [1,0,0,...])
L1 = ctx.const('__L1__')
next_L1 = ctx.next_const('__L1__') # L1 at row+1
# Get airgroup value (result)
gsum_result = ctx.airgroup_value(0)
# Detect prover vs verifier mode
try:
n = len(a) # Prover mode: a is an array
except TypeError:
n = None # Verifier mode: a is a scalar
# Helper for creating scalar/array constants
def const(value: int) -> FF3:
if n is None:
return FF3(value % GOLDILOCKS_PRIME)
return FF3(np.full(n, value % GOLDILOCKS_PRIME, dtype=np.uint64))
# Helper for 1-column compress
def compress_1col(busid: int, col: FF3) -> FF3:
return col * alpha + const(busid) + gamma
# Build constraint polynomials (unweighted)
constraints = []
neg_one = const(-1)
one = const(1)
# ===================================================================
# Constraint 0: im_cluster[0] for (c,d busid=1) + (e,f busid=2)
# im * D1 * D2 - (D2 + (-1)*D1) = 0
# Where D1 = compress(1, [c,d]), D2 = compress(2, [e,f])
# ===================================================================
D1 = compress_2col(1, c, d, alpha, gamma, n)
D2 = compress_2col(2, e, f, alpha, gamma, n)
constraint_0 = im[0] * D1 * D2 - (D2 + neg_one * D1)
constraints.append(constraint_0)
# ===================================================================
# Constraint 1: im_cluster[1] for (g,h busid=3) + (k[0] busid=100)
# im * D1 * D2 - ((-1)*D2 + (-1)*D1) = 0
# ===================================================================
D1 = compress_2col(3, g, h, alpha, gamma, n)
D2 = compress_1col(100, k[0])
constraint_1 = im[1] * D1 * D2 - (neg_one * D2 + neg_one * D1)
constraints.append(constraint_1)
# ===================================================================
# Constraint 2: im_cluster[2] for (k[1] busid=101) + (k[2]-1 busid=100)
# im * D1 * D2 - ((-1)*D2 + (-1)*D1) = 0
# ===================================================================
D1 = compress_1col(101, k[1])
D2 = compress_1col(100, k[2] - one)
constraint_2 = im[2] * D1 * D2 - (neg_one * D2 + neg_one * D1)
constraints.append(constraint_2)
# ===================================================================
# Constraint 3: im_cluster[3] for (255-k[2] busid=100) + (k[3] busid=101)
# im * D1 * D2 - ((-1)*D2 + (-1)*D1) = 0
# ===================================================================
D1 = compress_1col(100, const(255) - k[2])
D2 = compress_1col(101, k[3])
constraint_3 = im[3] * D1 * D2 - (neg_one * D2 + neg_one * D1)
constraints.append(constraint_3)
# ===================================================================
# Constraint 4: im_cluster[4] for (256-k[3] busid=101) + (k[4] busid=102)
# im * D1 * D2 - ((-1)*D2 + (-1)*D1) = 0
# ===================================================================
D1 = compress_1col(101, const(256) - k[3])
D2 = compress_1col(102, k[4])
constraint_4 = im[4] * D1 * D2 - (neg_one * D2 + neg_one * D1)
constraints.append(constraint_4)
# ===================================================================
# Constraint 5: im_cluster[5] for (k[5] busid=103) + (k[6] busid=104)
# im * D1 * D2 - ((-1)*D2 + (-1)*D1) = 0
# ===================================================================
D1 = compress_1col(103, k[5])
D2 = compress_1col(104, k[6])
constraint_5 = im[5] * D1 * D2 - (neg_one * D2 + neg_one * D1)
constraints.append(constraint_5)
# ===================================================================
# Constraint 6: gsum recurrence
# (gsum - prev_gsum*(1-L1) - sum_ims) * direct_den + 1 = 0
# direct_den = compress(1, [a, b])
# ===================================================================
sum_ims = im[0]
for i in range(1, 6):
sum_ims = sum_ims + im[i]
one_minus_L1 = one - L1
direct_den = compress_2col(1, a, b, alpha, gamma, n)
gsum_recurrence = (gsum - prev_gsum * one_minus_L1 - sum_ims) * direct_den + one
constraints.append(gsum_recurrence)
# ===================================================================
# Constraint 7: boundary at last row
# L1' * (gsum_result - gsum) = 0
# ===================================================================
boundary = next_L1 * (gsum_result - gsum)
constraints.append(boundary)
# Combine constraints using std_vc powers
return self._combine_constraints(constraints, vc)