LAWS.bend

qasim-bend-kit@0.1.0.2 · 621 lines · 97 definitions

1# Library correctness laws and integration obligations.

2
3import Base
4
5# JSON contract: libs/JSON.bend.

6#

7# Expected API:

8#   Json.parse(text: String) -> Result<&1, &1, Json.Error, Json.Value>

9#   Json.stringify(value: Json.Value) -> String

10
11import qasim-bend-kit@0.1.0.2/libs/JSON.bend as Json
12import qasim-bend-kit@0.1.0.2/libs/URL.bend as URL
13import qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend as AES
14
15# ============================================================

16# JSON: Core correctness

17# ============================================================

18
19law stringify_parse_roundtrip:
20    for value: Json.Value {
21        Json.parse(Json.stringify(value))
22        ==
23        Done{value}
24        :
25        Result<&1, &1, Json.Error, Json.Value>
26    }
27
28# ============================================================

29# JSON: Literals

30# ============================================================

31
32law parses_null:
33    { Json.parse("null") == Done{Json.Null{}} :
34        Result<&1, &1, Json.Error, Json.Value> }
35
36law parses_true:
37    { Json.parse("true") == Done{Json.Bool{True{}}} :
38        Result<&1, &1, Json.Error, Json.Value> }
39
40law parses_false:
41    { Json.parse("false") == Done{Json.Bool{False{}}} :
42        Result<&1, &1, Json.Error, Json.Value> }
43
44# ============================================================

45# JSON: Whitespace

46# ============================================================

47
48law accepts_leading_space:
49    for value: Json.Value {
50        Json.parse(" " ++ Json.stringify(value)) == Done{value} :
51        Result<&1, &1, Json.Error, Json.Value>
52    }
53
54law accepts_trailing_space:
55    for value: Json.Value {
56        Json.parse(Json.stringify(value) ++ " ") == Done{value} :
57        Result<&1, &1, Json.Error, Json.Value>
58    }
59
60law accepts_surrounding_space:
61    for value: Json.Value {
62        Json.parse(" \n\t\r" ++ Json.stringify(value) ++ "\r\t\n ") == Done{value} :
63        Result<&1, &1, Json.Error, Json.Value>
64    }
65
66# ============================================================

67# JSON: Invalid and incomplete input

68# ============================================================

69
70law rejects_trailing_garbage:
71    { Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse("nullx"))
72        == True{} : Bool }
73
74law rejects_second_value:
75    { Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse("null true"))
76        == True{} : Bool }
77
78law rejects_invalid_null:
79    { Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse("nul"))
80        == True{} : Bool }
81
82law rejects_invalid_true:
83    { Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse("tru"))
84        == True{} : Bool }
85
86law rejects_invalid_false:
87    { Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse("fals"))
88        == True{} : Bool }
89
90law rejects_empty_input:
91    { Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse(""))
92        == True{} : Bool }
93
94law rejects_whitespace_only:
95    { Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse(" \t\r\n "))
96        == True{} : Bool }
97
98# ============================================================

99# JSON: Strings

100# ============================================================

101
102law parses_empty_string:
103    { Json.parse("\"\"") == Done{Json.Str{""}} :
104        Result<&1, &1, Json.Error, Json.Value> }
105
106law parses_simple_string:
107    { Json.parse("\"hello\"") == Done{Json.Str{"hello"}} :
108        Result<&1, &1, Json.Error, Json.Value> }
109
110law parses_newline_escape:
111    { Json.parse("\"a\\nb\"") == Done{Json.Str{"a\nb"}} :
112        Result<&1, &1, Json.Error, Json.Value> }
113
114law parses_quote_escape:
115    { Json.parse("\"a\\\"b\"") == Done{Json.Str{"a\"b"}} :
116        Result<&1, &1, Json.Error, Json.Value> }
117
118law parses_backslash_escape:
119    { Json.parse("\"a\\\\b\"") == Done{Json.Str{"a\\b"}} :
120        Result<&1, &1, Json.Error, Json.Value> }
121
122law rejects_unterminated_string:
123    { Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse("\"hello"))
124        == True{} : Bool }
125
126# ============================================================

127# JSON: Arrays

128# ============================================================

129
130law parses_empty_array:
131    { Json.parse("[]") == Done{Json.Arr{Nil{}}} :
132        Result<&1, &1, Json.Error, Json.Value> }
133
134law parses_literal_array:
135    {
136        Json.parse("[null,true,false]")
137        ==
138        Done{Json.Arr{
139            Json.Null{} <>
140            Json.Bool{True{}} <>
141            Json.Bool{False{}} <>
142            Nil{}
143        }}
144        :
145        Result<&1, &1, Json.Error, Json.Value>
146    }
147
148law rejects_array_trailing_comma:
149    { Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse("[null,]"))
150        == True{} : Bool }
151
152# ============================================================

153# JSON: Objects

154# ============================================================

155
156law parses_empty_object:
157    { Json.parse("{}") == Done{Json.Obj{Nil{}}} :
158        Result<&1, &1, Json.Error, Json.Value> }
159
160law rejects_unquoted_object_key:
161    { Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse("{foo:null}"))
162        == True{} : Bool }
163
164law rejects_object_trailing_comma:
165    { Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse("{\"x\":null,}"))
166        == True{} : Bool }
167
168# ============================================================

169# JSON: Nesting

170# ============================================================

171
172law parses_nested_containers:
173    {
174        Json.parse("[{\"x\":[true,null]}]")
175        ==
176        Done{Json.Arr{
177            Json.Obj{
178                ("x", Json.Arr{
179                    Json.Bool{True{}} <>
180                    Json.Null{} <>
181                    Nil{}
182                }) <>
183                Nil{}
184            } <>
185            Nil{}
186        }}
187        :
188        Result<&1, &1, Json.Error, Json.Value>
189    }
190
191# ============================================================

192# JSON: Additional semantics

193# ============================================================

194
195# JSON permits only space, tab, carriage return and line feed as whitespace.

196law rejects_non_json_whitespace:
197    { Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse("\u{000b}null"))
198        == True{} : Bool }
199
200# A raw control character is forbidden inside a JSON string.

201law rejects_raw_string_control:
202    { Result.is_fail(&1, &1, Json.Error, Json.Value,
203            Json.parse("\"" ++ "\u{0001}" ++ "\""))
204        == True{} : Bool }
205
206# Unicode escapes decode to their scalar value, including a surrogate pair.

207law parses_unicode_escape:
208    { Json.parse("\"\\u263A\"") == Done{Json.Str{"\u{263a}"}} :
209        Result<&1, &1, Json.Error, Json.Value> }
210
211law parses_unicode_surrogate_pair:
212    { Json.parse("\"\\uD83D\\uDE00\"") == Done{Json.Str{"\u{1f600}"}} :
213        Result<&1, &1, Json.Error, Json.Value> }
214
215# This representative decimal/exponent form is accepted. A separate law below

216# checks that the smart number constructor preserves the original lexeme.

217law parses_fraction_and_exponent:
218    { Result.is_done(&1, &1, Json.Error, Json.Value, Json.parse("-12.50e+3"))
219        == True{} : Bool }
220
221law rejects_malformed_number_forms:
222    { Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse("01"))
223        && Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse("1."))
224        && Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse("1e+"))
225        == True{} : Bool }
226
227# Arrays retain source order. Objects retain source order and duplicate keys;

228# consumers that need map semantics must choose their own duplicate-key policy.

229law preserves_array_order:
230    { Json.parse("[3,1,2]") == Done{Json.Arr{
231            Json.Number{"3", Json.Certified{Json.number_proof("3", {==})}} <>
232            Json.Number{"1", Json.Certified{Json.number_proof("1", {==})}} <>
233            Json.Number{"2", Json.Certified{Json.number_proof("2", {==})}} <>
234            Nil{}
235        }} : Result<&1, &1, Json.Error, Json.Value> }
236
237law preserves_object_order_and_duplicates:
238    { Json.parse("{\"x\":1,\"x\":2}") == Done{Json.Obj{
239            ("x", Json.Number{"1", Json.Certified{Json.number_proof("1", {==})}}) <>
240            ("x", Json.Number{"2", Json.Certified{Json.number_proof("2", {==})}}) <>
241            Nil{}
242        }} : Result<&1, &1, Json.Error, Json.Value> }
243
244# GPU entry points have the same specified results as their CPU counterparts.

245law gpu_single_matches_cpu:
246    for text: String {
247        Json.parse_gpu(text) == Json.parse(text) :
248        Result<&1, &1, Json.Error, Json.Value>
249    }
250
251law preserves_number_lexeme:
252    { Json.number("-12.50e+3") == Done{Json.Number{
253            "-12.50e+3",
254            Json.Certified{Json.number_proof("-12.50e+3", {==})}
255        }} : Result<&1, &1, Json.Error, Json.Value> }
256
257law gpu_batch_matches_cpu:
258    for batch: Json.Batch {
259        Json.parse_batch_gpu(batch) == Json.parse_batch(batch) : Json.BatchResult
260    }
261
262# ============================================================

263# URL component encoding

264# ============================================================

265
266# Encode each UTF-8 byte with an uppercase percent escape.

267law url_component_ascii:
268    { URL.percent_component("A") == "%41" : String }
269
270law url_component_reserved:
271    { URL.percent_component("/") == "%2F" : String }
272
273law url_component_utf8:
274    { URL.percent_component(SCon{Chr{233}, SNil{}}) == "%C3%A9" : String }
275
276
277# ============================================================

278# AES-256-GCM: validated keys and nonces

279# ============================================================

280
281law aes256gcm_accepts_32_byte_key:
282    for +bytes: List<&2, U32>
283    for size: {List.length(&2, U32, bytes) == 32n : Nat}
284    for valid: {AES.bytes_valid(bytes) == True{} : Bool}
285    {AES.key(bytes) == Done{AES.SecretKey{bytes, size, valid}} :
286        Result<&2, &2, AES.Error, AES.SecretKey>}
287
288law aes256gcm_rejects_wrong_key_length:
289    for +bytes: List<&2, U32>
290    for size: {List.length(&2, U32, bytes) != 32n : Nat}
291    {AES.key(bytes) == Fail{AES.InvalidKey{}} :
292        Result<&2, &2, AES.Error, AES.SecretKey>}
293
294law aes256gcm_rejects_non_byte_key:
295    for +bytes: List<&2, U32>
296    for valid: {AES.bytes_valid(bytes) == False{} : Bool}
297    {AES.key(bytes) == Fail{AES.InvalidKey{}} :
298        Result<&2, &2, AES.Error, AES.SecretKey>}
299
300law aes256gcm_accepts_12_byte_nonce:
301    for +bytes: List<&2, U32>
302    for size: {List.length(&2, U32, bytes) == 12n : Nat}
303    for valid: {AES.bytes_valid(bytes) == True{} : Bool}
304    {AES.nonce(bytes) == Done{AES.Nonce{bytes, size, valid}} :
305        Result<&2, &2, AES.Error, AES.Nonce>}
306
307law aes256gcm_rejects_wrong_nonce_length:
308    for +bytes: List<&2, U32>
309    for size: {List.length(&2, U32, bytes) != 12n : Nat}
310    {AES.nonce(bytes) == Fail{AES.InvalidNonce{}} :
311        Result<&2, &2, AES.Error, AES.Nonce>}
312
313law aes256gcm_rejects_non_byte_nonce:
314    for +bytes: List<&2, U32>
315    for valid: {AES.bytes_valid(bytes) == False{} : Bool}
316    {AES.nonce(bytes) == Fail{AES.InvalidNonce{}} :
317        Result<&2, &2, AES.Error, AES.Nonce>}
318
319# ============================================================

320# AES-256-GCM: encryption and authenticated decryption

321# ============================================================

322
323# This prevents satisfying the conditional roundtrip by always failing.

324law aes256gcm_encrypts_valid_input:
325    for key: AES.SecretKey
326    for nonce: AES.Nonce
327    for aad: List<&2, U32>
328    for plaintext: List<&2, U32>
329    for aad_ok: {AES.aad_valid(aad) == True{} : Bool}
330    for plaintext_ok: {AES.plaintext_valid(plaintext) == True{} : Bool}
331    {Result.is_done(&2, &2, AES.Error, AES.Envelope,
332        AES.encrypt(key, nonce, aad, plaintext)) == True{} : Bool}
333
334law aes256gcm_rejects_invalid_plaintext:
335    for +key: AES.SecretKey
336    for +nonce: AES.Nonce
337    for +aad: List<&2, U32>
338    for +plaintext: List<&2, U32>
339    for valid: {AES.plaintext_valid(plaintext) == False{} : Bool}
340    {AES.encrypt(key, nonce, aad, plaintext) == Fail{AES.InvalidBytes{}} :
341        Result<&2, &2, AES.Error, AES.Envelope>}
342
343law aes256gcm_rejects_invalid_aad:
344    for +key: AES.SecretKey
345    for +nonce: AES.Nonce
346    for +aad: List<&2, U32>
347    for +plaintext: List<&2, U32>
348    for valid: {AES.aad_valid(aad) == False{} : Bool}
349    {AES.encrypt(key, nonce, aad, plaintext) == Fail{AES.InvalidBytes{}} :
350        Result<&2, &2, AES.Error, AES.Envelope>}
351
352law aes256gcm_decrypt_rejects_invalid_aad:
353    for +key: AES.SecretKey
354    for +aad: List<&2, U32>
355    for +envelope: AES.Envelope
356    for valid: {AES.aad_valid(aad) == False{} : Bool}
357    {AES.decrypt(key, aad, envelope) == Fail{AES.InvalidBytes{}} :
358        Result<&2, &2, AES.Error, List<&2, U32>>}
359
360law aes256gcm_roundtrip:
361    for +key: AES.SecretKey
362    for +nonce: AES.Nonce
363    for +aad: List<&2, U32>
364    for +plaintext: List<&2, U32>
365    for +envelope: AES.Envelope
366    for encrypted: {AES.encrypt(key, nonce, aad, plaintext) == Done{envelope} :
367        Result<&2, &2, AES.Error, AES.Envelope>}
368    {AES.decrypt(key, aad, envelope) == Done{plaintext} :
369        Result<&2, &2, AES.Error, List<&2, U32>>}
370
371law aes256gcm_preserves_nonce:
372    for +key: AES.SecretKey
373    for +nonce: AES.Nonce
374    for +aad: List<&2, U32>
375    for +plaintext: List<&2, U32>
376    for +envelope: AES.Envelope
377    for encrypted: {AES.encrypt(key, nonce, aad, plaintext) == Done{envelope} :
378        Result<&2, &2, AES.Error, AES.Envelope>}
379    {AES.envelope_nonce(envelope) == nonce : AES.Nonce}
380
381law aes256gcm_preserves_plaintext_length:
382    for +key: AES.SecretKey
383    for +nonce: AES.Nonce
384    for +aad: List<&2, U32>
385    for +plaintext: List<&2, U32>
386    for +envelope: AES.Envelope
387    for encrypted: {AES.encrypt(key, nonce, aad, plaintext) == Done{envelope} :
388        Result<&2, &2, AES.Error, AES.Envelope>}
389    {List.length(&2, U32, AES.ciphertext(envelope)) ==
390        List.length(&2, U32, plaintext) : Nat}
391
392# For fixed key, nonce, AAD, and ciphertext there is exactly one valid tag.

393# Different ciphertext/AAD/key/nonce can collide in a finite tag space; do not

394# claim that every possible change to those fields is mathematically rejected.

395law aes256gcm_rejects_changed_tag:
396    for +key: AES.SecretKey
397    for +nonce: AES.Nonce
398    for +aad: List<&2, U32>
399    for +plaintext: List<&2, U32>
400    for +envelope: AES.Envelope
401    for +tampered: AES.Envelope
402    for encrypted: {AES.encrypt(key, nonce, aad, plaintext) == Done{envelope} :
403        Result<&2, &2, AES.Error, AES.Envelope>}
404    for same_nonce: {AES.envelope_nonce(tampered) ==
405        AES.envelope_nonce(envelope) : AES.Nonce}
406    for same_ciphertext: {AES.ciphertext(tampered) ==
407        AES.ciphertext(envelope) : List<&2, U32>}
408    for changed_tag: {AES.tag_bytes(AES.envelope_tag(tampered)) !=
409        AES.tag_bytes(AES.envelope_tag(envelope)) : List<&2, U32>}
410    {AES.decrypt(key, aad, tampered) == Fail{AES.AuthenticationFailed{}} :
411        Result<&2, &2, AES.Error, List<&2, U32>>}
412
413# ============================================================

414# AES-256-GCM: strict, canonical versioned envelope

415# ============================================================

416
417law aes256gcm_envelope_roundtrip:
418    for +envelope: AES.Envelope
419    {AES.parse(AES.encode(envelope)) == Done{envelope} :
420        Result<&2, &2, AES.Error, AES.Envelope>}
421
422law aes256gcm_envelope_is_canonical:
423    for +text: String
424    for +envelope: AES.Envelope
425    for parsed: {AES.parse(text) == Done{envelope} :
426        Result<&2, &2, AES.Error, AES.Envelope>}
427    {AES.encode(envelope) == text : String}
428
429law aes256gcm_rejects_empty_envelope:
430    {AES.parse("") == Fail{AES.InvalidEnvelope{}} :
431        Result<&2, &2, AES.Error, AES.Envelope>}
432
433law aes256gcm_rejects_unknown_version:
434    {AES.parse("v2.cafebabefacedbaddecaf888.fd2caa16a5832e76aa132c1453eeda7e.") == Fail{AES.InvalidEnvelope{}} :
435        Result<&2, &2, AES.Error, AES.Envelope>}
436
437law aes256gcm_rejects_missing_version:
438    {AES.parse("cafebabefacedbaddecaf888.fd2caa16a5832e76aa132c1453eeda7e.") == Fail{AES.InvalidEnvelope{}} :
439        Result<&2, &2, AES.Error, AES.Envelope>}
440
441law aes256gcm_rejects_short_nonce:
442    {AES.parse("v1.cafebabefacedbaddecaf8.fd2caa16a5832e76aa132c1453eeda7e.") == Fail{AES.InvalidEnvelope{}} :
443        Result<&2, &2, AES.Error, AES.Envelope>}
444
445law aes256gcm_rejects_long_nonce:
446    {AES.parse("v1.cafebabefacedbaddecaf88800.fd2caa16a5832e76aa132c1453eeda7e.") == Fail{AES.InvalidEnvelope{}} :
447        Result<&2, &2, AES.Error, AES.Envelope>}
448
449law aes256gcm_rejects_short_tag:
450    {AES.parse("v1.cafebabefacedbaddecaf888.fd2caa16a5832e76aa132c1453eeda.") == Fail{AES.InvalidEnvelope{}} :
451        Result<&2, &2, AES.Error, AES.Envelope>}
452
453law aes256gcm_rejects_long_tag:
454    {AES.parse("v1.cafebabefacedbaddecaf888.fd2caa16a5832e76aa132c1453eeda7e00.") == Fail{AES.InvalidEnvelope{}} :
455        Result<&2, &2, AES.Error, AES.Envelope>}
456
457law aes256gcm_rejects_odd_ciphertext_hex:
458    {AES.parse("v1.cafebabefacedbaddecaf888.fd2caa16a5832e76aa132c1453eeda7e.0") == Fail{AES.InvalidEnvelope{}} :
459        Result<&2, &2, AES.Error, AES.Envelope>}
460
461law aes256gcm_rejects_non_hex_ciphertext:
462    {AES.parse("v1.cafebabefacedbaddecaf888.fd2caa16a5832e76aa132c1453eeda7e.gg") == Fail{AES.InvalidEnvelope{}} :
463        Result<&2, &2, AES.Error, AES.Envelope>}
464
465law aes256gcm_rejects_non_hex_nonce:
466    {AES.parse("v1.zzfebabefacedbaddecaf888.fd2caa16a5832e76aa132c1453eeda7e.") == Fail{AES.InvalidEnvelope{}} :
467        Result<&2, &2, AES.Error, AES.Envelope>}
468
469law aes256gcm_rejects_non_hex_tag:
470    {AES.parse("v1.cafebabefacedbaddecaf888.zz2caa16a5832e76aa132c1453eeda7e.") == Fail{AES.InvalidEnvelope{}} :
471        Result<&2, &2, AES.Error, AES.Envelope>}
472
473law aes256gcm_rejects_uppercase_hex:
474    {AES.parse("v1.CAFEBABEFACEDBADDECAF888.fd2caa16a5832e76aa132c1453eeda7e.") == Fail{AES.InvalidEnvelope{}} :
475        Result<&2, &2, AES.Error, AES.Envelope>}
476
477law aes256gcm_rejects_extra_field:
478    {AES.parse("v1.cafebabefacedbaddecaf888.fd2caa16a5832e76aa132c1453eeda7e..") == Fail{AES.InvalidEnvelope{}} :
479        Result<&2, &2, AES.Error, AES.Envelope>}
480
481law aes256gcm_rejects_missing_ciphertext_field:
482    {AES.parse("v1.cafebabefacedbaddecaf888.fd2caa16a5832e76aa132c1453eeda7e") == Fail{AES.InvalidEnvelope{}} :
483        Result<&2, &2, AES.Error, AES.Envelope>}
484
485law aes256gcm_rejects_trailing_garbage:
486    {AES.parse("v1.cafebabefacedbaddecaf888.fd2caa16a5832e76aa132c1453eeda7e.00!") == Fail{AES.InvalidEnvelope{}} :
487        Result<&2, &2, AES.Error, AES.Envelope>}
488
489law aes256gcm_rejects_surrounding_whitespace:
490    {AES.parse(" v1.cafebabefacedbaddecaf888.fd2caa16a5832e76aa132c1453eeda7e. ") == Fail{AES.InvalidEnvelope{}} :
491        Result<&2, &2, AES.Error, AES.Envelope>}
492
493# ============================================================

494# AES-256-GCM: NIST known-answer laws (not roundtrip-only tests)

495# ============================================================

496# Source: NIST AES_GCM.pdf, GCM-AES256 examples 1-5 (pages 21-28).

497# https://csrc.nist.gov/CSRC/media/Projects/Cryptographic-Standards-and-Guidelines/documents/examples/AES_GCM.pdf

498# These are public test fixtures, never production keys/nonces.

499
500def aes256gcm_nist_key() -> AES.SecretKey:
501    AES.SecretKey{[254, 255, 233, 146, 134, 101, 115, 28, 109, 106, 143, 148, 103, 48, 131, 8, 254, 255, 233, 146, 134, 101, 115, 28, 109, 106, 143, 148, 103, 48, 131, 8], {==}, {==}}
502
503def aes256gcm_nist_nonce() -> AES.Nonce:
504    AES.Nonce{[202, 254, 186, 190, 250, 206, 219, 173, 222, 202, 248, 136], {==}, {==}}
505
506def aes256gcm_nist_empty() -> AES.Envelope:
507    AES.Envelope{aes256gcm_nist_nonce(), [],
508        AES.Tag{[253, 44, 170, 22, 165, 131, 46, 118, 170, 19, 44, 20, 83, 238, 218, 126], {==}, {==}}, {==}}
509
510# Compare the protocol-visible result while leaving internal certificate terms
511# out of the NIST contract: success, nonce bytes, ciphertext, and tag bytes.
512def aes256gcm_nist_encrypt_observation(result: Result<&2, &2, AES.Error, AES.Envelope>) -> List<&2, U32>:
513    match result:
514        case Fail{error}: []
515        case Done{envelope}:
516            match envelope:
517                case AES.Envelope{nonce, ciphertext, tag, valid}:
518                    match nonce tag:
519                        case AES.Nonce{nonce_bytes, nonce_size, nonce_valid}
520                             AES.Tag{tag_bytes, tag_size, tag_valid}:
521                            List.append(&2, U32, nonce_bytes,
522                                List.append(&2, U32, ciphertext, tag_bytes))
523
524law aes256gcm_nist_empty_encrypt:
525    {aes256gcm_nist_encrypt_observation(AES.encrypt(aes256gcm_nist_key(), aes256gcm_nist_nonce(),
526        [], [])) == aes256gcm_nist_encrypt_observation(Done{aes256gcm_nist_empty()}) :
527        List<&2, U32>}
528
529law aes256gcm_nist_empty_decrypt:
530    {AES.decrypt(aes256gcm_nist_key(), [],
531        aes256gcm_nist_empty()) == Done{[]} :
532        Result<&2, &2, AES.Error, List<&2, U32>>}
533
534def aes256gcm_nist_multiblock() -> AES.Envelope:
535    AES.Envelope{aes256gcm_nist_nonce(), [82, 45, 193, 240, 153, 86, 125, 7, 244, 127, 55, 163, 42, 132, 66, 125, 100, 58, 140, 220, 191, 229, 192, 201, 117, 152, 162, 189, 37, 85, 209, 170, 140, 176, 142, 72, 89, 13, 187, 61, 167, 176, 139, 16, 86, 130, 136, 56, 197, 246, 30, 99, 147, 186, 122, 10, 188, 201, 246, 98, 137, 128, 21, 173],
536        AES.Tag{[176, 148, 218, 197, 217, 52, 113, 189, 236, 26, 80, 34, 112, 227, 204, 108], {==}, {==}}, {==}}
537
538law aes256gcm_nist_multiblock_encrypt:
539    {aes256gcm_nist_encrypt_observation(AES.encrypt(aes256gcm_nist_key(), aes256gcm_nist_nonce(),
540        [], [217, 49, 50, 37, 248, 132, 6, 229, 165, 89, 9, 197, 175, 245, 38, 154, 134, 167, 169, 83, 21, 52, 247, 218, 46, 76, 48, 61, 138, 49, 138, 114, 28, 60, 12, 149, 149, 104, 9, 83, 47, 207, 14, 36, 73, 166, 181, 37, 177, 106, 237, 245, 170, 13, 230, 87, 186, 99, 123, 57, 26, 175, 210, 85])) == aes256gcm_nist_encrypt_observation(Done{aes256gcm_nist_multiblock()}) :
541        List<&2, U32>}
542
543law aes256gcm_nist_multiblock_decrypt:
544    {AES.decrypt(aes256gcm_nist_key(), [],
545        aes256gcm_nist_multiblock()) == Done{[217, 49, 50, 37, 248, 132, 6, 229, 165, 89, 9, 197, 175, 245, 38, 154, 134, 167, 169, 83, 21, 52, 247, 218, 46, 76, 48, 61, 138, 49, 138, 114, 28, 60, 12, 149, 149, 104, 9, 83, 47, 207, 14, 36, 73, 166, 181, 37, 177, 106, 237, 245, 170, 13, 230, 87, 186, 99, 123, 57, 26, 175, 210, 85]} :
546        Result<&2, &2, AES.Error, List<&2, U32>>}
547
548def aes256gcm_nist_aad_only() -> AES.Envelope:
549    AES.Envelope{aes256gcm_nist_nonce(), [],
550        AES.Tag{[222, 52, 182, 220, 212, 206, 226, 253, 190, 195, 206, 160, 26, 241, 238, 68], {==}, {==}}, {==}}
551
552law aes256gcm_nist_aad_only_encrypt:
553    {aes256gcm_nist_encrypt_observation(AES.encrypt(aes256gcm_nist_key(), aes256gcm_nist_nonce(),
554        [58, 215, 123, 180, 13, 122, 54, 96, 168, 158, 202, 243, 36, 102, 239, 151, 245, 211, 213, 133, 3, 185, 105, 157, 231, 133, 137, 90, 150, 253, 186, 175, 67, 177, 205, 127, 89, 142, 206, 35, 136, 27, 0, 227, 237, 3, 6, 136, 123, 12, 120, 94, 39, 232, 173, 63, 130, 35, 32, 113, 4, 114, 93, 212], [])) == aes256gcm_nist_encrypt_observation(Done{aes256gcm_nist_aad_only()}) :
555        List<&2, U32>}
556
557law aes256gcm_nist_aad_only_decrypt:
558    {AES.decrypt(aes256gcm_nist_key(), [58, 215, 123, 180, 13, 122, 54, 96, 168, 158, 202, 243, 36, 102, 239, 151, 245, 211, 213, 133, 3, 185, 105, 157, 231, 133, 137, 90, 150, 253, 186, 175, 67, 177, 205, 127, 89, 142, 206, 35, 136, 27, 0, 227, 237, 3, 6, 136, 123, 12, 120, 94, 39, 232, 173, 63, 130, 35, 32, 113, 4, 114, 93, 212],
559        aes256gcm_nist_aad_only()) == Done{[]} :
560        Result<&2, &2, AES.Error, List<&2, U32>>}
561
562def aes256gcm_nist_aad_and_multiblock() -> AES.Envelope:
563    AES.Envelope{aes256gcm_nist_nonce(), [82, 45, 193, 240, 153, 86, 125, 7, 244, 127, 55, 163, 42, 132, 66, 125, 100, 58, 140, 220, 191, 229, 192, 201, 117, 152, 162, 189, 37, 85, 209, 170, 140, 176, 142, 72, 89, 13, 187, 61, 167, 176, 139, 16, 86, 130, 136, 56, 197, 246, 30, 99, 147, 186, 122, 10, 188, 201, 246, 98, 137, 128, 21, 173],
564        AES.Tag{[192, 109, 118, 243, 25, 48, 254, 243, 122, 202, 226, 62, 212, 101, 174, 98], {==}, {==}}, {==}}
565
566law aes256gcm_nist_aad_and_multiblock_encrypt:
567    {aes256gcm_nist_encrypt_observation(AES.encrypt(aes256gcm_nist_key(), aes256gcm_nist_nonce(),
568        [58, 215, 123, 180, 13, 122, 54, 96, 168, 158, 202, 243, 36, 102, 239, 151, 245, 211, 213, 133, 3, 185, 105, 157, 231, 133, 137, 90, 150, 253, 186, 175, 67, 177, 205, 127, 89, 142, 206, 35, 136, 27, 0, 227, 237, 3, 6, 136, 123, 12, 120, 94, 39, 232, 173, 63, 130, 35, 32, 113, 4, 114, 93, 212], [217, 49, 50, 37, 248, 132, 6, 229, 165, 89, 9, 197, 175, 245, 38, 154, 134, 167, 169, 83, 21, 52, 247, 218, 46, 76, 48, 61, 138, 49, 138, 114, 28, 60, 12, 149, 149, 104, 9, 83, 47, 207, 14, 36, 73, 166, 181, 37, 177, 106, 237, 245, 170, 13, 230, 87, 186, 99, 123, 57, 26, 175, 210, 85])) == aes256gcm_nist_encrypt_observation(Done{aes256gcm_nist_aad_and_multiblock()}) :
569        List<&2, U32>}
570
571law aes256gcm_nist_aad_and_multiblock_decrypt:
572    {AES.decrypt(aes256gcm_nist_key(), [58, 215, 123, 180, 13, 122, 54, 96, 168, 158, 202, 243, 36, 102, 239, 151, 245, 211, 213, 133, 3, 185, 105, 157, 231, 133, 137, 90, 150, 253, 186, 175, 67, 177, 205, 127, 89, 142, 206, 35, 136, 27, 0, 227, 237, 3, 6, 136, 123, 12, 120, 94, 39, 232, 173, 63, 130, 35, 32, 113, 4, 114, 93, 212],
573        aes256gcm_nist_aad_and_multiblock()) == Done{[217, 49, 50, 37, 248, 132, 6, 229, 165, 89, 9, 197, 175, 245, 38, 154, 134, 167, 169, 83, 21, 52, 247, 218, 46, 76, 48, 61, 138, 49, 138, 114, 28, 60, 12, 149, 149, 104, 9, 83, 47, 207, 14, 36, 73, 166, 181, 37, 177, 106, 237, 245, 170, 13, 230, 87, 186, 99, 123, 57, 26, 175, 210, 85]} :
574        Result<&2, &2, AES.Error, List<&2, U32>>}
575
576def aes256gcm_nist_partial_block() -> AES.Envelope:
577    AES.Envelope{aes256gcm_nist_nonce(), [82, 45, 193, 240, 153, 86, 125, 7, 244, 127, 55, 163, 42, 132, 66, 125, 100, 58, 140, 220, 191, 229, 192, 201, 117, 152, 162, 189, 37, 85, 209, 170, 140, 176, 142, 72, 89, 13, 187, 61, 167, 176, 139, 16, 86, 130, 136, 56, 197, 246, 30, 99, 147, 186, 122, 10, 188, 201, 246, 98],
578        AES.Tag{[224, 151, 25, 95, 69, 50, 218, 137, 95, 185, 23, 165, 165, 92, 106, 160], {==}, {==}}, {==}}
579
580law aes256gcm_nist_partial_block_encrypt:
581    {aes256gcm_nist_encrypt_observation(AES.encrypt(aes256gcm_nist_key(), aes256gcm_nist_nonce(),
582        [58, 215, 123, 180, 13, 122, 54, 96, 168, 158, 202, 243, 36, 102, 239, 151, 245, 211, 213, 133], [217, 49, 50, 37, 248, 132, 6, 229, 165, 89, 9, 197, 175, 245, 38, 154, 134, 167, 169, 83, 21, 52, 247, 218, 46, 76, 48, 61, 138, 49, 138, 114, 28, 60, 12, 149, 149, 104, 9, 83, 47, 207, 14, 36, 73, 166, 181, 37, 177, 106, 237, 245, 170, 13, 230, 87, 186, 99, 123, 57])) == aes256gcm_nist_encrypt_observation(Done{aes256gcm_nist_partial_block()}) :
583        List<&2, U32>}
584
585law aes256gcm_nist_partial_block_decrypt:
586    {AES.decrypt(aes256gcm_nist_key(), [58, 215, 123, 180, 13, 122, 54, 96, 168, 158, 202, 243, 36, 102, 239, 151, 245, 211, 213, 133],
587        aes256gcm_nist_partial_block()) == Done{[217, 49, 50, 37, 248, 132, 6, 229, 165, 89, 9, 197, 175, 245, 38, 154, 134, 167, 169, 83, 21, 52, 247, 218, 46, 76, 48, 61, 138, 49, 138, 114, 28, 60, 12, 149, 149, 104, 9, 83, 47, 207, 14, 36, 73, 166, 181, 37, 177, 106, 237, 245, 170, 13, 230, 87, 186, 99, 123, 57]} :
588        Result<&2, &2, AES.Error, List<&2, U32>>}
589
590law aes256gcm_nist_canonical_encoding:
591    {AES.encode(aes256gcm_nist_empty()) == "v1.cafebabefacedbaddecaf888.fd2caa16a5832e76aa132c1453eeda7e." : String}
592
593law aes256gcm_nist_canonical_parsing:
594    {AES.parse("v1.cafebabefacedbaddecaf888.fd2caa16a5832e76aa132c1453eeda7e.") == Done{aes256gcm_nist_empty()} :
595        Result<&2, &2, AES.Error, AES.Envelope>}
596
597# Concrete tamper checks supplement tag uniqueness without claiming collision-

598# free authentication for all distinct AAD, nonce, key, or ciphertext inputs.

599law aes256gcm_nist_rejects_changed_aad:
600    {AES.decrypt(aes256gcm_nist_key(), [1], aes256gcm_nist_empty()) ==
601        Fail{AES.AuthenticationFailed{}} :
602        Result<&2, &2, AES.Error, List<&2, U32>>}
603
604law aes256gcm_nist_rejects_changed_key:
605    {AES.decrypt(AES.SecretKey{List.replicate(U32, 32n, 0), {==}, {==}},
606        [], aes256gcm_nist_empty()) == Fail{AES.AuthenticationFailed{}} :
607        Result<&2, &2, AES.Error, List<&2, U32>>}
608
609law aes256gcm_nist_rejects_changed_nonce:
610    {AES.decrypt(aes256gcm_nist_key(), [],
611        AES.Envelope{AES.Nonce{List.replicate(U32, 12n, 0), {==}, {==}},
612            [], AES.Tag{[253, 44, 170, 22, 165, 131, 46, 118, 170, 19, 44, 20, 83, 238, 218, 126], {==}, {==}}, {==}}) ==
613        Fail{AES.AuthenticationFailed{}} :
614        Result<&2, &2, AES.Error, List<&2, U32>>}
615
616law aes256gcm_nist_rejects_changed_ciphertext:
617    {AES.decrypt(aes256gcm_nist_key(), [],
618        AES.Envelope{aes256gcm_nist_nonce(), [1],
619            AES.Tag{[253, 44, 170, 22, 165, 131, 46, 118, 170, 19, 44, 20, 83, 238, 218, 126], {==}, {==}}, {==}}) ==
620        Fail{AES.AuthenticationFailed{}} :
621        Result<&2, &2, AES.Error, List<&2, U32>>}