Incremental.absorb256_inv: 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 39-45 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=39&end_line=45

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha/state.bend as S256
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/hash.bend as H

law absorb256_inv:
  for +fuel: Nat
  for +bytes: List<&2, U32>
  for +q: Nat
  for +s: S256.State
  for +z: List<&2, U32>
  {C256.block_bytes(List.append(&2, U32, bytes, z), q, C256.round_constants(), s) == C256.block_bytes(List.append(&2, U32, buf256(H.absorb256(fuel, H.read256_0(bytes), bytes, q, s)), z), q, C256.round_constants(), st256(H.absorb256(fuel, H.read256_0(bytes), bytes, q, s))) : S256.State}

Uses (14):
  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=Nat
  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=st256
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/sha/conformance.bend&name=fips16_correct
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/hash.bend&name=absorb256
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/hash.bend&name=read256_0
  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=fips_compress16
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/sha/core.bend&name=pack
  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/state.bend&name=State