law read1_correct

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

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

1008law read1_correct:
1009  for +r: Nat
1010  for +index: U32
1011  for +s: T.State
1012  for +w0: U32
1013  for pair: Array<U32> & U32
1014  {K.read1(r,index,s,w0,pair) == R.gather(r,32n,index,2,False{},0n,s,[w0],pair) : Array<U32> & T.State}