Refuse Rather Than Guess: Importing WIT, OpenAPI, MCP, Cordis and A2A Surfaces as Emission-by-Default Services

Pitch

A foreign interface description says nothing about whether an operation can be undone, so an importer that wants a sound effect audit must default every operation to "irreversible", weaken that only on a written positive claim, refuse any signature it would have to guess, and treat its own generated text as an attack surface.

Abstract

Language bindings and client generators turn an interface description (WIT, OpenAPI, an MCP tool list, an untyped TypeScript plugin, an A2A Agent Card) into typed stubs. They transcribe shapes, but a shape does not say whether a call is read-only, retryable or reversible, and a generator that silently fills the gap makes every later effect audit unsound. We describe five importers in the revl compiler that share one rule: every imported operation is declared emission (crosses the system boundary irreversibly) unless a written positive claim says otherwise: an author or engineer assertion written in the generated source next to the operation or, for OpenAPI, a safe HTTP method under RFC 9110. Because a service declaration bounds what its providers may do, the compiler rejects a plain operation backed by an emission extern, so a weakened operation cannot call an emission extern, although the check cannot make a false author claim true. Constructs the importer cannot map faithfully (WIT streams, OpenAPI allOf, untyped TypeScript parameters, gRPC) are refused by name with a pointer and a way forward; the Cordis importer's --mark-unrecovered mode makes gaps loud instead of fatal. Results from an A2A peer are returned as Untrusted, and reach is bounded by endpoint host alone. Treating the generator as an attack surface found two defects in the OpenAPI importer: a newline in document text ended a comment and injected a compiled host-code extern, and a URL credential became a capability token and leaked into the compiled IR. Both are fixed and covered by tests (4 and 11 respectively). The importers total about 6000 lines with about 250 test functions.

Problem and claim

Existing generators (OpenAPI Generator, wit-bindgen, protobuf and gRPC codegen, MCP client wrappers) are judged on whether the output compiles and round-trips data. They do not answer a second question that matters once the output sits inside a system with an effect audit: what does the generator assert about side effects that the source interface never stated? A generated client for GET /logout or delete-everything: func() is indistinguishable, at the type level, from one that reads.

The claim: the sound default for an imported operation is the pessimistic one, and the weakening rules can be made small, explicit and auditable. The compiler, not the generator, enforces the pairing between a plain operation and a pure extern. Failure to recover a signature must stop or be marked, never be filled in. The generator's own output is untrusted-input-derived code and needs the same discipline as any template engine.

This is a tool and design paper, not a soundness proof. The claim is bounded by what the docs say: "Safe-by-spec is a claim, not a proof" (docs/import-openapi.md section 1).

Contributions

1. One import rule across five interface languages (WIT, OpenAPI, MCP tool lists, Cordis TS plugins, A2A Agent Cards): service plus extern plus provider, operations default to emission, weakening needs a written positive claim (or, for OpenAPI, a safe HTTP method), an unmatched override is an error.
2. A graded evidence table for weakening: a WIT /// @revl:pure comment by the interface author or a --pure flag by the importing engineer (WIT), a purpose-built author assertion (MCP readOnlyHint), the HTTP method under RFC 9110 (OpenAPI), JSDoc @revl:pure (Cordis), with strengthening taking one voice and weakening taking unanimity.
3. Refuse-by-name tables for unmappable constructs, with JSON pointer or line and a remedy, plus --mark-unrecovered (Cordis) for the untyped-source case.
4. Two generator-injection findings with executed reproducers and fixes: comment-ending newline injecting a compiled extern; URL userinfo becoming a capability token and reaching the IR.
5. The A2A binding: card as a claim, results Untrusted, host-only reach bound, exact version claim, no inverse synthesised, Task lifecycle as a four-operation projection with shape-gated replies.
6. Export in the other direction (WIT, client, OpenAPI), so a revl composition can publish the typed surface it consumes.

Related work

Evidence on main

Numbers that exist

• Source size: src/revl/import_wit.py 1058 lines, src/revl/import_openapi.py 1964, src/revl/import_cordis.py 1474, src/revl/import_a2a.py 1480, plus src/revl/a2a_boundary.py 526 and src/revl/a2a_task.py 325 (wc -l at 45bec431f).
• Test function counts above (def-level, not parametrised cases).
• Injection test: 5 vectors per the roadmap entry (docs/v2.0-roadmap.md:1568), 4 test functions (one is parametrised, label); URL credential: 11 tests.
• No measurements of import coverage on real-world specs exist. No count of how many public OpenAPI documents are refused (the doc itself says allOf "will bite most often").
• No user study and no false-refusal rate.

Paper outline

1. Motivation: two operations that look the same to a schema.
2. The family rule and the evidence ladder (table).
3. Why the weakened form is still sound: the compiler check, with the rejection message.
4. Refusal tables and --mark-unrecovered.
5. The generator as an attack surface: the two findings.
6. A2A: a card as a claim; taint, reach, version, Task lifecycle.
7. Export direction and round-trip.
8. Evaluation (to be done): coverage, false-weakening rate, fuzz.
9. Limits and related work.

Threats to validity and limits

• Weakening rests on human or author claims the compiler cannot verify. A GET that writes remains a lie, "with a verb, a path and an author attached" (docs/import-openapi.md:155-160). The result is not verified.
• Idempotent is not reversible: PUT and DELETE are emission idempotent, still irreversible for the reversal guarantee.
• The compensate-grade claim is a ceiling: audit surface only, best-effort, and does not undo observation (docs/import-openapi.md:196-205).
• A2A: "There is no verified remote badge" (docs/import-a2a.md:62-72). Untrusted bounds what flows to authority sinks locally; it does not make the peer trustworthy. The remote call is not part of the teardown guarantee, and the docs say so.
• A2A streaming, push notifications, non-text modalities and the remote row failure semantics are listed as not projected (docs/import-a2a.md:252-270). The Task lifecycle is projected as four operations in code; whether that is complete for real peers is untested.
• The injection findings are from internal audits of the importer; no external adversary study. The audit itself lists other surfaces as unexamined at the time (docs/v2.0-roadmap.md:1568): non-py bridge/seam crossings and Python repr() injection.
• The type mapping is lossy in places the docs admit: u64 above 2^63-1 does not survive; WIT char widens to Str.
• The importers and the checking compiler are one project; "the compiler enforces the pairing" only means as much as the checker's effect propagation, including its documented name-based limits (docs/mcp-bridge.md section 1: emissions hidden behind function values are treated as may-emit).

Fact-check

Claims in this draft were checked against revl main at commit 45bec431f: 32 checked, 10 corrected.

Cite this draft

@misc{revlp52,
  author       = {Thomas Moussajee},
  title        = {Refuse Rather Than Guess: Importing WIT, OpenAPI, MCP, Cordis and A2A Surfaces as Emission-by-Default Services},
  year         = {2026},
  howpublished = {\url{https://inso1337.github.io/revl/research/P52.html}},
  note         = {Research draft, not peer reviewed. Written against revl commit 45bec431f. Licensed CC BY 4.0.}
}

Text licensed CC BY 4.0, author Thomas Moussajee.