Core Concepts

1. The Central Idea

Classical proof theory assigns proofs a term structure: a derivation tree whose nodes are inference rules. JuGeo takes a different stance. A proof obligation over a piece of code is not a single term — it is a geometric object living at a coordinate in the program's semantic space. When the program evolves, the obligation transforms. When the program branches, the obligation splits. This is the language of sheaves.

The key operations on judgments mirror those on sheaf sections:

• Restriction \(J|_U\): project a judgment to a sub-coordinate \(U \hookrightarrow c\).
• Gluing \(\mathrm{glue}(J_1, \ldots, J_n)\): assemble compatible local judgments into a global one.
• Transport \(f^* J\): pull back a judgment along a morphism \(f : c' \to c\) (inlining, specialization).
• Challenge \(\partial J\): lower the trust level and require re-verification.
• Escalate \(\uparrow J\): route to a higher-authority channel for re-evaluation.

2. Semantic Sites

A semantic site is a small category \(\mathcal{S}_P\) equipped with a Grothendieck topology \(J_P\). The objects of \(\mathcal{S}_P\) are the coordinates of program \(P\); the morphisms model how one coordinate relates to another via scope nesting, control flow, or module inclusion. The topology specifies which families of morphisms constitute covers — enough local data to reconstruct global behavior.

Objects — Program Coordinates

A coordinate is any syntactically delimited region of \(P\). The taxonomy is:

Morphisms — Four Primitive Relations

Covering Families — The Grothendieck Topology

A family \(\{f_i : U_i \to U\}_{i \in I}\) is a covering sieve of \(U\) in \(J_P\) when it belongs to one of four standard generating classes:

The Grothendieck Axioms

The covering sieves must satisfy three axioms to form a Grothendieck topology on \(\mathcal{S}_P\):

The Sheaf Condition on Specification Functors

A specification functor \(\mathcal{F} : \mathcal{S}_P^{\mathrm{op}} \to \mathbf{Set}\) assigns to each coordinate a set of local specifications. It is a sheaf (equivalently: local specifications glue to global ones) iff the following equalizer diagram is exact for every covering sieve \(\{U_i \to U\}\):

In plain terms: a collection of local specifications \(\{s_i \in \mathcal{F}(U_i)\}\) that agree on all pairwise overlaps \(U_i \times_U U_j\) is the restriction of a unique global specification \(s \in \mathcal{F}(U)\). This is exactly what program verification needs: branch-level postconditions that agree on shared state glue into a function-level postcondition.

from jugeo.geometry.site import Coordinate, CoordinateKind, build_site

base = Coordinate(("mypackage",), CoordinateKind.MODULE)
parse_fn = Coordinate(("mypackage", "parse"), CoordinateKind.FUNCTION)
site = build_site([base, parse_fn])

print(site.coordinate_count())
print(site.morphism_count())
print([obj.name for obj in site.objects()])

3. Sheaf Descent

Descent is the process of assembling a global judgment from a compatible family of local judgments. Given a covering family \(\{U_i \to U\}_{i \in I}\) and local judgments \(J_i\) on each \(U_i\), descent asks: do the \(J_i\) agree on all pairwise overlaps, and if so, is there a unique global \(J\) restricting to each \(J_i\)?

Diagram: Descent for a Branching Function

Four Descent Strategies

JuGeo implements four strategies for orchestrating the descent computation, trading off coverage guarantees against resource consumption:

from jugeo.geometry.descent import DescentEngine, DescentStrategy

engine = DescentEngine()
print(type(engine).__name__)
print([strategy.name for strategy in DescentStrategy])

4. The Trust Algebra

Not all evidence is equal. A runtime test witnessing a property once is less reliable than a formal proof that holds for all inputs. JuGeo makes this precise with a trust algebra — a partially ordered monoid with operations for combining, promoting, and challenging trust annotations.

The Seven Trust Levels

Algebra Operations

Conservative Join \(\oplus\)

Combining two trust levels yields the minimum — trust is only as strong as the weakest link:

Promotion \(\uparrow_\pi\)

Promotion upgrades trust when a new evidence object \(\pi\) is provided. Promotion is bounded by the trust ceiling of the channel that produced \(\pi\):

Demotion \(\downarrow_\chi\)

When a challenge \(\chi\) (a counter-example candidate, a failing test, a conflicting oracle report) is issued against a judgment at trust level \(T\):

The Three Laws

from jugeo.evidence.trust import TrustLevel, TrustAlgebra

T = TrustAlgebra()
combined = T.join(TrustLevel.RUNTIME_WITNESSED, TrustLevel.SOLVER_DISCHARGED)
print(combined)
print(T.promote(TrustLevel.COPILOT_SUGGESTED, "solver witness"))
print(T.demote(TrustLevel.SOLVER_DISCHARGED, TrustLevel.RUNTIME_WITNESSED))

5. Evidence Channels

An evidence channel is a named source of proof evidence, equipped with a jurisdiction (the class of properties it can handle), a trust ceiling (the maximum trust level it can award), and a cost model. JuGeo ships six built-in channels and supports third-party channel plugins.

Channel Routing

JuGeo's router maps each formula \(\varphi\) to the cheapest channel whose jurisdiction contains \(\varphi\) and whose trust ceiling meets the required trust level:

6. Cohomological Obstructions

When descent fails — when local judgments do not agree on overlaps — the failure is not discarded. Instead it is captured as a cohomological obstruction: an element of a sheaf cohomology group \(H^n(\mathcal{S}_P;\, \mathcal{F}_J)\). The degree \(n\) encodes the severity of the failure.

The Obstruction Exact Sequence

For a short exact sequence of sheaves \(0 \to \mathcal{A} \to \mathcal{B} \to \mathcal{C} \to 0\) on \(\mathcal{S}_P\), the long exact cohomology sequence is:

The connecting homomorphism \(\delta\) is JuGeo's repair operator: it takes a global section of \(\mathcal{C}\) (a verified sub-judgment) and produces the obstruction in \(H^1(\mathcal{A})\) that remains to be repaired.

Obstruction Persistence and the Cohomology Ring

Obstructions are persistent: they are stored with the judgment and survive incremental recompilation. Moreover, the cup product

gives the set of obstruction classes the structure of a graded ring. This ring can be queried — e.g., to find all judgments whose obstruction is in the same cohomology class (likely sharing a common root cause) — and used to plan repair strategies.

Four Obstruction Operations

from jugeo.geometry.site import Coordinate, CoordinateKind
from jugeo.geometry.covers import Cover
from jugeo.geometry.descent import GluingData

base = Coordinate(("mypackage",), CoordinateKind.MODULE)
left = Coordinate(("mypackage", "validate"), CoordinateKind.FUNCTION)
right = Coordinate(("mypackage", "emit"), CoordinateKind.FUNCTION)

cover = Cover(
    target=base,
    patches=(left, right),
    overlaps=((left.key, right.key),),
    provenance=("docs",),
)

gluing = GluingData.from_cover(
    cover,
    {
        left.key: {"status": "ok", "currency": "USD"},
        right.key: {"status": "ok", "currency": "EUR"},
    },
)

cocycle = gluing.compute_cocycle()
print(cocycle.dimension)
print(cocycle.summary())

7. Semantic Moves

A semantic move is an atomic proof-search operation that transforms one or more judgments. Moves play the role that tactics play in interactive theorem provers, but they operate on the geometric structure of judgments rather than on proof terms. JuGeo defines 16 primitive moves; users may compose them into strategies.

Move Composition and Strategy DSL

Moves compose via a small DSL. The sequential combinator \(m_1 \,;\, m_2\) applies \(m_1\) then \(m_2\) on the output; the parallel combinator \(m_1 \parallel m_2\) applies both to independent sub-judgments simultaneously; and the try combinator \(m_1 \mathbin{||} m_2\) applies \(m_2\) when \(m_1\) fails:

from jugeo.evidence.trust import TrustAlgebra, TrustLevel
from jugeo.moves import MoveKind

algebra = TrustAlgebra()
combined = algebra.meet(TrustLevel.SOLVER_DISCHARGED, TrustLevel.HUMAN_ATTESTED)
print(combined)
print([move.name for move in MoveKind][:6])

8. Python Effects as Sheaf Sections

Python's effect system — exceptions, mutable state, asynchronous suspension, generators, context managers — maps precisely onto the geometric language of sheaves. This correspondence is not merely an analogy; it is the formal bridge that lets JuGeo extract judgments automatically from unannotated Python code.

Example: Exception Branches

from jugeo.easy import spec

review = spec(
    '''
def sum_positive(items):
    total = 0
    for x in items:
        if x < 0:
            raise ValueError(f"negative item: {x}")
        total += x
    return total
''',
    '''
def spec(result, items):
    return result >= 0
''',
    input_cover=[
        {"args": [[1, 2, 3]], "kwargs": {}},
        {"args": [[]], "kwargs": {}},
    ],
    entrypoint="sum_positive",
)
print(review)
print(review.satisfied, review.witness_count)

Example: Context Manager as Covering Family

from jugeo.easy import bugs

result = bugs('''
def load_text(path):
    fh = open(path, "r")
    return fh.read()
''')

print(result)
for bug in result.items:
    print(bug.message)

The Effect-Sheaf Correspondence

The correspondence can be stated as a theorem relating Python's operational semantics to the sheaf-theoretic model: