def rne_up
import bend-collections-laws-crypto@1.0.0.0/spec/math/f64.bend as F64import 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)))))