Actual polynomial-time SAT verification

The Boolean verifier described here satisfies $C(R)$ for $R$ equal to that verifier. Thus one existential machine and one natural-coefficient polynomial compute its output for every tagged pair $(w,y)$ in a time bounded by that polynomial at $|w|+|y|$, including parse failures and incorrect certificate lengths, without imposing a promise on the inputs. Here $B=\{\mathrm{false},\mathrm{true}\}$, $B^*$ is the set of all finite Boolean lists, including the empty list, and $|w|$ is list length. Write $C(R)$ for existence of such a machine and a polynomial $p\in\mathbb N[X]$ that, for all $w,y\in B^*$, compute $[R(w,y)]$ in at most $p(|w|+|y|)$ steps from the list obtained by tagging every bit of $w$ with the left injection into $B\sqcup B$, tagging every bit of $y$ with the right injection, and concatenating those two lists. A machine in these assertions is a Mathlib TM2 stack machine with finitely many stack indices, instruction labels, and control states, a finite input-stack alphabet, designated input and output stacks, a program, and initial label and control state; its other stack alphabets need not be finite. Input and output alphabet bijections transport the specified encoded lists to the corresponding stack alphabets. Computation starts with only the input stack populated, and reaches a halted configuration with the specified output on the output stack, all other stacks empty, and the control state reset to its initial value. Time counts executions of whole TM2 statements, each of which may contain several stack operations. The parser $\operatorname{parse}(w)$ works as follows. Its outer recursion starts with fuel $|w|+1$, returns the empty formula on an empty remainder even at fuel zero, and otherwise fails at fuel zero; with positive fuel it parses one clause from the current nonempty remainder using clause fuel equal to that remainder’s length plus one, then recurses on the returned suffix with outer fuel reduced by one. Clause parsing fails at fuel zero; with positive fuel it consumes $[\mathrm{true},\mathrm{true}]$ as the end of an empty remaining clause, or parses one literal and recurses on its suffix with clause fuel reduced by one. Literal parsing requires an initial pair $[\mathrm{false},b]$ for the sign. On the remainder $r$ it starts data fuel $|r|+1$: zero data fuel fails; with positive data fuel $[\mathrm{true},\mathrm{false}]$ ends the digit sequence, while $[\mathrm{false},d]$ contributes digit $d$ and decreases fuel by one; all other cases fail. The collected digits are interpreted little-endian and accepted only if they equal the canonical binary digits of the resulting natural number. A parsed literal is that sign/index pair together with the suffix after its delimiter; any failed subparse makes the containing parse fail. Success of the outer parse requires consuming the complete input. The variable list $V(F)$ is obtained by reading the indices of all literals in the flattened clause list in order and deleting duplicate occurrences while retaining the first occurrence of each index. The Boolean verifier on $(w,y)$ first applies this parser to $w$, returning false on failure. For a parsed formula $F$, it returns false unless $|y|=|V(F)|$; if the lengths agree, it evaluates $F$ under the assignment that gives the $j$th variable in $V(F)$ the $j$th bit of $y$, and gives every unlisted index false. More generally this assignment is formed by zipping $V(F)$ with $y$, looking up an index in that truncated list of pairs, and using false when it is absent. A formula is a finite list of clauses, each clause a finite list of literals $(b,j)\in B\times\mathbb N$. Under an assignment $\tau:\mathbb N\to B$, the literal $(b,j)$ is true exactly when $\tau(j)=b$, a clause is true exactly when some literal in it is true, and a formula is true exactly when every clause is true. Thus an empty clause is false and an empty formula is true. The supplied body is admitted with sorry; no proof of this assertion is supplied there.