~/bend-docscommunity

LAWS.bend open laws/TODOs

raw source on the hub · import qasim-bend-kit@0.1.0.2/LAWS.bend as LAWS

Library correctness laws and integration obligations.

4 imports
import Base
import ./libs/JSON.bend as Json
import ./libs/URL.bend as URL
import ./libs/AES256GCM.bend as AES

Laws

law stringify_parse_roundtrip openits proof in PROOF.bend does not pass the checker (timeout)source · line 19 · raw

@value:0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value -> {0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.parse(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.stringify(value)) == Done{value} : Result<&1, &1, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value>}

law parses_null openits proof in PROOF.bend does not pass the checker (timeout)source · line 32 · raw

{0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.parse("null") == Done{0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Null{}} : Result<&1, &1, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value>}

law parses_true openits proof in PROOF.bend does not pass the checker (timeout)source · line 36 · raw

{0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.parse("true") == Done{0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Bool{True{}}} : Result<&1, &1, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value>}

law parses_false openits proof in PROOF.bend does not pass the checker (timeout)source · line 40 · raw

{0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.parse("false") == Done{0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Bool{False{}}} : Result<&1, &1, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value>}

law accepts_leading_space openits proof in PROOF.bend does not pass the checker (timeout)source · line 48 · raw

@value:0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value -> {0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.parse(String.append(" ", 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.stringify(value))) == Done{value} : Result<&1, &1, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value>}

law accepts_trailing_space openits proof in PROOF.bend does not pass the checker (timeout)source · line 54 · raw

@value:0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value -> {0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.parse(String.append(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.stringify(value), " ")) == Done{value} : Result<&1, &1, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value>}

law accepts_surrounding_space openits proof in PROOF.bend does not pass the checker (timeout)source · line 60 · raw

@value:0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value -> {0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.parse(String.append(" \n\t\r", String.append(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.stringify(value), "\r\t\n "))) == Done{value} : Result<&1, &1, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value>}

law rejects_trailing_garbage openits proof in PROOF.bend does not pass the checker (timeout)source · line 70 · raw

{Result.is_fail(&1, &1, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.parse("nullx")) == True{} : Bool}

law rejects_second_value openits proof in PROOF.bend does not pass the checker (timeout)source · line 74 · raw

{Result.is_fail(&1, &1, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.parse("null true")) == True{} : Bool}

law rejects_invalid_null openits proof in PROOF.bend does not pass the checker (timeout)source · line 78 · raw

{Result.is_fail(&1, &1, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.parse("nul")) == True{} : Bool}

law rejects_invalid_true openits proof in PROOF.bend does not pass the checker (timeout)source · line 82 · raw

{Result.is_fail(&1, &1, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.parse("tru")) == True{} : Bool}

law rejects_invalid_false openits proof in PROOF.bend does not pass the checker (timeout)source · line 86 · raw

{Result.is_fail(&1, &1, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.parse("fals")) == True{} : Bool}

law rejects_empty_input openits proof in PROOF.bend does not pass the checker (timeout)source · line 90 · raw

{Result.is_fail(&1, &1, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.parse("")) == True{} : Bool}

law rejects_whitespace_only openits proof in PROOF.bend does not pass the checker (timeout)source · line 94 · raw

{Result.is_fail(&1, &1, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.parse(" \t\r\n ")) == True{} : Bool}

law parses_empty_string openits proof in PROOF.bend does not pass the checker (timeout)source · line 102 · raw

{0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.parse("\"\"") == Done{0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Str{""}} : Result<&1, &1, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value>}

law parses_simple_string openits proof in PROOF.bend does not pass the checker (timeout)source · line 106 · raw

{0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.parse("\"hello\"") == Done{0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Str{"hello"}} : Result<&1, &1, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value>}

law parses_newline_escape openits proof in PROOF.bend does not pass the checker (timeout)source · line 110 · raw

{0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.parse("\"a\\nb\"") == Done{0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Str{"a\nb"}} : Result<&1, &1, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value>}

law parses_quote_escape openits proof in PROOF.bend does not pass the checker (timeout)source · line 114 · raw

{0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.parse("\"a\\\"b\"") == Done{0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Str{"a\"b"}} : Result<&1, &1, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value>}

law parses_backslash_escape openits proof in PROOF.bend does not pass the checker (timeout)source · line 118 · raw

{0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.parse("\"a\\\\b\"") == Done{0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Str{"a\\b"}} : Result<&1, &1, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value>}

law rejects_unterminated_string openits proof in PROOF.bend does not pass the checker (timeout)source · line 122 · raw

{Result.is_fail(&1, &1, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.parse("\"hello")) == True{} : Bool}

law parses_empty_array openits proof in PROOF.bend does not pass the checker (timeout)source · line 130 · raw

{0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.parse("[]") == Done{0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Arr{[]}} : Result<&1, &1, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value>}

law parses_literal_array openits proof in PROOF.bend does not pass the checker (timeout)source · line 134 · raw

{0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.parse("[null,true,false]") == Done{0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Arr{[0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Null{}, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Bool{True{}}, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Bool{False{}}]}} : Result<&1, &1, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value>}

law rejects_array_trailing_comma openits proof in PROOF.bend does not pass the checker (timeout)source · line 148 · raw

{Result.is_fail(&1, &1, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.parse("[null,]")) == True{} : Bool}

law parses_empty_object openits proof in PROOF.bend does not pass the checker (timeout)source · line 156 · raw

{0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.parse("{}") == Done{0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Obj{[]}} : Result<&1, &1, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value>}

law rejects_unquoted_object_key openits proof in PROOF.bend does not pass the checker (timeout)source · line 160 · raw

{Result.is_fail(&1, &1, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.parse("{foo:null}")) == True{} : Bool}

law rejects_object_trailing_comma openits proof in PROOF.bend does not pass the checker (timeout)source · line 164 · raw

{Result.is_fail(&1, &1, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.parse("{\"x\":null,}")) == True{} : Bool}

law parses_nested_containers openits proof in PROOF.bend does not pass the checker (timeout)source · line 172 · raw

{0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.parse("[{\"x\":[true,null]}]") == Done{0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Arr{[0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Obj{[("x", 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Arr{[0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Bool{True{}}, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Null{}]})]}]}} : Result<&1, &1, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value>}

law rejects_non_json_whitespace openits proof in PROOF.bend does not pass the checker (timeout)source · line 196 · raw

{Result.is_fail(&1, &1, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.parse("\u{b}null")) == True{} : Bool}

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

law rejects_raw_string_control openits proof in PROOF.bend does not pass the checker (timeout)source · line 201 · raw

{Result.is_fail(&1, &1, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.parse(String.append("\"", String.append("\u{1}", "\"")))) == True{} : Bool}

A raw control character is forbidden inside a JSON string.

law parses_unicode_escape openits proof in PROOF.bend does not pass the checker (timeout)source · line 207 · raw

{0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.parse("\"\\u263A\"") == Done{0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Str{"☺"}} : Result<&1, &1, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value>}

Unicode escapes decode to their scalar value, including a surrogate pair.

law parses_unicode_surrogate_pair openits proof in PROOF.bend does not pass the checker (timeout)source · line 211 · raw

{0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.parse("\"\\uD83D\\uDE00\"") == Done{0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Str{"😀"}} : Result<&1, &1, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value>}

law parses_fraction_and_exponent openits proof in PROOF.bend does not pass the checker (timeout)source · line 217 · raw

{Result.is_done(&1, &1, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.parse("-12.50e+3")) == True{} : Bool}

This representative decimal/exponent form is accepted. A separate law below checks that the smart number constructor preserves the original lexeme.

law rejects_malformed_number_forms openits proof in PROOF.bend does not pass the checker (timeout)source · line 221 · raw

{Bool.and(Bool.and(Result.is_fail(&1, &1, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.parse("01")), Result.is_fail(&1, &1, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.parse("1."))), Result.is_fail(&1, &1, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.parse("1e+"))) == True{} : Bool}

law preserves_array_order openits proof in PROOF.bend does not pass the checker (timeout)source · line 229 · raw

{0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.parse("[3,1,2]") == Done{0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Arr{[0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Number{"3", 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Certified{0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.number_proof("3", {==})}}, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Number{"1", 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Certified{0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.number_proof("1", {==})}}, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Number{"2", 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Certified{0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.number_proof("2", {==})}}]}} : Result<&1, &1, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value>}

Arrays retain source order. Objects retain source order and duplicate keys; consumers that need map semantics must choose their own duplicate-key policy.

law preserves_object_order_and_duplicates openits proof in PROOF.bend does not pass the checker (timeout)source · line 237 · raw

{0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.parse("{\"x\":1,\"x\":2}") == Done{0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Obj{[("x", 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Number{"1", 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Certified{0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.number_proof("1", {==})}}), ("x", 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Number{"2", 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Certified{0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.number_proof("2", {==})}})]}} : Result<&1, &1, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value>}

law gpu_single_matches_cpu openits proof in PROOF.bend does not pass the checker (timeout)source · line 245 · raw

@text:String -> {0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.parse_gpu(text) == 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.parse(text) : Result<&1, &1, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value>}

GPU entry points have the same specified results as their CPU counterparts.

law preserves_number_lexeme openits proof in PROOF.bend does not pass the checker (timeout)source · line 251 · raw

{0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.number("-12.50e+3") == Done{0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Number{"-12.50e+3", 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Certified{0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.number_proof("-12.50e+3", {==})}}} : Result<&1, &1, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value>}

law gpu_batch_matches_cpu openits proof in PROOF.bend does not pass the checker (timeout)source · line 257 · raw

@batch:0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Batch -> {0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.parse_batch_gpu(batch) == 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.parse_batch(batch) : 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.BatchResult}

law url_component_ascii openits proof in PROOF.bend does not pass the checker (timeout)source · line 267 · raw

{0xaca801afcf3e822677fd6d06895d2c71/libs/URL.percent_component("A") == "%41" : String}

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

law url_component_reserved openits proof in PROOF.bend does not pass the checker (timeout)source · line 270 · raw

{0xaca801afcf3e822677fd6d06895d2c71/libs/URL.percent_component("/") == "%2F" : String}

law url_component_utf8 openits proof in PROOF.bend does not pass the checker (timeout)source · line 273 · raw

{0xaca801afcf3e822677fd6d06895d2c71/libs/URL.percent_component("é") == "%C3%A9" : String}

law aes256gcm_accepts_32_byte_key openits proof in PROOF.bend does not pass the checker (timeout)source · line 281 · raw

@+bytes:List<&2, U32> -> @size:{List.length(&2, U32, bytes) == 32n : Nat} -> @valid:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.bytes_valid(bytes) == True{} : Bool} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.key(bytes) == Done{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.SecretKey{bytes, size, valid}} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.SecretKey>}

law aes256gcm_rejects_wrong_key_length openits proof in PROOF.bend does not pass the checker (timeout)source · line 288 · raw

@+bytes:List<&2, U32> -> @size:(@_:{List.length(&2, U32, bytes) == 32n : Nat} -> Empty) -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.key(bytes) == Fail{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.InvalidKey{}} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.SecretKey>}

law aes256gcm_rejects_non_byte_key openits proof in PROOF.bend does not pass the checker (timeout)source · line 294 · raw

@+bytes:List<&2, U32> -> @valid:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.bytes_valid(bytes) == False{} : Bool} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.key(bytes) == Fail{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.InvalidKey{}} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.SecretKey>}

law aes256gcm_accepts_12_byte_nonce openits proof in PROOF.bend does not pass the checker (timeout)source · line 300 · raw

@+bytes:List<&2, U32> -> @size:{List.length(&2, U32, bytes) == 12n : Nat} -> @valid:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.bytes_valid(bytes) == True{} : Bool} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.nonce(bytes) == Done{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Nonce{bytes, size, valid}} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Nonce>}

law aes256gcm_rejects_wrong_nonce_length openits proof in PROOF.bend does not pass the checker (timeout)source · line 307 · raw

@+bytes:List<&2, U32> -> @size:(@_:{List.length(&2, U32, bytes) == 12n : Nat} -> Empty) -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.nonce(bytes) == Fail{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.InvalidNonce{}} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Nonce>}

law aes256gcm_rejects_non_byte_nonce openits proof in PROOF.bend does not pass the checker (timeout)source · line 313 · raw

@+bytes:List<&2, U32> -> @valid:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.bytes_valid(bytes) == False{} : Bool} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.nonce(bytes) == Fail{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.InvalidNonce{}} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Nonce>}

law aes256gcm_encrypts_valid_input openits proof in PROOF.bend does not pass the checker (timeout)source · line 324 · raw

@key:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.SecretKey -> @nonce:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Nonce -> @aad:List<&2, U32> -> @plaintext:List<&2, U32> -> @aad_ok:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.aad_valid(aad) == True{} : Bool} -> @plaintext_ok:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.plaintext_valid(plaintext) == True{} : Bool} -> {Result.is_done(&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encrypt(key, nonce, aad, plaintext)) == True{} : Bool}

This prevents satisfying the conditional roundtrip by always failing.

law aes256gcm_rejects_invalid_plaintext openits proof in PROOF.bend does not pass the checker (timeout)source · line 334 · raw

@+key:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.SecretKey -> @+nonce:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Nonce -> @+aad:List<&2, U32> -> @+plaintext:List<&2, U32> -> @valid:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.plaintext_valid(plaintext) == False{} : Bool} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encrypt(key, nonce, aad, plaintext) == Fail{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.InvalidBytes{}} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope>}

law aes256gcm_rejects_invalid_aad openits proof in PROOF.bend does not pass the checker (timeout)source · line 343 · raw

@+key:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.SecretKey -> @+nonce:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Nonce -> @+aad:List<&2, U32> -> @+plaintext:List<&2, U32> -> @valid:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.aad_valid(aad) == False{} : Bool} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encrypt(key, nonce, aad, plaintext) == Fail{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.InvalidBytes{}} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope>}

law aes256gcm_decrypt_rejects_invalid_aad openits proof in PROOF.bend does not pass the checker (timeout)source · line 352 · raw

@+key:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.SecretKey -> @+aad:List<&2, U32> -> @+envelope:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope -> @valid:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.aad_valid(aad) == False{} : Bool} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.decrypt(key, aad, envelope) == Fail{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.InvalidBytes{}} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, List<&2, U32>>}

law aes256gcm_roundtrip openits proof in PROOF.bend does not pass the checker (timeout)source · line 360 · raw

@+key:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.SecretKey -> @+nonce:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Nonce -> @+aad:List<&2, U32> -> @+plaintext:List<&2, U32> -> @+envelope:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope -> @encrypted:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encrypt(key, nonce, aad, plaintext) == Done{envelope} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope>} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.decrypt(key, aad, envelope) == Done{plaintext} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, List<&2, U32>>}

law aes256gcm_preserves_nonce openits proof in PROOF.bend does not pass the checker (timeout)source · line 371 · raw

@+key:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.SecretKey -> @+nonce:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Nonce -> @+aad:List<&2, U32> -> @+plaintext:List<&2, U32> -> @+envelope:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope -> @encrypted:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encrypt(key, nonce, aad, plaintext) == Done{envelope} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope>} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.envelope_nonce(envelope) == nonce : 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Nonce}

law aes256gcm_preserves_plaintext_length openits proof in PROOF.bend does not pass the checker (timeout)source · line 381 · raw

@+key:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.SecretKey -> @+nonce:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Nonce -> @+aad:List<&2, U32> -> @+plaintext:List<&2, U32> -> @+envelope:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope -> @encrypted:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encrypt(key, nonce, aad, plaintext) == Done{envelope} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope>} -> {List.length(&2, U32, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.ciphertext(envelope)) == List.length(&2, U32, plaintext) : Nat}

law aes256gcm_rejects_changed_tag openits proof in PROOF.bend does not pass the checker (timeout)source · line 395 · raw

@+key:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.SecretKey -> @+nonce:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Nonce -> @+aad:List<&2, U32> -> @+plaintext:List<&2, U32> -> @+envelope:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope -> @+tampered:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope -> @encrypted:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encrypt(key, nonce, aad, plaintext) == Done{envelope} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope>} -> @same_nonce:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.envelope_nonce(tampered) == 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.envelope_nonce(envelope) : 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Nonce} -> @same_ciphertext:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.ciphertext(tampered) == 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.ciphertext(envelope) : List<&2, U32>} -> @changed_tag:(@_:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.tag_bytes(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.envelope_tag(tampered)) == 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.tag_bytes(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.envelope_tag(envelope)) : List<&2, U32>} -> Empty) -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.decrypt(key, aad, tampered) == Fail{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.AuthenticationFailed{}} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, List<&2, U32>>}

For fixed key, nonce, AAD, and ciphertext there is exactly one valid tag. Different ciphertext/AAD/key/nonce can collide in a finite tag space; do not claim that every possible change to those fields is mathematically rejected.

law aes256gcm_envelope_roundtrip openits proof in PROOF.bend does not pass the checker (timeout)source · line 417 · raw

@+envelope:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.parse(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encode(envelope)) == Done{envelope} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope>}

law aes256gcm_envelope_is_canonical openits proof in PROOF.bend does not pass the checker (timeout)source · line 422 · raw

@+text:String -> @+envelope:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope -> @parsed:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.parse(text) == Done{envelope} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope>} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encode(envelope) == text : String}

law aes256gcm_rejects_empty_envelope openits proof in PROOF.bend does not pass the checker (timeout)source · line 429 · raw

{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.parse("") == Fail{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.InvalidEnvelope{}} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope>}

law aes256gcm_rejects_unknown_version openits proof in PROOF.bend does not pass the checker (timeout)source · line 433 · raw

{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.parse("v2.cafebabefacedbaddecaf888.fd2caa16a5832e76aa132c1453eeda7e.") == Fail{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.InvalidEnvelope{}} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope>}

law aes256gcm_rejects_missing_version openits proof in PROOF.bend does not pass the checker (timeout)source · line 437 · raw

{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.parse("cafebabefacedbaddecaf888.fd2caa16a5832e76aa132c1453eeda7e.") == Fail{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.InvalidEnvelope{}} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope>}

law aes256gcm_rejects_short_nonce openits proof in PROOF.bend does not pass the checker (timeout)source · line 441 · raw

{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.parse("v1.cafebabefacedbaddecaf8.fd2caa16a5832e76aa132c1453eeda7e.") == Fail{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.InvalidEnvelope{}} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope>}

law aes256gcm_rejects_long_nonce openits proof in PROOF.bend does not pass the checker (timeout)source · line 445 · raw

{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.parse("v1.cafebabefacedbaddecaf88800.fd2caa16a5832e76aa132c1453eeda7e.") == Fail{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.InvalidEnvelope{}} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope>}

law aes256gcm_rejects_short_tag openits proof in PROOF.bend does not pass the checker (timeout)source · line 449 · raw

{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.parse("v1.cafebabefacedbaddecaf888.fd2caa16a5832e76aa132c1453eeda.") == Fail{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.InvalidEnvelope{}} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope>}

law aes256gcm_rejects_long_tag openits proof in PROOF.bend does not pass the checker (timeout)source · line 453 · raw

{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.parse("v1.cafebabefacedbaddecaf888.fd2caa16a5832e76aa132c1453eeda7e00.") == Fail{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.InvalidEnvelope{}} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope>}

law aes256gcm_rejects_odd_ciphertext_hex openits proof in PROOF.bend does not pass the checker (timeout)source · line 457 · raw

{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.parse("v1.cafebabefacedbaddecaf888.fd2caa16a5832e76aa132c1453eeda7e.0") == Fail{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.InvalidEnvelope{}} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope>}

law aes256gcm_rejects_non_hex_ciphertext openits proof in PROOF.bend does not pass the checker (timeout)source · line 461 · raw

{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.parse("v1.cafebabefacedbaddecaf888.fd2caa16a5832e76aa132c1453eeda7e.gg") == Fail{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.InvalidEnvelope{}} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope>}

law aes256gcm_rejects_non_hex_nonce openits proof in PROOF.bend does not pass the checker (timeout)source · line 465 · raw

{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.parse("v1.zzfebabefacedbaddecaf888.fd2caa16a5832e76aa132c1453eeda7e.") == Fail{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.InvalidEnvelope{}} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope>}

law aes256gcm_rejects_non_hex_tag openits proof in PROOF.bend does not pass the checker (timeout)source · line 469 · raw

{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.parse("v1.cafebabefacedbaddecaf888.zz2caa16a5832e76aa132c1453eeda7e.") == Fail{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.InvalidEnvelope{}} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope>}

law aes256gcm_rejects_uppercase_hex openits proof in PROOF.bend does not pass the checker (timeout)source · line 473 · raw

{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.parse("v1.CAFEBABEFACEDBADDECAF888.fd2caa16a5832e76aa132c1453eeda7e.") == Fail{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.InvalidEnvelope{}} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope>}

law aes256gcm_rejects_extra_field openits proof in PROOF.bend does not pass the checker (timeout)source · line 477 · raw

{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.parse("v1.cafebabefacedbaddecaf888.fd2caa16a5832e76aa132c1453eeda7e..") == Fail{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.InvalidEnvelope{}} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope>}

law aes256gcm_rejects_missing_ciphertext_field openits proof in PROOF.bend does not pass the checker (timeout)source · line 481 · raw

{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.parse("v1.cafebabefacedbaddecaf888.fd2caa16a5832e76aa132c1453eeda7e") == Fail{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.InvalidEnvelope{}} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope>}

law aes256gcm_rejects_trailing_garbage openits proof in PROOF.bend does not pass the checker (timeout)source · line 485 · raw

{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.parse("v1.cafebabefacedbaddecaf888.fd2caa16a5832e76aa132c1453eeda7e.00!") == Fail{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.InvalidEnvelope{}} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope>}

law aes256gcm_rejects_surrounding_whitespace openits proof in PROOF.bend does not pass the checker (timeout)source · line 489 · raw

{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.parse(" v1.cafebabefacedbaddecaf888.fd2caa16a5832e76aa132c1453eeda7e. ") == Fail{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.InvalidEnvelope{}} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope>}

law aes256gcm_nist_empty_encrypt openits proof in PROOF.bend does not pass the checker (timeout)source · line 524 · raw

{aes256gcm_nist_encrypt_observation(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encrypt(aes256gcm_nist_key, aes256gcm_nist_nonce, [], [])) == aes256gcm_nist_encrypt_observation(Done{aes256gcm_nist_empty}) : List<&2, U32>}

law aes256gcm_nist_empty_decrypt openits proof in PROOF.bend does not pass the checker (timeout)source · line 529 · raw

{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.decrypt(aes256gcm_nist_key, [], aes256gcm_nist_empty) == Done{[]} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, List<&2, U32>>}

law aes256gcm_nist_multiblock_encrypt openits proof in PROOF.bend does not pass the checker (timeout)source · line 538 · raw

{aes256gcm_nist_encrypt_observation(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encrypt(aes256gcm_nist_key, aes256gcm_nist_nonce, [], [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}) : List<&2, U32>}

law aes256gcm_nist_multiblock_decrypt openits proof in PROOF.bend does not pass the checker (timeout)source · line 543 · raw

{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.decrypt(aes256gcm_nist_key, [], 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]} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, List<&2, U32>>}

law aes256gcm_nist_aad_only_encrypt openits proof in PROOF.bend does not pass the checker (timeout)source · line 552 · raw

{aes256gcm_nist_encrypt_observation(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encrypt(aes256gcm_nist_key, aes256gcm_nist_nonce, [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}) : List<&2, U32>}

law aes256gcm_nist_aad_only_decrypt openits proof in PROOF.bend does not pass the checker (timeout)source · line 557 · raw

{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.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], aes256gcm_nist_aad_only) == Done{[]} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, List<&2, U32>>}

law aes256gcm_nist_aad_and_multiblock_encrypt openits proof in PROOF.bend does not pass the checker (timeout)source · line 566 · raw

{aes256gcm_nist_encrypt_observation(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encrypt(aes256gcm_nist_key, aes256gcm_nist_nonce, [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}) : List<&2, U32>}

law aes256gcm_nist_aad_and_multiblock_decrypt openits proof in PROOF.bend does not pass the checker (timeout)source · line 571 · raw

{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.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], 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]} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, List<&2, U32>>}

law aes256gcm_nist_partial_block_encrypt openits proof in PROOF.bend does not pass the checker (timeout)source · line 580 · raw

{aes256gcm_nist_encrypt_observation(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encrypt(aes256gcm_nist_key, aes256gcm_nist_nonce, [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}) : List<&2, U32>}

law aes256gcm_nist_partial_block_decrypt openits proof in PROOF.bend does not pass the checker (timeout)source · line 585 · raw

{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.decrypt(aes256gcm_nist_key, [58, 215, 123, 180, 13, 122, 54, 96, 168, 158, 202, 243, 36, 102, 239, 151, 245, 211, 213, 133], 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]} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, List<&2, U32>>}

law aes256gcm_nist_canonical_encoding openits proof in PROOF.bend does not pass the checker (timeout)source · line 590 · raw

{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encode(aes256gcm_nist_empty) == "v1.cafebabefacedbaddecaf888.fd2caa16a5832e76aa132c1453eeda7e." : String}

law aes256gcm_nist_canonical_parsing openits proof in PROOF.bend does not pass the checker (timeout)source · line 593 · raw

{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.parse("v1.cafebabefacedbaddecaf888.fd2caa16a5832e76aa132c1453eeda7e.") == Done{aes256gcm_nist_empty} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope>}

law aes256gcm_nist_rejects_changed_aad openits proof in PROOF.bend does not pass the checker (timeout)source · line 599 · raw

{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.decrypt(aes256gcm_nist_key, [1], aes256gcm_nist_empty) == Fail{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.AuthenticationFailed{}} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, List<&2, U32>>}

Concrete tamper checks supplement tag uniqueness without claiming collision- free authentication for all distinct AAD, nonce, key, or ciphertext inputs.

law aes256gcm_nist_rejects_changed_key openits proof in PROOF.bend does not pass the checker (timeout)source · line 604 · raw

{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.decrypt(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.SecretKey{List.replicate(U32, 32n, 0), {==}, {==}}, [], aes256gcm_nist_empty) == Fail{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.AuthenticationFailed{}} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, List<&2, U32>>}

law aes256gcm_nist_rejects_changed_nonce openits proof in PROOF.bend does not pass the checker (timeout)source · line 609 · raw

{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.decrypt(aes256gcm_nist_key, [], 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Nonce{List.replicate(U32, 12n, 0), {==}, {==}}, [], 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Tag{[253, 44, 170, 22, 165, 131, 46, 118, 170, 19, 44, 20, 83, 238, 218, 126], {==}, {==}}, {==}}) == Fail{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.AuthenticationFailed{}} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, List<&2, U32>>}

law aes256gcm_nist_rejects_changed_ciphertext openits proof in PROOF.bend does not pass the checker (timeout)source · line 616 · raw

{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.decrypt(aes256gcm_nist_key, [], 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope{aes256gcm_nist_nonce, [1], 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Tag{[253, 44, 170, 22, 165, 131, 46, 118, 170, 19, 44, 20, 83, 238, 218, 126], {==}, {==}}, {==}}) == Fail{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.AuthenticationFailed{}} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, List<&2, U32>>}

Definitions

def aes256gcm_nist_key source · line 500 · raw

0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.SecretKey

def aes256gcm_nist_nonce source · line 503 · raw

0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Nonce

def aes256gcm_nist_empty source · line 506 · raw

0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope

def aes256gcm_nist_encrypt_observation source · line 512 · raw

@result:Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope> -> List<&2, U32>

Compare the protocol-visible result while leaving internal certificate terms out of the NIST contract: success, nonce bytes, ciphertext, and tag bytes.

def aes256gcm_nist_multiblock source · line 534 · raw

0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope

def aes256gcm_nist_aad_only source · line 548 · raw

0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope

def aes256gcm_nist_aad_and_multiblock source · line 562 · raw

0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope

def aes256gcm_nist_partial_block source · line 576 · raw

0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope