LSP crash when indexing out of bounds

[sullyj3]

Prerequisites

• [X ] Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

LSP server crash when indexing arrays out of bounds. Note that I'm using regular indexing arr[idx], not the unchecked arr[idx]! version. I believe crashing for unchecked out of bounds indexing is expected behaviour.

The behaviour seems to differ between combinations of array length and index.

Steps to Reproduce

Paste into vscode with lean 4 extension running

def northernTrees : Array String :=
  #["sloe", "birch", "elm", "oak"]

#eval northernTrees[4]

Expected behavior: [What you expect to happen]
no crash

Actual behavior: [What actually happens]
lsp crashes. It also crashes with northernTrees[5], but curiously northernTrees[6] gives a type error without crashing, as expected.

Reproduces how often: [What percentage of the time does it reproduce?]
100% for this particular case.

At first I thought the rule was arr[arr.length] and arr[arr.length+1] cause crashes and other indices don't. However this doesn't generalize to arrays of different lengths, eg with array of one element

def northernTrees : Array String :=
  #["sloe"]

All indices from 1 to 10 inclusive cause the crash consistently (I didn't keep testing with higher indices)

Versions

Lean (version 4.0.0-nightly-2023-05-22, commit 8d4dd23, Release)

Arch linux (rolling release)

Additional Information

N/A

[digama0]

While #eval northernTrees[6] doesn't crash, it also prints something interesting:

$ lean Test.lean
Test.lean:3:6: error: failed to prove index is valid, possible solutions:
  - Use `have`-expressions to prove the index is valid
  - Use `a[i]!` notation instead, runtime check is perfomed, and 'Panic' error message is produced if index is not valid
  - Use `a[i]?` notation instead, result is an `Option` type
  - Use `a[i]'h` notation instead, where `h` is a proof that index is valid
⊢ 6 < Array.size northernTrees
"Agņ"

$ lean Test.lean
Test.lean:3:6: error: failed to prove index is valid, possible solutions:
  - Use `have`-expressions to prove the index is valid
  - Use `a[i]!` notation instead, runtime check is perfomed, and 'Panic' error message is produced if index is not valid
  - Use `a[i]?` notation instead, result is an `Option` type
  - Use `a[i]'h` notation instead, where `h` is a proof that index is valid
⊢ 6 < Array.size northernTrees
"Agœ"

I'm pretty sure this is a buffer overrun, which is why the behavior is nondeterministic, and why it seems to depend on the index: some indexes have something kind of stringish like this one, while others lead to permissions errors.

That said, this is a known issue and expected behavior. Duplicate of #1697. What's happening is that the syntax a[i] looks in the context for a proof of i < a.size, assuming it can't trivially be proved, and if that fails it prints an error message, which is what you can see above. It then puts a sorry into that location in the expression, but then #eval runs (!) and the compiler ignores proof objects, assuming them to be correct for having been typechecked. You can use sorry to cause undefined behavior and this is an example of such. But probably #eval shouldn't be evaluating terms containing sorry.

[david-christiansen]

Perhaps two versions of sorry are in order? If I'm working on a program that requires a proof of something that I'm pretty sure is true, I'd like to be able to test it by using sorry as a placeholder for the rest of the proof. On the other hand, when Lean inserts a sorry on its own, I'd probably prefer that I got a message like Can't #eval expressions with missing proofs. In particular, I couldn't automatically prove that i < a.size..

Alternatively, the existence of a #eval_unsafe that eval'ed terms with sorry would address this concern.

[digama0]

There are actually two versions of sorry:

/--
Auxiliary axiom used to implement `sorry`.

The `sorry` term/tactic expands to `sorryAx _ (synthetic := false)`. This is a
proof of anything, which is intended for stubbing out incomplete parts of a
proof while still having a syntactically correct proof skeleton. Lean will give
a warning whenever a proof uses `sorry`, so you aren't likely to miss it, but
you can double check if a theorem depends on `sorry` by using
`#print axioms my_thm` and looking for `sorryAx` in the axiom list.

The `synthetic` flag is false when written explicitly by the user, but it is
set to `true` when a tactic fails to prove a goal, or if there is a type error
in the expression. A synthetic `sorry` acts like a regular one, except that it
suppresses follow-up errors in order to prevent one error from causing a cascade
of other errors because the desired term was not constructed.
-/
@[extern "lean_sorry", never_extract]
axiom sorryAx (α : Sort u) (synthetic := false) : α

the kind of sorry that is used in this example is the synthetic one, which I agree have an especially good reason to abort #eval without error since the whole point is to prevent a flood of errors caused by earlier errors.

[digama0]

I think that because of the possibility of UB, it would be better to be conservative and not allow either kind of sorry in an #eval. It is easy to accidentally introduce this while editing code and crash the server, or worse, and I would rather it be a teaching moment than a loaded gun. This behavior could be toggled with a flag though, for those cases where you are deliberately stubbing things out. Using axioms instead of sorry would be another way to work around it.

[david-christiansen]

That makes sense to me, so long as the flag is convenient and discoverable.

[mhuisi]

This issue was fixed by #4810.