src/crypto/chacha/core.bend

bend-collections@1.0.0.0 · 150 lines · 9 definitions

1# Generated by tools/generators/chacha_gen.py; do not edit.
2# The ChaCha core (RFC 8439 sections 2.1-2.3): the sixteen-word state as a
3# record, one double round (four column and four diagonal quarter rounds)
4# fully unrolled with constant rotations, and the block function with the
5# number of double rounds as a parameter (ChaCha20: 10; ChaCha8: 4;
6# ChaCha12: 6). No operation depends on secret data for its control flow or
7# memory access: the round count is public and every step is an add, xor or
8# constant rotation.
9import Base
10
11type State is Data:
12  S{x0: U32, x1: U32, x2: U32, x3: U32, x4: U32, x5: U32, x6: U32, x7: U32, x8: U32, x9: U32, x10: U32, x11: U32, x12: U32, x13: U32, x14: U32, x15: U32}
13
14# One double round: QUARTERROUND on the columns (0,4,8,12) .. (3,7,11,15),
15# then on the diagonals (0,5,10,15) (1,6,11,12) (2,7,8,13) (3,4,9,14).
16def double_round(s: State) -> State:
17  match s:
18    case S{+a0,+a1,+a2,+a3,+a4,+a5,+a6,+a7,+a8,+a9,+a10,+a11,+a12,+a13,+a14,+a15}:
19      +q0a1 = U32.add(a0,a4)
20      +q0d1x = U32.xor(a12,q0a1)
21      +q0d1 = U32.or(U32.shln(q0d1x,16n),U32.shrn(q0d1x,16n))
22      +q0c1 = U32.add(a8,q0d1)
23      +q0b1x = U32.xor(a4,q0c1)
24      +q0b1 = U32.or(U32.shln(q0b1x,12n),U32.shrn(q0b1x,20n))
25      +q0a2 = U32.add(q0a1,q0b1)
26      +q0d2x = U32.xor(q0d1,q0a2)
27      +q0d2 = U32.or(U32.shln(q0d2x,8n),U32.shrn(q0d2x,24n))
28      +q0c2 = U32.add(q0c1,q0d2)
29      +q0b2x = U32.xor(q0b1,q0c2)
30      +q0b2 = U32.or(U32.shln(q0b2x,7n),U32.shrn(q0b2x,25n))
31      +q1a1 = U32.add(a1,a5)
32      +q1d1x = U32.xor(a13,q1a1)
33      +q1d1 = U32.or(U32.shln(q1d1x,16n),U32.shrn(q1d1x,16n))
34      +q1c1 = U32.add(a9,q1d1)
35      +q1b1x = U32.xor(a5,q1c1)
36      +q1b1 = U32.or(U32.shln(q1b1x,12n),U32.shrn(q1b1x,20n))
37      +q1a2 = U32.add(q1a1,q1b1)
38      +q1d2x = U32.xor(q1d1,q1a2)
39      +q1d2 = U32.or(U32.shln(q1d2x,8n),U32.shrn(q1d2x,24n))
40      +q1c2 = U32.add(q1c1,q1d2)
41      +q1b2x = U32.xor(q1b1,q1c2)
42      +q1b2 = U32.or(U32.shln(q1b2x,7n),U32.shrn(q1b2x,25n))
43      +q2a1 = U32.add(a2,a6)
44      +q2d1x = U32.xor(a14,q2a1)
45      +q2d1 = U32.or(U32.shln(q2d1x,16n),U32.shrn(q2d1x,16n))
46      +q2c1 = U32.add(a10,q2d1)
47      +q2b1x = U32.xor(a6,q2c1)
48      +q2b1 = U32.or(U32.shln(q2b1x,12n),U32.shrn(q2b1x,20n))
49      +q2a2 = U32.add(q2a1,q2b1)
50      +q2d2x = U32.xor(q2d1,q2a2)
51      +q2d2 = U32.or(U32.shln(q2d2x,8n),U32.shrn(q2d2x,24n))
52      +q2c2 = U32.add(q2c1,q2d2)
53      +q2b2x = U32.xor(q2b1,q2c2)
54      +q2b2 = U32.or(U32.shln(q2b2x,7n),U32.shrn(q2b2x,25n))
55      +q3a1 = U32.add(a3,a7)
56      +q3d1x = U32.xor(a15,q3a1)
57      +q3d1 = U32.or(U32.shln(q3d1x,16n),U32.shrn(q3d1x,16n))
58      +q3c1 = U32.add(a11,q3d1)
59      +q3b1x = U32.xor(a7,q3c1)
60      +q3b1 = U32.or(U32.shln(q3b1x,12n),U32.shrn(q3b1x,20n))
61      +q3a2 = U32.add(q3a1,q3b1)
62      +q3d2x = U32.xor(q3d1,q3a2)
63      +q3d2 = U32.or(U32.shln(q3d2x,8n),U32.shrn(q3d2x,24n))
64      +q3c2 = U32.add(q3c1,q3d2)
65      +q3b2x = U32.xor(q3b1,q3c2)
66      +q3b2 = U32.or(U32.shln(q3b2x,7n),U32.shrn(q3b2x,25n))
67      +q4a1 = U32.add(q0a2,q1b2)
68      +q4d1x = U32.xor(q3d2,q4a1)
69      +q4d1 = U32.or(U32.shln(q4d1x,16n),U32.shrn(q4d1x,16n))
70      +q4c1 = U32.add(q2c2,q4d1)
71      +q4b1x = U32.xor(q1b2,q4c1)
72      +q4b1 = U32.or(U32.shln(q4b1x,12n),U32.shrn(q4b1x,20n))
73      +q4a2 = U32.add(q4a1,q4b1)
74      +q4d2x = U32.xor(q4d1,q4a2)
75      +q4d2 = U32.or(U32.shln(q4d2x,8n),U32.shrn(q4d2x,24n))
76      +q4c2 = U32.add(q4c1,q4d2)
77      +q4b2x = U32.xor(q4b1,q4c2)
78      +q4b2 = U32.or(U32.shln(q4b2x,7n),U32.shrn(q4b2x,25n))
79      +q5a1 = U32.add(q1a2,q2b2)
80      +q5d1x = U32.xor(q0d2,q5a1)
81      +q5d1 = U32.or(U32.shln(q5d1x,16n),U32.shrn(q5d1x,16n))
82      +q5c1 = U32.add(q3c2,q5d1)
83      +q5b1x = U32.xor(q2b2,q5c1)
84      +q5b1 = U32.or(U32.shln(q5b1x,12n),U32.shrn(q5b1x,20n))
85      +q5a2 = U32.add(q5a1,q5b1)
86      +q5d2x = U32.xor(q5d1,q5a2)
87      +q5d2 = U32.or(U32.shln(q5d2x,8n),U32.shrn(q5d2x,24n))
88      +q5c2 = U32.add(q5c1,q5d2)
89      +q5b2x = U32.xor(q5b1,q5c2)
90      +q5b2 = U32.or(U32.shln(q5b2x,7n),U32.shrn(q5b2x,25n))
91      +q6a1 = U32.add(q2a2,q3b2)
92      +q6d1x = U32.xor(q1d2,q6a1)
93      +q6d1 = U32.or(U32.shln(q6d1x,16n),U32.shrn(q6d1x,16n))
94      +q6c1 = U32.add(q0c2,q6d1)
95      +q6b1x = U32.xor(q3b2,q6c1)
96      +q6b1 = U32.or(U32.shln(q6b1x,12n),U32.shrn(q6b1x,20n))
97      +q6a2 = U32.add(q6a1,q6b1)
98      +q6d2x = U32.xor(q6d1,q6a2)
99      +q6d2 = U32.or(U32.shln(q6d2x,8n),U32.shrn(q6d2x,24n))
100      +q6c2 = U32.add(q6c1,q6d2)
101      +q6b2x = U32.xor(q6b1,q6c2)
102      +q6b2 = U32.or(U32.shln(q6b2x,7n),U32.shrn(q6b2x,25n))
103      +q7a1 = U32.add(q3a2,q0b2)
104      +q7d1x = U32.xor(q2d2,q7a1)
105      +q7d1 = U32.or(U32.shln(q7d1x,16n),U32.shrn(q7d1x,16n))
106      +q7c1 = U32.add(q1c2,q7d1)
107      +q7b1x = U32.xor(q0b2,q7c1)
108      +q7b1 = U32.or(U32.shln(q7b1x,12n),U32.shrn(q7b1x,20n))
109      +q7a2 = U32.add(q7a1,q7b1)
110      +q7d2x = U32.xor(q7d1,q7a2)
111      +q7d2 = U32.or(U32.shln(q7d2x,8n),U32.shrn(q7d2x,24n))
112      +q7c2 = U32.add(q7c1,q7d2)
113      +q7b2x = U32.xor(q7b1,q7c2)
114      +q7b2 = U32.or(U32.shln(q7b2x,7n),U32.shrn(q7b2x,25n))
115      S{q4a2,q5a2,q6a2,q7a2,q7b2,q4b2,q5b2,q6b2,q6c2,q7c2,q4c2,q5c2,q5d2,q6d2,q7d2,q4d2}
116# n double rounds (2n rounds).
117def rounds(n: Nat, s: State) -> State:
118  match n:
119    case 0n: s
120    case 1n+p: rounds(p, double_round(s))
121
122# Word-wise sum of two states (the feed-forward).
123def add(a: State, b: State) -> State:
124  match a b:
125    case S{x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15} S{y0,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15}:
126      S{U32.add(x0,y0),U32.add(x1,y1),U32.add(x2,y2),U32.add(x3,y3),U32.add(x4,y4),U32.add(x5,y5),U32.add(x6,y6),U32.add(x7,y7),U32.add(x8,y8),U32.add(x9,y9),U32.add(x10,y10),U32.add(x11,y11),U32.add(x12,y12),U32.add(x13,y13),U32.add(x14,y14),U32.add(x15,y15)}
127
128# The block function with n double rounds: the rounds, then the input added.
129def block(+n: Nat, +s: State) -> State:
130  add(s, rounds(n, s))
131
132# The ChaCha20 input state: constants, key, block counter, nonce.
133def init(k0: U32, k1: U32, k2: U32, k3: U32, k4: U32, k5: U32, k6: U32, k7: U32, counter: U32, n0: U32, n1: U32, n2: U32) -> State:
134  S{1634760805, 857760878, 2036477234, 1797285236, k0, k1, k2, k3, k4, k5, k6, k7, counter, n0, n1, n2}
135
136# The HChaCha20 input state: constants, key, the four words of the 16-byte nonce.
137def hinit(k0: U32, k1: U32, k2: U32, k3: U32, k4: U32, k5: U32, k6: U32, k7: U32, n0: U32, n1: U32, n2: U32, n3: U32) -> State:
138  S{1634760805, 857760878, 2036477234, 1797285236, k0, k1, k2, k3, k4, k5, k6, k7, n0, n1, n2, n3}
139
140# The 64 little-endian bytes of a state.
141def bytes(s: State) -> List<&2, U32>:
142  match s:
143    case S{+x0,+x1,+x2,+x3,+x4,+x5,+x6,+x7,+x8,+x9,+x10,+x11,+x12,+x13,+x14,+x15}:
144      [U32.and(x0,255), U32.and(U32.shrn(x0,8n),255), U32.and(U32.shrn(x0,16n),255), U32.shrn(x0,24n), U32.and(x1,255), U32.and(U32.shrn(x1,8n),255), U32.and(U32.shrn(x1,16n),255), U32.shrn(x1,24n), U32.and(x2,255), U32.and(U32.shrn(x2,8n),255), U32.and(U32.shrn(x2,16n),255), U32.shrn(x2,24n), U32.and(x3,255), U32.and(U32.shrn(x3,8n),255), U32.and(U32.shrn(x3,16n),255), U32.shrn(x3,24n), U32.and(x4,255), U32.and(U32.shrn(x4,8n),255), U32.and(U32.shrn(x4,16n),255), U32.shrn(x4,24n), U32.and(x5,255), U32.and(U32.shrn(x5,8n),255), U32.and(U32.shrn(x5,16n),255), U32.shrn(x5,24n), U32.and(x6,255), U32.and(U32.shrn(x6,8n),255), U32.and(U32.shrn(x6,16n),255), U32.shrn(x6,24n), U32.and(x7,255), U32.and(U32.shrn(x7,8n),255), U32.and(U32.shrn(x7,16n),255), U32.shrn(x7,24n), U32.and(x8,255), U32.and(U32.shrn(x8,8n),255), U32.and(U32.shrn(x8,16n),255), U32.shrn(x8,24n), U32.and(x9,255), U32.and(U32.shrn(x9,8n),255), U32.and(U32.shrn(x9,16n),255), U32.shrn(x9,24n), U32.and(x10,255), U32.and(U32.shrn(x10,8n),255), U32.and(U32.shrn(x10,16n),255), U32.shrn(x10,24n), U32.and(x11,255), U32.and(U32.shrn(x11,8n),255), U32.and(U32.shrn(x11,16n),255), U32.shrn(x11,24n), U32.and(x12,255), U32.and(U32.shrn(x12,8n),255), U32.and(U32.shrn(x12,16n),255), U32.shrn(x12,24n), U32.and(x13,255), U32.and(U32.shrn(x13,8n),255), U32.and(U32.shrn(x13,16n),255), U32.shrn(x13,24n), U32.and(x14,255), U32.and(U32.shrn(x14,8n),255), U32.and(U32.shrn(x14,16n),255), U32.shrn(x14,24n), U32.and(x15,255), U32.and(U32.shrn(x15,8n),255), U32.and(U32.shrn(x15,16n),255), U32.shrn(x15,24n)]
145
146# HChaCha20's output: the little-endian bytes of words 0..3 and 12..15.
147def hbytes(s: State) -> List<&2, U32>:
148  match s:
149    case S{+x0,+x1,+x2,+x3,x4,x5,x6,x7,x8,x9,x10,x11,+x12,+x13,+x14,+x15}:
150      [U32.and(x0,255), U32.and(U32.shrn(x0,8n),255), U32.and(U32.shrn(x0,16n),255), U32.shrn(x0,24n), U32.and(x1,255), U32.and(U32.shrn(x1,8n),255), U32.and(U32.shrn(x1,16n),255), U32.shrn(x1,24n), U32.and(x2,255), U32.and(U32.shrn(x2,8n),255), U32.and(U32.shrn(x2,16n),255), U32.shrn(x2,24n), U32.and(x3,255), U32.and(U32.shrn(x3,8n),255), U32.and(U32.shrn(x3,16n),255), U32.shrn(x3,24n), U32.and(x12,255), U32.and(U32.shrn(x12,8n),255), U32.and(U32.shrn(x12,16n),255), U32.shrn(x12,24n), U32.and(x13,255), U32.and(U32.shrn(x13,8n),255), U32.and(U32.shrn(x13,16n),255), U32.shrn(x13,24n), U32.and(x14,255), U32.and(U32.shrn(x14,8n),255), U32.and(U32.shrn(x14,16n),255), U32.shrn(x14,24n), U32.and(x15,255), U32.and(U32.shrn(x15,8n),255), U32.and(U32.shrn(x15,16n),255), U32.shrn(x15,24n)]