Semantic Moves

Semantic moves are the atomic proof operations by which JuGeo advances judgments toward verified status. The move system provides 16 named kinds, a composable dataclass, a selection pipeline, and four control laws that govern how moves are sequenced automatically.

🕑 22 min read Advanced

📋

On this page: Overview · Move dataclass · 16 move kinds · Selection pipeline · Control laws · Inference rules · Python examples

Overview

A semantic move is a single, justified step in a proof search. It takes the current judgment state and transforms it — either by generating new sub-goals, resolving existing ones, or rewriting the formulas involved. Moves are the fundamental currency of JuGeo's proof engine: all higher-level strategies (descent, repair, treaty negotiation) are ultimately sequences of moves.

The move system is inspired by sequent-calculus tactics in proof assistants like Coq and Lean, but adapted to JuGeo's three-layer architecture (site, judgment sheaf, evidence). Moves operate on judgment states rather than raw formulas, so they carry trust, evidence provenance, and obstruction data as first-class citizens.

Move Semantics

\[ \text{move}(m) : \text{JState}(\Gamma \vdash J) \;\longmapsto\; \text{JState}(\Gamma' \vdash J') \;\cup\; \Delta_{\text{new goals}} \]

Move Dataclass

Every move is represented as an instance of the SemanticMove dataclass. The key fields are:

python

from dataclasses import dataclass, field

@dataclass(frozen=True)
class SemanticMoveSummary:
    kind: str
    parameters: dict
    cost: float
    rationale: str
    evidence_channels: tuple[str, ...] = field(default_factory=tuple)

move = SemanticMoveSummary(
    kind="GLUE",
    parameters={"cover": "payments.validate + payments.charge"},
    cost=0.4,
    rationale="Try descent before escalating to repair.",
    evidence_channels=("solver", "runtime"),
)

print(move)

16 Move Kinds

JuGeo defines 16 canonical move kinds, organised into four groups: basic verification, structural, sheaf-theoretic, and social/coordination. Each kind has a formal inference rule that specifies its preconditions and postconditions.

Kind	Group	Description
VERIFY	Basic	Call the SMT solver on the current judgment's VC. The simplest move: succeeds if UNSAT, fails if SAT or UNKNOWN.
CONSTRUCT	Basic	Generate an explicit proof term or certificate. Used when the solver cannot decide but a manual construction exists.
NORMALIZE	Basic	Simplify the judgment formula using rewrite rules before attempting verification. Reduces solver load for complex formulas.
WEAKEN	Structural	Replace the judgment's conclusion with a weaker formula that is easier to verify. Records the weakening in the evidence chain.
CONTRACT	Structural	Merge duplicate hypotheses in the judgment context to reduce redundancy and simplify the proof state.
EXCHANGE	Structural	Reorder hypotheses in the context. Required before applying rules that are sensitive to hypothesis order.
CUT	Structural	Introduce an intermediate lemma: split the goal into “prove the lemma” and “use the lemma to prove the original goal”.
RESTRICT	Sheaf	Apply a restriction map to push a judgment from a coordinate \(U\) to a sub-coordinate \(V \hookrightarrow U\).
TRANSPORT	Sheaf	Transport a judgment along an isomorphism of coordinates. Used to reuse proofs from structurally equivalent functions.
GLUE	Sheaf	Assemble local sections into a global section via the sheaf gluing axiom. The core move for descent.
REPAIR	Sheaf	Attempt to automatically repair a H⁰ or H¹ obstruction by modifying the failing section(s).
NEGOTIATE_TREATY	Coordination	Open a treaty negotiation with another coordinate to resolve an H¹ interface conflict. See Trust Algebra.
REFINE_COVER	Coordination	Replace the current covering family with a finer cover that may admit descent where the coarser cover fails.
PROMOTE_TRUST	Coordination	Upgrade the trust level of an existing judgment by supplying additional evidence (e.g., a formal proof after a solver result).
CHALLENGE	Coordination	Dispute a judgment made by another evidence channel. Initiates a challenge protocol that requires the original channel to produce a certificate.
ESCALATE	Coordination	Escalate an unresolved judgment to a higher-trust evidence channel (e.g., from SOLVER to FORMAL_PROOF).

Move Selection Pipeline

When JuGeo needs to advance a judgment, it runs the move selection pipeline to choose the most promising next move. The pipeline has five stages:

Applicability filtering

Each of the 16 move kinds is checked for applicability to the current judgment state. Moves whose preconditions are not satisfied are eliminated.

Cost estimation

For each applicable move, the pipeline estimates the resource cost (solver time, I/O, LLM tokens) and the expected trust delta if the move succeeds.

Control law evaluation

The active control law (GREEDY, LOOKAHEAD, BALANCED, or ADAPTIVE) scores each candidate move using its own objective function and selects the highest-scoring move.

Application

The selected move is applied. If it succeeds, the judgment state is updated and the move is recorded in the evidence chain. If it fails, the pipeline falls back to the next best candidate.

Feedback update

The pipeline records the outcome (success, failure, cost incurred) and updates the control law's internal state. ADAPTIVE law uses this to improve future move selection.

Control Laws

A control law determines how moves are selected and sequenced. JuGeo provides four built-in laws, each with different time/quality trade-offs.

GREEDY

Greedy

Always apply the locally cheapest applicable move. No lookahead. Fast; good for well-structured proofs.

LOOKAHEAD

Lookahead (depth-\(k\))

Search \(k\) moves ahead before committing. Slower but avoids cheap moves that lead to expensive dead ends.

BALANCED

Balanced

Optimise a weighted combination of cost and expected trust gain. Good default for production use.

ADAPTIVE

Adaptive

Learns from past outcomes via a bandit update rule. Performance improves as the system accumulates history.

💡

Default law. The default control law is BALANCED. Switch to GREEDY for interactive use where latency matters, and to ADAPTIVE for long-running CI pipelines where the system can learn from a large history of proof attempts.

Inference Rules

Each move kind has a corresponding inference rule. Here are the rules for several key moves. The notation \(\vdash_{\mathcal{S}}\) means “provable in the semantic site \(\mathcal{S}\)”; \(\tau\) is a trust level.

VERIFY rule

\[ \frac{\text{SMT}(\varphi) = \text{UNSAT}} {\Gamma \vdash_{\mathcal{S}}^{\tau_{\text{SOLVER}}} \varphi} \quad (\text{VERIFY}) \]

GLUE rule (descent)

\[ \frac{\bigl\{\Gamma \vdash_{\mathcal{S}}^{\tau_i} \varphi|_{U_i}\bigr\}_{i \in I} \quad \bigl\{\varphi|_{U_i} \sim \varphi|_{U_j} \text{ on } U_{ij}\bigr\}_{i

CUT rule

\[ \frac{\Gamma \vdash_{\mathcal{S}}^{\tau_1} \psi \qquad \Gamma, \psi \vdash_{\mathcal{S}}^{\tau_2} \varphi} {\Gamma \vdash_{\mathcal{S}}^{\tau_1 \wedge \tau_2} \varphi} \quad (\text{CUT}) \]

WEAKEN rule

\[ \frac{\Gamma \vdash_{\mathcal{S}}^{\tau} \varphi \qquad \varphi \Rightarrow \psi} {\Gamma \vdash_{\mathcal{S}}^{\tau} \psi} \quad (\text{WEAKEN}) \]

Python Examples

Manually constructing and applying a move:

python

from jugeo.geometry.descent import DescentConfiguration, DescentStrategy

config = DescentConfiguration(
    strategy=DescentStrategy.ITERATIVE,
    depth_limit=3,
    copilot_assisted_repair=True,
)

print(config.strategy)
print(config.depth_limit)
print(config.copilot_assisted_repair)

Running the full move pipeline on a module:

python

import subprocess

completed = subprocess.run(
    ["python3", "-m", "jugeo", "--format", "json", "prove", "src/example.py"],
    check=True,
    capture_output=True,
    text=True,
)

print(completed.stdout)

Registering a custom move kind:

python

from jugeo.geometry.descent import RepairFrontier

frontier = RepairFrontier(
    missing_evidence=("solver certificate for numeric bounds",),
    suggested_refinements=("split numeric cases into a finer cover",),
    estimated_cost=1.0,
)

for category, item in frontier.prioritized_items():
    print(category, item)