law step_correct

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/sha512/conformance.bend:14

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

14law step_correct:
15  for +s: T.State
16  for +k: T.Lane
17  for +w: T.Lane
18  {C.step(s, k, w) == F.step(s, k, w) : T.State}