diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Nat/Binary.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Nat/Binary.lean
index cbd5deba3a..da57e60f51 100644
--- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Nat/Binary.lean
+++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Nat/Binary.lean
@@ -9,10 +9,13 @@ module
 
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Arith
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List
+public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Degree
 public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Decoder
 public import Complexity.Foundations.Data.Nat.Bits
+import Complexity.Foundations.Data.BitString.List.Binary
+import Complexity.Tactic.PolyTime.Init
 import Mathlib.Data.List.GetD
 import Mathlib.Data.Nat.Bitwise
 
@@ -61,6 +64,12 @@ multiplication.
   composition rules for `fun_prop`.
 * `Turing.MultiTapeTM.ComputableTidilyInPolyTime.binary_mul'`, `.binary_sub'`, `.binary_pow'`:
   composition rules for `fun_prop`.
+* `Turing.MultiTapeTM.ComputableInPolyTime.binary_bitwise`, `.binary_and`, `.binary_or`,
+  `.binary_xor`, `.binary_and'`, `.binary_or'`, `.binary_xor'`: bitwise operations on binary
+  naturals, and their composition rules.
+* `Turing.MultiTapeTM.ComputableInPolyTime.binary_size`, `.binary_min_unary`,
+  `.binary_min_unary'`, `.binary_shiftRight`, `.binary_shiftRight'`: bit-length in unary, capping
+  a binary natural by a unary bound, and binary right shift.
 * `Turing.MultiTapeTM.ComputableTidilyInPolyTime.binary_testBit`: a bit of a binary number at a
   unary position.
 -/
@@ -217,6 +226,49 @@ lemma sub_eq (p : ℕ × ℕ) : p.1 - p.2 =
     simp only [h, Bool.toNat_true, Bool.toNat_false, Bool.false_eq_true, ↓reduceIte] at hval ⊢ <;>
     lia
 
+private lemma foldl_append_singleton {α β : Type} (f : α → β) (l : List α) (out : List β) :
+    l.foldl (fun acc a => acc ++ [f a]) out = out ++ l.map f := by
+  induction l generalizing out with
+  | nil => simp
+  | cons a l ih => simp [ih]
+
+/-- Any zero-preserving bitwise operation on `ℕ` is read off by folding `op` over `digitPairs`. -/
+private lemma bitwise_eq (op : Bool → Bool → Bool) (h0 : op false false = false) (p : ℕ × ℕ) :
+    Nat.bitwise op p.1 p.2 =
+      ofBits ((digitPairs p).foldl (fun acc d => acc ++ [op d.1 d.2]) []) := by
+  rw [foldl_append_singleton, List.nil_append, ofBits]
+  have hmap : (digitPairs p).map (fun d => op d.1 d.2) =
+      (List.range (p.1.bits.length + p.2.bits.length)).map
+        (Nat.bitwise op p.1 p.2).testBit := by
+    simp only [digitPairs, List.map_map, Function.comp_def, bits_getD, ← Nat.testBit_bitwise h0]
+  rw [hmap, Nat.foldr_bit_testBit]
+  rw [Nat.size_eq_bits_len, Nat.size_eq_bits_len]
+  refine Nat.size_le.2 (Nat.bitwise_lt_two_pow ?_ ?_)
+  · exact (Nat.lt_size_self p.1).trans_le (Nat.pow_le_pow_right (by lia) (by lia))
+  · exact (Nat.lt_size_self p.2).trans_le (Nat.pow_le_pow_right (by lia) (by lia))
+
+private lemma ofBits_tail (w : List Bool) : ofBits w.tail = ofBits w / 2 := by
+  cases w with
+  | nil => simp [ofBits]
+  | cons b w =>
+    simp only [List.tail_cons, ofBits, List.foldr_cons, Nat.bit_val]
+    cases b <;> simp only [Bool.toNat_false, Bool.toNat_true] <;> lia
+
+private lemma ofBits_drop (w : List Bool) (k : ℕ) : ofBits (w.drop k) = ofBits w / 2 ^ k := by
+  induction k generalizing w with
+  | zero => simp
+  | succ k ih =>
+    rw [← List.drop_tail, ih, ofBits_tail, Nat.div_div_eq_div_mul, Nat.pow_succ']
+
+/-- Right shift drops at most the dividend's bit length of least-significant digits. -/
+private lemma shiftRight_eq_ofBits_drop (p : ℕ × ℕ) :
+    p.1 >>> p.2 = ofBits (p.1.bits.drop (min p.1.bits.length p.2)) := by
+  have hdrop : p.1.bits.drop (min p.1.bits.length p.2) = p.1.bits.drop p.2 := by
+    rcases le_total p.1.bits.length p.2 with h | h
+    · rw [Nat.min_eq_left h, List.drop_eq_nil_of_le le_rfl, List.drop_eq_nil_of_le h]
+    · rw [Nat.min_eq_right h]
+  rw [hdrop, ofBits_drop, ofBits, Nat.foldr_bit_bits, Nat.shiftRight_eq_div_pow]
+
 end Turing.MultiTapeTM.BinarySub
 
 namespace Turing.MultiTapeTM.ComputableTidilyInPolyTime
@@ -425,4 +477,161 @@ theorem binary_testBit {α : Type} {input : α ↪ List Bool} {n i : α → ℕ}
   simp only [Function.comp_apply, Nat.testBit_eq_inth, ← List.getD_default_eq_getI]
   rfl
 
+/-- Any zero-preserving bitwise operation on binary naturals is polynomial-time. -/
+private theorem binary_bitwise (op : Bool → Bool → Bool) (h0 : op false false = false) :
+    ComputableTidilyInPolyTime (fun p : ℕ × ℕ => Nat.bitwise op p.1 p.2)
+      (encPair encNat encNat) encNat := by
+  have hpairs : ComputableTidilyInPolyTime BinarySub.digitPairs (encPair encNat encNat)
+      (encList (encPair encBool encBool)) := by
+    unfold BinarySub.digitPairs
+    fun_prop
+  have hop : ComputableTidilyInPolyTime (fun d : Bool × Bool => op d.1 d.2)
+      (encPair encBool encBool) encBool := of_finite _
+  have hstep : ComputableTidilyInPolyTime
+      (fun p : List Bool × (Bool × Bool) => p.1 ++ [op p.2.1 p.2.2])
+      (encPair encBits (encPair encBool encBool)) encBits :=
+    bitsAppend (fst _ _) (bitsCons (hop.comp (snd _ _)) (const []))
+  have hfold := foldl_of_bounded_growth (encA := encPair encBool encBool)
+    (encL := encList (encPair encBool encBool)) (encB := encBits)
+    (step := fun acc d => acc ++ [op d.1 d.2])
+    (init := fun _ => []) hpairs (const []) hstep (growth := 1) (fun _ _ => by simp)
+  convert bitsToNat.comp hfold using 1
+  funext p
+  exact BinarySub.bitwise_eq op h0 p
+
+/-- The smaller of a unary natural and a binary natural, returned in unary by saturating binary
+decoding. -/
+private theorem binary_min_unary : ComputableTidilyInPolyTime (fun p : ℕ × ℕ => min p.1 p.2)
+    (encPair encUnary encNat) encUnary := by
+  have h := foldlWith (encA := encBool) (encL := encBits) (encP := encUnary)
+    (par := Prod.fst) (list := fun p : ℕ × ℕ => p.2.bits.reverse)
+    (step := fun cap value bit => min cap (2 * value + bit.toNat))
+    (fst encUnary encNat) (bitsReverse.comp (natBits.comp (snd encUnary encNat)))
+    (const 0) (by fun_prop) (B := Prod.fst)
+    (by simpa only [encUnary_apply, List.length_replicate] using
+      (fst encUnary encNat).polyBounded_length)
+    (fun p i _ => by
+      simpa only [encUnary_apply, List.length_replicate, Cslib.BitString.boundedBinaryValue] using
+        Cslib.BitString.boundedBinaryValue_le p.1 (p.2.bits.reverse.take i))
+  convert h using 1
+  funext p
+  rw [← Cslib.BitString.boundedBinaryValue, Cslib.BitString.boundedBinaryValue_eq,
+    Cslib.BitString.binaryValue_reverse_bits]
+
+/-- Cap a computed binary natural by a computed unary bound, returning the result in unary. -/
+private theorem binary_min_unary' {α : Type} {input : α ↪ List Bool} {left right : α → ℕ}
+    (hleft : ComputableTidilyInPolyTime left input encUnary)
+    (hright : ComputableTidilyInPolyTime right input encNat) :
+    ComputableTidilyInPolyTime (fun a => min (left a) (right a)) input encUnary :=
+  binary_min_unary.comp (hleft.prod hright)
+
+/-- Right shift of binary naturals, by dropping at most the dividend's bit length of low-order
+digits. -/
+private theorem binary_shiftRight : ComputableTidilyInPolyTime (fun p : ℕ × ℕ => p.1 >>> p.2)
+    (encPair encNat encNat) encNat := by
+  have hbits := natBits.comp (fst encNat encNat)
+  have hlen : ComputableTidilyInPolyTime (fun p : ℕ × ℕ => p.1.bits.length)
+      (encPair encNat encNat) encUnary := (length encBool).comp hbits
+  have hdrop := bitsDropWithInput hbits (binary_min_unary' hlen (snd encNat encNat))
+  convert bitsToNat.comp hdrop using 1
+  funext p
+  exact BinarySub.shiftRight_eq_ofBits_drop p
+
 end Turing.MultiTapeTM.ComputableTidilyInPolyTime
+
+namespace Turing.MultiTapeTM.ComputableInPolyTime
+
+/-- Any zero-preserving bitwise operation on binary naturals is polynomial-time. -/
+@[program_certificate]
+theorem binary_bitwise (op : Bool → Bool → Bool) (h0 : op false false = false) :
+    ComputableInPolyTime (fun p : ℕ × ℕ => Nat.bitwise op p.1 p.2)
+      (encPair encNat encNat) encNat :=
+  .of_tidy (ComputableTidilyInPolyTime.binary_bitwise op h0)
+
+/-- Bitwise AND of binary naturals. -/
+@[fun_prop, program_certificate]
+theorem binary_and : ComputableInPolyTime (fun p : ℕ × ℕ => p.1 &&& p.2)
+    (encPair encNat encNat) encNat :=
+  .of_tidy <| (ComputableTidilyInPolyTime.binary_bitwise and rfl).of_enc_eq fun p =>
+    congrArg encNat <| Nat.eq_of_testBit_eq fun i => by
+      rw [Nat.testBit_bitwise rfl, Nat.testBit_and]
+
+/-- Bitwise OR of binary naturals. -/
+@[fun_prop, program_certificate]
+theorem binary_or : ComputableInPolyTime (fun p : ℕ × ℕ => p.1 ||| p.2)
+    (encPair encNat encNat) encNat :=
+  .of_tidy <| (ComputableTidilyInPolyTime.binary_bitwise or rfl).of_enc_eq fun p =>
+    congrArg encNat <| Nat.eq_of_testBit_eq fun i => by
+      rw [Nat.testBit_bitwise rfl, Nat.testBit_or]
+
+/-- Bitwise XOR of binary naturals. -/
+@[fun_prop, program_certificate]
+theorem binary_xor : ComputableInPolyTime (fun p : ℕ × ℕ => p.1 ^^^ p.2)
+    (encPair encNat encNat) encNat :=
+  .of_tidy <| (ComputableTidilyInPolyTime.binary_bitwise xor rfl).of_enc_eq fun p =>
+    congrArg encNat <| Nat.eq_of_testBit_eq fun i => by
+      rw [Nat.testBit_bitwise rfl, Nat.testBit_xor]
+
+/-- Bitwise AND of computed binary naturals. -/
+@[fun_prop, program_certificate]
+theorem binary_and' {α : Type} {input : α ↪ List Bool} {left right : α → ℕ}
+    (hleft : ComputableInPolyTime left input encNat)
+    (hright : ComputableInPolyTime right input encNat) :
+    ComputableInPolyTime (fun a => left a &&& right a) input encNat :=
+  binary_and.comp (hleft.prod hright)
+
+/-- Bitwise OR of computed binary naturals. -/
+@[fun_prop, program_certificate]
+theorem binary_or' {α : Type} {input : α ↪ List Bool} {left right : α → ℕ}
+    (hleft : ComputableInPolyTime left input encNat)
+    (hright : ComputableInPolyTime right input encNat) :
+    ComputableInPolyTime (fun a => left a ||| right a) input encNat :=
+  binary_or.comp (hleft.prod hright)
+
+/-- Bitwise XOR of computed binary naturals. -/
+@[fun_prop, program_certificate]
+theorem binary_xor' {α : Type} {input : α ↪ List Bool} {left right : α → ℕ}
+    (hleft : ComputableInPolyTime left input encNat)
+    (hright : ComputableInPolyTime right input encNat) :
+    ComputableInPolyTime (fun a => left a ^^^ right a) input encNat :=
+  binary_xor.comp (hleft.prod hright)
+
+/-- The bit-length `Nat.size n` of a binary natural, returned in unary. -/
+@[fun_prop, program_certificate]
+theorem binary_size : ComputableInPolyTime Nat.size encNat encUnary :=
+  .of_tidy <|
+    ((ComputableTidilyInPolyTime.length encBool).comp
+      ComputableTidilyInPolyTime.natBits).of_enc_eq fun n =>
+      congrArg encUnary (Nat.size_eq_bits_len n).symm
+
+/-- The smaller of a unary natural and a binary natural, returned in unary by saturating binary
+decoding. -/
+@[fun_prop, program_certificate]
+theorem binary_min_unary : ComputableInPolyTime (fun p : ℕ × ℕ => min p.1 p.2)
+    (encPair encUnary encNat) encUnary :=
+  .of_tidy ComputableTidilyInPolyTime.binary_min_unary
+
+/-- Cap a computed binary natural by a computed unary bound, returning the result in unary. -/
+@[fun_prop, program_certificate]
+theorem binary_min_unary' {α : Type} {input : α ↪ List Bool} {left right : α → ℕ}
+    (hleft : ComputableInPolyTime left input encUnary)
+    (hright : ComputableInPolyTime right input encNat) :
+    ComputableInPolyTime (fun a => min (left a) (right a)) input encUnary :=
+  binary_min_unary.comp (hleft.prod hright)
+
+/-- Right shift of binary naturals, by dropping at most the dividend's bit length of low-order
+digits. -/
+@[fun_prop, program_certificate]
+theorem binary_shiftRight : ComputableInPolyTime (fun p : ℕ × ℕ => p.1 >>> p.2)
+    (encPair encNat encNat) encNat :=
+  .of_tidy ComputableTidilyInPolyTime.binary_shiftRight
+
+/-- Right shift of computed binary naturals. -/
+@[fun_prop, program_certificate]
+theorem binary_shiftRight' {α : Type} {input : α ↪ List Bool} {left right : α → ℕ}
+    (hleft : ComputableInPolyTime left input encNat)
+    (hright : ComputableInPolyTime right input encNat) :
+    ComputableInPolyTime (fun a => left a >>> right a) input encNat :=
+  binary_shiftRight.comp (hleft.prod hright)
+
+end Turing.MultiTapeTM.ComputableInPolyTime
diff --git a/Complexity/Computability/WordRAM/Native.lean b/Complexity/Computability/WordRAM/Native.lean
index 9d8182f7dc..8a5515cfb7 100644
--- a/Complexity/Computability/WordRAM/Native.lean
+++ b/Complexity/Computability/WordRAM/Native.lean
@@ -12,17 +12,26 @@ public import Complexity.Computability.GenericRAM.Simulation.Run
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Binary
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Pi
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Option
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.BinaryDiv
 import Complexity.Tactic.PolyTime.Init
 
 /-!
 # Native primitive certificates and whole-run transport for WordRAM
 
-The width is a runtime input encoded in unary; operand values are encoded in binary. A single
-native machine handles every width and both operands, returning `none` precisely when the sum
-does not fit. Its polynomial bound is in the complete encoded input length, including the unary
-width, not the bit length of a binary-encoded width. No claim about the other standard-basis
-operations, memory access or whole-program simulation follows from this primitive certificate.
-Computable width selection with charged costs and input fit remain separate obligations.
+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
@@ -30,10 +39,30 @@ Via `WordRAM.Program.toGeneric`, halting `WordRAM.Executes` runs correspond to h
 `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
 
-* `checkedAdd_polyTime`: native polynomial time for checked standard-basis addition.
-* `checkedAddCertificate`: arbitrary-bound interface obtained from that implementation.
+* `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`.
@@ -50,30 +79,287 @@ library's polynomial-time calculus.
 
 namespace Cslib.WordRAM
 
+open Cslib.GenericRAM
 open Turing.MultiTapeTM Turing.MultiTapeTM.ComputableTidilyInPolyTime
 
+/-- Binary encodings for word values and addresses, with the runtime word width encoded in unary. -/
+def Basis.encoding (B : Basis) : B.genericModel.Encoding :=
+  ⟨encNat, encNat, encUnary⟩
+
+/-- Check whether a computed natural result fits a runtime unary width `w`, returning `none` on
+overflow. -/
+private theorem checkFits_polyTime {k : ℕ} {val : ℕ × (Fin k → ℕ) → ℕ}
+    (hval : ComputableTidilyInPolyTime val (encPair encUnary (encPi encNat)) encNat) :
+    ComputableInPolyTime
+      (fun p : ℕ × (Fin k → ℕ) => if decide (Fits p.1 (val p)) then some (val p) else none)
+      (encPair encUnary (encPi encNat)) (encOption encNat) := by
+  have hpow := binary_two_pow.comp (fst encUnary (encPi encNat (Index := Fin k)))
+  simp only [fits_iff, decide_eq_true_eq]
+  exact .of_tidy <|
+    (binary_lt' hval hpow).ite_decide ((optionSome encNat).comp hval) (const none)
+
+/-- A literal is checked against `2 ^ w` at every unary-encoded runtime width `w`. -/
+@[fun_prop, program_certificate]
+theorem checkedConstant_polyTime (B : Basis) (c : ℕ) :
+    ComputableInPolyTime (B.genericModel.checkedConstant c)
+      encUnary (encOption encNat) := by
+  change ComputableInPolyTime
+    (fun w : ℕ => if decide (c < 2 ^ w) then some c else none) encUnary (encOption encNat)
+  simp only [decide_eq_true_eq]
+  exact .of_tidy <|
+    (binary_lt' (const c) binary_two_pow).ite_decide (const (some c)) (const none)
+
+/-- Both word-RAM register tests (`eq` and `lt`) are polynomial-time at every encoded width. -/
+@[fun_prop, program_certificate]
+theorem evalTest_polyTime (B : Basis) (t : Bool) :
+    ComputableInPolyTime (fun p => B.genericModel.evalTest p.1 t p.2)
+      (encPair encUnary (encPi encNat)) (encOption encBool) := by
+  have hx := (pi_apply encNat (0 : Fin 2)).comp (snd encUnary (encPi encNat))
+  have hy := (pi_apply encNat (1 : Fin 2)).comp (snd encUnary (encPi encNat))
+  cases t
+  · change ComputableInPolyTime
+      (fun p : ℕ × (Fin 2 → ℕ) => some (decide (p.2 0 = p.2 1)))
+      (encPair encUnary (encPi encNat (Index := Fin 2))) (encOption encBool)
+    exact .of_tidy <| (optionSome encBool).comp ((decide_eq encNat).comp (hx.prod hy))
+  · change ComputableInPolyTime
+      (fun p : ℕ × (Fin 2 → ℕ) => some (decide (p.2 0 < p.2 1)))
+      (encPair encUnary (encPi encNat (Index := Fin 2))) (encOption encBool)
+    exact .of_tidy <| (optionSome encBool).comp (binary_lt' hx hy)
+
+/-- Word-RAM address extraction is the total identity into `Option ℕ`. -/
+@[fun_prop, program_certificate]
+theorem address_polyTime (B : Basis) :
+    ComputableInPolyTime (fun p => B.genericModel.address p.1 p.2)
+      (encPair encUnary encNat) (encOption encNat) :=
+  .of_tidy <| (optionSome encNat).comp (snd encUnary encNat)
+
+/-- Copies, loads, stores and halts move existing words without an extra range check. -/
+@[fun_prop, program_certificate]
+theorem validMove_polyTime (B : Basis) :
+    ComputableInPolyTime (fun p => B.genericModel.validMove p.1 p.2)
+      (encPair encUnary encNat) encBool :=
+  .of_tidy (const true)
+
+/-- Control labels in `WordRAM` are unbounded natural numbers validated at instruction fetch. -/
+@[fun_prop, program_certificate]
+theorem validPC_polyTime (B : Basis) :
+    ComputableInPolyTime (fun p => B.genericModel.validPC p.1 p.2)
+      (encPair encUnary encNat) encBool :=
+  .of_tidy (const true)
+
+/-- 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 checkedShiftLeft_eq (w x y : ℕ) :
+    (if decide (Fits w (x <<< y)) then some (x <<< y) else none) =
+      if decide (Fits w (x * 2 ^ min w y)) then some (x * 2 ^ min w y) else none := by
+  rw [Nat.shiftLeft_eq]
+  rcases le_or_gt y w with h | h
+  · rw [Nat.min_eq_right h]
+  · rw [Nat.min_eq_left h.le]
+    rcases Nat.eq_zero_or_pos x with rfl | hx
+    · simp
+    · have h1 : ¬Fits w (x * 2 ^ y) := by
+        rw [fits_iff, not_lt]
+        exact (Nat.pow_le_pow_right Nat.two_pos h.le).trans (Nat.le_mul_of_pos_left _ hx)
+      have h2 : ¬Fits w (x * 2 ^ w) := by
+        rw [fits_iff, not_lt]
+        exact Nat.le_mul_of_pos_left _ hx
+      simp [h1, h2]
+
 /-- Checked addition is polynomial in the full encoding: unary width and binary operands. -/
-@[program_certificate]
+@[fun_prop, program_certificate]
 theorem checkedAdd_polyTime :
-    ComputableTidilyInPolyTime (Basis.standard.genericModel.checkedOp (.bin .add))
+    ComputableInPolyTime (Basis.standard.genericModel.checkedOp (.bin .add))
       (encPair encUnary (encPi encNat)) (encOption encNat) := by
   have hx := (pi_apply encNat (0 : Fin 2)).comp (snd encUnary (encPi encNat))
   have hy := (pi_apply encNat (1 : Fin 2)).comp (snd encUnary (encPi encNat))
-  have hadd := binary_add.comp (hx.prod hy)
-  have hpow := binary_two_pow.comp (fst encUnary (encPi encNat (Index := Fin 2)))
-  change ComputableTidilyInPolyTime
-    (fun p : ℕ × (Fin 2 → ℕ) => if decide (p.2 0 + p.2 1 < 2 ^ p.1)
-      then some (p.2 0 + p.2 1) else none)
-    (encPair encUnary (encPi encNat (Index := Fin 2))) (encOption encNat)
-  simp only [decide_eq_true_eq]
-  exact (binary_lt.comp (hadd.prod hpow)).ite_decide
-    ((optionSome encNat).comp hadd) (const none)
+  exact checkFits_polyTime (binary_add' hx hy)
 
 /-- One native checked-add implementation works at every encoded width. -/
 noncomputable def checkedAddCertificate :
     GenericRAM.NativeCertificate (Basis.standard.genericModel.checkedOp (.bin .add))
       (encPair encUnary (encPi encNat)) (encOption encNat) :=
-  .ofPolyTime checkedAdd_polyTime
+  .ofPolyTime checkedAdd_polyTime.tidy
+
+/-- Every binary operation in `Basis.standard` has a polynomial-time checked implementation. -/
+@[fun_prop, program_certificate]
+theorem checkedBinOp_polyTime (f : BinOp) :
+    ComputableInPolyTime (Basis.standard.genericModel.checkedOp (.bin f))
+      (encPair encUnary (encPi encNat)) (encOption encNat) := by
+  have hw := fst encUnary (encPi encNat (Index := Fin 2))
+  have hx := (pi_apply encNat (0 : Fin 2)).comp (snd encUnary (encPi encNat))
+  have hy := (pi_apply encNat (1 : Fin 2)).comp (snd encUnary (encPi encNat))
+  have hwp := hw.computableInPolyTime
+  have hxp := hx.computableInPolyTime
+  have hyp := hy.computableInPolyTime
+  cases f
+  · exact checkedAdd_polyTime
+  · exact checkFits_polyTime (binary_sub' hx hy)
+  · exact checkFits_polyTime (binary_mul' hx hy)
+  · exact checkFits_polyTime (binary_div' hx hy)
+  · exact checkFits_polyTime (binary_mod' hx hy)
+  · exact checkFits_polyTime (ComputableInPolyTime.binary_and' hxp hyp).tidy
+  · exact checkFits_polyTime (ComputableInPolyTime.binary_or' hxp hyp).tidy
+  · exact checkFits_polyTime (ComputableInPolyTime.binary_xor' hxp hyp).tidy
+  · have h := checkFits_polyTime
+      (binary_mul' hx (binary_two_pow.comp (ComputableInPolyTime.binary_min_unary' hwp hyp).tidy))
+    refine .of_tidy (h.tidy.of_enc_eq fun ⟨w, x⟩ => congrArg (encOption encNat) ?_)
+    exact checkedShiftLeft_eq w (x 0) (x 1)
+  · exact checkFits_polyTime (ComputableInPolyTime.binary_shiftRight' hxp hyp).tidy
+
+/-- Reading the word size in `Basis.standard` is polynomial-time. -/
+@[fun_prop, program_certificate]
+theorem checkedWidth_polyTime :
+    ComputableInPolyTime (Basis.standard.genericModel.checkedOp .width)
+      (encPair encUnary (encPi encNat)) (encOption encNat) :=
+  checkFits_polyTime (unary_to_binary.comp (fst encUnary (encPi encNat (Index := Fin 0))))
+
+/-- Every operation in `Basis.standard` has a polynomial-time checked implementation. -/
+@[fun_prop, program_certificate]
+theorem checkedOp_polyTime (op : StandardOp) :
+    ComputableInPolyTime (Basis.standard.genericModel.checkedOp op)
+      (encPair encUnary (encPi encNat)) (encOption encNat) := by
+  cases op with
+  | bin f => exact checkedBinOp_polyTime f
+  | width => exact checkedWidth_polyTime
+
+/-- Every operation in `Basis.exact` has a polynomial-time checked implementation, preserving
+exact subtraction-underflow and zero-divisor faults. -/
+@[fun_prop, program_certificate]
+theorem checkedExactOp_polyTime (op : StandardOp) :
+    ComputableInPolyTime (Basis.exact.genericModel.checkedOp op)
+      (encPair encUnary (encPi encNat)) (encOption encNat) := by
+  cases op with
+  | width => exact checkedWidth_polyTime
+  | bin f =>
+    have hx := (pi_apply encNat (0 : Fin 2)).comp (snd encUnary (encPi encNat))
+    have hy := (pi_apply encNat (1 : Fin 2)).comp (snd encUnary (encPi encNat))
+    cases f
+    · exact checkedBinOp_polyTime .add
+    · have h := (binary_le' hy hx).ite_decide (checkedBinOp_polyTime .sub).tidy (const none)
+      refine .of_tidy (h.of_enc_eq fun ⟨w, x⟩ => congrArg (encOption encNat) ?_)
+      by_cases hle : x 1 ≤ x 0 <;>
+        simp [Model.checkedOp, Basis.genericModel, StandardOp.evalExact, StandardOp.eval, hle]
+    · exact checkedBinOp_polyTime .mul
+    · have h := ((decide_eq encNat).comp (hy.prod (const 0))).ite_decide
+        (const none) (checkedBinOp_polyTime .div).tidy
+      refine .of_tidy (h.of_enc_eq fun ⟨w, x⟩ => congrArg (encOption encNat) ?_)
+      by_cases hz : x 1 = 0 <;>
+        simp [Model.checkedOp, Basis.genericModel, StandardOp.evalExact, StandardOp.eval, hz]
+    · have h := ((decide_eq encNat).comp (hy.prod (const 0))).ite_decide
+        (const none) (checkedBinOp_polyTime .mod).tidy
+      refine .of_tidy (h.of_enc_eq fun ⟨w, x⟩ => congrArg (encOption encNat) ?_)
+      by_cases hz : x 1 = 0 <;>
+        simp [Model.checkedOp, Basis.genericModel, StandardOp.evalExact, StandardOp.eval, hz]
+    · exact checkedBinOp_polyTime .and
+    · exact checkedBinOp_polyTime .or
+    · exact checkedBinOp_polyTime .xor
+    · exact checkedBinOp_polyTime .shiftLeft
+    · exact checkedBinOp_polyTime .shiftRight
+
+/-- Pull back polynomial-time checked-operation certificates along any map of bases. -/
+theorem Basis.Hom.checkedOp_polyTime {B B' : Basis} (φ : B.Hom B')
+    (hop : ∀ op : B'.Op,
+      ComputableInPolyTime (B'.genericModel.checkedOp op)
+        (encPair encUnary (encPi encNat)) (encOption encNat))
+    (op : B.Op) :
+    ComputableInPolyTime (B.genericModel.checkedOp op)
+      (encPair encUnary (encPi encNat)) (encOption encNat) := by
+  have hargs : ComputableTidilyInPolyTime
+      (fun (p : ℕ × (Fin (B.Arity op) → ℕ)) (a : Fin (B'.Arity (φ.map op))) =>
+        p.2 (Fin.cast (φ.arity_map op) a))
+      (encPair encUnary (encPi encNat)) (encPi encNat) :=
+    pi fun a => (pi_apply encNat (Fin.cast (φ.arity_map op) a)).comp
+      (snd encUnary (encPi encNat))
+  have h := (hop (φ.map op)).tidy.comp ((fst encUnary (encPi encNat)).prod hargs)
+  refine .of_tidy (h.of_enc_eq fun ⟨w, x⟩ => congrArg (encOption encNat) ?_)
+  simp only [Function.comp_apply, Model.checkedOp, Basis.genericModel, φ.interp_map]
+
+/-- Restricting a basis preserves polynomial-time checked-operation certificates definitionally. -/
+theorem Basis.restrict_checkedOp_polyTime (B : Basis) (P : B.Op → Prop)
+    (hop : ∀ op : B.Op,
+      ComputableInPolyTime (B.genericModel.checkedOp op)
+        (encPair encUnary (encPi encNat)) (encOption encNat))
+    (op : (B.restrict P).Op) :
+    ComputableInPolyTime ((B.restrict P).genericModel.checkedOp op)
+      (encPair encUnary (encPi encNat)) (encOption encNat) :=
+  hop op.1
+
+noncomputable section
+
+/-- Package a complete `NativePrimitives` bundle for a word-RAM basis from polynomial-time
+certificates for its operations. -/
+def Basis.nativePrimitivesOfPolyTime (B : Basis)
+    (hop : ∀ op : B.Op,
+      ComputableInPolyTime (B.genericModel.checkedOp op)
+        (encPair encUnary (encPi encNat)) (encOption encNat)) :
+    B.genericModel.NativePrimitives B.encoding where
+  constant c := .ofPolyTime (checkedConstant_polyTime B c).tidy
+  operation op := .ofPolyTime (hop op).tidy
+  test t := .ofPolyTime (evalTest_polyTime B t).tidy
+  address := .ofPolyTime (address_polyTime B).tidy
+  validMove := .ofPolyTime (validMove_polyTime B).tidy
+  validPC := .ofPolyTime (validPC_polyTime B).tidy
+
+/-- Every primitive certificate in `Basis.nativePrimitivesOfPolyTime` has polynomial resource
+bounds. -/
+theorem Basis.nativePrimitivesOfPolyTime_isPolynomial (B : Basis)
+    (hop : ∀ op : B.Op,
+      ComputableInPolyTime (B.genericModel.checkedOp op)
+        (encPair encUnary (encPi encNat)) (encOption encNat)) :
+    (B.nativePrimitivesOfPolyTime hop).IsPolynomial where
+  constant c := NativeCertificate.ofPolyTime_isPolynomial (checkedConstant_polyTime B c).tidy
+  operation op := NativeCertificate.ofPolyTime_isPolynomial (hop op).tidy
+  test t := NativeCertificate.ofPolyTime_isPolynomial (evalTest_polyTime B t).tidy
+  address := NativeCertificate.ofPolyTime_isPolynomial (address_polyTime B).tidy
+  validMove := NativeCertificate.ofPolyTime_isPolynomial (validMove_polyTime B).tidy
+  validPC := NativeCertificate.ofPolyTime_isPolynomial (validPC_polyTime B).tidy
+
+/-- Complete native scalar primitive bundle for `Basis.standard`. -/
+def Basis.standard.nativePrimitives :
+    Basis.standard.genericModel.NativePrimitives Basis.standard.encoding :=
+  Basis.standard.nativePrimitivesOfPolyTime checkedOp_polyTime
+
+/-- The standard word-RAM primitive bundle has polynomial time and space bounds in all fields. -/
+theorem Basis.standard.nativePrimitives_isPolynomial :
+    Basis.standard.nativePrimitives.IsPolynomial :=
+  Basis.standard.nativePrimitivesOfPolyTime_isPolynomial checkedOp_polyTime
+
+/-- Complete native scalar primitive bundle for `Basis.additive`. -/
+def Basis.additive.nativePrimitives :
+    Basis.additive.genericModel.NativePrimitives Basis.additive.encoding :=
+  Basis.additive.nativePrimitivesOfPolyTime
+    (Basis.standard.restrict_checkedOp_polyTime _ checkedOp_polyTime)
+
+/-- The additive word-RAM primitive bundle has polynomial time and space bounds in all fields. -/
+theorem Basis.additive.nativePrimitives_isPolynomial :
+    Basis.additive.nativePrimitives.IsPolynomial :=
+  Basis.additive.nativePrimitivesOfPolyTime_isPolynomial
+    (Basis.standard.restrict_checkedOp_polyTime _ checkedOp_polyTime)
+
+/-- Complete native scalar primitive bundle for `Basis.arithmetic`. -/
+def Basis.arithmetic.nativePrimitives :
+    Basis.arithmetic.genericModel.NativePrimitives Basis.arithmetic.encoding :=
+  Basis.arithmetic.nativePrimitivesOfPolyTime
+    (Basis.standard.restrict_checkedOp_polyTime _ checkedOp_polyTime)
+
+/-- The arithmetic word-RAM primitive bundle has polynomial time and space bounds in all fields. -/
+theorem Basis.arithmetic.nativePrimitives_isPolynomial :
+    Basis.arithmetic.nativePrimitives.IsPolynomial :=
+  Basis.arithmetic.nativePrimitivesOfPolyTime_isPolynomial
+    (Basis.standard.restrict_checkedOp_polyTime _ checkedOp_polyTime)
+
+/-- Complete native scalar primitive bundle for `Basis.exact`. -/
+def Basis.exact.nativePrimitives :
+    Basis.exact.genericModel.NativePrimitives Basis.exact.encoding :=
+  Basis.exact.nativePrimitivesOfPolyTime checkedExactOp_polyTime
+
+/-- The exact word-RAM primitive bundle has polynomial time and space bounds in all fields. -/
+theorem Basis.exact.nativePrimitives_isPolynomial :
+    Basis.exact.nativePrimitives.IsPolynomial :=
+  Basis.exact.nativePrimitivesOfPolyTime_isPolynomial checkedExactOp_polyTime
+
+end
 
 /-! ## Whole-run transport adapter -/
 
@@ -125,7 +411,7 @@ theorem transport_inO (enc : B.genericModel.Encoding) (N : B.genericModel.Native
         FiniteState.runSpace enc N p.toGeneric (steps a, (cfg a, initState a))) :=
   (transportCertificate enc N p cSteps cCfg cInit hden hExec).computes
 
-/-- Automatic `ComputableTidilyInPolyTime` transport corollary from `WordRAM.Executes`. -/
+/-- Automatic `ComputableInPolyTime` transport corollary from `WordRAM.Executes`. -/
 theorem transport_polyTime (enc : B.genericModel.Encoding)
     (N : B.genericModel.NativePrimitives enc)
     (p : Program B r) {f : α → ℕ} {cfg : α → ℕ}
@@ -142,15 +428,15 @@ theorem transport_polyTime (enc : B.genericModel.Encoding)
     (hOutLen : ∀ a, ∀ j ≤ steps a,
       (FiniteState.resultEncoding enc
         (FiniteState.run (cfg a) p.toGeneric j (initState a))).length ≤ bound a) :
-    ComputableTidilyInPolyTime f ei enc.value :=
-  FiniteState.transport_polyTime enc N p.toGeneric cSteps cCfg cInit
+    ComputableInPolyTime f ei enc.value :=
+  .of_tidy <| FiniteState.transport_polyTime enc N p.toGeneric cSteps cCfg cInit
     (fun a => by
       obtain ⟨m, hm, hex⟩ := hExec a
       rw [hden a]
       exact ⟨m, hm, executes_toGeneric_iff.mpr hex⟩)
     hN hSteps hCfg hInit hStepsBound hB hOutLen
 
-/-- Automatic `ComputableTidilyInPolyTime` transport corollary from `WordRAM.Executes` under a
+/-- Automatic `ComputableInPolyTime` transport corollary from `WordRAM.Executes` under a
 constant step-budget bound `∀ a, steps a ≤ K`. -/
 theorem transport_polyTime_of_le_const (enc : B.genericModel.Encoding)
     (N : B.genericModel.NativePrimitives enc)
@@ -164,8 +450,8 @@ theorem transport_polyTime_of_le_const (enc : B.genericModel.Encoding)
     (hN : N.IsPolynomial)
     (hSteps : cSteps.IsPolynomial) (hCfg : cCfg.IsPolynomial) (hInit : cInit.IsPolynomial)
     (K : ℕ) (hStepsLe : ∀ a, steps a ≤ K) :
-    ComputableTidilyInPolyTime f ei enc.value :=
-  FiniteState.transport_polyTime_of_le_const enc N p.toGeneric cSteps cCfg cInit
+    ComputableInPolyTime f ei enc.value :=
+  .of_tidy <| FiniteState.transport_polyTime_of_le_const enc N p.toGeneric cSteps cCfg cInit
     (fun a => by
       obtain ⟨m, hm, hex⟩ := hExec a
       rw [hden a]
diff --git a/Complexity/Tactic/PolyTime.lean b/Complexity/Tactic/PolyTime.lean
index 0087bd0792..e1c9937650 100644
--- a/Complexity/Tactic/PolyTime.lean
+++ b/Complexity/Tactic/PolyTime.lean
@@ -44,9 +44,9 @@ namespace Cslib.Tactic.PolyTime
 
 open Turing.MultiTapeTM
 
--- Plain polynomial time is tidy polynomial time, so plain goals and hypotheses enter the tidy
--- search without loss.
-attribute [aesop safe apply (rule_sets := [PolyTime])] ComputableInPolyTime.of_tidy
+-- Prefer plain certificates before the transitional raw-construction fallback. A safe bridge
+-- would consume a plain goal before its named-certificate alternatives can be considered.
+attribute [aesop unsafe 5% apply (rule_sets := [PolyTime])] ComputableInPolyTime.of_tidy
 attribute [aesop safe forward (rule_sets := [PolyTime])] ComputableInPolyTime.tidy
 
 -- A fixed finite input type admits a lookup machine for any fixed encodings. This does not
@@ -90,12 +90,20 @@ private meta def polytimeListInstance : TacticM Unit := withMainContext do
 attribute [aesop unsafe 75% apply (rule_sets := [PolyTime])]
   ComputableTidilyInPolyTime.pi_apply'
 
+open Lean Meta in
+/-- Select the certificate family before searching, keeping plain goals in the plain calculus. -/
+private meta def polytimePredicate (target : Expr) : MetaM Name := do
+  let target := (← instantiateMVars target).consumeMData
+  if target.isAppOf ``ComputableInPolyTime then return ``ComputableInPolyTime
+  if target.isAppOf ``ComputableTidilyInPolyTime then return ``ComputableTidilyInPolyTime
+  throwError "expected a polynomial-time goal"
+
 /-- Expose local routine certificates and their argument obligations as search alternatives. -/
 -- Equal priority lets argument goals run before expensive alternatives at the parent goal.
 @[aesop unsafe 100% tactic (rule_sets := [PolyTime])]
-private meta def polytimeKnownCall : Aesop.RuleTac :=
-  Cslib.Tactic.applyKnownCall ``ComputableTidilyInPolyTime 2
-    ``ComputableTidilyInPolyTime.comp `g `hf
+private meta def polytimeKnownCall : Aesop.RuleTac := fun input => do
+  let predicate ← input.goal.withContext do polytimePredicate (← input.goal.getType)
+  Cslib.Tactic.applyKnownCall predicate 2 (predicate ++ `comp) `g `hf input
 
 open Lean Meta Elab Tactic in
 /-- Test whether any local routine certificate applies to the current goal. -/
@@ -111,8 +119,7 @@ restores the caller's state and leaves argument preparation open, so this tests
 without choosing an intermediate encoding. -/
 private meta def withoutLocalCall (tactic : TacticM Unit) : TacticM Unit := withMainContext do
   let goal ← getMainGoal
-  unless (← goal.getType).consumeMData.isAppOf ``ComputableTidilyInPolyTime do
-    throwError "expected a polynomial-time goal"
+  discard <| polytimePredicate (← goal.getType)
   if ← hasLocalCall goal then throwError "a local certificate is an alternative to decomposition"
   tactic
 
@@ -120,15 +127,15 @@ open Lean Meta Elab Tactic in
 /-- Retain decomposition as an alternative when a local certificate competes with it. -/
 private meta def withLocalCall (tactic : TacticM Unit) : TacticM Unit := withMainContext do
   let goal ← getMainGoal
-  unless (← goal.getType).consumeMData.isAppOf ``ComputableTidilyInPolyTime do
-    throwError "expected a polynomial-time goal"
+  discard <| polytimePredicate (← goal.getType)
   unless ← hasLocalCall goal do throwError "no competing local certificate"
   tactic
 
 /-- Expose named deterministic certificates as search alternatives. -/
 @[aesop unsafe 99% tactic (rule_sets := [PolyTime])]
-private meta def polytimeCertificate : Aesop.RuleTac :=
-  Cslib.Tactic.applyCertificates ``ComputableTidilyInPolyTime
+private meta def polytimeCertificate : Aesop.RuleTac := fun input => do
+  let predicate ← input.goal.withContext do polytimePredicate (← input.goal.getType)
+  Cslib.Tactic.applyCertificates predicate input
 
 open Lean Meta Elab Tactic in
 /-- Decompose constructors before generic composition can guess intermediate encodings. -/
@@ -154,8 +161,7 @@ open Lean Meta Elab Tactic in
 /-- Let compositional certificates finish a goal before trying loop specifications. -/
 private meta def polytimeFunProp : TacticM Unit :=
   withMainContext <| Term.withoutErrToSorry <| withoutRecover do
-    unless (← getMainTarget).consumeMData.isAppOf ``ComputableTidilyInPolyTime do
-      throwError "expected a polynomial-time goal"
+    discard <| polytimePredicate (← getMainTarget)
     -- A failed compositional attempt must leave time for the specification rules.
     evalTactic (← `(tactic| solve | fun_prop (config := { maxSteps := 256 })))
 
diff --git a/Complexity/Tactic/PolyTime/Init.lean b/Complexity/Tactic/PolyTime/Init.lean
index 832e4c9eae..db5ba3efb9 100644
--- a/Complexity/Tactic/PolyTime/Init.lean
+++ b/Complexity/Tactic/PolyTime/Init.lean
@@ -72,7 +72,8 @@ def efficiencyKey (statement : Expr) : MetaM (Name × Name × Bool) := do
   let statement := statement.consumeMData
   let some predicate := statement.getAppFn.constName?
     | throwError "expected an efficiency statement"
-  let argument := if predicate == `Turing.MultiTapeTM.ComputableTidilyInPolyTime then
+  let argument := if predicate == `Turing.MultiTapeTM.ComputableTidilyInPolyTime ||
+      predicate == `Turing.MultiTapeTM.ComputableInPolyTime then
     statement.getAppArgs[2]! else statement.getAppArgs.back!
   let program ← Core.betaReduce (← etaExpand argument)
   let some (head, encoded) ← lambdaTelescope program fun _ body => pure (programHead? body)
@@ -148,6 +149,7 @@ initialize registerBuiltinAttribute {
         efficiencyKey conclusion
       return (certificate, key)
     if key.1 == `Turing.MultiTapeTM.ComputableTidilyInPolyTime ||
+        key.1 == `Turing.MultiTapeTM.ComputableInPolyTime ||
         key.1 == `Cslib.Probability.IsPPTOn then
       unless ← hasGlobalFunProp certificate do
         Attribute.add certificate `fun_prop .missing kind
diff --git a/ComplexityTests.lean b/ComplexityTests.lean
index 6026c26181..974334c072 100644
--- a/ComplexityTests.lean
+++ b/ComplexityTests.lean
@@ -320,6 +320,7 @@ import ComplexityTests.PolyTimeContracts
 import ComplexityTests.PolyTimeMetadata
 import ComplexityTests.PolyTimeMixes
 import ComplexityTests.PolyTimePlain
+import ComplexityTests.PolyTimePlainDriver
 import ComplexityTests.PolyTimeScans
 import ComplexityTests.PolyTimeSearch
 import ComplexityTests.PolyTimeSum
diff --git a/ComplexityTests/GenericRAMNative.lean b/ComplexityTests/GenericRAMNative.lean
index e801bca994..cc7d7d85fd 100644
--- a/ComplexityTests/GenericRAMNative.lean
+++ b/ComplexityTests/GenericRAMNative.lean
@@ -69,14 +69,70 @@ example : addressAccepted.IsPolynomial :=
 example : IsComputable (fun p => (model.address p.1 p.2).isSome)
     (encPair encNat encNat) encBool := addressAccepted.isComputable
 
--- Named certificates are reused without unfolding their implementations.
+-- Named certificates are reused without unfolding their implementations (via both `polytime` and
+-- `fun_prop`).
 example : ComputableTidilyInPolyTime (model.checkedOp ())
     (encPair encNat (encPi encNat)) (encOption encNat) := by polytime
 example : ComputableTidilyInPolyTime
     (fun k => (model.checkedConstant 7 k).getD 0) encNat encNat := by polytime
-example : ComputableTidilyInPolyTime
+example : ComputableInPolyTime
     (Cslib.WordRAM.Basis.standard.genericModel.checkedOp (.bin .add))
     (encPair encUnary (encPi encNat)) (encOption encNat) := by polytime
+example (op : Cslib.WordRAM.StandardOp) : ComputableInPolyTime
+    (Cslib.WordRAM.Basis.standard.genericModel.checkedOp op)
+    (encPair encUnary (encPi encNat)) (encOption encNat) := by polytime
+example (op : Cslib.WordRAM.StandardOp) : ComputableInPolyTime
+    (Cslib.WordRAM.Basis.exact.genericModel.checkedOp op)
+    (encPair encUnary (encPi encNat)) (encOption encNat) := by polytime
+example (op : Cslib.WordRAM.Basis.additive.Op) : ComputableInPolyTime
+    (Cslib.WordRAM.Basis.additive.genericModel.checkedOp op)
+    (encPair encUnary (encPi encNat)) (encOption encNat) := by polytime
+example (op : Cslib.WordRAM.Basis.arithmetic.Op) : ComputableInPolyTime
+    (Cslib.WordRAM.Basis.arithmetic.genericModel.checkedOp op)
+    (encPair encUnary (encPi encNat)) (encOption encNat) := by polytime
+example (B : Cslib.WordRAM.Basis) (c : ℕ) : ComputableInPolyTime
+    (B.genericModel.checkedConstant c) encUnary (encOption encNat) := by polytime
+example (B : Cslib.WordRAM.Basis) (c : ℕ) : ComputableInPolyTime
+    (B.genericModel.checkedConstant c) encUnary (encOption encNat) := by fun_prop
+example (B : Cslib.WordRAM.Basis) (t : Bool) : ComputableInPolyTime
+    (fun p => B.genericModel.evalTest p.1 t p.2)
+    (encPair encUnary (encPi encNat)) (encOption encBool) := by polytime
+example (B : Cslib.WordRAM.Basis) : ComputableInPolyTime
+    (fun p => B.genericModel.address p.1 p.2)
+    (encPair encUnary encNat) (encOption encNat) := by polytime
+example (B : Cslib.WordRAM.Basis) : ComputableInPolyTime
+    (fun p => B.genericModel.validMove p.1 p.2)
+    (encPair encUnary encNat) encBool := by polytime
+example (B : Cslib.WordRAM.Basis) : ComputableInPolyTime
+    (fun p => B.genericModel.validPC p.1 p.2)
+    (encPair encUnary encNat) encBool := by polytime
+example (op : Cslib.WordRAM.StandardOp) : ComputableInPolyTime
+    (Cslib.WordRAM.Basis.standard.genericModel.checkedOp op)
+    (encPair encUnary (encPi encNat)) (encOption encNat) := by fun_prop
+example (op : Cslib.WordRAM.StandardOp) : ComputableInPolyTime
+    (Cslib.WordRAM.Basis.exact.genericModel.checkedOp op)
+    (encPair encUnary (encPi encNat)) (encOption encNat) := by fun_prop
+
+-- Binary bitwise, right-shift, bit-length, and unary-capped minimum plain certificates.
+example : ComputableInPolyTime (fun p : ℕ × ℕ => p.1 &&& p.2)
+    (encPair encNat encNat) encNat := by polytime
+example : ComputableInPolyTime (fun p : ℕ × ℕ => p.1 &&& p.2)
+    (encPair encNat encNat) encNat := by fun_prop
+example : ComputableInPolyTime (fun p : ℕ × ℕ => p.1 ||| p.2)
+    (encPair encNat encNat) encNat := by polytime
+example : ComputableInPolyTime (fun p : ℕ × ℕ => p.1 ^^^ p.2)
+    (encPair encNat encNat) encNat := by polytime
+example : ComputableInPolyTime (fun p : ℕ × ℕ => p.1 >>> p.2)
+    (encPair encNat encNat) encNat := by polytime
+example : ComputableInPolyTime Nat.size encNat encUnary := by polytime
+example : ComputableInPolyTime Nat.size encNat encUnary := by fun_prop
+example : ComputableInPolyTime (fun p : ℕ × ℕ => min p.1 p.2)
+    (encPair encUnary encNat) encUnary := by polytime
+example : ComputableInPolyTime (fun p : ℕ × ℕ => min p.1 p.2)
+    (encPair encUnary encNat) encUnary := by fun_prop
+example : ComputableInPolyTime
+    (fun p : List ℕ × ℕ => (p.1.foldl (fun acc _ => acc) p.2) &&& p.2)
+    (encPair (encList encNat) encNat) encNat := by polytime
 
 -- Literals, results, tests, addresses, moves and labels have live rejection paths.
 example : model.checkedConstant 3 4 = some 3 := by decide
@@ -121,13 +177,47 @@ example (k : ℕ) (x : Data model 2) :
 
 -- WordRAM uses an exclusive bound 2^w, so width zero still admits zero.
 private abbrev word := Cslib.WordRAM.Basis.standard.genericModel
+private abbrev exactWord := Cslib.WordRAM.Basis.exact.genericModel
 example : word.checkedOp (.bin .add) (0, ![0, 0]) = some 0 := by decide
 example : word.checkedOp (.bin .add) (0, ![0, 1]) = none := by decide
 example : word.checkedOp (.bin .add) (2, ![1, 2]) = some 3 := by decide
 example : word.checkedOp (.bin .add) (2, ![2, 2]) = none := by decide
 example : word.checkedOp (.bin .add) (3, ![2, 2]) = some 4 := by decide
+example : word.checkedOp .width (0, ![]) = some 0 := by decide
+example : word.checkedOp .width (1, ![]) = some 1 := by decide
+example : word.checkedOp .width (2, ![]) = some 2 := by decide
+example : word.checkedOp (.bin .and) (2, ![3, 1]) = some 1 := by decide
+example : word.checkedOp (.bin .or) (2, ![2, 1]) = some 3 := by decide
+example : word.checkedOp (.bin .xor) (2, ![3, 1]) = some 2 := by decide
+example : word.checkedOp (.bin .shiftRight) (2, ![6, 1]) = some 3 := by decide
+example : word.checkedOp (.bin .shiftRight) (1, ![6, 1]) = none := by decide
+example : word.checkedOp (.bin .shiftLeft) (3, ![1, 2]) = some 4 := by decide
+example : word.checkedOp (.bin .shiftLeft) (2, ![1, 2]) = none := by decide
+-- Large shift counts y > w preserve zero and reject nonzero left shifts.
+example : word.checkedOp (.bin .shiftLeft) (2, ![0, 100]) = some 0 := by decide
+example : word.checkedOp (.bin .shiftLeft) (2, ![1, 100]) = none := by decide
+-- Standard saturating/zero-default arithmetic vs. exact partial arithmetic on underflow/zero-div.
+example : word.checkedOp (.bin .sub) (2, ![2, 3]) = some 0 := by decide
+example : exactWord.checkedOp (.bin .sub) (2, ![2, 3]) = none := by decide
+example : exactWord.checkedOp (.bin .sub) (2, ![3, 2]) = some 1 := by decide
+example : word.checkedOp (.bin .div) (2, ![3, 0]) = some 0 := by decide
+example : exactWord.checkedOp (.bin .div) (2, ![3, 0]) = none := by decide
+example : exactWord.checkedOp (.bin .div) (2, ![3, 2]) = some 1 := by decide
+example : word.checkedOp (.bin .mod) (2, ![3, 0]) = some 3 := by decide
+example : exactWord.checkedOp (.bin .mod) (2, ![3, 0]) = none := by decide
+example : exactWord.checkedOp (.bin .mod) (2, ![3, 2]) = some 1 := by decide
+
+-- Complete native primitive bundles for standard, additive, arithmetic, and exact bases.
 example : Cslib.WordRAM.checkedAddCertificate.IsPolynomial :=
-  NativeCertificate.ofPolyTime_isPolynomial Cslib.WordRAM.checkedAdd_polyTime
+  NativeCertificate.ofPolyTime_isPolynomial Cslib.WordRAM.checkedAdd_polyTime.tidy
+example : Cslib.WordRAM.Basis.standard.nativePrimitives.IsPolynomial :=
+  Cslib.WordRAM.Basis.standard.nativePrimitives_isPolynomial
+example : Cslib.WordRAM.Basis.additive.nativePrimitives.IsPolynomial :=
+  Cslib.WordRAM.Basis.additive.nativePrimitives_isPolynomial
+example : Cslib.WordRAM.Basis.arithmetic.nativePrimitives.IsPolynomial :=
+  Cslib.WordRAM.Basis.arithmetic.nativePrimitives_isPolynomial
+example : Cslib.WordRAM.Basis.exact.nativePrimitives.IsPolynomial :=
+  Cslib.WordRAM.Basis.exact.nativePrimitives_isPolynomial
 
 /--
 info: 'Cslib.GenericRAM.NativeCertificate.nonempty_iff_isComputable' depends on axioms: [propext, Classical.choice, Quot.sound]
@@ -145,9 +235,64 @@ info: 'Cslib.GenericRAM.BoundedNat.nativePrimitives' depends on axioms: [propext
 #guard_msgs (whitespace := lax) in
 #print axioms BoundedNat.nativePrimitives
 /--
+info: 'Turing.MultiTapeTM.ComputableInPolyTime.binary_bitwise' depends on axioms: [propext, Classical.choice, Quot.sound]
+-/
+#guard_msgs (whitespace := lax) in
+#print axioms Turing.MultiTapeTM.ComputableInPolyTime.binary_bitwise
+/--
+info: 'Turing.MultiTapeTM.ComputableInPolyTime.binary_shiftRight' depends on axioms: [propext, Classical.choice, Quot.sound]
+-/
+#guard_msgs (whitespace := lax) in
+#print axioms Turing.MultiTapeTM.ComputableInPolyTime.binary_shiftRight
+/--
+info: 'Turing.MultiTapeTM.ComputableInPolyTime.binary_min_unary' depends on axioms: [propext, Classical.choice, Quot.sound]
+-/
+#guard_msgs (whitespace := lax) in
+#print axioms Turing.MultiTapeTM.ComputableInPolyTime.binary_min_unary
+/--
 info: 'Cslib.WordRAM.checkedAdd_polyTime' depends on axioms: [propext, Classical.choice, Quot.sound]
 -/
 #guard_msgs (whitespace := lax) in
 #print axioms Cslib.WordRAM.checkedAdd_polyTime
+/--
+info: 'Cslib.WordRAM.Basis.standard.nativePrimitives' depends on axioms: [propext, Classical.choice, Quot.sound]
+-/
+#guard_msgs (whitespace := lax) in
+#print axioms Cslib.WordRAM.Basis.standard.nativePrimitives
+/--
+info: 'Cslib.WordRAM.Basis.standard.nativePrimitives_isPolynomial' depends on axioms: [propext, Classical.choice, Quot.sound]
+-/
+#guard_msgs (whitespace := lax) in
+#print axioms Cslib.WordRAM.Basis.standard.nativePrimitives_isPolynomial
+/--
+info: 'Cslib.WordRAM.Basis.additive.nativePrimitives' depends on axioms: [propext, Classical.choice, Quot.sound]
+-/
+#guard_msgs (whitespace := lax) in
+#print axioms Cslib.WordRAM.Basis.additive.nativePrimitives
+/--
+info: 'Cslib.WordRAM.Basis.additive.nativePrimitives_isPolynomial' depends on axioms: [propext, Classical.choice, Quot.sound]
+-/
+#guard_msgs (whitespace := lax) in
+#print axioms Cslib.WordRAM.Basis.additive.nativePrimitives_isPolynomial
+/--
+info: 'Cslib.WordRAM.Basis.arithmetic.nativePrimitives' depends on axioms: [propext, Classical.choice, Quot.sound]
+-/
+#guard_msgs (whitespace := lax) in
+#print axioms Cslib.WordRAM.Basis.arithmetic.nativePrimitives
+/--
+info: 'Cslib.WordRAM.Basis.arithmetic.nativePrimitives_isPolynomial' depends on axioms: [propext, Classical.choice, Quot.sound]
+-/
+#guard_msgs (whitespace := lax) in
+#print axioms Cslib.WordRAM.Basis.arithmetic.nativePrimitives_isPolynomial
+/--
+info: 'Cslib.WordRAM.Basis.exact.nativePrimitives' depends on axioms: [propext, Classical.choice, Quot.sound]
+-/
+#guard_msgs (whitespace := lax) in
+#print axioms Cslib.WordRAM.Basis.exact.nativePrimitives
+/--
+info: 'Cslib.WordRAM.Basis.exact.nativePrimitives_isPolynomial' depends on axioms: [propext, Classical.choice, Quot.sound]
+-/
+#guard_msgs (whitespace := lax) in
+#print axioms Cslib.WordRAM.Basis.exact.nativePrimitives_isPolynomial
 
 end ComplexityTests.GenericRAMNative
diff --git a/ComplexityTests/GenericRAMSimulation.lean b/ComplexityTests/GenericRAMSimulation.lean
index 1a46e03796..e13ca96fe8 100644
--- a/ComplexityTests/GenericRAMSimulation.lean
+++ b/ComplexityTests/GenericRAMSimulation.lean
@@ -11,7 +11,9 @@ public import Complexity.Computability.GenericRAM.Simulation.Turing
 public import Complexity.Computability.GenericRAM.Simulation.Run
 public import Complexity.Computability.GenericRAM.Native.Nat
 public import Complexity.Computability.WordRAM.Native
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat
 import Mathlib.Data.Fin.VecNotation
+import Mathlib.Data.Nat.Size
 
 /-!
 # Finite RAM simulation, multi-step execution, and native transport checks
@@ -368,6 +370,123 @@ theorem double_step_polyTime :
       (FiniteState.inputEncoding encoding) (FiniteState.resultEncoding encoding) :=
   FiniteState.step_polyTime encoding nativePrimitives doubleProgram nativePrimitives_isPolynomial
 
+/-! ### End-to-end WordRAM program transport over `Basis.standard` -/
+
+/-- Five-instruction `Basis.standard` word-RAM program that clears register `0` via bitwise XOR,
+stores `x` (initially in register `1`) at memory address `0`, loads it back into register `0`,
+adds registers `0` and `1`, and halts returning `x + x`. -/
+def wordDoubleProgram : Cslib.WordRAM.Program Cslib.WordRAM.Basis.standard 2 :=
+  [.op (.alu (.bin .xor) 0 ![0, 0]),
+   .op (.store 0 1),
+   .op (.load 0 0),
+   .op (.alu (.bin .add) 1 ![0, 1]),
+   .halt 1]
+
+/-- Initial finite generic state for `wordDoubleProgram` with both registers set to `x`. -/
+def wordDoubleInit (x : ℕ) : FiniteState Cslib.WordRAM.Basis.standard.genericModel 2 :=
+  FiniteState.initConst x 0 ∅
+
+/-- Corresponding semantic `WordRAM.State` with both registers set to `x` and zeroed memory. -/
+def wordDoubleState (x : ℕ) : Cslib.WordRAM.State 2 :=
+  ⟨0, ⟨fun _ => x, fun _ => 0⟩⟩
+
+/-- Native certificate for `wordDoubleInit`. -/
+noncomputable def wordDoubleInitCert :
+    NativeCertificate wordDoubleInit encNat
+      (FiniteState.encoding Cslib.WordRAM.Basis.standard.encoding) :=
+  FiniteState.initConstCertificate (r := 2) Cslib.WordRAM.Basis.standard.encoding
+    (NativeCertificate.linear ComputableTidilyInDegree.id'.inO_one)
+    (NativeCertificate.const 0)
+    (NativeCertificate.const ∅)
+
+theorem wordDoubleInitCert_isPolynomial : wordDoubleInitCert.IsPolynomial :=
+  FiniteState.initConstCertificate_isPolynomial (r := 2) Cslib.WordRAM.Basis.standard.encoding _ _ _
+    (NativeCertificate.linear_isPolynomial ComputableTidilyInDegree.id'.inO_one)
+    (NativeCertificate.const_isPolynomial 0)
+    (NativeCertificate.const_isPolynomial ∅)
+
+/-- Runtime word width `x.size + 2` (encoded in unary), accommodating `0`, `x`, and `x + x`. -/
+def wordDoubleWidth (x : ℕ) : ℕ := x.size + 2
+
+theorem wordDoubleWidth_polyTime :
+    ComputableInPolyTime wordDoubleWidth encNat encUnary :=
+  .of_tidy <| ComputableTidilyInPolyTime.unary_add.comp
+    (ComputableInPolyTime.binary_size.tidy.prod (ComputableTidilyInPolyTime.const 2))
+
+/-- Native certificate for `wordDoubleWidth`. -/
+noncomputable def wordDoubleWidthCert : NativeCertificate wordDoubleWidth encNat encUnary :=
+  .ofPolyTime wordDoubleWidth_polyTime.tidy
+
+theorem wordDoubleWidthCert_isPolynomial : wordDoubleWidthCert.IsPolynomial :=
+  NativeCertificate.ofPolyTime_isPolynomial wordDoubleWidth_polyTime.tidy
+
+/-- Constant step budget `5` for `wordDoubleProgram`. -/
+noncomputable def wordDoubleStepsCert : NativeCertificate (fun _ : ℕ => 5) encNat encNat :=
+  NativeCertificate.const 5
+
+theorem wordDoubleStepsCert_isPolynomial : wordDoubleStepsCert.IsPolynomial :=
+  NativeCertificate.const_isPolynomial 5
+
+/-- `wordDoubleProgram.toGeneric` halts in `5` steps with output `x + x` at width
+`wordDoubleWidth x` from initial state `wordDoubleInit x`. -/
+theorem wordDoubleProgram_run (x : ℕ) :
+    FiniteState.run (wordDoubleWidth x) wordDoubleProgram.toGeneric 5 (wordDoubleInit x) =
+      some (.inr (x + x)) := by
+  have hfit0 : Cslib.WordRAM.Fits (wordDoubleWidth x) 0 := Cslib.WordRAM.fits_zero _
+  have hfitxx : Cslib.WordRAM.Fits (wordDoubleWidth x) (x + x) := by
+    rw [Cslib.WordRAM.fits_iff, wordDoubleWidth]
+    have hx : x < 2 ^ x.size := Nat.lt_size_self x
+    have hpow : 2 ^ (x.size + 2) = 4 * 2 ^ x.size := by ring
+    omega
+  have hmem : SparseMemory.read 0 (0 : ℕ) (AList.singleton 0 x) = x := by
+    simpa using congrFun (SparseMemory.read_insert 0 (0 : ℕ) x ∅) 0
+  simp only [wordDoubleProgram, Cslib.WordRAM.Program.toGeneric, List.map_cons, List.map_nil,
+    Cslib.WordRAM.Instr.toGeneric, Cslib.WordRAM.Op.toGeneric]
+  simp [FiniteState.run, FiniteState.step, FiniteState.dispatch, FiniteState.evalInstr,
+    FiniteState.evalOp, FiniteState.resume, FiniteState.set, FiniteState.write, FiniteState.move,
+    Model.checkedOp, wordDoubleInit, FiniteState.initConst, FiniteState.init,
+    Cslib.WordRAM.Basis.genericModel, Cslib.WordRAM.Basis.standard,
+    Cslib.WordRAM.StandardOp.eval, Cslib.WordRAM.BinOp.eval, hfit0, hfitxx, hmem]
+
+/-- `wordDoubleProgram` satisfies semantic `WordRAM.Executes` within `5` steps for all `x`. -/
+theorem wordDoubleProgram_executes (x : ℕ) :
+    ∃ m ≤ 5, Cslib.WordRAM.Executes (wordDoubleWidth x) wordDoubleProgram
+      (wordDoubleState x) (x + x) m := by
+  obtain ⟨m, hm, hex⟩ := FiniteState.executes_of_run_eq_inr (wordDoubleProgram_run x)
+  exact ⟨m, hm, Cslib.WordRAM.executes_toGeneric_iff.mp hex⟩
+
+/-- Whole-run `ComputableTidilyInO` bound transported from `wordDoubleProgram` via
+`Cslib.WordRAM.transport_inO` and `Basis.standard.nativePrimitives`. -/
+theorem wordDouble_inO :
+    ComputableTidilyInO (fun x : ℕ => x + x) encNat encNat
+      (fun x => wordDoubleStepsCert.time x +
+        (wordDoubleWidthCert.time x + wordDoubleInitCert.time x) +
+        FiniteState.runTime Cslib.WordRAM.Basis.standard.encoding
+          Cslib.WordRAM.Basis.standard.nativePrimitives wordDoubleProgram.toGeneric
+          (5, (wordDoubleWidth x, wordDoubleInit x)))
+      (fun x => wordDoubleStepsCert.space x +
+        (wordDoubleWidthCert.space x + wordDoubleInitCert.space x) +
+        FiniteState.runSpace Cslib.WordRAM.Basis.standard.encoding
+          Cslib.WordRAM.Basis.standard.nativePrimitives wordDoubleProgram.toGeneric
+          (5, (wordDoubleWidth x, wordDoubleInit x))) :=
+  Cslib.WordRAM.transport_inO Cslib.WordRAM.Basis.standard.encoding
+    Cslib.WordRAM.Basis.standard.nativePrimitives wordDoubleProgram
+    wordDoubleStepsCert wordDoubleWidthCert wordDoubleInitCert
+    (fun _ => rfl) wordDoubleProgram_executes
+
+/-- Automatic `ComputableInPolyTime` transport for `wordDoubleProgram` via
+`Cslib.WordRAM.transport_polyTime_of_le_const` and `Basis.standard.nativePrimitives`. -/
+theorem wordDouble_polyTime :
+    ComputableInPolyTime (fun x : ℕ => x + x) encNat encNat :=
+  Cslib.WordRAM.transport_polyTime_of_le_const Cslib.WordRAM.Basis.standard.encoding
+    Cslib.WordRAM.Basis.standard.nativePrimitives wordDoubleProgram
+    wordDoubleStepsCert wordDoubleWidthCert wordDoubleInitCert
+    (fun _ => rfl) wordDoubleProgram_executes
+    Cslib.WordRAM.Basis.standard.nativePrimitives_isPolynomial
+    wordDoubleStepsCert_isPolynomial wordDoubleWidthCert_isPolynomial
+    wordDoubleInitCert_isPolynomial
+    5 (fun _ => le_rfl)
+
 /--
 info: 'Turing.MultiTapeTM.ComputableTidilyInO.inl' depends on axioms: [propext, Classical.choice, Quot.sound]
 -/
@@ -482,4 +601,10 @@ info: 'ComplexityTests.GenericRAMSimulation.double_polyTime' depends on axioms:
 #guard_msgs (whitespace := lax) in
 #print axioms double_polyTime
 
+/--
+info: 'ComplexityTests.GenericRAMSimulation.wordDouble_polyTime' depends on axioms: [propext, Classical.choice, Quot.sound]
+-/
+#guard_msgs (whitespace := lax) in
+#print axioms wordDouble_polyTime
+
 end ComplexityTests.GenericRAMSimulation
diff --git a/ComplexityTests/PolyTimePlainDriver.lean b/ComplexityTests/PolyTimePlainDriver.lean
new file mode 100644
index 0000000000..8994c065f4
--- /dev/null
+++ b/ComplexityTests/PolyTimePlainDriver.lean
@@ -0,0 +1,51 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+import Complexity.Computability.WordRAM.Native
+import Complexity.Tactic.PolyTime
+
+/-! Plain `polytime` must invoke compositional, captured-local and named certificates. -/
+
+open Turing.MultiTapeTM
+
+example : ComputableInPolyTime (fun p : ℕ × ℕ => p.1 &&& p.2)
+    (encPair encNat encNat) encNat := by fun_prop
+
+example : ComputableInPolyTime (fun p : ℕ × ℕ => p.1 &&& p.2)
+    (encPair encNat encNat) encNat := by polytime
+
+example (B : Cslib.WordRAM.Basis) (c : ℕ) : ComputableInPolyTime
+    (B.genericModel.checkedConstant c) encUnary (encOption encNat) := by fun_prop
+
+example (B : Cslib.WordRAM.Basis) (c : ℕ) : ComputableInPolyTime
+    (B.genericModel.checkedConstant c) encUnary (encOption encNat) := by polytime
+
+example (routine : ℕ × ℕ → ℕ)
+    (hroutine : ComputableInPolyTime routine (encPair encNat encNat) encNat) :
+    ComputableInPolyTime (fun p : ℕ × ℕ => routine (p.2, p.1))
+      (encPair encNat encNat) encNat := by polytime
+
+namespace PlainDriverTests
+
+-- Keep this body opaque to compositional search: the named certificate carries the contract.
+@[irreducible] def checkedNamedConstant (B : Cslib.WordRAM.Basis) (limit c w : ℕ) : Option ℕ :=
+  if c ≤ limit then B.genericModel.checkedConstant c w else none
+
+@[program_certificate hbound]
+theorem checkedNamedConstant_polyTime (B : Cslib.WordRAM.Basis) (limit c : ℕ)
+    (hbound : c ≤ limit) : ComputableInPolyTime (checkedNamedConstant B limit c)
+      encUnary (encOption encNat) := by
+  unfold checkedNamedConstant
+  simp only [ite_eq_left hbound]
+  exact Cslib.WordRAM.checkedConstant_polyTime B c
+
+-- `fun_prop` cannot discharge the contract; named lookup must expose and solve it through Aesop.
+example (B : Cslib.WordRAM.Basis) (c : ℕ) :
+    ComputableInPolyTime (checkedNamedConstant B c c) encUnary (encOption encNat) := by
+  fail_if_success fun_prop
+  polytime
+
+end PlainDriverTests
diff --git a/ROADMAP.md b/ROADMAP.md
index 5d208cc9a0..cc0db33671 100644
--- a/ROADMAP.md
+++ b/ROADMAP.md
@@ -1469,8 +1469,10 @@ space bounds. Further class-level work needs resource certificates for the actua
   native TM time/space bounds; it is equivalent to native computability when bounds are unrestricted.
   Polynomial bounds yield native polynomial time. A
   [bounded-natural addition model](Complexity/Computability/GenericRAM/Native/Nat.lean) supplies every
-  scalar certificate, and [checked word addition](Complexity/Computability/WordRAM/Native.lean)
-  handles all unary-encoded widths with binary operands. The native tidy calculus has
+  scalar certificate, and [WordRAM native primitives](Complexity/Computability/WordRAM/Native.lean)
+  supply complete polynomial-time `NativePrimitives` bundles for `Basis.standard`, `Basis.additive`,
+  `Basis.arithmetic`, and `Basis.exact` (plus restricted sub-bases and homomorphic preimages) across
+  all unary-encoded widths with binary operands (#489). The native tidy calculus has
   [fixed finite tuple rules](Complexity/Computability/Machines/Turing/MultiTape/Complexity/BigO/Pi.lean)
   with linear access/gather/update and arbitrary summed construction bounds,
   [retained-input option elimination](Complexity/Computability/Machines/Turing/MultiTape/Complexity/BigO/Option.lean)
diff --git a/UPSTREAM.md b/UPSTREAM.md
index b31b3bc127..b4615ee6e6 100644
--- a/UPSTREAM.md
+++ b/UPSTREAM.md
@@ -115,7 +115,9 @@ Do not add a ledger row for an ordinary candidate or repeat its source marker he
   encoded scalar primitives, with caller-selected configuration encoding and unrestricted
   input-dependent bounds. Its forgetful bridge reuses `IsComputable`; polynomiality is a separate
   bound property. `GenericRAM/Native/Nat` supplies a checked bounded-natural addition model;
-  `WordRAM/Native` certifies checked standard addition with unary width and binary operands.
+  `WordRAM/Native` supplies complete polynomial-time `NativePrimitives` bundles for
+  `Basis.standard`, `Basis.additive`, `Basis.arithmetic`, and `Basis.exact` (plus restricted
+  sub-bases and homomorphic preimages) with unary width and binary operands (#489).
   Both reuse Christian Reitwiessner's native arithmetic/encoding calculus.
   `GenericRAM/Simulation/{Finite,Turing,Run}` combine these per-symbol certificates with sparse
   memory and finite control to simulate single steps and clocked multi-step runs of any fixed