law step3_inv

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

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/keccak/types.bend as TK
import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha3/core.bend as C3
import bend-collections-laws-crypto@1.0.0.0/src/crypto/hash.bend as H

971law step3_inv:
972  for +st: H.Sha3State
973  for +xs: List<&2, U32>
974  for +q: Nat
975  for +z: List<&2, U32>
976  {C3.absorb(C3.lanes(List.append(&2, U32, List.append(&2, U32, buf3(st), xs), z)), q, st3(st)) == C3.absorb(C3.lanes(List.append(&2, U32, buf3(H.step3(st, xs, q)), z)), q, st3(H.step3(st, xs, q))) : TK.State}