fix: soundness bug in {Expr, Level}.data

[digama0]

This PR fixes an issue with handling of extremely large or deep expressions in the kernel which could lead to unsound behavior in some scenarios.

The problem

Every Expr and Level comes with a small computed field which keeps track of some aggregate data. Because this is a fixed size field, only small or approximate information can be stored, and unlike e.g. the maximum bound on array sizes, this is visible to lean code and the bit tricks are implemented in lean itself. Both types are however using this field for a nominally infinite piece of data: Level tracks the depth of the expression, and Expr tracks the largest loose bvar index. Computed fields are pure functions, which have no error pathway, so this leads to a problem - how to handle overflow?

Currently, this is handled using assert! and/or panic!. But panic! is not a good substitute for error handling, because a panic does not abort execution, and lean continues with the default value for the type. In this case, that means inserting a 0 for the whole Level.Data / Expr.Data field, which is the worst possible answer: it means that the expression appears to have no loose bvars, no mvars, no fvars, even if it actually does, meaning that all of the functions Expr.hasFVar, Expr.hasExprMVar, Expr.hasLevelMVar, Expr.hasMVar, Expr.hasLevelParam, Expr.hasLooseBVars fail to be conservative, which leads to unsoundness (a test is included). See also the discussion on zulip.

The solution

Changing the computed data field to be an Option or otherwise contain error handling would likely be too expensive, and result in significant API changes. Instead, we simply make the data field give conservative answers when an overflow occurs, and avoid contaminating unrelated fields in the bitfield.

• In Level, we can simply saturate the depth at the maximum value, as is already done inside Expr. This field isn't even used for anything as far as I can tell, and there should be no added checks since the assertion was already present.
• In Expr, the mkData function is performance critical, so I tried to avoid any unnecessary branches or bounds checks. We can again saturate when the bound variable index overflows, but because we subtract 1 from looseBVarRange when constructing a binder, we have to take care to not reduce an overflowed value. This ensures conservativity. (One slight change here is that the maximum bvar number has to be decreased by 1, from 2^20-1 to 2^20-2 to leave space for the overflow value.)

In order to compensate for the removed asserts, the handling of this field is now mediated by the BVarRange type, which is just a wrapper for UInt32. I believe that the fact that this is a bounded type will actually improve performance here; the original version of the code was converting to and from Nat in order to do the arithmetic.

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 90462e25518a28ff78b96a1e35aa7edadbaa7dac --onto 72141b05fd9a3328c1e5d99211dc4da4495cbd42. You can force Mathlib CI using the force-mathlib-ci label. (2025-05-30 19:16:00)

[Kha]

I'll close this as it is covered by the PR above

[digama0]

If you are referring to #8559, that only covers one half of this issue, and it says "Another PR will implement the same fix for Expr.Data." So maybe this should be left open until that second PR lands.

[Rob23oba]

Note: #8560 also got merged