API Reference

Enumeration of semantic positions a coordinate may occupy within a Python codebase.

A point in the semantic site — the smallest addressable unit of a Python program that JuGeo can reason about. Coordinates are immutable and hashable, serving as keys in descent data structures.

• fqn() -> strFully-qualified name: path + "." + name.
• is_ancestor_of(other: Coordinate) -> boolTrue if self is a proper ancestor in the containment hierarchy.
• children(site: Site) -> list[Coordinate]Return all direct children registered on the given site.

from jugeo.geometry import Coordinate, CoordinateKind

mod = Coordinate(("mylib", "core"), CoordinateKind.MODULE)
fn = Coordinate(("mylib", "core", "parse"), CoordinateKind.FUNCTION, metadata={"lineno": 42})

print(fn.components)
print(fn.name)
print(fn.metadata["lineno"])

A Grothendieck site over a Python codebase. Packages together a category of coordinates and morphisms with a Grothendieck topology (encoded as covering families). Normally created via build_site() or SiteBuilder.

• covering_sieves(c: Coordinate) -> list[CoveringFamily]All covering families whose target is c.
• hom(src: Coordinate, tgt: Coordinate) -> list[Morphism]Morphisms from src to tgt.
• sheaf_condition(F, c) -> boolCheck that presheaf F satisfies the sheaf condition at c.
• restrict(J: Judgment, m: Morphism) -> JudgmentPull back a judgment along a morphism.

Fluent builder for constructing Site objects incrementally. Validates consistency (e.g., all morphism endpoints exist) before finalising.

• add_coordinate(c: Coordinate) -> SiteBuilderRegister a coordinate; returns self for chaining.
• add_morphism(m: Morphism) -> SiteBuilderRegister a morphism; raises ValueError if endpoints are unknown.
• add_covering(cf: CoveringFamily) -> SiteBuilderRegister a covering family.
• build() -> SiteValidate and construct the Site. Raises SiteError on inconsistency.

from jugeo.geometry import SiteBuilder, Coordinate, CoordinateKind, Morphism
from jugeo.geometry.site import MorphismKind

builder = SiteBuilder("my_project")
mod = Coordinate(("mylib",), CoordinateKind.MODULE)
fn = Coordinate(("mylib", "parse"), CoordinateKind.FUNCTION)
builder.add_coordinate(mod).add_coordinate(fn)
builder.add_morphism(Morphism(fn, mod, MorphismKind.RESTRICTION, "contained-in"))
site = builder.build()
print(site.coordinate_count(), site.morphism_count())

A directed arrow between two coordinates representing a structural or semantic relationship. Common kind values are "inclusion", "call", "import", "subtype", and "data_flow".

A sieve over a coordinate: a collection of morphisms whose sources jointly cover the target, satisfying the Grothendieck topology axioms (stability and transitivity).

Automatically construct a Site by introspecting a Python package on disk. Parses ASTs, extracts coordinates at each requested CoordinateKind, and infers morphisms from containment and import relationships.

from jugeo.geometry import build_site, Coordinate, CoordinateKind

mod = Coordinate(("mylib",), CoordinateKind.MODULE)
fn = Coordinate(("mylib", "parse"), CoordinateKind.FUNCTION)
site = build_site([mod, fn])
print(site.coordinate_count(), site.morphism_count())

Pull back a coordinate along a morphism within the site. Equivalent to computing the fiber product in the category of coordinates.

Strategy governing how the DescentEngine handles incompatible local sections.

Orchestrates the descent process: given a collection of LocalSections over a covering family, attempts to glue them into a GlobalSection. Detects and classifies DescentObstructions when gluing fails.

• glue(sections: list[LocalSection], cover: CoveringFamily) -> GlobalSection | DescentObstructionMain entry point. Attempts to glue local sections over the given cover.
• check_cocycle(data: GluingData) -> list[DescentObstruction]Verify the cocycle condition on overlaps. Returns empty list on success.
• obstruction_class(obs: DescentObstruction) -> CohomologyClassCompute the first Cech cohomology class witnessing the obstruction.
• repair(obs: DescentObstruction) -> GlobalSection | NoneAttempt repair; returns None if repair is impossible.

from jugeo.geometry.descent import DescentEngine, DescentStrategy

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

A judgment localised to a single member of a covering family. The morphism connects the local coordinate back to the covered object.

A successfully glued global judgment. The provenance field records which local sections were combined and through which covering family.

Records a failure of the gluing/descent process. The cohomology_class encodes the algebraic obstruction in \(\check{H}^1\).

Complete record of a gluing attempt: the covering family, local sections, pairwise overlap data, and the cocycle maps used to check compatibility.

An element of \(\check{H}^n\) for the semantic site. Degree 0 is sections; degree 1 encodes gluing obstructions. is_trivial is True when the class vanishes (successful gluing).

A priority queue of repair strategies applied when the DescentEngine encounters an obstruction. Each strategy is tried in priority order until one succeeds or the budget is exhausted.

• attempt(obs: DescentObstruction) -> LocalSection | NoneTry each strategy in turn; return the repaired section or None.
• add_strategy(fn, priority=0) -> NoneRegister a new repair strategy with the given priority.

A validated covering family. Unlike raw CoveringFamily, a Cover has been checked for the stability and transitivity axioms of the Grothendieck topology.

• overlaps() -> list[OverlapDatum]Compute all pairwise intersections of cover members.
• is_good_cover() -> boolTrue if all pairwise and higher overlaps are contractible.
• refine(extra: list[CoverMember]) -> CoverReturn a refined cover by adding extra members.

A single patch in a covering family. The weight is used by budget-allocation strategies to prioritise verification effort.

Fluent builder for Cover objects. Validates topology axioms on build().

• add_member(c: Coordinate, inclusion: Morphism, weight=1.0) -> CoverBuilderAdd a patch to the cover.
• build() -> CoverValidate and construct the Cover.

from jugeo.geometry import Coordinate, CoordinateKind, Morphism
from jugeo.geometry.site import MorphismKind
from jugeo.geometry.covers import CoverBuilder

base = Coordinate(("pricing",), CoordinateKind.MODULE)
patch = Coordinate(("pricing", "total"), CoordinateKind.FUNCTION)
inclusion = Morphism(patch, base, MorphismKind.RESTRICTION, "contained-in")
cover = CoverBuilder().set_base(base).add_member(patch, inclusion).build()
print(len(cover.members))
print(type(cover).__name__)

Records the intersection of two cover members together with the restriction morphisms from each member into the intersection. Used by DescentEngine.check_cocycle().

The fundamental unit of reasoning in JuGeo. A judgment \(J = (c,\varphi,A,E,O,B,T,\Pi)\) ties a logical claim to a specific coordinate, its supporting evidence, any residual proof obligations, and a trust annotation.

• restrict(m: Morphism) -> JudgmentPull back along a morphism; propagates evidence and obligations.
• compose(other: Judgment) -> JudgmentSequential composition: self feeds into other as antecedent.
• is_closed() -> boolTrue if all residual obligations are discharged.
• trust_level() -> TrustLevelShortcut for self.trust.level.
• to_dict() -> dictSerialise to a JSON-compatible dictionary.

from jugeo import judgments

print(sorted(name for name in dir(judgments) if not name.startswith("_")))

A logical formula. The language field indicates the syntax: "jugeo" for native JuGeo logic, "z3smt" for SMT-LIB2, "lean4" for Lean 4 term syntax.

The set of antecedent judgments on which a judgment depends. kind specifies how antecedents combine: "conjunction" (all required) or "disjunction" (any sufficient).

A collection of evidence items from potentially multiple channels. The overall trust level is derived by applying the combination rule across all items.

• effective_trust() -> TrustLevelAggregate trust level according to the combination rule.
• channel_summary() -> dict[str, int]Count items per channel name.

A single piece of evidence from one channel. payload is channel-specific (e.g., an SMT proof certificate, a Lean term, a test result).

The set of open proof goals remaining after current evidence has been applied. An empty goals list means the judgment is fully discharged.

• is_discharged() -> boolTrue iff goals is empty.
• discharge(goal: Proposition) -> ResidualObligationReturn a new obligation with goal removed.

A known impediment to discharging the residual obligation. Use Obstruction.none() for judgments with no known obstruction.

• Obstruction.none() -> ObstructionCanonical sentinel representing the absence of any obstruction.

Trust metadata attached to a judgment. Records the enumerated trust level and the identity of the agent or tool that produced the evidence.

Ordered enumeration of trust levels, from highest to lowest confidence. Levels form a lattice with VERIFIED at the top and CONTRADICTED as a distinguished bottom element indicating active refutation.

from jugeo.evidence.trust import TrustLevel, TrustAlgebra

algebra = TrustAlgebra()
print([level.name for level in TrustLevel])
print(algebra.join(TrustLevel.RUNTIME_WITNESSED, TrustLevel.SOLVER_DISCHARGED))

A richer trust descriptor recording not just the level but the contributing channels, a temporal decay rate (for runtime evidence), and an overall confidence score in [0, 1].

• age(days: float) -> TrustProfileReturn a new profile with confidence decayed by days * decay_rate.
• effective_level(threshold=0.5) -> TrustLevelDowngrade the level if confidence falls below threshold.

Stateless class providing lattice operations over TrustLevel and TrustProfile. All methods are classmethods.

• meet(a: TrustLevel, b: TrustLevel) -> TrustLevelGreatest lower bound (weakest-link combination).
• join(a: TrustLevel, b: TrustLevel) -> TrustLevelLeast upper bound (strongest-wins combination).
• combine(profiles: list[TrustProfile], rule="meet") -> TrustProfileCombine multiple profiles using "meet", "join", or "weighted".
• transfer(J: Judgment, m: Morphism) -> TrustAnnotationCompute the trust annotation for a judgment restricted along m.
• sufficient_for(level: TrustLevel, requirement: TrustLevel) -> boolTrue if level >= requirement in the lattice order.

from jugeo.evidence.trust import TrustAlgebra, TrustLevel

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

Identifies the logical fragment of an SMT formula. Used by SolverRouter to select the most efficient solver tactic.

High-level policy for the SolverRouter when multiple solver sessions are available.

A formula ready for dispatch to Z3, expressed in SMT-LIB2 syntax. fragment is pre-classified to allow the router to pick the right tactic.

Result from a Z3 query. status is one of "sat", "unsat", or "unknown". model is populated on "sat"; proof on "unsat" when proof generation is enabled.

• is_proved() -> boolTrue iff status is "unsat" (negation unsatisfiable means original formula is valid).
• to_evidence_item() -> EvidenceItemConvert to an EvidenceItem with trust SOLVER (unsat) or RUNTIME (sat-model).

Manages a persistent Z3 context, supporting incremental solving (push/pop), tactic selection, and result caching. Thread-safe when config.threadsafe=True.

• solve(formula: Z3Formula) -> Z3ResultSubmit a formula and return the result.
• solve_batch(formulas: list[Z3Formula]) -> list[Z3Result]Solve multiple formulas, sharing the Z3 context.
• push() / pop()Incremental checkpoint operations.
• reset()Clear all assertions and restore the initial context.

from jugeo.solver.z3_session import Z3Session, Z3Formula, FragmentTag

session = Z3Session()
formula = Z3Formula(FragmentTag.QF_LIA, "(assert (> x 0))")
print(type(session).__name__)
print(formula.kind)
print(formula.expression)

Routes verification queries to the appropriate Z3 session or solver backend based on formula fragment, strategy, and available budget.

• dispatch(formula: Z3Formula) -> Z3ResultRoute a single formula to the best session.
• dispatch_judgment(J: Judgment) -> JudgmentDispatch all open obligations in J; return an updated judgment.
• stats() -> dictReturn routing statistics: calls per session, success rates, total time.

from jugeo.solver.router import SolverRouter, RoutingStrategyKind

router = SolverRouter()
print(type(router).__name__)
print([strategy.name for strategy in RoutingStrategyKind][:4])

Abstract base class for all evidence channels. Concrete subclasses implement query() to obtain evidence for a proposition at a coordinate. Built-in channels: Z3Channel, LeanChannel, PytestChannel, OracleChannel, CopilotChannel.

• query(proposition: Proposition, coordinate: Coordinate) -> EvidenceItem | NoneAttempt to produce evidence. Returns None on failure or timeout.
• is_available() -> boolCheck whether the backing tool or service is reachable.

from jugeo.evidence.channels import EvidenceChannel

print([channel.name for channel in EvidenceChannel])
print(EvidenceChannel.COPILOT.requires_corroboration())

Routes a proposition to one or more evidence channels according to a dispatching policy and aggregates results into an EvidenceBundle.

• gather(proposition: Proposition, coordinate: Coordinate) -> EvidenceBundleQuery channels per policy and aggregate results.
• add_channel(ch: EvidenceChannel, priority=0) -> NoneRegister a new channel at the given priority.

from jugeo.evidence.channels import ChannelRouter

router = ChannelRouter()
print(type(router).__name__)
print([name for name in dir(router) if not name.startswith("_")][:5])

Federates multiple ChannelRouter instances, each potentially representing a separate node in a distributed verification network. Evidence from all routers is merged into a single EvidenceBundle.

• gather(proposition: Proposition, coordinate: Coordinate) -> EvidenceBundleFan out across all routers and merge results.
• status() -> dict[str, bool]Availability status of each constituent router.

from jugeo.evidence.channels import ChannelFederation, ChannelRouter

federation = ChannelFederation(ChannelRouter())
print(type(federation).__name__)
print([name for name in dir(federation) if not name.startswith("_")][:4])