law fold3_inv

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

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

991law fold3_inv:
992  for +cs: List<&2, List<&2, U32>>
993  for +q: Nat
994  for +st: H.Sha3State
995  for +z: List<&2, U32>
996  {C3.absorb(C3.lanes(List.append(&2, U32, List.append(&2, U32, buf3(st), List.concat(&2, U32, cs)), z)), q, st3(st)) == C3.absorb(C3.lanes(List.append(&2, U32, buf3(fold3(cs, q, st)), z)), q, st3(fold3(cs, q, st))) : TK.State}