A fixed-width binary counter inside the polynomial-time algebra

⚠️ Unreviewed by Bolton

Savitch's recursion searches for a midpoint by enumerating every bitstring of the width a configuration code occupies. The enumeration is an ordinary little-endian increment that wraps around, and the wrap is what tells the search it has run out of candidates.

Complexity.addBit is that increment as a plain recursion — carry in, carry out, result — and Complexity.bumpStep is the same thing as a left-to-right scan on a packed state, the shape Cobham.iterate_mem_FP iterates. The two agree (Complexity.bumpStep_iterate_run), so the arithmetic can be done on the recursion and the polynomial-time bound on the scan.

Main definitions

• Complexity.addBit — increment a little-endian bitstring, with carry
• Complexity.bumpBits, Complexity.bumpOver — its two components
• Complexity.bumpStep — one step of the scan that computes it
• Complexity.bumpFlag, Complexity.bumpCode — the packed verdicts

Main results

• Complexity.addBit_binValLE — the adder is correct
• Complexity.bumpBits_length — the width is preserved
• Complexity.bumpOver_iff — the carry fires exactly on the last candidate
• Complexity.bumpCodeFn_mem_FP, Complexity.bumpFlagFn_mem_FP — both are in FP

The increment as a recursion

def Complexity.addBit : Bool → List Bool → Bool × List Bool

Add a carry bit into a little-endian bitstring: the carry out and the result.

Equations

• Complexity.addBit x✝ [] = (x✝, [])
• Complexity.addBit x✝ (b :: t) = ((Complexity.addBit (x✝ && b) t).1, (x✝ ^^ b) :: (Complexity.addBit (x✝ && b) t).2)

@[simp]

theorem Complexity.addBit_nil (c : Bool) : addBit c [] = (c, [])

@[simp]

theorem Complexity.addBit_cons (c b : Bool) (t : List Bool) : addBit c (b :: t) = ((addBit (c && b) t).1, (c ^^ b) :: (addBit (c && b) t).2)

def Complexity.bumpBits (w : List Bool) : List Bool

The increment of a little-endian bitstring, wrapping on overflow.

Equations

• Complexity.bumpBits w = (Complexity.addBit true w).2

def Complexity.bumpOver (w : List Bool) : Bool

Did the increment wrap around?

Equations

• Complexity.bumpOver w = (Complexity.addBit true w).1

@[simp]

theorem Complexity.addBit_false (w : List Bool) : addBit false w = (false, w)

Adding no carry changes nothing.

@[simp]

theorem Complexity.addBit_length (c : Bool) (w : List Bool) : (addBit c w).2.length = w.length

The width is preserved.

@[simp]

theorem Complexity.bumpBits_length (w : List Bool) : (bumpBits w).length = w.length

theorem Complexity.addBit_binValLE (c : Bool) (w : List Bool) : (binValLE (addBit c w).2 + if (addBit c w).1 = true then 2 ^ w.length else 0) = binValLE w + if c = true then 1 else 0

The adder is correct.

theorem Complexity.bumpOver_iff (w : List Bool) : bumpOver w = true ↔ binValLE w = 2 ^ w.length - 1

The carry fires exactly on the last candidate.

theorem Complexity.binValLE_bumpBits_of_not_over (w : List Bool) (h : bumpOver w = false) : binValLE (bumpBits w) = binValLE w + 1

The increment counts.

theorem Complexity.bumpBits_iterate (ℓ j : ℕ) : j < 2 ^ ℓ → bumpBits^[j] (bitsOfLenLE ℓ 0) = bitsOfLenLE ℓ j

Iterating the increment from zero enumerates the candidates in order.

The increment as a scan

The same increment, written as a left-to-right pass over the string: carry, the bits already emitted, and the bits still to read. This is the shape Cobham.iterate_mem_FP iterates, and every operation in it is one of the algebra's.

def Complexity.bumpStep : List Bool × List Bool × List Bool → List Bool × List Bool × List Bool

One step of the increment scan.

Equations

• Complexity.bumpStep (c, acc, []) = (c, acc, [])
• Complexity.bumpStep (c, acc, b :: t) = (Complexity.andBit c [b], acc ++ Complexity.Cobham.selectHead c (Complexity.notBit [b]) [b], t)

@[simp]

theorem Complexity.bumpStep_nil (c acc : List Bool) : bumpStep (c, acc, []) = (c, acc, [])

theorem Complexity.bumpStep_flag (c b : Bool) (acc t : List Bool) : bumpStep ([c], acc, b :: t) = ([c && b], acc ++ [c ^^ b], t)

theorem Complexity.bumpStep_iterate_run (c : Bool) (acc w : List Bool) : bumpStep^[w.length] ([c], acc, w) = ([(addBit c w).1], acc ++ (addBit c w).2, [])

The scan computes the increment.

theorem Complexity.bumpStep_iterate_length (c : Bool) (acc w : List Bool) (n : ℕ) : (bumpStep^[n] ([c], acc, w)).1.length = 1 ∧ (bumpStep^[n] ([c], acc, w)).2.1.length + (bumpStep^[n] ([c], acc, w)).2.2.length ≤ acc.length + w.length

The scan never has more in hand than it started with.

The packed scan

def Complexity.bumpPack (c acc rest : List Bool) : List Bool

The packed scan state.

Equations

• Complexity.bumpPack c acc rest = Complexity.pair c (Complexity.pair acc rest)

@[simp]

theorem Complexity.bumpPack_length (c acc rest : List Bool) : (bumpPack c acc rest).length = 2 * c.length + 2 * acc.length + rest.length + 4

def Complexity.bumpStepP (z : List Bool) : List Bool

One step of the packed scan.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.bumpStepP_pack (c acc rest : List Bool) : bumpStepP (bumpPack c acc rest) = bumpPack (bumpStep (c, acc, rest)).1 (bumpStep (c, acc, rest)).2.1 (bumpStep (c, acc, rest)).2.2

The packed step is the unpacked step.

theorem Complexity.bumpStepP_iterate (s : List Bool × List Bool × List Bool) (n : ℕ) : bumpStepP^[n] (bumpPack s.1 s.2.1 s.2.2) = bumpPack (bumpStep^[n] s).1 (bumpStep^[n] s).2.1 (bumpStep^[n] s).2.2

The packed iteration is the unpacked one.

theorem Complexity.bumpStepP_iterate_args (c acc rest : List Bool) (n : ℕ) : bumpStepP^[n] (bumpPack c acc rest) = bumpPack (bumpStep^[n] (c, acc, rest)).1 (bumpStep^[n] (c, acc, rest)).2.1 (bumpStep^[n] (c, acc, rest)).2.2

The packed iteration, with the state's three components spelled out.

The verdicts

def Complexity.bumpRun (w : List Bool) : List Bool

The packed scan run to completion.

Equations

• Complexity.bumpRun w = Complexity.bumpStepP^[w.length] (Complexity.bumpPack [true] [] w)

def Complexity.bumpCode (w : List Bool) : List Bool

The increment of w, computed by the scan.

Equations

• Complexity.bumpCode w = Complexity.pairFst (Complexity.pairSnd (Complexity.bumpRun w))

def Complexity.bumpFlag (w : List Bool) : List Bool

The carry out of the increment, as a flag.

Equations

• Complexity.bumpFlag w = Complexity.pairFst (Complexity.bumpRun w)

theorem Complexity.bumpRun_eq (w : List Bool) : bumpRun w = bumpPack [bumpOver w] (bumpBits w) []

@[simp]

theorem Complexity.bumpCode_eq (w : List Bool) : bumpCode w = bumpBits w

@[simp]

theorem Complexity.bumpFlag_eq (w : List Bool) : bumpFlag w = [bumpOver w]

Both are polynomial-time

theorem Complexity.bumpStepP_mem_FP : bumpStepP ∈ FP

theorem Complexity.bumpRunFn_mem_FP {a : List Bool → List Bool} (ha : a ∈ FP) : (fun (z : List Bool) => bumpRun (a z)) ∈ FP

The increment is polynomial-time.

theorem Complexity.bumpCodeFn_mem_FP {a : List Bool → List Bool} (ha : a ∈ FP) : (fun (z : List Bool) => bumpCode (a z)) ∈ FP

theorem Complexity.bumpFlagFn_mem_FP {a : List Bool → List Bool} (ha : a ∈ FP) : (fun (z : List Bool) => bumpFlag (a z)) ∈ FP