Stateful prefix sums implemented by one fixed Word-RAM program

The abstract state is a list, independently of the tree representation. An operation either increments one entry or returns the sum of an initial segment. A complete balanced tree stores n = 2 ^ h entries in 2 n - 1 words. One fixed fourteen-register program dispatches both operations, with every executed instruction charged, including its final halt.

The representation is supplied at entry. Installing the three operation-argument registers is the external calling convention and is uncharged. Tree construction is a separate obligation; these theorems do not charge or claim a construction algorithm. Natural-number sums and increments must fit the chosen word width. This is a segment tree, not a Fenwick tree.

Main definitions

• spec: array operations and mathematical answers, with word-fit admissibility conditions.
• program: the fixed dispatcher and register-only calling convention.
• certificate: a semantic realization on the bounded-word machine.

Main results

• dispatch_spec: per-operation correctness and instruction estimate.
• instruction_bound: a separate cost certificate, at 13 (h + 1) + 12 instructions per call.

References

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

inductive Cslib.Algorithms.WordRAM.PrefixSums.Operation : Type

Array operations. Updates use a zero-based position; queries use a prefix length.

• add (position increment : ℕ) : Operation

  Add a nonnegative increment to one array entry.

• sum (length : ℕ) : Operation

  Return the sum of the given number of initial entries.

@[instance_reducible]

instance Cslib.Algorithms.WordRAM.PrefixSums.instDecidableEqOperation : DecidableEq Operation

def Cslib.Algorithms.WordRAM.PrefixSums.instDecidableEqOperation.decEq (x✝ x✝¹ : Operation) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Cslib.Algorithms.WordRAM.PrefixSums.instReprOperation : Repr Operation

def Cslib.Algorithms.WordRAM.PrefixSums.instReprOperation.repr : Operation → ℕ → Std.Format

def Cslib.Algorithms.WordRAM.PrefixSums.spec (h w : ℕ) : Stateful.Spec

Abstract list specification. The admissibility of an update includes the word bound on its new total; a query does not modify the array.

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

Initialize constants and traversal registers, charging all seven instructions.

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

One dispatcher for both operations, independent of size and word width.

def Cslib.Algorithms.WordRAM.PrefixSums.program (h w : ℕ) : WordRAM.DynamicProgram (spec h w) 14

Fixed code and external argument registers. Decoding reads only the answer register.

def Cslib.Algorithms.WordRAM.PrefixSums.setupData (x : WordRAM.Data 14) : WordRAM.Data 14

Mathematical description of charged register setup.

theorem Cslib.Algorithms.WordRAM.PrefixSums.setup_exec {w : ℕ} {x : WordRAM.Data 14} (hw : WordRAM.Fits w 2) : WordRAM.Exec w setup x (setupData x) 7

theorem Cslib.Algorithms.WordRAM.PrefixSums.setup_entry {x : WordRAM.Data 14} : Entry (x.regs Reg.root) (x.regs Reg.capacity) (x.regs Reg.position) (x.regs Reg.delta) (setupData x)

structure Cslib.Algorithms.WordRAM.PrefixSums.Rep (h b w : ℕ) (s : List ℕ) (x : WordRAM.Data 14) : Prop

A list is represented by a bounded tree, with persistent root and capacity registers.

• bounded : WordRAM.Data.Bounded w x
• root_eq : x.regs Reg.root = b
• capacity_eq : x.regs Reg.capacity = 2 ^ h
• tree : ∃ (t : Tree h), t.leaves = s ∧ t.Rep b x.mem

theorem Cslib.Algorithms.WordRAM.PrefixSums.Rep.length {h w b : ℕ} {x : WordRAM.Data 14} {s : List ℕ} (hx : Rep h b w s x) : s.length = 2 ^ h

The abstract array length is determined by the persistent tree representation.

theorem Cslib.Algorithms.WordRAM.PrefixSums.arguments_fit {h w b : ℕ} (ha : WordRAM.Fits w (b + 2 * 2 ^ h)) {s : List ℕ} (o : Operation) (ho : (spec h w).valid s o) (j : Fin 14) : WordRAM.Fits w ((program h w).encode o j)

theorem Cslib.Algorithms.WordRAM.PrefixSums.dispatch_spec {h w b : ℕ} {x : WordRAM.Data 14} (ha : WordRAM.Fits w (b + 2 * 2 ^ h)) {s : List ℕ} (o : Operation) (hx : Rep h b w s x) (ho : (spec h w).valid s o) : ∃ (y : WordRAM.Data 14), WordRAM.ExecWithin w dispatch ((program h w).prepare o x) y (13 * (h + 1) + 11) ∧ y.regs Reg.ans = ((spec h w).step s o).2 ∧ Rep h b w ((spec h w).step s o).1 y ∧ ∀ (a : ℕ), a < b ∨ b + Tree.words h ≤ a → y.mem a = x.mem a

Every operation uses the same dispatcher, restores the list representation and returns the specified result within 13 (h + 1) + 11 structured instructions. All memory outside the 2 * 2 ^ h - 1 words of the tree is preserved.

def Cslib.Algorithms.WordRAM.PrefixSums.certificate {h w b : ℕ} (ha : WordRAM.Fits w (b + 2 * 2 ^ h)) : WordRAM.DynamicCertificate (program h w) w

Semantic correctness and totality of the fixed bounded-word implementation.

theorem Cslib.Algorithms.WordRAM.PrefixSums.instruction_bound {h w b : ℕ} (ha : WordRAM.Fits w (b + 2 * 2 ^ h)) : Stateful.Bound (certificate ha).realization WordRAM.DynamicProgram.OperationTrace.instructions fun (x : (spec h w).State) (x_1 : (spec h w).Op) => 13 * (h + 1) + 12

Separate worst-case instruction certificate, counting the final halt.

theorem Cslib.Algorithms.WordRAM.PrefixSums.instruction_bound_log {h w b : ℕ} (ha : WordRAM.Fits w (b + 2 * 2 ^ h)) : Stateful.Bound (certificate ha).realization WordRAM.DynamicProgram.OperationTrace.instructions fun (s : (spec h w).State) (x : (spec h w).Op) => 13 * (Nat.log 2 (List.length s) + 1) + 12

The same instruction certificate stated in terms of the abstract array length.

theorem Cslib.Algorithms.WordRAM.PrefixSums.execOp_frame {h w b : ℕ} {x : WordRAM.Data 14} (ha : WordRAM.Fits w (b + 2 * 2 ^ h)) {s : List ℕ} {o : Operation} {y : WordRAM.Data 14} {a : ℕ} {trace : WordRAM.DynamicProgram.OperationTrace} (hx : Rep h b w s x) (ho : (spec h w).valid s o) (he : (program h w).ExecOp w x o a y trace) {j : ℕ} (hj : j < b ∨ b + Tree.words h ≤ j) : y.mem j = x.mem j

Every actual call preserves the complement of the fixed tree region. In particular, updates do not allocate storage depending on the number of previous operations.

theorem Cslib.Algorithms.WordRAM.PrefixSums.client_spec {h w b : ℕ} {x : WordRAM.Data 14} (ha : WordRAM.Fits w (b + 2 * 2 ^ h)) {α : Type} (p : (spec h w).Client α) {s : List ℕ} (hx : Rep h b w s x) (hv : (spec h w).ValidHistory s ((spec h w).runClient s p).2.2) : ∃ (y : WordRAM.Data 14) (traces : List WordRAM.DynamicProgram.OperationTrace), Stateful.Executes ((program h w).ExecOp w) p x ((spec h w).runClient s p).1 y traces ∧ Rep h b w ((spec h w).runClient s p).2.1 y ∧ Stateful.total WordRAM.DynamicProgram.OperationTrace.instructions traces ≤ ((spec h w).runClient s p).2.2.length * (13 * (h + 1) + 12)

Every admissible adaptive client has a concrete execution with the specified result and final array, and at most 13 (h + 1) + 12 instructions for each selected operation. The client controller itself is mathematical; this counts its calls into the fixed machine program.

def Cslib.Algorithms.WordRAM.PrefixSums.zeroData (h b : ℕ) : WordRAM.Data 14

Concrete zero memory and persistent metadata. Supplying this state is not a charged initialization algorithm.

theorem Cslib.Algorithms.WordRAM.PrefixSums.rep_zeroData {h w b : ℕ} (ha : WordRAM.Fits w (b + 2 * 2 ^ h)) : Rep h b w (Tree.zero h).leaves (zeroData h b)

The representation assumptions are inhabited at every fitting size and root pointer.