proofs/math/typed/fixbits.bend

bend-collections-laws-math@1.0.0.0 · 142 lines · 11 definitions

1import Base
2import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
3import bend-collections-laws-math@1.0.0.0/spec/math/generic.bend as SG
4import bend-collections-laws-math@1.0.0.0/spec/math/fixed.bend as SF
5import bend-collections-laws-math@1.0.0.0/spec/math/number.bend as SN
6import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
7import bend-collections-laws-math@1.0.0.0/src/math/fixed.bend as F
8import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
9import bend-collections-laws-math@1.0.0.0/proofs/lib/u32div.bend as UD
10import bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend as R
11import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW
12import bend-collections-laws-math@1.0.0.0/proofs/math/typed/shrn.bend as SHN
13import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32laws.bend as LW
14import bend-collections-laws-math@1.0.0.0/proofs/math/typed/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
23def 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
32def 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
42def 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
54def 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
64def 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
101def 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
104def 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
109def q4(k: Nat) -> Nat:
110  match k:
111    case 0n:
112      0n
113    case 1n+p:
114      Nat.add(4n, q4(p))
115
116def 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
127def 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
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)))