From c222a3d9bb088d5ad0892d0a43415c754656c6f4 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 5 May 2026 14:59:13 +0000 Subject: [PATCH 1/3] Add resolution diagnostic for multi-output procedure in expression position When a StaticCall to a multi-output procedure appears in expression position (not as the RHS of an Assign), emit an error diagnostic: the extra outputs would be silently discarded, which is a semantic bug (e.g., error channels lost). The diagnostic is suppressed when the call is the direct RHS of an assignment (where the target count check already validates arity). Includes a test in ResolutionKindTests demonstrating the diagnostic. Co-authored-by: Kiro --- Strata/Languages/Laurel/Resolution.lean | 21 +++++++++++++++++++ .../Languages/Laurel/ResolutionKindTests.lean | 13 ++++++++++++ 2 files changed, 34 insertions(+) diff --git a/Strata/Languages/Laurel/Resolution.lean b/Strata/Languages/Laurel/Resolution.lean index 16bcf1333f..df2840e6f9 100644 --- a/Strata/Languages/Laurel/Resolution.lean +++ b/Strata/Languages/Laurel/Resolution.lean @@ -213,6 +213,8 @@ structure ResolveState where /-- When resolving inside an instance procedure, the owning composite type name. Used by `resolveFieldRef` to resolve `self.field` when `self` has type `Any`. -/ instanceTypeName : Option String := none + /-- True when resolving the RHS of an Assign statement (suppresses multi-output diagnostic). -/ + inAssignRhs : Bool := false @[expose] abbrev ResolveM := StateM ResolveState @@ -402,7 +404,10 @@ def resolveStmtExpr (exprMd : StmtExprMd) : ResolveM StmtExprMd := do let ty' ← resolveHighType param.type let name' ← defineNameCheckDup param.name (.var param.name ty') pure (⟨.Declare ⟨name', ty'⟩, vs⟩ : VariableMd) + let savedFlag := (← get).inAssignRhs + modify fun s => { s with inAssignRhs := true } let value' ← resolveStmtExpr value + modify fun s => { s with inAssignRhs := savedFlag } -- Check that LHS target count matches the number of outputs from the RHS. -- This fires for procedure calls (which can have multiple outputs). -- Functions always have exactly 1 output in the model, so single-target function calls pass trivially. @@ -438,6 +443,22 @@ def resolveStmtExpr (exprMd : StmtExprMd) : ResolveM StmtExprMd := do let callee' ← resolveRef callee source (expected := #[.parameter, .staticProcedure, .datatypeConstructor, .constant]) let args' ← args.mapM resolveStmtExpr + -- Multi-output procedures must not appear in expression position: the extra + -- outputs (e.g. error channels) would be silently discarded. + let s ← get + if !s.inAssignRhs then + match s.scope.get? callee'.text with + | some (_, .staticProcedure proc) => + if proc.outputs.length > 1 then + let diag := diagnosticFromSource source + s!"Multi-output procedure '{callee'.text}' used in expression position; it returns {proc.outputs.length} values but only one can be used here. Use a multi-target assignment instead." + modify fun s => { s with errors := s.errors.push diag } + | some (_, .instanceProcedure _ proc) => + if proc.outputs.length > 1 then + let diag := diagnosticFromSource source + s!"Multi-output procedure '{callee'.text}' used in expression position; it returns {proc.outputs.length} values but only one can be used here. Use a multi-target assignment instead." + modify fun s => { s with errors := s.errors.push diag } + | _ => pure () pure (.StaticCall callee' args') | .PrimitiveOp op args => let args' ← args.mapM resolveStmtExpr diff --git a/StrataTest/Languages/Laurel/ResolutionKindTests.lean b/StrataTest/Languages/Laurel/ResolutionKindTests.lean index acbef556b6..6c58bcd573 100644 --- a/StrataTest/Languages/Laurel/ResolutionKindTests.lean +++ b/StrataTest/Languages/Laurel/ResolutionKindTests.lean @@ -97,4 +97,17 @@ composite Foo extends nat { } #guard_msgs (error, drop all) in #eval testInputWithOffset "ExtendConstrained" extendConstrained 90 processResolution +/-! ## Multi-output procedure used in expression position -/ + +def multiOutputInExpr := r" +procedure multi(x: int) returns (a: int, b: int) opaque; +procedure test() opaque { + assert multi(1) == 1 +// ^^^^^^^^ error: Multi-output procedure 'multi' used in expression position +}; +" + +#guard_msgs (error, drop all) in +#eval testInputWithOffset "MultiOutputInExpr" multiOutputInExpr 100 processResolution + end Laurel From 352fdf81c6d974c37d10b08f52f53c5c72941476 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 5 May 2026 17:43:48 +0000 Subject: [PATCH 2/3] Replace inAssignRhs with inValueContext for precise diagnostic scoping Address review feedback: - Replace coarse inAssignRhs flag with inValueContext that is set when recursing into arguments of StaticCall/PrimitiveOp. This correctly diagnoses nested multi-output calls (e.g., f(multi(1))) while not firing for statement-position calls or direct assignment RHS. - Factor out duplicate staticProcedure/instanceProcedure branches into a single outputCount lookup. Co-authored-by: Kiro --- Strata/Languages/Laurel/Resolution.lean | 41 +++++++++++++------------ 1 file changed, 22 insertions(+), 19 deletions(-) diff --git a/Strata/Languages/Laurel/Resolution.lean b/Strata/Languages/Laurel/Resolution.lean index df2840e6f9..2a44c7a595 100644 --- a/Strata/Languages/Laurel/Resolution.lean +++ b/Strata/Languages/Laurel/Resolution.lean @@ -213,8 +213,10 @@ structure ResolveState where /-- When resolving inside an instance procedure, the owning composite type name. Used by `resolveFieldRef` to resolve `self.field` when `self` has type `Any`. -/ instanceTypeName : Option String := none - /-- True when resolving the RHS of an Assign statement (suppresses multi-output diagnostic). -/ - inAssignRhs : Bool := false + /-- True when resolving inside an expression where the value is used (e.g., as an + argument to another call or operator). Multi-output calls are only diagnosed + in value context, not in statement position or direct assignment RHS. -/ + inValueContext : Bool := false @[expose] abbrev ResolveM := StateM ResolveState @@ -404,10 +406,7 @@ def resolveStmtExpr (exprMd : StmtExprMd) : ResolveM StmtExprMd := do let ty' ← resolveHighType param.type let name' ← defineNameCheckDup param.name (.var param.name ty') pure (⟨.Declare ⟨name', ty'⟩, vs⟩ : VariableMd) - let savedFlag := (← get).inAssignRhs - modify fun s => { s with inAssignRhs := true } let value' ← resolveStmtExpr value - modify fun s => { s with inAssignRhs := savedFlag } -- Check that LHS target count matches the number of outputs from the RHS. -- This fires for procedure calls (which can have multiple outputs). -- Functions always have exactly 1 output in the model, so single-target function calls pass trivially. @@ -442,26 +441,30 @@ def resolveStmtExpr (exprMd : StmtExprMd) : ResolveM StmtExprMd := do | .StaticCall callee args => let callee' ← resolveRef callee source (expected := #[.parameter, .staticProcedure, .datatypeConstructor, .constant]) + -- Resolve arguments in value context (their results are used as values) + let saved := (← get).inValueContext + modify fun s => { s with inValueContext := true } let args' ← args.mapM resolveStmtExpr - -- Multi-output procedures must not appear in expression position: the extra + modify fun s => { s with inValueContext := saved } + -- Multi-output procedures must not appear in value context: the extra -- outputs (e.g. error channels) would be silently discarded. let s ← get - if !s.inAssignRhs then - match s.scope.get? callee'.text with - | some (_, .staticProcedure proc) => - if proc.outputs.length > 1 then - let diag := diagnosticFromSource source - s!"Multi-output procedure '{callee'.text}' used in expression position; it returns {proc.outputs.length} values but only one can be used here. Use a multi-target assignment instead." - modify fun s => { s with errors := s.errors.push diag } - | some (_, .instanceProcedure _ proc) => - if proc.outputs.length > 1 then - let diag := diagnosticFromSource source - s!"Multi-output procedure '{callee'.text}' used in expression position; it returns {proc.outputs.length} values but only one can be used here. Use a multi-target assignment instead." - modify fun s => { s with errors := s.errors.push diag } - | _ => pure () + if s.inValueContext then + let outputCount := match s.scope.get? callee'.text with + | some (_, .staticProcedure proc) => proc.outputs.length + | some (_, .instanceProcedure _ proc) => proc.outputs.length + | _ => 0 + if outputCount > 1 then + let diag := diagnosticFromSource source + s!"Multi-output procedure '{callee'.text}' used in expression position; it returns {outputCount} values but only one can be used here. Use a multi-target assignment instead." + modify fun s => { s with errors := s.errors.push diag } pure (.StaticCall callee' args') | .PrimitiveOp op args => + -- Resolve arguments in value context + let saved := (← get).inValueContext + modify fun s => { s with inValueContext := true } let args' ← args.mapM resolveStmtExpr + modify fun s => { s with inValueContext := saved } pure (.PrimitiveOp op args') | .New ref => let ref' ← resolveRef ref source From 1713b147ed3e30758bf3540ef6b632249a59edaf Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 5 May 2026 17:57:39 +0000 Subject: [PATCH 3/3] Set inValueContext for assert, assume, if, and while conditions These are all value contexts where a multi-output procedure call would silently discard outputs. Co-authored-by: Kiro --- Strata/Languages/Laurel/Resolution.lean | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/Strata/Languages/Laurel/Resolution.lean b/Strata/Languages/Laurel/Resolution.lean index 2a44c7a595..71c1510d91 100644 --- a/Strata/Languages/Laurel/Resolution.lean +++ b/Strata/Languages/Laurel/Resolution.lean @@ -362,7 +362,10 @@ def resolveStmtExpr (exprMd : StmtExprMd) : ResolveM StmtExprMd := do | AstNode.mk expr source => let val' ← match _: expr with | .IfThenElse cond thenBr elseBr => + let saved := (← get).inValueContext + modify fun s => { s with inValueContext := true } let cond' ← resolveStmtExpr cond + modify fun s => { s with inValueContext := saved } let thenBr' ← resolveStmtExpr thenBr let elseBr' ← elseBr.attach.mapM (fun a => have := a.property; resolveStmtExpr a.val) pure (.IfThenElse cond' thenBr' elseBr') @@ -371,7 +374,10 @@ def resolveStmtExpr (exprMd : StmtExprMd) : ResolveM StmtExprMd := do let stmts' ← stmts.mapM resolveStmtExpr pure (.Block stmts' label) | .While cond invs dec body => + let saved := (← get).inValueContext + modify fun s => { s with inValueContext := true } let cond' ← resolveStmtExpr cond + modify fun s => { s with inValueContext := saved } let invs' ← invs.attach.mapM (fun a => have := a.property; resolveStmtExpr a.val) let dec' ← dec.attach.mapM (fun a => have := a.property; resolveStmtExpr a.val) let body' ← resolveStmtExpr body @@ -506,10 +512,16 @@ def resolveStmtExpr (exprMd : StmtExprMd) : ResolveM StmtExprMd := do let val' ← resolveStmtExpr val pure (.Fresh val') | .Assert ⟨condExpr, summary⟩ => + let saved := (← get).inValueContext + modify fun s => { s with inValueContext := true } let cond' ← resolveStmtExpr condExpr + modify fun s => { s with inValueContext := saved } pure (.Assert { condition := cond', summary }) | .Assume cond => + let saved := (← get).inValueContext + modify fun s => { s with inValueContext := true } let cond' ← resolveStmtExpr cond + modify fun s => { s with inValueContext := saved } pure (.Assume cond') | .ProveBy val proof => let val' ← resolveStmtExpr val