halo2_axiom/dev/failure/
emitter.rs

Help
1use std::collections::BTreeMap;
2use std::iter;
3
4use group::ff::Field;
5
6use super::FailureLocation;
7use crate::{
8    dev::{metadata, util},
9    plonk::{Advice, Any, Expression},
10};
11
12fn padded(p: char, width: usize, text: &str) -> String {
13    let pad = width - text.len();
14
15    format!(
16        "{}{}{}",
17        iter::repeat(p).take(pad - pad / 2).collect::<String>(),
18        text,
19        iter::repeat(p).take(pad / 2).collect::<String>(),
20    )
21}
22
23fn column_type_and_idx(column: &metadata::Column) -> String {
24    format!(
25        "{}{}",
26        match column.column_type {
27            Any::Advice(_) => "A",
28            Any::Fixed => "F",
29            Any::Instance => "I",
30        },
31        column.index
32    )
33}
34
35/// Renders a cell layout around a given failure location.
36///
37/// `highlight_row` is called at the end of each row, with the offset of the active row
38/// (if `location` is in a region), and the rotation of the current row relative to the
39/// active row.
40pub(super) fn render_cell_layout(
41    prefix: &str,
42    location: &FailureLocation,
43    columns: &BTreeMap<metadata::Column, usize>,
44    layout: &BTreeMap<i32, BTreeMap<metadata::Column, String>>,
45    highlight_row: impl Fn(Option<i32>, i32),
46) {
47    let col_width = |cells: usize| cells.to_string().len() + 3;
48    let mut col_headers = String::new();
49
50    // If we are in a region, show rows at offsets relative to it. Otherwise, just show
51    // the rotations directly.
52    let offset = match location {
53        FailureLocation::InRegion { region, offset } => {
54            col_headers
55                .push_str(format!("{}Cell layout in region '{}':\n", prefix, region.name).as_str());
56            col_headers.push_str(format!("{}  | Offset |", prefix).as_str());
57            Some(*offset as i32)
58        }
59        FailureLocation::OutsideRegion { row } => {
60            col_headers.push_str(format!("{}Cell layout at row {}:\n", prefix, row).as_str());
61            col_headers.push_str(format!("{}  |Rotation|", prefix).as_str());
62            None
63        }
64    };
65    eprint!("\n{}", col_headers);
66
67    let widths: Vec<usize> = columns
68        .iter()
69        .map(|(col, _)| {
70            let size = match location {
71                FailureLocation::InRegion { region, offset: _ } => {
72                    if let Some(column_ann) = region.column_annotations.as_ref() {
73                        if let Some(ann) = column_ann.get(col) {
74                            ann.len()
75                        } else {
76                            col_width(column_type_and_idx(col).as_str().len())
77                        }
78                    } else {
79                        col_width(column_type_and_idx(col).as_str().len())
80                    }
81                }
82                FailureLocation::OutsideRegion { row: _ } => {
83                    col_width(column_type_and_idx(col).as_str().len())
84                }
85            };
86            size
87        })
88        .collect();
89
90    // Print the assigned cells, and their region offset or rotation + the column name at which they're assigned to.
91    for ((column, _), &width) in columns.iter().zip(widths.iter()) {
92        eprint!(
93            "{}|",
94            padded(
95                ' ',
96                width,
97                &match location {
98                    FailureLocation::InRegion { region, offset: _ } => {
99                        region
100                            .column_annotations
101                            .as_ref()
102                            .and_then(|column_ann| column_ann.get(column).cloned())
103                            .unwrap_or_else(|| column_type_and_idx(column))
104                    }
105                    FailureLocation::OutsideRegion { row: _ } => {
106                        column_type_and_idx(column)
107                    }
108                }
109                .to_string()
110            )
111        );
112    }
113
114    eprintln!();
115    eprint!("{}  +--------+", prefix);
116    for &width in widths.iter() {
117        eprint!("{}+", padded('-', width, ""));
118    }
119    eprintln!();
120    for (rotation, row) in layout {
121        eprint!(
122            "{}  |{}|",
123            prefix,
124            padded(' ', 8, &(offset.unwrap_or(0) + rotation).to_string())
125        );
126        for ((col, _), &width) in columns.iter().zip(widths.iter()) {
127            eprint!(
128                "{}|",
129                padded(
130                    ' ',
131                    width,
132                    row.get(col).map(|s| s.as_str()).unwrap_or_default()
133                )
134            );
135        }
136        highlight_row(offset, *rotation);
137        eprintln!();
138    }
139}
140
141pub(super) fn expression_to_string<F: Field>(
142    expr: &Expression<F>,
143    layout: &BTreeMap<i32, BTreeMap<metadata::Column, String>>,
144) -> String {
145    expr.evaluate(
146        &util::format_value,
147        &|_| panic!("virtual selectors are removed during optimization"),
148        &|query| {
149            if let Some(label) = layout
150                .get(&query.rotation.0)
151                .and_then(|row| row.get(&(Any::Fixed, query.column_index).into()))
152            {
153                label.clone()
154            } else if query.rotation.0 == 0 {
155                // This is most likely a merged selector
156                format!("S{}", query.index.unwrap())
157            } else {
158                // No idea how we'd get here...
159                format!("F{}@{}", query.column_index, query.rotation.0)
160            }
161        },
162        &|query| {
163            layout
164                .get(&query.rotation.0)
165                .and_then(|map| {
166                    map.get(
167                        &(
168                            Any::Advice(Advice { phase: query.phase }),
169                            query.column_index,
170                        )
171                            .into(),
172                    )
173                })
174                .cloned()
175                .unwrap_or_default()
176        },
177        &|query| {
178            layout
179                .get(&query.rotation.0)
180                .unwrap()
181                .get(&(Any::Instance, query.column_index).into())
182                .unwrap()
183                .clone()
184        },
185        &|challenge| format!("C{}({})", challenge.index(), challenge.phase()),
186        &|a| {
187            if a.contains(' ') {
188                format!("-({})", a)
189            } else {
190                format!("-{}", a)
191            }
192        },
193        &|a, b| {
194            if let Some(b) = b.strip_prefix('-') {
195                format!("{} - {}", a, b)
196            } else {
197                format!("{} + {}", a, b)
198            }
199        },
200        &|a, b| match (a.contains(' '), b.contains(' ')) {
201            (false, false) => format!("{} * {}", a, b),
202            (false, true) => format!("{} * ({})", a, b),
203            (true, false) => format!("({}) * {}", a, b),
204            (true, true) => format!("({}) * ({})", a, b),
205        },
206        &|a, s| {
207            if a.contains(' ') {
208                format!("({}) * {}", a, util::format_value(s))
209            } else {
210                format!("{} * {}", a, util::format_value(s))
211            }
212        },
213    )
214}
halo2_axiom/dev/failure/emitter.rs

halo2_axiom/dev/failure/
emitter.rs
