Skip to content

xpile v0.1.1 — Python types lane increment

Choose a tag to compare

@noahgift noahgift released this 22 May 06:06
· 589 commits to main since this release
cf9af3d

xpile v0.1.1 — Python types lane increment

Incremental release on top of v0.1.0. Adds the Python types lanestr, list[T], and dict[K, V] foundation — without touching the v0.1.0 substrate.

Install

cargo install xpile

All 27 workspace crates published at v0.1.1 on crates.io.

What's new

str lane (PMAT-449..454)

def greet(name: str) -> str:
    return f"Hello, {name}!"

Contract C-XLATE-PY-STR-TO-RUST-STRING at QUORUM, depth-13 UNIVERSAL with all 13 Diamond categories wired (Templates 1, 2, 6, 6b, 6c, 9, 10, 11, 12, 13).

list[T] lane (PMAT-455..461)

def reverse_in_place(xs: list[int]) -> int:
    i = 0
    j = len(xs) - 1
    while i < j:
        tmp = xs[i]
        xs[i] = xs[j]
        xs[j] = tmp
        i = i + 1
        j = j - 1
    return len(xs)
  • Element types: list[int], list[str], list[bool], nested list[list[int]].
  • Operations: indexed access xs[i], indexed assignment xs[i] = v, iteration for x in xs:, len(xs), xs.append(v).
  • Automatic param-mut threading: xs.append(v) or xs[i] = v marks xs as mut Vec<T> in emitted Rust.

dict[K, V] foundation (PMAT-462)

def counts() -> dict[str, int]:
    return {"alice": 1, "bob": 2, "carol": 3}
  • Rust: HashMap<K, V> block expression.
  • Lean: List (K × V) first cut (Std.HashMap encoding deferred to v0.3.0).

Substrate state

Unchanged from v0.1.0:

  • 13 contracts at QUORUM (xpile quorum).
  • 184 Diamond theorems across 13 contracts (xpile diamond).
  • Depth-13 UNIVERSAL strict-equality CI gate (22 tests in diamond_coverage.rs).
  • 638 stratum-vote artifacts (Lean + Kani + Runtime + Extrinsic).

Deferred to v0.2.0

  • Dict operations: d[k], d[k] = v, len(d), for k in d:, k in d.
  • Lean iteration / mutation (Stmt::ForEach, Stmt::ListAppend, Stmt::IndexAssign refuse in Lean backend).
  • list.extend(), .insert(), .pop(), slicing xs[a:b].
  • float type, negative-index wrap (xs[-1]).
  • Track 2 — decy real C frontend merger.
  • Track 3 — bashrs check-back option (c) Lean composition idempotence theorem.

Links