1 import Base 2 import ./proof/AES_NistInputProof.bend as AESNistInputProof 3 import ./LAWS.bend as L 4 import ./libs/JSON.bend as Json 5 import ./libs/URL.bend as URL 6 import ./libs/AES256GCM.bend as AES 7 import ./libs/AES256GCMCore.bend as Core 8 import ./proof/AES_EncryptProof.bend as AESEncryptProof 9 import ./proof/AES_TamperProof.bend as AESTamperProof 10 import ./proof/AES_CanonicalProof.bend as AESCanonicalProof 11 import ./proof/AES_ConstructorProof.bend as AESConstructorProof 12 import ./proof/AES_IdentityProof.bend as AESIdentityProof 13 import ./proof/AES_NistKeyScheduleProof.bend as AESNistKeyScheduleProof 14 import ./proof/AES_NistBlockComposeProof.bend as AESNistBlockComposeProof 15 import ./proof/AES_NistBlockProof.bend as AESNistBlockProof 16 import ./proof/AES_NistObservationProof.bend as AESNistObservationProof 17 import ./proof/AES_NistVectorProof.bend as AESNistVectorProof 18 import ./proof/AES_NistTamperVectorProof.bend as AESNistTamperVectorProof 19 import ./proof/JSON_StringProof.bend as StringProof 20 import ./proof/JSON_PrimitiveProof.bend as PrimitiveProof 21 import ./proof/JSON_NumberLexProof.bend as NumberLexProof 22 import ./proof/JSON_ParallelProof.bend as ParallelProof 23 import ./proof/JSON_LexWhitespaceProof.bend as LexWhitespaceProof 24 import ./proof/JSON_AssemblyProof.bend as AssemblyProof 25 import ./proof/JSON_SourceProof.bend as SourceProof 26 import ./proof/JSON_RenderLexProof.bend as RenderLexProof 27 28 def ResultValue() -> Type: 29 Result<&1, &1, Json.Error, Json.Value> 30 31 def parse_for_equality(text: String) -> ResultValue(): 32 Json.parse(text) 33 34 def 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 39 def 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}: 40 Equal.trans(List, 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 44 def 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, 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, 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, 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, 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 71 def parse_number_payload(+text: String, 72 +certificate: Json.NumberCert) -> {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, 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 96 def 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 100 def 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, 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 118 def parse_leading_space(+text: String) -> {Json.parse(" " ++ text) == Json.parse(text) : Result<&1, &1, Json.Error, Json.Value>}: 119 {==} 120 121 def 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 128 def 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 135 def 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 142 def 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 149 def 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 156 def 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 163 def 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 170 def 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 177 def parse_leading_surround(+text: String) -> {Json.parse(" \n\t\r" ++ text) == Json.parse(text) : Result<&1, &1, Json.Error, Json.Value>}: 178 {==} 179 180 def 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 190 def L.parses_null(): 191 {==} 192 193 def L.parses_true(): 194 {==} 195 196 def L.parses_false(): 197 {==} 198 199 def L.rejects_trailing_garbage(): 200 {==} 201 202 def L.rejects_second_value(): 203 {==} 204 205 def L.rejects_invalid_null(): 206 {==} 207 208 def L.rejects_invalid_true(): 209 {==} 210 211 def L.rejects_invalid_false(): 212 {==} 213 214 def L.rejects_empty_input(): 215 {==} 216 217 def L.rejects_whitespace_only(): 218 {==} 219 220 def L.parses_empty_string(): 221 {==} 222 223 def L.parses_simple_string(): 224 {==} 225 226 def L.parses_newline_escape(): 227 {==} 228 229 def L.parses_quote_escape(): 230 {==} 231 232 def L.parses_backslash_escape(): 233 {==} 234 235 def L.rejects_unterminated_string(): 236 {==} 237 238 def L.parses_empty_array(): 239 {==} 240 241 def L.parses_literal_array(): 242 {==} 243 244 def L.rejects_array_trailing_comma(): 245 {==} 246 247 def L.parses_empty_object(): 248 {==} 249 250 def L.rejects_unquoted_object_key(): 251 {==} 252 253 def L.rejects_object_trailing_comma(): 254 {==} 255 256 def L.parses_nested_containers(): 257 {==} 258 259 def L.rejects_non_json_whitespace(): 260 {==} 261 262 def L.rejects_raw_string_control(): 263 {==} 264 265 def L.parses_unicode_escape(): 266 {==} 267 268 def L.parses_unicode_surrogate_pair(): 269 {==} 270 271 def L.parses_fraction_and_exponent(): 272 {==} 273 274 def L.rejects_malformed_number_forms(): 275 {==} 276 277 def L.preserves_array_order(): 278 {==} 279 280 def L.preserves_object_order_and_duplicates(): 281 {==} 282 283 def L.gpu_single_matches_cpu(text): 284 {==} 285 286 def L.preserves_number_lexeme(): 287 {==} 288 289 def L.gpu_batch_matches_cpu(batch): 290 {==} 291 292 def 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 303 def 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 307 def 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 311 def 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 315 def L.url_component_ascii(): 316 {==} 317 318 def L.url_component_reserved(): 319 {==} 320 321 def L.url_component_utf8(): 322 {==} 323 324 def L.aes256gcm_rejects_empty_envelope(): 325 {==} 326 327 def L.aes256gcm_rejects_unknown_version(): 328 {==} 329 330 def L.aes256gcm_rejects_missing_version(): 331 {==} 332 333 def L.aes256gcm_rejects_short_nonce(): 334 {==} 335 336 def L.aes256gcm_rejects_long_nonce(): 337 {==} 338 339 def L.aes256gcm_rejects_short_tag(): 340 {==} 341 342 def L.aes256gcm_rejects_long_tag(): 343 {==} 344 345 def L.aes256gcm_rejects_odd_ciphertext_hex(): 346 {==} 347 348 def L.aes256gcm_rejects_non_hex_ciphertext(): 349 {==} 350 351 def L.aes256gcm_rejects_non_hex_nonce(): 352 {==} 353 354 def L.aes256gcm_rejects_non_hex_tag(): 355 {==} 356 357 def L.aes256gcm_rejects_uppercase_hex(): 358 {==} 359 360 def L.aes256gcm_rejects_extra_field(): 361 {==} 362 363 def L.aes256gcm_rejects_missing_ciphertext_field(): 364 {==} 365 366 def L.aes256gcm_rejects_trailing_garbage(): 367 {==} 368 369 def L.aes256gcm_rejects_surrounding_whitespace(): 370 {==} 371 372 def 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 376 def aes_nat_pred(n: Nat) -> Nat: 377 match n: 378 case 0n: 0n 379 case 1n+p: p 380 381 def 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 387 def 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 393 def 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 402 def 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 417 def 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)) 429 def 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 450 def 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 466 def 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 473 def 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 481 def 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) 491 def 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 500 def 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 509 def 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 514 def L.aes256gcm_preserves_nonce(key, nonce, aad, plaintext, envelope, 515 encrypted): 516 AESEncryptProof.preserves_nonce(key, nonce, aad, plaintext, envelope, 517 encrypted) 518 519 def 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 524 def 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 528 def L.aes256gcm_envelope_roundtrip(envelope): 529 AESIdentityProof.exact_roundtrip(envelope) 530 531 def 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 537 def 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 545 def 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 558 def 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 574 def 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 580 def 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 588 def 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 601 def 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 617 def 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 625 def 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 631 def 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 643 def 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 651 def 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 657 def 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 668 def 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 677 def 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 683 def 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 694 def L.aes256gcm_roundtrip(key, nonce, aad, plaintext, envelope, encrypted): 695 AESEncryptProof.successful_encrypt_decrypt_roundtrip(key, nonce, aad, 696 plaintext, envelope, encrypted) 697 698 def 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 706 def L.aes256gcm_nist_canonical_encoding(): 707 {==} 708 709 def 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 716 def 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 722 def L.aes256gcm_nist_canonical_parsing(): 723 {==} 724 725 # Keep the composed NIST AES block certificate in the law proof book. This 726 # checkpoint proves the exact J0 AES result used by the empty-message vector. 727 def 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 733 def 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 740 def 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 746 def 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 753 def 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 759 def 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 766 def 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 772 def 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 779 def 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 785 def 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 792 def 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 799 def 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 807 def 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())