halo2_proofs/circuit/floor_planner/
v1.rs

1use std::fmt;
2
3use ff::Field;
4
5use crate::{
6    circuit::{
7        floor_planner::single_pass::SimpleTableLayouter,
8        layouter::{RegionColumn, RegionLayouter, RegionShape, TableLayouter},
9        Cell, Layouter, Region, RegionIndex, RegionStart, Table,
10    },
11    plonk::{
12        Advice, Any, Assigned, Assignment, Circuit, Column, Error, Fixed, FloorPlanner, Instance,
13        Selector, TableColumn,
14    },
15};
16
17mod strategy;
18
19/// The version 1 [`FloorPlanner`] provided by `halo2`.
20///
21/// - No column optimizations are performed. Circuit configuration is left entirely to the
22///   circuit designer.
23/// - A dual-pass layouter is used to measures regions prior to assignment.
24/// - Regions are measured as rectangles, bounded on the cells they assign.
25/// - Regions are laid out using a greedy first-fit strategy, after sorting regions by
26///   their "advice area" (number of advice columns * rows).
27#[derive(Debug)]
28pub struct V1;
29
30struct V1Plan<'a, F: Field, CS: Assignment<F> + 'a> {
31    cs: &'a mut CS,
32    /// Stores the starting row for each region.
33    regions: Vec<RegionStart>,
34    /// Stores the constants to be assigned, and the cells to which they are copied.
35    constants: Vec<(Assigned<F>, Cell)>,
36    /// Stores the table fixed columns.
37    table_columns: Vec<TableColumn>,
38}
39
40impl<'a, F: Field, CS: Assignment<F> + 'a> fmt::Debug for V1Plan<'a, F, CS> {
41    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
42        f.debug_struct("floor_planner::V1Plan").finish()
43    }
44}
45
46impl<'a, F: Field, CS: Assignment<F>> V1Plan<'a, F, CS> {
47    /// Creates a new v1 layouter.
48    pub fn new(cs: &'a mut CS) -> Result<Self, Error> {
49        let ret = V1Plan {
50            cs,
51            regions: vec![],
52            constants: vec![],
53            table_columns: vec![],
54        };
55        Ok(ret)
56    }
57}
58
59impl FloorPlanner for V1 {
60    fn synthesize<F: Field, CS: Assignment<F>, C: Circuit<F>>(
61        cs: &mut CS,
62        circuit: &C,
63        config: C::Config,
64        constants: Vec<Column<Fixed>>,
65    ) -> Result<(), Error> {
66        let mut plan = V1Plan::new(cs)?;
67
68        // First pass: measure the regions within the circuit.
69        let mut measure = MeasurementPass::new();
70        {
71            let pass = &mut measure;
72            circuit
73                .without_witnesses()
74                .synthesize(config.clone(), V1Pass::<_, CS>::measure(pass))?;
75        }
76
77        // Planning:
78        // - Position the regions.
79        let (regions, column_allocations) = strategy::slot_in_biggest_advice_first(measure.regions);
80        plan.regions = regions;
81
82        // - Determine how many rows our planned circuit will require.
83        let first_unassigned_row = column_allocations
84            .iter()
85            .map(|(_, a)| a.unbounded_interval_start())
86            .max()
87            .unwrap_or(0);
88
89        // - Position the constants within those rows.
90        let fixed_allocations: Vec<_> = constants
91            .into_iter()
92            .map(|c| {
93                (
94                    c,
95                    column_allocations
96                        .get(&Column::<Any>::from(c).into())
97                        .cloned()
98                        .unwrap_or_default(),
99                )
100            })
101            .collect();
102        let constant_positions = || {
103            fixed_allocations.iter().flat_map(|(c, a)| {
104                let c = *c;
105                a.free_intervals(0, Some(first_unassigned_row))
106                    .flat_map(move |e| e.range().unwrap().map(move |i| (c, i)))
107            })
108        };
109
110        // Second pass:
111        // - Assign the regions.
112        let mut assign = AssignmentPass::new(&mut plan);
113        {
114            let pass = &mut assign;
115            circuit.synthesize(config, V1Pass::assign(pass))?;
116        }
117
118        // - Assign the constants.
119        if constant_positions().count() < plan.constants.len() {
120            return Err(Error::NotEnoughColumnsForConstants);
121        }
122        for ((fixed_column, fixed_row), (value, advice)) in
123            constant_positions().zip(plan.constants.into_iter())
124        {
125            plan.cs.assign_fixed(
126                || format!("Constant({:?})", value.evaluate()),
127                fixed_column,
128                fixed_row,
129                || Ok(value),
130            )?;
131            plan.cs.copy(
132                fixed_column.into(),
133                fixed_row,
134                advice.column,
135                *plan.regions[*advice.region_index] + advice.row_offset,
136            )?;
137        }
138
139        Ok(())
140    }
141}
142
143#[derive(Debug)]
144enum Pass<'p, 'a, F: Field, CS: Assignment<F> + 'a> {
145    Measurement(&'p mut MeasurementPass),
146    Assignment(&'p mut AssignmentPass<'p, 'a, F, CS>),
147}
148
149/// A single pass of the [`V1`] layouter.
150#[derive(Debug)]
151pub struct V1Pass<'p, 'a, F: Field, CS: Assignment<F> + 'a>(Pass<'p, 'a, F, CS>);
152
153impl<'p, 'a, F: Field, CS: Assignment<F> + 'a> V1Pass<'p, 'a, F, CS> {
154    fn measure(pass: &'p mut MeasurementPass) -> Self {
155        V1Pass(Pass::Measurement(pass))
156    }
157
158    fn assign(pass: &'p mut AssignmentPass<'p, 'a, F, CS>) -> Self {
159        V1Pass(Pass::Assignment(pass))
160    }
161}
162
163impl<'p, 'a, F: Field, CS: Assignment<F> + 'a> Layouter<F> for V1Pass<'p, 'a, F, CS> {
164    type Root = Self;
165
166    fn assign_region<A, AR, N, NR>(&mut self, name: N, assignment: A) -> Result<AR, Error>
167    where
168        A: FnMut(Region<'_, F>) -> Result<AR, Error>,
169        N: Fn() -> NR,
170        NR: Into<String>,
171    {
172        match &mut self.0 {
173            Pass::Measurement(pass) => pass.assign_region(assignment),
174            Pass::Assignment(pass) => pass.assign_region(name, assignment),
175        }
176    }
177
178    fn assign_table<A, N, NR>(&mut self, name: N, assignment: A) -> Result<(), Error>
179    where
180        A: FnMut(Table<'_, F>) -> Result<(), Error>,
181        N: Fn() -> NR,
182        NR: Into<String>,
183    {
184        match &mut self.0 {
185            Pass::Measurement(_) => Ok(()),
186            Pass::Assignment(pass) => pass.assign_table(name, assignment),
187        }
188    }
189
190    fn constrain_instance(
191        &mut self,
192        cell: Cell,
193        instance: Column<Instance>,
194        row: usize,
195    ) -> Result<(), Error> {
196        match &mut self.0 {
197            Pass::Measurement(_) => Ok(()),
198            Pass::Assignment(pass) => pass.constrain_instance(cell, instance, row),
199        }
200    }
201
202    fn get_root(&mut self) -> &mut Self::Root {
203        self
204    }
205
206    fn push_namespace<NR, N>(&mut self, name_fn: N)
207    where
208        NR: Into<String>,
209        N: FnOnce() -> NR,
210    {
211        if let Pass::Assignment(pass) = &mut self.0 {
212            pass.plan.cs.push_namespace(name_fn);
213        }
214    }
215
216    fn pop_namespace(&mut self, gadget_name: Option<String>) {
217        if let Pass::Assignment(pass) = &mut self.0 {
218            pass.plan.cs.pop_namespace(gadget_name);
219        }
220    }
221}
222
223/// Measures the circuit.
224#[derive(Debug)]
225pub struct MeasurementPass {
226    regions: Vec<RegionShape>,
227}
228
229impl MeasurementPass {
230    fn new() -> Self {
231        MeasurementPass { regions: vec![] }
232    }
233
234    fn assign_region<F: Field, A, AR>(&mut self, mut assignment: A) -> Result<AR, Error>
235    where
236        A: FnMut(Region<'_, F>) -> Result<AR, Error>,
237    {
238        let region_index = self.regions.len();
239
240        // Get shape of the region.
241        let mut shape = RegionShape::new(region_index.into());
242        let result = {
243            let region: &mut dyn RegionLayouter<F> = &mut shape;
244            assignment(region.into())
245        }?;
246        self.regions.push(shape);
247
248        Ok(result)
249    }
250}
251
252/// Assigns the circuit.
253#[derive(Debug)]
254pub struct AssignmentPass<'p, 'a, F: Field, CS: Assignment<F> + 'a> {
255    plan: &'p mut V1Plan<'a, F, CS>,
256    /// Counter tracking which region we need to assign next.
257    region_index: usize,
258}
259
260impl<'p, 'a, F: Field, CS: Assignment<F> + 'a> AssignmentPass<'p, 'a, F, CS> {
261    fn new(plan: &'p mut V1Plan<'a, F, CS>) -> Self {
262        AssignmentPass {
263            plan,
264            region_index: 0,
265        }
266    }
267
268    fn assign_region<A, AR, N, NR>(&mut self, name: N, mut assignment: A) -> Result<AR, Error>
269    where
270        A: FnMut(Region<'_, F>) -> Result<AR, Error>,
271        N: Fn() -> NR,
272        NR: Into<String>,
273    {
274        // Get the next region we are assigning.
275        let region_index = self.region_index;
276        self.region_index += 1;
277
278        self.plan.cs.enter_region(name);
279        let mut region = V1Region::new(self.plan, region_index.into());
280        let result = {
281            let region: &mut dyn RegionLayouter<F> = &mut region;
282            assignment(region.into())
283        }?;
284        self.plan.cs.exit_region();
285
286        Ok(result)
287    }
288
289    fn assign_table<A, AR, N, NR>(&mut self, name: N, mut assignment: A) -> Result<AR, Error>
290    where
291        A: FnMut(Table<'_, F>) -> Result<AR, Error>,
292        N: Fn() -> NR,
293        NR: Into<String>,
294    {
295        // Maintenance hazard: there is near-duplicate code in `SingleChipLayouter::assign_table`.
296
297        // Assign table cells.
298        self.plan.cs.enter_region(name);
299        let mut table = SimpleTableLayouter::new(self.plan.cs, &self.plan.table_columns);
300        let result = {
301            let table: &mut dyn TableLayouter<F> = &mut table;
302            assignment(table.into())
303        }?;
304        let default_and_assigned = table.default_and_assigned;
305        self.plan.cs.exit_region();
306
307        // Check that all table columns have the same length `first_unused`,
308        // and all cells up to that length are assigned.
309        let first_unused = {
310            match default_and_assigned
311                .values()
312                .map(|(_, assigned)| {
313                    if assigned.iter().all(|b| *b) {
314                        Some(assigned.len())
315                    } else {
316                        None
317                    }
318                })
319                .reduce(|acc, item| match (acc, item) {
320                    (Some(a), Some(b)) if a == b => Some(a),
321                    _ => None,
322                }) {
323                Some(Some(len)) => len,
324                _ => return Err(Error::Synthesis), // TODO better error
325            }
326        };
327
328        // Record these columns so that we can prevent them from being used again.
329        for column in default_and_assigned.keys() {
330            self.plan.table_columns.push(*column);
331        }
332
333        for (col, (default_val, _)) in default_and_assigned {
334            // default_val must be Some because we must have assigned
335            // at least one cell in each column, and in that case we checked
336            // that all cells up to first_unused were assigned.
337            self.plan
338                .cs
339                .fill_from_row(col.inner(), first_unused, default_val.unwrap())?;
340        }
341
342        Ok(result)
343    }
344
345    fn constrain_instance(
346        &mut self,
347        cell: Cell,
348        instance: Column<Instance>,
349        row: usize,
350    ) -> Result<(), Error> {
351        self.plan.cs.copy(
352            cell.column,
353            *self.plan.regions[*cell.region_index] + cell.row_offset,
354            instance.into(),
355            row,
356        )
357    }
358}
359
360struct V1Region<'r, 'a, F: Field, CS: Assignment<F> + 'a> {
361    plan: &'r mut V1Plan<'a, F, CS>,
362    region_index: RegionIndex,
363}
364
365impl<'r, 'a, F: Field, CS: Assignment<F> + 'a> fmt::Debug for V1Region<'r, 'a, F, CS> {
366    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
367        f.debug_struct("V1Region")
368            .field("plan", &self.plan)
369            .field("region_index", &self.region_index)
370            .finish()
371    }
372}
373
374impl<'r, 'a, F: Field, CS: Assignment<F> + 'a> V1Region<'r, 'a, F, CS> {
375    fn new(plan: &'r mut V1Plan<'a, F, CS>, region_index: RegionIndex) -> Self {
376        V1Region { plan, region_index }
377    }
378}
379
380impl<'r, 'a, F: Field, CS: Assignment<F> + 'a> RegionLayouter<F> for V1Region<'r, 'a, F, CS> {
381    fn enable_selector<'v>(
382        &'v mut self,
383        annotation: &'v (dyn Fn() -> String + 'v),
384        selector: &Selector,
385        offset: usize,
386    ) -> Result<(), Error> {
387        self.plan.cs.enable_selector(
388            annotation,
389            selector,
390            *self.plan.regions[*self.region_index] + offset,
391        )
392    }
393
394    fn assign_advice<'v>(
395        &'v mut self,
396        annotation: &'v (dyn Fn() -> String + 'v),
397        column: Column<Advice>,
398        offset: usize,
399        to: &'v mut (dyn FnMut() -> Result<Assigned<F>, Error> + 'v),
400    ) -> Result<Cell, Error> {
401        self.plan.cs.assign_advice(
402            annotation,
403            column,
404            *self.plan.regions[*self.region_index] + offset,
405            to,
406        )?;
407
408        Ok(Cell {
409            region_index: self.region_index,
410            row_offset: offset,
411            column: column.into(),
412        })
413    }
414
415    fn assign_advice_from_constant<'v>(
416        &'v mut self,
417        annotation: &'v (dyn Fn() -> String + 'v),
418        column: Column<Advice>,
419        offset: usize,
420        constant: Assigned<F>,
421    ) -> Result<Cell, Error> {
422        let advice = self.assign_advice(annotation, column, offset, &mut || Ok(constant))?;
423        self.constrain_constant(advice, constant)?;
424
425        Ok(advice)
426    }
427
428    fn assign_advice_from_instance<'v>(
429        &mut self,
430        annotation: &'v (dyn Fn() -> String + 'v),
431        instance: Column<Instance>,
432        row: usize,
433        advice: Column<Advice>,
434        offset: usize,
435    ) -> Result<(Cell, Option<F>), Error> {
436        let value = self.plan.cs.query_instance(instance, row)?;
437
438        let cell = self.assign_advice(annotation, advice, offset, &mut || {
439            value.ok_or(Error::Synthesis).map(|v| v.into())
440        })?;
441
442        self.plan.cs.copy(
443            cell.column,
444            *self.plan.regions[*cell.region_index] + cell.row_offset,
445            instance.into(),
446            row,
447        )?;
448
449        Ok((cell, value))
450    }
451
452    fn assign_fixed<'v>(
453        &'v mut self,
454        annotation: &'v (dyn Fn() -> String + 'v),
455        column: Column<Fixed>,
456        offset: usize,
457        to: &'v mut (dyn FnMut() -> Result<Assigned<F>, Error> + 'v),
458    ) -> Result<Cell, Error> {
459        self.plan.cs.assign_fixed(
460            annotation,
461            column,
462            *self.plan.regions[*self.region_index] + offset,
463            to,
464        )?;
465
466        Ok(Cell {
467            region_index: self.region_index,
468            row_offset: offset,
469            column: column.into(),
470        })
471    }
472
473    fn constrain_constant(&mut self, cell: Cell, constant: Assigned<F>) -> Result<(), Error> {
474        self.plan.constants.push((constant, cell));
475        Ok(())
476    }
477
478    fn constrain_equal(&mut self, left: Cell, right: Cell) -> Result<(), Error> {
479        self.plan.cs.copy(
480            left.column,
481            *self.plan.regions[*left.region_index] + left.row_offset,
482            right.column,
483            *self.plan.regions[*right.region_index] + right.row_offset,
484        )?;
485
486        Ok(())
487    }
488}
489
490#[cfg(test)]
491mod tests {
492    use pasta_curves::vesta;
493
494    use crate::{
495        dev::MockProver,
496        plonk::{Advice, Circuit, Column, Error},
497    };
498
499    #[test]
500    fn not_enough_columns_for_constants() {
501        struct MyCircuit {}
502
503        impl Circuit<vesta::Scalar> for MyCircuit {
504            type Config = Column<Advice>;
505            type FloorPlanner = super::V1;
506
507            fn without_witnesses(&self) -> Self {
508                MyCircuit {}
509            }
510
511            fn configure(meta: &mut crate::plonk::ConstraintSystem<vesta::Scalar>) -> Self::Config {
512                meta.advice_column()
513            }
514
515            fn synthesize(
516                &self,
517                config: Self::Config,
518                mut layouter: impl crate::circuit::Layouter<vesta::Scalar>,
519            ) -> Result<(), crate::plonk::Error> {
520                layouter.assign_region(
521                    || "assign constant",
522                    |mut region| {
523                        region.assign_advice_from_constant(
524                            || "one",
525                            config,
526                            0,
527                            vesta::Scalar::one(),
528                        )
529                    },
530                )?;
531
532                Ok(())
533            }
534        }
535
536        let circuit = MyCircuit {};
537        assert!(matches!(
538            MockProver::run(3, &circuit, vec![]).unwrap_err(),
539            Error::NotEnoughColumnsForConstants,
540        ));
541    }
542}