From 6b3c7f33eb41b18b16b76921d079e2ad89bc59ed Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Fri, 13 Mar 2026 12:27:13 -0700 Subject: [PATCH 01/31] add type constraint assertion and preconds for function inputs --- Strata/Languages/Python/PythonToLaurel.lean | 106 +++++++++++++----- StrataMain.lean | 5 +- .../test_func_input_type_constraints.expected | 41 +++++++ .../test_function_def_calls.expected | 2 + .../tests/test_func_input_type_constraints.py | 10 ++ 5 files changed, 138 insertions(+), 26 deletions(-) create mode 100644 StrataTest/Languages/Python/expected_laurel/test_func_input_type_constraints.expected create mode 100644 StrataTest/Languages/Python/tests/test_func_input_type_constraints.py diff --git a/Strata/Languages/Python/PythonToLaurel.lean b/Strata/Languages/Python/PythonToLaurel.lean index 8a3848421..06ab0cd49 100644 --- a/Strata/Languages/Python/PythonToLaurel.lean +++ b/Strata/Languages/Python/PythonToLaurel.lean @@ -62,7 +62,7 @@ deriving Inhabited structure PythonFunctionDecl where name : String --args include name, type, default value - args : List (String × String × Option (Python.expr SourceRange)) + args : List (String × MetaData × List String × Option (Python.expr SourceRange)) hasKwargs: Bool ret : Option String deriving Repr, Inhabited @@ -170,10 +170,11 @@ partial def getSubscriptBaseName (e : Python.expr SourceRange) : String := | .Subscript _ val _ _ => getSubscriptBaseName val | _ => pyExprToString e +def PyLauType.None := "None" def PyLauType.Int := "int" def PyLauType.Bool := "bool" def PyLauType.Str := "str" -def PyLauType.Datetime := "Datetime" +def PyLauType.Datetime := "datetime" def PyLauType.DictStrAny := "DictStrAny" def PyLauType.ListStr := "ListStr" def PyLauType.Package := "Package" @@ -496,6 +497,7 @@ partial def inferExprType (ctx : TranslationContext) (e: Python.expr SourceRange | .Constant _ (.ConFalse _) _ | .BoolOp _ _ _ | .Compare _ _ _ _=> return PyLauType.Bool + | .Constant _ (.ConNone _) _ => return PyLauType.None -- Variable references | .Name _ n _ => match ctx.variableTypes.find? (λ v => v.fst == n.val) with @@ -617,10 +619,10 @@ partial def combinePositionalAndKeywordArgs let kwords := pyKwordsToHashMap kwords 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 check_args := (unprovidedPosArgs.map (λ (name, _, default) => (name ∈ kwords.keys) || default.isSome)).all (fun a => a) + let check_args := (unprovidedPosArgs.map (λ (name,_, _,default) => (name ∈ kwords.keys) || default.isSome)).all (fun a => a) let filledPosArgs ← if check_args then - unprovidedPosArgs.mapM (λ (name, _, default) => + unprovidedPosArgs.mapM (λ (name, _, _,default) => match kwords.get? name with | some expr => return expr | none => match default with @@ -683,8 +685,9 @@ def withException (ctx : TranslationContext) (funcname: String) : Bool := | some sig => sig.outputs.length > 0 && sig.outputs.getLast! == "Error" | _ => false -def maybeExceptVar := mkStmtExprMd (.Identifier "maybe_except") -def nullcall_var := mkStmtExprMd (.Identifier "nullcall_ret") +def freeVar (name: String) := mkStmtExprMd (.Identifier name) +def maybeExceptVar := freeVar "maybe_except" +def nullcall_var := freeVar "nullcall_ret" partial def translateAssign (ctx : TranslationContext) (lhs: Python.expr SourceRange) @@ -987,24 +990,33 @@ partial def getNestedSubscripts (expr: Python.expr SourceRange) : List ( Python | .Subscript _ val slice _ => [val] ++ (getNestedSubscripts slice) | _ => [expr] -partial def argumentTypeToString (arg: Python.expr SourceRange) : Except TranslationError String := +def getUnionTypes (arg: Python.expr SourceRange) : List (Python.expr SourceRange) := match arg with - | .Name _ n _ => return n.val + | .BinOp _ left _ right => getUnionTypes left ++ getUnionTypes right + | _ => [arg] + +partial def argumentTypeToString (arg: Python.expr SourceRange) : Except TranslationError (List String) := + match arg with + | .Name _ n _ => return [n.val] | .Subscript _ _ _ _ => let subscript_list:= getNestedSubscripts arg let subscript_head := subscript_list[0]! let slice_head := subscript_list[1]! let v_name := pyExprToString subscript_head match v_name with - | "Optional" => return "NoneOr" ++ pyExprToString slice_head - | _ => return v_name - | .Constant _ _ _ => return "None" - | .Attribute _ _ _ _ => return pyExprToString arg + | "Optional" => return [pyExprToString slice_head, "None"] + | "Union" => match slice_head with + | .Tuple _ tys _ => return (← tys.val.toList.mapM argumentTypeToString).flatten + | _ => throw (.internalError s!"Unhandled Expr: {repr arg}") + | _ => return [v_name] + | .Constant _ _ _ => return ["None"] + | .Attribute _ _ _ _ => return [pyExprToString arg] + | .BinOp _ _ _ _ => return (← (getUnionTypes arg).mapM argumentTypeToString).flatten | _ => throw (.internalError s!"Unhandled Expr: {repr arg}") --The return is a List (inputname, type, default value) and a bool indicating if the function has Kwargs input -def unpackPyArguments (args: Python.arguments SourceRange) - : Except TranslationError ((List (String × String × Option (Python.expr SourceRange))) × Bool):= do +def unpackPyArguments (ctx : TranslationContext) (args: Python.arguments SourceRange) + : Except TranslationError ((List (String × MetaData × List String × Option (Python.expr SourceRange))) × Bool):= do match args with | .mk_arguments _ _ args _ _ _ kwargs defaults => let argscount := args.val.size @@ -1015,17 +1027,22 @@ def unpackPyArguments (args: Python.arguments SourceRange) let argtypes ← argsinfo.mapM (λ a: Python.arg SourceRange × Option (Python.expr SourceRange) => match a.fst with - | .mk_arg _ name oty _ => + | .mk_arg sr name oty _ => + let md := sourceRangeToMetaData ctx.filePath sr match oty.val with - | .some ty => return (name.val, ← argumentTypeToString ty, a.snd) - | _ => return (name.val, PyLauType.Any, a.snd)) + | .some ty => + let defaultType := match a.snd.mapM (inferExprType ctx) with + | .ok (some ty) => [ty] + | _ => [] + return (name.val, md, (← argumentTypeToString ty) ++ defaultType, a.snd) + | _ => return (name.val, md, [PyLauType.Any], a.snd)) return (argtypes, kwargs.val.isSome) def pyFuncDefToPythonFunctionDecl (ctx : TranslationContext) (f : Python.stmt SourceRange) : Except TranslationError PythonFunctionDecl := do match f with | .FunctionDef _ name args _body _decorator_list returns _type_comment _ => let name := match ctx.currentClassName with | none => name.val | some classname => classname ++ "_" ++ name.val - let args_trans ← unpackPyArguments args + let args_trans ← unpackPyArguments ctx args let args := if name.endsWith "@__init__" then args_trans.fst.tail else args_trans.fst let ret := if name.endsWith "@__init__" then some (name.dropEnd "@__init__".length).toString else @@ -1041,6 +1058,42 @@ def pyFuncDefToPythonFunctionDecl (ctx : TranslationContext) (f : Python.stmt S } | _ => throw (.internalError "Expected FunctionDef") +def getSingleTypeConstraint (var: String) (ty: String): Option StmtExprMd := + match ty with + | "str" => mkStmtExprMd (.StaticCall "Any..isfrom_string" [freeVar var]) + | "int" => mkStmtExprMd (.StaticCall "Any..isfrom_int" [freeVar var]) + | "bool" => mkStmtExprMd (.StaticCall "Any..isfrom_bool" [freeVar var]) + | "datetime" => mkStmtExprMd (.StaticCall "Any..isfrom_datetime" [freeVar var]) + | "None" => mkStmtExprMd (.StaticCall "Any..isfrom_none" [freeVar var]) + | _ => if ty.startsWith "Dict" then mkStmtExprMd (.StaticCall "Any..isfrom_Dict" [freeVar var]) + else if ty.startsWith "List" then mkStmtExprMd (.StaticCall "Any..isfrom_ListAny" [freeVar var]) + else none + +def creatBoolOrExpr (exprs: List StmtExprMd) : StmtExprMd := + match exprs with + | [] => mkStmtExprMd (.LiteralBool true) + | [expr] => expr + | expr::exprs => mkStmtExprMd (.StaticCall "Bool.Or" [expr, creatBoolOrExpr exprs]) + +def getUnionTypeConstraint (var: String) (md: MetaData) (tys: List String) (funcname: String): Option StmtExprMd := + let type_constraints := tys.filterMap (getSingleTypeConstraint var) + if type_constraints.isEmpty then none else + let md: MetaData := md.withPropertySummary ("(" ++ funcname ++ " requires) Type constraint of " ++ var) + some {creatBoolOrExpr type_constraints with md:=md} + +def getUnionTypeAssertions (var: String) (md: MetaData) (tys: List String) (funcname: String): Option StmtExprMd := + match getUnionTypeConstraint var md tys funcname with + | some constraint => + let md: MetaData := md.withPropertySummary ("(" ++ funcname ++ " assert) Type constraint of " ++ var) + mkStmtExprMdWithLoc (.Assert constraint) md + | _ => none + +def getInputTypePreconditions (funcDecl : PythonFunctionDecl): List StmtExprMd := + funcDecl.args.filterMap (λ(var, md, tys, _) => getUnionTypeConstraint var md tys funcDecl.name) + +def getInputTypecheckAssertions (funcDecl : PythonFunctionDecl): List StmtExprMd := + funcDecl.args.filterMap (λ(var, md, tys, _)=> getUnionTypeAssertions var md tys funcDecl.name) + /-- Translate Python function to Laurel Procedure -/ def translateFunction (ctx : TranslationContext) (funcDecl : PythonFunctionDecl) (body: List (Python.stmt SourceRange)) : Except TranslationError (Laurel.Procedure × TranslationContext) := do @@ -1048,16 +1101,17 @@ def translateFunction (ctx : TranslationContext) (funcDecl : PythonFunctionDecl) -- Translate parameters let mut inputs : List Parameter := [] - inputs := funcDecl.args.map (fun (name, ty, _) => - if ctx.compositeTypes.any (fun ct => ct.name == ty) then - { name := name, type := mkHighTypeMd (.UserDefined ty) } + inputs := funcDecl.args.map (fun (name, _, ty, _) => + if ty.length == 1 && ctx.compositeTypes.any (fun ct => ct.name == ty[0]!) then + { name := name, type := mkHighTypeMd (.UserDefined ty[0]!) } else { name := name, type := AnyTy}) if funcDecl.hasKwargs then let paramType ← translateType ctx PyLauType.DictStrAny inputs:= inputs ++ [{ name := "kwargs", type := paramType }] - -- Translate return type + let typeConstraintAssertions := getInputTypecheckAssertions funcDecl + let typeConstraintPreconditions := getInputTypePreconditions funcDecl -- Determine outputs based on return type @@ -1067,11 +1121,13 @@ def translateFunction (ctx : TranslationContext) (funcDecl : PythonFunctionDecl) | some _ => [{ name := "LaurelResult", type := AnyTy }] -- Translate function body - let inputTypes := funcDecl.args.map (λ (name, type, _) => (name, type)) + let inputTypes := funcDecl.args.map (λ (name, _, type, _) => + match type with | [ty] => (name, ty) | _ => (name, PyLauType.Any)) let ctx := {ctx with variableTypes:= ("nullcall_ret", PyLauType.Any)::inputTypes} let (newctx, bodyStmts) ← translateStmtList ctx body let bodyStmts := prependExceptHandlingHelper bodyStmts let bodyStmts := (mkStmtExprMd (.LocalVariable "nullcall_ret" AnyTy (some AnyNone))) :: bodyStmts + let bodyStmts := typeConstraintAssertions ++ bodyStmts let bodyBlock := mkStmtExprMd (StmtExpr.Block bodyStmts none) -- Create procedure with transparent body (no contracts for now) @@ -1079,7 +1135,7 @@ def translateFunction (ctx : TranslationContext) (funcDecl : PythonFunctionDecl) name := funcDecl.name inputs := inputs outputs := outputs - preconditions := [] + preconditions := typeConstraintPreconditions determinism := .deterministic none -- TODO: need to set reads decreases := none body := Body.Transparent bodyBlock @@ -1125,7 +1181,7 @@ def preludeSignatureToPythonFunctionDecl (prelude : Core.Program) : List PythonF let noneexpr : Python.expr SourceRange := .Constant default (.ConNone default) default some { name:= proc.header.name.name - args:= (inputnames.zip inputTypes).map (λ(n,t) => (n,t,noneexpr)) + args:= (inputnames.zip inputTypes).map (λ(n,t) => (n, defaultMetadata, [t],noneexpr)) hasKwargs := false ret := if outputtypes.length == 0 then none else outputtypes[0]! } diff --git a/StrataMain.lean b/StrataMain.lean index fc789a2d3..aa1accfd1 100644 --- a/StrataMain.lean +++ b/StrataMain.lean @@ -521,7 +521,10 @@ def pyAnalyzeLaurelCommand : Command where else ("", "") | none => ("", "") - s := s ++ s!"{locationPrefix}{vcResult.obligation.label}: {match vcResult.outcome with | .ok o => Std.format o | .error e => e}{locationSuffix}\n" + let vcLabel := match vcResult.obligation.metadata.getPropertySummary with + | some msg => msg + | _ => vcResult.obligation.label + s := s ++ s!"{locationPrefix}{vcLabel}: {match vcResult.outcome with | .ok o => Std.format o | .error e => e}{locationSuffix}\n" IO.println s -- Output in SARIF format if requested if outputSarif then diff --git a/StrataTest/Languages/Python/expected_laurel/test_func_input_type_constraints.expected b/StrataTest/Languages/Python/expected_laurel/test_func_input_type_constraints.expected new file mode 100644 index 000000000..a07be9d40 --- /dev/null +++ b/StrataTest/Languages/Python/expected_laurel/test_func_input_type_constraints.expected @@ -0,0 +1,41 @@ + +==== Verification Results ==== +List_get_body_calls_List_get_0: ✅ pass +List_take_body_calls_List_take_0: ✅ pass +List_drop_body_calls_List_drop_0: ✅ pass +List_slice_body_calls_List_drop_0: ✅ pass +List_slice_body_calls_List_take_1: ✅ pass +List_set_body_calls_List_set_0: ✅ pass +DictStrAny_get_body_calls_DictStrAny_get_0: ✅ pass +Any_get_body_calls_DictStrAny_get_0: ✅ pass +Any_get_body_calls_List_get_1: ✅ pass +Any_get!_body_calls_DictStrAny_get_0: ✅ pass +Any_get!_body_calls_List_get_1: ✅ pass +Any_set_body_calls_List_set_0: ✅ pass +Any_set!_body_calls_List_set_0: ✅ pass +PFloorDiv_body_calls_Int.SafeDiv_0: ✅ pass +PFloorDiv_body_calls_Int.SafeDiv_1: ✅ pass +PFloorDiv_body_calls_Int.SafeDiv_2: ✅ pass +PFloorDiv_body_calls_Int.SafeDiv_3: ✅ pass +PAnd_body_calls_Any_to_bool_0: ✅ pass +POr_body_calls_Any_to_bool_0: ✅ pass +ret_type: ✅ pass (in prelude file) +ret_type: ✅ pass (in prelude file) +ret_pos: ✅ pass (in prelude file) +assert_name_is_foo: ✅ pass (in prelude file) +assert_opt_name_none_or_str: ✅ pass (in prelude file) +assert_opt_name_none_or_bar: ✅ pass (in prelude file) +ensures_maybe_except_none: ✅ pass (in prelude file) +(Mul assert) Type constraint of x: ✅ pass (at line 1, col 8) +(Mul assert) Type constraint of y: ✅ pass (at line 1, col 23) +(Sum assert) Type constraint of x: ✅ pass (at line 4, col 8) +(Sum assert) Type constraint of y: ✅ pass (at line 4, col 30) +ite_cond_calls_Any_to_bool_0: ✅ pass +(Mul requires) Type constraint of x: ✅ pass (at line 1, col 8) +(Mul requires) Type constraint of y: ✅ pass (at line 1, col 23) +(Sum requires) Type constraint of x: ✅ pass (at line 4, col 8) +(Sum requires) Type constraint of y: ✅ pass (at line 4, col 30) +(Mul requires) Type constraint of x: ✅ pass (at line 1, col 8) +(Mul requires) Type constraint of y: ✅ pass (at line 1, col 23) +(Sum requires) Type constraint of x: ✅ pass (at line 4, col 8) +(Sum requires) Type constraint of y: ✅ pass (at line 4, col 30) diff --git a/StrataTest/Languages/Python/expected_laurel/test_function_def_calls.expected b/StrataTest/Languages/Python/expected_laurel/test_function_def_calls.expected index 13a7ae3da..ddac03ac1 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_function_def_calls.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_function_def_calls.expected @@ -26,7 +26,9 @@ assert_name_is_foo: ✅ pass (in prelude file) assert_opt_name_none_or_str: ✅ pass (in prelude file) assert_opt_name_none_or_bar: ✅ pass (in prelude file) ensures_maybe_except_none: ✅ pass (in prelude file) +(my_f assert) Type constraint of s: ✅ pass (at line 5, col 9) (Origin_test_helper_procedure_Requires)req_name_is_foo: ❓ unknown (in prelude file) (Origin_test_helper_procedure_Requires)req_opt_name_none_or_str: ✅ pass (in prelude file) (Origin_test_helper_procedure_Requires)req_opt_name_none_or_bar: ✅ pass (in prelude file) +(my_f requires) Type constraint of s: ✅ pass (at line 5, col 9) ite_cond_calls_Any_to_bool_0: ✅ pass diff --git a/StrataTest/Languages/Python/tests/test_func_input_type_constraints.py b/StrataTest/Languages/Python/tests/test_func_input_type_constraints.py new file mode 100644 index 000000000..10548a9f8 --- /dev/null +++ b/StrataTest/Languages/Python/tests/test_func_input_type_constraints.py @@ -0,0 +1,10 @@ +def Mul(x: int | bool, y: int | bool = "abc") -> int: + return x * y + +def Sum(x: Union[int , bool], y: Union[int , bool] = None) -> int: + if y == None: + return x + return x + y + +a = Mul(1, True) +a = Sum(1, None) From 425494d975f2ac02d3ba52056bc9afc5bab4f83a Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Fri, 13 Mar 2026 13:06:51 -0700 Subject: [PATCH 02/31] add skip test to non-laurel sarif --- StrataTest/Languages/Python/run_py_analyze_sarif.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/StrataTest/Languages/Python/run_py_analyze_sarif.py b/StrataTest/Languages/Python/run_py_analyze_sarif.py index f043dc1a0..77cd0a547 100755 --- a/StrataTest/Languages/Python/run_py_analyze_sarif.py +++ b/StrataTest/Languages/Python/run_py_analyze_sarif.py @@ -20,7 +20,7 @@ ) BOTH_SKIP = {"test_foo_client_folder", "test_invalid_client_type", "test_unsupported_config"} -SKIP_TESTS = BOTH_SKIP | {"test_class_field_use", "test_list", "test_subscription"} +SKIP_TESTS = BOTH_SKIP | {"test_class_field_use", "test_list", "test_subscription", "test_func_input_type_constraints"} SKIP_TESTS_LAUREL = BOTH_SKIP From 2218a637716d82137dbcc1cf627e444f15ead31f Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Mon, 16 Mar 2026 08:44:36 -0700 Subject: [PATCH 03/31] merge conflict --- StrataMain.lean | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/StrataMain.lean b/StrataMain.lean index 63390a6d8..8a9d6f42d 100644 --- a/StrataMain.lean +++ b/StrataMain.lean @@ -518,7 +518,10 @@ def pyAnalyzeLaurelCommand : Command where ("", "") | none => ("", "") let outcomeStr := vcResult.formatOutcome - s := s ++ s!"{locationPrefix}{vcResult.obligation.label}: \ + let vcLabel := match vcResult.obligation.metadata.getPropertySummary with + | some msg => msg + | _ => vcResult.obligation.label + s := s ++ s!"{locationPrefix}{vcLabel}: \ {outcomeStr}{locationSuffix}\n" IO.println s -- Output in SARIF format if requested From e08098acbbe4b4f9da716868ab9f6f7a56cdcc90 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Tue, 17 Mar 2026 11:46:19 -0700 Subject: [PATCH 04/31] merge conflict --- StrataMain.lean | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/StrataMain.lean b/StrataMain.lean index 059efe8c8..c698f6aea 100644 --- a/StrataMain.lean +++ b/StrataMain.lean @@ -596,7 +596,7 @@ def pyAnalyzeLaurelCommand : Command where else ("", s!" (at line {pos.line}, col {pos.column})") else -git if vcResult.isFailure then + if vcResult.isFailure then (s!"Assertion failed in prelude file: ", "") else ("", s!" (in prelude file)") @@ -607,7 +607,10 @@ git if vcResult.isFailure then ("", "") | none => ("", "") let outcomeStr := vcResult.formatOutcome - s := s ++ s!"{locationPrefix}{vcResult.obligation.label}: \ + let vcLabel := match vcResult.obligation.metadata.getPropertySummary with + | some msg => msg + | _ => vcResult.obligation.label + s := s ++ s!"{locationPrefix}{vcLabel}: \ {outcomeStr}{locationSuffix}\n" IO.println s -- Output in SARIF format if requested From 5e8b9e67f464d58a353279d089e7606649306c13 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Tue, 17 Mar 2026 12:59:44 -0700 Subject: [PATCH 05/31] merge conflict --- StrataTest/Languages/Python/run_py_analyze_sarif.py | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/StrataTest/Languages/Python/run_py_analyze_sarif.py b/StrataTest/Languages/Python/run_py_analyze_sarif.py index ac3d184ac..c60550460 100755 --- a/StrataTest/Languages/Python/run_py_analyze_sarif.py +++ b/StrataTest/Languages/Python/run_py_analyze_sarif.py @@ -20,8 +20,7 @@ ) BOTH_SKIP = {"test_foo_client_folder", "test_invalid_client_type", "test_unsupported_config"} -SKIP_TESTS = BOTH_SKIP | {"test_class_field_use", "test_list", "test_subscription", "test_func_input_type_constraints"} -SKIP_TESTS = BOTH_SKIP | {"test_class_field_use", "test_list", "test_subscription", "test_with_statement"} +SKIP_TESTS = BOTH_SKIP | {"test_class_field_use", "test_list", "test_subscription", "test_with_statement", "test_func_input_type_constraints"} SKIP_TESTS_LAUREL = BOTH_SKIP From e7c8ae9b9d7c6b7660aaf554006e58ff8198f85b Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Thu, 19 Mar 2026 10:53:50 -0700 Subject: [PATCH 06/31] add PyArgInfo structure + fix expected test --- Strata/Languages/Python/PySpecPipeline.lean | 5 +- Strata/Languages/Python/PythonToLaurel.lean | 55 +++++++++++-------- StrataMain.lean | 4 +- .../test_func_input_type_constraints.expected | 4 -- 4 files changed, 34 insertions(+), 34 deletions(-) diff --git a/Strata/Languages/Python/PySpecPipeline.lean b/Strata/Languages/Python/PySpecPipeline.lean index d1fbadf17..c8e5d4d80 100644 --- a/Strata/Languages/Python/PySpecPipeline.lean +++ b/Strata/Languages/Python/PySpecPipeline.lean @@ -39,9 +39,8 @@ private def specDefaultToExpr : Python.Specs.SpecDefault → Python.expr SourceR | .none => .Constant default (.ConNone default) default /-- Convert a pyspec Arg to a PythonFunctionDecl arg tuple. -/ -private def specArgToFuncDeclArg (arg : Python.Specs.Arg) - : String × String × Option (Python.expr SourceRange) := - (arg.name, "Any", arg.default.map specDefaultToExpr) +private def specArgToFuncDeclArg (arg : Python.Specs.Arg): Python.PyArgInfo := + {name:= arg.name, md:= default, tys:= ["Any"], default:= arg.default.map specDefaultToExpr} /-- Build a PythonFunctionDecl from a PySpec FunctionDecl or class method, expanding `**kwargs` TypedDict fields into individual parameters. -/ diff --git a/Strata/Languages/Python/PythonToLaurel.lean b/Strata/Languages/Python/PythonToLaurel.lean index 8e0c65df3..f29b84403 100644 --- a/Strata/Languages/Python/PythonToLaurel.lean +++ b/Strata/Languages/Python/PythonToLaurel.lean @@ -59,10 +59,17 @@ inductive UnmodeledFunctionBehavior where | havocInputsAndOutputs deriving Inhabited +structure PyArgInfo where + name : String + md : MetaData + tys : List String + default : Option (Python.expr SourceRange) +deriving Repr + structure PythonFunctionDecl where name : String --args include name, type, default value - args : List (String × MetaData × List String × Option (Python.expr SourceRange)) + args : List PyArgInfo hasKwargs: Bool ret : Option String deriving Repr, Inhabited @@ -683,7 +690,7 @@ partial def removePosargsFromKwargs (kwords : List (Python.keyword SourceRange)) kwords.filter (λ kw => match kw with | .mk_keyword _ name _ => match name.val with - | some n => n.val ∉ funcDecl.args.unzip.fst + | some n => n.val ∉ funcDecl.args.map (·.name) | none => true) partial def combinePositionalAndKeywordArgs @@ -705,18 +712,18 @@ partial def combinePositionalAndKeywordArgs let kwords := pyKwordsToHashMap kwords 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 (name,_, _, d) => - !(name ∈ kwords.keys) && d.isNone + let missingArgs := unprovidedPosArgs.filter fun arg => + !(arg.name ∈ kwords.keys) && arg.default.isNone if missingArgs.length > 0 then let missingNames := missingArgs.map (·.1) throwUserError callRange s!"'{name}' called with missing required arguments: {missingNames}" let filledPosArgs ← - unprovidedPosArgs.mapM (λ (argName,_, _, d) => - match kwords.get? argName with + unprovidedPosArgs.mapM (λ arg => + match kwords.get? arg.name with | some expr => return expr - | none => match d with + | none => match arg.default with | some val => return val - | _ => throw (.typeError s!"'{name}' missing required argument '{argName}'")) + | _ => throw (.typeError s!"'{name}' missing required argument '{arg.name}'")) let posArgs := posArgs ++ filledPosArgs return (posArgs, kwordArgs, funcDecl.hasKwargs) | _ => return (posArgs, kwords, false) @@ -1211,7 +1218,7 @@ partial def argumentTypeToString (arg: Python.expr SourceRange) : Except Transla --The return is a List (inputname, type, default value) and a bool indicating if the function has Kwargs input def unpackPyArguments (ctx : TranslationContext) (args: Python.arguments SourceRange) - : Except TranslationError ((List (String × MetaData × List String × Option (Python.expr SourceRange))) × Bool):= do + : Except TranslationError ((List PyArgInfo) × Bool):= do match args with | .mk_arguments _ _ args _ _ _ kwargs defaults => let argscount := args.val.size @@ -1219,7 +1226,7 @@ def unpackPyArguments (ctx : TranslationContext) (args: Python.arguments SourceR let listdefaults := (List.range (argscount - defaultscount)).map (λ _ => none) ++ defaults.val.toList.map (λ x => some x) let argsinfo := args.val.toList.zip listdefaults - let argtypes ← + let argtypes : List PyArgInfo ← argsinfo.mapM (λ a: Python.arg SourceRange × Option (Python.expr SourceRange) => match a.fst with | .mk_arg sr name oty _ => @@ -1229,8 +1236,8 @@ def unpackPyArguments (ctx : TranslationContext) (args: Python.arguments SourceR let defaultType := match a.snd.mapM (inferExprType ctx) with | .ok (some ty) => [ty] | _ => [] - return (name.val, md, (← argumentTypeToString ty) ++ defaultType, a.snd) - | _ => return (name.val, md, [PyLauType.Any], a.snd)) + return {name:= name.val, md:=md, tys:=(← argumentTypeToString ty) ++ defaultType, default:= a.snd} + | _ => return {name:= name.val, md:= md, tys:=[PyLauType.Any], default:=a.snd}) return (argtypes, kwargs.val.isSome) def pyFuncDefToPythonFunctionDecl (ctx : TranslationContext) (f : Python.stmt SourceRange) : Except TranslationError PythonFunctionDecl := do @@ -1273,21 +1280,21 @@ def creatBoolOrExpr (exprs: List StmtExprMd) : StmtExprMd := def getUnionTypeConstraint (var: String) (md: MetaData) (tys: List String) (funcname: String): Option StmtExprMd := let type_constraints := tys.filterMap (getSingleTypeConstraint var) if type_constraints.isEmpty then none else - let md: MetaData := md.withPropertySummary ("(" ++ funcname ++ " requires) Type constraint of " ++ var) + let md: MetaData := md.withPropertySummary $ "(" ++ funcname ++ " requires) Type constraint of " ++ var some {creatBoolOrExpr type_constraints with md:=md} def getUnionTypeAssertions (var: String) (md: MetaData) (tys: List String) (funcname: String): Option StmtExprMd := match getUnionTypeConstraint var md tys funcname with | some constraint => - let md: MetaData := md.withPropertySummary ("(" ++ funcname ++ " assert) Type constraint of " ++ var) + let md: MetaData := md.withPropertySummary $ "(" ++ funcname ++ " assert) Type constraint of " ++ var mkStmtExprMdWithLoc (.Assert constraint) md | _ => none def getInputTypePreconditions (funcDecl : PythonFunctionDecl): List StmtExprMd := - funcDecl.args.filterMap (λ(var, md, tys, _) => getUnionTypeConstraint var md tys funcDecl.name) + funcDecl.args.filterMap (λ arg => getUnionTypeConstraint arg.name arg.md arg.tys funcDecl.name) def getInputTypecheckAssertions (funcDecl : PythonFunctionDecl): List StmtExprMd := - funcDecl.args.filterMap (λ(var, md, tys, _)=> getUnionTypeAssertions var md tys funcDecl.name) + funcDecl.args.filterMap (λ arg => getUnionTypeAssertions arg.name arg.md arg.tys funcDecl.name) /-- Translate Python function to Laurel Procedure -/ def translateFunction (ctx : TranslationContext) (sourceRange: SourceRange) (funcDecl : PythonFunctionDecl) (body: List (Python.stmt SourceRange)) @@ -1296,11 +1303,11 @@ def translateFunction (ctx : TranslationContext) (sourceRange: SourceRange) (fun -- Translate parameters let mut inputs : List Parameter := [] - inputs := funcDecl.args.map (fun (name, _, ty, _) => - if ty.length == 1 && ty[0]! ∈ ctx.compositeTypeNames then - { name := name, type := mkHighTypeMd (.UserDefined ty[0]!) } + inputs := funcDecl.args.map (fun arg => + if arg.tys.length == 1 && arg.tys[0]! ∈ ctx.compositeTypeNames then + { name := arg.name, type := mkHighTypeMd (.UserDefined {text:= arg.tys[0]!}) } else - { name := name, type := AnyTy}) + { name := arg.name, type := AnyTy}) if funcDecl.hasKwargs then let paramType ← translateType ctx PyLauType.DictStrAny inputs:= inputs ++ [{ name := "kwargs", type := paramType }] @@ -1316,8 +1323,8 @@ def translateFunction (ctx : TranslationContext) (sourceRange: SourceRange) (fun | some _ => [{ name := "LaurelResult", type := AnyTy }] -- Translate function body - let inputTypes := funcDecl.args.map (λ (name, _, type, _) => - match type with | [ty] => (name, ty) | _ => (name, PyLauType.Any)) + let inputTypes := funcDecl.args.map (λ arg => + match arg.tys with | [ty] => (arg.name, ty) | _ => (arg.name, PyLauType.Any)) let ctx := {ctx with variableTypes:= ("nullcall_ret", PyLauType.Any)::inputTypes} let (newctx, bodyStmts) ← translateStmtList ctx body let bodyStmts := prependExceptHandlingHelper bodyStmts @@ -1376,7 +1383,7 @@ def preludeSignatureToPythonFunctionDecl (prelude : Core.Program) : List PythonF let noneexpr : Python.expr SourceRange := .Constant default (.ConNone default) default some { name:= proc.header.name.name - args:= (inputnames.zip inputTypes).map (λ(n,t) => (n, defaultMetadata, [t],noneexpr)) + args:= (inputnames.zip inputTypes).map (λ(n,t) => {name:= n, md:= defaultMetadata, tys:= [t], default:= noneexpr}) hasKwargs := false ret := if outputtypes.length == 0 then none else outputtypes[0]! } @@ -1625,7 +1632,7 @@ def PreludeInfo.ofLaurelProgram (prog : Laurel.Program) : PreludeInfo where else let noDefault : Option (Python.expr SourceRange) := none let args := p.inputs.map fun param => - (param.name.text, default, [getHighTypeName param.type.val], noDefault) + {name:= param.name.text, md:= default, tys:= [getHighTypeName param.type.val], default:= noDefault} let ret := p.outputs.head?.map fun param => getHighTypeName param.type.val some { name := p.name.text, args := args, hasKwargs := false, ret := ret } functions := diff --git a/StrataMain.lean b/StrataMain.lean index 8292340b7..432a698aa 100644 --- a/StrataMain.lean +++ b/StrataMain.lean @@ -485,9 +485,7 @@ def pyAnalyzeLaurelCommand : Command where ("", "") | none => ("", "") let outcomeStr := vcResult.formatOutcome - let vcLabel := match vcResult.obligation.metadata.getPropertySummary with - | some msg => msg - | _ => vcResult.obligation.label + let vcLabel := vcResult.obligation.metadata.getPropertySummary.getD vcResult.obligation.label s := s ++ s!"{locationPrefix}{vcLabel}: \ {outcomeStr}{locationSuffix}\n" IO.println s diff --git a/StrataTest/Languages/Python/expected_laurel/test_func_input_type_constraints.expected b/StrataTest/Languages/Python/expected_laurel/test_func_input_type_constraints.expected index a07be9d40..1c826568b 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_func_input_type_constraints.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_func_input_type_constraints.expected @@ -35,7 +35,3 @@ ite_cond_calls_Any_to_bool_0: ✅ pass (Mul requires) Type constraint of y: ✅ pass (at line 1, col 23) (Sum requires) Type constraint of x: ✅ pass (at line 4, col 8) (Sum requires) Type constraint of y: ✅ pass (at line 4, col 30) -(Mul requires) Type constraint of x: ✅ pass (at line 1, col 8) -(Mul requires) Type constraint of y: ✅ pass (at line 1, col 23) -(Sum requires) Type constraint of x: ✅ pass (at line 4, col 8) -(Sum requires) Type constraint of y: ✅ pass (at line 4, col 30) From 104afcc45309ad57387ed865dfafac5772aa60b5 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Mon, 23 Mar 2026 11:50:55 -0700 Subject: [PATCH 07/31] merge conflict --- StrataTest/Languages/Python/run_py_analyze_sarif.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/StrataTest/Languages/Python/run_py_analyze_sarif.py b/StrataTest/Languages/Python/run_py_analyze_sarif.py index ce4048e0e..fc97fae2b 100755 --- a/StrataTest/Languages/Python/run_py_analyze_sarif.py +++ b/StrataTest/Languages/Python/run_py_analyze_sarif.py @@ -21,7 +21,7 @@ BOTH_SKIP = {"test_foo_client_folder", "test_invalid_client_type", "test_unsupported_config"} SKIP_TESTS = BOTH_SKIP | {"test_class_field_use", "test_list", "test_subscription", "test_with_statement", "test_class_field_init", "test_break_continue", "test_try_except", "test_try_except_scoping", "test_loops", - "test_augmented_assign", "test_list_slice", "test_class_field_any"} # sarif pipeline uses PythonToCore which doesn't yet support AugAssign + "test_augmented_assign", "test_list_slice", "test_class_field_any", "test_func_input_type_constraints"} # sarif pipeline uses PythonToCore which doesn't yet support AugAssign SKIP_TESTS_LAUREL = BOTH_SKIP From 185e629522e99f0107480a5b5023c75373bc2f55 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Mon, 23 Mar 2026 12:21:37 -0700 Subject: [PATCH 08/31] fix expected test --- .../expected_laurel/test_func_input_type_constraints.expected | 2 ++ 1 file changed, 2 insertions(+) diff --git a/StrataTest/Languages/Python/expected_laurel/test_func_input_type_constraints.expected b/StrataTest/Languages/Python/expected_laurel/test_func_input_type_constraints.expected index 1c826568b..b2751a477 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_func_input_type_constraints.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_func_input_type_constraints.expected @@ -9,6 +9,8 @@ List_set_body_calls_List_set_0: ✅ pass DictStrAny_get_body_calls_DictStrAny_get_0: ✅ pass Any_get_body_calls_DictStrAny_get_0: ✅ pass Any_get_body_calls_List_get_1: ✅ pass +Any_get_body_calls_List_slice_2: ✅ pass +Any_get_body_calls_List_drop_3: ✅ pass Any_get!_body_calls_DictStrAny_get_0: ✅ pass Any_get!_body_calls_List_get_1: ✅ pass Any_set_body_calls_List_set_0: ✅ pass From d4ebde6d7b0d4a16bb1e5e3c7879a90b7d27213a Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Tue, 24 Mar 2026 10:28:43 -0700 Subject: [PATCH 09/31] merge conflict --- StrataTest/Languages/Python/run_py_analyze_sarif.py | 1 + 1 file changed, 1 insertion(+) diff --git a/StrataTest/Languages/Python/run_py_analyze_sarif.py b/StrataTest/Languages/Python/run_py_analyze_sarif.py index 6d4dd7c0e..984ee2864 100755 --- a/StrataTest/Languages/Python/run_py_analyze_sarif.py +++ b/StrataTest/Languages/Python/run_py_analyze_sarif.py @@ -32,6 +32,7 @@ "test_default_params", "test_dict_operations", "test_for_loop", + "test_func_input_type_constraints", "test_if_elif", "test_list", "test_list_slice", From a2019e73628ed07ed671b0e3106e28382f49ac68 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Tue, 24 Mar 2026 11:16:25 -0700 Subject: [PATCH 10/31] fix expected test --- .../expected_laurel/test_default_params.expected | 14 +++++++++++++- .../Python/expected_laurel/test_if_elif.expected | 9 +++++++-- .../expected_laurel/test_multi_function.expected | 14 ++++++++++++-- .../expected_laurel/test_nested_calls.expected | 8 ++++++++ .../expected_laurel/test_return_types.expected | 4 ++++ 5 files changed, 44 insertions(+), 5 deletions(-) diff --git a/StrataTest/Languages/Python/expected_laurel/test_default_params.expected b/StrataTest/Languages/Python/expected_laurel/test_default_params.expected index e494ea9d1..24cec03a1 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_default_params.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_default_params.expected @@ -28,14 +28,26 @@ assert_name_is_foo: ✅ pass (in prelude file) assert_opt_name_none_or_str: ✅ pass (in prelude file) assert_opt_name_none_or_bar: ✅ pass (in prelude file) ensures_maybe_except_none: ✅ pass (in prelude file) -loop_guard_calls_Any_to_bool_0: ❓ unknown +(greet assert) Type constraint of name: ✅ pass (at line 1, col 10) +(greet assert) Type constraint of greeting: ✅ pass (at line 1, col 21) +(power assert) Type constraint of base: ✅ pass (at line 5, col 10) +(power assert) Type constraint of exp: ✅ pass (at line 5, col 21) +loop_guard_calls_Any_to_bool_0: ✅ pass loop_guard_end_calls_Any_to_bool_0: ✅ pass +(greet requires) Type constraint of name: ✅ pass (at line 1, col 10) +(greet requires) Type constraint of greeting: ✅ pass (at line 1, col 21) assert_assert(325)_calls_Any_to_bool_0: ✅ pass (at line 15, col 4) assert(325): ❓ unknown (at line 15, col 4) +(greet requires) Type constraint of name: ✅ pass (at line 1, col 10) +(greet requires) Type constraint of greeting: ✅ pass (at line 1, col 21) assert_assert(421)_calls_Any_to_bool_0: ✅ pass (at line 18, col 4) assert(421): ❓ unknown (at line 18, col 4) +(power requires) Type constraint of base: ✅ pass (at line 5, col 10) +(power requires) Type constraint of exp: ✅ pass (at line 5, col 21) assert_assert(501)_calls_Any_to_bool_0: ✅ pass (at line 21, col 4) assert(501): ❓ unknown (at line 21, col 4) +(power requires) Type constraint of base: ✅ pass (at line 5, col 10) +(power requires) Type constraint of exp: ✅ pass (at line 5, col 21) assert_assert(571)_calls_Any_to_bool_0: ✅ pass (at line 24, col 4) assert(571): ❓ unknown (at line 24, col 4) ite_cond_calls_Any_to_bool_0: ✅ pass diff --git a/StrataTest/Languages/Python/expected_laurel/test_if_elif.expected b/StrataTest/Languages/Python/expected_laurel/test_if_elif.expected index 4f691bbed..69523bca4 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_if_elif.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_if_elif.expected @@ -28,15 +28,20 @@ assert_name_is_foo: ✅ pass (in prelude file) assert_opt_name_none_or_str: ✅ pass (in prelude file) assert_opt_name_none_or_bar: ✅ pass (in prelude file) ensures_maybe_except_none: ✅ pass (in prelude file) -ite_cond_calls_Any_to_bool_0: ❓ unknown +(classify assert) Type constraint of x: ✅ pass (at line 1, col 13) ite_cond_calls_Any_to_bool_0: ✅ pass -ite_cond_calls_Any_to_bool_0: ❓ unknown +ite_cond_calls_Any_to_bool_0: ✅ pass +ite_cond_calls_Any_to_bool_0: ✅ pass +(classify requires) Type constraint of x: ✅ pass (at line 1, col 13) assert_assert(225)_calls_Any_to_bool_0: ✅ pass (at line 13, col 4) assert(225): ❓ unknown (at line 13, col 4) +(classify requires) Type constraint of x: ✅ pass (at line 1, col 13) assert_assert(302)_calls_Any_to_bool_0: ✅ pass (at line 16, col 4) assert(302): ❓ unknown (at line 16, col 4) +(classify requires) Type constraint of x: ✅ pass (at line 1, col 13) assert_assert(371)_calls_Any_to_bool_0: ✅ pass (at line 19, col 4) assert(371): ❓ unknown (at line 19, col 4) +(classify requires) Type constraint of x: ✅ pass (at line 1, col 13) assert_assert(444)_calls_Any_to_bool_0: ✅ pass (at line 22, col 4) assert(444): ❓ unknown (at line 22, col 4) ite_cond_calls_Any_to_bool_0: ✅ pass diff --git a/StrataTest/Languages/Python/expected_laurel/test_multi_function.expected b/StrataTest/Languages/Python/expected_laurel/test_multi_function.expected index b371d0cea..576e0286c 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_multi_function.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_multi_function.expected @@ -28,12 +28,22 @@ assert_name_is_foo: ✅ pass (in prelude file) assert_opt_name_none_or_str: ✅ pass (in prelude file) assert_opt_name_none_or_bar: ✅ pass (in prelude file) ensures_maybe_except_none: ✅ pass (in prelude file) -ite_cond_calls_PNotIn_0: ❓ unknown +(create_config assert) Type constraint of name: ✅ pass (at line 4, col 18) +(create_config assert) Type constraint of value: ✅ pass (at line 4, col 29) +(validate_config assert) Type constraint of config: ✅ pass (at line 8, col 20) +ite_cond_calls_PNotIn_0: ✅ pass ite_cond_calls_Any_to_bool_1: ✅ pass -ite_cond_calls_PNotIn_0: ❓ unknown +ite_cond_calls_PNotIn_0: ✅ pass ite_cond_calls_Any_to_bool_1: ✅ pass +(process_config assert) Type constraint of name: ✅ pass (at line 15, col 19) +(process_config assert) Type constraint of value: ✅ pass (at line 15, col 30) +(create_config requires) Type constraint of name: ✅ pass (at line 4, col 18) +(create_config requires) Type constraint of value: ✅ pass (at line 4, col 29) +(validate_config requires) Type constraint of config: ❓ unknown (at line 8, col 20) ite_cond_calls_Any_to_bool_0: ❓ unknown set_LaurelResult_calls_Any_get_0: ❓ unknown +(process_config requires) Type constraint of name: ✅ pass (at line 15, col 19) +(process_config requires) Type constraint of value: ✅ pass (at line 15, col 30) assert_assert(651)_calls_Any_to_bool_0: ✅ pass (at line 24, col 4) assert(651): ❓ unknown (at line 24, col 4) (Origin_test_helper_procedure_Requires)req_name_is_foo: ✅ pass (in prelude file) diff --git a/StrataTest/Languages/Python/expected_laurel/test_nested_calls.expected b/StrataTest/Languages/Python/expected_laurel/test_nested_calls.expected index 26ab4368d..c65dd6c16 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_nested_calls.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_nested_calls.expected @@ -28,10 +28,18 @@ assert_name_is_foo: ✅ pass (in prelude file) assert_opt_name_none_or_str: ✅ pass (in prelude file) assert_opt_name_none_or_bar: ✅ pass (in prelude file) ensures_maybe_except_none: ✅ pass (in prelude file) +(double assert) Type constraint of x: ✅ pass (at line 1, col 11) +(add_one assert) Type constraint of x: ✅ pass (at line 4, col 12) +(double requires) Type constraint of x: ✅ pass (at line 1, col 11) +(double requires) Type constraint of x: ❓ unknown (at line 1, col 11) assert_assert(153)_calls_Any_to_bool_0: ✅ pass (at line 10, col 4) assert(153): ❓ unknown (at line 10, col 4) +(double requires) Type constraint of x: ✅ pass (at line 1, col 11) +(add_one requires) Type constraint of x: ❓ unknown (at line 4, col 12) assert_assert(254)_calls_Any_to_bool_0: ✅ pass (at line 14, col 4) assert(254): ❓ unknown (at line 14, col 4) +(add_one requires) Type constraint of x: ✅ pass (at line 4, col 12) +(double requires) Type constraint of x: ❓ unknown (at line 1, col 11) assert_assert(356)_calls_Any_to_bool_0: ✅ pass (at line 18, col 4) assert(356): ❓ unknown (at line 18, col 4) ite_cond_calls_Any_to_bool_0: ✅ pass diff --git a/StrataTest/Languages/Python/expected_laurel/test_return_types.expected b/StrataTest/Languages/Python/expected_laurel/test_return_types.expected index 644c5adc7..ef0c24b42 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_return_types.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_return_types.expected @@ -28,12 +28,16 @@ assert_name_is_foo: ✅ pass (in prelude file) assert_opt_name_none_or_str: ✅ pass (in prelude file) assert_opt_name_none_or_bar: ✅ pass (in prelude file) ensures_maybe_except_none: ✅ pass (in prelude file) +(add assert) Type constraint of a: ✅ pass (at line 14, col 8) +(add assert) Type constraint of b: ✅ pass (at line 14, col 16) assert_assert(304)_calls_Any_to_bool_0: ✅ pass (at line 20, col 4) assert(304): ❓ unknown (at line 20, col 4) assert_assert(387)_calls_Any_to_bool_0: ✅ pass (at line 23, col 4) assert(387): ❓ unknown (at line 23, col 4) assert_assert(474)_calls_Any_to_bool_0: ✅ pass (at line 26, col 4) assert(474): ❓ unknown (at line 26, col 4) +(add requires) Type constraint of a: ✅ pass (at line 14, col 8) +(add requires) Type constraint of b: ✅ pass (at line 14, col 16) assert_assert(558)_calls_Any_to_bool_0: ✅ pass (at line 29, col 4) assert(558): ❓ unknown (at line 29, col 4) ite_cond_calls_Any_to_bool_0: ✅ pass From 1ec59313d864c8e02055e143257a1c79e7996fae Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Tue, 24 Mar 2026 15:22:12 -0700 Subject: [PATCH 11/31] remove assertions + add checking that input types are either a single composite type or a list of value type + minor fixes --- Strata/Languages/Python/PythonToLaurel.lean | 31 +++++++------------ .../test_default_params.expected | 4 --- .../test_func_input_type_constraints.expected | 12 +++---- .../test_func_type_constraint.expected | 0 .../test_function_def_calls.expected | 1 - .../expected_laurel/test_if_elif.expected | 1 - .../test_multi_function.expected | 5 --- .../test_nested_calls.expected | 2 -- .../test_return_types.expected | 2 -- .../tests/test_func_input_type_constraints.py | 2 ++ 10 files changed, 17 insertions(+), 43 deletions(-) create mode 100644 StrataTest/Languages/Python/expected_laurel/test_func_type_constraint.expected diff --git a/Strata/Languages/Python/PythonToLaurel.lean b/Strata/Languages/Python/PythonToLaurel.lean index c7f3089fd..1489055f5 100644 --- a/Strata/Languages/Python/PythonToLaurel.lean +++ b/Strata/Languages/Python/PythonToLaurel.lean @@ -1232,7 +1232,9 @@ partial def argumentTypeToString (arg: Python.expr SourceRange) : Except Transla | "Union" => match slice_head with | .Tuple _ tys _ => return (← tys.val.toList.mapM argumentTypeToString).flatten | _ => throw (.internalError s!"Unhandled Expr: {repr arg}") - | _ => return [v_name] + | "List" => return ["ListAny"] + | "Dict" => return ["DictStrAny"] + | _ => throw (.internalError s!"Unhandled Expr: {repr arg}") | .Constant _ _ _ => return ["None"] | .Attribute _ _ _ _ => return [pyExprToString arg] | .BinOp _ _ _ _ => return (← (getUnionTypes arg).mapM argumentTypeToString).flatten @@ -1274,6 +1276,8 @@ def pyFuncDefToPythonFunctionDecl (ctx : TranslationContext) (f : Python.stmt S | some retExpr => some (pyExprToString retExpr) | none => none let hasKwargs := args_trans.snd + if args.any (λ arg => arg.tys.length > 1 && (arg.tys.any (λ ty => ty ∈ ctx.compositeTypeNames))) then + throw (.unsupportedConstruct "Arg of union of class types is not supported" (toString (repr f))) return { name args @@ -1289,35 +1293,25 @@ def getSingleTypeConstraint (var: String) (ty: String): Option StmtExprMd := | "bool" => mkStmtExprMd (.StaticCall "Any..isfrom_bool" [freeVar var]) | "datetime" => mkStmtExprMd (.StaticCall "Any..isfrom_datetime" [freeVar var]) | "None" => mkStmtExprMd (.StaticCall "Any..isfrom_none" [freeVar var]) - | _ => if ty.startsWith "Dict" then mkStmtExprMd (.StaticCall "Any..isfrom_Dict" [freeVar var]) - else if ty.startsWith "List" then mkStmtExprMd (.StaticCall "Any..isfrom_ListAny" [freeVar var]) - else none + | "ListAny" => mkStmtExprMd (.StaticCall "Any..isfrom_ListAny" [freeVar var]) + | "DictStrAny" => mkStmtExprMd (.StaticCall "Any..isfrom_Dict" [freeVar var]) + | _ => none -def creatBoolOrExpr (exprs: List StmtExprMd) : StmtExprMd := +def createBoolOrExpr (exprs: List StmtExprMd) : StmtExprMd := match exprs with | [] => mkStmtExprMd (.LiteralBool true) | [expr] => expr - | expr::exprs => mkStmtExprMd (.StaticCall "Bool.Or" [expr, creatBoolOrExpr exprs]) + | expr::exprs => mkStmtExprMd (.PrimitiveOp .Or [expr, createBoolOrExpr exprs]) def getUnionTypeConstraint (var: String) (md: MetaData) (tys: List String) (funcname: String): Option StmtExprMd := let type_constraints := tys.filterMap (getSingleTypeConstraint var) if type_constraints.isEmpty then none else let md: MetaData := md.withPropertySummary $ "(" ++ funcname ++ " requires) Type constraint of " ++ var - some {creatBoolOrExpr type_constraints with md:=md} - -def getUnionTypeAssertions (var: String) (md: MetaData) (tys: List String) (funcname: String): Option StmtExprMd := - match getUnionTypeConstraint var md tys funcname with - | some constraint => - let md: MetaData := md.withPropertySummary $ "(" ++ funcname ++ " assert) Type constraint of " ++ var - mkStmtExprMdWithLoc (.Assert constraint) md - | _ => none + some {createBoolOrExpr type_constraints with md:=md} def getInputTypePreconditions (funcDecl : PythonFunctionDecl): List StmtExprMd := funcDecl.args.filterMap (λ arg => getUnionTypeConstraint arg.name arg.md arg.tys funcDecl.name) -def getInputTypecheckAssertions (funcDecl : PythonFunctionDecl): List StmtExprMd := - funcDecl.args.filterMap (λ arg => getUnionTypeAssertions arg.name arg.md arg.tys funcDecl.name) - /-- Translate Python function to Laurel Procedure -/ def translateFunction (ctx : TranslationContext) (sourceRange: SourceRange) (funcDecl : PythonFunctionDecl) (body: List (Python.stmt SourceRange)) : Except TranslationError (Laurel.Procedure × TranslationContext) := do @@ -1334,10 +1328,8 @@ def translateFunction (ctx : TranslationContext) (sourceRange: SourceRange) (fun let paramType ← translateType ctx PyLauType.DictStrAny inputs:= inputs ++ [{ name := "kwargs", type := paramType }] - let typeConstraintAssertions := getInputTypecheckAssertions funcDecl let typeConstraintPreconditions := getInputTypePreconditions funcDecl - -- Declare an output parameter when the function has a return type annotation. -- Return statements explicitly assign to LaurelResult and exit $body. let outputs : List Parameter := @@ -1352,7 +1344,6 @@ def translateFunction (ctx : TranslationContext) (sourceRange: SourceRange) (fun let (newctx, bodyStmts) ← translateStmtList ctx body let bodyStmts := prependExceptHandlingHelper bodyStmts let bodyStmts := (mkStmtExprMd (.LocalVariable "nullcall_ret" AnyTy (some AnyNone))) :: bodyStmts - let bodyStmts := typeConstraintAssertions ++ bodyStmts let bodyBlock := mkStmtExprMd (StmtExpr.Block bodyStmts none) -- Create procedure with transparent body (no contracts for now) diff --git a/StrataTest/Languages/Python/expected_laurel/test_default_params.expected b/StrataTest/Languages/Python/expected_laurel/test_default_params.expected index 24cec03a1..565cb2fff 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_default_params.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_default_params.expected @@ -28,10 +28,6 @@ assert_name_is_foo: ✅ pass (in prelude file) assert_opt_name_none_or_str: ✅ pass (in prelude file) assert_opt_name_none_or_bar: ✅ pass (in prelude file) ensures_maybe_except_none: ✅ pass (in prelude file) -(greet assert) Type constraint of name: ✅ pass (at line 1, col 10) -(greet assert) Type constraint of greeting: ✅ pass (at line 1, col 21) -(power assert) Type constraint of base: ✅ pass (at line 5, col 10) -(power assert) Type constraint of exp: ✅ pass (at line 5, col 21) loop_guard_calls_Any_to_bool_0: ✅ pass loop_guard_end_calls_Any_to_bool_0: ✅ pass (greet requires) Type constraint of name: ✅ pass (at line 1, col 10) diff --git a/StrataTest/Languages/Python/expected_laurel/test_func_input_type_constraints.expected b/StrataTest/Languages/Python/expected_laurel/test_func_input_type_constraints.expected index b2751a477..f489afd75 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_func_input_type_constraints.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_func_input_type_constraints.expected @@ -28,12 +28,8 @@ assert_name_is_foo: ✅ pass (in prelude file) assert_opt_name_none_or_str: ✅ pass (in prelude file) assert_opt_name_none_or_bar: ✅ pass (in prelude file) ensures_maybe_except_none: ✅ pass (in prelude file) -(Mul assert) Type constraint of x: ✅ pass (at line 1, col 8) -(Mul assert) Type constraint of y: ✅ pass (at line 1, col 23) -(Sum assert) Type constraint of x: ✅ pass (at line 4, col 8) -(Sum assert) Type constraint of y: ✅ pass (at line 4, col 30) ite_cond_calls_Any_to_bool_0: ✅ pass -(Mul requires) Type constraint of x: ✅ pass (at line 1, col 8) -(Mul requires) Type constraint of y: ✅ pass (at line 1, col 23) -(Sum requires) Type constraint of x: ✅ pass (at line 4, col 8) -(Sum requires) Type constraint of y: ✅ pass (at line 4, col 30) +(Mul requires) Type constraint of x: ✅ pass (at line 3, col 8) +(Mul requires) Type constraint of y: ✅ pass (at line 3, col 23) +(Sum requires) Type constraint of x: ✅ pass (at line 6, col 8) +(Sum requires) Type constraint of y: ✅ pass (at line 6, col 30) diff --git a/StrataTest/Languages/Python/expected_laurel/test_func_type_constraint.expected b/StrataTest/Languages/Python/expected_laurel/test_func_type_constraint.expected new file mode 100644 index 000000000..e69de29bb diff --git a/StrataTest/Languages/Python/expected_laurel/test_function_def_calls.expected b/StrataTest/Languages/Python/expected_laurel/test_function_def_calls.expected index d4ee625bd..176b8011d 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_function_def_calls.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_function_def_calls.expected @@ -28,7 +28,6 @@ assert_name_is_foo: ✅ pass (in prelude file) assert_opt_name_none_or_str: ✅ pass (in prelude file) assert_opt_name_none_or_bar: ✅ pass (in prelude file) ensures_maybe_except_none: ✅ pass (in prelude file) -(my_f assert) Type constraint of s: ✅ pass (at line 5, col 9) (Origin_test_helper_procedure_Requires)req_name_is_foo: ❓ unknown (in prelude file) (Origin_test_helper_procedure_Requires)req_opt_name_none_or_str: ✅ pass (in prelude file) (Origin_test_helper_procedure_Requires)req_opt_name_none_or_bar: ✅ pass (in prelude file) diff --git a/StrataTest/Languages/Python/expected_laurel/test_if_elif.expected b/StrataTest/Languages/Python/expected_laurel/test_if_elif.expected index 69523bca4..e95f9bad0 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_if_elif.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_if_elif.expected @@ -28,7 +28,6 @@ assert_name_is_foo: ✅ pass (in prelude file) assert_opt_name_none_or_str: ✅ pass (in prelude file) assert_opt_name_none_or_bar: ✅ pass (in prelude file) ensures_maybe_except_none: ✅ pass (in prelude file) -(classify assert) Type constraint of x: ✅ pass (at line 1, col 13) ite_cond_calls_Any_to_bool_0: ✅ pass ite_cond_calls_Any_to_bool_0: ✅ pass ite_cond_calls_Any_to_bool_0: ✅ pass diff --git a/StrataTest/Languages/Python/expected_laurel/test_multi_function.expected b/StrataTest/Languages/Python/expected_laurel/test_multi_function.expected index 576e0286c..f9f2ad873 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_multi_function.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_multi_function.expected @@ -28,15 +28,10 @@ assert_name_is_foo: ✅ pass (in prelude file) assert_opt_name_none_or_str: ✅ pass (in prelude file) assert_opt_name_none_or_bar: ✅ pass (in prelude file) ensures_maybe_except_none: ✅ pass (in prelude file) -(create_config assert) Type constraint of name: ✅ pass (at line 4, col 18) -(create_config assert) Type constraint of value: ✅ pass (at line 4, col 29) -(validate_config assert) Type constraint of config: ✅ pass (at line 8, col 20) ite_cond_calls_PNotIn_0: ✅ pass ite_cond_calls_Any_to_bool_1: ✅ pass ite_cond_calls_PNotIn_0: ✅ pass ite_cond_calls_Any_to_bool_1: ✅ pass -(process_config assert) Type constraint of name: ✅ pass (at line 15, col 19) -(process_config assert) Type constraint of value: ✅ pass (at line 15, col 30) (create_config requires) Type constraint of name: ✅ pass (at line 4, col 18) (create_config requires) Type constraint of value: ✅ pass (at line 4, col 29) (validate_config requires) Type constraint of config: ❓ unknown (at line 8, col 20) diff --git a/StrataTest/Languages/Python/expected_laurel/test_nested_calls.expected b/StrataTest/Languages/Python/expected_laurel/test_nested_calls.expected index c65dd6c16..cdb58f848 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_nested_calls.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_nested_calls.expected @@ -28,8 +28,6 @@ assert_name_is_foo: ✅ pass (in prelude file) assert_opt_name_none_or_str: ✅ pass (in prelude file) assert_opt_name_none_or_bar: ✅ pass (in prelude file) ensures_maybe_except_none: ✅ pass (in prelude file) -(double assert) Type constraint of x: ✅ pass (at line 1, col 11) -(add_one assert) Type constraint of x: ✅ pass (at line 4, col 12) (double requires) Type constraint of x: ✅ pass (at line 1, col 11) (double requires) Type constraint of x: ❓ unknown (at line 1, col 11) assert_assert(153)_calls_Any_to_bool_0: ✅ pass (at line 10, col 4) diff --git a/StrataTest/Languages/Python/expected_laurel/test_return_types.expected b/StrataTest/Languages/Python/expected_laurel/test_return_types.expected index ef0c24b42..73a51f684 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_return_types.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_return_types.expected @@ -28,8 +28,6 @@ assert_name_is_foo: ✅ pass (in prelude file) assert_opt_name_none_or_str: ✅ pass (in prelude file) assert_opt_name_none_or_bar: ✅ pass (in prelude file) ensures_maybe_except_none: ✅ pass (in prelude file) -(add assert) Type constraint of a: ✅ pass (at line 14, col 8) -(add assert) Type constraint of b: ✅ pass (at line 14, col 16) assert_assert(304)_calls_Any_to_bool_0: ✅ pass (at line 20, col 4) assert(304): ❓ unknown (at line 20, col 4) assert_assert(387)_calls_Any_to_bool_0: ✅ pass (at line 23, col 4) diff --git a/StrataTest/Languages/Python/tests/test_func_input_type_constraints.py b/StrataTest/Languages/Python/tests/test_func_input_type_constraints.py index 10548a9f8..4a16e3c6e 100644 --- a/StrataTest/Languages/Python/tests/test_func_input_type_constraints.py +++ b/StrataTest/Languages/Python/tests/test_func_input_type_constraints.py @@ -1,3 +1,5 @@ +from typing import Union + def Mul(x: int | bool, y: int | bool = "abc") -> int: return x * y From 74c071cda5897b3c8c2f7b8fc33b05b93a7e41b9 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Wed, 25 Mar 2026 11:00:01 -0700 Subject: [PATCH 12/31] fix defaultValue type + List, Dict element types --- Strata/Languages/Python/PythonToLaurel.lean | 83 +++++++++++++------ .../test_func_input_type_constraints.expected | 5 ++ .../tests/test_func_input_type_constraints.py | 7 +- 3 files changed, 69 insertions(+), 26 deletions(-) diff --git a/Strata/Languages/Python/PythonToLaurel.lean b/Strata/Languages/Python/PythonToLaurel.lean index 026780390..1aa47844b 100644 --- a/Strata/Languages/Python/PythonToLaurel.lean +++ b/Strata/Languages/Python/PythonToLaurel.lean @@ -1225,25 +1225,45 @@ def getUnionTypes (arg: Python.expr SourceRange) : List (Python.expr SourceRange | .BinOp _ left _ right => getUnionTypes left ++ getUnionTypes right | _ => [arg] -partial def argumentTypeToString (arg: Python.expr SourceRange) : Except TranslationError (List String) := +def isOfAnyType (ty: String): Bool := ty ∈ ["None", "bool", "int", "str", "float", "datetime", "ListAny", "DictStrAny", "Any"] + +partial def getArgumentTypes (arg: Python.expr SourceRange) : Except TranslationError (List String) := match arg with | .Name _ n _ => return [n.val] - | .Subscript _ _ _ _ => - let subscript_list:= getNestedSubscripts arg - let subscript_head := subscript_list[0]! - let slice_head := subscript_list[1]! - let v_name := pyExprToString subscript_head - match v_name with - | "Optional" => return [pyExprToString slice_head, "None"] - | "Union" => match slice_head with - | .Tuple _ tys _ => return (← tys.val.toList.mapM argumentTypeToString).flatten + | .Subscript _ _ slice _ => + let subscriptList:= getNestedSubscripts arg + let subscriptRoot := pyExprToString subscriptList[0]! + let sliceHead := subscriptList[1]! + match subscriptRoot with + | "Optional" => return [pyExprToString sliceHead, "None"] + | "Union" => match sliceHead with + | .Tuple _ tys _ => return (← tys.val.toList.mapM getArgumentTypes).flatten | _ => throw (.internalError s!"Unhandled Expr: {repr arg}") - | "List" => return ["ListAny"] - | "Dict" => return ["DictStrAny"] + | "List" => do + match ← getArgumentTypes slice with + | [ty] => + if isOfAnyType ty then + return ["ListAny"] + else + throw (.unsupportedConstruct "List of non-value type is not supported" s!"List[{ty}]") + | _ => throw (.unsupportedConstruct "Invalid list element type" s!"List[{toString (repr slice)}]") + | "Dict" => do match sliceHead with + | .Tuple _ tys _ => + if tys.val.size != 2 then + throw (.internalError s!"Unhandled Expr: {repr arg}") + else + match ← getArgumentTypes tys.val[0]!, ← getArgumentTypes tys.val[1]! with + | ["str"], [ty] => + if isOfAnyType ty then + return ["DictStrAny"] + else + throw (.unsupportedConstruct "Dict of non-value type is not supported" ty) + | _, _ => throw (.internalError s!"Unhandled Dict key/value types: {repr arg}") + | _ => throw (.unsupportedConstruct "Unhandled Dict key/value types" (toString (repr sliceHead))) | _ => throw (.internalError s!"Unhandled Expr: {repr arg}") | .Constant _ _ _ => return ["None"] | .Attribute _ _ _ _ => return [pyExprToString arg] - | .BinOp _ _ _ _ => return (← (getUnionTypes arg).mapM argumentTypeToString).flatten + | .BinOp _ _ _ _ => return (← (getUnionTypes arg).mapM getArgumentTypes).flatten | _ => throw (.internalError s!"Unhandled Expr: {repr arg}") --The return is a List (inputname, type, default value) and a bool indicating if the function has Kwargs input @@ -1256,18 +1276,32 @@ def unpackPyArguments (ctx : TranslationContext) (args: Python.arguments SourceR let listdefaults := (List.range (argscount - defaultscount)).map (λ _ => none) ++ defaults.val.toList.map (λ x => some x) let argsinfo := args.val.toList.zip listdefaults - let argtypes : List PyArgInfo ← - argsinfo.mapM (λ a: Python.arg SourceRange × Option (Python.expr SourceRange) => - match a.fst with + let mut argtypes : List PyArgInfo := [] + let mut tys : List String := [] + for (arg, default) in argsinfo do + match arg with | .mk_arg sr name oty _ => let md := sourceRangeToMetaData ctx.filePath sr - match oty.val with - | .some ty => - let defaultType := match a.snd.mapM (inferExprType ctx) with - | .ok (some ty) => [ty] - | _ => [] - return {name:= name.val, md:=md, tys:=(← argumentTypeToString ty) ++ defaultType, default:= a.snd} - | _ => return {name:= name.val, md:= md, tys:=[PyLauType.Any], default:=a.snd}) + let defaultType := match default.mapM (inferExprType ctx) with + | .ok (some ty) => some ty + | _ => none + tys ← match oty.val with + | .some ty => getArgumentTypes ty + | _ => pure [PyLauType.Any] + match defaultType with + | .some "None" => --Only None is allowed to add to type list + if tys != [PyLauType.Any] then + tys:= (PyLauType.None::tys).dedup + | .some defaultType => + if isOfAnyType defaultType && tys != [PyLauType.Any] && defaultType ∉ tys then + throw (.unsupportedConstruct "Default value type is invalid" (toString (repr arg))) + | _ => pure () + for ty in tys do + if ¬ (isOfAnyType ty || ty ∈ ctx.compositeTypeNames) then + throw (.unsupportedConstruct "Unknown type" ty) + if tys.length > 1 && tys.any (λ ty => ty ∈ ctx.compositeTypeNames) then + throw (.unsupportedConstruct "Argument of union of class types is not supported" (toString (repr arg))) + argtypes := argtypes ++ [{name:= name.val, md:=md, tys:= tys, default:= default}] return (argtypes, kwargs.val.isSome) def pyFuncDefToPythonFunctionDecl (ctx : TranslationContext) (f : Python.stmt SourceRange) : Except TranslationError PythonFunctionDecl := do @@ -1282,8 +1316,6 @@ def pyFuncDefToPythonFunctionDecl (ctx : TranslationContext) (f : Python.stmt S | some retExpr => some (pyExprToString retExpr) | none => none let hasKwargs := args_trans.snd - if args.any (λ arg => arg.tys.length > 1 && (arg.tys.any (λ ty => ty ∈ ctx.compositeTypeNames))) then - throw (.unsupportedConstruct "Arg of union of class types is not supported" (toString (repr f))) return { name args @@ -1297,6 +1329,7 @@ def getSingleTypeConstraint (var: String) (ty: String): Option StmtExprMd := | "str" => mkStmtExprMd (.StaticCall "Any..isfrom_string" [freeVar var]) | "int" => mkStmtExprMd (.StaticCall "Any..isfrom_int" [freeVar var]) | "bool" => mkStmtExprMd (.StaticCall "Any..isfrom_bool" [freeVar var]) + | "float" => mkStmtExprMd (.StaticCall "Any..isfrom_float" [freeVar var]) | "datetime" => mkStmtExprMd (.StaticCall "Any..isfrom_datetime" [freeVar var]) | "None" => mkStmtExprMd (.StaticCall "Any..isfrom_none" [freeVar var]) | "ListAny" => mkStmtExprMd (.StaticCall "Any..isfrom_ListAny" [freeVar var]) diff --git a/StrataTest/Languages/Python/expected_laurel/test_func_input_type_constraints.expected b/StrataTest/Languages/Python/expected_laurel/test_func_input_type_constraints.expected index f489afd75..08c4b801d 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_func_input_type_constraints.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_func_input_type_constraints.expected @@ -29,7 +29,12 @@ assert_opt_name_none_or_str: ✅ pass (in prelude file) assert_opt_name_none_or_bar: ✅ pass (in prelude file) ensures_maybe_except_none: ✅ pass (in prelude file) ite_cond_calls_Any_to_bool_0: ✅ pass +set_LaurelResult_calls_Any_get_0: ❓ unknown +set_LaurelResult_calls_Any_get_1: ❓ unknown (Mul requires) Type constraint of x: ✅ pass (at line 3, col 8) (Mul requires) Type constraint of y: ✅ pass (at line 3, col 23) (Sum requires) Type constraint of x: ✅ pass (at line 6, col 8) (Sum requires) Type constraint of y: ✅ pass (at line 6, col 30) +(List_Dict_index requires) Type constraint of l: ✅ pass (at line 11, col 20) +(List_Dict_index requires) Type constraint of i: ✅ pass (at line 11, col 45) +(List_Dict_index requires) Type constraint of s: ✅ pass (at line 11, col 54) diff --git a/StrataTest/Languages/Python/tests/test_func_input_type_constraints.py b/StrataTest/Languages/Python/tests/test_func_input_type_constraints.py index 4a16e3c6e..e40f2dab3 100644 --- a/StrataTest/Languages/Python/tests/test_func_input_type_constraints.py +++ b/StrataTest/Languages/Python/tests/test_func_input_type_constraints.py @@ -1,6 +1,6 @@ from typing import Union -def Mul(x: int | bool, y: int | bool = "abc") -> int: +def Mul(x: int | bool, y: int | bool = True) -> int: return x * y def Sum(x: Union[int , bool], y: Union[int , bool] = None) -> int: @@ -8,5 +8,10 @@ def Sum(x: Union[int , bool], y: Union[int , bool] = None) -> int: return x return x + y +def List_Dict_index(l: List[Dict[str, Any]], i: int, s: str) -> int: + return l[i][s] + + a = Mul(1, True) a = Sum(1, None) +a = List_Dict_index([{ "a": 1 }, {"b": 2}], 0, "a") From e0537493eb11850cf9c8a132d849f250c2b360c6 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Wed, 25 Mar 2026 11:30:40 -0700 Subject: [PATCH 13/31] merge conflict --- Strata/Languages/Python/PythonToLaurel.lean | 22 +++++++++++---------- 1 file changed, 12 insertions(+), 10 deletions(-) diff --git a/Strata/Languages/Python/PythonToLaurel.lean b/Strata/Languages/Python/PythonToLaurel.lean index 36fac66ed..2545789a2 100644 --- a/Strata/Languages/Python/PythonToLaurel.lean +++ b/Strata/Languages/Python/PythonToLaurel.lean @@ -1262,6 +1262,10 @@ def getUnionTypes (arg: Python.expr SourceRange) : List (Python.expr SourceRange def isOfAnyType (ty: String): Bool := ty ∈ ["None", "bool", "int", "str", "float", "datetime", "ListAny", "DictStrAny", "Any"] +def isCompositeType (ctx : TranslationContext) (ty: String) : Bool := match ctx.importedSymbols[ty]? with + | some (ImportedSymbol.compositeType _) => true + | _ => false + partial def getArgumentTypes (arg: Python.expr SourceRange) : Except TranslationError (List String) := match arg with | .Name _ n _ => return [n.val] @@ -1332,9 +1336,9 @@ def unpackPyArguments (ctx : TranslationContext) (args: Python.arguments SourceR throw (.unsupportedConstruct "Default value type is invalid" (toString (repr arg))) | _ => pure () for ty in tys do - if ¬ (isOfAnyType ty || ty ∈ ctx.compositeTypeNames) then + if ¬ (isOfAnyType ty || isCompositeType ctx ty) then throw (.unsupportedConstruct "Unknown type" ty) - if tys.length > 1 && tys.any (λ ty => ty ∈ ctx.compositeTypeNames) then + if tys.length > 1 && tys.any (isCompositeType ctx) then throw (.unsupportedConstruct "Argument of union of class types is not supported" (toString (repr arg))) argtypes := argtypes ++ [{name:= name.val, md:=md, tys:= tys, default:= default}] return (argtypes, kwargs.val.isSome) @@ -1393,14 +1397,12 @@ def translateFunction (ctx : TranslationContext) (sourceRange: SourceRange) (fun -- Translate parameters let mut inputs : List Parameter := [] - inputs ← funcDecl.args.mapM (fun (name, ty, _) => do - match ctx.importedSymbols[ty]? with - | some (ImportedSymbol.compositeType _) => - pure { name := name, type := mkHighTypeMd (.UserDefined ty) } - | some _ => - throw (.userPythonError sourceRange s!"'{ty}' is not a type") - | _ => - pure { name := name, type := AnyTy}) + inputs := funcDecl.args.map (fun arg => + if arg.tys.length == 1 && isCompositeType ctx arg.tys[0]! then + { name := arg.name, type := mkHighTypeMd (.UserDefined {text:= arg.tys[0]!}) } + else + { name := arg.name, type := AnyTy}) + if funcDecl.hasKwargs then let paramType ← translateType ctx PyLauType.DictStrAny inputs:= inputs ++ [{ name := "kwargs", type := paramType }] From 6288e119df4c39e36ca453c2c733152d3cb26233 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Wed, 25 Mar 2026 12:10:36 -0700 Subject: [PATCH 14/31] add compositeTypes from overloadtable to ImportedSymbol --- Strata/Languages/Python/PythonToLaurel.lean | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/Strata/Languages/Python/PythonToLaurel.lean b/Strata/Languages/Python/PythonToLaurel.lean index 2545789a2..d042be4a6 100644 --- a/Strata/Languages/Python/PythonToLaurel.lean +++ b/Strata/Languages/Python/PythonToLaurel.lean @@ -1793,9 +1793,17 @@ def pythonToLaurel' (info : PreludeInfo) instanceProcedures := [] } + let overloadCompositeType := Std.HashSet.ofList $ + (overloadTable.values.flatMap (·.values)).map fun ident => + if ident.pythonModule.isEmpty then + ident.name + else + ident.pythonModule ++ "_" ++ ident.name + let mut compositeTypeNames := info.compositeTypes.union overloadCompositeType + -- FIRST PASS: Collect all class definitions and field type info let mut compositeTypes : List CompositeType := [pyErrorTy] - let mut compositeTypeNames := info.compositeTypes.insert "PythonError" + compositeTypeNames := compositeTypeNames.insert "PythonError" let mut classFieldHighType : Std.HashMap String (Std.HashMap String HighType) := {} for stmt in body do match stmt with From 1f10a602468e8a26226f0abdb8a657eff4629a18 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Wed, 25 Mar 2026 14:48:38 -0700 Subject: [PATCH 15/31] fix throw error type invalid --- Strata/Languages/Python/PythonToLaurel.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Strata/Languages/Python/PythonToLaurel.lean b/Strata/Languages/Python/PythonToLaurel.lean index d042be4a6..622b8a102 100644 --- a/Strata/Languages/Python/PythonToLaurel.lean +++ b/Strata/Languages/Python/PythonToLaurel.lean @@ -1337,7 +1337,7 @@ def unpackPyArguments (ctx : TranslationContext) (args: Python.arguments SourceR | _ => pure () for ty in tys do if ¬ (isOfAnyType ty || isCompositeType ctx ty) then - throw (.unsupportedConstruct "Unknown type" ty) + throw (.userPythonError .none s!"'{ty}' is not a type") if tys.length > 1 && tys.any (isCompositeType ctx) then throw (.unsupportedConstruct "Argument of union of class types is not supported" (toString (repr arg))) argtypes := argtypes ++ [{name:= name.val, md:=md, tys:= tys, default:= default}] From 76acdb3e4d3842ee967e6dae11efe80955a93dad Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Wed, 25 Mar 2026 15:05:08 -0700 Subject: [PATCH 16/31] fix expected tests --- .../expected_laurel/test_default_params.expected | 4 ++-- .../test_func_input_type_constraints.expected | 3 +++ .../expected_laurel/test_function_def_calls.expected | 2 +- .../Python/expected_laurel/test_if_elif.expected | 4 ++-- .../expected_laurel/test_multi_function.expected | 4 ++-- .../expected_laurel/test_nested_calls.expected | 12 ++++++------ .../expected_laurel/test_return_types.expected | 4 ++-- 7 files changed, 18 insertions(+), 15 deletions(-) diff --git a/StrataTest/Languages/Python/expected_laurel/test_default_params.expected b/StrataTest/Languages/Python/expected_laurel/test_default_params.expected index 8c0a1646b..320d6689b 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_default_params.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_default_params.expected @@ -41,12 +41,12 @@ assert(421): ❓ unknown (at line 18, col 4) (power requires) Type constraint of base: ✅ pass (at line 5, col 10) (power requires) Type constraint of exp: ✅ pass (at line 5, col 21) assert_assert(501)_calls_Any_to_bool_0: ✅ pass (at line 21, col 4) -assert(501): ❓ unknown (at line 21, col 4) +Assertion failed at line 21, col 4: assert(501): ❌ fail (power requires) Type constraint of base: ✅ pass (at line 5, col 10) (power requires) Type constraint of exp: ✅ pass (at line 5, col 21) assert_assert(571)_calls_Any_to_bool_0: ✅ pass (at line 24, col 4) Assertion failed at line 24, col 4: assert(571): ❌ fail ite_cond_calls_Any_to_bool_0: ✅ pass -DETAIL: 34 passed, 3 failed, 2 inconclusive +DETAIL: 43 passed, 2 failed, 2 inconclusive RESULT: Failures found diff --git a/StrataTest/Languages/Python/expected_laurel/test_func_input_type_constraints.expected b/StrataTest/Languages/Python/expected_laurel/test_func_input_type_constraints.expected index 08c4b801d..c8c5d28ba 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_func_input_type_constraints.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_func_input_type_constraints.expected @@ -38,3 +38,6 @@ set_LaurelResult_calls_Any_get_1: ❓ unknown (List_Dict_index requires) Type constraint of l: ✅ pass (at line 11, col 20) (List_Dict_index requires) Type constraint of i: ✅ pass (at line 11, col 45) (List_Dict_index requires) Type constraint of s: ✅ pass (at line 11, col 54) + +DETAIL: 36 passed, 0 failed, 2 inconclusive +RESULT: Inconclusive diff --git a/StrataTest/Languages/Python/expected_laurel/test_function_def_calls.expected b/StrataTest/Languages/Python/expected_laurel/test_function_def_calls.expected index 927ec62bf..35ae67f70 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_function_def_calls.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_function_def_calls.expected @@ -34,5 +34,5 @@ ensures_maybe_except_none: ✅ pass (in prelude file) (my_f requires) Type constraint of s: ✅ pass (at line 5, col 9) ite_cond_calls_Any_to_bool_0: ✅ pass -DETAIL: 31 passed, 0 failed, 1 inconclusive +DETAIL: 32 passed, 0 failed, 1 inconclusive RESULT: Inconclusive diff --git a/StrataTest/Languages/Python/expected_laurel/test_if_elif.expected b/StrataTest/Languages/Python/expected_laurel/test_if_elif.expected index d3cf31310..6337fb264 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_if_elif.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_if_elif.expected @@ -45,5 +45,5 @@ assert_assert(444)_calls_Any_to_bool_0: ✅ pass (at line 22, col 4) assert(444): ❓ unknown (at line 22, col 4) ite_cond_calls_Any_to_bool_0: ✅ pass -DETAIL: 34 passed, 2 failed, 4 inconclusive -RESULT: Failures found +DETAIL: 40 passed, 0 failed, 4 inconclusive +RESULT: Inconclusive diff --git a/StrataTest/Languages/Python/expected_laurel/test_multi_function.expected b/StrataTest/Languages/Python/expected_laurel/test_multi_function.expected index 90f2e1b7e..fcd09f804 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_multi_function.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_multi_function.expected @@ -34,7 +34,7 @@ ite_cond_calls_PNotIn_0: ✅ pass ite_cond_calls_Any_to_bool_1: ✅ pass (create_config requires) Type constraint of name: ✅ pass (at line 4, col 18) (create_config requires) Type constraint of value: ✅ pass (at line 4, col 29) -(validate_config requires) Type constraint of config: ❓ unknown (at line 8, col 20) +Assertion failed at line 8, col 20: (validate_config requires) Type constraint of config: ❌ fail ite_cond_calls_Any_to_bool_0: ❓ unknown set_LaurelResult_calls_Any_get_0: ❓ unknown (process_config requires) Type constraint of name: ✅ pass (at line 15, col 19) @@ -46,5 +46,5 @@ Assertion failed at line 24, col 4: assert(651): ❌ fail (Origin_test_helper_procedure_Requires)req_opt_name_none_or_bar: ✅ pass (in prelude file) ite_cond_calls_Any_to_bool_0: ✅ pass -DETAIL: 35 passed, 2 failed, 3 inconclusive +DETAIL: 41 passed, 2 failed, 2 inconclusive RESULT: Failures found diff --git a/StrataTest/Languages/Python/expected_laurel/test_nested_calls.expected b/StrataTest/Languages/Python/expected_laurel/test_nested_calls.expected index a47f80a4a..a2fe02b16 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_nested_calls.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_nested_calls.expected @@ -29,18 +29,18 @@ assert_opt_name_none_or_str: ✅ pass (in prelude file) assert_opt_name_none_or_bar: ✅ pass (in prelude file) ensures_maybe_except_none: ✅ pass (in prelude file) (double requires) Type constraint of x: ✅ pass (at line 1, col 11) -(double requires) Type constraint of x: ❓ unknown (at line 1, col 11) +Assertion failed at line 1, col 11: (double requires) Type constraint of x: ❌ fail assert_assert(153)_calls_Any_to_bool_0: ✅ pass (at line 10, col 4) -assert(153): ❓ unknown (at line 10, col 4) +Assertion failed at line 10, col 4: assert(153): ❌ fail (double requires) Type constraint of x: ✅ pass (at line 1, col 11) -(add_one requires) Type constraint of x: ❓ unknown (at line 4, col 12) +Assertion failed at line 4, col 12: (add_one requires) Type constraint of x: ❌ fail assert_assert(254)_calls_Any_to_bool_0: ✅ pass (at line 14, col 4) -assert(254): ❓ unknown (at line 14, col 4) +Assertion failed at line 14, col 4: assert(254): ❌ fail (add_one requires) Type constraint of x: ✅ pass (at line 4, col 12) -(double requires) Type constraint of x: ❓ unknown (at line 1, col 11) +Assertion failed at line 1, col 11: (double requires) Type constraint of x: ❌ fail assert_assert(356)_calls_Any_to_bool_0: ✅ pass (at line 18, col 4) Assertion failed at line 18, col 4: assert(356): ❌ fail ite_cond_calls_Any_to_bool_0: ✅ pass -DETAIL: 32 passed, 3 failed, 0 inconclusive +DETAIL: 35 passed, 6 failed, 0 inconclusive RESULT: Failures found diff --git a/StrataTest/Languages/Python/expected_laurel/test_return_types.expected b/StrataTest/Languages/Python/expected_laurel/test_return_types.expected index dd5fa6c31..637fe8422 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_return_types.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_return_types.expected @@ -33,12 +33,12 @@ Assertion failed at line 20, col 4: assert(304): ❌ fail assert_assert(387)_calls_Any_to_bool_0: ✅ pass (at line 23, col 4) assert(387): ❓ unknown (at line 23, col 4) assert_assert(474)_calls_Any_to_bool_0: ✅ pass (at line 26, col 4) -assert(474): ❓ unknown (at line 26, col 4) +Assertion failed at line 26, col 4: assert(474): ❌ fail (add requires) Type constraint of a: ✅ pass (at line 14, col 8) (add requires) Type constraint of b: ✅ pass (at line 14, col 16) assert_assert(558)_calls_Any_to_bool_0: ✅ pass (at line 29, col 4) Assertion failed at line 29, col 4: assert(558): ❌ fail ite_cond_calls_Any_to_bool_0: ✅ pass -DETAIL: 33 passed, 3 failed, 1 inconclusive +DETAIL: 35 passed, 3 failed, 1 inconclusive RESULT: Failures found From 8770c48c295b7bc9da6567386d62366f20eb409d Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Thu, 26 Mar 2026 08:49:40 -0700 Subject: [PATCH 17/31] merge conflict in expected files --- .../test_default_params.expected | 4 +- .../test_func_input_type_constraints.expected | 44 +++++++++---------- .../test_function_def_calls.expected | 2 +- .../expected_laurel/test_if_elif.expected | 6 +-- .../test_multi_function.expected | 10 ++--- 5 files changed, 33 insertions(+), 33 deletions(-) diff --git a/StrataTest/Languages/Python/expected_laurel/test_default_params.expected b/StrataTest/Languages/Python/expected_laurel/test_default_params.expected index bdcd5d6fa..703bf972c 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_default_params.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_default_params.expected @@ -28,8 +28,8 @@ assert_name_is_foo: ✅ pass (in prelude file) assert_opt_name_none_or_str: ✅ pass (in prelude file) assert_opt_name_none_or_bar: ✅ pass (in prelude file) ensures_maybe_except_none: ✅ pass (in prelude file) -loop_guard_calls_Any_to_bool_0: ✅ pass -loop_guard_end_calls_Any_to_bool_0: ✅ pass +loop_guard_calls_Any_to_bool_0: ✅ pass (at line 8, col 4) +loop_guard_end_calls_Any_to_bool_0: ✅ pass (at line 8, col 4) (greet requires) Type constraint of name: ✅ pass (at line 1, col 10) (greet requires) Type constraint of greeting: ✅ pass (at line 1, col 21) assert_assert(325)_calls_Any_to_bool_0: ✅ pass (at line 15, col 4) diff --git a/StrataTest/Languages/Python/expected_laurel/test_func_input_type_constraints.expected b/StrataTest/Languages/Python/expected_laurel/test_func_input_type_constraints.expected index c8c5d28ba..48cbbad0d 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_func_input_type_constraints.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_func_input_type_constraints.expected @@ -1,26 +1,26 @@ ==== Verification Results ==== -List_get_body_calls_List_get_0: ✅ pass -List_take_body_calls_List_take_0: ✅ pass -List_drop_body_calls_List_drop_0: ✅ pass -List_slice_body_calls_List_drop_0: ✅ pass -List_slice_body_calls_List_take_1: ✅ pass -List_set_body_calls_List_set_0: ✅ pass -DictStrAny_get_body_calls_DictStrAny_get_0: ✅ pass -Any_get_body_calls_DictStrAny_get_0: ✅ pass -Any_get_body_calls_List_get_1: ✅ pass -Any_get_body_calls_List_slice_2: ✅ pass -Any_get_body_calls_List_drop_3: ✅ pass -Any_get!_body_calls_DictStrAny_get_0: ✅ pass -Any_get!_body_calls_List_get_1: ✅ pass -Any_set_body_calls_List_set_0: ✅ pass -Any_set!_body_calls_List_set_0: ✅ pass -PFloorDiv_body_calls_Int.SafeDiv_0: ✅ pass -PFloorDiv_body_calls_Int.SafeDiv_1: ✅ pass -PFloorDiv_body_calls_Int.SafeDiv_2: ✅ pass -PFloorDiv_body_calls_Int.SafeDiv_3: ✅ pass -PAnd_body_calls_Any_to_bool_0: ✅ pass -POr_body_calls_Any_to_bool_0: ✅ pass +List_get_body_calls_List_get_0: ✅ pass (in prelude file) +List_take_body_calls_List_take_0: ✅ pass (in prelude file) +List_drop_body_calls_List_drop_0: ✅ pass (in prelude file) +List_slice_body_calls_List_drop_0: ✅ pass (in prelude file) +List_slice_body_calls_List_take_1: ✅ pass (in prelude file) +List_set_body_calls_List_set_0: ✅ pass (in prelude file) +DictStrAny_get_body_calls_DictStrAny_get_0: ✅ pass (in prelude file) +Any_get_body_calls_DictStrAny_get_0: ✅ pass (in prelude file) +Any_get_body_calls_List_get_1: ✅ pass (in prelude file) +Any_get_body_calls_List_slice_2: ✅ pass (in prelude file) +Any_get_body_calls_List_drop_3: ✅ pass (in prelude file) +Any_get!_body_calls_DictStrAny_get_0: ✅ pass (in prelude file) +Any_get!_body_calls_List_get_1: ✅ pass (in prelude file) +Any_set_body_calls_List_set_0: ✅ pass (in prelude file) +Any_set!_body_calls_List_set_0: ✅ pass (in prelude file) +PFloorDiv_body_calls_Int.SafeDiv_0: ✅ pass (in prelude file) +PFloorDiv_body_calls_Int.SafeDiv_1: ✅ pass (in prelude file) +PFloorDiv_body_calls_Int.SafeDiv_2: ✅ pass (in prelude file) +PFloorDiv_body_calls_Int.SafeDiv_3: ✅ pass (in prelude file) +PAnd_body_calls_Any_to_bool_0: ✅ pass (in prelude file) +POr_body_calls_Any_to_bool_0: ✅ pass (in prelude file) ret_type: ✅ pass (in prelude file) ret_type: ✅ pass (in prelude file) ret_pos: ✅ pass (in prelude file) @@ -28,7 +28,7 @@ assert_name_is_foo: ✅ pass (in prelude file) assert_opt_name_none_or_str: ✅ pass (in prelude file) assert_opt_name_none_or_bar: ✅ pass (in prelude file) ensures_maybe_except_none: ✅ pass (in prelude file) -ite_cond_calls_Any_to_bool_0: ✅ pass +ite_cond_calls_Any_to_bool_0: ✅ pass (at line 7, col 4) set_LaurelResult_calls_Any_get_0: ❓ unknown set_LaurelResult_calls_Any_get_1: ❓ unknown (Mul requires) Type constraint of x: ✅ pass (at line 3, col 8) diff --git a/StrataTest/Languages/Python/expected_laurel/test_function_def_calls.expected b/StrataTest/Languages/Python/expected_laurel/test_function_def_calls.expected index 31922e682..52efc40ca 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_function_def_calls.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_function_def_calls.expected @@ -32,7 +32,7 @@ ensures_maybe_except_none: ✅ pass (in prelude file) (Origin_test_helper_procedure_Requires)req_opt_name_none_or_str: ✅ pass (in prelude file) (Origin_test_helper_procedure_Requires)req_opt_name_none_or_bar: ✅ pass (in prelude file) (my_f requires) Type constraint of s: ✅ pass (at line 5, col 9) -ite_cond_calls_Any_to_bool_0: ✅ pass +ite_cond_calls_Any_to_bool_0: ✅ pass (at line 11, col 0) DETAIL: 32 passed, 0 failed, 1 inconclusive RESULT: Inconclusive diff --git a/StrataTest/Languages/Python/expected_laurel/test_if_elif.expected b/StrataTest/Languages/Python/expected_laurel/test_if_elif.expected index b123a8b7f..35f8cc7c8 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_if_elif.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_if_elif.expected @@ -28,9 +28,9 @@ assert_name_is_foo: ✅ pass (in prelude file) assert_opt_name_none_or_str: ✅ pass (in prelude file) assert_opt_name_none_or_bar: ✅ pass (in prelude file) ensures_maybe_except_none: ✅ pass (in prelude file) -ite_cond_calls_Any_to_bool_0: ✅ pass -ite_cond_calls_Any_to_bool_0: ✅ pass -ite_cond_calls_Any_to_bool_0: ✅ pass +ite_cond_calls_Any_to_bool_0: ✅ pass (at line 2, col 4) +ite_cond_calls_Any_to_bool_0: ✅ pass (at line 4, col 4) +ite_cond_calls_Any_to_bool_0: ✅ pass (at line 6, col 4) (classify requires) Type constraint of x: ✅ pass (at line 1, col 13) assert_assert(225)_calls_Any_to_bool_0: ✅ pass (at line 13, col 4) assert(225): ❓ unknown (at line 13, col 4) diff --git a/StrataTest/Languages/Python/expected_laurel/test_multi_function.expected b/StrataTest/Languages/Python/expected_laurel/test_multi_function.expected index 27ccebe21..7288f308f 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_multi_function.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_multi_function.expected @@ -28,14 +28,14 @@ assert_name_is_foo: ✅ pass (in prelude file) assert_opt_name_none_or_str: ✅ pass (in prelude file) assert_opt_name_none_or_bar: ✅ pass (in prelude file) ensures_maybe_except_none: ✅ pass (in prelude file) -ite_cond_calls_PNotIn_0: ✅ pass -ite_cond_calls_Any_to_bool_1: ✅ pass -ite_cond_calls_PNotIn_0: ✅ pass -ite_cond_calls_Any_to_bool_1: ✅ pass +ite_cond_calls_PNotIn_0: ✅ pass (at line 9, col 4) +ite_cond_calls_Any_to_bool_1: ✅ pass (at line 9, col 4) +ite_cond_calls_PNotIn_0: ✅ pass (at line 11, col 4) +ite_cond_calls_Any_to_bool_1: ✅ pass (at line 11, col 4) (create_config requires) Type constraint of name: ✅ pass (at line 4, col 18) (create_config requires) Type constraint of value: ✅ pass (at line 4, col 29) Assertion failed at line 8, col 20: (validate_config requires) Type constraint of config: ❌ fail -ite_cond_calls_Any_to_bool_0: ❓ unknown +ite_cond_calls_Any_to_bool_0: ❓ unknown (at line 18, col 4) set_LaurelResult_calls_Any_get_0: ❓ unknown (process_config requires) Type constraint of name: ✅ pass (at line 15, col 19) (process_config requires) Type constraint of value: ✅ pass (at line 15, col 30) From 61724566850cdf67859acdbb5cf7b13c36c47f5f Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Thu, 26 Mar 2026 11:13:40 -0700 Subject: [PATCH 18/31] add return type constraints as postcondition --- Strata/Languages/Python/PythonToLaurel.lean | 53 +++++++++++++------ .../test_break_continue.expected | 8 ++- .../expected_laurel/test_class_decl.expected | 3 +- .../test_class_field_init.expected | 3 +- .../test_class_field_use.expected | 4 +- .../test_class_methods.expected | 3 +- .../test_class_with_methods.expected | 3 +- .../test_default_params.expected | 4 +- .../test_func_input_type_constraints.expected | 6 ++- .../expected_laurel/test_if_elif.expected | 6 ++- .../test_multi_function.expected | 10 ++-- .../test_nested_calls.expected | 10 ++-- .../test_return_types.expected | 7 ++- .../expected_laurel/test_while_loop.expected | 7 ++- .../test_with_statement.expected | 5 +- .../tests/test_func_input_type_constraints.py | 2 +- 16 files changed, 97 insertions(+), 37 deletions(-) diff --git a/Strata/Languages/Python/PythonToLaurel.lean b/Strata/Languages/Python/PythonToLaurel.lean index 2b1742045..978395a1d 100644 --- a/Strata/Languages/Python/PythonToLaurel.lean +++ b/Strata/Languages/Python/PythonToLaurel.lean @@ -66,7 +66,7 @@ structure PythonFunctionDecl where --args include name, type, default value args : List PyArgInfo hasKwargs: Bool - ret : Option String + ret : Option (List String × MetaData) deriving Repr, Inhabited /-- A symbol imported from a PySpec module, carrying its Laurel-internal @@ -202,6 +202,8 @@ def PyLauType.ListStr := "ListStr" def PyLauType.Package := "Package" def PyLauType.Any := "Any" +def PyLauFuncReturnVar := "LaurelResult" + /-- Convert a Laurel HighType to a PyLauType string for type inference. -/ def highTypeToPyLauType : HighType → String | .TInt => PyLauType.Int @@ -654,7 +656,9 @@ partial def getFunctionReturnType (ctx : TranslationContext) (func: Python.expr | _=> let (fname, _) ← refineFunctionCallExpr ctx func match ctx.functionSignatures.find? (λ f => f.name == fname) with - | some funcDecl => match funcDecl.ret with | some ty => return ty | _ => return PyLauType.Any + | some funcDecl => match funcDecl.ret with + | some ([ty], _) => return ty + | _ => return PyLauType.Any | _ => return PyLauType.Any @@ -1060,7 +1064,7 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang let stmts ← match value.val with | some expr => do let e ← translateExpr ctx expr - let assign := mkStmtExprMd (StmtExpr.Assign [mkStmtExprMd (StmtExpr.Identifier "LaurelResult")] e) + let assign := mkStmtExprMd (StmtExpr.Assign [mkStmtExprMd (StmtExpr.Identifier PyLauFuncReturnVar)] e) .ok [assign, mkStmtExprMd (StmtExpr.Exit "$body")] | none => .ok [mkStmtExprMd (StmtExpr.Exit "$body")] return (ctx, stmts) @@ -1266,6 +1270,14 @@ def isCompositeType (ctx : TranslationContext) (ty: String) : Bool := match ctx. | some (ImportedSymbol.compositeType _) => true | _ => false +def checkValidTypeList (ctx : TranslationContext) (tys: List String) : Except TranslationError (List String) := do + for ty in tys do + if ¬ (isOfAnyType ty || isCompositeType ctx ty) then + throw (.userPythonError .none s!"'{ty}' is not a type") + if tys.length > 1 && tys.any (isCompositeType ctx) then + throw (.unsupportedConstruct "Argument of union of class types is not supported" (toString tys)) + return tys + partial def getArgumentTypes (arg: Python.expr SourceRange) : Except TranslationError (List String) := match arg with | .Name _ n _ => return [n.val] @@ -1335,11 +1347,7 @@ def unpackPyArguments (ctx : TranslationContext) (args: Python.arguments SourceR if isOfAnyType defaultType && tys != [PyLauType.Any] && defaultType ∉ tys then throw (.unsupportedConstruct "Default value type is invalid" (toString (repr arg))) | _ => pure () - for ty in tys do - if ¬ (isOfAnyType ty || isCompositeType ctx ty) then - throw (.userPythonError .none s!"'{ty}' is not a type") - if tys.length > 1 && tys.any (isCompositeType ctx) then - throw (.unsupportedConstruct "Argument of union of class types is not supported" (toString (repr arg))) + tys ← checkValidTypeList ctx tys argtypes := argtypes ++ [{name:= name.val, md:=md, tys:= tys, default:= default}] return (argtypes, kwargs.val.isSome) @@ -1349,11 +1357,14 @@ def pyFuncDefToPythonFunctionDecl (ctx : TranslationContext) (f : Python.stmt S let name := match ctx.currentClassName with | none => name.val | some classname => classname ++ "_" ++ name.val let args_trans ← unpackPyArguments ctx args let args := if ctx.currentClassName.isSome then args_trans.fst.tail else args_trans.fst - let ret := if name.endsWith "@__init__" then some (name.dropEnd "@__init__".length).toString + let retMd := sourceRangeToMetaData ctx.filePath returns.ann + let ret ← if name.endsWith "@__init__" then pure $ some ([(name.dropEnd "@__init__".length).toString], retMd) else match returns.val with - | some retExpr => some (pyExprToString retExpr) - | none => none + | some retTy => + let tys ← checkValidTypeList ctx (← getArgumentTypes retTy) + pure (tys, retMd) + | none => pure none let hasKwargs := args_trans.snd return { name @@ -1387,6 +1398,12 @@ def getUnionTypeConstraint (var: String) (md: MetaData) (tys: List String) (func let md: MetaData := md.withPropertySummary $ "(" ++ funcname ++ " requires) Type constraint of " ++ var some {createBoolOrExpr type_constraints with md:=md} +def getReturnTypeEnsure (md: MetaData) (tys: List String) (funcname: String): Option StmtExprMd := + let type_constraints := tys.filterMap (getSingleTypeConstraint PyLauFuncReturnVar) + if type_constraints.isEmpty then none else + let md: MetaData := md.withPropertySummary $ "(" ++ funcname ++ " ensures) Return type constraint" + some {createBoolOrExpr type_constraints with md:=md} + def getInputTypePreconditions (funcDecl : PythonFunctionDecl): List StmtExprMd := funcDecl.args.filterMap (λ arg => getUnionTypeConstraint arg.name arg.md arg.tys funcDecl.name) @@ -1408,13 +1425,17 @@ def translateFunction (ctx : TranslationContext) (sourceRange: SourceRange) (fun inputs:= inputs ++ [{ name := "kwargs", type := paramType }] let typeConstraintPreconditions := getInputTypePreconditions funcDecl + let typeConstraintPostcondition := + match funcDecl.ret.map fun (tys, md) => getReturnTypeEnsure md tys funcDecl.name with + | some (some constraint) => [constraint] + | _ => [] -- Declare an output parameter when the function has a return type annotation. -- Return statements explicitly assign to LaurelResult and exit $body. let outputs : List Parameter := match funcDecl.ret with | none => [] - | some _ => [{ name := "LaurelResult", type := AnyTy }] + | some _ => [{ name := PyLauFuncReturnVar, type := AnyTy }] -- Translate function body let inputTypes := funcDecl.args.map (λ arg => @@ -1433,7 +1454,7 @@ def translateFunction (ctx : TranslationContext) (sourceRange: SourceRange) (fun preconditions := typeConstraintPreconditions determinism := .deterministic none -- TODO: need to set reads decreases := none - body := Body.Transparent bodyBlock + body := Body.Opaque typeConstraintPostcondition bodyBlock [] md := sourceRangeToMetaData ctx.filePath sourceRange isFunctional := false } @@ -1478,7 +1499,7 @@ def preludeSignatureToPythonFunctionDecl (prelude : Core.Program) : List PythonF name:= proc.header.name.name args:= (inputnames.zip inputTypes).map (λ(n,t) => {name:= n, md:= defaultMetadata, tys:= [t], default:= noneexpr}) hasKwargs := false - ret := if outputtypes.length == 0 then none else outputtypes[0]! + ret := if outputtypes.length == 0 then none else ([outputtypes[0]!], defaultMetadata) } | none => none /-- Extract field declarations from class body (annotated assignments at class level) -/ @@ -1539,7 +1560,7 @@ def translateMethod (ctx : TranslationContext) (className : String) let retType ← translateType ctx (pyExprToString retExpr) pure (match retType.val with | HighType.TVoid => [] - | _ => [{name := "LaurelResult", type := AnyTy}]) + | _ => [{name := PyLauFuncReturnVar, type := AnyTy}]) | none => pure [] -- Translate method body with class context @@ -1733,7 +1754,7 @@ def PreludeInfo.ofLaurelProgram (prog : Laurel.Program) : PreludeInfo where let noDefault : Option (Python.expr SourceRange) := none let args := p.inputs.map fun param => {name:= param.name.text, md:= default, tys:= [getHighTypeName param.type.val], default:= noDefault} - let ret := p.outputs.head?.map fun param => getHighTypeName param.type.val + let ret := p.outputs.head?.map fun param => ([getHighTypeName param.type.val], defaultMetadata) some { name := p.name.text, args := args, hasKwargs := false, ret := ret } functions := let funcNames := prog.staticProcedures.filterMap fun p => diff --git a/StrataTest/Languages/Python/expected_laurel/test_break_continue.expected b/StrataTest/Languages/Python/expected_laurel/test_break_continue.expected index b5cafb793..f4ab0d4c0 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_break_continue.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_break_continue.expected @@ -29,8 +29,12 @@ assert_opt_name_none_or_str: ✅ pass (in prelude file) assert_opt_name_none_or_bar: ✅ pass (in prelude file) ensures_maybe_except_none: ✅ pass (in prelude file) loop_guard_calls_Any_to_bool_0: ✅ pass (at line 3, col 4) +(test_while_break ensures) Return type constraint: ❌ fail loop_guard_calls_Any_to_bool_0: ✅ pass (at line 8, col 4) loop_guard_end_calls_Any_to_bool_0: ✅ pass (at line 8, col 4) +(test_while_continue ensures) Return type constraint: ❓ unknown +(test_for_break ensures) Return type constraint: ❌ fail +(test_for_continue ensures) Return type constraint: ❌ fail -DETAIL: 31 passed, 0 failed, 0 inconclusive -RESULT: Analysis success +DETAIL: 31 passed, 3 failed, 1 inconclusive +RESULT: Failures found diff --git a/StrataTest/Languages/Python/expected_laurel/test_class_decl.expected b/StrataTest/Languages/Python/expected_laurel/test_class_decl.expected index 068cc4cc7..ce725645c 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_class_decl.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_class_decl.expected @@ -28,7 +28,8 @@ assert_name_is_foo: ✅ pass (in prelude file) assert_opt_name_none_or_str: ✅ pass (in prelude file) assert_opt_name_none_or_bar: ✅ pass (in prelude file) ensures_maybe_except_none: ✅ pass (in prelude file) +postcondition: ✅ pass (at line 8, col 0) ite_cond_calls_Any_to_bool_0: ✅ pass (at line 13, col 0) -DETAIL: 29 passed, 0 failed, 0 inconclusive +DETAIL: 30 passed, 0 failed, 0 inconclusive RESULT: Analysis success diff --git a/StrataTest/Languages/Python/expected_laurel/test_class_field_init.expected b/StrataTest/Languages/Python/expected_laurel/test_class_field_init.expected index 068cc4cc7..1e93b3882 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_class_field_init.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_class_field_init.expected @@ -28,7 +28,8 @@ assert_name_is_foo: ✅ pass (in prelude file) assert_opt_name_none_or_str: ✅ pass (in prelude file) assert_opt_name_none_or_bar: ✅ pass (in prelude file) ensures_maybe_except_none: ✅ pass (in prelude file) +postcondition: ✅ pass (at line 9, col 0) ite_cond_calls_Any_to_bool_0: ✅ pass (at line 13, col 0) -DETAIL: 29 passed, 0 failed, 0 inconclusive +DETAIL: 30 passed, 0 failed, 0 inconclusive RESULT: Analysis success diff --git a/StrataTest/Languages/Python/expected_laurel/test_class_field_use.expected b/StrataTest/Languages/Python/expected_laurel/test_class_field_use.expected index 1522a3043..5e79e2d58 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_class_field_use.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_class_field_use.expected @@ -30,6 +30,8 @@ assert_opt_name_none_or_bar: ✅ pass (in prelude file) ensures_maybe_except_none: ✅ pass (in prelude file) assert_assert(285)_calls_Any_to_bool_0: ✅ pass (at line 14, col 4) Assertion failed at line 14, col 4: assert(285): ❌ fail +postcondition: ✅ pass (at line 11, col 0) +(process_buffer ensures) Return type constraint: ✅ pass -DETAIL: 29 passed, 1 failed, 0 inconclusive +DETAIL: 31 passed, 1 failed, 0 inconclusive RESULT: Failures found diff --git a/StrataTest/Languages/Python/expected_laurel/test_class_methods.expected b/StrataTest/Languages/Python/expected_laurel/test_class_methods.expected index f41b07ac4..89a07fb33 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_class_methods.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_class_methods.expected @@ -37,7 +37,8 @@ Assertion failed at line 28, col 4: assert(654): ❌ fail (Origin_test_helper_procedure_Requires)req_name_is_foo: ✅ pass (in prelude file) (Origin_test_helper_procedure_Requires)req_opt_name_none_or_str: ✅ pass (in prelude file) (Origin_test_helper_procedure_Requires)req_opt_name_none_or_bar: ✅ pass (in prelude file) +postcondition: ✅ pass (at line 17, col 0) ite_cond_calls_Any_to_bool_0: ✅ pass (at line 32, col 0) -DETAIL: 35 passed, 2 failed, 1 inconclusive +DETAIL: 36 passed, 2 failed, 1 inconclusive RESULT: Failures found diff --git a/StrataTest/Languages/Python/expected_laurel/test_class_with_methods.expected b/StrataTest/Languages/Python/expected_laurel/test_class_with_methods.expected index d3ed6f512..470658359 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_class_with_methods.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_class_with_methods.expected @@ -35,7 +35,8 @@ assert(544): ❓ unknown (at line 26, col 4) (Origin_test_helper_procedure_Requires)req_name_is_foo: ✅ pass (in prelude file) (Origin_test_helper_procedure_Requires)req_opt_name_none_or_str: ✅ pass (in prelude file) (Origin_test_helper_procedure_Requires)req_opt_name_none_or_bar: ✅ pass (in prelude file) +postcondition: ✅ pass (at line 17, col 0) ite_cond_calls_Any_to_bool_0: ✅ pass (at line 30, col 0) -DETAIL: 34 passed, 1 failed, 1 inconclusive +DETAIL: 35 passed, 1 failed, 1 inconclusive RESULT: Failures found diff --git a/StrataTest/Languages/Python/expected_laurel/test_default_params.expected b/StrataTest/Languages/Python/expected_laurel/test_default_params.expected index 703bf972c..7ed22f6a8 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_default_params.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_default_params.expected @@ -28,8 +28,10 @@ assert_name_is_foo: ✅ pass (in prelude file) assert_opt_name_none_or_str: ✅ pass (in prelude file) assert_opt_name_none_or_bar: ✅ pass (in prelude file) ensures_maybe_except_none: ✅ pass (in prelude file) +(greet ensures) Return type constraint: ✅ pass loop_guard_calls_Any_to_bool_0: ✅ pass (at line 8, col 4) loop_guard_end_calls_Any_to_bool_0: ✅ pass (at line 8, col 4) +(power ensures) Return type constraint: ❌ fail (greet requires) Type constraint of name: ✅ pass (at line 1, col 10) (greet requires) Type constraint of greeting: ✅ pass (at line 1, col 21) assert_assert(325)_calls_Any_to_bool_0: ✅ pass (at line 15, col 4) @@ -48,5 +50,5 @@ assert_assert(571)_calls_Any_to_bool_0: ✅ pass (at line 24, col 4) Assertion failed at line 24, col 4: assert(571): ❌ fail ite_cond_calls_Any_to_bool_0: ✅ pass (at line 26, col 0) -DETAIL: 43 passed, 2 failed, 2 inconclusive +DETAIL: 44 passed, 3 failed, 2 inconclusive RESULT: Failures found diff --git a/StrataTest/Languages/Python/expected_laurel/test_func_input_type_constraints.expected b/StrataTest/Languages/Python/expected_laurel/test_func_input_type_constraints.expected index 48cbbad0d..30ff653fb 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_func_input_type_constraints.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_func_input_type_constraints.expected @@ -28,9 +28,13 @@ assert_name_is_foo: ✅ pass (in prelude file) assert_opt_name_none_or_str: ✅ pass (in prelude file) assert_opt_name_none_or_bar: ✅ pass (in prelude file) ensures_maybe_except_none: ✅ pass (in prelude file) +(Mul ensures) Return type constraint: ✅ pass ite_cond_calls_Any_to_bool_0: ✅ pass (at line 7, col 4) +(Sum ensures) Return type constraint: ✅ pass +(Sum ensures) Return type constraint: ✅ pass set_LaurelResult_calls_Any_get_0: ❓ unknown set_LaurelResult_calls_Any_get_1: ❓ unknown +(List_Dict_index ensures) Return type constraint: ❓ unknown (Mul requires) Type constraint of x: ✅ pass (at line 3, col 8) (Mul requires) Type constraint of y: ✅ pass (at line 3, col 23) (Sum requires) Type constraint of x: ✅ pass (at line 6, col 8) @@ -39,5 +43,5 @@ set_LaurelResult_calls_Any_get_1: ❓ unknown (List_Dict_index requires) Type constraint of i: ✅ pass (at line 11, col 45) (List_Dict_index requires) Type constraint of s: ✅ pass (at line 11, col 54) -DETAIL: 36 passed, 0 failed, 2 inconclusive +DETAIL: 39 passed, 0 failed, 3 inconclusive RESULT: Inconclusive diff --git a/StrataTest/Languages/Python/expected_laurel/test_if_elif.expected b/StrataTest/Languages/Python/expected_laurel/test_if_elif.expected index 35f8cc7c8..20cc088af 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_if_elif.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_if_elif.expected @@ -29,8 +29,12 @@ assert_opt_name_none_or_str: ✅ pass (in prelude file) assert_opt_name_none_or_bar: ✅ pass (in prelude file) ensures_maybe_except_none: ✅ pass (in prelude file) ite_cond_calls_Any_to_bool_0: ✅ pass (at line 2, col 4) +(classify ensures) Return type constraint: ✅ pass ite_cond_calls_Any_to_bool_0: ✅ pass (at line 4, col 4) +(classify ensures) Return type constraint: ✅ pass ite_cond_calls_Any_to_bool_0: ✅ pass (at line 6, col 4) +(classify ensures) Return type constraint: ✅ pass +(classify ensures) Return type constraint: ✅ pass (classify requires) Type constraint of x: ✅ pass (at line 1, col 13) assert_assert(225)_calls_Any_to_bool_0: ✅ pass (at line 13, col 4) assert(225): ❓ unknown (at line 13, col 4) @@ -45,5 +49,5 @@ assert_assert(444)_calls_Any_to_bool_0: ✅ pass (at line 22, col 4) assert(444): ❓ unknown (at line 22, col 4) ite_cond_calls_Any_to_bool_0: ✅ pass (at line 24, col 0) -DETAIL: 40 passed, 0 failed, 4 inconclusive +DETAIL: 44 passed, 0 failed, 4 inconclusive RESULT: Inconclusive diff --git a/StrataTest/Languages/Python/expected_laurel/test_multi_function.expected b/StrataTest/Languages/Python/expected_laurel/test_multi_function.expected index 7288f308f..aa87548bd 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_multi_function.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_multi_function.expected @@ -28,14 +28,18 @@ assert_name_is_foo: ✅ pass (in prelude file) assert_opt_name_none_or_str: ✅ pass (in prelude file) assert_opt_name_none_or_bar: ✅ pass (in prelude file) ensures_maybe_except_none: ✅ pass (in prelude file) +(create_config ensures) Return type constraint: ✅ pass ite_cond_calls_PNotIn_0: ✅ pass (at line 9, col 4) ite_cond_calls_Any_to_bool_1: ✅ pass (at line 9, col 4) +(validate_config ensures) Return type constraint: ✅ pass ite_cond_calls_PNotIn_0: ✅ pass (at line 11, col 4) ite_cond_calls_Any_to_bool_1: ✅ pass (at line 11, col 4) +(validate_config ensures) Return type constraint: ✅ pass +(validate_config ensures) Return type constraint: ✅ pass (create_config requires) Type constraint of name: ✅ pass (at line 4, col 18) (create_config requires) Type constraint of value: ✅ pass (at line 4, col 29) -Assertion failed at line 8, col 20: (validate_config requires) Type constraint of config: ❌ fail -ite_cond_calls_Any_to_bool_0: ❓ unknown (at line 18, col 4) +(validate_config requires) Type constraint of config: ✅ pass (at line 8, col 20) +ite_cond_calls_Any_to_bool_0: ✅ pass (at line 18, col 4) set_LaurelResult_calls_Any_get_0: ❓ unknown (process_config requires) Type constraint of name: ✅ pass (at line 15, col 19) (process_config requires) Type constraint of value: ✅ pass (at line 15, col 30) @@ -46,5 +50,5 @@ Assertion failed at line 24, col 4: assert(651): ❌ fail (Origin_test_helper_procedure_Requires)req_opt_name_none_or_bar: ✅ pass (in prelude file) ite_cond_calls_Any_to_bool_0: ✅ pass (at line 28, col 0) -DETAIL: 41 passed, 2 failed, 2 inconclusive +DETAIL: 47 passed, 1 failed, 1 inconclusive RESULT: Failures found diff --git a/StrataTest/Languages/Python/expected_laurel/test_nested_calls.expected b/StrataTest/Languages/Python/expected_laurel/test_nested_calls.expected index dfc3f6874..7c4058c50 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_nested_calls.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_nested_calls.expected @@ -28,19 +28,21 @@ assert_name_is_foo: ✅ pass (in prelude file) assert_opt_name_none_or_str: ✅ pass (in prelude file) assert_opt_name_none_or_bar: ✅ pass (in prelude file) ensures_maybe_except_none: ✅ pass (in prelude file) +(double ensures) Return type constraint: ✅ pass +(add_one ensures) Return type constraint: ✅ pass +(double requires) Type constraint of x: ✅ pass (at line 1, col 11) (double requires) Type constraint of x: ✅ pass (at line 1, col 11) -Assertion failed at line 1, col 11: (double requires) Type constraint of x: ❌ fail assert_assert(153)_calls_Any_to_bool_0: ✅ pass (at line 10, col 4) Assertion failed at line 10, col 4: assert(153): ❌ fail (double requires) Type constraint of x: ✅ pass (at line 1, col 11) -Assertion failed at line 4, col 12: (add_one requires) Type constraint of x: ❌ fail +(add_one requires) Type constraint of x: ✅ pass (at line 4, col 12) assert_assert(254)_calls_Any_to_bool_0: ✅ pass (at line 14, col 4) Assertion failed at line 14, col 4: assert(254): ❌ fail (add_one requires) Type constraint of x: ✅ pass (at line 4, col 12) -Assertion failed at line 1, col 11: (double requires) Type constraint of x: ❌ fail +(double requires) Type constraint of x: ✅ pass (at line 1, col 11) assert_assert(356)_calls_Any_to_bool_0: ✅ pass (at line 18, col 4) Assertion failed at line 18, col 4: assert(356): ❌ fail ite_cond_calls_Any_to_bool_0: ✅ pass (at line 20, col 0) -DETAIL: 35 passed, 6 failed, 0 inconclusive +DETAIL: 40 passed, 3 failed, 0 inconclusive RESULT: Failures found diff --git a/StrataTest/Languages/Python/expected_laurel/test_return_types.expected b/StrataTest/Languages/Python/expected_laurel/test_return_types.expected index 1a2f808dd..ba1e56339 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_return_types.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_return_types.expected @@ -28,6 +28,11 @@ assert_name_is_foo: ✅ pass (in prelude file) assert_opt_name_none_or_str: ✅ pass (in prelude file) assert_opt_name_none_or_bar: ✅ pass (in prelude file) ensures_maybe_except_none: ✅ pass (in prelude file) +(get_number ensures) Return type constraint: ✅ pass +(get_greeting ensures) Return type constraint: ✅ pass +(get_flag ensures) Return type constraint: ✅ pass +(get_nothing ensures) Return type constraint: ✅ pass +(add ensures) Return type constraint: ✅ pass assert_assert(304)_calls_Any_to_bool_0: ✅ pass (at line 20, col 4) Assertion failed at line 20, col 4: assert(304): ❌ fail assert_assert(387)_calls_Any_to_bool_0: ✅ pass (at line 23, col 4) @@ -40,5 +45,5 @@ assert_assert(558)_calls_Any_to_bool_0: ✅ pass (at line 29, col 4) Assertion failed at line 29, col 4: assert(558): ❌ fail ite_cond_calls_Any_to_bool_0: ✅ pass (at line 31, col 0) -DETAIL: 35 passed, 3 failed, 1 inconclusive +DETAIL: 40 passed, 3 failed, 1 inconclusive RESULT: Failures found diff --git a/StrataTest/Languages/Python/expected_laurel/test_while_loop.expected b/StrataTest/Languages/Python/expected_laurel/test_while_loop.expected index b96183649..226d0d131 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_while_loop.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_while_loop.expected @@ -32,21 +32,26 @@ loop_guard_calls_Any_to_bool_0: ✅ pass (at line 4, col 4) loop_guard_end_calls_Any_to_bool_0: ✅ pass (at line 4, col 4) assert_assert(134)_calls_Any_to_bool_0: ✅ pass (at line 7, col 4) Assertion failed at line 7, col 4: assert(134): ❌ fail +(test_while_countdown ensures) Return type constraint: ❌ fail loop_guard_calls_Any_to_bool_0: ✅ pass (at line 12, col 4) ite_cond_calls_Any_to_bool_0: ✅ pass (at line 14, col 8) assert_assert(344)_calls_Any_to_bool_0: ✅ pass (at line 16, col 4) assert(344): ✅ pass (at line 16, col 4) +(test_while_true_break ensures) Return type constraint: ❓ unknown loop_guard_end_calls_Any_to_bool_0: ✅ pass (at line 12, col 4) assert_assert(344)_calls_Any_to_bool_0: ✅ pass (at line 16, col 4) assert(344): ✅ pass (at line 16, col 4) +(test_while_true_break ensures) Return type constraint: ✅ pass loop_guard_calls_Any_to_bool_0: ✅ pass (at line 22, col 4) ite_cond_calls_Any_to_bool_0: ✅ pass (at line 24, col 8) loop_guard_end_calls_Any_to_bool_0: ✅ pass (at line 22, col 4) assert_assert(589)_calls_Any_to_bool_0: ✅ pass (at line 27, col 4) assert(589): ❓ unknown (at line 27, col 4) +(test_while_with_continue ensures) Return type constraint: ❓ unknown loop_guard_end_calls_Any_to_bool_0: ✅ pass (at line 22, col 4) assert_assert(589)_calls_Any_to_bool_0: ✅ pass (at line 27, col 4) assert(589): ❓ unknown (at line 27, col 4) +(test_while_with_continue ensures) Return type constraint: ❓ unknown -DETAIL: 44 passed, 1 failed, 2 inconclusive +DETAIL: 45 passed, 2 failed, 5 inconclusive RESULT: Failures found diff --git a/StrataTest/Languages/Python/expected_laurel/test_with_statement.expected b/StrataTest/Languages/Python/expected_laurel/test_with_statement.expected index d3876eec6..3fbf73090 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_with_statement.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_with_statement.expected @@ -30,10 +30,13 @@ assert_opt_name_none_or_bar: ✅ pass (in prelude file) ensures_maybe_except_none: ✅ pass (in prelude file) assert_assert(368)_calls_Any_to_bool_0: ✅ pass (at line 19, col 4) Assertion failed at line 19, col 4: assert(368): ❌ fail +postcondition: ✅ pass (at line 14, col 0) assert_assert(500)_calls_Any_to_bool_0: ✅ pass (at line 25, col 8) Assertion failed at line 25, col 8: assert(500): ❌ fail +postcondition: ✅ pass (at line 21, col 0) assert_assert(666)_calls_Any_to_bool_0: ✅ pass (at line 32, col 8) assert(666): ❓ unknown (at line 32, col 8) +postcondition: ✅ pass (at line 27, col 0) -DETAIL: 31 passed, 2 failed, 1 inconclusive +DETAIL: 34 passed, 2 failed, 1 inconclusive RESULT: Failures found diff --git a/StrataTest/Languages/Python/tests/test_func_input_type_constraints.py b/StrataTest/Languages/Python/tests/test_func_input_type_constraints.py index e40f2dab3..f37b1c392 100644 --- a/StrataTest/Languages/Python/tests/test_func_input_type_constraints.py +++ b/StrataTest/Languages/Python/tests/test_func_input_type_constraints.py @@ -3,7 +3,7 @@ def Mul(x: int | bool, y: int | bool = True) -> int: return x * y -def Sum(x: Union[int , bool], y: Union[int , bool] = None) -> int: +def Sum(x: Union[int , bool], y: Union[int , bool] = None) -> int | bool: if y == None: return x return x + y From 062301cb33dcc17b4d2b76d0cf1d0a5e01556ce7 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Thu, 26 Mar 2026 13:53:53 -0700 Subject: [PATCH 19/31] merge conflict --- Strata/Languages/Python/PythonToLaurel.lean | 4 +-- .../test_break_continue.expected | 2 +- .../expected_laurel/test_class_decl.expected | 9 +------ .../test_class_field_init.expected | 9 +------ .../test_class_field_use.expected | 2 +- .../test_class_methods.expected | 8 +++--- .../test_class_with_methods.expected | 8 +++--- .../test_default_params.expected | 25 +++++++------------ .../test_func_input_type_constraints.expected | 24 +++++++----------- .../test_function_def_calls.expected | 17 ++++--------- .../expected_laurel/test_if_elif.expected | 17 ++++--------- .../test_multi_function.expected | 25 +++++++------------ .../test_nested_calls.expected | 21 ++++++---------- .../test_return_types.expected | 13 +++------- .../expected_laurel/test_while_loop.expected | 2 +- .../test_with_statement.expected | 2 +- 16 files changed, 63 insertions(+), 125 deletions(-) diff --git a/Strata/Languages/Python/PythonToLaurel.lean b/Strata/Languages/Python/PythonToLaurel.lean index 4c4301122..ab7f062fe 100644 --- a/Strata/Languages/Python/PythonToLaurel.lean +++ b/Strata/Languages/Python/PythonToLaurel.lean @@ -838,8 +838,8 @@ partial def translateCall (ctx : TranslationContext) let trans_posArgs ← args.mapM (translateExpr ctx) let trans_dict ← translateVarKwargs ctx kwords let remainingParams := funcDecl.args.drop args.length - let trans_dictArgs := remainingParams.map fun (argName, _, dflt) => - DictStrAny_get_param trans_dict argName dflt.isSome + let trans_dictArgs := remainingParams.map fun arg => + DictStrAny_get_param trans_dict arg.name arg.default.isSome let allArgs := trans_posArgs ++ trans_dictArgs let kwargsArg := if funcDecl.hasKwargs then [trans_dict] else [] emitCall (allArgs ++ kwargsArg) diff --git a/StrataTest/Languages/Python/expected_laurel/test_break_continue.expected b/StrataTest/Languages/Python/expected_laurel/test_break_continue.expected index c263ad708..3faeac68f 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_break_continue.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_break_continue.expected @@ -30,5 +30,5 @@ loop_guard_end_calls_Any_to_bool_0: ✅ pass (at line 8, col 4) (test_for_break ensures) Return type constraint: ❌ fail (test_for_continue ensures) Return type constraint: ❌ fail -DETAIL: 31 passed, 3 failed, 1 inconclusive +DETAIL: 25 passed, 3 failed, 1 inconclusive RESULT: Failures found diff --git a/StrataTest/Languages/Python/expected_laurel/test_class_decl.expected b/StrataTest/Languages/Python/expected_laurel/test_class_decl.expected index 8b73b3619..9a6d6744a 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_class_decl.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_class_decl.expected @@ -22,15 +22,8 @@ PFloorDiv_body_calls_Int.SafeDiv_2: ✅ pass (in prelude file) PFloorDiv_body_calls_Int.SafeDiv_3: ✅ pass (in prelude file) PAnd_body_calls_Any_to_bool_0: ✅ pass (in prelude file) POr_body_calls_Any_to_bool_0: ✅ pass (in prelude file) -ret_type: ✅ pass (in prelude file) -ret_type: ✅ pass (in prelude file) -ret_pos: ✅ pass (in prelude file) -assert_name_is_foo: ✅ pass (in prelude file) -assert_opt_name_none_or_str: ✅ pass (in prelude file) -assert_opt_name_none_or_bar: ✅ pass (in prelude file) -ensures_maybe_except_none: ✅ pass (in prelude file) postcondition: ✅ pass (at line 8, col 0) ite_cond_calls_Any_to_bool_0: ✅ pass (at line 13, col 0) -DETAIL: 30 passed, 0 failed, 0 inconclusive +DETAIL: 24 passed, 0 failed, 0 inconclusive RESULT: Analysis success diff --git a/StrataTest/Languages/Python/expected_laurel/test_class_field_init.expected b/StrataTest/Languages/Python/expected_laurel/test_class_field_init.expected index e0099da5a..89aada430 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_class_field_init.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_class_field_init.expected @@ -22,15 +22,8 @@ PFloorDiv_body_calls_Int.SafeDiv_2: ✅ pass (in prelude file) PFloorDiv_body_calls_Int.SafeDiv_3: ✅ pass (in prelude file) PAnd_body_calls_Any_to_bool_0: ✅ pass (in prelude file) POr_body_calls_Any_to_bool_0: ✅ pass (in prelude file) -ret_type: ✅ pass (in prelude file) -ret_type: ✅ pass (in prelude file) -ret_pos: ✅ pass (in prelude file) -assert_name_is_foo: ✅ pass (in prelude file) -assert_opt_name_none_or_str: ✅ pass (in prelude file) -assert_opt_name_none_or_bar: ✅ pass (in prelude file) -ensures_maybe_except_none: ✅ pass (in prelude file) postcondition: ✅ pass (at line 9, col 0) ite_cond_calls_Any_to_bool_0: ✅ pass (at line 13, col 0) -DETAIL: 30 passed, 0 failed, 0 inconclusive +DETAIL: 24 passed, 0 failed, 0 inconclusive RESULT: Analysis success diff --git a/StrataTest/Languages/Python/expected_laurel/test_class_field_use.expected b/StrataTest/Languages/Python/expected_laurel/test_class_field_use.expected index 5751e5f3d..2f8e1c96e 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_class_field_use.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_class_field_use.expected @@ -27,5 +27,5 @@ Assertion failed at line 14, col 4: assert(285): ❌ fail postcondition: ✅ pass (at line 11, col 0) (process_buffer ensures) Return type constraint: ✅ pass -DETAIL: 31 passed, 1 failed, 0 inconclusive +DETAIL: 25 passed, 1 failed, 0 inconclusive RESULT: Failures found diff --git a/StrataTest/Languages/Python/expected_laurel/test_class_methods.expected b/StrataTest/Languages/Python/expected_laurel/test_class_methods.expected index 91a99019c..d42e866fa 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_class_methods.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_class_methods.expected @@ -28,11 +28,11 @@ assert_assert(539)_calls_Any_to_bool_0: ✅ pass (at line 24, col 4) Assertion failed at line 24, col 4: assert(539): ❌ fail assert_assert(654)_calls_Any_to_bool_0: ✅ pass (at line 28, col 4) Assertion failed at line 28, col 4: assert(654): ❌ fail -(Origin_test_helper_procedure_Requires)req_name_is_foo: ✅ pass (in prelude file) -(Origin_test_helper_procedure_Requires)req_opt_name_none_or_str: ✅ pass (in prelude file) -(Origin_test_helper_procedure_Requires)req_opt_name_none_or_bar: ✅ pass (in prelude file) +callElimAssert_req_name_is_foo_4: ✅ pass (at line 30, col 4) +callElimAssert_req_opt_name_none_or_str_5: ✅ pass (at line 30, col 4) +callElimAssert_req_opt_name_none_or_bar_6: ✅ pass (at line 30, col 4) postcondition: ✅ pass (at line 17, col 0) ite_cond_calls_Any_to_bool_0: ✅ pass (at line 32, col 0) -DETAIL: 36 passed, 2 failed, 1 inconclusive +DETAIL: 30 passed, 2 failed, 1 inconclusive RESULT: Failures found diff --git a/StrataTest/Languages/Python/expected_laurel/test_class_with_methods.expected b/StrataTest/Languages/Python/expected_laurel/test_class_with_methods.expected index 0aded5e11..4c1d330cc 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_class_with_methods.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_class_with_methods.expected @@ -26,11 +26,11 @@ assert_assert(459)_calls_Any_to_bool_0: ✅ pass (at line 23, col 4) Assertion failed at line 23, col 4: assert(459): ❌ fail assert_assert(544)_calls_Any_to_bool_0: ✅ pass (at line 26, col 4) assert(544): ❓ unknown (at line 26, col 4) -(Origin_test_helper_procedure_Requires)req_name_is_foo: ✅ pass (in prelude file) -(Origin_test_helper_procedure_Requires)req_opt_name_none_or_str: ✅ pass (in prelude file) -(Origin_test_helper_procedure_Requires)req_opt_name_none_or_bar: ✅ pass (in prelude file) +callElimAssert_req_name_is_foo_4: ✅ pass (at line 28, col 4) +callElimAssert_req_opt_name_none_or_str_5: ✅ pass (at line 28, col 4) +callElimAssert_req_opt_name_none_or_bar_6: ✅ pass (at line 28, col 4) postcondition: ✅ pass (at line 17, col 0) ite_cond_calls_Any_to_bool_0: ✅ pass (at line 30, col 0) -DETAIL: 35 passed, 1 failed, 1 inconclusive +DETAIL: 29 passed, 1 failed, 1 inconclusive RESULT: Failures found diff --git a/StrataTest/Languages/Python/expected_laurel/test_default_params.expected b/StrataTest/Languages/Python/expected_laurel/test_default_params.expected index 6fe786c6a..179ecaf7f 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_default_params.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_default_params.expected @@ -22,34 +22,27 @@ PFloorDiv_body_calls_Int.SafeDiv_2: ✅ pass (in prelude file) PFloorDiv_body_calls_Int.SafeDiv_3: ✅ pass (in prelude file) PAnd_body_calls_Any_to_bool_0: ✅ pass (in prelude file) POr_body_calls_Any_to_bool_0: ✅ pass (in prelude file) -ret_type: ✅ pass (in prelude file) -ret_type: ✅ pass (in prelude file) -ret_pos: ✅ pass (in prelude file) -assert_name_is_foo: ✅ pass (in prelude file) -assert_opt_name_none_or_str: ✅ pass (in prelude file) -assert_opt_name_none_or_bar: ✅ pass (in prelude file) -ensures_maybe_except_none: ✅ pass (in prelude file) (greet ensures) Return type constraint: ✅ pass loop_guard_calls_Any_to_bool_0: ✅ pass (at line 8, col 4) loop_guard_end_calls_Any_to_bool_0: ✅ pass (at line 8, col 4) (power ensures) Return type constraint: ❌ fail -(greet requires) Type constraint of name: ✅ pass (at line 1, col 10) -(greet requires) Type constraint of greeting: ✅ pass (at line 1, col 21) +callElimAssert_requires_0_21: ✅ pass +callElimAssert_requires_1_22: ✅ pass assert_assert(325)_calls_Any_to_bool_0: ✅ pass (at line 15, col 4) assert(325): ❓ unknown (at line 15, col 4) -(greet requires) Type constraint of name: ✅ pass (at line 1, col 10) -(greet requires) Type constraint of greeting: ✅ pass (at line 1, col 21) +callElimAssert_requires_0_15: ✅ pass +callElimAssert_requires_1_16: ✅ pass assert_assert(421)_calls_Any_to_bool_0: ✅ pass (at line 18, col 4) assert(421): ❓ unknown (at line 18, col 4) -(power requires) Type constraint of base: ✅ pass (at line 5, col 10) -(power requires) Type constraint of exp: ✅ pass (at line 5, col 21) +callElimAssert_requires_0_9: ✅ pass +callElimAssert_requires_1_10: ✅ pass assert_assert(501)_calls_Any_to_bool_0: ✅ pass (at line 21, col 4) Assertion failed at line 21, col 4: assert(501): ❌ fail -(power requires) Type constraint of base: ✅ pass (at line 5, col 10) -(power requires) Type constraint of exp: ✅ pass (at line 5, col 21) +callElimAssert_requires_0_3: ✅ pass +callElimAssert_requires_1_4: ✅ pass assert_assert(571)_calls_Any_to_bool_0: ✅ pass (at line 24, col 4) Assertion failed at line 24, col 4: assert(571): ❌ fail ite_cond_calls_Any_to_bool_0: ✅ pass (at line 26, col 0) -DETAIL: 44 passed, 3 failed, 2 inconclusive +DETAIL: 38 passed, 3 failed, 2 inconclusive RESULT: Failures found diff --git a/StrataTest/Languages/Python/expected_laurel/test_func_input_type_constraints.expected b/StrataTest/Languages/Python/expected_laurel/test_func_input_type_constraints.expected index 30ff653fb..6879251c3 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_func_input_type_constraints.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_func_input_type_constraints.expected @@ -7,6 +7,7 @@ List_slice_body_calls_List_drop_0: ✅ pass (in prelude file) List_slice_body_calls_List_take_1: ✅ pass (in prelude file) List_set_body_calls_List_set_0: ✅ pass (in prelude file) DictStrAny_get_body_calls_DictStrAny_get_0: ✅ pass (in prelude file) +DictStrAny_get_or_none_body_calls_DictStrAny_get_0: ✅ pass (in prelude file) Any_get_body_calls_DictStrAny_get_0: ✅ pass (in prelude file) Any_get_body_calls_List_get_1: ✅ pass (in prelude file) Any_get_body_calls_List_slice_2: ✅ pass (in prelude file) @@ -21,13 +22,6 @@ PFloorDiv_body_calls_Int.SafeDiv_2: ✅ pass (in prelude file) PFloorDiv_body_calls_Int.SafeDiv_3: ✅ pass (in prelude file) PAnd_body_calls_Any_to_bool_0: ✅ pass (in prelude file) POr_body_calls_Any_to_bool_0: ✅ pass (in prelude file) -ret_type: ✅ pass (in prelude file) -ret_type: ✅ pass (in prelude file) -ret_pos: ✅ pass (in prelude file) -assert_name_is_foo: ✅ pass (in prelude file) -assert_opt_name_none_or_str: ✅ pass (in prelude file) -assert_opt_name_none_or_bar: ✅ pass (in prelude file) -ensures_maybe_except_none: ✅ pass (in prelude file) (Mul ensures) Return type constraint: ✅ pass ite_cond_calls_Any_to_bool_0: ✅ pass (at line 7, col 4) (Sum ensures) Return type constraint: ✅ pass @@ -35,13 +29,13 @@ ite_cond_calls_Any_to_bool_0: ✅ pass (at line 7, col 4) set_LaurelResult_calls_Any_get_0: ❓ unknown set_LaurelResult_calls_Any_get_1: ❓ unknown (List_Dict_index ensures) Return type constraint: ❓ unknown -(Mul requires) Type constraint of x: ✅ pass (at line 3, col 8) -(Mul requires) Type constraint of y: ✅ pass (at line 3, col 23) -(Sum requires) Type constraint of x: ✅ pass (at line 6, col 8) -(Sum requires) Type constraint of y: ✅ pass (at line 6, col 30) -(List_Dict_index requires) Type constraint of l: ✅ pass (at line 11, col 20) -(List_Dict_index requires) Type constraint of i: ✅ pass (at line 11, col 45) -(List_Dict_index requires) Type constraint of s: ✅ pass (at line 11, col 54) +callElimAssert_requires_0_17: ✅ pass +callElimAssert_requires_1_18: ✅ pass +callElimAssert_requires_0_11: ✅ pass +callElimAssert_requires_1_12: ✅ pass +callElimAssert_requires_0_4: ✅ pass +callElimAssert_requires_1_5: ✅ pass +callElimAssert_requires_2_6: ✅ pass -DETAIL: 39 passed, 0 failed, 3 inconclusive +DETAIL: 33 passed, 0 failed, 3 inconclusive RESULT: Inconclusive diff --git a/StrataTest/Languages/Python/expected_laurel/test_function_def_calls.expected b/StrataTest/Languages/Python/expected_laurel/test_function_def_calls.expected index 9faa00e3d..2926d779a 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_function_def_calls.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_function_def_calls.expected @@ -22,18 +22,11 @@ PFloorDiv_body_calls_Int.SafeDiv_2: ✅ pass (in prelude file) PFloorDiv_body_calls_Int.SafeDiv_3: ✅ pass (in prelude file) PAnd_body_calls_Any_to_bool_0: ✅ pass (in prelude file) POr_body_calls_Any_to_bool_0: ✅ pass (in prelude file) -ret_type: ✅ pass (in prelude file) -ret_type: ✅ pass (in prelude file) -ret_pos: ✅ pass (in prelude file) -assert_name_is_foo: ✅ pass (in prelude file) -assert_opt_name_none_or_str: ✅ pass (in prelude file) -assert_opt_name_none_or_bar: ✅ pass (in prelude file) -ensures_maybe_except_none: ✅ pass (in prelude file) -(Origin_test_helper_procedure_Requires)req_name_is_foo: ❓ unknown (in prelude file) -(Origin_test_helper_procedure_Requires)req_opt_name_none_or_str: ✅ pass (in prelude file) -(Origin_test_helper_procedure_Requires)req_opt_name_none_or_bar: ✅ pass (in prelude file) -(my_f requires) Type constraint of s: ✅ pass (at line 5, col 9) +callElimAssert_req_name_is_foo_4: ❓ unknown (at line 6, col 4) +callElimAssert_req_opt_name_none_or_str_5: ✅ pass (at line 6, col 4) +callElimAssert_req_opt_name_none_or_bar_6: ✅ pass (at line 6, col 4) +callElimAssert_requires_9: ✅ pass (at line 9, col 4) ite_cond_calls_Any_to_bool_0: ✅ pass (at line 11, col 0) -DETAIL: 32 passed, 0 failed, 1 inconclusive +DETAIL: 26 passed, 0 failed, 1 inconclusive RESULT: Inconclusive diff --git a/StrataTest/Languages/Python/expected_laurel/test_if_elif.expected b/StrataTest/Languages/Python/expected_laurel/test_if_elif.expected index f105d6e28..21260eed8 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_if_elif.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_if_elif.expected @@ -22,13 +22,6 @@ PFloorDiv_body_calls_Int.SafeDiv_2: ✅ pass (in prelude file) PFloorDiv_body_calls_Int.SafeDiv_3: ✅ pass (in prelude file) PAnd_body_calls_Any_to_bool_0: ✅ pass (in prelude file) POr_body_calls_Any_to_bool_0: ✅ pass (in prelude file) -ret_type: ✅ pass (in prelude file) -ret_type: ✅ pass (in prelude file) -ret_pos: ✅ pass (in prelude file) -assert_name_is_foo: ✅ pass (in prelude file) -assert_opt_name_none_or_str: ✅ pass (in prelude file) -assert_opt_name_none_or_bar: ✅ pass (in prelude file) -ensures_maybe_except_none: ✅ pass (in prelude file) ite_cond_calls_Any_to_bool_0: ✅ pass (at line 2, col 4) (classify ensures) Return type constraint: ✅ pass ite_cond_calls_Any_to_bool_0: ✅ pass (at line 4, col 4) @@ -36,19 +29,19 @@ ite_cond_calls_Any_to_bool_0: ✅ pass (at line 4, col 4) ite_cond_calls_Any_to_bool_0: ✅ pass (at line 6, col 4) (classify ensures) Return type constraint: ✅ pass (classify ensures) Return type constraint: ✅ pass -(classify requires) Type constraint of x: ✅ pass (at line 1, col 13) +callElimAssert_requires_14: ✅ pass assert_assert(225)_calls_Any_to_bool_0: ✅ pass (at line 13, col 4) assert(225): ❓ unknown (at line 13, col 4) -(classify requires) Type constraint of x: ✅ pass (at line 1, col 13) +callElimAssert_requires_10: ✅ pass assert_assert(302)_calls_Any_to_bool_0: ✅ pass (at line 16, col 4) assert(302): ❓ unknown (at line 16, col 4) -(classify requires) Type constraint of x: ✅ pass (at line 1, col 13) +callElimAssert_requires_6: ✅ pass assert_assert(371)_calls_Any_to_bool_0: ✅ pass (at line 19, col 4) assert(371): ❓ unknown (at line 19, col 4) -(classify requires) Type constraint of x: ✅ pass (at line 1, col 13) +callElimAssert_requires_2: ✅ pass assert_assert(444)_calls_Any_to_bool_0: ✅ pass (at line 22, col 4) assert(444): ❓ unknown (at line 22, col 4) ite_cond_calls_Any_to_bool_0: ✅ pass (at line 24, col 0) -DETAIL: 44 passed, 0 failed, 4 inconclusive +DETAIL: 38 passed, 0 failed, 4 inconclusive RESULT: Inconclusive diff --git a/StrataTest/Languages/Python/expected_laurel/test_multi_function.expected b/StrataTest/Languages/Python/expected_laurel/test_multi_function.expected index 784b785a6..abf46c960 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_multi_function.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_multi_function.expected @@ -22,13 +22,6 @@ PFloorDiv_body_calls_Int.SafeDiv_2: ✅ pass (in prelude file) PFloorDiv_body_calls_Int.SafeDiv_3: ✅ pass (in prelude file) PAnd_body_calls_Any_to_bool_0: ✅ pass (in prelude file) POr_body_calls_Any_to_bool_0: ✅ pass (in prelude file) -ret_type: ✅ pass (in prelude file) -ret_type: ✅ pass (in prelude file) -ret_pos: ✅ pass (in prelude file) -assert_name_is_foo: ✅ pass (in prelude file) -assert_opt_name_none_or_str: ✅ pass (in prelude file) -assert_opt_name_none_or_bar: ✅ pass (in prelude file) -ensures_maybe_except_none: ✅ pass (in prelude file) (create_config ensures) Return type constraint: ✅ pass ite_cond_calls_PNotIn_0: ✅ pass (at line 9, col 4) ite_cond_calls_Any_to_bool_1: ✅ pass (at line 9, col 4) @@ -37,19 +30,19 @@ ite_cond_calls_PNotIn_0: ✅ pass (at line 11, col 4) ite_cond_calls_Any_to_bool_1: ✅ pass (at line 11, col 4) (validate_config ensures) Return type constraint: ✅ pass (validate_config ensures) Return type constraint: ✅ pass -(create_config requires) Type constraint of name: ✅ pass (at line 4, col 18) -(create_config requires) Type constraint of value: ✅ pass (at line 4, col 29) -(validate_config requires) Type constraint of config: ✅ pass (at line 8, col 20) +callElimAssert_requires_0_7: ✅ pass +callElimAssert_requires_1_8: ✅ pass +callElimAssert_requires_2: ✅ pass ite_cond_calls_Any_to_bool_0: ✅ pass (at line 18, col 4) set_LaurelResult_calls_Any_get_0: ❓ unknown -(process_config requires) Type constraint of name: ✅ pass (at line 15, col 19) -(process_config requires) Type constraint of value: ✅ pass (at line 15, col 30) +callElimAssert_requires_0_21: ✅ pass +callElimAssert_requires_1_22: ✅ pass assert_assert(651)_calls_Any_to_bool_0: ✅ pass (at line 24, col 4) Assertion failed at line 24, col 4: assert(651): ❌ fail -callElimAssert_req_name_is_foo_9: ✅ pass (at line 26, col 4) -callElimAssert_req_opt_name_none_or_str_10: ✅ pass (at line 26, col 4) -callElimAssert_req_opt_name_none_or_bar_11: ✅ pass (at line 26, col 4) +callElimAssert_req_name_is_foo_14: ✅ pass (at line 26, col 4) +callElimAssert_req_opt_name_none_or_str_15: ✅ pass (at line 26, col 4) +callElimAssert_req_opt_name_none_or_bar_16: ✅ pass (at line 26, col 4) ite_cond_calls_Any_to_bool_0: ✅ pass (at line 28, col 0) -DETAIL: 47 passed, 1 failed, 1 inconclusive +DETAIL: 41 passed, 1 failed, 1 inconclusive RESULT: Failures found diff --git a/StrataTest/Languages/Python/expected_laurel/test_nested_calls.expected b/StrataTest/Languages/Python/expected_laurel/test_nested_calls.expected index 4fa806bbc..1bbdc9647 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_nested_calls.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_nested_calls.expected @@ -22,28 +22,21 @@ PFloorDiv_body_calls_Int.SafeDiv_2: ✅ pass (in prelude file) PFloorDiv_body_calls_Int.SafeDiv_3: ✅ pass (in prelude file) PAnd_body_calls_Any_to_bool_0: ✅ pass (in prelude file) POr_body_calls_Any_to_bool_0: ✅ pass (in prelude file) -ret_type: ✅ pass (in prelude file) -ret_type: ✅ pass (in prelude file) -ret_pos: ✅ pass (in prelude file) -assert_name_is_foo: ✅ pass (in prelude file) -assert_opt_name_none_or_str: ✅ pass (in prelude file) -assert_opt_name_none_or_bar: ✅ pass (in prelude file) -ensures_maybe_except_none: ✅ pass (in prelude file) (double ensures) Return type constraint: ✅ pass (add_one ensures) Return type constraint: ✅ pass -(double requires) Type constraint of x: ✅ pass (at line 1, col 11) -(double requires) Type constraint of x: ✅ pass (at line 1, col 11) +callElimAssert_requires_22: ✅ pass +callElimAssert_requires_18: ✅ pass assert_assert(153)_calls_Any_to_bool_0: ✅ pass (at line 10, col 4) Assertion failed at line 10, col 4: assert(153): ❌ fail -(double requires) Type constraint of x: ✅ pass (at line 1, col 11) -(add_one requires) Type constraint of x: ✅ pass (at line 4, col 12) +callElimAssert_requires_14: ✅ pass +callElimAssert_requires_10: ✅ pass assert_assert(254)_calls_Any_to_bool_0: ✅ pass (at line 14, col 4) Assertion failed at line 14, col 4: assert(254): ❌ fail -(add_one requires) Type constraint of x: ✅ pass (at line 4, col 12) -(double requires) Type constraint of x: ✅ pass (at line 1, col 11) +callElimAssert_requires_6: ✅ pass +callElimAssert_requires_2: ✅ pass assert_assert(356)_calls_Any_to_bool_0: ✅ pass (at line 18, col 4) Assertion failed at line 18, col 4: assert(356): ❌ fail ite_cond_calls_Any_to_bool_0: ✅ pass (at line 20, col 0) -DETAIL: 40 passed, 3 failed, 0 inconclusive +DETAIL: 34 passed, 3 failed, 0 inconclusive RESULT: Failures found diff --git a/StrataTest/Languages/Python/expected_laurel/test_return_types.expected b/StrataTest/Languages/Python/expected_laurel/test_return_types.expected index b9a6c727c..8c66fddb4 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_return_types.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_return_types.expected @@ -22,13 +22,6 @@ PFloorDiv_body_calls_Int.SafeDiv_2: ✅ pass (in prelude file) PFloorDiv_body_calls_Int.SafeDiv_3: ✅ pass (in prelude file) PAnd_body_calls_Any_to_bool_0: ✅ pass (in prelude file) POr_body_calls_Any_to_bool_0: ✅ pass (in prelude file) -ret_type: ✅ pass (in prelude file) -ret_type: ✅ pass (in prelude file) -ret_pos: ✅ pass (in prelude file) -assert_name_is_foo: ✅ pass (in prelude file) -assert_opt_name_none_or_str: ✅ pass (in prelude file) -assert_opt_name_none_or_bar: ✅ pass (in prelude file) -ensures_maybe_except_none: ✅ pass (in prelude file) (get_number ensures) Return type constraint: ✅ pass (get_greeting ensures) Return type constraint: ✅ pass (get_flag ensures) Return type constraint: ✅ pass @@ -40,11 +33,11 @@ assert_assert(387)_calls_Any_to_bool_0: ✅ pass (at line 23, col 4) assert(387): ❓ unknown (at line 23, col 4) assert_assert(474)_calls_Any_to_bool_0: ✅ pass (at line 26, col 4) Assertion failed at line 26, col 4: assert(474): ❌ fail -(add requires) Type constraint of a: ✅ pass (at line 14, col 8) -(add requires) Type constraint of b: ✅ pass (at line 14, col 16) +callElimAssert_requires_0_3: ✅ pass +callElimAssert_requires_1_4: ✅ pass assert_assert(558)_calls_Any_to_bool_0: ✅ pass (at line 29, col 4) Assertion failed at line 29, col 4: assert(558): ❌ fail ite_cond_calls_Any_to_bool_0: ✅ pass (at line 31, col 0) -DETAIL: 40 passed, 3 failed, 1 inconclusive +DETAIL: 34 passed, 3 failed, 1 inconclusive RESULT: Failures found diff --git a/StrataTest/Languages/Python/expected_laurel/test_while_loop.expected b/StrataTest/Languages/Python/expected_laurel/test_while_loop.expected index f785d3883..01ea9b4e4 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_while_loop.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_while_loop.expected @@ -47,5 +47,5 @@ assert_assert(589)_calls_Any_to_bool_0: ✅ pass (at line 27, col 4) assert(589): ❓ unknown (at line 27, col 4) (test_while_with_continue ensures) Return type constraint: ❓ unknown -DETAIL: 45 passed, 2 failed, 5 inconclusive +DETAIL: 39 passed, 2 failed, 5 inconclusive RESULT: Failures found diff --git a/StrataTest/Languages/Python/expected_laurel/test_with_statement.expected b/StrataTest/Languages/Python/expected_laurel/test_with_statement.expected index 2fa14c856..5a5033895 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_with_statement.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_with_statement.expected @@ -32,5 +32,5 @@ assert_assert(666)_calls_Any_to_bool_0: ✅ pass (at line 32, col 8) assert(666): ❓ unknown (at line 32, col 8) postcondition: ✅ pass (at line 27, col 0) -DETAIL: 34 passed, 2 failed, 1 inconclusive +DETAIL: 28 passed, 2 failed, 1 inconclusive RESULT: Failures found From f6266267a2fbc256ee98cb8ba422d69f93eae5c4 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Thu, 26 Mar 2026 14:27:06 -0700 Subject: [PATCH 20/31] remove return type check for None type (temporary) --- Strata/Languages/Python/PythonToLaurel.lean | 1 + .../Python/expected_laurel/test_break_continue.expected | 8 ++------ .../test_func_input_type_constraints.expected | 2 ++ .../Python/expected_laurel/test_return_types.expected | 3 +-- 4 files changed, 6 insertions(+), 8 deletions(-) diff --git a/Strata/Languages/Python/PythonToLaurel.lean b/Strata/Languages/Python/PythonToLaurel.lean index ab7f062fe..11f6154c2 100644 --- a/Strata/Languages/Python/PythonToLaurel.lean +++ b/Strata/Languages/Python/PythonToLaurel.lean @@ -1421,6 +1421,7 @@ def getUnionTypeConstraint (var: String) (md: MetaData) (tys: List String) (func some {createBoolOrExpr type_constraints with md:=md} def getReturnTypeEnsure (md: MetaData) (tys: List String) (funcname: String): Option StmtExprMd := + let tys := tys.filter (λ ty => ty ≠ "None") let type_constraints := tys.filterMap (getSingleTypeConstraint PyLauFuncReturnVar) if type_constraints.isEmpty then none else let md: MetaData := md.withPropertySummary $ "(" ++ funcname ++ " ensures) Return type constraint" diff --git a/StrataTest/Languages/Python/expected_laurel/test_break_continue.expected b/StrataTest/Languages/Python/expected_laurel/test_break_continue.expected index 3faeac68f..dc0be46ba 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_break_continue.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_break_continue.expected @@ -23,12 +23,8 @@ PFloorDiv_body_calls_Int.SafeDiv_3: ✅ pass (in prelude file) PAnd_body_calls_Any_to_bool_0: ✅ pass (in prelude file) POr_body_calls_Any_to_bool_0: ✅ pass (in prelude file) loop_guard_calls_Any_to_bool_0: ✅ pass (at line 3, col 4) -(test_while_break ensures) Return type constraint: ❌ fail loop_guard_calls_Any_to_bool_0: ✅ pass (at line 8, col 4) loop_guard_end_calls_Any_to_bool_0: ✅ pass (at line 8, col 4) -(test_while_continue ensures) Return type constraint: ❓ unknown -(test_for_break ensures) Return type constraint: ❌ fail -(test_for_continue ensures) Return type constraint: ❌ fail -DETAIL: 25 passed, 3 failed, 1 inconclusive -RESULT: Failures found +DETAIL: 25 passed, 0 failed, 0 inconclusive +RESULT: Analysis success diff --git a/StrataTest/Languages/Python/expected_laurel/test_func_input_type_constraints.expected b/StrataTest/Languages/Python/expected_laurel/test_func_input_type_constraints.expected index 6879251c3..46afcb595 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_func_input_type_constraints.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_func_input_type_constraints.expected @@ -1,3 +1,5 @@ +⚠️ [addPathCondition] Label clash detected for requires_0, using unique label requires_0_1. +⚠️ [addPathCondition] Label clash detected for requires_1, using unique label requires_1_1. ==== Verification Results ==== List_get_body_calls_List_get_0: ✅ pass (in prelude file) diff --git a/StrataTest/Languages/Python/expected_laurel/test_return_types.expected b/StrataTest/Languages/Python/expected_laurel/test_return_types.expected index 8c66fddb4..df21219ec 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_return_types.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_return_types.expected @@ -25,7 +25,6 @@ POr_body_calls_Any_to_bool_0: ✅ pass (in prelude file) (get_number ensures) Return type constraint: ✅ pass (get_greeting ensures) Return type constraint: ✅ pass (get_flag ensures) Return type constraint: ✅ pass -(get_nothing ensures) Return type constraint: ✅ pass (add ensures) Return type constraint: ✅ pass assert_assert(304)_calls_Any_to_bool_0: ✅ pass (at line 20, col 4) Assertion failed at line 20, col 4: assert(304): ❌ fail @@ -39,5 +38,5 @@ assert_assert(558)_calls_Any_to_bool_0: ✅ pass (at line 29, col 4) Assertion failed at line 29, col 4: assert(558): ❌ fail ite_cond_calls_Any_to_bool_0: ✅ pass (at line 31, col 0) -DETAIL: 34 passed, 3 failed, 1 inconclusive +DETAIL: 33 passed, 3 failed, 1 inconclusive RESULT: Failures found From 86da7eab19a256ba7f76b3c1a3fb3d7f5e051ba2 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Thu, 26 Mar 2026 14:33:06 -0700 Subject: [PATCH 21/31] fix expected test --- .../expected_laurel/test_func_input_type_constraints.expected | 2 -- 1 file changed, 2 deletions(-) diff --git a/StrataTest/Languages/Python/expected_laurel/test_func_input_type_constraints.expected b/StrataTest/Languages/Python/expected_laurel/test_func_input_type_constraints.expected index 46afcb595..6879251c3 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_func_input_type_constraints.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_func_input_type_constraints.expected @@ -1,5 +1,3 @@ -⚠️ [addPathCondition] Label clash detected for requires_0, using unique label requires_0_1. -⚠️ [addPathCondition] Label clash detected for requires_1, using unique label requires_1_1. ==== Verification Results ==== List_get_body_calls_List_get_0: ✅ pass (in prelude file) From 8fa67fdb4e4bd17fb8a1e1a2e80b792bb6326c91 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Fri, 27 Mar 2026 09:41:53 -0700 Subject: [PATCH 22/31] merge conflict --- Strata/Languages/Python/PythonToLaurel.lean | 10 +--- .../expected_laurel/test_class_decl.expected | 4 +- .../test_class_field_init.expected | 6 +-- .../test_class_field_use.expected | 9 ++-- .../test_class_methods.expected | 4 +- .../test_class_with_methods.expected | 4 +- .../test_default_params.expected | 4 +- .../expected_laurel/test_if_elif.expected | 3 -- .../expected_laurel/test_pin_any.expected | 52 +++++++++---------- .../expected_laurel/test_while_loop.expected | 7 +-- .../test_with_statement.expected | 14 ++--- 11 files changed, 49 insertions(+), 68 deletions(-) diff --git a/Strata/Languages/Python/PythonToLaurel.lean b/Strata/Languages/Python/PythonToLaurel.lean index a88587c35..c7e92fe79 100644 --- a/Strata/Languages/Python/PythonToLaurel.lean +++ b/Strata/Languages/Python/PythonToLaurel.lean @@ -1331,10 +1331,6 @@ def getUnionTypes (arg: Python.expr SourceRange) : List (Python.expr SourceRange def isOfAnyType (ty: String): Bool := ty ∈ ["None", "bool", "int", "str", "float", "datetime", "ListAny", "DictStrAny", "Any"] -def isCompositeType (ctx : TranslationContext) (ty: String) : Bool := match ctx.importedSymbols[ty]? with - | some (ImportedSymbol.compositeType _) => true - | _ => false - def checkValidTypeList (ctx : TranslationContext) (tys: List String) : Except TranslationError (List String) := do for ty in tys do if ¬ (isOfAnyType ty || isCompositeType ctx ty) then @@ -1420,7 +1416,7 @@ def pyFuncDefToPythonFunctionDecl (ctx : TranslationContext) (f : Python.stmt S match f with | .FunctionDef _ name args _body _decorator_list returns _type_comment _ => let name := match ctx.currentClassName with | none => name.val | some classname => classname ++ "@" ++ name.val - let args_trans ← unpackPyArguments args + let args_trans ← unpackPyArguments ctx args let args := if ctx.currentClassName.isSome then args_trans.fst.tail else args_trans.fst let retMd := sourceRangeToMetaData ctx.filePath returns.ann let ret ← if name.endsWith "@__init__" then pure $ some ([(name.dropEnd "@__init__".length).toString], retMd) @@ -1877,11 +1873,9 @@ def pythonToLaurel' (info : PreludeInfo) let mut compositeTypeNames := info.compositeTypes.union overloadCompositeType -- FIRST PASS: Collect all class definitions and field type info - let mut compositeTypes : List CompositeType := [pyErrorTy] - compositeTypeNames := compositeTypeNames.insert "PythonError" let mut procedures : Array Procedure := #[] let mut compositeTypes : Array TypeDefinition := #[.Composite pyErrorTy] - let mut compositeTypeNames := info.compositeTypes.insert "PythonError" + compositeTypeNames := compositeTypeNames.insert "PythonError" let mut classFieldHighType : Std.HashMap String (Std.HashMap String HighType) := {} for stmt in body do match stmt with diff --git a/StrataTest/Languages/Python/expected_laurel/test_class_decl.expected b/StrataTest/Languages/Python/expected_laurel/test_class_decl.expected index bf7f0ed01..b664c6df3 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_class_decl.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_class_decl.expected @@ -22,9 +22,9 @@ PFloorDiv_body_calls_Int.SafeDiv_2: ✅ pass (in prelude file) PFloorDiv_body_calls_Int.SafeDiv_3: ✅ pass (in prelude file) PAnd_body_calls_Any_to_bool_0: ✅ pass (in prelude file) POr_body_calls_Any_to_bool_0: ✅ pass (in prelude file) -postcondition: ✅ pass (at line 8, col 0) callElimAssert_requires_5: ✅ pass +postcondition: ✅ pass (at line 8, col 0) ite_cond_calls_Any_to_bool_0: ✅ pass (at line 13, col 0) -DETAIL: 24 passed, 0 failed, 0 inconclusive +DETAIL: 25 passed, 0 failed, 0 inconclusive RESULT: Analysis success diff --git a/StrataTest/Languages/Python/expected_laurel/test_class_field_init.expected b/StrataTest/Languages/Python/expected_laurel/test_class_field_init.expected index d11d69237..cc2879a4e 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_class_field_init.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_class_field_init.expected @@ -22,9 +22,9 @@ PFloorDiv_body_calls_Int.SafeDiv_2: ✅ pass (in prelude file) PFloorDiv_body_calls_Int.SafeDiv_3: ✅ pass (in prelude file) PAnd_body_calls_Any_to_bool_0: ✅ pass (in prelude file) POr_body_calls_Any_to_bool_0: ✅ pass (in prelude file) -postcondition: ✅ pass (at line 9, col 0) callElimAssert_requires_7: ✅ pass +Assertion failed at line 9, col 0: postcondition: ❌ fail ite_cond_calls_Any_to_bool_0: ✅ pass (at line 13, col 0) -DETAIL: 24 passed, 0 failed, 0 inconclusive -RESULT: Analysis success +DETAIL: 24 passed, 1 failed, 0 inconclusive +RESULT: Failures found diff --git a/StrataTest/Languages/Python/expected_laurel/test_class_field_use.expected b/StrataTest/Languages/Python/expected_laurel/test_class_field_use.expected index e8e67e1f6..346c33755 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_class_field_use.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_class_field_use.expected @@ -22,12 +22,11 @@ PFloorDiv_body_calls_Int.SafeDiv_2: ✅ pass (in prelude file) PFloorDiv_body_calls_Int.SafeDiv_3: ✅ pass (in prelude file) PAnd_body_calls_Any_to_bool_0: ✅ pass (in prelude file) POr_body_calls_Any_to_bool_0: ✅ pass (in prelude file) -callElimAssert_requires_10: ✅ pass +callElimAssert_requires_11: ✅ pass assert_assert(285)_calls_Any_to_bool_0: ✅ pass (at line 14, col 4) Assertion failed at line 14, col 4: assert(285): ❌ fail -postcondition: ✅ pass (at line 11, col 0) -(process_buffer ensures) Return type constraint: ✅ pass +Assertion failed at line 11, col 0: postcondition: ❌ fail +(process_buffer ensures) Return type constraint: ❓ unknown -DETAIL: 25 passed, 1 failed, 0 inconclusive -DETAIL: 24 passed, 1 failed, 0 inconclusive +DETAIL: 24 passed, 2 failed, 1 inconclusive RESULT: Failures found diff --git a/StrataTest/Languages/Python/expected_laurel/test_class_methods.expected b/StrataTest/Languages/Python/expected_laurel/test_class_methods.expected index 968f73cc7..afeb8febd 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_class_methods.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_class_methods.expected @@ -32,8 +32,8 @@ Assertion failed at line 28, col 4: assert(654): ❌ fail callElimAssert_req_name_is_foo_4: ✅ pass (at line 30, col 4) callElimAssert_req_opt_name_none_or_str_5: ✅ pass (at line 30, col 4) callElimAssert_req_opt_name_none_or_bar_6: ✅ pass (at line 30, col 4) -postcondition: ✅ pass (at line 17, col 0) +Assertion failed at line 17, col 0: postcondition: ❌ fail ite_cond_calls_Any_to_bool_0: ✅ pass (at line 32, col 0) -DETAIL: 30 passed, 2 failed, 1 inconclusive +DETAIL: 30 passed, 3 failed, 1 inconclusive RESULT: Failures found diff --git a/StrataTest/Languages/Python/expected_laurel/test_class_with_methods.expected b/StrataTest/Languages/Python/expected_laurel/test_class_with_methods.expected index 2759f4313..5e1025659 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_class_with_methods.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_class_with_methods.expected @@ -30,8 +30,8 @@ assert(544): ❓ unknown (at line 26, col 4) callElimAssert_req_name_is_foo_4: ✅ pass (at line 28, col 4) callElimAssert_req_opt_name_none_or_str_5: ✅ pass (at line 28, col 4) callElimAssert_req_opt_name_none_or_bar_6: ✅ pass (at line 28, col 4) -postcondition: ✅ pass (at line 17, col 0) +Assertion failed at line 17, col 0: postcondition: ❌ fail ite_cond_calls_Any_to_bool_0: ✅ pass (at line 30, col 0) -DETAIL: 29 passed, 1 failed, 1 inconclusive +DETAIL: 29 passed, 2 failed, 1 inconclusive RESULT: Failures found diff --git a/StrataTest/Languages/Python/expected_laurel/test_default_params.expected b/StrataTest/Languages/Python/expected_laurel/test_default_params.expected index 179ecaf7f..cde7c0a7d 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_default_params.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_default_params.expected @@ -25,7 +25,7 @@ POr_body_calls_Any_to_bool_0: ✅ pass (in prelude file) (greet ensures) Return type constraint: ✅ pass loop_guard_calls_Any_to_bool_0: ✅ pass (at line 8, col 4) loop_guard_end_calls_Any_to_bool_0: ✅ pass (at line 8, col 4) -(power ensures) Return type constraint: ❌ fail +(power ensures) Return type constraint: ❓ unknown callElimAssert_requires_0_21: ✅ pass callElimAssert_requires_1_22: ✅ pass assert_assert(325)_calls_Any_to_bool_0: ✅ pass (at line 15, col 4) @@ -44,5 +44,5 @@ assert_assert(571)_calls_Any_to_bool_0: ✅ pass (at line 24, col 4) Assertion failed at line 24, col 4: assert(571): ❌ fail ite_cond_calls_Any_to_bool_0: ✅ pass (at line 26, col 0) -DETAIL: 38 passed, 3 failed, 2 inconclusive +DETAIL: 38 passed, 2 failed, 3 inconclusive RESULT: Failures found diff --git a/StrataTest/Languages/Python/expected_laurel/test_if_elif.expected b/StrataTest/Languages/Python/expected_laurel/test_if_elif.expected index f0407e895..21260eed8 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_if_elif.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_if_elif.expected @@ -30,7 +30,6 @@ ite_cond_calls_Any_to_bool_0: ✅ pass (at line 6, col 4) (classify ensures) Return type constraint: ✅ pass (classify ensures) Return type constraint: ✅ pass callElimAssert_requires_14: ✅ pass -ite_cond_calls_Any_to_bool_0: ❓ unknown (at line 6, col 4) assert_assert(225)_calls_Any_to_bool_0: ✅ pass (at line 13, col 4) assert(225): ❓ unknown (at line 13, col 4) callElimAssert_requires_10: ✅ pass @@ -46,5 +45,3 @@ ite_cond_calls_Any_to_bool_0: ✅ pass (at line 24, col 0) DETAIL: 38 passed, 0 failed, 4 inconclusive RESULT: Inconclusive -DETAIL: 28 passed, 1 failed, 5 inconclusive -RESULT: Failures found diff --git a/StrataTest/Languages/Python/expected_laurel/test_pin_any.expected b/StrataTest/Languages/Python/expected_laurel/test_pin_any.expected index 8a3a353e1..d0ad11d82 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_pin_any.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_pin_any.expected @@ -1,31 +1,31 @@ ==== Verification Results ==== -List_get_body_calls_List_get_0: ✔️ always true if reached (in prelude file) -List_take_body_calls_List_take_0: ✔️ always true if reached (in prelude file) -List_drop_body_calls_List_drop_0: ✔️ always true if reached (in prelude file) -List_slice_body_calls_List_drop_0: ✔️ always true if reached (in prelude file) -List_slice_body_calls_List_take_1: ✔️ always true if reached (in prelude file) -List_set_body_calls_List_set_0: ✔️ always true if reached (in prelude file) -DictStrAny_get_body_calls_DictStrAny_get_0: ✔️ always true if reached (in prelude file) -DictStrAny_get_or_none_body_calls_DictStrAny_get_0: ✔️ always true if reached (in prelude file) -Any_get_body_calls_DictStrAny_get_0: ✔️ always true if reached (in prelude file) -Any_get_body_calls_List_get_1: ✔️ always true if reached (in prelude file) -Any_get_body_calls_List_slice_2: ✔️ always true if reached (in prelude file) -Any_get_body_calls_List_drop_3: ✔️ always true if reached (in prelude file) -Any_get!_body_calls_DictStrAny_get_0: ✔️ always true if reached (in prelude file) -Any_get!_body_calls_List_get_1: ✔️ always true if reached (in prelude file) -Any_set_body_calls_List_set_0: ✔️ always true if reached (in prelude file) -Any_set!_body_calls_List_set_0: ✔️ always true if reached (in prelude file) -PFloorDiv_body_calls_Int.SafeDiv_0: ✅ always true and is reachable from declaration entry (in prelude file) -PFloorDiv_body_calls_Int.SafeDiv_1: ✅ always true and is reachable from declaration entry (in prelude file) -PFloorDiv_body_calls_Int.SafeDiv_2: ✅ always true and is reachable from declaration entry (in prelude file) -PFloorDiv_body_calls_Int.SafeDiv_3: ✅ always true and is reachable from declaration entry (in prelude file) -PAnd_body_calls_Any_to_bool_0: ✅ always true and is reachable from declaration entry (in prelude file) -POr_body_calls_Any_to_bool_0: ✅ always true and is reachable from declaration entry (in prelude file) -ite_cond_calls_Any_to_bool_0: 🔶 can be both true and false and is reachable from declaration entry (at line 3, col 4) +List_get_body_calls_List_get_0: ✅ pass (in prelude file) +List_take_body_calls_List_take_0: ✅ pass (in prelude file) +List_drop_body_calls_List_drop_0: ✅ pass (in prelude file) +List_slice_body_calls_List_drop_0: ✅ pass (in prelude file) +List_slice_body_calls_List_take_1: ✅ pass (in prelude file) +List_set_body_calls_List_set_0: ✅ pass (in prelude file) +DictStrAny_get_body_calls_DictStrAny_get_0: ✅ pass (in prelude file) +DictStrAny_get_or_none_body_calls_DictStrAny_get_0: ✅ pass (in prelude file) +Any_get_body_calls_DictStrAny_get_0: ✅ pass (in prelude file) +Any_get_body_calls_List_get_1: ✅ pass (in prelude file) +Any_get_body_calls_List_slice_2: ✅ pass (in prelude file) +Any_get_body_calls_List_drop_3: ✅ pass (in prelude file) +Any_get!_body_calls_DictStrAny_get_0: ✅ pass (in prelude file) +Any_get!_body_calls_List_get_1: ✅ pass (in prelude file) +Any_set_body_calls_List_set_0: ✅ pass (in prelude file) +Any_set!_body_calls_List_set_0: ✅ pass (in prelude file) +PFloorDiv_body_calls_Int.SafeDiv_0: ✅ pass (in prelude file) +PFloorDiv_body_calls_Int.SafeDiv_1: ✅ pass (in prelude file) +PFloorDiv_body_calls_Int.SafeDiv_2: ✅ pass (in prelude file) +PFloorDiv_body_calls_Int.SafeDiv_3: ✅ pass (in prelude file) +PAnd_body_calls_Any_to_bool_0: ✅ pass (in prelude file) +POr_body_calls_Any_to_bool_0: ✅ pass (in prelude file) +Assertion failed at line 3, col 4: ite_cond_calls_Any_to_bool_0: ❌ fail assert_assert(124)_calls_PIn_0: ❓ unknown (at line 4, col 8) -assert_assert(124)_calls_Any_to_bool_1: ✔️ always true if reached (at line 4, col 8) +assert_assert(124)_calls_Any_to_bool_1: ✅ pass (at line 4, col 8) assert(124): ❓ unknown (at line 4, col 8) -DETAIL: 23 passed, 0 failed, 3 inconclusive -RESULT: Inconclusive +DETAIL: 23 passed, 1 failed, 2 inconclusive +RESULT: Failures found diff --git a/StrataTest/Languages/Python/expected_laurel/test_while_loop.expected b/StrataTest/Languages/Python/expected_laurel/test_while_loop.expected index 4c98cee02..fed204b4d 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_while_loop.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_while_loop.expected @@ -25,9 +25,8 @@ POr_body_calls_Any_to_bool_0: ✅ pass (in prelude file) loop_guard_calls_Any_to_bool_0: ✅ pass (at line 4, col 4) loop_guard_end_calls_Any_to_bool_0: ✅ pass (at line 4, col 4) assert_assert(134)_calls_Any_to_bool_0: ✅ pass (at line 7, col 4) -Assertion failed at line 7, col 4: assert(134): ❌ fail -(test_while_countdown ensures) Return type constraint: ❌ fail assert(134): ❓ unknown (at line 7, col 4) +(test_while_countdown ensures) Return type constraint: ❓ unknown loop_guard_calls_Any_to_bool_0: ✅ pass (at line 12, col 4) ite_cond_calls_Any_to_bool_0: ✅ pass (at line 14, col 8) assert_assert(344)_calls_Any_to_bool_0: ✅ pass (at line 16, col 4) @@ -48,7 +47,5 @@ assert_assert(589)_calls_Any_to_bool_0: ✅ pass (at line 27, col 4) assert(589): ❓ unknown (at line 27, col 4) (test_while_with_continue ensures) Return type constraint: ❓ unknown -DETAIL: 39 passed, 2 failed, 5 inconclusive -RESULT: Failures found -DETAIL: 38 passed, 0 failed, 3 inconclusive +DETAIL: 39 passed, 0 failed, 7 inconclusive RESULT: Inconclusive diff --git a/StrataTest/Languages/Python/expected_laurel/test_with_statement.expected b/StrataTest/Languages/Python/expected_laurel/test_with_statement.expected index 491e11bce..19d429206 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_with_statement.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_with_statement.expected @@ -27,20 +27,13 @@ callElimAssert_requires_6: ✅ pass callElimAssert_requires_2: ✅ pass assert_assert(368)_calls_Any_to_bool_0: ✅ pass (at line 19, col 4) Assertion failed at line 19, col 4: assert(368): ❌ fail -postcondition: ✅ pass (at line 14, col 0) -assert_assert(500)_calls_Any_to_bool_0: ✅ pass (at line 25, col 8) -Assertion failed at line 25, col 8: assert(500): ❌ fail -postcondition: ✅ pass (at line 21, col 0) -assert_assert(666)_calls_Any_to_bool_0: ✅ pass (at line 32, col 8) -assert(666): ❓ unknown (at line 32, col 8) -postcondition: ✅ pass (at line 27, col 0) - -DETAIL: 28 passed, 2 failed, 1 inconclusive +Assertion failed at line 14, col 0: postcondition: ❌ fail callElimAssert_requires_25: ✅ pass callElimAssert_requires_19: ✅ pass assert_assert(500)_calls_Any_to_bool_0: ✅ pass (at line 25, col 8) Assertion failed at line 25, col 8: assert(500): ❌ fail callElimAssert_requires_15: ✅ pass +Assertion failed at line 21, col 0: postcondition: ❌ fail callElimAssert_requires_51: ✅ pass callElimAssert_requires_45: ✅ pass callElimAssert_requires_39: ✅ pass @@ -49,6 +42,7 @@ assert_assert(666)_calls_Any_to_bool_0: ✅ pass (at line 32, col 8) assert(666): ❓ unknown (at line 32, col 8) callElimAssert_requires_31: ✅ pass callElimAssert_requires_28: ✅ pass +Assertion failed at line 27, col 0: postcondition: ❌ fail -DETAIL: 37 passed, 2 failed, 1 inconclusive +DETAIL: 37 passed, 5 failed, 1 inconclusive RESULT: Failures found From 22cc2767ddc1239e88188216c08ff0f257c8fb79 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Fri, 27 Mar 2026 10:03:39 -0700 Subject: [PATCH 23/31] fix expected test --- .../expected_laurel/test_pin_any.expected | 52 +++++++++---------- 1 file changed, 26 insertions(+), 26 deletions(-) diff --git a/StrataTest/Languages/Python/expected_laurel/test_pin_any.expected b/StrataTest/Languages/Python/expected_laurel/test_pin_any.expected index d0ad11d82..8a3a353e1 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_pin_any.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_pin_any.expected @@ -1,31 +1,31 @@ ==== Verification Results ==== -List_get_body_calls_List_get_0: ✅ pass (in prelude file) -List_take_body_calls_List_take_0: ✅ pass (in prelude file) -List_drop_body_calls_List_drop_0: ✅ pass (in prelude file) -List_slice_body_calls_List_drop_0: ✅ pass (in prelude file) -List_slice_body_calls_List_take_1: ✅ pass (in prelude file) -List_set_body_calls_List_set_0: ✅ pass (in prelude file) -DictStrAny_get_body_calls_DictStrAny_get_0: ✅ pass (in prelude file) -DictStrAny_get_or_none_body_calls_DictStrAny_get_0: ✅ pass (in prelude file) -Any_get_body_calls_DictStrAny_get_0: ✅ pass (in prelude file) -Any_get_body_calls_List_get_1: ✅ pass (in prelude file) -Any_get_body_calls_List_slice_2: ✅ pass (in prelude file) -Any_get_body_calls_List_drop_3: ✅ pass (in prelude file) -Any_get!_body_calls_DictStrAny_get_0: ✅ pass (in prelude file) -Any_get!_body_calls_List_get_1: ✅ pass (in prelude file) -Any_set_body_calls_List_set_0: ✅ pass (in prelude file) -Any_set!_body_calls_List_set_0: ✅ pass (in prelude file) -PFloorDiv_body_calls_Int.SafeDiv_0: ✅ pass (in prelude file) -PFloorDiv_body_calls_Int.SafeDiv_1: ✅ pass (in prelude file) -PFloorDiv_body_calls_Int.SafeDiv_2: ✅ pass (in prelude file) -PFloorDiv_body_calls_Int.SafeDiv_3: ✅ pass (in prelude file) -PAnd_body_calls_Any_to_bool_0: ✅ pass (in prelude file) -POr_body_calls_Any_to_bool_0: ✅ pass (in prelude file) -Assertion failed at line 3, col 4: ite_cond_calls_Any_to_bool_0: ❌ fail +List_get_body_calls_List_get_0: ✔️ always true if reached (in prelude file) +List_take_body_calls_List_take_0: ✔️ always true if reached (in prelude file) +List_drop_body_calls_List_drop_0: ✔️ always true if reached (in prelude file) +List_slice_body_calls_List_drop_0: ✔️ always true if reached (in prelude file) +List_slice_body_calls_List_take_1: ✔️ always true if reached (in prelude file) +List_set_body_calls_List_set_0: ✔️ always true if reached (in prelude file) +DictStrAny_get_body_calls_DictStrAny_get_0: ✔️ always true if reached (in prelude file) +DictStrAny_get_or_none_body_calls_DictStrAny_get_0: ✔️ always true if reached (in prelude file) +Any_get_body_calls_DictStrAny_get_0: ✔️ always true if reached (in prelude file) +Any_get_body_calls_List_get_1: ✔️ always true if reached (in prelude file) +Any_get_body_calls_List_slice_2: ✔️ always true if reached (in prelude file) +Any_get_body_calls_List_drop_3: ✔️ always true if reached (in prelude file) +Any_get!_body_calls_DictStrAny_get_0: ✔️ always true if reached (in prelude file) +Any_get!_body_calls_List_get_1: ✔️ always true if reached (in prelude file) +Any_set_body_calls_List_set_0: ✔️ always true if reached (in prelude file) +Any_set!_body_calls_List_set_0: ✔️ always true if reached (in prelude file) +PFloorDiv_body_calls_Int.SafeDiv_0: ✅ always true and is reachable from declaration entry (in prelude file) +PFloorDiv_body_calls_Int.SafeDiv_1: ✅ always true and is reachable from declaration entry (in prelude file) +PFloorDiv_body_calls_Int.SafeDiv_2: ✅ always true and is reachable from declaration entry (in prelude file) +PFloorDiv_body_calls_Int.SafeDiv_3: ✅ always true and is reachable from declaration entry (in prelude file) +PAnd_body_calls_Any_to_bool_0: ✅ always true and is reachable from declaration entry (in prelude file) +POr_body_calls_Any_to_bool_0: ✅ always true and is reachable from declaration entry (in prelude file) +ite_cond_calls_Any_to_bool_0: 🔶 can be both true and false and is reachable from declaration entry (at line 3, col 4) assert_assert(124)_calls_PIn_0: ❓ unknown (at line 4, col 8) -assert_assert(124)_calls_Any_to_bool_1: ✅ pass (at line 4, col 8) +assert_assert(124)_calls_Any_to_bool_1: ✔️ always true if reached (at line 4, col 8) assert(124): ❓ unknown (at line 4, col 8) -DETAIL: 23 passed, 1 failed, 2 inconclusive -RESULT: Failures found +DETAIL: 23 passed, 0 failed, 3 inconclusive +RESULT: Inconclusive From 58a0f09b05217eaace32b9a7982acd58ad1735a3 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Fri, 27 Mar 2026 10:22:08 -0700 Subject: [PATCH 24/31] fix validType checking --- Strata/Languages/Python/PythonToLaurel.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Strata/Languages/Python/PythonToLaurel.lean b/Strata/Languages/Python/PythonToLaurel.lean index c7e92fe79..5640b82a7 100644 --- a/Strata/Languages/Python/PythonToLaurel.lean +++ b/Strata/Languages/Python/PythonToLaurel.lean @@ -227,6 +227,7 @@ def pythonTypeToCoreType (typeStr : String) : Option String := | "Dict[str, Any]" => some PyLauType.DictStrAny | "List[str]" => some PyLauType.ListStr | "Any" => some PyLauType.Any + | "None" => some PyLauType.Any | "datetime" => some PyLauType.Datetime | "timedelta" => some PyLauType.Int | _ => none @@ -1333,8 +1334,7 @@ def isOfAnyType (ty: String): Bool := ty ∈ ["None", "bool", "int", "str", "flo def checkValidTypeList (ctx : TranslationContext) (tys: List String) : Except TranslationError (List String) := do for ty in tys do - if ¬ (isOfAnyType ty || isCompositeType ctx ty) then - throw (.userPythonError .none s!"'{ty}' is not a type") + let _ ← translateType ctx ty if tys.length > 1 && tys.any (isCompositeType ctx) then throw (.unsupportedConstruct "Argument of union of class types is not supported" (toString tys)) return tys From 635dc20ff2d2e5350bfe12ef7e78fd59e0e6f6e3 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Mon, 30 Mar 2026 11:00:21 -0700 Subject: [PATCH 25/31] fix expected file + rename Option constructors to avoid confict with Python None --- .../Python/PythonLaurelCorePrelude.lean | 10 ++++---- .../Python/PythonRuntimeLaurelPart.lean | 4 ++-- Strata/Languages/Python/PythonToLaurel.lean | 12 +++------- .../expected_laurel/test_class_decl.expected | 2 +- .../test_class_field_init.expected | 4 ++-- .../test_class_field_use.expected | 4 ++-- .../test_class_methods.expected | 2 +- .../test_class_with_methods.expected | 2 +- .../test_default_params.expected | 5 ++-- .../test_func_input_type_constraints.expected | 24 +------------------ .../test_func_type_constraint.expected | 0 .../test_function_def_calls.expected | 2 +- .../expected_laurel/test_if_elif.expected | 7 +++--- .../test_multi_function.expected | 5 ++-- .../test_nested_calls.expected | 6 ++++- .../test_return_types.expected | 6 ++++- .../expected_laurel/test_while_loop.expected | 2 +- .../test_with_statement.expected | 2 +- 18 files changed, 41 insertions(+), 58 deletions(-) delete mode 100644 StrataTest/Languages/Python/expected_laurel/test_func_type_constraint.expected diff --git a/Strata/Languages/Python/PythonLaurelCorePrelude.lean b/Strata/Languages/Python/PythonLaurelCorePrelude.lean index 952b04f07..e73e602d0 100644 --- a/Strata/Languages/Python/PythonLaurelCorePrelude.lean +++ b/Strata/Languages/Python/PythonLaurelCorePrelude.lean @@ -68,8 +68,8 @@ datatype Error () { // that the conversion from a string constant is handled by the translator. datatype OptionInt { - Some (unwrap: int), - None () + OptSome (unwrap: int), + OptNone () } datatype Any () { @@ -412,14 +412,14 @@ inline function Any_get (dictOrList: Any, index: Any): Any requires (Any..isfrom_Dict(dictOrList) && Any..isfrom_string(index) && DictStrAny_contains(Any..as_Dict!(dictOrList), Any..as_string!(index))) || (Any..isfrom_ListAny(dictOrList) && Any..isfrom_int(index) && Any..as_int!(index) >= 0 && Any..as_int!(index) < List_len(Any..as_ListAny!(dictOrList)))|| (Any..isfrom_ListAny(dictOrList) && Any..isfrom_Slice(index) && Any..start!(index) >= 0 && Any..start!(index) < List_len(Any..as_ListAny!(dictOrList)) && - ((OptionInt..isSome(Any..stop!(index))) && OptionInt..unwrap!(Any..stop!(index)) >= 0 && OptionInt..unwrap!(Any..stop!(index)) <= List_len(Any..as_ListAny!(dictOrList)) && Any..start!(index) <= OptionInt..unwrap!(Any..stop!(index)) - || (OptionInt..isNone(Any..stop!(index))))); + ((OptionInt..isOptSome(Any..stop!(index))) && OptionInt..unwrap!(Any..stop!(index)) >= 0 && OptionInt..unwrap!(Any..stop!(index)) <= List_len(Any..as_ListAny!(dictOrList)) && Any..start!(index) <= OptionInt..unwrap!(Any..stop!(index)) + || (OptionInt..isOptNone(Any..stop!(index))))); { if Any..isfrom_Dict(dictOrList) then DictStrAny_get(Any..as_Dict!(dictOrList), Any..as_string!(index)) else if Any..isfrom_ListAny(dictOrList) && Any..isfrom_int(index) then List_get(Any..as_ListAny!(dictOrList), Any..as_int!(index)) - else if Any..isfrom_ListAny(dictOrList) && Any..isfrom_Slice(index) && OptionInt..isSome(Any..stop!(index)) then + else if Any..isfrom_ListAny(dictOrList) && Any..isfrom_Slice(index) && OptionInt..isOptSome(Any..stop!(index)) then from_ListAny(List_slice(Any..as_ListAny!(dictOrList), Any..start!(index), OptionInt..unwrap!(Any..stop!(index)))) else from_ListAny(List_drop(Any..as_ListAny!(dictOrList), Any..start!(index))) diff --git a/Strata/Languages/Python/PythonRuntimeLaurelPart.lean b/Strata/Languages/Python/PythonRuntimeLaurelPart.lean index 9de71728c..56cf2af06 100644 --- a/Strata/Languages/Python/PythonRuntimeLaurelPart.lean +++ b/Strata/Languages/Python/PythonRuntimeLaurelPart.lean @@ -64,8 +64,8 @@ datatype Error { // Laurel does not support mutual blocks, so they are declared separately. datatype OptionInt { - Some (unwrap: int), - None () + OptSome (unwrap: int), + OptNone () } datatype Any { diff --git a/Strata/Languages/Python/PythonToLaurel.lean b/Strata/Languages/Python/PythonToLaurel.lean index 8184de632..574671855 100644 --- a/Strata/Languages/Python/PythonToLaurel.lean +++ b/Strata/Languages/Python/PythonToLaurel.lean @@ -307,7 +307,7 @@ def lookupFieldHighType (ctx : TranslationContext) (className fieldName : String | some ty => .ok ty def NoError : StmtExprMd := mkStmtExprMd (StmtExpr.StaticCall "NoError" []) -def optNone := mkStmtExprMd (StmtExpr.StaticCall "None" []) +def optNone := mkStmtExprMd (StmtExpr.StaticCall "OptNone" []) def getSubscriptList (expr: Python.expr SourceRange) : List ( Python.expr SourceRange) := match expr with @@ -415,7 +415,7 @@ partial def translateSlice (ctx : TranslationContext) (start stop step: Option ( let start ← translateExpr ctx start let stop ← translateExpr ctx stop let start := mkStmtExprMd (.StaticCall "Any..as_int!" [start]) - let stop := mkStmtExprMd (.StaticCall "Some" [mkStmtExprMd (.StaticCall "Any..as_int!" [stop])]) + let stop := mkStmtExprMd (.StaticCall "OptSome" [mkStmtExprMd (.StaticCall "Any..as_int!" [stop])]) return mkStmtExprMd (.StaticCall "from_Slice" [start, stop]) | some start, none => let start ← translateExpr ctx start @@ -424,7 +424,7 @@ partial def translateSlice (ctx : TranslationContext) (start stop step: Option ( | none, some stop => let start := mkStmtExprMd (.LiteralInt 0) let stop ← translateExpr ctx stop - let stop := mkStmtExprMd (.StaticCall "Some" [mkStmtExprMd (.StaticCall "Any..as_int!" [stop])]) + let stop := mkStmtExprMd (.StaticCall "OptSome" [mkStmtExprMd (.StaticCall "Any..as_int!" [stop])]) return mkStmtExprMd (.StaticCall "from_Slice" [start, stop]) | _ , _ => let start := mkStmtExprMd (.LiteralInt 0) @@ -1563,12 +1563,6 @@ def translateFunction (ctx : TranslationContext) (sourceRange: SourceRange) (fun -- Translate function body let inputTypes := funcDecl.args.map (λ arg => match arg.tys with | [ty] => (arg.name, ty) | _ => (arg.name, PyLauType.Any)) - let ctx := {ctx with variableTypes:= ("nullcall_ret", PyLauType.Any)::inputTypes} - let (newctx, bodyStmts) ← translateStmtList ctx body - let bodyStmts := prependExceptHandlingHelper bodyStmts - let bodyStmts := (mkStmtExprMd (.LocalVariable "nullcall_ret" AnyTy (some AnyNone))) :: bodyStmts - let bodyBlock := mkStmtExprMd (StmtExpr.Block bodyStmts none) - let inputTypes := funcDecl.args.map (λ (name, type, _) => (name, type)) let (bodyBlock, newCtx) ← translateFunctionBody ctx inputTypes body -- Create procedure with transparent body (no contracts for now) diff --git a/StrataTest/Languages/Python/expected_laurel/test_class_decl.expected b/StrataTest/Languages/Python/expected_laurel/test_class_decl.expected index cea3531f9..f55bcabc6 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_class_decl.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_class_decl.expected @@ -4,5 +4,5 @@ callElimAssert_requires_5: ✅ pass postcondition: ✅ pass (at line 8, col 0) ite_cond_calls_Any_to_bool_0: ✅ pass (at line 13, col 0) -DETAIL: 2 passed, 0 failed, 0 inconclusive +DETAIL: 3 passed, 0 failed, 0 inconclusive RESULT: Analysis success diff --git a/StrataTest/Languages/Python/expected_laurel/test_class_field_init.expected b/StrataTest/Languages/Python/expected_laurel/test_class_field_init.expected index 05cad802f..98a4202f1 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_class_field_init.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_class_field_init.expected @@ -4,5 +4,5 @@ callElimAssert_requires_7: ✅ pass Assertion failed at line 9, col 0: postcondition: ❌ fail ite_cond_calls_Any_to_bool_0: ✅ pass (at line 13, col 0) -DETAIL: 2 passed, 0 failed, 0 inconclusive -RESULT: Analysis success +DETAIL: 2 passed, 1 failed, 0 inconclusive +RESULT: Failures found diff --git a/StrataTest/Languages/Python/expected_laurel/test_class_field_use.expected b/StrataTest/Languages/Python/expected_laurel/test_class_field_use.expected index 90f8f487a..050884c00 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_class_field_use.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_class_field_use.expected @@ -1,10 +1,10 @@ ==== Verification Results ==== -callElimAssert_requires_10: ✅ pass +callElimAssert_requires_11: ✅ pass assert_assert(285)_calls_Any_to_bool_0: ✅ pass (at line 14, col 4) Assertion failed at line 14, col 4: assert(285): ❌ fail Assertion failed at line 11, col 0: postcondition: ❌ fail (process_buffer ensures) Return type constraint: ❓ unknown -DETAIL: 2 passed, 1 failed, 0 inconclusive +DETAIL: 2 passed, 2 failed, 1 inconclusive RESULT: Failures found diff --git a/StrataTest/Languages/Python/expected_laurel/test_class_methods.expected b/StrataTest/Languages/Python/expected_laurel/test_class_methods.expected index ee1671268..2123d4ead 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_class_methods.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_class_methods.expected @@ -13,5 +13,5 @@ callElimAssert_req_opt_name_none_or_bar_6: ✅ pass (at line 30, col 4) Assertion failed at line 17, col 0: postcondition: ❌ fail ite_cond_calls_Any_to_bool_0: ✅ pass (at line 32, col 0) -DETAIL: 8 passed, 2 failed, 1 inconclusive +DETAIL: 8 passed, 3 failed, 1 inconclusive RESULT: Failures found diff --git a/StrataTest/Languages/Python/expected_laurel/test_class_with_methods.expected b/StrataTest/Languages/Python/expected_laurel/test_class_with_methods.expected index 27d41b792..c307497b7 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_class_with_methods.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_class_with_methods.expected @@ -11,5 +11,5 @@ callElimAssert_req_opt_name_none_or_bar_6: ✅ pass (at line 28, col 4) Assertion failed at line 17, col 0: postcondition: ❌ fail ite_cond_calls_Any_to_bool_0: ✅ pass (at line 30, col 0) -DETAIL: 7 passed, 1 failed, 1 inconclusive +DETAIL: 7 passed, 2 failed, 1 inconclusive RESULT: Failures found diff --git a/StrataTest/Languages/Python/expected_laurel/test_default_params.expected b/StrataTest/Languages/Python/expected_laurel/test_default_params.expected index fc1c81c97..65da0107d 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_default_params.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_default_params.expected @@ -1,6 +1,7 @@ ==== Verification Results ==== -Assertion failed at line 8, col 4: loop_guard_calls_Any_to_bool_0: ❌ fail +(greet ensures) Return type constraint: ✅ pass +loop_guard_calls_Any_to_bool_0: ✅ pass (at line 8, col 4) loop_guard_end_calls_Any_to_bool_0: ✅ pass (at line 8, col 4) (power ensures) Return type constraint: ❓ unknown callElimAssert_requires_0_21: ✅ pass @@ -21,5 +22,5 @@ assert_assert(571)_calls_Any_to_bool_0: ✅ pass (at line 24, col 4) Assertion failed at line 24, col 4: assert(571): ❌ fail ite_cond_calls_Any_to_bool_0: ✅ pass (at line 26, col 0) -DETAIL: 6 passed, 3 failed, 2 inconclusive +DETAIL: 16 passed, 2 failed, 3 inconclusive RESULT: Failures found diff --git a/StrataTest/Languages/Python/expected_laurel/test_func_input_type_constraints.expected b/StrataTest/Languages/Python/expected_laurel/test_func_input_type_constraints.expected index 6879251c3..f91d20ced 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_func_input_type_constraints.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_func_input_type_constraints.expected @@ -1,27 +1,5 @@ ==== Verification Results ==== -List_get_body_calls_List_get_0: ✅ pass (in prelude file) -List_take_body_calls_List_take_0: ✅ pass (in prelude file) -List_drop_body_calls_List_drop_0: ✅ pass (in prelude file) -List_slice_body_calls_List_drop_0: ✅ pass (in prelude file) -List_slice_body_calls_List_take_1: ✅ pass (in prelude file) -List_set_body_calls_List_set_0: ✅ pass (in prelude file) -DictStrAny_get_body_calls_DictStrAny_get_0: ✅ pass (in prelude file) -DictStrAny_get_or_none_body_calls_DictStrAny_get_0: ✅ pass (in prelude file) -Any_get_body_calls_DictStrAny_get_0: ✅ pass (in prelude file) -Any_get_body_calls_List_get_1: ✅ pass (in prelude file) -Any_get_body_calls_List_slice_2: ✅ pass (in prelude file) -Any_get_body_calls_List_drop_3: ✅ pass (in prelude file) -Any_get!_body_calls_DictStrAny_get_0: ✅ pass (in prelude file) -Any_get!_body_calls_List_get_1: ✅ pass (in prelude file) -Any_set_body_calls_List_set_0: ✅ pass (in prelude file) -Any_set!_body_calls_List_set_0: ✅ pass (in prelude file) -PFloorDiv_body_calls_Int.SafeDiv_0: ✅ pass (in prelude file) -PFloorDiv_body_calls_Int.SafeDiv_1: ✅ pass (in prelude file) -PFloorDiv_body_calls_Int.SafeDiv_2: ✅ pass (in prelude file) -PFloorDiv_body_calls_Int.SafeDiv_3: ✅ pass (in prelude file) -PAnd_body_calls_Any_to_bool_0: ✅ pass (in prelude file) -POr_body_calls_Any_to_bool_0: ✅ pass (in prelude file) (Mul ensures) Return type constraint: ✅ pass ite_cond_calls_Any_to_bool_0: ✅ pass (at line 7, col 4) (Sum ensures) Return type constraint: ✅ pass @@ -37,5 +15,5 @@ callElimAssert_requires_0_4: ✅ pass callElimAssert_requires_1_5: ✅ pass callElimAssert_requires_2_6: ✅ pass -DETAIL: 33 passed, 0 failed, 3 inconclusive +DETAIL: 11 passed, 0 failed, 3 inconclusive RESULT: Inconclusive diff --git a/StrataTest/Languages/Python/expected_laurel/test_func_type_constraint.expected b/StrataTest/Languages/Python/expected_laurel/test_func_type_constraint.expected deleted file mode 100644 index e69de29bb..000000000 diff --git a/StrataTest/Languages/Python/expected_laurel/test_function_def_calls.expected b/StrataTest/Languages/Python/expected_laurel/test_function_def_calls.expected index ac585870c..fd1e89da7 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_function_def_calls.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_function_def_calls.expected @@ -6,5 +6,5 @@ callElimAssert_req_opt_name_none_or_bar_6: ✅ pass (at line 6, col 4) callElimAssert_requires_9: ✅ pass (at line 9, col 4) ite_cond_calls_Any_to_bool_0: ✅ pass (at line 11, col 0) -DETAIL: 3 passed, 0 failed, 1 inconclusive +DETAIL: 4 passed, 0 failed, 1 inconclusive RESULT: Inconclusive diff --git a/StrataTest/Languages/Python/expected_laurel/test_if_elif.expected b/StrataTest/Languages/Python/expected_laurel/test_if_elif.expected index 8ef0b5061..2fc2c7a7d 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_if_elif.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_if_elif.expected @@ -1,6 +1,7 @@ ==== Verification Results ==== -Assertion failed at line 2, col 4: ite_cond_calls_Any_to_bool_0: ❌ fail +ite_cond_calls_Any_to_bool_0: ✅ pass (at line 2, col 4) +(classify ensures) Return type constraint: ✅ pass ite_cond_calls_Any_to_bool_0: ✅ pass (at line 4, col 4) (classify ensures) Return type constraint: ✅ pass ite_cond_calls_Any_to_bool_0: ✅ pass (at line 6, col 4) @@ -20,5 +21,5 @@ assert_assert(444)_calls_Any_to_bool_0: ✅ pass (at line 22, col 4) assert(444): ❓ unknown (at line 22, col 4) ite_cond_calls_Any_to_bool_0: ✅ pass (at line 24, col 0) -DETAIL: 6 passed, 1 failed, 5 inconclusive -RESULT: Failures found +DETAIL: 16 passed, 0 failed, 4 inconclusive +RESULT: Inconclusive diff --git a/StrataTest/Languages/Python/expected_laurel/test_multi_function.expected b/StrataTest/Languages/Python/expected_laurel/test_multi_function.expected index bc184469a..371f6ef50 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_multi_function.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_multi_function.expected @@ -1,6 +1,7 @@ ==== Verification Results ==== -Assertion failed at line 9, col 4: ite_cond_calls_PNotIn_0: ❌ fail +(create_config ensures) Return type constraint: ✅ pass +ite_cond_calls_PNotIn_0: ✅ pass (at line 9, col 4) ite_cond_calls_Any_to_bool_1: ✅ pass (at line 9, col 4) (validate_config ensures) Return type constraint: ✅ pass ite_cond_calls_PNotIn_0: ✅ pass (at line 11, col 4) @@ -21,5 +22,5 @@ callElimAssert_req_opt_name_none_or_str_15: ✅ pass (at line 26, col 4) callElimAssert_req_opt_name_none_or_bar_16: ✅ pass (at line 26, col 4) ite_cond_calls_Any_to_bool_0: ✅ pass (at line 28, col 0) -DETAIL: 7 passed, 2 failed, 3 inconclusive +DETAIL: 19 passed, 1 failed, 1 inconclusive RESULT: Failures found diff --git a/StrataTest/Languages/Python/expected_laurel/test_nested_calls.expected b/StrataTest/Languages/Python/expected_laurel/test_nested_calls.expected index ee45cb026..09f69047a 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_nested_calls.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_nested_calls.expected @@ -1,5 +1,9 @@ ==== Verification Results ==== +(double ensures) Return type constraint: ✅ pass +(add_one ensures) Return type constraint: ✅ pass +callElimAssert_requires_22: ✅ pass +callElimAssert_requires_18: ✅ pass assert_assert(153)_calls_Any_to_bool_0: ✅ pass (at line 10, col 4) Assertion failed at line 10, col 4: assert(153): ❌ fail callElimAssert_requires_14: ✅ pass @@ -12,5 +16,5 @@ assert_assert(356)_calls_Any_to_bool_0: ✅ pass (at line 18, col 4) Assertion failed at line 18, col 4: assert(356): ❌ fail ite_cond_calls_Any_to_bool_0: ✅ pass (at line 20, col 0) -DETAIL: 4 passed, 3 failed, 0 inconclusive +DETAIL: 12 passed, 3 failed, 0 inconclusive RESULT: Failures found diff --git a/StrataTest/Languages/Python/expected_laurel/test_return_types.expected b/StrataTest/Languages/Python/expected_laurel/test_return_types.expected index bd2f91dcb..5cc78dab0 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_return_types.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_return_types.expected @@ -1,5 +1,9 @@ ==== Verification Results ==== +(get_number ensures) Return type constraint: ✅ pass +(get_greeting ensures) Return type constraint: ✅ pass +(get_flag ensures) Return type constraint: ✅ pass +(add ensures) Return type constraint: ✅ pass assert_assert(304)_calls_Any_to_bool_0: ✅ pass (at line 20, col 4) Assertion failed at line 20, col 4: assert(304): ❌ fail assert_assert(387)_calls_Any_to_bool_0: ✅ pass (at line 23, col 4) @@ -12,5 +16,5 @@ assert_assert(558)_calls_Any_to_bool_0: ✅ pass (at line 29, col 4) Assertion failed at line 29, col 4: assert(558): ❌ fail ite_cond_calls_Any_to_bool_0: ✅ pass (at line 31, col 0) -DETAIL: 5 passed, 3 failed, 1 inconclusive +DETAIL: 11 passed, 3 failed, 1 inconclusive RESULT: Failures found diff --git a/StrataTest/Languages/Python/expected_laurel/test_while_loop.expected b/StrataTest/Languages/Python/expected_laurel/test_while_loop.expected index f495935a4..f7450551e 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_while_loop.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_while_loop.expected @@ -25,5 +25,5 @@ assert_assert(589)_calls_Any_to_bool_0: ✅ pass (at line 27, col 4) assert(589): ❓ unknown (at line 27, col 4) (test_while_with_continue ensures) Return type constraint: ❓ unknown -DETAIL: 16 passed, 0 failed, 3 inconclusive +DETAIL: 17 passed, 0 failed, 7 inconclusive RESULT: Inconclusive diff --git a/StrataTest/Languages/Python/expected_laurel/test_with_statement.expected b/StrataTest/Languages/Python/expected_laurel/test_with_statement.expected index 3329376fa..0d352bc8a 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_with_statement.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_with_statement.expected @@ -22,5 +22,5 @@ callElimAssert_requires_31: ✅ pass callElimAssert_requires_28: ✅ pass Assertion failed at line 27, col 0: postcondition: ❌ fail -DETAIL: 15 passed, 2 failed, 1 inconclusive +DETAIL: 15 passed, 5 failed, 1 inconclusive RESULT: Failures found From 600b18a83b83fa03d268804ed2cc1bcb15063513 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Tue, 31 Mar 2026 11:58:32 -0700 Subject: [PATCH 26/31] remove slice checking for dict and list --- Strata/Languages/Python/PythonToLaurel.lean | 28 +++++---------------- 1 file changed, 6 insertions(+), 22 deletions(-) diff --git a/Strata/Languages/Python/PythonToLaurel.lean b/Strata/Languages/Python/PythonToLaurel.lean index 9cc9ac584..65c3969bc 100644 --- a/Strata/Languages/Python/PythonToLaurel.lean +++ b/Strata/Languages/Python/PythonToLaurel.lean @@ -1397,36 +1397,20 @@ partial def getArgumentTypes (arg: Python.expr SourceRange) : Except Translation | .Name _ n _ => return [n.val] | .Subscript _ _ slice _ => let subscriptList:= getNestedSubscripts arg - let subscriptRoot := pyExprToString subscriptList[0]! + let subscriptRoot := match subscriptList[0]! with + | .Attribute _ (.Name _ n _) att _ => if n.val == "typing" then att.val else pyExprToString subscriptList[0]! + | _ => pyExprToString subscriptList[0]! let sliceHead := subscriptList[1]! match subscriptRoot with | "Optional" => return [pyExprToString sliceHead, "None"] | "Union" => match sliceHead with | .Tuple _ tys _ => return (← tys.val.toList.mapM getArgumentTypes).flatten | _ => throw (.internalError s!"Unhandled Expr: {repr arg}") - | "List" => do - match ← getArgumentTypes slice with - | [ty] => - if isOfAnyType ty then - return ["ListAny"] - else - throw (.unsupportedConstruct "List of non-value type is not supported" s!"List[{ty}]") - | _ => throw (.unsupportedConstruct "Invalid list element type" s!"List[{toString (repr slice)}]") - | "Dict" => do match sliceHead with - | .Tuple _ tys _ => - if tys.val.size != 2 then - throw (.internalError s!"Unhandled Expr: {repr arg}") - else - match ← getArgumentTypes tys.val[0]!, ← getArgumentTypes tys.val[1]! with - | ["str"], [ty] => - if isOfAnyType ty then - return ["DictStrAny"] - else - throw (.unsupportedConstruct "Dict of non-value type is not supported" ty) - | _, _ => throw (.internalError s!"Unhandled Dict key/value types: {repr arg}") - | _ => throw (.unsupportedConstruct "Unhandled Dict key/value types" (toString (repr sliceHead))) + | "List" => return ["ListAny"] + | "Dict" => return ["DictStrAny"] | _ => throw (.internalError s!"Unhandled Expr: {repr arg}") | .Constant _ _ _ => return ["None"] + | .Attribute _ (.Name _ {val:= "typing",..} _) att _ => return [att.val] | .Attribute _ _ _ _ => return [pyExprToString arg] | .BinOp _ _ _ _ => return (← (getUnionTypes arg).mapM getArgumentTypes).flatten | _ => throw (.internalError s!"Unhandled Expr: {repr arg}") From d31bc90d3d1362f089beb0b56a2d5f161e232216 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Tue, 31 Mar 2026 16:18:01 -0700 Subject: [PATCH 27/31] fix internal regression --- .../Python/PythonLaurelCorePrelude.lean | 3 +- .../Python/PythonRuntimeLaurelPart.lean | 9 ++++ Strata/Languages/Python/PythonToLaurel.lean | 44 ++++++++++++------- .../Languages/Python/PreludeVerifyTest.lean | 6 +-- .../test_break_continue.expected | 10 ++++- .../expected_laurel/test_for_loop.expected | 10 ++++- .../test_function_def_calls.expected | 2 +- .../expected_laurel/test_loops.expected | 4 +- .../expected_laurel/test_pin_any.expected | 3 +- .../test_return_types.expected | 3 +- 10 files changed, 67 insertions(+), 27 deletions(-) diff --git a/Strata/Languages/Python/PythonLaurelCorePrelude.lean b/Strata/Languages/Python/PythonLaurelCorePrelude.lean index f95dd9bb0..d04088958 100644 --- a/Strata/Languages/Python/PythonLaurelCorePrelude.lean +++ b/Strata/Languages/Python/PythonLaurelCorePrelude.lean @@ -69,7 +69,7 @@ datatype Error () { datatype OptionInt { OptSome (unwrap: int), OptNone () -} +}; datatype Any () { from_none (), @@ -78,6 +78,7 @@ datatype Any () { from_float (as_float : real), from_string (as_string : string), from_datetime (as_datetime : int), + from_bytes (as_bytes: string), from_Dict (as_Dict: DictStrAny), from_ListAny (as_ListAny : ListAny), from_ClassInstance (classname : string, instance_attributes: DictStrAny), diff --git a/Strata/Languages/Python/PythonRuntimeLaurelPart.lean b/Strata/Languages/Python/PythonRuntimeLaurelPart.lean index ef2b37fdd..e455f1a01 100644 --- a/Strata/Languages/Python/PythonRuntimeLaurelPart.lean +++ b/Strata/Languages/Python/PythonRuntimeLaurelPart.lean @@ -75,6 +75,7 @@ datatype Any { from_float (as_float : real), from_string (as_string : string), from_datetime (as_datetime : int), + from_bytes (as_bytes: string), from_Dict (as_Dict: DictStrAny), from_ListAny (as_ListAny : ListAny), from_ClassInstance (classname : string, instance_attributes: DictStrAny), @@ -391,6 +392,14 @@ function List_set (l : ListAny, i : int, v: Any) : ListAny //Require recursive function on int function List_repeat (l: ListAny, n: int): ListAny; +function ListAny_range(i: Any) : ListAny; + +function range (i: Any) : Any + requires Any..isfrom_int(i) +{ + from_ListAny (ListAny_range(i)) +}; + // ///////////////////////////////////////////////////////////////////////////////////// // DictStrAny functions // ///////////////////////////////////////////////////////////////////////////////////// diff --git a/Strata/Languages/Python/PythonToLaurel.lean b/Strata/Languages/Python/PythonToLaurel.lean index 65c3969bc..5b66c89b1 100644 --- a/Strata/Languages/Python/PythonToLaurel.lean +++ b/Strata/Languages/Python/PythonToLaurel.lean @@ -1317,7 +1317,7 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang -- This is sound: if there are 0 iterations, we havoc; if >0, we execute once and havoc | .For _ target iter body _orelse _ => do -- The iterator expression (we abstract it away) - let _iterExpr ← translateExpr ctx iter + let iterExpr ← translateExpr ctx iter -- Create context with target(s) and loop labels let breakLabel := s!"for_break_{iter.toAst.ann.start.byteIdx}" let continueLabel := s!"for_continue_{iter.toAst.ann.start.byteIdx}" @@ -1329,6 +1329,14 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang loopBreakLabel := some breakLabel loopContinueLabel := some continueLabel } let (finalCtx, bodyStmts) ← translateStmtList bodyCtx body.val.toList + let assumeInStmts :=match target with + | .Name _ n _ => + let targetVar := mkStmtExprMd (StmtExpr.Identifier n.val) + let targetInIter := mkStmtExprMd (.StaticCall "PIn" [targetVar, iterExpr]) + let assumeInStmt := mkStmtExprMd (.Assume (Any_to_bool targetInIter)) + [assumeInStmt] + | _ => [] + let bodyStmts := assumeInStmts ++ bodyStmts let innerBlock := mkStmtExprMd (StmtExpr.Block bodyStmts (some continueLabel)) let loopBlock := mkStmtExprMdWithLoc (StmtExpr.Block [innerBlock] (some breakLabel)) md return (finalCtx, targetDecls ++ [loopBlock]) @@ -1383,12 +1391,12 @@ def getUnionTypes (arg: Python.expr SourceRange) : List (Python.expr SourceRange | .BinOp _ left _ right => getUnionTypes left ++ getUnionTypes right | _ => [arg] -def isOfAnyType (ty: String): Bool := ty ∈ ["None", "bool", "int", "str", "float", "datetime", "ListAny", "DictStrAny", "Any"] +def isOfAnyType (ty: String): Bool := ty ∈ ["None", "bool", "int", "str", "float", "datetime", "bytes", "ListAny", "DictStrAny", "Any"] -def checkValidTypeList (ctx : TranslationContext) (tys: List String) : Except TranslationError (List String) := do +def checkValidInputTypeList (ctx : TranslationContext) (tys: List String) : Except TranslationError (List String) := do for ty in tys do let _ ← translateType ctx ty - if tys.length > 1 && tys.any (isCompositeType ctx) then + if tys.length > 1 && tys.any (λ ty => ¬ isOfAnyType ty) then throw (.unsupportedConstruct "Argument of union of class types is not supported" (toString tys)) return tys @@ -1398,11 +1406,12 @@ partial def getArgumentTypes (arg: Python.expr SourceRange) : Except Translation | .Subscript _ _ slice _ => let subscriptList:= getNestedSubscripts arg let subscriptRoot := match subscriptList[0]! with - | .Attribute _ (.Name _ n _) att _ => if n.val == "typing" then att.val else pyExprToString subscriptList[0]! + | .Attribute _ _ {val:= "Dict", ..} _ => "Dict" + | .Attribute _ _ {val:= "List", ..} _ => "List" | _ => pyExprToString subscriptList[0]! let sliceHead := subscriptList[1]! match subscriptRoot with - | "Optional" => return [pyExprToString sliceHead, "None"] + | "Optional" => return (← getArgumentTypes slice) ++ ["None"] | "Union" => match sliceHead with | .Tuple _ tys _ => return (← tys.val.toList.mapM getArgumentTypes).flatten | _ => throw (.internalError s!"Unhandled Expr: {repr arg}") @@ -1410,9 +1419,11 @@ partial def getArgumentTypes (arg: Python.expr SourceRange) : Except Translation | "Dict" => return ["DictStrAny"] | _ => throw (.internalError s!"Unhandled Expr: {repr arg}") | .Constant _ _ _ => return ["None"] - | .Attribute _ (.Name _ {val:= "typing",..} _) att _ => return [att.val] | .Attribute _ _ _ _ => return [pyExprToString arg] | .BinOp _ _ _ _ => return (← (getUnionTypes arg).mapM getArgumentTypes).flatten + | .Slice _ lower upper _ => match lower.val, upper.val with + | some (.Name _ _ _ ), some upper => getArgumentTypes upper + | _, _ => throw (.internalError s!"Unhandled Expr: {repr arg}") | _ => throw (.internalError s!"Unhandled Expr: {repr arg}") --The return is a List (inputname, type, default value) and a bool indicating if the function has Kwargs input @@ -1445,7 +1456,7 @@ def unpackPyArguments (ctx : TranslationContext) (args: Python.arguments SourceR if isOfAnyType defaultType && tys != [PyLauType.Any] && defaultType ∉ tys then throw (.unsupportedConstruct "Default value type is invalid" (toString (repr arg))) | _ => pure () - tys ← checkValidTypeList ctx tys + tys ← checkValidInputTypeList ctx tys argtypes := argtypes ++ [{name:= name.val, md:=md, tys:= tys, default:= default}] let kwargsName := kwargs.val.map (λ kwarg => match kwarg with | .mk_arg _ name _ _ => name.val) return (argtypes, kwargsName) @@ -1461,8 +1472,9 @@ def pyFuncDefToPythonFunctionDecl (ctx : TranslationContext) (f : Python.stmt S else match returns.val with | some retTy => - let tys ← checkValidTypeList ctx (← getArgumentTypes retTy) - pure (tys, retMd) + match checkValidInputTypeList ctx (← getArgumentTypes retTy) with + | .ok tys => pure (tys, retMd) + | _ => pure none | none => pure none let kwargsName := args_trans.snd return { @@ -1480,6 +1492,7 @@ def getSingleTypeConstraint (var: String) (ty: String): Option StmtExprMd := | "bool" => mkStmtExprMd (.StaticCall "Any..isfrom_bool" [freeVar var]) | "float" => mkStmtExprMd (.StaticCall "Any..isfrom_float" [freeVar var]) | "datetime" => mkStmtExprMd (.StaticCall "Any..isfrom_datetime" [freeVar var]) + | "bytes" => mkStmtExprMd (.StaticCall "Any..isfrom_bytes" [freeVar var]) | "None" => mkStmtExprMd (.StaticCall "Any..isfrom_none" [freeVar var]) | "ListAny" => mkStmtExprMd (.StaticCall "Any..isfrom_ListAny" [freeVar var]) | "DictStrAny" => mkStmtExprMd (.StaticCall "Any..isfrom_Dict" [freeVar var]) @@ -1498,7 +1511,6 @@ def getUnionTypeConstraint (var: String) (md: MetaData) (tys: List String) (func some {createBoolOrExpr type_constraints with md:=md} def getReturnTypeEnsure (md: MetaData) (tys: List String) (funcname: String): Option StmtExprMd := - let tys := tys.filter (λ ty => ty ≠ "None") let type_constraints := tys.filterMap (getSingleTypeConstraint PyLauFuncReturnVar) if type_constraints.isEmpty then none else let md: MetaData := md.withPropertySummary $ "(" ++ funcname ++ " ensures) Return type constraint" @@ -1540,18 +1552,18 @@ def translateFunction (ctx : TranslationContext) (sourceRange: SourceRange) (fun match funcDecl.ret.map fun (tys, md) => getReturnTypeEnsure md tys funcDecl.name with | some (some constraint) => [constraint] | _ => [] - -- Declare an output parameter when the function has a return type annotation. -- Return statements explicitly assign to LaurelResult and exit $body. - let outputs : List Parameter := - match funcDecl.ret with - | none => [] - | some _ => [{ name := PyLauFuncReturnVar, type := AnyTy }] + let outputs : List Parameter := [{ name := PyLauFuncReturnVar, type := AnyTy }] -- Translate function body let inputTypes := funcDecl.args.map (λ arg => match arg.tys with | [ty] => (arg.name, ty) | _ => (arg.name, PyLauType.Any)) let (bodyBlock, newCtx) ← translateFunctionBody ctx inputTypes body + let noneReturn := mkStmtExprMd (.Assign [mkStmtExprMd (.Identifier PyLauFuncReturnVar)] AnyNone) + let bodyBlock : StmtExprMd := match bodyBlock.val with + | .Block bodyStmts label => {bodyBlock with val:= .Block (noneReturn::bodyStmts) label} + | _ => bodyBlock -- Create procedure with transparent body (no contracts for now) let proc : Procedure := { diff --git a/StrataTest/Languages/Python/PreludeVerifyTest.lean b/StrataTest/Languages/Python/PreludeVerifyTest.lean index 26591602f..728543dcf 100644 --- a/StrataTest/Languages/Python/PreludeVerifyTest.lean +++ b/StrataTest/Languages/Python/PreludeVerifyTest.lean @@ -157,15 +157,15 @@ Obligation: postcondition Property: assert Result: ✅ pass -Obligation: assert(41605) +Obligation: assert(41796) Property: assert Result: ✅ pass -Obligation: assert(41675) +Obligation: assert(41866) Property: assert Result: ✅ pass -Obligation: assert(41786) +Obligation: assert(41977) Property: assert Result: ✅ pass diff --git a/StrataTest/Languages/Python/expected_laurel/test_break_continue.expected b/StrataTest/Languages/Python/expected_laurel/test_break_continue.expected index 00a8205c2..d4c426640 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_break_continue.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_break_continue.expected @@ -1,8 +1,16 @@ ==== Verification Results ==== loop_guard_calls_Any_to_bool_0: ✅ pass (at line 3, col 4) +(test_while_break ensures) Return type constraint: ✅ pass loop_guard_calls_Any_to_bool_0: ✅ pass (at line 8, col 4) loop_guard_end_calls_Any_to_bool_0: ✅ pass (at line 8, col 4) +(test_while_continue ensures) Return type constraint: ✅ pass +assume_assume(0)_calls_PIn_0: ✅ pass +assume_assume(0)_calls_Any_to_bool_1: ✅ pass +(test_for_break ensures) Return type constraint: ✅ pass +assume_assume(0)_calls_PIn_0: ✅ pass +assume_assume(0)_calls_Any_to_bool_1: ✅ pass +(test_for_continue ensures) Return type constraint: ✅ pass -DETAIL: 3 passed, 0 failed, 0 inconclusive +DETAIL: 11 passed, 0 failed, 0 inconclusive RESULT: Analysis success diff --git a/StrataTest/Languages/Python/expected_laurel/test_for_loop.expected b/StrataTest/Languages/Python/expected_laurel/test_for_loop.expected index 8a80af716..495cf01a8 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_for_loop.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_for_loop.expected @@ -1,15 +1,21 @@ ==== Verification Results ==== +assume_assume(0)_calls_PIn_0: ✅ pass +assume_assume(0)_calls_Any_to_bool_1: ✅ pass assert_assert(129)_calls_Any_to_bool_0: ✅ pass (at line 6, col 4) assert(129): ❓ unknown (at line 6, col 4) -Assertion failed at line 13, col 8: ite_cond_calls_Any_to_bool_0: ❌ fail +assume_assume(0)_calls_PIn_0: ✅ pass +assume_assume(0)_calls_Any_to_bool_1: ✅ pass +ite_cond_calls_Any_to_bool_0: ✅ pass (at line 13, col 8) assert_assert(361)_calls_Any_to_bool_0: ✅ pass (at line 15, col 4) assert(361): ❓ unknown (at line 15, col 4) +assume_assume(0)_calls_PIn_0: ✅ pass +assume_assume(0)_calls_Any_to_bool_1: ✅ pass ite_cond_calls_Any_to_bool_0: ✅ pass (at line 22, col 8) assert_assert(611)_calls_Any_to_bool_0: ✅ pass (at line 25, col 4) assert(611): ✅ pass (at line 25, col 4) assert_assert(611)_calls_Any_to_bool_0: ✅ pass (at line 25, col 4) Assertion failed at line 25, col 4: assert(611): ❌ fail -DETAIL: 6 passed, 2 failed, 2 inconclusive +DETAIL: 13 passed, 1 failed, 2 inconclusive RESULT: Failures found diff --git a/StrataTest/Languages/Python/expected_laurel/test_function_def_calls.expected b/StrataTest/Languages/Python/expected_laurel/test_function_def_calls.expected index e3af3f68e..533f8dc69 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_function_def_calls.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_function_def_calls.expected @@ -3,7 +3,7 @@ callElimAssert_requires_0_4: ❓ unknown (at line 6, col 4) callElimAssert_requires_1_5: ✅ pass (at line 6, col 4) callElimAssert_requires_2_6: ✅ pass (at line 6, col 4) -callElimAssert_requires_9: ✅ pass (at line 9, col 4) +callElimAssert_requires_10: ✅ pass (at line 9, col 4) ite_cond_calls_Any_to_bool_0: ✅ pass (at line 11, col 0) DETAIL: 4 passed, 0 failed, 1 inconclusive diff --git a/StrataTest/Languages/Python/expected_laurel/test_loops.expected b/StrataTest/Languages/Python/expected_laurel/test_loops.expected index 0c0a3532d..59d1e6cf1 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_loops.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_loops.expected @@ -1,5 +1,7 @@ ==== Verification Results ==== +assume_assume(0)_calls_PIn_0: ✅ pass +assume_assume(0)_calls_Any_to_bool_1: ✅ pass assert_assert(95)_calls_Any_to_bool_0: ✅ pass (at line 6, col 4) assert(95): ✅ pass (at line 6, col 4) set_a_calls_Any_get_0: ❓ unknown @@ -17,5 +19,5 @@ loop_guard_end_calls_Any_to_bool_0: ✅ pass (at line 22, col 4) assert_assert(531)_calls_Any_to_bool_0: ❓ unknown (at line 24, col 4) assert(531): ❓ unknown (at line 24, col 4) -DETAIL: 8 passed, 0 failed, 8 inconclusive +DETAIL: 10 passed, 0 failed, 8 inconclusive RESULT: Inconclusive diff --git a/StrataTest/Languages/Python/expected_laurel/test_pin_any.expected b/StrataTest/Languages/Python/expected_laurel/test_pin_any.expected index 499a03261..9718801d0 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_pin_any.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_pin_any.expected @@ -4,6 +4,7 @@ ite_cond_calls_Any_to_bool_0: 🔶 can be both true and false and is reachable f assert_assert(124)_calls_PIn_0: ❓ unknown (at line 4, col 8) assert_assert(124)_calls_Any_to_bool_1: ✔️ always true if reached (at line 4, col 8) assert(124): ❓ unknown (at line 4, col 8) +(test_in_on_any ensures) Return type constraint: ✔️ always true if reached -DETAIL: 1 passed, 0 failed, 3 inconclusive +DETAIL: 2 passed, 0 failed, 3 inconclusive RESULT: Inconclusive diff --git a/StrataTest/Languages/Python/expected_laurel/test_return_types.expected b/StrataTest/Languages/Python/expected_laurel/test_return_types.expected index 5cc78dab0..92a8b0d89 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_return_types.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_return_types.expected @@ -3,6 +3,7 @@ (get_number ensures) Return type constraint: ✅ pass (get_greeting ensures) Return type constraint: ✅ pass (get_flag ensures) Return type constraint: ✅ pass +(get_nothing ensures) Return type constraint: ✅ pass (add ensures) Return type constraint: ✅ pass assert_assert(304)_calls_Any_to_bool_0: ✅ pass (at line 20, col 4) Assertion failed at line 20, col 4: assert(304): ❌ fail @@ -16,5 +17,5 @@ assert_assert(558)_calls_Any_to_bool_0: ✅ pass (at line 29, col 4) Assertion failed at line 29, col 4: assert(558): ❌ fail ite_cond_calls_Any_to_bool_0: ✅ pass (at line 31, col 0) -DETAIL: 11 passed, 3 failed, 1 inconclusive +DETAIL: 12 passed, 3 failed, 1 inconclusive RESULT: Failures found From 1e86ce3299a1ef826b1111c3a441ea594039533b Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Wed, 1 Apr 2026 09:35:39 -0700 Subject: [PATCH 28/31] rename Any constructors to make it consistent with Python type names, not Core's ones --- .../Python/PythonLaurelCorePrelude.lean | 6 +- .../Python/PythonRuntimeLaurelPart.lean | 130 +++++++++--------- 2 files changed, 68 insertions(+), 68 deletions(-) diff --git a/Strata/Languages/Python/PythonLaurelCorePrelude.lean b/Strata/Languages/Python/PythonLaurelCorePrelude.lean index d04088958..0f8e92ba5 100644 --- a/Strata/Languages/Python/PythonLaurelCorePrelude.lean +++ b/Strata/Languages/Python/PythonLaurelCorePrelude.lean @@ -72,14 +72,14 @@ datatype OptionInt { }; datatype Any () { - from_none (), + from_None (), from_bool (as_bool : bool), from_int (as_int : int), from_float (as_float : real), - from_string (as_string : string), + from_str (as_string : string), from_datetime (as_datetime : int), from_bytes (as_bytes: string), - from_Dict (as_Dict: DictStrAny), + from_DictStrAny (as_Dict: DictStrAny), from_ListAny (as_ListAny : ListAny), from_ClassInstance (classname : string, instance_attributes: DictStrAny), from_Slice(start: int, stop: OptionInt), diff --git a/Strata/Languages/Python/PythonRuntimeLaurelPart.lean b/Strata/Languages/Python/PythonRuntimeLaurelPart.lean index e455f1a01..4671dd157 100644 --- a/Strata/Languages/Python/PythonRuntimeLaurelPart.lean +++ b/Strata/Languages/Python/PythonRuntimeLaurelPart.lean @@ -69,14 +69,14 @@ datatype OptionInt { } datatype Any { - from_none (), + from_None (), from_bool (as_bool : bool), from_int (as_int : int), from_float (as_float : real), - from_string (as_string : string), + from_str (as_string : string), from_datetime (as_datetime : int), from_bytes (as_bytes: string), - from_Dict (as_Dict: DictStrAny), + from_DictStrAny (as_Dict: DictStrAny), from_ListAny (as_ListAny : ListAny), from_ClassInstance (classname : string, instance_attributes: DictStrAny), from_Slice(start: int, stop: OptionInt), @@ -106,7 +106,7 @@ datatype DictStrAny { // // The Python-through-Laurel pipeline is entirely Any-typed: all user // variables and function inputs/outputs are wrapped in the Any datatype. -// Consequently, re_match/re_search/re_fullmatch return Any (from_none +// Consequently, re_match/re_search/re_fullmatch return Any (from_None // or from_ClassInstance wrapping a re_Match). If the pipeline ever // moves to concrete types, these should return re_Match | None directly. // @@ -186,7 +186,7 @@ function Str.Length(s: string): int external; function mk_re_Match(s : string) : Any { from_ClassInstance("re_Match", - DictStrAny_cons("re_match_string", from_string(s), + DictStrAny_cons("re_match_string", from_str(s), DictStrAny_cons("re_match_pos", from_int(0), DictStrAny_cons("re_match_endpos", from_int(Str.Length(s)), DictStrAny_empty())))) @@ -194,37 +194,37 @@ function mk_re_Match(s : string) : Any { // re.compile is a no-op: returns the pattern string unchanged. function re_compile(pattern : Any) : Any - requires Any..isfrom_string(pattern) + requires Any..isfrom_str(pattern) { pattern }; function re_fullmatch(pattern : Any, s : Any) : Any - requires Any..isfrom_string(pattern) && Any..isfrom_string(s) + requires Any..isfrom_str(pattern) && Any..isfrom_str(s) { if Error..isRePatternError(re_pattern_error(Any..as_string!(pattern))) then exception(re_pattern_error(Any..as_string!(pattern))) else if re_fullmatch_bool(Any..as_string!(pattern), Any..as_string!(s)) then mk_re_Match(Any..as_string!(s)) - else from_none() + else from_None() }; function re_match(pattern : Any, s : Any) : Any - requires Any..isfrom_string(pattern) && Any..isfrom_string(s) + requires Any..isfrom_str(pattern) && Any..isfrom_str(s) { if Error..isRePatternError(re_pattern_error(Any..as_string!(pattern))) then exception(re_pattern_error(Any..as_string!(pattern))) else if re_match_bool(Any..as_string!(pattern), Any..as_string!(s)) then mk_re_Match(Any..as_string!(s)) - else from_none() + else from_None() }; function re_search(pattern : Any, s : Any) : Any - requires Any..isfrom_string(pattern) && Any..isfrom_string(s) + requires Any..isfrom_str(pattern) && Any..isfrom_str(s) { if Error..isRePatternError(re_pattern_error(Any..as_string!(pattern))) then exception(re_pattern_error(Any..as_string!(pattern))) else if re_search_bool(Any..as_string!(pattern), Any..as_string!(s)) then mk_re_Match(Any..as_string!(s)) - else from_none() + else from_None() }; // ///////////////////////////////////////////////////////////////////////////////////// @@ -244,7 +244,7 @@ function isFloat (v: Any) : Any { }; function isString (v: Any) : Any { - from_bool (Any..isfrom_string(v)) + from_bool (Any..isfrom_str(v)) }; function isdatetime (v: Any) : Any { @@ -252,7 +252,7 @@ function isdatetime (v: Any) : Any { }; function isDict (v: Any) : Any { - from_bool (Any..isfrom_Dict(v)) + from_bool (Any..isfrom_DictStrAny(v)) }; function isList (v: Any) : Any { @@ -307,13 +307,13 @@ function isError (e: Error) : bool { // ///////////////////////////////////////////////////////////////////////////////////// function Any_to_bool (v: Any) : bool - requires (Any..isfrom_bool(v) || Any..isfrom_none(v) || Any..isfrom_string(v) || Any..isfrom_int(v) || Any..isfrom_Dict(v) || Any..isfrom_ListAny(v)) + requires (Any..isfrom_bool(v) || Any..isfrom_None(v) || Any..isfrom_str(v) || Any..isfrom_int(v) || Any..isfrom_DictStrAny(v) || Any..isfrom_ListAny(v)) { if (Any..isfrom_bool(v)) then Any..as_bool!(v) else - if (Any..isfrom_none(v)) then false else - if (Any..isfrom_string(v)) then !(Any..as_string!(v) == "") else + if (Any..isfrom_None(v)) then false else + if (Any..isfrom_str(v)) then !(Any..as_string!(v) == "") else if (Any..isfrom_int(v)) then !(Any..as_int!(v) == 0) else - if (Any..isfrom_Dict(v)) then !(Any..as_Dict!(v) == DictStrAny_empty()) else + if (Any..isfrom_DictStrAny(v)) then !(Any..as_Dict!(v) == DictStrAny_empty()) else if (Any..isfrom_ListAny(v)) then !(Any..as_ListAny!(v) == ListAny_nil()) else false //WILL BE ADDED @@ -346,7 +346,7 @@ function List_extend (l1 : ListAny, l2: ListAny) : ListAny function List_get (l : ListAny, i : int) : Any requires i >= 0 && i < List_len(l) { - if ListAny..isListAny_nil(l) then from_none() + if ListAny..isListAny_nil(l) then from_None() else if i == 0 then ListAny..head!(l) else List_get(ListAny..tail!(l), i - 1) }; @@ -413,7 +413,7 @@ function DictStrAny_contains (d : DictStrAny, key: string) : bool function DictStrAny_get (d : DictStrAny, key: string) : Any requires DictStrAny_contains(d, key) { - if DictStrAny..isDictStrAny_empty(d) then from_none() + if DictStrAny..isDictStrAny_empty(d) then from_None() else if DictStrAny..key!(d) == key then DictStrAny..val!(d) else DictStrAny_get(DictStrAny..tail!(d), key) }; @@ -421,11 +421,11 @@ function DictStrAny_get (d : DictStrAny, key: string) : Any function DictStrAny_get_or_none (d : DictStrAny, key: string) : Any { if DictStrAny_contains(d, key) then DictStrAny_get(d, key) - else from_none() + else from_None() }; function Any_get_or_none (dict: Any, key: Any) : Any - requires Any..isfrom_Dict(dict) && Any..isfrom_string(key) + requires Any..isfrom_DictStrAny(dict) && Any..isfrom_str(key) { DictStrAny_get_or_none(Any..as_Dict!(dict), Any..as_string!(key)) }; @@ -438,13 +438,13 @@ function DictStrAny_insert (d : DictStrAny, key: string, val: Any) : DictStrAny }; function Any_get (dictOrList: Any, index: Any): Any - requires (Any..isfrom_Dict(dictOrList) && Any..isfrom_string(index) && DictStrAny_contains(Any..as_Dict!(dictOrList), Any..as_string!(index))) || + requires (Any..isfrom_DictStrAny(dictOrList) && Any..isfrom_str(index) && DictStrAny_contains(Any..as_Dict!(dictOrList), Any..as_string!(index))) || (Any..isfrom_ListAny(dictOrList) && Any..isfrom_int(index) && Any..as_int!(index) >= 0 && Any..as_int!(index) < List_len(Any..as_ListAny!(dictOrList)))|| (Any..isfrom_ListAny(dictOrList) && Any..isfrom_Slice(index) && Any..start!(index) >= 0 && Any..start!(index) < List_len(Any..as_ListAny!(dictOrList)) && ((OptionInt..isOptSome(Any..stop!(index))) && OptionInt..unwrap!(Any..stop!(index)) >= 0 && OptionInt..unwrap!(Any..stop!(index)) <= List_len(Any..as_ListAny!(dictOrList)) && Any..start!(index) <= OptionInt..unwrap!(Any..stop!(index)) || (OptionInt..isOptNone(Any..stop!(index))))) { - if Any..isfrom_Dict(dictOrList) then + if Any..isfrom_DictStrAny(dictOrList) then DictStrAny_get(Any..as_Dict!(dictOrList), Any..as_string!(index)) else if Any..isfrom_ListAny(dictOrList) && Any..isfrom_int(index) then List_get(Any..as_ListAny!(dictOrList), Any..as_int!(index)) @@ -458,9 +458,9 @@ function Any_get! (dictOrList: Any, index: Any): Any { if Any..isexception(dictOrList) then dictOrList else if Any..isexception(index) then index - else if !(Any..isfrom_Dict(dictOrList) && Any..isfrom_string(index)) && !(Any..isfrom_ListAny(dictOrList) && Any..isfrom_int(index)) then + else if !(Any..isfrom_DictStrAny(dictOrList) && Any..isfrom_str(index)) && !(Any..isfrom_ListAny(dictOrList) && Any..isfrom_int(index)) then exception (TypeError("Invalid subscription type")) - else if Any..isfrom_Dict(dictOrList) && Any..isfrom_string(index) && DictStrAny_contains(Any..as_Dict!(dictOrList), Any..as_string!(index)) then + else if Any..isfrom_DictStrAny(dictOrList) && Any..isfrom_str(index) && DictStrAny_contains(Any..as_Dict!(dictOrList), Any..as_string!(index)) then DictStrAny_get(Any..as_Dict!(dictOrList), Any..as_string!(index)) else if Any..isfrom_ListAny(dictOrList) && Any..isfrom_int(index) && Any..as_int!(index) >= 0 && Any..as_int!(index) < List_len(Any..as_ListAny!(dictOrList)) then List_get(Any..as_ListAny!(dictOrList), Any..as_int!(index)) @@ -469,11 +469,11 @@ function Any_get! (dictOrList: Any, index: Any): Any }; function Any_set (dictOrList: Any, index: Any, val: Any): Any - requires (Any..isfrom_Dict(dictOrList) && Any..isfrom_string(index)) || + requires (Any..isfrom_DictStrAny(dictOrList) && Any..isfrom_str(index)) || (Any..isfrom_ListAny(dictOrList) && Any..isfrom_int(index) && Any..as_int!(index) >= 0 && Any..as_int!(index) < List_len(Any..as_ListAny!(dictOrList))) { - if Any..isfrom_Dict(dictOrList) then - from_Dict(DictStrAny_insert(Any..as_Dict!(dictOrList), Any..as_string!(index), val)) + if Any..isfrom_DictStrAny(dictOrList) then + from_DictStrAny(DictStrAny_insert(Any..as_Dict!(dictOrList), Any..as_string!(index), val)) else from_ListAny(List_set(Any..as_ListAny!(dictOrList), Any..as_int!(index), val)) }; @@ -483,10 +483,10 @@ function Any_set! (dictOrList: Any, index: Any, val: Any): Any if Any..isexception(dictOrList) then dictOrList else if Any..isexception(index) then index else if Any..isexception(val) then val - else if !(Any..isfrom_Dict(dictOrList) && Any..isfrom_string(index)) && !(Any..isfrom_ListAny(dictOrList) && Any..isfrom_int(index)) then + else if !(Any..isfrom_DictStrAny(dictOrList) && Any..isfrom_str(index)) && !(Any..isfrom_ListAny(dictOrList) && Any..isfrom_int(index)) then exception (TypeError("Invalid subscription type")) - else if Any..isfrom_Dict(dictOrList) && Any..isfrom_string(index) then - from_Dict(DictStrAny_insert(Any..as_Dict!(dictOrList), Any..as_string!(index), val)) + else if Any..isfrom_DictStrAny(dictOrList) && Any..isfrom_str(index) then + from_DictStrAny(DictStrAny_insert(Any..as_Dict!(dictOrList), Any..as_string!(index), val)) else if Any..isfrom_ListAny(dictOrList) && Any..isfrom_int(index) && Any..as_int!(index) >= 0 && Any..as_int!(index) < List_len(Any..as_ListAny!(dictOrList)) then from_ListAny(List_set(Any..as_ListAny!(dictOrList), Any..as_int!(index), val)) else @@ -502,10 +502,10 @@ function Any_sets (indices: ListAny, dictOrList: Any, val: Any): Any }; function PIn (v: Any, dictOrList: Any) : Any - requires (Any..isfrom_Dict(dictOrList) && Any..isfrom_string(v)) || Any..isfrom_ListAny(dictOrList) + requires (Any..isfrom_DictStrAny(dictOrList) && Any..isfrom_str(v)) || Any..isfrom_ListAny(dictOrList) { from_bool( - if Any..isfrom_Dict(dictOrList) then + if Any..isfrom_DictStrAny(dictOrList) then DictStrAny_contains(Any..as_Dict!(dictOrList), Any..as_string!(v)) else List_contains(Any..as_ListAny!(dictOrList), v) @@ -513,10 +513,10 @@ function PIn (v: Any, dictOrList: Any) : Any }; function PNotIn ( v: Any, dictOrList: Any) : Any - requires (Any..isfrom_Dict(dictOrList) && Any..isfrom_string(v)) || Any..isfrom_ListAny(dictOrList) + requires (Any..isfrom_DictStrAny(dictOrList) && Any..isfrom_str(v)) || Any..isfrom_ListAny(dictOrList) { from_bool( - if Any..isfrom_Dict(dictOrList) then + if Any..isfrom_DictStrAny(dictOrList) then !DictStrAny_contains(Any..as_Dict!(dictOrList), Any..as_string!(v)) else !List_contains(Any..as_ListAny!(dictOrList), v) @@ -583,7 +583,7 @@ function PNot (v: Any) : Any from_bool(!(Any..as_int!(v) == 0)) else if Any..isfrom_float(v) then from_bool(!(Any..as_float!(v) == 0.0)) - else if Any..isfrom_string(v) then + else if Any..isfrom_str(v) then from_bool(!(Any..as_string!(v) == "")) else if Any..isfrom_ListAny(v) then from_bool(!(List_len(Any..as_ListAny!(v)) == 0)) @@ -616,8 +616,8 @@ function PAdd (v1: Any, v2: Any) : Any from_float(Any..as_float!(v1) + int_to_real(Any..as_int!(v2)) ) else if Any..isfrom_float(v1) && Any..isfrom_float(v2) then from_float(Any..as_float!(v1) + Any..as_float!(v2)) - else if Any..isfrom_string(v1) && Any..isfrom_string(v2) then - from_string(Str.Concat(Any..as_string!(v1),Any..as_string!(v2))) + else if Any..isfrom_str(v1) && Any..isfrom_str(v2) then + from_str(Str.Concat(Any..as_string!(v1),Any..as_string!(v2))) else if Any..isfrom_ListAny(v1) && Any..isfrom_ListAny(v2) then from_ListAny(List_extend(Any..as_ListAny!(v1),Any..as_ListAny!(v2))) else if Any..isfrom_datetime(v1) && Any..isfrom_int(v2) then @@ -670,20 +670,20 @@ function PMul (v1: Any, v2: Any) : Any from_float(bool_to_real(Any..as_bool!(v1)) * Any..as_float!(v2)) else if Any..isfrom_float(v1) && Any..isfrom_bool(v2) then from_float(Any..as_float!(v1) * bool_to_real(Any..as_bool!(v2))) - else if Any..isfrom_bool(v1) && Any..isfrom_string(v2) then - if Any..as_bool!(v1) then v2 else from_string("") - else if Any..isfrom_string(v1) && Any..isfrom_bool(v2) then - if Any..as_bool!(v2) then v1 else from_string("") + else if Any..isfrom_bool(v1) && Any..isfrom_str(v2) then + if Any..as_bool!(v1) then v2 else from_str("") + else if Any..isfrom_str(v1) && Any..isfrom_bool(v2) then + if Any..as_bool!(v2) then v1 else from_str("") else if Any..isfrom_int(v1) && Any..isfrom_int(v2) then from_int(Any..as_int!(v1) * Any..as_int!(v2)) else if Any..isfrom_int(v1) && Any..isfrom_float(v2) then from_float(int_to_real(Any..as_int!(v1)) * Any..as_float!(v2)) else if Any..isfrom_float(v1) && Any..isfrom_int(v2) then from_float(Any..as_float!(v1) * int_to_real(Any..as_int!(v2)) ) - else if Any..isfrom_int(v1) && Any..isfrom_string(v2) then - from_string(string_repeat(Any..as_string!(v2), Any..as_int!(v1))) - else if Any..isfrom_string(v1) && Any..isfrom_int(v2) then - from_string(string_repeat(Any..as_string!(v1), Any..as_int!(v2))) + else if Any..isfrom_int(v1) && Any..isfrom_str(v2) then + from_str(string_repeat(Any..as_string!(v2), Any..as_int!(v1))) + else if Any..isfrom_str(v1) && Any..isfrom_int(v2) then + from_str(string_repeat(Any..as_string!(v1), Any..as_int!(v2))) else if Any..isfrom_int(v1) && Any..isfrom_ListAny(v2) then from_ListAny(List_repeat(Any..as_ListAny!(v2), Any..as_int!(v1))) else if Any..isfrom_ListAny(v1) && Any..isfrom_int(v2) then @@ -744,7 +744,7 @@ function PLt (v1: Any, v2: Any) : Any from_bool(Any..as_float!(v1) < int_to_real(Any..as_int!(v2))) else if Any..isfrom_float(v1) && Any..isfrom_float(v2) then from_bool(Any..as_float!(v1) < Any..as_float!(v2)) - else if Any..isfrom_string(v1) && Any..isfrom_string(v2) then + else if Any..isfrom_str(v1) && Any..isfrom_str(v2) then from_bool(string_lt(Any..as_string!(v1), Any..as_string!(v2))) else if Any..isfrom_ListAny(v1) && Any..isfrom_ListAny(v2) then from_bool(List_lt(Any..as_ListAny!(v1),Any..as_ListAny!(v2))) @@ -775,7 +775,7 @@ function PLe (v1: Any, v2: Any) : Any from_bool(Any..as_float!(v1) <= int_to_real(Any..as_int!(v2))) else if Any..isfrom_float(v1) && Any..isfrom_float(v2) then from_bool(Any..as_float!(v1) <= Any..as_float!(v2)) - else if Any..isfrom_string(v1) && Any..isfrom_string(v2) then + else if Any..isfrom_str(v1) && Any..isfrom_str(v2) then from_bool(string_le(Any..as_string!(v1), Any..as_string!(v2))) else if Any..isfrom_ListAny(v1) && Any..isfrom_ListAny(v2) then from_bool(List_le(Any..as_ListAny!(v1),Any..as_ListAny!(v2))) @@ -806,7 +806,7 @@ function PGt (v1: Any, v2: Any) : Any from_bool(Any..as_float!(v1) > int_to_real(Any..as_int!(v2))) else if Any..isfrom_float(v1) && Any..isfrom_float(v2) then from_bool(Any..as_float!(v1) > Any..as_float!(v2)) - else if Any..isfrom_string(v1) && Any..isfrom_string(v2) then + else if Any..isfrom_str(v1) && Any..isfrom_str(v2) then from_bool(string_gt(Any..as_string!(v1), Any..as_string!(v2))) else if Any..isfrom_ListAny(v1) && Any..isfrom_ListAny(v2) then from_bool(List_gt(Any..as_ListAny!(v1),Any..as_ListAny!(v2))) @@ -837,7 +837,7 @@ function PGe (v1: Any, v2: Any) : Any from_bool(Any..as_float!(v1) >= int_to_real(Any..as_int!(v2))) else if Any..isfrom_float(v1) && Any..isfrom_float(v2) then from_bool(Any..as_float!(v1) >= Any..as_float!(v2)) - else if Any..isfrom_string(v1) && Any..isfrom_string(v2) then + else if Any..isfrom_str(v1) && Any..isfrom_str(v2) then from_bool(string_ge(Any..as_string!(v1), Any..as_string!(v2))) else if Any..isfrom_ListAny(v1) && Any..isfrom_ListAny(v2) then from_bool(List_ge(Any..as_ListAny!(v1),Any..as_ListAny!(v2))) @@ -860,13 +860,13 @@ function PNEq (v: Any, v': Any) : Any { // ///////////////////////////////////////////////////////////////////////////////////// function PAnd (v1: Any, v2: Any) : Any - requires (Any..isfrom_bool(v1) || Any..isfrom_none(v1) || Any..isfrom_string(v1) || Any..isfrom_int(v1)) + requires (Any..isfrom_bool(v1) || Any..isfrom_None(v1) || Any..isfrom_str(v1) || Any..isfrom_int(v1)) { if ! Any_to_bool (v1) then v1 else v2 }; function POr (v1: Any, v2: Any) : Any - requires (Any..isfrom_bool(v1) || Any..isfrom_none(v1) || Any..isfrom_string(v1) || Any..isfrom_int(v1)) + requires (Any..isfrom_bool(v1) || Any..isfrom_None(v1) || Any..isfrom_str(v1) || Any..isfrom_int(v1)) { if Any_to_bool (v1) then v1 else v2 }; @@ -911,14 +911,14 @@ function PMod (v1: Any, v2: Any) : Any function to_string(a: Any) : string; function to_string_any(a: Any) : Any { - from_string(to_string(a)) + from_str(to_string(a)) }; function datetime_strptime(dtstring: Any, format: Any) : Any; procedure datetime_tostring_cancel(dt: Any) - invokeOn datetime_strptime(to_string_any(dt), from_string ("%Y-%m-%d")) - ensures datetime_strptime(to_string_any(dt), from_string ("%Y-%m-%d")) == dt; + invokeOn datetime_strptime(to_string_any(dt), from_str ("%Y-%m-%d")) + ensures datetime_strptime(to_string_any(dt), from_str ("%Y-%m-%d")) == dt; procedure datetime_date(d: Any) returns (ret: Any, error: Error) requires Any..isfrom_datetime(d) summary "(Origin_datetime_date_Requires)d_type" @@ -932,7 +932,7 @@ procedure datetime_date(d: Any) returns (ret: Any, error: Error) error := NoError() } else { - ret := from_none(); + ret := from_None(); error := TypeError("Input must be datetime") } }; @@ -945,8 +945,8 @@ procedure datetime_now() returns (ret: Any) }; procedure timedelta_func(days: Any, hours: Any) returns (delta : Any, maybe_except: Error) - requires Any..isfrom_none(days) || Any..isfrom_int(days) summary "(Origin_timedelta_Requires)" - requires Any..isfrom_none(hours) || Any..isfrom_int(hours) summary "(Origin_timedelta_Requires)hours_type" + requires Any..isfrom_None(days) || Any..isfrom_int(days) summary "(Origin_timedelta_Requires)" + requires Any..isfrom_None(hours) || Any..isfrom_int(hours) summary "(Origin_timedelta_Requires)hours_type" requires Any..isfrom_int(days) ==> Any..as_int!(days)>=0 summary "(Origin_timedelta_Requires)days_pos" requires Any..isfrom_int(hours) ==> Any..as_int!(hours)>=0 summary "(Origin_timedelta_Requires)hours_pos" ensures Any..isfrom_int(delta) && Any..as_int!(delta)>=0 summary "ret_pos" @@ -967,14 +967,14 @@ procedure timedelta_func(days: Any, hours: Any) returns (delta : Any, maybe_exce // ///////////////////////////////////////////////////////////////////////////////////// procedure test_helper_procedure(req_name : Any, opt_name : Any) returns (ret: Any, maybe_except: Error) - requires req_name == from_string("foo") summary "(Origin_test_helper_procedure_Requires)req_name_is_foo" - requires (Any..isfrom_none(opt_name)) || (Any..isfrom_string(opt_name)) summary "(Origin_test_helper_procedure_Requires)req_opt_name_none_or_str" - requires (opt_name == from_none()) || (opt_name == from_string("bar")) summary "(Origin_test_helper_procedure_Requires)req_opt_name_none_or_bar" + requires req_name == from_str("foo") summary "(Origin_test_helper_procedure_Requires)req_name_is_foo" + requires (Any..isfrom_None(opt_name)) || (Any..isfrom_str(opt_name)) summary "(Origin_test_helper_procedure_Requires)req_opt_name_none_or_str" + requires (opt_name == from_None()) || (opt_name == from_str("bar")) summary "(Origin_test_helper_procedure_Requires)req_opt_name_none_or_bar" ensures (Error..isNoError(maybe_except)) summary "ensures_maybe_except_none" { - assert req_name == from_string("foo") summary "assert_name_is_foo"; - assert (Any..isfrom_none(opt_name)) || (Any..isfrom_string(opt_name)) summary "assert_opt_name_none_or_str"; - assert (opt_name == from_none()) || (opt_name == from_string("bar")) summary "assert_opt_name_none_or_bar"; + assert req_name == from_str("foo") summary "assert_name_is_foo"; + assert (Any..isfrom_None(opt_name)) || (Any..isfrom_str(opt_name)) summary "assert_opt_name_none_or_str"; + assert (opt_name == from_None()) || (opt_name == from_str("bar")) summary "assert_opt_name_none_or_bar"; assume (Error..isNoError(maybe_except)) // summary "assume_maybe_except_none" }; From ce46cdf2f7701c8bdfbbff8579955431ceb7c366 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Wed, 1 Apr 2026 09:36:56 -0700 Subject: [PATCH 29/31] rewrite code of some functions for better mantainance --- Strata/Languages/Python/PythonToLaurel.lean | 51 ++++++++++----------- 1 file changed, 23 insertions(+), 28 deletions(-) diff --git a/Strata/Languages/Python/PythonToLaurel.lean b/Strata/Languages/Python/PythonToLaurel.lean index 5b66c89b1..3b0555ba2 100644 --- a/Strata/Languages/Python/PythonToLaurel.lean +++ b/Strata/Languages/Python/PythonToLaurel.lean @@ -205,12 +205,18 @@ def PyLauType.None := "None" def PyLauType.Int := "int" def PyLauType.Bool := "bool" def PyLauType.Str := "str" +def PyLauType.Float := "float" +def PyLauType.Bytes := "bytes" def PyLauType.Datetime := "datetime" def PyLauType.DictStrAny := "DictStrAny" +def PyLauType.ListAny := "ListAny" def PyLauType.ListStr := "ListStr" def PyLauType.Package := "Package" def PyLauType.Any := "Any" +def isOfAnyType (ty: String): Bool := ty ∈ [PyLauType.None, PyLauType.Bool, PyLauType.Int, PyLauType.Float, + PyLauType.Str, PyLauType.Datetime, PyLauType.Bytes, PyLauType.ListAny, PyLauType.DictStrAny, PyLauType.Any] + def PyLauFuncReturnVar := "LaurelResult" /-- Convert a Laurel HighType to a PyLauType string for type inference. -/ @@ -272,10 +278,10 @@ def compositeToStringAnyName (typeName : String) : String := "$composite_to_stri def isCompositeType (ctx : TranslationContext) (typeName : String) : Bool := typeName != PyLauType.Any && (ctx.importedSymbols[typeName]?.any fun s => match s with | .compositeType _ => true | _ => false) -def strToAny (s: String) := mkStmtExprMd (.StaticCall "from_string" [mkStmtExprMd (StmtExpr.LiteralString s)]) +def strToAny (s: String) := mkStmtExprMd (.StaticCall "from_str" [mkStmtExprMd (StmtExpr.LiteralString s)]) def intToAny (i: Int) := mkStmtExprMd (.StaticCall "from_int" [mkStmtExprMd (StmtExpr.LiteralInt i)]) def boolToAny (b: Bool) := mkStmtExprMd (.StaticCall "from_bool" [mkStmtExprMd (StmtExpr.LiteralBool b)]) -def AnyNone := mkStmtExprMd (.StaticCall "from_none" []) +def AnyNone := mkStmtExprMd (.StaticCall "from_None" []) def Any_to_bool (b: StmtExprMd) := mkStmtExprMd (.StaticCall "Any_to_bool" [b]) /-- Wrap a field access expression in the appropriate Any constructor based on HighType. @@ -287,7 +293,7 @@ def wrapFieldInAny (ty : HighType) (expr : StmtExprMd) : Except TranslationError | .TBool => .ok <| mkStmtExprMd (.StaticCall "from_bool" [expr]) | .TFloat64 => .ok <| mkStmtExprMd (.StaticCall "from_float" [expr]) | .TReal => .ok <| mkStmtExprMd (.StaticCall "from_float" [expr]) - | .TString => .ok <| mkStmtExprMd (.StaticCall "from_string" [expr]) + | .TString => .ok <| mkStmtExprMd (.StaticCall "from_str" [expr]) | .TCore "Any" => .ok expr | .UserDefined name => .error (.unsupportedConstruct s!"Coercion from user-defined class '{name.text}' to Any is not yet supported" name.text) @@ -332,8 +338,8 @@ def DictStrAny_empty:= mkStmtExprMd (StmtExpr.StaticCall "DictStrAny_empty" []) def DictStrAny_mk (kv: List (String × StmtExprMd)) := DictStrAny_mk_aux kv DictStrAny_empty /-- Extract a value from a dictionary for a function parameter. - For required params, generates `Any_get(dict, from_string(key))` (with precondition). - For optional params, generates `Any_get_or_none(dict, from_string(key))` (returns `None` if absent). + For required params, generates `Any_get(dict, from_str(key))` (with precondition). + For optional params, generates `Any_get_or_none(dict, from_str(key))` (returns `None` if absent). Both operate on `Any`-typed dictionaries. -/ def DictStrAny_get_param (dict : StmtExprMd) (key : String) (isOptional : Bool) : StmtExprMd := let func := if isOptional then "Any_get_or_none" else "Any_get" @@ -404,7 +410,7 @@ partial def translateDictStrAny (ctx : TranslationContext) let kv := keys.zip values let val_trans ← kv.unzip.snd.mapM (translateExpr ctx) let keys ← keys.mapM pyOptExprToString - return mkStmtExprMd (.StaticCall "from_Dict" [DictStrAny_mk (keys.zip val_trans)]) + return mkStmtExprMd (.StaticCall "from_DictStrAny" [DictStrAny_mk (keys.zip val_trans)]) partial def translateSlice (ctx : TranslationContext) (start stop step: Option (expr SourceRange)) : Except TranslationError StmtExprMd := do @@ -557,7 +563,7 @@ partial def translateExpr (ctx : TranslationContext) (e : Python.expr SourceRang let concat := parts.foldl (fun acc part => mkStmtExprMd (.PrimitiveOp .StrConcat [acc, unwrap part])) (mkStmtExprMd (.LiteralString "")) - return mkStmtExprMd (.StaticCall "from_string" [concat]) + return mkStmtExprMd (.StaticCall "from_str" [concat]) -- Interpolation / TemplateStr (Python 3.14+ t-strings) - not yet supported | .Interpolation .. => return mkStmtExprMd .Hole @@ -824,7 +830,7 @@ partial def combinePositionalAndKeywordArgs let missingArgs := unprovidedPosArgs.filter fun arg => !(arg.name ∈ kwords.keys) && arg.default.isNone if missingArgs.length > 0 then - let missingNames := missingArgs.map (·.1) + let missingNames := missingArgs.map (·.name) throwUserError callRange s!"'{name}' called with missing required arguments: {missingNames}" let filledPosArgs ← unprovidedPosArgs.mapM (λ arg => @@ -1391,8 +1397,6 @@ def getUnionTypes (arg: Python.expr SourceRange) : List (Python.expr SourceRange | .BinOp _ left _ right => getUnionTypes left ++ getUnionTypes right | _ => [arg] -def isOfAnyType (ty: String): Bool := ty ∈ ["None", "bool", "int", "str", "float", "datetime", "bytes", "ListAny", "DictStrAny", "Any"] - def checkValidInputTypeList (ctx : TranslationContext) (tys: List String) : Except TranslationError (List String) := do for ty in tys do let _ ← translateType ctx ty @@ -1421,6 +1425,7 @@ partial def getArgumentTypes (arg: Python.expr SourceRange) : Except Translation | .Constant _ _ _ => return ["None"] | .Attribute _ _ _ _ => return [pyExprToString arg] | .BinOp _ _ _ _ => return (← (getUnionTypes arg).mapM getArgumentTypes).flatten + --Temporary: just to handle "typing:some_type ... " | .Slice _ lower upper _ => match lower.val, upper.val with | some (.Name _ _ _ ), some upper => getArgumentTypes upper | _, _ => throw (.internalError s!"Unhandled Expr: {repr arg}") @@ -1486,17 +1491,7 @@ def pyFuncDefToPythonFunctionDecl (ctx : TranslationContext) (f : Python.stmt S | _ => throw (.internalError "Expected FunctionDef") def getSingleTypeConstraint (var: String) (ty: String): Option StmtExprMd := - match ty with - | "str" => mkStmtExprMd (.StaticCall "Any..isfrom_string" [freeVar var]) - | "int" => mkStmtExprMd (.StaticCall "Any..isfrom_int" [freeVar var]) - | "bool" => mkStmtExprMd (.StaticCall "Any..isfrom_bool" [freeVar var]) - | "float" => mkStmtExprMd (.StaticCall "Any..isfrom_float" [freeVar var]) - | "datetime" => mkStmtExprMd (.StaticCall "Any..isfrom_datetime" [freeVar var]) - | "bytes" => mkStmtExprMd (.StaticCall "Any..isfrom_bytes" [freeVar var]) - | "None" => mkStmtExprMd (.StaticCall "Any..isfrom_none" [freeVar var]) - | "ListAny" => mkStmtExprMd (.StaticCall "Any..isfrom_ListAny" [freeVar var]) - | "DictStrAny" => mkStmtExprMd (.StaticCall "Any..isfrom_Dict" [freeVar var]) - | _ => none + if isOfAnyType ty && ty ≠ "Any" then mkStmtExprMd (.StaticCall ("Any..isfrom_" ++ ty) [freeVar var]) else none def createBoolOrExpr (exprs: List StmtExprMd) : StmtExprMd := match exprs with @@ -1511,13 +1506,12 @@ def getUnionTypeConstraint (var: String) (md: MetaData) (tys: List String) (func some {createBoolOrExpr type_constraints with md:=md} def getReturnTypeEnsure (md: MetaData) (tys: List String) (funcname: String): Option StmtExprMd := - let type_constraints := tys.filterMap (getSingleTypeConstraint PyLauFuncReturnVar) - if type_constraints.isEmpty then none else - let md: MetaData := md.withPropertySummary $ "(" ++ funcname ++ " ensures) Return type constraint" - some {createBoolOrExpr type_constraints with md:=md} + getUnionTypeConstraint PyLauFuncReturnVar md tys funcname + |>.map fun c => {c with md := md.withPropertySummary $ "(" ++ funcname ++ " ensures) Return type constraint"} def getInputTypePreconditions (funcDecl : PythonFunctionDecl): List StmtExprMd := funcDecl.args.filterMap (λ arg => getUnionTypeConstraint arg.name arg.md arg.tys funcDecl.name) + /-- Translate a Python function body: collect all variable declarations, hoist them to the top, and translate the remaining statements. --/ def translateFunctionBody (ctx : TranslationContext) (inputTypes : List (String × String)) (body: List (Python.stmt SourceRange)) @@ -1552,8 +1546,9 @@ def translateFunction (ctx : TranslationContext) (sourceRange: SourceRange) (fun match funcDecl.ret.map fun (tys, md) => getReturnTypeEnsure md tys funcDecl.name with | some (some constraint) => [constraint] | _ => [] - -- Declare an output parameter when the function has a return type annotation. - -- Return statements explicitly assign to LaurelResult and exit $body. + + -- Translate return type + -- All methods return Any (void methods return Any via from_None) let outputs : List Parameter := [{ name := PyLauFuncReturnVar, type := AnyTy }] -- Translate function body @@ -1677,7 +1672,7 @@ def translateMethod (ctx : TranslationContext) (className : String) | _ => pure () -- Translate return type - -- All methods return Any (void methods return Any via from_none) + -- All methods return Any (void methods return Any via from_None) let outputs : List Parameter := [{name := "LaurelResult", type := AnyTy}] -- Translate method body with class context From 035b6db0bbeeb761e08d81c2bf2635f2c97c1fd4 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Wed, 1 Apr 2026 10:15:29 -0700 Subject: [PATCH 30/31] fix CI fails --- Strata/Languages/Python/Specs/ToLaurel.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Strata/Languages/Python/Specs/ToLaurel.lean b/Strata/Languages/Python/Specs/ToLaurel.lean index f4edd619f..b01516325 100644 --- a/Strata/Languages/Python/Specs/ToLaurel.lean +++ b/Strata/Languages/Python/Specs/ToLaurel.lean @@ -359,7 +359,7 @@ partial def specExprToLaurel (e : SpecExpr) (md : Imperative.MetaData Core.Expre | .var "kwargs" => -- containsKey(kwargs, "key") → parameter was provided (not None) return some (mkStmt (.PrimitiveOp .Not - [mkStmt (.StaticCall (mkId "Any..isfrom_none") [mkStmt (.Identifier (mkId key)) md]) md]) + [mkStmt (.StaticCall (mkId "Any..isfrom_None") [mkStmt (.Identifier (mkId key)) md]) md]) md) | _ => let c? ← specExprToLaurel container md @@ -396,7 +396,7 @@ def buildSpecBody (preconditions : Array Assertion) -- Assert that required parameters are provided (not None) for param in requiredParams do let cond := mkStmt (.PrimitiveOp .Not - [mkStmt (.StaticCall (mkId "Any..isfrom_none") + [mkStmt (.StaticCall (mkId "Any..isfrom_None") [mkStmt (.Identifier (mkId param)) md]) md]) md let assertStmt ← mkStmtWithLoc (.Assert cond) default s!"Required parameter '{param}' is missing" stmts := assertStmt :: stmts From e317d55a0b891d555060dc332a1ecb17e37114b4 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Wed, 1 Apr 2026 10:17:44 -0700 Subject: [PATCH 31/31] fix verifyprelude output --- StrataTest/Languages/Python/PreludeVerifyTest.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/StrataTest/Languages/Python/PreludeVerifyTest.lean b/StrataTest/Languages/Python/PreludeVerifyTest.lean index 728543dcf..81007ba18 100644 --- a/StrataTest/Languages/Python/PreludeVerifyTest.lean +++ b/StrataTest/Languages/Python/PreludeVerifyTest.lean @@ -157,15 +157,15 @@ Obligation: postcondition Property: assert Result: ✅ pass -Obligation: assert(41796) +Obligation: assert(41763) Property: assert Result: ✅ pass -Obligation: assert(41866) +Obligation: assert(41830) Property: assert Result: ✅ pass -Obligation: assert(41977) +Obligation: assert(41938) Property: assert Result: ✅ pass