Add type constraint preconditions/postcondition for function inputs/output

[thanhnguyen-aws]

Description of changes:
This PR adds type constraint pre-conditions for function inputs to ensure consistency with the original Python code. Currently, all function inputs are translated to Any type, which loses type information during translation.

Changes

• Add type constraint assertions for function input parameters at the beginning of the function's body.

• Add pre-conditions based on declared input types.

• Add post-conditions based on declared out types, we also translate Python function into Opaque procedures to accommodate this.

• Support Python's type union operator (|) for type constraints.

Limitation:

• This PR does not add type constraint for class methods. An upcoming separate PR will unify functions translation with class's methods translation.

• This PR does not add postcondition when the function return None.

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

[shigoel]

@thanhnguyen-aws Could you please resolve merge conflicts?

[keyboardDrummer]

Have you considered using the constrained types feature from Laurel that @fabiomadge merged recently? It means that instead of generating preconditions you'd generate constrained types and reference these in the function parameters.

Currently that implementation also generates preconditions like this one does, but when using constrained types there is the potential to have more checking be done statically through the type system, for example when you pass a variable to a function that already has the same constrained type.

@andrewmwells-amazon thoughts?

[thanhnguyen-aws]

Currently that implementation also generates preconditions like this one does, but when using constrained types there is the potential to have more checking be done statically through the type system, for example when you pass a variable to a function that already has the same constrained type.

I don't think it is convenient using that feature for this PR because for each union of types, we need to define a constrained type for it.

[thanhnguyen-aws]

@thanhnguyen-aws Could you please resolve merge conflicts?

I resolved the conflict.

[keyboardDrummer]

Currently that implementation also generates preconditions like this one does, but when using constrained types there is the potential to have more checking be done statically through the type system, for example when you pass a variable to a function that already has the same constrained type.

I don't think it is convenient using that feature for this PR because for each union of types, we need to define a constrained type for it.

Indeed you would need a unique constrained type for each union. I don't think that's necessarily as issue, but if the constrained type is only referenced once then it's rather pointless to generate it. I think it's usefulness depends on what type of Python programs we receive.

[keyboardDrummer]

Left a few small comments, but otherwise seems good to me. I would appreciate the second reviewer having more context on the PythonToLaurel code.

[aqjune-aws]

It seems there is a merge conflict, and it could possibly be related to Joe's patch. Do you want to resolve the merge conflict?

[MikaelMayer]

Overall this is a solid PR that adds type constraint preconditions/postconditions for function inputs/outputs. The approach of generating Any..isfrom_* checks as preconditions and postconditions is clean. A few issues found below, one of which is a likely bug.

[tautschnig]

1. Merge conflicts with main — unrelated regressions. The branch is 2 commits behind main and the last merge (cfaa896) introduced regressions in unrelated files:

• Strata/DDM/Integration/Lean/Gen.lean reverts the resolveScopedName extraction from PR #728
• StrataTest/DDM/Integration/Lean/Gen.lean deletes the duplicate-name test from PR #728
• Strata/Languages/Laurel/ModifiesClauses.lean deletes filterNonCompositeModifies (fix for issue #490)
• Strata/Languages/Laurel/LaurelTypes.lean deletes classifyModifiesHighType and isHeapRelevantType
• StrataTest/Languages/Laurel/Examples/Objects/T8_NonCompositeModifies.lean deletes the regression test for #490

The branch needs to be re-merged with current main, carefully preserving the changes from PRs #728 and the modifies-clause fix.

2. Constructor renames are a breaking change for pyspecs. Renaming from_none → from_None, from_string → from_str, from_Dict → from_DictStrAny, Some → OptSome, None → OptNone in the runtime will break any existing pyspec files that reference the old names. This should be called out in the PR description and coordinated with pyspec consumers.

3. All functions now return Any (even void functions). Previously, functions without return type annotations had no output parameters. Now all functions get outputs := [{ name := PyLauFuncReturnVar, type := AnyTy }] and a from_None default return at the top of the body. This changes the verification semantics — callers of void functions will now see a return value. Is this intentional?

[tautschnig]

Re-review after the latest merge (6e79200). The merge regressions I flagged in my previous review are now fixed — PR #728 (Gen.lean) and PR #731 (modifies clause fix) are properly included.

The only potential concern left: Constructor renames are a breaking change for pyspecs — Still applies. from_none → from_None, from_string → from_str, from_Dict → from_DictStrAny, Some → OptSome, None → OptNone. Any existing pyspec files referencing old names will break.