xpile

A polyglot transpile workbench with provable contracts at every layer.

xpile is a CLI + library that takes a source file in one language and emits an equivalent program in another, with the equivalence itself pinned down as a machine-checked contract.

Four source languages — Python, C, Shell, WebAssembly text — share a single canonical meta-HIR and dispatch through nine backends — Rust, Ruchy, PTX, WGSL, SPIR-V, WebAssembly, Lean 4, Shell, forjar YAML. A fifth frontend, Ruchy, is registered for routing but refuses every .ruchy input — there is no Ruchy parser, so reading Ruchy is a non-zero exit with a reason, not a silent empty transpile. A proof lane parallel to the code lane relates LaTeX and Lean 4 theorems through the same YAML contract substrate — one contract frontend (LaTeX) and two contract backends (LaTeX, Lean 4 theorems), both of which are scaffolds today. There is no mdBook contract frontend or backend; through v0.1.617 this sentence named one (PMAT-1440).

Run xpile info for the live registry and xpile quorum for the live per-contract stratum table and its QUORUM / PARTIAL / UNVERIFIED totals. Not every contract is discharged: the totals line reports how many reach §14.4 quorum and how many are still PARTIAL.

Why xpile exists

Most transpilers live in a single repo per source-target pair: depyler for Python→Rust, decy for C→Rust, and so on. That topology hits a wall the moment you need hybrid transpilation — a single artifact that crosses a language boundary:

• CPython program calling a C extension
• Python kernel launching CUDA code via PTX
• Python orchestrator shelling out to a POSIX script
• Rust crate invoking a Lean-derived correctness proof

xpile’s premise: a shared meta-HIR + a shared contract substrate makes those hybrid flows tractable. The same C-PY-INT-ARITH contract that governs the Python-int → Rust-i64 overflow lane also governs the Python-int → Lean-Int proof-lane shadow.

What you can do today

• xpile transpile factorial.py → emit Rust with overflow checks
• xpile transpile factorial.py --target ruchy → emit Ruchy
• xpile transpile factorial.py --target lean → emit a Lean 4 def
• xpile transpile factorial.py --target wasm → emit WebAssembly text
• xpile transpile script.sh --target shell → POSIX-shell round-trip
• xpile info, xpile diamond, xpile quorum — inspect the substrate

How this book is organised

• Getting started walks you through install + a first transpile.
• Concepts explains the two lanes, the contract taxonomy, and the Diamond-tier substrate.
• Tutorials are end-to-end recipes for common flows.
• Reference is exhaustive CLI / frontend / backend documentation.
• Contributing covers adding a frontend or backend.

Every concept page links back to the governing contract YAML so you can trace a sentence in prose to the equation in contracts/ to the Lean theorem in contracts/lean/ to the Kani harness in contracts/kani/.

Installation

From crates.io (recommended)

cargo install xpile

This installs the xpile CLI binary into ~/.cargo/bin/. Requires Rust 1.93 or newer.

Verify:

xpile --version

It prints xpile <version> for the release you just installed. No version is pinned in this book: a transcript with a numeral in it goes stale the next time the workspace is published, which is exactly how this page came to claim xpile 0.1.0 for two months after 0.1.6xx was live. Compare against crates.io/crates/xpile for the current release.

From source

git clone https://github.com/paiml/xpile
cd xpile
cargo install --path crates/xpile

A source checkout is required for three of the four analysis commands, and not for the fourth. Measured in an empty directory on 2026-07-31, against the shipped binary:

The contracts/ directory is not what any of the three are blocked on: when it is absent all four fall back to the embedded contract set and say so on stderr. Through v0.1.618 this page said a checkout was required for all four because they “default to reading the contracts/ directory” — wrong about xpile diamond, which README.md correctly documents as working anywhere, and wrong about the cause for the other three. crates/xpile/tests/book_published_command_witness.rs (XPILE-BOOKTRANSCRIPT-001, PMAT-1511) now derives the roster from xpile --help and re-measures each verdict by running the subcommand in an empty scratch directory, so this table cannot drift from the binary in either direction.

Workspace crates

xpile is structured as a 31-crate workspace, published to crates.io as one lockstep batch — every member carries the same version as the xpile CLI. To use a sub-crate as a library:

# Cargo.toml
[dependencies]
xpile-core      = "0.1"
xpile-frontend  = "0.1"
xpile-backend   = "0.1"
xpile-meta-hir  = "0.1"
xpile-contracts = "0.1"

See the Reference: backends page for the full crate list and what each one does.

Optional tools

These are not required to use xpile but are mentioned throughout this book:

• pv (provable-contracts on crates.io) — validates contract YAML against the published schema. Install with cargo install aprender-contracts-cli.
• pmat — the PAIML quality enforcer. Used by the contributing flows.
• cargo kani — bounded model checker used in the Symbolic stratum. Install via the official Kani instructions.

Quick start

This walks you through your first xpile transpile.

Prerequisite

cargo install xpile

See Installation for alternatives.

1. A Python file

Save the following as factorial.py:

def factorial(n: int) -> int:
    return 1 if n <= 1 else n * factorial(n - 1)

2. Transpile to Rust

$ xpile transpile factorial.py
// xpile-generated from Python module factorial

// xpile-contract: C-PY-INT-ARITH
pub fn factorial(n: i64) -> i64 {
    if (n <= 1i64) { 1i64 } else {
        (n).checked_mul(factorial(
            (n).checked_sub(1i64).expect("xpile: i64 subtraction overflow; bigint promotion (contract C-PY-INT-ARITH slow path) not yet implemented")
        )).expect("xpile: i64 multiplication overflow; bigint promotion (contract C-PY-INT-ARITH slow path) not yet implemented")
    }
}

Note the // xpile-contract: C-PY-INT-ARITH citation and the .checked_*().expect(...) wrappers. Every arithmetic operation preserves the C-PY-INT-ARITH contract: i64 overflow panics with a pointer to the unimplemented bigint slow path, rather than silently wrapping the way native i64 arithmetic would.

You can type-check the output directly:

$ xpile transpile factorial.py --out factorial.rs
$ rustc -O factorial.rs --crate-type lib --emit=metadata --out-dir .

--emit=metadata type-checks and stops; it produces no runnable artifact, so this pair proves the emit compiles, not that it computes anything. Through v0.1.618 the second line was written -o /dev/null, which exits 1 on any host where the invoking user cannot write to /dev — i.e. essentially every reader’s: rustc puts its temp dir beside the -o path, and reports error: couldn't create a temp dir: Permission denied (os error 13) at path "/dev/rmeta…". That is an environment error wearing a compile error’s clothes, and this repository had already diagnosed it once, in its own sweep harness, and written the correction down — “correct invocation is --out-dir” (PMAT-1446, CHANGELOG [0.1.618]) — two months after this page started telling readers to run the broken spelling.

CI runs the compile-and-execute path on the README.md copy of the transcript above, not on this page’s copy: crates/xpile/tests/readme_quickstart_witness.rs parses the two blocks out of README.md, transpiles, compiles with rustc -O, and executes to assert factorial(10) == 3628800 and that factorial(21) panics naming C-PY-INT-ARITH rather than wrapping. The three published copies of that transcript — README.md, this page, and Tutorial: Python → Rust — are byte-identical as measured on 2026-07-31, but nothing enforces it: only the README.md copy is gated, so a correction applied there can leave these two behind. That is a measurement, not an invariant; the gate is specified as XPILE-BOOKTRANSCRIPT-001 in docs/roadmaps/queue.yaml next_lane. Before PMAT-1415 the paragraph claimed the execution with nothing behind it at all: the test that asserted 3628800 read the -> BigInt fixture, a different program whose emit has no checked_ call to overflow.

3. Same source, different backends

$ xpile transpile factorial.py --target ruchy
// xpile-generated from Python module factorial

// xpile-contract: C-PY-INT-ARITH
fun factorial(n: i64) -> i64 {
    if (n <= 1i64) { 1i64 } else {
        (n).checked_mul(factorial(
            (n).checked_sub(1i64).expect("xpile: i64 subtraction overflow; bigint promotion (contract C-PY-INT-ARITH slow path) not yet implemented")
        )).expect("xpile: i64 multiplication overflow; bigint promotion (contract C-PY-INT-ARITH slow path) not yet implemented")
    }
}

$ xpile transpile factorial.py --target lean
-- xpile-generated from Python module factorial

/-- xpile-contract: C-PY-INT-ARITH -/
def factorial (n : Int) : Int :=
  if (n <= (1: Int)) then (1: Int) else (n * (factorial (n - (1: Int))))

Three different targets, the same governing contract — and you can see it in all three, because all three emit it: // xpile-contract: on the Rust and Ruchy lanes, /-- xpile-contract: … -/ as a Lean docstring, which is the form lean will actually parse (see Tutorial: Python → Lean for why the attribute spelling was retired). Lean’s Int is unbounded, so C-PY-INT-ARITH is satisfied by construction — no overflow checks emitted, because there is no overflow.

Through v0.1.618 both transcripts above were shown without their header and citation lines, and the Ruchy one shortened its two panic messages to "..." — so the two blocks offered as evidence for “the same governing contract” were the two with the contract deleted, on the page a first-time reader reaches first. They were born that way in the commit that created this book (2026-05-20, PMAT-446), in which the Rust block on this same page did show the citation; the emitter never changed under them. Both are now the live emit of the shipped binary as measured on 2026-07-31 — the Lean block byte-for-byte — with the sole exception that the Ruchy if is reflowed to fit the page (the binary prints it on one line) — the same reflow the Rust block above uses, and the only difference between what is printed here and what the binary writes.

4. Inspect the substrate

$ xpile info
$ xpile diamond     # works anywhere — the contracts are compiled in
$ xpile quorum      # needs a checkout (reads docs/roadmaps/roadmap.yaml)

See the CLI reference for everything xpile can do, and Installation for the measured per-command table. Through v0.1.618 both lines above read # if you're in a repo with contracts/, which was false for xpile diamond — it exits 0 in an empty directory, README.md had always said so, and xpile quorum’s own error text said so too — and named the wrong cause for xpile quorum, whose blocker is the development ledger rather than contracts/.

5. Runnable examples (library API)

The repository ships six runnable examples under crates/xpile/examples/ that use the library API instead of the CLI:

$ git clone https://github.com/paiml/xpile && cd xpile
$ cargo run --example 01_python_to_rust   -p xpile  # factorial → Rust
$ cargo run --example 02_python_to_lean   -p xpile  # factorial → Lean
$ cargo run --example 03_python_to_ruchy  -p xpile  # gcd → Ruchy (Python-floor `%`)
$ cargo run --example 04_shell_roundtrip  -p xpile  # POSIX shell in → POSIX shell out
$ cargo run --example 05_python_to_shell  -p xpile  # `subprocess.run([...])` → shell
$ cargo run --example 06_inspect_session  -p xpile  # what's registered?

Each one prints input + output + a “what this demonstrates” block.

Next steps

• Two lanes, one substrate — the mental model.
• Tutorial: Python → Rust — same example, expanded with the full overflow-discharge story.
• Tutorial: POSIX shell round-trip — a different shape of transpile.

Two lanes, one substrate

xpile has two parallel pipelines that share the YAML contract substrate. This is the single most important mental model in the system.

Frontends                      Backends
─────────                      ─────────
python   ─┐               ┌─→ rust
c        ─┤               ├─→ ruchy
bashrs   ─┼→ meta-HIR ─→ ─┼─→ bashrs
ruchy    ─┤               ├─→ lean
wasm     ─┘               ├─→ wasm
                          ├─→ ptx
                          ├─→ wgsl
                          ├─→ spirv
                          └─→ forjar

That is the code lane — runnable code in, runnable code out. The names are the registry keys xpile info prints, and this roster is checked against the live registry in both directions by crates/xpile/tests/lane_roster_witness.rs — a name here that nothing registers, or a registered name missing here, reds.

What a name in the left column does and does not mean. It means the registry routes that spelling to a frontend, not that the frontend parses it: ruchy is registered so a .ruchy input gets a named refusal, and it refuses every input. xpile info is the live word on which frontends lower — it prints frontends (5 registered, 4 lowering) and tags the exception. Per-backend maturity is not shown here on purpose: it lives in one place, the measured Backends → Status table, and it used to be duplicated into this diagram — where it went stale, marking PTX, WGSL, SPIR-V and Lean as scaffolds or planned long after all four emitted (PMAT-1440).

ContractFrontends             ContractBackends
─────────────────             ─────────────────
                                ┌─→ latex
latex       ───→ contracts ←──←─┤
                                └─→ lean-theorem

That is the proof lane — notation in, notation and proofs out, both sides talking to the same contract YAML.

The proof lane is the immature one, and the diagram above is a wiring diagram, not a capability claim. One contract frontend is registered and it does parse; both contract backends are scaffolds that return a fixed _scaffold payload no field of the contract can influence, so xpile info reports them as contract_backends (2 registered, 0 rendering) and tags each. Real rendering is v0.2.0 work — see Backends and PMAT-1429.

There is no mdBook contract frontend or backend, and no Lean 4 contract frontend. MdBook is an enum variant in xpile-contracts with nothing behind it. Through v0.1.617 this page drew both, and drew three code-lane frontends (C++, Rust, Lean 4) that likewise do not exist — .cpp, .rs and .lean inputs all exit non-zero — while omitting the wasm frontend and the wasm and forjar backends that do (PMAT-1440).

Why two lanes?

The conventional answer for “how do I prove a transpile is correct?” involves either:

1. A handwritten paper: prose argument that the transpile preserves semantics. Convincing to a reader, opaque to a machine.
2. A whole-system mechanization: every transpile path encoded as a theorem in a single proof assistant. Convincing to a machine, exhausting to a maintainer.

xpile takes a middle path: contracts in YAML are the shared substrate. Each contract has one fact (“Python int overflow is unbounded; an i64 codomain requires bigint promotion to discharge it”), expressed three ways:

• Code lane: the Rust backend emits checked_mul().expect(...) so every overflow becomes a panic, not silent wrapping.
• Proof lane: a Lean 4 theorem pyIntArithRefinement proves the refinement of ℤ → Option Int64 at the structural level.
• Audit lane (extrinsic): a Kani BMC harness exhaustively explores 256⁴ ≈ 4.3B configurations checking the invariant.

When all three voices agree, the contract is at quorum — the mechanically-checked equivalent of “consensus across independent oracles.”

Lean 4 spans both lanes

Lean 4 is special: it’s both a programming language (so it appears in the code lane as a backend) and a proof assistant (so it appears in the proof lane as the canonical theorem-bearing format). LaTeX is proof-lane-only.

The citation bridge between the two lanes uses format-native structured constructs, never regex over body text:

• In Lean: @[xpile_contract "C-PY-INT-ARITH"] attribute.
• In LaTeX: \xpileContract{C-PY-INT-ARITH}{Python int arithmetic}.
• In mdBook: a structured HTML comment — specified, not implemented; no mdBook ContractBackend is registered, so nothing emits this form today (PMAT-1440).

Those are the ContractBackend forms — contract YAML rendered to theorem text or LaTeX, which is read as prose and never elaborated. The code lane is separate: xpile transpile x.py --target lean cites with a /-- xpile-contract: … -/ docstring, because a file that lean must actually parse cannot carry an attribute no prelude registers (see Reference: backends). Both are structured; only the docstring is resolvable out of a live elaborated environment.

This is the design decision that makes the proof lane robust against edit churn — see the C-XPILE-CONTRACT-BACKEND-TRAIT contract for the formal statement.

What flows through meta-HIR

The middle box in the code-lane diagram is meta-HIR — a canonical intermediate representation that every frontend lowers into and every backend lowers from. It is intentionally minimal and includes:

• Function signatures with typed parameters and return types
• All binary + unary operators (Python semantics, not C semantics — so // is floor-division, not truncating-division)
• Function calls including self-recursion
• A kind: kernel vs kind: pattern distinction in the contract taxonomy that disambiguates “specific construct” from “structural invariant”

When you add a new frontend or backend, the meta-HIR is the contract you commit to — see Adding a frontend.

Where to go next

• Contracts and the 5-layer taxonomy — the YAML substrate that both lanes share.
• The Diamond-tier substrate — how pv enforces algebraic equivalence on top of the contract.
• Tutorial: Python → Lean 4 — what the proof-lane shadow of a code-lane transpile looks like.

Contracts and the 5-layer taxonomy

Governing contracts: C-XPILE-FRONTEND-TRAIT, C-XPILE-BACKEND-TRAIT, C-XPILE-CONTRACT-FRONTEND-TRAIT, C-XPILE-CONTRACT-BACKEND-TRAIT — these are the “structural” Layer-3 contracts that govern the trait surfaces themselves. The invariants it pins: extension_ownership, target_ownership, format_ownership, parse_idempotency, lower_idempotency, render_idempotency, citation_preservation, compile_contract_citation.

A contract in xpile is a YAML file in contracts/ that pins down one fact about the transpile pipeline. Each file declares:

• id — C-PY-INT-ARITH, etc. (unique, globally cited)
• layer — one of the 5 layers (see below)
• lane — code, proof, or both
• kind — kernel (a specific construct) or pattern (a structural invariant)
• equations — the actual statements being claimed
• stratum_votes — which oracles have ratified each statement

pv lint contracts/ validates every YAML against the published schema and must report 0 errors — it runs in the pre-push gate, so a contract that does not lint cannot land. Run it for the live count and warning tally.

The 5 layers

Every layer has both a code-lane and a proof-lane shadow. ls contracts/*.yaml is the live population — it spans all 5 layers and grows most sprints; see the reference table for the annotated list.

The 4-stratum quorum

Per the ruchy 5.0 §14.4 N-of-M oracle quorum rule, a contract is discharged when ≥1 vote arrives from ≥3 of these 4 strata:

xpile quorum prints one row per contract and ends with a totals line:

totals: <N> QUORUM, <N> PARTIAL, <N> UNVERIFIED (<N> contracts total)

No numerals are reproduced here on purpose. This page carried a pasted totals line — twelve contracts, all of them at quorum, none partial — for two months after the substrate had grown past it, and every numeral in it was wrong by the end. A transcript is a claim, and a claim in prose is not re-derived when the tree moves. Run the command. Not every contract is at quorum: a contract that lands before its Lean theorem or Kani harness sits at PARTIAL until the missing stratum votes, and the totals line is where that shows.

Why YAML (not Lean)?

A natural question: why not declare contracts directly in Lean? Two reasons:

1. Non-experts must read them. A C++ backend implementer who doesn’t know Lean still needs to know what C-COMPILE-RUST-TO-PTX-MMA actually says about mma.sync instruction scheduling. YAML is the floor; Lean is the ceiling.
2. Multiple oracles, one source of truth. Kani BMC harnesses, Lean theorems, and runtime fixtures all reference the same equation. If the equation lived in Lean, you’d have to round-trip through Lean even to spell it out in a Kani comment.

So YAML is the substrate; Lean theorems and Kani harnesses are bound to YAML equations via citation. The C-NOTATION-LATEX-MATH-TO-EQUATION contract governs that citation bridge.

What “kind: kernel” vs “kind: pattern” means

A kernel contract pins down one specific construct end-to-end. For example, C-PY-INT-ARITH says exactly: “Python int is unbounded; an i64 codomain must emit .checked_*().expect(...)”.

A pattern contract pins down a structural invariant that any implementation must satisfy. For example, C-XPILE-FRONTEND-TRAIT says: “Any type implementing the Frontend trait must produce a deterministic parse — same input, same xpile_meta_hir::Module.”

The distinction matters because kernels compose by addition (more constructs supported), but patterns compose by intersection (more invariants required). Pattern contracts are typically thinner but apply to every implementation; kernel contracts are typically larger but apply only to one construct.

What comes next

• The Diamond-tier substrate — how pv enforces algebraic invariants on top of the equations.
• Reference: contracts at v0.1.0 — the exhaustive 12-contract table.

The Diamond-tier substrate

Source of truth: docs/specifications/sub/diamond-taxonomy.md in the canonical spec. The Diamond program runs in parallel to the book and is the deepest layer of contract enforcement.

The 4-stratum quorum (Semantic, Symbolic, Runtime, Extrinsic) is the floor: it answers “does the contract hold?”. The Diamond-tier substrate answers a stronger question: “which algebraic invariants of the contract hold, and at what depth?”

Concretely: each contract carries a growing portfolio of _diamond theorems in contracts/lean/, each proving a structural property that any conforming implementation must satisfy.

Refinement tiers

A contract can be discharged at increasing levels of confidence:

Higher tiers strictly entail lower tiers. Bronze is by construction; Diamond is by careful axiomatization.

What “depth-N UNIVERSAL” means

A Diamond program isn’t proved in one go — it grows monotonically. We say the substrate is at depth-N UNIVERSAL when every contract has at least N distinct Diamond theorem categories.

Read the universal depth off xpile diamond, not off this page. The totals block prints how many contracts sit at each depth-N+; the universal depth is the largest N whose count still equals contracts_total.

Eleven UNIVERSAL milestones (depth-3 through depth-13) were achieved over the founding twelve contracts, each via a “broadening sweep” that extended a previously narrow-deep pattern out to the whole substrate of the day. That deep core is still there — a group of contracts carries ≥13 Diamond categories, and two go past depth-20.

But the substrate has since grown well past twelve, and crates/xpile/tests/diamond_coverage.rs deliberately grandfathers the depth-13 gate: a new contract joins at depth-1+ rather than paying a depth-13 treadmill on arrival. So over the whole population the universal depth is far lower than the deep core’s — most contracts carry a single Diamond category. This page said “depth-1..13 UNIVERSAL — all 12 contracts have ≥13 Diamond categories” long after that stopped describing every contract, which under the definition directly above it is the difference between a claim about all contracts and a claim about thirteen of them.

The 13 recurring templates

By v0.1.0 the substrate had discovered 13 recurring algebraic templates that show up across many contracts:

Templates 10–13 form a compositional suite: lift Bronze→Silver, project Silver→Bronze, and the composition equals identity. This is the substrate-level proof that the canonical refinement-tier model is internally coherent.

Inspecting the Diamond state

$ xpile diamond
xpile diamond — Diamond-tier coverage (PMAT-249)
depth: 0 Diamonds = none, N Diamonds = depth-N (exact — the column is never bucketed; the `depth-N+` figures in the totals block are CUMULATIVE counts, not classifications)

  contract                                 diamond  depth
  ------------------------------------------------------------
  C-PY-INT-ARITH                                21  depth-21
  C-COMPILE-RUST-TO-PTX-MMA                     20  depth-20
  C-BASHRS-POSIX-IDEMPOTENCE                    13  depth-13
  C-FFI-CPYTHON-EXT                             13  depth-13
  C-NOTATION-LATEX-MATH-TO-EQUATION             13  depth-13
  ...

totals: <N> Diamond theorems across <N> contracts
  depth-1+: <N> contracts, depth-2+: <N> contracts, ...

The legend line and every contract row above are compared to the live binary, by equality, in crates/xpile/tests/diamond_depth_label_witness.rs. The earlier copy of this transcript omitted the legend — an unmarked elision, which is why the honest repair of this page never saw that the legend was the falsehood: it announced a depth-3+ bucket the reporter could not produce, directly above a column whose first three rows read depth-21+, depth-20, depth-13 (PMAT-1448).

The totals block is reproduced here as a shape, not as numbers. A pasted numeral is a claim that nothing re-derives, and the numerals that used to sit here (171 Diamond theorems across 12 contracts, depth-1+..depth-13+: 12 contracts each (UNIVERSAL)) outlived the tree they described by twenty-three contracts.

JSON output is available via xpile diamond --json and is parsed by the CI gate crates/xpile/tests/diamond_coverage.rs, which holds the depth-13 floor over a named, grandfathered set of contracts — the ones that had reached it when the gate was written. A contract outside that set is deliberately not checked against the floor, so the gate protects the deep core against regression and does not claim anything about the rest.

What comes next

• Tutorial: Python → Rust — the complete C-PY-INT-ARITH story, from spec to emit.
• Reference: contracts — the founding-twelve catalogue with links to Lean theorems and Kani harnesses.

Tutorial: Python → Rust (with overflow checks)

Governing contract: C-PY-INT-ARITH — Layer 1 (semantics), code lane, kind: kernel. The invariants it pins: addition_no_overflow, addition_overflow_promotion, multiplication_quadratic_promotion, division_floor_semantics, modulo_floor_semantics — the mismatch between Python’s unbounded int and Rust’s fixed-width i64, which is why the emit carries .checked_*().expect(...) at every arithmetic site until the bigint slow path is implemented.

This tutorial walks through what happens, step by step, when you transpile a Python arithmetic function to Rust. By the end you’ll know exactly which contract is doing what work, and where to look in the codebase for each step.

1. The Python source

# factorial.py
def factorial(n: int) -> int:
    return 1 if n <= 1 else n * factorial(n - 1)

This is the same example from the quick start. The function is deliberately small — typed parameter, typed return, one ternary, one self-recursive call, two arithmetic ops.

2. The transpile

$ xpile transpile factorial.py --target rust
// xpile-generated from Python module factorial

// xpile-contract: C-PY-INT-ARITH
pub fn factorial(n: i64) -> i64 {
    if (n <= 1i64) { 1i64 } else {
        (n).checked_mul(factorial(
            (n).checked_sub(1i64).expect("xpile: i64 subtraction overflow; bigint promotion (contract C-PY-INT-ARITH slow path) not yet implemented")
        )).expect("xpile: i64 multiplication overflow; bigint promotion (contract C-PY-INT-ARITH slow path) not yet implemented")
    }
}

Three things to notice:

1. // xpile-contract: C-PY-INT-ARITH at the top of the emitted function. This is the citation that links the emitted Rust back to the contract YAML. The C-XPILE-BACKEND-TRAIT contract’s compile_contract_citation equation quantifies over the constructs of the emitted artifact, so it requires a citation exactly where a construct has a governing contract. factorial does arithmetic, so it gets one; a comparison-only function emits none, at exit 0, by design. Through v0.1.617 this step said the contract “requires every emitted function to carry such a citation”.
2. checked_sub / checked_mul wrap every arithmetic op. Python ints are unbounded, Rust i64 isn’t. The contract requires that we do not silently wrap; instead we panic and point the user at the bigint slow path.
3. The panic message itself names the contract. Anyone debugging an overflow gets a literal pointer to C-PY-INT-ARITH in the panic text — no detective work required.

3. Verifying the round-trip in CI

xpile’s CI doesn’t just check that the emitted Rust compiles — it checks that it computes the right values. Two tests do it, over two different programs, and the difference matters:

// crates/xpile/tests/readme_quickstart_witness.rs — the i64 program
// shown above. Source and expected transcript are parsed out of
// README.md, so the published example cannot rot.
the_readme_output_compiles_under_rustc_o_and_computes_3628800
the_readme_overflow_claim_panics_naming_the_contract   // factorial(21)

// crates/xpile/tests/transpile_e2e.rs — a DIFFERENT factorial.py,
// annotated `-> BigInt`. Emits no `checked_` call at all; compiled
// against an inline BigInt shim.
factorial_emitted_rust_computes_correct_values

Every PR runs both. Through v0.1.617 only the second existed, while this page and README.md both described it as covering the i64 emit — which it never did: a shim whose Mul is a plain * cannot observe an overflow panic. PMAT-1415 added the first test rather than softening the claim, because the claim turned out to be true.

4. The proof-lane shadow

Same source, proof lane:

$ xpile transpile factorial.py --target lean
-- xpile-generated from Python module factorial

/-- xpile-contract: C-PY-INT-ARITH -/
def factorial (n : Int) : Int :=
  if (n <= (1: Int)) then (1: Int) else (n * (factorial (n - (1: Int))))

Notice the /-- xpile-contract: C-PY-INT-ARITH -/ docstring — this is the proof-lane analogue of the // citation in the Rust output. Both sides of the dual emission carry the same contract ID, so any downstream analyzer (a doc generator, a citation graph, the audit falsifier) can join the two — and on the Lean side it joins through Lean.findDocString? on the elaborated environment rather than a regex over the file. (Through v0.1.617 this was an @[xpile_contract "…"] attribute; see Python → Lean for why it changed.)

Lean’s Int is unbounded, so the contract is satisfied by construction — no .checked_*() calls needed. The same contract, discharged two different ways depending on the host language.

5. Where this lives in the codebase

What you’ve learnt

• A xpile transpile is dual-emitted: code lane and proof lane both carry the same contract citation.
• The contract YAML is the single source of truth; everything else cites it.
• Discharge happens differently per target — checked_*() in Rust, free-by-construction in Lean.
• CI doesn’t just check compilation, it checks semantic round-trip (assert_eq!(factorial(10), 3628800)).

What’s next

• Tutorial: Python → Lean 4 — going deeper on the proof-lane side.
• Tutorial: POSIX shell round-trip — a qualitatively different shape (same-language round-trip).

Tutorial: Python → Lean 4 (proof-lane shadow)

Governing contracts: C-PY-INT-ARITH (the Layer-1 semantics of Python int arithmetic) and C-XLATE-LEAN-TO-RUST (the inverse-direction Layer-2 lowering, used for the proof-lane round-trip check). The invariants it pins: addition_no_overflow, division_floor_semantics, modulo_floor_semantics, def_to_rust_fn, theorem_carried_as_lean_sidecar.

In the Python → Rust tutorial the emitted Rust runs. In this tutorial the emitted Lean 4 proves. The same source file produces a Lean def carrying the same contract citation, and the proof-lane version of “CI passed” is “the Lean file kernel-checks.”

1. The same Python source

# factorial.py
def factorial(n: int) -> int:
    return 1 if n <= 1 else n * factorial(n - 1)

2. Transpile to Lean

$ xpile transpile factorial.py --target lean
-- xpile-generated from Python module factorial

/-- xpile-contract: C-PY-INT-ARITH -/
def factorial (n : Int) : Int :=
  if (n <= (1: Int)) then (1: Int) else (n * (factorial (n - (1: Int))))

A few things to notice:

1. /-- xpile-contract: C-PY-INT-ARITH -/ is a Lean docstring, not a line comment. The C-XPILE-CONTRACT-BACKEND-TRAIT contract forbids regex-over-body citations and requires format-native structured constructs; a docstring is one, and Lean.findDocString? env factorial` retrieves the citation out of the elaborated environment by declaration name.

   Through v0.1.617 this lane emitted @[xpile_contract "…"] instead. That form reads as more structured and was strictly worse: xpile_contract is registered as a Lean attribute nowhere, so lean rejected the file with a parse error — and since --contracts on is the CLI default, --target lean was the one backend whose default output its own toolchain could not read. PMAT-1405 replaced it with the docstring, which elaborates standalone with no import. The attribute form survives only in the contract-rendering lane (contract YAML → Lean theorem text), whose output is prose and is never elaborated.

2. Int, not Int64. Lean’s Int is unbounded. The C-PY-INT-ARITH contract is satisfied by construction — nothing to discharge, no overflow checks emitted, no slow-path placeholder.

3. Direct arithmetic, no .checked_*(). Because nothing can overflow.

3. Why this matters

When you transpile Python to Rust, you get something that runs but needs runtime checks. When you transpile the same Python to Lean, you get something that proves the function is well-defined over the unbounded integers. The two are shadows of each other through the shared C-PY-INT-ARITH contract.

This is the proof-lane analogue of the code-lane round-trip:

4. Cross-lane citation graph

Because both emissions carry the same C-PY-INT-ARITH citation — just in language-native form — a downstream tool can build a citation graph:

contracts/py-int-arith-v1.yaml
    │
    ├── (Semantic stratum)   contracts/lean/PyIntArith.lean
    │                          ├── theorem refinement_bronze
    │                          ├── theorem refinement_silver_int_to_i64
    │                          ├── ... 21 Diamond theorems ...
    │                          └── theorem round_trip_identity_diamond
    │
    ├── (Symbolic stratum)   contracts/kani/py_int_arith.rs
    │                          └── #[kani::proof] fn property_overflow_bound
    │
    ├── (Runtime stratum)    tests/fixtures/factorial.py
    │                          (mentions C-PY-INT-ARITH in a doctring)
    │
    └── (Extrinsic stratum)  roadmap.yaml :: PMAT-{017..156, 214..251, ...}
                               (human attestations across the project history)

— and a single tool, xpile quorum, reports the per-stratum vote tally that determines whether C-PY-INT-ARITH is at QUORUM, PARTIAL, or UNVERIFIED.

5. The full proof-lane round-trip

Beyond Python → Lean, the proof lane includes a second direction: Lean → Rust, governed by C-XLATE-LEAN-TO-RUST. This means a Lean def can be lowered back to a Rust function with panic-on-overflow, preserving the contract citation across both directions.

The bidirectional flow is what enables the “single contract, multiple discharges” workflow described in Two lanes, one substrate.

What’s next

• Tutorial: POSIX shell round-trip — a different shape of “same-language round-trip” for the C-BASHRS-POSIX-IDEMPOTENCE contract.
• The Diamond-tier substrate — the algebraic-invariants layer on top of every contract.

Tutorial: POSIX shell round-trip

Governing contract: C-BASHRS-POSIX-IDEMPOTENCE — Layer 1 (semantics), code lane, kind: pattern. The invariants it pins: subprocess_run_equals_shell_run, exit_code_consistency — the supported POSIX-shell subset, and the cross-domain Python↔shell flow.

This tutorial walks through xpile’s same-language round-trip for POSIX shell: parse .sh, lower into meta-HIR, emit POSIX shell again. It’s the simplest demonstration of the bashrs merger that landed at v0.1.0 (PMAT-037..119).

1. The source

#!/usr/bin/env sh
mkdir -p /tmp/out
echo "hello" > /tmp/out/file.txt

Save this as script.sh. Two POSIX commands, idempotent by virtue of mkdir -p and the > redirect.

2. Round-trip

$ xpile transpile script.sh --target shell
#!/bin/sh
# xpile-bashrs-backend (v0.1.0 PMAT-039 / XPILE-BASHRS-MERGER-001 Layer B)
# xpile-contract: C-BASHRS-POSIX-IDEMPOTENCE
# module: script
mkdir -p /tmp/out
echo "hello" > /tmp/out/file.txt

The emitted file:

• carries a # xpile-contract: C-BASHRS-POSIX-IDEMPOTENCE citation,
• preserves the shebang (normalised to #!/bin/sh — the supported POSIX dialect),
• emits each Cmd statement back in its original form, and
• adds a backend-identifier comment so users know which lane produced the file.

3. Cross-domain: Python → shell

The bashrs merger isn’t just about same-language round-trip; it also enables cross-domain transpiles like Python → shell, where a Python subprocess.run([...]) call lowers to a Cmd statement and emits real POSIX shell. (Stricter Python subsets fall in scope here as the work item series continues; see PMAT-040..052 for the lowering roster.)

Conversely, asking the Rust backend to lower a shell-only construct fails cleanly:

$ xpile transpile script.sh --target rust
Error: backend `rust` failed

Caused by:
    lowering error: unsupported item: Rust backend does not lower
    Stmt::Cmd (`mkdir` with 2 arg(s)) — contract
    C-BASHRS-POSIX-IDEMPOTENCE governs this construct; use
    `--target shell` to emit POSIX sh via bashrs-backend

This message names the governing contract and suggests the correct target, and rust is one of the backends whose refusals do. It is a good message, not an instance of a general rule: most probed refusals name neither, and five of the nine backends name neither in any of theirs. The measured counts live in exactly one place — Backends → Status.

C-XPILE-BACKEND-TRAIT does not require either half; every one of its equations is a property of the emitted artifact. Through v0.1.617 this paragraph called this message an instance of that contract’s “structural compile-contract citation” invariant — a name that is not an equation key, for an equation whose formula ranges over Artifact.primary (PMAT-1437, PMAT-1438).

4. The idempotence invariant

C-BASHRS-POSIX-IDEMPOTENCE does not say “the script is idempotent” in the general sense (that’s undecidable). It says the supported subset of POSIX shell — the constructs the bashrs frontend recognizes — round-trip without drift, and that the constructs we emit are idempotent by their nature (mkdir -p, redirects, conditional file creation, etc.).

The substrate enforces this at four strata:

— all four voices agree at v0.1.0; xpile quorum reports QUORUM.

5. Where this lives

What’s next

• Reference: CLI commands — the full surface.
• Reference: backends — what each backend emits and what it refuses to emit.

CLI reference

Governing contract: C-XPILE-BACKEND-TRAIT for emit-side dispatch and citation. The invariants it pins: target_ownership (each --target reaches exactly one backend) and compile_contract_citation (a target-specific construct may not be emitted without a Layer-5 citation). It pins nothing about ERROR paths — through v0.1.617 this line said it governed them (PMAT-1437).

All commands are subcommands of xpile. Run xpile --help or xpile <cmd> --help for inline documentation.

xpile info (default)

Lists registered frontends and backends.

$ xpile info
xpile — polyglot transpile workbench

Code lane:
  frontends (5 registered, 4 lowering):
    - python (py, pyi)
    - c (c, h)
    - ruchy (ruchy)  [routing only — INPUT refuses, no parser]
    - bashrs (sh, bash, zsh, mk)  [claims REFUSED — no parser: *.mk, Makefile, Dockerfile]
    - wasm (wat)
  backends (9):
    - rust → Rust
    - ruchy → Ruchy
    - ptx → Ptx
    - wgsl → Wgsl
    - spirv → Spirv
    - wasm → Wasm
    - lean → Lean
    - bashrs → Shell
    - forjar → ForjarYaml

Proof lane:
  contract_frontends (1):
    - latex ← LatexMath
  contract_backends (2 registered, 0 rendering):
    - lean-theorem → LeanTheorem  [scaffold — fixed `_scaffold` payload, ignores the contract]
    - latex → LatexMath  [scaffold — fixed `_scaffold` payload, ignores the contract]

Use this to confirm your install can see every lane. The two count forms are load-bearing: frontends (5 registered, 4 lowering) and contract_backends (2 registered, 0 rendering) mean the registry holds entries that do not do the job their name implies. ruchy is registered so a .ruchy input gets a specific refusal rather than a generic one (PMAT-1346), and both proof-lane contract backends are scaffolds that return a fixed _scaffold payload for every contract (PMAT-1429). The third form, [claims REFUSED — no parser: …], is the PARTIAL case (PMAT-1433): bashrs genuinely lowers .sh / .bash / .zsh, so it counts among the 4 lowering frontends, but *.mk, Makefile and Dockerfile are routed only so the refusal can name the missing dialect — they never lower. Read the extension list as “what reaches this frontend”, not “what it parses”; the bracket is what separates the two. This transcript is regenerated from the binary and pinned by crates/xpile/tests/cli_docs_drift.rs.

xpile transpile

xpile transpile [OPTIONS] <INPUT>

The main command. The file extension selects the frontend; --target selects the backend.

Examples:

xpile transpile factorial.py                     # Python → Rust (default)
xpile transpile factorial.py --target ruchy      # Python → Ruchy
xpile transpile factorial.py --target lean       # Python → Lean 4
xpile transpile script.sh --target shell         # Shell round-trip
xpile transpile factorial.py --out factorial.rs  # Write to a file

If a backend cannot lower a particular construct, transpile exits non-zero and writes no artifact; the message names the backend that refused and the construct it refused. Some messages also name the governing contract and a better --target — the shell-roundtrip tutorial shows one that does — but that is house style, not a guarantee, and most backends do neither. The counts are measured, and they live in exactly one place: Backends → Status. Through v0.1.617 this paragraph asserted both halves as universal (PMAT-1437, PMAT-1438).

xpile hybrid

Phases 1–2 of the hybrid flow (§16). Walks a module directory, dispatches each source file to its frontend, and reconciles the cross-language FFI boundaries (FfiManifest::reconcile) into a manifest. Prints one line per resolved boundary (symbol, from→to, shim_id); on unresolved boundaries it prints them and exits non-zero — the manifest_completeness gate of C-FFI-CPYTHON-EXT.

xpile hybrid [OPTIONS] <PATH>

<PATH> is a directory holding the mixed-language module (e.g. app.py alongside _core.c); sources are detected by extension.

--verify is the north-star executing differential: it is the one command that compares xpile’s output against CPython by running both, rather than by comparing text.

xpile diamond

Reports per-contract Diamond-tier coverage. Walks every YAML in contracts/ and counts _diamond-suffixed lean_theorem: references.

xpile diamond [--contracts-dir <DIR>] [--json]

The --contracts-dir flag defaults to ./contracts. If you installed xpile via cargo install xpile and don’t have a checkout, point this at a clone of the repo.

JSON output is consumed by the CI gate at crates/xpile/tests/diamond_coverage.rs. That gate does not hold a universal depth above 1. It holds a depth-13 floor over a named, grandfathered set — the contracts that had already reached it when the gate was written (PMAT-475) — so a contract joining the substrate today is checked against depth-1 and nothing deeper. The universal depth over the whole population is whatever xpile diamond’s totals block reports, and it is set by the shallowest contract, not by the deep core.

See The Diamond-tier substrate for what the numbers mean.

xpile quorum

Reports the §14.4 N-of-M oracle quorum per contract.

xpile quorum [--contracts-dir <DIR>] [--json]

For each contract, tallies votes across the four strata:

• Semantic — lean_theorem: refs in the contract YAML
• Symbolic — kani_harness: refs in the contract YAML
• Runtime — the union of fixtures under tests/fixtures/ mentioning the contract ID and top-level *.rs files under each --witness-dir that mention it and carry a runtime-availability probe call (naming the ID alone is not execution)
• Extrinsic — roadmap work items mentioning the contract ID

A contract is QUORUM when ≥1 vote arrives from ≥3 strata, PARTIAL at 1–2, UNVERIFIED at 0. The command’s last line is the live totals — read it there rather than from this page. Not every contract is at quorum; the PARTIAL count is routinely non-zero as new contracts land ahead of their Lean or Kani votes.

xpile audit

Reports falsifier F1 (Layer-1 contract citation coverage) for a corpus. Walks the given path, transpiles every recognised source file, and reports the % of the functions that require a citation which actually carry one. The denominator is not every emitted function: it is the subset whose applicable_contracts() is non-empty (XPILE-FALSIFY-002 / PMAT-023 narrowed it there precisely because comparison-only and logical-only functions correctly emit none). The report prints both numbers on separate lines — functions emitted and require citation — and F1 is the second one’s coverage. On a corpus of three functions of which one does arithmetic, it reads:

  functions emitted   : 3
  require citation    : 1
  with citation       : 1
  coverage (F1)       : 100.0%   [OK]

Through v0.1.617 this page described the denominator as “emitted functions”, which reads that same output as 33.3%.

xpile audit <PATH>

Drives the XPILE-FALSIFY-001 metric from the provability roadmap — the falsifier fires if Layer-1 coverage ever drops below the contracted threshold.

xpile attestations

Reports the Extrinsic stratum’s per-contract attestation counts. Walks contracts/*.yaml to discover the contract ID universe, then scans roadmap.yaml work-item mentions for each ID.

xpile attestations [--contracts-dir <DIR>] [--roadmap <PATH>]

Feeds the §14.4 quorum’s Extrinsic-stratum vote tally alongside Semantic (Lean), Symbolic (Kani), and Runtime (diff_exec).

xpile help

xpile help [SUBCOMMAND]

Prints help for a subcommand. Equivalent to --help.

Frontends

Governing contract: C-XPILE-FRONTEND-TRAIT — Layer 3 (architectural), code lane, kind: pattern. Every frontend implements this trait. The invariants it pins: extension_ownership, parse_idempotency, source_lang_consistency, ffi_boundaries_are_outgoing_only (plus Gold/Platinum/Diamond refinements over the same records).

A frontend reads a source file and lowers it to xpile’s canonical meta-HIR. Frontends never see other frontends; they all funnel through meta-HIR.

Status

xpile info prints this table live from the registry the CLI actually dispatches through — prefer it to this page.

The Name column is the key xpile info prints, not a display label.

The two path columns are DIFFERENT claims and PMAT-1433 exists because this table used to have only one. A frontend can be routed a path spelling and still refuse it: bashrs-frontend is claimed for *.mk, Makefile and Dockerfile so the refusal can name the dialect that is missing (PMAT-1420) instead of degrading to a generic “no frontend handles .mk” — but it has no Makefile dialect and no Dockerfile dialect, and every such input exits non-zero. Until PMAT-1433 the Extensions column read .sh, .bash, .zsh, .mk under status “Real POSIX parser”, and xpile info printed the same four extensions unannotated, because Frontend::lowers_input() is one boolean for the whole frontend and bashrs earns it on .sh. Both columns are now derived from the registry and checked by crates/xpile/tests/frontend_claim_disposition_witness.rs, which drives every claimed spelling through the frontend and asserts set equality in BOTH directions — so implementing the Makefile dialect reds this page until the row moves.

“Lowers” is a claim about the GRAMMAR, not about the file format

A claimed extension means the registry routes that spelling to that frontend and the frontend applies its own grammar to the bytes. It does not mean the file format the extension normally denotes is supported — and for .pyi and .h those are different things, because the canonical content of each format is precisely what the grammar rejects:

Both still appear under Extensions that LOWER above, and that is correct rather than a contradiction: put a .py-shaped definition in a .pyi, or a .c-shaped definition in a .h, and it lowers at exit 0. crates/xpile/tests/format_canonical_form_witness.rs (XPILE-FORMATFORM-001) measures both halves — the canonical form refuses AND the definition form lowers at the same path — so the table above cannot drift in either direction, and neither claim can be satisfied by a probe that was simply malformed.

Through v0.1.617 nothing said this. .pyi and .h were published as extensions that LOWER, with an empty Routed → REFUSED cell, on all three surfaces — this table, xpile info, and the dispatch-failure message — and no file in the canonical form of either format lowered at any of them (PMAT-1442).

The disposition gate could not have caught it, and says so itself: its subject is “does the answer depend on the path spelling”, so PROBES carries one program per FRONTEND and writes those same bytes to every spelling that frontend claims. PMAT-1433 generalised the paths a probe reaches and left the content fixed; that is [[PMAT-1433]]’s own “one probe per subject samples one of its N claims”, one dimension over.

⚠️ xpile info still prints - python (py, pyi) and - c (c, h) unannotated. Saying more there needs a per-INPUT granularity the refused_claims() mechanism does not have — it is per-CLAIM — so this page carries the measured table and xpile info does not. That is a disclosed gap, not a fixed one.

The proof lane registers one contract frontend, LaTeX math (latex-contract-frontend), which reads contract sources rather than programs.

Ruchy is registered but has no parser. It exists so that a .ruchy input gets a named refusal instead of a generic “no frontend handles this extension” — xpile transpile x.ruchy --target rust exits non-zero with a reason. It does not mean Ruchy input works; Ruchy is a fully supported output target (see backends). Nothing here silently returns an empty module: crates/xpile/tests/claims_drift.rs runs every registered frontend against a real program in its own language and fails if one answers with Ok(Module { items: [] }).

There is no C++, Rust, or Lean 4 frontend. This page claimed all three as “planned”/“scaffold” workspace members; no such crate exists and none is registered. Lean 4 and LaTeX appear in the proof lane and Rust appears as a backend, which is where the confusion came from.

Python frontend — what’s supported

The depyler frontend is the deepest at v0.1.0. The supported subset includes:

• typed def functions
• multi-statement function bodies
• ternary expressions
• if/elif/else chains
• function calls including self-recursion

An emitted function carries a xpile-contract: citation only when its body uses a construct some contract governs — a minority of the functions in a typical corpus, and by design. Function::applicable_contracts() returns nothing for comparison-only, logical-only, constant-only and call-only bodies, and the backends emit one line per returned ID, so an empty list emits no line at all. Measured: def ident(a: int) -> int: return a and a comparison-driven pick emit zero citations from --target rust, --target ruchy and --target lean, at exit 0. xpile audit’s F1 denominator excludes exactly those functions (XPILE-FALSIFY-002), and crates/xpile/tests/citation_surface_witness.rs (XPILE-CITESURFACE-001) pins it.

When a citation is emitted, two things vary independently, and both are measured by crates/xpile/tests/citation_id_matrix_witness.rs (XPILE-CITEMATRIX-001) rather than asserted here:

Which contract, by the function’s type — the same ID on every code lane:

Which comment form, by lane — the same form for every type:

That the ID is lane-independent and the form is type-independent is itself checked, so a lane that started citing something different would red rather than quietly disagree with the other two.

Through v0.1.617 this section said “Each emitted Rust/Ruchy/Lean function carries a // xpile-contract: C-PY-INT-ARITH citation for the arithmetic contract” — one sentence, false three times. The ID is type-directed, so C-PY-INT-ARITH is right only for int functions; // is not the Lean form, because PMAT-1405 changed that lane to a /-- … -/ docstring deliberately (a file lean must actually parse cannot carry the old attribute) and this page went on naming the Rust comment syntax for it; and the citation is not universal at all. PMAT-1445 corrected the first two and, in replacing the sentence, restated the third as “Each emitted function carries a xpile-contract: citation”. PMAT-1447 removed it and gated the class across every surface that states it.

For the full list, see the CHANGELOG Python subset (live, runtime-verified) section — that’s the canonical list to avoid duplication-and-drift.

Operator surface

Until PMAT-1441 this section claimed the whole of Python’s binary and unary operator sets, without listing either. Both claims were false — @, is, is not and unary + refuse — and the frontend’s own refusal message says so in the same breath (unsupported binary operator: MatMult — supported: + - * / // % & | ^ << >> **). The canonical CHANGELOG list linked above is enumerative and was correct; this page had paraphrased it into a universal it never states.

The block below is DERIVED: one probe per Python operator, driven through the live PythonFrontend, compared to this page by equality in crates/xpile/tests/frontend_operator_surface_witness.rs (XPILE-PYOPSURFACE-001). A REFUSES row is recorded only when the frontend’s own error names the operator and the same program with a reference operator in that slot lowers — so a mis-typed probe reds as a corpus bug instead of publishing a false refusal. Implementing one of these reds this page until the row moves.

class     variant   probe       disposition
BinOp     Add       a + b       lowers
BinOp     Sub       a - b       lowers
BinOp     Mult      a * b       lowers
BinOp     MatMult   a @ b       REFUSES
BinOp     Div       a / b       lowers
BinOp     Mod       a % b       lowers
BinOp     Pow       a ** b      lowers
BinOp     LShift    a << b      lowers
BinOp     RShift    a >> b      lowers
BinOp     BitOr     a | b       lowers
BinOp     BitXor    a ^ b       lowers
BinOp     BitAnd    a & b       lowers
BinOp     FloorDiv  a // b      lowers
Compare   Eq        a == b      lowers
Compare   NotEq     a != b      lowers
Compare   Lt        a < b       lowers
Compare   LtE       a <= b      lowers
Compare   Gt        a > b       lowers
Compare   GtE       a >= b      lowers
Compare   Is        a is b      REFUSES
Compare   IsNot     a is not b  REFUSES
Compare   In        a in b      lowers
Compare   NotIn     a not in b  lowers
UnaryOp   USub      -a          lowers
UnaryOp   UAdd      +a          REFUSES
UnaryOp   Invert    ~a          lowers
UnaryOp   Not       not a       lowers

ast.BinOp: 13 in Python, 12 lower, 1 REFUSE
ast.Compare: 10 in Python, 8 lower, 2 REFUSE
ast.UnaryOp: 4 in Python, 3 lower, 1 REFUSE

in / not in lower against a list[...] right operand (.contains), not against a scalar. Chained comparisons (0 < a < b) desugar to the and of adjacent pairs.

Shell frontend — what’s supported

The bashrs frontend parses a POSIX-shell subset sufficient for realistic build scripts:

• shebang normalisation
• variable assignment + expansion
• conditional file creation (mkdir -p, > file, >> file)
• pipelines
• if/elif/else
• for loops over expansions
• subprocess invocation (cmd arg1 arg2)

The supported set is locked in by the C-BASHRS-POSIX-IDEMPOTENCE contract. See the shell-roundtrip tutorial for an end-to-end example.

Calling a frontend as a library

#![allow(unused)]
fn main() {
use depyler_frontend::PythonFrontend;
use xpile_frontend::Frontend;

let frontend = PythonFrontend;
let module = frontend.parse_and_lower(path, source)?;
// `module` is a `xpile_meta_hir::Module`
}

The Frontend trait surface is intentionally minimal — see Adding a frontend for the full implementation guide.

Backends

Governing contract: C-XPILE-BACKEND-TRAIT — Layer 3 (architectural), code lane, kind: pattern. Every backend implements this trait. The invariants it pins: target_ownership, lower_idempotency, target_consistency, compile_contract_citation, frame_lower_is_pure (plus thirteen Diamond refinements over the same records). Every one of them is a property of the SUCCESS path — the contract says nothing at all about what a REFUSAL message contains. Through v0.1.617 this blockquote claimed it pinned “error paths must name the governing contract” and a “target-suggestion message”; it pins neither, and five of the nine backends do neither. See the measured table below and PMAT-1437.

A backend reads a xpile_meta_hir::Module and emits an artifact in some target language. Backends never see other backends; they all read from meta-HIR.

Status

xpile info prints this table live from the Target enum the CLI actually dispatches through — prefer it to this page.

Name and --target are two different strings, and for one backend they differ. Name is the registry key xpile info prints on the left of the arrow; --target is what you pass on the command line, and what parse_target accepts. They coincide for eight of the nine backends. They do not for the shell backend: xpile info prints - bashrs → Shell, and the flag is --target shell. Through v0.1.617 this column published bashrs, which the CLI rejects outright (unknown target) — see PMAT-1430.

--target also accepts the aliases wat (→ wasm), sh / bash (→ shell) and forjar-yaml (→ forjar). All four resolve to the canonical target in the table above and are otherwise indistinguishable from it. xpile transpile --help and the unknown target refusal both name the nine canonical spellings AND the four aliases; through PMAT-1435 they named only the nine, so this sentence was the only place in the repo that said so.

The proof lane registers two contract backends, lean-theorem and latex. Both are scaffolds: each returns a fixed _scaffold payload that no field of the contract can influence, so neither actually renders contract YAML today. xpile info reports them as contract_backends (2 registered, 0 rendering) and tags each one; crates/xpile/tests/proof_lane_scaffold_witness.rs measures the contract-independence rather than asserting it. Real rendering is v0.2.0 work — see PMAT-1429.

A ✅ here means “emits for its supported subset”, not “emits for every program” — each backend refuses constructs outside its subset rather than emitting something wrong. That refusal, and its exit status, is the guarantee. What the refusal MESSAGE contains is not.

Through v0.1.617 this paragraph said the message names “the governing contract and, where one exists, a better --target”. It usually names neither. The table below is measured, not asserted: crates/xpile/tests/backend_refusal_disclosure_witness.rs (XPILE-BACKENDREFUSE-001) runs a fixed seven-program corpus against every registered backend, keeps the failures that reached that backend’s own lower(), and re-derives these counts on every run. It compares them by equality — improving a message reds the gate and this table has to move with it.

Read it as a property of that corpus, not a verdict on each backend: a single probe samples one of a backend’s many refusal messages. What it does establish is that the old universal claim was false — 4 of 40 probed refusals named a contract ID, 7 named a better --target, and ptx, wgsl, spirv, bashrs and forjar did neither in any of theirs. Every message does name the backend that refused and the construct it refused. See the shell round-trip tutorial for a worked example.

Rust backend — what’s emitted

The Rust backend produces:

• pub fn declarations with typed parameters and typed returns
• All binary + unary operators using Python semantics:
  • // → checked_div + a floor correction (subtract 1 when the remainder is non-zero and its sign differs from the divisor’s)
  • % → checked_rem + a floor correction (add the divisor under the same condition), so the result takes the divisor’s sign as CPython does
  • neither uses div_euclid / rem_euclid: PMAT-538 removed those in v0.1.237 because they only match Python for a positive divisor (7 % -3 is -2 in Python but 1 under rem_euclid)
  • *, +, - → checked_mul, checked_add, checked_sub
• .expect("…contract C-PY-INT-ARITH slow path…") on every arithmetic wrap — the panic text names the contract
• A // xpile-contract: <ID> citation above each emitted function whose body uses a construct a contract governs — not above every function. applicable_contracts() is empty for comparison-only, logical-only, constant-only and call-only bodies, and those emit no citation line at all (see frontends). Through v0.1.617 this bullet stated it unconditionally.

The semantics-preserving choice of checked_div_euclid over the sloppy / operator is what discharges Layer-1 of C-PY-INT-ARITH: Python 7 // -2 == -4, not -3. The Rust default would be wrong; the backend’s choice is right by construction.

Lean 4 backend — what’s emitted

The Lean backend produces:

• def declarations with Int/Nat/typed parameters
• Int.fdiv and Int.fmod for // and %
• a /-- xpile-contract: <ID>[, <ID>]* -/ docstring above each emitted definition (one comma-separated docstring, because Lean permits at most one per declaration). Through v0.1.617 this was an @[xpile_contract "<ID>"] attribute, which no Lean prelude registers and which therefore made the default emit unparseable — PMAT-1405 replaced it, and crates/xpile/tests/lean_default_emit_witness.rs now runs lean on the default emit rather than asserting about it.

Because Lean’s Int is unbounded, C-PY-INT-ARITH is satisfied by construction — no overflow checks are needed. The emitted Lean is typically the most concise emit xpile produces.

Shell backend — what’s emitted

The bashrs backend produces:

• A #!/bin/sh shebang (normalised to the supported POSIX dialect)
• A # xpile-bashrs-backend (v0.1.0 ...) provenance comment
• A # xpile-contract: C-BASHRS-POSIX-IDEMPOTENCE citation
• One emitted Cmd statement per source command

See shell-roundtrip tutorial for real output.

Calling a backend as a library

#![allow(unused)]
fn main() {
use xpile_backend::{Backend, BackendConfig, Profile, Target};
use xpile_rust_codegen::RustBackend;

let config = BackendConfig {
    target: Target::Rust,
    profile: Profile::RustOut,
    hardware: None,
    emit_contracts: true,
};
let backend = RustBackend;
let artifact = backend.lower(&module, &config)?;
// `artifact` is a `xpile_backend::Artifact`; `artifact.primary` is the
// emitted Rust source.
}

The Backend trait surface is intentionally minimal — see Adding a backend for the full implementation guide.

How far the Ruchy lane actually gets

✅ Real emission above means xpile emits a .ruchy artifact for every input in its subset — and it does, for all of them. It does not mean the artifact survives the Ruchy toolchain. Measured over the repo’s own crates/xpile/tests/oracle_fixtures/*.py with ruchy v4.2.1:

So “compiles to Rust” holds for 8 of 39, and 21 emitted artifacts do not parse as Ruchy at all (Expected RightBrace, found Let). Through v0.1.617 the Status cell said compiles to Rust with no qualifier and the README diagram said full emission (compiles to Rust) — both read as a property of the lane rather than of a minority of it (PMAT-1440 established the ✅ itself is honest; this is the parenthetical beside it).

The counts are re-derived by crates/xpile/tests/ruchy_conformance_witness.rs (XPILE-RUCHYCONF-001) from the live fixture directory, with no denominator written down anywhere — so a 39th fixture cannot silently make this table stale, which is how the sibling figures in ruchy_exec_witness.rs came to read 38.

⚠️ CI cannot check the numbers. ruchy is not installed in any workflow, so the four counts are verified only where the toolchain is present; the wording rule below them is checked everywhere. That split is stated here rather than left to be discovered.

Error handling

When a backend cannot lower a particular construct it fails — non-zero, with no artifact — and the message names the backend that refused and the construct it refused (Stmt::Cmd, Expr::AwaitYield, etc.). That is the whole of what holds for every backend.

Naming the governing contract and suggesting a better --target are worth doing and are what the best messages do, but they are house style, not an invariant — see the measured table above: 4 of 40 probed refusals name a contract ID, 7 name a --target, and ptx, wgsl, spirv, bashrs and forjar do neither in any of theirs.

Nor does the contract require them. C-XPILE-BACKEND-TRAIT’s compile_contract_citation equation quantifies over ir_constructs(Artifact.primary) — the emitted artifact — so it constrains the success path only; refus, suggest and error path occur zero times in its 776 lines.

Through v0.1.617 this section published the contract and target halves as a numbered must and attributed them to that same equation “in action”. PMAT-1437 corrected the page header and the guarantee paragraph and left this section standing 100 lines below the table that refutes it — the same claim, in a different grammatical mood, in the same file. PMAT-1438 is the rest of that class.

Contracts — the founding twelve

The twelve contracts that shipped at v0.1.0, in source order. Each entry links to the contract YAML, its Lean theorems, and its Kani harness.

This page is not the full population. The substrate has grown well past twelve; ls contracts/*.yaml is the live set and xpile quorum prints one row per contract with its per-stratum votes and status. The entries below are annotated in a depth this page cannot sustain for every contract, so it stays scoped to the founding set rather than silently going stale — which is what it did do, presenting itself as “all N contracts” for two months while the tree grew.

pv lint contracts/ → PASS with 0 errors, enforced in the pre-push gate. Run xpile quorum for the live QUORUM / PARTIAL / UNVERIFIED totals; PARTIAL is routinely non-zero.

The Lean theorems and Kani harnesses for each contract live at the parallel paths contracts/lean/<Name>.lean and contracts/kani/<name>.rs in the repository.

C-PY-INT-ARITH

Layer 1 (semantics) / code lane / kind: kernel

Python int is unbounded; emitted target code must either:

1. discharge by construction (Lean’s Int is unbounded — no action), or
2. discharge by checked op + bigint fallback (Rust/Ruchy’s i64 needs .checked_*().expect("…C-PY-INT-ARITH slow path…") until the bigint slow path is implemented).

Diamond depth: 21 (deepest contract in the substrate). See the Python → Rust tutorial.

C-BASHRS-POSIX-IDEMPOTENCE

Layer 1 (semantics) / code lane / kind: pattern

The supported POSIX-shell subset round-trips without drift, and the emitted constructs are idempotent (mkdir -p, conditional file creation, redirects). Covers cross-domain Python↔shell.

See the shell-roundtrip tutorial.

C-XLATE-PY-LIST-TO-VEC

Layer 2 (translation) / code lane / kind: kernel

Python list → Rust Vec, with alias-preservation semantics. Pins down what happens when a = [1,2,3]; b = a; b.append(4) — both a and b see the mutation.

C-XLATE-LEAN-TO-RUST

Layer 2 (translation) / code lane / kind: kernel

Modelled only — nothing implements this direction. The contract specifies how all Lean 4 constructs (def, partial, inductive, instance, axiom, …) would lower to Rust, the inverse of the Python→Lean flow, and carries 33 equations, 33 Lean refinement theorems and 10 Kani harnesses saying so — one theorem per equation, and a Kani harness on ten of them. There is no Lean frontend: no registered frontend claims .lean (see frontends), so xpile transpile x.lean --target rust exits non-zero with “no frontend handles .lean” and no SourceLang::Lean module can be produced at all. The proofs range over abstract models — a LeanDef is a byte array — so they hold, and they hold of nothing shipped.

Through v0.1.617 the sentence above said 40 equations — seven more than the contract holds, and the one number in it that was wrong INFLATED the proof volume of the paragraph whose point is that none of it constrains shipped code. crates/xpile/tests/claims_drift.rs now derives all three from the YAML (PMAT-1455).

This page previously stated the lowering as present-tense fact. What kept that readable was the §14.4 quorum reporting C-XLATE-LEAN-TO-RUST at 4-of-4 strata: three of the four strata are satisfied by writing YAML and roadmap prose, and the fourth, Runtime, was completed by a fixture file that no test loads. xpile quorum now scores it Runtime 0 (still QUORUM, on Semantic + Symbolic + Extrinsic — which is the honest reading: a 3-of-4 quorum needs no implementation). crates/xpile/tests/quorum_fixture_evidence_witness.rs reds the day a Lean frontend lands, so this paragraph has to move rather than stay wrong.

C-XLATE-RUST-FN-TO-LEAN-THM

Layer 2 (translation) / proof lane / kind: kernel

A Rust fn annotated with a contract citation lifts to a Lean 4 theorem carrying the @[xpile_contract "..."] attribute. The proof-lane analogue of C-XLATE-LEAN-TO-RUST.

C-NOTATION-LATEX-MATH-TO-EQUATION

Layer 2 (translation) / proof lane / kind: kernel

LaTeX math — $...$, \(...\), \[...\], and the equation, align and gather environments — lowers to contract equations. Theorem-class environments (theorem, lemma, corollary, proposition, claim, definition, remark) lower to proof obligations, whose type is precondition when the body opens with \textbf{Precondition:} and postcondition otherwise. A \begin{proof} body is consumed and never reaches the equations block. Governs the bidirectional notation bridge between human-written math and machine-checked YAML.

The exact surface is machine-readable — the notation_surface block at the end of the contract — and crates/xpile/tests/notation_claim_witness.rs checks it both ways: every construct listed as lowering must produce output, and every construct listed as unimplemented must produce none. Four things are listed as unimplemented and are not claimed here: the lean_pointer half of proof-env lowering, multi-row align/gather splitting, [label] resolution to an equation key (it is passed through verbatim), and nested theorem environments.

This paragraph was false until 2026-07-28 (PMAT-1431). The theorem/proof half had never been implemented, and a theorem body’s math surfaced as a free-standing equation rather than as an obligation. The Lean theorems and Kani harnesses that back this contract stayed green throughout, because they range over abstract models rather than over the shipped parser. The two-way notation_surface check is what now ties them together.

C-XPILE-FRONTEND-TRAIT

Layer 3 (architectural) / code lane / kind: pattern

Every Frontend implementation must produce a deterministic parse (same input → same xpile_meta_hir::Module) and preserve source location information for diagnostic round-trip.

C-XPILE-BACKEND-TRAIT

Layer 3 (architectural) / code lane / kind: pattern

Every target-specific IR construct a Backend emits must cite a Layer-5 compile contract that sanctions it, structurally — on Artifact.citations, which the equation’s own invariant says is “NOT regex over Artifact.primary text”. That is compile_contract_citation, and like all twenty of this contract’s equations it quantifies over the emitted artifact. The contract says nothing about error paths.

Two things it also does not say, corrected at PMAT-1447 — through v0.1.617 this entry read “Every Backend emission must carry a structural contract citation (// xpile-contract: <ID>)”:

1. It is not about the // xpile-contract: <ID> comment. That line is the Layer-1/2 citation channel, emitted per ID returned by Function::applicable_contracts(); compile_contract_citation governs Layer-5 hardware sanctioning (mma.sync, @workgroup_size, asm!). The PTX lane makes the split visible: --contracts on and --contracts off emit byte-identical PTX, and its citations live only on Artifact.citations.
2. It is not universal over emissions. The equation’s domain says so outright — “Pure language-level constructs (function definitions, structs, arithmetic) do NOT require a citation”. Measured: xpile transpile ident.py --target rust on def ident(a: int) -> int: return a emits an artifact with no xpile-contract line anywhere, at exit 0. Through v0.1.617 this entry added “Error paths must name the governing contract”, which no equation states and most backends do not do; see Backends → Error handling for the measured position (PMAT-1437, PMAT-1438).

C-XPILE-CONTRACT-FRONTEND-TRAIT

Layer 3 (architectural) / proof lane / kind: pattern

Every ContractFrontend must produce a deterministic parse of its notation source into contract equations. One is registered — LaTeX. Through v0.1.617 this entry listed “LaTeX, mdBook, Lean”: there is no mdBook contract frontend and no Lean contract frontend, and naming them here read as a roster of what exists (PMAT-1440).

C-XPILE-CONTRACT-BACKEND-TRAIT

Layer 3 (architectural) / proof lane / kind: pattern

Every ContractBackend must use format-native structured constructs for the citation bridge — never regex over body text. In Lean: @[xpile_contract "..."]. In LaTeX: \xpileContract{...}{...}. In mdBook: a structured HTML comment — specified, not implemented; no mdBook ContractBackend is registered. Both registered contract backends are scaffolds today (xpile info reports contract_backends (2 registered, 0 rendering)), so this equation constrains a form nothing yet emits (PMAT-1440).

C-FFI-CPYTHON-EXT

Layer 4 (hybrid) / code lane / kind: pattern

The semantics of a CPython C-extension boundary: refcount discipline, GIL acquire/release at the boundary, error-propagation rules for PyErr_Occurred().

C-COMPILE-RUST-TO-PTX-MMA

Layer 5 (compile) / code lane / kind: pattern

The deepest layer — emitted PTX must respect the mma.sync shape constraints, cp.async pipelining, and SMEM budget. Diamond depth: 20. The PTX backend shipped as a scaffold at v0.1.0; it now emits real PTX — xpile transpile k.py --target ptx --hardware ptx:sm_80 produces a .version / .target / .visible .entry module for the scalar element-wise + control subset. --hardware is required to reach this backend; without a compute capability it refuses.

Adding a frontend

Governing contract: C-XPILE-FRONTEND-TRAIT — read this first. The invariants it pins: extension_ownership, parse_idempotency, source_lang_consistency, ffi_boundaries_are_outgoing_only. Those are what your implementation must satisfy.

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

1. Scope the language subset

A frontend never has to handle “all of language X.” It handles a subset, and the subset is the contract. So before you write any parser code:

1. Identify which xpile-meta-HIR constructs your language needs to lower into. (Likely: function decls, primitive arithmetic, control flow — the same set that depyler-frontend handles for Python.)
2. Write the subset YAML in contracts/. Pattern it after contracts/bashrs-posix-idempotence-v1.yaml.
3. Run pv lint contracts/ — your YAML must pass before you start writing Rust.

2. Scaffold the crate

$ cargo new --lib crates/my-frontend

Register it in the workspace Cargo.toml:

members = [
    ...
    "crates/my-frontend",
]

[workspace.dependencies]
...
my-frontend = { version = "0.1.0", path = "crates/my-frontend" }

In the crate’s Cargo.toml:

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

3. Implement the trait

#![allow(unused)]
fn main() {
use std::path::Path;

use xpile_frontend::{Frontend, FrontendError};
use xpile_meta_hir::Module;

pub struct MyFrontend;

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

    fn extensions(&self) -> &[&'static str] {
        &["myl"]
    }

    /// Path spellings this frontend CLAIMS but refuses for every input.
    /// Required, with no default: a frontend that lowers only some of what
    /// it claims must be able to say so (PMAT-1433).
    fn refused_claims(&self) -> &[&'static str] {
        &[]
    }

    fn parse_and_lower(&self, path: &Path, source: &str) -> Result<Module, FrontendError> {
        let _ = (path, source);
        // parse source → lower to meta-HIR
        todo!()
    }
}
}

Determinism is non-negotiable — the trait contract requires identical inputs to produce identical xpile_meta_hir::Module outputs. Test this directly: parse the same input twice, assert equality.

4. Register in xpile-core::default_session

Wire the frontend into the default registry. Look at how bashrs-frontend and depyler-frontend are registered in crates/xpile-core/src/lib.rs::default_session().

5. Write the tests

Three layers of testing are expected:

6. Lift the contract

Once the frontend compiles and the basic round-trip works, lift the substrate:

1. Write Lean theorems for each YAML equation (in contracts/lean/MyLangIdempotence.lean or similar).
2. Write Kani harnesses (in contracts/kani/my_lang_idempotence.rs).
3. Register both in the YAML’s stratum_votes: block.
4. Run xpile quorum — your contract should reach QUORUM.

7. Run the quality gate

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

All five must pass before pushing. Open a PR; CI enforces the same gate as a required status check.

8. Add a Diamond category

Once the contract is at QUORUM, add a structural-extensionality Diamond theorem to push the substrate towards UNIVERSAL coverage at the next depth. See docs/specifications/sub/diamond-taxonomy.md for the template families.

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.

Changelog

The canonical changelog lives at CHANGELOG.md in the repository root.

v0.1.0 — 2026-05-20 — first real release

• All 27 workspace crates published to crates.io.
• Factorial round-trip green in CI (Python → Rust + rustc -O + assert_eq!).
• 12 contracts at 100% QUORUM; 638 stratum-vote artifacts.
• Eleven UNIVERSAL Diamond milestones (depth-3..13); 171 wired Diamond theorems; 13 recurring algebraic templates.
• cargo install xpile installs the CLI for end users.

See the full CHANGELOG for the PMAT work-item series.