A certified RAM of bounded natural numbers

This small model has one binary addition operation and one strict-order test. Its runtime configuration is an exclusive upper bound on values, addresses and control labels. All three sorts are encoded in binary. Literals and addition results are checked against the bound; tests reject either out-of-range operand; moves, address extraction and control also check the bound. The model is intentionally small, to demonstrate every scalar certificate with both accepting and rejecting inputs. The configuration is a bound, not a binary-encoded word width.

Every certificate handles all configurations and operands with one fixed native machine. This is a certificate of scalar primitives, not of memory, complete RAM steps or runs.

Main definitions

• model: checked addition RAM with a runtime exclusive bound.
• encoding: binary encodings of all three sorts.
• nativePrimitives: a complete scalar certificate bundle.

Main results

• constant_polyTime, operation_polyTime, test_polyTime, address_polyTime, validMove_polyTime, validPC_polyTime, nativePrimitives_isPolynomial: native polynomial-time implementations and bundle polynomiality.

References

Uses Christian Reitwiessner's binary natural encodings and native machine arithmetic through the library's polynomial-time calculus.

@[reducible, inline]

abbrev Cslib.GenericRAM.BoundedNat.model : Model

Addition and strict comparison with an exclusive bound on values, addresses and labels.

def Cslib.GenericRAM.BoundedNat.encoding : model.Encoding

Binary encodings of the exclusive bound, stored values and addresses.

theorem Cslib.GenericRAM.BoundedNat.constant_polyTime (c : ℕ) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (model.checkedConstant c) Turing.MultiTapeTM.encNat (Turing.MultiTapeTM.encOption Turing.MultiTapeTM.encNat)

A literal is checked at every runtime bound, including zero.

theorem Cslib.GenericRAM.BoundedNat.operation_polyTime (op : model.operations.Op) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (model.checkedOp op) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat (Turing.MultiTapeTM.encPi Turing.MultiTapeTM.encNat)) (Turing.MultiTapeTM.encOption Turing.MultiTapeTM.encNat)

Addition checks its result before accepting it.

theorem Cslib.GenericRAM.BoundedNat.test_polyTime (t : model.tests.Op) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (p : ℕ × (Fin (model.tests.Arity t) → ℕ)) => model.evalTest p.1 t p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat (Turing.MultiTapeTM.encPi Turing.MultiTapeTM.encNat)) (Turing.MultiTapeTM.encOption Turing.MultiTapeTM.encBool)

Tests distinguish a false result from rejection of either invalid operand.

theorem Cslib.GenericRAM.BoundedNat.address_polyTime : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (p : ℕ × ℕ) => model.address p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encNat) (Turing.MultiTapeTM.encOption Turing.MultiTapeTM.encNat)

Address extraction checks the runtime bound.

theorem Cslib.GenericRAM.BoundedNat.validMove_polyTime : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (p : ℕ × ℕ) => model.validMove p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encNat) Turing.MultiTapeTM.encBool

Existing values are checked independently of newly produced values.

theorem Cslib.GenericRAM.BoundedNat.validPC_polyTime : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (p : ℕ × ℕ) => model.validPC p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encNat) Turing.MultiTapeTM.encBool

Both current and continuing control labels use this checked predicate.

noncomputable def Cslib.GenericRAM.BoundedNat.nativePrimitives : model.NativePrimitives encoding

Complete native scalar evidence; no field assumes a RAM simulator.

theorem Cslib.GenericRAM.BoundedNat.nativePrimitives_isPolynomial : nativePrimitives.IsPolynomial

The bounded-natural primitive bundle has polynomial resource bounds in all fields.