diff --git a/Benchmarks/Kernel/AnthropicFLT/README.md b/Benchmarks/Kernel/AnthropicFLT/README.md
new file mode 100644
index 000000000..c576219cb
--- /dev/null
+++ b/Benchmarks/Kernel/AnthropicFLT/README.md
@@ -0,0 +1,192 @@
+# Focused anonymous FLT regression suite
+
+Use this for the inner optimization loop, before whole-Mathlib/FLT checks.
+The kernel checks each selected **work item only**, trusting lazily ingressed
+dependencies. This is a diagnostic benchmark, not full-corpus verification.
+Declaration names and expression metadata are not needed or loaded.
+
+For separate diagnostics, `IX_GUARD_STACKS=1` on the subject helper emits
+bounded native stacks at resource guards. `IX_DEF_EQ_NEAR_GUARD=1` emits
+bounded expression-pair summaries near the depth limit. Leave both off
+for paired timings. Guard fuel counters inside a speculative comparison
+describe its temporary slice; the final helper report accounts for the
+actual total work charged to the subject.
+
+For separate cache/reduction diagnostics, the subject helper prints cache
+hit rates to stderr with `IX_PERF_COUNTERS=1`, and the top 20 delta/iota
+addresses with `IX_REDUCE_HISTO=1`. Histogram totals include addresses beyond
+the displayed top 20. These counters measure reduction events, not proof
+size or unique allocations. Diagnostics leave the subject JSON unchanged;
+keep both flags unset for paired timings.
+
+`IX_SAME_HEAD_PROFILE=1` reports actual same-head comparisons by outcome
+and definition head. Inclusive fuel overlaps across nested attempts;
+exclusive and root fuel do not double-count it. Window skips and rejected-
+probe cache hits are separate from attempts. Failed-attempt fuel is not
+necessarily all avoidable: attempts may also populate useful caches.
+Per-head attribution is bounded and holds no expression graphs. Leave this
+flag unset for clean paired timing runs; subject JSON stays unchanged.
+
+The same-head report also ranks roots separately and prints at most 32
+expensive root-pair snapshots (at least 65,536 fuel) per thread/check.
+These carry expression uids, the legacy context identity, and compact shapes;
+they do not canonicalize free variables or claim alpha-equivalence.
+`IX_HOT_MISSES=1` prints the final member's top 25 miss shapes once when the
+subject helper finishes; add `IX_HOT_MISS_CTX=1` for context keys. It does
+not require the much noisier per-guard `IX_REC_FUEL_DUMP`.
+The hot-miss collector retains at most 4,096 keys, with labels capped at
+512 UTF-8 bytes. Its Space-Saving summary can discover late hotspots by
+replacing low-frequency entries. Printed counts are lower/upper bounds
+(exact before replacement); the number of retained keys is **not** the
+total number of distinct misses. Exact expression/context identities, not
+truncated labels, distinguish keys. No expression graphs are retained, and
+the collector resets per member. Leave it off for clean timings.
+
+Application inference selectively caches repeated dependent prefixes using
+the existing exact context-sensitive keys and separate full/infer-only result
+caches. Only successful inference publishes a prefix type; a bounded two-touch
+fingerprint filter merely nominates work and never supplies a type or a
+validity judgment. Each spine materializes at most one extra dependent suffix
+for caching, leaving the remaining telescope substitution batched. The
+admission history resets per member and retains at most 32 KiB of slots. With
+`IX_PERF_COUNTERS=1`, `dependent_prefix_inserts` counts these materializations.
+
+Same-head congruence probes use a 131,072-fuel slice for Regular definitions
+and 4,096 for other hints. Nested probes inherit the remaining allowance.
+Exhaustion resumes ordinary unfolding with consumed work charged to the
+check; it does not establish inequality. Regular root probes back off after
+33,554,432 fuel in unsuccessful attempts across the declaration. This is an
+admission threshold: the last admitted attempt can cross it by up to its
+allowance. There is no per-head blacklist. Successful roots do not charge
+the history;
+nested work is charged only as part of its unsuccessful root. Skips resume
+ordinary unfolding, and `skipped_backoff` is reported separately from actual
+attempts. This constant-space history resets per member; it is not a
+semantic cache.
+Non-Regular probes retain their startup window, measured in actual work
+rather than temporarily withheld fuel. The per-constant fuel cap is unchanged.
+
+To resolve anonymous addresses to names without decoding expression
+metadata, use the `resolve_anon_names` Rust example with `FILE.ixe` followed
+by hex prefixes (8–64 digits). It prints all aliases, not a single guessed
+name. This separate diagnostic reads the full file into RAM: apply an
+appropriate memory limit for large artifacts. Name lookup is not checking.
+
+`cases.json` pins the exact existing `.ixe` by SHA-256 and byte length. It
+tracks 138 target addresses: 120 fuel failures, four depth failures, five
+unfinished tails, and nine passing-baseline controls. The default **25-case core**
+contains all five original tails, all four depth cases, ten fuel failures,
+and six positive controls. Five fuel cases were promoted
+from the existing extended inventory after they formed the final tail of
+the completed 100M full FLT run; no addresses were duplicated. The positive
+control that needed 558 seconds in the original full sweep belongs to the
+extended suite. The remaining V3 failure `fuel-6c43f78d96e1` is also promoted
+with 100M fuel and a 300-second timeout, without adding a duplicate address.
+
+Six controls were added after early backoff V5 regressed the full FLT sweep.
+The three new failures (`50cb089d71a0`, `6234fd409441`, `7bf34ca3444c`) and
+V3's highest-fuel passing subject (`6303d6c017f7`, 28.385M) are in the core.
+Two near-cap V5 passes (`bfeba60bbbc6`, `eac5f4ec9db3`) are extended controls.
+All six have explicit 100M/300-second budgets. Their recorded observations
+are full-sweep results under contention, not isolated benchmark timings.
+
+Initial observations came from the stopped `28fc2270` full FLT run at 40M
+fuel and 64 workers, plus the earlier bounded single-subject trials. The
+five new core cases are `fuel-f38456f556fd`, `fuel-f5ebaf348a49`,
+`fuel-fa1b74facf9a`, `fuel-fbba56420b6b`, and `fuel-fdfcfa70a9e8`. Each
+exhausted 100M fuel in `check-flt-fuel100m-v1-1` (September 6, 2026).
+Their recorded full-run times are under 64-worker contention, not isolated
+benchmark results. Resolved names/aliases in the manifest are descriptive
+only: execution remains anonymous and addresses are authoritative. Resource
+failures are not expected kernel rejections: fuel/depth limits leave checking
+unresolved.
+“Unfinished” does not establish a deadlock. Addresses identify declarations
+in this pinned artifact; do not substitute a rebuilt corpus silently.
+
+## Build and run
+
+Build the same `check_anon_subject` example against each kernel variant,
+using the same native CPU/toolchain/feature settings. Preserve both binaries
+under distinct filenames before running; never rebuild while measuring.
+
+```sh
+nix develop --offline --command cargo build -p ix-ffi --release \
+ --example check_anon_subject --features parallel,net --offline
+```
+
+On the Linux CPU box, run inside tmux. The harness is Lean (`import Lean`
+only; no project rebuild needed). It uses GNU time/timeout, systemd, and
+noninteractive sudo for the per-process scopes.
+The output directory must not exist. No corpus is copied or rebuilt.
+
+```sh
+lean --run Benchmarks/Kernel/AnthropicFLT/RunSuite.lean \
+ --ixe /path/to/flt-after-source-hints-1.ixe \
+ --baseline /path/to/check-subject-baseline \
+ --adaptive /path/to/check-subject-adaptive \
+ --output /path/to/new-run-directory
+```
+
+Use `--case tail-04e32656609b` (repeatable) for a tiny iteration, `--rounds 3`
+for repeated pairs, or `--suite all` for the extended set. The extended set
+can take much longer; it is not the default inner loop.
+
+The preflight resolves every recorded target to its work-item primary in
+**both** binaries, without checking it. Both resolutions must agree.
+Members of the same mutual block are deduplicated for matching fuel budgets.
+Each timed invocation has a fresh process/KEnv, one checker worker, the
+manifest's fixed fuel cap, 96 GiB MemoryMax, and zero MemorySwapMax. Defaults
+are 40M fuel and 120 seconds per process; the 17.1M-fuel passing control uses
+20M, and the extended slow positive control gets 600 seconds. The five
+newly promoted tail cases explicitly use **100M fuel and 300 seconds per
+process**, still one worker and 96 GiB/no swap. The original 15 cases keep
+their old budgets for comparable performance regressions; the additional
+V3 failure and the six backoff controls also have explicit 100M/300-second
+budgets. Raising the
+kernel default does not override the manifest. Pair order
+alternates across cases and rounds. Hot-miss/perf/step diagnostics are off.
+
+## Results and interpretation
+
+- `run.json`: complete manifest, selected IDs, artifact and binary hashes,
+ file identities, host, driver hash, and start time. `source/` preserves
+ the explicit prototype source files and pinned Cargo/toolchain inputs.
+- `resolved.json`: target-to-primary mapping and deduplicated selected work.
+- `results.jsonl`: flushed after every invocation, even if a later one times
+ out. Contains outcome, raw helper report, wall/CPU time and peak RSS.
+- Per-invocation `.log`, `.stderr.log`, `.time.json`, and `.command.json`:
+ original evidence, exact argv, and the unique cgroup scope name. Both
+ streams are flushed as they arrive, and the harness prints a heartbeat
+ every 30 seconds. Caught orchestration errors clean up only that scope;
+ the child's independent timeout remains in force if the harness is killed.
+- `summary.json`: written only after all scheduled pairs finish; compares
+ completed results/work counts and checker times. A completed *harness*
+ does not mean its subjects all passed. Read each outcome.
+
+Checker time excludes initial mmap/enumeration; whole-process time includes
+load, checking, and teardown. Peak RSS includes the whole helper process,
+not just scratch storage. A timeout is censored, not a kernel failure or an
+exact checker-time measurement; no speedup ratio is manufactured from it.
+Exit 137 is reported as `killed`, not automatically called OOM. Missing time
+or JSON data remains missing. Compare fuel usage only under matched caps.
+
+The helper's `last_member_fuel` and `last_member_def_eq_peak` refer to the
+last checked member. The latter is a **definitional-equality depth metric**,
+not an overall peak infer/WHNF recursion-depth measurement. Do not label
+these as block aggregates. Operation counts span the work item; aggregate
+fuel is unavailable with perf diagnostics disabled.
+
+For the storage-only scratch change, completed outcomes and work/fuel counts
+should agree. The driver flags mismatches without treating timeout cases as
+passes. For algorithmic optimizations such as batched binder inference,
+explicitly pass `--allow-work-changes`: changed work/fuel/depth counts are
+still recorded, but labeled `same_outcome_changed_work` when the verdict,
+error, and target count agree. Verdict/error/target changes remain mismatches
+requiring review; timeouts remain incomplete. The selected policy is saved
+in `run.json`; the default storage-only policy is unchanged. Keep passing
+controls, kernel tests, Mathlib, and periodic full FLT sweeps as separate
+correctness and whole-run performance gates.
+
+```sh
+lean --run Benchmarks/Kernel/AnthropicFLT/RunSuite.lean --self-test
+```
diff --git a/Benchmarks/Kernel/AnthropicFLT/RunSuite.lean b/Benchmarks/Kernel/AnthropicFLT/RunSuite.lean
new file mode 100644
index 000000000..6831cb0e8
--- /dev/null
+++ b/Benchmarks/Kernel/AnthropicFLT/RunSuite.lean
@@ -0,0 +1,489 @@
+import Lean
+
+/-!
+Bounded paired anonymous FLT subject checks, orchestrated in Lean.
+No builds, downloads, corpus rewriting, or full-environment checks occur here.
+The Rust subject helper trusts dependencies. See README.md for scope/metrics.
+-/
+
+open Lean System
+
+namespace Benchmarks.AnthropicFLT
+
+def suiteDir : FilePath := "Benchmarks/Kernel/AnthropicFLT"
+
+structure Case where
+ id : String
+ address : String
+ category : String
+ core : Bool
+ fuel : Option Nat := none
+ timeout_seconds : Option Nat := none
+ deriving FromJson, ToJson, Inhabited
+
+structure Defaults where
+ fuel : Nat
+ timeout_seconds : Nat
+ memory_gib : Nat
+ workers : Nat
+ deriving FromJson, ToJson
+
+structure Artifact where
+ filename : String
+ bytes : Nat
+ sha256 : String
+ deriving FromJson, ToJson
+
+structure Manifest where
+ schema : Nat
+ artifact : Artifact
+ defaults : Defaults
+ cases : Array Case
+ deriving FromJson
+
+structure Resolution where
+ requested : String
+ primary : String
+ targets : Nat
+ deriving FromJson, ToJson, BEq, Inhabited
+
+structure Group where
+ primary : String
+ targets : Nat
+ fuel : Nat
+ timeoutSeconds : Nat
+ caseIds : Array String
+ categories : Array String
+ requested : Array String
+ deriving ToJson, Inhabited
+
+def isHex (s : String) : Bool :=
+ s.length == 64 && s.toList.all (fun c => c.isDigit || ('a' ≤ c && c ≤ 'f'))
+
+def isId (s : String) : Bool :=
+ !s.isEmpty && s.toList.all (fun c => c.isLower || c.isDigit || c == '-')
+
+def need (value : Except String α) : IO α :=
+ match value with
+ | .ok a => pure a
+ | .error e => throw (IO.userError e)
+
+def validate (m : Manifest) : Except String Unit := do
+ unless m.schema == 1 && isHex m.artifact.sha256 do throw "invalid manifest/artifact"
+ unless m.defaults.workers == 1 do throw "suite requires one fresh worker"
+ unless 0 < m.defaults.memory_gib && m.defaults.memory_gib ≤ 96 do
+ throw "memory budget must be between 1 and 96 GiB"
+ let mut ids := #[]
+ let mut addresses := #[]
+ for c in m.cases do
+ unless isId c.id && !ids.contains c.id do throw "invalid or duplicate case ID"
+ unless isHex c.address && !addresses.contains c.address do throw "invalid or duplicate address"
+ unless #["tail", "depth", "fuel", "control"].contains c.category do throw "unknown category"
+ let fuel := c.fuel.getD m.defaults.fuel
+ let timeout := c.timeout_seconds.getD m.defaults.timeout_seconds
+ unless 0 < fuel && fuel ≤ 100000000 do throw "invalid fuel budget"
+ unless 0 < timeout && timeout ≤ 600 do throw "invalid time budget"
+ ids := ids.push c.id
+ addresses := addresses.push c.address
+
+def normalize (cases : Array Case) (rows : Array Resolution) (d : Defaults) :
+ Except String (Array Group) := do
+ let mut groups : Array Group := #[]
+ for c in cases do
+ let some r := rows.find? (·.requested == c.address) | throw s!"unresolved target {c.address}"
+ unless isHex r.primary && r.targets > 0 do throw "invalid resolver output"
+ let fuel := c.fuel.getD d.fuel
+ let timeout := c.timeout_seconds.getD d.timeout_seconds
+ if let some i := groups.findIdx? (fun g => g.primary == r.primary && g.fuel == fuel) then
+ let g := groups[i]!
+ groups := groups.set! i { g with
+ timeoutSeconds := max g.timeoutSeconds timeout
+ caseIds := g.caseIds.push c.id
+ categories := g.categories.push c.category
+ requested := g.requested.push c.address }
+ else
+ groups := groups.push {
+ primary := r.primary, targets := r.targets, fuel, timeoutSeconds := timeout
+ caseIds := #[c.id], categories := #[c.category], requested := #[c.address] }
+ return groups
+
+def field (j : Json) (key : String) : Json := (j.getObjVal? key).toOption.getD .null
+def str (j : Json) (key : String) : String := (j.getObjValAs? String key).toOption.getD ""
+
+def classify (code : Nat) (report : Json) : String := Id.run do
+ if code == 124 then return "timeout"
+ if code == 137 then return "killed" -- Not automatically an OOM diagnosis.
+ if code ≥ 128 then return "crash"
+ if str report "scope" != "subject-only" then return "harness_error"
+ if code == 0 && field report "passed" == toJson true then return "pass"
+ if code != 1 || field report "passed" != toJson false then return "harness_error"
+ return match str report "error" with
+ | "recursive fuel exhausted" => "fuel_exhausted"
+ | "max recursion depth exceeded" => "depth_exceeded"
+ | _ => "kernel_error"
+
+def compare (baseline adaptive : Json) (allowWorkChanges : Bool := false) : Json := Id.run do
+ let a := str baseline "outcome"
+ let b := str adaptive "outcome"
+ let mut result := Json.mkObj [("baseline", toJson a), ("adaptive", toJson b)]
+ let incomplete := #["timeout", "killed", "crash", "harness_error"]
+ if incomplete.contains a || incomplete.contains b then
+ return result.setObjVal! "comparison" (toJson "incomplete")
+ let ar := field baseline "report"
+ let br := field adaptive "report"
+ let keys := #["passed", "error", "targets", "last_member_fuel", "last_member_def_eq_peak",
+ "subst", "whnf", "def_eq", "intern", "nat_arith"]
+ let mismatches := keys.filter (fun k => field ar k != field br k)
+ result := result.setObjVal! "mismatched_fields" (toJson mismatches)
+ let verdictChanged := a != b ||
+ #["passed", "error", "targets"].any (fun k => field ar k != field br k)
+ result := result.setObjVal! "comparison" (toJson
+ (if verdictChanged then "mismatch"
+ else if mismatches.isEmpty then "same_outcome_and_work"
+ else if allowWorkChanges then "same_outcome_changed_work"
+ else "mismatch"))
+ if let (.ok baseTime, .ok adaptiveTime) :=
+ (ar.getObjValAs? Float "check_secs", br.getObjValAs? Float "check_secs") then
+ if baseTime > 0 then
+ result := result.setObjVal! "adaptive_over_baseline_check_time" (toJson (adaptiveTime / baseTime))
+ return result
+
+def announce (message : String) : IO Unit := do
+ IO.println message
+ (← IO.getStdout).flush
+
+def saveJson (path : FilePath) (j : Json) : IO Unit := do
+ if ← path.pathExists then throw (IO.userError s!"refusing to overwrite {path}")
+ IO.FS.writeFile path (j.pretty ++ "\n")
+
+def lastJson (path : FilePath) : IO Json := do
+ if !(← path.pathExists) then return .null
+ let mut result := Json.null
+ for line in (← IO.FS.readFile path).splitOn "\n" do
+ if let .ok (.obj obj) := Json.parse line then result := .obj obj
+ return result
+
+def checkedOutput (cmd : String) (args : Array String) : IO String := do
+ let r ← IO.Process.output { cmd, args }
+ unless r.exitCode == 0 do throw (IO.userError s!"{cmd}: {r.stderr}")
+ return r.stdout.trimAscii.toString
+
+def digest (path : FilePath) : IO String := do
+ let output ← checkedOutput "sha256sum" #["--", path.toString]
+ let hash := (output.splitOn " ").head!
+ unless isHex hash do throw (IO.userError "invalid sha256sum output")
+ return hash
+
+def identities (paths : Array FilePath) : IO (Array String) :=
+ paths.mapM fun p => checkedOutput "stat" #["-c", "%d:%i:%s:%y", "--", p.toString]
+
+def timeFormat : String :=
+ "{\"elapsed_seconds\":%e,\"user_seconds\":%U,\"system_seconds\":%S,\"peak_rss_kib\":%M,\"exit_code\":%x}"
+
+def scopeArgs (unit user : String) (binary : FilePath) (args : Array String)
+ (timing : FilePath) (seconds fuel memory : Nat) : Array String :=
+ #["-n", "systemd-run", "--quiet", "--scope", s!"--unit={unit}",
+ "-p", s!"MemoryMax={memory}G", "-p", "MemorySwapMax=0",
+ "sudo", "-u", user, "/usr/bin/env", "-i", "PATH=/usr/bin:/bin", "LANG=C", "LC_ALL=C",
+ "LEAN_NUM_THREADS=1", "RAYON_NUM_THREADS=1", s!"IX_MAX_REC_FUEL={fuel}",
+ "/usr/bin/time", "-f", timeFormat, "-o", timing.toString,
+ "/usr/bin/timeout", "--signal=TERM", "--kill-after=10s", toString seconds,
+ binary.toString] ++ args
+
+partial def pump (src dst : IO.FS.Handle) (echo : Bool) : IO Unit := do
+ let line ← src.getLine
+ unless line.isEmpty do
+ dst.putStr line
+ dst.flush
+ if echo then
+ (← IO.getStdout).putStr line
+ (← IO.getStdout).flush
+ pump src dst echo
+
+structure Invocation where
+ exitCode : Nat
+ report : Json
+ timing : Json
+ wrapperSeconds : Float
+
+def limited (binary : FilePath) (args : Array String) (out : FilePath)
+ (name runId user : String) (seconds fuel memory : Nat) : IO Invocation := do
+ let unit := s!"ix-flt-suite-{runId}-{name}"
+ let timing := out / s!"{name}.time.json"
+ let argv := scopeArgs unit user binary args timing seconds fuel memory
+ saveJson (out / s!"{name}.command.json") (Json.mkObj [
+ ("unit", toJson unit), ("argv", toJson (#["sudo"] ++ argv))])
+ announce s!"START {name}: timeout={seconds}s fuel={fuel} memory={memory}GiB"
+ let log ← IO.FS.Handle.mk (out / s!"{name}.log") .write
+ let err ← IO.FS.Handle.mk (out / s!"{name}.stderr.log") .write
+ let child ← IO.Process.spawn {
+ cmd := "sudo", args := argv, stdin := .null, stdout := .piped, stderr := .piped, setsid := true }
+ let stdoutTask ← IO.asTask (pump child.stdout log false) .dedicated
+ let stderrTask ← IO.asTask (pump child.stderr err true) .dedicated
+ let start ← IO.monoMsNow
+ let mut lastNotice := start
+ let code ← try
+ let mut status : Option UInt32 := none
+ while status.isNone do
+ status ← child.tryWait
+ if status.isNone then
+ let now ← IO.monoMsNow
+ if now - start > (seconds + 40) * 1000 then
+ throw (IO.userError s!"scope wrapper exceeded timeout for {name}")
+ if now - lastNotice ≥ 30000 then
+ announce s!"WAIT {name}: {(now - start) / 1000}s (process cap {seconds}s)"
+ lastNotice := now
+ IO.sleep 250
+ pure status.get!
+ catch e =>
+ let _ ← IO.Process.output { cmd := "sudo", args := #["-n", "systemctl", "kill",
+ "--signal=KILL", "--kill-whom=all", unit] }
+ child.kill
+ throw e
+ IO.ofExcept stdoutTask.get
+ IO.ofExcept stderrTask.get
+ let report ← lastJson (out / s!"{name}.log")
+ let measured ← lastJson timing
+ let finish ← IO.monoMsNow
+ return {
+ exitCode := code.toNat
+ report := report
+ timing := measured
+ wrapperSeconds := (finish - start).toFloat / 1000
+ }
+
+structure Options where
+ ixe : String := ""
+ baseline : String := ""
+ adaptive : String := ""
+ output : String := ""
+ manifest : String := (suiteDir / "cases.json").toString
+ all : Bool := false
+ cases : Array String := #[]
+ rounds : Nat := 1
+ selfTest : Bool := false
+ allowWorkChanges : Bool := false
+
+def parseArgs : List String → Options → Except String Options
+ | [], opts => .ok opts
+ | "--self-test" :: rest, opts => parseArgs rest { opts with selfTest := true }
+ | "--allow-work-changes" :: rest, opts => parseArgs rest { opts with allowWorkChanges := true }
+ | "--ixe" :: v :: rest, opts => parseArgs rest { opts with ixe := v }
+ | "--baseline" :: v :: rest, opts => parseArgs rest { opts with baseline := v }
+ | "--adaptive" :: v :: rest, opts => parseArgs rest { opts with adaptive := v }
+ | "--output" :: v :: rest, opts => parseArgs rest { opts with output := v }
+ | "--manifest" :: v :: rest, opts => parseArgs rest { opts with manifest := v }
+ | "--case" :: v :: rest, opts => parseArgs rest { opts with cases := opts.cases.push v }
+ | "--suite" :: v :: rest, opts =>
+ if v == "all" || v == "core" then parseArgs rest { opts with all := v == "all" }
+ else .error "--suite must be core or all"
+ | "--rounds" :: v :: rest, opts => do
+ let some n := v.toNat? | throw "invalid --rounds"
+ unless 0 < n && n ≤ 10 do throw "--rounds must be 1..10"
+ parseArgs rest { opts with rounds := n }
+ | flag :: _, _ => .error s!"unknown or incomplete option {flag}"
+
+def ensure (condition : Bool) (message : String) : IO Unit :=
+ unless condition do throw (IO.userError message)
+
+def selfTest (m : Manifest) : IO Unit := do
+ need (validate m)
+ ensure (m.cases.size == 138) "inventory size"
+ let core := m.cases.filter (·.core)
+ ensure (core.size == 25) "core size"
+ for (category, count) in #[("tail", 5), ("depth", 4), ("fuel", 10), ("control", 6)] do
+ ensure ((core.filter (·.category == category)).size == count) s!"core {category}"
+ ensure ((m.cases.filter (·.category == "fuel")).size == 120) "extended fuel count"
+ let lateTail := #["fuel-6c43f78d96e1", "fuel-f38456f556fd", "fuel-f5ebaf348a49", "fuel-fa1b74facf9a",
+ "fuel-fbba56420b6b", "fuel-fdfcfa70a9e8"]
+ for id in lateTail do
+ let some c := core.find? (·.id == id) | throw (IO.userError s!"missing late tail {id}")
+ ensure (c.category == "fuel" && c.fuel == some 100000000 &&
+ c.timeout_seconds == some 300) s!"late-tail budget {id}"
+ let backoffControls := #["control-50cb089d71a0", "control-6234fd409441",
+ "control-7bf34ca3444c", "control-6303d6c017f7", "control-bfeba60bbbc6",
+ "control-eac5f4ec9db3"]
+ for id in backoffControls do
+ let some c := m.cases.find? (·.id == id) | throw (IO.userError s!"missing backoff control {id}")
+ ensure (c.category == "control" && c.fuel == some 100000000 &&
+ c.timeout_seconds == some 300) s!"backoff-control budget {id}"
+ for c in core.filter (fun c => !lateTail.contains c.id && !backoffControls.contains c.id) do
+ ensure (c.fuel.getD m.defaults.fuel ≤ 40000000) s!"original core budget {c.id}"
+ for c in #[{ m.cases[0]! with fuel := some 0 },
+ { m.cases[0]! with fuel := some 100000001 },
+ { m.cases[0]! with timeout_seconds := some 601 },
+ { m.cases[0]! with id := "../bad" }] do
+ ensure ((validate { m with cases := #[c] }).toOption.isNone) "manifest guard"
+ let a := String.ofList (List.replicate 64 'a')
+ let b := String.ofList (List.replicate 64 'b')
+ let cases : Array Case := #[
+ { id := "one", address := a, category := "depth", core := true },
+ { id := "two", address := b, category := "depth", core := true }]
+ let resolutions : Array Resolution := #[
+ { requested := a, primary := a, targets := 2 },
+ { requested := b, primary := a, targets := 2 }]
+ let groups ← need (normalize cases resolutions m.defaults)
+ ensure (groups.size == 1 && groups[0]!.caseIds.size == 2) "block alias dedup"
+ ensure ((normalize cases #[] m.defaults).toOption.isNone) "unresolved target must fail"
+ let different := cases.set! 1 { cases[1]! with fuel := some 20000000 }
+ ensure ((← need (normalize different resolutions m.defaults)).size == 2) "distinct budgets"
+ let fail := Json.mkObj [("scope", toJson "subject-only"), ("passed", toJson false),
+ ("error", toJson "recursive fuel exhausted")]
+ ensure (classify 1 fail == "fuel_exhausted") "fuel classification"
+ ensure (classify 0 fail == "harness_error") "inconsistent exit/report"
+ ensure (classify 0 .null == "harness_error") "missing report"
+ ensure (classify 124 .null == "timeout" && classify 137 .null == "killed") "resource outcomes"
+ ensure (classify 1 (fail.setObjVal! "error" (toJson "max recursion depth exceeded")) ==
+ "depth_exceeded") "depth outcome"
+ let report := Json.mkObj [("passed", toJson true), ("last_member_fuel", toJson (7 : Nat)),
+ ("check_secs", toJson (2 : Nat))]
+ let row := Json.mkObj [("outcome", toJson "pass"), ("report", report)]
+ ensure (str (compare row row) "comparison" == "same_outcome_and_work") "matching work"
+ let changed := row.setObjVal! "report" (report.setObjVal! "last_member_fuel" (toJson (8 : Nat)))
+ ensure (str (compare row changed) "comparison" == "mismatch") "fuel mismatch"
+ ensure (str (compare row changed true) "comparison" == "same_outcome_changed_work")
+ "explicit algorithmic comparison retains changed work"
+ for changed in #[row.setObjVal! "outcome" (toJson "depth_exceeded"),
+ row.setObjVal! "report" (report.setObjVal! "passed" (toJson false)),
+ row.setObjVal! "report" (report.setObjVal! "targets" (toJson (2 : Nat))),
+ row.setObjVal! "report" (report.setObjVal! "error" (toJson "new error"))] do
+ ensure (str (compare row changed true) "comparison" == "mismatch")
+ "algorithmic comparison must not permit outcome/target/error changes"
+ let timedOut := Json.mkObj [("outcome", toJson "timeout")]
+ let censored := compare timedOut row
+ ensure (str censored "comparison" == "incomplete" &&
+ field censored "adaptive_over_baseline_check_time" == .null) "no invented timeout speedup"
+ let cmd := scopeArgs "test-unit" "test-user" "/binary" #[] "/time" 120 100 96
+ for flag in #["MemoryMax=96G", "MemorySwapMax=0", "-i", "RAYON_NUM_THREADS=1",
+ "IX_MAX_REC_FUEL=100", "--kill-after=10s", "--unit=test-unit"] do
+ ensure (cmd.contains flag) s!"missing guard {flag}"
+ announce "Lean suite self-tests passed."
+
+def run (opts : Options) : IO UInt32 := do
+ let manifestJson ← need (Json.parse (← IO.FS.readFile opts.manifest))
+ let m : Manifest ← need (fromJson? manifestJson)
+ need (validate m)
+ if opts.selfTest then selfTest m; return 0
+ unless [opts.ixe, opts.baseline, opts.adaptive, opts.output].all (!·.isEmpty) do
+ throw (IO.userError "required: --ixe FILE --baseline BIN --adaptive BIN --output NEW_DIR")
+ for id in opts.cases do
+ ensure (m.cases.any (·.id == id)) s!"unknown case {id}"
+ let selected := m.cases.filter fun c =>
+ if opts.cases.isEmpty then opts.all || c.core else opts.cases.contains c.id
+ let paths ← #[opts.ixe, opts.baseline, opts.adaptive].mapM (IO.FS.realPath ∘ FilePath.mk)
+ let ixe := paths[0]!
+ let binaries := paths.extract 1 3
+ let initial ← identities paths
+ ensure ((← ixe.metadata).byteSize.toNat == m.artifact.bytes) "artifact size mismatch"
+ let out : FilePath := opts.output
+ ensure (!(← out.pathExists)) s!"refusing to overwrite directory {out}"
+ IO.FS.createDir out
+ let out ← IO.FS.realPath out
+ announce "Fingerprinting input and executables before timed checks..."
+ let hashes ← paths.mapM digest
+ ensure (hashes[0]! == m.artifact.sha256) "artifact SHA-256 mismatch"
+ ensure (hashes[1]! != hashes[2]!) "baseline/adaptive binaries are identical"
+ ensure ((← identities paths) == initial) "input changed during fingerprinting"
+ let runId := s!"{← IO.Process.getPID}-{← IO.monoMsNow}"
+ let user ← checkedOutput "id" #["-un"]
+ saveJson (out / "run.json") (Json.mkObj [
+ ("schema", toJson (1 : Nat)), ("run_id", toJson runId), ("manifest", manifestJson),
+ ("selected_case_ids", toJson (selected.map (·.id))),
+ ("paths", toJson (paths.map (·.toString))), ("sha256", toJson hashes),
+ ("file_identity", toJson initial), ("rounds", toJson opts.rounds),
+ ("allow_work_changes", toJson opts.allowWorkChanges),
+ ("host", toJson (← checkedOutput "uname" #["-a"])),
+ ("driver_sha256", toJson (← digest (suiteDir / "RunSuite.lean"))),
+ ("started_utc", toJson (← checkedOutput "date" #["-u", "+%Y-%m-%dT%H:%M:%SZ"])),
+ ("scope", toJson "subject-only; dependencies trusted"), ("workers", toJson (1 : Nat))])
+ -- Explicit prototype source snapshot; no unrelated worktree files.
+ for relative in #["crates/kernel/src/env.rs", "crates/kernel/src/env/scratch.rs",
+ "crates/kernel/src/subst.rs", "crates/kernel/src/subst/scratch_tests.rs",
+ "crates/kernel/src/infer.rs", "crates/kernel/src/infer/binders.rs",
+ "crates/kernel/src/infer/binders/tests.rs",
+ "crates/kernel/src/infer/application.rs",
+ "crates/kernel/src/infer/application/prefix.rs",
+ "crates/kernel/src/infer/application/tests.rs",
+ "crates/kernel/src/infer/summary.rs",
+ "crates/kernel/src/infer/summary/tests.rs", "crates/kernel/src/perf.rs",
+ "crates/kernel/src/perf/same_head.rs",
+ "crates/kernel/src/perf/hot_misses.rs",
+ "crates/kernel/src/def_eq.rs", "crates/kernel/src/tc.rs",
+ "crates/kernel/src/tc/spine_tests.rs", "crates/kernel/src/whnf.rs",
+ "crates/kernel/src/def_eq/projection_tests.rs",
+ "crates/kernel/src/def_eq/application.rs",
+ "crates/kernel/src/def_eq/application/tests.rs",
+ "crates/kernel/src/def_eq/same_head_tests.rs",
+ "crates/kernel/src/def_eq/speculation.rs",
+ "crates/kernel/src/def_eq/binders.rs",
+ "crates/kernel/src/def_eq/binders/tests.rs",
+ "crates/ffi/examples/check_anon_subject.rs", "Cargo.toml", "Cargo.lock",
+ "crates/kernel/Cargo.toml", "rust-toolchain.toml", "lean-toolchain",
+ "flake.nix", "flake.lock",
+ ".cargo/config.toml", "Benchmarks/Kernel/AnthropicFLT/RunSuite.lean"] do
+ let src : FilePath := relative
+ if ← src.pathExists then
+ let dst := out / "source" / relative
+ if let some parent := dst.parent then IO.FS.createDirAll parent
+ IO.FS.writeBinFile dst (← IO.FS.readBinFile src)
+ let requested := m.cases.map (·.address)
+ let mut resolutions : Array Resolution := #[]
+ for (binary, variant) in binaries.zip #["baseline", "adaptive"] do
+ let result ← limited binary (#["--resolve", ixe.toString] ++ requested) out
+ s!"resolve-{variant}" runId user 120 m.defaults.fuel m.defaults.memory_gib
+ ensure (result.exitCode == 0 && str result.report "scope" == "index-only")
+ s!"{variant} resolution failed; see its logs"
+ let rows : Array Resolution ← need (result.report.getObjValAs? _ "resolutions")
+ ensure (rows.map (·.requested) == requested) "incomplete/reordered resolution"
+ if variant == "baseline" then resolutions := rows
+ else ensure (rows == resolutions) "variants disagree on work-item resolution"
+ let groups ← need (normalize selected resolutions m.defaults)
+ saveJson (out / "resolved.json") (Json.mkObj [
+ ("all_targets", toJson resolutions), ("selected_work", toJson groups)])
+ announce s!"Resolved {requested.size} targets; running {groups.size} work items × 2 variants × {opts.rounds} rounds"
+ let results ← IO.FS.Handle.mk (out / "results.jsonl") .write
+ let mut pairs : Array Json := #[]
+ for round in [:opts.rounds] do
+ for i in [:groups.size] do
+ let g := groups[i]!
+ let order := if (round + i) % 2 == 0 then #[1, 0] else #[0, 1]
+ let mut rows := #[Json.null, Json.null]
+ for v in order do
+ ensure ((← identities paths) == initial) "input/binary changed during suite"
+ let variant := if v == 0 then "baseline" else "adaptive"
+ let name := s!"r{round + 1}-{g.caseIds[0]!}-{variant}"
+ let r ← limited binaries[v]! #[ixe.toString, g.primary] out name runId user
+ g.timeoutSeconds g.fuel m.defaults.memory_gib
+ ensure ((← identities paths) == initial) "input/binary changed during check"
+ let mut outcome := classify r.exitCode r.report
+ if str r.report "scope" == "subject-only" then
+ if str r.report "primary" != g.primary || field r.report "targets" != toJson g.targets ||
+ field r.report "fuel_cap_per_member" != toJson g.fuel then
+ outcome := "harness_error"
+ let row := Json.mkObj [
+ ("work", toJson g), ("variant", toJson variant), ("round", toJson (round + 1)),
+ ("exit_code", toJson r.exitCode), ("outcome", toJson outcome),
+ ("report", r.report), ("time", r.timing), ("wrapper_seconds", toJson r.wrapperSeconds)]
+ results.putStrLn row.compress
+ results.flush
+ rows := rows.set! v row
+ announce s!"DONE {name}: {outcome} check={(field r.report "check_secs").compress}s peak_rss={(field r.timing "peak_rss_kib").compress}KiB"
+ ensure (outcome != "harness_error") s!"harness error in {name}; stopping"
+ let pair := (compare rows[0]! rows[1]! opts.allowWorkChanges).setObjVal! "case_ids" (toJson g.caseIds)
+ |>.setObjVal! "round" (toJson (round + 1))
+ pairs := pairs.push pair
+ announce s!"PAIR {pair.compress}"
+ saveJson (out / "summary.json") (Json.mkObj [
+ ("complete", toJson true), ("pairs", toJson pairs),
+ ("warning", toJson "Completed harness is not full-corpus verification; timeouts remain unresolved.")])
+ return if pairs.any (fun p => str p "comparison" == "mismatch") then 1 else 0
+
+end Benchmarks.AnthropicFLT
+
+def main (args : List String) : IO UInt32 := do
+ try
+ let opts ← Benchmarks.AnthropicFLT.need (Benchmarks.AnthropicFLT.parseArgs args {})
+ Benchmarks.AnthropicFLT.run opts
+ catch e =>
+ IO.eprintln s!"FLT suite: {e}"
+ return 2
diff --git a/Benchmarks/Kernel/AnthropicFLT/cases.json b/Benchmarks/Kernel/AnthropicFLT/cases.json
new file mode 100644
index 000000000..59b907d6f
--- /dev/null
+++ b/Benchmarks/Kernel/AnthropicFLT/cases.json
@@ -0,0 +1,1068 @@
+{
+ "schema": 1,
+ "description": "Anonymous subject-only FLT performance regressions; dependencies are trusted, not certified.",
+ "baseline_kernel_commit": "28fc22702964058cd7cfe4eb012baf23b3af6e3a",
+ "artifact": {
+ "filename": "flt-after-source-hints-1.ixe",
+ "bytes": 30113168066,
+ "sha256": "5251edf00c0050d766702cd32d777b30889c167f4e0021b5ba89496abbb2f4d8"
+ },
+ "source": "Initial inventory: check-flt-28fc2270-40m-1.log and .failures.txt, stopped 2026-09-06 with 5 unfinished work items and 124 failed target addresses. Five existing fuel cases promoted to the core from the final tail of check-flt-fuel100m-v1-1 on 2026-09-06; that full run completed with 50 fuel failures and no depth failures. Six passing V3 controls added after full-flt-same-head-backoff-v5-1 exposed three new failures and two near-cap passes, alongside V3's highest-fuel passing control.",
+ "defaults": {
+ "fuel": 40000000,
+ "timeout_seconds": 120,
+ "memory_gib": 96,
+ "workers": 1
+ },
+ "cases": [
+ {
+ "id": "control-50cb089d71a0",
+ "address": "50cb089d71a05918fd793b026249f998556b8e16010becf5498e1501de6f092c",
+ "category": "control",
+ "core": true,
+ "fuel": 100000000,
+ "timeout_seconds": 300,
+ "observed": "V3 passed at 3748333 fuel / 8.372s; early backoff V5 exhausted 100M / 207.450s in the full sweep",
+ "observed_run": "full-flt-same-head-backoff-v5-1",
+ "observed_workers": 64
+ },
+ {
+ "id": "control-6234fd409441",
+ "address": "6234fd409441faeed33e68b7609594f9e7984907f421026fcc39eed4e2abf78f",
+ "category": "control",
+ "core": true,
+ "fuel": 100000000,
+ "timeout_seconds": 300,
+ "observed": "V3 passed at 3773953 fuel / 8.669s; early backoff V5 exhausted 100M / 221.590s in the full sweep",
+ "observed_run": "full-flt-same-head-backoff-v5-1",
+ "observed_workers": 64
+ },
+ {
+ "id": "control-7bf34ca3444c",
+ "address": "7bf34ca3444c8fc5baa18e74fea3ba57610cd79951470802f31a4e1edef4249b",
+ "category": "control",
+ "core": true,
+ "fuel": 100000000,
+ "timeout_seconds": 300,
+ "observed": "V3 passed at 2374766 fuel / 8.426s; early backoff V5 exhausted 100M / 301.760s in the full sweep",
+ "observed_run": "full-flt-same-head-backoff-v5-1",
+ "observed_workers": 64
+ },
+ {
+ "id": "control-6303d6c017f7",
+ "address": "6303d6c017f7b93869c735dcf4b49268aa2138d8e8b668e243d5034919081001",
+ "category": "control",
+ "core": true,
+ "fuel": 100000000,
+ "timeout_seconds": 300,
+ "observed": "Highest-fuel passing V3 work item: 28384918 fuel / 69.216s in the full sweep",
+ "observed_run": "full-flt-same-head-v3-1",
+ "observed_workers": 64
+ },
+ {
+ "id": "control-bfeba60bbbc6",
+ "address": "bfeba60bbbc6897cb90ecbff9143e211ee0bcde5ce67f164482d2eb78592ba22",
+ "category": "control",
+ "core": false,
+ "fuel": 100000000,
+ "timeout_seconds": 300,
+ "observed": "V3 passed at 27023380 fuel / 157.405s; early backoff V5 passed near the cap at 99998101 fuel / 198.240s",
+ "observed_run": "full-flt-same-head-backoff-v5-1",
+ "observed_workers": 64
+ },
+ {
+ "id": "control-eac5f4ec9db3",
+ "address": "eac5f4ec9db39307726e86dbdedb8c1c89d69918ce92c971ae7233f950031d44",
+ "category": "control",
+ "core": false,
+ "fuel": 100000000,
+ "timeout_seconds": 300,
+ "observed": "V3 passed at 1742241 fuel / 5.950s; early backoff V5 passed near the cap at 99999478 fuel / 158.042s",
+ "observed_run": "full-flt-same-head-backoff-v5-1",
+ "observed_workers": 64
+ },
+ {
+ "id": "tail-04e32656609b",
+ "address": "04e32656609b0e31aed0fa6707304432c5f27d3b6105267fd9389f8ea6cf0e93",
+ "category": "tail",
+ "core": true,
+ "observed": "unfinished when full run was stopped",
+ "observed_inflight_seconds": 2104
+ },
+ {
+ "id": "control-0139effa7dd4",
+ "address": "0139effa7dd49f683e998e3e5f2201878fb7c7cd4ddc7d7a76808bb7de66add4",
+ "category": "control",
+ "core": true,
+ "observed": "passed in full 40M run; 7.0s under 64-worker contention"
+ },
+ {
+ "id": "depth-0dc6387b2eda",
+ "address": "0dc6387b2eda18aaefad0eda80bc5bd7a62aa8db4c2e1226de871e839dd9b631",
+ "category": "depth",
+ "core": true,
+ "observed": "max recursion depth exceeded"
+ },
+ {
+ "id": "fuel-0072dda8396f",
+ "address": "0072dda8396f92d5cc944230c618d0168d168e66f6fece01862f455c3bfa3ea0",
+ "category": "fuel",
+ "core": true,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "tail-083005c8704e",
+ "address": "083005c8704eb6b9890471b8af71fbe24d18a8af6dc18473b7d4078a1db44ab4",
+ "category": "tail",
+ "core": true,
+ "observed": "unfinished when full run was stopped",
+ "observed_inflight_seconds": 2092
+ },
+ {
+ "id": "control-00023a804270",
+ "address": "00023a804270e12c13a5f6dca9b717950d6836803716bcd8baeafd69b72f56ec",
+ "category": "control",
+ "core": true,
+ "fuel": 20000000,
+ "observed": "passed subject-only at 20M and 40M, using 17107271 fuel"
+ },
+ {
+ "id": "depth-10e4f6ca8c39",
+ "address": "10e4f6ca8c396e268a791a3f598b25e7a9116964d328638a5dab7c600081d995",
+ "category": "depth",
+ "core": true,
+ "observed": "max recursion depth exceeded"
+ },
+ {
+ "id": "fuel-00f8aa1e8ed4",
+ "address": "00f8aa1e8ed4865d7c1a8755e4e36259d425f42edd618b89d348fe38635bb79e",
+ "category": "fuel",
+ "core": true,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "tail-0cb53e4ef3d4",
+ "address": "0cb53e4ef3d416681b5e41654ec3cac73179d3a0a75b1fcc5cdc71011cb28b85",
+ "category": "tail",
+ "core": true,
+ "observed": "unfinished when full run was stopped",
+ "observed_inflight_seconds": 2074
+ },
+ {
+ "id": "depth-088d4f086b58",
+ "address": "088d4f086b588e4aa54ac66d1d0407fbc44686a8c162749549ec97d62487d85d",
+ "category": "depth",
+ "core": true,
+ "observed": "max recursion depth exceeded"
+ },
+ {
+ "id": "fuel-07956a57e7f0",
+ "address": "07956a57e7f0386045ebdc88c4288d8b8a911657b2f34001973faf8c8868b113",
+ "category": "fuel",
+ "core": true,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "tail-b6d12915d27e",
+ "address": "b6d12915d27e8d6663ae3839afaa68eb760427d66966936b5ae9068a59f5f177",
+ "category": "tail",
+ "core": true,
+ "observed": "unfinished when full run was stopped",
+ "observed_inflight_seconds": 1217
+ },
+ {
+ "id": "depth-73c0037a49a3",
+ "address": "73c0037a49a3aa23b52e0604ebb59d96e829b600ebb334c036507ce7bbc7a5e7",
+ "category": "depth",
+ "core": true,
+ "observed": "max recursion depth exceeded"
+ },
+ {
+ "id": "fuel-03a6d7ba729b",
+ "address": "03a6d7ba729bb97c8c88eb53403bc52de6e236585ecb4276140be4830daf80d9",
+ "category": "fuel",
+ "core": true,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "tail-dfce3bf04cff",
+ "address": "dfce3bf04cffd1877f6d43b0749c845d1531ac879aef5d5157c4fd9ece8aaae0",
+ "category": "tail",
+ "core": true,
+ "observed": "unfinished when full run was stopped",
+ "observed_inflight_seconds": 987
+ },
+ {
+ "id": "control-f5e005d2f057",
+ "address": "f5e005d2f0578605572f5e516761d5b8621445062908398d1ef1db060ec83a32",
+ "category": "control",
+ "core": false,
+ "timeout_seconds": 600,
+ "observed": "passed in full 40M run after 558s; extended slow positive control"
+ },
+ {
+ "id": "fuel-07d8b8833a08",
+ "address": "07d8b8833a087877199dec944d0844b177914c1041d0ce86d82e3099a3254c40",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-0bdaebb92c97",
+ "address": "0bdaebb92c97340d9d2a21b487d7194e19ee7c7f55cf6afc0ec786bf66c1a490",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-0c37e3af2549",
+ "address": "0c37e3af25492275f5c24d3fd79807ad3b1d48abd1cad4d67fcf56cc46bd9406",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-0e85ce4d19c8",
+ "address": "0e85ce4d19c8adf95d112d4d0a9d4a8bd866125574e1d7356a79cbf30d122d5d",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-0ec7030808af",
+ "address": "0ec7030808af282501c58304828723230d91aa110ed679e7b0c06ece4b6a14c0",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-0f70ae355991",
+ "address": "0f70ae3559914dbb6808e42969ad2c663348f8601ff0abf1d2fc86458c02ec38",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-11a4ac392437",
+ "address": "11a4ac39243731c5c45772ba2871cbe58adbd30890c9398b967b2cd85fb62d8e",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-1405b7494f3b",
+ "address": "1405b7494f3b77d89fb7b3b46f6b6851958a63172afb0cae019b1b25bdd3f067",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-15026274ccb6",
+ "address": "15026274ccb6ca020522bf2627b0dc5785e5dfc513fcb78e0308e9885872587d",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-16942012be6f",
+ "address": "16942012be6f4115066ed234661a5f07b30c6d9e2860afe1d13e73818eb285bb",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-17dc3c88aedf",
+ "address": "17dc3c88aedfae687f6c7cab4a85f674f55d64f50082d58ab6def21fab8113c4",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-1c917fd2e840",
+ "address": "1c917fd2e840101dadcf6ca57bc03632abc50864351224842c2d9119758f05de",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-1e1a9a86ce35",
+ "address": "1e1a9a86ce351b16a35be7214bdb8e37889ce935f2ba6b04233daaf1be0f0e3d",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-1e21710daa90",
+ "address": "1e21710daa9064806b8edc43348aa9e6f7106709f4398b4ace8a9b8e6165625c",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-20a4bd9db684",
+ "address": "20a4bd9db684fd46437e608e30ceb2777aff674a902cb54ca1a98eee71062be8",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-243116eed67e",
+ "address": "243116eed67e812348fe49f8e1a2abfee6ca789fbd826e7c7cee72c9108a9a85",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-248d9675e38f",
+ "address": "248d9675e38fc1f2c391bb9e14f36196b2b5c1ebff2ba16440d357800fd1ee2d",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-26b361908968",
+ "address": "26b3619089682cc2dce6ec3f40b52de4263a799c27d79fa4dda8f487bfff5c9b",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-28b243bcb6be",
+ "address": "28b243bcb6be053fa0bcd90924189c586ee7c27abf65ea19b84d84dd2f9259d8",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-2d1b0b1de8a7",
+ "address": "2d1b0b1de8a7aa2b8c30ea06a26522343c458292d80d3f9b7d88877abfe8d7f0",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-37c291146040",
+ "address": "37c2911460409e226f182dd2b31d980417b8267844a19e6475cdf29892b7ddd1",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-37d7aafd083d",
+ "address": "37d7aafd083d02b5884816f3ec04d0d3be6f1655c058471495d8dc026c8354c9",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-3884666acc2b",
+ "address": "3884666acc2b49fdbe37cd74663040047a74cfa1fe18a3211f2d965cfd2b9860",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-392e414d3364",
+ "address": "392e414d336442a07fecae22c8f9c65bea3569704a50921ebd75669ec5f2ee96",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-3bb38796c801",
+ "address": "3bb38796c80106cb5dfafce7149672e141e50819f7040491981532056aa3255f",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-3d76157b6b06",
+ "address": "3d76157b6b0694ec1413d12ff7a884a1eeee4c45f39a1c2f51336d53ee2be581",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-3fe3373f9792",
+ "address": "3fe3373f97925d6c1b569f4c4baaab57630b94499d7ef67d60ef90f314f9d758",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-453f9a7935ad",
+ "address": "453f9a7935ad2940d51f011e8339c4f71137d99c4053f36010af17e26588d321",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-4658e560668d",
+ "address": "4658e560668d97ca7faa7b0478a1646cdf8f7d1dce5938535a6ba8752a5d224a",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-47a2fc199316",
+ "address": "47a2fc19931658e010269db4cba32b23e168a2d1d90cbad452a89eb17388a66a",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-4a457de5c3f1",
+ "address": "4a457de5c3f1d92ed84179931d9870b89b1d3c0b5b66f4857a842479ce669ec6",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-4abd2603d23f",
+ "address": "4abd2603d23fae7a5428a320d0b5bf62a4ba696e3eeb5319ecfc491744e8d7ee",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-4c85963c570b",
+ "address": "4c85963c570be2aa1aaf8bb9d1680d327152ad9a1b9793230d1bca25573df4f1",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-4d91369fe012",
+ "address": "4d91369fe01213d6a64bf38dc9205844d320c46bda8a422f783cd983e87d2fb0",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-52ea9de8ec4a",
+ "address": "52ea9de8ec4a256a841956b5705d4444168ce75c72375f1f7b4e032ff824031b",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-56d43a04e16e",
+ "address": "56d43a04e16e99938570317e0f989070515b45ca433fa59b81b22fb0bba7f161",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-57a8b257a0ed",
+ "address": "57a8b257a0ed572a86ceb2b943c92af6d397aa6787b68da716ac4924bc41b8dc",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-5a43f3a65af9",
+ "address": "5a43f3a65af97d7f371afdd531fcbf62ce84aa63a98010c5cf63917eb8f9e895",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-5b251facf177",
+ "address": "5b251facf177fe81ac3c27e07ecf1181c4ad827b87b60f06458ebdaca2a53a79",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-5e22bfd63817",
+ "address": "5e22bfd638178e11079e7aa119e096f14fa268380e84d34584f99c556afeebe2",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-5efa2221cc6e",
+ "address": "5efa2221cc6e94ad8220303a881f7745934f8d9d836c553bd6b56ca25a7dfd5c",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-6c43f78d96e1",
+ "address": "6c43f78d96e1efe2574d5f0527de3fef23c9f67aba636f3d790a48dff29b0ab1",
+ "category": "fuel",
+ "core": true,
+ "fuel": 100000000,
+ "timeout_seconds": 300,
+ "observed": "sole remaining recursive fuel exhaustion at 100M",
+ "observed_run": "full-flt-same-head-v3-1",
+ "observed_workers": 64,
+ "observed_check_seconds": 237.671428457,
+ "names": [
+ "P2MW.S_AutomorphicForm_exists_elliptic_family_coupled_inf_twistedCentralizer_conjAe_of_neg.HA.main"
+ ]
+ },
+ {
+ "id": "fuel-6efa80cf44b0",
+ "address": "6efa80cf44b037aa38a11589943536e38ef13582425244e364ebb45aaa517602",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-6f1c9f571133",
+ "address": "6f1c9f5711330a6225278338ffba7a63f16d17ac7103189a23097dc204589251",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-70f279c028f0",
+ "address": "70f279c028f0fc3838e3e0267a937d5b79cb4a61c619775d5a42731cc2100f22",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-717e97820f76",
+ "address": "717e97820f764d281a0b9c30b8f667e18cc372cd8cc4b42ee22e3c5c0ea0dd15",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-734d1b55e5d0",
+ "address": "734d1b55e5d01ea828c6d44c40fd0036d8fd923e7e64ed7a7524bb0b051ec9b7",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-738204d710b0",
+ "address": "738204d710b03c925845249ac22a2b669fa7185b7c8edda1c99dfa6c8b0852a7",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-77df39414404",
+ "address": "77df39414404f98008a7342510e3638a00ad8486205abb8b3183c566b8f16f37",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-7a5d012eeef0",
+ "address": "7a5d012eeef0d74fb5bf95f2463e8c1626d485572d6d849578426f539e0e2e60",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-7c9c03fb378a",
+ "address": "7c9c03fb378a53f57857293be7586763788ccf0f66c95dd3ae2c688d3711a89e",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-7d8fbfacce07",
+ "address": "7d8fbfacce07d6f465c705757ef061659cec8d21c23f9246a194582963a10e25",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-7d9bdd35ac9c",
+ "address": "7d9bdd35ac9caffa4b19487377fcdaee54f5003d60a954149b00cb9a7c3268d8",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-7fc267727e58",
+ "address": "7fc267727e58541f8e2935f7e27a5f52d405b9aed7f760440f3dbee047dd6524",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-856bccdf8bf9",
+ "address": "856bccdf8bf98f658cd238e815add6624690a1b01806097321b14f0f81855d89",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-86d58c2a911b",
+ "address": "86d58c2a911bb4aa6b034082fab6fa98392051818aeb132ec1bdfd19bcc3bb06",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-87a00bd519e8",
+ "address": "87a00bd519e84e5ea2f19836f98d810075bdbe37656c67ea69d9cf487af1d246",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-87f6482adf99",
+ "address": "87f6482adf9941d77c8da9548daa8bc48a43d1411cbf9ee7b2109089a193ecee",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-883aee507aa5",
+ "address": "883aee507aa5ea8c126534ef13bac5d17429a38392db67a71d78c248ac8bef7c",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-8c3e8f09907a",
+ "address": "8c3e8f09907a174e824b957b6f0c1fcd90882edc5e72d5b0ca765a96dda54787",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-8fd965d4f9e4",
+ "address": "8fd965d4f9e4fa39e5895b687dfdc7d7908c230950d7da82a52d739a6e2fceca",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-907a79fe0ff5",
+ "address": "907a79fe0ff545e9d723dda9451096d92b4eea775ff985e672e623a34323cd8f",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-913fac06f1a7",
+ "address": "913fac06f1a72a97dc2fe180ea166dc62051d0db9e5703be937109846d9e13b6",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-921c16fe1fde",
+ "address": "921c16fe1fde3397dd9ccdbfedcfd1626cb7dce2342db902fada4b2048a7ec0b",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-98347e9eb5a8",
+ "address": "98347e9eb5a88f1860b3ce1f72050f30fffb19c0e49b4c386cd098b9147df46f",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-98fb758e8747",
+ "address": "98fb758e874764e23e78a3ff25cc75341a67ad3ba5eaf299344b380d9c6d495a",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-99ef9a2634d2",
+ "address": "99ef9a2634d2cbf28eb48c58cae257ddb47a4b9da44cd615c52f15019c1bf9b2",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-9a23b89995c7",
+ "address": "9a23b89995c7da21c805e6faf2ae6b410cfce5aa8babc34d2a769c0fa6165898",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-a2dd4adb20e5",
+ "address": "a2dd4adb20e564d0acccda9d646a013a38cd02d4e1265188cf11fb22e41b6af8",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-a6f35da719fc",
+ "address": "a6f35da719fc4751c751dceb2484cb08e9e3af4846713d3e1e37ec3e6c5e4eec",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-acac0fa9cc2c",
+ "address": "acac0fa9cc2cd1a0fcf47bcd95426859efecd68ef84a3024443ee00a6d615230",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-b277b4a39efd",
+ "address": "b277b4a39efdb13d15a0f73a014b19bfdc6e81be49f72dab2365937aa3a60b37",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-b306d39e0a70",
+ "address": "b306d39e0a70ce7c6bfb5e1d8d7084104d343b89ab73b4d854bb436dbdf26745",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-b369a9877935",
+ "address": "b369a9877935484b475deea6f3f49ff92be4d572dd095a898355b93bacbecf8a",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-b5f3069e3f7d",
+ "address": "b5f3069e3f7db33398d175498749e56c4058a34228ae46780c28cb2e5692a45a",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-b73e6f6e6d67",
+ "address": "b73e6f6e6d6718fdd6a83997bdcebb4394674c5ef674ce8b13901d366ac3f220",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-b7cc5cd0d80d",
+ "address": "b7cc5cd0d80d4ad134759092f05307917dab7de800bd4a3dc39fed0511bb7031",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-b9a7a817fca6",
+ "address": "b9a7a817fca69204b12da527e7a432601baec892b8bcaa74a512df8b9d600fd5",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-bc2e15748fee",
+ "address": "bc2e15748fee9feb1620d6dc28bfa5697404f274301e8aca0243085fb18e090f",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-bcd0b945831a",
+ "address": "bcd0b945831ac045a5b4fa612eb073f58f8ad46d06fa3692f83617cd05f0b35b",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-be270b7de1ca",
+ "address": "be270b7de1ca444e256a5fd397f31ea5b5b1ca8f5f371204ae59bf3c128cd00d",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-be9f592e20d8",
+ "address": "be9f592e20d8fdf5ac96782d99ca2376da2f220c6fe036745e7ea27c448bc870",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-bf72b0f4b4a0",
+ "address": "bf72b0f4b4a0816dec00259582e0dff373bc17f8a22f295996ecab4c9a06d7de",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-bf8dcd15bed0",
+ "address": "bf8dcd15bed075968122aa241cc695a2a60467b06115afad08fae8ec1833cd03",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-bffa13764333",
+ "address": "bffa13764333d0982f132565b2ae6600ea18576061f68c03c1615474db38466b",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-c102cb3dfae3",
+ "address": "c102cb3dfae3cf8a444d661b9658653966a8cfd2cffc36b78b00ab32290ed807",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-c17f4952807b",
+ "address": "c17f4952807bbb9c2beca9b5e207437e5153e39a0ddc63e5627faad79f5ae8be",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-c39f0bbaa298",
+ "address": "c39f0bbaa298f541cffe9e1496e0f776a86ae91c34dc6296db906f3023fef1d7",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-c4d4d0e1afa2",
+ "address": "c4d4d0e1afa2a965dc6f1244f305a62a5284bcc73688debfd8e4edaff3c06b01",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-c4ebf48fe5f1",
+ "address": "c4ebf48fe5f1415c82b1377f75f314eb9f65ef774a29da1fe25669b9577d3fd6",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-c5b89e205dc3",
+ "address": "c5b89e205dc30526a5befae5a9fd673ef6eb7ed96a190ed45ab20f80383c4605",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-c5bd67268ffa",
+ "address": "c5bd67268ffa182281d6b66b01dc406bf503132b424ceeed62f52213d9fd95b3",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-c94b74124c02",
+ "address": "c94b74124c0237baf5f51a073b1c6c94e4911bd9a9ac9b1e67a4d058b7d5a200",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-cbb8b729f984",
+ "address": "cbb8b729f984e651985790e8e4b5a6d1969e91841f7ae02701320e818ca5975b",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-cdef51c9c404",
+ "address": "cdef51c9c404cf0c29491b78758cac611faeef2915500a5b30a7a2f133d6e075",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-ce7e4b9cb918",
+ "address": "ce7e4b9cb918acf0314bf48ab879bd8bc258b46a5a139c2f6983dab519092d15",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-d03bdbdfaa1e",
+ "address": "d03bdbdfaa1eca2764a8a02bc5bf22f4c4f7b3b2254d98597968113f0c2b6158",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-d14e5a6274aa",
+ "address": "d14e5a6274aac1ce5f670b2c8428e1eca620ade0ca32ba624ee15cb53a0b914e",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-d22080b5eac3",
+ "address": "d22080b5eac3f3bdf10e4871b20781b828317a55ee1e863ba426761cc0cb349d",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-db7259a54167",
+ "address": "db7259a54167e37b31dd4f7909a768efbb4c610849063e6674ded5ba6a315d9b",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-de82bec0e810",
+ "address": "de82bec0e81006cbb6eef366a9cd5dcd00b79d1ebd7f094654da0a149a860266",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-df49324dbaeb",
+ "address": "df49324dbaeb64f97e0fd0ced5634de9b9eb761429db3143a7c356f313299cd0",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-dfc612609ef2",
+ "address": "dfc612609ef2a6dceecc24644fd4bce9a9c77ef31ba6fff7a6cf023f3cec3214",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-e05a4fb88aa2",
+ "address": "e05a4fb88aa2c277b7b1581da3c62edcab966dbb45b6f1bed0642b66f70aa121",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-e6afc96bd8b0",
+ "address": "e6afc96bd8b0a02f61e146e57d8d10ca143932f7bd1ca1bd6672c48e390c9ef0",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-eb3ed3c3c64a",
+ "address": "eb3ed3c3c64a507f29f7c118248a4346498f6bb383c4f40f4a9497a1bc514be9",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-eb60cc653dd9",
+ "address": "eb60cc653dd9521239cd73cdcaef716ce105b23e1ecfb0e2d85ef7e0be39e2c5",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-ed39b646a289",
+ "address": "ed39b646a2898600c75bc12cfe211c7773abd8e7f981e69f7de5bed2a9979acb",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-f1d5f1580e9c",
+ "address": "f1d5f1580e9cccb6b8db85fa60e974afb149895208906a205ae473a130d72e69",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-f38456f556fd",
+ "address": "f38456f556fd08a454d52efe87123261bc2bf1e4b3e09d0fa4fe8d2df8f848bb",
+ "category": "fuel",
+ "core": true,
+ "fuel": 100000000,
+ "timeout_seconds": 300,
+ "observed": "recursive fuel exhausted at 100M; one of the final five work items",
+ "observed_run": "check-flt-fuel100m-v1-1",
+ "observed_workers": 64,
+ "observed_check_seconds": 136.3,
+ "names": [
+ "P2MW.S_ModularCurve_FullLevel_exists_mem_igusaNodes_over_of_levelAut_transport_linear_nodes_iff_of_eq_two_of_dvd.IgusaNodesE133.exists_transcendental_finiteDimensional_modularFunctionFieldC",
+ "P2MW.S_ModularCurve_FullLevel_exists_mem_igusaNodes_over_of_levelAut_transport_linear_nodes_iff_of_eq_three_of_dvd.IgusaNodesE133.exists_transcendental_finiteDimensional_modularFunctionFieldC",
+ "P2MW.S_ModularCurve_FullLevel_exists_mem_igusaNodes_over_of_levelAut_transport_linear_nodes_iff.IgusaNodesE133.exists_transcendental_finiteDimensional_modularFunctionFieldC"
+ ]
+ },
+ {
+ "id": "fuel-f59ec053d54b",
+ "address": "f59ec053d54bc8c62d12c892740dfb505a94ff9be46db030f95aaebccbd825d6",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-f5ebaf348a49",
+ "address": "f5ebaf348a49a196753e9731393d8e1d31af6ba40d0454cefd5f823e37948776",
+ "category": "fuel",
+ "core": true,
+ "fuel": 100000000,
+ "timeout_seconds": 300,
+ "observed": "recursive fuel exhausted at 100M; one of the final five work items",
+ "observed_run": "check-flt-fuel100m-v1-1",
+ "observed_workers": 64,
+ "observed_check_seconds": 139.9,
+ "names": [
+ "CerednikDrinfeld.FormalODModule.endAct_varpiEnd_endAct_varpiEnd"
+ ]
+ },
+ {
+ "id": "fuel-fa1b74facf9a",
+ "address": "fa1b74facf9a8d3381d44139e410c2c51b60c76032c1a4ac7f26e74505c0b376",
+ "category": "fuel",
+ "core": true,
+ "fuel": 100000000,
+ "timeout_seconds": 300,
+ "observed": "recursive fuel exhausted at 100M; one of the final five work items",
+ "observed_run": "check-flt-fuel100m-v1-1",
+ "observed_workers": 64,
+ "observed_check_seconds": 107.9,
+ "names": [
+ "_private.P2M.Sol.S_AutomorphicForm_isAutomorphicFnAt_pseudoEisenstein_slab.0.P2MW.S_AutomorphicForm_isAutomorphicFnAt_pseudoEisenstein_slab.AutomorphicForm.PseudoEisensteinAutomorphy.finite_and_ncard_setOf_bruhatRep_mul_le"
+ ]
+ },
+ {
+ "id": "fuel-faf080f4c6dc",
+ "address": "faf080f4c6dc7b3b3faf00b93ec6c5e3b6271984c852708b5cce1e51900f5e7f",
+ "category": "fuel",
+ "core": false,
+ "observed": "recursive fuel exhausted"
+ },
+ {
+ "id": "fuel-fbba56420b6b",
+ "address": "fbba56420b6b657e435567ce3b557fa6b20b8cd1143c55daec90c19854abde32",
+ "category": "fuel",
+ "core": true,
+ "fuel": 100000000,
+ "timeout_seconds": 300,
+ "observed": "recursive fuel exhausted at 100M; one of the final five work items",
+ "observed_run": "check-flt-fuel100m-v1-1",
+ "observed_workers": 64,
+ "observed_check_seconds": 125.6,
+ "names": [
+ "P2MW.S_CerednikDrinfeld_SpecialFormalODModule_exists_fin_two_endAct_varpiEnd_eq_verschiebung_of_isAlgClosed.P2mKcUnitRootLattice.pi_pi",
+ "P2MW.S_CerednikDrinfeld_SpecialFormalODModule_exists_fin_two_mem_invariants_forall_existsUnique_eq_sum_smul_of_isCritical.P2mKcCritFibre.pi_pi",
+ "P2MW.S_CerednikDrinfeld_SpecialFormalODModule_exists_addMonoidHom_cartierModule_injective_of_isAlgClosed.P2mKcBC52Module.pi_pi"
+ ]
+ },
+ {
+ "id": "fuel-fdfcfa70a9e8",
+ "address": "fdfcfa70a9e8645e8a03a0ab5034886bf0b328b796c88a11e3818a44d374741f",
+ "category": "fuel",
+ "core": true,
+ "fuel": 100000000,
+ "timeout_seconds": 300,
+ "observed": "recursive fuel exhausted at 100M; last work item to finish",
+ "observed_run": "check-flt-fuel100m-v1-1",
+ "observed_workers": 64,
+ "observed_check_seconds": 146.8,
+ "names": [
+ "P2MW.S_ModularCurve_exists_injective_heckeEquivariant_addMonoidHom_jZero_pic0_complex.ModularCurve.K1BC.restrictAlong_liftPlace"
+ ]
+ }
+ ]
+}
diff --git a/Cargo.lock b/Cargo.lock
index fe8e19385..c8c03e78f 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -1864,6 +1864,7 @@ dependencies = [
"quickcheck_macros",
"rayon",
"rustc-hash",
+ "smallvec",
]
[[package]]
diff --git a/Cargo.toml b/Cargo.toml
index e728cb1da..818e14d55 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -66,6 +66,7 @@ rayon = "1"
rustc-hash = "2"
serde_json = "1"
sha2 = "0.10"
+smallvec = "1.15.1"
tiny-keccak = { version = "2", features = ["keccak"] }
tracing = "0.1"
tracing-subscriber = { version = "0.3", features = ["env-filter"] }
diff --git a/crates/compile/src/compile/aux_gen/recursor.rs b/crates/compile/src/compile/aux_gen/recursor.rs
index e1b173642..0e819e216 100644
--- a/crates/compile/src/compile/aux_gen/recursor.rs
+++ b/crates/compile/src/compile/aux_gen/recursor.rs
@@ -2821,12 +2821,14 @@ mod tests {
/// cross-reference the sibling. `all = [A, B]` on both inductives.
/// No hand-written recursors — aux_gen generates them.
fn build_alpha_collapse_env() -> (LeanEnv, Name, Name) {
+ build_alpha_collapse_env_named(n("A"), n("B"))
+ }
+
+ fn build_alpha_collapse_env_named(a: Name, b: Name) -> (LeanEnv, Name, Name) {
let hyg = Name::num(
Name::str(Name::anon(), "a._@._internal._hyg".into()),
Nat::from(0u64),
);
- let a = n("A");
- let b = n("B");
let a_ctor = Name::str(a.clone(), "a".into());
let b_ctor = Name::str(b.clone(), "b".into());
let all = vec![a.clone(), b.clone()];
@@ -2906,6 +2908,8 @@ mod tests {
(env, a, b)
}
+ /// Presence-only stub for tests that call aux_gen directly. Do not schedule
+ /// these via compile_env: Sort 0 + no rules has no inductive dependencies.
fn insert_aux_stub_rec(env: &mut LeanEnv, all: &[Name], ind: &Name) -> Name {
let rec_name = Name::str(ind.clone(), "rec".into());
env.insert(
@@ -2929,6 +2933,231 @@ mod tests {
rec_name
}
+ /// The uncollapsed recursors Lean generates for the Prop A/B fixture.
+ /// Transcribed from Lean 4.33.1's `#print A.rec` / `#print B.rec`, not
+ /// generated by the compiler under test. Both have two dependent Prop
+ /// motives, two minors, and a rule recursively calling the sibling recursor.
+ fn build_alpha_collapse_env_with_recursors() -> (LeanEnv, Name, Name) {
+ build_alpha_collapse_env_with_recursors_named(n("A"), n("B"))
+ }
+
+ fn build_alpha_collapse_env_with_recursors_named(
+ a: Name,
+ b: Name,
+ ) -> (LeanEnv, Name, Name) {
+ let (mut env, a, b) = build_alpha_collapse_env_named(a, b);
+ let a_ctor = Name::str(a.clone(), "a".into());
+ let b_ctor = Name::str(b.clone(), "b".into());
+ let a_rec = Name::str(a.clone(), "rec".into());
+ let b_rec = Name::str(b.clone(), "rec".into());
+ let a_c = LeanExpr::cnst(a.clone(), vec![]);
+ let b_c = LeanExpr::cnst(b.clone(), vec![]);
+ insert_two_motive_recursors(
+ &mut env,
+ &[a.clone(), b.clone()],
+ [a_rec, b_rec],
+ [a_c, b_c],
+ [
+ (a_ctor.clone(), LeanExpr::cnst(a_ctor, vec![])),
+ (b_ctor.clone(), LeanExpr::cnst(b_ctor, vec![])),
+ ],
+ &[],
+ );
+ (env, a, b)
+ }
+
+ /// Shared binder/rule shape of the Lean-transcribed A/B and Tree/Wrap Tree
+ /// fixtures. `ctor_apps` includes specialized parameters (Wrap.mk Tree).
+ fn insert_two_motive_recursors(
+ env: &mut LeanEnv,
+ all: &[Name],
+ rec_names: [Name; 2],
+ major_types: [LeanExpr; 2],
+ ctor_apps: [(Name, LeanExpr); 2],
+ level_params: &[Name],
+ ) {
+ let [a_rec, b_rec] = rec_names;
+ let [a_c, b_c] = major_types;
+ let [(a_ctor, a_ctor_app), (b_ctor, b_ctor_app)] = ctor_apps;
+ let elim_level = level_params
+ .first()
+ .map_or_else(Level::zero, |u| Level::param(u.clone()));
+ let motive_sort = LeanExpr::sort(elim_level);
+ let rec_us: Vec<_> =
+ level_params.iter().cloned().map(Level::param).collect();
+ let bv = |i: u64| LeanExpr::bvar(Nat::from(i));
+
+ // Domains are scoped under the preceding prefix binders:
+ // {mA : A → Sort u} {mB : B → Sort u} (u = 0 for the Prop fixture)
+ // (a : ∀ x : B, mB x → mA (A.a x))
+ // (b : ∀ x : A, mA x → mB (B.b x)).
+ let prefix = [
+ (
+ n("motive_1"),
+ epi(n("t"), a_c.clone(), motive_sort.clone()),
+ BinderInfo::Implicit,
+ ),
+ (
+ n("motive_2"),
+ epi(n("t"), b_c.clone(), motive_sort),
+ BinderInfo::Implicit,
+ ),
+ (
+ n("a"),
+ epi(
+ n("x"),
+ b_c.clone(),
+ epi(
+ n("ih"),
+ LeanExpr::app(bv(1), bv(0)),
+ LeanExpr::app(bv(3), LeanExpr::app(a_ctor_app, bv(1))),
+ ),
+ ),
+ BinderInfo::Default,
+ ),
+ (
+ n("b"),
+ epi(
+ n("x"),
+ a_c.clone(),
+ epi(
+ n("ih"),
+ LeanExpr::app(bv(3), bv(0)),
+ LeanExpr::app(bv(3), LeanExpr::app(b_ctor_app, bv(1))),
+ ),
+ ),
+ BinderInfo::Default,
+ ),
+ ];
+
+ for (rec_name, ctor, major_ty, field_ty, motive_idx, minor_idx, peer) in [
+ (&a_rec, &a_ctor, &a_c, &b_c, 4, 2, &b_rec),
+ (&b_rec, &b_ctor, &b_c, &a_c, 3, 1, &a_rec),
+ ] {
+ let typ = prefix.iter().rev().fold(
+ epi(n("t"), major_ty.clone(), LeanExpr::app(bv(motive_idx), bv(0))),
+ |body, (name, domain, info)| {
+ LeanExpr::all(name.clone(), domain.clone(), body, info.clone())
+ },
+ );
+ // λ mA mB a b x, minor x (peer.rec mA mB a b x).
+ let recursive_call = (0..=4)
+ .rev()
+ .fold(LeanExpr::cnst(peer.clone(), rec_us.clone()), |f, i| {
+ LeanExpr::app(f, bv(i))
+ });
+ let rhs = LeanExpr::lam(
+ n("x"),
+ field_ty.clone(),
+ LeanExpr::app(LeanExpr::app(bv(minor_idx), bv(0)), recursive_call),
+ BinderInfo::Default,
+ );
+ let rhs = prefix.iter().rev().fold(rhs, |body, (name, domain, _)| {
+ LeanExpr::lam(name.clone(), domain.clone(), body, BinderInfo::Default)
+ });
+ env.insert(
+ rec_name.clone(),
+ ConstantInfo::RecInfo(RecursorVal {
+ cnst: ConstantVal {
+ name: rec_name.clone(),
+ level_params: level_params.to_vec(),
+ typ,
+ },
+ all: all.to_vec(),
+ num_params: Nat::from(0u64),
+ num_indices: Nat::from(0u64),
+ num_motives: Nat::from(2u64),
+ num_minors: Nat::from(2u64),
+ rules: vec![RecursorRule {
+ ctor: ctor.clone(),
+ n_fields: Nat::from(1u64),
+ rhs,
+ }],
+ k: false,
+ is_unsafe: false,
+ }),
+ );
+ }
+ }
+
+ /// Lean 4.33.1: Wrap (α : Type) | mk : α → Wrap α;
+ /// Tree | node : Wrap Tree → Tree. The nested source peers are
+ /// Tree.rec, Tree.rec_1, both universe-polymorphic with two motives/minors.
+ fn build_nested_source_recursors() -> (LeanEnv, Name) {
+ let mut env = LeanEnv::default();
+ let wrap = n("Wrap");
+ let tree = n("Tree");
+ let wrap_mk = Name::str(wrap.clone(), "mk".into());
+ let node = Name::str(tree.clone(), "node".into());
+ let tree_c = LeanExpr::cnst(tree.clone(), vec![]);
+ let wrap_c = LeanExpr::cnst(wrap.clone(), vec![]);
+ let wrap_tree = LeanExpr::app(wrap_c.clone(), tree_c.clone());
+ let type0 = LeanExpr::sort(Level::succ(Level::zero()));
+ for (name, typ, ctor, params, nested) in [
+ (&wrap, epi(n("α"), type0.clone(), type0.clone()), &wrap_mk, 1u64, 0u64),
+ (&tree, type0.clone(), &node, 0, 1),
+ ] {
+ env.insert(
+ name.clone(),
+ ConstantInfo::InductInfo(InductiveVal {
+ cnst: ConstantVal { name: name.clone(), level_params: vec![], typ },
+ num_params: Nat::from(params),
+ num_indices: Nat::from(0u64),
+ all: vec![name.clone()],
+ ctors: vec![ctor.clone()],
+ num_nested: Nat::from(nested),
+ is_rec: nested != 0,
+ is_unsafe: false,
+ is_reflexive: false,
+ }),
+ );
+ }
+ let wrap_mk_ty = LeanExpr::all(
+ n("α"),
+ type0,
+ epi(
+ n("x"),
+ LeanExpr::bvar(Nat::from(0u64)),
+ LeanExpr::app(wrap_c, LeanExpr::bvar(Nat::from(1u64))),
+ ),
+ BinderInfo::Implicit,
+ );
+ for (name, typ, induct, params) in [
+ (&wrap_mk, wrap_mk_ty, &wrap, 1u64),
+ (&node, epi(n("x"), wrap_tree.clone(), tree_c.clone()), &tree, 0),
+ ] {
+ env.insert(
+ name.clone(),
+ ConstantInfo::CtorInfo(ConstructorVal {
+ cnst: ConstantVal { name: name.clone(), level_params: vec![], typ },
+ induct: induct.clone(),
+ cidx: Nat::from(0u64),
+ num_params: Nat::from(params),
+ num_fields: Nat::from(1u64),
+ is_unsafe: false,
+ }),
+ );
+ }
+ insert_two_motive_recursors(
+ &mut env,
+ std::slice::from_ref(&tree),
+ [
+ Name::str(tree.clone(), "rec".into()),
+ Name::str(tree.clone(), "rec_1".into()),
+ ],
+ [tree_c.clone(), wrap_tree],
+ [
+ (node.clone(), LeanExpr::cnst(node, vec![])),
+ (
+ wrap_mk.clone(),
+ LeanExpr::app(LeanExpr::cnst(wrap_mk, vec![]), tree_c),
+ ),
+ ],
+ &[n("u")],
+ );
+ (env, tree)
+ }
+
fn insert_aux_stub_def(env: &mut LeanEnv, ind: &Name, suffix: &str) -> Name {
use ix_common::env::{DefinitionSafety, DefinitionVal, ReducibilityHints};
@@ -3978,55 +4207,244 @@ mod tests {
}
}
- /// 3h. Full compile pipeline for alpha-collapsed recursor aliases.
- ///
- /// Builds A/B inductives with stub recursors, runs `compile_env`, then
- /// verifies their regenerated recursors share one canonical block.
+ fn assert_source_recursors_check(
+ source: &LeanEnv,
+ head: &Name,
+ expected_peers: &[Name],
+ ) {
+ use ix_kernel::{constant::KConst, ingress::lean_ingress, tc::TypeChecker};
+
+ let mut entries: Vec<_> =
+ source.iter().map(|(name, ci)| (name.clone(), (*ci).clone())).collect();
+ entries.sort_by_key(|(name, _)| name.pretty());
+ for reverse in [false, true] {
+ if reverse {
+ entries.reverse();
+ }
+ let mut source = LeanEnv::default();
+ for (name, ci) in &entries {
+ source.insert(name.clone(), ci.clone());
+ }
+ let mut kenv = lean_ingress(&source);
+ let (block, _) =
+ kenv.consts.iter().find(|(id, _)| &id.name == head).unwrap();
+ let peers: Vec<_> = kenv.blocks[block]
+ .iter()
+ .filter(|id| matches!(kenv.consts.get(id), Some(KConst::Recr { .. })))
+ .map(|id| id.name.clone())
+ .collect();
+ assert_eq!(
+ peers, expected_peers,
+ "recursors must follow source .all, not name or insertion order",
+ );
+ let mut ids: Vec<_> = kenv.consts.keys().cloned().collect();
+ ids.sort_by_key(|id| id.name.pretty());
+ for id in ids {
+ TypeChecker::new(&mut kenv).check_const(&id).unwrap_or_else(|e| {
+ panic!("source fixture {}: {e}", id.name.pretty())
+ });
+ }
+ }
+ }
+
#[test]
- fn test_aux_gen_compile_roundtrip() {
+ fn test_lean_ingress_checks_source_recursors_in_declaration_order() {
+ for (a, b) in [(n("A"), n("B")), (n("Z"), n("A"))] {
+ let (source, _, _) =
+ build_alpha_collapse_env_with_recursors_named(a.clone(), b.clone());
+ assert_source_recursors_check(
+ &source,
+ &a,
+ &[Name::str(a.clone(), "rec".into()), Name::str(b, "rec".into())],
+ );
+ }
+ }
+
+ #[test]
+ fn test_lean_ingress_checks_nested_source_recursors() {
+ let (source, tree) = build_nested_source_recursors();
+ assert_source_recursors_check(
+ &source,
+ &tree,
+ &[
+ Name::str(tree.clone(), "rec".into()),
+ Name::str(tree.clone(), "rec_1".into()),
+ ],
+ );
+ }
+
+ #[test]
+ fn test_compiled_recursors_keep_meta_and_anon_layout() {
use crate::compile::env::compile_env;
+ use ix_kernel::{
+ env::KEnv,
+ id::KId,
+ ingress::ixon_ingress,
+ mode::{Anon, Meta},
+ tc::TypeChecker,
+ };
use std::sync::Arc;
- let (mut env, a, b) = build_alpha_collapse_env();
+ let (flat, _, _) = build_alpha_collapse_env_with_recursors();
+ let (nested, _) = build_nested_source_recursors();
+ for source in [flat, nested] {
+ let source = Arc::new(source);
+ let stt = compile_env(&source).unwrap();
+ assert!(stt.ungrounded.is_empty(), "{:?}", stt.ungrounded);
+ let (mut meta_env, _intern) = ixon_ingress::(&stt.env).unwrap();
+ let mut anon_env = KEnv::::new();
+ for (name, _) in source.iter() {
+ let addr = stt.resolve_addr(name).unwrap();
+ // Meta ingress stores canonical representatives, not every source
+ // alias. Use the actual ingressed KId for this canonical address.
+ let meta_id = meta_env
+ .consts
+ .keys()
+ .find(|id| id.addr == addr)
+ .unwrap_or_else(|| {
+ panic!("missing canonical Meta target for {}", name.pretty())
+ })
+ .clone();
+ TypeChecker::new(&mut meta_env)
+ .check_const(&meta_id)
+ .unwrap_or_else(|e| panic!("compiled Meta {}: {e}", name.pretty()));
+ TypeChecker::new_with_lazy_anon(&mut anon_env, &stt.env)
+ .check_const(&KId::new(addr, ()))
+ .unwrap_or_else(|e| panic!("compiled Anon {}: {e}", name.pretty()));
+ }
+ }
+ }
- // aux_gen only emits a regenerated `.rec` when the source env already has
- // one (gate: `lean_env.get(rec_name).is_some()`). The minimal
- // `build_alpha_collapse_env` doesn't add the auxiliary constants Lean
- // would normally generate, so insert stub `.rec` entries here. Note: the
- // stubs only have to exist for the gate; aux_gen replaces their contents
- // with the regenerated value.
- let all = vec![a.clone(), b.clone()];
- let _ = insert_aux_stub_rec(&mut env, &all, &a);
- let _ = insert_aux_stub_rec(&mut env, &all, &b);
+ #[test]
+ fn test_lean_ingress_rejects_recursors_with_swapped_names() {
+ use ix_kernel::{ingress::lean_ingress, tc::TypeChecker};
+
+ let (mut source, a, b) = build_alpha_collapse_env_with_recursors();
+ let a_rec = Name::str(a, "rec".into());
+ let b_rec = Name::str(b, "rec".into());
+ let mut left = source.get(&a_rec).unwrap().cloned();
+ let mut right = source.get(&b_rec).unwrap().cloned();
+ for (ci, name) in [(&mut left, &b_rec), (&mut right, &a_rec)] {
+ let ConstantInfo::RecInfo(rec) = ci else { unreachable!() };
+ rec.cnst.name = name.clone();
+ }
+ source.insert(a_rec.clone(), right);
+ source.insert(b_rec, left);
+ let mut kenv = lean_ingress(&source);
+ let id = kenv.consts.keys().find(|id| id.name == a_rec).unwrap().clone();
+ let error = TypeChecker::new(&mut kenv).check_const(&id).unwrap_err();
+ assert!(error.to_string().contains("canonical-order mismatch"), "{error}");
+ }
+
+ #[test]
+ fn test_lean_ingress_retains_extra_recursors_for_rejection() {
+ use ix_kernel::{constant::KConst, ingress::lean_ingress, tc::TypeChecker};
+
+ let (mut source, a, _) = build_alpha_collapse_env_with_recursors();
+ let a_rec = Name::str(a, "rec".into());
+ let extra_name = n("UnexpectedRecursor");
+ let mut extra = source.get(&a_rec).unwrap().cloned();
+ let ConstantInfo::RecInfo(rec) = &mut extra else { unreachable!() };
+ rec.cnst.name = extra_name.clone();
+ source.insert(extra_name.clone(), extra);
+ let mut kenv = lean_ingress(&source);
+ let id = kenv.consts.keys().find(|id| id.name == a_rec).unwrap().clone();
+ let KConst::Recr { block, .. } = &kenv.consts[&id] else { unreachable!() };
+ assert!(kenv.blocks[block].iter().any(|id| id.name == extra_name));
+ let error = TypeChecker::new(&mut kenv).check_const(&id).unwrap_err();
+ assert!(
+ error.to_string().contains("rec_ids/flat count mismatch"),
+ "{error}"
+ );
+ }
+
+ #[test]
+ fn test_alpha_collapse_source_recursors_have_structural_dependencies() {
+ let (env, a, b) = build_alpha_collapse_env_with_recursors();
+ for (ind, peer) in [(&a, &b), (&b, &a)] {
+ let rec_name = Name::str(ind.clone(), "rec".into());
+ let rec = env.get(&rec_name).unwrap();
+ let ConstantInfo::RecInfo(val) = &*rec else {
+ panic!("expected a source recursor");
+ };
+ assert_eq!(val.num_motives, Nat::from(2u64));
+ assert_eq!(val.num_minors, Nat::from(2u64));
+ assert_eq!(val.rules.len(), 1);
+ let refs = crate::graph::get_constant_info_references(&rec);
+ // These must be structural edges from the type/rules, not `.all`
+ // metadata: the inductive block must finish before either recursor.
+ assert!(refs.contains(&a));
+ assert!(refs.contains(&b));
+ assert!(refs.contains(&val.rules[0].ctor));
+ assert!(refs.contains(&Name::str(peer.clone(), "rec".into())));
+ }
+ }
+
+ /// 3h. Full compile pipeline for alpha-collapsed recursor aliases.
+ ///
+ /// Compile genuine uncollapsed recursors and check their canonical content,
+ /// not just alias equality (two compiled placeholders could compare equal).
+ #[test]
+ fn test_aux_gen_compile_roundtrip() {
+ use crate::compile::{CompileOptions, env::compile_env_with_options};
+ use ix_kernel::{env::KEnv, id::KId, mode::Anon, tc::TypeChecker};
+ use ixon::constant::ConstantInfo as IxonCI;
+ use std::sync::Arc;
+ let (env, a, b) = build_alpha_collapse_env_with_recursors();
let lean_env = Arc::new(env);
+ let a_rec = Name::str(a.clone(), "rec".into());
+ let b_rec = Name::str(b.clone(), "rec".into());
+ let mut canonical_addrs = Vec::new();
- // Compile.
- let stt = compile_env(&lean_env)
+ for max_workers in [1, 4] {
+ let stt = compile_env_with_options(
+ &lean_env,
+ CompileOptions { max_workers: Some(max_workers) },
+ )
.expect("compile_env should succeed for alpha-collapse inductives");
+ assert!(
+ stt.ungrounded.is_empty(),
+ "compile_env must not silently return partial results: {:?}",
+ stt.ungrounded,
+ );
- // Verify A.rec was compiled.
- let has_name = |n: &Name| stt.resolve_addr(n).is_some();
- let a_rec = Name::str(a.clone(), "rec".into());
- assert!(has_name(&a_rec), "A.rec should be compiled");
+ let a_addr = stt.resolve_addr(&a_rec).expect("A.rec should be compiled");
+ let b_addr = stt.resolve_addr(&b_rec).expect("B.rec should be compiled");
+ assert_eq!(a_addr, b_addr, "alpha-equivalent recursors must alias");
+ assert!(stt.aux_gen_extra_names.contains(&a_rec));
+ assert!(stt.aux_gen_extra_names.contains(&b_rec));
+
+ // The collapsed singleton is a standalone recursor with 1+1 binders,
+ // not the original mutual's 2+2, nor the old stub's 0+0.
+ let compiled = stt.env.get_const(&a_addr).unwrap();
+ let IxonCI::Recr(rec) = &compiled.info else {
+ panic!("expected a standalone canonical recursor");
+ };
+ assert_eq!(
+ (rec.params, rec.indices, rec.motives, rec.minors),
+ (0, 0, 1, 1)
+ );
+ assert_eq!(rec.rules.len(), 1);
+ assert_eq!(rec.rules[0].fields, 1);
+
+ // Validate the regenerated type and rule RHS as well as their shape.
+ // Check every source name's canonical target, including the inductives
+ // and constructors, so dependencies are checked rather than trusted.
+ let mut kenv = KEnv::::new();
+ let mut tc = TypeChecker::new_with_lazy_anon(&mut kenv, &stt.env);
+ for (name, _) in lean_env.iter() {
+ let addr = stt.resolve_addr(name).unwrap();
+ tc.check_const(&KId::new(addr, ())).unwrap_or_else(|e| {
+ panic!("compiled fixture {}: {e}", name.pretty())
+ });
+ }
+ canonical_addrs.push(a_addr);
+ }
- // B.rec should also be registered (as an alias to the same canonical content).
- let b_rec = Name::str(b.clone(), "rec".into());
- assert!(has_name(&b_rec), "B.rec should be compiled");
-
- // Note: .below, .brecOn, .casesOn, and .recOn are only generated if the
- // original Lean env contains them (same gate as `.rec`). This minimal
- // test env doesn't add those, so they aren't generated.
- // Full-environment tests (lake test -- rust-compile) exercise that path.
-
- // Verify A.rec and B.rec resolve to the same underlying Ixon block.
- // Both are alpha-equivalent, so their compiled block addresses should
- // be identical (they share the same RPrj/singleton block).
- let a_addr = stt.resolve_addr(&a_rec).unwrap();
- let b_addr = stt.resolve_addr(&b_rec).unwrap();
assert_eq!(
- a_addr, b_addr,
- "A.rec and B.rec should point to the same compiled block (alpha-equivalent)"
+ canonical_addrs[0], canonical_addrs[1],
+ "canonical recursor content must not depend on worker count",
);
}
diff --git a/crates/ffi/examples/check_anon_subject.rs b/crates/ffi/examples/check_anon_subject.rs
new file mode 100644
index 000000000..39e6eccc8
--- /dev/null
+++ b/crates/ffi/examples/check_anon_subject.rs
@@ -0,0 +1,308 @@
+//! Bounded-run building block for profiling ONE anonymous work item by primary
+//! address. Dependencies are lazily ingressed but trusted, exactly as in one
+//! work item of `ix check-rs --anon`. This is NOT corpus/closure verification.
+//!
+//! cargo run --release -p ix-ffi --example check_anon_subject -- FILE.ixe HEX
+//! cargo run --release -p ix-ffi --example check_anon_subject -- --resolve FILE.ixe HEX...
+//!
+//! `--resolve` only enumerates work: map target addresses (including non-primary
+//! block members) to their primary, without checking anything or loading names.
+//!
+//! Run under an external timeout/memory limit. IX_MAX_REC_FUEL and the existing
+//! kernel diagnostic variables are honored. A fresh process gives a fresh
+//! KEnv and avoids carrying worker-history caches between samples.
+//!
+//! Diagnostic-only runs: `IX_PERF_COUNTERS=1` prints cache hit rates;
+//! `IX_REDUCE_HISTO=1` prints the top 20 delta/iota addresses and totals.
+//! `IX_SAME_HEAD_PROFILE=1` reports actual same-head attempts and their fuel.
+//! `IX_HOT_MISSES=1` prints miss shapes once at completion; optional
+//! `IX_HOT_MISS_CTX=1` includes their context identities.
+//! Collection is bounded to 4,096 keys; reported counts are intervals after
+//! low-frequency entries are replaced, not exact per-key totals.
+//! Reports go to stderr after checking; stdout's subject JSON is unchanged.
+//! Leave these flags unset for paired benchmark timings.
+
+use std::{
+ collections::{HashMap, HashSet},
+ path::Path,
+ process::ExitCode,
+ sync::atomic::Ordering,
+ time::Instant,
+};
+
+use ix_common::address::Address;
+use ix_kernel::{
+ anon_work::{AnonWorkItem, build_anon_work},
+ env::KEnv,
+ id::KId,
+ mode::Anon,
+ tc::TypeChecker,
+};
+use ixon::env::Env;
+
+// Match the native ix executable, without calling its Lean FFI entrypoints.
+#[global_allocator]
+static GLOBAL: mimalloc::MiMalloc = mimalloc::MiMalloc;
+
+#[derive(Debug, PartialEq, Eq)]
+struct ResolvedSubject {
+ requested: Address,
+ primary: Address,
+ targets: usize,
+}
+
+fn resolve_subjects(
+ work: &[AnonWorkItem],
+ requested: &[Address],
+) -> Result, String> {
+ let wanted: HashSet<_> = requested.iter().cloned().collect();
+ let mut found = HashMap::new();
+ for item in work {
+ for target in item.targets() {
+ if wanted.contains(target) {
+ found.insert(target.clone(), (item.primary(), item.targets().len()));
+ }
+ }
+ }
+ requested
+ .iter()
+ .map(|addr| {
+ let (primary, targets) = found.get(addr).ok_or_else(|| {
+ format!("{} is not a kernel-checkable target address", addr.hex())
+ })?;
+ Ok(ResolvedSubject {
+ requested: addr.clone(),
+ primary: (*primary).clone(),
+ targets: *targets,
+ })
+ })
+ .collect()
+}
+
+fn run(args: &[String]) -> Result {
+ if args.first().is_some_and(|arg| arg == "--resolve") && args.len() >= 3 {
+ let requested: Vec<_> = args[2..]
+ .iter()
+ .map(|arg| {
+ Address::from_hex(arg).ok_or_else(|| format!("invalid address: {arg}"))
+ })
+ .collect::>()?;
+ let env = Env::get_anon_mmap(Path::new(&args[1]))?;
+ let work = build_anon_work(&env)?;
+ let resolved = resolve_subjects(&work, &requested)?;
+ let rows: Vec<_> = resolved
+ .iter()
+ .map(|row| {
+ serde_json::json!({
+ "requested": row.requested.hex(), "primary": row.primary.hex(),
+ "targets": row.targets,
+ })
+ })
+ .collect();
+ println!(
+ "{}",
+ serde_json::json!({
+ "scope": "index-only", "resolutions": rows,
+ })
+ );
+ return Ok(true);
+ }
+ if args.len() != 2 || args[0] == "--resolve" {
+ return Err("usage: check_anon_subject FILE.ixe PRIMARY_HEX\n check_anon_subject --resolve FILE.ixe TARGET_HEX...\nSubject-only profiling: dependencies are trusted, not checked.".to_owned());
+ }
+ let primary = Address::from_hex(&args[1])
+ .ok_or_else(|| format!("invalid primary address: {}", args[1]))?;
+ check(&args[0], &primary)
+}
+
+fn check(path: &str, primary: &Address) -> Result {
+ let start = Instant::now();
+ let env = Env::get_anon_mmap(Path::new(path))?;
+ let load_secs = start.elapsed().as_secs_f64();
+ let start = Instant::now();
+ let work = build_anon_work(&env)?;
+ let item =
+ work.iter().find(|item| item.primary() == primary).ok_or_else(|| {
+ format!("{} is not a work-item primary address", primary.hex())
+ })?;
+ let targets = item.targets().len();
+ eprintln!(
+ "[subject] primary={} targets={targets} scope=subject-only workers=1 fuel_cap_per_member={} load={load_secs:.3}s enumerate={:.3}s",
+ primary.hex(),
+ ix_kernel::tc::max_rec_fuel(),
+ start.elapsed().as_secs_f64()
+ );
+ let mut kenv = KEnv::::new();
+ let _ = ix_kernel::profile::take_op_counts();
+ ix_kernel::perf::same_head::reset();
+ let start = Instant::now();
+ let (result, last_member_fuel, peak_def_eq_depth, hot_misses) = {
+ let mut tc = TypeChecker::new_with_lazy_anon(&mut kenv, &env);
+ tc.set_debug_label(format!("#{}", primary.hex()));
+ let result = tc.check_const(&KId::new(primary.clone(), ()));
+ let fuel = tc.fuel_used();
+ let peak = tc.def_eq_peak;
+ // TypeChecker has no Drop accounting. Flush the final member explicitly,
+ // after capturing its allowance and before discarding the checker.
+ tc.finish_constant_accounting();
+ (result, fuel, peak, tc.hot_miss_summary())
+ };
+ let check_secs = start.elapsed().as_secs_f64();
+ let ops = ix_kernel::profile::take_op_counts();
+ let aggregate_fuel = ix_kernel::perf::enabled()
+ .then(|| kenv.perf.total_rec_fuel_used.load(Ordering::Relaxed));
+ let report = serde_json::json!({
+ "primary": primary.hex(), "scope": "subject-only", "targets": targets,
+ "passed": result.is_ok(), "error": result.as_ref().err().map(ToString::to_string),
+ "load_secs": load_secs, "check_secs": check_secs,
+ "fuel_cap_per_member": ix_kernel::tc::max_rec_fuel(),
+ "last_member_fuel": last_member_fuel,
+ // Null unless IX_PERF_COUNTERS is enabled; do not label the final member's
+ // budget as the total fuel of a multi-member work item.
+ "aggregate_fuel": aggregate_fuel, "last_member_def_eq_peak": peak_def_eq_depth,
+ "subst": ops.subst_nodes, "whnf": ops.whnf_calls,
+ "def_eq": ops.def_eq_calls, "intern": ops.intern_nodes,
+ "nat_arith": ops.nat_arith,
+ });
+ println!("{report}");
+ eprint!("{hot_misses}");
+ eprint!("{}", ix_kernel::perf::same_head::summary());
+ if ix_kernel::perf::enabled() {
+ // The example does not install a log backend, so KEnv's log::info!
+ // drop summary would otherwise be invisible. No checker work is rerun.
+ eprint!("{}", kenv.perf.summary());
+ }
+ if ix_kernel::perf::reduce_histo_enabled() {
+ print_reductions(
+ "delta",
+ ix_kernel::perf::DELTA_HISTO
+ .iter()
+ .map(|entry| (entry.key().clone(), *entry.value()))
+ .collect(),
+ );
+ print_reductions(
+ "iota",
+ ix_kernel::perf::IOTA_HISTO
+ .iter()
+ .map(|entry| (entry.key().clone(), *entry.value()))
+ .collect(),
+ );
+ eprintln!(
+ "[reduce-histo] nat_succ_peels={}",
+ ix_kernel::perf::NAT_SUCC_PEELS.load(Ordering::Relaxed)
+ );
+ }
+ Ok(result.is_ok())
+}
+
+const REDUCTION_REPORT_LIMIT: usize = 20;
+
+fn top_reductions(
+ mut entries: Vec<(Address, u64)>,
+) -> (u128, usize, Vec<(Address, u64)>) {
+ let total = entries.iter().map(|(_, n)| u128::from(*n)).sum();
+ let distinct = entries.len();
+ entries.sort_unstable_by(|(a, x), (b, y)| y.cmp(x).then_with(|| a.cmp(b)));
+ entries.truncate(REDUCTION_REPORT_LIMIT);
+ (total, distinct, entries)
+}
+
+fn print_reductions(label: &str, entries: Vec<(Address, u64)>) {
+ let (total, distinct, top) = top_reductions(entries);
+ eprintln!(
+ "[reduce-histo] {label}: {total} reductions across {distinct} addresses; top {}",
+ top.len()
+ );
+ for (addr, count) in top {
+ eprintln!("[reduce-histo] {label} {count} #{}", addr.hex());
+ }
+}
+
+fn main() -> ExitCode {
+ let args: Vec<_> = std::env::args().skip(1).collect();
+ // Match the CLI's dedicated worker stack, not the process main stack.
+ let worker = std::thread::Builder::new()
+ .name("ix-kernel-subject".to_owned())
+ .stack_size(256 * 1024 * 1024)
+ .spawn(move || run(&args));
+ match worker {
+ Ok(worker) => match worker.join() {
+ Ok(Ok(true)) => ExitCode::SUCCESS,
+ Ok(Ok(false)) => ExitCode::FAILURE,
+ Ok(Err(error)) => {
+ eprintln!("{error}");
+ ExitCode::from(2)
+ },
+ Err(_) => {
+ eprintln!("subject worker panicked");
+ ExitCode::from(2)
+ },
+ },
+ Err(error) => {
+ eprintln!("cannot start subject worker: {error}");
+ ExitCode::from(2)
+ },
+ }
+}
+
+#[cfg(test)]
+mod tests {
+ use super::*;
+
+ #[test]
+ fn reduction_report_bounds_rows_but_preserves_complete_totals() {
+ let entries: Vec<_> =
+ (0..25u64).map(|n| (Address::hash(&n.to_le_bytes()), n + 1)).collect();
+ let (total, distinct, top) = top_reductions(entries);
+ assert_eq!(total, 325);
+ assert_eq!(distinct, 25);
+ assert_eq!(top.len(), REDUCTION_REPORT_LIMIT);
+ assert_eq!(top.first().unwrap().1, 25);
+ assert_eq!(top.last().unwrap().1, 6);
+ }
+
+ #[test]
+ fn reduction_report_handles_ties_empty_input_and_wide_totals() {
+ assert_eq!(top_reductions(Vec::new()), (0, 0, Vec::new()));
+ let a = Address::hash(b"a");
+ let b = Address::hash(b"b");
+ let (total, distinct, top) =
+ top_reductions(vec![(b.clone(), u64::MAX), (a.clone(), u64::MAX)]);
+ assert_eq!(total, 2 * u128::from(u64::MAX));
+ assert_eq!(distinct, 2);
+ assert!(top[0].0 < top[1].0);
+ assert_eq!(top_reductions(vec![(a, u64::MAX), (b, u64::MAX)]).2, top);
+ }
+
+ #[test]
+ fn resolves_members_to_primary_preserving_request_order() {
+ let a = Address::hash(b"standalone");
+ let b = Address::hash(b"primary");
+ let c = Address::hash(b"member");
+ let work = vec![
+ AnonWorkItem::Standalone { addr: a.clone() },
+ AnonWorkItem::Block {
+ block_addr: Address::hash(b"block"),
+ primary: b.clone(),
+ targets: vec![b.clone(), c.clone()],
+ },
+ ];
+ let rows =
+ resolve_subjects(&work, &[c.clone(), a.clone(), b.clone()]).unwrap();
+ assert_eq!(
+ rows,
+ vec![
+ ResolvedSubject { requested: c, primary: b.clone(), targets: 2 },
+ ResolvedSubject { requested: a.clone(), primary: a, targets: 1 },
+ ResolvedSubject { requested: b.clone(), primary: b, targets: 2 },
+ ]
+ );
+ }
+
+ #[test]
+ fn missing_address_is_an_error_not_a_partial_success() {
+ let a = Address::hash(b"present");
+ let work = vec![AnonWorkItem::Standalone { addr: a.clone() }];
+ assert!(resolve_subjects(&work, &[a, Address::hash(b"absent")]).is_err());
+ }
+}
diff --git a/crates/ffi/examples/resolve_anon_names.rs b/crates/ffi/examples/resolve_anon_names.rs
new file mode 100644
index 000000000..1116a4105
--- /dev/null
+++ b/crates/ffi/examples/resolve_anon_names.rs
@@ -0,0 +1,37 @@
+//! Diagnostic name lookup without decoding expression metadata or checking.
+//! cargo run --release -p ix-ffi --example resolve_anon_names -- FILE.ixe PREFIX...
+
+use std::process::ExitCode;
+
+fn run() -> Result<(), String> {
+ let args: Vec<_> = std::env::args().skip(1).collect();
+ if args.len() < 2
+ || args[1..].iter().any(|p| {
+ p.len() < 8 || p.len() > 64 || !p.bytes().all(|c| c.is_ascii_hexdigit())
+ })
+ {
+ return Err(
+ "usage: resolve_anon_names FILE.ixe HEX_PREFIX... (8–64 hex digits)"
+ .into(),
+ );
+ }
+ let bytes = std::fs::read(&args[0]).map_err(|e| e.to_string())?;
+ let index = ixon::env::Env::parse_lazy_index(&bytes)?;
+ for entry in &index.named {
+ let hex = entry.addr.hex();
+ if args[1..].iter().any(|p| hex.starts_with(&p.to_ascii_lowercase())) {
+ println!("{} {} {:?}", hex, entry.name, entry.hints);
+ }
+ }
+ Ok(())
+}
+
+fn main() -> ExitCode {
+ match run() {
+ Ok(()) => ExitCode::SUCCESS,
+ Err(e) => {
+ eprintln!("{e}");
+ ExitCode::FAILURE
+ },
+ }
+}
diff --git a/crates/ffi/src/kernel.rs b/crates/ffi/src/kernel.rs
index 1786bcf52..02525767a 100644
--- a/crates/ffi/src/kernel.rs
+++ b/crates/ffi/src/kernel.rs
@@ -1409,6 +1409,14 @@ fn run_anon_checks_parallel(
eprintln!(
"[rs_kernel_check_anon] checking {work_total} work item(s) for {total} consts with {worker_count} worker(s)..."
);
+ // Opt-in native throughput experiment: reuse bucket capacity, never
+ // logical cache entries. Zero preserves the existing release policy.
+ let retain_capacity = env_usize("IX_KERNEL_CHECK_RETAIN_CAPACITY", 0);
+ if retain_capacity > 0 {
+ eprintln!(
+ "[rs_kernel_check_anon] cache reset: retaining at most {retain_capacity} entries of empty capacity per cleared table"
+ );
+ }
// Per-work-item attribution entries (addr-keyed CSV; the CLI joins
// Lean names afterwards). An entry measures checking THAT item alone —
// one constant, or one whole Muts block — NOT re-checking its
@@ -1463,7 +1471,11 @@ fn run_anon_checks_parallel(
}
let item = &work[work_idx];
if checks_since_clear >= clear_every {
- kenv.clear_releasing_memory();
+ if retain_capacity == 0 {
+ kenv.clear_releasing_memory();
+ } else {
+ kenv.clear_with_capacity_limit(retain_capacity);
+ }
checks_since_clear = 0;
}
let (primary_addr, result_idxs): (Address, Vec) = match item {
diff --git a/crates/kernel/Cargo.toml b/crates/kernel/Cargo.toml
index edaef73dd..e61c721a4 100644
--- a/crates/kernel/Cargo.toml
+++ b/crates/kernel/Cargo.toml
@@ -15,6 +15,7 @@ itertools = { workspace = true }
log = { workspace = true }
num-bigint = { workspace = true }
rustc-hash = { workspace = true }
+smallvec = { workspace = true }
[target.'cfg(not(target_arch = "riscv64"))'.dependencies]
dashmap = { workspace = true, features = ["rayon"] }
diff --git a/crates/kernel/src/check.rs b/crates/kernel/src/check.rs
index dd84baa88..e6a71854c 100644
--- a/crates/kernel/src/check.rs
+++ b/crates/kernel/src/check.rs
@@ -1519,6 +1519,34 @@ mod tests {
assert_eq!(tc.def_eq_peak, 0);
}
+ #[test]
+ fn bounded_capacity_reset_matches_release_across_success_and_failure() {
+ for capacity in [0, 16, 4_096] {
+ let mut retained = KEnv::::new();
+ let mut released = KEnv::::new();
+ // Reuse the same fixture names after both successful and failed checks.
+ // Reset must not turn either a cached success or a cached error into the
+ // next check's result, including when empty bucket storage survives.
+ for name in ["id", "wrong", "Nat", "nonexistent", "wrong", "id"] {
+ retained.clear_with_capacity_limit(capacity);
+ released.clear_releasing_memory();
+ for env in [&mut retained, &mut released] {
+ for (id, c) in test_env().iter() {
+ env.insert(id.clone(), c.clone());
+ }
+ }
+ let run = |env: &mut KEnv| {
+ let mut tc = TypeChecker::new(env);
+ let result = tc.check_const(&mk_id(name)).map_err(|e| e.to_string());
+ (result, tc.fuel_used())
+ };
+ let expected = run(&mut released);
+ assert_eq!(expected.0.is_ok(), matches!(name, "id" | "Nat"));
+ assert_eq!(run(&mut retained), expected);
+ }
+ }
+ }
+
// =========================================================================
// Theorem must land in Prop
// =========================================================================
diff --git a/crates/kernel/src/def_eq.rs b/crates/kernel/src/def_eq.rs
index 7d8f84d5f..7e04e0170 100644
--- a/crates/kernel/src/def_eq.rs
+++ b/crates/kernel/src/def_eq.rs
@@ -19,10 +19,18 @@ use super::level::{KUniv, univ_eq};
use super::mode::KernelMode;
use super::subst::{instantiate_rev, lift};
use super::tc::{
- MAX_DEF_EQ_DEPTH, MAX_WHNF_FUEL, TypeChecker, collect_app_spine,
+ MAX_DEF_EQ_DEPTH, MAX_WHNF_FUEL, TypeChecker, app_head, borrow_app_spine,
+ collect_app_spine,
};
use super::whnf::PrimFamily;
+mod application;
+mod binders;
+mod speculation;
+pub(crate) use speculation::SameHeadBackoff;
+#[cfg(test)]
+mod same_head_tests;
+
/// When set, trace every `is_def_eq` call where one side's head constant
/// starts with the prefix in `IX_DEF_EQ_TRACE` (e.g. `IX_DEF_EQ_TRACE=bmod`
/// to watch all `Int.bmod`-involving comparisons). Prints `[deq] a b`
@@ -45,6 +53,13 @@ static IX_DEF_EQ_COUNT_LOG: crate::EnvFlag =
static IX_DEF_EQ_MAX_DUMP: crate::EnvString =
crate::EnvString::new(|| crate::env_var("IX_DEF_EQ_MAX_DUMP").ok());
+/// Print at most 96 cache-missing pairs near the depth guard. Identity and
+/// mode/context fields distinguish a repeated state from a long descent.
+static IX_DEF_EQ_NEAR_GUARD: crate::EnvFlag =
+ crate::EnvFlag::new(|| crate::env_var("IX_DEF_EQ_NEAR_GUARD").is_ok());
+static NEAR_GUARD_COUNT: std::sync::atomic::AtomicUsize =
+ std::sync::atomic::AtomicUsize::new(0);
+
static IX_ETA_TRACE: crate::EnvString =
crate::EnvString::new(|| crate::env_var("IX_ETA_TRACE").ok());
@@ -54,12 +69,22 @@ static IX_PROJ_DELTA_TRACE: crate::EnvString =
static DEF_EQ_COUNT: std::sync::atomic::AtomicUsize =
std::sync::atomic::AtomicUsize::new(0);
-/// Non-Regular same-head comparisons are speculative: a failed attempt must
-/// not be allowed to consume the entire constant-check budget before ordinary
+/// Same-head comparisons are speculative for every reducibility hint: a miss
+/// must not consume the entire constant-check budget before ordinary
/// delta reduction gets its turn.
const SAME_HEAD_SPECULATION_ATTEMPT_FUEL: u64 = 4_096;
+/// Regular congruence can profitably compare larger arguments (a Mathlib
+/// regression needs about 76k fuel). Leave headroom without allowing a single
+/// speculative comparison to consume the entire 100M check allowance.
+const SAME_HEAD_REGULAR_ATTEMPT_FUEL: u64 = 131_072;
+/// Only non-Regular probes have a per-constant startup window. Regular
+/// congruence remains useful throughout a check, but each attempt is bounded.
const SAME_HEAD_SPECULATION_START_FUEL: u64 = 16_384;
+/// Try comparing the requested fields before comparing whole records, without
+/// letting an unsuccessful probe starve the ordinary conversion algorithm.
+const PROJECTION_PROBE_FUEL: u64 = 4_096;
+
/// Step journal (`IX_STEP_TRACE=1`): one `[deq] ~ ` line
/// per `is_def_eq` entry (plus `[whnf+]` lines in whnf.rs), mirroring the
/// Lean kernel's `IX_TC_STEP_TRACE` journal (`Ix.Tc` / `TcM.stepTrace`).
@@ -215,6 +240,27 @@ impl TypeChecker<'_, M> {
self.env.perf.record_def_eq_miss();
self.record_hot_def_eq_miss(a, b);
+ if *IX_DEF_EQ_NEAR_GUARD
+ && self.def_eq_depth >= MAX_DEF_EQ_DEPTH.saturating_sub(32)
+ && self.debug_label_matches_env()
+ && NEAR_GUARD_COUNT.fetch_add(1, std::sync::atomic::Ordering::Relaxed)
+ < 96
+ {
+ eprintln!(
+ "[deq near guard] depth={} local={} ctx={} cheap={} infer_only={} eager={} a={} {} b={} {}",
+ self.def_eq_depth,
+ self.depth(),
+ eq_ctx,
+ self.cheap_recursion_depth,
+ self.infer_only,
+ self.eager_reduce,
+ a.hash_key(),
+ compact_def_eq_expr(a),
+ b.hash_key(),
+ compact_def_eq_expr(b),
+ );
+ }
+
// Charge recursive fuel only after the O(1) exits above. Large proof
// terms can perform hundreds of thousands of pointer/equiv/cache hits;
// those should not consume the same budget as an actual comparison.
@@ -228,6 +274,7 @@ impl TypeChecker<'_, M> {
self.def_eq_peak = self.def_eq_depth;
}
if self.def_eq_depth > MAX_DEF_EQ_DEPTH {
+ self.dump_guard_stack("def-eq-depth");
self.def_eq_depth -= 1;
self.dump_def_eq_max("depth", a, b, None, None);
return Err(TcError::MaxRecDepth);
@@ -237,6 +284,11 @@ impl TypeChecker<'_, M> {
self.def_eq_depth -= 1;
let ok = result?;
+ // Some optional reducers treat an inner error as a miss. Do not let an
+ // exhausted speculative slice escape that way as a cached inequality.
+ if !ok && self.rec_fuel == 0 {
+ return Err(TcError::MaxRecFuel);
+ }
if trace_active {
log::info!(
"[deq] depth={} -> {} ({})",
@@ -358,18 +410,94 @@ impl TypeChecker<'_, M> {
return Ok(true);
}
+ if let Some(result) = self.def_eq_lazy_delta(a, b, &mut wa, &mut wb)? {
+ return Ok(result);
+ }
+
+ if self.def_eq_trace_depth > 0 {
+ log::info!("[deq tier4 break] depth={}", self.def_eq_depth);
+ log::info!(" wa: {wa}");
+ log::info!(" wb: {wb}");
+ }
+
+ // Tier 4b: post-delta congruence checks (lean4lean isDefEqConst/Fvar/Proj)
+ if self.try_structural_congruence(&wa, &wb)? {
+ return Ok(true);
+ }
+
+ // Tier 4c: second structural pass (lean4lean:683-686, lean4
+ // type_checker.cpp:1109-1110). This is deliberately `whnfCore`, not full
+ // `whnf`: full WHNF would delta-unfold stuck open primitives such as
+ // `Nat.ble` and can literally walk enormous Nat literals in their
+ // recursive logical models.
+ let wa_core = self.whnf_core(&wa)?;
+ let wb_core = self.whnf_core(&wb)?;
+ let wa_changed =
+ !wa_core.ptr_eq(&wa) && wa_core.hash_key() != wa.hash_key();
+ let wb_changed =
+ !wb_core.ptr_eq(&wb) && wb_core.hash_key() != wb.hash_key();
+ if wa_changed || wb_changed {
+ return self.is_def_eq(&wa_core, &wb_core);
+ }
+ let wa = wa_core;
+ let wb = wb_core;
+ if wa.ptr_eq(&wb) {
+ return Ok(true);
+ }
+ if self.quick_def_eq(&wa, &wb)? {
+ return Ok(true);
+ }
+
+ // Tier 4d: app spine comparison (lean4lean isDefEqApp, lean4 type_checker.cpp:1115)
+ if self.try_def_eq_app(&wa, &wb)? {
+ return Ok(true);
+ }
+
+ let result = self.is_def_eq_whnf(&wa, &wb);
+
+ // Tier 5 final-fail trace: when IX_DEF_EQ_TIER5_DUMP is set and the
+ // pair's head names contain the configured substring, dump the
+ // post-whnfCore wa/wb. This is where lazy-delta + Tier 4c gave up.
+ if let Ok(prefix) = crate::env_var("IX_DEF_EQ_TIER5_DUMP")
+ && let Ok(false) = result.as_ref()
+ {
+ let a_match = head_const_name(&wa).is_some_and(|n| n.contains(&prefix));
+ let b_match = head_const_name(&wb).is_some_and(|n| n.contains(&prefix));
+ if prefix.is_empty() || a_match || b_match {
+ log::info!("[deq tier5 fail] depth={}", self.def_eq_depth);
+ log::info!(" wa: {wa}");
+ log::info!(" wb: {wb}");
+ }
+ }
+
+ result
+ }
+
+ /// Keep lazy-delta temporaries out of the native frame retained while
+ /// recursively comparing irreducible applications. In unoptimized builds
+ /// those temporaries otherwise occupy many KiB at EVERY application level,
+ /// even when neither head can unfold. Reduction order/fuel are unchanged.
+ #[inline]
+ fn def_eq_lazy_delta(
+ &mut self,
+ a: &KExpr,
+ b: &KExpr,
+ wa: &mut KExpr,
+ wb: &mut KExpr,
+ ) -> Result, TcError> {
// Tier 4: iterative lazy delta (lean4lean lazyDeltaReduction)
let mut fuel = MAX_WHNF_FUEL;
loop {
if fuel == 0 {
- self.dump_def_eq_max("fuel", a, b, Some(&wa), Some(&wb));
+ self.dump_guard_stack("def-eq-lazy-delta-fuel");
+ self.dump_def_eq_max("fuel", a, b, Some(wa), Some(wb));
return Err(TcError::MaxRecDepth);
}
fuel -= 1;
// M2: Nat offset reduction at top of loop (lean4lean isDefEqOffset)
- if let Some(result) = self.try_def_eq_offset(&wa, &wb)? {
- return Ok(result);
+ if let Some(result) = self.try_def_eq_offset(wa, wb)? {
+ return Ok(Some(result));
}
// Nat primitive reduction inside lazy delta. Mirrors lean4
@@ -378,18 +506,18 @@ impl TypeChecker<'_, M> {
// primitives entirely when either side has a free variable, unless
// eagerReduce is active.
let nat_ok = (!wa.has_fvars() && !wb.has_fvars()) || self.eager_reduce;
- let fam_a = self.head_prim_family(&wa);
- let fam_b = self.head_prim_family(&wb);
+ let fam_a = self.head_prim_family(wa);
+ let fam_b = self.head_prim_family(wb);
if nat_ok {
if fam_a == PrimFamily::Nat
- && let Some(wa2) = self.try_reduce_nat(&wa)?
+ && let Some(wa2) = self.try_reduce_nat(wa)?
{
- return self.is_def_eq(&wa2, &wb);
+ return self.is_def_eq(&wa2, wb).map(Some);
}
if fam_b == PrimFamily::Nat
- && let Some(wb2) = self.try_reduce_nat(&wb)?
+ && let Some(wb2) = self.try_reduce_nat(wb)?
{
- return self.is_def_eq(&wa, &wb2);
+ return self.is_def_eq(wa, &wb2).map(Some);
}
}
@@ -399,29 +527,29 @@ impl TypeChecker<'_, M> {
// Ix-specific `try_reduce_decidable` runs after native to keep the
// reference-aligned segment tight.
if fam_a == PrimFamily::Native
- && let Some(wa2) = self.try_reduce_native(&wa)?
+ && let Some(wa2) = self.try_reduce_native(wa)?
{
- return self.is_def_eq(&wa2, &wb);
+ return self.is_def_eq(&wa2, wb).map(Some);
}
if fam_b == PrimFamily::Native
- && let Some(wb2) = self.try_reduce_native(&wb)?
+ && let Some(wb2) = self.try_reduce_native(wb)?
{
- return self.is_def_eq(&wa, &wb2);
+ return self.is_def_eq(wa, &wb2).map(Some);
}
if fam_a == PrimFamily::Decidable
- && let Some(wa2) = self.try_reduce_decidable(&wa)?
+ && let Some(wa2) = self.try_reduce_decidable(wa)?
{
- return self.is_def_eq(&wa2, &wb);
+ return self.is_def_eq(&wa2, wb).map(Some);
}
if fam_b == PrimFamily::Decidable
- && let Some(wb2) = self.try_reduce_decidable(&wb)?
+ && let Some(wb2) = self.try_reduce_decidable(wb)?
{
- return self.is_def_eq(&wa, &wb2);
+ return self.is_def_eq(wa, &wb2).map(Some);
}
- let a_head = head_const_id(&wa);
- let b_head = head_const_id(&wb);
+ let a_head = head_const_id(wa);
+ let b_head = head_const_id(wb);
let a_delta = match &a_head {
Some(h) => self.is_delta(h)?,
None => false,
@@ -438,15 +566,15 @@ impl TypeChecker<'_, M> {
// C6: Before unfolding a definition, try reducing projection apps
// on the non-definition side (lean4lean tryUnfoldProjApp).
if a_delta && !b_delta {
- if let Some(wb2) = self.try_unfold_proj_app(&wb)? {
- wb = wb2;
+ if let Some(wb2) = self.try_unfold_proj_app(wb)? {
+ *wb = wb2;
continue;
}
} else if b_delta
&& !a_delta
- && let Some(wa2) = self.try_unfold_proj_app(&wa)?
+ && let Some(wa2) = self.try_unfold_proj_app(wa)?
{
- wa = wa2;
+ *wa = wa2;
continue;
}
@@ -466,138 +594,86 @@ impl TypeChecker<'_, M> {
};
if wa_w == wb_w {
- // H2: Same-head congruence is sound for every hint. Keep Regular
- // attempts unbounded; bound non-Regular speculation so a miss cannot
- // starve the ordinary delta path. Cache only rejected attempts.
+ // H2: Same-head congruence is sound for every hint, but it is only
+ // a sufficient condition: unfolding may erase unequal arguments.
+ // Bound speculation and cache only inconclusive/rejected probes,
+ // never an inequality of the enclosing applications.
if let (Some(ah), Some(bh)) = (&a_head, &b_head)
&& ah.addr == bh.addr
{
let (lo, hi) = canonical_pair(wa.hash_key(), wb.hash_key());
- let failure_key = (lo, hi, self.def_eq_ctx_key(&wa, &wb));
+ let failure_key = (lo, hi, self.def_eq_ctx_key(wa, wb));
if !self.env.def_eq_failure.contains(&failure_key) {
- let result = if self.is_regular(ah)? {
- self.try_same_head_spine(&wa, &wb)?
- } else {
- self.try_same_head_spine_speculative(&wa, &wb)?
- };
+ let regular = self.is_regular(ah)?;
+ let result =
+ self.try_same_head_spine_speculative(wa, wb, ah, regular)?;
if let Some(result) = result {
- return Ok(result);
+ return Ok(Some(result));
}
- // Spine comparison was attempted and failed — cache it
+ // This pair did not yield a useful probe (possibly skipped or
+ // resource-limited). The cache only skips future speculation.
self.env.def_eq_failure.insert(failure_key);
self.env.perf.record_def_eq_failure_insert();
} else {
self.env.perf.record_def_eq_failure_hit();
+ crate::perf::same_head::skip(
+ wa_w.0 == 1,
+ crate::perf::same_head::Skip::FailureCache,
+ );
}
}
// H1: Equal height — unfold BOTH sides (lean4lean:596)
- let ua = self.delta_unfold_one(&wa)?;
- let ub = self.delta_unfold_one(&wb)?;
+ let ua = self.delta_unfold_one(wa)?;
+ let ub = self.delta_unfold_one(wb)?;
match (ua, ub) {
(Some(ua), Some(ub)) => {
- wa = self.whnf_no_delta_for_def_eq(&ua)?;
- wb = self.whnf_no_delta_for_def_eq(&ub)?;
+ *wa = self.whnf_no_delta_for_def_eq(&ua)?;
+ *wb = self.whnf_no_delta_for_def_eq(&ub)?;
},
(Some(ua), None) => {
- wa = self.whnf_no_delta_for_def_eq(&ua)?;
+ *wa = self.whnf_no_delta_for_def_eq(&ua)?;
},
(None, Some(ub)) => {
- wb = self.whnf_no_delta_for_def_eq(&ub)?;
+ *wb = self.whnf_no_delta_for_def_eq(&ub)?;
},
(None, None) => break,
}
} else if wa_w > wb_w {
// a is heavier — unfold a first
- if let Some(ua) = self.delta_unfold_one(&wa)? {
- wa = self.whnf_no_delta_for_def_eq(&ua)?;
+ if let Some(ua) = self.delta_unfold_one(wa)? {
+ *wa = self.whnf_no_delta_for_def_eq(&ua)?;
} else {
break;
}
} else {
// b is heavier — unfold b first
- if let Some(ub) = self.delta_unfold_one(&wb)? {
- wb = self.whnf_no_delta_for_def_eq(&ub)?;
+ if let Some(ub) = self.delta_unfold_one(wb)? {
+ *wb = self.whnf_no_delta_for_def_eq(&ub)?;
} else {
break;
}
}
} else if a_delta {
- if let Some(ua) = self.delta_unfold_one(&wa)? {
- wa = self.whnf_no_delta_for_def_eq(&ua)?;
+ if let Some(ua) = self.delta_unfold_one(wa)? {
+ *wa = self.whnf_no_delta_for_def_eq(&ua)?;
} else {
break;
}
- } else if let Some(ub) = self.delta_unfold_one(&wb)? {
- wb = self.whnf_no_delta_for_def_eq(&ub)?;
+ } else if let Some(ub) = self.delta_unfold_one(wb)? {
+ *wb = self.whnf_no_delta_for_def_eq(&ub)?;
} else {
break;
}
- if wa.ptr_eq(&wb) {
- return Ok(true);
+ if wa.ptr_eq(wb) {
+ return Ok(Some(true));
}
- if self.quick_def_eq(&wa, &wb)? {
- return Ok(true);
+ if self.quick_def_eq(wa, wb)? {
+ return Ok(Some(true));
}
}
- if self.def_eq_trace_depth > 0 {
- log::info!("[deq tier4 break] depth={}", self.def_eq_depth);
- log::info!(" wa: {wa}");
- log::info!(" wb: {wb}");
- }
-
- // Tier 4b: post-delta congruence checks (lean4lean isDefEqConst/Fvar/Proj)
- if self.try_structural_congruence(&wa, &wb)? {
- return Ok(true);
- }
-
- // Tier 4c: second structural pass (lean4lean:683-686, lean4
- // type_checker.cpp:1109-1110). This is deliberately `whnfCore`, not full
- // `whnf`: full WHNF would delta-unfold stuck open primitives such as
- // `Nat.ble` and can literally walk enormous Nat literals in their
- // recursive logical models.
- let wa_core = self.whnf_core(&wa)?;
- let wb_core = self.whnf_core(&wb)?;
- let wa_changed =
- !wa_core.ptr_eq(&wa) && wa_core.hash_key() != wa.hash_key();
- let wb_changed =
- !wb_core.ptr_eq(&wb) && wb_core.hash_key() != wb.hash_key();
- if wa_changed || wb_changed {
- return self.is_def_eq(&wa_core, &wb_core);
- }
- let wa = wa_core;
- let wb = wb_core;
- if wa.ptr_eq(&wb) {
- return Ok(true);
- }
- if self.quick_def_eq(&wa, &wb)? {
- return Ok(true);
- }
-
- // Tier 4d: app spine comparison (lean4lean isDefEqApp, lean4 type_checker.cpp:1115)
- if self.try_def_eq_app(&wa, &wb)? {
- return Ok(true);
- }
-
- let result = self.is_def_eq_whnf(&wa, &wb);
-
- // Tier 5 final-fail trace: when IX_DEF_EQ_TIER5_DUMP is set and the
- // pair's head names contain the configured substring, dump the
- // post-whnfCore wa/wb. This is where lazy-delta + Tier 4c gave up.
- if let Ok(prefix) = crate::env_var("IX_DEF_EQ_TIER5_DUMP")
- && let Ok(false) = result.as_ref()
- {
- let a_match = head_const_name(&wa).is_some_and(|n| n.contains(&prefix));
- let b_match = head_const_name(&wb).is_some_and(|n| n.contains(&prefix));
- if prefix.is_empty() || a_match || b_match {
- log::info!("[deq tier5 fail] depth={}", self.def_eq_depth);
- log::info!(" wa: {wa}");
- log::info!(" wb: {wb}");
- }
- }
-
- result
+ Ok(None)
}
/// Quick structural: same constructor, recursively same children (no WHNF).
@@ -608,42 +684,8 @@ impl TypeChecker<'_, M> {
) -> Result> {
match (a.data(), b.data()) {
(ExprData::Sort(u1, _), ExprData::Sort(u2, _)) => Ok(univ_eq(u1, u2)),
- (
- ExprData::Lam(name, bi, ty1, body1, _),
- ExprData::Lam(_, _, ty2, body2, _),
- )
- | (
- ExprData::All(name, bi, ty1, body1, _),
- ExprData::All(_, _, ty2, body2, _),
- ) => {
- if !self.is_def_eq(ty1, ty2)? {
- return Ok(false);
- }
- // Open both bodies with the SAME fresh fvar — the common-fvar
- // trick that makes alpha-renamed bodies hash-equal under
- // `instantiate_rev` and lets def-eq compare them structurally.
- // Mirrors lean4lean `isDefEqBinding`
- // (refs/lean4lean/Lean4Lean/TypeChecker.lean:546).
- self.with_lctx_scope(|tc| {
- let fv_id = tc.fresh_fvar_id();
- let fv = tc.intern(KExpr::fvar(fv_id, name.clone()));
- tc.lctx.push(
- fv_id,
- LocalDecl::CDecl {
- name: name.clone(),
- bi: bi.clone(),
- ty: ty1.clone(),
- },
- );
- let b1_open = instantiate_rev(
- &mut tc.env.intern,
- body1,
- std::slice::from_ref(&fv),
- );
- let b2_open = instantiate_rev(&mut tc.env.intern, body2, &[fv]);
- tc.is_def_eq(&b1_open, &b2_open)
- })
- },
+ (ExprData::Lam(..), ExprData::Lam(..))
+ | (ExprData::All(..), ExprData::All(..)) => self.def_eq_binders(a, b),
_ => Ok(false),
}
}
@@ -654,8 +696,8 @@ impl TypeChecker<'_, M> {
a: &KExpr,
b: &KExpr,
) -> Result, TcError> {
- let (a_head, a_args) = collect_app_spine(a);
- let (b_head, b_args) = collect_app_spine(b);
+ let (a_head, a_args) = borrow_app_spine(a);
+ let (b_head, b_args) = borrow_app_spine(b);
let (a_id, a_us) = match a_head.data() {
ExprData::Const(id, us, _) => (id, us),
_ => return Ok(None),
@@ -672,6 +714,9 @@ impl TypeChecker<'_, M> {
{
return Ok(None);
}
+ if self.try_app_congruence(a, b)? {
+ return Ok(Some(true));
+ }
for (ai, bi) in a_args.iter().zip(b_args.iter()) {
if !self.is_def_eq(ai, bi)? {
return Ok(None);
@@ -680,7 +725,54 @@ impl TypeChecker<'_, M> {
Ok(Some(true))
}
- /// Give a non-Regular same-head attempt a small local slice of recursive
+ /// Measurement wraps only a real attempt, inside any speculative fuel slice.
+ /// Nested inclusive counts overlap; the diagnostic also reports exclusive
+ /// and root fuel. The result and all accounting of actual checking work are
+ /// unchanged, including errors that a speculative caller may swallow.
+ fn try_same_head_spine_measured(
+ &mut self,
+ a: &KExpr,
+ b: &KExpr,
+ head: &KId,
+ regular: bool,
+ ) -> Result, TcError> {
+ use crate::perf::same_head::{self, Outcome};
+ if !same_head::enabled() {
+ return self.try_same_head_spine(a, b);
+ }
+ let ticket = same_head::begin(&head.addr, regular);
+ let before = self.rec_fuel;
+ let result = self.try_same_head_spine(a, b);
+ let outcome = match &result {
+ Ok(Some(true)) => Outcome::Success,
+ Ok(_) => Outcome::Miss,
+ Err(TcError::MaxRecFuel) => Outcome::FuelAbort,
+ Err(TcError::MaxRecDepth) => Outcome::DepthAbort,
+ Err(_) => Outcome::Error,
+ };
+ let consumed = before.saturating_sub(self.rec_fuel);
+ same_head::finish(ticket, consumed, outcome);
+ if let Some(sample) = same_head::take_root_trace(ticket, consumed) {
+ eprintln!(
+ "[same-head-root] sample={sample} head=#{} regular={regular} outcome={outcome:?} fuel={consumed} pair={},{} legacy_ctx={} lbr={},{} depth={} def_eq_depth={} cheap={} infer_only={} a={} b={}",
+ head.addr.hex(),
+ a.hash_key(),
+ b.hash_key(),
+ self.ctx_id,
+ a.lbr(),
+ b.lbr(),
+ self.depth(),
+ self.def_eq_depth,
+ self.cheap_recursion_depth,
+ self.infer_only,
+ compact_def_eq_expr(a),
+ compact_def_eq_expr(b)
+ );
+ }
+ result
+ }
+
+ /// Give a same-head attempt a small local slice of recursive
/// fuel. Nested attempts inherit the remaining slice; an exhausted slice is
/// a speculative miss, after which the caller follows the ordinary delta
/// path with the consumed work charged to the enclosing check.
@@ -688,17 +780,45 @@ impl TypeChecker<'_, M> {
&mut self,
a: &KExpr,
b: &KExpr,
+ head: &KId,
+ regular: bool,
) -> Result, TcError> {
let saved_fuel = self.rec_fuel;
+ // Preserve the existing non-Regular policy inside small inherited slices.
+ // A Regular slice is larger: its temporarily withheld fuel is NOT work
+ // already performed, and must not prematurely close the startup window.
let nested = saved_fuel <= SAME_HEAD_SPECULATION_ATTEMPT_FUEL;
- if !nested && self.fuel_used() >= SAME_HEAD_SPECULATION_START_FUEL {
+ let used = self.fuel_used().saturating_sub(self.same_head_fuel_reserve);
+ if !regular && !nested && used >= SAME_HEAD_SPECULATION_START_FUEL {
+ crate::perf::same_head::skip(false, crate::perf::same_head::Skip::Window);
+ return Ok(None);
+ }
+ if self.same_head_backoff.should_skip(regular) {
+ crate::perf::same_head::skip(
+ regular,
+ crate::perf::same_head::Skip::Backoff,
+ );
return Ok(None);
}
- let local_fuel = saved_fuel.min(SAME_HEAD_SPECULATION_ATTEMPT_FUEL);
+ let allowance = if regular {
+ SAME_HEAD_REGULAR_ATTEMPT_FUEL
+ } else {
+ SAME_HEAD_SPECULATION_ATTEMPT_FUEL
+ };
+ let local_fuel = saved_fuel.min(allowance);
+ let saved_reserve = self.same_head_fuel_reserve;
+ self.same_head_fuel_reserve += saved_fuel - local_fuel;
self.rec_fuel = local_fuel;
- let result = self.try_same_head_spine(a, b);
+ self.same_head_backoff.enter();
+ let result = self.try_same_head_spine_measured(a, b, head, regular);
let consumed = local_fuel.saturating_sub(self.rec_fuel);
self.rec_fuel = saved_fuel.saturating_sub(consumed);
+ self.same_head_fuel_reserve = saved_reserve;
+ let unsuccessful = matches!(
+ result,
+ Ok(None | Some(false)) | Err(TcError::MaxRecDepth | TcError::MaxRecFuel)
+ );
+ self.same_head_backoff.leave(regular, unsuccessful, consumed);
match result {
Err(TcError::MaxRecDepth | TcError::MaxRecFuel) => Ok(None),
other => other,
@@ -734,38 +854,10 @@ impl TypeChecker<'_, M> {
}
false
},
- (
- ExprData::Lam(name, bi, ty1, body1, _),
- ExprData::Lam(_, _, ty2, body2, _),
- )
- | (
- ExprData::All(name, bi, ty1, body1, _),
- ExprData::All(_, _, ty2, body2, _),
- ) => {
- if self.is_def_eq(ty1, ty2)? {
- // Open both bodies with the same fresh fvar (see `quick_def_eq`).
- let r = self.with_lctx_scope(|tc| {
- let fv_id = tc.fresh_fvar_id();
- let fv = tc.intern(KExpr::fvar(fv_id, name.clone()));
- tc.lctx.push(
- fv_id,
- LocalDecl::CDecl {
- name: name.clone(),
- bi: bi.clone(),
- ty: ty1.clone(),
- },
- );
- let b1_open = instantiate_rev(
- &mut tc.env.intern,
- body1,
- std::slice::from_ref(&fv),
- );
- let b2_open = instantiate_rev(&mut tc.env.intern, body2, &[fv]);
- tc.is_def_eq(&b1_open, &b2_open)
- })?;
- if r {
- return Ok(true);
- }
+ (ExprData::Lam(..), ExprData::Lam(..))
+ | (ExprData::All(..), ExprData::All(..)) => {
+ if self.def_eq_binders(a, b)? {
+ return Ok(true);
}
false
},
@@ -873,6 +965,9 @@ impl TypeChecker<'_, M> {
a: &KExpr,
b: &KExpr,
) -> Result> {
+ if self.known_non_proof(a) {
+ return Ok(false);
+ }
let a_ty = match self.with_infer_only(|tc| tc.infer(a)) {
Ok(ty) => ty,
Err(_) => return Ok(false),
@@ -893,9 +988,9 @@ impl TypeChecker<'_, M> {
///
/// On a hit this is one `FxHashMap` probe; on a miss it pays the
/// existing `infer ∘ whnf` chain and stores the result. Errors from
- /// the inner chain are propagated as `Ok(false)` (treating ill-typed
- /// metadata as non-prop), matching the previous behaviour of
- /// `try_proof_irrel`.
+ /// the inner chain are treated as a miss, but are NOT cached: in particular,
+ /// exhausting a speculative fuel slice must not permanently classify a
+ /// proposition as non-propositional.
pub(crate) fn is_prop_type(&mut self, ty: &KExpr) -> bool {
let cache_key = (ty.hash_key(), self.ctx_addr_for_lbr(ty.lbr()));
if let Some(&cached) = self.env.is_prop_cache.get(&cache_key) {
@@ -914,9 +1009,9 @@ impl TypeChecker<'_, M> {
ExprData::Sort(u, _) => u.is_semantic_zero(),
_ => false,
},
- Err(_) => false,
+ Err(_) => return false,
},
- Err(_) => false,
+ Err(_) => return false,
};
self.env.is_prop_cache.insert(cache_key, result);
result
@@ -937,7 +1032,7 @@ impl TypeChecker<'_, M> {
Ok(w) => w,
Err(_) => return Ok(false),
};
- let (a_head, _) = collect_app_spine(&a_ty_w);
+ let a_head = app_head(&a_ty_w);
let a_ind = match a_head.data() {
ExprData::Const(id, _, _) => id.clone(),
_ => return Ok(false),
@@ -1254,12 +1349,10 @@ impl TypeChecker<'_, M> {
t: &KExpr,
s: &KExpr,
) -> Result> {
- use super::tc::collect_app_spine;
-
let t_norm = self.whnf_no_delta(t).unwrap_or_else(|_| t.clone());
// s must be a constructor application
- let (s_head, s_args) = collect_app_spine(s);
+ let (s_head, s_args) = borrow_app_spine(s);
let ctor_id = match s_head.data() {
ExprData::Const(id, _, _) => id.clone(),
_ => {
@@ -1341,13 +1434,13 @@ impl TypeChecker<'_, M> {
for i in 0..num_fields {
let proj =
self.intern(KExpr::prj(induct_id.clone(), i as u64, t_norm.clone()));
- if !self.is_def_eq(&proj, &s_args[num_params + i])? {
+ if !self.is_def_eq(&proj, s_args[num_params + i])? {
self.dump_eta_trace(
"field-mismatch",
Some(&induct_id),
i,
&proj,
- &s_args[num_params + i],
+ s_args[num_params + i],
);
return Ok(false);
}
@@ -1362,7 +1455,7 @@ impl TypeChecker<'_, M> {
induct_id: &KId,
num_params: usize,
num_fields: usize,
- args: &[KExpr],
+ args: &[&KExpr],
) -> Result>, TcError> {
let mut base: Option> = None;
for i in 0..num_fields {
@@ -1396,14 +1489,17 @@ impl TypeChecker<'_, M> {
{
return Ok(false);
}
- let (a_head, a_args) = collect_app_spine(a);
- let (b_head, b_args) = collect_app_spine(b);
+ let (a_head, a_args) = borrow_app_spine(a);
+ let (b_head, b_args) = borrow_app_spine(b);
if a_args.len() != b_args.len() {
return Ok(false);
}
- if !self.is_def_eq(&a_head, &b_head)? {
+ if !self.is_def_eq(a_head, b_head)? {
return Ok(false);
}
+ if self.try_app_congruence(a, b)? {
+ return Ok(true);
+ }
for (ai, bi) in a_args.iter().zip(b_args.iter()) {
if !self.is_def_eq(ai, bi)? {
return Ok(false);
@@ -1491,6 +1587,9 @@ impl TypeChecker<'_, M> {
if id1.addr != id2.addr || f1 != f2 {
return Ok(false);
}
+ if self.try_projected_def_eq(a, b)? {
+ return Ok(true);
+ }
let mut v1 = v1.clone();
let mut v2 = v2.clone();
self.lazy_delta_proj_reduction(id1, *f1, &mut v1, &mut v2)
@@ -1499,6 +1598,39 @@ impl TypeChecker<'_, M> {
}
}
+ /// A positive-only shortcut: compare reduced fields before traversing the
+ /// other fields/arguments of their records. Failure (including local budget
+ /// exhaustion) leaves the ORIGINAL record-congruence path available. Never
+ /// turn an interrupted record comparison into a negative conversion result.
+ fn try_projected_def_eq(
+ &mut self,
+ a: &KExpr,
+ b: &KExpr,
+ ) -> Result> {
+ if self.in_projection_probe {
+ return Ok(false);
+ }
+ let saved_fuel = self.rec_fuel;
+ let local_fuel = saved_fuel.min(PROJECTION_PROBE_FUEL);
+ self.rec_fuel = local_fuel;
+ self.in_projection_probe = true;
+ let result = (|| {
+ let pa = self.whnf_core(a)?;
+ let pb = self.whnf_core(b)?;
+ if pa.hash_key() == a.hash_key() && pb.hash_key() == b.hash_key() {
+ return Ok(false);
+ }
+ self.is_def_eq(&pa, &pb)
+ })();
+ self.in_projection_probe = false;
+ let consumed = local_fuel.saturating_sub(self.rec_fuel);
+ self.rec_fuel = saved_fuel.saturating_sub(consumed);
+ match result {
+ Err(TcError::MaxRecDepth | TcError::MaxRecFuel) => Ok(false),
+ other => other,
+ }
+ }
+
fn lazy_delta_proj_reduction(
&mut self,
struct_id: &KId,
@@ -1509,6 +1641,7 @@ impl TypeChecker<'_, M> {
let mut fuel = MAX_WHNF_FUEL;
loop {
if fuel == 0 {
+ self.dump_guard_stack("def-eq-projection-delta-fuel");
self.dump_def_eq_max("proj-delta-fuel", a, b, None, None);
return Err(TcError::MaxRecDepth);
}
@@ -1595,11 +1728,9 @@ impl TypeChecker<'_, M> {
}
} else {
if a_id.addr == b_id.addr {
- let result = if self.is_regular(a_id)? {
- self.try_same_head_spine(a, b)?
- } else {
- self.try_same_head_spine_speculative(a, b)?
- };
+ let regular = self.is_regular(a_id)?;
+ let result =
+ self.try_same_head_spine_speculative(a, b, a_id, regular)?;
if let Some(true) = result {
return Ok(LazyDeltaStep::Equal);
}
@@ -1670,7 +1801,7 @@ impl TypeChecker<'_, M> {
&mut self,
e: &KExpr,
) -> Result>, TcError> {
- let (head, _) = collect_app_spine(e);
+ let head = app_head(e);
if !matches!(head.data(), ExprData::Prj(..)) {
return Ok(None);
}
@@ -1778,7 +1909,7 @@ fn head_const_id(e: &KExpr) -> Option> {
match e.data() {
ExprData::Const(id, _, _) => Some(id.clone()),
ExprData::App(..) => {
- let (head, _) = collect_app_spine(e);
+ let head = app_head(e);
match head.data() {
ExprData::Const(id, _, _) => Some(id.clone()),
_ => None,
@@ -1885,6 +2016,10 @@ impl TypeChecker<'_, M> {
}
}
+#[cfg(test)]
+#[path = "def_eq/projection_tests.rs"]
+mod projection_tests;
+
#[cfg(test)]
mod tests {
@@ -1924,6 +2059,21 @@ mod tests {
AE::sort(AU::succ(AU::zero()))
}
+ #[test]
+ fn declaration_summary_skips_only_non_proof_irrelevance() {
+ let mut env = env_with_same_head_hint(ReducibilityHints::Abbrev);
+ let a = AE::cnst(mk_id("same_head.c"), Box::new([]));
+ let b = AE::cnst(mk_id("same_head.d"), Box::new([]));
+ let mut tc = TypeChecker::new(&mut env);
+ assert!(!tc.try_proof_irrel(&a, &b).unwrap());
+ assert!(!tc.env.decl_summary_cache.is_empty());
+ assert!(tc.env.infer_cache.is_empty());
+ assert!(tc.env.infer_only_cache.is_empty());
+ // Other conversion rules can still infer (e.g. structure eta). The
+ // summary bypasses only this probe, and never establishes equality.
+ assert!(!tc.is_def_eq(&a, &b).unwrap());
+ }
+
fn env_with_id() -> KEnv {
let mut env = KEnv::new();
let id_ty = AE::all((), (), sort0(), sort0());
@@ -2071,6 +2221,81 @@ mod tests {
);
}
+ #[test]
+ fn same_head_profile_preserves_success_result_and_fuel() {
+ use crate::perf::same_head;
+ let run = |measured: bool| {
+ let mut env = env_with_same_head_hint(ReducibilityHints::Regular(7));
+ let a = AE::cnst(mk_id("same_head.A"), Box::new([]));
+ let c = AE::cnst(mk_id("same_head.c"), Box::new([]));
+ let id = mk_id("same_head.head");
+ let head = AE::cnst(id.clone(), Box::new([]));
+ let beta_arg = AE::app(AE::lam((), (), a, AE::var(0, ())), c.clone());
+ let left = AE::app(head.clone(), beta_arg);
+ let right = AE::app(head, c);
+ let mut tc = TypeChecker::new(&mut env);
+ same_head::reset();
+ let result = if measured {
+ tc.try_same_head_spine_measured(&left, &right, &id, true)
+ } else {
+ tc.try_same_head_spine(&left, &right)
+ }
+ .unwrap();
+ if measured && same_head::enabled() {
+ let report = same_head::summary();
+ assert!(report.contains("regular outcome=success calls=1"), "{report}");
+ assert!(
+ report.contains(&format!("root_fuel={} ", tc.fuel_used())),
+ "{report}"
+ );
+ assert!(report.contains("active=0 "), "{report}");
+ assert!(report.contains("accounting_errors=0"), "{report}");
+ }
+ (result, tc.fuel_used())
+ };
+ assert_eq!(run(false), run(true));
+ }
+
+ #[test]
+ fn same_head_profile_distinguishes_window_skip_from_fuel_abort() {
+ use crate::perf::same_head;
+ let mut env = env_with_same_head_hint(ReducibilityHints::Abbrev);
+ let a = AE::cnst(mk_id("same_head.A"), Box::new([]));
+ let c = AE::cnst(mk_id("same_head.c"), Box::new([]));
+ let id = mk_id("same_head.head");
+ let head = AE::cnst(id.clone(), Box::new([]));
+ let beta_arg = AE::app(AE::lam((), (), a, AE::var(0, ())), c.clone());
+ let left = AE::app(head.clone(), beta_arg);
+ let right = AE::app(head, c);
+ let mut tc = TypeChecker::new(&mut env);
+ tc.rec_fuel = crate::tc::max_rec_fuel()
+ .saturating_sub(super::SAME_HEAD_SPECULATION_START_FUEL);
+ let before = tc.rec_fuel;
+ same_head::reset();
+ assert_eq!(
+ tc.try_same_head_spine_speculative(&left, &right, &id, false).unwrap(),
+ None
+ );
+ assert_eq!(tc.rec_fuel, before);
+ tc.rec_fuel = 1;
+ assert_eq!(
+ tc.try_same_head_spine_speculative(&left, &right, &id, false).unwrap(),
+ None
+ );
+ assert_eq!(tc.rec_fuel, 0);
+ if same_head::enabled() {
+ let report = same_head::summary();
+ assert!(report.contains("non_regular skipped_window=1"), "{report}");
+ assert!(
+ report.contains("non_regular outcome=fuel_abort calls=1"),
+ "{report}"
+ );
+ assert!(report.contains("root_fuel=1 "), "{report}");
+ assert!(report.contains("active=0 "), "{report}");
+ assert!(report.contains("accounting_errors=0"), "{report}");
+ }
+ }
+
/// Insert a `Defn` with the given reducibility hints under `name`, returning
/// its `KId`. Used by `def_rank_id` ordering tests.
fn insert_rank_def(
diff --git a/crates/kernel/src/def_eq/application.rs b/crates/kernel/src/def_eq/application.rs
new file mode 100644
index 000000000..a0682f29a
--- /dev/null
+++ b/crates/kernel/src/def_eq/application.rs
@@ -0,0 +1,159 @@
+//! Positive-only application congruence with an explicit postorder worklist.
+//!
+//! Invariant: a Finish frame is reached ONLY after both child comparisons
+//! succeeded in the frame's original context. Thus every published equality
+//! follows from application congruence, not from a pending/visited-pair guess.
+//! See Ix/Tc/Verify/DefEq/SpineArguments.lean (TrAppSpine.defEq_of_zip) for the
+//! corresponding semantic rule. That theorem does not certify this Rust loop.
+//!
+//! No binders are opened here. All non-App pairs use ordinary conversion,
+//! with recursive worklist entry disabled. A failed child abandons the probe;
+//! it does NOT imply inequality of its applications (functions may ignore
+//! arguments). The caller retains the original conversion path on every miss.
+
+use super::*;
+use crate::env::CtxAddr;
+use crate::equiv::EqKey;
+
+const APP_CONGRUENCE_FUEL: u64 = 4_096;
+// Ordinary conversion is usually cheaper than speculative congruence. Use
+// the worklist as a near-guard fallback, not a general structural fast path:
+// a shallow trigger can spend much more work on arguments that reduction
+// would erase. Reserve stack headroom for the ordinary leaf comparisons.
+// This scheduling choice changes neither equality rules nor the depth cap.
+const APP_CONGRUENCE_MIN_DEPTH: u32 = MAX_DEF_EQ_DEPTH - 512;
+
+/// Compute these in the original context, before calling any leaf reducer.
+/// Only positive entries are published, so FULL may also consume cheap-mode
+/// successes, just as in is_def_eq. Negative results are never published here.
+struct CompletedAppKeys {
+ cache: (Addr, Addr, CtxAddr),
+ left: EqKey,
+ right: EqKey,
+ cheap: bool,
+}
+
+enum Task {
+ Compare(KExpr, KExpr),
+ Finish(CompletedAppKeys),
+}
+
+impl TypeChecker<'_, M> {
+ #[inline]
+ pub(super) fn try_app_congruence(
+ &mut self,
+ a: &KExpr,
+ b: &KExpr,
+ ) -> Result> {
+ if self.def_eq_depth < APP_CONGRUENCE_MIN_DEPTH {
+ return Ok(false);
+ }
+ self.app_congruence_probe(a, b)
+ }
+
+ #[cold]
+ #[inline(never)]
+ fn app_congruence_probe(
+ &mut self,
+ a: &KExpr,
+ b: &KExpr,
+ ) -> Result> {
+ if self.in_app_congruence
+ || !matches!((a.data(), b.data()), (ExprData::App(..), ExprData::App(..)))
+ {
+ return Ok(false);
+ }
+ // Bound failed speculation, including leaf reductions, without changing
+ // the constant's global allowance. Pending frames consume O(local_fuel)
+ // space: each expansion is ticked before pushing at most three tasks.
+ let saved_fuel = self.rec_fuel;
+ let local_fuel = saved_fuel.min(APP_CONGRUENCE_FUEL);
+ self.rec_fuel = local_fuel;
+ self.in_app_congruence = true;
+ let result = self.app_congruence_worklist(a, b);
+ self.in_app_congruence = false;
+ let consumed = local_fuel.saturating_sub(self.rec_fuel);
+ self.rec_fuel = saved_fuel.saturating_sub(consumed);
+ match result {
+ Err(TcError::MaxRecDepth | TcError::MaxRecFuel) => Ok(false),
+ other => other,
+ }
+ }
+
+ fn app_congruence_worklist(
+ &mut self,
+ a: &KExpr,
+ b: &KExpr,
+ ) -> Result> {
+ let mut work = vec![Task::Compare(a.clone(), b.clone())];
+ while let Some(task) = work.pop() {
+ let (a, b) = match task {
+ Task::Finish(keys) => {
+ // Both children completed. No pending parent can take this path
+ // after a miss/error, because those return from the entire loop.
+ self.env.def_eq_cache.insert(keys.cache, true);
+ if keys.cheap {
+ self.env.def_eq_cheap_cache.insert(keys.cache, true);
+ }
+ self.equiv_manager.add_equiv(keys.left, keys.right);
+ continue;
+ },
+ Task::Compare(a, b) => (a, b),
+ };
+ if a.ptr_eq(&b) || a.hash_key() == b.hash_key() {
+ continue;
+ }
+ let (ExprData::App(af, aa, _), ExprData::App(bf, ba, _)) =
+ (a.data(), b.data())
+ else {
+ if !self.is_def_eq(&a, &b)? {
+ return Ok(false);
+ }
+ continue;
+ };
+
+ crate::profile::bump_def_eq();
+ let lbr = a.lbr().max(b.lbr());
+ let ctx = self.def_eq_ctx_key(&a, &b);
+ let (lo, hi) = canonical_pair(a.hash_key(), b.hash_key());
+ let keys = CompletedAppKeys {
+ cache: (lo, hi, ctx),
+ left: EqKey::new(a.hash_key(), ctx, lbr, a.lbr()),
+ right: EqKey::new(b.hash_key(), ctx, lbr, b.lbr()),
+ cheap: self.cheap_recursion_depth > 0,
+ };
+ // Completed equality is enough to skip a shared DAG branch. In-flight
+ // frames are deliberately absent from both caches and the union-find.
+ if self.equiv_manager.is_equiv(&keys.left, &keys.right)
+ || self.env.def_eq_cache.get(&keys.cache) == Some(&true)
+ || (keys.cheap
+ && self.env.def_eq_cheap_cache.get(&keys.cache) == Some(&true))
+ {
+ self.env.perf.record_def_eq_hit();
+ continue;
+ }
+ // A cached inequality makes this congruence attempt unproductive.
+ // Abandon the probe, NOT its enclosing application comparison: a
+ // surrounding function can still ignore this unequal child.
+ if self.env.def_eq_cache.get(&keys.cache) == Some(&false)
+ || (keys.cheap
+ && self.env.def_eq_cheap_cache.get(&keys.cache) == Some(&false))
+ {
+ self.env.perf.record_def_eq_hit();
+ return Ok(false);
+ }
+ self.env.perf.record_def_eq_miss();
+ self.tick()?;
+ // LIFO order: function first, then argument, then completion. Each
+ // argument is checked after its function prefix, preserving dependent
+ // application order. The caller-held roots keep descendants alive.
+ work.push(Task::Finish(keys));
+ work.push(Task::Compare(aa.clone(), ba.clone()));
+ work.push(Task::Compare(af.clone(), bf.clone()));
+ }
+ Ok(true)
+ }
+}
+
+#[cfg(test)]
+mod tests;
diff --git a/crates/kernel/src/def_eq/application/tests.rs b/crates/kernel/src/def_eq/application/tests.rs
new file mode 100644
index 000000000..3f99dcddf
--- /dev/null
+++ b/crates/kernel/src/def_eq/application/tests.rs
@@ -0,0 +1,552 @@
+use super::*;
+use crate::{
+ constant::KConst,
+ env::KEnv,
+ mode::{Anon, Meta},
+};
+use ix_common::{
+ address::Address,
+ env::{BinderInfo, DefinitionSafety, Name, ReducibilityHints},
+};
+
+fn id(s: &str) -> KId {
+ KId::new(
+ Address::hash(s.as_bytes()),
+ M::meta_field(Name::str(Name::anon(), s.to_owned())),
+ )
+}
+
+fn cnst(s: &str) -> KExpr {
+ KExpr::cnst(id(s), Box::new([]))
+}
+
+fn arrow(a: KExpr, b: KExpr) -> KExpr {
+ KExpr::all(
+ M::meta_field(Name::anon()),
+ M::meta_field(BinderInfo::Default),
+ a,
+ b,
+ )
+}
+
+fn lam(body: KExpr) -> KExpr {
+ KExpr::lam(
+ M::meta_field(Name::anon()),
+ M::meta_field(BinderInfo::Default),
+ cnst("A"),
+ body,
+ )
+}
+
+fn axiom(env: &mut KEnv, name: &str, ty: KExpr) {
+ env.insert(
+ id(name),
+ KConst::Axio {
+ name: M::meta_field(Name::anon()),
+ level_params: M::meta_field(vec![]),
+ is_unsafe: false,
+ lvls: 0,
+ ty,
+ },
+ );
+}
+
+fn defn(
+ env: &mut KEnv,
+ name: &str,
+ ty: KExpr,
+ val: KExpr,
+) {
+ env.insert(
+ id(name),
+ KConst::Defn {
+ name: M::meta_field(Name::anon()),
+ level_params: M::meta_field(vec![]),
+ kind: DefKind::Definition,
+ safety: DefinitionSafety::Safe,
+ hints: ReducibilityHints::Regular(7),
+ lvls: 0,
+ ty,
+ val,
+ lean_all: M::meta_field(vec![]),
+ block: id(name),
+ },
+ );
+}
+
+fn setup() -> KEnv {
+ let mut env = KEnv::new();
+ axiom(&mut env, "A", KExpr::sort(KUniv::succ(KUniv::zero())));
+ axiom(&mut env, "a", cnst("A"));
+ axiom(&mut env, "b", cnst("A"));
+ axiom(&mut env, "F", arrow(cnst("A"), cnst("A")));
+ axiom(&mut env, "G", arrow(cnst("A"), arrow(cnst("A"), cnst("A"))));
+ defn(&mut env, "alias", cnst("A"), cnst("a"));
+ defn(
+ &mut env,
+ "id",
+ arrow(cnst("A"), cnst("A")),
+ lam(KExpr::var(0, M::meta_field(Name::anon()))),
+ );
+ defn(&mut env, "ignore", arrow(cnst("A"), cnst("A")), lam(cnst("a")));
+ env
+}
+
+fn app(
+ tc: &mut TypeChecker<'_, M>,
+ f: KExpr,
+ a: KExpr,
+) -> KExpr {
+ tc.intern(KExpr::app(f, a))
+}
+
+fn pair_key(
+ tc: &mut TypeChecker<'_, M>,
+ a: &KExpr,
+ b: &KExpr,
+) -> (Addr, Addr, CtxAddr) {
+ let (lo, hi) = canonical_pair(a.hash_key(), b.hash_key());
+ (lo, hi, tc.def_eq_ctx_key(a, b))
+}
+
+fn chain(
+ tc: &mut TypeChecker<'_, M>,
+ n: usize,
+) -> (KExpr, KExpr) {
+ let f = tc.intern(cnst("F"));
+ let mut a = tc.intern(cnst("alias"));
+ let mut b = tc.intern(cnst("a"));
+ for _ in 0..n {
+ a = app(tc, f.clone(), a);
+ b = app(tc, f.clone(), b);
+ }
+ (a, b)
+}
+
+fn deep_chain() {
+ let mut env = setup::();
+ let mut tc = TypeChecker::new(&mut env);
+ let (a, b) = chain(&mut tc, MAX_DEF_EQ_DEPTH as usize + 100);
+ assert!(tc.is_def_eq(&a, &b).unwrap());
+ assert!(
+ tc.def_eq_peak < APP_CONGRUENCE_MIN_DEPTH + 20,
+ "depth {}",
+ tc.def_eq_peak
+ );
+ assert_eq!(tc.def_eq_depth, 0);
+ assert!(!tc.in_app_congruence);
+
+ // Fresh caches and the original path: same well-typed finite chain still
+ // reaches the old guard. Large stack matches the real dedicated worker.
+ let mut old_env = setup::();
+ let mut old = TypeChecker::new(&mut old_env);
+ old.in_app_congruence = true;
+ let (a, b) = chain(&mut old, MAX_DEF_EQ_DEPTH as usize + 100);
+ assert!(matches!(old.is_def_eq(&a, &b), Err(TcError::MaxRecDepth)));
+ assert_eq!(old.def_eq_depth, 0);
+}
+
+#[test]
+fn long_application_chain_uses_worklist_not_def_eq_stack() {
+ std::thread::Builder::new()
+ .stack_size(256 * 1024 * 1024)
+ .spawn(|| {
+ deep_chain::();
+ deep_chain::();
+ })
+ .unwrap()
+ .join()
+ .unwrap();
+}
+
+fn partial_success() {
+ let mut env = setup::();
+ let mut tc = TypeChecker::new(&mut env);
+ let left_inner = app(&mut tc, cnst("F"), cnst("alias"));
+ let right_inner = app(&mut tc, cnst("F"), cnst("a"));
+ let left_fn = app(&mut tc, cnst("G"), left_inner);
+ let right_fn = app(&mut tc, cnst("G"), right_inner);
+ let a = app(&mut tc, left_fn.clone(), cnst("a"));
+ let b = app(&mut tc, right_fn.clone(), cnst("b"));
+ let root_key = pair_key(&mut tc, &a, &b);
+ let fn_key = pair_key(&mut tc, &left_fn, &right_fn);
+ assert!(!tc.app_congruence_probe(&a, &b).unwrap());
+ assert_eq!(tc.env.def_eq_cache.get(&fn_key), Some(&true));
+ assert!(!tc.env.def_eq_cache.contains_key(&root_key));
+ assert!(!tc.equiv_manager.is_equiv(
+ &EqKey::new(a.hash_key(), root_key.2, 0, 0),
+ &EqKey::new(b.hash_key(), root_key.2, 0, 0),
+ ));
+ assert!(!tc.is_def_eq(&a, &b).unwrap());
+ assert!(!tc.is_def_eq(&b, &a).unwrap());
+}
+
+#[test]
+fn failed_child_never_completes_pending_parent() {
+ partial_success::();
+ partial_success::();
+}
+
+fn non_injective() {
+ let mut env = setup::();
+ let mut tc = TypeChecker::new(&mut env);
+ tc.def_eq_depth = APP_CONGRUENCE_MIN_DEPTH;
+ let a = app(&mut tc, cnst("ignore"), cnst("a"));
+ let b = app(&mut tc, cnst("ignore"), cnst("b"));
+ let key = pair_key(&mut tc, &a, &b);
+ assert!(!tc.app_congruence_probe(&a, &b).unwrap());
+ assert!(!tc.env.def_eq_cache.contains_key(&key));
+ assert!(tc.is_def_eq(&a, &b).unwrap());
+}
+
+#[test]
+fn unequal_arguments_of_ignoring_function_fall_back_to_reduction() {
+ non_injective::();
+ non_injective::();
+}
+
+fn diamond() {
+ let mut env = setup::();
+ let mut tc = TypeChecker::new(&mut env);
+ let g = tc.intern(cnst("G"));
+ let (mut a, mut b) = (tc.intern(cnst("alias")), tc.intern(cnst("a")));
+ for _ in 0..64 {
+ let af = app(&mut tc, g.clone(), a.clone());
+ let bf = app(&mut tc, g.clone(), b.clone());
+ a = app(&mut tc, af, a);
+ b = app(&mut tc, bf, b);
+ }
+ tc.rec_fuel = 1_000;
+ assert!(tc.app_congruence_probe(&a, &b).unwrap());
+ assert!(tc.rec_fuel > 700, "completed DAG branches must not be revisited");
+}
+
+#[test]
+fn shared_diamond_uses_only_completed_equalities() {
+ diamond::();
+ diamond::();
+}
+
+fn budgets() {
+ let mut env = setup::();
+ let mut tc = TypeChecker::new(&mut env);
+ let (a, b) = chain(&mut tc, 4);
+ let key = pair_key(&mut tc, &a, &b);
+ tc.rec_fuel = 1;
+ assert!(!tc.app_congruence_probe(&a, &b).unwrap());
+ assert_eq!(tc.rec_fuel, 0);
+ assert!(!tc.in_app_congruence);
+ assert!(!tc.env.def_eq_cache.contains_key(&key));
+ assert_eq!(tc.def_eq_depth, 0);
+
+ tc.rec_fuel = 10_000;
+ tc.def_eq_depth = MAX_DEF_EQ_DEPTH;
+ assert!(!tc.app_congruence_probe(&a, &b).unwrap());
+ assert_eq!(tc.def_eq_depth, MAX_DEF_EQ_DEPTH);
+ assert!(tc.rec_fuel < 10_000);
+ assert!(!tc.in_app_congruence);
+ assert!(!tc.env.def_eq_cache.contains_key(&key));
+ tc.def_eq_depth = 0;
+ assert!(tc.is_def_eq(&a, &b).unwrap());
+
+ let (a, b) =
+ chain(&mut tc, usize::try_from(APP_CONGRUENCE_FUEL).unwrap() + 100);
+ let key = pair_key(&mut tc, &a, &b);
+ tc.rec_fuel = 20_000;
+ assert!(!tc.app_congruence_probe(&a, &b).unwrap());
+ assert_eq!(tc.rec_fuel, 20_000 - APP_CONGRUENCE_FUEL);
+ assert!(!tc.in_app_congruence);
+ assert!(!tc.env.def_eq_cache.contains_key(&key));
+}
+
+#[test]
+fn budget_and_depth_misses_restore_state_without_refunds() {
+ std::thread::Builder::new()
+ .stack_size(256 * 1024 * 1024)
+ .spawn(|| {
+ budgets::();
+ budgets::();
+ })
+ .unwrap()
+ .join()
+ .unwrap();
+}
+
+fn malformed() {
+ let mut env = setup::();
+ defn(
+ &mut env,
+ "bad",
+ cnst("A"),
+ KExpr::sort(KUniv::param(1, M::meta_field(Name::anon()))),
+ );
+ let mut tc = TypeChecker::new(&mut env);
+ let a =
+ app(&mut tc, cnst("F"), KExpr::cnst(id("bad"), Box::new([KUniv::zero()])));
+ let b = app(&mut tc, cnst("F"), cnst("a"));
+ let key = pair_key(&mut tc, &a, &b);
+ let fuel = tc.rec_fuel;
+ assert!(matches!(
+ tc.app_congruence_probe(&a, &b),
+ Err(TcError::UnivParamOutOfRange { .. })
+ ));
+ assert!(!tc.in_app_congruence);
+ assert_eq!(tc.def_eq_depth, 0);
+ assert!(tc.rec_fuel < fuel);
+ assert!(!tc.env.def_eq_cache.contains_key(&key));
+}
+
+#[test]
+fn non_budget_leaf_error_propagates_without_parent_cache_entry() {
+ malformed::();
+ malformed::();
+}
+
+fn contexts() {
+ let mut env = setup::();
+ let mut tc = TypeChecker::new(&mut env);
+ let a = app(&mut tc, cnst("F"), KExpr::var(0, M::meta_field(Name::anon())));
+ let b = app(&mut tc, cnst("F"), cnst("a"));
+ tc.push_let(cnst("A"), cnst("a"));
+ let first = pair_key(&mut tc, &a, &b);
+ assert!(tc.app_congruence_probe(&a, &b).unwrap());
+ assert_eq!(tc.depth(), 1);
+ tc.pop_local();
+ tc.push_let(cnst("A"), cnst("b"));
+ let second = pair_key(&mut tc, &a, &b);
+ assert_ne!(first, second);
+ assert!(!tc.app_congruence_probe(&a, &b).unwrap());
+ assert!(!tc.env.def_eq_cache.contains_key(&second));
+ assert!(!tc.is_def_eq(&a, &b).unwrap());
+ assert_eq!(tc.depth(), 1);
+}
+
+#[test]
+fn completed_open_pair_is_not_reused_in_another_context() {
+ contexts::();
+ contexts::();
+}
+
+fn modes() {
+ let mut env = setup::();
+ let mut tc = TypeChecker::new(&mut env);
+ let (a, b) = chain(&mut tc, 4);
+ let key = pair_key(&mut tc, &a, &b);
+ // A failed cheap attempt is not a full-mode inequality certificate.
+ tc.env.def_eq_cheap_cache.insert(key, false);
+ assert!(tc.app_congruence_probe(&a, &b).unwrap());
+ assert_eq!(tc.env.def_eq_cache.get(&key), Some(&true));
+ tc.env.clear_reduction_caches();
+ tc.equiv_manager.clear();
+ tc.cheap_recursion_depth = 1;
+ tc.infer_only = true;
+ tc.eager_reduce = true;
+ assert!(tc.app_congruence_probe(&a, &b).unwrap());
+ assert_eq!(tc.env.def_eq_cheap_cache.get(&key), Some(&true));
+ assert_eq!(tc.env.def_eq_cache.get(&key), Some(&true));
+ assert_eq!(tc.cheap_recursion_depth, 1);
+ assert!(tc.infer_only && tc.eager_reduce);
+ assert_eq!(tc.depth(), 0);
+}
+
+#[test]
+fn mode_boundaries_and_positive_cache_promotion_are_preserved() {
+ modes::();
+ modes::();
+}
+
+fn dependent() {
+ let mut env = setup::();
+ axiom(
+ &mut env,
+ "B",
+ arrow(cnst("A"), KExpr::sort(KUniv::succ(KUniv::zero()))),
+ );
+ let b_a = KExpr::app(cnst("B"), cnst("a"));
+ axiom(&mut env, "v", b_a);
+ let b_alias = KExpr::app(cnst("B"), cnst("alias"));
+ defn(&mut env, "vAlias", b_alias, cnst("v"));
+ axiom(
+ &mut env,
+ "dep",
+ arrow(
+ cnst("A"),
+ arrow(
+ KExpr::app(cnst("B"), KExpr::var(0, M::meta_field(Name::anon()))),
+ cnst("A"),
+ ),
+ ),
+ );
+ let mut tc = TypeChecker::new(&mut env);
+ let af = app(&mut tc, cnst("dep"), cnst("alias"));
+ let bf = app(&mut tc, cnst("dep"), cnst("a"));
+ let a = app(&mut tc, af, cnst("vAlias"));
+ let b = app(&mut tc, bf, cnst("v"));
+ tc.infer(&a).unwrap();
+ tc.infer(&b).unwrap();
+ assert!(tc.app_congruence_probe(&a, &b).unwrap());
+ assert!(tc.is_def_eq(&a, &b).unwrap());
+}
+
+#[test]
+fn dependent_spine_compares_prefix_before_later_arguments() {
+ dependent::();
+ dependent::();
+}
+
+#[test]
+fn probe_does_not_nest_and_reset_clears_its_flag() {
+ let mut env = setup::();
+ let mut tc = TypeChecker::new(&mut env);
+ let (a, b) = chain(&mut tc, 4);
+ tc.in_app_congruence = true;
+ let fuel = tc.rec_fuel;
+ assert!(!tc.app_congruence_probe(&a, &b).unwrap());
+ assert!(tc.in_app_congruence);
+ assert_eq!(tc.rec_fuel, fuel);
+ tc.reset();
+ assert!(!tc.in_app_congruence);
+}
+
+#[test]
+fn shallow_comparisons_do_not_pay_for_speculative_work() {
+ let mut env = setup::();
+ let mut tc = TypeChecker::new(&mut env);
+ let (a, b) = chain(&mut tc, 4);
+ tc.def_eq_depth = APP_CONGRUENCE_MIN_DEPTH - 1;
+ let fuel = tc.rec_fuel;
+ assert!(!tc.try_app_congruence(&a, &b).unwrap());
+ assert_eq!(tc.rec_fuel, fuel);
+ assert!(tc.env.def_eq_cache.is_empty());
+ tc.def_eq_depth += 1;
+ assert!(tc.try_app_congruence(&a, &b).unwrap());
+ assert_eq!(tc.def_eq_depth, APP_CONGRUENCE_MIN_DEPTH);
+}
+
+fn below_guard_matches_original() {
+ for n in [1, 64, 128] {
+ let check = |old: bool| {
+ let mut env = setup::();
+ let mut tc = TypeChecker::new(&mut env);
+ tc.in_app_congruence = old;
+ let (a, b) = chain(&mut tc, n);
+ assert!(tc.is_def_eq(&a, &b).unwrap());
+ assert!(tc.def_eq_peak < APP_CONGRUENCE_MIN_DEPTH);
+ (tc.fuel_used(), tc.def_eq_peak)
+ };
+ assert_eq!(check(false), check(true), "chain length {n}");
+ }
+}
+
+#[test]
+fn ordinary_comparisons_preserve_recursive_work_and_depth() {
+ // Depth 64 was enough to activate the earlier eager variant. These
+ // successful ordinary checks should do exactly the original work now.
+ below_guard_matches_original::();
+ below_guard_matches_original::();
+}
+
+#[test]
+fn cached_unequal_child_only_abandons_the_probe() {
+ let mut env = setup::();
+ let mut tc = TypeChecker::new(&mut env);
+ let a = app(&mut tc, cnst("F"), cnst("a"));
+ let b = app(&mut tc, cnst("F"), cnst("b"));
+ assert!(!tc.is_def_eq(&a, &b).unwrap());
+ let left = app(&mut tc, cnst("ignore"), a);
+ let right = app(&mut tc, cnst("ignore"), b);
+ let fuel = tc.rec_fuel;
+ let key = pair_key(&mut tc, &left, &right);
+ assert!(!tc.app_congruence_probe(&left, &right).unwrap());
+ assert_eq!(tc.rec_fuel, fuel - 1, "the cached child must not be expanded");
+ assert!(!tc.env.def_eq_cache.contains_key(&key));
+ assert!(tc.is_def_eq(&left, &right).unwrap());
+}
+
+fn generated(
+ tc: &mut TypeChecker<'_, M>,
+ seed: u64,
+ depth: u64,
+) -> KExpr {
+ if depth == 0 {
+ return tc.intern(cnst(["a", "b", "alias"][(seed % 3) as usize]));
+ }
+ let child = generated(tc, seed / 3 + 1, depth - 1);
+ match seed % 4 {
+ 0 => app(tc, cnst("F"), child),
+ 1 => app(tc, cnst("id"), child),
+ 2 => app(tc, cnst("ignore"), child),
+ _ => {
+ let f = app(tc, cnst("G"), child.clone());
+ app(tc, f, child)
+ },
+ }
+}
+
+fn differential() {
+ for n in 0..96 {
+ let check = |old: bool| {
+ let mut env = setup::();
+ let mut tc = TypeChecker::new(&mut env);
+ tc.in_app_congruence = old;
+ // Exercise the worklist even on these small terms. Both variants
+ // start at the same depth; only the old path disables the probe.
+ tc.def_eq_depth = APP_CONGRUENCE_MIN_DEPTH;
+ let a = generated(&mut tc, n * 17 + 3, 5);
+ let b = generated(&mut tc, n * 13 + 3, 5);
+ tc.is_def_eq(&a, &b).unwrap()
+ };
+ assert_eq!(check(false), check(true), "seed {n}");
+ }
+}
+
+#[test]
+fn small_well_typed_terms_match_original_recursive_conversion() {
+ differential::();
+ differential::();
+}
+
+fn universes_and_arity() {
+ let mut env = setup::();
+ // An unused universe parameter leaves both applications well typed, but
+ // different instantiations of an irreducible axiom are not def-eq heads.
+ env.insert(
+ id("poly"),
+ KConst::Axio {
+ name: M::meta_field(Name::anon()),
+ level_params: M::meta_field(vec![Name::str(
+ Name::anon(),
+ "u".to_owned(),
+ )]),
+ is_unsafe: false,
+ lvls: 1,
+ ty: arrow(cnst("A"), cnst("A")),
+ },
+ );
+ let mut tc = TypeChecker::new(&mut env);
+ tc.def_eq_depth = APP_CONGRUENCE_MIN_DEPTH;
+ let a =
+ app(&mut tc, KExpr::cnst(id("poly"), Box::new([KUniv::zero()])), cnst("a"));
+ let b = app(
+ &mut tc,
+ KExpr::cnst(id("poly"), Box::new([KUniv::succ(KUniv::zero())])),
+ cnst("a"),
+ );
+ tc.infer(&a).unwrap();
+ tc.infer(&b).unwrap();
+ assert_eq!(tc.try_same_head_spine(&a, &b).unwrap(), None);
+ assert!(!tc.app_congruence_probe(&a, &b).unwrap());
+ assert!(!tc.is_def_eq(&a, &b).unwrap());
+
+ let partial = app(&mut tc, cnst("G"), cnst("a"));
+ let full = app(&mut tc, partial.clone(), cnst("b"));
+ tc.infer(&partial).unwrap();
+ tc.infer(&full).unwrap();
+ assert_eq!(tc.try_same_head_spine(&partial, &full).unwrap(), None);
+}
+
+#[test]
+fn same_head_is_not_enough_without_matching_universes_and_arity() {
+ universes_and_arity::();
+ universes_and_arity::();
+}
diff --git a/crates/kernel/src/def_eq/binders.rs b/crates/kernel/src/def_eq/binders.rs
new file mode 100644
index 000000000..4e7e9f00c
--- /dev/null
+++ b/crates/kernel/src/def_eq/binders.rs
@@ -0,0 +1,191 @@
+//! Positive-only batched lambda/forall congruence.
+//!
+//! Domains are compared under the already-accepted prefix, before adding
+//! the SAME fresh local to both sides. The terminal bodies are opened once.
+//! Each accepted binder therefore follows the existing single-binder rule.
+//! See Ix/Tc/Verify/DefEq/Structural.lean (quickBinder_wf) and the lamDF /
+//! forallEDF rules in lean4lean. Those proofs do not certify this Rust loop.
+//!
+//! This is not a complete conversion procedure for binder terms: skipping
+//! intermediate conversion can miss reduction/proof-irrelevance/cache wins.
+//! A false or exhausted probe falls back to the original single-binder path,
+//! with batching disabled throughout that fallback. No pending/suffix pair
+//! is published equal, and no failed probe is published as an inequality.
+
+use super::*;
+use ix_common::env::{BinderInfo, Name};
+
+const BINDER_BATCH_MIN_LENGTH: usize = 4;
+const BINDER_BATCH_FUEL: u64 = 4_096;
+
+struct BinderPair<'a, M: KernelMode> {
+ name: &'a M::MField,
+ bi: &'a M::MField,
+ left_ty: &'a KExpr,
+ right_ty: &'a KExpr,
+ left_body: &'a KExpr,
+ right_body: &'a KExpr,
+}
+
+fn binder_pair<'a, M: KernelMode>(
+ a: &'a KExpr,
+ b: &'a KExpr,
+) -> Option> {
+ match (a.data(), b.data()) {
+ (ExprData::Lam(name, bi, at, ab, _), ExprData::Lam(_, _, bt, bb, _))
+ | (ExprData::All(name, bi, at, ab, _), ExprData::All(_, _, bt, bb, _)) => {
+ Some(BinderPair {
+ name,
+ bi,
+ left_ty: at,
+ right_ty: bt,
+ left_body: ab,
+ right_body: bb,
+ })
+ },
+ _ => None,
+ }
+}
+
+fn has_batch_prefix<'a, M: KernelMode>(
+ mut a: &'a KExpr,
+ mut b: &'a KExpr,
+) -> bool {
+ for _ in 0..BINDER_BATCH_MIN_LENGTH {
+ let Some(pair) = binder_pair(a, b) else { return false };
+ a = pair.left_body;
+ b = pair.right_body;
+ }
+ true
+}
+
+impl TypeChecker<'_, M> {
+ pub(super) fn def_eq_binders(
+ &mut self,
+ a: &KExpr,
+ b: &KExpr,
+ ) -> Result> {
+ if self.in_binder_batch || !has_batch_prefix(a, b) {
+ return self.def_eq_one_binder(a, b);
+ }
+ self.in_binder_batch = true;
+ let saved_fuel = self.rec_fuel;
+ let local_fuel = saved_fuel.min(BINDER_BATCH_FUEL);
+ self.rec_fuel = local_fuel;
+ let result = self.with_lctx_scope(|tc| tc.def_eq_binder_telescope(a, b));
+ let consumed = local_fuel.saturating_sub(self.rec_fuel);
+ self.rec_fuel = saved_fuel.saturating_sub(consumed);
+ let result = match result {
+ Ok(false) | Err(TcError::MaxRecDepth | TcError::MaxRecFuel) => {
+ // Do not start another failed probe at every recursive suffix.
+ self.def_eq_one_binder(a, b)
+ },
+ other => other,
+ };
+ self.in_binder_batch = false;
+ result
+ }
+
+ /// Original binder comparison, also the reference path for differential
+ /// tests. Scope cleanup occurs on success, false, and every returned error.
+ fn def_eq_one_binder(
+ &mut self,
+ a: &KExpr,
+ b: &KExpr,
+ ) -> Result> {
+ let Some(pair) = binder_pair(a, b) else { return Ok(false) };
+ if !self.is_def_eq(pair.left_ty, pair.right_ty)? {
+ return Ok(false);
+ }
+ self.with_lctx_scope(|tc| {
+ let id = tc.fresh_fvar_id();
+ let fv = tc.intern(KExpr::fvar(id, pair.name.clone()));
+ tc.lctx.push(
+ id,
+ LocalDecl::CDecl {
+ name: pair.name.clone(),
+ bi: pair.bi.clone(),
+ ty: pair.left_ty.clone(),
+ },
+ );
+ let left = instantiate_rev(
+ &mut tc.env.intern,
+ pair.left_body,
+ std::slice::from_ref(&fv),
+ );
+ let right = instantiate_rev(&mut tc.env.intern, pair.right_body, &[fv]);
+ tc.is_def_eq(&left, &right)
+ })
+ }
+
+ fn def_eq_binder_telescope<'a>(
+ &mut self,
+ mut a: &'a KExpr,
+ mut b: &'a KExpr,
+ ) -> Result> {
+ let mut fvars = Vec::new();
+ loop {
+ // Opening the same raw expression under the same prefix yields the
+ // same expression. This is structural identity, not an in-flight pair.
+ if a.ptr_eq(b) || a.hash_key() == b.hash_key() {
+ return Ok(true);
+ }
+ // Closed suffixes are unchanged by opening: honor existing conversion
+ // caches without materializing suffixes merely to look them up.
+ if !fvars.is_empty()
+ && a.lbr() == 0
+ && b.lbr() == 0
+ && self.has_closed_binder_result(a, b)
+ {
+ return self.is_def_eq(a, b);
+ }
+ let Some(pair) = binder_pair(a, b) else { break };
+ if !fvars.is_empty() {
+ // Corresponds to entering another nontrivial binder comparison.
+ // Keeps the iterative walk fuel-bounded without growing the stack.
+ self.tick()?;
+ crate::profile::bump_def_eq();
+ }
+ // Each substitution has its own memo: distinct prefixes must never
+ // share a semantic substitution result just to reuse scratch storage.
+ let left_ty = instantiate_rev(&mut self.env.intern, pair.left_ty, &fvars);
+ let right_ty =
+ instantiate_rev(&mut self.env.intern, pair.right_ty, &fvars);
+ if !self.is_def_eq(&left_ty, &right_ty)? {
+ return Ok(false);
+ }
+ let id = self.fresh_fvar_id();
+ let fv = self.intern(KExpr::fvar(id, pair.name.clone()));
+ self.lctx.push(
+ id,
+ LocalDecl::CDecl {
+ name: pair.name.clone(),
+ bi: pair.bi.clone(),
+ ty: left_ty,
+ },
+ );
+ fvars.push(fv);
+ a = pair.left_body;
+ b = pair.right_body;
+ }
+ let left = instantiate_rev(&mut self.env.intern, a, &fvars);
+ let right = instantiate_rev(&mut self.env.intern, b, &fvars);
+ self.is_def_eq(&left, &right)
+ }
+
+ fn has_closed_binder_result(&mut self, a: &KExpr, b: &KExpr) -> bool {
+ let ctx = self.def_eq_ctx_key(a, b);
+ let (lo, hi) = canonical_pair(a.hash_key(), b.hash_key());
+ let key = (lo, hi, ctx);
+ self.env.def_eq_cache.contains_key(&key)
+ || (self.cheap_recursion_depth > 0
+ && self.env.def_eq_cheap_cache.contains_key(&key))
+ || self.equiv_manager.is_equiv(
+ &crate::equiv::EqKey::new(a.hash_key(), ctx, 0, 0),
+ &crate::equiv::EqKey::new(b.hash_key(), ctx, 0, 0),
+ )
+ }
+}
+
+#[cfg(test)]
+mod tests;
diff --git a/crates/kernel/src/def_eq/binders/tests.rs b/crates/kernel/src/def_eq/binders/tests.rs
new file mode 100644
index 000000000..9c7a81277
--- /dev/null
+++ b/crates/kernel/src/def_eq/binders/tests.rs
@@ -0,0 +1,516 @@
+use super::*;
+use crate::env::KEnv;
+use crate::level::KUniv;
+use crate::mode::{Anon, Meta};
+use crate::profile::{OpCounts, take_op_counts};
+use ix_common::address::Address;
+use ix_common::env::{DefinitionSafety, ReducibilityHints};
+
+fn name(s: &str) -> M::MField {
+ M::meta_field(Name::str(Name::anon(), s.to_owned()))
+}
+
+fn id(s: &str) -> KId {
+ KId::new(Address::hash(s.as_bytes()), name::(s))
+}
+
+fn cnst(s: &str) -> KExpr {
+ KExpr::cnst(id(s), Box::new([]))
+}
+
+fn var(i: u64) -> KExpr {
+ KExpr::var(i, name::("original-var"))
+}
+
+fn sort() -> KExpr {
+ KExpr::sort(KUniv::succ(KUniv::zero()))
+}
+
+fn binder(
+ is_lam: bool,
+ ty: KExpr,
+ body: KExpr,
+) -> KExpr {
+ let n = name::(if is_lam { "lambda" } else { "forall" });
+ let bi = M::meta_field(BinderInfo::Implicit);
+ if is_lam { KExpr::lam(n, bi, ty, body) } else { KExpr::all(n, bi, ty, body) }
+}
+
+fn axiom(env: &mut KEnv, s: &str, ty: KExpr) {
+ env.insert(
+ id(s),
+ KConst::Axio {
+ name: name::(s),
+ level_params: M::meta_field(vec![]),
+ is_unsafe: false,
+ lvls: 0,
+ ty,
+ },
+ );
+}
+
+fn defn(
+ env: &mut KEnv,
+ s: &str,
+ ty: KExpr,
+ val: KExpr,
+) {
+ env.insert(
+ id(s),
+ KConst::Defn {
+ name: name::(s),
+ level_params: M::meta_field(vec![]),
+ kind: DefKind::Definition,
+ safety: DefinitionSafety::Safe,
+ hints: ReducibilityHints::Regular(7),
+ lvls: 0,
+ ty,
+ val,
+ lean_all: M::meta_field(vec![]),
+ block: id(s),
+ },
+ );
+}
+
+fn setup() -> KEnv {
+ let mut env = KEnv::new();
+ axiom(&mut env, "A", sort());
+ axiom(&mut env, "B", sort());
+ axiom(&mut env, "a", cnst("A"));
+ axiom(&mut env, "b", cnst("A"));
+ axiom(
+ &mut env,
+ "G",
+ binder(false, sort(), binder(false, var(0), binder(false, var(1), var(2)))),
+ );
+ axiom(&mut env, "P", binder(false, sort(), binder(false, var(0), sort())));
+ defn(&mut env, "Alias", sort(), cnst("A"));
+ defn(&mut env, "alias", cnst("A"), cnst("a"));
+ defn(
+ &mut env,
+ "id",
+ binder(false, cnst("A"), cnst("A")),
+ binder(true, cnst("A"), var(0)),
+ );
+ defn(
+ &mut env,
+ "ignore",
+ binder(false, cnst("A"), cnst("A")),
+ binder(true, cnst("A"), cnst("a")),
+ );
+ env
+}
+
+fn telescope(
+ n: usize,
+ is_lam: bool,
+ mut body: KExpr,
+) -> KExpr {
+ for _ in 0..n {
+ body = binder(is_lam, cnst("A"), body);
+ }
+ body
+}
+
+fn compare(
+ a: &KExpr,
+ b: &KExpr,
+ old: bool,
+) -> (bool, u64, u32, OpCounts) {
+ let mut env = setup::();
+ let mut tc = TypeChecker::new(&mut env);
+ tc.in_binder_batch = old;
+ let a = tc.intern(a.clone());
+ let b = tc.intern(b.clone());
+ take_op_counts();
+ let verdict = tc.is_def_eq(&a, &b).unwrap();
+ assert!(tc.lctx.is_empty());
+ assert_eq!(tc.def_eq_depth, 0);
+ assert_eq!(tc.in_binder_batch, old);
+ (verdict, tc.fuel_used(), tc.def_eq_peak, take_op_counts())
+}
+
+fn long_positive(
+ count: u64,
+ compare_reference: bool,
+ report: bool,
+) {
+ for is_lam in [false, true] {
+ // (T : Type) (x1 : T) ... (x_{count-1} : T). Unlike closed suffixes,
+ // these domains really must be traversed by repeated single opening.
+ let make = |alias: bool| {
+ // Every value binder is used, so each single opening must revisit
+ // the terminal DAG; merely depending on T would only traverse once.
+ let g = KExpr::app(cnst("G"), var(count - 1));
+ let mut body = var(0);
+ for i in 1..count - 1 {
+ body = KExpr::app(KExpr::app(g.clone(), var(i)), body);
+ }
+ if !is_lam {
+ body = KExpr::app(KExpr::app(cnst("P"), var(count - 1)), body);
+ }
+ if alias {
+ let ty = if is_lam { var(count - 1) } else { sort() };
+ body = KExpr::let_(name::("alias"), ty, body, var(0), false);
+ }
+ for i in (0..count).rev() {
+ let ty = if i == 0 { sort() } else { var(i - 1) };
+ body = binder(is_lam, ty, body);
+ }
+ body
+ };
+ let a = make(false);
+ let b = make(true);
+ let mut env = setup::();
+ let mut tc = TypeChecker::new(&mut env);
+ tc.infer(&a).unwrap();
+ tc.infer(&b).unwrap();
+ let new = compare::(&a, &b, false);
+ assert!(new.0);
+ assert!(new.2 < 10, "batch peak {}", new.2);
+ if !compare_reference {
+ continue;
+ }
+ let old = compare::(&a, &b, true);
+ if report {
+ println!(
+ "mode={} lambda={is_lam} subst={}->{} intern={}->{} fuel={}->{} peak={}->{}",
+ std::any::type_name::(),
+ old.3.subst_nodes,
+ new.3.subst_nodes,
+ old.3.intern_nodes,
+ new.3.intern_nodes,
+ old.1,
+ new.1,
+ old.2,
+ new.2,
+ );
+ }
+ assert!(old.0);
+ assert!(u64::from(old.2) >= count);
+ assert!(
+ new.3.subst_nodes * 4 < old.3.subst_nodes,
+ "subst {} vs {}",
+ new.3.subst_nodes,
+ old.3.subst_nodes
+ );
+ }
+}
+
+#[test]
+fn long_telescope_opens_terminal_bodies_once() {
+ // The deliberately recursive reference needs one native frame per
+ // binder. Keep this differential/work-counter fixture within the normal
+ // test stack; exercise the full deep case on the production path below.
+ long_positive::(32, true, false);
+ long_positive::(32, true, false);
+}
+
+#[test]
+fn deep_batched_telescope_uses_default_stack() {
+ // Do not spawn a large-stack worker or require RUST_MIN_STACK here.
+ long_positive::(128, false, false);
+ long_positive::(128, false, false);
+}
+
+#[test]
+#[ignore = "manual paired work-counter report; not a wall-time benchmark"]
+fn report_dependent_telescope_work() {
+ long_positive::(32, true, true);
+ long_positive::(32, true, true);
+}
+
+fn dependent() {
+ let mut env = setup::();
+ // idPoly : (T : Type) -> T -> T
+ let id_ty = binder(false, sort(), binder(false, var(0), var(1)));
+ let id_val = binder(true, sort(), binder(true, var(0), var(0)));
+ defn(&mut env, "idPoly", id_ty, id_val);
+ for is_lam in [false, true] {
+ let make = |alias: bool| {
+ // (T : Type) (x : T) (y : T) (z : T), x / T.
+ let terminal = if is_lam { var(2) } else { var(3) };
+ let terminal = if alias && is_lam {
+ KExpr::app(KExpr::app(cnst("idPoly"), var(3)), terminal)
+ } else {
+ terminal
+ };
+ let domain_z = if alias {
+ // A local type alias reduces to T; both domains are well typed.
+ KExpr::let_(name::("D"), sort(), var(2), var(0), false)
+ } else {
+ var(2)
+ };
+ binder(
+ is_lam,
+ sort(),
+ binder(
+ is_lam,
+ var(0),
+ binder(is_lam, var(1), binder(is_lam, domain_z, terminal)),
+ ),
+ )
+ };
+ let mut tc = TypeChecker::new(&mut env);
+ let a = tc.intern(make(false));
+ let b = tc.intern(make(true));
+ tc.infer(&a).unwrap();
+ tc.infer(&b).unwrap();
+ assert!(tc.is_def_eq(&a, &b).unwrap());
+ assert!(tc.lctx.is_empty());
+ assert!(!tc.in_binder_batch);
+ }
+}
+
+#[test]
+fn dependent_domains_and_shared_fresh_locals_are_preserved() {
+ dependent::();
+ dependent::();
+}
+
+fn negative_cases() {
+ for n in [4, 8, 17] {
+ // Same domains but unequal terminal values/types.
+ for is_lam in [false, true] {
+ let (a, b) =
+ if is_lam { (cnst("a"), cnst("b")) } else { (cnst("A"), cnst("B")) };
+ let a = telescope(n, is_lam, a);
+ let b = telescope(n, is_lam, b);
+ assert!(!compare::(&a, &b, true).0);
+ assert!(!compare::(&a, &b, false).0);
+ }
+ let a = telescope(n, false, binder(false, cnst("A"), cnst("A")));
+ let b = telescope(n, false, binder(false, cnst("B"), cnst("A")));
+ assert!(!compare::(&a, &b, true).0);
+ assert!(!compare::(&a, &b, false).0);
+ }
+}
+
+#[test]
+fn failed_domains_and_terminal_comparisons_match_original() {
+ negative_cases::();
+ negative_cases::();
+}
+
+fn diverging() {
+ let a = telescope(4, true, binder(true, cnst("A"), var(0)));
+ let b = telescope(4, true, cnst("id"));
+ assert!(compare::(&a, &b, true).0);
+ assert!(compare::(&a, &b, false).0);
+ let a = telescope(4, false, cnst("A"));
+ let b = telescope(3, false, cnst("A"));
+ assert!(!compare::(&a, &b, true).0);
+ assert!(!compare::