From c0e885931cdd39be45e18fb9221fbb4a9c27bfda Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 3 Jul 2021 15:44:25 -0700 Subject: [PATCH] na --- src/math/bigfix/u256.cpp | 153 ++++++++++++++++++++++++++++++++++----- src/math/bigfix/u256.h | 18 +++-- 2 files changed, 147 insertions(+), 24 deletions(-) diff --git a/src/math/bigfix/u256.cpp b/src/math/bigfix/u256.cpp index 0a6f626cf..d9c05e34c 100644 --- a/src/math/bigfix/u256.cpp +++ b/src/math/bigfix/u256.cpp @@ -34,10 +34,71 @@ u256 u256::operator*(u256 const& other) const { return u256(result); } +u256 u256::operator<<(uint64_t sh) const { + u256 r; + if (0 == sh || sh >= 256) + ; + else if (sh >= 176) + r.m_num[3] = m_num[0] << (sh - 176); + else if (sh >= 128) { + sh -= 128; + r.m_num[2] = m_num[0] << sh; + r.m_num[3] = (m_num[1] << sh) | (m_num[0] >> (64 - sh)); + } + else if (sh >= 64) { + sh -= 64; + r.m_num[1] = m_num[0] << sh; + r.m_num[2] = (m_num[1] << sh) | (m_num[0] >> (64 - sh)); + r.m_num[3] = (m_num[2] << sh) | (m_num[1] >> (64 - sh)); + } + else { + r.m_num[0] = m_num[0] << sh; + r.m_num[1] = (m_num[1] << sh) | (m_num[0] >> (64 - sh)); + r.m_num[2] = (m_num[2] << sh) | (m_num[1] >> (64 - sh)); + r.m_num[3] = (m_num[3] << sh) | (m_num[2] >> (64 - sh)); + } + return r; +} + +u256 u256::operator>>(uint64_t sh) const { + u256 r; + if (0 == sh || sh >= 256) + ; + else if (sh >= 176) + r.m_num[0] = m_num[3] >> (sh - 176); + else if (sh >= 128) { + sh -= 128; + r.m_num[0] = (m_num[2] >> sh) | (m_num[3] << (64 - sh)); + r.m_num[1] = (m_num[3] >> sh); + } + else if (sh >= 64) { + sh -= 64; + r.m_num[0] = (m_num[1] >> sh) | (m_num[2] << (64 - sh)); + r.m_num[1] = (m_num[2] >> sh) | (m_num[3] << (64 - sh)); + r.m_num[2] = (m_num[3] >> sh); + } + else { + r.m_num[0] = (m_num[0] >> sh) | (m_num[1] << (64 - sh)); + r.m_num[1] = (m_num[1] >> sh) | (m_num[2] << (64 - sh)); + r.m_num[2] = (m_num[2] >> sh) | (m_num[3] << (64 - sh)); + r.m_num[3] = (m_num[3] >> sh); + } + return r; +} + +u256 u256::operator&(u256 const& other) const { + u256 r; + for (unsigned i = 0; i < 4; ++i) + r.m_num[i] = m_num[i] & other.m_num[i]; + return r; +} + + + u256& u256::operator*=(u256 const& other) { uint64_t result[8]; Hacl_Bignum256_mul(const_cast(m_num), const_cast(other.m_num), result); - std::uninitialized_copy(m_num, m_num + sizeof(*this), result); + std::uninitialized_copy(m_num, m_num + 4, result); return *this; } @@ -58,22 +119,34 @@ u256& u256::inv() { return *this; } +u256 u256::mod(u256 const& other) const { + if (other.is_zero()) + throw default_exception("mod 0 is not defined"); + if (other.is_one()) + return u256(); + + u256 r; + uint64_t a[8]; + a[4] = a[5] = a[6] = a[7] = 0; + + if (!other.is_even()) { + std::uninitialized_copy(m_num, m_num + 4, a); + VERIFY(Hacl_Bignum256_mod(const_cast(other.m_num), a, r.m_num)); + return r; + } + unsigned tz = other.trailing_zeros(); + u256 thz = *this >> tz; + u256 n = other >> tz; + SASSERT(!n.is_even() && n > 1); + std::uninitialized_copy(thz.m_num, thz.m_num + 4, a); + VERIFY(Hacl_Bignum256_mod(const_cast(n.m_num), a, r.m_num)); + r = r << tz; + r += *this & ((u256(1) << tz) - 1); + return r; +} + u256 u256::mul_inverse() const { NOT_IMPLEMENTED_YET(); - - /* - Write `a mod n` in `res`. - - The argument a is meant to be a 512-bit bignum, i.e. uint64_t[8]. - The argument n and the outparam res are meant to be 256-bit bignums, i.e. uint64_t[4]. - - The function returns false if any of the following preconditions are violated, - true otherwise. - • 1 < n - • n % 2 = 1 - VERIFY(Hacl_Bignum256_mod(uint64_t *n, uint64_t *a, uint64_t *res)); - */ - return *this; } @@ -88,10 +161,56 @@ unsigned u256::trailing_zeros() const { } u256 u256::gcd(u256 const& other) const { - NOT_IMPLEMENTED_YET(); - return *this; + if (is_zero()) + return other; + if (other.is_zero()) + return *this; + if (is_one()) + return *this; + if (other.is_one()) + return other; + u256 x = *this; + u256 y = other; + unsigned tz = x.trailing_zeros(); + unsigned shift = std::min(y.trailing_zeros(), tz); + x = x >> tz; + if (x == 1) + return x << shift; + if (y == 1) + return y << shift; + if (x == y) + return x << shift; + do { + tz = y.trailing_zeros(); + y = y >> tz; + if (x > y) + std::swap(x, y); + y -= x; + } + while (!y.is_zero()); + return x << shift; } + +bool u256::operator<(u256 const& other) const { + return 0 != Hacl_Bignum256_lt_mask(const_cast(m_num), const_cast(other.m_num)); +} + +bool u256::operator<(uint64_t other) const { + uint64_t _other[4]; + _other[0] = other; + _other[1] = _other[2] = _other[3] = 0; + return 0 != Hacl_Bignum256_lt_mask(const_cast(m_num), _other); +} + +bool u256::operator>(uint64_t other) const { + uint64_t _other[4]; + _other[0] = other; + _other[1] = _other[2] = _other[3] = 0; + return 0 != Hacl_Bignum256_lt_mask(_other, const_cast(m_num)); +} + + std::ostream& u256::display(std::ostream& out) const { rational n; for (unsigned i = 0; i < 4; ++i) diff --git a/src/math/bigfix/u256.h b/src/math/bigfix/u256.h index 620910734..3b13d841c 100644 --- a/src/math/bigfix/u256.h +++ b/src/math/bigfix/u256.h @@ -14,7 +14,11 @@ public: u256 operator+(u256 const& other) const { u256 r = *this; return r += other; } u256 operator-(u256 const& other) const { u256 r = *this; return r -= other; } u256 operator-() const { u256 r = *this; return r.inv(); } + u256 operator<<(uint64_t sh) const; + u256 operator>>(uint64_t sh) const; + u256 operator&(u256 const& other) const; + u256 mod(u256 const& other) const; u256 mul_inverse() const; unsigned trailing_zeros() const; u256 gcd(u256 const& other) const; @@ -27,17 +31,17 @@ public: u256& inv(); /* unary minus */ // comparisons - bool operator==(u256 const& other) const; - bool operator!=(u256 const& other) const; + bool operator==(u256 const& other) const { return m_num[0] == other.m_num[0] && m_num[1] == other.m_num[1] && m_num[2] == other.m_num[2] && m_num[3] == other.m_num[3]; } + bool operator!=(u256 const& other) const { return !(*this == other); } bool operator<(u256 const& other) const; - bool operator<=(u256 const& other) const; - bool operator>(u256 const& other) const; - bool operator>=(u256 const& other) const; + bool operator<=(u256 const& other) const { return !(other < *this); } + bool operator>(u256 const& other) const { return other < *this; } + bool operator>=(u256 const& other) const { return !(*this < other); } bool operator<(uint64_t other) const; - bool operator<=(uint64_t other) const; + bool operator<=(uint64_t other) const { return !(*this > other); } bool operator>(uint64_t other) const; - bool operator>=(uint64_t other) const; + bool operator>=(uint64_t other) const { return !(*this < other); } bool is_zero() const { return m_num[0] == 0 && m_num[1] == 0 && m_num[2] == 0 && m_num[3] == 0; } bool is_one() const { return m_num[0] == 1 && m_num[1] == 0 && m_num[2] == 0 && m_num[3] == 0; }