Soundness bug: hasLooseBVars is not conservative

Stream: lean4

[Mario Carneiro]

The "possible" is because it is arguable whether this should count as a soundness bug given that it produces a panic. Nevertheless, this is causing problems for lean4lean having false theorems.

#guard (Expr.bvar (2^20)).hasLooseBVars == false

Normally you would need gargantuan terms to get this many bvars in an expression, but in this case you can just pass this bvar expression on input and various parts of lean will ignore it because it doesn't "look" like a bvar.

[Mario Carneiro]

Actually it seems to be possible to build terms large enough to hit the bvar limit without running into stack overflows:

def mkProps : Nat → Expr → Expr
  | 0, e => e
  | n+1, e => mkProps n (.forallE `_ (.sort .zero) e .default)

run_elab
  let env ← getEnv
  let decl := .axiomDecl {
    name := `foo
    levelParams := []
    type := mkProps (2^20+1) (.bvar (2^20-1))
    isUnsafe := false
  }
  setEnv <| ← ofExceptKernelException <| env.addDecl {} decl

The usual symptom is an error (kernel) type checker does not support loose bound variables, because I believe when traversing into the body it does not actually reduce the bvar number as it normally would because it thinks the bvar isn't there, meaning that when it eventually gets to actually typechecking it the bvar is still there instead of being replaced by a fvar, so it thinks the term is ill-scoped

[Mario Carneiro]

This one isn't even a panic:

#eval Lean.Expr.liftLooseBVars (.bvar 1) 0 (2^32 + 2)
-- Lean.Expr.bvar 3
#eval Lean.Expr.liftLooseBVars (.bvar 1) 0 (2^64 + 2)
-- Lean.Expr.bvar 1

[Mario Carneiro]

cc: @Leonardo de Moura . There are a lot of missing bounds checks in these functions, and the biggest issue is that they don't even have an error pathway. Should I look for an actual unsoundness, or can they be changed to return an optional result? I might try going ahead with the proof as is (keeping track of their limitations and proving that either they aren't called with too big inputs or that the garbage outputs don't make it too far before an error is raised) but these functions are used to produce trusted terms that are not revisited, so I have a high suspicion that this is real unsoundness

[Henrik Böving]

CC @Markus Himmel / @Paul Reichert are these the same ones that you saw?

[Paul Reichert]

Our fuzzer also found a problem related to the bvar handling, but I think we got sidetracked and haven't finished the analysis yet (and also weren't able to expoit it so far). I need to revisit where we left off to remember more details and try to find the time for it this week.

[Markus Himmel]

We found various segfaults in the kernel triggered by feeding terms with loose bvars to the kernel. Our fuzzer only generates bvars with de bruijn index at most 2^16, so I guess our findings are somewhat orthogonal.

[Mario Carneiro]

I would love to have some of those tests for lean4lean

[Mario Carneiro]

you should definitely test bvars around 2^20, 2^32 and 2^64, these are all interesting crossover points in the code

[Mario Carneiro]

I have figured out how to upgrade this to an actual unsoundness. This repro uses a similar bug, not the one in Expr.data but in Level.data.

import Lean
open Lean

def isProp.{u} : Prop := ∀ (x : Sort u) (y z : x), y = z

theorem isProp_prop : isProp.{0} := fun _ _ _ => rfl
theorem not_isProp_type : ¬isProp.{1} := fun h => nomatch h _ 0 1

theorem isProp_not_invariant : isProp.{0} ≠ isProp.{1} :=
  mt (fun h => cast h isProp_prop) not_isProp_type

def mkLevel : Nat → Level → Level
  | 0, e => e
  | n+1, e => mkLevel n (.max .zero e)

-- #eval (mkLevel (2^24) (.param `u)).hasParam -- false!

#guard_msgs(drop all) in
run_elab
  let l := mkLevel (2^24) (.param `u)
  Lean.addDecl <| .defnDecl {
    name := `magic
    levelParams := []
    type := .sort .zero
    value := .const `isProp [l]
    hints := .opaque
    safety := .safe
  }

run_elab
  Lean.addDecl <| .defnDecl {
    name := `magic_eq
    levelParams := [`u]
    type := mkPropEq (.const `magic []) (.const `isProp [.param `u])
    value := mkApp2 (mkConst ``Eq.refl [levelOne]) (.sort .zero) (.const `magic [])
    hints := .opaque
    safety := .safe
  }

universe u
example : magic = isProp.{u} := magic_eq.{u}

theorem contradiction : False := isProp_not_invariant (magic_eq.{0}.symm.trans magic_eq.{1})

#print axioms contradiction
-- 'contradiction' does not depend on any axioms

[Floris van Doorn]

Just checking: magic and magic_eq themselves do type-check, according to the Kernel? Because otherwise this is just a special case of "you can put type-incorrect theorems into the environment using addDecl", right?

[Mario Carneiro]

that's right, the kernel validates these theorems

[Floris van Doorn]

Oh, good point. I misremembered: the other unsoundness is not with addDecl but with a more lower-level "adapt the environment yourself"

[Mario Carneiro]

the use of addDecl is because the construction involves the level expression max 0 ... 0 u where there are 2^24 0's, and so it is better to not have the elaborator look at it because it takes a long time and sometimes stack overflows

[Edward van de Meent]

that's a lot of zeroes :looking:

[Mario Carneiro]

fixed in lean4#8554

[Mario Carneiro]

Unfortunately, it seems Leo has not accepted the PR, and has instead fixed the issue in a way that can't be proved correct :(

[Martin Dvořák]

For people who review formalization papers, what is the recommended way to check that a presented proof doesn't exploit this bug?

[Mario Carneiro]

the fix is already on the latest stable

[Mario Carneiro]

so the easiest way is to just make sure it's upgraded to the latest version