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.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.