1 # Library correctness laws and integration obligations. 2 3 import Base 4 5 # JSON contract: libs/JSON.bend. 6 # 7 # Expected API: 8 # Json.parse(text: String) -> Result<&1, &1, Json.Error, Json.Value> 9 # Json.stringify(value: Json.Value) -> String 10 11 import ./libs/JSON.bend as Json 12 import ./libs/URL.bend as URL 13 14 # ============================================================ 15 # JSON: Core correctness 16 # ============================================================ 17 18 law stringify_parse_roundtrip: 19 for value: Json.Value { 20 Json.parse(Json.stringify(value)) 21 == 22 Done{value} 23 : 24 Result<&1, &1, Json.Error, Json.Value> 25 } 26 27 # ============================================================ 28 # JSON: Literals 29 # ============================================================ 30 31 law parses_null: 32 { Json.parse("null") == Done{Json.Null{}} : 33 Result<&1, &1, Json.Error, Json.Value> } 34 35 law parses_true: 36 { Json.parse("true") == Done{Json.Bool{True{}}} : 37 Result<&1, &1, Json.Error, Json.Value> } 38 39 law parses_false: 40 { Json.parse("false") == Done{Json.Bool{False{}}} : 41 Result<&1, &1, Json.Error, Json.Value> } 42 43 # ============================================================ 44 # JSON: Whitespace 45 # ============================================================ 46 47 law accepts_leading_space: 48 for value: Json.Value { 49 Json.parse(" " ++ Json.stringify(value)) == Done{value} : 50 Result<&1, &1, Json.Error, Json.Value> 51 } 52 53 law accepts_trailing_space: 54 for value: Json.Value { 55 Json.parse(Json.stringify(value) ++ " ") == Done{value} : 56 Result<&1, &1, Json.Error, Json.Value> 57 } 58 59 law accepts_surrounding_space: 60 for value: Json.Value { 61 Json.parse(" \n\t\r" ++ Json.stringify(value) ++ "\r\t\n ") == Done{value} : 62 Result<&1, &1, Json.Error, Json.Value> 63 } 64 65 # ============================================================ 66 # JSON: Invalid and incomplete input 67 # ============================================================ 68 69 law rejects_trailing_garbage: 70 { Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse("nullx")) 71 == True{} : Bool } 72 73 law rejects_second_value: 74 { Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse("null true")) 75 == True{} : Bool } 76 77 law rejects_invalid_null: 78 { Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse("nul")) 79 == True{} : Bool } 80 81 law rejects_invalid_true: 82 { Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse("tru")) 83 == True{} : Bool } 84 85 law rejects_invalid_false: 86 { Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse("fals")) 87 == True{} : Bool } 88 89 law rejects_empty_input: 90 { Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse("")) 91 == True{} : Bool } 92 93 law rejects_whitespace_only: 94 { Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse(" \t\r\n ")) 95 == True{} : Bool } 96 97 # ============================================================ 98 # JSON: Strings 99 # ============================================================ 100 101 law parses_empty_string: 102 { Json.parse("\"\"") == Done{Json.Str{""}} : 103 Result<&1, &1, Json.Error, Json.Value> } 104 105 law parses_simple_string: 106 { Json.parse("\"hello\"") == Done{Json.Str{"hello"}} : 107 Result<&1, &1, Json.Error, Json.Value> } 108 109 law parses_newline_escape: 110 { Json.parse("\"a\\nb\"") == Done{Json.Str{"a\nb"}} : 111 Result<&1, &1, Json.Error, Json.Value> } 112 113 law parses_quote_escape: 114 { Json.parse("\"a\\\"b\"") == Done{Json.Str{"a\"b"}} : 115 Result<&1, &1, Json.Error, Json.Value> } 116 117 law parses_backslash_escape: 118 { Json.parse("\"a\\\\b\"") == Done{Json.Str{"a\\b"}} : 119 Result<&1, &1, Json.Error, Json.Value> } 120 121 law rejects_unterminated_string: 122 { Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse("\"hello")) 123 == True{} : Bool } 124 125 # ============================================================ 126 # JSON: Arrays 127 # ============================================================ 128 129 law parses_empty_array: 130 { Json.parse("[]") == Done{Json.Arr{Nil{}}} : 131 Result<&1, &1, Json.Error, Json.Value> } 132 133 law parses_literal_array: 134 { 135 Json.parse("[null,true,false]") 136 == 137 Done{Json.Arr{ 138 Json.Null{} <> 139 Json.Bool{True{}} <> 140 Json.Bool{False{}} <> 141 Nil{} 142 }} 143 : 144 Result<&1, &1, Json.Error, Json.Value> 145 } 146 147 law rejects_array_trailing_comma: 148 { Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse("[null,]")) 149 == True{} : Bool } 150 151 # ============================================================ 152 # JSON: Objects 153 # ============================================================ 154 155 law parses_empty_object: 156 { Json.parse("{}") == Done{Json.Obj{Nil{}}} : 157 Result<&1, &1, Json.Error, Json.Value> } 158 159 law rejects_unquoted_object_key: 160 { Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse("{foo:null}")) 161 == True{} : Bool } 162 163 law rejects_object_trailing_comma: 164 { Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse("{\"x\":null,}")) 165 == True{} : Bool } 166 167 # ============================================================ 168 # JSON: Nesting 169 # ============================================================ 170 171 law parses_nested_containers: 172 { 173 Json.parse("[{\"x\":[true,null]}]") 174 == 175 Done{Json.Arr{ 176 Json.Obj{ 177 ("x", Json.Arr{ 178 Json.Bool{True{}} <> 179 Json.Null{} <> 180 Nil{} 181 }) <> 182 Nil{} 183 } <> 184 Nil{} 185 }} 186 : 187 Result<&1, &1, Json.Error, Json.Value> 188 } 189 190 # ============================================================ 191 # JSON: Additional semantics 192 # ============================================================ 193 194 # JSON permits only space, tab, carriage return and line feed as whitespace. 195 law rejects_non_json_whitespace: 196 { Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse("\u{000b}null")) 197 == True{} : Bool } 198 199 # A raw control character is forbidden inside a JSON string. 200 law rejects_raw_string_control: 201 { Result.is_fail(&1, &1, Json.Error, Json.Value, 202 Json.parse("\"" ++ "\u{0001}" ++ "\"")) 203 == True{} : Bool } 204 205 # Unicode escapes decode to their scalar value, including a surrogate pair. 206 law parses_unicode_escape: 207 { Json.parse("\"\\u263A\"") == Done{Json.Str{"\u{263a}"}} : 208 Result<&1, &1, Json.Error, Json.Value> } 209 210 law parses_unicode_surrogate_pair: 211 { Json.parse("\"\\uD83D\\uDE00\"") == Done{Json.Str{"\u{1f600}"}} : 212 Result<&1, &1, Json.Error, Json.Value> } 213 214 # This representative decimal/exponent form is accepted. A separate law below 215 # checks that the smart number constructor preserves the original lexeme. 216 law parses_fraction_and_exponent: 217 { Result.is_done(&1, &1, Json.Error, Json.Value, Json.parse("-12.50e+3")) 218 == True{} : Bool } 219 220 law rejects_malformed_number_forms: 221 { Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse("01")) 222 && Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse("1.")) 223 && Result.is_fail(&1, &1, Json.Error, Json.Value, Json.parse("1e+")) 224 == True{} : Bool } 225 226 # Arrays retain source order. Objects retain source order and duplicate keys; 227 # consumers that need map semantics must choose their own duplicate-key policy. 228 law preserves_array_order: 229 { Json.parse("[3,1,2]") == Done{Json.Arr{ 230 Json.Number{"3", Json.Certified{Json.number_proof("3", {==})}} <> 231 Json.Number{"1", Json.Certified{Json.number_proof("1", {==})}} <> 232 Json.Number{"2", Json.Certified{Json.number_proof("2", {==})}} <> 233 Nil{} 234 }} : Result<&1, &1, Json.Error, Json.Value> } 235 236 law preserves_object_order_and_duplicates: 237 { Json.parse("{\"x\":1,\"x\":2}") == Done{Json.Obj{ 238 ("x", Json.Number{"1", Json.Certified{Json.number_proof("1", {==})}}) <> 239 ("x", Json.Number{"2", Json.Certified{Json.number_proof("2", {==})}}) <> 240 Nil{} 241 }} : Result<&1, &1, Json.Error, Json.Value> } 242 243 # GPU entry points have the same specified results as their CPU counterparts. 244 law gpu_single_matches_cpu: 245 for text: String { 246 Json.parse_gpu(text) == Json.parse(text) : 247 Result<&1, &1, Json.Error, Json.Value> 248 } 249 250 law preserves_number_lexeme: 251 { Json.number("-12.50e+3") == Done{Json.Number{ 252 "-12.50e+3", 253 Json.Certified{Json.number_proof("-12.50e+3", {==})} 254 }} : Result<&1, &1, Json.Error, Json.Value> } 255 256 law gpu_batch_matches_cpu: 257 for batch: Json.Batch { 258 Json.parse_batch_gpu(batch) == Json.parse_batch(batch) : Json.BatchResult 259 } 260 261 # ============================================================ 262 # URL component encoding 263 # ============================================================ 264 265 # Encode each UTF-8 byte with an uppercase percent escape. 266 law url_component_ascii: 267 { URL.percent_component("A") == "%41" : String } 268 269 law url_component_reserved: 270 { URL.percent_component("/") == "%2F" : String } 271 272 law url_component_utf8: 273 { URL.percent_component(SCon{Chr{233}, SNil{}}) == "%C3%A9" : String }