~/bend-docscommunity

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

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

10 imports
import Base
import ../../../../src/crypto/blake/blake3/types.bend as T
import ../../../../src/crypto/blake/blake3/compress.bend as C
import ../../../../src/crypto/blake/blake3/blake3.bend as K
import ../../../lib/logic.bend as L
import ../../../lib/nat.bend as N
import ../../../../spec/lib/common.bend as SC
import ../../../../spec/crypto/blake/blake3.bend as S
import ./compress.bend as P
import ./lists.bend as LS

Definitions

def out_cv_correct source · line 24 · raw

@+o:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.out_cv(o) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.cv(o) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.CV}

def parent_block_correct source · line 28 · raw

@+l:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.CV -> @+r:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.CV -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.parent_block(l, r) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.block_of(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.append(U32, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.cv_words(l), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.cv_words(r))) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Block}

def iv_correct source · line 32 · raw

{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.iv == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.cv_of(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.iv) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.CV}

def parent_out_correct source · line 35 · raw

@+l:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.CV -> @+r:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.CV -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.parent_out(l, r) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.parent(l, r) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out}

def parent_cv_correct source · line 39 · raw

@+l:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.CV -> @+r:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.CV -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.parent_cv(l, r) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.cv(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.parent(l, r)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.CV}

def emps source · line 55 · raw

@h:Nat -> @y:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.Stack -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.Stack

h empty slots below y.

def E source · line 61 · raw

@+h:Nat -> @t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.Stack -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.Stack

The stack t with h empty slots below it (the empty stack stays empty).

def lift source · line 67 · raw

@t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.Stack -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.Stack

def pushes source · line 73 · raw

@cs:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.CV> -> @s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.Stack -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.Stack

def push_all source · line 79 · raw

@s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.Stack -> @cs:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.CV> -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.Stack

Pushes the chaining values cs in order.

def cvs source · line 82 · raw

@xs:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out> -> List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.CV>

def E_succ source · line 87 · raw

@+g:Nat -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.Stack -> {E(1n+g, t) == E(g, lift(t)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.Stack}

def E_zero source · line 93 · raw

@+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.Stack -> {E(0n, t) == t : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.Stack}

def push_lift source · line 99 · raw

@+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.Stack -> @+c:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.CV -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.push(lift(t), c) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.SFull{c, t} : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.Stack}

def lift_push source · line 105 · raw

@+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.Stack -> @+c:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.CV -> {lift(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.push(t, c)) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.SEmpty{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.push(t, c)} : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.Stack}

def finish_lift source · line 111 · raw

@+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.Stack -> @+o:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.finish(lift(t), o) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.finish(t, o) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out}

def pushes_append source · line 117 · raw

@+xs:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.CV> -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.Stack -> @+ys:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.CV> -> {push_all(s, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.append(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.CV, xs, ys)) == push_all(push_all(s, xs), ys) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.Stack}

def push_all_append source · line 122 · raw

@+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.Stack -> @+xs:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.CV> -> @+ys:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.CV> -> {push_all(s, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.append(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.CV, xs, ys)) == push_all(push_all(s, xs), ys) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.Stack}

def cvs_append source · line 125 · raw

@+xs:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out> -> @+ys:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out> -> {cvs(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.append(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out, xs, ys)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.append(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.CV, cvs(xs), cvs(ys)) : List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.CV>}

def push_split source · line 131 · raw

@+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.Stack -> @+xs:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out> -> @+ys:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out> -> {push_all(s, cvs(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.append(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out, xs, ys))) == push_all(push_all(s, cvs(xs)), cvs(ys)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.Stack}

Pushing the chaining values of xs ++ ys.

def tree_con source · line 137 · raw

@+g:Nat -> @+xs:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out> -> @+ne:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.is_nil(xs) == False{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.tree(1n+g, xs) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.join(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.tree(g, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.take(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out, xs, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(g))), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.tree(g, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.drop(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out, xs, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(g))), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.is_nil(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.drop(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out, xs, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(g)))) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out}

def nil_is_empty source · line 142 · raw

@+xs:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.is_nil(xs) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/blake/blake3/lists.is_empty(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out, xs) : Bool}

def snoc_ne source · line 147 · raw

@+xs:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out> -> @+o:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.is_nil(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.append(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out, xs, [o])) == False{} : Bool}

def len_ne source · line 152 · raw

@+xs:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out> -> @+n:Nat -> @+h:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out, xs) == 1n+n : Nat} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.is_nil(xs) == False{} : Bool}

def drop_nil source · line 158 · raw

@+xs:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out> -> @+k:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.is_nil(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.drop(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out, xs, k)) == Nat.is_le(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out, xs), k) : Bool}

The drop is empty exactly when the list fits.

def join_false source · line 162 · raw

@+l:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out -> @+r:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.join(l, r, False{}) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.parent(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.cv(l), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.cv(r)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out}

def zero_pow source · line 165 · raw

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

def pow_ne source · line 169 · raw

@+xs:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out> -> @+p:Nat -> @+hl:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out, xs) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(p) : Nat} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.is_nil(xs) == False{} : Bool}

def half_len_take source · line 177 · raw

@+xs:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out> -> @+g:Nat -> @+hl:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out, xs) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(1n+g) : Nat} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.take(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out, xs, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(g))) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(g) : Nat}

The two halves of a list of 2^(g+1) outputs.

def half_len_drop source · line 181 · raw

@+xs:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out> -> @+g:Nat -> @+hl:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out, xs) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(1n+g) : Nat} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.drop(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out, xs, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(g))) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(g) : Nat}

def half_not_nil source · line 186 · raw

@+xs:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out> -> @+g:Nat -> @+hl:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out, xs) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(1n+g) : Nat} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.is_nil(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.drop(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out, xs, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(g))) == False{} : Bool}

def complete_step source · line 191 · raw

@+g:Nat -> @+xs:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out> -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.Stack -> @ne:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.is_nil(xs) == False{} : Bool} -> @nd:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.is_nil(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.drop(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out, xs, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(g))) == False{} : Bool} -> @ih1:{push_all(E(g, lift(t)), cvs(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.take(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out, xs, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(g)))) == E(g, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.push(lift(t), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.cv(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.tree(g, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.take(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out, xs, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(g)))))) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.Stack} -> @ih2:{push_all(E(g, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.SFull{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.cv(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.tree(g, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.take(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out, xs, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(g)))), t}), cvs(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.drop(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out, xs, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(g)))) == E(g, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.push(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.SFull{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.cv(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.tree(g, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.take(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out, xs, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(g)))), t}, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.cv(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.tree(g, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.drop(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out, xs, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(g)))))) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.Stack} -> {push_all(E(1n+g, t), cvs(xs)) == E(1n+g, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.push(t, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.cv(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.tree(1n+g, xs)))) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.Stack}

def complete_zero source · line 210 · raw

@+xs:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out> -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.Stack -> @+hl:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out, xs) == 1n : Nat} -> {push_all(E(0n, t), cvs(xs)) == E(0n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.push(t, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.cv(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.tree(0n, xs)))) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.Stack}

def complete source · line 222 · raw

@+g:Nat -> @+xs:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out> -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.Stack -> @+hl:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out, xs) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(g) : Nat} -> {push_all(E(g, t), cvs(xs)) == E(g, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.push(t, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.cv(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.tree(g, xs)))) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.Stack}

A stack with g empty low slots absorbs the chaining values of 2^g outputs as one complete subtree pushed at slot g.

def partial_zero source · line 232 · raw

@+fs:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out> -> @+o:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.Stack -> @+hl:{Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out, fs), 1n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.finish(push_all(E(0n, t), cvs(fs)), o) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.finish(t, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.tree(0n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.append(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out, fs, [o]))) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out}

def partial_fit source · line 240 · raw

@+p:Nat -> @+fs:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out> -> @+o:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.Stack -> @+hb:{Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out, fs), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(p)) == True{} : Bool} -> @rec:(@f2:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out> -> @t2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.Stack -> @h2:{Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out, f2), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(p)) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.finish(push_all(E(p, t2), cvs(f2)), o) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.finish(t2, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.tree(p, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.append(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out, f2, [o]))) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out}) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.finish(push_all(E(1n+p, t), cvs(fs)), o) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.finish(t, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.tree(1n+p, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.append(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out, fs, [o]))) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out}

Fewer than 2^p outputs before o: the whole tree fits in height p.

def partial_big source · line 257 · raw

@+p:Nat -> @+fs:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out> -> @+o:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.Stack -> @+hl:{Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out, fs), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(1n+p)) == True{} : Bool} -> @+hb:{Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out, fs), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(p)) == False{} : Bool} -> @rec:(@f2:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out> -> @t2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.Stack -> @h2:{Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out, f2), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(p)) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.finish(push_all(E(p, t2), cvs(f2)), o) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.finish(t2, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.tree(p, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.append(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out, f2, [o]))) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out}) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.finish(push_all(E(1n+p, t), cvs(fs)), o) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.finish(t, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.tree(1n+p, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.append(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out, fs, [o]))) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out}

At least 2^p outputs before o: a complete left subtree of 2^p chunks, then the rest with o.

def partial_split source · line 287 · raw

@+p:Nat -> @+fs:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out> -> @+o:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.Stack -> @+hl:{Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out, fs), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(1n+p)) == True{} : Bool} -> @+b:Bool -> @+hb:{Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out, fs), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(p)) == b : Bool} -> @rec:(@f2:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out> -> @t2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.Stack -> @h2:{Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out, f2), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(p)) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.finish(push_all(E(p, t2), cvs(f2)), o) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.finish(t2, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.tree(p, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.append(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out, f2, [o]))) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out}) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.finish(push_all(E(1n+p, t), cvs(fs)), o) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.finish(t, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.tree(1n+p, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.append(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out, fs, [o]))) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out}

def partial source · line 299 · raw

@+g:Nat -> @+fs:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out> -> @+o:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.Stack -> @+hl:{Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out, fs), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(g)) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.finish(push_all(E(g, t), cvs(fs)), o) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.finish(t, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.tree(g, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.append(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out, fs, [o]))) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out}

Fewer than 2^g chaining values pushed on a stack with g empty low slots, then folded into the pending output o: the specification's tree of height g over the outputs and o, folded into the rest of the stack.

def tree_stack source · line 306 · raw

@+fs:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out> -> @+o:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.finish(push_all(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.StkNil{}, cvs(fs)), o) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.tree(1n+0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out, fs), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.append(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out, fs, [o])) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out}

The whole message: the stack starts empty and the height is the chunk count.