From 3ca53391d2acfbb5fd6dc2f1c8980f450096652d Mon Sep 17 00:00:00 2001 From: David Cook Date: Sat, 22 Jul 2023 17:31:32 -0500 Subject: [PATCH] Rust: Create newtype structs for typedefs --- fiat-rust/Cargo.toml | 2 +- fiat-rust/src/curve25519_32.rs | 36 +++++++++++++++++-- fiat-rust/src/curve25519_64.rs | 36 +++++++++++++++++-- fiat-rust/src/curve25519_scalar_32.rs | 36 +++++++++++++++++-- fiat-rust/src/curve25519_scalar_64.rs | 36 +++++++++++++++++-- fiat-rust/src/p224_32.rs | 36 +++++++++++++++++-- fiat-rust/src/p224_64.rs | 36 +++++++++++++++++-- fiat-rust/src/p256_32.rs | 36 +++++++++++++++++-- fiat-rust/src/p256_64.rs | 36 +++++++++++++++++-- fiat-rust/src/p256_scalar_32.rs | 36 +++++++++++++++++-- fiat-rust/src/p256_scalar_64.rs | 36 +++++++++++++++++-- fiat-rust/src/p384_32.rs | 36 +++++++++++++++++-- fiat-rust/src/p384_64.rs | 36 +++++++++++++++++-- fiat-rust/src/p384_scalar_32.rs | 36 +++++++++++++++++-- fiat-rust/src/p384_scalar_64.rs | 36 +++++++++++++++++-- fiat-rust/src/p434_64.rs | 36 +++++++++++++++++-- fiat-rust/src/p448_solinas_32.rs | 36 +++++++++++++++++-- fiat-rust/src/p448_solinas_64.rs | 36 +++++++++++++++++-- fiat-rust/src/p521_32.rs | 36 +++++++++++++++++-- fiat-rust/src/p521_64.rs | 36 +++++++++++++++++-- fiat-rust/src/poly1305_32.rs | 36 +++++++++++++++++-- fiat-rust/src/poly1305_64.rs | 36 +++++++++++++++++-- fiat-rust/src/secp256k1_montgomery_32.rs | 36 +++++++++++++++++-- fiat-rust/src/secp256k1_montgomery_64.rs | 36 +++++++++++++++++-- .../src/secp256k1_montgomery_scalar_32.rs | 36 +++++++++++++++++-- .../src/secp256k1_montgomery_scalar_64.rs | 36 +++++++++++++++++-- src/Stringification/Rust.v | 26 ++++++++++---- 27 files changed, 871 insertions(+), 57 deletions(-) diff --git a/fiat-rust/Cargo.toml b/fiat-rust/Cargo.toml index 1d50e778a5..14a1948d5c 100644 --- a/fiat-rust/Cargo.toml +++ b/fiat-rust/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "fiat-crypto" -version = "0.1.21" +version = "0.2.0" authors = ["Fiat Crypto library authors "] edition = "2018" description = "Fiat-crypto generated Rust" diff --git a/fiat-rust/src/curve25519_32.rs b/fiat-rust/src/curve25519_32.rs index 0a48a8a976..34f3e91498 100644 --- a/fiat-rust/src/curve25519_32.rs +++ b/fiat-rust/src/curve25519_32.rs @@ -22,11 +22,43 @@ pub type fiat_25519_i2 = i8; /* The type fiat_25519_loose_field_element is a field element with loose bounds. */ /* Bounds: [[0x0 ~> 0xc000000], [0x0 ~> 0x6000000], [0x0 ~> 0xc000000], [0x0 ~> 0x6000000], [0x0 ~> 0xc000000], [0x0 ~> 0x6000000], [0x0 ~> 0xc000000], [0x0 ~> 0x6000000], [0x0 ~> 0xc000000], [0x0 ~> 0x6000000]] */ -pub type fiat_25519_loose_field_element = [u32; 10]; +#[derive(Clone, Copy)] +pub struct fiat_25519_loose_field_element(pub [u32; 10]); + +impl std::ops::Index for fiat_25519_loose_field_element { + type Output = u32; + #[inline] + fn index(&self, index: usize) -> &Self::Output { + &self.0[index] + } +} + +impl std::ops::IndexMut for fiat_25519_loose_field_element { + #[inline] + fn index_mut(&mut self, index: usize) -> &mut Self::Output { + &mut self.0[index] + } +} /* The type fiat_25519_tight_field_element is a field element with tight bounds. */ /* Bounds: [[0x0 ~> 0x4000000], [0x0 ~> 0x2000000], [0x0 ~> 0x4000000], [0x0 ~> 0x2000000], [0x0 ~> 0x4000000], [0x0 ~> 0x2000000], [0x0 ~> 0x4000000], [0x0 ~> 0x2000000], [0x0 ~> 0x4000000], [0x0 ~> 0x2000000]] */ -pub type fiat_25519_tight_field_element = [u32; 10]; +#[derive(Clone, Copy)] +pub struct fiat_25519_tight_field_element(pub [u32; 10]); + +impl std::ops::Index for fiat_25519_tight_field_element { + type Output = u32; + #[inline] + fn index(&self, index: usize) -> &Self::Output { + &self.0[index] + } +} + +impl std::ops::IndexMut for fiat_25519_tight_field_element { + #[inline] + fn index_mut(&mut self, index: usize) -> &mut Self::Output { + &mut self.0[index] + } +} /// The function fiat_25519_addcarryx_u26 is an addition with carry. diff --git a/fiat-rust/src/curve25519_64.rs b/fiat-rust/src/curve25519_64.rs index 13a36c4f41..d3ad9287af 100644 --- a/fiat-rust/src/curve25519_64.rs +++ b/fiat-rust/src/curve25519_64.rs @@ -22,11 +22,43 @@ pub type fiat_25519_i2 = i8; /* The type fiat_25519_loose_field_element is a field element with loose bounds. */ /* Bounds: [[0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000]] */ -pub type fiat_25519_loose_field_element = [u64; 5]; +#[derive(Clone, Copy)] +pub struct fiat_25519_loose_field_element(pub [u64; 5]); + +impl std::ops::Index for fiat_25519_loose_field_element { + type Output = u64; + #[inline] + fn index(&self, index: usize) -> &Self::Output { + &self.0[index] + } +} + +impl std::ops::IndexMut for fiat_25519_loose_field_element { + #[inline] + fn index_mut(&mut self, index: usize) -> &mut Self::Output { + &mut self.0[index] + } +} /* The type fiat_25519_tight_field_element is a field element with tight bounds. */ /* Bounds: [[0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000]] */ -pub type fiat_25519_tight_field_element = [u64; 5]; +#[derive(Clone, Copy)] +pub struct fiat_25519_tight_field_element(pub [u64; 5]); + +impl std::ops::Index for fiat_25519_tight_field_element { + type Output = u64; + #[inline] + fn index(&self, index: usize) -> &Self::Output { + &self.0[index] + } +} + +impl std::ops::IndexMut for fiat_25519_tight_field_element { + #[inline] + fn index_mut(&mut self, index: usize) -> &mut Self::Output { + &mut self.0[index] + } +} /// The function fiat_25519_addcarryx_u51 is an addition with carry. diff --git a/fiat-rust/src/curve25519_scalar_32.rs b/fiat-rust/src/curve25519_scalar_32.rs index e38b24c239..4a42488c71 100644 --- a/fiat-rust/src/curve25519_scalar_32.rs +++ b/fiat-rust/src/curve25519_scalar_32.rs @@ -27,11 +27,43 @@ pub type fiat_25519_scalar_i2 = i8; /* The type fiat_25519_scalar_montgomery_domain_field_element is a field element in the Montgomery domain. */ /* Bounds: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] */ -pub type fiat_25519_scalar_montgomery_domain_field_element = [u32; 8]; +#[derive(Clone, Copy)] +pub struct fiat_25519_scalar_montgomery_domain_field_element(pub [u32; 8]); + +impl std::ops::Index for fiat_25519_scalar_montgomery_domain_field_element { + type Output = u32; + #[inline] + fn index(&self, index: usize) -> &Self::Output { + &self.0[index] + } +} + +impl std::ops::IndexMut for fiat_25519_scalar_montgomery_domain_field_element { + #[inline] + fn index_mut(&mut self, index: usize) -> &mut Self::Output { + &mut self.0[index] + } +} /* The type fiat_25519_scalar_non_montgomery_domain_field_element is a field element NOT in the Montgomery domain. */ /* Bounds: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] */ -pub type fiat_25519_scalar_non_montgomery_domain_field_element = [u32; 8]; +#[derive(Clone, Copy)] +pub struct fiat_25519_scalar_non_montgomery_domain_field_element(pub [u32; 8]); + +impl std::ops::Index for fiat_25519_scalar_non_montgomery_domain_field_element { + type Output = u32; + #[inline] + fn index(&self, index: usize) -> &Self::Output { + &self.0[index] + } +} + +impl std::ops::IndexMut for fiat_25519_scalar_non_montgomery_domain_field_element { + #[inline] + fn index_mut(&mut self, index: usize) -> &mut Self::Output { + &mut self.0[index] + } +} /// The function fiat_25519_scalar_addcarryx_u32 is an addition with carry. diff --git a/fiat-rust/src/curve25519_scalar_64.rs b/fiat-rust/src/curve25519_scalar_64.rs index dc45f1b8ef..1cb6c9e8d9 100644 --- a/fiat-rust/src/curve25519_scalar_64.rs +++ b/fiat-rust/src/curve25519_scalar_64.rs @@ -27,11 +27,43 @@ pub type fiat_25519_scalar_i2 = i8; /* The type fiat_25519_scalar_montgomery_domain_field_element is a field element in the Montgomery domain. */ /* Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] */ -pub type fiat_25519_scalar_montgomery_domain_field_element = [u64; 4]; +#[derive(Clone, Copy)] +pub struct fiat_25519_scalar_montgomery_domain_field_element(pub [u64; 4]); + +impl std::ops::Index for fiat_25519_scalar_montgomery_domain_field_element { + type Output = u64; + #[inline] + fn index(&self, index: usize) -> &Self::Output { + &self.0[index] + } +} + +impl std::ops::IndexMut for fiat_25519_scalar_montgomery_domain_field_element { + #[inline] + fn index_mut(&mut self, index: usize) -> &mut Self::Output { + &mut self.0[index] + } +} /* The type fiat_25519_scalar_non_montgomery_domain_field_element is a field element NOT in the Montgomery domain. */ /* Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] */ -pub type fiat_25519_scalar_non_montgomery_domain_field_element = [u64; 4]; +#[derive(Clone, Copy)] +pub struct fiat_25519_scalar_non_montgomery_domain_field_element(pub [u64; 4]); + +impl std::ops::Index for fiat_25519_scalar_non_montgomery_domain_field_element { + type Output = u64; + #[inline] + fn index(&self, index: usize) -> &Self::Output { + &self.0[index] + } +} + +impl std::ops::IndexMut for fiat_25519_scalar_non_montgomery_domain_field_element { + #[inline] + fn index_mut(&mut self, index: usize) -> &mut Self::Output { + &mut self.0[index] + } +} /// The function fiat_25519_scalar_addcarryx_u64 is an addition with carry. diff --git a/fiat-rust/src/p224_32.rs b/fiat-rust/src/p224_32.rs index ebe45dfd6c..19a2130cc2 100644 --- a/fiat-rust/src/p224_32.rs +++ b/fiat-rust/src/p224_32.rs @@ -27,11 +27,43 @@ pub type fiat_p224_i2 = i8; /* The type fiat_p224_montgomery_domain_field_element is a field element in the Montgomery domain. */ /* Bounds: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] */ -pub type fiat_p224_montgomery_domain_field_element = [u32; 7]; +#[derive(Clone, Copy)] +pub struct fiat_p224_montgomery_domain_field_element(pub [u32; 7]); + +impl std::ops::Index for fiat_p224_montgomery_domain_field_element { + type Output = u32; + #[inline] + fn index(&self, index: usize) -> &Self::Output { + &self.0[index] + } +} + +impl std::ops::IndexMut for fiat_p224_montgomery_domain_field_element { + #[inline] + fn index_mut(&mut self, index: usize) -> &mut Self::Output { + &mut self.0[index] + } +} /* The type fiat_p224_non_montgomery_domain_field_element is a field element NOT in the Montgomery domain. */ /* Bounds: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] */ -pub type fiat_p224_non_montgomery_domain_field_element = [u32; 7]; +#[derive(Clone, Copy)] +pub struct fiat_p224_non_montgomery_domain_field_element(pub [u32; 7]); + +impl std::ops::Index for fiat_p224_non_montgomery_domain_field_element { + type Output = u32; + #[inline] + fn index(&self, index: usize) -> &Self::Output { + &self.0[index] + } +} + +impl std::ops::IndexMut for fiat_p224_non_montgomery_domain_field_element { + #[inline] + fn index_mut(&mut self, index: usize) -> &mut Self::Output { + &mut self.0[index] + } +} /// The function fiat_p224_addcarryx_u32 is an addition with carry. diff --git a/fiat-rust/src/p224_64.rs b/fiat-rust/src/p224_64.rs index 785eac4051..f4ca4ca9e6 100644 --- a/fiat-rust/src/p224_64.rs +++ b/fiat-rust/src/p224_64.rs @@ -27,11 +27,43 @@ pub type fiat_p224_i2 = i8; /* The type fiat_p224_montgomery_domain_field_element is a field element in the Montgomery domain. */ /* Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] */ -pub type fiat_p224_montgomery_domain_field_element = [u64; 4]; +#[derive(Clone, Copy)] +pub struct fiat_p224_montgomery_domain_field_element(pub [u64; 4]); + +impl std::ops::Index for fiat_p224_montgomery_domain_field_element { + type Output = u64; + #[inline] + fn index(&self, index: usize) -> &Self::Output { + &self.0[index] + } +} + +impl std::ops::IndexMut for fiat_p224_montgomery_domain_field_element { + #[inline] + fn index_mut(&mut self, index: usize) -> &mut Self::Output { + &mut self.0[index] + } +} /* The type fiat_p224_non_montgomery_domain_field_element is a field element NOT in the Montgomery domain. */ /* Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] */ -pub type fiat_p224_non_montgomery_domain_field_element = [u64; 4]; +#[derive(Clone, Copy)] +pub struct fiat_p224_non_montgomery_domain_field_element(pub [u64; 4]); + +impl std::ops::Index for fiat_p224_non_montgomery_domain_field_element { + type Output = u64; + #[inline] + fn index(&self, index: usize) -> &Self::Output { + &self.0[index] + } +} + +impl std::ops::IndexMut for fiat_p224_non_montgomery_domain_field_element { + #[inline] + fn index_mut(&mut self, index: usize) -> &mut Self::Output { + &mut self.0[index] + } +} /// The function fiat_p224_addcarryx_u64 is an addition with carry. diff --git a/fiat-rust/src/p256_32.rs b/fiat-rust/src/p256_32.rs index 5eb80994db..15eaeb343b 100644 --- a/fiat-rust/src/p256_32.rs +++ b/fiat-rust/src/p256_32.rs @@ -27,11 +27,43 @@ pub type fiat_p256_i2 = i8; /* The type fiat_p256_montgomery_domain_field_element is a field element in the Montgomery domain. */ /* Bounds: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] */ -pub type fiat_p256_montgomery_domain_field_element = [u32; 8]; +#[derive(Clone, Copy)] +pub struct fiat_p256_montgomery_domain_field_element(pub [u32; 8]); + +impl std::ops::Index for fiat_p256_montgomery_domain_field_element { + type Output = u32; + #[inline] + fn index(&self, index: usize) -> &Self::Output { + &self.0[index] + } +} + +impl std::ops::IndexMut for fiat_p256_montgomery_domain_field_element { + #[inline] + fn index_mut(&mut self, index: usize) -> &mut Self::Output { + &mut self.0[index] + } +} /* The type fiat_p256_non_montgomery_domain_field_element is a field element NOT in the Montgomery domain. */ /* Bounds: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] */ -pub type fiat_p256_non_montgomery_domain_field_element = [u32; 8]; +#[derive(Clone, Copy)] +pub struct fiat_p256_non_montgomery_domain_field_element(pub [u32; 8]); + +impl std::ops::Index for fiat_p256_non_montgomery_domain_field_element { + type Output = u32; + #[inline] + fn index(&self, index: usize) -> &Self::Output { + &self.0[index] + } +} + +impl std::ops::IndexMut for fiat_p256_non_montgomery_domain_field_element { + #[inline] + fn index_mut(&mut self, index: usize) -> &mut Self::Output { + &mut self.0[index] + } +} /// The function fiat_p256_addcarryx_u32 is an addition with carry. diff --git a/fiat-rust/src/p256_64.rs b/fiat-rust/src/p256_64.rs index 0a3c6fb843..c72638d5b7 100644 --- a/fiat-rust/src/p256_64.rs +++ b/fiat-rust/src/p256_64.rs @@ -27,11 +27,43 @@ pub type fiat_p256_i2 = i8; /* The type fiat_p256_montgomery_domain_field_element is a field element in the Montgomery domain. */ /* Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] */ -pub type fiat_p256_montgomery_domain_field_element = [u64; 4]; +#[derive(Clone, Copy)] +pub struct fiat_p256_montgomery_domain_field_element(pub [u64; 4]); + +impl std::ops::Index for fiat_p256_montgomery_domain_field_element { + type Output = u64; + #[inline] + fn index(&self, index: usize) -> &Self::Output { + &self.0[index] + } +} + +impl std::ops::IndexMut for fiat_p256_montgomery_domain_field_element { + #[inline] + fn index_mut(&mut self, index: usize) -> &mut Self::Output { + &mut self.0[index] + } +} /* The type fiat_p256_non_montgomery_domain_field_element is a field element NOT in the Montgomery domain. */ /* Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] */ -pub type fiat_p256_non_montgomery_domain_field_element = [u64; 4]; +#[derive(Clone, Copy)] +pub struct fiat_p256_non_montgomery_domain_field_element(pub [u64; 4]); + +impl std::ops::Index for fiat_p256_non_montgomery_domain_field_element { + type Output = u64; + #[inline] + fn index(&self, index: usize) -> &Self::Output { + &self.0[index] + } +} + +impl std::ops::IndexMut for fiat_p256_non_montgomery_domain_field_element { + #[inline] + fn index_mut(&mut self, index: usize) -> &mut Self::Output { + &mut self.0[index] + } +} /// The function fiat_p256_addcarryx_u64 is an addition with carry. diff --git a/fiat-rust/src/p256_scalar_32.rs b/fiat-rust/src/p256_scalar_32.rs index 4028e42edc..38cf115da6 100644 --- a/fiat-rust/src/p256_scalar_32.rs +++ b/fiat-rust/src/p256_scalar_32.rs @@ -27,11 +27,43 @@ pub type fiat_p256_scalar_i2 = i8; /* The type fiat_p256_scalar_montgomery_domain_field_element is a field element in the Montgomery domain. */ /* Bounds: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] */ -pub type fiat_p256_scalar_montgomery_domain_field_element = [u32; 8]; +#[derive(Clone, Copy)] +pub struct fiat_p256_scalar_montgomery_domain_field_element(pub [u32; 8]); + +impl std::ops::Index for fiat_p256_scalar_montgomery_domain_field_element { + type Output = u32; + #[inline] + fn index(&self, index: usize) -> &Self::Output { + &self.0[index] + } +} + +impl std::ops::IndexMut for fiat_p256_scalar_montgomery_domain_field_element { + #[inline] + fn index_mut(&mut self, index: usize) -> &mut Self::Output { + &mut self.0[index] + } +} /* The type fiat_p256_scalar_non_montgomery_domain_field_element is a field element NOT in the Montgomery domain. */ /* Bounds: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] */ -pub type fiat_p256_scalar_non_montgomery_domain_field_element = [u32; 8]; +#[derive(Clone, Copy)] +pub struct fiat_p256_scalar_non_montgomery_domain_field_element(pub [u32; 8]); + +impl std::ops::Index for fiat_p256_scalar_non_montgomery_domain_field_element { + type Output = u32; + #[inline] + fn index(&self, index: usize) -> &Self::Output { + &self.0[index] + } +} + +impl std::ops::IndexMut for fiat_p256_scalar_non_montgomery_domain_field_element { + #[inline] + fn index_mut(&mut self, index: usize) -> &mut Self::Output { + &mut self.0[index] + } +} /// The function fiat_p256_scalar_addcarryx_u32 is an addition with carry. diff --git a/fiat-rust/src/p256_scalar_64.rs b/fiat-rust/src/p256_scalar_64.rs index 3467605c99..ff12be104f 100644 --- a/fiat-rust/src/p256_scalar_64.rs +++ b/fiat-rust/src/p256_scalar_64.rs @@ -27,11 +27,43 @@ pub type fiat_p256_scalar_i2 = i8; /* The type fiat_p256_scalar_montgomery_domain_field_element is a field element in the Montgomery domain. */ /* Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] */ -pub type fiat_p256_scalar_montgomery_domain_field_element = [u64; 4]; +#[derive(Clone, Copy)] +pub struct fiat_p256_scalar_montgomery_domain_field_element(pub [u64; 4]); + +impl std::ops::Index for fiat_p256_scalar_montgomery_domain_field_element { + type Output = u64; + #[inline] + fn index(&self, index: usize) -> &Self::Output { + &self.0[index] + } +} + +impl std::ops::IndexMut for fiat_p256_scalar_montgomery_domain_field_element { + #[inline] + fn index_mut(&mut self, index: usize) -> &mut Self::Output { + &mut self.0[index] + } +} /* The type fiat_p256_scalar_non_montgomery_domain_field_element is a field element NOT in the Montgomery domain. */ /* Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] */ -pub type fiat_p256_scalar_non_montgomery_domain_field_element = [u64; 4]; +#[derive(Clone, Copy)] +pub struct fiat_p256_scalar_non_montgomery_domain_field_element(pub [u64; 4]); + +impl std::ops::Index for fiat_p256_scalar_non_montgomery_domain_field_element { + type Output = u64; + #[inline] + fn index(&self, index: usize) -> &Self::Output { + &self.0[index] + } +} + +impl std::ops::IndexMut for fiat_p256_scalar_non_montgomery_domain_field_element { + #[inline] + fn index_mut(&mut self, index: usize) -> &mut Self::Output { + &mut self.0[index] + } +} /// The function fiat_p256_scalar_addcarryx_u64 is an addition with carry. diff --git a/fiat-rust/src/p384_32.rs b/fiat-rust/src/p384_32.rs index 8160e28ea9..9ebc80cb48 100644 --- a/fiat-rust/src/p384_32.rs +++ b/fiat-rust/src/p384_32.rs @@ -27,11 +27,43 @@ pub type fiat_p384_i2 = i8; /* The type fiat_p384_montgomery_domain_field_element is a field element in the Montgomery domain. */ /* Bounds: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] */ -pub type fiat_p384_montgomery_domain_field_element = [u32; 12]; +#[derive(Clone, Copy)] +pub struct fiat_p384_montgomery_domain_field_element(pub [u32; 12]); + +impl std::ops::Index for fiat_p384_montgomery_domain_field_element { + type Output = u32; + #[inline] + fn index(&self, index: usize) -> &Self::Output { + &self.0[index] + } +} + +impl std::ops::IndexMut for fiat_p384_montgomery_domain_field_element { + #[inline] + fn index_mut(&mut self, index: usize) -> &mut Self::Output { + &mut self.0[index] + } +} /* The type fiat_p384_non_montgomery_domain_field_element is a field element NOT in the Montgomery domain. */ /* Bounds: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] */ -pub type fiat_p384_non_montgomery_domain_field_element = [u32; 12]; +#[derive(Clone, Copy)] +pub struct fiat_p384_non_montgomery_domain_field_element(pub [u32; 12]); + +impl std::ops::Index for fiat_p384_non_montgomery_domain_field_element { + type Output = u32; + #[inline] + fn index(&self, index: usize) -> &Self::Output { + &self.0[index] + } +} + +impl std::ops::IndexMut for fiat_p384_non_montgomery_domain_field_element { + #[inline] + fn index_mut(&mut self, index: usize) -> &mut Self::Output { + &mut self.0[index] + } +} /// The function fiat_p384_addcarryx_u32 is an addition with carry. diff --git a/fiat-rust/src/p384_64.rs b/fiat-rust/src/p384_64.rs index a14d7d3c24..07d1594f71 100644 --- a/fiat-rust/src/p384_64.rs +++ b/fiat-rust/src/p384_64.rs @@ -27,11 +27,43 @@ pub type fiat_p384_i2 = i8; /* The type fiat_p384_montgomery_domain_field_element is a field element in the Montgomery domain. */ /* Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] */ -pub type fiat_p384_montgomery_domain_field_element = [u64; 6]; +#[derive(Clone, Copy)] +pub struct fiat_p384_montgomery_domain_field_element(pub [u64; 6]); + +impl std::ops::Index for fiat_p384_montgomery_domain_field_element { + type Output = u64; + #[inline] + fn index(&self, index: usize) -> &Self::Output { + &self.0[index] + } +} + +impl std::ops::IndexMut for fiat_p384_montgomery_domain_field_element { + #[inline] + fn index_mut(&mut self, index: usize) -> &mut Self::Output { + &mut self.0[index] + } +} /* The type fiat_p384_non_montgomery_domain_field_element is a field element NOT in the Montgomery domain. */ /* Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] */ -pub type fiat_p384_non_montgomery_domain_field_element = [u64; 6]; +#[derive(Clone, Copy)] +pub struct fiat_p384_non_montgomery_domain_field_element(pub [u64; 6]); + +impl std::ops::Index for fiat_p384_non_montgomery_domain_field_element { + type Output = u64; + #[inline] + fn index(&self, index: usize) -> &Self::Output { + &self.0[index] + } +} + +impl std::ops::IndexMut for fiat_p384_non_montgomery_domain_field_element { + #[inline] + fn index_mut(&mut self, index: usize) -> &mut Self::Output { + &mut self.0[index] + } +} /// The function fiat_p384_addcarryx_u64 is an addition with carry. diff --git a/fiat-rust/src/p384_scalar_32.rs b/fiat-rust/src/p384_scalar_32.rs index ef07b88f17..1621faa1bd 100644 --- a/fiat-rust/src/p384_scalar_32.rs +++ b/fiat-rust/src/p384_scalar_32.rs @@ -27,11 +27,43 @@ pub type fiat_p384_scalar_i2 = i8; /* The type fiat_p384_scalar_montgomery_domain_field_element is a field element in the Montgomery domain. */ /* Bounds: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] */ -pub type fiat_p384_scalar_montgomery_domain_field_element = [u32; 12]; +#[derive(Clone, Copy)] +pub struct fiat_p384_scalar_montgomery_domain_field_element(pub [u32; 12]); + +impl std::ops::Index for fiat_p384_scalar_montgomery_domain_field_element { + type Output = u32; + #[inline] + fn index(&self, index: usize) -> &Self::Output { + &self.0[index] + } +} + +impl std::ops::IndexMut for fiat_p384_scalar_montgomery_domain_field_element { + #[inline] + fn index_mut(&mut self, index: usize) -> &mut Self::Output { + &mut self.0[index] + } +} /* The type fiat_p384_scalar_non_montgomery_domain_field_element is a field element NOT in the Montgomery domain. */ /* Bounds: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] */ -pub type fiat_p384_scalar_non_montgomery_domain_field_element = [u32; 12]; +#[derive(Clone, Copy)] +pub struct fiat_p384_scalar_non_montgomery_domain_field_element(pub [u32; 12]); + +impl std::ops::Index for fiat_p384_scalar_non_montgomery_domain_field_element { + type Output = u32; + #[inline] + fn index(&self, index: usize) -> &Self::Output { + &self.0[index] + } +} + +impl std::ops::IndexMut for fiat_p384_scalar_non_montgomery_domain_field_element { + #[inline] + fn index_mut(&mut self, index: usize) -> &mut Self::Output { + &mut self.0[index] + } +} /// The function fiat_p384_scalar_addcarryx_u32 is an addition with carry. diff --git a/fiat-rust/src/p384_scalar_64.rs b/fiat-rust/src/p384_scalar_64.rs index 63474c2399..c3b56faf1f 100644 --- a/fiat-rust/src/p384_scalar_64.rs +++ b/fiat-rust/src/p384_scalar_64.rs @@ -27,11 +27,43 @@ pub type fiat_p384_scalar_i2 = i8; /* The type fiat_p384_scalar_montgomery_domain_field_element is a field element in the Montgomery domain. */ /* Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] */ -pub type fiat_p384_scalar_montgomery_domain_field_element = [u64; 6]; +#[derive(Clone, Copy)] +pub struct fiat_p384_scalar_montgomery_domain_field_element(pub [u64; 6]); + +impl std::ops::Index for fiat_p384_scalar_montgomery_domain_field_element { + type Output = u64; + #[inline] + fn index(&self, index: usize) -> &Self::Output { + &self.0[index] + } +} + +impl std::ops::IndexMut for fiat_p384_scalar_montgomery_domain_field_element { + #[inline] + fn index_mut(&mut self, index: usize) -> &mut Self::Output { + &mut self.0[index] + } +} /* The type fiat_p384_scalar_non_montgomery_domain_field_element is a field element NOT in the Montgomery domain. */ /* Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] */ -pub type fiat_p384_scalar_non_montgomery_domain_field_element = [u64; 6]; +#[derive(Clone, Copy)] +pub struct fiat_p384_scalar_non_montgomery_domain_field_element(pub [u64; 6]); + +impl std::ops::Index for fiat_p384_scalar_non_montgomery_domain_field_element { + type Output = u64; + #[inline] + fn index(&self, index: usize) -> &Self::Output { + &self.0[index] + } +} + +impl std::ops::IndexMut for fiat_p384_scalar_non_montgomery_domain_field_element { + #[inline] + fn index_mut(&mut self, index: usize) -> &mut Self::Output { + &mut self.0[index] + } +} /// The function fiat_p384_scalar_addcarryx_u64 is an addition with carry. diff --git a/fiat-rust/src/p434_64.rs b/fiat-rust/src/p434_64.rs index 1879479606..8c396a05cd 100644 --- a/fiat-rust/src/p434_64.rs +++ b/fiat-rust/src/p434_64.rs @@ -27,11 +27,43 @@ pub type fiat_p434_i2 = i8; /* The type fiat_p434_montgomery_domain_field_element is a field element in the Montgomery domain. */ /* Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] */ -pub type fiat_p434_montgomery_domain_field_element = [u64; 7]; +#[derive(Clone, Copy)] +pub struct fiat_p434_montgomery_domain_field_element(pub [u64; 7]); + +impl std::ops::Index for fiat_p434_montgomery_domain_field_element { + type Output = u64; + #[inline] + fn index(&self, index: usize) -> &Self::Output { + &self.0[index] + } +} + +impl std::ops::IndexMut for fiat_p434_montgomery_domain_field_element { + #[inline] + fn index_mut(&mut self, index: usize) -> &mut Self::Output { + &mut self.0[index] + } +} /* The type fiat_p434_non_montgomery_domain_field_element is a field element NOT in the Montgomery domain. */ /* Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] */ -pub type fiat_p434_non_montgomery_domain_field_element = [u64; 7]; +#[derive(Clone, Copy)] +pub struct fiat_p434_non_montgomery_domain_field_element(pub [u64; 7]); + +impl std::ops::Index for fiat_p434_non_montgomery_domain_field_element { + type Output = u64; + #[inline] + fn index(&self, index: usize) -> &Self::Output { + &self.0[index] + } +} + +impl std::ops::IndexMut for fiat_p434_non_montgomery_domain_field_element { + #[inline] + fn index_mut(&mut self, index: usize) -> &mut Self::Output { + &mut self.0[index] + } +} /// The function fiat_p434_addcarryx_u64 is an addition with carry. diff --git a/fiat-rust/src/p448_solinas_32.rs b/fiat-rust/src/p448_solinas_32.rs index 9f37fd21ae..97b6c25aff 100644 --- a/fiat-rust/src/p448_solinas_32.rs +++ b/fiat-rust/src/p448_solinas_32.rs @@ -22,11 +22,43 @@ pub type fiat_p448_i2 = i8; /* The type fiat_p448_loose_field_element is a field element with loose bounds. */ /* Bounds: [[0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000]] */ -pub type fiat_p448_loose_field_element = [u32; 16]; +#[derive(Clone, Copy)] +pub struct fiat_p448_loose_field_element(pub [u32; 16]); + +impl std::ops::Index for fiat_p448_loose_field_element { + type Output = u32; + #[inline] + fn index(&self, index: usize) -> &Self::Output { + &self.0[index] + } +} + +impl std::ops::IndexMut for fiat_p448_loose_field_element { + #[inline] + fn index_mut(&mut self, index: usize) -> &mut Self::Output { + &mut self.0[index] + } +} /* The type fiat_p448_tight_field_element is a field element with tight bounds. */ /* Bounds: [[0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000]] */ -pub type fiat_p448_tight_field_element = [u32; 16]; +#[derive(Clone, Copy)] +pub struct fiat_p448_tight_field_element(pub [u32; 16]); + +impl std::ops::Index for fiat_p448_tight_field_element { + type Output = u32; + #[inline] + fn index(&self, index: usize) -> &Self::Output { + &self.0[index] + } +} + +impl std::ops::IndexMut for fiat_p448_tight_field_element { + #[inline] + fn index_mut(&mut self, index: usize) -> &mut Self::Output { + &mut self.0[index] + } +} /// The function fiat_p448_addcarryx_u28 is an addition with carry. diff --git a/fiat-rust/src/p448_solinas_64.rs b/fiat-rust/src/p448_solinas_64.rs index 13a99ccc6c..029ed6ea57 100644 --- a/fiat-rust/src/p448_solinas_64.rs +++ b/fiat-rust/src/p448_solinas_64.rs @@ -22,11 +22,43 @@ pub type fiat_p448_i2 = i8; /* The type fiat_p448_loose_field_element is a field element with loose bounds. */ /* Bounds: [[0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000]] */ -pub type fiat_p448_loose_field_element = [u64; 8]; +#[derive(Clone, Copy)] +pub struct fiat_p448_loose_field_element(pub [u64; 8]); + +impl std::ops::Index for fiat_p448_loose_field_element { + type Output = u64; + #[inline] + fn index(&self, index: usize) -> &Self::Output { + &self.0[index] + } +} + +impl std::ops::IndexMut for fiat_p448_loose_field_element { + #[inline] + fn index_mut(&mut self, index: usize) -> &mut Self::Output { + &mut self.0[index] + } +} /* The type fiat_p448_tight_field_element is a field element with tight bounds. */ /* Bounds: [[0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000]] */ -pub type fiat_p448_tight_field_element = [u64; 8]; +#[derive(Clone, Copy)] +pub struct fiat_p448_tight_field_element(pub [u64; 8]); + +impl std::ops::Index for fiat_p448_tight_field_element { + type Output = u64; + #[inline] + fn index(&self, index: usize) -> &Self::Output { + &self.0[index] + } +} + +impl std::ops::IndexMut for fiat_p448_tight_field_element { + #[inline] + fn index_mut(&mut self, index: usize) -> &mut Self::Output { + &mut self.0[index] + } +} /// The function fiat_p448_addcarryx_u56 is an addition with carry. diff --git a/fiat-rust/src/p521_32.rs b/fiat-rust/src/p521_32.rs index 95b7a6e6af..09a1778c02 100644 --- a/fiat-rust/src/p521_32.rs +++ b/fiat-rust/src/p521_32.rs @@ -22,11 +22,43 @@ pub type fiat_p521_i2 = i8; /* The type fiat_p521_loose_field_element is a field element with loose bounds. */ /* Bounds: [[0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x18000000]] */ -pub type fiat_p521_loose_field_element = [u32; 19]; +#[derive(Clone, Copy)] +pub struct fiat_p521_loose_field_element(pub [u32; 19]); + +impl std::ops::Index for fiat_p521_loose_field_element { + type Output = u32; + #[inline] + fn index(&self, index: usize) -> &Self::Output { + &self.0[index] + } +} + +impl std::ops::IndexMut for fiat_p521_loose_field_element { + #[inline] + fn index_mut(&mut self, index: usize) -> &mut Self::Output { + &mut self.0[index] + } +} /* The type fiat_p521_tight_field_element is a field element with tight bounds. */ /* Bounds: [[0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x8000000]] */ -pub type fiat_p521_tight_field_element = [u32; 19]; +#[derive(Clone, Copy)] +pub struct fiat_p521_tight_field_element(pub [u32; 19]); + +impl std::ops::Index for fiat_p521_tight_field_element { + type Output = u32; + #[inline] + fn index(&self, index: usize) -> &Self::Output { + &self.0[index] + } +} + +impl std::ops::IndexMut for fiat_p521_tight_field_element { + #[inline] + fn index_mut(&mut self, index: usize) -> &mut Self::Output { + &mut self.0[index] + } +} /// The function fiat_p521_addcarryx_u28 is an addition with carry. diff --git a/fiat-rust/src/p521_64.rs b/fiat-rust/src/p521_64.rs index c220311a1d..c333b751b8 100644 --- a/fiat-rust/src/p521_64.rs +++ b/fiat-rust/src/p521_64.rs @@ -22,11 +22,43 @@ pub type fiat_p521_i2 = i8; /* The type fiat_p521_loose_field_element is a field element with loose bounds. */ /* Bounds: [[0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0x600000000000000]] */ -pub type fiat_p521_loose_field_element = [u64; 9]; +#[derive(Clone, Copy)] +pub struct fiat_p521_loose_field_element(pub [u64; 9]); + +impl std::ops::Index for fiat_p521_loose_field_element { + type Output = u64; + #[inline] + fn index(&self, index: usize) -> &Self::Output { + &self.0[index] + } +} + +impl std::ops::IndexMut for fiat_p521_loose_field_element { + #[inline] + fn index_mut(&mut self, index: usize) -> &mut Self::Output { + &mut self.0[index] + } +} /* The type fiat_p521_tight_field_element is a field element with tight bounds. */ /* Bounds: [[0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x200000000000000]] */ -pub type fiat_p521_tight_field_element = [u64; 9]; +#[derive(Clone, Copy)] +pub struct fiat_p521_tight_field_element(pub [u64; 9]); + +impl std::ops::Index for fiat_p521_tight_field_element { + type Output = u64; + #[inline] + fn index(&self, index: usize) -> &Self::Output { + &self.0[index] + } +} + +impl std::ops::IndexMut for fiat_p521_tight_field_element { + #[inline] + fn index_mut(&mut self, index: usize) -> &mut Self::Output { + &mut self.0[index] + } +} /// The function fiat_p521_addcarryx_u58 is an addition with carry. diff --git a/fiat-rust/src/poly1305_32.rs b/fiat-rust/src/poly1305_32.rs index 19a167a4e2..a5f1d8284e 100644 --- a/fiat-rust/src/poly1305_32.rs +++ b/fiat-rust/src/poly1305_32.rs @@ -22,11 +22,43 @@ pub type fiat_poly1305_i2 = i8; /* The type fiat_poly1305_loose_field_element is a field element with loose bounds. */ /* Bounds: [[0x0 ~> 0xc000000], [0x0 ~> 0xc000000], [0x0 ~> 0xc000000], [0x0 ~> 0xc000000], [0x0 ~> 0xc000000]] */ -pub type fiat_poly1305_loose_field_element = [u32; 5]; +#[derive(Clone, Copy)] +pub struct fiat_poly1305_loose_field_element(pub [u32; 5]); + +impl std::ops::Index for fiat_poly1305_loose_field_element { + type Output = u32; + #[inline] + fn index(&self, index: usize) -> &Self::Output { + &self.0[index] + } +} + +impl std::ops::IndexMut for fiat_poly1305_loose_field_element { + #[inline] + fn index_mut(&mut self, index: usize) -> &mut Self::Output { + &mut self.0[index] + } +} /* The type fiat_poly1305_tight_field_element is a field element with tight bounds. */ /* Bounds: [[0x0 ~> 0x4000000], [0x0 ~> 0x4000000], [0x0 ~> 0x4000000], [0x0 ~> 0x4000000], [0x0 ~> 0x4000000]] */ -pub type fiat_poly1305_tight_field_element = [u32; 5]; +#[derive(Clone, Copy)] +pub struct fiat_poly1305_tight_field_element(pub [u32; 5]); + +impl std::ops::Index for fiat_poly1305_tight_field_element { + type Output = u32; + #[inline] + fn index(&self, index: usize) -> &Self::Output { + &self.0[index] + } +} + +impl std::ops::IndexMut for fiat_poly1305_tight_field_element { + #[inline] + fn index_mut(&mut self, index: usize) -> &mut Self::Output { + &mut self.0[index] + } +} /// The function fiat_poly1305_addcarryx_u26 is an addition with carry. diff --git a/fiat-rust/src/poly1305_64.rs b/fiat-rust/src/poly1305_64.rs index 05c51c8213..2d835a7fb9 100644 --- a/fiat-rust/src/poly1305_64.rs +++ b/fiat-rust/src/poly1305_64.rs @@ -22,11 +22,43 @@ pub type fiat_poly1305_i2 = i8; /* The type fiat_poly1305_loose_field_element is a field element with loose bounds. */ /* Bounds: [[0x0 ~> 0x300000000000], [0x0 ~> 0x180000000000], [0x0 ~> 0x180000000000]] */ -pub type fiat_poly1305_loose_field_element = [u64; 3]; +#[derive(Clone, Copy)] +pub struct fiat_poly1305_loose_field_element(pub [u64; 3]); + +impl std::ops::Index for fiat_poly1305_loose_field_element { + type Output = u64; + #[inline] + fn index(&self, index: usize) -> &Self::Output { + &self.0[index] + } +} + +impl std::ops::IndexMut for fiat_poly1305_loose_field_element { + #[inline] + fn index_mut(&mut self, index: usize) -> &mut Self::Output { + &mut self.0[index] + } +} /* The type fiat_poly1305_tight_field_element is a field element with tight bounds. */ /* Bounds: [[0x0 ~> 0x100000000000], [0x0 ~> 0x80000000000], [0x0 ~> 0x80000000000]] */ -pub type fiat_poly1305_tight_field_element = [u64; 3]; +#[derive(Clone, Copy)] +pub struct fiat_poly1305_tight_field_element(pub [u64; 3]); + +impl std::ops::Index for fiat_poly1305_tight_field_element { + type Output = u64; + #[inline] + fn index(&self, index: usize) -> &Self::Output { + &self.0[index] + } +} + +impl std::ops::IndexMut for fiat_poly1305_tight_field_element { + #[inline] + fn index_mut(&mut self, index: usize) -> &mut Self::Output { + &mut self.0[index] + } +} /// The function fiat_poly1305_addcarryx_u44 is an addition with carry. diff --git a/fiat-rust/src/secp256k1_montgomery_32.rs b/fiat-rust/src/secp256k1_montgomery_32.rs index 9d0024faff..955d39dacd 100644 --- a/fiat-rust/src/secp256k1_montgomery_32.rs +++ b/fiat-rust/src/secp256k1_montgomery_32.rs @@ -27,11 +27,43 @@ pub type fiat_secp256k1_montgomery_i2 = i8; /* The type fiat_secp256k1_montgomery_montgomery_domain_field_element is a field element in the Montgomery domain. */ /* Bounds: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] */ -pub type fiat_secp256k1_montgomery_montgomery_domain_field_element = [u32; 8]; +#[derive(Clone, Copy)] +pub struct fiat_secp256k1_montgomery_montgomery_domain_field_element(pub [u32; 8]); + +impl std::ops::Index for fiat_secp256k1_montgomery_montgomery_domain_field_element { + type Output = u32; + #[inline] + fn index(&self, index: usize) -> &Self::Output { + &self.0[index] + } +} + +impl std::ops::IndexMut for fiat_secp256k1_montgomery_montgomery_domain_field_element { + #[inline] + fn index_mut(&mut self, index: usize) -> &mut Self::Output { + &mut self.0[index] + } +} /* The type fiat_secp256k1_montgomery_non_montgomery_domain_field_element is a field element NOT in the Montgomery domain. */ /* Bounds: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] */ -pub type fiat_secp256k1_montgomery_non_montgomery_domain_field_element = [u32; 8]; +#[derive(Clone, Copy)] +pub struct fiat_secp256k1_montgomery_non_montgomery_domain_field_element(pub [u32; 8]); + +impl std::ops::Index for fiat_secp256k1_montgomery_non_montgomery_domain_field_element { + type Output = u32; + #[inline] + fn index(&self, index: usize) -> &Self::Output { + &self.0[index] + } +} + +impl std::ops::IndexMut for fiat_secp256k1_montgomery_non_montgomery_domain_field_element { + #[inline] + fn index_mut(&mut self, index: usize) -> &mut Self::Output { + &mut self.0[index] + } +} /// The function fiat_secp256k1_montgomery_addcarryx_u32 is an addition with carry. diff --git a/fiat-rust/src/secp256k1_montgomery_64.rs b/fiat-rust/src/secp256k1_montgomery_64.rs index f892ea5618..ad6788116a 100644 --- a/fiat-rust/src/secp256k1_montgomery_64.rs +++ b/fiat-rust/src/secp256k1_montgomery_64.rs @@ -27,11 +27,43 @@ pub type fiat_secp256k1_montgomery_i2 = i8; /* The type fiat_secp256k1_montgomery_montgomery_domain_field_element is a field element in the Montgomery domain. */ /* Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] */ -pub type fiat_secp256k1_montgomery_montgomery_domain_field_element = [u64; 4]; +#[derive(Clone, Copy)] +pub struct fiat_secp256k1_montgomery_montgomery_domain_field_element(pub [u64; 4]); + +impl std::ops::Index for fiat_secp256k1_montgomery_montgomery_domain_field_element { + type Output = u64; + #[inline] + fn index(&self, index: usize) -> &Self::Output { + &self.0[index] + } +} + +impl std::ops::IndexMut for fiat_secp256k1_montgomery_montgomery_domain_field_element { + #[inline] + fn index_mut(&mut self, index: usize) -> &mut Self::Output { + &mut self.0[index] + } +} /* The type fiat_secp256k1_montgomery_non_montgomery_domain_field_element is a field element NOT in the Montgomery domain. */ /* Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] */ -pub type fiat_secp256k1_montgomery_non_montgomery_domain_field_element = [u64; 4]; +#[derive(Clone, Copy)] +pub struct fiat_secp256k1_montgomery_non_montgomery_domain_field_element(pub [u64; 4]); + +impl std::ops::Index for fiat_secp256k1_montgomery_non_montgomery_domain_field_element { + type Output = u64; + #[inline] + fn index(&self, index: usize) -> &Self::Output { + &self.0[index] + } +} + +impl std::ops::IndexMut for fiat_secp256k1_montgomery_non_montgomery_domain_field_element { + #[inline] + fn index_mut(&mut self, index: usize) -> &mut Self::Output { + &mut self.0[index] + } +} /// The function fiat_secp256k1_montgomery_addcarryx_u64 is an addition with carry. diff --git a/fiat-rust/src/secp256k1_montgomery_scalar_32.rs b/fiat-rust/src/secp256k1_montgomery_scalar_32.rs index b2ed348a11..d7e29f81a0 100644 --- a/fiat-rust/src/secp256k1_montgomery_scalar_32.rs +++ b/fiat-rust/src/secp256k1_montgomery_scalar_32.rs @@ -27,11 +27,43 @@ pub type fiat_secp256k1_montgomery_scalar_i2 = i8; /* The type fiat_secp256k1_montgomery_scalar_montgomery_domain_field_element is a field element in the Montgomery domain. */ /* Bounds: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] */ -pub type fiat_secp256k1_montgomery_scalar_montgomery_domain_field_element = [u32; 8]; +#[derive(Clone, Copy)] +pub struct fiat_secp256k1_montgomery_scalar_montgomery_domain_field_element(pub [u32; 8]); + +impl std::ops::Index for fiat_secp256k1_montgomery_scalar_montgomery_domain_field_element { + type Output = u32; + #[inline] + fn index(&self, index: usize) -> &Self::Output { + &self.0[index] + } +} + +impl std::ops::IndexMut for fiat_secp256k1_montgomery_scalar_montgomery_domain_field_element { + #[inline] + fn index_mut(&mut self, index: usize) -> &mut Self::Output { + &mut self.0[index] + } +} /* The type fiat_secp256k1_montgomery_scalar_non_montgomery_domain_field_element is a field element NOT in the Montgomery domain. */ /* Bounds: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] */ -pub type fiat_secp256k1_montgomery_scalar_non_montgomery_domain_field_element = [u32; 8]; +#[derive(Clone, Copy)] +pub struct fiat_secp256k1_montgomery_scalar_non_montgomery_domain_field_element(pub [u32; 8]); + +impl std::ops::Index for fiat_secp256k1_montgomery_scalar_non_montgomery_domain_field_element { + type Output = u32; + #[inline] + fn index(&self, index: usize) -> &Self::Output { + &self.0[index] + } +} + +impl std::ops::IndexMut for fiat_secp256k1_montgomery_scalar_non_montgomery_domain_field_element { + #[inline] + fn index_mut(&mut self, index: usize) -> &mut Self::Output { + &mut self.0[index] + } +} /// The function fiat_secp256k1_montgomery_scalar_addcarryx_u32 is an addition with carry. diff --git a/fiat-rust/src/secp256k1_montgomery_scalar_64.rs b/fiat-rust/src/secp256k1_montgomery_scalar_64.rs index 98f6bfde4d..f92e6840d6 100644 --- a/fiat-rust/src/secp256k1_montgomery_scalar_64.rs +++ b/fiat-rust/src/secp256k1_montgomery_scalar_64.rs @@ -27,11 +27,43 @@ pub type fiat_secp256k1_montgomery_scalar_i2 = i8; /* The type fiat_secp256k1_montgomery_scalar_montgomery_domain_field_element is a field element in the Montgomery domain. */ /* Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] */ -pub type fiat_secp256k1_montgomery_scalar_montgomery_domain_field_element = [u64; 4]; +#[derive(Clone, Copy)] +pub struct fiat_secp256k1_montgomery_scalar_montgomery_domain_field_element(pub [u64; 4]); + +impl std::ops::Index for fiat_secp256k1_montgomery_scalar_montgomery_domain_field_element { + type Output = u64; + #[inline] + fn index(&self, index: usize) -> &Self::Output { + &self.0[index] + } +} + +impl std::ops::IndexMut for fiat_secp256k1_montgomery_scalar_montgomery_domain_field_element { + #[inline] + fn index_mut(&mut self, index: usize) -> &mut Self::Output { + &mut self.0[index] + } +} /* The type fiat_secp256k1_montgomery_scalar_non_montgomery_domain_field_element is a field element NOT in the Montgomery domain. */ /* Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] */ -pub type fiat_secp256k1_montgomery_scalar_non_montgomery_domain_field_element = [u64; 4]; +#[derive(Clone, Copy)] +pub struct fiat_secp256k1_montgomery_scalar_non_montgomery_domain_field_element(pub [u64; 4]); + +impl std::ops::Index for fiat_secp256k1_montgomery_scalar_non_montgomery_domain_field_element { + type Output = u64; + #[inline] + fn index(&self, index: usize) -> &Self::Output { + &self.0[index] + } +} + +impl std::ops::IndexMut for fiat_secp256k1_montgomery_scalar_non_montgomery_domain_field_element { + #[inline] + fn index_mut(&mut self, index: usize) -> &mut Self::Output { + &mut self.0[index] + } +} /// The function fiat_secp256k1_montgomery_scalar_addcarryx_u64 is an addition with carry. diff --git a/src/Stringification/Rust.v b/src/Stringification/Rust.v index 6a88adc44f..58f1e92cb4 100644 --- a/src/Stringification/Rust.v +++ b/src/Stringification/Rust.v @@ -45,18 +45,32 @@ Module Rust. : list string := let '(name, (ty, array_len), description) := name_and_type_and_describe_typedef prefix private typedef in ((comment_block description) - ++ [(if private then "type " else "pub type ") - ++ name ++ " = " ++ + ++ [ let ty_string := match ty with | Some ty => int_type_to_string internal_private prefix ty | None => "ℤ" (* blackboard bold Z for unbounded integers (which don't actually exist, and thus will error) *) end in + let visibility := (if private then "" else "pub ") in match array_len with - | None (* just an integer *) => ty_string - | Some None (* unknown array length *) => "*mut " ++ ty_string - | Some (Some len) => "[" ++ ty_string ++ "; " ++ Decimal.Z.to_string (Z.of_nat len) ++ "]" + | None (* just an integer *) => visibility ++ "type " ++ name ++ " = " ++ ty_string ++ ";" + | Some None (* unknown array length *) => visibility ++ "type " ++ name ++ " = *mut " ++ ty_string ++ ";" + | Some (Some len) => "#[derive(Clone, Copy)]" ++ String.NewLine + ++ visibility ++ "struct " ++ name ++ "(pub [" ++ ty_string ++ "; " ++ Decimal.Z.to_string (Z.of_nat len) ++ "]);" ++ String.NewLine ++ String.NewLine + ++ "impl std::ops::Index for " ++ name ++ " {" ++ String.NewLine + ++ " type Output = " ++ ty_string ++ ";" ++ String.NewLine + ++ " #[inline]" ++ String.NewLine + ++ " fn index(&self, index: usize) -> &Self::Output {" ++ String.NewLine + ++ " &self.0[index]" ++ String.NewLine + ++ " }" ++ String.NewLine + ++ "}" ++ String.NewLine ++ String.NewLine + ++ "impl std::ops::IndexMut for " ++ name ++ " {" ++ String.NewLine + ++ " #[inline]" ++ String.NewLine + ++ " fn index_mut(&mut self, index: usize) -> &mut Self::Output {" ++ String.NewLine + ++ " &mut self.0[index]" ++ String.NewLine + ++ " }" ++ String.NewLine + ++ "}" end - ++ ";"]%string)%list. + ]%string)%list. (* Header imports and type defs *) Definition header