law step512_inv

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

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha512/types.bend as T512
import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha512/core.bend as C512
import bend-collections-laws-crypto@1.0.0.0/src/crypto/hash.bend as H

571law step512_inv:
572  for +st: H.Sha512State
573  for +xs: List<&2, U32>
574  for +q: Nat
575  for +z: List<&2, U32>
576  {C512.blocks(C512.lanes(List.append(&2, U32, List.append(&2, U32, buf512(st), xs), z)), q, C512.round_constants(), st512(st)) == C512.blocks(C512.lanes(List.append(&2, U32, buf512(H.step512(st, xs, q)), z)), q, C512.round_constants(), st512(H.step512(st, xs, q))) : T512.State}