Reading one pair of a block to Comparing the sum with the target

DefinitionReading one pair of a block#✓fully proved

For a flag \(z\) (the bits read so far end in false), a statement \(\mathit{done}\) and statements \(\mathit{body}(b)\) for each bit \(b\): if the input stack \(X\) is empty, go to the label \(\mathsf{no}\). Otherwise pop the top of \(X\) as a bit, a symbol that is not a bit counting as false. If it is false (the end marker), go to \(\mathsf{no}\) when \(z\) is true and run \(\mathit{done}\) otherwise. If it is true, go to \(\mathsf{no}\) if \(X\) is now empty, and otherwise pop the next symbol of \(X\) as a payload bit \(b\) (again a non-bit counts as false) and run \(\mathit{body}(b)\).

def rdS (z : Bool) (done : Stmt) (body : Bool → Stmt) : Stmt :=
  .peek .X (fun _ o => o.isNone) <| .branch id (.goto fun _ => .no) <|
  .pop .X (fun _ o => bitOf Sym.bit? o) <| .branch id
    (.peek .X (fun _ o => o.isNone) <| .branch id (.goto fun _ => .no) <|
      .pop .X (fun _ o => bitOf Sym.bit? o) <| .branch id (body true) (body false))
    (bif z then .goto fun _ => .no else done)

Uses 6 · Used by 3

Statement usesStacks of the SUBSET-SUM verifier · Labels of the SUBSET-SUM verifier · Statements of the SUBSET-SUM verifier · Stack alphabet of the SAT verifier · Reading a symbol as a name bit · Bit on top of a stack

Used byPadding machine embeds the summation machine · Membership transducer embeds the summation machine · The SUBSET-SUM verifier program

DefinitionAdding one payload bit to the sum#✓fully proved

The machine statement for adding the payload bit \(b\) with carry \(c\): pop the top symbol of the sum stack \(A\) and read it as a bit \(a\) (false if \(A\) is empty or the symbol is not a bit), push the bit \(a \oplus b \oplus c\) onto \(B\), and go to the label that adds a chosen number with carry the carry out of \(a\), \(b\) and \(c\) and flag \(\lnot b\) (the flag records whether the bits of the block read so far end in false).

def addS (c b : Bool) : Stmt :=
  .pop .A (fun _ o => bitOf Sym.bit? o) <| .push .B (fun a => .bit (a ^^ b ^^ c)) <|
    .goto fun a => .add (carry a b c) (!b)

Uses 7 · Used by 7

Statement usesStacks of the SUBSET-SUM verifier · Labels of the SUBSET-SUM verifier · Statements of the SUBSET-SUM verifier · Carry bit of a full adder · Stack alphabet of the SAT verifier · Reading a symbol as a name bit · Bit on top of a stack

Used byPadding machine embeds the summation machine · Membership transducer embeds the summation machine · The verifier rejects an unterminated chosen block · The verifier rejects a chosen block that ends in false · Adding a canonical chosen block · The SUBSET-SUM verifier program · Binary addition of framed numbers in quadratic time

DefinitionCarry step of the SUBSET-SUM verifier#✓fully proved

For a carry bit \(c\), the verifier statement that carries \(c\) through the rest of the sum on stack \(A\): if \(A\) is empty, it sets the local variable to true, pushes the bit \(1\) onto \(B\) when \(c\) is true and goes to label \(\mathrm{back}\); otherwise it pops the top symbol of \(A\), read as a bit \(a\) (a symbol that is not a bit reads as \(0\)), sets the local variable to \(a\), pushes the bit \(a \oplus c\) onto \(B\) and goes to label \(\mathrm{fin}(a \wedge c)\).

def finS (c : Bool) : Stmt :=
  .peek .A (fun _ o => o.isNone) <| .branch id
    (bif c then .push .B (fun _ => .bit true) (.goto fun _ => .back) else .goto fun _ => .back)
    (.pop .A (fun _ o => bitOf Sym.bit? o) <| .push .B (fun a => .bit (a ^^ c)) <|
      .goto fun a => .fin (a && c))

Uses 6 · Used by 3

Statement usesStacks of the SUBSET-SUM verifier · Labels of the SUBSET-SUM verifier · Statements of the SUBSET-SUM verifier · Stack alphabet of the SAT verifier · Reading a symbol as a name bit · Bit on top of a stack

Used byPadding machine embeds the summation machine · Membership transducer embeds the summation machine · The SUBSET-SUM verifier program

DefinitionStarting the next number#✓fully proved

The verifier's statement at the label \(\mathsf{next}\). If the input stack \(X\) is empty, it goes to the label \(\mathsf{fmove}\) (move the sum, then compare). Otherwise it pops the top of the witness stack \(W\) and reads it as a bit \(c\), taking \(c\) false when \(W\) is empty or its top is not a bit; \(c\) becomes the internal state. It then goes to the label \(\mathsf{add}\) with carry false if \(c\) is true, and to the label \(\mathsf{skip}\) if \(c\) is false, in both cases with the flag "the bits read so far end in false" unset.

def nextS : Stmt :=
  .peek .X (fun _ o => o.isNone) <| .branch id (.goto fun _ => .fmove) <|
  .pop .W (fun _ o => bitOf Sym.bit? o) <|
    .goto fun c => bif c then .add false false else .skip false

Uses 6 · Used by 3

Statement usesStacks of the SUBSET-SUM verifier · Labels of the SUBSET-SUM verifier · Statements of the SUBSET-SUM verifier · Stack alphabet of the SAT verifier · Reading a symbol as a name bit · Bit on top of a stack

Used byPadding machine embeds the summation machine · Membership transducer embeds the summation machine · The SUBSET-SUM verifier program

DefinitionThe SUBSET-SUM verifier program#✓fully proved

The program on the stacks \(X, W, T, A, B, P, Q\) over the verifier's symbols, with Boolean internal state, given label by label. A popped symbol that is not a bit counts as false, as does a pop from an empty stack. Reading a pair of a block off \(X\) with flag \(z\) ("the bits read so far end in false") goes to \(\mathsf{no}\) if \(X\) is empty; on the end marker false it goes to \(\mathsf{no}\) if \(z\) holds and otherwise ends the block; on true it reads a payload bit \(b\), going to \(\mathsf{no}\) if \(X\) has ended.

• \(\mathsf{tgt}(z)\): read a pair of the target block with flag \(z\); at the end of the block go to \(\mathsf{next}\); on a payload bit \(b\), push \(b\) onto \(T\) and go to \(\mathsf{tgt}(\lnot b)\).
• \(\mathsf{next}\): if \(X\) is empty go to \(\mathsf{fmove}\); otherwise pop a witness bit \(c\) off \(W\) (false if absent) and go to \(\mathsf{add}\) with carry false if \(c\), else to \(\mathsf{skip}\), with the flag unset.
• \(\mathsf{add}(c, z)\): read a pair with flag \(z\); at the end of the block go to \(\mathsf{fin}(c)\); on a payload bit \(b\), pop a bit \(a\) off \(A\) (false if absent), push \(a \oplus b \oplus c\) onto \(B\) and go to \(\mathsf{add}(c', \lnot b)\), where \(c'\) is the carry out of \(a + b + c\).
• \(\mathsf{skip}(z)\): read a pair with flag \(z\); at the end of the block go to \(\mathsf{next}\); on a payload bit \(b\) go to \(\mathsf{skip}(\lnot b)\).
• \(\mathsf{fin}(c)\): carry \(c\) through the rest of \(A\), pushing the result bits onto \(B\), then go to \(\mathsf{back}\).
• \(\mathsf{back}\): move the bits on top of \(B\) onto \(A\) one by one, then go to \(\mathsf{next}\).
• \(\mathsf{fmove}\): move the bits on top of \(A\) onto \(B\) one by one, then go to \(\mathsf{cmp}\).
• \(\mathsf{cmp}\): compare the bit blocks on top of \(B\) and \(T\), using \(P\) and \(Q\) as scratch, and go to \(\mathsf{yes}\) if they are equal and to \(\mathsf{no}\) otherwise.
• \(\mathsf{yes}\) and \(\mathsf{no}\): halt.

def prog : Lab → TM2.Stmt (fun _ : K => Sym) Lab Bool
  | .tgt z => rdS z (.goto fun _ => .next) fun b =>
      .push .T (fun _ => .bit b) <| .goto fun _ => .tgt (!b)
  | .next => nextS
  | .add c z => rdS z (.goto fun _ => .fin c) (addS c)
  | .skip z => rdS z (.goto fun _ => .next) fun b => .goto fun _ => .skip (!b)
  | .fin c => finS c
  | .back => moveB .B .A Sym.bit? Sym.bit .back .next
  | .fmove => moveB .A .B Sym.bit? Sym.bit .fmove .cmp
  | .cmp => cmpB .B .T .P .Q Sym.bit? Sym.bit? Sym.bit Sym.bit .cmp .yes .no
  | .yes => .halt
  | .no => .halt

Uses 11 · Used by 27

Statement usesStacks of the SUBSET-SUM verifier · Labels of the SUBSET-SUM verifier · Adding one payload bit to the sum · Carry step of the SUBSET-SUM verifier · Starting the next number · Reading one pair of a block · 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 byPadding 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 · Raw-input PARTITION membership machine 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 · Moving the new sum back · Comparing the sum with the target · Carry phase of the SUBSET-SUM verifier · Moving the final sum for the comparison · Rejection by the SUBSET-SUM verifier within a step bound · Rejecting in one step · The verifier rejects an unterminated skipped block · Skipping a number block · The verifier rejects an unterminated target block · Reading the target block · The summing loop of the SUBSET-SUM verifier · Binary addition program built on the SUBSET-SUM machine · The SUBSET-SUM verifier machine · Binary addition of framed numbers in quadratic time · The SUBSET-SUM verifier machine as a host component · SUBSET-SUM is in NP · SUBSET-SUM verifier computes the mask-selected sum · Embedded SUBSET-SUM summing component reaches the mapped label

DefinitionStart state of the SUBSET-SUM verifier#✓fully proved

The SUBSET-SUM verifier machine starts in its target-reading state, with the flag recording whether the bits read so far end in false set to false.

def start : Lab := .tgt false

Uses 1 · Used by 2

Statement usesLabels of the SUBSET-SUM verifier

Used byThe SUBSET-SUM verifier machine · SUBSET-SUM is in NP

DefinitionStack contents of the SUBSET-SUM verifier#✓fully proved

For lists of symbols \(x\), \(w\), \(t\), \(a\), \(b\), this assigns contents to the seven stacks of the SUBSET-SUM verifier machine: the input stack \(X\) holds \(x\), the witness stack \(W\) holds \(w\), the target stack \(T\) holds \(t\), the sum stacks \(A\) and \(B\) hold \(a\) and \(b\), and the scratch stacks \(P\) and \(Q\) are empty.

def st (x w t a b : List Sym) : K → List Sym
  | .X => x
  | .W => w
  | .T => t
  | .A => a
  | .B => b
  | .P => []
  | .Q => []

Uses 2 · Used by 19

Statement usesStacks of the SUBSET-SUM verifier · Stack alphabet of the SAT verifier

Used byQuadratic run of the padding machine on canonical instances · 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 · Moving the new sum back · Comparing the sum with the target · Carry phase of the SUBSET-SUM verifier · Moving the final sum for the comparison · 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 · The SUBSET-SUM verifier machine · Binary addition of framed numbers in quadratic time · SUBSET-SUM verifier computes the mask-selected sum · Embedded SUBSET-SUM summing component reaches the mapped label · Embedded run of the binary addition component

DefinitionRejection by the SUBSET-SUM verifier within a step bound#✓fully proved

For a natural number \(n\) and a configuration \(c\) of the SUBSET-SUM verifier, \(\mathrm{Rej}(n, c)\) holds when there are an internal state \(v\) and stack contents \(S\) such that the verifier runs from \(c\) in at most \(n\) steps to the configuration with label \(\mathsf{no}\), internal state \(v\) and stacks \(S\).

def Rej (n : ℕ) (c : TM2.Cfg (fun _ : K => Sym) Lab Bool) : Prop :=
  ∃ v S, RunLe prog n c ⟨some .no, v, S⟩

Uses 5 · Used by 7

Statement usesStacks of the SUBSET-SUM verifier · Labels of the SUBSET-SUM verifier · The SUBSET-SUM verifier program · Stack alphabet of the SAT verifier · Runs within a step budget

Used byThe verifier rejects an unterminated chosen block · The verifier rejects a chosen block that ends in false · Rejecting in one step · The verifier rejects an unterminated skipped block · The verifier rejects an unterminated target block · The summing loop of the SUBSET-SUM verifier · The SUBSET-SUM verifier machine

TheoremRejecting in one step#✓fully proved

Let \(l\) be a label, \(v\) a Boolean and \(S\) an assignment of stack contents. If executing the verifier's statement at label \(l\) from internal state \(v\) and stacks \(S\) yields the next label \(\mathsf{no}\), then the verifier reaches a configuration with label \(\mathsf{no}\) from the configuration \((l, v, S)\) within one step.

theorem rej_one {l : Lab} {v : Bool} {S : K → List Sym}
    (h : (TM2.stepAux (prog l) v S).l = some .no) : Rej 1 ⟨some l, v, S⟩

Uses 8 · Used by 4

Statement usesStacks of the SUBSET-SUM verifier · Labels of the SUBSET-SUM verifier · Rejection by the SUBSET-SUM verifier within a step bound · The SUBSET-SUM verifier program · Stack alphabet of the SAT verifier

Proof usesExact-length runs of a TM2 machine · A single step executes the statement at the current label · Runs within a step budget

Used byThe verifier rejects an unterminated chosen block · The verifier rejects a chosen block that ends in false · The verifier rejects an unterminated skipped block · The verifier rejects an unterminated target block

TheoremReading the target block#✓fully proved

Let \(p\) and \(s\) be lists of bits, and write \(\mathrm{delimit}(p)\) for the self-delimiting encoding of \(p\) (each bit \(b\) written as true followed by \(b\), then a terminating false). Suppose the SUBSET-SUM verifier machine is in its target-reading state, with flag \(z\) recording whether the bits read so far end in false and any value of its local Boolean variable, with the bits of \(\mathrm{delimit}(p)\) followed by the bits of \(s\) on the input stack \(X\), a list \(t\) of symbols on the target stack \(T\), arbitrary contents on the stacks \(W\), \(A\), \(B\), and the scratch stacks \(P\), \(Q\) empty. Then after exactly \(|p| + 1\) steps the stack \(X\) holds the bits of \(s\), the bits of \(p\) have been pushed onto \(T\) one at a time (so that \(T\) holds, from the top, the bits of \(p\) in reverse order followed by \(t\)), the stacks \(W\), \(A\), \(B\), \(P\), \(Q\) are unchanged, the local variable is false, and the machine is in its rejecting state if either \(p\) is non-empty and ends in false or \(p\) is empty and \(z\) is true, and in the state that starts the next number otherwise.

theorem tgt_run (rest : List Bool) (w a b : List Sym) :
    ∀ (p : List Bool) (z : Bool) (t : List Sym) (v : Bool),
    Run prog (p.length + 1) ⟨some (.tgt z), v, st ((delimit p ++ rest).map .bit) w t a b⟩
      ⟨some (if lastF z p then .no else .next), false,
        st (rest.map .bit) w ((p.map .bit).reverse ++ t) a b⟩

Uses 11 · Used by 1

Statement usesStacks of the SUBSET-SUM verifier · Labels of the SUBSET-SUM verifier · Whether a bit string ends in false · The SUBSET-SUM verifier program · Stack contents of the SUBSET-SUM verifier · Stack alphabet of the SAT verifier · Self-delimiting form of a bitstring · 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 · Bit on top of a stack

Used byThe SUBSET-SUM verifier machine

TheoremSkipping a number block#✓fully proved

Let \(p\) and \(s\) be lists of bits, and write \(\mathrm{delimit}(p)\) for the self-delimiting encoding of \(p\) (each bit \(b\) written as true followed by \(b\), then a terminating false). Suppose the SUBSET-SUM verifier machine is in the state that skips an unchosen number block, with flag \(z\) recording whether the bits read so far end in false and any value of its local Boolean variable, with the bits of \(\mathrm{delimit}(p)\) followed by the bits of \(s\) on the input stack \(X\), arbitrary contents on the stacks \(W\), \(T\), \(A\), \(B\), and the scratch stacks \(P\), \(Q\) empty. Then after exactly \(|p| + 1\) steps the stack \(X\) holds the bits of \(s\), all other stacks are unchanged, the local variable is false, and the machine is in its rejecting state if either \(p\) is non-empty and ends in false or \(p\) is empty and \(z\) is true, and in the state that starts the next number otherwise.

theorem skip_run (rest : List Bool) (w t a b : List Sym) :
    ∀ (p : List Bool) (z : Bool) (v : Bool),
    Run prog (p.length + 1) ⟨some (.skip z), v, st ((delimit p ++ rest).map .bit) w t a b⟩
      ⟨some (if lastF z p then .no else .next), false, st (rest.map .bit) w t a b⟩

Uses 11 · Used by 1

Statement usesStacks of the SUBSET-SUM verifier · Labels of the SUBSET-SUM verifier · Whether a bit string ends in false · The SUBSET-SUM verifier program · Stack contents of the SUBSET-SUM verifier · Stack alphabet of the SAT verifier · Self-delimiting form of a bitstring · 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 · Bit on top of a stack

Used byThe summing loop of the SUBSET-SUM verifier

TheoremCarry phase of the SUBSET-SUM verifier#✓fully proved

Let \(x\), \(w\), \(t\) and \(\mathit{acc}\) be lists of stack symbols, \(u\) a list of bits, \(c\) a carry bit and \(v\) a Boolean, and write \(\mathrm{inc}(c, u)\) for the result of adding the carry \(c\) to \(u\) (least significant bit first). Started at label \(\mathrm{fin}(c)\) with variable \(v\), with \(x\), \(w\), \(t\) on the stacks \(X\), \(W\), \(T\), the bits of \(u\) on \(A\) (first bit on top), \(\mathit{acc}\) on \(B\) and \(P\), \(Q\) empty, the verifier takes exactly \(|u| + 1\) steps to reach label \(\mathrm{back}\) with variable true, where \(X\), \(W\), \(T\) are unchanged, \(A\), \(P\), \(Q\) are empty, and \(B\) holds the bits of \(\mathrm{inc}(c, u)\) on top of \(\mathit{acc}\), last bit on top.

theorem fin_run (x w t : List Sym) : ∀ (u : List Bool) (c : Bool) (acc : List Sym) (v : Bool),
    Run prog (u.length + 1) ⟨some (.fin c), v, st x w t (u.map .bit) acc⟩
      ⟨some .back, true, st x w t [] (((incB c u).map .bit).reverse ++ acc)⟩

Uses 10 · Used by 1

Statement usesStacks of the SUBSET-SUM verifier · Labels of the SUBSET-SUM verifier · Adding a carry bit · The SUBSET-SUM verifier program · Stack contents of the SUBSET-SUM verifier · Stack alphabet of the SAT verifier · 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 · Bit on top of a stack

Used byAdding a canonical chosen block

TheoremAdding a canonical chosen block#✓fully proved

Let \(p\) and \(\mathit{rest}\) be bit lists and \(z\) a bit such that \(p\) is nonempty and ends in true, or \(p\) is empty and \(z\) is false (the flag \(z\) records whether the bits of the block read so far end in false), and let \(c\) be a bit. Start the SUBSET-SUM verifier machine at the label that adds a chosen number with carry \(c\) and flag \(z\), with any value of the local variable, the self-delimiting encoding of \(p\) followed by \(\mathit{rest}\) (as bit symbols) on the input stack \(X\), symbol lists \(w\) on \(W\) and \(t\) on \(T\), a bit list \(u\) (as bit symbols, least significant bit first) on the sum stack \(A\), a symbol list \(\mathit{acc}\) on \(B\), and the scratch stacks \(P\) and \(Q\) empty. Then within \(|p| + |u| + 2\) steps the machine reaches the label that moves the new sum back, with some value of the local variable, \(\mathit{rest}\) on \(X\), \(w\) on \(W\), \(t\) on \(T\), \(A\), \(P\) and \(Q\) empty, and on \(B\) the ripple-carry sum of \(u\) and \(p\) with carry-in \(c\) (as bit symbols, most significant bit on top) above \(\mathit{acc}\).

theorem add_run (rest : List Bool) (w t : List Sym) :
    ∀ (p : List Bool) (c z : Bool) (u : List Bool) (acc : List Sym) (v : Bool),
    lastF z p = false →
    ∃ v', RunLe prog (p.length + u.length + 2)
      ⟨some (.add c z), v, st ((delimit p ++ rest).map .bit) w t (u.map .bit) acc⟩
      ⟨some .back, v', st (rest.map .bit) w t [] (((addB c u p).map .bit).reverse ++ acc)⟩

Uses 17 · Used by 1

Statement usesStacks of the SUBSET-SUM verifier · Labels of the SUBSET-SUM verifier · Ripple-carry addition of bit lists · Whether a bit string ends in false · The SUBSET-SUM verifier program · Stack contents of the SUBSET-SUM verifier · Stack alphabet of the SAT verifier · Self-delimiting form of a bitstring · Runs within a step budget

Proof usesStatements of the SUBSET-SUM verifier · Adding one payload bit to the sum · Carry bit of a full adder · Carry phase of the SUBSET-SUM verifier · Adding a carry bit · Reading a symbol as a name bit · Exact-length runs of a TM2 machine · Bit on top of a stack

Used byThe summing loop of the SUBSET-SUM verifier

TheoremThe verifier rejects a chosen block that ends in false#✓fully proved

Let \(p\) and \(\mathit{rest}\) be bit lists and \(z\) a bit such that \(p\) is nonempty and ends in false, or \(p\) is empty and \(z\) is true (the flag \(z\) records whether the bits of the block read so far end in false). Let \(c\) be a bit and \(u\) a bit list. Start the SUBSET-SUM verifier machine at the label that adds a chosen number with carry \(c\) and flag \(z\), with any value of the local variable, the self-delimiting encoding of \(p\) followed by \(\mathit{rest}\) (as bit symbols) on the input stack \(X\), any symbol lists on \(W\), \(T\) and \(B\), \(u\) (as bit symbols) on the sum stack \(A\), and the scratch stacks \(P\) and \(Q\) empty. Then the machine reaches the rejecting label within \(|p| + 1\) steps.

theorem add_rej (rest : List Bool) (w t : List Sym) :
    ∀ (p : List Bool) (c z : Bool) (u : List Bool) (acc : List Sym) (v : Bool),
    lastF z p = true →
    Rej (p.length + 1) ⟨some (.add c z), v, st ((delimit p ++ rest).map .bit) w t (u.map .bit) acc⟩

Uses 17 · Used by 1

Statement usesStacks of the SUBSET-SUM verifier · Labels of the SUBSET-SUM verifier · Rejection by the SUBSET-SUM verifier within a step bound · Whether a bit string ends in false · Stack contents of the SUBSET-SUM verifier · Stack alphabet of the SAT verifier · Self-delimiting form of a bitstring

Proof usesStatements of the SUBSET-SUM verifier · Adding one payload bit to the sum · Carry bit of a full adder · The SUBSET-SUM verifier program · Rejecting in one step · Reading a symbol as a name 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

Used byThe summing loop of the SUBSET-SUM verifier

TheoremThe verifier rejects an unterminated target block#✓fully proved

Let \(r\) be a list of bits that does not begin with a self-delimiting block, that is, parsing one self-delimiting block off the front of \(r\) fails. Suppose the SUBSET-SUM verifier machine is in its target-reading state, with either value of the flag \(z\) recording whether the bits read so far end in false and either value of its local Boolean variable, with the bits of \(r\) on the input stack \(X\), arbitrary contents on the stacks \(W\), \(T\), \(A\), \(B\), and the scratch stacks \(P\), \(Q\) empty. Then the machine reaches its rejecting state within \(|r| + 1\) steps.

theorem tgt_fail (w a b : List Sym) : ∀ (r : List Bool), undelimit r = none →
    ∀ (z : Bool) (t : List Sym) (v : Bool), Rej (r.length + 1)
      ⟨some (.tgt z), v, st (r.map .bit) w t a b⟩

Uses 13 · Used by 1

Statement usesStacks of the SUBSET-SUM verifier · Labels of the SUBSET-SUM verifier · Rejection by the SUBSET-SUM verifier within a step bound · Stack contents of the SUBSET-SUM verifier · Stack alphabet of the SAT verifier · Parsing one self-delimiting block

Proof usesThe SUBSET-SUM verifier program · Rejecting in one step · Reading a symbol as a name 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

Used byThe SUBSET-SUM verifier machine

TheoremThe verifier rejects an unterminated skipped block#✓fully proved

Let \(r\) be a list of bits that does not begin with a self-delimiting block, that is, parsing one self-delimiting block off the front of \(r\) fails. Suppose the SUBSET-SUM verifier machine is in the state that skips an unchosen number block, with either value of the flag \(z\) recording whether the bits read so far end in false and either value of its local Boolean variable, with the bits of \(r\) on the input stack \(X\), arbitrary contents on the stacks \(W\), \(T\), \(A\), \(B\), and the scratch stacks \(P\), \(Q\) empty. Then the machine reaches its rejecting state within \(|r| + 1\) steps.

theorem skip_fail (w t a b : List Sym) : ∀ (r : List Bool), undelimit r = none →
    ∀ (z : Bool) (v : Bool), Rej (r.length + 1) ⟨some (.skip z), v, st (r.map .bit) w t a b⟩

Uses 13 · Used by 1

Statement usesStacks of the SUBSET-SUM verifier · Labels of the SUBSET-SUM verifier · Rejection by the SUBSET-SUM verifier within a step bound · Stack contents of the SUBSET-SUM verifier · Stack alphabet of the SAT verifier · Parsing one self-delimiting block

Proof usesThe SUBSET-SUM verifier program · Rejecting in one step · Reading a symbol as a name 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

Used byThe summing loop of the SUBSET-SUM verifier

TheoremThe verifier rejects an unterminated chosen block#✓fully proved

Let \(r\) be a bit list from whose front no complete self-delimiting block can be parsed, let \(c\) and \(z\) be bits, and let \(u\) be a bit list. Start the SUBSET-SUM verifier machine at the label that adds a chosen number with carry \(c\) and flag \(z\) (the flag records whether the bits of the block read so far end in false), with any value of the local variable, \(r\) (as bit symbols) on the input stack \(X\), any symbol lists on \(W\), \(T\) and \(B\), \(u\) (as bit symbols) on the sum stack \(A\), and the scratch stacks \(P\) and \(Q\) empty. Then the machine reaches the rejecting label within \(|r| + 1\) steps.

theorem add_fail (w t : List Sym) : ∀ (r : List Bool), undelimit r = none →
    ∀ (c z : Bool) (u : List Bool) (acc : List Sym) (v : Bool),
    Rej (r.length + 1) ⟨some (.add c z), v, st (r.map .bit) w t (u.map .bit) acc⟩

Uses 16 · Used by 1

Statement usesStacks of the SUBSET-SUM verifier · Labels of the SUBSET-SUM verifier · Rejection by the SUBSET-SUM verifier within a step bound · Stack contents of the SUBSET-SUM verifier · Stack alphabet of the SAT verifier · Parsing one self-delimiting block

Proof usesStatements of the SUBSET-SUM verifier · Adding one payload bit to the sum · Carry bit of a full adder · The SUBSET-SUM verifier program · Rejecting in one step · Reading a symbol as a name 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

Used byThe summing loop of the SUBSET-SUM verifier

TheoremMoving the new sum back#✓fully proved

Let \(\mathit{res}\) be a bit list. Start the SUBSET-SUM verifier machine at the label that moves the new sum back, with any value of the local variable, symbol lists \(x\), \(w\), \(t\) on \(X\), \(W\), \(T\), the sum stack \(A\) empty, \(\mathit{res}\) (as bit symbols, last bit on top) on \(B\), and the scratch stacks \(P\) and \(Q\) empty. Then after exactly \(|\mathit{res}| + 1\) steps the machine is at the label that starts the next number, with some value of the local variable, \(x\), \(w\), \(t\) unchanged, \(\mathit{res}\) (as bit symbols, first bit on top) on \(A\), and \(B\), \(P\), \(Q\) empty.

theorem back_run (x w t : List Sym) (res : List Bool) (v : Bool) :
    ∃ v', Run prog (res.length + 1) ⟨some .back, v, st x w t [] (res.map .bit).reverse⟩
      ⟨some .next, v', st x w t (res.map .bit) []⟩

Uses 9 · Used by 1

Statement usesStacks of the SUBSET-SUM verifier · Labels of the SUBSET-SUM verifier · The SUBSET-SUM verifier program · Stack contents of the SUBSET-SUM verifier · Stack alphabet of the SAT verifier · Exact-length runs of a TM2 machine

Proof usesReading a symbol as a name bit · Flag bit of a machine state · Running the bit-moving loop

Used byThe summing loop of the SUBSET-SUM verifier

TheoremMoving the final sum for the comparison#✓fully proved

Let \(x\), \(w\), \(t\) be lists of stack symbols, \(s\) a list of bits and \(v\) a Boolean. Started at label \(\mathrm{fmove}\) with variable \(v\), with \(x\), \(w\), \(t\) on the stacks \(X\), \(W\), \(T\), the bits of \(s\) on \(A\) (first bit on top) and \(B\), \(P\), \(Q\) empty, the verifier takes exactly \(|s| + 1\) steps to reach label \(\mathrm{cmp}\), with some value of the variable, where \(X\), \(W\), \(T\) are unchanged, \(A\), \(P\), \(Q\) are empty, and \(B\) holds the bits of \(s\), last bit on top.

theorem fmove_run (x w t : List Sym) (s : List Bool) (v : Bool) :
    ∃ v', Run prog (s.length + 1) ⟨some .fmove, v, st x w t (s.map .bit) []⟩
      ⟨some .cmp, v', st x w t [] (s.map .bit).reverse⟩

Uses 9 · Used by 2

Statement usesStacks of the SUBSET-SUM verifier · Labels of the SUBSET-SUM verifier · The SUBSET-SUM verifier program · Stack contents of the SUBSET-SUM verifier · Stack alphabet of the SAT verifier · Exact-length runs of a TM2 machine

Proof usesReading a symbol as a name bit · Flag bit of a machine state · Running the bit-moving loop

Used byThe SUBSET-SUM verifier machine · SUBSET-SUM verifier computes the mask-selected sum

TheoremComparing the sum with the target#✓fully proved

Let \(s\) and \(\tau\) be bit lists. Start the SUBSET-SUM verifier machine at the comparison label, with any value of the local variable, symbol lists \(x\) and \(w\) on \(X\) and \(W\), the target \(\tau\) on \(T\) and the sum \(s\) on \(B\) (both as bit symbols, last bit on top), and the stacks \(A\), \(P\) and \(Q\) empty. Then within \(|s| + 1\) steps the machine reaches the accepting label if \(s = \tau\) and the rejecting label otherwise.

theorem cmp_run (x w : List Sym) (s tt : List Bool) (v : Bool) :
    ∃ v' S', RunLe prog (s.length + 1)
      ⟨some .cmp, v, st x w (tt.map .bit).reverse [] (s.map .bit).reverse⟩
      ⟨some (if s = tt then .yes else .no), v', S'⟩

Uses 11 · Used by 1

Statement usesStacks of the SUBSET-SUM verifier · Labels of the SUBSET-SUM verifier · The SUBSET-SUM verifier program · Stack contents of the SUBSET-SUM verifier · Stack alphabet of the SAT verifier · Runs within a step budget

Proof usesReading a symbol as a name bit · Four pairwise distinct stacks · Flag bit of a machine state · Exact-length runs of a TM2 machine · Correctness of the bit-block comparison

Used byThe SUBSET-SUM verifier machine

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.