Programming multi-stack machines

ClassFlag bit of a machine state#✓fully proved

A flag on a type \(\sigma\) of machine states consists of a map \(\mathrm{tag} : \mathrm{Bool} \to \sigma\) that stores a bit in a state and a map \(\mathrm{untag} : \sigma \to \mathrm{Bool}\) that reads it back, such that \(\mathrm{untag}(\mathrm{tag}(\beta)) = \beta\) for every bit \(\beta\). The program primitives use it to branch on whether a pop found a symbol.

class Flag (σ : Type) where
  /-- Store a bit in the state. -/
  tag : Bool → σ
  /-- Read the stored bit back. -/
  untag : σ → Bool
  /-- Reading back what was stored. -/
  untag_tag : ∀ b, untag (tag b) = b

Used by 198

Used byProgram of the reversal component · Running the reversal component · Program of the checking machine · Program of the layout machine · The checking run · The layout run · List canonicalizer normalizes one element · Program of the list-of-naturals canonicalizer · List canonicalizer runs in linear time on decodable input · Program of the payload normalizer machine · Linear step bound for the payload normalizer machine · Pair-list projector emits one weight and one value frame per item · Program of the pair-list projector · Pair-list projector fails on malformed input in linear time · Pair-list projector yields canonical weight and value lists · Bit-block copy keeps the order and restores source and scratch · One frame adds one unary count bit · Program of the frame counter for lists of naturals · Number normalizer restores its work stacks and prepends its answer · Program of the raw pair-frame splitter · Pair-frame splitter extracts both raw fields · Program of the unary-to-binary converter · Converter turns a unary count into a canonical binary frame · Converter turns a unary count into a raw canonical binary payload · One clause of the accept generator · Literal routine of the accept generator · Run of the literal routine of the accept generator · Run of the accept generator's precomputation · Generator machine for the accept family · Loop body of the cell-shift generator · One clause of the cell-shift generator · Correctness of the shift generator on one block · Literal routine of the cell-shift generator · One literal routine of the cell-shift generator · One iteration of the overflow loop of the cell-shift generator · The cell-shift generator · The decrement chain takes \(n\) steps · One iteration of the in-range loop of the cell-shift generator · Correctness of the shift generator, with its explicit time bound · Block stages of the cell-shift generator · One iteration of the time loop of the shift generator · One phase-loop iteration of the initial-row generator · Run of one clause (initial-row generator) · The I3 loop · Counter part of one I3 iteration · The literal routine of the initial-row generator · Run of one literal routine (initial-row generator) · Run of the precomputation (initial-row generator) · The counter part of the initial-row generator · Run of the transition-family generator on one clause · Correctness of the clause-family generator, with its explicit time bound · Literal routine of the transition-clause generator · Run of one literal routine (transition-clause generator) · Generator machine for the transition clause families · One iteration of the time loop · The drain · The drain program · Running a program, then the drain · The composed program · Draining a stack with the transfer loop · Generator run for one cell · One clause of the one-hot generator · One stack iteration of the one-hot generator · One-hot generator: the routine for one literal · Run of one literal routine (one-hot generator) · Correctness of the one-hot generator, with its explicit time bound · The one-hot generator · Generator run over one time step · Gap emission in the counter view · The multiplication routine of a counter machine · A runtime for loop in the counter view · The counter program · The counter program's run · One Horner round · The statements of one Horner round · The power loop · Power-loop program · Multi-target transfer · The lookup program · The return loop of the lookup machine · Serving a live table entry · One scan step of the lookup · Restoring and stashing after a comparison in the lookup machine · Program of the SAT verifier host · Cleanup of the SAT host · The tokenizer embeds in the SAT verifier host · Phase 0 of the SAT verifier host · The 3-COLOR emitter machine · The 3-COLOR emitter clears its OR-output counter · Name comparison in the 3-COLOR emitter · Moving \(U\) onto \(E\) · Copying a counter through \(W\) · Moving an earlier name from \(D\) to \(E\) · Moving an earlier literal vertex from \(D\) to \(U\) · Moving the current name from \(T\) to \(A\) · Skipping an earlier literal vertex · The 3-COLOR emitter processes one clause · The emitter processes the remaining literals of a clause · Recording the current occurrence · The 3-COLOR verifier machine · Restoring the color stack in the 3-COLOR verifier · Correctness and time bound of the 3-coloring verifier machine · Program of the clique verifier · One row of the clique verifier's walk · Moving a walked name from \(D\) to \(E\) · CLIQUE emitter: reading a variable name · The CLIQUE emitter machine · Clique emitter: comparing two names · Clique emitter: the instance prefix · CLIQUE emitter: putting the current occurrence on the walked stack · The KG-map machine · Number output of the clique reduction machine · Membership transducer embeds the doubling machine · Padding machine embeds the summation machine · Membership transducer embeds the summation machine · Program of the PARTITION doubling machine · Program of the raw-input SUBSET-SUM to PARTITION machine · Program of the SUBSET-SUM to PARTITION padding machine · Program of the raw-input PARTITION membership machine · Program of the canonical PARTITION membership transducer · Linear step bound for the PARTITION doubling machine · Quadratic run of the raw-input SUBSET-SUM to PARTITION machine · Quadratic run of the padding machine on canonical instances · Raw-input PARTITION membership machine runs in quadratic time · Canonical PARTITION membership transducer runs in quadratic time · Edge-number phase (SUBSET-SUM reduction machine) · The subset-sum emitter machine · Subset-sum emitter: one vertex number · Run of the pair-counting loop of the subset-sum emitter · Run of the subset-sum emitter's pair walk · Binary conversion (SUBSET-SUM reduction machine) · Run of the VERTEX-COVER to SUBSET-SUM machine · Moving the new sum back · Comparing the sum with the target · Moving the final sum for the comparison · The SUBSET-SUM verifier program · Binary addition program built on the SUBSET-SUM machine · Binary addition of framed numbers in quadratic time · SUBSET-SUM verifier computes the mask-selected sum · HAMPATH emitter, phase A: searching the variable stack for a name · Comparing a name with the top entry of the variable stack · Copying a counter in the HAMPATH emitter · The HAMPATH emitter machine · HAMPATH emitter, phase A: one literal · One literal of the detour walk · Draining a counter · The row loop of a diamond in the HAMPATH emitter · End of a diamond · The output phase of the HAMPATH emitter · Run of a HAMPATH-verifier counter comparison · HAMPATH-verifier unary comparison with the counter restored · Moving a stack of bits · The Hamiltonian path verifier machine · The rest of a vertex step in the Hamiltonian-path verifier · Fresh-literal subroutine of the 3SAT emitter · The SAT-to-3SAT emitter machine · The SAT-to-3SAT emitter writes the encoded translation in quadratic time · The edge loop of a pass · The pass loop of the marking machine · The marking machine for PATH · Restoring the parked marks · Walking to a vertex and setting its mark · Adding two counters into a third · Cleanup empties its stacks · Cleanup round · Bit-block comparison statement · Deciding step of the comparison · Comparison pops a common prefix · Correctness of the bit-block comparison · The comparison loop · Non-destructive comparison of two counters · One round of counter comparison · Copying a counter through a scratch stack · Decrement · Gap emission · Loop head of a for loop over a counter · Time bound for a for loop over a counter · A for loop over a counter reaches its exit · Exact running time of a for loop over a counter · Bit-moving loop · Restoring a stack after a comparison · Running the bit-moving loop · Multiplying unary counters · Popping a list of stacks · Counter transfer loop · Draining a counter while prepending a block · Running a counter transfer · Cleanup in a host · Moving a bit block through a buffer · Reduction host program · Verifier host program · The tape update · The clocked loop · Writing the output · Reading the input · The clocked universal program · One simulated step, halting case · One simulated step, running case

TheoremA halted run stays halted#✓fully proved

Let \(f : \sigma \to \mathrm{Option}\,\sigma\) be a partial step function and let \(\hat f\) be its lift to \(\mathrm{Option}\,\sigma\), which sends \(\mathrm{none}\) to \(\mathrm{none}\) and \(\mathrm{some}\,x\) to \(f(x)\). Then \(\hat f^{\,n}(\mathrm{none}) = \mathrm{none}\) for every \(n \in \mathbb{N}\).

theorem iter_none {σ : Type} (f : σ → Option σ) (n : ℕ) : (flip bind f)^[n] none = none

Used by 11

Used byQuadratic overhead of the single-tape emulation · Polynomial-time machines have polynomially bounded output · Converter turns a unary count into a canonical binary frame · Converter turns a unary count into a raw canonical binary payload · The TM2 SAT verifier · Binary addition of framed numbers in quadratic time · The composite machine computes the composite function in time · Simulation transports runs · Run embedding · Exact program matching transports a run with its step count · Stack lengths grow by at most the push bound per step

DefinitionExact-length runs of a TM2 machine#✓fully proved

Let \(M\) be a TM2 machine, given by a statement for each label, and let \(c\) and \(d\) be configurations. For \(n \in \mathbb{N}\), \(M\) runs from \(c\) to \(d\) in exactly \(n\) steps when applying the step function of \(M\) \(n\) times, starting at \(c\), is defined at every step (no configuration before the last one has halted) and ends at \(d\).

def Run (n : ℕ) (c d : TM2.Cfg Γ Λ σ) : Prop :=
  (flip bind (TM2.step M))^[n] (some c) = some d

Used by 377

Used byRunning the reversal component · Mapping the first component of a pair is polynomial-time · The checking run · The layout run · The readout run · List canonicalizer normalizes a sequence of framed payloads · List canonicalizer normalizes one element · List canonicalizer reaches the decoding outcome with canonical output · List canonicalizer fails on malformed input · List canonicalizer runs in linear time on decodable input · Read phase of the payload normalizer consumes each bit once · Linear step bound for the payload normalizer machine · Pair-list projector main loop emits both lists in reverse · Pair-list projector emits one weight and one value frame per item · Pair-list projector always terminates at the decoding outcome · Pair-list projector fails on malformed input in linear time · Pair-list projector yields canonical weight and value lists · Bit-block copy keeps the order and restores source and scratch · Two-destination bit transfer takes one step per bit plus one · Frame counter yields the number of raw frames in unary · One frame adds one unary count bit · Frame counter decides decodability and counts length in unary · Frame counter fails on malformed list framing · Frame emitter takes one step per payload bit plus one · Polynomial-time decoder of the canonical bit-list encoding · Polynomial-time encoder to the canonical bit-list encoding · Run of the pair-to-canonical converter · Runs of the converter to the canonical pair encoding · Runs of the bit-list decoder · Runs of the bit-list encoder · Four-output decoder fails on malformed input · Four-output decoder emits four canonical outputs on success · Full run of the pair-encoding converter · Runs of the pair-encoding converter · Number normalizer restores its work stacks and prepends its answer · Number-pair projector reaches the decoding outcome · Number-pair projector normalizes both fields of a raw pair frame · Pair-frame splitter extracts both raw fields · Pair-frame splitter projects every well-framed input in linear time · Reading a complete framed block · Framed block reader fails on truncated framing · Converter turns a unary count into a canonical binary frame · Converter turns a unary count into a raw canonical binary payload · Correctness of the accept generator, with its explicit time bound · Polynomial time bound of the accept generator · Run of the accept cell chain · One clause of the accept generator · Run of the code-clause chain of the accept generator · Run of the literal routine of the accept generator · Run of the accept generator's precomputation · One clause of the cell-shift generator · Correctness of the shift generator on one block · Correctness of the shift generator on the situation chain · Correctness of the shift generator on the stack chain of a situation · One literal routine of the cell-shift generator · The literal routines of one clause of the cell-shift generator · One iteration of the overflow loop of the cell-shift generator · The pushed-fill chain of the cell-shift generator · The decrement chain takes \(n\) steps · One iteration of the in-range loop of the cell-shift generator · Correctness of the shift generator, with its explicit time bound · Polynomial time bound for the shift generator · One iteration of the time loop of the shift generator · The in-range chain of the cell-shift generator · One phase-loop iteration of the initial-row generator · Run of one clause (initial-row generator) · The I3 loop · Counter part of one I3 iteration · Correctness of the init generator, with its explicit time bound · Polynomial time bound for the init generator · Run of one literal routine (initial-row generator) · Run of the literal routines of a clause (initial-row generator) · One phase loop · Run of the precomputation (initial-row generator) · The read chain · Run lifting · Run of the transition-family generator on one clause · Correctness of the clause-family generator · Correctness of the clause-family generator, with its explicit time bound · Polynomial time bound for the clause-family generator · Run of one literal routine (transition-clause generator) · Run of the literal routines of a clause (transition-clause generator) · One iteration of the time loop · The drain · One polynomial bounds the reduction machine · The reduction machine halts with the emitted formula · Running a program, then the drain · A bounded halting run certifies the output · Draining a stack with the transfer loop · Generator run for one cell · One clause of the one-hot generator · One stack iteration of the one-hot generator · Run of one literal routine (one-hot generator) · Run of the literal routines of a clause (one-hot generator) · Correctness of the one-hot generator, with its explicit time bound · Polynomial time bound for the one-hot generator · Generator run over one row of at-most-one clauses · Generator run over the first rows and the at-least-one clause · Generator run over one time step · Gap emission in the counter view · Sequencing · The counter program's run · The composed machine, raw input to formula · Polynomial time bound of the composed machine · One Horner round · Horner rounds · The power loop · The precomputation · The read loop's run · Multi-target transfer · The dense-to-binary translation on raw bits is polynomial-time · Draining the work stacks of the dense-SAT verifier · The converter's final phase · Running the generic copy loop of the dense-SAT verifier · Moving the input onto the stash · Splitting the verifier input · Exact runs of the dense-to-binary converter · The verifier's main scan · Polynomial-time verifier for dense CNF-SAT · Clause loop of the clause check · Literal loop of the clause check · The return loop of the lookup machine · Serving a live table entry · One scan step of the lookup · Initialization step of the lookup machine · One step to rejection · Correctness of the SAT-verifier lookup machine · The scan loop of the lookup machine · Restoring and stashing after a comparison in the lookup machine · Reading a unary count · Tokenizer run on one clause · Tokenizer rejects undecodable clauses · Tokenizer run on all clauses · The tokenizer accepts when the formula stack is empty · Tokenizer rejects an undecodable literal · Tokenizer run on one literal · Tokenizer rejects undecodable literals · Reading the literals of a clause · Rejecting an unterminated name block · Reading a name block · Reading a polarity · Rejecting run · Accepting run of the SAT tokenizer · An unterminated unary count is rejected · Cleanup phase of the SAT verifier host · Phase 0 of the SAT verifier host · The TM2 SAT verifier · Running a sequence of copy sites of the 3-COLOR emitter · The 3-COLOR emitter clears its OR-output counter · Name comparison in the 3-COLOR emitter · Moving \(U\) onto \(E\) · Copying a counter through \(W\) · Adding the vertex counter to the OR output · Moving an earlier name from \(D\) to \(E\) · Moving an earlier literal vertex from \(D\) to \(U\) · Moving the current name from \(T\) to \(A\) · Running a copy site of the 3-COLOR emitter · Skipping an earlier literal vertex · 3-COLOR emitter: moving the walk side back · The 3-COLOR emitter processes one clause · One step of the walk over earlier occurrences · The emitter on a list of clauses · The emitter processes the remaining literals of a clause · Emitting one literal occurrence · Recording the current occurrence · Walking the earlier occurrences · Correctness and step bound of the 3-COLOR emitter · One step of the 3-COLOR verifier · Restoring the color stack in the 3-COLOR verifier · Correctness and running time of the edge loop · Run of the load phase of the 3-COLOR verifier · The unary reader rejects an unterminated number · The unary reader on a terminated number · Correctness and time bound of the 3-coloring verifier machine · The joint walk of the 3-COLOR verifier decides one edge · The walk towards the farther endpoint decides the edge · 3-COLOR is in NP · Run of the load phase · Reading an unterminated unary number rejects · The clique verifier's unary reader succeeds · One row of the clique verifier's walk · All rows of the clique verifier's walk · The verifier machine for clique, independent set and vertex cover · One step of a clique-verifier program to a known label · Walking the pairs of one row of the clique verifier · Moving a walked name from \(D\) to \(E\) · CLIQUE emitter: reading a variable name · Clique emitter: moving the walk side back · Clique emitter: one clause · Clique emitter: comparing two names · Clique emitter: the instance prefix · Emitter run over a formula's clauses · Emitter run over one literal occurrence · Emitter run over a clause's literals · CLIQUE emitter: putting the current occurrence on the walked stack · The CLIQUE emitter computes Karp's instance in cubic time · Walk over the occurrence stack in the CLIQUE emitter · CLIQUE ≤ INDEPENDENT-SET is polynomial-time · INDEPENDENT-SET ≤ VERTEX-COVER is polynomial-time · Moving the pair bits onto stack \(Y\) · Output phase of the KG-map machine · Output loop for the pair bits of the KG-map machine · Unterminated first unary number in the KG-map machine · Reading the first unary number in the KG-map machine · Unterminated second unary number in the KG-map machine · Reading the second unary number in the KG-map machine · Correctness and running time of the KG-map machine · Failed subtraction in the KG-map machine · Subtraction loop of the clique reduction machine · Number output of the clique reduction machine · NP membership from the CLIQUE, INDEPENDENT-SET and VERTEX-COVER verifier · Linear step bound for the PARTITION doubling machine · Quadratic run of the raw-input SUBSET-SUM to PARTITION machine · Quadratic run of the padding machine on canonical instances · Raw-input PARTITION membership machine runs in quadratic time · Canonical PARTITION membership transducer runs in quadratic time · Edge-number phase (SUBSET-SUM reduction machine) · One halving step of the binary conversion (SUBSET-SUM reduction machine) · Subset-sum emitter: moving the pair bits · Subset-sum emitter: one row of the pair walk · Subset-sum emitter: unterminated unary prefix at rdK · Subset-sum emitter: reading the unary k · Subset-sum emitter: unterminated unary prefix at rdN · Subset-sum emitter: reading the unary n · Subset-sum emitter: one vertex number · Subset-sum emitter: moving unmarked vertices back to L · Run of the mark-return loop of the subset-sum emitter · Run of the pair-counting loop of the subset-sum emitter · Run of the vertex-number phase of the subset-sum emitter · Run of the subset-sum emitter's pair walk · Binary conversion (SUBSET-SUM reduction machine) · Run of the VERTEX-COVER to SUBSET-SUM machine · Run of the target-bit loop of the subset-sum emitter · Run of the target-output phase of the subset-sum emitter · The verifier rejects an unterminated chosen block · The verifier rejects a chosen block that ends in false · Adding a canonical chosen block · Moving the new sum back · Comparing the sum with the target · Carry phase of the SUBSET-SUM verifier · Moving the final sum for the comparison · Rejecting in one step · The verifier rejects an unterminated skipped block · Skipping a number block · The verifier rejects an unterminated target block · Reading the target block · The VERTEX-COVER to SUBSET-SUM reduction is polynomial-time · The summing loop of the SUBSET-SUM verifier · The SUBSET-SUM verifier machine · Binary addition of framed numbers in quadratic time · SUBSET-SUM is in NP · SUBSET-SUM verifier computes the mask-selected sum · HAMPATH emitter, phase A: moving the walk stack back onto the variable stack · HAMPATH emitter, phase A: copying a reversed name onto two stacks · HAMPATH emitter, phase A: searching the variable stack for a name · Running a chain of copy sites in the HAMPATH emitter · Comparing a name with the top entry of the variable stack · Copying a counter in the HAMPATH emitter · Run of a HAMPATH copy site · HAMPATH emitter, phase A: one clause · HAMPATH emitter, phase A: the clauses of a formula · HAMPATH emitter, phase A: one literal · HAMPATH emitter, phase A: the literals of a clause · One clause of the detour walk · Front of a diamond · One literal of the detour walk · The literals of a clause in the detour walk · Draining a counter · The row loop of a diamond in the HAMPATH emitter · The detour walk of a diamond in the HAMPATH emitter · Phase A of the HAMPATH emitter · Moving the tokens back in the HAMPATH emitter · End of a diamond · The detours of a diamond · One diamond · The diamonds · The row of a diamond in the HAMPATH emitter · The output phase of the HAMPATH emitter · Correctness and running time of the HAMPATH emitter · Run of the HAMPATH verifier's unary comparison loop · Run of a HAMPATH-verifier counter comparison · HAMPATH-verifier unary comparison with the counter restored · One step of the emptiness test · Moving a stack of bits · The unary reader of the Hamiltonian path verifier rejects an unterminated number · The unary reader of the Hamiltonian path verifier reads a terminated number · The edge scan of the Hamiltonian path verifier · The unary mover of the Hamiltonian path verifier rejects an unterminated number · The unary mover of the Hamiltonian path verifier moves a terminated number · A single step of the Hamiltonian-path verifier · The edge-list check of the Hamiltonian-path verifier · The witness check of the Hamiltonian-path verifier · HAMPATH is in NP · Running the head-or-edge check · Running the vertex loop · The repeat scan of the Hamiltonian path verifier · Correctness and running time of the Hamiltonian path verifier · One vertex step of the Hamiltonian-path verifier · The rest of a vertex step in the Hamiltonian-path verifier · The return phase ends on an empty side stack · The 3SAT filter's return phase moves the side stack back · One step of the 3SAT filter's return phase · A clause with more than three literals makes the capped 3SAT filter fail · The 3SAT filter walks one clause within the cap · The 3SAT emitter processes one clause · A long clause makes the capped 3SAT filter fail on a list of clauses · The 3SAT filter walks a list of clauses within the cap · Name copy loop of the 3SAT emitter · The 3SAT emitter processes a whole formula · Fresh-literal subroutine of the 3SAT emitter · The 3SAT emitter reads a literal marker · Emitter reductions out of SAT are polynomial-time · One literal of the emitter · The capped filter fails on a clause with too many literals · The filter walks a clause's literals within the cap · The literals of a clause in the emitter · Copying a renamed name · The SAT-to-3SAT emitter writes the encoded translation in quadratic time · Correctness of the clause-length filter · Tokenize, then emit · Closing an output clause in the SAT-to-3SAT emitter · Walking over name bits keeps the label · An empty token stack ends the walk · Walking over a literal advances the literal count · A capped walk fails on a literal past the third · One step of the clause-length walk on a token · The edge loop of a pass · The marking algorithm is polynomial-time · The pass loop of the marking machine · Reading a cut-off unary number · Reading a unary number · Reading the mark of a vertex · Restoring the parked marks · Running time and output of the marking machine · Walking to a vertex and setting its mark · Validation phase of the PATH marking machine · Walking along the marks of the PATH marking machine · Adding two counters into a third · Budgeted run · Cleanup empties its stacks · Deciding step of the comparison · Comparison pops a common prefix · Correctness of the bit-block comparison · The comparison loop · Non-destructive comparison of two counters · Copying a counter through a scratch stack · Gap emission · Time bound for a for loop over a counter · A for loop over a counter reaches its exit · Exact running time of a for loop over a counter · Restoring a stack after a comparison · Running the bit-moving loop · Multiplying unary counters · Reachability for a TM2 machine · Run embedding · Exact program matching transports a run with its step count · Exact run transport to supplied host final stacks · Runs within a step budget · Run embedding for bounded runs · Exact matching transports a bounded run · A single step executes the statement at the current label · Running a counter transfer · Moving a bit block through a buffer · Reduction host · The reduction host's run on one input · Stack lengths grow by at most the push bound per step · Verifier host · The verifier host's run · The tape update · The clocked loop · The clocked universal function is polynomial-time computable · Writing the output · Reading the input · One simulated step, halting case · One simulated step, running case · Writing a timeout · Correctness and running time of the clocked universal machine

TheoremA single step executes the statement at the current label#✓fully proved

Let \(M\) be a TM2 machine, \(l\) a label, \(v\) an internal state, \(S\) an assignment of a list of symbols to each stack, and \(d\) a configuration. If executing the statement \(M(l)\) from state \(v\) and stacks \(S\) yields \(d\), then \(M\) runs in exactly one step from the configuration with label \(l\), state \(v\) and stacks \(S\) to \(d\).

theorem Run.single {l : Λ} {v : σ} {S : ∀ k, List (Γ k)} {d : TM2.Cfg Γ Λ σ}
    (h : TM2.stepAux (M l) v S = d) : Run M 1 ⟨some l, v, S⟩ d

Uses 1 · Used by 211

Statement usesExact-length runs of a TM2 machine

Used byRunning the reversal component · Mapping the first component of a pair is polynomial-time · The checking run · The layout run · List canonicalizer normalizes a sequence of framed payloads · List canonicalizer normalizes one element · List canonicalizer fails on malformed input · Read phase of the payload normalizer consumes each bit once · Pair-list projector main loop emits both lists in reverse · Pair-list projector emits one weight and one value frame per item · Pair-list projector fails on malformed input in linear time · Two-destination bit transfer takes one step per bit plus one · Frame counter yields the number of raw frames in unary · One frame adds one unary count bit · Frame counter fails on malformed list framing · Frame emitter takes one step per payload bit plus one · Polynomial-time decoder of the canonical bit-list encoding · Polynomial-time encoder to the canonical bit-list encoding · Run of the pair-to-canonical converter · Full run of the pair-encoding converter · Reading a complete framed block · Framed block reader fails on truncated framing · Converter turns a unary count into a canonical binary frame · Converter turns a unary count into a raw canonical binary payload · One clause of the accept generator · Run of the literal routine of the accept generator · Run of the accept generator's precomputation · One clause of the cell-shift generator · Correctness of the shift generator on one block · One literal routine of the cell-shift generator · The decrement chain takes \(n\) steps · Correctness of the shift generator, with its explicit time bound · Run of one clause (initial-row generator) · The I3 loop · Counter part of one I3 iteration · Run of one literal routine (initial-row generator) · Run of the precomputation (initial-row generator) · The read chain · Run of the transition-family generator on one clause · Correctness of the clause-family generator, with its explicit time bound · Run of one literal routine (transition-clause generator) · The drain · Running a program, then the drain · Draining a stack with the transfer loop · One clause of the one-hot generator · One stack iteration of the one-hot generator · Run of one literal routine (one-hot generator) · Correctness of the one-hot generator, with its explicit time bound · Sequencing · The counter program's run · One Horner round · The power loop · The precomputation · The read loop's run · The dense-to-binary translation on raw bits is polynomial-time · The converter's final phase · Moving the input onto the stash · Clause loop of the clause check · Literal loop of the clause check · The return loop of the lookup machine · Serving a live table entry · One scan step of the lookup · Initialization step of the lookup machine · One step to rejection · The scan loop of the lookup machine · Reading a unary count · Tokenizer run on one clause · Tokenizer rejects undecodable clauses · Tokenizer run on all clauses · The tokenizer accepts when the formula stack is empty · Tokenizer rejects undecodable literals · Reading the literals of a clause · Rejecting an unterminated name block · Reading a name block · Reading a polarity · An unterminated unary count is rejected · Cleanup phase of the SAT verifier host · Phase 0 of the SAT verifier host · Running a copy site of the 3-COLOR emitter · 3-COLOR emitter: moving the walk side back · The 3-COLOR emitter processes one clause · One step of the walk over earlier occurrences · The emitter processes the remaining literals of a clause · Emitting one literal occurrence · Recording the current occurrence · Walking the earlier occurrences · Correctness and step bound of the 3-COLOR emitter · One step of the 3-COLOR verifier · Correctness and running time of the edge loop · Run of the load phase of the 3-COLOR verifier · The unary reader rejects an unterminated number · The unary reader on a terminated number · The joint walk of the 3-COLOR verifier decides one edge · The walk towards the farther endpoint decides the edge · Run of the load phase · Reading an unterminated unary number rejects · The clique verifier's unary reader succeeds · One step of a clique-verifier program to a known label · Walking the pairs of one row of the clique verifier · Clique emitter: moving the walk side back · Clique emitter: one clause · Clique emitter: comparing two names · Clique emitter: the instance prefix · Emitter run over one literal occurrence · CLIQUE emitter: putting the current occurrence on the walked stack · The CLIQUE emitter computes Karp's instance in cubic time · Walk over the occurrence stack in the CLIQUE emitter · Moving the pair bits onto stack \(Y\) · Output loop for the pair bits of the KG-map machine · Unterminated first unary number in the KG-map machine · Reading the first unary number in the KG-map machine · Unterminated second unary number in the KG-map machine · Reading the second unary number in the KG-map machine · Correctness and running time of the KG-map machine · Failed subtraction in the KG-map machine · Subtraction loop of the clique reduction machine · Number output of the clique reduction machine · Linear step bound for the PARTITION doubling machine · Quadratic run of the raw-input SUBSET-SUM to PARTITION machine · Quadratic run of the padding machine on canonical instances · Raw-input PARTITION membership machine runs in quadratic time · Canonical PARTITION membership transducer runs in quadratic time · Edge-number phase (SUBSET-SUM reduction machine) · One halving step of the binary conversion (SUBSET-SUM reduction machine) · Subset-sum emitter: moving the pair bits · Subset-sum emitter: one row of the pair walk · Subset-sum emitter: unterminated unary prefix at rdK · Subset-sum emitter: reading the unary k · Subset-sum emitter: unterminated unary prefix at rdN · Subset-sum emitter: reading the unary n · Subset-sum emitter: one vertex number · Subset-sum emitter: moving unmarked vertices back to L · Run of the mark-return loop of the subset-sum emitter · Run of the pair-counting loop of the subset-sum emitter · Run of the vertex-number phase of the subset-sum emitter · Run of the subset-sum emitter's pair walk · Binary conversion (SUBSET-SUM reduction machine) · Run of the VERTEX-COVER to SUBSET-SUM machine · Run of the target-bit loop of the subset-sum emitter · Run of the target-output phase of the subset-sum emitter · The verifier rejects an unterminated chosen block · The verifier rejects a chosen block that ends in false · Carry phase of the SUBSET-SUM verifier · Rejecting in one step · The verifier rejects an unterminated skipped block · Skipping a number block · The verifier rejects an unterminated target block · Reading the target block · The summing loop of the SUBSET-SUM verifier · Binary addition of framed numbers in quadratic time · SUBSET-SUM verifier computes the mask-selected sum · HAMPATH emitter, phase A: moving the walk stack back onto the variable stack · HAMPATH emitter, phase A: copying a reversed name onto two stacks · HAMPATH emitter, phase A: searching the variable stack for a name · Run of a HAMPATH copy site · HAMPATH emitter, phase A: one clause · HAMPATH emitter, phase A: one literal · One clause of the detour walk · Front of a diamond · One literal of the detour walk · The row loop of a diamond in the HAMPATH emitter · The detour walk of a diamond in the HAMPATH emitter · Phase A of the HAMPATH emitter · Moving the tokens back in the HAMPATH emitter · End of a diamond · The detours of a diamond · The row of a diamond in the HAMPATH emitter · The output phase of the HAMPATH emitter · The unary reader of the Hamiltonian path verifier rejects an unterminated number · The unary mover of the Hamiltonian path verifier rejects an unterminated number · A single step of the Hamiltonian-path verifier · The rest of a vertex step in the Hamiltonian-path verifier · The return phase ends on an empty side stack · One step of the 3SAT filter's return phase · The 3SAT emitter processes one clause · Name copy loop of the 3SAT emitter · Fresh-literal subroutine of the 3SAT emitter · The 3SAT emitter reads a literal marker · Copying a renamed name · The SAT-to-3SAT emitter writes the encoded translation in quadratic time · Tokenize, then emit · Closing an output clause in the SAT-to-3SAT emitter · An empty token stack ends the walk · One step of the clause-length walk on a token · The edge loop of a pass · The pass loop of the marking machine · Reading a cut-off unary number · Reading a unary number · Reading the mark of a vertex · Running time and output of the marking machine · Walking to a vertex and setting its mark · Validation phase of the PATH marking machine · Walking along the marks of the PATH marking machine · Cleanup empties its stacks · Deciding step of the comparison · The comparison loop · Gap emission · Time bound for a for loop over a counter · A for loop over a counter reaches its exit · Exact running time of a for loop over a counter · Running the bit-moving loop · Running a counter transfer · The reduction host's run on one input · The verifier host's run · The tape update · The clocked loop · Writing the output · Reading the input · One simulated step, halting case · One simulated step, running case · Writing a timeout

AbbreviationUnary counter#✓fully proved

The unary counter with unit symbol \(u\) and value \(n \in \mathbb{N}\) is the list \(u^n\) consisting of exactly \(n\) copies of \(u\).

abbrev cnt {α : Type} (u : α) (n : ℕ) : List α := List.replicate n u

Used by 160

Used byDecoding a list of cells · Cell-by-cell check of a code stack · The cell-by-cell check recognizes code stacks · Decoding inverts the code stack · The diagonal answer read from the encoded output · The diagonal language through the universal machine · Code stacks are recognized · Code stacks, entry by entry · The code stack determines the table lookups · Reading a unary length prefix reads one cell · The checking run · The layout run · Converter turns a unary count into a canonical binary frame · Converter turns a unary count into a raw canonical binary payload · One clause of the accept generator · Run of the literal routine of the accept generator · Run of the accept generator's precomputation · One clause of the cell-shift generator · Correctness of the shift generator on one block · One literal routine of the cell-shift generator · One iteration of the overflow loop of the cell-shift generator · The decrement chain takes \(n\) steps · One iteration of the in-range loop of the cell-shift generator · Correctness of the shift generator, with its explicit time bound · One iteration of the time loop of the shift generator · One phase-loop iteration of the initial-row generator · Run of one clause (initial-row generator) · The I3 loop · Counter part of one I3 iteration · Run of one literal routine (initial-row generator) · Run of the precomputation (initial-row generator) · Run of the transition-family generator on one clause · Correctness of the clause-family generator, with its explicit time bound · Run of one literal routine (transition-clause generator) · One iteration of the time loop · Generator run for one cell · One clause of the one-hot generator · One stack iteration of the one-hot generator · Run of one literal routine (one-hot generator) · Correctness of the one-hot generator, with its explicit time bound · Generator run over one time step · Gap emission in the counter view · Stacks holding given counter values · A runtime for loop in the counter view · The assembled generator, after the precomputation · Sequencing · The counter program's run · Stacks during the read loop · The composed machine, raw input to formula · One Horner round · The power loop · The read loop's run · Multi-target transfer · The 3-COLOR emitter machine · Encoding of an earlier occurrence on stack \(D\) · Moving \(U\) onto \(E\) · Copying a counter through \(W\) · Adding the vertex counter to the OR output · Moving an earlier literal vertex from \(D\) to \(U\) · Running a copy site of the 3-COLOR emitter · Skipping an earlier literal vertex · Stacks of a quiescent state · The 3-COLOR emitter processes one clause · One step of the walk over earlier occurrences · The emitter processes the remaining literals of a clause · The size invariant survives a new literal occurrence · Emitting one literal occurrence · Recording the current occurrence · Walking the earlier occurrences · Correctness and running time of the edge loop · Run of the load phase of the 3-COLOR verifier · The unary reader on a terminated number · Correctness and time bound of the 3-coloring verifier machine · Joint-walk step with both counters nonempty · Joint-walk step when the second endpoint counter runs out first · Joint-walk step when the first endpoint counter runs out first · Walk-on step with a unit on the counter · The joint walk of the 3-COLOR verifier decides one edge · The walk towards the farther endpoint decides the edge · Run of the load phase · The clique verifier's unary reader succeeds · The verifier machine for clique, independent set and vertex cover · Configuration stacks of the CLIQUE emitter · CLIQUE emitter: recognizing a standard state · Clique emitter: the instance prefix · Output phase of the KG-map machine · Reading the first unary number in the KG-map machine · Reading the second unary number in the KG-map machine · Correctness and running time of the KG-map machine · Failed subtraction in the KG-map machine · Subtraction loop of the clique reduction machine · Number output of the clique reduction machine · Edge-number phase (SUBSET-SUM reduction machine) · One halving step of the binary conversion (SUBSET-SUM reduction machine) · Subset-sum emitter: moving the pair bits · Subset-sum emitter: reading the unary k · Subset-sum emitter: reading the unary n · Subset-sum emitter: moving unmarked vertices back to L · Run of the mark-return loop of the subset-sum emitter · Run of the pair-counting loop of the subset-sum emitter · Binary conversion (SUBSET-SUM reduction machine) · Run of the VERTEX-COVER to SUBSET-SUM machine · Copying a counter in the HAMPATH emitter · Run of a HAMPATH copy site · Stacks of a quiescent emitter state · Front of a diamond · Draining a counter · The row loop of a diamond in the HAMPATH emitter · Phase A of the HAMPATH emitter · End of a diamond · The detours of a diamond · The row of a diamond in the HAMPATH emitter · The output phase of the HAMPATH emitter · Run of the HAMPATH verifier's unary comparison loop · Run of a HAMPATH-verifier counter comparison · HAMPATH-verifier unary comparison with the counter restored · The unary reader of the Hamiltonian path verifier reads a terminated number · The edge scan of the Hamiltonian path verifier · Running the head-or-edge check · Stack layout between vertex steps · Running the vertex loop · Stack layout during a vertex step · The repeat scan of the Hamiltonian path verifier · Correctness and running time of the Hamiltonian path verifier · One vertex step of the Hamiltonian-path verifier · The rest of a vertex step in the Hamiltonian-path verifier · Fresh-literal subroutine of the 3SAT emitter · The SAT-to-3SAT emitter writes the encoded translation in quadratic time · Stack contents of the SAT-to-3SAT emitter · The edge loop of a pass · The frame of a read · The pass loop of the marking machine · Reading a cut-off unary number · Reading a unary number · Reading the mark of a vertex · Running time and output of the marking machine · Walking to a vertex and setting its mark · Validation phase of the PATH marking machine · Walking along the marks of the PATH marking machine · Adding two counters into a third · Adding units to target stacks · The comparison loop · Non-destructive comparison of two counters · Copying a counter through a scratch stack · Gap emission · Time bound for a for loop over a counter · A for loop over a counter reaches its exit · Exact running time of a for loop over a counter · Multiplying unary counters · Running a counter transfer · The tape update · The cell of a number · The clocked loop · Writing the output · Reading the input · One simulated step, halting case · One simulated step, running case · The stacks of a simulated configuration · Correctness and running time of the clocked universal machine · The step bound of the clocked universal machine is quadratic

DefinitionCounter increment#✓fully proved

For a stack \(k\), a symbol \(u\) of stack \(k\) (the unit of a unary counter) and a label \(\ell\), this statement pushes \(u\) onto stack \(k\) and then goes to label \(\ell\).

def incr (k : K) (u : Γ k) (next : Λ) : TM2.Stmt Γ Λ σ :=
  .push k (fun _ => u) (.goto fun _ => next)

Used by 20

Used byProgram of the checking machine · Program of the layout machine · The checking run · The layout run · Run of the accept generator's precomputation · Generator machine for the accept family · Run of the precomputation (initial-row generator) · The counter part of the initial-row generator · Correctness of the clause-family generator, with its explicit time bound · Generator machine for the transition clause families · Correctness of the one-hot generator, with its explicit time bound · The one-hot generator · The Hamiltonian path verifier machine · The rest of a vertex step in the Hamiltonian-path verifier · The tape update · Writing the output · The clocked universal program · One simulated step, halting case · One simulated step, running case · Writing a timeout

DefinitionDecrement#✓fully proved

For a stack \(k\) and labels \(\ell_0\) and \(\ell_+\), this machine statement pops stack \(k\), stores in the state whether a symbol was popped, and goes to \(\ell_+\) if a symbol was popped and to \(\ell_0\) if stack \(k\) was empty.

def decr (k : K) (ifZero ifPos : Λ) : TM2.Stmt Γ Λ σ :=
  .pop k (fun _ o => Flag.tag o.isSome)
    (.branch Flag.untag (.goto fun _ => ifPos) (.goto fun _ => ifZero))

Uses 1 · Used by 29

Statement usesFlag bit of a machine state

Used byProgram of the checking machine · The checking run · Literal routine of the accept generator · Literal routine of the cell-shift generator · The cell-shift generator · The decrement chain takes \(n\) steps · The I3 loop · Counter part of one I3 iteration · The literal routine of the initial-row generator · The counter part of the initial-row generator · Literal routine of the transition-clause generator · One-hot generator: the routine for one literal · Gap emission in the counter view · The power loop · Power-loop program · The 3-COLOR emitter machine · The 3-COLOR emitter processes one clause · The emitter processes the remaining literals of a clause · The subset-sum emitter machine · Run of the pair-counting loop of the subset-sum emitter · The pass loop of the marking machine · The marking machine for PATH · Gap emission · The tape update · The clocked loop · Reading the input · The clocked universal program · One simulated step, halting case · One simulated step, running case

DefinitionPushing symbols onto several stacks#✓fully proved

Let \(ps\) be a list of pairs \((k, x)\) of a stack index \(k\) and a symbol \(x\) of the alphabet of stack \(k\), and let \(q\) be a statement of a TM2 machine. This is the statement that, for each pair \((k, x)\) of \(ps\) in list order, pushes \(x\) onto stack \(k\), and then continues with \(q\).

def pushAll (ps : List (Σ k, Γ k)) (q : TM2.Stmt Γ Λ σ) : TM2.Stmt Γ Λ σ :=
  ps.foldr (fun p q => .push p.1 (fun _ => p.2) q) q

Used by 6

Used byDraining a stack with the transfer loop · The unary read instruction · Reading a cut-off unary number · Reading a unary number · Counter transfer loop · Running a counter transfer

DefinitionAdding units to target stacks#✓fully proved

Let \(ps\) be a list of pairs \((j, x)\) of a stack \(j\) and a symbol \(x\) of stack \(j\), let \(i \in \mathbb{N}\) and let \(S\) be stacks. The resulting stacks are as follows: if \((k, x)\) is the first pair in \(ps\) whose stack is \(k\), stack \(k\) holds \(i\) copies of \(x\) followed by \(S_k\) (so the copies are on top); if no pair in \(ps\) has stack \(k\), stack \(k\) holds \(S_k\).

When the stacks in the pairs of \(ps\) are distinct, the first pair with stack \(k\) is the only one.

def addU (ps : List (Σ k, Γ k)) (i : ℕ) (S : ∀ k, List (Γ k)) : ∀ k, List (Γ k) :=
  fun k => (List.dlookup k ps).elim (S k) (fun x => cnt x i ++ S k)

Uses 1 · Used by 50

Statement usesUnary counter

Used byThe checking run · The layout run · Run of the literal routine of the accept generator · Correctness of the shift generator on one block · One literal routine of the cell-shift generator · One iteration of the overflow loop of the cell-shift generator · One iteration of the in-range loop of the cell-shift generator · Correctness of the shift generator, with its explicit time bound · One iteration of the time loop of the shift generator · One phase-loop iteration of the initial-row generator · The I3 loop · Run of one literal routine (initial-row generator) · Run of the precomputation (initial-row generator) · Correctness of the clause-family generator, with its explicit time bound · Run of one literal routine (transition-clause generator) · One iteration of the time loop · Generator run for one cell · One stack iteration of the one-hot generator · Run of one literal routine (one-hot generator) · Generator run over one time step · One Horner round · The power loop · Multi-target transfer · The 3-COLOR emitter clears its OR-output counter · Moving \(U\) onto \(E\) · Copying a counter through \(W\) · Number output of the clique reduction machine · Binary conversion (SUBSET-SUM reduction machine) · Copying a counter in the HAMPATH emitter · Adding units along no stacks · Draining a counter · End of a diamond · HAMPATH-verifier unary comparison with the counter restored · The rest of a vertex step in the Hamiltonian-path verifier · The edge loop of a pass · The frame of a read · Reading a cut-off unary number · Reading a unary number · Running time and output of the marking machine · Validation phase of the PATH marking machine · Non-destructive comparison of two counters · Copying a counter through a scratch stack · Time bound for a for loop over a counter · A for loop over a counter reaches its exit · Exact running time of a for loop over a counter · Running a counter transfer · The tape update · Writing the output · One simulated step, halting case · One simulated step, running case

DefinitionCounter transfer loop#✓fully proved

For a stack \(k\), a list \(ps\) of pairs \((t, x)\) of a stack \(t\) and a symbol \(x\) of stack \(t\), and labels \(\ell\) and \(\ell'\), this machine statement pops stack \(k\), stores in the state whether a symbol was popped, and branches on it: if a symbol was popped, it pushes \(x\) onto \(t\) for each pair \((t, x)\) of \(ps\) in list order and goes to \(\ell\); if stack \(k\) was empty, it goes to \(\ell'\).

Placed at label \(\ell\), it pops \(k\) until \(k\) is empty and pushes one copy of every target symbol per popped symbol: with \(ps\) empty it drains \(k\), with one target it moves the counter, and with two targets it copies it.

def xfer (k : K) (ps : List (Σ k, Γ k)) (self next : Λ) : TM2.Stmt Γ Λ σ :=
  .pop k (fun _ o => Flag.tag o.isSome)
    (.branch Flag.untag (pushAll ps (.goto fun _ => self)) (.goto fun _ => next))

Uses 2 · Used by 71

Statement usesFlag bit of a machine state · Pushing symbols onto several stacks

Used byProgram of the checking machine · Program of the layout machine · One clause of the accept generator · Literal routine of the accept generator · Run of the literal routine of the accept generator · Run of the accept generator's precomputation · Generator machine for the accept family · Loop body of the cell-shift generator · One clause of the cell-shift generator · Correctness of the shift generator on one block · Literal routine of the cell-shift generator · One literal routine of the cell-shift generator · One iteration of the overflow loop of the cell-shift generator · The cell-shift generator · One iteration of the in-range loop of the cell-shift generator · Correctness of the shift generator, with its explicit time bound · Block stages of the cell-shift generator · One iteration of the time loop of the shift generator · One phase-loop iteration of the initial-row generator · Run of one clause (initial-row generator) · The I3 loop · Counter part of one I3 iteration · The literal routine of the initial-row generator · Run of one literal routine (initial-row generator) · Run of the precomputation (initial-row generator) · The counter part of the initial-row generator · Literal routine of the transition-clause generator · Generator machine for the transition clause families · The drain · The drain program · Draining a stack with the transfer loop · Generator run for one cell · One clause of the one-hot generator · One stack iteration of the one-hot generator · One-hot generator: the routine for one literal · Run of one literal routine (one-hot generator) · The one-hot generator · Generator run over one time step · Gap emission in the counter view · The multiplication routine of a counter machine · A runtime for loop in the counter view · The counter program · The counter program's run · One Horner round · The statements of one Horner round · The power loop · Power-loop program · Multi-target transfer · The 3-COLOR emitter machine · Copying a counter through \(W\) · The KG-map machine · The subset-sum emitter machine · Copying a counter in the HAMPATH emitter · The HAMPATH emitter machine · Draining a counter · HAMPATH-verifier unary comparison with the counter restored · The Hamiltonian path verifier machine · The SAT-to-3SAT emitter machine · The marking machine for PATH · Adding two counters into a third · Non-destructive comparison of two counters · Copying a counter through a scratch stack · Gap emission · Time bound for a for loop over a counter · A for loop over a counter reaches its exit · Exact running time of a for loop over a counter · Multiplying unary counters · Running a counter transfer · The clocked universal program · One simulated step, halting case · One simulated step, running case

TheoremRunning a counter transfer#✓fully proved

Let \(M\) be a multi-stack machine whose state carries a flag bit, and suppose that at label \(\ell\) it executes the transfer loop that empties stack \(k\) into the targets \(p_1, \dots, p_m\) and then goes to label \(\ell'\). Here each target \(p_i\) is a pair of a stack \(t_i\) and a symbol \(x_i\) of its alphabet, the stacks \(t_1, \dots, t_m\) are distinct, and \(k\) is none of them. Let \(u\) be a symbol of stack \(k\). Then for every \(n\), every state \(v\) and all stack contents \(S\) in which stack \(k\) holds exactly \(u^n\), the machine goes in exactly \(n + 1\) steps from label \(\ell\) with state \(v\) and stacks \(S\) to label \(\ell'\) with the state that stores the flag value false and the stacks obtained from \(S\) by emptying stack \(k\) and then pushing \(n\) copies of \(x_i\) on each stack \(t_i\).

theorem xfer_run {self next : Λ} {k : K} {ps : List (Σ k, Γ k)}
    (hp : M self = xfer k ps self next) (hps : ps.NodupKeys) (hk : k ∉ ps.keys) (u : Γ k) :
    ∀ (n : ℕ) (v : σ) (S : ∀ k, List (Γ k)), S k = cnt u n →
      Run M (n + 1) ⟨some self, v, S⟩ ⟨some next, Flag.tag false, addU ps n (update S k [])⟩

Uses 7 · Used by 43

Statement usesFlag bit of a machine state · Exact-length runs of a TM2 machine · Adding units to target stacks · Unary counter · Counter transfer loop

Proof usesA single step executes the statement at the current label · Pushing symbols onto several stacks

Used byThe checking run · The layout run · Run of the literal routine of the accept generator · Correctness of the shift generator on one block · One literal routine of the cell-shift generator · One iteration of the overflow loop of the cell-shift generator · One iteration of the in-range loop of the cell-shift generator · Correctness of the shift generator, with its explicit time bound · One iteration of the time loop of the shift generator · One phase-loop iteration of the initial-row generator · The I3 loop · Run of one literal routine (initial-row generator) · Run of the precomputation (initial-row generator) · Correctness of the clause-family generator, with its explicit time bound · Run of one literal routine (transition-clause generator) · One iteration of the time loop · Generator run for one cell · One stack iteration of the one-hot generator · Run of one literal routine (one-hot generator) · Generator run over one time step · One Horner round · The power loop · Multi-target transfer · The 3-COLOR emitter clears its OR-output counter · Moving \(U\) onto \(E\) · Copying a counter through \(W\) · Number output of the clique reduction machine · Binary conversion (SUBSET-SUM reduction machine) · Copying a counter in the HAMPATH emitter · Draining a counter · End of a diamond · HAMPATH-verifier unary comparison with the counter restored · The rest of a vertex step in the Hamiltonian-path verifier · The edge loop of a pass · Non-destructive comparison of two counters · Copying a counter through a scratch stack · Time bound for a for loop over a counter · A for loop over a counter reaches its exit · Exact running time of a for loop over a counter · The tape update · Writing the output · One simulated step, halting case · One simulated step, running case

DefinitionOne round of counter comparison#✓fully proved

For stacks \(a, b, t_a, t_b\), symbols \(u_{t_a}\) of stack \(t_a\) and \(u_{t_b}\) of stack \(t_b\), and labels \(\mathit{self}\), \(\mathit{lt}\), \(\mathit{eq}\) and \(\mathit{gt}\), this machine statement pops stack \(a\) and then stack \(b\); after each pop it stores in the state whether the pop found a symbol and branches on it. If both pops found a symbol, it pushes \(u_{t_a}\) onto \(t_a\), then \(u_{t_b}\) onto \(t_b\), and goes to \(\mathit{self}\). If only the pop of \(a\) found a symbol, it pushes \(u_{t_a}\) onto \(t_a\) and goes to \(\mathit{gt}\); if only the pop of \(b\) found one, it pushes \(u_{t_b}\) onto \(t_b\) and goes to \(\mathit{lt}\); if neither did, it goes to \(\mathit{eq}\).

def cmpStep (a b ta tb : K) (uta : Γ ta) (utb : Γ tb)
    (self lt eq gt : Λ) : TM2.Stmt Γ Λ σ :=
  .pop a (fun _ o => Flag.tag o.isSome) <| .branch Flag.untag
    (.pop b (fun _ o => Flag.tag o.isSome) <| .branch Flag.untag
      (.push ta (fun _ => uta) <| .push tb (fun _ => utb) <| .goto fun _ => self)
      (.push ta (fun _ => uta) <| .goto fun _ => gt))
    (.pop b (fun _ o => Flag.tag o.isSome) <| .branch Flag.untag
      (.push tb (fun _ => utb) <| .goto fun _ => lt)
      (.goto fun _ => eq))

Uses 1 · Used by 13

Statement usesFlag bit of a machine state

Used byProgram of the checking machine · Literal routine of the accept generator · Literal routine of the cell-shift generator · The literal routine of the initial-row generator · Literal routine of the transition-clause generator · One-hot generator: the routine for one literal · Gap emission in the counter view · The subset-sum emitter machine · The Hamiltonian path verifier machine · The comparison loop · Non-destructive comparison of two counters · Gap emission · The clocked universal program

TheoremThe comparison loop#✓fully proved

Let \(a, b, t_a, t_b\) be pairwise distinct stacks with unit symbols \(u_a, u_b, u_{t_a}, u_{t_b}\), and let \(r\) map each ordering to a label. Suppose the machine \(M\) has at label \(\ell\) the comparison round of \(a\) and \(b\) with scratch stacks \(t_a, t_b\) and units \(u_{t_a}, u_{t_b}\) that repeats at \(\ell\) and exits to \(r(\mathrm{lt})\), \(r(\mathrm{eq})\) and \(r(\mathrm{gt})\): it pops \(a\) and \(b\), pushes \(u_{t_a}\) onto \(t_a\) if \(a\) was non-empty and \(u_{t_b}\) onto \(t_b\) if \(b\) was non-empty, and goes to \(\ell\) if both were non-empty, to \(r(\mathrm{lt})\) if only \(b\) was, to \(r(\mathrm{eq})\) if neither was and to \(r(\mathrm{gt})\) if only \(a\) was. Then for all \(m, n, p, q \in \mathbb{N}\), every state \(v\) and all stacks \(S\) in which \(a, b, t_a, t_b\) hold exactly \(u_a^m, u_b^n, u_{t_a}^p, u_{t_b}^q\) respectively, there are a state \(v'\) and stacks \(S'\) such that exactly \(\min(m, n) + 1\) steps of \(M\) lead from label \(\ell\) with state \(v\) and stacks \(S\) to label \(r(\mathrm{compare}(m, n))\) with state \(v'\) and stacks \(S'\), where in \(S'\) the stack \(a\) holds \(u_a^{m - \min(m, n+1)}\), \(b\) holds \(u_b^{n - \min(n, m+1)}\), \(t_a\) holds \(u_{t_a}^{p + \min(m, n+1)}\), \(t_b\) holds \(u_{t_b}^{q + \min(n, m+1)}\), and every other stack is as in \(S\).

theorem cmpLoop_run {a b ta tb : K} {ua : Γ a} {ub : Γ b} {uta : Γ ta} {utb : Γ tb}
    {self : Λ} {r : Ordering → Λ}
    (hp : M self = cmpStep a b ta tb uta utb self (r .lt) (r .eq) (r .gt))
    (hab : a ≠ b) (hata : a ≠ ta) (hatb : a ≠ tb) (hbta : b ≠ ta) (hbtb : b ≠ tb)
    (htt : ta ≠ tb) :
    ∀ (m n p q : ℕ) (v : σ) (S : ∀ k, List (Γ k)), S a = cnt ua m → S b = cnt ub n →
      S ta = cnt uta p → S tb = cnt utb q →
      ∃ (v' : σ) (S' : ∀ k, List (Γ k)),
        Run M (min m n + 1) ⟨some self, v, S⟩ ⟨some (r (compare m n)), v', S'⟩ ∧
        S' a = cnt ua (m - min m (n + 1)) ∧ S' b = cnt ub (n - min n (m + 1)) ∧
        S' ta = cnt uta (p + min m (n + 1)) ∧ S' tb = cnt utb (q + min n (m + 1)) ∧
        ∀ k, k ≠ a → k ≠ b → k ≠ ta → k ≠ tb → S' k = S k

Uses 5 · Used by 1

Statement usesFlag bit of a machine state · Exact-length runs of a TM2 machine · One round of counter comparison · Unary counter

Proof usesA single step executes the statement at the current label

Used byNon-destructive comparison of two counters

TheoremNon-destructive comparison of two counters#✓fully proved

Let \(M\) be a TM2 machine whose state type carries a flag bit, let \(a, b, t_a, t_b\) be pairwise distinct stacks with symbols \(u_a\), \(u_b\), \(u_{t_a}\), \(u_{t_b}\) of their alphabets, let \(\ell\) be a label and let \(r\), \(r'\), \(o\) map each ordering to a label. Suppose that \(M\) has at \(\ell\) the comparison round of \(a\) and \(b\) with scratch stacks \(t_a, t_b\) and units \(u_{t_a}, u_{t_b}\) that goes to \(\ell\) again and exits to \(r(\mathrm{lt})\), \(r(\mathrm{eq})\) and \(r(\mathrm{gt})\), and that for every ordering \(\omega\), \(M\) has at \(r(\omega)\) the counter transfer loop of \(t_a\) into the single target \((a, u_a)\) that repeats at \(r(\omega)\) and exits to \(r'(\omega)\), and has at \(r'(\omega)\) the counter transfer loop of \(t_b\) into the single target \((b, u_b)\) that repeats at \(r'(\omega)\) and exits to \(o(\omega)\). Write \(\mathrm{compare}(m, n)\) for the ordering of natural numbers \(m\) and \(n\), and \([m \ne n]\) for \(1\) if \(m \ne n\) and \(0\) otherwise. Then for all \(m, n \in \mathbb{N}\), every state \(v\) and all stacks \(S\) in which \(a\) holds exactly \(u_a^m\), \(b\) holds exactly \(u_b^n\) and \(t_a\) and \(t_b\) are empty, \(M\) runs in exactly \(3\min(m, n) + 3 + [m \ne n]\) steps from label \(\ell\) with state \(v\) and stacks \(S\) to label \(o(\mathrm{compare}(m, n))\) with the state that stores the flag value false and with the same stacks \(S\).

theorem cmp_run {a b ta tb : K} {ua : Γ a} {ub : Γ b} {uta : Γ ta} {utb : Γ tb}
    {self : Λ} {r rB out : Ordering → Λ}
    (hp : M self = cmpStep a b ta tb uta utb self (r .lt) (r .eq) (r .gt))
    (hA : ∀ o, M (r o) = xfer ta [⟨a, ua⟩] (r o) (rB o))
    (hB : ∀ o, M (rB o) = xfer tb [⟨b, ub⟩] (rB o) (out o))
    (hab : a ≠ b) (hata : a ≠ ta) (hatb : a ≠ tb) (hbta : b ≠ ta) (hbtb : b ≠ tb)
    (htt : ta ≠ tb) (m n : ℕ) (v : σ) (S : ∀ k, List (Γ k)) (ha : S a = cnt ua m)
    (hb : S b = cnt ub n) (hta : S ta = []) (htb : S tb = []) :
    Run M (3 * min m n + 3 + (if m = n then 0 else 1)) ⟨some self, v, S⟩
      ⟨some (out (compare m n)), Flag.tag false, S⟩

Uses 8 · Used by 6

Statement usesFlag bit of a machine state · Exact-length runs of a TM2 machine · One round of counter comparison · Unary counter · Counter transfer loop

Proof usesAdding units to target stacks · The comparison loop · Running a counter transfer

Used byThe checking run · Run of the VERTEX-COVER to SUBSET-SUM machine · Run of a HAMPATH-verifier counter comparison · Gap emission · One simulated step, halting case · One simulated step, running case

DefinitionSum of consecutive values#✓fully proved

For \(f : \mathbb{N} \to \mathbb{N}\) and \(i, j \in \mathbb{N}\), \(\mathrm{sumFrom}(f, i, j) = f(i) + f(i+1) + \dots + f(i+j-1)\) is the sum of \(f(t)\) over the \(j\) indices \(t\) with \(i \le t < i + j\); it is \(0\) when \(j = 0\).

def sumFrom (f : ℕ → ℕ) (i : ℕ) : ℕ → ℕ
  | 0 => 0
  | j + 1 => f i + sumFrom f (i + 1) j

Used by 4

Used byThe row loop of a diamond in the HAMPATH emitter · Exact running time of a for loop over a counter · Multiplying unary counters · Termwise bound on a sum of consecutive values

TheoremTermwise bound on a sum of consecutive values#✓fully proved

Let \(f : \mathbb{N} \to \mathbb{N}\) and \(c, i, j \in \mathbb{N}\). If \(f(t) \le c\) for every \(t\) with \(i \le t < i + j\), then \(\mathrm{sumFrom}(f, i, j) = f(i) + f(i+1) + \dots + f(i+j-1)\) is at most \(j \cdot c\).

theorem sumFrom_le {f : ℕ → ℕ} {c : ℕ} :
    ∀ (i j : ℕ), (∀ t, i ≤ t → t < i + j → f t ≤ c) → sumFrom f i j ≤ j * c

Uses 1 · Used by 1

Statement usesSum of consecutive values

Used byThe row loop of a diamond in the HAMPATH emitter

DefinitionLoop head of a for loop over a counter#✓fully proved

For stacks \(c\) and \(c'\), a symbol \(u'\) of stack \(c'\) and labels \(b\) and \(r\), the loop head is the statement that pops stack \(c\), replaces the machine state by the state whose flag bit records whether a symbol was popped, and branches on that bit: if a symbol was popped, it pushes \(u'\) onto the index stack \(c'\) and goes to label \(b\) (the loop body); if \(c\) was empty, it goes to label \(r\).

def forHead (c cd : K) (ucd : Γ cd) (body rest : Λ) : TM2.Stmt Γ Λ σ :=
  .pop c (fun _ o => Flag.tag o.isSome) <| .branch Flag.untag
    (.push cd (fun _ => ucd) <| .goto fun _ => body) (.goto fun _ => rest)

Uses 1 · Used by 13

Statement usesFlag bit of a machine state

Used byProgram of the layout machine · The cell-shift generator · Block stages of the cell-shift generator · The counter part of the initial-row generator · Generator machine for the transition clause families · The one-hot generator · The multiplication routine of a counter machine · A runtime for loop in the counter view · The HAMPATH emitter machine · Time bound for a for loop over a counter · A for loop over a counter reaches its exit · Exact running time of a for loop over a counter · Multiplying unary counters

TheoremExact running time of a for loop over a counter#✓fully proved

Let \(M\) be a multi-stack machine whose states carry a flag bit, with \(\mathrm{tag}(\beta)\) the state storing the bit \(\beta\); write \((\ell, v, S)\) for the configuration at label \(\ell\) with state \(v\) and stack contents \(S\), and \(u^m\) for a stack holding exactly \(m\) copies of the symbol \(u\). Let \(c \ne c'\) be stacks with a symbol \(u\) of stack \(c\) and a symbol \(u'\) of stack \(c'\), and let \(h, b, r, e\) be labels such that at \(h\) the machine runs the loop head on \(c\) with index stack \(c'\) (pop \(c\); if a symbol was popped, push \(u'\) onto \(c'\) and go to \(b\), otherwise go to \(r\)), and at \(r\) it runs the transfer that drains \(c'\), pushing one \(u\) onto \(c\) per popped symbol, and then goes to \(e\). Let \(n \in \mathbb{N}\), let \(\mathrm{cost} : \mathbb{N} \to \mathbb{N}\), and let \(P(i, S)\) be a predicate such that \(P(i, S)\) implies \(P(i, S')\) whenever \(S\) and \(S'\) agree on every stack other than \(c\) and \(c'\). Assume that for every \(i < n\) and all stack contents \(S\) with \(S_c = u^{n-1-i}\), \(S_{c'} = u'^{\,i+1}\) and \(P(i, S)\), there are a state \(v'\) and stack contents \(S'\) such that \(M\) goes from \((b, \mathrm{tag}(\mathrm{true}), S)\) to \((h, v', S')\) in exactly \(\mathrm{cost}(i)\) steps, with \(S'_c = S_c\), \(S'_{c'} = S_{c'}\) and \(P(i + 1, S')\). Then for every state \(v\) and all stack contents \(S\) with \(S_c = u^n\), \(S_{c'}\) empty and \(P(0, S)\), there are stack contents \(S'\) such that \(M\) goes from \((h, v, S)\) to \((e, \mathrm{tag}(\mathrm{false}), S')\) in exactly \(\sum_{i < n} (\mathrm{cost}(i) + 1) + n + 2\) steps, with \(S'_c = u^n\), \(S'_{c'}\) empty and \(P(n, S')\).

MetaMathlibExt.TM2Program.forLoop_run · 15 lines

theorem forLoop_run {c cd : K} {uc : Γ c} {ucd : Γ cd} {head body rest next : Λ}
    (hHead : M head = forHead c cd ucd body rest)
    (hRest : M rest = xfer cd [⟨c, uc⟩] rest next) (hc : c ≠ cd) (n : ℕ)
    (P : ℕ → (∀ k, List (Γ k)) → Prop)
    (hP : ∀ i S S', (∀ k, k ≠ c → k ≠ cd → S' k = S k) → P i S → P i S')
    (cost : ℕ → ℕ)
    (hbody : ∀ i < n, ∀ S : ∀ k, List (Γ k), S c = cnt uc (n - 1 - i) → S cd = cnt ucd (i + 1) →
      P i S → ∃ (v' : σ) (S' : ∀ k, List (Γ k)),
        Run M (cost i) ⟨some body, Flag.tag true, S⟩ ⟨some head, v', S'⟩ ∧
        S' c = S c ∧ S' cd = S cd ∧ P (i + 1) S')
    (v : σ) (S : ∀ k, List (Γ k)) (hSc : S c = cnt uc n) (hScd : S cd = []) (h0 : P 0 S) :
    ∃ S' : ∀ k, List (Γ k),
      Run M (sumFrom (fun i => cost i + 1) 0 n + n + 2) ⟨some head, v, S⟩
        ⟨some next, Flag.tag false, S'⟩ ∧
      S' c = cnt uc n ∧ S' cd = [] ∧ P n S'

Uses 9 · Used by 2

Statement usesFlag bit of a machine state · Exact-length runs of a TM2 machine · Unary counter · Loop head of a for loop over a counter · Sum of consecutive values · Counter transfer loop

Proof usesA single step executes the statement at the current label · Adding units to target stacks · Running a counter transfer

Used byThe row loop of a diamond in the HAMPATH emitter · Multiplying unary counters

DefinitionPushing a list of symbols onto one stack#✓fully proved

Let \(k\) be a stack index, \(xs = [x_1, \dots, x_m]\) a list of symbols of the alphabet of stack \(k\), and \(q\) a statement of a TM2 machine. This is the statement that pushes \(x_1, \dots, x_m\) onto stack \(k\) in that order, so that \(x_m\) ends on top when \(m \ge 1\), and then continues with \(q\).

def pushList (k : K) (xs : List (Γ k)) (q : TM2.Stmt Γ Λ σ) : TM2.Stmt Γ Λ σ :=
  xs.foldr (fun x q => .push k (fun _ => x) q) q

Used by 54

Used byThe checking run · The layout run · Converter turns a unary count into a canonical binary frame · Converter turns a unary count into a raw canonical binary payload · One clause of the accept generator · Run of the literal routine of the accept generator · Run of the accept generator's precomputation · One clause of the cell-shift generator · Correctness of the shift generator on one block · One literal routine of the cell-shift generator · Correctness of the shift generator, with its explicit time bound · Run of one clause (initial-row generator) · Run of one literal routine (initial-row generator) · Run of the precomputation (initial-row generator) · Run of the transition-family generator on one clause · Correctness of the clause-family generator, with its explicit time bound · Run of one literal routine (transition-clause generator) · One clause of the one-hot generator · One stack iteration of the one-hot generator · Run of one literal routine (one-hot generator) · Correctness of the one-hot generator, with its explicit time bound · The counter program's run · One Horner round · The 3-COLOR emitter machine · Running a copy site of the 3-COLOR emitter · The 3-COLOR emitter processes one clause · The emitter processes the remaining literals of a clause · Correctness and step bound of the 3-COLOR emitter · Clique emitter: the instance prefix · Correctness and running time of the KG-map machine · Number output of the clique reduction machine · Linear step bound for the PARTITION doubling machine · Quadratic run of the raw-input SUBSET-SUM to PARTITION machine · Raw-input PARTITION membership machine runs in quadratic time · Edge-number phase (SUBSET-SUM reduction machine) · Subset-sum emitter: one vertex number · Run of the VERTEX-COVER to SUBSET-SUM machine · The HAMPATH emitter machine · Run of a HAMPATH copy site · HAMPATH emitter, phase A: one clause · HAMPATH emitter, phase A: one literal · One clause of the detour walk · Phase A of the HAMPATH emitter · The detours of a diamond · The output phase of the HAMPATH emitter · Name copy loop of the 3SAT emitter · Fresh-literal subroutine of the 3SAT emitter · Copying a renamed name · The SAT-to-3SAT emitter writes the encoded translation in quadratic time · Tokenize, then emit · Closing an output clause in the SAT-to-3SAT emitter · Pushing a constant list · Gap emission · Draining a counter while prepending a block

DefinitionPushing a constant list#✓fully proved

For a stack \(k\), a list \((x_1, \dots, x_m)\) of symbols of stack \(k\) and a label \(\ell\), this statement pushes \(x_1, \dots, x_m\) onto stack \(k\) in this order, so that \(x_m\) ends on top, and then goes to label \(\ell\). The machine executes it in a single step.

def emit (k : K) (xs : List (Γ k)) (next : Λ) : TM2.Stmt Γ Λ σ :=
  pushList k xs (.goto fun _ => next)

Uses 1 · Used by 44

Statement usesPushing a list of symbols onto one stack

Used byProgram of the checking machine · The checking run · The layout run · Converter turns a unary count into a canonical binary frame · Converter turns a unary count into a raw canonical binary payload · One clause of the accept generator · Run of the literal routine of the accept generator · Run of the accept generator's precomputation · One clause of the cell-shift generator · Correctness of the shift generator on one block · One literal routine of the cell-shift generator · Correctness of the shift generator, with its explicit time bound · Run of one clause (initial-row generator) · Run of one literal routine (initial-row generator) · Run of the precomputation (initial-row generator) · Run of the transition-family generator on one clause · Correctness of the clause-family generator, with its explicit time bound · Run of one literal routine (transition-clause generator) · One clause of the one-hot generator · One stack iteration of the one-hot generator · Run of one literal routine (one-hot generator) · Correctness of the one-hot generator, with its explicit time bound · The counter program's run · One Horner round · The 3-COLOR emitter machine · Running a copy site of the 3-COLOR emitter · The KG-map machine · Correctness and running time of the KG-map machine · Number output of the clique reduction machine · Membership transducer embeds the doubling machine · Program of the PARTITION doubling machine · Linear step bound for the PARTITION doubling machine · Quadratic run of the raw-input SUBSET-SUM to PARTITION machine · Raw-input PARTITION membership machine runs in quadratic time · The subset-sum emitter machine · Subset-sum emitter: one vertex number · Run of the VERTEX-COVER to SUBSET-SUM machine · The HAMPATH emitter machine · Run of a HAMPATH copy site · Fresh-literal subroutine of the 3SAT emitter · Program of the tokenize-then-emit machine · Tokenize, then emit · Gap emission · Prepending a constant list

TheoremCopying a counter through a scratch stack#✓fully proved

Let \(a, c, t\) be pairwise distinct stacks with unit symbols \(u_a, u_c, u_t\). Write \(\mathrm{xfer}(k, ps, \ell, \ell')\) for the transfer loop at label \(\ell\) that pops stack \(k\) until it is empty, pushing \(x\) onto stack \(j\) for each pair \((j, x)\) in \(ps\) per popped symbol, and then goes to \(\ell'\). Suppose the machine \(M\) has \(M(l_1) = \mathrm{xfer}(a, [(c, u_c), (t, u_t)], l_1, l_2)\) and \(M(l_2) = \mathrm{xfer}(t, [(a, u_a)], l_2, \mathit{next})\). Let \(m, p \in \mathbb{N}\), let \(v\) be a state and let \(S\) be stacks in which \(a\) holds exactly \(u_a^m\), \(c\) holds \(u_c^p\) and \(t\) is empty. Then exactly \(2m + 2\) steps of \(M\) lead from label \(l_1\) with state \(v\) and stacks \(S\) to label \(\mathit{next}\) with the state storing the flag false and the stacks \(S\) with \(c\) replaced by \(u_c^{m+p}\).

theorem copy_run {a c t : K} {ua : Γ a} {uc : Γ c} {ut : Γ t} {l₁ l₂ next : Λ}
    (h₁ : M l₁ = xfer a [⟨c, uc⟩, ⟨t, ut⟩] l₁ l₂) (h₂ : M l₂ = xfer t [⟨a, ua⟩] l₂ next)
    (hac : a ≠ c) (hat : a ≠ t) (hct : c ≠ t) (m p : ℕ) (v : σ) (S : ∀ k, List (Γ k))
    (ha : S a = cnt ua m) (hc : S c = cnt uc p) (ht : S t = []) :
    Run M (2 * m + 2) ⟨some l₁, v, S⟩ ⟨some next, Flag.tag false, update S c (cnt uc (m + p))⟩

Uses 6 · Used by 28

Statement usesFlag bit of a machine state · Exact-length runs of a TM2 machine · Unary counter · Counter transfer loop

Proof usesAdding units to target stacks · Running a counter transfer

Used byOne clause of the accept generator · Run of the literal routine of the accept generator · Run of the accept generator's precomputation · One clause of the cell-shift generator · Correctness of the shift generator on one block · One literal routine of the cell-shift generator · One iteration of the overflow loop of the cell-shift generator · One iteration of the in-range loop of the cell-shift generator · Correctness of the shift generator, with its explicit time bound · One iteration of the time loop of the shift generator · One phase-loop iteration of the initial-row generator · Run of one clause (initial-row generator) · Counter part of one I3 iteration · Run of one literal routine (initial-row generator) · Run of the precomputation (initial-row generator) · Run of the transition-family generator on one clause · Correctness of the clause-family generator, with its explicit time bound · Run of one literal routine (transition-clause generator) · Generator run for one cell · One clause of the one-hot generator · One stack iteration of the one-hot generator · Run of one literal routine (one-hot generator) · The counter program's run · Edge-number phase (SUBSET-SUM reduction machine) · Run of the pair-counting loop of the subset-sum emitter · Fresh-literal subroutine of the 3SAT emitter · Adding two counters into a third · Multiplying unary counters

TheoremAdding two counters into a third#✓fully proved

Let \(a, b, c, t\) be stacks with \(a \ne c\), \(a \ne t\), \(b \ne c\), \(b \ne t\) and \(c \ne t\), with unit symbols \(u_a, u_b, u_c, u_t\). Write \(\mathrm{xfer}(k, ps, \ell, \ell')\) for the transfer loop at label \(\ell\) that pops stack \(k\) until it is empty, pushing \(x\) onto stack \(j\) for each pair \((j, x)\) in \(ps\) per popped symbol, and then goes to \(\ell'\). Suppose the machine \(M\) has \(M(l_1) = \mathrm{xfer}(a, [(c, u_c), (t, u_t)], l_1, l_2)\), \(M(l_2) = \mathrm{xfer}(t, [(a, u_a)], l_2, l_3)\), \(M(l_3) = \mathrm{xfer}(b, [(c, u_c), (t, u_t)], l_3, l_4)\) and \(M(l_4) = \mathrm{xfer}(t, [(b, u_b)], l_4, \mathit{next})\). Let \(m, n, p \in \mathbb{N}\), let \(v\) be a state and let \(S\) be stacks in which \(a\) holds exactly \(u_a^m\), \(b\) holds \(u_b^n\), \(c\) holds \(u_c^p\) and \(t\) is empty. Then exactly \(2m + 2n + 4\) steps of \(M\) lead from label \(l_1\) with state \(v\) and stacks \(S\) to label \(\mathit{next}\) with the state storing the flag false and the stacks \(S\) with \(c\) replaced by \(u_c^{m+n+p}\).

theorem add_run {a b c t : K} {ua : Γ a} {ub : Γ b} {uc : Γ c} {ut : Γ t}
    {l₁ l₂ l₃ l₄ next : Λ}
    (h₁ : M l₁ = xfer a [⟨c, uc⟩, ⟨t, ut⟩] l₁ l₂) (h₂ : M l₂ = xfer t [⟨a, ua⟩] l₂ l₃)
    (h₃ : M l₃ = xfer b [⟨c, uc⟩, ⟨t, ut⟩] l₃ l₄) (h₄ : M l₄ = xfer t [⟨b, ub⟩] l₄ next)
    (hac : a ≠ c) (hat : a ≠ t) (hbc : b ≠ c) (hbt : b ≠ t) (hct : c ≠ t) (m n p : ℕ) (v : σ)
    (S : ∀ k, List (Γ k)) (ha : S a = cnt ua m) (hb : S b = cnt ub n) (hc : S c = cnt uc p)
    (ht : S t = []) :
    Run M (2 * m + 2 * n + 4) ⟨some l₁, v, S⟩
      ⟨some next, Flag.tag false, update S c (cnt uc (m + n + p))⟩

Uses 5

Statement usesFlag bit of a machine state · Exact-length runs of a TM2 machine · Unary counter · Counter transfer loop

Proof usesCopying a counter through a scratch stack

TheoremMultiplying unary counters#✓fully proved

Let \(M\) be a multi-stack machine whose states carry a flag bit, with \(\mathrm{tag}(\mathrm{false})\) the state storing the bit false; write \((\ell, v, S)\) for the configuration at label \(\ell\) with state \(v\) and stack contents \(S\), and \(u^m\) for a stack holding exactly \(m\) copies of the symbol \(u\). Let \(a, a', b, c, t\) be pairwise distinct stacks with symbols \(u_a, u_{a'}, u_b, u_c, u_t\) of the respective stacks, and let \(h, \ell_1, \ell_2, r, e\) be labels such that: at \(h\) the machine runs the loop head on \(a\) with index stack \(a'\) (pop \(a\); if a symbol was popped, push \(u_{a'}\) onto \(a'\) and go to \(\ell_1\), otherwise go to \(r\)); at \(\ell_1\) it runs the transfer that drains \(b\), pushing \(u_c\) onto \(c\) and \(u_t\) onto \(t\) per popped symbol, and then goes to \(\ell_2\); at \(\ell_2\) it runs the transfer that drains \(t\), pushing \(u_b\) onto \(b\) per popped symbol, and then goes to \(h\); and at \(r\) it runs the transfer that drains \(a'\), pushing \(u_a\) onto \(a\) per popped symbol, and then goes to \(e\). Then for all \(m, n, p \in \mathbb{N}\), every state \(v\) and all stack contents \(S\) with \(S_a = u_a^m\), \(S_{a'}\) empty, \(S_b = u_b^n\), \(S_c = u_c^p\) and \(S_t\) empty, \(M\) goes from \((h, v, S)\) to \((e, \mathrm{tag}(\mathrm{false}), S')\) in exactly \(m(2n + 3) + m + 2\) steps, where \(S'\) agrees with \(S\) on every stack except \(c\) and \(S'_c = u_c^{mn + p}\).

theorem mul_run {a ad b c t : K} {ua : Γ a} {uad : Γ ad} {ub : Γ b} {uc : Γ c} {ut : Γ t}
    {head body l₂ rest next : Λ}
    (hHead : M head = forHead a ad uad body rest)
    (hBody : M body = xfer b [⟨c, uc⟩, ⟨t, ut⟩] body l₂)
    (hL₂ : M l₂ = xfer t [⟨b, ub⟩] l₂ head)
    (hRest : M rest = xfer ad [⟨a, ua⟩] rest next)
    (hnd : [a, ad, b, c, t].Nodup) (m n p : ℕ) (v : σ) (S : ∀ k, List (Γ k))
    (ha : S a = cnt ua m) (had : S ad = []) (hb : S b = cnt ub n) (hc : S c = cnt uc p)
    (ht : S t = []) :
    Run M (m * (2 * n + 3) + m + 2) ⟨some head, v, S⟩
      ⟨some next, Flag.tag false, update S c (cnt uc (m * n + p))⟩

Uses 8 · Used by 20

Statement usesFlag bit of a machine state · Exact-length runs of a TM2 machine · Unary counter · Loop head of a for loop over a counter · Counter transfer loop

Proof usesCopying a counter through a scratch stack · Exact running time of a for loop over a counter · Sum of consecutive values

Used byThe layout run · Run of the accept generator's precomputation · Correctness of the shift generator on one block · One iteration of the overflow loop of the cell-shift generator · One iteration of the in-range loop of the cell-shift generator · Correctness of the shift generator, with its explicit time bound · One iteration of the time loop of the shift generator · One phase-loop iteration of the initial-row generator · Counter part of one I3 iteration · Run of the precomputation (initial-row generator) · Correctness of the clause-family generator, with its explicit time bound · Run of one literal routine (transition-clause generator) · One iteration of the time loop · Generator run for one cell · One stack iteration of the one-hot generator · Correctness of the one-hot generator, with its explicit time bound · Generator run over one time step · The counter program's run · One Horner round · The power loop

DefinitionRepeated block#✓fully proved

For a list \(ys\) and \(n \in \mathbb{N}\), \(\mathrm{rep}(ys, n)\) is the concatenation of \(n\) copies of \(ys\); it is the empty list when \(n = 0\).

def rep {α : Type} (ys : List α) (n : ℕ) : List α := (List.replicate n ys).flatten

Used by 34

Used byOne clause of the accept generator · Run of the literal routine of the accept generator · One clause of the cell-shift generator · One literal routine of the cell-shift generator · The literal routines of one clause of the cell-shift generator · Run of one clause (initial-row generator) · Run of one literal routine (initial-row generator) · Run of the literal routines of a clause (initial-row generator) · Run of the transition-family generator on one clause · Encoding a dense clause block by block · Gap encoding of a dense clause · Shifting the start of a gap encoding · Run of one literal routine (transition-clause generator) · Run of the literal routines of a clause (transition-clause generator) · One clause of the one-hot generator · Run of one literal routine (one-hot generator) · Run of the literal routines of a clause (one-hot generator) · Gap emission in the counter view · The dense-to-binary translation on raw bits is polynomial-time · The dense-to-binary translation on the reversed bit string · The translation on the remaining clauses · The translation computes the binary encoding · The translation on the slots of a clause · Self-delimiting code of a block of ones · Binary codes of literals on variables one less than a power of two · Clique emitter: the instance prefix · Output block of an edge number · Edge-number phase (SUBSET-SUM reduction machine) · Run of the VERTEX-COVER to SUBSET-SUM machine · Code of a fresh literal · Fresh-literal subroutine of the 3SAT emitter · Repeating a single bit · The SAT-to-3SAT emitter writes the encoded translation in quadratic time · Gap emission

DefinitionPrepending a constant list#✓fully proved

For a stack \(k\), a list \((y_1, \dots, y_m)\) of symbols of stack \(k\) and a label \(\ell\), this statement pushes \(y_m, \dots, y_1\) onto stack \(k\) in this order and then goes to label \(\ell\); it is the constant-list push of the reversed list. Afterwards \(y_1, \dots, y_m\) sit on top of stack \(k\), read from the top down.

def emitR (k : K) (ys : List (Γ k)) (next : Λ) : TM2.Stmt Γ Λ σ := emit k ys.reverse next

Uses 1 · Used by 51

Statement usesPushing a constant list

Used byProgram of the layout machine · The layout run · One clause of the accept generator · Literal routine of the accept generator · Run of the literal routine of the accept generator · Run of the accept generator's precomputation · Generator machine for the accept family · Loop body of the cell-shift generator · One clause of the cell-shift generator · Correctness of the shift generator on one block · Literal routine of the cell-shift generator · One literal routine of the cell-shift generator · The cell-shift generator · Correctness of the shift generator, with its explicit time bound · Block stages of the cell-shift generator · Run of one clause (initial-row generator) · The literal routine of the initial-row generator · Run of one literal routine (initial-row generator) · Run of the precomputation (initial-row generator) · The counter part of the initial-row generator · Run of the transition-family generator on one clause · Correctness of the clause-family generator, with its explicit time bound · Literal routine of the transition-clause generator · Run of one literal routine (transition-clause generator) · Generator machine for the transition clause families · One clause of the one-hot generator · One stack iteration of the one-hot generator · One-hot generator: the routine for one literal · Run of one literal routine (one-hot generator) · Correctness of the one-hot generator, with its explicit time bound · The one-hot generator · Gap emission in the counter view · The counter program · The counter program's run · One Horner round · The statements of one Horner round · The 3-COLOR emitter machine · Running a copy site of the 3-COLOR emitter · The KG-map machine · Correctness and running time of the KG-map machine · Program of the raw-input SUBSET-SUM to PARTITION machine · Program of the raw-input PARTITION membership machine · Quadratic run of the raw-input SUBSET-SUM to PARTITION machine · Raw-input PARTITION membership machine runs in quadratic time · The subset-sum emitter machine · Run of the VERTEX-COVER to SUBSET-SUM machine · Name copy loop of the 3SAT emitter · Fresh-literal subroutine of the 3SAT emitter · The SAT-to-3SAT emitter machine · Closing an output clause in the SAT-to-3SAT emitter · Gap emission

DefinitionDraining a counter while prepending a block#✓fully proved

Let \(k\) and \(o\) be stack indices, \(ys\) a list of symbols of the alphabet of stack \(o\), and \(\ell\) and \(\ell'\) labels. This is the TM2 statement that pops stack \(k\) and sets the internal state to the flag bit recording whether a symbol was popped. If one was, it prepends \(ys\) to stack \(o\) (so that \(ys\) reads from the top down) and goes to \(\ell\); if stack \(k\) was empty, it goes to \(\ell'\).

Used as the statement at label \(\ell\) with \(k \ne o\), it empties a unary counter on stack \(k\) and prepends one copy of \(ys\) to stack \(o\) per unit removed, then goes to \(\ell'\).

def xferE (k o : K) (ys : List (Γ o)) (self next : Λ) : TM2.Stmt Γ Λ σ :=
  .pop k (fun _ o => Flag.tag o.isSome)
    (.branch Flag.untag (pushList o ys.reverse (.goto fun _ => self)) (.goto fun _ => next))

Uses 2 · Used by 17

Statement usesFlag bit of a machine state · Pushing a list of symbols onto one stack

Used byOne clause of the accept generator · Generator machine for the accept family · Loop body of the cell-shift generator · One clause of the cell-shift generator · Run of one clause (initial-row generator) · The counter part of the initial-row generator · Run of the transition-family generator on one clause · Generator machine for the transition clause families · One clause of the one-hot generator · The one-hot generator · The CLIQUE emitter machine · Clique emitter: the instance prefix · Edge-number phase (SUBSET-SUM reduction machine) · The subset-sum emitter machine · Fresh-literal subroutine of the 3SAT emitter · The SAT-to-3SAT emitter machine · The SAT-to-3SAT emitter writes the encoded translation in quadratic time

TheoremGap emission#✓fully proved

Let \(P, Q, T_1, T_2, o\) be pairwise distinct stacks, with unit symbols \(u_P, u_Q, u_{T_1}, u_{T_2}\) for the first four, and let \(ys\) be a list of symbols of stack \(o\). Write \(\mathrm{xfer}(k, ps, \ell, \ell')\) for the transfer loop at label \(\ell\) that pops stack \(k\) until it is empty, pushing \(x\) onto stack \(j\) for each pair \((j, x)\) in \(ps\) per popped symbol, and then goes to \(\ell'\). Let \(r, r_B, \mathit{out}\) map each ordering to a label, with \(\mathit{out}(\mathrm{eq}) = \mathit{next}\) and \(\mathit{out}(\omega) = \mathit{emit}\) for every ordering \(\omega \ne \mathrm{eq}\). Suppose the machine \(M\) has: at label \(\mathit{dec}\) the decrement of \(P\) that goes to \(\mathit{cmp}\) if a symbol was popped and to \(\mathit{ifZero}\) if \(P\) was empty; at label \(\mathit{cmp}\) the comparison round of \(P\) and \(Q\) with scratch stacks \(T_1, T_2\) and units \(u_{T_1}, u_{T_2}\) that repeats at \(\mathit{cmp}\) and exits to \(r(\mathrm{lt})\), \(r(\mathrm{eq})\) and \(r(\mathrm{gt})\); for every ordering \(\omega\), \(M(r(\omega)) = \mathrm{xfer}(T_1, [(P, u_P)], r(\omega), r_B(\omega))\) and \(M(r_B(\omega)) = \mathrm{xfer}(T_2, [(Q, u_Q)], r_B(\omega), \mathit{out}(\omega))\); and at label \(\mathit{emit}\) the statement that prepends \(ys\) to stack \(o\) (so that \(ys\) reads top-down) and goes to \(\mathit{dec}\). Let \(q \in \mathbb{N}\). Then for every \(g \in \mathbb{N}\), every state \(v\) and all stacks \(S\) in which \(P\) holds exactly \(u_P^{q+g+1}\), \(Q\) holds \(u_Q^q\), and \(T_1\) and \(T_2\) are empty, exactly \(g(3q + 6) + 3q + 4\) steps of \(M\) lead from label \(\mathit{dec}\) with state \(v\) and stacks \(S\) to label \(\mathit{next}\) with the state storing the flag false and the stacks \(S\) with \(P\) replaced by \(u_P^q\) and \(o\) replaced by \(g\) copies of \(ys\) concatenated, followed by the old contents of \(o\).

theorem emitDiff_run {P Q T1 T2 o : K} {uP : Γ P} {uQ : Γ Q} {uT1 : Γ T1} {uT2 : Γ T2}
    {ys : List (Γ o)} {dec cmpL emitL ifZero next : Λ} {r rB out : Ordering → Λ}
    (hdec : M dec = decr P ifZero cmpL)
    (hcmp : M cmpL = cmpStep P Q T1 T2 uT1 uT2 cmpL (r .lt) (r .eq) (r .gt))
    (hr : ∀ o, M (r o) = xfer T1 [⟨P, uP⟩] (r o) (rB o))
    (hrB : ∀ o, M (rB o) = xfer T2 [⟨Q, uQ⟩] (rB o) (out o))
    (hout : ∀ o, out o = if o = .eq then next else emitL)
    (hemit : M emitL = emitR o ys dec)
    (hnd : [P, Q, T1, T2, o].Nodup) (q : ℕ) :
    ∀ (gap : ℕ) (v : σ) (S : ∀ k, List (Γ k)), S P = cnt uP (q + gap + 1) → S Q = cnt uQ q →
      S T1 = [] → S T2 = [] →
      Run M (gap * (3 * q + 6) + 3 * q + 4) ⟨some dec, v, S⟩
        ⟨some next, Flag.tag false, update (update S P (cnt uP q)) o (rep ys gap ++ S o)⟩

Uses 12 · Used by 2

Statement usesFlag bit of a machine state · Exact-length runs of a TM2 machine · One round of counter comparison · Unary counter · Decrement · Prepending a constant list · Repeated block · Counter transfer loop

Proof usesA single step executes the statement at the current label · Non-destructive comparison of two counters · Pushing a constant list · Pushing a list of symbols onto one stack

Used byRun of one literal routine (transition-clause generator) · Gap emission in the counter view

DefinitionReachability for a TM2 machine#✓fully proved

For a TM2 machine \(M\) and configurations \(c\) and \(d\), \(d\) is reachable from \(c\) when there is some \(n \in \mathbb{N}\) such that \(M\) runs from \(c\) to \(d\) in exactly \(n\) steps.

def Reach (M : Λ → TM2.Stmt Γ Λ σ) (c d : TM2.Cfg Γ Λ σ) : Prop := ∃ n, Run M n c d

Uses 1 · Used by 2

Statement usesExact-length runs of a TM2 machine

Used byCorrectness of the clause-family generator · A for loop over a counter reaches its exit

TheoremA for loop over a counter reaches its exit#✓fully proved

Let \(M\) be a multi-stack machine whose states carry a flag bit, with \(\mathrm{tag}(\beta)\) the state storing the bit \(\beta\); write \((\ell, v, S)\) for the configuration at label \(\ell\) with state \(v\) and stack contents \(S\), and \(u^m\) for a stack holding exactly \(m\) copies of the symbol \(u\). Let \(c \ne c'\) be stacks with a symbol \(u\) of stack \(c\) and a symbol \(u'\) of stack \(c'\), and let \(h, b, r, e\) be labels such that at \(h\) the machine runs the loop head on \(c\) with index stack \(c'\) (pop \(c\); if a symbol was popped, push \(u'\) onto \(c'\) and go to \(b\), otherwise go to \(r\)), and at \(r\) it runs the transfer that drains \(c'\), pushing one \(u\) onto \(c\) per popped symbol, and then goes to \(e\). Let \(n \in \mathbb{N}\), and let \(P(i, S)\) be a predicate such that \(P(i, S)\) implies \(P(i, S')\) whenever \(S\) and \(S'\) agree on every stack other than \(c\) and \(c'\). Assume that for every \(i < n\) and all stack contents \(S\) with \(S_c = u^{n-1-i}\), \(S_{c'} = u'^{\,i+1}\) and \(P(i, S)\), there are a state \(v'\) and stack contents \(S'\) such that \(M\) goes from \((b, \mathrm{tag}(\mathrm{true}), S)\) to \((h, v', S')\) in finitely many steps, with \(S'_c = S_c\), \(S'_{c'} = S_{c'}\) and \(P(i + 1, S')\). Then for every state \(v\) and all stack contents \(S\) with \(S_c = u^n\), \(S_{c'}\) empty and \(P(0, S)\), there are stack contents \(S'\) such that \(M\) goes from \((h, v, S)\) to \((e, \mathrm{tag}(\mathrm{false}), S')\) in finitely many steps, with \(S'_c = u^n\), \(S'_{c'}\) empty and \(P(n, S')\).

theorem forLoop_reach {c cd : K} {uc : Γ c} {ucd : Γ cd} {head body rest next : Λ}
    (hHead : M head = forHead c cd ucd body rest)
    (hRest : M rest = xfer cd [⟨c, uc⟩] rest next) (hc : c ≠ cd) (n : ℕ)
    (P : ℕ → (∀ k, List (Γ k)) → Prop)
    (hP : ∀ i S S', (∀ k, k ≠ c → k ≠ cd → S' k = S k) → P i S → P i S')
    (hbody : ∀ i < n, ∀ S : ∀ k, List (Γ k), S c = cnt uc (n - 1 - i) → S cd = cnt ucd (i + 1) →
      P i S → ∃ (v' : σ) (S' : ∀ k, List (Γ k)),
        Reach M ⟨some body, Flag.tag true, S⟩ ⟨some head, v', S'⟩ ∧
        S' c = S c ∧ S' cd = S cd ∧ P (i + 1) S')
    (v : σ) (S : ∀ k, List (Γ k)) (hSc : S c = cnt uc n) (hScd : S cd = []) (h0 : P 0 S) :
    ∃ S' : ∀ k, List (Γ k),
      Reach M ⟨some head, v, S⟩ ⟨some next, Flag.tag false, S'⟩ ∧
      S' c = cnt uc n ∧ S' cd = [] ∧ P n S'

Uses 9

Statement usesFlag bit of a machine state · Reachability for a TM2 machine · Unary counter · Loop head of a for loop over a counter · Counter transfer loop

Proof usesExact-length runs of a TM2 machine · A single step executes the statement at the current label · Adding units to target stacks · Running a counter transfer

DefinitionRuns within a step budget#✓fully proved

For a TM2 machine \(M\), a bound \(B \in \mathbb{N}\) and configurations \(c\) and \(d\), \(M\) runs from \(c\) to \(d\) within \(B\) steps when there is some \(n \le B\) such that \(M\) runs from \(c\) to \(d\) in exactly \(n\) steps.

def RunLe (M : Λ → TM2.Stmt Γ Λ σ) (B : ℕ) (c d : TM2.Cfg Γ Λ σ) : Prop :=
  ∃ n, n ≤ B ∧ Run M n c d

Uses 1 · Used by 276

Statement usesExact-length runs of a TM2 machine

Used byReversing and dropping the first bit is polynomial-time · Running the reversal component · The readout on raw bits in polynomial time · The checking machine in polynomial time · The layout in polynomial time · The checking run · The layout run · The readout run · List canonicalizer normalizes a sequence of framed payloads · List canonicalizer normalizes one element · List canonicalizer reaches the decoding outcome with canonical output · Embedded list canonicalizer preserves outside stacks · List canonicalizer fails on malformed input · List canonicalizer runs in linear time on decodable input · Payload normalization is polynomial-time · Linear step bound for the payload normalizer machine · Pair-list projector main loop emits both lists in reverse · Pair-list projector emits one weight and one value frame per item · Pair-list projector always terminates at the decoding outcome · Embedded pair-list projector preserves outside stacks · Pair-list projector fails on malformed input in linear time · Pair-list projector yields canonical weight and value lists · Frame counter yields the number of raw frames in unary · One frame adds one unary count bit · Frame counter decides decodability and counts length in unary · Embedded frame counter preserves caller stacks · Frame counter fails on malformed list framing · Frame counter counts every successfully decoded list of naturals · Four-output decoder reaches exactly the canonical decoding outcome · Embedded four-output decoder preserves outside stacks · Four-output decoder fails on malformed input · Four-output decoder emits four canonical outputs on success · Number normalizer restores its work stacks and prepends its answer · Number-pair projector reaches the decoding outcome · Number-pair projector normalizes both fields of a raw pair frame · Embedded number-pair projector preserves outside stacks · Number-pair projector fails on malformed framing in linear time · Number-pair projector yields both canonical payloads on success · Pair-frame splitter reaches the framing outcome · Raw field projection agrees with the pair decoder · Embedded pair-frame splitter preserves caller stacks · Pair-frame splitter fails on malformed first-field framing · Pair-frame splitter projects every well-framed input in linear time · Framed block reader fails on truncated framing · Converter turns a unary count into a canonical binary frame · Converter turns a unary count into a raw canonical binary payload · Time bound of the accept generator for a concrete machine · Correctness of the accept generator, with its explicit time bound · Polynomial time bound of the accept generator · Run of the accept cell chain · One clause of the accept generator · Run of the code-clause chain of the accept generator · Run of the literal routine of the accept generator · Run of the accept generator's precomputation · One clause of the cell-shift generator · Correctness of the shift generator on one block · Correctness of the shift generator on the situation chain · Correctness of the shift generator on the stack chain of a situation · One literal routine of the cell-shift generator · The literal routines of one clause of the cell-shift generator · One iteration of the overflow loop of the cell-shift generator · The pushed-fill chain of the cell-shift generator · One iteration of the in-range loop of the cell-shift generator · Correctness of the shift generator, with its explicit time bound · Polynomial time bound for the shift generator · One iteration of the time loop of the shift generator · The in-range chain of the cell-shift generator · One phase-loop iteration of the initial-row generator · Run of one clause (initial-row generator) · The I3 loop on the whole input · The I3 loop · Counter part of one I3 iteration · The init generator at the stack cap · Time and output of the init generator for an encoding · Correctness of the init generator, with its explicit time bound · Polynomial time bound for the init generator · Run of one literal routine (initial-row generator) · Run of the literal routines of a clause (initial-row generator) · One phase loop · Run of the precomputation (initial-row generator) · Run of the transition-family generator on one clause · Correctness of the clause-family generator · Correctness of the clause-family generator, with its explicit time bound · Polynomial time bound for the clause-family generator · Run of one literal routine (transition-clause generator) · Run of the literal routines of a clause (transition-clause generator) · One iteration of the time loop · The reduction machine as a polynomial-time computation · One polynomial bounds the reduction machine · The reduction machine halts with the emitted formula · Running a program, then the drain · A bounded halting run certifies the output · A bounded halting run certifies the output, up to an equal output · Time bound of the situation-definition generator on the tables of a machine · Time bound of the shift generator on the tables of a machine · Time bound of the transition-clause generator on the tables of a machine · Generator run for one cell · One clause of the one-hot generator · One stack iteration of the one-hot generator · Run of one literal routine (one-hot generator) · Run of the literal routines of a clause (one-hot generator) · Correctness of the one-hot generator, with its explicit time bound · Polynomial time bound for the one-hot generator · Generator run over one row of at-most-one clauses · Generator run over the first rows and the at-least-one clause · Generator run over one time step · A runtime for loop in the counter view · The assembled generator, after the precomputation · Sequencing · The counter program's run · The composed machine, raw input to formula · Polynomial time bound of the composed machine · The power loop · The precomputation · Clause loop of the clause check · Literal loop of the clause check · The lookup contract · The clause check · The return loop of the lookup machine · Serving a live table entry · One scan step of the lookup · Rejection of the SAT tokenizer within a step bound · One step to rejection · Correctness of the SAT-verifier lookup machine · The scan loop of the lookup machine · Tokenizer run on one clause · Tokenizer rejects undecodable clauses · Tokenizer run on all clauses · Tokenizer rejects an undecodable literal · Tokenizer rejects undecodable literals · Reading the literals of a clause · Rejecting an unterminated name block · Rejecting run · Accepting run of the SAT tokenizer · An unterminated unary count is rejected · Cleanup of the SAT host · Cleanup phase of the SAT verifier host · The embedded lookup meets the lookup contract · The TM2 SAT verifier · Running a sequence of copy sites of the 3-COLOR emitter · Name comparison in the 3-COLOR emitter · The 3-COLOR emitter processes one clause · One step of the walk over earlier occurrences · The emitter on a list of clauses · The emitter processes the remaining literals of a clause · Emitting one literal occurrence · Walking the earlier occurrences · Correctness and step bound of the 3-COLOR emitter · Correctness and running time of the edge loop · Run of the load phase of the 3-COLOR verifier · The unary reader rejects an unterminated number · Correctness and time bound of the 3-coloring verifier machine · The joint walk of the 3-COLOR verifier decides one edge · The walk towards the farther endpoint decides the edge · 3-COLOR is in NP · The 3-COLOR emitter · Run of the load phase · Reading an unterminated unary number rejects · One row of the clique verifier's walk · All rows of the clique verifier's walk · The verifier machine for clique, independent set and vertex cover · Walking the pairs of one row of the clique verifier · Clique emitter: one clause · Clique emitter: comparing two names · Emitter run over a formula's clauses · Emitter run over one literal occurrence · Emitter run over a clause's literals · The CLIQUE emitter computes Karp's instance in cubic time · Walk over the occurrence stack in the CLIQUE emitter · The CLIQUE emitter · CLIQUE ≤ INDEPENDENT-SET is polynomial-time · INDEPENDENT-SET ≤ VERTEX-COVER is polynomial-time · Correctness and running time of the KG-map machine · NP membership from the CLIQUE, INDEPENDENT-SET and VERTEX-COVER verifier · SUBSET-SUM to PARTITION map is polynomial-time · PARTITION to SUBSET-SUM map is polynomial-time · PARTITION doubling pass is polynomial-time · Linear step bound for the PARTITION doubling machine · Quadratic run of the raw-input SUBSET-SUM to PARTITION machine · Quadratic run of the padding machine on canonical instances · Raw-input PARTITION membership machine runs in quadratic time · Canonical PARTITION membership transducer runs in quadratic time · Edge-number phase (SUBSET-SUM reduction machine) · Run of the vertex-number phase of the subset-sum emitter · Binary conversion (SUBSET-SUM reduction machine) · Run of the VERTEX-COVER to SUBSET-SUM machine · The verifier rejects an unterminated chosen block · The verifier rejects a chosen block that ends in false · Adding a canonical chosen block · Comparing the sum with the target · Rejection by the SUBSET-SUM verifier within a step bound · Rejecting in one step · The verifier rejects an unterminated skipped block · The verifier rejects an unterminated target block · The VERTEX-COVER to SUBSET-SUM reduction is polynomial-time · The summing loop of the SUBSET-SUM verifier · The SUBSET-SUM verifier machine · Binary addition of framed numbers in quadratic time · SUBSET-SUM is in NP · SUBSET-SUM verifier computes the mask-selected sum · Embedded SUBSET-SUM summing component reaches the mapped label · Embedded run of the binary addition component · HAMPATH emitter, phase A: searching the variable stack for a name · Comparing a name with the top entry of the variable stack · HAMPATH emitter, phase A: one clause · HAMPATH emitter, phase A: the clauses of a formula · HAMPATH emitter, phase A: one literal · HAMPATH emitter, phase A: the literals of a clause · One clause of the detour walk · Front of a diamond · One literal of the detour walk · The literals of a clause in the detour walk · The row loop of a diamond in the HAMPATH emitter · The detour walk of a diamond in the HAMPATH emitter · Phase A of the HAMPATH emitter · The detours of a diamond · One diamond · The diamonds · The row of a diamond in the HAMPATH emitter · Correctness and running time of the HAMPATH emitter · Run of a HAMPATH-verifier counter comparison · The unary reader of the Hamiltonian path verifier rejects an unterminated number · The edge scan of the Hamiltonian path verifier · The unary mover of the Hamiltonian path verifier rejects an unterminated number · The edge-list check of the Hamiltonian-path verifier · The witness check of the Hamiltonian-path verifier · The HAMPATH emitter · HAMPATH is in NP · Running the head-or-edge check · Running the vertex loop · The repeat scan of the Hamiltonian path verifier · Correctness and running time of the Hamiltonian path verifier · One vertex step of the Hamiltonian-path verifier · The rest of a vertex step in the Hamiltonian-path verifier · A clause with more than three literals makes the capped 3SAT filter fail · The 3SAT emitter processes one clause · A long clause makes the capped 3SAT filter fail on a list of clauses · The SAT-to-3SAT emitter · Emitter · The 3SAT emitter processes a whole formula · Emitter reductions out of SAT are polynomial-time · One literal of the emitter · The capped filter fails on a clause with too many literals · The literals of a clause in the emitter · The SAT-to-3SAT emitter writes the encoded translation in quadratic time · Correctness of the clause-length filter · Tokenize, then emit · The edge loop of a pass · The marking algorithm is polynomial-time · The pass loop of the marking machine · Reading a cut-off unary number · Reading the mark of a vertex · Running time and output of the marking machine · Walking to a vertex and setting its mark · Validation phase of the PATH marking machine · Cleanup empties its stacks · Time bound for a for loop over a counter · Run embedding for bounded runs · Exact matching transports a bounded run · Cleanup in a host · Decider host · Reduction host, canonical form · Verifier host, canonical form · Reduction host · The reduction host's run · The reduction host's run on one input · Verifier host · The verifier host's run · The tape update · The clocked universal machine on stacks · The clocked loop · The clocked universal function is polynomial-time computable · Writing the output · One simulated step, halting case · One simulated step, running case · Correctness and running time of the clocked universal machine

DefinitionBudgeted run#✓fully proved

For a machine \(M\), numbers \(K, X \in \mathbb{N}\) and configurations \(c\) and \(d\), the budgeted run from \(c\) to \(d\) with \(K\) steps already spent and budget \(X\) holds when there is an \(n \in \mathbb{N}\) with \(K + n \le X\) such that \(n\) steps of \(M\) lead from \(c\) to \(d\).

It is used for goal-directed chaining of runs: the chaining lemmas only increase \(K\).

def Bud (M : Λ → TM2.Stmt Γ Λ σ) (K X : ℕ) (c d : TM2.Cfg Γ Λ σ) : Prop :=
  ∃ n, K + n ≤ X ∧ Run M n c d

Uses 1 · Used by 42

Statement usesExact-length runs of a TM2 machine

Used byCorrectness of the accept generator, with its explicit time bound · Run of the accept cell chain · One clause of the accept generator · Run of the code-clause chain of the accept generator · Run of the literal routine of the accept generator · Run of the accept generator's precomputation · One clause of the cell-shift generator · Correctness of the shift generator on one block · Correctness of the shift generator on the situation chain · Correctness of the shift generator on the stack chain of a situation · One literal routine of the cell-shift generator · The literal routines of one clause of the cell-shift generator · One iteration of the overflow loop of the cell-shift generator · The pushed-fill chain of the cell-shift generator · One iteration of the in-range loop of the cell-shift generator · Correctness of the shift generator, with its explicit time bound · One iteration of the time loop of the shift generator · The in-range chain of the cell-shift generator · One phase-loop iteration of the initial-row generator · Run of one clause (initial-row generator) · The I3 loop · Counter part of one I3 iteration · Correctness of the init generator, with its explicit time bound · Run of one literal routine (initial-row generator) · Run of the literal routines of a clause (initial-row generator) · Run of the precomputation (initial-row generator) · Run of the transition-family generator on one clause · Correctness of the clause-family generator, with its explicit time bound · Run of one literal routine (transition-clause generator) · Run of the literal routines of a clause (transition-clause generator) · One iteration of the time loop · Generator run for one cell · One clause of the one-hot generator · One stack iteration of the one-hot generator · Run of one literal routine (one-hot generator) · Run of the literal routines of a clause (one-hot generator) · Correctness of the one-hot generator, with its explicit time bound · Generator run over one row of at-most-one clauses · Generator run over the first rows and the at-least-one clause · Generator run over one time step · Budgeted runs transport along equal counter values · The counter program's run

TheoremTime bound for a for loop over a counter#✓fully proved

Let \(M\) be a multi-stack machine whose states carry a flag bit, with \(\mathrm{tag}(\beta)\) the state storing the bit \(\beta\); write \((\ell, v, S)\) for the configuration at label \(\ell\) with state \(v\) and stack contents \(S\), and \(u^m\) for a stack holding exactly \(m\) copies of the symbol \(u\). Let \(c \ne c'\) be stacks with a symbol \(u\) of stack \(c\) and a symbol \(u'\) of stack \(c'\), and let \(h, b, r, e\) be labels such that at \(h\) the machine runs the loop head on \(c\) with index stack \(c'\) (pop \(c\); if a symbol was popped, push \(u'\) onto \(c'\) and go to \(b\), otherwise go to \(r\)), and at \(r\) it runs the transfer that drains \(c'\), pushing one \(u\) onto \(c\) per popped symbol, and then goes to \(e\). Let \(n \in \mathbb{N}\), let \(B \in \mathbb{N}\), and let \(P(i, S)\) be a predicate such that \(P(i, S)\) implies \(P(i, S')\) whenever \(S\) and \(S'\) agree on every stack other than \(c\) and \(c'\). Assume that for every \(i < n\) and all stack contents \(S\) with \(S_c = u^{n-1-i}\), \(S_{c'} = u'^{\,i+1}\) and \(P(i, S)\), there are a state \(v'\) and stack contents \(S'\) such that \(M\) goes from \((b, \mathrm{tag}(\mathrm{true}), S)\) to \((h, v', S')\) in at most \(B\) steps, with \(S'_c = S_c\), \(S'_{c'} = S_{c'}\) and \(P(i + 1, S')\). Then for every state \(v\) and all stack contents \(S\) with \(S_c = u^n\), \(S_{c'}\) empty and \(P(0, S)\), there are stack contents \(S'\) such that \(M\) goes from \((h, v, S)\) to \((e, \mathrm{tag}(\mathrm{false}), S')\) in at most \(n(B + 1) + n + 2\) steps, with \(S'_c = u^n\), \(S'_{c'}\) empty and \(P(n, S')\).

theorem forLoop_le {c cd : K} {uc : Γ c} {ucd : Γ cd} {head body rest next : Λ}
    (hHead : M head = forHead c cd ucd body rest)
    (hRest : M rest = xfer cd [⟨c, uc⟩] rest next) (hc : c ≠ cd) (n B : ℕ)
    (P : ℕ → (∀ k, List (Γ k)) → Prop)
    (hP : ∀ i S S', (∀ k, k ≠ c → k ≠ cd → S' k = S k) → P i S → P i S')
    (hbody : ∀ i < n, ∀ S : ∀ k, List (Γ k), S c = cnt uc (n - 1 - i) → S cd = cnt ucd (i + 1) →
      P i S → ∃ (v' : σ) (S' : ∀ k, List (Γ k)),
        RunLe M B ⟨some body, Flag.tag true, S⟩ ⟨some head, v', S'⟩ ∧
        S' c = S c ∧ S' cd = S cd ∧ P (i + 1) S')
    (v : σ) (S : ∀ k, List (Γ k)) (hSc : S c = cnt uc n) (hScd : S cd = []) (h0 : P 0 S) :
    ∃ S' : ∀ k, List (Γ k),
      RunLe M (n * (B + 1) + n + 2) ⟨some head, v, S⟩ ⟨some next, Flag.tag false, S'⟩ ∧
      S' c = cnt uc n ∧ S' cd = [] ∧ P n S'

Uses 9 · Used by 2

Statement usesFlag bit of a machine state · Runs within a step budget · Unary counter · Loop head of a for loop over a counter · Counter transfer loop

Proof usesExact-length runs of a TM2 machine · A single step executes the statement at the current label · Adding units to target stacks · Running a counter transfer

Used byCorrectness of the clause-family generator, with its explicit time bound · A runtime for loop in the counter view

DefinitionBit test for the top of a stack#✓fully proved

Let \(d\) be a decoder that reads each symbol either as a bit or as a marker. For an optional symbol \(o\) (the top of a stack, absent when the stack is empty), the test is true when \(o\) is a symbol that \(d\) reads as a bit, and false when \(o\) is absent or \(d\) reads it as a marker.

def isBit {α : Type} (d : α → Option Bool) (o : Option α) : Bool := (o.bind d).isSome

Used by 21

Used byTwo-destination bit-block transfer · Two-destination bit transfer takes one step per bit plus one · Reversed self-delimiting frame emitter · Frame emitter takes one step per payload bit plus one · Machine step reading one framed payload pair · The clause-check driver · Literal loop of the clause check · The tokenizer program · Rejecting an unterminated name block · Reading a name block · Linear step bound for the PARTITION doubling machine · Binary addition of framed numbers in quadratic time · The HAMPATH emitter machine · Moving the tokens back in the HAMPATH emitter · Name copy loop of the 3SAT emitter · The SAT-to-3SAT emitter machine · Bit-block comparison statement · Comparison pops a common prefix · Bit-moving loop · Running the bit-moving loop · The clocked universal program

DefinitionBit on top of a stack#✓fully proved

Let \(d\) be a decoder that reads each symbol either as a bit or as a marker. For an optional symbol \(o\) (the top of a stack, absent when the stack is empty), the bit of \(o\) under \(d\) is \(x\) when \(o\) is a symbol that \(d\) reads as the bit \(x\), and false when \(o\) is absent or \(d\) reads it as a marker.

def bitOf {α : Type} (d : α → Option Bool) (o : Option α) : Bool := (o.bind d).getD false

Used by 69

Used byTwo-destination bit-block transfer · Two-destination bit transfer takes one step per bit plus one · Reversed self-delimiting frame emitter · Frame emitter takes one step per payload bit plus one · Machine step reading one framed payload pair · The tokenizer program · Tokenizer rejects an undecodable literal · Rejecting an unterminated name block · Reading a name block · Load step of the 3-COLOR verifier · Moving one color code in the 3-COLOR verifier · Unary reader of the 3-COLOR verifier · Run of the load phase of the 3-COLOR verifier · The unary reader rejects an unterminated number · The color-moving block rejects on an empty color stack · The joint walk of the 3-COLOR verifier decides one edge · The walk towards the farther endpoint decides the edge · Run of the load phase · Load step of the CLIQUE verifier · The clique verifier's unary reader · Reading an unterminated unary number rejects · All rows of the clique verifier's walk · Walking the pairs of one row of the clique verifier · Walk step of the clique verifier · Rest of a walk step of the clique verifier · Program of the SUBSET-SUM to PARTITION padding machine · Program of the canonical PARTITION membership transducer · Linear step bound for the PARTITION doubling machine · Quadratic run of the raw-input SUBSET-SUM to PARTITION machine · Quadratic run of the padding machine on canonical instances · Raw-input PARTITION membership machine runs in quadratic time · Canonical PARTITION membership transducer runs in quadratic time · The verifier rejects an unterminated chosen block · The verifier rejects a chosen block that ends in false · Adding a canonical chosen block · Adding one payload bit to the sum · Carry phase of the SUBSET-SUM verifier · Carry step of the SUBSET-SUM verifier · Starting the next number · Reading one pair of a block · The verifier rejects an unterminated skipped block · Skipping a number block · The verifier rejects an unterminated target block · Reading the target block · The summing loop of the SUBSET-SUM verifier · Binary addition of framed numbers in quadratic time · SUBSET-SUM verifier computes the mask-selected sum · HAMPATH emitter, phase A: copying a reversed name onto two stacks · The HAMPATH emitter machine · Moving the tokens back in the HAMPATH emitter · Step of the HAMPATH verifier's unary comparison loop · The unary reader of the Hamiltonian path verifier · The unary mover of the Hamiltonian path verifier · The unary reader of the Hamiltonian path verifier rejects an unterminated number · The unary mover of the Hamiltonian path verifier rejects an unterminated number · Reading the mark of vertex \(j\) · The marking machine for PATH · The unary read instruction · Reading a cut-off unary number · Reading the mark of a vertex · Running time and output of the marking machine · A walk step with an exhausted counter · Walking along the marks of the PATH marking machine · Walk step of the PATH marking machine · Bit-block comparison statement · Deciding step of the comparison · Comparison pops a common prefix · Bit-moving loop · Running the bit-moving loop

DefinitionBit blocks#✓fully proved

Let \(d\) be a decoder that reads each symbol either as a bit or as a marker. A list of symbols \(s_1, \dots, s_n\) is the bit block of a bit string \(p\) under \(d\) when \(p\) has the same length \(n\) and, for each \(i\), \(d\) reads \(s_i\) as the \(i\)-th bit of \(p\).

def IsBitBlock {α : Type} (d : α → Option Bool) (xs : List α) (p : List Bool) : Prop :=
  xs.map d = p.map some

Used by 33

Used byThe checking run · The return loop of the lookup machine · Serving a live table entry · One scan step of the lookup · Restoring and stashing after a comparison in the lookup machine · Name comparison in the 3-COLOR emitter · Moving an earlier name from \(D\) to \(E\) · Moving an earlier literal vertex from \(D\) to \(U\) · Moving the current name from \(T\) to \(A\) · Skipping an earlier literal vertex · Recording the current occurrence · Moving a walked name from \(D\) to \(E\) · CLIQUE emitter: reading a variable name · Clique emitter: comparing two names · CLIQUE emitter: putting the current occurrence on the walked stack · Testing a popped input bit · Run of the subset-sum emitter's pair walk · HAMPATH emitter, phase A: searching the variable stack for a name · Comparing a name with the top entry of the variable stack · HAMPATH emitter, phase A: one literal · One literal of the detour walk · End of a diamond · The output phase of the HAMPATH emitter · Comparison pops a common prefix · Correctness of the bit-block comparison · Restoring a stack after a comparison · Running the bit-moving loop · Recovering a bit block from its bits · Moving a bit block through a buffer · The tape update · Reading the input · One simulated step, halting case · One simulated step, running case

DefinitionEnd of a bit block#✓fully proved

Let \(d\) be a decoder that reads each symbol either as a bit or as a marker. A list of symbols \(A\) (the rest of a stack below a block) ends a bit block under \(d\) when \(A\) is empty or \(d\) reads its first symbol as a marker.

def EndsBitBlock {α : Type} (d : α → Option Bool) (A : List α) : Prop := A.head?.bind d = none

Used by 13

Used byBit-block copy keeps the order and restores source and scratch · Two-destination bit transfer takes one step per bit plus one · Frame emitter takes one step per payload bit plus one · The return loop of the lookup machine · Serving a live table entry · One scan step of the lookup · The scan loop of the lookup machine · Restoring and stashing after a comparison in the lookup machine · Correctness of the bit-block comparison · Restoring a stack after a comparison · Running the bit-moving loop · Moving a bit block through a buffer · The tape update

DefinitionBit-moving loop#✓fully proved

For stacks \(a\) and \(b\), a decoder \(d\) reading each symbol of \(a\) as a bit or a marker, an encoder \(g\) from bits to symbols of \(b\), and labels \(\mathit{self}\) and \(\mathit{next}\), the bit-moving loop from \(a\) to \(b\) is the statement that looks at the top of \(a\): if it is a symbol that \(d\) reads as a bit \(x\), it pops it, pushes \(g(x)\) onto \(b\) and goes to \(\mathit{self}\); if it is a marker or \(a\) is empty, it goes to \(\mathit{next}\). It overwrites the state with a flag bit, used as scratch.

def moveB (a b : K) (d : Γ a → Option Bool) (g : Bool → Γ b) (self next : Λ) :
    TM2.Stmt Γ Λ σ :=
  .peek a (fun _ o => Flag.tag (isBit d o))
    (.branch Flag.untag
      (.pop a (fun _ o => Flag.tag (bitOf d o))
        (.branch Flag.untag
          (.push b (fun _ => g true) (.goto fun _ => self))
          (.push b (fun _ => g false) (.goto fun _ => self))))
      (.goto fun _ => next))

Uses 3 · Used by 50

Statement usesFlag bit of a machine state · Bit on top of a stack · Bit test for the top of a stack

Used byProgram of the reversal component · Program of the checking machine · Program of the layout machine · The checking run · Program of the list-of-naturals canonicalizer · Program of the payload normalizer machine · Program of the pair-list projector · Bit-block copy keeps the order and restores source and scratch · Program of the raw pair-frame splitter · Program of the unary-to-binary converter · Converter turns a unary count into a canonical binary frame · Converter turns a unary count into a raw canonical binary payload · The lookup program · Program of the SAT verifier host · The tokenizer embeds in the SAT verifier host · The 3-COLOR emitter machine · The 3-COLOR verifier machine · Program of the clique verifier · The CLIQUE emitter machine · Membership transducer embeds the doubling machine · Padding machine embeds the summation machine · Membership transducer embeds the summation machine · Program of the PARTITION doubling machine · Program of the raw-input SUBSET-SUM to PARTITION machine · Program of the SUBSET-SUM to PARTITION padding machine · Program of the raw-input PARTITION membership machine · Program of the canonical PARTITION membership transducer · Quadratic run of the raw-input SUBSET-SUM to PARTITION machine · Raw-input PARTITION membership machine runs in quadratic time · The subset-sum emitter machine · The SUBSET-SUM verifier program · Binary addition program built on the SUBSET-SUM machine · Binary addition of framed numbers in quadratic time · Comparing a name with the top entry of the variable stack · The HAMPATH emitter machine · Moving a stack of bits · The Hamiltonian path verifier machine · The marking machine for PATH · Restoring the parked marks · Walking to a vertex and setting its mark · Restoring a stack after a comparison · Running the bit-moving loop · Moving a bit block through a buffer · Reduction host program · Verifier host program · Writing the output · Reading the input · The clocked universal program · One simulated step, halting case · One simulated step, running case

TheoremRunning the bit-moving loop#✓fully proved

Let \(a \ne b\) be stacks of a program \(M\) whose state carries a flag bit, \(d\) a decoder reading each symbol of \(a\) as a bit or a marker, \(g\) an encoder from bits to symbols of \(b\), and \(\mathit{self}\), \(\mathit{next}\) labels such that \(M\) runs at \(\mathit{self}\) the bit-moving loop from \(a\) to \(b\) with decoder \(d\) and encoder \(g\), looping at \(\mathit{self}\) and exiting to \(\mathit{next}\). Let \(p = p_1 \cdots p_n\) be a bit list and \(S\) stack contents in which \(a\) holds a bit block for \(p\) under \(d\) followed by a rest \(A\) that ends a bit block under \(d\). Then for every state \(v\) there are a state \(v'\) and stack contents \(S'\) such that \(M\) runs in exactly \(n + 1\) steps from label \(\mathit{self}\), state \(v\) and stacks \(S\) to label \(\mathit{next}\), state \(v'\) and stacks \(S'\), where \(S'(a) = A\), \(S'(b)\) is \(g(p_n), \dots, g(p_1)\) (top first) followed by \(S(b)\), and \(S'(k) = S(k)\) for every other stack \(k\).

theorem moveB_run {self next : Λ} {a b : K} {d : Γ a → Option Bool} {g : Bool → Γ b}
    (hp : M self = moveB a b d g self next) (hab : a ≠ b) :
    ∀ (p : List Bool) (xs A : List (Γ a)) (v : σ) (S : ∀ k, List (Γ k)),
      S a = xs ++ A → IsBitBlock d xs p → EndsBitBlock d A →
      ∃ v' S', Run M (p.length + 1) ⟨some self, v, S⟩ ⟨some next, v', S'⟩ ∧
        S' a = A ∧ S' b = (p.map g).reverse ++ S b ∧ ∀ k, k ≠ a → k ≠ b → S' k = S k

Uses 8 · Used by 52

Statement usesEnd of a bit block · Flag bit of a machine state · Bit blocks · Exact-length runs of a TM2 machine · Bit-moving loop

Proof usesA single step executes the statement at the current label · Bit on top of a stack · Bit test for the top of a stack

Used byRunning the reversal component · The checking run · The layout run · List canonicalizer normalizes one element · List canonicalizer runs in linear time on decodable input · Linear step bound for the payload normalizer machine · Pair-list projector emits one weight and one value frame per item · Pair-list projector fails on malformed input in linear time · Pair-list projector yields canonical weight and value lists · Bit-block copy keeps the order and restores source and scratch · Number normalizer restores its work stacks and prepends its answer · Pair-frame splitter extracts both raw fields · Converter turns a unary count into a raw canonical binary payload · The return loop of the lookup machine · One scan step of the lookup · Restoring and stashing after a comparison in the lookup machine · Phase 0 of the SAT verifier host · Moving an earlier name from \(D\) to \(E\) · Moving an earlier literal vertex from \(D\) to \(U\) · Moving the current name from \(T\) to \(A\) · Skipping an earlier literal vertex · Recording the current occurrence · Restoring the color stack in the 3-COLOR verifier · Correctness and time bound of the 3-coloring verifier machine · One row of the clique verifier's walk · Moving a walked name from \(D\) to \(E\) · CLIQUE emitter: reading a variable name · CLIQUE emitter: putting the current occurrence on the walked stack · Quadratic run of the raw-input SUBSET-SUM to PARTITION machine · Quadratic run of the padding machine on canonical instances · Canonical PARTITION membership transducer runs in quadratic time · Subset-sum emitter: one vertex number · Run of the subset-sum emitter's pair walk · Run of the VERTEX-COVER to SUBSET-SUM machine · Moving the new sum back · Moving the final sum for the comparison · Binary addition of framed numbers in quadratic time · HAMPATH emitter, phase A: searching the variable stack for a name · HAMPATH emitter, phase A: one literal · One literal of the detour walk · End of a diamond · The output phase of the HAMPATH emitter · Moving a stack of bits · The pass loop of the marking machine · Restoring the parked marks · Restoring a stack after a comparison · Moving a bit block through a buffer · The tape update · Writing the output · Reading the input · One simulated step, halting case · One simulated step, running case

DefinitionBit-block comparison statement#✓fully proved

Let \(a\) and \(b\) be stacks with decoders \(d_a\) and \(d_b\) that read each symbol either as a bit or as a marker, let \(t_a\) and \(t_b\) be scratch stacks with bit encoders \(e_a\) and \(e_b\), and let \(\ell\), \(\ell_=\) and \(\ell_{\ne}\) be labels. The comparison statement with loop label \(\ell\) performs one round of comparison: if the tops of \(a\) and \(b\) are the same bit \(x\), it pops both, pushes \(e_a(x)\) onto \(t_a\) and \(e_b(x)\) onto \(t_b\), and goes to \(\ell\). Otherwise it changes no stack: it goes to \(\ell_=\) if neither top is a bit (each of \(a\) and \(b\) is empty or has a marker on top), and to \(\ell_{\ne}\) if the tops are different bits or exactly one of them is a bit. It records its tests in the one-bit flag of the machine state.

MetaMathlibExt.TM2Program.cmpB · 20 lines

def cmpB (a b ta tb : K) (da : Γ a → Option Bool) (db : Γ b → Option Bool)
    (ea : Bool → Γ ta) (eb : Bool → Γ tb) (self eqL neL : Λ) : TM2.Stmt Γ Λ σ :=
  .peek a (fun _ o => Flag.tag (isBit da o))
    (.branch Flag.untag
      (.peek a (fun _ o => Flag.tag (bitOf da o))
        (.branch Flag.untag
          (.peek b (fun _ o => Flag.tag (decide (o.bind db = some true)))
            (.branch Flag.untag
              (.pop a (fun s _ => s) (.pop b (fun s _ => s)
                (.push ta (fun _ => ea true) (.push tb (fun _ => eb true)
                  (.goto fun _ => self)))))
              (.goto fun _ => neL)))
          (.peek b (fun _ o => Flag.tag (decide (o.bind db = some false)))
            (.branch Flag.untag
              (.pop a (fun s _ => s) (.pop b (fun s _ => s)
                (.push ta (fun _ => ea false) (.push tb (fun _ => eb false)
                  (.goto fun _ => self)))))
              (.goto fun _ => neL)))))
      (.peek b (fun _ o => Flag.tag (isBit db o))
        (.branch Flag.untag (.goto fun _ => neL) (.goto fun _ => eqL))))

Uses 3 · Used by 13

Statement usesFlag bit of a machine state · Bit on top of a stack · Bit test for the top of a stack

Used byThe lookup program · The 3-COLOR emitter machine · The CLIQUE emitter machine · Padding machine embeds the summation machine · Membership transducer embeds the summation machine · Program of the raw-input SUBSET-SUM to PARTITION machine · Quadratic run of the raw-input SUBSET-SUM to PARTITION machine · The SUBSET-SUM verifier program · Comparing a name with the top entry of the variable stack · The HAMPATH emitter machine · Deciding step of the comparison · Comparison pops a common prefix · Correctness of the bit-block comparison

StructureFour pairwise distinct stacks#✓fully proved

Four stack indices \(a\), \(b\), \(t_a\), \(t_b\) are pairwise distinct: \(a \ne b\), \(a \ne t_a\), \(a \ne t_b\), \(b \ne t_a\), \(b \ne t_b\) and \(t_a \ne t_b\).

These are the two compared stacks and the two scratch stacks of the bit-block comparison.

structure Distinct4 (a b ta tb : K) : Prop where
  /-- The compared stacks differ. -/
  ab : a ≠ b
  /-- `a` is not the first scratch stack. -/
  ata : a ≠ ta
  /-- `a` is not the second scratch stack. -/
  atb : a ≠ tb
  /-- `b` is not the first scratch stack. -/
  bta : b ≠ ta
  /-- `b` is not the second scratch stack. -/
  btb : b ≠ tb
  /-- The scratch stacks differ. -/
  tatb : ta ≠ tb

Used by 8

Used byServing a live table entry · Name comparison in the 3-COLOR emitter · Clique emitter: comparing two names · Quadratic run of the raw-input SUBSET-SUM to PARTITION machine · Comparing the sum with the target · Comparing a name with the top entry of the variable stack · Comparison pops a common prefix · Correctness of the bit-block comparison

TheoremComparison pops a common prefix#✓fully proved

Suppose the program has at label \(\ell\) the bit-block comparison statement of stacks \(a\) and \(b\) (decoders \(d_a\), \(d_b\)) with scratch stacks \(t_a\) and \(t_b\) (encoders \(e_a\), \(e_b\)) and loop label \(\ell\), and that \(a\), \(b\), \(t_a\), \(t_b\) are pairwise distinct. Let \(p = p_1 \dots p_n\) be a bit string, and take a configuration at label \(\ell\), with any state, in which stack \(a\) holds a list \(X\) on top of \(A\) and stack \(b\) holds a list \(Y\) on top of \(B\), where \(X\) is the bit block \(p\) under \(d_a\) and \(Y\) is the bit block \(p\) under \(d_b\). Then in exactly \(n\) steps the program reaches a configuration at label \(\ell\), with some state, in which stack \(a\) is \(A\), stack \(b\) is \(B\), stack \(t_a\) holds \(e_a(p_n), \dots, e_a(p_1)\) on top of its old contents, stack \(t_b\) holds \(e_b(p_n), \dots, e_b(p_1)\) on top of its old contents, and every other stack is unchanged.

theorem cmpB_prefix (hp : M self = cmpB a b ta tb da db ea eb self eqL neL)
    (hd : Distinct4 a b ta tb) :
    ∀ (p : List Bool) (xs A : List (Γ a)) (ys B : List (Γ b)) (v : σ) (S : ∀ k, List (Γ k)),
      S a = xs ++ A → S b = ys ++ B → IsBitBlock da xs p → IsBitBlock db ys p →
      ∃ v' S', Run M p.length ⟨some self, v, S⟩ ⟨some self, v', S'⟩ ∧
        S' a = A ∧ S' b = B ∧ S' ta = (p.map ea).reverse ++ S ta ∧
        S' tb = (p.map eb).reverse ++ S tb ∧
        ∀ k, k ≠ a → k ≠ b → k ≠ ta → k ≠ tb → S' k = S k

Uses 7 · Used by 2

Statement usesFour pairwise distinct stacks · Flag bit of a machine state · Bit blocks · Exact-length runs of a TM2 machine · Bit-block comparison statement

Proof usesBit on top of a stack · Bit test for the top of a stack

Used byQuadratic run of the raw-input SUBSET-SUM to PARTITION machine · Correctness of the bit-block comparison

TheoremDeciding step of the comparison#✓fully proved

Suppose the program has at label \(\ell\) the bit-block comparison statement of stacks \(a\) and \(b\) (decoders \(d_a\), \(d_b\); scratch stacks arbitrary) with loop label \(\ell\), equality label \(\ell_=\) and mismatch label \(\ell_{\ne}\). From a configuration at label \(\ell\), with any state, in which the tops of \(a\) and \(b\) are not the same bit, the program takes one step to a configuration with the same stacks and some state, at label \(\ell_=\) if neither top is a bit (each of \(a\) and \(b\) is empty or has a marker on top) and at label \(\ell_{\ne}\) otherwise.

theorem cmpB_last (hp : M self = cmpB a b ta tb da db ea eb self eqL neL) (v : σ)
    (S : ∀ k, List (Γ k))
    (h : ¬ ∃ c, (S a).head?.bind da = some c ∧ (S b).head?.bind db = some c) :
    ∃ v', Run M 1 ⟨some self, v, S⟩
      ⟨some (if (S a).head?.bind da = none ∧ (S b).head?.bind db = none then eqL else neL),
        v', S⟩

Uses 5 · Used by 2

Statement usesFlag bit of a machine state · Exact-length runs of a TM2 machine · Bit-block comparison statement

Proof usesA single step executes the statement at the current label · Bit on top of a stack

Used byQuadratic run of the raw-input SUBSET-SUM to PARTITION machine · Correctness of the bit-block comparison

TheoremCorrectness of the bit-block comparison#✓fully proved

Suppose the program has at label \(\ell\) the bit-block comparison statement of stacks \(a\) and \(b\) (decoders \(d_a\), \(d_b\)) with scratch stacks \(t_a\) and \(t_b\) (encoders \(e_a\), \(e_b\)), loop label \(\ell\), equality label \(\ell_=\) and mismatch label \(\ell_{\ne}\), and that \(a\), \(b\), \(t_a\), \(t_b\) are pairwise distinct. Let \(u\) and \(w\) be bit strings, and take a configuration at label \(\ell\), with any state, in which stack \(a\) holds a list \(X\) on top of \(A\) and stack \(b\) holds a list \(Y\) on top of \(B\), where \(X\) is the bit block \(u\) under \(d_a\), \(Y\) is the bit block \(w\) under \(d_b\), \(A\) ends a bit block under \(d_a\) and \(B\) ends a bit block under \(d_b\). Then there is a common prefix \(c = c_1 \dots c_m\) of \(u\) and \(w\), after which \(u\) and \(w\) do not continue with the same bit, such that in exactly \(m + 1\) steps the program reaches a configuration, with some state, at label \(\ell_=\) if \(u = w\) and at label \(\ell_{\ne}\) otherwise, in which stack \(a\) holds \(X\) without its first \(m\) symbols on top of \(A\), stack \(b\) holds \(Y\) without its first \(m\) symbols on top of \(B\), stack \(t_a\) holds \(e_a(c_m), \dots, e_a(c_1)\) on top of its old contents, stack \(t_b\) holds \(e_b(c_m), \dots, e_b(c_1)\) on top of its old contents, and every other stack is unchanged.

theorem cmpB_run (hp : M self = cmpB a b ta tb da db ea eb self eqL neL)
    (hd : Distinct4 a b ta tb) :
    ∀ (u w : List Bool) (xs A : List (Γ a)) (ys B : List (Γ b)) (v : σ) (S : ∀ k, List (Γ k)),
      S a = xs ++ A → S b = ys ++ B → IsBitBlock da xs u → IsBitBlock db ys w → EndsBitBlock da A →
      EndsBitBlock db B →
      ∃ (c : List Bool) (v' : σ) (S' : ∀ k, List (Γ k)), c <+: u ∧ c <+: w ∧
        (∀ bit, (u.drop c.length).head? = some bit → (w.drop c.length).head? ≠ some bit) ∧
        Run M (c.length + 1) ⟨some self, v, S⟩ ⟨some (if u = w then eqL else neL), v', S'⟩ ∧
        S' a = xs.drop c.length ++ A ∧ S' b = ys.drop c.length ++ B ∧
        S' ta = (c.map ea).reverse ++ S ta ∧ S' tb = (c.map eb).reverse ++ S tb ∧
        ∀ k, k ≠ a → k ≠ b → k ≠ ta → k ≠ tb → S' k = S k

Uses 8 · Used by 6

Statement usesFour pairwise distinct stacks · End of a bit block · Flag bit of a machine state · Bit blocks · Exact-length runs of a TM2 machine · Bit-block comparison statement

Proof usesDeciding step of the comparison · Comparison pops a common prefix

Used byServing a live table entry · Name comparison in the 3-COLOR emitter · Clique emitter: comparing two names · Quadratic run of the raw-input SUBSET-SUM to PARTITION machine · Comparing the sum with the target · Comparing a name with the top entry of the variable stack

TheoremRecovering a bit block from its bits#✓fully proved

Let \(d\) be a decoder reading symbols as bits or markers and \(g\) an encoder from bits to symbols such that \(g(b) = x\) whenever \(d\) reads \(x\) as the bit \(b\). If the symbol list \(xs\) is a bit block for the bit list \(u\) under \(d\) and \(c = c_1 \cdots c_m\) is a prefix of \(u\), then the first \(m\) symbols of \(xs\) are \(g(c_1), \dots, g(c_m)\).

theorem IsBitBlock.take_eq_map {α : Type} {d : α → Option Bool} {g : Bool → α}
    (hg : ∀ x b, d x = some b → g b = x) :
    ∀ {xs : List α} {u c : List Bool}, IsBitBlock d xs u → c <+: u → xs.take c.length = c.map g

Uses 1 · Used by 1

Statement usesBit blocks

Used byRestoring a stack after a comparison

TheoremRestoring a stack after a comparison#✓fully proved

Let \(t \ne a\) be stacks with decoders \(d_t\) and \(d_a\) that read each symbol either as a bit or as a marker. Let \(e_t\) be a bit encoder for \(t\) that \(d_t\) reads back (\(d_t\) reads \(e_t(x)\) as the bit \(x\)), and let \(g_a\) be a bit encoder for \(a\) that inverts \(d_a\) (\(g_a(x) = s\) whenever \(d_a\) reads the symbol \(s\) as the bit \(x\)). Suppose the program has at label \(\ell\) the bit-block move statement from \(t\) (decoder \(d_t\)) onto \(a\) (re-encoding \(g_a\)) with loop label \(\ell\) and exit label \(\ell'\). Let \(X\) be the bit block of a bit string \(u\) under \(d_a\) and let \(c = c_1 \dots c_m\) be a prefix of \(u\). From a configuration at label \(\ell\), with any state, in which stack \(t\) holds \(e_t(c_m), \dots, e_t(c_1)\) on top of a list \(R\) that ends a bit block under \(d_t\), and stack \(a\) holds \(X\) without its first \(m\) symbols on top of a list \(A\), the program reaches in exactly \(m + 1\) steps a configuration at label \(\ell'\), with some state, in which stack \(t\) is \(R\), stack \(a\) holds \(X\) on top of \(A\), and every other stack is unchanged.

theorem moveB_restore {t : K} {dt : Γ t → Option Bool} {et : Bool → Γ t} {ga : Bool → Γ a}
    {self' next : Λ} (hp : M self' = moveB t a dt ga self' next) (hta : t ≠ a)
    (hdt : ∀ bit, dt (et bit) = some bit) (hga : ∀ x bit, da x = some bit → ga bit = x)
    (u c : List Bool) (xs A : List (Γ a)) (R : List (Γ t)) (v : σ) (S : ∀ k, List (Γ k))
    (hxs : IsBitBlock da xs u) (hc : c <+: u) (hSt : S t = (c.map et).reverse ++ R)
    (hSa : S a = xs.drop c.length ++ A) (hR : EndsBitBlock dt R) :
    ∃ v' S', Run M (c.length + 1) ⟨some self', v, S⟩ ⟨some next, v', S'⟩ ∧
      S' t = R ∧ S' a = xs ++ A ∧ ∀ k, k ≠ t → k ≠ a → S' k = S k

Uses 7 · Used by 4

Statement usesEnd of a bit block · Flag bit of a machine state · Bit blocks · Exact-length runs of a TM2 machine · Bit-moving loop

Proof usesRecovering a bit block from its bits · Running the bit-moving loop

Used byRestoring and stashing after a comparison in the lookup machine · Name comparison in the 3-COLOR emitter · Clique emitter: comparing two names · Comparing a name with the top entry of the variable stack

DefinitionPopping a list of stacks#✓fully proved

For a list \(ks\) of stacks and a statement \(q\), this is the statement that pops the stacks listed in \(ks\) in order, once per entry (an empty stack stays empty), after each pop replacing the state by the one storing the old flag or-ed with whether that pop found a symbol, and then continues with \(q\).

def popAll : List K → TM2.Stmt Γ Λ σ → TM2.Stmt Γ Λ σ
  | [], q => q
  | k :: ks, q => .pop k (fun s o => Flag.tag (Flag.untag s || o.isSome)) (popAll ks q)

Uses 1 · Used by 2

Statement usesFlag bit of a machine state

Used byCleanup empties its stacks · Cleanup round

DefinitionCleanup round#✓fully proved

For a list \(ks\) of stacks and labels \(\mathit{self}\) and \(\mathit{next}\), the cleanup round is the statement that sets the state to the one storing the flag value false, pops the stacks listed in \(ks\) in order, once per entry (an empty stack stays empty), while recording in the flag whether some pop found a symbol, and then goes to \(\mathit{self}\) if one did and to \(\mathit{next}\) otherwise.

def cleanS (ks : List K) (self next : Λ) : TM2.Stmt Γ Λ σ :=
  .load (fun _ => Flag.tag false) <| popAll ks <|
    .branch Flag.untag (.goto fun _ => self) (.goto fun _ => next)

Uses 2 · Used by 12

Statement usesFlag bit of a machine state · Popping a list of stacks

Used byProgram of the frame counter for lists of naturals · Program of the unary-to-binary converter · Converter turns a unary count into a canonical binary frame · Converter turns a unary count into a raw canonical binary payload · Program of the SAT verifier host · The tokenizer embeds in the SAT verifier host · Binary addition program built on the SUBSET-SUM machine · Binary addition of framed numbers in quadratic time · Cleanup empties its stacks · Cleanup in a host · Reduction host program · Verifier host program

TheoremCleanup empties its stacks#✓fully proved

Let \(ks\) be a list of pairwise distinct stacks of a program \(M\) whose state carries a flag bit, and \(\mathit{self}\), \(\mathit{next}\) labels such that \(M\) runs at \(\mathit{self}\) the cleanup round for \(ks\), looping at \(\mathit{self}\) and exiting to \(\mathit{next}\). Let \(m\) be a natural number and \(S\) stack contents in which every stack of \(ks\) holds at most \(m\) symbols. Then for every state \(v\), \(M\) runs in at most \(m + 1\) steps from label \(\mathit{self}\), state \(v\) and stacks \(S\) to label \(\mathit{next}\), the state storing the flag value false, and the stacks \(S'\) with \(S'(k)\) empty for every \(k\) in \(ks\) and \(S'(k) = S(k)\) for every other stack \(k\).

theorem clean_run {M : Λ → TM2.Stmt Γ Λ σ} {ks : List K} {self next : Λ}
    (hM : M self = cleanS ks self next) (hks : ks.Nodup) :
    ∀ (m : ℕ) (v : σ) (S : ∀ k, List (Γ k)), (∀ k ∈ ks, (S k).length ≤ m) →
      RunLe M (m + 1) ⟨some self, v, S⟩
        ⟨some next, Flag.tag false, fun k => if k ∈ ks then [] else S k⟩

Uses 6 · Used by 6

Statement usesFlag bit of a machine state · Runs within a step budget · Cleanup round

Proof usesExact-length runs of a TM2 machine · A single step executes the statement at the current label · Popping a list of stacks

Used byOne frame adds one unary count bit · Converter turns a unary count into a canonical binary frame · Converter turns a unary count into a raw canonical binary payload · Cleanup of the SAT host · Binary addition of framed numbers in quadratic time · Cleanup in a host

StructureStack embedding#✓fully proved

Given a family of stack alphabets \(\Gamma\) indexed by the stacks \(K\) of a sub-machine and a family \(\Gamma'\) indexed by the stacks \(K'\) of a host, a stack embedding consists of an injective map \(e : K \to K'\) renaming the stacks together with, for each stack \(k \in K\), a bijection \(\iota_k : \Gamma_k \to \Gamma'_{e(k)}\) from the alphabet of \(k\) onto the alphabet of its image.

structure SEmb {K K' : Type} (Γ : K → Type) (Γ' : K' → Type) where
  /-- The stack renaming. -/
  e : K → K'
  /-- Distinct sub-machine stacks go to distinct host stacks. -/
  inj : Injective e
  /-- The alphabet of each sub-machine stack, identified with its host stack's. -/
  ι : ∀ k, Γ k ≃ Γ' (e k)

Used by 74

Used byMapping the first component of a pair is polynomial-time · List canonicalizer normalizes one element · Stack embedding of the number normalizer in the list canonicalizer · Embedded list canonicalizer preserves outside stacks · Pair-list projector emits one weight and one value frame per item · Stack embedding of the pair normalizer in the pair-list projector · Embedded pair-list projector preserves outside stacks · Pair-list projector fails on malformed input in linear time · Embedded frame counter preserves caller stacks · List-projector stack embedding in the four-output decoder · Final pair-projector stack embedding in the four-output decoder · Embedded four-output decoder preserves outside stacks · Four-output decoder fails on malformed input · Four-output decoder emits four canonical outputs on success · Outer-splitter stack embedding in the four-output decoder · Field-normalizer stack embedding in the number-pair projector · Pair-frame splitter stack embedding in the number-pair projector · Number-pair projector normalizes both fields of a raw pair frame · Embedded number-pair projector preserves outside stacks · Number-pair projector fails on malformed framing in linear time · Embedded pair-frame splitter preserves caller stacks · Emitter stack embedding in the unary-to-binary converter · Converter turns a unary count into a canonical binary frame · Converter turns a unary count into a raw canonical binary payload · The counter stacks inside the generator's stacks · Run lifting · Running a program, then the drain · The identity stack embedding · Embedding of the accept generator into the host · Embedding of the shift generator into the host · Embedding of the init generator into the host · Embedding of the situation-definition generator into the host · Embedding of the update generator's stacks into the host · Sequencing · Embedding of the counter program's stacks · Embedding of the host's stacks · The composed machine, raw input to formula · The precomputation · Stack embedding of the clause-check driver into the host · Stack embedding of the clause-length filter into the host · Stack embedding of the lookup into the clause-check driver · Stack embedding of the tokenizer into the host · The embedded lookup meets the lookup contract · The TM2 SAT verifier · Numeric-core workspace of the raw-input PARTITION membership machine · Doubling-machine stack embedding in the membership transducer · Normalizer workspace of the raw-input PARTITION membership machine · Program of the raw-input SUBSET-SUM to PARTITION machine · Quadratic run of the raw-input SUBSET-SUM to PARTITION machine · Quadratic run of the padding machine on canonical instances · Raw-input PARTITION membership machine runs in quadratic time · Canonical PARTITION membership transducer runs in quadratic time · Summation-machine stack embedding in the padding machine · Summation-machine stack embedding in the membership transducer · Identity embedding of the verifier stacks · Binary addition of framed numbers in quadratic time · Embedded SUBSET-SUM summing component reaches the mapped label · Embedded run of the binary addition component · Embedding the emitter's stacks into tokenize-then-emit · Embedding the tokenizer's stacks into tokenize-then-emit · Tokenize, then emit · Agreement of host and sub-machine stacks · Embedding of a machine in a host · Frame condition for a stack embedding · Translating a statement along a stack embedding · Run embedding · Exact program matching transports a run with its step count · Exact run transport to supplied host final stacks · Run embedding for bounded runs · Exact matching transports a bounded run · Executing a translated statement · Agreement with the embedded component · The component's stacks inside a host · The verifier host's run

DefinitionTranslating a statement along a stack embedding#✓fully proved

Let \(E\) be a stack embedding with stack renaming \(e\) and alphabet bijections \(\iota_k\), and let \(\varphi\) map the sub-machine's labels to the host's labels. The translation of a sub-machine statement is the host statement obtained recursively, where \(s\) denotes the current state. A push of the symbol \(f(s)\) on stack \(k\) becomes a push of \(\iota_k(f(s))\) on stack \(e(k)\). A peek or pop on stack \(k\) becomes a peek or pop on stack \(e(k)\) whose result is mapped back by \(\iota_k^{-1}\) before the state update. A jump to label \(f(s)\) becomes a jump to \(\varphi(f(s))\). State updates, branches and halt are kept, with their sub-statements translated.

def mapS : TM2.Stmt Γ Λ σ → TM2.Stmt Γ' Λ' σ
  | .push k f q => .push (E.e k) (fun s => E.ι k (f s)) (mapS q)
  | .peek k f q => .peek (E.e k) (fun s o => f s (o.map (E.ι k).symm)) (mapS q)
  | .pop k f q => .pop (E.e k) (fun s o => f s (o.map (E.ι k).symm)) (mapS q)
  | .load a q => .load a (mapS q)
  | .branch f q₁ q₂ => .branch f (mapS q₁) (mapS q₂)
  | .goto f => .goto fun s => φ (f s)
  | .halt => .halt

Uses 1 · Used by 53

Statement usesStack embedding

Used byMapping the first component of a pair is polynomial-time · List canonicalizer normalizes one element · Program of the list-of-naturals canonicalizer · Pair-list projector emits one weight and one value frame per item · Program of the pair-list projector · Pair-list projector fails on malformed input in linear time · Program of the four-output pair-list decoder · Four-output decoder fails on malformed input · Four-output decoder emits four canonical outputs on success · Program of the number-pair projector · Number-pair projector normalizes both fields of a raw pair frame · Number-pair projector fails on malformed framing in linear time · Program of the unary-to-binary converter · Converter turns a unary count into a canonical binary frame · Converter turns a unary count into a raw canonical binary payload · The I3 loop · Correctness of the init generator, with its explicit time bound · The initial-row generator · Running a program, then the drain · The composed program · The host program · Sequencing · The full program · The composed machine, raw input to formula · The precomputation · Program of the SAT verifier host · The embedded lookup program · The tokenizer embeds in the SAT verifier host · The embedded lookup meets the lookup contract · The TM2 SAT verifier · Membership transducer embeds the doubling machine · Padding machine embeds the summation machine · Membership transducer embeds the summation machine · Program of the raw-input SUBSET-SUM to PARTITION machine · Program of the SUBSET-SUM to PARTITION padding machine · Program of the raw-input PARTITION membership machine · Program of the canonical PARTITION membership transducer · Quadratic run of the raw-input SUBSET-SUM to PARTITION machine · Raw-input PARTITION membership machine runs in quadratic time · Binary addition program built on the SUBSET-SUM machine · Binary addition of framed numbers in quadratic time · Program of the tokenize-then-emit machine · Tokenize, then emit · Embedding of a machine in a host · Run embedding · Exact program matching transports a run with its step count · Exact run transport to supplied host final stacks · Exact matching transports a bounded run · Executing a translated statement · The reduction host embeds the component · The verifier host embeds the component · Reduction host program · Verifier host program

DefinitionEmbedding of a machine in a host#✓fully proved

Let \(E\) be a stack embedding and \(\varphi\) a map from the labels of a machine \(M\) to the labels of a host machine \(M'\) over the same internal states. Then \(M\) embeds in \(M'\) along \(E\) and \(\varphi\) when, for every label \(\ell\) of \(M\), either the statement of \(M'\) at \(\varphi(\ell)\) is the statement of \(M\) at \(\ell\) translated along \(E\) and \(\varphi\), or the statement of \(M\) at \(\ell\) is the halt statement (in which case \(M'\) may do anything at \(\varphi(\ell)\)).

def Embeds (M : Λ → TM2.Stmt Γ Λ σ) (M' : Λ' → TM2.Stmt Γ' Λ' σ) : Prop :=
  ∀ l, M' (φ l) = mapS E φ (M l) ∨ M l = .halt

Uses 2 · Used by 38

Statement usesStack embedding · Translating a statement along a stack embedding

Used byList canonicalizer normalizes one element · Embedded list canonicalizer preserves outside stacks · Pair-list projector emits one weight and one value frame per item · Embedded pair-list projector preserves outside stacks · Pair-list projector fails on malformed input in linear time · Embedded frame counter preserves caller stacks · Embedded four-output decoder preserves outside stacks · Four-output decoder fails on malformed input · Four-output decoder emits four canonical outputs on success · Number-pair projector normalizes both fields of a raw pair frame · Embedded number-pair projector preserves outside stacks · Number-pair projector fails on malformed framing in linear time · Embedded pair-frame splitter preserves caller stacks · Converter turns a unary count into a canonical binary frame · Converter turns a unary count into a raw canonical binary payload · The I3 loop · Correctness of the init generator, with its explicit time bound · Run lifting · Running a program, then the drain · Sequencing · The composed machine, raw input to formula · The precomputation · The tokenizer embeds in the SAT verifier host · The embedded lookup meets the lookup contract · The TM2 SAT verifier · Membership transducer embeds the doubling machine · Padding machine embeds the summation machine · Membership transducer embeds the summation machine · Quadratic run of the raw-input SUBSET-SUM to PARTITION machine · Raw-input PARTITION membership machine runs in quadratic time · Binary addition of framed numbers in quadratic time · Embedded SUBSET-SUM summing component reaches the mapped label · Embedded run of the binary addition component · Tokenize, then emit · Run embedding · Run embedding for bounded runs · The reduction host embeds the component · The verifier host embeds the component

DefinitionAgreement of host and sub-machine stacks#✓fully proved

Let \(E\) be a stack embedding with stack renaming \(e\) and alphabet bijections \(\iota_k\). Stack contents \(S\) of the sub-machine and \(S'\) of the host agree when, for every sub-machine stack \(k\), the host stack \(e(k)\) holds the list obtained from \(S(k)\) by applying \(\iota_k\) to each symbol.

def Agree (S : ∀ k, List (Γ k)) (S' : ∀ k', List (Γ' k')) : Prop :=
  ∀ k, S' (E.e k) = (S k).map (E.ι k)

Uses 1 · Used by 39

Statement usesStack embedding

Used byList canonicalizer normalizes one element · Embedded list canonicalizer preserves outside stacks · Pair-list projector emits one weight and one value frame per item · Embedded pair-list projector preserves outside stacks · Pair-list projector fails on malformed input in linear time · Embedded frame counter preserves caller stacks · Embedded four-output decoder preserves outside stacks · Four-output decoder fails on malformed input · Four-output decoder emits four canonical outputs on success · Number-pair projector normalizes both fields of a raw pair frame · Embedded number-pair projector preserves outside stacks · Number-pair projector fails on malformed framing in linear time · Embedded pair-frame splitter preserves caller stacks · Converter turns a unary count into a canonical binary frame · Converter turns a unary count into a raw canonical binary payload · Run lifting · Running a program, then the drain · Sequencing · The composed machine, raw input to formula · The precomputation · The embedded lookup meets the lookup contract · The TM2 SAT verifier · Quadratic run of the raw-input SUBSET-SUM to PARTITION machine · Quadratic run of the padding machine on canonical instances · Raw-input PARTITION membership machine runs in quadratic time · Canonical PARTITION membership transducer runs in quadratic time · Binary addition of framed numbers in quadratic time · Embedded SUBSET-SUM summing component reaches the mapped label · Embedded run of the binary addition component · Tokenize, then emit · Run embedding · Exact program matching transports a run with its step count · Exact run transport to supplied host final stacks · Run embedding for bounded runs · Exact matching transports a bounded run · Executing a translated statement · Agreement with the embedded component · The reduction host's run on one input · The verifier host's run

DefinitionFrame condition for a stack embedding#✓fully proved

Let \(E\) be a stack embedding with stack renaming \(e\). Two contents \(S'\) and \(S''\) of the host's stacks satisfy the frame condition when every host stack \(k'\) outside the image of \(e\) has the same contents in both: \(S''(k') = S'(k')\) whenever \(e(k) \ne k'\) for every sub-machine stack \(k\).

def Frame (S' S'' : ∀ k', List (Γ' k')) : Prop :=
  ∀ k', (∀ k, E.e k ≠ k') → S'' k' = S' k'

Uses 1 · Used by 38

Statement usesStack embedding

Used byList canonicalizer normalizes one element · Embedded list canonicalizer preserves outside stacks · Pair-list projector emits one weight and one value frame per item · Embedded pair-list projector preserves outside stacks · Pair-list projector fails on malformed input in linear time · Embedded frame counter preserves caller stacks · Embedded four-output decoder preserves outside stacks · Four-output decoder fails on malformed input · Four-output decoder emits four canonical outputs on success · Number-pair projector normalizes both fields of a raw pair frame · Embedded number-pair projector preserves outside stacks · Number-pair projector fails on malformed framing in linear time · Embedded pair-frame splitter preserves caller stacks · Converter turns a unary count into a canonical binary frame · Converter turns a unary count into a raw canonical binary payload · Run lifting · Running a program, then the drain · Sequencing · The composed machine, raw input to formula · The precomputation · The embedded lookup meets the lookup contract · The TM2 SAT verifier · Quadratic run of the raw-input SUBSET-SUM to PARTITION machine · Quadratic run of the padding machine on canonical instances · Raw-input PARTITION membership machine runs in quadratic time · Canonical PARTITION membership transducer runs in quadratic time · Binary addition of framed numbers in quadratic time · Embedded SUBSET-SUM summing component reaches the mapped label · Embedded run of the binary addition component · Tokenize, then emit · Run embedding · Exact program matching transports a run with its step count · Exact run transport to supplied host final stacks · Run embedding for bounded runs · Exact matching transports a bounded run · Executing a translated statement · The reduction host's run on one input · The verifier host's run

TheoremExecuting a translated statement#✓fully proved

Let \(E\) be a stack embedding with stack renaming \(e\), and let \(\varphi\) map sub-machine labels to host labels. Let \(q\) be a sub-machine statement, \(v\) a state, \(S\) sub-machine stacks and \(S'\) host stacks that agree with \(S\). Let executing \(q\) from state \(v\) and stacks \(S\) yield the next label \(\ell\) (possibly none), state \(w\) and stacks \(T\). Then there are host stacks \(T'\) such that executing the translation of \(q\) along \(E\) and \(\varphi\) from state \(v\) and stacks \(S'\) yields the next label \(\varphi(\ell)\) (none if \(\ell\) is none), state \(w\) and stacks \(T'\). Moreover \(T'\) agrees with \(T\), and \(S'\), \(T'\) satisfy the frame condition.

theorem stepAux_mapS (q : TM2.Stmt Γ Λ σ) (v : σ) (S : ∀ k, List (Γ k)) (S' : ∀ k', List (Γ' k'))
    (hA : Agree E S S') :
    ∃ T' : ∀ k', List (Γ' k'),
      TM2.stepAux (mapS E φ q) v S' =
        ⟨(TM2.stepAux q v S).l.map φ, (TM2.stepAux q v S).var, T'⟩ ∧
      Agree E (TM2.stepAux q v S).stk T' ∧ Frame E S' T'

Uses 4 · Used by 2

Statement usesAgreement of host and sub-machine stacks · Frame condition for a stack embedding · Stack embedding · Translating a statement along a stack embedding

Used byRun embedding · Exact program matching transports a run with its step count

TheoremRun embedding#✓fully proved

Let \(E\) be a stack embedding with stack renaming \(e\), let \(\varphi\) map the labels of a machine \(M\) to those of a host machine \(M'\), and suppose \(M\) embeds in \(M'\) along \(E\) and \(\varphi\). Suppose \(M\) goes in exactly \(n\) steps from label \(\ell\), state \(v\) and stacks \(S\) to a live label \(\ell'\), state \(v'\) and stacks \(T\), where the start may also be the halted configuration with no label (whose image under \(\varphi\) again has no label). If host stacks \(S'\) agree with \(S\), then there are host stacks \(T'\) such that \(M'\) goes in exactly \(n\) steps from label \(\varphi(\ell)\), state \(v\) and stacks \(S'\) to label \(\varphi(\ell')\), state \(v'\) and stacks \(T'\). Moreover \(T'\) agrees with \(T\), and \(S'\), \(T'\) satisfy the frame condition: host stacks outside the image of \(e\) are unchanged.

theorem run_embed {M : Λ → TM2.Stmt Γ Λ σ} {M' : Λ' → TM2.Stmt Γ' Λ' σ} (hM : Embeds E φ M M') :
    ∀ (n : ℕ) (l : Option Λ) (v : σ) (S : ∀ k, List (Γ k)) (l' : Λ) (v' : σ)
      (T : ∀ k, List (Γ k)) (S' : ∀ k', List (Γ' k')),
      Run M n ⟨l, v, S⟩ ⟨some l', v', T⟩ → Agree E S S' →
      ∃ T' : ∀ k', List (Γ' k'),
        Run M' n ⟨l.map φ, v, S'⟩ ⟨some (φ l'), v', T'⟩ ∧ Agree E T T' ∧ Frame E S' T'

Uses 8 · Used by 5

Statement usesAgreement of host and sub-machine stacks · Embedding of a machine in a host · Frame condition for a stack embedding · Stack embedding · Exact-length runs of a TM2 machine

Proof usesTranslating a statement along a stack embedding · Executing a translated statement · A halted run stays halted

Used byFour-output decoder fails on malformed input · Four-output decoder emits four canonical outputs on success · Number-pair projector normalizes both fields of a raw pair frame · Run lifting · Run embedding for bounded runs

TheoremRun embedding for bounded runs#✓fully proved

Let \(E\) be a stack embedding with stack renaming \(e\), let \(\varphi\) map the labels of a machine \(M\) to those of a host machine \(M'\), and suppose \(M\) embeds in \(M'\) along \(E\) and \(\varphi\). Suppose \(M\) goes in at most \(B\) steps from label \(\ell\), state \(v\) and stacks \(S\) to label \(\ell'\), state \(v'\) and stacks \(T\), and host stacks \(S'\) agree with \(S\). Then there are host stacks \(T'\) such that \(M'\) goes in at most \(B\) steps from label \(\varphi(\ell)\), state \(v\) and stacks \(S'\) to label \(\varphi(\ell')\), state \(v'\) and stacks \(T'\). Moreover \(T'\) agrees with \(T\), and \(S'\), \(T'\) satisfy the frame condition: host stacks outside the image of \(e\) are unchanged.

theorem runLe_embed {M : Λ → TM2.Stmt Γ Λ σ} {M' : Λ' → TM2.Stmt Γ' Λ' σ} (hM : Embeds E φ M M')
    {B : ℕ} {l : Λ} {v : σ} {S : ∀ k, List (Γ k)} {l' : Λ} {v' : σ} {T : ∀ k, List (Γ k)}
    {S' : ∀ k', List (Γ' k')} (h : RunLe M B ⟨some l, v, S⟩ ⟨some l', v', T⟩) (hA : Agree E S S') :
    ∃ T' : ∀ k', List (Γ' k'),
      RunLe M' B ⟨some (φ l), v, S'⟩ ⟨some (φ l'), v', T'⟩ ∧ Agree E T T' ∧ Frame E S' T'

Uses 7 · Used by 30

Statement usesAgreement of host and sub-machine stacks · Embedding of a machine in a host · Frame condition for a stack embedding · Stack embedding · Runs within a step budget

Proof usesRun embedding · Exact-length runs of a TM2 machine

Used byList canonicalizer normalizes one element · Embedded list canonicalizer preserves outside stacks · Pair-list projector emits one weight and one value frame per item · Embedded pair-list projector preserves outside stacks · Pair-list projector fails on malformed input in linear time · Embedded frame counter preserves caller stacks · Embedded four-output decoder preserves outside stacks · Four-output decoder fails on malformed input · Four-output decoder emits four canonical outputs on success · Number-pair projector normalizes both fields of a raw pair frame · Embedded number-pair projector preserves outside stacks · Number-pair projector fails on malformed framing in linear time · Embedded pair-frame splitter preserves caller stacks · Converter turns a unary count into a canonical binary frame · Converter turns a unary count into a raw canonical binary payload · Running a program, then the drain · Sequencing · The composed machine, raw input to formula · The precomputation · The embedded lookup meets the lookup contract · The TM2 SAT verifier · Quadratic run of the raw-input SUBSET-SUM to PARTITION machine · Raw-input PARTITION membership machine runs in quadratic time · Canonical PARTITION membership transducer runs in quadratic time · Binary addition of framed numbers in quadratic time · Embedded SUBSET-SUM summing component reaches the mapped label · Embedded run of the binary addition component · Tokenize, then emit · The reduction host's run on one input · The verifier host's run

TheoremExact program matching transports a run with its step count#✓fully proved

Exact program matching transports a run, including a halted endpoint, while preserving the local state, embedded stacks, untouched host stacks, and exact number of steps.

theorem run_embed_exact (hM : ∀ l, M' (φ l) = mapS E φ (M l))
    {n : ℕ} {l l' : Option Λ} {v v' : σ}
    {S T : ∀ k, List (Γ k)} {S' : ∀ k', List (Γ' k')}
    (h : Run M n ⟨l, v, S⟩ ⟨l', v', T⟩) (hA : Agree E S S') :
    ∃ T', Run M' n ⟨l.map φ, v, S'⟩ ⟨l'.map φ, v', T'⟩ ∧
      Agree E T T' ∧ Frame E S' T'

Uses 7 · Used by 2

Statement usesAgreement of host and sub-machine stacks · Frame condition for a stack embedding · Stack embedding · Translating a statement along a stack embedding · Exact-length runs of a TM2 machine

Proof usesExecuting a translated statement · A halted run stays halted

Used byExact run transport to supplied host final stacks · Exact matching transports a bounded run

TheoremExact run transport to supplied host final stacks#✓fully proved

Source-shaped transport to supplied host final stacks: agreement fixes embedded slots and the frame condition fixes every other slot, so the host endpoint is exact.

theorem run_embed_exact_of_agree_frame (hM : ∀ l, M' (φ l) = mapS E φ (M l))
    {n : ℕ} {l l' : Option Λ} {v v' : σ}
    {S T : ∀ k, List (Γ k)} {S' T' : ∀ k', List (Γ' k')}
    (h : Run M n ⟨l, v, S⟩ ⟨l', v', T⟩) (hA : Agree E S S')
    (hT : Agree E T T') (hF : Frame E S' T') :
    Run M' n ⟨l.map φ, v, S'⟩ ⟨l'.map φ, v', T'⟩

Uses 6 · Used by 1

Statement usesAgreement of host and sub-machine stacks · Frame condition for a stack embedding · Stack embedding · Translating a statement along a stack embedding · Exact-length runs of a TM2 machine

Proof usesExact program matching transports a run with its step count

Used byMapping the first component of a pair is polynomial-time

TheoremExact matching transports a bounded run#✓fully proved

Exact matching transports a bounded run with arbitrary optional endpoints, retaining the same step witness and budget as well as agreement and the host frame.

theorem runLe_embed_exact (hM : ∀ l, M' (φ l) = mapS E φ (M l))
    {B : ℕ} {l l' : Option Λ} {v v' : σ}
    {S T : ∀ k, List (Γ k)} {S' : ∀ k', List (Γ' k')}
    (h : RunLe M B ⟨l, v, S⟩ ⟨l', v', T⟩) (hA : Agree E S S') :
    ∃ T', RunLe M' B ⟨l.map φ, v, S'⟩ ⟨l'.map φ, v', T'⟩ ∧
      Agree E T T' ∧ Frame E S' T'

Uses 7

Statement usesAgreement of host and sub-machine stacks · Frame condition for a stack embedding · Stack embedding · Translating a statement along a stack embedding · Runs within a step budget

Proof usesExact program matching transports a run with its step count · Exact-length runs of a TM2 machine

59 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.