Fixed Word-RAM prefix queries

The query descends through an aggregation tree, adding the complete left subtree whenever it descends right. It stops at an empty prefix or a complete subtree. The program is fixed; the array size, query position and tree pointer are register inputs.

Main definitions

• queryLoop: a fixed program for prefix queries.

Main results

• queryLoop_spec: the answer equals the mathematical prefix sum within 13 (h + 1) + 2 instructions, with all memory preserved.

References

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

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

One prefix-query iteration.

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

Fixed prefix-query loop. Its answer is added to the initial accumulator.

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

Mathematical description of one query iteration, used only in the proof.

theorem Cslib.Algorithms.WordRAM.PrefixSums.queryBody_exec {w b n i δ a : ℕ} {x : WordRAM.Data 14} (hx : Entry b n i δ x) (hi : i ≤ n) (hn : 0 < n) (hxans : x.regs Reg.ans = a) (ha : WordRAM.Fits w (b + 2 * n)) (hv : WordRAM.Fits w (a + x.mem b)) (hl : i ≠ n → n / 2 ≤ i → WordRAM.Fits w (a + x.mem (b + 1))) : WordRAM.ExecWithin w queryBody x (queryNext x b n i a) 11

@[simp]

theorem Cslib.Algorithms.WordRAM.PrefixSums.queryNext_mem {b n i a : ℕ} {x : WordRAM.Data 14} : (queryNext x b n i a).mem = x.mem

theorem Cslib.Algorithms.WordRAM.PrefixSums.queryNext_entry {b n i δ a : ℕ} {x : WordRAM.Data 14} (hx : Entry b n i δ x) (he : i ≠ n) : 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) δ (queryNext x b n i a)

theorem Cslib.Algorithms.WordRAM.PrefixSums.queryLoop_full {w b n δ a : ℕ} {x : WordRAM.Data 14} (hx : Entry b n n δ x) (hn : 0 < n) (hxans : x.regs Reg.ans = a) (ha : WordRAM.Fits w (b + 2 * n)) (hv : WordRAM.Fits w (a + x.mem b)) : ∃ (y : WordRAM.Data 14), WordRAM.ExecWithin w queryLoop x y 15 ∧ y.regs Reg.ans = a + x.mem b ∧ y.mem = x.mem

theorem Cslib.Algorithms.WordRAM.PrefixSums.queryLoop_spec {w h b i δ a : ℕ} {x : WordRAM.Data 14} (t : Tree h) (hx : Entry b (2 ^ h) i δ x) (hi : i ≤ 2 ^ h) (hxans : x.regs Reg.ans = a) (hr : t.Rep b x.mem) (ha : WordRAM.Fits w (b + 2 * 2 ^ h)) (hv : WordRAM.Fits w (a + t.total)) : ∃ (y : WordRAM.Data 14), WordRAM.ExecWithin w queryLoop x y (13 * (h + 1) + 2) ∧ y.regs Reg.ans = a + t.prefixSum i ∧ y.mem = x.mem

A query adds precisely the first i leaf values to its initial accumulator, using at most 13 (h + 1) + 2 instructions. The whole memory is unchanged. Bounds include the loop tests and jumps, but entry-register installation and tree construction are separate.