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

fix: ensure to_bytes returns the canonical decomposition #6084

Merged
merged 19 commits into from
Oct 1, 2024
Merged
Show file tree
Hide file tree
Changes from 10 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
104 changes: 86 additions & 18 deletions noir_stdlib/src/field/mod.nr
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
mod bn254;
use bn254::lt as bn254_lt;
use crate::runtime::is_unconstrained;

impl Field {
/// Asserts that `self` can be represented in `bit_size` bits.
Expand Down Expand Up @@ -49,39 +50,69 @@ impl Field {
pub fn to_be_bits<let N: u32>(self: Self) -> [u1; N] {}
// docs:end:to_be_bits

/// Decomposes `self` into its little endian byte decomposition as a `[u8]` slice of length `byte_size`.
/// This slice will be zero padded should not all bytes be necessary to represent `self`.
/// 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`.
///
/// # Failures
/// Causes a constraint failure for `Field` values exceeding `2^{8*byte_size}` as the resulting slice will not
/// be able to represent the original `Field`.
/// The length N of the array must be big enough to contain all the bytes of the 'self',
/// and no more than the number of bytes required to represent the field modulus
///
/// # Safety
/// Values of `byte_size` equal to or greater than the number of bytes necessary to represent the `Field` modulus
/// (e.g. 32 for the BN254 field) allow for multiple byte decompositions. This is due to how the `Field` will
/// wrap around due to overflow when verifying the decomposition.
/// The result is ensured to be the canonical decomposition of the field element
// docs:start:to_le_bytes
pub fn to_le_bytes<let N: u32>(self: Self) -> [u8; N] {
self.to_le_radix(256)
// docs:end:to_le_bytes
// Compute the byte decomposition
let bytes = unsafe {
compute_byte_decomposition(self)
};
guipublic marked this conversation as resolved.
Show resolved Hide resolved

if !is_unconstrained() {
// Verify that the byte decomposition is correct
let mut y = 0;
let mut r = 1;
for i in 0..N {
y += (bytes[i] as Field)*r;
r *= 256;
}
assert_eq(self, y);
guipublic marked this conversation as resolved.
Show resolved Hide resolved

// Ensure that the byte decomposition does not overflow the modulus
let p = modulus_le_bytes();
assert(bytes.len() <= p.len());
let mut ok = bytes.len() != p.len();
for i in 0..N {
if !ok {
if (bytes[N - 1 - i] != p[N - 1 - i]) {
assert(bytes[N - 1 - i] < p[N - 1 - i]);
ok = true;
}
}
}
assert(ok);
TomAFrench marked this conversation as resolved.
Show resolved Hide resolved
}
bytes
}
// docs:end:to_le_bytes

/// Decomposes `self` into its big endian byte decomposition as a `[u8]` slice of length `byte_size`.
/// This slice will be zero padded should not all bytes be necessary to represent `self`.
/// 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`.
///
/// # Failures
/// Causes a constraint failure for `Field` values exceeding `2^{8*byte_size}` as the resulting slice will not
/// be able to represent the original `Field`.
/// The length N of the array must be big enough to contain all the bytes of the 'self',
/// and no more than the number of bytes required to represent the field modulus
///
/// # Safety
/// Values of `byte_size` equal to or greater than the number of bytes necessary to represent the `Field` modulus
/// (e.g. 32 for the BN254 field) allow for multiple byte decompositions. This is due to how the `Field` will
/// wrap around due to overflow when verifying the decomposition.
/// The result is ensured to be the canonical decomposition of the field element
// docs:start:to_be_bytes
pub fn to_be_bytes<let N: u32>(self: Self) -> [u8; N] {
self.to_be_radix(256)
// docs:end:to_be_bytes
let le_bytes: [u8; N] = self.to_le_bytes();
let mut be_bytes = [0; N];
for i in 0..N {
be_bytes[i] = le_bytes[N - 1 - i];
}
be_bytes
TomAFrench marked this conversation as resolved.
Show resolved Hide resolved
}
// docs:end:to_be_bytes

// docs:start:to_le_radix
pub fn to_le_radix<let N: u32>(self: Self, radix: u32) -> [u8; N] {
Expand Down Expand Up @@ -132,6 +163,30 @@ impl Field {
}
}

/// Convert a big endian byte array to a field element by modding
guipublic marked this conversation as resolved.
Show resolved Hide resolved
pub fn from_le_bytes<let N: u32>(bytes: [u8; N]) -> Field {
let mut v = 1;
let mut result = 0;

for i in 0..N {
result += (bytes[i] as Field) * v;
v = v * 256;
}
result
}

/// Convert a little endian byte array to a field element by modding
pub fn from_be_bytes<let N: u32>(bytes: [u8; N]) -> Field {
guipublic marked this conversation as resolved.
Show resolved Hide resolved
let mut v = 1;
let mut result = 0;

for i in 0..N {
result += (bytes[N-1-i] as Field) * v;
v = v * 256;
}
result
}

#[builtin(modulus_num_bits)]
pub comptime fn modulus_num_bits() -> u64 {}

Expand Down Expand Up @@ -182,6 +237,15 @@ fn lt_fallback(x: Field, y: Field) -> bool {
x_is_lt
}

unconstrained fn compute_byte_decomposition<let N: u32>(mut x: Field) -> [u8; N] {
let mut a = [0; N];
for i in 0..N {
a[i] = x as u8;
x = (x-(a[i] as Field)) / 256;
}
a
}

mod tests {
#[test]
// docs:start:to_be_bits_example
Expand All @@ -207,6 +271,7 @@ mod tests {
let field = 2;
let bits: [u8; 8] = field.to_be_bytes();
assert_eq(bits, [0, 0, 0, 0, 0, 0, 0, 2]);
assert_eq(crate::field::from_be_bytes(bits), field);
}
// docs:end:to_be_bytes_example

Expand All @@ -216,6 +281,7 @@ mod tests {
let field = 2;
let bits: [u8; 8] = field.to_le_bytes();
assert_eq(bits, [2, 0, 0, 0, 0, 0, 0, 0]);
assert_eq(crate::field::from_le_bytes(bits), field);
}
// docs:end:to_le_bytes_example

Expand All @@ -225,6 +291,7 @@ mod tests {
let field = 2;
let bits: [u8; 8] = field.to_be_radix(256);
assert_eq(bits, [0, 0, 0, 0, 0, 0, 0, 2]);
assert_eq(crate::field::from_be_bytes(bits), field);
}
// docs:end:to_be_radix_example

Expand All @@ -234,6 +301,7 @@ mod tests {
let field = 2;
let bits: [u8; 8] = field.to_le_radix(256);
assert_eq(bits, [2, 0, 0, 0, 0, 0, 0, 0]);
assert_eq(crate::field::from_le_bytes(bits), field);
}
// docs:end:to_le_radix_example
}
7 changes: 1 addition & 6 deletions test_programs/execution_success/to_le_bytes/src/main.nr
Original file line number Diff line number Diff line change
Expand Up @@ -3,16 +3,11 @@ fn main(x: Field, cond: bool) -> pub [u8; 31] {
let byte_array: [u8; 31] = x.to_le_bytes();
assert(byte_array.len() == 31);

let mut bytes = [0; 31];
for i in 0..31 {
bytes[i] = byte_array[i];
}

if cond {
// We've set x = "2040124" so we shouldn't be able to represent this as a single byte.
let bad_byte_array: [u8; 1] = x.to_le_bytes();
assert_eq(bad_byte_array.len(), 1);
}

bytes
byte_array
}
Loading