~/bend-docscommunity

proofs/containers/bitset/fastcount.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitset/fastcount.bend as Fastcount

7 imports
import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../lib/u32alg.bend as UA
import ../../lib/list.bend as LL
import ../../../spec/lib/common.bend as SC
import ../../../src/containers/bitset.bend as B

Definitions

def mul8 source · line 13 · raw

@k:Nat -> Nat

def reassoc source · line 21 · raw

@+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}

one level of re-association: (b + R) + W = b + T when R + W = T

def push_end source · line 24 · raw

@+w:U32 -> @+m:Nat -> {Nat.add(Nat.add(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.bit_value(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.low(w)), Nat.add(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.bit_value(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.low(U32.shr(w))), Nat.add(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.bit_value(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.low(U32.shr(U32.shr(w)))), Nat.add(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.bit_value(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.low(U32.shr(U32.shr(U32.shr(w))))), Nat.add(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.bit_value(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.low(U32.shr(U32.shr(U32.shr(U32.shr(w)))))), Nat.add(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.bit_value(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.low(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(w))))))), Nat.add(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.bit_value(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.low(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(w)))))))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.bit_value(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.low(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(w)))))))))))))))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.word_count(m, U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(w)))))))))) == Nat.add(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.bit_value(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.low(w)), Nat.add(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.bit_value(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.low(U32.shr(w))), Nat.add(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.bit_value(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.low(U32.shr(U32.shr(w)))), Nat.add(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.bit_value(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.low(U32.shr(U32.shr(U32.shr(w))))), Nat.add(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.bit_value(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.low(U32.shr(U32.shr(U32.shr(U32.shr(w)))))), Nat.add(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.bit_value(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.low(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(w))))))), Nat.add(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.bit_value(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.low(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(w)))))))), Nat.add(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.bit_value(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.low(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(w))))))))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.word_count(m, U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(w))))))))))))))))) : Nat}

def wc8 source · line 27 · raw

@k:Nat -> @+w:U32 -> @+acc:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.word_count_8(k, w, acc) == Nat.add(acc, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.word_count(mul8(k), w)) : Nat}

def count_word_ok source · line 37 · raw

@+w:U32 -> @+acc:Nat -> @z:Bool -> @+ez:{U32.is_eq(w, 0) == z : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.count_word(w, acc, z) == Nat.add(acc, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.word_count(32n, w)) : Nat}

def wm_app_go source · line 47 · raw

@b:Bool -> @+off:Nat -> @+m1:List<&2, Nat> -> @+m0:List<&2, Nat> -> @+rest:List<&2, Nat> -> @+ih:{m1 == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, m0, rest) : List<&2, Nat>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.member_pick(b, off, m1) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.member_pick(b, off, m0), rest) : List<&2, Nat>}

def wm_app source · line 54 · raw

@m:Nat -> @+w:U32 -> @+off:Nat -> @+rest:List<&2, Nat> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.word_members(m, w, off, rest) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.word_members(m, w, off, []), rest) : List<&2, Nat>}

def desc_go source · line 61 · raw

@b:Bool -> @+off:Nat -> @+mm:List<&2, Nat> -> @+acc:List<&2, Nat> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.reverse(Nat, mm), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.member_pick(b, off, acc)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.reverse(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.member_pick(b, off, mm)), acc) : List<&2, Nat>}

def desc_ok source · line 68 · raw

@m:Nat -> @+w:U32 -> @+off:Nat -> @+acc:List<&2, Nat> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.word_desc(m, w, off, acc) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.reverse(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.word_members(m, w, off, [])), acc) : List<&2, Nat>}

def members_word_ok source · line 77 · raw

@+w:U32 -> @+off:Nat -> @+rest:List<&2, Nat> -> @z:Bool -> @+ez:{U32.is_eq(w, 0) == z : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.members_word(w, off, rest, z) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.word_members(32n, w, off, rest) : List<&2, Nat>}