LAWS.bend fails

raw source on the hub · import 0x3d2147650fe101ae3c3e4a95333b4238/LAWS.bend as LAWS

Library correctness laws and integration obligations.

3 imports

import Base
import ./libs/JSON.bend as Json
import ./libs/HTTPClient.bend as HttpClient

Laws

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

{Result.is_fail(&1, &1, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Error, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Value, 0x3d2147650fe101ae3c3e4a95333b4238/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 (fails)source · line 200 · raw

{Result.is_fail(&1, &1, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Error, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Value, 0x3d2147650fe101ae3c3e4a95333b4238/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 (fails)source · line 206 · raw

{0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.parse("\"\\u263A\"") == Done{0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Str{"☺"}} : Result<&1, &1, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Error, 0x3d2147650fe101ae3c3e4a95333b4238/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 (fails)source · line 210 · raw

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

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

{Result.is_done(&1, &1, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Error, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Value, 0x3d2147650fe101ae3c3e4a95333b4238/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 (fails)source · line 220 · raw

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

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

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

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

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

@text:String -> {0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.parse_gpu(text) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.parse(text) : Result<&1, &1, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Error, 0x3d2147650fe101ae3c3e4a95333b4238/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 (fails)source · line 250 · raw

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

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

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

law http_utf8_octets openits proof in PROOF.bend does not pass the checker (fails)source · line 312 · raw

{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8("é") == [195, 169] : List<&2, U32>}

law http_binary_boundaries openits proof in PROOF.bend does not pass the checker (fails)source · line 321 · raw

{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.valid_bytes([0, 127, 128, 255]) == True{} : Bool}

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

{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.valid_bytes([256]) == False{} : Bool}

law http_https_target openits proof in PROOF.bend does not pass the checker (fails)source · line 333 · raw

{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.parse_url("https://Example.com/v1/responses?x=%2F&x=2#local") == Done{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Target{True{}, "example.com", 443, "example.com", "/v1/responses?x=%2F&x=2"}} : Result<&2, &2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Error, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Target>}

law http_http_default_path openits proof in PROOF.bend does not pass the checker (fails)source · line 337 · raw

{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.parse_url("http://example.com") == Done{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Target{False{}, "example.com", 80, "example.com", "/"}} : Result<&2, &2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Error, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Target>}

law http_query_without_path openits proof in PROOF.bend does not pass the checker (fails)source · line 341 · raw

{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.parse_url("https://example.com?q=1") == Done{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Target{True{}, "example.com", 443, "example.com", "/?q=1"}} : Result<&2, &2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Error, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Target>}

law http_nondefault_port openits proof in PROOF.bend does not pass the checker (fails)source · line 345 · raw

{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.parse_url("https://example.com:8443/a") == Done{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Target{True{}, "example.com", 8443, "example.com:8443", "/a"}} : Result<&2, &2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Error, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Target>}

law http_explicit_default_port openits proof in PROOF.bend does not pass the checker (fails)source · line 349 · raw

{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.parse_url("https://example.com:443/") == Done{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Target{True{}, "example.com", 443, "example.com", "/"}} : Result<&2, &2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Error, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Target>}

law http_signed_path_unchanged openits proof in PROOF.bend does not pass the checker (fails)source · line 353 · raw

{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.parse_url("https://example.com/a/../b%2fc?z=2&a=1&a=0") == Done{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Target{True{}, "example.com", 443, "example.com", "/a/../b%2fc?z=2&a=1&a=0"}} : Result<&2, &2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Error, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Target>}

law http_reject_unsupported_scheme openits proof in PROOF.bend does not pass the checker (fails)source · line 357 · raw

{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.parse_url("ftp://example.com/") == Fail{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.UnsupportedScheme{}} : Result<&2, &2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Error, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Target>}

law http_reject_userinfo openits proof in PROOF.bend does not pass the checker (fails)source · line 361 · raw

{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.parse_url("https://user:secret@example.com/") == Fail{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.InvalidUrl{}} : Result<&2, &2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Error, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Target>}

law http_reject_empty_host openits proof in PROOF.bend does not pass the checker (fails)source · line 365 · raw

{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.parse_url("https:///a") == Fail{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.InvalidUrl{}} : Result<&2, &2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Error, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Target>}

law http_reject_port_overflow openits proof in PROOF.bend does not pass the checker (fails)source · line 369 · raw

{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.parse_url("https://example.com:65536/") == Fail{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.InvalidUrl{}} : Result<&2, &2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Error, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Target>}

law http_reject_port_zero openits proof in PROOF.bend does not pass the checker (fails)source · line 373 · raw

{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.parse_url("https://example.com:0/") == Fail{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.InvalidUrl{}} : Result<&2, &2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Error, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Target>}

law http_reject_empty_port openits proof in PROOF.bend does not pass the checker (fails)source · line 377 · raw

{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.parse_url("https://example.com:/") == Fail{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.InvalidUrl{}} : Result<&2, &2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Error, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Target>}

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

{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.parse_url("/a") == Fail{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.InvalidUrl{}} : Result<&2, &2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Error, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Target>}

law http_reject_url_injection openits proof in PROOF.bend does not pass the checker (fails)source · line 385 · raw

{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.parse_url("https://example.com/a\r\nX: y") == Fail{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.InvalidUrl{}} : Result<&2, &2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Error, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Target>}

law http_reject_url_space openits proof in PROOF.bend does not pass the checker (fails)source · line 389 · raw

{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.parse_url("https://example.com/a b") == Fail{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.InvalidUrl{}} : Result<&2, &2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Error, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Target>}

law http_reject_invalid_escape openits proof in PROOF.bend does not pass the checker (fails)source · line 393 · raw

{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.parse_url("https://example.com/%Q0") == Fail{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.InvalidUrl{}} : Result<&2, &2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Error, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Target>}

law http_reject_unsupported_ipv6 openits proof in PROOF.bend does not pass the checker (fails)source · line 397 · raw

{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.parse_url("https://[::1]/") == Fail{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.UnsupportedHost{}} : Result<&2, &2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Error, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Target>}

law http_header_lookup_case_insensitive openits proof in PROOF.bend does not pass the checker (fails)source · line 407 · raw

{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.field_values("set-cookie", [http_header("Set-Cookie", "a=1"), http_header("X-Other", "skip"), http_header("sEt-CoOkIe", "b=2")]) == [0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8("a=1"), 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8("b=2")] : List<&2, List<&2, U32>>}

law http_header_lookup_missing openits proof in PROOF.bend does not pass the checker (fails)source · line 411 · raw

{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.field_values("missing", []) == [] : List<&2, List<&2, U32>>}

law http_encode_get openits proof in PROOF.bend does not pass the checker (fails)source · line 421 · raw

{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.encode(0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Request{"GET", "https://example.com", [], []}) == Done{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8("GET / HTTP/1.1\r\nHost: example.com\r\nAccept-Encoding: identity\r\nConnection: close\r\n\r\n")} : Result<&2, &2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Error, List<&2, U32>>}

law http_encode_head openits proof in PROOF.bend does not pass the checker (fails)source · line 425 · raw

{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.encode(0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Request{"HEAD", "https://example.com", [], []}) == Done{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8("HEAD / HTTP/1.1\r\nHost: example.com\r\nAccept-Encoding: identity\r\nConnection: close\r\n\r\n")} : Result<&2, &2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Error, List<&2, U32>>}

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

{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.encode(0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Request{"POST", "https://example.com", [], []}) == Done{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8("POST / HTTP/1.1\r\nHost: example.com\r\nContent-Length: 0\r\nAccept-Encoding: identity\r\nConnection: close\r\n\r\n")} : Result<&2, &2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Error, List<&2, U32>>}

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

{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.encode(0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Request{"PUT", "https://example.com", [], []}) == Done{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8("PUT / HTTP/1.1\r\nHost: example.com\r\nContent-Length: 0\r\nAccept-Encoding: identity\r\nConnection: close\r\n\r\n")} : Result<&2, &2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Error, List<&2, U32>>}

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

{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.encode(0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Request{"PATCH", "https://example.com", [], []}) == Done{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8("PATCH / HTTP/1.1\r\nHost: example.com\r\nContent-Length: 0\r\nAccept-Encoding: identity\r\nConnection: close\r\n\r\n")} : Result<&2, &2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Error, List<&2, U32>>}

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

{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.encode(0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Request{"DELETE", "https://example.com", [], []}) == Done{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8("DELETE / HTTP/1.1\r\nHost: example.com\r\nAccept-Encoding: identity\r\nConnection: close\r\n\r\n")} : Result<&2, &2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Error, List<&2, U32>>}

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

{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.encode(0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Request{"OPTIONS", "https://example.com", [], []}) == Done{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8("OPTIONS / HTTP/1.1\r\nHost: example.com\r\nAccept-Encoding: identity\r\nConnection: close\r\n\r\n")} : Result<&2, &2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Error, List<&2, U32>>}

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

{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.encode(0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Request{"POST", "https://example.com:8443/a?x=1&x=2", [http_header("Authorization", "Bearer sample"), http_header("Content-Type", "application/json")], 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8("é")}) == Done{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8("POST /a?x=1&x=2 HTTP/1.1\r\nHost: example.com:8443\r\nAuthorization: Bearer sample\r\nContent-Type: application/json\r\nContent-Length: 2\r\nAccept-Encoding: identity\r\nConnection: close\r\n\r\né")} : Result<&2, &2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Error, List<&2, U32>>}

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

{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.encode(0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Request{"POST", "https://example.com/", [http_header("host", "x")], []}) == Fail{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.ReservedHeader{}} : Result<&2, &2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Error, List<&2, U32>>}

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

{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.encode(0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Request{"POST", "https://example.com/", [http_header("content-length", "x")], []}) == Fail{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.ReservedHeader{}} : Result<&2, &2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Error, List<&2, U32>>}

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

{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.encode(0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Request{"POST", "https://example.com/", [http_header("transfer-encoding", "x")], []}) == Fail{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.ReservedHeader{}} : Result<&2, &2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Error, List<&2, U32>>}

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

{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.encode(0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Request{"POST", "https://example.com/", [http_header("connection", "x")], []}) == Fail{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.ReservedHeader{}} : Result<&2, &2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Error, List<&2, U32>>}

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

{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.encode(0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Request{"POST", "https://example.com/", [http_header("accept-encoding", "x")], []}) == Fail{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.ReservedHeader{}} : Result<&2, &2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Error, List<&2, U32>>}

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

{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.encode(0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Request{"POST", "https://example.com/", [http_header("expect", "x")], []}) == Fail{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.ReservedHeader{}} : Result<&2, &2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Error, List<&2, U32>>}

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

{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.encode(0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Request{"POST", "https://example.com/", [http_header("upgrade", "x")], []}) == Fail{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.ReservedHeader{}} : Result<&2, &2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Error, List<&2, U32>>}

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

{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.encode(0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Request{"POST", "https://example.com/", [http_header("trailer", "x")], []}) == Fail{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.ReservedHeader{}} : Result<&2, &2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Error, List<&2, U32>>}

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

{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.encode(0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Request{"GET", "https://example.com/", [http_header("Bad Name", "x")], []}) == Fail{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.InvalidHeader{}} : Result<&2, &2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Error, List<&2, U32>>}

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

{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.encode(0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Request{"GET", "https://example.com/", [http_header("X\r\nInjected", "x")], []}) == Fail{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.InvalidHeader{}} : Result<&2, &2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Error, List<&2, U32>>}

law http_header_value_injection openits proof in PROOF.bend does not pass the checker (fails)source · line 493 · raw

{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.encode(0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Request{"GET", "https://example.com/", [http_header("X", "ok\r\nInjected: bad")], []}) == Fail{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.InvalidHeader{}} : Result<&2, &2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Error, List<&2, U32>>}

law http_header_nul openits proof in PROOF.bend does not pass the checker (fails)source · line 497 · raw

{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.encode(0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Request{"GET", "https://example.com/", [http_header("X", "a\0b")], []}) == Fail{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.InvalidHeader{}} : Result<&2, &2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Error, List<&2, U32>>}

law http_unsupported_method openits proof in PROOF.bend does not pass the checker (fails)source · line 501 · raw

{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.encode(0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Request{"CONNECT", "https://example.com/", [], []}) == Fail{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.InvalidMethod{}} : Result<&2, &2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Error, List<&2, U32>>}

law http_body_non_octet openits proof in PROOF.bend does not pass the checker (fails)source · line 505 · raw

{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.encode(0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Request{"POST", "https://example.com/", [], [256]}) == Fail{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.InvalidByte{}} : Result<&2, &2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Error, List<&2, U32>>}

law http_encode_arbitrary_body openits proof in PROOF.bend does not pass the checker (fails)source · line 510 · raw

@+body:List<&2, U32> -> @valid:{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.valid_bytes(body) == True{} : Bool} -> {0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.encode(0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Request{"POST", "https://example.com/", [], body}) == Done{http_append(0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8(String.append("POST / HTTP/1.1\r\nHost: example.com\r\nContent-Length: ", String.append(Nat.show(http_length(body)), "\r\nAccept-Encoding: identity\r\nConnection: close\r\n\r\n"))), body)} : Result<&2, &2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Error, List<&2, U32>>}

Universal body conservation: independent list length fixes Content-Length.

law http_decode_partition_invariant openits proof in PROOF.bend does not pass the checker (fails)source · line 523 · raw

@+method:String -> @+limits:0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Limits -> @+left:List<&2, U32> -> @+right:List<&2, U32> -> @+eof:Bool -> {0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.decode_parts(method, limits, [left, right], eof) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.decode(method, limits, http_append(left, right), eof) : 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Decode}

Fragmentation invariance includes splits within CRLF, UTF-8, chunk lengths, chunk data and trailers. Includes malformed inputs, EOF and leftover bytes.

law http_decode_empty_fragments openits proof in PROOF.bend does not pass the checker (fails)source · line 533 · raw

@+method:String -> @+limits:0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Limits -> @+bytes:List<&2, U32> -> @+eof:Bool -> {0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.decode_parts(method, limits, [[], bytes, []], eof) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.decode(method, limits, bytes, eof) : 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Decode}

law http_content_length openits proof in PROOF.bend does not pass the checker (fails)source · line 561 · raw

{http_decode("GET", "HTTP/1.1 200 OK\r\nContent-Length: 3\r\n\r\nabc", False{}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Parsed{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Response{200, [http_header("Content-Length", "3")], 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8("abc"), []}, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8("")} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Decode}

law http_preserve_remainder openits proof in PROOF.bend does not pass the checker (fails)source · line 565 · raw

{http_decode("GET", "HTTP/1.1 200 OK\r\nContent-Length: 3\r\n\r\nabcNEXT", False{}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Parsed{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Response{200, [http_header("Content-Length", "3")], 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8("abc"), []}, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8("NEXT")} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Decode}

law http_partial_body openits proof in PROOF.bend does not pass the checker (fails)source · line 569 · raw

{http_decode("GET", "HTTP/1.1 200 OK\r\nContent-Length: 3\r\n\r\nab", False{}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.NeedMore{} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Decode}

law http_truncated_body openits proof in PROOF.bend does not pass the checker (fails)source · line 573 · raw

{http_decode("GET", "HTTP/1.1 200 OK\r\nContent-Length: 3\r\n\r\nab", True{}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Rejected{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.UnexpectedEof{}} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Decode}

law http_incomplete_headers openits proof in PROOF.bend does not pass the checker (fails)source · line 577 · raw

{http_decode("GET", "HTTP/1.1 200 OK\r\nContent-Length: 0\r", False{}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.NeedMore{} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Decode}

law http_empty_eof openits proof in PROOF.bend does not pass the checker (fails)source · line 581 · raw

{http_decode("GET", "", True{}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Rejected{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.UnexpectedEof{}} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Decode}

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

{http_decode("GET", "HTTP/1.1 200 OK\r\n\r\nabc", False{}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.NeedMore{} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Decode}

law http_close_delimited_eof openits proof in PROOF.bend does not pass the checker (fails)source · line 589 · raw

{http_decode("GET", "HTTP/1.1 200 OK\r\n\r\nabc", True{}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Parsed{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Response{200, [], 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8("abc"), []}, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8("")} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Decode}

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

{http_decode("HEAD", "HTTP/1.1 200 OK\r\nContent-Length: 9999999\r\n\r\nNEXT", False{}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Parsed{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Response{200, [http_header("Content-Length", "9999999")], 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8(""), []}, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8("NEXT")} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Decode}

law http_no_content openits proof in PROOF.bend does not pass the checker (fails)source · line 597 · raw

{http_decode("GET", "HTTP/1.1 204 No Content\r\n\r\nNEXT", False{}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Parsed{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Response{204, [], 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8(""), []}, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8("NEXT")} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Decode}

law http_not_modified openits proof in PROOF.bend does not pass the checker (fails)source · line 601 · raw

{http_decode("GET", "HTTP/1.1 304 Not Modified\r\nContent-Length: 100\r\n\r\nNEXT", False{}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Parsed{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Response{304, [http_header("Content-Length", "100")], 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8(""), []}, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8("NEXT")} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Decode}

law http_reset_content_still_framed openits proof in PROOF.bend does not pass the checker (fails)source · line 605 · raw

{http_decode("GET", "HTTP/1.1 205 Reset Content\r\nContent-Length: 0\r\n\r\nNEXT", False{}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Parsed{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Response{205, [http_header("Content-Length", "0")], 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8(""), []}, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8("NEXT")} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Decode}

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

{http_decode("GET", "HTTP/1.1 100 Continue\r\n\r\nHTTP/1.1 103 Early Hints\r\n\r\nHTTP/1.1 200 OK\r\nContent-Length: 3\r\n\r\nabc", False{}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Parsed{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Response{200, [http_header("Content-Length", "3")], 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8("abc"), []}, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8("")} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Decode}

law http_interim_without_final openits proof in PROOF.bend does not pass the checker (fails)source · line 613 · raw

{http_decode("GET", "HTTP/1.1 100 Continue\r\n\r\n", True{}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Rejected{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.UnexpectedEof{}} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Decode}

law http_status_301_is_response openits proof in PROOF.bend does not pass the checker (fails)source · line 617 · raw

{http_decode("GET", "HTTP/1.1 301 Status\r\nContent-Length: 3\r\n\r\nerr", False{}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Parsed{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Response{301, [http_header("Content-Length", "3")], 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8("err"), []}, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8("")} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Decode}

law http_status_400_is_response openits proof in PROOF.bend does not pass the checker (fails)source · line 621 · raw

{http_decode("GET", "HTTP/1.1 400 Status\r\nContent-Length: 3\r\n\r\nerr", False{}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Parsed{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Response{400, [http_header("Content-Length", "3")], 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8("err"), []}, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8("")} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Decode}

law http_status_401_is_response openits proof in PROOF.bend does not pass the checker (fails)source · line 625 · raw

{http_decode("GET", "HTTP/1.1 401 Status\r\nContent-Length: 3\r\n\r\nerr", False{}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Parsed{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Response{401, [http_header("Content-Length", "3")], 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8("err"), []}, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8("")} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Decode}

law http_status_403_is_response openits proof in PROOF.bend does not pass the checker (fails)source · line 629 · raw

{http_decode("GET", "HTTP/1.1 403 Status\r\nContent-Length: 3\r\n\r\nerr", False{}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Parsed{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Response{403, [http_header("Content-Length", "3")], 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8("err"), []}, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8("")} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Decode}

law http_status_404_is_response openits proof in PROOF.bend does not pass the checker (fails)source · line 633 · raw

{http_decode("GET", "HTTP/1.1 404 Status\r\nContent-Length: 3\r\n\r\nerr", False{}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Parsed{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Response{404, [http_header("Content-Length", "3")], 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8("err"), []}, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8("")} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Decode}

law http_status_429_is_response openits proof in PROOF.bend does not pass the checker (fails)source · line 637 · raw

{http_decode("GET", "HTTP/1.1 429 Status\r\nContent-Length: 3\r\n\r\nerr", False{}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Parsed{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Response{429, [http_header("Content-Length", "3")], 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8("err"), []}, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8("")} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Decode}

law http_status_500_is_response openits proof in PROOF.bend does not pass the checker (fails)source · line 641 · raw

{http_decode("GET", "HTTP/1.1 500 Status\r\nContent-Length: 3\r\n\r\nerr", False{}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Parsed{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Response{500, [http_header("Content-Length", "3")], 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8("err"), []}, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8("")} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Decode}

law http_status_503_is_response openits proof in PROOF.bend does not pass the checker (fails)source · line 645 · raw

{http_decode("GET", "HTTP/1.1 503 Status\r\nContent-Length: 3\r\n\r\nerr", False{}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Parsed{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Response{503, [http_header("Content-Length", "3")], 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8("err"), []}, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8("")} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Decode}

law http_header_value_trimming openits proof in PROOF.bend does not pass the checker (fails)source · line 649 · raw

{http_decode("GET", "HTTP/1.1 200 OK\r\ncOnTeNt-LeNgTh:\t3 \t\r\nSet-Cookie: a=1\r\nSet-Cookie: b=2\r\n\r\nabc", False{}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Parsed{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Response{200, [http_header("cOnTeNt-LeNgTh", "3"), http_header("Set-Cookie", "a=1"), http_header("Set-Cookie", "b=2")], 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8("abc"), []}, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8("")} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Decode}

law http_chunked openits proof in PROOF.bend does not pass the checker (fails)source · line 659 · raw

{http_decode("GET", "HTTP/1.1 200 OK\r\nTransfer-Encoding: chunked\r\n\r\n2\r\nab\r\n1\r\nc\r\n0\r\n\r\nNEXT", False{}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Parsed{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Response{200, [http_header("Transfer-Encoding", "chunked")], 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8("abc"), []}, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8("NEXT")} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Decode}

law http_chunk_extensions_trailers openits proof in PROOF.bend does not pass the checker (fails)source · line 663 · raw

{http_decode("GET", "HTTP/1.1 200 OK\r\nTransfer-Encoding: chunked\r\n\r\n3;foo=\"bar\"\r\nabc\r\n0\r\nX-End: yes\r\nX-End: again\r\n\r\n", False{}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Parsed{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Response{200, [http_header("Transfer-Encoding", "chunked")], 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8("abc"), [http_header("X-End", "yes"), http_header("X-End", "again")]}, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8("")} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Decode}

law http_uppercase_hex_chunk openits proof in PROOF.bend does not pass the checker (fails)source · line 667 · raw

{http_decode("GET", "HTTP/1.1 200 OK\r\nTransfer-Encoding: chunked\r\n\r\nA\r\n0123456789\r\n0\r\n\r\n", False{}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Parsed{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Response{200, [http_header("Transfer-Encoding", "chunked")], 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8("0123456789"), []}, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8("")} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Decode}

law http_chunk_truncation openits proof in PROOF.bend does not pass the checker (fails)source · line 671 · raw

{http_decode("GET", "HTTP/1.1 200 OK\r\nTransfer-Encoding: chunked\r\n\r\n3\r\nab", True{}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Rejected{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.UnexpectedEof{}} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Decode}

law http_chunk_incomplete openits proof in PROOF.bend does not pass the checker (fails)source · line 675 · raw

{http_decode("GET", "HTTP/1.1 200 OK\r\nTransfer-Encoding: chunked\r\n\r\n3\r\nab", False{}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.NeedMore{} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Decode}

law http_missing_final_chunk openits proof in PROOF.bend does not pass the checker (fails)source · line 679 · raw

{http_decode("GET", "HTTP/1.1 200 OK\r\nTransfer-Encoding: chunked\r\n\r\n3\r\nabc\r\n", True{}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Rejected{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.UnexpectedEof{}} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Decode}

law http_unfinished_trailers openits proof in PROOF.bend does not pass the checker (fails)source · line 683 · raw

{http_decode("GET", "HTTP/1.1 200 OK\r\nTransfer-Encoding: chunked\r\n\r\n0\r\nX-End: yes\r\n", True{}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Rejected{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.UnexpectedEof{}} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Decode}

law http_reject_duplicate_equal_length openits proof in PROOF.bend does not pass the checker (fails)source · line 693 · raw

{http_decode("GET", "HTTP/1.1 200 OK\r\nContent-Length: 3\r\nContent-Length: 3\r\n\r\nabc", True{}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Rejected{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.InvalidFraming{}} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Decode}

law http_reject_conflicting_length openits proof in PROOF.bend does not pass the checker (fails)source · line 697 · raw

{http_decode("GET", "HTTP/1.1 200 OK\r\nContent-Length: 3\r\nContent-Length: 4\r\n\r\nabc", True{}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Rejected{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.InvalidFraming{}} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Decode}

law http_reject_length_list openits proof in PROOF.bend does not pass the checker (fails)source · line 701 · raw

{http_decode("GET", "HTTP/1.1 200 OK\r\nContent-Length: 3, 3\r\n\r\nabc", True{}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Rejected{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.InvalidFraming{}} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Decode}

law http_reject_te_and_cl openits proof in PROOF.bend does not pass the checker (fails)source · line 705 · raw

{http_decode("GET", "HTTP/1.1 200 OK\r\nTransfer-Encoding: chunked\r\nContent-Length: 3\r\n\r\n", True{}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Rejected{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.InvalidFraming{}} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Decode}

law http_reject_negative_length openits proof in PROOF.bend does not pass the checker (fails)source · line 709 · raw

{http_decode("GET", "HTTP/1.1 200 OK\r\nContent-Length: -1\r\n\r\n", True{}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Rejected{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.InvalidFraming{}} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Decode}

law http_reject_huge_length openits proof in PROOF.bend does not pass the checker (fails)source · line 713 · raw

{http_decode("GET", "HTTP/1.1 200 OK\r\nContent-Length: 18446744073709551616\r\n\r\n", True{}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Rejected{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.LimitExceeded{}} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Decode}

law http_reject_huge_chunk openits proof in PROOF.bend does not pass the checker (fails)source · line 717 · raw

{http_decode("GET", "HTTP/1.1 200 OK\r\nTransfer-Encoding: chunked\r\n\r\n10000000000000000\r\n", True{}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Rejected{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.LimitExceeded{}} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Decode}

law http_reject_bad_transfer_coding openits proof in PROOF.bend does not pass the checker (fails)source · line 721 · raw

{http_decode("GET", "HTTP/1.1 200 OK\r\nTransfer-Encoding: gzip, chunked\r\n\r\n", True{}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Rejected{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.UnsupportedTransferEncoding{}} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Decode}

law http_reject_repeated_chunked openits proof in PROOF.bend does not pass the checker (fails)source · line 725 · raw

{http_decode("GET", "HTTP/1.1 200 OK\r\nTransfer-Encoding: chunked, chunked\r\n\r\n", True{}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Rejected{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.InvalidFraming{}} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Decode}

law http_reject_bad_chunk_size openits proof in PROOF.bend does not pass the checker (fails)source · line 729 · raw

{http_decode("GET", "HTTP/1.1 200 OK\r\nTransfer-Encoding: chunked\r\n\r\nZ\r\n", True{}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Rejected{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.InvalidFraming{}} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Decode}

law http_reject_bad_chunk_terminator openits proof in PROOF.bend does not pass the checker (fails)source · line 733 · raw

{http_decode("GET", "HTTP/1.1 200 OK\r\nTransfer-Encoding: chunked\r\n\r\n1\r\naXX", True{}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Rejected{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.InvalidFraming{}} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Decode}

law http_reject_forbidden_trailer openits proof in PROOF.bend does not pass the checker (fails)source · line 737 · raw

{http_decode("GET", "HTTP/1.1 200 OK\r\nTransfer-Encoding: chunked\r\n\r\n0\r\nContent-Length: 0\r\n\r\n", True{}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Rejected{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.InvalidFraming{}} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Decode}

law http_reject_bare_lf openits proof in PROOF.bend does not pass the checker (fails)source · line 741 · raw

{http_decode("GET", "HTTP/1.1 200 OK\nContent-Length: 0\n\n", True{}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Rejected{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.InvalidFraming{}} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Decode}

law http_reject_obsolete_fold openits proof in PROOF.bend does not pass the checker (fails)source · line 745 · raw

{http_decode("GET", "HTTP/1.1 200 OK\r\nX: a\r\n b\r\n\r\n", True{}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Rejected{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.InvalidHeader{}} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Decode}

law http_reject_space_before_colon openits proof in PROOF.bend does not pass the checker (fails)source · line 749 · raw

{http_decode("GET", "HTTP/1.1 200 OK\r\nX : a\r\n\r\n", True{}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Rejected{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.InvalidHeader{}} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Decode}

law http_reject_invalid_status openits proof in PROOF.bend does not pass the checker (fails)source · line 753 · raw

{http_decode("GET", "HTTP/1.1 20 OK\r\n\r\n", True{}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Rejected{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.InvalidStatus{}} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Decode}

law http_reject_invalid_version openits proof in PROOF.bend does not pass the checker (fails)source · line 757 · raw

{http_decode("GET", "HTTP/2.0 200 OK\r\n\r\n", True{}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Rejected{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.InvalidVersion{}} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Decode}

law http_accept_http_10_response openits proof in PROOF.bend does not pass the checker (fails)source · line 761 · raw

{http_decode("GET", "HTTP/1.0 200 OK\r\nContent-Length: 2\r\n\r\nok", False{}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Parsed{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Response{200, [http_header("Content-Length", "2")], 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8("ok"), []}, []} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Decode}

law http_reject_upgrade openits proof in PROOF.bend does not pass the checker (fails)source · line 765 · raw

{http_decode("GET", "HTTP/1.1 101 Switching Protocols\r\n\r\n", True{}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Rejected{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.UnsupportedUpgrade{}} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Decode}

law http_body_limit_exact openits proof in PROOF.bend does not pass the checker (fails)source · line 775 · raw

{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.decode("GET", 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Limits{16384, 100, 3, 8192, 50, 8, 1024, 2097152}, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8("HTTP/1.1 200 OK\r\nContent-Length: 3\r\n\r\nabc"), False{}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Parsed{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Response{200, [http_header("Content-Length", "3")], 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8("abc"), []}, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8("")} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Decode}

law http_body_limit_over openits proof in PROOF.bend does not pass the checker (fails)source · line 779 · raw

{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.decode("GET", 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Limits{16384, 100, 3, 8192, 50, 8, 1024, 2097152}, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8("HTTP/1.1 200 OK\r\nContent-Length: 4\r\n\r\nabcd"), False{}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Rejected{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.LimitExceeded{}} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Decode}

law http_chunk_body_limit_over openits proof in PROOF.bend does not pass the checker (fails)source · line 783 · raw

{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.decode("GET", 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Limits{16384, 100, 3, 8192, 50, 8, 1024, 2097152}, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8("HTTP/1.1 200 OK\r\nTransfer-Encoding: chunked\r\n\r\n2\r\nab\r\n2\r\ncd\r\n0\r\n\r\n"), False{}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Rejected{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.LimitExceeded{}} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Decode}

law http_close_body_limit_over openits proof in PROOF.bend does not pass the checker (fails)source · line 787 · raw

{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.decode("GET", 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Limits{16384, 100, 3, 8192, 50, 8, 1024, 2097152}, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8("HTTP/1.1 200 OK\r\n\r\nabcd"), True{}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Rejected{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.LimitExceeded{}} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Decode}

law http_header_bytes_exact openits proof in PROOF.bend does not pass the checker (fails)source · line 791 · raw

{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.decode("GET", 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Limits{38, 100, 1048576, 8192, 50, 8, 1024, 2097152}, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8("HTTP/1.1 200 OK\r\nContent-Length: 0\r\n\r\n"), False{}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Parsed{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Response{200, [http_header("Content-Length", "0")], 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8(""), []}, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8("")} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Decode}

law http_header_bytes_over openits proof in PROOF.bend does not pass the checker (fails)source · line 795 · raw

{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.decode("GET", 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Limits{37, 100, 1048576, 8192, 50, 8, 1024, 2097152}, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8("HTTP/1.1 200 OK\r\nContent-Length: 0\r\n\r\n"), False{}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Rejected{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.LimitExceeded{}} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Decode}

law http_wire_bytes_exact openits proof in PROOF.bend does not pass the checker (fails)source · line 799 · raw

{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.decode("GET", 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Limits{16384, 100, 1048576, 8192, 50, 8, 1024, 38}, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8("HTTP/1.1 200 OK\r\nContent-Length: 0\r\n\r\n"), False{}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Parsed{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Response{200, [http_header("Content-Length", "0")], 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8(""), []}, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8("")} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Decode}

law http_wire_bytes_over openits proof in PROOF.bend does not pass the checker (fails)source · line 803 · raw

{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.decode("GET", 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Limits{16384, 100, 1048576, 8192, 50, 8, 1024, 37}, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8("HTTP/1.1 200 OK\r\nContent-Length: 0\r\n\r\n"), False{}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Rejected{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.LimitExceeded{}} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Decode}

law http_wire_bytes_excludes_remainder openits proof in PROOF.bend does not pass the checker (fails)source · line 809 · raw

{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.decode("GET", 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Limits{16384, 100, 1048576, 8192, 50, 8, 1024, 38}, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8("HTTP/1.1 200 OK\r\nContent-Length: 0\r\n\r\nNEXT"), False{}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Parsed{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Response{200, [http_header("Content-Length", "0")], 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8(""), []}, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8("NEXT")} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Decode}

Bytes after the first complete response are returned untouched and do not consume that response's wire budget.

law http_header_count_over openits proof in PROOF.bend does not pass the checker (fails)source · line 813 · raw

{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.decode("GET", 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Limits{16384, 0, 1048576, 8192, 50, 8, 1024, 2097152}, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8("HTTP/1.1 200 OK\r\nContent-Length: 0\r\n\r\n"), False{}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Rejected{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.LimitExceeded{}} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Decode}

law http_interim_count_over openits proof in PROOF.bend does not pass the checker (fails)source · line 817 · raw

{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.decode("GET", 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Limits{16384, 100, 1048576, 8192, 50, 0, 1024, 2097152}, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8("HTTP/1.1 100 Continue\r\n\r\nHTTP/1.1 200 OK\r\nContent-Length: 0\r\n\r\n"), False{}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Rejected{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.LimitExceeded{}} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Decode}

law http_trailer_count_over openits proof in PROOF.bend does not pass the checker (fails)source · line 821 · raw

{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.decode("GET", 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Limits{16384, 100, 1048576, 8192, 0, 8, 1024, 2097152}, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8("HTTP/1.1 200 OK\r\nTransfer-Encoding: chunked\r\n\r\n0\r\nX: y\r\n\r\n"), False{}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Rejected{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.LimitExceeded{}} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Decode}

law http_trailer_bytes_over openits proof in PROOF.bend does not pass the checker (fails)source · line 825 · raw

{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.decode("GET", 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Limits{16384, 100, 1048576, 7, 50, 8, 1024, 2097152}, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8("HTTP/1.1 200 OK\r\nTransfer-Encoding: chunked\r\n\r\n0\r\nX: y\r\n\r\n"), False{}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Rejected{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.LimitExceeded{}} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Decode}

law http_chunk_line_bytes_over openits proof in PROOF.bend does not pass the checker (fails)source · line 829 · raw

{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.decode("GET", 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Limits{16384, 100, 1048576, 8192, 50, 8, 3, 2097152}, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8("HTTP/1.1 200 OK\r\nTransfer-Encoding: chunked\r\n\r\n0;foo=bar\r\n\r\n"), False{}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Rejected{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.LimitExceeded{}} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Decode}

law http_partial_write openits proof in PROOF.bend does not pass the checker (fails)source · line 839 · raw

{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.drop_written([0, 255, 1, 2], 2) == Done{[1, 2]} : Result<&2, &2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Error, List<&2, U32>>}

law http_full_write openits proof in PROOF.bend does not pass the checker (fails)source · line 843 · raw

{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.drop_written([0, 255], 2) == Done{[]} : Result<&2, &2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Error, List<&2, U32>>}

law http_empty_write openits proof in PROOF.bend does not pass the checker (fails)source · line 847 · raw

{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.drop_written([], 0) == Done{[]} : Result<&2, &2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Error, List<&2, U32>>}

law http_zero_write_progress openits proof in PROOF.bend does not pass the checker (fails)source · line 851 · raw

{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.drop_written([1], 0) == Fail{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.NoProgress{}} : Result<&2, &2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Error, List<&2, U32>>}

law http_write_overreport openits proof in PROOF.bend does not pass the checker (fails)source · line 855 · raw

{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.drop_written([1], 2) == Fail{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.InvalidFraming{}} : Result<&2, &2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Error, List<&2, U32>>}

law http_json_error_response openits proof in PROOF.bend does not pass the checker (fails)source · line 873 · raw

{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.read_json(0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Response{400, [], 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8("null"), []}) == Done{0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Null{}} : Result<&1, &1, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Error, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Value>}

law http_json_empty openits proof in PROOF.bend does not pass the checker (fails)source · line 877 · raw

{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.read_json(0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Response{204, [], 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8(""), []}) == Fail{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.InvalidJson{}} : Result<&1, &1, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Error, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Value>}

law http_json_trailing openits proof in PROOF.bend does not pass the checker (fails)source · line 881 · raw

{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.read_json(0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Response{200, [], 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8("{}oops"), []}) == Fail{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.InvalidJson{}} : Result<&1, &1, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Error, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Value>}

law http_json_compressed openits proof in PROOF.bend does not pass the checker (fails)source · line 885 · raw

{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.read_json(0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Response{200, [http_header("Content-Encoding", "gzip")], 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8("{}"), []}) == Fail{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.UnsupportedContentEncoding{}} : Result<&1, &1, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Error, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Value>}

law http_json_invalid_utf8 openits proof in PROOF.bend does not pass the checker (fails)source · line 889 · raw

{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.read_json(0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Response{200, [], [255], []}) == Fail{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.InvalidUtf8{}} : Result<&1, &1, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Error, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Value>}

law http_gpu_encode_matches_cpu openits proof in PROOF.bend does not pass the checker (fails)source · line 901 · raw

@+request:0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Request -> {0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.encode_gpu(request) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.encode(request) : Result<&2, &2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Error, List<&2, U32>>}

law http_gpu_decode_matches_cpu openits proof in PROOF.bend does not pass the checker (fails)source · line 907 · raw

@+method:String -> @+limits:0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Limits -> @+bytes:List<&2, U32> -> @+eof:Bool -> {0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.decode_gpu(method, limits, bytes, eof) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.decode(method, limits, bytes, eof) : 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Decode}

law http_gpu_json_matches_cpu openits proof in PROOF.bend does not pass the checker (fails)source · line 916 · raw

@+response:0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Response -> {0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.read_json_gpu(response) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.read_json(response) : Result<&1, &1, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Error, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Value>}

law http_work_encode_uses_codec openits proof in PROOF.bend does not pass the checker (fails)source · line 922 · raw

@+request:0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Request -> {0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.run_work(0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.EncodeWork{request}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Encoded{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.encode(request)} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Outcome}

law http_work_decode_uses_codec openits proof in PROOF.bend does not pass the checker (fails)source · line 928 · raw

@+method:String -> @+limits:0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Limits -> @+bytes:List<&2, U32> -> @+eof:Bool -> {0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.run_work(0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.DecodeWork{method, limits, bytes, eof}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Decoded{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.decode(method, limits, bytes, eof)} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Outcome}

law http_batch_leaf openits proof in PROOF.bend does not pass the checker (fails)source · line 937 · raw

@+work:0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Work -> {0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.run_batch(0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Leaf{work}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.LeafResult{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.run_work(work)} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.BatchResult}

law http_batch_fork openits proof in PROOF.bend does not pass the checker (fails)source · line 943 · raw

@+left:0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Batch -> @+right:0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Batch -> {0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.run_batch(0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Fork{left, right}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.ForkResult{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.run_batch(left), 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.run_batch(right)} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.BatchResult}

law http_gpu_batch_matches_cpu openits proof in PROOF.bend does not pass the checker (fails)source · line 951 · raw

@+batch:0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Batch -> {0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.run_batch_gpu(batch) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.run_batch(batch) : 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.BatchResult}

law http_gpu_many_matches_cpu openits proof in PROOF.bend does not pass the checker (fails)source · line 956 · raw

@+jobs:List<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Work> -> {0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.run_many_gpu(jobs) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.run_many(jobs) : Maybe<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.BatchResult>}

law http_empty_batch_builder openits proof in PROOF.bend does not pass the checker (fails)source · line 962 · raw

{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.batch_from_list([]) == None{} : Maybe<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Batch>}

law http_singleton_batch_builder openits proof in PROOF.bend does not pass the checker (fails)source · line 965 · raw

@+work:0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Work -> {0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.batch_from_list([work]) == Some{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Leaf{work}} : Maybe<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Batch>}

law http_empty_gpu_many openits proof in PROOF.bend does not pass the checker (fails)source · line 971 · raw

{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.run_many_gpu([]) == None{} : Maybe<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.BatchResult>}

law http_singleton_gpu_many openits proof in PROOF.bend does not pass the checker (fails)source · line 974 · raw

@+work:0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Work -> {0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.run_many_gpu([work]) == Some{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.LeafResult{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.run_work(work)}} : Maybe<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.BatchResult>}

law http_gpu_batch_preserves_order_and_errors openits proof in PROOF.bend does not pass the checker (fails)source · line 999 · raw

@+jobs:List<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Work> -> {http_optional_outcomes(0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.run_many_gpu(jobs)) == http_expected_outcomes(jobs) : List<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Outcome>}

law http_flatten_leaf openits proof in PROOF.bend does not pass the checker (fails)source · line 1005 · raw

@+outcome:0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Outcome -> {0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.flatten_results(0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.LeafResult{outcome}) == [outcome] : List<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Outcome>}

law http_flatten_fork openits proof in PROOF.bend does not pass the checker (fails)source · line 1017 · raw

@+left:0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.BatchResult -> @+right:0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.BatchResult -> {0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.flatten_results(0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.ForkResult{left, right}) == http_append_outcomes(0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.flatten_results(left), 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.flatten_results(right)) : List<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Outcome>}

Definitions

def http_append source · line 276 · raw

@xs:List<&2, U32> -> @ys:List<&2, U32> -> List<&2, U32>

Independent specification helpers; do not delegate these to HTTP helpers.

def http_length source · line 281 · raw

@xs:List<&2, U32> -> Nat

def http_limits source · line 289 · raw

0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Limits

Header cap includes the status line and terminating blank line, per head. Trailer cap includes its terminating blank line. Chunk-line cap includes CRLF. Body cap counts decoded payload; wire cap counts consumed framing and payload.

def http_header source · line 292 · raw

@name:String -> @value:String -> 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Header

def http_decode source · line 295 · raw

@method:String -> @text:String -> @eof:Bool -> 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Decode

def http_unicode_scalar source · line 300 · raw

@+c:U32 -> Bool

JSON wire roundtrips are defined for Unicode scalar strings. Bend's String type permits arbitrary U32 characters, while HTTP JSON crosses strict UTF-8.

def http_unicode_string source · line 303 · raw

@text:String -> Bool

def http_expected_outcome source · line 982 · raw

@work:0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Work -> 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Outcome

The sequential oracle calls the codec directly, not run_work/run_many. This prevents two identically wrong batch implementations satisfying parity.

def http_expected_outcomes source · line 988 · raw

@jobs:List<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Work> -> List<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Outcome>

def http_optional_outcomes source · line 994 · raw

@result:Maybe<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.BatchResult> -> List<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Outcome>

def http_append_outcomes source · line 1011 · raw

@xs:List<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Outcome> -> @ys:List<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Outcome> -> List<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Outcome>