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::{AndConstraint, ConstraintSystem, ImulConstraint, ValueIndex, ValueVec},
8	word::Word,
9};
10
11/// Verifies that an AND constraint is satisfied: (A & B) ^ C = 0
12pub fn verify_and_constraint(witness: &ValueVec, constraint: &AndConstraint) -> Result<(), String> {
13	let Word(a) = witness.eval_operand(constraint.a());
14	let Word(b) = witness.eval_operand(constraint.b());
15	let Word(c) = witness.eval_operand(constraint.c());
16
17	let result = (a & b) ^ c;
18	if result != 0 {
19		Err(format!(
20			"AND constraint failed: ({a:016x} & {b:016x}) ^ {c:016x} = {result:016x} (expected 0)",
21		))
22	} else {
23		Ok(())
24	}
25}
26
27/// Verifies that an IMUL constraint is satisfied: A * B = (HI << 64) | LO
28pub fn verify_imul_constraint(
29	witness: &ValueVec,
30	constraint: &ImulConstraint,
31) -> Result<(), String> {
32	let Word(a) = witness.eval_operand(constraint.a());
33	let Word(b) = witness.eval_operand(constraint.b());
34	let Word(lo) = witness.eval_operand(constraint.lo());
35	let Word(hi) = witness.eval_operand(constraint.hi());
36
37	let a_val = a as u128;
38	let b_val = b as u128;
39	let product = a_val * b_val;
40
41	let expected_lo = (product & 0xFFFFFFFFFFFFFFFF) as u64;
42	let expected_hi = (product >> 64) as u64;
43
44	if lo != expected_lo || hi != expected_hi {
45		Err(format!(
46			"IMUL constraint failed: {a:016x} * {b:016x} = {hi:016x}{lo:016x} (expected {expected_hi:016x}{expected_lo:016x})",
47		))
48	} else {
49		Ok(())
50	}
51}
52
53/// Verifies all constraints in a constraint system are satisfied by the witness
54pub fn verify_constraints(cs: &ConstraintSystem, witness: &ValueVec) -> Result<(), String> {
55	cs.value_vec_layout
56		.validate()
57		.map_err(|e| format!("ValueVec layout validation failed: {e}"))?;
58
59	// First check that the witness correctly populated the constants section.
60	for (index, constant) in cs.constants.iter().enumerate() {
61		if witness[ValueIndex(index as u32)] != *constant {
62			return Err(format!(
63				"Constant at index {index} does not match expected value {:016x} in value vec",
64				constant.as_u64()
65			));
66		}
67	}
68	for (i, constraint) in cs.and_constraints.iter().enumerate() {
69		verify_and_constraint(witness, constraint)
70			.map_err(|e| format!("AND constraint {i} failed: {e}"))?;
71	}
72	for (i, constraint) in cs.imul_constraints.iter().enumerate() {
73		verify_imul_constraint(witness, constraint)
74			.map_err(|e| format!("IMUL constraint {i} failed: {e}"))?;
75	}
76	Ok(())
77}
binius_core/verify.rs

binius_core/
verify.rs
