Skip to content

Commit

Permalink
feat(debug): tag relations with debug information (#33)
Browse files Browse the repository at this point in the history
* feat: add debug labels to check circuit

* fmt

* fix

* fix: more than one file issue

* inline fix
  • Loading branch information
Maddiaa0 authored Dec 13, 2023
1 parent 5e3bffa commit e3e8dfd
Show file tree
Hide file tree
Showing 9 changed files with 112 additions and 33 deletions.
13 changes: 10 additions & 3 deletions asm_to_pil/src/vm_to_constrained.rs
Original file line number Diff line number Diff line change
Expand Up @@ -144,6 +144,7 @@ impl<T: FieldElement> ASMPILConverter<T> {
),
PilStatement::PolynomialIdentity(
0,
None,
lhs - (Expression::from(T::one())
- next_reference("first_step"))
* direct_reference(pc_update_name),
Expand All @@ -154,10 +155,14 @@ impl<T: FieldElement> ASMPILConverter<T> {
ReadOnly => {
let not_reset: Expression<T> =
Expression::from(T::one()) - direct_reference("instr__reset");
vec![PilStatement::PolynomialIdentity(0, not_reset * (lhs - rhs))]
vec![PilStatement::PolynomialIdentity(
0,
None,
not_reset * (lhs - rhs),
)]
}
_ => {
vec![PilStatement::PolynomialIdentity(0, lhs - rhs)]
vec![PilStatement::PolynomialIdentity(0, None, lhs - rhs)]
}
}
})
Expand Down Expand Up @@ -389,7 +394,7 @@ impl<T: FieldElement> ASMPILConverter<T> {
});

for mut statement in body {
if let PilStatement::PolynomialIdentity(_start, expr) = statement {
if let PilStatement::PolynomialIdentity(_start, _attr, expr) = statement {
match extract_update(expr) {
(Some(var), expr) => {
let reference = direct_reference(&instruction_flag);
Expand All @@ -406,6 +411,7 @@ impl<T: FieldElement> ASMPILConverter<T> {
}
(None, expr) => self.pil.push(PilStatement::PolynomialIdentity(
0,
None,
direct_reference(&instruction_flag) * expr.clone(),
)),
}
Expand Down Expand Up @@ -715,6 +721,7 @@ impl<T: FieldElement> ASMPILConverter<T> {
.sum();
self.pil.push(PilStatement::PolynomialIdentity(
0,
None,
direct_reference(register) - assign_constraint,
));
}
Expand Down
2 changes: 1 addition & 1 deletion ast/src/parsed/display.rs
Original file line number Diff line number Diff line change
Expand Up @@ -383,7 +383,7 @@ impl<T: Display> Display for PilStatement<T> {
value.as_ref().map(|v| format!("{v}")).unwrap_or_default()
)
}
PilStatement::PolynomialIdentity(_, expression) => {
PilStatement::PolynomialIdentity(_, _attr, expression) => {
if let Expression::BinaryOperation(left, BinaryOperator::Sub, right) = expression {
write!(f, "{left} = {right};")
} else {
Expand Down
2 changes: 1 addition & 1 deletion ast/src/parsed/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,7 @@ pub enum PilStatement<T> {
PolynomialConstantDeclaration(usize, Vec<PolynomialName<T>>),
PolynomialConstantDefinition(usize, String, FunctionDefinition<T>),
PolynomialCommitDeclaration(usize, Vec<PolynomialName<T>>, Option<FunctionDefinition<T>>),
PolynomialIdentity(usize, Expression<T>),
PolynomialIdentity(usize, Option<String>, Expression<T>),
PlookupIdentity(
usize,
SelectedExpressions<Expression<T>>,
Expand Down
4 changes: 2 additions & 2 deletions ast/src/parsed/visitor.rs
Original file line number Diff line number Diff line change
Expand Up @@ -208,7 +208,7 @@ impl<T> ExpressionVisitable<Expression<T, NamespacedPolynomialReference>> for Pi

PilStatement::Namespace(_, _, e)
| PilStatement::PolynomialDefinition(_, _, e)
| PilStatement::PolynomialIdentity(_, e)
| PilStatement::PolynomialIdentity(_, _, e)
| PilStatement::PublicDeclaration(_, _, _, None, e)
| PilStatement::ConstantDefinition(_, _, e)
| PilStatement::LetStatement(_, _, Some(e)) => e.visit_expressions_mut(f, o),
Expand Down Expand Up @@ -250,7 +250,7 @@ impl<T> ExpressionVisitable<Expression<T, NamespacedPolynomialReference>> for Pi

PilStatement::Namespace(_, _, e)
| PilStatement::PolynomialDefinition(_, _, e)
| PilStatement::PolynomialIdentity(_, e)
| PilStatement::PolynomialIdentity(_, _, e)
| PilStatement::PublicDeclaration(_, _, _, None, e)
| PilStatement::ConstantDefinition(_, _, e)
| PilStatement::LetStatement(_, _, Some(e)) => e.visit_expressions(f, o),
Expand Down
10 changes: 6 additions & 4 deletions bberg/src/circuit_builder.rs
Original file line number Diff line number Diff line change
Expand Up @@ -79,7 +79,7 @@ impl CircuitBuilder for BBFiles {
|name: &String| format!("polys.{name}_shift = Polynomial(polys.{name}.shifted());");
let check_circuit_transformation = |relation_name: &String| {
format!(
"if (!evaluate_relation.template operator()<{name}_vm::{relation_name}<FF>>(\"{relation_name}\")) {{
"if (!evaluate_relation.template operator()<{name}_vm::{relation_name}<FF>>(\"{relation_name}\", {name}_vm::get_relation_label_{relation_name})) {{
return false;
}}",
name = name,
Expand Down Expand Up @@ -220,7 +220,7 @@ fn get_permutation_check_closure() -> String {
}
for (auto r : permutation_result) {
if (r != 0) {
info(\"Tuple\", permutation_name, \"failed.\");
info(\"Tuple \", permutation_name, \" failed.\");
return false;
}
}
Expand All @@ -231,7 +231,8 @@ fn get_permutation_check_closure() -> String {

fn get_relation_check_closure() -> String {
"
const auto evaluate_relation = [&]<typename Relation>(const std::string& relation_name) {
const auto evaluate_relation = [&]<typename Relation>(const std::string& relation_name,
std::string (*debug_label)(int)) {
typename Relation::SumcheckArrayOfValuesOverSubrelations result;
for (auto& r : result) {
r = 0;
Expand All @@ -244,8 +245,9 @@ fn get_relation_check_closure() -> String {
bool x = true;
for (size_t j = 0; j < NUM_SUBRELATIONS; ++j) {
if (result[j] != 0) {
std::string row_name = debug_label(static_cast<int>(j));
throw_or_abort(
format(\"Relation \", relation_name, \", subrelation index \", j, \" failed at row \", i));
format(\"Relation \", relation_name, \", subrelation index \", row_name, \" failed at row \", i));
x = false;
}
}
Expand Down
97 changes: 79 additions & 18 deletions bberg/src/relation_builder.rs
Original file line number Diff line number Diff line change
Expand Up @@ -58,6 +58,7 @@ pub trait RelationBuilder {
sub_relations: &[String],
identities: &[BBIdentity],
row_type: &str,
labels_lookup: String,
);

/// Declare views
Expand Down Expand Up @@ -85,23 +86,30 @@ impl RelationBuilder for BBFiles {

// ----------------------- Create the relation files -----------------------
for (relation_name, analyzed_idents) in grouped_relations.iter() {
let (subrelations, identities, collected_polys, collected_shifts) =
create_identities(file_name, analyzed_idents);
let IdentitiesOutput {
subrelations,
identities,
collected_cols,
collected_shifts,
expression_labels,
} = create_identities(file_name, analyzed_idents);

shifted_polys.extend(collected_shifts);

// let all_cols_with_shifts = combine_cols(collected_polys, collected_shifts);
// TODO: This can probably be moved into the create_identities function
let row_type = create_row_type(&capitalize(relation_name), &collected_polys);
let row_type = create_row_type(&capitalize(relation_name), &collected_cols);

// Aggregate all shifted polys
shifted_polys.extend(collected_shifts);
// Aggregate all rows
all_rows.insert(relation_name.to_owned(), row_type.clone());

let labels_lookup = create_relation_labels(relation_name, expression_labels);
self.create_relation(
file_name,
relation_name,
&subrelations,
&identities,
&row_type,
labels_lookup,
);
}

Expand All @@ -118,6 +126,7 @@ impl RelationBuilder for BBFiles {
sub_relations: &[String],
identities: &[BBIdentity],
row_type: &str,
labels_lookup: String,
) {
let includes = relation_includes();
let class_boilerplate = relation_class_boilerplate(name, sub_relations, identities);
Expand All @@ -129,6 +138,8 @@ namespace proof_system::{root_name}_vm {{
{row_type};
{labels_lookup}
{class_boilerplate}
{export}
Expand Down Expand Up @@ -362,34 +373,45 @@ fn craft_expression<T: FieldElement>(
}
}

pub struct IdentitiesOutput {
subrelations: Vec<String>,
identities: Vec<BBIdentity>,
collected_cols: Vec<String>,
collected_shifts: Vec<String>,
expression_labels: HashMap<usize, String>,
}

pub(crate) fn create_identities<F: FieldElement>(
file_name: &str,
identities: &[Identity<Expression<F>>],
) -> (Vec<String>, Vec<BBIdentity>, Vec<String>, Vec<String>) {
) -> IdentitiesOutput {
// We only want the expressions for now
// When we have a poly type, we only need the left side of it
let expressions = identities
let ids = identities
.iter()
.filter_map(|identity| {
if identity.kind == IdentityKind::Polynomial {
Some(identity.left.clone())
} else {
None
}
})
.filter(|identity| identity.kind == IdentityKind::Polynomial)
.collect::<Vec<_>>();

let mut identities = Vec::new();
let mut subrelations = Vec::new();
let mut expression_labels: HashMap<usize, String> = HashMap::new(); // Each relation can be given a label, this label can be assigned here
let mut collected_cols: HashSet<String> = HashSet::new();
let mut collected_public_identities: HashSet<String> = HashSet::new();

// Collect labels for each identity
// TODO: shite
for (i, id) in ids.iter().enumerate() {
if let Some(label) = &id.attribute {
expression_labels.insert(i, label.clone());
}
}

let expressions = ids.iter().map(|id| id.left.clone()).collect::<Vec<_>>();
for (i, expression) in expressions.iter().enumerate() {
let relation_boilerplate = format!(
"{file_name}_DECLARE_VIEWS({i});
",
);
// TODO: deal with unwrap

// TODO: collected pattern is shit
let mut identity = create_identity(
Expand Down Expand Up @@ -424,6 +446,45 @@ pub(crate) fn create_identities<F: FieldElement>(
})
.collect();

// Returning both for now
(subrelations, identities, collected_cols, collected_shifts)
IdentitiesOutput {
subrelations,
identities,
collected_cols,
collected_shifts,
expression_labels,
}
}

/// Relation labels
///
/// To view relation labels we create a sparse switch that contains all of the collected labels
/// Whenever there is a failure, we can lookup into this mapping
///
/// Note: this mapping will never be that big, so we are quite naive in implementation
/// It should be able to be called from else where with relation_name::get_relation_label
fn create_relation_labels(relation_name: &str, labels: HashMap<usize, String>) -> String {
let label_transformation = |(index, label)| {
format!(
"case {index}:
return \"{label}\";
"
)
};

let switch_statement: String = labels
.into_iter()
.map(label_transformation)
.collect::<Vec<String>>()
.join("\n");

format!(
"
inline std::string get_relation_label_{relation_name}(int index) {{
switch (index) {{
{switch_statement}
}}
return std::to_string(index);
}}
"
)
}
2 changes: 1 addition & 1 deletion parser/src/powdr.lalrpop
Original file line number Diff line number Diff line change
Expand Up @@ -127,7 +127,7 @@ PolynomialCommitDeclaration: PilStatement<T> = {
}

PolynomialIdentity: PilStatement<T> = {
<start:@L> <l:BoxedExpression> "=" <r:BoxedExpression> => PilStatement::PolynomialIdentity(start, Expression::BinaryOperation(l, BinaryOperator::Sub, r))
<start:@L> <attr:Attribute?> <l:BoxedExpression> "=" <r:BoxedExpression> => PilStatement::PolynomialIdentity(start, attr, Expression::BinaryOperation(l, BinaryOperator::Sub, r))
}

PolynomialNameList: Vec<PolynomialName<T>> = {
Expand Down
13 changes: 11 additions & 2 deletions pil_analyzer/src/statement_processor.rs
Original file line number Diff line number Diff line change
Expand Up @@ -199,8 +199,17 @@ where

fn handle_identity_statement(&mut self, statement: PilStatement<T>) -> Vec<PILItem<T>> {
let (start, kind, attribute, left, right) = match statement {
PilStatement::PolynomialIdentity(start, expression)
| PilStatement::Expression(start, expression) => (
PilStatement::PolynomialIdentity(start, attr, expression) => (
start,
IdentityKind::Polynomial,
attr,
SelectedExpressions {
selector: Some(self.process_expression(expression)),
expressions: vec![],
},
SelectedExpressions::default(),
),
PilStatement::Expression(start, expression) => (
start,
IdentityKind::Polynomial,
None,
Expand Down
2 changes: 1 addition & 1 deletion type_check/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -318,7 +318,7 @@ impl<T: FieldElement> TypeChecker<T> {
let errors: Vec<_> = statements
.iter()
.filter_map(|s| match s {
ast::parsed::PilStatement::PolynomialIdentity(_, _) => None,
ast::parsed::PilStatement::PolynomialIdentity(_, _, _) => None,
ast::parsed::PilStatement::PermutationIdentity(
_, //
_, //
Expand Down

0 comments on commit e3e8dfd

Please sign in to comment.