law absorb_correct

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/sha3/conformance.bend:42

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/keccak/types.bend as T
import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha3/core.bend as C
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/sha3.bend as F

42law absorb_correct:
43  for +ls: List<&2, T.Lane>
44  for +rounds: Nat
45  for +s: T.State
46  {C.absorb(ls, rounds, s) == F.absorb(ls, rounds, s) : T.State}