def mod32_value

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

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

149# Mod32.value: a 64-bit value mod a nonzero U32
150def mod32_value(+a: WU.U64, +d: U32, +hd: {U32.is_zero(d) == False{} : Bool}) -> SW.Mod32.value(a, d, hd):
151  match a:
152    case WU.U64{+lo, +hi}:
153      %Equal.sym(U32, X.mod32(WU.U64{lo, hi}, d), mod32g(WU.U64{lo, hi}, d, 65536, 65535), impl_mod(WU.U64{lo, hi}, d)) : {U32.to_nat(_) == Nat.mod(SW.value(WU.U64{lo, hi}), U32.to_nat(d)) : Nat}
154      mod_inner(1n, {==}, 32n, {==}, lo, hi, d, hd, 65536, {==}, 65535, {==}, v(d), {==})