Bit encodings of Tree Evaluation instances

An instance of height h and value length ℓ is encoded by the unary header 1^ℓ 0 1^h 0, followed by its body in pre-order: a leaf is its ℓ bits, and a gate f is its table, the 4^ℓ * ℓ bits f (α k) (β k) i for k < 4^ℓ and i < ℓ in this order, where α k and β k read the low and high ℓ bits of k, followed by the bodies of its children.

The body of a subtree of height d has length bodyLength ℓ d, so the node at a path starts at the offset pathOffset, which a machine can recompute from the path alone.

Main definitions

• Cslib.TreeEval.Tree.body, Cslib.TreeEval.Tree.encode: the body and the full encoding.
• Cslib.TreeEval.tableBit: the bit of a gate's table at a position.
• Cslib.TreeEval.pathOffset: the offset of the node at a path within a body.

Main results

• Cslib.TreeEval.two_pow_ell_le_bodyLength, Cslib.TreeEval.two_pow_height_le_bodyLength: exponential lower bounds 2 ^ ℓ ≤ bodyLength ℓ H (for 1 ≤ ℓ, 1 ≤ H) and 2 ^ H ≤ bodyLength ℓ H (for 1 ≤ ℓ) on the body length.
• Cslib.TreeEval.Tree.getElem_body_pathOffset: the bits of the node at a path, read off the body at its offset; Cslib.TreeEval.Tree.getElem_body_gate and Cslib.TreeEval.Tree.getElem_body_leaf for gates and leaves.

References

• S. Cook, P. McKenzie, D. Wehr, M. Braverman and R. Santhanam, Pebbles and branching programs for tree evaluation introduce the problem, with gates given by their tables.

def Cslib.TreeEval.lowBits (ℓ k : ℕ) : Fin ℓ → Bool

The low ℓ bits of k.

def Cslib.TreeEval.highBits (ℓ k : ℕ) : Fin ℓ → Bool

The bits ℓ, …, 2ℓ - 1 of k.

def Cslib.TreeEval.tableLength (ℓ : ℕ) : ℕ

The number of bits in the table of a gate on ℓ-bit values.

def Cslib.TreeEval.tableBit {ℓ : ℕ} (f : Gate ℓ) (q : ℕ) : Bool

The bit at position q of the table of f: output bit q % ℓ on the inputs indexed by q / ℓ.

def Cslib.TreeEval.table {ℓ : ℕ} (f : Gate ℓ) : List Bool

The table of a gate.

@[simp]

theorem Cslib.TreeEval.length_table {ℓ : ℕ} (f : Gate ℓ) : (table f).length = tableLength ℓ

def Cslib.TreeEval.bodyLength (ℓ : ℕ) : ℕ → ℕ

The length of the body of a subtree of height d.

theorem Cslib.TreeEval.tableLength_le_bodyLength_of_pos {ℓ H : ℕ} (hH : 1 ≤ H) : tableLength ℓ ≤ bodyLength ℓ H

A tree of positive height includes at least the root gate table.

theorem Cslib.TreeEval.two_pow_ell_le_bodyLength {ℓ H : ℕ} (hℓ : 1 ≤ ℓ) (hH : 1 ≤ H) : 2 ^ ℓ ≤ bodyLength ℓ H

For 1 ≤ ℓ and 1 ≤ H, the body has length at least 2 ^ ℓ.

theorem Cslib.TreeEval.two_pow_height_le_bodyLength {ℓ : ℕ} (hℓ : 1 ≤ ℓ) (H : ℕ) : 2 ^ H ≤ bodyLength ℓ H

For 1 ≤ ℓ, the body of a height-H tree has length at least 2 ^ H.

def Cslib.TreeEval.pathOffset (ℓ : ℕ) : ℕ → List Bool → ℕ

The offset of the node at a path within the body of a subtree of height d.

def Cslib.TreeEval.Tree.body {ℓ h : ℕ} : Tree ℓ h → List Bool

The body of an instance: leaves by their values, gates by their tables, in pre-order.

@[simp]

theorem Cslib.TreeEval.Tree.length_body {ℓ h : ℕ} (T : Tree ℓ h) : T.body.length = bodyLength ℓ h

def Cslib.TreeEval.Tree.header (ℓ h : ℕ) : List Bool

The header 1^ℓ 0 1^h 0.

@[simp]

theorem Cslib.TreeEval.Tree.length_header (ℓ h : ℕ) : (header ℓ h).length = ℓ + h + 2

theorem Cslib.TreeEval.Tree.header_append_inj {ℓ h ℓ' h' : ℕ} {b b' : List Bool} (e : header ℓ h ++ b = header ℓ' h' ++ b') : ℓ = ℓ' ∧ h = h' ∧ b = b'

The header determines the value length and the height.

def Cslib.TreeEval.Tree.encode {ℓ h : ℕ} (T : Tree ℓ h) : List Bool

The encoding of an instance: its header, then its body.

@[simp]

theorem Cslib.TreeEval.Tree.length_encode {ℓ h : ℕ} (T : Tree ℓ h) : T.encode.length = ℓ + h + 2 + bodyLength ℓ h

def Cslib.TreeEval.Tree.Node.bits {ℓ : ℕ} : Node ℓ → List Bool

The bits of a node in the body: the value of a leaf, the table of a gate.

theorem Cslib.TreeEval.Tree.getElem_body_pathOffset {ℓ d : ℕ} (U : Tree ℓ d) {P : List Bool} {q : ℕ} (hq : q < (U.nodeAt P).bits.length) : U.body[pathOffset ℓ d P + q]? = (U.nodeAt P).bits[q]?

The bits of the node at a path, read off the body at the offset of the path.

theorem Cslib.TreeEval.Tree.getElem_body_gate {ℓ d : ℕ} (U : Tree ℓ d) {P : List Bool} {f : Gate ℓ} (hP : U.nodeAt P = Node.gate f) {q : ℕ} (hq : q < tableLength ℓ) : U.body[pathOffset ℓ d P + q]? = some (tableBit f q)

The table of the gate at a path, read off the body at the offset of the path.

theorem Cslib.TreeEval.Tree.getElem_body_leaf {ℓ d : ℕ} (U : Tree ℓ d) {P : List Bool} {v : Fin ℓ → Bool} (hP : U.nodeAt P = Node.leaf v) (i : Fin ℓ) : U.body[pathOffset ℓ d P + ↑i]? = some (v i)

The value of the leaf at a path, read off the body at the offset of the path.