Stack alphabet of the SAT verifier to A clause has at most as many tokens as code bits

InductiveStack alphabet of the SAT verifier#✓fully proved

The symbols of the token and table stacks are a name bit \(b\) for each boolean \(b\), a polarity marker for each polarity \(p\), a clause end marker, a value marker for each boolean \(b\), and a dead marker. Equality of symbols is decidable.

inductive Sym
  | bit (b : Bool) | lit (p : Bool) | cl | val (b : Bool) | dead
  deriving DecidableEq

Used by 410

DefinitionReading a symbol as a name bit#✓fully proved

A symbol of the token and table stacks that is the name bit \(b\) reads as the bit \(b\); every other symbol reads as no bit, and so ends a name block.

def Sym.bit? : Sym → Option Bool
  | .bit b => some b
  | _ => none

Uses 1 · Used by 135

Statement usesStack alphabet of the SAT verifier

Used byProgram 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 clause-check driver · Literal loop of the clause check · The lookup contract · The lookup program · The return loop of the lookup machine · A name bit reads as itself · Serving a live table entry · One scan step of the lookup · The tokenizer program · Correctness of the SAT-verifier lookup machine · The scan loop of the lookup machine · Restoring and stashing after a comparison in the lookup machine · Tokenizer rejects an undecodable literal · Rejecting an unterminated name block · Reading a name block · Reading a polarity · Program of the SAT verifier host · The tokenizer embeds in the SAT verifier host · The embedded lookup meets the lookup contract · Phase 0 of the SAT verifier host · The 3-COLOR emitter machine · Name comparison in the 3-COLOR emitter · Moving an earlier name from \(D\) to \(E\) · Moving the current name from \(T\) to \(A\) · 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 · Load step of the 3-COLOR verifier · Moving one color code in the 3-COLOR verifier · The 3-COLOR verifier machine · Unary reader of the 3-COLOR verifier · Restoring the color stack in the 3-COLOR verifier · 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 · Moving one color code from the color stack · 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 · Program of the clique verifier · The clique verifier's unary reader · 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 · 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 · Moving a walked name from \(D\) to \(E\) · CLIQUE emitter: reading a variable name · The CLIQUE emitter machine · Clique emitter: one clause · Clique emitter: comparing two names · Emitter run over one literal occurrence · Emitter run over a clause's literals · CLIQUE emitter: putting the current occurrence on the walked stack · Walk over the occurrence stack in the CLIQUE emitter · Padding machine embeds the summation machine · Membership transducer embeds the summation machine · Program of the SUBSET-SUM to PARTITION padding machine · Program of the canonical PARTITION membership transducer · 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 · Moving the new sum back · Comparing the sum with the target · Carry phase of the SUBSET-SUM verifier · Carry step of the SUBSET-SUM verifier · Moving the final sum for the comparison · Starting the next number · The SUBSET-SUM verifier program · 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 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: copying a reversed name onto two stacks · HAMPATH emitter, phase A: searching the variable stack for a name · A symbol that reads as a name bit is that bit · Comparing a name with the top entry of the variable stack · The HAMPATH emitter machine · HAMPATH emitter, phase A: one clause · HAMPATH emitter, phase A: one literal · HAMPATH emitter, phase A: the literals of a clause · One literal of the detour walk · Moving the tokens back in the HAMPATH emitter · End of a diamond · The output phase of 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 · Run of the HAMPATH verifier's unary comparison loop · Moving a stack of bits · The Hamiltonian path verifier machine · 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 unary mover of the Hamiltonian path verifier rejects an unterminated number · The unary mover of the Hamiltonian path verifier moves a terminated number · The 3SAT emitter processes one clause · Name copy loop of the 3SAT emitter · One literal of the emitter · The literals of a clause in the emitter · Copying a renamed name · The SAT-to-3SAT emitter machine · Reading the mark of vertex \(j\) · The pass loop of the marking machine · The marking machine for PATH · The unary read instruction · 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 · A walk step with an exhausted counter · Walking along the marks of the PATH marking machine · Walk step of the PATH marking machine

DefinitionTokens of a literal#✓fully proved

For a literal \((n, p)\) with variable index \(n\) and polarity \(p\), the token list is one bit symbol for each bit of the canonical binary representation of \(n\) (least significant bit first, empty for \(n = 0\)), in order, followed by the polarity marker symbol for \(p\).

def litToks (l : ℕ × Bool) : List Sym := (encodeNat l.1).map .bit ++ [.lit l.2]

Uses 1 · Used by 22

Statement usesStack alphabet of the SAT verifier

Used byTokens of a clause · A clause has at most as many tokens as code bits · The clause check · Tokenizer run on one literal · Tokenizer rejects undecodable literals · Reading the literals of a clause · The TM2 SAT verifier · Correctness and step bound of the 3-COLOR emitter · The CLIQUE emitter computes Karp's instance in cubic time · HAMPATH emitter, phase A: one clause · HAMPATH emitter, phase A: one literal · HAMPATH emitter, phase A: the literals of a clause · One clause of the detour walk · One literal of the detour walk · The literals of a clause in the detour walk · The tokens of a literal do not start with a clause end · Phase A of the HAMPATH emitter · End of a diamond · One diamond · Correctness and running time of the HAMPATH emitter · The SAT-to-3SAT emitter writes the encoded translation in quadratic time · Correctness of the clause-length filter

DefinitionTokens of a clause#✓fully proved

The tokens of a CNF clause are the tokens of its literals, in order, followed by the clause-end symbol.

def clauseToks (C : CNFClause) : List Sym := C.flatMap litToks ++ [.cl]

abbrev CNFClause := List (Nat × Bool)

CSLibExt/Logics/Propositional/CNF/Basic.lean:30

inductive Sym
  | bit (b : Bool) | lit (p : Bool) | cl | val (b : Bool) | dead
  deriving DecidableEq

CSLibExt/Computability/Complexity/SatVerifierSpec.lean:41

def litToks (l : ℕ × Bool) : List Sym := (encodeNat l.1).map .bit ++ [.lit l.2]

CSLibExt/Computability/Complexity/SatVerifierSpec.lean:51

Uses 3 · Used by 23

Statement usesStack alphabet of the SAT verifier · Tokens of a literal · CNF clause

Used byA clause has at most as many tokens as code bits · Token sequence of a CNF formula · The clause check · Token count is bounded by the encoding length · Tokenizer run on one clause · Tokenizer rejects undecodable clauses · Tokenizer run on all clauses · Reading the literals of a clause · The TM2 SAT verifier · Clause token length bound for the SAT verifier (moved alias) · Correctness and step bound of the 3-COLOR emitter · The CLIQUE emitter computes Karp's instance in cubic time · HAMPATH emitter, phase A: one clause · HAMPATH emitter, phase A: the clauses of a formula · One clause of the detour walk · The detour walk of a diamond in the HAMPATH emitter · Phase A of the HAMPATH emitter · End of a diamond · The detours of a diamond · One diamond · Correctness and running time of the HAMPATH emitter · The SAT-to-3SAT emitter writes the encoded translation in quadratic time · Correctness of the clause-length filter

DefinitionToken sequence of a CNF formula#✓fully proved

For a CNF formula \(\varphi\) with clauses \(C_1, \dots, C_k\) (in order), the token sequence of \(\varphi\) is the concatenation of the token sequences of \(C_1, \dots, C_k\). The token sequence of a clause is the concatenation of the token sequences of its literals, in order, followed by a clause-end symbol; the token sequence of a literal with variable index \(n \in \mathbb{N}\) and polarity \(p\) is the bits of the binary encoding of \(n\) (Mathlib's encodeNat), each as a name-bit symbol, followed by a polarity marker for \(p\).

The verifier's token stack holds this sequence in reverse order.

def toks (φ : CNF) : List Sym := φ.flatMap clauseToks

abbrev CNF := List CNFClause

CSLibExt/Logics/Propositional/CNF/Basic.lean:33

inductive Sym
  | bit (b : Bool) | lit (p : Bool) | cl | val (b : Bool) | dead
  deriving DecidableEq

CSLibExt/Computability/Complexity/SatVerifierSpec.lean:41

def clauseToks (C : CNFClause) : List Sym := C.flatMap litToks ++ [.cl]

CSLibExt/Computability/Complexity/SatVerifierSpec.lean:54

Uses 4 · Used by 29

Statement usesStack alphabet of the SAT verifier · Tokens of a clause · CNF formula · CNF clause

Used byTokenizer of the SAT verifier · The clause check · Token count is bounded by the encoding length · Tokenizer run on all clauses · Rejecting run · Accepting run of the SAT tokenizer · Driver stacks after tokenization · The TM2 SAT verifier · Token length bound for the SAT verifier (moved alias) · Correctness and step bound of the 3-COLOR emitter · The 3-COLOR emitter · The CLIQUE emitter computes Karp's instance in cubic time · The CLIQUE emitter · HAMPATH emitter, phase A: the clauses of a formula · The emitter state before the diamonds · The detour walk of a diamond in the HAMPATH emitter · Initial state of the HAMPATH emitter · Phase A of the HAMPATH emitter · End of a diamond · The detours of a diamond · One diamond · The diamonds · Correctness and running time of the HAMPATH emitter · The HAMPATH emitter · The SAT-to-3SAT emitter · Emitter · The SAT-to-3SAT emitter writes the encoded translation in quadratic time · Correctness of the clause-length filter · Tokenize, then emit

AbbreviationTable entries#✓fully proved

A table entry is a pair of a name, which is a list of bits, and an optional bit, its value; the value is absent for occurrences past the end of the witness.

abbrev Ent := List Bool × Option Bool

Used by 21

DefinitionClosing marker of a table entry#✓fully proved

The marker closing a table entry whose value is the boolean \(b\) is the value symbol for \(b\); for an entry with no value it is the dead symbol.

def markOf : Option Bool → Sym
  | some b => .val b
  | none => .dead

Uses 1 · Used by 7

Statement usesStack alphabet of the SAT verifier

Used bySymbols of a table entry · The return loop of the lookup machine · One scan step of the lookup · The scan loop of the lookup machine · Tokenizer run on one literal · Reading a polarity · The TM2 SAT verifier

DefinitionSymbols of a table entry#✓fully proved

The symbols of a table entry with name \(q\) and value \(v\) are the bits of \(q\) as name-bit symbols, in order, followed by one closing marker: the value marker of \(b\) if \(v\) is a bit \(b\), and the dead marker if \(v\) is absent.

def entToks (e : Ent) : List Sym := e.1.map .bit ++ [markOf e.2]

abbrev Ent := List Bool × Option Bool

CSLibExt/Computability/Complexity/SatVerifierSpec.lean:60

inductive Sym
  | bit (b : Bool) | lit (p : Bool) | cl | val (b : Bool) | dead
  deriving DecidableEq

CSLibExt/Computability/Complexity/SatVerifierSpec.lean:41

def markOf : Option Bool → Sym
  | some b => .val b
  | none => .dead

CSLibExt/Computability/Complexity/SatVerifierSpec.lean:63

Uses 3 · Used by 10

Statement usesTable entries · Stack alphabet of the SAT verifier · Closing marker of a table entry

Used byTable stack of an entry list · The return loop of the lookup machine · One scan step of the lookup · Correctness of the SAT-verifier lookup machine · The scan loop of the lookup machine · Tokenizer run on all clauses · Tokenizer run on one literal · Tokenizer rejects undecodable literals · Reading the literals of a clause · The TM2 SAT verifier

DefinitionTable stack of an entry list#✓fully proved

Write each table entry as one bit symbol per bit of its name followed by its closing marker (the value symbol for its value, or the dead symbol if it has no value), and concatenate these in the order of the list. The table stack is the reverse of this sequence, with the head as the top of the stack, so the first entry lies at the bottom.

def tblStk (es : List Ent) : List Sym := (es.flatMap entToks).reverse

abbrev Ent := List Bool × Option Bool

CSLibExt/Computability/Complexity/SatVerifierSpec.lean:60

inductive Sym
  | bit (b : Bool) | lit (p : Bool) | cl | val (b : Bool) | dead
  deriving DecidableEq

CSLibExt/Computability/Complexity/SatVerifierSpec.lean:41

def entToks (e : Ent) : List Sym := e.1.map .bit ++ [markOf e.2]

CSLibExt/Computability/Complexity/SatVerifierSpec.lean:68

Uses 3 · Used by 18

Statement usesTable entries · Stack alphabet of the SAT verifier · Symbols of a table entry

Used byTokenizer of the SAT verifier · 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 · 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 · Reading the literals of a clause · Rejecting run · Accepting run of the SAT tokenizer · Driver stacks after tokenization · The embedded lookup meets the lookup contract · The TM2 SAT verifier · Tokenize, then emit

DefinitionOccurrence table of a list of variables#✓fully proved

Given natural numbers \(n_0, \dots, n_{k-1}\) and a list \(w\) of bits, the occurrence table is the list of \(k\) table entries whose \(i\)-th entry has as name the binary code of \(n_i\) (Mathlib's encoding of natural numbers as bit lists) and as value the bit \(w_i\) if \(i\) is less than the length of \(w\), and no value otherwise.

def entsOf : List ℕ → List Bool → List Ent
  | [], _ => []
  | n :: ns, [] => (encodeNat n, none) :: entsOf ns []
  | n :: ns, b :: bs => (encodeNat n, some b) :: entsOf ns bs

Uses 1 · Used by 11

Statement usesTable entries

Used byOccurrence table of a formula and a witness · Table lookup agrees with the verifier's variable lookup · Tokenizer run on one clause · Tokenizer rejects undecodable clauses · Tokenizer run on all clauses · Occurrence table of a nonempty list · Reading the literals of a clause · Rejecting run · Accepting run of the SAT tokenizer · Name lengths in an occurrence table · The TM2 SAT verifier

DefinitionOccurrence table of a formula and a witness#✓fully proved

Let \(\varphi\) be a CNF formula, \(w\) a list of booleans, and \(n_0, \dots, n_{k-1}\) the variable indices of the literals of \(\varphi\) in reading order, with repetitions. The occurrence table is the list of \(k\) entries whose \(i\)-th entry pairs the binary name of \(n_i\) (its canonical binary representation, least significant bit first, empty for \(0\)) with the value \(w_i\) if \(i\) is less than the length of \(w\), and with no value otherwise.

def ents (φ : CNF) (w : List Bool) : List Ent := entsOf (varsOf φ) w

abbrev CNF := List CNFClause

CSLibExt/Logics/Propositional/CNF/Basic.lean:33

abbrev Ent := List Bool × Option Bool

CSLibExt/Computability/Complexity/SatVerifierSpec.lean:60

def entsOf : List ℕ → List Bool → List Ent
  | [], _ => []
  | n :: ns, [] => (encodeNat n, none) :: entsOf ns []
  | n :: ns, b :: bs => (encodeNat n, some b) :: entsOf ns bs

CSLibExt/Computability/Complexity/SatVerifierSpec.lean:74

def varsOf (φ : CNF) : List Nat := φ.flatMap fun C => C.map Prod.fst

CSLibExt/Computability/SatTimeM.lean:70

Uses 4 · Used by 10

Statement usesTable entries · Occurrence table of a list of variables · Occurrence list of a CNF formula · CNF formula

Used byThe clause check on the occurrence table is the formula check · The SAT verifier's answer through the occurrence table · Tokenizer of the SAT verifier · Accepting run of the SAT tokenizer · Answer of the SAT host · Driver stacks after tokenization · The SAT verifier is polynomial-time · The TM2 SAT verifier · Answer of the SAT host with the three-literal filter · Tokenize, then emit

DefinitionLive value of a name in a table#✓fully proved

Given a list of table entries, each pairing a name (a bit string) with either a boolean value or no value, and a bit string \(q\), the live value of \(q\) is the value of the first entry whose name is \(q\) and which carries a value, or false if there is no such entry.

def liveVal (es : List Ent) (q : List Bool) : Bool :=
  (es.findSome? fun e => if e.1 = q then e.2 else none).getD false

Uses 1 · Used by 11

Statement usesTable entries

Used byClause check against an occurrence table · The clause check on the occurrence table is the formula check · Table lookup agrees with the verifier's variable lookup · Clause loop of the clause check · Literal loop of the clause check · The lookup contract · The clause check · One scan step of the lookup · Correctness of the SAT-verifier lookup machine · The scan loop of the lookup machine · The embedded lookup meets the lookup contract

DefinitionClause check against an occurrence table#✓fully proved

For a CNF formula \(\varphi\) and a list \(es\) of table entries, the clause check is true exactly when every clause of \(\varphi\) contains a literal \((x, p)\) whose live value equals its polarity \(p\). Here the live value of \(x\) is the value of the first entry of \(es\) that is named by the binary code of \(x\) and has a value, and false if there is no such entry.

def checkSpec (φ : CNF) (es : List Ent) : Bool :=
  φ.all fun C => C.any fun l => liveVal es (encodeNat l.1) == l.2

abbrev CNF := List CNFClause

CSLibExt/Logics/Propositional/CNF/Basic.lean:33

abbrev Ent := List Bool × Option Bool

CSLibExt/Computability/Complexity/SatVerifierSpec.lean:60

def liveVal (es : List Ent) (q : List Bool) : Bool :=
  (es.findSome? fun e => if e.1 = q then e.2 else none).getD false

CSLibExt/Computability/Complexity/SatVerifierSpec.lean:83

Uses 4 · Used by 7

Statement usesTable entries · Live value of a name in a table · CNF formula · CNF clause

Used byThe clause check on the occurrence table is the formula check · The SAT verifier's answer through the occurrence table · The clause check · Answer of the SAT host · The SAT verifier is polynomial-time · The TM2 SAT verifier · Answer of the SAT host with the three-literal filter

DefinitionTokenizer of the SAT verifier#✓fully proved

Given bit strings \(x\) and \(w\), the tokenizer rejects (returns no result) if \(x\) does not decode to a CNF formula. If \(x\) decodes to a formula \(\varphi\), it returns the pair consisting of the token stack, the reverse of the tokens of \(\varphi\) in reading order, and the table stack of the occurrence table of \(\varphi\) and \(w\).

def tokenize (x w : List Bool) : Option (List Sym × List Sym) :=
  (decodeCNF x).map fun φ => ((toks φ).reverse, tblStk (ents φ w))

inductive Sym
  | bit (b : Bool) | lit (p : Bool) | cl | val (b : Bool) | dead
  deriving DecidableEq

CSLibExt/Computability/Complexity/SatVerifierSpec.lean:41

def decodeCNF (input : List Bool) : Option CNF := do
  let (φ, rest) ← decodeCNFAux input
  if rest.isEmpty then some φ else none

CSLibExt/Computability/CookLevin.lean:108

def toks (φ : CNF) : List Sym := φ.flatMap clauseToks

CSLibExt/Computability/Complexity/SatVerifierSpec.lean:57

def tblStk (es : List Ent) : List Sym := (es.flatMap entToks).reverse

CSLibExt/Computability/Complexity/SatVerifierSpec.lean:71

def ents (φ : CNF) (w : List Bool) : List Ent := entsOf (varsOf φ) w

CSLibExt/Computability/Complexity/SatVerifierSpec.lean:80

Uses 6

Statement usesStack alphabet of the SAT verifier · 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 · CNF formula

TheoremThe binary code of natural numbers is injective#✓fully proved

For natural numbers \(m\) and \(n\), the binary codes of \(m\) and \(n\) (Mathlib's encoding of natural numbers as bit lists) are equal if and only if \(m = n\).

theorem encodeNat_inj {m n : ℕ} : encodeNat m = encodeNat n ↔ m = n

Used by 6

Used byTable lookup agrees with the verifier's variable lookup · One step of the walk over earlier occurrences · Walk over the occurrence stack in the CLIQUE emitter · The SUBSET-SUM verifier machine · HAMPATH emitter, phase A: searching the variable stack for a name · One literal of the detour walk

TheoremCanonical binary names#✓fully proved

For every list \(l\) of bits, encoding the natural number that \(l\) decodes to (Mathlib's binary code of natural numbers, least significant bit first) gives back \(l\) if and only if \(l\) is empty or its last bit is true.

theorem encodeNat_decodeNat_eq_iff (l : List Bool) :
    encodeNat (decodeNat l) = l ↔ l = [] ∨ l.getLast? = some true

Used by 2

Used byName-loop outcome from the start of a name · Canonical binary strings are those not ending in zero

TheoremTable lookup agrees with the verifier's variable lookup#✓fully proved

Let \(n = (n_0, \dots, n_{k-1})\) be a list of natural numbers, \(w\) a list of booleans and \(x\) a natural number. Write \([m]\) for the binary name of a natural number \(m\): its canonical binary representation, least significant bit first, empty for \(m = 0\). Form the table whose \(i\)-th entry, for \(i < k\), pairs \([n_i]\) with \(w_i\) if \(i\) is less than the length of \(w\), and with no value otherwise. Then the live value of \([x]\) in this table (the value of the first entry named \([x]\) that carries a value, or false if there is none) equals the return value of the verifier's lookup of \(x\) in the lists \(n\) and \(w\): the value \(w_i\) for the first \(i\) below both \(k\) and the length of \(w\) with \(n_i = x\), or false if there is none.

theorem liveVal_entsOf (ns : List ℕ) (w : List Bool) (x : ℕ) :
    liveVal (entsOf ns w) (encodeNat x) = (lookupVar ns w x).ret

def liveVal (es : List Ent) (q : List Bool) : Bool :=
  (es.findSome? fun e => if e.1 = q then e.2 else none).getD false

CSLibExt/Computability/Complexity/SatVerifierSpec.lean:83

def entsOf : List ℕ → List Bool → List Ent
  | [], _ => []
  | n :: ns, [] => (encodeNat n, none) :: entsOf ns []
  | n :: ns, b :: bs => (encodeNat n, some b) :: entsOf ns bs

CSLibExt/Computability/Complexity/SatVerifierSpec.lean:74

def lookupVar : List Nat → List Bool → Nat → TimeM Nat Bool
  | [], _, _ => pure false
  | _, [], _ => pure false
  | n :: ns, b :: bs, x =>
      TimeM.tick 1 >>= fun _ =>
        if x = n then pure b else lookupVar ns bs x

CSLibExt/Computability/SatTimeM.lean:75

Uses 5 · Used by 1

Statement usesOccurrence table of a list of variables · Live value of a name in a table · Witness lookup

Proof usesTable entries · The binary code of natural numbers is injective

Used byThe clause check on the occurrence table is the formula check

TheoremThe clause check on the occurrence table is the formula check#✓fully proved

For every CNF formula \(\varphi\) and every list \(w\) of bits, the clause check of \(\varphi\) against the occurrence table of \(\varphi\) and \(w\) equals the value returned (ignoring the time count) by the formula check of \(\varphi\) against \(w\) that uses the variable occurrences of \(\varphi\), in order, as its variable list.

theorem checkSpec_ents (φ : CNF) (w : List Bool) :
    checkSpec φ (ents φ w) = (checkCNF (varsOf φ) w φ).ret

abbrev CNF := List CNFClause

CSLibExt/Logics/Propositional/CNF/Basic.lean:33

def checkSpec (φ : CNF) (es : List Ent) : Bool :=
  φ.all fun C => C.any fun l => liveVal es (encodeNat l.1) == l.2

CSLibExt/Computability/Complexity/SatVerifierSpec.lean:87

def ents (φ : CNF) (w : List Bool) : List Ent := entsOf (varsOf φ) w

CSLibExt/Computability/Complexity/SatVerifierSpec.lean:80

def checkCNF (vars : List Nat) (w : List Bool) : CNF → TimeM Nat Bool
  | [] => pure true
  | C :: Cs =>
      checkClause vars w C >>= fun ok =>
        if ok = true then checkCNF vars w Cs else pure false

CSLibExt/Computability/SatTimeM.lean:94

def varsOf (φ : CNF) : List Nat := φ.flatMap fun C => C.map Prod.fst

CSLibExt/Computability/SatTimeM.lean:70

Uses 12 · Used by 1

Statement usesClause check against an occurrence table · Occurrence table of a formula and a witness · Formula check against a witness · Occurrence list of a CNF formula · CNF formula

Proof usesLive value of a name in a table · Table lookup agrees with the verifier's variable lookup · Correctness of the witness formula check · Witness lookup · Satisfaction of a CNF formula · CNF clause · Satisfaction of a clause

Used byThe SAT verifier's answer through the occurrence table

TheoremThe SAT verifier's answer through the occurrence table#✓fully proved

For all lists \(x\) and \(w\) of bits, the value returned by the SAT verifier on \((x, w)\), ignoring the time count, is false if the complete length-prefixed CNF decoder fails on \(x\), and is the clause check of \(\varphi\) against the occurrence table of \(\varphi\) and \(w\) if \(x\) decodes to the CNF formula \(\varphi\).

theorem satVerifier_ret_eq (x w : List Bool) :
    (satVerifier (x, w)).ret = ((decodeCNF x).map fun φ => checkSpec φ (ents φ w)).getD false

def satVerifier : List Bool × List Bool → TimeM Nat Bool := fun xw =>
  match decodeCNF xw.1 with
  | none => pure false
  | some φ => checkCNF (varsOf φ) xw.2 φ

CSLibExt/Computability/SatTimeM.lean:103

def decodeCNF (input : List Bool) : Option CNF := do
  let (φ, rest) ← decodeCNFAux input
  if rest.isEmpty then some φ else none

CSLibExt/Computability/CookLevin.lean:108

def checkSpec (φ : CNF) (es : List Ent) : Bool :=
  φ.all fun C => C.any fun l => liveVal es (encodeNat l.1) == l.2

CSLibExt/Computability/Complexity/SatVerifierSpec.lean:87

def ents (φ : CNF) (w : List Bool) : List Ent := entsOf (varsOf φ) w

CSLibExt/Computability/Complexity/SatVerifierSpec.lean:80

Uses 10 · Used by 2

Statement usesClause check against an occurrence table · Occurrence table of a formula and a witness · Decoding a complete length-prefixed CNF formula · The SAT verifier · CNF formula

Proof usesThe clause check on the occurrence table is the formula check · Formula check against a witness · The SAT verifier rejects undecodable inputs · The SAT verifier on a decodable input · Occurrence list of a CNF formula

Used byThe SAT verifier is polynomial-time · Answer of the SAT host with the three-literal filter

TheoremA clause has at most as many tokens as code bits#✓fully proved

For every CNF clause \(C\), the number of tokens of \(C\) is at most the length of the binary code of \(C\).

theorem clauseToks_length_le (C : CNFClause) :
    (clauseToks C).length ≤ (encodeClause C).length

abbrev CNFClause := List (Nat × Bool)

CSLibExt/Logics/Propositional/CNF/Basic.lean:30

def clauseToks (C : CNFClause) : List Sym := C.flatMap litToks ++ [.cl]

CSLibExt/Computability/Complexity/SatVerifierSpec.lean:54

def encodeClause (C : CNFClause) : List Bool :=
  List.replicate C.length true ++ false :: C.flatMap encodeLit

CSLibExt/Computability/CookLevin.lean:82

Uses 7 · Used by 2

Statement usesStack alphabet of the SAT verifier · Tokens of a clause · Length-prefixed binary code of a clause · CNF clause

Proof usesTokens of a literal · Binary code of a literal · Self-delimiting form of a bitstring

Used byToken count is bounded by the encoding length · Clause token length bound for the SAT verifier (moved alias)

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.