use crate::ProgramCell;
use crate::constraint::{ConstraintAst, ConstraintExpr, ExprId};
use alloc::vec;
use alloc::vec::Vec;
use hekate_math::{Flat, HardwareField, TowerField};
#[derive(Clone, Copy, Debug, Eq, PartialEq)]
pub enum WireRole {
Lhs = 0,
Rhs = 1,
Product = 2,
}
#[derive(Clone, Copy, Debug, Eq, PartialEq)]
pub enum Unknown {
Pad(u32),
Wire { mul: u32, role: WireRole },
}
#[derive(Clone, Copy, Debug, Eq, PartialEq)]
pub struct ClaimLayout {
pub pad_first: u32,
pub half: u32,
}
impl ClaimLayout {
pub fn index(&self, cell: ProgramCell) -> u32 {
let base = cell.col_idx as u32;
match cell.next_row {
true => base + self.half,
false => base,
}
}
}
#[derive(Clone, Debug)]
pub struct AffineRow<F> {
pub unknowns: Vec<(Unknown, Flat<F>)>,
pub claims: Vec<(u32, Flat<F>)>,
pub constant: Flat<F>,
}
#[derive(Clone, Debug)]
pub struct PredicateRows<F> {
pub affine: Vec<AffineRow<F>>,
pub mul_nodes: u32,
pub roots: Vec<Form<F>>,
}
#[derive(Clone, Debug)]
pub struct Form<F> {
pub unknowns: Vec<(Unknown, Flat<F>)>,
pub claims: Vec<(u32, Flat<F>)>,
pub constant: Flat<F>,
}
impl<F: TowerField> Default for Form<F> {
fn default() -> Self {
Self {
unknowns: Vec::new(),
claims: Vec::new(),
constant: Flat::from_raw(F::ZERO),
}
}
}
impl<F: HardwareField> Form<F> {
fn extend(&mut self, other: &Self) {
self.unknowns.extend_from_slice(&other.unknowns);
self.claims.extend_from_slice(&other.claims);
self.constant += other.constant;
}
fn scaled(&self, coeff: Flat<F>) -> Self {
Self {
unknowns: self.unknowns.iter().map(|&(v, c)| (v, c * coeff)).collect(),
claims: self.claims.iter().map(|&(v, c)| (v, c * coeff)).collect(),
constant: self.constant * coeff,
}
}
pub fn evaluate(&self, claims: &[Flat<F>], pad: &[Flat<F>], wires: &[[Flat<F>; 3]]) -> Flat<F> {
let mut acc = self.constant;
for &(idx, coeff) in &self.claims {
acc += coeff * claims[idx as usize];
}
for &(unknown, coeff) in &self.unknowns {
let v = match unknown {
Unknown::Pad(i) => pad[i as usize],
Unknown::Wire { mul, role } => wires[mul as usize][role as usize],
};
acc += coeff * v;
}
acc
}
}
pub fn wire_values<F: TowerField + HardwareField>(
ast: &ConstraintAst<F>,
node_values: &[Flat<F>],
) -> Vec<[Flat<F>; 3]> {
let live = crate::outer::reachable(ast);
let mut wires = Vec::new();
for (i, &alive) in live.iter().enumerate() {
if !alive {
continue;
}
if let ConstraintExpr::Mul(a, b) = ast.arena.get(ExprId(i as u32)) {
wires.push([
node_values[a.0 as usize],
node_values[b.0 as usize],
node_values[i],
]);
}
}
wires
}
pub fn compile<F: HardwareField>(ast: &ConstraintAst<F>, layout: ClaimLayout) -> PredicateRows<F> {
let n = ast.arena.len();
let live = crate::outer::reachable(ast);
let one = Flat::from_raw(F::ONE);
let mut forms: Vec<Form<F>> = Vec::with_capacity(n);
let mut affine: Vec<AffineRow<F>> = Vec::new();
let mut mul_nodes: u32 = 0;
for (i, &alive) in live.iter().enumerate() {
if !alive {
forms.push(Form::default());
continue;
}
let form = match ast.arena.get(ExprId(i as u32)) {
ConstraintExpr::Cell(cell) => {
let idx = layout.index(*cell);
Form {
unknowns: vec![(Unknown::Pad(layout.pad_first + idx), one)],
claims: vec![(idx, one)],
constant: Flat::from_raw(F::ZERO),
}
}
ConstraintExpr::Const(v) => Form {
unknowns: Vec::new(),
claims: Vec::new(),
constant: v.to_hardware(),
},
ConstraintExpr::Add(a, b) => {
let mut acc = forms[a.0 as usize].clone();
acc.extend(&forms[b.0 as usize]);
acc
}
ConstraintExpr::Scale(coeff, a) => forms[a.0 as usize].scaled(coeff.to_hardware()),
ConstraintExpr::Sum(children) => {
let mut acc = Form::default();
for c in children {
acc.extend(&forms[c.0 as usize]);
}
acc
}
ConstraintExpr::Mul(a, b) => {
let mul = mul_nodes;
mul_nodes += 1;
for (role, side) in [(WireRole::Lhs, a), (WireRole::Rhs, b)] {
let operand = &forms[side.0 as usize];
let mut unknowns = operand.unknowns.clone();
unknowns.push((Unknown::Wire { mul, role }, one));
affine.push(AffineRow {
unknowns,
claims: operand.claims.clone(),
constant: operand.constant,
});
}
Form {
unknowns: vec![(
Unknown::Wire {
mul,
role: WireRole::Product,
},
one,
)],
claims: Vec::new(),
constant: Flat::from_raw(F::ZERO),
}
}
};
forms.push(form);
}
let roots = ast
.roots
.iter()
.map(|r| forms[r.0 as usize].clone())
.collect();
PredicateRows {
affine,
mul_nodes,
roots,
}
}
#[cfg(test)]
mod tests {
use super::*;
use crate::constraint::ConstraintArena;
use hekate_math::{Block128, Flat, HardwareField};
type F = Block128;
const LAYOUT: ClaimLayout = ClaimLayout {
pad_first: 100,
half: 8,
};
const COLS: usize = 6;
const HONEST: ClaimLayout = ClaimLayout {
pad_first: 0,
half: COLS as u32,
};
fn mix(seed: u128) -> F {
F::from(
seed.wrapping_mul(0x9e37_79b9_7f4a_7c15)
.wrapping_add(0x51ed_2701),
)
}
fn one() -> Flat<F> {
Flat::from_raw(F::ONE)
}
fn value_of(
unknowns: &[(Unknown, Flat<F>)],
claims: &[(u32, Flat<F>)],
constant: Flat<F>,
masked: &[F],
pad: &[F],
wires: &[[Flat<F>; 3]],
) -> Flat<F> {
let mut acc = constant;
for &(idx, coeff) in claims {
acc += coeff * masked[idx as usize].to_hardware();
}
for &(unknown, coeff) in unknowns {
let v = match unknown {
Unknown::Pad(i) => pad[i as usize].to_hardware(),
Unknown::Wire { mul, role } => {
let slot = match role {
WireRole::Lhs => 0,
WireRole::Rhs => 1,
WireRole::Product => 2,
};
wires[mul as usize][slot]
}
};
acc += coeff * v;
}
acc
}
fn ast_of(build: impl FnOnce(&mut ConstraintArena<F>) -> Vec<ExprId>) -> ConstraintAst<F> {
let mut arena = ConstraintArena::<F>::new();
let roots = build(&mut arena);
let labels = roots.iter().map(|_| None).collect();
ConstraintAst {
arena,
roots,
labels,
}
}
fn rich_ast() -> ConstraintAst<F> {
ast_of(|a| {
let cols: Vec<ExprId> = (0..COLS).map(|i| a.cell(ProgramCell::current(i))).collect();
let nexts: Vec<ExprId> = (0..COLS).map(|i| a.cell(ProgramCell::next(i))).collect();
let shared = a.mul(cols[0], cols[1]);
let k = a.constant(mix(7));
let scaled = a.scale(mix(11), shared);
let summed = a.sum(vec![cols[2], nexts[3], k, scaled]);
let deep = a.mul(summed, nexts[4]);
let nested = a.mul(deep, cols[5]);
let tail = a.add(nested, shared);
vec![tail, a.add(shared, nexts[0]), deep]
})
}
#[test]
fn honest_values_satisfy_every_affine_row() {
let ast = rich_ast();
let rows = compile(&ast, HONEST);
let plain: Vec<F> = (0..2 * COLS).map(|i| mix(i as u128 + 1)).collect();
let pad: Vec<F> = (0..2 * COLS).map(|i| mix(i as u128 + 977)).collect();
let masked: Vec<F> = plain.iter().zip(&pad).map(|(c, h)| *c + *h).collect();
let current: Vec<Flat<F>> = plain[..COLS].iter().map(|v| v.to_hardware()).collect();
let next: Vec<Flat<F>> = plain[COLS..].iter().map(|v| v.to_hardware()).collect();
let consts = ast.precompute_hardware_consts();
let mut node_values = Vec::new();
ast.evaluate_into(&consts, ¤t, &next, &mut node_values);
let wires = wire_values(&ast, &node_values);
assert_eq!(wires.len(), rows.mul_nodes as usize);
for row in &rows.affine {
let zero = Flat::from_raw(F::ZERO);
let lhs = value_of(&row.unknowns, &[], zero, &masked, &pad, &wires);
let rhs = value_of(&[], &row.claims, row.constant, &masked, &pad, &wires);
assert_eq!(lhs, rhs);
}
for wire in &wires {
assert_eq!(wire[0] * wire[1], wire[2]);
}
}
#[test]
fn compiled_roots_reproduce_ast_evaluation() {
let ast = rich_ast();
let rows = compile(&ast, HONEST);
let plain: Vec<F> = (0..2 * COLS).map(|i| mix(i as u128 + 1)).collect();
let pad: Vec<F> = (0..2 * COLS).map(|i| mix(i as u128 + 977)).collect();
let masked: Vec<F> = plain.iter().zip(&pad).map(|(c, h)| *c + *h).collect();
let current: Vec<Flat<F>> = plain[..COLS].iter().map(|v| v.to_hardware()).collect();
let next: Vec<Flat<F>> = plain[COLS..].iter().map(|v| v.to_hardware()).collect();
let consts = ast.precompute_hardware_consts();
let mut node_values = Vec::new();
ast.evaluate_into(&consts, ¤t, &next, &mut node_values);
let wires = wire_values(&ast, &node_values);
let expected = ast.evaluate(¤t, &next);
for (k, form) in rows.roots.iter().enumerate() {
let got = value_of(
&form.unknowns,
&form.claims,
form.constant,
&masked,
&pad,
&wires,
);
assert_eq!(got, expected[k]);
}
}
#[test]
fn flipped_claim_breaks_roots_that_read_it() {
let ast = rich_ast();
let rows = compile(&ast, HONEST);
let plain: Vec<F> = (0..2 * COLS).map(|i| mix(i as u128 + 1)).collect();
let pad: Vec<F> = (0..2 * COLS).map(|i| mix(i as u128 + 977)).collect();
let mut masked: Vec<F> = plain.iter().zip(&pad).map(|(c, h)| *c + *h).collect();
let current: Vec<Flat<F>> = plain[..COLS].iter().map(|v| v.to_hardware()).collect();
let next: Vec<Flat<F>> = plain[COLS..].iter().map(|v| v.to_hardware()).collect();
let consts = ast.precompute_hardware_consts();
let mut node_values = Vec::new();
ast.evaluate_into(&consts, ¤t, &next, &mut node_values);
let wires = wire_values(&ast, &node_values);
let honest: Vec<Flat<F>> = rows
.roots
.iter()
.map(|f| value_of(&f.unknowns, &f.claims, f.constant, &masked, &pad, &wires))
.collect();
const FLIPPED: u32 = 2;
masked[FLIPPED as usize] += F::ONE;
for (k, form) in rows.roots.iter().enumerate() {
let got = value_of(
&form.unknowns,
&form.claims,
form.constant,
&masked,
&pad,
&wires,
);
let reads_it = form.claims.iter().any(|&(idx, _)| idx == FLIPPED);
assert_eq!(got != honest[k], reads_it);
}
}
#[test]
fn cell_binds_one_pad_entry_and_one_claim() {
let ast = ast_of(|a| vec![a.cell(ProgramCell::current(3))]);
let rows = compile(&ast, LAYOUT);
assert_eq!(rows.mul_nodes, 0);
assert!(rows.affine.is_empty());
assert_eq!(rows.roots[0].unknowns, vec![(Unknown::Pad(103), one())]);
assert_eq!(rows.roots[0].claims, vec![(3, one())]);
}
#[test]
fn next_row_cell_lands_in_second_half() {
let ast = ast_of(|a| vec![a.cell(ProgramCell::next(3))]);
let rows = compile(&ast, LAYOUT);
assert_eq!(rows.roots[0].claims, vec![(11, one())]);
assert_eq!(rows.roots[0].unknowns, vec![(Unknown::Pad(111), one())]);
}
#[test]
fn mul_emits_two_affine_rows_and_yields_its_product_wire() {
let ast = ast_of(|a| {
let x = a.cell(ProgramCell::current(0));
let y = a.cell(ProgramCell::current(1));
vec![a.mul(x, y)]
});
let rows = compile(&ast, LAYOUT);
assert_eq!(rows.mul_nodes, 1);
assert_eq!(rows.affine.len(), 2);
assert_eq!(
rows.roots[0].unknowns,
vec![(
Unknown::Wire {
mul: 0,
role: WireRole::Product
},
one()
)]
);
}
#[test]
fn wire_row_pins_its_operand() {
let ast = ast_of(|a| {
let x = a.cell(ProgramCell::current(0));
let y = a.cell(ProgramCell::current(1));
vec![a.mul(x, y)]
});
let rows = compile(&ast, LAYOUT);
let lhs = &rows.affine[0];
assert_eq!(lhs.claims, vec![(0, one())]);
assert!(lhs.unknowns.contains(&(Unknown::Pad(100), one())));
assert!(lhs.unknowns.contains(&(
Unknown::Wire {
mul: 0,
role: WireRole::Lhs
},
one()
)));
}
#[test]
fn nested_muls_number_their_wires_in_arena_order() {
let ast = ast_of(|a| {
let x = a.cell(ProgramCell::current(0));
let y = a.cell(ProgramCell::current(1));
let z = a.cell(ProgramCell::current(2));
let inner = a.mul(x, y);
vec![a.mul(inner, z)]
});
let rows = compile(&ast, LAYOUT);
assert_eq!(rows.mul_nodes, 2);
assert_eq!(rows.affine.len(), 4);
assert_eq!(
rows.affine[2].unknowns,
vec![
(
Unknown::Wire {
mul: 0,
role: WireRole::Product
},
one()
),
(
Unknown::Wire {
mul: 1,
role: WireRole::Lhs
},
one()
)
]
);
}
#[test]
fn shared_mul_is_compiled_once() {
let ast = ast_of(|a| {
let x = a.cell(ProgramCell::current(0));
let y = a.cell(ProgramCell::current(1));
let shared = a.mul(x, y);
vec![a.add(shared, x), a.add(shared, y)]
});
let rows = compile(&ast, LAYOUT);
assert_eq!(rows.mul_nodes, 1);
assert_eq!(rows.affine.len(), 2);
}
#[test]
fn constant_lands_on_public_side() {
let ast = ast_of(|a| {
let k = a.constant(F::ONE);
let x = a.cell(ProgramCell::current(0));
vec![a.add(k, x)]
});
let rows = compile(&ast, LAYOUT);
assert_eq!(rows.roots[0].constant, one());
assert_eq!(rows.roots[0].claims, vec![(0, one())]);
}
#[test]
fn scale_multiplies_every_coefficient() {
let two = F::from(2u8);
let ast = ast_of(|a| {
let x = a.cell(ProgramCell::current(0));
let k = a.constant(F::ONE);
let s = a.add(x, k);
vec![a.scale(two, s)]
});
let rows = compile(&ast, LAYOUT);
assert_eq!(rows.roots[0].claims, vec![(0, two.to_hardware())]);
assert_eq!(rows.roots[0].constant, two.to_hardware());
}
#[test]
fn sum_collects_every_child() {
let ast = ast_of(|a| {
let cells: Vec<ExprId> = (0..4).map(|i| a.cell(ProgramCell::current(i))).collect();
vec![a.sum(cells)]
});
let rows = compile(&ast, LAYOUT);
assert_eq!(rows.roots[0].claims.len(), 4);
assert_eq!(rows.roots[0].unknowns.len(), 4);
}
#[test]
fn mul_count_agrees_with_shape_pass() {
let ast = ast_of(|a| {
let x = a.cell(ProgramCell::current(0));
let y = a.cell(ProgramCell::current(1));
let z = a.cell(ProgramCell::current(2));
let p = a.mul(x, y);
let q = a.mul(p, z);
vec![a.add(p, q)]
});
let rows = compile(&ast, LAYOUT);
assert_eq!(rows.mul_nodes as usize, crate::outer::mul_node_count(&ast));
}
}