Tactic Portfolio Availability

It turns one captured Lean smoke run into an explicit list of callable tactics, checking pre-recorded status rows for honesty without running Lean itself. tactic_portfolio_availability_probe turns one captured Lean run into an explicit list of which proof tactics were callable, before any router or proof search treats a tactic as usable. It reads pre-recorded status rows from a real smoke run and checks them for honesty. It does not run Lean itself.

The copied 2026-05-11 fixture covers eight tactics, seven compiling and aesop failed on a missing Mathlib import, reproduced into a metadata-only board and result records. The fixture is copied from a 2026-05-11 tactic affordance probe. It covers eight tactics: rfl, decide, omega, simp, simp_all, grind, native_decide, and aesop. Seven are recorded as compiling. aesop is recorded as failed because the paired environment probe reports that the Mathlib import it needs was absent. The component reproduces that verdict from the copied rows and writes a metadata-only availability board plus result records.

Purpose

A tactic name is not availability

A tactic name alone does not mean it can run; a router trusting the bare name reaches for tactics the environment cannot run and misreads the failure as a fact about the goal. A tactic name is not a usable tactic. aesop runs only if the surrounding Lean and Std environment carries the imports it needs. omega is callable in one project layout and not in another. A router that trusts a bare tactic name will reach for tactics the current environment cannot run, then misread the failure as a fact about the goal rather than a fact about the environment.

Missing import kept distinct from broken tactic

It answers which tactics were callable and on what evidence, keeping a missing import distinct from a broken tactic so a router can re-attempt elsewhere. The component answers one question: in the observed environment, which tactics were callable, and on what evidence? The interesting part is how it treats failure. A recorded Lean FAIL is not flattened into one "unavailable" verdict. A missing import is kept distinct from a broken tactic, so a router can re-attempt the same tactic in a different environment instead of striking it off for good.

How it works

Two entrypoints over _build_result

run validates the first-wave fixture with negatives on, run_availability_bundle validates an exported bundle with negatives off and reuses an unchanged prior result. Two entrypoints drive the pipeline. run validates the first-wave fixture with negative cases enabled. run_availability_bundle validates an exported bundle with negative cases disabled, and reuses a prior result when _fresh_availability_bundle_receipt finds a matching record whose inputs have not changed since it was written. Both delegate the work to _build_result and then persist records.

_build_result runs these steps in order.

Digest-checking the copied source payloads

It loads the three copied source payloads and digest-checks each body against a recorded SHA-256, so a silently edited body becomes a finding rather than trusted input. It loads the copied source payloads with _load_source_payloads: the run-level affordance probe, the portfolio_core_v0 availability artifact, and the paired corpus-readiness file. Each copied body is digest-checked by _source_body_imports and _probe_source_imports against a recorded SHA-256, so a silently edited body becomes a finding rather than trusted input.

Mathlib probe gates dependent tactics

It derives the environment state from the Mathlib probe, whose single fact of whether the Lake import was available gates every Mathlib-dependent tactic. It derives the environment state with _authoritative_environment_state, which reads the Mathlib probe and reports whether the Mathlib Lake import was available. That single fact gates every Mathlib-dependent tactic.

Deriving each tactic's public status

It builds one row per tactic, mapping a source PASS to compile_pass and a FAIL to environment_fail when a required Mathlib import was absent, else compile_fail. It builds one availability row per tactic with _availability_rows_from_source. The public status comes from _derived_public_status_from_source: a source PASS becomes compile_pass; a source FAIL becomes environment_fail when the tactic requires Mathlib and Mathlib was absent, and compile_fail otherwise. When the status is a failure, _failure_classifier_from_source labels a Mathlib gap as MATHLIB_IMPORT_MISSING and otherwise carries the source error class through. This is why aesop reads as an environment failure, not a broken tactic.

Portfolio summary and latency banding

It summarises available and unavailable ids and bands each available tactic's copied duration as fast, moderate, or slow, stamped environment-scoped rather than a benchmark. It summarises the rows with _portfolio_summary: available and unavailable tactic ids, Mathlib-dependent ids, and a latency profile. _latency_band bands each available tactic by its copied duration as fast at 2500ms or less, moderate up to 5000ms, and slow above that. The latency profile is stamped environment-scoped, so a router can prefer a cheaper available tactic without reading speed as a benchmark result.

Negatives, secret scan, and result records

It evaluates the negative cases, scans every input path for forbidden material, and passes only with no finding, all negatives observed, and zero secret hits before writing result records. It evaluates the declared negative cases with _negative_findings, scans all input paths for forbidden material with scan_paths, and sets the overall status. The result is pass only when no category produced a finding, every expected negative case was observed, and the secret scan had zero blocking hits. _write_receipts then writes the result record, the availability board, the validation record, and the sign-off record, each carrying result record paths but no tactic bodies.

flowchart TD A["Copied affordance probe rows compile_status, requires_mathlib, duration_ms"] --> B["_build_result"] C["Mathlib environment probe"] --> B B --> D{"source compile_status"} D -->|PASS| E["compile_pass band duration fast / moderate / slow"] D -->|FAIL + requires Mathlib + Mathlib absent| F["environment_fail reason MATHLIB_IMPORT_MISSING"] D -->|FAIL otherwise| G["compile_fail"] E --> H["Availability board"] F --> H G --> H B --> I["metadata-only result and validation records"]

Negative cases

Six perturbed fixtures and their codes

Six perturbed fixtures must each be rejected with a specific error code, spanning missing status, unbacked Mathlib claims, unprobed tactics, missing durations, leaked bodies, and authority overclaim. _negative_findings checks six perturbed fixtures and requires each to be rejected with a specific error code. A tactic row with no compile_status gives TACTIC_PORTFOLIO_MISSING_COMPILE_STATUS. A Mathlib-dependent tactic marked available with no passing Mathlib probe gives TACTIC_PORTFOLIO_MATHLIB_CLAIM_WITHOUT_PROBE. A downstream request for a tactic not in the probed portfolio gives TACTIC_PORTFOLIO_UNPROBED_TACTIC_REFERENCED. An available tactic with no copied duration gives TACTIC_PORTFOLIO_AVAILABLE_DURATION_MISSING. A fixture carrying a proof or provider body gives TACTIC_PORTFOLIO_PROOF_BODY_FORBIDDEN. A payload asserting proof, provider, benchmark, or launch-scope decision gives TACTIC_PORTFOLIO_AUTHORITY_OVERCLAIM. A missing expected case blocks the run.

Prior Art Grounding

Feature-detection discipline from Autoconf and Lean

It follows the feature-detection habit of probing a local capability before relying on it, applying Autoconf and Lean's environment-sensitive discipline to one recorded run. The component follows the feature-detection habit of testing a local capability before relying on it, the same discipline GNU Autoconf's configure workflow established for build environments. Lean's own tactic documentation notes that tactic use is environment- and goal-sensitive, so a tactic name alone does not justify downstream routing. This component applies that probe discipline to one recorded run and keeps a Mathlib-dependent absence as evidence rather than discarding it.

• GNU Autoconf feature probing: https://ftp.gnu.org/old-gnu/Manuals/autoconf-2.57/html_chapter/autoconf.html
• Lean 4 tactic documentation: https://lean-lang.org/theorem_proving_in_lean4/Tactics/

Validation Result record Path

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

What a pass certifies

A pass means every copied body matched its digest, the eight rows produced the expected board with aesop as an environment failure, all six negatives were rejected, and the secret scan was clean. A pass means every copied source body matched its recorded digest, the eight tactic rows produced the expected availability board with aesop as an environment failure, all six negative cases were rejected, and the secret scan found no forbidden material.