law checked_correct

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/keccak/sponge.bend:2320

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/keccak/keccak.bend as K
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/keccak/main.bend as R

2320law checked_correct:
2321  for +r: Nat
2322  for +valid: Bool
2323  for a: Array<U32>
2324  for +length: Nat
2325  {K.checked(r,valid,a,length) == R.checked(r,valid,a,length) : Maybe<&1,Array<U32>>}