~/bend-docscommunity

proofs/containers/bitlist/bits.bend checks

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

16 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 ../../lib/arith.bend as AT
import ../../../src/containers/bitset.bend as B
import ../../../src/containers/bitlist.bend as BLI
import ../../../src/containers/types/bitlist.bend as E
import ../../../spec/containers/bitset.bend as BS
import ../bitset/lists.bend as BL
import ../bitset/listx.bend as LX
import ../bitset/word.bend as W
import ../bitset/model.bend as MD
import ../bitset/state.bend as ST
import ../../../spec/containers/bitlist.bend as S

Definitions

def nth_false source · line 29 · raw

@+xs:List<&2, Bool> -> @+n:Nat -> @+h:{Nat.is_lt(n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs)) == True{} : Bool} -> @+ht:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/lists.allf(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.drop(Bool, xs, n)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(Bool, xs, n) == Some{False{}} : Maybe<&2, Bool>}

def allf_succ source · line 44 · raw

@+xs:List<&2, Bool> -> @+n:Nat -> @+ht:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/lists.allf(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.drop(Bool, xs, n)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/lists.allf(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.drop(Bool, xs, 1n+n)) == True{} : Bool}

def invf_succ source · line 60 · raw

@+n:Nat -> @+xs:List<&2, Bool> -> @+h:{Nat.is_lt(n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs)) == True{} : Bool} -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.invf(n, xs) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.invf(1n+n, xs) == True{} : Bool}

def push_zero source · line 64 · raw

@+n:Nat -> @+xs:List<&2, Bool> -> @+h:{Nat.is_lt(n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs)) == True{} : Bool} -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.invf(n, xs) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(Bool, xs, 1n+n) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.snoc(Bool, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(Bool, xs, n), False{}) : List<&2, Bool>}

push of a zero bit into stored space: nothing is written

def push_put source · line 68 · raw

@+n:Nat -> @+xs:List<&2, Bool> -> @+v:Bool -> @+h:{Nat.is_lt(n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(Bool, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Bool, xs, n, v), 1n+n) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.snoc(Bool, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(Bool, xs, n), v) : List<&2, Bool>}

push of any bit into stored space: bit n is written

def push_put_inv source · line 71 · raw

@+n:Nat -> @+xs:List<&2, Bool> -> @+v:Bool -> @+h:{Nat.is_lt(n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs)) == True{} : Bool} -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.invf(n, xs) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.invf(1n+n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Bool, xs, n, v)) == True{} : Bool}

def flat_snoc source · line 79 · raw

@+ws:List<&2, U32> -> @+x:U32 -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.flat(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.snoc(U32, ws, x)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Bool, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.flat(ws), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/word.ubits(x)) : List<&2, Bool>}

def sub_succ_self source · line 87 · raw

@+n:Nat -> {Nat.sub(1n+n, n) == 1n : Nat}

def first_bit source · line 94 · raw

@+v:Bool -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(Bool, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/word.ubits(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.word_put(v, 0, 0n)), 1n) == [v] : List<&2, Bool>}

def rest_zero source · line 101 · raw

@+v:Bool -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/lists.allf(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.drop(Bool, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/word.ubits(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.word_put(v, 0, 0n)), 1n)) == True{} : Bool}

def drop_append_succ source · line 108 · raw

@+xs:List<&2, Bool> -> @+ys:List<&2, Bool> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.drop(Bool, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Bool, xs, ys), 1n+0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.drop(Bool, ys, 1n) : List<&2, Bool>}

def push_new_abs source · line 116 · raw

@+ws:List<&2, U32> -> @+v:Bool -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(Bool, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.flat(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.snoc(U32, ws, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.word_put(v, 0, 0n))), 1n+0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.flat(ws))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.snoc(Bool, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(Bool, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.flat(ws), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.flat(ws))), v) : List<&2, Bool>}

the new word holds bit |F| = v in its low position, zeros above

def push_new_inv source · line 124 · raw

@+ws:List<&2, U32> -> @+v:Bool -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.invf(1n+0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.flat(ws)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.flat(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.snoc(U32, ws, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.word_put(v, 0, 0n)))) == True{} : Bool}

def pop_spec source · line 134 · raw

@+l:Maybe<&2, Nat> -> @+c:Nat -> @+ys:List<&2, Bool> -> @+b:Bool -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.pop(l, c, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.snoc(Bool, ys, b)) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.M{l, c, ys}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.OBit{Done{b}}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.Model, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Obs)}

def lt_of_inv source · line 143 · raw

@+m:Nat -> @+xs:List<&2, Bool> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.invf(1n+m, xs) == True{} : Bool} -> {Nat.is_lt(m, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs)) == True{} : Bool}

def pop_keep_inv source · line 147 · raw

@+m:Nat -> @+xs:List<&2, Bool> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.invf(1n+m, xs) == True{} : Bool} -> @+hb:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(Bool, xs, m) == Some{False{}} : Maybe<&2, Bool>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.invf(m, xs) == True{} : Bool}

a zero last bit: the stored bits stay as they are

def pop_clear_inv source · line 152 · raw

@+m:Nat -> @+xs:List<&2, Bool> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.invf(1n+m, xs) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.invf(m, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Bool, xs, m, False{})) == True{} : Bool}

a one last bit is cleared

def word_bits source · line 161 · raw

@+m:Nat -> @+x:U32 -> @+rest:List<&2, Bool> -> @+h:{Nat.is_le(m, 32n) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitlist.word_bits(m, x, rest) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Bool, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(Bool, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/word.ubits(x), m), rest) : List<&2, Bool>}

def sub_le_zero source · line 178 · raw

@+a:Nat -> @+b:Nat -> @+h:{Nat.is_le(a, b) == True{} : Bool} -> {Nat.sub(a, b) == 0n : Nat}

def sub_sub source · line 189 · raw

@+b:Nat -> @+a:Nat -> @+c:Nat -> {Nat.sub(Nat.sub(a, b), c) == Nat.sub(a, Nat.add(c, b)) : Nat}

def take_word source · line 205 · raw

@+a:List<&2, Bool> -> @+bs:List<&2, Bool> -> @+s:Nat -> @+ha:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, a) == 32n : Nat} -> @c:Bool -> @+ec:{Nat.is_lt(32n, s) == c : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(Bool, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Bool, a, bs), s) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Bool, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(Bool, a, Nat.min(32n, s)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(Bool, bs, Nat.sub(s, 32n))) : List<&2, Bool>}

the first s bits of 32 bits then more: a prefix of the word, then of the rest

def min_le source · line 223 · raw

@+a:Nat -> @+b:Nat -> {Nat.is_le(Nat.min(a, b), a) == True{} : Bool}

def bits_step source · line 236 · raw

@+ws:List<&2, U32> -> @+n:Nat -> @+q:Nat -> @+x:U32 -> @+hx:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(U32, ws, q) == Some{x} : Maybe<&2, U32>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(Bool, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.flat(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.drop(U32, ws, q)), Nat.sub(n, Nat.mul(q, 32n))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitlist.word_bits(Nat.min(32n, Nat.sub(n, Nat.mul(q, 32n))), x, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(Bool, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.flat(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.drop(U32, ws, 1n+q)), Nat.sub(n, Nat.mul(1n+q, 32n)))) : List<&2, Bool>}

word q of the first n bits: words q.. restricted to bits below n

def below_eq source · line 244 · raw

@+l:Maybe<&2, Nat> -> @+n:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitlist.below(l, n) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.below(l, n) : Bool}

def upd_snoc_end source · line 251 · raw

@+p:List<&2, Bool> -> @+x:Bool -> @+v:Bool -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Bool, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.snoc(Bool, p, x), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, p), v) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.snoc(Bool, p, v) : List<&2, Bool>}

def lt_plus source · line 258 · raw

@+k:Nat -> @+x:Nat -> {Nat.is_lt(x, Nat.add(1n+k, x)) == True{} : Bool}

def lt_mul32 source · line 265 · raw

@+a:Nat -> @+b:Nat -> @+h:{Nat.is_lt(a, b) == True{} : Bool} -> {Nat.is_lt(Nat.mul(a, 32n), Nat.mul(b, 32n)) == True{} : Bool}

def mul32_lt source · line 269 · raw

@+a:Nat -> @+b:Nat -> @c:Bool -> @+ec:{Nat.is_lt(a, b) == c : Bool} -> @+h:{Nat.is_lt(Nat.mul(a, 32n), Nat.mul(b, 32n)) == True{} : Bool} -> {Nat.is_lt(a, b) == True{} : Bool}

def mul32_nlt source · line 276 · raw

@+a:Nat -> @+b:Nat -> @c:Bool -> @+ec:{Nat.is_lt(a, b) == c : Bool} -> @+h:{Nat.is_lt(Nat.mul(a, 32n), Nat.mul(b, 32n)) == False{} : Bool} -> {Nat.is_lt(a, b) == False{} : Bool}