Chunk.compress_full: law of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/chunk.bend as Chunk
Lines 18-25 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/chunk.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/chunk.bend&start_line=18&end_line=25

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

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

Uses (9):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/compress.bend&name=compress_correct
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/read.bend&name=zero_tail_full
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake3.bend&name=compress
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake3.bend&name=zero_tail
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake3/compress.bend&name=compress
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake3/types.bend&name=Block
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake3/types.bend&name=CV