Token count is bounded by the encoding length to The lookup program

TheoremToken count is bounded by the encoding length#✓fully proved

For every CNF formula \(\varphi\), the number of tokens of \(\varphi\) is at most the length of the binary encoding of \(\varphi\).

theorem toks_length_le (φ : CNF) : (toks φ).length ≤ (encodeCNF φ).length

Uses 8 · Used by 3

Statement usesStack alphabet of the SAT verifier · Token sequence of a CNF formula · Length-prefixed binary code of a CNF formula · CNF formula

Proof usesTokens of a clause · A clause has at most as many tokens as code bits · Length-prefixed binary code of a clause · CNF clause

Used byThe TM2 SAT verifier · Token length bound for the SAT verifier (moved alias) · Tokenize, then emit

InductiveStacks of the clause check#✓fully proved

The eight stacks of the clause-check machine: \(T\) (tokens), \(B\) (table), \(S\) (the lookup's stash), \(A\) and \(C\) (the lookup's scratch stacks), \(V\) (looked-up value), \(P\) (polarity) and \(F\) (clause flag).

inductive K | T | B | S | A | C | V | P | F
  deriving DecidableEq

Used by 18

Used byCalling the lookup · Configurations of the clause-check machine · Clause loop of the clause check · The clause-check driver · Literal loop of the clause check · The lookup contract · The clause check · Clause-check statements · Driver stacks in the SAT host · Placement of the lookup's stacks in the clause-check driver · Stack embedding of the clause-check driver into the host · Stack embedding of the lookup into the clause-check driver · Program of the SAT verifier host · The embedded lookup program · Driver stacks after tokenization · The tokenizer embeds in the SAT verifier host · The embedded lookup meets the lookup contract · The TM2 SAT verifier

InductiveDriver labels of the clause check#✓fully proved

The seven labels of the clause-check driver: start (begin the next clause), lits (read the next literal), ret (return from the lookup), drop (discard a literal's name bits), endc (end of a clause), yes (accept) and no (reject).

inductive DLab | start | lits | ret | drop | endc | yes | no
  deriving DecidableEq

Used by 20

Used byCalling the lookup · Configurations of the clause-check machine · Clause loop of the clause check · The clause-check driver · Literal loop of the clause check · The lookup contract · The clause-check driver with a lookup sub-program · The clause check · Clause-check statements · Driver labels in the SAT host · Host labels as a sum type · Filter exits in the SAT verifier host · Labels of the SAT verifier host · Program of the SAT verifier host · Lookup labels in the clause-check driver · The embedded lookup program · The tokenizer embeds in the SAT verifier host · The embedded lookup meets the lookup contract · The SAT verifier machine · The TM2 SAT verifier

AbbreviationClause-check statements#✓fully proved

For a label set \(L\), the statements of a multi-stack Turing machine with the eight driver stacks, each over the symbols of the token and table stacks, with labels in \(D \sqcup L\), where \(D\) is the set of driver labels, and with a Boolean internal state.

abbrev Stmt (LL : Type) := TM2.Stmt (fun _ : K => Sym) (DLab ⊕ LL) Bool

Uses 3 · Used by 9

Statement usesDriver labels of the clause check · Stacks of the clause check · Stack alphabet of the SAT verifier

Used byCalling the lookup · Clause loop of the clause check · The clause-check driver · Literal loop of the clause check · The lookup contract · The clause-check driver with a lookup sub-program · The clause check · The embedded lookup program · The embedded lookup meets the lookup contract

AbbreviationConfigurations of the clause-check machine#✓fully proved

For a type \(LL\) of lookup labels, a configuration of the multi-stack Turing machine of the clause check: a current label (absent once the machine halts) that is either a driver label or a label in \(LL\), a Boolean internal state, and the contents of the eight stacks \(T\), \(B\), \(S\), \(A\), \(C\), \(V\), \(P\), \(F\) of the clause check, each a list of symbols of the token and table stacks (name bits, literal and clause markers, and table markers).

abbrev Cfg (LL : Type) := TM2.Cfg (fun _ : K => Sym) (DLab ⊕ LL) Bool

Uses 3

Statement usesDriver labels of the clause check · Stacks of the clause check · Stack alphabet of the SAT verifier

DefinitionCalling the lookup#✓fully proved

For the lookup's start label \(l_0\) and a polarity \(p\), the statement that pops the top of the token stack \(T\), pushes the bit \(p\) onto the polarity stack \(P\), and then goes to label \(l_0\).

def callS (l0 : LL) (p : Bool) : Stmt LL :=
  .pop .T (fun s _ => s) (.push .P (fun _ => .bit p) (.goto fun _ => .inr l0))

Uses 4 · Used by 2

Statement usesDriver labels of the clause check · Stacks of the clause check · Clause-check statements · Stack alphabet of the SAT verifier

Used byThe clause-check driver · Literal loop of the clause check

DefinitionThe clause-check driver#✓fully proved

Given the lookup's start label \(l_0\), the statement at each driver label. At start: if the token stack \(T\) is empty, go to yes; if its top is a clause marker, pop it, push the bit false onto the flag stack \(F\) and go to lits; otherwise go to no. At lits: if the top of \(T\) is a literal marker of polarity \(p\), pop it, push the bit \(p\) onto the polarity stack \(P\) and go to \(l_0\); otherwise go to endc. At ret: if the top of the value stack \(V\) is the bit true exactly when the top of \(P\) is the bit true, pop \(F\) and push the bit true onto it; in either case then pop \(V\), pop \(P\) and go to drop. At drop: if the top of \(T\) is a bit, pop it and go to drop; otherwise go to lits. At endc: if the top of \(F\) is the bit true, pop it and go to start; otherwise go to no. At yes and at no: halt.

Cslib.Complexity.SatVerifier.Check.drv · 19 lines

def drv (l0 : LL) : DLab → Stmt LL
  | .start => .peek .T (fun _ o => o.isNone) <| .branch id (.goto fun _ => .inl .yes) <|
      .peek .T (fun _ o => o == some .cl) <| .branch id
        (.pop .T (fun s _ => s) (.push .F (fun _ => .bit false) (.goto fun _ => .inl .lits)))
        (.goto fun _ => .inl .no)
  | .lits => .peek .T (fun _ o => o == some (.lit true)) <| .branch id (callS l0 true) <|
      .peek .T (fun _ o => o == some (.lit false)) <| .branch id (callS l0 false)
        (.goto fun _ => .inl .endc)
  | .ret => .peek .V (fun _ o => o == some (.bit true)) <|
      .peek .P (fun s o => s == (o == some (.bit true))) <| .branch id
        (.pop .F (fun s _ => s) <| .push .F (fun _ => .bit true) <|
          .pop .V (fun s _ => s) <| .pop .P (fun s _ => s) <| .goto fun _ => .inl .drop)
        (.pop .V (fun s _ => s) <| .pop .P (fun s _ => s) <| .goto fun _ => .inl .drop)
  | .drop => .peek .T (fun _ o => isBit Sym.bit? o) <| .branch id
      (.pop .T (fun s _ => s) (.goto fun _ => .inl .drop)) (.goto fun _ => .inl .lits)
  | .endc => .peek .F (fun _ o => o == some (.bit true)) <| .branch id
      (.pop .F (fun s _ => s) (.goto fun _ => .inl .start)) (.goto fun _ => .inl .no)
  | .yes => .halt
  | .no => .halt

Uses 7 · Used by 2

Statement usesDriver labels of the clause check · Stacks of the clause check · Clause-check statements · Calling the lookup · Stack alphabet of the SAT verifier · Reading a symbol as a name bit · Bit test for the top of a stack

Used byThe clause-check driver with a lookup sub-program · The embedded lookup meets the lookup contract

DefinitionThe clause-check driver with a lookup sub-program#✓fully proved

Given a lookup sub-program \(lk\) on a label set \(L\) and an entry label \(l_0 \in L\), this is the program on the labels \(D \sqcup L\), where \(D\) is the set of driver labels: at a driver label \(d\) it runs the driver's statement for \(d\) (the driver calls the lookup by jumping to \(l_0\)), and at a label \(l \in L\) it runs \(lk(l)\).

def prog (lk : LL → Stmt LL) (l0 : LL) : DLab ⊕ LL → Stmt LL
  | .inl d => drv l0 d
  | .inr l => lk l

Uses 3 · Used by 8

Statement usesDriver labels of the clause check · Clause-check statements · The clause-check driver

Used byClause loop of the clause check · Literal loop of the clause check · The lookup contract · The clause check · 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

DefinitionThe lookup contract#✓fully proved

A lookup sub-program \(lk\) with start label \(l_0\) meets the contract with constants \(a\) and \(b\) when the following holds. For every name \(q\) (a list of bits), every table \(es\), with table stack \(B_{es}\), and every list of symbols \(R\) whose first symbol, if any, is not a bit, start the clause-check machine with lookup \(lk\) at label \(l_0\), with any internal state and with stack contents that have the bits of \(q\) in reverse order followed by \(R\) on the token stack \(T\), \(B_{es}\) on \(B\), and \(S\), \(A\), \(C\), \(V\) empty. Then it reaches label ret in at most \(a \cdot |B_{es}| + b\) steps, with some internal state, with \(V\) holding exactly the bit that is the live value of \(q\) in \(es\), and with every other stack unchanged.

def LookupSpec (lk : LL → Stmt LL) (l0 : LL) (a b : ℕ) : Prop :=
  ∀ (q : List Bool) (es : List Ent) (R : List Sym), R.head?.bind Sym.bit? = none →
    ∀ (v : Bool) (St : ∀ _ : K, List Sym), St .T = (q.map Sym.bit).reverse ++ R →
      St .B = tblStk es → St .S = [] → St .A = [] → St .C = [] → St .V = [] →
      ∃ v', RunLe (prog lk l0) (a * (tblStk es).length + b) ⟨some (.inr l0), v, St⟩
        ⟨some (.inl .ret), v', update St .V [Sym.bit (liveVal es q)]⟩

Uses 10 · Used by 4

Statement usesDriver labels of the clause check · Stacks of the clause check · Clause-check statements · The clause-check driver with a lookup sub-program · Table entries · 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

Used byClause loop of the clause check · Literal loop of the clause check · The clause check · The embedded lookup meets the lookup contract

DefinitionA literal's tokens on the token stack#✓fully proved

For a literal \((n, p)\) with variable index \(n\) and polarity \(p\), the list of symbols consisting of the literal marker of polarity \(p\) followed by the bits of the binary encoding of \(n\) (least significant bit first, empty for \(n = 0\)) in reverse order.

def litRev (l : ℕ × Bool) : List Sym := .lit l.2 :: ((encodeNat l.1).map Sym.bit).reverse

Uses 1 · Used by 31

Statement usesStack alphabet of the SAT verifier

Used byA clause's tokens on the token stack · Clause loop of the clause check · Literal loop of the clause check · The clause check · The 3-COLOR emitter processes one clause · The emitter on a list of clauses · The emitter processes the remaining literals of a clause · The size invariant survives a new literal occurrence · Emitting one literal occurrence · Correctness and step bound of the 3-COLOR emitter · Clique emitter: one clause · Emitter run over a formula's clauses · Emitter run over one literal occurrence · Emitter run over a clause's literals · The CLIQUE emitter computes Karp's instance in cubic time · HAMPATH emitter, phase A: one clause · HAMPATH emitter, phase A: the clauses of a formula · HAMPATH emitter, phase A: one literal · HAMPATH emitter, phase A: the literals of a clause · Phase A of the HAMPATH emitter · A clause with more than three literals makes the capped 3SAT filter fail · The 3SAT filter walks one clause within the cap · The 3SAT emitter processes one clause · One literal of the emitter · The capped filter fails on a clause with too many literals · The filter walks a clause's literals within the cap · The literals of a clause in the emitter · The SAT-to-3SAT emitter writes the encoded translation in quadratic time · Correctness of the clause-length filter · Walking over a literal advances the literal count · A capped walk fails on a literal past the third

DefinitionA clause's tokens on the token stack#✓fully proved

For a clause with literals \(l_1, \dots, l_k\), the list of symbols consisting of the clause marker followed by the stack tokens of \(l_k\), then of \(l_{k-1}\), down to \(l_1\), where the stack tokens of a literal \((n, p)\) are the literal marker of polarity \(p\) followed by the bits of the binary encoding of \(n\) (least significant bit first, empty for \(n = 0\)) in reverse order.

def clRev (C : CNFClause) : List Sym := .cl :: C.reverse.flatMap litRev

Uses 3 · Used by 19

Statement usesA literal's tokens on the token stack · Stack alphabet of the SAT verifier · CNF clause

Used byClause loop of the clause check · The clause check · The 3-COLOR emitter processes one clause · The emitter on a list of clauses · Correctness and step bound of the 3-COLOR emitter · Clique emitter: one clause · Emitter run over a formula's clauses · 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 · Phase A of the HAMPATH emitter · A clause with more than three literals makes the capped 3SAT filter fail · The 3SAT filter walks one clause within the cap · The 3SAT emitter processes one clause · A long clause makes the capped 3SAT filter fail on a list of clauses · The 3SAT filter walks a list of clauses within the cap · The 3SAT emitter processes a whole formula · The SAT-to-3SAT emitter writes the encoded translation in quadratic time · Correctness of the clause-length filter

TheoremLiteral loop of the clause check#✓fully proved

Suppose the lookup sub-program \(lk\) with start label \(l_0\) meets the lookup contract with constants \(a\) and \(b\). Let \(es\) be a table with table stack \(B_{es}\), let \(R\) be a list of symbols that is empty or starts with a clause marker, and let \(s\) be a bit. The stack tokens of a literal \((n, p)\) are the literal marker of polarity \(p\) followed by the bits of the binary encoding of \(n\) (least significant bit first, empty for \(n = 0\)) in reverse order. Let \(l_1, \dots, l_k\) be literals whose stack tokens have total length \(N\). Start the clause-check machine with lookup \(lk\) at label lits, with any internal state and with the stack tokens of \(l_1\), then of \(l_2\), up to \(l_k\), followed by \(R\) on the token stack \(T\), \(B_{es}\) on \(B\), the single bit \(s\) on the flag stack \(F\), and \(S\), \(A\), \(C\), \(V\), \(P\) empty. Then it reaches label endc in at most \(k \cdot (a \cdot |B_{es}| + b + 2) + N + 1\) steps, with some internal state, with \(T\) holding \(R\), with \(F\) holding the single bit that is true exactly when \(s\) is true or some literal \(l_i = (n, p)\) has live value of the binary encoding of \(n\) in \(es\) equal to \(p\), and with every other stack unchanged.

theorem lits_run (hlk : LookupSpec lk l0 a b) (es : List Ent) (R : List Sym)
    (hR : R = [] ∨ R.head? = some .cl) :
    ∀ (Ls : List (ℕ × Bool)) (s v : Bool) (St : ∀ _ : K, List Sym),
      St .T = Ls.flatMap litRev ++ R → St .B = tblStk es → St .S = [] → St .A = [] →
      St .C = [] → St .V = [] → St .P = [] → St .F = [.bit s] →
      ∃ v', RunLe (prog lk l0)
        (Ls.length * (a * (tblStk es).length + b + 2) + (Ls.flatMap litRev).length + 1)
        ⟨some (.inl .lits), v, St⟩ ⟨some (.inl .endc), v', update (update St .T R) .F
          [.bit (s || Ls.any fun l => liveVal es (encodeNat l.1) == l.2)]⟩

Uses 16 · Used by 1

Statement usesDriver labels of the clause check · Stacks of the clause check · The lookup contract · Clause-check statements · A literal's tokens on the token stack · The clause-check driver with a lookup sub-program · Table entries · Stack alphabet of the SAT verifier · Live value of a name in a table · Table stack of an entry list · Runs within a step budget

Proof usesCalling the lookup · Reading a symbol as a name bit · Exact-length runs of a TM2 machine · A single step executes the statement at the current label · Bit test for the top of a stack

Used byClause loop of the clause check

TheoremClause loop of the clause check#✓fully proved

Suppose the lookup sub-program \(lk\) with start label \(l_0\) meets the lookup contract with constants \(a\) and \(b\). Let \(es\) be a table with table stack \(B_{es}\), and let \(\varphi\) be a CNF formula with clauses \(D_1, \dots, D_m\). The stack tokens of a clause are its clause marker followed by the stack tokens of its literals, last literal first, where the stack tokens of a literal \((n, p)\) are the literal marker of polarity \(p\) followed by the bits of the binary encoding of \(n\) (least significant bit first, empty for \(n = 0\)) in reverse order. Let \(N\) be the total length of the stack tokens of \(D_1, \dots, D_m\). Start the clause-check machine with lookup \(lk\) at label start, with any internal state and with the stack tokens of \(D_1\), then of \(D_2\), up to \(D_m\) on the token stack \(T\), \(B_{es}\) on \(B\), and \(S\), \(A\), \(C\), \(V\), \(P\), \(F\) empty. Then within \(N \cdot (a \cdot |B_{es}| + b + 5) + 1\) steps it reaches, with some internal state and some stack contents, label yes if every clause \(D_j\) has a literal \((n, p)\) such that the live value of the binary encoding of \(n\) in \(es\) is \(p\), and label no otherwise.

theorem clauses_run (hlk : LookupSpec lk l0 a b) (es : List Ent) :
    ∀ (Cs : CNF) (v : Bool) (St : ∀ _ : K, List Sym),
      St .T = Cs.flatMap clRev → St .B = tblStk es → St .S = [] → St .A = [] →
      St .C = [] → St .V = [] → St .P = [] → St .F = [] →
      ∃ v' S', RunLe (prog lk l0)
        ((Cs.flatMap clRev).length * (a * (tblStk es).length + b + 5) + 1)
        ⟨some (.inl .start), v, St⟩ ⟨some (.inl (if Cs.all (fun C => C.any fun l =>
          liveVal es (encodeNat l.1) == l.2) then .yes else .no)), v', S'⟩

Uses 17 · Used by 1

Statement usesDriver labels of the clause check · Stacks of the clause check · The lookup contract · Clause-check statements · A clause's tokens on the token stack · The clause-check driver with a lookup sub-program · Table entries · Stack alphabet of the SAT verifier · Live value of a name in a table · Table stack of an entry list · CNF formula · CNF clause · Runs within a step budget

Proof usesA literal's tokens on the token stack · Literal loop of the clause check · Exact-length runs of a TM2 machine · A single step executes the statement at the current label

Used byThe clause check

TheoremThe clause check#✓fully proved

Suppose the lookup sub-program \(lk\) with entry label \(l_0\) satisfies the lookup contract with constants \(a, b \in \mathbb{N}\). Let \(\varphi\) be a CNF formula, \(es\) a list of table entries, \(t\) the token list of \(\varphi\) and \(m\) the length of the table stack of \(es\). Start the driver with lookup \(lk\) at its start label, with any internal state, with \(t\) reversed on the token stack, the table stack of \(es\) on the table stack, and the other six stacks empty. Then within at most \(|t| \cdot (a m + b + 5) + 1\) steps it reaches the label yes, with some internal state and some stack contents, if every clause of \(\varphi\) has a literal whose polarity equals the value of its variable, and it reaches the label no otherwise. Here the value of a variable \(n\) is the value of the first entry of \(es\) that is named by the binary encoding of \(n\) and has a value, or false if there is no such entry.

theorem run {lk : LL → Stmt LL} {l0 : LL} {a b : ℕ} (hlk : LookupSpec lk l0 a b) (φ : CNF)
    (es : List Ent) (v : Bool) (St : ∀ _ : K, List Sym) (hT : St .T = (toks φ).reverse)
    (hB : St .B = tblStk es) (hS : St .S = []) (hA : St .A = []) (hC : St .C = [])
    (hV : St .V = []) (hP : St .P = []) (hF : St .F = []) :
    ∃ v' S', RunLe (prog lk l0) ((toks φ).length * (a * (tblStk es).length + b + 5) + 1)
      ⟨some (.inl .start), v, St⟩
      ⟨some (.inl (if checkSpec φ es then .yes else .no)), v', S'⟩

Uses 19 · Used by 1

Statement usesDriver labels of the clause check · Stacks of the clause check · The lookup contract · Clause-check statements · The clause-check driver with a lookup sub-program · Table entries · Stack alphabet of the SAT verifier · Clause check against an occurrence table · Table stack of an entry list · Token sequence of a CNF formula · CNF formula · Runs within a step budget

Proof usesA clause's tokens on the token stack · Clause loop of the clause check · A literal's tokens on the token stack · Tokens of a clause · Tokens of a literal · Live value of a name in a table · CNF clause

Used byThe TM2 SAT verifier

InductiveStacks of the lookup machine#✓fully proved

The lookup machine has six stacks: the query stack \(T\), the table stack \(B\), the stash \(S\), the two scratch stacks \(A\) and \(C\) used for comparisons, and the value stack \(V\).

inductive K | T | B | S | A | C | V
  deriving DecidableEq

Used by 15

Used byMoving a table marker between stacks · Moving a symbol between stacks · The lookup program · The 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 · Stack contents of the lookup machine · Restoring and stashing after a comparison in the lookup machine · Placement of the lookup's stacks in the clause-check driver · Stack embedding of the lookup into the clause-check driver · The embedded lookup program · The embedded lookup meets the lookup contract

InductiveLabels of the lookup machine#✓fully proved

The lookup machine has the labels \(\mathsf{init}\), \(\mathsf{scan}\), \(\mathsf{cmp}(b)\) and \(\mathsf{put}(b)\) for each bit \(b\), \(\mathsf{rstT}\), \(\mathsf{rstB}\), \(\mathsf{mvN}\), \(\mathsf{back}\), \(\mathsf{mark}\) and \(\mathsf{done}\). The labels \(\mathsf{cmp}(b)\) and \(\mathsf{put}(b)\) serve a live table entry with value \(b\).

inductive Lab
  | init | scan | cmp (b : Bool) | put (b : Bool) | rstT | rstB | mvN | back | mark | done
  deriving DecidableEq

Used by 23

Used byMoving a table marker between stacks · Moving a symbol between stacks · The lookup program · Next label of the lookup scan · The 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 · Start label of the lookup machine · Restoring and stashing after a comparison in the lookup machine · Driver labels in the SAT host · Host labels as a sum type · Filter exits in the SAT verifier host · Labels of the SAT verifier host · Program of the SAT verifier host · Lookup labels in the clause-check driver · The embedded lookup program · The tokenizer embeds in the SAT verifier host · The embedded lookup meets the lookup contract · The SAT verifier machine · The TM2 SAT verifier

DefinitionMoving a symbol between stacks#✓fully proved

For stacks \(a\) and \(b\), a symbol \(x\) and a map \(f\) from symbols to labels, this machine instruction pops the top of \(a\) (if any), pushes \(x\) onto \(b\) and goes to the label \(f(x)\).

def mvSym (a b : K) (x : Sym) (f : Sym → Lab) : TM2.Stmt (fun _ : K => Sym) Lab Bool :=
  .pop a (fun s _ => s) <| .push b (fun _ => x) <| .goto fun _ => f x

Uses 3 · Used by 3

Statement usesStacks of the lookup machine · Labels of the lookup machine · Stack alphabet of the SAT verifier

Used byMoving a table marker between stacks · The return loop of the lookup machine · The scan loop of the lookup machine

DefinitionMoving a table marker between stacks#✓fully proved

For stacks \(a\) and \(b\), a label \(e\) and a map \(f\) from symbols to labels, this machine instruction does the following: if the top of \(a\) is a table marker \(y\) (that is, \(\mathsf{dead}\) or \(\mathsf{val}(c)\) for a bit \(c\)), it pops \(y\) from \(a\), pushes it onto \(b\) and goes to \(f(y)\); if \(a\) is empty or has another symbol on top, it goes to \(e\) and leaves the stacks unchanged.

The invariants of the lookup machine rule out another symbol on top of \(a\).

def mvMark (a b : K) (e : Lab) (f : Sym → Lab) : TM2.Stmt (fun _ : K => Sym) Lab Bool :=
  .peek a (fun _ (o : Option Sym) => decide (o = none)) <| .branch id (.goto fun _ => e) <|
  .peek a (fun _ (o : Option Sym) => decide (o = some .dead)) <|
    .branch id (mvSym a b .dead f) <|
  .peek a (fun _ (o : Option Sym) => decide (o = some (.val true))) <|
    .branch id (mvSym a b (.val true) f) <|
  .peek a (fun _ (o : Option Sym) => decide (o = some (.val false))) <|
    .branch id (mvSym a b (.val false) f) (.goto fun _ => e)

Uses 4 · Used by 1

Statement usesStacks of the lookup machine · Labels of the lookup machine · Moving a symbol between stacks · Stack alphabet of the SAT verifier

Used byThe lookup program

DefinitionNext label of the lookup scan#✓fully proved

The label at which the lookup scan continues after moving a marker symbol \(x\): the comparison label \(\mathsf{cmp}(b)\) if \(x\) is the value marker \(\mathsf{val}(b)\), and the name-moving label \(\mathsf{mvN}\) for every other symbol.

def scanNext : Sym → Lab
  | .val b => .cmp b
  | _ => .mvN

Uses 2 · Used by 3

Statement usesLabels of the lookup machine · Stack alphabet of the SAT verifier

Used byThe lookup program · One scan step of the lookup · The scan loop of the lookup machine

DefinitionThe lookup program#✓fully proved

The lookup machine works on the stacks \(T\), \(B\), \(S\), \(A\), \(C\) and \(V\) and acts at each label as follows. At \(\mathsf{init}\) it pushes the bit symbol of false onto \(V\) and goes to \(\mathsf{scan}\). At \(\mathsf{scan}\), if the top of \(B\) is a table marker it moves that marker onto \(S\) and goes to \(\mathsf{cmp}(b)\) if the marker is \(\mathsf{val}(b)\) and to \(\mathsf{mvN}\) if it is \(\mathsf{dead}\); if \(B\) is empty or has another symbol on top it goes to \(\mathsf{back}\). At \(\mathsf{cmp}(b)\) it compares the bit blocks on top of \(T\) and \(B\): while both tops are equal bits it pops them, pushes that bit symbol onto \(A\) and onto \(C\) and stays at \(\mathsf{cmp}(b)\); when both blocks end together it goes to \(\mathsf{put}(b)\), and on a mismatch (different bits, or one block ending first) it goes to \(\mathsf{rstT}\) without popping. At \(\mathsf{put}(b)\) it pops \(V\), pushes the bit symbol of \(b\) onto \(V\) and goes to \(\mathsf{rstT}\). At \(\mathsf{rstT}\), \(\mathsf{rstB}\), \(\mathsf{mvN}\) and \(\mathsf{back}\) it moves the bit block on top of \(A\) onto \(T\), of \(C\) onto \(B\), of \(B\) onto \(S\) and of \(S\) onto \(B\) respectively, staying at the label while the top is a bit and then going to \(\mathsf{rstB}\), \(\mathsf{mvN}\), \(\mathsf{scan}\) and \(\mathsf{mark}\) respectively. At \(\mathsf{mark}\), if the top of \(S\) is a table marker it moves that marker onto \(B\) and goes to \(\mathsf{back}\); if \(S\) is empty or has another symbol on top it goes to \(\mathsf{done}\). At \(\mathsf{done}\) it halts.

def prog : Lab → TM2.Stmt (fun _ : K => Sym) Lab Bool
  | .init => .push .V (fun _ => Sym.bit false) (.goto fun _ => .scan)
  | .scan => mvMark .B .S .back scanNext
  | .cmp b => cmpB .T .B .A .C Sym.bit? Sym.bit? Sym.bit Sym.bit (.cmp b) (.put b) .rstT
  | .put b => .pop .V (fun s _ => s) (.push .V (fun _ => Sym.bit b) (.goto fun _ => .rstT))
  | .rstT => moveB .A .T Sym.bit? Sym.bit .rstT .rstB
  | .rstB => moveB .C .B Sym.bit? Sym.bit .rstB .mvN
  | .mvN => moveB .B .S Sym.bit? Sym.bit .mvN .scan
  | .back => moveB .S .B Sym.bit? Sym.bit .back .mark
  | .mark => mvMark .S .B .done fun _ => .back
  | .done => .halt

Uses 9 · Used by 9

Statement usesStacks of the lookup machine · Labels of the lookup machine · Moving a table marker between stacks · Next label of the lookup scan · Stack alphabet of the SAT verifier · Reading a symbol as a name bit · Flag bit of a machine state · Bit-block comparison statement · Bit-moving loop

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 · The embedded lookup program · The embedded lookup meets the lookup contract

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.