diff --git a/Cargo.lock b/Cargo.lock index fd609f8758a..a043f07d810 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -1546,6 +1546,27 @@ dependencies = [ "syn 2.0.102", ] +[[package]] +name = "derive_more" +version = "2.0.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "093242cf7570c207c83073cf82f79706fe7b8317e98620a47d5be7c3d8497678" +dependencies = [ + "derive_more-impl", +] + +[[package]] +name = "derive_more-impl" +version = "2.0.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "bda628edc44c4bb645fbe0f758797143e4e07926f7ebf4e9bdfbd3d2ce621df3" +dependencies = [ + "proc-macro2", + "quote", + "syn 2.0.102", + "unicode-xid", +] + [[package]] name = "difflib" version = "0.4.0" @@ -1942,6 +1963,32 @@ dependencies = [ "percent-encoding", ] +[[package]] +name = "formal_verification" +version = "1.0.0-beta.7" +dependencies = [ + "base64", + "bn254_blackbox_solver", + "cfg-if", + "derive_more", + "function_name", + "insta", + "noirc_errors", + "noirc_evaluator", + "noirc_frontend", + "nom", + "num-bigint 0.4.6", + "num-traits", + "proptest", + "proptest-derive", + "serde", + "serde_json", + "strum 0.24.1", + "strum_macros 0.24.3", + "tracing", + "vir", +] + [[package]] name = "fs2" version = "0.4.3" @@ -2074,6 +2121,25 @@ dependencies = [ "thread_local", ] +[[package]] +name = "fv_bridge" +version = "1.0.0-beta.7" +dependencies = [ + "acvm", + "fm", + "formal_verification", + "iter-extended", + "noirc_driver", + "noirc_errors", + "noirc_evaluator", + "noirc_frontend", + "num-bigint 0.4.6", + "num-traits", + "serde", + "thiserror 1.0.69", + "vir", +] + [[package]] name = "fxhash" version = "0.2.1" @@ -3334,6 +3400,7 @@ dependencies = [ "dirs", "fm", "fs2", + "fv_bridge", "fxhash", "iai", "insta", @@ -3382,6 +3449,7 @@ dependencies = [ "tracing", "tracing-appender", "tracing-subscriber", + "vir", ] [[package]] @@ -3930,6 +3998,15 @@ dependencies = [ "serde_json", ] +[[package]] +name = "nom" +version = "8.0.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "df9761775871bdef83bee530e60050f7e54b1105350d6884eb0fb4f46c2f9405" +dependencies = [ + "memchr", +] + [[package]] name = "normalize-line-endings" version = "0.3.0" diff --git a/Cargo.toml b/Cargo.toml index f5744673690..d27e9dfd288 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -1,6 +1,8 @@ [workspace] members = [ + # FV crates + "compiler/fv_bridge", # Compiler crates "compiler/noirc_arena", "compiler/noirc_evaluator", @@ -8,6 +10,7 @@ members = [ "compiler/noirc_errors", "compiler/noirc_driver", "compiler/noirc_printable_type", + "compiler/formal_verification", "compiler/fm", "compiler/wasm", # Crates related to tooling built on top of the Noir compiler @@ -154,6 +157,8 @@ codespan-reporting = "0.11.1" # Formal verification vir = {git = "https://github.com/Aristotelis2002/verus-lib", branch = "synced_main"} +formal_verification = { path = "compiler/formal_verification"} +fv_bridge = { path = "compiler/fv_bridge" } # Benchmarking criterion = "^0.5.0" diff --git a/compiler/formal_verification/Cargo.toml b/compiler/formal_verification/Cargo.toml new file mode 100644 index 00000000000..af792906fef --- /dev/null +++ b/compiler/formal_verification/Cargo.toml @@ -0,0 +1,37 @@ +[package] +name = "formal_verification" +version.workspace = true +authors.workspace = true +edition.workspace = true +rust-version.workspace = true +license.workspace = true + +[dependencies] +bn254_blackbox_solver.workspace = true +serde_json.workspace = true +serde.workspace = true +num-bigint.workspace = true +num-traits.workspace = true +noirc_errors.workspace = true +noirc_evaluator.workspace = true +noirc_frontend.workspace = true +vir.workspace = true +cfg-if.workspace = true +tracing.workspace = true +strum.workspace = true +strum_macros.workspace = true +nom = "8.0" +derive_more = { version = "2.0.1", features = ["deref", "from", "into", "debug"] } + +[dev-dependencies] +base64.workspace = true +function_name = "0.3.0" +proptest.workspace = true +proptest-derive.workspace = true +insta.workspace = true + +[features] +bn254 = [] +bls12_381 = [] +test_utils = [] +nextest = [] diff --git a/compiler/formal_verification/src/ast.rs b/compiler/formal_verification/src/ast.rs new file mode 100644 index 00000000000..181ab9f7f4e --- /dev/null +++ b/compiler/formal_verification/src/ast.rs @@ -0,0 +1,312 @@ +use std::fmt::{Debug, Display}; + +use noirc_errors::Location; +use noirc_frontend::monomorphization::ast::Type as NoirType; +use num_bigint::BigInt; + +pub type Identifier = String; + +#[derive(Clone, Debug, PartialEq, Eq)] +pub enum ExprF { + BinaryOp { op: BinaryOp, expr_left: R, expr_right: R }, + UnaryOp { op: UnaryOp, expr: R }, + Parenthesised { expr: R }, + Quantified { quantifier: Quantifier, variables: Vec, expr: R }, + FnCall { name: Identifier, args: Vec }, + Index { expr: R, index: R }, + TupleAccess { expr: R, index: u32 }, + StructureAccess { expr: R, field: Identifier }, + Cast { expr: R, target: NoirType }, + Literal { value: Literal }, + Tuple { exprs: Vec }, + Array { exprs: Vec }, + Variable(Variable), +} + +#[derive(Clone, Debug, PartialEq, Eq)] +pub struct AnnExpr { + pub ann: A, + pub expr: Box>>, +} + +pub type SpannedTypedExpr = AnnExpr<(Location, NoirType)>; +pub type SpannedExpr = AnnExpr; +pub type OffsetExpr = AnnExpr<(u32, u32)>; + +#[derive(Clone, derive_more::Debug, PartialEq, Eq)] +#[debug("{_0:?}")] +pub struct RawExpr(pub Box>); + +pub fn strip_ann(expr: AnnExpr) -> RawExpr { + cata(expr, &|_, expr| RawExpr(Box::new(expr))) +} + +#[derive(Clone, Debug, PartialEq, Eq)] +pub enum Literal { + Bool(bool), + Int(BigInt), +} + +#[derive(Clone, Debug, PartialEq, Eq)] +pub enum Quantifier { + Forall, + Exists, +} + +#[derive(Clone, Debug, PartialEq, Eq)] +pub enum UnaryOp { + // neither + Dereference, + + // Arithmetic and Boolean + Not, +} + +#[derive(Clone, Debug, PartialEq, Eq)] +pub enum BinaryOp { + // pure Arithmetic (data -> data) + Mul, + Div, + Mod, + Add, + Sub, + ShiftLeft, + ShiftRight, + + // pure Predicates (data -> bool) + Eq, + Neq, + Lt, + Le, + Gt, + Ge, + + // pure Boolean (bool -> bool) + Implies, + + // Arithmentic and Boolean + And, + Or, + Xor, +} + +impl BinaryOp { + /// An operator is "arithmetic" if it performs an arithmetic operation + /// (e.g., +, -, *) and returns a value of the same numeric type as its operands. + pub fn is_arithmetic(&self) -> bool { + matches!(self, Self::Add | Self::Sub | Self::Mul | Self::Div | Self::Mod) + } + + /// An operator is "bitwise" if it performs a bitwise operation (e.g., &, |, ^). + /// In this language, these can operate on both integers and booleans. + pub fn is_bitwise(&self) -> bool { + matches!(self, Self::And | Self::Or | Self::Xor) + } + + /// An operator is a "shift" if it performs a bit shift (e.g., <<, >>). + /// These have unique type rules, requiring a numeric type on the left + /// and a `u8` on the right. + pub fn is_shift(&self) -> bool { + matches!(self, Self::ShiftLeft | Self::ShiftRight) + } + + /// An operator is a "comparison" if it compares two values and always returns a boolean. + pub fn is_comparison(&self) -> bool { + matches!(self, Self::Eq | Self::Neq | Self::Lt | Self::Le | Self::Gt | Self::Ge) + } + + /// An operator is "logical" if its operands are expected to be booleans. + /// This includes `==>` and the bitwise operators when used in a boolean context. + pub fn is_logical(&self) -> bool { + matches!(self, Self::Implies | Self::And | Self::Or) + } +} + +#[derive(Clone, Debug, PartialEq, Eq)] +pub struct Variable { + pub path: Vec, + pub name: Identifier, + pub id: Option, +} + +/* +* cata stuff +* */ + +pub fn fmap(expr: ExprF, cata_fn: &impl Fn(A) -> B) -> ExprF { + match expr { + ExprF::BinaryOp { op, expr_left, expr_right } => { + ExprF::BinaryOp { op, expr_left: cata_fn(expr_left), expr_right: cata_fn(expr_right) } + } + ExprF::UnaryOp { op, expr } => ExprF::UnaryOp { op, expr: cata_fn(expr) }, + ExprF::Parenthesised { expr } => ExprF::Parenthesised { expr: cata_fn(expr) }, + ExprF::Quantified { quantifier, variables, expr } => { + ExprF::Quantified { quantifier, variables, expr: cata_fn(expr) } + } + ExprF::FnCall { name, args } => { + ExprF::FnCall { name, args: args.into_iter().map(cata_fn).collect() } + } + ExprF::Index { expr, index } => ExprF::Index { expr: cata_fn(expr), index: cata_fn(index) }, + ExprF::TupleAccess { expr, index } => ExprF::TupleAccess { expr: cata_fn(expr), index }, + ExprF::StructureAccess { expr, field } => { + ExprF::StructureAccess { expr: cata_fn(expr), field } + } + ExprF::Cast { expr, target } => ExprF::Cast { expr: cata_fn(expr), target }, + ExprF::Literal { value } => ExprF::Literal { value }, + ExprF::Tuple { exprs } => { + ExprF::Tuple { exprs: exprs.into_iter().map(cata_fn).collect::>() } + } + ExprF::Array { exprs } => { + ExprF::Array { exprs: exprs.into_iter().map(cata_fn).collect::>() } + } + ExprF::Variable(Variable { path, name, id }) => { + ExprF::Variable(Variable { path, name, id }) + } + } +} + +fn try_fmap(expr: ExprF, cata_fn: &impl Fn(A) -> Result) -> Result, E> { + Ok(match expr { + ExprF::BinaryOp { op, expr_left, expr_right } => { + ExprF::BinaryOp { op, expr_left: cata_fn(expr_left)?, expr_right: cata_fn(expr_right)? } + } + ExprF::UnaryOp { op, expr } => ExprF::UnaryOp { op, expr: cata_fn(expr)? }, + ExprF::Parenthesised { expr } => ExprF::Parenthesised { expr: cata_fn(expr)? }, + ExprF::Quantified { quantifier, variables, expr } => { + ExprF::Quantified { quantifier, variables, expr: cata_fn(expr)? } + } + ExprF::FnCall { name, args } => { + let processed_args = args.into_iter().map(cata_fn).collect::, _>>()?; + ExprF::FnCall { name, args: processed_args } + } + ExprF::Index { expr, index } => { + ExprF::Index { expr: cata_fn(expr)?, index: cata_fn(index)? } + } + ExprF::TupleAccess { expr, index } => ExprF::TupleAccess { expr: cata_fn(expr)?, index }, + ExprF::StructureAccess { expr, field } => { + ExprF::StructureAccess { expr: cata_fn(expr)?, field } + } + ExprF::Cast { expr, target } => ExprF::Cast { expr: cata_fn(expr)?, target }, + ExprF::Literal { value } => ExprF::Literal { value }, + ExprF::Tuple { exprs } => { + ExprF::Tuple { exprs: exprs.into_iter().map(cata_fn).collect::, _>>()? } + } + ExprF::Array { exprs } => { + ExprF::Array { exprs: exprs.into_iter().map(cata_fn).collect::, _>>()? } + } + ExprF::Variable(Variable { path, name, id }) => { + ExprF::Variable(Variable { path, name, id }) + } + }) +} + +fn try_fmap_mut(expr: ExprF, cata_fn: &mut impl FnMut(A) -> Result) -> Result, E> { + Ok(match expr { + ExprF::BinaryOp { op, expr_left, expr_right } => { + ExprF::BinaryOp { op, expr_left: cata_fn(expr_left)?, expr_right: cata_fn(expr_right)? } + } + ExprF::UnaryOp { op, expr } => ExprF::UnaryOp { op, expr: cata_fn(expr)? }, + ExprF::Parenthesised { expr } => ExprF::Parenthesised { expr: cata_fn(expr)? }, + ExprF::Quantified { quantifier, variables, expr } => { + ExprF::Quantified { quantifier, variables, expr: cata_fn(expr)? } + } + ExprF::FnCall { name, args } => { + let processed_args = args.into_iter().map(cata_fn).collect::, _>>()?; + ExprF::FnCall { name, args: processed_args } + } + ExprF::Index { expr, index } => { + ExprF::Index { index: cata_fn(index)? , expr: cata_fn(expr)? } + } + ExprF::TupleAccess { expr, index } => ExprF::TupleAccess { expr: cata_fn(expr)?, index }, + ExprF::StructureAccess { expr, field } => { + ExprF::StructureAccess { expr: cata_fn(expr)?, field } + } + ExprF::Cast { expr, target } => ExprF::Cast { expr: cata_fn(expr)?, target }, + ExprF::Literal { value } => ExprF::Literal { value }, + ExprF::Tuple { exprs } => { + ExprF::Tuple { exprs: exprs.into_iter().map(cata_fn).collect::, _>>()? } + } + ExprF::Array { exprs } => { + ExprF::Array { exprs: exprs.into_iter().map(cata_fn).collect::, _>>()? } + } + ExprF::Variable(Variable { path, name, id }) => { + ExprF::Variable(Variable { path, name, id }) + } + }) +} + +pub fn cata(expr: AnnExpr, algebra: &impl Fn(A, ExprF) -> B) -> B { + let children_results = fmap(*expr.expr, &|child| cata(child, algebra)); + + algebra(expr.ann, children_results) +} + +pub fn try_cata( + expr: AnnExpr, + algebra: &impl Fn(A, ExprF) -> Result, +) -> Result { + let children_results = try_fmap(*expr.expr, &|child| try_cata(child, algebra))?; + + algebra(expr.ann, children_results) +} + +pub fn try_cata_mut( + expr: AnnExpr, + algebra: &mut impl FnMut(A, ExprF) -> Result, +) -> Result { + let children_results = try_fmap_mut(*expr.expr, &mut |child| try_cata_mut(child, algebra))?; + + algebra(expr.ann, children_results) +} + +pub fn try_contextual_cata( + expr: AnnExpr, + initial_context: C, + update_context: &impl Fn(C, &AnnExpr) -> C, + algebra: &impl Fn(A, C, ExprF) -> Result, +) -> Result +where + C: Clone, +{ + fn recurse( + expr: AnnExpr, + context: C, + update_context: &impl Fn(C, &AnnExpr) -> C, + algebra: &impl Fn(A, C, ExprF) -> Result, + ) -> Result + where + C: Clone, + { + let new_context = update_context(context, &expr); + + let children_results = try_fmap(*expr.expr, &|child_expr| { + recurse(child_expr, new_context.clone(), update_context, algebra) + })?; + + algebra(expr.ann, new_context, children_results) + } + + recurse(expr, initial_context, update_context, algebra) +} + +pub fn try_cata_recoverable( + expr: AnnExpr, + algebra: &impl Fn(A, Result, E>) -> Result, +) -> Result { + let children_results = try_fmap(*expr.expr, &|child| try_cata_recoverable(child, algebra)); + + algebra(expr.ann, children_results) +} + +impl Display for Quantifier { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + write!( + f, + "{}", + match self { + Quantifier::Forall => "forall", + Quantifier::Exists => "exists", + } + ) + } +} diff --git a/compiler/formal_verification/src/convert_structs.rs b/compiler/formal_verification/src/convert_structs.rs new file mode 100644 index 00000000000..4dcaad7835c --- /dev/null +++ b/compiler/formal_verification/src/convert_structs.rs @@ -0,0 +1,125 @@ +use std::collections::HashMap; + +use noirc_frontend::{ + ast::Ident, + hir::{resolution::errors::ResolverError, type_check::TypeCheckError}, +}; + +use crate::ast::{ExprF, SpannedExpr, try_cata_mut}; + +pub fn convert_struct_access_to_tuple_access( + expr: SpannedExpr, + parameters_hir_types: &HashMap, +) -> Result { + let mut last_important_type: Option = None; + + let res: SpannedExpr = + try_cata_mut(expr, &mut |loc, exprf| -> Result<_, ResolverOrTypeError> { + match exprf { + ExprF::Index { .. } => { + if let Some(last_type) = &last_important_type { + if let noirc_frontend::Type::Array(_size, inner_type) = last_type { + last_important_type = Some(*inner_type.clone()); + Ok(SpannedExpr { ann: loc, expr: Box::new(exprf) }) + } else { + // Error, tried to index a non array type + Err(ResolverOrTypeError::TypeError(TypeCheckError::TypeMismatch { + expr_typ: last_type.to_string(), + expected_typ: String::from("array"), + expr_location: loc, + })) + } + } else { + Ok(SpannedExpr { ann: loc, expr: Box::new(exprf) }) + } + } + ExprF::TupleAccess { ref index, .. } => { + if let Some(last_type) = &last_important_type { + if let noirc_frontend::Type::Tuple(inner_types) = last_type { + last_important_type = Some(inner_types[*index as usize].clone()); + Ok(SpannedExpr { ann: loc, expr: Box::new(exprf) }) + } else { + // Error, tried to index a non tuple + Err(ResolverOrTypeError::TypeError(TypeCheckError::TypeMismatch { + expr_typ: last_type.to_string(), + expected_typ: String::from("tuple"), + expr_location: loc, + })) + } + } else { + Ok(SpannedExpr { ann: loc, expr: Box::new(exprf) }) + } + } + ExprF::StructureAccess { expr, field } => { + if let Some(last_type) = last_important_type.take() { + if let noirc_frontend::Type::DataType(struct_type, _) = last_type { + if let Some((typ, _, index)) = + struct_type.borrow().get_field(&field, &[]) + { + last_important_type = Some(typ); + Ok(SpannedExpr { + ann: loc, + expr: Box::new(ExprF::TupleAccess { + expr: expr, + index: index as u32, + }), + }) + } else { + // Error tried to access a non existing field of a structure + Err(ResolverOrTypeError::ResolverError( + ResolverError::NoSuchField { + field: Ident::new(field, loc), + struct_definition: struct_type.borrow().name.clone(), + }, + )) + } + } else { + // Error, tried to access a field of a non struct type + Err(ResolverOrTypeError::TypeError(TypeCheckError::TypeMismatch { + expr_typ: last_type.to_string(), + expected_typ: String::from("structure"), + expr_location: loc, + })) + } + } else { + // Error, can't convert structure access to tuple access because + // of missing type information for inner expression + // Should be unreachable + unreachable!() + } + } + ExprF::Variable(ref var) => { + if let Some(var_typ) = parameters_hir_types.get(&var.name) { + last_important_type = Some(var_typ.clone()); + } else { + // NOTE: We are processing a quantifier index, therefore we don't have + // to keep track of its type because it's an integer + last_important_type = None; + } + Ok(SpannedExpr { ann: loc, expr: Box::new(exprf) }) + } + ExprF::Parenthesised { .. } + | ExprF::UnaryOp { op: crate::ast::UnaryOp::Dereference, .. } => { + Ok(SpannedExpr { ann: loc, expr: Box::new(exprf) }) + } + ExprF::BinaryOp { .. } + | ExprF::Quantified { .. } + | ExprF::FnCall { .. } + | ExprF::Cast { .. } + | ExprF::Literal { .. } + | ExprF::Tuple { .. } + | ExprF::Array { .. } + | ExprF::UnaryOp { .. } => { + last_important_type = None; + Ok(SpannedExpr { ann: loc, expr: Box::new(exprf) }) + } + } + })?; + + Ok(res) +} + +pub enum ResolverOrTypeError { + ResolverError(ResolverError), + TypeError(TypeCheckError), +} diff --git a/compiler/formal_verification/src/inline_globals.rs b/compiler/formal_verification/src/inline_globals.rs new file mode 100644 index 00000000000..977d1c8ee9f --- /dev/null +++ b/compiler/formal_verification/src/inline_globals.rs @@ -0,0 +1,152 @@ +use noirc_errors::Location; +use noirc_frontend::{ + ast::Ident, + hir::{ + comptime::Value, + resolution::{errors::ResolverError, import::PathResolutionError}, + }, + node_interner::GlobalValue, +}; +use num_bigint::{BigInt, BigUint, Sign}; +use std::collections::HashMap; + +use crate::ast::{AnnExpr, ExprF, Literal, SpannedExpr, try_cata}; + +/// Replaces all global identifiers with their resolved constant value. +pub fn inline_global_consts( + expr: SpannedExpr, + pathed_globals_with_values: &HashMap, + function_parameters: &[&str], +) -> Result { + try_cata(expr, &|loc, exprf| -> Result<_, ResolverError> { + match exprf { + ExprF::Variable(variable) => { + // --- Guard 1: Handle function parameters first --- + // Parameters have the highest precedence and are never inlined. + let is_parameter = variable.path.is_empty() + && function_parameters.contains(&variable.name.as_str()); + + if is_parameter { + // It's a parameter. Leave it as is and we're done with this variable. + return Ok(SpannedExpr { ann: loc, expr: Box::new(ExprF::Variable(variable)) }); + } + + // --- Guard 2: Try to resolve as a global constant --- + // At this point, we know it's not a shadowed parameter. + let full_path = join_path_segments(variable.path.clone(), variable.name.clone()); + if let Some(global_val) = pathed_globals_with_values.get(&full_path) { + // It's a valid global. Inline it. + return match global_val { + GlobalValue::Unresolved | GlobalValue::Resolving => { + unreachable!("All global constants must have been resolved by now") + } + GlobalValue::Resolved(value) => { + let global_const_as_exprf = resolved_value_to_exprf(value, loc)?; + Ok(SpannedExpr { ann: loc, expr: Box::new(global_const_as_exprf) }) + } + }; + } + + // --- Guard 3: Check for invalid, unresolved paths --- + // It's not a parameter and not a known global. If it has a path, it's an error. + if !variable.path.is_empty() { + return Err(ResolverError::PathResolutionError( + PathResolutionError::Unresolved(Ident::new(full_path, loc)), + )); + } + + // --- Default Case --- + // If none of the guards above returned, the variable must be a local identifier + // that is not a parameter (e.g., `result`, quantifier, or undeclared variable). + // We leave it as is for a later compiler stage to handle. + Ok(SpannedExpr { ann: loc, expr: Box::new(ExprF::Variable(variable)) }) + } + // For any other expression type, just reconstruct it. + _ => Ok(SpannedExpr { ann: loc, expr: Box::new(exprf) }), + } + }) +} + +fn resolved_value_to_exprf( + value: &Value, + location: Location, +) -> Result>, ResolverError> { + Ok(match value { + Value::Unit => ExprF::Tuple { exprs: Vec::new() }, + Value::Bool(bool_val) => ExprF::Literal { value: Literal::Bool(*bool_val) }, + Value::Field(signed_field) => { + let field_as_big_uint: BigUint = signed_field.to_field_element().into_repr().into(); + ExprF::Literal { + value: Literal::Int(BigInt::from_biguint(Sign::Plus, field_as_big_uint)), + } + } + Value::I8(integer) => ExprF::Literal { value: Literal::Int(BigInt::from(*integer)) }, + Value::I16(integer) => ExprF::Literal { value: Literal::Int(BigInt::from(*integer)) }, + Value::I32(integer) => ExprF::Literal { value: Literal::Int(BigInt::from(*integer)) }, + Value::I64(integer) => ExprF::Literal { value: Literal::Int(BigInt::from(*integer)) }, + Value::U1(integer) => ExprF::Literal { value: Literal::Int(BigInt::from(*integer)) }, + Value::U8(integer) => ExprF::Literal { value: Literal::Int(BigInt::from(*integer)) }, + Value::U16(integer) => ExprF::Literal { value: Literal::Int(BigInt::from(*integer)) }, + Value::U32(integer) => ExprF::Literal { value: Literal::Int(BigInt::from(*integer)) }, + Value::U64(integer) => ExprF::Literal { value: Literal::Int(BigInt::from(*integer)) }, + Value::U128(integer) => ExprF::Literal { value: Literal::Int(BigInt::from(*integer)) }, + Value::Tuple(values) => { + let exprs = values + .iter() + .map(|val| { + let exprf = resolved_value_to_exprf(val, location)?; + Ok(SpannedExpr { ann: location, expr: Box::new(exprf) }) + }) + .collect::>()?; + ExprF::Tuple { exprs } + } + Value::Array(values, _) => { + let exprs = values + .iter() + .map(|val| { + let exprf = resolved_value_to_exprf(val, location)?; + Ok(SpannedExpr { ann: location, expr: Box::new(exprf) }) + }) + .collect::>()?; + ExprF::Array { exprs } + } + Value::String(..) + | Value::FormatString(..) + | Value::CtString(..) + // We currently don't support strings in formal verification + | Value::Function(..) + | Value::Closure(..) + | Value::Struct(..) + | Value::Enum(..) + | Value::Pointer(..) + | Value::Slice(..) + | Value::Quoted(..) + | Value::TypeDefinition(..) + | Value::TraitConstraint(..) + | Value::TraitDefinition(..) + | Value::TraitImpl(..) + | Value::FunctionDefinition(..) + | Value::ModuleDefinition(..) + | Value::Type(..) + | Value::Zeroed(..) + | Value::Expr(..) + | Value::TypedExpr(..) + | Value::UnresolvedType(..) => { + // We believe that all global const values are resolved + return Err(ResolverError::UnevaluatedGlobalType { location }); + } + }) +} + +/// Joins path segments and an identifier into a single "::" delimited string. +/// +/// # Arguments +/// * `path_parts` - A vector of strings for the path's base (e.g., ["super", "foo"]). +/// * `identifier` - The final identifier to append (e.g., "bar"). +/// +/// # Returns +/// A single string like "super::foo::bar". +fn join_path_segments(mut path_parts: Vec, identifier: String) -> String { + path_parts.push(identifier); + path_parts.join("::") +} diff --git a/compiler/formal_verification/src/lib.rs b/compiler/formal_verification/src/lib.rs new file mode 100644 index 00000000000..83c0a53322c --- /dev/null +++ b/compiler/formal_verification/src/lib.rs @@ -0,0 +1,45 @@ +use noirc_errors::Location; +use noirc_frontend::monomorphization::ast as mast; +use std::{cell::RefCell, collections::BTreeMap, fmt::Debug, rc::Rc}; +use typing::OptionalType; + +use crate::{ + ast::{OffsetExpr, SpannedExpr, cata}, + parse::build_location, +}; + +// NOTE: all types inside are not prefixed, to be used as `ast::OffsetExpr` +pub mod ast; +pub mod convert_structs; +pub mod inline_globals; +pub mod parse; +pub mod type_conversion; +pub mod typing; + +#[derive(Debug)] +pub struct State<'a> { + pub function: &'a mast::Function, + pub global_constants: &'a BTreeMap, + pub functions: &'a BTreeMap, + pub min_local_id: Rc>, +} + +#[derive(Debug, Clone)] +pub enum Attribute { + Ghost, + Ensures(ast::SpannedExpr), + Requires(ast::SpannedExpr), +} + +#[derive(Debug, Clone)] +pub struct MonomorphizationRequest { + pub function_identifier: String, + pub param_types: Vec, +} + +fn span_expr(annotation_location: Location, full_length: u32, expr: OffsetExpr) -> SpannedExpr { + cata(expr, &|(prev_offset, after_offset), exprf| SpannedExpr { + ann: build_location(annotation_location, full_length, prev_offset, after_offset), + expr: Box::new(exprf), + }) +} diff --git a/compiler/formal_verification/src/parse.rs b/compiler/formal_verification/src/parse.rs new file mode 100644 index 00000000000..d8fa1f57ae0 --- /dev/null +++ b/compiler/formal_verification/src/parse.rs @@ -0,0 +1,1326 @@ +use noirc_errors::{Location, Span}; +use noirc_frontend::{ + ast::IntegerBitSize, + monomorphization::ast::{self as mast, Type as NoirType}, + shared::Signedness, +}; +use nom::{ + Err as NomErr, IResult, Parser, + branch::alt, + bytes::complete::{tag, take_while, take_while1}, + character::complete::{digit1 as digit, multispace0 as multispace, multispace1}, + combinator::{cut, map, not, opt, recognize, value}, + error::context, + multi::{many0, separated_list0, separated_list1}, + sequence::{delimited, pair, preceded, terminated}, +}; +use num_bigint::{BigInt, BigUint, Sign}; +use std::collections::BTreeMap; + +pub mod errors; +use errors::{ + Error, ParserError, ParserErrorKind, ParserErrorWithLocation, build_error, expect, map_nom_err, +}; + +use crate::{ + Attribute, + ast::{BinaryOp, ExprF, Identifier, Literal, OffsetExpr, Quantifier, UnaryOp, Variable}, + span_expr, +}; + +pub type Input<'a> = &'a str; +pub type PResult<'a, T> = IResult, T, Error>; + +pub(crate) fn build_location( + annotation_location: Location, + full_length: u32, + prev_offset: u32, + after_offset: u32, +) -> Location { + Location { + span: Span::inclusive( + annotation_location.span.start() + full_length - prev_offset, + annotation_location.span.start() + full_length - after_offset, + ), + file: annotation_location.file, + } +} + +pub(crate) fn build_expr( + prev_offset: usize, + after_offset: usize, + exprf: ExprF, +) -> OffsetExpr { + OffsetExpr { ann: (prev_offset as u32, after_offset as u32), expr: Box::new(exprf) } +} + +pub(crate) fn build_offset_from_exprs(left: &OffsetExpr, right: &OffsetExpr) -> (u32, u32) { + (left.ann.0, right.ann.1) +} + +/************************************************************************* +* Main parser combinators, in order of precedence, like in upstream Noir * +**************************************************************************/ + +pub fn parse_attribute<'a>( + annotation: &'a str, + location: Location, + _function: &'a mast::Function, + _global_constants: &'a BTreeMap, + _functions: &'a BTreeMap, +) -> Result, Vec)> { + let locate_parser_error = |parser_error: ParserError| ParserErrorWithLocation { + location: build_location( + location, + annotation.len() as u32, + parser_error.offset, + parser_error.offset, // This span is inclusive + ), + kind: parser_error.kind.clone(), + }; + + let convert_nom_error = |nom_err: Error| -> (Vec, Vec) { + (nom_err.parser_errors.into_iter().map(locate_parser_error).collect(), nom_err.contexts) + }; + + let (input, ident) = match expect("attribute name", parse_identifier)(annotation) { + Ok(result) => result, + Err(nom_err) => { + return Err(convert_nom_error(match nom_err { + NomErr::Error(e) | NomErr::Failure(e) => e, + NomErr::Incomplete(_) => build_error( + annotation, + ParserErrorKind::Message("Incomplete input".to_string()), + ), + })); + } + }; + + match ident { + "ghost" => { + if !input.is_empty() { + return Err(convert_nom_error(build_error( + input, + ParserErrorKind::Message(format!( + "Unexpected input after 'ghost' attribute: '{}'", + input + )), + ))); + } + Ok(Attribute::Ghost) + } + "ensures" | "requires" => { + let mut expr_parser = delimited( + preceded(multispace, expect("'('", tag("("))), + delimited(multispace, parse_expression, multispace), + cut(expect("')'", tag(")"))), + ); + + match expr_parser.parse(input) { + Ok((rest, expr)) => { + if !rest.is_empty() { + return Err(convert_nom_error(build_error( + rest, + ParserErrorKind::Message(format!( + "Unexpected trailing input: '{}'", + rest + )), + ))); + } + let spanned_expr = span_expr(location, annotation.len() as u32, expr); + if ident == "ensures" { + Ok(Attribute::Ensures(spanned_expr)) + } else { + Ok(Attribute::Requires(spanned_expr)) + } + } + Err(nom_err) => match nom_err { + NomErr::Error(e) | NomErr::Failure(e) => Err(convert_nom_error(e)), + NomErr::Incomplete(_) => Err(convert_nom_error(build_error( + input, + ParserErrorKind::Message("Incomplete input".to_string()), + ))), + }, + } + } + unknown => { + let err_kind = ParserErrorKind::UnknownAttribute(unknown.to_string()); + Err(convert_nom_error(build_error(annotation, err_kind))) + } + } +} + +pub(crate) fn parse_expression<'a>(input: Input<'a>) -> PResult<'a, OffsetExpr> { + // NOTE: we start parsing from the highest precedence operator + parse_implication_expr(input) +} + +pub(crate) fn parse_implication_expr<'a>(input: Input<'a>) -> PResult<'a, OffsetExpr> { + let (mut input, mut expr_left) = parse_equality_expr(input)?; + loop { + let (next_input, remainder) = opt(context( + "implication", + pair( + delimited( + multispace, + expect("'==>'", tag("==>").map(|_| BinaryOp::Implies)), + multispace, + ), + cut(parse_equality_expr), + ), + )) + .parse(input)?; + + if let Some((op, expr_right)) = remainder { + expr_left = OffsetExpr { + ann: build_offset_from_exprs(&expr_left, &expr_right), + expr: Box::new(ExprF::BinaryOp { op, expr_left, expr_right }), + }; + input = next_input; + } else { + return Ok((input, expr_left)); + } + } +} + +pub(crate) fn parse_equality_expr<'a>(input: Input<'a>) -> PResult<'a, OffsetExpr> { + let (mut input, mut expr_left) = parse_or_expr(input)?; + + loop { + let (next_input, remainder) = opt( + // Re-introduce `context` here to wrap the operator and RHS parser + context( + "equality expression", // The context name for error messages + pair( + delimited( + multispace, + expect( + "'==' or '!='", + alt(( + // NOTE: We need to check that the immediate next character after + // the `==` is not `>`, otherwise, we'll `cut` into trying to + // parse it a normal expression while it should actually be + // parsed as implication (`==>`) + terminated(tag("=="), not(tag(">"))).map(|_| BinaryOp::Eq), + tag("!=").map(|_| BinaryOp::Neq), + )), + ), + multispace, + ), + cut(parse_or_expr), + ), + ), + ) + .parse(input)?; + + if let Some((op, expr_right)) = remainder { + expr_left = OffsetExpr { + ann: build_offset_from_exprs(&expr_left, &expr_right), + expr: Box::new(ExprF::BinaryOp { op, expr_left, expr_right }), + }; + input = next_input; + } else { + return Ok((input, expr_left)); + } + } +} + +pub(crate) fn parse_or_expr<'a>(input: Input<'a>) -> PResult<'a, OffsetExpr> { + let (mut input, mut expr_left) = parse_and_expr(input)?; + loop { + let (next_input, remainder) = opt(context( + "or", + pair( + delimited(multispace, expect("'|'", tag("|").map(|_| BinaryOp::Or)), multispace), + cut(parse_and_expr), + ), + )) + .parse(input)?; + + if let Some((op, expr_right)) = remainder { + expr_left = OffsetExpr { + ann: build_offset_from_exprs(&expr_left, &expr_right), + expr: Box::new(ExprF::BinaryOp { op, expr_left, expr_right }), + }; + input = next_input; + } else { + return Ok((input, expr_left)); + } + } +} + +pub(crate) fn parse_and_expr<'a>(input: Input<'a>) -> PResult<'a, OffsetExpr> { + let (mut input, mut expr_left) = parse_xor_expr(input)?; + loop { + let (next_input, remainder) = opt(context( + "and", + pair( + delimited(multispace, expect("'&'", tag("&").map(|_| BinaryOp::And)), multispace), + cut(parse_xor_expr), + ), + )) + .parse(input)?; + + if let Some((op, expr_right)) = remainder { + expr_left = OffsetExpr { + ann: build_offset_from_exprs(&expr_left, &expr_right), + expr: Box::new(ExprF::BinaryOp { op, expr_left, expr_right }), + }; + input = next_input; + } else { + return Ok((input, expr_left)); + } + } +} + +pub(crate) fn parse_xor_expr<'a>(input: Input<'a>) -> PResult<'a, OffsetExpr> { + let (mut input, mut expr_left) = parse_comparison_expr(input)?; + loop { + let (next_input, remainder) = opt(context( + "xor", + pair( + delimited(multispace, expect("'^'", tag("^").map(|_| BinaryOp::Xor)), multispace), + cut(parse_comparison_expr), + ), + )) + .parse(input)?; + + if let Some((op, expr_right)) = remainder { + expr_left = OffsetExpr { + ann: build_offset_from_exprs(&expr_left, &expr_right), + expr: Box::new(ExprF::BinaryOp { op, expr_left, expr_right }), + }; + input = next_input; + } else { + return Ok((input, expr_left)); + } + } +} +pub(crate) fn parse_comparison_expr<'a>(input: Input<'a>) -> PResult<'a, OffsetExpr> { + let (input, mut expr_left) = parse_shift_expr(input)?; + + // Comparison operators are not associative (e.g., `a < b < c` is invalid), + // so we just look for one optional occurrence. + if let (input, Some((op, expr_right))) = opt(pair( + delimited( + multispace, + expect( + "'<=', '>=', '<' or '>'".to_string(), + alt(( + tag("<=").map(|_| BinaryOp::Le), + tag(">=").map(|_| BinaryOp::Ge), + tag("<").map(|_| BinaryOp::Lt), + tag(">").map(|_| BinaryOp::Gt), + )), + ), + multispace, + ), + // NOTE: If an operator was found, the RHS is now MANDATORY. `cut` enforces this. + cut(parse_shift_expr), + )) + .parse(input)? + { + expr_left = OffsetExpr { + ann: build_offset_from_exprs(&expr_left, &expr_right), + expr: Box::new(ExprF::BinaryOp { op, expr_left, expr_right }), + }; + return Ok((input, expr_left)); + } + + Ok((input, expr_left)) +} + +pub(crate) fn parse_shift_expr<'a>(input: Input<'a>) -> PResult<'a, OffsetExpr> { + let (input, mut expr_left) = parse_additive_expr(input)?; + + if let (input, Some((op, expr_right))) = opt(pair( + delimited( + multispace, + expect( + "'<<' or '>>'", + alt(( + tag("<<").map(|_| BinaryOp::ShiftLeft), + tag(">>").map(|_| BinaryOp::ShiftRight), + )), + ), + multispace, + ), + cut(parse_additive_expr), + )) + .parse(input)? + { + expr_left = OffsetExpr { + ann: build_offset_from_exprs(&expr_left, &expr_right), + expr: Box::new(ExprF::BinaryOp { op, expr_left, expr_right }), + }; + return Ok((input, expr_left)); + } + + Ok((input, expr_left)) +} + +pub(crate) fn parse_additive_expr<'a>(input: Input<'a>) -> PResult<'a, OffsetExpr> { + let (mut input, mut expr_left) = parse_multiplicative_expr(input)?; + + loop { + let (next_input, remainder) = opt(pair( + delimited( + multispace, + expect( + "'+' or '-'", + alt((tag("+").map(|_| BinaryOp::Add), tag("-").map(|_| BinaryOp::Sub))), + ), + multispace, + ), + cut(parse_multiplicative_expr), + )) + .parse(input)?; + + if let Some((op, expr_right)) = remainder { + expr_left = OffsetExpr { + ann: build_offset_from_exprs(&expr_left, &expr_right), + expr: Box::new(ExprF::BinaryOp { op, expr_left, expr_right }), + }; + input = next_input; + } else { + return Ok((input, expr_left)); + } + } +} + +pub(crate) fn parse_multiplicative_expr<'a>(input: Input<'a>) -> PResult<'a, OffsetExpr> { + let (mut input, mut expr_left) = parse_prefix_expr(input)?; + + loop { + let (next_input, remainder) = opt(pair( + delimited( + multispace, + expect( + "'*', '/', or '%'", + alt(( + tag("*").map(|_| BinaryOp::Mul), + tag("/").map(|_| BinaryOp::Div), + tag("%").map(|_| BinaryOp::Mod), + )), + ), + multispace, + ), + cut(parse_prefix_expr), + )) + .parse(input)?; + + if let Some((op, expr_right)) = remainder { + expr_left = OffsetExpr { + ann: build_offset_from_exprs(&expr_left, &expr_right), + expr: Box::new(ExprF::BinaryOp { op, expr_left, expr_right }), + }; + input = next_input; + } else { + return Ok((input, expr_left)); + } + } +} + +pub(crate) enum Prefix { + Dereference, + Not, +} + +pub(crate) fn parse_prefix_expr<'a>(input: Input<'a>) -> PResult<'a, OffsetExpr> { + let prev_offset = input.len(); + + let (input, prefixes) = context("prefix", many0(parse_any_prefix)).parse(input)?; + + let (input, base_expr) = parse_postfix_expr(input)?; + + let after_offset = input.len(); + + let final_expr = prefixes.into_iter().rev().fold(base_expr, |inner_expr, prefix| { + let expr_f = match prefix { + Prefix::Dereference => ExprF::UnaryOp { op: UnaryOp::Dereference, expr: inner_expr }, + Prefix::Not => ExprF::UnaryOp { op: UnaryOp::Not, expr: inner_expr }, + }; + build_expr(prev_offset, after_offset, expr_f) + }); + + Ok((input, final_expr)) +} + +pub(crate) fn parse_any_prefix<'a>(input: Input<'a>) -> PResult<'a, Prefix> { + alt(( + // + context( + "dereference", + terminated(expect("'*'", tag("*")), multispace).map(|_| Prefix::Dereference), + ), + context("not", terminated(expect("'!'", tag("!")), multispace).map(|_| Prefix::Not)), + )) + .parse(input) +} + +pub(crate) enum Postfix { + ArrayIndex(OffsetExpr), + TupleMember(BigInt), + Cast(CastTargetType), + FieldAccess(Identifier), +} + +pub(crate) enum CastTargetType { + Field, + Integer(Signedness, IntegerBitSize), + Bool, +} + +pub(crate) fn parse_postfix_expr<'a>(input: Input<'a>) -> PResult<'a, OffsetExpr> { + let prev_offset = input.len(); + + let (mut input, mut expr_base) = parse_atom_expr(input)?; + + loop { + // `cut` ensures that if we see a `.` or `[` but the rest is invalid, we get a hard error. + let (next_input, suffix) = cut(opt(parse_any_suffix)).parse(input)?; + + if let Some(s) = suffix { + let after_offset = next_input.len(); + + expr_base = match s { + Postfix::ArrayIndex(index_expr) => build_expr( + prev_offset, + after_offset, + ExprF::Index { expr: expr_base, index: index_expr }, + ), + Postfix::TupleMember(index) => { + let index_u32 = index.try_into().map_err(|_| { + NomErr::Error(build_error(input, ParserErrorKind::InvalidTupleIndex)) + })?; + build_expr( + prev_offset, + after_offset, + ExprF::TupleAccess { expr: expr_base, index: index_u32 }, + ) + } + Postfix::FieldAccess(field) => build_expr( + prev_offset, + after_offset, + ExprF::StructureAccess { expr: expr_base, field }, + ), + Postfix::Cast(target_type) => build_expr( + prev_offset, + after_offset, + ExprF::Cast { + expr: expr_base, + target: match target_type { + CastTargetType::Field => NoirType::Field, + CastTargetType::Integer(s, b) => NoirType::Integer(s, b), + CastTargetType::Bool => NoirType::Bool, + }, + }, + ), + }; + + input = next_input; + } else { + return Ok((input, expr_base)); + } + } +} + +pub(crate) fn parse_any_suffix<'a>(input: Input<'a>) -> PResult<'a, Postfix> { + alt(( + context("index", map(parse_index_suffix, Postfix::ArrayIndex)), + context("member", map(parse_member_suffix, Postfix::TupleMember)), + context("struct_field", map(parse_field_access_suffix, Postfix::FieldAccess)), + context("cast", map(parse_cast_suffix, Postfix::Cast)), + )) + .parse(input) +} + +pub(crate) fn parse_index_suffix<'a>(input: Input<'a>) -> PResult<'a, OffsetExpr> { + preceded( + multispace, + delimited( + expect("'[".to_string(), tag("[")), + cut(delimited(multispace, parse_expression, multispace)), + expect("']'".to_string(), tag("]")), + ), + ) + .parse(input) +} + +pub(crate) fn parse_member_suffix<'a>(input: Input<'a>) -> PResult<'a, BigInt> { + preceded(pair(multispace, expect("'.' for tuple access".to_string(), tag("."))), parse_int) + .parse(input) +} + +pub(crate) fn parse_field_access_suffix<'a>(input: Input<'a>) -> PResult<'a, String> { + map( + preceded( + pair(multispace, expect("'.' for field access".to_string(), tag("."))), + cut(parse_identifier), + ), + |s: &str| s.to_string(), + ) + .parse(input) +} + +pub(crate) fn parse_cast_suffix<'a>(input: Input<'a>) -> PResult<'a, CastTargetType> { + let (input, type_ident) = preceded( + expect("'as'", delimited(multispace1, tag("as"), multispace1)), + cut(parse_identifier), + ) + .parse(input)?; + + if type_ident == "Field" { + return Ok((input, CastTargetType::Field)); + } + + if type_ident == "bool" { + return Ok((input, CastTargetType::Bool)); + } + + if let Some((signedness @ ("i" | "u"), size)) = type_ident.split_at_checked(1) { + return Ok(( + input, + CastTargetType::Integer( + match signedness { + "i" => Signedness::Signed, + "u" => Signedness::Unsigned, + _ => unreachable!(), + }, + match size { + "1" => IntegerBitSize::One, + "8" => IntegerBitSize::Eight, + "16" => IntegerBitSize::Sixteen, + "32" => IntegerBitSize::ThirtyTwo, + "64" => IntegerBitSize::SixtyFour, + "128" => IntegerBitSize::HundredTwentyEight, + _ => { + return Err(NomErr::Error(build_error( + size, + ParserErrorKind::InvalidIntegerLiteral, + ))); + } + }, + ), + )); + } + + Err(NomErr::Error(build_error(type_ident, ParserErrorKind::InvalidIntegerLiteral))) +} + +pub(crate) fn parse_atom_expr<'a>(input: Input<'a>) -> PResult<'a, OffsetExpr> { + alt(( + context("parenthesised or tuple", parse_parenthesised_or_tuple_expr), + context("quantifier", parse_quantifier_expr), + context("fn_call", parse_fn_call_expr), + // context("member", parse_member_expr), + // context("method_call", parse_method_call_expr), + context("array", parse_array_expr), + context("literal", parse_literal_expr), + context("var", parse_var_expr), + )) + .parse(input) +} + +pub(crate) fn parse_parenthesised_or_tuple_expr<'a>(input: Input<'a>) -> PResult<'a, OffsetExpr> { + let prev_offset = input.len(); + + // NOTE: Both parenthesised and tuple expressions have a starting `(` + let (input, (exprs, trailing_comma)) = delimited( + pair(expect("(", tag("(")), multispace), + // NOTE: Inside, we have a list of 0 or more expressions separated by commas... + pair( + separated_list0( + delimited(multispace, expect(",", tag(",")), multispace), + parse_expression, + ), + // NOTE: ...with an optional trailing comma + opt(delimited(multispace, tag(","), multispace)), + ), + pair(multispace, cut(expect(")", tag(")")))), + ) + .parse(input)?; + + let after_offset = input.len(); + + let result_expr = if let Some((only, [])) = exprs.split_first() + && trailing_comma.is_none() + { + // NOTE: + // Special case: exactly one expression and NO comma + // This is a parenthesized expression + build_expr(prev_offset, after_offset, ExprF::Parenthesised { expr: only.clone() }) + } else { + // NOTE: + // All other cases are tuples: + // - `()` -> 0 expressions + // - `(1,)` -> 1 expression with a trailing comma + // - `(1, 2)` -> 2 expressions + build_expr(prev_offset, after_offset, ExprF::Tuple { exprs }) + }; + + Ok((input, result_expr)) +} + +pub(crate) fn parse_quantifier_expr<'a>(input: Input<'a>) -> PResult<'a, OffsetExpr> { + let prev_offset = input.len(); + let (input, quantifier) = context("quantifier keyword", parse_quantifier_kind).parse(input)?; + + let (input, _) = multispace(input)?; + let (input, (variables, expr)) = delimited( + expect("'('".to_string(), tag("(")), + cut(pair( + delimited( + expect("'|'".to_string(), pair(tag("|"), multispace)), + // NOTE: unlike functions, quantifiers need to have at least one bound variable + cut(separated_list1( + delimited(multispace, expect("','".to_string(), tag(",")), multispace), + parse_identifier, + )), + expect("'|'".to_string(), pair(multispace, tag("|"))), + ), + delimited(multispace, parse_expression, multispace), + )), + expect("')'".to_string(), tag(")")), + ) + .parse(input)?; + let after_offset = input.len(); + + Ok(( + input, + build_expr( + prev_offset, + after_offset, + ExprF::Quantified { + quantifier, + variables: variables + .into_iter() + .map(|name| Variable { path: vec![], name: name.to_string(), id: None }) + .collect(), + expr, + }, + ), + )) +} + +fn parse_quantifier_kind<'a>(input: Input<'a>) -> PResult<'a, Quantifier> { + let (input, ident) = parse_identifier(input)?; + match ident { + "forall" => Ok((input, Quantifier::Forall)), + "exists" => Ok((input, Quantifier::Exists)), + // NOTE: If the identifier is not a valid quantifier, fail with a specific error + _ => Err(NomErr::Error(build_error( + input, + ParserErrorKind::InvalidQuantifier(ident.to_string()), + ))), + } +} + +pub(crate) fn parse_fn_call_expr<'a>(input: Input<'a>) -> PResult<'a, OffsetExpr> { + let prev_offset = input.len(); + let (input, name) = context("fn_call name", parse_identifier).parse(input)?; + + let (input, params) = delimited( + expect("'('".to_string(), tag("(")), + cut(separated_list0( + delimited(multispace, expect("','".to_string(), tag(",")), multispace), + parse_expression, + )), + expect("')'", tag(")")), + ) + .parse(input)?; + let after_offset = input.len(); + + Ok(( + input, + build_expr( + prev_offset, + after_offset, + ExprF::FnCall { name: name.to_string(), args: params }, + ), + )) +} + +pub(crate) fn parse_array_expr<'a>(input: Input<'a>) -> PResult<'a, OffsetExpr> { + let prev_offset = input.len(); + + let (input, exprs) = delimited( + expect("[", tag("[")), + separated_list0(delimited(multispace, expect(",", tag(",")), multispace), parse_expression), + cut(expect("]", tag("]"))), + ) + .parse(input)?; + + let after_offset = input.len(); + + let result_expr = build_expr(prev_offset, after_offset, ExprF::Array { exprs }); + + Ok((input, result_expr)) +} + +pub(crate) fn parse_literal_expr<'a>(input: Input<'a>) -> PResult<'a, OffsetExpr> { + let prev_offset = input.len(); + let (input, exprf) = alt(( + map(parse_bool, |b| ExprF::Literal { value: Literal::Bool(b) }), + map(parse_int, |bi| ExprF::Literal { value: Literal::Int(bi) }), + )) + .parse(input)?; + + let after_offset = input.len(); + + let res = build_expr(prev_offset, after_offset, exprf); + + Ok((input, res)) +} + +pub(crate) fn parse_bool<'a>(input: Input<'a>) -> PResult<'a, bool> { + expect("boolean 'true' or 'false'", alt((value(true, tag("true")), value(false, tag("false"))))) + .parse(input) +} + +pub(crate) fn parse_int<'a>(input: Input<'a>) -> PResult<'a, BigInt> { + let (input, sign) = parse_sign(input)?; + + let (input, digits) = expect("an integer".to_string(), digit)(input)?; + + let biguint = digits + .chars() + .map(|c| c.to_digit(10).expect("`digit1` should return digits")) + .fold(BigUint::ZERO, |acc, d| acc * 10u8 + d); + + let bigint = BigInt::from_biguint( + match sign { + true => Sign::Plus, + false => Sign::Minus, + }, + biguint, + ); + + Ok((input, bigint)) +} + +pub(crate) fn parse_sign<'a>(input: Input<'a>) -> PResult<'a, bool> { + let (input, opt_sign) = opt(map_nom_err( + alt((value(false, tag("-")), value(true, tag("+")))), + |_| ParserErrorKind::Message("Should not fail".to_string()), // NOTE: `opt` makes this effectively infallible + )) + .parse(input)?; + let sign = opt_sign.unwrap_or(true); + Ok((input, sign)) +} + +const FORBIDDEN_IDENTIFIERS: &[&str] = &["forall", "exists"]; + +pub(crate) fn parse_var_expr<'a>(input: Input<'a>) -> PResult<'a, OffsetExpr> { + let prev_offset = input.len(); + + // Wrapper of `parse_identifier` that denies some identifiers + let path_segment_parser = |input: Input<'a>| -> PResult<'a, &'a str> { + let (input, ident) = parse_identifier(input)?; + + if FORBIDDEN_IDENTIFIERS.contains(&ident) { + return Err(NomErr::Error(build_error( + input, + ParserErrorKind::Message(format!( + "The keyword `{}` cannot be used as an identifier", + ident + )), + ))); + } + + Ok((input, ident)) + }; + + let (input, all_path_segments) = + separated_list1(expect("'::'", tag("::")), path_segment_parser).parse(input)?; + + let after_offset = input.len(); + + let (&name, path) = + all_path_segments.split_last().expect("`separated_list1` should return a non-empty `Vec`"); + + Ok(( + input, + build_expr( + prev_offset, + after_offset, + ExprF::Variable(Variable { + path: path.into_iter().map(|&s| s.to_string()).collect(), + name: name.to_string(), + id: None, + }), + ), + )) +} + +pub(crate) fn parse_identifier<'a>(input: Input<'a>) -> PResult<'a, &'a str> { + fn is_valid_start(c: char) -> bool { + c.is_ascii_alphabetic() || c == '_' + } + + fn is_valid_char(c: char) -> bool { + c.is_ascii_alphanumeric() || c == '_' + } + + let identifier_parser = recognize(pair(take_while1(is_valid_start), take_while(is_valid_char))); + + expect("an identifier".to_string(), identifier_parser)(input) +} + +#[cfg(test)] +pub mod tests { + use std::{cell::RefCell, rc::Rc}; + + use noirc_frontend::{ + monomorphization::ast::{ + Expression, FuncId, Function, InlineType, LocalId, Type as NoirType, + }, + shared::Visibility, + }; + + use crate::{ + Attribute, State, + ast::{Literal, cata, strip_ann}, + }; + + use super::*; + + pub fn empty_state() -> State<'static> { + State { + function: Box::leak(Box::new(Function { + id: FuncId(4321), + name: "tutmanik".to_string(), + parameters: vec![ + ( + LocalId(0), + false, + "a".to_string(), + NoirType::Integer( + noirc_frontend::shared::Signedness::Signed, + noirc_frontend::ast::IntegerBitSize::ThirtyTwo, + ), + Visibility::Public, + ), + (LocalId(1), false, "kek".to_string(), NoirType::Unit, Visibility::Public), + ( + LocalId(2), + false, + "Banica_123_".to_string(), + NoirType::Bool, + Visibility::Public, + ), + ( + LocalId(3), + false, + "xs".to_string(), + NoirType::Array(3, Box::new(NoirType::Field)), + Visibility::Public, + ), + ( + LocalId(3), + false, + "rxs".to_string(), + NoirType::Reference( + Box::new(NoirType::Array(3, Box::new(NoirType::Field))), + false, + ), + Visibility::Public, + ), + ( + LocalId(4), + false, + "user".to_string(), + NoirType::Tuple(vec![NoirType::Bool, NoirType::Unit]), + Visibility::Public, + ), + ( + LocalId(5), + false, + "pair".to_string(), + NoirType::Tuple(vec![ + NoirType::Integer(Signedness::Unsigned, IntegerBitSize::Sixteen), + NoirType::Field, + ]), + Visibility::Public, + ), + ( + LocalId(6), + false, + "object".to_string(), + // Structures are of type Tuple in the Mon. Ast + NoirType::Tuple(vec![ + NoirType::Integer(Signedness::Unsigned, IntegerBitSize::Sixteen), + NoirType::Field, + NoirType::Bool, + ]), + Visibility::Public, + ), + ], + body: Expression::Block(vec![]), + return_type: NoirType::Integer( + noirc_frontend::shared::Signedness::Signed, + noirc_frontend::ast::IntegerBitSize::ThirtyTwo, + ), + return_visibility: Visibility::Public, + unconstrained: false, + inline_type: InlineType::Inline, + func_sig: (vec![], None), + formal_verification_attributes: vec![], + })), + global_constants: Box::leak(Box::new(vec![].into_iter().collect())), + functions: Box::leak(Box::new( + vec![( + FuncId(0), + Function { + id: FuncId(0), + name: "banica".to_string(), + // NOTE: no tests are calling this function (yet) + // it's only used in the `parse.rs` tests, + // so it's fine being argument-less + parameters: vec![], + body: Expression::Block(vec![]), + return_type: NoirType::Field, + return_visibility: Visibility::Public, + unconstrained: false, + inline_type: InlineType::Inline, + func_sig: (vec![], None), + formal_verification_attributes: vec![], + }, + )] + .into_iter() + .collect(), + )), + min_local_id: Rc::new(RefCell::new(7)), + } + } + + pub fn parse<'a>(input: &'a str) -> PResult<'a, OffsetExpr> { + parse_expression(input) + } + + pub fn test_precedence_equality(raw: &str, parenthesised: &str) { + let expr = parse(raw).unwrap(); + let expr_expected = parse(parenthesised).unwrap(); + dbg!(&strip_ann(expr.1.clone())); + assert_eq!(expr.0, ""); + assert_eq!(expr_expected.0, ""); + + let expr_flat: OffsetExpr = cata(expr.1, &|ann, expr| match expr { + ExprF::Parenthesised { expr } => expr, + _ => OffsetExpr { ann, expr: Box::new(expr) }, + }); + let expr_expected_flat: OffsetExpr = cata(expr_expected.1, &|ann, expr| match expr { + ExprF::Parenthesised { expr } => expr, + _ => OffsetExpr { ann, expr: Box::new(expr) }, + }); + + assert_eq!(strip_ann(expr_flat), strip_ann(expr_expected_flat)); + } + + #[test] + fn test_bool_true() { + let (input, expr) = parse("true").unwrap(); + assert_eq!(input, ""); + assert!(matches!(*expr.expr, ExprF::Literal { value: Literal::Bool(true) })); + } + + #[test] + fn test_int() { + let chislo = "1234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890"; + let (input, expr) = parse(chislo).unwrap(); + assert_eq!(input, ""); + let ExprF::Literal { value: Literal::Int(ref bi) } = *expr.expr else { panic!() }; + assert_eq!(bi.to_str_radix(10), chislo); + } + + #[test] + fn test_ident() { + let identche = "Banica_123_"; + let (input, expr) = parse(identche).unwrap(); + assert_eq!(input, ""); + let ExprF::Variable(Variable { name: input, .. }) = *expr.expr else { panic!() }; + assert_eq!(&input, identche); + } + + #[test] + #[should_panic] + fn test_ident_starts_with_digit() { + let identche = "1Banica_123_"; + let expr = parse_var_expr(identche).unwrap(); + dbg!(&expr); + assert_eq!(expr.0, ""); + } + + #[test] + fn test_function_call() { + let expr = parse("banica(1, banica(a, kek))").unwrap(); + dbg!(&expr); + assert_eq!(expr.0, ""); + } + + #[test] + fn test_equality_precedence() { + test_precedence_equality("a == b | c == d", "((a == (b | c)) == d)"); + } + + #[test] + fn test_and_precedence() { + test_precedence_equality( + "exists(|i| (0 <= i) & (i < 20) & arr[i] > 100)", + "exists(|i| (((0 <= i) & (i < 20)) & (arr[i] > 100)))", + ); + } + + #[test] + fn test_identifier_with_path() { + let expr = parse("f(alo::da::kek + !2 ^ bani::c::a.0)").unwrap(); + dbg!(&expr); + assert_eq!(expr.0, ""); + } + + #[test] + fn test_sum() { + let identche = "1 + 2 * 3"; + let expr = parse(identche).unwrap(); + dbg!(&expr); + assert_eq!(expr.0, ""); + } + + #[test] + fn test_parenthesis() { + let s = "( (( 1 + 2 ) ) * 3 )"; + let expr = parse(s).unwrap(); + dbg!(&expr); + assert_eq!(expr.0, ""); + } + + #[test] + fn test_quantifier() { + let expr = parse("exists(|x| 1 + x)").unwrap(); + dbg!(&expr); + assert_eq!(expr.0, ""); + } + + #[test] + fn test_index() { + let expr = parse("(tutmanik + 3)[12 < 3]").unwrap(); + dbg!(&expr); + assert_eq!(expr.0, ""); + } + + #[test] + fn test_member() { + let expr = parse("ala.0.17").unwrap(); + dbg!(&expr); + assert_eq!(expr.0, ""); + } + + #[test] + fn test_prefix() { + let expr = parse("(!1 + !2 * !x)").unwrap(); + dbg!(&expr); + assert_eq!(expr.0, ""); + } + + #[test] + fn test_postfix() { + let expr = parse("5 + ala.126[nica].012[1[3]][2].15[da] / 5").unwrap(); + dbg!(&expr); + assert_eq!(expr.0, ""); + } + + #[test] + fn test_tuple() { + let expr = parse("(1, kek, true).2").unwrap(); + dbg!(&expr); + assert_eq!(expr.0, ""); + } + + #[test] + fn test_array() { + let expr = parse("[1, kek, true][2]").unwrap(); + dbg!(&expr); + assert_eq!(expr.0, ""); + } + + #[test] + fn test_quantifier_span() { + let expr = parse("forall(|x| bool == x)").unwrap(); + dbg!(&expr); + assert_eq!(expr.0, ""); + } + + #[test] + fn test_ghost() { + let annotation = "ghost"; + let state = empty_state(); + let attribute = parse_attribute( + annotation, + Location { + span: Span::inclusive(0, annotation.len() as u32), + file: Default::default(), + }, + state.function, + state.global_constants, + state.functions, + ) + .unwrap(); + + assert!(matches!(attribute, Attribute::Ghost)); + } + + #[test] + fn test_bitshift() { + let annotation = "ensures(result == x >> y)"; + let state = empty_state(); + let attribute = parse_attribute( + annotation, + Location { + span: Span::inclusive(0, annotation.len() as u32), + file: Default::default(), + }, + state.function, + state.global_constants, + state.functions, + ) + .unwrap(); + + let Attribute::Ensures(expr) = attribute else { panic!() }; + dbg!(strip_ann(expr)); + } + + #[test] + fn test_cast() { + let annotation = "ensures((15 as i16 - 3 > 2) & ((result as Field - 6) as u64 == 1 + a as u64 >> kek as u8))"; + let state = empty_state(); + let attribute = parse_attribute( + annotation, + Location { + span: Span::inclusive(0, annotation.len() as u32), + file: Default::default(), + }, + state.function, + state.global_constants, + state.functions, + ) + .unwrap(); + + let Attribute::Ensures(expr) = attribute else { panic!() }; + dbg!(strip_ann(expr)); + } + + #[test] + fn test_structure_access() { + let annotation = "ensures(object.some_field)"; + let state = empty_state(); + let attribute = parse_attribute( + annotation, + Location { + span: Span::inclusive(0, annotation.len() as u32), + file: Default::default(), + }, + state.function, + state.global_constants, + state.functions, + ) + .unwrap(); + + let Attribute::Ensures(expr) = attribute else { panic!("Expected an 'ensures' attribute") }; + + let ExprF::StructureAccess { expr: inner, field } = &*expr.expr else { + panic!("Expected a StructureAccess expression"); + }; + + let ExprF::Variable(Variable { name, .. }) = &*inner.expr else { + panic!("Expected inner expression to be a variable"); + }; + assert_eq!(name, "object"); + + assert_eq!(field, "some_field"); + } + + #[test] + fn test_parse_failure_identifier() { + let annotation = "ensures(5 > 'invalid)"; + let state = empty_state(); + let result = parse_attribute( + annotation, + Location { + span: Span::inclusive(0, annotation.len() as u32), + file: Default::default(), + }, + state.function, + state.global_constants, + state.functions, + ); + + let err = result.unwrap_err(); + + let first_error = err.0.get(0).expect("Should have one parser error"); + assert!(matches!(&first_error.kind, ParserErrorKind::Expected { expected, found } + if expected == "an identifier" && found.starts_with("'invalid") + )); + } + + #[test] + fn test_parse_failure_attribute() { + let annotation = "banica(true)"; + let state = empty_state(); + let result = parse_attribute( + annotation, + Location { + span: Span::inclusive(0, annotation.len() as u32), + file: Default::default(), + }, + state.function, + state.global_constants, + state.functions, + ); + + let err = result.unwrap_err(); + + let first_error = err.0.get(0).expect("Should have one parser error"); + assert!(matches!(&first_error.kind, ParserErrorKind::UnknownAttribute(attr) + if attr == "banica" + )); + } + + #[test] + fn test_parse_failure_salvo() { + let annotations = vec![ + // Valid annotation, invalid quantifier + "requires(exists(x > 5))", + "requires(forall(|| x > 5))", + "requires(forall(||))", + "requires(forall)", + "requires(forall(|i x > 5))", + "requires(exists |j| x < 4)", + "requires(exists())", + // Invalid annotation + "ensures(result > 5", + "ensures result > 5)", + "ensures result > 5", + "requires", + "ensures", + "ensures()", + "ensures(result > 4)x", + "requires x == 4)", + ]; + for annotation in annotations { + let state = empty_state(); + let result = parse_attribute( + annotation, + Location { + span: Span::inclusive(0, annotation.len() as u32), + file: Default::default(), + }, + state.function, + state.global_constants, + state.functions, + ); + + let err = result.unwrap_err(); + dbg!(annotation, err); + } + } +} diff --git a/compiler/formal_verification/src/parse/errors.rs b/compiler/formal_verification/src/parse/errors.rs new file mode 100644 index 00000000000..1e775e24388 --- /dev/null +++ b/compiler/formal_verification/src/parse/errors.rs @@ -0,0 +1,167 @@ +use noirc_errors::{CustomDiagnostic, Location, Span}; +use nom::{ + Err as NomErr, IResult, Parser, + error::{ContextError, ErrorKind, ParseError}, +}; +use std::fmt::Debug; + +use super::Input; + +#[derive(Debug, Clone)] +pub struct ParserError { + /// Offset from the end of the annotation + pub offset: u32, + pub kind: ParserErrorKind, +} + +#[derive(Debug, Clone)] +pub struct ParserErrorWithLocation { + pub location: Location, + pub kind: ParserErrorKind, +} + +// The different kinds of specific errors. +#[derive(Debug, Clone)] +pub enum ParserErrorKind { + Expected { + // e.g., "Expected ')'" + expected: String, + // e.g., "found 'foo'" + found: String, + }, + // e.g., "forall" + InvalidQuantifier(String), + // e.g., "reassures(...)" + UnknownAttribute(String), + // e.g., "123_abc" + InvalidIntegerLiteral, + // e.g., "user.5" where the member access must be an integer literal + InvalidTupleIndex, + // When an identifier doesn't follow the rules (e.g., starts with a number) + InvalidIdentifier(String), + // A generic message for when other errors don't fit + Message(String), +} + +// The error type that nom's functions will return +#[derive(Debug, Clone)] +pub struct Error { + pub parser_errors: Vec, + pub contexts: Vec, +} + +pub fn input_to_offset(i: Input) -> u32 { + i.len() as u32 +} + +/// Builds and returns our custom Error struct directly. +pub fn build_error(input: Input, kind: ParserErrorKind) -> Error { + Error { + parser_errors: vec![ParserError { offset: input_to_offset(input), kind }], + contexts: vec![], + } +} + +/// From an input slice, get the next token for use in an error message. +pub fn get_found_token(input: Input) -> String { + match input.split_whitespace().next() { + Some("") | None => "end of input".to_string(), + Some(token) => token.to_string(), + } +} + +/// A specialized version of `map_nom_err` for the common "Expected" error. +pub fn expect<'a, P, O>( + expected_msg: impl AsRef, + parser: P, +) -> impl FnMut(Input<'a>) -> IResult, O, Error> +where + P: Parser, Output = O, Error = Error>, +{ + map_nom_err(parser, move |fail_input| ParserErrorKind::Expected { + expected: expected_msg.as_ref().to_string(), + found: fail_input.to_string(), + }) +} + +/// A combinator that wraps a parser and maps any `NomErr::Error` to a custom error kind. +/// +/// It takes a closure `F` that generates the error kind, allowing dynamic error +/// messages based on the input at the failure point. +pub fn map_nom_err<'a, P, O, F>( + mut parser: P, + error_fn: F, +) -> impl FnMut(Input<'a>) -> IResult, O, Error> +where + P: Parser, Output = O, Error = Error>, + F: Fn(Input<'a>) -> ParserErrorKind, +{ + move |input: Input<'a>| { + parser.parse(input).map_err(|e: NomErr| { + if let NomErr::Error(_) = e { + // Generate the error dynamically using the input at the point of failure. + NomErr::Error(build_error(input, error_fn(input))) + } else { + e + } + }) + } +} + +impl<'a> ParseError> for Error { + fn from_error_kind(input: Input<'a>, kind: ErrorKind) -> Self { + // TODO: it'd be best in the future if we actually manage to suppress the builtin `nom` + // errors at all levels, even under the `expect and `map_nom_err` calls + // unreachable!( + // "We should wrap all errors and never have to convert from the built-in `nom` ones, still got a {:?} while parsing {:?} tho", + // kind, input + // ); + + // NOTE: these errors should not matter, because of our usage of `expect` and `map_nom_err` + // throughout the parser, ensuring that a primitive parser's error never sees the + // light of day + let err = ParserError { + offset: input_to_offset(input), + kind: ParserErrorKind::Message(format!("nom primitive failed: {:?}", kind)), + }; + Error { parser_errors: vec![err], contexts: vec![] } + } + + fn append(_input: Input<'a>, _kind: ErrorKind, other: Self) -> Self { + // TODO: it'd be best to assert that this never happens either, check the `TODO` comment in + // the `from_error_kind` function above + // unreachable!( + // "We should wrap all errors and never have to convert from the built-in `nom` ones, still got a {:?} on top of {:?} while parsing {:?} tho", + // kind, other, input + // ); + + // NOTE: This usually adds context of which primitive parsers were called before + // encountering the `other` error + other + } +} + +impl<'a> ContextError> for Error { + fn add_context(_input: Input<'a>, ctx: &'static str, mut other: Self) -> Self { + other.contexts.push(ctx.to_string()); + other + } +} + +impl From for CustomDiagnostic { + fn from(value: ParserErrorWithLocation) -> Self { + let primary_message = match value.kind { + ParserErrorKind::Expected { expected, found } => { + format!("Expected {} but found {}", expected, found) + } + ParserErrorKind::InvalidQuantifier(q) => format!("Invalid quantifier {}", q), + ParserErrorKind::UnknownAttribute(attr) => format!("Unknown attribute {}", attr), + ParserErrorKind::InvalidIntegerLiteral => "Invalid integer literal".to_string(), + ParserErrorKind::InvalidTupleIndex => "Invalid tuple index".to_string(), + ParserErrorKind::InvalidIdentifier(identifier) => format!("Invalid identifier {}", identifier), + ParserErrorKind::Message(msg) => msg, + }; + + CustomDiagnostic::simple_error(primary_message, String::new(), value.location) + } +} diff --git a/compiler/formal_verification/src/type_conversion.rs b/compiler/formal_verification/src/type_conversion.rs new file mode 100644 index 00000000000..f2a9d4b9d88 --- /dev/null +++ b/compiler/formal_verification/src/type_conversion.rs @@ -0,0 +1,146 @@ +use noirc_frontend::{Kind, Type as NoirType, monomorphization::ast::Type as MastType}; + +pub fn convert_mast_to_noir_type(mast_type: MastType) -> NoirType { + match mast_type { + MastType::Field => NoirType::FieldElement, + MastType::Array(len, element_type) => { + // In noirc_frontend, the length of an array is a type itself. + // We represent the concrete length from MAST as a `Type::Constant`. + let length_type = Box::new(NoirType::Constant(len.into(), Kind::Normal)); + let converted_element_type = Box::new(convert_mast_to_noir_type(*element_type)); + NoirType::Array(length_type, converted_element_type) + } + MastType::Integer(sign, bits) => NoirType::Integer(sign, bits), + MastType::Bool => NoirType::Bool, + MastType::String(len) => { + // Similar to arrays, the string length is a `Type::Constant`. + let length_type = Box::new(NoirType::Constant(len.into(), Kind::Normal)); + NoirType::String(length_type) + } + MastType::FmtString(len, elements_type) => { + let length_type = Box::new(NoirType::Constant(len.into(), Kind::Normal)); + let converted_elements_type = Box::new(convert_mast_to_noir_type(*elements_type)); + NoirType::FmtString(length_type, converted_elements_type) + } + MastType::Unit => NoirType::Unit, + MastType::Tuple(mast_elements) => { + // Recursively convert each type within the tuple. + let noir_elements = mast_elements.into_iter().map(convert_mast_to_noir_type).collect(); + NoirType::Tuple(noir_elements) + } + MastType::Slice(element_type) => { + // Recursively convert the slice's element type. + let converted_element_type = Box::new(convert_mast_to_noir_type(*element_type)); + NoirType::Slice(converted_element_type) + } + MastType::Reference(element_type, mutable) => { + let converted_element_type = Box::new(convert_mast_to_noir_type(*element_type)); + NoirType::Reference(converted_element_type, mutable) + } + MastType::Function(args, ret, env, unconstrained) => { + // Recursively convert all function components: arguments, return type, and environment. + let noir_args = args.into_iter().map(convert_mast_to_noir_type).collect(); + let noir_ret = Box::new(convert_mast_to_noir_type(*ret)); + let noir_env = Box::new(convert_mast_to_noir_type(*env)); + NoirType::Function(noir_args, noir_ret, noir_env, unconstrained) + } + } +} + +#[cfg(test)] +mod tests { + use super::convert_mast_to_noir_type; + use noirc_frontend::ast::IntegerBitSize; + use noirc_frontend::shared::Signedness; + use noirc_frontend::{Kind, Type as NoirType, monomorphization::ast::Type as MastType}; + + #[test] + fn test_convert_field() { + let mast_type = MastType::Field; + let expected_noir_type = NoirType::FieldElement; + assert_eq!(convert_mast_to_noir_type(mast_type), expected_noir_type); + } + + #[test] + fn test_convert_integer() { + let mast_type = MastType::Integer(Signedness::Unsigned, IntegerBitSize::ThirtyTwo); + let expected_noir_type = NoirType::Integer(Signedness::Unsigned, IntegerBitSize::ThirtyTwo); + assert_eq!(convert_mast_to_noir_type(mast_type), expected_noir_type); + } + + #[test] + fn test_convert_bool() { + let mast_type = MastType::Bool; + let expected_noir_type = NoirType::Bool; + assert_eq!(convert_mast_to_noir_type(mast_type), expected_noir_type); + } + + #[test] + fn test_convert_unit() { + let mast_type = MastType::Unit; + let expected_noir_type = NoirType::Unit; + assert_eq!(convert_mast_to_noir_type(mast_type), expected_noir_type); + } + + #[test] + fn test_convert_string() { + let mast_type = MastType::String(10); + let expected_noir_type = + NoirType::String(Box::new(NoirType::Constant(10u32.into(), Kind::Normal))); + assert_eq!(convert_mast_to_noir_type(mast_type), expected_noir_type); + } + + #[test] + fn test_convert_array() { + let mast_type = MastType::Array(5, Box::new(MastType::Field)); + let expected_noir_type = NoirType::Array( + Box::new(NoirType::Constant(5u32.into(), Kind::Normal)), + Box::new(NoirType::FieldElement), + ); + assert_eq!(convert_mast_to_noir_type(mast_type), expected_noir_type); + } + + #[test] + fn test_convert_slice() { + let mast_type = MastType::Slice(Box::new(MastType::Bool)); + let expected_noir_type = NoirType::Slice(Box::new(NoirType::Bool)); + assert_eq!(convert_mast_to_noir_type(mast_type), expected_noir_type); + } + + #[test] + fn test_convert_tuple() { + let mast_type = MastType::Tuple(vec![MastType::Field, MastType::Bool]); + let expected_noir_type = NoirType::Tuple(vec![NoirType::FieldElement, NoirType::Bool]); + assert_eq!(convert_mast_to_noir_type(mast_type), expected_noir_type); + } + + #[test] + fn test_convert_reference() { + // Immutable reference + let mast_imm_ref = MastType::Reference(Box::new(MastType::Field), false); + let expected_imm_ref = NoirType::Reference(Box::new(NoirType::FieldElement), false); + assert_eq!(convert_mast_to_noir_type(mast_imm_ref), expected_imm_ref); + + // Mutable reference + let mast_mut_ref = MastType::Reference(Box::new(MastType::Field), true); + let expected_mut_ref = NoirType::Reference(Box::new(NoirType::FieldElement), true); + assert_eq!(convert_mast_to_noir_type(mast_mut_ref), expected_mut_ref); + } + + #[test] + fn test_convert_function() { + let mast_type = MastType::Function( + vec![MastType::Field, MastType::Bool], + Box::new(MastType::Unit), + Box::new(MastType::Tuple(vec![])), + false, + ); + let expected_noir_type = NoirType::Function( + vec![NoirType::FieldElement, NoirType::Bool], + Box::new(NoirType::Unit), + Box::new(NoirType::Tuple(vec![])), + false, + ); + assert_eq!(convert_mast_to_noir_type(mast_type), expected_noir_type); + } +} diff --git a/compiler/formal_verification/src/typing.rs b/compiler/formal_verification/src/typing.rs new file mode 100644 index 00000000000..628022acb39 --- /dev/null +++ b/compiler/formal_verification/src/typing.rs @@ -0,0 +1,1676 @@ +use std::{convert::identity, fmt::Display, ops::AddAssign}; + +use crate::{ + MonomorphizationRequest, State, + ast::{ + AnnExpr, BinaryOp, ExprF, Literal, SpannedExpr, SpannedTypedExpr, UnaryOp, Variable, cata, + try_cata, try_contextual_cata, + }, +}; +use noirc_errors::Location; +use noirc_frontend::{ + ast::IntegerBitSize, + hir::{resolution::errors::ResolverError, type_check::TypeCheckError}, + monomorphization::{FUNC_RETURN_VAR_NAME, ast::Type as NoirType}, + shared::Signedness, +}; +use num_bigint::{BigInt, BigUint}; +use num_traits::{One, Zero}; + +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum OptionalType { + /// Well-typed + Well(NoirType), + /// Untyped (yet) integer literal or quantified variable + IntegerLiteral, + /// Tuple with holes + PartialTuple(Vec), +} + +impl Display for OptionalType { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + match self { + OptionalType::Well(t) => write!(f, "{t}"), + OptionalType::IntegerLiteral => write!(f, "Integer literal"), + OptionalType::PartialTuple(types) => write!(f, "Partial tuple with types: {:?}", types), + } + } +} + +impl OptionalType { + pub fn unwrap_or(self, or_arg: NoirType) -> NoirType { + match self { + OptionalType::Well(noir_typ) => noir_typ, + OptionalType::IntegerLiteral => or_arg, + OptionalType::PartialTuple(_optional_types) => { + unreachable!("Partial types must have been resolved") + } + } + } +} + +pub type SpannedPartiallyTypedExpr = AnnExpr<(Location, OptionalType)>; + +#[derive(Debug, Clone)] +pub enum TypeInferenceError { + MonomorphizationRequest(MonomorphizationRequest), + // NOTE: We are converting IntegerLiteralDoesNotFit to TypeCheckError later + // We cannot do it during construction because we need a function + // located in a module which depends on us. + IntegerLiteralDoesNotFit { + literal: BigInt, + literal_type: NoirType, + fit_into: Option, + location: Location, + message: String, + }, + NoirTypeError(TypeCheckError), +} + +#[derive(Debug, PartialEq, Eq)] +pub enum FitsIn { + Yes, + No { + /// `None` means there is no possible `IntegerBitSize` that could contain us + need: Option, + }, +} +pub fn bi_can_fit_in(bi: &BigInt, hole_size: &IntegerBitSize, hole_sign: &Signedness) -> FitsIn { + let is_negative = match bi.sign() { + num_bigint::Sign::Minus => true, + num_bigint::Sign::Plus | num_bigint::Sign::NoSign => false, + }; + + // NOTE: if we have a negative literal, but try to fit into an unsigned integer + let is_wrong_sign = is_negative && !hole_sign.is_signed(); + + let mut bits = bi.bits(); + + // NOTE: Add one bit for the sign. + if hole_sign.is_signed() { + bits += 1; + } + + if is_negative { + fn is_power_of_two(n: &BigUint) -> bool { + // 10000000 + // 01111111 + !n.is_zero() && ((n & (n - BigUint::one())) == BigUint::zero()) + } + + // NOTE: ...unless we have a negative number whose magnitude is a power of two. + // This is the because it fits perfectly into the two's complement minimum value. + // (e.g., -128 fits in `i8`, the same as -127, but not 128). + if is_power_of_two(bi.magnitude()) { + bits -= 1; + } + } + + // NOTE: find the smallest `IntegerBitSize` that could contain us, `None` if no such one exists + let smallest_fit_size = + IntegerBitSize::allowed_sizes().into_iter().find(|size| bits <= size.bit_size() as u64); + + // NOTE: using the `PartialOrd` instance for `IntegerBitSize`, + // which definitionally orders the bit sizes in an increasing order + let size_fits = smallest_fit_size.map(|sfs| sfs <= *hole_size).unwrap_or(false); + + if !size_fits || is_wrong_sign { + return FitsIn::No { + need: smallest_fit_size.map(|sfs| { + NoirType::Integer(if is_wrong_sign { Signedness::Signed } else { *hole_sign }, sfs) + }), + }; + } + + return FitsIn::Yes; +} + +impl SpannedPartiallyTypedExpr { + /// Unifies a partially-typed expression with a target concrete type + /// - If the expression is an `IntegerLiteral`, it's checked and given the target type + /// - If the expression is already `Well`-typed, it checks if the types match + /// - If the expression is a `PartialTuple`, it recursively unifies its elements + pub fn unify_with_type(&mut self, target_type: NoirType) -> Result<(), TypeInferenceError> { + match &self.ann.1 { + OptionalType::IntegerLiteral => match self.expr.as_mut() { + ExprF::Literal { value: Literal::Int(bi) } => { + if let NoirType::Integer(ref sign, ref size) = target_type + && let FitsIn::No { need } = bi_can_fit_in(&bi, size, sign) + { + return Err(TypeInferenceError::IntegerLiteralDoesNotFit { + literal: bi.clone(), + literal_type: target_type.clone(), + fit_into: need.clone(), + location: self.ann.0, + message: format!( + "Integer literal {} cannot fit in {}, needs at least {:?} or larger", + bi, target_type, need + ), + }); + } + + self.ann.1 = OptionalType::Well(target_type); + } + // NOTE: quantified variable + ExprF::Variable(_var) => self.ann.1 = OptionalType::Well(target_type), + // NOTE: not shifting + ExprF::BinaryOp { op: _, expr_left, expr_right } => { + expr_left.unify_with_type(target_type.clone())?; + expr_right.unify_with_type(target_type.clone())?; + self.ann.1 = OptionalType::Well(target_type); + } + ExprF::UnaryOp { op, expr } => match op { + UnaryOp::Dereference => { + return Err(TypeInferenceError::NoirTypeError( + TypeCheckError::TypeMismatch { + expected_typ: self.ann.1.to_string(), + expr_typ: "Reference".to_string(), + expr_location: self.ann.0, + }, + )); + } + UnaryOp::Not => { + expr.unify_with_type(target_type.clone())?; + self.ann.1 = OptionalType::Well(target_type); + } + }, + ExprF::TupleAccess { expr: inner_tuple_expr, index } => { + let ExprF::Tuple { exprs } = inner_tuple_expr.expr.as_mut() else { + unreachable!() + }; + + let new_element_types = exprs + .into_iter() + .enumerate() + .map(|(i, elem_expr)| { + if i as u32 == *index { + elem_expr.unify_with_type(target_type.clone())?; + } else if matches!(elem_expr.ann.1, OptionalType::IntegerLiteral) { + // NOTE: Default other integer literals to Field, as they are unconstrained. + elem_expr.unify_with_type(NoirType::Field)?; + } + + Ok(elem_expr.ann.1.clone()) + }) + .collect::, _>>()?; + + let updated_inner_tuple_type = new_element_types + .iter() + .map(|ot| match ot { + OptionalType::Well(t) => Some(t.clone()), + _ => None, + }) + .collect::>>() + .map(NoirType::Tuple) + .map(OptionalType::Well) + .unwrap_or(OptionalType::PartialTuple(new_element_types)); + + inner_tuple_expr.ann.1 = updated_inner_tuple_type; + self.ann.1 = OptionalType::Well(target_type); + } + ExprF::Parenthesised { expr: inner_expr } => { + inner_expr.unify_with_type(target_type.clone())?; + self.ann.1 = OptionalType::Well(target_type); + } + + ExprF::Literal { value: Literal::Bool(..) } + | ExprF::Quantified { .. } + | ExprF::FnCall { .. } + | ExprF::Index { .. } + | ExprF::Cast { .. } + | ExprF::Tuple { .. } + | ExprF::Array { .. } + | ExprF::StructureAccess { .. } => unreachable!( + "ICE: Unexpected expression {:?} found with IntegerLiteral type", + self.expr + ), + }, + + OptionalType::Well(well_type) => { + if *well_type != target_type { + return Err(TypeInferenceError::NoirTypeError(TypeCheckError::TypeMismatch { + expected_typ: target_type.to_string(), + expr_typ: well_type.to_string(), + expr_location: self.ann.0, + })); + } + + self.ann.1 = OptionalType::Well(target_type); + } + + OptionalType::PartialTuple(_) => { + let NoirType::Tuple(ref target_expr_types) = target_type else { + return Err(TypeInferenceError::NoirTypeError(TypeCheckError::TypeMismatch { + expected_typ: target_type.to_string(), + expr_typ: "tuple".to_string(), + expr_location: self.ann.0, + })); + }; + + let ExprF::Tuple { exprs } = self.expr.as_mut() else { unreachable!() }; + + if exprs.len() != target_expr_types.len() { + return Err(TypeInferenceError::NoirTypeError(TypeCheckError::TupleMismatch { + tuple_types: vec![], + actual_count: exprs.len(), + location: self.ann.0, + })); + } + + std::iter::zip(exprs, target_expr_types) + .try_for_each(|(expr, t)| expr.unify_with_type(t.clone()))?; + + self.ann.1 = OptionalType::Well(target_type); + } + } + + Ok(()) + } +} + +/// Converts an `OptionalType` into a concrete `NoirType`, +/// using the default for any remaining untyped integer literals, +/// unless in a partial tuple +pub fn concretize_type( + opt_type: OptionalType, + default_integer_literal_type: &NoirType, +) -> Option { + match opt_type { + OptionalType::Well(t) => Some(t), + OptionalType::IntegerLiteral => Some(default_integer_literal_type.clone()), + OptionalType::PartialTuple(elements) => elements + .into_iter() + .map(|e| match e { + OptionalType::IntegerLiteral => None, + _ => concretize_type(e, default_integer_literal_type), + }) + .collect::>() + .map(NoirType::Tuple), + } +} + +pub fn type_infer( + state: &State, + expr: SpannedExpr, +) -> Result { + // TODO(totel): Assert that there are no Expressions of type StructureAccess in the AST + + // NOTE: predicate, always bool, + // assume subterms are `u32` (like `Noir` does) + let default_literal_type = NoirType::Integer(Signedness::Unsigned, IntegerBitSize::ThirtyTwo); + + let is_numeric = |t: &NoirType| matches!(t, NoirType::Integer(_, _) | NoirType::Field); + + let sote: SpannedPartiallyTypedExpr = try_contextual_cata( + expr, + vec![], + &|mut quantifier_bound_variables, e| { + if let ExprF::Quantified { variables, .. } = e.expr.as_ref() { + quantifier_bound_variables.extend(variables.iter().map( + |Variable { path, name, .. }| { + // NOTE: quantified variables should have no path + debug_assert_eq!(path.len(), 0); + + // NOTE:: reserve an `id` for this variable + let id = state.min_local_id.borrow().clone(); + state.min_local_id.borrow_mut().add_assign(1); + + (id, name.clone()) + }, + )); + } + quantifier_bound_variables + }, + &|location, quantifier_bound_variables, mut exprf| { + let exprf_type = match &mut exprf { + ExprF::Literal { value } => match value { + Literal::Bool(_) => OptionalType::Well(NoirType::Bool), + Literal::Int(_) => { + // NOTE: `OptionalType::IntegerLiteral` signifies that this has to be inferred up the chain, + // will gain a concrete type when it gets matched in an (arithmetic or predicate) operation + // with a variable with a real (integer) type + OptionalType::IntegerLiteral + } + }, + ExprF::Variable(Variable { path, name, id }) => { + // NOTE: All paths should be empty because we have inlined all global variables with paths. + // This occurs in the `inline_globals` pass located in `compiler/formal_verification/src/inline_globals.rs` + assert!(path.is_empty()); + + // NOTE: parsing should not yield `id`s + debug_assert_eq!(*id, None); + let (variable_ident, variable_id, variable_type): ( + &str, + Option, + OptionalType, + ) = quantifier_bound_variables + .iter() + .find_map(|(id, bound_variable)| { + (bound_variable == name).then(|| { + (name.as_str(), Some(id.clone()), OptionalType::IntegerLiteral) + }) + }) + .or_else(|| { + state.function.parameters.iter().find_map(|(id, _, par_name, t, _)| { + (par_name == name).then(|| { + (name.as_str(), Some(id.0), OptionalType::Well(t.clone())) + }) + }) + }) + .or_else(|| { + state.global_constants.iter().find_map( + |(global_id, (global_name, t, _))| { + (global_name == name).then(|| { + ( + name.as_str(), + Some(global_id.0), + OptionalType::Well(t.clone()), + ) + }) + }, + ) + }) + .or_else(|| { + (name == "result").then(|| { + ( + FUNC_RETURN_VAR_NAME, + None, + OptionalType::Well(state.function.return_type.clone()), + ) + }) + }) + .ok_or(TypeInferenceError::NoirTypeError(TypeCheckError::ResolverError( + ResolverError::VariableNotDeclared { name: name.to_string(), location }, + )))?; + + *name = variable_ident.to_string(); + *id = variable_id; + + variable_type + } + ExprF::FnCall { name, args } => { + let func_object = state + .functions + .iter() + .find_map(|(_, func)| (func.name == *name).then_some(func)) + .ok_or(TypeInferenceError::MonomorphizationRequest( + MonomorphizationRequest { + function_identifier: name.clone(), + param_types: args + .iter() + .map(|arg: &SpannedPartiallyTypedExpr| arg.ann.1.clone()) + .collect(), + }, + ))?; + + // Unify the function call arguments with their expected type + for (arg, (_id, _mut, _name, typ, _visibility)) in + args.iter_mut().zip(&func_object.parameters) + { + arg.unify_with_type(typ.clone())?; + } + + OptionalType::Well(func_object.return_type.clone()) + } + ExprF::Quantified { variables, .. } => { + variables + .iter() + .map(|Variable { path, .. }| { + if !path.is_empty() { + Err(TypeInferenceError::NoirTypeError( + // TODO(totel): better error? + TypeCheckError::ParameterCountMismatch { + expected: 0, + found: path.len(), + location, + }, + )) + } else { + Ok(()) + } + }) + .collect::, _>>()?; + + // NOTE: add predertimed `id`s to the quantified variables + variables.iter_mut().for_each(|variable| { + variable.id = Some( + *quantifier_bound_variables + .iter() + .find_map(|(id, bound_variable)| { + (*bound_variable == variable.name).then(|| id) + }) + .expect("Should have been populated while traversing down the AST"), + ); + }); + + OptionalType::Well(NoirType::Bool) + } + ExprF::Parenthesised { expr } => expr.ann.1.clone(), + ExprF::UnaryOp { op, expr } => { + let t = match op { + UnaryOp::Dereference => { + match &expr.ann.1 { + OptionalType::Well(NoirType::Reference(t, _)) => { + OptionalType::Well(*t.clone()) + } + _ => { + // TODO(totel): better error? + return Err(TypeInferenceError::NoirTypeError( + TypeCheckError::UnconstrainedReferenceToConstrained { + location, + }, + )); + } + } + } + UnaryOp::Not => expr.ann.1.clone(), + }; + + t + } + ExprF::BinaryOp { op, expr_left, expr_right } => { + fn is_tupleish(t: &OptionalType) -> bool { + matches!( + t, + OptionalType::Well(NoirType::Tuple(_)) | OptionalType::PartialTuple(_) + ) + } + + if matches!(op, BinaryOp::Eq | BinaryOp::Neq) + && is_tupleish(&expr_left.ann.1) + && is_tupleish(&expr_right.ann.1) + { + enum TupleElement<'a> { + Literal(&'a mut SpannedPartiallyTypedExpr, OptionalType), + Variable(NoirType), + } + fn tuple_elements_from_expr<'a>( + expr: &'a mut ExprF, + ann: OptionalType, + location: Location, + ) -> Result>, TypeInferenceError> + { + match (expr, ann) { + ( + ExprF::Tuple { exprs }, + OptionalType::Well(NoirType::Tuple(types)), + ) => Ok(std::iter::zip(exprs, types) + .map(|(e, t)| TupleElement::Literal(e, OptionalType::Well(t))) + .collect()), + + (ExprF::Tuple { exprs }, OptionalType::PartialTuple(types)) => { + Ok(std::iter::zip(exprs, types) + .map(|(e, t)| TupleElement::Literal(e, t)) + .collect()) + } + + ( + ExprF::Variable(_), + OptionalType::Well(NoirType::Tuple(types)), + ) => Ok(types.into_iter().map(TupleElement::Variable).collect()), + + (ExprF::Variable(_), OptionalType::PartialTuple(_)) => { + // Unreachable because if we have a variable of type tuple we + // would always know its type. + unreachable!() + } + + _ => Err(TypeInferenceError::NoirTypeError( + TypeCheckError::TupleMismatch { + location, + tuple_types: vec![], + actual_count: 0, + }, + )), + } + } + + let left_elements: Vec = tuple_elements_from_expr( + expr_left.expr.as_mut(), + expr_left.ann.1.clone(), + location, + )?; + let right_elements: Vec = tuple_elements_from_expr( + expr_right.expr.as_mut(), + expr_right.ann.1.clone(), + location, + )?; + + if left_elements.len() != right_elements.len() { + // TODO(totel): better error? + return Err(TypeInferenceError::NoirTypeError( + TypeCheckError::TupleMismatch { + location, + tuple_types: vec![], + actual_count: left_elements.len(), + }, + )); + } + + // NOTE: Unify all pair of elements + let new_exprs_types: Vec<_> = std::iter::zip(left_elements, right_elements) + .map(|(left, right)| { + match (left, right) { + ( + TupleElement::Literal(left_expr, left_type), + TupleElement::Literal(right_expr, right_type), + ) => match (left_type, right_type) { + (OptionalType::Well(t1), OptionalType::Well(t2)) => { + if t1 != t2 { + return Err(TypeInferenceError::NoirTypeError( + TypeCheckError::TypeMismatch { + expected_typ: t1.to_string(), + expr_typ: t2.to_string(), + expr_location: right_expr.ann.0, + }, + )); + } + Ok(t1.clone()) + } + (OptionalType::Well(t), OptionalType::IntegerLiteral) => { + right_expr.unify_with_type(t.clone())?; + Ok(t.clone()) + } + (OptionalType::IntegerLiteral, OptionalType::Well(t)) => { + left_expr.unify_with_type(t.clone())?; + Ok(t.clone()) + } + ( + OptionalType::IntegerLiteral, + OptionalType::IntegerLiteral, + ) => { + left_expr + .unify_with_type(default_literal_type.clone())?; + right_expr + .unify_with_type(default_literal_type.clone())?; + Ok(default_literal_type.clone()) + } + // NOTE: All other combinations (e.g., trying to unify a bool with a tuple) are a type mismatch. + // The calling function is responsible for handling recursive cases like tuples. + (t1, t2) => Err(TypeInferenceError::NoirTypeError( + TypeCheckError::TypeMismatch { + expected_typ: t1.to_string(), + expr_typ: t2.to_string(), + expr_location: right_expr.ann.0, + }, + )), + }, + ( + TupleElement::Literal(left_expr, _left_type), + TupleElement::Variable(right_type), + ) => { + left_expr.unify_with_type(right_type.clone())?; + Ok(right_type) + } + ( + TupleElement::Variable(left_type), + TupleElement::Literal(right_expr, _right_type), + ) => { + right_expr.unify_with_type(left_type.clone())?; + Ok(left_type) + } + ( + TupleElement::Variable(left_type), + TupleElement::Variable(right_type), + ) => { + if left_type != right_type { + return Err(TypeInferenceError::NoirTypeError( + TypeCheckError::TypeMismatch { + expected_typ: right_type.to_string(), + expr_typ: left_type.to_string(), + expr_location: location, + }, + )); + } + + Ok(left_type) + } + } + }) + .collect::, _>>()?; + + expr_left.ann.1 = + OptionalType::Well(NoirType::Tuple(new_exprs_types.clone())); + expr_right.ann.1 = OptionalType::Well(NoirType::Tuple(new_exprs_types)); + + OptionalType::Well(NoirType::Bool) + } else if op.is_shift() { + let shift_amount_type = + NoirType::Integer(Signedness::Unsigned, IntegerBitSize::Eight); + + match &expr_right.ann.1 { + OptionalType::Well(t) if *t == shift_amount_type => {} // OK + OptionalType::IntegerLiteral => { + expr_right.unify_with_type(shift_amount_type)?; + } + OptionalType::Well(_) | OptionalType::PartialTuple(_) => { + return Err(TypeInferenceError::NoirTypeError( + TypeCheckError::InvalidShiftSize { location }, + )); + } + } + + if let OptionalType::IntegerLiteral = &expr_left.ann.1 { + expr_left.unify_with_type(default_literal_type.clone())?; + } + + expr_left.ann.1.clone() + } else { + match (&expr_left.ann.1, &expr_right.ann.1) { + (OptionalType::Well(t1), OptionalType::Well(t2)) => { + if t1 != t2 { + return Err(TypeInferenceError::NoirTypeError( + TypeCheckError::TypeMismatch { + expected_typ: t1.to_string(), + expr_typ: t2.to_string(), + expr_location: expr_right.ann.0, + }, + )); + } + + OptionalType::Well(if op.is_comparison() { + NoirType::Bool + } else { + t1.clone() + }) + } + + (OptionalType::Well(t1), OptionalType::IntegerLiteral) => { + if (op.is_arithmetic() || op.is_bitwise()) && !is_numeric(t1) { + return Err(TypeInferenceError::NoirTypeError( + TypeCheckError::TypeMismatch { + expected_typ: "a numeric type".to_string(), + expr_typ: t1.to_string(), + expr_location: expr_left.ann.0, + }, + )); + } + + expr_right.unify_with_type(t1.clone())?; + + OptionalType::Well(if op.is_comparison() { + NoirType::Bool + } else { + t1.clone() + }) + } + + (OptionalType::IntegerLiteral, OptionalType::Well(t2)) => { + if (op.is_arithmetic() || op.is_bitwise()) && !is_numeric(t2) { + return Err(TypeInferenceError::NoirTypeError( + TypeCheckError::TypeMismatch { + expected_typ: "a numeric type".to_string(), + expr_typ: t2.to_string(), + expr_location: expr_right.ann.0, + }, + )); + } + + expr_left.unify_with_type(t2.clone())?; + + OptionalType::Well(if op.is_comparison() { + NoirType::Bool + } else { + t2.clone() + }) + } + + (OptionalType::IntegerLiteral, OptionalType::IntegerLiteral) => { + if op.is_arithmetic() || op.is_bitwise() { + OptionalType::IntegerLiteral + } else { + expr_left.unify_with_type(default_literal_type.clone())?; + expr_right.unify_with_type(default_literal_type.clone())?; + + OptionalType::Well(NoirType::Bool) + } + } + + // NOTE: Any other combination involving tuples is an error in this arm + (t1, t2) => { + return Err(TypeInferenceError::NoirTypeError( + TypeCheckError::TypeMismatch { + expected_typ: t1.to_string(), + expr_typ: t2.to_string(), + expr_location: location, + }, + )); + } + } + } + } + ExprF::Index { expr, index } => { + let OptionalType::Well(NoirType::Array(_, type_inner)) = &expr.ann.1 else { + return Err(TypeInferenceError::NoirTypeError( + TypeCheckError::TypeMismatch { + expr_typ: expr.ann.1.to_string(), + expected_typ: String::from("Array type"), + expr_location: location, + }, + )); + }; + match &index.ann.1 { + // Fine index + OptionalType::Well(NoirType::Integer(Signedness::Unsigned, _)) => {} + // Integer literal, try type inferring to `u32` + OptionalType::IntegerLiteral => { + index.unify_with_type(default_literal_type.clone())?; + } + // Not fine index + t => { + return Err(TypeInferenceError::NoirTypeError( + TypeCheckError::TypeMismatch { + expr_typ: t.to_string(), + expected_typ: String::from("Unsigned integer type"), + expr_location: location, + }, + )); + } + } + + OptionalType::Well(*type_inner.clone()) + } + ExprF::TupleAccess { expr, index } => { + let t = match &expr.ann.1 { + OptionalType::Well(NoirType::Tuple(types)) => { + types.get(*index as usize).cloned().map(OptionalType::Well).ok_or( + TypeInferenceError::NoirTypeError( + TypeCheckError::TupleIndexOutOfBounds { + index: *index as usize, + // NOTE: We are converting to Type::Tuple of empty vec because + // the inner types don't really matter for the error reporting + lhs_type: noirc_frontend::Type::Tuple(vec![]), + length: types.len(), + location, + }, + ), + )? + } + OptionalType::PartialTuple(types) => { + types.get(*index as usize).cloned().ok_or( + TypeInferenceError::NoirTypeError( + TypeCheckError::TupleIndexOutOfBounds { + index: *index as usize, + // NOTE: We are converting to Type::Tuple of empty vec because + // the inner types don't really matter for the error reporting + lhs_type: noirc_frontend::Type::Tuple(vec![]), + length: types.len(), + location, + }, + ), + )? + } + _ => { + // TODO(totel): better error? + return Err(TypeInferenceError::NoirTypeError( + TypeCheckError::ResolverError(ResolverError::SelfReferentialType { + location, + }), + )); + } + }; + + t + } + ExprF::Cast { expr, target } => { + // Non-booleans cannot cast to bool + if matches!(target, NoirType::Bool) + && !matches!(expr.ann.1, OptionalType::Well(NoirType::Bool)) + { + return Err(TypeInferenceError::NoirTypeError( + TypeCheckError::CannotCastNumericToBool { + // NOTE: We are using a mock type, because we can't convert to wanted type + typ: noirc_frontend::Type::FieldElement, + location, + }, + )); + } + + // Non-numerics cannot cast to numeric types + if is_numeric(target) + && let OptionalType::Well(ref t) = expr.ann.1 + && !is_numeric(t) + && !matches!(t, NoirType::Bool) + { + return Err(TypeInferenceError::NoirTypeError( + TypeCheckError::TypeMismatch { + expected_typ: String::from("Numeric or a boolean type"), + expr_typ: t.to_string(), + expr_location: location, + }, + )); + } + + // Try to type infer integer literals as the target type + if matches!(expr.ann.1, OptionalType::IntegerLiteral) { + expr.unify_with_type(target.clone())?; + } + + OptionalType::Well(target.clone()) + } + ExprF::Tuple { exprs } => { + // NOTE: if all sub-expressions are well-typed, produce a well-typed `Tuple` + // otherwise, produce a `OptionalType::PartialTuple` + let t = exprs + .iter() + .map(|e| e.ann.1.clone()) + .map(|ot| match ot { + OptionalType::Well(t) => Some(t), + _ => None, + }) + .collect::>>() + .map(NoirType::Tuple) + .map(OptionalType::Well) + .unwrap_or(OptionalType::PartialTuple( + exprs.iter().map(|ae| ae.ann.1.clone()).collect(), + )); + + t + } + ExprF::Array { exprs } => { + if exprs.is_empty() { + // TODO(totel): better error? + return Err(TypeInferenceError::NoirTypeError( + TypeCheckError::InvalidTypeForEntryPoint { location }, + )); + } + + let unified_opt_type = exprs.iter().try_fold( + OptionalType::IntegerLiteral, + |acc, current_expr| { + // This closure acts as our "join" operation. + fn join_types( + t1: OptionalType, + t2: OptionalType, + location: Location, + ) -> Result + { + match (t1, t2) { + // An integer literal can join with any other type. + (t, OptionalType::IntegerLiteral) => Ok(t), + (OptionalType::IntegerLiteral, t) => Ok(t), + + // If both types are well-known, they must be identical. + (OptionalType::Well(w1), OptionalType::Well(w2)) => { + if w1 == w2 { + Ok(OptionalType::Well(w1)) + } else { + Err(TypeInferenceError::NoirTypeError( + // TODO: calculate indices + TypeCheckError::NonHomogeneousArray { + first_type: w1.to_string(), + first_location: location, + first_index: 0, + second_type: w2.to_string(), + second_location: location, + second_index: 0, + }, + )) + } + } + + // Recursively join partial tuples. + ( + OptionalType::PartialTuple(v1), + OptionalType::PartialTuple(v2), + ) => { + if v1.len() != v2.len() { + /* TODO: Mismatch error */ + Ok(OptionalType::PartialTuple(vec![])) + } else { + let joined = v1 + .into_iter() + .zip(v2.into_iter()) + .map(|(e1, e2)| join_types(e1, e2, location)) + .collect::>()?; + Ok(OptionalType::PartialTuple(joined)) + } + } + + // Coerce Well(Tuple) to PartialTuple for joining. + ( + OptionalType::Well(NoirType::Tuple(v1)), + t2 @ OptionalType::PartialTuple(_), + ) => join_types( + OptionalType::PartialTuple( + v1.into_iter().map(OptionalType::Well).collect(), + ), + t2, + location, + ), + ( + t1 @ OptionalType::PartialTuple(_), + OptionalType::Well(NoirType::Tuple(v2)), + ) => join_types( + t1, + OptionalType::PartialTuple( + v2.into_iter().map(OptionalType::Well).collect(), + ), + location, + ), + + // NOTE: All other combinations are a non-homogeneous array error + (other1, other2) => Err(TypeInferenceError::NoirTypeError( + TypeCheckError::NonHomogeneousArray { + first_type: other1.to_string(), + first_location: location, + first_index: 0, + second_type: other2.to_string(), + second_location: location, + second_index: 0, + }, + )), + } + } + join_types(acc, current_expr.ann.1.clone(), location) + }, + )?; + + let concrete_element_type = + concretize_type(unified_opt_type, &default_literal_type).ok_or( + TypeInferenceError::NoirTypeError( + TypeCheckError::TypeAnnotationNeededOnArrayLiteral { + is_array: true, + location, + }, + ), + )?; + + exprs + .into_iter() + .try_for_each(|expr| expr.unify_with_type(concrete_element_type.clone()))?; + + OptionalType::Well(NoirType::Array( + exprs.len() as u32, + Box::new(concrete_element_type), + )) + } + ExprF::StructureAccess { .. } => { + // All StructureAccess have been converted into TupleAccess expressions + unreachable!() + } + }; + + Ok(SpannedPartiallyTypedExpr { ann: (location, exprf_type), expr: Box::new(exprf) }) + }, + )?; + + let fully_typed_expr: SpannedTypedExpr = + try_cata(sote, &|(location, otype), exprf| match otype { + OptionalType::Well(t) => { + Ok(SpannedTypedExpr { ann: (location, t), expr: Box::new(exprf) }) + } + _ => Err(format!("Expr {:?} still has no type ({:?})", exprf, otype)), + }) + .expect("Typing should have either succeeded or have resulted in an expected error"); + + // NOTE: only the `FUNC_RETURN_VAR_NAME` variable should have no id + assert!(cata(fully_typed_expr.clone(), &|ann, exprf| match exprf { + ExprF::Variable(Variable { path: _, name, id }) => { + let res = if name == FUNC_RETURN_VAR_NAME { id.is_none() } else { id.is_some() }; + if !res { + dbg!(ann, name, id); + } + res + } + + ExprF::FnCall { args, .. } => args.into_iter().all(identity), + ExprF::Quantified { expr, .. } => expr, + ExprF::Parenthesised { expr } => expr, + ExprF::UnaryOp { expr, .. } => expr, + ExprF::BinaryOp { expr_left, expr_right, .. } => expr_left && expr_right, + ExprF::Index { expr, index } => expr && index, + ExprF::TupleAccess { expr, .. } => expr, + ExprF::Cast { expr, .. } => expr, + ExprF::Tuple { exprs } => exprs.into_iter().all(identity), + ExprF::Array { exprs } => exprs.into_iter().all(identity), + + // Non-recursive variants don't carry information + ExprF::Literal { .. } => true, + + // All StructureAccess have been converted into TupleAccess expressions + ExprF::StructureAccess { .. } => { + unreachable!() + } + })); + + Ok(fully_typed_expr) +} + +#[cfg(test)] +mod tests { + use noirc_errors::{Location, Span}; + use noirc_frontend::ast::IntegerBitSize; + use noirc_frontend::shared::Signedness; + use num_traits::Num; + use std::convert::identity; + + use super::*; + + use crate::{ + Attribute, + ast::{Literal, Variable, cata, strip_ann}, + parse::{parse_attribute, tests::*}, + }; + + #[test] + fn test_integer_types() { + { + let bi127 = BigInt::from_str_radix("127", 10).unwrap(); + let bi128 = BigInt::from_str_radix("128", 10).unwrap(); + let bi129 = BigInt::from_str_radix("129", 10).unwrap(); + let bin127 = BigInt::from_str_radix("-127", 10).unwrap(); + let bin128 = BigInt::from_str_radix("-128", 10).unwrap(); + let bin129 = BigInt::from_str_radix("-129", 10).unwrap(); + + let hole_size = IntegerBitSize::Eight; + let hole_sign = Signedness::Signed; + + let bi127_fit = bi_can_fit_in(&bi127, &hole_size, &hole_sign); + let bi128_fit = bi_can_fit_in(&bi128, &hole_size, &hole_sign); + let bi129_fit = bi_can_fit_in(&bi129, &hole_size, &hole_sign); + let bin127_fit = bi_can_fit_in(&bin127, &hole_size, &hole_sign); + let bin128_fit = bi_can_fit_in(&bin128, &hole_size, &hole_sign); + let bin129_fit = bi_can_fit_in(&bin129, &hole_size, &hole_sign); + + assert_eq!(bi127_fit, FitsIn::Yes); + assert_eq!( + bi128_fit, + FitsIn::No { need: Some(NoirType::Integer(hole_sign, IntegerBitSize::Sixteen)) } + ); + assert_eq!( + bi129_fit, + FitsIn::No { need: Some(NoirType::Integer(hole_sign, IntegerBitSize::Sixteen)) } + ); + + assert_eq!(bin127_fit, FitsIn::Yes); + assert_eq!(bin128_fit, FitsIn::Yes); + assert_eq!( + bin129_fit, + FitsIn::No { need: Some(NoirType::Integer(hole_sign, IntegerBitSize::Sixteen)) } + ); + } + + { + let bi255 = BigInt::from_str_radix("255", 10).unwrap(); + let bi256 = BigInt::from_str_radix("256", 10).unwrap(); + let bi257 = BigInt::from_str_radix("257", 10).unwrap(); + let bin1 = BigInt::from_str_radix("-1", 10).unwrap(); + + let hole_size = IntegerBitSize::Eight; + let hole_sign = Signedness::Unsigned; + + let bi255_fit = bi_can_fit_in(&bi255, &hole_size, &hole_sign); + let bi256_fit = bi_can_fit_in(&bi256, &hole_size, &hole_sign); + let bi257_fit = bi_can_fit_in(&bi257, &hole_size, &hole_sign); + let bin1_fit = bi_can_fit_in(&bin1, &hole_size, &hole_sign); + + assert_eq!(bi255_fit, FitsIn::Yes); + assert_eq!( + bi256_fit, + FitsIn::No { need: Some(NoirType::Integer(hole_sign, IntegerBitSize::Sixteen)) } + ); + assert_eq!( + bi257_fit, + FitsIn::No { need: Some(NoirType::Integer(hole_sign, IntegerBitSize::Sixteen)) } + ); + + assert_eq!( + bin1_fit, + FitsIn::No { + need: Some(NoirType::Integer(Signedness::Signed, IntegerBitSize::One)) + } + ); + } + } + + #[test] + fn test_whole_attribute() { + let attribute = "ensures(result >= a + (16 / 2 % (7 * 4)))"; + let state = empty_state(); + let attribute = parse_attribute( + attribute, + Location { span: Span::inclusive(0, attribute.len() as u32), file: Default::default() }, + state.function, + state.global_constants, + state.functions, + ) + .unwrap(); + let Attribute::Ensures(spanned_expr) = attribute else { panic!() }; + let spanned_typed_expr = type_infer(&state, spanned_expr).unwrap(); + assert!( + cata(spanned_typed_expr, &|(_, expr_type), expr| { + match expr { + ExprF::Literal { value: Literal::Int(_) } => { + expr_type + == NoirType::Integer(Signedness::Signed, IntegerBitSize::ThirtyTwo) + } + ExprF::FnCall { args, .. } => args.into_iter().all(identity), + ExprF::Quantified { expr, .. } => expr, + ExprF::Parenthesised { expr } => expr, + ExprF::UnaryOp { expr, .. } => expr, + ExprF::BinaryOp { expr_left, expr_right, .. } => expr_left && expr_right, + ExprF::Index { expr, index } => expr && index, + ExprF::TupleAccess { expr, .. } => expr, + ExprF::Cast { expr, .. } => expr, + ExprF::Tuple { exprs } => exprs.into_iter().all(identity), + ExprF::Array { exprs } => exprs.into_iter().all(identity), + + // Non-recursive variants don't carry information + ExprF::Literal { value: Literal::Bool(_) } | ExprF::Variable(_) => true, + + ExprF::StructureAccess { .. } => unreachable!(), + } + }), + "All integer literals have the correct inferred type" + ); + } + + #[test] + fn test_quantifiers() { + let attribute = "ensures(exists(| i , j | result >= a + (16 / i % (7 * 4))))"; + let state = empty_state(); + let attribute = parse_attribute( + attribute, + Location { span: Span::inclusive(0, attribute.len() as u32), file: Default::default() }, + state.function, + state.global_constants, + state.functions, + ) + .unwrap(); + let Attribute::Ensures(spanned_expr) = attribute else { panic!() }; + let spanned_typed_expr = type_infer(&state, spanned_expr).unwrap(); + assert!( + cata(spanned_typed_expr.clone(), &|(_, expr_type), expr| { + match expr { + ExprF::Literal { value: Literal::Int(_) } => { + expr_type + == NoirType::Integer(Signedness::Signed, IntegerBitSize::ThirtyTwo) + } + + ExprF::FnCall { args, .. } => args.into_iter().all(identity), + ExprF::Quantified { expr, .. } => expr, + ExprF::Parenthesised { expr } => expr, + ExprF::UnaryOp { expr, .. } => expr, + ExprF::BinaryOp { expr_left, expr_right, .. } => expr_left && expr_right, + ExprF::Index { expr, index } => expr && index, + ExprF::TupleAccess { expr, .. } => expr, + ExprF::Cast { expr, .. } => expr, + ExprF::Tuple { exprs } => exprs.into_iter().all(identity), + ExprF::Array { exprs } => exprs.into_iter().all(identity), + + // Non-recursive variants don't carry information + ExprF::Literal { value: Literal::Bool(_) } | ExprF::Variable(_) => true, + + ExprF::StructureAccess { .. } => unreachable!(), + } + }), + "All integer literals have the correct inferred type" + ); + assert!( + cata(spanned_typed_expr, &|(_, expr_type), expr| { + match expr { + ExprF::Variable(Variable { name, .. }) => { + if name == "i" { + expr_type + == NoirType::Integer(Signedness::Signed, IntegerBitSize::ThirtyTwo) + } else { + true + } + } + + ExprF::FnCall { args, .. } => args.into_iter().all(identity), + ExprF::Quantified { expr, .. } => expr, + ExprF::Parenthesised { expr } => expr, + ExprF::UnaryOp { expr, .. } => expr, + ExprF::BinaryOp { expr_left, expr_right, .. } => expr_left && expr_right, + ExprF::Index { expr, index } => expr && index, + ExprF::TupleAccess { expr, .. } => expr, + ExprF::Cast { expr, .. } => expr, + ExprF::Tuple { exprs } => exprs.into_iter().all(identity), + ExprF::Array { exprs } => exprs.into_iter().all(identity), + + // Non-recursive variants don't carry information + ExprF::Literal { .. } => true, + + ExprF::StructureAccess { .. } => unreachable!(), + } + }), + "All bound variables have the correct inferred type" + ); + } + + #[test] + fn test_index() { + let attribute = "ensures(xs[1 + 1] > 5)"; + let state = empty_state(); + let attribute = parse_attribute( + attribute, + Location { span: Span::inclusive(0, attribute.len() as u32), file: Default::default() }, + state.function, + state.global_constants, + state.functions, + ) + .unwrap(); + let Attribute::Ensures(spanned_expr) = attribute else { panic!() }; + let spanned_typed_expr = type_infer(&state, spanned_expr).unwrap(); + dbg!(&spanned_typed_expr); + assert_eq!(spanned_typed_expr.ann.1, NoirType::Bool); + } + + #[test] + fn test_dereference_index() { + let attribute = "ensures((*rxs)[1 + 1] > 5)"; + let state = empty_state(); + let attribute = parse_attribute( + attribute, + Location { span: Span::inclusive(0, attribute.len() as u32), file: Default::default() }, + state.function, + state.global_constants, + state.functions, + ) + .unwrap(); + let Attribute::Ensures(spanned_expr) = attribute else { panic!() }; + let spanned_typed_expr = type_infer(&state, spanned_expr).unwrap(); + dbg!(&spanned_typed_expr); + assert_eq!(spanned_typed_expr.ann.1, NoirType::Bool); + } + + #[test] + fn test_operators_mixed_types() { + let attribute = "ensures(1 + true)"; + let state = empty_state(); + let attribute = parse_attribute( + attribute, + Location { span: Span::inclusive(0, attribute.len() as u32), file: Default::default() }, + state.function, + state.global_constants, + state.functions, + ) + .unwrap(); + let Attribute::Ensures(spanned_expr) = attribute else { panic!() }; + let type_inference_error = type_infer(&state, spanned_expr).unwrap_err(); + let TypeInferenceError::NoirTypeError(TypeCheckError::TypeMismatch { + expected_typ, + expr_typ, + expr_location, + }) = type_inference_error + else { + panic!() + }; + dbg!(&expr_typ, &expected_typ, &expr_location); + + // NOTE: untyped integer literal (same for quantifier variables) force the other argument + // to also be numeric + assert_eq!(expr_typ, "bool"); + assert_eq!(expected_typ, "a numeric type"); + } + + #[test] + fn test_bitshift() { + let attribute = "ensures(1 << 256)"; + let state = empty_state(); + let attribute = parse_attribute( + attribute, + Location { span: Span::inclusive(0, attribute.len() as u32), file: Default::default() }, + state.function, + state.global_constants, + state.functions, + ) + .unwrap(); + let Attribute::Ensures(spanned_expr) = attribute else { panic!() }; + let type_inference_error = type_infer(&state, spanned_expr).unwrap_err(); + let TypeInferenceError::IntegerLiteralDoesNotFit { + literal: _, + literal_type, + fit_into, + location: _, + message, + } = type_inference_error + else { + panic!() + }; + dbg!(&literal_type, &fit_into, &message); + assert_eq!(literal_type, NoirType::Integer(Signedness::Unsigned, IntegerBitSize::Eight)); + // NOTE: minimal size that fits `256` + assert_eq!( + fit_into, + Some(NoirType::Integer(Signedness::Unsigned, IntegerBitSize::Sixteen)) + ); + assert_eq!(message, "Integer literal 256 cannot fit in u8, needs at least Some(Integer(Unsigned, Sixteen)) or larger".to_string()); + } + + #[test] + fn test_tuple_access() { + let attribute = "ensures(user.0 ==> true)"; + let state = empty_state(); + let attribute = parse_attribute( + attribute, + Location { span: Span::inclusive(0, attribute.len() as u32), file: Default::default() }, + state.function, + state.global_constants, + state.functions, + ) + .unwrap(); + let Attribute::Ensures(spanned_expr) = attribute else { panic!() }; + let spanned_typed_expr = type_infer(&state, spanned_expr).unwrap(); + dbg!(&spanned_typed_expr); + assert_eq!(spanned_typed_expr.ann.1, NoirType::Bool); + } + + #[test] + fn test_tuple_access_combos() { + let attribute = "ensures(exists(|i| (0 <= i) & (i < 20) & xs[i] > 100))"; + let state = empty_state(); + let attribute = parse_attribute( + attribute, + Location { span: Span::inclusive(0, attribute.len() as u32), file: Default::default() }, + state.function, + state.global_constants, + state.functions, + ) + .unwrap(); + let Attribute::Ensures(spanned_expr) = attribute else { panic!() }; + let spanned_typed_expr = type_infer(&state, spanned_expr).unwrap(); + dbg!(&spanned_typed_expr); + assert_eq!(spanned_typed_expr.ann.1, NoirType::Bool); + } + + #[test] + fn test_unary_op_literals() { + let attribute = "ensures(result as Field != !15)"; + let state = empty_state(); + let attribute = parse_attribute( + attribute, + Location { span: Span::inclusive(0, attribute.len() as u32), file: Default::default() }, + state.function, + state.global_constants, + state.functions, + ) + .unwrap(); + let Attribute::Ensures(spanned_expr) = attribute else { panic!() }; + let spanned_typed_expr = type_infer(&state, spanned_expr).unwrap(); + dbg!(&spanned_typed_expr); + assert_eq!(spanned_typed_expr.ann.1, NoirType::Bool); + } + + #[test] + fn test_cast_simple() { + let annotation = "ensures(15 == 1 as u8)"; + let state = empty_state(); + let attribute = parse_attribute( + annotation, + Location { + span: Span::inclusive(0, annotation.len() as u32), + file: Default::default(), + }, + state.function, + state.global_constants, + state.functions, + ) + .unwrap(); + + let Attribute::Ensures(spanned_expr) = attribute else { panic!() }; + let spanned_typed_expr = type_infer(&state, spanned_expr).unwrap(); + dbg!(&strip_ann(spanned_typed_expr)); + // assert_eq!(spanned_typed_expr.ann.1, NoirType::Bool); + } + + #[test] + fn test_cast() { + let annotation = "ensures((15 as i16 - 3 > 2) & ((result as Field - 6) as u64 == 1 + a as u64 >> 4 as u8))"; + let state = empty_state(); + let attribute = parse_attribute( + annotation, + Location { + span: Span::inclusive(0, annotation.len() as u32), + file: Default::default(), + }, + state.function, + state.global_constants, + state.functions, + ) + .unwrap(); + + let Attribute::Ensures(spanned_expr) = attribute else { panic!() }; + let spanned_typed_expr = type_infer(&state, spanned_expr).unwrap(); + dbg!(&strip_ann(spanned_typed_expr)); + // assert_eq!(spanned_typed_expr.ann.1, NoirType::Bool); + } + + #[test] + fn test_double_cast() { + let annotation = "ensures(a == (a as i16) as i32)"; + let state = empty_state(); + let attribute = parse_attribute( + annotation, + Location { + span: Span::inclusive(0, annotation.len() as u32), + file: Default::default(), + }, + state.function, + state.global_constants, + state.functions, + ) + .unwrap(); + + let Attribute::Ensures(spanned_expr) = attribute else { panic!() }; + let spanned_typed_expr = type_infer(&state, spanned_expr).unwrap(); + dbg!(&strip_ann(spanned_typed_expr)); + // assert_eq!(spanned_typed_expr.ann.1, NoirType::Bool); + } + + #[test] + fn test_tuple_complex() { + let annotation = "ensures((1000, 5, 1000).1 == 15 as u8)"; + let state = empty_state(); + let attribute = parse_attribute( + annotation, + Location { + span: Span::inclusive(0, annotation.len() as u32), + file: Default::default(), + }, + state.function, + state.global_constants, + state.functions, + ) + .unwrap(); + + let Attribute::Ensures(spanned_expr) = attribute else { panic!() }; + let spanned_typed_expr = type_infer(&state, spanned_expr).unwrap(); + dbg!(&strip_ann(spanned_typed_expr)); + } + + #[test] + fn test_tuple() { + let annotation = "ensures(((), kek, true).2)"; + let state = empty_state(); + let attribute = parse_attribute( + annotation, + Location { + span: Span::inclusive(0, annotation.len() as u32), + file: Default::default(), + }, + state.function, + state.global_constants, + state.functions, + ) + .unwrap(); + + let Attribute::Ensures(spanned_expr) = attribute else { panic!() }; + let spanned_typed_expr = type_infer(&state, spanned_expr).unwrap(); + dbg!(&strip_ann(spanned_typed_expr)); + } + + #[test] + fn test_partial_tuple_equality() { + let annotation = "ensures((1 as u8, 15) == (1, 15 as i16))"; + let state = empty_state(); + let attribute = parse_attribute( + annotation, + Location { + span: Span::inclusive(0, annotation.len() as u32), + file: Default::default(), + }, + state.function, + state.global_constants, + state.functions, + ) + .unwrap(); + + let Attribute::Ensures(spanned_expr) = attribute else { panic!() }; + let spanned_typed_expr = type_infer(&state, spanned_expr).unwrap(); + dbg!(&strip_ann(spanned_typed_expr.clone())); + + let ExprF::BinaryOp { op: BinaryOp::Eq, expr_left, expr_right } = *spanned_typed_expr.expr + else { + panic!() + }; + + let ExprF::Tuple { exprs: _ } = *expr_left.expr else { panic!() }; + let ExprF::Tuple { exprs: _ } = *expr_right.expr else { panic!() }; + + // Assert that both tuple types are fully unified + assert_eq!( + expr_left.ann.1, + NoirType::Tuple(vec![ + NoirType::Integer(Signedness::Unsigned, IntegerBitSize::Eight), + NoirType::Integer(Signedness::Signed, IntegerBitSize::Sixteen) + ]) + ); + assert_eq!(expr_left.ann.1, expr_right.ann.1); + } + + #[test] + fn test_tuple_equality() { + let annotation = "ensures((1, 15) == pair)"; + let state = empty_state(); + let attribute = parse_attribute( + annotation, + Location { + span: Span::inclusive(0, annotation.len() as u32), + file: Default::default(), + }, + state.function, + state.global_constants, + state.functions, + ) + .unwrap(); + + let Attribute::Ensures(spanned_expr) = attribute else { panic!() }; + let spanned_typed_expr = type_infer(&state, spanned_expr).unwrap(); + dbg!(&strip_ann(spanned_typed_expr.clone())); + + let ExprF::BinaryOp { op: BinaryOp::Eq, expr_left, expr_right } = *spanned_typed_expr.expr + else { + panic!() + }; + + let ExprF::Tuple { exprs: _ } = *expr_left.expr else { panic!() }; + let ExprF::Variable(_) = *expr_right.expr else { panic!() }; + + // Assert that both tuple types are fully unified + assert_eq!( + expr_left.ann.1, + NoirType::Tuple(vec![ + NoirType::Integer(Signedness::Unsigned, IntegerBitSize::Sixteen), + NoirType::Field, + ]) + ); + assert_eq!(expr_left.ann.1, expr_right.ann.1); + } + + #[test] + fn test_array_equality() { + let annotation = "ensures([(1, 2), (1 as u8, 7), (8, 9 as i16)] == [(0, 0), (1 as u8, 2 as i16), (0, 0)])"; + let state = empty_state(); + let attribute = parse_attribute( + annotation, + Location { + span: Span::inclusive(0, annotation.len() as u32), + file: Default::default(), + }, + state.function, + state.global_constants, + state.functions, + ) + .unwrap(); + + let Attribute::Ensures(spanned_expr) = attribute else { panic!() }; + let spanned_typed_expr = type_infer(&state, spanned_expr).unwrap(); + dbg!(&strip_ann(spanned_typed_expr.clone())); + + let ExprF::BinaryOp { op: BinaryOp::Eq, expr_left, expr_right } = *spanned_typed_expr.expr + else { + panic!() + }; + + let ExprF::Array { exprs: _ } = *expr_left.expr else { panic!() }; + let ExprF::Array { exprs: _ } = *expr_right.expr else { panic!() }; + + // Assert that both array types are fully unified + assert_eq!( + expr_left.ann.1, + NoirType::Array( + 3, + Box::new(NoirType::Tuple(vec![ + NoirType::Integer(Signedness::Unsigned, IntegerBitSize::Eight), + NoirType::Integer(Signedness::Signed, IntegerBitSize::Sixteen) + ])) + ) + ); + assert_eq!(expr_left.ann.1, expr_right.ann.1); + } + + #[test] + fn test_array() { + let annotation = "ensures([15 as i32, a, 129 as i32][2])"; + let state = empty_state(); + let attribute = parse_attribute( + annotation, + Location { + span: Span::inclusive(0, annotation.len() as u32), + file: Default::default(), + }, + state.function, + state.global_constants, + state.functions, + ) + .unwrap(); + + let Attribute::Ensures(spanned_expr) = attribute else { panic!() }; + let spanned_typed_expr = type_infer(&state, spanned_expr).unwrap(); + dbg!(&strip_ann(spanned_typed_expr)); + } + + #[test] + fn test_monomorphization_request() { + let attribute = "ensures(f(result))"; + let state = empty_state(); + let attribute = parse_attribute( + attribute, + Location { span: Span::inclusive(0, attribute.len() as u32), file: Default::default() }, + state.function, + state.global_constants, + state.functions, + ) + .unwrap(); + let Attribute::Ensures(spanned_expr) = attribute else { panic!() }; + let type_inference_error = type_infer(&state, spanned_expr).unwrap_err(); + let TypeInferenceError::MonomorphizationRequest(MonomorphizationRequest { + function_identifier, + param_types, + }) = type_inference_error + else { + panic!() + }; + assert_eq!(function_identifier, "f"); + assert_eq!( + param_types, + vec![OptionalType::Well(NoirType::Integer( + Signedness::Signed, + IntegerBitSize::ThirtyTwo + ))] + ); + } +} diff --git a/compiler/fv_bridge/Cargo.toml b/compiler/fv_bridge/Cargo.toml new file mode 100644 index 00000000000..27c7d12bc9b --- /dev/null +++ b/compiler/fv_bridge/Cargo.toml @@ -0,0 +1,29 @@ +[package] +name = "fv_bridge" +version.workspace = true +authors.workspace = true +edition.workspace = true +rust-version.workspace = true +license.workspace = true + +[lints] +workspace = true + + +[dependencies] +vir.workspace = true +serde.workspace = true +noirc_errors.workspace = true +noirc_frontend.workspace = true +noirc_evaluator.workspace = true +noirc_driver.workspace = true +fm.workspace = true +iter-extended.workspace = true +formal_verification.workspace = true +acvm.workspace = true +num-bigint.workspace = true +num-traits.workspace = true +thiserror.workspace = true + +[dev-dependencies] +iter-extended.workspace = true diff --git a/compiler/fv_bridge/src/errors.rs b/compiler/fv_bridge/src/errors.rs new file mode 100644 index 00000000000..97cbbff15f5 --- /dev/null +++ b/compiler/fv_bridge/src/errors.rs @@ -0,0 +1,83 @@ +use fm::FileId; +use formal_verification::{ + parse::errors::{self, ParserError, ParserErrorKind, ParserErrorWithLocation}, + typing::TypeInferenceError, +}; +use noirc_driver::CompileError; +use noirc_errors::{CustomDiagnostic, Location}; +use noirc_frontend::{ + hir::{resolution::errors::ResolverError, type_check::TypeCheckError}, + monomorphization::{ast::Type, errors::MonomorphizationError}, + parser::ParserError as NoirParserError, +}; +use thiserror::Error; + +use crate::typed_attrs_to_vir::signed_field_from_bigint_wrapping; + +pub(crate) enum MonomorphizationErrorBundle { + MonomorphizationError(MonomorphizationError), + FvError(FvMonomorphizationError), + TypeError(TypeCheckError), + ParserErrors(Vec), + ResolverError(ResolverError), +} + +pub(crate) enum CompilationErrorBundle { + CompileError(CompileError), + FvError(FvMonomorphizationError), + TypeError(TypeCheckError), + ParserErrors(Vec), + ResolverError(ResolverError), +} + +#[derive(Error, Debug, Clone)] +pub(crate) enum FvMonomorphizationError { + #[error("Non-ghost function {func_name} was called in FV annotation")] + ExecInSpecError { func_name: String, location: Location }, +} + +impl From for CustomDiagnostic { + fn from(value: FvMonomorphizationError) -> Self { + match value { + FvMonomorphizationError::ExecInSpecError { func_name, location } => { + CustomDiagnostic::simple_error( + format!("Non-ghost function {func_name} was called in FV annotation"), + String::new(), + location, + ) + } + } + } +} + +impl From for MonomorphizationErrorBundle { + fn from(value: TypeInferenceError) -> Self { + match value { + TypeInferenceError::MonomorphizationRequest(monomorphization_request) => { + panic!("Monomorphization request can not be converted to an error") + } + TypeInferenceError::IntegerLiteralDoesNotFit { + literal, + literal_type, + fit_into, + location, + message, + } => MonomorphizationErrorBundle::TypeError( + TypeCheckError::IntegerLiteralDoesNotFitItsType { + expr: signed_field_from_bigint_wrapping(literal), + ty: noirc_frontend::Type::Unit, // We present the range which is enough + range: { + match fit_into { + Some(Type::Integer(_, bit_size)) => bit_size.to_string(), + _ => "Unknown range".to_string(), + } + }, + location, + }, + ), + TypeInferenceError::NoirTypeError(type_check_error) => { + MonomorphizationErrorBundle::TypeError(type_check_error) + } + } + } +} diff --git a/compiler/fv_bridge/src/lib.rs b/compiler/fv_bridge/src/lib.rs new file mode 100644 index 00000000000..398a191ca0d --- /dev/null +++ b/compiler/fv_bridge/src/lib.rs @@ -0,0 +1,711 @@ +use fm::FileId; +use formal_verification::ast::{AnnExpr, SpannedTypedExpr}; +use formal_verification::convert_structs::convert_struct_access_to_tuple_access; +use formal_verification::inline_globals::inline_global_consts; +use formal_verification::type_conversion::convert_mast_to_noir_type; +use formal_verification::typing::{OptionalType, TypeInferenceError, type_infer}; +use formal_verification::{State, parse::parse_attribute}; +use iter_extended::vecmap; +use noirc_driver::{CompilationResult, CompileError, CompileOptions, check_crate}; +use noirc_errors::Location; +use noirc_errors::{CustomDiagnostic, Span}; +use noirc_evaluator::vir::vir_gen::Attribute; +use noirc_evaluator::vir::vir_gen::expr_to_vir::std_functions::OLD; +use noirc_evaluator::{ + errors::{RuntimeError, SsaReport}, + vir::{create_verus_vir_with_ready_annotations, vir_gen::BuildingKrateError}, +}; +use noirc_frontend::Kind; +use noirc_frontend::graph::CrateGraph; +use noirc_frontend::hir::def_map::{ + DefMaps, LocalModuleId, ModuleDefId, ModuleId, fully_qualified_module_path, +}; +use noirc_frontend::hir_def::expr::HirCallExpression; +use noirc_frontend::hir_def::expr::{HirExpression, HirLiteral}; +use noirc_frontend::hir_def::stmt::HirPattern; +use noirc_frontend::monomorphization::ast::LocalId; +use noirc_frontend::node_interner::{ExprId, FunctionModifiers, GlobalValue}; +use noirc_frontend::token::SecondaryAttribute; +use noirc_frontend::{ + debug::DebugInstrumenter, + graph::CrateId, + hir::Context, + monomorphization::{ + Monomorphizer, + ast::{FuncId, Program}, + debug_types::DebugTypeTracker, + errors::MonomorphizationError, + perform_impl_bindings, perform_instantiation_bindings, undo_instantiation_bindings, + }, + node_interner::{self, NodeInterner}, + parser::ParserError, + token::SecondaryAttributeKind, +}; +use std::cell::RefCell; +use std::collections::{BTreeMap, HashMap, HashSet}; +use std::rc::Rc; +use vir::ast::Krate; + +use crate::errors::{CompilationErrorBundle, MonomorphizationErrorBundle}; +use crate::typed_attrs_to_vir::convert_typed_attribute_to_vir_attribute; + +mod errors; +pub mod typed_attrs_to_vir; + +pub fn compile_and_build_vir_krate( + context: &mut Context, + crate_id: CrateId, + options: &CompileOptions, +) -> CompilationResult { + modified_compile_main(context, crate_id, options) +} + +fn modified_compile_main( + context: &mut Context, + crate_id: CrateId, + options: &CompileOptions, +) -> CompilationResult { + let (_, mut warnings) = check_crate(context, crate_id, options)?; + + let main = context.get_main_function(&crate_id).ok_or_else(|| { + let err = CustomDiagnostic::from_message( + "cannot compile crate into a program as it does not contain a `main` function", + FileId::default(), + ); + vec![err] + })?; + + let compiled_program = + modified_compile_no_check(context, options, main).map_err(|error| match error { + CompilationErrorBundle::CompileError(compile_error) => vec![compile_error.into()], + CompilationErrorBundle::FvError(fv_monomorphization_error) => { + vec![fv_monomorphization_error.into()] + } + CompilationErrorBundle::TypeError(type_check_error) => { + vec![CustomDiagnostic::from(&type_check_error)] + } + CompilationErrorBundle::ParserErrors(parser_errors) => { + parser_errors.into_iter().map(CustomDiagnostic::from).collect() + } + CompilationErrorBundle::ResolverError(resolver_error) => { + vec![CustomDiagnostic::from(&resolver_error)] + } + })?; + + let compilation_warnings = vecmap(compiled_program.warnings.clone(), CustomDiagnostic::from); + if options.deny_warnings && !compilation_warnings.is_empty() { + return Err(compilation_warnings); + } + if !options.silence_warnings { + warnings.extend(compilation_warnings); + } + + Ok((compiled_program.krate, warnings)) +} + +// Something like the method `compile_no_check()` +fn modified_compile_no_check( + context: &mut Context, + options: &CompileOptions, + main_function: node_interner::FuncId, +) -> Result { + let force_unconstrained = options.force_brillig || options.minimal_ssa; + + let (program, fv_annotations) = modified_monomorphize( + main_function, + &mut context.def_interner, + &DebugInstrumenter::default(), + force_unconstrained, + &context.crate_graph, + &context.def_maps, + ) + .map_err(|e| match e { + MonomorphizationErrorBundle::MonomorphizationError(monomorphization_error) => { + CompilationErrorBundle::CompileError(CompileError::MonomorphizationError( + monomorphization_error, + )) + } + MonomorphizationErrorBundle::FvError(fv_monomorphization_error) => { + CompilationErrorBundle::FvError(fv_monomorphization_error) + } + MonomorphizationErrorBundle::TypeError(type_check_error) => { + CompilationErrorBundle::TypeError(type_check_error) + } + MonomorphizationErrorBundle::ParserErrors(parser_errors) => { + CompilationErrorBundle::ParserErrors(parser_errors) + } + MonomorphizationErrorBundle::ResolverError(resolver_error) => { + CompilationErrorBundle::ResolverError(resolver_error) + } + })?; + + if options.show_monomorphized { + println!("{program}"); + } + + Ok(KrateAndWarnings { + krate: create_verus_vir_with_ready_annotations(program, fv_annotations) + .map_err(|BuildingKrateError::Error(msg)| { + RuntimeError::InternalError(noirc_evaluator::errors::InternalError::General { + message: msg, + call_stack: vec![], + }) + }) + .map_err(|runtime_error| { + CompilationErrorBundle::CompileError(CompileError::RuntimeError(runtime_error)) + })?, + warnings: vec![], + parse_annotations_errors: vec![], // TODO(totel): Get the errors from `modified_monomorphize()` + }) +} + +enum TypedAttribute { + Ghost, + Requires(SpannedTypedExpr), + Ensures(SpannedTypedExpr), +} + +fn modified_monomorphize( + main: node_interner::FuncId, + interner: &mut NodeInterner, + debug_instrumenter: &DebugInstrumenter, + force_unconstrained: bool, + crate_graph: &CrateGraph, + def_maps: &DefMaps, +) -> Result<(Program, Vec<(FuncId, Vec)>), MonomorphizationErrorBundle> { + let debug_type_tracker = DebugTypeTracker::build_from_debug_instrumenter(debug_instrumenter); + // NOTE: Monomorphizer is a `pub(crate)` struct which we changed to pub + let mut monomorphizer = Monomorphizer::new(interner, debug_type_tracker); + monomorphizer.in_unconstrained_function = force_unconstrained; + let function_sig = monomorphizer + .compile_main(main) + .map_err(MonomorphizationErrorBundle::MonomorphizationError)?; + let mut new_ids_to_old_ids: HashMap = HashMap::new(); + new_ids_to_old_ids.insert(Program::main_id(), main); + + while !monomorphizer.queue.is_empty() { + let (next_fn_id, new_id, bindings, trait_method, is_unconstrained, location) = + monomorphizer.queue.pop_front().unwrap(); + monomorphizer.locals.clear(); + + monomorphizer.in_unconstrained_function = is_unconstrained; + + perform_instantiation_bindings(&bindings); + let interner = &monomorphizer.interner; + let impl_bindings = perform_impl_bindings(interner, trait_method, next_fn_id, location) + .map_err(MonomorphizationError::InterpreterError) + .map_err(MonomorphizationErrorBundle::MonomorphizationError)?; + + monomorphizer + .function(next_fn_id, new_id, location) + .map_err(MonomorphizationErrorBundle::MonomorphizationError)?; + new_ids_to_old_ids.insert(new_id, next_fn_id); + undo_instantiation_bindings(impl_bindings); + undo_instantiation_bindings(bindings); + } + + let func_sigs = monomorphizer + .finished_functions + .iter() + .flat_map(|(_, f)| { + if (!force_unconstrained && f.inline_type.is_entry_point()) + || f.id == Program::main_id() + { + Some(f.func_sig.clone()) + } else { + None + } + }) + .collect(); + + // Clone because of the borrow checker + let globals = monomorphizer.finished_globals.clone().into_iter().collect::>(); + + let min_available_id: u32 = + monomorphizer.locals.values().map(|LocalId(id)| *id).max().unwrap_or_default() + 1; + let min_available_id = Rc::new(RefCell::new(min_available_id)); + + let functions_to_process: Vec<(FuncId, node_interner::FuncId)> = monomorphizer + .finished_functions + .keys() + .rev() + .copied() + .filter_map(|new_func_id| { + new_ids_to_old_ids.get(&new_func_id).map(|old_id| (new_func_id, *old_id)) + }) + .collect(); + + let mut fv_annotations = Vec::with_capacity(functions_to_process.len()); + // Functions which get resolved via a MonomorphRequest we have to + // manually add ghost attributes to them. + let mut to_be_added_ghost_attribute: HashSet = HashSet::new(); + + // Initialize the globals map and a tracker for the last seen crate ID outside the loop. + let mut globals_with_paths: HashMap = HashMap::new(); + let mut last_crate_id: Option = None; + + for (new_func_id, old_id) in functions_to_process { + let parameters_hir_types: HashMap = + collect_parameter_hir_types(&monomorphizer, &old_id); + + // Determine the crate ID of the function currently being processed. + let current_func_crate_id = monomorphizer.interner.function_meta(&old_id).source_crate; + let current_func_module_id = monomorphizer.interner.function_meta(&old_id).source_module; + + // Conditionally update the globals map based on the current crate context. + update_globals_if_needed( + &mut last_crate_id, + &mut globals_with_paths, + current_func_crate_id, + current_func_module_id, + &monomorphizer, + def_maps, + crate_graph, + ); + + let attribute_data: Vec<_> = monomorphizer + .interner + .function_attributes(&old_id) + .secondary + .iter() + .filter_map(|attribute| { + if let SecondaryAttributeKind::Tag(annotation) = &attribute.kind { + Some((annotation.as_str().to_owned(), attribute.location)) + } else { + None + } + }) + .collect(); + + let mut processed_attributes = Vec::new(); + + for (annotation_body, location) in attribute_data { + let function_for_parser = &monomorphizer.finished_functions[&new_func_id]; + + // NOTE: #['...] + // ^^^^^^^ - received `Location` + // ^^^ - relevant stuff + let location = Location { + span: Span::inclusive(location.span.start() + 3, location.span.end() - 1), + ..location + }; + + let parsed_attribute = parse_attribute( + &annotation_body, + location, + function_for_parser, + &globals, + &monomorphizer.finished_functions, + ) + .map_err(|e| MonomorphizationErrorBundle::ParserErrors(e.0))?; + // Ghost functions always get a monomorphization request because + // they are not part of the monomorphizer.finished_functions + let typed_attribute = match parsed_attribute { + formal_verification::Attribute::Ghost => TypedAttribute::Ghost, + formal_verification::Attribute::Ensures(expr) => { + let typed_expr = type_infer_attribute_expr( + &mut monomorphizer, + new_func_id, + &globals, + min_available_id.clone(), + ¶meters_hir_types, + &globals_with_paths, + expr, + &mut new_ids_to_old_ids, + &mut to_be_added_ghost_attribute, + )?; + TypedAttribute::Ensures(typed_expr) + } + formal_verification::Attribute::Requires(expr) => { + let typed_expr = type_infer_attribute_expr( + &mut monomorphizer, + new_func_id, + &globals, + min_available_id.clone(), + ¶meters_hir_types, + &globals_with_paths, + expr, + &mut new_ids_to_old_ids, + &mut to_be_added_ghost_attribute, + )?; + TypedAttribute::Requires(typed_expr) + } + }; + + let final_state = State { + function: &monomorphizer.finished_functions[&new_func_id], + global_constants: &globals, + functions: &monomorphizer.finished_functions, + min_local_id: min_available_id.clone(), + }; + + processed_attributes + .push(convert_typed_attribute_to_vir_attribute(typed_attribute, &final_state)); + } + + fv_annotations.push((new_func_id, processed_attributes)); + } + + to_be_added_ghost_attribute.into_iter().for_each(|func_id| { + fv_annotations.push((func_id, vec![Attribute::Ghost])); + }); + + let functions = vecmap(monomorphizer.finished_functions, |(_, f)| f); + + let (debug_variables, debug_functions, debug_types) = + monomorphizer.debug_type_tracker.extract_vars_and_types(); + + let program = Program::new( + functions, + func_sigs, + function_sig, + monomorphizer.return_location, + globals, + debug_variables, + debug_functions, + debug_types, + ); + + Ok((program.handle_ownership(), fv_annotations)) +} + +pub struct KrateAndWarnings { + pub krate: Krate, + pub warnings: Vec, + pub parse_annotations_errors: Vec, +} + +// Helper function using a bounded for-loop for safer retries. +/// Does type inferring and processes monomorphization requests. +/// Returns the typed attribute expression and a flag if monomorphization +/// request was processed. +fn type_infer_attribute_expr( + monomorphizer: &mut Monomorphizer, + new_func_id: FuncId, + globals: &BTreeMap< + noirc_frontend::monomorphization::ast::GlobalId, + ( + String, + noirc_frontend::monomorphization::ast::Type, + noirc_frontend::monomorphization::ast::Expression, + ), + >, + min_available_id: Rc>, + parameters_hir_types: &HashMap, + pathed_globals_with_values: &HashMap, + expr: AnnExpr, + new_ids_to_old_ids: &mut HashMap, + to_be_added_ghost_attribute: &mut HashSet, +) -> Result { + // Set a reasonable limit to prevent infinite loops in case of a bug. + const MAX_RETRIES: u32 = 100; + // TODO(totel): Check if a monomorphization request was send for the same function twice + // This will indicate that we have reached an infinite recursion point. (Some would call it a fix point) + for _ in 0..MAX_RETRIES { + // The following two variables are defined inside of the `for` loop + // because of the borrow checker. + let function = &monomorphizer.finished_functions[&new_func_id]; + let state = State { + function, + global_constants: &globals, + functions: &monomorphizer.finished_functions, + min_local_id: min_available_id.clone(), + }; + + let expr = convert_struct_access_to_tuple_access(expr.clone(), parameters_hir_types) + .map_err(|e| match e { + formal_verification::convert_structs::ResolverOrTypeError::ResolverError( + resolver_error, + ) => MonomorphizationErrorBundle::ResolverError(resolver_error), + formal_verification::convert_structs::ResolverOrTypeError::TypeError( + type_check_error, + ) => MonomorphizationErrorBundle::TypeError(type_check_error), + })?; + + let param_names: Vec<&str> = state + .function + .parameters + .iter() + .map(|(_, _, param_name, _, _)| param_name.as_str()) + .collect(); + // NOTE: If a global variable is added to the scope via `use foo::x` it wont be added to + // the `finished_globals` map unless it's being used somewhere in a function's body. + // Therefore the user has to use the full path for global variables even though they + // are added to the scope. + + // NOTE: Because the `finished_globals` map doesn't contain + // all globals but only the ones which are used inside of function's + // body and the fact that we can not easily add values to that map, + // we are doing the following: + // We are gathering all globals from the HIR form of the AST. + // We visit the FV annotation AST and if we encounter a node which + // is a global variable, we inline the const value of that global variable. + + let expr = inline_global_consts(expr, pathed_globals_with_values, ¶m_names) + .map_err(MonomorphizationErrorBundle::ResolverError)?; + + match type_infer(&state, expr.clone()) { + Ok(typed_expr) => { + // Success, return immediately. + return Ok(typed_expr); + } + Err(type_error) => match type_error { + TypeInferenceError::MonomorphizationRequest(request) => { + // This is a recoverable error. Try to resolve it. + monomorphize_one_function( + &request.function_identifier, + request.param_types, + monomorphizer, + new_ids_to_old_ids, + to_be_added_ghost_attribute, + )?; + // After monomorphizing the function try to type infer again. + } + other_error => { + // This is an unrecoverable error, return immediately. + return Err(MonomorphizationErrorBundle::from(other_error)); + } + }, + } + } + + // If the loop finishes, we've exceeded the retry limit. This indicates a likely bug. + // TODO(totel): Define a better error + panic!("Monomorphization limit reached") +} + +fn monomorphize_one_function( + func_name: &str, + param_types: Vec, + monomorphizer: &mut Monomorphizer, + new_ids_to_old_ids: &mut HashMap, + to_be_added_ghost_attribute: &mut HashSet, +) -> Result<(), MonomorphizationErrorBundle> { + let func_id = monomorphizer.interner.find_function(func_name).expect(&format!( + "The provided function name {}, was not found during the completion of MonomorphRequest", + func_name + )); + let func_id_as_expr_id = monomorphizer.interner.function(&func_id).as_expr(); + + let pseudo_args: Vec = std::iter::repeat_with(|| { + monomorphizer.interner.push_expr_full( + HirExpression::Literal(HirLiteral::Bool(true)), + Location::dummy(), + noirc_frontend::Type::Bool, + ) + }) + .take(param_types.len()) + .collect(); + + let pseudo_call_expr = HirExpression::Call(HirCallExpression { + func: func_id_as_expr_id, + arguments: pseudo_args, + location: Location::dummy(), + is_macro_call: false, + }); + + let pseudo_call_expr_id = monomorphizer.interner.push_expr_full( + pseudo_call_expr, + Location::dummy(), + noirc_frontend::Type::Unit, + ); + + let mut typ_bindings = noirc_frontend::Type::Unit.instantiate(&monomorphizer.interner).1; + + // Bind generic types to the type used in the function call + monomorphizer + .interner + .function_meta(&func_id) + .parameters + .0 + .iter() + .map(|(_pattern, typ, _visibility)| typ) + .enumerate() + .filter_map(|(pos, typ)| match typ { + noirc_frontend::Type::NamedGeneric(named_generic) => { + Some((pos, &named_generic.type_var)) + } + noirc_frontend::Type::TypeVariable(type_var) => Some((pos, type_var)), + _ => None, + }) + .for_each(|(param_index, type_var)| { + // The last argument of method `.insert` is the important one + typ_bindings.insert( + type_var.id(), + ( + type_var.clone(), + Kind::Normal, + convert_mast_to_noir_type( + param_types[param_index] + .clone() + .unwrap_or(noirc_frontend::monomorphization::ast::Type::Field), + ), + ), + ); + }); + + monomorphizer.interner.store_instantiation_bindings(pseudo_call_expr_id, typ_bindings); + + // NOTE: `queue_function` was made public by us + monomorphizer.queue_function( + func_id, + pseudo_call_expr_id, + monomorphizer.interner.id_type(func_id_as_expr_id), + vec![], + None, + ); + + while !monomorphizer.queue.is_empty() { + let (next_fn_id, new_id, bindings, trait_method, is_unconstrained, location) = + monomorphizer.queue.pop_front().unwrap(); + monomorphizer.locals.clear(); + + monomorphizer.in_unconstrained_function = is_unconstrained; + + perform_instantiation_bindings(&bindings); + let interner = &monomorphizer.interner; + let impl_bindings = perform_impl_bindings(interner, trait_method, next_fn_id, location) + .map_err(MonomorphizationError::InterpreterError) + .map_err(MonomorphizationErrorBundle::MonomorphizationError)?; + + monomorphizer + .function(next_fn_id, new_id, location) + .map_err(MonomorphizationErrorBundle::MonomorphizationError)?; + new_ids_to_old_ids.insert(new_id, next_fn_id); + undo_instantiation_bindings(impl_bindings); + undo_instantiation_bindings(bindings); + + if has_ghost_attribute(monomorphizer.interner.function_modifiers(&func_id)) { + to_be_added_ghost_attribute.insert(new_id); + } else if func_name == OLD { + // Note: We don't want to monomorphize `fv_std::old` into + // a ghost function because we may get a verifier error for + // having a ghost function with a mut reference parameter type. + + // The function call to `fv_std::old` gets converted to a special + // Verus expressions anyways. Therefore the function `old` is not + // being actually called anywhere in the code. + + // Therefore we don't want to produce an error + } else { + // A non-ghost function has been called in a FV annotation. + // This isn't allowed and we have to produce an adequate error. + + return Err(MonomorphizationErrorBundle::FvError( + errors::FvMonomorphizationError::ExecInSpecError { + func_name: func_name.to_string(), + location: monomorphizer.interner.function_meta(&func_id).location, + }, + )); + } + } + + Ok(()) +} + +fn has_ghost_attribute(func_modifiers: &FunctionModifiers) -> bool { + func_modifiers.attributes.secondary.iter().any(|SecondaryAttribute { kind, location: _ }| { + matches!(kind, SecondaryAttributeKind::Tag(tag) if tag == "ghost") + }) +} + +fn collect_parameter_hir_types( + monomorphizer: &Monomorphizer, + old_id: &node_interner::FuncId, +) -> HashMap { + let interner = &monomorphizer.interner; + let func_meta = interner.function_meta(old_id); + + let mut struct_arguments: HashMap = func_meta + .parameters + .0 + .iter() + .map(|(hir_pattern, typ, _)| { + // Extract identifier from the pattern + let ident = match hir_pattern { + HirPattern::Identifier(ident) => ident, + HirPattern::Mutable(inner, _) => match inner.as_ref() { + HirPattern::Identifier(ident) => ident, + // NOTE: We assume that only the Hir patterns "Identifier" and "Mutable" + // appear for function parameters + other => unreachable!( + "Expected HirPattern::Identifier inside HirPattern::Mutable, got: {:?}", + other + ), + }, + other => unreachable!( + "Expected HirPattern::Identifier or HirPattern::Mutable, got: {:?}", + other + ), + }; + + (interner.definition(ident.id).name.clone(), typ.clone()) + }) + .collect(); + + struct_arguments.insert("result".to_string(), func_meta.return_type().clone()); + + struct_arguments +} + +/// Updates the `globals_with_paths` map if the current function belongs to a new crate. +/// +/// The fully qualified paths of globals are relative to the crate being processed. +/// This function checks if the `current_func_crate_id` is different from the last one seen. +/// If it is, it re-calculates the paths for all globals and updates the map. +/// Otherwise, the existing map is considered valid and is not modified. +fn update_globals_if_needed( + last_crate_id: &mut Option, + globals_with_paths: &mut HashMap, + current_func_crate_id: CrateId, + current_func_module_id: LocalModuleId, + monomorphizer: &Monomorphizer, + def_maps: &DefMaps, + crate_graph: &CrateGraph, +) { + if last_crate_id.map_or(true, |id| id != current_func_crate_id) { + let fully_imported_globals: HashMap<_, _> = def_maps[¤t_func_crate_id] + [current_func_module_id] + .scope() + .values() + .into_iter() + .filter_map(|(identifier, map)| match map.get(&None) { + Some((ModuleDefId::GlobalId(id), ..)) => Some((id, identifier)), + _ => None, + }) + .collect(); + + *globals_with_paths = monomorphizer + .interner + .get_all_globals() + .iter() + .map(|global_info| { + let module_id = + ModuleId { krate: global_info.crate_id, local_id: global_info.local_id }; + + let mut module_path = fully_qualified_module_path( + def_maps, + crate_graph, + ¤t_func_crate_id, + module_id, + ); + // HACK: The function `fully_qualified_module_path` fails to consistently add `::` + // at the end of each path. Therefore we manually add double colons if they are missing. + if !module_path.ends_with("::") { + module_path.push_str("::"); + } + + let full_path = + if let Some(identifier) = fully_imported_globals.get(&global_info.id) { + identifier.identifier().to_string() + } else { + format!("{}{}", module_path, global_info.ident.as_str()) + }; + + (full_path, global_info.value.clone()) + }) + .collect(); + + *last_crate_id = Some(current_func_crate_id); + } +} diff --git a/compiler/fv_bridge/src/typed_attrs_to_vir.rs b/compiler/fv_bridge/src/typed_attrs_to_vir.rs new file mode 100644 index 00000000000..6933970ddfb --- /dev/null +++ b/compiler/fv_bridge/src/typed_attrs_to_vir.rs @@ -0,0 +1,421 @@ +use std::sync::Arc; + +use formal_verification::{ + State, + ast::{BinaryOp, ExprF, Quantifier, SpannedTypedExpr, Variable, cata}, +}; +use noirc_evaluator::vir::vir_gen::{ + Attribute, build_span, build_span_no_id, + expr_to_vir::{ + expr::{function_name_to_vir_fun, numeric_const_to_vir_exprx, wrap_with_field_modulo}, + std_functions::handle_fv_std_call_in_annotations, + types::{ + ast_const_to_vir_type_const, ast_type_to_vir_type, get_bit_not_bitwidth, is_type_field, + }, + }, +}; +use noirc_frontend::monomorphization::FUNC_RETURN_VAR_NAME; +use vir::{ + ast::{ + AirQuant, BinaryOp as VirBinaryOp, BinderX, BitwiseOp, Dt, FieldOpr, FunX, ImplPath, + InequalityOp, IntRange, PathX, Primitive, Quant, Typ, UnaryOpr, VarBinder, VarBinderX, + VarIdent, VarIdentDisambiguate, VariantCheck, + }, + ast_util::int_range_from_type, +}; +use vir::{ + ast::{ + ArithOp, AutospecUsage, CallTarget, CallTargetKind, Constant, Expr, ExprX, Mode, + SpannedTyped, TypX, + }, + ast_util::{bitwidth_from_type, is_integer_type_signed}, +}; + +use crate::TypedAttribute; + +use acvm::{AcirField, FieldElement}; +use noirc_frontend::signed_field::SignedField; +use num_bigint::{BigInt, ToBigInt}; // Replace with the actual path to SignedField + +pub fn signed_field_from_bigint_wrapping(value: BigInt) -> SignedField { + let modulus = FieldElement::modulus().to_bigint().unwrap(); + + // Wrap value to the positive modulus range + let wrapped = ((&value % &modulus) + &modulus) % &modulus; + + // Convert the reduced BigInt into FieldElement + let wrapped_biguint = wrapped.to_biguint().unwrap(); + let bytes = wrapped_biguint.to_bytes_be(); + let field = FieldElement::from_be_bytes_reduce(&bytes); + // Fields are always positive + let is_negative = false; + SignedField::new(field, is_negative) +} + +pub(crate) fn convert_typed_attribute_to_vir_attribute( + typed_attribute: TypedAttribute, + state: &State, +) -> Attribute { + match typed_attribute { + TypedAttribute::Ghost => Attribute::Ghost, + TypedAttribute::Requires(ann_expr) => { + Attribute::Requires(ann_expr_to_vir_expr(ann_expr, state)) + } + TypedAttribute::Ensures(ann_expr) => { + Attribute::Ensures(ann_expr_to_vir_expr(ann_expr, state)) + } + } +} + +pub(crate) fn ann_expr_to_vir_expr(ann_expr: SpannedTypedExpr, state: &State) -> Expr { + let mode = Mode::Spec; + cata(ann_expr, &|(loc, typ), expr| -> Arc> { + // Helper to construct a standard SpannedTyped expression. + // It captures `loc` from the outer scope. + let make_expr = |exprx: ExprX, vir_type: Typ, span_msg: String| -> Expr { + SpannedTyped::new(&build_span_no_id(span_msg, Some(loc)), &vir_type, exprx) + }; + match expr { + ExprF::Literal { value } => { + let (exprx, span_msg) = match value { + formal_verification::ast::Literal::Bool(val) => { + (ExprX::Const(Constant::Bool(val)), format!("Const boolean {}", val)) + } + formal_verification::ast::Literal::Int(big_int) => ( + numeric_const_to_vir_exprx( + &signed_field_from_bigint_wrapping(big_int.clone()), + &typ, + ), + format!("Int literal {}", big_int), + ), + }; + make_expr(exprx, ast_type_to_vir_type(&typ), span_msg) + } + ExprF::Variable(Variable { name, id, path: _ }) => { + let is_global = state.global_constants.iter().any(|(_, (gn, _, _))| *gn == name); + let span_msg = format!("Var {}", name); + + // Handle the simpler global case first and return early. + if is_global { + let exprx = ExprX::ConstVar( + Arc::new(FunX { + path: Arc::new(PathX { + krate: None, + segments: Arc::new(vec![Arc::new(name)]), + }), + }), + AutospecUsage::Final, + ); + + // Globals don't have a specific noir DefId, so use build_span_no_id. + return SpannedTyped::new( + &build_span_no_id(span_msg, Some(loc)), + &ast_type_to_vir_type(&typ), + exprx, + ); + } + + // --- Logic below is now only for non-global (local) variables --- + + let disambiguate = if name == FUNC_RETURN_VAR_NAME { + VarIdentDisambiguate::AirLocal + } else { + let rustc_id = id + .expect("Non-return variable must have an ID") + .try_into() + .expect("Failed to convert ast id to usize"); + VarIdentDisambiguate::RustcId(rustc_id) + }; + + let exprx = ExprX::Var(VarIdent(Arc::new(name), disambiguate)); + + // Idiomatically create the span based on whether an ID exists. + let span = if let Some(def_id) = id { + build_span(def_id, span_msg, Some(loc)) + } else { + build_span_no_id(span_msg, Some(loc)) + }; + + SpannedTyped::new(&span, &ast_type_to_vir_type(&typ), exprx) + } + ExprF::FnCall { name, args } => { + if let Some(expr) = + handle_fv_std_call_in_annotations(&name, &args, loc, &typ) + { + return expr; + } + + let exprx = ExprX::Call( + CallTarget::Fun( + CallTargetKind::Static, + function_name_to_vir_fun(name.clone()), + Arc::new(vec![]), + Arc::new(vec![]), + AutospecUsage::Final, + ), + Arc::new(args), + ); + make_expr(exprx, ast_type_to_vir_type(&typ), format!("Function call {}", name)) + } + ExprF::Quantified { quantifier, variables, expr } => { + let quantifier_type = match quantifier { + Quantifier::Forall => Quant { quant: AirQuant::Forall }, + Quantifier::Exists => Quant { quant: AirQuant::Exists }, + }; + let make_binder = |ident: &Variable| -> VarBinder { + let rustc_id = ident + .id + .expect("Quantifier index should have a local id") + .try_into() + .expect("Failed to convert u32 id to usize"); + Arc::new(VarBinderX { + name: VarIdent( + Arc::new(ident.name.clone()), + VarIdentDisambiguate::RustcId(rustc_id), + ), + a: Arc::new(TypX::Int(IntRange::Int)), + }) + }; + let quantifier_vir_indices = Arc::new(variables.iter().map(make_binder).collect()); + + assert!( + matches!(expr.typ.as_ref(), TypX::Bool), + "All quantifier bodies must be of type bool" + ); + + let exprx = ExprX::Quant(quantifier_type, quantifier_vir_indices, expr); + make_expr(exprx, Arc::new(TypX::Bool), format!("Quantifier {}", quantifier)) + } + ExprF::Parenthesised { expr } => expr, + ExprF::UnaryOp { op, expr } => { + let (exprx, span_msg) = match op { + formal_verification::ast::UnaryOp::Not => { + if matches!(typ, noirc_frontend::monomorphization::ast::Type::Bool) { + ( + ExprX::Unary(vir::ast::UnaryOp::Not, expr), + "Logical Not op".to_string(), + ) + } else { + ( + ExprX::Unary( + vir::ast::UnaryOp::BitNot(get_bit_not_bitwidth(&typ)), + expr, + ), + "BitNot expr".to_string(), + ) + } + } + formal_verification::ast::UnaryOp::Dereference => { + // If we have Dereference(Expr), Verus treats them as if it is only Expr. + // Also the expr type gets trimmed from the reference "decoration". + // Therefore we will do the same and only change the type of the expression. + let deref_expr = SpannedTyped::new( + &build_span_no_id( + format!("Dereference expression with type {}", typ), + Some(loc), + ), + &ast_type_to_vir_type(&typ), + expr.x.clone(), // Can not move out of Arc + ); + + return deref_expr; + } + }; + make_expr(exprx, ast_type_to_vir_type(&typ), span_msg) + } + ExprF::BinaryOp { op, expr_left, expr_right } => { + let lhs_type = expr_left.typ.clone(); + let is_lhs_bool = matches!(lhs_type.as_ref(), TypX::Bool); + let bool_or_bitwise = |bool_op, bitwise_op| { + if is_lhs_bool { bool_op } else { VirBinaryOp::Bitwise(bitwise_op, mode) } + }; + + let vir_binary_op = match op { + BinaryOp::Mul => VirBinaryOp::Arith(ArithOp::Mul, mode), + BinaryOp::Div => VirBinaryOp::Arith(ArithOp::EuclideanDiv, mode), + BinaryOp::Mod => VirBinaryOp::Arith(ArithOp::EuclideanMod, mode), + BinaryOp::Add => VirBinaryOp::Arith(ArithOp::Add, mode), + BinaryOp::Sub => VirBinaryOp::Arith(ArithOp::Sub, mode), + BinaryOp::ShiftLeft => VirBinaryOp::Bitwise( + BitwiseOp::Shl( + bitwidth_from_type(&lhs_type) + .expect("Bitwise operation with non int type"), + is_integer_type_signed(&lhs_type), + ), + mode, + ), + BinaryOp::ShiftRight => VirBinaryOp::Bitwise( + BitwiseOp::Shr( + bitwidth_from_type(&lhs_type) + .expect("Bitwise operation with non int type"), + ), + mode, + ), + BinaryOp::Eq => VirBinaryOp::Eq(mode), + BinaryOp::Neq => VirBinaryOp::Ne, + BinaryOp::Lt => VirBinaryOp::Inequality(InequalityOp::Lt), + BinaryOp::Le => VirBinaryOp::Inequality(InequalityOp::Le), + BinaryOp::Gt => VirBinaryOp::Inequality(InequalityOp::Gt), + BinaryOp::Ge => VirBinaryOp::Inequality(InequalityOp::Ge), + BinaryOp::Implies => VirBinaryOp::Implies, + BinaryOp::And => bool_or_bitwise(VirBinaryOp::And, BitwiseOp::BitAnd), + BinaryOp::Or => bool_or_bitwise(VirBinaryOp::Or, BitwiseOp::BitOr), + BinaryOp::Xor => bool_or_bitwise(VirBinaryOp::Xor, BitwiseOp::BitXor), + }; + + let binary_op_type = ast_type_to_vir_type(&typ); + let exprx = ExprX::Binary(vir_binary_op, expr_left, expr_right); + + let vir_binary_expr = + make_expr(exprx, binary_op_type, "Binary op expression".to_string()); + + if is_type_field(&typ) && op.is_arithmetic() { + // Wrap expression with `% Field::modulus()` if the expression type is Field + wrap_with_field_modulo(vir_binary_expr, mode) + } else { + vir_binary_expr + } + } + ExprF::TupleAccess { expr, index } => { + let TypX::Datatype(Dt::Tuple(tuple_len), _, _) = expr.typ.as_ref() else { + unreachable!("Unexpected type for tuple access: {:#?}", expr); + }; + + let exprx = ExprX::UnaryOpr( + UnaryOpr::Field(FieldOpr { + datatype: Dt::Tuple(*tuple_len), + variant: Arc::new(format!("tuple%{}", tuple_len)), + field: Arc::new(index.to_string()), + get_variant: false, + check: VariantCheck::None, + }), + expr, + ); + + make_expr(exprx, ast_type_to_vir_type(&typ), format!("Tuple access at {}", index)) + } + ExprF::Index { expr, index } => { + let element_type = ast_type_to_vir_type(&typ); + + // Ensure we're indexing into a proper array with a const length + let array_type = match expr.typ.as_ref() { + TypX::Primitive(Primitive::Array, inner) => inner, + _ => unreachable!("Arrays must be of type Primitive"), + }; + + let array_len = match array_type[1].as_ref() { + TypX::ConstInt(len) => len, + _ => unreachable!("Arrays must have a constant length"), + }; + + let array_len_type = ast_const_to_vir_type_const( + array_len.try_into().expect("Failed to convert u32 to usize"), + ); + + // Build types for the vstd::array::spec_index function + let vstd_krate = Some(Arc::new("vstd".to_string())); + let element_and_len = Arc::new(vec![element_type.clone(), array_len_type.clone()]); + let array_typ = + Arc::new(TypX::Primitive(Primitive::Array, element_and_len.clone())); + let typs_for_call = Arc::new(vec![array_typ.clone(), element_type.clone()]); + + // Define the call target and trait impl paths + let make_path = |segments: Vec<&str>| { + Arc::new(PathX { + krate: vstd_krate.clone(), + segments: Arc::new( + segments.into_iter().map(|s| Arc::new(s.to_string())).collect(), + ), + }) + }; + + let call_target = CallTarget::Fun( + CallTargetKind::DynamicResolved { + resolved: Arc::new(FunX { + path: make_path(vec!["array", "impl&%2", "spec_index"]), + }), + typs: array_type.clone(), + impl_paths: Arc::new(vec![]), + is_trait_default: false, + }, + Arc::new(FunX { + path: make_path(vec!["array", "ArrayAdditionalSpecFns", "spec_index"]), + }), + typs_for_call.clone(), + Arc::new(vec![ + ImplPath::TraitImplPath(make_path(vec!["array", "impl&%0"])), + ImplPath::TraitImplPath(make_path(vec!["array", "impl&%2"])), + ]), + AutospecUsage::IfMarked, + ); + + let vir_exprx = ExprX::Call(call_target, Arc::new(vec![expr.clone(), index])); + + make_expr(vir_exprx, element_type, "Array indexing expression".to_string()) + } + ExprF::Cast { expr: castee, target } => { + let target_type = ast_type_to_vir_type(&target); + // The following unwrap is safe because the semantic analysis of + // the compiler should guarantee correctly typed expressions. + let target_int_range = + int_range_from_type(&target_type).expect("Can not cast to a non integer type"); + + let exprx = ExprX::Unary( + vir::ast::UnaryOp::Clip { + range: target_int_range, + truncate: false, // We are not truncating because Verus doesn't truncate casts + }, + castee, + ); + + SpannedTyped::new( + &build_span_no_id( + format!("Cast expression to target type {}", target), + Some(loc), + ), + &target_type, + exprx, + ) + } + ExprF::Tuple { exprs } => { + let tuple_length = exprs.len(); + + let tuple_exprx = ExprX::Ctor( + Dt::Tuple(tuple_length), + Arc::new(format!("tuple%{tuple_length}")), + Arc::new( + exprs + .into_iter() + .enumerate() + .map(|(index, tuple_expr)| { + Arc::new(BinderX { + name: Arc::new(index.to_string()), + a: tuple_expr, + }) + }) + .collect(), + ), + None, + ); + + SpannedTyped::new( + &build_span_no_id(format!("Tuple constructor expression"), Some(loc)), + &ast_type_to_vir_type(&typ), + tuple_exprx, + ) + } + ExprF::Array { exprs } => { + let exprx = ExprX::ArrayLiteral(Arc::new(exprs)); + SpannedTyped::new( + &build_span_no_id(format!("Array literal expression"), Some(loc)), + &ast_type_to_vir_type(&typ), + exprx, + ) + } + ExprF::StructureAccess { .. } => { + // All expressions of type StructureAccess have been converted to TupleAccess + unreachable!() + } + } + }) +} diff --git a/compiler/noirc_evaluator/src/vir/mod.rs b/compiler/noirc_evaluator/src/vir/mod.rs index 648a317dfc1..1b70916c195 100644 --- a/compiler/noirc_evaluator/src/vir/mod.rs +++ b/compiler/noirc_evaluator/src/vir/mod.rs @@ -1,12 +1,25 @@ -use noirc_frontend::monomorphization::ast::Program; +use noirc_frontend::monomorphization::ast::{FuncId, Program}; use vir::ast::Krate; +use vir_gen::Attribute; use vir_gen::{BuildingKrateError, build_krate}; -use crate::vir::opt_passes::monomorph_ast_optimization_passes; -pub mod vir_gen; +use crate::vir::{ + opt_passes::monomorph_ast_optimization_passes, vir_gen::build_krate_with_ready_annotations, +}; pub mod opt_passes; +pub mod vir_gen; pub fn create_verus_vir(program: Program) -> Result { let program = monomorph_ast_optimization_passes(program); build_krate(program) } + +/// Same as `create_verus_vir` but expects the FV attributes +/// to be already transformed into VIR form. +pub fn create_verus_vir_with_ready_annotations( + program: Program, + fv_annotations: Vec<(FuncId, Vec)>, +) -> Result { + let program = monomorph_ast_optimization_passes(program); + build_krate_with_ready_annotations(program, fv_annotations) +} diff --git a/compiler/noirc_evaluator/src/vir/vir_gen/expr_to_vir/expr.rs b/compiler/noirc_evaluator/src/vir/vir_gen/expr_to_vir/expr.rs index ddccf78197e..e02b1806bb3 100644 --- a/compiler/noirc_evaluator/src/vir/vir_gen/expr_to_vir/expr.rs +++ b/compiler/noirc_evaluator/src/vir/vir_gen/expr_to_vir/expr.rs @@ -229,7 +229,7 @@ fn ast_literal_to_vir_expr( expr } -fn numeric_const_to_vir_exprx(signed_field: &SignedField, ast_type: &Type) -> ExprX { +pub fn numeric_const_to_vir_exprx(signed_field: &SignedField, ast_type: &Type) -> ExprX { // If we have a negative Field const we want to wrap it around the finite field modulus let (const_big_uint, big_int_sign): (BigUint, _) = { match ast_type { @@ -997,7 +997,7 @@ fn build_var_ident(name: String, id: u32) -> VarIdent { ) } -fn function_name_to_vir_fun(func_name: String) -> Fun { +pub fn function_name_to_vir_fun(func_name: String) -> Fun { Arc::new(FunX { path: Arc::new(PathX { krate: None, segments: Arc::new(vec![Arc::new(func_name)]) }), }) @@ -1121,7 +1121,7 @@ pub fn ast_definition_to_id(definition: &Definition) -> Option { /// For the Noir Field type we have to wrap all arithmetic instructions /// with a Euclidean modulo `p` operation where `p` is the modulus of /// the Noir Field. -fn wrap_with_field_modulo(dividend: Expr, mode: Mode) -> Expr { +pub fn wrap_with_field_modulo(dividend: Expr, mode: Mode) -> Expr { let expr_span = dividend.span.clone(); let expr_type = dividend.typ.clone(); diff --git a/compiler/noirc_evaluator/src/vir/vir_gen/expr_to_vir/std_functions.rs b/compiler/noirc_evaluator/src/vir/vir_gen/expr_to_vir/std_functions.rs index dfe2af9dd64..3f33f73584c 100644 --- a/compiler/noirc_evaluator/src/vir/vir_gen/expr_to_vir/std_functions.rs +++ b/compiler/noirc_evaluator/src/vir/vir_gen/expr_to_vir/std_functions.rs @@ -1,5 +1,6 @@ use std::collections::BTreeMap; +use noirc_errors::Location; use noirc_frontend::monomorphization::ast::{Call, Expression, GlobalId, Type}; use vir::ast::{Expr, ExprX, Mode, SpannedTyped}; @@ -17,7 +18,7 @@ use crate::vir::vir_gen::{ /// The function `assume()` from `fv_std_lib` static ASSUME: &str = "assume"; /// The function `old()` from `fv_std_lib` -static OLD: &str = "old"; +pub static OLD: &str = "old"; /// Handles function calls from the `fv_std` library and converts them to special VIR expressions. pub fn handle_fv_std_call( @@ -30,51 +31,68 @@ pub fn handle_fv_std_call( _ => return None, }; - match ident.name.as_str() { + // Convert Noir AST exprs into VIR exprs + let arguments = call_expr + .arguments + .iter() + .map(|arg| ast_expr_to_vir_expr(arg, Mode::Spec, globals)) + .collect::>(); + + handle_fv_std_inner(&ident.name, arguments, call_expr.location, &call_expr.return_type) +} + +/// Handles function calls from the `fv_std` library and converts them to special VIR expressions. +pub fn handle_fv_std_call_in_annotations( + function_name: &str, + arguments: &Vec, + location: Location, + return_typ: &Type, +) -> Option { + handle_fv_std_inner(function_name, arguments.clone(), location, return_typ) +} + +fn handle_fv_std_inner( + function_name: &str, + arguments: Vec, + location: Location, + return_typ: &Type, +) -> Option { + match function_name { // Special logic for handling the function `assume` from our Noir `fv_std` library s if s == ASSUME => { assert!( - call_expr.arguments.len() == 1, + arguments.len() == 1, "Expected function `assume` from `noir_fv_std` to have exactly one argument" ); - let condition_expr = ast_expr_to_vir_expr(&call_expr.arguments[0], Mode::Spec, globals); - let exprx = ExprX::AssertAssume { is_assume: true, expr: condition_expr }; + let condition_expr = arguments.into_iter().next().unwrap(); + let exprx = ExprX::AssertAssume { is_assume: true, expr: condition_expr }; let assume_expr = SpannedTyped::new( - &build_span_no_id( - format!("Assume {} is true", call_expr.arguments[0]), - Some(call_expr.location), - ), + &build_span_no_id("Assume expression".to_string(), Some(location)), &make_unit_vir_type(), exprx, ); - Some(wrap_with_ghost_block(assume_expr, Some(call_expr.location))) + Some(wrap_with_ghost_block(assume_expr, Some(location))) } // Special logic for handling the function `old` from our Noir `fv_std` library s if s == OLD => { assert!( - call_expr.arguments.len() == 1, + arguments.len() == 1, "Expected function `old` from `noir_fv_std` to have exactly one argument" ); - let Expression::Ident(var_ident) = &call_expr.arguments[0] else { + let ExprX::Var(vir_ident) = &arguments[0].x else { return None; }; - let ident_id = - ast_definition_to_id(&var_ident.definition).expect("Definition doesn't have an id"); - let vir_ident = ast_ident_to_vir_var_ident(var_ident, ident_id); - let exprx = ExprX::VarAt(vir_ident, vir::ast::VarAt::Pre); + let exprx = ExprX::VarAt(vir_ident.clone(), vir::ast::VarAt::Pre); Some(SpannedTyped::new( - &build_span_no_id( - format!("old({})", call_expr.arguments[0]), - Some(call_expr.location), - ), - &ast_type_to_vir_type(&call_expr.return_type), + &build_span_no_id(format!("old({})", vir_ident.0), Some(location)), + &ast_type_to_vir_type(return_typ), exprx, )) } diff --git a/compiler/noirc_evaluator/src/vir/vir_gen/expr_to_vir/types.rs b/compiler/noirc_evaluator/src/vir/vir_gen/expr_to_vir/types.rs index 11ba9930ec7..13794f1f6ef 100644 --- a/compiler/noirc_evaluator/src/vir/vir_gen/expr_to_vir/types.rs +++ b/compiler/noirc_evaluator/src/vir/vir_gen/expr_to_vir/types.rs @@ -71,7 +71,7 @@ fn get_integer_type_bitwidth(integer_type: &Type) -> IntegerTypeBitwidth { /// Similar to `get_integer_type_bitwidth` but we have a different logic /// for the types Field and Signed integer. /// Will `panic` if the type is not an integer. -pub(crate) fn get_bit_not_bitwidth(integer_type: &Type) -> Option { +pub fn get_bit_not_bitwidth(integer_type: &Type) -> Option { match integer_type { Type::Field | Type::Integer(Signedness::Signed, _) => None, Type::Integer(Signedness::Unsigned, _) => Some(get_integer_type_bitwidth(integer_type)), diff --git a/compiler/noirc_evaluator/src/vir/vir_gen/function.rs b/compiler/noirc_evaluator/src/vir/vir_gen/function.rs index 60d3b634cef..10734c950ad 100644 --- a/compiler/noirc_evaluator/src/vir/vir_gen/function.rs +++ b/compiler/noirc_evaluator/src/vir/vir_gen/function.rs @@ -7,14 +7,17 @@ use super::{ BuildingKrateError, attribute::{func_ensures_to_vir_expr, func_requires_to_vir_expr}, }; +use crate::vir::vir_gen::Attribute; use noirc_errors::Location; -use noirc_frontend::monomorphization::ast::{Expression, Function, GlobalId, MonomorphizedFvAttribute, Type}; +use noirc_frontend::monomorphization::ast::{ + Expression, Function, GlobalId, MonomorphizedFvAttribute, Type, +}; use std::collections::BTreeMap; use std::sync::Arc; use vir::ast::{ - BodyVisibility, Fun, FunX, FunctionAttrs, FunctionAttrsX, FunctionKind, FunctionX, ItemKind, - Mode, Module, Opaqueness, Param, ParamX, Params, PathX, VarIdent, VarIdentDisambiguate, - Visibility, + BodyVisibility, Exprs, Fun, FunX, FunctionAttrs, FunctionAttrsX, FunctionKind, FunctionX, + ItemKind, Mode, Module, Opaqueness, Param, ParamX, Params, PathX, VarIdent, + VarIdentDisambiguate, Visibility, }; use vir::def::Spanned; @@ -154,3 +157,69 @@ pub fn build_funx( Ok(funx) } + +// Converts the given Monomorphized AST function into a VIR function. +/// Same as `build_funx` but expects the FV attributes +/// to be already transformed into VIR form. +pub fn build_funx_with_ready_annotations( + function: &Function, + current_module: &Module, + globals: &BTreeMap, + annotations: Vec, +) -> Result { + let mut is_ghost = false; + let mut requires_annotations_inner = vec![]; + let mut ensures_annotations_inner = vec![]; + + for a in annotations.into_iter() { + match a { + Attribute::Ghost => { + is_ghost = true; + } + Attribute::Ensures(expr) => ensures_annotations_inner.push(expr), + Attribute::Requires(expr) => requires_annotations_inner.push(expr), + } + } + + let mode = get_function_mode(is_ghost); + + let function_params = get_function_params(function, mode)?; + let function_return_param = get_function_return_param(function, mode)?; + + let funx = FunctionX { + name: function_into_funx_name(function), + proxy: None, // Only needed for external fn specifications which we currently don't support + kind: FunctionKind::Static, // Monomorphized AST has only static functions + visibility: Visibility { + restricted_to: None, // `None` is for functions with public visibility + }, // Categorization for public/private visibility doesn't exist in the Mon. AST + body_visibility: BodyVisibility::Visibility(Visibility { + restricted_to: None, // We currently support only fully visible ghost functions + }), + opaqueness: Opaqueness::Revealed { + visibility: Visibility { restricted_to: None }, // We currently don't support opaqueness control + }, + owning_module: Some(current_module.x.path.clone()), // The module in which this function is located. + mode, + typ_params: Arc::new(Vec::new()), // There are no generics in Monomorphized AST + typ_bounds: Arc::new(Vec::new()), // There are no generics in Monomorphized AST + params: function_params, + ret: function_return_param, + ens_has_return: !is_function_return_void(function), + require: Arc::new(requires_annotations_inner), + ensure: Arc::new(ensures_annotations_inner), + returns: None, // We don't support the special clause called `return` + decrease: Arc::new(vec![]), // Annotation for recursive functions. We currently don't support it + decrease_when: None, // Annotation for recursive functions. We currently don't support it + decrease_by: None, // Annotation for recursive functions. We currently don't support it + fndef_axioms: None, // We currently don't support this feature + mask_spec: None, // We currently don't support this feature + unwind_spec: None, // To be able to use functions from Verus std we need None on unwinding + item_kind: ItemKind::Function, + attrs: build_default_funx_attrs(function.parameters.is_empty(), !function.unconstrained), + body: Some(func_body_to_vir_expr(function, mode, globals)), + extra_dependencies: Vec::new(), + }; + + Ok(funx) +} diff --git a/compiler/noirc_evaluator/src/vir/vir_gen/mod.rs b/compiler/noirc_evaluator/src/vir/vir_gen/mod.rs index 7731df511d9..1b52fa1c91f 100644 --- a/compiler/noirc_evaluator/src/vir/vir_gen/mod.rs +++ b/compiler/noirc_evaluator/src/vir/vir_gen/mod.rs @@ -5,29 +5,39 @@ pub mod globals; use function::build_funx; use noirc_errors::Location; -use noirc_frontend::monomorphization::ast::Program; +use noirc_frontend::monomorphization::ast::{FuncId, Program}; use serde::{Deserialize, Serialize}; -use std::{fmt::Display, sync::Arc}; +use std::{collections::HashMap, fmt::Display, sync::Arc}; use vir::{ - ast::{Krate, KrateX, ModuleX, PathX}, + ast::{Expr, Krate, KrateX, ModuleX, PathX}, def::Spanned, messages::Span, }; -use crate::vir::vir_gen::{expr_to_vir::expression_location, globals::build_global_const_x}; +use crate::vir::vir_gen::{ + expr_to_vir::expression_location, function::build_funx_with_ready_annotations, + globals::build_global_const_x, +}; + +#[derive(Debug, Clone)] +pub enum Attribute { + Ghost, + Ensures(Expr), + Requires(Expr), +} -fn encode_span_to_string(location: Location) -> String { +pub fn encode_span_to_string(location: Location) -> String { let stringified_span: String = format!("{}, {}", location.span.start(), location.span.end()); let stringified_file_id: String = format!("{}", location.file.as_usize()); format!("({}, {})", stringified_span, stringified_file_id) } -fn build_span_no_id(debug_string: String, span: Option) -> Span { +pub fn build_span_no_id(debug_string: String, span: Option) -> Span { build_span(0, debug_string, span) } -fn build_span(id: u32, debug_string: String, span: Option) -> Span { +pub fn build_span(id: u32, debug_string: String, span: Option) -> Span { let encoded_span = span.map(encode_span_to_string).unwrap_or_default(); Span { raw_span: Arc::new(()), // Currently unusable because of hard to resolve bug @@ -113,3 +123,75 @@ pub fn build_krate(program: Program) -> Result { Ok(Arc::new(vir)) } + +/// Same as `build_krate` but expects the FV attributes +/// to be already transformed into VIR form. +pub fn build_krate_with_ready_annotations( + program: Program, + fv_annotations: Vec<(FuncId, Vec)>, +) -> Result { + let mut vir = KrateX { + functions: Vec::new(), + reveal_groups: Vec::new(), + datatypes: Vec::new(), + traits: Vec::new(), + trait_impls: Vec::new(), + assoc_type_impls: Vec::new(), + modules: Vec::new(), + external_fns: Vec::new(), + external_types: Vec::new(), + path_as_rust_names: vir::ast_util::get_path_as_rust_names_for_krate(&Arc::new( + vir::def::VERUSLIB.to_string(), + )), + arch: vir::ast::Arch { word_bits: vir::ast::ArchWordBits::Either32Or64 }, + }; + + // There are no modules in the Noir's monomorphized AST. + // Therefore we are creating a default module and all functions will be a part of it. + let module = Spanned::new( + build_span_no_id(String::from("module"), None), + ModuleX { + path: Arc::new(PathX { + krate: None, + segments: Arc::new(vec![Arc::new(String::from("Mon. AST"))]), + }), + reveals: None, + }, + ); + + // Insert global constants as functions. This is how Verus processes constants + vir.functions.extend(program.globals.iter().map( + |(global_id, (name, ast_type, expression))| { + let global_const_x = + build_global_const_x(name, ast_type, expression, &module, &program.globals); + Spanned::new( + build_span( + global_id.0, + format!("Global const {} = {}", name, expression), + expression_location(expression), + ), + global_const_x, + ) + }, + )); + + let mut annotations_map: HashMap> = fv_annotations.into_iter().collect(); + + for function in &program.functions { + let attrs = annotations_map.remove(&function.id).unwrap_or_else(Vec::new); + let func_x = build_funx_with_ready_annotations(function, &module, &program.globals, attrs)?; + let function = Spanned::new( + build_span( + function.id.0, + format!("Function({}) with name {}", function.id.0, function.name), + None, + ), + func_x, + ); + vir.functions.push(function); + } + + vir.modules.push(module); + + Ok(Arc::new(vir)) +} diff --git a/compiler/noirc_frontend/src/lexer/lexer.rs b/compiler/noirc_frontend/src/lexer/lexer.rs index cab99e5514d..1dcb2af5840 100644 --- a/compiler/noirc_frontend/src/lexer/lexer.rs +++ b/compiler/noirc_frontend/src/lexer/lexer.rs @@ -73,6 +73,10 @@ impl<'a> Lexer<'a> { self } + pub fn set_skip_whitespaces_flag(&mut self, flag: bool) { + self.skip_whitespaces = flag; + } + /// Iterates the cursor and returns the char at the new cursor position fn next_char(&mut self) -> Option { let (position, ch) = self.chars.next()?; diff --git a/compiler/noirc_frontend/src/monomorphization/mod.rs b/compiler/noirc_frontend/src/monomorphization/mod.rs index f00eba151a9..1b56cb9d5d1 100644 --- a/compiler/noirc_frontend/src/monomorphization/mod.rs +++ b/compiler/noirc_frontend/src/monomorphization/mod.rs @@ -52,7 +52,7 @@ use self::{ /// and its value is the body expression of the function to which the `ensures` /// attribute is attached to. /// The leading `%` makes it an illegal identifier which ensures that it won't -/// clash with existing identifiers. +/// clash with existing identifiers. pub const FUNC_RETURN_VAR_NAME: &str = "%return"; pub mod ast; @@ -71,7 +71,7 @@ struct LambdaContext { /// /// This struct holds the FIFO queue of functions to monomorphize, which is added to /// whenever a new (function, type) combination is encountered. -pub(super) struct Monomorphizer<'interner> { +pub struct Monomorphizer<'interner> { /// Functions are keyed by their unique ID, whether they're unconstrained, their expected type, /// and any generics they have so that we can monomorphize a new version of the function for each type. /// @@ -83,16 +83,16 @@ pub(super) struct Monomorphizer<'interner> { /// duplicated during monomorphization. Doing so would allow them to be used polymorphically /// but would also cause them to be re-evaluated which is a performance trap that would /// confuse users. - locals: HashMap, + pub locals: HashMap, /// Globals are keyed by their unique ID because they are never duplicated during monomorphization. globals: HashMap, - finished_globals: HashMap, + pub finished_globals: HashMap, /// Queue of functions to monomorphize next each item in the queue is a tuple of: /// (old_id, new_monomorphized_id, any type bindings to apply, the trait method if old_id is from a trait impl, is_unconstrained, location) - queue: VecDeque<( + pub queue: VecDeque<( node_interner::FuncId, FuncId, TypeBindings, @@ -103,10 +103,10 @@ pub(super) struct Monomorphizer<'interner> { /// When a function finishes being monomorphized, the monomorphized ast::Function is /// stored here along with its FuncId. - finished_functions: BTreeMap, + pub finished_functions: BTreeMap, /// Used to reference existing definitions in the HIR - interner: &'interner mut NodeInterner, + pub interner: &'interner mut NodeInterner, lambda_envs_stack: Vec, @@ -117,11 +117,11 @@ pub(super) struct Monomorphizer<'interner> { is_range_loop: bool, - return_location: Option, + pub return_location: Option, - debug_type_tracker: DebugTypeTracker, + pub debug_type_tracker: DebugTypeTracker, - in_unconstrained_function: bool, + pub in_unconstrained_function: bool, } /// Using nested HashMaps here lets us avoid cloning HirTypes when calling .get() @@ -215,7 +215,7 @@ pub fn monomorphize_debug( } impl<'interner> Monomorphizer<'interner> { - pub(crate) fn new( + pub fn new( interner: &'interner mut NodeInterner, debug_type_tracker: DebugTypeTracker, ) -> Self { @@ -343,7 +343,7 @@ impl<'interner> Monomorphizer<'interner> { .insert(turbofish_generics, new_id); } - fn compile_main( + pub fn compile_main( &mut self, main_id: node_interner::FuncId, ) -> Result { @@ -365,7 +365,7 @@ impl<'interner> Monomorphizer<'interner> { Ok(main_meta.function_signature()) } - fn function( + pub fn function( &mut self, f: node_interner::FuncId, id: FuncId, @@ -1892,7 +1892,7 @@ impl<'interner> Monomorphizer<'interner> { Expression::Literal(Literal::Slice(arr_literal)) } - fn queue_function( + pub fn queue_function( &mut self, id: node_interner::FuncId, expr_id: node_interner::ExprId, diff --git a/compiler/noirc_frontend/src/parser/parser.rs b/compiler/noirc_frontend/src/parser/parser.rs index e97f197afe0..1a1d4708830 100644 --- a/compiler/noirc_frontend/src/parser/parser.rs +++ b/compiler/noirc_frontend/src/parser/parser.rs @@ -475,6 +475,19 @@ impl<'a> Parser<'a> { self.at(Token::Keyword(keyword)) } + fn at_whitespace(&self) -> bool { + matches!(self.token.token(), Token::Whitespace(_)) + } + + fn set_lexer_skip_whitespaces_flag(&mut self, flag: bool) { + match &mut self.tokens { + TokenStream::Lexer(lexer) => { + lexer.set_skip_whitespaces_flag(flag); + } + _ => {} + }; + } + fn next_is(&self, token: Token) -> bool { self.next_token.token() == &token } diff --git a/compiler/noirc_frontend/src/parser/parser/attributes.rs b/compiler/noirc_frontend/src/parser/parser/attributes.rs index 2166aa128fb..233140a0527 100644 --- a/compiler/noirc_frontend/src/parser/parser/attributes.rs +++ b/compiler/noirc_frontend/src/parser/parser/attributes.rs @@ -7,6 +7,7 @@ use crate::lexer::fv_attributes::{ }; use crate::parser::ParserErrorReason; use crate::parser::labels::ParsingRuleLabel; +use crate::parser::parser::TokenStream; use crate::token::{ Attribute, FunctionAttribute, FunctionAttributeKind, FuzzingScope, MetaAttribute, MetaAttributeName, SecondaryAttribute, SecondaryAttributeKind, TestScope, Token, @@ -114,6 +115,8 @@ impl Parser<'_> { let mut brackets_count = 1; // 1 because of the starting `#[` + self.set_lexer_skip_whitespaces_flag(false); + while !self.at_eof() { if self.at(Token::LeftBracket) { brackets_count += 1; @@ -129,6 +132,11 @@ impl Parser<'_> { self.bump(); } + self.set_lexer_skip_whitespaces_flag(true); + while self.at_whitespace() { + self.bump(); + } + let location = self.location_since(start_location); let kind = SecondaryAttributeKind::Tag(contents); let attr = SecondaryAttribute { kind, location }; diff --git a/flake.lock b/flake.lock index 46fba19bf79..5727fd6914e 100644 --- a/flake.lock +++ b/flake.lock @@ -8,11 +8,11 @@ "rust-analyzer-src": "rust-analyzer-src" }, "locked": { - "lastModified": 1748846362, - "narHash": "sha256-D2LUpaxJFrkahPE1U6S01u1ZY9Wsr82jOSjAVoIZ/hs=", + "lastModified": 1753339339, + "narHash": "sha256-r9Frae3VnbgKrWWQcV6WEykm6PxfPHVrxdOqgyt1VcU=", "owner": "nix-community", "repo": "fenix", - "rev": "6a5e421c05cb29bffecdb3a1c3c80cec22d62efd", + "rev": "af1c3d7dd242ebf50ac75665d5c44af79730b491", "type": "github" }, "original": { @@ -26,11 +26,11 @@ "nixpkgs-lib": "nixpkgs-lib" }, "locked": { - "lastModified": 1748821116, - "narHash": "sha256-F82+gS044J1APL0n4hH50GYdPRv/5JWm34oCJYmVKdE=", + "lastModified": 1753121425, + "narHash": "sha256-TVcTNvOeWWk1DXljFxVRp+E0tzG1LhrVjOGGoMHuXio=", "owner": "hercules-ci", "repo": "flake-parts", - "rev": "49f0870db23e8c1ca0b5259734a02cd9e1e371a1", + "rev": "644e0fc48951a860279da645ba77fe4a6e814c5e", "type": "github" }, "original": { @@ -41,11 +41,11 @@ }, "nixpkgs": { "locked": { - "lastModified": 1748693115, - "narHash": "sha256-StSrWhklmDuXT93yc3GrTlb0cKSS0agTAxMGjLKAsY8=", + "lastModified": 1753250450, + "narHash": "sha256-i+CQV2rPmP8wHxj0aq4siYyohHwVlsh40kV89f3nw1s=", "owner": "NixOS", "repo": "nixpkgs", - "rev": "910796cabe436259a29a72e8d3f5e180fc6dfacc", + "rev": "fc02ee70efb805d3b2865908a13ddd4474557ecf", "type": "github" }, "original": { @@ -73,11 +73,11 @@ }, "nixpkgs-lib": { "locked": { - "lastModified": 1748740939, - "narHash": "sha256-rQaysilft1aVMwF14xIdGS3sj1yHlI6oKQNBRTF40cc=", + "lastModified": 1751159883, + "narHash": "sha256-urW/Ylk9FIfvXfliA1ywh75yszAbiTEVgpPeinFyVZo=", "owner": "nix-community", "repo": "nixpkgs.lib", - "rev": "656a64127e9d791a334452c6b6606d17539476e2", + "rev": "14a40a1d7fb9afa4739275ac642ed7301a9ba1ab", "type": "github" }, "original": { @@ -98,11 +98,11 @@ "rust-analyzer-src": { "flake": false, "locked": { - "lastModified": 1748695646, - "narHash": "sha256-VwSuuRF4NvAoeHZJRRlX8zAFZ+nZyuiIvmVqBAX0Bcg=", + "lastModified": 1753282007, + "narHash": "sha256-PgTUdSShfGVqZtDJk5noAB1rKdD/MeZ1zq4jY8n9p3c=", "owner": "rust-lang", "repo": "rust-analyzer", - "rev": "2a388d1103450d814a84eda98efe89c01b158343", + "rev": "b5b10fb10facef4d18b4cae8ef22e640ca601255", "type": "github" }, "original": { diff --git a/flake.nix b/flake.nix index 17377bc5b75..b83134451e0 100644 --- a/flake.nix +++ b/flake.nix @@ -47,7 +47,7 @@ { legacyPackages.rustToolchain = with inputs'.fenix.packages; - with latest; + with stable; combine [ cargo clippy diff --git a/rust-toolchain.toml b/rust-toolchain.toml index ed1915d2613..0aaa62c24ab 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -1,5 +1,5 @@ [toolchain] -channel = "1.85.0" +channel = "1.88.0" components = [ "rust-src" ] targets = [ "wasm32-unknown-unknown", "wasm32-wasip1", "aarch64-apple-darwin" ] profile = "default" diff --git a/test_programs/formal_verify_failure/exec_function_in_attribute/Nargo.toml b/test_programs/formal_verify_failure/exec_function_in_attribute/Nargo.toml new file mode 100644 index 00000000000..9b6fc7cdb40 --- /dev/null +++ b/test_programs/formal_verify_failure/exec_function_in_attribute/Nargo.toml @@ -0,0 +1,7 @@ +[package] +name = "exec_function_in_attribute" +type = "bin" +authors = [""] +compiler_version = ">=0.35.0" + +[dependencies] diff --git a/test_programs/formal_verify_failure/exec_function_in_attribute/src/main.nr b/test_programs/formal_verify_failure/exec_function_in_attribute/src/main.nr new file mode 100644 index 00000000000..667d5803c51 --- /dev/null +++ b/test_programs/formal_verify_failure/exec_function_in_attribute/src/main.nr @@ -0,0 +1,13 @@ +#['ensures(result == baz())] +fn main(x: Field, y: pub Field) -> pub u32 { + foo().1 +} + +#['ensures(result.1 == 2)] +fn foo() -> (u32, u32){ + (1, 2) +} + +fn baz() -> u32 { + 2 +} diff --git a/test_programs/formal_verify_failure/fv_attribute_name_resolution_1/src/main.nr b/test_programs/formal_verify_failure/fv_attribute_name_resolution_1/src/main.nr index bca9f6af325..446cc24727e 100644 --- a/test_programs/formal_verify_failure/fv_attribute_name_resolution_1/src/main.nr +++ b/test_programs/formal_verify_failure/fv_attribute_name_resolution_1/src/main.nr @@ -2,7 +2,7 @@ fn main(x: Field, y: pub Field) { assert(x != y); } -#[requires(y > 5)] +#['requires(y > 5)] fn foo(x: Field) -> Field { x + x } diff --git a/test_programs/formal_verify_failure/fv_attribute_name_resolution_2/src/main.nr b/test_programs/formal_verify_failure/fv_attribute_name_resolution_2/src/main.nr index 3bf470570f6..1751d2004d9 100644 --- a/test_programs/formal_verify_failure/fv_attribute_name_resolution_2/src/main.nr +++ b/test_programs/formal_verify_failure/fv_attribute_name_resolution_2/src/main.nr @@ -2,7 +2,7 @@ fn main(x: Field, y: pub Field) { assert(x != y); } -#[requires(result > 5)] // result can be only used in the ensures attribute +#['requires(result > 5)] // result can be only used in the ensures attribute fn foo(x: Field) -> Field { x + x } diff --git a/test_programs/formal_verify_failure/fv_attribute_name_resolution_3/src/main.nr b/test_programs/formal_verify_failure/fv_attribute_name_resolution_3/src/main.nr index c73980635bf..e2e18936cfd 100644 --- a/test_programs/formal_verify_failure/fv_attribute_name_resolution_3/src/main.nr +++ b/test_programs/formal_verify_failure/fv_attribute_name_resolution_3/src/main.nr @@ -2,7 +2,7 @@ fn main(x: Field, y: pub Field) { assert(x != y); } -#[ensures(result > y)] +#['ensures(result > y)] fn foo(x: Field) -> Field { x + x } diff --git a/test_programs/formal_verify_failure/fv_attribute_type_check_1/src/main.nr b/test_programs/formal_verify_failure/fv_attribute_type_check_1/src/main.nr index 1782692eff6..e45f6de79f2 100644 --- a/test_programs/formal_verify_failure/fv_attribute_type_check_1/src/main.nr +++ b/test_programs/formal_verify_failure/fv_attribute_type_check_1/src/main.nr @@ -2,7 +2,7 @@ fn main(x: Field, y: pub Field) { assert(x != y); } -#[requires(x)] +#['requires(x)] fn foo(x: Field) -> Field { x + x } diff --git a/test_programs/formal_verify_failure/fv_attribute_type_check_2/src/main.nr b/test_programs/formal_verify_failure/fv_attribute_type_check_2/src/main.nr index 8885c56169f..2b600bc322b 100644 --- a/test_programs/formal_verify_failure/fv_attribute_type_check_2/src/main.nr +++ b/test_programs/formal_verify_failure/fv_attribute_type_check_2/src/main.nr @@ -2,7 +2,7 @@ fn main(x: Field, y: pub Field) { assert(x != y); } -#[ensures(result)] +#['ensures(result)] fn foo(x: Field) -> Field { x + x } diff --git a/test_programs/formal_verify_failure/fv_attribute_type_check_3/src/main.nr b/test_programs/formal_verify_failure/fv_attribute_type_check_3/src/main.nr index 8a12d54ebc5..e70c2270fca 100644 --- a/test_programs/formal_verify_failure/fv_attribute_type_check_3/src/main.nr +++ b/test_programs/formal_verify_failure/fv_attribute_type_check_3/src/main.nr @@ -2,7 +2,7 @@ fn main(x: Field, y: pub Field) { assert(x != y); } -#[requires(5)] +#['requires(5)] fn foo(x: Field) -> Field { x + x } diff --git a/test_programs/formal_verify_success/array_as_attribute/src/main.nr b/test_programs/formal_verify_success/array_as_attribute/src/main.nr index 3779b9c26b4..93a21246367 100644 --- a/test_programs/formal_verify_success/array_as_attribute/src/main.nr +++ b/test_programs/formal_verify_success/array_as_attribute/src/main.nr @@ -5,22 +5,22 @@ fn main() { let _ = foo4([1, 0, 8, 0, 0]); } -#[requires((x[1] == 1) & (x[0] == 1) & (x[2] == 8))] +#['requires((x[1] == 1) & (x[0] == 1) & (x[2] == 8))] fn foo1(x: [u32; 5]) { assert(x[2] == 8); } -#[requires((x[1] == 1) & (x[0] == 8) & (x[2] == 8))] +#['requires((x[1] == 1) & (x[0] == 8) & (x[2] == 8))] fn foo2(x: [u32; 5]) { assert(x[2] == 8); } -#[requires((x[1] == 8) & (x[0] == 1) & (x[2] == 8))] +#['requires((x[1] == 8) & (x[0] == 1) & (x[2] == 8))] fn foo3(x: [u32; 5]) { assert(x[2] == 8); } -#[requires((x[0] == 1) & (x[2] == 8))] +#['requires((x[0] == 1) & (x[2] == 8))] fn foo4(x: [u32; 5]) { assert(x[2] == 8); } diff --git a/test_programs/formal_verify_success/array_as_result_attr/src/main.nr b/test_programs/formal_verify_success/array_as_result_attr/src/main.nr index 730a6c8abc3..a12faeb2388 100644 --- a/test_programs/formal_verify_success/array_as_result_attr/src/main.nr +++ b/test_programs/formal_verify_success/array_as_result_attr/src/main.nr @@ -1,4 +1,4 @@ -#[ensures((result[0] == x[0]) & (result[1] == x[1]))] +#['ensures((result[0] == x[0]) & (result[1] == x[1]))] fn main(x: [u32; 2]) -> pub [u32; 2] { x } diff --git a/test_programs/formal_verify_success/array_as_result_attr_copy/src/main.nr b/test_programs/formal_verify_success/array_as_result_attr_copy/src/main.nr index fc153a5938d..fce93e63ea4 100644 --- a/test_programs/formal_verify_success/array_as_result_attr_copy/src/main.nr +++ b/test_programs/formal_verify_success/array_as_result_attr_copy/src/main.nr @@ -1,4 +1,4 @@ -#[ensures((result[0] == x[0]) & (result[1] == x[1]))] +#['ensures((result[0] == x[0]) & (result[1] == x[1]))] fn main(x: [u32; 2]) -> pub [u32; 2] { [x[0], x[1]] } diff --git a/test_programs/formal_verify_success/array_as_result_attrs_copies/src/main.nr b/test_programs/formal_verify_success/array_as_result_attrs_copies/src/main.nr index 1fee3a9f756..db8b7c84229 100644 --- a/test_programs/formal_verify_success/array_as_result_attrs_copies/src/main.nr +++ b/test_programs/formal_verify_success/array_as_result_attrs_copies/src/main.nr @@ -1,4 +1,4 @@ -#[ensures((result[0] == x) & (result[1] == y))] +#['ensures((result[0] == x) & (result[1] == y))] fn main(x: u32, y: u32) -> pub [u32; 2] { [x, y] } diff --git a/test_programs/formal_verify_success/array_as_result_const/src/main.nr b/test_programs/formal_verify_success/array_as_result_const/src/main.nr index 4787154b56e..bb61756a445 100644 --- a/test_programs/formal_verify_success/array_as_result_const/src/main.nr +++ b/test_programs/formal_verify_success/array_as_result_const/src/main.nr @@ -1,4 +1,4 @@ -#[ensures((result[0] == 64) & (result[1] == 820))] +#['ensures((result[0] == 64) & (result[1] == 820))] fn main() -> pub [u32; 2] { [64, 820] } diff --git a/test_programs/formal_verify_success/array_as_result_global/src/main.nr b/test_programs/formal_verify_success/array_as_result_global/src/main.nr index 08591ecb092..3acf373328b 100644 --- a/test_programs/formal_verify_success/array_as_result_global/src/main.nr +++ b/test_programs/formal_verify_success/array_as_result_global/src/main.nr @@ -1,4 +1,4 @@ -#[ensures((result[0] == 64))] +#['ensures((result[0] == 64))] fn main() -> pub [u32; 2] { out } diff --git a/test_programs/formal_verify_success/array_copy/src/main.nr b/test_programs/formal_verify_success/array_copy/src/main.nr index 9ddf32280f9..396f84fc364 100644 --- a/test_programs/formal_verify_success/array_copy/src/main.nr +++ b/test_programs/formal_verify_success/array_copy/src/main.nr @@ -1,5 +1,5 @@ // ArrayGet is not yet implemented -#[ensures((result[0] == x[0]) & (result[1] == 1) & (result[2] == x[2]))] +#['ensures((result[0] == x[0]) & (result[1] == 1) & (result[2] == x[2]))] fn main(x: [u8; 3]) -> pub [u8; 3] { [x[0], 1, x[2]] } diff --git a/test_programs/formal_verify_success/array_param_index/Nargo.toml b/test_programs/formal_verify_success/array_param_index/Nargo.toml new file mode 100644 index 00000000000..3785031132b --- /dev/null +++ b/test_programs/formal_verify_success/array_param_index/Nargo.toml @@ -0,0 +1,7 @@ +[package] +name = "array_param_index" +type = "bin" +authors = [""] +compiler_version = ">=0.35.0" + +[dependencies] diff --git a/test_programs/formal_verify_success/array_param_index/src/main.nr b/test_programs/formal_verify_success/array_param_index/src/main.nr new file mode 100644 index 00000000000..fa1abd1e207 --- /dev/null +++ b/test_programs/formal_verify_success/array_param_index/src/main.nr @@ -0,0 +1,6 @@ +#['requires(x[3].0 == -2)] +#['requires(i < 5)] +fn main(mut x: [(i32, u32); 5], i: u32, y: u32) -> pub [(i32, u32); 5] { + x[i].1 = y; + x +} diff --git a/test_programs/formal_verify_success/array_set_1/src/main.nr b/test_programs/formal_verify_success/array_set_1/src/main.nr index 61101c3b38d..1b0efa7957a 100644 --- a/test_programs/formal_verify_success/array_set_1/src/main.nr +++ b/test_programs/formal_verify_success/array_set_1/src/main.nr @@ -1,5 +1,5 @@ -#[requires(i < 5)] -#[ensures(result[i] == y)] +#['requires(i < 5)] +#['ensures(result[i] == y)] fn main(mut x: [u32; 5], i: u32, y: u32) -> pub [u32; 5] { x[i] = y; x diff --git a/test_programs/formal_verify_success/array_set_complex_composite_type/src/main.nr b/test_programs/formal_verify_success/array_set_complex_composite_type/src/main.nr index 9a9675b1ce2..d67073724d9 100644 --- a/test_programs/formal_verify_success/array_set_complex_composite_type/src/main.nr +++ b/test_programs/formal_verify_success/array_set_complex_composite_type/src/main.nr @@ -12,8 +12,8 @@ struct B { y: ([A;19],(i16, bool, (i8, [(C, u32);5], u32), u16)) } -#[requires(x < 2)] -#[ensures(result[x].y.1.2.1[x].0.b[x].third.0 == 5)] +#['requires(x < 2)] +#['ensures(result[x].y.1.2.1[x].0.b[x].third.0 == 5)] fn main(mut arr: [B;2], x: u32) -> pub [B;2] { arr[x].y.1.2.1[x].0.b[x].third.0 = 5; arr diff --git a/test_programs/formal_verify_success/array_set_composite_types_1/src/main.nr b/test_programs/formal_verify_success/array_set_composite_types_1/src/main.nr index 0cdce4a1ff2..31222425e1f 100644 --- a/test_programs/formal_verify_success/array_set_composite_types_1/src/main.nr +++ b/test_programs/formal_verify_success/array_set_composite_types_1/src/main.nr @@ -1,5 +1,5 @@ -#[requires(index < 5)] -#[ensures(result[index].1 == y)] +#['requires(index < 5)] +#['ensures(result[index].1 == y)] fn main(mut x: [(u32, i32); 5], y: i32, index: u32) -> pub [(u32, i32); 5] { x[index].1 = y; x diff --git a/test_programs/formal_verify_success/array_set_composite_types_3/src/main.nr b/test_programs/formal_verify_success/array_set_composite_types_3/src/main.nr index e33cf20ef81..7e7213356d3 100644 --- a/test_programs/formal_verify_success/array_set_composite_types_3/src/main.nr +++ b/test_programs/formal_verify_success/array_set_composite_types_3/src/main.nr @@ -3,8 +3,8 @@ struct A { second: (u32, u32, u32), } -#[requires(x < 1)] -#[ensures(result[x + 1].second.2 == 1)] +#['requires(x < 1)] +#['ensures(result[x + 1].second.2 == 1)] fn main(mut arr: [A; 2], x: u32) -> pub [A; 2] { arr[x + 1].second.2 = 1; arr diff --git a/test_programs/formal_verify_success/array_set_simple/src/main.nr b/test_programs/formal_verify_success/array_set_simple/src/main.nr index 8f2b70e471d..03fb5bedfcd 100644 --- a/test_programs/formal_verify_success/array_set_simple/src/main.nr +++ b/test_programs/formal_verify_success/array_set_simple/src/main.nr @@ -1,4 +1,4 @@ -#[ensures(result == 15)] +#['ensures(result == 15)] fn main(x: [u32; 5], i: u32, y: u32) -> pub u32 { let mut arr = x; arr[3] = 15; diff --git a/test_programs/formal_verify_success/bitshifts/src/main.nr b/test_programs/formal_verify_success/bitshifts/src/main.nr index 32ce9154aa0..ce10ab556ac 100644 --- a/test_programs/formal_verify_success/bitshifts/src/main.nr +++ b/test_programs/formal_verify_success/bitshifts/src/main.nr @@ -1,17 +1,17 @@ -#[requires((x < 10) & (y < 3))] +#['requires((x < 10) & (y < 3))] fn main(x: u32, y: u8) { let _ = lbs(x, y); let _ = rbs(x, y); } -#[requires((x < 10) & (y < 3))] -#[ensures(result == x << y)] +#['requires((x < 10) & (y < 3))] +#['ensures(result == x << y)] fn lbs(x: u32, y: u8) -> u32 { x << y } -#[requires((x < 10) & (y < 3))] -#[ensures(result == x >> y)] +#['requires((x < 10) & (y < 3))] +#['ensures(result == x >> y)] fn rbs(x: u32, y: u8) -> u32 { x >> y } diff --git a/test_programs/formal_verify_success/boolean/src/main.nr b/test_programs/formal_verify_success/boolean/src/main.nr index 7fe5b037a76..b210ccefb2a 100644 --- a/test_programs/formal_verify_success/boolean/src/main.nr +++ b/test_programs/formal_verify_success/boolean/src/main.nr @@ -5,22 +5,22 @@ fn main(x: bool, y: bool) { let _ = not(x); } -#[ensures(result == x ^ y)] +#['ensures(result == x ^ y)] fn xor(x: bool, y: bool) -> bool { x ^ y } -#[ensures(result == x & y)] +#['ensures(result == x & y)] fn and(x: bool, y: bool) -> bool { x & y } -#[ensures(result == x | y)] +#['ensures(result == x | y)] fn or(x: bool, y: bool) -> bool { x | y } -#[ensures(result == ! x)] +#['ensures(result == ! x)] fn not(x: bool) -> bool { ! x } diff --git a/test_programs/formal_verify_success/call_struct_method/src/main.nr b/test_programs/formal_verify_success/call_struct_method/src/main.nr index 22c011eb973..f4bd6ebdd77 100644 --- a/test_programs/formal_verify_success/call_struct_method/src/main.nr +++ b/test_programs/formal_verify_success/call_struct_method/src/main.nr @@ -4,7 +4,7 @@ struct A { } impl A { - #[ensures(result.balance == self.balance / 2)] + #['ensures(result.balance == self.balance / 2)] fn foo(mut self) -> Self { self.balance = self.balance / 2; self diff --git a/test_programs/formal_verify_success/cast/src/main.nr b/test_programs/formal_verify_success/cast/src/main.nr index 4fd90704d50..d1034305bed 100644 --- a/test_programs/formal_verify_success/cast/src/main.nr +++ b/test_programs/formal_verify_success/cast/src/main.nr @@ -1,4 +1,4 @@ -#[ensures(result == (x as u32) as u8)] +#['ensures(result == (x as u32) as u8)] fn main(x: u16) -> pub u8 { (x as u32) as u8 } diff --git a/test_programs/formal_verify_success/cast_from_to_field/src/main.nr b/test_programs/formal_verify_success/cast_from_to_field/src/main.nr index 0cc81a946e3..9edd569c453 100644 --- a/test_programs/formal_verify_success/cast_from_to_field/src/main.nr +++ b/test_programs/formal_verify_success/cast_from_to_field/src/main.nr @@ -1,4 +1,4 @@ -#[requires((x == 0) | (x == 1))] +#['requires((x == 0) | (x == 1))] fn main(x: Field) -> pub Field { ((x as u32) + 1) as Field } diff --git a/test_programs/formal_verify_success/comparison/src/main.nr b/test_programs/formal_verify_success/comparison/src/main.nr index 01153fe0c05..d1119041641 100644 --- a/test_programs/formal_verify_success/comparison/src/main.nr +++ b/test_programs/formal_verify_success/comparison/src/main.nr @@ -7,32 +7,32 @@ fn main(x: u8, y: u8) { let _ = neq(x, y); } -#[ensures(result == (x < y))] +#['ensures(result == (x < y))] fn lt(x: u8, y: u8) -> bool { x < y } -#[ensures(result == (x <= y))] +#['ensures(result == (x <= y))] fn lte(x: u8, y: u8) -> bool { x <= y } -#[ensures(result == (x > y))] +#['ensures(result == (x > y))] fn gt(x: u8, y: u8) -> bool { x > y } -#[ensures(result == (x >= y))] +#['ensures(result == (x >= y))] fn gte(x: u8, y: u8) -> bool { x >= y } -#[ensures(result == (x == y))] +#['ensures(result == (x == y))] fn eq(x: u8, y: u8) -> bool { x == y } -#[ensures(result == (x != y))] +#['ensures(result == (x != y))] fn neq(x: u8, y: u8) -> bool { x != y } diff --git a/test_programs/formal_verify_success/eq_trait/Nargo.toml b/test_programs/formal_verify_success/eq_trait/Nargo.toml new file mode 100644 index 00000000000..2d491de682b --- /dev/null +++ b/test_programs/formal_verify_success/eq_trait/Nargo.toml @@ -0,0 +1,7 @@ +[package] +name = "eq_trait" +type = "bin" +authors = [""] +compiler_version = ">=0.34.0" + +[dependencies] diff --git a/test_programs/formal_verify_success/eq_trait/src/main.nr b/test_programs/formal_verify_success/eq_trait/src/main.nr new file mode 100644 index 00000000000..313b94f4284 --- /dev/null +++ b/test_programs/formal_verify_success/eq_trait/src/main.nr @@ -0,0 +1,10 @@ +#['ensures(result == x)] +fn main(x: u32) -> pub u32 { + id(x) +} + +#['ensures(result == x)] +fn id(x: T) -> T + where T: Eq { + x +} diff --git a/test_programs/formal_verify_success/eq_trait_1/Nargo.toml b/test_programs/formal_verify_success/eq_trait_1/Nargo.toml new file mode 100644 index 00000000000..b243a2d5963 --- /dev/null +++ b/test_programs/formal_verify_success/eq_trait_1/Nargo.toml @@ -0,0 +1,7 @@ +[package] +name = "eq_trait_1" +type = "bin" +authors = [""] +compiler_version = ">=0.34.0" + +[dependencies] diff --git a/test_programs/formal_verify_success/eq_trait_1/src/main.nr b/test_programs/formal_verify_success/eq_trait_1/src/main.nr new file mode 100644 index 00000000000..c4d458816d0 --- /dev/null +++ b/test_programs/formal_verify_success/eq_trait_1/src/main.nr @@ -0,0 +1,14 @@ +#['ensures(result == x)] +fn main(x: u32) -> pub u32 { + id(x) +} + +#['ensures(result == x)] +fn id(x: T) -> T + where T: Eq { + if x == x { + x + } else { + x + } +} diff --git a/test_programs/formal_verify_success/exists_big_element_sum/src/main.nr b/test_programs/formal_verify_success/exists_big_element_sum/src/main.nr index 9e1df918091..5ac49a1ef7d 100644 --- a/test_programs/formal_verify_success/exists_big_element_sum/src/main.nr +++ b/test_programs/formal_verify_success/exists_big_element_sum/src/main.nr @@ -1,5 +1,5 @@ -#[requires(exists(|i| (0 <= i) & (i < 20) & arr[i] > 100))] -#[ensures(result > 100)] +#['requires(exists(|i| (0 <= i) & (i < 20) & arr[i] > 100))] +#['ensures(result > 100)] // We require that an element bigger than 100 exists in the array. // Therefore we expect the sum to be bigger than 100. fn main(arr: [u16; 20]) -> pub u64 { diff --git a/test_programs/formal_verify_success/exists_zero_in_array/src/main.nr b/test_programs/formal_verify_success/exists_zero_in_array/src/main.nr index 7f56c7c52aa..9ccef827f47 100644 --- a/test_programs/formal_verify_success/exists_zero_in_array/src/main.nr +++ b/test_programs/formal_verify_success/exists_zero_in_array/src/main.nr @@ -1,5 +1,5 @@ -#[requires(exists(|i| (0 <= i) & (i < 7) & (arr[i] == 0)))] -#[ensures(result == 0)] +#['requires(exists(|i| (0 <= i) & (i < 7) & (arr[i] == 0)))] +#['ensures(result == 0)] fn main(arr: [u8; 7]) -> pub u64 { let mut mul: u64 = 1; for i in 0..7 { diff --git a/test_programs/formal_verify_success/field_arithmetic/src/main.nr b/test_programs/formal_verify_success/field_arithmetic/src/main.nr index c003aab277c..54d0a9cafee 100644 --- a/test_programs/formal_verify_success/field_arithmetic/src/main.nr +++ b/test_programs/formal_verify_success/field_arithmetic/src/main.nr @@ -7,22 +7,22 @@ fn main(x: Field, y: Field) { let _ = div(x, y); } -#[ensures(result == x + y)] +#['ensures(result == x + y)] fn plus(x: Field, y: Field) -> Field { x + y } -#[ensures(result == x - y)] +#['ensures(result == x - y)] fn minus(x: Field, y: Field) -> Field { x - y } -#[ensures(result == x * y)] +#['ensures(result == x * y)] fn mult(x: Field, y: Field) -> Field { x * y } -#[ensures(result == x / y)] +#['ensures(result == x / y)] fn div(x: Field, y: Field) -> Field { x / y } diff --git a/test_programs/formal_verify_success/field_minus_one_is_max/src/main.nr b/test_programs/formal_verify_success/field_minus_one_is_max/src/main.nr index 7c24ba5783e..246dcd8d6df 100644 --- a/test_programs/formal_verify_success/field_minus_one_is_max/src/main.nr +++ b/test_programs/formal_verify_success/field_minus_one_is_max/src/main.nr @@ -1,4 +1,4 @@ -#[requires(x == -1)] +#['requires(x == -1)] fn main(x: Field) { let z: Field = 21888242871839275222246405745257275088548364400416034343698204186575808495616; assert(x == z); diff --git a/test_programs/formal_verify_success/field_wrapped_overflow_1/src/main.nr b/test_programs/formal_verify_success/field_wrapped_overflow_1/src/main.nr index 4dab13353c8..e30110dc8b5 100644 --- a/test_programs/formal_verify_success/field_wrapped_overflow_1/src/main.nr +++ b/test_programs/formal_verify_success/field_wrapped_overflow_1/src/main.nr @@ -1,7 +1,7 @@ // The prime that defines the integer field is // p = 21888242871839275222246405745257275088548364400416034343698204186575808495617 // Adding 1 to p-1 should result in 0. -#[requires((x == 0) & (y == 1))] +#['requires((x == 0) & (y == 1))] fn main(x: Field, y: Field) { let z: Field = 21888242871839275222246405745257275088548364400416034343698204186575808495616; assert(z + y == x); diff --git a/test_programs/formal_verify_success/field_wrapped_overflow_2/src/main.nr b/test_programs/formal_verify_success/field_wrapped_overflow_2/src/main.nr index f3930c6ef04..03917fa10c5 100644 --- a/test_programs/formal_verify_success/field_wrapped_overflow_2/src/main.nr +++ b/test_programs/formal_verify_success/field_wrapped_overflow_2/src/main.nr @@ -1,7 +1,7 @@ // The prime that defines the integer field is // p = 21888242871839275222246405745257275088548364400416034343698204186575808495617 // Adding 1 to p-1 should result in 0. y is 1 and x is 0 in Prover.toml. -#[requires((x == 9) & (y == 10))] +#['requires((x == 9) & (y == 10))] fn main(x: Field, y: Field) { let z: Field = 21888242871839275222246405745257275088548364400416034343698204186575808495616; diff --git a/test_programs/formal_verify_success/field_wrapped_overflow_3/src/main.nr b/test_programs/formal_verify_success/field_wrapped_overflow_3/src/main.nr index 7b4c2b00098..47627d1f961 100644 --- a/test_programs/formal_verify_success/field_wrapped_overflow_3/src/main.nr +++ b/test_programs/formal_verify_success/field_wrapped_overflow_3/src/main.nr @@ -1,8 +1,8 @@ // The prime that defines the integer field is // p = 21888242871839275222246405745257275088548364400416034343698204186575808495617 // Adding 1 to p-1 should result in 0. -#[requires((x == 21888242871839275222246405745257275088548364400416034343698204186575808495616) & (y == 1))] -#[ensures(result == x + y)] // Tests if Field sum in annotation is also correct. +#['requires((x == 21888242871839275222246405745257275088548364400416034343698204186575808495616) & (y == 1))] +#['ensures(result == x + y)] // Tests if Field sum in annotation is also correct. fn main(x: Field, y: Field) -> pub Field { x + y // Wraps around and the result should equal to zero. } diff --git a/test_programs/formal_verify_success/field_wrapped_overflow_4/src/main.nr b/test_programs/formal_verify_success/field_wrapped_overflow_4/src/main.nr index 68ed3330a16..7d5fca5c678 100644 --- a/test_programs/formal_verify_success/field_wrapped_overflow_4/src/main.nr +++ b/test_programs/formal_verify_success/field_wrapped_overflow_4/src/main.nr @@ -2,7 +2,7 @@ // p = 21888242871839275222246405745257275088548364400416034343698204186575808495617 // Adding p-1 + p-1 + p-1 should result in p-3. // Goal is to prove (p - 3 + 3) == 0 -#[requires((x == 0) & (y == 21888242871839275222246405745257275088548364400416034343698204186575808495616))] +#['requires((x == 0) & (y == 21888242871839275222246405745257275088548364400416034343698204186575808495616))] fn main(x: Field, y: Field) { let z = y + y + y; assert(z + 3 == x); diff --git a/test_programs/formal_verify_success/field_wrapped_overflow_5/src/main.nr b/test_programs/formal_verify_success/field_wrapped_overflow_5/src/main.nr index bcc099f553d..00717437592 100644 --- a/test_programs/formal_verify_success/field_wrapped_overflow_5/src/main.nr +++ b/test_programs/formal_verify_success/field_wrapped_overflow_5/src/main.nr @@ -2,7 +2,7 @@ // p = 21888242871839275222246405745257275088548364400416034343698204186575808495617 // If we have the value (p+1)/2 and we multiply it by 2 we will get p+1 // but if we divide p+1 by 2 we will not get the original value but we will get 0. -#[requires((x == 2) & (y == 0))] +#['requires((x == 2) & (y == 0))] fn main(x: Field, y: Field) { let z: Field = 10944121435919637611123202872628637544274182200208017171849102093287904247809; // ((p + 1) / 2) let w = z * x; // ((p + 1)/2) * 2 ==> w == p + 1 == 1 diff --git a/test_programs/formal_verify_success/for_loop_array_const/src/main.nr b/test_programs/formal_verify_success/for_loop_array_const/src/main.nr index 09def704f27..4ad7507f47c 100644 --- a/test_programs/formal_verify_success/for_loop_array_const/src/main.nr +++ b/test_programs/formal_verify_success/for_loop_array_const/src/main.nr @@ -1,4 +1,4 @@ -#[ensures(result == 10)] +#['ensures(result == 10)] fn main() -> pub u32 { let x = [2, 5]; let y = x[1]; diff --git a/test_programs/formal_verify_success/for_loop_blocks/src/main.nr b/test_programs/formal_verify_success/for_loop_blocks/src/main.nr index 676e04799d8..5a969ff7b35 100644 --- a/test_programs/formal_verify_success/for_loop_blocks/src/main.nr +++ b/test_programs/formal_verify_success/for_loop_blocks/src/main.nr @@ -1,4 +1,4 @@ -#[ensures(result == 10)] +#['ensures(result == 10)] fn main() -> pub u32 { let x = { let a = 3; diff --git a/test_programs/formal_verify_success/for_loop_nested_complex/src/main.nr b/test_programs/formal_verify_success/for_loop_nested_complex/src/main.nr index cb70ade3ef4..b662dbb515c 100644 --- a/test_programs/formal_verify_success/for_loop_nested_complex/src/main.nr +++ b/test_programs/formal_verify_success/for_loop_nested_complex/src/main.nr @@ -1,4 +1,4 @@ -#[ensures(result == 2)] +#['ensures(result == 2)] fn main() -> pub u32 { let x = 2; let y = 3; diff --git a/test_programs/formal_verify_success/for_loop_nested_simple/src/main.nr b/test_programs/formal_verify_success/for_loop_nested_simple/src/main.nr index 0a9f9c3583a..d9965abe3bc 100644 --- a/test_programs/formal_verify_success/for_loop_nested_simple/src/main.nr +++ b/test_programs/formal_verify_success/for_loop_nested_simple/src/main.nr @@ -1,4 +1,4 @@ -#[ensures(result == 10)] +#['ensures(result == 10)] fn main() -> pub u32 { let x = 3; let mut sum = 0; diff --git a/test_programs/formal_verify_success/for_loop_simple/src/main.nr b/test_programs/formal_verify_success/for_loop_simple/src/main.nr index 12414d91bda..ea2bf2f09ed 100644 --- a/test_programs/formal_verify_success/for_loop_simple/src/main.nr +++ b/test_programs/formal_verify_success/for_loop_simple/src/main.nr @@ -1,4 +1,4 @@ -#[ensures(result == 10)] +#['ensures(result == 10)] fn main() -> pub u32 { let x = 2 + 3; let mut sum = 0; diff --git a/test_programs/formal_verify_success/for_loop_structure_const/src/main.nr b/test_programs/formal_verify_success/for_loop_structure_const/src/main.nr index cab4df3f070..2d5e4c0dcb9 100644 --- a/test_programs/formal_verify_success/for_loop_structure_const/src/main.nr +++ b/test_programs/formal_verify_success/for_loop_structure_const/src/main.nr @@ -3,7 +3,7 @@ struct A { b: u32 } -#[ensures(result == 10)] +#['ensures(result == 10)] fn main() -> pub u32 { let x = A{a: 2, b: 5}; let y = x.b; diff --git a/test_programs/formal_verify_success/for_loop_tuple_const/src/main.nr b/test_programs/formal_verify_success/for_loop_tuple_const/src/main.nr index 578474233e9..c827b5e2624 100644 --- a/test_programs/formal_verify_success/for_loop_tuple_const/src/main.nr +++ b/test_programs/formal_verify_success/for_loop_tuple_const/src/main.nr @@ -1,4 +1,4 @@ -#[ensures(result == 10)] +#['ensures(result == 10)] fn main() -> pub u32 { let x = (2, 5); let y = x.1; diff --git a/test_programs/formal_verify_success/forall_max_is_max/src/main.nr b/test_programs/formal_verify_success/forall_max_is_max/src/main.nr index 48213a1ae50..9f129e104f1 100644 --- a/test_programs/formal_verify_success/forall_max_is_max/src/main.nr +++ b/test_programs/formal_verify_success/forall_max_is_max/src/main.nr @@ -1,5 +1,5 @@ -#[requires(forall(|i, j| (0 <= i) & (i < j) & (j < 15) ==> v[i] <= v[j]))] -#[ensures(forall(|i| (0 <= i) & (i < 15) ==> v[i] <= result))] +#['requires(forall(|i, j| (0 <= i) & (i < j) & (j < 15) ==> v[i] <= v[j]))] +#['ensures(forall(|i| (0 <= i) & (i < 15) ==> v[i] <= result))] fn main(v: [u64; 15], k: u64) -> pub u64 { v[14] // The array is sorted and this is the last element, therefore it's the maximum element. } diff --git a/test_programs/formal_verify_success/forall_structure/src/main.nr b/test_programs/formal_verify_success/forall_structure/src/main.nr index 5a4eefb352b..94a6ddf1510 100644 --- a/test_programs/formal_verify_success/forall_structure/src/main.nr +++ b/test_programs/formal_verify_success/forall_structure/src/main.nr @@ -2,7 +2,7 @@ struct A { id: Field, balance: u32, } -#[requires(forall(|i, j| (0 <= i) & (i < j) & (j < 2) +#['requires(forall(|i, j| (0 <= i) & (i < j) & (j < 2) ==> x[i].id != x[j].id))] fn main(x: [A; 2]) {} diff --git a/test_programs/formal_verify_success/forall_sum_of_evens/src/main.nr b/test_programs/formal_verify_success/forall_sum_of_evens/src/main.nr index a612e27502c..cdc9fdabc9b 100644 --- a/test_programs/formal_verify_success/forall_sum_of_evens/src/main.nr +++ b/test_programs/formal_verify_success/forall_sum_of_evens/src/main.nr @@ -1,6 +1,6 @@ -#[requires(forall(|i| (0 <= i) & (i < 10) ==> arr[i] % 2 == 0) +#['requires(forall(|i| (0 <= i) & (i < 10) ==> arr[i] % 2 == 0) & forall(|i| (0 <= i) & (i < 10) ==> arr[i] < 100) )] -#[ensures((result % 2 == 0) & (result < 1000))] +#['ensures((result % 2 == 0) & (result < 1000))] // The sum of an array which constist of even elements upper bounded by 100 // will be even and upper bounded by 1000 fn main(arr: [u32; 10]) -> pub u32 { diff --git a/test_programs/formal_verify_success/func_call_in_annotation/Nargo.toml b/test_programs/formal_verify_success/func_call_in_annotation/Nargo.toml new file mode 100644 index 00000000000..880c4736df8 --- /dev/null +++ b/test_programs/formal_verify_success/func_call_in_annotation/Nargo.toml @@ -0,0 +1,6 @@ +[package] +name = "func_call_in_annotation" +type = "bin" +authors = [""] + +[dependencies] \ No newline at end of file diff --git a/test_programs/formal_verify_success/func_call_in_annotation/src/main.nr b/test_programs/formal_verify_success/func_call_in_annotation/src/main.nr new file mode 100644 index 00000000000..854881424fd --- /dev/null +++ b/test_programs/formal_verify_success/func_call_in_annotation/src/main.nr @@ -0,0 +1,7 @@ +#['ensures(foo(5))] +fn main() {} + +#['ghost] +fn foo(x: u16) -> bool { + true +} diff --git a/test_programs/formal_verify_success/func_call_in_if/src/main.nr b/test_programs/formal_verify_success/func_call_in_if/src/main.nr index e683dbe04ab..7f69e0cfc17 100644 --- a/test_programs/formal_verify_success/func_call_in_if/src/main.nr +++ b/test_programs/formal_verify_success/func_call_in_if/src/main.nr @@ -2,7 +2,7 @@ fn main(x: u32) -> pub u32 { if x > 5 { foo(x) } else { x } } -#[requires(x > 5)] +#['requires(x > 5)] fn foo(x: u32) -> u32 { 0 } diff --git a/test_programs/formal_verify_success/func_call_in_if_2/src/main.nr b/test_programs/formal_verify_success/func_call_in_if_2/src/main.nr index fbd5c20f0af..6f65e35eab8 100644 --- a/test_programs/formal_verify_success/func_call_in_if_2/src/main.nr +++ b/test_programs/formal_verify_success/func_call_in_if_2/src/main.nr @@ -2,7 +2,7 @@ fn main(x: u32) -> pub (u32, u32) { if x > 5 { foo(x) } else { (x, x) } } -#[requires(x > 5)] +#['requires(x > 5)] fn foo(x: u32) -> (u32, u32) { (0, 0) } diff --git a/test_programs/formal_verify_success/func_call_in_if_3/src/main.nr b/test_programs/formal_verify_success/func_call_in_if_3/src/main.nr index 861503a10a9..36a9a593bf5 100644 --- a/test_programs/formal_verify_success/func_call_in_if_3/src/main.nr +++ b/test_programs/formal_verify_success/func_call_in_if_3/src/main.nr @@ -2,7 +2,7 @@ fn main(x: u32) -> pub [u32; 3] { if x > 5 { foo(x) } else { [x, x, x] } } -#[requires(x > 5)] +#['requires(x > 5)] fn foo(x: u32) -> [u32; 3] { [0, 0, 0] } diff --git a/test_programs/formal_verify_success/func_call_in_if_4/src/main.nr b/test_programs/formal_verify_success/func_call_in_if_4/src/main.nr index 9e131148e1c..2f02b75bb3b 100644 --- a/test_programs/formal_verify_success/func_call_in_if_4/src/main.nr +++ b/test_programs/formal_verify_success/func_call_in_if_4/src/main.nr @@ -7,5 +7,5 @@ fn main(x: u32) -> pub u32 { } } -#[requires(x > 5)] +#['requires(x > 5)] fn foo(x: u32) {} diff --git a/test_programs/formal_verify_success/fv_attribute_name_resolution_1/src/main.nr b/test_programs/formal_verify_success/fv_attribute_name_resolution_1/src/main.nr index 6b5fff5807b..b694e0d9c5e 100644 --- a/test_programs/formal_verify_success/fv_attribute_name_resolution_1/src/main.nr +++ b/test_programs/formal_verify_success/fv_attribute_name_resolution_1/src/main.nr @@ -1,6 +1,6 @@ fn main() {} -#[requires(x as u32 > 5)] // as u32 because fields can not be compared +#['requires(x as u32 > 5)] // as u32 because fields can not be compared fn foo(x: Field) -> Field { x + x } diff --git a/test_programs/formal_verify_success/fv_attribute_name_resolution_2/src/main.nr b/test_programs/formal_verify_success/fv_attribute_name_resolution_2/src/main.nr index 711edd0209d..cc0b378f6b2 100644 --- a/test_programs/formal_verify_success/fv_attribute_name_resolution_2/src/main.nr +++ b/test_programs/formal_verify_success/fv_attribute_name_resolution_2/src/main.nr @@ -1,6 +1,6 @@ fn main() {} -#[ensures(result as u32 > 5)] // result can be only used in the ensures attribute +#['ensures(result as u32 > 5)] // result can be only used in the ensures attribute fn foo(x: Field) -> Field { x + x } diff --git a/test_programs/formal_verify_success/fv_attribute_name_resolution_3/src/main.nr b/test_programs/formal_verify_success/fv_attribute_name_resolution_3/src/main.nr index 2f4d33d43b3..9eaabfdb421 100644 --- a/test_programs/formal_verify_success/fv_attribute_name_resolution_3/src/main.nr +++ b/test_programs/formal_verify_success/fv_attribute_name_resolution_3/src/main.nr @@ -1,6 +1,6 @@ fn main() {} -#[ensures(result == x + x)] +#['ensures(result == x + x)] fn foo(x: Field) -> Field { x + x } diff --git a/test_programs/formal_verify_success/fv_attribute_type_check_1/src/main.nr b/test_programs/formal_verify_success/fv_attribute_type_check_1/src/main.nr index 91da7fd3889..99abb903ed4 100644 --- a/test_programs/formal_verify_success/fv_attribute_type_check_1/src/main.nr +++ b/test_programs/formal_verify_success/fv_attribute_type_check_1/src/main.nr @@ -1,6 +1,6 @@ fn main() {} -#[requires(x)] +#['requires(x)] fn foo(x: bool) -> Field { 5 } diff --git a/test_programs/formal_verify_success/fv_attribute_type_check_2/src/main.nr b/test_programs/formal_verify_success/fv_attribute_type_check_2/src/main.nr index e6bfe101217..57897c1464d 100644 --- a/test_programs/formal_verify_success/fv_attribute_type_check_2/src/main.nr +++ b/test_programs/formal_verify_success/fv_attribute_type_check_2/src/main.nr @@ -1,6 +1,6 @@ fn main() {} -#[ensures(result)] +#['ensures(result)] fn foo() -> bool { true } diff --git a/test_programs/formal_verify_success/fv_attribute_type_check_3/src/main.nr b/test_programs/formal_verify_success/fv_attribute_type_check_3/src/main.nr index 51bb51d539f..ab571a88cf9 100644 --- a/test_programs/formal_verify_success/fv_attribute_type_check_3/src/main.nr +++ b/test_programs/formal_verify_success/fv_attribute_type_check_3/src/main.nr @@ -1,5 +1,5 @@ fn main() {} -#[requires(5 > 5)] +#['requires(5 > 5)] fn foo() {} diff --git a/test_programs/formal_verify_success/fv_std_old/src/main.nr b/test_programs/formal_verify_success/fv_std_old/src/main.nr index 8c75f8a5b3b..ff28d8ec3ef 100644 --- a/test_programs/formal_verify_success/fv_std_old/src/main.nr +++ b/test_programs/formal_verify_success/fv_std_old/src/main.nr @@ -1,14 +1,14 @@ use fv_std::old; -#[requires(x == 4)] -#[ensures(result == 5)] +#['requires(x == 4)] +#['ensures(result == 5)] fn main(mut x: u32) -> pub u32 { foo(&mut x); x } -#[requires(*old(x) == 4)] -#[ensures(*x == *old(x) + 1)] +#['requires(*old(x) == 4)] +#['ensures(*x == *old(x) + 1)] fn foo(x: &mut u32) { *x = *x + 1; } diff --git a/test_programs/formal_verify_success/generics_basic/Nargo.toml b/test_programs/formal_verify_success/generics_basic/Nargo.toml new file mode 100644 index 00000000000..e795dcdebf7 --- /dev/null +++ b/test_programs/formal_verify_success/generics_basic/Nargo.toml @@ -0,0 +1,6 @@ +[package] +name = "generics_testing_ground" +type = "bin" +authors = [""] + +[dependencies] \ No newline at end of file diff --git a/test_programs/formal_verify_success/generics_basic/src/main.nr b/test_programs/formal_verify_success/generics_basic/src/main.nr new file mode 100644 index 00000000000..7ae15302c34 --- /dev/null +++ b/test_programs/formal_verify_success/generics_basic/src/main.nr @@ -0,0 +1,8 @@ +#['requires(generic_func(x, x))] +fn main(x: u32) { +} + +#['ghost] +fn generic_func(x: T, y: u32) -> bool { + true +} diff --git a/test_programs/formal_verify_success/ghost_function_in_attribute/Nargo.toml b/test_programs/formal_verify_success/ghost_function_in_attribute/Nargo.toml new file mode 100644 index 00000000000..6af505de980 --- /dev/null +++ b/test_programs/formal_verify_success/ghost_function_in_attribute/Nargo.toml @@ -0,0 +1,7 @@ +[package] +name = "ghost_function_in_attribute" +type = "bin" +authors = [""] +compiler_version = ">=0.35.0" + +[dependencies] diff --git a/test_programs/formal_verify_success/ghost_function_in_attribute/src/main.nr b/test_programs/formal_verify_success/ghost_function_in_attribute/src/main.nr new file mode 100644 index 00000000000..88fdab1921c --- /dev/null +++ b/test_programs/formal_verify_success/ghost_function_in_attribute/src/main.nr @@ -0,0 +1,14 @@ +#['ensures(result == baz())] +fn main(x: Field, y: pub Field) -> pub u32 { + foo().1 +} + +#['ensures(result.1 == 2)] +fn foo() -> (u32, u32){ + (1, 2) +} + +#['ghost] +fn baz() -> u32 { + 2 +} diff --git a/test_programs/formal_verify_success/global_const_in_module/Nargo.toml b/test_programs/formal_verify_success/global_const_in_module/Nargo.toml new file mode 100644 index 00000000000..6a4192ee5b2 --- /dev/null +++ b/test_programs/formal_verify_success/global_const_in_module/Nargo.toml @@ -0,0 +1,7 @@ +[package] +name = "global_const_in_module" +type = "bin" +authors = [""] + +[dependencies] +fv_std = { path = "../../../fv_std" } diff --git a/test_programs/formal_verify_success/global_const_in_module/src/main.nr b/test_programs/formal_verify_success/global_const_in_module/src/main.nr new file mode 100644 index 00000000000..4b39b4ae15e --- /dev/null +++ b/test_programs/formal_verify_success/global_const_in_module/src/main.nr @@ -0,0 +1,9 @@ +use fv_std; + +#['ensures(bar::x == fv_std::U8_MIN)] +fn main() { +} + +mod bar { + global x: u32 = 0; +} diff --git a/test_programs/formal_verify_success/global_const_in_nested_module/Nargo.toml b/test_programs/formal_verify_success/global_const_in_nested_module/Nargo.toml new file mode 100644 index 00000000000..e9ad7c0742b --- /dev/null +++ b/test_programs/formal_verify_success/global_const_in_nested_module/Nargo.toml @@ -0,0 +1,7 @@ +[package] +name = "global_const_in_nested_module" +type = "bin" +authors = [""] + +[dependencies] +fv_std = { path = "../../../fv_std" } diff --git a/test_programs/formal_verify_success/global_const_in_nested_module/src/main.nr b/test_programs/formal_verify_success/global_const_in_nested_module/src/main.nr new file mode 100644 index 00000000000..11ca6ada33c --- /dev/null +++ b/test_programs/formal_verify_success/global_const_in_nested_module/src/main.nr @@ -0,0 +1,12 @@ +use fv_std::U8_MAX; + +#['ensures(bar::qux::x == result)] +fn main(y: u32) -> pub u32 { + (U8_MAX - 250) as u32 +} + +mod bar { + mod qux { + global x: u32 = 5; + } +} diff --git a/test_programs/formal_verify_success/identity_function/src/main.nr b/test_programs/formal_verify_success/identity_function/src/main.nr index bdf50e52ef8..2e2ca39ade3 100644 --- a/test_programs/formal_verify_success/identity_function/src/main.nr +++ b/test_programs/formal_verify_success/identity_function/src/main.nr @@ -1,4 +1,4 @@ -#[ensures(result == x)] +#['ensures(result == x)] fn main(x: u32) -> pub u32 { x } diff --git a/test_programs/formal_verify_success/if_overflow_2/src/main.nr b/test_programs/formal_verify_success/if_overflow_2/src/main.nr index b755e27dd71..432e3f22c6a 100644 --- a/test_programs/formal_verify_success/if_overflow_2/src/main.nr +++ b/test_programs/formal_verify_success/if_overflow_2/src/main.nr @@ -3,7 +3,7 @@ // We also expect the requires clause // to work correctly and make the test // equivalent to if_test_overflow_1 -#[requires(y == 255)] +#['requires(y == 255)] fn main(x: u8, y: u8) -> pub u8 { if x < y { x + 1 diff --git a/test_programs/formal_verify_success/implication_operator_1/src/main.nr b/test_programs/formal_verify_success/implication_operator_1/src/main.nr index ccf9781967a..01073a6dacd 100644 --- a/test_programs/formal_verify_success/implication_operator_1/src/main.nr +++ b/test_programs/formal_verify_success/implication_operator_1/src/main.nr @@ -1,4 +1,4 @@ -#[ensures((y ==> result == x) & (!y ==> result == 0))] +#['ensures((y ==> result == x) & (!y ==> result == 0))] fn main(x: u32, y: bool) -> pub u32 { if y { x diff --git a/test_programs/formal_verify_success/implication_operator_2/src/main.nr b/test_programs/formal_verify_success/implication_operator_2/src/main.nr index 680f6c50ce1..6aecc384942 100644 --- a/test_programs/formal_verify_success/implication_operator_2/src/main.nr +++ b/test_programs/formal_verify_success/implication_operator_2/src/main.nr @@ -1,6 +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)] +#['requires(y ==> x > 5)] fn main(x: u32, y: bool) { assert(y ==> x > 5); } diff --git a/test_programs/formal_verify_success/index_array/src/main.nr b/test_programs/formal_verify_success/index_array/src/main.nr index ae629485911..46cb602aeaf 100644 --- a/test_programs/formal_verify_success/index_array/src/main.nr +++ b/test_programs/formal_verify_success/index_array/src/main.nr @@ -1,4 +1,4 @@ -#[ensures(result == arr[3])] +#['ensures(result == arr[3])] fn main(arr: [u32; 5]) -> pub u32 { arr[3] } diff --git a/test_programs/formal_verify_success/index_composite_array_with_const/src/main.nr b/test_programs/formal_verify_success/index_composite_array_with_const/src/main.nr index 1f4c982c3c8..4e384c10e6a 100644 --- a/test_programs/formal_verify_success/index_composite_array_with_const/src/main.nr +++ b/test_programs/formal_verify_success/index_composite_array_with_const/src/main.nr @@ -1,5 +1,5 @@ struct A { first: i32, second: u32, } -#[ensures(result == arr[1].second)] +#['ensures(result == arr[1].second)] fn main(arr: [A;2]) -> pub u32 { arr[1].second } diff --git a/test_programs/formal_verify_success/index_composite_array_with_var_1/src/main.nr b/test_programs/formal_verify_success/index_composite_array_with_var_1/src/main.nr index e5e0ffd462b..8008f9b2b48 100644 --- a/test_programs/formal_verify_success/index_composite_array_with_var_1/src/main.nr +++ b/test_programs/formal_verify_success/index_composite_array_with_var_1/src/main.nr @@ -1,6 +1,6 @@ struct A { first: i32, second: u32, } -#[requires(x < 2)] -#[ensures(result == arr[x].first)] +#['requires(x < 2)] +#['ensures(result == arr[x].first)] fn main(arr: [A;2], x: u32) -> pub i32 { arr[x].first } diff --git a/test_programs/formal_verify_success/index_composite_array_with_var_2/src/main.nr b/test_programs/formal_verify_success/index_composite_array_with_var_2/src/main.nr index 478bd44e30d..07333d54993 100644 --- a/test_programs/formal_verify_success/index_composite_array_with_var_2/src/main.nr +++ b/test_programs/formal_verify_success/index_composite_array_with_var_2/src/main.nr @@ -1,6 +1,6 @@ struct A { first: i32, second: u32, } -#[requires(x < 2)] -#[ensures(result == arr[x].second)] +#['requires(x < 2)] +#['ensures(result == arr[x].second)] fn main(arr: [A;2], x: u32) -> pub u32 { arr[x].second } diff --git a/test_programs/formal_verify_success/index_composite_array_with_var_3/src/main.nr b/test_programs/formal_verify_success/index_composite_array_with_var_3/src/main.nr index da285cb5a65..a52b61ebcfc 100644 --- a/test_programs/formal_verify_success/index_composite_array_with_var_3/src/main.nr +++ b/test_programs/formal_verify_success/index_composite_array_with_var_3/src/main.nr @@ -12,8 +12,8 @@ struct B { y: ([A;19],(i16, bool, (i8, [(C, u32);5], u32), u16)) } -#[requires((x < 2) & (arr[x].y.1.2.1[x].0.b[x].third.0 == 1))] -#[ensures(result == arr[x].y.1.2.1[x].0.b[x].third.0 / 2)] +#['requires((x < 2) & (arr[x].y.1.2.1[x].0.b[x].third.0 == 1))] +#['ensures(result == arr[x].y.1.2.1[x].0.b[x].third.0 / 2)] fn main(arr: [B;2], x: u32) -> pub u32 { arr[x].y.1.2.1[x].0.b[x].third.0 / 2 } diff --git a/test_programs/formal_verify_success/index_composite_array_with_var_4/src/main.nr b/test_programs/formal_verify_success/index_composite_array_with_var_4/src/main.nr index 91c3ac0eddb..b57322b693d 100644 --- a/test_programs/formal_verify_success/index_composite_array_with_var_4/src/main.nr +++ b/test_programs/formal_verify_success/index_composite_array_with_var_4/src/main.nr @@ -3,8 +3,8 @@ struct A { second: u32, } -#[requires((x < 2) & (arr[x].second == 1))] -#[ensures(result == 1)] +#['requires((x < 2) & (arr[x].second == 1))] +#['ensures(result == 1)] fn main(arr: [A; 2], x: u32) -> pub u32 { arr[x].second } diff --git a/test_programs/formal_verify_success/index_composite_array_with_var_5/src/main.nr b/test_programs/formal_verify_success/index_composite_array_with_var_5/src/main.nr index 3e8b7bba9b5..f02285a8559 100644 --- a/test_programs/formal_verify_success/index_composite_array_with_var_5/src/main.nr +++ b/test_programs/formal_verify_success/index_composite_array_with_var_5/src/main.nr @@ -1,8 +1,8 @@ // Here we are testing for a structure which has fields // of the same type. struct A { first: u32, second: u32, } -#[requires((x < 2) & (arr[x].first == 4) )] -#[ensures(result == 4)] +#['requires((x < 2) & (arr[x].first == 4) )] +#['ensures(result == 4)] fn main(arr: [A;2], x: u32) -> pub u32 { arr[x].first } diff --git a/test_programs/formal_verify_success/index_var_array_with_constant/src/main.nr b/test_programs/formal_verify_success/index_var_array_with_constant/src/main.nr index cb4568a9294..6edede7d58f 100644 --- a/test_programs/formal_verify_success/index_var_array_with_constant/src/main.nr +++ b/test_programs/formal_verify_success/index_var_array_with_constant/src/main.nr @@ -1,4 +1,4 @@ -#[ensures(result == 65)] +#['ensures(result == 65)] fn main() -> pub u32 { let arr = [857, 1, 65]; arr[2] diff --git a/test_programs/formal_verify_success/index_var_array_with_var/src/main.nr b/test_programs/formal_verify_success/index_var_array_with_var/src/main.nr index 1438a356e68..acbf131b406 100644 --- a/test_programs/formal_verify_success/index_var_array_with_var/src/main.nr +++ b/test_programs/formal_verify_success/index_var_array_with_var/src/main.nr @@ -1,5 +1,5 @@ -#[requires(x == 2)] -#[ensures(result == 65)] +#['requires(x == 2)] +#['ensures(result == 65)] fn main(x: u32) -> pub u32 { let arr = [857, 1, 65]; arr[x] diff --git a/test_programs/formal_verify_success/integer_and/src/main.nr b/test_programs/formal_verify_success/integer_and/src/main.nr index 2c3eba17af5..08b32b19693 100644 --- a/test_programs/formal_verify_success/integer_and/src/main.nr +++ b/test_programs/formal_verify_success/integer_and/src/main.nr @@ -9,42 +9,42 @@ fn main(x: i64, y: i64) { let _ = integer_u64(x as u64, y as u64); } -#[ensures(result == x & y)] +#['ensures(result == x & y)] fn integer_i8(x: i8, y: i8) -> i8 { x & y } -#[ensures(result == x & y)] +#['ensures(result == x & y)] fn integer_i16(x: i16, y: i16) -> i16 { x & y } -#[ensures(result == x & y)] +#['ensures(result == x & y)] fn integer_i32(x: i32, y: i32) -> i32 { x & y } -#[ensures(result == x & y)] +#['ensures(result == x & y)] fn integer_i64(x: i64, y: i64) -> i64 { x & y } -#[ensures(result == x & y)] +#['ensures(result == x & y)] fn integer_u8(x: u8, y: u8) -> u8 { x & y } -#[ensures(result == x & y)] +#['ensures(result == x & y)] fn integer_u16(x: u16, y: u16) -> u16 { x & y } -#[ensures(result == x & y)] +#['ensures(result == x & y)] fn integer_u32(x: u32, y: u32) -> u32 { x & y } -#[ensures(result == x & y)] +#['ensures(result == x & y)] fn integer_u64(x: u64, y: u64) -> u64 { x & y } diff --git a/test_programs/formal_verify_success/integer_consts/src/main.nr b/test_programs/formal_verify_success/integer_consts/src/main.nr index 7732226fcd8..d614e1a0ee7 100644 --- a/test_programs/formal_verify_success/integer_consts/src/main.nr +++ b/test_programs/formal_verify_success/integer_consts/src/main.nr @@ -1,7 +1,7 @@ use fv_std; -#[requires(x <= fv_std::U8_MAX & y <= fv_std::U8_MAX)] -#[ensures((x <= fv_std::U8_MAX - y) ==> result == x + y)] +#['requires(x <= fv_std::U8_MAX & y <= fv_std::U8_MAX)] +#['ensures((x <= fv_std::U8_MAX - y) ==> result == x + y)] fn safe_add_u8(x: u8, y: u8) -> u8 { if x <= fv_std::U8_MAX - y { x + y @@ -18,13 +18,13 @@ fn safe_sub_i16(a: i16, b: i16) -> i16 { } } -#[ensures(result == (p & q))] +#['ensures(result == (p & q))] fn bitwise_and_u32(p: u32, q: u32) -> u32 { p & q } -#[requires(p <= fv_std::U32_MAX & q <= fv_std::U32_MAX)] -#[ensures((p <= fv_std::U32_MAX - q) ==> result == p + q)] +#['requires(p <= fv_std::U32_MAX & q <= fv_std::U32_MAX)] +#['ensures((p <= fv_std::U32_MAX - q) ==> result == p + q)] fn safe_add_u32(p: u32, q: u32) -> u32 { if p <= fv_std::U32_MAX - q { p + q @@ -33,7 +33,7 @@ fn safe_add_u32(p: u32, q: u32) -> u32 { } } -#[requires((x <= fv_std::U8_MAX) & (y <= fv_std::U8_MAX))] +#['requires((x <= fv_std::U8_MAX) & (y <= fv_std::U8_MAX))] fn main(x: u8, y: u8, a: i16, b: i16, p: u32, q: u32) { let _ = safe_add_u8(x, y); let _ = safe_sub_i16(a, b); diff --git a/test_programs/formal_verify_success/integer_div/src/main.nr b/test_programs/formal_verify_success/integer_div/src/main.nr index a8f70478ef2..ea3fb99eb7d 100644 --- a/test_programs/formal_verify_success/integer_div/src/main.nr +++ b/test_programs/formal_verify_success/integer_div/src/main.nr @@ -1,4 +1,4 @@ -#[requires((-10 < x) & (x < 10) & (0 < y) & (y < 10))] +#['requires((-10 < x) & (x < 10) & (0 < y) & (y < 10))] fn main(x: i64, y: i64) { let _ = integer_i8(x as i8, y as i8); let _ = integer_i16(x as i16, y as i16); @@ -10,50 +10,50 @@ fn main(x: i64, y: i64) { let _ = integer_u64(x as u64, y as u64); } -#[requires(y != 0)] -#[ensures(result == x / y)] +#['requires(y != 0)] +#['ensures(result == x / y)] fn integer_i8(x: i8, y: i8) -> i8 { x / y } -#[requires(y != 0)] -#[ensures(result == x / y)] +#['requires(y != 0)] +#['ensures(result == x / y)] fn integer_i16(x: i16, y: i16) -> i16 { x / y } -#[requires(y != 0)] -#[ensures(result == x / y)] +#['requires(y != 0)] +#['ensures(result == x / y)] fn integer_i32(x: i32, y: i32) -> i32 { x / y } -#[requires(y != 0)] -#[ensures(result == x / y)] +#['requires(y != 0)] +#['ensures(result == x / y)] fn integer_i64(x: i64, y: i64) -> i64 { x / y } -#[requires(y != 0)] -#[ensures(result == x / y)] +#['requires(y != 0)] +#['ensures(result == x / y)] fn integer_u8(x: u8, y: u8) -> u8 { x / y } -#[requires(y != 0)] -#[ensures(result == x / y)] +#['requires(y != 0)] +#['ensures(result == x / y)] fn integer_u16(x: u16, y: u16) -> u16 { x / y } -#[requires(y != 0)] -#[ensures(result == x / y)] +#['requires(y != 0)] +#['ensures(result == x / y)] fn integer_u32(x: u32, y: u32) -> u32 { x / y } -#[requires(y != 0)] -#[ensures(result == x / y)] +#['requires(y != 0)] +#['ensures(result == x / y)] fn integer_u64(x: u64, y: u64) -> u64 { x / y } diff --git a/test_programs/formal_verify_success/integer_mod/src/main.nr b/test_programs/formal_verify_success/integer_mod/src/main.nr index 4e6020d5dc6..119fb67cec9 100644 --- a/test_programs/formal_verify_success/integer_mod/src/main.nr +++ b/test_programs/formal_verify_success/integer_mod/src/main.nr @@ -1,4 +1,4 @@ -#[requires((-10 < x) & (x < 10) & (0 < y) & (y < 10))] +#['requires((-10 < x) & (x < 10) & (0 < y) & (y < 10))] fn main(x: i64, y: i64) { let _ = integer_i8(x as i8, y as i8); let _ = integer_i16(x as i16, y as i16); @@ -10,50 +10,50 @@ fn main(x: i64, y: i64) { let _ = integer_u64(x as u64, y as u64); } -#[requires(y != 0)] -#[ensures(result == x % y)] +#['requires(y != 0)] +#['ensures(result == x % y)] fn integer_i8(x: i8, y: i8) -> i8 { x % y } -#[requires(y != 0)] -#[ensures(result == x % y)] +#['requires(y != 0)] +#['ensures(result == x % y)] fn integer_i16(x: i16, y: i16) -> i16 { x % y } -#[requires(y != 0)] -#[ensures(result == x % y)] +#['requires(y != 0)] +#['ensures(result == x % y)] fn integer_i32(x: i32, y: i32) -> i32 { x % y } -#[requires(y != 0)] -#[ensures(result == x % y)] +#['requires(y != 0)] +#['ensures(result == x % y)] fn integer_i64(x: i64, y: i64) -> i64 { x % y } -#[requires(y != 0)] -#[ensures(result == x % y)] +#['requires(y != 0)] +#['ensures(result == x % y)] fn integer_u8(x: u8, y: u8) -> u8 { x % y } -#[requires(y != 0)] -#[ensures(result == x % y)] +#['requires(y != 0)] +#['ensures(result == x % y)] fn integer_u16(x: u16, y: u16) -> u16 { x % y } -#[requires(y != 0)] -#[ensures(result == x % y)] +#['requires(y != 0)] +#['ensures(result == x % y)] fn integer_u32(x: u32, y: u32) -> u32 { x % y } -#[requires(y != 0)] -#[ensures(result == x % y)] +#['requires(y != 0)] +#['ensures(result == x % y)] fn integer_u64(x: u64, y: u64) -> u64 { x % y } diff --git a/test_programs/formal_verify_success/integer_not/src/main.nr b/test_programs/formal_verify_success/integer_not/src/main.nr index 0a5d276897a..f7c6a81031b 100644 --- a/test_programs/formal_verify_success/integer_not/src/main.nr +++ b/test_programs/formal_verify_success/integer_not/src/main.nr @@ -1,4 +1,4 @@ -#[requires((0 < x) & (x < 10))] +#['requires((0 < x) & (x < 10))] fn main(x: i64) { let _ = integer_i8(x as i8); let _ = integer_i16(x as i16); @@ -10,50 +10,50 @@ fn main(x: i64) { let _ = integer_u64(x as u64); } -#[requires((0 < x) & (x < 10))] -#[ensures(result == ! x)] +#['requires((0 < x) & (x < 10))] +#['ensures(result == ! x)] fn integer_i8(x: i8) -> i8 { ! x } -#[requires((0 < x) & (x < 10))] -#[ensures(result == ! x)] +#['requires((0 < x) & (x < 10))] +#['ensures(result == ! x)] fn integer_i16(x: i16) -> i16 { ! x } -#[requires((0 < x) & (x < 10))] -#[ensures(result == ! x)] +#['requires((0 < x) & (x < 10))] +#['ensures(result == ! x)] fn integer_i32(x: i32) -> i32 { ! x } -#[requires((0 < x) & (x < 10))] -#[ensures(result == ! x)] +#['requires((0 < x) & (x < 10))] +#['ensures(result == ! x)] fn integer_i64(x: i64) -> i64 { ! x } -#[requires(x < 10)] -#[ensures(result == ! x)] +#['requires(x < 10)] +#['ensures(result == ! x)] fn integer_u8(x: u8) -> u8 { ! x } -#[requires(x < 10)] -#[ensures(result == ! x)] +#['requires(x < 10)] +#['ensures(result == ! x)] fn integer_u16(x: u16) -> u16 { ! x } -#[requires(x < 10)] -#[ensures(result == ! x)] +#['requires(x < 10)] +#['ensures(result == ! x)] fn integer_u32(x: u32) -> u32 { ! x } -#[requires(x < 10)] -#[ensures(result == ! x)] +#['requires(x < 10)] +#['ensures(result == ! x)] fn integer_u64(x: u64) -> u64 { ! x } diff --git a/test_programs/formal_verify_success/integer_or/src/main.nr b/test_programs/formal_verify_success/integer_or/src/main.nr index 858d036a08c..358aacd6bea 100644 --- a/test_programs/formal_verify_success/integer_or/src/main.nr +++ b/test_programs/formal_verify_success/integer_or/src/main.nr @@ -9,42 +9,42 @@ fn main(x: i64, y: i64) { let _ = integer_u64(x as u64, y as u64); } -#[ensures(result == x | y)] +#['ensures(result == x | y)] fn integer_i8(x: i8, y: i8) -> i8 { x | y } -#[ensures(result == x | y)] +#['ensures(result == x | y)] fn integer_i16(x: i16, y: i16) -> i16 { x | y } -#[ensures(result == x | y)] +#['ensures(result == x | y)] fn integer_i32(x: i32, y: i32) -> i32 { x | y } -#[ensures(result == x | y)] +#['ensures(result == x | y)] fn integer_i64(x: i64, y: i64) -> i64 { x | y } -#[ensures(result == x | y)] +#['ensures(result == x | y)] fn integer_u8(x: u8, y: u8) -> u8 { x | y } -#[ensures(result == x | y)] +#['ensures(result == x | y)] fn integer_u16(x: u16, y: u16) -> u16 { x | y } -#[ensures(result == x | y)] +#['ensures(result == x | y)] fn integer_u32(x: u32, y: u32) -> u32 { x | y } -#[ensures(result == x | y)] +#['ensures(result == x | y)] fn integer_u64(x: u64, y: u64) -> u64 { x | y } diff --git a/test_programs/formal_verify_success/integer_sub/src/main.nr b/test_programs/formal_verify_success/integer_sub/src/main.nr index b98ffd375c2..4c9d619a4f1 100644 --- a/test_programs/formal_verify_success/integer_sub/src/main.nr +++ b/test_programs/formal_verify_success/integer_sub/src/main.nr @@ -1,4 +1,4 @@ -#[requires((10 < x) & (x < 100) & (0 < y) & (y < 10))] +#['requires((10 < x) & (x < 100) & (0 < y) & (y < 10))] fn main(x: i64, y: i64) { let _ = integer_i8(x as i8, y as i8); let _ = integer_i16(x as i16, y as i16); @@ -10,50 +10,50 @@ fn main(x: i64, y: i64) { let _ = integer_u64(x as u64, y as u64); } -#[requires((10 < x) & (x < 100) & (0 < y) & (y < 10))] -#[ensures(result == x - y)] +#['requires((10 < x) & (x < 100) & (0 < y) & (y < 10))] +#['ensures(result == x - y)] fn integer_i8(x: i8, y: i8) -> i8 { x - y } -#[requires((10 < x) & (x < 100) & (0 < y) & (y < 10))] -#[ensures(result == x - y)] +#['requires((10 < x) & (x < 100) & (0 < y) & (y < 10))] +#['ensures(result == x - y)] fn integer_i16(x: i16, y: i16) -> i16 { x - y } -#[requires((10 < x) & (x < 100) & (0 < y) & (y < 10))] -#[ensures(result == x - y)] +#['requires((10 < x) & (x < 100) & (0 < y) & (y < 10))] +#['ensures(result == x - y)] fn integer_i32(x: i32, y: i32) -> i32 { x - y } -#[requires((10 < x) & (x < 100) & (0 < y) & (y < 10))] -#[ensures(result == x - y)] +#['requires((10 < x) & (x < 100) & (0 < y) & (y < 10))] +#['ensures(result == x - y)] fn integer_i64(x: i64, y: i64) -> i64 { x - y } -#[requires((10 < x) & (x < 100) & (y < 10))] -#[ensures(result == x - y)] +#['requires((10 < x) & (x < 100) & (y < 10))] +#['ensures(result == x - y)] fn integer_u8(x: u8, y: u8) -> u8 { x - y } -#[requires((10 < x) & (x < 100) & (y < 10))] -#[ensures(result == x - y)] +#['requires((10 < x) & (x < 100) & (y < 10))] +#['ensures(result == x - y)] fn integer_u16(x: u16, y: u16) -> u16 { x - y } -#[requires((10 < x) & (x < 100) & (y < 10))] -#[ensures(result == x - y)] +#['requires((10 < x) & (x < 100) & (y < 10))] +#['ensures(result == x - y)] fn integer_u32(x: u32, y: u32) -> u32 { x - y } -#[requires((10 < x) & (x < 100) & (y < 10))] -#[ensures(result == x - y)] +#['requires((10 < x) & (x < 100) & (y < 10))] +#['ensures(result == x - y)] fn integer_u64(x: u64, y: u64) -> u64 { x - y } diff --git a/test_programs/formal_verify_success/integer_sum/src/main.nr b/test_programs/formal_verify_success/integer_sum/src/main.nr index fa6d8cb178d..f02898da06f 100644 --- a/test_programs/formal_verify_success/integer_sum/src/main.nr +++ b/test_programs/formal_verify_success/integer_sum/src/main.nr @@ -1,4 +1,4 @@ -#[requires((0 < x) & (x < 10) & (0 < y) & (y < 10))] +#['requires((0 < x) & (x < 10) & (0 < y) & (y < 10))] fn main(x: u64, y: u64) { let _ = integer_i8(x as i8, y as i8); let _ = integer_i16(x as i16, y as i16); @@ -10,50 +10,50 @@ fn main(x: u64, y: u64) { let _ = integer_u64(x, y); } -#[requires((0 < x) & (x < 10) & (0 < y) & (y < 10))] -#[ensures(result == x + y)] +#['requires((0 < x) & (x < 10) & (0 < y) & (y < 10))] +#['ensures(result == x + y)] fn integer_i8(x: i8, y: i8) -> i8 { x + y } -#[requires((0 < x) & (x < 10) & (0 < y) & (y < 10))] -#[ensures(result == x + y)] +#['requires((0 < x) & (x < 10) & (0 < y) & (y < 10))] +#['ensures(result == x + y)] fn integer_i16(x: i16, y: i16) -> i16 { x + y } -#[requires((0 < x) & (x < 10) & (0 < y) & (y < 10))] -#[ensures(result == x + y)] +#['requires((0 < x) & (x < 10) & (0 < y) & (y < 10))] +#['ensures(result == x + y)] fn integer_i32(x: i32, y: i32) -> i32 { x + y } -#[requires((0 < x) & (x < 10) & (0 < y) & (y < 10))] -#[ensures(result == x + y)] +#['requires((0 < x) & (x < 10) & (0 < y) & (y < 10))] +#['ensures(result == x + y)] fn integer_i64(x: i64, y: i64) -> i64 { x + y } -#[requires((x < 10) & (y < 10))] -#[ensures(result == x + y)] +#['requires((x < 10) & (y < 10))] +#['ensures(result == x + y)] fn integer_u8(x: u8, y: u8) -> u8 { x + y } -#[requires((x < 10) & (y < 10))] -#[ensures(result == x + y)] +#['requires((x < 10) & (y < 10))] +#['ensures(result == x + y)] fn integer_u16(x: u16, y: u16) -> u16 { x + y } -#[requires((x < 10) & (y < 10))] -#[ensures(result == x + y)] +#['requires((x < 10) & (y < 10))] +#['ensures(result == x + y)] fn integer_u32(x: u32, y: u32) -> u32 { x + y } -#[requires((x < 10) & (y < 10))] -#[ensures(result == x + y)] +#['requires((x < 10) & (y < 10))] +#['ensures(result == x + y)] fn integer_u64(x: u64, y: u64) -> u64 { x + y } diff --git a/test_programs/formal_verify_success/integer_xor/src/main.nr b/test_programs/formal_verify_success/integer_xor/src/main.nr index eacffbb7078..4c479d874e6 100644 --- a/test_programs/formal_verify_success/integer_xor/src/main.nr +++ b/test_programs/formal_verify_success/integer_xor/src/main.nr @@ -9,42 +9,42 @@ fn main(x: i64, y: i64) { let _ = integer_u64(x as u64, y as u64); } -#[ensures(result == x ^ y)] +#['ensures(result == x ^ y)] fn integer_i8(x: i8, y: i8) -> i8 { x ^ y } -#[ensures(result == x ^ y)] +#['ensures(result == x ^ y)] fn integer_i16(x: i16, y: i16) -> i16 { x ^ y } -#[ensures(result == x ^ y)] +#['ensures(result == x ^ y)] fn integer_i32(x: i32, y: i32) -> i32 { x ^ y } -#[ensures(result == x ^ y)] +#['ensures(result == x ^ y)] fn integer_i64(x: i64, y: i64) -> i64 { x ^ y } -#[ensures(result == x ^ y)] +#['ensures(result == x ^ y)] fn integer_u8(x: u8, y: u8) -> u8 { x ^ y } -#[ensures(result == x ^ y)] +#['ensures(result == x ^ y)] fn integer_u16(x: u16, y: u16) -> u16 { x ^ y } -#[ensures(result == x ^ y)] +#['ensures(result == x ^ y)] fn integer_u32(x: u32, y: u32) -> u32 { x ^ y } -#[ensures(result == x ^ y)] +#['ensures(result == x ^ y)] fn integer_u64(x: u64, y: u64) -> u64 { x ^ y } diff --git a/test_programs/formal_verify_success/is_even/src/main.nr b/test_programs/formal_verify_success/is_even/src/main.nr index f11a3ff2768..77f8d2c241d 100644 --- a/test_programs/formal_verify_success/is_even/src/main.nr +++ b/test_programs/formal_verify_success/is_even/src/main.nr @@ -1,7 +1,7 @@ -#[requires((x % 2 == 0) & (z % 2 == 0) +#['requires((x % 2 == 0) & (z % 2 == 0) & (x < z ) & (z < 1000))] -#[ensures(result == 0)] +#['ensures(result == 0)] fn main(x: u32, z: u32) -> pub u32 { let mut y = x + z; y % 2 diff --git a/test_programs/formal_verify_success/is_power_of_2/src/main.nr b/test_programs/formal_verify_success/is_power_of_2/src/main.nr index b3468773c3e..8ad18c6c1b2 100644 --- a/test_programs/formal_verify_success/is_power_of_2/src/main.nr +++ b/test_programs/formal_verify_success/is_power_of_2/src/main.nr @@ -1,4 +1,4 @@ -#[ghost] +#['ghost] fn is_power_of_2(x: i32) -> bool { if x <= 0 { false @@ -7,8 +7,8 @@ fn is_power_of_2(x: i32) -> bool { } } -#[requires(is_power_of_2(arr[0]))] -#[ensures(is_power_of_2(result))] +#['requires(is_power_of_2(arr[0]))] +#['ensures(is_power_of_2(result))] fn main(arr: [i32; 3]) -> pub i32 { arr[0] } diff --git a/test_programs/formal_verify_success/lhs_tuple_access/src/main.nr b/test_programs/formal_verify_success/lhs_tuple_access/src/main.nr index 31216a63d71..be6079e625a 100644 --- a/test_programs/formal_verify_success/lhs_tuple_access/src/main.nr +++ b/test_programs/formal_verify_success/lhs_tuple_access/src/main.nr @@ -1,4 +1,4 @@ -#[ensures(result.1 == x)] +#['ensures(result.1 == x)] fn main(x: u8) -> pub (u8, u8) { let mut y = (3, 5); y.1 = x; diff --git a/test_programs/formal_verify_success/mutate_array_of_tuples/src/main.nr b/test_programs/formal_verify_success/mutate_array_of_tuples/src/main.nr index 5520bafc886..49455b34703 100644 --- a/test_programs/formal_verify_success/mutate_array_of_tuples/src/main.nr +++ b/test_programs/formal_verify_success/mutate_array_of_tuples/src/main.nr @@ -1,6 +1,6 @@ -#[requires(x[3].0 == -2)] -#[requires(i < 5)] -#[ensures(result[i].1 == y)] +#['requires(x[3].0 == -2)] +#['requires(i < 5)] +#['ensures(result[i].1 == y)] fn main(mut x: [(i32, u32); 5], i: u32, y: u32) -> pub [(i32, u32); 5] { x[i].1 = y; x diff --git a/test_programs/formal_verify_success/non_full_path_global_var/Nargo.toml b/test_programs/formal_verify_success/non_full_path_global_var/Nargo.toml new file mode 100644 index 00000000000..b9e0dfb8f2f --- /dev/null +++ b/test_programs/formal_verify_success/non_full_path_global_var/Nargo.toml @@ -0,0 +1,7 @@ +[package] +name = "non_full_path_global_var" +type = "bin" +authors = [""] + +[dependencies] +fv_std = { path = "../../../fv_std" } diff --git a/test_programs/formal_verify_success/non_full_path_global_var/src/main.nr b/test_programs/formal_verify_success/non_full_path_global_var/src/main.nr new file mode 100644 index 00000000000..47b32b07f74 --- /dev/null +++ b/test_programs/formal_verify_success/non_full_path_global_var/src/main.nr @@ -0,0 +1,6 @@ +use fv_std::U8_MIN; + +#['ensures(U8_MIN == result)] +fn main() -> pub u8 { + 0 +} diff --git a/test_programs/formal_verify_success/operation_comutativity/src/main.nr b/test_programs/formal_verify_success/operation_comutativity/src/main.nr index fbda307da46..efbef804a09 100644 --- a/test_programs/formal_verify_success/operation_comutativity/src/main.nr +++ b/test_programs/formal_verify_success/operation_comutativity/src/main.nr @@ -1,17 +1,17 @@ -#[requires(x < 127)] +#['requires(x < 127)] fn main(x: u8) { let _ = left(x); let _ = right(x); } -#[requires(x <= 126)] -#[ensures(result == ((x + 1) * 2))] +#['requires(x <= 126)] +#['ensures(result == ((x + 1) * 2))] fn left(x: u8) -> u8 { (x + 1) * 2 } -#[requires(x <= 126)] -#[ensures(result == (2 * (x + 1)))] +#['requires(x <= 126)] +#['ensures(result == (2 * (x + 1)))] fn right(x: u8) -> u8 { (x + 1) * 2 } diff --git a/test_programs/formal_verify_success/shadow_global_const/Nargo.toml b/test_programs/formal_verify_success/shadow_global_const/Nargo.toml new file mode 100644 index 00000000000..d081e36529e --- /dev/null +++ b/test_programs/formal_verify_success/shadow_global_const/Nargo.toml @@ -0,0 +1,6 @@ +[package] +name = "shadow_global_const" +type = "bin" +authors = [""] + +[dependencies] \ No newline at end of file diff --git a/test_programs/formal_verify_success/shadow_global_const/src/main.nr b/test_programs/formal_verify_success/shadow_global_const/src/main.nr new file mode 100644 index 00000000000..ad87985f671 --- /dev/null +++ b/test_programs/formal_verify_success/shadow_global_const/src/main.nr @@ -0,0 +1,8 @@ +global x: u32 = 4; + +// We are showing that 'x' here will be resolved as the parameter x of +// function `main` and not the global variable `x`. +#['ensures(result == x / 2)] +fn main(x: u32) -> pub u32 { + x / 2 +} diff --git a/test_programs/formal_verify_success/struct/src/main.nr b/test_programs/formal_verify_success/struct/src/main.nr index 49270bb3c50..10a6d3b3876 100644 --- a/test_programs/formal_verify_success/struct/src/main.nr +++ b/test_programs/formal_verify_success/struct/src/main.nr @@ -1,7 +1,9 @@ -struct A { x: u8, y: u8 } +struct A { x: u8, y: u8, w: B } -#[requires((a.x < 10) & (a.y < 10))] -#[ensures((result.x == a.x + a.y) & (result.y == a.y))] +struct B { z: u32 } + +#['requires((a.x < 10) & (a.y < 10))] +#['ensures((result.x == a.x + a.y) & (result.y == a.y))] fn main(a: A) -> pub A { - A { x: a.x + a.y, y: a.y } + A { x: a.x + a.y, y: a.y, w: B {z: 5} } } diff --git a/test_programs/formal_verify_success/struct_return/src/main.nr b/test_programs/formal_verify_success/struct_return/src/main.nr index a10f65455f3..9897974caf5 100644 --- a/test_programs/formal_verify_success/struct_return/src/main.nr +++ b/test_programs/formal_verify_success/struct_return/src/main.nr @@ -3,20 +3,20 @@ struct A { y: u32, } -#[requires(x < 1000)] -#[ensures((result.x == x + 1) & (result.y == x + 2))] +#['requires(x < 1000)] +#['ensures((result.x == x + 1) & (result.y == x + 2))] fn f(x: u32) -> A { A { x: x + 1, y: x + 2 } } -#[requires(x < 1000)] -#[ensures((result.x == x + 2) & (result.y == x + 1))] +#['requires(x < 1000)] +#['ensures((result.x == x + 2) & (result.y == x + 1))] fn g(x: u32) -> A { let res = f(x); A { x: res.y, y: res.x } } -#[ensures(result == 13)] +#['ensures(result == 13)] fn main() -> pub u32 { let A { x, y } = g(5); x + y diff --git a/test_programs/formal_verify_success/struct_return_basic/src/main.nr b/test_programs/formal_verify_success/struct_return_basic/src/main.nr index f864789bbdb..9ef2cd157e2 100644 --- a/test_programs/formal_verify_success/struct_return_basic/src/main.nr +++ b/test_programs/formal_verify_success/struct_return_basic/src/main.nr @@ -3,7 +3,7 @@ struct A { y: u32, } -#[ensures(result == 3)] +#['ensures(result == 3)] fn main() -> pub u32 { let A { x, y } = A {x: 1, y: 2}; x + y diff --git a/test_programs/formal_verify_success/tmp b/test_programs/formal_verify_success/tmp deleted file mode 100644 index 15589fc767c..00000000000 --- a/test_programs/formal_verify_success/tmp +++ /dev/null @@ -1,26 +0,0 @@ - array_as_result_global ../../fix_those_tests - array_let_var_in_trigger ../../fix_those_tests - array_set_complex_composite_type ../../fix_those_tests - array_set_composite_types_1 ../../fix_those_tests - array_set_composite_types_2 ../../fix_those_tests - array_set_composite_types_3 ../../fix_those_tests - binary_search_v1 ../../fix_those_tests - binary_search_v2 ../../fix_those_tests - exists_big_element_sum ../../fix_those_tests - exists_zero_in_array ../../fix_those_tests - field_minus_one_is_max ../../fix_those_tests - forall_max_is_max ../../fix_those_tests - forall_structure ../../fix_those_tests - forall_sum_of_evens ../../fix_those_tests - generics ../../fix_those_tests - inline_functions_in_attributes ../../fix_those_tests - inline_tuple_returning_func ../../fix_those_tests - integer_and ../../fix_those_tests - integer_or ../../fix_those_tests - integer_xor ../../fix_those_tests - is_power_of_2 ../../fix_those_tests - is_sorted_no_quant ../../fix_those_tests - load_store_instructions ../../fix_those_tests - self_in_annotation ../../fix_those_tests - struct_return ../../fix_those_tests - tuple_return ../../fix_those_tests diff --git a/test_programs/formal_verify_success/tuple_deconstruct/src/main.nr b/test_programs/formal_verify_success/tuple_deconstruct/src/main.nr index 3b26b63eaa3..2443e0e5da3 100644 --- a/test_programs/formal_verify_success/tuple_deconstruct/src/main.nr +++ b/test_programs/formal_verify_success/tuple_deconstruct/src/main.nr @@ -1,4 +1,4 @@ -#[ensures(result == 1)] +#['ensures(result == 1)] fn main() -> pub u32 { let (a, b) = (1, 2); a diff --git a/test_programs/formal_verify_success/tuple_deconstruct_2/src/main.nr b/test_programs/formal_verify_success/tuple_deconstruct_2/src/main.nr index 9b4b89fe998..710d4b446b3 100644 --- a/test_programs/formal_verify_success/tuple_deconstruct_2/src/main.nr +++ b/test_programs/formal_verify_success/tuple_deconstruct_2/src/main.nr @@ -1,4 +1,4 @@ -#[ensures(result == 5)] +#['ensures(result == 5)] fn main() -> pub u32 { let (a, b) = (1, 2); let (c, d) = (3, 4); diff --git a/test_programs/formal_verify_success/tuple_return/src/main.nr b/test_programs/formal_verify_success/tuple_return/src/main.nr index 93ea288448e..8810c30fa9a 100644 --- a/test_programs/formal_verify_success/tuple_return/src/main.nr +++ b/test_programs/formal_verify_success/tuple_return/src/main.nr @@ -1,17 +1,17 @@ -#[requires(x < 1000)] -#[ensures((result.0 == x + 1) & (result.1 == x + 2) & (result.2 == x + 3))] +#['requires(x < 1000)] +#['ensures((result.0 == x + 1) & (result.1 == x + 2) & (result.2 == x + 3))] fn f(x: u32) -> (u32, u32, u32) { (x + 1, x + 2, x + 3) } -#[requires(x < 1000)] -#[ensures((result.0 == x + 3) & (result.1 == x + 1) & (result.2 == x + 2))] +#['requires(x < 1000)] +#['ensures((result.0 == x + 3) & (result.1 == x + 1) & (result.2 == x + 2))] fn g(x: u32) -> (u32, u32, u32) { let res = f(x); (res.2, res.0, res.1) } -#[ensures(result == 7)] +#['ensures(result == 7)] fn main() -> pub u32 { let (a, b, c) = g(5); a + b - c diff --git a/test_programs/formal_verify_success/tuple_return_basic/src/main.nr b/test_programs/formal_verify_success/tuple_return_basic/src/main.nr index a8a17b602f8..d7c4c9ae920 100644 --- a/test_programs/formal_verify_success/tuple_return_basic/src/main.nr +++ b/test_programs/formal_verify_success/tuple_return_basic/src/main.nr @@ -1,10 +1,10 @@ -#[requires(x < 1000)] -#[ensures((result.0 == x + 1) & (result.1 == x + 2) & (result.2 == x + 3))] +#['requires(x < 1000)] +#['ensures((result.0 == x + 1) & (result.1 == x + 2) & (result.2 == x + 3))] fn f(x: u32) -> (u32, u32, u32) { (x + 1, x + 2, x + 3) } -#[ensures(result == 5)] +#['ensures(result == 5)] fn main() -> pub u32 { let (a, b, c) = f(5); a + b - c diff --git a/test_programs/formal_verify_success/tuples/src/main.nr b/test_programs/formal_verify_success/tuples/src/main.nr index 3168ea9757d..e2b4267fd34 100644 --- a/test_programs/formal_verify_success/tuples/src/main.nr +++ b/test_programs/formal_verify_success/tuples/src/main.nr @@ -1,5 +1,5 @@ -#[requires((x.0 < 10) & (x.2 < 10))] -#[ensures((result.0 == x.0) & (result.2 == x.2 + x.0))] +#['requires((x.0 < 10) & (x.2 < 10))] +#['ensures((result.0 == x.0) & (result.2 == x.2 + x.0))] fn main(x: (u8, Field, u8)) -> pub (u8, Field, u8) { (x.0, x.1, x.2 + x.0) } diff --git a/tooling/nargo_cli/Cargo.toml b/tooling/nargo_cli/Cargo.toml index ee6da9fe1fe..b9539288d10 100644 --- a/tooling/nargo_cli/Cargo.toml +++ b/tooling/nargo_cli/Cargo.toml @@ -87,6 +87,10 @@ tracing-appender = "0.2.3" clap_complete = "4.5.36" fs2 = "0.4.3" +# Formal Verification +fv_bridge.workspace = true +vir.workspace = true + [target.'cfg(not(unix))'.dependencies] tokio-util = { version = "0.7.8", features = ["compat"] } diff --git a/tooling/nargo_cli/build.rs b/tooling/nargo_cli/build.rs index 33b324c175c..36c5d3fe3d1 100644 --- a/tooling/nargo_cli/build.rs +++ b/tooling/nargo_cli/build.rs @@ -901,6 +901,7 @@ fn formal_verify_success_{test_name}() {{ let mut cmd = Command::cargo_bin("nargo").unwrap(); cmd.arg("--program-dir").arg(test_program_dir); cmd.arg("formal-verify"); + cmd.arg("--new-syntax"); cmd.assert().success(); }} @@ -929,6 +930,7 @@ fn formal_verify_failure_{test_name}() {{ let mut cmd = Command::cargo_bin("nargo").unwrap(); cmd.arg("--program-dir").arg(test_program_dir); cmd.arg("formal-verify"); + cmd.arg("--new-syntax"); cmd.assert().failure().stderr( predicate::str::contains("The application panicked (crashed).") @@ -961,4 +963,4 @@ fn formal_verify_failure_{test_name}() {{ ) .expect("Could not write templated test file."); } -} \ No newline at end of file +} diff --git a/tooling/nargo_cli/src/cli/fv_cmd.rs b/tooling/nargo_cli/src/cli/fv_cmd.rs index df95527b485..b7914e4ff2a 100644 --- a/tooling/nargo_cli/src/cli/fv_cmd.rs +++ b/tooling/nargo_cli/src/cli/fv_cmd.rs @@ -5,12 +5,14 @@ use std::{ use clap::Args; use fm::{FileId, FileManager, FileMap}; +use fv_bridge::compile_and_build_vir_krate; use nargo::{ops::report_errors, prepare_package, workspace::Workspace}; use nargo_toml::PackageSelection; -use noirc_driver::{CompileOptions, CompiledProgram, link_to_debug_crate}; +use noirc_driver::{CompileOptions, link_to_debug_crate}; use noirc_errors::{CustomDiagnostic, DiagnosticKind, Location, Span, reporter::ReportedErrors}; use noirc_frontend::debug::DebugInstrumenter; use serde::Deserialize; +use vir::ast::Krate; use crate::{cli::compile_cmd::parse_workspace, errors::CliError}; @@ -31,6 +33,10 @@ pub(crate) struct FormalVerifyCommand { #[arg(long, hide = true)] pub show_vir: bool, + /// Use the new syntax for FV annotations + #[arg(long)] + pub new_syntax: bool, + // Flags which will be propagated to the Venir binary #[clap(last = true)] venir_flags: Vec, @@ -58,24 +64,39 @@ pub(crate) fn run(args: FormalVerifyCommand, workspace: Workspace) -> Result<(), context.package_build_path = workspace.package_build_path(package); context.perform_formal_verification = true; - let compiled_program = - noirc_driver::compile_main(&mut context, crate_id, &args.compile_options, None); - - // We want to formally verify only compilable programs - let compiled_program = report_errors( - compiled_program, - &workspace_file_manager, - args.compile_options.deny_warnings, - true, // We don't want to report compile related warnings - )?; - + let krate: Krate = if args.new_syntax { + // Compile with new syntax and report errors + report_errors( + compile_and_build_vir_krate(&mut context, crate_id, &args.compile_options), + &workspace_file_manager, + args.compile_options.deny_warnings, + true, + )? + } else { + // Compile with old syntax, report errors, then extract and unwrap VIR + let compiled = report_errors( + noirc_driver::compile_main(&mut context, crate_id, &args.compile_options, None), + &workspace_file_manager, + args.compile_options.deny_warnings, + true, + )?; + + let vir_result = compiled.verus_vir + .ok_or_else(|| CliError::Generic("Failed to generate VIR with no specific error".into()))?; + + let krate = vir_result.map_err(|e| CliError::Generic(e.to_string()))?; + + krate + }; + + // Shared post-processing if args.show_vir { println!("Generated VIR:"); - println!("{:#?}", compiled_program.verus_vir); + println!("{:#?}", krate); } - + z3_verify( - compiled_program, + krate, &workspace_file_manager, args.compile_options.deny_warnings, &args.venir_flags, @@ -88,18 +109,11 @@ pub(crate) fn run(args: FormalVerifyCommand, workspace: Workspace) -> Result<(), /// Runs the Venir binary and passes the compiled program in VIR format to it /// Reports all errors produced during Venir (SMT solver) verification fn z3_verify( - compiled_program: CompiledProgram, + krate: Krate, workspace_file_manager: &FileManager, deny_warnings: bool, venir_args: &Vec, ) -> Result<(), CliError> { - let krate = compiled_program - .verus_vir - .ok_or_else(|| { - CliError::Generic(String::from("Failed to generate VIR with no specific error")) - })? - .map_err(|e| CliError::Generic(e.to_string()))?; - let serialized_vir_krate = serde_json::to_string(&krate).expect("Failed to serialize"); // Run the Venir binary which is used for verifying the vir_krate input.