SAT verifier correctness with bounded certificates

For every Boolean word $w$, membership $w\in SAT$ is equivalent to the existence of a Boolean word $y$ with $|y|\le |w|$ such that the verifier described here accepts $(w,y)$. The existential certificate bound is non-strict and has no multiplicative or additive constant; the verifier itself separately demands exact equality of $|y|$ with the number of distinct variables of the parsed formula. The empty word is included in the assertion. Here $B=\{\mathrm{false},\mathrm{true}\}$, $B^*$ is the set of all finite Boolean lists, including the empty list, and $|w|$ is list length. The language $SAT$ consists of exactly those $w\in B^*$ for which there are a formula $F$ and an assignment $\tau:\mathbb N\to B$ such that $E(F)=w$ and every clause of $F$ is true under $\tau$; strings without such an encoding are excluded. Write $E(F)$ for this Boolean-list encoding of a formula $F$: for each literal $(b,j)$, take $[b]$ followed by the little-endian canonical binary digits of $j$ (the digits of $0$ form the empty list), replace each bit $d$ by $[\mathrm{false},d]$, and append $[\mathrm{true},\mathrm{false}]$; concatenate these literal encodings within each clause and append $[\mathrm{true},\mathrm{true}]$; then concatenate the clause encodings in formula order. In particular $E([])=[]$. 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 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. The supplied body is admitted with sorry; no proof of this assertion is supplied there.