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.

Seven frontends — Python, C, C++, Rust, Ruchy, Lean 4, Shell — share a single canonical meta-HIR and dispatch through seven backends — Rust, Ruchy, PTX, WGSL, SPIR-V, Lean 4, Shell. A proof lane parallel to the code lane round-trips between LaTeX, Lean 4 theorems, and mdBook through the same YAML contract substrate.

The repository ships with 12 contracts at full quorum (pv lint PASS, 0 errors), 638 stratum-vote artifacts (Lean theorems + Kani BMC harnesses), and eleven UNIVERSAL Diamond milestones — every contract has paired algebraic theorems at depths 3 through 13.

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 at v0.1.0

• 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 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
xpile 0.1.0

From source

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

A source checkout is also required if you want to run the analysis commands (xpile diamond, xpile quorum, xpile audit, xpile attestations) without passing --contracts-dir — they default to reading the contracts/ directory next to the working directory.

Workspace crates

xpile is structured as a 27-crate workspace; all crates are published to crates.io at v0.1.0. 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 compile and run the output directly:

$ xpile transpile factorial.py --out factorial.rs
$ rustc -O factorial.rs --crate-type lib --emit=metadata -o /dev/null
$ # CI uses this exact path: rustc -O + assert_eq!(factorial(10), 3628800)

3. Same source, different backends

$ xpile transpile factorial.py --target ruchy
fun factorial(n: i64) -> i64 {
    if (n <= 1i64) { 1i64 } else {
        (n).checked_mul(factorial((n).checked_sub(1i64).expect("..."))).expect("...")
    }
}

$ xpile transpile factorial.py --target lean
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. Lean’s Int is unbounded, so C-PY-INT-ARITH is satisfied by construction — no overflow checks emitted, because there is no overflow.

4. Inspect the substrate

$ xpile info
$ xpile diamond     # if you're in a repo with contracts/
$ xpile quorum      # if you're in a repo with contracts/

See the CLI reference for everything xpile can do.

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        ✅ real emission
C        ─┤               ├─→ Ruchy       ✅ real emission
Shell    ─┤               ├─→ Shell       ✅ real emission (POSIX)
C++      ─┼→ meta-HIR ─→ ─┼─→ PTX         🚧 scaffold + Layer-5 contract
Rust     ─┤               ├─→ WGSL        🚧 scaffold
Ruchy    ─┤               ├─→ SPIR-V      🚧 planned
Lean 4   ─┘               └─→ Lean 4      🚧 scaffold

That is the code lane — runnable code in, runnable code out.

ContractFrontends             ContractBackends
─────────────────             ─────────────────
LaTeX       ─┐                  ┌─→ LaTeX (papers)
Lean 4 thm  ─┼─→ contracts ←──←─┼─→ Lean 4 theorems
mdBook      ─┘                  └─→ mdBook

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

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.

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.

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. At v0.1.0, all 12 contracts pass with 0 errors and 0 warnings.

The 5 layers

Every layer has both a code-lane and a proof-lane shadow. At v0.1.0 there are 12 contracts spanning all 5 layers; see the reference table for the full 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:

At v0.1.0:

$ xpile quorum
  ... (12 contracts, all at QUORUM)
  totals: 12 QUORUM, 0 PARTIAL, 0 UNVERIFIED (12 contracts total)

— 638 stratum-vote artifacts total (285 Semantic + 53 Symbolic + 15 Runtime + 285 Extrinsic).

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 MetaHirModule.”

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.

Eleven UNIVERSAL milestones (depth-3 through depth-13) have been achieved, each via a “broadening sweep” that extends a previously narrow-deep contract pattern out to the full 12-contract substrate.

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)

  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: 171 Diamond theorems across 12 contracts
  depth-1+..depth-13+: 12 contracts each (UNIVERSAL)
  depth-14+..depth-20+: 2 contracts each
  depth-21+: 1 contract

JSON output is available via xpile diamond --json and is parsed by the CI gate crates/xpile/tests/diamond_coverage.rs. The gate has 22 integration tests covering depth-1..depth-13 UNIVERSAL invariants — any regression fails the build.

What comes next

• Tutorial: Python → Rust — the complete C-PY-INT-ARITH story, from spec to emit.
• Reference: contracts — the 12-contract 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. Pins down the mismatch between Python’s unbounded int and Rust’s fixed-width i64, requiring .checked_*().expect(...) wrappers 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 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. The CI test is:

#![allow(unused)]
fn main() {
// crates/xpile/tests/transpile_e2e.rs (paraphrased)
#[test]
fn factorial_emitted_rust_computes_correct_values() {
    let rust = xpile_transpile("factorial.py", Target::Rust);
    let exe = compile_with_rustc_O(&rust);
    assert_eq!(exe.call("factorial", 10), 3628800);
}
}

Every PR runs this; the v0.1.0 release shipped with it green.

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"] attribute — 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.

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).

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 real Lean attribute. Not a comment. The C-XPILE-CONTRACT-BACKEND-TRAIT contract forbids regex-over-body citations and requires format-native structured constructs. In Lean that’s @[...]; in LaTeX it’s \xpileContract{...}{...}.
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. Pins down the idempotence invariant for the supported POSIX-shell subset and governs 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

The error message names the governing contract and suggests the correct target. This is the C-XPILE-BACKEND-TRAIT contract’s “structural compile-contract citation” invariant in action.

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 error paths and citation requirements.

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 (4):
    - python (py, pyi)
    - c (c, h)
    - ruchy (ruchy)
    - bashrs (sh, bash, zsh, mk)
  backends (6):
    - rust → Rust
    - ruchy → Ruchy
    - ptx → Ptx
    - wgsl → Wgsl
    - lean → Lean
    - bashrs → Shell

Proof lane:
  contract_frontends (1):
    - latex ← LatexMath
  contract_backends (2):
    - lean-theorem → LeanTheorem
    - latex → LatexMath

Use this to confirm your install can see every lane.

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, the error message names the governing contract and suggests the correct target — see the shell-roundtrip tutorial for an example.

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 — 22 integration tests ensuring depth-1..13 UNIVERSAL invariants don’t regress.

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 — fixtures under tests/fixtures/ mentioning the contract ID
• Extrinsic — roadmap work items mentioning the contract ID

A contract is QUORUM when ≥1 vote arrives from ≥3 strata. At v0.1.0 all 12 contracts are at QUORUM.

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 emitted functions that carry a // xpile-contract: <ID> citation.

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 contract pins down determinism (same input → same MetaHirModule) and the citation invariants the parsed module must carry.

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 at v0.1.0

Two more frontends ship as workspace members but live in the xpile-frontend shared trait crate:

• C++ — planned
• Rust — scaffold
• Lean 4 — scaffold (sub-spec: sub/lean-bidirectional.md)

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
• all binary operators (with Python-floor semantics for // and %)
• all unary operators
• ternary expressions
• if/elif/else chains
• function calls including self-recursion

Each emitted Rust/Ruchy/Lean function carries a // xpile-contract: C-PY-INT-ARITH citation for the arithmetic contract.

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

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::DepylerFrontend;
use xpile_frontend::Frontend;

let frontend = DepylerFrontend::default();
let module = frontend.parse_file("factorial.py")?;
// `module` is a `xpile_meta_hir::MetaHirModule`
}

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 contract pins down structural emit invariants: every emitted artifact must carry a // xpile-contract: <ID> citation, error paths must name the governing contract, and unsupported constructs must fail cleanly with a target-suggestion message.

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

Status at v0.1.0

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_euclid (Python-floor, not C-truncating)
  • % → checked_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

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 %
• @[xpile_contract "<ID>"] attribute above each emitted definition

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 of the three real backends.

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_rust_codegen::RustBackend;
use xpile_backend::Backend;
use xpile_meta_hir::MetaHirModule;

let backend = RustBackend::default();
let emitted = backend.emit_module(&module)?;
// `emitted` is a `xpile_backend::EmittedArtifact`
}

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

Error handling

When a backend cannot lower a particular construct it must fail with an error message that:

1. Names the construct (Stmt::Cmd, Expr::AwaitYield, etc.).
2. Names the governing contract (e.g. C-BASHRS-POSIX-IDEMPOTENCE).
3. Suggests the correct target if one exists (use --target shell).

This is the C-XPILE-BACKEND-TRAIT “structural compile-contract citation” invariant — see the contract reference.

Contracts at v0.1.0

All 12 contracts that ship at v0.1.0, in source order. Each row links to the contract YAML, its Lean theorems, and its Kani harness.

pv lint contracts/ → PASS, 0 errors and 0 warnings. xpile quorum → 12 QUORUM, 0 PARTIAL, 0 UNVERIFIED.

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

All Lean 4 constructs (def, partial, inductive, instance, axiom, …) lower to Rust. The inverse direction of the Python→Lean flow.

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 environments and theorem/lemma blocks lower to contract equations. Governs the bidirectional notation bridge between human-written math and machine-checked YAML equations.

C-XPILE-FRONTEND-TRAIT

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

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

C-XPILE-BACKEND-TRAIT

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

Every Backend emission must carry a structural contract citation (// xpile-contract: <ID>). Error paths must name the governing contract.

C-XPILE-CONTRACT-FRONTEND-TRAIT

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

Every ContractFrontend (LaTeX, mdBook, Lean) must produce a deterministic parse of its notation source into contract equations.

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.

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 at v0.1.0 ships as a scaffold; the contract holds the placeholder pinned down for the real implementation to discharge.

Adding a frontend

Governing contract: C-XPILE-FRONTEND-TRAIT — read this first. The trait’s structural invariants 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 xpile_frontend::{Frontend, FrontendError};
use xpile_meta_hir::MetaHirModule;

pub struct MyFrontend;

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

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

    fn parse_str(&self, source: &str, module_name: &str)
        -> Result<MetaHirModule, FrontendError>
    {
        // parse source → lower to meta-HIR
        todo!()
    }
}
}

Determinism is non-negotiable — the trait contract requires identical inputs to produce identical MetaHirModule 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 trait’s emit invariants (citation requirement, error-path-names-the-contract requirement, target-suggestion on unsupported constructs) are what your implementation must satisfy.

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, plan the error message — name the governing contract, suggest the right target.

The xpile-rust-codegen crate is the reference implementation; the shell rejection error (see shell-roundtrip tutorial) is what your error path should look like.

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::{Backend, BackendError, EmittedArtifact};
use xpile_meta_hir::MetaHirModule;

pub struct MyLangBackend;

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

    fn target_label(&self) -> &str { "MyLang" }

    fn emit_module(&self, module: &MetaHirModule)
        -> Result<EmittedArtifact, BackendError>
    {
        // 1. Begin with a provenance comment naming the backend +
        //    governing contract.
        // 2. Emit a `// xpile-contract: <ID>` citation per function.
        // 3. Lower meta-HIR statements.
        // 4. On unsupported constructs, return an error naming the
        //    construct, the governing contract, and the suggested
        //    target.
        todo!()
    }
}
}

The citation requirement is non-negotiable. The CI gate crates/xpile/tests/qa_gate.rs parses every emitted artifact and fails if a citation is missing.

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.