proofs/crypto/chacha/core.bend

bend-collections-laws-crypto@1.0.0.0 · 177 lines · 25 definitions

1# Generated by tools/generators/chacha_gen.py; do not edit.
2# The unrolled ChaCha core refines the list-based RFC 8439 specification.
3#
4# vec(s) is the RFC state list of a record state, one projection per entry,
5# so that the list has its shape even when the state is abstract. One double
6# round is compared with inner_block on a destructured state (both sides
7# normalize to the same sixteen words); the round count is then an induction,
8# so the theorems hold for every number of double rounds (ChaCha20, ChaCha8,
9# ChaCha12 alike).
10import Base
11import bend-collections-laws-crypto@1.0.0.0/src/crypto/chacha/core.bend as C
12import bend-collections-laws-crypto@1.0.0.0/spec/crypto/chacha.bend as R
13
14def p0(s: C.State) -> U32:
15  match s:
16    case C.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a0
17
18def p1(s: C.State) -> U32:
19  match s:
20    case C.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a1
21
22def p2(s: C.State) -> U32:
23  match s:
24    case C.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a2
25
26def p3(s: C.State) -> U32:
27  match s:
28    case C.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a3
29
30def p4(s: C.State) -> U32:
31  match s:
32    case C.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a4
33
34def p5(s: C.State) -> U32:
35  match s:
36    case C.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a5
37
38def p6(s: C.State) -> U32:
39  match s:
40    case C.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a6
41
42def p7(s: C.State) -> U32:
43  match s:
44    case C.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a7
45
46def p8(s: C.State) -> U32:
47  match s:
48    case C.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a8
49
50def p9(s: C.State) -> U32:
51  match s:
52    case C.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a9
53
54def p10(s: C.State) -> U32:
55  match s:
56    case C.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a10
57
58def p11(s: C.State) -> U32:
59  match s:
60    case C.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a11
61
62def p12(s: C.State) -> U32:
63  match s:
64    case C.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a12
65
66def p13(s: C.State) -> U32:
67  match s:
68    case C.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a13
69
70def p14(s: C.State) -> U32:
71  match s:
72    case C.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a14
73
74def p15(s: C.State) -> U32:
75  match s:
76    case C.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a15
77
78def vec(+s: C.State) -> List<&2, U32>:
79  [p0(s), p1(s), p2(s), p3(s), p4(s), p5(s), p6(s), p7(s), p8(s), p9(s), p10(s), p11(s), p12(s), p13(s), p14(s), p15(s)]
80
81law double_round_correct:
82  for +s: C.State
83  {vec(C.double_round(s)) == R.inner_block(vec(s)) : List<&2, U32>}
84
85def double_round_correct(s):
86  match s:
87    case C.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: {==}
88
89law rounds_correct:
90  for +n: Nat
91  for +s: C.State
92  {vec(C.rounds(n, s)) == R.inner_blocks(n, vec(s)) : List<&2, U32>}
93
94def rounds_correct(n, s):
95  match n:
96    case 0n: {==}
97    case 1n+p:
98      Equal.trans(List<&2, U32>,
99        vec(C.rounds(p, C.double_round(s))),
100        R.inner_blocks(p, vec(C.double_round(s))),
101        R.inner_blocks(p, R.inner_block(vec(s))),
102        rounds_correct(p, C.double_round(s)),
103        Equal.cong(List<&2, U32>, List<&2, U32>, l => R.inner_blocks(p, l), vec(C.double_round(s)), R.inner_block(vec(s)), double_round_correct(s)))
104
105law add_correct:
106  for +a: C.State
107  for +b: C.State
108  {vec(C.add(a, b)) == R.add_words(vec(a), vec(b)) : List<&2, U32>}
109
110def add_correct(a, b):
111  match a b:
112    case C.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15} C.S{b0,b1,b2,b3,b4,b5,b6,b7,b8,b9,b10,b11,b12,b13,b14,b15}: {==}
113
114law bytes_correct:
115  for +s: C.State
116  {C.bytes(s) == R.serialize(vec(s)) : List<&2, U32>}
117
118def bytes_correct(s):
119  match s:
120    case C.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: {==}
121
122# The block function with n double rounds, serialized, is the RFC's.
123law block_correct:
124  for +n: Nat
125  for +s: C.State
126  {C.bytes(C.block(n, s)) == R.serialize(R.add_words(vec(s), R.inner_blocks(n, vec(s)))) : List<&2, U32>}
127
128def block_correct(n, s):
129  Equal.trans(List<&2, U32>, C.bytes(C.block(n, s)), R.serialize(vec(C.add(s, C.rounds(n, s)))), R.serialize(R.add_words(vec(s), R.inner_blocks(n, vec(s)))),
130    bytes_correct(C.add(s, C.rounds(n, s))),
131    Equal.trans(List<&2, U32>, R.serialize(vec(C.add(s, C.rounds(n, s)))), R.serialize(R.add_words(vec(s), vec(C.rounds(n, s)))), R.serialize(R.add_words(vec(s), R.inner_blocks(n, vec(s)))),
132      Equal.cong(List<&2, U32>, List<&2, U32>, l => R.serialize(l), vec(C.add(s, C.rounds(n, s))), R.add_words(vec(s), vec(C.rounds(n, s))), add_correct(s, C.rounds(n, s))),
133      Equal.cong(List<&2, U32>, List<&2, U32>, l => R.serialize(R.add_words(vec(s), l)), vec(C.rounds(n, s)), R.inner_blocks(n, vec(s)), rounds_correct(n, s))))
134
135law init_correct:
136  for +k0: U32
137  for +k1: U32
138  for +k2: U32
139  for +k3: U32
140  for +k4: U32
141  for +k5: U32
142  for +k6: U32
143  for +k7: U32
144  for +c: U32
145  for +n0: U32
146  for +n1: U32
147  for +n2: U32
148  {vec(C.init(k0, k1, k2, k3, k4, k5, k6, k7, c, n0, n1, n2)) == R.state([k0, k1, k2, k3, k4, k5, k6, k7], c, [n0, n1, n2]) : List<&2, U32>}
149
150def init_correct(k0, k1, k2, k3, k4, k5, k6, k7, c, n0, n1, n2):
151  {==}
152
153law hinit_correct:
154  for +k0: U32
155  for +k1: U32
156  for +k2: U32
157  for +k3: U32
158  for +k4: U32
159  for +k5: U32
160  for +k6: U32
161  for +k7: U32
162  for +n0: U32
163  for +n1: U32
164  for +n2: U32
165  for +n3: U32
166  {vec(C.hinit(k0, k1, k2, k3, k4, k5, k6, k7, n0, n1, n2, n3)) == R.hstate([k0, k1, k2, k3, k4, k5, k6, k7], [n0, n1, n2, n3]) : List<&2, U32>}
167
168def hinit_correct(k0, k1, k2, k3, k4, k5, k6, k7, n0, n1, n2, n3):
169  {==}
170
171law hbytes_correct:
172  for +s: C.State
173  {C.hbytes(s) == R.serialize([R.get(vec(s), 0n), R.get(vec(s), 1n), R.get(vec(s), 2n), R.get(vec(s), 3n), R.get(vec(s), 12n), R.get(vec(s), 13n), R.get(vec(s), 14n), R.get(vec(s), 15n)]) : List<&2, U32>}
174
175def hbytes_correct(s):
176  match s:
177    case C.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: {==}