$TSAT$ is $NP$-complete In "Computational Complexity" by Arora and Barak they state that the following is $NP$-complete:

$\{ \langle \alpha, x, 1^n , 1^t \rangle : \exists u \in \{0,1\}^n \text{ s.t. } M_{\alpha} \text{ outputs } 1 \text{ on input } \langle x,u \rangle, \text{ within } t \text{ steps} \}$.

They call this language $TSAT$. 

I am trying to check the "complete" part of the claim.

Suppose $L \in NP.$ By definition, there is a polynomial $p$ and poly-time TM $M$ such that $\forall x \in \{0,1\}^*,$ we have $$x \in L \iff \exists u \in \{0,1\}^{p(|x|)} \text{ such that } M(x,u)=1.$$ 
Let $t()$ be the polynomial in which $M$ runs, and let $\alpha$ be the TM $M$ represented as a binary string. Then I think this mapping reduction $f$ works: $$f(x) = \langle \alpha, x, 1^{p(|x|)}, 1^{t(|x|)} \rangle.$$

My two questions are:

1) Is this correct?

2) If it's correct, how do we know that $f$ is computable? Just because some verifier $M$ exists, how do we guarantee that $f$ can "compute" it? Or is $M$ "hardcoded" in the Turing machine that is used to compute $f(x)$ from $x$?
It's not correct. As you said, you cannot prove $f$ is polynomial-time computable.

However, you can reduce from a particular NP-complete language, for example, 3SAT. Now $f$ is polynomial-time computable as you can easily write a verifier for 3SAT.