Verifier Lab Execution Spine

It runs bounded Lean proof-step candidates in a throwaway copy of a public project and records each checker return code while keeping proof text and payloads out. verifier_lab_execution_spine is the component that actually runs bounded Lean proof-step attempts and writes down what the checker said. It copies a small public Lean project into a throwaway workspace, builds it once, writes one .lean file per candidate, runs the Lean checker on each, and records the return code. It keeps the proof text, the tool output, and every provider or oracle payload out of the result. A reader gets the pass or fail facts and the safety counts, and nothing that would leak.

Narrower than the kernel, the spine executes each transition, turns a zero exit into accepted, and rejects contaminated candidates before the checker ever runs. The component is narrower than verifier_lab_kernel. The kernel reasons about the shape of a transition; this spine executes it. A zero exit code from the Lean checker becomes accepted. Anything else becomes a residual with a failure class. Candidates that carry a forbidden field, or that mark an oracle or provider as visible, are rejected before the checker is ever invoked, so a contaminated run cannot be dressed up as a clean one.

It emits four records, full result, board summary, validation, and fixture sign-off, each stating the same scope limit and carrying counts without bodies. It emits four result records: a full result, a board summary, a validation record, and a fixture-sign-off record. All four state the same scope limit, carry the return codes and counts, and omit the bodies.

Purpose

Keeping hidden help out of the record

Proof systems can report success while hiding oracle or provider help, so this component answers one question: did a bounded Lean candidate pass the checker unaided? Automated proof systems can blur how a result was reached. A model can be handed the answer by an oracle, or shown the proof by a provider, and still report the result as if it had found the proof alone. A loose result record hides that distinction: it prints a success without saying what help was in the room. This component exists to keep that blur out of the record. It answers one question. Did a bounded Lean candidate pass the checker, with no help the record is hiding?

Authority separation holds counters at zero

Authority separation keeps verified candidates, oracle references, and provider hypotheses as distinct classes, pinning the forward-success and export counters at zero by construction. The discipline is authority separation. A verified candidate is one class. An oracle reference and a provider hypothesis are separate classes that are never counted as forward success. The counters oracle_forward_success_increment_count and provider_results_counted are held at zero by construction, alongside proof_body_export_count and source_mutation_count. Real execution and a clean record are not in tension: the leak checks run first, so the Lean run that follows is already free of the fields that would compromise it.

How it works

Two entry points over _build_result

run executes Lean for real on the fixture while run_execution_bundle validates an exported group offline, and both flow through _build_result then write_receipts. Two entry points drive the component. run handles the first-wave fixture and executes Lean for real. run_execution_bundle validates an exported group without a Lean toolchain, so a third party can inspect a shipped bundle offline. Both call _build_result, then write_receipts.

_build_result scans, copies, and builds once

_build_result loads the packet, secret-scans every input, and builds the copied Lean project once, executing candidates only when that build returns zero. _build_result is the spine. It loads the execution packet, scans every input path for forbidden content with the shared secret-exclusion scan, and reads the tool versions. In fixture mode it opens a temporary directory, copies the Lean project into it, and calls _build_lake_project, which runs lake build MicrocosmProofWitness once with a sixty-second limit. Only if that build returns zero does it execute the transition candidates.

Per-candidate contract check in _execute_transition

_execute_transition first runs the contract check for forbidden keys, visible oracle or provider, and unknown action class, rejecting the candidate or else running lake env lean and recording the return code. Each candidate goes through _execute_transition. That function first calls _validate_transition_contract. The contract check walks the candidate for any key in FORBIDDEN_TRANSITION_KEYS (proof_body, raw_tactic_script, oracle_template, provider_output_body, and similar) using _walk_forbidden_keys, checks whether oracle_visible or provider_visible is set, and checks that the action_class is one of the nine names in ALLOWED_ACTION_CLASSES. If any check fires, the candidate becomes a CONTRACT_REJECTED record with the error codes attached and no Lean run. If the contract is clean, _execute_transition writes a .lean source built by _lean_source_for_transition, runs lake env lean on it, and sets accepted from the return code. The record carries the return code, the action class, and the failure class. It never carries the proof text or the stdout and stderr bodies.

CP2 translation and evolve mutation lanes

Two smaller lanes also run: CP2 translation emits typed next-action candidates from a fixed vocabulary, and evolve mutation touches only bounded policy artifacts, each rejecting out-of-scope requests. Two smaller lanes run on the same packet. CP2 translation reads residual cases and emits typed next-action candidates drawn from a fixed vocabulary; a request that smuggles a proof body is rejected. Evolve mutation adjusts only the bounded policy artifacts named in ALLOWED_EVOLVE_ARTIFACTS; a mutation aimed at anything else is rejected.

Digest checks on the exported group

validate_source_module_imports recomputes each copied file's SHA-256 against the manifest and blocks the group on any digest mismatch, missing anchor, or out-of-prefix source. validate_source_module_imports handles the exported group. It reads source_module_manifest.json, confirms the declared module count matches the rows, and for each row recomputes the SHA-256 digest of the copied file and compares it to the manifest. A digest mismatch, a missing anchor, or a source reference outside the allowed prefixes blocks the group. The copied bodies live in the bundle, never in the record.

write_receipts pins the zero-authority facts

write_receipts composes the four records with every authority flag false, and the status passes only when the scan is clean, the build returned zero, and the expected transition counts are met. write_receipts composes the four records and pins the safety facts: receipts_include_proof_bodies false, provider_calls_authorized false, source_mutation_authorized false, release_authorized false. The overall status in _build_result passes only when the secret scan is clean, Lean and Lake are available, the project build returned zero, no expected negative case is missing, and the run produced at least four transitions, two accepted, one residual, one CP2 effect, and one accepted mutation.

flowchart TD Packet["Execution packet transition candidates, CP2 requests, evolve mutations, oracle/provider refs"] Scan["Secret-exclusion scan over every input path"] Gate["Contract check forbidden field? oracle/provider visible? action class out of vocabulary?"] Rejected["CONTRACT_REJECTED no Lean run"] Build["lake build MicrocosmProofWitness once, in a temporary copy"] Run["Write .lean, run lake env lean return code 0 = accepted"] Verified["Accepted transition"] Residual["Residual non-zero return code"] Records["Four result records return codes and counts kept, bodies and proof text omitted"] Packet --> Scan Scan --> Gate Gate -->|leak found| Rejected Gate -->|clean| Build Build -->|return 0| Run Run -->|exit 0| Verified Run -->|non-zero| Residual Rejected --> Records Verified --> Records Residual --> Records

Negative cases

Four negative inputs the run must observe

The fixture ships four negative inputs listed in EXPECTED_NEGATIVE_CASES, each expected to raise one error code, and a run is blocked unless all four are observed. The fixture ships four negative inputs, each expected to raise one error code, declared in EXPECTED_NEGATIVE_CASES. A run that fails to observe all four is blocked.

• transition_leaks_candidate_body must raise VERIFIER_LAB_EXECUTION_TRANSITION_FIELD_FORBIDDEN: a candidate carrying a proof body or raw tactic script.
• provider_oracle_visible_transition must raise VERIFIER_LAB_EXECUTION_PROVIDER_OR_ORACLE_VISIBLE: a candidate that exposes an oracle structured source record or provider text to forward execution.
• cp2_candidate_contains_proof_body must raise VERIFIER_LAB_EXECUTION_CP2_PROOF_BODY_FORBIDDEN: a translation request that smuggles a proof body into the typed-action lane.
• evolve_mutates_unbounded_source must raise VERIFIER_LAB_EXECUTION_EVOLVE_SCOPE_FORBIDDEN: a mutation aimed outside the bounded policy artifacts.

Prior Art Grounding

Small-kernel trust and artifact evaluation

Execution follows the small-kernel proof-assistant tradition where trust rests on the checker not the tactic, and the record shape follows artifact-evaluation practice. The Lean and Lake execution inherits from the small-kernel proof-assistant tradition, the Lean theorem prover and LCF-style systems such as HOL Light, where trust rests on a small checker rather than the tactic that produced the term. The record shape follows artifact-evaluation practice: record the command identity, the tool facts, and the pass or fail counts separately from the claim they support, and keep the underlying artifact out of the summary.

Validation Result record Path

Run from microcosm-substrate:

What a green run proves

A green run counts as bounded execution-spine evidence only and never as general proof certification. A green run proves only bounded execution-spine evidence: command intent, tool facts, return-code pass or fail per candidate, the four observed negative cases, and the zero-held authority counters.