def red96

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

import Base
import bend-collections-laws-crypto@1.0.0.0/src/math/u64.bend as W

395# (the zero test of hi(m) only guards the digit: red96 is called with
396# hi(m) != 0; it also stops the proof checker from expanding the digit in
397# every statement that names red96)
398def red96(+xh: W.U64, +x0: U32, +m: W.U64) -> W.U64:
399  red96_z(xh, x0, m, U32.is_zero(hi(m)))