Propagate Python assert messages as Laurel property summaries

[tautschnig]

Python assert with string message (e.g., assert x > 0, "positive") now flows through as a Laurel property summary. CBMC displays these as property descriptions instead of opaque labels.

Before: [main.1] line 2 assert(38): SUCCESS
After: [main.1] line 2 sum is reflexive: SUCCESS

Only simple string literals are supported; f-strings and non-string messages are silently ignored (the label is used as fallback).

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

[Copilot]

Pull request overview

This PR propagates Python assert string-literal messages into Laurel metadata as propertySummary, enabling downstream backends (notably CBMC) to show meaningful property descriptions instead of generated labels.

Changes:

• Update Python assert statement translation to capture simple string-literal messages.
• Attach the extracted message to the translated Laurel assert via MetaData.withPropertySummary.

Comments suppressed due to low confidence (1)

Strata/Languages/Python/PythonToLaurel.lean:992

• This change introduces user-visible behavior (assert message → propertySummary) that is intended to affect downstream reporting (e.g., CBMC property descriptions), but the existing Python golden/e2e tests don’t appear to assert on property summaries. Please add/extend a test that fails if the assert message is not propagated (e.g., inspect generated Laurel/Core metadata or the produced GOTO source-location comment), so regressions are caught automatically.

  | .Assert _ test msg => do
    let condExpr ← translateExpr ctx test
    -- Extract assert message as property summary
    let md := match msg.val with
      | some (.Constant _ (.ConString _ str) _) => md.withPropertySummary str.val
      | _ => md
    -- Check if condition contains a Hole - if so, hoist to variable
    let (condStmts, finalCondExpr, condCtx) :=
      match condExpr.val with
      | .Hole =>
        let freshVar := s!"assert_cond_{test.toAst.ann.start.byteIdx}"
        let varType := mkHighTypeMd .TBool
        let varDecl := mkStmtExprMd (StmtExpr.LocalVariable freshVar varType (some condExpr))
        let varRef := mkStmtExprMd (StmtExpr.Identifier freshVar)
        ([varDecl], varRef, { ctx with variableTypes := ctx.variableTypes ++ [(freshVar, "bool")] })
      | _ => ([], condExpr, ctx)

    let assertStmt := mkStmtExprMdWithLoc (StmtExpr.Assert (Any_to_bool finalCondExpr)) md

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[Copilot]

Pull request overview

This PR propagates Python assert string messages into Laurel property summaries so that downstream GOTO/CBMC output displays meaningful property descriptions instead of opaque labels.

Changes:

• Extend Python→Laurel translation to attach assert ... , "message" as MetaData.propertySummary on generated Laurel assert.
• Add a Python-focused regression test that checks the resulting GOTO JSON includes the message in sourceLocation.comment.
• Add an end-to-end Laurel→GOTO→CBMC shell test that verifies property summaries appear in CBMC’s output.

Reviewed changes

Copilot reviewed 3 out of 3 changed files in this pull request and generated 5 comments.

File	Description
Strata/Languages/Python/PythonToLaurel.lean	Extracts constant string assert messages and stores them as property summary metadata.
StrataTest/Languages/Python/tests/test_property_summary.sh	New test that generates GOTO JSON from Python and asserts the summary comment is present.
StrataTest/Backends/CBMC/GOTO/test_property_summary_e2e.sh	New E2E test ensuring property summaries survive through CBMC output.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[aqjune-aws]

It seems this can potentially help better diagnostics when Core -> SMT path is used too.

[keyboardDrummer]

I have several concerns with a test like this:

• It interweaves test framework and test contents code
• The test framework part is not reusable.
• It mixes programming languages
• It's not run on lake test
• It's not obvious what the user experience when running Strata on the input program

Can we write this test in Lean so it'll run on lake test ?
Can we place the results that the user will see, inline in the test?

[tautschnig]

Thank you for pushing me to do the right thing, I admittedly had been cutting a corner here. I believe b1c0e0e implements your request.

[MikaelMayer]

I feel uncomfortable having a bash script to do this kind of testing. First is this script executed anywhere in the CI? Second, as soon as we want to make more end to end tests, it's likely agents will simply want to make a variation of this file, meaning things will get duplicated and hard to maintain.
At the minimum I would like to see the test program and expectations in two different separate files from the machinery that verifies that the current strata converts the test to the expectations correctly.
That way the machinery can ideally be reused as well.

[tautschnig]

Yes, this is part of CI. If you are uncomfortable with bash, what would you be comfortable with instead?

[keyboardDrummer]

IMO we should use the same style of testing as Laurel uses for Python as well, so this test would simplify to a .lean file containing

def program := # strata
program Python;

def main(x: int) -> None:
    assert x == x + 1, "a big lie"
#          ^^^^^^^^^^ error: a big lie does not hold

#end

#guard_msgs(drop info, error) in
#eval testAnnotatedPython program

I think we should prioritize enabling our Python tests to be written like that.