law rounds7_correct

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/blake/blake3/compress.bend:70

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

70law rounds7_correct:
71  for +s: T.St
72  for +m0: U32
73  for +m1: U32
74  for +m2: U32
75  for +m3: U32
76  for +m4: U32
77  for +m5: U32
78  for +m6: U32
79  for +m7: U32
80  for +m8: U32
81  for +m9: U32
82  for +m10: U32
83  for +m11: U32
84  for +m12: U32
85  for +m13: U32
86  for +m14: U32
87  for +m15: U32
88  {st_list(C.rounds7(s,T.B{m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15})) == S.rounds(7n,st_list(s),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15]) : List<&2,U32>}