Adding a backend

Governing contract: C-XPILE-BACKEND-TRAIT — read this first. The invariants it pins: target_ownership, lower_idempotency, target_consistency, compile_contract_citation, frame_lower_is_pure. Those are what your implementation must satisfy, and all five are about the SUCCESS path. Through v0.1.617 this line also listed an “error-path-names-the-contract requirement” and a “target-suggestion on unsupported constructs” — the contract has neither, so contributors were told to satisfy a requirement that does not exist and that most shipped backends do not meet (PMAT-1437).

This walks through what it takes to add a new code-lane backend to xpile. See Adding a frontend for the read-side flow; if you’re adding a proof-lane backend the broad strokes are the same but you’d implement ContractBackend instead.

1. Scope what your backend will and won’t emit

A backend doesn’t have to handle every construct in meta-HIR. It does have to fail cleanly on the ones it can’t. So:

1. Pick the meta-HIR subset you’ll lower.
2. For each unhandled construct, return BackendError::Lower naming the construct — never emit something approximate.

Naming the governing contract and suggesting a better --target are worth doing and are what the best existing messages do, but they are house style, not an invariant: measured over a fixed corpus, 4 of 40 refusals name a contract and 7 suggest a target (see the backends reference). The xpile-rust-codegen crate is the reference implementation; its shell rejection (see shell-roundtrip tutorial) is the shape to copy.

2. Scaffold the crate

$ cargo new --lib crates/xpile-mylang-codegen

Register in the workspace Cargo.toml:

members = [
    ...
    "crates/xpile-mylang-codegen",
]

[workspace.dependencies]
...
xpile-mylang-codegen = { version = "0.1.0", path = "crates/xpile-mylang-codegen" }

In the crate’s Cargo.toml:

[dependencies]
xpile-backend  = { workspace = true }
xpile-meta-hir = { workspace = true }
thiserror      = "1"

3. Implement the trait

#![allow(unused)]
fn main() {
use xpile_backend::{Artifact, Backend, BackendConfig, BackendError, Target};
use xpile_meta_hir::Module;

pub struct MyLangBackend;

impl Backend for MyLangBackend {
    fn name(&self) -> &'static str {
        "mylang"
    }

    fn targets(&self) -> &[Target] {
        &[]
    }

    fn lower(&self, module: &Module, config: &BackendConfig) -> Result<Artifact, BackendError> {
        let _ = (module, config);
        // 1. Begin with a provenance comment naming the backend +
        //    governing contract.
        // 2. Emit a `// xpile-contract: <ID>` citation per contract in
        //    `f.applicable_contracts()` — which is often EMPTY (a
        //    comparison-only body has no governing contract), and then
        //    you emit no citation line. Do not emit one per function.
        // 3. Lower meta-HIR statements.
        // 4. On unsupported constructs, return `BackendError::Lower`
        //    naming the construct. Naming the governing contract and
        //    a better `--target` too is house style (see §1), not a
        //    requirement — most shipped backends do neither.
        todo!()
    }
}
}

What is non-negotiable is that the citations you emit are derived from applicable_contracts() and resolve to a real contract — not that every function has one. The CI gate is crates/xpile/tests/contract_citation_integrity.rs, which transpiles the fixture corpus and fails if an emitted citation names a contract absent from contracts/*.yaml (every_emitted_citation_resolves_to_an_on_disk_contract) or if a contract that is applicable goes uncited (every_applicable_contract_is_actually_cited).

Through v0.1.617 this paragraph named crates/xpile/tests/qa_gate.rs as the gate that “parses every emitted artifact and fails if a citation is missing”. That file contains no citation logic at all — it binds contracts’ qa_gate: required_tests: names to real #[test] fns — so the requirement stated here was enforced by nothing under that name.

4. Register in xpile-core::default_session

Wire the backend into the default registry. Look at how xpile-rust-codegen and xpile-ruchy-codegen are registered in crates/xpile-core/src/lib.rs::default_session().

5. Decide how to discharge C-PY-INT-ARITH

This contract governs arithmetic. Your backend’s choice:

• By construction (target has unbounded integers — like Lean’s Int): emit native arithmetic, no overflow checks.
• By checked-op + slow path (target has fixed-width integers — like Rust’s i64): emit .checked_*().expect("…C-PY-INT-ARITH slow path…") calls.
• By compile-time guarantee (target has refinement types or unbounded compile-time constants — like SPIR-V OpConstant): document why and how.

Whichever you pick, the panic/error text must name the contract.

6. Write the tests

7. Lift the contract

If your backend introduces a new construct or boundary, write a Layer-2 translation contract for it. Pattern after xlate-py-list-to-vec-v1.yaml. Then add Lean theorems and Kani harnesses; run xpile quorum until it reports QUORUM.

8. Run the quality gate

Same as for frontends:

cargo fmt --all -- --check
cargo check --workspace
cargo clippy --workspace --all-targets -- -D warnings
pv lint contracts/
cargo deny check advisories

9. Update the book

If your backend is meaningfully new (a new target language, not just an internal improvement), add a row to the Reference: backends table and link a tutorial.