Skip to content
New issue

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

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

Already on GitHub? Sign in to your account

feat: Arithmetic Generics #5950

Merged
merged 8 commits into from
Sep 6, 2024
Merged
Show file tree
Hide file tree
Changes from 2 commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions aztec_macros/src/utils/hir_utils.rs
Original file line number Diff line number Diff line change
Expand Up @@ -195,7 +195,7 @@
let trait_id = None;
items.functions.push(UnresolvedFunctions { file_id, functions, trait_id, self_type: None });

let mut errors = Elaborator::elaborate(context, *crate_id, items, None, false);
let mut errors = Elaborator::elaborate(context, *crate_id, items, None);
errors.retain(|(error, _)| !CustomDiagnostic::from(error).is_warning());

if !errors.is_empty() {
Expand Down Expand Up @@ -241,7 +241,7 @@
let mut items = CollectedItems::default();
items.globals.push(UnresolvedGlobal { file_id, module_id, global_id, stmt_def: global });

let _errors = Elaborator::elaborate(context, *crate_id, items, None, false);
let _errors = Elaborator::elaborate(context, *crate_id, items, None);
}

pub fn fully_qualified_note_path(context: &HirContext, note_id: StructId) -> Option<String> {
Expand Down Expand Up @@ -335,7 +335,7 @@
}
}

pub fn get_global_numberic_const(

Check warning on line 338 in aztec_macros/src/utils/hir_utils.rs

View workflow job for this annotation

GitHub Actions / Code

Unknown word (numberic)
context: &HirContext,
const_name: &str,
) -> Result<u128, MacroError> {
Expand Down
5 changes: 0 additions & 5 deletions compiler/noirc_driver/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -120,10 +120,6 @@ pub struct CompileOptions {
#[arg(long, hide = true)]
pub show_artifact_paths: bool,

/// Temporary flag to enable the experimental arithmetic generics feature
#[arg(long, hide = true)]
pub arithmetic_generics: bool,

/// Flag to turn off the compiler check for under constrained values.
/// Warning: This can improve compilation speed but can also lead to correctness errors.
/// This check should always be run on production code.
Expand Down Expand Up @@ -289,7 +285,6 @@ pub fn check_crate(
crate_id,
context,
options.debug_comptime_in_file.as_deref(),
options.arithmetic_generics,
error_on_unused_imports,
macros,
);
Expand Down
1 change: 0 additions & 1 deletion compiler/noirc_frontend/src/elaborator/comptime.rs
Original file line number Diff line number Diff line change
Expand Up @@ -64,7 +64,6 @@ impl<'context> Elaborator<'context> {
self.def_maps,
self.crate_id,
self.debug_comptime_in_file,
self.enable_arithmetic_generics,
self.interpreter_call_stack.clone(),
);

Expand Down
25 changes: 2 additions & 23 deletions compiler/noirc_frontend/src/elaborator/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -29,7 +29,7 @@
DefinitionKind, DependencyId, ExprId, FuncId, FunctionModifiers, GlobalId, ReferenceId,
TraitId, TypeAliasId,
},
token::CustomAtrribute,

Check warning on line 32 in compiler/noirc_frontend/src/elaborator/mod.rs

View workflow job for this annotation

GitHub Actions / Code

Unknown word (Atrribute)
Shared, Type, TypeVariable,
};
use crate::{
Expand Down Expand Up @@ -168,9 +168,6 @@
/// they are elaborated (e.g. in a function's type or another global's RHS).
unresolved_globals: BTreeMap<GlobalId, UnresolvedGlobal>,

/// Temporary flag to enable the experimental arithmetic generics feature
enable_arithmetic_generics: bool,

pub(crate) interpreter_call_stack: im::Vector<Location>,
}

Expand All @@ -194,7 +191,6 @@
def_maps: &'context mut DefMaps,
crate_id: CrateId,
debug_comptime_in_file: Option<FileId>,
enable_arithmetic_generics: bool,
interpreter_call_stack: im::Vector<Location>,
) -> Self {
Self {
Expand All @@ -217,7 +213,6 @@
current_trait_impl: None,
debug_comptime_in_file,
unresolved_globals: BTreeMap::new(),
enable_arithmetic_generics,
current_trait: None,
interpreter_call_stack,
}
Expand All @@ -227,14 +222,12 @@
context: &'context mut Context,
crate_id: CrateId,
debug_comptime_in_file: Option<FileId>,
enable_arithmetic_generics: bool,
) -> Self {
Self::new(
&mut context.def_interner,
&mut context.def_maps,
crate_id,
debug_comptime_in_file,
enable_arithmetic_generics,
im::Vector::new(),
)
}
Expand All @@ -244,31 +237,17 @@
crate_id: CrateId,
items: CollectedItems,
debug_comptime_in_file: Option<FileId>,
enable_arithmetic_generics: bool,
) -> Vec<(CompilationError, FileId)> {
Self::elaborate_and_return_self(
context,
crate_id,
items,
debug_comptime_in_file,
enable_arithmetic_generics,
)
.errors
Self::elaborate_and_return_self(context, crate_id, items, debug_comptime_in_file).errors
}

pub fn elaborate_and_return_self(
context: &'context mut Context,
crate_id: CrateId,
items: CollectedItems,
debug_comptime_in_file: Option<FileId>,
enable_arithmetic_generics: bool,
) -> Self {
let mut this = Self::from_context(
context,
crate_id,
debug_comptime_in_file,
enable_arithmetic_generics,
);
let mut this = Self::from_context(context, crate_id, debug_comptime_in_file);
this.elaborate_items(items);
this.check_and_pop_function_context();
this
Expand Down Expand Up @@ -816,7 +795,7 @@
let attributes = func.secondary_attributes().iter();
let attributes =
attributes.filter_map(|secondary_attribute| secondary_attribute.as_custom());
let attributes: Vec<CustomAtrribute> = attributes.cloned().collect();

Check warning on line 798 in compiler/noirc_frontend/src/elaborator/mod.rs

View workflow job for this annotation

GitHub Actions / Code

Unknown word (Atrribute)

let meta = FuncMeta {
name: name_ident,
Expand Down
11 changes: 1 addition & 10 deletions compiler/noirc_frontend/src/elaborator/types.rs
Original file line number Diff line number Diff line change
Expand Up @@ -450,7 +450,6 @@ impl<'context> Elaborator<'context> {
}
UnresolvedTypeExpression::Constant(int, _) => Type::Constant(int),
UnresolvedTypeExpression::BinaryOperation(lhs, op, rhs, span) => {
let (lhs_span, rhs_span) = (lhs.span(), rhs.span());
let lhs = self.convert_expression_type(*lhs);
let rhs = self.convert_expression_type(*rhs);

Expand All @@ -463,15 +462,7 @@ impl<'context> Elaborator<'context> {
Type::Error
}
}
(lhs, rhs) => {
if !self.enable_arithmetic_generics {
let span =
if !matches!(lhs, Type::Constant(_)) { lhs_span } else { rhs_span };
self.push_err(ResolverError::InvalidArrayLengthExpr { span });
}

Type::InfixExpr(Box::new(lhs), op, Box::new(rhs)).canonicalize()
}
(lhs, rhs) => Type::InfixExpr(Box::new(lhs), op, Box::new(rhs)).canonicalize(),
}
}
UnresolvedTypeExpression::AsTraitPath(path) => self.resolve_as_trait_path(*path),
Expand Down
11 changes: 2 additions & 9 deletions compiler/noirc_frontend/src/hir/def_collector/dc_crate.rs
Original file line number Diff line number Diff line change
Expand Up @@ -271,7 +271,6 @@ impl DefCollector {
ast: SortedModule,
root_file_id: FileId,
debug_comptime_in_file: Option<&str>,
enable_arithmetic_generics: bool,
error_on_unused_items: bool,
macro_processors: &[&dyn MacroProcessor],
) -> Vec<(CompilationError, FileId)> {
Expand All @@ -291,7 +290,6 @@ impl DefCollector {
dep.crate_id,
context,
debug_comptime_in_file,
enable_arithmetic_generics,
error_on_usage_tracker,
macro_processors,
));
Expand Down Expand Up @@ -471,13 +469,8 @@ impl DefCollector {
})
});

let mut more_errors = Elaborator::elaborate(
context,
crate_id,
def_collector.items,
debug_comptime_in_file,
enable_arithmetic_generics,
);
let mut more_errors =
Elaborator::elaborate(context, crate_id, def_collector.items, debug_comptime_in_file);

errors.append(&mut more_errors);

Expand Down
2 changes: 0 additions & 2 deletions compiler/noirc_frontend/src/hir/def_map/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -76,7 +76,6 @@ impl CrateDefMap {
crate_id: CrateId,
context: &mut Context,
debug_comptime_in_file: Option<&str>,
enable_arithmetic_generics: bool,
error_on_unused_imports: bool,
macro_processors: &[&dyn MacroProcessor],
) -> Vec<(CompilationError, FileId)> {
Expand Down Expand Up @@ -133,7 +132,6 @@ impl CrateDefMap {
ast,
root_file_id,
debug_comptime_in_file,
enable_arithmetic_generics,
error_on_unused_imports,
macro_processors,
));
Expand Down
99 changes: 93 additions & 6 deletions docs/docs/noir/concepts/generics.md
Original file line number Diff line number Diff line change
Expand Up @@ -45,17 +45,20 @@ fn main() {

The `print` function will print `Hello!` an arbitrary number of times, twice in this case.

## Numeric Generics

If we want to be generic over array lengths (which are type-level integers), we can use numeric
generics. Using these looks just like using regular generics, but these generics can resolve to
integers at compile-time, rather than resolving to types. Here's an example of a struct that is
generic over the size of the array it contains internally:
generics. Using these looks similar to using regular generics, but introducing them into scope
requires declaring them with `let MyGenericName: IntegerType`. This can be done anywhere a normal
generic is declared. Instead of types, these generics resolve to integers at compile-time.
Here's an example of a struct that is generic over the size of the array it contains internally:

```rust
struct BigInt<N> {
struct BigInt<let N: u32> {
limbs: [u32; N],
}

impl<N> BigInt<N> {
impl<let N: u32> BigInt<N> {
// `N` is in scope of all methods in the impl
fn first(first: BigInt<N>, second: BigInt<N>) -> Self {
assert(first.limbs != second.limbs);
Expand All @@ -77,7 +80,7 @@ This is what [traits](../concepts/traits.md) are for in Noir. Here's an example
any type `T` that implements the `Eq` trait for equality:

```rust
fn first_element_is_equal<T, N>(array1: [T; N], array2: [T; N]) -> bool
fn first_element_is_equal<T, let N: u32>(array1: [T; N], array2: [T; N]) -> bool
where T: Eq
{
if (array1.len() == 0) | (array2.len() == 0) {
Expand Down Expand Up @@ -161,3 +164,87 @@ fn example() {
assert(10 as u32 == foo.generic_method::<Field>());
}
```

## Arithmetic Generics

In addition to numeric generics, Noir also allows a limited form of arithmetic on generics.
When you have a numeric generic such as `N`, you can use the following operators on it in a
type position: `+`, `-`, `*`, `/`, and `%`.

Note that type checking arithmetic generics is a best effort guess from the compiler and there
are many cases of types that are equal that the compiler may not see as such. For example,
we know that `T * (N + M)` should be equal to `T*N + T*M` but the compiler does not currently
apply the distributive law and thus sees these as different types.

Even with this limitation though, the compiler can handle common cases decently well:

```rs
trait Serialize<let N: u32> {
fn serialize(self) -> [Field; N];
}

impl Serialize<1> for Field { .. }

impl<T, let N: u32, M: u32> Serialize<N * M> for [T; N]
where T: Serialize<M> { .. }

impl<T, U, let N: u32, M: u32> Serialize<N + M> for (T, U)
where T: Serialize<N>, U: Serialize<M> { .. }

fn main() {
let data = (1, [2, 3, 4]);
assert(data.serialize().len(), 4);
}
```

Note that if there is any over or underflow the types will fail to unify:

```rs
fn pop<let N: u32>(array: [Field; N]) -> [Field; N - 1] {
let mut result: [Field; N - 1] = std::mem::zeroed();
for i in 0 .. N {
result[i] = array[i];
}
result
}

fn main() {
// error: Could not determine array length `(0 - 1)`
pop([]);
}
```

This also applies if there is underflow in an intermediate calculation:

```rs
fn pop<let N: u32>(array: [Field; N]) -> [Field; N - 1] {
let mut result: [Field; N - 1] = std::mem::zeroed();
for i in 0 .. N {
result[i] = array[i];
}
result
}

fn push_zero<let N: u32>(array: [Field; N]) -> [Field; N + 1] {
let mut result: [Field; N + 1] = std::mem::zeroed();
for i in 0 .. N {
result[i] = array[i];
}
// index N is already zeroed
result
}

fn main() {
// From main it looks like there's nothing sketchy going on
seems_fine([]);
}

// Since `seems_fine` says it can receive and return any length N
fn seems_fine<let N: u32>(array: [Field; N]) -> [Field; N] {
// But inside `seems_fine` we pop from the array which
// requires the length to be greater than zero.

// error: Could not determine array length `(0 - 1)`
push_zero(pop(array))
}
```
2 changes: 1 addition & 1 deletion tooling/nargo_cli/build.rs
Original file line number Diff line number Diff line change
Expand Up @@ -218,7 +218,7 @@ fn generate_compile_success_empty_tests(test_file: &mut File, test_data_dir: &Pa
&test_dir,
&format!(
r#"
nargo.arg("info").arg("--arithmetic-generics").arg("--json").arg("--force");
nargo.arg("info").arg("--json").arg("--force");

{assert_zero_opcodes}"#,
),
Expand Down
Loading