Part 4 — Sidecar Proofs

Verify existing Python libraries without modifying a single line of their source code.

The Problem

Most real Python code depends on third-party libraries. When you import numpy, sympy, or torch, you're importing hundreds of thousands of lines of code that you cannot modify. Traditional verification systems face a hard choice:

• Ignore libraries — treat every external call as a black box, losing the ability to reason about most of your program.
• Rewrite everything — port the library into the verification language (impractical for anything beyond toy examples).
• Require source annotations — like F*, which needs val specifications inside the library source. You can't do this for pip install numpy.

Deppy takes a fourth path: sidecar proofs.

The Sidecar Philosophy

A sidecar is a separate file that rides alongside the library it describes — just like a motorcycle sidecar. The library runs unmodified; the sidecar provides the formal specifications.

How It Works

For any module foo, you create a companion file foo.deppy. This file contains:

1. Type specifications — refined types for function parameters and return values.
2. Preconditions — what must be true before calling a function.
3. Postconditions — what the function guarantees.
4. Algebraic laws — properties like commutativity, associativity, or idempotence that the library's operations satisfy.
5. Trust level — how much you trust each specification (from LEAN_KERNEL_VERIFIED to UNTRUSTED).

# math.deppy — sidecar specs for Python's math module
module: math

foundation Real_sqrt_nonneg: "sqrt(x) >= 0 when x >= 0"
foundation Real_sqrt_sq: "sqrt(x)**2 == x when x >= 0"

spec math.sqrt:
  guarantee: "math.sqrt(x) is defined and non-negative when x >= 0"
  pure: true
  axiom sqrt_nonneg: "math.sqrt(x) >= 0 when x >= 0"
  axiom sqrt_inverse: "math.sqrt(x)**2 == x when x >= 0"

Equivalently, when you own the calling code, you can use the decorator form (see next chapter):

from deppy.sidecar import about, ExternalSpec, law

@about("math.sqrt")
class SqrtSpec(ExternalSpec):
    @law
    def nonneg(self, x: float) -> bool:
        """math.sqrt(x) >= 0 when x >= 0."""
        if x < 0: return True
        return self.call(x) >= 0

The @about Decorator

The @about decorator is the key mechanism. It binds a specification class to an external function or class by its fully qualified name — the library code is never touched.

@about("collections.OrderedDict.popitem")
class PopItemSpec(ExternalSpec):
    """popitem(last=True) returns the last-inserted key-value pair."""

    @law
    def returns_pair(self, d: OrderedDict) -> bool:
        # Each ``@law`` is a runtime-checkable claim about the live
        # target.  It also becomes a sidecar axiom in the kernel.
        if len(d) == 0: return True
        result = self.call(d)
        return isinstance(result, tuple) and len(result) == 2

Deppy resolves the dotted name at verification time, matches it to the installed library, and checks every call site in your code against the spec.

Trust Levels (Preview)

Not all specifications carry the same weight. Deppy tracks trust along two parallel lattices: a 7-element deppy-kernel lattice (TrustLevel) and a 6-element Lean-export lattice (LeanTrustLevel). This preview shows the most commonly-cited rungs of each — see Trust & Verification Levels for the full list.

Trust propagates through dependencies: if function A calls function B, then A's trust level can never exceed B's. We'll explore this in detail in Trust & Verification Levels.

Gradual Verification

Sidecar proofs enable gradual verification — you don't have to specify everything at once. Start with the functions that matter most:

Comparison with Other Systems

// F*: must add specs INSIDE the module
val sqrt: x:float{x >= 0.0}
         -> y:float{y >= 0.0
                /\ y *. y ≈ x}
let sqrt x = // implementation here
  // ← Can't do this for pip packages!

# math.deppy — lives BESIDE the library
module: math

foundation Real_sqrt_nonneg: "sqrt(x) >= 0 when x >= 0"

spec math.sqrt:
  guarantee: "non-negative output when input >= 0"
  pure: true
  axiom sqrt_nonneg: "math.sqrt(x) >= 0 when x >= 0"
  # ← Library stays untouched!

Anatomy of a .deppy File

Every sidecar file follows a consistent structure. Here is the complete anatomy:

# ─── Header: identify the target module ───
# filename: numpy_linalg.deppy
module: numpy
version: ">=1.24,<3"

# ─── Foundations: generic mathematical facts ───
foundation Linear_solve_unique: "A·x == b has at most one solution when det(A) != 0"

# ─── Spec block: one per target function/method ───
spec numpy.linalg.solve:
  guarantee: "A @ solve(A, b) ≈ b when A is square and non-singular"
  pure: true
  axiom solve_inverts: "numpy.allclose(A @ numpy.linalg.solve(A, b), b)"
  axiom solve_unique: "numpy.linalg.solve(A, b) is independent of run"

verify hypotenuse_solve_safe:
  function: my_module.hypotenuse_solve
  property: "my_module.hypotenuse_solve(A, b) is non-empty"
  via: "foundation Linear_solve_unique"

The key design principles:

• Foundations are generic mathematical facts that you trust as axioms (the system can also discharge many of them via Z3).
• Axioms inside a spec are formal claims about the live target — Deppy parses each statement as a Python expression and resolves its referenced attributes against the actual class or module.
• Verify blocks are theorems that have to be discharged from foundations + axioms via the proof kernel (PSDL bodies, citation, chain, rewrite-then-cite).
• Version pinning — sidecars declare version: … so API changes don't silently break your specs.

How Sidecar Verification Works

When you run python -m deppy.pipeline.run_verify, the pipeline (in deppy.lean.sidecar_runner) performs these steps:

Why Not Just Modify the Source?

Some verification systems require annotations inside the source code. This doesn't work for the Python ecosystem:

The sidecar approach extends Python's existing .pyi stub file convention — but adds preconditions, postconditions, algebraic laws, trust levels, and verification support.

What You'll Learn in Part 4

1. Sidecar Basics — Creating .deppy files, the @about decorator, ExternalSpec, and verifying specs for math and collections.
2. Case Study: SymPy — A full sidecar verification of SymPy's algebraic, matrix, and calculus modules. Using homotopy to transport properties between symbolic and numerical computation.
3. Trust & Verification Levels — The four trust levels, trust propagation, gradual verification, CI integration, and the trust dashboard.

Quick Example: Verifying Your Code Against a Sidecar

Suppose your project uses math.sqrt. Here's the full workflow:

# my_geometry.py — YOUR code
import math

def circle_area(radius: float) -> float:
    """Compute area of a circle. Radius must be non-negative."""
    assert radius >= 0
    return math.pi * radius * radius

def hypotenuse(a: float, b: float) -> float:
    """Compute hypotenuse. a, b must be non-negative."""
    assert a >= 0 and b >= 0
    return math.sqrt(a * a + b * b)
    # ↑ Deppy checks: a*a + b*b >= 0 (sqrt precondition)
    #   This is automatically discharged by Z3!

Running verification:

$ python -m deppy.pipeline.run_verify math.deppy --out math.lean

════════════════════════════════════════════════════════════════════════
  Deppy sidecar verification report
  Sidecar:  math.deppy
  Library:  math (built-in) — Python ≥3.10
  Output:   math.lean
────────────────────────────────────────────────────────────────────────
  foundations:                       (axioms about real arithmetic)
  spec(s) bound:        math.sqrt
  axiom(s):             sqrt_nonneg, sqrt_inverse_when_nonneg
  verify block(s):      hypotenuse_nonneg
    PSDL → kernel ProofTerm:         OK
    Lean export round-trip:          OK
────────────────────────────────────────────────────────────────────────
  ✓ CERTIFIED — top-level certify_or_die: PASS

Counts and trust badges in the report come from the section_counters dict written to math.json alongside the Lean output — see Lean Export for the full schema.