Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat(noir): added assert keyword #1227

Merged
merged 9 commits into from
Apr 26, 2023
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 @@ -447,6 +448,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 @@ -483,6 +485,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 @@ -428,6 +428,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 @@ -442,6 +443,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 @@ -1214,6 +1224,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 @@ -1468,7 +1519,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