fix: instantiateRange_eq / instantiateRevRange_eq are missing a side condition by vasnesterov · Pull Request #4 · vasnesterov/lean4lean

vasnesterov · 2026-08-22T12:41:01Z

The bug

@[simp] axiom instantiateRange_eq (e : Expr) (start stop : Nat) (subst : Array Expr) :
    e.instantiateRange start stop subst = …
@[simp] axiom instantiateRevRange_eq …

Lean.Expr.instantiateRange and instantiateRevRange are @[extern] wrappers
over kernel/instantiate.cpp. When the range is out of bounds the C function
does not return some other value — it prints INTERNAL PANIC and aborts
the process (instantiate.cpp:82). The axioms assert an equation on those
inputs anyway, so they are true only under a side condition they do not state.

Unlike the two axioms that prove False outright, these are not
Lean-inconsistent: the upstream side is opaque, so no contradiction is
derivable inside Lean. They are still wrong as descriptions of what runs, and
the checker's correctness rests on them.

The fix

Add the two bounds:

@[simp] axiom instantiateRange_eq (e : Expr) (start stop : Nat) (subst : Array Expr)
    (h₁ : start ≤ stop) (h₂ : stop ≤ subst.size) : …

Cost: zero proof changes

Both are @[simp], and simp's own discharger closes start ≤ stop and
stop ≤ subst.size at every call site. Verify/TypeChecker/WHNF.lean and
Verify/TypeChecker/InferType.lean are untouched.

I checked that the rewrites still actually fire — rather than silently failing
to apply while the proofs succeed by some other route — with #print axioms:
both names remain in the axiom cone of TypeChecker.Inner.whnfCore'.WF and
TypeChecker.Inner.inferApp.loop.WF.

lake build Lean4Lean.Verify green, 1197 jobs, no new warnings.

Lean4Lean/Inductive/Add.lean:626 also calls instantiateRevRange, but has no
verified counterpart in the Lean4Lean.Verify cone, so there was nothing to
repair there.

One caveat worth keeping

These are now conditional simp lemmas. If a future call site's bound is not
discharged by simp's discharger, the rewrite will silently not fire rather than
error. That is the fail-safe direction — the proof breaks rather than
succeeding wrongly — but it makes the #print axioms spot-check above worth
repeating when call sites are added.

Note on the freeze

Verify/Axioms.lean is frozen per CLAUDE.md; this is a proposal for sign-off.
Axiom names are unchanged, so guard 1's 32-axiom list still matches.

Found by an audit of all 32 axioms, which also produced #1 (merged) and the
sibling PRs for the other findings.

🤖 Generated with Claude Code

…tion Both equate a Lean model with `Lean.Expr.instantiateRange` / `instantiateRevRange`, which are `@[extern]` wrappers over `kernel/instantiate.cpp`. Out of range the C function does not return a different value -- it prints INTERNAL PANIC and aborts the process. The axioms assert an equation there anyway. Both now carry `start ≤ stop` and `stop ≤ subst.size`. No proof changes were needed. Both are `@[simp]`, and simp's own discharger closes the two bounds at every call site, so Verify/TypeChecker/WHNF.lean and Verify/TypeChecker/InferType.lean are untouched. That the rewrites still fire, rather than silently failing while the proofs succeed by another route, was confirmed with `#print axioms`: both names remain in the axiom cone of whnfCore'.WF and inferApp.loop.WF. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

vasnesterov · 2026-08-22T12:58:53Z

I approve, merge this

…d a guard class the audit missed **The systemic finding: a guard class §6/§7.1 did not account for.** Every `@[extern]` C entry point in scope that takes a `Nat` begins with a **`lean_is_scalar` bignum test -- before** the range test the audit records. `LEAN_MAX_SMALL_NAT = SIZE_MAX >> 1`, so it fires at `2^63`. §6 describes `lean_expr_instantiate_range` as "starts with `if (b > e || e > sz) lean_internal_panic`" -- that is the function's **second** statement, not its first. **Seven axioms in scope sit on that guard**, and it resolves four different ways. ## #21 `Lean.Expr.liftLooseBVars_eq` is FALSE if (!lean_is_scalar(s) || !lean_is_scalar(d)) { lean_inc(e); return e; } Witness `e := .bvar 0`, `s := 0`, `d := 2^63`. Both halves machine-checked, deliberately **by different instruments**: - C side, differential test on compiled code: `#eval idx ((Expr.bvar 0).liftLooseBVars 0 (2^63))` prints `"bvar 0"`. - Model side, kernel reduction: `liftLooseBVars' (.bvar 0) 0 (2^63) = .bvar (2^63)`, and `≠ .bvar 0`. So the axiom asserts `.bvar 0 = .bvar (2^63)`. Worse than #26/digama0#27 in one specific way: **the call completes.** No panic, no exotic input -- `2^63` is an ordinary literal and `.bvar 0` an ordinary `Expr`. Only the *model's* output is not runtime-constructible, which is why the two sides cannot be evaluated in one expression (`#eval` of the model's answer trips `lean_expr_mk_data`'s own panic -- observed). **Not an inconsistency**: `liftLooseBVars` is `opaque @[extern]` and the toolchain has no core theorem about it, so there is no second fact to contradict. Same category as #12/#17. Fix is `d < 2^63` or a `USize` restatement -- frozen file, needs sign-off. ## Three failed attacks, recorded as failed attacks - **#22, digama0#30** carry the same guard and **survive**: the C fallback coincides with the model on every input a real `Expr` can supply, with machine-checked agreement lemmas for both. One of the stream's own witnesses was wrong -- `(.bvar 7).lowerLooseBVars (2^63) 1` returns `bvar 7` from *both* sides -- and the correction is recorded rather than quietly dropped. - **digama0#29 `abstractRange_eq`**, the only unconditional range axiom, also survives: its fallback uses `lean_array_size` and `Array.extract 0 n` clamps to the same thing, agreeing at **every** input, logical or not. Verdict unchanged, for a reason §7.1 did not state. ## #26/digama0#27: the side condition is necessary but NOT sufficient `start ≤ stop ≤ subst.size` excludes the second guard, not the first -- `stop` may be non-scalar provided `subst.size` is too, which needs `subst.size ≥ 2^63`: expressible, not constructible. Strictly weaker than #21, no differential test possible. **Source reading only, and marked as such.** ## The two other priority targets, answered - **#17 `Expr.mkData_eq` -- no analogous consequence.** `lean_expr_mk_data` panics twice, and its hypothesis implies **both** are passed; the `approxDepth` clamp matches too. Unlike #12, correctly guarded. - **#3 `PersistentArray.toList'_push` -- hypothesis adequate**, in the strongest available sense: `WF` is generated by `empty`/`push` only, and a reverse scan shows lean4lean uses **no other `PersistentArray` operation**. So `WF` is exactly the reachable set, not an approximation. Not reached: #4-#7. **digama0#31's dependency on #15 deliberately not pursued** -- #15 belongs to another stream's section, and a cross-section attack run from one side only is the weaker version of the test. **No `False` was derived.** §11.9 keeps the evidence strengths separate: differential-test-plus-source, source-only, and proof are three different things, and none of this is a proof. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

…er, not the worker **The criterion answered a different question than expected.** Asked which side condition the consumers satisfy for free, an axiom-cone scan (`Lean.collectAxioms`) over every non-internal `Lean4Lean.*` declaration returned: | axiom | dependents | |---|---| | **`Lean.Expr.liftLooseBVars_eq`** | **0** | | the other 13 in scope | 35 - 162 each | Zero for a structural reason, not by luck: **the checker never calls `Expr.liftLooseBVars`.** No occurrence outside `Verify/` and `Experimental/`, and the only textual matches inside `Verify/` are theorems about the *model* `liftLooseBVars'`, none about the opaque constant. The axiom is `@[simp]`, so it has no explicit call sites either way -- and the cone scan is exactly what settles that, since a `@[simp]` lemma that fires does appear in the proof term. **So the fix is subtraction, not domestication:** deleting it cannot break a proof, and it removes a live false axiom. Fallback if a reviewer prefers to keep the statement: the C guard is `!lean_is_scalar(s) || !lean_is_scalar(d)`, so **both** arguments need bounding -- `s < 2^63 ∧ d < 2^63`, not `d < 2^63` alone. A `USize` restatement does not fit without changing the signature. **The guard class, stated as method in §11.1.** §7.1's entries describe the *worker* functions faithfully; what they skip is the `extern "C"` wrapper, which is where argument validation lives. > For any `@[extern]` axiom, read the wrapper first and enumerate every > early return before reading the algorithm. A `Nat` crossing into C is boxed, hence always bignum-guarded, and the guard either panics or silently substitutes a fallback the axiom must then match. **Seven of fourteen axioms in scope sit on one.** **Four more failed attacks (#4-#7), recorded with their failure step.** - **#6 `findAux_isSome` survives** -- both sides use the *same* `==` and the functions are parallel clause-for-clause; the shared panic-index agrees whatever `default : Entry` is. - **#4/#5 survive a non-reflexive `BEq`.** `PartialEquivBEq` requires symmetry and transitivity but **not** reflexivity, so `⟨fun _ _ => false⟩` is legal and `LawfulHashable` is vacuous -- a key can be inserted twice and the filter deletes nothing. Both axioms still hold. Hand-executed, not machine-checked, and marked so. - **#7 `structEq_eq` survives, but §7.3's reason was wrong**, in a way worth keeping. It claims `Substring.Raw.Internal.beq` *is* the `BEq` instance. Not definitionally: `example : @Substring.Raw.Internal.beq = (· == ·) := rfl` **fails**. The identity holds *through the linker*, via an `@[extern]`/`@[export]` pairing -- weaker assurance, and the reason this axiom can never be discharged by unfolding. The attack it prompted (position-sensitivity like `Substring.Raw.sameAs`) fails under differential test, with both negative controls checked. Still declined: **digama0#31's dependency on #15**, since from one side it is the weaker test. Ready to pair with the `Level` stream. §11.9 keeps the three evidence strengths separate and now names the cone scan as the strongest instrument in the pass -- a complete search over the environment rather than a sample -- which is why #21's recommendation is *delete* rather than *weaken*. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

… a documentation artifact **`ORCHESTRATOR.md`** -- orchestrator-only instructions, separate from `CLAUDE.md` which is for every agent. Centrepiece: **prefer handoffs to resumes.** A resumed agent carries a long, mostly irrelevant transcript and drifts toward what it already believes; instead ask a stream at a boundary to write `docs/handoff-<topic>.md` and point a **fresh** agent at it. The handoff must carry what a newcomer cannot cheaply reconstruct -- in particular **what was tried and failed, and the step it failed at**, which is the half that gets lost and the most common waste to re-derive. Also records the git gate, explicit-path staging, one-file-one-stream with boundaries rather than arbitration, and ruling on measurements rather than reasons. **Audit §13.** No inconsistency found; one recorded justification corrected, one risk bounded. **digama0#31's "depends on 15" is a documentation artifact.** A constant-dependency scan over statement, value and the `brecOn` helper shows `Expr.eqv_eq`, `Expr.eqv'` and `eqv'._f` mention `instLawfulBEqLevel` **nowhere**. What digama0#31 actually rests on is different in kind and strictly weaker: that `BEq Level` is **the same function** C uses, not that it is **lawful** -- the instance *is* `Level.beq` definitionally, `Level.beq` is `@[extern "lean_level_eq"]`, and `expr_eq_fn.cpp` compares levels with that same symbol. **Why it is worth fixing:** if #15 were refuted -- if `lean_level_eq` normalised and so were not structural -- **digama0#31 would be unaffected**, because both sides of `eqv_eq` would use the same non-structural comparison and still agree. The annotation invites the inference *"refuting 15 propagates to 31"*, which is false. Same shape as §7.3: right verdict, wrong recorded reason. Bonus sweep: the `LawfulBEq Expr` route was re-run as an environment-wide instance scan over the **whole import closure** rather than core alone. The only such instance in scope is `instLawfulBEqLevel`, and it is for `Level`. Route closed over the closure. **Container axioms: `WF` is the reachable set for #4/#5 too**, by a longer chain. Only 7 distinct `PersistentHashMap`/`PersistentArray` constants are referenced by any `Lean4Lean.*` declaration, and `insert`/`find?` are not among them -- they arrive through `ConstMap = SMap Name ConstantInfo`. `SMap.map₂` **defaults to empty**; `fromHashMap` sets only `map₁` and the stage; `SMap.insert` is **the only writer of `map₂`**; the single construction site is at stage 2, so every later insert lands in `map₂` starting from `∅`. Hence every reachable `PersistentHashMap` is `empty` followed by `insert`s -- exactly `WF`'s two generators. `erase`, `modify`, `insertIfNew`, `ofList` are unreachable. **What that buys, stated narrowly:** it rules out the failure mode that actually produced a `False` here -- an axiom stated for arbitrary, including malformed, structures -- since a hypothesis that is exactly the reachable set cannot be applied outside its domain. It does **not** make the axioms true *on* that domain: no model of the HAMT or the trie exists, so an error in the algorithms themselves survives untouched. **Class (B) risk is bounded, not removed**, and §13.5's evidence table ends with the row `#4/#5 are true -- none, still no model`, which is the point of the table. Three more failed attacks recorded in §13.4. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

…is a sixth instrument blindness Two streams. Both closed something; both found that a thing I called an open question was already in the tree. ## Input A of the model side is discharged `Theory/SetModel/ModelExists.lean`. `ModelExistsInput` really was Foundation-gluing, ~10 lines, and the two non-obvious steps are why nobody had applied it: `small_satisfiable_of_consistent` is `Satisfiable.{0}` for `ℒₛₑₜ : Language.{0}`, so the model lands in `Type 0` -- exactly the `V : Type` downstream binds, with no `ULift` needed *or available*; and `QuotNormalize` needs `M ⊧* 𝗘𝗤`, which is **not** automatic for a bare structure and has to come from the theory via `eq_subset_zfcInacc`. So `inaccModelInput : InaccModelInput` is a **theorem** and `upper_bound_of_modelFits` puts the whole model side on **one** input. Bounded both ways with care: `modelExists_iff_consistent` states the *consistency-free* form as equivalent to `Consistent 𝗭𝗙𝗖+𝗜𝗻𝗮𝗰𝗰`, deliberately **not** as `↔ True`, which is true and useless. Also: `inductOracleOK_zero` closes **both** fields of `InductOracleOK` at `boxDecl` -- a block certified `WF` on a reachable history -- filling §5's open `consts` cell, with `oracleFits_zero`/`coherentOn_zero` leaving only the `PropSplit` hypotheses. Limitation stated rather than upgraded: the oracle is `fun _ _ ↦ ∅`, so every declared type is a `∀` over an empty domain; the sharpened open case is a `WF` block with *inhabited* parameter domains. ## A sixth instrument blindness, and the most dangerous yet `Above M P := ∃ m, IsInaccessibleChain m M.κ → P`. If there is **any** `m` at which `M.κ` fails to be a chain, the implication is vacuously true and so is `Above M P` **for every `P`, including `False`** -- and `not_isInaccessibleChain_const` supplies such a `κ`. Every field of `OracleOK`, `QuotOracleOK`, `InductOracleOK` and `DefEqOK` is an `Above`. So **any "this residual is satisfiable" claim stated through the wrapper at arbitrary `κ` measures nothing.** I verified both halves myself. This sits one level *below* the field level row 11a taught us to check. Guard: a positive bound on an `Above`-wrapped field must factor through `Above.pure`, or be restated with the wrapper stripped -- the stream did both (`mem_interp_consts_zero`, `defEq_rules_zero`). **Every pre-existing positive bound in `Theory/SetModel/` needs re-auditing against this.** ## The β-gap is closed -- and my "open question" was an import line `VEnv.IsDefEq.betaMkLams` (`StructureClosed.lean:305`) *is* the direct typed-β lemma: it takes `env.Ordered` and nothing else, so no `Params`, no `env.WF`, no circularity. I verified that `beta` is a **primitive constructor** of `IsDefEq` (`Theory/Typing/Basic.lean:45`), so one typed β-step never needed confluence at all. My `Params`/`ChurchRosser` reading was right; "a direct typed-β lemma avoiding it is the open question" was wrong -- `StructureClosed` was simply outside `NestedRules`' import cone. `substC_tyApp_defeq_tyAppR_comp` now has **no bound on `D.np`**, and `substC_tyApp_defeqU_tyAppR` drops `hp : D.params = []`. `csubst_WF` derives three of four fields (`closed`, `const`, `defeq`); `val` is the only hypothesis left, bounded both ways -- upper by `csubst_val_cases`, lower by `instAt_indep_of_tyArgs`, which shows `Faithful` **cannot** constrain the spine at all (`instAt` takes the same value for every spine once the body is closed), so the residual is data, not a lemma waiting. **And `hargs` ≡ §8.8's `hbody`: the β-gap and the `CSubst.WF` remainder are one obligation, not two.** ## Five corrections to my brief, and #4 unseats my own ordering rule 1. "`(R.csubst D K).WF` is the shared remainder of all three" -- not for (A), which takes `csubstTy`, a strictly smaller domain. Three substitution/environment pairs. 2. **"closing the β-gap likely lifts all three -- verify that"**: verified, and it does not. (B)/(C) are strictly **downstream** of (A) three ways, and the defeq-tolerant bridges they would need (`recConstsR_wf_of_substC'`, `iotaRulesRS_wf_of_substC'`) **do not exist** -- 0 hits. Asking for verification instead of asserting was the right call and I was wrong. 3. "no `Classical.choice`" -- true of the two `NestedRules` results, false of (A)'s `ctorConstsCR_wf_of_np_zero'`. All three together do use it. 4. **The implementation-side `SubstFree` discharge is not "in scope" -- it is currently impossible.** There is **no function anywhere** mapping `ElimNestedInductive.Result` to a `VIndRestore`; all eight producers are hand-written examples or `idRestore`, and the only place the implementation supplies an `R` is the degenerate `res.aux2nested = []` case. Worse, the fact that would make `SubstFree` true is **not expressible**: no abstract predicate constrains `K`'s names, and the only `_nested`-prefix test is `checkNoNestedAux`, which nothing abstract consumes. So my ordering rule -- prove the implementation side first, then add the conjunct -- set an **unsatisfiable** precondition. **The critical path is an `R`-from-checker-data construction, which does not exist and which I never named.** 5. The working tree was clean at session start, not carrying uncommitted work. The stream also self-reported a false negative in my own taxonomy: its first grep missed `theorem VEnv.…`-qualified names. Acceptance: cone green (1385 jobs), guards 1 ✓ (24) / 2 ✓ (INCOMPLETE) / 3 ✓ (2/2), census **13**, dup-names clean, 295 modules / **0 orphaned**. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

…exact edit, in writing I had queued 'close census holes #3 and #4, 13 -> 11' and recorded that it was my call and I was taking it, on the grounds that a hole which can be honestly closed should be. Opening the file to apply it, both sorry sites begin 'Still sorry, deliberately' and name the exact proof term my audit proposed. Their argument is better than mine on every point. The close is not honest: the producer does not mention the first term at all, so the conclusion would hold for a completely arbitrary translation of it — it proves the branch is dead, not that the checker is sound on it, and 'honestly closable' was my whole justification. The producer is a deliberate tripwire, kept live because it goes red the moment the nested construction gains constructors, which is when the obligation becomes real — closing the hole trades a loud failure for a silent one at exactly that moment. And the real statement is already in the file: the hole is that statement with its two hypotheses removed, neither provable today. Cancelled, not deferred, with the queue entry struck through rather than deleted so the reversal stays visible. Three things I take from it. My audit read the producers and not the holes — it verified the one-line close elaborates and ranked it first without reading the docstring attached to the very sorry it proposed to fill, and its one piece of restraint (leave the third hole alone, its sorry carries information) was right for a reason that applies verbatim to the other two. 'Look at the target before overwriting' is the only reason this did not land: a census number would have improved and the project would have been worse. And I had the trade backwards — a census that counts vacuous closes is worse than one that overstates, because two of those thirteen entries are load-bearing tripwires and the source says so. Standing brief line added: before proposing a proof for a hole, read that hole's own docstring and quote it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

vasnesterov merged commit f077b5a into master Aug 22, 2026

Navigation Menu

fix: instantiateRange_eq / instantiateRevRange_eq are missing a side condition - #4

fix: instantiateRange_eq / instantiateRevRange_eq are missing a side condition#4
vasnesterov merged 1 commit into
masterfrom
fix/instantiate-range-axioms

vasnesterov commented Aug 22, 2026

Uh oh!

vasnesterov commented Aug 22, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

vasnesterov commented Aug 22, 2026

The bug

The fix

Cost: zero proof changes

One caveat worth keeping

Note on the freeze

Uh oh!

vasnesterov commented Aug 22, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant