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;