law read2_correct

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/blake/blake2s/reads.bend:393

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2s/types.bend as T
import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2s/blake2s.bend as K
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake2s.bend as R

393law read2_correct:
394  for +index: U32
395  for +h: T.State
396  for +t0: U32
397  for +t1: U32
398  for +u1: U32
399  for e: {t1 == u1 : U32}
400  for +w0: U32
401  for +w1: U32
402  for pair: Array<U32> & U32
403  {K.read2(index,h,t0,t1,w0,w1,pair) == R.full_block(10n,R.gather(13n,index,3,[w1,w0],pair),h,t0,u1) : Array<U32> & T.State}