strata-org · julesmt · May 21, 2026
@@ -429,6 +429,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
@@ -470,7 +471,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}")

@@ -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 }
@@ -577,21 +608,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 +641,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 +808,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
@@ -846,7 +889,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 +916,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)))
 
@@ -1703,8 +1757,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 +1852,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 +1917,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__()
@@ -1907,7 +1972,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
@@ -2714,6 +2782,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 +2891,8 @@ def pythonToLaurel (info : PreludeInfo)
     compositeTypeReverse := compositeTypeReverse,
     exhaustiveClasses := exhaustiveClasses,
     classesInHierarchy := classesInHierarchy,
-    filePath := filePath
+    filePath := filePath,
+    rejectApproximations := rejectApproximations
   }
 
   -- Separate functions from other statements

@@ -587,6 +587,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 +615,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

@@ -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