bend-collections

Search uses release 1.0.0.0 · 4,483 definitions

Releases (1)

1.0.0.0 indexed

Definitions (4,483)

src/math/w64.bend

def mul_32_64_finthe product of a U32 and a U64 as (low 64 bits, top 32 bits)
def mul_32_64
def over96the 96-bit product p exceeds x = xh * 2^64 + xl
def q_fixq - 1 while q * b > x: at most q steps (fuel q + 1)
def q_startfloor(x / b) from an estimate q >= floor(x / b): down while q * b > x (at most q steps, fuel q + 1)
def est_loKnuth's estimate for x = xh * 2^64 + xl < b * 2^32 and b >= 2^32, t = bits(hi(b)): with Y = x >> t (below 2^64) and B = b >> t in [2^31, 2^32), min(floor(Y / B), 2^32 - 1) is at least floor(x / b) (as B 2^t <= b) and at most 2 over it (Theorem B), so q_start takes a step or two
def est_mid
def est_pickmin(floor(y / d), 2^32 - 1) for d > 0: when hi(y) >= d the quotient needs more than 32 bits; otherwise the high word is its own remainder, and div32's two 16-bit Nat digit steps finish the division without dividing the high word.
def est32
def q_est
def q96floor(x / b) for x = xh * 2^64 + xl < b * 2^32 and b >= 2^32, t = bits(hi(b))
def dm_small
def dm_big
def dm_pick
def divmod(a / b, a mod b) for b > 0
def pfst
def psnd
def quot
def rem
def red96_zx mod m for x = xh * 2^32 + x0 with xh < m and m >= 2^32
def red96(the zero test of hi(m) only guards the digit: red96 is called with hi(m) != 0; it also stops the proof checker from expanding the digit in every statement that names red96)
def mul128_fin
def mul128_mid
def mul128the full product as (low 64 bits, high 64 bits)
def mm_big
def mm_pick
def mulmoda * b mod m for a, b < m
def down32r - 1 while r * r > x: from r <= 65535 at most r steps (fuel r + 1), and r * r never wraps
def up_ok
def up32r + 1 while r < 65535 and (r + 1)^2 <= x: at most 65535 - r steps
def isqrt32_fix
def isqrt32_estfloor(sqrt(x)) from any estimate r <= 65535: down while r^2 > x, then up while (r + 1)^2 <= x.
def isqrt32
def sq_over
def down64
def up64_ok
def up64
def isqrt64_fix
def isqrt_newtonfloor(sqrt(n)) from any estimate r1: down while r^2 > n, then up while (r + 1)^2 <= n; the fuel covers any estimate
def isqrt_bigone Newton step from the F32 estimate r0 > 0 lands within a few units of floor(sqrt(n)); the correction makes the result exact for any r0
def f32_clamp32
def isqrt_est
def isqrt_pick
def isqrt
def w_pow2
def or_bit
def jam_pick
def shr_jama >> k with the bits shifted out OR-ed into bit 0 (SoftFloat's shiftRightJam64)
def clz_pick
def clzthe number of leading zero bits of a (64 for 0)
def clear0a with bit 0 cleared when b
def cmp_pick
def cmp
def inv_stepx (2 - m x): doubles the correct low bits of an inverse of m mod 2^64
def minv-1 / m mod 2^64 for odd m (m is its own inverse mod 8; five Newton steps reach 96 >= 64 bits)
def sub_if
def redc_r
def redc_p
def redct / 2^64 mod m for t = (tl, th) < m^2
def monta b / 2^64 mod m for a, b < m
def mbit
def mpow_gopow_mod_go of generic.bend on Montgomery forms x 2^64 mod m
def to_montx 2^64 mod m for x < m, m >= 2^32
def mont_okm odd with 2^32 <= m < 2^63 and m minv(m) = -1 mod 2^64 (always so for odd m; checked, so the proof needs no Hensel lemma)
def mpow_m
def mpowb^e mod m for b < m and mont_ok(m)
def inv32_step
def minv32-1 / m mod 2^32 for odd m
def sub_if32
def redc32_r
def redc32_s
def redc32_p
def redc32
def mont32
def mbit32
def mpow32_go
def mont32_ok
def mpow32_m
def mpow32
def small2a and b fit 48 bits (runtime Nats) and a has more than 16: the binary gcd then hands them to Euclid on Nat (native division); below 2^16 its few steps are cheaper
def n48
def of48_hthe words of g < 2^64 from h = g div 2^32 (two divisions by 2^16, so no closed 2^32 appears: the proof checker would expand it in unary)
def of48