An unterminated unary count is rejected to Stack alphabets of the SAT verifier host

TheoremAn unterminated unary count is rejected#✓fully proved

Let \(r\) be a bit string on which reading a unary length prefix fails. For every bit \(c\), symbol lists \(w, t, b\), counter values \(m, \ell\) and value of the Boolean variable, the tokenizer started at the label \(\mathrm{un}(c)\) with \(X\) holding the bits of \(r\), with \(W\), \(T\), \(B\) holding \(w\), \(t\), \(b\), and with the counters \(CC\) and \(LC\) holding \(m\) and \(\ell\) in unary reaches the rejecting label within \(|r| + 1\) steps.

theorem un_fail (c : Bool) (w t b : List Sym) : ∀ (r : List Bool), readUnaryLength r = none →
    ∀ (cc lc : ℕ) (v : Bool), Rej (r.length + 1) ⟨some (.un c), v, st (r.map .bit) w t b cc lc⟩

Uses 12 · Used by 2

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 · Tokenizer stack contents · Reading a unary length prefix

Proof usesThe tokenizer program · One step to rejection · Testing whether the top symbol is a given bit · Exact-length runs of a TM2 machine · A single step executes the statement at the current label · Runs within a step budget

Used byTokenizer rejects undecodable clauses · Rejecting run

DefinitionName-loop outcome#✓fully proved

For an optional bit \(\ell\) and a bit string \(u\), the name-loop outcome is the tokenizer label defined by recursion on \(u\): for empty \(u\) it is \(\mathsf{rej}\) if \(\ell\) is the bit false and \(\mathsf{pol}\) otherwise, and for \(u = c\,u'\) it is the outcome for the bit \(c\) and the string \(u'\). So it is \(\mathsf{rej}\) exactly when the string formed by \(\ell\) (if present) followed by \(u\) is non-empty and ends in false, and \(\mathsf{pol}\) otherwise.

def nmEnd : Option Bool → List Bool → Lab
  | last, [] => if last = some false then .rej else .pol
  | _, c :: bits => nmEnd (some c) bits

Uses 1 · Used by 4

Statement usesLabels of the SAT tokenizer

Used byTokenizer rejects an undecodable literal · Tokenizer run on one literal · Name-loop outcome from the start of a name · Reading a name block

TheoremName-loop outcome from the start of a name#✓fully proved

For every bit string \(u\), the name-loop outcome with no previous bit after \(u\) is the label \(\mathsf{pol}\) if \(u\) is a canonical name, that is, encoding the natural number that \(u\) decodes to gives back \(u\), and the label \(\mathsf{rej}\) otherwise.

theorem nmEnd_none (bits : List Bool) :
    nmEnd none bits = if encodeNat (decodeNat bits) = bits then .pol else .rej

Uses 3 · Used by 2

Statement usesLabels of the SAT tokenizer · Name-loop outcome

Proof usesCanonical binary names

Used byTokenizer rejects an undecodable literal · Tokenizer run on one literal

TheoremReading a name block#✓fully proved

Let \(u\) and \(r\) be bit strings, \(\ell\) an optional bit, \(v\) a bit, \(w\), \(t\), \(b\) symbol stacks and \(c\), \(l\) natural numbers. Started at label \(\mathsf{nm}(\ell)\) with internal bit \(v\), the bits of the self-delimiting block of \(u\) followed by \(r\) on the formula stack \(X\), \(w\) on the witness stack \(W\), \(t\) on the token stack \(T\), \(b\) on the table stack \(B\), clause counter \(c\) and literal counter \(l\), the tokenizer runs in exactly \(|u| + 1\) steps to the configuration whose label is the name-loop outcome for \(\ell\) and \(u\), with internal bit true, the bits of \(r\) on \(X\), \(w\) on \(W\), the bits of \(u\) in reverse order (last bit on top) above \(t\) on \(T\) and above \(b\) on \(B\), and the same counters.

theorem nm_run (rest : List Bool) (w : List Sym) (cc lc : ℕ) :
    ∀ (bits : List Bool) (last : Option Bool) (t b : List Sym) (v : Bool),
    Run prog (bits.length + 1)
      ⟨some (.nm last), v, st ((delimit bits ++ rest).map .bit) w t b cc lc⟩
      ⟨some (nmEnd last bits), true, st (rest.map .bit) w ((bits.map .bit).reverse ++ t)
        ((bits.map .bit).reverse ++ b) cc lc⟩

Uses 13 · Used by 2

Statement usesStack alphabet of the SAT verifier · Stacks of the SAT tokenizer · Labels of the SAT tokenizer · Name-loop outcome · The tokenizer program · Tokenizer stack contents · Self-delimiting form of a bitstring · Exact-length runs of a TM2 machine

Proof usesReading a symbol as a name bit · Testing whether the top symbol is a given bit · A single step executes the statement at the current label · Bit on top of a stack · Bit test for the top of a stack

Used byTokenizer rejects an undecodable literal · Tokenizer run on one literal

TheoremRejecting an unterminated name block#✓fully proved

Let \(r\) be a bit string from whose front no self-delimiting block can be parsed. For every optional last bit \(\ell\), internal bit \(v\), symbol stacks \(w\), \(t\), \(b\) and natural numbers \(c\), \(l\), the tokenizer started at label \(\mathsf{nm}(\ell)\) with internal bit \(v\), the bits of \(r\) on the formula stack \(X\), \(w\) on the witness stack \(W\), \(t\) on the token stack \(T\), \(b\) on the table stack \(B\), clause counter \(c\) and literal counter \(l\) reaches the label \(\mathsf{rej}\) within \(|r| + 1\) steps.

theorem nm_fail (w : List Sym) (cc lc : ℕ) : ∀ (r : List Bool), undelimit r = none →
    ∀ (last : Option Bool) (t b : List Sym) (v : Bool),
    Rej (r.length + 1) ⟨some (.nm last), v, st (r.map .bit) w t b cc lc⟩

Uses 15 · Used by 1

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 · Tokenizer stack contents · Parsing one self-delimiting block

Proof usesReading a symbol as a name bit · The tokenizer program · One step to rejection · Testing whether the top symbol is a given bit · Exact-length runs of a TM2 machine · A single step executes the statement at the current label · Runs within a step budget · Bit on top of a stack · Bit test for the top of a stack

Used byTokenizer rejects an undecodable literal

TheoremReading a polarity#✓fully proved

Let \(p\), \(v\) be bits, \(r\), \(w\) bit strings, \(t\), \(b\) symbol stacks and \(c\), \(l\) natural numbers. Started at label \(\mathsf{pol}\) with internal bit \(v\), the bit \(p\) followed by the bits of \(r\) on the formula stack \(X\), the bits of \(w\) on the witness stack \(W\), \(t\) on the token stack \(T\), \(b\) on the table stack \(B\), clause counter \(c\) and literal counter \(l\), the tokenizer moves in exactly one step to label \(\mathsf{lits}\) with the bits of \(r\) on \(X\), the bits of \(w\) after its first on \(W\), the polarity marker \(\mathsf{lit}(p)\) pushed onto \(t\), and the same counters. If \(w\) starts with the bit \(w_1\), the internal bit becomes \(w_1\) and the marker \(\mathsf{val}(w_1)\) is pushed onto \(b\); if \(w\) is empty, the internal bit becomes false and the marker \(\mathsf{dead}\) is pushed onto \(b\).

theorem pol_run (p : Bool) (rest w : List Bool) (t b : List Sym) (cc lc : ℕ) (v : Bool) :
    Run prog 1 ⟨some .pol, v, st ((p :: rest).map .bit) (w.map .bit) t b cc lc⟩
      ⟨some .lits, w.head?.getD false, st (rest.map .bit) (w.tail.map .bit) (.lit p :: t)
        (markOf w.head? :: b) cc lc⟩

Uses 9 · Used by 1

Statement usesStack alphabet of the SAT verifier · Stacks of the SAT tokenizer · Labels of the SAT tokenizer · The tokenizer program · Tokenizer stack contents · Closing marker of a table entry · Exact-length runs of a TM2 machine

Proof usesReading a symbol as a name bit · A single step executes the statement at the current label

Used byTokenizer run on one literal

TheoremTokenizer run on one literal#✓fully proved

A configuration \(\langle \ell, v \mid x, w, t, b, i, j\rangle\) of the SAT tokenizer has label \(\ell\), internal bit \(v\), stacks \(X\), \(W\), \(T\), \(B\) holding \(x\), \(w\), \(t\), \(b\) (top first; a bit string stands for its list of bit symbols), and \(i\) and \(j\) marks on the clause and literal counters; \(\mathbin{+\!\!+}\) is concatenation. Let \(n, i, j \in \mathbb{N}\), let \(p\) and \(v\) be bits, \(r\) and \(w\) bit strings and \(t\) and \(b\) symbol lists. Let \(q\) be the binary code of \(n\) (Mathlib's canonical bits of \(n\), least significant first, empty for \(0\)), \(E\) the encoding of the literal \((n, p)\), \(o\) the first bit of \(w\) (none if \(w\) is empty), \(o'\) that bit with default false, and \(w'\) the string \(w\) with its first bit, if any, removed. Then the tokenizer goes in exactly \(|q| + 2\) steps from \(\langle \mathsf{nm}(\mathrm{none}), v \mid E \mathbin{+\!\!+} r, w, t, b, i, j\rangle\) to \(\langle \mathsf{lits}, o' \mid r, w', \mathrm{rev}(\lambda) \mathbin{+\!\!+} t, \mathrm{rev}(\eta) \mathbin{+\!\!+} b, i, j\rangle\), where \(\lambda\) is the token list of the literal \((n, p)\) (the bits of \(q\), then the polarity marker of \(p\)) and \(\eta\) is the symbol list of the table entry \((q, o)\) (the bits of \(q\), then the value marker of \(o\), which is dead if \(o\) is none).

theorem lit_run (n : ℕ) (p : Bool) (rest w : List Bool) (t b : List Sym) (cc lc : ℕ)
    (v : Bool) :
    Run prog ((encodeNat n).length + 2)
      ⟨some (.nm none), v, st ((encodeLit (n, p) ++ rest).map .bit) (w.map .bit) t b cc lc⟩
      ⟨some .lits, w.head?.getD false, st (rest.map .bit) (w.tail.map .bit)
        ((litToks (n, p)).reverse ++ t) ((entToks (encodeNat n, w.head?)).reverse ++ b)
        cc lc⟩

Uses 15 · Used by 2

Statement usesStack alphabet of the SAT verifier · Stacks of the SAT tokenizer · Labels of the SAT tokenizer · The tokenizer program · Tokenizer stack contents · Symbols of a table entry · Tokens of a literal · Binary code of a literal · Exact-length runs of a TM2 machine

Proof usesName-loop outcome · Name-loop outcome from the start of a name · Reading a name block · Reading a polarity · Closing marker of a table entry · Self-delimiting form of a bitstring

Used byTokenizer rejects undecodable literals · Reading the literals of a clause

TheoremTokenizer rejects an undecodable literal#✓fully proved

A configuration \(\langle \ell, v \mid x, w, t, b, i, j\rangle\) of the SAT tokenizer has label \(\ell\), internal bit \(v\), stacks \(X\), \(W\), \(T\), \(B\) holding \(x\), \(w\), \(t\), \(b\) (top first; a bit string stands for its list of bit symbols), and \(i\) and \(j\) marks on the clause and literal counters. Let \(r\) be a bit string from whose front no literal can be decoded (a literal being a self-delimited canonical variable code followed by a polarity bit), let \(w\), \(t\), \(b\) be symbol lists, \(i, j \in \mathbb{N}\) and \(v\) a bit. Then from \(\langle \mathsf{nm}(\mathrm{none}), v \mid r, w, t, b, i, j\rangle\) the tokenizer reaches the label \(\mathsf{rej}\) within \(|r| + 2\) steps.

theorem lit_fail (r : List Bool) (hr : decodeLit r = none) (w t b : List Sym) (cc lc : ℕ)
    (v : Bool) : Rej (r.length + 2) ⟨some (.nm none), v, st (r.map .bit) w t b cc lc⟩

Uses 20 · Used by 1

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 · Tokenizer stack contents · Decoding a literal

Proof usesReading a symbol as a name bit · Name-loop outcome · Name-loop outcome from the start of a name · Rejecting an unterminated name block · Reading a name block · The tokenizer program · One step to rejection · Decoding a prefix-coded natural number · Parsing a self-delimiting block · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Exact-length runs of a TM2 machine · Runs within a step budget · Bit on top of a stack

Used byTokenizer rejects undecodable literals

TheoremOccurrence table of a nonempty list#✓fully proved

Let \(n\) be a natural number, \(L\) a list of natural numbers and \(w\) a list of bits. The occurrence table of the list \(n\) followed by \(L\), with \(w\), is the entry whose name is the binary code of \(n\) and whose value is the first bit of \(w\) (no value if \(w\) is empty), followed by the occurrence table of \(L\) with \(w\) minus its first bit (with the empty list if \(w\) is empty).

theorem entsOf_cons (n : ℕ) (ns : List ℕ) (w : List Bool) :
    entsOf (n :: ns) w = (encodeNat n, w.head?) :: entsOf ns w.tail

Uses 2 · Used by 2

Statement usesTable entries · Occurrence table of a list of variables

Used byTokenizer run on all clauses · Reading the literals of a clause

TheoremReading the literals of a clause#✓fully proved

Let \(C\) be a clause with literals \((n_1, p_1), \dots, (n_k, p_k)\), let \(u\) be the concatenation of their literal codes, and let \(r\), \(w\) be bit strings, \(t\), \(b\) stacks of symbols, \(c\) a natural number and \(v\) a bit. Started at label \(\mathsf{lits}\) with internal bit \(v\), the bits of \(u\) followed by \(r\) on the formula stack \(X\), the bits of \(w\) on the witness stack \(W\), \(t\) on the token stack \(T\), \(b\) on the table stack \(B\), clause counter \(c\) and literal counter \(k\), the tokenizer reaches within \(2|u| + 1\) steps the configuration with label \(\mathsf{cls}\), internal bit false, the bits of \(r\) on \(X\), the bits of \(w\) with its first \(k\) bits removed on \(W\), the tokens of \(C\) in reverse order (its final \(\mathsf{cl}\) on top) above \(t\) on \(T\), the table stack of the entries \(e_1, \dots, e_k\) above \(b\) on \(B\), clause counter \(c\) and literal counter \(0\). Here \(e_i\) pairs the binary name of \(n_i\) with the \(i\)-th bit of \(w\), or with no value when \(w\) has fewer than \(i\) bits.

theorem lits_run (rest : List Bool) (cc : ℕ) :
    ∀ (C : CNFClause) (w : List Bool) (t b : List Sym) (v : Bool),
    RunLe prog (2 * (C.flatMap encodeLit).length + 1)
      ⟨some .lits, v, st ((C.flatMap encodeLit ++ rest).map .bit) (w.map .bit) t b cc C.length⟩
      ⟨some .cls, false, st (rest.map .bit) ((w.drop C.length).map .bit)
        ((clauseToks C).reverse ++ t) (tblStk (entsOf (C.map Prod.fst) w) ++ b) cc 0⟩

Uses 20 · Used by 1

Statement usesStack alphabet of the SAT verifier · Stacks of the SAT tokenizer · Labels of the SAT tokenizer · The tokenizer program · Tokenizer stack contents · Tokens of a clause · Occurrence table of a list of variables · Table stack of an entry list · Binary code of a literal · CNF clause · Runs within a step budget

Proof usesTable entries · Occurrence table of a nonempty list · Tokenizer run on one literal · Symbols of a table entry · Tokens of a literal · Prefix-free code of a natural number · Self-delimiting form of a bitstring · Exact-length runs of a TM2 machine · A single step executes the statement at the current label

Used byTokenizer run on one clause

TheoremTokenizer rejects undecodable literals#✓fully proved

A configuration \(\langle \ell, v \mid x, w, t, b, i, j\rangle\) of the SAT tokenizer has label \(\ell\), internal bit \(v\), stacks \(X\), \(W\), \(T\), \(B\) holding \(x\), \(w\), \(t\), \(b\) (top first; a bit string stands for its list of bit symbols), and \(i\) and \(j\) marks on the clause and literal counters. Let \(c, k \in \mathbb{N}\), let \(r\) and \(w\) be bit strings, \(t\) and \(b\) symbol lists and \(v\) a bit, and suppose that decoding \(k\) literals from the front of \(r\) fails. Then from \(\langle \mathsf{lits}, v \mid r, w, t, b, c, k\rangle\) the tokenizer reaches the label \(\mathsf{rej}\) within \(2|r| + 3\) steps.

theorem lits_fail (cc : ℕ) : ∀ (k : ℕ) (r w : List Bool) (t b : List Sym) (v : Bool),
    decodeLits k r = none →
    Rej (2 * r.length + 3) ⟨some .lits, v, st (r.map .bit) (w.map .bit) t b cc k⟩

Uses 22 · Used by 1

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 · Tokenizer stack contents · Decoding a fixed number of literals · CNF clause

Proof usesTokenizer rejects an undecodable literal · Tokenizer run on one literal · The tokenizer program · Symbols of a table entry · Tokens of a literal · Decoding a literal · Decoding a prefix-coded natural number · Binary code of a literal · Prefix-free code of a natural number · Parsing a self-delimiting block · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Exact-length runs of a TM2 machine · A single step executes the statement at the current label · Runs within a step budget

Used byTokenizer rejects undecodable clauses

TheoremTokenizer run on one clause#✓fully proved

A configuration \(\langle \ell, v \mid x, w, t, b, i, j\rangle\) of the SAT tokenizer has label \(\ell\), internal bit \(v\), stacks \(X\), \(W\), \(T\), \(B\) holding \(x\), \(w\), \(t\), \(b\) (top first; a bit string stands for its list of bit symbols), and \(i\) and \(j\) marks on the clause and literal counters; \(\mathbin{+\!\!+}\) is concatenation. Let \(C\) be a clause, \(r\) and \(w\) bit strings, \(t\) and \(b\) symbol lists, \(c \in \mathbb{N}\) and \(v\) a bit. Let \(E\) be the encoding of \(C\), \(N\) the list of variable indices of the literals of \(C\) in order, and \(w'\) the string \(w\) with its first \(|C|\) bits removed (all of them if \(w\) is shorter). Then the tokenizer goes in at most \(2|E| + 1\) steps from \(\langle \mathsf{cls}, v \mid E \mathbin{+\!\!+} r, w, t, b, c + 1, 0\rangle\) to \(\langle \mathsf{cls}, \mathsf{false} \mid r, w', \mathrm{rev}(\tau) \mathbin{+\!\!+} t, \beta \mathbin{+\!\!+} b, c, 0\rangle\), where \(\tau\) is the token list of \(C\) and \(\beta\) is the table stack of the occurrence table of \(N\) against \(w\).

theorem clause_run (C : CNFClause) (rest w : List Bool) (t b : List Sym) (cc : ℕ) (v : Bool) :
    RunLe prog (2 * (encodeClause C).length + 1)
      ⟨some .cls, v, st ((encodeClause C ++ rest).map .bit) (w.map .bit) t b (cc + 1) 0⟩
      ⟨some .cls, false, st (rest.map .bit) ((w.drop C.length).map .bit)
        ((clauseToks C).reverse ++ t) (tblStk (entsOf (C.map Prod.fst) w) ++ b) cc 0⟩

Uses 18 · Used by 2

Statement usesStack alphabet of the SAT verifier · Stacks of the SAT tokenizer · Labels of the SAT tokenizer · The tokenizer program · Tokenizer stack contents · Tokens of a clause · Occurrence table of a list of variables · Table stack of an entry list · Length-prefixed binary code of a clause · CNF clause · Runs within a step budget

Proof usesReading the literals of a clause · Reading a unary count · Binary code of a literal · Prefix-free code of a natural number · Self-delimiting form of a bitstring · Exact-length runs of a TM2 machine · A single step executes the statement at the current label

Used byTokenizer rejects undecodable clauses · Tokenizer run on all clauses

TheoremTokenizer run on all clauses#✓fully proved

A configuration \(\langle \ell, v \mid x, w, t, b, i, j\rangle\) of the SAT tokenizer has label \(\ell\), internal bit \(v\), stacks \(X\), \(W\), \(T\), \(B\) holding \(x\), \(w\), \(t\), \(b\) (top first; a bit string stands for its list of bit symbols), and \(i\) and \(j\) marks on the clause and literal counters; \(\mathbin{+\!\!+}\) is concatenation. Let \(r\) and \(w\) be bit strings, \(\varphi\) a CNF formula with \(m\) clauses, \(t\) and \(b\) symbol lists and \(v\) a bit. Let \(E\) be the concatenation of the encodings of the clauses of \(\varphi\), \(N\) the list of variable indices of all literal occurrences of \(\varphi\) in order, and \(w'\) the string \(w\) with its first \(|N|\) bits removed (all of them if \(w\) is shorter). Then the tokenizer goes in at most \(2|E| + m + 1\) steps from \(\langle \mathsf{cls}, v \mid E \mathbin{+\!\!+} r, w, t, b, m, 0\rangle\) to \(\langle \mathsf{fin}, \mathsf{false} \mid r, w', \mathrm{rev}(\tau) \mathbin{+\!\!+} t, \beta \mathbin{+\!\!+} b, 0, 0\rangle\), where \(\tau\) is the token list of \(\varphi\) and \(\beta\) is the table stack of the occurrence table of \(N\) against \(w\).

theorem clauses_run (rest : List Bool) :
    ∀ (φ : CNF) (w : List Bool) (t b : List Sym) (v : Bool),
    RunLe prog (2 * (φ.flatMap encodeClause).length + φ.length + 1)
      ⟨some .cls, v, st ((φ.flatMap encodeClause ++ rest).map .bit) (w.map .bit) t b φ.length 0⟩
      ⟨some .fin, false, st (rest.map .bit) ((w.drop (varsOf φ).length).map .bit)
        ((toks φ).reverse ++ t) (tblStk (entsOf (varsOf φ) w) ++ b) 0 0⟩

Uses 20 · Used by 2

Statement usesStack alphabet of the SAT verifier · Stacks of the SAT tokenizer · Labels of the SAT tokenizer · The tokenizer program · Tokenizer stack contents · Occurrence table of a list of variables · Table stack of an entry list · Token sequence of a CNF formula · Length-prefixed binary code of a clause · Occurrence list of a CNF formula · CNF formula · CNF clause · Runs within a step budget

Proof usesTable entries · Tokenizer run on one clause · Occurrence table of a nonempty list · Tokens of a clause · Symbols of a table entry · Exact-length runs of a TM2 machine · A single step executes the statement at the current label

Used byRejecting run · Accepting run of the SAT tokenizer

TheoremTokenizer rejects undecodable clauses#✓fully proved

A configuration \(\langle \ell, v \mid x, w, t, b, i, j\rangle\) of the SAT tokenizer has label \(\ell\), internal bit \(v\), stacks \(X\), \(W\), \(T\), \(B\) holding \(x\), \(w\), \(t\), \(b\) (top first; a bit string stands for its list of bit symbols), and \(i\) and \(j\) marks on the clause and literal counters. Let \(n \in \mathbb{N}\), let \(r\) and \(w\) be bit strings, \(t\) and \(b\) symbol lists and \(v\) a bit, and suppose that decoding \(n\) clauses (each a unary literal count followed by that many encoded literals) from the front of \(r\) fails. Then from \(\langle \mathsf{cls}, v \mid r, w, t, b, n, 0\rangle\) the tokenizer reaches the label \(\mathsf{rej}\) within \(2|r| + n + 2\) steps.

theorem clauses_fail : ∀ (n : ℕ) (r w : List Bool) (t b : List Sym) (v : Bool),
    decodeClauses n r = none →
    Rej (2 * r.length + n + 2) ⟨some .cls, v, st (r.map .bit) (w.map .bit) t b n 0⟩

Uses 30 · Used by 1

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 · Tokenizer stack contents · Decoding a fixed number of clauses · CNF formula

Proof usesTokenizer run on one clause · Tokenizer rejects undecodable literals · The tokenizer program · An unterminated unary count is rejected · Reading a unary count · Tokens of a clause · Occurrence table of a list of variables · Table stack of an entry list · Decoding a length-prefixed clause · Decoding a literal · Decoding a fixed number of literals · Decoding a prefix-coded natural number · Length-prefixed binary code of a clause · Binary code of a literal · Prefix-free code of a natural number · Reading a unary length prefix · Parsing a self-delimiting block · CNF clause · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Exact-length runs of a TM2 machine · A single step executes the statement at the current label · Runs within a step budget

Used byRejecting run

TheoremThe tokenizer accepts when the formula stack is empty#✓fully proved

Let \(w\), \(t\), \(b\) be lists of symbols, \(i, j \in \mathbb{N}\) and \(v\) a bit. In exactly one step, the SAT tokenizer goes from the label \(\mathsf{fin}\) with internal bit \(v\), empty formula stack \(X\), stacks \(W\), \(T\), \(B\) holding \(w\), \(t\), \(b\), and \(i\) and \(j\) marks on the clause and literal counters, to the label \(\mathsf{acc}\) with internal bit false and all stacks unchanged.

theorem fin_acc (w t b : List Sym) (cc lc : ℕ) (v : Bool) :
    Run prog 1 ⟨some .fin, v, st [] w t b cc lc⟩ ⟨some .acc, false, st [] w t b cc lc⟩

Uses 7 · Used by 1

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 usesA single step executes the statement at the current label

Used byAccepting run of the SAT tokenizer

TheoremAccepting run of the SAT tokenizer#✓fully proved

Let \(x\) and \(w\) be bit strings such that \(x\) decodes to the CNF formula \(\varphi\), and let \(S\) be contents of the tokenizer's stacks in which \(X\) holds the bits of \(x\), \(W\) holds the bits of \(w\), and the counters \(CC\) and \(LC\) are empty. Started at the start label with stacks \(S\) and any value of its Boolean variable, the tokenizer reaches the accepting label within \(2|x| + 2\) steps, with final stacks \(S'\) such that \(X\), \(CC\) and \(LC\) are empty, \(W\) holds the bits of \(w\) without their first \(m\) entries, where \(m\) is the number of literal occurrences in \(\varphi\), \(T\) holds the reversed token list of \(\varphi\) on top of the original contents of \(T\), and \(B\) holds the table stack of the occurrence table of \(\varphi\) and \(w\) on top of the original contents of \(B\).

theorem run_some {x w : List Bool} {φ : CNF} (h : decodeCNF x = some φ) (v : Bool)
    (S : ∀ _ : K, List Sym) (hX : S .X = x.map Sym.bit) (hW : S .W = w.map Sym.bit)
    (hCC : S .CC = []) (hLC : S .LC = []) :
    ∃ v' S', RunLe prog (2 * x.length + 2) ⟨some start, v, S⟩ ⟨some .acc, v', S'⟩ ∧
      S' .X = [] ∧ S' .W = (w.drop (varsOf φ).length).map Sym.bit ∧ S' .CC = [] ∧
      S' .LC = [] ∧ S' .T = (toks φ).reverse ++ S .T ∧ S' .B = tblStk (ents φ w) ++ S .B

Uses 22 · Used by 2

Statement usesStack alphabet of the SAT verifier · Stacks of the SAT tokenizer · Labels of the SAT tokenizer · The tokenizer program · Start label of the SAT tokenizer · Occurrence table of a formula and a witness · Table stack of an entry list · Token sequence of a CNF formula · Decoding a complete length-prefixed CNF formula · Occurrence list of a CNF formula · CNF formula · Runs within a step budget

Proof usesTokenizer run on all clauses · The tokenizer accepts when the formula stack is empty · Tokenizer stack contents · Reading a unary count · Occurrence table of a list of variables · The CNF decoder inverts the length-prefixed CNF code · Length-prefixed binary code of a CNF formula · Length-prefixed binary code of a clause · CNF clause · Exact-length runs of a TM2 machine

Used byThe TM2 SAT verifier · Tokenize, then emit

TheoremRejecting run#✓fully proved

Let \(x\) and \(w\) be bit strings such that \(x\) does not decode as a CNF formula. For every bit \(v\) and stacks \(S\) with the bits of \(x\) on the formula stack \(X\), the bits of \(w\) on the witness stack \(W\), and both counter stacks \(CC\) and \(LC\) empty, the tokenizer started at its start label with internal bit \(v\) and stacks \(S\) reaches a configuration with label \(\mathsf{rej}\) within \(2|x| + 2\) steps.

theorem run_none {x w : List Bool} (h : decodeCNF x = none) (v : Bool) (S : ∀ _ : K, List Sym)
    (hX : S .X = x.map Sym.bit) (hW : S .W = w.map Sym.bit) (hCC : S .CC = [])
    (hLC : S .LC = []) :
    ∃ v' S', RunLe prog (2 * x.length + 2) ⟨some start, v, S⟩ ⟨some .rej, v', S'⟩

Uses 35 · Used by 2

Statement usesStack alphabet of the SAT verifier · Stacks of the SAT tokenizer · Labels of the SAT tokenizer · The tokenizer program · Start label of the SAT tokenizer · Decoding a complete length-prefixed CNF formula · CNF formula · Runs within a step budget

Proof usesRejection of the SAT tokenizer within a step bound · Tokenizer rejects undecodable clauses · Tokenizer run on all clauses · One step to rejection · Tokenizer stack contents · An unterminated unary count is rejected · Reading a unary count · Occurrence table of a list of variables · Table stack of an entry list · Token sequence of a CNF formula · Decoding a length-prefixed CNF formula · Decoding a length-prefixed clause · Decoding a fixed number of clauses · Decoding a literal · Decoding a fixed number of literals · Decoding a prefix-coded natural number · Length-prefixed binary code of a CNF formula · Length-prefixed binary code of a clause · Binary code of a literal · Prefix-free code of a natural number · Reading a unary length prefix · Parsing a self-delimiting block · Occurrence list of a CNF formula · CNF clause · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Exact-length runs of a TM2 machine

Used byThe TM2 SAT verifier · Tokenize, then emit

AbbreviationInput alphabet of the SAT verifier host#✓fully proved

The alphabet \(G\) of the host's input stack is the pair alphabet \(\mathrm{Bool} \oplus \mathrm{Option}\ \mathrm{Bool}\) of the dense SAT verifier.

In the encoding of a pair \((x, w)\), a formula bit \(b\) is \(\mathrm{inl}\ b\), the separator \(\#\) is \(\mathrm{inr}\ \mathrm{none}\) and a certificate bit \(b\) is \(\mathrm{inr}\ (\mathrm{some}\ b)\).

abbrev G := Cslib.Complexity.DenseSAT.Verifier.G

Uses 1 · Used by 6

Statement usesWork alphabet of the dense-SAT verifier

Used byStack alphabets of the SAT verifier host · Reading a witness bit in the SAT host · Reading a formula bit in the SAT host · Initial configuration of the SAT verifier machine · Initial stacks of the SAT verifier host · The TM2 SAT verifier

InductiveStacks of the SAT verifier host#✓fully proved

The SAT verifier host has seventeen stacks: the input stack, the output stack, and fifteen work stacks, namely two holding the formula bits and the certificate bits, two scratch stacks used to move them in phase 0, the token and table stacks, six further stacks of the clause-check driver, two further stacks of the tokenizer, and one further stack of the 3-clause filter.

inductive HK | inp | out | X | W | T | B | S | A | C | V | P | F | CC | LC | X1 | W1 | U
  deriving DecidableEq

Used by 18

Used byStack alphabets of the SAT verifier host · Driver stacks in the SAT host · Placement of the filter's stacks in the host · Placement of the tokenizer's stacks in the host · Stack embedding of the clause-check driver into the host · Stack embedding of the clause-length filter into the host · Stack embedding of the tokenizer into the host · Program of the SAT verifier host · Stacks emptied by the SAT verifier's cleanup · Cleanup of the SAT host · The tokenizer embeds in the SAT verifier host · Cleanup phase of the SAT verifier host · Initial configuration of the SAT verifier machine · Initial stacks of the SAT verifier host · Phase 0 of the SAT verifier host · The SAT verifier machine · The TM2 SAT verifier · The cleanup stacks are distinct

DefinitionStack alphabets of the SAT verifier host#✓fully proved

Each stack of the SAT verifier host has an alphabet: the input stack has the input alphabet \(G\), the output stack has alphabet \(\mathrm{Bool}\), and every other stack has the token alphabet \(\mathrm{Sym}\).

@[reducible] def HΓ : HK → Type
  | .inp => G
  | .out => Bool
  | _ => Sym

Uses 3 · Used by 11

Statement usesInput alphabet of the SAT verifier host · Stacks of the SAT verifier host · Stack alphabet of the SAT verifier

Used byStack embedding of the clause-check driver into the host · Stack embedding of the clause-length filter into the host · Stack embedding of the tokenizer into the host · Program of the SAT verifier host · Cleanup of the SAT host · The tokenizer embeds in the SAT verifier host · Cleanup phase of the SAT verifier host · Initial stacks of the SAT verifier host · Phase 0 of the SAT verifier host · The SAT verifier machine · The TM2 SAT verifier

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.