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

binius_core/
verify.rs
