law step256_inv

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

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

187law step256_inv:
188  for +st: H.Sha256State
189  for +xs: List<&2, U32>
190  for +q: Nat
191  for +z: List<&2, U32>
192  {C256.block_bytes(List.append(&2, U32, List.append(&2, U32, buf256(st), xs), z), q, C256.round_constants(), st256(st)) == C256.block_bytes(List.append(&2, U32, buf256(H.step256(st, xs, q)), z), q, C256.round_constants(), st256(H.step256(st, xs, q))) : S256.State}