Doubling arrays on the word RAM

A fixed twelve-register append routine uses the charged zeroing allocator and a charged copy loop. Old blocks are retained: the space theorem concerns total allocated words over append-only histories, rather than reclamation. The abstract state exposes only the list. A companion two-instruction indexed read routine and a fixed operation dispatcher connect the doubling array to Cslib.Stateful and Cslib.Stateful.Amortized.

Main definitions

• Cslib.Algorithms.WordRAM.DynamicArray.program: the fixed twelve-register append procedure.
• Cslib.Algorithms.WordRAM.DynamicArray.getProgram: the two-instruction indexed read procedure.
• Cslib.Algorithms.WordRAM.DynamicArray.initProgram: charged fifteen-instruction initializer.
• Cslib.Algorithms.WordRAM.DynamicArray.dispatch: fixed append/get operation dispatcher.
• Cslib.Algorithms.WordRAM.DynamicArray.Rep: the live array and allocator frontier invariant.
• Cslib.Algorithms.WordRAM.DynamicArray.potential: natural-valued credit 15 * (2 * |vs| - cap).

Main results

• Cslib.Algorithms.WordRAM.DynamicArray.Rep.space: total allocated words < 4 * vs.length for nonempty arrays.
• Cslib.Algorithms.WordRAM.DynamicArray.grow_exec: capacity doubling within 15 * cap + 14 instructions.
• Cslib.Algorithms.WordRAM.DynamicArray.append_exec: append correctness, memory preservation, and the 49-instruction potential inequality.
• Cslib.Algorithms.WordRAM.DynamicArray.get_exec: two-instruction indexed read correctness.
• Cslib.Algorithms.WordRAM.DynamicArray.init_exec: charged initialization of the empty array.
• Cslib.Algorithms.WordRAM.DynamicArray.amortized: Stateful.Amortized certificate for adaptive histories.
• Cslib.Algorithms.WordRAM.DynamicArray.run_initialized: end-to-end adaptive execution from charged initialization with linear total instruction bound and < 4 * m space.
• Cslib.Algorithms.WordRAM.DynamicArray.run_appendAll: appending m words from an initialized empty array in at most 15 + 52 * m total instructions and < 4 * m total allocated words.

References

• Cormen, Leiserson, Rivest and Stein, Introduction to Algorithms, Chapter 17.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.DynamicArray.ptr : Fin 12

Pointer to the live block.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.DynamicArray.dest : Fin 12

New block pointer and operation dispatch tag.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.DynamicArray.len : Fin 12

Logical length.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.DynamicArray.idx : Fin 12

Copy/allocation loop cursor.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.DynamicArray.addr : Fin 12

Temporary address.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.DynamicArray.temp : Fin 12

Temporary copied value and read output register.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.DynamicArray.one : Fin 12

Constant one.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.DynamicArray.cap : Fin 12

Current capacity.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.DynamicArray.frontier : Fin 12

Bump allocator frontier.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.DynamicArray.arg : Fin 12

Caller-supplied value to append or index to read.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.DynamicArray.count : Fin 12

Requested allocation size.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.DynamicArray.zero : Fin 12

Constant zero.

def Cslib.Algorithms.WordRAM.DynamicArray.copy : WordRAM.Code WordRAM.Basis.standard 12

The copy routine embedded in the first seven registers.

def Cslib.Algorithms.WordRAM.DynamicArray.grow : WordRAM.Code WordRAM.Basis.standard 12

Allocate twice the capacity, copy the live prefix, and switch the pointer.

def Cslib.Algorithms.WordRAM.DynamicArray.program : WordRAM.Code WordRAM.Basis.standard 12

Append a word, growing precisely when the array is full.

def Cslib.Algorithms.WordRAM.DynamicArray.getProgram : WordRAM.Code WordRAM.Basis.standard 12

Read the word at the index in arg into temp.

def Cslib.Algorithms.WordRAM.DynamicArray.initProgram : WordRAM.Code WordRAM.Basis.standard 12

Allocate the initial one-word block at address zero and install the empty representation.

structure Cslib.Algorithms.WordRAM.DynamicArray.Rep (vs : List ℕ) (x : WordRAM.Data 12) : Prop

The live prefix, capacity and total allocation. The equalities express the geometric allocation series starting with a single cell at address zero.

• length_eq : x.regs len = vs.length
• capacity_pos : 0 < x.regs cap
• length_le : vs.length ≤ x.regs cap
• capacity_le : x.regs cap ≤ max 1 (2 * vs.length)
• pointer_eq : x.regs ptr + 1 = x.regs cap
• frontier_eq : x.regs frontier + 1 = 2 * x.regs cap
• contents (i : Fin vs.length) : x.mem (x.regs ptr + ↑i) = vs[i]

theorem Cslib.Algorithms.WordRAM.DynamicArray.Rep.space {vs : List ℕ} {x : WordRAM.Data 12} (h : Rep vs x) (hne : vs ≠ []) : x.regs frontier < 4 * vs.length

Capacity and all historically allocated blocks occupy fewer than four words per live element once the array is nonempty.

theorem Cslib.Algorithms.WordRAM.DynamicArray.Rep.frontier_add_two_cap_le {vs : List ℕ} {x : WordRAM.Data 12} (h : Rep vs x) : x.regs frontier + 2 * x.regs cap ≤ 8 * vs.length + 3

The doubled frontier bound x.regs frontier + 2 * x.regs cap is bounded by 8 * vs.length + 3 for every represented state.

def Cslib.Algorithms.WordRAM.DynamicArray.potential (vs : List ℕ) (x : WordRAM.Data 12) : ℕ

The natural-valued credit used to pay for allocation and copying.

theorem Cslib.Algorithms.WordRAM.DynamicArray.copy_exec {w : ℕ} (x : WordRAM.Data 12) (h1 : WordRAM.Fits w 1) (hs : WordRAM.Fits w (x.regs ptr + x.regs len)) (hd : WordRAM.Fits w (x.regs dest + x.regs len)) (hdisj : x.regs ptr + x.regs len ≤ x.regs dest) : ∃ (y : WordRAM.Data 12), WordRAM.ExecWithin w copy x y (7 * x.regs len + 4) ∧ y.mem = WordRAM.ArrayCopy.copyPrefix x.mem (x.regs ptr) (x.regs dest) (x.regs len)

The exact copy contract lifts to a larger register file without charging a meta-level call.

theorem Cslib.Algorithms.WordRAM.DynamicArray.grow_exec {w : ℕ} (x : WordRAM.Data 12) (h1 : WordRAM.Fits w 1) (hn : x.regs len = x.regs cap) (hp : x.regs ptr + x.regs len ≤ x.regs frontier) (hw : WordRAM.Fits w (x.regs frontier + 2 * x.regs cap)) : ∃ (y : WordRAM.Data 12), WordRAM.ExecWithin w grow x y (15 * x.regs cap + 14) ∧ y.regs ptr = x.regs frontier ∧ y.regs cap = 2 * x.regs cap ∧ y.regs frontier = x.regs frontier + 2 * x.regs cap ∧ (∀ i < x.regs len, y.mem (y.regs ptr + i) = x.mem (x.regs ptr + i)) ∧ ∀ (a : ℕ), a < x.regs frontier ∨ x.regs frontier + 2 * x.regs cap ≤ a → y.mem a = x.mem a

A growth phase preserves the live values and sets aside a zeroed block, charging both allocation and copying. The resulting capacity, frontier, and frame are explicit.

theorem Cslib.Algorithms.WordRAM.DynamicArray.appendTail_exec {w : ℕ} (z : WordRAM.Data 12) (h1 : WordRAM.Fits w 1) (haddr : WordRAM.Fits w (z.regs ptr + z.regs len)) (hlen : WordRAM.Fits w (z.regs len + 1)) : have y := (((z.set one 1).set addr (z.regs ptr + z.regs len)).write (z.regs ptr + z.regs len) (z.regs arg)).set len (z.regs len + 1); WordRAM.Exec w ((WordRAM.Code.op (WordRAM.Op.const one 1)).seq ((WordRAM.writeAt addr ptr len arg).seq (WordRAM.Code.op (WordRAM.Op.bin WordRAM.BinOp.add len len one)))) z y 4

Four-instruction suffix of program: set one ← #1, write arg at ptr + len, and increment len.

theorem Cslib.Algorithms.WordRAM.DynamicArray.append_exec {w : ℕ} {vs : List ℕ} {x : WordRAM.Data 12} (hr : Rep vs x) (hw : WordRAM.Fits w (x.regs frontier + 2 * x.regs cap)) : ∃ (y : WordRAM.Data 12) (n : ℕ), WordRAM.Exec w program x y n ∧ Rep (vs ++ [x.regs arg]) y ∧ (∀ (a : ℕ), a < x.regs ptr ∨ y.regs frontier ≤ a → y.mem a = x.mem a) ∧ n + potential (vs ++ [x.regs arg]) y ≤ 49 + potential vs x ∧ n + potential (vs ++ [x.regs arg]) y - potential vs x ≤ 49

Appending a word preserves the doubling-array invariant, modifies only cells in [x.regs ptr, y.regs frontier) (hence only within [0, y.regs frontier)), and satisfies the potential-method amortized bound with constant 49.

theorem Cslib.Algorithms.WordRAM.DynamicArray.get_exec {w : ℕ} {vs : List ℕ} {x : WordRAM.Data 12} (hr : Rep vs x) (hi : x.regs arg < vs.length) (hw : WordRAM.Fits w (x.regs frontier)) : ∃ (y : WordRAM.Data 12), WordRAM.Exec w getProgram x y 2 ∧ y.regs temp = vs.getD (x.regs arg) 0 ∧ Rep vs y ∧ y.mem = x.mem ∧ potential vs y = potential vs x

Indexed read returns vs[x.regs arg] in temp in two instructions without changing the representation, memory, or potential.

theorem Cslib.Algorithms.WordRAM.DynamicArray.init_exec {w : ℕ} (x : WordRAM.Data 12) (h1 : WordRAM.Fits w 1) : ∃ (y : WordRAM.Data 12), WordRAM.Exec w initProgram x y 15 ∧ Rep [] y ∧ y.regs frontier = 1 ∧ potential [] y = 0 ∧ y.mem 0 = 0 ∧ ∀ (a : ℕ), 1 ≤ a → y.mem a = x.mem a

Charged initialization allocates the initial one-word block at address zero in fifteen instructions, establishing Rep [] with zero potential and frontier 1.

Connection to Cslib.Stateful and Cslib.Stateful.Amortized

inductive Cslib.Algorithms.WordRAM.DynamicArray.Op : Type

Doubling-array operations: append a word at the end or read an existing index.

• append (value : ℕ) : Op

  Append a word to the array.

• get (index : ℕ) : Op

  Read the word at a zero-based index.

@[instance_reducible]

instance Cslib.Algorithms.WordRAM.DynamicArray.instDecidableEqOp : DecidableEq Op

def Cslib.Algorithms.WordRAM.DynamicArray.instDecidableEqOp.decEq (x✝ x✝¹ : Op) : Decidable (x✝ = x✝¹)

def Cslib.Algorithms.WordRAM.DynamicArray.instReprOp.repr : Op → ℕ → Std.Format

@[instance_reducible]

instance Cslib.Algorithms.WordRAM.DynamicArray.instReprOp : Repr Op

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.DynamicArray.spec (w : ℕ) : Stateful.Spec

Mathematical specification of a bounded-word dynamic array. Appending requires the value and the worst-case doubled frontier bound 8 * vs.length + 4 to fit in a machine word; indexed reads require a valid index fitting a machine word.

def Cslib.Algorithms.WordRAM.DynamicArray.dispatch : WordRAM.Code WordRAM.Basis.standard 12

Fixed operation dispatcher: dest = 0 runs program (append), dest = 1 runs getProgram.

def Cslib.Algorithms.WordRAM.DynamicArray.implementation (w : ℕ) : WordRAM.DynamicProgram (spec w) 12

Register calling convention for dispatch.

structure Cslib.Algorithms.WordRAM.DynamicArray.BoundedRep (w : ℕ) (vs : List ℕ) (x : WordRAM.Data 12) : Prop

Bounded-word doubling-array representation for DynamicCertificate.

• bounded : WordRAM.Data.Bounded w x
• rep : Rep vs x

def Cslib.Algorithms.WordRAM.DynamicArray.charge : Op → ℕ

Amortized instruction charge per operation, including dispatch and final halt.

theorem Cslib.Algorithms.WordRAM.DynamicArray.arguments_fit {w : ℕ} (h1 : WordRAM.Fits w 1) {vs : List ℕ} (o : Op) (hv : (spec w).valid vs o) (i : Fin 12) : WordRAM.Fits w ((implementation w).encode o i)

Encoded arguments fit the word width whenever 1 fits and the operation is valid.

theorem Cslib.Algorithms.WordRAM.DynamicArray.prepare_rep {vs : List ℕ} {x : WordRAM.Data 12} (hr : Rep vs x) (w : ℕ) (o : Op) : Rep vs ((implementation w).prepare o x)

Argument delivery preserves Rep because dest and arg are not persistent representation registers.

theorem Cslib.Algorithms.WordRAM.DynamicArray.dispatch_exec {w : ℕ} (h1 : WordRAM.Fits w 1) {vs : List ℕ} {x : WordRAM.Data 12} (hr : BoundedRep w vs x) (o : Op) (hv : (spec w).valid vs o) : ∃ (y : WordRAM.Data 12) (n : ℕ), WordRAM.Exec w dispatch ((implementation w).prepare o x) y n ∧ (implementation w).decode o y.regs = some ((spec w).step vs o).2 ∧ BoundedRep w ((spec w).step vs o).1 y ∧ (∀ (a : ℕ), y.regs frontier ≤ a → y.mem a = x.mem a) ∧ n + 1 + potential ((spec w).step vs o).1 y ≤ charge o + potential vs x

Every admissible operation executes dispatch, preserves BoundedRep, modifies only cells below y.regs frontier, and satisfies the potential inequality with charge o (counting the final halt).

def Cslib.Algorithms.WordRAM.DynamicArray.certificate {w : ℕ} (h1 : WordRAM.Fits w 1) : WordRAM.DynamicCertificate (implementation w) w

Semantic realization certificate for the bounded-word dynamic array.

theorem Cslib.Algorithms.WordRAM.DynamicArray.amortized {w : ℕ} (h1 : WordRAM.Fits w 1) : Stateful.Amortized (certificate h1).realization WordRAM.DynamicProgram.OperationTrace.instructions potential fun (x : (spec w).State) (o : (spec w).Op) => charge o

Amortized instruction-cost certificate for the dynamic array (52 per append, 6 per get, including dispatch and final halt).

theorem Cslib.Algorithms.WordRAM.DynamicArray.amortized_uniform {w : ℕ} (h1 : WordRAM.Fits w 1) : Stateful.Amortized (certificate h1).realization WordRAM.DynamicProgram.OperationTrace.instructions potential fun (x : (spec w).State) (x_1 : (spec w).Op) => 52

Uniform amortized instruction-cost certificate (52 instructions per operation).

theorem Cslib.Algorithms.WordRAM.DynamicArray.modifies {w : ℕ} (h1 : WordRAM.Fits w 1) {vs : List ℕ} {x y : WordRAM.Data 12} {o : Op} {a : (spec w).Result o} {trace : WordRAM.DynamicProgram.OperationTrace} (hr : BoundedRep w vs x) (hv : (spec w).valid vs o) (he : (implementation w).ExecOp w x o a y trace) : WordRAM.Modifies (Finset.range (y.regs frontier)) x.mem y.mem

Every concrete call modifies only cells below y.regs frontier.

theorem Cslib.Algorithms.WordRAM.DynamicArray.frame {w : ℕ} (h1 : WordRAM.Fits w 1) {vs : List ℕ} {x y : WordRAM.Data 12} {o : Op} {a : (spec w).Result o} {trace : WordRAM.DynamicProgram.OperationTrace} (hr : BoundedRep w vs x) (hv : (spec w).valid vs o) (he : (implementation w).ExecOp w x o a y trace) {Q : WordRAM.HeapAssertion} (hQ : Q.holds x.mem) (hd : Disjoint Q.footprint (Finset.range (y.regs frontier))) : Q.holds y.mem

Disjoint heap assertions above y.regs frontier survive every dynamic-array call.

theorem Cslib.Algorithms.WordRAM.DynamicArray.run_client {w : ℕ} (h1 : WordRAM.Fits w 1) {α : Type} (p : (spec w).Client α) {vs : List ℕ} {x : WordRAM.Data 12} (hr : BoundedRep w vs x) (hv : (spec w).ValidHistory vs ((spec w).runClient vs p).2.2) : ∃ (y : WordRAM.Data 12) (traces : List WordRAM.DynamicProgram.OperationTrace), Stateful.Executes ((implementation w).ExecOp w) p x ((spec w).runClient vs p).1 y traces ∧ BoundedRep w ((spec w).runClient vs p).2.1 y ∧ Stateful.total WordRAM.DynamicProgram.OperationTrace.instructions traces + potential ((spec w).runClient vs p).2.1 y ≤ ((spec w).runClient vs p).2.2.length * 52 + potential vs x ∧ (((spec w).runClient vs p).2.1 ≠ [] → y.regs frontier < 4 * List.length ((spec w).runClient vs p).2.1)

Every admissible adaptive client executes with total instructions bounded by 52 per operation plus initial credit, retaining final credit and the < 4 * m space invariant.

theorem Cslib.Algorithms.WordRAM.DynamicArray.run_initialized {w : ℕ} (h1 : WordRAM.Fits w 1) {α : Type} (p : (spec w).Client α) {x : WordRAM.Data 12} (hx : WordRAM.Data.Bounded w x) (hv : (spec w).ValidHistory [] ((spec w).runClient [] p).2.2) : ∃ (ready : WordRAM.Data 12) (y : WordRAM.Data 12) (traces : List WordRAM.DynamicProgram.OperationTrace), WordRAM.Exec w initProgram x ready 15 ∧ Stateful.Executes ((implementation w).ExecOp w) p ready ((spec w).runClient [] p).1 y traces ∧ BoundedRep w ((spec w).runClient [] p).2.1 y ∧ 15 + Stateful.total WordRAM.DynamicProgram.OperationTrace.instructions traces + potential ((spec w).runClient [] p).2.1 y ≤ 15 + ((spec w).runClient [] p).2.2.length * 52 ∧ (((spec w).runClient [] p).2.1 ≠ [] → y.regs frontier < 4 * List.length ((spec w).runClient [] p).2.1)

Starting from arbitrary bounded machine data, run initProgram (15 instructions) followed by any admissible adaptive client p. Total instructions across initialization and m operations are at most 15 + 52 * m, and the allocator frontier is < 4 * n whenever the final list of length n is nonempty.

def Cslib.Algorithms.WordRAM.DynamicArray.appendAll {w : ℕ} : List ℕ → (spec w).Client Unit

Client that appends each element of us in order.

@[simp]

theorem Cslib.Algorithms.WordRAM.DynamicArray.runClient_appendAll (w : ℕ) (vs us : List ℕ) : (spec w).runClient vs (appendAll us) = ((), vs ++ us, List.map Op.append us)

Mathematical execution of appendAll appends us to vs and records us.map Op.append.

theorem Cslib.Algorithms.WordRAM.DynamicArray.validHistory_appendAll {w : ℕ} {vs us : List ℕ} (hvals : ∀ v ∈ us, WordRAM.Fits w v) (hlen : WordRAM.Fits w (8 * (vs.length + us.length) + 4)) : (spec w).ValidHistory vs ((spec w).runClient vs (appendAll us)).2.2

appendAll us is admissible from vs whenever every element of us fits w and 8 * (vs.length + us.length) + 4 fits w.

theorem Cslib.Algorithms.WordRAM.DynamicArray.run_appendAll {w : ℕ} (h1 : WordRAM.Fits w 1) {vs : List ℕ} {x : WordRAM.Data 12} (hx : WordRAM.Data.Bounded w x) (hvals : ∀ v ∈ vs, WordRAM.Fits w v) (hlen : WordRAM.Fits w (8 * vs.length + 4)) : ∃ (ready : WordRAM.Data 12) (y : WordRAM.Data 12) (traces : List WordRAM.DynamicProgram.OperationTrace), WordRAM.Exec w initProgram x ready 15 ∧ Stateful.Executes ((implementation w).ExecOp w) (appendAll vs) ready () y traces ∧ BoundedRep w vs y ∧ 15 + Stateful.total WordRAM.DynamicProgram.OperationTrace.instructions traces + potential vs y ≤ 15 + vs.length * 52 ∧ (vs ≠ [] → y.regs frontier < 4 * vs.length)

Any sequence of m = vs.length appends starting from the charged initializer executes in at most 15 + 52 * m total charged instructions and uses fewer than 4 * m total allocated words whenever vs ≠ [].