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, MulConstraint, 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 a MUL constraint is satisfied: A * B = (HI << 64) | LO
28pub fn verify_mul_constraint(witness: &ValueVec, constraint: &MulConstraint) -> Result<(), String> {
29	let Word(a) = witness.eval_operand(&constraint.a);
30	let Word(b) = witness.eval_operand(&constraint.b);
31	let Word(lo) = witness.eval_operand(&constraint.lo);
32	let Word(hi) = witness.eval_operand(&constraint.hi);
33
34	let a_val = a as u128;
35	let b_val = b as u128;
36	let product = a_val * b_val;
37
38	let expected_lo = (product & 0xFFFFFFFFFFFFFFFF) as u64;
39	let expected_hi = (product >> 64) as u64;
40
41	if lo != expected_lo || hi != expected_hi {
42		Err(format!(
43			"MUL constraint failed: {a:016x} * {b:016x} = {hi:016x}{lo:016x} (expected {expected_hi:016x}{expected_lo:016x})",
44		))
45	} else {
46		Ok(())
47	}
48}
49
50/// Verifies all constraints in a constraint system are satisfied by the witness
51pub fn verify_constraints(cs: &ConstraintSystem, witness: &ValueVec) -> Result<(), String> {
52	cs.value_vec_layout
53		.validate()
54		.map_err(|e| format!("ValueVec layout validation failed: {e}"))?;
55
56	// First check that the witness correctly populated the constants section.
57	for (index, constant) in cs.constants.iter().enumerate() {
58		if witness.get(index) != *constant {
59			return Err(format!(
60				"Constant at index {index} does not match expected value {:016x} in value vec",
61				constant.as_u64()
62			));
63		}
64	}
65	for (i, constraint) in cs.and_constraints.iter().enumerate() {
66		verify_and_constraint(witness, constraint)
67			.map_err(|e| format!("AND constraint {i} failed: {e}"))?;
68	}
69	for (i, constraint) in cs.mul_constraints.iter().enumerate() {
70		verify_mul_constraint(witness, constraint)
71			.map_err(|e| format!("MUL constraint {i} failed: {e}"))?;
72	}
73	Ok(())
74}
binius_core/verify.rs

binius_core/
verify.rs
