diff --git a/Strata/Languages/Laurel/Resolution.lean b/Strata/Languages/Laurel/Resolution.lean index cf32780f2b..cc3cf534eb 100644 --- a/Strata/Languages/Laurel/Resolution.lean +++ b/Strata/Languages/Laurel/Resolution.lean @@ -579,26 +579,30 @@ That list is bound on entry to a procedure body (by every other rule is independent of it. Several constructs are *statements*: their job is to have an effect, -not to produce a value. They are handled by `Synth.resolveStmtExpr` -and synthesize `TVoid`: - -- **Control-flow terminators** (`Exit`, `Return`): they jump somewhere - else and never hand a value back. -- **Effect-only forms** (`Assert`, `Assume`, `While`, `Var-Declare`): - they run and fall through without producing a value. - -In either case, `Check.statement` (the `⋄` judgment) simply -synthesizes and discards the type, so any expression — including -value-producing ones like calls — is admitted in statement position. +not to produce a value. Their check rules accept whatever type the +surrounding context expects — the rule is written with the expected +type `A` left as a free variable (we call this **check at any `A`**), +which just means the rule does not look at `A` at all. There are two +reasons a construct ignores `A`: + +- It is a **control-flow terminator** (`Exit`, `Return`): it jumps + somewhere else and never hands a value back, so whatever the + context wanted, the jump satisfies it vacuously. `if c then 5 else + return` is fine in an `Int` context because the `else` branch never + produces anything at all. +- It runs and then **falls through without a value** (`Assert`, + `Assume`, `While`, `Var-Declare`). These conceptually have the unit + type `TVoid`; accepting any `A` is a slight over-acceptance that is + harmless in practice because such statements only ever appear in + non-last (discard) position, which is checked at `TVoid` anyway. `Assign` is the one statement that *does* produce a value: it synthesizes the type of its right-hand side (so `x := e` can be used where that type is expected), and its check rule skips the \[⇐\] Sub boundary check only when the expected type is `TVoid` — i.e. when the assignment is used purely for effect. `Block` routes the surrounding -expected type to its last statement (the block's value); non-last -statements are in effect position (synthesized and discarded via -`Check.statement`). +expected type to its last statement (the block's value), not to the +non-last statements (which are effects, checked at `TVoid`). Each typing rule is implemented as its own helper inside the mutual block below. Helpers are grouped by section to mirror the *Typing @@ -622,7 +626,9 @@ rules* index in `LaurelDoc.lean`: - Holes — `Check.holeSome`, `Check.holeNone` The dispatch functions `Synth.resolveStmtExpr` and `Check.resolveStmtExpr` -pattern-match on the constructor and delegate to the corresponding helper. -/ +pattern-match on the constructor and delegate to the corresponding helper. +`Synth.resolveStmtExpr` is non-total: constructors without a synthesis rule +hit a wildcard arm that emits a diagnostic and returns `Unknown`. -/ namespace Resolution @@ -643,8 +649,10 @@ mutual /-- Synth-mode resolution: resolve `e` and synthesize its `HighType`, written `Γ ⊢ e ⇒ T`. Each constructor with a synthesis rule delegates - to its rule's helper. Statement-shaped constructs (`While`, `Exit`, - `Return`, `Assert`, `Assume`, `Var-Declare`) synthesize `TVoid`. + to its rule's helper; constructors without one (statement-shaped + constructs like `While`, `Exit`, `Return`, …) hit + a wildcard arm that emits a `typeMismatch` diagnostic and + returns `Unknown` to suppress cascading errors. Synthesis returns a type inferred from the expression itself; checking (`Check.resolveStmtExpr`) verifies that the expression has @@ -714,24 +722,12 @@ def Synth.resolveStmtExpr (exprMd : StmtExprMd) : ResolveM (StmtExprMd × HighTy | .Hole det (some ty) => let ty' ← resolveHighType ty pure (.Hole det (some ty'), ty') - | .Var (.Declare param) => do - let r ← Check.varDeclare param source - return (r, ⟨ .TVoid, source ⟩) - | .While cond invs dec body => do - let r ← Check.while exprMd cond invs dec body source (by rw [h_node]) - return (r, ⟨ .TVoid, source ⟩) - | .Exit target => do - let r ← Check.exit target source - return (r, ⟨ .TVoid, source ⟩) - | .Return val => do - let r ← Check.return exprMd val source (by rw [h_node]) - return (r, ⟨ .TVoid, source ⟩) - | .Assert ⟨condExpr, summary, free⟩ => do - let r ← Check.assert exprMd condExpr summary free source (by rw [h_node]) - return (r, ⟨ .TVoid, source ⟩) - | .Assume cond => do - let r ← Check.assume exprMd cond source (by rw [h_node]) - return (r, ⟨ .TVoid, source ⟩) + | _ => + let unknown : HighTypeMd := { val := .Unknown, source := source } + typeMismatch source (some expr) + "this expression's type cannot be synthesized; try to annotate it or use it in a context where there is an expected type" + unknown + pure (expr, unknown) return ({ val := val', source := source }, ty) termination_by (exprMd, 2) decreasing_by all_goals first @@ -780,6 +776,16 @@ def Check.resolveStmtExpr (exprMd : StmtExprMd) (expected : HighTypeMd) : Resolv Check.assign exprMd targets value expected source (by rw [h_node]) | .Hole det none => pure (Check.holeNone det expected source) | .Hole det (some ty) => Check.holeSome det ty expected source + | .Var (.Declare param) => Check.varDeclare param source + | .While cond invs dec body => + Check.while exprMd cond invs dec body source (by rw [h_node]) + | .Exit target => Check.exit target source + | .Return val => + Check.return exprMd val source (by rw [h_node]) + | .Assert ⟨condExpr, summary, free⟩ => + Check.assert exprMd condExpr summary free source (by rw [h_node]) + | .Assume cond => + Check.assume exprMd cond source (by rw [h_node]) | .Old val => Check.old exprMd val expected source (by rw [h_node]) | .ProveBy val proof => @@ -902,13 +908,14 @@ def Synth.varField (exprMd : StmtExprMd) /-- (Var-Declare) ``` x ∉ dom(Γ) - ──────────────────────────────────────────────────── - Γ ⊢ Var (.Declare ⟨x, T_x⟩) ⇒ TVoid ⊣ Γ, x : T_x + ──────────────────────────────────────────── + Γ ⊢ Var (.Declare ⟨x, T_x⟩) ⇐ A ⊣ Γ, x : T_x ``` `⊣ Γ, x : T_x` records that the surrounding scope is extended with the new binding for the remainder of the enclosing block. The declaration itself does no work other than registering `x : T_x`, - and yields no value, so it synthesizes `TVoid`. + and yields no value, so its rule accepts whatever type `A` the + context expects (the rule ignores `A`). `x ∉ dom(Γ)` is a soft side condition, not a hard premise: when `x` is already bound in the current scope, `defineNameCheckDup` emits a @@ -932,14 +939,15 @@ def Check.varDeclare (param : Parameter) (source : Option FileRange) : Numeric U Γ ⊢ body ⇐ Unknown ───────────────────────────────────────────────── - Γ ⊢ While cond invs decreases body ⇒ TVoid + Γ ⊢ While cond invs decreases body ⇐ A ``` `cond` is checked against `TBool`, and each invariant against `TBool`. The body's *value type* is discarded — control either re-enters the loop or falls through, so the body is checked at `Unknown` (the gradual wildcard) and any value the body's tail might produce is ignored. A loop is a statement: it yields no - value, so it synthesizes `TVoid`. + value, so its rule accepts whatever type `A` the context expects + (the rule ignores `A`). The optional `decreases` clause is synthesized and required to have a numeric type, via the same `Numeric U` predicate @@ -978,11 +986,15 @@ def Check.while (exprMd : StmtExprMd) ``` l ∈ Γ_lbl ─────────────────── - Γ ⊢ Exit l ⇒ TVoid + Γ ⊢ Exit l ⇐ A ``` `exit` is a control-flow terminator — an unconditional jump out of the enclosing labeled block. Because it never falls through, it - never delivers a value, so it synthesizes `TVoid`. + never delivers a value, so the rule accepts whatever type `A` the + context expects (the rule ignores `A`): an `exit` slots into any + position, even one expecting a value, since control leaves before + any value would be needed. Anything after `exit l` in the same + block is dead code, flagged by `Resolution.Check.block`. The premise `l ∈ Γ_lbl` requires the target label to name an enclosing labeled block; labels live in their own namespace @@ -1006,19 +1018,19 @@ def Check.exit (target : String) (source : Option FileRange) : ``` T_o-bar = [] (Return-None-Void) ───────────────────────── - Γ ⊢ Return none ⇒ TVoid + Γ ⊢ Return none ⇐ A T_o-bar = [T] (Return-None-Single) ────────────────────────────────── - Γ ⊢ Return none ⇒ TVoid + Γ ⊢ Return none ⇐ A T_o-bar = [T_1;…;T_n] n ≥ 2 (Return-None-Multi) ────────────────────────────────── - Γ ⊢ Return none ⇒ TVoid + Γ ⊢ Return none ⇐ A T_o-bar = [T] Γ ⊢ e ⇐ T (Return-Some) ────────────────────────────────── - Γ ⊢ Return (some e) ⇒ TVoid + Γ ⊢ Return (some e) ⇐ A T_o-bar = [] (Return-Void-Error) ─────────────────────────────────────────────────────────── @@ -1029,23 +1041,28 @@ def Check.exit (target : String) (source : Option FileRange) : Γ ⊢ Return (some e) ↝ "multi-output procedure cannot use 'return e'; assign to named outputs instead" ``` `return` is the *only* rule whose premises depend on the enclosing - procedure's declared outputs. It is a control-flow terminator: it - transfers control out of the enclosing procedure and never falls - through, so it synthesizes `TVoid`. The returned value, if any, is - checked against the procedure's declared output. Anything after - `return` in the same block is dead code, flagged by - `Resolution.Check.block`. + procedure's declared outputs. Like `Exit`, it is a control-flow + terminator: it transfers control out of the enclosing procedure and + never falls through to the surrounding block, so the rule accepts + whatever type `A` the context expects (the rule ignores `A`). The + returned value, if any, is checked against the procedure's declared + output rather than against `A`. Anything after `return` in the same + block is dead code, flagged by `Resolution.Check.block`. When `answerType = none` we are not inside any procedure body (e.g. resolving a constant initializer), so all `Return` checks are skipped — `Return` should not occur there in well-formed input. - `return;` (no payload) is unconditionally accepted in all cases: - void-output procedures (Return-None-Void), single-output procedures - (Return-None-Single), and multi-output procedures (Return-None-Multi). - In the multi-output case it acts as an early-exit shorthand — each - declared output retains whatever was last assigned to it via - named-output assignment. + A valueless `return;` carries no payload, so there is nothing to + check against the declared output: it is accepted unconditionally in + every shape — void-output (Return-None-Void), single-output + (Return-None-Single), and multi-output (Return-None-Multi). It is the + Dafny-style early-exit shorthand: each declared output retains + whatever was last assigned to it via named-output assignment. This + also keeps the `EliminateValueInReturns` pass's output well-typed — + that pass rewrites `return e` into `out := e; return;`, and the + trailing bare `return;` must re-resolve cleanly even when the + procedure returns a non-void type. `return e` is checked against the declared output type in the single-output case. Multi-output procedures use named-output @@ -1069,7 +1086,15 @@ def Check.return (exprMd : StmtExprMd) | _ => let (e', _) ← Synth.resolveStmtExpr a.val; pure e') match val, expectedReturn with | none, some [] => pure () - | none, some [singleOutput] => pure () + | none, some [_singleOutput] => + -- A valueless `return;` carries no payload to check against the declared + -- output: it is the Dafny-style early-exit shorthand, where the single + -- output parameter keeps whatever was last assigned to it. Accepted + -- unconditionally (no `TVoid <:~ T` premise). This is also what the + -- `EliminateValueInReturns` pass relies on — it rewrites `return e` into + -- `out := e; return;`, whose trailing bare `return;` must re-resolve + -- cleanly even in an `int`/`bool`/etc.-returning procedure. + pure () | none, some _ => pure () | some _, some [] => let diag := diagnosticFromSource source @@ -1104,7 +1129,7 @@ def Check.return (exprMd : StmtExprMd) The empty block has a fixed type `TVoid`. This is the only block-level rule that synthesizes unconditionally: non-empty blocks are typed structurally by `Resolution.Check.block` (last statement - carries the value, non-last positions via `Check.statement`), + carries the value, non-last positions `⇐ TVoid` or Discard-Call), which always splits off a last statement and so never reaches an empty list. When an empty block appears in check position, `Resolution.Check.resolveStmtExpr`'s wildcard arm synth-then-subsumes @@ -1112,33 +1137,51 @@ def Check.return (exprMd : StmtExprMd) def Synth.emptyBlock (source : Option FileRange) : HighTypeMd := { val := .TVoid, source := source } -/-- (Synth-Discard) Check a statement in *effect position*, written `Γ ⊢ s ⋄`. +/-- (Discard) Check a statement in *effect position*, written `Γ ⊢ s ⋄`. Laurel has no syntactic statement/expression split — everything is a `StmtExpr` — so "what may appear where its value is discarded" is - defined by this rule rather than by the grammar. Every expression in - statement position is synthesized and its type discarded: - - ``` - Γ ⊢ s ⇒ _ - ────────────── - Γ ⊢ s ⋄ - ``` - - Statement-shaped forms (`Var-Declare`, `Assign`, `Assert`, `Assume`, - `While`, `Exit`, `Return`) synthesize `TVoid`; value-producing forms - (calls, `IncrDecr`, literals, etc.) synthesize their natural type, - which is then discarded. This means any expression is accepted in - statement position — the `f(x);` idiom works regardless of `f`'s - return type, and `x++;` is admitted even though `++` synthesizes the - target's type. + defined by this rule rather than by the grammar. The rule cases on the + *shape* of `s`: + + * **Statement-shaped / control-flow forms** — `Var-Declare`, `While`, + the terminators `Exit`/`Return`, `Assert`, `Assume`, `IfThenElse`, + and a nested `Block` — are checked against `TVoid` + (`Γ ⊢ s ⇐ TVoid`). The first six have no synthesis rule, so they + *must* be reached through check mode. `IfThenElse` and `Block` are + check-routed (rather than synthesized) so the void expectation is + pushed into their branches/statements: a terminator branch + (`if c then return …`) and nested blocks then resolve under their + own check rules instead of tripping the synth wildcard. + + * **Value-producing forms** — everything else (calls, `IncrDecr`, + literals, operators, a variable load, `new`, casts, …) — are + **synthesized and their result discarded** (`Γ ⊢ s ⇒ _`). A bare + `f(x);`, `x++;`, a stranded literal `5;`, or a stranded operator + `a < b;` is admitted with no `expected void` diagnostic. This is + what lets the lowering passes' output type-check: e.g. + `EliminateIncrDecr` rewrites a statement-position `x++` into the + `PrimitiveOp` `((x := x + 1) - 1)`, an operator in effect position, + which is simply synthesized and dropped here. This is the single definition of "what counts as a statement". It is - used by `Check.block` for every non-last statement, and for the last - statement when the block itself sits in statement position - (`expected = TVoid`). -/ + used by `Check.block` for every non-last statement that is not itself + a block (non-last blocks are handled directly by `Check.block`, which + propagates the expected type into them), and for the last statement + when the block itself sits in statement position (`expected = TVoid`). -/ def Check.statement (s : StmtExprMd) : ResolveM StmtExprMd := do - let (s', _) ← Synth.resolveStmtExpr s; pure s' + match s.val with + -- Forms that must be *checked* in effect position: the statement-shaped + -- constructs without a synth rule (`Var-Declare`, `While`, `Exit`, + -- `Return`, `Assert`, `Assume`) and the control-flow forms `IfThenElse` / + -- `Block`, whose check rules push the void expectation into their + -- branches/statements so terminators and nested blocks resolve correctly. + | .Var (.Declare ..) | .While .. | .Exit .. | .Return .. + | .Assert .. | .Assume .. | .IfThenElse .. | .Block .. => + Check.resolveStmtExpr s { val := .TVoid, source := s.source } + -- Every other form is value-producing: synthesize and discard the result. + | _ => + let (s', _) ← Synth.resolveStmtExpr s; pure s' termination_by (s, 4) decreasing_by all_goals (apply Prod.Lex.right; decide) @@ -1149,18 +1192,34 @@ def Check.statement (s : StmtExprMd) : ResolveM StmtExprMd := do statement list into `[s₁; … ; sₙ]` (all but the last) and `last`, handling each part as follows: - * **non-last — `Γ ⊢ s ⋄`.** A non-last statement is in effect - position: it is synthesized and its type discarded (see - `Check.statement`). Any expression is accepted — statement-shaped - forms synthesize `TVoid`, value-producing forms (calls, - `IncrDecr`, etc.) synthesize their natural type which is then - discarded. + This is a continuation-passing-style traversal: at each `hd :: tl` + the rule cases on the **head** `hd` and threads the surrounding + expected type `T` down the tail. Most heads are typed in effect + position and `T` is irrelevant to them; the one head that consumes + `T` is a nested block (an implicit control-flow join arm). + + * **non-last, head is a nested `Block` — `Γ ⊢ hd ⇐ T`.** A non-last + block is *not* a pure effect: it may transfer control out of the + enclosing block (an `exit`/`return` in its tail), so its own value + is a join arm of the surrounding block and must satisfy the same + `T`. The expected type is therefore propagated into it (rather than + forcing it to `TVoid`), so its last statement is checked at `T`. + This is what keeps lowered code well-typed: passes routinely emit a + value-carrying block in non-last position. + + * **non-last, any other head — `Γ ⊢ hd ⋄`.** Every other non-last + statement is in effect position, handled by `Check.statement` + (`Γ ⊢ hd ⋄`): statement-shaped and control-flow forms are checked + at `TVoid`, and value-producing forms (calls, `IncrDecr`, literals, + operators, …) are synthesized and their result discarded. A bare + `5;`, `x++;`, or `list.add(x);` is admitted regardless of the value + it produces. * **last — `Γ ⊢ last ⇐ T`.** The surrounding expected type `T` is routed to the last statement, so a check-only trailing form (`IfThenElse`, a nested `Block`, `Hole`, `Return`, …) still receives its expected type. When `T = TVoid` (the block is in - statement position), the last statement is also in effect position + statement position) the last statement is also in effect position and goes through `Check.statement`. A block most often occurs in check position (procedure bodies, @@ -1179,10 +1238,15 @@ def Check.block (exprMd : StmtExprMd) (stmts : List StmtExprMd) (label : Option String) (expected : HighTypeMd) (source : Option FileRange) (h : exprMd.val = .Block stmts label) : ResolveM StmtExprMd := do - -- A non-last statement is in effect position: admitted by `Check.statement` - -- (`Γ ⊢ s ⋄` — synthesized and the type discarded). - let checkNonLast (s : StmtExprMd) (_h_mem : s ∈ stmts) : ResolveM StmtExprMd := - Check.statement s + -- A non-last statement is typed by casing on its head (CPS dispatch). A + -- nested `Block` head is an implicit join arm — it may `exit`/`return` out + -- of the enclosing block — so the surrounding `expected` is propagated into + -- it (`Γ ⊢ hd ⇐ T`). Every other head is in effect position, admitted by + -- `Check.statement` (`Γ ⊢ hd ⋄`). + let checkNonLast (s : StmtExprMd) (_h_mem : s ∈ stmts) : ResolveM StmtExprMd := do + match s.val with + | .Block .. => Check.resolveStmtExpr s expected + | _ => Check.statement s -- The last statement carries the block's value: push `expected` in (so -- check-only forms are reachable). When the block itself sits in statement -- position (`expected = TVoid`), the last statement is also in effect @@ -1352,12 +1416,13 @@ def Synth.ifThenElse (exprMd : StmtExprMd) ``` Synth-mode rule for a non-empty block used where no expected type is available (e.g. `{ x := 1; x } == y`). Mirrors `Check.block`'s - structure — fresh scope, optional label, non-last statements in - effect position (`Check.statement`), dead-code-after-terminator - diagnostic — but *synthesizes* the last statement instead of checking - it against an expected type, and returns that synthesized type as the - block's value type. The empty block is handled by `Synth.emptyBlock` - at the dispatch site; this rule only runs on a non-empty block. -/ + structure — fresh scope, optional label, non-last statements checked + in effect position (`Check.statement`, i.e. at `TVoid` with the + Discard-Call carve-out), dead-code-after-terminator diagnostic — but + *synthesizes* the last statement instead of checking it against an + expected type, and returns that synthesized type as the block's value + type. The empty block is handled by `Synth.emptyBlock` at the + dispatch site; this rule only runs on a non-empty block. -/ def Synth.block (exprMd : StmtExprMd) (stmts : List StmtExprMd) (label : Option String) (source : Option FileRange) @@ -1407,10 +1472,11 @@ def Synth.block (exprMd : StmtExprMd) ``` Γ ⊢ cond ⇐ TBool ────────────────────────────────── - Γ ⊢ Assert cond ⇒ TVoid + Γ ⊢ Assert cond ⇐ A ``` `cond` is checked against `TBool`. `assert` is a statement: it - yields no value, so it synthesizes `TVoid`. -/ + yields no value, so the rule accepts whatever type `A` the context + expects (the rule ignores `A`). -/ def Check.assert (exprMd : StmtExprMd) (condExpr : StmtExprMd) (summary : Option String) (free : Bool) (source : Option FileRange) @@ -1430,10 +1496,11 @@ def Check.assert (exprMd : StmtExprMd) ``` Γ ⊢ cond ⇐ TBool ────────────────────────────────── - Γ ⊢ Assume cond ⇒ TVoid + Γ ⊢ Assume cond ⇐ A ``` `cond` is checked against `TBool`. `assume` is a statement: it - yields no value, so it synthesizes `TVoid`. -/ + yields no value, so the rule accepts whatever type `A` the context + expects (the rule ignores `A`). -/ def Check.assume (exprMd : StmtExprMd) (cond : StmtExprMd) (source : Option FileRange) (h : exprMd.val = .Assume cond) : @@ -2603,37 +2670,58 @@ def resolveParameter (param : Parameter) : ResolveM Parameter := do let name' ← defineNameCheckDup param.name (.parameter ⟨param.name, ty'⟩) return ⟨name', ty'⟩ -/-- Resolve a procedure body by synthesizing its impl block (if any). - Bodies without an impl block (`Abstract`, `External`) resolve - postconditions only. -/ -def resolveBody (body : Body) : ResolveM Body := do +/-- Resolve a procedure body, checking its impl block (if any) against + `expected`. The expected type comes from the procedure's declared + output: a single output `T` for single-output functional procedures, + `Unknown` otherwise. Bodies without an impl block (`Abstract`, `External`) ignore + `expected`. -/ +def resolveBody (body : Body) (expected : HighTypeMd) : ResolveM Body := do match body with | .Transparent b => - let (b', _) ← Synth.resolveStmtExpr b + let b' ← Check.resolveStmtExpr b expected return .Transparent b' | .Opaque posts impl mods => let posts' ← posts.mapM (·.mapM resolveStmtExpr) - let impl' ← impl.mapM Synth.resolveStmtExpr + let impl' ← impl.mapM (Check.resolveStmtExpr · expected) let mods' ← mods.mapM resolveStmtExpr - return .Opaque posts' (impl'.map (fun t => t.1)) mods' + return .Opaque posts' impl' mods' | .Abstract posts => let posts' ← posts.mapM (·.mapM resolveStmtExpr) return .Abstract posts' | .External => return .External +/-- Compute the expected *value type* `A` for a procedure body, i.e. + the `A` in `Γ ⊢ body ⇐ A`. Functional procedures with a single + output `T` expect `A = T`: the body's last statement is the result + and must produce a `T`. Non-functional procedures expect + `A = Unknown`: their body is run as a statement and the last + statement's value (if any) is discarded — outputs are observed via + `return e` (whose payload is matched against the procedure's + declared outputs by `Resolution.Check.return`) or via named-output + assignment. + + This computes only the body's value type. The procedure's declared + output list is bound separately by the procedure rule + (`resolveProcedure` / `resolveInstanceProcedure`) into + `ResolveState.answerType`. -/ +private def procedureBodyType (isFunctional : Bool) (outputs : List Parameter) + (source : Option FileRange) : HighTypeMd := + match isFunctional, outputs with + | true, [singleOutput] => singleOutput.type + | _, _ => { val := .Unknown, source := source } + /-- (Procedure) ``` - T_o-bar = proc.outputs.types - Γ_global, params(proc) ⊢ proc.body ⇒ _ + T_o-bar = proc.outputs.types A = procedureBodyType proc + Γ_global, params(proc) ⊢ proc.body ⇐ A ────────────────────────────────────────────────────────── Γ_global ⊢ Procedure proc ``` - The body is synthesized (not checked against a computed expected - type) under a scope that includes the procedure's input and output - parameters. Outputs are matched only via `return e` (checked against - the declared output by `Check.return`) or via named-output - assignment. The procedure's declared output list `T_o-bar` is stored - on `ResolveState.answerType`, set on entry and restored on exit. -/ + The body is resolved under a scope that includes the procedure's + input and output parameters, and is checked against the value type + `A` computed by `procedureBodyType`. The Return rules consult the + procedure's declared output list `T_o-bar` (stored on + `ResolveState.answerType`, set on entry and restored on exit). -/ def resolveProcedure (proc : Procedure) : ResolveM Procedure := do let procName' ← resolveRef proc.name withScope do @@ -2643,11 +2731,12 @@ def resolveProcedure (proc : Procedure) : ResolveM Procedure := do let dec' ← proc.decreases.mapM resolveStmtExpr let savedAnswer := (← get).answerType modify fun s => { s with answerType := some (outputs'.map (·.type)) } + let bodyExpected := procedureBodyType proc.isFunctional outputs' proc.name.source -- Pre-register the implicit `bodyLabel` block that the LaurelToCore -- translator wraps every body in (`Core.Statement.block bodyLabel …`), -- so that frontends emitting `Exit bodyLabel` for early-return lowering -- (e.g. PythonToLaurel) don't trip Check.exit's label-scope check. - let body' ← withLabel (some bodyLabel) <| resolveBody proc.body + let body' ← withLabel (some bodyLabel) <| resolveBody proc.body bodyExpected modify fun s => { s with answerType := savedAnswer } -- Transparent (static) procedure bodies are supported (#1215): the -- TransparencyPass derives a functional `$asFunction` copy, and the @@ -2686,8 +2775,9 @@ def resolveInstanceProcedure (typeName : Identifier) (proc : Procedure) : Resolv let dec' ← proc.decreases.mapM resolveStmtExpr let savedAnswer := (← get).answerType modify fun s => { s with answerType := some (outputs'.map (·.type)) } + let bodyExpected := procedureBodyType proc.isFunctional outputs' proc.name.source -- See `resolveProcedure` for the rationale on `bodyLabel`. - let body' ← withLabel (some bodyLabel) <| resolveBody proc.body + let body' ← withLabel (some bodyLabel) <| resolveBody proc.body bodyExpected modify fun s => { s with answerType := savedAnswer } if !proc.isFunctional && body'.isTransparent && !proc.name.text.any (· == '$') then let diag := diagnosticFromSource proc.name.source diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressionsError.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressionsError.lean index d1e67ff6f6..41e05dc33c 100644 --- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressionsError.lean +++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressionsError.lean @@ -34,9 +34,8 @@ function functionWithMutatingAssignment(x: int): int function functionWithWhile(x: int): int { - while(false) {}; + while(false) {} //^^^^^^^^^^^^^^^ error: loops are not supported in functions or contracts - 3 }; function functionCallingHasMutationAssignment(x: int): int { diff --git a/StrataTest/Languages/Laurel/ResolutionTypeCheckTests.lean b/StrataTest/Languages/Laurel/ResolutionTypeCheckTests.lean index e3888db451..dfb6e79568 100644 --- a/StrataTest/Languages/Laurel/ResolutionTypeCheckTests.lean +++ b/StrataTest/Languages/Laurel/ResolutionTypeCheckTests.lean @@ -16,18 +16,6 @@ open Strata /-! ## Non-boolean conditions -/ -#eval testLaurelResolution <| -#strata -program Laurel; - -procedure voidReturn(x: int) - returns (r: int) -{ - r := 1; - return -}; -#end - #eval testLaurelResolution <| #strata program Laurel; @@ -94,20 +82,20 @@ function cmp(x: string, y: int): bool { #eval testLaurelResolution <| #strata program Laurel; -procedure invalidAssignment() opaque { +procedure foo() opaque { var x: int := true // ^^^^ error: expected 'int', got 'bool' }; #end -/-! ## Procedure return type checks -/ +/-! ## Function return type checks -/ #eval testLaurelResolution <| #strata program Laurel; -procedure foo(): int { - return true -// ^^^^ error: expected 'int', got 'bool' +function foo(): int { + true +//^^^^ error: expected 'int', got 'bool' }; #end diff --git a/docs/verso/LaurelDoc.lean b/docs/verso/LaurelDoc.lean index eedf40093d..698db8dc04 100644 --- a/docs/verso/LaurelDoc.lean +++ b/docs/verso/LaurelDoc.lean @@ -379,15 +379,15 @@ The Index below links to each construct's subsection. - {ref "rules-subsumption"}[*Subsumption*] — \[⇐\] Sub - {ref "rules-literals"}[*Literals*] — \[⇒\] Lit-Int, \[⇒\] Lit-Bool, \[⇒\] Lit-String, \[⇒\] Lit-Decimal -- {ref "rules-variables"}[*Variables*] — \[⇒\] Var-Local, \[⇒\] Var-Field, \[⇒\] Var-Declare +- {ref "rules-variables"}[*Variables*] — \[⇒\] Var-Local, \[⇒\] Var-Field, \[⇐\] Var-Declare - {ref "rules-control-flow"}[*Control flow*] — \[⇐\] If, \[⇐\] If-NoElse, \[⇒\] If-Synth, \[⇒\] If-Synth-NoElse; - \[⇐\] Block, \[⇒\] Block-Synth, \[⋄\] Synth-Discard, - \[⇒\] Empty-Block; \[⇒\] Exit; - \[⇒\] Return-None-Void, \[⇒\] Return-None-Single, \[⇒\] Return-None-Multi, - \[⇒\] Return-Some, \[⇒\] Return-Void-Error, - \[⇒\] Return-Multi-Error; \[⇒\] While -- {ref "rules-verification-statements"}[*Verification statements*] — \[⇒\] Assert, \[⇒\] Assume + \[⇐\] Block, \[⇒\] Block-Synth, \[⋄\] Stmt, \[⋄\] Discard-Call, + \[⇒\] Empty-Block; \[⇐\] Exit; + \[⇐\] Return-None-Void, \[⇐\] Return-None-Single, \[⇐\] Return-None-Multi, + \[⇐\] Return-Some, \[⇐\] Return-Void-Error, + \[⇐\] Return-Multi-Error; \[⇐\] While +- {ref "rules-verification-statements"}[*Verification statements*] — \[⇐\] Assert, \[⇐\] Assume - {ref "rules-assignment"}[*Assignment*] — \[⇒\] Assign, \[⇐\] Assign - {ref "rules-calls"}[*Calls*] — \[⇒\] Static-Call, \[⇒\] Static-Call-Multi, \[⇒\] Instance-Call, \[⇒\] Instance-Call-Multi @@ -447,7 +447,7 @@ $$`\frac{\Gamma \vdash e \Rightarrow \_ \quad \Gamma(f) = T_f}{\Gamma \vdash \ma {docstring Strata.Laurel.Resolution.Synth.varField} -$$`\frac{x \notin \mathrm{dom}(\Gamma)}{\Gamma \vdash \mathsf{Var}\;(\mathsf{.Declare}\;\langle x, T_x\rangle) \Rightarrow \mathsf{TVoid} \quad \dashv \quad \Gamma, x : T_x} \quad \text{([⇒] Var-Declare)}` +$$`\frac{x \notin \mathrm{dom}(\Gamma)}{\Gamma \vdash \mathsf{Var}\;(\mathsf{.Declare}\;\langle x, T_x\rangle) \Leftarrow A \quad \dashv \quad \Gamma, x : T_x} \quad \text{([⇐] Var-Declare)}` $`x \notin \mathrm{dom}(\Gamma)` is a soft side condition rather than a hard premise: when $`x` is already bound in the current scope the rule still @@ -519,19 +519,25 @@ $`\mathit{last}\;\diamond` rather than $`\mathit{last} \Leftarrow $`\{\ldots;\,\mathit{foo}()\}` type-checks as a statement even when `foo` returns a non-void type. -The effect-position judgment $`\Gamma \vdash s\;\diamond` synthesizes -the statement and discards the result: +The effect-position judgment $`\Gamma \vdash s\;\diamond` admits a +statement in one of two ways: -$$`\frac{\Gamma \vdash s \Rightarrow \_ \;\dashv\; \Gamma'}{\Gamma \vdash s \;\diamond \;\dashv\; \Gamma'} \quad \text{([⋄] Synth-Discard)}` +$$`\frac{\Gamma \vdash s \Leftarrow \mathsf{TVoid} \;\dashv\; \Gamma'}{\Gamma \vdash s \;\diamond \;\dashv\; \Gamma'} \quad \text{([⋄] Stmt)}` -Every expression in statement position is synthesized and its type -discarded. Statement-shaped forms (`Var-Declare`, `Assign`, `Assert`, -`Assume`, `While`, `Exit`, `Return`) synthesize $`\mathsf{TVoid}`; -value-producing forms (calls, `IncrDecr`, literals, etc.) synthesize -their natural type, which is then discarded. This means any expression -is accepted in statement position — the `f(x);` idiom works regardless -of `f`'s return type, and `x++;` is admitted even though `++` -synthesizes the target's type. +$$`\frac{s = \mathsf{StaticCall}\;\ldots \lor s = \mathsf{InstanceCall}\;\ldots \quad \Gamma \vdash s \Rightarrow \_}{\Gamma \vdash s \;\diamond \;\dashv\; \Gamma} \quad \text{([⋄] Discard-Call)}` + +\[⋄\] Stmt admits every statement form (`Var-Declare`, `Assign`, +`Assert`, `Assume`, `While`, `Exit`, `Return`, `IfThenElse`): each +either yields no value — so $`\mathsf{TVoid}` is exactly right — or, for +the terminators `Exit`/`Return`, accepts *any* expected type (their +rules leave the value type free — see \[⇐\] Exit and the Return rules +below — because control leaves before any value is needed). A stranded +value such as `5;` fails it, since $`\mathsf{TInt}` is not consistent +with $`\mathsf{TVoid}`. \[⋄\] Discard-Call is the one carve-out for a +value-producing form: a call is synthesized and its result dropped, so +the standard `f(x);` idiom is allowed even when `f` returns a value. +These two are the only block-level cases that aren't already +consequences of the rules for the individual statement forms. Only `Var (.Declare …)` actually extends the scope $`\Gamma_i`; every other statement leaves it unchanged. The block opens a fresh nested @@ -563,18 +569,21 @@ $`\mathsf{TVoid} <: \mathit{expected}`). {docstring Strata.Laurel.Resolution.Check.block} -The $`\Gamma \vdash s\;\diamond` judgment — the \[⋄\] Synth-Discard -rule above — is the single definition of what counts as a statement in -effect position, factored out into +The $`\Gamma \vdash s\;\diamond` judgment — the \[⋄\] Stmt / \[⋄\] +Discard-Call carve-out above — is the single definition of what counts +as a statement in effect position, factored out into {name Strata.Laurel.Resolution.Check.statement}`Check.statement`: {docstring Strata.Laurel.Resolution.Check.statement} -$$`\frac{l \in \Gamma_{\mathrm{lbl}}}{\Gamma \vdash \mathsf{Exit}\;l \Rightarrow \mathsf{TVoid}} \quad \text{([⇒] Exit)}` +$$`\frac{l \in \Gamma_{\mathrm{lbl}}}{\Gamma \vdash \mathsf{Exit}\;l \Leftarrow A} \quad \text{([⇐] Exit)}` `exit` is an unconditional jump out of the enclosing labeled block. -It synthesizes $`\mathsf{TVoid}` unconditionally. Labels live in their -own namespace $`\Gamma_{\mathrm{lbl}}`, populated by the surrounding +Because control leaves before any value is needed, the rule accepts +*any* expected value type $`A` — it leaves $`A` free, with no +$`\mathsf{TVoid}` side condition — so an `exit` slots into any +position, even one expecting a value. Labels live in their own +namespace $`\Gamma_{\mathrm{lbl}}`, populated by the surrounding `Block` rule when its $`\mathit{label}` is `some l`. An $`\mathsf{Exit}\;l` targeting a label not in $`\Gamma_{\mathrm{lbl}}` is rejected. @@ -585,37 +594,40 @@ In the Return rules below, $`\overline{T_o}` denotes the declared output-parameter type list of the enclosing procedure (an implicit parameter of the rules — the procedure binds it once on entry). -$$`\frac{\overline{T_o} = []}{\Gamma \vdash \mathsf{Return}\;\mathsf{none} \Rightarrow \mathsf{TVoid}} \quad \text{([⇒] Return-None-Void)}` +$$`\frac{\overline{T_o} = []}{\Gamma \vdash \mathsf{Return}\;\mathsf{none} \Leftarrow A} \quad \text{([⇐] Return-None-Void)}` -$$`\frac{\overline{T_o} = [T]}{\Gamma \vdash \mathsf{Return}\;\mathsf{none} \Rightarrow \mathsf{TVoid}} \quad \text{([⇒] Return-None-Single)}` +$$`\frac{\overline{T_o} = [T] \quad \mathsf{TVoid} <:_\sim T}{\Gamma \vdash \mathsf{Return}\;\mathsf{none} \Leftarrow A} \quad \text{([⇐] Return-None-Single)}` -$$`\frac{\overline{T_o} = [T_1; \ldots; T_n] \quad (n \ge 2)}{\Gamma \vdash \mathsf{Return}\;\mathsf{none} \Rightarrow \mathsf{TVoid}} \quad \text{([⇒] Return-None-Multi)}` +$$`\frac{\overline{T_o} = [T_1; \ldots; T_n] \quad (n \ge 2)}{\Gamma \vdash \mathsf{Return}\;\mathsf{none} \Leftarrow A} \quad \text{([⇐] Return-None-Multi)}` -$$`\frac{\overline{T_o} = [T] \quad \Gamma \vdash e \Leftarrow T}{\Gamma \vdash \mathsf{Return}\;(\mathsf{some}\;e) \Rightarrow \mathsf{TVoid}} \quad \text{([⇒] Return-Some)}` +$$`\frac{\overline{T_o} = [T] \quad \Gamma \vdash e \Leftarrow T}{\Gamma \vdash \mathsf{Return}\;(\mathsf{some}\;e) \Leftarrow A} \quad \text{([⇐] Return-Some)}` -$$`\frac{\overline{T_o} = []}{\Gamma \vdash \mathsf{Return}\;(\mathsf{some}\;e) \rightsquigarrow \text{error: “void procedure cannot return a value”}} \quad \text{([⇒] Return-Void-Error)}` +$$`\frac{\overline{T_o} = []}{\Gamma \vdash \mathsf{Return}\;(\mathsf{some}\;e) \rightsquigarrow \text{error: “void procedure cannot return a value”}} \quad \text{([⇐] Return-Void-Error)}` -$$`\frac{\overline{T_o} = [T_1; \ldots; T_n] \quad (n \ge 2)}{\Gamma \vdash \mathsf{Return}\;(\mathsf{some}\;e) \rightsquigarrow \text{error: “multi-output procedure cannot use 'return e'; assign to named outputs instead”}} \quad \text{([⇒] Return-Multi-Error)}` +$$`\frac{\overline{T_o} = [T_1; \ldots; T_n] \quad (n \ge 2)}{\Gamma \vdash \mathsf{Return}\;(\mathsf{some}\;e) \rightsquigarrow \text{error: “multi-output procedure cannot use 'return e'; assign to named outputs instead”}} \quad \text{([⇐] Return-Multi-Error)}` `return` is the only rule whose premises depend on the enclosing -procedure's declared outputs. The rule synthesizes $`\mathsf{TVoid}` -because `return` is a control-flow terminator: it never falls through -and produces no value for the surrounding context. The returned value -(if any) is checked against the procedure's declared output. The error -arms fire when $`\overline{T_o}`'s arity does not match the syntactic -shape of `return e`. +procedure's declared outputs. The conclusion's value type $`A` is left +free — the rule accepts any expected type — because `return` is a +control-flow terminator: it never falls through, so it can stand in +any position, even one expecting a value. The returned value (if any) +is checked against the procedure's declared output, not against $`A`. +The error arms fire when $`\overline{T_o}`'s arity does not match the +syntactic shape of `return e`. Regardless of which arm fires, $`e` is always elaborated — it is checked against the declared output in the single-output case, otherwise synthesized — so any errors inside $`e` are reported in addition to the arity diagnostic. -The three Return-None rules all accept `return;` unconditionally. -Void-output procedures accept it naturally (Return-None-Void); -single-output procedures accept it without a subtype check -(Return-None-Single); multi-output procedures accept it as an -early-exit shorthand that leaves the named outputs at whatever they -were last assigned to (Return-None-Multi). +The three Return-None rules treat the missing payload as having type +$`\mathsf{TVoid}`. Void-output procedures accept it unconditionally +(Return-None-Void); single-output procedures require +$`\mathsf{TVoid} <:_\sim T` (Return-None-Single), accepting void +returns and rejecting `return;` in an `int`/`bool`/etc. procedure; +multi-output procedures accept it as an early-exit shorthand that +leaves the named outputs at whatever they were last assigned to +(Return-None-Multi). When the surrounding context has no enclosing procedure body (e.g. inside a constant initializer), `answerType = none` and all Return @@ -623,12 +635,13 @@ checks are skipped; well-formed input never produces this case. {docstring Strata.Laurel.Resolution.Check.return} -$$`\frac{\Gamma \vdash \mathit{cond} \Leftarrow \mathsf{TBool} \quad \Gamma \vdash \mathit{invs}_i \Leftarrow \mathsf{TBool} \quad \Gamma \vdash \mathit{decreases} \Rightarrow U \quad \mathsf{Numeric}\;U \quad \Gamma \vdash \mathit{body} \Leftarrow \mathsf{Unknown}}{\Gamma \vdash \mathsf{While}\;\mathit{cond}\;\mathit{invs}\;\mathit{decreases}\;\mathit{body} \Rightarrow \mathsf{TVoid}} \quad \text{([⇒] While)}` +$$`\frac{\Gamma \vdash \mathit{cond} \Leftarrow \mathsf{TBool} \quad \Gamma \vdash \mathit{invs}_i \Leftarrow \mathsf{TBool} \quad \Gamma \vdash \mathit{decreases} \Rightarrow U \quad \mathsf{Numeric}\;U \quad \Gamma \vdash \mathit{body} \Leftarrow \mathsf{Unknown}}{\Gamma \vdash \mathsf{While}\;\mathit{cond}\;\mathit{invs}\;\mathit{decreases}\;\mathit{body} \Leftarrow A} \quad \text{([⇐] While)}` The body is checked at $`\mathsf{Unknown}`: control either re-enters the loop or falls through, so the body's value type is never observed by the surrounding context. A loop is a statement and yields no value, -so the rule synthesizes $`\mathsf{TVoid}`. +so the rule accepts any expected type $`A` (it leaves $`A` free), +exactly like the other statement forms. The optional $`\mathit{decreases}` clause is synthesized and required to have a numeric type via the same $`\mathsf{Numeric}` predicate @@ -645,11 +658,11 @@ the clause runs in synth mode rather than check mode. tag := "rules-verification-statements" %%% -$$`\frac{\Gamma \vdash \mathit{cond} \Leftarrow \mathsf{TBool}}{\Gamma \vdash \mathsf{Assert}\;\mathit{cond} \Rightarrow \mathsf{TVoid}} \quad \text{([⇒] Assert)}` +$$`\frac{\Gamma \vdash \mathit{cond} \Leftarrow \mathsf{TBool}}{\Gamma \vdash \mathsf{Assert}\;\mathit{cond} \Leftarrow A} \quad \text{([⇐] Assert)}` {docstring Strata.Laurel.Resolution.Check.assert} -$$`\frac{\Gamma \vdash \mathit{cond} \Leftarrow \mathsf{TBool}}{\Gamma \vdash \mathsf{Assume}\;\mathit{cond} \Rightarrow \mathsf{TVoid}} \quad \text{([⇒] Assume)}` +$$`\frac{\Gamma \vdash \mathit{cond} \Leftarrow \mathsf{TBool}}{\Gamma \vdash \mathsf{Assume}\;\mathit{cond} \Leftarrow A} \quad \text{([⇐] Assume)}` {docstring Strata.Laurel.Resolution.Check.assume} @@ -915,19 +928,21 @@ $$`\frac{}{\Gamma \vdash \mathsf{Hole}\;d\;(\mathsf{some}\;T_h) \Rightarrow T_h} tag := "rules-procedure" %%% -A procedure body is synthesized (not checked against a computed -expected type) and is resolved under a scope that includes the -procedure's input and output parameters. The Return rules above refer -to the same output list $`\overline{T_o}` that the procedure binds -here. +A procedure body is checked against an expected type $`A` and is +resolved under a scope that includes the procedure's input and output +parameters. The Return rules above refer to the same output list +$`\overline{T_o}` that the procedure binds here. -$$`\frac{\overline{T_o} = \mathit{proc}.\mathit{outputs}.\mathit{types} \quad \Gamma_\mathit{global},\,\mathit{params}(\mathit{proc}) \vdash \mathit{proc}.\mathit{body} \Rightarrow \_}{\Gamma_\mathit{global} \vdash \mathsf{Procedure}\;\mathit{proc}} \quad \text{(Procedure)}` +$$`\frac{\overline{T_o} = \mathit{proc}.\mathit{outputs}.\mathit{types} \quad A = \mathsf{procedureBodyType}(\mathit{proc}) \quad \Gamma_\mathit{global},\,\mathit{params}(\mathit{proc}) \vdash \mathit{proc}.\mathit{body} \Leftarrow A}{\Gamma_\mathit{global} \vdash \mathsf{Procedure}\;\mathit{proc}} \quad \text{(Procedure)}` -The body is synthesized and its type is discarded — there is no -constraint from the output list pushed into the body. Outputs are -matched only via `return e` (checked against $`\overline{T_o}` by -{name Strata.Laurel.Resolution.Check.return}`Check.return`) or via -named-output assignment. +The body's value type $`A` is computed by `procedureBodyType`: a +single-output functional procedure expects $`A = T` (its body's last +statement is the result), while every other procedure expects +$`A = \mathsf{Unknown}` (its body is run as a statement and the last +statement's value is discarded; outputs are observed via `return e`, +matched against $`\overline{T_o}` by +{name Strata.Laurel.Resolution.Check.return}`Check.return`, or via +named-output assignment). {docstring Strata.Laurel.resolveProcedure}