Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
18 changes: 9 additions & 9 deletions ezhttp/ENTRY.bend → ENTRY.bend
Original file line number Diff line number Diff line change
Expand Up @@ -3,18 +3,18 @@
#
# 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
# covers every def of every import. `bend 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 ./src/http.bend as Http
import ./src/url.bend as Url
import ./src/body.bend as Body
import ./src/auth.bend as Auth
import ./src/cookie.bend as Cookie
import ./src/cache.bend as Cache
import ./src/cors.bend as Cors
import ./src/client.bend as Client
import ./main.bend as Ez

# LAW: parse_url is Url.parse
Expand Down
22 changes: 11 additions & 11 deletions ezhttp/LAWS.bend → LAWS.bend
Original file line number Diff line number Diff line change
Expand Up @@ -2,18 +2,18 @@
# message framing (RFC 9112), HTTP semantics (RFC 9110), TLS selection
# (RFC 2818), Basic and Bearer credentials (RFC 7617, RFC 4648, RFC 6750),
# cookies (RFC 6265), caching directives (RFC 9111), and Fetch CORS.
# PROOF.bend fills them. `bend ezhttp/PROOF.bend` is the gate.
# PROOF.bend fills them. `bend PROOF.bend` is the gate.
import Base
import ./http.bend as Http
import ./url.bend as Url
import ./body.bend as Body
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 ./src/http.bend as Http
import ./src/url.bend as Url
import ./src/body.bend as Body
import ./src/auth.bend as Auth
import ./src/wirespec.bend as Spec
import ./src/b64.bend as B64
import ./src/cookie.bend as Cookie
import ./src/cache.bend as Cache
import ./src/cors.bend as Cors
import ./src/json.bend as Json
import 0x81c67699424929b5c44cd8577e18117f/main.bend as Ezjson

# LAW (RFC 3986 §3.3 path-absolute / path-abempty with authority): the path a
Expand Down
8 changes: 4 additions & 4 deletions ezhttp/PROOF.bend → PROOF.bend
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
# ezhttp: the proofs. `bend ezhttp/PROOF.bend` is the gate.
# ezhttp: the proofs. `bend PROOF.bend` is the gate.
import Base
import ./http.bend as Http
import ./url.bend as Url
import ./body.bend as Body
import ./src/http.bend as Http
import ./src/url.bend as Url
import ./src/body.bend as Body
import ./LAWS.bend as Laws

# --- Base facts used by the framing proofs ---
Expand Down
18 changes: 9 additions & 9 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,7 @@ Shared types cover both sides: `Header`, structured `Request` / `Reply`
(status or method, headers, body). Bodies are empty, UTF-8 text, or an octet
list. The HTTP API does not need JSON: `Request`, `Reply`, and the client
`Response` stay text and octets, and `encode` / `decode` take any codec. The
hub package is the HTTP library alone. `ezhttp/json.bend`, the optional
hub package is the HTTP library alone. `src/json.bend`, the optional
helper that calls [ezjson](https://github.com/Emerging-Patterns/ezjson), is
in this repository but not reachable from `main.bend`, so it is not in the
hub package; import ezjson from the hub to read a JSON body (below).
Expand All @@ -43,7 +43,7 @@ and port 443.

```
import 0x5e4e2a9db839a0214ace6923b04b685b/main.bend as Http
import 0x5e4e2a9db839a0214ace6923b04b685b/client.bend as Client
import 0x5e4e2a9db839a0214ace6923b04b685b/src/client.bend as Client

def main() -> IO(Client.Response):
Http.http.get("https://example.com/")
Expand All @@ -65,7 +65,7 @@ in v0 for the server. A HEAD response is written with an empty body.

```
import 0x5e4e2a9db839a0214ace6923b04b685b/main.bend as Http
import 0x5e4e2a9db839a0214ace6923b04b685b/http.bend as Msg
import 0x5e4e2a9db839a0214ace6923b04b685b/src/http.bend as Msg

def handle(req: Msg.Request) -> Msg.Reply:
match req:
Expand All @@ -82,9 +82,9 @@ Cookies, `Cache-Control`, and CORS are pure helpers on the same messages.

```
import 0x5e4e2a9db839a0214ace6923b04b685b/main.bend as Http
import 0x5e4e2a9db839a0214ace6923b04b685b/http.bend as Msg
import 0x5e4e2a9db839a0214ace6923b04b685b/cookie.bend as Cookie
import 0x5e4e2a9db839a0214ace6923b04b685b/cors.bend as Cors
import 0x5e4e2a9db839a0214ace6923b04b685b/src/http.bend as Msg
import 0x5e4e2a9db839a0214ace6923b04b685b/src/cookie.bend as Cookie
import 0x5e4e2a9db839a0214ace6923b04b685b/src/cors.bend as Cors

def authed() -> Msg.Header:
Http.basic("user", "pass")
Expand Down Expand Up @@ -122,10 +122,10 @@ never pair with `Access-Control-Allow-Origin: *`.

## Compliance

Closed equalities in `ezhttp/LAWS.bend`, proved in `ezhttp/PROOF.bend`
(`bend ezhttp/PROOF.bend` prints `ALL PROOFS CHECK`). The laws that say the
Closed equalities in `LAWS.bend`, proved in `PROOF.bend`
(`bend 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
definitions are in `ENTRY.bend`. `main.bend` and `src/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:

Expand Down
2 changes: 1 addition & 1 deletion bench/compare.nix
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@
# Request→response is timed by one ureq process, not a CLI wrapper.
# - Load: hey (outside the timed path) reports RPS and p50/p99. Same payload,
# count, and concurrency on both servers.
# - JSON cases use ezhttp/json.bend on the Bend side and serde_json on the
# - JSON cases use src/json.bend on the Bend side and serde_json on the
# Rust side. Text and octet bodies are the same fixture bytes.
# - Ratio = ezhttp/ref when both timers resolve. If MS stays 0, wall/n is
# reported and there is no vs claim. Ratios never fail the check.
Expand Down
5 changes: 3 additions & 2 deletions bench/default.nix
Original file line number Diff line number Diff line change
Expand Up @@ -18,14 +18,15 @@ let
bendLib = ez.bendLib (self + "/ez.lock.toml");

# Sandbox-safe CC: nixpkgs clang (native ELF). BEND_LIB is the locked ezjson
# tree, so ezhttp/json.bend resolves without a hub publish.
# tree, so src/json.bend resolves without a hub publish.
drv = pkgs.stdenv.mkDerivation {
pname = "ezhttp-bench-drv";
version = "0.1.0";
dontUnpack = true;
nativeBuildInputs = [ bend llvm.clang ];
buildPhase = ''
cp -r ${self}/ezhttp ./ezhttp
cp ${self}/main.bend ./main.bend
cp -r ${self}/src ./src
mkdir -p bench
cp ${./main.bend} bench/main.bend
cp ${./fix.bend} bench/fix.bend
Expand Down
14 changes: 7 additions & 7 deletions bench/main.bend
Original file line number Diff line number Diff line change
@@ -1,12 +1,12 @@
# Fair HTTP bench driver. Fixtures are loaded before IO.now. Timed loops stay
# in this process: GET/POST through ezhttp, and serve / serve_once for the
# server track. JSON cases call ezhttp/json.bend (ezjson). Core HTTP types
# server track. JSON cases call src/json.bend (ezjson). Core HTTP types
# stay text and octets.
import ../ezhttp/main.bend as Http
import ../ezhttp/http.bend as Msg
import ../ezhttp/body.bend as Body
import ../ezhttp/client.bend as Client
import ../ezhttp/json.bend as Json
import ../main.bend as Http
import ../src/http.bend as Msg
import ../src/body.bend as Body
import ../src/client.bend as Client
import ../src/json.bend as Json
import 0x81c67699424929b5c44cd8577e18117f/src/value.bend as V
import ./fix.bend as Fix

Expand Down Expand Up @@ -413,7 +413,7 @@ def reply.json.of(m: Maybe<&2, V.Json>) -> Msg.Reply:
case Some{j}:
reply.ok(ctype.json(), json.out(Some{j}))

# POST /json: parse with ezhttp/json.bend and answer with the print
# POST /json: parse with src/json.bend and answer with the print
def reply.json(body: String) -> Msg.Reply:
reply.json.of(Json.json.parse(body))

Expand Down
2 changes: 1 addition & 1 deletion ez.toml
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
[package]
name = "ezhttp"
entry = "ezhttp/main.bend"
entry = "main.bend"

[deps.ezjson]
hash = "0x81c67699424929b5c44cd8577e18117f"
Expand Down
4 changes: 2 additions & 2 deletions flake.nix
Original file line number Diff line number Diff line change
Expand Up @@ -44,7 +44,7 @@
checks.${system} = {
# 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,
# 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" {
Expand All @@ -58,7 +58,7 @@
echo "$p: $first"
[ "$first" = "ALL PROOFS CHECK" ] || exit 1
done
out_entry=$(cd ezhttp && bend ENTRY.bend 2>&1 || true)
out_entry=$(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 \
Expand Down
22 changes: 12 additions & 10 deletions ezhttp/main.bend → main.bend
Original file line number Diff line number Diff line change
@@ -1,14 +1,16 @@
# ezhttp: HTTP client and server for Bend 2. Shared message types, BYO JSON
# via encode/decode. TLS for the client stays at the wire/runtime layer.
# ezhttp: HTTP/1.1 client and server for Bend 2, with auth, cookie and CORS helpers.
#
# Shared message types, BYO JSON via encode/decode. TLS for the client stays
# at the wire/runtime layer.
import Base
import ./url.bend as Url
import ./http.bend as Http
import ./body.bend as Body
import ./client.bend as Client
import ./server.bend as Server
import ./cookie.bend as Cookie
import ./cache.bend as Cache
import ./cors.bend as Cors
import ./src/url.bend as Url
import ./src/http.bend as Http
import ./src/body.bend as Body
import ./src/client.bend as Client
import ./src/server.bend as Server
import ./src/cookie.bend as Cookie
import ./src/cache.bend as Cache
import ./src/cors.bend as Cors

# URL parse re-export
def parse_url(url: String) -> Url.Loc:
Expand Down
2 changes: 1 addition & 1 deletion ezhttp/auth.bend → src/auth.bend
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
# ezhttp/auth: Authorization header values, pure. Kept apart from client.bend
# ezhttp/src/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
Expand Down
2 changes: 1 addition & 1 deletion ezhttp/b64.bend → src/b64.bend
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
# ezhttp/b64: Base64 encoding for HTTP credentials (RFC 4648 §4). The
# ezhttp/src/b64: Base64 encoding for HTTP credentials (RFC 4648 §4). The
# alphabet is the standard table, with `=` padding. Decoding is not required
# for the Authorization helpers.
import Base
Expand Down
2 changes: 1 addition & 1 deletion ezhttp/body.bend → src/body.bend
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
# ezhttp/body: request entity as empty, UTF-8 text, or octet list. Core does
# ezhttp/src/body: request entity as empty, UTF-8 text, or octet list. Core does
# not depend on ezjson. Callers plug encode/decode through Bend type
# parameters (BYO JSON or any other representation).
import Base
Expand Down
2 changes: 1 addition & 1 deletion ezhttp/cache.bend → src/cache.bend
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
# ezhttp/cache: Cache-Control and a small freshness check (RFC 9111). This is
# ezhttp/src/cache: Cache-Control and a small freshness check (RFC 9111). This is
# not a shared cache. Expires is recorded; max-age overrides it for freshness.
# IMF-fixdate arithmetic is not evaluated.
import Base
Expand Down
2 changes: 1 addition & 1 deletion ezhttp/client.bend → src/client.bend
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
# ezhttp/client: fetch a URL. URL and HTTP parsing joined to the wire effect.
# ezhttp/src/client: fetch a URL. URL and HTTP parsing joined to the wire effect.
# Answers a structured Response (status + headers + body), not a hub-style
# "0\n…" string contract.
import Base
Expand Down
2 changes: 1 addition & 1 deletion ezhttp/cookie.bend → src/cookie.bend
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
# ezhttp/cookie: Set-Cookie and Cookie (RFC 6265 §§4–5). A thin jar: parse
# ezhttp/src/cookie: Set-Cookie and Cookie (RFC 6265 §§4–5). A thin jar: parse
# attributes, serialize the request header, and domain/path/secure matching.
# Expires is stored, not evaluated against a clock. SameSite is stored; there
# is no browsing context to suppress cross-site sends.
Expand Down
2 changes: 1 addition & 1 deletion ezhttp/cors.bend → src/cors.bend
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
# ezhttp/cors: Fetch CORS response headers for a simple request and an OPTIONS
# ezhttp/src/cors: Fetch CORS response headers for a simple request and an OPTIONS
# preflight. Origins are reflected, or `*`, and credentials never pair with `*`.
# See https://fetch.spec.whatwg.org/#cors-protocol.
import Base
Expand Down
File renamed without changes.
File renamed without changes.
2 changes: 1 addition & 1 deletion ezhttp/http.bend → src/http.bend
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
# ezhttp/http: HTTP/1.1 message text for client and server — request and
# ezhttp/src/http: HTTP/1.1 message text for client and server — request and
# response formatting/parsing — with no sockets. Semantics follow RFC 9110;
# message syntax and framing follow RFC 9112. TLS is outside this module.
import Base
Expand Down
2 changes: 1 addition & 1 deletion ezhttp/json.bend → src/json.bend
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
# ezhttp/json: optional JSON helpers. HTTP messages stay text and octets.
# ezhttp/src/json: optional JSON helpers. HTTP messages stay text and octets.
# This module is the only one that imports ezjson. Request, Reply, and the
# client Response do not.
import Base
Expand Down
2 changes: 1 addition & 1 deletion ezhttp/server.bend → src/server.bend
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
# ezhttp/server: listen, accept, parse one request, write one response.
# ezhttp/src/server: listen, accept, parse one request, write one response.
# Uses Base TCP (no TLS in v0). One exchange per connection with
# Connection: close. Handler is a pure Request -> Reply function.
import Base
Expand Down
2 changes: 1 addition & 1 deletion ezhttp/url.bend → src/url.bend
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
# ezhttp/url: a URL taken apart far enough for an HTTP request. Scheme, host,
# ezhttp/src/url: a URL taken apart far enough for an HTTP request. Scheme, host,
# port, and an origin-form path (absolute-path, optional query). Userinfo is
# stripped. The fragment is not part of the request-target.
#
Expand Down
2 changes: 1 addition & 1 deletion ezhttp/wire.bend → src/wire.bend
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
# ezhttp/wire: one request out and one response back. TLS and DNS stay in
# ezhttp/src/wire: one request out and one response back. TLS and DNS stay in
# the effect (OpenSSL via dlopen); this module does not re-specify TLS.
#
# Spec: scheme, host, port each on their own line; everything after the third
Expand Down
2 changes: 1 addition & 1 deletion ezhttp/wirespec.bend → src/wirespec.bend
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
# ezhttp/wirespec: the text the wire effect reads, pure. Kept apart from
# ezhttp/src/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
Expand Down
Loading