Start label of the lookup machine to Reading a unary count

DefinitionStart label of the lookup machine#✓fully proved

The lookup program starts at its initialization label \(\mathsf{init}\).

def start : Lab := .init
Uses 1 · Used by 5
Statement usesLabels of the lookup machine
Used byCorrectness of the SAT-verifier lookup machine · Program of the SAT verifier host · The tokenizer embeds in the SAT verifier host · The embedded lookup meets the lookup contract · The TM2 SAT verifier

DefinitionStack contents of the lookup machine#✓fully proved

For lists of symbols \(t\), \(b\), \(s\), \(a\), \(c\), \(v\), the assignment of contents to the six stacks of the lookup machine that gives \(T\) the list \(t\), \(B\) the list \(b\), \(S\) the list \(s\), \(A\) the list \(a\), \(C\) the list \(c\) and \(V\) the list \(v\).

def stk (t b s a c v : List Sym) : ∀ _ : K, List Sym
  | .T => t
  | .B => b
  | .S => s
  | .A => a
  | .C => c
  | .V => v
Uses 2 · Used by 7
Statement usesStacks of the lookup machine · Stack alphabet of the SAT verifier
Used byThe return loop of the lookup machine · Serving a live table entry · One scan step of the lookup · Initialization step of the lookup machine · Correctness of the SAT-verifier lookup machine · The scan loop of the lookup machine · Restoring and stashing after a comparison in the lookup machine

TheoremA name bit reads as itself#✓fully proved

For every bit \(b\), the name-bit symbol for \(b\) reads as the bit \(b\).

theorem bit?_bit (b : Bool) : Sym.bit? (.bit b) = some b
Uses 2 · Used by 1
Statement usesStack alphabet of the SAT verifier · Reading a symbol as a name bit
Used byRestoring and stashing after a comparison in the lookup machine

TheoremInitialization step of the lookup machine#✓fully proved

Let \(t\) and \(b\) be lists of symbols and \(v\) a bit. In exactly one step, the lookup program goes from the label \(\mathsf{init}\) with internal bit \(v\), stack \(T\) holding \(t\), stack \(B\) holding \(b\) and the stacks \(S\), \(A\), \(C\), \(V\) empty, to the label \(\mathsf{scan}\) with internal bit \(v\), the same contents of \(T\), \(B\), \(S\), \(A\) and \(C\), and stack \(V\) holding the single symbol name bit false.

theorem init_run (t b : List Sym) (v : Bool) :
    Run prog 1 ⟨some .init, v, stk t b [] [] [] []⟩
      ⟨some .scan, v, stk t b [] [] [] [Sym.bit false]⟩
Uses 7 · Used by 1
Statement usesStacks of the lookup machine · Labels of the lookup machine · The lookup program · Stack contents of the lookup machine · Stack alphabet of the SAT verifier · Exact-length runs of a TM2 machine
Proof usesA single step executes the statement at the current label
Used byCorrectness of the SAT-verifier lookup machine

TheoremRestoring and stashing after a comparison in the lookup machine#✓fully proved

Let \(q\), \(n\), \(c\) be lists of bits such that \(c\) is a prefix of both the reverse of \(q\) and the reverse of \(n\); let \(R\), \(r\), \(s\), \(w\) be lists of symbols with \(r\) empty or starting with a symbol other than a name bit; and for a list of bits \(x\) write \(\bar x\) for the list of its bits as name bits. Suppose the lookup program is at label \(\mathsf{rstT}\), with any internal bit, and its stacks are: \(T\) holds the reverse of \(\bar q\) with its first \(|c|\) symbols removed, followed by \(R\); \(B\) holds the reverse of \(\bar n\) with its first \(|c|\) symbols removed, followed by \(r\); \(S\) holds \(s\); \(A\) and \(C\) both hold the reverse of \(\bar c\); and \(V\) holds \(w\). Then after exactly \(2(|c| + 1) + (|n| + 1)\) steps the program is at label \(\mathsf{scan}\), with some internal bit, where \(T\) holds the reverse of \(\bar q\) followed by \(R\), \(B\) holds \(r\), \(S\) holds \(\bar n\) followed by \(s\), \(A\) and \(C\) are empty, and \(V\) holds \(w\).

theorem tail_run (q n c : List Bool) (hcq : c <+: q.reverse) (hcn : c <+: n.reverse)
    (R r s w : List Sym) (hr : EndsBitBlock Sym.bit? r) (v : Bool) :
    ∃ v', Run prog (2 * (c.length + 1) + (n.length + 1))
      ⟨some .rstT, v, stk (((q.map Sym.bit).reverse).drop c.length ++ R)
        (((n.map Sym.bit).reverse).drop c.length ++ r) s (c.map Sym.bit).reverse
        (c.map Sym.bit).reverse w⟩
      ⟨some .scan, v', stk ((q.map Sym.bit).reverse ++ R) r (n.map Sym.bit ++ s) [] [] w⟩
Uses 13 · Used by 1
Statement usesStacks of the lookup machine · Labels of the lookup machine · The lookup program · Stack contents of the lookup machine · Stack alphabet of the SAT verifier · Reading a symbol as a name bit · End of a bit block · Exact-length runs of a TM2 machine
Proof usesA name bit reads as itself · Flag bit of a machine state · Bit blocks · Restoring a stack after a comparison · Running the bit-moving loop
Used byServing a live table entry

TheoremServing a live table entry#✓fully proved

Write stack contents top first, and for a list of bits \(u\) let \(\overrightarrow{u}\) be its bit symbols in order and \(\overleftarrow{u}\) the same symbols in reverse order. Let \(q\) and \(n\) be lists of bits, \(b\) and \(x\) bits, \(s\) a list of symbols, and \(R\), \(r\) lists of symbols each empty or topped by a symbol that is not a bit. From label \(\mathsf{cmp}(b)\) with any internal state, \(\overleftarrow{q}R\) on \(T\), \(\overleftarrow{n}r\) on \(B\), \(s\) on \(S\), the stacks \(A\) and \(C\) empty and the bit symbol of \(x\) alone on \(V\), the lookup program reaches, in at most \(4|n| + 5\) steps, label \(\mathsf{scan}\) with some internal state, \(\overleftarrow{q}R\) on \(T\), \(r\) on \(B\), \(\overrightarrow{n}s\) on \(S\), the stacks \(A\) and \(C\) empty and on \(V\) alone the bit symbol of \(b\) if \(n = q\) and of \(x\) otherwise.

theorem cmp_run (q : List Bool) (R : List Sym) (hR : EndsBitBlock Sym.bit? R) (n : List Bool)
    (b x : Bool) (r s : List Sym) (hr : EndsBitBlock Sym.bit? r) (v : Bool) :
    ∃ v', RunLe prog (4 * n.length + 5)
      ⟨some (.cmp b), v, stk ((q.map Sym.bit).reverse ++ R) ((n.map Sym.bit).reverse ++ r) s
        [] [] [Sym.bit x]⟩
      ⟨some .scan, v', stk ((q.map Sym.bit).reverse ++ R) r (n.map Sym.bit ++ s) [] []
        [Sym.bit (if n = q then b else x)]⟩
Uses 15 · Used by 1
Statement usesStacks of the lookup machine · Labels of the lookup machine · The lookup program · Stack contents of the lookup machine · Stack alphabet of the SAT verifier · Reading a symbol as a name bit · End of a bit block · Runs within a step budget
Proof usesRestoring and stashing after a comparison in the lookup machine · Four pairwise distinct stacks · Flag bit of a machine state · Bit blocks · Exact-length runs of a TM2 machine · A single step executes the statement at the current label · Correctness of the bit-block comparison
Used byOne scan step of the lookup

TheoremOne scan step of the lookup#✓fully proved

Write stack contents top first; for a list of bits \(u\) let \(\overleftarrow{u}\) be its bit symbols in reverse order; for a list \(E\) of table entries let \(\tau(E)\) be the symbols of its entries in reading order (each entry's name bits, then its marker) and \(\mathrm{val}_E(q)\) the value of the first live entry of \(E\) named \(q\), or false if there is none. Let \(q\) be a list of bits, \(e = (n, m)\) a table entry, \(E\) a list of entries, \(eE\) the list \(E\) with \(e\) prepended, and \(R\), \(r\) lists of symbols each empty or topped by a symbol that is not a bit. From label \(\mathsf{scan}\) with any internal state, \(\overleftarrow{q}R\) on \(T\), the marker of \(e\) above \(\overleftarrow{n}r\) on \(B\), \(\tau(E)\) on \(S\), the stacks \(A\) and \(C\) empty and the bit symbol of \(\mathrm{val}_E(q)\) alone on \(V\), the lookup program reaches, in at most \(4|n| + 6\) steps, label \(\mathsf{scan}\) with some internal state, \(\overleftarrow{q}R\) on \(T\), \(r\) on \(B\), \(\tau(eE)\) on \(S\), the stacks \(A\) and \(C\) empty and the bit symbol of \(\mathrm{val}_{eE}(q)\) alone on \(V\).

theorem entry_run (q : List Bool) (R : List Sym) (hR : EndsBitBlock Sym.bit? R) (e : Ent)
    (r : List Sym) (hr : EndsBitBlock Sym.bit? r) (post : List Ent) (v : Bool) :
    ∃ v', RunLe prog (4 * e.1.length + 6)
      ⟨some .scan, v, stk ((q.map Sym.bit).reverse ++ R)
        (markOf e.2 :: ((e.1.map Sym.bit).reverse ++ r)) (post.flatMap entToks) [] []
        [Sym.bit (liveVal post q)]⟩
      ⟨some .scan, v', stk ((q.map Sym.bit).reverse ++ R) r ((e :: post).flatMap entToks) [] []
        [Sym.bit (liveVal (e :: post) q)]⟩
Uses 19 · Used by 1
Statement usesTable entries · Stacks of the lookup machine · Labels of the lookup machine · The lookup program · Stack contents of the lookup machine · Stack alphabet of the SAT verifier · Reading a symbol as a name bit · Symbols of a table entry · Live value of a name in a table · Closing marker of a table entry · End of a bit block · Runs within a step budget
Proof usesServing a live table entry · Next label of the lookup scan · Flag bit of a machine state · Bit blocks · Exact-length runs of a TM2 machine · A single step executes the statement at the current label · Running the bit-moving loop
Used byThe scan loop of the lookup machine

TheoremThe scan loop of the lookup machine#✓fully proved

Let \(q\) be a list of bits, let \(R\) be a list of symbols that is empty or starts with a symbol other than a name bit, and let \(pre\) and \(post\) be lists of table entries; the live value of \(q\) in an entry list is the value of its first entry named \(q\) that has a value, or false if there is none. Suppose the lookup program is at label \(\mathsf{scan}\), with any internal bit, and its stacks are: \(T\) holds the bits of \(q\) as name bits, last bit on top, above \(R\); \(B\) holds the table stack of \(pre\), of length \(\ell\); \(S\) holds the symbols of the entries of \(post\) in reading order, first entry on top; \(A\) and \(C\) are empty; and \(V\) holds the single name bit carrying the live value of \(q\) in \(post\). Then within \(6\ell + 1\) steps the program reaches label \(\mathsf{back}\), with some internal bit, where \(B\) is empty, \(S\) holds the symbols of the entries of \(pre\) followed by \(post\) in reading order, first entry on top, \(V\) holds the single name bit carrying the live value of \(q\) in \(pre\) followed by \(post\), and \(T\), \(A\) and \(C\) are unchanged.

theorem scan_loop (q : List Bool) (R : List Sym) (hR : EndsBitBlock Sym.bit? R)
    (pre : List Ent) :
    ∀ (post : List Ent) (v : Bool), ∃ v', RunLe prog (6 * (tblStk pre).length + 1)
      ⟨some .scan, v, stk ((q.map Sym.bit).reverse ++ R) (tblStk pre) (post.flatMap entToks) []
        [] [Sym.bit (liveVal post q)]⟩
      ⟨some .back, v', stk ((q.map Sym.bit).reverse ++ R) [] ((pre ++ post).flatMap entToks) []
        [] [Sym.bit (liveVal (pre ++ post) q)]⟩
Uses 18 · Used by 1
Statement usesTable entries · Stacks of the lookup machine · Labels of the lookup machine · The lookup program · Stack contents of the lookup machine · Stack alphabet of the SAT verifier · Reading a symbol as a name bit · Symbols of a table entry · Live value of a name in a table · Table stack of an entry list · End of a bit block · Runs within a step budget
Proof usesOne scan step of the lookup · Moving a symbol between stacks · Next label of the lookup scan · Closing marker of a table entry · Exact-length runs of a TM2 machine · A single step executes the statement at the current label
Used byCorrectness of the SAT-verifier lookup machine

TheoremThe return loop of the lookup machine#✓fully proved

Let \(t\) and \(w\) be lists of symbols, let \(pre\) and \(post\) be lists of table entries, and let \(m\) be the total number of symbols of the entries of \(post\). Suppose the lookup program is at label \(\mathsf{back}\), with any internal bit, and its stacks are: \(T\) holds \(t\); \(B\) holds the table stack of \(pre\); \(S\) holds the symbols of the entries of \(post\) in reading order, first entry on top; \(A\) and \(C\) are empty; and \(V\) holds \(w\). Then within \(2m + 2\) steps the program reaches label \(\mathsf{done}\), with some internal bit, where \(B\) holds the table stack of the entry list \(pre\) followed by \(post\), the stacks \(S\), \(A\) and \(C\) are empty, and \(T\) and \(V\) still hold \(t\) and \(w\).

theorem back_loop (T w : List Sym) (post : List Ent) :
    ∀ (pre : List Ent) (v : Bool), ∃ v', RunLe prog (2 * (post.flatMap entToks).length + 2)
      ⟨some .back, v, stk T (tblStk pre) (post.flatMap entToks) [] [] w⟩
      ⟨some .done, v', stk T (tblStk (pre ++ post)) [] [] [] w⟩
Uses 18 · Used by 1
Statement usesTable entries · Stacks of the lookup machine · Labels of the lookup machine · The lookup program · Stack contents of the lookup machine · Stack alphabet of the SAT verifier · Symbols of a table entry · Table stack of an entry list · Runs within a step budget
Proof usesMoving a symbol between stacks · Reading a symbol as a name bit · Closing marker of a table entry · End of a bit block · Flag bit of a machine state · Bit blocks · Exact-length runs of a TM2 machine · A single step executes the statement at the current label · Running the bit-moving loop
Used byCorrectness of the SAT-verifier lookup machine

TheoremCorrectness of the SAT-verifier lookup machine#✓fully proved

Let \(q\) be a list of bits, \(es\) a list of table entries and \(R\) a list of symbols that is empty or starts with a symbol other than a name bit. Suppose the stacks of the lookup machine are as follows: \(T\) holds the bits of \(q\) as name bits, last bit on top, above \(R\); \(B\) holds the table stack of \(es\), of length \(\ell\); and \(S\), \(A\), \(C\) and \(V\) are empty. Then the lookup program, started at its start label with any internal bit, reaches the label \(\mathsf{done}\) within \(8\ell + 4\) steps, with some internal bit; there \(V\) holds the single name bit carrying the live value of \(q\) in \(es\) (the value of the first entry of \(es\) named \(q\) that has a value, or false if there is none), and every other stack is as it started.

theorem run (q : List Bool) (es : List Ent) (R : List Sym) (hR : R.head?.bind Sym.bit? = none)
    (v : Bool) (St : ∀ _ : K, List Sym) (hT : St .T = (q.map Sym.bit).reverse ++ R)
    (hB : St .B = tblStk es) (hS : St .S = []) (hA : St .A = []) (hC : St .C = [])
    (hV : St .V = []) :
    ∃ v', RunLe prog (8 * (tblStk es).length + 4) ⟨some start, v, St⟩
      ⟨some .done, v', update St .V [Sym.bit (liveVal es q)]⟩
Uses 16 · Used by 1
Statement usesTable entries · Stacks of the lookup machine · Labels of the lookup machine · The lookup program · Start label of the lookup machine · Stack alphabet of the SAT verifier · Reading a symbol as a name bit · Live value of a name in a table · Table stack of an entry list · Runs within a step budget
Proof usesThe return loop of the lookup machine · Initialization step of the lookup machine · The scan loop of the lookup machine · Stack contents of the lookup machine · Symbols of a table entry · Exact-length runs of a TM2 machine
Used byThe embedded lookup meets the lookup contract

InductiveStacks of the SAT tokenizer#✓fully proved

The SAT tokenizer has six stacks: \(X\) for the formula bits, \(W\) for the witness bits, \(T\) for the token output, \(B\) for the table output, and the clause counter \(\mathsf{CC}\) and the literal counter \(\mathsf{LC}\).

inductive K | X | W | T | B | CC | LC
  deriving DecidableEq
Used by 38
Used byThe tokenizer program · Rejection of the SAT tokenizer within a step bound · One step to rejection · Tokenizer stack contents · Reading a unary count · Instruction for 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 · Placement of the tokenizer's stacks in the host · Stack embedding of the tokenizer into the host · Program of the SAT verifier host · The tokenizer embeds in the SAT verifier host · Tokenizer stacks after phase 0 · The TM2 SAT verifier · The tokenize-then-emit machine as a host component · Tokenizer stacks in the tokenize-then-emit machine · Embedding the emitter's stacks into tokenize-then-emit · Embedding the tokenizer's stacks into tokenize-then-emit · Initial stacks of the tokenize-then-emit machine · Emitter reductions out of SAT are polynomial-time · Stacks of the tokenize-then-emit machine · Program of the tokenize-then-emit machine · Tokenize, then emit · List of the tokenizer's stacks · Initial stacks of the tokenizer · Alphabets of the tokenize-then-emit machine

InductiveLabels of the SAT tokenizer#✓fully proved

The labels of the SAT tokenizer are: \(\mathsf{un}(c)\) for a bit \(c\), which reads a unary count onto the clause counter \(\mathsf{CC}\) if \(c\) is true and onto the literal counter \(\mathsf{LC}\) otherwise; \(\mathsf{cls}\), which starts a clause; \(\mathsf{lits}\), which starts a literal; \(\mathsf{nm}(\ell)\), where \(\ell\) is a bit or none, which reads the bit pairs of a name block, \(\ell\) being the last name bit read (none before the first one); \(\mathsf{pol}\), which reads the polarity and the next witness bit; \(\mathsf{fin}\), which checks that the formula stack \(X\) is used up; and the halting labels \(\mathsf{acc}\) and \(\mathsf{rej}\).

inductive Lab
  | un (c : Bool)
  | cls
  | lits
  | nm (last : Option Bool)
  | pol
  | fin
  | acc
  | rej
  deriving DecidableEq
Used by 38
Used byThe tokenizer program · Rejection of the SAT tokenizer within a step bound · One step to rejection · Start label of the SAT tokenizer · Reading a unary count · Instruction for 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 · Name-loop outcome · Name-loop outcome from the start of a name · 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 · Host labels as a sum type · Labels of the SAT verifier host · Program of the SAT verifier host · Tokenizer labels in the host machine · The tokenizer embeds in the SAT verifier host · Phase 0 of the SAT verifier host · The SAT verifier machine · The TM2 SAT verifier · The tokenize-then-emit machine as a host component · Emitter labels in the tokenize-then-emit machine · Exit label of the tokenize-then-emit machine · Labels of the tokenize-then-emit machine · Program of the tokenize-then-emit machine · Tokenize, then emit · Start label of the tokenize-then-emit machine · Renaming the tokenizer's labels

DefinitionTesting whether the top symbol is a given bit#✓fully proved

For a bit \(b\) and the result of peeking at a stack (a symbol, or nothing when the stack is empty), this is true exactly when the peeked symbol is the bit symbol carrying \(b\); it is false for an empty stack and for every other symbol.

def topIsBit (b : Bool) : Option Sym → Bool
  | some (.bit c) => c == b
  | _ => false
Uses 1 · Used by 6
Statement usesStack alphabet of the SAT verifier
Used byThe tokenizer program · Reading a unary count · Instruction for reading a unary count · Rejecting an unterminated name block · Reading a name block · An unterminated unary count is rejected

DefinitionInstruction for reading a unary count#✓fully proved

For a stack \(k\) of the tokenizer and labels \(s\) and \(t\), this is the tokenizer instruction that looks at the top of the formula stack \(X\). If it is the bit true, the instruction pops it, pushes the clause-end symbol \(\mathsf{cl}\) onto \(k\) and goes to \(s\); if it is the bit false, it pops it and goes to \(t\); otherwise, when \(X\) is empty or its top is not a bit, it goes to \(\mathsf{rej}\). The internal bit is set to true in the first two cases and to false in the last.

When \(k\) is not \(X\) and the instruction is placed at label \(s\), a run on a formula stack that starts with \(m\) bits true followed by a bit false pops these \(m + 1\) bits, pushes \(m\) copies of \(\mathsf{cl}\) onto \(k\) and goes to \(t\).

def unary (k : K) (self next : Lab) : TM2.Stmt (fun _ : K => Sym) Lab Bool :=
  peek .X (fun _ o => topIsBit true o) <| branch id
    (pop .X (fun s _ => s) <| push k (fun _ => .cl) <| goto fun _ => self)
    (peek .X (fun _ o => topIsBit false o) <| branch id
      (pop .X (fun s _ => s) <| goto fun _ => next)
      (goto fun _ => .rej))
Uses 4 · Used by 1
Statement usesStack alphabet of the SAT verifier · Stacks of the SAT tokenizer · Labels of the SAT tokenizer · Testing whether the top symbol is a given bit
Used byThe tokenizer program

DefinitionThe tokenizer program#✓fully proved

The tokenizer is a multi-stack machine with stacks \(X\) (formula bits), \(W\) (witness bits), \(T\) (tokens), \(B\) (table) and the unary counters \(CC\), \(LC\) (over the unit symbol \(\mathsf{cl}\)), and one bit of internal state. Its instruction at each label is:

  • \(\mathsf{un}(\mathrm{true})\), \(\mathsf{un}(\mathrm{false})\): read a unary count from \(X\) onto \(CC\) and \(LC\) respectively. If the top of \(X\) is the bit true, pop it, push \(\mathsf{cl}\) onto the counter and stay; if it is the bit false, pop it and go to \(\mathsf{cls}\) (from \(\mathsf{un}(\mathrm{true})\)) or \(\mathsf{lits}\) (from \(\mathsf{un}(\mathrm{false})\)); otherwise go to \(\mathsf{rej}\).
  • \(\mathsf{cls}\): pop \(CC\); if it was non-empty go to \(\mathsf{un}(\mathrm{false})\), else go to \(\mathsf{fin}\).
  • \(\mathsf{lits}\): pop \(LC\); if it was non-empty go to \(\mathsf{nm}(\mathrm{none})\), else push \(\mathsf{cl}\) onto \(T\) and go to \(\mathsf{cls}\).
  • \(\mathsf{nm}(\ell)\), where \(\ell\) is an optional bit: if the top of \(X\) is the bit true, pop it; then if the top of \(X\) is a bit \(s\), pop it, push the name bit \(s\) onto \(T\) and onto \(B\) and go to \(\mathsf{nm}(s)\), and otherwise go to \(\mathsf{rej}\). If instead the top of \(X\) is the bit false, pop it and go to \(\mathsf{rej}\) if \(\ell\) is the bit false and to \(\mathsf{pol}\) otherwise. In any other case go to \(\mathsf{rej}\).
  • \(\mathsf{pol}\): if the top of \(X\) is a bit \(p\), pop it and push \(\mathsf{lit}(p)\) onto \(T\); then if \(W\) is non-empty, pop its top symbol, read as a bit \(s\) (false if it is not a bit), and push \(\mathsf{val}(s)\) onto \(B\), and otherwise push \(\mathsf{dead}\) onto \(B\); go to \(\mathsf{lits}\). If the top of \(X\) is not a bit, go to \(\mathsf{rej}\).
  • \(\mathsf{fin}\): go to \(\mathsf{rej}\) if \(X\) is non-empty and to \(\mathsf{acc}\) if it is empty.
  • \(\mathsf{acc}\), \(\mathsf{rej}\): halt.

Each test stores its outcome in the internal bit: whether the top of \(X\) or \(W\) has the stated form, or, for the pop of \(CC\) or \(LC\), whether that counter was non-empty. Popping a name bit \(s\) in \(\mathsf{nm}(\ell)\), the polarity \(p\) in \(\mathsf{pol}\) or a witness symbol in \(\mathsf{pol}\) stores the bit read (\(s\), \(p\) or the witness bit \(s\)); the remaining pops and all pushes leave the internal bit unchanged. So after popping a bit of a unary count, or the closing bit false of a name block, the internal bit is true.

Cslib.Complexity.SatVerifier.Tokenizer.prog · 25 lines 
def prog : Lab → TM2.Stmt (fun _ : K => Sym) Lab Bool
  | .un true => unary .CC (.un true) .cls
  | .un false => unary .LC (.un false) .lits
  | .cls => pop .CC (fun _ o => o.isSome) <| branch id (goto fun _ => .un false)
      (goto fun _ => .fin)
  | .lits => pop .LC (fun _ o => o.isSome) <| branch id (goto fun _ => .nm none)
      (push .T (fun _ => .cl) <| goto fun _ => .cls)
  | .nm last => peek .X (fun _ o => topIsBit true o) <| branch id
      (pop .X (fun s _ => s) <| peek .X (fun _ o => isBit Sym.bit? o) <| branch id
        (pop .X (fun _ o => bitOf Sym.bit? o) <| push .T (fun s => .bit s) <|
          push .B (fun s => .bit s) <|
          goto fun s => .nm (some s))
        (goto fun _ => .rej))
      (peek .X (fun _ o => topIsBit false o) <| branch id
        (pop .X (fun s _ => s) <| goto fun _ => if last = some false then .rej else .pol)
        (goto fun _ => .rej))
  | .pol => peek .X (fun _ o => isBit Sym.bit? o) <| branch id
      (pop .X (fun _ o => bitOf Sym.bit? o) <| push .T (fun s => .lit s) <|
        peek .W (fun _ o => o.isSome) <| branch id
          (pop .W (fun _ o => bitOf Sym.bit? o) <| push .B (fun s => .val s) <| goto fun _ => .lits)
          (push .B (fun _ => .dead) <| goto fun _ => .lits))
      (goto fun _ => .rej)
  | .fin => peek .X (fun _ o => o.isSome) <| branch id (goto fun _ => .rej) (goto fun _ => .acc)
  | .acc => halt
  | .rej => halt
Uses 8 · Used by 22
Statement usesStack alphabet of the SAT verifier · Reading a symbol as a name bit · Stacks of the SAT tokenizer · Labels of the SAT tokenizer · Testing whether the top symbol is a given bit · Instruction for reading a unary count · Bit on top of a stack · Bit test for the top of a stack
Used byRejection of the SAT tokenizer within a step bound · One step to rejection · 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 · Program of the SAT verifier host · The tokenizer embeds in the SAT verifier host · The TM2 SAT verifier · Program of the tokenize-then-emit machine · Tokenize, then emit

DefinitionStart label of the SAT tokenizer#✓fully proved

The tokenizer starts at the label \(\mathrm{un}(1)\), which reads a unary count from the input stack \(X\) onto the clause counter \(CC\).

def start : Lab := .un true
Uses 1 · Used by 8
Statement usesLabels of the SAT tokenizer
Used byRejecting run · Accepting run of the SAT tokenizer · Program of the SAT verifier host · The tokenizer embeds in the SAT verifier host · Phase 0 of the SAT verifier host · The TM2 SAT verifier · Tokenize, then emit · Start label of the tokenize-then-emit machine

DefinitionTokenizer stack contents#✓fully proved

For symbol lists \(x, w, t, b\) and natural numbers \(c, \ell\), this assigns to the tokenizer's stacks \(X\), \(W\), \(T\), \(B\) the lists \(x\), \(w\), \(t\), \(b\), and to the counter stacks \(CC\) and \(LC\) the lists of \(c\) and \(\ell\) copies of the clause-end symbol \(\mathrm{cl}\) (the counters in unary).

def st (x w t b : List Sym) (cc lc : ℕ) : K → List Sym
  | .X => x
  | .W => w
  | .T => t
  | .B => b
  | .CC => List.replicate cc .cl
  | .LC => List.replicate lc .cl
Uses 2 · Used by 15
Statement usesStack alphabet of the SAT verifier · Stacks of the SAT tokenizer
Used byReading 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

DefinitionRejection of the SAT tokenizer within a step bound#✓fully proved

For a natural number \(n\) and a configuration \(c\) of the tokenizer, the tokenizer rejects from \(c\) within \(n\) steps when there are an internal bit \(v\) and stacks \(S\) such that it runs in at most \(n\) steps from \(c\) to the configuration with label \(\mathsf{rej}\), internal bit \(v\) and stacks \(S\).

def Rej (n : ℕ) (c : TM2.Cfg (fun _ : K => Sym) Lab Bool) : Prop :=
  ∃ v S, RunLe prog n c ⟨some .rej, v, S⟩
Uses 5 · Used by 7
Statement usesStack alphabet of the SAT verifier · Stacks of the SAT tokenizer · Labels of the SAT tokenizer · The tokenizer program · Runs within a step budget
Used byOne step to rejection · Tokenizer rejects undecodable clauses · Tokenizer rejects an undecodable literal · Tokenizer rejects undecodable literals · Rejecting an unterminated name block · Rejecting run · An unterminated unary count is rejected

TheoremOne step to rejection#✓fully proved

Let \(\ell\) be a label, \(v\) a bit and \(S\) an assignment of symbol stacks to the tokenizer's stacks. If executing the tokenizer's instruction at \(\ell\) from internal bit \(v\) and stacks \(S\) yields a configuration with label \(\mathsf{rej}\), then the tokenizer reaches \(\mathsf{rej}\) within one step from the configuration with label \(\ell\), internal bit \(v\) and stacks \(S\).

theorem rej_one {l : Lab} {v : Bool} {S : K → List Sym}
    (h : (TM2.stepAux (prog l) v S).l = some .rej) : Rej 1 ⟨some l, v, S⟩
Uses 8 · Used by 4
Statement usesStack alphabet of the SAT verifier · Stacks of the SAT tokenizer · Labels of the SAT tokenizer · Rejection of the SAT tokenizer within a step bound · The tokenizer program
Proof usesExact-length runs of a TM2 machine · A single step executes the statement at the current label · Runs within a step budget
Used byTokenizer rejects an undecodable literal · Rejecting an unterminated name block · Rejecting run · An unterminated unary count is rejected

TheoremReading a unary count#✓fully proved

Let \(c\) be a bit, \(n\) a natural number, \(r\) a bit string, \(w, t, b\) symbol lists and \(m, \ell\) counter values. Started at the label \(\mathrm{un}(c)\) with any value of its Boolean variable, with \(X\) holding the bits of \(1^n 0 r\), with \(W\), \(T\), \(B\) holding \(w\), \(t\), \(b\), and with the counters \(CC\) and \(LC\) holding \(m\) and \(\ell\) in unary, the tokenizer takes exactly \(n + 1\) steps to reach the configuration whose label is \(\mathrm{cls}\) if \(c = 1\) and \(\mathrm{lits}\) if \(c = 0\), whose Boolean variable is \(1\), whose stack \(X\) holds the bits of \(r\), whose stacks \(W\), \(T\), \(B\) still hold \(w\), \(t\), \(b\), and whose counters hold \(m + n\) and \(\ell\) if \(c = 1\), and \(m\) and \(\ell + n\) if \(c = 0\).

theorem un_run (c : Bool) (rest : List Bool) (w t b : List Sym) : ∀ (n cc lc : ℕ) (v : Bool),
    Run prog (n + 1)
      ⟨some (.un c), v, st ((List.replicate n true ++ false :: rest).map .bit) w t b cc lc⟩
      ⟨some (if c then .cls else .lits), true,
        st (rest.map .bit) w t b (if c then cc + n else cc) (if c then lc else lc + n)⟩
Uses 8 · Used by 4
Statement usesStack alphabet of the SAT verifier · Stacks of the SAT tokenizer · Labels of the SAT tokenizer · The tokenizer program · Tokenizer stack contents · Exact-length runs of a TM2 machine
Proof usesTesting whether the top symbol is a given bit · A single step executes the statement at the current label
Used byTokenizer run on one clause · Tokenizer rejects undecodable clauses · Rejecting run · Accepting run of the SAT tokenizer
20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.