Complete anonymous checking of AnthropicFLT and reduce repeated kernel work

[johnchandlerburnham]

Make anonymous FLT checking complete and reduce repeated kernel work

Draft scope: jcb/anthropic-flt-check, including the current uncommitted
dependent-prefix/profiling follow-ups. Intended stacked base:
jcb/anthropic-flt-benchmark (a527d950), or main after that branch lands.
Against current main, this branch also includes the earlier FLT compiler
benchmark, memory scheduling, and compiler DAG-memoization changes; those
are described separately in plans/anthropic-flt-benchmark-pr.md.
No PR has been opened by writing this file.

Summary

Make the Rust kernel complete anonymous checking of the Anthropic FLT
environment, while reducing repeated inference/substitution work and
bounding unproductive conversion speculation.

The committed checkpoint (40623162) checks all 1,321,973 FLT constants
with zero failures in 613.152 seconds, at a 100M per-declaration fuel cap.
The previously remaining failure is resolved by controlling optional
same-head comparison work, not by treating exhausted fuel as a verdict or
increasing the cap again.

The newest dependent-prefix cache and bounded hot-miss profiler have passed
local Mathlib validation. Their remote FLT validation is in progress; the
checkpoint result above must not be attributed to those follow-ups until
the new full run completes.

Changes

Reduce inference, allocation, and traversal overhead

• Batch lambda/forall inference and dependent application inference. Delay
  codomain substitution, instantiate each domain when needed, and preserve
  all argument/annotation checks in full inference mode. Keep small-term
  paths and existing usable prefix-cache hits.
• Add conservative declaration summaries to avoid proof-irrelevance probes
  for known non-proof terms. Unknown summaries fall back to ordinary work;
  summaries do not establish equality or validate declarations.
• Selectively cache repeated dependent application prefixes. Materialize
  at most one extra dependent suffix per spine, preserve the remaining
  batched substitution, and publish results only under the existing exact
  context-sensitive, full/infer-only cache contracts.
• Reduce unnecessary expression allocation and repeated shared-DAG walks;
  adapt substitution scratch-table allocation to recent occupancy without
  retaining logical entries between independent traversals.
• Accelerate persistent closure-environment lookup while preserving captured
  environments and constant-time extension. Retain a small-offset fast path.
• Keep cross-work-item allocation-capacity reuse opt-in. Its default remains
  zero; retaining buckets never retains logical memo entries.

Keep optional conversion work bounded

• Try projection equality before comparing entire record values, with the
  ordinary comparison as fallback.
• Add positive-only batched binder congruence and iterative application
  congruence. The latter is a bounded near-depth-guard fallback, not a blanket
  replacement for ordinary conversion on small applications.
• Bound same-head probes to 131,072 fuel for Regular definitions and 4,096
  for other hints, with nested probes sharing the remaining slice.
• Back off new Regular root probes after 33,554,432 fuel in unsuccessful
  root attempts within a declaration. Successful attempts do not charge
  this history, and nested work is counted only once in its root. This is
  admission history, not an equality/inequality cache or per-head blacklist.
• Raise the branch's default cumulative fuel allowance from 10M to 100M,
  retaining the separate depth and WHNF guards and IX_MAX_REC_FUEL
  override. The final same-head and prefix-cache experiments hold 100M fixed.

Correctness fixes and diagnostics

• Preserve source recursor peer ordering in direct Lean ingress. Replace
  unrealistic round-trip fixtures with independently transcribed source
  recursors, including nested and alpha-collapsed examples; retain negative
  tests for swapped types and extra peers.
• Split large conversion frames to reduce native stack pressure. The kernel
  unit suite runs without an external RUST_MIN_STACK override; this does
  not make all kernel traversals stack-independent or remove the CLI's
  existing worker-stack reservation.
• Add an anonymous isolated-subject helper and a Lean-driven FLT regression
  suite, with a pinned corpus, matched resource limits, preserved binaries,
  raw measurements, and explicit reporting of verdict/work changes.
• Add opt-in same-head accounting and a bounded hot-miss heavy-hitter report.
  Hot misses retain at most 4,096 keys and 512-byte labels; late hotspots can
  replace cold entries. Reports show count intervals after replacement,
  not misleading exact totals or an alleged total distinct-key count.
  Oversized metadata names, naturals, and universes cannot force unbounded
  diagnostic rendering. No expression graphs are retained by these counters.

Correctness boundaries

• Application/binder congruence publishes equality only after the required
  child/domain/body comparisons succeed. Pending pairs are never facts.
  A failed or exhausted optional probe is inconclusive and falls back;
  consumed work is charged, never refunded.
• Validated inference results may serve either mode. Infer-only results
  never satisfy full checking. Cache keys retain context, expression, and
  universe identity; fresh FVar identities are not reused across live caches.
• Prefix-admission fingerprints only choose when to compute a result. A
  collision can change extra work or lose a cache opportunity, but cannot
  supply a type, merge semantic keys, or establish validity.
• Delayed application substitution uses ambient-context substitution with
  lifting under surviving binders, not an FVar-only substitution shortcut.
• Declaration summaries are conservative under symbolic universe
  assignments and invalidate with their environment. They do not promote
  lazily loaded dependencies into independently verified declarations.
• These changes do not replace the kernel with an NbE/closure-conversion
  backend or introduce new proof rules. Existing Lean semantic lemmas help
  explain the rules; they are not a formal certification of these Rust loops.

Validation and performance

Results use existing, unchanged version-2 .ixe inputs in anonymous mode.
Full-corpus checking checks every kernel-checkable target; focused subjects
trust dependencies and are diagnostic benchmarks, not full verification.

Gate	Variant and conditions	Result
Kernel unit suite	Current follow-ups, diagnostics off and on, no external stack override	838 passed, 8 ignored
Formatting, strict kernel Clippy, Lean driver self-tests, native CLI build	Current follow-ups	Pass locally; remote 838-test suite and native builds also pass
Full Mathlib	Current final candidate, 8 workers, 100M fuel, no per-item CSV	672,981 / 672,981 pass; 240.818 s; ~3.25 GiB sampled peak RSS
Matched whole-Mathlib pair	Committed checkpoint vs prefix cache, 8 workers, both with per-item CSV	Both pass; 282.628 → 285.180 s (+0.9% in one pair); ~4.76 GiB sampled peak RSS on both
Full Anthropic FLT	Committed checkpoint, 64 workers, 100M fuel	1,321,973 / 1,321,973 pass; 613.152 s; 102.84 GiB GNU-time peak RSS
Focused FLT and full FLT	Current prefix-cache/profiling follow-ups	Pending; update after remote validation

The matched Mathlib pair does not demonstrate a throughput improvement.
Its aggregate predicted Zisk work-cost decreases 1.5%, but that is a model,
not measured guest cycles. Some declarations do extra interner work from
newly materialized types. Do not describe this as a pure per-declaration win.
The 240.818-second gate omits CSV attribution and is not the comparable
denominator for that matched pair.

The earlier last failing FLT subject (6c43f78d96e1…) passed in isolation
at 35.49M fuel / 30.285 s after conservative same-head backoff. Full-corpus
time was essentially unchanged versus the immediately prior one-failure
run (613.152 vs 612.422 s). This is a completion improvement, not a claim
of a large additional whole-FLT speedup from backoff alone.

An earlier aggressive backoff policy passed isolated cases but introduced
three failures in full FLT; it was rejected. Those declarations and other
high-fuel positive controls are retained in the regression inventory.

Reproduction

nix develop --offline --command cargo test -p ix-kernel --lib --offline
nix develop --offline --command cargo clippy -p ix-kernel --lib --tests \
  --offline -- -D warnings
nix develop --offline --command lean --run \
  Benchmarks/Kernel/AnthropicFLT/RunSuite.lean --self-test

# Build the CLI first; reuse the pinned existing FLT artifact.
lake exe ix check-rs /path/to/flt-after-source-hints-1.ixe --anon --workers 64

For comparative timing, freeze both binaries and use clean environments,
identical inputs/worker counts/fuel caps, and external memory/time limits.
See Benchmarks/Kernel/AnthropicFLT/README.md for the subject-only protocol,
manifest budgets, and diagnostic switches. The remote full check uses a
420 GiB memory limit, no swap, and a 3,600-second timeout; these are external
safeguards, not changes to kernel acceptance.