qasim-bend-kit

Releases (2):
  0.1.0.2  0xaca801afcf3e822677fd6d06895d2c71  indexed  https://jend.leeeet.dev/files.txt?path=qasim-bend-kit@0.1.0.2
  0.1.0.1  0x0b4f68372ee8cbe03f4a66931f85cfdc  unindexed  https://jend.leeeet.dev/files.txt?path=qasim-bend-kit@0.1.0.1

Definitions (1592, 1 to 100 shown):
  LAWS.stringify_parse_roundtrip (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=stringify_parse_roundtrip)
   law stringify_parse_roundtrip:
       for value: Json.Value {
           Json.parse(Json.stringify(value))
           ==
           Done{value}
           :
           Result<&1, &1, Json.Error, Json.Value>
       }
  LAWS.parses_null (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=parses_null)
   law parses_null:
       { Json.parse("null") == Done{Json.Null{}} :
           Result<&1, &1, Json.Error, Json.Value> }
  LAWS.parses_true (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=parses_true)
   law parses_true:
       { Json.parse("true") == Done{Json.Bool{True{}}} :
           Result<&1, &1, Json.Error, Json.Value> }
  LAWS.parses_false (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=parses_false)
   law parses_false:
       { Json.parse("false") == Done{Json.Bool{False{}}} :
           Result<&1, &1, Json.Error, Json.Value> }
  LAWS.accepts_leading_space (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=accepts_leading_space)
   law accepts_leading_space:
       for value: Json.Value {
           Json.parse(" " ++ Json.stringify(value)) == Done{value} :
           Result<&1, &1, Json.Error, Json.Value>
       }
  LAWS.accepts_trailing_space (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=accepts_trailing_space)
   law accepts_trailing_space:
       for value: Json.Value {
           Json.parse(Json.stringify(value) ++ " ") == Done{value} :
           Result<&1, &1, Json.Error, Json.Value>
       }
  LAWS.accepts_surrounding_space (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=accepts_surrounding_space)
   law accepts_surrounding_space:
       for value: Json.Value {
           Json.parse(" \n\t\r" ++ Json.stringify(value) ++ "\r\t\n ") == Done{value} :
           Result<&1, &1, Json.Error, Json.Value>
       }
  LAWS.rejects_trailing_garbage (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=rejects_trailing_garbage)
   law rejects_trailing_garbage:
       { Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse("nullx"))
           == True{} : Bool }
  LAWS.rejects_second_value (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=rejects_second_value)
   law rejects_second_value:
       { Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse("null true"))
           == True{} : Bool }
  LAWS.rejects_invalid_null (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=rejects_invalid_null)
   law rejects_invalid_null:
       { Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse("nul"))
           == True{} : Bool }
  LAWS.rejects_invalid_true (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=rejects_invalid_true)
   law rejects_invalid_true:
       { Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse("tru"))
           == True{} : Bool }
  LAWS.rejects_invalid_false (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=rejects_invalid_false)
   law rejects_invalid_false:
       { Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse("fals"))
           == True{} : Bool }
  LAWS.rejects_empty_input (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=rejects_empty_input)
   law rejects_empty_input:
       { Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse(""))
           == True{} : Bool }
  LAWS.rejects_whitespace_only (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=rejects_whitespace_only)
   law rejects_whitespace_only:
       { Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse(" \t\r\n "))
           == True{} : Bool }
  LAWS.parses_empty_string (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=parses_empty_string)
   law parses_empty_string:
       { Json.parse("\"\"") == Done{Json.Str{""}} :
           Result<&1, &1, Json.Error, Json.Value> }
  LAWS.parses_simple_string (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=parses_simple_string)
   law parses_simple_string:
       { Json.parse("\"hello\"") == Done{Json.Str{"hello"}} :
           Result<&1, &1, Json.Error, Json.Value> }
  LAWS.parses_newline_escape (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=parses_newline_escape)
   law parses_newline_escape:
       { Json.parse("\"a\\nb\"") == Done{Json.Str{"a\nb"}} :
           Result<&1, &1, Json.Error, Json.Value> }
  LAWS.parses_quote_escape (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=parses_quote_escape)
   law parses_quote_escape:
       { Json.parse("\"a\\\"b\"") == Done{Json.Str{"a\"b"}} :
           Result<&1, &1, Json.Error, Json.Value> }
  LAWS.parses_backslash_escape (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=parses_backslash_escape)
   law parses_backslash_escape:
       { Json.parse("\"a\\\\b\"") == Done{Json.Str{"a\\b"}} :
           Result<&1, &1, Json.Error, Json.Value> }
  LAWS.rejects_unterminated_string (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=rejects_unterminated_string)
   law rejects_unterminated_string:
       { Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse("\"hello"))
           == True{} : Bool }
  LAWS.parses_empty_array (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=parses_empty_array)
   law parses_empty_array:
       { Json.parse("[]") == Done{Json.Arr{Nil{}}} :
           Result<&1, &1, Json.Error, Json.Value> }
  LAWS.parses_literal_array (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=parses_literal_array)
   law parses_literal_array:
       {
           Json.parse("[null,true,false]")
           ==
           Done{Json.Arr{
               Json.Null{} <>
               Json.Bool{True{}} <>
               Json.Bool{False{}} <>
               Nil{}
           }}
           :
     …
  LAWS.rejects_array_trailing_comma (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=rejects_array_trailing_comma)
   law rejects_array_trailing_comma:
       { Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse("[null,]"))
           == True{} : Bool }
  LAWS.parses_empty_object (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=parses_empty_object)
   law parses_empty_object:
       { Json.parse("{}") == Done{Json.Obj{Nil{}}} :
           Result<&1, &1, Json.Error, Json.Value> }
  LAWS.rejects_unquoted_object_key (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=rejects_unquoted_object_key)
   law rejects_unquoted_object_key:
       { Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse("{foo:null}"))
           == True{} : Bool }
  LAWS.rejects_object_trailing_comma (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=rejects_object_trailing_comma)
   law rejects_object_trailing_comma:
       { Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse("{\"x\":null,}"))
           == True{} : Bool }
  LAWS.parses_nested_containers (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=parses_nested_containers)
   law parses_nested_containers:
       {
           Json.parse("[{\"x\":[true,null]}]")
           ==
           Done{Json.Arr{
               Json.Obj{
                   ("x", Json.Arr{
                       Json.Bool{True{}} <>
                       Json.Null{} <>
                       Nil{}
                   }) <>
     …
  LAWS.rejects_non_json_whitespace (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=rejects_non_json_whitespace)
   # JSON permits only space, tab, carriage return and line feed as whitespace.
   law rejects_non_json_whitespace:
       { Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse("\u{000b}null"))
           == True{} : Bool }
  LAWS.rejects_raw_string_control (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=rejects_raw_string_control)
   # A raw control character is forbidden inside a JSON string.
   law rejects_raw_string_control:
       { Result.is_fail(&1, &1, Json.Error, Json.Value,
               Json.parse("\"" ++ "\u{0001}" ++ "\""))
           == True{} : Bool }
  LAWS.parses_unicode_escape (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=parses_unicode_escape)
   # Unicode escapes decode to their scalar value, including a surrogate pair.
   law parses_unicode_escape:
       { Json.parse("\"\\u263A\"") == Done{Json.Str{"\u{263a}"}} :
           Result<&1, &1, Json.Error, Json.Value> }
  LAWS.parses_unicode_surrogate_pair (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=parses_unicode_surrogate_pair)
   law parses_unicode_surrogate_pair:
       { Json.parse("\"\\uD83D\\uDE00\"") == Done{Json.Str{"\u{1f600}"}} :
           Result<&1, &1, Json.Error, Json.Value> }
  LAWS.parses_fraction_and_exponent (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=parses_fraction_and_exponent)
   # This representative decimal/exponent form is accepted. A separate law below
   # checks that the smart number constructor preserves the original lexeme.
   law parses_fraction_and_exponent:
       { Result.is_done(&1, &1, Json.Error, Json.Value, Json.parse("-12.50e+3"))
           == True{} : Bool }
  LAWS.rejects_malformed_number_forms (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=rejects_malformed_number_forms)
   law rejects_malformed_number_forms:
       { Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse("01"))
           && Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse("1."))
           && Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse("1e+"))
           == True{} : Bool }
  LAWS.preserves_array_order (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=preserves_array_order)
   # 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_array_order:
       { Json.parse("[3,1,2]") == Done{Json.Arr{
               Json.Number{"3", Json.Certified{Json.number_proof("3", {==})}} <>
               Json.Number{"1", Json.Certified{Json.number_proof("1", {==})}} <>
               Json.Number{"2", Json.Certified{Json.number_proof("2", {==})}} <>
               Nil{}
           }} : Result<&1, &1, Json.Error, Json.Value> }
  LAWS.preserves_object_order_and_duplicates (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=preserves_object_order_and_duplicates)
   law preserves_object_order_and_duplicates:
       { Json.parse("{\"x\":1,\"x\":2}") == Done{Json.Obj{
               ("x", Json.Number{"1", Json.Certified{Json.number_proof("1", {==})}}) <>
               ("x", Json.Number{"2", Json.Certified{Json.number_proof("2", {==})}}) <>
               Nil{}
           }} : Result<&1, &1, Json.Error, Json.Value> }
  LAWS.gpu_single_matches_cpu (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=gpu_single_matches_cpu)
   # GPU entry points have the same specified results as their CPU counterparts.
   law gpu_single_matches_cpu:
       for text: String {
           Json.parse_gpu(text) == Json.parse(text) :
           Result<&1, &1, Json.Error, Json.Value>
       }
  LAWS.preserves_number_lexeme (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=preserves_number_lexeme)
   law preserves_number_lexeme:
       { Json.number("-12.50e+3") == Done{Json.Number{
               "-12.50e+3",
               Json.Certified{Json.number_proof("-12.50e+3", {==})}
           }} : Result<&1, &1, Json.Error, Json.Value> }
  LAWS.gpu_batch_matches_cpu (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=gpu_batch_matches_cpu)
   law gpu_batch_matches_cpu:
       for batch: Json.Batch {
           Json.parse_batch_gpu(batch) == Json.parse_batch(batch) : Json.BatchResult
       }
  LAWS.url_component_ascii (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=url_component_ascii)
   # Encode each UTF-8 byte with an uppercase percent escape.
   law url_component_ascii:
       { URL.percent_component("A") == "%41" : String }
  LAWS.url_component_reserved (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=url_component_reserved)
   law url_component_reserved:
       { URL.percent_component("/") == "%2F" : String }
  LAWS.url_component_utf8 (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=url_component_utf8)
   law url_component_utf8:
       { URL.percent_component(SCon{Chr{233}, SNil{}}) == "%C3%A9" : String }
  LAWS.aes256gcm_accepts_32_byte_key (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=aes256gcm_accepts_32_byte_key)
   law aes256gcm_accepts_32_byte_key:
       for +bytes: List<&2, U32>
       for size: {List.length(&2, U32, bytes) == 32n : Nat}
       for valid: {AES.bytes_valid(bytes) == True{} : Bool}
       {AES.key(bytes) == Done{AES.SecretKey{bytes, size, valid}} :
           Result<&2, &2, AES.Error, AES.SecretKey>}
  LAWS.aes256gcm_rejects_wrong_key_length (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=aes256gcm_rejects_wrong_key_length)
   law aes256gcm_rejects_wrong_key_length:
       for +bytes: List<&2, U32>
       for size: {List.length(&2, U32, bytes) != 32n : Nat}
       {AES.key(bytes) == Fail{AES.InvalidKey{}} :
           Result<&2, &2, AES.Error, AES.SecretKey>}
  LAWS.aes256gcm_rejects_non_byte_key (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=aes256gcm_rejects_non_byte_key)
   law aes256gcm_rejects_non_byte_key:
       for +bytes: List<&2, U32>
       for valid: {AES.bytes_valid(bytes) == False{} : Bool}
       {AES.key(bytes) == Fail{AES.InvalidKey{}} :
           Result<&2, &2, AES.Error, AES.SecretKey>}
  LAWS.aes256gcm_accepts_12_byte_nonce (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=aes256gcm_accepts_12_byte_nonce)
   law aes256gcm_accepts_12_byte_nonce:
       for +bytes: List<&2, U32>
       for size: {List.length(&2, U32, bytes) == 12n : Nat}
       for valid: {AES.bytes_valid(bytes) == True{} : Bool}
       {AES.nonce(bytes) == Done{AES.Nonce{bytes, size, valid}} :
           Result<&2, &2, AES.Error, AES.Nonce>}
  LAWS.aes256gcm_rejects_wrong_nonce_length (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=aes256gcm_rejects_wrong_nonce_length)
   law aes256gcm_rejects_wrong_nonce_length:
       for +bytes: List<&2, U32>
       for size: {List.length(&2, U32, bytes) != 12n : Nat}
       {AES.nonce(bytes) == Fail{AES.InvalidNonce{}} :
           Result<&2, &2, AES.Error, AES.Nonce>}
  LAWS.aes256gcm_rejects_non_byte_nonce (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=aes256gcm_rejects_non_byte_nonce)
   law aes256gcm_rejects_non_byte_nonce:
       for +bytes: List<&2, U32>
       for valid: {AES.bytes_valid(bytes) == False{} : Bool}
       {AES.nonce(bytes) == Fail{AES.InvalidNonce{}} :
           Result<&2, &2, AES.Error, AES.Nonce>}
  LAWS.aes256gcm_encrypts_valid_input (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=aes256gcm_encrypts_valid_input)
   # This prevents satisfying the conditional roundtrip by always failing.
   law aes256gcm_encrypts_valid_input:
       for key: AES.SecretKey
       for nonce: AES.Nonce
       for aad: List<&2, U32>
       for plaintext: List<&2, U32>
       for aad_ok: {AES.aad_valid(aad) == True{} : Bool}
       for plaintext_ok: {AES.plaintext_valid(plaintext) == True{} : Bool}
       {Result.is_done(&2, &2, AES.Error, AES.Envelope,
           AES.encrypt(key, nonce, aad, plaintext)) == True{} : Bool}
  LAWS.aes256gcm_rejects_invalid_plaintext (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=aes256gcm_rejects_invalid_plaintext)
   law aes256gcm_rejects_invalid_plaintext:
       for +key: AES.SecretKey
       for +nonce: AES.Nonce
       for +aad: List<&2, U32>
       for +plaintext: List<&2, U32>
       for valid: {AES.plaintext_valid(plaintext) == False{} : Bool}
       {AES.encrypt(key, nonce, aad, plaintext) == Fail{AES.InvalidBytes{}} :
           Result<&2, &2, AES.Error, AES.Envelope>}
  LAWS.aes256gcm_rejects_invalid_aad (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=aes256gcm_rejects_invalid_aad)
   law aes256gcm_rejects_invalid_aad:
       for +key: AES.SecretKey
       for +nonce: AES.Nonce
       for +aad: List<&2, U32>
       for +plaintext: List<&2, U32>
       for valid: {AES.aad_valid(aad) == False{} : Bool}
       {AES.encrypt(key, nonce, aad, plaintext) == Fail{AES.InvalidBytes{}} :
           Result<&2, &2, AES.Error, AES.Envelope>}
  LAWS.aes256gcm_decrypt_rejects_invalid_aad (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=aes256gcm_decrypt_rejects_invalid_aad)
   law aes256gcm_decrypt_rejects_invalid_aad:
       for +key: AES.SecretKey
       for +aad: List<&2, U32>
       for +envelope: AES.Envelope
       for valid: {AES.aad_valid(aad) == False{} : Bool}
       {AES.decrypt(key, aad, envelope) == Fail{AES.InvalidBytes{}} :
           Result<&2, &2, AES.Error, List<&2, U32>>}
  LAWS.aes256gcm_roundtrip (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=aes256gcm_roundtrip)
   law aes256gcm_roundtrip:
       for +key: AES.SecretKey
       for +nonce: AES.Nonce
       for +aad: List<&2, U32>
       for +plaintext: List<&2, U32>
       for +envelope: AES.Envelope
       for encrypted: {AES.encrypt(key, nonce, aad, plaintext) == Done{envelope} :
           Result<&2, &2, AES.Error, AES.Envelope>}
       {AES.decrypt(key, aad, envelope) == Done{plaintext} :
           Result<&2, &2, AES.Error, List<&2, U32>>}
  LAWS.aes256gcm_preserves_nonce (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=aes256gcm_preserves_nonce)
   law aes256gcm_preserves_nonce:
       for +key: AES.SecretKey
       for +nonce: AES.Nonce
       for +aad: List<&2, U32>
       for +plaintext: List<&2, U32>
       for +envelope: AES.Envelope
       for encrypted: {AES.encrypt(key, nonce, aad, plaintext) == Done{envelope} :
           Result<&2, &2, AES.Error, AES.Envelope>}
       {AES.envelope_nonce(envelope) == nonce : AES.Nonce}
  LAWS.aes256gcm_preserves_plaintext_length (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=aes256gcm_preserves_plaintext_length)
   law aes256gcm_preserves_plaintext_length:
       for +key: AES.SecretKey
       for +nonce: AES.Nonce
       for +aad: List<&2, U32>
       for +plaintext: List<&2, U32>
       for +envelope: AES.Envelope
       for encrypted: {AES.encrypt(key, nonce, aad, plaintext) == Done{envelope} :
           Result<&2, &2, AES.Error, AES.Envelope>}
       {List.length(&2, U32, AES.ciphertext(envelope)) ==
           List.length(&2, U32, plaintext) : Nat}
  LAWS.aes256gcm_rejects_changed_tag (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=aes256gcm_rejects_changed_tag)
   # 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_rejects_changed_tag:
       for +key: AES.SecretKey
       for +nonce: AES.Nonce
       for +aad: List<&2, U32>
       for +plaintext: List<&2, U32>
       for +envelope: AES.Envelope
       for +tampered: AES.Envelope
       for encrypted: {AES.encrypt(key, nonce, aad, plaintext) == Done{envelope} :
     …
  LAWS.aes256gcm_envelope_roundtrip (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=aes256gcm_envelope_roundtrip)
   law aes256gcm_envelope_roundtrip:
       for +envelope: AES.Envelope
       {AES.parse(AES.encode(envelope)) == Done{envelope} :
           Result<&2, &2, AES.Error, AES.Envelope>}
  LAWS.aes256gcm_envelope_is_canonical (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=aes256gcm_envelope_is_canonical)
   law aes256gcm_envelope_is_canonical:
       for +text: String
       for +envelope: AES.Envelope
       for parsed: {AES.parse(text) == Done{envelope} :
           Result<&2, &2, AES.Error, AES.Envelope>}
       {AES.encode(envelope) == text : String}
  LAWS.aes256gcm_rejects_empty_envelope (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=aes256gcm_rejects_empty_envelope)
   law aes256gcm_rejects_empty_envelope:
       {AES.parse("") == Fail{AES.InvalidEnvelope{}} :
           Result<&2, &2, AES.Error, AES.Envelope>}
  LAWS.aes256gcm_rejects_unknown_version (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=aes256gcm_rejects_unknown_version)
   law aes256gcm_rejects_unknown_version:
       {AES.parse("v2.cafebabefacedbaddecaf888.fd2caa16a5832e76aa132c1453eeda7e.") == Fail{AES.InvalidEnvelope{}} :
           Result<&2, &2, AES.Error, AES.Envelope>}
  LAWS.aes256gcm_rejects_missing_version (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=aes256gcm_rejects_missing_version)
   law aes256gcm_rejects_missing_version:
       {AES.parse("cafebabefacedbaddecaf888.fd2caa16a5832e76aa132c1453eeda7e.") == Fail{AES.InvalidEnvelope{}} :
           Result<&2, &2, AES.Error, AES.Envelope>}
  LAWS.aes256gcm_rejects_short_nonce (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=aes256gcm_rejects_short_nonce)
   law aes256gcm_rejects_short_nonce:
       {AES.parse("v1.cafebabefacedbaddecaf8.fd2caa16a5832e76aa132c1453eeda7e.") == Fail{AES.InvalidEnvelope{}} :
           Result<&2, &2, AES.Error, AES.Envelope>}
  LAWS.aes256gcm_rejects_long_nonce (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=aes256gcm_rejects_long_nonce)
   law aes256gcm_rejects_long_nonce:
       {AES.parse("v1.cafebabefacedbaddecaf88800.fd2caa16a5832e76aa132c1453eeda7e.") == Fail{AES.InvalidEnvelope{}} :
           Result<&2, &2, AES.Error, AES.Envelope>}
  LAWS.aes256gcm_rejects_short_tag (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=aes256gcm_rejects_short_tag)
   law aes256gcm_rejects_short_tag:
       {AES.parse("v1.cafebabefacedbaddecaf888.fd2caa16a5832e76aa132c1453eeda.") == Fail{AES.InvalidEnvelope{}} :
           Result<&2, &2, AES.Error, AES.Envelope>}
  LAWS.aes256gcm_rejects_long_tag (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=aes256gcm_rejects_long_tag)
   law aes256gcm_rejects_long_tag:
       {AES.parse("v1.cafebabefacedbaddecaf888.fd2caa16a5832e76aa132c1453eeda7e00.") == Fail{AES.InvalidEnvelope{}} :
           Result<&2, &2, AES.Error, AES.Envelope>}
  LAWS.aes256gcm_rejects_odd_ciphertext_hex (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=aes256gcm_rejects_odd_ciphertext_hex)
   law aes256gcm_rejects_odd_ciphertext_hex:
       {AES.parse("v1.cafebabefacedbaddecaf888.fd2caa16a5832e76aa132c1453eeda7e.0") == Fail{AES.InvalidEnvelope{}} :
           Result<&2, &2, AES.Error, AES.Envelope>}
  LAWS.aes256gcm_rejects_non_hex_ciphertext (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=aes256gcm_rejects_non_hex_ciphertext)
   law aes256gcm_rejects_non_hex_ciphertext:
       {AES.parse("v1.cafebabefacedbaddecaf888.fd2caa16a5832e76aa132c1453eeda7e.gg") == Fail{AES.InvalidEnvelope{}} :
           Result<&2, &2, AES.Error, AES.Envelope>}
  LAWS.aes256gcm_rejects_non_hex_nonce (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=aes256gcm_rejects_non_hex_nonce)
   law aes256gcm_rejects_non_hex_nonce:
       {AES.parse("v1.zzfebabefacedbaddecaf888.fd2caa16a5832e76aa132c1453eeda7e.") == Fail{AES.InvalidEnvelope{}} :
           Result<&2, &2, AES.Error, AES.Envelope>}
  LAWS.aes256gcm_rejects_non_hex_tag (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=aes256gcm_rejects_non_hex_tag)
   law aes256gcm_rejects_non_hex_tag:
       {AES.parse("v1.cafebabefacedbaddecaf888.zz2caa16a5832e76aa132c1453eeda7e.") == Fail{AES.InvalidEnvelope{}} :
           Result<&2, &2, AES.Error, AES.Envelope>}
  LAWS.aes256gcm_rejects_uppercase_hex (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=aes256gcm_rejects_uppercase_hex)
   law aes256gcm_rejects_uppercase_hex:
       {AES.parse("v1.CAFEBABEFACEDBADDECAF888.fd2caa16a5832e76aa132c1453eeda7e.") == Fail{AES.InvalidEnvelope{}} :
           Result<&2, &2, AES.Error, AES.Envelope>}
  LAWS.aes256gcm_rejects_extra_field (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=aes256gcm_rejects_extra_field)
   law aes256gcm_rejects_extra_field:
       {AES.parse("v1.cafebabefacedbaddecaf888.fd2caa16a5832e76aa132c1453eeda7e..") == Fail{AES.InvalidEnvelope{}} :
           Result<&2, &2, AES.Error, AES.Envelope>}
  LAWS.aes256gcm_rejects_missing_ciphertext_field (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=aes256gcm_rejects_missing_ciphertext_field)
   law aes256gcm_rejects_missing_ciphertext_field:
       {AES.parse("v1.cafebabefacedbaddecaf888.fd2caa16a5832e76aa132c1453eeda7e") == Fail{AES.InvalidEnvelope{}} :
           Result<&2, &2, AES.Error, AES.Envelope>}
  LAWS.aes256gcm_rejects_trailing_garbage (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=aes256gcm_rejects_trailing_garbage)
   law aes256gcm_rejects_trailing_garbage:
       {AES.parse("v1.cafebabefacedbaddecaf888.fd2caa16a5832e76aa132c1453eeda7e.00!") == Fail{AES.InvalidEnvelope{}} :
           Result<&2, &2, AES.Error, AES.Envelope>}
  LAWS.aes256gcm_rejects_surrounding_whitespace (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=aes256gcm_rejects_surrounding_whitespace)
   law aes256gcm_rejects_surrounding_whitespace:
       {AES.parse(" v1.cafebabefacedbaddecaf888.fd2caa16a5832e76aa132c1453eeda7e. ") == Fail{AES.InvalidEnvelope{}} :
           Result<&2, &2, AES.Error, AES.Envelope>}
  LAWS.aes256gcm_nist_key (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=aes256gcm_nist_key)
   def aes256gcm_nist_key() -> AES.SecretKey:
  LAWS.aes256gcm_nist_nonce (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=aes256gcm_nist_nonce)
   def aes256gcm_nist_nonce() -> AES.Nonce:
  LAWS.aes256gcm_nist_empty (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=aes256gcm_nist_empty)
   def aes256gcm_nist_empty() -> AES.Envelope:
  LAWS.aes256gcm_nist_encrypt_observation (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=aes256gcm_nist_encrypt_observation)
   # 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_encrypt_observation(result: Result<&2, &2, AES.Error, AES.Envelope>) -> List<&2, U32>:
  LAWS.aes256gcm_nist_empty_encrypt (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=aes256gcm_nist_empty_encrypt)
   law aes256gcm_nist_empty_encrypt:
       {aes256gcm_nist_encrypt_observation(AES.encrypt(aes256gcm_nist_key(), aes256gcm_nist_nonce(),
           [], [])) == aes256gcm_nist_encrypt_observation(Done{aes256gcm_nist_empty()}) :
           List<&2, U32>}
  LAWS.aes256gcm_nist_empty_decrypt (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=aes256gcm_nist_empty_decrypt)
   law aes256gcm_nist_empty_decrypt:
       {AES.decrypt(aes256gcm_nist_key(), [],
           aes256gcm_nist_empty()) == Done{[]} :
           Result<&2, &2, AES.Error, List<&2, U32>>}
  LAWS.aes256gcm_nist_multiblock (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=aes256gcm_nist_multiblock)
   def aes256gcm_nist_multiblock() -> AES.Envelope:
  LAWS.aes256gcm_nist_multiblock_encrypt (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=aes256gcm_nist_multiblock_encrypt)
   law aes256gcm_nist_multiblock_encrypt:
       {aes256gcm_nist_encrypt_observation(AES.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>}
  LAWS.aes256gcm_nist_multiblock_decrypt (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=aes256gcm_nist_multiblock_decrypt)
   law aes256gcm_nist_multiblock_decrypt:
       {AES.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, AES.Error, List<&2, U32>>}
  LAWS.aes256gcm_nist_aad_only (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=aes256gcm_nist_aad_only)
   def aes256gcm_nist_aad_only() -> AES.Envelope:
  LAWS.aes256gcm_nist_aad_only_encrypt (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=aes256gcm_nist_aad_only_encrypt)
   law aes256gcm_nist_aad_only_encrypt:
       {aes256gcm_nist_encrypt_observation(AES.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>}
  LAWS.aes256gcm_nist_aad_only_decrypt (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=aes256gcm_nist_aad_only_decrypt)
   law aes256gcm_nist_aad_only_decrypt:
       {AES.decrypt(aes256gcm_nist_key(), [58, 215, 123, 180, 13, 122, 54, 96, 168, 158, 202, 243, 36, 102, 239, 151, 245, 211, 213, 133, 3, 185, 105, 157, 231, 133, 137, 90, 150, 253, 186, 175, 67, 177, 205, 127, 89, 142, 206, 35, 136, 27, 0, 227, 237, 3, 6, 136, 123, 12, 120, 94, 39, 232, 173, 63, 130, 35, 32, 113, 4, 114, 93, 212],
           aes256gcm_nist_aad_only()) == Done{[]} :
           Result<&2, &2, AES.Error, List<&2, U32>>}
  LAWS.aes256gcm_nist_aad_and_multiblock (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=aes256gcm_nist_aad_and_multiblock)
   def aes256gcm_nist_aad_and_multiblock() -> AES.Envelope:
  LAWS.aes256gcm_nist_aad_and_multiblock_encrypt (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=aes256gcm_nist_aad_and_multiblock_encrypt)
   law aes256gcm_nist_aad_and_multiblock_encrypt:
       {aes256gcm_nist_encrypt_observation(AES.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>}
  LAWS.aes256gcm_nist_aad_and_multiblock_decrypt (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=aes256gcm_nist_aad_and_multiblock_decrypt)
   law aes256gcm_nist_aad_and_multiblock_decrypt:
       {AES.decrypt(aes256gcm_nist_key(), [58, 215, 123, 180, 13, 122, 54, 96, 168, 158, 202, 243, 36, 102, 239, 151, 245, 211, 213, 133, 3, 185, 105, 157, 231, 133, 137, 90, 150, 253, 186, 175, 67, 177, 205, 127, 89, 142, 206, 35, 136, 27, 0, 227, 237, 3, 6, 136, 123, 12, 120, 94, 39, 232, 173, 63, 130, 35, 32, 113, 4, 114, 93, 212],
           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, AES.Error, List<&2, U32>>}
  LAWS.aes256gcm_nist_partial_block (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=aes256gcm_nist_partial_block)
   def aes256gcm_nist_partial_block() -> AES.Envelope:
  LAWS.aes256gcm_nist_partial_block_encrypt (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=aes256gcm_nist_partial_block_encrypt)
   law aes256gcm_nist_partial_block_encrypt:
       {aes256gcm_nist_encrypt_observation(AES.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>}
  LAWS.aes256gcm_nist_partial_block_decrypt (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=aes256gcm_nist_partial_block_decrypt)
   law aes256gcm_nist_partial_block_decrypt:
       {AES.decrypt(aes256gcm_nist_key(), [58, 215, 123, 180, 13, 122, 54, 96, 168, 158, 202, 243, 36, 102, 239, 151, 245, 211, 213, 133],
           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, AES.Error, List<&2, U32>>}
  LAWS.aes256gcm_nist_canonical_encoding (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=aes256gcm_nist_canonical_encoding)
   law aes256gcm_nist_canonical_encoding:
       {AES.encode(aes256gcm_nist_empty()) == "v1.cafebabefacedbaddecaf888.fd2caa16a5832e76aa132c1453eeda7e." : String}
  LAWS.aes256gcm_nist_canonical_parsing (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=aes256gcm_nist_canonical_parsing)
   law aes256gcm_nist_canonical_parsing:
       {AES.parse("v1.cafebabefacedbaddecaf888.fd2caa16a5832e76aa132c1453eeda7e.") == Done{aes256gcm_nist_empty()} :
           Result<&2, &2, AES.Error, AES.Envelope>}
  LAWS.aes256gcm_nist_rejects_changed_aad (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=aes256gcm_nist_rejects_changed_aad)
   # 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_aad:
       {AES.decrypt(aes256gcm_nist_key(), [1], aes256gcm_nist_empty()) ==
           Fail{AES.AuthenticationFailed{}} :
           Result<&2, &2, AES.Error, List<&2, U32>>}
  LAWS.aes256gcm_nist_rejects_changed_key (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=aes256gcm_nist_rejects_changed_key)
   law aes256gcm_nist_rejects_changed_key:
       {AES.decrypt(AES.SecretKey{List.replicate(U32, 32n, 0), {==}, {==}},
           [], aes256gcm_nist_empty()) == Fail{AES.AuthenticationFailed{}} :
           Result<&2, &2, AES.Error, List<&2, U32>>}
  LAWS.aes256gcm_nist_rejects_changed_nonce (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=aes256gcm_nist_rejects_changed_nonce)
   law aes256gcm_nist_rejects_changed_nonce:
       {AES.decrypt(aes256gcm_nist_key(), [],
           AES.Envelope{AES.Nonce{List.replicate(U32, 12n, 0), {==}, {==}},
               [], AES.Tag{[253, 44, 170, 22, 165, 131, 46, 118, 170, 19, 44, 20, 83, 238, 218, 126], {==}, {==}}, {==}}) ==
           Fail{AES.AuthenticationFailed{}} :
           Result<&2, &2, AES.Error, List<&2, U32>>}
  LAWS.aes256gcm_nist_rejects_changed_ciphertext (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=aes256gcm_nist_rejects_changed_ciphertext)
   law aes256gcm_nist_rejects_changed_ciphertext:
       {AES.decrypt(aes256gcm_nist_key(), [],
           AES.Envelope{aes256gcm_nist_nonce(), [1],
               AES.Tag{[253, 44, 170, 22, 165, 131, 46, 118, 170, 19, 44, 20, 83, 238, 218, 126], {==}, {==}}, {==}}) ==
           Fail{AES.AuthenticationFailed{}} :
           Result<&2, &2, AES.Error, List<&2, U32>>}
  PROOF.ResultValue (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/PROOF.bend&name=ResultValue)
   def ResultValue() -> Type:
  PROOF.parse_for_equality (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/PROOF.bend&name=parse_for_equality)
   def parse_for_equality(text: String) -> ResultValue():
  PROOF.assemble_atom (https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/PROOF.bend&name=assemble_atom)
   def assemble_atom(result: ResultValue()) -> {Json.assemble(Json.Atom{result} <> Nil{}, Json.NeedValue{Json.Top{}}) == result : ResultValue()}:
More: https://jend.leeeet.dev/packages/qasim-bend-kit.txt?definitions_offset=100