law column2_correct

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/blake/blake2b/compress.bend:127

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/types.bend as T
import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/compress.bend as I
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake2b.bend as S

127law column2_correct:
128  for +v: T.State
129  for +x0: T.Lane
130  for +x1: T.Lane
131  for +x2: T.Lane
132  for +x3: T.Lane
133  for +x4: T.Lane
134  for +x5: T.Lane
135  for +x6: T.Lane
136  for +x7: T.Lane
137  {I.column2(v,x0,x1,x2,x3,x4,x5,x6,x7) == S.G(S.G(S.G(S.G(v,0n,4n,8n,12n,x0,x1),1n,5n,9n,13n,x2,x3),2n,6n,10n,14n,x4,x5),3n,7n,11n,15n,x6,x7) : T.State}