Part 3 — Python-Specific Verification

Parts 1 and 2 introduced Deppy's core type theory and proof system using features that have close analogues in F*, Lean, or Coq — refinement types, inductive datatypes, lemmas, and higher-order proofs. But Python is not F*. It is a dynamically-typed, duck-typed, mutable, metaprogrammable language, and any serious verification framework for Python must confront these realities head-on rather than pretending they don't exist.

This part is unique to Deppy. There is no equivalent section in the F* tutorial, because the problems we address here simply do not arise in statically-typed languages with nominal type systems. This is where Deppy's homotopy-theoretic foundation pays its largest dividends.

Why Python Needs Its Own Approach

Consider three features that every Python programmer uses daily but that make verification researchers reach for the aspirin:

Traditional approaches either forbid these features (too restrictive to be useful) or approximate them unsoundly (producing false negatives or false positives). Deppy takes a third path: we model each feature using the appropriate concept from cubical homotopy type theory.

The HoTT Correspondence

The key insight of Part 3 is that Python's "weird" features aren't bugs — they're features that correspond to well-understood mathematical structures:

What This Part Covers

This part contains six chapters, each devoted to one of the major Python-specific verification challenges:

Duck Typing & Protocols

We show how Python's structural subtyping via PEP 544 Protocol classes is modeled as path equivalence in HoTT. The DuckPath proof term lets you prove that a class conforms to a protocol without inheriting from it. We work through detailed examples including the Iterable protocol, file-like objects, and dynamic attribute resolution via __getattr__.

MRO & Descriptors

Python's two attribute-lookup mechanisms get complementary kernel encodings. C3 linearization compiles to a DuckPath through the class hierarchy; shared methods across overlapping bases form a Cocycle; super() chains via PathComp. The four-route descriptor protocol (data / instance / non-data / __getattr__) compiles to a 4-fibre Fiber; monkey-patching emits a Patch with a contract proof.

Operator Dispatch

The __r*__ fallback for binary operators (a + b tries a.__add__(b) first, then b.__radd__(a) on NotImplemented, with subclass priority overriding when type(b) subclasses type(a)) compiles to a ConditionalDuckPath. Subclass priority adds an outer Fiber over issubclass.

Coalgebras: Generators & Async

yield x compiles to EffectWitness("yield:N@epoch_M", Refl(value)); await e compiles to EffectWitness("await:e@epoch_M") followed by a resumption. g.send(v) and the await-resume both use TransportProof along the suspension path. g.close() is Sym: the inverse of the yield-path. Generators and coroutines are coalgebras of the same comonad.

Decorators & Metaprogramming

Python decorators are higher-order functions that transform functions or classes. We show how to prove that decorators preserve specifications and how metaclasses form fibrations over the class hierarchy. Case studies include a verified caching decorator and a verified retry decorator.

Dynamic Typing Verification

Python's runtime type system — isinstance, type(), gradual typing, Any, Union, TypeGuard — is modeled as a universe with decidable predicates. We show how to verify code that mixes typed and untyped regions, how monkey patching is sound when it preserves paths, and how runtime validation becomes proof obligation discharge.

Prerequisites

You should be comfortable with:

• Deppy refinement types and Z3 integration (Part 1)
• Basic familiarity with Python Protocols, decorators, and metaclasses
• The concept of path types from Part 2 (we'll review what we need)

Comparison with F*

To illustrate why this part is necessary, here's a quick comparison of how F* and Deppy handle a simple "is this thing iterable?" check:

// F*: must explicitly implement
noeq type iterable (a: Type) = {
  has_next : unit -> Tot bool;
  next     : unit -> Tot a;
}

// Every type must declare it
let my_list_iterable :
  iterable int = {
    has_next = ...;
    next     = ...;
  }

# Deppy: if you have the methods,
# you're iterable — prove it with a path
class Iterable(Protocol[T]):
    def __iter__(self) -> Iterator[T]: ...
    def __next__(self) -> T: ...

# MyList automatically satisfies it
# Deppy constructs DuckPath proof
@deppy.verify
class MyList:
    def __iter__(self): ...
    def __next__(self): ...

In F*, the relationship between a type and an interface is declared. In Deppy, the relationship is discovered and proved. This mirrors how Python actually works: you never declare that your class "implements" Iterable — you just provide the right methods, and Python's runtime (and mypy's checker) figure it out.

A Preview: The DuckPath

The central proof term of this part is DuckPath. Here's a taste of what it looks like:

from deppy.hott import DuckPath, PathType, transport

# Define a protocol
class Drawable(Protocol):
    def draw(self, canvas: Canvas) -> None: ...
    def bounding_box(self) -> Rect: ...

# A class that doesn't inherit from Drawable
class Circle:
    def __init__(self, center: Point, radius: float):
        self.center = center
        self.radius = radius

    def draw(self, canvas: Canvas) -> None:
        canvas.circle(self.center, self.radius)

    def bounding_box(self) -> Rect:
        return Rect(
            self.center.x - self.radius,
            self.center.y - self.radius,
            self.radius * 2, self.radius * 2
        )

# Deppy constructs this proof automatically:
proof : DuckPath[Circle, Drawable] = DuckPath.construct(
    # For each method in the protocol, show Circle has a matching one
    draw    = MethodPath(Circle.draw,    Drawable.draw,
                         sig_match=True, ret_compat=True),
    bounding_box = MethodPath(Circle.bounding_box, Drawable.bounding_box,
                              sig_match=True, ret_compat=True),
)
# proof.is_valid == True
# Circle is now verified as a Drawable ✅

The Verification Pipeline for Python

In this part, we'll see Deppy's verification pipeline handle Python-specific challenges at each stage:

Running the Examples

All examples in Part 3 require the Deppy runtime with Z3 support:

# Install Deppy with Z3 backend
pip install git+https://github.com/thehalleyyoung/deppy.git
pip install z3-solver

# Verify a sidecar (works for any module structure)
python -m deppy.pipeline.run_verify drawing.deppy --out drawing.lean

# Or for the decorator form
python -m deppy.pipeline.run_verify --from-module drawing --out drawing.lean

# Example output (truncated):
$ python -m deppy.pipeline.run_verify drawing.deppy --out drawing.lean
  ProofTerm subclasses (C1–C7 audit batch):
    constructed / kernel-accepted:         N / N
  ──────────────────────────────────────────
  deppy.lean.lean_runner round-trip:       OK
  ──────────────────────────────────────────
  ✓ CERTIFIED — top-level certify_or_die: PASS

Mathematical Foundations

For readers interested in the theory, here's the formal statement of the main theorem underlying Part 3:

Theorem (Duck Typing Soundness). Let P be a Protocol with methods m₁, …, mₖ and let C be a class. If for each mᵢ there exists a method C.mᵢ with a compatible signature (covariant return, contravariant arguments), then there exists a path p : C =_{Protocol} P in the protocol universe, and for any property Φ verified against P, we have transport(p, Φ) : Φ(C).

This theorem is proved in Deppy's core library using cubical Agda as the metalanguage, with Z3 handling the signature compatibility checks. The practical consequence: if you verify your code against a Protocol, and a new class satisfies that Protocol, the verification transfers automatically.