spec/lib/numeric.bend source

spec/lib/numeric.bend on the hub · documented module

import Base# The 64-bit word model: a Word(n) denotes the natural number of its bits# (least significant first), and machine operations are specified through# Nat arithmetic (modulo 2^n, unsigned and signed quotients). Shared by the# src/math specs (u64, w64, hash) and by the proofs about words and U32s.# Independent mathematical interpretation. Nat here is a specification value;# no public executable conversion of a 64-bit number through Nat is required.def bit_value(b: Bool) -> Nat:  match b:    case False{}:      0n    case True{}:      1ndef unsigned(n: Nat, w: Word(n)) -> Nat:  match n:    case 0n:      0n    case 1n+p:      match w:        case WCon{b, tail}:          Nat.add(bit_value(b), Nat.double(unsigned(p, tail)))def sign_threshold(n: Nat) -> Word(1n+n):  match n:    case 0n:      WCon{True{}, WNil{}}    case 1n+p:      WCon{False{}, sign_threshold(p)}def negative(+w: Word(64n)) -> Bool:  Cmp.is_ge(Word.cmp(64n, w, sign_threshold(63n)))def zero(w: Word(64n)) -> Bool:  Cmp.is_eq(Word.cmp(64n, w, Word.zero(64n)))def order(a: Word(64n), b: Word(64n), sign_a: Bool, sign_b: Bool) -> Bool:  match sign_a sign_b:    case False{} True{}:      False{}    case True{} False{}:      True{}    case x y:      Cmp.is_le(Word.cmp(64n, a, b))# These mathematical definitions specify modulo arithmetic through Nat values,# independently of the implementation's ripple addition and binary long division.def from_nat(n: Nat, +value: Nat) -> Word(n):  match n:    case 0n:      WNil{}    case 1n+p:      WCon{Nat.is_eq(Nat.mod(value, 2n), 1n), from_nat(p, Nat.div(value, 2n))}def modulus() -> Nat:  Nat.pow(2n, 64n)# 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 unsigned_quotient(n: Nat, word: Word(n), d: U32) -> Word(n):  match n:    case 0n: WNil{}    case 1n+ +p:      match word:        case WCon{bit, tail}:          from_nat(1n+p, Nat.div(unsigned(1n+p, WCon{bit, tail}), U32.to_nat(d)))def negative_quotient(n: Nat, word: Word(n), d: U32) -> Word(n):  match n:    case 0n: WNil{}    case 1n+ +p:      match word:        case WCon{bit, tail}:          from_nat(1n+p, Nat.sub(Nat.pow(2n, 1n+p), Nat.div(Nat.sub(Nat.pow(2n, 1n+p), unsigned(1n+p, WCon{bit, tail})), U32.to_nat(d))))def quotient_signed(bits: Word(64n), negative: Bool) -> Word(64n):  match negative:    case False{}:      unsigned_quotient(64n, bits, 1000000)    case True{}:      negative_quotient(64n, bits, 1000000)# Mathematical multiplication by 2^places, specified without machine shifts.def scale_binary(places: Nat, value: Nat) -> Nat:  match places:    case 0n:      value    case 1n+p:      Nat.double(scale_binary(p, value))# A 64-bit word from two 32-bit limbs (low first).def join(n: Nat, +m: Nat, a: Word(n), b: Word(m)) -> Word(Nat.add(n, m)):  match n:    case 0n:      b    case 1n+p:      match a:        case WCon{h, tail}:          WCon{h, join(p, m, tail, b)}def pack(low: U32, high: U32) -> Word(64n):  match low high:    case U32{lo} U32{hi}:      join(32n, 32n, lo, hi)# The low k bits set, the rest clear.def mask(+n: Nat, +k: Nat) -> Word(n):  match n k:    case 0n _:      WNil{}    case 1n+p 0n:      WCon{False{}, mask(p, 0n)}    case 1n+p 1n+j:      WCon{True{}, mask(p, j)}