~/bend-docscommunity

proof/HTTPClientProof.bend fails

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

6 imports
import Base
import ../LAWS.bend as L
import ../libs/JSON.bend as Json
import ../libs/HTTPClient.bend as HttpClient
import 0xcfc8be7b076f41f95c8e118383892d55/encoding.bend as Encoding
import 0x49814d83de8f70993a43e1002be29ecd/bytes.bend as Bytes

Definitions

def http_encode_accepts_valid_body source · line 137 · raw

@+body:List<&2, U32> -> @valid:{0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.valid_bytes(body) == True{} : Bool} -> {0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.encode_checked("POST", 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Target{True{}, "example.com", 443, "example.com", "/"}, [], body, True{}, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.valid_bytes(body), Done{Unit{}}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.encode_checked("POST", 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Target{True{}, "example.com", 443, "example.com", "/"}, [], body, True{}, True{}, Done{Unit{}}) : Result<&2, &2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Error, List<&2, U32>>}

def http_length_same source · line 143 · raw

@+body:List<&2, U32> -> {List.length(&2, U32, body) == 0x3d2147650fe101ae3c3e4a95333b4238/LAWS.http_length(body) : Nat}

def append_bytes_assoc source · line 150 · raw

@+x:List<&2, U32> -> @+y:List<&2, U32> -> @+z:List<&2, U32> -> {0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.append_bytes(0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.append_bytes(x, y), z) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.append_bytes(x, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.append_bytes(y, z)) : List<&2, U32>}

def utf8_append_same source · line 160 · raw

@+x:String -> @+y:String -> {0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8(String.append(x, y)) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.append_bytes(0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8(x), 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8(y)) : List<&2, U32>}

def http_append_outcomes_same source · line 453 · raw

@+xs:List<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Outcome> -> @+ys:List<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Outcome> -> {0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.append_outcomes(xs, ys) == 0x3d2147650fe101ae3c3e4a95333b4238/LAWS.http_append_outcomes(xs, ys) : List<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Outcome>}

def flatten_empty_edges source · line 468 · raw

@+bytes:List<&2, U32> -> {0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.flatten_bytes([[], bytes, []]) == bytes : List<&2, U32>}

def append_bytes_nil source · line 473 · raw

@+bytes:List<&2, U32> -> {0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.append_bytes(bytes, []) == bytes : List<&2, U32>}

def flatten_bytes_pair source · line 480 · raw

@+left:List<&2, U32> -> @+right:List<&2, U32> -> {0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.flatten_bytes([left, right]) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.append_bytes(left, right) : List<&2, U32>}

def append_bytes_same source · line 489 · raw

@+left:List<&2, U32> -> @+right:List<&2, U32> -> {0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.append_bytes(left, right) == 0x3d2147650fe101ae3c3e4a95333b4238/LAWS.http_append(left, right) : List<&2, U32>}

def string_append_assoc source · line 497 · raw

@+x:String -> @+y:String -> @+z:String -> {String.append(String.append(x, y), z) == String.append(x, String.append(y, z)) : String}

def http_concat_tail source · line 506 · raw

@+x:String -> @+y:String -> @+body:List<&2, U32> -> {0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.append_bytes(0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8(x), 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.append_bytes(0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8(y), body)) == 0x3d2147650fe101ae3c3e4a95333b4238/LAWS.http_append(0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.utf8(String.append(x, y)), body) : List<&2, U32>}

def http_encode_body_core source · line 527 · raw

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

def http_read_json_select_parity source · line 582 · raw

@+text:String -> @encoding_ok:Bool -> @is_utf8:Bool -> {0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.read_json_select(text, encoding_ok, is_utf8, True{}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.read_json_select(text, encoding_ok, is_utf8, False{}) : Result<&1, &1, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Error, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Value>}

def http_expected_batch source · line 603 · raw

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

def http_run_work_expected source · line 609 · raw

@work:0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Work -> {0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.run_work(work) == 0x3d2147650fe101ae3c3e4a95333b4238/LAWS.http_expected_outcome(work) : 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Outcome}

def http_batch_cpu_expected source · line 614 · raw

@+batch:0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Batch -> {0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.flatten_results(0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.run_batch(batch)) == http_expected_batch(batch) : List<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Outcome>}

def http_batch_gpu_expected source · line 634 · raw

@+batch:0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Batch -> {0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.flatten_results(0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.run_batch_gpu(batch)) == http_expected_batch(batch) : List<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Outcome>}

def http_append_work source · line 641 · raw

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

def http_append_work_assoc source · line 647 · raw

@+xs:List<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Work> -> @+ys:List<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Work> -> @+zs:List<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Work> -> {http_append_work(xs, http_append_work(ys, zs)) == http_append_work(http_append_work(xs, ys), zs) : List<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Work>}

def http_append_work_nil source · line 657 · raw

@+xs:List<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Work> -> {http_append_work(xs, []) == xs : List<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Work>}

def http_batch_work_order source · line 664 · raw

@+batch:0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Batch -> List<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Work>

def http_batches_work_order source · line 670 · raw

@+batches:List<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Batch> -> List<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Work>

def http_batch_pairs_work_order source · line 676 · raw

@+batches:List<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Batch> -> {http_batches_work_order(0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.batch_pairs(batches)) == http_batches_work_order(batches) : List<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Work>}

def http_optional_batch_work_order source · line 697 · raw

@batch:Maybe<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Batch> -> List<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Work>

def http_batch_fold_result_order source · line 702 · raw

@head:0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Batch -> @rest:Maybe<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Batch> -> @+tail:List<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Batch> -> @rest_order:{http_optional_batch_work_order(rest) == http_batches_work_order(tail) : List<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Work>} -> {http_optional_batch_work_order(0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.batch_fold_result(head, rest)) == http_append_work(http_batch_work_order(head), http_batches_work_order(tail)) : List<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Work>}

def http_batch_fold_work_order source · line 719 · raw

@+batches:List<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Batch> -> {http_optional_batch_work_order(0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.batch_fold(batches)) == http_batches_work_order(batches) : List<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Work>}

def http_batch_build_work_order source · line 725 · raw

@fuel:Nat -> @+batches:List<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Batch> -> {http_optional_batch_work_order(0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.batch_build(fuel, batches)) == http_batches_work_order(batches) : List<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Work>}

def http_batch_leaves_work_order source · line 743 · raw

@+jobs:List<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Work> -> {http_batches_work_order(0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.batch_leaves(jobs)) == jobs : List<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Work>}

def http_batch_from_list_work_order source · line 750 · raw

@+jobs:List<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Work> -> {http_optional_batch_work_order(0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.batch_from_list(jobs)) == jobs : List<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Work>}

def http_expected_outcomes_append source · line 757 · raw

@+xs:List<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Work> -> @+ys:List<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Work> -> {0x3d2147650fe101ae3c3e4a95333b4238/LAWS.http_expected_outcomes(http_append_work(xs, ys)) == 0x3d2147650fe101ae3c3e4a95333b4238/LAWS.http_append_outcomes(0x3d2147650fe101ae3c3e4a95333b4238/LAWS.http_expected_outcomes(xs), 0x3d2147650fe101ae3c3e4a95333b4238/LAWS.http_expected_outcomes(ys)) : List<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Outcome>}

def http_expected_batch_work_order source · line 767 · raw

@+batch:0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Batch -> {http_expected_batch(batch) == 0x3d2147650fe101ae3c3e4a95333b4238/LAWS.http_expected_outcomes(http_batch_work_order(batch)) : List<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Outcome>}

def http_optional_gpu_expected source · line 793 · raw

@batch:Maybe<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Batch> -> @+jobs:List<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Work> -> @batch_order:{http_optional_batch_work_order(batch) == jobs : List<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Work>} -> {0x3d2147650fe101ae3c3e4a95333b4238/LAWS.http_optional_outcomes(0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.run_many_gpu_tree(batch)) == 0x3d2147650fe101ae3c3e4a95333b4238/LAWS.http_expected_outcomes(jobs) : List<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Outcome>}

def http_run_many_gpu_expected source · line 813 · raw

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

def http_run_many_tree_parity source · line 816 · raw

@tree:Maybe<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.Batch> -> {0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.run_many_gpu_tree(tree) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.run_many_tree(tree) : Maybe<&2, 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.BatchResult>}