Is this padded version of the Halting Problem in NP?

Question

I'm using the following definition of $NP$:

$$A \in NP \Longleftrightarrow A(x) = \exists w: B(x,w) $$ where $B \in P$ and $|w| = poly(|x|)$.

Now instead of the problem whether the program $\Pi$ halts on input $x$, I'll use the close cousin that asks whether $\Pi$ halts on $0$. Then I can write:

$$HaltsOnZero(\Pi) = \exists t: HaltsOnZeroInTime(\Pi, t) $$

where $HaltsOnZeroInTime$ is the decidable problem of checking whether $\Pi$ halts on input $0$ after $t$ steps. Comparing this with the definition of $NP$ $HaltsOnZeroInTime$ is already in $P$ as long as $t$ is encoded in unary. After all running $\Pi$ for $t$ steps takes only about $t$ steps, so this is a linear algorithm.
The only issue is that $t$ isn't in $poly(|\Pi|)$ because programs of size $|\Pi|$ when given $0$ as input run for $BusyBeaver(|\Pi|)$ time, which isn't even computable, much less polynomial. But now suppose we insist that $\Pi$ is padded until it reaches length $BusyBeaver(|\Pi|)$ and call that new input $\Pi'$. Then $t$ would be polynomial (in fact linear) in the size of $\Pi'$ and $HaltsOnZero(\Pi')$ would be in $NP$.
At this point there's of course a voice inside me shouting that this is all nonsense because $BusyBeaver$ isn't computable. Well I certainly haven't reduced the classical formulation of the Halting Problem to a problem in $NP$ because I had an uncomputable step in the reduction. But it seems to me like I've still defined a problem in $NP$ with the strange property that just writing down a problem instance requires uncomputable superpowers.
Is this really a bona fide $NP$-problem or am I making a subtle mistake somewhere?

Answer 1

Unless you're talking about promise problems, you are required to handle arbitrary inputs.

Given a string $x\in\left\{0,1\right\}^*$, we have $x\in L$ iff $x=\langle M\rangle \cdot BB\left(|M|\right)$ and $M$ halts for some fixed input ($\cdot$ denotes concatenation).

This means that even before talking about the witness (which is indeed linear), you must verify that $x$ has this specific form (unlike in promise problems, where you only care about specific inputs), and this is undecidable.

Note that this only shows why your justification to why this problem is in NP does not work. However, this language is obviously undecidable, since otherwise you could compute $BB(x)$, and thus lies outside of NP.