fix: add missing opt parameter to Laurel print declaration (#971)

PR requested and agreed on by @olivier-aws 

## Summary

The Laurel `print` procedure declaration in
`PythonRuntimeLaurelPart.lean` was missing the `opt` parameter that
models Python's variadic `*objects`. Without it, a call like `print("a",
"b")` would be handled differently in the Laurel path vs the Core path,
since positional arguments would shift.

## Changes

1. **`Strata/Languages/Python/PythonRuntimeLaurelPart.lean`** — Added
`opt : Any` parameter to the `print` declaration, matching the Core
declaration's parameter list:
   ```
   // Before
procedure print(msg : Any, sep : Any, end : Any, file : Any, flush :
Any) returns ();
   // After
procedure print(msg : Any, opt : Any, sep : Any, end : Any, file : Any,
flush : Any) returns ();
   ```

2. **`StrataTest/Languages/Python/VerifyPythonTest.lean`** — Added a
test exercising `print` with multiple positional arguments (`print()`,
`print("a")`, `print("a", "b")`, `print("a", "b", "c")`) and
combinations with keyword arguments (`sep`, `end`, `flush`).

Per @olivier-aws's guidance, the parameter types are kept as `Any` (not
changed to match Core's `StrOrNone`/`BoolOrNone`/`AnyOrNone`).

Both the source and test files build successfully with `lake build`.

Fixes #941

---------

Co-authored-by: keyboardDrummer-bot <keyboardDrummer-bot@users.noreply.github.com>
Co-authored-by: Shilpi Goel <shigoel@gmail.com>
Co-authored-by: Fabio Madge <fmadge@amazon.com>

Author: 3 people

Strata/Languages/Python/PythonRuntimeLaurelPart.lean

@@ -1073,7 +1073,7 @@ procedure test_helper_procedure(req_name : Any, opt_name : Any) returns (ret: An
   assume (Error..isNoError(maybe_except)) // summary "assume_maybe_except_none"
 };
 
-procedure print(msg : Any, sep : Any, end : Any, file : Any, flush : Any) returns ();
+procedure print(msg : Any, opt : Any, sep : Any, end : Any, file : Any, flush : Any) returns ();
 
 #end
 

StrataTest/Languages/Python/VerifyPythonTest.lean

@@ -505,6 +505,22 @@ def test() -> None:
   if diags.size ≠ 0 then
     throw <| .userError s!"Expected 0 diagnostics, got {diags.size}: {diags.map (·.message)}"
 
+-- print() with multiple positional arguments exercises the opt parameter.
+#guard_msgs in
+#eval withPython (warnOnSkip := false) fun pythonCmd => do
+  let program :=
+"def main() -> None:
+    print()
+    print(\"a\")
+    print(\"a\", \"b\")
+    print(\"a\", \"b\", \"c\")
+    print(\"a\", \"b\", sep=\",\", end=\"\\n\", flush=True)
+    print(\"x\", \"y\", \"z\", sep=\" \")
+"
+  let diags ← processPythonFile pythonCmd (stringInputContext "test.py" program)
+  if diags.size ≠ 0 then
+    throw <| .userError s!"Expected 0 diagnostics, got {diags.size}: {diags.map (·.message)}"
+
 -- PreludeInfo.ofLaurelProgram should strip the $in_ prefix from parameter
 -- names so that cross-module keyword argument calls use the original names.
 #guard_msgs in

StrataTest/Languages/Python/expected_laurel/test_class_decl.expected

@@ -1,4 +1,4 @@
-test_class_decl.py(9, 4): ✅ pass - callElimAssert_requires_13
+test_class_decl.py(9, 4): ✅ pass - callElimAssert_requires_15
 test_class_decl.py(8, 0): ✅ pass - postcondition
 test_class_decl.py(13, 0): ✅ pass - ite_cond_calls_Any_to_bool_0
 DETAIL: 3 passed, 0 failed, 0 inconclusive