Cook-Levin: SAT is NP-complete

Parse the proposed SAT input. Reject if malformed. Otherwise enumerate distinct variable names by first occurrence, read that many certificate bits and recursively evaluate the formula. There are at most as many variables and nodes as input bits, and even repeated scans and pairwise name comparisons take polynomial time. Accept exactly when evaluation is true. The empty conjunction and true constant need no certificate bits, while an empty clause and false constant never pass. Thus SAT belongs to verifier-defined NP.

Fix the verifier of $L$ and normalize its guarded certificates using the explicit length field. The tableau lemma then gives, for every binary $x$, $x\in L$ iff ${\mathrm{\Phi }}_{M,x}$ is satisfiable. All strings are legitimate source inputs; there is no implicit promise to parse $x$ as a machine or formula. The fixed verifier itself determines any desired rejection of special source encodings.

Output the CNF encoding from F4. Its polynomial construction bound includes the whole input and witness length, and it always returns a well-formed formula. The equivalence in step 1.2 makes this a total many-one reduction to SAT. At length zero the same normalized verifier and enlarged polynomial bound apply; no exceptional input is omitted. Since $L$ was arbitrary, SAT is NP-hard, and step 1.1 proves NP-completeness.