Skip to content

Commit

Permalink
feat(noir): added assert keyword (#1227)
Browse files Browse the repository at this point in the history
* feat(keyword): added assert keyword

* test(keyword): added integration test

* fix(parser): separate parser for assertion

* test(parser): fix test

* style(parser): fix whitespaces

* refactor(keyword): assert use constrain parser

* feat(parser): give assertions function form

* fix(lexer): update the basic test

* style: label the whole assertion statement
  • Loading branch information
sirasistant authored Apr 26, 2023
1 parent e551e55 commit 0dc2cac
Show file tree
Hide file tree
Showing 6 changed files with 75 additions and 0 deletions.
5 changes: 5 additions & 0 deletions crates/nargo_cli/tests/test_data/assert/Nargo.toml
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
[package]
authors = [""]
compiler_version = "0.1"

[dependencies]
1 change: 1 addition & 0 deletions crates/nargo_cli/tests/test_data/assert/Prover.toml
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
x = "1"
3 changes: 3 additions & 0 deletions crates/nargo_cli/tests/test_data/assert/src/main.nr
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
fn main(x: Field) {
assert(x == 1);
}
10 changes: 10 additions & 0 deletions crates/noirc_frontend/src/lexer/lexer.rs
Original file line number Diff line number Diff line change
Expand Up @@ -560,6 +560,7 @@ fn test_basic_language_syntax() {
x * y;
};
constrain mul(five, ten) == 50;
assert(ten + five == 15);
";

let expected = vec![
Expand Down Expand Up @@ -601,6 +602,15 @@ fn test_basic_language_syntax() {
Token::Equal,
Token::Int(50_i128.into()),
Token::Semicolon,
Token::Keyword(Keyword::Assert),
Token::LeftParen,
Token::Ident("ten".to_string()),
Token::Plus,
Token::Ident("five".to_string()),
Token::Equal,
Token::Int(15_i128.into()),
Token::RightParen,
Token::Semicolon,
Token::EOF,
];
let mut lexer = Lexer::new(input);
Expand Down
3 changes: 3 additions & 0 deletions crates/noirc_frontend/src/lexer/token.rs
Original file line number Diff line number Diff line change
Expand Up @@ -414,6 +414,7 @@ impl AsRef<str> for Attribute {
#[cfg_attr(test, derive(strum_macros::EnumIter))]
pub enum Keyword {
As,
Assert,
Bool,
Char,
CompTime,
Expand Down Expand Up @@ -448,6 +449,7 @@ impl fmt::Display for Keyword {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
match *self {
Keyword::As => write!(f, "as"),
Keyword::Assert => write!(f, "assert"),
Keyword::Bool => write!(f, "bool"),
Keyword::Char => write!(f, "char"),
Keyword::CompTime => write!(f, "comptime"),
Expand Down Expand Up @@ -485,6 +487,7 @@ impl Keyword {
pub(crate) fn lookup_keyword(word: &str) -> Option<Token> {
let keyword = match word {
"as" => Keyword::As,
"assert" => Keyword::Assert,
"bool" => Keyword::Bool,
"char" => Keyword::Char,
"comptime" => Keyword::CompTime,
Expand Down
53 changes: 53 additions & 0 deletions crates/noirc_frontend/src/parser/parser.rs
Original file line number Diff line number Diff line change
Expand Up @@ -435,6 +435,7 @@ where
{
choice((
constrain(expr_parser.clone()),
assertion(expr_parser.clone()),
declaration(expr_parser.clone()),
assignment(expr_parser.clone()),
expr_parser.map(Statement::Expression),
Expand All @@ -449,6 +450,15 @@ where
.map(|expr| Statement::Constrain(ConstrainStatement(expr)))
}

fn assertion<'a, P>(expr_parser: P) -> impl NoirParser<Statement> + 'a
where
P: ExprParser + 'a,
{
ignore_then_commit(keyword(Keyword::Assert), parenthesized(expr_parser))
.labelled("statement")
.map(|expr| Statement::Constrain(ConstrainStatement(expr)))
}

fn declaration<'a, P>(expr_parser: P) -> impl NoirParser<Statement> + 'a
where
P: ExprParser + 'a,
Expand Down Expand Up @@ -1228,6 +1238,47 @@ mod test {
);
}

#[test]
fn parse_assert() {
parse_with(assertion(expression()), "assert(x == y)").unwrap();

// Currently we disallow constrain statements where the outer infix operator
// produces a value. This would require an implicit `==` which
// may not be intuitive to the user.
//
// If this is deemed useful, one would either apply a transformation
// or interpret it with an `==` in the evaluator
let disallowed_operators = vec![
BinaryOpKind::And,
BinaryOpKind::Subtract,
BinaryOpKind::Divide,
BinaryOpKind::Multiply,
BinaryOpKind::Or,
];

for operator in disallowed_operators {
let src = format!("assert(x {} y);", operator.as_string());
parse_with(assertion(expression()), &src).unwrap_err();
}

// These are general cases which should always work.
//
// The first case is the most noteworthy. It contains two `==`
// The first (inner) `==` is a predicate which returns 0/1
// The outer layer is an infix `==` which is
// associated with the Constrain statement
parse_all(
assertion(expression()),
vec![
"assert(((x + y) == k) + z == y)",
"assert((x + !y) == y)",
"assert((x ^ y) == y)",
"assert((x ^ y) == (y + m))",
"assert(x + x ^ x == y | m)",
],
);
}

#[test]
fn parse_let() {
// Why is it valid to specify a let declaration as having type u8?
Expand Down Expand Up @@ -1483,7 +1534,9 @@ mod test {
("let", 3, "let $error: unspecified = Error"),
("foo = one two three", 1, "foo = plain::one"),
("constrain", 1, "constrain Error"),
("assert", 1, "constrain Error"),
("constrain x ==", 1, "constrain (plain::x == Error)"),
("assert(x ==)", 1, "constrain (plain::x == Error)"),
];

let show_errors = |v| vecmap(v, ToString::to_string).join("\n");
Expand Down

0 comments on commit 0dc2cac

Please sign in to comment.