Scanning a serialized Data value

Data.toBits writes a value as balanced brackets: false opens a node, its children follow in order, and true closes it. Reading one child back out of such a string is a single left-to-right pass keeping a bracket depth and a count of the children already passed, collecting bits only while inside the child asked for.

This module writes that pass in the form recFoldClamp accepts, so that polynomial-time computability comes from the general fold rather than from a bespoke machine. The fold recurses head-then-tail, so it runs right to left; the caller therefore hands it the reversed string.

The state is pair (unary depth) (pair (unary count) collected) and the workspace is the requested index in unary. Every component stays below the length of the string being scanned, so a linear clamp suffices.

Main definitions

• Complexity.DataScan.openStep, closeStep — the two fold steps
• Complexity.DataScan.childOf — the scan, packaged as one function

Main results

• Complexity.DataScan.childOf_mem_FP — the scan is polynomial time
• Complexity.DataScan.recFoldClamp_eq_pack — the fold runs the model
• Complexity.DataScan.child_flatten — the packaged scan extracts the child
• Complexity.DataScan.childCount_flatten — and counts the children
• Complexity.DataScan.inner_toBits — the bits between the outer brackets

Reading the packed fold argument

recFoldClamp hands each step pair (pair W st) t, with W the workspace, st the state built so far and t the unscanned tail.

def Complexity.DataScan.wsOf (z : List Bool) : List Bool

The workspace: the index of the child being extracted, in unary.

Equations

• Complexity.DataScan.wsOf z = Complexity.pairFst (Complexity.pairFst z)

def Complexity.DataScan.stOf (z : List Bool) : List Bool

The state carried by the scan.

Equations

• Complexity.DataScan.stOf z = Complexity.pairSnd (Complexity.pairFst z)

def Complexity.DataScan.depthOf (z : List Bool) : List Bool

The bracket depth, in unary.

Equations

• Complexity.DataScan.depthOf z = Complexity.pairFst (Complexity.DataScan.stOf z)

def Complexity.DataScan.countOf (z : List Bool) : List Bool

The number of children already passed, in unary.

Equations

• Complexity.DataScan.countOf z = Complexity.pairFst (Complexity.pairSnd (Complexity.DataScan.stOf z))

def Complexity.DataScan.accOf (z : List Bool) : List Bool

The bits collected so far.

Equations

• Complexity.DataScan.accOf z = Complexity.pairSnd (Complexity.pairSnd (Complexity.DataScan.stOf z))

def Complexity.DataScan.collect (z : List Bool) (b : Bool) : List Bool

Append the current bit, but only while inside the requested child.

Equations

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

The two steps

def Complexity.DataScan.openStep (z : List Bool) : List Bool

An opening bracket: descend one level.

Equations

• Complexity.DataScan.openStep z = Complexity.pair (true :: Complexity.DataScan.depthOf z) (Complexity.pair (Complexity.DataScan.countOf z) (Complexity.DataScan.collect z false))

def Complexity.DataScan.closeStep (z : List Bool) : List Bool

A closing bracket: rise one level, and if that returns to the top level, one more child has been passed.

Equations

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

def Complexity.DataScan.initState : List Bool

The state a scan starts from.

Equations

• Complexity.DataScan.initState = Complexity.pair [] (Complexity.pair [] [])

Polynomial time

theorem Complexity.DataScan.wsOf_mem_FP : wsOf ∈ FP

theorem Complexity.DataScan.stOf_mem_FP : stOf ∈ FP

theorem Complexity.DataScan.depthOf_mem_FP : depthOf ∈ FP

theorem Complexity.DataScan.countOf_mem_FP : countOf ∈ FP

theorem Complexity.DataScan.accOf_mem_FP : accOf ∈ FP

theorem Complexity.DataScan.collect_mem_FP (b : Bool) : (fun (z : List Bool) => collect z b) ∈ FP

theorem Complexity.DataScan.openStep_mem_FP : openStep ∈ FP

theorem Complexity.DataScan.closeStep_mem_FP : closeStep ∈ FP

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

The scan. On pair (unary i) s it runs the two steps over s, keeping every intermediate state within p.eval bits, and returns the collected bits.

Equations

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

theorem Complexity.DataScan.childOf_mem_FP (p : Polynomial ℕ) : childOf p ∈ FP

The fold runs the model

The state the fold carries is the model's state written out: two unary counters and the collected bits. Once that is checked step by step, the fold and the model agree, provided the clamp is wide enough never to truncate.

def Complexity.DataScan.pack (st : ℕ × ℕ × List Bool) : List Bool

The model's state, written out as a bitstring.

Equations

• Complexity.DataScan.pack st = Complexity.pair (List.replicate st.1 true) (Complexity.pair (List.replicate st.2.1 true) st.2.2)

theorem Complexity.DataScan.pack_length (st : ℕ × ℕ × List Bool) : (pack st).length = 2 * st.1 + 2 * st.2.1 + st.2.2.length + 4

theorem Complexity.DataScan.pack_init : pack (0, 0, []) = initState

theorem Complexity.DataScan.eqFlag_replicate (c i : ℕ) : Cobham.eqFlag (List.replicate c true) (List.replicate i true) = if c = i then [true] else [false]

theorem Complexity.DataScan.depthOf_pack (i : ℕ) (st : ℕ × ℕ × List Bool) (t : List Bool) : depthOf (pair (pair (List.replicate i true) (pack st)) t) = List.replicate st.1 true

theorem Complexity.DataScan.countOf_pack (i : ℕ) (st : ℕ × ℕ × List Bool) (t : List Bool) : countOf (pair (pair (List.replicate i true) (pack st)) t) = List.replicate st.2.1 true

theorem Complexity.DataScan.collect_pack (i : ℕ) (st : ℕ × ℕ × List Bool) (t : List Bool) (b : Bool) : collect (pair (pair (List.replicate i true) (pack st)) t) b = if st.2.1 = i then st.2.2 ++ [b] else st.2.2

theorem Complexity.DataScan.openStep_pack (i : ℕ) (st : ℕ × ℕ × List Bool) (t : List Bool) : openStep (pair (pair (List.replicate i true) (pack st)) t) = pack (stepSpec i st false)

theorem Complexity.DataScan.closeStep_pack (i : ℕ) (st : ℕ × ℕ × List Bool) (t : List Bool) : closeStep (pair (pair (List.replicate i true) (pack st)) t) = pack (stepSpec i st true)

The state stays small

theorem Complexity.DataScan.runSpec_bounds (i : ℕ) (s : List Bool) (d c : ℕ) (acc : List Bool) : (runSpec i (d, c, acc) s).1 ≤ d + s.length ∧ (runSpec i (d, c, acc) s).2.1 ≤ c + s.length ∧ (runSpec i (d, c, acc) s).2.2.length ≤ acc.length + s.length

theorem Complexity.DataScan.pack_runSpec_length_le (i : ℕ) (s : List Bool) : (pack (runSpec i (0, 0, []) s)).length ≤ 5 * s.length + 4

theorem Complexity.DataScan.recFoldClamp_eq_pack (i bound : ℕ) (l : List Bool) (hb : 5 * l.length + 4 ≤ bound) : Cobham.recFoldClamp openStep closeStep bound initState (List.replicate i true) l = pack (runSpec i (0, 0, []) l.reverse)

The fold runs the model. Reading the reversed string with the clamped fold gives exactly the model's state, as long as the clamp is wide enough.

The packaged scan

noncomputable def Complexity.DataScan.scanPoly : Polynomial ℕ

A clamp wide enough for any scan: the state never exceeds 5 n + 4 bits.

Equations

• Complexity.DataScan.scanPoly = Polynomial.C 5 * Polynomial.X + Polynomial.C 4

@[simp]

theorem Complexity.DataScan.scanPoly_eval (n : ℕ) : Polynomial.eval n scanPoly = 5 * n + 4

def Complexity.DataScan.scanArg (i : ℕ) (s : List Bool) : List Bool

The scan's argument: the index in unary paired with the reversed string, the order the fold consumes.

Equations

• Complexity.DataScan.scanArg i s = Complexity.pair (List.replicate i true) s.reverse

theorem Complexity.DataScan.scanArg_mem_FP {a b : List Bool → List Bool} (ha : a ∈ FP) (hb : b ∈ FP) : (fun (z : List Bool) => scanArg (a z).length (b z)) ∈ FP

theorem Complexity.DataScan.child_flatten (i : ℕ) (xs : List Data) : childOf scanPoly (scanArg i (List.map Data.toBits xs).flatten) = (Option.map Data.toBits xs[i]?).getD []

The scan extracts the child. Reading the concatenated serializations of xs returns the i-th one, or nothing when there is no such child.

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

How many children there are, in unary: the same pass, reading off the counter instead of the collected bits.

Equations

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

theorem Complexity.DataScan.childCount_mem_FP (p : Polynomial ℕ) : childCount p ∈ FP

theorem Complexity.DataScan.childCount_flatten (i : ℕ) (xs : List Data) : childCount scanPoly (scanArg i (List.map Data.toBits xs).flatten) = List.replicate xs.length true

theorem Complexity.DataScan.inner_toBits (xs : List Data) : List.take ((Data.l xs).toBits.length - 2) (List.drop 1 (Data.l xs).toBits) = (List.map Data.toBits xs).flatten

The bits strictly between the outer brackets of a serialized list.