Clocked multi-step execution and whole-run native transport for generic RAMs

Iterating FiniteState.step yields a clocked multi-step finite-state semantics FiniteState.run whose halting outputs agree with GenericRAM.run and GenericRAM.Executes. Each continuing step adds at most one distinct address to the sparse store.

On the native multitape Turing-machine side, applying NativeCertificate.iterate to FiniteState.stepCertificate yields FiniteState.runCertificate and FiniteState.evalCertificate, together with automatic whole-run algorithm transport (FiniteState.transportCertificate, FiniteState.transport_inO, FiniteState.transport_polyTime, and FiniteState.transport_polyTime_of_le_const).

Main definitions

• FiniteState.init, FiniteState.initConst: finite initial configurations at instruction 0.
• FiniteState.stepResult, FiniteState.run, FiniteState.eval: clocked multi-step execution and halting output extraction.
• FiniteState.initCertificate, FiniteState.initConstCertificate: native initialization certificates.
• FiniteState.runCertificate, FiniteState.evalCertificate, FiniteState.runTime, FiniteState.runSpace: native clocked whole-run certificates and parameterized resource bounds.
• FiniteState.transportCertificate: automatic whole-run transport of GenericRAM.Executes certificates to native multitape Turing machines.

Main results

• FiniteState.length_entries_run_le: n steps add at most n stored sparse-memory cells.
• FiniteState.denote_run, FiniteState.executes_iff_exists_run: exact multi-step refinement.
• FiniteState.run_inO, FiniteState.eval_inO: one finite native machine implements clocked multi-step execution uniformly across runtime configurations, step budgets, and states.
• FiniteState.le_runTime_of_run_eq_inl, FiniteState.le_runSpace_of_run_eq_inl: retention of per-step primitive and sparse-memory bounds along the run.
• FiniteState.step_polyTime, FiniteState.transport_inO, FiniteState.transport_polyTime, FiniteState.transport_polyTime_of_le_const: parameterized and polynomial-time whole-run transport theorems.

References

• S. A. Cook and R. A. Reckhow, Time bounded random access machines
• M. Sipser, Introduction to the Theory of Computation

Multi-step finite-state execution and refinement

def Cslib.GenericRAM.FiniteState.continuing {M : Model} {r : ℕ} : Result M r → Option (FiniteState M r)

Extract the continuing finite state from a step outcome, if any.

@[simp]

theorem Cslib.GenericRAM.FiniteState.continuing_none {M : Model} {r : ℕ} : continuing none = none

@[simp]

theorem Cslib.GenericRAM.FiniteState.continuing_inl {M : Model} {r : ℕ} (s : FiniteState M r) : continuing (some (Sum.inl s)) = some s

@[simp]

theorem Cslib.GenericRAM.FiniteState.continuing_inr {M : Model} {r : ℕ} (v : M.Value) : continuing (some (Sum.inr v)) = none

theorem Cslib.GenericRAM.FiniteState.continuing_eq_elim {M : Model} {r : ℕ} (res : Result M r) : continuing res = Option.elim res none Sum.getLeft?

def Cslib.GenericRAM.FiniteState.output {M : Model} {r : ℕ} : Result M r → Option M.Value

Extract the halting output value from a step outcome, if any.

@[simp]

theorem Cslib.GenericRAM.FiniteState.output_none {M : Model} {r : ℕ} : output none = none

@[simp]

theorem Cslib.GenericRAM.FiniteState.output_inl {M : Model} {r : ℕ} (s : FiniteState M r) : output (some (Sum.inl s)) = none

@[simp]

theorem Cslib.GenericRAM.FiniteState.output_inr {M : Model} {r : ℕ} (v : M.Value) : output (some (Sum.inr v)) = some v

theorem Cslib.GenericRAM.FiniteState.output_eq_elim {M : Model} {r : ℕ} (res : Result M r) : output res = Option.elim res none Sum.getRight?

def Cslib.GenericRAM.FiniteState.init {M : Model} {r : ℕ} (regs : Fin r → M.Value) (default : M.Value) (memory : SparseMemory M.Address M.Value) : FiniteState M r

Initial finite configuration at control label 0.

def Cslib.GenericRAM.FiniteState.initConst {M : Model} {r : ℕ} (initReg default : M.Value) (memory : SparseMemory M.Address M.Value) : FiniteState M r

Initial finite configuration at control label 0 with a uniform initial register value.

@[simp]

theorem Cslib.GenericRAM.FiniteState.denote_init_empty {M : Model} {r : ℕ} (initReg default : M.Value) : (initConst initReg default ∅).denote = { pc := 0, data := Data.init initReg fun (x : M.Address) => default }

def Cslib.GenericRAM.FiniteState.stepResult {M : Model} {r : ℕ} (k : M.Config) (p : Program M r) : Result M r → Result M r

Advance a continuing finite state by one step; halting and faulting outcomes are absorbing.

@[simp]

theorem Cslib.GenericRAM.FiniteState.stepResult_none {M : Model} {r : ℕ} (k : M.Config) (p : Program M r) : stepResult k p none = none

@[simp]

theorem Cslib.GenericRAM.FiniteState.stepResult_inl {M : Model} {r : ℕ} (k : M.Config) (p : Program M r) (s : FiniteState M r) : stepResult k p (some (Sum.inl s)) = step k p s

@[simp]

theorem Cslib.GenericRAM.FiniteState.stepResult_inr {M : Model} {r : ℕ} (k : M.Config) (p : Program M r) (v : M.Value) : stepResult k p (some (Sum.inr v)) = some (Sum.inr v)

theorem Cslib.GenericRAM.FiniteState.stepResult_eq {M : Model} {r : ℕ} (k : M.Config) (p : Program M r) (res : Result M r) : stepResult k p res = (continuing res).elim res fun (s : FiniteState M r) => step k p s

@[simp]

theorem Cslib.GenericRAM.FiniteState.iterate_stepResult_none {M : Model} {r : ℕ} (k : M.Config) (p : Program M r) (n : ℕ) : (stepResult k p)^[n] none = none

@[simp]

theorem Cslib.GenericRAM.FiniteState.iterate_stepResult_inr {M : Model} {r : ℕ} (k : M.Config) (p : Program M r) (n : ℕ) (v : M.Value) : (stepResult k p)^[n] (some (Sum.inr v)) = some (Sum.inr v)

def Cslib.GenericRAM.FiniteState.run {M : Model} {r : ℕ} (k : M.Config) (p : Program M r) : ℕ → FiniteState M r → Result M r

Execute a fixed program for at most n steps from s, stopping early on halt or fault.

@[simp]

theorem Cslib.GenericRAM.FiniteState.run_zero {M : Model} {r : ℕ} (k : M.Config) (p : Program M r) (s : FiniteState M r) : run k p 0 s = some (Sum.inl s)

theorem Cslib.GenericRAM.FiniteState.run_succ {M : Model} {r : ℕ} (k : M.Config) (p : Program M r) (n : ℕ) (s : FiniteState M r) : run k p (n + 1) s = match step k p s with | some (Sum.inl t) => run k p n t | out => out

theorem Cslib.GenericRAM.FiniteState.run_eq_iterate_stepResult {M : Model} {r : ℕ} (k : M.Config) (p : Program M r) (n : ℕ) (s : FiniteState M r) : run k p n s = (stepResult k p)^[n] (some (Sum.inl s))

Multi-step execution is exact iteration of stepResult from some (.inl s).

theorem Cslib.GenericRAM.FiniteState.run_add {M : Model} {r : ℕ} (k : M.Config) (p : Program M r) (m n : ℕ) (s : FiniteState M r) : run k p (m + n) s = match run k p m s with | some (Sum.inl t) => run k p n t | out => out

def Cslib.GenericRAM.FiniteState.eval {M : Model} {r : ℕ} (k : M.Config) (p : Program M r) (n : ℕ) (s : FiniteState M r) : Option M.Value

Halting output after at most n finite steps (none on fault or unhalted continuation).

Memory-growth and default-preservation invariants

theorem Cslib.GenericRAM.FiniteState.default_move {M : Model} {r : ℕ} {k : M.Config} {s t : FiniteState M r} {d : Fin r} {v : M.Value} (h : move k s d v = some t) : t.default = s.default

theorem Cslib.GenericRAM.FiniteState.length_entries_move_eq {M : Model} {r : ℕ} {k : M.Config} {s t : FiniteState M r} {d : Fin r} {v : M.Value} (h : move k s d v = some t) : t.memory.entries.length = s.memory.entries.length

theorem Cslib.GenericRAM.FiniteState.default_evalOp {M : Model} {r : ℕ} {k : M.Config} {o : Op M r} {s t : FiniteState M r} (h : evalOp k o s = some t) : t.default = s.default

theorem Cslib.GenericRAM.FiniteState.length_entries_evalOp_le {M : Model} {r : ℕ} {k : M.Config} {o : Op M r} {s t : FiniteState M r} (h : evalOp k o s = some t) : t.memory.entries.length ≤ s.memory.entries.length + 1

A single data operation adds at most one stored address to sparse memory.

theorem Cslib.GenericRAM.FiniteState.default_resume {M : Model} {r : ℕ} {k : M.Config} {pc : ℕ} {s t : FiniteState M r} (h : resume k pc s = some (Sum.inl t)) : t.default = s.default

theorem Cslib.GenericRAM.FiniteState.memory_resume {M : Model} {r : ℕ} {k : M.Config} {pc : ℕ} {s t : FiniteState M r} (h : resume k pc s = some (Sum.inl t)) : t.memory = s.memory

theorem Cslib.GenericRAM.FiniteState.default_evalInstr {M : Model} {r : ℕ} {k : M.Config} {nextPC : ℕ} {i : Instr M r} {s t : FiniteState M r} (h : evalInstr k nextPC i s = some (Sum.inl t)) : t.default = s.default

theorem Cslib.GenericRAM.FiniteState.length_entries_evalInstr_le {M : Model} {r : ℕ} {k : M.Config} {nextPC : ℕ} {i : Instr M r} {s t : FiniteState M r} (h : evalInstr k nextPC i s = some (Sum.inl t)) : t.memory.entries.length ≤ s.memory.entries.length + 1

theorem Cslib.GenericRAM.FiniteState.default_step {M : Model} {r : ℕ} {k : M.Config} {p : Program M r} {s t : FiniteState M r} (h : step k p s = some (Sum.inl t)) : t.default = s.default

A continuing finite step preserves the memory default.

theorem Cslib.GenericRAM.FiniteState.length_entries_step_le {M : Model} {r : ℕ} {k : M.Config} {p : Program M r} {s t : FiniteState M r} (h : step k p s = some (Sum.inl t)) : t.memory.entries.length ≤ s.memory.entries.length + 1

A continuing finite step adds at most one stored address to sparse memory.

theorem Cslib.GenericRAM.FiniteState.default_run {M : Model} {r : ℕ} {k : M.Config} {p : Program M r} {n : ℕ} {s t : FiniteState M r} (h : run k p n s = some (Sum.inl t)) : t.default = s.default

Multi-step execution preserves the memory default on all continuing states.

theorem Cslib.GenericRAM.FiniteState.length_entries_run_le {M : Model} {r : ℕ} {k : M.Config} {p : Program M r} {n : ℕ} {s t : FiniteState M r} (h : run k p n s = some (Sum.inl t)) : t.memory.entries.length ≤ s.memory.entries.length + n

Across n finite steps, sparse memory grows by at most n stored cells.

Multi-step denotation and Executes correspondence

theorem Cslib.GenericRAM.FiniteState.runs_of_run_eq_inl {M : Model} {r : ℕ} {k : M.Config} {p : Program M r} {n : ℕ} {s t : FiniteState M r} (h : run k p n s = some (Sum.inl t)) : Runs k p s.denote t.denote n

Continuing for n finite steps refines an n-step GenericRAM.Runs trace.

theorem Cslib.GenericRAM.FiniteState.exists_run_eq_inl_of_runs {M : Model} {r : ℕ} {k : M.Config} {p : Program M r} {n : ℕ} {s : FiniteState M r} {u : State M r} (h : Runs k p s.denote u n) : ∃ (t : FiniteState M r), run k p n s = some (Sum.inl t) ∧ t.denote = u

Every n-step GenericRAM.Runs trace from s.denote lifts to a continuing finite state.

theorem Cslib.GenericRAM.FiniteState.denote_run {M : Model} {r : ℕ} (k : M.Config) (p : Program M r) (n : ℕ) (s : FiniteState M r) : eval k p n s = Option.map Prod.fst (GenericRAM.run k p n s.denote)

Exact multi-step output refinement: at every step budget n, the finite-state evaluator agrees with the fuel-bounded generic RAM interpreter.

theorem Cslib.GenericRAM.FiniteState.run_eq_inr_of_executes {M : Model} {r : ℕ} {k : M.Config} {p : Program M r} {s : FiniteState M r} {v : M.Value} {m n : ℕ} (h : Executes k p s.denote v m) (hmn : m ≤ n) : run k p n s = some (Sum.inr v)

A halting execution of m ≤ n instructions halts with the same output in n finite steps.

theorem Cslib.GenericRAM.FiniteState.eval_eq_some_of_executes {M : Model} {r : ℕ} {k : M.Config} {p : Program M r} {s : FiniteState M r} {v : M.Value} {m n : ℕ} (h : Executes k p s.denote v m) (hmn : m ≤ n) : eval k p n s = some v

A halting execution of m ≤ n instructions produces some v under eval.

theorem Cslib.GenericRAM.FiniteState.executes_of_run_eq_inr {M : Model} {r : ℕ} {k : M.Config} {p : Program M r} {n : ℕ} {s : FiniteState M r} {v : M.Value} (h : run k p n s = some (Sum.inr v)) : ∃ m ≤ n, Executes k p s.denote v m

Every halting finite-state run within n steps witnesses a halting GenericRAM.Executes run of at most n instructions.

theorem Cslib.GenericRAM.FiniteState.executes_iff_exists_run {M : Model} {r : ℕ} (k : M.Config) (p : Program M r) (s : FiniteState M r) (v : M.Value) : (∃ (m : ℕ), Executes k p s.denote v m) ↔ ∃ (n : ℕ), run k p n s = some (Sum.inr v)

Halting generic-RAM executions from s.denote correspond to halting finite-state runs.

Native certificates for initialization, clocked execution, and transport

@[reducible, inline]

noncomputable abbrev Cslib.GenericRAM.FiniteState.initEncoding {M : Model} {r : ℕ} (enc : M.Encoding) : (Fin r → M.Value) × M.Value × SparseMemory M.Address M.Value ↪ List Bool

Framed encoding of initialization arguments (regs, default, memory).

noncomputable def Cslib.GenericRAM.FiniteState.initCertificate {M : Model} {r : ℕ} {α : Type} {ei : α ↪ List Bool} (enc : M.Encoding) {regsFn : α → Fin r → M.Value} {defaultFn : α → M.Value} {memoryFn : α → SparseMemory M.Address M.Value} (regs : NativeCertificate regsFn ei (Turing.MultiTapeTM.encPi enc.value)) (default : NativeCertificate defaultFn ei enc.value) (memory : NativeCertificate memoryFn ei (SparseMemory.encoding enc.address enc.value)) : NativeCertificate (fun (a : α) => init (regsFn a) (defaultFn a) (memoryFn a)) ei (encoding enc)

Construct an initial finite configuration at pc = 0 from certificates for its fields.

@[simp]

theorem Cslib.GenericRAM.FiniteState.initCertificate_time {M : Model} {r : ℕ} {α : Type} {ei : α ↪ List Bool} (enc : M.Encoding) {regsFn : α → Fin r → M.Value} {defaultFn : α → M.Value} {memoryFn : α → SparseMemory M.Address M.Value} (regs : NativeCertificate regsFn ei (Turing.MultiTapeTM.encPi enc.value)) (default : NativeCertificate defaultFn ei enc.value) (memory : NativeCertificate memoryFn ei (SparseMemory.encoding enc.address enc.value)) (a : α) : (initCertificate enc regs default memory).time a = (ei a).length + (regs.time a + (default.time a + memory.time a))

@[simp]

theorem Cslib.GenericRAM.FiniteState.initCertificate_space {M : Model} {r : ℕ} {α : Type} {ei : α ↪ List Bool} (enc : M.Encoding) {regsFn : α → Fin r → M.Value} {defaultFn : α → M.Value} {memoryFn : α → SparseMemory M.Address M.Value} (regs : NativeCertificate regsFn ei (Turing.MultiTapeTM.encPi enc.value)) (default : NativeCertificate defaultFn ei enc.value) (memory : NativeCertificate memoryFn ei (SparseMemory.encoding enc.address enc.value)) (a : α) : (initCertificate enc regs default memory).space a = (ei a).length + (regs.space a + (default.space a + memory.space a))

def Cslib.GenericRAM.FiniteState.constRegsCertificate {M : Model} {r : ℕ} {α : Type} {ei : α ↪ List Bool} (enc : M.Encoding) {initRegFn : α → M.Value} (initReg : NativeCertificate initRegFn ei enc.value) : NativeCertificate (fun (a : α) (x : Fin r) => initRegFn a) ei (Turing.MultiTapeTM.encPi enc.value)

Construct a constant-register tuple fun _ : Fin r => initReg a via ComputableTidilyInO.pi.

noncomputable def Cslib.GenericRAM.FiniteState.initConstCertificate {M : Model} {r : ℕ} {α : Type} {ei : α ↪ List Bool} (enc : M.Encoding) {initRegFn defaultFn : α → M.Value} {memoryFn : α → SparseMemory M.Address M.Value} (initReg : NativeCertificate initRegFn ei enc.value) (default : NativeCertificate defaultFn ei enc.value) (memory : NativeCertificate memoryFn ei (SparseMemory.encoding enc.address enc.value)) : NativeCertificate (fun (a : α) => initConst (initRegFn a) (defaultFn a) (memoryFn a)) ei (encoding enc)

Construct an initial finite configuration at pc = 0 with constant registers initReg.

theorem Cslib.GenericRAM.FiniteState.init_inO {M : Model} {r : ℕ} (enc : M.Encoding) : Turing.MultiTapeTM.ComputableTidilyInO (fun (q : (Fin r → M.Value) × M.Value × SparseMemory M.Address M.Value) => init q.1 q.2.1 q.2.2) (initEncoding enc) (encoding enc) (fun (q : (Fin r → M.Value) × M.Value × SparseMemory M.Address M.Value) => 4 * ((initEncoding enc) q).length) fun (q : (Fin r → M.Value) × M.Value × SparseMemory M.Address M.Value) => 4 * ((initEncoding enc) q).length

Top-level native certificate for init on (regs, default, memory).

Outcome projection certificates

noncomputable def Cslib.GenericRAM.FiniteState.continuingCertificate {M : Model} {r : ℕ} (enc : M.Encoding) : NativeCertificate continuing (resultEncoding enc) (Turing.MultiTapeTM.encOption (encoding enc))

Extract a continuing finite state from Result M r in linear time and space.

@[simp]

theorem Cslib.GenericRAM.FiniteState.continuingCertificate_time {M : Model} {r : ℕ} (enc : M.Encoding) (res : Result M r) : (continuingCertificate enc).time res = ((resultEncoding enc) res).length

@[simp]

theorem Cslib.GenericRAM.FiniteState.continuingCertificate_space {M : Model} {r : ℕ} (enc : M.Encoding) (res : Result M r) : (continuingCertificate enc).space res = ((resultEncoding enc) res).length

noncomputable def Cslib.GenericRAM.FiniteState.outputCertificate {M : Model} {r : ℕ} (enc : M.Encoding) : NativeCertificate output (resultEncoding enc) (Turing.MultiTapeTM.encOption enc.value)

Extract a halting output value from Result M r in linear time and space.

@[simp]

theorem Cslib.GenericRAM.FiniteState.outputCertificate_time {M : Model} {r : ℕ} (enc : M.Encoding) (res : Result M r) : (outputCertificate enc).time res = ((resultEncoding enc) res).length

@[simp]

theorem Cslib.GenericRAM.FiniteState.outputCertificate_space {M : Model} {r : ℕ} (enc : M.Encoding) (res : Result M r) : (outputCertificate enc).space res = ((resultEncoding enc) res).length

Clocked multi-step simulation certificates

@[reducible, inline]

noncomputable abbrev Cslib.GenericRAM.FiniteState.loopEncoding {M : Model} {r : ℕ} (enc : M.Encoding) : M.Config × Result M r ↪ List Bool

Encoding of the loop state (k, res) : M.Config × Result M r.

@[reducible, inline]

noncomputable abbrev Cslib.GenericRAM.FiniteState.runInputEncoding {M : Model} {r : ℕ} (enc : M.Encoding) : ℕ × M.Config × FiniteState M r ↪ List Bool

Encoding of a clocked simulation input (n, (k, s)) : ℕ × (M.Config × FiniteState M r).

def Cslib.GenericRAM.FiniteState.round {M : Model} {r : ℕ} (p : Program M r) (q : M.Config × Result M r) : M.Config × Result M r

One round of the clocked simulator, preserving the runtime configuration.

theorem Cslib.GenericRAM.FiniteState.iterate_round {M : Model} {r : ℕ} (p : Program M r) (n : ℕ) (k : M.Config) (res : Result M r) : (round p)^[n] (k, res) = (k, (stepResult k p)^[n] res)

theorem Cslib.GenericRAM.FiniteState.iterate_round_inl {M : Model} {r : ℕ} (p : Program M r) (n : ℕ) (k : M.Config) (s : FiniteState M r) : (round p)^[n] (k, some (Sum.inl s)) = (k, run k p n s)

noncomputable def Cslib.GenericRAM.FiniteState.stepResultCertificate {M : Model} {r : ℕ} (enc : M.Encoding) (N : M.NativePrimitives enc) (p : Program M r) : NativeCertificate (fun (q : M.Config × Result M r) => stepResult q.1 p q.2) (loopEncoding enc) (resultEncoding enc)

Native certificate for stepResult, charging stepCertificate only on continuing states.

noncomputable def Cslib.GenericRAM.FiniteState.roundCertificate {M : Model} {r : ℕ} (enc : M.Encoding) (N : M.NativePrimitives enc) (p : Program M r) : NativeCertificate (round p) (loopEncoding enc) (loopEncoding enc)

Native certificate for one clocked simulation round on M.Config × Result M r.

noncomputable def Cslib.GenericRAM.FiniteState.initLoopCertificate {M : Model} {r : ℕ} (enc : M.Encoding) : NativeCertificate (fun (q : ℕ × M.Config × FiniteState M r) => (q.2.1, some (Sum.inl q.2.2))) (runInputEncoding enc) (loopEncoding enc)

Prepare the initial loop state (k, some (.inl s)) from (n, (k, s)).

noncomputable def Cslib.GenericRAM.FiniteState.runCertificate {M : Model} {r : ℕ} (enc : M.Encoding) (N : M.NativePrimitives enc) (p : Program M r) : NativeCertificate (fun (q : ℕ × M.Config × FiniteState M r) => run q.2.1 p q.1 q.2.2) (runInputEncoding enc) (resultEncoding enc)

Native certificate for clocked multi-step execution run q.2.1 p q.1 q.2.2.

noncomputable def Cslib.GenericRAM.FiniteState.runTime {M : Model} {r : ℕ} (enc : M.Encoding) (N : M.NativePrimitives enc) (p : Program M r) : ℕ × M.Config × FiniteState M r → ℕ

Parameterized time bound for clocked multi-step execution.

noncomputable def Cslib.GenericRAM.FiniteState.runSpace {M : Model} {r : ℕ} (enc : M.Encoding) (N : M.NativePrimitives enc) (p : Program M r) : ℕ × M.Config × FiniteState M r → ℕ

Parameterized space bound for clocked multi-step execution.

theorem Cslib.GenericRAM.FiniteState.run_inO {M : Model} {r : ℕ} (enc : M.Encoding) (N : M.NativePrimitives enc) (p : Program M r) : Turing.MultiTapeTM.ComputableTidilyInO (fun (q : ℕ × M.Config × FiniteState M r) => run q.2.1 p q.1 q.2.2) (runInputEncoding enc) (resultEncoding enc) (runTime enc N p) (runSpace enc N p)

One finite native machine implements clocked multi-step execution uniformly across step budgets, runtime configurations, and finite states.

noncomputable def Cslib.GenericRAM.FiniteState.evalCertificate {M : Model} {r : ℕ} (enc : M.Encoding) (N : M.NativePrimitives enc) (p : Program M r) : NativeCertificate (fun (q : ℕ × M.Config × FiniteState M r) => eval q.2.1 p q.1 q.2.2) (runInputEncoding enc) (Turing.MultiTapeTM.encOption enc.value)

Native certificate for clocked output evaluation eval q.2.1 p q.1 q.2.2.

@[simp]

theorem Cslib.GenericRAM.FiniteState.evalCertificate_time {M : Model} {r : ℕ} (enc : M.Encoding) (N : M.NativePrimitives enc) (p : Program M r) : (evalCertificate enc N p).time = runTime enc N p

@[simp]

theorem Cslib.GenericRAM.FiniteState.evalCertificate_space {M : Model} {r : ℕ} (enc : M.Encoding) (N : M.NativePrimitives enc) (p : Program M r) : (evalCertificate enc N p).space = runSpace enc N p

theorem Cslib.GenericRAM.FiniteState.eval_inO {M : Model} {r : ℕ} (enc : M.Encoding) (N : M.NativePrimitives enc) (p : Program M r) : Turing.MultiTapeTM.ComputableTidilyInO (fun (q : ℕ × M.Config × FiniteState M r) => eval q.2.1 p q.1 q.2.2) (runInputEncoding enc) (Turing.MultiTapeTM.encOption enc.value) (runTime enc N p) (runSpace enc N p)

Native ComputableTidilyInO theorem for clocked output evaluation.

Retention of per-step resource bounds in runTime and runSpace

theorem Cslib.GenericRAM.FiniteState.le_roundCertificate_time_inl {M : Model} {r : ℕ} (enc : M.Encoding) (N : M.NativePrimitives enc) (p : Program M r) (k : M.Config) (s : FiniteState M r) : stepTime enc N p (k, s) ≤ (roundCertificate enc N p).time (k, some (Sum.inl s))

theorem Cslib.GenericRAM.FiniteState.le_roundCertificate_space_inl {M : Model} {r : ℕ} (enc : M.Encoding) (N : M.NativePrimitives enc) (p : Program M r) (k : M.Config) (s : FiniteState M r) : stepSpace enc N p (k, s) ≤ (roundCertificate enc N p).space (k, some (Sum.inl s))

theorem Cslib.GenericRAM.FiniteState.le_runTime_of_run_eq_inl {M : Model} {r : ℕ} (enc : M.Encoding) (N : M.NativePrimitives enc) (p : Program M r) {n j : ℕ} {k : M.Config} {s t : FiniteState M r} (hj : j ≤ n) (hrun : run k p j s = some (Sum.inl t)) : stepTime enc N p (k, t) ≤ runTime enc N p (n, k, s)

Every continuing state reached within j ≤ n steps has its single-step time bound retained in runTime.

theorem Cslib.GenericRAM.FiniteState.le_runSpace_of_run_eq_inl {M : Model} {r : ℕ} (enc : M.Encoding) (N : M.NativePrimitives enc) (p : Program M r) {n j : ℕ} {k : M.Config} {s t : FiniteState M r} (hj : j ≤ n) (hrun : run k p j s = some (Sum.inl t)) : stepSpace enc N p (k, t) ≤ runSpace enc N p (n, k, s)

Every continuing state reached within j ≤ n steps has its single-step space bound retained in runSpace.

Automatic whole-run algorithm transport

theorem Cslib.GenericRAM.FiniteState.unoption_inO {M : Model} (ev : M.Value ↪ List Bool) : Turing.MultiTapeTM.ComputableTidilyInO (fun (o : Option M.Value) => ((Turing.MultiTapeTM.encOption ev) o).tail) (Turing.MultiTapeTM.encOption ev) Turing.MultiTapeTM.encBits (fun (o : Option M.Value) => ((Turing.MultiTapeTM.encOption ev) o).length) fun (o : Option M.Value) => ((Turing.MultiTapeTM.encOption ev) o).length

noncomputable def Cslib.GenericRAM.FiniteState.transportCertificate {M : Model} {r : ℕ} {α : Type} {ei : α ↪ List Bool} (enc : M.Encoding) (N : M.NativePrimitives enc) (p : Program M r) {f : α → M.Value} {cfg : α → M.Config} {initState : α → FiniteState M r} {steps : α → ℕ} (cSteps : NativeCertificate steps ei Turing.MultiTapeTM.encNat) (cCfg : NativeCertificate cfg ei enc.config) (cInit : NativeCertificate initState ei (encoding enc)) (hExec : ∀ (a : α), ∃ m ≤ steps a, Executes (cfg a) p (initState a).denote (f a) m) : NativeCertificate f ei enc.value

Transport a halting generic-RAM execution certificate (GenericRAM.Executes) within steps a instructions to a native multitape Turing-machine certificate for f : α → M.Value. No [Inhabited M.Value] or polynomiality assumption is required.

@[simp]

theorem Cslib.GenericRAM.FiniteState.transportCertificate_time {M : Model} {r : ℕ} {α : Type} {ei : α ↪ List Bool} (enc : M.Encoding) (N : M.NativePrimitives enc) (p : Program M r) {f : α → M.Value} {cfg : α → M.Config} {initState : α → FiniteState M r} {steps : α → ℕ} (cSteps : NativeCertificate steps ei Turing.MultiTapeTM.encNat) (cCfg : NativeCertificate cfg ei enc.config) (cInit : NativeCertificate initState ei (encoding enc)) (hExec : ∀ (a : α), ∃ m ≤ steps a, Executes (cfg a) p (initState a).denote (f a) m) (a : α) : (transportCertificate enc N p cSteps cCfg cInit hExec).time a = cSteps.time a + (cCfg.time a + cInit.time a) + runTime enc N p (steps a, cfg a, initState a)

@[simp]

theorem Cslib.GenericRAM.FiniteState.transportCertificate_space {M : Model} {r : ℕ} {α : Type} {ei : α ↪ List Bool} (enc : M.Encoding) (N : M.NativePrimitives enc) (p : Program M r) {f : α → M.Value} {cfg : α → M.Config} {initState : α → FiniteState M r} {steps : α → ℕ} (cSteps : NativeCertificate steps ei Turing.MultiTapeTM.encNat) (cCfg : NativeCertificate cfg ei enc.config) (cInit : NativeCertificate initState ei (encoding enc)) (hExec : ∀ (a : α), ∃ m ≤ steps a, Executes (cfg a) p (initState a).denote (f a) m) (a : α) : (transportCertificate enc N p cSteps cCfg cInit hExec).space a = cSteps.space a + (cCfg.space a + cInit.space a) + runSpace enc N p (steps a, cfg a, initState a)

theorem Cslib.GenericRAM.FiniteState.transport_inO {M : Model} {r : ℕ} {α : Type} {ei : α ↪ List Bool} (enc : M.Encoding) (N : M.NativePrimitives enc) (p : Program M r) {f : α → M.Value} {cfg : α → M.Config} {initState : α → FiniteState M r} {steps : α → ℕ} (cSteps : NativeCertificate steps ei Turing.MultiTapeTM.encNat) (cCfg : NativeCertificate cfg ei enc.config) (cInit : NativeCertificate initState ei (encoding enc)) (hExec : ∀ (a : α), ∃ m ≤ steps a, Executes (cfg a) p (initState a).denote (f a) m) : Turing.MultiTapeTM.ComputableTidilyInO f ei enc.value (fun (a : α) => cSteps.time a + (cCfg.time a + cInit.time a) + runTime enc N p (steps a, cfg a, initState a)) fun (a : α) => cSteps.space a + (cCfg.space a + cInit.space a) + runSpace enc N p (steps a, cfg a, initState a)

Parameterized ComputableTidilyInO transport theorem from GenericRAM.Executes.

Polynomiality of single steps, rounds, and whole runs

theorem Cslib.GenericRAM.FiniteState.Native.fields_isPolynomial {M : Model} {r : ℕ} {α : Type} {ei : α ↪ List Bool} {s : α → FiniteState M r} (enc : M.Encoding) (c : NativeCertificate s ei (encoding enc)) (hc : c.IsPolynomial) : (fields enc c).IsPolynomial

theorem Cslib.GenericRAM.FiniteState.Native.register_isPolynomial {M : Model} {r : ℕ} {α : Type} {ei : α ↪ List Bool} {s : α → FiniteState M r} (enc : M.Encoding) (c : NativeCertificate s ei (encoding enc)) (i : Fin r) (hc : c.IsPolynomial) : (register enc c i).IsPolynomial

theorem Cslib.GenericRAM.FiniteState.Native.operands_isPolynomial {M : Model} {r : ℕ} {α : Type} {ei : α ↪ List Bool} {s : α → FiniteState M r} (enc : M.Encoding) (c : NativeCertificate s ei (encoding enc)) {n : ℕ} (args : Fin n → Fin r) (hc : c.IsPolynomial) : (operands enc c args).IsPolynomial

theorem Cslib.GenericRAM.FiniteState.Native.setCertificate_isPolynomial {M : Model} {r : ℕ} {α : Type} {ei : α ↪ List Bool} {s : α → FiniteState M r} {v : α → M.Value} (enc : M.Encoding) (c : NativeCertificate s ei (encoding enc)) (d : Fin r) (value : NativeCertificate v ei enc.value) (hc : c.IsPolynomial) (hv : value.IsPolynomial) : (setCertificate enc c d value).IsPolynomial

theorem Cslib.GenericRAM.FiniteState.Native.moveCertificate_isPolynomial {M : Model} {r : ℕ} {α : Type} {ei : α ↪ List Bool} {s : α → FiniteState M r} {k : α → M.Config} {v : α → M.Value} (enc : M.Encoding) (N : M.NativePrimitives enc) (config : NativeCertificate k ei enc.config) (c : NativeCertificate s ei (encoding enc)) (d : Fin r) (value : NativeCertificate v ei enc.value) (hN : N.IsPolynomial) (hk : config.IsPolynomial) (hc : c.IsPolynomial) (hv : value.IsPolynomial) : (moveCertificate enc N config c d value).IsPolynomial

theorem Cslib.GenericRAM.FiniteState.Native.readCertificate_isPolynomial {M : Model} {r : ℕ} {α : Type} {ei : α ↪ List Bool} {s : α → FiniteState M r} (enc : M.Encoding) (c : NativeCertificate s ei (encoding enc)) {a : α → M.Address} (address : NativeCertificate a ei enc.address) (hc : c.IsPolynomial) (ha : address.IsPolynomial) : (readCertificate enc c address).IsPolynomial

theorem Cslib.GenericRAM.FiniteState.Native.writeCertificate_isPolynomial {M : Model} {r : ℕ} {α : Type} {ei : α ↪ List Bool} {s : α → FiniteState M r} {v : α → M.Value} (enc : M.Encoding) (c : NativeCertificate s ei (encoding enc)) {a : α → M.Address} (address : NativeCertificate a ei enc.address) (value : NativeCertificate v ei enc.value) (hc : c.IsPolynomial) (ha : address.IsPolynomial) (hv : value.IsPolynomial) : (writeCertificate enc c address value).IsPolynomial

theorem Cslib.GenericRAM.FiniteState.Native.evalOpCertificate_isPolynomial {M : Model} {r : ℕ} {α : Type} {ei : α ↪ List Bool} {s : α → FiniteState M r} {k : α → M.Config} (enc : M.Encoding) (N : M.NativePrimitives enc) (config : NativeCertificate k ei enc.config) (c : NativeCertificate s ei (encoding enc)) (o : Op M r) (hN : N.IsPolynomial) (hk : config.IsPolynomial) (hc : c.IsPolynomial) : (evalOpCertificate enc N config c o).IsPolynomial

theorem Cslib.GenericRAM.FiniteState.Native.resumeCertificate_isPolynomial {M : Model} {r : ℕ} {α : Type} {ei : α ↪ List Bool} {s : α → FiniteState M r} {k : α → M.Config} (enc : M.Encoding) (N : M.NativePrimitives enc) (config : NativeCertificate k ei enc.config) (c : NativeCertificate s ei (encoding enc)) (pc : ℕ) (hN : N.IsPolynomial) (hk : config.IsPolynomial) (hc : c.IsPolynomial) : (resumeCertificate enc N config c pc).IsPolynomial

theorem Cslib.GenericRAM.FiniteState.Native.evalInstrCertificate_isPolynomial {M : Model} {r : ℕ} {α : Type} {ei : α ↪ List Bool} {s : α → FiniteState M r} {k : α → M.Config} (enc : M.Encoding) (N : M.NativePrimitives enc) (config : NativeCertificate k ei enc.config) (c : NativeCertificate s ei (encoding enc)) (nextPC : ℕ) (i : Instr M r) (hN : N.IsPolynomial) (hk : config.IsPolynomial) (hc : c.IsPolynomial) : (evalInstrCertificate enc N config c nextPC i).IsPolynomial

theorem Cslib.GenericRAM.FiniteState.Native.pcEquals_isPolynomial {M : Model} {r : ℕ} {α : Type} {ei : α ↪ List Bool} {s : α → FiniteState M r} (enc : M.Encoding) (c : NativeCertificate s ei (encoding enc)) (pc : ℕ) (hc : c.IsPolynomial) : (pcEquals enc c pc).IsPolynomial

theorem Cslib.GenericRAM.FiniteState.Native.dispatchCertificate_isPolynomial {M : Model} {r : ℕ} {α : Type} {ei : α ↪ List Bool} {s : α → FiniteState M r} {k : α → M.Config} (enc : M.Encoding) (N : M.NativePrimitives enc) (config : NativeCertificate k ei enc.config) (c : NativeCertificate s ei (encoding enc)) (p : Program M r) (pc : ℕ) (hN : N.IsPolynomial) (hk : config.IsPolynomial) (hc : c.IsPolynomial) : (dispatchCertificate enc N config c p pc).IsPolynomial

theorem Cslib.GenericRAM.FiniteState.stepCertificate_isPolynomial {M : Model} {r : ℕ} (enc : M.Encoding) (N : M.NativePrimitives enc) (p : Program M r) (hN : N.IsPolynomial) : (stepCertificate enc N p).IsPolynomial

When all scalar primitive certificates are polynomial, stepCertificate is polynomial.

theorem Cslib.GenericRAM.FiniteState.step_polyTime {M : Model} {r : ℕ} (enc : M.Encoding) (N : M.NativePrimitives enc) (p : Program M r) (hN : N.IsPolynomial) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (q : M.Config × FiniteState M r) => step q.1 p q.2) (inputEncoding enc) (resultEncoding enc)

When all scalar primitive certificates are polynomial, the encoded single-step transition of any fixed program is tidily computable in polynomial time.

theorem Cslib.GenericRAM.FiniteState.roundCertificate_isPolynomial {M : Model} {r : ℕ} (enc : M.Encoding) (N : M.NativePrimitives enc) (p : Program M r) (hN : N.IsPolynomial) : (roundCertificate enc N p).IsPolynomial

When all scalar primitive certificates are polynomial, roundCertificate is polynomial.

theorem Cslib.GenericRAM.FiniteState.initCertificate_isPolynomial {M : Model} {r : ℕ} {α : Type} {ei : α ↪ List Bool} (enc : M.Encoding) {regsFn : α → Fin r → M.Value} {defaultFn : α → M.Value} {memoryFn : α → SparseMemory M.Address M.Value} (regs : NativeCertificate regsFn ei (Turing.MultiTapeTM.encPi enc.value)) (default : NativeCertificate defaultFn ei enc.value) (memory : NativeCertificate memoryFn ei (SparseMemory.encoding enc.address enc.value)) (hregs : regs.IsPolynomial) (hdef : default.IsPolynomial) (hmem : memory.IsPolynomial) : (initCertificate enc regs default memory).IsPolynomial

theorem Cslib.GenericRAM.FiniteState.constRegsCertificate_isPolynomial {M : Model} {r : ℕ} {α : Type} {ei : α ↪ List Bool} (enc : M.Encoding) {initRegFn : α → M.Value} (initReg : NativeCertificate initRegFn ei enc.value) (hreg : initReg.IsPolynomial) : (constRegsCertificate enc initReg).IsPolynomial

theorem Cslib.GenericRAM.FiniteState.initConstCertificate_isPolynomial {M : Model} {r : ℕ} {α : Type} {ei : α ↪ List Bool} (enc : M.Encoding) {initRegFn defaultFn : α → M.Value} {memoryFn : α → SparseMemory M.Address M.Value} (initReg : NativeCertificate initRegFn ei enc.value) (default : NativeCertificate defaultFn ei enc.value) (memory : NativeCertificate memoryFn ei (SparseMemory.encoding enc.address enc.value)) (hreg : initReg.IsPolynomial) (hdef : default.IsPolynomial) (hmem : memory.IsPolynomial) : (initConstCertificate enc initReg default memory).IsPolynomial

theorem Cslib.GenericRAM.FiniteState.transportCertificate_isPolynomial {M : Model} {r : ℕ} {α : Type} {ei : α ↪ List Bool} (enc : M.Encoding) (N : M.NativePrimitives enc) (p : Program M r) {f : α → M.Value} {cfg : α → M.Config} {initState : α → FiniteState M r} {steps : α → ℕ} (cSteps : NativeCertificate steps ei Turing.MultiTapeTM.encNat) (cCfg : NativeCertificate cfg ei enc.config) (cInit : NativeCertificate initState ei (encoding enc)) (hExec : ∀ (a : α), ∃ m ≤ steps a, Executes (cfg a) p (initState a).denote (f a) m) (hN : N.IsPolynomial) (hSteps : cSteps.IsPolynomial) (hCfg : cCfg.IsPolynomial) (hInit : cInit.IsPolynomial) (hStepsBound : Turing.MultiTapeTM.PolyBounded (fun (a : α) => (ei a).length) steps) {B : α → ℕ} (hB : Turing.MultiTapeTM.PolyBounded (fun (a : α) => (ei a).length) B) (hOutLen : ∀ (a : α), ∀ j ≤ steps a, ((resultEncoding enc) (run (cfg a) p j (initState a))).length ≤ B a) : (transportCertificate enc N p cSteps cCfg cInit hExec).IsPolynomial

Polynomial-time whole-run transport: if scalar primitives, step-budget certificate, configuration certificate, and initial-state certificate are polynomial, the step budget steps a is polynomially bounded, and the encoded outcomes along 0 ≤ j ≤ steps a are bounded by a polynomially bounded function B, then the transported certificate is polynomial.

theorem Cslib.GenericRAM.FiniteState.transport_polyTime {M : Model} {r : ℕ} {α : Type} {ei : α ↪ List Bool} (enc : M.Encoding) (N : M.NativePrimitives enc) (p : Program M r) {f : α → M.Value} {cfg : α → M.Config} {initState : α → FiniteState M r} {steps : α → ℕ} (cSteps : NativeCertificate steps ei Turing.MultiTapeTM.encNat) (cCfg : NativeCertificate cfg ei enc.config) (cInit : NativeCertificate initState ei (encoding enc)) (hExec : ∀ (a : α), ∃ m ≤ steps a, Executes (cfg a) p (initState a).denote (f a) m) (hN : N.IsPolynomial) (hSteps : cSteps.IsPolynomial) (hCfg : cCfg.IsPolynomial) (hInit : cInit.IsPolynomial) (hStepsBound : Turing.MultiTapeTM.PolyBounded (fun (a : α) => (ei a).length) steps) {B : α → ℕ} (hB : Turing.MultiTapeTM.PolyBounded (fun (a : α) => (ei a).length) B) (hOutLen : ∀ (a : α), ∀ j ≤ steps a, ((resultEncoding enc) (run (cfg a) p j (initState a))).length ≤ B a) : Turing.MultiTapeTM.ComputableTidilyInPolyTime f ei enc.value

Automatic ComputableTidilyInPolyTime transport corollary from GenericRAM.Executes.

def Cslib.GenericRAM.FiniteState.roundIterCertificate {M : Model} {r : ℕ} {α : Type} {ei : α ↪ List Bool} (enc : M.Encoding) (N : M.NativePrimitives enc) (p : Program M r) {cfg : α → M.Config} {initState : α → FiniteState M r} (cCfg : NativeCertificate cfg ei enc.config) (cInit : NativeCertificate initState ei (encoding enc)) (j : ℕ) : NativeCertificate (fun (a : α) => (round p)^[j] (cfg a, some (Sum.inl (initState a)))) ei (loopEncoding enc)

Iterating roundCertificate a fixed number of rounds j yields a certificate for the j-th loop state.

theorem Cslib.GenericRAM.FiniteState.roundIterCertificate_isPolynomial {M : Model} {r : ℕ} {α : Type} {ei : α ↪ List Bool} (enc : M.Encoding) (N : M.NativePrimitives enc) (p : Program M r) {cfg : α → M.Config} {initState : α → FiniteState M r} (cCfg : NativeCertificate cfg ei enc.config) (cInit : NativeCertificate initState ei (encoding enc)) (hN : N.IsPolynomial) (hCfg : cCfg.IsPolynomial) (hInit : cInit.IsPolynomial) (j : ℕ) : (roundIterCertificate enc N p cCfg cInit j).IsPolynomial

theorem Cslib.GenericRAM.FiniteState.polyBounded_length_run {M : Model} {r : ℕ} {α : Type} {ei : α ↪ List Bool} (enc : M.Encoding) (N : M.NativePrimitives enc) (p : Program M r) {cfg : α → M.Config} {initState : α → FiniteState M r} (cCfg : NativeCertificate cfg ei enc.config) (cInit : NativeCertificate initState ei (encoding enc)) (hN : N.IsPolynomial) (hCfg : cCfg.IsPolynomial) (hInit : cInit.IsPolynomial) (j : ℕ) : Turing.MultiTapeTM.PolyBounded (fun (a : α) => (ei a).length) fun (a : α) => ((resultEncoding enc) (run (cfg a) p j (initState a))).length

theorem Cslib.GenericRAM.FiniteState.transport_polyTime_of_le_const {M : Model} {r : ℕ} {α : Type} {ei : α ↪ List Bool} (enc : M.Encoding) (N : M.NativePrimitives enc) (p : Program M r) {f : α → M.Value} {cfg : α → M.Config} {initState : α → FiniteState M r} {steps : α → ℕ} (cSteps : NativeCertificate steps ei Turing.MultiTapeTM.encNat) (cCfg : NativeCertificate cfg ei enc.config) (cInit : NativeCertificate initState ei (encoding enc)) (hExec : ∀ (a : α), ∃ m ≤ steps a, Executes (cfg a) p (initState a).denote (f a) m) (hN : N.IsPolynomial) (hSteps : cSteps.IsPolynomial) (hCfg : cCfg.IsPolynomial) (hInit : cInit.IsPolynomial) (K : ℕ) (hStepsLe : ∀ (a : α), steps a ≤ K) : Turing.MultiTapeTM.ComputableTidilyInPolyTime f ei enc.value

Automatic ComputableTidilyInPolyTime transport for a constant step-budget bound ∀ a, steps a ≤ K: the intermediate outcome lengths along 0 ≤ j ≤ K are bounded by induction on K using roundCertificate_isPolynomial.