binius_spartan_verifier/wrapper/
builder_channel.rs

1// Copyright 2026 The Binius Developers
2
3//! [`IronSpartanBuilderChannel`]: an [`IPVerifierChannel`] that symbolically executes a verifier
4//! and records the computation as constraints on a [`ConstraintBuilder`].
5
6use std::{
7	cell::RefCell,
8	rc::{Rc, Weak},
9};
10
11use binius_core::word::Word;
12use binius_field::{BinaryField, Field};
13use binius_iop::channel::{IOPVerifierChannel, OracleSpec, TransparentEvalFn};
14use binius_ip::channel::{
15	IPVerifierChannel, WordIPVerifierChannel, n_packed_elems, select_word, subset_sum_word,
16};
17use binius_spartan_frontend::circuit_builder::{CircuitBuilder, ConstraintBuilder};
18
19use super::circuit_elem::CircuitElem;
20
21/// A channel that symbolically executes a verifier, building up an IronSpartan constraint system.
22///
23/// Instead of performing actual verification, this channel records all operations as constraints
24/// in a [`ConstraintBuilder`]. The typical usage pattern is:
25///
26/// 1. Construct a fresh [`IronSpartanBuilderChannel`] via [`Self::new`]
27/// 2. Run the verifier on the channel (e.g., `verify_iop`)
28/// 3. The channel's `finish()` method returns the [`ConstraintBuilder`] with all recorded
29///    constraints
30pub struct IronSpartanBuilderChannel<F: Field> {
31	builder: Rc<RefCell<ConstraintBuilder<F>>>,
32}
33
34impl<F: Field> Default for IronSpartanBuilderChannel<F> {
35	fn default() -> Self {
36		Self::new()
37	}
38}
39
40impl<F: Field> IronSpartanBuilderChannel<F> {
41	/// Creates a new builder channel backed by a fresh [`ConstraintBuilder`].
42	pub fn new() -> Self {
43		Self {
44			builder: Rc::new(RefCell::new(ConstraintBuilder::new())),
45		}
46	}
47
48	fn alloc_inout_elem(&self) -> CircuitElem<F, ConstraintBuilder<F>> {
49		let wire = self.builder.borrow_mut().alloc_inout();
50		CircuitElem::wire(&self.builder, wire)
51	}
52
53	fn alloc_precommit_elem(&self) -> CircuitElem<F, ConstraintBuilder<F>> {
54		let wire = self.builder.borrow_mut().alloc_precommit();
55		CircuitElem::wire(&self.builder, wire)
56	}
57
58	/// Consumes the channel and returns the underlying [`ConstraintBuilder`].
59	///
60	/// This must be called after all `CircuitElem` values derived from this channel have been
61	/// dropped, as it requires sole ownership of the builder via `Rc::try_unwrap`.
62	pub fn finish(self) -> ConstraintBuilder<F> {
63		Rc::try_unwrap(self.builder)
64			.expect("CircuitElem values should only hold Weak references")
65			.into_inner()
66	}
67}
68
69impl<F: Field> IPVerifierChannel<F> for IronSpartanBuilderChannel<F> {
70	type Elem = CircuitElem<F, ConstraintBuilder<F>>;
71
72	fn recv_one(&mut self) -> Result<Self::Elem, binius_ip::channel::Error> {
73		// For each element that the inner prover sends, the wrapped prover allocates a one-time-pad
74		// encryption key in the precommit segment and encrypts the underlying value before sending.
75		// Here the verifier gets the encryption key from the precommit segment and decrypts.
76		let inout = self.alloc_inout_elem();
77		let key = self.alloc_precommit_elem();
78		Ok(inout - key)
79	}
80
81	fn recv_public_claim(&mut self) -> Result<Self::Elem, binius_ip::channel::Error> {
82		// A claim is public, so the wrapped prover sends it unencrypted: one inout wire, no
83		// precommit key. What it leaves behind is a public-derivable wire, which is what the
84		// checks reading it need it to be.
85		Ok(self.alloc_inout_elem())
86	}
87
88	fn sample(&mut self) -> Self::Elem {
89		self.alloc_inout_elem()
90	}
91
92	fn observe_one(&mut self, _val: F) -> Self::Elem {
93		self.alloc_inout_elem()
94	}
95
96	fn assert_zero(&mut self, val: Self::Elem) -> Result<(), binius_ip::channel::Error> {
97		match val {
98			// A compile-time constant is checked here; a non-zero one is an unsatisfiable
99			// assertion.
100			CircuitElem::Constant(c) => {
101				if c == F::ZERO {
102					Ok(())
103				} else {
104					Err(binius_ip::channel::Error::InvalidAssert)
105				}
106			}
107			// Record the assertion as a constraint over the wire (whether public-derivable or
108			// private). The outer verifier enforces it; with derived wires there is no need to
109			// special-case public values out of the constraint system.
110			CircuitElem::Wire { builder, wire } => {
111				assert!(Weak::ptr_eq(&Rc::downgrade(&self.builder), &builder));
112				self.builder.borrow_mut().assert_zero(wire);
113				Ok(())
114			}
115		}
116	}
117}
118
119impl<F: BinaryField> WordIPVerifierChannel<F> for IronSpartanBuilderChannel<F> {
120	type Word = Word;
121
122	// The outer verifier rebinds the public inputs, so the wrapper records no Fiat-Shamir state.
123	fn observe_words(&mut self, words: &[Word]) -> Vec<Word> {
124		words.to_vec()
125	}
126
127	fn subset_sum(&mut self, elems: &[Self::Elem], word: &Word) -> Self::Elem {
128		// The word is concrete, so which elements the sum runs over is settled while building.
129		subset_sum_word(elems, *word)
130	}
131
132	fn select(&mut self, elems: &[Self::Elem], word: &Word) -> Self::Elem {
133		select_word(elems, *word)
134	}
135
136	fn sample_bits(&mut self, _bits: usize) -> Word {
137		Word::ZERO
138	}
139
140	fn pack_words(&mut self, words: &[Word]) -> Vec<Self::Elem> {
141		// The words are the statement, and this circuit is built once to be reused across every
142		// statement, so the packed elements cannot be settled here: a constant would fix the
143		// statement it was built against into the circuit. They enter as inout wires instead, which
144		// `ZKWrappedVerifierChannel` and `ReplayChannel` fill with the concrete packing.
145		(0..n_packed_elems::<F>(words.len()))
146			.map(|_| self.alloc_inout_elem())
147			.collect()
148	}
149}
150
151impl<F: Field> IOPVerifierChannel<F> for IronSpartanBuilderChannel<F> {
152	type Oracle = ();
153
154	fn remaining_oracle_specs(&self) -> &[OracleSpec] {
155		&[]
156	}
157
158	fn recv_oracle(
159		&mut self,
160		_log_msg_len: usize,
161		_is_witness_dependent: bool,
162	) -> Result<Self::Oracle, binius_iop::channel::Error> {
163		Ok(())
164	}
165
166	fn verify_oracle_relation(
167		&mut self,
168		_oracle: Self::Oracle,
169		_transparent: TransparentEvalFn<Self::Elem>,
170		claim: Self::Elem,
171	) -> Result<(), binius_iop::channel::Error> {
172		// For each oracle opening, the prover sends the decrypted evaluation. The outer verifier
173		// checks in the circuit equality of this value with the expected expression over encrypted
174		// values.
175		let decrypted_claim = self.alloc_inout_elem();
176		self.assert_zero(claim - decrypted_claim)?;
177		Ok(())
178	}
179}
binius_spartan_verifier/wrapper/builder_channel.rs

binius_spartan_verifier/wrapper/
builder_channel.rs
