def run_chunks

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/blake/blake3/loop.bend:64

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

64# The specification's chunk list is never empty.
65def run_chunks(+n: Nat, +t: U32, +index: U32, +len: Nat, q: Array<U32> & T.Out) -> {run(K.StkNil{},S.chunks(n,t,index,len,q)) == S.tree(SC.length(T.Out,S.chunks(n,t,index,len,q)),S.chunks(n,t,index,len,q)) : T.Out}:
66  match n q:
67    case 0n Tuple{a,o}: run_tree(o,Nil{})
68    case 1n+p Tuple{a,o}: run_tree(o,S.chunks(p,U32.inc(t),U32.add(index,256),len,S.chunk_at(p,U32.inc(t),U32.add(index,256),len,a)))