vm check failed

Stream: new members

[Bhavik Mehta]

import data.list.range

def burgerfy (n : ℕ) : string :=
begin
  apply nat.strong_rec_on n,
  intros k h,
  apply "{" ++ string.intercalate "," (list.map _ (list.fin_range k)) ++ "}",
  intro m,
  apply h m.1 m.2,
end

#eval (burgerfy 1)
#eval (burgerfy 2)

The first works and the second fails with the error message "vm check failed: is_closure(o) (possibly due to incorrect axioms, or sorry)" but I'm not using sorry and only using mathlib/core functions, why is this?

[Bhavik Mehta]

Also, this is a def which isn't noncomputable, so I expected it to compute fine

[Mario Carneiro]

There appears to be a bug in the VM implementation of nat.strong_rec_on:

#eval @nat.strong_rec_on (λ _, ℕ) 0 (λ n ih, if h : n - 1 < n then ih _ h + 1 else 0) -- 0
#eval @nat.strong_rec_on (λ _, ℕ) 1 (λ n ih, if h : n - 1 < n then ih _ h + 1 else 0) -- 1
#eval @nat.strong_rec_on (λ _, ℕ) 2 (λ n ih, if h : n - 1 < n then ih _ h + 1 else 0) -- 2
#eval @nat.strong_rec_on (λ _, ℕ) 3 (λ n ih, if h : n - 1 < n then ih _ h + 1 else 0) -- vm check failed: cidx(closure) == 0 (possibly due to incorrect axioms, or sorry

[Bhavik Mehta]

yay I found a vm bug

[Mario Carneiro]

A workaround is to not use strong_rec_on to write wf definitions for the VM

[Mario Carneiro]

def burgerfy : ℕ → string
| n := "{" ++ string.intercalate "," ((list.fin_range n).map (λ ⟨m, h⟩, burgerfy m)) ++ "}"

This generally performs better anyway

[Mario Carneiro]

But this is the first time I have ever seen a VM bug so congrats

[Scott Olson]

Do you know if the VM has a specialized version of nat.strong_rec_on, or does it compile its Lean definition like usual?

[Mario Carneiro]

I think it just compiles the regular definition

[Scott Olson]

I might try shrinking it to find the cause

[Bhavik Mehta]

Oh that's the version I was looking for! I tried using the equation compiler but couldn't satisfy it, so went straight to strong_rec_on in tactic mode

[Mario Carneiro]

universe u
open nat
def strong_rec_on₂ {p : nat → Sort u} (n : nat) (h : ∀ n, (∀ m, m < n → p m) → p n) : p n :=
suffices ∀ n m, m < n → p m, from this (succ n) n (lt_succ_self _),
begin
  intros n, induction n with n ih,
    {intros m h₁, exact absurd h₁ (not_lt_zero _)},
    {intros m h₁,
      apply or.by_cases (lt_or_eq_of_le (le_of_lt_succ h₁)),
        {intros, apply ih, assumption},
        {intros, subst m, apply h _ ih}}
end

#eval @strong_rec_on₂ (λ _, ℕ) 3 (λ n ih, if h : n - 1 < n then ih _ h + 1 else 0) -- vm check failed: cidx(closure) == 0 (possibly due to incorrect axioms, or sorry

still fails

[Bhavik Mehta]

Huh, I'm surprised there's a difference between

import data.list.range

def burgerfy : ℕ → string
| 0 := "nothing burger"
| n := string.intercalate " and " ((list.fin_range n).map (λ ⟨m, h⟩, burgerfy m)) ++ " burger"

and

import data.list.range

def burgerfy : ℕ → string
| 0 := "nothing burger"
| n := string.intercalate " and " ((list.fin_range n).map (λ ⟨m, _⟩, burgerfy m)) ++ " burger"

[Mario Carneiro]

That's because default_dec_tac automatically clears hypotheses with "internal" names (meaning initial underscore)

[Scott Olson]

After picking apart nat.strong_rec_on a bit, I reached a step where I replaced a nat.rec with a pattern match and it seemingly fixed it. I'll try to investigate the difference

[Scott Olson]

Hmm, the pattern matching elaborator generates much more complicated code than a simple nat.rec.

[Mario Carneiro]

def bar (n : ℕ) (ih : ∀ m, m < n → ℕ) : ℕ := if h : n - 1 < n then ih _ h + 1 else 0
def foo : ∀ n m : ℕ, m < n → nat
| 0 := λ m h₁, absurd h₁ (nat.not_lt_zero _)
| (n+1) := λ m h₁, if h : m < n then foo _ _ h else bar n (foo _)

def foo' (n) : ∀ m : ℕ, m < n → nat :=
nat.rec_on n (λ m h₁, absurd h₁ (nat.not_lt_zero _))
  (λ n IH m h₁, if h : m < n then IH _ h else bar n IH)

#eval @foo 3 2 dec_trivial -- 2
#eval @foo' 3 2 dec_trivial -- vm check failed: cidx(closure) == 0 (possibly due to incorrect axioms, or sorry

[Scott Olson]

Nice

[Mario Carneiro]

The VM has special support for definitions using the equation compiler

[Mario Carneiro]

But in any case it's different code so it's not particularly surprising that it doesn't behave the same; there probably isn't too much point in examining the pattern match code to find out why it works

[Scott Olson]

Yeah, I had switched to simplifying the nat.rec code instead, but you came up with something simpler anyway

[Mario Carneiro]

I would be surprised if there was a difference between nat.rec and nat.rec_on here; they both get special support

[Mario Carneiro]

def bar (n : ℕ) (IH : ℕ → ℕ) : ℕ := IH n + 1
def foo (n) : ℕ → ℕ := nat.rec_on n (λ m, 0) (λ n IH m, bar n IH)
def foo' (n) : ℕ → ℕ := nat.rec_on n (λ m, 0) (λ n IH m, IH n + 1)

#eval @foo 3 2 -- vm check failed: cidx(closure) == 0 (possibly due to incorrect axioms, or sorry
#eval @foo' 3 2 -- 3

[Mario Carneiro]

def bar (n : ℕ) (IH : ℕ → ℕ) : ℕ := IH n + 1
set_option trace.compiler.optimize_bytecode true
def foo (n) : ℕ → ℕ := nat.rec_on n (λ m, 0) (λ n IH m, bar n IH)

[compiler.optimize_bytecode]  foo._rec_1 1
0: move 0
1: nat_cases 4
2: scnstr #0
3: ret
4: push 1
5: ginvoke foo._rec_1
6: move 1
7: ginvoke bar
8: drop 1
9: ret
[compiler.optimize_bytecode]  foo 2
0: move 1
1: ginvoke foo._rec_1
2: ret

[Mario Carneiro]

This compilation is a bit odd. As a primer for those who don't know, the main function foo 2 here indicates that foo is a function with two arguments. It calls move 1, pushing argument 1 (I think this is n) on the stack, and then calls foo._rec_1, which is the recursive function that is constructed as part of nat.rec_on. This could normally be a closure, depending on arguments outside the nat.rec_on, but in this case we don't reference any external variables so foo._rec_1 has only one argument, the index. You can think of it as being defined like this:

def func := ℕ → ℕ
meta def foo.rec_1 : ℕ → func | n :=
nat.cases_on n
-- 0: move 0
-- 1: nat_cases 4
( -- 2: scnstr #0
  -- 3: ret
  λ _, 0)
(λ m,
  -- 4: push 1
  -- 5: ginvoke foo._rec_1
  let IH := foo.rec_1 m in
  -- 6: move 1
  -- 7: ginvoke bar
  let x := bar n IH in
  -- 8: drop 1
  -- 9: ret
  λ _, x)

[Mario Carneiro]

The thing that is weird is that there doesn't seem to be any indication of the second lambda; foo.rec_1 is supposed to be producing a function, not a natural number, and I've fudged it in the gloss by adding λ _, in two places

[Mario Carneiro]

an even simpler version:

def bar (n : ℕ) (IH : unit → ℕ) : ℕ := IH () + 1
set_option trace.compiler.optimize_bytecode true
def foo (n) : unit → ℕ := nat.rec_on n (λ _, 0) (λ n IH _, bar n IH)
#eval @foo 3 () -- vm check failed: cidx(closure) == 0 (possibly due to incorrect axioms, or sorry

The +1 only matters, by the way, in order to cause the crash by doing something that requires the result to be a nat

[Scott Olson]

It also fails at @foo 2 () now for what it's worth

[Mario Carneiro]

def bar (IH : unit → ℕ) : ℕ := IH () + 0
set_option trace.compiler.optimize_bytecode true
def foo (n) : unit → ℕ := nat.rec_on n (λ _, 1) (λ n IH _, bar IH)
meta def foo' : ℕ → unit → ℕ | n _ := nat.cases_on n 1 (λ n, bar (foo' n))
#eval @foo 1 () -- vm check failed: cidx(closure) == 0 (possibly due to incorrect axioms, or sorry
#eval @foo' 1 () -- 1

I think this gets to the heart of it. The meta def is very close to the final compiled form, but you will notice that the recursive function after compilation has 2 arguments instead of 1 and is called using closure instead of ginvoke

[Mario Carneiro]

The compiler has some logic in it to eliminate curried functions and remove erased arguments, and I think the bug is there

[Scott Olson]

Do you think it comes from this function? https://github.com/leanprover-community/lean/blob/7b2f3fa452e4bdb38c5d96e64d29205c5986a1a8/src/library/compiler/elim_recursors.cpp#L97-L99

[Scott Olson]

Line 119 makes it look like this deals with the ginvoke/closure distinction you mentioned

[Mario Carneiro]

I think it's happening in an optimization pass. The original expression nat.rec_on n (λ _, 1) (λ n IH _, bar IH) is translated to nat.cases_on n (λ _, 1) (λ n _, bar (self n)) and then it notices that we have a cases followed by a lambda and lifts one over the other to get λ _, nat.cases_on n (1) (λ n, bar (self n)), whereupon we can deduce that the ignored argument can be eliminated. But eliminating this argument changes the type of self n, so bar ends up getting passed a value of type nat instead of unit -> nat

[Mario Carneiro]

The reason it works with 0 in place of 1 in the base case is that 0 plays many roles in the VM; it is the neutral value meaning that all proofs become 0, and in particular application 0 x is defined and equals 0

[Scott Olson]

def bar (n : ℕ) (IH : unit → ℕ) : ℕ := IH () + 1
set_option trace.compiler.elim_recursors true
set_option trace.compiler.reduce_arity true
def foo (n) : unit → ℕ := nat.rec_on n (λ _, 0) (λ n IH _, bar n IH)

[compiler.elim_recursors]
>> foo._rec_1
λ (n : ℕ) (a : unit), n.cases_on (λ (_x : unit), 0) (λ (n : ℕ) (_x : unit), bar n ([foo._rec_1] n)) a
>> foo
λ (n : ℕ) (a : unit), foo._rec_1 n a
[compiler.reduce_arity]
>> foo._rec_1
λ (n : ℕ), nat.cases_on n 0 (λ (n : ℕ), bar n (foo._rec_1 n))
>> foo
λ (n : ℕ) (a : unit), foo._rec_1 n

[Mario Carneiro]

aha, as I suspected

[Scott Olson]

Like you said, after the reduce_arity pass it's not type-correct on bar's argument

[Scott Olson]

My mistake, it's the erase_irrelevant pass

[Scott Olson]

Those traces are actually next to each other so there's no more doubt:

        lean_trace(name({"compiler", "elim_recursors"}), tout() << "\n"; display(procs););
        erase_irrelevant(procs);
        lean_trace(name({"compiler", "erase_irrelevant"}), tout() << "\n"; display(procs););

[Mario Carneiro]

The erase_irrelevant pass still looks okay though

[Mario Carneiro]

[compiler.erase_irrelevant]
>> foo._rec_1
λ (n : ℕ) (a : unit), nat.cases_on n 0 (λ (n : ℕ), bar (foo._rec_1 n))
>> foo
λ (n : ℕ) (a : unit), foo._rec_1 n a

[Mario Carneiro]

It has done the lambda-over-cases transformation, which is not itself harmful

[Mario Carneiro]

notice that foo._rec_1 is still accepting two arguments and passes a partially applied version of itself to bar

[Scott Olson]

Ah! I didn't read carefully enough

[Mario Carneiro]

https://github.com/leanprover-community/lean/blob/7b2f3fa452e4bdb38c5d96e64d29205c5986a1a8/src/library/compiler/reduce_arity.cpp#L48-L53

[Mario Carneiro]

I think this is where the action is

[Mario Carneiro]

In particular it says "we try to eta expand applications" which is the right idea but isn't being implemented right here?