1	# Library correctness laws and integration obligations.
2	
3	import 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	
11	import ./libs/JSON.bend as Json
12	import ./libs/URL.bend as URL
13	import ./libs/AES256GCM.bend as AES
14	
15	# ============================================================
16	# JSON: Core correctness
17	# ============================================================
18	
19	law 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	
32	law parses_null:
33	    { Json.parse("null") == Done{Json.Null{}} :
34	        Result<&1, &1, Json.Error, Json.Value> }
35	
36	law parses_true:
37	    { Json.parse("true") == Done{Json.Bool{True{}}} :
38	        Result<&1, &1, Json.Error, Json.Value> }
39	
40	law 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	
48	law 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	
54	law 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	
60	law 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	
70	law rejects_trailing_garbage:
71	    { Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse("nullx"))
72	        == True{} : Bool }
73	
74	law rejects_second_value:
75	    { Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse("null true"))
76	        == True{} : Bool }
77	
78	law rejects_invalid_null:
79	    { Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse("nul"))
80	        == True{} : Bool }
81	
82	law rejects_invalid_true:
83	    { Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse("tru"))
84	        == True{} : Bool }
85	
86	law rejects_invalid_false:
87	    { Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse("fals"))
88	        == True{} : Bool }
89	
90	law rejects_empty_input:
91	    { Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse(""))
92	        == True{} : Bool }
93	
94	law 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	
102	law parses_empty_string:
103	    { Json.parse("\"\"") == Done{Json.Str{""}} :
104	        Result<&1, &1, Json.Error, Json.Value> }
105	
106	law parses_simple_string:
107	    { Json.parse("\"hello\"") == Done{Json.Str{"hello"}} :
108	        Result<&1, &1, Json.Error, Json.Value> }
109	
110	law parses_newline_escape:
111	    { Json.parse("\"a\\nb\"") == Done{Json.Str{"a\nb"}} :
112	        Result<&1, &1, Json.Error, Json.Value> }
113	
114	law parses_quote_escape:
115	    { Json.parse("\"a\\\"b\"") == Done{Json.Str{"a\"b"}} :
116	        Result<&1, &1, Json.Error, Json.Value> }
117	
118	law parses_backslash_escape:
119	    { Json.parse("\"a\\\\b\"") == Done{Json.Str{"a\\b"}} :
120	        Result<&1, &1, Json.Error, Json.Value> }
121	
122	law 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	
130	law parses_empty_array:
131	    { Json.parse("[]") == Done{Json.Arr{Nil{}}} :
132	        Result<&1, &1, Json.Error, Json.Value> }
133	
134	law 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	
148	law 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	
156	law parses_empty_object:
157	    { Json.parse("{}") == Done{Json.Obj{Nil{}}} :
158	        Result<&1, &1, Json.Error, Json.Value> }
159	
160	law rejects_unquoted_object_key:
161	    { Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse("{foo:null}"))
162	        == True{} : Bool }
163	
164	law 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	
172	law 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.
196	law 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.
201	law 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.
207	law parses_unicode_escape:
208	    { Json.parse("\"\\u263A\"") == Done{Json.Str{"\u{263a}"}} :
209	        Result<&1, &1, Json.Error, Json.Value> }
210	
211	law 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.
217	law parses_fraction_and_exponent:
218	    { Result.is_done(&1, &1, Json.Error, Json.Value, Json.parse("-12.50e+3"))
219	        == True{} : Bool }
220	
221	law 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.
229	law 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	
237	law 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.
245	law 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	
251	law 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	
257	law 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.
267	law url_component_ascii:
268	    { URL.percent_component("A") == "%41" : String }
269	
270	law url_component_reserved:
271	    { URL.percent_component("/") == "%2F" : String }
272	
273	law 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	
281	law 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	
288	law 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	
294	law 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	
300	law 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	
307	law 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	
313	law 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.
324	law 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	
334	law 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	
343	law 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	
352	law 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	
360	law 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	
371	law 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	
381	law 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.
395	law 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	
417	law 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	
422	law 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	
429	law aes256gcm_rejects_empty_envelope:
430	    {AES.parse("") == Fail{AES.InvalidEnvelope{}} :
431	        Result<&2, &2, AES.Error, AES.Envelope>}
432	
433	law aes256gcm_rejects_unknown_version:
434	    {AES.parse("v2.cafebabefacedbaddecaf888.fd2caa16a5832e76aa132c1453eeda7e.") == Fail{AES.InvalidEnvelope{}} :
435	        Result<&2, &2, AES.Error, AES.Envelope>}
436	
437	law aes256gcm_rejects_missing_version:
438	    {AES.parse("cafebabefacedbaddecaf888.fd2caa16a5832e76aa132c1453eeda7e.") == Fail{AES.InvalidEnvelope{}} :
439	        Result<&2, &2, AES.Error, AES.Envelope>}
440	
441	law aes256gcm_rejects_short_nonce:
442	    {AES.parse("v1.cafebabefacedbaddecaf8.fd2caa16a5832e76aa132c1453eeda7e.") == Fail{AES.InvalidEnvelope{}} :
443	        Result<&2, &2, AES.Error, AES.Envelope>}
444	
445	law aes256gcm_rejects_long_nonce:
446	    {AES.parse("v1.cafebabefacedbaddecaf88800.fd2caa16a5832e76aa132c1453eeda7e.") == Fail{AES.InvalidEnvelope{}} :
447	        Result<&2, &2, AES.Error, AES.Envelope>}
448	
449	law aes256gcm_rejects_short_tag:
450	    {AES.parse("v1.cafebabefacedbaddecaf888.fd2caa16a5832e76aa132c1453eeda.") == Fail{AES.InvalidEnvelope{}} :
451	        Result<&2, &2, AES.Error, AES.Envelope>}
452	
453	law aes256gcm_rejects_long_tag:
454	    {AES.parse("v1.cafebabefacedbaddecaf888.fd2caa16a5832e76aa132c1453eeda7e00.") == Fail{AES.InvalidEnvelope{}} :
455	        Result<&2, &2, AES.Error, AES.Envelope>}
456	
457	law aes256gcm_rejects_odd_ciphertext_hex:
458	    {AES.parse("v1.cafebabefacedbaddecaf888.fd2caa16a5832e76aa132c1453eeda7e.0") == Fail{AES.InvalidEnvelope{}} :
459	        Result<&2, &2, AES.Error, AES.Envelope>}
460	
461	law aes256gcm_rejects_non_hex_ciphertext:
462	    {AES.parse("v1.cafebabefacedbaddecaf888.fd2caa16a5832e76aa132c1453eeda7e.gg") == Fail{AES.InvalidEnvelope{}} :
463	        Result<&2, &2, AES.Error, AES.Envelope>}
464	
465	law aes256gcm_rejects_non_hex_nonce:
466	    {AES.parse("v1.zzfebabefacedbaddecaf888.fd2caa16a5832e76aa132c1453eeda7e.") == Fail{AES.InvalidEnvelope{}} :
467	        Result<&2, &2, AES.Error, AES.Envelope>}
468	
469	law aes256gcm_rejects_non_hex_tag:
470	    {AES.parse("v1.cafebabefacedbaddecaf888.zz2caa16a5832e76aa132c1453eeda7e.") == Fail{AES.InvalidEnvelope{}} :
471	        Result<&2, &2, AES.Error, AES.Envelope>}
472	
473	law aes256gcm_rejects_uppercase_hex:
474	    {AES.parse("v1.CAFEBABEFACEDBADDECAF888.fd2caa16a5832e76aa132c1453eeda7e.") == Fail{AES.InvalidEnvelope{}} :
475	        Result<&2, &2, AES.Error, AES.Envelope>}
476	
477	law aes256gcm_rejects_extra_field:
478	    {AES.parse("v1.cafebabefacedbaddecaf888.fd2caa16a5832e76aa132c1453eeda7e..") == Fail{AES.InvalidEnvelope{}} :
479	        Result<&2, &2, AES.Error, AES.Envelope>}
480	
481	law aes256gcm_rejects_missing_ciphertext_field:
482	    {AES.parse("v1.cafebabefacedbaddecaf888.fd2caa16a5832e76aa132c1453eeda7e") == Fail{AES.InvalidEnvelope{}} :
483	        Result<&2, &2, AES.Error, AES.Envelope>}
484	
485	law aes256gcm_rejects_trailing_garbage:
486	    {AES.parse("v1.cafebabefacedbaddecaf888.fd2caa16a5832e76aa132c1453eeda7e.00!") == Fail{AES.InvalidEnvelope{}} :
487	        Result<&2, &2, AES.Error, AES.Envelope>}
488	
489	law 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	
500	def 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	
503	def aes256gcm_nist_nonce() -> AES.Nonce:
504	    AES.Nonce{[202, 254, 186, 190, 250, 206, 219, 173, 222, 202, 248, 136], {==}, {==}}
505	
506	def 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.
512	def 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	
524	law 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	
529	law 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	
534	def 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	
538	law 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	
543	law 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	
548	def 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	
552	law 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	
557	law 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	
562	def 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	
566	law 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	
571	law 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	
576	def 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	
580	law 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	
585	law 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	
590	law aes256gcm_nist_canonical_encoding:
591	    {AES.encode(aes256gcm_nist_empty()) == "v1.cafebabefacedbaddecaf888.fd2caa16a5832e76aa132c1453eeda7e." : String}
592	
593	law 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.
599	law 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	
604	law 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	
609	law 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	
616	law 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>>}