Counting out the value of a bit string

A verifier turns its coins into an index — into a list of edges, say — and an index has to be counted out in unary before a polynomial-time loop can use it. This module does that: it reads a bit string as a little-endian binary number and writes that many marks.

The conversion is only polynomial time when the value is, which is why the result is clamped: the fold's state is truncated to a width the caller supplies. On strings short enough for the clamp — logarithmically many coins, say — the answer is exact.

Main definitions

• Complexity.unaryVal — the value of a bit string, in unary

Main results

• Complexity.unaryVal_eq — it is exact when the clamp is wide enough
• Complexity.unaryVal_mem_FP — it is polynomial time

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

Reading a zero: the value doubles.

Equations

• Complexity.binDbl z = Complexity.pairSnd (Complexity.pairFst z) ++ Complexity.pairSnd (Complexity.pairFst z)

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

Reading a one: the value doubles and gains one.

Equations

• Complexity.binDblOne z = Complexity.pairSnd (Complexity.pairFst z) ++ Complexity.pairSnd (Complexity.pairFst z) ++ [true]

theorem Complexity.binDbl_mem_FP : binDbl ∈ FP

theorem Complexity.binDblOne_mem_FP : binDblOne ∈ FP

def Complexity.unaryVal (p : Polynomial ℕ) (z : List Bool) : List Bool

The value of a bit string, in unary, computed on pair anything bits.

Equations

• Complexity.unaryVal p z = Complexity.Cobham.recFoldClamp Complexity.binDbl Complexity.binDblOne (Polynomial.eval z.length p) [] (Complexity.pairFst z) (Complexity.pairSnd z)

theorem Complexity.unaryVal_mem_FP (p : Polynomial ℕ) : unaryVal p ∈ FP

theorem Complexity.binValLE_cons_false (l : List Bool) : binValLE (false :: l) = 2 * binValLE l

theorem Complexity.binValLE_cons_true (l : List Bool) : binValLE (true :: l) = 2 * binValLE l + 1

theorem Complexity.recFoldClamp_binValLE (bound : ℕ) (W l : List Bool) : 2 ^ l.length ≤ bound → Cobham.recFoldClamp binDbl binDblOne bound [] W l = List.replicate (binValLE l) true

The fold really counts out the value, as long as the clamp is wide enough.

theorem Complexity.unaryVal_eq {p : Polynomial ℕ} {z : List Bool} (h : 2 ^ (pairSnd z).length ≤ Polynomial.eval z.length p) : unaryVal p z = List.replicate (binValLE (pairSnd z)) true

The conversion is exact when the clamp is wide enough for the value.