halo2_axiom/dev/gates.rs
1use std::{
2 collections::BTreeSet,
3 fmt::{self, Write},
4};
5
6use ff::PrimeField;
7
8use crate::{
9 dev::util,
10 plonk::{sealed::SealedPhase, Circuit, ConstraintSystem, FirstPhase},
11};
12
13#[derive(Debug)]
14struct Constraint {
15 name: String,
16 expression: String,
17 queries: BTreeSet<String>,
18}
19
20#[derive(Debug)]
21struct Gate {
22 name: String,
23 constraints: Vec<Constraint>,
24}
25
26/// A struct for collecting and displaying the gates within a circuit.
27///
28/// # Examples
29///
30/// ```
31/// use ff::Field;
32/// use halo2_axiom::{
33/// circuit::{Layouter, SimpleFloorPlanner},
34/// dev::CircuitGates,
35/// plonk::{Circuit, ConstraintSystem, Error},
36/// poly::Rotation,
37/// };
38/// use halo2curves::pasta::pallas;
39///
40/// #[derive(Copy, Clone)]
41/// struct MyConfig {}
42///
43/// #[derive(Clone, Default)]
44/// struct MyCircuit {}
45///
46/// impl<F: Field> Circuit<F> for MyCircuit {
47/// type Config = MyConfig;
48/// type FloorPlanner = SimpleFloorPlanner;
49/// #[cfg(feature = "circuit-params")]
50/// type Params = ();
51///
52/// fn without_witnesses(&self) -> Self {
53/// Self::default()
54/// }
55///
56/// fn configure(meta: &mut ConstraintSystem<F>) -> MyConfig {
57/// let a = meta.advice_column();
58/// let b = meta.advice_column();
59/// let c = meta.advice_column();
60/// let s = meta.selector();
61///
62/// meta.create_gate("R1CS constraint", |meta| {
63/// let a = meta.query_advice(a, Rotation::cur());
64/// let b = meta.query_advice(b, Rotation::cur());
65/// let c = meta.query_advice(c, Rotation::cur());
66/// let s = meta.query_selector(s);
67///
68/// Some(("R1CS", s * (a * b - c)))
69/// });
70///
71/// // We aren't using this circuit for anything in this example.
72/// MyConfig {}
73/// }
74///
75/// fn synthesize(&self, _: MyConfig, _: impl Layouter<F>) -> Result<(), Error> {
76/// // Gates are known at configure time; it doesn't matter how we use them.
77/// Ok(())
78/// }
79/// }
80///
81/// #[cfg(feature = "circuit-params")]
82/// let gates = CircuitGates::collect::<pallas::Base, MyCircuit>(());
83/// #[cfg(not(feature = "circuit-params"))]
84/// let gates = CircuitGates::collect::<pallas::Base, MyCircuit>();
85/// assert_eq!(
86/// format!("{}", gates),
87/// r#####"R1CS constraint:
88/// - R1CS:
89/// S0 * (A0@0 * A1@0 - A2@0)
90/// Total gates: 1
91/// Total custom constraint polynomials: 1
92/// Total negations: 1
93/// Total additions: 1
94/// Total multiplications: 2
95/// "#####,
96/// );
97/// ```
98#[derive(Debug)]
99pub struct CircuitGates {
100 gates: Vec<Gate>,
101 total_negations: usize,
102 total_additions: usize,
103 total_multiplications: usize,
104}
105
106impl CircuitGates {
107 /// Collects the gates from within the circuit.
108 pub fn collect<F: PrimeField, C: Circuit<F>>(
109 #[cfg(feature = "circuit-params")] params: C::Params,
110 ) -> Self {
111 // Collect the graph details.
112 let mut cs = ConstraintSystem::default();
113 #[cfg(feature = "circuit-params")]
114 let _ = C::configure_with_params(&mut cs, params);
115 #[cfg(not(feature = "circuit-params"))]
116 let _ = C::configure(&mut cs);
117
118 let gates = cs
119 .gates
120 .iter()
121 .map(|gate| Gate {
122 name: gate.name().to_string(),
123 constraints: gate
124 .polynomials()
125 .iter()
126 .enumerate()
127 .map(|(i, constraint)| Constraint {
128 name: gate.constraint_name(i).to_string(),
129 expression: constraint.evaluate(
130 &util::format_value,
131 &|selector| format!("S{}", selector.0),
132 &|query| format!("F{}@{}", query.column_index, query.rotation.0),
133 &|query| {
134 if query.phase == FirstPhase.to_sealed() {
135 format!("A{}@{}", query.column_index, query.rotation.0)
136 } else {
137 format!(
138 "A{}({})@{}",
139 query.column_index,
140 query.phase(),
141 query.rotation.0
142 )
143 }
144 },
145 &|query| format!("I{}@{}", query.column_index, query.rotation.0),
146 &|challenge| format!("C{}({})", challenge.index(), challenge.phase()),
147 &|a| {
148 if a.contains(' ') {
149 format!("-({})", a)
150 } else {
151 format!("-{}", a)
152 }
153 },
154 &|a, b| {
155 if let Some(b) = b.strip_prefix('-') {
156 format!("{} - {}", a, b)
157 } else {
158 format!("{} + {}", a, b)
159 }
160 },
161 &|a, b| match (a.contains(' '), b.contains(' ')) {
162 (false, false) => format!("{} * {}", a, b),
163 (false, true) => format!("{} * ({})", a, b),
164 (true, false) => format!("({}) * {}", a, b),
165 (true, true) => format!("({}) * ({})", a, b),
166 },
167 &|a, s| {
168 if a.contains(' ') {
169 format!("({}) * {}", a, util::format_value(s))
170 } else {
171 format!("{} * {}", a, util::format_value(s))
172 }
173 },
174 ),
175 queries: constraint.evaluate(
176 &|_| BTreeSet::default(),
177 &|selector| vec![format!("S{}", selector.0)].into_iter().collect(),
178 &|query| {
179 vec![format!("F{}@{}", query.column_index, query.rotation.0)]
180 .into_iter()
181 .collect()
182 },
183 &|query| {
184 let query = if query.phase == FirstPhase.to_sealed() {
185 format!("A{}@{}", query.column_index, query.rotation.0)
186 } else {
187 format!(
188 "A{}({})@{}",
189 query.column_index,
190 query.phase(),
191 query.rotation.0
192 )
193 };
194 vec![query].into_iter().collect()
195 },
196 &|query| {
197 vec![format!("I{}@{}", query.column_index, query.rotation.0)]
198 .into_iter()
199 .collect()
200 },
201 &|challenge| {
202 vec![format!("C{}({})", challenge.index(), challenge.phase())]
203 .into_iter()
204 .collect()
205 },
206 &|a| a,
207 &|mut a, mut b| {
208 a.append(&mut b);
209 a
210 },
211 &|mut a, mut b| {
212 a.append(&mut b);
213 a
214 },
215 &|a, _| a,
216 ),
217 })
218 .collect(),
219 })
220 .collect();
221
222 let (total_negations, total_additions, total_multiplications) = cs
223 .gates
224 .iter()
225 .flat_map(|gate| {
226 gate.polynomials().iter().map(|poly| {
227 poly.evaluate(
228 &|_| (0, 0, 0),
229 &|_| (0, 0, 0),
230 &|_| (0, 0, 0),
231 &|_| (0, 0, 0),
232 &|_| (0, 0, 0),
233 &|_| (0, 0, 0),
234 &|(a_n, a_a, a_m)| (a_n + 1, a_a, a_m),
235 &|(a_n, a_a, a_m), (b_n, b_a, b_m)| (a_n + b_n, a_a + b_a + 1, a_m + b_m),
236 &|(a_n, a_a, a_m), (b_n, b_a, b_m)| (a_n + b_n, a_a + b_a, a_m + b_m + 1),
237 &|(a_n, a_a, a_m), _| (a_n, a_a, a_m + 1),
238 )
239 })
240 })
241 .fold((0, 0, 0), |(acc_n, acc_a, acc_m), (n, a, m)| {
242 (acc_n + n, acc_a + a, acc_m + m)
243 });
244
245 CircuitGates {
246 gates,
247 total_negations,
248 total_additions,
249 total_multiplications,
250 }
251 }
252
253 /// Prints the queries in this circuit to a CSV grid.
254 pub fn queries_to_csv(&self) -> String {
255 let mut queries = BTreeSet::new();
256 for gate in &self.gates {
257 for constraint in &gate.constraints {
258 for query in &constraint.queries {
259 queries.insert(query);
260 }
261 }
262 }
263
264 let mut ret = String::new();
265 let w = &mut ret;
266 for query in &queries {
267 write!(w, "{},", query).unwrap();
268 }
269 writeln!(w, "Name").unwrap();
270
271 for gate in &self.gates {
272 for constraint in &gate.constraints {
273 for query in &queries {
274 if constraint.queries.contains(*query) {
275 write!(w, "1").unwrap();
276 } else {
277 write!(w, "0").unwrap();
278 }
279 write!(w, ",").unwrap();
280 }
281 writeln!(w, "{}/{}", gate.name, constraint.name).unwrap();
282 }
283 }
284 ret
285 }
286}
287
288impl fmt::Display for CircuitGates {
289 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> Result<(), fmt::Error> {
290 for gate in &self.gates {
291 writeln!(f, "{}:", gate.name)?;
292 for constraint in &gate.constraints {
293 if constraint.name.is_empty() {
294 writeln!(f, "- {}", constraint.expression)?;
295 } else {
296 writeln!(f, "- {}:", constraint.name)?;
297 writeln!(f, " {}", constraint.expression)?;
298 }
299 }
300 }
301 writeln!(f, "Total gates: {}", self.gates.len())?;
302 writeln!(
303 f,
304 "Total custom constraint polynomials: {}",
305 self.gates
306 .iter()
307 .map(|gate| gate.constraints.len())
308 .sum::<usize>()
309 )?;
310 writeln!(f, "Total negations: {}", self.total_negations)?;
311 writeln!(f, "Total additions: {}", self.total_additions)?;
312 writeln!(f, "Total multiplications: {}", self.total_multiplications)
313 }
314}