1 import Base 2 import ../../../spec/lib/common.bend as C 3 import ../../../spec/math/generic.bend as SG 4 import ../../../spec/math/fixed.bend as SF 5 import ../../../spec/math/number.bend as SN 6 import ../../../src/math/u64.bend as WU 7 import ../../../src/math/fixed.bend as F 8 import ../../lib/nat.bend as N 9 import ../../lib/u32div.bend as UD 10 import ../natural/arith.bend as R 11 import ./width.bend as WW 12 import ./shrn.bend as SHN 13 import ./u32laws.bend as LW 14 import ./fixgen.bend as G 15 16 # bit_count (Python int.bit_count, Rust count_ones) for U32 and U64 against 17 # spec/math/number.bend's ones(w, n): the 1 bits of n split at any width 18 # (ones(a + b, n) == ones(a, n) + ones(b, n >> a), Mathlib Nat.bits_append), 19 # depend only on the low a bits, and a nibble's count is the 16-entry table. 20 21 # ---- ones over a split ---- 22 23 def bit_bit(+n: Nat) -> {C.bit(C.bit(n)) == C.bit(n) : Nat}: 24 match n: 25 case 0n: 26 {==} 27 case 1n: 28 {==} 29 case 2n+ +q: 30 bit_bit(q) 31 32 def half_bit(+n: Nat) -> {C.half(C.bit(n)) == 0n : Nat}: 33 match n: 34 case 0n: 35 {==} 36 case 1n: 37 {==} 38 case 2n+ +q: 39 half_bit(q) 40 41 # only the a low bits count 42 def ones_low(+a: Nat, +n: Nat) -> {SN.ones(a, C.low(a, n)) == SN.ones(a, n) : Nat}: 43 match a: 44 case 0n: 45 {==} 46 case 1n+ +p: 47 +y = C.low(p, C.half(n)) 48 +eb = Equal.trans(Nat, C.bit(Nat.add(C.bit(n), Nat.double(y))), C.bit(C.bit(n)), C.bit(n), WW.bit_dbl(C.bit(n), y), bit_bit(n)) 49 +eh = Equal.trans(Nat, C.half(Nat.add(C.bit(n), Nat.double(y))), Nat.add(C.half(C.bit(n)), y), y, WW.half_dbl(C.bit(n), y), Equal.cong(Nat, Nat, t => Nat.add(t, y), C.half(C.bit(n)), 0n, half_bit(n))) 50 %Equal.sym(Nat, C.bit(Nat.add(C.bit(n), Nat.double(y))), C.bit(n), eb) : {Nat.add(_, SN.ones(p, C.half(Nat.add(C.bit(n), Nat.double(y))))) == Nat.add(C.bit(n), SN.ones(p, C.half(n))) : Nat} 51 %Equal.sym(Nat, C.half(Nat.add(C.bit(n), Nat.double(y))), y, eh) : {Nat.add(C.bit(n), SN.ones(p, _)) == Nat.add(C.bit(n), SN.ones(p, C.half(n))) : Nat} 52 Equal.cong(Nat, Nat, t => Nat.add(C.bit(n), t), SN.ones(p, y), SN.ones(p, C.half(n)), ones_low(p, C.half(n))) 53 54 def ones_add(+a: Nat, +b: Nat, +n: Nat) -> {SN.ones(Nat.add(a, b), n) == Nat.add(SN.ones(a, n), SN.ones(b, C.high(a, n))) : Nat}: 55 match a: 56 case 0n: 57 Equal.sym(Nat, Nat.add(0n, SN.ones(b, n)), SN.ones(b, n), Equal.trans(Nat, Nat.add(0n, SN.ones(b, n)), Nat.add(SN.ones(b, n), 0n), SN.ones(b, n), N.add_comm(0n, SN.ones(b, n)), N.add_zero(SN.ones(b, n)))) 58 case 1n+ +p: 59 +ih = ones_add(p, b, C.half(n)) 60 Equal.trans(Nat, Nat.add(C.bit(n), SN.ones(Nat.add(p, b), C.half(n))), Nat.add(C.bit(n), Nat.add(SN.ones(p, C.half(n)), SN.ones(b, C.high(p, C.half(n))))), Nat.add(Nat.add(C.bit(n), SN.ones(p, C.half(n))), SN.ones(b, C.high(p, C.half(n)))), Equal.cong(Nat, Nat, t => Nat.add(C.bit(n), t), SN.ones(Nat.add(p, b), C.half(n)), Nat.add(SN.ones(p, C.half(n)), SN.ones(b, C.high(p, C.half(n)))), ih), Equal.sym(Nat, Nat.add(Nat.add(C.bit(n), SN.ones(p, C.half(n))), SN.ones(b, C.high(p, C.half(n)))), Nat.add(C.bit(n), Nat.add(SN.ones(p, C.half(n)), SN.ones(b, C.high(p, C.half(n))))), N.add_assoc(C.bit(n), SN.ones(p, C.half(n)), SN.ones(b, C.high(p, C.half(n)))))) 61 62 # ---- U32: a nibble at a time ---- 63 64 def ones4_eq(+n: Nat, +h: {Nat.is_lt(n, 16n) == True{} : Bool}) -> {F.ones4(n) == SN.ones(4n, n) : Nat}: 65 match n: 66 case 0n: 67 {==} 68 case 1n: 69 {==} 70 case 2n: 71 {==} 72 case 3n: 73 {==} 74 case 4n: 75 {==} 76 case 5n: 77 {==} 78 case 6n: 79 {==} 80 case 7n: 81 {==} 82 case 8n: 83 {==} 84 case 9n: 85 {==} 86 case 10n: 87 {==} 88 case 11n: 89 {==} 90 case 12n: 91 {==} 92 case 13n: 93 {==} 94 case 14n: 95 {==} 96 case 15n: 97 {==} 98 case 16n+m: 99 Empty.absurd({F.ones4(16n+m) == SN.ones(4n, 16n+m) : Nat}, N.lt_zero_absurd(m, h)) 100 101 def nib_low(+x: U32) -> {U32.to_nat(U32.mod(x, 16)) == C.low(4n, U32.to_nat(x)) : Nat}: 102 Equal.trans(Nat, U32.to_nat(U32.mod(x, 16)), Nat.mod(U32.to_nat(x), 16n), C.low(4n, U32.to_nat(x)), UD.mod_nat(x, 16, {==}), Equal.sym(Nat, C.low(4n, U32.to_nat(x)), Nat.mod(U32.to_nat(x), 16n), G.low_mod(4n, U32.to_nat(x), 15n, {==}))) 103 104 def nib_ones(+x: U32) -> {F.ones4(U32.to_nat(U32.mod(x, 16))) == SN.ones(4n, U32.to_nat(x)) : Nat}: 105 +hl = Equal.trans(Bool, Nat.is_lt(U32.to_nat(U32.mod(x, 16)), 16n), Nat.is_lt(Nat.mod(U32.to_nat(x), 16n), 16n), True{}, Equal.cong(Nat, Bool, t => Nat.is_lt(t, 16n), U32.to_nat(U32.mod(x, 16)), Nat.mod(U32.to_nat(x), 16n), UD.mod_nat(x, 16, {==})), R.dm_lt(15n, U32.to_nat(x))) 106 Equal.trans(Nat, F.ones4(U32.to_nat(U32.mod(x, 16))), SN.ones(4n, U32.to_nat(U32.mod(x, 16))), SN.ones(4n, U32.to_nat(x)), ones4_eq(U32.to_nat(U32.mod(x, 16)), hl), Equal.trans(Nat, SN.ones(4n, U32.to_nat(U32.mod(x, 16))), SN.ones(4n, C.low(4n, U32.to_nat(x))), SN.ones(4n, U32.to_nat(x)), Equal.cong(Nat, Nat, t => SN.ones(4n, t), U32.to_nat(U32.mod(x, 16)), C.low(4n, U32.to_nat(x)), nib_low(x)), ones_low(4n, U32.to_nat(x)))) 107 108 # 4 k 109 def q4(k: Nat) -> Nat: 110 match k: 111 case 0n: 112 0n 113 case 1n+p: 114 Nat.add(4n, q4(p)) 115 116 def bc_go(+k: Nat, +x: U32) -> {F.u32_bc_go(k, x) == SN.ones(q4(k), U32.to_nat(x)) : Nat}: 117 match k: 118 case 0n: 119 {==} 120 case 1n+ +p: 121 +vx = U32.to_nat(x) 122 +ih = Equal.trans(Nat, F.u32_bc_go(p, U32.shrn(x, 4n)), SN.ones(q4(p), U32.to_nat(U32.shrn(x, 4n))), SN.ones(q4(p), C.high(4n, vx)), bc_go(p, U32.shrn(x, 4n)), Equal.cong(Nat, Nat, t => SN.ones(q4(p), t), U32.to_nat(U32.shrn(x, 4n)), C.high(4n, vx), SHN.shrn_high(x, 4n))) 123 +e1 = Equal.cong(Nat, Nat, t => Nat.add(t, F.u32_bc_go(p, U32.shrn(x, 4n))), F.ones4(U32.to_nat(U32.mod(x, 16))), SN.ones(4n, vx), nib_ones(x)) 124 +e2 = Equal.cong(Nat, Nat, t => Nat.add(SN.ones(4n, vx), t), F.u32_bc_go(p, U32.shrn(x, 4n)), SN.ones(q4(p), C.high(4n, vx)), ih) 125 Equal.trans(Nat, Nat.add(F.ones4(U32.to_nat(U32.mod(x, 16))), F.u32_bc_go(p, U32.shrn(x, 4n))), Nat.add(SN.ones(4n, vx), F.u32_bc_go(p, U32.shrn(x, 4n))), SN.ones(Nat.add(4n, q4(p)), vx), e1, Equal.trans(Nat, Nat.add(SN.ones(4n, vx), F.u32_bc_go(p, U32.shrn(x, 4n))), Nat.add(SN.ones(4n, vx), SN.ones(q4(p), C.high(4n, vx))), SN.ones(Nat.add(4n, q4(p)), vx), e2, Equal.sym(Nat, SN.ones(Nat.add(4n, q4(p)), vx), Nat.add(SN.ones(4n, vx), SN.ones(q4(p), C.high(4n, vx))), ones_add(4n, q4(p), vx)))) 126 127 def u32_bit_count(+a: U32) -> SF.BitCount.value(~U32, ~SG.u32_val, ~F.u32_bit_count, 32n, a): 128 bc_go(8n, a) 129 130 # ---- U64: the two limbs ---- 131 132 def 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)))