From c26ad351242b381326be1d6f873ca30a3f04d113 Mon Sep 17 00:00:00 2001 From: Noah Gardner Date: Tue, 29 Sep 2026 19:49:42 -0400 Subject: [PATCH] feat!: server takes the host to bind; bend 2.0.34 Bend 2.0.32 made TCP.listen take the address to bind, so the server now takes a host before the port, as bend does: http.serve(handle, host: String, port: U32, limit: U32) http.serve_once(handle, host: String, port: U32) server.listen(host: String, port: U32) server.serve(handle, host, port, limit) server.once(handle, host, port) 2.0.32's verdict covers every def of every import, and main.bend and client.bend reach the wire effect, so PROOF.bend no longer imports them: the pure header helpers move to auth.bend and the wire spec to wirespec.bend (client.bend and wire.bend delegate, same names), LAWS.bend states their laws there, and the laws on the entry's re-exports move to ENTRY.bend. PROOF.bend prints ALL PROOFS CHECK; ENTRY.bend's only error is the foreign-code list, and checks.proofs holds both to that. The flake pins bend at 777ee0b (2.0.34); ez stays on its own bend (2.0.31) with bolt v1.9.0, which builds there. The bench driver drops the program name IO.args now puts first, and binds 127.0.0.1. BREAKING CHANGE: http.serve and http.serve_once (and server.listen, server.serve, server.once) take `host: String` before `port`, the address to bind, e.g. "127.0.0.1" for loopback or "0.0.0.0" for every interface. Replace `http.serve(handle, 8080, n)` with `http.serve(handle, "127.0.0.1", 8080, n)`. ezhttp now needs bend 2.0.32 or later. Co-Authored-By: Claude Opus 5.5 --- README.md | 14 ++- bench/main.bend | 11 ++- ez.lock.toml | 6 +- ez.toml | 6 +- ezhttp/ENTRY.bend | 204 +++++++++++++++++++++++++++++++++++++++++++ ezhttp/LAWS.bend | 110 ++--------------------- ezhttp/PROOF.bend | 52 ----------- ezhttp/auth.bend | 13 +++ ezhttp/client.bend | 10 +-- ezhttp/main.bend | 15 ++-- ezhttp/server.bend | 18 ++-- ezhttp/wire.bend | 13 +-- ezhttp/wirespec.bend | 18 ++++ flake.lock | 15 ++-- flake.nix | 39 +++++++-- 15 files changed, 336 insertions(+), 208 deletions(-) create mode 100644 ezhttp/ENTRY.bend create mode 100644 ezhttp/auth.bend create mode 100644 ezhttp/wirespec.bend diff --git a/README.md b/README.md index af3e1db..fd3daae 100644 --- a/README.md +++ b/README.md @@ -1,6 +1,7 @@ # ezhttp HTTP client and server for [Bend 2](https://github.com/bendlang/bend). +It needs bend 2.0.32 or later (the server binds `TCP.listen(host, port)`). ## Install @@ -56,9 +57,10 @@ def create() -> IO(Client.Response): ### Server -`http.serve` listens with Base TCP, accepts connections, parses one request +`http.serve(handle, host, port, limit)` listens with Base TCP on `host` +(`"127.0.0.1"` for loopback only, `"0.0.0.0"` for every interface), accepts connections, parses one request per connection, calls a pure handler, and writes one response -(`Connection: close`). `http.serve_once` stops after a single client. No TLS +(`Connection: close`). `http.serve_once(handle, host, port)` stops after a single client. No TLS in v0 for the server. A HEAD response is written with an empty body. ``` @@ -73,7 +75,7 @@ def handle(req: Msg.Request) -> Msg.Reply: Msg.Reply{200, [], "ok"} def main() -> IO(Unit): - Http.http.serve(handle, 8080, 1024) + Http.http.serve(handle, "127.0.0.1", 8080, 1024) ``` Cookies, `Cache-Control`, and CORS are pure helpers on the same messages. @@ -121,7 +123,11 @@ never pair with `Access-Control-Allow-Origin: *`. ## Compliance Closed equalities in `ezhttp/LAWS.bend`, proved in `ezhttp/PROOF.bend` -(`bend ezhttp/PROOF.bend`), target: +(`bend ezhttp/PROOF.bend` prints `ALL PROOFS CHECK`). The laws that say the +entry's re-exports and the client's header helpers equal those pure +definitions are in `ezhttp/ENTRY.bend`. `main.bend` and `client.bend` reach +the wire effect, so bend's verdict on that file is `SOME PROOFS FAIL`, with +the list of defs that rely on foreign code as its only error. The laws target: - [RFC 3986](https://www.rfc-editor.org/rfc/rfc3986) URI: scheme before the first colon and lowercased (§3.1), `hier-part` requiring `//` (§3), diff --git a/bench/main.bend b/bench/main.bend index 1d0e4da..20389f2 100644 --- a/bench/main.bend +++ b/bench/main.bend @@ -519,11 +519,11 @@ def handle(req: Msg.Request) -> Msg.Reply: # listen; the handler is closed, so fixtures stay in the binary def serve.go(port: U32, limit: U32) -> IO(Unit): - Http.http.serve(handle, port, limit) + Http.http.serve(handle, "127.0.0.1", port, limit) # one connection, then stop def once.go(port: U32) -> IO(Unit): - Http.http.serve_once(handle, port) + Http.http.serve_once(handle, "127.0.0.1", port) # serve port limit def run.serve(+cmd: String, a1: String, a2: String) -> IO(Unit): @@ -608,9 +608,14 @@ def main.go.un(quad: String & String & String & String) -> IO(Unit): (cmd, a1, a2, a3) = quad run.ping(cmd, a1, a2, a3) +# drop the program (bend 2.0.32 puts it at the head of IO.args), then # unpack argv and run the named command def main.go(args: List) -> IO(Unit): - main.go.un(argv.w0(args)) + match args: + case Nil{}: + main.go.un(argv.w0([])) + case prog <> rest: + main.go.un(argv.w0(rest)) # CLI entry def main() -> IO(Unit): diff --git a/ez.lock.toml b/ez.lock.toml index e2eb059..c95f606 100644 --- a/ez.lock.toml +++ b/ez.lock.toml @@ -23,8 +23,8 @@ LICENSE = "309f5aae946e4db157750e002fb179a74ed0fe27fce09a7be68a6977b14f205f" [tools] [tools.bolt] git = "https://github.com/Emerging-Patterns/bolt" -rev = "02fb09377f5c0fbddb5f6b7c32c8ab4ae14240df" -tag = "v1.8.0" +rev = "d5a67600a96ba423f2212bd661a30c1fba38eb55" +tag = "v1.9.0" root = "." -narHash = "sha256-53zE+3lZ/jn9GvIeGoavvNMaFyUs5dEFWd7fwP49TlM=" +narHash = "sha256-HmJ8J1xDshBdSWXIiEp48GZ9qHsm+bmpHw06ZWwcDVE=" entry = "main.bend" diff --git a/ez.toml b/ez.toml index 6d0f999..e622bbc 100644 --- a/ez.toml +++ b/ez.toml @@ -13,8 +13,8 @@ entry = "main.bend" [tools.bolt] git = "https://github.com/Emerging-Patterns/bolt" -rev = "02fb09377f5c0fbddb5f6b7c32c8ab4ae14240df" -tag = "v1.8.0" +rev = "d5a67600a96ba423f2212bd661a30c1fba38eb55" +tag = "v1.9.0" root = "." -narHash = "sha256-53zE+3lZ/jn9GvIeGoavvNMaFyUs5dEFWd7fwP49TlM=" +narHash = "sha256-HmJ8J1xDshBdSWXIiEp48GZ9qHsm+bmpHw06ZWwcDVE=" entry = "main.bend" diff --git a/ezhttp/ENTRY.bend b/ezhttp/ENTRY.bend new file mode 100644 index 0000000..4fd7cf2 --- /dev/null +++ b/ezhttp/ENTRY.bend @@ -0,0 +1,204 @@ +# ezhttp: laws on the entry (main.bend) and client.bend. Their re-exports and +# helpers are the pure definitions LAWS.bend states laws for. +# +# main.bend and client.bend reach the wire effect (user foreign code), so from +# bend 2.0.32 no file importing them can print ALL PROOFS CHECK: the verdict +# covers every def of every import. `bend ezhttp/ENTRY.bend` must print +# SOME PROOFS FAIL with the foreign-code list as its only error (the wire +# effect and the defs that reach it); the flake's proofs check holds it to that. +import Base +import ./http.bend as Http +import ./url.bend as Url +import ./body.bend as Body +import ./auth.bend as Auth +import ./cookie.bend as Cookie +import ./cache.bend as Cache +import ./cors.bend as Cors +import ./client.bend as Client +import ./main.bend as Ez + +# LAW: parse_url is Url.parse +law parse_url_is_url_parse: + for url: String + {Ez.parse_url(url) == Url.parse(url) : Url.Loc} + +# LAW: parse_response is Http.parse +law parse_response_is_http_parse: + for raw: String + {Ez.parse_response(raw) == Http.parse(raw) : Http.Reply} + +# LAW: parse_request is Http.ask +law parse_request_is_ask: + for raw: String + {Ez.parse_request(raw) == Http.ask(raw) : Http.Request} + +# LAW: format_response is Http.respond +law format_response_is_respond: + for +status: U32 + for hs: List<&2, Http.Header> + for +body: String + {Ez.format_response(status, hs, body) == Http.respond(status, hs, body) + : String} + +# LAW: empty_body is empty +law empty_body_is_empty: + {Ez.empty_body() == Body.body.empty() : Body.Body} + +# LAW: text_body wraps Text +law text_body_is_text: + for s: String + {Ez.text_body(s) == Body.body.text(s) : Body.Body} + +# LAW: octets_body wraps Octets +law octets_body_is_octets: + for bs: List<&2, U32> + {Ez.octets_body(bs) == Body.body.octets(bs) : Body.Body} + +# LAW: bearer builds Authorization: Bearer … +law bearer_is_authorization: + for token: String + {Ez.bearer(token) == Http.H{"Authorization", "Bearer " ++ token} + : Http.Header} + +# LAW: bearer is the client helper (reaches client.bend for type coverage) +law bearer_is_client_bearer: + for token: String + {Ez.bearer(token) == Client.client.bearer(token) : Http.Header} + +# LAW: encode is Body.body.encode (identity of the wrapper) +law encode_is_body_encode: + for +s: String + {Ez.encode(String, x => x, s) == Body.body.encode(String, x => x, s) + : Body.Body} + +# LAW: decode is Body.body.decode +law decode_is_body_decode: + for +s: String + {Ez.decode(String, x => Some{x}, s) + == Body.body.decode(String, x => Some{x}, s) : Maybe<&2, String>} + +# LAW (RFC 7617 §2): Basic credentials are Base64 of user:password +law basic_user_pass: + {Ez.basic("user", "pass") + == Http.H{"Authorization", "Basic dXNlcjpwYXNz"} : Http.Header} + +# LAW: basic is the client helper +law basic_is_client_basic: + for user: String + for password: String + {Ez.basic(user, password) == Client.client.basic(user, password) + : Http.Header} + +# LAW: set_cookie is the Set-Cookie serializer +law set_cookie_is_cookie_set: + for c: Cookie.Cookie + {Ez.set_cookie(c) == Cookie.cookie.set(c) : Http.Header} + +# LAW: parse_cookie is the Set-Cookie parser +law parse_cookie_is_parse: + for line: String + {Ez.parse_cookie(line) == Cookie.cookie.parse(line) + : Maybe<&2, Cookie.Cookie>} + +# LAW: cookie_header is the Cookie request header +law cookie_header_is_request: + for cs: List<&2, Cookie.Cookie> + {Ez.cookie_header(cs) == Cookie.cookie.request(cs) : Http.Header} + +# LAW: cache_control is the Cache-Control parser +law cache_control_is_parse: + for value: String + {Ez.cache_control(value) == Cache.cache.parse(value) : Cache.Cc} + +# LAW: fresh is freshness of the parsed directives +law fresh_is_cache_fresh: + for value: String + for age: Nat + {Ez.fresh(value, age) + == Cache.cache.fresh(Cache.cache.parse(value), age) : Bool} + +# LAW: cors_reply is the CORS helper +law cors_reply_is_on: + for cfg: Cors.Cfg + for req: Http.Request + for reply: Http.Reply + {Ez.cors_reply(cfg, req, reply) == Cors.cors.on(cfg, req, reply) + : Http.Reply} + +# --- fills --- + +# parse_url_is_url_parse holds by unfolding the re-export +def parse_url_is_url_parse(_url): + {==} + +# parse_response_is_http_parse holds by unfolding the re-export +def parse_response_is_http_parse(_raw): + {==} + +# parse_request_is_ask holds by unfolding the re-export +def parse_request_is_ask(_raw): + {==} + +# format_response_is_respond holds by unfolding the re-export +def format_response_is_respond(_status, _hs, _body): + {==} + +# empty_body_is_empty holds by unfolding the re-export +def empty_body_is_empty(): + {==} + +# text_body_is_text holds by unfolding the re-export +def text_body_is_text(_s): + {==} + +# octets_body_is_octets holds by unfolding the re-export +def octets_body_is_octets(_bs): + {==} + +# bearer_is_authorization holds by unfolding the re-export +def bearer_is_authorization(_token): + {==} + +# bearer_is_client_bearer holds by unfolding the re-export +def bearer_is_client_bearer(_token): + {==} + +# encode_is_body_encode holds by unfolding the re-export +def encode_is_body_encode(_s): + {==} + +# decode_is_body_decode holds by unfolding the re-export +def decode_is_body_decode(_s): + {==} + +# basic_user_pass holds by unfolding the re-export +def basic_user_pass(): + {==} + +# basic_is_client_basic holds by unfolding the re-export +def basic_is_client_basic(_user, _password): + {==} + +# set_cookie_is_cookie_set holds by unfolding the re-export +def set_cookie_is_cookie_set(_c): + {==} + +# parse_cookie_is_parse holds by unfolding the re-export +def parse_cookie_is_parse(_line): + {==} + +# cookie_header_is_request holds by unfolding the re-export +def cookie_header_is_request(_cs): + {==} + +# cache_control_is_parse holds by unfolding the re-export +def cache_control_is_parse(_value): + {==} + +# fresh_is_cache_fresh holds by unfolding the re-export +def fresh_is_cache_fresh(_value, _age): + {==} + +# cors_reply_is_on holds by unfolding the re-export +def cors_reply_is_on(_cfg, _req, _reply): + {==} diff --git a/ezhttp/LAWS.bend b/ezhttp/LAWS.bend index 014ea4b..925b915 100644 --- a/ezhttp/LAWS.bend +++ b/ezhttp/LAWS.bend @@ -7,14 +7,13 @@ import Base import ./http.bend as Http import ./url.bend as Url import ./body.bend as Body -import ./client.bend as Client -import ./wire.bend as Wire +import ./auth.bend as Auth +import ./wirespec.bend as Spec import ./b64.bend as B64 import ./cookie.bend as Cookie import ./cache.bend as Cache import ./cors.bend as Cors import ./json.bend as Json -import ./main.bend as Ez import 0x81c67699424929b5c44cd8577e18117f/main.bend as Ezjson # LAW (RFC 3986 §3.3 path-absolute / path-abempty with authority): the path a @@ -293,66 +292,12 @@ law url_show_opens_with_scheme: # --- main API surface (named so bolt laws stay clean) --- -# LAW: parse_url is Url.parse -law parse_url_is_url_parse: - for url: String - {Ez.parse_url(url) == Url.parse(url) : Url.Loc} - -# LAW: parse_response is Http.parse -law parse_response_is_http_parse: - for raw: String - {Ez.parse_response(raw) == Http.parse(raw) : Http.Reply} - -# LAW: parse_request is Http.ask -law parse_request_is_ask: - for raw: String - {Ez.parse_request(raw) == Http.ask(raw) : Http.Request} - -# LAW: format_response is Http.respond -law format_response_is_respond: - for +status: U32 - for hs: List<&2, Http.Header> - for +body: String - {Ez.format_response(status, hs, body) == Http.respond(status, hs, body) - : String} - -# LAW: empty_body is empty -law empty_body_is_empty: - {Ez.empty_body() == Body.body.empty() : Body.Body} - -# LAW: text_body wraps Text -law text_body_is_text: - for s: String - {Ez.text_body(s) == Body.body.text(s) : Body.Body} - -# LAW: octets_body wraps Octets -law octets_body_is_octets: - for bs: List<&2, U32> - {Ez.octets_body(bs) == Body.body.octets(bs) : Body.Body} - # LAW: bearer builds Authorization: Bearer … law bearer_is_authorization: for token: String - {Ez.bearer(token) == Http.H{"Authorization", "Bearer " ++ token} + {Auth.auth.bearer(token) == Http.H{"Authorization", "Bearer " ++ token} : Http.Header} -# LAW: bearer is the client helper (reaches client.bend for type coverage) -law bearer_is_client_bearer: - for token: String - {Ez.bearer(token) == Client.client.bearer(token) : Http.Header} - -# LAW: encode is Body.body.encode (identity of the wrapper) -law encode_is_body_encode: - for +s: String - {Ez.encode(String, x => x, s) == Body.body.encode(String, x => x, s) - : Body.Body} - -# LAW: decode is Body.body.decode -law decode_is_body_decode: - for +s: String - {Ez.decode(String, x => Some{x}, s) - == Body.body.decode(String, x => Some{x}, s) : Maybe<&2, String>} - # --- RFC 3986 authority, query, fragment --- # LAW (RFC 3986 §3.3): an empty path-abempty is the origin-form `/` @@ -404,12 +349,12 @@ law url_https_explicit_port: # LAW (RFC 2818): a secure exchange is labeled tls, on the given port law wire_https_is_tls: - {Wire.wire.spec(True{}, "example.com", 443, "GET / HTTP/1.1\r\n\r\n") + {Spec.wire.spec(True{}, "example.com", 443, "GET / HTTP/1.1\r\n\r\n") == "tls\nexample.com\n443\nGET / HTTP/1.1\r\n\r\n" : String} # LAW: a cleartext exchange is labeled tcp law wire_http_is_tcp: - {Wire.wire.spec(False{}, "example.com", 80, "GET / HTTP/1.1\r\n\r\n") + {Spec.wire.spec(False{}, "example.com", 80, "GET / HTTP/1.1\r\n\r\n") == "tcp\nexample.com\n80\nGET / HTTP/1.1\r\n\r\n" : String} # --- RFC 9112 request and response writers --- @@ -618,16 +563,9 @@ law b64_foo: # LAW (RFC 7617 §2): Basic credentials are Base64 of user:password law basic_user_pass: - {Ez.basic("user", "pass") + {Auth.auth.basic("user", "pass") == Http.H{"Authorization", "Basic dXNlcjpwYXNz"} : Http.Header} -# LAW: basic is the client helper -law basic_is_client_basic: - for user: String - for password: String - {Ez.basic(user, password) == Client.client.basic(user, password) - : Http.Header} - # --- RFC 6265 cookies --- # LAW (RFC 6265 §4.1.1): attributes serialize with `; ` separators @@ -720,22 +658,6 @@ law cookie_max_age_open: law cookie_session_alive: {Cookie.cookie.alive("", 5n) == True{} : Bool} -# LAW: set_cookie is the Set-Cookie serializer -law set_cookie_is_cookie_set: - for c: Cookie.Cookie - {Ez.set_cookie(c) == Cookie.cookie.set(c) : Http.Header} - -# LAW: parse_cookie is the Set-Cookie parser -law parse_cookie_is_parse: - for line: String - {Ez.parse_cookie(line) == Cookie.cookie.parse(line) - : Maybe<&2, Cookie.Cookie>} - -# LAW: cookie_header is the Cookie request header -law cookie_header_is_request: - for cs: List<&2, Cookie.Cookie> - {Ez.cookie_header(cs) == Cookie.cookie.request(cs) : Http.Header} - # --- RFC 9111 cache directives --- # LAW (RFC 9111 §5.2): directive names are case-insensitive @@ -789,18 +711,6 @@ law fresh_max_age_overrides_expires: law cache_max_age_present: {Cache.cache.max_age(Cache.cache.parse("max-age=1")) == True{} : Bool} -# LAW: cache_control is the Cache-Control parser -law cache_control_is_parse: - for value: String - {Ez.cache_control(value) == Cache.cache.parse(value) : Cache.Cc} - -# LAW: fresh is freshness of the parsed directives -law fresh_is_cache_fresh: - for value: String - for age: Nat - {Ez.fresh(value, age) - == Cache.cache.fresh(Cache.cache.parse(value), age) : Bool} - # --- Fetch CORS (https://fetch.spec.whatwg.org/#cors-protocol) --- # LAW (Fetch CORS): credentials reflect the request origin, never `*` @@ -913,14 +823,6 @@ law cors_request_headers_header: {Cors.cors.request_headers("Content-Type") == Http.H{"Access-Control-Request-Headers", "Content-Type"} : Http.Header} -# LAW: cors_reply is the CORS helper -law cors_reply_is_on: - for cfg: Cors.Cfg - for req: Http.Request - for reply: Http.Reply - {Ez.cors_reply(cfg, req, reply) == Cors.cors.on(cfg, req, reply) - : Http.Reply} - # --- thicker fence: more closed witnesses of the same RFCs --- # LAW (RFC 3986 §3.2.3): http with no port is 80 diff --git a/ezhttp/PROOF.bend b/ezhttp/PROOF.bend index 27c1296..56801b6 100644 --- a/ezhttp/PROOF.bend +++ b/ezhttp/PROOF.bend @@ -3,8 +3,6 @@ import Base import ./http.bend as Http import ./url.bend as Url import ./body.bend as Body -import ./client.bend as Client -import ./main.bend as Ez import ./LAWS.bend as Laws # --- Base facts used by the framing proofs --- @@ -464,39 +462,9 @@ def Laws.url_show_bad_is_marked(why): def Laws.url_show_opens_with_scheme(scheme, host, port, path): eq.starts_append(scheme, " " ++ host ++ " " ++ U32.show(port) ++ " " ++ path) -def Laws.parse_url_is_url_parse(_url): - {==} - -def Laws.parse_response_is_http_parse(_raw): - {==} - -def Laws.parse_request_is_ask(_raw): - {==} - -def Laws.format_response_is_respond(_status, _hs, _body): - {==} - -def Laws.empty_body_is_empty(): - {==} - -def Laws.text_body_is_text(_s): - {==} - -def Laws.octets_body_is_octets(_bs): - {==} - def Laws.bearer_is_authorization(_token): {==} -def Laws.bearer_is_client_bearer(_token): - {==} - -def Laws.encode_is_body_encode(_s): - {==} - -def Laws.decode_is_body_decode(_s): - {==} - def Laws.url_empty_path(): {==} @@ -659,9 +627,6 @@ def Laws.b64_foo(): def Laws.basic_user_pass(): {==} -def Laws.basic_is_client_basic(_user, _password): - {==} - def Laws.cookie_line_attributes(): {==} @@ -719,15 +684,6 @@ def Laws.cookie_max_age_open(): def Laws.cookie_session_alive(): {==} -def Laws.set_cookie_is_cookie_set(_c): - {==} - -def Laws.parse_cookie_is_parse(_line): - {==} - -def Laws.cookie_header_is_request(_cs): - {==} - def Laws.cache_directive_case(): {==} @@ -761,12 +717,6 @@ def Laws.fresh_max_age_overrides_expires(): def Laws.cache_max_age_present(): {==} -def Laws.cache_control_is_parse(_value): - {==} - -def Laws.fresh_is_cache_fresh(_value, _age): - {==} - def Laws.cors_credentials_reflect_origin(): {==} @@ -815,8 +765,6 @@ def Laws.cors_request_method_header(): def Laws.cors_request_headers_header(): {==} -def Laws.cors_reply_is_on(_cfg, _req, _reply): - {==} def Laws.url_http_default_port(): {==} diff --git a/ezhttp/auth.bend b/ezhttp/auth.bend new file mode 100644 index 0000000..bcc7c84 --- /dev/null +++ b/ezhttp/auth.bend @@ -0,0 +1,13 @@ +# ezhttp/auth: Authorization header values, pure. Kept apart from client.bend +# (which reaches the wire effect) so the proof gate can import it. +import Base +import ./http.bend as Http +import ./b64.bend as B64 + +# Authorization: Bearer … (RFC 6750) +def auth.bearer(token: String) -> Http.Header: + Http.H{"Authorization", "Bearer " ++ token} + +# Authorization: Basic … (RFC 7617, credentials are RFC 4648 Base64) +def auth.basic(user: String, password: String) -> Http.Header: + Http.H{"Authorization", "Basic " ++ B64.b64.encode(user ++ ":" ++ password)} diff --git a/ezhttp/client.bend b/ezhttp/client.bend index 6358772..45f7d8c 100644 --- a/ezhttp/client.bend +++ b/ezhttp/client.bend @@ -6,7 +6,7 @@ import ./url.bend as Url import ./http.bend as Http import ./body.bend as Body import ./wire.bend as Wire -import ./b64.bend as B64 +import ./auth.bend as Auth # structured client result: transport/parse error, or an HTTP response type Response is Data: @@ -99,10 +99,10 @@ def client.delete(url: String, headers: List<&2, Http.Header>, body: Body.Body) def client.options(url: String, headers: List<&2, Http.Header>) -> IO(Response): http.loc("OPTIONS", Url.parse(url), headers, "") -# Authorization: Bearer … +# Authorization: Bearer … (auth.bend) def client.bearer(token: String) -> Http.Header: - Http.H{"Authorization", "Bearer " ++ token} + Auth.auth.bearer(token) -# Authorization: Basic … (RFC 7617, credentials are RFC 4648 Base64) +# Authorization: Basic … (auth.bend; RFC 7617, RFC 4648 Base64) def client.basic(user: String, password: String) -> Http.Header: - Http.H{"Authorization", "Basic " ++ B64.b64.encode(user ++ ":" ++ password)} + Auth.auth.basic(user, password) diff --git a/ezhttp/main.bend b/ezhttp/main.bend index 9b4f307..7e3751f 100644 --- a/ezhttp/main.bend +++ b/ezhttp/main.bend @@ -143,14 +143,19 @@ def http.options_with(url: String, headers: List<&2, Http.Header>) -> IO(Client.Response): Client.client.options(url, headers) -# listen and serve up to `limit` connections +# listen on host:port and serve up to `limit` connections def http.serve( ~handle: Http.Request -> Http.Reply, + host: String, port: U32, limit: U32 ) -> IO(Unit): - Server.server.serve(handle, port, limit) + Server.server.serve(handle, host, port, limit) -# serve one connection then stop -def http.serve_once(~handle: Http.Request -> Http.Reply, port: U32) -> IO(Unit): - Server.server.once(handle, port) +# listen on host:port, serve one connection, then stop +def http.serve_once( + ~handle: Http.Request -> Http.Reply, + host: String, + port: U32 +) -> IO(Unit): + Server.server.once(handle, host, port) diff --git a/ezhttp/server.bend b/ezhttp/server.bend index db3e163..1ad0cf3 100644 --- a/ezhttp/server.bend +++ b/ezhttp/server.bend @@ -9,9 +9,10 @@ import ./cors.bend as Cors def server.max() -> U32: 65536 -# listen on a port (RFC 9112 connection establishment stays at the socket) -def server.listen(port: U32) -> IO(Listener): - IO.try(Listener, TCP.listen(port)) +# listen on a host address and port, e.g. "127.0.0.1" or "0.0.0.0" +# (RFC 9112 connection establishment stays at the socket) +def server.listen(host: String, port: U32) -> IO(Listener): + IO.try(Listener, TCP.listen(host, port)) # unpack accept: listener stays, socket from the Result def server.accept.of( @@ -247,10 +248,11 @@ def server.loop( # listen and serve up to `limit` connections def server.serve( ~handle: Http.Request -> Http.Reply, + host: String, port: U32, limit: U32 ) -> IO(Unit): - IO.bind(Listener, Unit, server.listen(port), + IO.bind(Listener, Unit, server.listen(host, port), lst => server.loop(handle, lst, limit)) # serve exactly one connection then stop @@ -262,7 +264,11 @@ def server.once.cont( IO.bind(Unit, Unit, server.exchange(handle, sock), _u => Listener.close(lst)) -def server.once(~handle: Http.Request -> Http.Reply, port: U32) -> IO(Unit): - IO.bind(Listener, Unit, server.listen(port), lst => +def server.once( + ~handle: Http.Request -> Http.Reply, + host: String, + port: U32 +) -> IO(Unit): + IO.bind(Listener, Unit, server.listen(host, port), lst => IO.bind(Listener & Socket, Unit, server.accept(lst), pair => server.once.cont(handle, pair))) diff --git a/ezhttp/wire.bend b/ezhttp/wire.bend index 4557bcd..15da751 100644 --- a/ezhttp/wire.bend +++ b/ezhttp/wire.bend @@ -5,23 +5,16 @@ # newline is the request verbatim. Answer: status on the first line, then text # ("0" and the raw response, or a non-zero code and the reason). import Base +import ./wirespec.bend as Spec # the exchange def ezwire.talk(spec: String) -> IO(String): import "./effs/wire.c" import "./effs/wire.js" -# the word the effect reads for a scheme that wants TLS -def wire.scheme(secure: Bool) -> String: - match secure: - case True{}: - "tls" - case False{}: - "tcp" - -# the spec the effect reads +# the spec the effect reads (wirespec.bend) def wire.spec(secure: Bool, host: String, port: U32, req: String) -> String: - wire.scheme(secure) ++ "\n" ++ host ++ "\n" ++ U32.show(port) ++ "\n" ++ req + Spec.wire.spec(secure, host, port, req) # a request sent to a host and its whole answer read back def wire.talk(secure: Bool, host: String, port: U32, req: String) -> IO(String): diff --git a/ezhttp/wirespec.bend b/ezhttp/wirespec.bend new file mode 100644 index 0000000..db9ddfb --- /dev/null +++ b/ezhttp/wirespec.bend @@ -0,0 +1,18 @@ +# ezhttp/wirespec: the text the wire effect reads, pure. Kept apart from +# wire.bend (the effect) so the proof gate can import it. +# +# Spec: scheme, host, port each on their own line; everything after the third +# newline is the request verbatim. +import Base + +# the word the effect reads for a scheme that wants TLS +def wire.scheme(secure: Bool) -> String: + match secure: + case True{}: + "tls" + case False{}: + "tcp" + +# the spec the effect reads +def wire.spec(secure: Bool, host: String, port: U32, req: String) -> String: + wire.scheme(secure) ++ "\n" ++ host ++ "\n" ++ U32.show(port) ++ "\n" ++ req diff --git a/flake.lock b/flake.lock index e2c72df..d916190 100644 --- a/flake.lock +++ b/flake.lock @@ -7,16 +7,17 @@ ] }, "locked": { - "lastModified": 1790359392, - "narHash": "sha256-z0Xwg46QesyRnlb7+sQue2GRq90v9M2XVaNVVSdd5Vs=", + "lastModified": 1790643370, + "narHash": "sha256-VYGPIHkNeccEaBHGer1B7+GNiWKQBiN/iiS7PozBXx0=", "owner": "bendlang", "repo": "bend", - "rev": "11c65a2572e16d0bfc2e83068b23ed8fb180ccc0", + "rev": "777ee0b55c485afdd7e68bd917b3d23a88d77371", "type": "github" }, "original": { "owner": "bendlang", "repo": "bend", + "rev": "777ee0b55c485afdd7e68bd917b3d23a88d77371", "type": "github" } }, @@ -25,17 +26,17 @@ "nixpkgs": "nixpkgs" }, "locked": { - "lastModified": 1790200275, - "narHash": "sha256-huYLnKbMUukFhFLypIXx/wLVU3EmgsUEe9l67mU6CDw=", + "lastModified": 1790482124, + "narHash": "sha256-Gv309ikt48M8cISbwSo6V0md2572iieIRiyl3noF1cA=", "owner": "bendlang", "repo": "bend", - "rev": "d37909174ebd664338ae3194799a9e0899dedd51", + "rev": "af569d4826913b2ce3557e9829ccad31fcf86f94", "type": "github" }, "original": { "owner": "bendlang", "repo": "bend", - "rev": "d37909174ebd664338ae3194799a9e0899dedd51", + "rev": "af569d4826913b2ce3557e9829ccad31fcf86f94", "type": "github" } }, diff --git a/flake.nix b/flake.nix index 1f932aa..90cbdb4 100644 --- a/flake.nix +++ b/flake.nix @@ -2,17 +2,19 @@ description = "ezhttp: HTTP client and server for Bend 2"; inputs.nixpkgs.url = "github:NixOS/nixpkgs/nixos-unstable"; + # bendlang/bend's flake at the commit that packages 2.0.34 (the v2.0.34 tag + # still packages 2.0.33) inputs.bend = { - url = "github:bendlang/bend"; + url = "github:bendlang/bend/777ee0b55c485afdd7e68bd917b3d23a88d77371"; inputs.nixpkgs.follows = "nixpkgs"; }; inputs.ez = { url = "github:Emerging-Patterns/ez"; inputs.nixpkgs.follows = "nixpkgs"; - # not `inputs.bend.follows = "bend"`: ez 1.2.0 does not build on bend - # 2.0.28, so ez (and `ez prove`, and bolt through mkLint) keep the bend - # ez 1.2.0 locks, 2.0.27 - inputs.bend.url = "github:bendlang/bend/d37909174ebd664338ae3194799a9e0899dedd51"; + # ez and its bolt stay on the bend ez's own flake.lock records until ez + # releases on 2.0.34, so ez's inputs.bend is pinned, not followed. The + # package's own builds and its proofs (checks.proofs) run on 2.0.34. + inputs.bend.url = "github:bendlang/bend/af569d4826913b2ce3557e9829ccad31fcf86f94"; }; outputs = { self, nixpkgs, ... }@inputs: @@ -40,7 +42,32 @@ apps.${system} = bench.apps; checks.${system} = { - proofs = ez.mkProofs { ez = ezBin; src = self; }; + # every PROOF.bend on this flake's bend: its first line must be + # ALL PROOFS CHECK. ez.mkProofs comes back when ez runs on 2.0.34. + # ezhttp/ENTRY.bend states the laws on main.bend and client.bend, + # which reach the wire effect, so its verdict is SOME PROOFS FAIL; + # its only error may be the list of defs relying on foreign code. + proofs = pkgs.runCommand "ezhttp-proofs" { + nativeBuildInputs = [ bend ]; + BEND_LIB = ez.bendLib ./ez.lock.toml; + } '' + export HOME=$TMPDIR + cp -r ${self} src && chmod -R u+w src && cd src + for p in $(find . -name PROOF.bend -not -path './.ez/*' | sort); do + first=$(cd "$(dirname "$p")" && bend "$(basename "$p")" | head -n 1) + echo "$p: $first" + [ "$first" = "ALL PROOFS CHECK" ] || exit 1 + done + out_entry=$(cd ezhttp && bend ENTRY.bend 2>&1 || true) + echo "$out_entry" | head -n 2 + [ "$(echo "$out_entry" | sed -n 1p)" = "SOME PROOFS FAIL" ] || exit 1 + echo "$out_entry" | sed -n 2p \ + | grep -Eq '^Error: [0-9]+ defs? rel(y|ies) on unsafe or foreign code:$' || exit 1 + if echo "$out_entry" | tail -n +3 | grep -v '^- ' | grep -q .; then + echo "$out_entry"; exit 1 + fi + touch $out + ''; lint = ez.mkLint { src = self; }; } // bench.checks;