binius_core/constraint_system/m4/
witness.rs

1// Copyright 2026 The Binius Developers
2
3//! The witness for an M4 constraint system: the main chip's values and one table per chip.
4
5use std::borrow::Cow;
6
7use super::{ChipInstances, ConstraintSystemM4};
8use crate::{ValueTable, ValueVec, error::VerificationM4Error};
9
10/// A full M4 witness: the main chip's values and one [`ValueTable`] per chip of a
11/// [`ConstraintSystemM4`].
12///
13/// The tables are indexed by chip ID, so `tables[i]` holds every instance of chip `i`. One row of a
14/// table is one invocation of that chip: the chip's local constraints must hold on the row, and the
15/// row's inout values must be matched by exactly one chip call elsewhere in the system.
16///
17/// Generating one is the circuit frontend's business, since it takes circuits to evaluate — see
18/// `CircuitM4::generate_witness`. This crate is where one is checked.
19#[derive(Debug)]
20pub struct WitnessM4 {
21	/// The values of the main chip, which runs once.
22	pub main: ValueVec,
23	/// The instances of each chip, indexed by chip ID.
24	pub tables: Vec<ValueTable>,
25}
26
27impl WitnessM4 {
28	/// Checks that this witness satisfies an M4 constraint system.
29	///
30	/// [`ConstraintSystemM4::verify`] checks the local constraints of every instance and matches
31	/// every chip call against the instance serving it. It reads the instances one at a time, so a
32	/// table is never expanded into value vectors whole: the tables are the witness, and they stay
33	/// the only copy of it.
34	pub fn verify(&self, cs: &ConstraintSystemM4) -> Result<(), VerificationM4Error> {
35		cs.verify(
36			&self.main,
37			&TableInstances {
38				tables: &self.tables,
39				cs,
40			},
41		)
42	}
43}
44
45/// A witness's tables read as chip instances, each built when it is asked for.
46///
47/// The constants are the one part of an instance a table does not store, so the system is held
48/// alongside to supply them.
49struct TableInstances<'a> {
50	tables: &'a [ValueTable],
51	cs: &'a ConstraintSystemM4,
52}
53
54impl ChipInstances for TableInstances<'_> {
55	fn n_chips(&self) -> usize {
56		self.tables.len()
57	}
58
59	fn n_instances(&self, chip_id: usize) -> usize {
60		self.tables[chip_id].n_instances()
61	}
62
63	fn instance(&self, chip_id: usize, row: usize) -> Cow<'_, ValueVec> {
64		let constants = &self.cs.chips[chip_id].0.cs.constants;
65		Cow::Owned(self.tables[chip_id].instance_value_vec(row, constants))
66	}
67}
binius_core/constraint_system/m4/witness.rs

binius_core/constraint_system/m4/
witness.rs
