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

• queryBody, queryLoop, queryNext: one iteration of a prefix query, the fixed prefix-query loop, and the state transition of one iteration.

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.

@[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

One prefix-query iteration leaves RAM memory unchanged.

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.