PROOF.bend
qasim-bend-kit@0.1.0.2 · 813 lines · 42 definitions
1import Base
2import qasim-bend-kit@0.1.0.2/proof/AES_NistInputProof.bend as AESNistInputProof
3import qasim-bend-kit@0.1.0.2/LAWS.bend as L
4import qasim-bend-kit@0.1.0.2/libs/JSON.bend as Json
5import qasim-bend-kit@0.1.0.2/libs/URL.bend as URL
6import qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend as AES
7import qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend as Core
8import qasim-bend-kit@0.1.0.2/proof/AES_EncryptProof.bend as AESEncryptProof
9import qasim-bend-kit@0.1.0.2/proof/AES_TamperProof.bend as AESTamperProof
10import qasim-bend-kit@0.1.0.2/proof/AES_CanonicalProof.bend as AESCanonicalProof
11import qasim-bend-kit@0.1.0.2/proof/AES_ConstructorProof.bend as AESConstructorProof
12import qasim-bend-kit@0.1.0.2/proof/AES_IdentityProof.bend as AESIdentityProof
13import qasim-bend-kit@0.1.0.2/proof/AES_NistKeyScheduleProof.bend as AESNistKeyScheduleProof
14import qasim-bend-kit@0.1.0.2/proof/AES_NistBlockComposeProof.bend as AESNistBlockComposeProof
15import qasim-bend-kit@0.1.0.2/proof/AES_NistBlockProof.bend as AESNistBlockProof
16import qasim-bend-kit@0.1.0.2/proof/AES_NistObservationProof.bend as AESNistObservationProof
17import qasim-bend-kit@0.1.0.2/proof/AES_NistVectorProof.bend as AESNistVectorProof
18import qasim-bend-kit@0.1.0.2/proof/AES_NistTamperVectorProof.bend as AESNistTamperVectorProof
19import qasim-bend-kit@0.1.0.2/proof/JSON_StringProof.bend as StringProof
20import qasim-bend-kit@0.1.0.2/proof/JSON_PrimitiveProof.bend as PrimitiveProof
21import qasim-bend-kit@0.1.0.2/proof/JSON_NumberLexProof.bend as NumberLexProof
22import qasim-bend-kit@0.1.0.2/proof/JSON_ParallelProof.bend as ParallelProof
23import qasim-bend-kit@0.1.0.2/proof/JSON_LexWhitespaceProof.bend as LexWhitespaceProof
24import qasim-bend-kit@0.1.0.2/proof/JSON_AssemblyProof.bend as AssemblyProof
25import qasim-bend-kit@0.1.0.2/proof/JSON_SourceProof.bend as SourceProof
26import qasim-bend-kit@0.1.0.2/proof/JSON_RenderLexProof.bend as RenderLexProof
27
28def ResultValue() -> Type:
29 Result<&1, &1, Json.Error, Json.Value>
30
31def parse_for_equality(text: String) -> ResultValue():
32 Json.parse(text)
33
34def assemble_atom(result: ResultValue()) -> {Json.assemble(Json.Atom{result} <> Nil{}, Json.NeedValue{Json.Top{}}) == result : ResultValue()}:
35 match result:
36 case Done{value}: {==}
37 case Fail{Json.Error{}}: {==}
38
39def parallel_single(+text: String) -> {Json.token_list(Json.decode_tree(Json.lex_tree(Json.Payload{text} <> Nil{})), Nil{}) == Json.decode_lexeme(Json.Payload{text}) <> Nil{} : List<Json.Token>}:
40 Equal.trans(List<Json.Token>, Json.token_list(Json.decode_tree(Json.lex_tree(Json.Payload{text} <> Nil{})), Nil{}),
41 ParallelProof.flat(Json.Payload{text} <> Nil{}, Nil{}), Json.decode_lexeme(Json.Payload{text}) <> Nil{},
42 ParallelProof.decode(Json.Payload{text} <> Nil{}, Nil{}), {==})
43
44def assemble_source(+value: Json.Value) -> {Json.assemble(Json.token_list(Json.decode_tree(Json.lex_tree(Json.source(value, False{}, Nil{}))), Nil{}), Json.NeedValue{Json.Top{}}) == Done{value} : ResultValue()}:
45 Equal.trans(ResultValue(),
46 Json.assemble(Json.token_list(Json.decode_tree(Json.lex_tree(Json.source(value, False{}, Nil{}))), Nil{}), Json.NeedValue{Json.Top{}}),
47 Json.assemble(AssemblyProof.tokens(value, AssemblyProof.Whole{}, Nil{}), AssemblyProof.start(value, AssemblyProof.Whole{}, Nil{}, Nil{}, Json.Top{})),
48 Done{value},
49 Equal.cong(List<Json.Token>, ResultValue(), tokens => Json.assemble(tokens, Json.NeedValue{Json.Top{}}),
50 Json.token_list(Json.decode_tree(Json.lex_tree(Json.source(value, False{}, Nil{}))), Nil{}),
51 AssemblyProof.tokens(value, AssemblyProof.Whole{}, Nil{}),
52 Equal.trans(List<Json.Token>,
53 Json.token_list(Json.decode_tree(Json.lex_tree(Json.source(value, False{}, Nil{}))), Nil{}),
54 SourceProof.token_source(Json.source(value, False{}, Nil{}), Nil{}),
55 AssemblyProof.tokens(value, AssemblyProof.Whole{}, Nil{}),
56 Equal.trans(List<Json.Token>,
57 Json.token_list(Json.decode_tree(Json.lex_tree(Json.source(value, False{}, Nil{}))), Nil{}),
58 ParallelProof.flat(Json.source(value, False{}, Nil{}), Nil{}),
59 SourceProof.token_source(Json.source(value, False{}, Nil{}), Nil{}),
60 ParallelProof.decode(Json.source(value, False{}, Nil{}), Nil{}),
61 Equal.sym(List<Json.Token>, SourceProof.token_source(Json.source(value, False{}, Nil{}), Nil{}),
62 ParallelProof.flat(Json.source(value, False{}, Nil{}), Nil{}),
63 SourceProof.token_source_flat(Json.source(value, False{}, Nil{}), Nil{}))),
64 SourceProof.source_tokens(value, AssemblyProof.Whole{}, Nil{}, Nil{}))),
65 Equal.trans(ResultValue(),
66 Json.assemble(AssemblyProof.tokens(value, AssemblyProof.Whole{}, Nil{}), AssemblyProof.start(value, AssemblyProof.Whole{}, Nil{}, Nil{}, Json.Top{})),
67 Json.assemble(Nil{}, Json.assembly_resume(Json.Top{}, value)),
68 Done{value},
69 AssemblyProof.roundtrip(value, AssemblyProof.Whole{}, Nil{}, Nil{}, Nil{}, Json.Top{}), {==}))
70
71def parse_number_payload(+text: String,
72 +certificate: Json.NumberCert<text>) -> {Json.parse_normalized(text) == Done{Json.Number{text, certificate}} : ResultValue()}:
73 Equal.trans(ResultValue(), Json.parse_normalized(text),
74 Json.assemble(Json.token_list(Json.decode_tree(Json.lex_tree(Json.Payload{text} <> Nil{})), Nil{}), Json.NeedValue{Json.Top{}}),
75 Done{Json.Number{text, certificate}},
76 Equal.cong(List<&2, Json.Lexeme>, ResultValue(), items => Json.assemble(Json.token_list(Json.decode_tree(Json.lex_tree(items)), Nil{}), Json.NeedValue{Json.Top{}}),
77 Json.lex_scan(text, Json.Outside{}, SNil{}, Nil{}), Json.Payload{text} <> Nil{},
78 NumberLexProof.lex_number_payload(text, PrimitiveProof.cert_valid(text, certificate))),
79 Equal.trans(ResultValue(),
80 Json.assemble(Json.token_list(Json.decode_tree(Json.lex_tree(Json.Payload{text} <> Nil{})), Nil{}), Json.NeedValue{Json.Top{}}),
81 Json.decode_payload(text), Done{Json.Number{text, certificate}},
82 Equal.trans(ResultValue(),
83 Json.assemble(Json.token_list(Json.decode_tree(Json.lex_tree(Json.Payload{text} <> Nil{})), Nil{}), Json.NeedValue{Json.Top{}}),
84 Json.assemble(Json.decode_lexeme(Json.Payload{text}) <> Nil{}, Json.NeedValue{Json.Top{}}),
85 Json.decode_payload(text),
86 Equal.cong(List<Json.Token>, ResultValue(), tokens => Json.assemble(tokens, Json.NeedValue{Json.Top{}}),
87 Json.token_list(Json.decode_tree(Json.lex_tree(Json.Payload{text} <> Nil{})), Nil{}),
88 Json.decode_lexeme(Json.Payload{text}) <> Nil{},
89 parallel_single(text)),
90 Equal.trans(ResultValue(),
91 Json.assemble(Json.decode_lexeme(Json.Payload{text}) <> Nil{}, Json.NeedValue{Json.Top{}}),
92 Json.decode_payload(text), Json.decode_payload(text),
93 assemble_atom(Json.decode_payload(text)), {==})),
94 PrimitiveProof.number_roundtrip(text, certificate)))
95
96def assembled_string_payload(+text: String) -> {Json.assemble(Json.Atom{Json.decode_payload("\"" ++ Json.escape_string(text) ++ "\"")} <> Nil{}, Json.NeedValue{Json.Top{}}) == Done{Json.Str{text}} : ResultValue()}:
97 Equal.cong(ResultValue(), ResultValue(), result => Json.assemble(Json.Atom{result} <> Nil{}, Json.NeedValue{Json.Top{}}),
98 Json.decode_payload("\"" ++ Json.escape_string(text) ++ "\""), Done{Json.Str{text}}, StringProof.string_payload(text))
99
100def parse_string_payload(+text: String) -> {Json.parse_normalized("\"" ++ Json.escape_string(text) ++ "\"") == Done{Json.Str{text}} : ResultValue()}:
101 Equal.trans(ResultValue(), Json.parse_normalized("\"" ++ Json.escape_string(text) ++ "\""),
102 Json.assemble(Json.token_list(Json.decode_tree(Json.lex_tree(Json.Payload{"\"" ++ Json.escape_string(text) ++ "\""} <> Nil{})), Nil{}), Json.NeedValue{Json.Top{}}),
103 Done{Json.Str{text}},
104 Equal.cong(List<&2, Json.Lexeme>, ResultValue(), items => Json.assemble(Json.token_list(Json.decode_tree(Json.lex_tree(items)), Nil{}), Json.NeedValue{Json.Top{}}),
105 Json.lex_scan("\"" ++ Json.escape_string(text) ++ "\"", Json.Outside{}, SNil{}, Nil{}),
106 Json.Payload{"\"" ++ Json.escape_string(text) ++ "\""} <> Nil{},
107 LexWhitespaceProof.lex_rendered_string(text)),
108 Equal.trans(ResultValue(),
109 Json.assemble(Json.token_list(Json.decode_tree(Json.lex_tree(Json.Payload{"\"" ++ Json.escape_string(text) ++ "\""} <> Nil{})), Nil{}), Json.NeedValue{Json.Top{}}),
110 Json.assemble(Json.decode_lexeme(Json.Payload{"\"" ++ Json.escape_string(text) ++ "\""}) <> Nil{}, Json.NeedValue{Json.Top{}}),
111 Done{Json.Str{text}},
112 Equal.cong(List<Json.Token>, ResultValue(), tokens => Json.assemble(tokens, Json.NeedValue{Json.Top{}}),
113 Json.token_list(Json.decode_tree(Json.lex_tree(Json.Payload{"\"" ++ Json.escape_string(text) ++ "\""} <> Nil{})), Nil{}),
114 Json.decode_lexeme(Json.Payload{"\"" ++ Json.escape_string(text) ++ "\""}) <> Nil{},
115 parallel_single("\"" ++ Json.escape_string(text) ++ "\"")),
116 assembled_string_payload(text)))
117
118def parse_leading_space(+text: String) -> {Json.parse(" " ++ text) == Json.parse(text) : Result<&1, &1, Json.Error, Json.Value>}:
119 {==}
120
121def parse_trailing_space(+text: String) -> {Json.parse(text ++ " ") == Json.parse(text) : Result<&1, &1, Json.Error, Json.Value>}:
122 Equal.cong(List<&2, Json.Lexeme>, ResultValue(),
123 items => Json.assemble(Json.token_list(Json.decode_tree(Json.lex_tree(items)), Nil{}), Json.NeedValue{Json.Top{}}),
124 Json.lex_scan(text ++ " ", Json.Outside{}, SNil{}, Nil{}),
125 Json.lex_scan(text, Json.Outside{}, SNil{}, Nil{}),
126 LexWhitespaceProof.trailing_space(text, Json.Outside{}, SNil{}, Nil{}))
127
128def parse_trailing_tab(+text: String) -> {Json.parse(text ++ "\t") == Json.parse(text) : Result<&1, &1, Json.Error, Json.Value>}:
129 Equal.cong(List<&2, Json.Lexeme>, ResultValue(),
130 items => Json.assemble(Json.token_list(Json.decode_tree(Json.lex_tree(items)), Nil{}), Json.NeedValue{Json.Top{}}),
131 Json.lex_scan(text ++ "\t", Json.Outside{}, SNil{}, Nil{}),
132 Json.lex_scan(text, Json.Outside{}, SNil{}, Nil{}),
133 LexWhitespaceProof.trailing_tab(text, Json.Outside{}, SNil{}, Nil{}))
134
135def parse_trailing_return(+text: String) -> {Json.parse(text ++ "\r") == Json.parse(text) : Result<&1, &1, Json.Error, Json.Value>}:
136 Equal.cong(List<&2, Json.Lexeme>, ResultValue(),
137 items => Json.assemble(Json.token_list(Json.decode_tree(Json.lex_tree(items)), Nil{}), Json.NeedValue{Json.Top{}}),
138 Json.lex_scan(text ++ "\r", Json.Outside{}, SNil{}, Nil{}),
139 Json.lex_scan(text, Json.Outside{}, SNil{}, Nil{}),
140 LexWhitespaceProof.trailing_return(text, Json.Outside{}, SNil{}, Nil{}))
141
142def parse_trailing_newline(+text: String) -> {Json.parse(text ++ "\n") == Json.parse(text) : Result<&1, &1, Json.Error, Json.Value>}:
143 Equal.cong(List<&2, Json.Lexeme>, ResultValue(),
144 items => Json.assemble(Json.token_list(Json.decode_tree(Json.lex_tree(items)), Nil{}), Json.NeedValue{Json.Top{}}),
145 Json.lex_scan(text ++ "\n", Json.Outside{}, SNil{}, Nil{}),
146 Json.lex_scan(text, Json.Outside{}, SNil{}, Nil{}),
147 LexWhitespaceProof.trailing_newline(text, Json.Outside{}, SNil{}, Nil{}))
148
149def parse_suffix_space(+text: String,
150 +suffix: String) -> {Json.parse(text ++ (suffix ++ " ")) == Json.parse(text ++ suffix) : Result<&1, &1, Json.Error, Json.Value>}:
151 Equal.trans(ResultValue(), Json.parse(text ++ (suffix ++ " ")), Json.parse((text ++ suffix) ++ " "), Json.parse(text ++ suffix),
152 Equal.sym(ResultValue(), Json.parse((text ++ suffix) ++ " "), Json.parse(text ++ (suffix ++ " ")),
153 Equal.cong(String, ResultValue(), parse_for_equality, (text ++ suffix) ++ " ", text ++ (suffix ++ " "), StringProof.append_assoc(text, suffix, " "))),
154 parse_trailing_space(text ++ suffix))
155
156def parse_suffix_tab(+text: String,
157 +suffix: String) -> {Json.parse(text ++ (suffix ++ "\t")) == Json.parse(text ++ suffix) : Result<&1, &1, Json.Error, Json.Value>}:
158 Equal.trans(ResultValue(), Json.parse(text ++ (suffix ++ "\t")), Json.parse((text ++ suffix) ++ "\t"), Json.parse(text ++ suffix),
159 Equal.sym(ResultValue(), Json.parse((text ++ suffix) ++ "\t"), Json.parse(text ++ (suffix ++ "\t")),
160 Equal.cong(String, ResultValue(), parse_for_equality, (text ++ suffix) ++ "\t", text ++ (suffix ++ "\t"), StringProof.append_assoc(text, suffix, "\t"))),
161 parse_trailing_tab(text ++ suffix))
162
163def parse_suffix_return(+text: String,
164 +suffix: String) -> {Json.parse(text ++ (suffix ++ "\r")) == Json.parse(text ++ suffix) : Result<&1, &1, Json.Error, Json.Value>}:
165 Equal.trans(ResultValue(), Json.parse(text ++ (suffix ++ "\r")), Json.parse((text ++ suffix) ++ "\r"), Json.parse(text ++ suffix),
166 Equal.sym(ResultValue(), Json.parse((text ++ suffix) ++ "\r"), Json.parse(text ++ (suffix ++ "\r")),
167 Equal.cong(String, ResultValue(), parse_for_equality, (text ++ suffix) ++ "\r", text ++ (suffix ++ "\r"), StringProof.append_assoc(text, suffix, "\r"))),
168 parse_trailing_return(text ++ suffix))
169
170def parse_suffix_newline(+text: String,
171 +suffix: String) -> {Json.parse(text ++ (suffix ++ "\n")) == Json.parse(text ++ suffix) : Result<&1, &1, Json.Error, Json.Value>}:
172 Equal.trans(ResultValue(), Json.parse(text ++ (suffix ++ "\n")), Json.parse((text ++ suffix) ++ "\n"), Json.parse(text ++ suffix),
173 Equal.sym(ResultValue(), Json.parse((text ++ suffix) ++ "\n"), Json.parse(text ++ (suffix ++ "\n")),
174 Equal.cong(String, ResultValue(), parse_for_equality, (text ++ suffix) ++ "\n", text ++ (suffix ++ "\n"), StringProof.append_assoc(text, suffix, "\n"))),
175 parse_trailing_newline(text ++ suffix))
176
177def parse_leading_surround(+text: String) -> {Json.parse(" \n\t\r" ++ text) == Json.parse(text) : Result<&1, &1, Json.Error, Json.Value>}:
178 {==}
179
180def parse_surrounding_space(+text: String) -> {Json.parse(" \n\t\r" ++ text ++ "\r\t\n ") == Json.parse(text) : Result<&1, &1, Json.Error, Json.Value>}:
181 Equal.trans(ResultValue(), Json.parse(" \n\t\r" ++ text ++ "\r\t\n "), Json.parse(text ++ "\r\t\n "), Json.parse(text),
182 parse_leading_surround(text ++ "\r\t\n "),
183 Equal.trans(ResultValue(), Json.parse(text ++ "\r\t\n "), Json.parse(text ++ "\r\t\n"), Json.parse(text),
184 parse_suffix_space(text, "\r\t\n"),
185 Equal.trans(ResultValue(), Json.parse(text ++ "\r\t\n"), Json.parse(text ++ "\r\t"), Json.parse(text),
186 parse_suffix_newline(text, "\r\t"),
187 Equal.trans(ResultValue(), Json.parse(text ++ "\r\t"), Json.parse(text ++ "\r"), Json.parse(text),
188 parse_suffix_tab(text, "\r"), parse_trailing_return(text)))))
189
190def L.parses_null():
191 {==}
192
193def L.parses_true():
194 {==}
195
196def L.parses_false():
197 {==}
198
199def L.rejects_trailing_garbage():
200 {==}
201
202def L.rejects_second_value():
203 {==}
204
205def L.rejects_invalid_null():
206 {==}
207
208def L.rejects_invalid_true():
209 {==}
210
211def L.rejects_invalid_false():
212 {==}
213
214def L.rejects_empty_input():
215 {==}
216
217def L.rejects_whitespace_only():
218 {==}
219
220def L.parses_empty_string():
221 {==}
222
223def L.parses_simple_string():
224 {==}
225
226def L.parses_newline_escape():
227 {==}
228
229def L.parses_quote_escape():
230 {==}
231
232def L.parses_backslash_escape():
233 {==}
234
235def L.rejects_unterminated_string():
236 {==}
237
238def L.parses_empty_array():
239 {==}
240
241def L.parses_literal_array():
242 {==}
243
244def L.rejects_array_trailing_comma():
245 {==}
246
247def L.parses_empty_object():
248 {==}
249
250def L.rejects_unquoted_object_key():
251 {==}
252
253def L.rejects_object_trailing_comma():
254 {==}
255
256def L.parses_nested_containers():
257 {==}
258
259def L.rejects_non_json_whitespace():
260 {==}
261
262def L.rejects_raw_string_control():
263 {==}
264
265def L.parses_unicode_escape():
266 {==}
267
268def L.parses_unicode_surrogate_pair():
269 {==}
270
271def L.parses_fraction_and_exponent():
272 {==}
273
274def L.rejects_malformed_number_forms():
275 {==}
276
277def L.preserves_array_order():
278 {==}
279
280def L.preserves_object_order_and_duplicates():
281 {==}
282
283def L.gpu_single_matches_cpu(text):
284 {==}
285
286def L.preserves_number_lexeme():
287 {==}
288
289def L.gpu_batch_matches_cpu(batch):
290 {==}
291
292def L.stringify_parse_roundtrip(value):
293 +v = value
294 Equal.trans(ResultValue(), Json.parse(Json.stringify(v)),
295 Json.assemble(Json.token_list(Json.decode_tree(Json.lex_tree(Json.source(v, False{}, Nil{}))), Nil{}), Json.NeedValue{Json.Top{}}),
296 Done{v},
297 Equal.cong(List<&2, Json.Lexeme>, ResultValue(), items =>
298 Json.assemble(Json.token_list(Json.decode_tree(Json.lex_tree(items)), Nil{}), Json.NeedValue{Json.Top{}}),
299 Json.lex_scan(Json.stringify(v), Json.Outside{}, SNil{}, Nil{}),
300 Json.source(v, False{}, Nil{}), RenderLexProof.lex_source(v)),
301 assemble_source(v))
302
303def L.accepts_leading_space(value):
304 +v = value
305 Equal.trans(Result<&1, &1, Json.Error, Json.Value>, Json.parse(" " ++ Json.stringify(v)), Json.parse(Json.stringify(v)), Done{v}, parse_leading_space(Json.stringify(v)), L.stringify_parse_roundtrip(v))
306
307def L.accepts_trailing_space(value):
308 +v = value
309 Equal.trans(Result<&1, &1, Json.Error, Json.Value>, Json.parse(Json.stringify(v) ++ " "), Json.parse(Json.stringify(v)), Done{v}, parse_trailing_space(Json.stringify(v)), L.stringify_parse_roundtrip(v))
310
311def L.accepts_surrounding_space(value):
312 +v = value
313 Equal.trans(Result<&1, &1, Json.Error, Json.Value>, Json.parse(" \n\t\r" ++ Json.stringify(v) ++ "\r\t\n "), Json.parse(Json.stringify(v)), Done{v}, parse_surrounding_space(Json.stringify(v)), L.stringify_parse_roundtrip(v))
314
315def L.url_component_ascii():
316 {==}
317
318def L.url_component_reserved():
319 {==}
320
321def L.url_component_utf8():
322 {==}
323
324def L.aes256gcm_rejects_empty_envelope():
325 {==}
326
327def L.aes256gcm_rejects_unknown_version():
328 {==}
329
330def L.aes256gcm_rejects_missing_version():
331 {==}
332
333def L.aes256gcm_rejects_short_nonce():
334 {==}
335
336def L.aes256gcm_rejects_long_nonce():
337 {==}
338
339def L.aes256gcm_rejects_short_tag():
340 {==}
341
342def L.aes256gcm_rejects_long_tag():
343 {==}
344
345def L.aes256gcm_rejects_odd_ciphertext_hex():
346 {==}
347
348def L.aes256gcm_rejects_non_hex_ciphertext():
349 {==}
350
351def L.aes256gcm_rejects_non_hex_nonce():
352 {==}
353
354def L.aes256gcm_rejects_non_hex_tag():
355 {==}
356
357def L.aes256gcm_rejects_uppercase_hex():
358 {==}
359
360def L.aes256gcm_rejects_extra_field():
361 {==}
362
363def L.aes256gcm_rejects_missing_ciphertext_field():
364 {==}
365
366def L.aes256gcm_rejects_trailing_garbage():
367 {==}
368
369def L.aes256gcm_rejects_surrounding_whitespace():
370 {==}
371
372def aes_nat_tail_ne(+a: Nat, +b: Nat,
373 no: {1n+a != 1n+b : Nat}) -> {a != b : Nat}:
374 e => no(Equal.cong(Nat, Nat, n => 1n+n, a, b, e))
375
376def aes_nat_pred(n: Nat) -> Nat:
377 match n:
378 case 0n: 0n
379 case 1n+p: p
380
381def aes_nat_zero_ne_succ(+p: Nat) -> {0n != 1n+p : Nat}:
382 e => PrimitiveProof.absurd(Empty,
383 PrimitiveProof.false_true(Equal.sym(Bool, True{}, False{},
384 Equal.cong(Nat, Bool, n => Nat.is_eq(n, 0n),
385 0n, 1n+p, e))))
386
387def aes_nat_succ_ne_zero(+p: Nat) -> {1n+p != 0n : Nat}:
388 e => PrimitiveProof.absurd(Empty,
389 PrimitiveProof.false_true(
390 Equal.cong(Nat, Bool, n => Nat.is_eq(n, 0n),
391 1n+p, 0n, e)))
392
393def aes_nat_eq_step_status(+a: Nat, +b: Nat,
394 result: Maybe<&0, {a == b : Nat}>) ->
395 {Maybe.is_some(&0, {1n+a == 1n+b : Nat},
396 AES.aes_nat_eq_step(a, b, result)) ==
397 Maybe.is_some(&0, {a == b : Nat}, result) : Bool}:
398 match result:
399 case None{}: {==}
400 case Some{proof}: {==}
401
402def aes_nat_eq_refl_is_some(+n: Nat) ->
403 {Maybe.is_some(&0, {n == n : Nat},
404 AES.aes_nat_eq_proof(n, n)) == True{} : Bool}:
405 match n:
406 case 0n: {==}
407 case 1n+p:
408 Equal.trans(Bool,
409 Maybe.is_some(&0, {1n+p == 1n+p : Nat},
410 AES.aes_nat_eq_proof(1n+p, 1n+p)),
411 Maybe.is_some(&0, {p == p : Nat},
412 AES.aes_nat_eq_proof(p, p)),
413 True{},
414 aes_nat_eq_step_status(p, p, AES.aes_nat_eq_proof(p, p)),
415 aes_nat_eq_refl_is_some(p))
416
417def aes_nat_eq_is_some(+a: Nat, +b: Nat, evidence: {a == b : Nat}) ->
418 {Maybe.is_some(&0, {a == b : Nat},
419 AES.aes_nat_eq_proof(a, b)) == True{} : Bool}:
420 Equal.trans(Bool,
421 Maybe.is_some(&0, {a == b : Nat}, AES.aes_nat_eq_proof(a, b)),
422 Maybe.is_some(&0, {b == b : Nat}, AES.aes_nat_eq_proof(b, b)),
423 True{},
424 Equal.cong(Nat, Bool,
425 value => Maybe.is_some(&0, {value == b : Nat},
426 AES.aes_nat_eq_proof(value, b)),
427 a, b, evidence),
428 aes_nat_eq_refl_is_some(b))
429def aes_nat_eq_none_if_ne(+a: Nat, +b: Nat,
430 no: {a != b : Nat}) ->
431 {AES.aes_nat_eq_proof(a, b) == None{} : Maybe<&0, {a == b : Nat}>}:
432 match a b:
433 case 0n 0n:
434 PrimitiveProof.absurd({AES.aes_nat_eq_proof(0n, 0n) == None{} :
435 Maybe<&0, {0n == 0n : Nat}>}, no({==}))
436 case 0n 1n+bp: {==}
437 case 1n+ap 0n: {==}
438 case 1n+ap 1n+bp:
439 recursive = aes_nat_eq_none_if_ne(ap, bp,
440 aes_nat_tail_ne(ap, bp, no))
441 Equal.trans(Maybe<&0, {1n+ap == 1n+bp : Nat}>,
442 AES.aes_nat_eq_step(ap, bp, AES.aes_nat_eq_proof(ap, bp)),
443 AES.aes_nat_eq_step(ap, bp, None{}), None{},
444 Equal.cong(Maybe<&0, {ap == bp : Nat}>,
445 Maybe<&0, {1n+ap == 1n+bp : Nat}>,
446 result => AES.aes_nat_eq_step(ap, bp, result),
447 AES.aes_nat_eq_proof(ap, bp), None{}, recursive),
448 {==})
449
450def aes_bytes_proof_none_if_invalid(+bytes: List<&2, U32>,
451 generated: Maybe<&0, {AES.bytes_valid(bytes) == True{} : Bool}>,
452 no: {AES.bytes_valid(bytes) == False{} : Bool}) ->
453 {generated == None{} : Maybe<&0, {AES.bytes_valid(bytes) == True{} : Bool}>}:
454 match generated:
455 case None{}: {==}
456 case Some{valid}:
457 contradiction = Equal.trans(Bool, True{}, AES.bytes_valid(bytes),
458 False{}, Equal.sym(Bool, AES.bytes_valid(bytes), True{}, valid),
459 no)
460 PrimitiveProof.absurd(
461 {Some{valid} == None{} :
462 Maybe<&0, {AES.bytes_valid(bytes) == True{} : Bool}>},
463 PrimitiveProof.false_true(Equal.sym(Bool, True{}, False{},
464 contradiction)))
465
466def aes_bytes_valid_none_if_false(+bytes: List<&2, U32>,
467 no: {AES.bytes_valid(bytes) == False{} : Bool}) ->
468 {AES.aes_bytes_valid_proof(bytes) == None{} :
469 Maybe<&0, {AES.bytes_valid(bytes) == True{} : Bool}>}:
470 aes_bytes_proof_none_if_invalid(bytes,
471 AES.aes_bytes_valid_proof(bytes), no)
472
473def aes_bytes_valid_status(+bytes: List<&2, U32>, b: Bool,
474 link: {b == AES.bytes_valid(bytes) : Bool}) ->
475 {Maybe.is_some(&0, {AES.bytes_valid(bytes) == True{} : Bool},
476 AES.aes_bytes_valid_from_bool(bytes, b, link)) == b : Bool}:
477 match b:
478 case False{}: {==}
479 case True{}: {==}
480
481def aes_bytes_cert_is_some(+bytes: List<&2, U32>,
482 evidence: {AES.bytes_valid(bytes) == True{} : Bool}) ->
483 {Maybe.is_some(&0, {AES.bytes_valid(bytes) == True{} : Bool},
484 AES.aes_bytes_valid_proof(bytes)) == True{} : Bool}:
485 Equal.trans(Bool,
486 Maybe.is_some(&0, {AES.bytes_valid(bytes) == True{} : Bool},
487 AES.aes_bytes_valid_proof(bytes)),
488 AES.bytes_valid(bytes), True{},
489 aes_bytes_valid_status(bytes, AES.bytes_valid(bytes), {==}),
490 evidence)
491def L.aes256gcm_accepts_32_byte_key(bytes, size, valid):
492 +size_copy = size
493 +valid_copy = valid
494 AESConstructorProof.key_accepts(bytes, size_copy, valid_copy,
495 AES.aes_nat_eq_proof(List.length(&2, U32, bytes), 32n),
496 AES.aes_bytes_valid_proof(bytes),
497 aes_nat_eq_is_some(List.length(&2, U32, bytes), 32n, size_copy),
498 aes_bytes_cert_is_some(bytes, valid_copy))
499
500def L.aes256gcm_accepts_12_byte_nonce(bytes, size, valid):
501 +size_copy = size
502 +valid_copy = valid
503 AESConstructorProof.nonce_accepts(bytes, size_copy, valid_copy,
504 AES.aes_nat_eq_proof(List.length(&2, U32, bytes), 12n),
505 AES.aes_bytes_valid_proof(bytes),
506 aes_nat_eq_is_some(List.length(&2, U32, bytes), 12n, size_copy),
507 aes_bytes_cert_is_some(bytes, valid_copy))
508
509def L.aes256gcm_encrypts_valid_input(key, nonce, aad, plaintext, aad_ok,
510 plaintext_ok):
511 AESEncryptProof.valid_input_is_done(key, nonce, aad, plaintext, aad_ok,
512 plaintext_ok)
513
514def L.aes256gcm_preserves_nonce(key, nonce, aad, plaintext, envelope,
515 encrypted):
516 AESEncryptProof.preserves_nonce(key, nonce, aad, plaintext, envelope,
517 encrypted)
518
519def L.aes256gcm_preserves_plaintext_length(key, nonce, aad, plaintext,
520 envelope, encrypted):
521 AESEncryptProof.successful_encrypt_preserves_length(key, nonce, aad,
522 plaintext, envelope, encrypted)
523
524def L.aes256gcm_envelope_is_canonical(text, envelope, parsed):
525 AESCanonicalProof.canonical_sound(text,
526 AES.parse_fields(String.split(text, Chr{46})), envelope, parsed)
527
528def L.aes256gcm_envelope_roundtrip(envelope):
529 AESIdentityProof.exact_roundtrip(envelope)
530
531def aes_key_from_no_size(+bytes: List<&2, U32>,
532 valid: Maybe<&0, {AES.bytes_valid(bytes) == True{} : Bool}>) ->
533 {AES.key_from_proofs(bytes, None{}, valid) == Fail{AES.InvalidKey{}} :
534 Result<&2, &2, AES.Error, AES.SecretKey>}:
535 {==}
536
537def aes_key_from_no_valid(+bytes: List<&2, U32>,
538 size: Maybe<&0, {List.length(&2, U32, bytes) == 32n : Nat}>) ->
539 {AES.key_from_proofs(bytes, size, None{}) == Fail{AES.InvalidKey{}} :
540 Result<&2, &2, AES.Error, AES.SecretKey>}:
541 match size:
542 case None{}: {==}
543 case Some{size}: {==}
544
545def L.aes256gcm_rejects_wrong_key_length(bytes, size):
546 Equal.trans(Result<&2, &2, AES.Error, AES.SecretKey>,
547 AES.key_impl(bytes),
548 AES.key_from_proofs(bytes, None{}, AES.aes_bytes_valid_proof(bytes)),
549 Fail{AES.InvalidKey{}},
550 Equal.cong(Maybe<&0, {List.length(&2, U32, bytes) == 32n : Nat}>,
551 Result<&2, &2, AES.Error, AES.SecretKey>,
552 maybe_size => AES.key_from_proofs(bytes, maybe_size,
553 AES.aes_bytes_valid_proof(bytes)),
554 AES.aes_nat_eq_proof(List.length(&2, U32, bytes), 32n), None{},
555 aes_nat_eq_none_if_ne(List.length(&2, U32, bytes), 32n, size)),
556 aes_key_from_no_size(bytes, AES.aes_bytes_valid_proof(bytes)))
557
558def L.aes256gcm_rejects_non_byte_key(bytes, invalid):
559 Equal.trans(Result<&2, &2, AES.Error, AES.SecretKey>,
560 AES.key_impl(bytes),
561 AES.key_from_proofs(bytes,
562 AES.aes_nat_eq_proof(List.length(&2, U32, bytes), 32n), None{}),
563 Fail{AES.InvalidKey{}},
564 Equal.cong(Maybe<&0, {AES.bytes_valid(bytes) == True{} : Bool}>,
565 Result<&2, &2, AES.Error, AES.SecretKey>,
566 maybe_valid => AES.key_from_proofs(bytes,
567 AES.aes_nat_eq_proof(List.length(&2, U32, bytes), 32n),
568 maybe_valid),
569 AES.aes_bytes_valid_proof(bytes), None{},
570 aes_bytes_valid_none_if_false(bytes, invalid)),
571 aes_key_from_no_valid(bytes,
572 AES.aes_nat_eq_proof(List.length(&2, U32, bytes), 32n)))
573
574def aes_nonce_from_no_size(+bytes: List<&2, U32>,
575 valid: Maybe<&0, {AES.bytes_valid(bytes) == True{} : Bool}>) ->
576 {AES.nonce_from_proofs(bytes, None{}, valid) == Fail{AES.InvalidNonce{}} :
577 Result<&2, &2, AES.Error, AES.Nonce>}:
578 {==}
579
580def aes_nonce_from_no_valid(+bytes: List<&2, U32>,
581 size: Maybe<&0, {List.length(&2, U32, bytes) == 12n : Nat}>) ->
582 {AES.nonce_from_proofs(bytes, size, None{}) == Fail{AES.InvalidNonce{}} :
583 Result<&2, &2, AES.Error, AES.Nonce>}:
584 match size:
585 case None{}: {==}
586 case Some{size}: {==}
587
588def L.aes256gcm_rejects_wrong_nonce_length(bytes, size):
589 Equal.trans(Result<&2, &2, AES.Error, AES.Nonce>,
590 AES.nonce_impl(bytes),
591 AES.nonce_from_proofs(bytes, None{}, AES.aes_bytes_valid_proof(bytes)),
592 Fail{AES.InvalidNonce{}},
593 Equal.cong(Maybe<&0, {List.length(&2, U32, bytes) == 12n : Nat}>,
594 Result<&2, &2, AES.Error, AES.Nonce>,
595 maybe_size => AES.nonce_from_proofs(bytes, maybe_size,
596 AES.aes_bytes_valid_proof(bytes)),
597 AES.aes_nat_eq_proof(List.length(&2, U32, bytes), 12n), None{},
598 aes_nat_eq_none_if_ne(List.length(&2, U32, bytes), 12n, size)),
599 aes_nonce_from_no_size(bytes, AES.aes_bytes_valid_proof(bytes)))
600
601def L.aes256gcm_rejects_non_byte_nonce(bytes, invalid):
602 Equal.trans(Result<&2, &2, AES.Error, AES.Nonce>,
603 AES.nonce_impl(bytes),
604 AES.nonce_from_proofs(bytes,
605 AES.aes_nat_eq_proof(List.length(&2, U32, bytes), 12n), None{}),
606 Fail{AES.InvalidNonce{}},
607 Equal.cong(Maybe<&0, {AES.bytes_valid(bytes) == True{} : Bool}>,
608 Result<&2, &2, AES.Error, AES.Nonce>,
609 maybe_valid => AES.nonce_from_proofs(bytes,
610 AES.aes_nat_eq_proof(List.length(&2, U32, bytes), 12n),
611 maybe_valid),
612 AES.aes_bytes_valid_proof(bytes), None{},
613 aes_bytes_valid_none_if_false(bytes, invalid)),
614 aes_nonce_from_no_valid(bytes,
615 AES.aes_nat_eq_proof(List.length(&2, U32, bytes), 12n)))
616
617def encrypt_invalid_plaintext(key: AES.SecretKey, nonce: AES.Nonce,
618 +aad: List<&2, U32>, +plaintext: List<&2, U32>, aad_ok: Bool) ->
619 {AES.encrypt_checked(key, nonce, aad, plaintext, aad_ok, False{}) ==
620 Fail{AES.InvalidBytes{}} : Result<&2, &2, AES.Error, AES.Envelope>}:
621 match aad_ok:
622 case True{}: {==}
623 case False{}: {==}
624
625def encrypt_using_plaintext_validity(key: AES.SecretKey, nonce: AES.Nonce,
626 +aad: List<&2, U32>, +plaintext: List<&2, U32>, plaintext_ok: Bool) ->
627 Result<&2, &2, AES.Error, AES.Envelope>:
628 AES.encrypt_checked(key, nonce, aad, plaintext,
629 AES.aad_valid(aad), plaintext_ok)
630
631def L.aes256gcm_rejects_invalid_plaintext(key, nonce, aad, plaintext, valid):
632 Equal.trans(Result<&2, &2, AES.Error, AES.Envelope>,
633 AES.encrypt_impl(key, nonce, aad, plaintext),
634 encrypt_using_plaintext_validity(key, nonce, aad, plaintext, False{}),
635 Fail{AES.InvalidBytes{}},
636 Equal.cong(Bool, Result<&2, &2, AES.Error, AES.Envelope>,
637 plaintext_ok => encrypt_using_plaintext_validity(
638 key, nonce, aad, plaintext, plaintext_ok),
639 AES.plaintext_valid(plaintext), False{}, valid),
640 encrypt_invalid_plaintext(key, nonce, aad, plaintext,
641 AES.aad_valid(aad)))
642
643def encrypt_invalid_aad(key: AES.SecretKey, nonce: AES.Nonce,
644 +aad: List<&2, U32>, +plaintext: List<&2, U32>, plaintext_ok: Bool) ->
645 {AES.encrypt_checked(key, nonce, aad, plaintext, False{}, plaintext_ok) ==
646 Fail{AES.InvalidBytes{}} : Result<&2, &2, AES.Error, AES.Envelope>}:
647 match plaintext_ok:
648 case True{}: {==}
649 case False{}: {==}
650
651def encrypt_using_aad_validity(key: AES.SecretKey, nonce: AES.Nonce,
652 +aad: List<&2, U32>, +plaintext: List<&2, U32>, aad_ok: Bool) ->
653 Result<&2, &2, AES.Error, AES.Envelope>:
654 AES.encrypt_checked(key, nonce, aad, plaintext, aad_ok,
655 AES.plaintext_valid(plaintext))
656
657def L.aes256gcm_rejects_invalid_aad(key, nonce, aad, plaintext, valid):
658 Equal.trans(Result<&2, &2, AES.Error, AES.Envelope>,
659 AES.encrypt_impl(key, nonce, aad, plaintext),
660 encrypt_using_aad_validity(key, nonce, aad, plaintext, False{}),
661 Fail{AES.InvalidBytes{}},
662 Equal.cong(Bool, Result<&2, &2, AES.Error, AES.Envelope>,
663 aad_ok => encrypt_using_aad_validity(key, nonce, aad, plaintext, aad_ok),
664 AES.aad_valid(aad), False{}, valid),
665 encrypt_invalid_aad(key, nonce, aad, plaintext,
666 AES.plaintext_valid(plaintext)))
667
668def decrypt_invalid_aad(key: AES.SecretKey, +aad: List<&2, U32>,
669 +envelope: AES.Envelope, ciphertext_ok: Bool) ->
670 {AES.decrypt_checked(key, aad, envelope, False{}, ciphertext_ok) ==
671 Fail{AES.InvalidBytes{}} :
672 Result<&2, &2, AES.Error, List<&2, U32>>}:
673 match ciphertext_ok:
674 case True{}: {==}
675 case False{}: {==}
676
677def decrypt_using_aad_validity(key: AES.SecretKey, +aad: List<&2, U32>,
678 +envelope: AES.Envelope, aad_ok: Bool) ->
679 Result<&2, &2, AES.Error, List<&2, U32>>:
680 AES.decrypt_checked(key, aad, envelope, aad_ok,
681 AES.plaintext_valid(AES.ciphertext(envelope)))
682
683def L.aes256gcm_decrypt_rejects_invalid_aad(key, aad, envelope, valid):
684 Equal.trans(Result<&2, &2, AES.Error, List<&2, U32>>,
685 AES.decrypt_impl(key, aad, envelope),
686 decrypt_using_aad_validity(key, aad, envelope, False{}),
687 Fail{AES.InvalidBytes{}},
688 Equal.cong(Bool, Result<&2, &2, AES.Error, List<&2, U32>>,
689 aad_ok => decrypt_using_aad_validity(key, aad, envelope, aad_ok),
690 AES.aad_valid(aad), False{}, valid),
691 decrypt_invalid_aad(key, aad, envelope,
692 AES.plaintext_valid(AES.ciphertext(envelope))))
693
694def L.aes256gcm_roundtrip(key, nonce, aad, plaintext, envelope, encrypted):
695 AESEncryptProof.successful_encrypt_decrypt_roundtrip(key, nonce, aad,
696 plaintext, envelope, encrypted)
697
698def L.aes256gcm_rejects_changed_tag(key, nonce, aad, plaintext, envelope,
699 tampered, encrypted, same_nonce, same_ciphertext, changed_tag):
700 AESTamperProof.rejects_changed_tag(key, nonce, aad, plaintext, envelope,
701 tampered, encrypted,
702 Equal.cong(AES.Nonce, List<&2, U32>, AES.raw_nonce_bytes,
703 AES.envelope_nonce(tampered), AES.envelope_nonce(envelope),
704 same_nonce), same_ciphertext, changed_tag)
705
706def L.aes256gcm_nist_canonical_encoding():
707 {==}
708
709def L.aes256gcm_nist_empty_encrypt():
710 AESNistInputProof.encrypt_inputs(L.aes256gcm_nist_key(), L.aes256gcm_nist_nonce(),
711 [], AESNistVectorProof.empty_aad(),
712 [], AESNistVectorProof.empty_plaintext(),
713 L.aes256gcm_nist_encrypt_observation(Done{L.aes256gcm_nist_empty()}),
714 {==}, {==}, AESNistVectorProof.empty_encrypt())
715
716def L.aes256gcm_nist_empty_decrypt():
717 AESNistInputProof.decrypt_inputs(L.aes256gcm_nist_key(), L.aes256gcm_nist_key(),
718 [], AESNistVectorProof.empty_aad(),
719 L.aes256gcm_nist_empty(), L.aes256gcm_nist_empty(), Done{AESNistVectorProof.empty_plaintext()},
720 {==}, {==}, {==}, AESNistVectorProof.empty_decrypt())
721
722def L.aes256gcm_nist_canonical_parsing():
723 {==}
724
725
726
727def aes256gcm_nist_j0_block_checkpoint() ->
728 {Core.aes256_encrypt_expanded(AESNistKeyScheduleProof.words_60(),
729 AESNistBlockProof.block()) ==
730 AESNistBlockProof.result() : List<&2, U32>}:
731 AESNistBlockComposeProof.expanded_block_matches()
732
733def L.aes256gcm_nist_multiblock_encrypt():
734 AESNistInputProof.encrypt_inputs(L.aes256gcm_nist_key(), L.aes256gcm_nist_nonce(),
735 [], AESNistVectorProof.multiblock_aad(),
736 [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], AESNistVectorProof.multiblock_plaintext(),
737 L.aes256gcm_nist_encrypt_observation(Done{L.aes256gcm_nist_multiblock()}),
738 {==}, {==}, AESNistVectorProof.multiblock_encrypt())
739
740def L.aes256gcm_nist_multiblock_decrypt():
741 AESNistInputProof.decrypt_inputs(L.aes256gcm_nist_key(), L.aes256gcm_nist_key(),
742 [], AESNistVectorProof.multiblock_aad(),
743 L.aes256gcm_nist_multiblock(), L.aes256gcm_nist_multiblock(), Done{AESNistVectorProof.multiblock_plaintext()},
744 {==}, {==}, {==}, AESNistVectorProof.multiblock_decrypt())
745
746def L.aes256gcm_nist_aad_only_encrypt():
747 AESNistInputProof.encrypt_inputs(L.aes256gcm_nist_key(), L.aes256gcm_nist_nonce(),
748 [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], AESNistVectorProof.aad_only_aad(),
749 [], AESNistVectorProof.aad_only_plaintext(),
750 L.aes256gcm_nist_encrypt_observation(Done{L.aes256gcm_nist_aad_only()}),
751 {==}, {==}, AESNistVectorProof.aad_only_encrypt())
752
753def L.aes256gcm_nist_aad_only_decrypt():
754 AESNistInputProof.decrypt_inputs(L.aes256gcm_nist_key(), L.aes256gcm_nist_key(),
755 [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], AESNistVectorProof.aad_only_aad(),
756 L.aes256gcm_nist_aad_only(), L.aes256gcm_nist_aad_only(), Done{AESNistVectorProof.aad_only_plaintext()},
757 {==}, {==}, {==}, AESNistVectorProof.aad_only_decrypt())
758
759def L.aes256gcm_nist_aad_and_multiblock_encrypt():
760 AESNistInputProof.encrypt_inputs(L.aes256gcm_nist_key(), L.aes256gcm_nist_nonce(),
761 [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], AESNistVectorProof.aad_and_multiblock_aad(),
762 [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], AESNistVectorProof.aad_and_multiblock_plaintext(),
763 L.aes256gcm_nist_encrypt_observation(Done{L.aes256gcm_nist_aad_and_multiblock()}),
764 {==}, {==}, AESNistVectorProof.aad_and_multiblock_encrypt())
765
766def L.aes256gcm_nist_aad_and_multiblock_decrypt():
767 AESNistInputProof.decrypt_inputs(L.aes256gcm_nist_key(), L.aes256gcm_nist_key(),
768 [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], AESNistVectorProof.aad_and_multiblock_aad(),
769 L.aes256gcm_nist_aad_and_multiblock(), L.aes256gcm_nist_aad_and_multiblock(), Done{AESNistVectorProof.aad_and_multiblock_plaintext()},
770 {==}, {==}, {==}, AESNistVectorProof.aad_and_multiblock_decrypt())
771
772def L.aes256gcm_nist_partial_block_encrypt():
773 AESNistInputProof.encrypt_inputs(L.aes256gcm_nist_key(), L.aes256gcm_nist_nonce(),
774 [58, 215, 123, 180, 13, 122, 54, 96, 168, 158, 202, 243, 36, 102, 239, 151, 245, 211, 213, 133], AESNistVectorProof.partial_block_aad(),
775 [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], AESNistVectorProof.partial_block_plaintext(),
776 L.aes256gcm_nist_encrypt_observation(Done{L.aes256gcm_nist_partial_block()}),
777 {==}, {==}, AESNistVectorProof.partial_block_encrypt())
778
779def L.aes256gcm_nist_partial_block_decrypt():
780 AESNistInputProof.decrypt_inputs(L.aes256gcm_nist_key(), L.aes256gcm_nist_key(),
781 [58, 215, 123, 180, 13, 122, 54, 96, 168, 158, 202, 243, 36, 102, 239, 151, 245, 211, 213, 133], AESNistVectorProof.partial_block_aad(),
782 L.aes256gcm_nist_partial_block(), L.aes256gcm_nist_partial_block(), Done{AESNistVectorProof.partial_block_plaintext()},
783 {==}, {==}, {==}, AESNistVectorProof.partial_block_decrypt())
784
785def L.aes256gcm_nist_rejects_changed_aad():
786 AESNistInputProof.decrypt_inputs(L.aes256gcm_nist_key(), L.aes256gcm_nist_key(),
787 [1], AESNistTamperVectorProof.changed_aad_aad(),
788 L.aes256gcm_nist_empty(), AESNistTamperVectorProof.changed_aad_envelope(),
789 Fail{AES.AuthenticationFailed{}}, {==}, {==}, {==},
790 AESNistTamperVectorProof.rejects_changed_aad())
791
792def L.aes256gcm_nist_rejects_changed_key():
793 AESNistInputProof.decrypt_inputs(AES.SecretKey{List.replicate(U32, 32n, 0), {==}, {==}}, AESNistTamperVectorProof.zero_key(),
794 [], AESNistTamperVectorProof.changed_key_aad(),
795 L.aes256gcm_nist_empty(), AESNistTamperVectorProof.changed_key_envelope(),
796 Fail{AES.AuthenticationFailed{}}, {==}, {==}, {==},
797 AESNistTamperVectorProof.rejects_changed_key())
798
799def L.aes256gcm_nist_rejects_changed_nonce():
800 AESNistInputProof.decrypt_inputs(L.aes256gcm_nist_key(), L.aes256gcm_nist_key(),
801 [], AESNistTamperVectorProof.changed_nonce_aad(),
802 AES.Envelope{AES.Nonce{List.replicate(U32, 12n, 0), {==}, {==}},
803 [], AES.Tag{[253, 44, 170, 22, 165, 131, 46, 118, 170, 19, 44, 20, 83, 238, 218, 126], {==}, {==}}, {==}}, AESNistTamperVectorProof.changed_nonce_envelope(),
804 Fail{AES.AuthenticationFailed{}}, {==}, {==}, {==},
805 AESNistTamperVectorProof.rejects_changed_nonce())
806
807def L.aes256gcm_nist_rejects_changed_ciphertext():
808 AESNistInputProof.decrypt_inputs(L.aes256gcm_nist_key(), L.aes256gcm_nist_key(),
809 [], AESNistTamperVectorProof.changed_ciphertext_aad(),
810 AES.Envelope{L.aes256gcm_nist_nonce(), [1],
811 AES.Tag{[253, 44, 170, 22, 165, 131, 46, 118, 170, 19, 44, 20, 83, 238, 218, 126], {==}, {==}}, {==}}, AESNistTamperVectorProof.changed_ciphertext_envelope(),
812 Fail{AES.AuthenticationFailed{}}, {==}, {==}, {==},
813 AESNistTamperVectorProof.rejects_changed_ciphertext())