binius_core/
verify.rs

1// Copyright 2025 Irreducible Inc.
2//! Routines for checking whether the
3//! [constraint system][`crate::constraint_system::ConstraintSystem`] is satisfied with the given
4//! [value vector][`ValueVec`].
5
6use crate::{
7	constraint_system::{
8		AndConstraint, ConstraintSystem, MulConstraint, ShiftVariant, ShiftedValueIndex, ValueVec,
9	},
10	word::Word,
11};
12
13/// Evaluates a shifted value from the witness
14fn eval_shifted(witness: &ValueVec, sv: &ShiftedValueIndex) -> Word {
15	let Word(val) = witness[sv.value_index];
16	match sv.shift_variant {
17		ShiftVariant::Sll => Word(val << sv.amount),
18		ShiftVariant::Slr => Word(val >> sv.amount),
19		ShiftVariant::Sar => Word(((val as i64) >> sv.amount) as u64),
20	}
21}
22
23/// Evaluates an operand (XOR of shifted values)
24pub fn eval_operand(witness: &ValueVec, operand: &[ShiftedValueIndex]) -> Word {
25	operand
26		.iter()
27		.map(|sv| eval_shifted(witness, sv))
28		.fold(Word(0), |acc, val| acc ^ val)
29}
30
31/// Verifies that an AND constraint is satisfied: (A & B) ^ C = 0
32pub fn verify_and_constraint(witness: &ValueVec, constraint: &AndConstraint) -> Result<(), String> {
33	let Word(a) = eval_operand(witness, &constraint.a);
34	let Word(b) = eval_operand(witness, &constraint.b);
35	let Word(c) = eval_operand(witness, &constraint.c);
36
37	let result = (a & b) ^ c;
38	if result != 0 {
39		Err(format!(
40			"AND constraint failed: ({a:016x} & {b:016x}) ^ {c:016x} = {result:016x} (expected 0)",
41		))
42	} else {
43		Ok(())
44	}
45}
46
47/// Verifies that a MUL constraint is satisfied: A * B = (HI << 64) | LO
48pub fn verify_mul_constraint(witness: &ValueVec, constraint: &MulConstraint) -> Result<(), String> {
49	let Word(a) = eval_operand(witness, &constraint.a);
50	let Word(b) = eval_operand(witness, &constraint.b);
51	let Word(lo) = eval_operand(witness, &constraint.lo);
52	let Word(hi) = eval_operand(witness, &constraint.hi);
53
54	let a_val = a as u128;
55	let b_val = b as u128;
56	let product = a_val * b_val;
57
58	let expected_lo = (product & 0xFFFFFFFFFFFFFFFF) as u64;
59	let expected_hi = (product >> 64) as u64;
60
61	if lo != expected_lo || hi != expected_hi {
62		Err(format!(
63			"MUL constraint failed: {a:016x} * {b:016x} = {hi:016x}{lo:016x} (expected {expected_hi:016x}{expected_lo:016x})",
64		))
65	} else {
66		Ok(())
67	}
68}
69
70/// Verifies all constraints in a constraint system are satisfied by the witness
71pub fn verify_constraints(cs: &ConstraintSystem, witness: &ValueVec) -> Result<(), String> {
72	cs.value_vec_layout
73		.validate()
74		.map_err(|e| format!("ValueVec layout validation failed: {e}"))?;
75
76	// First check that the witness correctly populated the constants section.
77	for (index, constant) in cs.constants.iter().enumerate() {
78		if witness.get(index) != *constant {
79			return Err(format!(
80				"Constant at index {index} does not match expected value {:016x} in value vec",
81				constant.as_u64()
82			));
83		}
84	}
85	for (i, constraint) in cs.and_constraints.iter().enumerate() {
86		verify_and_constraint(witness, constraint)
87			.map_err(|e| format!("AND constraint {i} failed: {e}"))?;
88	}
89	for (i, constraint) in cs.mul_constraints.iter().enumerate() {
90		verify_mul_constraint(witness, constraint)
91			.map_err(|e| format!("MUL constraint {i} failed: {e}"))?;
92	}
93	Ok(())
94}
binius_core/verify.rs

binius_core/
verify.rs
