~/bend-docscommunity

proofs/crypto/blake/blake3/lists.bend checks

raw source on the hub · import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/lists.bend as Lists

4 imports
import Base
import ../../../lib/logic.bend as L
import ../../../lib/nat.bend as N
import ../../../../spec/lib/common.bend as SC

Definitions

def cons_cong source · line 9 · raw

@-A:Data -> @+h:A -> @+xs:List<&2, A> -> @+ys:List<&2, A> -> @e:{xs == ys : List<&2, A>} -> {h <> xs == h <> ys : List<&2, A>}

def take_drop source · line 12 · raw

@-A:Data -> @+xs:List<&2, A> -> @+k:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.append(A, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.take(A, xs, k), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.drop(A, xs, k)) == xs : List<&2, A>}

def length_drop source · line 18 · raw

@-A:Data -> @+xs:List<&2, A> -> @+k:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(A, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.drop(A, xs, k)) == Nat.sub(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(A, xs), k) : Nat}

def take_all source · line 25 · raw

@-A:Data -> @+xs:List<&2, A> -> @+k:Nat -> @+h:{Nat.is_le(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(A, xs), k) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.take(A, xs, k) == xs : List<&2, A>}

def drop_all source · line 31 · raw

@-A:Data -> @+xs:List<&2, A> -> @+k:Nat -> @+h:{Nat.is_le(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(A, xs), k) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.drop(A, xs, k) == [] : List<&2, A>}

def drop_zero source · line 37 · raw

@-A:Data -> @+ys:List<&2, A> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.drop(A, ys, 0n) == ys : List<&2, A>}

def take_zero source · line 42 · raw

@-A:Data -> @+ys:List<&2, A> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.take(A, ys, 0n) == [] : List<&2, A>}

def drop_append_left source · line 47 · raw

@-A:Data -> @+xs:List<&2, A> -> @+ys:List<&2, A> -> @+k:Nat -> @+h:{Nat.is_le(k, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(A, xs)) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.drop(A, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.append(A, xs, ys), k) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.append(A, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.drop(A, xs, k), ys) : List<&2, A>}

def take_append_left source · line 54 · raw

@-A:Data -> @+xs:List<&2, A> -> @+ys:List<&2, A> -> @+k:Nat -> @+h:{Nat.is_le(k, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(A, xs)) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.take(A, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.append(A, xs, ys), k) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.take(A, xs, k) : List<&2, A>}

def length_take source · line 61 · raw

@-A:Data -> @+xs:List<&2, A> -> @+k:Nat -> @+h:{Nat.is_le(k, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(A, xs)) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(A, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.take(A, xs, k)) == k : Nat}

def length_snoc source · line 68 · raw

@-A:Data -> @+xs:List<&2, A> -> @+x:A -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(A, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.append(A, xs, [x])) == 1n+0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(A, xs) : Nat}

def is_empty source · line 73 · raw

@-A:Data -> @xs:List<&2, A> -> Bool

def empty_drop source · line 78 · raw

@-A:Data -> @+xs:List<&2, A> -> @+k:Nat -> {is_empty(A, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.drop(A, xs, k)) == Nat.is_le(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(A, xs), k) : Bool}

def double_add source · line 85 · raw

@+p:Nat -> {Nat.double(p) == Nat.add(p, p) : Nat}

def sub_double source · line 92 · raw

@+p:Nat -> {Nat.sub(Nat.double(p), p) == p : Nat}

def lt_pow2 source · line 97 · raw

@+n:Nat -> {Nat.is_lt(n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(n)) == True{} : Bool}

2^h is strictly above h - 1, i.e. n < 2^(n+1).

def lt_pow2_succ source · line 103 · raw

@+n:Nat -> {Nat.is_lt(n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(1n+n)) == True{} : Bool}