Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
28 commits
Select commit Hold shift + click to select a range
5884ff6
chore: print ACIR AssertZero as an equation
asterite Sep 23, 2025
6fb656b
Omit zero coefficients
asterite Sep 23, 2025
88c0859
Don't write coefficient 1
asterite Sep 23, 2025
f78b8a9
Use standalone minus when possible
asterite Sep 23, 2025
8a2e7bb
Witness equality to constant
asterite Sep 23, 2025
e4e358c
Another witness equality to constant
asterite Sep 23, 2025
8b0e22c
Handle `-1` in first term
asterite Sep 23, 2025
91eed2c
Stop parsing the old way
asterite Sep 23, 2025
b06db65
Special case for `w0 = w1`
asterite Sep 23, 2025
25cdb75
One more tiny change
asterite Sep 23, 2025
62c1e33
Don't print zero coefficients
asterite Sep 23, 2025
27fedc6
Try to show q_c on the right-hand side of the equation
asterite Sep 23, 2025
fb83a4a
Use new syntax in comments
asterite Sep 23, 2025
f86d431
Merge branch 'master' into ab/acir-print-assert-zero
asterite Sep 23, 2025
3230415
Update acvm-repo/acir/src/circuit/opcodes.rs
asterite Sep 23, 2025
accc53d
Simpler and better parsing
asterite Sep 24, 2025
b22518e
One more special case
asterite Sep 24, 2025
56c48f0
Don't simplify too much
asterite Sep 25, 2025
257818b
Show AssertZero based on actual code
asterite Sep 25, 2025
13f4812
Fix snapshot
asterite Sep 25, 2025
4aec259
Extract `display_term`
asterite Sep 25, 2025
c86a544
More snapshots
asterite Sep 25, 2025
b08b770
Update acvm-repo/acir/src/circuit/opcodes.rs
asterite Sep 25, 2025
959add0
Remove extra space in test
asterite Sep 25, 2025
5e04384
Show expressions that equal zero as `0 = ...`
asterite Sep 25, 2025
ecfb272
Preserve original signs when it's a zero equality
asterite Sep 25, 2025
6f07f9b
Merge branch 'ab/acir-print-assert-zero' of github.com:noir-lang/noir…
asterite Sep 25, 2025
3329457
Merge branch 'master' into ab/acir-print-assert-zero
asterite Sep 25, 2025
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion acvm-repo/acir/src/circuit/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -544,7 +544,7 @@ mod tests {
private parameters: []
public parameters: [w2]
return values: [w2]
EXPR [ (2, w1) 8 ]
EXPR 0 = 2*w1 + 8
BLACKBOX::RANGE [w1]:8 bits []
BLACKBOX::AND [w1, w2]:4 bits [w3]
BLACKBOX::KECCAKF1600 [w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, w16, w17, w18, w19, w20, w21, w22, w23, w24, w25] [w26, w27, w28, w29, w30, w31, w32, w33, w34, w35, w36, w37, w38, w39, w40, w41, w42, w43, w44, w45, w46, w47, w48, w49, w50]
Expand Down
127 changes: 124 additions & 3 deletions acvm-repo/acir/src/circuit/opcodes.rs
Original file line number Diff line number Diff line change
Expand Up @@ -146,16 +146,97 @@ pub enum Opcode<F: AcirField> {
impl<F: AcirField> std::fmt::Display for Opcode<F> {
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
match self {
Opcode::AssertZero(expr) => expr.fmt(f),
Opcode::AssertZero(expr) => {
write!(f, "EXPR ")?;

// This is set to an index if we show this expression "as a witness assignment", meaning
// that the linear combination at this index must not be printed again.
let mut assignment_witness: Option<usize> = None;

// If true, negate all coefficients when printing.
// This is set to true if we show this expression "as a witness assignment", and the witness
// had a coefficient of 1 and we "moved" everything to the right of the equal sign.
let mut negate_coefficients = false;

// Find a linear combination with a coefficient of 1 or -1 and, if there are many,
// keep the one with the largest witness.
let linear_witness_one = expr
.linear_combinations
.iter()
.enumerate()
.filter(|(_, (coefficient, _))| {
coefficient.is_one() || (-*coefficient).is_one()
})
.max_by_key(|(_, (_, witness))| witness);

// If we find one, show the expression as equaling this witness to everything else
// (this is likely to happen as in ACIR gen we tend to equate a witness to previous expressions)
if let Some((index, (coefficient, witness))) = linear_witness_one {
assignment_witness = Some(index);
negate_coefficients = coefficient.is_one();
write!(f, "{witness} = ")?;
} else {
write!(f, "0 = ")?;
}

let mut printed_term = false;

for (coefficient, witness1, witness2) in &expr.mul_terms {
let witnesses = [*witness1, *witness2];
display_term(*coefficient, witnesses, printed_term, negate_coefficients, f)?;
printed_term = true;
}

for (index, (coefficient, witness)) in expr.linear_combinations.iter().enumerate() {
if assignment_witness
.is_some_and(|show_as_assignment_index| show_as_assignment_index == index)
{
// We already printed this term as part of the assignment
continue;
}

let witnesses = [*witness];
display_term(*coefficient, witnesses, printed_term, negate_coefficients, f)?;
printed_term = true;
}

if expr.q_c.is_zero() {
if !printed_term {
write!(f, "0")?;
}
} else {
let coefficient = expr.q_c;
let coefficient = if negate_coefficients { -coefficient } else { coefficient };
let coefficient_as_string = coefficient.to_string();
let coefficient_is_negative = coefficient_as_string.starts_with('-');

if printed_term {
if coefficient_is_negative {
write!(f, " - ")?;
} else {
write!(f, " + ")?;
}
}

let coefficient = if printed_term && coefficient_is_negative {
-coefficient
} else {
coefficient
};
write!(f, "{coefficient}")?;
}

Ok(())
}
Opcode::BlackBoxFuncCall(g) => g.fmt(f),
Opcode::MemoryOp { block_id, op } => {
write!(f, "MEM ")?;

let is_read = op.operation.is_zero();
if is_read {
write!(f, "(id: {}, read at: {}, value: {}) ", block_id.0, op.index, op.value)
write!(f, "(id: {}, read at: {}, value: {})", block_id.0, op.index, op.value)
} else {
write!(f, "(id: {}, write {} at: {}) ", block_id.0, op.value, op.index)
write!(f, "(id: {}, write {} at: {})", block_id.0, op.value, op.index)
}
}
Opcode::MemoryInit { block_id, init, block_type: databus } => {
Expand Down Expand Up @@ -207,6 +288,46 @@ impl<F: AcirField> std::fmt::Display for Opcode<F> {
}
}

fn display_term<F: AcirField, const N: usize>(
coefficient: F,
witnesses: [Witness; N],
printed_term: bool,
negate_coefficients: bool,
f: &mut std::fmt::Formatter<'_>,
) -> std::fmt::Result {
let coefficient = if negate_coefficients { -coefficient } else { coefficient };
let coefficient_as_string = coefficient.to_string();
let coefficient_is_negative = coefficient_as_string.starts_with('-');

if printed_term {
if coefficient_is_negative {
write!(f, " - ")?;
} else {
write!(f, " + ")?;
}
}

let coefficient =
if printed_term && coefficient_is_negative { -coefficient } else { coefficient };

if coefficient.is_one() {
// Don't print the coefficient
} else if (-coefficient).is_one() {
write!(f, "-")?;
} else {
write!(f, "{coefficient}*")?;
}

for (index, witness) in witnesses.iter().enumerate() {
if index != 0 {
write!(f, "*")?;
}
write!(f, "{witness}")?;
}

Ok(())
}

impl<F: AcirField> std::fmt::Debug for Opcode<F> {
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
std::fmt::Display::fmt(self, f)
Expand Down
7 changes: 5 additions & 2 deletions acvm-repo/acir/src/native_types/expression/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -58,9 +58,12 @@ impl<F: std::fmt::Display> std::fmt::Display for Expression<F> {
for i in &self.linear_combinations {
write!(f, "({}, {}) ", i.0, i.1)?;
}
write!(f, "{}", self.q_c)?;

write!(f, " ]")
let q_c_as_string = self.q_c.to_string();
if q_c_as_string != "0" {
write!(f, "{} ", self.q_c)?;
}
write!(f, "]")
}
}

Expand Down
6 changes: 6 additions & 0 deletions acvm-repo/acir/src/parser/lexer.rs
Original file line number Diff line number Diff line change
Expand Up @@ -64,6 +64,12 @@ impl<'a> Lexer<'a> {
',' => self.single_char_token(Token::Comma),
':' => self.single_char_token(Token::Colon),
';' => self.single_char_token(Token::Semicolon),
'+' => self.single_char_token(Token::Plus),
'-' if self.peek_char().is_none_or(|char| !char.is_ascii_digit()) => {
self.single_char_token(Token::Minus)
}
'*' => self.single_char_token(Token::Star),
'=' => self.single_char_token(Token::Equal),
'w' if self.peek_char().is_some_and(|char| char.is_ascii_digit()) => {
let start = self.position;

Expand Down
138 changes: 131 additions & 7 deletions acvm-repo/acir/src/parser/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -235,7 +235,7 @@ impl<'a> Parser<'a> {
while let Some(keyword) = self.peek_keyword() {
match keyword {
Keyword::Expression => {
let expr = self.parse_arithmetic_expression()?;
let expr = self.parse_assert_zero_expression()?;
opcodes.push(Opcode::AssertZero(expr));
}
Keyword::BlackBoxFuncCall => {
Expand All @@ -260,6 +260,86 @@ impl<'a> Parser<'a> {
Ok(opcodes)
}

fn parse_assert_zero_expression(&mut self) -> ParseResult<Expression<FieldElement>> {
// 'EXPR'
self.eat_keyword_or_error(Keyword::Expression)?;

// Parse the left-hand side terms
let lhs_terms = self.parse_terms_or_error()?;

// '='
self.eat_or_error(Token::Equal)?;

// Parse the right-hand side terms
let rhs_terms = self.parse_terms_or_error()?;

// If we have something like `0 = ...` or `... = 0`, just consider the expressions
// on the non-zero side. Otherwise we could be "moving" terms to the other side and
// negating them, which won't accurately reflect the original expression.
let expression = if is_zero_term(&lhs_terms) {
build_expression_from_terms(rhs_terms.into_iter())
} else if is_zero_term(&rhs_terms) {
build_expression_from_terms(lhs_terms.into_iter())
} else {
// "Move" the terms to the left by negating them
let rhs_terms = rhs_terms.into_iter().map(|term| term.negate()).collect::<Vec<_>>();
build_expression_from_terms(lhs_terms.into_iter().chain(rhs_terms))
};

Ok(expression)
}

fn parse_terms_or_error(&mut self) -> ParseResult<Vec<Term>> {
let mut terms = Vec::new();
let mut negative = self.eat(Token::Minus)?;
loop {
let term = self.parse_term_or_error()?;
let term = if negative { term.negate() } else { term };
terms.push(term);

if self.eat(Token::Plus)? {
negative = false;
continue;
}

if self.eat(Token::Minus)? {
negative = true;
continue;
}

break;
}
Ok(terms)
}

fn parse_term_or_error(&mut self) -> ParseResult<Term> {
if let Some(coefficient) = self.eat_field_element()? {
if self.eat(Token::Star)? {
let w1 = self.eat_witness_or_error()?;
self.parse_linear_or_multiplication_term(coefficient, w1)
} else {
Ok(Term::Constant(coefficient))
}
} else if let Some(w1) = self.eat_witness()? {
self.parse_linear_or_multiplication_term(FieldElement::one(), w1)
} else {
self.expected_term()
}
}

fn parse_linear_or_multiplication_term(
&mut self,
coefficient: FieldElement,
w1: Witness,
) -> Result<Term, ParserError> {
if self.eat(Token::Star)? {
let w2 = self.eat_witness_or_error()?;
Ok(Term::Multiplication(coefficient, w1, w2))
} else {
Ok(Term::Linear(coefficient, w1))
}
}

fn parse_arithmetic_expression(&mut self) -> ParseResult<Expression<FieldElement>> {
self.eat_keyword_or_error(Keyword::Expression)?;
self.eat_or_error(Token::LeftBracket)?;
Expand Down Expand Up @@ -308,9 +388,8 @@ impl<'a> Parser<'a> {
}
}

let Some(q_c) = constant else {
return Err(ParserError::MissingConstantTerm { span: self.token.span() });
};
// If a constant isn't provided, we default it to zero
let q_c = constant.unwrap_or_default();

Ok(Expression { mul_terms, linear_combinations, q_c })
}
Expand Down Expand Up @@ -977,6 +1056,13 @@ impl<'a> Parser<'a> {
})
}

fn expected_term<T>(&mut self) -> ParseResult<T> {
Err(ParserError::ExpectedTerm {
found: self.token.token().clone(),
span: self.token.span(),
})
}

fn expected_token<T>(&mut self, token: Token) -> ParseResult<T> {
Err(ParserError::ExpectedToken {
token,
Expand All @@ -994,10 +1080,48 @@ impl<'a> Parser<'a> {
}
}

fn build_expression_from_terms(terms: impl Iterator<Item = Term>) -> Expression<FieldElement> {
// Gather all terms, summing the constants
let mut q_c = FieldElement::zero();
let mut linear_combinations = Vec::new();
let mut mul_terms = Vec::new();

for term in terms {
match term {
Term::Constant(c) => q_c += c,
Term::Linear(c, w) => linear_combinations.push((c, w)),
Term::Multiplication(c, w1, w2) => mul_terms.push((c, w1, w2)),
}
}

Expression { mul_terms, linear_combinations, q_c }
}

fn is_zero_term(terms: &[Term]) -> bool {
terms.len() == 1 && matches!(terms[0], Term::Constant(c) if c.is_zero())
}

fn eof_spanned_token() -> SpannedToken {
SpannedToken::new(Token::Eof, Default::default())
}

#[derive(Debug, Clone, Copy)]
enum Term {
Constant(FieldElement),
Linear(FieldElement, Witness),
Multiplication(FieldElement, Witness, Witness),
}

impl Term {
fn negate(self) -> Self {
match self {
Term::Constant(c) => Term::Constant(-c),
Term::Linear(c, w) => Term::Linear(-c, w),
Term::Multiplication(c, w1, w2) => Term::Multiplication(-c, w1, w2),
}
}
}

type ParseResult<T> = Result<T, ParserError>;

#[derive(Debug, Error)]
Expand All @@ -1014,10 +1138,10 @@ pub(crate) enum ParserError {
ExpectedFieldElement { found: Token, span: Span },
#[error("Expected a witness index, found '{found}'")]
ExpectedWitness { found: Token, span: Span },
#[error("Expected a term, found '{found}'")]
ExpectedTerm { found: Token, span: Span },
#[error("Duplicate constant term in native Expression")]
DuplicatedConstantTerm { found: Token, span: Span },
#[error("Missing constant term in native Expression")]
MissingConstantTerm { span: Span },
#[error("Expected valid black box function name, found '{found}'")]
ExpectedBlackBoxFuncName { found: Token, span: Span },
#[error("Number does not fit in u32, got: '{number}'")]
Expand All @@ -1042,8 +1166,8 @@ impl ParserError {
| ExpectedIdentifier { span, .. }
| ExpectedFieldElement { span, .. }
| ExpectedWitness { span, .. }
| ExpectedTerm { span, .. }
| DuplicatedConstantTerm { span, .. }
| MissingConstantTerm { span }
| ExpectedBlackBoxFuncName { span, .. }
| IntegerLargerThanU32 { span, .. }
| IncorrectInputLength { span, .. }
Expand Down
Loading
Loading