def partial_split

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

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/spec/lib/common.bend as SC
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake3.bend as S

287def partial_split(+p: Nat, +fs: List<&2,T.Out>, +o: T.Out, +t: K.Stack,
288    +hl: {Nat.is_lt(SC.length(T.Out,fs),SC.pow2(1n+p)) == True{} : Bool},
289    +b: Bool, +hb: {Nat.is_lt(SC.length(T.Out,fs),SC.pow2(p)) == b : Bool},
290    rec: @f2: List<&2,T.Out> -> @t2: K.Stack -> @h2: {Nat.is_lt(SC.length(T.Out,f2),SC.pow2(p)) == True{} : Bool} -> {K.finish(push_all(E(p,t2),cvs(f2)),o) == K.finish(t2,S.tree(p,SC.append(T.Out,f2,Con{o,Nil{}}))) : T.Out}
291  ) -> {K.finish(push_all(E(1n+p,t),cvs(fs)),o) == K.finish(t,S.tree(1n+p,SC.append(T.Out,fs,Con{o,Nil{}}))) : T.Out}:
292  match b:
293    case True{}: partial_fit(p,fs,o,t,hb,rec)
294    case False{}: partial_big(p,fs,o,t,hl,hb,rec)