fix(polytime): diagnose unsupported certificate predicates

Complexity/Tactic/PolyTime/Init.lean

@@ -72,6 +72,14 @@ def efficiencyKey (statement : Expr) : MetaM (Name × Name × Bool) := do
   let statement := statement.consumeMData
   let some predicate := statement.getAppFn.constName?
     | throwError "expected an efficiency statement"
+  unless predicate == `Turing.MultiTapeTM.ComputableInPolyTime ||
+      predicate == `Turing.MultiTapeTM.ComputableTidilyInPolyTime ||
+      predicate == `Cslib.Probability.IsPPTOn || predicate == `Cslib.Probability.IsPPT ||
+      predicate == `Cslib.WordRAM.Refines ||
+      predicate == `Cslib.WordRAM.ComputableInPolyTime ||
+      predicate == `Cslib.WordRAM.UniformComputableInPolyTime do
+    throwError "unsupported efficiency predicate `{predicate}` for `program_certificate`; \
+      expected TM polynomial time, PPT, or a documented word-RAM certificate"
   let argument := if predicate == `Turing.MultiTapeTM.ComputableTidilyInPolyTime ||
       predicate == `Turing.MultiTapeTM.ComputableInPolyTime then
     statement.getAppArgs[2]! else statement.getAppArgs.back!
@@ -126,8 +134,11 @@ private def hasGlobalFunProp (decl : Name) : CoreM Bool := do
     (← hasGlobalEntry transitionTheoremsExt (·.thmName) decl)
 
 /-- `@[program_certificate]` registers an efficiency certificate for `polytime` and `ppt`. Its
-conclusion must be a `ComputableTidilyInPolyTime`, `IsPPTOn` or `IsPPT` statement whose program
-body applies a constant, possibly under an output encoding.
+conclusion must be a `ComputableInPolyTime`, `ComputableTidilyInPolyTime`, `IsPPTOn` or `IsPPT`
+statement, or one of the word-RAM predicates `WordRAM.Refines`, `WordRAM.ComputableInPolyTime`,
+`WordRAM.UniformComputableInPolyTime` used by `Tactic.WordRAM`. The indexed argument must apply
+a constant, possibly under an output encoding. Other predicates are rejected rather than indexed
+by an unrelated final argument.
 Certificates are also registered with `fun_prop` for use in larger compositions, unless the same
 declaration already has a global registration.
 

ComplexityTests.lean

@@ -349,6 +349,7 @@ import ComplexityTests.ProbabilityNotation
 import ComplexityTests.ProbabilityToolkit
 import ComplexityTests.ProbabilityToolkit2
 import ComplexityTests.ProbabilityToolkit3
+import ComplexityTests.ProgramCertificateDiagnostics
 import ComplexityTests.Programs
 import ComplexityTests.ProofComplexity
 import ComplexityTests.ProofComplexity.Pigeonhole

ComplexityTests/ProgramCertificateDiagnostics.lean

@@ -0,0 +1,66 @@
+/-
+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.Crypto.Computational.Signature
+import Complexity.Crypto.Computational.MAC
+import ComplexityTests.PolyTimePlainDriver
+
+/-! Actual imported verification projections must be indexed by their programs. Unsupported
+predicates must not silently register an inert certificate under their last argument. -/
+
+open Turing.MultiTapeTM Cslib.Crypto
+
+run_meta do
+  for (certificate, program) in
+      [(`Cslib.Crypto.SignatureScheme.verify_polyTime, `Cslib.Crypto.SignatureScheme.verify),
+       (`Cslib.Crypto.MACScheme.verify_polyTime, `Cslib.Crypto.MACScheme.verify)] do
+    let type := (← Lean.getConstInfo certificate).type
+    let key ← Lean.Meta.forallTelescope type fun _ conclusion =>
+      Cslib.Tactic.efficiencyKey conclusion
+    unless key == (`Turing.MultiTapeTM.ComputableInPolyTime, program, false) do
+      throwError "incorrect imported verification key: {key}"
+    let entries := (Cslib.Tactic.certificateExt.getState (← Lean.getEnv)).getD key #[]
+    unless entries.any (fun entry => entry.1 == certificate) do
+      throwError "actual verification certificate absent from its program key: {certificate}"
+
+example (S : SignatureScheme) : ComputableInPolyTime
+    (fun p : List Bool × List Bool × List Bool => S.verify p.1 p.2.1 p.2.2)
+    (encPair encBits (encPair encBits encBits)) encBool := by polytime
+
+example (M : MACScheme) : ComputableInPolyTime
+    (fun p : List Bool × List Bool × List Bool => M.verify p.1 p.2.1 p.2.2)
+    (encPair encBits (encPair encBits encBits)) encBool := by polytime
+
+-- This existing irreducible routine and certificate come from another ordinary module import.
+-- The eager contract prevents fun_prop alone from hiding an inert named-certificate path.
+example (B : Cslib.WordRAM.Basis) (c : ℕ) : ComputableInPolyTime
+    (PlainDriverTests.checkedNamedConstant B c c) encUnary (encOption encNat) := by
+  fail_if_success fun_prop
+  polytime
+
+namespace ProgramCertificateDiagnostics
+
+def NotEfficiency (_ : List Bool → List Bool) : Prop := True
+
+theorem wrongPredicate : NotEfficiency List.reverse := True.intro
+
+/--
+error: unsupported efficiency predicate `ProgramCertificateDiagnostics.NotEfficiency` for
+`program_certificate`; expected TM polynomial time, PPT, or a documented word-RAM certificate
+-/
+#guard_msgs (whitespace := lax) in
+attribute [program_certificate] wrongPredicate
+
+theorem noProgram : True := True.intro
+
+/--
+error: unsupported efficiency predicate `True` for `program_certificate`; expected
+TM polynomial time, PPT, or a documented word-RAM certificate
+-/
+#guard_msgs (whitespace := lax) in
+attribute [program_certificate] noProgram
+
+end ProgramCertificateDiagnostics