~/bend-docscommunity

proofs/containers/bitset/zip.bend checks

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

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 ./model.bend as MD
import ./walk.bend as WK
import ./listx.bend as LX
import ./arr.bend as AR
import ./loops.bend as LP

Definitions

def ztree source · line 20 · raw

@m:Nat -> @+k:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.WordOp -> @+d:Nat -> @+ta:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @+tb:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @+q:Nat -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd>

def zl source · line 27 · raw

@m:Nat -> @+k:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.WordOp -> @+q:Nat -> @+xs:List<&2, U32> -> @+ys:List<&2, U32> -> List<&2, U32>

def zip_go_ok source · line 36 · raw

@m:Nat -> @+k:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.WordOp -> @+d:Nat -> @+ta:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @+tb:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @+q:Nat -> @+hd:{Nat.is_lt(d, 32n) == True{} : Bool} -> @+pa:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd, d, ta) == True{} : Bool} -> @+pb:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd, d, tb) == True{} : Bool} -> @+hm:{Nat.is_le(Nat.add(q, m), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.zip_go(m, (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd, ta), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd, tb)), k, d, q) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd, ztree(m, k, d, ta, tb, q)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd, tb)) : Pair(Array<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd>, Array<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd>)}

def ztree_ws source · line 50 · raw

@m:Nat -> @+k:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.WordOp -> @+d:Nat -> @+ta:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @+tb:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @+q:Nat -> @+pa:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd, d, ta) == True{} : Bool} -> @+hm:{Nat.is_le(Nat.add(q, m), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/arr.ws(ztree(m, k, d, ta, tb, q)) == zl(m, k, q, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/arr.ws(ta), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/arr.ws(tb)) : List<&2, U32>}

def ztree_perfect source · line 60 · raw

@m:Nat -> @+k:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.WordOp -> @+d:Nat -> @+ta:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @+tb:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @+q:Nat -> @+pa:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd, d, ta) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd, d, ztree(m, k, d, ta, tb, q)) == True{} : Bool}

def zl_spec source · line 70 · raw

@m:Nat -> @+k:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.WordOp -> @+q:Nat -> @+xs:List<&2, U32> -> @+ys:List<&2, U32> -> @+hx:{Nat.add(q, m) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, xs) : Nat} -> @+hy:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, ys) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, xs) : Nat} -> {zl(m, k, q, xs, ys) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(U32, xs, q), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/model.zip_words(k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.drop(U32, xs, q), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.drop(U32, ys, q))) : List<&2, U32>}

def zl_edges source · line 98 · raw

@+k:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.WordOp -> @+xs:List<&2, U32> -> @+ys:List<&2, U32> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(U32, xs, 0n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/model.zip_words(k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.drop(U32, xs, 0n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.drop(U32, ys, 0n))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/model.zip_words(k, xs, ys) : List<&2, U32>}

def zl_full source · line 104 · raw

@+k:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.WordOp -> @+xs:List<&2, U32> -> @+ys:List<&2, U32> -> @+hy:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, ys) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, xs) : Nat} -> {zl(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, xs), k, 0n, xs, ys) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/model.zip_words(k, xs, ys) : List<&2, U32>}