def dig_t

bend-collections-laws-crypto@1.0.0.0 · src/math/w64.bend:108

import Base

108# One digit of the long division by d: (r * base + g) / d and mod d, for a
109# remainder r < d < 2^32 and a digit g < base = 2^16, so every partial
110# dividend r * 2^16 + g is below 2^48 (the runtime's Nat bound). The low word
111# is taken as two 16-bit digits; the base is written 256 * 256 so the proof
112# checker never expands a 17-bit literal.
113def dig_t(+r: Nat, +base: Nat, +g: Nat) -> Nat:
114  Nat.add(Nat.mul(r, base), g)