Skip to content

verification.md

Latest commit

 

History

History
140 lines (106 loc) · 5 KB

verification.md

File metadata and controls

140 lines (106 loc) · 5 KB
Raw

Verification

Static Python supports two verification backends:

  1. Theorem provers (Lean) — transpile with --lean and let Lean prove correctness at compile time. Theorems are discharged with tactics such as native_decide and omega; lake build succeeding means the proof checked.
  2. SMT solvers (z3) — transpile with --smt to an SMT-LIB query and check it with z3.

Both backends read the same specification markers from the source. The markers are compiled out at runtime (every if condition is a constant False), so a verified file is also ordinary runnable Python.

Specification markers

Prefer the CHECKER namespace from py2many.spec:

from py2many.spec import CHECKER

def deposit(self, amount: int) -> "BankAccount":
    if CHECKER.pre:
        amount > 0
    if CHECKER.post:
        result.balance == self.balance + amount
    return BankAccount(self.balance + amount)
  • CHECKER.pre — precondition. Becomes a proof parameter on the emitted function/def.
  • CHECKER.post — postcondition. Becomes a constraint on the return value.
  • CHECKER.invariant — class invariant. Becomes a structure field of proposition type (e.g. balance >= 0 → inv_balance : balance ≥ 0).

The older flat names (smt.pre, smt.post, smt.invariant) remain exported for backward compatibility.

The theorem-prover backends also accept decorator markers from py2many.theorem:

from py2many.theorem import theorem, lemma, by

@lemma
@by("native_decide")
def sqrt_of_9() -> bool:
    return safe_sqrt(9) == 3
  • @theorem / @lemma emit theorem instead of def in Lean.
  • @by("tactic") supplies the proof block (native_decide, omega, ...).
  • The body should be a single return <expr> stating the property to prove (it is emitted as <expr> = true).

These decorators are no-ops at runtime, so the file still executes in plain Python.

Theorem-prover flow (Lean)

uvx py2many --lean test.py
lake build

If lake build exits 0, every theorem was proved (native_decide evaluated the claim, omega closed the arithmetic goal, ...). A failing theorem fails the build with a traceback of the unclosed goal.

SMT flow (z3)

uvx py2many --smt test.py - | z3 -smt2 -in

If the result is UNSAT and there is a counter example, fix it before continuing.

End-to-end flow

The two roles can be split across targets from one source. For example, a sort is transpiled to Lean (for formal verification) and Rust (for native execution) from the same file:

                   ┌─── py2many --lean ──▶  .lean  ──▶  lake build ──▶ yes/no
verified_sort.py ──┤
                   └─── py2many --rust ──▶  .rs    ──▶  cargo run  ──▶ output
Target Role Signal
Lean Verification — theorems proved by native_decide lake build exit 0 = proved
Rust Execution — run the algorithm at full speed cargo run exit 0 = correct for test input

The CHECKER blocks are handled by Lean and stripped by the other backends, so the executable Rust output contains no verification artifacts.

Convenience runners (single-file tests)

py2many/scripts/ ships two runners that set up the environment needed to build and run a single generated file, so you don't have to scaffold a lake project or Cargo project by hand. Each takes an optional mode and the generated source file (plus any program arguments for run).

lean-runner.sh — build/run one generated .lean file through lake build:

# verify only (a successful build IS the proof)
MISE_ENV=lean mise exec -- lean-runner.sh build sorted.lean

# build then execute the binary
MISE_ENV=lean mise exec -- lean-runner.sh run sorted.lean
  • It copies the file to a fresh temp lake project (Main.lean), builds it, and (in run mode) executes .lake/build/bin/verify. A private per-TMPDIR project means concurrent runs don't clobber a shared Main.lean/.lake.
  • Build noise goes to stderr so stdout carries only the program's own output.
  • lean/lake come from the http:lean mise tool (MISE_ENV=lean), so it is invoked under MISE_ENV=lean mise exec -- ....
  • lake build succeeding means the file type-checks, i.e. its pre/post conditions and invariants hold — the Lean analogue of py2many --smt file.py | z3 -smt2 -in reporting no counter-example.

rust-runner.sh — compile/run one generated .rs file:

rust-runner.sh compile sorted.rs    # cargo build only
rust-runner.sh lint   sorted.rs     # cargo clippy
rust-runner.sh run    sorted.rs     # cargo run (default)
  • It creates/reuses a common-rust-proj Cargo binary, fills Cargo.toml from a cargo ....... block embedded in the doc comment of the generated Rust file (stripping the //! prefix), and copies the file to src/main.rs.
  • MODE is the first argument (compile | lint | default run); remaining args go to the built executable in run mode.