Contiguous static fusion-tree records

Every record has an 18-word header. Leaves store tag 0, presence, and key (zero when absent), followed by fifteen zero words. Internal nodes have tag 1, followed by exactly n interleaved pairs of full child minima and absolute child pointers, and the recursively encoded children in order. No capacity-sized arrays are allocated. The header indices are: tag 0, child count 1, minimum 2, compression mask C 3, multiplier digits 4--6, D 7, copies 8, packed complements 9, packed normal 10, guards 11, bits 12, middle 13, radix 14, maximum 15, width-dependent global offset 16, and reserved 17. Parameters supplies indices 3--17; it asserts no node-search oracle.

This is a static representation, with explicit arena/address and stored-word fit contracts. It asserts neither preprocessing time nor a query running time.

Main definitions

• span, encode: allocation length and concrete list of RAM words.
• Rep: actual memory realizes that list using WordRAM.Block.Realizes.
• ArenaFits, ContentFits: separate address/frontier and stored-content contracts.

Main results

• encode_length: the concrete list has precisely the claimed allocation length.
• Rep.node_header, Rep.child: literal loads and recursive child representations.
• child_span_le, access_owned, child_access_owned: allocation safety.
• decode_encode: the concrete memory round-trips through a load-based decoder.
• span_build_le: at most 126n + 18 allocated words, uniformly in branching capacity.
• encoding_exists: a fitting concrete memory, decoder and linear allocation bound together.

References

• [FW93]

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.Parameters : Type

The fifteen preprocessing words in header slots 3 through 17, for each internal node. The final two slots accommodate a width-dependent global offset and one reserved word.

def Cslib.Algorithms.WordRAM.FusionTree.headerWords : ℕ

Fixed record header length, independent of branching capacity.

Stable offsets within internal headers. The fifteen parameter words are named here so node-search implementations can use the layout without duplicating numerical indices.

def Cslib.Algorithms.WordRAM.FusionTree.HeaderOffset.tag : ℕ

Record tag: 0 for leaves, 1 for internal nodes.

def Cslib.Algorithms.WordRAM.FusionTree.HeaderOffset.count : ℕ

Number of actual children (presence for a leaf).

def Cslib.Algorithms.WordRAM.FusionTree.HeaderOffset.minimum : ℕ

Cached minimum (the key for a leaf).

def Cslib.Algorithms.WordRAM.FusionTree.HeaderOffset.compression : ℕ

Compression mask C.

def Cslib.Algorithms.WordRAM.FusionTree.HeaderOffset.multiplierLow : ℕ

First multiplier digit.

def Cslib.Algorithms.WordRAM.FusionTree.HeaderOffset.multiplierMiddle : ℕ

Second multiplier digit.

def Cslib.Algorithms.WordRAM.FusionTree.HeaderOffset.multiplierHigh : ℕ

Third multiplier digit.

def Cslib.Algorithms.WordRAM.FusionTree.HeaderOffset.maskD : ℕ

Compression mask D.

def Cslib.Algorithms.WordRAM.FusionTree.HeaderOffset.copies : ℕ

Copies constant.

def Cslib.Algorithms.WordRAM.FusionTree.HeaderOffset.packedComplements : ℕ

Packed complement sketches.

def Cslib.Algorithms.WordRAM.FusionTree.HeaderOffset.packedNormal : ℕ

Packed ordinary sketches.

def Cslib.Algorithms.WordRAM.FusionTree.HeaderOffset.guards : ℕ

Packed field guards.

def Cslib.Algorithms.WordRAM.FusionTree.HeaderOffset.bits : ℕ

Sketch bit count.

def Cslib.Algorithms.WordRAM.FusionTree.HeaderOffset.middle : ℕ

Middle-field constant.

def Cslib.Algorithms.WordRAM.FusionTree.HeaderOffset.radix : ℕ

Packed field radix.

def Cslib.Algorithms.WordRAM.FusionTree.HeaderOffset.maximum : ℕ

Maximum compressed payload.

def Cslib.Algorithms.WordRAM.FusionTree.HeaderOffset.globalOffset : ℕ

Width-dependent global offset.

def Cslib.Algorithms.WordRAM.FusionTree.HeaderOffset.reserved : ℕ

Reserved preprocessing word.

@[irreducible]

def Cslib.Algorithms.WordRAM.FusionTree.span : Lean.FusionTree.Tree → ℕ

Actual allocated words, without any padding to the maximum branching capacity.

def Cslib.Algorithms.WordRAM.FusionTree.childAddress (base : ℕ) (cs : List Lean.FusionTree.Tree) (i : ℕ) : ℕ

Starting address of child i, after the parent's actual tables and earlier children.

def Cslib.Algorithms.WordRAM.FusionTree.header (p : Parameters) (m : ℕ) (cs : List Lean.FusionTree.Tree) : List ℕ

The concrete internal header.

def Cslib.Algorithms.WordRAM.FusionTree.childTable (base : ℕ) (cs : List Lean.FusionTree.Tree) : List ℕ

Stride-two child table: a full minimum followed by its absolute pointer.

def Cslib.Algorithms.WordRAM.FusionTree.encode (p : Parameters) (base : ℕ) : Lean.FusionTree.Tree → List ℕ

Serialize a tree at its absolute address. Invalid nonsingleton leaves are truncated; decode_encode requires Tree.Valid, which excludes them.

def Cslib.Algorithms.WordRAM.FusionTree.encodeForest (p : Parameters) (base : ℕ) : List Lean.FusionTree.Tree → List ℕ

Serialize consecutive child records; the next record starts at the previous one's end.

theorem Cslib.Algorithms.WordRAM.FusionTree.encode_length (p : Parameters) (base : ℕ) (t : Lean.FusionTree.Tree) : (encode p base t).length = span t

Every serialized tree occupies exactly its claimed span.

theorem Cslib.Algorithms.WordRAM.FusionTree.encodeForest_length (p : Parameters) (base : ℕ) (cs : List Lean.FusionTree.Tree) : (encodeForest p base cs).length = (List.map span cs).sum

The concrete child-record list has the sum of the child spans as its length.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.Stores (xs : List ℕ) (base : ℕ) (mem : ℕ → ℕ) : Prop

Actual RAM contents of a contiguous list, using the existing allocation API.

def Cslib.Algorithms.WordRAM.FusionTree.Rep (p : Parameters) (t : Lean.FusionTree.Tree) (base : ℕ) (mem : ℕ → ℕ) : Prop

Memory represents the concrete serialized tree, with arbitrary memory outside its block.

def Cslib.Algorithms.WordRAM.FusionTree.arena (p : Parameters) (t : Lean.FusionTree.Tree) (base : ℕ) : WordRAM.HeapAssertion

The existing heap assertion for the serialized arena, including exactly its allocated cells.

theorem Cslib.Algorithms.WordRAM.FusionTree.arena_holds (p : Parameters) (t : Lean.FusionTree.Tree) (base : ℕ) (mem : ℕ → ℕ) : (arena p t base).holds mem ↔ Rep p t base mem

The heap assertion's contents are exactly the representation predicate.

theorem Cslib.Algorithms.WordRAM.FusionTree.arena_footprint (p : Parameters) (t : Lean.FusionTree.Tree) (base : ℕ) : (arena p t base).footprint = { base := base, length := span t }.footprint

The heap footprint counts actual allocated words, including each fixed header.

theorem Cslib.Algorithms.WordRAM.FusionTree.Rep.frame {p : Parameters} {t : Lean.FusionTree.Tree} {base : ℕ} {mem mem' : ℕ → ℕ} {writes : Finset ℕ} (hr : Rep p t base mem) (hd : Disjoint { base := base, length := span t }.footprint writes) (hm : WordRAM.Modifies writes mem mem') : Rep p t base mem'

Writes disjoint from the contiguous arena preserve the complete tree representation.

def Cslib.Algorithms.WordRAM.FusionTree.memory (p : Parameters) (t : Lean.FusionTree.Tree) (base : ℕ) : ℕ → ℕ

A concrete total memory obtained by placing the serialized words into an otherwise zero RAM.

theorem Cslib.Algorithms.WordRAM.FusionTree.rep_memory (p : Parameters) (t : Lean.FusionTree.Tree) (base : ℕ) : Rep p t base (memory p t base)

The explicit list encoding has an actual RAM realization.

theorem Cslib.Algorithms.WordRAM.FusionTree.Rep.node_parts {p : Parameters} {m base : ℕ} {cs : List Lean.FusionTree.Tree} {mem : ℕ → ℕ} (hr : Rep p (Lean.FusionTree.Tree.node m cs) base mem) : Stores (header p m cs) base mem ∧ Stores (childTable base cs) (base + headerWords) mem ∧ Stores (encodeForest p (base + headerWords + 2 * cs.length) cs) (base + headerWords + 2 * cs.length) mem

A represented internal node exposes its header, minima, pointers and child-record interval.

theorem Cslib.Algorithms.WordRAM.FusionTree.Rep.node_header {p : Parameters} {m base : ℕ} {cs : List Lean.FusionTree.Tree} {mem : ℕ → ℕ} (hr : Rep p (Lean.FusionTree.Tree.node m cs) base mem) : mem base = 1 ∧ mem (base + 1) = cs.length ∧ mem (base + 2) = m ∧ ∀ (j : Fin 15), mem (base + 3 + ↑j) = p (Lean.FusionTree.Tree.node m cs) j

The first three internal header words and all fifteen preprocessing words decode literally.

theorem Cslib.Algorithms.WordRAM.FusionTree.Rep.leaf_fields {p : Parameters} {base : ℕ} {xs : List ℕ} {mem : ℕ → ℕ} (hr : Rep p (Lean.FusionTree.Tree.leaf xs) base mem) : mem base = 0 ∧ (mem (base + 1) = if xs.isEmpty = true then 0 else 1) ∧ mem (base + 2) = xs.headD 0

The three leaf words decode as tag, presence and key.

theorem Cslib.Algorithms.WordRAM.FusionTree.Rep.child {p : Parameters} {m base : ℕ} {cs : List Lean.FusionTree.Tree} {mem : ℕ → ℕ} (hr : Rep p (Lean.FusionTree.Tree.node m cs) base mem) (i : Fin cs.length) : mem (base + headerWords + 2 * ↑i) = cs[i].minimum ∧ mem (base + headerWords + (2 * ↑i + 1)) = childAddress base cs ↑i ∧ Rep p cs[i] (childAddress base cs ↑i) mem

Following a stored child pointer gives the representation of precisely that child.

theorem Cslib.Algorithms.WordRAM.FusionTree.span_pos (t : Lean.FusionTree.Tree) : 0 < span t

Every record is nonempty, including the empty leaf.

theorem Cslib.Algorithms.WordRAM.FusionTree.child_span_le (base m : ℕ) (cs : List Lean.FusionTree.Tree) (i : Fin cs.length) : base + headerWords + 2 * cs.length ≤ childAddress base cs ↑i ∧ childAddress base cs ↑i + span cs[i] ≤ base + span (Lean.FusionTree.Tree.node m cs)

A whole child allocation lies inside its parent's allocation.

theorem Cslib.Algorithms.WordRAM.FusionTree.access_owned (base : ℕ) (t : Lean.FusionTree.Tree) (a : ℕ) (ha : a < span t) : { base := base, length := span t }.Owns (base + a)

Every valid offset denotes an allocated cell, including the full leaf header.

theorem Cslib.Algorithms.WordRAM.FusionTree.node_access_owned (base m : ℕ) (cs : List Lean.FusionTree.Tree) (a : ℕ) (ha : a < headerWords + 2 * cs.length) : { base := base, length := span (Lean.FusionTree.Tree.node m cs) }.Owns (base + a)

Every direct header/table read is an owned parent word. Tables use their actual lengths.

theorem Cslib.Algorithms.WordRAM.FusionTree.header_access_owned (base : ℕ) (t : Lean.FusionTree.Tree) (j : Fin 18) : { base := base, length := span t }.Owns (base + ↑j)

Each of the eighteen header loads lies inside the record, including for empty leaves.

theorem Cslib.Algorithms.WordRAM.FusionTree.child_entry_access_owned (base m : ℕ) (cs : List Lean.FusionTree.Tree) (i : Fin cs.length) : { base := base, length := span (Lean.FusionTree.Tree.node m cs) }.Owns (base + headerWords + 2 * ↑i) ∧ { base := base, length := span (Lean.FusionTree.Tree.node m cs) }.Owns (base + headerWords + (2 * ↑i + 1))

Both stride-two table loads are inside the parent's allocation.

theorem Cslib.Algorithms.WordRAM.FusionTree.child_access_owned (base m : ℕ) (cs : List Lean.FusionTree.Tree) (i : Fin cs.length) (a : ℕ) (ha : a < span cs[i]) : { base := base, length := span (Lean.FusionTree.Tree.node m cs) }.Owns (childAddress base cs ↑i + a)

Every word read inside a child record is owned by the parent allocation. Repeated use provides the same guarantee at arbitrary descendant depth.

theorem Cslib.Algorithms.WordRAM.FusionTree.span_le_slots (t : Lean.FusionTree.Tree) : span t ≤ 9 * t.slots

The concrete allocation is at most nine times the structural scalar-slot count.

theorem Cslib.Algorithms.WordRAM.FusionTree.span_build_le {B : ℕ} (hB : 2 ≤ B) (xs : List ℕ) : span (Lean.FusionTree.Tree.build B xs) ≤ 126 * xs.length + 18

Uniform linear allocated RAM words, with constants independent of branching capacity and word width. This counts the actual serialized words, including all preprocessing headers.

theorem Cslib.Algorithms.WordRAM.FusionTree.span_build_le_uniform {B : ℕ} (hB : 2 ≤ B) (xs : List ℕ) : span (Lean.FusionTree.Tree.build B xs) ≤ 126 * xs.length + 126

A single absolute constant works for both terms in the usual C * n + C bound.

def Cslib.Algorithms.WordRAM.FusionTree.decode : ℕ → (ℕ → ℕ) → ℕ → Lean.FusionTree.Tree

Recover the functional tree by loads of tags, fields and absolute child pointers. Fuel bounds recursive depth, not the number of machine instructions. The zero-fuel result is a default; correctness requires fuel strictly larger than the tree height.

theorem Cslib.Algorithms.WordRAM.FusionTree.decode_rep {B fuel base : ℕ} {p : Parameters} {t : Lean.FusionTree.Tree} {mem : ℕ → ℕ} (ht : Lean.FusionTree.Tree.Valid B t) (hr : Rep p t base mem) (hf : t.height < fuel) : decode fuel mem base = t

Concrete RAM decoding recovers every valid tree. In particular, empty and singleton leaves remain distinct even when the stored key is zero.

theorem Cslib.Algorithms.WordRAM.FusionTree.decode_encode {B fuel : ℕ} {t : Lean.FusionTree.Tree} (ht : Lean.FusionTree.Tree.Valid B t) (hf : t.height < fuel) (p : Parameters) (base : ℕ) : decode fuel (memory p t base) base = t

The explicit serializer and total RAM realization round-trip through the load-based decoder.

def Cslib.Algorithms.WordRAM.FusionTree.ArenaFits (w base : ℕ) (t : Lean.FusionTree.Tree) : Prop

Every owned address and the one-past-end allocation frontier fit a word. This strict frontier condition also suffices for the existing WordRAM.alloc execution contract.

theorem Cslib.Algorithms.WordRAM.FusionTree.arenaFits_build_of_bound {B w base : ℕ} (hB : 2 ≤ B) (xs : List ℕ) (hw : WordRAM.Fits w (base + 126 * xs.length + 18)) : ArenaFits w base (Lean.FusionTree.Tree.build B xs)

A numerical sufficient arena contract, using only input length and the allocation base. It bounds the entire one-past-end frontier, rather than only the input key values.

theorem Cslib.Algorithms.WordRAM.FusionTree.ArenaFits.allocation {w base : ℕ} {t : Lean.FusionTree.Tree} (ha : ArenaFits w base t) : WordRAM.Fits w base ∧ WordRAM.Fits w (span t) ∧ WordRAM.Fits w 1

Allocation size, base address and tag one all fit under the arena contract. Together with the fitting frontier, these are the numerical inputs to WordRAM.alloc_exec.

@[irreducible]

def Cslib.Algorithms.WordRAM.FusionTree.ContentFits (w : ℕ) (p : Parameters) : Lean.FusionTree.Tree → Prop

Explicit key and preprocessing-word assumptions. Child counts and addresses are instead bounded by ArenaFits; fitting input keys alone does not imply either contract.

theorem Cslib.Algorithms.WordRAM.FusionTree.ContentFits.minimum {w : ℕ} {p : Parameters} {t : Lean.FusionTree.Tree} (ht : ContentFits w p t) : WordRAM.Fits w t.minimum

Cached child minima fit whenever all explicit tree contents fit.

theorem Cslib.Algorithms.WordRAM.FusionTree.ArenaFits.address {w base a : ℕ} {t : Lean.FusionTree.Tree} (ha : ArenaFits w base t) (ho : { base := base, length := span t }.Owns a) : WordRAM.Fits w a

The fit assumption for the arena bounds every owned access address.

theorem Cslib.Algorithms.WordRAM.FusionTree.ArenaFits.child {w base m : ℕ} {cs : List Lean.FusionTree.Tree} (ha : ArenaFits w base (Lean.FusionTree.Tree.node m cs)) (i : Fin cs.length) : ArenaFits w (childAddress base cs ↑i) cs[i]

The child's whole allocation also fits; in particular following its pointer cannot wrap.

theorem Cslib.Algorithms.WordRAM.FusionTree.encode_fits {w : ℕ} {p : Parameters} (t : Lean.FusionTree.Tree) (base : ℕ) : ArenaFits w base t → ContentFits w p t → ∀ v ∈ encode p base t, WordRAM.Fits w v

Every serialized data word fits under explicit content and arena assumptions.

theorem Cslib.Algorithms.WordRAM.FusionTree.memory_fits {w base : ℕ} {p : Parameters} {t : Lean.FusionTree.Tree} (ha : ArenaFits w base t) (ht : ContentFits w p t) (a : ℕ) : WordRAM.Fits w (memory p t base a)

The concrete memory consists entirely of fitting words, including its zero exterior.

theorem Cslib.Algorithms.WordRAM.FusionTree.encoding_exists {B w base : ℕ} (hB : 2 ≤ B) (xs : List ℕ) (p : Parameters) (ha : ArenaFits w base (Lean.FusionTree.Tree.build B xs)) (ht : ContentFits w p (Lean.FusionTree.Tree.build B xs)) : ∃ (mem : ℕ → ℕ), Rep p (Lean.FusionTree.Tree.build B xs) base mem ∧ (∀ (a : ℕ), WordRAM.Fits w (mem a)) ∧ decode ((Lean.FusionTree.Tree.build B xs).height + 1) mem base = Lean.FusionTree.Tree.build B xs ∧ (encode p base (Lean.FusionTree.Tree.build B xs)).length ≤ 126 * xs.length + 18

A fitting contiguous encoding exists for every built tree whose explicit address and content assumptions hold. The decoder uses depth fuel; no preprocessing-time claim is made.