Retaining a uniform realization witness

Realizes.Witness retains supplied scratch, factor and emitter data with the same execution contract as Realizes. Its erasure supplies the existential judgment without discarding the data used by a concrete backend.

The legacy projections choose one witness of Realizes before any runtime argument, width, memory or register layout. They use classical choice from a proposition: they do not claim executable extraction from an arbitrary proof. They let adapters refer to the same emitted native code and its proved exchange factor, without adding another realization judgment.

Main definitions

• Realizes.scratchSize, Realizes.factor, Realizes.code: select the uniform witness.
• Realizes.Witness: retain a specified witness and its execution contract.
• Realizes.Witness.ofRealizes: an existential-only choice fallback.
• Realizes.Witness.consequence, Realizes.Witness.consequenceValid, Realizes.Witness.congr, Realizes.Witness.reindex: the Realizes adapters, retaining every supplied field.

Main results

• Realizes.code_spec: the selected code has the complete original realization contract.

structure Cslib.WordRAM.Realization.Realizes.Witness {δ α : Type} {k l : ℕ} (B : Basis) (p : δ → DataStructure.Memory.Prog α) (input : δ ↪ Fin k → ℕ) (output : α ↪ Fin l → ℕ) (safe : ℕ → δ → DataStructure.Memory.State → Prop) (work : δ → DataStructure.Memory.State → ℕ) : Type

A specified realization, retaining its resource parameters and emitter as data. Correctness is the same contract existentially quantified by Realizes, not a new execution semantics.

• scratchSize : ℕ

  Auxiliary registers, excluding results and the reserved extra slot.

• factor : ℕ

  Exchange factor for memory charges plus local work.

• code {r : ℕ} (frontier : Fin r) : (Fin k → Fin r) → (Fin (l + self.scratchSize + 1) → Fin r) → Code B r

  The emitter, fixed before all runtime values and register placements.

• code_spec : Spec B p input output safe work self.scratchSize self.factor fun {r : ℕ} => self.code

  The existing execution, whole-memory/frontier and register-frame contract.

theorem Cslib.WordRAM.Realization.Realizes.Witness.toRealizes {B : Basis} {δ α : Type} {k l : ℕ} {p : δ → DataStructure.Memory.Prog α} {input : δ ↪ Fin k → ℕ} {output : α ↪ Fin l → ℕ} {safe : ℕ → δ → DataStructure.Memory.State → Prop} {work : δ → DataStructure.Memory.State → ℕ} (h : Witness B p input output safe work) : Realizes B p input output safe work

Forget resource and emitter selection while retaining the original realization judgment.

noncomputable def Cslib.WordRAM.Realization.Realizes.scratchSize {B : Basis} {δ α : Type} {k l : ℕ} {p : δ → DataStructure.Memory.Prog α} {input : δ ↪ Fin k → ℕ} {output : α ↪ Fin l → ℕ} {safe : ℕ → δ → DataStructure.Memory.State → Prop} {work : δ → DataStructure.Memory.State → ℕ} (h : Realizes B p input output safe work) : ℕ

Number of auxiliary registers, chosen independently of every runtime value.

noncomputable def Cslib.WordRAM.Realization.Realizes.factor {B : Basis} {δ α : Type} {k l : ℕ} {p : δ → DataStructure.Memory.Prog α} {input : δ ↪ Fin k → ℕ} {output : α ↪ Fin l → ℕ} {safe : ℕ → δ → DataStructure.Memory.State → Prop} {work : δ → DataStructure.Memory.State → ℕ} (h : Realizes B p input output safe work) : ℕ

Uniform exchange factor for memory charges plus local work.

noncomputable def Cslib.WordRAM.Realization.Realizes.code {B : Basis} {δ α : Type} {k l : ℕ} {p : δ → DataStructure.Memory.Prog α} {input : δ ↪ Fin k → ℕ} {output : α ↪ Fin l → ℕ} {safe : ℕ → δ → DataStructure.Memory.State → Prop} {work : δ → DataStructure.Memory.State → ℕ} (h : Realizes B p input output safe work) {r : ℕ} (frontier : Fin r) : (Fin k → Fin r) → (Fin (l + h.scratchSize + 1) → Fin r) → Code B r

One emitter, selected before the register layout or any runtime data.

theorem Cslib.WordRAM.Realization.Realizes.code_spec {B : Basis} {δ α : Type} {k l : ℕ} {p : δ → DataStructure.Memory.Prog α} {input : δ ↪ Fin k → ℕ} {output : α ↪ Fin l → ℕ} {safe : ℕ → δ → DataStructure.Memory.State → Prop} {work : δ → DataStructure.Memory.State → ℕ} (h : Realizes B p input output safe work) {r : ℕ} (frontier : Fin r) (src : Fin k → Fin r) (tmp : Fin (l + h.scratchSize + 1) → Fin r) (hi : Function.Injective tmp) (hd : ∀ (i : Fin k) (j : Fin (l + h.scratchSize + 1)), src i ≠ tmp j) (hf : ∀ (j : Fin (l + h.scratchSize + 1)), tmp j ≠ frontier) (hs : ∀ (i : Fin k), src i ≠ frontier) : ¬(h.code frontier src tmp).ReadsWidth ∧ ∀ (w : ℕ) (d : δ) (x : Data r), Data.Bounded w x → x.regs ∘ src = input d → safe w d (memoryState frontier x) → (DataStructure.Memory.spec w).ValidHistory (memoryState frontier x) ((DataStructure.Memory.spec w).clientHistory (memoryState frontier x) (p d)) → ∃ (y : Data r), ExecWithin w (h.code frontier src tmp) x y (h.factor * (memoryCost (p d) (memoryState frontier x) + work d (memoryState frontier x) + 1)) ∧ memoryState frontier y = (DataStructure.Memory.spec w).clientState (memoryState frontier x) (p d) ∧ (∀ (i : Fin l), y.regs (tmp (Fin.castAdd (h.scratchSize + 1) i)) = output ((DataStructure.Memory.spec w).clientResult (memoryState frontier x) (p d)) i) ∧ ∀ (i : Fin r), i ≠ frontier → (∀ (j : Fin (l + h.scratchSize + 1)), tmp j ≠ i) → y.regs i = x.regs i

The selected witness retains width independence, literal whole-memory semantics, all result coordinates, and the original live-register frame.

noncomputable def Cslib.WordRAM.Realization.Realizes.Witness.ofRealizes {B : Basis} {δ α : Type} {k l : ℕ} {p : δ → DataStructure.Memory.Prog α} {input : δ ↪ Fin k → ℕ} {output : α ↪ Fin l → ℕ} {safe : ℕ → δ → DataStructure.Memory.State → Prop} {work : δ → DataStructure.Memory.State → ℕ} (h : Realizes B p input output safe work) : Witness B p input output safe work

Select a witness from an existential realization. This fallback preserves correctness but does not assert concrete scratch, factor or code identities for a particular derivation.

def Cslib.WordRAM.Realization.Realizes.Witness.consequence {B : Basis} {δ α : Type} {k l : ℕ} {p : δ → DataStructure.Memory.Prog α} {input : δ ↪ Fin k → ℕ} {output : α ↪ Fin l → ℕ} {safe : ℕ → δ → DataStructure.Memory.State → Prop} {work : δ → DataStructure.Memory.State → ℕ} {safe' : ℕ → δ → DataStructure.Memory.State → Prop} {work' : δ → DataStructure.Memory.State → ℕ} (h : Witness B p input output safe work) (hsafe : ∀ (w : ℕ) (d : δ) (s : DataStructure.Memory.State), (∀ (i : Fin k), Fits w (input d i)) → DataStructure.Memory.WellFormed w s → safe' w d s → safe w d s) (hwork : ∀ (d : δ) (s : DataStructure.Memory.State), work d s ≤ work' d s) : Witness B p input output safe' work'

Strengthen the entry domain or enlarge local work without reselecting any witness data.

def Cslib.WordRAM.Realization.Realizes.Witness.consequenceValid {B : Basis} {δ α : Type} {k l : ℕ} {p : δ → DataStructure.Memory.Prog α} {input : δ ↪ Fin k → ℕ} {output : α ↪ Fin l → ℕ} {safe : ℕ → δ → DataStructure.Memory.State → Prop} {work : δ → DataStructure.Memory.State → ℕ} {safe' : ℕ → δ → DataStructure.Memory.State → Prop} (h : Witness B p input output safe work) (hsafe : ∀ (w : ℕ) (d : δ) (s : DataStructure.Memory.State), (∀ (i : Fin k), Fits w (input d i)) → DataStructure.Memory.WellFormed w s → (DataStructure.Memory.spec w).ValidHistory s ((DataStructure.Memory.spec w).clientHistory s (p d)) → safe' w d s → safe w d s) : Witness B p input output safe' work

The client's own admissible history can discharge a stronger entry domain. The supplied scratch, factor and emitter remain unchanged.

def Cslib.WordRAM.Realization.Realizes.Witness.congr {B : Basis} {δ α : Type} {k l : ℕ} {p : δ → DataStructure.Memory.Prog α} {input : δ ↪ Fin k → ℕ} {output : α ↪ Fin l → ℕ} {safe : ℕ → δ → DataStructure.Memory.State → Prop} {work : δ → DataStructure.Memory.State → ℕ} {p' : δ → DataStructure.Memory.Prog α} (h : Witness B p input output safe work) (hp : ∀ (d : δ), p d = p' d) : Witness B p' input output safe work

Exact source equality changes no witness field or code.

def Cslib.WordRAM.Realization.Realizes.Witness.reindex {B : Basis} {δ α : Type} {k l : ℕ} {p : δ → DataStructure.Memory.Prog α} {input : δ ↪ Fin k → ℕ} {output : α ↪ Fin l → ℕ} {safe : ℕ → δ → DataStructure.Memory.State → Prop} {work : δ → DataStructure.Memory.State → ℕ} {ε : Type} {m : ℕ} (h : Witness B p input output safe work) (f : ε → δ) (env : ε ↪ Fin m → ℕ) (ix : Fin k → Fin m) (hw : ∀ (e : ε) (i : Fin k), input (f e) i = env e (ix i)) : Witness B (fun (e : ε) => p (f e)) env output (fun (w : ℕ) (e : ε) (s : DataStructure.Memory.State) => safe w (f e) s) fun (e : ε) (s : DataStructure.Memory.State) => work (f e) s

Rewire already live input words by a fixed index map, retaining the supplied resources. The pointwise encoding equality charges no new host-side argument computation.

structure Cslib.WordRAM.Realization.RealizesBounded.Witness {δ α : Type} {k l : ℕ} (B : Basis) (p : δ → DataStructure.Memory.Prog α) (input : δ ↪ Fin k → ℕ) (output : α ↪ Fin l → ℕ) (safe : ℕ → δ → DataStructure.Memory.State → Prop) (work : δ → DataStructure.Memory.State → ℕ) : Type

A specified frontier-bounded realization, retaining its resource parameters and emitter.

• scratchSize : ℕ

  Auxiliary registers, excluding results and the reserved extra slot.

• factor : ℕ

  Exchange factor for memory charges plus local work.

• code {r : ℕ} (frontier : Fin r) : (Fin k → Fin r) → (Fin (l + self.scratchSize + 1) → Fin r) → Code B r

  The emitter, fixed before all runtime values and register placements.

• code_spec : Realizes.SpecBounded B p input output safe work self.scratchSize self.factor fun {r : ℕ} => self.code

  The frontier-bounded execution, whole-memory/frontier and register-frame contract.

theorem Cslib.WordRAM.Realization.RealizesBounded.Witness.toRealizesBounded {B : Basis} {δ α : Type} {k l : ℕ} {p : δ → DataStructure.Memory.Prog α} {input : δ ↪ Fin k → ℕ} {output : α ↪ Fin l → ℕ} {safe : ℕ → δ → DataStructure.Memory.State → Prop} {work : δ → DataStructure.Memory.State → ℕ} (h : Witness B p input output safe work) : RealizesBounded B p input output safe work

Forget resource and emitter selection to RealizesBounded.

def Cslib.WordRAM.Realization.RealizesBounded.Witness.toWitness {B : Basis} {δ α : Type} {k l : ℕ} {p : δ → DataStructure.Memory.Prog α} {input : δ ↪ Fin k → ℕ} {output : α ↪ Fin l → ℕ} {safe : ℕ → δ → DataStructure.Memory.State → Prop} {work : δ → DataStructure.Memory.State → ℕ} (h : Witness B p input output safe work) : Realizes.Witness B p input output safe work

Erase the frontier bound on a retained witness.

noncomputable def Cslib.WordRAM.Realization.RealizesBounded.Witness.ofRealizesBounded {B : Basis} {δ α : Type} {k l : ℕ} {p : δ → DataStructure.Memory.Prog α} {input : δ ↪ Fin k → ℕ} {output : α ↪ Fin l → ℕ} {safe : ℕ → δ → DataStructure.Memory.State → Prop} {work : δ → DataStructure.Memory.State → ℕ} (h : RealizesBounded B p input output safe work) : Witness B p input output safe work

Select a witness from an existential RealizesBounded proof.