law round7_correct

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

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

459law round7_correct:
460  for +v: T.State
461  for +m0: T.Lane
462  for +m1: T.Lane
463  for +m2: T.Lane
464  for +m3: T.Lane
465  for +m4: T.Lane
466  for +m5: T.Lane
467  for +m6: T.Lane
468  for +m7: T.Lane
469  for +m8: T.Lane
470  for +m9: T.Lane
471  for +m10: T.Lane
472  for +m11: T.Lane
473  for +m12: T.Lane
474  for +m13: T.Lane
475  for +m14: T.Lane
476  for +m15: T.Lane
477  {I.round7(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15) == S.round(v,[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15],S.sigma(7n)) : T.State}