Part 2 — Advanced Proofs

Inductive types, dependent data structures, and the foundations of homotopy verification in Python.

What You'll Learn

Part 1 gave you the tools to write verified Python with refinement types and Z3. In Part 2, we go deeper: you'll use Python's Generic type system, dataclass-based inductive types, and Deppy's homotopy constructs to build programs whose correctness is guaranteed at a much richer level.

Where F*'s Part 2 introduces inductive types and dependent pattern matching, Deppy maps those ideas onto Python idioms — generics, dataclasses, protocols — and extends them with path types and cubical constructions that let you reason about equality of behaviour, not just equality of values.

Chapters at a Glance

Prerequisites

• Comfortable with all Part 1 chapters (refinement types, Z3, lemmas).
• Familiarity with Python generics (typing.Generic, TypeVar).
• Basic understanding of algebraic data types (tagged unions / sum types).

How This Differs from F*

F*'s Part 2 introduces inductive types with ML-style type declarations and dependent pattern matching. Deppy achieves the same expressive power through:

• Dataclasses as constructors — each @dataclass variant is an inductive constructor; match statements provide exhaustive pattern matching.
• Generics as universe-polymorphic types — Python's Generic[T] corresponds to F*'s implicit type parameters.
• Path types for equality — where F* uses propositional equality (==), Deppy can additionally use path types to prove behavioural equivalence of Python objects that may have different internal representations.
• Z3 + sidecar proofs — arithmetic obligations are discharged to Z3 automatically; complex domain proofs live in sidecar .deppy files (or in @verify / @psdl_proof decorators when you own the module).

type vec (a:Type) : nat -> Type =
  | Nil  : vec a 0
  | Cons : a -> vec a n
          -> vec a (n+1)

from __future__ import annotations

@dataclass(frozen=True)
class Vec(Generic[T, N]):
    # length encoded at the type level
    items: tuple[T, ...]
    # refined: len(items) == N

Running the Examples

Every code snippet in Part 2 can be verified with:

# Verify a single file
$ python -m deppy.pipeline.run_verify part2/vectors_example.py

# Run the test suite for this part
$ python -m pytest tests/test_part2/ -v

Inductive Types in Python

In F*, inductive types are declared with the type keyword. In Python, we build the same structures from @dataclass and Union:

from __future__ import annotations
from dataclasses import dataclass
from typing import Union, Generic, TypeVar

T = TypeVar('T')

# An inductive list: either Nil or Cons(head, tail)
@dataclass(frozen=True)
class Nil(Generic[T]):
    pass

@dataclass(frozen=True)
class Cons(Generic[T]):
    head: T
    tail: List[T]

List = Union[Nil[T], Cons[T]]

# Pattern matching with Python 3.10+ match/case
def length(lst: List[T]) -> int:
    match lst:
        case Nil():       return 0
        case Cons(_, tl): return 1 + length(tl)

Each @dataclass variant acts as a constructor; Python's match statement gives exhaustive pattern matching. Deppy verifies that all cases are covered and that recursive calls terminate.

Verification Levels in Part 2

Different chapters exercise different verification strategies:

A Roadmap

The chapters are designed to be read in order, but you can skip ahead if a topic interests you. The dependency graph is:

generics ──→ vectors ──→ merkle
                            │
          equality_types ◄──┘
               │
          connectives ──→ stlc

Equality & Path Types is the conceptual centrepiece — it connects the purely Pythonic material (generics, vectors, Merkle trees) with the homotopy foundations (connectives, STLC) that make Deppy unique.