From e998c9d81d69dd8a350d5ecb138a7e415167c057 Mon Sep 17 00:00:00 2001
From: Jules <julesmt@amazon.com>
Date: Tue, 26 May 2026 17:10:31 -0700
Subject: [PATCH 1/6] pyspec: add --reject-approximations CLI flag

Strict mode for the Python frontend. Sites that silently lower
unsupported constructs to a Hole or drop a statement now raise
`unsupportedConstruct` (exit 4). Off by default.

Test: RejectApproximationsTest.lean.
---
 Strata/Languages/Python/PySpecPipeline.lean   |  26 ++-
 Strata/Languages/Python/PythonToLaurel.lean   | 180 ++++++++++++++----
 Strata/Languages/Python/Specs.lean            |  24 ++-
 Strata/Languages/Python/Specs/ToLaurel.lean   |  10 +-
 Strata/SimpleAPI.lean                         |   4 +-
 StrataMain.lean                               |  13 +-
 .../Python/RejectApproximationsTest.lean      |  48 +++++
 7 files changed, 251 insertions(+), 54 deletions(-)
 create mode 100644 StrataTest/Languages/Python/RejectApproximationsTest.lean

diff --git a/Strata/Languages/Python/PySpecPipeline.lean b/Strata/Languages/Python/PySpecPipeline.lean
index 21129ebe39..b3839cc495 100644
--- a/Strata/Languages/Python/PySpecPipeline.lean
+++ b/Strata/Languages/Python/PySpecPipeline.lean
@@ -134,7 +134,8 @@ private def mergeOverloads (old new : OverloadTable) : OverloadTable :=
     to namespace all generated Laurel names (e.g., `"servicelib_Storage"` for
     module `servicelib.Storage`). -/
 public def buildPySpecLaurel (pyspecEntries : Array (String × String))
-    (overloads : OverloadTable) : EIO String PySpecLaurelResult := do
+    (overloads : OverloadTable) (rejectApproximations : Bool := false)
+    : EIO String PySpecLaurelResult := do
   let mut combinedProcedures : Array (Laurel.Procedure × String) := #[]
   let mut combinedTypes : Array (Laurel.TypeDefinition × String) := #[]
   let mut allOverloads := overloads
@@ -150,6 +151,11 @@ public def buildPySpecLaurel (pyspecEntries : Array (String × String))
       | .error msg => throw s!"Could not read {ionFile}: {msg}"
     let { program, errors, overloads, typeAliases, exhaustiveClasses } :=
       Python.Specs.ToLaurel.signaturesToLaurel ionPath sigs modulePrefix
+        (rejectApproximations := rejectApproximations)
+    if rejectApproximations && !errors.isEmpty then
+      let lines := errors.toList.map fun e =>
+        s!"  {e.file}:{e.loc.start}: [approximation] [{e.kind.category}] {e.message}"
+      throw s!"Rejected approximations in pyspec '{ionPath}':\n{String.intercalate "\n" lines}"
     allWarnings := allWarnings ++ errors
     allOverloads := mergeOverloads allOverloads overloads
     allTypeAliases := typeAliases.fold (init := allTypeAliases) fun m k v => m.insert k v
@@ -244,6 +250,7 @@ public def resolveAndBuildLaurelPrelude
     (stmts : Array (Python.stmt SourceRange))
     (specDir : System.FilePath := ".")
     (quiet : Bool := false)
+    (rejectApproximations : Bool := false)
     : EIO String PySpecLaurelResult := do
   -- Resolve dispatch module names to Ion paths
   let mut dispatchPaths : Array String := #[]
@@ -276,6 +283,7 @@ public def resolveAndBuildLaurelPrelude
     | none => throw s!"PySpec module '{modName}' not found in {specDir}"
   let allSpecEntries := autoSpecEntries ++ explicitEntries
   let result ← buildPySpecLaurel allSpecEntries dispatchOverloads
+                  (rejectApproximations := rejectApproximations)
   return { result with pyspecWarnings := dispatchWarnings ++ result.pyspecWarnings }
 
 /-! ### Pipeline Steps -/
@@ -429,6 +437,7 @@ public def pythonAndSpecToLaurel
     (profile : Bool := false)
     (quiet : Bool := false)
     (warningSummaryFile : Option String := none)
+    (rejectApproximations : Bool := false)
     : EIO PipelineError Laurel.Program := do
   let stmts ← profileStep profile "Read Python Ion" do
     match ← Python.readPythonStrata pythonIonPath |>.toBaseIO with
@@ -436,9 +445,17 @@ public def pythonAndSpecToLaurel
     | .error msg => throw (.internal msg)
 
   let result ← profileStep profile "Resolve and build Laurel prelude" do
-    match ← resolveAndBuildLaurelPrelude dispatchModules pyspecModules stmts specDir (quiet := quiet) |>.toBaseIO with
+    match ← resolveAndBuildLaurelPrelude dispatchModules pyspecModules stmts specDir
+              (quiet := quiet)
+              (rejectApproximations := rejectApproximations) |>.toBaseIO with
     | .ok r => pure r
-    | .error msg => throw (.internal msg)
+    | .error msg =>
+      -- Strict-mode rejections are user-actionable (the spec uses a pattern
+      -- pyspec can't translate yet), not tool bugs.
+      if msg.startsWith "Rejected approximations" then
+        throw (.knownLimitation msg)
+      else
+        throw (.internal msg)
 
   -- Print and write PySpec warnings before later stages can fail
   let pyspecWarnings := result.pyspecWarnings
@@ -470,7 +487,8 @@ public def pythonAndSpecToLaurel
 
   let metadataPath := sourcePath.getD pythonIonPath
   let (laurelProgram, _ctx) ← profileStep profile "Translate Python to Laurel" do
-    match Python.pythonToLaurel preludeInfo stmts metadataPath result.overloads with
+    match Python.pythonToLaurel preludeInfo stmts metadataPath result.overloads
+            (rejectApproximations := rejectApproximations) with
     | .error (.userPythonError range msg) => throw (.userCode range msg)
     | .error (.unsupportedConstruct msg ast) =>
         throw (.knownLimitation s!"Unsupported construct: {msg}\nAST: {ast}")
diff --git a/Strata/Languages/Python/PythonToLaurel.lean b/Strata/Languages/Python/PythonToLaurel.lean
index 0310fb473f..3cc5e5ed6a 100644
--- a/Strata/Languages/Python/PythonToLaurel.lean
+++ b/Strata/Languages/Python/PythonToLaurel.lean
@@ -129,6 +129,11 @@ structure TranslationContext where
   classesInHierarchy : Std.HashSet String := {}
   loopBreakLabel : Option String := none
   loopContinueLabel : Option String := none
+  /-- When `true`, every site that would silently emit a `Hole` for a
+      Python construct outside the precise sound subset raises a hard
+      `unsupportedConstruct` error instead. Default is `false` for
+      back-compat; the `--reject-approximations` CLI flag turns it on. -/
+  rejectApproximations : Bool := false
 deriving Inhabited
 
 /-! ## Error Handling -/
@@ -207,6 +212,32 @@ def stmtExprToVar (e : StmtExprMd) : Except TranslationError VariableMd :=
 /-- A wildcard modifies list, meaning the procedure may modify anything. -/
 def wildcardModifies : List StmtExprMd := [mkStmtExprMd .All]
 
+/-- Emit a `Hole` (the lax behavior) or raise `unsupportedConstruct`
+    under `--reject-approximations`. Used at every site that would
+    otherwise approximate an unsupported Python construct as a havoc'd
+    Hole. The `construct` argument names the surface form (e.g.,
+    `"BinOp Div"`) for the error message. -/
+def rejectableHole (rejectApproximations : Bool) (construct astRepr : String)
+    : Except TranslationError StmtExprMd :=
+  if rejectApproximations then
+    throw (.unsupportedConstruct
+      s!"[approximation] {construct} is approximated as Hole; not in the sound subset"
+      astRepr)
+  else
+    pure (mkStmtExprMd .Hole)
+
+/-- Same as `rejectableHole` but for sites that silently drop a Python
+    statement (e.g., `raise`, `try…else`, `for…else`) under lax mode.
+    The error message names the dropped construct. -/
+def rejectableDrop (rejectApproximations : Bool) (construct astRepr : String)
+    : Except TranslationError Unit :=
+  if rejectApproximations then
+    throw (.unsupportedConstruct
+      s!"[approximation] {construct} is silently dropped today; not in the sound subset"
+      astRepr)
+  else
+    pure ()
+
 /-- Create a StmtExprMd with source location metadata. -/
 def mkStmtExprMdWithLoc (expr : StmtExpr) (source : Option FileRange) : StmtExprMd :=
   { val := expr, source := source }
@@ -224,12 +255,18 @@ def manglePythonMethod (className : String) (methodName : String) : String :=
   className ++ "@" ++ methodName
 
 /-- Build a StaticCall for an instance method: ClassName@methodName(self, args...).
-    For Any-typed receivers (no model available), returns a Hole instead. -/
-def mkInstanceMethodCall (className : String) (methodName : String)
+    For Any-typed receivers (no model available), returns a Hole under lax
+    mode, or raises `unsupportedConstruct` under `--reject-approximations`. -/
+def mkInstanceMethodCall (rejectApproximations : Bool) (className : String) (methodName : String)
     (self : StmtExprMd) (args : List StmtExprMd)
-    (source : Option FileRange := none) : StmtExprMd :=
-  if className == "Any" then mkStmtExprMdWithLoc .Hole source
-  else mkStmtExprMdWithLoc (StmtExpr.StaticCall (manglePythonMethod className methodName) (self :: args)) source
+    (source : Option FileRange := none) : Except TranslationError StmtExprMd :=
+  if className == "Any" then
+    rejectableHole rejectApproximations
+      s!"instance method call '{methodName}' on Any-typed receiver"
+      s!"<{className}>.{methodName}(...)" |>.map (fun h =>
+        { h with source := source })
+  else
+    pure (mkStmtExprMdWithLoc (StmtExpr.StaticCall (manglePythonMethod className methodName) (self :: args)) source)
 
 /-- Extract string representation from Python expression (for type annotations) -/
 partial def pyExprToString (e : Python.expr SourceRange) : String :=
@@ -577,21 +614,25 @@ partial def translateExpr (ctx : TranslationContext) (e : Python.expr SourceRang
 
   -- Bytes literal
   | .Constant _ (.ConBytes _ _) _ =>
-    return mkStmtExprMd .Hole
+    rejectableHole ctx.rejectApproximations
+      "bytes literal" (toString (repr e))
 
   -- Float literal
   | .Constant _ (.ConFloat _ f) _ =>
     match parseFloatString f.val with
     | some d => return floatToAny d
-    | none => return mkStmtExprMd .Hole
+    | none => rejectableHole ctx.rejectApproximations
+                "unparseable float literal" (toString (repr e))
 
   -- Complex literal
   | .Constant _ (.ConComplex _ _ _) _ =>
-    return mkStmtExprMd .Hole
+    rejectableHole ctx.rejectApproximations
+      "complex literal" (toString (repr e))
 
   -- Ellipsis literal
   | .Constant _ (.ConEllipsis _) _ =>
-    return mkStmtExprMd .Hole
+    rejectableHole ctx.rejectApproximations
+      "ellipsis (...) as expression" (toString (repr e))
 
   -- Variable references
   | .Name _ name _ =>
@@ -606,15 +647,19 @@ partial def translateExpr (ctx : TranslationContext) (e : Python.expr SourceRang
       | .Add _ => .ok "PAdd"
       | .Sub _ => .ok "PSub"
       | .Mult _ => .ok "PMul"
-      | .Div _ => return mkStmtExprMd .Hole -- Floating-point are not supported yet
+      | .Div _ => return ← rejectableHole ctx.rejectApproximations
+                              "BinOp Div (true division)" (toString (repr e))
       | .FloorDiv _ => .ok "PFloorDiv"  -- Python // maps to Laurel Div
       | .Mod _ => .ok "PMod"
       | .Pow _ => .ok "PPow"
       | .LShift _ => .ok "PLShift"
       | .RShift _ => .ok "PRShift"
-      | .BitAnd _ => return mkStmtExprMd .Hole --TODO: Adding BitVector subtype in Any type, then the related operations
-      | .BitOr _ => return mkStmtExprMd .Hole
-      | .BitXor _ => return mkStmtExprMd .Hole
+      | .BitAnd _ => return ← rejectableHole ctx.rejectApproximations
+                                "BinOp BitAnd" (toString (repr e))
+      | .BitOr _ => return ← rejectableHole ctx.rejectApproximations
+                               "BinOp BitOr" (toString (repr e))
+      | .BitXor _ => return ← rejectableHole ctx.rejectApproximations
+                                "BinOp BitXor" (toString (repr e))
       -- Unsupported for now
       | _ => throw (.unsupportedConstruct s!"Binary operator not yet supported: {repr op}" (toString (repr e)))
     return mkStmtExprMdWithLoc (StmtExpr.StaticCall preludeOpnames [leftExpr, rightExpr]) md
@@ -769,8 +814,12 @@ partial def translateExpr (ctx : TranslationContext) (e : Python.expr SourceRang
       return mkStmtExprMd (.StaticCall "from_str" [concat])
 
   -- Interpolation / TemplateStr (Python 3.14+ t-strings) - not yet supported
-  | .Interpolation .. => return mkStmtExprMd .Hole
-  | .TemplateStr .. => return mkStmtExprMd .Hole
+  | .Interpolation .. =>
+    rejectableHole ctx.rejectApproximations
+      "string interpolation (t-string)" (toString (repr e))
+  | .TemplateStr .. =>
+    rejectableHole ctx.rejectApproximations
+      "template string (t-string)" (toString (repr e))
 
   | .IfExp _ cond thenb elseb =>
     let condExpr ← translateExpr ctx cond
@@ -838,7 +887,8 @@ partial def translateExpr (ctx : TranslationContext) (e : Python.expr SourceRang
           -- so standalone reads like `x = self.field` are not silently lost.
           let hasDispatch := ctx.dispatchFieldTypes[className]?.any (·.contains attr.val)
           if hasDispatch then
-            return mkStmtExprMd .Hole
+            rejectableHole ctx.rejectApproximations
+              s!"dispatch field read (self.{attr.val})" (toString (repr e))
           else
             return fieldExpr
         | _ =>
@@ -846,7 +896,8 @@ partial def translateExpr (ctx : TranslationContext) (e : Python.expr SourceRang
       else if isPackage ctx obj then
         -- FIXME: Module attribute (e.g., sys.argv): modules are not modeled as
         -- Laurel values, so return Hole like we do for unmodeled package calls.
-        return mkStmtExprMd .Hole
+        rejectableHole ctx.rejectApproximations
+          "module attribute access" (toString (repr e))
       else
         -- Regular object.field access
         let objExpr ← translateExpr ctx obj
@@ -872,24 +923,34 @@ partial def translateExpr (ctx : TranslationContext) (e : Python.expr SourceRang
 
   -- Set literal: {1, 2, 3}
   -- Abstract: return havoc'd set (sound abstraction)
-  | .Set .. => return mkStmtExprMd .Hole
+  | .Set .. =>
+    rejectableHole ctx.rejectApproximations
+      "Set literal" (toString (repr e))
 
   -- Tuple literal: (1, 2)
   | .Tuple _ elems _ => translateList ctx elems.val.toList
 
   -- List comprehension: [x for x in items]
   -- Abstract: return havoc'd list (sound abstraction)
-  | .ListComp .. => return mkStmtExprMd .Hole
+  | .ListComp .. =>
+    rejectableHole ctx.rejectApproximations
+      "list comprehension" (toString (repr e))
 
   -- Set comprehension: {x for x in items}
   -- Abstract: return havoc'd set (sound abstraction)
-  | .SetComp .. => return mkStmtExprMd .Hole
+  | .SetComp .. =>
+    rejectableHole ctx.rejectApproximations
+      "set comprehension" (toString (repr e))
 
   -- Dict comprehension: {k: v for k, v in items}
-  | .DictComp .. => return mkStmtExprMd .Hole
+  | .DictComp .. =>
+    rejectableHole ctx.rejectApproximations
+      "dict comprehension" (toString (repr e))
 
   -- Generator expression: (x for x in items)
-  | .GeneratorExp .. => return mkStmtExprMd .Hole
+  | .GeneratorExp .. =>
+    rejectableHole ctx.rejectApproximations
+      "generator expression" (toString (repr e))
 
   | _ => throw (.unsupportedConstruct "Expression type not yet supported" (toString (repr e)))
 
@@ -983,12 +1044,14 @@ The following function return a tuple (translated function name, first argument,
 /-- Coerce an expression to Any if its inferred type is a Composite class.
     Composite values are replaced with a Hole (unconstrained Any value)
     since Composite→Any coercion is not yet modeled. This limits
-    bug-finding ability but avoids type unification errors. -/
+    bug-finding ability but avoids type unification errors.
+    Under `--reject-approximations`, refuse to lower the coercion. -/
 partial def coerceToAny (ctx : TranslationContext) (expr : Python.expr SourceRange)
     (translated : StmtExprMd) : Except TranslationError StmtExprMd := do
   let ty ← inferExprType ctx expr
   if isCompositeType ctx ty then
-    pure <| mkStmtExprMd (.Hole)
+    rejectableHole ctx.rejectApproximations
+      s!"Composite-to-Any coercion ({ty})" (toString (repr expr))
   else pure translated
 
 partial def refineFunctionCallExpr (ctx : TranslationContext) (func: Python.expr SourceRange) :
@@ -1202,10 +1265,13 @@ partial def translateCall (ctx : TranslationContext)
         | _ => []
       else []
     let havocStmts := receiverHavoc ++ argHavoc
+    let h ← rejectableHole ctx.rejectApproximations
+              s!"unmodeled call to '{funcName}'"
+              (toString (repr f))
     if havocStmts.isEmpty then
-      return mkStmtExprMd .Hole
+      return h
     else
-      return mkStmtExprMd (.Block (havocStmts ++ [mkStmtExprMd .Hole]) none)
+      return mkStmtExprMd (.Block (havocStmts ++ [h]) none)
   -- Step 3: translate the resolved call
   let methodName := match f with
     | .Attribute _ _ attr _ => attr.val
@@ -1255,12 +1321,17 @@ partial def translateCall (ctx : TranslationContext)
             -- so the static resolution may be wrong. Emit a Hole in that case.
             let classPrefix := funcName.splitOn "@" |>.head!
             if ctx.classesInHierarchy.contains classPrefix then
-              return mkStmtExprMdWithLoc (.Hole) callMd
-            let callWithSelf := mkStmtExprMdWithLoc
-              (StmtExpr.StaticCall funcName (target_trans :: callArgs)) callMd
-            return callWithSelf
+              rejectableHole ctx.rejectApproximations
+                s!"method call '{funcName}' with uncertain inheritance dispatch"
+                (toString (repr f))
+            else
+              let callWithSelf := mkStmtExprMdWithLoc
+                (StmtExpr.StaticCall funcName (target_trans :: callArgs)) callMd
+              return callWithSelf
           else
-            return mkStmtExprMdWithLoc (.Hole) callMd
+            rejectableHole ctx.rejectApproximations
+              s!"method call '{funcName}' on receiver of unknown type"
+              (toString (repr f))
         else return mkCall funcName
     | _ => throw (.unsupportedConstruct "Invalid call construct" (toString (repr f)))
   -- When ** is used at the call site and we have a known function signature,
@@ -1411,7 +1482,12 @@ partial def translateAssign  (ctx : TranslationContext)
               let newExpr := mkStmtExprMd (StmtExpr.New resolvedId)
               let varType := mkHighTypeMd (.UserDefined resolvedId)
               let selfRef := mkStmtExprMd (StmtExpr.Var (.Local n.val))
-              let initStmt := mkInstanceMethodCall laurelName "__init__" selfRef args source
+              -- `laurelName` came from `ImportedSymbol.compositeType` so it
+              -- is a concrete class name, never `"Any"`.
+              let initStmt := mkStmtExprMdWithLoc
+                (StmtExpr.StaticCall
+                  (manglePythonMethod laurelName "__init__")
+                  (selfRef :: args)) source
               if n.val ∈ ctx.variableTypes.unzip.1 then
                 let assignStmt := mkStmtExprMdWithLoc (StmtExpr.Assign [target] newExpr) source
                 [assignStmt, initStmt]
@@ -1703,8 +1779,11 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang
     return (bodyCtx, preamble ++ [ifStmt])
 
   -- While loop
-  | .While _ test body _orelse => do
+  | .While _ test body orelse => do
     -- Note: Python while-else not supported yet
+    if !orelse.val.isEmpty then
+      rejectableDrop ctx.rejectApproximations
+        "while…else clause" (toString (repr s))
     let condExpr ← translateExpr ctx test
     let breakLabel := s!"loop_break_{test.toAst.ann.start.byteIdx}"
     let continueLabel := s!"loop_continue_{test.toAst.ann.start.byteIdx}"
@@ -1795,7 +1874,13 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang
   | .Import _ _ | .ImportFrom _ _ _ _ |.Pass _ => return (ctx, [])
 
   -- Try/except - wrap body with exception checks and handlers
-  | .Try _ body handlers _ _ => do
+  | .Try _ body handlers orelse finalbody => do
+    if !orelse.val.isEmpty then
+      rejectableDrop ctx.rejectApproximations
+        "try…else clause" (toString (repr s))
+    if !finalbody.val.isEmpty then
+      rejectableDrop ctx.rejectApproximations
+        "try…finally clause" (toString (repr s))
     let tryLabel := s!"try_end_{s.toAst.ann.start.byteIdx}"
     let catchersLabel := s!"exception_handlers_{s.toAst.ann.start.byteIdx}"
     let (bodyCtx, bodyStmts) ← translateStmtList ctx body.val.toList
@@ -1854,7 +1939,9 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang
 
   -- FIXME: Placeholder — `raise` is dropped so the Hole type inferrer doesn't
   -- produce Unknown types. Must be replaced to correctly model exceptions later.
-  | .Raise _ _ _ => return (ctx, [])
+  | .Raise _ _ _ => do
+    rejectableDrop ctx.rejectApproximations "raise" (toString (repr s))
+    return (ctx, [])
 
   -- With statement: with EXPR as VAR: BODY
   -- Desugars to: mgr = EXPR; VAR = mgr.__enter__(); BODY; mgr.__exit__()
@@ -1872,8 +1959,8 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang
         let mgrDecl := mkVarDeclInit mgrName mgrLauTy mgrExpr
         let mgrRef := mkStmtExprMd (StmtExpr.Var (.Local mgrName))
         currentCtx := {currentCtx with variableTypes := currentCtx.variableTypes ++ [(mgrName, mgrTy)]}
-        let enterCall := mkInstanceMethodCall mgrTy "__enter__" mgrRef [] md
-        let exitCall := mkInstanceMethodCall mgrTy "__exit__" mgrRef [] md
+        let enterCall ← mkInstanceMethodCall ctx.rejectApproximations mgrTy "__enter__" mgrRef [] md
+        let exitCall ← mkInstanceMethodCall ctx.rejectApproximations mgrTy "__exit__" mgrRef [] md
         match optVars.val with
         | some varExpr =>
           let varName := pyExprToString varExpr
@@ -1907,7 +1994,10 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang
   -- Note that Any_iter_index(iter, index) should not return an exception when 0 <= index < Any_len(iter)
   -- and Any_iter_index is only called inside the loop body where that condition is satisfied,
   -- so it is sound to not put it inside AnyMaybeExceptionList
-  | .For _ target iter body _orelse _ => do
+  | .For _ target iter body orelse _ => do
+    if !orelse.val.isEmpty then
+      rejectableDrop ctx.rejectApproximations
+        "for…else clause" (toString (repr s))
     -- The iterator expression (we abstract it away).
     -- When the expression contains side-effect statements (e.g. a block with
     -- receiver havoc from an unmodeled method call), bind it to a temporary
@@ -1985,11 +2075,17 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang
   | .Break _ =>
     match ctx.loopBreakLabel with
     | some lbl => return (ctx, [mkStmtExprMdWithLoc (StmtExpr.Exit lbl) md])
-    | none => return (ctx, [mkStmtExprMdWithLoc (StmtExpr.Assert { condition := mkStmtExprMd .Hole }) md])
+    | none =>
+      let h ← rejectableHole ctx.rejectApproximations
+        "break outside enclosing loop" "break"
+      return (ctx, [mkStmtExprMdWithLoc (StmtExpr.Assert { condition := h }) md])
   | .Continue _ =>
     match ctx.loopContinueLabel with
     | some lbl => return (ctx, [mkStmtExprMdWithLoc (StmtExpr.Exit lbl) md])
-    | none => return (ctx, [mkStmtExprMdWithLoc (StmtExpr.Assert { condition := mkStmtExprMd .Hole }) md])
+    | none =>
+      let h ← rejectableHole ctx.rejectApproximations
+        "continue outside enclosing loop" "continue"
+      return (ctx, [mkStmtExprMdWithLoc (StmtExpr.Assert { condition := h }) md])
 
   -- Augmented assignment: x += expr  →  x = x op expr
   | .AugAssign sr target op value => do
@@ -2714,6 +2810,7 @@ def pythonToLaurel (info : PreludeInfo)
     (body : Array (stmt SourceRange))
     (filePath : String := "")
     (overloadTable : OverloadTable := {})
+    (rejectApproximations : Bool := false)
     : Except TranslationError (Laurel.Program × TranslationContext) := do
   -- Collect user function names (top-level and class methods)
   let userFunctions := body.toList.flatMap fun stmt =>
@@ -2822,7 +2919,8 @@ def pythonToLaurel (info : PreludeInfo)
     compositeTypeReverse := compositeTypeReverse,
     exhaustiveClasses := exhaustiveClasses,
     classesInHierarchy := classesInHierarchy,
-    filePath := filePath
+    filePath := filePath,
+    rejectApproximations := rejectApproximations
   }
 
   -- Separate functions from other statements
diff --git a/Strata/Languages/Python/Specs.lean b/Strata/Languages/Python/Specs.lean
index 00ec5f786d..6495902253 100644
--- a/Strata/Languages/Python/Specs.lean
+++ b/Strata/Languages/Python/Specs.lean
@@ -291,6 +291,11 @@ structure PySpecContext where
   /-- Python module name for the current file (e.g., "boto3.dynamodb").
       Used as `pythonModule` for locally-defined classes. -/
   currentModule : ModuleName
+  /-- When `true`, any `specWarning` or `specError` reported during
+      icontract decorator parsing (which today silently falls back to
+      `.placeholder` for unrecognized patterns) is treated as a fatal
+      error by the downstream pipeline. Off by default. -/
+  rejectApproximations : Bool := false
 
 /-- Resolve a module name to a file path, registering the file's FileMap
     for source-location error reporting.  Returns `(filePath, modulePrefix)`
@@ -362,9 +367,16 @@ instance : PySpecMClass PySpecM where
   specError loc message := do
     specErrorAt (←read).pythonFile loc message
   specWarning loc message := do
-    let file := (←read).pythonFile
-    let w : SpecError := { file, loc, kind := .pySpecParsingWarning, message }
-    modify fun s => { s with warnings := s.warnings.push w }
+    let ctx ← read
+    -- Under strict mode (`--reject-approximations`), every warning is an
+    -- error: the parser only emits warnings on patterns it falls back to
+    -- `.placeholder` for, which silently drops the user's spec.
+    if ctx.rejectApproximations then
+      specErrorAt ctx.pythonFile loc s!"[approximation] {message}"
+    else
+      let w : SpecError := { file := ctx.pythonFile, loc,
+                             kind := .pySpecParsingWarning, message }
+      modify fun s => { s with warnings := s.warnings.push w }
   runChecked act := do
     let cnt := (←get).errors.size
     let r ← act
@@ -1675,7 +1687,8 @@ def translateModule
     (pythonCmd : String := "python")
     (events : Std.HashSet EventType := {})
     (skipNames : Std.HashSet PythonIdent := {})
-    (currentModulePrefix : Array String := #[]) :
+    (currentModulePrefix : Array String := #[])
+    (rejectApproximations : Bool := false) :
     BaseIO (FileMaps × Array Signature × Array SpecError × Array SpecError) := do
   let fmm : FileMaps := {}
   let fmm := fmm.insert pythonFile fileMap
@@ -1691,6 +1704,7 @@ def translateModule
     strataDir := strataDir
     pythonFile := pythonFile
     currentModule := currentModule
+    rejectApproximations := rejectApproximations
   }
   let (res, s) ← translateModuleAux body |>.run ctx |>.run { warnings := #[], errors := #[] }
   let fmm ← fileMapsRef.get
@@ -1703,6 +1717,7 @@ public def translateFile
     (events : Std.HashSet EventType := {})
     (skipNames : Std.HashSet PythonIdent := {})
     (moduleName : Option ModuleName := none)
+    (rejectApproximations : Bool := false)
     : EIO String (Array Signature × Array String) := do
   let currentModule ← match moduleName with
     | some m => pure m
@@ -1741,6 +1756,7 @@ public def translateFile
         (currentModulePrefix := modulePrefix)
         (strataDir := strataDir)
         (pythonFile := pythonFile)
+        (rejectApproximations := rejectApproximations)
         (.ofString contents)
         body
         currentModule
diff --git a/Strata/Languages/Python/Specs/ToLaurel.lean b/Strata/Languages/Python/Specs/ToLaurel.lean
index da75cc4076..801723d2fa 100644
--- a/Strata/Languages/Python/Specs/ToLaurel.lean
+++ b/Strata/Languages/Python/Specs/ToLaurel.lean
@@ -72,6 +72,12 @@ structure ToLaurelContext where
   /-- Module prefix prepended to generated type and procedure names
       to avoid collisions when multiple PySpec files are combined. -/
   modulePrefix : String
+  /-- When `true`, every spec-level approximation (placeholder expression,
+      unsupported `isinstance` / `forall` / float literal, etc.) raises a
+      hard error rather than being silently skipped. The downstream
+      pipeline should fail the build when this flag is on and any errors
+      were reported. Off by default for back-compat. -/
+  rejectApproximations : Bool := false
 
 /-- State for PySpec to Laurel translation. -/
 structure ToLaurelState where
@@ -633,9 +639,9 @@ public structure TranslationResult where
 /-- Run the translation and return a Laurel Program, dispatch table,
     and any errors. -/
 public def signaturesToLaurel (filepath : System.FilePath) (sigs : Array Signature)
-    (modulePrefix : String)
+    (modulePrefix : String) (rejectApproximations : Bool := false)
     : TranslationResult :=
-  let ctx : ToLaurelContext := { filepath, modulePrefix }
+  let ctx : ToLaurelContext := { filepath, modulePrefix, rejectApproximations }
   let ((), state) := (sigs.forM signatureToLaurel).run ctx |>.run {}
   let pgm : Laurel.Program := {
     staticProcedures := state.procedures.toList
diff --git a/Strata/SimpleAPI.lean b/Strata/SimpleAPI.lean
index 4e536c732b..272c6eae00 100644
--- a/Strata/SimpleAPI.lean
+++ b/Strata/SimpleAPI.lean
@@ -453,6 +453,7 @@ def pySpecsDir (sourceDir strataDir dialectFile : System.FilePath)
     (skipNames : Array String := #[])
     (warningOutput : WarningOutput := .detail)
     (pythonCmd : String := "python")
+    (rejectApproximations : Bool := false)
     : EIO String Unit := do
   -- Create output dir
   match ← IO.FS.createDirAll strataDir |>.toBaseIO with
@@ -510,7 +511,8 @@ def pySpecsDir (sourceDir strataDir dialectFile : System.FilePath)
     match ← Strata.Python.Specs.translateFile
         dialectFile strataDir pythonFile sourceDir
         (events := events) (skipNames := skipIdents)
-        (moduleName := mod) (pythonCmd := pythonCmd) |>.toBaseIO with
+        (moduleName := mod) (pythonCmd := pythonCmd)
+        (rejectApproximations := rejectApproximations) |>.toBaseIO with
     | .error msg =>
       Python.Specs.baseLogEvent events "import" s!"Failed {mod}: {msg}"
       failures := failures.push (toString mod, msg)
diff --git a/StrataMain.lean b/StrataMain.lean
index 1e6700ff54..f1c846a09e 100644
--- a/StrataMain.lean
+++ b/StrataMain.lean
@@ -401,7 +401,9 @@ def pySpecsCommand : Command where
       takesArg := .repeat "name" },
     { name := "module",
       help := "Translate only the named module (dot-separated). May be repeated.",
-      takesArg := .repeat "module" }
+      takesArg := .repeat "module" },
+    { name := "reject-approximations",
+      help := "Reject every spec construct silently lowered to a placeholder or warning. Off by default." }
   ]
   help := "Translate Python specification files in a directory into Strata DDM Ion format. If --module is given, translates only those modules; otherwise translates all .py files. Creates subdirectories as needed. (Experimental)"
   callback := fun v pflags => do
@@ -415,6 +417,7 @@ def pySpecsCommand : Command where
     let modules := pflags.getRepeated "module"
     let warningOutput : Strata.WarningOutput :=
       if quiet then .none else .detail
+    let rejectApproximations := pflags.getBool "reject-approximations"
     -- Serialize embedded dialect for Python subprocess
     IO.FS.withTempFile fun _handle dialectFile => do
       IO.FS.writeBinFile dialectFile Strata.Python.Python.toIon
@@ -422,6 +425,7 @@ def pySpecsCommand : Command where
                 (skipNames := skipNames)
                 (modules := modules)
                 (warningOutput := warningOutput)
+                (rejectApproximations := rejectApproximations)
                 v[0] v[1] dialectFile |>.toBaseIO
       match r with
       | .ok () => pure ()
@@ -587,6 +591,9 @@ def pyAnalyzeLaurelCommand : Command where
               takesArg := .arg "file" },
             { name := "skip-verification",
               help := "Run Python-to-Laurel and Laurel-to-Core translation only (skip SMT verification).",
+              takesArg := .none },
+            { name := "reject-approximations",
+              help := "Reject every Python construct currently approximated as a havoc'd Hole or silently dropped. First error stops translation. Off by default.",
               takesArg := .none }]
   help := "Verify a Python Ion program via the Laurel pipeline. Translates Python to Laurel to Core, then runs SMT verification."
   callback := fun v pflags => do
@@ -612,11 +619,13 @@ def pyAnalyzeLaurelCommand : Command where
       | some (pyPath, srcText) => some (pyPath, .ofString srcText)
       | none => none
     let warningSummaryFile := pflags.getString "warning-summary"
+    let rejectApproximations := pflags.getBool "reject-approximations"
     let combinedLaurel ←
       match ← Strata.pythonAndSpecToLaurel filePath dispatchModules pyspecModules sourcePath
                 (specDir := specDir) (profile := profile)
                 (quiet := quiet)
-                (warningSummaryFile := warningSummaryFile) |>.toBaseIO with
+                (warningSummaryFile := warningSummaryFile)
+                (rejectApproximations := rejectApproximations) |>.toBaseIO with
       | .ok r => pure r
       | .error (.userCode range msg) =>
         let location := if range.isNone then "" else
diff --git a/StrataTest/Languages/Python/RejectApproximationsTest.lean b/StrataTest/Languages/Python/RejectApproximationsTest.lean
new file mode 100644
index 0000000000..ca5a17b101
--- /dev/null
+++ b/StrataTest/Languages/Python/RejectApproximationsTest.lean
@@ -0,0 +1,48 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+
+import Strata.Languages.Python.PythonToLaurel
+
+/-! # `--reject-approximations` flag tests
+
+Unit tests for the `rejectableHole` / `rejectableDrop` helpers: with
+the flag off, they emit a `Hole` / no-op (lax behavior); with the flag
+on, they raise `unsupportedConstruct` with an `[approximation]` tag.
+-/
+
+namespace Strata.Python.RejectApproximationsTest
+
+open Strata.Python (rejectableHole rejectableDrop)
+open Strata.Python.TranslationError
+
+-- rejectableHole false -> emits a Hole (lax behavior preserved)
+#guard
+  match rejectableHole false "BinOp Div" "<ast>" with
+  | .ok ⟨.Hole, _⟩ => true
+  | _ => false
+
+-- rejectableHole true -> raises unsupportedConstruct with [approximation] tag
+#guard
+  match rejectableHole true "BinOp Div" "<ast>" with
+  | .error (.unsupportedConstruct msg _) =>
+      msg.startsWith "[approximation]" && (msg.splitOn "BinOp Div").length > 1
+  | _ => false
+
+-- rejectableDrop false -> no-op
+#guard
+  match rejectableDrop false "raise" "<ast>" with
+  | .ok () => true
+  | _ => false
+
+-- rejectableDrop true -> raises with "silently dropped" wording
+#guard
+  match rejectableDrop true "raise" "<ast>" with
+  | .error (.unsupportedConstruct msg _) =>
+      msg.startsWith "[approximation]"
+        && (msg.splitOn "silently dropped").length > 1
+  | _ => false
+
+end Strata.Python.RejectApproximationsTest

From a534c08d7b563ec932bbbf5f6b1b0a2c636e6773 Mon Sep 17 00:00:00 2001
From: keyboardDrummer-bot <keyboardDrummer-bot@users.noreply.github.com>
Date: Fri, 29 May 2026 13:33:39 +0000
Subject: [PATCH 2/6] ci: retry CBMC job (cache miss on previous run)


From a49b740b6c276a971970fe7d6793573f845a58b6 Mon Sep 17 00:00:00 2001
From: Jules <julesmt@amazon.com>
Date: Tue, 2 Jun 2026 14:41:48 -0700
Subject: [PATCH 3/6] pyspec: shorter approximation diagnostics
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The strict-mode error helpers used to dump the full Python AST `repr`
into every diagnostic, producing multi-kilobyte messages on real specs.
Take an `Option FileRange` instead and render `file:offset` when one is
available; cap the AST string fallback at 200 chars. Also stamp the
returned `Hole` with the source so callers don't have to.

Reword `"silently dropped today"` → `"silently dropped by current
translation"` so the message doesn't read as date-dependent.
---
 Strata/Languages/Python/PythonToLaurel.lean   | 97 +++++++++++--------
 .../Python/RejectApproximationsTest.lean      | 25 ++++-
 2 files changed, 77 insertions(+), 45 deletions(-)

diff --git a/Strata/Languages/Python/PythonToLaurel.lean b/Strata/Languages/Python/PythonToLaurel.lean
index 88963f3a25..9c14f4d357 100644
--- a/Strata/Languages/Python/PythonToLaurel.lean
+++ b/Strata/Languages/Python/PythonToLaurel.lean
@@ -212,36 +212,51 @@ def stmtExprToVar (e : StmtExprMd) : Except TranslationError VariableMd :=
 /-- A wildcard modifies list, meaning the procedure may modify anything. -/
 def wildcardModifies : List StmtExprMd := [mkStmtExprMd .All]
 
+/-- Create a StmtExprMd with source location metadata. -/
+def mkStmtExprMdWithLoc (expr : StmtExpr) (source : Option FileRange) : StmtExprMd :=
+  { val := expr, source := source }
+
+/-- Build the `pyAst` payload for an approximation diagnostic.
+    Prefers the source location (cheap, useful) when available; otherwise
+    falls back to a capped AST string so user-facing errors don't grow to
+    multi-kilobyte sizes for deeply nested expressions. -/
+private def approximationAstPayload (source : Option FileRange) (astRepr : String) : String :=
+  match source with
+  | some fr => toString (Std.format fr)
+  | none =>
+    if astRepr.length ≤ 200 then astRepr
+    else (astRepr.toRawSubstring.take 200).toString ++ "…"
+
 /-- Emit a `Hole` (the lax behavior) or raise `unsupportedConstruct`
     under `--reject-approximations`. Used at every site that would
     otherwise approximate an unsupported Python construct as a havoc'd
     Hole. The `construct` argument names the surface form (e.g.,
-    `"BinOp Div"`) for the error message. -/
-def rejectableHole (rejectApproximations : Bool) (construct astRepr : String)
+    `"BinOp Div"`) for the error message. The optional `source` is
+    stamped on the resulting `Hole` and used to render a short
+    `file:line:col` payload on the rejection error. -/
+def rejectableHole (rejectApproximations : Bool) (construct : String)
+    (source : Option FileRange := none) (astRepr : String := "")
     : Except TranslationError StmtExprMd :=
   if rejectApproximations then
     throw (.unsupportedConstruct
       s!"[approximation] {construct} is approximated as Hole; not in the sound subset"
-      astRepr)
+      (approximationAstPayload source astRepr))
   else
-    pure (mkStmtExprMd .Hole)
+    pure (mkStmtExprMdWithLoc .Hole source)
 
 /-- Same as `rejectableHole` but for sites that silently drop a Python
     statement (e.g., `raise`, `try…else`, `for…else`) under lax mode.
     The error message names the dropped construct. -/
-def rejectableDrop (rejectApproximations : Bool) (construct astRepr : String)
+def rejectableDrop (rejectApproximations : Bool) (construct : String)
+    (source : Option FileRange := none) (astRepr : String := "")
     : Except TranslationError Unit :=
   if rejectApproximations then
     throw (.unsupportedConstruct
-      s!"[approximation] {construct} is silently dropped today; not in the sound subset"
-      astRepr)
+      s!"[approximation] {construct} is silently dropped by current translation; not in the sound subset"
+      (approximationAstPayload source astRepr))
   else
     pure ()
 
-/-- Create a StmtExprMd with source location metadata. -/
-def mkStmtExprMdWithLoc (expr : StmtExpr) (source : Option FileRange) : StmtExprMd :=
-  { val := expr, source := source }
-
 /-- Create a local variable declaration with initializer. -/
 def mkVarDeclInit (name : Identifier) (ty : AstNode HighType) (init : StmtExprMd) : StmtExprMd :=
   mkStmtExprMd (.Assign [mkVariableMd (.Declare ⟨name, ty⟩)] init)
@@ -263,8 +278,7 @@ def mkInstanceMethodCall (rejectApproximations : Bool) (className : String) (met
   if className == "Any" then
     rejectableHole rejectApproximations
       s!"instance method call '{methodName}' on Any-typed receiver"
-      s!"<{className}>.{methodName}(...)" |>.map (fun h =>
-        { h with source := source })
+      (source := source)
   else
     pure (mkStmtExprMdWithLoc (StmtExpr.StaticCall (manglePythonMethod className methodName) (self :: args)) source)
 
@@ -610,24 +624,24 @@ partial def translateExpr (ctx : TranslationContext) (e : Python.expr SourceRang
   -- Bytes literal
   | .Constant _ (.ConBytes _ _) _ =>
     rejectableHole ctx.rejectApproximations
-      "bytes literal" (toString (repr e))
+      "bytes literal" (source := md)
 
   -- Float literal
   | .Constant _ (.ConFloat _ f) _ =>
     match parseFloatString f.val with
     | some d => return floatToAny d
     | none => rejectableHole ctx.rejectApproximations
-                "unparseable float literal" (toString (repr e))
+                "unparseable float literal" (source := md)
 
   -- Complex literal
   | .Constant _ (.ConComplex _ _ _) _ =>
     rejectableHole ctx.rejectApproximations
-      "complex literal" (toString (repr e))
+      "complex literal" (source := md)
 
   -- Ellipsis literal
   | .Constant _ (.ConEllipsis _) _ =>
     rejectableHole ctx.rejectApproximations
-      "ellipsis (...) as expression" (toString (repr e))
+      "ellipsis (...) as expression" (source := md)
 
   -- Variable references
   | .Name _ name _ =>
@@ -643,18 +657,18 @@ partial def translateExpr (ctx : TranslationContext) (e : Python.expr SourceRang
       | .Sub _ => .ok "PSub"
       | .Mult _ => .ok "PMul"
       | .Div _ => return ← rejectableHole ctx.rejectApproximations
-                              "BinOp Div (true division)" (toString (repr e))
+                              "BinOp Div (true division)" (source := md)
       | .FloorDiv _ => .ok "PFloorDiv"  -- Python // maps to Laurel Div
       | .Mod _ => .ok "PMod"
       | .Pow _ => .ok "PPow"
       | .LShift _ => .ok "PLShift"
       | .RShift _ => .ok "PRShift"
       | .BitAnd _ => return ← rejectableHole ctx.rejectApproximations
-                                "BinOp BitAnd" (toString (repr e))
+                                "BinOp BitAnd" (source := md)
       | .BitOr _ => return ← rejectableHole ctx.rejectApproximations
-                               "BinOp BitOr" (toString (repr e))
+                               "BinOp BitOr" (source := md)
       | .BitXor _ => return ← rejectableHole ctx.rejectApproximations
-                                "BinOp BitXor" (toString (repr e))
+                                "BinOp BitXor" (source := md)
       -- Unsupported for now
       | _ => throw (.unsupportedConstruct s!"Binary operator not yet supported: {repr op}" (toString (repr e)))
     return mkStmtExprMdWithLoc (StmtExpr.StaticCall preludeOpnames [leftExpr, rightExpr]) md
@@ -811,10 +825,10 @@ partial def translateExpr (ctx : TranslationContext) (e : Python.expr SourceRang
   -- Interpolation / TemplateStr (Python 3.14+ t-strings) - not yet supported
   | .Interpolation .. =>
     rejectableHole ctx.rejectApproximations
-      "string interpolation (t-string)" (toString (repr e))
+      "string interpolation (t-string)" (source := md)
   | .TemplateStr .. =>
     rejectableHole ctx.rejectApproximations
-      "template string (t-string)" (toString (repr e))
+      "template string (t-string)" (source := md)
 
   | .IfExp _ cond thenb elseb =>
     let condExpr ← translateExpr ctx cond
@@ -883,7 +897,7 @@ partial def translateExpr (ctx : TranslationContext) (e : Python.expr SourceRang
           let hasDispatch := ctx.dispatchFieldTypes[className]?.any (·.contains attr.val)
           if hasDispatch then
             rejectableHole ctx.rejectApproximations
-              s!"dispatch field read (self.{attr.val})" (toString (repr e))
+              s!"dispatch field read (self.{attr.val})" (source := md)
           else
             return fieldExpr
         | _ =>
@@ -892,7 +906,7 @@ partial def translateExpr (ctx : TranslationContext) (e : Python.expr SourceRang
         -- FIXME: Module attribute (e.g., sys.argv): modules are not modeled as
         -- Laurel values, so return Hole like we do for unmodeled package calls.
         rejectableHole ctx.rejectApproximations
-          "module attribute access" (toString (repr e))
+          "module attribute access" (source := md)
       else
         -- Regular object.field access
         let objExpr ← translateExpr ctx obj
@@ -920,7 +934,7 @@ partial def translateExpr (ctx : TranslationContext) (e : Python.expr SourceRang
   -- Abstract: return havoc'd set (sound abstraction)
   | .Set .. =>
     rejectableHole ctx.rejectApproximations
-      "Set literal" (toString (repr e))
+      "Set literal" (source := md)
 
   -- Tuple literal: (1, 2)
   | .Tuple _ elems _ => translateList ctx elems.val.toList
@@ -929,23 +943,23 @@ partial def translateExpr (ctx : TranslationContext) (e : Python.expr SourceRang
   -- Abstract: return havoc'd list (sound abstraction)
   | .ListComp .. =>
     rejectableHole ctx.rejectApproximations
-      "list comprehension" (toString (repr e))
+      "list comprehension" (source := md)
 
   -- Set comprehension: {x for x in items}
   -- Abstract: return havoc'd set (sound abstraction)
   | .SetComp .. =>
     rejectableHole ctx.rejectApproximations
-      "set comprehension" (toString (repr e))
+      "set comprehension" (source := md)
 
   -- Dict comprehension: {k: v for k, v in items}
   | .DictComp .. =>
     rejectableHole ctx.rejectApproximations
-      "dict comprehension" (toString (repr e))
+      "dict comprehension" (source := md)
 
   -- Generator expression: (x for x in items)
   | .GeneratorExp .. =>
     rejectableHole ctx.rejectApproximations
-      "generator expression" (toString (repr e))
+      "generator expression" (source := md)
 
   | _ => throw (.unsupportedConstruct "Expression type not yet supported" (toString (repr e)))
 
@@ -1046,7 +1060,8 @@ partial def coerceToAny (ctx : TranslationContext) (expr : Python.expr SourceRan
   let ty ← inferExprType ctx expr
   if isCompositeType ctx ty then
     rejectableHole ctx.rejectApproximations
-      s!"Composite-to-Any coercion ({ty})" (toString (repr expr))
+      s!"Composite-to-Any coercion ({ty})"
+      (source := sourceRangeToSource ctx.filePath expr.toAst.ann)
   else pure translated
 
 partial def refineFunctionCallExpr (ctx : TranslationContext) (func: Python.expr SourceRange) :
@@ -1262,7 +1277,7 @@ partial def translateCall (ctx : TranslationContext)
     let havocStmts := receiverHavoc ++ argHavoc
     let h ← rejectableHole ctx.rejectApproximations
               s!"unmodeled call to '{funcName}'"
-              (toString (repr f))
+              (source := sourceRangeToSource ctx.filePath f.toAst.ann)
     if havocStmts.isEmpty then
       return h
     else
@@ -1318,7 +1333,7 @@ partial def translateCall (ctx : TranslationContext)
             if ctx.classesInHierarchy.contains classPrefix then
               rejectableHole ctx.rejectApproximations
                 s!"method call '{funcName}' with uncertain inheritance dispatch"
-                (toString (repr f))
+                (source := callMd)
             else
               let callWithSelf := mkStmtExprMdWithLoc
                 (StmtExpr.StaticCall funcName (target_trans :: callArgs)) callMd
@@ -1326,7 +1341,7 @@ partial def translateCall (ctx : TranslationContext)
           else
             rejectableHole ctx.rejectApproximations
               s!"method call '{funcName}' on receiver of unknown type"
-              (toString (repr f))
+              (source := callMd)
         else return mkCall funcName
     | _ => throw (.unsupportedConstruct "Invalid call construct" (toString (repr f)))
   -- When ** is used at the call site and we have a known function signature,
@@ -1880,7 +1895,7 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang
     -- Note: Python while-else not supported yet
     if !orelse.val.isEmpty then
       rejectableDrop ctx.rejectApproximations
-        "while…else clause" (toString (repr s))
+        "while…else clause" (source := md)
     let condExpr ← translateExpr ctx test
     let breakLabel := s!"loop_break_{test.toAst.ann.start.byteIdx}"
     let continueLabel := s!"loop_continue_{test.toAst.ann.start.byteIdx}"
@@ -1974,10 +1989,10 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang
   | .Try _ body handlers orelse finalbody => do
     if !orelse.val.isEmpty then
       rejectableDrop ctx.rejectApproximations
-        "try…else clause" (toString (repr s))
+        "try…else clause" (source := md)
     if !finalbody.val.isEmpty then
       rejectableDrop ctx.rejectApproximations
-        "try…finally clause" (toString (repr s))
+        "try…finally clause" (source := md)
     let tryLabel := s!"try_end_{s.toAst.ann.start.byteIdx}"
     let catchersLabel := s!"exception_handlers_{s.toAst.ann.start.byteIdx}"
     let (bodyCtx, bodyStmts) ← translateStmtList ctx body.val.toList
@@ -2037,7 +2052,7 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang
   -- FIXME: Placeholder — `raise` is dropped so the Hole type inferrer doesn't
   -- produce Unknown types. Must be replaced to correctly model exceptions later.
   | .Raise _ _ _ => do
-    rejectableDrop ctx.rejectApproximations "raise" (toString (repr s))
+    rejectableDrop ctx.rejectApproximations "raise" (source := md)
     return (ctx, [])
 
   -- With statement: with EXPR as VAR: BODY
@@ -2094,7 +2109,7 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang
   | .For _ target iter body orelse _ => do
     if !orelse.val.isEmpty then
       rejectableDrop ctx.rejectApproximations
-        "for…else clause" (toString (repr s))
+        "for…else clause" (source := md)
     -- The iterator expression (we abstract it away).
     -- When the expression contains side-effect statements (e.g. a block with
     -- receiver havoc from an unmodeled method call), bind it to a temporary
@@ -2174,14 +2189,14 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang
     | some lbl => return (ctx, [mkStmtExprMdWithLoc (StmtExpr.Exit lbl) md])
     | none =>
       let h ← rejectableHole ctx.rejectApproximations
-        "break outside enclosing loop" "break"
+        "break outside enclosing loop" (source := md)
       return (ctx, [mkStmtExprMdWithLoc (StmtExpr.Assert { condition := h }) md])
   | .Continue _ =>
     match ctx.loopContinueLabel with
     | some lbl => return (ctx, [mkStmtExprMdWithLoc (StmtExpr.Exit lbl) md])
     | none =>
       let h ← rejectableHole ctx.rejectApproximations
-        "continue outside enclosing loop" "continue"
+        "continue outside enclosing loop" (source := md)
       return (ctx, [mkStmtExprMdWithLoc (StmtExpr.Assert { condition := h }) md])
 
   -- Augmented assignment: x += expr  →  x = x op expr
diff --git a/StrataTest/Languages/Python/RejectApproximationsTest.lean b/StrataTest/Languages/Python/RejectApproximationsTest.lean
index ca5a17b101..29a1c1ac42 100644
--- a/StrataTest/Languages/Python/RejectApproximationsTest.lean
+++ b/StrataTest/Languages/Python/RejectApproximationsTest.lean
@@ -20,29 +20,46 @@ open Strata.Python.TranslationError
 
 -- rejectableHole false -> emits a Hole (lax behavior preserved)
 #guard
-  match rejectableHole false "BinOp Div" "<ast>" with
+  match rejectableHole false "BinOp Div" (astRepr := "<ast>") with
   | .ok ⟨.Hole, _⟩ => true
   | _ => false
 
 -- rejectableHole true -> raises unsupportedConstruct with [approximation] tag
 #guard
-  match rejectableHole true "BinOp Div" "<ast>" with
+  match rejectableHole true "BinOp Div" (astRepr := "<ast>") with
   | .error (.unsupportedConstruct msg _) =>
       msg.startsWith "[approximation]" && (msg.splitOn "BinOp Div").length > 1
   | _ => false
 
 -- rejectableDrop false -> no-op
 #guard
-  match rejectableDrop false "raise" "<ast>" with
+  match rejectableDrop false "raise" (astRepr := "<ast>") with
   | .ok () => true
   | _ => false
 
 -- rejectableDrop true -> raises with "silently dropped" wording
 #guard
-  match rejectableDrop true "raise" "<ast>" with
+  match rejectableDrop true "raise" (astRepr := "<ast>") with
   | .error (.unsupportedConstruct msg _) =>
       msg.startsWith "[approximation]"
         && (msg.splitOn "silently dropped").length > 1
   | _ => false
 
+-- astRepr longer than 200 chars is truncated with an ellipsis
+#guard
+  let big := String.ofList (List.replicate 500 'x')
+  match rejectableHole true "huge" (astRepr := big) with
+  | .error (.unsupportedConstruct _ payload) =>
+      payload.length < big.length && payload.endsWith "…"
+  | _ => false
+
+-- a `source` is preferred over the AST repr for the diagnostic payload
+#guard
+  let fr : Strata.FileRange := ⟨.file "f.py", ⟨⟨10⟩, ⟨20⟩⟩⟩
+  match rejectableHole true "x" (source := some fr) (astRepr := "huge") with
+  | .error (.unsupportedConstruct _ payload) =>
+      (payload.splitOn "huge").length == 1
+        && (payload.splitOn "f.py").length > 1
+  | _ => false
+
 end Strata.Python.RejectApproximationsTest

From 006a03e530fc41798c2ee560ec034fa2dafcce66 Mon Sep 17 00:00:00 2001
From: Jules <julesmt@amazon.com>
Date: Tue, 2 Jun 2026 14:41:57 -0700
Subject: [PATCH 4/6] pyspec: pass TranslationContext to mkInstanceMethodCall

`mkInstanceMethodCall` took a single `rejectApproximations : Bool`
parameter; both call sites just forwarded `ctx.rejectApproximations`.
Take the whole context so future fields don't each grow a new bool
parameter.
---
 Strata/Languages/Python/PythonToLaurel.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/Strata/Languages/Python/PythonToLaurel.lean b/Strata/Languages/Python/PythonToLaurel.lean
index 9c14f4d357..adbc3a68d6 100644
--- a/Strata/Languages/Python/PythonToLaurel.lean
+++ b/Strata/Languages/Python/PythonToLaurel.lean
@@ -272,11 +272,11 @@ def manglePythonMethod (className : String) (methodName : String) : String :=
 /-- Build a StaticCall for an instance method: ClassName@methodName(self, args...).
     For Any-typed receivers (no model available), returns a Hole under lax
     mode, or raises `unsupportedConstruct` under `--reject-approximations`. -/
-def mkInstanceMethodCall (rejectApproximations : Bool) (className : String) (methodName : String)
+def mkInstanceMethodCall (ctx : TranslationContext) (className : String) (methodName : String)
     (self : StmtExprMd) (args : List StmtExprMd)
     (source : Option FileRange := none) : Except TranslationError StmtExprMd :=
   if className == "Any" then
-    rejectableHole rejectApproximations
+    rejectableHole ctx.rejectApproximations
       s!"instance method call '{methodName}' on Any-typed receiver"
       (source := source)
   else
@@ -2071,8 +2071,8 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang
         let mgrDecl := mkVarDeclInit mgrName mgrLauTy mgrExpr
         let mgrRef := mkStmtExprMd (StmtExpr.Var (.Local mgrName))
         currentCtx := {currentCtx with variableTypes := currentCtx.variableTypes ++ [(mgrName, mgrTy)]}
-        let enterCall ← mkInstanceMethodCall ctx.rejectApproximations mgrTy "__enter__" mgrRef [] md
-        let exitCall ← mkInstanceMethodCall ctx.rejectApproximations mgrTy "__exit__" mgrRef [] md
+        let enterCall ← mkInstanceMethodCall ctx mgrTy "__enter__" mgrRef [] md
+        let exitCall ← mkInstanceMethodCall ctx mgrTy "__exit__" mgrRef [] md
         match optVars.val with
         | some varExpr =>
           let varName := pyExprToString varExpr

From 49bfb26b173fc9c1cec6eb95d31995f0dfa03f19 Mon Sep 17 00:00:00 2001
From: Jules <julesmt@amazon.com>
Date: Tue, 2 Jun 2026 14:42:07 -0700
Subject: [PATCH 5/6] pyspec: centralize the [approximation] message format
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Three places currently spell out the `[approximation] ` prefix and the
strict-mode wording inline: `rejectableHole`, `rejectableDrop`, and the
`specWarning` warning→error promotion in `Specs.lean`. They were
already drifting.

Add a small `Strata.Languages.Python.Approximation` module with a
`Kind` (`hole | drop | warningPromotion`), a single `prefixTag`, and a
`render` function. All three sites now route through it. New sites
won't need to retype the prefix.
---
 Strata/Languages/Python/Approximation.lean    | 50 +++++++++++++++++++
 Strata/Languages/Python/PythonToLaurel.lean   |  5 +-
 Strata/Languages/Python/Specs.lean            |  3 +-
 .../Python/RejectApproximationsTest.lean      | 32 ++++++++++++
 4 files changed, 87 insertions(+), 3 deletions(-)
 create mode 100644 Strata/Languages/Python/Approximation.lean

diff --git a/Strata/Languages/Python/Approximation.lean b/Strata/Languages/Python/Approximation.lean
new file mode 100644
index 0000000000..ca169f5d59
--- /dev/null
+++ b/Strata/Languages/Python/Approximation.lean
@@ -0,0 +1,50 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+module
+
+/-!
+# Approximation diagnostics
+
+Single source of truth for the wording and `[approximation]` prefix used by
+both the Python→Laurel translator and the PySpec parser when an unsupported
+Python construct is approximated (or silently dropped) under lax mode and
+would be rejected as an error under `--reject-approximations`. Keeping the
+prefix in one place lets downstream tooling filter on it reliably.
+-/
+
+public section
+
+namespace Strata.Python.Approximation
+
+/-- Kind of approximation site. -/
+inductive Kind where
+  /-- The translator emits a havoc'd `Hole` instead of a faithful translation. -/
+  | hole
+  /-- The translator silently drops the construct from the lowered program. -/
+  | drop
+  /-- The PySpec parser fell back to `.placeholder` and emitted a warning;
+      strict mode promotes that warning to an error. -/
+  | warningPromotion
+  deriving DecidableEq, Repr
+
+/-- The `[approximation] ` prefix that downstream tooling filters on. Must
+    not change without coordinating with consumers. -/
+def prefixTag : String := "[approximation] "
+
+/-- Render a strict-mode approximation diagnostic. The `construct` argument
+    names the surface form (e.g. `"BinOp Div"`) for `.hole` and `.drop`; for
+    `.warningPromotion`, it carries the original warning message verbatim. -/
+def render : Kind → (construct : String) → String
+  | .hole, c =>
+    s!"{prefixTag}{c} is approximated as Hole; not in the sound subset"
+  | .drop, c =>
+    s!"{prefixTag}{c} is silently dropped by current translation; not in the sound subset"
+  | .warningPromotion, msg =>
+    s!"{prefixTag}{msg}"
+
+end Strata.Python.Approximation
+
+end
diff --git a/Strata/Languages/Python/PythonToLaurel.lean b/Strata/Languages/Python/PythonToLaurel.lean
index adbc3a68d6..bc1b988c71 100644
--- a/Strata/Languages/Python/PythonToLaurel.lean
+++ b/Strata/Languages/Python/PythonToLaurel.lean
@@ -9,6 +9,7 @@ public import Strata.Languages.Core.Program
 public import Strata.Languages.Laurel.Laurel
 public import Strata.Languages.Python.OverloadTable
 public import Strata.Languages.Python.PythonDialect
+import Strata.Languages.Python.Approximation
 import Strata.Languages.Python.PythonRuntimeLaurelPart
 import Strata.Util.DecideProp
 
@@ -239,7 +240,7 @@ def rejectableHole (rejectApproximations : Bool) (construct : String)
     : Except TranslationError StmtExprMd :=
   if rejectApproximations then
     throw (.unsupportedConstruct
-      s!"[approximation] {construct} is approximated as Hole; not in the sound subset"
+      (Strata.Python.Approximation.render .hole construct)
       (approximationAstPayload source astRepr))
   else
     pure (mkStmtExprMdWithLoc .Hole source)
@@ -252,7 +253,7 @@ def rejectableDrop (rejectApproximations : Bool) (construct : String)
     : Except TranslationError Unit :=
   if rejectApproximations then
     throw (.unsupportedConstruct
-      s!"[approximation] {construct} is silently dropped by current translation; not in the sound subset"
+      (Strata.Python.Approximation.render .drop construct)
       (approximationAstPayload source astRepr))
   else
     pure ()
diff --git a/Strata/Languages/Python/Specs.lean b/Strata/Languages/Python/Specs.lean
index 5425161e9d..8699ee68f2 100644
--- a/Strata/Languages/Python/Specs.lean
+++ b/Strata/Languages/Python/Specs.lean
@@ -7,6 +7,7 @@ module
 
 import        Strata.DDM.Format
 import all    Strata.DDM.Util.Fin
+import        Strata.Languages.Python.Approximation
 import        Strata.Languages.Python.ReadPython
 import        Strata.Languages.Python.Specs.DDM
 public import Strata.Languages.Python.Specs.Decls
@@ -308,7 +309,7 @@ instance : PySpecMClass PySpecM where
     -- error: the parser only emits warnings on patterns it falls back to
     -- `.placeholder` for, which silently drops the user's spec.
     if ctx.rejectApproximations then
-      specErrorAt ctx.pythonFile loc s!"[approximation] {message}"
+      specErrorAt ctx.pythonFile loc (Strata.Python.Approximation.render .warningPromotion message)
     else
       let w : PipelineMessage := { file := ctx.pythonFile, loc, phase := pySpecParsingPhase, kind := .pySpecParsingWarning, message }
       modify fun s => { s with warnings := s.warnings.push w }
diff --git a/StrataTest/Languages/Python/RejectApproximationsTest.lean b/StrataTest/Languages/Python/RejectApproximationsTest.lean
index 29a1c1ac42..eaef3fe0e1 100644
--- a/StrataTest/Languages/Python/RejectApproximationsTest.lean
+++ b/StrataTest/Languages/Python/RejectApproximationsTest.lean
@@ -4,6 +4,7 @@
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
 
+import Strata.Languages.Python.Approximation
 import Strata.Languages.Python.PythonToLaurel
 
 /-! # `--reject-approximations` flag tests
@@ -62,4 +63,35 @@ open Strata.Python.TranslationError
         && (payload.splitOn "f.py").length > 1
   | _ => false
 
+/-! ## Shared `Approximation.render` format
+
+All three approximation sites — `rejectableHole`, `rejectableDrop`, and
+`Specs.lean`'s `specWarning` warning→error promotion — render through
+`Strata.Python.Approximation.render`. The guards below pin the prefix
+and per-kind wording so the three sites cannot drift apart. -/
+
+open Strata.Python.Approximation (render Kind prefixTag)
+
+#guard (render .hole "BinOp Div").startsWith prefixTag
+#guard (render .drop "raise").startsWith prefixTag
+#guard (render .warningPromotion "fallback to placeholder").startsWith prefixTag
+
+#guard prefixTag == "[approximation] "
+
+#guard ((render .hole "X").splitOn "approximated as Hole").length > 1
+#guard ((render .drop "X").splitOn "silently dropped").length > 1
+#guard render .warningPromotion "msg" == "[approximation] msg"
+
+-- The strict-mode arm of `rejectableHole` shares wording with `render .hole`.
+#guard
+  match rejectableHole true "X" with
+  | .error (.unsupportedConstruct msg _) => msg == render .hole "X"
+  | _ => false
+
+-- Likewise for `rejectableDrop`.
+#guard
+  match rejectableDrop true "X" with
+  | .error (.unsupportedConstruct msg _) => msg == render .drop "X"
+  | _ => false
+
 end Strata.Python.RejectApproximationsTest

From d904dd01d4250e25e2ed63eb8dc1d19d5d13a149 Mon Sep 17 00:00:00 2001
From: Jules <julesmt@amazon.com>
Date: Tue, 2 Jun 2026 14:42:15 -0700
Subject: [PATCH 6/6] pyspec: lock in rejectableHole/Drop dispatch with
 theorems

Add four `rfl`-provable lemmas that pin the strict/lax branch of
`rejectableHole` and `rejectableDrop`, plus existence lemmas pinning
the strict-mode message to `Approximation.render`. A future refactor
that flips a branch or drifts the prefix won't compile.
---
 .../Python/RejectApproximationsTest.lean      | 33 +++++++++++++++++++
 1 file changed, 33 insertions(+)

diff --git a/StrataTest/Languages/Python/RejectApproximationsTest.lean b/StrataTest/Languages/Python/RejectApproximationsTest.lean
index eaef3fe0e1..c114263aca 100644
--- a/StrataTest/Languages/Python/RejectApproximationsTest.lean
+++ b/StrataTest/Languages/Python/RejectApproximationsTest.lean
@@ -19,6 +19,39 @@ namespace Strata.Python.RejectApproximationsTest
 open Strata.Python (rejectableHole rejectableDrop)
 open Strata.Python.TranslationError
 
+/-! ## Boolean dispatch lemmas
+
+Pin the bool branch of `rejectableHole` / `rejectableDrop` so a future
+refactor cannot accidentally reverse the strict/lax meaning. -/
+
+theorem rejectableHole_strict (c : String) (r : String) :
+    (rejectableHole (rejectApproximations := true) c (astRepr := r)).isOk = false := rfl
+
+theorem rejectableHole_lax (c : String) (r : String) :
+    (rejectableHole (rejectApproximations := false) c (astRepr := r)).isOk = true := rfl
+
+theorem rejectableDrop_strict (c : String) (r : String) :
+    (rejectableDrop (rejectApproximations := true) c (astRepr := r)).isOk = false := rfl
+
+theorem rejectableDrop_lax (c : String) (r : String) :
+    (rejectableDrop (rejectApproximations := false) c (astRepr := r)).isOk = true := rfl
+
+/-- Strict mode produces a `.unsupportedConstruct` whose message starts
+    with `Approximation.prefixTag`. Downstream tooling can rely on this. -/
+theorem rejectableHole_strict_message (c : String) (r : String) :
+    ∃ msg ast,
+      rejectableHole (rejectApproximations := true) c (astRepr := r)
+        = .error (.unsupportedConstruct msg ast)
+      ∧ msg = Strata.Python.Approximation.render .hole c :=
+  ⟨_, _, rfl, rfl⟩
+
+theorem rejectableDrop_strict_message (c : String) (r : String) :
+    ∃ msg ast,
+      rejectableDrop (rejectApproximations := true) c (astRepr := r)
+        = .error (.unsupportedConstruct msg ast)
+      ∧ msg = Strata.Python.Approximation.render .drop c :=
+  ⟨_, _, rfl, rfl⟩
+
 -- rejectableHole false -> emits a Hole (lax behavior preserved)
 #guard
   match rejectableHole false "BinOp Div" (astRepr := "<ast>") with