feat!: server takes the host to bind; bend 2.0.34

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),

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<String>) -> 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):

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"

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"

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):
+  {==}