From 8a1c7b00501fc0213aa38ce66dff7b0df0c74384 Mon Sep 17 00:00:00 2001 From: Massart Date: Tue, 5 May 2026 09:47:59 -0700 Subject: [PATCH 1/2] Python: skip Any_to_bool for bool-typed assert conditions (#1102) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit When an assert condition translates to a .Hole (e.g. a call to an unmodelled function like isinstance), the assert translator hoists it into a fresh bool-typed variable. Unconditionally wrapping that variable in Any_to_bool is ill-typed since Any_to_bool : Any -> bool, producing: Impossible to unify (arrow Any bool) with (arrow bool $__ty…) Check the invariant directly: if the translated condition is already a reference to a bool-typed local, skip the Any_to_bool coercion. This handles the Hole-hoisting path and any future path producing a bool-typed identifier uniformly. Adds regression fixtures under StrataTestExtra/Languages/Python/Issue1102/ and a Lean test harness that asserts the translation pipeline produces no type-check or Laurel-to-Core crash on the minimal fuzz reproductions from issue #1102 (seed 1777894483, fuzz_semantic_0004). --- Strata/Languages/Python/PythonToLaurel.lean | 16 +++- .../Python/Issue1102/isinstance_if.py | 6 ++ .../Python/Issue1102/isinstance_int.py | 4 + .../Python/Issue1102/isinstance_list.py | 4 + .../Languages/Python/Issue1102Test.lean | 77 +++++++++++++++++++ 5 files changed, 105 insertions(+), 2 deletions(-) create mode 100644 StrataTestExtra/Languages/Python/Issue1102/isinstance_if.py create mode 100644 StrataTestExtra/Languages/Python/Issue1102/isinstance_int.py create mode 100644 StrataTestExtra/Languages/Python/Issue1102/isinstance_list.py create mode 100644 StrataTestExtra/Languages/Python/Issue1102Test.lean diff --git a/Strata/Languages/Python/PythonToLaurel.lean b/Strata/Languages/Python/PythonToLaurel.lean index d6cbbd7c98..d08d2f49cc 100644 --- a/Strata/Languages/Python/PythonToLaurel.lean +++ b/Strata/Languages/Python/PythonToLaurel.lean @@ -1736,7 +1736,8 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang let summary := match msg.val with | some (.Constant _ (.ConString _ str) _) => some str.val | _ => none - -- Check if condition contains a Hole - if so, hoist to variable + -- Hoist unmodelled conditions (e.g. isinstance(...)) into a fresh + -- bool-typed variable. let (condStmts, finalCondExpr, condCtx) := match condExpr.val with | .Hole => @@ -1747,7 +1748,18 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang ([varDecl], varRef, { ctx with variableTypes := ctx.variableTypes ++ [(freshVar, "bool")] }) | _ => ([], condExpr, ctx) - let assertStmt := mkStmtExprMdWithLoc (StmtExpr.Assert { condition := Any_to_bool finalCondExpr, summary }) md + -- Skip Any_to_bool when the condition is already a bool-typed local; + -- wrapping it would produce ill-typed Any_to_bool(bool). See #1102. + let isBoolTypedVar : Bool := + match finalCondExpr.val with + | .Var (.Local name) => + match condCtx.variableTypes.find? (fun (n, _) => n == name) with + | some (_, ty) => ty == PyLauType.Bool + | none => false + | _ => false + let coercedCond := + if isBoolTypedVar then finalCondExpr else Any_to_bool finalCondExpr + let assertStmt := mkStmtExprMdWithLoc (StmtExpr.Assert { condition := coercedCond, summary }) md -- Wrap in block if we hoisted condition let result := if condStmts.isEmpty then diff --git a/StrataTestExtra/Languages/Python/Issue1102/isinstance_if.py b/StrataTestExtra/Languages/Python/Issue1102/isinstance_if.py new file mode 100644 index 0000000000..08877c0321 --- /dev/null +++ b/StrataTestExtra/Languages/Python/Issue1102/isinstance_if.py @@ -0,0 +1,6 @@ +def main(): + x: int = 5 + if isinstance(x, int): + assert x > 0 + +main() diff --git a/StrataTestExtra/Languages/Python/Issue1102/isinstance_int.py b/StrataTestExtra/Languages/Python/Issue1102/isinstance_int.py new file mode 100644 index 0000000000..224d6f3f83 --- /dev/null +++ b/StrataTestExtra/Languages/Python/Issue1102/isinstance_int.py @@ -0,0 +1,4 @@ +def main(): + assert isinstance(5, int) + +main() diff --git a/StrataTestExtra/Languages/Python/Issue1102/isinstance_list.py b/StrataTestExtra/Languages/Python/Issue1102/isinstance_list.py new file mode 100644 index 0000000000..19d5959fd2 --- /dev/null +++ b/StrataTestExtra/Languages/Python/Issue1102/isinstance_list.py @@ -0,0 +1,4 @@ +def main(): + assert isinstance([1], list) + +main() diff --git a/StrataTestExtra/Languages/Python/Issue1102Test.lean b/StrataTestExtra/Languages/Python/Issue1102Test.lean new file mode 100644 index 0000000000..942444ec75 --- /dev/null +++ b/StrataTestExtra/Languages/Python/Issue1102Test.lean @@ -0,0 +1,77 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import StrataTest.Languages.Python.TestExamples +import StrataTest.Util.TestDiagnostics + +open StrataTest.Util +open Strata.Python (processPythonFile withPython) +open Strata.Parser (stringInputContext) +open Strata + +namespace Strata.Python.Issue1102 + +/-! Regression test for #1102: `isinstance(...)` inside `assert` must not +crash the Python-to-Laurel-to-Core translation pipeline. Before the fix +these programs failed in Laurel type checking with +"Impossible to unify (arrow Any bool) with (arrow bool $__ty…)". + +Each fixture snapshots both the diagnostic `type` and the full rendered +message, so a silent-drop regression (translating the assert to a no-op) +or a message reword would also fail. Fixtures live in `Issue1102/`. + +Note: compound assert conditions such as `isinstance(x, T) and x > 0` or +`not isinstance(x, T)` currently trip a *separate* StrataBug ("block +expression should have been lowered in a separate pass") that is +independent of #1102 and should be tracked in its own issue. -/ + +private meta def fixtureDir : System.FilePath := + "StrataTestExtra/Languages/Python/Issue1102" + +/-- Render a diagnostic as a single deterministic line: +"type @ line:colStart-colEnd :: message". -/ +private def renderDiag (d : Diagnostic) : String := + s!"{repr d.type} @ {d.start.line}:{d.start.column}-{d.ending.column} :: {d.message}" + +/-- Load a fixture and print each diagnostic on its own line, prefixed +with the fixture name. Prefer this over ad-hoc prose filters: it asserts +structurally on `type` and keeps the full message in the snapshot. -/ +private def snapshotDiags (pythonCmd : System.FilePath) (pyFile : String) : IO Unit := do + let path := fixtureDir / pyFile + let source ← IO.FS.readFile path + let diags ← processPythonFile pythonCmd (stringInputContext pyFile source) + for d in diags do + IO.println s!"{pyFile}: {renderDiag d}" + -- Belt-and-braces structural check: any StrataBug is a regression. + if diags.any (fun d => d.type == Strata.DiagnosticType.StrataBug) then + throw <| .userError s!"{pyFile}: unexpected StrataBug diagnostic" + +-- `assert isinstance(5, int)` — the minimal fuzz reproduction. Before +-- the fix this raised a Laurel type error; after the fix the pipeline +-- completes and the verifier reports the assertion as unprovable +-- (expected, since `isinstance` is unmodelled). +/-- +info: isinstance_int.py: Strata.DiagnosticType.UserError @ 2:4-29 :: assertion could not be proved +-/ +#guard_msgs in +#eval withPython fun pythonCmd => snapshotDiags pythonCmd "isinstance_int.py" + +-- `assert isinstance([1], list)` — the original fuzz_semantic_0004 shape. +/-- +info: isinstance_list.py: Strata.DiagnosticType.UserError @ 2:4-32 :: assertion could not be proved +-/ +#guard_msgs in +#eval withPython fun pythonCmd => snapshotDiags pythonCmd "isinstance_list.py" + +-- `if isinstance(x, int): assert x > 0` — the non-hoisting .If path, +-- included to show the fix does not affect the path that already worked. +/-- +info: isinstance_if.py: Strata.DiagnosticType.UserError @ 4:8-20 :: assertion could not be proved +-/ +#guard_msgs in +#eval withPython fun pythonCmd => snapshotDiags pythonCmd "isinstance_if.py" + +end Strata.Python.Issue1102 From 2206f4384cb2fd5c7ba2fa559afc377d686f6205 Mon Sep 17 00:00:00 2001 From: Jules Date: Wed, 6 May 2026 09:20:37 -0700 Subject: [PATCH 2/2] Surface alreadyBool flag from hoisting match in assert translation Replaces the downstream variableTypes.find? + string comparison with a Bool produced directly by the match arm that constructs the bool-typed ref. This removes two fragilities flagged on #1102: - Renaming PyLauType.Bool no longer affects the Any_to_bool skip. - A future pass filtering/replacing variableTypes between hoisting and the check also can't silently regress back to Any_to_bool(bool). Also swaps the string literal "bool" for PyLauType.Bool in the variableTypes insertion for consistency. --- Strata/Languages/Python/PythonToLaurel.lean | 20 ++++++++------------ 1 file changed, 8 insertions(+), 12 deletions(-) diff --git a/Strata/Languages/Python/PythonToLaurel.lean b/Strata/Languages/Python/PythonToLaurel.lean index d08d2f49cc..5a2e9f8f5f 100644 --- a/Strata/Languages/Python/PythonToLaurel.lean +++ b/Strata/Languages/Python/PythonToLaurel.lean @@ -1737,28 +1737,24 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang | some (.Constant _ (.ConString _ str) _) => some str.val | _ => none -- Hoist unmodelled conditions (e.g. isinstance(...)) into a fresh - -- bool-typed variable. - let (condStmts, finalCondExpr, condCtx) := + -- bool-typed variable. The `alreadyBool` flag records, at the point of + -- construction, whether `finalCondExpr` is statically known to have type + -- bool -- avoiding a fragile round-trip through `variableTypes` later. + -- See #1102. + let (condStmts, finalCondExpr, condCtx, alreadyBool) := match condExpr.val with | .Hole => let freshVar := s!"assert_cond_{test.toAst.ann.start.byteIdx}" let varType := mkHighTypeMd .TBool let varDecl := mkVarDeclInit freshVar varType condExpr let varRef := mkStmtExprMd (StmtExpr.Var (.Local freshVar)) - ([varDecl], varRef, { ctx with variableTypes := ctx.variableTypes ++ [(freshVar, "bool")] }) - | _ => ([], condExpr, ctx) + ([varDecl], varRef, { ctx with variableTypes := ctx.variableTypes ++ [(freshVar, PyLauType.Bool)] }, true) + | _ => ([], condExpr, ctx, false) -- Skip Any_to_bool when the condition is already a bool-typed local; -- wrapping it would produce ill-typed Any_to_bool(bool). See #1102. - let isBoolTypedVar : Bool := - match finalCondExpr.val with - | .Var (.Local name) => - match condCtx.variableTypes.find? (fun (n, _) => n == name) with - | some (_, ty) => ty == PyLauType.Bool - | none => false - | _ => false let coercedCond := - if isBoolTypedVar then finalCondExpr else Any_to_bool finalCondExpr + if alreadyBool then finalCondExpr else Any_to_bool finalCondExpr let assertStmt := mkStmtExprMdWithLoc (StmtExpr.Assert { condition := coercedCond, summary }) md -- Wrap in block if we hoisted condition