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 given a word
14#[inline]
15pub fn eval_shifted_word(word: Word, shift_variant: ShiftVariant, amount: usize) -> Word {
16	match shift_variant {
17		ShiftVariant::Sll => word << (amount as u32),
18		ShiftVariant::Slr => word >> (amount as u32),
19		ShiftVariant::Sar => word.sar(amount as u32),
20		ShiftVariant::Rotr => word.rotr(amount as u32),
21		ShiftVariant::Sll32 => word.sll32(amount as u32),
22		ShiftVariant::Srl32 => word.srl32(amount as u32),
23		ShiftVariant::Sra32 => word.sra32(amount as u32),
24		ShiftVariant::Rotr32 => word.rotr32(amount as u32),
25	}
26}
27
28/// Evaluates an operand (XOR of shifted values) using a ValueVec
29#[inline]
30pub fn eval_operand(witness: &ValueVec, operand: &[ShiftedValueIndex]) -> Word {
31	operand.iter().fold(Word::ZERO, |acc, sv| {
32		let word = witness[sv.value_index];
33		let shifted_word = eval_shifted_word(word, sv.shift_variant, sv.amount);
34		acc ^ shifted_word
35	})
36}
37
38/// Verifies that an AND constraint is satisfied: (A & B) ^ C = 0
39pub fn verify_and_constraint(witness: &ValueVec, constraint: &AndConstraint) -> Result<(), String> {
40	let Word(a) = eval_operand(witness, &constraint.a);
41	let Word(b) = eval_operand(witness, &constraint.b);
42	let Word(c) = eval_operand(witness, &constraint.c);
43
44	let result = (a & b) ^ c;
45	if result != 0 {
46		Err(format!(
47			"AND constraint failed: ({a:016x} & {b:016x}) ^ {c:016x} = {result:016x} (expected 0)",
48		))
49	} else {
50		Ok(())
51	}
52}
53
54/// Verifies that a MUL constraint is satisfied: A * B = (HI << 64) | LO
55pub fn verify_mul_constraint(witness: &ValueVec, constraint: &MulConstraint) -> Result<(), String> {
56	let Word(a) = eval_operand(witness, &constraint.a);
57	let Word(b) = eval_operand(witness, &constraint.b);
58	let Word(lo) = eval_operand(witness, &constraint.lo);
59	let Word(hi) = eval_operand(witness, &constraint.hi);
60
61	let a_val = a as u128;
62	let b_val = b as u128;
63	let product = a_val * b_val;
64
65	let expected_lo = (product & 0xFFFFFFFFFFFFFFFF) as u64;
66	let expected_hi = (product >> 64) as u64;
67
68	if lo != expected_lo || hi != expected_hi {
69		Err(format!(
70			"MUL constraint failed: {a:016x} * {b:016x} = {hi:016x}{lo:016x} (expected {expected_hi:016x}{expected_lo:016x})",
71		))
72	} else {
73		Ok(())
74	}
75}
76
77/// Verifies all constraints in a constraint system are satisfied by the witness
78pub fn verify_constraints(cs: &ConstraintSystem, witness: &ValueVec) -> Result<(), String> {
79	cs.value_vec_layout
80		.validate()
81		.map_err(|e| format!("ValueVec layout validation failed: {e}"))?;
82
83	// First check that the witness correctly populated the constants section.
84	for (index, constant) in cs.constants.iter().enumerate() {
85		if witness.get(index) != *constant {
86			return Err(format!(
87				"Constant at index {index} does not match expected value {:016x} in value vec",
88				constant.as_u64()
89			));
90		}
91	}
92	for (i, constraint) in cs.and_constraints.iter().enumerate() {
93		verify_and_constraint(witness, constraint)
94			.map_err(|e| format!("AND constraint {i} failed: {e}"))?;
95	}
96	for (i, constraint) in cs.mul_constraints.iter().enumerate() {
97		verify_mul_constraint(witness, constraint)
98			.map_err(|e| format!("MUL constraint {i} failed: {e}"))?;
99	}
100	Ok(())
101}
binius_core/verify.rs

binius_core/
verify.rs
