def rne_up

bend-collections-laws-crypto@1.0.0.0 · spec/math/f64.bend:148

import bend-collections-laws-crypto@1.0.0.0/spec/math/f64.bend as F64
import Base

148# m / 2^k rounded to nearest, ties to even: the quotient q, the remainder
149# r and half the divisor h
150def rne_up(+q: Nat, +r: Nat, +h: Nat) -> Nat:
151  Nat.add(q, b2n(Bool.or(Nat.is_lt(h, r), Bool.and(Nat.is_eq(r, h), Nat.is_eq(Nat.mod(q, 2n), 1n)))))

Uses (8)

Used by (1)