Bounded memory-client loops

Bounded iteration remains an ordinary Memory.Prog term. The local-work currency counts body work and every iteration, including iterations issuing no memory query. The native realization uses one fixed body emitter and static registers for the mutable state and countdown counter.

Main definitions

• iterate: bounded iteration in the existing memory-client monad.
• iterationWork, iterationSafe: local work and domains along the actual semantic states.
• loopEmit, loopBody: the native loop with a fixed body emitter, and one native iteration, over the register bank stateSlot, counterSlot, zeroSlot, oneSlot, bodySlot.

Main results

• iterationSum_eq: the native grading rule's semantic sum is memory charge plus local work.
• loopEmit_entry, loopBody_tail: the native loop's entry prologue and the control tail of one iteration, shared by the deterministic and randomized loop realizations.
• bodyBank_layout, bodySlot_injective, stateSlot_ne_bodySlot, regs_comp_append_eq_appendWords, loopEmit_not_readsWidth: the body bank's register premises, the state words read back as appended words, and width-freedom of the loop.
• iterationWork_zero: evaluate local work when the body has no local-work charge.
• Realizes.Witness.loopEmit_spec: the loop emitter with additive per-iteration overhead.
• Realizes.Witness.iterateRuntime, Realizes.iterateRuntime: one uniform body witness or certificate realizes a runtime-bounded loop.

The iteration grading and realization are original infrastructure over the existing free monad and structured Word-RAM code. No additional program syntax or memory model is introduced. Fixed-environment transport laws are provided by the LoopCongr module.

def Cslib.WordRAM.Realization.iterate {δ σ : Type} (body : δ × σ → DataStructure.Memory.Prog σ) (d : δ) : ℕ → σ → DataStructure.Memory.Prog σ

Execute one fixed body family a runtime-bounded number of times.

def Cslib.WordRAM.Realization.iterationWork {δ σ : Type} (body : δ × σ → DataStructure.Memory.Prog σ) (work : δ × σ → DataStructure.Memory.State → ℕ) (d : δ) : ℕ → σ → DataStructure.Memory.State → ℕ

Local computation and one control-work unit per iteration, along actual semantic states.

@[simp]

theorem Cslib.WordRAM.Realization.iterationWork_zero {δ σ : Type} (body : δ × σ → DataStructure.Memory.Prog σ) (d : δ) (n : ℕ) (a : σ) (s : DataStructure.Memory.State) : iterationWork body (fun (x : δ × σ) (x_1 : DataStructure.Memory.State) => 0) d n a s = n

With no body-local work, the local grade is exactly one control unit per iteration.

def Cslib.WordRAM.Realization.iterationSafe {δ σ : Type} (body : δ × σ → DataStructure.Memory.Prog σ) (safe : ℕ → δ × σ → DataStructure.Memory.State → Prop) (w : ℕ) (d : δ) : ℕ → σ → DataStructure.Memory.State → Prop

Every executed body must satisfy its explicit domain at the reached state.

theorem Cslib.WordRAM.Realization.iteration_charge_succ {δ σ : Type} (body : δ × σ → DataStructure.Memory.Prog σ) (work : δ × σ → DataStructure.Memory.State → ℕ) (d : δ) (n : ℕ) (a : σ) (s : DataStructure.Memory.State) : memoryCost (iterate body d (n + 1) a) s + iterationWork body work d (n + 1) a s = memoryCost (body (d, a)) s + work (d, a) s + (memoryCost (iterate body d n ((DataStructure.Memory.spec 0).clientResult s (body (d, a)))) ((DataStructure.Memory.spec 0).clientState s (body (d, a))) + iterationWork body work d n ((DataStructure.Memory.spec 0).clientResult s (body (d, a))) ((DataStructure.Memory.spec 0).clientState s (body (d, a)))) + 1

Memory cost and certified local work decompose at each actual iteration.

def Cslib.WordRAM.Realization.iterationStep {δ σ : Type} (body : δ × σ → DataStructure.Memory.Prog σ) (d : δ) (a : σ × DataStructure.Memory.State) : σ × DataStructure.Memory.State

One semantic iteration updates both the mutable value and the complete memory state.

theorem Cslib.WordRAM.Realization.iterate_result_state {δ σ : Type} (body : δ × σ → DataStructure.Memory.Prog σ) (d : δ) (n : ℕ) (a : σ) (s : DataStructure.Memory.State) : ((DataStructure.Memory.spec 0).clientResult s (iterate body d n a), (DataStructure.Memory.spec 0).clientState s (iterate body d n a)) = (iterationStep body d)^[n] (a, s)

The interpreter follows precisely the bounded semantic transition, not an arbitrary state.

theorem Cslib.WordRAM.Realization.iterationSum_eq {δ σ : Type} (body : δ × σ → DataStructure.Memory.Prog σ) (work : δ × σ → DataStructure.Memory.State → ℕ) (d : δ) (n : ℕ) (a : σ) (s : DataStructure.Memory.State) : iterationSum (iterationStep body d) (fun (q : σ × DataStructure.Memory.State) => memoryCost (body (d, q.1)) q.2 + work (d, q.1) q.2) n (a, s) + n = memoryCost (iterate body d n a) s + iterationWork body work d n a s

The native grading rule's semantic sum is exactly memory charge plus local iteration work.

def Cslib.WordRAM.Realization.stateSlot {l n : ℕ} (i : Fin l) : Fin (l + (l + n + 3) + 1)

The loop's state words, which are also its result slots.

def Cslib.WordRAM.Realization.counterSlot (l n : ℕ) : Fin (l + (l + n + 3) + 1)

The loop's countdown register.

def Cslib.WordRAM.Realization.zeroSlot (l n : ℕ) : Fin (l + (l + n + 3) + 1)

A register holding zero, for the loop test.

def Cslib.WordRAM.Realization.oneSlot (l n : ℕ) : Fin (l + (l + n + 3) + 1)

A register holding one, for the countdown.

def Cslib.WordRAM.Realization.bodySlot {l n : ℕ} (i : Fin (l + n + 1)) : Fin (l + (l + n + 3) + 1)

The body's scratch bank inside the loop's bank.

def Cslib.WordRAM.Realization.loopBody {r k l n : ℕ} (emit : {r : ℕ} → Fin r → (Fin (k + l) → Fin r) → (Fin (l + n + 1) → Fin r) → Code Basis.exact r) (frontier : Fin r) (src : Fin (k + l + 1) → Fin r) (tmp : Fin (l + (l + n + 3) + 1) → Fin r) : Code Basis.exact r

One native iteration: run the body on the environment and state words, copy its result into the state words and count down.

def Cslib.WordRAM.Realization.loopEmit {r k l n : ℕ} (emit : {r : ℕ} → Fin r → (Fin (k + l) → Fin r) → (Fin (l + n + 1) → Fin r) → Code Basis.exact r) (frontier : Fin r) (src : Fin (k + l + 1) → Fin r) (tmp : Fin (l + (l + n + 3) + 1) → Fin r) : Code Basis.exact r

The native loop: install the state words and the counter, then iterate loopBody while the counter is positive.

theorem Cslib.WordRAM.Realization.regs_comp_append_eq_appendWords {δ σ : Type} {r k l : ℕ} (input : δ ↪ Fin k → ℕ) (output : σ ↪ Fin l → ℕ) {x : Data r} {env : Fin k → Fin r} {st : Fin l → Fin r} {d : δ} {a : σ} (henv : ∀ (i : Fin k), x.regs (env i) = input d i) (hst : ∀ (i : Fin l), x.regs (st i) = output a i) : x.regs ∘ Fin.append env st = (appendWords input output) (d, a)

Registers holding the environment words followed by the state words read back the appended words.

theorem Cslib.WordRAM.Realization.bodyBank_layout {r k l m p : ℕ} {frontier : Fin r} {env : Fin k → Fin r} {tmp : Fin m → Fin r} {stS : Fin l → Fin m} {btS : Fin p → Fin m} (hi : Function.Injective tmp) (hbt : Function.Injective btS) (hsb : ∀ (i : Fin l) (j : Fin p), stS i ≠ btS j) (hd : ∀ (i : Fin k) (j : Fin m), env i ≠ tmp j) (hf : ∀ (j : Fin m), tmp j ≠ frontier) (hs : ∀ (i : Fin k), env i ≠ frontier) : (Function.Injective fun (j : Fin p) => tmp (btS j)) ∧ (∀ (i : Fin (k + l)) (j : Fin p), Fin.append env (fun (i : Fin l) => tmp (stS i)) i ≠ tmp (btS j)) ∧ (∀ (j : Fin p), tmp (btS j) ≠ frontier) ∧ ∀ (i : Fin (k + l)), Fin.append env (fun (i : Fin l) => tmp (stS i)) i ≠ frontier

A body bank tmp ∘ btS inside an injective scratch bank tmp meets the register hypotheses of the body's certificate, which reads the environment env and the state words tmp ∘ stS.

theorem Cslib.WordRAM.Realization.loopEmit_not_readsWidth {r k l n : ℕ} (emit : {r : ℕ} → Fin r → (Fin (k + l) → Fin r) → (Fin (l + n + 1) → Fin r) → Code Basis.exact r) {frontier : Fin r} {src : Fin (k + l + 1) → Fin r} {tmp : Fin (l + (l + n + 3) + 1) → Fin r} (hnw : ¬(emit frontier (Fin.append (fun (i : Fin k) => src ⟨↑i, ⋯⟩) fun (i : Fin l) => tmp (stateSlot i)) fun (i : Fin (l + n + 1)) => tmp (bodySlot i)).ReadsWidth) : ¬(loopEmit (fun {r : ℕ} => emit) frontier src tmp).ReadsWidth

The native loop reads the word width only where its body does.

theorem Cslib.WordRAM.Realization.bodySlot_injective {l n : ℕ} : Function.Injective bodySlot

The loop's body bank does not repeat a register.

theorem Cslib.WordRAM.Realization.stateSlot_ne_bodySlot {l n : ℕ} (i : Fin l) (j : Fin (l + n + 1)) : stateSlot i ≠ bodySlot j

The loop's state words lie outside its body bank.

theorem Cslib.WordRAM.Realization.loopEmit_entry {δ σ : Type} {r k l : ℕ} (input : δ ↪ Fin k → ℕ) (output : σ ↪ Fin l → ℕ) {n : ℕ} {frontier : Fin r} {src : Fin (k + l + 1) → Fin r} {tmp : Fin (l + (l + n + 3) + 1) → Fin r} (hi : Function.Injective tmp) (hd : ∀ (i : Fin (k + l + 1)) (j : Fin (l + (l + n + 3) + 1)), src i ≠ tmp j) (hf : ∀ (j : Fin (l + (l + n + 3) + 1)), tmp j ≠ frontier) {w : ℕ} {x : Data r} {d : δ} {a : σ} {fuel : ℕ} (hx : Data.Bounded w x) (hin : x.regs ∘ src = (((appendWords input output).prodMap (Equiv.funUnique (Fin 1) ℕ).symm.toEmbedding).trans (Fin.appendEquiv (k + l) 1).toEmbedding) ((d, a), fuel)) : ∃ (x₁ : Data r) (x₂ : Data r) (z : Data r), ExecWithin w (copyBank (fun (i : Fin l) => src ⟨k + ↑i, ⋯⟩) (fun (i : Fin l) => tmp (stateSlot i)) (tmp (zeroSlot l n))) x x₁ (l + 1) ∧ ExecWithin w (Code.op (Op.copy (tmp (counterSlot l n)) (src ⟨k + l, ⋯⟩))) x₁ x₂ 1 ∧ ExecWithin w (Code.op (Op.const (tmp (zeroSlot l n)) 0)) x₂ z 1 ∧ Data.Bounded w z ∧ memoryState frontier z = memoryState frontier x ∧ (∀ (i : Fin k), z.regs (src ⟨↑i, ⋯⟩) = input d i) ∧ (∀ (i : Fin l), z.regs (tmp (stateSlot i)) = output a i) ∧ z.regs (tmp (counterSlot l n)) = fuel ∧ z.regs (tmp (zeroSlot l n)) = 0 ∧ ∀ (i : Fin r), i ≠ frontier → (∀ (j : Fin (l + (l + n + 3) + 1)), tmp j ≠ i) → z.regs i = x.regs i

Entering the native loop of loopEmit: copy the state words into the bank, install the counter and clear the zero register. Memory, the frontier and every register outside the scratch bank are unchanged.

theorem Cslib.WordRAM.Realization.loopBody_tail {r l n : ℕ} (frontier : Fin r) (tmp : Fin (l + (l + n + 3) + 1) → Fin r) (hi : Function.Injective tmp) (hf : ∀ (j : Fin (l + (l + n + 3) + 1)), tmp j ≠ frontier) (w j : ℕ) {y u : Data r} (hub : Data.Bounded w u) (hyc : y.regs (tmp (counterSlot l n)) = j + 1) (huf : ∀ (i : Fin r), i ≠ frontier → (∀ (b : Fin (l + n + 1)), tmp (bodySlot b) ≠ i) → u.regs i = y.regs i) : ∃ (y' : Data r), ExecWithin w ((copyBank (fun (i : Fin l) => tmp (bodySlot (Fin.castAdd (n + 1) i))) (fun (i : Fin l) => tmp (stateSlot i)) (tmp (zeroSlot l n))).seq ((Code.op (Op.const (tmp (oneSlot l n)) 1)).seq (Code.op (Op.exactBin BinOp.sub (tmp (counterSlot l n)) (tmp (counterSlot l n)) (tmp (oneSlot l n)))))) u y' (l + 3) ∧ memoryState frontier y' = memoryState frontier u ∧ (∀ (i : Fin l), y'.regs (tmp (stateSlot i)) = u.regs (tmp (bodySlot (Fin.castAdd (n + 1) i)))) ∧ y'.regs (tmp (counterSlot l n)) = j ∧ y'.regs (tmp (zeroSlot l n)) = y.regs (tmp (zeroSlot l n)) ∧ ∀ (i : Fin r), i ≠ frontier → (∀ (b : Fin (l + (l + n + 3) + 1)), tmp b ≠ i) → y'.regs i = y.regs i

The control tail of one iteration of loopBody, after the body ran from y to u: copy the body's result words into the state words and count down. Memory, the frontier, the zero register and every register outside the scratch bank keep their values.

theorem Cslib.WordRAM.Realization.Realizes.Witness.loopEmit_spec {δ σ : Type} {k l : ℕ} (input : δ ↪ Fin k → ℕ) (output : σ ↪ Fin l → ℕ) {body : δ × σ → DataStructure.Memory.Prog σ} {safe : ℕ → δ × σ → DataStructure.Memory.State → Prop} {work : δ × σ → DataStructure.Memory.State → ℕ} (h : Witness Basis.exact body (appendWords input output) output safe work) {r : ℕ} (frontier : Fin r) (src : Fin (k + l + 1) → Fin r) (tmp : Fin (l + (l + h.scratchSize + 3) + 1) → Fin r) : Function.Injective tmp → (∀ (i : Fin (k + l + 1)) (j : Fin (l + (l + h.scratchSize + 3) + 1)), src i ≠ tmp j) → (∀ (j : Fin (l + (l + h.scratchSize + 3) + 1)), tmp j ≠ frontier) → (∀ (i : Fin (k + l + 1)), src i ≠ frontier) → ¬(loopEmit (fun {r : ℕ} => h.code) frontier src tmp).ReadsWidth ∧ ∀ (w : ℕ) (d : (δ × σ) × ℕ) (x : Data r), Data.Bounded w x → x.regs ∘ src = (((appendWords input output).prodMap (Equiv.funUnique (Fin 1) ℕ).symm.toEmbedding).trans (Fin.appendEquiv (k + l) 1).toEmbedding) d → iterationSafe body safe w d.1.1 d.2 d.1.2 (memoryState frontier x) → (DataStructure.Memory.spec w).ValidHistory (memoryState frontier x) ((DataStructure.Memory.spec w).clientHistory (memoryState frontier x) (iterate body d.1.1 d.2 d.1.2)) → ∃ (y : Data r), ExecWithin w (loopEmit (fun {r : ℕ} => h.code) frontier src tmp) x y (h.factor * (memoryCost (iterate body d.1.1 d.2 d.1.2) (memoryState frontier x) + iterationWork body work d.1.1 d.2 d.1.2 (memoryState frontier x)) + (l + 5) * (d.2 + 1)) ∧ memoryState frontier y = (DataStructure.Memory.spec w).clientState (memoryState frontier x) (iterate body d.1.1 d.2 d.1.2) ∧ (∀ (i : Fin l), y.regs (tmp (Fin.castAdd (l + h.scratchSize + 3 + 1) i)) = output ((DataStructure.Memory.spec w).clientResult (memoryState frontier x) (iterate body d.1.1 d.2 d.1.2)) i) ∧ ∀ (i : Fin r), i ≠ frontier → (∀ (j : Fin (l + (l + h.scratchSize + 3) + 1)), tmp j ≠ i) → y.regs i = x.regs i

The existing loop emitter retains the complete realization postcondition while paying body charges and state/control overhead separately. This bounds that supplied emitter, not a classically reselected implementation.

def Cslib.WordRAM.Realization.Realizes.Witness.iterateRuntime {δ σ : Type} {k l : ℕ} (input : δ ↪ Fin k → ℕ) (output : σ ↪ Fin l → ℕ) {body : δ × σ → DataStructure.Memory.Prog σ} {safe : ℕ → δ × σ → DataStructure.Memory.State → Prop} {work : δ × σ → DataStructure.Memory.State → ℕ} (h : Witness Basis.exact body (appendWords input output) output safe work) : Witness Basis.exact (fun (x : (δ × σ) × ℕ) => match x with | ((d, a), fuel) => iterate body d fuel a) (((appendWords input output).prodMap (Equiv.funUnique (Fin 1) ℕ).symm.toEmbedding).trans (Fin.appendEquiv (k + l) 1).toEmbedding) output (fun (w : ℕ) (x : (δ × σ) × ℕ) (s : DataStructure.Memory.State) => match x with | ((d, a), fuel) => iterationSafe body safe w d fuel a s) fun (x : (δ × σ) × ℕ) (s : DataStructure.Memory.State) => match x with | ((d, a), fuel) => iterationWork body work d fuel a s

Retain the supplied body and the existing loop emitter as data. Its original coarse realization contract follows from the sharper same-emitter loopEmit_spec.

theorem Cslib.WordRAM.Realization.Realizes.iterateRuntime {δ σ : Type} {k l : ℕ} (input : δ ↪ Fin k → ℕ) (output : σ ↪ Fin l → ℕ) {body : δ × σ → DataStructure.Memory.Prog σ} {safe : ℕ → δ × σ → DataStructure.Memory.State → Prop} {work : δ × σ → DataStructure.Memory.State → ℕ} (h : Realizes Basis.exact body (appendWords input output) output safe work) : Realizes Basis.exact (fun (x : (δ × σ) × ℕ) => match x with | ((d, a), fuel) => iterate body d fuel a) (((appendWords input output).prodMap (Equiv.funUnique (Fin 1) ℕ).symm.toEmbedding).trans (Fin.appendEquiv (k + l) 1).toEmbedding) output (fun (w : ℕ) (x : (δ × σ) × ℕ) (s : DataStructure.Memory.State) => match x with | ((d, a), fuel) => iterationSafe body safe w d fuel a s) fun (x : (δ × σ) × ℕ) (s : DataStructure.Memory.State) => match x with | ((d, a), fuel) => iterationWork body work d fuel a s

The existential runtime-loop realization erases the retained supplied emitter.

theorem Cslib.WordRAM.Realization.RealizesBounded.iterateRuntime {δ σ : Type} {k l : ℕ} (input : δ ↪ Fin k → ℕ) (output : σ ↪ Fin l → ℕ) {body : δ × σ → DataStructure.Memory.Prog σ} {safe : ℕ → δ × σ → DataStructure.Memory.State → Prop} {work : δ × σ → DataStructure.Memory.State → ℕ} (h : RealizesBounded Basis.exact body (appendWords input output) output safe work) : RealizesBounded Basis.exact (fun (x : (δ × σ) × ℕ) => match x with | ((d, a), fuel) => iterate body d fuel a) (((appendWords input output).prodMap (Equiv.funUnique (Fin 1) ℕ).symm.toEmbedding).trans (Fin.appendEquiv (k + l) 1).toEmbedding) output (fun (w : ℕ) (x : (δ × σ) × ℕ) (s : DataStructure.Memory.State) => match x with | ((d, a), fuel) => iterationSafe body safe w d fuel a s) fun (x : (δ × σ) × ℕ) (s : DataStructure.Memory.State) => match x with | ((d, a), fuel) => iterationWork body work d fuel a s

Frontier-bounded realization of runtime-bounded iterate.