Skip to content

Python: skip Any_to_bool for bool-typed assert conditions (#1102) #1119

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
julesmt wants to merge 2 commits into
base: main
Choose a base branch
from
Open

Python: skip Any_to_bool for bool-typed assert conditions (#1102) #1119

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
8a1c7b0
Python: skip Any_to_bool for bool-typed assert conditions (#1102)
May 5, 2026
2206f43
Surface alreadyBool flag from hoisting match in assert translation
May 6, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
20 changes: 14 additions & 6 deletions Strata/Languages/Python/PythonToLaurel.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1736,18 +1736,26 @@ 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
let (condStmts, finalCondExpr, condCtx) :=
-- Hoist unmodelled conditions (e.g. isinstance(...)) into a fresh
-- 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)

let assertStmt := mkStmtExprMdWithLoc (StmtExpr.Assert { condition := Any_to_bool finalCondExpr, summary }) md
([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 coercedCond :=
if alreadyBool then finalCondExpr else Any_to_bool finalCondExpr
let assertStmt := mkStmtExprMdWithLoc (StmtExpr.Assert { condition := coercedCond, summary }) md
Comment on lines +1744 to +1758
Copy link
Copy Markdown
Contributor

@tautschnig tautschnig May 7, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Stylistic simplification: alreadyBool is used in exactly one if. You can push the Any_to_bool decision directly into the match arms and drop both the flag and the separate conditional. This is shorter, and the "bool-typed reference needs no coercion" invariant then lives at the site that establishes it rather than being re-asserted three lines later:

Suggested change
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)
let assertStmt := mkStmtExprMdWithLoc (StmtExpr.Assert { condition := Any_to_bool finalCondExpr, summary }) md
([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 coercedCond :=
if alreadyBool then finalCondExpr else Any_to_bool finalCondExpr
let assertStmt := mkStmtExprMdWithLoc (StmtExpr.Assert { condition := coercedCond, summary }) md
-- Hoist unmodelled conditions (e.g. isinstance(...)) into a fresh
-- bool-typed variable, and pick the coerced-condition expression for
-- the assert up-front so the "already bool, don't re-wrap" invariant
-- lives at the point where it is established. Wrapping a bool-typed
-- ref in `Any_to_bool : Any → bool` produces ill-typed
-- `Any_to_bool(bool)` — see #1102.
let (condStmts, coercedCond, condCtx) :=
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))
-- `varRef` is declared `TBool`; no `Any_to_bool` wrap needed.
([varDecl], varRef,
{ ctx with variableTypes := ctx.variableTypes ++ [(freshVar, PyLauType.Bool)] })
| _ =>
([], Any_to_bool condExpr, ctx)
let assertStmt := mkStmtExprMdWithLoc (StmtExpr.Assert { condition := coercedCond, summary }) md

Keeps the same behaviour — happy to leave as-is if you prefer the explicit flag for future extensibility (e.g. a second hoisting path that also produces a bool-typed ref), but in that case the comment should say so.


-- Wrap in block if we hoisted condition
let result := if condStmts.isEmpty then
Expand Down
6 changes: 6 additions & 0 deletions StrataTestExtra/Languages/Python/Issue1102/isinstance_if.py
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
def main():
x: int = 5
if isinstance(x, int):
assert x > 0

main()
4 changes: 4 additions & 0 deletions StrataTestExtra/Languages/Python/Issue1102/isinstance_int.py
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
def main():
assert isinstance(5, int)

main()
4 changes: 4 additions & 0 deletions StrataTestExtra/Languages/Python/Issue1102/isinstance_list.py
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
def main():
assert isinstance([1], list)

main()
77 changes: 77 additions & 0 deletions StrataTestExtra/Languages/Python/Issue1102Test.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 :=
Copy link
Copy Markdown
Contributor

@tautschnig tautschnig May 7, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This header comment is exactly the kind of documentation reviewers-of-the-future will thank you for — it explicitly names the adjacent bug ("block expression should have been lowered in a separate pass") and which shapes are in / out of scope. One small add: a tracking issue number for that separate bug, if one exists, so the reader can look it up. If it doesn't exist yet, filing it now and linking it here keeps this test's scope honest (so someone doesn't later "fix" this file by adding the compound cases and being surprised they still fail).

"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"
Comment on lines +39 to +50
Copy link
Copy Markdown
Contributor

@tautschnig tautschnig May 7, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Proof / property-coverage suggestion. The correctness of this fix depends on one invariant of translateStmt .Assert:

If the .Hole arm fires, the resulting coercedCond does not contain the subterm Any_to_bool (Var (Local freshVar)) where variableTypes[freshVar] = PyLauType.Bool.

This is straightforwardly checkable in Lean via pattern recognition on the returned StmtExprMd. Adding one #guard that inspects the translated AST directly (rather than routing through the verifier diagnostics) would turn the load-bearing invariant into a machine-checked property and wouldn't depend on the Python runtime being present (so it'd also run under plain lake build, not just lake test):

/-- Reject any `Any_to_bool` applied to a reference to a bool-typed local.
    Traverses the Laurel AST; conservatively over-approximates "bool-typed"
    by consulting the passed-in `variableTypes`. -/
def containsAnyToBoolOfBoolVar (vt : List (String × String)) : StmtExprMd → Bool := …

#guard
  let src := "def main():\n    assert isinstance(5, int)\n\nmain()\n"
  let ast ← … (run translator up to translateStmt on the Assert) …
  !containsAnyToBoolOfBoolVar ast.variableTypes ast.stmt

Alternatively — and I realise this is more involved — a small inductive lemma on the translator would nail it formally, roughly:

theorem translateAssert_no_Any_to_bool_of_bool
    (ctx : TranslationContext) (test msg : …)
    (h : someWellFormednessHypothesis ctx) :
    let (_, stmts) := translateStmt ctx (.Assert _ test msg)
    ∀ s ∈ stmts, ¬ containsAnyToBoolOfBoolVar ctx.variableTypes s

I don't expect either proof in this PR (the translator is partial and doesn't currently admit this style of reasoning without groundwork), but a minimal AST-inspection #guard is low-cost and would outlive any future message/diagnostic reword. Flagging as the testing direction most aligned with this PR's intent — diagnostic snapshots catch "it doesn't crash", AST inspection catches "the shape we expect is what we produce".


-- `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"
Comment on lines +52 to +75
Copy link
Copy Markdown
Contributor

@tautschnig tautschnig May 7, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The three fixtures cover the main Hole-hoisting paths well. A few more that would make this suite robust to adjacent refactors:

  1. assert isinstance(5, int), "must be int" — exercises both the Hole-hoisting path and the summary-extraction branch (line 1737's msg.val match) simultaneously. If someone ever reorders let summary := and the hoisting match, or introduces a dependency between them, this catches it. The summary "must be int" should show up in the verifier's property summary.

  2. "Should still coerce" case — the current suite only confirms the fix doesn't break working paths. Nothing confirms it doesn't over-apply. A fixture whose condition is a bool-typed local not introduced by Hole-hoisting — e.g. assert (x > 0) where x > 0 translates via the non-.Hole arm and is legitimately an Any-typed expression in the current pipeline — pins down that the _ => arm still emits Any_to_bool. This is cheap insurance against a future refactor that infers alreadyBool from variableTypes instead of from the match arm and then silently accepts false positives.

  3. assert isinstance(x, int) and x > 0 / assert not isinstance(x, int) — your header comment correctly notes these hit a separate StrataBug. Worth adding them as xfail-style fixtures here (asserting that the StrataBug is produced) so the day that separate bug gets fixed, this test file is the one that tells the fixer to come back and update the snapshot. A tracking issue number in the comment would also help.

Concrete proposal for (3): snapshot the current behaviour explicitly:

-- `assert isinstance(x, int) and x > 0` — tracks the separate
-- "block expression should have been lowered" StrataBug mentioned in
-- the header. When this fixture starts producing a UserError instead,
-- that separate bug has been fixed and this snapshot needs updating.
/--
info: isinstance_and.py: Strata.DiagnosticType.StrataBug @ … :: …
-/
#guard_msgs in
#eval withPython fun pythonCmd => snapshotDiags pythonCmd "isinstance_and.py"

(For this one, you'd also want to drop the "any StrataBug is a regression" guard in snapshotDiags, or parameterise it with an allowStrataBug : Bool knob, since by construction this fixture is producing one on purpose.)


end Strata.Python.Issue1102
Loading