def partial_zero

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/blake/blake3/tree.bend:232

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake3/types.bend as T
import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake3/blake3.bend as K
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as SC
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake3.bend as S

232def partial_zero(+fs: List<&2,T.Out>, +o: T.Out, +t: K.Stack, +hl: {Nat.is_lt(SC.length(T.Out,fs),1n) == True{} : Bool}) -> {K.finish(push_all(E(0n,t),cvs(fs)),o) == K.finish(t,S.tree(0n,SC.append(T.Out,fs,Con{o,Nil{}}))) : T.Out}:
233  match fs:
234    case Nil{}:
235      %Equal.sym(K.Stack,E(0n,t),t,E_zero(t)) : {K.finish(_,o) == K.finish(t,S.tree(0n,Con{o,Nil{}})) : T.Out}
236      {==}
237    case Con{+f,+r}: Empty.absurd({K.finish(push_all(E(0n,t),cvs(Con{f,r})),o) == K.finish(t,S.tree(0n,SC.append(T.Out,Con{f,r},Con{o,Nil{}}))) : T.Out},N.lt_zero_absurd(SC.length(T.Out,r),hl))