law unchecked_correct

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

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/keccak/keccak.bend as K
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/keccak/main.bend as R

2285law unchecked_correct:
2286  for +r: Nat
2287  for a: Array<U32>
2288  for +length: Nat
2289  {K.unchecked(r,a,length) == R.unchecked(r,a,length) : T.State}