feat(polytime): report a failed certificate subterm

Complexity/Tactic/PolyTime.lean

@@ -28,6 +28,9 @@ are unfolded. `fun_prop` handles composition; Aesop chooses loop rules and uses
 contracts. Plain and internal tidy goals use separate rules, with fixed machines and polynomial
 bounds across all encoded inputs. Plain search applies plain statements directly; it does not
 lower a goal or restate its hypotheses tidily. Unknown algorithms still require certificates.
+On ordinary failure, `polytime` includes one failed compositional attempt when the backend has
+reported one. This is a search hint, not a claim that the subterm is uncomputable. Resource-limit
+and interrupt exceptions are unchanged.
 
 ## Main definitions
 
@@ -610,6 +613,28 @@ private meta def polytimeConditionalFast : TacticM Unit := withMainContext do
     catch _ => before.restore
   throwError "no supplied-guard conditional proof closed all premises"
 
+open Lean in
+/-- The current invocation's rendered hint. The reference survives search backtracking, but the
+local environment containing it is discarded when the invocation finishes. -/
+private meta initialize failureHint : EnvExtension (Option (IO.Ref (Option String))) ←
+  registerEnvExtension (pure none) (asyncMode := .local)
+
+open Lean Elab Tactic in
+/-- Collect one backend hint without rerunning search. Each invocation, including a nested one,
+has its own reference; `withEnv` restores the caller's environment even on resource exceptions.
+The ordinary `catch` does not intercept Lean's resource-limit or interrupt exceptions. -/
+private meta def withFailureHint (action : TacticM Unit) : TacticM Unit := do
+  let hint ← IO.mkRef (none : Option String)
+  try
+    withEnv (failureHint.setState (← getEnv) (some hint)) action
+  catch ex =>
+    let some message ← hint.get | throw ex
+    match ex with
+    | .error ref messageData =>
+      throw <| .error ref (messageData ++ .note m!"polytime could not certify a subterm in one \
+        attempted route:\n{message}")
+    | .internal .. => throw ex
+
 open Lean Meta Elab Tactic Mathlib.Meta.FunProp in
 /-- Shared compositional backend with a fresh alias-aware raw-premise boundary. The standard
 assumption discharger and ordinary transition depth are retained; callers keep their step limit.
@@ -634,7 +659,13 @@ meta def Internal.funPropWithPlainBoundary (maxSteps : Nat) : TacticM Unit := do
       transitionTheorems := ← plainGeneralTheorems (transitionTheoremsExt.getState env) }
     let ruleEnv ← plainRuleEnvironment env
     let (result, state) ← withEnv ruleEnv <| (funProp target ctx).run state
-    let some result := result | throwError "no compositional plain certificate: {state.msgLog}"
+    let some result := result | do
+      if let some hint := failureHint.getState (← getEnv) then
+        if (← hint.get).isNone then
+          -- FunProp rendered these strings while its telescope variables were in scope.
+          -- Keep its first report, without retaining expressions from its failure cache.
+          hint.set state.msgLog.getLast?
+      throwError "no compositional plain certificate: {state.msgLog}"
     goal.assign result.proof
     replaceMainGoal []
 open Lean Elab Tactic in
@@ -893,7 +924,7 @@ private meta def polytimeIterateAlternative : Lean.Elab.Tactic.TacticM Unit :=
 /-- Prove a polynomial-time certificate from known routines and controlled loop rules. -/
 -- Unfold only reducible aliases when comparing assumptions. Ordinary program definitions may
 -- contain large fixed enumerations; their named certificates should be tried before unfolding.
-elab "polytime" : tactic => Internal.withPlainRuleCache do
+elab "polytime" : tactic => withFailureHint <| Internal.withPlainRuleCache do
   Lean.Elab.Tactic.evalTactic (← `(tactic| solve |
     aesop (config := { terminal := true, assumptionTransparency := .reducible })
       (rule_sets := [PolyTime])))

ComplexityTests/PolyTimeFailureHint.lean

@@ -0,0 +1,91 @@
+/-
+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.Tactic.PolyTime
+
+/-! # Polynomial-time failure hints
+
+Ordinary imported clients exercise missing callbacks, captured variables and recovery into a
+successful proof. Each failed invocation must report its own subterm, without leaking into a
+subsequent invocation or changing the successful tactic's output.
+-/
+
+open Lean Meta Elab Tactic Turing.MultiTapeTM
+
+namespace ComplexityTests.PolyTimeFailureHint
+
+/-- Check a real failed invocation while preserving the surrounding proof and its goals. -/
+private meta def checkFailure (type : Expr) (required forbidden : Array String) : TacticM Unit := do
+  let saved ← saveState
+  try
+    let goal ← mkFreshExprSyntheticOpaqueMVar type
+    setGoals [goal.mvarId!]
+    let result ← observing <| Term.withoutErrToSorry <| withoutRecover <|
+      evalTactic (← `(tactic| polytime))
+    let .error ex := result | throwError "expected polytime to fail"
+    let message ← ex.toMessageData.toString
+    let marker := "polytime could not certify a subterm"
+    let [_, hint] := message.splitOn marker | throwError "expected one failure hint\n{message}"
+    let hint := marker ++ hint
+    for text in required do
+      unless hint.contains text do
+        throwError "missing diagnostic fragment {text}\n{message}"
+    for text in forbidden do
+      if hint.contains text then
+        throwError "unexpected diagnostic fragment {text}\n{message}"
+  finally
+    saved.restore
+
+elab (name := checkPolytimeFailure)
+    "check_polytime_failure " target:term " containing " "[" required:str,* "]"
+    " excluding " "[" forbidden:str,* "]" : tactic => do
+  checkFailure (← Term.elabType target)
+    (required.getElems.map (·.getString)) (forbidden.getElems.map (·.getString))
+
+local allow_unused_tactic checkPolytimeFailure
+
+-- A callback is certified when supplied, and is named when its certificate is missing.
+example (missingCallback : List Bool → Bool) : missingCallback = missingCallback := by
+  check_polytime_failure
+    (ComputableInPolyTime (fun word => !(missingCallback word)) encBits encBool)
+    containing ["polytime could not certify a subterm", "missingCallback", "encBits"]
+    excluding ["unknown free variable"]
+  rfl
+
+#guard_msgs in
+example (callback : List Bool → Bool)
+    (hcallback : ComputableInPolyTime callback encBits encBool) :
+    ComputableInPolyTime (fun word => !(callback word)) encBits encBool := by
+  polytime
+
+-- Captured parameters remain readable after the backend has closed its telescope.
+example (missingCaptured : List Bool → List Bool → Bool) : missingCaptured = missingCaptured := by
+  check_polytime_failure
+    (ComputableInPolyTime (fun pair : List Bool × List Bool =>
+      !(missingCaptured pair.1 pair.2)) (encPair encBits encBits) encBool)
+    containing ["polytime could not certify a subterm", "missingCaptured", "encPair"]
+    excluding ["unknown free variable"]
+  rfl
+
+-- Repeated invocations in one elaboration may not retain a prior callback's failure.
+example (firstMissing secondMissing : List Bool → Bool) :
+    (firstMissing, secondMissing) = (firstMissing, secondMissing) := by
+  check_polytime_failure (ComputableInPolyTime firstMissing encBits encBool)
+    containing ["polytime could not certify a subterm", "firstMissing", "encBits", "encBool"]
+    excluding ["secondMissing"]
+  check_polytime_failure (ComputableInPolyTime secondMissing encBits encBool)
+    containing ["polytime could not certify a subterm", "secondMissing"] excluding ["firstMissing"]
+  rfl
+
+-- A failed alternative leaves ordinary successful certificate search available and silent.
+#guard_msgs in
+example (callback : List Bool → Bool)
+    (hcallback : ComputableInPolyTime callback encBits encBool) :
+    ComputableInPolyTime (fun word => !(callback word)) encBits encBool := by
+  fail_if_success (clear hcallback; polytime)
+  polytime
+
+end ComplexityTests.PolyTimeFailureHint

ComplexityTests/PolyTimeFailureHintScope.lean

@@ -0,0 +1,96 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+
+public import Complexity.Tactic.PolyTime
+import all Complexity.Tactic.PolyTime
+
+/-! # Failure-hint scope and exceptional exits
+
+These internal controls seed real backend failures inside the invocation wrapper, including
+nested invocations. Lean's own exception constructors exercise resource and interrupt exits
+without changing search limits or relying on machine-dependent resource exhaustion.
+-/
+
+open Lean Meta Elab Tactic Turing.MultiTapeTM Cslib.Tactic.PolyTime
+
+namespace ComplexityTests.PolyTimeFailureHintScope
+
+/-- Exercise a failed backend attempt and retain only the invocation's diagnostic state. -/
+private meta def seedHint (type : Expr) : TacticM Unit := do
+  let saved ← saveState
+  try
+    let goal ← mkFreshExprSyntheticOpaqueMVar type
+    setGoals [goal.mvarId!]
+    let result ← observing <| Internal.funPropWithPlainBoundary 256
+    unless result matches .error _ do throwError "expected the backend to fail"
+  finally
+    saved.restore
+
+private meta def failureMessage (action : TacticM Unit) : TacticM String := do
+  let .error ex ← observing action | throwError "expected failure"
+  ex.toMessageData.toString
+
+private meta def checkHint (message expected unexpected : String) : TacticM Unit := do
+  unless message.contains "polytime could not certify a subterm" && message.contains expected &&
+      !message.contains unexpected do
+    throwError "incorrect invocation hint\n{message}"
+
+/-- Only this test observer catches all exceptions; the production wrapper uses normal catch. -/
+private meta def observeAll (action : TacticM Unit) : TacticM (Except Exception Unit) :=
+  (inferInstance : MonadAlwaysExcept Exception TacticM).except.tryCatch
+    (do action; pure (.ok ())) (fun ex => pure (.error ex))
+
+elab (name := checkFailureScope) "check_failure_scope " outer:term ", " inner:term : tactic => do
+  let outer ← Term.elabType outer
+  let inner ← Term.elabType inner
+  let message ← failureMessage <| withFailureHint do
+    let nested ← failureMessage <| withFailureHint do
+      seedHint inner
+      throwError "nested failure"
+    checkHint nested "innerMissing" "outerMissing"
+    -- The first nested invocation must restore the outer collector before it is populated.
+    seedHint outer
+    let nested ← failureMessage <| withFailureHint do
+      seedHint inner
+      throwError "nested failure"
+    checkHint nested "innerMissing" "outerMissing"
+    throwError "outer failure"
+  checkHint message "outerMissing" "innerMissing"
+  -- A successful invocation can have failed routes; neither exit may leave a collector behind.
+  withFailureHint (seedHint outer)
+  unless (failureHint.getState (← getEnv)).isNone do
+    throwError "failure hint escaped its invocation"
+  let message ← failureMessage <| withFailureHint (throwError "unseeded failure")
+  unless message == "unseeded failure" do throwError "unexpected unseeded hint\n{message}"
+  let raises : Array (TacticM Unit × (Exception → Bool)) := #[
+    ((do Core.throwMaxHeartbeat `polytimeFailureHint `maxHeartbeats 1000),
+      Exception.isMaxHeartbeat),
+    (throwMaxRecDepthAt (← getRef), Exception.isMaxRecDepth),
+    (throwInterruptException, Exception.isInterrupt)]
+  for (raise, isExpected) in raises do
+    let .error original ← observeAll raise | throwError "expected a resource or interrupt exception"
+    let .error wrapped ← observeAll <| withFailureHint do
+      seedHint outer
+      raise
+      | throwError "expected the wrapped exception"
+    unless isExpected wrapped &&
+        (← wrapped.toMessageData.toString) == (← original.toMessageData.toString) do
+      throwError "the failure wrapper changed a resource or interrupt exception"
+    unless (failureHint.getState (← getEnv)).isNone do
+      throwError "failure hint escaped an exceptional exit"
+
+local allow_unused_tactic checkFailureScope
+
+#guard_msgs in
+example (outerMissing innerMissing : List Bool → Bool) :
+    (outerMissing, innerMissing) = (outerMissing, innerMissing) := by
+  check_failure_scope (ComputableInPolyTime outerMissing encBits encBool),
+    (ComputableInPolyTime innerMissing encBits encBool)
+  rfl
+
+end ComplexityTests.PolyTimeFailureHintScope