Incremental.incremental256: law of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/hash/incremental.bend as Incremental
Lines 268-271 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/hash/incremental.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/hash/incremental.bend&start_line=268&end_line=271

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha/core.bend as C256
import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha/sha256.bend as SHA256
import bend-collections-laws-crypto@1.0.0.0/src/crypto/hash.bend as H

# digest(update_all(new, chunks)) is the padded block loop over concat(chunks).
law incremental256:
  for +cs: List<&2, List<&2, U32>>
  {H.digest(H.update_all(H.new_sha256(), cs)) == SHA256.digest_bytes(C256.digest(C256.block_bytes(List.append(&2, U32, List.concat(&2, U32, cs), C256.suffix(List.length(&2, U32, List.concat(&2, U32, cs)))), 48n, C256.round_constants(), C256.initial()))) : List<&2, U32>}

Uses (27):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.append
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.concat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.length
  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/hash/incremental.bend&name=buf256
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/hash/incremental.bend&name=finish256_eta
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/hash/incremental.bend&name=fold256
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/hash/incremental.bend&name=fold256_inv
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/hash/incremental.bend&name=st256
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/hash/incremental.bend&name=state256
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/hash.bend&name=Hasher
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/hash.bend&name=Sha256State
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/hash.bend&name=digest
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/hash.bend&name=finish256
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/hash.bend&name=fold
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/hash.bend&name=new_sha256
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/hash.bend&name=update_all
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/sha/core.bend&name=block_bytes
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/sha/core.bend&name=digest
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/sha/core.bend&name=initial
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/sha/core.bend&name=round_constants
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/sha/core.bend&name=suffix
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/sha/sha256.bend&name=digest_bytes
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/sha/state.bend&name=State