LAWS.bend source
LAWS.bend on the hub · documented module
# Library correctness laws and integration obligations.import Base# JSON contract: libs/JSON.bend.## Expected API:# Json.parse(text: String) -> Result<&1, &1, Json.Error, Json.Value># Json.stringify(value: Json.Value) -> Stringimport ./libs/JSON.bend as Jsonimport ./libs/URL.bend as URL# ============================================================# JSON: Core correctness# ============================================================law stringify_parse_roundtrip: for value: Json.Value { Json.parse(Json.stringify(value)) == Done{value} : Result<&1, &1, Json.Error, Json.Value> }# ============================================================# JSON: Literals# ============================================================law parses_null: { Json.parse("null") == Done{Json.Null{}} : Result<&1, &1, Json.Error, Json.Value> }law parses_true: { Json.parse("true") == Done{Json.Bool{True{}}} : Result<&1, &1, Json.Error, Json.Value> }law parses_false: { Json.parse("false") == Done{Json.Bool{False{}}} : Result<&1, &1, Json.Error, Json.Value> }# ============================================================# JSON: Whitespace# ============================================================law accepts_leading_space: for value: Json.Value { Json.parse(" " ++ Json.stringify(value)) == Done{value} : Result<&1, &1, Json.Error, Json.Value> }law accepts_trailing_space: for value: Json.Value { Json.parse(Json.stringify(value) ++ " ") == Done{value} : Result<&1, &1, Json.Error, Json.Value> }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> }# ============================================================# JSON: Invalid and incomplete input# ============================================================law rejects_trailing_garbage: { Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse("nullx")) == True{} : Bool }law rejects_second_value: { Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse("null true")) == True{} : Bool }law rejects_invalid_null: { Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse("nul")) == True{} : Bool }law rejects_invalid_true: { Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse("tru")) == True{} : Bool }law rejects_invalid_false: { Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse("fals")) == True{} : Bool }law rejects_empty_input: { Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse("")) == True{} : Bool }law rejects_whitespace_only: { Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse(" \t\r\n ")) == True{} : Bool }# ============================================================# JSON: Strings# ============================================================law parses_empty_string: { Json.parse("\"\"") == Done{Json.Str{""}} : Result<&1, &1, Json.Error, Json.Value> }law parses_simple_string: { Json.parse("\"hello\"") == Done{Json.Str{"hello"}} : Result<&1, &1, Json.Error, Json.Value> }law parses_newline_escape: { Json.parse("\"a\\nb\"") == Done{Json.Str{"a\nb"}} : Result<&1, &1, Json.Error, Json.Value> }law parses_quote_escape: { Json.parse("\"a\\\"b\"") == Done{Json.Str{"a\"b"}} : Result<&1, &1, Json.Error, Json.Value> }law parses_backslash_escape: { Json.parse("\"a\\\\b\"") == Done{Json.Str{"a\\b"}} : Result<&1, &1, Json.Error, Json.Value> }law rejects_unterminated_string: { Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse("\"hello")) == True{} : Bool }# ============================================================# JSON: Arrays# ============================================================law parses_empty_array: { Json.parse("[]") == Done{Json.Arr{Nil{}}} : Result<&1, &1, Json.Error, Json.Value> }law parses_literal_array: { Json.parse("[null,true,false]") == Done{Json.Arr{ Json.Null{} <> Json.Bool{True{}} <> Json.Bool{False{}} <> Nil{} }} : Result<&1, &1, Json.Error, Json.Value> }law rejects_array_trailing_comma: { Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse("[null,]")) == True{} : Bool }# ============================================================# JSON: Objects# ============================================================law parses_empty_object: { Json.parse("{}") == Done{Json.Obj{Nil{}}} : Result<&1, &1, Json.Error, Json.Value> }law rejects_unquoted_object_key: { Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse("{foo:null}")) == True{} : Bool }law rejects_object_trailing_comma: { Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse("{\"x\":null,}")) == True{} : Bool }# ============================================================# JSON: Nesting# ============================================================law parses_nested_containers: { Json.parse("[{\"x\":[true,null]}]") == Done{Json.Arr{ Json.Obj{ ("x", Json.Arr{ Json.Bool{True{}} <> Json.Null{} <> Nil{} }) <> Nil{} } <> Nil{} }} : Result<&1, &1, Json.Error, Json.Value> }# ============================================================# JSON: Additional semantics# ============================================================# 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 }# 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 }# 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> }law parses_unicode_surrogate_pair: { Json.parse("\"\\uD83D\\uDE00\"") == Done{Json.Str{"\u{1f600}"}} : Result<&1, &1, Json.Error, Json.Value> }# 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 }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 }# 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> }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> }# 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> }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> }law gpu_batch_matches_cpu: for batch: Json.Batch { Json.parse_batch_gpu(batch) == Json.parse_batch(batch) : Json.BatchResult }# ============================================================# URL component encoding# ============================================================# Encode each UTF-8 byte with an uppercase percent escape.law url_component_ascii: { URL.percent_component("A") == "%41" : String }law url_component_reserved: { URL.percent_component("/") == "%2F" : String }law url_component_utf8: { URL.percent_component(SCon{Chr{233}, SNil{}}) == "%C3%A9" : String }