~/bend-docscommunity

LAWS.bend open laws/TODOs

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

Library correctness laws and integration obligations.

3 imports
import Base
import ./libs/JSON.bend as Json
import ./libs/URL.bend as URL

Laws

law stringify_parse_roundtrip provedin PROOF.bendsource · line 18 · raw

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

law parses_null provedin PROOF.bendsource · line 31 · raw

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

law parses_true provedin PROOF.bendsource · line 35 · raw

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

law parses_false provedin PROOF.bendsource · line 39 · raw

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

law accepts_leading_space provedin PROOF.bendsource · line 47 · raw

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

law accepts_trailing_space provedin PROOF.bendsource · line 53 · raw

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

law accepts_surrounding_space provedin PROOF.bendsource · line 59 · raw

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

law rejects_trailing_garbage provedin PROOF.bendsource · line 69 · raw

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

law rejects_second_value provedin PROOF.bendsource · line 73 · raw

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

law rejects_invalid_null provedin PROOF.bendsource · line 77 · raw

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

law rejects_invalid_true provedin PROOF.bendsource · line 81 · raw

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

law rejects_invalid_false provedin PROOF.bendsource · line 85 · raw

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

law rejects_empty_input provedin PROOF.bendsource · line 89 · raw

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

law rejects_whitespace_only provedin PROOF.bendsource · line 93 · raw

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

law parses_empty_string provedin PROOF.bendsource · line 101 · raw

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

law parses_simple_string provedin PROOF.bendsource · line 105 · raw

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

law parses_newline_escape provedin PROOF.bendsource · line 109 · raw

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

law parses_quote_escape provedin PROOF.bendsource · line 113 · raw

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

law parses_backslash_escape provedin PROOF.bendsource · line 117 · raw

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

law rejects_unterminated_string provedin PROOF.bendsource · line 121 · raw

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

law parses_empty_array provedin PROOF.bendsource · line 129 · raw

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

law parses_literal_array provedin PROOF.bendsource · line 133 · raw

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

law rejects_array_trailing_comma provedin PROOF.bendsource · line 147 · raw

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

law parses_empty_object provedin PROOF.bendsource · line 155 · raw

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

law rejects_unquoted_object_key provedin PROOF.bendsource · line 159 · raw

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

law rejects_object_trailing_comma provedin PROOF.bendsource · line 163 · raw

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

law parses_nested_containers provedin PROOF.bendsource · line 171 · raw

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

law rejects_non_json_whitespace provedin PROOF.bendsource · line 195 · raw

{Result.is_fail(&1, &1, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Error, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Value, 0x0b4f68372ee8cbe03f4a66931f85cfdc/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 provedin PROOF.bendsource · line 200 · raw

{Result.is_fail(&1, &1, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Error, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Value, 0x0b4f68372ee8cbe03f4a66931f85cfdc/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 provedin PROOF.bendsource · line 206 · raw

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

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

law parses_unicode_surrogate_pair provedin PROOF.bendsource · line 210 · raw

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

law parses_fraction_and_exponent provedin PROOF.bendsource · line 216 · raw

{Result.is_done(&1, &1, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Error, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Value, 0x0b4f68372ee8cbe03f4a66931f85cfdc/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 provedin PROOF.bendsource · line 220 · raw

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

law preserves_array_order provedin PROOF.bendsource · line 228 · raw

{0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.parse("[3,1,2]") == Done{0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Arr{[0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Number{"3", 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Certified{0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.number_proof("3", {==})}}, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Number{"1", 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Certified{0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.number_proof("1", {==})}}, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Number{"2", 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Certified{0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.number_proof("2", {==})}}]}} : Result<&1, &1, 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Error, 0x0b4f68372ee8cbe03f4a66931f85cfdc/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 provedin PROOF.bendsource · line 236 · raw

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

law gpu_single_matches_cpu provedin PROOF.bendsource · line 244 · raw

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

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

law preserves_number_lexeme provedin PROOF.bendsource · line 250 · raw

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

law gpu_batch_matches_cpu provedin PROOF.bendsource · line 256 · raw

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

law url_component_ascii provedin PROOF.bendsource · line 266 · raw

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

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

law url_component_reserved provedin PROOF.bendsource · line 269 · raw

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

law url_component_utf8 provedin PROOF.bendsource · line 272 · raw

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