0x3d214765 fails

0x3d2147650fe101ae3c3e4a95333b4238

Library correctness laws and integration obligations.

Anonymous package: import it by hash.

Published: 2026-10-01
Size: 1,139,762 bytes, 33 files
License: MIT-0 (no LICENSE file; the hub's default)
Declarations: 174 laws (0 proved), 1263 defs, 64 types

Import

import 0x3d2147650fe101ae3c3e4a95333b4238/LAWS.bend as LAWS
import 0x3d2147650fe101ae3c3e4a95333b4238/PROOF.bend as PROOF
import 0x3d2147650fe101ae3c3e4a95333b4238/bend_libs.bend as Bend_libs
import 0x3d2147650fe101ae3c3e4a95333b4238/libs/HTTPClient.bend as HTTPClient
import 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.bend as JSON
import 0x3d2147650fe101ae3c3e4a95333b4238/libs/SQL.bend as SQL
import 0x3d2147650fe101ae3c3e4a95333b4238/libs/wire/deps/bytes.bend as Bytes
import 0x3d2147650fe101ae3c3e4a95333b4238/libs/wire/deps/int.bend as Int
import 0x3d2147650fe101ae3c3e4a95333b4238/libs/wire/dns.bend as Dns
import 0x3d2147650fe101ae3c3e4a95333b4238/libs/wire/wire.bend as Wire
import 0x3d2147650fe101ae3c3e4a95333b4238/proof/HTTPClientProof.bend as HTTPClientProof
import 0x3d2147650fe101ae3c3e4a95333b4238/proof/JSON_AssemblyProof.bend as JSON_AssemblyProof
import 0x3d2147650fe101ae3c3e4a95333b4238/proof/JSON_LexWhitespaceProof.bend as JSON_LexWhitespaceProof
import 0x3d2147650fe101ae3c3e4a95333b4238/proof/JSON_ListProof.bend as JSON_ListProof
import 0x3d2147650fe101ae3c3e4a95333b4238/proof/JSON_NumberLexProof.bend as JSON_NumberLexProof
import 0x3d2147650fe101ae3c3e4a95333b4238/proof/JSON_ParallelProof.bend as JSON_ParallelProof
import 0x3d2147650fe101ae3c3e4a95333b4238/proof/JSON_PrimitiveProof.bend as JSON_PrimitiveProof
import 0x3d2147650fe101ae3c3e4a95333b4238/proof/JSON_RenderLexProof.bend as JSON_RenderLexProof
import 0x3d2147650fe101ae3c3e4a95333b4238/proof/JSON_SourceProof.bend as JSON_SourceProof
import 0x3d2147650fe101ae3c3e4a95333b4238/proof/JSON_StringProof.bend as JSON_StringProof
import 0x3d2147650fe101ae3c3e4a95333b4238/usage/HTTP.bend as HTTP
import 0x3d2147650fe101ae3c3e4a95333b4238/usage/HTTP_Decode.bend as HTTP_Decode
import 0x3d2147650fe101ae3c3e4a95333b4238/usage/HTTP_Encode.bend as HTTP_Encode
import 0x3d2147650fe101ae3c3e4a95333b4238/usage/HTTP_GPU.bend as HTTP_GPU
import 0x3d2147650fe101ae3c3e4a95333b4238/usage/HTTP_JSON.bend as HTTP_JSON
import 0x3d2147650fe101ae3c3e4a95333b4238/usage/HTTP_Send.bend as HTTP_Send
import 0x3d2147650fe101ae3c3e4a95333b4238/usage/HTTP_URL.bend as HTTP_URL
import 0x3d2147650fe101ae3c3e4a95333b4238/usage/JSON_GPU.bend as JSON_GPU
import 0x3d2147650fe101ae3c3e4a95333b4238/usage/JSON_SafeTest.bend as JSON_SafeTest

Modules

LAWS.bend 185 declarations, 174 laws — Library correctness laws and integration obligations.
PROOF.bend 19 declarations
bend_libs.bend 0 declarations
libs/HTTPClient.bend 360 declarations
libs/JSON.bend 235 declarations
libs/SQL.bend 36 declarations
libs/wire/deps/bytes.bend 123 declarations — Byte buffers packed four bytes to a U32, with bounds-checked access. Source: https://github.com/paymog/bend-kit/tree/main/bytes
libs/wire/deps/int.bend 331 declarations — Fixed-width integers U8, U16, U64, I32 and I64: wrapping, checked and saturating arithmetic, and text in radix 2 to 36.
libs/wire/dns.bend 123 declarations — DNS codec and host lookup. Source: https://github.com/paymog/bend-kit/tree/main/dns
libs/wire/wire.bend 19 declarations — Byte-exact TCP, UDP, and TLS sockets. Source: https://github.com/paymog/bend-kit/tree/main/wire
proof/HTTPClientProof.bend 34 declarations
proof/JSON_AssemblyProof.bend 15 declarations
proof/JSON_LexWhitespaceProof.bend 33 declarations
proof/JSON_ListProof.bend 7 declarations
proof/JSON_NumberLexProof.bend 16 declarations
proof/JSON_ParallelProof.bend 7 declarations
proof/JSON_PrimitiveProof.bend 14 declarations
proof/JSON_RenderLexProof.bend 42 declarations — Lexer/renderer bridge. All recursion follows the JSON value structure.
proof/JSON_SourceProof.bend 97 declarations
proof/JSON_StringProof.bend 10 declarations
usage/HTTP.bend 2 declarations
usage/HTTP_Decode.bend 1 declarations
usage/HTTP_Encode.bend 1 declarations
usage/HTTP_GPU.bend 9 declarations
usage/HTTP_JSON.bend 1 declarations
usage/HTTP_Send.bend 5 declarations
usage/HTTP_URL.bend 1 declarations
usage/JSON_GPU.bend 5 declarations
usage/JSON_SafeTest.bend 7 declarations

Other files

Dependencies

bend-kit-encoding@0.3.0.0 via libs/HTTPClient.bend: import 0xcfc8be7b076f41f95c8e118383892d55/encoding.bend as Encoding
bend-kit-bytes@0.3.0.0 via libs/HTTPClient.bend: import 0x49814d83de8f70993a43e1002be29ecd/bytes.bend as Bytes
bend-kit-url@0.4.1.0 via libs/HTTPClient.bend: import 0x1f2d80f53f971b16c6de6a65cb1918ae/url.bend as Url

Dependents

No package in this build imports it.

Status on bend 2.0.36

File	Status	Checker says	Time
LAWS.bend	fails	- expected : String output Error: - expected : String - observed : U32 Context: - name : String - ns : String - x : U32 Location: resolve.id 484 \| do IO<Maybe<&2, String>>: 485>\| u : Result<&1, &1, U32 & String, Socket> <- UDP.bind(0) \| ^ 486 \| resolve.sock(ns, U32.and(x, 65535), name, u)	2.8 s
PROOF.bend	fails	- expected : String output Error: - expected : String - observed : U32 Context: - name : String - ns : String - x : U32 Location: resolve.id 484 \| do IO<Maybe<&2, String>>: 485>\| u : Result<&1, &1, U32 & String, Socket> <- UDP.bind(0) \| ^ 486 \| resolve.sock(ns, U32.and(x, 65535), name, u)	4.0 s
bend_libs.bend	fails	- expected : String output Error: - expected : String - observed : U32 Context: - name : String - ns : String - x : U32 Location: resolve.id 484 \| do IO<Maybe<&2, String>>: 485>\| u : Result<&1, &1, U32 & String, Socket> <- UDP.bind(0) \| ^ 486 \| resolve.sock(ns, U32.and(x, 65535), name, u)	4.2 s
libs/HTTPClient.bend	fails	- expected : String output Error: - expected : String - observed : U32 Context: - name : String - ns : String - x : U32 Location: resolve.id 484 \| do IO<Maybe<&2, String>>: 485>\| u : Result<&1, &1, U32 & String, Socket> <- UDP.bind(0) \| ^ 486 \| resolve.sock(ns, U32.and(x, 65535), name, u)	3.5 s
libs/JSON.bend	checks	ALL PROOFS CHECK	3.6 s
libs/SQL.bend	fails	- expected : String output Error: - expected : String - observed : U32 Context: - name : String - ns : String - x : U32 Location: resolve.id 484 \| do IO<Maybe<&2, String>>: 485>\| u : Result<&1, &1, U32 & String, Socket> <- UDP.bind(0) \| ^ 486 \| resolve.sock(ns, U32.and(x, 65535), name, u)	3.2 s
libs/wire/deps/bytes.bend	checks	ALL PROOFS CHECK	0.6 s
libs/wire/deps/int.bend	checks	ALL PROOFS CHECK	0.7 s
libs/wire/dns.bend	fails	- expected : String output Error: - expected : String - observed : U32 Context: - name : String - ns : String - x : U32 Location: resolve.id 484 \| do IO<Maybe<&2, String>>: 485>\| u : Result<&1, &1, U32 & String, Socket> <- UDP.bind(0) \| ^ 486 \| resolve.sock(ns, U32.and(x, 65535), name, u)	0.7 s
libs/wire/wire.bend	relies on unsafe/foreign	19 defs rely on unsafe or foreign code defs: `connect`, `recv`, `send`, `send.timeout`, `recv_from`, `send_to`, `tls.connect`, `tls.connect.cert`, `tls.connect.alpn`, `tls.send`, `tls.send.timeout`, `tls.recv`, `tls.close`, `recv.words`, `send.words`, `recv_from.words`, `send_to.words`, `tls.recv.words`, `tls.send.words` output SOME PROOFS FAIL Error: 19 defs rely on unsafe or foreign code: - connect - recv - send - send.timeout - recv_from - send_to - tls.connect - tls.connect.cert - tls.connect.alpn - tls.send - tls.send.timeout - tls.recv - tls.close - recv.words - send.words - recv_from.words - send_to.words - tls.recv.words - tls.send.words	0.5 s
proof/HTTPClientProof.bend	fails	- expected : String output Error: - expected : String - observed : U32 Context: - name : String - ns : String - x : U32 Location: resolve.id 484 \| do IO<Maybe<&2, String>>: 485>\| u : Result<&1, &1, U32 & String, Socket> <- UDP.bind(0) \| ^ 486 \| resolve.sock(ns, U32.and(x, 65535), name, u)	3.1 s
proof/JSON_AssemblyProof.bend	checks	ALL PROOFS CHECK	5.4 s
proof/JSON_LexWhitespaceProof.bend	checks	ALL PROOFS CHECK	5.4 s
proof/JSON_ListProof.bend	checks	ALL PROOFS CHECK	0.6 s
proof/JSON_NumberLexProof.bend	checks	ALL PROOFS CHECK	5.3 s
proof/JSON_ParallelProof.bend	checks	ALL PROOFS CHECK	3.7 s
proof/JSON_PrimitiveProof.bend	checks	ALL PROOFS CHECK	4.7 s
proof/JSON_RenderLexProof.bend	checks	ALL PROOFS CHECK	7.1 s
proof/JSON_SourceProof.bend	checks	ALL PROOFS CHECK	6.9 s
proof/JSON_StringProof.bend	checks	ALL PROOFS CHECK	6.2 s
usage/HTTP.bend	fails	- expected : String output Error: - expected : String - observed : U32 Context: - name : String - ns : String - x : U32 Location: resolve.id 484 \| do IO<Maybe<&2, String>>: 485>\| u : Result<&1, &1, U32 & String, Socket> <- UDP.bind(0) \| ^ 486 \| resolve.sock(ns, U32.and(x, 65535), name, u)	3.8 s
usage/HTTP_Decode.bend	fails	- expected : String output Error: - expected : String - observed : U32 Context: - name : String - ns : String - x : U32 Location: resolve.id 484 \| do IO<Maybe<&2, String>>: 485>\| u : Result<&1, &1, U32 & String, Socket> <- UDP.bind(0) \| ^ 486 \| resolve.sock(ns, U32.and(x, 65535), name, u)	4.3 s
usage/HTTP_Encode.bend	fails	- expected : String output Error: - expected : String - observed : U32 Context: - name : String - ns : String - x : U32 Location: resolve.id 484 \| do IO<Maybe<&2, String>>: 485>\| u : Result<&1, &1, U32 & String, Socket> <- UDP.bind(0) \| ^ 486 \| resolve.sock(ns, U32.and(x, 65535), name, u)	4.4 s
usage/HTTP_GPU.bend	fails	- expected : String output Error: - expected : String - observed : U32 Context: - name : String - ns : String - x : U32 Location: resolve.id 484 \| do IO<Maybe<&2, String>>: 485>\| u : Result<&1, &1, U32 & String, Socket> <- UDP.bind(0) \| ^ 486 \| resolve.sock(ns, U32.and(x, 65535), name, u)	4.6 s
usage/HTTP_JSON.bend	fails	- expected : String output Error: - expected : String - observed : U32 Context: - name : String - ns : String - x : U32 Location: resolve.id 484 \| do IO<Maybe<&2, String>>: 485>\| u : Result<&1, &1, U32 & String, Socket> <- UDP.bind(0) \| ^ 486 \| resolve.sock(ns, U32.and(x, 65535), name, u)	4.0 s
usage/HTTP_Send.bend	fails	- expected : String output Error: - expected : String - observed : U32 Context: - name : String - ns : String - x : U32 Location: resolve.id 484 \| do IO<Maybe<&2, String>>: 485>\| u : Result<&1, &1, U32 & String, Socket> <- UDP.bind(0) \| ^ 486 \| resolve.sock(ns, U32.and(x, 65535), name, u)	4.0 s
usage/HTTP_URL.bend	fails	- expected : String output Error: - expected : String - observed : U32 Context: - name : String - ns : String - x : U32 Location: resolve.id 484 \| do IO<Maybe<&2, String>>: 485>\| u : Result<&1, &1, U32 & String, Socket> <- UDP.bind(0) \| ^ 486 \| resolve.sock(ns, U32.and(x, 65535), name, u)	4.4 s
usage/JSON_GPU.bend	checks	ALL PROOFS CHECK	4.8 s
usage/JSON_SafeTest.bend	checks	ALL PROOFS CHECK	5.3 s