Propagate Python assert messages as Laurel property summaries

.github/workflows/cbmc.yml

@@ -102,6 +102,10 @@ jobs:
         run: |
           pip install ./Tools/Python
           ./StrataTest/Languages/Python/run_py_cbmc_tests.sh
+      - name: Run property summary tests
+        shell: bash
+        run: |
+          ./StrataTest/Backends/CBMC/GOTO/test_property_summary_e2e.sh
       - name: Run Laurel CBMC pipeline tests
         shell: bash
         run: |

Strata/Languages/Python/PythonToLaurel.lean

@@ -971,8 +971,12 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang
     return (ctx, [retStmt])
 
   -- Assert statement
-  | .Assert _ test _msg => do
+  | .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
@@ -984,7 +988,7 @@ 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 (Any_to_bool finalCondExpr)) md
+    let assertStmt := mkStmtExprMdWithLoc (StmtExpr.Assert (Any_to_bool finalCondExpr)) md'
 
     -- Wrap in block if we hoisted condition
     let result := if condStmts.isEmpty then

StrataTest/Backends/CBMC/GOTO/test_property_summary_e2e.sh

@@ -0,0 +1,109 @@
+#!/bin/bash
+# E2E test: property summary metadata flows from Laurel through GOTO to CBMC output.
+#
+# Verifies that Laurel `assert ... summary "..."` annotations appear in
+# CBMC's verification output as property descriptions.
+
+set -eo pipefail
+
+SCRIPT_DIR="$(cd "$(dirname "$0")" && pwd)"
+PROJECT_ROOT="$(cd "$SCRIPT_DIR/../../../.." && pwd)"
+STRATA="$PROJECT_ROOT/.lake/build/bin/strata"
+CBMC=${CBMC:-cbmc}
+SYMTAB2GB=${SYMTAB2GB:-symtab2gb}
+
+WORK=$(mktemp -d)
+trap 'rm -rf "$WORK"' EXIT
+
+# Step 1: Create Laurel program with property summaries
+cat > "$WORK/test.lr.st" << 'LAUREL'
+procedure main() {
+    var x: int := 5;
+    var y: int := 3;
+    assert x + y == 8 summary "addition equals eight";
+    assert x - y == 2 summary "difference equals two"
+};
+LAUREL
+
+# Step 2: Translate to GOTO
+cd "$WORK"
+"$STRATA" laurelAnalyzeToGoto test.lr.st 2>&1 | grep -q "Written"
+
+# Step 3: Verify GOTO JSON contains property summaries
+python3 -c "
+import json, sys
+with open('test.lr.goto.json') as f:
+    data = json.load(f)
+summaries = []
+for fn in data['functions']:
+    for inst in fn['instructions']:
+        if inst.get('instructionId') == 'ASSERT':
+            summaries.append(inst.get('sourceLocation', {}).get('comment', ''))
+assert 'addition equals eight' in summaries, f'Missing summary in GOTO JSON: {summaries}'
+assert 'difference equals two' in summaries, f'Missing summary in GOTO JSON: {summaries}'
+print('GOTO JSON: property summaries present')
+"
+
+# Step 4: Wrap symtab and add CBMC default symbols
+python3 -c "
+import json
+with open('test.lr.symtab.json') as f:
+    data = json.load(f)
+# Add minimal __CPROVER_initialize symbol required by CBMC
+data['__CPROVER_initialize'] = {
+    'baseName': '__CPROVER_initialize',
+    'mode': 'C',
+    'module': '',
+    'name': '__CPROVER_initialize',
+    'prettyName': '__CPROVER_initialize',
+    'type': {'id': 'code', 'namedSub': {'parameters': {'sub': []}, 'return_type': {'id': 'empty'}}},
+    'value': {'id': 'nil'}
+}
+data['__CPROVER_rounding_mode'] = {
+    'baseName': '__CPROVER_rounding_mode',
+    'isLvalue': True,
+    'isStaticLifetime': True,
+    'isStateVar': True,
+    'mode': 'C',
+    'module': '',
+    'name': '__CPROVER_rounding_mode',
+    'prettyName': '__CPROVER_rounding_mode',
+    'type': {'id': 'signedbv', 'namedSub': {'width': {'id': '32'}}},
+    'value': {'id': 'nil'}
+}
+with open('wrapped.symtab.json', 'w') as f:
+    json.dump({'symbolTable': data}, f)
+"
+
+# Step 5: Convert to GOTO binary and run CBMC
+"$SYMTAB2GB" wrapped.symtab.json --goto-functions test.lr.goto.json --out test.gb 2>/dev/null
+
+cbmc_out=$("$CBMC" test.gb --z3 --no-pointer-check --function main 2>&1 || true)
+
+# Step 6: Verify CBMC output contains property summaries
+if echo "$cbmc_out" | grep -q "addition equals eight"; then
+  echo "CBMC output: 'addition equals eight' found"
+else
+  echo "FAIL: 'addition equals eight' not in CBMC output"
+  echo "$cbmc_out"
+  exit 1
+fi
+
+if echo "$cbmc_out" | grep -q "difference equals two"; then
+  echo "CBMC output: 'difference equals two' found"
+else
+  echo "FAIL: 'difference equals two' not in CBMC output"
+  echo "$cbmc_out"
+  exit 1
+fi
+
+# Step 7: Verify CBMC says SUCCESSFUL
+if echo "$cbmc_out" | grep -q "VERIFICATION SUCCESSFUL"; then
+  echo "CBMC: VERIFICATION SUCCESSFUL"
+else
+  echo "FAIL: CBMC did not report VERIFICATION SUCCESSFUL"
+  echo "$cbmc_out"
+  exit 1
+fi
+
+echo "PASS: property summaries flow end-to-end from Laurel to CBMC"

StrataTest/Languages/Python/PropertySummaryTest.lean

@@ -0,0 +1,72 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+
+module
+
+meta import Strata.SimpleAPI
+meta import StrataTest.Util.Python
+
+/-! ## Test: Python assert messages propagate as property summaries
+
+Verifies that `assert cond, "message"` in Python flows through as a
+property summary in the Core verification results.
+-/
+
+namespace Strata.Python.PropertySummaryTest
+
+open Strata (pyTranslateLaurel verifyCore)
+
+private meta def testPy : String :=
+"def main(x: int) -> None:
+    assert x == x, \"reflexivity\"
+    assert x + 0 == x, \"additive identity\"
+"
+
+/-- Compile a Python string to Ion, translate to Core, verify, and return
+    the property summaries from the VCResults. -/
+private meta def getPropertySummaries (pythonCmd : System.FilePath) : IO (Array String) := do
+  IO.FS.withTempDir fun tmpDir => do
+    -- Write Python source
+    let pyFile := tmpDir / "test.py"
+    IO.FS.writeFile pyFile testPy
+    -- Write dialect file
+    let dialectFile := tmpDir / "dialect.ion"
+    IO.FS.writeBinFile dialectFile Python.Python.toIon
+    -- Compile to Ion
+    let ionFile := tmpDir / "test.python.st.ion"
+    let child ← IO.Process.spawn {
+      cmd := pythonCmd.toString
+      args := #["-m", "strata.gen", "py_to_strata",
+                "--dialect", dialectFile.toString,
+                pyFile.toString, ionFile.toString]
+      inheritEnv := true
+      stdin := .null, stdout := .piped, stderr := .piped
+    }
+    let stderr ← child.stderr.readToEnd
+    let exitCode ← child.wait
+    if exitCode ≠ 0 then
+      throw <| .userError s!"py_to_strata failed: {stderr}"
+    -- Translate to Core
+    let core ← match ← pyTranslateLaurel ionFile.toString |>.toBaseIO with
+      | .ok r => pure r
+      | .error msg => throw <| .userError s!"pyTranslateLaurel failed: {msg}"
+    -- Verify
+    let results ← match ← verifyCore core Core.VerifyOptions.quiet |>.toBaseIO with
+      | .ok r => pure r
+      | .error msg => throw <| .userError s!"verifyCore failed: {msg}"
+    -- Extract property summaries
+    return results.filterMap fun vcr =>
+      vcr.obligation.metadata.getPropertySummary
+
+#eval withPython fun pythonCmd => do
+  let summaries ← getPropertySummaries pythonCmd
+  let expected := #["reflexivity", "additive identity"]
+  for msg in expected do
+    unless summaries.any (· == msg) do
+      throw <| .userError s!"FAIL: \"{msg}\" not found in summaries: {summaries}"
+  IO.println "PASS: Python assert messages propagate as property summaries"
+
+end Strata.Python.PropertySummaryTest