Add optional tz parameter to datetime_now and reject extra positional args (#725)

### Problem

`datetime.now(timezone.utc)` caused an arity mismatch because the
prelude's `datetime_now` declared 0 parameters while the Python call
passed 1 argument. This surfaced as a "call [end_time] :=
datetime_now($hole_12($heap_in))" error in check_storage_costs.

### Approach

Rather than silently dropping extra positional arguments (which could
mask real bugs), we model the missing optional parameter in the prelude
and add an arity check that rejects extra positional arguments for all
functions.

**Prelude changes:**
- Add `tz: Any` parameter to `datetime_now` in the Laurel prelude
- Add `tz: AnyOrNone` parameter to `datetime_now` in the Core prelude
and FunctionSignatures

**Arity checking:**
`combinePositionalAndKeywordArgs` now raises a user error when a call
passes more positional arguments than the function signature declares,
for both user-defined and prelude functions alike

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

---------

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Author: tautschnig

Strata/Languages/Python/CorePrelude.lean

@@ -217,7 +217,7 @@ function Datetime_get_timedelta(d : Datetime) : int;
 // means subtracting an 'old' timestamp from a 'new' timestamp may return
 // a negative difference.
 
-procedure datetime_now() returns (d:Datetime, maybe_except: ExceptOrNone)
+procedure datetime_now(tz: AnyOrNone) returns (d:Datetime, maybe_except: ExceptOrNone)
 spec {
   ensures (Datetime_get_timedelta(d) == Timedelta_mk(0,0,0));
 }

Strata/Languages/Python/FunctionSignatures.lean

@@ -136,7 +136,7 @@ def addCoreDecls : SignatureM Unit := do
   decl "json_loads" [msg :< string]
   decl "input" [msg :< string]
   decl "random_choice" [l :< ListStr]
-  decl "datetime_now" []
+  decl "datetime_now" [tz :< AnyOrNone]
   decl "datetime_utcnow" []
   decl "datetime_date" [dt :< Datetime]
   decl "timedelta" [ days :< IntOrNone, hours :< IntOrNone]

Strata/Languages/Python/PythonRuntimeLaurelPart.lean

@@ -937,7 +937,7 @@ procedure datetime_date(d: Any) returns (ret: Any, error: Error)
   }
 };
 
-procedure datetime_now() returns (ret: Any)
+procedure datetime_now(tz: Any) returns (ret: Any)
   ensures Any..isfrom_datetime(ret) summary "ret_type"
 {
   var d: int;

Strata/Languages/Python/PythonToLaurel.lean

@@ -839,6 +839,10 @@ partial def combinePositionalAndKeywordArgs
       throwUserError callRange
         s!"'{name}' called with unknown keyword arguments: {extraNames}"
     let kwords := pyKwordsToHashMap kwords
+    -- Extra positional args beyond the signature are an arity error.
+    if posArgs.length > funcDecl.args.length then
+      throwUserError callRange
+        s!"'{name}' called with too many positional arguments: expected at most {funcDecl.args.length}, got {posArgs.length}"
     let unprovidedPosArgs := funcDecl.args.drop posArgs.length
     --every unprovided positional args must have a default value in the function signature or be provided in the kwargs
     let missingArgs := unprovidedPosArgs.filter fun arg =>
@@ -926,6 +930,10 @@ partial def translateCall (ctx : TranslationContext)
   -- expand the dictionary into individual arguments using DictStrAny_get
   if isVarKwargs kwords && funcDecl.isSome then
     let funcDecl := funcDecl.get!
+    let name := if methodName.isEmpty then funcDecl.name else methodName
+    if args.length > funcDecl.args.length then
+      throwUserError callRange
+        s!"'{name}' called with too many positional arguments: expected at most {funcDecl.args.length}, got {args.length}"
     let trans_posArgs ← args.mapM (translateExpr ctx)
     let trans_dict ← translateVarKwargs ctx kwords
     let remainingParams := funcDecl.args.drop args.length

StrataTest/Languages/Python/PreludeVerifyTest.lean

@@ -158,15 +158,15 @@ Obligation: postcondition
 Property: assert
 Result: ✅ pass
 
-Obligation: assert(41763)
+Obligation: assert(41770)
 Property: assert
 Result: ✅ pass
 
-Obligation: assert(41830)
+Obligation: assert(41837)
 Property: assert
 Result: ✅ pass
 
-Obligation: assert(41938)
+Obligation: assert(41945)
 Property: assert
 Result: ✅ pass
 

StrataTest/Languages/Python/VerifyPythonTest.lean

@@ -17,7 +17,7 @@ Python → Laurel → Core → SMT pipeline and produces diagnostics.
 namespace Strata.Python.VerifyPythonTest
 
 open StrataTest.Util
-open Strata.Python (processPythonFile withPython)
+open Strata.Python (processPythonFile withPython containsSubstr)
 open Strata.Parser (stringInputContext)
 
 -- Passing assertions produce no diagnostics.
@@ -130,16 +130,16 @@ open Strata.Parser (stringInputContext)
   if diags.size ≠ 0 then
     throw <| .userError s!"Expected 0 diagnostics, got {diags.size}"
 
--- Multi-output prelude procedures: timedelta_func returns (delta: Any, maybe_except: Error).
--- This tests that withException detects the multi-output signature and generates
--- a 2-target assignment, and that computeExprType returns Unknown (→ Any in Core).
+-- datetime.now() with optional tz parameter and timedelta arithmetic.
+-- Also exercises multi-output prelude procedure detection (timedelta_func
+-- returns (delta: Any, maybe_except: Error)).
 #guard_msgs in
 #eval withPython (warnOnSkip := false) fun pythonCmd => do
   let program :=
 "from datetime import datetime, timedelta
 
 def main() -> None:
-    now: datetime = datetime.now()
+    now: datetime = datetime.now(None)
     delta: timedelta = timedelta(days=7)
     start: datetime = now - delta
     assert start <= now
@@ -148,6 +148,43 @@ def main() -> None:
   if diags.size ≠ 0 then
     throw <| .userError s!"Expected 0 diagnostics, got {diags.size}: {diags.map (·.message)}"
 
+-- Calling a user-defined function with too many positional args should error.
+#guard_msgs in
+#eval withPython (warnOnSkip := false) fun pythonCmd => do
+  let program :=
+"def greet(name: str) -> str:
+    return name
+
+def main() -> None:
+    x: str = greet(\"alice\", \"extra\")
+"
+  try
+    let _ ← processPythonFile pythonCmd (stringInputContext "test.py" program)
+    throw <| IO.userError "Expected pipeline error for too many positional arguments"
+  catch e =>
+    let msg := toString e
+    unless containsSubstr msg "too many positional arguments" do
+      throw <| IO.userError s!"Expected 'too many positional arguments' error, got: {msg}"
+
+-- Extra positional args with **kwargs expansion should also error.
+#guard_msgs in
+#eval withPython (warnOnSkip := false) fun pythonCmd => do
+  let program :=
+"def greet(name: str) -> str:
+    return name
+
+def main() -> None:
+    d: dict = {}
+    x: str = greet(\"alice\", \"extra\", **d)
+"
+  try
+    let _ ← processPythonFile pythonCmd (stringInputContext "test.py" program)
+    throw <| IO.userError "Expected pipeline error for too many positional arguments"
+  catch e =>
+    let msg := toString e
+    unless containsSubstr msg "too many positional arguments" do
+      throw <| IO.userError s!"Expected 'too many positional arguments' error, got: {msg}"
+
 -- Returning a Composite-typed value from a function with Any return type
 -- should not crash; the Composite is replaced with a Hole (unconstrained value).
 #guard_msgs in

StrataTest/Languages/Python/tests/cbmc_expected.txt

@@ -31,5 +31,6 @@ test_class_with_methods.py.ion  SKIP
 test_module_level.py.ion        SKIP
 test_if_elif.py.ion             SKIP
 test_variable_reassign.py.ion   SKIP
+test_datetime_now_tz.py.ion     SKIP
 test_timedelta_expr.py.ion      SKIP
 test_composite_return.py.ion    PASS

StrataTest/Languages/Python/tests/test_datetime_now_tz.py

@@ -0,0 +1,6 @@
+from datetime import datetime, timezone, timedelta
+
+now: datetime = datetime.now(timezone.utc)
+delta: timedelta = timedelta(days=7)
+start: datetime = now - delta
+assert start <= now