Native memory-query realizations

The native query arguments are already in the caller's live register environment. Loads and stores reuse the basis-generic execution rules. Allocation uses exact arithmetic and the existing generic zero-fill subroutine; it changes the full memory abstraction exactly as the memory oracle specifies. Argument computation, binds and the final halt are charged by the surrounding realization rules rather than hidden in these primitives.

Main definitions

• Realizes.readWitness, Realizes.writeWitness: supplied one-instruction witnesses.
• Realizes.allocDirtyWitness, Realizes.allocWitness: supplied allocation witnesses.

Main results

• Realizes.read, Realizes.write: one-instruction memory operations with live-register frames.
• Realizes.allocDirty: exact two-instruction bump allocation, including zero-width empty blocks.
• Realizes.alloc: zeroed allocation via the existing basis-generic zero-fill code.

def Cslib.WordRAM.Realization.Realizes.readWitness {B : Basis} {δ : Type} {k : ℕ} (input : δ ↪ Fin k → ℕ) (i : Fin k) : Witness B (fun (d : δ) => DataStructure.Memory.read (input d i)) input (Equiv.funUnique (Fin 1) ℕ).symm.toEmbedding (fun (x : ℕ) (x_1 : δ) (x_2 : DataStructure.Memory.State) => True) fun (x : δ) (x_1 : DataStructure.Memory.State) => 0

A read returns a word without changing the frontier or any memory cell. Its address is a live word; memory admissibility additionally states that the address is allocated.

theorem Cslib.WordRAM.Realization.Realizes.read {B : Basis} {δ : Type} {k : ℕ} (input : δ ↪ Fin k → ℕ) (i : Fin k) : Realizes B (fun (d : δ) => DataStructure.Memory.read (input d i)) input (Equiv.funUnique (Fin 1) ℕ).symm.toEmbedding (fun (x : ℕ) (x_1 : δ) (x_2 : DataStructure.Memory.State) => True) fun (x : δ) (x_1 : DataStructure.Memory.State) => 0

The existential realization supplied by readWitness.

def Cslib.WordRAM.Realization.Realizes.writeWitness {B : Basis} {δ : Type} {k : ℕ} (input : δ ↪ Fin k → ℕ) (i j : Fin k) : Witness B (fun (d : δ) => DataStructure.Memory.write (input d i) (input d j)) input (Equiv.ofUnique Unit (Fin 0 → ℕ)).toEmbedding (fun (x : ℕ) (x_1 : δ) (x_2 : DataStructure.Memory.State) => True) fun (x : δ) (x_1 : DataStructure.Memory.State) => 0

A store returns unit, updates precisely the selected memory cell and preserves all registers. The value and allocated-address hypotheses remain in the existing memory valid-history premise.

theorem Cslib.WordRAM.Realization.Realizes.write {B : Basis} {δ : Type} {k : ℕ} (input : δ ↪ Fin k → ℕ) (i j : Fin k) : Realizes B (fun (d : δ) => DataStructure.Memory.write (input d i) (input d j)) input (Equiv.ofUnique Unit (Fin 0 → ℕ)).toEmbedding (fun (x : ℕ) (x_1 : δ) (x_2 : DataStructure.Memory.State) => True) fun (x : δ) (x_1 : DataStructure.Memory.State) => 0

The existential realization supplied by writeWitness.

def Cslib.WordRAM.Realization.Realizes.allocDirtyWitness {δ : Type} {k : ℕ} (input : δ ↪ Fin k → ℕ) (i : Fin k) : Witness Basis.exact (fun (d : δ) => DataStructure.Memory.allocDirty (input d i)) input (Equiv.funUnique (Fin 1) ℕ).symm.toEmbedding (fun (x : ℕ) (x_1 : δ) (x_2 : DataStructure.Memory.State) => True) fun (x : δ) (x_1 : DataStructure.Memory.State) => 0

Dirty allocation returns the old frontier and adds the count exactly, without touching memory. No constant 1 is materialized, so a zero-width empty allocation is included.

theorem Cslib.WordRAM.Realization.Realizes.allocDirty {δ : Type} {k : ℕ} (input : δ ↪ Fin k → ℕ) (i : Fin k) : Realizes Basis.exact (fun (d : δ) => DataStructure.Memory.allocDirty (input d i)) input (Equiv.funUnique (Fin 1) ℕ).symm.toEmbedding (fun (x : ℕ) (x_1 : δ) (x_2 : DataStructure.Memory.State) => True) fun (x : δ) (x_1 : DataStructure.Memory.State) => 0

The existential realization supplied by allocDirtyWitness.

def Cslib.WordRAM.Realization.Realizes.allocWitness {δ : Type} {k : ℕ} (input : δ ↪ Fin k → ℕ) (i : Fin k) : Witness Basis.exact (fun (d : δ) => DataStructure.Memory.alloc (input d i)) input (Equiv.funUnique (Fin 1) ℕ).symm.toEmbedding (fun (x : ℕ) (x_1 : δ) (x_2 : DataStructure.Memory.State) => True) fun (x : δ) (x_1 : DataStructure.Memory.State) => 0

Zeroed allocation realizes the full oracle memory update on arbitrary old scratch contents. The reused clear code materializes 1 only in the positive-size branch.

theorem Cslib.WordRAM.Realization.Realizes.alloc {δ : Type} {k : ℕ} (input : δ ↪ Fin k → ℕ) (i : Fin k) : Realizes Basis.exact (fun (d : δ) => DataStructure.Memory.alloc (input d i)) input (Equiv.funUnique (Fin 1) ℕ).symm.toEmbedding (fun (x : ℕ) (x_1 : δ) (x_2 : DataStructure.Memory.State) => True) fun (x : δ) (x_1 : DataStructure.Memory.State) => 0

The existential realization supplied by allocWitness.

theorem Cslib.WordRAM.Realization.RealizesBounded.read {B : Basis} {δ : Type} {k : ℕ} (input : δ ↪ Fin k → ℕ) (i : Fin k) : RealizesBounded B (fun (d : δ) => DataStructure.Memory.read (input d i)) input (Equiv.funUnique (Fin 1) ℕ).symm.toEmbedding (fun (x : ℕ) (x_1 : δ) (x_2 : DataStructure.Memory.State) => True) fun (x : δ) (x_1 : DataStructure.Memory.State) => 0

Frontier-bounded realization of Memory.read.

theorem Cslib.WordRAM.Realization.RealizesBounded.write {B : Basis} {δ : Type} {k : ℕ} (input : δ ↪ Fin k → ℕ) (i j : Fin k) : RealizesBounded B (fun (d : δ) => DataStructure.Memory.write (input d i) (input d j)) input (Equiv.ofUnique Unit (Fin 0 → ℕ)).toEmbedding (fun (x : ℕ) (x_1 : δ) (x_2 : DataStructure.Memory.State) => True) fun (x : δ) (x_1 : DataStructure.Memory.State) => 0

Frontier-bounded realization of Memory.write.

theorem Cslib.WordRAM.Realization.RealizesBounded.allocDirty {δ : Type} {k : ℕ} (input : δ ↪ Fin k → ℕ) (i : Fin k) : RealizesBounded Basis.exact (fun (d : δ) => DataStructure.Memory.allocDirty (input d i)) input (Equiv.funUnique (Fin 1) ℕ).symm.toEmbedding (fun (x : ℕ) (x_1 : δ) (x_2 : DataStructure.Memory.State) => True) fun (x : δ) (x_1 : DataStructure.Memory.State) => 0

Frontier-bounded realization of Memory.allocDirty.

theorem Cslib.WordRAM.Realization.RealizesBounded.alloc {δ : Type} {k : ℕ} (input : δ ↪ Fin k → ℕ) (i : Fin k) : RealizesBounded Basis.exact (fun (d : δ) => DataStructure.Memory.alloc (input d i)) input (Equiv.funUnique (Fin 1) ℕ).symm.toEmbedding (fun (x : ℕ) (x_1 : δ) (x_2 : DataStructure.Memory.State) => True) fun (x : δ) (x_1 : DataStructure.Memory.State) => 0

Frontier-bounded realization of Memory.alloc.