I am learning complexity theory with a background in mathematics, and I want to better understand why certain reductions are polynomial-time computable. Let me give two examples of my worries.
Example 1: The Cook–Levin reduction. In the proof of the Cook–Levin theorem (say in Arora–Barak or Sipser), given a language $L\in\textbf{NP}$ and a polynomial-time verifier $M$ for $L$, we construct a reduction $f\colon x\mapsto\varphi_x$ mapping a string $x\in\{0,1\}^*$ to (an encoding of) a CNF formula that is satisfiable iff $x\in L$. It is then proven that the size of this formula is polynomial in the running time $T(n)$ of $M$. I am comfortable up to this point. But then now many authors claim that this immediately implies that the reduction $f$ is polynomial-time computable. Let me quote three books:
Sanjeev Arora and Boaz Barak, Computational Complexity: A Modern Approach section 2.3.4, page 49:
Moreover, this CNF formula can be computed in time polynomial in the running time of $M$.
Michael Sipser, Introduction to The Theory of Computation 3e, section 7.4, pages 309–310:
To see that we can generate the formula in polynomial time, observe its highly repetitive nature. Each component of the formula is composed of many nearly identical fragments, which differ only at the indices in a simple way. Therefore, we may easily construct a reduction that produces $\phi$ in polynomial time from the input $w$.
Michael Garey and David Johnson, Computers and Intractability: A Guide to the Theory of NP-completeness, section 2.6, page 44:
All that remains to be shown is that, for any fixed language $L$, $f_L(x)$ can be constructed from $x$ in time bounded by a polynomial function of $n=|x|$. … The polynomial boundedness of this computation will follow immediately once we show that $\text{Length}[f_L(x)]$ is bounded above by a polynomial function of $n$, where $\text{Length}[I]$ reflects the length of a string encoding the instance $I$ under a reasonable encoding scheme, as discussed in Section 2.1.
On an intuitive level, it feels right, and I am almost willing to accept such arguments. But nonetheless I feel uneasy about it, since we are arguing at a very high-level, with no discussion of the details of a TM that computes $f$.
Example 2: The halting problem is $\textbf{NP}$-hard. We may argue that the halting problem $\textsf{HALT}$ is $\textbf{NP}$-hard by reducing from $L\in\textbf{NP}$ as follows: since $\textbf{NP}\subset\textbf{EXP}$, there exists an exponential-time TM $M$ deciding $L$ (doing so by brute-force searching for a certificate); we may modify $M$ to enter an infinite loop if it rejects a string $x\in\{0,1\}^*$. This then gives us a reduction $x\mapsto\langle\llcorner M\lrcorner,x\rangle$ such that $x\in L$ iff $\langle \llcorner M\lrcorner,x\rangle\in\textsf{HALT}$, and intuitively this reduction is polynomial-time computable because “the modification of $M$ is quite minor”, whatever that means.
Summary. How do I be more comfortable with high-level arguments concerning whether certain functions are polynomial-time computable? Are there authors that write with careful attention to such details, or should I just learn to stop worrying about it? (This MathOverflow post may be relevant: https://mathoverflow.net/q/76558/)
Thank you.