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

def L.gpu_single_matches_cpu(text):
    {==}


def L.http_utf8_octets():
    {==}



def L.http_binary_boundaries():
    {==}

def L.http_reject_non_octet():
    {==}

def L.http_https_target():
    {==}

def L.http_http_default_path():
    {==}

def L.http_query_without_path():
    {==}

def L.http_nondefault_port():
    {==}

def L.http_explicit_default_port():
    {==}

def L.http_signed_path_unchanged():
    {==}

def L.http_reject_unsupported_scheme():
    {==}

def L.http_reject_userinfo():
    {==}

def L.http_reject_empty_host():
    {==}

def L.http_reject_port_overflow():
    {==}

def L.http_reject_port_zero():
    {==}

def L.http_reject_relative_url():
    {==}

def L.http_reject_url_injection():
    {==}

def L.http_reject_url_space():
    {==}

def L.http_header_lookup_case_insensitive():
    {==}

def L.http_header_lookup_missing():
    {==}

def L.http_encode_get():
    {==}

def L.http_encode_head():
    {==}

def L.http_encode_post():
    {==}

def L.http_encode_put():
    {==}

def L.http_encode_patch():
    {==}

def L.http_encode_delete():
    {==}

def L.http_encode_options():
    {==}

def L.http_utf8_content_length():
    {==}

def L.http_reserved_host():
    {==}

def L.http_reserved_content_length():
    {==}

def L.http_reserved_transfer_encoding():
    {==}

def L.http_reserved_connection():
    {==}

def L.http_reserved_accept_encoding():
    {==}

def L.http_reserved_expect():
    {==}

def L.http_reserved_upgrade():
    {==}

def L.http_reserved_trailer():
    {==}

def L.http_bad_header_name():
    {==}

def L.http_header_name_injection():
    {==}

def L.http_header_value_injection():
    {==}

def L.http_header_nul():
    {==}

def L.http_unsupported_method():
    {==}

def L.http_body_non_octet():
    {==}

def http_encode_accepts_valid_body(+body: List<&2, U32>,
                                   valid: {HttpClient.valid_bytes(body) == True{} : Bool}) -> {HttpClient.encode_checked("POST", HttpClient.Target{True{}, "example.com", 443, "example.com", "/"}, Nil{}, body, True{}, HttpClient.valid_bytes(body), Done{Unit{}}) == HttpClient.encode_checked("POST", HttpClient.Target{True{}, "example.com", 443, "example.com", "/"}, Nil{}, body, True{}, True{}, Done{Unit{}}) : Result<&2, &2, HttpClient.Error, List<&2, U32>>}:
    Equal.cong(Bool, Result<&2, &2, HttpClient.Error, List<&2, U32>>,
        ok => HttpClient.encode_checked("POST", HttpClient.Target{True{}, "example.com", 443, "example.com", "/"}, Nil{}, body, True{}, ok, Done{Unit{}}),
        HttpClient.valid_bytes(body), True{}, valid)

def http_length_same(+body: List<&2, U32>) -> {List.length(&2, U32, body) == L.http_length(body) : Nat}:
    match body:
        case Nil{}: {==}
        case _ <> tail:
            Equal.cong(Nat, Nat, length => (1n + length : Nat),
                List.length(&2, U32, tail), L.http_length(tail), http_length_same(tail))

def append_bytes_assoc(+x: List<&2, U32>,
                       +y: List<&2, U32>,
                       +z: List<&2, U32>) -> {HttpClient.append_bytes(HttpClient.append_bytes(x, y), z) == HttpClient.append_bytes(x, HttpClient.append_bytes(y, z)) : List<&2, U32>}:
    match x:
        case Nil{}: {==}
        case h <> t:
            Equal.cong(List<&2, U32>, List<&2, U32>, rest => h <> rest,
                HttpClient.append_bytes(HttpClient.append_bytes(t, y), z), HttpClient.append_bytes(t, HttpClient.append_bytes(y, z)),
                append_bytes_assoc(t, y, z))

def utf8_append_same(+x: String,
                     +y: String) -> {HttpClient.utf8(x ++ y) == HttpClient.append_bytes(HttpClient.utf8(x), HttpClient.utf8(y)) : List<&2, U32>}:
    match x:
        case SNil{}: {==}
        case SCon{Chr{+c}, rest}:
            Equal.trans(List<&2, U32>, HttpClient.utf8(x ++ y),
                HttpClient.append_bytes(HttpClient.utf8_char(c), HttpClient.utf8(rest ++ y)),
                HttpClient.append_bytes(HttpClient.append_bytes(HttpClient.utf8_char(c), HttpClient.utf8(rest)), HttpClient.utf8(y)),
                {==},
                Equal.trans(List<&2, U32>,
                    HttpClient.append_bytes(HttpClient.utf8_char(c), HttpClient.utf8(rest ++ y)),
                    HttpClient.append_bytes(HttpClient.utf8_char(c), HttpClient.append_bytes(HttpClient.utf8(rest), HttpClient.utf8(y))),
                    HttpClient.append_bytes(HttpClient.append_bytes(HttpClient.utf8_char(c), HttpClient.utf8(rest)), HttpClient.utf8(y)),
                    Equal.cong(List<&2, U32>, List<&2, U32>, tail => HttpClient.append_bytes(HttpClient.utf8_char(c), tail),
                        HttpClient.utf8(rest ++ y), HttpClient.append_bytes(HttpClient.utf8(rest), HttpClient.utf8(y)), utf8_append_same(rest, y)),
                    Equal.sym(List<&2, U32>,
                        HttpClient.append_bytes(HttpClient.append_bytes(HttpClient.utf8_char(c), HttpClient.utf8(rest)), HttpClient.utf8(y)),
                        HttpClient.append_bytes(HttpClient.utf8_char(c), HttpClient.append_bytes(HttpClient.utf8(rest), HttpClient.utf8(y))),
                    append_bytes_assoc(HttpClient.utf8_char(c), HttpClient.utf8(rest), HttpClient.utf8(y)))))



def L.http_json_error_response():
    {==}

def L.http_json_empty():
    {==}

def L.http_json_trailing():
    {==}

def L.http_json_compressed():
    {==}

def L.http_json_invalid_utf8():
    {==}

def L.http_partial_write():
    {==}

def L.http_full_write():
    {==}

def L.http_empty_write():
    {==}

def L.http_zero_write_progress():
    {==}

def L.http_write_overreport():
    {==}

def L.http_empty_batch_builder():
    {==}

def L.http_empty_gpu_many():
    {==}

def L.http_singleton_batch_builder(work):
    +item = work
    {==}

def L.http_singleton_gpu_many(work):
    +item = work
    {==}

def L.http_gpu_decode_matches_cpu(method, limits, bytes, eof):
    {==}


def L.http_work_encode_uses_codec(request):
    +req = request
    {==}

def L.http_work_decode_uses_codec(method, limits, bytes, eof):
    {==}

def L.http_batch_leaf(work):
    +job = work
    {==}

def L.http_batch_fork(left, right):
    +l = left
    +r = right
    {==}

def L.http_flatten_leaf(outcome):
    +result = outcome
    {==}


def L.http_content_length():
    {==}

def L.http_preserve_remainder():
    {==}

def L.http_partial_body():
    {==}

def L.http_truncated_body():
    {==}

def L.http_incomplete_headers():
    {==}

def L.http_empty_eof():
    {==}

def L.http_close_delimited_waits():
    {==}

def L.http_close_delimited_eof():
    {==}

def L.http_head_ignores_length():
    {==}

def L.http_no_content():
    {==}

def L.http_not_modified():
    {==}

def L.http_reset_content_still_framed():
    {==}

def L.http_reject_duplicate_equal_length():
    {==}

def L.http_reject_conflicting_length():
    {==}

def L.http_reject_length_list():
    {==}

def L.http_reject_te_and_cl():
    {==}

def L.http_reject_negative_length():
    {==}

def L.http_reject_huge_length():
    {==}

def L.http_reject_bad_transfer_coding():
    {==}


def L.http_reject_bare_lf():
    {==}

def L.http_reject_obsolete_fold():
    {==}

def L.http_reject_space_before_colon():
    {==}

def L.http_reject_invalid_status():
    {==}

def L.http_reject_invalid_version():
    {==}

def L.http_accept_http_10_response():
    {==}

def L.http_reject_upgrade():
    {==}

def L.http_body_limit_exact():
    {==}

def L.http_body_limit_over():
    {==}

def L.http_header_bytes_exact():
    {==}

def L.http_header_bytes_over():
    {==}

def L.http_wire_bytes_exact():
    {==}

def L.http_wire_bytes_over():
    {==}

def L.http_wire_bytes_excludes_remainder():
    {==}

def L.http_header_count_over():
    {==}

def L.http_reject_empty_port():
    {==}

def L.http_reject_invalid_escape():
    {==}

def L.http_reject_unsupported_ipv6():
    {==}

def L.http_header_value_trimming():
    {==}

def L.http_close_body_limit_over():
    {==}

def L.http_status_301_is_response():
    {==}

def L.http_status_400_is_response():
    {==}

def L.http_status_401_is_response():
    {==}

def L.http_status_403_is_response():
    {==}

def L.http_status_404_is_response():
    {==}

def L.http_status_429_is_response():
    {==}

def L.http_status_500_is_response():
    {==}

def L.http_status_503_is_response():
    {==}

def L.http_skip_interim():
    {==}

def L.http_interim_without_final():
    {==}

def L.http_interim_count_over():
    {==}

def L.http_chunked():
    {==}

def L.http_chunk_extensions_trailers():
    {==}

def L.http_uppercase_hex_chunk():
    {==}

def L.http_chunk_truncation():
    {==}

def L.http_chunk_incomplete():
    {==}

def L.http_missing_final_chunk():
    {==}

def L.http_unfinished_trailers():
    {==}

def L.http_reject_huge_chunk():
    {==}

def L.http_reject_repeated_chunked():
    {==}

def L.http_reject_bad_chunk_size():
    {==}

def L.http_reject_bad_chunk_terminator():
    {==}

def L.http_reject_forbidden_trailer():
    {==}

def L.http_chunk_body_limit_over():
    {==}

def L.http_trailer_count_over():
    {==}

def L.http_trailer_bytes_over():
    {==}

def L.http_chunk_line_bytes_over():
    {==}

def L.http_gpu_encode_matches_cpu(request):
    {==}

def http_append_outcomes_same(+xs: List<&2, HttpClient.Outcome>,
                              +ys: List<&2, HttpClient.Outcome>) -> {HttpClient.append_outcomes(xs, ys) == L.http_append_outcomes(xs, ys) : List<&2, HttpClient.Outcome>}:
    match xs:
        case Nil{}: {==}
        case Con{outcome, rest}:
            Equal.cong(List<&2, HttpClient.Outcome>, List<&2, HttpClient.Outcome>, tail => outcome <> tail,
                HttpClient.append_outcomes(rest, ys), L.http_append_outcomes(rest, ys), http_append_outcomes_same(rest, ys))

def L.http_flatten_fork(left, right):
    match left:
        case HttpClient.LeafResult{outcome}: {==}
        case HttpClient.ForkResult{inner_left, inner_right}:
            http_append_outcomes_same(HttpClient.append_outcomes(HttpClient.flatten_results(inner_left), HttpClient.flatten_results(inner_right)),
                HttpClient.flatten_results(right))

def flatten_empty_edges(+bytes: List<&2, U32>) -> {HttpClient.flatten_bytes([Nil{}, bytes, Nil{}]) == bytes : List<&2, U32>}:
    match bytes:
        case Nil{}: {==}
        case _ <> _: {==}

def append_bytes_nil(+bytes: List<&2, U32>) -> {HttpClient.append_bytes(bytes, Nil{}) == bytes : List<&2, U32>}:
    match bytes:
        case Nil{}: {==}
        case head <> tail:
            Equal.cong(List<&2, U32>, List<&2, U32>, rest => head <> rest,
                HttpClient.append_bytes(tail, Nil{}), tail, append_bytes_nil(tail))

def flatten_bytes_pair(+left: List<&2, U32>,
                       +right: List<&2, U32>) -> {HttpClient.flatten_bytes([left, right]) == HttpClient.append_bytes(left, right) : List<&2, U32>}:
    match left right:
        case Nil{} Nil{}: {==}
        case Nil{} head <> tail: {==}
        case head <> tail Nil{}:
            Equal.sym(List<&2, U32>, HttpClient.append_bytes(left, Nil{}), left, append_bytes_nil(left))
        case _ <> _ _ <> _: {==}

def append_bytes_same(+left: List<&2, U32>,
                      +right: List<&2, U32>) -> {HttpClient.append_bytes(left, right) == L.http_append(left, right) : List<&2, U32>}:
    match left:
        case Nil{}: {==}
        case head <> tail:
            Equal.cong(List<&2, U32>, List<&2, U32>, rest => head <> rest,
                HttpClient.append_bytes(tail, right), L.http_append(tail, right), append_bytes_same(tail, right))

def string_append_assoc(+x: String,
                        +y: String,
                        +z: String) -> {(x ++ y) ++ z == x ++ (y ++ z) : String}:
    match x:
        case SNil{}: {==}
        case SCon{head, tail}:
            Equal.cong(String, String, rest => SCon{head, rest},
                (tail ++ y) ++ z, tail ++ (y ++ z), string_append_assoc(tail, y, z))

def http_concat_tail(+x: String,
                     +y: String,
                     +body: List<&2, U32>) -> {HttpClient.append_bytes(HttpClient.utf8(x), HttpClient.append_bytes(HttpClient.utf8(y), body)) == L.http_append(HttpClient.utf8(x ++ y), body) : List<&2, U32>}:
    Equal.trans(List<&2, U32>,
        HttpClient.append_bytes(HttpClient.utf8(x), HttpClient.append_bytes(HttpClient.utf8(y), body)),
        HttpClient.append_bytes(HttpClient.append_bytes(HttpClient.utf8(x), HttpClient.utf8(y)), body),
        L.http_append(HttpClient.utf8(x ++ y), body),
        Equal.sym(List<&2, U32>,
            HttpClient.append_bytes(HttpClient.append_bytes(HttpClient.utf8(x), HttpClient.utf8(y)), body),
            HttpClient.append_bytes(HttpClient.utf8(x), HttpClient.append_bytes(HttpClient.utf8(y), body)),
            append_bytes_assoc(HttpClient.utf8(x), HttpClient.utf8(y), body)),
        Equal.trans(List<&2, U32>,
            HttpClient.append_bytes(HttpClient.append_bytes(HttpClient.utf8(x), HttpClient.utf8(y)), body),
            HttpClient.append_bytes(HttpClient.utf8(x ++ y), body),
            L.http_append(HttpClient.utf8(x ++ y), body),
            Equal.cong(List<&2, U32>, List<&2, U32>, head => HttpClient.append_bytes(head, body),
                HttpClient.append_bytes(HttpClient.utf8(x), HttpClient.utf8(y)), HttpClient.utf8(x ++ y),
                Equal.sym(List<&2, U32>, HttpClient.utf8(x ++ y),
                    HttpClient.append_bytes(HttpClient.utf8(x), HttpClient.utf8(y)), utf8_append_same(x, y))),
            append_bytes_same(HttpClient.utf8(x ++ y), body)))

def http_encode_body_core(+body: List<&2, U32>) -> {HttpClient.encode_checked("POST", HttpClient.Target{True{}, "example.com", 443, "example.com", "/"}, Nil{}, body, True{}, True{}, Done{Unit{}}) == Done{L.http_append(HttpClient.utf8("POST / HTTP/1.1\r\nHost: example.com\r\nContent-Length: " ++ Nat.show(List.length(&2, U32, body)) ++ "\r\nAccept-Encoding: identity\r\nConnection: close\r\n\r\n"), body)} : Result<&2, &2, HttpClient.Error, List<&2, U32>>}:
    Equal.trans(Result<&2, &2, HttpClient.Error, List<&2, U32>>,
        HttpClient.encode_checked("POST", HttpClient.Target{True{}, "example.com", 443, "example.com", "/"}, Nil{}, body, True{}, True{}, Done{Unit{}}),
        Done{HttpClient.append_bytes(HttpClient.utf8("POST / HTTP/1.1\r\nHost: example.com\r\nContent-Length: "),
            L.http_append(HttpClient.utf8((Nat.show(List.length(&2, U32, body)) ++ "\r\n") ++
                "Accept-Encoding: identity\r\nConnection: close\r\n\r\n"), body))},
        Done{L.http_append(HttpClient.utf8("POST / HTTP/1.1\r\nHost: example.com\r\nContent-Length: " ++ Nat.show(List.length(&2, U32, body)) ++ "\r\nAccept-Encoding: identity\r\nConnection: close\r\n\r\n"), body)},
    Equal.cong(List<&2, U32>, Result<&2, &2, HttpClient.Error, List<&2, U32>>,
        tail => Done{HttpClient.append_bytes(HttpClient.utf8("POST / HTTP/1.1\r\nHost: example.com\r\nContent-Length: "), tail)},
        HttpClient.append_bytes(HttpClient.utf8(Nat.show(List.length(&2, U32, body)) ++ "\r\n"),
            HttpClient.append_bytes(HttpClient.utf8("Accept-Encoding: identity\r\nConnection: close\r\n\r\n"), body)),
        L.http_append(HttpClient.utf8((Nat.show(List.length(&2, U32, body)) ++ "\r\n") ++ "Accept-Encoding: identity\r\nConnection: close\r\n\r\n"), body),
        http_concat_tail(Nat.show(List.length(&2, U32, body)) ++ "\r\n",
            "Accept-Encoding: identity\r\nConnection: close\r\n\r\n", body)),
    Equal.cong(String, Result<&2, &2, HttpClient.Error, List<&2, U32>>,
        text => Done{L.http_append(HttpClient.utf8("POST / HTTP/1.1\r\nHost: example.com\r\nContent-Length: " ++ text), body)},
        (Nat.show(List.length(&2, U32, body)) ++ "\r\n") ++ "Accept-Encoding: identity\r\nConnection: close\r\n\r\n",
        Nat.show(List.length(&2, U32, body)) ++ "\r\nAccept-Encoding: identity\r\nConnection: close\r\n\r\n",
        string_append_assoc(Nat.show(List.length(&2, U32, body)), "\r\n",
            "Accept-Encoding: identity\r\nConnection: close\r\n\r\n")))

def L.http_encode_arbitrary_body(body, valid):
    Equal.trans(Result<&2, &2, HttpClient.Error, List<&2, U32>>,
        HttpClient.encode(HttpClient.Request{"POST", "https://example.com/", Nil{}, body}),
        HttpClient.encode_checked("POST", HttpClient.Target{True{}, "example.com", 443, "example.com", "/"}, Nil{}, body, True{}, True{}, Done{Unit{}}),
        Done{L.http_append(HttpClient.utf8("POST / HTTP/1.1\r\nHost: example.com\r\nContent-Length: " ++ Nat.show(L.http_length(body)) ++ "\r\nAccept-Encoding: identity\r\nConnection: close\r\n\r\n"), body)},
        http_encode_accepts_valid_body(body, valid),
        Equal.trans(Result<&2, &2, HttpClient.Error, List<&2, U32>>,
            HttpClient.encode_checked("POST", HttpClient.Target{True{}, "example.com", 443, "example.com", "/"}, Nil{}, body, True{}, True{}, Done{Unit{}}),
            Done{L.http_append(HttpClient.utf8("POST / HTTP/1.1\r\nHost: example.com\r\nContent-Length: " ++ Nat.show(List.length(&2, U32, body)) ++ "\r\nAccept-Encoding: identity\r\nConnection: close\r\n\r\n"), body)},
            Done{L.http_append(HttpClient.utf8("POST / HTTP/1.1\r\nHost: example.com\r\nContent-Length: " ++ Nat.show(L.http_length(body)) ++ "\r\nAccept-Encoding: identity\r\nConnection: close\r\n\r\n"), body)},
            http_encode_body_core(body),
            Equal.cong(Nat, Result<&2, &2, HttpClient.Error, List<&2, U32>>,
                length => Done{L.http_append(HttpClient.utf8("POST / HTTP/1.1\r\nHost: example.com\r\nContent-Length: " ++ Nat.show(length) ++ "\r\nAccept-Encoding: identity\r\nConnection: close\r\n\r\n"), body)},
                List.length(&2, U32, body), L.http_length(body), http_length_same(body))))

def L.http_decode_partition_invariant(method, limits, left, right, eof):
    +m = method
    +l = limits
    +e = eof
    Equal.trans(HttpClient.Decode, HttpClient.decode_parts(m, l, [left, right], e),
        HttpClient.decode(m, l, HttpClient.append_bytes(left, right), e),
        HttpClient.decode(m, l, L.http_append(left, right), e),
        Equal.cong(List<&2, U32>, HttpClient.Decode, raw => HttpClient.decode(m, l, raw, e),
            HttpClient.flatten_bytes([left, right]), HttpClient.append_bytes(left, right), flatten_bytes_pair(left, right)),
        Equal.cong(List<&2, U32>, HttpClient.Decode, raw => HttpClient.decode(m, l, raw, e),
            HttpClient.append_bytes(left, right), L.http_append(left, right), append_bytes_same(left, right)))

def L.http_decode_empty_fragments(method, limits, bytes, eof):
    +m = method
    +l = limits
    +e = eof
    Equal.cong(List<&2, U32>, HttpClient.Decode, raw => HttpClient.decode(m, l, raw, e),
        HttpClient.flatten_bytes([Nil{}, bytes, Nil{}]), bytes, flatten_empty_edges(bytes))

def http_read_json_select_parity(+text: String,
                                 encoding_ok: Bool,
                                 is_utf8: Bool) -> {HttpClient.read_json_select(text, encoding_ok, is_utf8, True{}) == HttpClient.read_json_select(text, encoding_ok, is_utf8, False{}) : Result<&1, &1, HttpClient.Error, Json.Value>}:
    match encoding_ok is_utf8:
        case False{} _: {==}
        case True{} False{}: {==}
        case True{} True{}:
            Equal.cong(Result<&1, &1, Json.Error, Json.Value>, Result<&1, &1, HttpClient.Error, Json.Value>, parsed => HttpClient.read_json_parsed(parsed),
                Json.parse_gpu(text), Json.parse(text), L.gpu_single_matches_cpu(text))

def L.http_gpu_json_matches_cpu(response):
    match response:
        case HttpClient.Response{status, headers, +body, trailers}:
            +values = HttpClient.field_values("content-encoding", headers)
            +text = Encoding.utf8.decode(Bytes.from_string(HttpClient.octets_string(body)))
            http_read_json_select_parity(text, HttpClient.identity_encoding(values),
                Bool.and(HttpClient.valid_bytes(body), HttpClient.byte_lists_equal(HttpClient.utf8(text), body)))

def L.http_gpu_batch_matches_cpu(batch):
    {==}

def http_expected_batch(batch: HttpClient.Batch) -> List<&2, HttpClient.Outcome>:
    match batch:
        case HttpClient.Leaf{work}: [L.http_expected_outcome(work)]
        case HttpClient.Fork{+left, +right}:
            L.http_append_outcomes(http_expected_batch(left), http_expected_batch(right))

def http_run_work_expected(work: HttpClient.Work) -> {HttpClient.run_work(work) == L.http_expected_outcome(work) : HttpClient.Outcome}:
    match work:
        case HttpClient.EncodeWork{request}: {==}
        case HttpClient.DecodeWork{method, limits, bytes, eof}: {==}

def http_batch_cpu_expected(+batch: HttpClient.Batch) -> {HttpClient.flatten_results(HttpClient.run_batch(batch)) == http_expected_batch(batch) : List<&2, HttpClient.Outcome>}:
    match batch:
        case HttpClient.Leaf{work}:
            Equal.cong(HttpClient.Outcome, List<&2, HttpClient.Outcome>, outcome => [outcome],
                HttpClient.run_work(work), L.http_expected_outcome(work), http_run_work_expected(work))
        case HttpClient.Fork{+left, +right}:
            Equal.trans(List<&2, HttpClient.Outcome>,
                HttpClient.flatten_results(HttpClient.run_batch(batch)),
                L.http_append_outcomes(HttpClient.flatten_results(HttpClient.run_batch(left)), HttpClient.flatten_results(HttpClient.run_batch(right))),
                http_expected_batch(batch),
                L.http_flatten_fork(HttpClient.run_batch(left), HttpClient.run_batch(right)),
                Equal.trans(List<&2, HttpClient.Outcome>,
                    L.http_append_outcomes(HttpClient.flatten_results(HttpClient.run_batch(left)), HttpClient.flatten_results(HttpClient.run_batch(right))),
                    L.http_append_outcomes(http_expected_batch(left), HttpClient.flatten_results(HttpClient.run_batch(right))),
                    http_expected_batch(batch),
                    Equal.cong(List<&2, HttpClient.Outcome>, List<&2, HttpClient.Outcome>, xs => L.http_append_outcomes(xs, HttpClient.flatten_results(HttpClient.run_batch(right))),
                        HttpClient.flatten_results(HttpClient.run_batch(left)), http_expected_batch(left), http_batch_cpu_expected(left)),
                    Equal.cong(List<&2, HttpClient.Outcome>, List<&2, HttpClient.Outcome>, ys => L.http_append_outcomes(http_expected_batch(left), ys),
                        HttpClient.flatten_results(HttpClient.run_batch(right)), http_expected_batch(right), http_batch_cpu_expected(right))))

def http_batch_gpu_expected(+batch: HttpClient.Batch) -> {HttpClient.flatten_results(HttpClient.run_batch_gpu(batch)) == http_expected_batch(batch) : List<&2, HttpClient.Outcome>}:
    Equal.trans(List<&2, HttpClient.Outcome>, HttpClient.flatten_results(HttpClient.run_batch_gpu(batch)),
        HttpClient.flatten_results(HttpClient.run_batch(batch)), http_expected_batch(batch),
        Equal.cong(HttpClient.BatchResult, List<&2, HttpClient.Outcome>, HttpClient.flatten_results,
            HttpClient.run_batch_gpu(batch), HttpClient.run_batch(batch), L.http_gpu_batch_matches_cpu(batch)),
        http_batch_cpu_expected(batch))

def http_append_work(+xs: List<&2, HttpClient.Work>,
                     +ys: List<&2, HttpClient.Work>) -> List<&2, HttpClient.Work>:
    match xs:
        case Nil{}: ys
        case work <> tail: work <> http_append_work(tail, ys)

def http_append_work_assoc(+xs: List<&2, HttpClient.Work>,
                           +ys: List<&2, HttpClient.Work>,
                           +zs: List<&2, HttpClient.Work>) -> {http_append_work(xs, http_append_work(ys, zs)) == http_append_work(http_append_work(xs, ys), zs) : List<&2, HttpClient.Work>}:
    match xs:
        case Nil{}: {==}
        case work <> tail:
            Equal.cong(List<&2, HttpClient.Work>, List<&2, HttpClient.Work>, rest => work <> rest,
                http_append_work(tail, http_append_work(ys, zs)), http_append_work(http_append_work(tail, ys), zs),
                http_append_work_assoc(tail, ys, zs))

def http_append_work_nil(+xs: List<&2, HttpClient.Work>) -> {http_append_work(xs, Nil{}) == xs : List<&2, HttpClient.Work>}:
    match xs:
        case Nil{}: {==}
        case work <> tail:
            Equal.cong(List<&2, HttpClient.Work>, List<&2, HttpClient.Work>, rest => work <> rest,
                http_append_work(tail, Nil{}), tail, http_append_work_nil(tail))

def http_batch_work_order(+batch: HttpClient.Batch) -> List<&2, HttpClient.Work>:
    match batch:
        case HttpClient.Leaf{work}: [work]
        case HttpClient.Fork{+left, +right}:
            http_append_work(http_batch_work_order(left), http_batch_work_order(right))

def http_batches_work_order(+batches: List<&2, HttpClient.Batch>) -> List<&2, HttpClient.Work>:
    match batches:
        case Nil{}: Nil{}
        case batch <> tail:
            http_append_work(http_batch_work_order(batch), http_batches_work_order(tail))

def http_batch_pairs_work_order(+batches: List<&2, HttpClient.Batch>) -> {http_batches_work_order(HttpClient.batch_pairs(batches)) == http_batches_work_order(batches) : List<&2, HttpClient.Work>}:
    match batches:
        case Nil{}: {==}
        case batch <> Nil{}: {==}
        case +left <> +right <> +tail:
            Equal.trans(List<&2, HttpClient.Work>,
                http_batches_work_order(HttpClient.batch_pairs(batches)),
                http_append_work(http_batch_work_order(left),
                    http_append_work(http_batch_work_order(right), http_batches_work_order(HttpClient.batch_pairs(tail)))),
                http_batches_work_order(batches),
                Equal.sym(List<&2, HttpClient.Work>,
                    http_append_work(http_batch_work_order(left),
                        http_append_work(http_batch_work_order(right), http_batches_work_order(HttpClient.batch_pairs(tail)))),
                    http_append_work(http_append_work(http_batch_work_order(left), http_batch_work_order(right)),
                        http_batches_work_order(HttpClient.batch_pairs(tail))),
                    http_append_work_assoc(http_batch_work_order(left), http_batch_work_order(right), http_batches_work_order(HttpClient.batch_pairs(tail)))),
                Equal.cong(List<&2, HttpClient.Work>, List<&2, HttpClient.Work>, rest =>
                        http_append_work(http_batch_work_order(left), http_append_work(http_batch_work_order(right), rest)),
                    http_batches_work_order(HttpClient.batch_pairs(tail)), http_batches_work_order(tail),
                    http_batch_pairs_work_order(tail)))

def http_optional_batch_work_order(batch: Maybe<&2, HttpClient.Batch>) -> List<&2, HttpClient.Work>:
    match batch:
        case None{}: Nil{}
        case Some{tree}: http_batch_work_order(tree)

def http_batch_fold_result_order(head: HttpClient.Batch,
                                 rest: Maybe<&2, HttpClient.Batch>,
                                 +tail: List<&2, HttpClient.Batch>,
                                 rest_order: {http_optional_batch_work_order(rest) == http_batches_work_order(tail) : List<&2, HttpClient.Work>}) -> {http_optional_batch_work_order(HttpClient.batch_fold_result(head, rest)) == http_append_work(http_batch_work_order(head), http_batches_work_order(tail)) : List<&2, HttpClient.Work>}:
    match rest:
        case None{}:
            Equal.trans(List<&2, HttpClient.Work>, http_batch_work_order(head),
                http_append_work(http_batch_work_order(head), Nil{}),
                http_append_work(http_batch_work_order(head), http_batches_work_order(tail)),
                Equal.sym(List<&2, HttpClient.Work>, http_append_work(http_batch_work_order(head), Nil{}), http_batch_work_order(head),
                    http_append_work_nil(http_batch_work_order(head))),
                Equal.cong(List<&2, HttpClient.Work>, List<&2, HttpClient.Work>, jobs => http_append_work(http_batch_work_order(head), jobs),
                    Nil{}, http_batches_work_order(tail), rest_order))
        case Some{+tree}:
            Equal.cong(List<&2, HttpClient.Work>, List<&2, HttpClient.Work>, jobs => http_append_work(http_batch_work_order(head), jobs),
                http_batch_work_order(tree), http_batches_work_order(tail), rest_order)

def http_batch_fold_work_order(+batches: List<&2, HttpClient.Batch>) -> {http_optional_batch_work_order(HttpClient.batch_fold(batches)) == http_batches_work_order(batches) : List<&2, HttpClient.Work>}:
    match batches:
        case Nil{}: {==}
        case head <> tail:
            http_batch_fold_result_order(head, HttpClient.batch_fold(tail), tail, http_batch_fold_work_order(tail))

def http_batch_build_work_order(fuel: Nat,
                                +batches: List<&2, HttpClient.Batch>) -> {http_optional_batch_work_order(HttpClient.batch_build(fuel, batches)) == http_batches_work_order(batches) : List<&2, HttpClient.Work>}:
    match fuel:
        case 0n: http_batch_fold_work_order(batches)
        case 1n+p:
            match batches:
                case Nil{}: {==}
                case head <> Nil{}:
                    Equal.sym(List<&2, HttpClient.Work>, http_append_work(http_batch_work_order(head), Nil{}),
                        http_batch_work_order(head), http_append_work_nil(http_batch_work_order(head)))
                case +left <> +right <> +tail:
                    Equal.trans(List<&2, HttpClient.Work>,
                        http_optional_batch_work_order(HttpClient.batch_build(p, HttpClient.batch_pairs(batches))),
                        http_batches_work_order(HttpClient.batch_pairs(batches)),
                        http_batches_work_order(batches),
                        http_batch_build_work_order(p, HttpClient.batch_pairs(batches)),
                        http_batch_pairs_work_order(batches))

def http_batch_leaves_work_order(+jobs: List<&2, HttpClient.Work>) -> {http_batches_work_order(HttpClient.batch_leaves(jobs)) == jobs : List<&2, HttpClient.Work>}:
    match jobs:
        case Nil{}: {==}
        case work <> tail:
            Equal.cong(List<&2, HttpClient.Work>, List<&2, HttpClient.Work>, rest => work <> rest,
                http_batches_work_order(HttpClient.batch_leaves(tail)), tail, http_batch_leaves_work_order(tail))

def http_batch_from_list_work_order(+jobs: List<&2, HttpClient.Work>) -> {http_optional_batch_work_order(HttpClient.batch_from_list(jobs)) == jobs : List<&2, HttpClient.Work>}:
    Equal.trans(List<&2, HttpClient.Work>,
        http_optional_batch_work_order(HttpClient.batch_from_list(jobs)),
        http_batches_work_order(HttpClient.batch_leaves(jobs)), jobs,
        http_batch_build_work_order(List.length(&2, HttpClient.Work, jobs), HttpClient.batch_leaves(jobs)),
        http_batch_leaves_work_order(jobs))

def http_expected_outcomes_append(+xs: List<&2, HttpClient.Work>,
                                  +ys: List<&2, HttpClient.Work>) -> {L.http_expected_outcomes(http_append_work(xs, ys)) == L.http_append_outcomes(L.http_expected_outcomes(xs), L.http_expected_outcomes(ys)) : List<&2, HttpClient.Outcome>}:
    match xs:
        case Nil{}: {==}
        case work <> tail:
            Equal.cong(List<&2, HttpClient.Outcome>, List<&2, HttpClient.Outcome>, results => L.http_expected_outcome(work) <> results,
                L.http_expected_outcomes(http_append_work(tail, ys)),
                L.http_append_outcomes(L.http_expected_outcomes(tail), L.http_expected_outcomes(ys)),
                http_expected_outcomes_append(tail, ys))

def http_expected_batch_work_order(+batch: HttpClient.Batch) -> {http_expected_batch(batch) == L.http_expected_outcomes(http_batch_work_order(batch)) : List<&2, HttpClient.Outcome>}:
    match batch:
        case HttpClient.Leaf{work}: {==}
        case HttpClient.Fork{+left, +right}:
            Equal.trans(List<&2, HttpClient.Outcome>,
                http_expected_batch(batch),
                L.http_append_outcomes(http_expected_batch(left), http_expected_batch(right)),
                L.http_expected_outcomes(http_batch_work_order(batch)),
                {==},
                Equal.trans(List<&2, HttpClient.Outcome>,
                    L.http_append_outcomes(http_expected_batch(left), http_expected_batch(right)),
                    L.http_append_outcomes(L.http_expected_outcomes(http_batch_work_order(left)), L.http_expected_outcomes(http_batch_work_order(right))),
                    L.http_expected_outcomes(http_batch_work_order(batch)),
                    Equal.trans(List<&2, HttpClient.Outcome>,
                        L.http_append_outcomes(http_expected_batch(left), http_expected_batch(right)),
                        L.http_append_outcomes(L.http_expected_outcomes(http_batch_work_order(left)), http_expected_batch(right)),
                        L.http_append_outcomes(L.http_expected_outcomes(http_batch_work_order(left)), L.http_expected_outcomes(http_batch_work_order(right))),
                        Equal.cong(List<&2, HttpClient.Outcome>, List<&2, HttpClient.Outcome>, xs => L.http_append_outcomes(xs, http_expected_batch(right)),
                            http_expected_batch(left), L.http_expected_outcomes(http_batch_work_order(left)), http_expected_batch_work_order(left)),
                        Equal.cong(List<&2, HttpClient.Outcome>, List<&2, HttpClient.Outcome>, ys => L.http_append_outcomes(L.http_expected_outcomes(http_batch_work_order(left)), ys),
                            http_expected_batch(right), L.http_expected_outcomes(http_batch_work_order(right)), http_expected_batch_work_order(right))),
                    Equal.sym(List<&2, HttpClient.Outcome>,
                        L.http_expected_outcomes(http_batch_work_order(batch)),
                        L.http_append_outcomes(L.http_expected_outcomes(http_batch_work_order(left)), L.http_expected_outcomes(http_batch_work_order(right))),
                        http_expected_outcomes_append(http_batch_work_order(left), http_batch_work_order(right)))))

def http_optional_gpu_expected(batch: Maybe<&2, HttpClient.Batch>,
                               +jobs: List<&2, HttpClient.Work>,
                               batch_order: {http_optional_batch_work_order(batch) == jobs : List<&2, HttpClient.Work>}) -> {L.http_optional_outcomes(HttpClient.run_many_gpu_tree(batch)) == L.http_expected_outcomes(jobs) : List<&2, HttpClient.Outcome>}:
    match batch:
        case None{}:
            Equal.cong(List<&2, HttpClient.Work>, List<&2, HttpClient.Outcome>, L.http_expected_outcomes,
                Nil{}, jobs, batch_order)
        case Some{+tree}:
            Equal.trans(List<&2, HttpClient.Outcome>,
                L.http_optional_outcomes(HttpClient.run_many_gpu_tree(batch)),
                http_expected_batch(tree), L.http_expected_outcomes(jobs),
                http_batch_gpu_expected(tree),
                Equal.trans(List<&2, HttpClient.Outcome>,
                    http_expected_batch(tree),
                    L.http_expected_outcomes(http_batch_work_order(tree)),
                    L.http_expected_outcomes(jobs),
                    http_expected_batch_work_order(tree),
                    Equal.cong(List<&2, HttpClient.Work>, List<&2, HttpClient.Outcome>, L.http_expected_outcomes,
                        http_batch_work_order(tree), jobs, batch_order)))

def http_run_many_gpu_expected(+jobs: List<&2, HttpClient.Work>) -> {L.http_optional_outcomes(HttpClient.run_many_gpu(jobs)) == L.http_expected_outcomes(jobs) : List<&2, HttpClient.Outcome>}:
    http_optional_gpu_expected(HttpClient.batch_from_list(jobs), jobs, http_batch_from_list_work_order(jobs))

def http_run_many_tree_parity(tree: Maybe<&2, HttpClient.Batch>) -> {HttpClient.run_many_gpu_tree(tree) == HttpClient.run_many_tree(tree) : Maybe<&2, HttpClient.BatchResult>}:
    match tree:
        case None{}: {==}
        case Some{batch}:
            Equal.cong(HttpClient.BatchResult, Maybe<&2, HttpClient.BatchResult>, result => Some{result},
                HttpClient.run_batch_gpu(batch), HttpClient.run_batch(batch), L.http_gpu_batch_matches_cpu(batch))

def L.http_gpu_many_matches_cpu(jobs):
    http_run_many_tree_parity(HttpClient.batch_from_list(jobs))

def L.http_gpu_batch_preserves_order_and_errors(jobs):
    http_run_many_gpu_expected(jobs)