trepplein accepts input with malformed universe variable

[dwrensha]

Consider the following input (found by running AFL on a minimal testing harness):

9 #NS 0 u
2 #NS 0 eq
3 #NS 0 alpha
1 #UP 1
0 #ES 1
4 #NS 0 a
1 #EV 0
5 #NS 0 alpt
2 #EV 1
3 #ES 0
4 #EP #BD 5 2 3
5 #EP #BD 4 1 4
6 #EP #BI 3 0 5
6 #NS 2 refl
7 #EC 2 1
8 #EA 7 2
9 #EA 8 1
10 #EA 9 1
11 #EP #BD 4 1 10
12 #EP #BI 3 0 11
#IND 2 2 6 1 6 12 1

leanchecker rejects this with the output:

line 4: _Map_base::at

but trepplein accepts it with the output:

-- successfully checked 3 declarations

On zulip, @digama0 annotated the input like this

9 #NS 0 u = `u
2 #NS 0 eq = `eq
3 #NS 0 alpha = `alpha
1 #UP 1 = u1 (???)
0 #ES 1 = Sort u1
4 #NS 0 a = `a
1 #EV 0 = #0
5 #NS 0 alpt = `alpt
2 #EV 1 = #1
3 #ES 0 = Sort 0
4 #EP #BD 5 2 3 = Π (alpt : #1), Sort 0
5 #EP #BD 4 1 4 = Π (a : #0) (alpt : #0), Sort 0
6 #EP #BI 3 0 5 = Π {alpha : Sort u1} (a : alpha) (alpt : alpha), Sort 0
6 #NS 2 refl = `refl
7 #EC 2 1 = eq.{u1}
8 #EA 7 2 = eq.{u1} #1
9 #EA 8 1 = eq.{u1} #1 #0
10 #EA 9 1 = eq.{u1} #1 #0 #0
11 #EP #BD 4 1 10 = Π (a : #0), eq.{u1} #0 a a
12 #EP #BI 3 0 11 = Π {alpha : Sort u1} (a : alpha), eq.{u1} alpha a a
#IND 2 2 6 1 6 12 1 =
  inductive {u1} eq {alpha : Sort u1} (a : alpha) : Π (alpt : alpha), Sort 0
  | refl : Π {alpha : Sort u1} (a : alpha), eq.{u1} alpha a a

The problem is on line 4, which constructs a universe parameter referencing a non-existent name.

In my current understanding, it seems pretty clear that this is a bug in trepplein -- it ought to be rejecting this input, because it uses a malformed universe variable.