1	import Base
2	import ./AES256SBox.bend as SBox
3	
4	# Byte arithmetic. Inputs and outputs are represented by U32 values in [0,255].
5	# Turn a boolean into an all-zero or all-one word to keep field arithmetic branchless.
6	def xor_if(a: U32, b: U32, yes: Bool) -> U32:
7	    mask = U32.sub(0, Bool.to_u32(yes))
8	    U32.xor(a, U32.and(mask, b))
9	
10	def gf8_xtime.high(+a: U32, high: Bool) -> U32:
11	    xor_if(U32.and(255, U32.shln(a, 1n)), 27, high)
12	
13	def gf8_xtime(+a: U32) -> U32:
14	    gf8_xtime.high(a, U32.is_ne(U32.and(128, a), 0))
15	
16	def gf8_mul.go(fuel: Nat, +a: U32, +b: U32, acc: U32) -> U32:
17	    match fuel:
18	        case 0n: acc
19	        case 1n+p:
20	            bit = U32.is_ne(U32.and(1, b), 0)
21	            next = xor_if(acc, a, bit)
22	            gf8_mul.go(p, gf8_xtime(a), U32.shrn(b, 1n), next)
23	
24	def gf8_mul(a: U32, b: U32) -> U32:
25	    gf8_mul.go(8n, a, b, 0)
26	
27	def gf8_pow.go(fuel: Nat, +base: U32, +exp: U32, +acc: U32) -> U32:
28	    match fuel:
29	        case 0n: acc
30	        case 1n+p:
31	            next = Bool.pick(U32, U32.is_ne(U32.and(1, exp), 0), gf8_mul(acc, base), acc)
32	            gf8_pow.go(p, gf8_mul(base, base), U32.shrn(exp, 1n), next)
33	
34	def gf8_pow(a: U32, exp: U32) -> U32:
35	    gf8_pow.go(8n, a, exp, 1)
36	
37	def rotl8(+a: U32, +shift: Nat) -> U32:
38	    U32.and(255, U32.or(U32.shln(a, shift), U32.shrn(a, (8n - shift : Nat))))
39	
40	def aes_sbox_algebraic(+x: U32) -> U32:
41	    +inv = gf8_pow(x, 254)
42	    U32.xor(U32.xor(U32.xor(U32.xor(inv, rotl8(inv, 1n)),
43	        rotl8(inv, 2n)), rotl8(inv, 3n)),
44	        U32.xor(rotl8(inv, 4n), 99))
45	
46	def aes_sbox(+x: U32) -> U32:
47	    SBox.lookup(x)
48	
49	def aes_subword(+w: U32) -> U32:
50	    a b c d = aes_sbox(U32.shrn(w, 24n)) aes_sbox(U32.and(255, U32.shrn(w, 16n)))
51	        aes_sbox(U32.and(255, U32.shrn(w, 8n))) aes_sbox(U32.and(255, w))
52	    U32.or(U32.or(U32.shln(a, 24n), U32.shln(b, 16n)),
53	        U32.or(U32.shln(c, 8n), d))
54	
55	def aes_rotword(+w: U32) -> U32:
56	    U32.or(U32.shln(w, 8n), U32.shrn(w, 24n))
57	
58	def aes_rcon_step(r: U32) -> U32:
59	    gf8_xtime(r)
60	
61	def aes_word(a: U32, b: U32, c: U32, d: U32) -> U32:
62	    U32.or(U32.or(U32.shln(a, 24n), U32.shln(b, 16n)),
63	        U32.or(U32.shln(c, 8n), d))
64	
65	def aes_words(bytes: List<&2, U32>) -> List<&2, U32>:
66	    match bytes:
67	        case a <> b <> c <> d <> tail:
68	            aes_word(a, b, c, d) <> aes_words(tail)
69	        case _: Nil{}
70	
71	def aes_word_from_maybe(value: Maybe<&2, U32>) -> U32:
72	    match value:
73	        case None{}: 0
74	        case Some{w}: w
75	
76	def aes_word_at(words: List<&2, U32>, i: Nat) -> U32:
77	    aes_word_from_maybe(List.get(&2, U32, words, i))
78	
79	def aes_key_word_kind.step(previous: U32, rcon: U32, mod4: Bool) -> U32:
80	    match mod4:
81	        case True{}: aes_subword(previous)
82	        case False{}: previous
83	
84	def aes_key_word_kind.rcon(previous: U32, rcon: U32, mod4: Bool) -> U32:
85	    U32.xor(aes_subword(aes_rotword(previous)), U32.shln(rcon, 24n))
86	
87	def aes_key_word_kind(previous: U32, rcon: U32, mod0: Bool, mod4: Bool) -> U32:
88	    match mod0:
89	        case True{}: aes_key_word_kind.rcon(previous, rcon, mod4)
90	        case False{}: aes_key_word_kind.step(previous, rcon, mod4)
91	
92	def aes_rcon_kind(rcon: U32, advance: Bool) -> U32:
93	    match advance:
94	        case True{}: aes_rcon_step(rcon)
95	        case False{}: rcon
96	
97	def aes_expand.go(fuel: Nat, +i: U32, +rcon: U32,
98	                  +words: List<&2, U32>) -> List<&2, U32>:
99	    match fuel:
100	        case 0n: words
101	        case 1n+p:
102	            previous = aes_word_at(words, U32.to_nat(U32.sub(i, 1)))
103	            back8 = aes_word_at(words, U32.to_nat(U32.sub(i, 8)))
104	            part = aes_key_word_kind(previous, rcon, U32.is_eq(U32.mod(i, 8), 0), U32.is_eq(U32.mod(i, 8), 4))
105	            next = U32.xor(back8, part)
106	            next_rcon = aes_rcon_kind(rcon, U32.is_eq(U32.mod(i, 8), 0))
107	            aes_expand.go(p, U32.add(i, 1), next_rcon,
108	                List.append(&2, U32, words, [next]))
109	
110	def aes256_expand_impl(+key: List<&2, U32>) -> List<&2, U32>:
111	    aes_expand.go(52n, 8, 1, aes_words(key))
112	
113	# An abstract key remains neutral. The explicit fuel parameter also lets
114	# computation certificates compose without unfolding all 52 expansion steps.
115	def aes_expand_key(+fuel: Nat, +key: List<&2, U32>) -> List<&2, U32>:
116	    match key:
117	        case Nil{}: aes_expand.go(fuel, 8, 1, aes_words(key))
118	        case head <> tail: aes_expand.go(fuel, 8, 1, aes_words(key))
119	
120	def aes256_expand(+key: List<&2, U32>) -> List<&2, U32>:
121	    aes_expand_key(52n, key)
122	
123	def aes_add_key.go(+state: List<&2, U32>, +words: List<&2, U32>,
124	                   +round: Nat, +index: Nat, fuel: Nat,
125	                   acc: List<&2, U32>) -> List<&2, U32>:
126	    match state fuel:
127	        case Nil{} _: List.reverse(&2, U32, acc)
128	        case byte <> tail 0n: List.reverse(&2, U32, acc)
129	        case +byte <> tail 1n+p:
130	            word_index = ((round * 4n + (index / 4n : Nat)) : Nat)
131	            word = aes_word_at(words, word_index)
132	            shift = ((3n - (index % 4n : Nat)) * 8n : Nat)
133	            keybyte = U32.and(255, U32.shrn(word, shift))
134	            aes_add_key.go(tail, words, round, (index + 1n : Nat), p,
135	                U32.xor(byte, keybyte) <> acc)
136	
137	def aes_add_key(state: List<&2, U32>, words: List<&2, U32>, round: Nat) -> List<&2, U32>:
138	    aes_add_key.go(state, words, round, 0n, 16n, Nil{})
139	
140	def aes_sub_state.go(+state: List<&2, U32>, +acc: List<&2, U32>) -> List<&2, U32>:
141	    match state:
142	        case Nil{}: List.reverse(&2, U32, acc)
143	        case byte <> tail:
144	            aes_sub_state.go(tail, aes_sbox(byte) <> acc)
145	
146	def aes_sub_state(state: List<&2, U32>) -> List<&2, U32>:
147	    aes_sub_state.go(state, Nil{})
148	
149	def aes_byte_from_maybe(value: Maybe<&2, U32>) -> U32:
150	    match value:
151	        case None{}: 0
152	        case Some{byte}: byte
153	
154	def aes_byte_at(state: List<&2, U32>, index: Nat) -> U32:
155	    aes_byte_from_maybe(List.get(&2, U32, state, index))
156	
157	def aes_shift_rows(+state: List<&2, U32>) -> List<&2, U32>:
158	    [aes_byte_at(state, 0n), aes_byte_at(state, 5n), aes_byte_at(state, 10n), aes_byte_at(state, 15n),
159	     aes_byte_at(state, 4n), aes_byte_at(state, 9n), aes_byte_at(state, 14n), aes_byte_at(state, 3n),
160	     aes_byte_at(state, 8n), aes_byte_at(state, 13n), aes_byte_at(state, 2n), aes_byte_at(state, 7n),
161	     aes_byte_at(state, 12n), aes_byte_at(state, 1n), aes_byte_at(state, 6n), aes_byte_at(state, 11n)]
162	
163	type AesColumn is Data:
164	    AesColumn{a: U32, b: U32, c: U32, d: U32}
165	
166	def aes_mix_column(col: AesColumn) -> AesColumn:
167	    match col:
168	        case AesColumn{+a, +b, +c, +d}:
169	            AesColumn{
170	                U32.xor(U32.xor(U32.xor(gf8_mul(a, 2), gf8_mul(b, 3)), c), d),
171	                U32.xor(U32.xor(U32.xor(a, gf8_mul(b, 2)), gf8_mul(c, 3)), d),
172	                U32.xor(U32.xor(U32.xor(a, b), gf8_mul(c, 2)), gf8_mul(d, 3)),
173	                U32.xor(U32.xor(U32.xor(gf8_mul(a, 3), b), c), gf8_mul(d, 2))}
174	
175	def aes_mix_column.first(col: AesColumn) -> U32:
176	    match col:
177	        case AesColumn{+a, +b, +c, +d}:
178	            U32.xor(U32.xor(U32.xor(gf8_mul(a, 2), gf8_mul(b, 3)), c), d)
179	
180	def aes_mix_column.second(col: AesColumn) -> U32:
181	    match col:
182	        case AesColumn{+a, +b, +c, +d}:
183	            U32.xor(U32.xor(U32.xor(a, gf8_mul(b, 2)), gf8_mul(c, 3)), d)
184	
185	def aes_mix_column.third(col: AesColumn) -> U32:
186	    match col:
187	        case AesColumn{+a, +b, +c, +d}:
188	            U32.xor(U32.xor(U32.xor(a, b), gf8_mul(c, 2)), gf8_mul(d, 3))
189	
190	def aes_mix_column.fourth(col: AesColumn) -> U32:
191	    match col:
192	        case AesColumn{+a, +b, +c, +d}:
193	            U32.xor(U32.xor(U32.xor(gf8_mul(a, 3), b), c), gf8_mul(d, 2))
194	
195	def aes_mix_row(col: AesColumn, row: Nat) -> U32:
196	    match row:
197	        case 0n: aes_mix_column.first(col)
198	        case 1n: aes_mix_column.second(col)
199	        case 2n: aes_mix_column.third(col)
200	        case _: aes_mix_column.fourth(col)
201	
202	def aes_mix_byte(+state: List<&2, U32>, row: Nat, +col: Nat) -> U32:
203	    column: AesColumn = AesColumn{
204	        aes_byte_at(state, (col * 4n : Nat)),
205	        aes_byte_at(state, (col * 4n + 1n : Nat)),
206	        aes_byte_at(state, (col * 4n + 2n : Nat)),
207	        aes_byte_at(state, (col * 4n + 3n : Nat))}
208	    aes_mix_row(column, row)
209	
210	def aes_mix_state.finish(col0: AesColumn, col1: AesColumn, col2: AesColumn, col3: AesColumn) -> List<&2, U32>:
211	    match col0 col1 col2 col3:
212	        case AesColumn{a0, b0, c0, d0} AesColumn{a1, b1, c1, d1} AesColumn{a2, b2, c2, d2} AesColumn{a3, b3, c3, d3}:
213	            [a0,b0,c0,d0,a1,b1,c1,d1,a2,b2,c2,d2,a3,b3,c3,d3]
214	
215	def aes_mix_state(+state: List<&2, U32>) -> List<&2, U32>:
216	    col0 col1 col2 col3 =
217	        aes_mix_column(AesColumn{aes_byte_at(state, 0n), aes_byte_at(state, 1n), aes_byte_at(state, 2n), aes_byte_at(state, 3n)})
218	        aes_mix_column(AesColumn{aes_byte_at(state, 4n), aes_byte_at(state, 5n), aes_byte_at(state, 6n), aes_byte_at(state, 7n)})
219	        aes_mix_column(AesColumn{aes_byte_at(state, 8n), aes_byte_at(state, 9n), aes_byte_at(state, 10n), aes_byte_at(state, 11n)})
220	        aes_mix_column(AesColumn{aes_byte_at(state, 12n), aes_byte_at(state, 13n), aes_byte_at(state, 14n), aes_byte_at(state, 15n)})
221	    aes_mix_state.finish(col0, col1, col2, col3)
222	
223	def aes_middle_round(state: List<&2, U32>, words: List<&2, U32>, round: Nat) -> List<&2, U32>:
224	    aes_add_key(aes_mix_state(aes_shift_rows(aes_sub_state(state))), words, round)
225	
226	def aes_final_round(state: List<&2, U32>, words: List<&2, U32>) -> List<&2, U32>:
227	    aes_add_key(aes_shift_rows(aes_sub_state(state)), words, 14n)
228	
229	def aes_rounds.go(fuel: Nat, +state: List<&2, U32>, +words: List<&2, U32>, +round: Nat) -> List<&2, U32>:
230	    match fuel:
231	        case 0n: aes_final_round(state, words)
232	        case 1n+p:
233	            aes_rounds.go(p, aes_middle_round(state, words, round), words, (round + 1n : Nat))
234	
235	def aes256_encrypt_expanded(+words: List<&2, U32>, block: List<&2, U32>) -> List<&2, U32>:
236	    match words:
237	        case Nil{}: aes_rounds.go(13n, aes_add_key(block, words, 0n), words, 1n)
238	        case head <> tail: aes_rounds.go(13n, aes_add_key(block, words, 0n), words, 1n)
239	
240	def aes256_encrypt_block(key: List<&2, U32>, block: List<&2, U32>) -> List<&2, U32>:
241	    aes256_encrypt_expanded(aes256_expand(key), block)
242	
243	# GCM counter mode and GHASH use 16-byte blocks in network byte order.
244	def gcm_hex_mask(value: U32, mask: U32) -> U32:
245	    U32.and(mask, value)
246	
247	def gcm_mask_byte_valid(+value: U32) ->
248	    {U32.is_lt(gcm_hex_mask(value, 255), 256) == True{} : Bool}:
249	    match value:
250	        case U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: {==}
251	
252	def gcm_bytes_valid(bytes: List<&2, U32>) -> Bool:
253	    match bytes:
254	        case Nil{}: True{}
255	        case byte <> tail:
256	            U32.is_lt(byte, 256) && gcm_bytes_valid(tail)
257	
258	def gcm_mask_bytes(+bytes: List<&2, U32>) -> List<&2, U32>:
259	    match bytes:
260	        case Nil{}: Nil{}
261	        case byte <> tail:
262	            gcm_hex_mask(byte, 255) <> gcm_mask_bytes(tail)
263	
264	def gcm_mask_bytes_valid(+bytes: List<&2, U32>) ->
265	    {gcm_bytes_valid(gcm_mask_bytes(bytes)) == True{} : Bool}:
266	    match bytes:
267	        case Nil{}: {==}
268	        case byte <> tail:
269	            Equal.trans(Bool,
270	                gcm_bytes_valid(gcm_mask_bytes(byte <> tail)),
271	                Bool.and(True{}, gcm_bytes_valid(gcm_mask_bytes(tail))),
272	                True{},
273	                Equal.cong(Bool, Bool,
274	                    head => Bool.and(head,
275	                        gcm_bytes_valid(gcm_mask_bytes(tail))),
276	                    U32.is_lt(gcm_hex_mask(byte, 255), 256), True{},
277	                    gcm_mask_byte_valid(byte)),
278	                Equal.cong(Bool, Bool, tail_ok => Bool.and(True{}, tail_ok),
279	                    gcm_bytes_valid(gcm_mask_bytes(tail)), True{},
280	                    gcm_mask_bytes_valid(tail)))
281	
282	def gcm_mask_bytes_length(+bytes: List<&2, U32>) ->
283	    {List.length(&2, U32, gcm_mask_bytes(bytes)) ==
284	     List.length(&2, U32, bytes) : Nat}:
285	    match bytes:
286	        case Nil{}: {==}
287	        case byte <> tail:
288	            Equal.cong(Nat, Nat, n => 1n+n,
289	                List.length(&2, U32, gcm_mask_bytes(tail)),
290	                List.length(&2, U32, tail),
291	                gcm_mask_bytes_length(tail))
292	
293	type GcmTag is Data:
294	    GcmTag{
295	        bytes: List<&2, U32>,
296	        valid: {gcm_bytes_valid(bytes) == True{} : Bool},
297	        size: {List.length(&2, U32, bytes) == 16n : Nat}
298	    }
299	
300	type GcmCiphertext is Data:
301	    GcmCiphertext{
302	        bytes: List<&2, U32>,
303	        valid: {gcm_bytes_valid(bytes) == True{} : Bool}
304	    }
305	
306	def gcm_ciphertext_bytes(ciphertext: GcmCiphertext) -> List<&2, U32>:
307	    match ciphertext:
308	        case GcmCiphertext{bytes, valid}: bytes
309	
310	
311	def ghash_xor_if(a: U32, b: U32, yes: Bool) -> U32:
312	    match yes:
313	        case True{}: U32.xor(a, b)
314	        case False{}: a
315	
316	def ghash_xor_list.go(a: List<&2, U32>, b: List<&2, U32>, +yes: Bool,
317	                      +acc: List<&2, U32>) -> List<&2, U32>:
318	    match a b:
319	        case Nil{} _: List.reverse(&2, U32, acc)
320	        case _ Nil{}: List.reverse(&2, U32, acc)
321	        case x <> xt y <> yt:
322	            ghash_xor_list.go(xt, yt, yes, ghash_xor_if(x, y, yes) <> acc)
323	
324	def ghash_xor_list(a: List<&2, U32>, b: List<&2, U32>, yes: Bool) -> List<&2, U32>:
325	    ghash_xor_list.go(a, b, yes, Nil{})
326	
327	# Keep the 128-bit GHASH accumulator in four machine words during its hot loop.
328	type GhashField is Data:
329	    GhashField{w0: U32, w1: U32, w2: U32, w3: U32}
330	
331	def ghash_field(+bytes: List<&2, U32>) -> GhashField:
332	    +words = aes_words(bytes)
333	    GhashField{aes_word_at(words, 0n), aes_word_at(words, 1n),
334	        aes_word_at(words, 2n), aes_word_at(words, 3n)}
335	
336	def ghash_field_bytes(value: GhashField) -> List<&2, U32>:
337	    match value:
338	        case GhashField{+w0, +w1, +w2, +w3}:
339	            [U32.and(255, U32.shrn(w0, 24n)), U32.and(255, U32.shrn(w0, 16n)),
340	             U32.and(255, U32.shrn(w0, 8n)), U32.and(255, w0),
341	             U32.and(255, U32.shrn(w1, 24n)), U32.and(255, U32.shrn(w1, 16n)),
342	             U32.and(255, U32.shrn(w1, 8n)), U32.and(255, w1),
343	             U32.and(255, U32.shrn(w2, 24n)), U32.and(255, U32.shrn(w2, 16n)),
344	             U32.and(255, U32.shrn(w2, 8n)), U32.and(255, w2),
345	             U32.and(255, U32.shrn(w3, 24n)), U32.and(255, U32.shrn(w3, 16n)),
346	             U32.and(255, U32.shrn(w3, 8n)), U32.and(255, w3)]
347	
348	def ghash_field_word(value: GhashField, index: Nat) -> U32:
349	    match value index:
350	        case GhashField{w0, _, _, _} 0n: w0
351	        case GhashField{_, w1, _, _} 1n: w1
352	        case GhashField{_, _, w2, _} 2n: w2
353	        case GhashField{_, _, _, w3} _: w3
354	
355	def ghash_field_shift_top(w0: U32, reduce: Bool) -> U32:
356	    reduction_mask = U32.sub(0, Bool.to_u32(reduce))
357	    U32.xor(U32.shrn(w0, 1n), U32.and(3774873600, reduction_mask))
358	
359	def ghash_field_shift_right(value: GhashField) -> GhashField:
360	    match value:
361	        case GhashField{+w0, +w1, +w2, +w3}:
362	            GhashField{
363	                ghash_field_shift_top(w0, U32.is_ne(U32.and(1, w3), 0)),
364	                U32.or(U32.shrn(w1, 1n), U32.shln(U32.and(1, w0), 31n)),
365	                U32.or(U32.shrn(w2, 1n), U32.shln(U32.and(1, w1), 31n)),
366	                U32.or(U32.shrn(w3, 1n), U32.shln(U32.and(1, w2), 31n))}
367	
368	def ghash_field_xor_if(a: U32, b: U32, yes: Bool) -> U32:
369	    mask = U32.sub(0, Bool.to_u32(yes))
370	    U32.xor(a, U32.and(mask, b))
371	
372	def ghash_field_xor_if.all(a: GhashField, b: GhashField, +yes: Bool) -> GhashField:
373	    match a b:
374	        case GhashField{a0, a1, a2, a3} GhashField{b0, b1, b2, b3}:
375	            GhashField{ghash_field_xor_if(a0, b0, yes), ghash_field_xor_if(a1, b1, yes),
376	                ghash_field_xor_if(a2, b2, yes), ghash_field_xor_if(a3, b3, yes)}
377	
378	def ghash_mul.go(fuel: Nat, +x: GhashField, +v: GhashField,
379	                 +z: GhashField, +bit_index: Nat) -> GhashField:
380	    match fuel:
381	        case 0n: z
382	        case 1n+p:
383	            input_word = ghash_field_word(x, (bit_index / 32n : Nat))
384	            shift = (31n - (bit_index % 32n : Nat) : Nat)
385	            set = U32.is_ne(U32.and(1, U32.shrn(input_word, shift)), 0)
386	            next_z = ghash_field_xor_if.all(z, v, set)
387	            ghash_mul.go(p, x, ghash_field_shift_right(v), next_z, (bit_index + 1n : Nat))
388	
389	def ghash_mul(x: List<&2, U32>, h: List<&2, U32>) -> List<&2, U32>:
390	    ghash_field_bytes(ghash_mul.go(128n, ghash_field(x), ghash_field(h),
391	        GhashField{0,0,0,0}, 0n))
392	
393	def ghash_update(y: List<&2, U32>, h: List<&2, U32>, block: List<&2, U32>) -> List<&2, U32>:
394	    ghash_mul(ghash_xor_list(y, block, True{}), h)
395	
396	def ghash_zero_pad.go(fuel: Nat, +bytes: List<&2, U32>) -> List<&2, U32>:
397	    match fuel:
398	        case 0n: bytes
399	        case 1n+p: ghash_zero_pad.go(p, List.append(&2, U32, bytes, [0]))
400	
401	def ghash_finish(space: Nat, block_rev: List<&2, U32>, h: List<&2, U32>, y: List<&2, U32>) -> List<&2, U32>:
402	    match space:
403	        case 16n: y
404	        case 0n: ghash_update(y, h, List.reverse(&2, U32, block_rev))
405	        case 1n+p:
406	            ghash_update(y, h, ghash_zero_pad.go(space, List.reverse(&2, U32, block_rev)))
407	
408	def ghash_bytes.go(fuel: Nat, bytes: List<&2, U32>, space: Nat,
409	                   +block_rev: List<&2, U32>, +h: List<&2, U32>, +y: List<&2, U32>) -> List<&2, U32>:
410	    match fuel bytes space:
411	        case 0n Nil{} _: ghash_finish(space, block_rev, h, y)
412	        case 0n _ _: ghash_finish(space, block_rev, h, y)
413	        case 1n+p Nil{} _: ghash_finish(space, block_rev, h, y)
414	        case 1n+p byte <> tail 0n:
415	            y2 = ghash_update(y, h, List.reverse(&2, U32, block_rev))
416	            ghash_bytes.go(p, tail, 15n, [byte], h, y2)
417	        case 1n+p byte <> tail 1n+s:
418	            ghash_bytes.go(p, tail, s, byte <> block_rev, h, y)
419	
420	def ghash_bytes(+bytes: List<&2, U32>, h: List<&2, U32>, y: List<&2, U32>) -> List<&2, U32>:
421	    ghash_bytes.go(List.length(&2, U32, bytes), bytes, 16n, Nil{}, h, y)
422	
423	def ghash_nat_bytes.go(fuel: Nat, qr: Nat & Nat, +acc: List<&2, U32>) -> List<&2, U32>:
424	    match fuel:
425	        case 0n: acc
426	        case 1n+p:
427	            (q, r) = qr
428	            ghash_nat_bytes.go(p, Nat.divmod(q, 256n), U32.from_nat(r) <> acc)
429	
430	def ghash_nat_bytes(n: Nat) -> List<&2, U32>:
431	    ghash_nat_bytes.go(8n, Nat.divmod(n, 256n), Nil{})
432	
433	def ghash_auth_with_hash_impl(+h: List<&2, U32>, +aad: List<&2, U32>, +ciphertext: List<&2, U32>) -> List<&2, U32>:
434	    y0: List<&2, U32> = [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0]
435	    y1 = ghash_bytes(aad, h, y0)
436	    y2 = ghash_bytes(ciphertext, h, y1)
437	    aad_bits = ghash_nat_bytes((List.length(&2, U32, aad) * 8n : Nat))
438	    ct_bits = ghash_nat_bytes((List.length(&2, U32, ciphertext) * 8n : Nat))
439	    ghash_update(y2, h, List.append(&2, U32, aad_bits, ct_bits))
440	
441	# Do not expand a symbolic GHASH multiplication while transporting its hash.
442	def ghash_auth_with_hash(+h: List<&2, U32>, +aad: List<&2, U32>, +ciphertext: List<&2, U32>) -> List<&2, U32>:
443	    match aad:
444	        case Nil{}: ghash_auth_with_hash_impl(h, aad, ciphertext)
445	        case head <> tail: ghash_auth_with_hash_impl(h, aad, ciphertext)
446	
447	def ghash_auth_expanded(words: List<&2, U32>, aad: List<&2, U32>, ciphertext: List<&2, U32>) -> List<&2, U32>:
448	    ghash_auth_with_hash(aes256_encrypt_expanded(words,
449	        [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0]), aad, ciphertext)
450	
451	def gcm_j0(nonce: List<&2, U32>) -> List<&2, U32>:
452	    List.append(&2, U32, nonce, [0,0,0,1])
453	
454	def gcm_inc32(+counter: List<&2, U32>) -> List<&2, U32>:
455	    hi = U32.shln(aes_byte_at(counter, 12n), 24n)
456	    mid1 = U32.shln(aes_byte_at(counter, 13n), 16n)
457	    mid2 = U32.shln(aes_byte_at(counter, 14n), 8n)
458	    lo = aes_byte_at(counter, 15n)
459	    +word = U32.add(U32.or(U32.or(hi, mid1), U32.or(mid2, lo)), 1)
460	    List.append(&2, U32, List.take(&2, U32, counter, 12n),
461	        [U32.and(255, U32.shrn(word, 24n)), U32.and(255, U32.shrn(word, 16n)),
462	         U32.and(255, U32.shrn(word, 8n)), U32.and(255, word)])
463	
464	def gcm_ctr_stream.go(fuel: Nat, +words: List<&2, U32>, +counter: List<&2, U32>,
465	                      +acc: List<&2, U32>) -> List<&2, U32>:
466	    match fuel:
467	        case 0n: List.reverse(&2, U32, acc)
468	        case 1n+p:
469	            stream = aes256_encrypt_expanded(words, counter)
470	            next_acc = List.append(&2, U32, List.reverse(&2, U32, stream), acc)
471	            gcm_ctr_stream.go(p, words, gcm_inc32(counter), next_acc)
472	
473	def gcm_ctr_advance(fuel: Nat, +counter: List<&2, U32>) -> List<&2, U32>:
474	    match fuel:
475	        case 0n: counter
476	        case 1n+p: gcm_ctr_advance(p, gcm_inc32(counter))
477	
478	type GcmCtrStep is Data:
479	    GcmCtrStep{byte: U32, counter: List<&2, U32>, rest: List<&2, U32>}
480	
481	def gcm_ctr_step(+words: List<&2, U32>, +counter: List<&2, U32>,
482	    block: List<&2, U32>) -> GcmCtrStep:
483	    match block:
484	        case Nil{}:
485	            +next_block = aes256_encrypt_expanded(words, counter)
486	            GcmCtrStep{aes_byte_at(next_block, 0n), gcm_inc32(counter),
487	                List.tail(&2, U32, next_block)}
488	        case byte <> rest: GcmCtrStep{byte, counter, rest}
489	
490	def gcm_ctr_step_byte(step: GcmCtrStep) -> U32:
491	    match step:
492	        case GcmCtrStep{byte, _, _}: byte
493	
494	def gcm_ctr_step_counter(step: GcmCtrStep) -> List<&2, U32>:
495	    match step:
496	        case GcmCtrStep{_, counter, _}: counter
497	
498	def gcm_ctr_step_rest(step: GcmCtrStep) -> List<&2, U32>:
499	    match step:
500	        case GcmCtrStep{_, _, rest}: rest
501	
502	# Generate each AES counter block once and consume all of its bytes. Fuel is
503	# still a byte count, so partial final blocks have exactly the requested length.
504	def gcm_ctr_stream_exact.go(fuel: Nat, +words: List<&2, U32>,
505	    counter: List<&2, U32>, block: List<&2, U32>) -> List<&2, U32>:
506	    match fuel:
507	        case 0n: Nil{}
508	        case 1n+p:
509	            +step = gcm_ctr_step(words, counter, block)
510	            gcm_ctr_step_byte(step) <>
511	                gcm_ctr_stream_exact.go(p, words, gcm_ctr_step_counter(step),
512	                    gcm_ctr_step_rest(step))
513	
514	def gcm_ctr_stream_exact(fuel: Nat, +words: List<&2, U32>,
515	    +start: List<&2, U32>) -> List<&2, U32>:
516	    gcm_ctr_stream_exact.go(fuel, words, start, Nil{})
517	
518	def gcm_zip_xor(+bytes: List<&2, U32>, +stream: List<&2, U32>) -> List<&2, U32>:
519	    match bytes stream:
520	        case Nil{} _: Nil{}
521	        case _ Nil{}: Nil{}
522	        case byte <> tail stream_byte <> stream_tail:
523	            gcm_hex_mask(U32.xor(byte, stream_byte), 255) <>
524	                gcm_zip_xor(tail, stream_tail)
525	
526	def gcm_zip_xor_nil_left(+stream: List<&2, U32>) ->
527	    {gcm_zip_xor(Nil{}, stream) == Nil{} : List<&2, U32>}:
528	    match stream:
529	        case Nil{}: {==}
530	        case _ <> _: {==}
531	
532	def gcm_zip_xor_nil_right(+bytes: List<&2, U32>) ->
533	    {gcm_zip_xor(bytes, Nil{}) == Nil{} : List<&2, U32>}:
534	    match bytes:
535	        case Nil{}: {==}
536	        case _ <> _: {==}
537	
538	def gcm_zip_xor_valid(+bytes: List<&2, U32>, +stream: List<&2, U32>) ->
539	    {gcm_bytes_valid(gcm_zip_xor(bytes, stream)) == True{} : Bool}:
540	    match bytes stream:
541	        case Nil{} _:
542	            Equal.trans(Bool,
543	                gcm_bytes_valid(gcm_zip_xor(Nil{}, stream)),
544	                gcm_bytes_valid(Nil{}), True{},
545	                Equal.cong(List<&2, U32>, Bool, gcm_bytes_valid,
546	                    gcm_zip_xor(Nil{}, stream), Nil{},
547	                    gcm_zip_xor_nil_left(stream)),
548	                {==})
549	        case _ Nil{}:
550	            Equal.trans(Bool,
551	                gcm_bytes_valid(gcm_zip_xor(bytes, Nil{})),
552	                gcm_bytes_valid(Nil{}), True{},
553	                Equal.cong(List<&2, U32>, Bool, gcm_bytes_valid,
554	                    gcm_zip_xor(bytes, Nil{}), Nil{},
555	                    gcm_zip_xor_nil_right(bytes)),
556	                {==})
557	        case byte <> tail stream_byte <> stream_tail:
558	            recursive = gcm_zip_xor_valid(tail, stream_tail)
559	            range = gcm_mask_byte_valid(U32.xor(byte, stream_byte))
560	            head_changed = Equal.cong(Bool, Bool,
561	                head => Bool.and(head,
562	                    gcm_bytes_valid(gcm_zip_xor(tail, stream_tail))),
563	                U32.is_lt(gcm_hex_mask(U32.xor(byte, stream_byte), 255), 256),
564	                True{}, range)
565	            tail_changed = Equal.cong(Bool, Bool,
566	                valid => Bool.and(True{}, valid),
567	                gcm_bytes_valid(gcm_zip_xor(tail, stream_tail)), True{},
568	                recursive)
569	            Equal.trans(Bool,
570	                Bool.and(
571	                    U32.is_lt(gcm_hex_mask(U32.xor(byte, stream_byte), 255), 256),
572	                    gcm_bytes_valid(gcm_zip_xor(tail, stream_tail))),
573	                Bool.and(True{}, gcm_bytes_valid(gcm_zip_xor(tail, stream_tail))),
574	                True{}, head_changed,
575	                Equal.trans(Bool,
576	                    Bool.and(True{}, gcm_bytes_valid(gcm_zip_xor(tail, stream_tail))),
577	                    Bool.and(True{}, True{}), True{}, tail_changed, {==}))
578	
579	# A GCM tag is exactly sixteen bytes. Expose that shape without unfolding
580	# abstract AES rounds or GHASH values when checking its certificates.
581	def gcm_tag_parts(+auth: List<&2, U32>, +mask: List<&2, U32>) -> List<&2, U32>:
582	    [U32.xor(aes_byte_at(mask, 0n), aes_byte_at(auth, 0n)),
583	     U32.xor(aes_byte_at(mask, 1n), aes_byte_at(auth, 1n)),
584	     U32.xor(aes_byte_at(mask, 2n), aes_byte_at(auth, 2n)),
585	     U32.xor(aes_byte_at(mask, 3n), aes_byte_at(auth, 3n)),
586	     U32.xor(aes_byte_at(mask, 4n), aes_byte_at(auth, 4n)),
587	     U32.xor(aes_byte_at(mask, 5n), aes_byte_at(auth, 5n)),
588	     U32.xor(aes_byte_at(mask, 6n), aes_byte_at(auth, 6n)),
589	     U32.xor(aes_byte_at(mask, 7n), aes_byte_at(auth, 7n)),
590	     U32.xor(aes_byte_at(mask, 8n), aes_byte_at(auth, 8n)),
591	     U32.xor(aes_byte_at(mask, 9n), aes_byte_at(auth, 9n)),
592	     U32.xor(aes_byte_at(mask, 10n), aes_byte_at(auth, 10n)),
593	     U32.xor(aes_byte_at(mask, 11n), aes_byte_at(auth, 11n)),
594	     U32.xor(aes_byte_at(mask, 12n), aes_byte_at(auth, 12n)),
595	     U32.xor(aes_byte_at(mask, 13n), aes_byte_at(auth, 13n)),
596	     U32.xor(aes_byte_at(mask, 14n), aes_byte_at(auth, 14n)),
597	     U32.xor(aes_byte_at(mask, 15n), aes_byte_at(auth, 15n))]
598	
599	def gcm_tag_output_impl(+words: List<&2, U32>, nonce: List<&2, U32>,
600	                   aad: List<&2, U32>, ciphertext: List<&2, U32>) -> GcmTag:
601	    auth mask = ghash_auth_expanded(words, aad, ciphertext)
602	        aes256_encrypt_expanded(words, gcm_j0(nonce))
603	    +raw_tag = gcm_tag_parts(auth, mask)
604	    GcmTag{gcm_mask_bytes(raw_tag), gcm_mask_bytes_valid(raw_tag), {==}}
605	
606	# Keep an abstract key schedule abstract during proof normalization. Splitting
607	# on the nonce leaves the key schedule abstract in both identical branches.
608	def gcm_tag_output(+words: List<&2, U32>, nonce: List<&2, U32>,
609	                   aad: List<&2, U32>, ciphertext: List<&2, U32>) -> GcmTag:
610	    match nonce:
611	        case Nil{}: gcm_tag_output_impl(words, nonce, aad, ciphertext)
612	        case head <> tail: gcm_tag_output_impl(words, nonce, aad, ciphertext)
613	
614	def gcm_tag_bytes(tag_output: GcmTag) -> List<&2, U32>:
615	    match tag_output:
616	        case GcmTag{bytes, valid, size}: bytes
617	
618	def gcm_tag_valid(tag_output: GcmTag) ->
619	    {gcm_bytes_valid(gcm_tag_bytes(tag_output)) == True{} : Bool}:
620	    match tag_output:
621	        case GcmTag{bytes, valid, size}: valid
622	
623	def gcm_tag_size(tag_output: GcmTag) ->
624	    {List.length(&2, U32, gcm_tag_bytes(tag_output)) == 16n : Nat}:
625	    match tag_output:
626	        case GcmTag{bytes, valid, size}: size
627	
628	type GcmOutput is Data:
629	    GcmOutput{
630	        ciphertext: List<&2, U32>,
631	        ciphertext_valid: {gcm_bytes_valid(ciphertext) == True{} : Bool},
632	        tag_bytes: List<&2, U32>,
633	        tag_valid: {gcm_bytes_valid(tag_bytes) == True{} : Bool},
634	        tag_size: {List.length(&2, U32, tag_bytes) == 16n : Nat},
635	        tag_words: List<&2, U32>,
636	        tag_nonce: List<&2, U32>,
637	        tag_aad: List<&2, U32>,
638	        tag_matches: {tag_bytes == gcm_tag_bytes(
639	            gcm_tag_output(tag_words, tag_nonce, tag_aad, ciphertext)) :
640	            List<&2, U32>}
641	    }
642	
643	def gcm_output_tag_bytes(output: GcmOutput) -> List<&2, U32>:
644	    match output:
645	        case GcmOutput{ciphertext, ciphertext_valid, tag_bytes,
646	            tag_valid, tag_size, tag_words, tag_nonce, tag_aad, tag_matches}:
647	            tag_bytes
648	
649	def gcm_output_tag_valid(output: GcmOutput) ->
650	    {gcm_bytes_valid(gcm_output_tag_bytes(output)) == True{} : Bool}:
651	    match output:
652	        case GcmOutput{ciphertext, ciphertext_valid, tag_bytes,
653	            tag_valid, tag_size, tag_words, tag_nonce, tag_aad, tag_matches}:
654	            tag_valid
655	
656	def gcm_output_tag_size(output: GcmOutput) ->
657	    {List.length(&2, U32, gcm_output_tag_bytes(output)) == 16n : Nat}:
658	    match output:
659	        case GcmOutput{ciphertext, ciphertext_valid, tag_bytes,
660	            tag_valid, tag_size, tag_words, tag_nonce, tag_aad, tag_matches}:
661	            tag_size
662	
663	def gcm_output_from_tag(+words: List<&2, U32>, +nonce: List<&2, U32>,
664	    +aad: List<&2, U32>, +ciphertext: List<&2, U32>,
665	    ciphertext_valid: {gcm_bytes_valid(ciphertext) == True{} : Bool}) ->
666	    GcmOutput:
667	    +tag_output = gcm_tag_output(words, nonce, aad, ciphertext)
668	    GcmOutput{ciphertext, ciphertext_valid, gcm_tag_bytes(tag_output),
669	        gcm_tag_valid(tag_output), gcm_tag_size(tag_output), words, nonce,
670	        aad, {==}}
671	
672	def gcm_output_from_ciphertext(+words: List<&2, U32>,
673	    nonce: List<&2, U32>, aad: List<&2, U32>,
674	    cipher_output: GcmCiphertext) -> GcmOutput:
675	    match cipher_output:
676	        case GcmCiphertext{+ciphertext, valid}:
677	            gcm_output_from_tag(words, nonce, aad, ciphertext, valid)
678	
679	def gcm_ctr_encrypt(+words: List<&2, U32>, nonce: List<&2, U32>,
680	    +plaintext: List<&2, U32>) -> GcmCiphertext:
681	    +start = gcm_inc32(gcm_j0(nonce))
682	    +stream = gcm_ctr_stream_exact(List.length(&2, U32, plaintext),
683	        words, start)
684	    GcmCiphertext{gcm_zip_xor(plaintext, stream),
685	        gcm_zip_xor_valid(plaintext, stream)}
686	
687	def gcm_encrypt_raw(+key: List<&2, U32>, +nonce: List<&2, U32>,
688	                    +aad: List<&2, U32>, +plaintext: List<&2, U32>) -> GcmOutput:
689	    +words = aes256_expand(key)
690	    gcm_output_from_ciphertext(words, nonce, aad,
691	        gcm_ctr_encrypt(words, nonce, plaintext))
692	
693	def gcm_decrypt_expanded(+words: List<&2, U32>, nonce: List<&2, U32>, +ciphertext: List<&2, U32>) -> List<&2, U32>:
694	    +start = gcm_inc32(gcm_j0(nonce))
695	    +stream = gcm_ctr_stream_exact(List.length(&2, U32, ciphertext),
696	        words, start)
697	    gcm_zip_xor(ciphertext, stream)
698	
699	def gcm_decrypt_raw(+key: List<&2, U32>, nonce: List<&2, U32>, +ciphertext: List<&2, U32>) -> List<&2, U32>:
700	    gcm_decrypt_expanded(aes256_expand(key), nonce, ciphertext)
701	
702	# Authenticate ciphertext directly; expand the key once for both AES calls.
703	def gcm_tag_expanded(+words: List<&2, U32>, nonce: List<&2, U32>, aad: List<&2, U32>, ciphertext: List<&2, U32>) -> List<&2, U32>:
704	    gcm_tag_bytes(gcm_tag_output(words, nonce, aad, ciphertext))
705	
706	def gcm_tag(+key: List<&2, U32>, nonce: List<&2, U32>, aad: List<&2, U32>, ciphertext: List<&2, U32>) -> List<&2, U32>:
707	    gcm_tag_expanded(aes256_expand(key), nonce, aad, ciphertext)
708	
709	def ghash_auth(key: List<&2, U32>, aad: List<&2, U32>, ciphertext: List<&2, U32>) -> List<&2, U32>:
710	    ghash_auth_expanded(aes256_expand(key), aad, ciphertext)