Port main2 Python fixes to Strata-Python

.github/workflows/cbmc.yml

@@ -68,5 +68,5 @@ jobs:
       - name: Run Python CBMC pipeline tests
         shell: bash
         run: |
-          pip install ./.lake/packages/Strata/Tools/Python-base ./Tools/strata-python
+          pip install ./Tools/Python-base ./Tools/strata-python
           ./StrataPythonTest/run_py_cbmc_tests.sh

.github/workflows/ci.yml

@@ -42,10 +42,10 @@ jobs:
         with:
           python-version: '3.14'
       - name: Build using pip
-        # `strata-base` lives in the Strata package that lake cloned into
-        # `.lake/packages/Strata`; `strata-python` is in this repo.
+        # `strata-base` (Tools/Python-base) and `strata-python` (Tools/strata-python)
+        # both live in this repo.
         run: |
-          pip install ./.lake/packages/Strata/Tools/Python-base
+          pip install ./Tools/Python-base
           pip install ./Tools/strata-python
       - name: Run pyInterpret golden-file tests
         working-directory: StrataPythonTest
@@ -89,7 +89,7 @@ jobs:
         use-restore-keys: "false"
     - name: Build using pip
       run: |
-        pip install ./.lake/packages/Strata/Tools/Python-base
+        pip install ./Tools/Python-base
         pip install ./Tools/strata-python
     - name: Install Lean
       uses: leanprover/lean-action@v1
@@ -157,7 +157,7 @@ jobs:
         use-restore-keys: "false"
     - name: Build using pip
       run: |
-        pip install ./.lake/packages/Strata/Tools/Python-base
+        pip install ./Tools/Python-base
         pip install ./Tools/strata-python
     - name: Install Lean (for lake env)
       uses: leanprover/lean-action@v1

StrataPython/CorePrelude.lean

@@ -7,7 +7,7 @@ module
 
 public import Strata.Languages.Core.Program
 import Strata.Languages.Core.Verifier
-import StrataDDM.Integration.Lean.HashCommands -- shake: keep
+public import StrataDDM.Integration.Lean.HashCommands -- shake: keep
 
 open Strata
 

StrataPython/PythonToCore.lean

@@ -237,7 +237,7 @@ def handleList (_elmts: Array (expr SourceRange)) (expected_type : Lambda.LMonoT
 def PyOptExprToString (e : opt_expr SourceRange) : String :=
   match e with
   | .some_expr _ (.Constant _ (.ConString _ s) _) => s.val
-  | _ => panic! "Expected some constant string: {e}"
+  | _ => panic! s!"Expected some constant string: {repr e}"
 
 partial def PyExprToString (e : expr SourceRange) : String :=
   match e with
@@ -548,7 +548,7 @@ partial def PyExprToCore (translation_ctx : TranslationContext) (e : expr Source
     | .ListComp _ keys values => panic! "ListComp must be handled at stmt level"
     | .UnaryOp _ op arg => match op with
       | .Not _ => {stmts := [], expr := handleNot (PyExprToCore translation_ctx arg).expr}
-      | _ => panic! "Unsupported UnaryOp: {repr e}"
+      | _ => panic! s!"Unsupported UnaryOp: {repr e}"
     | .Subscript sr_sub v slice _ =>
       let sub_md := sourceRangeToMetaData translation_ctx.filePath sr_sub
       let l := PyExprToCore translation_ctx v
@@ -784,7 +784,7 @@ def translateFunctions (a : Array (stmt SourceRange)) (translation_ctx: Translat
                inputs := [],
                outputs := [("maybe_except", (.tcons "ExceptOrNone" []))]},
         spec := default,
-        body := varDecls ++ [.block "end" ((ArrPyStmtToCore translation_ctx body.val).fst) .empty]
+        body := .structured (varDecls ++ [.block "end" ((ArrPyStmtToCore translation_ctx body.val).fst) .empty])
       }
       some (.proc proc .empty)
     | _ => none)
@@ -815,7 +815,7 @@ def pythonFuncToCore (name : String) (args: List (String × String)) (body: Arra
                inputs,
                outputs},
     spec,
-    body
+    body := .structured body
   }
 
 def unpackPyArguments (args: arguments SourceRange) : List (String × String) :=

StrataPython/PythonToLaurel.lean

@@ -1360,7 +1360,7 @@ def extractMultiOutputCalls (ctx : TranslationContext) (e : StmtExprMd)
         return ([], e)
       else
         return (preamble, mkStmtExprMdWithLoc (.StaticCall callee.text newArgs) e.source)
-  | .PrimitiveOp op args =>
+  | .PrimitiveOp op args _ =>
     let results ← args.attach.mapM fun ⟨arg, _⟩ => extractMultiOutputCalls ctx arg
     let preamble := (results.map (fun (pre, _) => pre)).flatten
     let newArgs := results.map (·.2)
@@ -1651,7 +1651,7 @@ partial def getMaybeExceptionExprs (ctx : TranslationContext) (e : StmtExprMd) :
     if isMaybeExceptAnyFunc ctx funcname.text then
       [e]
     else args.flatMap $ getMaybeExceptionExprs ctx
-  | .PrimitiveOp _ args => args.flatMap $ getMaybeExceptionExprs ctx
+  | .PrimitiveOp _ args _ => args.flatMap $ getMaybeExceptionExprs ctx
   | .IfThenElse cond thenBranch elseBranch =>
       ([cond, thenBranch] ++ elseBranch.toList).flatMap $ getMaybeExceptionExprs ctx
   | _ => []
@@ -1677,7 +1677,7 @@ partial def containsUserCall (ctx : TranslationContext) (e : StmtExprMd) : Bool
     callee.text ∈ ctx.userFunctions ||
     withException ctx callee.text ||
     args.any (containsUserCall ctx)
-  | .PrimitiveOp _ args => args.any (containsUserCall ctx)
+  | .PrimitiveOp _ args _ => args.any (containsUserCall ctx)
   | .IfThenElse cond thenBranch elseBranch =>
     containsUserCall ctx cond || containsUserCall ctx thenBranch ||
       elseBranch.any (containsUserCall ctx)
@@ -2074,9 +2074,18 @@ partial def translateStmt (ctx : TranslationContext) (s : stmt SourceRange)
       | _ =>
           mkStmtExprMd $ .PrimitiveOp .Lt [counterExpr,
                           mkStmtExprMd $ .StaticCall "Any_len" [iterExpr]]
-    let bodyStmts := targetDecls ++ assumeStmts ++ bodyStmts ++ [counterIncrease]
-    let innerBlock := mkStmtExprMd (StmtExpr.Block bodyStmts (some continueLabel))
-    let loopStmt := mkStmtExprMdWithLoc (StmtExpr.While counterLtLen [] none innerBlock) md
+    -- The continue-labeled block contains the body but *not* the counter
+    -- increment: `continue` (translated to `exit continueLabel`) must skip
+    -- the rest of the body and fall through to the increment, otherwise the
+    -- loop counter never advances and the loop is non-terminating. Putting
+    -- the increment outside the labeled block also avoids spurious
+    -- "dead code after 'exit'" diagnostics from `break`/`continue` followed
+    -- by `counterIncrease` in the same block.
+    let bodyInner := targetDecls ++ assumeStmts ++ bodyStmts
+    let continueBlock := mkStmtExprMd (StmtExpr.Block bodyInner (some continueLabel))
+    let bodyStmts := [continueBlock, counterIncrease]
+    let whileBody := mkStmtExprMd (StmtExpr.Block bodyStmts none)
+    let loopStmt := mkStmtExprMdWithLoc (StmtExpr.While counterLtLen [] none whileBody) md
     let loopBlock := mkStmtExprMdWithLoc (StmtExpr.Block [loopStmt] (some breakLabel)) md
     let (preamble, _) := getExceptionCheckPreamble ctx iterExpr s!"$for_iter_{iter.toAst.ann.start.byteIdx}"
     return (finalCtx, iterPreamble ++ preamble ++ [counterDecl] ++ [loopBlock])

StrataPythonTest/CorePreludeTest.lean

@@ -18,7 +18,7 @@ Test that the Python CorePrelude can be serialized to Ion format and
 deserialized back without loss of information.
 -/
 private def testCorePreludeRoundTrip : Bool :=
-  let prelude := corePrelude
+  let prelude : Program := corePrelude
   let bytes := prelude.toIon
   match Program.fromIon Strata.Core_map Strata.Core.name bytes with
   | .ok pgm => pgm.commands.size == prelude.commands.size

StrataPythonTest/PySpecArgTypeTest.lean

@@ -106,7 +106,12 @@ preconditions redundant. -/
 info: procedure test_typed_func(x: Any, y: Any): Any
   opaque
   modifies *
-{ result := <??>; assert Any..isfrom_int(x); assert Any..isfrom_str(y); assume Any..isfrom_float(result) };
+{
+  result := <??>;
+  assert Any..isfrom_int(x);
+  assert Any..isfrom_str(y);
+  assume Any..isfrom_float(result)
+};
 -/
 #guard_msgs in
 #eval! do

StrataPythonTest/expected_laurel/test_bug_finding_unreachable.expected

@@ -1,7 +1,7 @@
 test_bug_finding_unreachable.py(3, 4): ✖️ always false if reached - impossible condition
 test_bug_finding_unreachable.py(4, 7): ✔️ always true if reached - Check PGt exception
 test_bug_finding_unreachable.py(5, 11): ✔️ always true if reached - Check PLt exception
-test_bug_finding_unreachable.py(6, 12): ❌ fail (❗path unreachable) - dead code
+test_bug_finding_unreachable.py(6, 12): ❌ fail (❗unreachable in this context) - dead code
 test_bug_finding_unreachable.py(2, 44): ✔️ always true if reached - (test_bug_finding_unreachable ensures) Return type constraint
 DETAIL: 3 passed, 2 failed, 0 inconclusive, 1 unreachable
 RESULT: Failures found

StrataPythonTest/expected_laurel/test_for_continue_advance.expected

@@ -0,0 +1,6 @@
+test_for_continue_advance.py(3, 4): ✅ pass - assert(72)
+test_for_continue_advance.py(4, 4): ✅ pass - assume_assume(87)_calls_PIn_0
+test_for_continue_advance.py(1, 35): ✅ pass - (test_for_continue_advance ensures) Return type constraint
+test_for_continue_advance.py(7, 12): ❓ unknown - Check PAdd exception
+DETAIL: 3 passed, 0 failed, 1 inconclusive
+RESULT: Inconclusive

StrataPythonTest/tests/test_for_continue_advance.py

@@ -0,0 +1,9 @@
+def test_for_continue_advance() -> None:
+    items: Any = [1, 2, 3]
+    s: int = 0
+    for x in items:
+        if x == 2:
+            continue
+        s = s + x
+
+test_for_continue_advance()

Tools/Python-base/.gitignore

@@ -0,0 +1 @@
+__pycache__

Tools/Python-base/pyproject.toml

@@ -0,0 +1,15 @@
+[project]
+name = "strata"
+version = "0.0.1"
+description = "Core Strata DDM datatypes and Ion serialization."
+requires-python = ">= 3.11"
+dependencies = [
+    "amazon.ion"
+]
+
+[tool.hatch.build.targets.wheel]
+packages = ["strata"]
+
+[build-system]
+requires = ["hatchling"]
+build-backend = "hatchling.build"