libs/AES256GCM.bend

qasim-bend-kit@0.1.0.2 · 588 lines · 86 definitions

1import Base
2import qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend as Core
3
4# AES-256-GCM with validated inputs and canonical envelope serialization.

5# Bytes use U32 storage, with validation certificates excluding values above 255.
6def bytes_valid(bytes: List<&2, U32>) -> Bool:
7    match bytes:
8        case Nil{}: True{}
9        case head <> tail:
10            U32.is_lt(head, 256) && bytes_valid(tail)
11
12def core_bytes_valid_eq(+bytes: List<&2, U32>) ->
13    {bytes_valid(bytes) == Core.gcm_bytes_valid(bytes) : Bool}:
14    match bytes:
15        case Nil{}: {==}
16        case head <> tail:
17            recursive = core_bytes_valid_eq(tail)
18            Equal.cong(Bool, Bool,
19                valid => Bool.and(U32.is_lt(head, 256), valid),
20                bytes_valid(tail), Core.gcm_bytes_valid(tail), recursive)
21
22def core_bytes_valid_proof(bytes: List<&2, U32>,
23    valid: {Core.gcm_bytes_valid(bytes) == True{} : Bool}) ->
24    {bytes_valid(bytes) == True{} : Bool}:
25    Equal.trans(Bool, bytes_valid(bytes), Core.gcm_bytes_valid(bytes), True{},
26        core_bytes_valid_eq(bytes), valid)
27
28# Count at most the supported byte bound with two wrapping words. This avoids

29# constructing or dividing enormous Peano Nat bounds for symbolic lists.

30
31def length_pair_high(low: U32, high_cmp: Cmp, max_low: U32) -> Bool:
32    match high_cmp:
33        case LT{}: True{}
34        case EQ{}: U32.is_le(low, max_low)
35        case GT{}: False{}
36
37def length_pair_within(low: U32, high: U32, max_low: U32, max_high: U32) -> Bool:
38    length_pair_high(low, U32.cmp(high, max_high), max_low)
39
40def bytes_length_limit.go(fuel: Nat, bytes: List<&2, U32>,
41                          low: U32, +high: U32, +max_low: U32, +max_high: U32,
42                          within: Bool) -> Bool:
43    match fuel bytes within:
44        case 0n Nil{} _: within
45        case 0n _ <> _ _: False{}
46        case 1n+p Nil{} _: False{}
47        case 1n+p _ <> _ False{}: False{}
48        case 1n+p _ <> tail True{}:
49            +next_low = U32.add(low, 1)
50            +next_high = Bool.pick(U32, U32.is_eq(next_low, 0), U32.add(high, 1), high)
51            bytes_length_limit.go(p, tail, next_low, next_high,
52                max_low, max_high,
53                length_pair_within(next_low, next_high, max_low, max_high))
54
55def bytes_length_limit(+bytes: List<&2, U32>, max_low: U32, max_high: U32) -> Bool:
56    bytes_length_limit.go(List.length(&2, U32, bytes), bytes,
57        0, 0, max_low, max_high, True{})
58
59# GCM limits are expressed in bytes after requiring byte-aligned input.

60def plaintext_valid(+bytes: List<&2, U32>) -> Bool:
61    bytes_valid(bytes) && bytes_length_limit(bytes, 4294967264, 15)
62
63def aad_valid(+bytes: List<&2, U32>) -> Bool:
64    bytes_valid(bytes) && bytes_length_limit(bytes, 4294967295, 536870911)
65
66type SecretKey is Data:
67    SecretKey{
68        bytes: List<&2, U32>,
69        -size: {List.length(&2, U32, bytes) == 32n : Nat},
70        -valid: {bytes_valid(bytes) == True{} : Bool}
71    }
72
73type Nonce is Data:
74    Nonce{
75        bytes: List<&2, U32>,
76        size: {List.length(&2, U32, bytes) == 12n : Nat},
77        valid: {bytes_valid(bytes) == True{} : Bool}
78    }
79
80type Tag is Data:
81    Tag{
82        bytes: List<&2, U32>,
83        size: {List.length(&2, U32, bytes) == 16n : Nat},
84        valid: {bytes_valid(bytes) == True{} : Bool}
85    }
86
87type Envelope is Data:
88    Envelope{
89        nonce: Nonce,
90        ciphertext: List<&2, U32>,
91        tag: Tag,
92        valid: {bytes_valid(ciphertext) == True{} : Bool}
93    }
94
95type Error is Data:
96    InvalidKey{}
97    InvalidNonce{}
98    InvalidBytes{}
99    InvalidEnvelope{}
100    AuthenticationFailed{}
101
102# Constructors validate raw input; SecretKey/Nonce/Tag certificates enforce sizes.

103law key:
104    for bytes: List<&2, U32>
105    Result<&2, &2, Error, SecretKey>
106
107law nonce:
108    for bytes: List<&2, U32>
109    Result<&2, &2, Error, Nonce>
110
111# Deterministic primitive: the caller supplies a nonce unique for this key.

112# The eventual effectful wrapper must generate nonces using an OS CSPRNG.

113law encrypt:
114    for key: SecretKey
115    for nonce: Nonce
116    for aad: List<&2, U32>
117    for plaintext: List<&2, U32>
118    Result<&2, &2, Error, Envelope>
119
120# Fail contains only an Error, never unauthenticated or partial plaintext.

121law decrypt:
122    for key: SecretKey
123    for aad: List<&2, U32>
124    for envelope: Envelope
125    Result<&2, &2, Error, List<&2, U32>>
126
127# Canonical envelope: v1.<lowercase nonce hex>.<lowercase tag hex>.<ciphertext hex>.

128# The nonce has 24 hex characters, the tag 32, ciphertext an even number (or 0).

129# AAD is external and must be supplied unchanged when decrypting.

130law encode:
131    for envelope: Envelope
132    String
133
134law parse:
135    for text: String
136    Result<&2, &2, Error, Envelope>
137
138# Read-only projections needed to state the contract.

139def nonce_bytes(nonce: Nonce) -> List<&2, U32>:
140    match nonce:
141        case Nonce{bytes, size, valid}: bytes
142
143def tag_bytes(tag: Tag) -> List<&2, U32>:
144    match tag:
145        case Tag{bytes, size, valid}: bytes
146
147def tag_bytes_size(tag: Tag) ->
148    {List.length(&2, U32, tag_bytes(tag)) == 16n : Nat}:
149    match tag:
150        case Tag{bytes, size, valid}: size
151
152def tag_bytes_valid(tag: Tag) ->
153    {bytes_valid(tag_bytes(tag)) == True{} : Bool}:
154    match tag:
155        case Tag{bytes, size, valid}: valid
156
157def ciphertext(envelope: Envelope) -> List<&2, U32>:
158    match envelope:
159        case Envelope{nonce, ciphertext, tag, valid}: ciphertext
160
161def envelope_ciphertext_valid(envelope: Envelope) ->
162    {bytes_valid(ciphertext(envelope)) == True{} : Bool}:
163    match envelope:
164        case Envelope{nonce, ciphertext, tag, valid}: valid
165
166def envelope_nonce(envelope: Envelope) -> Nonce:
167    match envelope:
168        case Envelope{nonce, ciphertext, tag, valid}: nonce
169
170def envelope_tag(envelope: Envelope) -> Tag:
171    match envelope:
172        case Envelope{nonce, ciphertext, tag, valid}: tag
173
174# Canonical lowercase hexadecimal envelope serialization.

175def hex_digit_kind(+n: U32, decimal: Bool) -> Char:
176    match decimal:
177        case True{}: Chr{U32.add(48, n)}
178        case False{}: Chr{U32.add(87, n)}
179
180# The mask-first implementation keeps zero mask bits visibly false to Bend's
181# checker, which supports the nibble range proofs used by the codec.
182def hex_word_and(n: Nat, mask: Word(n), +value: Word(n)) -> Word(n):
183    match n:
184        case 0n: WNil{}
185        case 1n+p:
186            match mask:
187                case WCon{False{}, mask_tail}:
188                    match value:
189                        case WCon{_, value_tail}:
190                            WCon{False{}, hex_word_and(p, mask_tail, value_tail)}
191                case WCon{True{}, mask_tail}:
192                    match value:
193                        case WCon{bit, value_tail}:
194                            WCon{bit, hex_word_and(p, mask_tail, value_tail)}
195
196def hex_mask(value: U32, mask: U32) -> U32:
197    match value mask:
198        case U32{value_word} U32{mask_word}:
199            U32{hex_word_and(32n, mask_word, value_word)}
200
201def hex_digit.nibble(+n: U32) -> Char:
202    match n:
203        case 0: Chr{48}
204        case 1: Chr{49}
205        case 2: Chr{50}
206        case 3: Chr{51}
207        case 4: Chr{52}
208        case 5: Chr{53}
209        case 6: Chr{54}
210        case 7: Chr{55}
211        case 8: Chr{56}
212        case 9: Chr{57}
213        case 10: Chr{97}
214        case 11: Chr{98}
215        case 12: Chr{99}
216        case 13: Chr{100}
217        case 14: Chr{101}
218        case 15: Chr{102}
219        case _: hex_digit_kind(n, U32.is_lt(n, 10))
220
221def hex_digit(+n: U32) -> Char:
222    hex_digit.nibble(hex_mask(n, 15))
223
224def hex_bytes(+bytes: List<&2, U32>) -> String:
225    match bytes:
226        case Nil{}: ""
227        case +byte <> tail:
228            +normalized = hex_mask(byte, 255)
229            SCon{hex_digit(U32.shrn(normalized, 4n)),
230                SCon{hex_digit(normalized), hex_bytes(tail)}}
231
232# Serialize validated fixed-size fields through a fixed-size byte view. This
233# makes the wire length structural even when the constructor certificate is
234# erased from runtime storage.
235def fixed_bytes(n: Nat, bytes: List<&2, U32>) -> List<&2, U32>:
236    match n:
237        case 0n: Nil{}
238        case 1n+p:
239            match bytes:
240                case Nil{}: 0 <> fixed_bytes(p, Nil{})
241                case byte <> tail: byte <> fixed_bytes(p, tail)
242
243def encode_impl(envelope: Envelope) -> String:
244    match envelope:
245        case Envelope{nonce, ciphertext, tag, valid}:
246            match nonce:
247                case Nonce{nonce_bytes, size, valid}:
248                    "v1." ++ hex_bytes(fixed_bytes(12n, nonce_bytes)) ++ "." ++
249                        hex_bytes(fixed_bytes(16n, tag_bytes(tag))) ++ "." ++
250                        hex_bytes(ciphertext)
251
252# Match the ASCII code point directly so each accepted nibble normalizes to a literal.

253def hex_nibble(+code: U32) -> Maybe<&2, U32>:
254    match code:
255        case 48: Some{0}
256        case 49: Some{1}
257        case 50: Some{2}
258        case 51: Some{3}
259        case 52: Some{4}
260        case 53: Some{5}
261        case 54: Some{6}
262        case 55: Some{7}
263        case 56: Some{8}
264        case 57: Some{9}
265        case 97: Some{10}
266        case 98: Some{11}
267        case 99: Some{12}
268        case 100: Some{13}
269        case 101: Some{14}
270        case 102: Some{15}
271        case _: None{}
272
273def hex_join(high: U32, low: U32) -> U32:
274    match high low:
275        case U32{WCon{h0, WCon{h1, WCon{h2, WCon{h3, _}}}}}
276             U32{WCon{l0, WCon{l1, WCon{l2, WCon{l3, _}}}}}:
277            U32{WCon{l0, WCon{l1, WCon{l2, WCon{l3,
278                WCon{h0, WCon{h1, WCon{h2, WCon{h3, Word.zero(24n)}}}}}}}}}
279
280def hex_pair.combine(high: Maybe<&2, U32>, low: Maybe<&2, U32>) -> Maybe<&2, U32>:
281    match high low:
282        case None{} _: None{}
283        case Some{high} None{}: None{}
284        case Some{high} Some{low}: Some{hex_join(high, low)}
285
286def hex_pair(first: Char, second: Char) -> Maybe<&2, U32>:
287    hex_pair.combine(hex_nibble(Char.to_u32(first)),
288        hex_nibble(Char.to_u32(second)))
289
290def hex_pairs(chars: List<&2, Char>) -> List<&2, Maybe<&2, U32>>:
291    match chars:
292        case Nil{}: Nil{}
293        case first <> Nil{}: [None{}]
294        case first <> second <> tail:
295            hex_pair(first, second) <> hex_pairs(tail)
296
297def collect_hex.cons(pair: Maybe<&2, U32>, result: Maybe<&2, List<&2, U32>>) ->
298    Maybe<&2, List<&2, U32>>:
299    match pair result:
300        case None{} _: None{}
301        case Some{_} None{}: None{}
302        case Some{byte} Some{bytes}: Some{byte <> bytes}
303
304def collect_hex(pairs: List<&2, Maybe<&2, U32>>) -> Maybe<&2, List<&2, U32>>:
305    match pairs:
306        case Nil{}: Some{Nil{}}
307        case pair <> tail: collect_hex.cons(pair, collect_hex(tail))
308
309def decode_hex(text: String) -> Maybe<&2, List<&2, U32>>:
310    collect_hex(hex_pairs(String.to_list(text)))
311
312def aes_nat_eq_step(+a: Nat, +b: Nat,
313                    result: Maybe<&0, {a == b : Nat}>) -> Maybe<&0, {1n+a == 1n+b : Nat}>:
314    match result:
315        case None{}: None{}
316        case Some{proof}: Some{Equal.cong(Nat, Nat, n => 1n+n, a, b, proof)}
317
318def aes_nat_eq_proof(+a: Nat, +b: Nat) -> Maybe<&0, {a == b : Nat}>:
319    match a b:
320        case 0n 0n: Some{{==}}
321        case 0n 1n+p: None{}
322        case 1n+p 0n: None{}
323        case 1n+pa 1n+pb: aes_nat_eq_step(pa, pb, aes_nat_eq_proof(pa, pb))
324
325def aes_bool_true_proof(+x: U32, b: Bool,
326                        link: {b == U32.is_lt(x, 256) : Bool}) -> Maybe<&0, {U32.is_lt(x, 256) == True{} : Bool}>:
327    match b:
328        case False{}: None{}
329        case True{}:
330            Some{Equal.trans(Bool, U32.is_lt(x, 256), b, True{},
331                Equal.sym(Bool, b, U32.is_lt(x, 256), link), {==})}
332
333def aes_bytes_valid_cons_proof(x: U32, tail: List<&2, U32>,
334    head_proof: Maybe<&0, {U32.is_lt(x, 256) == True{} : Bool}>,
335    tail_proof: Maybe<&0, {bytes_valid(tail) == True{} : Bool}>) ->
336    Maybe<&0, {bytes_valid(x <> tail) == True{} : Bool}>:
337    match head_proof tail_proof:
338        case None{} _: None{}
339        case _ None{}: None{}
340        case Some{hp} Some{tp}:
341            Some{Equal.trans(Bool, Bool.and(U32.is_lt(x, 256), bytes_valid(tail)),
342                Bool.and(True{}, bytes_valid(tail)), True{},
343                Equal.cong(Bool, Bool, b => Bool.and(b, bytes_valid(tail)),
344                    U32.is_lt(x, 256), True{}, hp),
345                Equal.trans(Bool, Bool.and(True{}, bytes_valid(tail)),
346                    bytes_valid(tail), True{}, {==}, tp))}
347
348def aes_bytes_valid_from_bool(+bytes: List<&2, U32>, b: Bool,
349    link: {b == bytes_valid(bytes) : Bool}) ->
350    Maybe<&0, {bytes_valid(bytes) == True{} : Bool}>:
351    match b:
352        case False{}: None{}
353        case True{}:
354            Some{Equal.sym(Bool, True{}, bytes_valid(bytes), link)}
355
356def aes_bytes_valid_proof(+bytes: List<&2, U32>) ->
357    Maybe<&0, {bytes_valid(bytes) == True{} : Bool}>:
358    aes_bytes_valid_from_bool(bytes, bytes_valid(bytes), {==})
359
360def key_checked(bytes: List<&2, U32>, -size: {List.length(&2, U32, bytes) == 32n : Nat},
361                -valid: {bytes_valid(bytes) == True{} : Bool}) -> Result<&2, &2, Error, SecretKey>:
362    Done{SecretKey{bytes, size, valid}}
363
364def key_from_proofs(+bytes: List<&2, U32>,
365    size: Maybe<&0, {List.length(&2, U32, bytes) == 32n : Nat}>,
366    valid: Maybe<&0, {bytes_valid(bytes) == True{} : Bool}>) -> Result<&2, &2, Error, SecretKey>:
367    match size valid:
368        case Some{size} Some{valid}: Done{SecretKey{bytes, size, valid}}
369        case _ _: Fail{InvalidKey{}}
370
371def key_impl(+bytes: List<&2, U32>) -> Result<&2, &2, Error, SecretKey>:
372    key_from_proofs(bytes, aes_nat_eq_proof(List.length(&2, U32, bytes), 32n),
373        aes_bytes_valid_proof(bytes))
374
375def nonce_checked(bytes: List<&2, U32>, size: {List.length(&2, U32, bytes) == 12n : Nat},
376                  valid: {bytes_valid(bytes) == True{} : Bool}) -> Result<&2, &2, Error, Nonce>:
377    Done{Nonce{bytes, size, valid}}
378
379def nonce_from_proofs(+bytes: List<&2, U32>,
380    size: Maybe<&0, {List.length(&2, U32, bytes) == 12n : Nat}>,
381    valid: Maybe<&0, {bytes_valid(bytes) == True{} : Bool}>) -> Result<&2, &2, Error, Nonce>:
382    match size valid:
383        case Some{size} Some{valid}: Done{Nonce{bytes, size, valid}}
384        case _ _: Fail{InvalidNonce{}}
385
386def nonce_impl(+bytes: List<&2, U32>) -> Result<&2, &2, Error, Nonce>:
387    nonce_from_proofs(bytes, aes_nat_eq_proof(List.length(&2, U32, bytes), 12n),
388        aes_bytes_valid_proof(bytes))
389
390def secret_key_bytes(key: SecretKey) -> List<&2, U32>:
391    match key:
392        case SecretKey{bytes, size, valid}: bytes
393
394def raw_nonce_bytes(nonce: Nonce) -> List<&2, U32>:
395    match nonce:
396        case Nonce{bytes, size, valid}: bytes
397
398def tag_from_proofs(bytes: List<&2, U32>,
399    size: Maybe<&0, {List.length(&2, U32, bytes) == 16n : Nat}>,
400    valid: Maybe<&0, {bytes_valid(bytes) == True{} : Bool}>) -> Maybe<&2, Tag>:
401    match size valid:
402        case Some{size} Some{valid}: Some{Tag{bytes, size, valid}}
403        case _ _: None{}
404
405def envelope_from_proofs(nonce: Nonce, +ciphertext: List<&2, U32>, tag: Tag,
406    valid: Maybe<&0, {bytes_valid(ciphertext) == True{} : Bool}>) -> Maybe<&2, Envelope>:
407    match valid:
408        case Some{valid}: Some{Envelope{nonce, ciphertext, tag, valid}}
409        case None{}: None{}
410
411def envelope_from_tag_proof(nonce: Nonce, +ciphertext: List<&2, U32>, tag_bytes: List<&2, U32>,
412    tag: Maybe<&2, Tag>, valid: Maybe<&0, {bytes_valid(ciphertext) == True{} : Bool}>) -> Maybe<&2, Envelope>:
413    match tag:
414        case None{}: None{}
415        case Some{tag}: envelope_from_proofs(nonce, ciphertext, tag, valid)
416
417def envelope_from_gcm(nonce: Nonce, output: Core.GcmOutput) -> Maybe<&2, Envelope>:
418    match output:
419        case Core.GcmOutput{+ciphertext, ciphertext_valid,
420            +tag_bytes, tag_valid, tag_size, tag_words, tag_nonce, tag_aad,
421            tag_matches}:
422            Some{Envelope{nonce, ciphertext,
423                Tag{tag_bytes, tag_size, core_bytes_valid_proof(tag_bytes, tag_valid)},
424                core_bytes_valid_proof(ciphertext, ciphertext_valid)}}
425
426def envelope_from_gcm_checked(nonce: Nonce, output: Core.GcmOutput) -> Envelope:
427    match output:
428        case Core.GcmOutput{+ciphertext, ciphertext_valid,
429            +tag_bytes, tag_valid, tag_size, tag_words, tag_nonce, tag_aad,
430            tag_matches}:
431            Envelope{nonce, ciphertext,
432                Tag{tag_bytes, tag_size, core_bytes_valid_proof(tag_bytes, tag_valid)},
433                core_bytes_valid_proof(ciphertext, ciphertext_valid)}
434
435def encrypt_output(nonce: Nonce, maybe_envelope: Maybe<&2, Envelope>) -> Result<&2, &2, Error, Envelope>:
436    match maybe_envelope:
437        case Some{envelope}: Done{envelope}
438        case None{}: Fail{InvalidBytes{}}
439
440def encrypt_output_from_gcm(+nonce: Nonce, output: Core.GcmOutput) ->
441    Result<&2, &2, Error, Envelope>:
442    Done{envelope_from_gcm_checked(nonce, output)}
443
444def encrypt_valid_output(key: SecretKey, +nonce: Nonce,
445                         aad: List<&2, U32>, plaintext: List<&2, U32>) ->
446    Core.GcmOutput:
447    Core.gcm_encrypt_raw(secret_key_bytes(key), raw_nonce_bytes(nonce), aad, plaintext)
448
449def encrypt_valid(key: SecretKey, +nonce: Nonce, aad: List<&2, U32>,
450                  plaintext: List<&2, U32>) -> Result<&2, &2, Error, Envelope>:
451    encrypt_output_from_gcm(nonce,
452        encrypt_valid_output(key, nonce, aad, plaintext))
453
454def encrypt_checked(key: SecretKey, nonce: Nonce, aad: List<&2, U32>,
455                    plaintext: List<&2, U32>, aad_ok: Bool, plaintext_ok: Bool) -> Result<&2, &2, Error, Envelope>:
456    match aad_ok plaintext_ok:
457        case True{} True{}: encrypt_valid(key, nonce, aad, plaintext)
458        case _ _: Fail{InvalidBytes{}}
459
460def encrypt_impl(key: SecretKey, nonce: Nonce, +aad: List<&2, U32>,
461            +plaintext: List<&2, U32>) -> Result<&2, &2, Error, Envelope>:
462    encrypt_checked(key, nonce, aad, plaintext, aad_valid(aad), plaintext_valid(plaintext))
463
464def bytes_difference.go(a: List<&2, U32>, b: List<&2, U32>, +difference: U32) -> U32:
465    match a b:
466        case Nil{} Nil{}: difference
467        case x <> xs y <> ys:
468            bytes_difference.go(xs, ys, U32.or(difference, U32.xor(x, y)))
469        case _ _: 1
470
471def bytes_equal_full_scan(a: List<&2, U32>, b: List<&2, U32>) -> Bool:
472    U32.is_eq(bytes_difference.go(a, b, 0), 0)
473
474def decrypt_payload(words: List<&2, U32>, envelope: Envelope) -> Result<&2, &2, Error, List<&2, U32>>:
475    match envelope:
476        case Envelope{nonce, ciphertext, tag, valid}:
477            Done{Core.gcm_decrypt_expanded(words, raw_nonce_bytes(nonce), ciphertext)}
478
479def decrypt_auth_result(words: List<&2, U32>, envelope: Envelope, authenticated: Bool) -> Result<&2, &2, Error, List<&2, U32>>:
480    match authenticated:
481        case False{}: Fail{AuthenticationFailed{}}
482        case True{}: decrypt_payload(words, envelope)
483
484def decrypt_authenticated_tag(+words: List<&2, U32>,
485    +nonce: List<&2, U32>, +aad: List<&2, U32>,
486    +ciphertext: List<&2, U32>, +envelope: Envelope, tag: Tag) ->
487    Result<&2, &2, Error, List<&2, U32>>:
488    match tag:
489        case Tag{tag_bytes, size, valid}:
490            authenticated = bytes_equal_full_scan(tag_bytes,
491                Core.gcm_tag_bytes(Core.gcm_tag_output(words, nonce, aad,
492                    ciphertext)))
493            decrypt_auth_result(words, envelope, authenticated)
494
495def decrypt_authenticated(key: SecretKey, +aad: List<&2, U32>, +envelope: Envelope) -> Result<&2, &2, Error, List<&2, U32>>:
496    match key envelope:
497        case SecretKey{+key_bytes, _, _} Envelope{nonce, ciphertext, +tag, _}:
498            +words = Core.aes256_expand(key_bytes)
499            decrypt_authenticated_tag(words, raw_nonce_bytes(nonce), aad,
500                ciphertext, envelope, tag)
501
502def decrypt_checked(+key: SecretKey, aad: List<&2, U32>, +envelope: Envelope,
503                    aad_ok: Bool, ciphertext_ok: Bool) -> Result<&2, &2, Error, List<&2, U32>>:
504    match aad_ok ciphertext_ok:
505        case False{} _: Fail{InvalidBytes{}}
506        case True{} False{}: Fail{InvalidBytes{}}
507        case True{} True{}: decrypt_authenticated(key, aad, envelope)
508
509def decrypt_impl(key: SecretKey, +aad: List<&2, U32>, +envelope: Envelope) -> Result<&2, &2, Error, List<&2, U32>>:
510    decrypt_checked(key, aad, envelope, aad_valid(aad), plaintext_valid(ciphertext(envelope)))
511
512def parse_decoded(+nonce_bytes: List<&2, U32>, +tag_bytes: List<&2, U32>, +ciphertext: List<&2, U32>,
513    nonce_size: Maybe<&0, {List.length(&2, U32, nonce_bytes) == 12n : Nat}>,
514    tag_size: Maybe<&0, {List.length(&2, U32, tag_bytes) == 16n : Nat}>,
515    nonce_valid: Maybe<&0, {bytes_valid(nonce_bytes) == True{} : Bool}>,
516    tag_valid: Maybe<&0, {bytes_valid(tag_bytes) == True{} : Bool}>,
517    ciphertext_valid: Maybe<&0, {bytes_valid(ciphertext) == True{} : Bool}>) -> Result<&2, &2, Error, Envelope>:
518    match nonce_size tag_size nonce_valid tag_valid ciphertext_valid:
519        case Some{ns} Some{ts} Some{nv} Some{tv} Some{cv}:
520            Done{Envelope{Nonce{nonce_bytes, ns, nv}, ciphertext, Tag{tag_bytes, ts, tv}, cv}}
521        case _ _ _ _ _: Fail{InvalidEnvelope{}}
522
523def parse_decoded_hex(nonce: Maybe<&2, List<&2, U32>>, tag: Maybe<&2, List<&2, U32>>,
524    ciphertext: Maybe<&2, List<&2, U32>>) -> Result<&2, &2, Error, Envelope>:
525    match nonce tag ciphertext:
526        case Some{+n} Some{+t} Some{+c}:
527            parse_decoded(n, t, c, aes_nat_eq_proof(List.length(&2, U32, n), 12n),
528                aes_nat_eq_proof(List.length(&2, U32, t), 16n), aes_bytes_valid_proof(n),
529                aes_bytes_valid_proof(t), aes_bytes_valid_proof(c))
530        case _ _ _: Fail{InvalidEnvelope{}}
531
532def parse_version_fields(fields: List<&2, String>) -> Result<&2, &2, Error, Envelope>:
533    match fields:
534        case version <> nonce_text <> tag_text <> ciphertext_text <> Nil{}:
535            parse_decoded_hex(decode_hex(nonce_text), decode_hex(tag_text), decode_hex(ciphertext_text))
536        case _: Fail{InvalidEnvelope{}}
537
538def parse_version(fields: List<&2, String>, valid_version: Bool) -> Result<&2, &2, Error, Envelope>:
539    match valid_version:
540        case False{}: Fail{InvalidEnvelope{}}
541        case True{}: parse_version_fields(fields)
542
543def parse_string_cmp_is_eq(result: ((String & String) & Cmp)) -> Bool:
544    match result:
545        case ((_, _), EQ{}): True{}
546        case ((_, _), _): False{}
547
548def parse_fields(fields: List<&2, String>) -> Result<&2, &2, Error, Envelope>:
549    match fields:
550        case +version <> rest:
551            parse_version(fields, parse_string_cmp_is_eq(String.cmp(version, "v1")))
552        case Nil{}: Fail{InvalidEnvelope{}}
553
554def parse_canonical_decision(text: String, envelope: Envelope,
555    canonical: Bool) -> Result<&2, &2, Error, Envelope>:
556    match canonical:
557        case True{}: Done{envelope}
558        case False{}: Fail{InvalidEnvelope{}}
559
560def parse_canonical(+text: String,
561    result: Result<&2, &2, Error, Envelope>) ->
562    Result<&2, &2, Error, Envelope>:
563    match result:
564        case Fail{error}: Fail{error}
565        case Done{+envelope}:
566            parse_canonical_decision(text, envelope,
567                String.eq(encode_impl(envelope), text))
568
569def parse_impl(+text: String) -> Result<&2, &2, Error, Envelope>:
570    parse_canonical(text, parse_fields(String.split(text, '.')))
571
572def key(bytes):
573    key_impl(bytes)
574
575def nonce(bytes):
576    nonce_impl(bytes)
577
578def encrypt(key, nonce, aad, plaintext):
579    encrypt_impl(key, nonce, aad, plaintext)
580
581def decrypt(key, aad, envelope):
582    decrypt_impl(key, aad, envelope)
583
584def encode(envelope):
585    encode_impl(envelope)
586
587def parse(text):
588    parse_impl(text)