def div32_quot

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/w64div.bend:234

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/math/w64.bend as SW
import bend-collections-laws-crypto@1.0.0.0/src/math/w64.bend as X
import bend-collections-laws-crypto@1.0.0.0/src/math/u64.bend as WU

234# Div32.quot: a 64-bit value divided by a nonzero U32
235def div32_quot(+a: WU.U64, +d: U32, +hd: {U32.is_zero(d) == False{} : Bool}) -> SW.Div32.quot(a, d, hd):
236  match a:
237    case WU.U64{+lo, +hi}:
238      %Equal.sym(WU.U64, X.fst_q(X.div32(WU.U64{lo, hi}, d)), div32q_g(lo, hi, d, 65536, 65535), impl_q(lo, hi, d)) : {SW.value(_) == Nat.div(SW.value(WU.U64{lo, hi}), U32.to_nat(d)) : Nat}
239      quot_inner(1n, {==}, 32n, {==}, lo, hi, d, hd, 65536, {==}, 65535, {==}, v(d), {==})