proofs/containers/bitset/fastcount.bend
bend-collections-laws-containers@1.0.0.0 · 88 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/logic.bend as L
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat.bend as N
4import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32alg.bend as UA
5import bend-collections-laws-containers@1.0.0.0/proofs/lib/list.bend as LL
6import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
7import bend-collections-laws-containers@1.0.0.0/src/containers/bitset.bend as B
8
9# The counting loop of src/bitset.bend (eight bits per iteration, a zero word
10# skipped) computes exactly word_count(32, w), the count proofs/bitset/word
11# relates to the bit model.
12
13def mul8(k: Nat) -> Nat:
14 match k:
15 case 0n:
16 0n
17 case 1n+p:
18 Nat.add(8n, mul8(p))
19
20# one level of re-association: (b + R) + W = b + T when R + W = T
21def reassoc(+b: Nat, +r: Nat, +w: Nat, +t: Nat, +e: {Nat.add(r, w) == t : Nat}) -> {Nat.add(Nat.add(b, r), w) == Nat.add(b, t) : Nat}:
22 Equal.trans(Nat, Nat.add(Nat.add(b, r), w), Nat.add(b, Nat.add(r, w)), Nat.add(b, t), N.add_assoc(b, r, w), Equal.cong(Nat, Nat, z => Nat.add(b, z), Nat.add(r, w), t, e))
23
24def push_end(+w: U32, +m: Nat) -> {Nat.add(Nat.add(B.bit_value(B.low(w)), Nat.add(B.bit_value(B.low(U32.shr(w))), Nat.add(B.bit_value(B.low(U32.shr(U32.shr(w)))), Nat.add(B.bit_value(B.low(U32.shr(U32.shr(U32.shr(w))))), Nat.add(B.bit_value(B.low(U32.shr(U32.shr(U32.shr(U32.shr(w)))))), Nat.add(B.bit_value(B.low(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(w))))))), Nat.add(B.bit_value(B.low(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(w)))))))), B.bit_value(B.low(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(w)))))))))))))))), B.word_count(m, U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(w)))))))))) == Nat.add(B.bit_value(B.low(w)), Nat.add(B.bit_value(B.low(U32.shr(w))), Nat.add(B.bit_value(B.low(U32.shr(U32.shr(w)))), Nat.add(B.bit_value(B.low(U32.shr(U32.shr(U32.shr(w))))), Nat.add(B.bit_value(B.low(U32.shr(U32.shr(U32.shr(U32.shr(w)))))), Nat.add(B.bit_value(B.low(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(w))))))), Nat.add(B.bit_value(B.low(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(w)))))))), Nat.add(B.bit_value(B.low(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(w))))))))), B.word_count(m, U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(w))))))))))))))))) : Nat}:
25 reassoc(B.bit_value(B.low(w)), Nat.add(B.bit_value(B.low(U32.shr(w))), Nat.add(B.bit_value(B.low(U32.shr(U32.shr(w)))), Nat.add(B.bit_value(B.low(U32.shr(U32.shr(U32.shr(w))))), Nat.add(B.bit_value(B.low(U32.shr(U32.shr(U32.shr(U32.shr(w)))))), Nat.add(B.bit_value(B.low(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(w))))))), Nat.add(B.bit_value(B.low(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(w)))))))), B.bit_value(B.low(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(w))))))))))))))), B.word_count(m, U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(w))))))))), Nat.add(B.bit_value(B.low(U32.shr(w))), Nat.add(B.bit_value(B.low(U32.shr(U32.shr(w)))), Nat.add(B.bit_value(B.low(U32.shr(U32.shr(U32.shr(w))))), Nat.add(B.bit_value(B.low(U32.shr(U32.shr(U32.shr(U32.shr(w)))))), Nat.add(B.bit_value(B.low(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(w))))))), Nat.add(B.bit_value(B.low(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(w)))))))), Nat.add(B.bit_value(B.low(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(w))))))))), B.word_count(m, U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(w)))))))))))))))), reassoc(B.bit_value(B.low(U32.shr(w))), Nat.add(B.bit_value(B.low(U32.shr(U32.shr(w)))), Nat.add(B.bit_value(B.low(U32.shr(U32.shr(U32.shr(w))))), Nat.add(B.bit_value(B.low(U32.shr(U32.shr(U32.shr(U32.shr(w)))))), Nat.add(B.bit_value(B.low(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(w))))))), Nat.add(B.bit_value(B.low(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(w)))))))), B.bit_value(B.low(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(w)))))))))))))), B.word_count(m, U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(w))))))))), Nat.add(B.bit_value(B.low(U32.shr(U32.shr(w)))), Nat.add(B.bit_value(B.low(U32.shr(U32.shr(U32.shr(w))))), Nat.add(B.bit_value(B.low(U32.shr(U32.shr(U32.shr(U32.shr(w)))))), Nat.add(B.bit_value(B.low(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(w))))))), Nat.add(B.bit_value(B.low(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(w)))))))), Nat.add(B.bit_value(B.low(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(w))))))))), B.word_count(m, U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(w))))))))))))))), reassoc(B.bit_value(B.low(U32.shr(U32.shr(w)))), Nat.add(B.bit_value(B.low(U32.shr(U32.shr(U32.shr(w))))), Nat.add(B.bit_value(B.low(U32.shr(U32.shr(U32.shr(U32.shr(w)))))), Nat.add(B.bit_value(B.low(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(w))))))), Nat.add(B.bit_value(B.low(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(w)))))))), B.bit_value(B.low(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(w))))))))))))), B.word_count(m, U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(w))))))))), Nat.add(B.bit_value(B.low(U32.shr(U32.shr(U32.shr(w))))), Nat.add(B.bit_value(B.low(U32.shr(U32.shr(U32.shr(U32.shr(w)))))), Nat.add(B.bit_value(B.low(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(w))))))), Nat.add(B.bit_value(B.low(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(w)))))))), Nat.add(B.bit_value(B.low(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(w))))))))), B.word_count(m, U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(w)))))))))))))), reassoc(B.bit_value(B.low(U32.shr(U32.shr(U32.shr(w))))), Nat.add(B.bit_value(B.low(U32.shr(U32.shr(U32.shr(U32.shr(w)))))), Nat.add(B.bit_value(B.low(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(w))))))), Nat.add(B.bit_value(B.low(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(w)))))))), B.bit_value(B.low(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(w)))))))))))), B.word_count(m, U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(w))))))))), Nat.add(B.bit_value(B.low(U32.shr(U32.shr(U32.shr(U32.shr(w)))))), Nat.add(B.bit_value(B.low(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(w))))))), Nat.add(B.bit_value(B.low(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(w)))))))), Nat.add(B.bit_value(B.low(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(w))))))))), B.word_count(m, U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(w))))))))))))), reassoc(B.bit_value(B.low(U32.shr(U32.shr(U32.shr(U32.shr(w)))))), Nat.add(B.bit_value(B.low(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(w))))))), Nat.add(B.bit_value(B.low(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(w)))))))), B.bit_value(B.low(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(w))))))))))), B.word_count(m, U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(w))))))))), Nat.add(B.bit_value(B.low(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(w))))))), Nat.add(B.bit_value(B.low(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(w)))))))), Nat.add(B.bit_value(B.low(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(w))))))))), B.word_count(m, U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(w)))))))))))), reassoc(B.bit_value(B.low(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(w))))))), Nat.add(B.bit_value(B.low(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(w)))))))), B.bit_value(B.low(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(w)))))))))), B.word_count(m, U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(w))))))))), Nat.add(B.bit_value(B.low(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(w)))))))), Nat.add(B.bit_value(B.low(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(w))))))))), B.word_count(m, U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(w))))))))))), reassoc(B.bit_value(B.low(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(w)))))))), B.bit_value(B.low(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(w))))))))), B.word_count(m, U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(w))))))))), Nat.add(B.bit_value(B.low(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(w))))))))), B.word_count(m, U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(w)))))))))), {==})))))))
26
27def wc8(k: Nat, +w: U32, +acc: Nat) -> {B.word_count_8(k, w, acc) == Nat.add(acc, B.word_count(mul8(k), w)) : Nat}:
28 match k:
29 case 0n:
30 Equal.sym(Nat, Nat.add(acc, 0n), acc, N.add_zero(acc))
31 case 1n+ +p:
32 +w8 = U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(w))))))))
33 +ih = wc8(p, w8, Nat.add(acc, B.bv8(w)))
34 Equal.trans(Nat, B.word_count_8(p, w8, Nat.add(acc, B.bv8(w))), Nat.add(Nat.add(acc, B.bv8(w)), B.word_count(mul8(p), w8)), Nat.add(acc, B.word_count(Nat.add(8n, mul8(p)), w)), ih,
35 reassoc(acc, B.bv8(w), B.word_count(mul8(p), w8), B.word_count(Nat.add(8n, mul8(p)), w), push_end(w, mul8(p))))
36
37def count_word_ok(+w: U32, +acc: Nat, z: Bool, +ez: {U32.is_eq(w, 0) == z : Bool}) -> {B.count_word(w, acc, z) == Nat.add(acc, B.word_count(32n, w)) : Nat}:
38 match z:
39 case True{}:
40 %Equal.sym(U32, w, 0, UA.eq_of(w, 0, ez)) : {acc == Nat.add(acc, B.word_count(32n, _)) : Nat}
41 Equal.sym(Nat, Nat.add(acc, 0n), acc, N.add_zero(acc))
42 case False{}:
43 wc8(4n, w, acc)
44
45# ---- members of one word ----
46
47def wm_app_go(b: Bool, +off: Nat, +m1: List<&2, Nat>, +m0: List<&2, Nat>, +rest: List<&2, Nat>, +ih: {m1 == SC.append(Nat, m0, rest) : List<&2, Nat>}) -> {B.member_pick(b, off, m1) == SC.append(Nat, B.member_pick(b, off, m0), rest) : List<&2, Nat>}:
48 match b:
49 case True{}:
50 LL.cons_cong(Nat, off, m1, SC.append(Nat, m0, rest), ih)
51 case False{}:
52 ih
53
54def wm_app(m: Nat, +w: U32, +off: Nat, +rest: List<&2, Nat>) -> {B.word_members(m, w, off, rest) == SC.append(Nat, B.word_members(m, w, off, Nil{}), rest) : List<&2, Nat>}:
55 match m:
56 case 0n:
57 {==}
58 case 1n+ +p:
59 wm_app_go(B.low(w), off, B.word_members(p, U32.shr(w), 1n+off, rest), B.word_members(p, U32.shr(w), 1n+off, Nil{}), rest, wm_app(p, U32.shr(w), 1n+off, rest))
60
61def desc_go(b: Bool, +off: Nat, +mm: List<&2, Nat>, +acc: List<&2, Nat>) -> {SC.append(Nat, SC.reverse(Nat, mm), B.member_pick(b, off, acc)) == SC.append(Nat, SC.reverse(Nat, B.member_pick(b, off, mm)), acc) : List<&2, Nat>}:
62 match b:
63 case True{}:
64 Equal.sym(List<&2, Nat>, SC.append(Nat, SC.snoc(Nat, SC.reverse(Nat, mm), off), acc), SC.append(Nat, SC.reverse(Nat, mm), Con{off, acc}), LL.snoc_append_cons(Nat, SC.reverse(Nat, mm), off, acc))
65 case False{}:
66 {==}
67
68def desc_ok(m: Nat, +w: U32, +off: Nat, +acc: List<&2, Nat>) -> {B.word_desc(m, w, off, acc) == SC.append(Nat, SC.reverse(Nat, B.word_members(m, w, off, Nil{})), acc) : List<&2, Nat>}:
69 match m:
70 case 0n:
71 {==}
72 case 1n+ +p:
73 Equal.trans(List<&2, Nat>, B.word_desc(p, U32.shr(w), 1n+off, B.member_pick(B.low(w), off, acc)), SC.append(Nat, SC.reverse(Nat, B.word_members(p, U32.shr(w), 1n+off, Nil{})), B.member_pick(B.low(w), off, acc)), SC.append(Nat, SC.reverse(Nat, B.member_pick(B.low(w), off, B.word_members(p, U32.shr(w), 1n+off, Nil{}))), acc),
74 desc_ok(p, U32.shr(w), 1n+off, B.member_pick(B.low(w), off, acc)),
75 desc_go(B.low(w), off, B.word_members(p, U32.shr(w), 1n+off, Nil{}), acc))
76
77def members_word_ok(+w: U32, +off: Nat, +rest: List<&2, Nat>, z: Bool, +ez: {U32.is_eq(w, 0) == z : Bool}) -> {B.members_word(w, off, rest, z) == B.word_members(32n, w, off, rest) : List<&2, Nat>}:
78 match z:
79 case True{}:
80 %Equal.sym(U32, w, 0, UA.eq_of(w, 0, ez)) : {rest == B.word_members(32n, _, off, rest) : List<&2, Nat>}
81 {==}
82 case False{}:
83 +mm = B.word_members(32n, w, off, Nil{})
84 %Equal.sym(List<&2, Nat>, List.reverse.go(&2, Nat, B.word_desc(32n, w, off, Nil{}), rest), SC.append(Nat, SC.reverse(Nat, B.word_desc(32n, w, off, Nil{})), rest), LL.base_rev_go(Nat, B.word_desc(32n, w, off, Nil{}), rest)) : {_ == B.word_members(32n, w, off, rest) : List<&2, Nat>}
85 %Equal.sym(List<&2, Nat>, B.word_desc(32n, w, off, Nil{}), SC.append(Nat, SC.reverse(Nat, mm), Nil{}), desc_ok(32n, w, off, Nil{})) : {SC.append(Nat, SC.reverse(Nat, _), rest) == B.word_members(32n, w, off, rest) : List<&2, Nat>}
86 %Equal.sym(List<&2, Nat>, SC.append(Nat, SC.reverse(Nat, mm), Nil{}), SC.reverse(Nat, mm), LL.append_nil(Nat, SC.reverse(Nat, mm))) : {SC.append(Nat, SC.reverse(Nat, _), rest) == B.word_members(32n, w, off, rest) : List<&2, Nat>}
87 %Equal.sym(List<&2, Nat>, SC.reverse(Nat, SC.reverse(Nat, mm)), mm, LL.spec_rev_rev(Nat, mm)) : {SC.append(Nat, _, rest) == B.word_members(32n, w, off, rest) : List<&2, Nat>}
88 Equal.sym(List<&2, Nat>, B.word_members(32n, w, off, rest), SC.append(Nat, mm, rest), wm_app(32n, w, off, rest))