1	# Generated by tools/generators/chacha8rand_gen.py; do not edit.
2	# The ChaCha8 core of ChaCha8Rand (C2SP chacha8rand; Go's
3	# internal/chacha8rand block_generic). One double round is fully unrolled
4	# (four column and four diagonal quarter rounds, RFC 8439 section 2.1-2.3,
5	# constant rotations); a block is four double rounds (eight rounds). As
6	# C2SP specifies, only the key words 4..11 are added back after the rounds:
7	# the constants and the counter are not (the standard ChaCha output minus
8	# them). A group is four consecutive blocks interleaved word by word, read
9	# as 32 little-endian 64-bit words: word 2w of the group is word w of the
10	# first block (low half) and of the second (high half), word 2w + 1 the
11	# same for the third and fourth block.
12	#
13	# Proved equal to spec/math/random/chacha8rand.bend for every key and
14	# counter (proofs/math/random/chacha8/).
15	import Base
16	import ../../u64.bend as W
17	
18	# the 256-bit key as eight little-endian words
19	type Key is Data:
20	  K{k0: U32, k1: U32, k2: U32, k3: U32, k4: U32, k5: U32, k6: U32, k7: U32}
21	
22	# the ChaCha state x[0..15]
23	type Vector is Data:
24	  V{v0: U32, v1: U32, v2: U32, v3: U32, v4: U32, v5: U32, v6: U32, v7: U32, v8: U32, v9: U32, v10: U32, v11: U32, v12: U32, v13: U32, v14: U32, v15: U32}
25	
26	# the initial state: constants, key, 32-bit block counter, zero nonce
27	def init(k: Key, +ctr: U32) -> Vector:
28	  match k:
29	    case K{k0,k1,k2,k3,k4,k5,k6,k7}:
30	      V{1634760805,857760878,2036477234,1797285236,k0,k1,k2,k3,k4,k5,k6,k7,ctr,0,0,0}
31	
32	# one double round: four column quarter rounds, then four diagonal ones
33	def dr(v: Vector) -> Vector:
34	  match v:
35	    case V{+a0,+a1,+a2,+a3,+a4,+a5,+a6,+a7,+a8,+a9,+a10,+a11,+a12,+a13,+a14,+a15}:
36	      +q0a1 = U32.add(a0,a4)
37	      +q0d1x = U32.xor(a12,q0a1)
38	      +q0d1 = U32.or(U32.shln(q0d1x,16n),U32.shrn(q0d1x,16n))
39	      +q0c1 = U32.add(a8,q0d1)
40	      +q0b1x = U32.xor(a4,q0c1)
41	      +q0b1 = U32.or(U32.shln(q0b1x,12n),U32.shrn(q0b1x,20n))
42	      +q0a2 = U32.add(q0a1,q0b1)
43	      +q0d2x = U32.xor(q0d1,q0a2)
44	      +q0d2 = U32.or(U32.shln(q0d2x,8n),U32.shrn(q0d2x,24n))
45	      +q0c2 = U32.add(q0c1,q0d2)
46	      +q0b2x = U32.xor(q0b1,q0c2)
47	      +q0b2 = U32.or(U32.shln(q0b2x,7n),U32.shrn(q0b2x,25n))
48	      +q1a1 = U32.add(a1,a5)
49	      +q1d1x = U32.xor(a13,q1a1)
50	      +q1d1 = U32.or(U32.shln(q1d1x,16n),U32.shrn(q1d1x,16n))
51	      +q1c1 = U32.add(a9,q1d1)
52	      +q1b1x = U32.xor(a5,q1c1)
53	      +q1b1 = U32.or(U32.shln(q1b1x,12n),U32.shrn(q1b1x,20n))
54	      +q1a2 = U32.add(q1a1,q1b1)
55	      +q1d2x = U32.xor(q1d1,q1a2)
56	      +q1d2 = U32.or(U32.shln(q1d2x,8n),U32.shrn(q1d2x,24n))
57	      +q1c2 = U32.add(q1c1,q1d2)
58	      +q1b2x = U32.xor(q1b1,q1c2)
59	      +q1b2 = U32.or(U32.shln(q1b2x,7n),U32.shrn(q1b2x,25n))
60	      +q2a1 = U32.add(a2,a6)
61	      +q2d1x = U32.xor(a14,q2a1)
62	      +q2d1 = U32.or(U32.shln(q2d1x,16n),U32.shrn(q2d1x,16n))
63	      +q2c1 = U32.add(a10,q2d1)
64	      +q2b1x = U32.xor(a6,q2c1)
65	      +q2b1 = U32.or(U32.shln(q2b1x,12n),U32.shrn(q2b1x,20n))
66	      +q2a2 = U32.add(q2a1,q2b1)
67	      +q2d2x = U32.xor(q2d1,q2a2)
68	      +q2d2 = U32.or(U32.shln(q2d2x,8n),U32.shrn(q2d2x,24n))
69	      +q2c2 = U32.add(q2c1,q2d2)
70	      +q2b2x = U32.xor(q2b1,q2c2)
71	      +q2b2 = U32.or(U32.shln(q2b2x,7n),U32.shrn(q2b2x,25n))
72	      +q3a1 = U32.add(a3,a7)
73	      +q3d1x = U32.xor(a15,q3a1)
74	      +q3d1 = U32.or(U32.shln(q3d1x,16n),U32.shrn(q3d1x,16n))
75	      +q3c1 = U32.add(a11,q3d1)
76	      +q3b1x = U32.xor(a7,q3c1)
77	      +q3b1 = U32.or(U32.shln(q3b1x,12n),U32.shrn(q3b1x,20n))
78	      +q3a2 = U32.add(q3a1,q3b1)
79	      +q3d2x = U32.xor(q3d1,q3a2)
80	      +q3d2 = U32.or(U32.shln(q3d2x,8n),U32.shrn(q3d2x,24n))
81	      +q3c2 = U32.add(q3c1,q3d2)
82	      +q3b2x = U32.xor(q3b1,q3c2)
83	      +q3b2 = U32.or(U32.shln(q3b2x,7n),U32.shrn(q3b2x,25n))
84	      +q4a1 = U32.add(q0a2,q1b2)
85	      +q4d1x = U32.xor(q3d2,q4a1)
86	      +q4d1 = U32.or(U32.shln(q4d1x,16n),U32.shrn(q4d1x,16n))
87	      +q4c1 = U32.add(q2c2,q4d1)
88	      +q4b1x = U32.xor(q1b2,q4c1)
89	      +q4b1 = U32.or(U32.shln(q4b1x,12n),U32.shrn(q4b1x,20n))
90	      +q4a2 = U32.add(q4a1,q4b1)
91	      +q4d2x = U32.xor(q4d1,q4a2)
92	      +q4d2 = U32.or(U32.shln(q4d2x,8n),U32.shrn(q4d2x,24n))
93	      +q4c2 = U32.add(q4c1,q4d2)
94	      +q4b2x = U32.xor(q4b1,q4c2)
95	      +q4b2 = U32.or(U32.shln(q4b2x,7n),U32.shrn(q4b2x,25n))
96	      +q5a1 = U32.add(q1a2,q2b2)
97	      +q5d1x = U32.xor(q0d2,q5a1)
98	      +q5d1 = U32.or(U32.shln(q5d1x,16n),U32.shrn(q5d1x,16n))
99	      +q5c1 = U32.add(q3c2,q5d1)
100	      +q5b1x = U32.xor(q2b2,q5c1)
101	      +q5b1 = U32.or(U32.shln(q5b1x,12n),U32.shrn(q5b1x,20n))
102	      +q5a2 = U32.add(q5a1,q5b1)
103	      +q5d2x = U32.xor(q5d1,q5a2)
104	      +q5d2 = U32.or(U32.shln(q5d2x,8n),U32.shrn(q5d2x,24n))
105	      +q5c2 = U32.add(q5c1,q5d2)
106	      +q5b2x = U32.xor(q5b1,q5c2)
107	      +q5b2 = U32.or(U32.shln(q5b2x,7n),U32.shrn(q5b2x,25n))
108	      +q6a1 = U32.add(q2a2,q3b2)
109	      +q6d1x = U32.xor(q1d2,q6a1)
110	      +q6d1 = U32.or(U32.shln(q6d1x,16n),U32.shrn(q6d1x,16n))
111	      +q6c1 = U32.add(q0c2,q6d1)
112	      +q6b1x = U32.xor(q3b2,q6c1)
113	      +q6b1 = U32.or(U32.shln(q6b1x,12n),U32.shrn(q6b1x,20n))
114	      +q6a2 = U32.add(q6a1,q6b1)
115	      +q6d2x = U32.xor(q6d1,q6a2)
116	      +q6d2 = U32.or(U32.shln(q6d2x,8n),U32.shrn(q6d2x,24n))
117	      +q6c2 = U32.add(q6c1,q6d2)
118	      +q6b2x = U32.xor(q6b1,q6c2)
119	      +q6b2 = U32.or(U32.shln(q6b2x,7n),U32.shrn(q6b2x,25n))
120	      +q7a1 = U32.add(q3a2,q0b2)
121	      +q7d1x = U32.xor(q2d2,q7a1)
122	      +q7d1 = U32.or(U32.shln(q7d1x,16n),U32.shrn(q7d1x,16n))
123	      +q7c1 = U32.add(q1c2,q7d1)
124	      +q7b1x = U32.xor(q0b2,q7c1)
125	      +q7b1 = U32.or(U32.shln(q7b1x,12n),U32.shrn(q7b1x,20n))
126	      +q7a2 = U32.add(q7a1,q7b1)
127	      +q7d2x = U32.xor(q7d1,q7a2)
128	      +q7d2 = U32.or(U32.shln(q7d2x,8n),U32.shrn(q7d2x,24n))
129	      +q7c2 = U32.add(q7c1,q7d2)
130	      +q7b2x = U32.xor(q7b1,q7c2)
131	      +q7b2 = U32.or(U32.shln(q7b2x,7n),U32.shrn(q7b2x,25n))
132	      V{q4a2,q5a2,q6a2,q7a2,q7b2,q4b2,q5b2,q6b2,q6c2,q7c2,q4c2,q5c2,q5d2,q6d2,q7d2,q4d2}
133	
134	# the key words added back to words 4..11
135	def finish(k: Key, v: Vector) -> Vector:
136	  match k v:
137	    case K{k0,k1,k2,k3,k4,k5,k6,k7} V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15}:
138	      V{v0,v1,v2,v3,U32.add(v4,k0),U32.add(v5,k1),U32.add(v6,k2),U32.add(v7,k3),U32.add(v8,k4),U32.add(v9,k5),U32.add(v10,k6),U32.add(v11,k7),v12,v13,v14,v15}
139	
140	# the ChaCha8Rand block with counter ctr: eight rounds
141	def block(+k: Key, +ctr: U32) -> Vector:
142	  finish(k,dr(dr(dr(dr(init(k,ctr))))))
143	
144	# four blocks interleaved word by word, as 32 little-endian 64-bit words
145	def interleave(a: Vector, b: Vector, c: Vector, d: Vector) -> List<&2,W.U64>:
146	  match a b c d:
147	    case V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15} V{b0,b1,b2,b3,b4,b5,b6,b7,b8,b9,b10,b11,b12,b13,b14,b15} V{c0,c1,c2,c3,c4,c5,c6,c7,c8,c9,c10,c11,c12,c13,c14,c15} V{d0,d1,d2,d3,d4,d5,d6,d7,d8,d9,d10,d11,d12,d13,d14,d15}:
148	      [W.U64{a0,b0},W.U64{c0,d0},W.U64{a1,b1},W.U64{c1,d1},W.U64{a2,b2},W.U64{c2,d2},W.U64{a3,b3},W.U64{c3,d3},W.U64{a4,b4},W.U64{c4,d4},W.U64{a5,b5},W.U64{c5,d5},W.U64{a6,b6},W.U64{c6,d6},W.U64{a7,b7},W.U64{c7,d7},W.U64{a8,b8},W.U64{c8,d8},W.U64{a9,b9},W.U64{c9,d9},W.U64{a10,b10},W.U64{c10,d10},W.U64{a11,b11},W.U64{c11,d11},W.U64{a12,b12},W.U64{c12,d12},W.U64{a13,b13},W.U64{c13,d13},W.U64{a14,b14},W.U64{c14,d14},W.U64{a15,b15},W.U64{c15,d15}]
149	
150	# the group of the blocks ctr, ctr + 1, ctr + 2, ctr + 3
151	def group(+k: Key, +ctr: U32) -> List<&2,W.U64>:
152	  interleave(block(k,ctr),block(k,U32.add(ctr,1)),block(k,U32.add(ctr,2)),block(k,U32.add(ctr,3)))