feat: prove Level cached-flag correctness

[kim-em]

This PR replaces the Level.hasParam_eq and Level.hasMVar_eq axioms with proofs derived from Level.mkData_eq, and moves them, along with the structural hasParam'/hasMVar' definitions, out of Verify/Axioms.lean into Verify/Level.lean, mirroring what #19 (Prove Expr cached flag correctness) did for the Expr flags. Closes #24 (Prove Level cached-flag correctness).

Please look closely at one part of this, because it goes beyond what the issue asked for and it changes what mkData_eq asserts. As stated, the two equalities are not just unprovable from mkData_eq, they are refutable, and fixing that meant changing the overflow branch of the mkData' model.

The old model was a character-for-character copy of the Lean definition of mkData that preceded the @[extern] one:

def mkData' (h : UInt64) (depth : Nat := 0) (hasMVar hasParam : Bool := false) : Level.Data :=
  if depth > Nat.pow 2 24 - 1 then panic! "universe level depth is too big"
  else ...

That is, it was a copy of the bug: panic! evaluates to default = 0, so the branch drops both flag bits, which is exactly the non-conservativity reported in leanprover/lean4#8554 (fix: soundness bug in {Expr, Level}.data). Level.data for .succ u passes u.data.depth.toNat + 1 and Data.depth reads 24 bits, so a level of cached depth 2 ^ 24 - 1 exists and its successor overflows. Hence Level.succ (succ^[2 ^ 24 - 1] (.param x)) has hasParam = false but hasParam' = true, and mkData_eq together with the old hasParam_eq axiom proves False. I checked that in Lean; the derivation is at the end of this description. The same goes for hasMVar_eq separately.

The kernel as it stands cannot reach that state. Level.mkData is opaque with @[extern "lean_level_mk_data"], and since leanprover/lean4#8559 (fix: block adversarial exploit of non-aborting assert!) the C++ calls lean_internal_panic on an overflowing depth, which prints to a saved stderr handle and calls exit(1). It never returns a Level.Data. leanprover/lean4#8560 (fix: block potential adversarial exploit of non-aborting assert!) did the same for Expr.

So on that branch there is no value to transcribe, and a total Lean model has to invent one. This PR invents the saturating one:

def mkData' (h : UInt64) (depth : Nat := 0) (hasMVar hasParam : Bool := false) : Level.Data :=
  h.toUInt32.toUInt64 +
  hasMVar.toUInt64.shiftLeft 32 +
  hasParam.toUInt64.shiftLeft 33 +
  (min depth (2 ^ 24 - 1)).toUInt64.shiftLeft 40

which keeps the flag bits and makes both equalities hold unconditionally. Two things to be clear about, both now recorded in the mkData' docstring:

• This is a chosen total specification for an opaque constant, not a transcription of the implementation. It agrees with the C++ wherever the C++ returns, so results proved from it transfer for runs that do not abort. It does not model termination, and nothing here says a level that deep is constructible in a running Lean.
• It is emphatically not a claim that the kernel saturates. The kernel aborts, and that is the behaviour this models around, not against. Saturation was proposed for the kernel in #8554 and not merged, but that decision was about what the kernel should do, which is a different question from which total function to assign to a branch where the kernel does nothing. The only requirements on that assignment are that it agree with the kernel wherever the kernel returns, and that it keep the cached fields conservative. Saturation is the natural pick meeting both; panic!/0 fails the second and is why the current axioms are inconsistent.

A consequence is that mkData_hasParam and mkData_hasMVar no longer need their d < 2 ^ 24 hypotheses; they are now projections of a shared mkData_flags, matching Expr.mkData_flags. mkData_depth still needs the hypothesis.

The structural definitions and the downstream API are unchanged, and the axiom footprint matches the Expr precedent:

'Lean.Level.hasParam_eq' depends on axioms: [propext, Classical.choice, Quot.sound,
 Lean.Level.mkData_eq, Lean.Level.mkData_flags._native.bv_decide.ax_1_10]
'Lean.Level.hasMVar_eq' depends on axioms: [propext, Classical.choice, Quot.sound,
 Lean.Level.mkData_eq, Lean.Level.mkData_flags._native.bv_decide.ax_1_10]

Not addressed here: Expr.looseBVarRange_eq is still an axiom carrying the same stale "should now be provable" comment, and it is refutable against the current Expr.mkData' for the same reason. .bvar i with i + 1 > 2 ^ 20 - 1 fails the assert!, so the data is 0 and looseBVarRange = 0 while looseBVarRange' = i + 1. The Expr flags were unaffected, since 0 is conservative for them, which is why #19 went through.

Derivation of `False` from the previous pair of axioms

Checked against the parent commit, 7842f38:

import Lean4Lean.Verify.Level

namespace Lean.Level

def succs : Nat → Level → Level
  | 0, l => l
  | n+1, l => .succ (succs n l)

theorem succs_data (x : Name) : ∀ n, n < 2^24 →
    (succs n (.param x)).data.depth.toNat = n ∧ (succs n (.param x)).data.hasParam = true
  | 0, _ => by
    show (Level.param x).data.depth.toNat = _ ∧ (Level.param x).data.hasParam = _
    simp only [Level.data]
    exact ⟨mkData_depth (by omega), mkData_hasParam (by omega)⟩
  | n+1, h => by
    have ⟨ih1, ih2⟩ := succs_data x n (by omega)
    show (Level.succ (succs n (.param x))).data.depth.toNat = _ ∧
      (Level.succ (succs n (.param x))).data.hasParam = _
    simp only [Level.data, ih1, ih2]
    exact ⟨mkData_depth h, mkData_hasParam h⟩

/-- One `succ` past the representable depth loses the `hasParam` bit. -/
theorem overflow (u : Level) (h : u.data.depth.toNat = 2^24 - 1) :
    (Level.succ u).hasParam = false := by
  show (Level.succ u).data.hasParam = false
  simp only [Level.data, h]
  rw [mkData_eq, mkData', if_pos (Nat.lt_succ_self _)]
  rfl

theorem hasParam'_succ (u : Level) : (Level.succ u).hasParam' = u.hasParam' := rfl

theorem hasParam'_succs (x : Name) : ∀ n, (succs n (.param x)).hasParam' = true
  | 0 => rfl
  | n+1 => hasParam'_succs x n

theorem bad : False := by
  have h := hasParam_eq (.succ (succs (2^24 - 1) (.param `x)))
  rw [overflow _ (succs_data _ _ (by omega)).1] at h
  rw [hasParam'_succ, hasParam'_succs] at h
  exact Bool.noConfusion h

end Lean.Level

🤖 Prepared with Claude Code

[digama0]

Yes I know it's false. This is what leanprover/lean4#8821 is for, maybe you can ask your human master to go poke at the FRO to stop sitting on year old PRs.

[kim-em]

Yes I know it's false. This is what leanprover/lean4#8821 is for, maybe you can ask your human master to go poke at the FRO to stop sitting on year old PRs.

Hi Mario (pure unadulterated human ignorance here, not LLM ignorance on top), what progress can we make in the meantime, without lean4#8821?

Is this progress in the right direction?

Is another reasonable alternative to be change mkData' to be Option valued, to represent the kernel abort as currently implemented?