def u64_bit_count

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/fixbits.bend:132

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/spec/math/generic.bend as SG
import bend-collections-laws-math@1.0.0.0/spec/math/fixed.bend as SF
import bend-collections-laws-math@1.0.0.0/spec/math/number.bend as SN
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
import bend-collections-laws-math@1.0.0.0/src/math/fixed.bend as F
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32laws.bend as LW

132def u64_bit_count(+a: WU.U64) -> SF.BitCount.value(~WU.U64, ~SG.u64_val, ~F.u64_bit_count, 64n, a):
133  match a:
134    case WU.U64{+l, +h}:
135      +vl = U32.to_nat(l)
136      +vh = U32.to_nat(h)
137      +n = Nat.add(vl, C.shift(32n, vh))
138      +e1 = Equal.trans(Nat, SN.ones(32n, vl), SN.ones(32n, C.low(32n, n)), SN.ones(32n, n), Equal.cong(Nat, Nat, t => SN.ones(32n, t), vl, C.low(32n, n), Equal.sym(Nat, C.low(32n, n), vl, WW.low_u(32n, vl, vh, LW.vb(l)))), ones_low(32n, n))
139      +e2 = Equal.cong(Nat, Nat, t => SN.ones(32n, t), vh, C.high(32n, n), Equal.sym(Nat, C.high(32n, n), vh, WW.high_u(32n, vl, vh, LW.vb(l))))
140      +e3 = Equal.trans(Nat, Nat.add(F.u32_bit_count(l), F.u32_bit_count(h)), Nat.add(SN.ones(32n, vl), F.u32_bit_count(h)), Nat.add(SN.ones(32n, vl), SN.ones(32n, vh)), Equal.cong(Nat, Nat, t => Nat.add(t, F.u32_bit_count(h)), F.u32_bit_count(l), SN.ones(32n, vl), bc_go(8n, l)), Equal.cong(Nat, Nat, t => Nat.add(SN.ones(32n, vl), t), F.u32_bit_count(h), SN.ones(32n, vh), bc_go(8n, h)))
141      +e4 = Equal.trans(Nat, Nat.add(SN.ones(32n, vl), SN.ones(32n, vh)), Nat.add(SN.ones(32n, n), SN.ones(32n, vh)), Nat.add(SN.ones(32n, n), SN.ones(32n, C.high(32n, n))), Equal.cong(Nat, Nat, t => Nat.add(t, SN.ones(32n, vh)), SN.ones(32n, vl), SN.ones(32n, n), e1), Equal.cong(Nat, Nat, t => Nat.add(SN.ones(32n, n), t), SN.ones(32n, vh), SN.ones(32n, C.high(32n, n)), e2))
142      Equal.trans(Nat, Nat.add(F.u32_bit_count(l), F.u32_bit_count(h)), Nat.add(SN.ones(32n, n), SN.ones(32n, C.high(32n, n))), SN.ones(Nat.add(32n, 32n), n), Equal.trans(Nat, Nat.add(F.u32_bit_count(l), F.u32_bit_count(h)), Nat.add(SN.ones(32n, vl), SN.ones(32n, vh)), Nat.add(SN.ones(32n, n), SN.ones(32n, C.high(32n, n))), e3, e4), Equal.sym(Nat, SN.ones(Nat.add(32n, 32n), n), Nat.add(SN.ones(32n, n), SN.ones(32n, C.high(32n, n))), ones_add(32n, 32n, n)))