spec/lib/numeric.bend checks
raw source on the hub · import bend-collections-laws-crypto@1.0.0.0/spec/lib/numeric.bend as Numeric
1 import
import Base
Definitions
def bit_value source · line 10 · raw
@b:Bool -> Nat
Independent mathematical interpretation. Nat here is a specification value; no public executable conversion of a 64-bit number through Nat is required.
def unsigned source · line 17 · raw
@n:Nat -> @w:Word(n) -> Nat
def sign_threshold source · line 26 · raw
@n:Nat -> Word(1n+n)
def negative source · line 33 · raw
@+w:Word(64n) -> Bool
def zero source · line 36 · raw
@w:Word(64n) -> Bool
def order source · line 39 · raw
@a:Word(64n) -> @b:Word(64n) -> @sign_a:Bool -> @sign_b:Bool -> Bool
def from_nat source · line 50 · raw
@n:Nat -> @+value:Nat -> Word(n)
These mathematical definitions specify modulo arithmetic through Nat values, independently of the implementation's ripple addition and binary long division.
def modulus source · line 57 · raw
Nat
def unsigned_quotient source · line 63 · raw
@n:Nat -> @word:Word(n) -> @d:U32 -> Word(n)
Observe the input constructor before evaluating mathematical division. This has the same from_nat(unsigned(input) / divisor) meaning; the structural guard keeps fixed large denominators from being expanded while input is unknown.
def negative_quotient source · line 71 · raw
@n:Nat -> @word:Word(n) -> @d:U32 -> Word(n)
def quotient_signed source · line 79 · raw
@bits:Word(64n) -> @negative:Bool -> Word(64n)
def scale_binary source · line 87 · raw
@places:Nat -> @value:Nat -> Nat
Mathematical multiplication by 2^places, specified without machine shifts.
def join source · line 95 · raw
@n:Nat -> @+m:Nat -> @a:Word(n) -> @b:Word(m) -> Word(Nat.add(n, m))
A 64-bit word from two 32-bit limbs (low first).
def pack source · line 104 · raw
@low:U32 -> @high:U32 -> Word(64n)
def mask source · line 110 · raw
@+n:Nat -> @+k:Nat -> Word(n)
The low k bits set, the rest clear.