~/bend-docscommunity

proofs/containers/bitlist/loops.bend checks

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

20 imports
import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../lib/list.bend as LL
import ../../../spec/lib/common.bend as SC
import ../../../src/containers/bitset.bend as B
import ../../../src/containers/bitlist.bend as BLI
import ../../../src/containers/dynamic_array.bend as D
import ../../../src/containers/types/dynamic_array.bend as DE
import ../../../spec/containers/dynamic_array.bend as DS
import ../dynamic_array/state.bend as DAS
import ../dynamic_array/steps.bend as DSP
import ../dynamic_array/trace.bend as DTR
import ../bitset/listx.bend as LX
import ../bitset/model.bend as MD
import ../bitset/walk.bend as WK
import ../bitset/state.bend as ST
import ../bitset/fastcount.bend as FC
import ./da.bend as DI
import ./bits.bend as BT

Definitions

def read_same source · line 31 · raw

@+s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<U32> -> @+gs:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(U32, s) == True{} : Bool} -> @+xs:List<&2, U32> -> @+c:Nat -> @+es:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/da.ws(s) == xs : List<&2, U32>} -> @+ec:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/da.lim(s) == c : Nat} -> @+q:Nat -> Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/da.gsh(s, gs, q)) == True{} : Bool}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/da.ws(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/da.gsh(s, gs, q)) == xs : List<&2, U32>}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/da.lim(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/da.gsh(s, gs, q)) == c : Nat}))

a read of word q: the new shadow keeps the words; the value is word q

def read_eq source · line 35 · raw

@+s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<U32> -> @+gs:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(U32, s) == True{} : Bool} -> @+xs:List<&2, U32> -> @+c:Nat -> @+es:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/da.ws(s) == xs : List<&2, U32>} -> @+ec:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/da.lim(s) == c : Nat} -> @+q:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.get(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(U32, s), q) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/da.gsh(s, gs, q)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.item_result(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(U32, xs, q))) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, U32>)}

def CountOK source · line 44 · raw

@k:Nat -> @s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<U32> -> @acc:Nat -> @q:Nat -> @xs:List<&2, U32> -> @c:Nat -> Type

def drop_none source · line 47 · raw

@-A:Data -> @+xs:List<&2, A> -> @+q:Nat -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(A, xs, q) == None{} : Maybe<&2, A>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.drop(A, xs, q) == [] : List<&2, A>}

def nth_none_succ source · line 58 · raw

@-A:Data -> @+xs:List<&2, A> -> @+q:Nat -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(A, xs, q) == None{} : Maybe<&2, A>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(A, xs, 1n+q) == None{} : Maybe<&2, A>}

def cw_none source · line 69 · raw

@+xs:List<&2, U32> -> @+k:Nat -> @+q:Nat -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(U32, xs, q) == None{} : Maybe<&2, U32>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/model.count_words(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.drop(U32, xs, q), 1n+k)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/model.count_words(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.drop(U32, xs, 1n+q), k)) : Nat}

def cw_some source · line 74 · raw

@+xs:List<&2, U32> -> @+k:Nat -> @+q:Nat -> @+x:U32 -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(U32, xs, q) == Some{x} : Maybe<&2, U32>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/model.count_words(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.drop(U32, xs, q), 1n+k)) == Nat.add(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.word_count(32n, x), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/model.count_words(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.drop(U32, xs, 1n+q), k))) : Nat}

def count_lift source · line 79 · raw

@+r:Nat -> @s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<U32> -> @+acc:Nat -> @+q:Nat -> @+xs:List<&2, U32> -> @+c:Nat -> @s1:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<U32> -> @+acc1:Nat -> @+e_step:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitlist.count_go(1n+r, (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(U32, s), acc), q) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitlist.count_go(r, (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(U32, s1), acc1), 1n+q) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>, Nat)} -> @+e_sum:{Nat.add(acc1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/model.count_words(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.drop(U32, xs, 1n+q), r))) == Nat.add(acc, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/model.count_words(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.drop(U32, xs, q), 1n+r))) : Nat} -> @ih:CountOK(r, s1, acc1, 1n+q, xs, c) -> CountOK(1n+r, s, acc, q, xs, c)

def count_rd source · line 87 · raw

@+r:Nat -> @+s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<U32> -> @+gs:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(U32, s) == True{} : Bool} -> @+xs:List<&2, U32> -> @+c:Nat -> @+es:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/da.ws(s) == xs : List<&2, U32>} -> @+ec:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/da.lim(s) == c : Nat} -> @+acc:Nat -> @+q:Nat -> @+y:Maybe<&2, U32> -> @+hy:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(U32, xs, q) == y : Maybe<&2, U32>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitlist.count_go(1n+r, (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(U32, s), acc), q) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitlist.count_go(r, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitlist.count_add((0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/da.gsh(s, gs, q)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.item_result(U32, y)), acc), 1n+q) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>, Nat)}

def count_sum source · line 94 · raw

@+acc:Nat -> @+r:Nat -> @+q:Nat -> @+xs:List<&2, U32> -> @+x:U32 -> @+hy:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(U32, xs, q) == Some{x} : Maybe<&2, U32>} -> {Nat.add(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.count_word(x, acc, U32.is_eq(x, 0)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/model.count_words(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.drop(U32, xs, 1n+q), r))) == Nat.add(acc, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/model.count_words(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.drop(U32, xs, q), 1n+r))) : Nat}

def count_y source · line 99 · raw

@+r:Nat -> @+s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<U32> -> @+gs:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(U32, s) == True{} : Bool} -> @+xs:List<&2, U32> -> @+c:Nat -> @+es:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/da.ws(s) == xs : List<&2, U32>} -> @+ec:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/da.lim(s) == c : Nat} -> @+acc:Nat -> @+q:Nat -> @+y:Maybe<&2, U32> -> @+hy:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(U32, xs, q) == y : Maybe<&2, U32>} -> @+e_rd:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitlist.count_go(1n+r, (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(U32, s), acc), q) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitlist.count_go(r, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitlist.count_add((0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/da.gsh(s, gs, q)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.item_result(U32, y)), acc), 1n+q) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>, Nat)} -> @rec:(@+a2:Nat -> @+q2:Nat -> @+s2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<U32> -> @+g2:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(U32, s2) == True{} : Bool} -> @+e2:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/da.ws(s2) == xs : List<&2, U32>} -> @+f2:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/da.lim(s2) == c : Nat} -> CountOK(r, s2, a2, q2, xs, c)) -> CountOK(1n+r, s, acc, q, xs, c)

def count_loop source · line 113 · raw

@k:Nat -> @+s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<U32> -> @+gs:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(U32, s) == True{} : Bool} -> @+xs:List<&2, U32> -> @+c:Nat -> @+es:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/da.ws(s) == xs : List<&2, U32>} -> @+ec:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/da.lim(s) == c : Nat} -> @+acc:Nat -> @+q:Nat -> CountOK(k, s, acc, q, xs, c)

def BitsOK source · line 125 · raw

@k:Nat -> @s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<U32> -> @n:Nat -> @xs:List<&2, U32> -> @c:Nat -> Type

def bits_lift source · line 128 · raw

@+q:Nat -> @s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<U32> -> @+n:Nat -> @+xs:List<&2, U32> -> @+c:Nat -> @s1:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<U32> -> @+e_step:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitlist.bits_go(1n+q, (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(U32, s), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(Bool, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.flat(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.drop(U32, xs, 1n+q)), Nat.sub(n, Nat.mul(1n+q, 32n)))), n) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitlist.bits_go(q, (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(U32, s1), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(Bool, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.flat(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.drop(U32, xs, q)), Nat.sub(n, Nat.mul(q, 32n)))), n) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>, List<&2, Bool>)} -> @ih:BitsOK(q, s1, n, xs, c) -> BitsOK(1n+q, s, n, xs, c)

def bits_rd source · line 134 · raw

@+s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<U32> -> @+gs:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(U32, s) == True{} : Bool} -> @+xs:List<&2, U32> -> @+c:Nat -> @+es:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/da.ws(s) == xs : List<&2, U32>} -> @+ec:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/da.lim(s) == c : Nat} -> @+n:Nat -> @+q:Nat -> @+hq:{Nat.is_lt(q, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, xs)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitlist.bits_go(1n+q, (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(U32, s), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(Bool, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.flat(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.drop(U32, xs, 1n+q)), Nat.sub(n, Nat.mul(1n+q, 32n)))), n) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitlist.bits_go(q, (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/da.gsh(s, gs, q)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(Bool, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.flat(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.drop(U32, xs, q)), Nat.sub(n, Nat.mul(q, 32n)))), n) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>, List<&2, Bool>)}

def bits_loop source · line 141 · raw

@k:Nat -> @+s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<U32> -> @+gs:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(U32, s) == True{} : Bool} -> @+xs:List<&2, U32> -> @+c:Nat -> @+es:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/da.ws(s) == xs : List<&2, U32>} -> @+ec:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/da.lim(s) == c : Nat} -> @+n:Nat -> @+hk:{Nat.is_le(k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, xs)) == True{} : Bool} -> BitsOK(k, s, n, xs, c)