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

chore: add compile-time assertions on generic arguments of stdlib functions #6981

Draft
wants to merge 10 commits into
base: master
Choose a base branch
from
Draft
5 changes: 3 additions & 2 deletions noir_stdlib/src/collections/bounded_vec.nr
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
use crate::{cmp::Eq, convert::From};
use crate::{cmp::Eq, convert::From, static_assert};

/// A `BoundedVec<T, MaxLen>` is a growable storage similar to a `Vec<T>` except that it
/// is bounded with a maximum possible length. Unlike `Vec`, `BoundedVec` is not implemented
Expand Down Expand Up @@ -339,7 +339,7 @@ impl<T, let MaxLen: u32> BoundedVec<T, MaxLen> {
/// let bounded_vec: BoundedVec<Field, 10> = BoundedVec::from_array([1, 2, 3])
/// ```
pub fn from_array<let Len: u32>(array: [T; Len]) -> Self {
assert(Len <= MaxLen, "from array out of bounds");
static_assert(Len <= MaxLen, "from array out of bounds");
let mut vec: BoundedVec<T, MaxLen> = BoundedVec::new();
vec.extend_from_array(array);
vec
Expand Down Expand Up @@ -612,6 +612,7 @@ mod bounded_vec_tests {
assert_eq(bounded_vec.get(2), 3);
}

// TODO: works with 'shoul_fail': does 'should_fail_with' support 'static_assert'?
#[test(should_fail_with = "from array out of bounds")]
fn max_len_lower_then_array_len() {
let _: BoundedVec<Field, 2> = BoundedVec::from_array([0; 3]);
Expand Down
13 changes: 11 additions & 2 deletions noir_stdlib/src/field/mod.nr
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We shouldn't split into safe and unsafe variants but instead have a check that the decomposition is canonical similar to how we do it for byte decompositions.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

  1. How would a check that the decomposition is canonical work at compile-time? I would expect to check that it's canonical in Add feature-gated runtime assertions to stdlib functions #6964
  2. R.e. avoiding splitting into safe and unsafe versions, do you mean to move these checks into the builtin function implementations?

Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
pub mod bn254;
use crate::runtime::is_unconstrained;
use crate::{runtime::is_unconstrained, static_assert};
use bn254::lt as bn254_lt;

impl Field {
Expand All @@ -10,13 +10,14 @@ impl Field {
// docs:start:assert_max_bit_size
pub fn assert_max_bit_size<let BIT_SIZE: u32>(self) {
// docs:end:assert_max_bit_size
assert(BIT_SIZE < modulus_num_bits() as u32);
static_assert(BIT_SIZE < modulus_num_bits() as u32, "BIT_SIZE must be less than modulus_num_bits");
self.__assert_max_bit_size(BIT_SIZE);
}

#[builtin(apply_range_constraint)]
fn __assert_max_bit_size(self, bit_size: u32) {}

// TODO: to_le_bits -> to_le_bits_unsafe
/// Decomposes `self` into its little endian bit decomposition as a `[u1; N]` array.
/// This slice will be zero padded should not all bits be necessary to represent `self`.
///
Expand All @@ -33,6 +34,7 @@ impl Field {
pub fn to_le_bits<let N: u32>(self: Self) -> [u1; N] {}
// docs:end:to_le_bits

// TODO: to_be_bits -> to_be_bits_unsafe
/// Decomposes `self` into its big endian bit decomposition as a `[u1; N]` array.
/// This array will be zero padded should not all bits be necessary to represent `self`.
///
Expand All @@ -49,6 +51,7 @@ impl Field {
pub fn to_be_bits<let N: u32>(self: Self) -> [u1; N] {}
// docs:end:to_be_bits

// TODO: static_assert for N
/// Decomposes `self` into its little endian byte decomposition as a `[u8;N]` array
/// This array will be zero padded should not all bytes be necessary to represent `self`.
///
Expand Down Expand Up @@ -82,6 +85,7 @@ impl Field {
bytes
}

// TODO: static_assert for N
/// Decomposes `self` into its big endian byte decomposition as a `[u8;N]` array of length required to represent the field modulus
/// This array will be zero padded should not all bytes be necessary to represent `self`.
///
Expand Down Expand Up @@ -135,10 +139,13 @@ impl Field {
}
// docs:end:to_be_radix

// TODO: static_assert for N
// `_radix` must be less than 256
#[builtin(to_le_radix)]
fn __to_le_radix<let N: u32>(self, radix: u32) -> [u8; N] {}

// TODO: static_assert for N
// TODO: is this also true? "`_radix` must be less than 256"
michaeljklein marked this conversation as resolved.
Show resolved Hide resolved
#[builtin(to_be_radix)]
fn __to_be_radix<let N: u32>(self, radix: u32) -> [u8; N] {}

Expand Down Expand Up @@ -169,6 +176,7 @@ impl Field {
}
}

// TODO: static_assert for N?
/// Convert a little endian byte array to a field element.
/// If the provided byte array overflows the field modulus then the Field will silently wrap around.
pub fn from_le_bytes<let N: u32>(bytes: [u8; N]) -> Field {
Expand All @@ -182,6 +190,7 @@ impl Field {
result
}

// TODO: static_assert for N?
/// Convert a big endian byte array to a field element.
/// If the provided byte array overflows the field modulus then the Field will silently wrap around.
pub fn from_be_bytes<let N: u32>(bytes: [u8; N]) -> Field {
Expand Down
3 changes: 2 additions & 1 deletion noir_stdlib/src/meta/ctstring.nr
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,8 @@ impl CtString {
"".as_ctstring()
}

// Bug: using &mut self as the object results in this method not being found
// TODO(https://github.com/noir-lang/noir/issues/6980): Bug: using &mut self
// as the object results in this method not being found
// docs:start:append_str
pub comptime fn append_str<let N: u32>(self, s: str<N>) -> Self {
// docs:end:append_str
Expand Down
6 changes: 4 additions & 2 deletions noir_stdlib/src/uint128.nr
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
use crate::cmp::{Eq, Ord, Ordering};
use crate::ops::{Add, BitAnd, BitOr, BitXor, Div, Mul, Not, Rem, Shl, Shr, Sub};
use crate::static_assert;
use super::convert::AsPrimitive;

global pow64: Field = 18446744073709551616; //2^64;
Expand Down Expand Up @@ -67,11 +68,12 @@ impl U128 {
}

pub fn from_hex<let N: u32>(hex: str<N>) -> U128 {
let N = N as u32;
// TODO cleanup if working
// let N = N as u32;
let bytes = hex.as_bytes();
// string must starts with "0x"
assert((bytes[0] == 48) & (bytes[1] == 120), "Invalid hexadecimal string");
assert(N < 35, "Input does not fit into a U128");
static_assert(N < 35, "Input does not fit into a U128");

let mut lo = 0;
let mut hi = 0;
Expand Down
Loading