What the bracket scan computes

A model of the left-to-right pass over a serialized Data value: a bracket depth, a count of the top-level children already passed, and the bits collected while inside the child that was asked for. This file is about the model alone — that it really does extract the requested child — and says nothing about computability.

Two facts drive everything. The depth and the count evolve without looking at the collected bits, and the collected bits only ever grow at the end (runSpec_append_acc); and a serialized value read at any depth returns to that depth, having contributed exactly its own serialization when it was the child being sought (runSpec_toBits).

Main definitions

• Complexity.DataScan.runSpec — the model of the pass

Main results

• Complexity.DataScan.runSpec_toBits — reading one serialized value
• Complexity.DataScan.runSpec_flatten — reading a whole run of children
• Complexity.DataScan.runSpec_inner — the pass over a serialized list returns the requested child

def Complexity.DataScan.stepSpec (i : ℕ) (st : ℕ × ℕ × List Bool) (b : Bool) : ℕ × ℕ × List Bool

One step of the pass: false opens a bracket, true closes one, and the bit joins the output exactly when the count matches the child sought.

Equations

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

def Complexity.DataScan.runSpec (i : ℕ) (st : ℕ × ℕ × List Bool) (s : List Bool) : ℕ × ℕ × List Bool

The pass over a whole string.

Equations

• Complexity.DataScan.runSpec i st s = List.foldl (Complexity.DataScan.stepSpec i) st s

@[simp]

theorem Complexity.DataScan.runSpec_nil (i : ℕ) (st : ℕ × ℕ × List Bool) : runSpec i st [] = st

theorem Complexity.DataScan.runSpec_append (i : ℕ) (st : ℕ × ℕ × List Bool) (s t : List Bool) : runSpec i st (s ++ t) = runSpec i (runSpec i st s) t

theorem Complexity.DataScan.runSpec_cons (i : ℕ) (st : ℕ × ℕ × List Bool) (b : Bool) (s : List Bool) : runSpec i st (b :: s) = runSpec i (stepSpec i st b) s

theorem Complexity.DataScan.runSpec_append_acc (i : ℕ) (s : List Bool) (d c : ℕ) (pre acc : List Bool) : runSpec i (d, c, pre ++ acc) s = ((runSpec i (d, c, acc) s).fst, (runSpec i (d, c, acc) s).snd.fst, pre ++ (runSpec i (d, c, acc) s).snd.snd)

The collected bits only grow at the end. A prefix already present in the output is carried through untouched, and the depth and count do not see it.

theorem Complexity.DataScan.runSpec_toBits (i : ℕ) (y : Data) (d c : ℕ) (acc : List Bool) : runSpec i (d, c, acc) y.toBits = (d, if d = 0 then c + 1 else c, if c = i then acc ++ y.toBits else acc)

Reading one serialized value. Starting at depth d with c children already passed, the pass over y.toBits returns to depth d; it counts one more child exactly when it was at the top level, and it contributes y.toBits to the output exactly when y is the child sought.

A run of children

def Complexity.DataScan.selFrom (xs : List Data) (i c : ℕ) : List Bool

The child a pass looking for index i picks out of xs, having already passed c children.

Equations

• Complexity.DataScan.selFrom xs i c = if c ≤ i then (Option.map Complexity.Data.toBits xs[i - c]?).getD [] else []

@[simp]

theorem Complexity.DataScan.selFrom_nil (i c : ℕ) : selFrom [] i c = []

theorem Complexity.DataScan.runSpec_flatten (i : ℕ) (xs : List Data) (c : ℕ) (acc : List Bool) : runSpec i (0, c, acc) (List.map Data.toBits xs).flatten = (0, c + xs.length, acc ++ selFrom xs i c)

Reading a run of children. At the top level the pass counts every child and contributes exactly the one it was asked for.

theorem Complexity.DataScan.runSpec_inner (i : ℕ) (xs : List Data) : runSpec i (0, 0, []) (List.map Data.toBits xs).flatten = (0, xs.length, (Option.map Data.toBits xs[i]?).getD [])

The pass over a serialized list. Reading the bits strictly between the outer brackets returns the requested child's own serialization.