def div_bits

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

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/spec/numeric.bend as S
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/division_quotient.bend as DQ
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32div.bend as UD
import bend-collections-laws-crypto@1.0.0.0/proofs/math/u64/u64.bend as P

285# THEOREM: div_small is the specification's unsigned 64-bit quotient.
286def div_bits(+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(a, d)) == S.unsigned_quotient(64n, P.bits(a), d) : Word(64n)}:
287  Equal.trans(Word(64n), P.bits(U.div_small(a, d)), S.from_nat(64n, P.val(U.div_small(a, d))), S.unsigned_quotient(64n, P.bits(a), d),
288    Equal.sym(Word(64n), S.from_nat(64n, P.val(U.div_small(a, d))), P.bits(U.div_small(a, d)), from_u(64n, P.bits(U.div_small(a, d)))),
289    Equal.trans(Word(64n), S.from_nat(64n, P.val(U.div_small(a, d))), S.from_nat(64n, Nat.div(P.val(a), UD.v(d))), S.unsigned_quotient(64n, P.bits(a), d),
290      Equal.cong(Nat, Word(64n), z => S.from_nat(64n, z), P.val(U.div_small(a, d)), Nat.div(P.val(a), UD.v(d)), div_value(a, d, hd0, hle)),
291      Equal.sym(Word(64n), S.unsigned_quotient(64n, P.bits(a), d), S.from_nat(64n, Nat.div(P.val(a), UD.v(d))), DQ.specification_equation(64n, P.bits(a), d))))