def signed_g

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

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

342def signed_g(+lo: U32, +hi: U32, +d: U32, +hd0: {U32.is_zero(d) == False{} : Bool}, +hle: {U32.is_le(d, 1048576) == True{} : Bool}, +g: Bool, +hg: {S.negative(W.pack(lo, hi)) == g : Bool}) -> {P.bits(U.div_sign(U.U64{lo, hi}, d, g)) == qs(W.pack(lo, hi), g, d) : Word(64n)}:
343  match g:
344    case False{}:
345      div_bits(U.U64{lo, hi}, d, hd0, hle)
346    case True{}:
347      +a = {U.U64{lo, hi} : U.U64}
348      +r = U.div_small(U.neg(a), d)
349      Equal.trans(Word(64n), P.bits(U.neg(r)), Word.inc(64n, Word.not(64n, P.bits(r))), S.negative_quotient(64n, W.pack(lo, hi), d), P.neg(r),
350        Equal.trans(Word(64n), Word.inc(64n, Word.not(64n, P.bits(r))), Word.inc(64n, Word.not(64n, S.unsigned_quotient(64n, P.bits(U.neg(a)), d))), S.negative_quotient(64n, W.pack(lo, hi), d),
351          Equal.cong(Word(64n), Word(64n), z => Word.inc(64n, Word.not(64n, z)), P.bits(r), S.unsigned_quotient(64n, P.bits(U.neg(a)), d), div_bits(U.neg(a), d, hd0, hle)),
352          Equal.trans(Word(64n), Word.inc(64n, Word.not(64n, S.unsigned_quotient(64n, P.bits(U.neg(a)), d))), Word.inc(64n, Word.not(64n, S.unsigned_quotient(64n, Word.inc(64n, Word.not(64n, W.pack(lo, hi))), d))), S.negative_quotient(64n, W.pack(lo, hi), d),
353            Equal.cong(Word(64n), Word(64n), z => Word.inc(64n, Word.not(64n, S.unsigned_quotient(64n, z, d))), P.bits(U.neg(a)), Word.inc(64n, Word.not(64n, W.pack(lo, hi))), P.neg(a)),
354            neg_quot(64n, W.pack(lo, hi), d, nz_neg(W.pack(lo, hi), hg)))))