law absorb3_inv

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

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

682law absorb3_inv:
683  for +fuel: Nat
684  for +bytes: List<&2, U32>
685  for +q: Nat
686  for +s: TK.State
687  for +z: List<&2, U32>
688  {C3.absorb(C3.lanes(List.append(&2, U32, bytes, z)), q, s) == C3.absorb(C3.lanes(List.append(&2, U32, buf3(H.absorb3(fuel, H.read3_0(bytes), bytes, q, s)), z)), q, st3(H.absorb3(fuel, H.read3_0(bytes), bytes, q, s))) : TK.State}