feat(fv): Add the implication operator

For writing more readable proofs we need the implication operator.
With this commit we now add it. The user can write x ==> y where x and y
are boolean statements.

We are transforming the implication operator into !x | y which is
logically equivalent to x ==> y.

The implication operator can be used both in attributes and function's
bodies.

Added tests which showcase the new feature.

compiler/noirc_evaluator/src/ssa/ssa_gen/context.rs

@@ -1000,6 +1000,7 @@ fn convert_operator(op: BinaryOpKind) -> BinaryOp {
         BinaryOpKind::Xor => BinaryOp::Xor,
         BinaryOpKind::ShiftLeft => BinaryOp::Shl,
         BinaryOpKind::ShiftRight => BinaryOp::Shr,
+        BinaryOpKind::Implication => unreachable!("No implication token should have remained."),
     }
 }
 

compiler/noirc_frontend/src/ast/expression.rs

@@ -326,6 +326,7 @@ pub enum BinaryOpKind {
     ShiftRight,
     ShiftLeft,
     Modulo,
+    Implication,
 }
 
 impl BinaryOpKind {
@@ -374,6 +375,7 @@ impl BinaryOpKind {
             BinaryOpKind::ShiftRight => ">>",
             BinaryOpKind::ShiftLeft => "<<",
             BinaryOpKind::Modulo => "%",
+            BinaryOpKind::Implication => "==>",
         }
     }
 
@@ -395,6 +397,7 @@ impl BinaryOpKind {
             BinaryOpKind::ShiftLeft => Token::ShiftLeft,
             BinaryOpKind::ShiftRight => Token::ShiftRight,
             BinaryOpKind::Modulo => Token::Percent,
+            BinaryOpKind::Implication => Token::Implication,
         }
     }
 }
@@ -770,6 +773,7 @@ impl Display for BinaryOpKind {
             BinaryOpKind::ShiftLeft => write!(f, "<<"),
             BinaryOpKind::ShiftRight => write!(f, ">>"),
             BinaryOpKind::Modulo => write!(f, "%"),
+            BinaryOpKind::Implication => write!(f, "==>"),
         }
     }
 }

compiler/noirc_frontend/src/ast/mod.rs

@@ -451,7 +451,8 @@ impl UnresolvedTypeExpression {
                     | BinaryOpKind::Or
                     | BinaryOpKind::Xor
                     | BinaryOpKind::ShiftRight
-                    | BinaryOpKind::ShiftLeft => {
+                    | BinaryOpKind::ShiftLeft
+                    | BinaryOpKind::Implication => {
                         unreachable!("impossible via `operator_allowed` check")
                     }
                 };

compiler/noirc_frontend/src/elaborator/types.rs

@@ -1873,6 +1873,9 @@ fn try_eval_array_length_id_with_fuel(
                 BinaryOpKind::ShiftRight => Ok(lhs >> rhs),
                 BinaryOpKind::ShiftLeft => Ok(lhs << rhs),
                 BinaryOpKind::Modulo => Ok(lhs % rhs),
+                BinaryOpKind::Implication => {
+                    unreachable!("No implication token shoud have remained.")
+                }
             }
         }
         HirExpression::Cast(cast) => {

compiler/noirc_frontend/src/hir/comptime/display.rs

@@ -292,6 +292,7 @@ impl<'interner> TokenPrettyPrinter<'interner> {
             Token::EOF => Ok(()),
             Token::Requires => write!(f, "{token}"),
             Token::Ensures => write!(f, "{token}"),
+            Token::Implication => write!(f, " {token} ")
         }
     }
 

compiler/noirc_frontend/src/hir/comptime/interpreter.rs

@@ -1102,6 +1102,9 @@ impl<'local, 'interner> Interpreter<'local, 'interner> {
                 (Value::U64(lhs), Value::U64(rhs)) => Ok(Value::U64(lhs % rhs)),
                 (lhs, rhs) => make_error(self, lhs, rhs, "%"),
             },
+            BinaryOpKind::Implication => {
+                unreachable!("All implications must have been transformed to !lsh | rhs")
+            }
         }
     }
 

compiler/noirc_frontend/src/lexer/lexer.rs

@@ -216,7 +216,16 @@ impl<'a> Lexer<'a> {
                 }
             }
             Token::Bang => self.single_double_peek_token('=', prev_token, Token::NotEqual),
-            Token::Assign => self.single_double_peek_token('=', prev_token, Token::Equal),
+            Token::Assign => {
+                if self.peek_char_is('=') && self.peek2_char_is('>') {
+                    let start = self.position;
+                    self.next_char();
+                    self.next_char();
+                    Ok(Token::Implication.into_span(start, start + 2))
+                } else {
+                    self.single_double_peek_token('=', prev_token, Token::Equal)
+                }
+            }
             Token::Minus => self.single_double_peek_token('>', prev_token, Token::Arrow),
             Token::Colon => self.single_double_peek_token(':', prev_token, Token::DoubleColon),
             Token::Slash => {

compiler/noirc_frontend/src/lexer/token.rs

@@ -112,6 +112,8 @@ pub enum BorrowedToken<'input> {
     Requires,
     /// #[ensures
     Ensures,
+    /// ==>
+    Implication,
 
     #[allow(clippy::upper_case_acronyms)]
     EOF,
@@ -236,6 +238,8 @@ pub enum Token {
     Requires,
     /// #[ensures
     Ensures,
+    /// ==>
+    Implication,
 
     #[allow(clippy::upper_case_acronyms)]
     EOF,
@@ -317,6 +321,7 @@ pub fn token_to_borrowed_token(token: &Token) -> BorrowedToken<'_> {
         Token::UnquoteMarker(id) => BorrowedToken::UnquoteMarker(*id),
         Token::Requires => BorrowedToken::Requires,
         Token::Ensures => BorrowedToken::Ensures,
+        Token::Implication => BorrowedToken::Implication,
     }
 }
 
@@ -450,6 +455,7 @@ impl fmt::Display for Token {
             Token::UnquoteMarker(_) => write!(f, "(UnquoteMarker)"),
             Token::Requires => write!(f, "#[requires"),
             Token::Ensures => write!(f, "#[ensures"),
+            Token::Implication => write!(f, "==>"),
         }
     }
 }
@@ -564,6 +570,7 @@ impl Token {
             Token::Greater => Greater,
             Token::GreaterEqual => GreaterEqual,
             Token::Percent => Modulo,
+            Token::Implication => Implication,
             _ => return None,
         };
         Some(Spanned::from(span, binary_op))

compiler/noirc_frontend/src/parser/mod.rs

@@ -455,6 +455,7 @@ impl SortedModule {
 
 #[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd)]
 pub enum Precedence {
+    Implication,
     Lowest,
     Or,
     And,
@@ -473,6 +474,7 @@ impl Precedence {
         let precedence = match tok {
             Token::Equal => Precedence::Lowest,
             Token::NotEqual => Precedence::Lowest,
+            Token::Implication => Precedence::Implication,
             Token::Pipe => Precedence::Or,
             Token::Ampersand => Precedence::And,
             Token::Caret => Precedence::Xor,
@@ -498,6 +500,7 @@ impl Precedence {
     fn next(self) -> Self {
         use Precedence::*;
         match self {
+            Implication => Lowest,
             Lowest => Or,
             Or => Xor,
             Xor => And,

compiler/noirc_frontend/src/parser/parser.rs

@@ -44,10 +44,7 @@ use super::{
 };
 use super::{spanned, Item, TopLevelStatement};
 use crate::ast::{
-    BinaryOp, BinaryOpKind, BlockExpression, Documented, ForLoopStatement, ForRange,
-    GenericTypeArgs, Ident, IfExpression, InfixExpression, LValue, Literal, ModuleDeclaration,
-    NoirTypeAlias, Param, Path, Pattern, Recoverable, Statement, TypeImpl, UnaryRhsMemberAccess,
-    UnaryRhsMethodCall, UseTree, UseTreeKind, Visibility,
+    BinaryOp, BinaryOpKind, BlockExpression, Documented, ForLoopStatement, ForRange, GenericTypeArgs, Ident, IfExpression, InfixExpression, LValue, Literal, ModuleDeclaration, NoirTypeAlias, Param, Path, Pattern, PrefixExpression, Recoverable, Statement, TypeImpl, UnaryOp, UnaryRhsMemberAccess, UnaryRhsMethodCall, UseTree, UseTreeKind, Visibility
 };
 use crate::ast::{
     Expression, ExpressionKind, LetStatement, StatementKind, UnresolvedType, UnresolvedTypeData,
@@ -731,7 +728,7 @@ fn call_data() -> impl NoirParser<Visibility> {
 pub fn expression() -> impl ExprParser {
     recursive(|expr| {
         expression_with_precedence(
-            Precedence::Lowest,
+            Precedence::Implication,
             expr.clone(),
             expression_no_constructors(expr.clone()),
             statement(expr.clone(), expression_no_constructors(expr)),
@@ -748,7 +745,7 @@ where
 {
     recursive(|expr_no_constructors| {
         expression_with_precedence(
-            Precedence::Lowest,
+            Precedence::Implication,
             expr_parser.clone(),
             expr_no_constructors.clone(),
             statement(expr_parser, expr_no_constructors),
@@ -823,7 +820,18 @@ where
 
 fn create_infix_expression(lhs: Expression, (operator, rhs): (BinaryOp, Expression)) -> Expression {
     let span = lhs.span.merge(rhs.span);
-    let infix = Box::new(InfixExpression { lhs, operator, rhs });
+
+    // If we have an implication (lhs ==> rhs) we want to transform it to (!lhs | rhs)
+    let infix = if operator.contents == BinaryOpKind::Implication {
+        let new_lhs = Expression::new(
+            ExpressionKind::Prefix(Box::new(PrefixExpression { operator: UnaryOp::Not, rhs: lhs.clone() })),
+            lhs.span,
+        );
+        let new_operator = Spanned::from(operator.span(), BinaryOpKind::Or);
+        Box::new(InfixExpression { lhs: new_lhs, operator: new_operator, rhs })
+    } else {
+        Box::new(InfixExpression { lhs, operator, rhs })
+    };
 
     Expression { span, kind: ExpressionKind::Infix(infix) }
 }

test_programs/formal_verify_failure/implication_operator/Nargo.toml

@@ -0,0 +1,7 @@
+[package]
+name = "implication_operator"
+type = "bin"
+authors = [""]
+compiler_version = ">=0.35.0"
+
+[dependencies]

test_programs/formal_verify_failure/implication_operator/src/main.nr

@@ -0,0 +1,9 @@
+// This test is expected to fail because if y is true, main returns x, not 0.
+#[ensures((y ==> result == 0))]
+fn main(x: u32, y: bool) -> pub u32 {
+    if y {
+        x
+    } else {
+        0
+    }
+}

test_programs/formal_verify_success/implication_operator_1/Nargo.toml

@@ -0,0 +1,7 @@
+[package]
+name = "implication_operator"
+type = "bin"
+authors = [""]
+compiler_version = ">=0.35.0"
+
+[dependencies]

test_programs/formal_verify_success/implication_operator_1/src/main.nr

@@ -0,0 +1,8 @@
+#[ensures((y ==> result == x) & (!y ==> result == 0))]
+fn main(x: u32, y: bool) -> pub u32 {
+    if y {
+        x
+    } else {
+        0
+    }
+}

test_programs/formal_verify_success/implication_operator_2/Nargo.toml

@@ -0,0 +1,7 @@
+[package]
+name = "implication_operator"
+type = "bin"
+authors = [""]
+compiler_version = ">=0.35.0"
+
+[dependencies]

test_programs/formal_verify_success/implication_operator_2/src/main.nr

@@ -0,0 +1,6 @@
+// This test shows that you can use the implication operator not
+// only in attributes but also in the function's body.
+#[requires(y ==> x > 5)]
+fn main(x: u32, y: bool) {
+    assert(y ==> x > 5);
+}