Native implementation of fixed-program finite RAM steps

The input contains configuration and the complete finite state, including the memory default. All encodings are injective representations of finite data, rather than of the denoted total memory function. Native certificates are assembled directly from arbitrary scalar time/space bounds, fixed tuple manipulation and parameterized sparse-memory scans. No polynomiality premise or selection of polynomial bounds is used.

For each fixed program and register count, the resulting finite native machine works on every encoded input. Constants may depend on that fixed program; this is not an arbitrary-program interpreter. Initialization, iteration, output decoding and charged configuration selection remain separate obligations.

Main definitions

• FiniteState.encoding: binary control label, complete register tuple, default and sparse store.
• FiniteState.inputEncoding, FiniteState.resultEncoding: explicit step interface.
• FiniteState.stepCertificate, FiniteState.stepTime, FiniteState.stepSpace: native fixed-program step implementation and its parameterized time and space bounds.
• FiniteState.opTime, .opSpace, .instrTime, .instrSpace, .dispatchTime, .dispatchSpace: component cost profiles decomposed across operations, instructions, and program dispatch.

Main results

• FiniteState.length_encoding, FiniteState.length_encoding_le: encoded finite-state length formula and upper bound in terms of register count, register word bound, default length, and stored-cell count.
• FiniteState.step_inO: one finite native machine implements FiniteState.step for all runtime configurations and finite states within stepTime and stepSpace.
• FiniteState.stepTime_eq, FiniteState.stepSpace_eq, FiniteState.dispatchTime_nil, FiniteState.dispatchTime_cons, FiniteState.dispatchSpace_nil, FiniteState.dispatchSpace_cons: public cost recurrences.
• FiniteState.le_opTime_const, FiniteState.le_opTime_alu, FiniteState.le_opTime_load, FiniteState.le_opTime_store, FiniteState.le_instrTime_op: retention of supplied scalar and sparse-memory resource bounds.

References

Reuses Christian Reitwiessner's native machine calculus and the certified scalar/sparse-memory interfaces; finite-state semantics is defined in Simulation.Finite.

noncomputable def Cslib.GenericRAM.FiniteState.encoding {M : Model} {r : ℕ} (enc : M.Encoding) : FiniteState M r ↪ List Bool

Encode all finite state components, including the default and distinct stored bindings.

@[simp]

theorem Cslib.GenericRAM.FiniteState.encoding_apply {M : Model} {r : ℕ} (enc : M.Encoding) (s : FiniteState M r) : (encoding enc) s = (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPi enc.value) (Turing.MultiTapeTM.encPair enc.value (SparseMemory.encoding enc.address enc.value)))) (s.pc, s.regs, s.default, s.memory)

@[reducible, inline]

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

Configuration is a runtime input, alongside the complete finite state.

@[reducible, inline]

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

Fault, continuing state and halted value have distinct tags.

theorem Cslib.GenericRAM.FiniteState.length_encoding {M : Model} {r : ℕ} (enc : M.Encoding) (s : FiniteState M r) : ((encoding enc) s).length = 2 * (Turing.MultiTapeTM.encNat s.pc).length + 2 * ((Turing.MultiTapeTM.encPi enc.value) s.regs).length + 2 * (enc.value s.default).length + ((SparseMemory.encoding enc.address enc.value) s.memory).length + 3

Exact bit length of an encoded finite state in terms of its four encoded fields.

theorem Cslib.GenericRAM.FiniteState.length_encoding_le {M : Model} {r : ℕ} (enc : M.Encoding) (s : FiniteState M r) {bound : ℕ} (hregs : ∀ (i : Fin r), (enc.value (s.regs i)).length ≤ bound) : ((encoding enc) s).length ≤ 2 * (Turing.MultiTapeTM.encNat s.pc).length + 2 * r * (2 * bound + 1) + 2 * (enc.value s.default).length + s.memory.entries.length * (4 * SparseMemory.maxKeyLength enc.address s.memory + 2 * SparseMemory.maxValueLength enc.value s.memory + 3) + 3

Bound the encoded finite state from the control label, register bound, default, and store.

@[reducible, inline]

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

The nested tuple representation underlying the finite-state encoding.

noncomputable def Cslib.GenericRAM.FiniteState.Native.unpack {M : Model} {r : ℕ} (enc : M.Encoding) : NativeCertificate (fun (s : FiniteState M r) => (s.pc, s.regs, s.default, s.memory)) (encoding enc) (tupleEncoding enc)

Expose the state fields with exactly the same encoded word.

noncomputable def Cslib.GenericRAM.FiniteState.Native.pack {M : Model} {r : ℕ} (enc : M.Encoding) : NativeCertificate (fun (p : ℕ × (Fin r → M.Value) × M.Value × SparseMemory M.Address M.Value) => { pc := p.1, regs := p.2.1, default := p.2.2.1, memory := p.2.2.2 }) (tupleEncoding enc) (encoding enc)

Construct the state from its identically encoded field tuple.

noncomputable def Cslib.GenericRAM.FiniteState.Native.fields {M : Model} {r : ℕ} {α : Type} {ei : α ↪ List Bool} {s : α → FiniteState M r} (enc : M.Encoding) (c : NativeCertificate s ei (encoding enc)) : NativeCertificate ((fun (s : FiniteState M r) => (s.pc, s.regs, s.default, s.memory)) ∘ s) ei (tupleEncoding enc)

Expose a produced state as its nested field tuple without extra asymptotic cost.

@[simp]

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

@[simp]

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

noncomputable def Cslib.GenericRAM.FiniteState.Native.register {M : Model} {r : ℕ} {α : Type} {ei : α ↪ List Bool} {s : α → FiniteState M r} (enc : M.Encoding) (c : NativeCertificate s ei (encoding enc)) (i : Fin r) : NativeCertificate (fun (a : α) => (s a).regs i) ei enc.value

Read a fixed register, using the complete tuple input-length guarantee.

@[simp]

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

@[simp]

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

noncomputable def Cslib.GenericRAM.FiniteState.Native.operands {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) : NativeCertificate (fun (a : α) => (s a).regs ∘ args) ei (Turing.MultiTapeTM.encPi enc.value)

Gather a fixed tuple of operand registers, permitting repeated indices.

@[simp]

theorem Cslib.GenericRAM.FiniteState.Native.operands_time {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) : (operands enc c args).time = c.time

@[simp]

theorem Cslib.GenericRAM.FiniteState.Native.operands_space {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) : (operands enc c args).space = c.space

noncomputable def Cslib.GenericRAM.FiniteState.Native.setCertificate {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) : NativeCertificate (fun (a : α) => (s a).set d (v a)) ei (encoding enc)

Update a fixed register and retain all other state fields.

@[simp]

theorem Cslib.GenericRAM.FiniteState.Native.setCertificate_time {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) (a : α) : (setCertificate enc c d value).time a = c.time a + (c.time a + value.time a + c.time a)

@[simp]

theorem Cslib.GenericRAM.FiniteState.Native.setCertificate_space {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) (a : α) : (setCertificate enc c d value).space a = c.space a + (c.space a + value.space a + c.space a)

noncomputable def Cslib.GenericRAM.FiniteState.Native.moveCertificate {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) : NativeCertificate (fun (a : α) => move (k a) (s a) d (v a)) ei (Turing.MultiTapeTM.encOption (encoding enc))

Validate a moved value before updating a fixed register.

@[simp]

theorem Cslib.GenericRAM.FiniteState.Native.moveCertificate_time {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) (a : α) : (moveCertificate enc N config c d value).time a = config.time a + value.time a + N.validMove.time (k a, v a) + if M.validMove (k a) (v a) = true then (setCertificate enc c d value).time a else (ei a).length

@[simp]

theorem Cslib.GenericRAM.FiniteState.Native.moveCertificate_space {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) (a : α) : (moveCertificate enc N config c d value).space a = config.space a + value.space a + N.validMove.space (k a, v a) + if M.validMove (k a) (v a) = true then (setCertificate enc c d value).space a else (ei a).length

noncomputable def Cslib.GenericRAM.FiniteState.Native.readCertificate {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) : NativeCertificate (fun (x : α) => SparseMemory.read (s x).default (a x) (s x).memory) ei enc.value

Read sparse memory, with the parameterized scan bound and explicit default.

@[simp]

theorem Cslib.GenericRAM.FiniteState.Native.readCertificate_time {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) (x : α) : (readCertificate enc c address).time x = address.time x + c.time x + c.time x + SparseMemory.readTime enc.address enc.value ((a x, (s x).memory), (s x).default)

@[simp]

theorem Cslib.GenericRAM.FiniteState.Native.readCertificate_space {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) (x : α) : (readCertificate enc c address).space x = address.space x + c.space x + c.space x + SparseMemory.readSpace enc.address enc.value ((a x, (s x).memory), (s x).default)

noncomputable def Cslib.GenericRAM.FiniteState.Native.writeCertificate {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) : NativeCertificate (fun (x : α) => (s x).write (a x) (v x)) ei (encoding enc)

Write sparse memory, with the parameterized scan bound and complete retained state.

@[simp]

theorem Cslib.GenericRAM.FiniteState.Native.writeCertificate_time {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) (x : α) : (writeCertificate enc c address value).time x = c.time x + (c.time x + (c.time x + (address.time x + value.time x + c.time x + SparseMemory.writeTime enc.address enc.value ((a x, v x), (s x).memory))))

@[simp]

theorem Cslib.GenericRAM.FiniteState.Native.writeCertificate_space {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) (x : α) : (writeCertificate enc c address value).space x = c.space x + (c.space x + (c.space x + (address.space x + value.space x + c.space x + SparseMemory.writeSpace enc.address enc.value ((a x, v x), (s x).memory))))

noncomputable def Cslib.GenericRAM.FiniteState.Native.evalOpCertificate {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) : NativeCertificate (fun (a : α) => evalOp (k a) o (s a)) ei (Turing.MultiTapeTM.encOption (encoding enc))

Implement one fixed operation from scalar, tuple and sparse-memory certificates.

noncomputable def Cslib.GenericRAM.FiniteState.Native.resumeCertificate {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 : ℕ) : NativeCertificate (fun (a : α) => resume (k a) pc (s a)) ei (resultEncoding enc)

Validate a fixed continuing label and emit the updated state.

noncomputable def Cslib.GenericRAM.FiniteState.Native.evalInstrCertificate {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) : NativeCertificate (fun (a : α) => evalInstr (k a) nextPC i (s a)) ei (resultEncoding enc)

Implement a fixed instruction, charging only the selected outcome branches.

noncomputable def Cslib.GenericRAM.FiniteState.Native.pcEquals {M : Model} {r : ℕ} {α : Type} {ei : α ↪ List Bool} {s : α → FiniteState M r} (enc : M.Encoding) (c : NativeCertificate s ei (encoding enc)) (pc : ℕ) : NativeCertificate (fun (a : α) => decide ((s a).pc = pc)) ei Turing.MultiTapeTM.encBool

Compare the current binary control label to a fixed label using native word comparison.

def Cslib.GenericRAM.FiniteState.Native.dispatchCertificate {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 : ℕ) : NativeCertificate (fun (a : α) => dispatch (k a) p pc (s a)) ei (resultEncoding enc)

Dispatch a fixed program by comparisons, charging each preceding rejected label.

noncomputable def Cslib.GenericRAM.FiniteState.Native.configInput {M : Model} {r : ℕ} (enc : M.Encoding) : NativeCertificate Prod.fst (inputEncoding enc) enc.config

Top-level runtime configuration projection from the step input.

@[simp]

theorem Cslib.GenericRAM.FiniteState.Native.configInput_time {M : Model} {r : ℕ} (enc : M.Encoding) (q : M.Config × FiniteState M r) : (configInput enc).time q = ((inputEncoding enc) q).length

@[simp]

theorem Cslib.GenericRAM.FiniteState.Native.configInput_space {M : Model} {r : ℕ} (enc : M.Encoding) (q : M.Config × FiniteState M r) : (configInput enc).space q = ((inputEncoding enc) q).length

noncomputable def Cslib.GenericRAM.FiniteState.Native.stateInput {M : Model} {r : ℕ} (enc : M.Encoding) : NativeCertificate Prod.snd (inputEncoding enc) (encoding enc)

Top-level finite-state projection from the step input.

@[simp]

theorem Cslib.GenericRAM.FiniteState.Native.stateInput_time {M : Model} {r : ℕ} (enc : M.Encoding) (q : M.Config × FiniteState M r) : (stateInput enc).time q = ((inputEncoding enc) q).length

@[simp]

theorem Cslib.GenericRAM.FiniteState.Native.stateInput_space {M : Model} {r : ℕ} (enc : M.Encoding) (q : M.Config × FiniteState M r) : (stateInput enc).space q = ((inputEncoding enc) q).length

noncomputable def Cslib.GenericRAM.FiniteState.Native.opCertificate {M : Model} {r : ℕ} (enc : M.Encoding) (N : M.NativePrimitives enc) (o : Op M r) : NativeCertificate (fun (q : M.Config × FiniteState M r) => evalOp q.1 o q.2) (inputEncoding enc) (Turing.MultiTapeTM.encOption (encoding enc))

Top-level operation certificate on the step input encoding.

noncomputable def Cslib.GenericRAM.FiniteState.Native.instrCertificate {M : Model} {r : ℕ} (enc : M.Encoding) (N : M.NativePrimitives enc) (nextPC : ℕ) (i : Instr M r) : NativeCertificate (fun (q : M.Config × FiniteState M r) => evalInstr q.1 nextPC i q.2) (inputEncoding enc) (resultEncoding enc)

Top-level instruction certificate on the step input encoding.

noncomputable def Cslib.GenericRAM.FiniteState.Native.programCertificate {M : Model} {r : ℕ} (enc : M.Encoding) (N : M.NativePrimitives enc) (p : Program M r) (pc : ℕ) : NativeCertificate (fun (q : M.Config × FiniteState M r) => dispatch q.1 p pc q.2) (inputEncoding enc) (resultEncoding enc)

Top-level dispatch certificate on the step input encoding.

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

A native finite machine for a fixed program, uniform in runtime configuration and state.

The certificate's bounds are constructed by sums, selected branches and substitution into the supplied scalar and sparse-memory bounds. Linear tuple manipulation is charged by input length or absorbed by a producer's output-length guarantee. Fixed control-label equality uses the native encoded comparison bound. No polynomial bound is selected by this construction.

noncomputable def Cslib.GenericRAM.FiniteState.opTime {M : Model} {r : ℕ} (enc : M.Encoding) (N : M.NativePrimitives enc) (o : Op M r) : M.Config × FiniteState M r → ℕ

Parameterized operation time on the step input encoding.

noncomputable def Cslib.GenericRAM.FiniteState.opSpace {M : Model} {r : ℕ} (enc : M.Encoding) (N : M.NativePrimitives enc) (o : Op M r) : M.Config × FiniteState M r → ℕ

Parameterized operation space on the step input encoding.

noncomputable def Cslib.GenericRAM.FiniteState.instrTime {M : Model} {r : ℕ} (enc : M.Encoding) (N : M.NativePrimitives enc) (nextPC : ℕ) (i : Instr M r) : M.Config × FiniteState M r → ℕ

Parameterized instruction time on the step input encoding.

noncomputable def Cslib.GenericRAM.FiniteState.instrSpace {M : Model} {r : ℕ} (enc : M.Encoding) (N : M.NativePrimitives enc) (nextPC : ℕ) (i : Instr M r) : M.Config × FiniteState M r → ℕ

Parameterized instruction space on the step input encoding.

noncomputable def Cslib.GenericRAM.FiniteState.pcEqualsTime {M : Model} {r : ℕ} (enc : M.Encoding) (pc : ℕ) : M.Config × FiniteState M r → ℕ

Time charged by comparing the current control label against a fixed instruction offset.

noncomputable def Cslib.GenericRAM.FiniteState.pcEqualsSpace {M : Model} {r : ℕ} (enc : M.Encoding) (pc : ℕ) : M.Config × FiniteState M r → ℕ

Space charged by comparing the current control label against a fixed instruction offset.

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

Parameterized dispatch time from instruction offset pc.

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

Parameterized dispatch space from instruction offset pc.

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

Parameterized step time, obtained by explicit compositional accounting, not a chosen polynomial. In particular it retains the time bounds supplied by N and sparse-memory scans.

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

Parameterized step space, also bounding the encoded output up to constants.

theorem Cslib.GenericRAM.FiniteState.step_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) => step q.1 p q.2) (inputEncoding enc) (resultEncoding enc) (stepTime enc N p) (stepSpace enc N p)

The actual native implementation satisfies the explicitly assembled time and space bounds. The existential machine and constant are outside the quantifier over all configurations/states; they may depend on the fixed program and register count.

@[simp]

theorem Cslib.GenericRAM.FiniteState.dispatchTime_nil {M : Model} {r : ℕ} (enc : M.Encoding) (N : M.NativePrimitives enc) (pc : ℕ) (q : M.Config × FiniteState M r) : dispatchTime enc N [] pc q = ((inputEncoding enc) q).length

@[simp]

theorem Cslib.GenericRAM.FiniteState.dispatchSpace_nil {M : Model} {r : ℕ} (enc : M.Encoding) (N : M.NativePrimitives enc) (pc : ℕ) (q : M.Config × FiniteState M r) : dispatchSpace enc N [] pc q = ((inputEncoding enc) q).length

@[simp]

theorem Cslib.GenericRAM.FiniteState.dispatchTime_cons {M : Model} {r : ℕ} (enc : M.Encoding) (N : M.NativePrimitives enc) (i : Instr M r) (p : Program M r) (pc : ℕ) (q : M.Config × FiniteState M r) : dispatchTime enc N (i :: p) pc q = pcEqualsTime enc pc q + if q.2.pc = pc then instrTime enc N (pc + 1) i q else dispatchTime enc N p (pc + 1) q

@[simp]

theorem Cslib.GenericRAM.FiniteState.dispatchSpace_cons {M : Model} {r : ℕ} (enc : M.Encoding) (N : M.NativePrimitives enc) (i : Instr M r) (p : Program M r) (pc : ℕ) (q : M.Config × FiniteState M r) : dispatchSpace enc N (i :: p) pc q = pcEqualsSpace enc pc q + if q.2.pc = pc then instrSpace enc N (pc + 1) i q else dispatchSpace enc N p (pc + 1) q

theorem Cslib.GenericRAM.FiniteState.stepTime_eq {M : Model} {r : ℕ} (enc : M.Encoding) (N : M.NativePrimitives enc) (p : Program M r) (q : M.Config × FiniteState M r) : stepTime enc N p q = 2 * ((inputEncoding enc) q).length + N.validPC.time (q.1, q.2.pc) + if M.validPC q.1 q.2.pc = true then dispatchTime enc N p 0 q else ((inputEncoding enc) q).length

Exact decomposition of stepTime into current-label validation and selected branch cost.

theorem Cslib.GenericRAM.FiniteState.stepSpace_eq {M : Model} {r : ℕ} (enc : M.Encoding) (N : M.NativePrimitives enc) (p : Program M r) (q : M.Config × FiniteState M r) : stepSpace enc N p q = 2 * ((inputEncoding enc) q).length + N.validPC.space (q.1, q.2.pc) + if M.validPC q.1 q.2.pc = true then dispatchSpace enc N p 0 q else ((inputEncoding enc) q).length

Exact decomposition of stepSpace into current-label validation and selected branch cost.

theorem Cslib.GenericRAM.FiniteState.stepTime_nil {M : Model} {r : ℕ} (enc : M.Encoding) (N : M.NativePrimitives enc) (q : M.Config × FiniteState M r) : stepTime enc N [] q = 3 * ((inputEncoding enc) q).length + N.validPC.time (q.1, q.2.pc)

Step time on the empty program.

theorem Cslib.GenericRAM.FiniteState.stepSpace_nil {M : Model} {r : ℕ} (enc : M.Encoding) (N : M.NativePrimitives enc) (q : M.Config × FiniteState M r) : stepSpace enc N [] q = 3 * ((inputEncoding enc) q).length + N.validPC.space (q.1, q.2.pc)

Step space on the empty program.

theorem Cslib.GenericRAM.FiniteState.stepTime_cons {M : Model} {r : ℕ} (enc : M.Encoding) (N : M.NativePrimitives enc) (i : Instr M r) (p : Program M r) (q : M.Config × FiniteState M r) : stepTime enc N (i :: p) q = 2 * ((inputEncoding enc) q).length + N.validPC.time (q.1, q.2.pc) + if M.validPC q.1 q.2.pc = true then pcEqualsTime enc 0 q + if q.2.pc = 0 then instrTime enc N 1 i q else dispatchTime enc N p 1 q else ((inputEncoding enc) q).length

Step time recurrence on a non-empty program.

theorem Cslib.GenericRAM.FiniteState.stepSpace_cons {M : Model} {r : ℕ} (enc : M.Encoding) (N : M.NativePrimitives enc) (i : Instr M r) (p : Program M r) (q : M.Config × FiniteState M r) : stepSpace enc N (i :: p) q = 2 * ((inputEncoding enc) q).length + N.validPC.space (q.1, q.2.pc) + if M.validPC q.1 q.2.pc = true then pcEqualsSpace enc 0 q + if q.2.pc = 0 then instrSpace enc N 1 i q else dispatchSpace enc N p 1 q else ((inputEncoding enc) q).length

Step space recurrence on a non-empty program.

theorem Cslib.GenericRAM.FiniteState.le_opTime_const {M : Model} {r : ℕ} (enc : M.Encoding) (N : M.NativePrimitives enc) (d : Fin r) (literal : M.Const) (q : M.Config × FiniteState M r) : (N.constant literal).time q.1 ≤ opTime enc N (Op.const d literal) q

Literal operations retain the supplied constant-certificate time bound.

theorem Cslib.GenericRAM.FiniteState.le_opSpace_const {M : Model} {r : ℕ} (enc : M.Encoding) (N : M.NativePrimitives enc) (d : Fin r) (literal : M.Const) (q : M.Config × FiniteState M r) : (N.constant literal).space q.1 ≤ opSpace enc N (Op.const d literal) q

Literal operations retain the supplied constant-certificate space bound.

theorem Cslib.GenericRAM.FiniteState.le_opTime_alu {M : Model} {r : ℕ} (enc : M.Encoding) (N : M.NativePrimitives enc) (op : M.operations.Op) (d : Fin r) (args : Fin (M.operations.Arity op) → Fin r) (q : M.Config × FiniteState M r) : (N.operation op).time (q.1, q.2.regs ∘ args) ≤ opTime enc N (Op.alu op d args) q

ALU operations retain the supplied operation-certificate time bound.

theorem Cslib.GenericRAM.FiniteState.le_opSpace_alu {M : Model} {r : ℕ} (enc : M.Encoding) (N : M.NativePrimitives enc) (op : M.operations.Op) (d : Fin r) (args : Fin (M.operations.Arity op) → Fin r) (q : M.Config × FiniteState M r) : (N.operation op).space (q.1, q.2.regs ∘ args) ≤ opSpace enc N (Op.alu op d args) q

ALU operations retain the supplied operation-certificate space bound.

theorem Cslib.GenericRAM.FiniteState.le_opTime_load {M : Model} {r : ℕ} (enc : M.Encoding) (N : M.NativePrimitives enc) (d a : Fin r) (q : M.Config × FiniteState M r) (addr : M.Address) (ha : M.address q.1 (q.2.regs a) = some addr) : SparseMemory.readTime enc.address enc.value ((addr, q.2.memory), q.2.default) ≤ opTime enc N (Op.load d a) q

Load operations retain the parameterized sparse-memory read time when the address succeeds.

theorem Cslib.GenericRAM.FiniteState.le_opSpace_load {M : Model} {r : ℕ} (enc : M.Encoding) (N : M.NativePrimitives enc) (d a : Fin r) (q : M.Config × FiniteState M r) (addr : M.Address) (ha : M.address q.1 (q.2.regs a) = some addr) : SparseMemory.readSpace enc.address enc.value ((addr, q.2.memory), q.2.default) ≤ opSpace enc N (Op.load d a) q

Load operations retain the parameterized sparse-memory read space when the address succeeds.

theorem Cslib.GenericRAM.FiniteState.le_opTime_store {M : Model} {r : ℕ} (enc : M.Encoding) (N : M.NativePrimitives enc) (a src : Fin r) (q : M.Config × FiniteState M r) (addr : M.Address) (ha : M.address q.1 (q.2.regs a) = some addr) (hm : M.validMove q.1 (q.2.regs src) = true) : SparseMemory.writeTime enc.address enc.value ((addr, q.2.regs src), q.2.memory) ≤ opTime enc N (Op.store a src) q

Store operations retain the parameterized sparse-memory write time on valid stores.

theorem Cslib.GenericRAM.FiniteState.le_opSpace_store {M : Model} {r : ℕ} (enc : M.Encoding) (N : M.NativePrimitives enc) (a src : Fin r) (q : M.Config × FiniteState M r) (addr : M.Address) (ha : M.address q.1 (q.2.regs a) = some addr) (hm : M.validMove q.1 (q.2.regs src) = true) : SparseMemory.writeSpace enc.address enc.value ((addr, q.2.regs src), q.2.memory) ≤ opSpace enc N (Op.store a src) q

Store operations retain the parameterized sparse-memory write space on valid stores.

theorem Cslib.GenericRAM.FiniteState.le_instrTime_op {M : Model} {r : ℕ} (enc : M.Encoding) (N : M.NativePrimitives enc) (nextPC : ℕ) (o : Op M r) (q : M.Config × FiniteState M r) : opTime enc N o q ≤ instrTime enc N nextPC (Instr.op o) q

Data instructions retain their operation time bound.

theorem Cslib.GenericRAM.FiniteState.le_instrSpace_op {M : Model} {r : ℕ} (enc : M.Encoding) (N : M.NativePrimitives enc) (nextPC : ℕ) (o : Op M r) (q : M.Config × FiniteState M r) : opSpace enc N o q ≤ instrSpace enc N nextPC (Instr.op o) q

Data instructions retain their operation space bound.