Target Shape Tactic Routing

Before any proof attempt it reads the candidate tactics for one goal and records an allow-or-reject decision for each. Before a proof is attempted, this component reads a list of candidate proof tactics for one goal and writes down an allow-or-reject decision for each. It runs in src/microcosm_core/organs/target_shape_tactic_routing_gate.py.

It decides from goal shape and an environment probe without calling Lean, emitting a tactic-by-tactic record of what was admitted or blocked and why. The decision is made from evidence that already exists: the shape of the goal and a probe that says which tactics the declared environment can run. Nothing here calls Lean, runs a prover, or proves anything. The output is a record that shows, tactic by tactic, what was admitted or blocked and the plain reason, in place of an opaque "we tried these" claim.

A rejection is one of three kinds: unprobed, known but unavailable, or available but wrong for the goal shape, kept separate so a reader sees which limit each hit. A rejection has one of three kinds. The tactic is not in the tested probe set, so it was never measured. It is known but marked unavailable in the declared environment. Or it is available but does not fit the goal shape. The record separates those three so a reader can see which limit each blocked tactic hit.

Purpose

Most proof cost is wasted on doomed tactics

Most proof cost goes to tactics that were never going to work, and a loose gate that trusts the route's own choice cannot catch an unavailable or unprobed one. A proof attempt is expensive, and most of that cost is spent on tactics that were never going to work. A loose gate that trusts the route's own declared choice cannot catch this: the route is a claim about what should run, and a route that admits an unavailable or unprobed tactic passes a loose check while still wasting the later prover call.

The gate recomputes the tactic choice

The gate recomputes the selection from a per-shape preferred order, skipping and recording unselectable tactics, and flags a route whose declared choice disagrees. So the gate recomputes the choice rather than accepting the declared one. Each target shape carries a short preferred-tactic order, held in PREFERRED_TACTICS_BY_TARGET_SHAPE (for example omega for int_linear_arithmetic, decide for closed_nat_mod_decision). The gate walks that order, skips any preferred tactic it cannot select, records why it skipped, and falls back to the next allowed candidate or to DEFAULT_PREFERRED_TACTICS for a shape it does not recognise. A route whose declared selection disagrees with the computed one is flagged, not honoured.

How it works

_build_result orders the pipeline

_build_result loads the two inputs, scans for forbidden material, builds availability sets, scores each route, folds in negatives, and sets one pass-or-blocked status. _build_result runs the pipeline in order. It loads the two input files through _load_payloads, scans every input path for forbidden material with scan_paths, builds the availability sets with _portfolio, sanitizes and scores each route case, checks the copied source artifacts, folds in the negative-case fixtures, then sets a single pass-or-blocked status and emits the result and board.

_portfolio splits the probe into three sets

_portfolio splits the probe into known, available, and unavailable ids, counting a tactic available only when its status is one of four passing values. _portfolio reads the tactic probe file and splits it into three sets: known_tactic_ids (every tactic listed), available_tactic_ids, and unavailable_tactic_ids. A tactic counts as available only when its status is one of available, pass, compiled, or compile_pass.

_score_case compares declared against computed

_score_case reads a case's allowed and candidate lists, gets a per-tactic verdict, computes the selection, and compares the declared tactic against the computed one. _score_case scores one route case. It reads the case's allowed_tactic_ids and candidate list, asks _decision_for_tactic for a verdict on each candidate, computes the selection with _shape_preferred_selection, and compares the case's declared selected_tactic_id against the computed one.

_decision_for_tactic rejects in a fixed order

_decision_for_tactic rejects in order as unprobed, unavailable, or shape-inadmissible, admitting only a tactic that is probed, available, and allowed for the shape. _decision_for_tactic is the per-tactic gate. It rejects in a fixed order: a tactic absent from known is UNPROBED_TACTIC, a known tactic absent from available is UNAVAILABLE_TACTIC, an available tactic absent from allowed is TARGET_SHAPE_ADMISSIBILITY_REJECTED. Only a tactic that is probed, available, and allowed for the shape gets TARGET_SHAPE_ADMISSIBLE.

_shape_preferred_selection picks the first allowed tactic

_shape_preferred_selection walks the shape's preferred order and returns the first allowed tactic, recording skips, the default-used flag, and a preferred-unavailable case. _shape_preferred_selection walks the preferred order for the shape and returns the first tactic that is allowed. It records the skipped preferred tactics and their reasons, sets unknown_shape_default_used when the shape has no specific map, and marks the preferred-unavailable case when the first preferred tactic is known but not usable.

_route_integrity_findings types each per-case problem

_route_integrity_findings turns any per-case problem into a typed finding: an admitted unavailable or unprobed tactic, a post-execution stage, or a selection mismatch. _route_integrity_findings turns any per-case problem into a typed finding: an admitted unavailable tactic, an admitted unprobed tactic, a post-execution route stage, or a declared selection that does not match the computed preference.

Sanitizing private goal material

The sanitizer keeps the public route shape but drops forbidden private-target keys and masks private-looking strings before any public row, reporting only the field path and class. _private_target_material_findings and _sanitize_private_target_material handle the scope limit on private goals. The sanitizer keeps the public route shape but drops any key in FORBIDDEN_PRIVATE_TARGET_KEYS (private target ids, formulas, target statuses, solver and derivation traces, proof-packet and certificate-search refs, submission packages) and replaces private-looking strings with private_target_material_omitted before any public row is built. The findings function reports the rejected field path and class, never the matched value.

Source-digest checks and the two entry points

_source_artifact_imports re-hashes the four copied source files and marks each copy, rewrite, or mismatch, while run includes the negative cases and run_routing_bundle omits them. _source_artifact_imports re-hashes the four copied source files named in REAL_SUBSTRATE_REFS and marks each as an exact copy, a path rewrite, or a digest mismatch. write_receipts writes the result, board, validation, and sign-off records. run drives the fixture with the negative cases included; run_routing_bundle drives the exported bundle without them.

flowchart TD Inputs["Probe file + route cases"] Portfolio["_portfolio known / available / unavailable"] Sanitize["_sanitize_private_target_material drop private goal keys"] Decide["_decision_for_tactic per-tactic verdict"] Select["_shape_preferred_selection compute the selection"] Score["_score_case declared vs computed"] Findings["_route_integrity_findings typed rejections"] Result["_build_result status + board"] Inputs --> Portfolio Inputs --> Sanitize Portfolio --> Decide Sanitize --> Decide Decide --> Select Select --> Score Score --> Findings Findings --> Result

What the exported bundle scores to

On the exported bundle four tactics are available and aesop unavailable, all seven route cases are pre-execution, and four source files are copied in with digest checks. On the exported bundle the probe marks decide, omega, simp_all, and rfl available and aesop unavailable. All seven route cases are pre_execution, and four source files are copied in with digest checks.

Negative cases

The gate must reject each of these, listed in EXPECTED_NEGATIVE_CASES: The gate must reject each of these, listed in EXPECTED_NEGATIVE_CASES:

• unavailable_tactic_admitted: a route admits a tactic the probe marks unavailable, here aesop while Mathlib is absent.
• unprobed_tactic_allowed: a route admits a tactic missing from the probe.
• shape_preferred_tactic_overridden: a declared tactic bypasses the computed shape preference.
• unknown_shape_fallback: a shape bypasses the default safe order.
• preferred_unavailable_fallback: a route bypasses the next available tactic after the first preferred one is unavailable.
• proof_body_leakage: a route carries a proof, provider, or Lean body field.
• private_target_material: a route carries a private target id, formula, status, trace, or challenge path, rejected without echoing the value.
• post_execution_route: a route selection carries execution evidence.
• release_overclaim: a route claims proof, provider, Lean, or launch-scope decision.

Prior Art Grounding

A pre-execution proof-search admissibility filter

It follows the proof-search habit of matching a goal shape to available methods before spending runtime, narrowed to a pre-execution admissibility filter over shape, references, and availability. The routing layer follows a known proof-search pattern: match a goal shape to methods that are known to be available before spending runtime on them. Lean's tactic documentation gives the proof-assistant context for goal-directed tactic choice, and Isabelle's Sledgehammer is a mature example of selecting external provers and relevant facts from a goal. This component narrows the idea to a pre-execution admissibility filter: shape, allowed references, and current availability must line up before a route is exported.

• Lean 4 tactic documentation: https://lean-lang.org/theorem_proving_in_lean4/Tactics/
• Isabelle Sledgehammer user guide: https://isabelle.in.tum.de/doc/sledgehammer.pdf

Validation Result record Path

From microcosm-substrate/, reproduce the result with temporary result records:

What a pass certifies

A pass means the seven cases scored as expected, the four source copies matched digests, every negative was rejected, and the secret scan was clean, without widening the ceiling. A pass means the seven route cases scored as expected, the four source copies matched their digests, every negative case was rejected, and the secret scan found no blocking hit. It does not widen the no-Lean, no-proof ceiling.