fix: Char.ofNat / String.ofList recognized up to defeq (1/4) - #7
Merged
Conversation
VEnv.HasPrimitives pins these two constants' VConstant to a literal syntactic type, and TrConstant reads v.type off structurally. But the recognizer only checked isDefEq, so declaring Char.ofNat at `(fun _ : Nat => Nat → Char) Nat.zero` passed and translated to a different constant, refuting the recognizer's postcondition -- which quantifies over every translation, so no proof could dodge it. Both branches now compare with Expr.eqv, structural up to binder name and binder info, which is exactly what the translation sees through. The toolchain declares both at the expected shape. Structural comparison is available only for these two: the Nat primitives' declared types carry @& borrow annotations, so it would reject them. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
This was referenced Aug 22, 2026
vasnesterov
pushed a commit
that referenced
this pull request
Aug 23, 2026
…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>
vasnesterov
pushed a commit
that referenced
this pull request
Aug 23, 2026
…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>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Split out of #2, as requested. 1 of 4. Each is independent and applies to
pristine
master; they compose in any order under a normal 3-way merge.The bug
VEnv.HasPrimitivespins these two constants'VConstantto a literalsyntactic type — e.g.
Char.ofNat ↦ ⟨0, .forallE .nat .char⟩— andTrConstantreadsv.typeoff structurally viaTrExprS. But therecognizer only checked definitional equality:
unless ← isDefEq v.type q(Nat → Char) do failDeclaring
Char.ofNatat(fun _ : Nat => Nat → Char) Nat.zeropasses that andtranslates to a structurally different
VConstant.PrimitiveResult.preservesquantifies over every
ci'withTrDefVal, so no proof can dodge it — therecognizer's postcondition was simply false. Same for
String.ofList.The fix
Compare with
Expr.eqv(==) — structural up to binder name and binder info,which is exactly what
TrExprSsees through (it discards both). Verified thetoolchain declares both at the expected shape:
Expr.eqvreturnstruefor both;Expr.equalreturnsfalsefor both (bindernames differ), confirming
eqvis the right notion.Also pins the
String.ofListbranch's containment guard, which belongs with it.This is available only for these two constants. The
Natprimitives'declared types carry
@&borrow annotations(
.mdata { borrowed := true }around eachNatdomain), so structuralcomparison would reject them — which is why the sibling PRs take a different
route for those.
Testing
lake build lean4leangreen, including therun_metaself-test that runs therecognizer over all 24 entries of
Environment.primitivesin the liveenvironment.
On the arena: the recognizer gets strictly stricter, and the combined
change of all four splits was arena-verified at 185 correct / 6 either /
0 incorrect, the baseline. Since each split is a subset of that strictness, no
split can reject anything the combined version accepted.
divergences.mdcarries the strictness note for the whole series — it landshere as the first of the four, so the sibling PRs need no doc change.
🤖 Generated with Claude Code