Native certificates for RAM primitives

A NativeCertificate records arbitrary input-dependent time and space bounds, including the encoded output size, for an actual finite native multi-tape machine. Model.NativePrimitives collects these certificates for the scalar obligations of a RAM model. Configuration and all operands are encoded runtime inputs; a single machine handles all of them for each fixed symbol. Constants may depend on the symbol, and hence on a fixed finite source program. Symbols themselves are not encoded inputs: this is not a uniform interpreter for arbitrary programs.

The semantic Model remains independent of finite encodings. In particular, this interface does not require an exact real RAM to admit a bit representation. It also supplies neither a memory representation nor a whole-machine simulation. Loads/stores still require charged lookup/update; control, initialization and output require their own certificates. Deriving an input-only bound from a configuration-and-input bound additionally requires charged, computable configuration selection and an input-fit guarantee, rather than instance-dependent width advice.

Main definitions

• NativeCertificate: native implementation with arbitrary resource bounds.
• Model.Encoding: selectable encodings of values, addresses and configuration.
• Model.checkedConstant, Model.checkedOp: include the result admissibility check.
• Model.NativePrimitives, Model.NativePrimitives.IsPolynomial: scalar obligations, including move and control-label validation, and their polynomiality predicate.

Main results

• NativeCertificate.nonempty_iff_isComputable: arbitrary-bound certificates exist exactly for native computable functions.
• NativeCertificate.isComputable: forget the resource bounds.
• NativeCertificate.polyTime: obtain polynomial time under separate polynomial bounds.
• NativeCertificate.comp: compose certificates with input-dependent resource accounting.

References

• M. Sipser, Introduction to the Theory of Computation

structure Cslib.GenericRAM.NativeCertificate {α β : Type} (f : α → β) (encIn : α ↪ List Bool) (encOut : β ↪ List Bool) : Type

An actual native implementation, with bounds also charging its encoded output length.

• time : α → ℕ

  Input-dependent time bound, up to a constant factor and additive constant.

• space : α → ℕ

  Input-dependent work space and encoded output bound, up to constants.

• computes : Turing.MultiTapeTM.ComputableTidilyInO f encIn encOut self.time self.space

  One finite machine implements the function on every encoded input.

theorem Cslib.GenericRAM.NativeCertificate.isComputable {α β : Type} {f : α → β} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} (c : NativeCertificate f encIn encMid) : Turing.MultiTapeTM.IsComputable f encIn encMid

Forgetting resource bounds retains native computability.

def Cslib.GenericRAM.NativeCertificate.IsPolynomial {α β : Type} {f : α → β} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} (c : NativeCertificate f encIn encMid) : Prop

Polynomiality is a separate property of both bounds in the encoded input length.

theorem Cslib.GenericRAM.NativeCertificate.polyTime {α β : Type} {f : α → β} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} (c : NativeCertificate f encIn encMid) (h : c.IsPolynomial) : Turing.MultiTapeTM.ComputableTidilyInPolyTime f encIn encMid

Derive the existing native polynomial-time predicate, for use by its compositional calculus.

def Cslib.GenericRAM.NativeCertificate.comp {α β γ : Type} {f : α → β} {g : β → γ} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {encOut : γ ↪ List Bool} (d : NativeCertificate g encMid encOut) (c : NativeCertificate f encIn encMid) : NativeCertificate (g ∘ f) encIn encOut

Compose implementations, charging the second bound at the first result.

theorem Cslib.GenericRAM.NativeCertificate.comp_isPolynomial {α β γ : Type} {f : α → β} {g : β → γ} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {encOut : γ ↪ List Bool} (d : NativeCertificate g encMid encOut) (c : NativeCertificate f encIn encMid) (hd : d.IsPolynomial) (hc : c.IsPolynomial) : (d.comp c).IsPolynomial

Composing polynomial certificates preserves polynomiality in the original input encoding.

def Cslib.GenericRAM.NativeCertificate.ofTimeAndSpace {α β : Type} {f : α → β} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {t s : α → ℕ} (h : Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace f encIn encMid t s) : NativeCertificate f encIn encMid

Package exact native bounds, including the running time in the space allowance to charge encoded output length. No polynomial hypothesis is needed.

theorem Cslib.GenericRAM.NativeCertificate.nonempty_iff_isComputable {α β : Type} {f : α → β} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} : Nonempty (NativeCertificate f encIn encMid) ↔ Turing.MultiTapeTM.IsComputable f encIn encMid

Arbitrary-bound certificates impose exactly native computability, not an efficiency assumption. Polynomial resource bounds remain a separate property.

theorem Cslib.GenericRAM.NativeCertificate.exists_polynomial {α β : Type} {f : α → β} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} (h : Turing.MultiTapeTM.ComputableTidilyInPolyTime f encIn encMid) : ∃ (c : NativeCertificate f encIn encMid), c.IsPolynomial

Every native polynomial-time proof supplies a certificate with polynomial bounds. The space bound includes the running time so that it also bounds the emitted output.

noncomputable def Cslib.GenericRAM.NativeCertificate.ofPolyTime {α β : Type} {f : α → β} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} (h : Turing.MultiTapeTM.ComputableTidilyInPolyTime f encIn encMid) : NativeCertificate f encIn encMid

Select resource bounds from an existing polynomial-time implementation proof.

theorem Cslib.GenericRAM.NativeCertificate.ofPolyTime_isPolynomial {α β : Type} {f : α → β} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} (h : Turing.MultiTapeTM.ComputableTidilyInPolyTime f encIn encMid) : (ofPolyTime h).IsPolynomial

Bounds selected by ofPolyTime are polynomial in the encoded input length.

structure Cslib.GenericRAM.Model.Encoding (M : Model) : Type

Finite bit representations are separate from the semantic model. Configuration encoding is chosen explicitly; in particular, unary and binary widths have different resource costs.

• value : M.Value ↪ List Bool

  Encoding of register and memory values.

• address : M.Address ↪ List Bool

  Encoding of memory addresses.

• config : M.Config ↪ List Bool

  Encoding of runtime model parameters, including any word width.

def Cslib.GenericRAM.Model.checkedConstant (M : Model) (c : M.Const) (k : M.Config) : Option M.Value

A fixed literal's result, including the admissibility check performed by Data.put.

def Cslib.GenericRAM.Model.checkedOp (M : Model) (op : M.operations.Op) (p : M.Config × (Fin (M.operations.Arity op) → M.Value)) : Option M.Value

A fixed operation's result, including the admissibility check performed by Data.put. A native implementation can reject overflow without materializing the unchecked result.

theorem Cslib.GenericRAM.Model.eval_const_eq_map_checkedConstant {M : Model} {r : ℕ} (k : M.Config) (x : Data M r) (d : Fin r) (c : M.Const) : Op.eval k (Op.const d c) x = Option.map (x.set d) (M.checkedConstant c k)

A constant instruction stores exactly the checked literal result, preserving faults.

theorem Cslib.GenericRAM.Model.eval_alu_eq_map_checkedOp {M : Model} {r : ℕ} (k : M.Config) (x : Data M r) (op : M.operations.Op) (d : Fin r) (args : Fin (M.operations.Arity op) → Fin r) : Op.eval k (Op.alu op d args) x = Option.map (x.set d) (M.checkedOp op (k, x.regs ∘ args))

An ALU instruction stores exactly the checked operation result, preserving faults.

structure Cslib.GenericRAM.Model.NativePrimitives (M : Model) (enc : M.Encoding) : Type

Scalar certificates needed by a fixed-program RAM simulation. Memory lookup/update and finite-program dispatch are additional obligations. There is no uniform symbol dispatcher here.

• constant (c : M.Const) : NativeCertificate (M.checkedConstant c) enc.config (Turing.MultiTapeTM.encOption enc.value)

  Literal symbols are fixed; configuration varies over every encoded input.

• operation (op : M.operations.Op) : NativeCertificate (M.checkedOp op) (Turing.MultiTapeTM.encPair enc.config (Turing.MultiTapeTM.encPi enc.value)) (Turing.MultiTapeTM.encOption enc.value)

  Operation symbols are fixed; configuration and all operands are runtime inputs.

• test (t : M.tests.Op) : NativeCertificate (fun (p : M.Config × (Fin (M.tests.Arity t) → M.Value)) => M.evalTest p.1 t p.2) (Turing.MultiTapeTM.encPair enc.config (Turing.MultiTapeTM.encPi enc.value)) (Turing.MultiTapeTM.encOption Turing.MultiTapeTM.encBool)

  Tests preserve the distinction between fault, false and true.

• address : NativeCertificate (fun (p : M.Config × M.Value) => M.address p.1 p.2) (Turing.MultiTapeTM.encPair enc.config enc.value) (Turing.MultiTapeTM.encOption enc.address)

  Address extraction can fault independently of move validation.

• validMove : NativeCertificate (fun (p : M.Config × M.Value) => M.validMove p.1 p.2) (Turing.MultiTapeTM.encPair enc.config enc.value) Turing.MultiTapeTM.encBool

  Copy/load/store/halt validate existing values through this predicate.

• validPC : NativeCertificate (fun (p : M.Config × ℕ) => M.validPC p.1 p.2) (Turing.MultiTapeTM.encPair enc.config Turing.MultiTapeTM.encNat) Turing.MultiTapeTM.encBool

  Current and continuing control labels both require validation.

structure Cslib.GenericRAM.Model.NativePrimitives.IsPolynomial {M : Model} {enc : M.Encoding} (N : M.NativePrimitives enc) : Prop

All six primitive certificates in a bundle have polynomial time and space bounds.

• constant (c : M.Const) : (N.constant c).IsPolynomial

  Every literal symbol's certificate has polynomial time and space bounds.

• operation (op : M.operations.Op) : (N.operation op).IsPolynomial

  Every ALU operation symbol's certificate has polynomial time and space bounds.

• test (t : M.tests.Op) : (N.test t).IsPolynomial

  Every test symbol's certificate has polynomial time and space bounds.

• address : N.address.IsPolynomial

  The address extraction certificate has polynomial time and space bounds.

• validMove : N.validMove.IsPolynomial

  The move validation certificate has polynomial time and space bounds.

• validPC : N.validPC.IsPolynomial

  The control-label validation certificate has polynomial time and space bounds.