Fixed Word-RAM point updates for aggregation trees

The program walks from the root to the updated leaf. Every visited node is incremented, and the next subtree is selected by the position relative to half the current length. The same code handles every height, position and increment. Its arithmetic and all its loads, stores, tests and jumps are actual bounded-word instructions.

Main definitions

• updateLoop: the fixed update loop.
• Entry: the register calling convention.

Main results

• updateLoop_spec: logarithmic instruction bound, restored tree representation and a frame theorem for every memory word outside the tree.

References

• T. H. Cormen, C. E. Leiserson, R. L. Rivest and C. Stein, Introduction to Algorithms.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PrefixSums.Reg.zero : Fin 14

Constant zero.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PrefixSums.Reg.one : Fin 14

Constant one.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PrefixSums.Reg.two : Fin 14

Constant two.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PrefixSums.Reg.ptr : Fin 14

Current subtree pointer.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PrefixSums.Reg.len : Fin 14

Current subtree length.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PrefixSums.Reg.idx : Fin 14

Position relative to the current subtree.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PrefixSums.Reg.delta : Fin 14

Increment supplied to an update.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PrefixSums.Reg.val : Fin 14

Loaded value and arithmetic scratch.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PrefixSums.Reg.tmp : Fin 14

Address scratch.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PrefixSums.Reg.ans : Fin 14

Query answer.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PrefixSums.Reg.tag : Fin 14

Operation tag, zero for update and nonzero for query.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PrefixSums.Reg.root : Fin 14

Persistent root pointer.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PrefixSums.Reg.capacity : Fin 14

Persistent array capacity.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PrefixSums.Reg.position : Fin 14

External operation position.

structure Cslib.Algorithms.WordRAM.PrefixSums.Entry (b n i δ : ℕ) (x : WordRAM.Data 14) : Prop

Registers used by both tree traversals.

• zero_eq : x.regs Reg.zero = 0
• one_eq : x.regs Reg.one = 1
• two_eq : x.regs Reg.two = 2
• ptr_eq : x.regs Reg.ptr = b
• len_eq : x.regs Reg.len = n
• idx_eq : x.regs Reg.idx = i
• delta_eq : x.regs Reg.delta = δ

def Cslib.Algorithms.WordRAM.PrefixSums.updateBody : WordRAM.Code WordRAM.Basis.standard 14

Increment one node and move to the selected child. A leaf has half-length zero; the resulting length stops the loop before another access.

def Cslib.Algorithms.WordRAM.PrefixSums.updateLoop : WordRAM.Code WordRAM.Basis.standard 14

Fixed update code, independent of array size, position and increment.

def Cslib.Algorithms.WordRAM.PrefixSums.updateNext (x : WordRAM.Data 14) (b n i δ : ℕ) : WordRAM.Data 14

The data after one update iteration; this is a mathematical description, not an additional instruction in the machine.

theorem Cslib.Algorithms.WordRAM.PrefixSums.updateBody_exec {w b n i δ : ℕ} {x : WordRAM.Data 14} (hx : Entry b n i δ x) (hi : i < n) (ha : WordRAM.Fits w (b + 2 * n)) (hv : WordRAM.Fits w (x.mem b + δ)) : WordRAM.ExecWithin w updateBody x (updateNext x b n i δ) 9

theorem Cslib.Algorithms.WordRAM.PrefixSums.updateNext_entry {b n i δ : ℕ} {x : WordRAM.Data 14} (hx : Entry b n i δ x) : Entry (if i < n / 2 then b + 1 else b + n / 2 + n / 2) (n / 2) (if i < n / 2 then i else i - n / 2) δ (updateNext x b n i δ)

@[simp]

theorem Cslib.Algorithms.WordRAM.PrefixSums.updateNext_mem {b n i δ : ℕ} {x : WordRAM.Data 14} (a : ℕ) : (updateNext x b n i δ).mem a = Function.update x.mem b (x.mem b + δ) a

theorem Cslib.Algorithms.WordRAM.PrefixSums.updateLoop_spec {w h b i δ : ℕ} {x : WordRAM.Data 14} (t : Tree h) (hx : Entry b (2 ^ h) i δ x) (hi : i < 2 ^ h) (hr : t.Rep b x.mem) (ha : WordRAM.Fits w (b + 2 * 2 ^ h)) (hv : WordRAM.Fits w (t.total + δ)) : ∃ (y : WordRAM.Data 14), WordRAM.ExecWithin w updateLoop x y (11 * (h + 1) + 2) ∧ (t.add i δ).Rep b y.mem ∧ ∀ (a : ℕ), a < b ∨ b + Tree.words h ≤ a → y.mem a = x.mem a

The fixed update loop runs in at most 11 (h + 1) + 2 instructions. It restores the complete aggregation invariant and preserves every word outside the original footprint. The bound assumes the existing tree is supplied in memory; it does not include construction.