def div_signed

bend-collections-laws-crypto@1.0.0.0 · proofs/math/u64/u64div.bend:356

import Base
import bend-collections-laws-crypto@1.0.0.0/src/math/u64.bend as U
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/src/wide.bend as W
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S
import bend-collections-laws-crypto@1.0.0.0/proofs/math/u64/u64.bend as P

356# THEOREM: div_small_signed is the specification's signed quotient
357# (truncating toward zero), for 0 < d <= 2^20.
358def div_signed(+a: U.U64, +d: U32, +hd0: {U32.is_zero(d) == False{} : Bool}, +hle: {U32.is_le(d, 1048576) == True{} : Bool}) -> {P.bits(U.div_small_signed(a, d)) == qs(P.bits(a), S.negative(P.bits(a)), d) : Word(64n)}:
359  match a:
360    case U.U64{+lo, +hi}:
361      %Equal.sym(Bool, S.negative(W.pack(lo, hi)), U32.is_ge(hi, 2147483648), P.negative_pack(lo, hi)) : {P.bits(U.div_small_signed(U.U64{lo, hi}, d)) == qs(W.pack(lo, hi), _, d) : Word(64n)}
362      signed_g(lo, hi, d, hd0, hle, U32.is_ge(hi, 2147483648), P.negative_pack(lo, hi))