Add optional tz parameter to datetime_now and reject extra positional args

[tautschnig]

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.

[Copilot]

Pull request overview

This PR adjusts the Python→Laurel translator to avoid arity mismatches when Python call sites pass more positional arguments than a modeled/prelude Laurel signature declares (e.g., datetime.now(timezone.utc) when the model declares 0 params), and adds a regression test for that scenario.

Changes:

• Truncate positional arguments to the modeled signature length during argument combination in PythonToLaurel.
• Add a new Python pipeline test covering datetime.now(timezone.utc) and basic datetime arithmetic.
• Register the new test in the Python CBMC expected-outcomes list as PASS.

Reviewed changes

Copilot reviewed 3 out of 3 changed files in this pull request and generated 1 comment.

File	Description
Strata/Languages/Python/PythonToLaurel.lean	Truncates extra positional args during call argument processing to prevent Laurel arity mismatch.
StrataTest/Languages/Python/tests/test_datetime_now_tz.py	Adds regression test exercising datetime.now(timezone.utc) and timedelta arithmetic.
StrataTest/Languages/Python/tests/cbmc_expected.txt	Marks the new test as expected PASS in the CBMC pipeline runner.

---

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

[olivier-aws]

I'm surprised this is sound in general. Another solution would be to modify our Prelude functions to have the optional argument, and add "holes" when one argument is missing. Any reason why we shouldn't use this approach?

[tautschnig]

I'm surprised this is sound in general. Another solution would be to modify our Prelude functions to have the optional argument, and add "holes" when one argument is missing. Any reason why we shouldn't use this approach?

That's a great point that we are using a different approach elsewhere. I have now adopted that approach here as well.