From 9267f6cebe4cc89e4c29ce428e75ba076f744b95 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 5 Aug 2021 13:44:01 -0700 Subject: [PATCH] start u128 Signed-off-by: Nikolaj Bjorner --- src/math/bigfix/CMakeLists.txt | 1 + src/math/bigfix/u128.cpp | 218 +++++++++++++++++++++++++++++++++ src/math/bigfix/u128.h | 81 ++++++++++++ 3 files changed, 300 insertions(+) create mode 100644 src/math/bigfix/u128.cpp create mode 100644 src/math/bigfix/u128.h diff --git a/src/math/bigfix/CMakeLists.txt b/src/math/bigfix/CMakeLists.txt index cc9f23aca..db8319eea 100644 --- a/src/math/bigfix/CMakeLists.txt +++ b/src/math/bigfix/CMakeLists.txt @@ -3,6 +3,7 @@ z3_add_component(bigfix Hacl_Bignum.c Hacl_Bignum256.c u256.cpp + u128.cpp COMPONENT_DEPENDENCIES util ) diff --git a/src/math/bigfix/u128.cpp b/src/math/bigfix/u128.cpp new file mode 100644 index 000000000..b13397d18 --- /dev/null +++ b/src/math/bigfix/u128.cpp @@ -0,0 +1,218 @@ +#include "util/mpn.h" +#include "math/bigfix/u128.h" +#include "math/bigfix/Hacl_Bignum256.h" +#include + +#if 0 + +u128::u128() { + NOT_IMPLEMENTED_YET(); + // m_num = 0; +} + +u128::u128(uint64_t n) { + NOT_IMPLEMENTED_YET(); +// m_num = n; +} + +u128::u128(int n) { + NOT_IMPLEMENTED_YET(); + SASSERT(n >= 0); +// m_num = n; +} + +u128::u128(rational const& n) { + NOT_IMPLEMENTED_YET(); +#if 0 + for (unsigned i = 0; i < 2; ++i) { + m_num[i] = 0; + for (unsigned j = 0; j < 64; ++j) + m_num[i] |= n.get_bit(i * 64 + j) << j; + } +#endif +} + + +u128::u128(uint64_t const* v) { + std::uninitialized_copy(v, v + 2, m_num); +} + +u128 u128::operator*(u128 const& other) const { + NOT_IMPLEMENTED_YET(); + return u128(); +} + +u128 u128::operator<<(uint64_t sh) const { + u128 r; + NOT_IMPLEMENTED_YET(); + // TODO + return r; +} + +u128 u128::operator>>(uint64_t sh) const { + u128 r; + NOT_IMPLEMENTED_YET(); + // TODO + return r; +} + +u128 u128::operator&(u128 const& other) const { + u128 r; + NOT_IMPLEMENTED_YET(); + // TODO + return r; +} + +u128& u128::operator*=(u128 const& other) { + NOT_IMPLEMENTED_YET(); + // TODO + return *this; +} + +u128& u128::operator+=(u128 const& other) { + // TODO + NOT_IMPLEMENTED_YET(); + return *this; +} + +u128& u128::operator-=(u128 const& other) { + // TODO + NOT_IMPLEMENTED_YET(); + return *this; +} + +u128& u128::uminus() { + // TODO + NOT_IMPLEMENTED_YET(); + return *this; +} + +u128 u128::mod(u128 const& other) const { + if (other.is_zero()) + throw default_exception("mod 0 is not defined"); + if (other.is_one()) + return u128(); + + // TODO + + u128 r; + uint64_t a[8]; + a[4] = a[5] = a[6] = a[7] = 0; + NOT_IMPLEMENTED_YET(); + + 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; + } + + // claim: + // a mod 2^k*b = ((a >> k) mod b) << k | (a & ((1 << k) - 1)) + + unsigned tz = other.trailing_zeros(); + u128 thz = *this >> tz; + u128 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 & ((u128(1) << tz) - 1); + return r; +} + +u128 u128::mul_inverse() const { + if (is_zero()) + return *this; + if (is_one()) + return *this; + if (is_even()) + return (*this >> trailing_zeros()).mul_inverse(); + + u128 t0(1); + u128 t1(-t0); + u128 r0(*this); + u128 r1(-r0); + while (!r1.is_zero()) { + u128 q = r0 / r1; + u128 tmp = t1; + t1 = t0 - q * t1; + t0 = tmp; + tmp = r1; + r1 = r0 - q * r1; + r0 = tmp; + } + return t0; +} + +unsigned u128::trailing_zeros() const { + unsigned r = 0; + // TODO + return r; +} + +u128 u128::gcd(u128 const& other) const { + if (is_zero()) + return other; + if (other.is_zero()) + return *this; + if (is_one()) + return *this; + if (other.is_one()) + return other; + u128 x = *this; + u128 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 u128::operator<(uint64_t other) const { + // TODO + NOT_IMPLEMENTED_YET(); + return false; +} + +bool u128::operator>(uint64_t other) const { + // TODO + NOT_IMPLEMENTED_YET(); + return false; +} + +rational u128::to_rational() const { + rational n; + // TODO + NOT_IMPLEMENTED_YET(); + return n; +} + +std::ostream& u128::display(std::ostream& out) const { + return out << to_rational(); +} + +// mpn implements the main functionality needed for unsigned fixed-point arithmetic +// we could use mpn for add/sub/mul as well and maybe punt on Hacl dependency. + +u128 u128::operator/(u128 const& other) const { + u128 result; + // TODO + NOT_IMPLEMENTED_YET(); + return result; +} + +#endif \ No newline at end of file diff --git a/src/math/bigfix/u128.h b/src/math/bigfix/u128.h new file mode 100644 index 000000000..8ba7ce9b4 --- /dev/null +++ b/src/math/bigfix/u128.h @@ -0,0 +1,81 @@ +#pragma once + +#include "util/util.h" +#include "util/rational.h" +#include "math/bigfix/FStar_UInt128.h" + +#if 0 +class u128 { + FStar_UInt128_uint128 m_num; + u128(uint64_t const* v); +public: + u128(); + u128(uint64_t n); + u128(int n); + u128(rational const& n); + rational to_rational() const; + u128& operator=(uint64_t n) { + *this = u128(n); + return *this; + } + u128 operator*(u128 const& other) const; + u128 operator+(u128 const& other) const { u128 r = *this; return r += other; } + u128 operator-(u128 const& other) const { u128 r = *this; return r -= other; } + u128 operator/(u128 const& other) const; + u128 operator-() const { u128 r = *this; return r.uminus(); } + u128 operator<<(uint64_t sh) const; + u128 operator>>(uint64_t sh) const; + u128 operator&(u128 const& other) const; + + u128 mod(u128 const& other) const; + u128 mul_inverse() const; + unsigned trailing_zeros() const; + u128 gcd(u128 const& other) const; + + // updates + void reset(); // { m_num = 0; } + u128& operator+=(u128 const& other); + u128& operator*=(u128 const& other); + u128& operator-=(u128 const& other); + u128& operator/=(u128 const& other) { *this = *this / other; return *this; } + u128& operator>>=(uint64_t sh) { *this = *this >> sh; return *this; } + u128& operator<<=(uint64_t sh) { *this = *this << sh; return *this; } + u128& uminus(); /* unary minus */ + + // comparisons + bool operator==(u128 const& other) const { return FStar_UInt128_eq(m_num, other.m_num); } + bool operator!=(u128 const& other) const { return !(*this == other); } + bool operator<(u128 const& other) const { return FStar_UInt128_lt(m_num, other.m_num); } + bool operator<=(u128 const& other) const { return !(other < *this); } + bool operator>(u128 const& other) const { return other < *this; } + bool operator>=(u128 const& other) const { return !(*this < other); } + + bool operator==(uint64_t other) const; // { return m_num == other; } + bool operator!=(uint64_t other) const { return !(*this == other); } + + 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 { return !(*this < other); } + + bool is_zero() const { return *this == 0; } + bool is_one() const { return *this == 1; } + bool is_even() const; // { return (m_num & 1) == 0; } + + std::ostream& display(std::ostream& out) const; + +}; + +inline std::ostream& operator<<(std::ostream& out, u128 const& u) { + return u.display(out); +} + +inline bool operator<(uint64_t n, u128 const& y) { return y > n; } +inline bool operator<=(uint64_t n, u128 const& y) { return y >= n; } +inline bool operator>(uint64_t n, u128 const& y) { return y < n; } +inline unsigned trailing_zeros(u128 const& n) { return n.trailing_zeros(); } + +inline u128 operator-(uint64_t n, u128 const& y) { return u128(n) - y; } +inline bool operator>=(uint64_t n, u128 const& y) { return y <= n; } +inline rational to_rational(u128 const& x) { return x.to_rational(); } +#endif \ No newline at end of file