li-httpd — minimal, proved, nginx-competitive¶

Parity milestones (agent-gateway vs nginx oracle)¶

Config/oracle todos may be completed while runtime parity rows stay pending until build/li-httpd passes full gates, tier5 bench/exploit vs nginx, and live SSE/TLS/H2/WS.

Non-goals (unchanged): nginx.conf drop-in, regex location, Lua/modules, HTTP/3, mail.

Honest starting point¶

Li today is optimized for proved HPC kernels (Tetris/SDL, physics benchmarks), not servers:

Product goal: AI/agent-native HTTP gateway — long-lived streaming (SSE), safe header policy, rate limits, load balancing to inference/tool backends, secure-by-design TOML (no misconfig vulns). Beat nginx on clarity and assurance at far lower LOC; match perf on agent workloads (many concurrent streams, fewer trivial GETs).

Not a goal: generic nginx clone, blog static hosting as primary story, or porting src/http/*.c.

Design pillars (in order)¶

Nginx source is read-only (what invariants matter). Li makes enforcing them smaller than C, not harder.

Self-contained delivery (you publish packages later)¶

Rule: implementation does not wait on crates, npm, or unpublished third-party Li packages. We write every dependency ourselves, split into publishable packages, and publish to a registry later; until lip (phase 8b+), use path / workspace deps only.

Package creation — master plan (do not hand-roll)¶

Follow Phase Pkg — package scaffold and canonical li.toml in lip plan § A3. Never invent a second manifest format.

Agents: use skill .cursor/skills/create-li-package — run li-new-package, do not mkdir/copy li.toml by hand.

lis repo note: infra stubs under packages/li-* were pre-Pkg placeholders; re-scaffold each with li-new-package once the script lands, then diff only intentional description / deps.

# From li compiler repo (after Pkg ships):
./scripts/li-new-package li-net --kind library --workspace packages --out /path/to/lis/packages
./scripts/li-new-package li-httpd --kind binary --workspace packages --out /path/to/lis/packages

Standard layout (scaffold output — same as lip):

packages/li-net/
  li.toml              # lip § A3 (edition, metadata.lip.min_coverage, …)
  li.lock              # lip install (8b+)
  README.md
  PUBLISH.md
  src/lib.li           # or src/main.li for binary (li-httpd)
  li-tests/manifest.toml
  li-tests/smoke/builds.li

Workspace root packages/li.toml or repo-root li.toml:

[workspace]
members = ["li-bytes", "li-net", "li-rng", "li-prob", "li-crypto", "li-tls", "li-acme", "li-schema", "li-log", "li-http", "li-httpd"]

li.toml excerpt (full schema: lip § A3):

[package]
name = "li-http"
version = "0.1.0"
edition = "2026"
license = "Apache-2.0 OR MIT"
description = "HTTP parser, router, proxy, leak_censor"

[dependencies]
li-net = { path = "../li-net" }

[package.metadata.lip]
min_coverage = 80

Default package split (each via li-new-package):

packages/
  li-bytes/ li-net/ li-rng/ li-prob/ li-crypto/ li-tls/ li-acme/
  li-schema/ li-log/ li-http/ li-httpd/
benchmarks/tier5_http/

li-httpd = binary (--kind binary); others = library. Publish via lip publish (8d) after proof + signature + coverage — not required for lis infra phase.

Harness / tooling: bench_http.py, exploit_http.py, audit_nginx_src.py in-repo (Python OK). Crypto: li-crypto in Li first; optional li-crypto-hacl org package later.

Agent discipline: engineering-standards.md (mandatory gates). Vision: product here; language/ecosystem in master plan. Learn from others: nginx/Envoy/LiteLLM for algorithms — not C ports; CVE rows in nginx_mitigations.toml + tier5 exploits must stay green.

Why provability makes li-httpd easier (not harder)¶

nginx stays secure by volume: checks scattered across modules, runtime limits, years of CVE patches, fuzzing, and ops lore. Li stays secure by theorem: one parser, one state machine, obligations that cannot compile if wrong.

What you write once (M1 core):

def parse_request(buf: bytes, limits: Limits) -> Result[Request, HttpError]
  requires buf.len <= limits.max_header_block
  ensures result.ok -> result.value.body_len <= limits.max_body
  decreases buf.len

If it builds, buffer over-reads and unbounded header growth are not “hopefully caught by tests”—they are obligations the toolchain rejected.

What stays small and trusted (explicit, RFC-capped):

• Syscalls (recv/send/epoll) in li_rt_net.c + trusted.lean
• Optional crypto extern boundary (M2) with contracts at the seam only

Exploit suite role (smaller than nginx QA): confirms [expect] on the trusted seam and that specs match reality—not to re-prove what Lean already proved.

Prerequisite: phases 2e–2f (VC → Lean on lic build). That gate is the reason M1 is tractable; without it, li-httpd is just another memory-safe language. P0 = turn on the proof pipeline, then M1 is mostly writing specs + thin code.

flowchart TB
  spec[requires ensures invariant]
  lean[Lean kernel]
  llvm[LLVM binary]
  exploit[exploit TOML on running server]
  spec --> lean
  lean --> llvm
  llvm --> exploit
  exploit -->|only if trusted or spec wrong| fix[fix spec or trusted]

Strategy: minimal implementation, nginx as oracle¶

flowchart LR
  audit[nginx CHANGES/CVE audit]
  map[nginx_mitigations.toml]
  design[Minimal li-httpd design]
  lihttpd[li-httpd small codebase]
  bench[bench TOML]
  exploits[exploit TOML]
  audit --> map
  map --> design
  design --> lihttpd
  map --> exploits
  bench --> nginx[stock nginx baseline]
  bench --> lihttpd
  exploits --> nginx
  exploits --> lihttpd

No porting: do not mirror nginx modules, structs, or config grammar. Where nginx has three parsers/paths, li-httpd uses one proved front-end.

LOC budget (enforced)¶

CI job: scripts/loc_httpd.sh fails if M1 exceeds budget without RFC. Prefer deleting features over growing LOC.

Capability scope (functionality without nginx parity)¶

Ship workloads, not nginx.conf compatibility:

M1 (v1 — minimal competitive server):

M2: HTTP/2 + gzip only if M1 meets perf gates under LOC cap.

M3 (optional): stream TCP proxy, WebSocket — RFC + LOC justification.

Explicit non-goals: HTTP/3, nginx config drop-in, mail module, module ecosystem.

flowchart TB
  toml[li-httpd.toml]
  router[Router host plus path]
  parse[Single HTTP parser]
  static[Static files]
  proxy[Reverse proxy]
  toml --> router
  router --> parse
  parse --> static
  parse --> proxy

Secure-by-design configuration (no user-induced vulns)¶

Principle: misconfiguration is a bug class nginx accepts (string DSL, sharp edges). li-httpd refuses to start on configs that could enable known vulnerability patterns—same rigor as parser proofs, applied to ops surface.

What nginx allows that we forbid¶

Config pipeline (validate before bind)¶

flowchart LR
  toml[li-httpd.toml]
  parse[Toml parse]
  schema[Config.validate]
  lean[Optional lic build on codegen]
  listen[bind listen sockets]
  toml --> parse
  parse --> schema
  schema -->|reject| err[exit 1 plus path]
  schema --> lean
  lean --> listen

1. **lic validate-config** — simple TOML → desugar → validate canonical
2. **li-httpd start** — refuse listen on error
3. **li-httpd explain-config** — show desugared TOML for debugging

Easy TOML (default — write this)¶

Ambiguous input → desugar error at line number (never guess).

[server]
listen = ":443"
host = "api.example.com"
tls = "lets_encrypt"
email = "ops@example.com"

[limits]
max_body = "1m"

[upstreams.inference_pool]
peers = ["http://10.0.0.1:8000", "http://10.0.0.2:8000"]

[routes]
"GET  /health"                  = "static:healthcheck"
"POST /v1/chat/completions"     = "proxy:inference_pool"
"POST /v1/*"                    = "proxy:inference_pool"
"POST /v1/*  x-model=gpt-4"     = "proxy:pool_gpt4"

Flatter: routes = ["GET /health -> static:healthcheck", ...] — do not mix with [routes] map.

Tests: li-tests/config_desugar/ golden files; li-httpd explain-config prints canonical form.

Typed schema (canonical — after desugar)¶

Config deserializes into HttpdConfig in std/http/config.li:

type UpstreamId = enum
  api_backend
  internal_only

type Route = object
  name: RouteName         # stable id for logs and tests
  match: MatchExpr        # structured — see "Readable routing" below
  action: RouteAction    # StaticRoot | Proxy(UpstreamId)

type HttpdConfig = object
  listen: ListenAddr
  routes: seq[Route]      # sorted by explicit priority at validate
  limits: Limits

Readable routing (replaces nginx regex)¶

Problem with nginx: location ~* ^/api/v[0-9]+/ is hard to read, order-dependent (=, ^~, ~), and easy to misconfigure into smuggling or accidental broad matches.

li-httpd rule: no PCRE / no user-supplied regex strings in config. Use a small MatchExpr algebra that reads top-to-bottom like a route table.

Match types (enum per field)¶

Priority: simple [routes] map uses file order (first line wins). Canonical [[routes]] may set explicit priority; ties → compile error.

Logs use route name from desugar (openai_chat auto from "POST /v1/*" → post_v1_wildcard or explicit name in advanced block).

nginx → li-httpd cheat sheet (migration doc)¶

Optional later: **li-httpd import-nginx-locations** suggests li routes from nginx.conf (best-effort, never emits regex — flags manual review).

Proved router (std/http/router.li)¶

def match_route(table: RouteTable, req: RequestView) -> Option[RouteName]
  requires table.sorted_valid
  ensures result.isSome -> route_matches(table[result.get], req)
  ensures result.isNone -> forall r in table, not route_matches(r, req)
  decreases table.len

route_matches is total and composed only from structurally recursive matchers (no backtracking regex engine).

Routing tests (functionality guaranteed)¶

Layout:

li-tests/routing/
  manifest.toml              # lists case files
  cases/
    api_prefix.toml          # table: request -> expect route
    host_suffix.toml
    method_reject.toml
    overlap_reject.toml      # config that must fail validate
  good/
    deterministic_order.li   # compile-time router unit tests (lic build)

Case file format (TOML — same ergonomics as bench):

[[case]]
id = "chat_completions"
request = { method = "POST", host = "api.example.com", path = "/v1/chat/completions" }
expect = { route = "openai_chat", action = "proxy" }

[[case]]
id = "health"
request = { method = "GET", host = "api.example.com", path = "/health" }
expect = { route = "health", action = "static" }

[[case]]
id = "no_match"
request = { method = "GET", host = "api.example.com", path = "/unknown" }
expect = { status = 404 }

Harness: ./li-tests/run_routing.sh (or run_all.sh routing suite):

1. Load examples/li-httpd/fixtures/routing.toml config
2. For each case: build RequestView, call match_route, assert route / status
3. CI: must pass on every PR touching std/http/router.li or match types

Validate-config tests (li-tests/config_reject/routing_*.toml):

• two routes same priority + overlapping match → reject
• glob_rest on public listener without max_depth → reject
• path containing .. or unnormalized → reject

Property / golden tests:

• Normalize path: /v1//chat → /v1/chat (single algorithm, tested)
• prefix_strip: /api/v1/foo + strip /api → upstream path /v1/foo (golden vectors)

Bench (optional): micro-bench match_route 10k paths — guard perf regression, not correctness.

M1 gate: routing suite green + config_reject overlap cases + router in lic build.

**def validate(c: HttpdConfig) -> Result[unit, ConfigError]** with contracts:

• ensures no ambiguous overlap on same priority (validator rejects)
• ensures every StaticRoot path ⊆ allowed filesystem roots (declared in config)
• ensures every Proxy target ∈ c.upstreams allowlist
• ensures each upstream has 1 <= peers.len <= MaxPeers (e.g. 32)
• ensures peer URLs are literal http(s)://host:port — no request-derived host
• ensures c.limits.max_body <= MaxBodyCap (compile-time constant)

Invalid configs = proof obligations fail or validator returns error—never “warn and run.”

Secure defaults (user omits dangerous knobs)¶

[server]
listen = ":443"
host = "api.example.com"
tls = "lets_encrypt"
email = "ops@example.com"

[limits]
max_body = "1m"

[upstreams.api]
peers = ["http://127.0.0.1:3000", "http://127.0.0.1:3001"]

[routes]
"GET  /health"     = "static:healthcheck"
"POST /v1/*"       = "proxy:api"

• User cannot raise limits above schema ceiling (only tighten)
• Public bind without TLS → validation error (unless valid server.tls mode configured)
• proxy = "http://evil.com" → unknown upstream id error
• Upstream with zero peers or > MaxPeers → validation error
• weight outside 1..100 or sum over cap → validation error

Automatic TLS certificates (setup-time, config-driven)¶

On first start (or li-httpd setup-tls), provision certs before binding public :443 — no manual openssl steps for the default path.

Three modes (enum — user picks one per listener):

[server]
listen = "0.0.0.0:443"

[server.tls]
mode = "lets_encrypt"              # manual | self_signed | lets_encrypt
min_protocol = "1.3"
cert_dir = "/var/lib/li-httpd/certs"   # created 0700 on setup; paths in config

# --- mode: manual ---
# [server.tls.manual]
# cert = "/etc/li-httpd/fullchain.pem"
# key  = "/etc/li-httpd/privkey.pem"

# --- mode: self_signed (dev) ---
# [server.tls.self_signed]
# dev = true                         # required for non-loopback bind
# valid_days = 90                    # schema max 365

# --- mode: Let's Encrypt ---
[server.tls.lets_encrypt]
email = "ops@example.com"            # required; ACME account contact
domains = ["api.example.com"]        # must match a route host
environment = "production"           # staging | production
renew_before = "30d"                 # renew when <30d left
http01_bind = "0.0.0.0:80"           # challenge listener (or share :80 vhost)

Setup flow:

flowchart TD
  start[li-httpd start or setup-tls]
  validate[lic validate-config]
  mode{tls.mode}
  manual[Load manual cert/key]
  selfsign[Generate self-signed ED25519/RSA]
  acme[ACME client: account + order]
  http01[Serve HTTP-01 challenge]
  write[Write cert_dir fullchain + privkey]
  listen[Bind TLS listener]
  start --> validate
  validate --> mode
  mode -->|manual| manual --> listen
  mode -->|self_signed| selfsign --> write --> listen
  mode -->|lets_encrypt| acme --> http01 --> write --> listen

1. **li-httpd setup-tls** — only TLS provisioning + exit (good for CI/images)
2. **li-httpd setup-censor** — read migrations/OpenAPI → leak_censor.generated.toml (see leak censorship section)
3. **li-httpd setup** — interactive/full: TLS + censor + default config paths (recommended first install)
4. **li-httpd normal start** — if cert_dir missing certs and mode is self_signed or lets_encrypt, run setup then listen
5. Background renew (Let's Encrypt): timer per renew_before; reload TLS context atomically (no drop active streams mid-charge if possible — document graceful)

Let's Encrypt assistance (built-in, not “install certbot”):

• Integrated ACME v2 client (std/tls/acme.li + thin trusted HTTP to Let's Encrypt directory)
• HTTP-01 challenge: auto route /.well-known/acme-challenge/ (cannot be overridden by user routes — reserved)
• Staging environment for tests (environment = "staging")
• Clear errors: dns not pointing to this host, port 80 blocked, rate limited
• Optional later: TLS-ALPN-01 (M2+) if :443 up before :80

Self-signed auto-generate:

• Generate on first run; store under cert_dir
• Log fingerprint + one-line trust hint for dev
• Browser/agent clients: document tls.dev_skip_verify for local SDKs only — never a production config flag

Validation rules (HttpdConfig.validate):

• lets_encrypt → every domain ∈ domains appears on at least one [[route]].host
• lets_encrypt on public listener → email present and valid format
• self_signed + public bind → error unless tls.self_signed.dev = true
• manual → cert/key readable, not expired at startup (warn if < renew_before)
• Forbidden: mode = "off" on 0.0.0.0

Proof / trust boundary:

• Cert parsing + TLS handshake: Li crypto / std/tls (M2)
• ACME signing (account key, JWS): v1 in trusted extern with contracts on URL and nonce handling; migrate to Li as crypto matures
• File write: only under cert_dir; ensures paths ⊆ cert_dir

Bench / tests:

• li-tests/tls_setup/ — staging ACME with pebble or LE staging
• config_reject/tls_public_self_signed.toml — must fail validate
• Exploit: cannot request cert for domain not in config

Milestone: self_signed + manual in M1.5 with TLS terminate; Let's Encrypt obtain + renew in M1.5 (agent public APIs need real certs) or early M2 if ACME LOC is tight.

Load balancing (M1 core)¶

Minimal L7 balancer inside reverse proxy—no separate binary, no nginx upstream {} grammar clone.

In scope (M1)¶

Secure-by-design LB rules¶

• Peer list fixed at validate — request headers/cookies never select backend
• balance is enum in TOML — no custom Lua/hash from user string
• Active health GET /path (M1.5): probe URL must be relative on peer base URL only; interval/fail bounds in schema
• Connection limits per peer optional (max_conns) — schema max to prevent DoS misconfig

Proved core (std/http/upstream.li)¶

def pick_peer(pool: var UpstreamPool, ctx: RequestCtx) -> Result[PeerId, UpstreamError]
  requires pool.peers.len > 0
  requires pool.active.len > 0
  ensures result.ok -> pool.peer_active(result.value)
  decreases pool.retry_budget

reload re-validates full config before swapping pools (no half-applied upstream).

Bench / exploit¶

Nginx oracle: same bench.toml topology against nginx upstream block for RPS/latency row.

Out of scope until RFC + LOC¶

ip_hash, consistent hash, random two, gRPC LB, slow-start, backup tier, zone shared memory across workers (M1: per-worker pools OK for v1; document stickiness limitation).

AI / agent-native gateway (product direction)¶

li-httpd is the edge in front of models and tools — not a human-facing website server. Design every feature for: long requests, streaming bodies, many parallel agents, observability, and policy at the edge (headers, auth, limits).

flowchart LR
  agent[Agent client]
  gateway[li-httpd]
  policy[Headers plus rate limit]
  lb[Upstream pool]
  infer[Inference / tool backends]
  agent --> gateway
  gateway --> policy
  policy --> lb
  lb --> infer

Approach: header controls (secure by design)¶

Three explicit phases — no “pass all headers” default:

Rules (non-negotiable):

• Policies are per-route in TOML — enums and literal sets, not regex strings from users
• Clients cannot set x-upstream-, x-route-, or hop-by-hop headers — rejected at parse or dropped before upstream
• inject values are LiteralString in config — no $variable substitution (prevents header injection via config)
• Hop-by-hop / connection headers handled only by gateway — never forwarded blindly

[[route]]
host = "api.example.com"
path = "/v1/"
proxy = "inference_pool"

[route.headers.ingress]
allow = ["authorization", "content-type", "accept", "traceparent", "x-request-id", "x-agent-id", "x-model", "idempotency-key"]

[route.headers.egress]
allow = ["content-type", "traceparent", "x-request-id", "x-model"]
inject = { "via" = "li-httpd/1" }   # literals only

[route.headers.response]
allow = ["content-type", "cache-control", "retry-after", "x-request-id"]

Proof hook: forward_ingress(h, policy) -> Headers with ensures every outgoing name ∈ policy.egress.allow`.

Agent-native: treat traceparent / x-request-id as required on inference routes (config require = ["traceparent"]) — validate fails at request time with 400, not silent drop.

Runtime leak censorship (optional — user can turn off)¶

Yes, partially. Upstream frameworks can leak secrets; li-httpd can censor egress when enabled. Censorship is opt-in per deployment (enabled = false is valid); production profile may warn but does not hard-require it (unlike rate limits on public routes).

Best setup path: during li-httpd setup, read the DB schema the user already defined via migrations and generate deny_paths + sensitive field hints — user reviews, edits, or disables censorship entirely.

flowchart TB
  mig[db/migrations applied SQL or JSON Schema]
  setup[li-httpd setup-censor]
  catalog[SchemaCatalog sensitive columns]
  gen[leak_censor.generated.toml]
  main[li-httpd.toml merge]
  runtime[leak_censor if enabled]
  mig --> setup
  setup --> catalog
  catalog --> gen
  gen --> main
  main --> runtime

flowchart LR
  upstream[Upstream response]
  hdr[Header allowlist]
  body[Body scrubber if enabled]
  client[Client]
  upstream --> hdr
  hdr --> body
  body --> client

Easy TOML — global off switch + per-route override:

# Global default — user may disable censorship entirely
[leak_censor]
enabled = false                 # true = scrub on routes that do not override

[route.leak_censor]
enabled = true                  # overrides global for this route only
on_detect = "redact"            # redact | block_502 | abort_stream
max_scrub_bytes = "4m"

[route.leak_censor.headers]
deny_names = ["x-api-key", "x-debug-stack"]

[route.leak_censor.json]
deny_paths = ["$.api_key", "$.secret"]   # often auto-filled by setup-censor
include_generated = true               # merge leak_censor.generated.toml

[route.leak_censor.patterns]
allow = ["openai_sk", "pem_private", "jwt_bearer"]   # enum IDs only

Detectors are built-in enums in packages/li-http/leak_detect.li — not user regex.

li-httpd setup-censor — schema from migrations (server setup)¶

Runs as part of li-httpd setup (with setup-tls) or standalone after the user has applied DB migrations.

li-httpd setup-censor \
  --migrations ./db/migrations \
  --dialect postgres \
  --openapi ./api/openapi.yaml    # optional: response field paths

Inputs (v1):

Output: leak_censor.generated.toml (checked in or gitignored per team policy):

# generated by li-httpd setup-censor @ 2026-05-16T12:00:00Z
# source: db/migrations/003_api_keys.sql
[generated.json_paths]
paths = [
  "$.api_keys[*].token",
  "$.users[*].password_hash",
  "$.settings.secret_value",
]

[generated.headers]
deny_names = ["x-internal-api-key"]

Merge at validate-config: deny_paths = user_paths ∪ generated_paths when include_generated = true. explain-config prints merged censor policy.

SQL migration convention (documented):

-- li:censor
ALTER TABLE api_keys ADD COLUMN token TEXT NOT NULL;

Explicit marker always generates $.api_keys[*].token (and table-qualified variants).

Package: packages/li-schema/ — parse SQL (subset), build SchemaCatalog, map column → JSONPath heuristics (snake_case → $.snake_case, nested users.password → $.users[*].password).

Proof: when enabled = false, censor procs are not invoked (ensures bypass_censor → out = forward_raw disallowed for headers-only path — header allowlist still runs). When enabled, same obligations as before.

Proof + probability story:

• Deterministic: header allowlist, JSON path denylist, bounded buffer, no forward until scrub pass completes on chunk (or redact in place within cap).
• **prob_ensures:** for configured detector set D, bound false-negative rate on corpus C in CI: P(leak in C reaches client) < ε via Monte Carlo + golden leak fixtures.
• Tier G exploits (exploits/leak_*.toml): run with leak_censor.enabled = true in server config — expect redact or 502; separate row censor_disabled.toml confirms passthrough when user turned censorship off (documented insecure mode).

What censorship cannot guarantee (honest limits):

Recommended (not forced): enable censorship on public proxy:* routes after setup-censor; validate-config prints hint if global and route both disabled on public listeners.

vs nginx: nginx has no schema-driven scrub; li-httpd generates policy from your migrations at setup time.

Packages: packages/li-http/leak_censor.li, leak_detect.li, packages/li-schema/ (migration parser); tests li-tests/leak_censor/, li-tests/schema_catalog/, benchmarks/tier5_http/exploits/leak_*.toml.

CLI: li-httpd setup orchestrates setup-tls → setup-censor → write default li-httpd.toml stub with # include generated censor file.

Logging engine (packages/li-log) — we build it¶

No third-party log libraries (no spdlog, zap, winston). li-log is a publishable package with secure defaults; li-httpd depends on it for every line emitted.

flowchart LR
  httpd[li-httpd workers]
  redact[redact_log from li-log]
  sinks[Sinks]
  access[access.log rotated]
  error[error.log rotated]
  audit[audit.jsonl rotated]
  stderr[stderr human]
  httpd --> redact
  redact --> sinks
  sinks --> access
  sinks --> error
  sinks --> audit
  sinks --> stderr

Defaults (best practices — zero config beyond path)¶

Easy TOML¶

[log]
# omitted = all defaults below apply
dir = "/var/log/li-httpd"
level = "info"              # trace | debug | info | warn | error
format = "human"            # human | json — per-sink override allowed

[log.access]
path = "access.log"         # under dir; rotated automatically
format = "human"

[log.error]
path = "error.log"
level = "warn"

[log.audit]
path = "audit.jsonl"
format = "json"
enabled = true              # required on public listeners (validate-config)

[log.rotation]
max_size = "100m"
max_age = "7d"
max_backups = 10
compress = true

[log.redact]
headers = ["authorization", "cookie", "x-api-key"]
patterns = ["openai_sk", "jwt_bearer", "pem_private"]   # same enum IDs as leak_censor

Desugar: if [log] absent → use defaults with dir = "./logs" for dev profile.

API (proved core)¶

type LogLevel = enum trace, debug, info, warn, error

def log_access(e: AccessEvent) raises Log
  ensures e.authorization == Redacted or e.authorization == Absent

def log_audit(e: AuditEvent) raises Log
  ensures ∀ k ∈ e.fields, k ∉ SecretFieldNames

def redact_log(msg: string) -> string
  ensures no SecretPattern in result

• Effect **raises Log** — separate from IO/Net; only li-log performs file I/O (thin extern write/rotate in li_rt_log.c if needed).
• Hot reload: SIGUSR1 reopens log files (rotation-safe) — same pattern as nginx reopen.

Channels (li-httpd wiring)¶

Prometheus stays a metrics endpoint, not a log backend — but histograms use the same request_id / route labels as audit JSONL.

Tests + exploits¶

• li-tests/log/ — rotation creates access.log.1.gz, timestamp format golden, redaction golden
• li-tests/log/exploits/ — log line must not contain injected sk-... from upstream response
• Tier G extension: leak_logged_secret.toml — upstream leak → censored on wire and absent from audit.jsonl

Docs¶

• docs/superpowers/specs/li-log.md — sinks, rotation, redaction contract
• PUBLISH.md in packages/li-log/ — reusable by non-httpd binaries later

Approach: rate limiting (agent workloads)¶

Agents generate few connections, long streams, bursty JSON — limits differ from CDN/static traffic.

Key selection (enum, not free string):

• api_key — from Authorization: Bearer (hash at edge, never log raw)
• agent_id — from allowlisted x-agent-id
• ip — optional for internal routes only (config must say allow_ip_key = true)

Secure by design:

• Public routes: must define [route.rate_limit] — validator error if missing
• User cannot set requests_per_sec = unlimited — schema max + default below nginx-equivalent abuse threshold
• On deny: 429 + Retry-After (proved header present) + structured log (no body leak)

[route.rate_limit]
key = "api_key"
requests_per_sec = 60
burst = 30
concurrent_streams = 100
stream_max_duration = "600s"
stream_idle_timeout = "120s"

Implementation: token bucket per key in shared memory (per-worker v1; document sharding in M2). Proved: check_rate returns within bounded time; decreases on window bookkeeping.

Bench: rate_limit_429, stream_cap_exceeded, sse_long_stream scenarios in tier5_http.

Streaming (M1.5 — core agent path)¶

Not in v1: bidirectional gRPC streaming (M3/RFC); use HTTP + WS for tools in M2.

Model / agent routing (M1.5)¶

Route to different upstream pools without user-controlled URLs:

[[route.match]]
header = "x-model"
value = "gpt-4"
proxy = "pool_gpt4"

[[route.match]]
header = "x-model"
value = "claude-3"
proxy = "pool_claude"

• value must be enum/literal in config — not regex from operator
• Unknown model → 404 with safe JSON body (no upstream leak)

Optional: path prefix /v1/models/{model}/ with same literal map.

Other agent-native features (phased)¶

Community research — what operators ask for (Reddit-adjacent)¶

Note: Reddit search/API returned 403 in this environment; synthesis uses the same communities (r/LocalLLaMA, r/selfhosted, r/devops patterns) via HN, GitHub wishlists, and Ollama/nginx operator guides that quote those pain points.

Mapped to li-httpd (prioritized backlog):

Config sketch (community-driven additions):

[server.api]
openai_compatible = true
base_path = "/v1"

[route.fallback]
chain = ["pool_gpt4", "pool_claude", "pool_local"]

[route.cache]
enabled = true
ttl = "5m"
key = ["model", "api_key"]   # never user-supplied body fields alone

[route.queue]
max_wait = "30s"
max_depth = 100              # when peers not ready

Reddit follow-up (manual): periodically search r/LocalLLaMA, r/selfhosted, r/MachineLearning for ollama proxy, litellm, vllm production, openai compatible gateway — append to docs/research/community-backlog.md (living doc).

Explicit non-goals (agent edition): HTML caching, if/rewrite, browser-oriented optimizations, arbitrary third-party modules, full LiteLLM feature parity.

Milestone map (agent-native)¶

LOC: agent features live in std/http/agent/ — still count toward cap; drop static-file polish before dropping stream limits.

What Li must gain (language + compiler + semantics)¶

1. Finish pillar 1 for real (blocker for everything)¶

Before any “ultra secure” claim ships:

• 2e: VC generation from requires/ensures/invariant/decreases
• 2f: lic build invokes Lean 4 kernel; cache by VC hash
• MIR: proved bounds on dynamic indices (today: partial — see architecture overview)
• **li-tests:** expand verify_ok / verify_fail beyond skeleton (contracts_verify)

Without this, a webserver is “memory-safe-ish C++ via LLVM,” not Li’s thesis.

2. Systems type + memory model for wire protocols¶

From the design spec:

• **bytes / bytearray / memoryview[T] / stringview** with linear ownership for parse buffers
• **ringbuffer[N, T]** (already on roadmap) for socket read paths without per-read Alloc
• Refinement types for protocol limits: e.g. HeaderName = {s: stringview | len(s) <= 256}, BodyLen = {n: u64 | n <= max_body}
• **Reader / Writer protocols** (PEP 3.14 direction) for incremental parse
• **checked int / wrapping int** for length arithmetic in parsers (forbid silent overflow)

3. Effects and IO model¶

Extend effects beyond raises IO / raises Alloc:

Rule: user handlers prove against abstract Net/Async in Lean; implementations live in trusted runtime + thin extern only where unavoidable.

4. Concurrency (small surface)¶

• Workers = cores; one async event loop per worker — no thread pool until benchmarks require it
• epoll/kqueue for M1 only
• parallel for not used on the connection path

Prove:

• No cross-worker mutable aliasing without Sync
• Connection state machine transitions are total (decreases on state depth)
• Timeouts and body draining always advance or close (no stuck connections)

5. Async runtime (language + std)¶

Ship:

• async proc / await lowering to state machines (MIR)
• Timer wheel, cancellation, backpressure
• Integration with reactor: readiness → resume tasks

Benchmark gate: see Nginx benchmark harness below — correctness and config parity before any published RPS numbers.

6. No dynamic modules (LOC + security)¶

Extensibility = edit li-httpd.toml and redeploy, or fork li-httpd. No .so plugins in M1–M2.

Stdlib and libraries to build (new std/net, std/http, std/tls, std/crypto)¶

Layer 0 — OS interface (trusted, minimal)¶

Expand trusted.lean only with:

• File descriptors as opaque Fd
• read/write/recv/send/poll/epoll_wait as axioms with contracts (bytes written ≤ buffer len, no phantom FDs)
• Not the whole HTTP stack

Prefer one audited syscall shim in C (li_rt_net.c) called from Li via extern proc with full contracts — keeps kernel ABI in one place.

Layer 1 — TCP/UDP + DNS¶

• TcpListener, TcpStream, UdpSocket
• Non-blocking mode + edge/level triggered readiness
• DNS resolver (async; bounded cache; proved cache size)

Layer 2 — HTTP/1.1 (first shipping milestone)¶

Proved components:

• Request-line + header parser (state machine + invariant on cursor ≤ buffer.len)
• Chunked encoding (proved termination via decreases on remaining chunk bytes)
• Response serializer
• Connection lifecycle (keep-alive limits)

Security properties to prove (examples):

• No read past buffer end
• Total header bytes ≤ max_header_bytes ⇒ reject before Alloc
• Body read loops terminate or return 413/408
• No unbounded header continuation without decreases

Fuzz + differential tests against nginx/httpbin (outside Lean, CI).

Layer 3 — Reverse proxy + stream¶

• Upstream selection, health checks (state machines with contracts)
• Full-duplex TCP proxy (stream module analog)
• WebSocket upgrade (proved handshake state machine)

Layer 4 — HTTP/2 + compression¶

• HPACK (dynamic table bounds proved)
• Huffman (constant stack or bounded heap)
• gzip/brotli: start as optional modules; compression bombs mitigated by proved output size caps

Layer 5 — HTTP/3 / QUIC (nginx 1.25+ territory)¶

Largest sub-project: QUIC state machine, loss recovery, TLS 1.3 integration. Plan as separate program once HTTP/2 + Li TLS stable.

Pure Li crypto (your choice) — architecture¶

Functional correctness (Lean): algorithm specs (AES-GCM, ChaCha20-Poly1305, X25519, ECDSA, RSA-PSS, SHA-2/3) match reference vectors.

Side-channel resistance (partially axiomatic): full timing proofs are research-grade; pragmatic approach:

1. **packages/li-crypto** — implementations in Li with:
2. requires/ensures on lengths and key sizes
3. No secret-dependent branches / indices enforced by checker + lint where possible
4. **trusted.lean axioms** only for syscall/RNG seam; constant-time may be axiomatic per primitive until measured
5. Roadmap: v1 ship Li-written ChaCha20-Poly1305 + X25519 + TLS 1.3 in li-crypto / li-tls; optional later **packages/li-crypto-hacl* (proved extern to HACL/Fiat) — you publish separately, not a dev blocker

TLS stack in Li:

TLS = record_layer + handshake_state_machine + cert_parser(X.509 subset) + LiCrypto

Prove: handshake states only advance on valid messages; transcript hash matches; no buffer overflow on cert chains (depth/size limits as refinements).

Reality check: “Pure Li crypto” for production TLS still needs audited constant-time and platform RNG (getrandom) in trusted base — document in RFC.

Randomness: deterministic proofs + probabilistic contracts + OS uniformity¶

Randomness is in scope end-to-end: deterministic Prng proofs, probabilistic prob_ensures (Monte Carlo + Lean measure theory), an explicit uniform OsRng contract for getrandom, and configurable Prng for TLS (lab vs production profiles). Simulation and Tier F exploits are how we validate probabilistic claims at runtime—not a substitute for specs, but part of the certificate story.

flowchart TB
  subgraph det [Deterministic — Lean kernel]
    Prng[Prng proofs]
  end
  subgraph prob [Probabilistic — in scope]
    ProbEnsures[prob_ensures P less than epsilon]
    MC[Monte Carlo lic build --prob-check]
    Measure[Mathlib measure lemmas]
    ProbEnsures --> MC
    ProbEnsures --> Measure
  end
  subgraph os [OS contract]
    Uniform[OsRngUniform axiom on getrandom]
    Evidence[PractRand + Tier F nightly]
    Uniform --> Evidence
  end
  Prng --> TLS
  Uniform --> Csprng[Csprng]
  Csprng --> TLS[TLS secrets]
  Prng --> TLS
  MC --> TLS
  Evidence --> Uniform

Concept A — Prng (deterministic, fully provable)¶

For benchmarks, tests, load-balancer tie-breaks, fuzz schedules, and any “random” that must replay:

Aligns with existing bench rule: deterministic seeds in params.toml (benchmarks plan).

Concept B — Csprng + raises Rng + uniform OS contract¶

For TLS key shares, IVs, session tickets, ACME account keys (default source):

-- trusted.lean — explicit RNG contract (RFC-reviewed, still minimal)
axiom rng_fill_bytes : (n : Nat) → IO (Vector UInt8 n)

/-- OS CSPRNG: i.i.d. uniform bytes. Evidence obligations in CI, not sorries. -/
axiom OsRngUniform :
  ∀ n (k : Vector UInt8 n),
    Pₒₛ(output = k) = (1 / 256) ^ n

User modules prove implications from OsRngUniform; they do not re-prove physics of /dev/urandom. Wrong axiom + passing Tier F = spec bug (same class as wrong ensures).

Default production: [server.rng] mode = "os". **Prng for TLS is allowed** when explicitly configured (see Concept D + config profiles)—not banned by the typechecker.

Concept C — RngSource trait + simulation (testing without lying to Lean)¶

Simulation technique: parametrize crypto-adjacent code over an **RngSource** interface; prove against the interface; swap implementation at link time or via test-only module.

type RngSource = object
  VTable  # fill_bytes, maybe label for logs

def tls_generate_iv(src: RngSource, ...) -> bytes
  requires ...
  ensures result.len == IV_LEN
  # deterministic ensures + prob_ensures on collision given OsRngUniform or PrngSeed

Concept D — Probabilistic Hoare (prob_ensures) — in scope¶

Li extends contracts with probability bounds, discharged by Lean (measure theory) and/or Monte Carlo evidence at build time.

def issue_iv(r: RngSource, key_id: uint64) -> bytes
  requires ...
  ensures result.len == IV_LEN
  prob_ensures collision_iv(key_id, result) < 1e-12
    given OsRngUniform
    samples 100_000   # Monte Carlo trials for lic build --prob-check

Monte Carlo is not “instead of proof”: for finite combinatorial events (IV collision in N draws, duplicate session id in N handshakes), MC estimates P with a reported confidence interval attached to the build log. For structural implications (OsRngUniform → prob_ensures), Lean proves the implication; MC validates the axiom’s empirical plausibility on the shipped binary.

Tier F + probabilistic: exploits with BadRng must violate prob_ensures predictions (handshake abort rate, collision rate) — ties runtime attacks to probabilistic specs.

Concept E — Config: Prng on TLS allowed (profile-gated)¶

[server.rng]
mode = "prng"       # os | prng | sim | bad (bad = exploit harness only)
seed = 42

Typed config records RngMode enum; no effect lint ban on Prng feeding TLS—policy is validate-config + ship profile, not compiler rejection.

**li-tests/rng/:**

• Golden vectors: seed → N outputs (xoshiro / ChaCha20 DRBG vectors)
• Replay: SimRng schedules
• **li-tests/prob/:** MC estimators, CI for prob_ensures discharge helpers
• PractRand / SP 800-22: evidence for OsRngUniform axiom — failure blocks release (M1.5+)

HTTP / li-httpd usage¶

RNG exploit testing (mandatory — Tier F)¶

Proofs do not replace runtime checks that the trusted RNG seam and TLS code behave under adversarial entropy. Every RNG-related invariant gets a Tier F row in nginx_mitigations.toml and a matching exploits/rng_*.toml.

Injection (li-httpd only): harness sets server RNG from TOML — nginx/OpenSSL cannot use BadRng; compare nginx on behavioral rows only where injection is N/A.

# scenarios/tls_handshake/bench.toml (or exploit-only overlay)
[server.rng]
mode = "bad"              # os | sim | bad | prng
bad_pattern = "constant"  # constant | repeat | short_cycle | partial_fill
bad_seed = 0
sim_schedule_file = "fixtures/rng_low_entropy.bin"   # when mode = sim

exploit_http.py merges [server.rng] into li-httpd env / config before [attack]; restarts server per exploit.

flowchart LR
  toml[exploits/rng_*.toml]
  harness[exploit_http.py]
  li[li-httpd + BadRng or SimRng]
  observe[TLS client + session capture]
  csv[exploit_report.csv]
  toml --> harness
  harness --> li
  harness --> observe
  observe --> csv

Tier F exploit files (benchmarks/tier5_http/exploits/):

Example exploit TOML:

id = "rng_repeat_iv"
tier = "F"
enabled = true
refs = ["CWE-330", "CWE-338"]

[nginx_src]
mitigation_id = "tls_record_iv_unique"
notes = "OpenSSL RAND_bytes — oracle behavior only; no BadRng inject"
li_invariant = "TLS record layer never emits two AEAD records with same (key, IV)"

[targets]
langs = ["li"]                # primary; optional nginx row = behavioral baseline
server_config = "../scenarios/tls_handshake/bench.toml"

[server.rng]
mode = "bad"
bad_pattern = "repeat"
bad_seed = 42

[attack]
driver = "python"
script = "drivers/tls_many_handshakes.py"
handshakes = 200
capture = ["session_id", "first_record_iv"]

[expect]
no_crash = true
no_duplicate_aead_iv = true
tls_handshake_fails_or_all_closed = true
legitimate_client_ok = false      # intentional — only attack traffic

[report]
severity = "critical"
pass_message = "predictable IV did not produce valid duplicate records"

**li-tests/rng/exploits/** (fast, no full server): unit-level BadRng into li-rng and li-tls record layer; lic build + run_rng_exploits.sh in PR when packages/li-rng/** changes.

**nginx_mitigations.toml rows** (examples):

[[mitigation]]
id = "tls_record_iv_unique"
cve = []
li_invariant = "AEAD IV unique per record under fixed key"
exploit = "exploits/rng_repeat_iv.toml"

[[mitigation]]
id = "rng_no_partial_read"
cve = []
li_invariant = "fill_bytes errors if fewer than requested bytes"
exploit = "exploits/rng_partial_fill.toml"

[[mitigation]]
id = "config_prng_tls_production_gate"
cve = []
li_invariant = "HttpdConfig rejects mode=prng for TLS on production profile unless allow_insecure_rng"
exploit = "exploits/rng_prng_on_tls_prod.toml"

[[mitigation]]
id = "prob_iv_collision_bound"
cve = []
li_invariant = "prob_ensures iv_collision < epsilon given OsRngUniform"
exploit = "exploits/rng_repeat_iv.toml"

CI:

Pass criteria (RNG-specific): same as global exploit policy — crash/ASan/RSS + **[expect] booleans** on crypto outcomes. Failing Tier F with OsCsprng in nightly = release blocker for M1.5+.

Docs: extend docs/security-http-exploits.md with Tier F table + ethics (lab-only BadRng).

Packages + docs (when executing)¶

• packages/li-rng/ — prng.li, rng_source.li, sim_rng.li, prng_rng.li, os_csprng.li
• packages/li-prob/ — MC estimators, prob_ensures discharge helpers, Lean lemma exports
• docs/superpowers/specs/li-rng.md — OsRngUniform, prob_ensures, evidence pipeline
• docs/superpowers/specs/li-probabilistic-contracts.md — syntax, MC confidence, Mathlib obligations
• docs/semantics/trusted.lean — rng_fill_bytes, **OsRngUniform** (explicit axiom + evidence duties)
• li-tests/rng/ — vectors, replay, production profile rejects prng without flag
• li-tests/prob/ — MC regression for shipped ε bounds
• li-tests/rng/exploits/ — unit BadRng/SimRng (fast PR gate)
• benchmarks/tier5_http/exploits/rng_*.toml — Tier F integration exploits
• benchmarks/tier5_http/harness/drivers/tls_many_handshakes.py — capture IVs/session ids
• P0 RFC: trusted surface budget includes RNG lines + forbidden axioms list

Compiler work (P0 → P2)¶

• P0: raises Rng effect tracking; only li-rng calls extern fill
• P1: parse prob_ensures, given OsRngUniform / given PrngSeed(s); emit VC to Lean + MC metadata
• P2: lic build --prob-check runs MC, attaches confidence to build certificate
• Config: no compile-time ban on Prng → TLS; validate-config enforces profile policy
• lic build --test-rng=sim for test targets (harness)

Security model: proofs first, exploits second¶

Li’s edge: security = what compiles (plus a tiny trusted base). nginx’s edge: maturity and features. li-httpd trades features for certified core.

M1 ship gate: lic build + lic validate-config on all shipped examples + config_reject + exploit A+B + LOC + bench + **li-log access/error with rotation smoke test**.

M1.5 ship gate: above + exploit Tier F (RNG) + Tier G with censorship enabled in test config + setup-censor golden; TLS scenarios enabled.

Honesty: wrong ensures → wrong theorem. Exploits + nginx audit catch that; Lean catches memory, bounds, and totality in user code.

Milestones (not nginx port phases)¶

Drop features from M1 before raising LOC cap.

Nginx benchmark harness (TOML-configurable, correctness-first)¶

Extend the existing benchmarks harness pattern — same CSV schema, same “verify before timing” rule as benchmarks plan.

Design principle: users never edit Python to add a scenario — only TOML. bench_http.py merges config layers, starts servers, runs load tools, writes CSV.

Layout¶

benchmarks/
  tier5_http/
    defaults.toml          # global: workers, warmup, ports, binary paths, load defaults
    suite.toml             # profiles (ci, nightly, baseline) + enable/disable scenarios
    fixtures/              # static files, certs (sizes from [fixtures] in defaults.toml)
    scenarios/
      static_small/bench.toml
      static_large/bench.toml
      proxy_loopback/bench.toml
      ...
    templates/
      nginx.conf.in        # rendered from bench.toml [server] (keeps nginx in sync)
  harness/
    bench_http.py          # reads TOML only
    verify_http.py         # reads [verify] from merged bench.toml
    plot_http.py
    params_schema.toml     # documented keys for tier5_http

lang column values: nginx, li (nginx is the reference impl).

CLI (easy local use)¶

./benchmarks/harness/bench_http.py                          # default profile in suite.toml
./benchmarks/harness/bench_http.py static_small             # one scenario
./benchmarks/harness/bench_http.py --profile ci             # verify only, no timing
./benchmarks/harness/bench_http.py --profile baseline     # nginx-only baselines
./benchmarks/harness/bench_http.py static_small --set load.connections=500
./benchmarks/harness/bench_http.py static_small --render-nginx-only

TOML layers (three files + optional sweep)¶

1. defaults.toml — machine-wide defaults:

[global]
workers = "auto"
port_base = 18080
warmup_sec = 30
measured_runs = 5

[servers.nginx]
binary = "nginx"

[servers.li]
binary = "../../../build/examples/li-httpd/li-httpd"

[load.wrk]
threads = 8
connections = 200
duration_sec = 30
pipeline = 1

2. suite.toml — what runs (toggle without touching scenarios):

[profiles.ci]
scenarios = ["static_small"]
timing = false

[profiles.baseline]
scenarios = ["static_small", "static_large"]
timing = true
langs = ["nginx"]

[default]
include = ["static_small", "static_large"]
exclude = ["h2_static"]

3. scenarios/<name>/bench.toml — self-contained scenario:

name = "static_small"
phase = "w2"
enabled = true

[server]
kind = "static"
document_root = "../../fixtures/static/1k"
sendfile = true

[verify]
requests = [
  { method = "GET", path = "/file.bin", expect_status = 200, body_sha256 = "..." },
]

[load]
tool = "wrk"
threads = 8
connections = 200

[[load.sweep]]
connections = [50, 200, 1000]
variant_prefix = "c"

[metrics]
collect = ["rps", "p50_latency_ms", "p99_latency_ms"]

li-httpd reads [server], [proxy], [tls] from the same bench.toml. Nginx gets a generated .conf from templates/nginx.conf.in + merged TOML (no hand-duplicated nginx.conf per scenario).

Merge order: defaults.toml ← scenarios/*/bench.toml ← --set key=value overrides.

Add a benchmark in 2 minutes¶

1. cp -r scenarios/static_small scenarios/my_bench and edit bench.toml
2. Add "my_bench" to suite.toml [default].include
3. ./benchmarks/harness/bench_http.py my_bench

Fairness rules (non-negotiable for published numbers)¶

Label rows when parity is incomplete (e.g. variant=no_sendfile, variant=li_crypto_v0) — never compare unfair configs without explicit variant.

Starter scenarios (each = scenarios/<name>/bench.toml)¶

Fixture sizes declared in defaults.toml [fixtures]; harness generates files before verify.

CSV schema (reuse existing)¶

Same columns as bench.py: benchmark, lang, variant, threads, metric, value, unit, git_sha, cpu_model, flags.

Example rows:

• static_small, nginx, sendfile_on, 8, rps, 125000, req/s, ...
• static_small, li, sendfile_on, 8, rps, 98000, req/s, ...
• static_small, li, sendfile_on, 8, p99_latency, 4.2, ms, ...

Add optional verify.csv pass/fail per scenario (mirror verify.csv).

bench_http.py flow¶

flowchart LR
  defaults[defaults.toml]
  suite[suite.toml]
  bench[scenarios/name/bench.toml]
  harness[bench_http.py]
  nginx[nginx rendered conf]
  lihttpd[li-httpd reads bench.toml]
  load[wrk or h2load]
  csv[results/latest.csv]
  defaults --> harness
  suite --> harness
  bench --> harness
  harness --> nginx
  harness --> lihttpd
  harness --> load
  load --> csv

1. Merge TOML; generate fixtures if missing.
2. For each lang in profile: start server → [verify] → if timing, [load] (+ sweeps) → CSV.
3. plot_http.py → benchmarks/results/share/http_*.png.

CI integration¶

• Tier 0 (no timing): verify_http.py only in PR CI — fast, no flakiness.
• Nightly: full bench_http.py on linux-x86_64 runner with perf governor; upload latest.csv artifact.
• Regression policy: investigate if li p99 > 2× nginx after M1; track LOC in same report.

Early spike (before li-httpd)¶

Land TOML + harness + nginx audit first (no li-httpd):

• defaults.toml, suite.toml, scenarios/static_small/bench.toml
• bench_http.py --profile baseline → nginx verify + timing → CSV
• benchmarks/tier5_http/README.md — copy-paste: install wrk, run one command

Docs to add¶

• docs/benchmarks-http.md — TOML key reference (links to params_schema.toml), fairness checklist, example bench.toml
• Extend .cursor/rules/benchmarks.mdc — all tier5_http config lives in TOML; do not hardcode scenarios in Python

Security via nginx source audit (+ exploit replay)¶

Read nginx source to build a checklist of invariants (what went wrong historically)—then implement those invariants in minimal Li code, not by translating C.

Replay exploits against stock nginx (baseline) and li-httpd. Li may fail closed stricter than nginx (e.g. always 400 on ambiguous Content-Length); document in exploit TOML [expect].li_behavior = "stricter".

Generic “hacker toolkit” fuzzing is secondary; every exploit file should cite where nginx mitigates (or where a CVE fixed it).

nginx_mitigations.toml (machine-readable audit)¶

[[mitigation]]
id = "duplicate_content_length"
cve = ["CVE-2019-20372"]
nginx_version_fixed = "1.17.7"
src = "src/http/ngx_http_parse.c"
symbol = "ngx_http_parse_header_line"
notes = "reject duplicate Content-Length"
exploit = "exploits/request_smuggling_cl_te.toml"
li_invariant = "single parser rejects duplicate Content-Length"
li_done = false

Generated/updated by audit_nginx_src.py:

• Scan third_party/nginx/CHANGES for Security: lines
• git log -S / blame on keywords (client_header_timeout, large_client_header_buffers, merge_slashes, …)
• Emit mitigation rows + stub exploits/<id>.toml if missing

Human review fills notes and li_invariant.

Key nginx source trees to audit (checklist)¶

Exploit harness layout¶

benchmarks/tier5_http/
  third_party/nginx/          # submodule
  nginx_mitigations.toml      # audit output (source of truth)
  suite_exploits.toml
  exploits/
    slowloris.toml
    slow_post_rudys.toml
    oversized_request_line.toml
    oversized_headers.toml
    chunked_encoding_abuse.toml
    request_smuggling_cl_te.toml
    request_smuggling_te_cl.toml
    path_traversal_encoded.toml
    host_header_poison.toml
    crlf_injection_headers.toml
    http_pipeline_desync.toml
    connection_flood.toml
    gzip_bomb.toml
    tls_invalid_handshake.toml
    tls_heartbleed_style_read.toml   # if custom TLS — probe overshoot reads
    h2_continuation_flood.toml       # M2
    hpack_table_bomb.toml            # M2
    proxy_ssrf_header.toml           # M1
    rng_constant_bytes.toml          # Tier F — BadRng inject
    rng_repeat_iv.toml
    rng_short_cycle.toml
    rng_partial_fill.toml
    rng_prng_on_tls_prod.toml
    rng_prng_on_tls_dev.toml
    rng_fork_duplicate.toml
    rng_session_id_predictable.toml
    rng_acme_key_reuse.toml
    rng_lb_deterministic.toml        # documentation / non-vuln
    leak_openai_key_in_sse.toml      # Tier G — upstream leaks sk- in stream
    leak_stack_trace_500.toml
    leak_json_nested_secret.toml
    leak_header_x_api_key.toml
    leak_logged_secret.toml          # Tier G — secret not in audit.jsonl
    censor_disabled_passthrough.toml # Tier G — global enabled=false, expect leak reaches client
    ...
  harness/
    exploit_http.py           # reads TOML only; merges [server.rng] for li-httpd
    drivers/tls_many_handshakes.py
  fixtures/
    rng_low_entropy.bin
li-tests/net_exploits/        # compile-fail / micro unit tests for parser rejects
li-tests/rng/exploits/        # unit BadRng into li-rng / record layer (PR-fast)

CLI¶

./benchmarks/harness/exploit_http.py                    # default profile
./benchmarks/harness/exploit_http.py slowloris
./benchmarks/harness/exploit_http.py --profile pr       # fast subset, <2 min
./benchmarks/harness/exploit_http.py --langs li         # only li-httpd
./benchmarks/harness/exploit_http.py --compare-nginx    # run same exploit vs nginx + li; diff [expect]

Exploit TOML schema (example)¶

id = "slowloris"
tier = "A"
enabled = true
refs = ["CAPEC-469"]

[nginx_src]
mitigation_id = "client_header_timeout"
src = "src/http/ngx_http_request.c"
config_keys = ["client_header_timeout", "client_body_timeout"]

[targets]
langs = ["nginx", "li"]       # always run nginx first — oracle
nginx_tag = "1.26.2"          # submodule pin
server_config = "../scenarios/static_small/bench.toml"

[attack]
driver = "python"             # python | raw_socket | h2_flood | tlsfuzzer | nuclei
script = "drivers/slowloris.py"
connections = 500
header_byte_interval_sec = 10
duration_sec = 60

[expect]
no_crash = true               # process exit 0 throughout
no_asan_error = true          # CI runs under -fsanitize=address
max_rss_mb = 512              # memory cap — detect leaks/exhaustion
responds_within_sec = 120     # no indefinite hang
legitimate_client_ok = true   # parallel GET /file.bin still returns 200
reject_or_close_attack = true # attack conns closed or 400, not queued forever

[report]
severity = "high"
pass_message = "limits and timeouts held"

Merge order: defaults.toml ← exploits/<id>.toml ← --set overrides (same as benchmarks).

Exploit tiers (map to W phases)¶

Tooling integration (referenced from TOML, not hardcoded)¶

Pin tool versions in defaults.toml [tools] for reproducible CI.

CI policy¶

Fail conditions: crash, ASan report, RSS above cap, legitimate client cannot connect, attack connections consume unbounded worker slots past bench.toml limits, duplicate AEAD IV / valid TLS on BadRng / uninitialized bytes after partial fill_bytes.

Pass ≠ “invulnerable”: pass means documented expectations in [expect] held. Update TOML when adding mitigations.

Pass criteria¶

1. nginx satisfies [expect] (documents real-world baseline).
2. li-httpd satisfies [expect] (or documented stricter variant).
3. li_invariant in nginx_mitigations.toml is implemented with matching requires/ensures.

results/exploit_report.csv: exploit_id, mitigation_id, lang, passed, li_invariant, git_sha, loc_httpd

Link audit → proofs¶

If Li proof passes but nginx-src audit shows a missing check → incomplete port, not “secure.”

Docs / tests to add¶

• docs/security-nginx-src-audit.md — how to run audit_nginx_src.py, read nginx_mitigations.toml, port checklist
• docs/security-http-exploits.md — exploit TOML + ethics (lab-only)
• li-tests/net_exploits/ — one-shot bytes copied from CVE advisories linked in mitigations table

Repository / docs to add (when execution starts)¶

• packages/ — workspace above; each subdir has li.toml, src/, PUBLISH.md, li-tests/ or re-exports tests from root
• packages/li-log/ — sinks, rotation, redaction, raises Log
• packages/li-schema/ — SQL migration + OpenAPI → SchemaCatalog for setup-censor
• packages/li-httpd/ — binary + CLI (not examples/ only)
• docs/superpowers/specs/li-log.md
• li-tests/log/ — rotation + redaction goldens
• docs/superpowers/specs/li-httpd.md — minimal architecture, LOC budget, threat model, li_invariant list, package dependency graph
• Compiler std/ may re-export from packages during bootstrap; long-term logic lives in publishable packages
• li-tests/net/ — parse limits, race fixtures, TLS vectors
• li-tests/net_exploits/ — malformed HTTP bytes
• li-tests/config_reject/ — TOML that must fail lic validate-config
• li-tests/routing/ — table-driven match_route cases + run_routing.sh
• li-tests/config_desugar/ — simple TOML → golden canonical
• std/http/desugar.toml — simple surface parser (Python or Li in harness)
• std/http/router.li — MatchExpr, match_route (proved)
• std/http/config.li — HttpdConfig, validate, secure defaults
• std/tls/acme.li, li-httpd setup-tls — ACME obtain/renew; reserved /.well-known/acme-challenge/
• li-tests/tls_setup/, config_reject/tls_*.toml
• benchmarks/tier5_http/third_party/nginx/ (submodule), nginx_mitigations.toml
• harness/audit_nginx_src.py, bench_http.py, exploit_http.py, …
• docs/security-nginx-src-audit.md
• docs/benchmarks-http.md
• docs/research/community-backlog.md — operator demand from Reddit/HN/GitHub (living)
• li-httpd reads scenario bench.toml [server] (typed config, no second format)

Critical risks (plan for them early)¶

1. Proof cost: HTTP/TLS specs explode VC size — need proof caching and lemma libraries in Mathlib.
2. Async + Lean: Totality on async loops needs careful decreases on logical steps, not OS callbacks.
3. Pure Li crypto vs LOC: small proved subset or thin extern at crypto boundary — pick smallest that passes M2 exploit tier.
4. Scope creep: every nginx feature request fights LOC budget — default no.
5. Compiler correctness: C++ lic is not meta-proved — server security still depends on codegen soundness (verification overview).
6. Package sprawl: too many packages/* before 2e–2f — start with li-net + li-http + li-httpd, split crypto/TLS when M1.5 needs them.
7. Probabilistic VC cost: prob_ensures + MC can be slow — cache by (proc_hash, ε, samples); cap samples in PR CI.
8. OsRngUniform honesty: axiom can be wrong on broken OS — PractRand + Tier F are mandatory evidence, not optional docs.

Recommended immediate next steps (before writing server code)¶

1. Land 2e–2f so “secure” is provable, not aspirational.
2. RFC: li-rng — Prng (proved) vs Csprng/raises Rng (trusted); SimRng for replay tests; see Randomness section above.
3. Spec std/bytes + HTTP parser contracts as first li-tests/contracts_verify real proofs.
4. Spike: proved HTTP/1.1 header parser only (no sockets) — validates refinement + state-machine story.
5. Crypto: implement **packages/li-crypto** in Li + vector tests; optional later li-crypto-hacl publish package — not a blocker.
6. Benchmarks: scaffold tier5_http + nginx baseline CSV before li-httpd ships — methodology frozen early.
7. P0: finish 2e–2f — this unlocks the “easy” path (write spec, implement, lic build or fail).
8. P0b: nginx audit → li_invariant list + bench baseline (no li-httpd).
9. M1: for each invariant, add proc + proof + minimal code; run bench/exploit.

Order: proof pipeline → spec from nginx lessons → small implementation → oracle tests (implementation is the easy part once specs compile).