TruthMines: validate constituent libraries independently

[johnchandlerburnham]

This PR adds an independently addressable Benchmarks/Compile fidelity surface
for every native TruthMines library and for the standalone Palomar.ix aggregate,
then runs the full eight-phase ix validate pipeline over all of them.

The resulting validation matrix contains 79 targets:

• 78 native TruthMines member libraries, each validated through its own generated
  Benchmarks/Compile/TruthMines/Members/<Qualifier>.lean driver.
• Palomar.ix as one aggregate library, validated through
  Members/Palomar.lean without moving Palomar's isolated constituent
  workspaces or compatibility ports back into this repository.

All 79 targets pass.

The sweep also found and fixed a real compiler fidelity bug in generated indexed
.brecOn.eq declarations. Our Lean and Rust models of substCore preserved
forward dependencies in their original local-context positions, while Lean
actually reverts those declarations and reintroduces them after every unaffected
declaration. The resulting binder-order difference broke Plfl's
Compositional.Holed.brecOn.eq and Inference.TyS.brecOn.eq. Both compiler
implementations now reproduce Lean's ordering, and a source-contained regression
fixture pins the behavior.

Motivation

TruthMines already compiled each native library independently into a catalog
piece, but metadata fidelity was not exposed as an ordinary per-library
Benchmarks/Compile target. That made it unnecessarily difficult to:

• Run ix validate against one constituent without building or checking the
  complete corpus.
• Reproduce a failure using the same import closure as the catalog member.
• Distinguish a library-specific compiler failure from a catalog assembly or
  kernel-checking failure.
• Add the full corpus to the metadata-fidelity gate incrementally.
• Validate the standalone Palomar.ix port without importing its colliding source
  workspaces into the native TruthMines Lake workspace.

The new surface keeps the typed TruthMines records and generated canonical
workspace as the authority for native dependency pins. It adds only thin import
wrappers, plus one explicit pin for the independently maintained Palomar.ix
aggregate.

What changed

1. Generated per-library compile workspace

Benchmarks/Compile/TruthMines is a nested Lake workspace with one module per
validation target:

Benchmarks/Compile/TruthMines/
  lakefile.toml
  lake-manifest.json
  lean-toolchain
  Members/
    Cli.lean
    Mathlib.lean
    CompPoly.lean
    TauCeti.lean
    ...
    Palomar.lean

Each native wrapper is deliberately minimal:

import Drivers.<Qualifier>

The imported Drivers.<Qualifier> module is generated by the canonical
TruthMines workspace from the typed member record, so its roots and dependency
closure cannot drift into a second hand-maintained pin set.

The compile workspace:

• Depends on ../../TruthMines by path.
• Shares ../../TruthMines/.lake/packages rather than fetching another copy of
  the native dependency graph.
• Uses the repository's derived Lean toolchain.
• Pins Palomar.ix at
  879aba8e6c7419bf40549f470e8867ef52c12a54.
• Builds all member wrappers through the TruthMinesMembers library target.

The projection generator now owns the workspace configuration, toolchain, all
native member wrappers, and the Palomar aggregate wrapper. Therefore:

lake exe truthmines gen
lake exe truthmines gen --check

create and verify both the catalog workspace and the independent compile
workspace.

The fast truthmines-spec suite additionally checks that:

• Both nested workspaces use the derived repository toolchain.
• Every generated wrapper is byte-identical to its typed projection.
• The compile lockfile points at the canonical TruthMines path workspace.
• The compile lockfile uses the shared package directory.
• The direct Palomar.ix URL and revision match the projection constants.

2. Palomar.ix as one aggregate validation library

Palomar's 19 projects intentionally remain in isolated Lake workspaces because
their source module names collide. They cannot safely be imported as 19 peers in
one ordinary Benchmarks/Compile workspace.

Instead, the new Members/Palomar.lean imports Palomar.Main from the standalone
Palomar.ix repository. This
provides one coherent 207,030-constant validation environment while preserving
Palomar's repository boundary and the isolated workspaces used to build its
catalog pieces.

Palomar is included in the full validation tier and can be selected directly:

lake exe truthmines validate --only Palomar

It is not added to the native catalog member registry and is not included in the
mini tier.

3. Deterministic prebuild boundary for parallel validation

ix validate <file> normally performs its own Lake build before loading the
file environment. That is convenient for an interactive single-file command,
but it is unsafe for a corpus orchestrator to launch several validators against
one shared package store: each validator starts an independent Lake process, and
those processes can race while updating the same artifacts.

This appeared during a two-job Carleson/Cslib sweep as false cross-process
metadata corruption, including 167 Carleson identity mismatches such as
const name mismatch: Option vs Option. Carleson validated cleanly when run by
itself, confirming that the failure was in the build boundary rather than the
compiler result.

The TruthMines runner now:

1. Resolves the selected validation targets.
2. Builds all selected Members.<Qualifier> targets in one authoritative Lake
   process.
3. Waits for that process to complete.
4. Runs the requested number of validators over the quiescent package store.
5. Passes --no-build to each validator so it only loads and validates the
   already-built environment.

The single-job path uses the same prebuild boundary, so serial and parallel
sweeps exercise identical artifact state.

ix validate gains the opt-in flag:

ix validate Some/Driver.lean --no-build

The default behavior remains unchanged. Without --no-build, ix validate
still builds the source file and fetches the Mathlib cache when necessary.

The Mathlib cache lookup now reads a workspace's configured packagesDir from
lake-manifest.json instead of assuming .lake/packages. This makes the normal
interactive validation path work for the nested compile workspace as well.

4. Full per-library TruthMines validation command

truthmines validate now operates on validation libraries rather than catalog
member driver paths:

# All 78 native libraries plus Palomar.ix
lake exe truthmines validate

# A controlled subset
lake exe truthmines validate --only Mathlib,CompPoly,TauCeti,Palomar

# Parallel validation after one authoritative prebuild
lake exe truthmines validate --only Carleson,Cslib --jobs 2

# Native mini tier only
lake exe truthmines validate --mini

The existing watchdog and memory-ceiling behavior remains in place. The default
is still one validator at a time because Mathlib-scale validation retains both
compile and decompile state; --jobs is intended for explicitly chosen
small-member batches or suitably provisioned machines.

Every failure remains exit-code gated and names its validation target. No side
report artifact is required.

5. Indexed .brecOn.eq local-context fidelity

The full sweep was clean except for Plfl, where six checks failed across
aux-generation congruence, roundtrip aux congruence, and per-constant fidelity.
The reduced failures were:

• Compositional.Holed.brecOn.eq
• Inference.TyS.brecOn.eq

Both declarations are generated for indexed inductives with constructor fields
whose dependency sets overlap only after an earlier index substitution.

Lean's substCore behavior is significant here. It:

1. Reverts the abstracted free variable and all forward dependencies.
2. Introduces the equality proof machinery.
3. Reintroduces the forward dependencies after every unaffected local
   declaration.

For a constructor shaped like:

C : I i j -> T j -> I i j

substituting i first moves the recursive I field behind the unaffected
T field. A subsequent substitution of j must therefore discover forward
dependencies in T, I order.

The old Ix model substituted forward dependencies in place. That preserved the
stale I, T order and generated an observably different proof telescope. The
fix, mirrored in Lean and Rust, is to:

• Remove the abstracted variable and the old forward-dependency declarations.
• Preserve unaffected local declarations in place.
• Append the substituted forward dependencies in revert order.

The new TypeBrecOnForwardDepOrder fixture includes recursive-then-payload and
payload-then-recursive constructor shapes. It reproduces the ordering condition
without importing Plfl and runs through the existing aux-generation validation
suite.

Validation results

All 79 independently addressable libraries pass the complete ix validate
pipeline. Notable large environments include:

Validation target	Constants	Result
Mathlib	771,135	Pass
FLT	780,912	Pass
Fad	797,651	Pass
TauCeti	646,279	Pass
Plfl	436,268	Pass
CompPoly	382,408	Pass
Palomar.ix	207,030	Pass

Plfl's final run reported zero failures in every phase:

• Compilation: 436,268 / 436,268.
• Aux-generation congruence: 13,991 / 13,991 over 4,171 unique blocks.
• No ephemeral leaks: 14,319 / 14,319.
• Alpha-equivalence canonicity: 4,681 / 4,681.
• Decompile with debug: 422,197 / 422,197, with zero aux-generation errors.
• Aux congruence after roundtrip: 14,319 / 14,319.
• Decompile without debug: 422,197 / 422,197, with zero aux-generation errors.
• Per-constant roundtrip fidelity: 436,268 / 436,268.

The complete generated TruthMinesMembers library also builds successfully
(14,850 Lake jobs), establishing that every independent driver elaborates in
the shared workspace before validation begins.

The Carleson/Cslib two-job regression sweep is clean with the new prebuild
boundary and no longer launches Lake from the individual validator processes.

Tests

The following checks are green:

nix develop --command lake lint
nix develop --command lake build ix truthmines Tests.Ix.TruthMinesRecords
nix develop --command lake test --wfail -- truthmines-spec
nix develop --command lake test --wfail -- --ignored validate-aux
nix develop --command lake exe truthmines gen --check
nix develop --command cargo fmt --all -- --check
nix develop --command cargo clippy --workspace --all-targets --all-features

The generated compile workspace was built with:

cd Benchmarks/Compile/TruthMines
nix develop --command lake build TruthMinesMembers

The 79 validation targets were exercised in controlled batches through
truthmines validate --only ..., with focused reruns for the concurrency and
Plfl regressions.

Review guide

The change is easiest to review in four layers:

1. Projection and workspace shape

   • Benchmarks/TruthMinesSpec/Projection.lean
   • Benchmarks/Compile/TruthMines/lakefile.toml
   • Representative native and Palomar wrappers
   • Tests/Ix/TruthMinesRecords.lean

2. Validation orchestration

   • Benchmarks/TruthMinesSpec/Main.lean
   • Ix/Cli/ValidateCmd.lean
   • Ix/Meta.lean

3. Compiler fidelity fix

   • crates/compile/src/compile/aux_gen/brecon.rs
   • Ix/AuxGen/BRecOn.lean

4. Regression fixture and documentation

   • Tests/Ix/Compile/Mutual.lean
   • Tests/Ix/TruthMines.lean
   • Benchmarks/Compile/README.md

Most of the file count is generated two-line member wrappers and the Lake
lockfile. The substantive logic is concentrated in the files listed above.

Compatibility and risk

• ix validate retains its existing build behavior unless callers explicitly
  pass --no-build.
• Native dependency pins still come exclusively from the typed TruthMines
  records and canonical generated workspace.
• Palomar.ix is the only new direct git pin in the compile workspace.
• The .brecOn.eq change makes both Ix implementations match Lean's actual
  local-context ordering and is covered by the same eight-phase fixture pipeline
  used to diagnose the external failure.
• Full-corpus validation remains intentionally expensive and serial by default;
  this PR does not weaken watchdog or memory-ceiling enforcement.

Non-goals

• Moving Palomar's ports or source workspaces back into this repository.
• Importing Palomar's 19 colliding projects as native peers in one Lake
  workspace.
• Changing native TruthMines catalog membership or .ixc composition.
• Changing the default build semantics of interactive ix validate commands.
• Making the full validation sweep a fast, always-run CI job.

[arthurpaulino]

!benchmark aiur-sharded-env

[argument-ci-bot]

!benchmark — main vs 697fd8c

backends: aiur-sharded-env · envs: ISLB

aiur-sharded-env · ISLB — main from: bencher @ 0f34977

1 constant · 0 with regressions · 1 with improvements (|Δ| > 3.0% on any metric).

constant	check-time (main)	check-time (PR)	Δ%	throughput (const/s) (main)	throughput (const/s) (PR)	Δ%	peak-ram (main)	peak-ram (PR)	Δ%	constants (main)	constants (PR)	Δ%	shards (main)	shards (PR)	Δ%
ISLB	1m 21.7s	1m 18.9s	-3.4% 🟢	2.24K	2.32K	+3.5% 🟢	94.18 GiB	96.14 GiB	+2.1%	183,062	183,062	+0.0%	151	151	+0.0%

Workflow logs