libs/AES256GCMCore.bend

qasim-bend-kit@0.1.0.2 · 710 lines · 113 definitions

1import Base
2import qasim-bend-kit@0.1.0.2/libs/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.

6def 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
10def gf8_xtime.high(+a: U32, high: Bool) -> U32:
11    xor_if(U32.and(255, U32.shln(a, 1n)), 27, high)
12
13def gf8_xtime(+a: U32) -> U32:
14    gf8_xtime.high(a, U32.is_ne(U32.and(128, a), 0))
15
16def 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
24def gf8_mul(a: U32, b: U32) -> U32:
25    gf8_mul.go(8n, a, b, 0)
26
27def 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
34def gf8_pow(a: U32, exp: U32) -> U32:
35    gf8_pow.go(8n, a, exp, 1)
36
37def rotl8(+a: U32, +shift: Nat) -> U32:
38    U32.and(255, U32.or(U32.shln(a, shift), U32.shrn(a, (8n - shift : Nat))))
39
40def 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
46def aes_sbox(+x: U32) -> U32:
47    SBox.lookup(x)
48
49def 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
55def aes_rotword(+w: U32) -> U32:
56    U32.or(U32.shln(w, 8n), U32.shrn(w, 24n))
57
58def aes_rcon_step(r: U32) -> U32:
59    gf8_xtime(r)
60
61def 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
65def 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
71def aes_word_from_maybe(value: Maybe<&2, U32>) -> U32:
72    match value:
73        case None{}: 0
74        case Some{w}: w
75
76def aes_word_at(words: List<&2, U32>, i: Nat) -> U32:
77    aes_word_from_maybe(List.get(&2, U32, words, i))
78
79def 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
84def 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
87def 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
92def aes_rcon_kind(rcon: U32, advance: Bool) -> U32:
93    match advance:
94        case True{}: aes_rcon_step(rcon)
95        case False{}: rcon
96
97def 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
110def 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.

115def 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
120def aes256_expand(+key: List<&2, U32>) -> List<&2, U32>:
121    aes_expand_key(52n, key)
122
123def 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
137def 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
140def 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
146def aes_sub_state(state: List<&2, U32>) -> List<&2, U32>:
147    aes_sub_state.go(state, Nil{})
148
149def aes_byte_from_maybe(value: Maybe<&2, U32>) -> U32:
150    match value:
151        case None{}: 0
152        case Some{byte}: byte
153
154def aes_byte_at(state: List<&2, U32>, index: Nat) -> U32:
155    aes_byte_from_maybe(List.get(&2, U32, state, index))
156
157def 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
163type AesColumn is Data:
164    AesColumn{a: U32, b: U32, c: U32, d: U32}
165
166def 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
175def 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
180def 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
185def 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
190def 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
195def 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
202def 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
210def 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
215def 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
223def 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
226def 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
229def 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
235def 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
240def 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.

244def gcm_hex_mask(value: U32, mask: U32) -> U32:
245    U32.and(mask, value)
246
247def 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
252def 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
258def 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
264def 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
282def 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
293type 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
300type GcmCiphertext is Data:
301    GcmCiphertext{
302        bytes: List<&2, U32>,
303        valid: {gcm_bytes_valid(bytes) == True{} : Bool}
304    }
305
306def gcm_ciphertext_bytes(ciphertext: GcmCiphertext) -> List<&2, U32>:
307    match ciphertext:
308        case GcmCiphertext{bytes, valid}: bytes
309
310
311def 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
316def 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
324def 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.

328type GhashField is Data:
329    GhashField{w0: U32, w1: U32, w2: U32, w3: U32}
330
331def 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
336def 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
348def 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
355def 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
359def 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
368def 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
372def 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
378def 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
389def 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
393def 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
396def 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
401def 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
408def 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
420def 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
423def 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
430def ghash_nat_bytes(n: Nat) -> List<&2, U32>:
431    ghash_nat_bytes.go(8n, Nat.divmod(n, 256n), Nil{})
432
433def 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.

442def 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
447def 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
451def gcm_j0(nonce: List<&2, U32>) -> List<&2, U32>:
452    List.append(&2, U32, nonce, [0,0,0,1])
453
454def 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
464def 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
473def 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
478type GcmCtrStep is Data:
479    GcmCtrStep{byte: U32, counter: List<&2, U32>, rest: List<&2, U32>}
480
481def 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
490def gcm_ctr_step_byte(step: GcmCtrStep) -> U32:
491    match step:
492        case GcmCtrStep{byte, _, _}: byte
493
494def gcm_ctr_step_counter(step: GcmCtrStep) -> List<&2, U32>:
495    match step:
496        case GcmCtrStep{_, counter, _}: counter
497
498def 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.

504def 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
514def 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
518def 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
526def 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
532def 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
538def 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.

581def 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
599def 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.

608def 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
614def gcm_tag_bytes(tag_output: GcmTag) -> List<&2, U32>:
615    match tag_output:
616        case GcmTag{bytes, valid, size}: bytes
617
618def 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
623def 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
628type 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
643def 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
649def 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
656def 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
663def 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
672def 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
679def 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
687def 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
693def 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
699def 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.

703def 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
706def 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
709def 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)