law compress_full

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/blake/blake3/chunk.bend:18

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

18# A full (64-byte) block: the implementation compresses the raw block, the
19# specification the block truncated to 64 bytes.
20law compress_full:
21  for +cv: T.CV
22  for +b: T.Block
23  for +t: U32
24  for +flags: U32
25  {C.compress(cv,b,t,64,flags) == S.compress(cv,S.zero_tail(b,64n),t,64,flags) : T.CV}