feat(effects): <HttpServer> — verified HTTP request handling via vera serve — release v0.0.193 by aallan · Pull Request #845 · aallan/vera

aallan · 2026-07-02T11:10:37Z

What

Verified HTTP request handling — the <HttpServer> effect (#305) — and release v0.0.193. Stage B of the server-effects sprint (WASI.md).

A server program defines a total, contract-checked handler and serves it:

public fn handle(@Request -> @Response)
  requires(true) ensures(true) effects(<HttpServer>)
{ ... }

vera serve examples/http_server.vera --port 8080

The accept loop lives in the host — handlers need no Diverge, are termination-checked like any function, and every contract on them is an ordinary Tier-1/Tier-3 obligation. The new examples/http_server.vera proves its status-range postcondition (result == 200 || result == 404) statically at Tier 1 — the headline: verified HTTP handlers.

Design

HttpServer is a marker effect (no operations; spec §7.7.5), registered like Async/Diverge. Request (method, path, headers, body) and Response (status, headers, body) are prelude ADTs, injected only when referenced (the Json/HtmlNode conditional pattern — an always-inject first cut broke six no-overhead WAT pins because the Map headers field pulls heap machinery into pure programs). User definitions shadow them.
Instance-per-request isolation: each request runs a fresh execute() (Stage-0 spike measured instantiation at ~0.02 ms). State<T> cannot leak between requests — pinned by test. Sequential handling in v1 (concurrency: WASI 0.3 compliance and native async I/O #406).
Layout-driven marshalling, never hardcoded: CompileResult.adt_layouts exports the constructor layouts this compilation computed; build_request_adt / decode_response_adt (vera/runtime/heap.py) fail loudly on an unexpected layout shape. A new InstanceCaller adapts a (Store, Instance) pair to the exact caller protocol the heap helpers already use (export lookup + store-context delegation) — validated empirically before building on it.
GC discipline: every intermediate allocation in the Request build is shadow-rooted (GC shadow-stack overflow in array_map (and sibling iterative builders) at ~4000 heap-allocating elements #570/html_parse and json_parse trap with Out-of-bounds memory access on inputs that pressure GC during host-side tree walk #692 class); an eager-GC round-trip test pins it, and dropping the pushes under mutation flips that test RED.
Contract violation → 500, always answered: a runtime trap inside a handler maps to a 500 whose JSON body carries the trap diagnostic (trap_kind, message, frames — the vera run --json envelope shape).
Fixed en route: Pass-1 fn signatures referencing prelude ADTs in params/return were computed before prelude registration and recorded unsupported in fn_param_types (the fn still compiled in Pass 2); a post-injection pass now re-registers exactly those (_register_fn is overwrite-idempotent). Functions may also now declare prelude-ADT-typed signatures servably.
Native-only: the browser runtime does not serve HTTP (documented divergence, spec §12.9.3).

Tests (all RED-first; 4 mutations kill)

tests/test_serve.py (8): GET/POST echo round-trips (method/path/headers/body all cross the boundary), status propagation, contract-violation → 500 with trap_kind, State<Int> isolation across requests, eager-GC round-trip, two clean make_server validation errors. All ephemeral ports.
Checker battery (5): effect-row acceptance pin, registry introspection, prelude-type destructure/construct (_check_clean — the vacuous _check_ok variants were tightened when 3 of 4 passed pre-change), State composition, status contract.
Codegen compilability/export test; CLI validation tests (missing file / type error before bind / missing-handler message).
Mutations: layout-shape guard broken → e2e RED; shadow pushes dropped → eager-GC RED; status offset shifted → status test RED; (plus the tier-count corpus pin moving 271/92/363 → 277/92/369 exactly by the example's 6 Tier-1 obligations).

Conformance + example

tests/conformance/ch09_http_server.vera at level verify (needs no network, unlike ch09_http/ch09_inference at check — rationale in the program header): 104 programs.
examples/http_server.vera (36 examples), examples/README.md row.

Docs

Spec §7.7.5 + §9.5.6 + §12.9.3; SKILL.md HttpServer section + effect list; TOOLCHAIN.md serve recipe; CLAUDE.md commands; TESTING/AGENTS/FAQ counts (suite at 5,615 via the corpus-parametrized tests); allowlist refresh with three fixer duplicate-key collisions resolved against the real spec lines.

Release v0.0.193

Version sync (6 sites), CHANGELOG cut + link refs, ROADMAP milestone chain updated, HISTORY: Stage-16 row plus the "By the numbers" table gains a permanent "HttpServer effect" milestone column (per maintainer direction, parallel to the v0.0.101 Inference column), the trailing soundness column refreshed to v0.0.191, totals footer and the opening sentence brought current (1,800+ commits / 193 releases / 92 active days — from git data).

Verification

full suite 5,615 + stress 26 green; mypy clean; ruff check (+ --select S) clean without --fix
conformance 104 / examples 36 / doc-counts / version-sync / site-assets / limitations / encoding / diagnostic-fields / spec+SKILL+README+FAQ+EXAMPLES example gates
vera verify examples/http_server.vera → 6/6 Tier 1
4 mutation kills, restored green

Closes #305

🤖 Generated with Claude Code

…pes (#305) S1 of the <HttpServer> stage (server-effects sprint, Stage B). The effect is a marker -- the accept loop lives in the host vera-serve driver, so a handler is an ordinary total, contract-checked handle(Request -> Response) function; no Diverge involved (premise corrected on the issue). - environment.py: HttpServer EffectInfo (no ops) + Request/Response AdtInfo (Request: method/path/headers/body; Response: status/headers/body; headers are Map<String, String>). - prelude.py: the two data decls inject CONDITIONALLY (a new _HTTP_SERVER_DATA block gated on _source_mentions_http_server, the Json/HtmlNode pattern) -- an always-inject first cut broke six no-overhead WAT pins because the Map headers field pulls heap machinery into pure programs; and a conditional _HTML_DATA placement before that never injected at all. User-defined data Request / data Response shadow the prelude. - compilability.py: HttpServer joins the effect whitelist (needs_memory: handlers touch Request/Response heap values). - _since.py: HttpServer since 0.0.193. RED-first: 5 checker tests (row acceptance pinned, registry introspection, prelude-type destructure/construct, State composition, status contract) + 1 codegen compilability/export test; the vacuous _check_ok variants were tightened to _check_clean when 3 of 4 passed before the change. Doc counts follow (5,588 tests). Refs #305 Co-Authored-By: Claude <[email protected]>

S2 of the <HttpServer> stage: the vera-serve driver serves a compiled program's handler with instance-per-request isolation (fresh execute() per request -- WASI.md check 9 measured instantiation at ~0.02 ms, so isolation is effectively free) and sequential v1 request handling. - vera/runtime/heap.py: InstanceCaller (adapts a (Store, Instance) pair to the caller protocol the heap helpers already use -- export lookup via __getitem__ + store-context delegation via __getattr__), build_request_adt (Request built from layout-supplied offsets, every intermediate allocation shadow-rooted per the #570/#692 discipline), decode_response_adt (read-only; status i64 + headers Map decode via _decode_attrs + body string). Both raise loudly on an unexpected layout shape rather than marshalling garbage. - CompileResult.adt_layouts: constructor layouts exported so the driver marshals with the exact offsets THIS compilation computed -- never hardcoded. - execute(): http_request=HttpRequestData(...) builds the Request ADT after instantiation and calls the handler with its pointer; ExecuteResult.http_response carries the decoded Response. - core.py: Pass-1 signatures for user fns whose params/return reference prelude ADTs were computed before the prelude registered those layouts (recorded 'unsupported' in fn_param_types even though the fn compiles in Pass 2); a post-injection pass re-registers exactly those (_register_fn is overwrite-idempotent). Found via the serve driver's handler validation, which reads fn_param_types. - vera/runtime/server.py: make_server(result, host, port) -- stdlib http.server, per-request execute(), handler traps (incl. runtime contract violations) map to 500 with the trap diagnostic JSON (trap_kind + frames, the vera run --json envelope shape), handler IO.print forwarded to the server console, loud ValueError when the program lacks a servable public handle(@request -> @response). RED-first (tests/test_serve.py, 7 tests): GET/POST echo round-trips (method/path/headers/body all cross the boundary), handler status propagation, contract-violation -> 500 with trap_kind, State<Int> isolation across requests (instance-per-request pinned), and two clean-validation errors. All on ephemeral ports. Doc counts follow (5,595 tests / 89 files). Refs #305 Co-Authored-By: Claude <[email protected]>

…305) S3 of the <HttpServer> stage plus the release machinery. - cli.py: cmd_serve (compile pipeline shared with cmd_run; clean exit-1 diagnostics for type errors / missing or wrong-signature handler / port-bind failure; Ctrl-C -> exit 130), --port/--host flags, dispatch + usage. RED-first CLI tests (missing file, type error before bind, missing-handler message). - examples/http_server.vera: the #305 headline demo -- a router whose status_of postcondition (result == 200 || result == 404) verifies at Tier 1 (vera verify: 6/6 Tier 1; the corpus tier pin moves 271/92/363 -> 277/92/369). examples/README.md row + count. - tests/conformance/ch09_http_server.vera at level VERIFY (needs no network, unlike ch09_http/ch09_inference at check) + manifest entry: 104 conformance programs. - Docs lockstep: spec 7.7.5 (marker effect), 9.5.6 (types, execution model, 500-on-violation), 12.9.3 (browser divergence row), SKILL.md HttpServer section + effect list, TOOLCHAIN.md serve recipe, CLAUDE.md commands + counts, AGENTS/FAQ/TESTING counts (suite grew to 5,614 via the corpus-parametrized tests), allowlist refresh with the fixer's three duplicate-key collisions resolved against the real spec lines (the known fix_allowlists pitfall). - Release v0.0.193: version sync across the six sites, CHANGELOG cut with the HttpServer section + link refs, ROADMAP milestone chain updated (#305 shipped), HISTORY: Stage-16 row, the By-the-numbers table gains a permanent 'HttpServer effect' milestone column (per maintainer direction, like the Inference column) with the trailing soundness column refreshed to v0.0.191, totals footer (1,800+ commits / 193 releases / 92 active days -- all from git data), and the stale opening sentence now reads Stage 16 / 92 days. Closes #305 Co-Authored-By: Claude <[email protected]>

Pins the shadow-rooting discipline in build_request_adt: with VERA_EAGER_GC=1 every allocation collects, so an unrooted method/path/headers/body allocation is swept mid-build and the echo returns garbage. Mutation-validated alongside the layout-shape guard and the Response status offset (each kill their discriminating test; suite restored green). Counts follow (5,615 tests). Refs #305 Co-Authored-By: Claude <[email protected]>

coderabbitai · 2026-07-02T11:11:02Z

Important

Review skipped

No new commits to review since the last review.

⚙️ Run configuration

Configuration used: Path: .coderabbit.yaml

Review profile: ASSERTIVE

Plan: Pro Plus

Run ID: cec2d0ce-689a-4f3b-96f0-c99bb06878e1

You can disable this status message by setting the reviews.review_status to false in the CodeRabbit configuration file.

Use the checkbox below for a quick retry:

🔍 Trigger review

📝 Walkthrough

[!WARNING]

Walkthrough skipped

File diffs could not be summarized.

🚥 Pre-merge checks | ❌ 3

❌ Failed checks (3 inconclusive)

Check name	Status	Explanation	Resolution
Changelog Covers Public-Surface Changes	❓ Inconclusive	Custom check execution failed before a final verdict was produced.	Retry the review run. If this persists, inspect pre-merge custom-check logs for infrastructure or agent runtime failures.
Spec And Implementation Move Together	❓ Inconclusive	Custom check execution failed before a final verdict was produced.	Retry the review run. If this persists, inspect pre-merge custom-check logs for infrastructure or agent runtime failures.
Diagnostics Carry An Error Code	❓ Inconclusive	Custom check execution failed before a final verdict was produced.	Retry the review run. If this persists, inspect pre-merge custom-check logs for infrastructure or agent runtime failures.

✨ Finishing Touches

🧪 Generate unit tests (beta)

Create PR with unit tests
Commit unit tests in branch feat/305-httpserver-effect

_{Comment @coderabbitai help to get the list of available commands.}

codecov · 2026-07-02T11:11:54Z

Codecov Report

❌ Patch coverage is 85.84906% with 30 lines in your changes missing coverage. Please review.
✅ Project coverage is 91.90%. Comparing base (78e5ef1) to head (7ad9e62).

Files with missing lines	Patch %	Lines
vera/cli.py	56.89%	25 Missing ⚠️
vera/runtime/server.py	94.44%	3 Missing ⚠️
vera/runtime/heap.py	96.29%	2 Missing ⚠️

Additional details and impacted files

@@            Coverage Diff             @@
##             main     #845      +/-   ##
==========================================
- Coverage   91.94%   91.90%   -0.04%     
==========================================
  Files          92       93       +1     
  Lines       27626    27836     +210     
  Branches      332      332              
==========================================
+ Hits        25400    25583     +183     
- Misses       2218     2245      +27     
  Partials        8        8

Flag	Coverage Δ
javascript	`65.23% <ø> (ø)`
python	`94.95% <85.84%> (-0.07%)`	⬇️

Flags with carried forward coverage won't be shown. Click here to find out more.

☔ View full report in Codecov by Harness.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.

The CI-only check_spec_examples gate (not in pre-commit) failed on this branch: the new effect-HttpServer and Request/Response prelude data blocks needed FRAGMENT allowlist entries, and the 9.5.6 insertion (+33 lines) had orphaned four pre-existing signature-fragment entries (float_is_nan, url_join, string_chars family, md_parse) that fix_allowlists cannot re-anchor once detached -- re-keyed to their fence lines and the three stale old keys removed. Gate now exits 0; no duplicate keys. Found in parallel by the local gate re-run (full output, not tail) and the review-toolkit round. Refs #305 Co-Authored-By: Claude <[email protected]>

aallan · 2026-07-02T11:21:49Z

Review round 1 (pr-review-toolkit code-reviewer) — recorded.

One merge-blocking finding, fixed in the commit just pushed:

Critical — the CI-only check_spec_examples gate failed on this branch (it is not in pre-commit, which is why local hooks stayed green). Two genuinely new spec blocks needed FRAGMENT allowlist entries (the §7.7.5 effect HttpServer {} fence and the §9.5.6 data Request/Response fence), and the §9.5.6 insertion (+33 lines) had orphaned four pre-existing signature-fragment entries (float_is_nan, url_join, the string_chars family, md_parse) that fix_allowlists.py cannot re-anchor once detached. All six re-keyed to their fence lines, the three stale old keys removed; the gate now exits 0 with zero duplicate keys.

Everything else came back verified clean: the core.py TypeAliasDecl branch byte-intact vs main with the #305 re-registration correctly scoped; layout-driven marshalling with loud shape guards and full shadow-rooting; http_response confined to the http_request path; server validation/isolation/trap-to-500 correct; CLI flag parsing safe on trailing flags; release prep consistent across all six version sites and the By-the-numbers metrics verified against the filesystem.

aallan · 2026-07-02T11:45:19Z

@coderabbitai review

coderabbitai · 2026-07-02T11:45:24Z

✅ Action performed

Review finished.

Note: CodeRabbit is an incremental review system and does not re-review already reviewed commits. This command is applicable only when automatic reviews are paused.

T and others added 4 commits July 2, 2026 11:12

aallan merged commit fa40f5b into main Jul 2, 2026
28 checks passed

aallan deleted the feat/305-httpserver-effect branch July 2, 2026 11:50

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat(effects): <HttpServer> — verified HTTP request handling via vera serve — release v0.0.193#845

feat(effects): <HttpServer> — verified HTTP request handling via vera serve — release v0.0.193#845
aallan merged 5 commits into
mainfrom
feat/305-httpserver-effect

aallan commented Jul 2, 2026 •

edited

Loading

Uh oh!

coderabbitai Bot commented Jul 2, 2026 •

edited

Loading

Review skipped

Walkthrough skipped

❌ Failed checks (3 inconclusive)

Uh oh!

codecov Bot commented Jul 2, 2026 •

edited

Loading

Uh oh!

aallan commented Jul 2, 2026

Uh oh!

aallan commented Jul 2, 2026

Uh oh!

coderabbitai Bot commented Jul 2, 2026 •

edited

Loading

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

aallan commented Jul 2, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

What

Design

Tests (all RED-first; 4 mutations kill)

Conformance + example

Docs

Release v0.0.193

Verification

Uh oh!

coderabbitai Bot commented Jul 2, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Review skipped

Walkthrough skipped

❌ Failed checks (3 inconclusive)

Uh oh!

codecov Bot commented Jul 2, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

aallan commented Jul 2, 2026

Uh oh!

aallan commented Jul 2, 2026

Uh oh!

coderabbitai Bot commented Jul 2, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

aallan commented Jul 2, 2026 •

edited

Loading

coderabbitai Bot commented Jul 2, 2026 •

edited

Loading

codecov Bot commented Jul 2, 2026 •

edited

Loading

coderabbitai Bot commented Jul 2, 2026 •

edited

Loading