~/bend-docscommunity

proofs/containers/bitset/loops.bend checks

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

12 imports
import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../lib/list.bend as LL
import ../../lib/array.bend as A
import ../../../spec/lib/common.bend as SC
import ../../../src/containers/bitset.bend as B
import ./fastcount.bend as FC
import ./model.bend as MD
import ./walk.bend as WK
import ./listx.bend as LX
import ./arr.bend as AR

Definitions

def lt_of_sum source · line 19 · raw

@+q:Nat -> @+r:Nat -> @+p:Nat -> @+h:{Nat.is_le(Nat.add(q, 1n+r), p) == True{} : Bool} -> {Nat.is_lt(q, p) == True{} : Bool}

q + (1 + r) <= P => q < P

def le_of_sum source · line 25 · raw

@+q:Nat -> @+r:Nat -> @+p:Nat -> @+h:{Nat.is_le(Nat.add(q, 1n+r), p) == True{} : Bool} -> {Nat.is_le(Nat.add(1n+q, r), p) == True{} : Bool}

def head_at source · line 29 · raw

@+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @+q:Nat -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd, d, t) == True{} : Bool} -> @+hq:{Nat.is_lt(q, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.drop(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/arr.ws(t), q) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/walk.nthw(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/arr.ws(t), q) <> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.drop(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/arr.ws(t), 1n+q) : List<&2, U32>}

The word at q, as the head of what remains from q.

def count_go_ok source · line 37 · raw

@m:Nat -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @+q:Nat -> @+acc:Nat -> @+hd:{Nat.is_lt(d, 32n) == True{} : Bool} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd, d, t) == True{} : Bool} -> @+hm:{Nat.is_le(Nat.add(q, m), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.count_go(m, (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd, t), acc), d, q) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd, t), Nat.add(acc, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/model.count_words(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.drop(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/arr.ws(t), q), m)))) : Pair(Array<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd>, Nat)}

def full_range source · line 51 · raw

@+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd, d, t) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.drop(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/arr.ws(t), 0n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/arr.ws(t) : List<&2, U32>}

def take_full source · line 56 · raw

@+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd, d, t) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/arr.ws(t), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/arr.ws(t) : List<&2, U32>}

def count_ok source · line 60 · raw

@+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @+hd:{Nat.is_lt(d, 32n) == True{} : Bool} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd, d, t) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.count_go(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d), (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd, t), 0n), d, 0n) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd, t), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/model.count_words(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/arr.ws(t))) : Pair(Array<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd>, Nat)}

def mw_acc source · line 72 · raw

@ws:List<&2, U32> -> @+off:Nat -> @acc:List<&2, Nat> -> List<&2, Nat>

members_words with an explicit tail, which is the shape members_go builds.

def mw_nil source · line 79 · raw

@ws:List<&2, U32> -> @+off:Nat -> {mw_acc(ws, off, []) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/model.members_words(ws, off) : List<&2, Nat>}

def off_shift source · line 88 · raw

@+x:Nat -> @+off:Nat -> {Nat.add(x, Nat.add(32n, off)) == Nat.add(Nat.add(32n, x), off) : Nat}

def mw_snoc source · line 93 · raw

@zs:List<&2, U32> -> @+off:Nat -> @+w:U32 -> @acc:List<&2, Nat> -> {mw_acc(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.snoc(U32, zs, w), off, acc) == mw_acc(zs, off, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.word_members(32n, w, Nat.add(Nat.mul(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, zs), 32n), off), acc)) : List<&2, Nat>}

def take_len source · line 104 · raw

@+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @+r:Nat -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd, d, t) == True{} : Bool} -> @+hr:{Nat.is_lt(r, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/arr.ws(t), r)) == r : Nat}

def members_go_ok source · line 110 · raw

@m:Nat -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @+acc:List<&2, Nat> -> @+hd:{Nat.is_lt(d, 32n) == True{} : Bool} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd, d, t) == True{} : Bool} -> @+hm:{Nat.is_le(m, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.members_go(m, (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd, t), acc), d) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd, t), mw_acc(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/arr.ws(t), m), 0n, acc)) : Pair(Array<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd>, List<&2, Nat>)}

def to_list_ok source · line 128 · raw

@+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @+hd:{Nat.is_lt(d, 32n) == True{} : Bool} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd, d, t) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.members_go(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d), (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd, t), []), d) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd, t), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/model.members_words(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/arr.ws(t), 0n)) : Pair(Array<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd>, List<&2, Nat>)}