Čech Decomposition

Verify branching code by decomposing it into patches, proving each patch independently, and gluing local proofs into a global guarantee.

What Is Čech Cohomology?

Imagine you want to verify that a painted canvas is entirely blue. The canvas is too large to inspect all at once, so you cover it with overlapping magnifying lenses — each lens shows a small region. You check that each region is blue. On the overlaps (where two lenses see the same area), you check that they agree. If every region is blue and the overlaps are consistent, you conclude the entire canvas is blue.

That's Čech cohomology in a nutshell. The canvas is your function's input domain. The lenses are your function's branches (if/elif/else). The property "is blue" is your postcondition. The overlap check is the gluing condition. And the conclusion — "the whole canvas is blue" — is your @guarantee.

Čech decomposition turns one hard global proof into many easy local proofs plus a consistency check.

The Čech Cover

A Čech cover of a function is a collection of patches {U₁, U₂, …, Uₙ} that together cover the entire input domain. Each patch corresponds to one branch of the function.

# Python function with three branches
def classify(x: int) -> str:
    if x < 0:
        return "negative"     # Patch U₁: { x | x < 0 }
    elif x == 0:
        return "zero"         # Patch U₂: { x | x = 0 }
    else:
        return "positive"     # Patch U₃: { x | x > 0 }

# Cover: U₁ ∪ U₂ ∪ U₃ = ℤ  (all integers)  ✓
# Pairwise overlaps: U₁ ∩ U₂ = ∅, U₂ ∩ U₃ = ∅, U₁ ∩ U₃ = ∅
# No overlaps to check → trivial gluing

Deppy automatically extracts the cover from the Python AST. Each if/elif/else condition defines a patch. match/case patterns define patches. try/except blocks define patches (normal execution vs. exception paths).

Why Branching Code Is Hard

The fundamental difficulty of verifying branching code is that you must reason about all paths simultaneously. A function with 5 branches has 5 possible execution paths, and the interactions between them can be subtle. Without Čech decomposition, you'd need a single monolithic proof that handles all cases.

With Čech decomposition, you:

1. Decompose the function body into patches (one per branch).
2. Verify each patch independently using Z3 or other solvers.
3. Check agreement on overlaps (where two branches could both apply).
4. Glue the local proofs into a global proof via CechGlue.

The Čech Verification Algorithm

Here is the full algorithm, step by step:

patches = extract_patches(function_ast)
# [Patch(guard=x<0, body=...), Patch(guard=x==0, body=...), ...]

z3_check(Not(Or(*[p.guard for p in patches])))
# Must be UNSAT → patches cover everything

for patch in patches:
    local_proof = verify(
        assume=patch.guard,
        body=patch.body,
        postcondition=guarantee
    )

for i, j in pairs(patches):
    overlap = And(patches[i].guard, patches[j].guard)
    if z3_sat(overlap):  # overlap is non-empty
        verify_agreement(patches[i].body, patches[j].body, overlap)

global_proof = CechGlue(local_proofs, overlap_proofs)
# global_proof : ∀x. guarantee(f(x))

Example: Piecewise Function Verification

from deppy import guarantee

@guarantee("returns a string describing the sign of x")
def classify(x: int) -> str:
    if x < 0:
        return "negative"
    elif x == 0:
        return "zero"
    else:
        return "positive"

Example: Exception Handling as Čech Cover

One of Deppy's most powerful insights is that try/except blocks are also Čech covers. The "try" body is one patch, and each except handler is another. Together they cover all possible execution paths.

from deppy import guarantee

@guarantee("returns a / b if b != 0, else returns float('inf')")
def safe_divide(a: float, b: float) -> float:
    try:
        return a / b               # Patch U₁: normal execution (b ≠ 0)
    except ZeroDivisionError:
        return float('inf')       # Patch U₂: exception path (b = 0)

Overlapping Branches

The most interesting (and most important) case is when branches overlap — when an input could trigger multiple branches. This happens more often than you might think:

@guarantee("returns max(a, b)")
def maximum(a: int, b: int) -> int:
    if a >= b:
        return a       # Patch U₁: { (a,b) | a ≥ b }
    else:
        return b       # Patch U₂: { (a,b) | a < b }

Here U₁ ∩ U₂ = ∅ because a ≥ b and a < b are mutually exclusive. But consider a variant:

@guarantee("returns max(a, b)")
def maximum_v2(a: int, b: int) -> int:
    if a >= b:
        return a       # Patch U₁: { (a,b) | a ≥ b }
    if b >= a:
        return b       # Patch U₂: { (a,b) | b ≥ a }

Now U₁ ∩ U₂ = {(a,b) | a = b} is non-empty. On the overlap, the first branch returns a and the second returns b. Since a = b on the overlap, both branches return the same value. The gluing condition is satisfied.

# Gluing check for maximum_v2
# On U₁ ∩ U₂ = {a = b}: branch 1 returns a, branch 2 returns b
# Need: a = b on the overlap
# Z3 query: a ≥ b ∧ b ≥ a → a = b  ...  VALID ✓
# Gluing condition satisfied!

Match/Case as Čech Cover

Python 3.10's structural pattern matching maps perfectly to Čech covers:

from deppy import guarantee

@guarantee("returns the area of the shape")
def area(shape: Shape) -> float:
    match shape:
        case Circle(r):                  # U₁
            return 3.14159 * r * r
        case Rectangle(w, h):             # U₂
            return w * h
        case Triangle(base, height):       # U₃
            return 0.5 * base * height
        case _:                            # U₄ (wildcard)
            raise ValueError("Unknown shape")

# Each case arm is a patch.
# The wildcard case _ catches everything not matched above.
# Coverage: U₁ ∪ U₂ ∪ U₃ ∪ U₄ = all Shape instances  ✓
# Overlaps: pattern matching is sequential → no overlap

Deppy treats match/case as a special Čech cover where the patches are ordered (first match wins), which means there are no overlaps to check — each case excludes all previous patterns.

Example: Proving Equivalence of Two Branching Functions

# Version 1: traditional if/elif
@guarantee("returns the grade letter for a score")
def grade_v1(score: int) -> str:
    if score >= 90: return "A"
    elif score >= 80: return "B"
    elif score >= 70: return "C"
    elif score >= 60: return "D"
    else: return "F"

# Version 2: dictionary lookup
@guarantee("returns the grade letter for a score")
def grade_v2(score: int) -> str:
    thresholds = [(90, "A"), (80, "B"), (70, "C"), (60, "D")]
    for threshold, letter in thresholds:
        if score >= threshold:
            return letter
    return "F"

To prove these equivalent, Deppy:

1. Čech-decomposes grade_v1 into 5 patches (one per branch).
2. Čech-decomposes grade_v2 into 5 patches (loop unrolling + final return).
3. Constructs a refinement of the two covers: a common cover where each patch of one function corresponds to a patch of the other.
4. On each patch of the common cover, checks that both functions return the same result.
5. Applies FunExt to conclude grade_v1 = grade_v2.

H¹ Obstruction: When Proofs Can't Be Glued

Not every collection of local proofs can be glued into a global proof. When they can't, the obstruction lives in H¹ — the first Čech cohomology group. This is the mathematical name for "the local proofs are inconsistent on overlaps."

# This function has an H¹ obstruction — it CANNOT be verified!

@guarantee("returns a consistent ordering of items")
def broken_sort(xs: list[int]) -> list[int]:
    if len(xs) <= 2:
        return sorted(xs)                 # U₁: len ≤ 2 → correct
    elif len(xs) <= 5:
        return sorted(xs, reverse=True)  # U₂: 3 ≤ len ≤ 5 → DESCENDING!
    else:
        return sorted(xs)                 # U₃: len > 5 → correct

Connection to Sheaf Theory

The Čech decomposition is an instance of sheaf theory — one of the most beautiful areas of modern mathematics. Here is how the correspondence works:

The sheaf condition says that local data can be glued into global data whenever it agrees on overlaps. In Deppy, the "data" is proof terms, and the sheaf condition becomes: local proofs can be glued into a global proof whenever they are consistent on overlapping branches.

Presheaf of Properties over Execution Paths

For each open set U in the input domain, we assign the set of all properties that are verified on U. This gives a presheaf — a functor from open sets to properties. The presheaf is a sheaf if and only if properties that hold locally (on every patch) and agree on overlaps also hold globally.

# Presheaf of properties
# F(U) = { P | P is verified for all inputs in U }

# For classify():
# F(U₁) = { "returns 'negative'" }   — verified on x < 0
# F(U₂) = { "returns 'zero'" }       — verified on x = 0
# F(U₃) = { "returns 'positive'" }   — verified on x > 0
#
# Sheaf condition: these local properties glue to
# F(ℤ) = { "returns correct sign description" }
# because they are consistent on overlaps (which are empty)

Nested Branching & Higher Čech

Real Python code often has nested branching — an if inside an if, a try/except inside a match/case, etc. Deppy handles this via iterated Čech decomposition: decompose the outer branches first, then decompose each inner branch.

@guarantee("returns a formatted string for the HTTP response")
def format_response(status: int, body: str) -> str:
    if status >= 200 and status < 300:           # Outer U₁: success
        if body:                                  # Inner U₁₁: has body
            return f"OK: {body}"
        else:                                     # Inner U₁₂: no body
            return "OK: (empty)"
    elif status >= 400 and status < 500:        # Outer U₂: client error
        return f"Client Error {status}: {body}"
    else:                                        # Outer U₃: other
        return f"Status {status}: {body}"

# Decomposition tree:
# ├─ U₁ (200 ≤ status < 300)
# │   ├─ U₁₁ (body non-empty)
# │   └─ U₁₂ (body empty)
# ├─ U₂ (400 ≤ status < 500)
# └─ U₃ (everything else)

The nested structure forms a tree of covers. Deppy verifies bottom-up: inner branches first, then glue to verify outer branches, then glue again for the global proof.

The CechGlue Proof Term

CechGlue is the proof term that combines local proofs into a global proof. Here is its formal signature:

# deppy.core.kernel.CechGlue (the real dataclass):
class CechGlue(ProofTerm):
    patches:        list[tuple[str, ProofTerm]]
    overlap_proofs: list[tuple[int, int, ProofTerm]]

# Each patch is ``(condition_string, local_proof)``.
# Each overlap is ``(i, j, agreement_proof)`` — only listed
# when patch[i] and patch[j] actually intersect on the input
# domain.  The kernel verifies:
#   1. ∪ patches = Domain (open cover obligation)
#   2. Each local_proof is itself kernel-checkable
#   3. For each ``(i, j, ag)``: ag witnesses that the local
#      proofs agree on the overlap (cocycle condition).

# The user-facing wrapper smooths over a few list shapes:
from deppy import cech_glue
glue = cech_glue(
    [("x < 0", neg_proof),
     ("x == 0", zero_proof),
     ("x > 0", pos_proof)],
    overlap_proofs=[],   # disjoint patches → no overlaps
)

The output is a single proof term that you can think of as: "for any input x, find which patch x belongs to and apply the corresponding local proof." The gluing proofs ensure that the choice of patch doesn't matter when x is in an overlap.

def sign(x: int) -> int:
    if x > 0: return 1
    if x < 0: return -1
    if x >= 0: return 0 if x == 0 else 1
    return 0