law absorb256_inv

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/hash/incremental.bend:39

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

39law absorb256_inv:
40  for +fuel: Nat
41  for +bytes: List<&2, U32>
42  for +q: Nat
43  for +s: S256.State
44  for +z: List<&2, U32>
45  {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}