law finish_correct
bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/blake/blake2s/compress.bend:417
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake2s/compress.bend as Compress
import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2s/types.bend as T
import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2s/compress.bend as C
417law finish_correct:
418 for +h0: U32
419 for +h1: U32
420 for +h2: U32
421 for +h3: U32
422 for +h4: U32
423 for +h5: U32
424 for +h6: U32
425 for +h7: U32
426 for +v: T.Vector
427 {C.finish(T.H{h0,h1,h2,h3,h4,h5,h6,h7},v) == fin(h0,h1,h2,h3,h4,h5,h6,h7,vec(v)) : T.State}