Native primitive certificates and whole-run transport for WordRAM

The width is a runtime input encoded in unary; operand values and addresses are encoded in binary (Basis.encoding). For each operation symbol, a single native machine handles every encoded width and operand tuple, returning none when an operation is undefined or overflows 2 ^ w. Left shift caps the shift count at the unary width before exponentiating (checkedShiftLeft_eq), rejecting overflow when x > 0 and y ≥ w without materializing x <<< y. Polynomial bounds are in the complete encoded input length, including the unary width, not the bit length of a binary-encoded width. Computable width selection with charged costs and input fit remain separate obligations.

Every word-RAM basis shares the same checked-constant, equality/comparison test, address, move, and control-label certificates (Basis.nativePrimitivesOfPolyTime). Supplying operation certificates yields complete GenericRAM.Model.NativePrimitives bundles and IsPolynomial proofs for Basis.standard, Basis.additive, Basis.arithmetic, and Basis.exact, as well as arbitrary sub-bases (Basis.restrict) and homomorphic preimages (Basis.Hom.checkedOp_polyTime).

Via WordRAM.Program.toGeneric, halting WordRAM.Executes runs correspond to halting GenericRAM.FiniteState.run executions and inherit whole-run native transport (WordRAM.transportCertificate, WordRAM.transport_inO, WordRAM.transport_polyTime, and WordRAM.transport_polyTime_of_le_const) whenever a NativePrimitives bundle is supplied for B.genericModel.

Main definitions

• Basis.encoding: binary value and address encodings with unary runtime word width.
• Basis.nativePrimitivesOfPolyTime: complete scalar primitive bundle for a word-RAM basis from polynomial-time operation certificates.
• Basis.standard.nativePrimitives, Basis.additive.nativePrimitives, Basis.arithmetic.nativePrimitives, Basis.exact.nativePrimitives: complete scalar certificate bundles for the standard, additive, arithmetic, and exact word-RAM bases.

Main results

• checkedConstant_polyTime, evalTest_polyTime, address_polyTime, validMove_polyTime, validPC_polyTime: basis-independent polynomial-time scalar certificates.
• checkedShiftLeft_eq: left shift fits a w-bit word iff shifting by min w y fits, with equal output.
• checkedAdd_polyTime, checkedAddCertificate, checkedBinOp_polyTime, checkedWidth_polyTime, checkedOp_polyTime, checkedExactOp_polyTime: native polynomial time for all checked operations of Basis.standard and Basis.exact.
• Basis.Hom.checkedOp_polyTime, Basis.restrict_checkedOp_polyTime: transport of polynomial-time operation certificates along basis homomorphisms and restrictions.
• Basis.nativePrimitivesOfPolyTime_isPolynomial, Basis.standard.nativePrimitives_isPolynomial, Basis.additive.nativePrimitives_isPolynomial, Basis.arithmetic.nativePrimitives_isPolynomial, Basis.exact.nativePrimitives_isPolynomial: bundle polynomiality for arbitrary and named bases.
• executes_iff_exists_finiteRun, transportCertificate, transport_inO, transport_polyTime, transport_polyTime_of_le_const: whole-run native transport for WordRAM programs via GenericRAM.FiniteState.

References

• MIT–ULB CompGeom Group, Undecidability of tiling with a tromino

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

def Cslib.WordRAM.Basis.encoding (B : Basis) : B.genericModel.Encoding

Binary encodings for word values and addresses, with the runtime word width encoded in unary.

theorem Cslib.WordRAM.checkedConstant_polyTime (B : Basis) (c : ℕ) : Turing.MultiTapeTM.ComputableInPolyTime (B.genericModel.checkedConstant c) Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encOption Turing.MultiTapeTM.encNat)

A literal is checked against 2 ^ w at every unary-encoded runtime width w.

theorem Cslib.WordRAM.evalTest_polyTime (B : Basis) (t : Bool) : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × (Fin (B.genericModel.tests.Arity t) → ℕ)) => B.genericModel.evalTest p.1 t p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPi Turing.MultiTapeTM.encNat)) (Turing.MultiTapeTM.encOption Turing.MultiTapeTM.encBool)

Both word-RAM register tests (eq and lt) are polynomial-time at every encoded width.

theorem Cslib.WordRAM.address_polyTime (B : Basis) : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × ℕ) => B.genericModel.address p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encNat) (Turing.MultiTapeTM.encOption Turing.MultiTapeTM.encNat)

Word-RAM address extraction is the total identity into Option ℕ.

theorem Cslib.WordRAM.validMove_polyTime (B : Basis) : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × ℕ) => B.genericModel.validMove p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encNat) Turing.MultiTapeTM.encBool

Copies, loads, stores and halts move existing words without an extra range check.

theorem Cslib.WordRAM.validPC_polyTime (B : Basis) : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × ℕ) => B.genericModel.validPC p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encNat) Turing.MultiTapeTM.encBool

Control labels in WordRAM are unbounded natural numbers validated at instruction fetch.

theorem Cslib.WordRAM.checkedShiftLeft_eq (w x y : ℕ) : (if decide (Fits w (x <<< y)) = true then some (x <<< y) else none) = if decide (Fits w (x * 2 ^ min w y)) = true then some (x * 2 ^ min w y) else none

Left shift fits a w-bit word if and only if shifting by min w y fits, and when it fits both shifts produce the same word. This avoids materializing x <<< y when y > w.

theorem Cslib.WordRAM.checkedAdd_polyTime : Turing.MultiTapeTM.ComputableInPolyTime (Basis.standard.genericModel.checkedOp (StandardOp.bin BinOp.add)) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPi Turing.MultiTapeTM.encNat)) (Turing.MultiTapeTM.encOption Turing.MultiTapeTM.encNat)

Checked addition is polynomial in the full encoding: unary width and binary operands.

noncomputable def Cslib.WordRAM.checkedAddCertificate : GenericRAM.NativeCertificate (Basis.standard.genericModel.checkedOp (StandardOp.bin BinOp.add)) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPi Turing.MultiTapeTM.encNat)) (Turing.MultiTapeTM.encOption Turing.MultiTapeTM.encNat)

One native checked-add implementation works at every encoded width.

theorem Cslib.WordRAM.checkedBinOp_polyTime (f : BinOp) : Turing.MultiTapeTM.ComputableInPolyTime (Basis.standard.genericModel.checkedOp (StandardOp.bin f)) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPi Turing.MultiTapeTM.encNat)) (Turing.MultiTapeTM.encOption Turing.MultiTapeTM.encNat)

Every binary operation in Basis.standard has a polynomial-time checked implementation.

theorem Cslib.WordRAM.checkedWidth_polyTime : Turing.MultiTapeTM.ComputableInPolyTime (Basis.standard.genericModel.checkedOp StandardOp.width) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPi Turing.MultiTapeTM.encNat)) (Turing.MultiTapeTM.encOption Turing.MultiTapeTM.encNat)

Reading the word size in Basis.standard is polynomial-time.

theorem Cslib.WordRAM.checkedOp_polyTime (op : StandardOp) : Turing.MultiTapeTM.ComputableInPolyTime (Basis.standard.genericModel.checkedOp op) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPi Turing.MultiTapeTM.encNat)) (Turing.MultiTapeTM.encOption Turing.MultiTapeTM.encNat)

Every operation in Basis.standard has a polynomial-time checked implementation.

theorem Cslib.WordRAM.checkedExactOp_polyTime (op : StandardOp) : Turing.MultiTapeTM.ComputableInPolyTime (Basis.exact.genericModel.checkedOp op) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPi Turing.MultiTapeTM.encNat)) (Turing.MultiTapeTM.encOption Turing.MultiTapeTM.encNat)

Every operation in Basis.exact has a polynomial-time checked implementation, preserving exact subtraction-underflow and zero-divisor faults.

theorem Cslib.WordRAM.Basis.Hom.checkedOp_polyTime {B B' : Basis} (φ : B.Hom B') (hop : ∀ (op : B'.Op), Turing.MultiTapeTM.ComputableInPolyTime (B'.genericModel.checkedOp op) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPi Turing.MultiTapeTM.encNat)) (Turing.MultiTapeTM.encOption Turing.MultiTapeTM.encNat)) (op : B.Op) : Turing.MultiTapeTM.ComputableInPolyTime (B.genericModel.checkedOp op) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPi Turing.MultiTapeTM.encNat)) (Turing.MultiTapeTM.encOption Turing.MultiTapeTM.encNat)

Pull back polynomial-time checked-operation certificates along any map of bases.

theorem Cslib.WordRAM.Basis.restrict_checkedOp_polyTime (B : Basis) (P : B.Op → Prop) (hop : ∀ (op : B.Op), Turing.MultiTapeTM.ComputableInPolyTime (B.genericModel.checkedOp op) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPi Turing.MultiTapeTM.encNat)) (Turing.MultiTapeTM.encOption Turing.MultiTapeTM.encNat)) (op : (B.restrict P).Op) : Turing.MultiTapeTM.ComputableInPolyTime ((B.restrict P).genericModel.checkedOp op) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPi Turing.MultiTapeTM.encNat)) (Turing.MultiTapeTM.encOption Turing.MultiTapeTM.encNat)

Restricting a basis preserves polynomial-time checked-operation certificates definitionally.

noncomputable def Cslib.WordRAM.Basis.nativePrimitivesOfPolyTime (B : Basis) (hop : ∀ (op : B.Op), Turing.MultiTapeTM.ComputableInPolyTime (B.genericModel.checkedOp op) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPi Turing.MultiTapeTM.encNat)) (Turing.MultiTapeTM.encOption Turing.MultiTapeTM.encNat)) : B.genericModel.NativePrimitives B.encoding

Package a complete NativePrimitives bundle for a word-RAM basis from polynomial-time certificates for its operations.

theorem Cslib.WordRAM.Basis.nativePrimitivesOfPolyTime_isPolynomial (B : Basis) (hop : ∀ (op : B.Op), Turing.MultiTapeTM.ComputableInPolyTime (B.genericModel.checkedOp op) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPi Turing.MultiTapeTM.encNat)) (Turing.MultiTapeTM.encOption Turing.MultiTapeTM.encNat)) : (B.nativePrimitivesOfPolyTime hop).IsPolynomial

Every primitive certificate in Basis.nativePrimitivesOfPolyTime has polynomial resource bounds.

noncomputable def Cslib.WordRAM.Basis.standard.nativePrimitives : standard.genericModel.NativePrimitives standard.encoding

Complete native scalar primitive bundle for Basis.standard.

theorem Cslib.WordRAM.Basis.standard.nativePrimitives_isPolynomial : nativePrimitives.IsPolynomial

The standard word-RAM primitive bundle has polynomial time and space bounds in all fields.

noncomputable def Cslib.WordRAM.Basis.additive.nativePrimitives : additive.genericModel.NativePrimitives additive.encoding

Complete native scalar primitive bundle for Basis.additive.

theorem Cslib.WordRAM.Basis.additive.nativePrimitives_isPolynomial : nativePrimitives.IsPolynomial

The additive word-RAM primitive bundle has polynomial time and space bounds in all fields.

noncomputable def Cslib.WordRAM.Basis.arithmetic.nativePrimitives : arithmetic.genericModel.NativePrimitives arithmetic.encoding

Complete native scalar primitive bundle for Basis.arithmetic.

theorem Cslib.WordRAM.Basis.arithmetic.nativePrimitives_isPolynomial : nativePrimitives.IsPolynomial

The arithmetic word-RAM primitive bundle has polynomial time and space bounds in all fields.

noncomputable def Cslib.WordRAM.Basis.exact.nativePrimitives : exact.genericModel.NativePrimitives exact.encoding

Complete native scalar primitive bundle for Basis.exact.

theorem Cslib.WordRAM.Basis.exact.nativePrimitives_isPolynomial : nativePrimitives.IsPolynomial

The exact word-RAM primitive bundle has polynomial time and space bounds in all fields.

Whole-run transport adapter

theorem Cslib.WordRAM.executes_iff_exists_finiteRun {B : Basis} {r : ℕ} (w : ℕ) (p : Program B r) (s : GenericRAM.FiniteState B.genericModel r) (u : State r) (hden : s.denote = State.toGeneric B u) (v : ℕ) : (∃ (m : ℕ), Executes w p u v m) ↔ ∃ (n : ℕ), GenericRAM.FiniteState.run w p.toGeneric n s = some (Sum.inr v)

Halting WordRAM.Executes runs correspond to halting FiniteState.run executions of p.toGeneric.

noncomputable def Cslib.WordRAM.transportCertificate {B : Basis} {r : ℕ} {α : Type} {ei : α ↪ List Bool} (enc : B.genericModel.Encoding) (N : B.genericModel.NativePrimitives enc) (p : Program B r) {f cfg : α → ℕ} {initState : α → GenericRAM.FiniteState B.genericModel r} {u : α → State r} {steps : α → ℕ} (cSteps : GenericRAM.NativeCertificate steps ei Turing.MultiTapeTM.encNat) (cCfg : GenericRAM.NativeCertificate cfg ei enc.config) (cInit : GenericRAM.NativeCertificate initState ei (GenericRAM.FiniteState.encoding enc)) (hden : ∀ (a : α), (initState a).denote = State.toGeneric B (u a)) (hExec : ∀ (a : α), ∃ m ≤ steps a, Executes (cfg a) p (u a) (f a) m) : GenericRAM.NativeCertificate f ei enc.value

Transport a halting WordRAM.Executes certificate within steps a instructions to a native multitape Turing-machine certificate for f : α → ℕ.

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

Parameterized ComputableInO transport theorem from WordRAM.Executes.

theorem Cslib.WordRAM.transport_polyTime {B : Basis} {r : ℕ} {α : Type} {ei : α ↪ List Bool} (enc : B.genericModel.Encoding) (N : B.genericModel.NativePrimitives enc) (p : Program B r) {f cfg : α → ℕ} {initState : α → GenericRAM.FiniteState B.genericModel r} {u : α → State r} {steps : α → ℕ} (cSteps : GenericRAM.NativeCertificate steps ei Turing.MultiTapeTM.encNat) (cCfg : GenericRAM.NativeCertificate cfg ei enc.config) (cInit : GenericRAM.NativeCertificate initState ei (GenericRAM.FiniteState.encoding enc)) (hden : ∀ (a : α), (initState a).denote = State.toGeneric B (u a)) (hExec : ∀ (a : α), ∃ m ≤ steps a, Executes (cfg a) p (u a) (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) {bound : α → ℕ} (hB : Turing.MultiTapeTM.PolyBounded (fun (a : α) => (ei a).length) bound) (hOutLen : ∀ (a : α), ∀ j ≤ steps a, ((GenericRAM.FiniteState.resultEncoding enc) (GenericRAM.FiniteState.run (cfg a) p.toGeneric j (initState a))).length ≤ bound a) : Turing.MultiTapeTM.ComputableInPolyTime f ei enc.value

Automatic ComputableInPolyTime transport corollary from WordRAM.Executes.

theorem Cslib.WordRAM.transport_polyTime_of_le_const {B : Basis} {r : ℕ} {α : Type} {ei : α ↪ List Bool} (enc : B.genericModel.Encoding) (N : B.genericModel.NativePrimitives enc) (p : Program B r) {f cfg : α → ℕ} {initState : α → GenericRAM.FiniteState B.genericModel r} {u : α → State r} {steps : α → ℕ} (cSteps : GenericRAM.NativeCertificate steps ei Turing.MultiTapeTM.encNat) (cCfg : GenericRAM.NativeCertificate cfg ei enc.config) (cInit : GenericRAM.NativeCertificate initState ei (GenericRAM.FiniteState.encoding enc)) (hden : ∀ (a : α), (initState a).denote = State.toGeneric B (u a)) (hExec : ∀ (a : α), ∃ m ≤ steps a, Executes (cfg a) p (u a) (f a) m) (hN : N.IsPolynomial) (hSteps : cSteps.IsPolynomial) (hCfg : cCfg.IsPolynomial) (hInit : cInit.IsPolynomial) (K : ℕ) (hStepsLe : ∀ (a : α), steps a ≤ K) : Turing.MultiTapeTM.ComputableInPolyTime f ei enc.value

Automatic ComputableInPolyTime transport corollary from WordRAM.Executes under a constant step-budget bound ∀ a, steps a ≤ K.