def at_eq

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/argon2/index.bend:47

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/argon2/argon2.bend as I
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake2b.bend as B

47def at_eq(+v: T.State, +j: Nat) -> {I.at(v, j) == B.at(v, j) : T.Lane}:
48  match v j:
49    case T.V{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} 0n:
50      {==}
51    case T.V{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} 1n:
52      {==}
53    case T.V{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} 2n:
54      {==}
55    case T.V{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} 3n:
56      {==}
57    case T.V{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} 4n:
58      {==}
59    case T.V{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} 5n:
60      {==}
61    case T.V{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} 6n:
62      {==}
63    case T.V{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} 7n:
64      {==}
65    case T.V{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} 8n:
66      {==}
67    case T.V{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} 9n:
68      {==}
69    case T.V{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} 10n:
70      {==}
71    case T.V{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} 11n:
72      {==}
73    case T.V{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} 12n:
74      {==}
75    case T.V{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} 13n:
76      {==}
77    case T.V{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} 14n:
78      {==}
79    case T.V{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} 15n:
80      {==}
81    case T.V{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} 16n+z:
82      {==}