Γ ⊢ LiteralInt n ⇒ TInt
2.3. Typing rules
Each construct is given as a derivation. Γ is the current lexical scope (see
ResolveState's scope); it threads identically through
every premise and conclusion unless a rule explicitly extends it (written Γ, x : T).
Each rule is tagged with [⇒] (synthesis) or [⇐] (checking) to make the
direction explicit. The Procedure rule is the one
exception: it is a top-level well-formedness judgment and carries no direction
tag.
The following notation recurs throughout the rules:
-
A <: B— subtyping (isSubtype); see Gradual typing above. In a checking premise or side condition (e.g. [⇐] Sub, [⇐] If-NoElse, [⇐] Assign, the check-mode operator rules, and [⇐] Hole-Some) the boundary check is the gradual consistent-subtype relation<:_\simbelow — the implementation routes every such check throughisConsistentSubtype, never bare<:— so\mathsf{Unknown}is admitted on either side. -
A \sim B— the consistency relationisConsistent: symmetric, with\mathsf{Unknown}acting as a wildcard. -
A <:_\sim B— the consistent-subtype relationisConsistentSubtype, the gradual combination of the two above. -
\mathsf{Numeric}\;T— a predicate holding whenTis consistent with one of\mathsf{TInt},\mathsf{TReal},\mathsf{TFloat64}, or\mathsf{TBv}_w(a bitvector of any widthw), with\mathsf{Unknown}admitted as the gradual escape hatch. -
\dashv \Gamma'— a rule's output scope: the judgment threads\Gammain and produces\Gamma'out. Only the declaring rules extend the scope — [⇒] Var-Declare / Var-Declare-Infer, the Decl-Synth pair, and [⇒]/[⇐] Assign when a target is aDeclare; the block rules thread it statement-to-statement (the\Gamma_{i-1} \to \Gamma_ichain in [⇐] Block / [⇒] Block-Synth). -
\rightsquigarrow \text{error: …}— the rule emits an error and aborts; no type is produced. -
[\text{emits …}]— the rule produces its type but also emits a diagnostic. -
\mapsto— elaboration: the construct is rewritten to the form on the right.
The Index below links to each construct's subsection.
2.3.1. Index
-
Subsumption — [⇐] Sub
-
Literals — [⇒] Lit-Int, [⇒] Lit-Bool, [⇒] Lit-String, [⇒] Lit-Decimal
-
Variables — [⇒] Var-Local, [⇒] Var-Field, [⇒] Var-Declare, [⇒] Var-Declare-Infer
-
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
-
Verification statements — [⇒] Assert, [⇒] Assume
-
Assignment — [⇒] Assign, [⇐] Assign, [⇒] Decl-Synth, [⇐] Decl-Synth
-
Calls — [⇒] Static-Call, [⇒] Static-Call-Multi, [⇒] Instance-Call, [⇒] Instance-Call-Multi
-
Operators — no operator-specific rules: operators are calls, typed by [⇒] Static-Call. Equality is the one special case: [⇒] Op-Eq
-
Object forms — [⇒] New-Ok, [⇒] New-Fallback; [⇒] AsType; [⇒] IsType; [⇒] RefEq; [⇒] PureFieldUpdate
-
Verification expressions — [⇒] Quantifier, [⇒] Assigned, [⇐] Old, [⇒] Old-Synth, [⇒] Fresh, [⇐] ProveBy, [⇒] ProveBy-Synth
-
Self reference — [⇒] This-Inside, [⇒] This-Outside
-
Untyped forms — [⇒] Abstract / All
-
ContractOf — [⇒] ContractOf-Bool, [⇒] ContractOf-Set, [⇒] ContractOf-Error
-
Holes — [⇐] Hole-Some, [⇐] Hole-None, [⇒] Hole-Synth-None, [⇒] Hole-Synth-Some
-
Procedure — Procedure
2.3.2. Subsumption
\frac{\Gamma \vdash e \Rightarrow A \quad A <: B}{\Gamma \vdash e \Leftarrow B} \quad \text{([⇐] Sub)}
Fallback in Check.resolveStmtExpr whenever no
bespoke check rule applies.
2.3.3. Literals
\frac{}{\Gamma \vdash \mathsf{LiteralInt}\;n \Rightarrow \mathsf{TInt}} \quad \text{([⇒] Lit-Int)}
def
Strata.Laurel.Resolution.Synth.litInt (v : Int) (source : Strata.FileRange) : Strata.Laurel.StmtExpr × Strata.Laurel.HighTypeMdStrata.Laurel.Resolution.Synth.litInt (v : Int) (source : Strata.FileRange) : Strata.Laurel.StmtExpr × Strata.Laurel.HighTypeMd
\frac{}{\Gamma \vdash \mathsf{LiteralBool}\;b \Rightarrow \mathsf{TBool}} \quad \text{([⇒] Lit-Bool)}
def
Strata.Laurel.Resolution.Synth.litBool (v : Bool) (source : Strata.FileRange) : Strata.Laurel.StmtExpr × Strata.Laurel.HighTypeMdStrata.Laurel.Resolution.Synth.litBool (v : Bool) (source : Strata.FileRange) : Strata.Laurel.StmtExpr × Strata.Laurel.HighTypeMd
Γ ⊢ LiteralBool b ⇒ TBool
\frac{}{\Gamma \vdash \mathsf{LiteralString}\;s \Rightarrow \mathsf{TString}} \quad \text{([⇒] Lit-String)}
def
Strata.Laurel.Resolution.Synth.litString (v : String) (source : Strata.FileRange) : Strata.Laurel.StmtExpr × Strata.Laurel.HighTypeMdStrata.Laurel.Resolution.Synth.litString (v : String) (source : Strata.FileRange) : Strata.Laurel.StmtExpr × Strata.Laurel.HighTypeMd
Γ ⊢ LiteralString s ⇒ TString
\frac{}{\Gamma \vdash \mathsf{LiteralDecimal}\;d \Rightarrow \mathsf{TReal}} \quad \text{([⇒] Lit-Decimal)}
def
Strata.Laurel.Resolution.Synth.litDecimal (v : StrataDDM.Decimal) (source : Strata.FileRange) : Strata.Laurel.StmtExpr × Strata.Laurel.HighTypeMdStrata.Laurel.Resolution.Synth.litDecimal (v : StrataDDM.Decimal) (source : Strata.FileRange) : Strata.Laurel.StmtExpr × Strata.Laurel.HighTypeMd
Γ ⊢ LiteralDecimal d ⇒ TReal
2.3.4. Variables
\frac{\Gamma(x) = T}{\Gamma \vdash \mathsf{Var}\;(\mathsf{.Local}\;x) \Rightarrow T} \quad \text{([⇒] Var-Local)}
def
Strata.Laurel.Resolution.Synth.varLocal (ref : Strata.Laurel.Identifier) (source : Strata.FileRange) : Strata.Laurel.ResolveM (Strata.Laurel.StmtExpr × Strata.Laurel.HighTypeMd)Strata.Laurel.Resolution.Synth.varLocal (ref : Strata.Laurel.Identifier) (source : Strata.FileRange) : Strata.Laurel.ResolveM (Strata.Laurel.StmtExpr × Strata.Laurel.HighTypeMd)
(Var-Local)
Γ(x) = T ────────────────────── Γ ⊢ Var (.Local x) ⇒ T
Resolves ref against the lexical scope and reads its declared type.
\frac{\Gamma \vdash e \Rightarrow \_ \quad \Gamma(f) = T_f}{\Gamma \vdash \mathsf{Var}\;(\mathsf{.Field}\;e\;f) \Rightarrow T_f} \quad \text{([⇒] Var-Field)}
def
Strata.Laurel.Resolution.Synth.varField (exprMd target : Strata.Laurel.StmtExprMd) (fieldName : Strata.Laurel.Identifier) (source : Strata.FileRange) (h : exprMd.val = Strata.Laurel.StmtExpr.Var (Strata.Laurel.Variable.Field target fieldName)) : Strata.Laurel.ResolveM (Strata.Laurel.StmtExpr × Strata.Laurel.HighTypeMd)Strata.Laurel.Resolution.Synth.varField (exprMd target : Strata.Laurel.StmtExprMd) (fieldName : Strata.Laurel.Identifier) (source : Strata.FileRange) (h : exprMd.val = Strata.Laurel.StmtExpr.Var (Strata.Laurel.Variable.Field target fieldName)) : Strata.Laurel.ResolveM (Strata.Laurel.StmtExpr × Strata.Laurel.HighTypeMd)
(Var-Field)
Γ ⊢ e ⇒ _ Γ(f) = T_f ─────────────────────────── Γ ⊢ Var (.Field e f) ⇒ T_f
f is looked up against the type of e (or the enclosing instance type
for self.f); the typing rule itself is path-agnostic.
\frac{x \notin \mathrm{dom}(\Gamma)}{\Gamma \vdash \mathsf{Var}\;(\mathsf{.Declare}\;\langle x, \mathsf{some}\;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, \mathsf{none}\rangle) \Rightarrow \mathsf{TVoid} \quad [\text{emits “cannot infer a type …”}] \quad \dashv \quad \Gamma, x : \mathsf{Unknown}} \quad \text{([⇒] Var-Declare-Infer)}
The type annotation is optional in the AST (type : Option). A bare
var x (annotation none) has neither an annotation nor an
initializer to read a type from, so [⇒] Var-Declare-Infer diagnoses it
and binds x : \mathsf{Unknown} so later uses of x don't cascade
further type errors. An unannotated declaration with an initializer
(var x := e) never reaches these rules: it parses as an Assign with a
sole Declare target and is handled by the [⇒]/[⇐] Decl-Synth rules
(see Assignment), which recover the
binding's type from the initializer. Either way the node is rewritten to a
fully-annotated Declare x (some T), so no none annotation survives
resolution.
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
fires, [\text{emits “Duplicate definition …”}], and extends the scope —
but with an unresolved placeholder instead of x : T_x, so later uses of
x don't cascade further type errors.
def
Strata.Laurel.Resolution.Check.varDeclare (param : Strata.Laurel.Parameter?) (source : Strata.FileRange) : Strata.Laurel.ResolveM Strata.Laurel.StmtExprMdStrata.Laurel.Resolution.Check.varDeclare (param : Strata.Laurel.Parameter?) (source : Strata.FileRange) : Strata.Laurel.ResolveM Strata.Laurel.StmtExprMd
(Var-Declare)
x ∉ dom(Γ) (annotated, type = some T_x) ──────────────────────────────────────────────────── Γ ⊢ Var (.Declare x (some T_x)) ⇒ TVoid ⊣ Γ, x : T_x x ∉ dom(Γ) (Var-Declare-Infer, type = none) ──────────────────────────────────────────────────── Γ ⊢ Var (.Declare x none) ⇒ TVoid ⊣ Γ, x : Unknown
⊣ Γ, 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.
When the annotation is absent (type = none, i.e. surface var x),
there is neither an annotation nor an initializer to read a type
from — var x := e is handled in Synth.declInfer/Check.declInfer by
synthesizing e — so this rule emits a "cannot infer a type"
diagnostic (binding x : Unknown, so that later uses of x do not
cascade further type errors). Either way the node is rewritten to a
fully-typed Declare x (some T), so no none annotation survives
resolution.
x ∉ dom(Γ) is a soft side condition, not a hard premise: when x
is already bound in the current scope, defineNameCheckDup emits a
"Duplicate definition '<x>' is already defined in this scope"
diagnostic and still extends the scope — but with an unresolved
placeholder rather than x : T_x, so later uses of x do not
cascade further type errors.
2.3.5. Control flow
\frac{\Gamma \vdash \mathit{cond} \Leftarrow \mathsf{TBool} \quad \Gamma \vdash \mathit{thenBr} \Leftarrow T \quad \Gamma \vdash \mathit{elseBr} \Leftarrow T}{\Gamma \vdash \mathsf{IfThenElse}\;\mathit{cond}\;\mathit{thenBr}\;(\mathsf{some}\;\mathit{elseBr}) \Leftarrow T} \quad \text{([⇐] If)}
\frac{\Gamma \vdash \mathit{cond} \Leftarrow \mathsf{TBool} \quad \Gamma \vdash \mathit{thenBr} \Leftarrow T \quad \mathsf{TVoid} <: T}{\Gamma \vdash \mathsf{IfThenElse}\;\mathit{cond}\;\mathit{thenBr}\;\mathsf{none} \Leftarrow T} \quad \text{([⇐] If-NoElse)}
def
Strata.Laurel.Resolution.Check.ifThenElse (exprMd cond thenBr : Strata.Laurel.StmtExprMd) (elseBr : Option Strata.Laurel.StmtExprMd) (expected : Strata.Laurel.HighTypeMd) (source : Strata.FileRange) (h : exprMd.val = Strata.Laurel.StmtExpr.IfThenElse cond thenBr elseBr) : Strata.Laurel.ResolveM Strata.Laurel.StmtExprMdStrata.Laurel.Resolution.Check.ifThenElse (exprMd cond thenBr : Strata.Laurel.StmtExprMd) (elseBr : Option Strata.Laurel.StmtExprMd) (expected : Strata.Laurel.HighTypeMd) (source : Strata.FileRange) (h : exprMd.val = Strata.Laurel.StmtExpr.IfThenElse cond thenBr elseBr) : Strata.Laurel.ResolveM Strata.Laurel.StmtExprMd
(If / If-NoElse)
Γ ⊢ cond ⇐ TBool (If) Γ ⊢ thenBr ⇐ T Γ ⊢ elseBr ⇐ T ────────────────────────────────────────────────────────────────── Γ ⊢ IfThenElse cond thenBr (some elseBr) ⇐ T Γ ⊢ cond ⇐ TBool (If-NoElse) Γ ⊢ thenBr ⇐ T TVoid <: T ────────────────────────────────────────────────────────────────── Γ ⊢ IfThenElse cond thenBr none ⇐ T
Pushes the surrounding T into both branches (rather than going
through If-Synth + Sub at the boundary): errors fire at the
offending branch instead of at the if, and the expectation
propagates through nested Block / IfThenElse / Hole
constructs that have their own check rules.
Without an else, the implicit branch is an empty block of type
TVoid, so the rule degenerates to require TVoid <: T — the
standard [⇐] Sub boundary check that Resolution.Synth.emptyBlock
composes with for an empty block.
When an if appears in operand position — where no expected type is
available to push down (e.g. as an operand of == / < / +\!+,
whose operands are synthesized) — the synth counterpart fires instead.
With an else, both branches are synthesized and their types must be
mutually consistent (\sim, the symmetric gradual relation);
inconsistent branches [\text{emits “'if' branches have incompatible
types X and Y”}] and synthesize \mathsf{Unknown}. The result is the
join T_t \sqcup T_e of the two branch types, so when one branch is a
hole (\mathsf{Unknown}) the join promotes to the other branch's
concrete type, and the synthesized type is independent of branch order.
Without an else, the missing branch cannot produce a value, so the if
synthesizes \mathsf{TVoid}.
`if` in operand position
-
(if c then 1 else 2) == y— both branches\mathsf{TInt}, so theifsynthesizes\mathsf{TInt} -
if c then 1 else <?>— the hole branch promotes; synthesizes\mathsf{TInt} -
if c then 1 else "x"— incompatible branches: 'if' branches have incompatible types 'int' and 'string', synthesizes\mathsf{Unknown} -
if c then 1(noelse) — synthesizes\mathsf{TVoid}
\frac{\Gamma \vdash \mathit{cond} \Leftarrow \mathsf{TBool} \quad \Gamma \vdash \mathit{thenBr} \Rightarrow T_t \quad \Gamma \vdash \mathit{elseBr} \Rightarrow T_e \quad T_t \sim T_e}{\Gamma \vdash \mathsf{IfThenElse}\;\mathit{cond}\;\mathit{thenBr}\;(\mathsf{some}\;\mathit{elseBr}) \Rightarrow T_t \sqcup T_e} \quad \text{([⇒] If-Synth)}
\frac{\Gamma \vdash \mathit{cond} \Leftarrow \mathsf{TBool} \quad \Gamma \vdash \mathit{thenBr} \Rightarrow \_}{\Gamma \vdash \mathsf{IfThenElse}\;\mathit{cond}\;\mathit{thenBr}\;\mathsf{none} \Rightarrow \mathsf{TVoid}} \quad \text{([⇒] If-Synth-NoElse)}
def
Strata.Laurel.Resolution.Synth.ifThenElse (exprMd cond thenBr : Strata.Laurel.StmtExprMd) (elseBr : Option Strata.Laurel.StmtExprMd) (source : Strata.FileRange) (h : exprMd.val = Strata.Laurel.StmtExpr.IfThenElse cond thenBr elseBr) : Strata.Laurel.ResolveM (Strata.Laurel.StmtExpr × Strata.Laurel.HighTypeMd)Strata.Laurel.Resolution.Synth.ifThenElse (exprMd cond thenBr : Strata.Laurel.StmtExprMd) (elseBr : Option Strata.Laurel.StmtExprMd) (source : Strata.FileRange) (h : exprMd.val = Strata.Laurel.StmtExpr.IfThenElse cond thenBr elseBr) : Strata.Laurel.ResolveM (Strata.Laurel.StmtExpr × Strata.Laurel.HighTypeMd)
(If-Synth)
Γ ⊢ cond ⇐ TBool Γ ⊢ thenBr ⇒ T_t Γ ⊢ elseBr ⇒ T_e T_t ~ T_e T = T_t ⨆ T_e (consistency join) (If-Synth) ────────────────────────────────────────────────────────────────────────── Γ ⊢ IfThenElse cond thenBr (some elseBr) ⇒ T Γ ⊢ cond ⇐ TBool Γ ⊢ thenBr ⇒ _ (If-Synth-NoElse) ────────────────────────────────────────────────────────────────────────── Γ ⊢ IfThenElse cond thenBr none ⇒ TVoid
Synth-mode rule for an if used where no expected type is available
(e.g. as an operand of ==/</++, whose operands are synthesized).
cond is checked against TBool; both branches are synthesized.
With an else, the two branch types must be mutually consistent
(isConsistent, the symmetric gradual relation — Unknown flows
freely either way); when consistent, the result is their symmetric
join (Unknown ⊔ T = T), so a hole branch promotes to the other
branch's concrete type and the synthesized type is independent of
branch order. (isConsistent stays the accept/reject gate: it admits
a gradual corner where join is none, for which the result
falls back to the then-branch type, leaving that boundary unchanged.)
Inconsistent branches (e.g. if c then 1 else "x") emit a diagnostic
and synthesize Unknown to suppress cascading errors. Without an
else, the if cannot produce a value on the missing branch, so it
synthesizes TVoid.
This is the synth counterpart to Check.ifThenElse: when an expected
type is available the dispatcher prefers the check rule (pushing the
type into both branches); this rule fires only at the synth wildcard.
A non-empty block is typed by splitting its statement list into the
last statement and the statements before it. The last statement
carries the block's value and inherits the surrounding expected type;
each earlier statement runs only for its effect — written
\Gamma \vdash s\;\diamond (effect position: the statement's value
is discarded). The check and synth rules share this shape, differing
only in how the last statement is treated:
\frac{\Gamma_0 = \Gamma \quad \Gamma_{i-1} \vdash s_i \;\diamond \;\dashv\; \Gamma_i \;\;(1 \le i \le n) \quad \Gamma_n \vdash \mathit{last} \Leftarrow T}{\Gamma \vdash \mathsf{Block}\;[s_1; \ldots; s_n; \mathit{last}]\;\mathit{label} \Leftarrow T} \quad \text{([⇐] Block)}
\frac{\Gamma_0 = \Gamma \quad \Gamma_{i-1} \vdash s_i \;\diamond \;\dashv\; \Gamma_i \;\;(1 \le i \le n) \quad \Gamma_n \vdash \mathit{last} \Rightarrow T}{\Gamma \vdash \mathsf{Block}\;[s_1; \ldots; s_n; \mathit{last}]\;\mathit{label} \Rightarrow T} \quad \text{([⇒] Block-Synth)}
[⇐] Block fires whenever an expected type T is supplied (procedure
bodies, branches, loop bodies, assignment RHS, call arguments);
[⇒] Block-Synth fires in operand position, where no expected type is
available (e.g. \{\,x := 1;\; x\,\} == y), synthesizing the last
statement's type as the block's value type.
When the block itself sits in statement position (T = \mathsf{TVoid})
the last statement is in effect position too: its premise becomes
\mathit{last}\;\diamond rather than \mathit{last} \Leftarrow
\mathsf{TVoid}, so a trailing call discards its result and
\{\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:
\frac{\Gamma \vdash s \Rightarrow \_ \;\dashv\; \Gamma'}{\Gamma \vdash s \;\diamond \;\dashv\; \Gamma'} \quad \text{([⋄] Synth-Discard)}
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.
Only declarations actually extend the scope \Gamma_i — Var (.Declare …)
and Assign statements with Declare targets (var x := e,
assign var x, y := call()); every other statement leaves it unchanged. The block opens a fresh nested
scope, so declarations made inside don't leak out — once the block ends,
the surrounding \Gamma is restored. It also emits a
"dead code after '<terminator>'" diagnostic when an Exit or
Return is followed by further statements in the same block.
Pushing T into the last statement (rather than synthesizing the whole
block and applying [⇐] Sub at the boundary) means a type mismatch is
reported at the offending subexpression's source location, and the
expectation keeps propagating through nested Block / IfThenElse /
Hole / Quantifier constructs that have their own check rules.
\frac{}{\Gamma \vdash \mathsf{Block}\;[]\;\mathit{label} \Rightarrow \mathsf{TVoid}} \quad \text{([⇒] Empty-Block)}
The empty block has a fixed type and is the only block-level rule that
synthesizes unconditionally. [⇐] Block and [⇒] Block-Synth always
split off a last statement, so they never reach an empty list; the
empty case is hit only when the block is literally empty at the dispatch
site. When an empty block appears in check position with
expected ≠ TVoid, the standard [⇐] Sub rule fires at the boundary
(Check.resolveStmtExpr's subsumption-fallback wildcard arm, requiring
\mathsf{TVoid} <: \mathit{expected}).
def
Strata.Laurel.Resolution.Synth.emptyBlock (source : Strata.FileRange) : Strata.Laurel.HighTypeMdStrata.Laurel.Resolution.Synth.emptyBlock (source : Strata.FileRange) : Strata.Laurel.HighTypeMd
(Empty-Block)
───────────────────────────────── Γ ⊢ Block [] label ⇒ TVoid
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),
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
via the standard [⇐] Sub fallback.
def
Strata.Laurel.Resolution.Synth.block (exprMd : Strata.Laurel.StmtExprMd) (stmts : List Strata.Laurel.StmtExprMd) (label : Option String) (source : Strata.FileRange) (h : exprMd.val = Strata.Laurel.StmtExpr.Block stmts label) : Strata.Laurel.ResolveM (Strata.Laurel.StmtExpr × Strata.Laurel.HighTypeMd)Strata.Laurel.Resolution.Synth.block (exprMd : Strata.Laurel.StmtExprMd) (stmts : List Strata.Laurel.StmtExprMd) (label : Option String) (source : Strata.FileRange) (h : exprMd.val = Strata.Laurel.StmtExpr.Block stmts label) : Strata.Laurel.ResolveM (Strata.Laurel.StmtExpr × Strata.Laurel.HighTypeMd)
(Block-Synth)
Γ ⊢ sᵢ ⋄ (1 ≤ i ≤ n) Γ ⊢ last ⇒ T (Block-Synth) ────────────────────────────────────────────────────────────── Γ ⊢ Block [s₁; … ; sₙ; last] label ⇒ T
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.
def
Strata.Laurel.Resolution.Check.block (exprMd : Strata.Laurel.StmtExprMd) (stmts : List Strata.Laurel.StmtExprMd) (label : Option String) (expected : Strata.Laurel.HighTypeMd) (source : Strata.FileRange) (h : exprMd.val = Strata.Laurel.StmtExpr.Block stmts label) : Strata.Laurel.ResolveM Strata.Laurel.StmtExprMdStrata.Laurel.Resolution.Check.block (exprMd : Strata.Laurel.StmtExprMd) (stmts : List Strata.Laurel.StmtExprMd) (label : Option String) (expected : Strata.Laurel.HighTypeMd) (source : Strata.FileRange) (h : exprMd.val = Strata.Laurel.StmtExpr.Block stmts label) : Strata.Laurel.ResolveM Strata.Laurel.StmtExprMd
(Block) Check-mode typing rule for a non-empty block.
A block's value is the value of its last statement; every
earlier statement is run only for its effect. The rule splits the
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 (seeCheck.statement). Any expression is accepted — statement-shaped forms synthesizeTVoid, value-producing forms (calls,IncrDecr, etc.) synthesize their natural type which is then discarded. -
last —
Γ ⊢ last ⇐ T. The surrounding expected typeTis routed to the last statement, so a check-only trailing form (IfThenElse, a nestedBlock,Hole,Return, …) still receives its expected type. WhenT = TVoid(the block is in statement position), the last statement is also in effect position and goes throughCheck.statement.
A block most often occurs in check position (procedure bodies,
branches, loop bodies, assignment RHS, and call arguments all supply
an expected type). When one appears in synth-only operand position
with no contextual type, Resolution.Synth.block handles it with the
same structure, synthesizing the last statement instead.
The block opens a fresh nested scope (declarations made inside
don't leak), and emits a "dead code after exit/return"
diagnostic when a terminator is followed by further statements.
When label is some l, l is registered in
ResolveState.labelScope (via withLabel) for the block's extent
so nested exit l checks can see it.
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
Check.statement:
def
Strata.Laurel.Resolution.Check.statement (s : Strata.Laurel.StmtExprMd) : Strata.Laurel.ResolveM Strata.Laurel.StmtExprMdStrata.Laurel.Resolution.Check.statement (s : Strata.Laurel.StmtExprMd) : Strata.Laurel.ResolveM Strata.Laurel.StmtExprMd
(Synth-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.
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).
\frac{l \in \Gamma_{\mathrm{lbl}}}{\Gamma \vdash \mathsf{Exit}\;l \Rightarrow \mathsf{TVoid}} \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
Block rule when its \mathit{label} is some l. An
\mathsf{Exit}\;l targeting a label not in \Gamma_{\mathrm{lbl}}
is rejected.
def
Strata.Laurel.Resolution.Check.exit (target : String) (source : Strata.FileRange) : Strata.Laurel.ResolveM Strata.Laurel.StmtExprMdStrata.Laurel.Resolution.Check.exit (target : String) (source : Strata.FileRange) : Strata.Laurel.ResolveM Strata.Laurel.StmtExprMd
(Exit)
l ∈ Γ_lbl ─────────────────── Γ ⊢ Exit l ⇒ TVoid
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.
The premise l ∈ Γ_lbl requires the target label to name an
enclosing labeled block; labels live in their own namespace
(ResolveState.labelScope, populated by Check.block via
withLabel). An unknown label is reported here as
"label '<l>' is not in scope".
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} = [T]}{\Gamma \vdash \mathsf{Return}\;\mathsf{none} \Rightarrow \mathsf{TVoid}} \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] \quad \Gamma \vdash e \Leftarrow T}{\Gamma \vdash \mathsf{Return}\;(\mathsf{some}\;e) \Rightarrow \mathsf{TVoid}} \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} = [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.
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).
When the surrounding context has no enclosing procedure body (e.g.
inside a constant initializer), answerType = none and all Return
checks are skipped; well-formed input never produces this case.
def
Strata.Laurel.Resolution.Check.return (exprMd : Strata.Laurel.StmtExprMd) (val : Option Strata.Laurel.StmtExprMd) (source : Strata.FileRange) (h : exprMd.val = Strata.Laurel.StmtExpr.Return val) : Strata.Laurel.ResolveM Strata.Laurel.StmtExprMdStrata.Laurel.Resolution.Check.return (exprMd : Strata.Laurel.StmtExprMd) (val : Option Strata.Laurel.StmtExprMd) (source : Strata.FileRange) (h : exprMd.val = Strata.Laurel.StmtExpr.Return val) : Strata.Laurel.ResolveM Strata.Laurel.StmtExprMd
(Return)
Below, T_o-bar denotes the enclosing procedure's declared
output-type list (bound on entry to a procedure body, stored on
ResolveState.answerType).
T_o-bar = [] (Return-None-Void) ───────────────────────── Γ ⊢ Return none ⇒ TVoid T_o-bar = [T] (Return-None-Single) ────────────────────────────────── Γ ⊢ Return none ⇒ TVoid T_o-bar = [T_1;…;T_n] n ≥ 2 (Return-None-Multi) ────────────────────────────────── Γ ⊢ Return none ⇒ TVoid T_o-bar = [T] Γ ⊢ e ⇐ T (Return-Some) ────────────────────────────────── Γ ⊢ Return (some e) ⇒ TVoid T_o-bar = [] (Return-Void-Error) ─────────────────────────────────────────────────────────── Γ ⊢ Return (some e) ↝ "void procedure cannot return a value" T_o-bar = [T_1;…;T_n] n ≥ 2 (Return-Multi-Error) ─────────────────────────────────────────────────────────── Γ ⊢ 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.
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.
return e is checked against the declared output type in the
single-output case. Multi-output procedures use named-output
assignment (r := … on the declared output parameters); return e
syntactically takes a single Option StmtExpr and cannot carry
multiple values, so it is flagged with a diagnostic pointing users
at the named-output convention.
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.
\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)}
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}.
The optional \mathit{decreases} clause is synthesized and required
to have a numeric type via the same \mathsf{Numeric} predicate
used by the arithmetic primitive operations. \mathsf{Numeric} is
a predicate (it admits \mathsf{TInt}, \mathsf{TReal},
\mathsf{TFloat64}, \mathsf{TBv}_w (a bitvector of any width), and
\mathsf{Unknown} as the gradual escape hatch), not a single type, so
the clause runs in synth mode rather than check mode.
def
Strata.Laurel.Resolution.Check.while (exprMd cond : Strata.Laurel.StmtExprMd) (invs : List Strata.Laurel.StmtExprMd) (dec : Option Strata.Laurel.StmtExprMd) (body : Strata.Laurel.StmtExprMd) (postTest : Bool) (source : Strata.FileRange) (h : exprMd.val = Strata.Laurel.StmtExpr.While cond invs dec body postTest) : Strata.Laurel.ResolveM Strata.Laurel.StmtExprMdStrata.Laurel.Resolution.Check.while (exprMd cond : Strata.Laurel.StmtExprMd) (invs : List Strata.Laurel.StmtExprMd) (dec : Option Strata.Laurel.StmtExprMd) (body : Strata.Laurel.StmtExprMd) (postTest : Bool) (source : Strata.FileRange) (h : exprMd.val = Strata.Laurel.StmtExpr.While cond invs dec body postTest) : Strata.Laurel.ResolveM Strata.Laurel.StmtExprMd
(While)
Γ ⊢ cond ⇐ TBool Γ ⊢ invs_i ⇐ TBool Γ ⊢ decreases ⇒ U Numeric U Γ ⊢ body ⇐ Unknown ───────────────────────────────────────────────── Γ ⊢ While cond invs decreases body ⇒ TVoid
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.
The optional decreases clause is synthesized and required to
have a numeric type, via the same Numeric U predicate
used by the arithmetic primitive ops. Numeric is a predicate,
not a single type, so the clause runs in synth mode rather than
check mode.
2.3.6. Verification statements
\frac{\Gamma \vdash \mathit{cond} \Leftarrow \mathsf{TBool}}{\Gamma \vdash \mathsf{Assert}\;\mathit{cond} \Rightarrow \mathsf{TVoid}} \quad \text{([⇒] Assert)}
def
Strata.Laurel.Resolution.Check.assert (exprMd condExpr : Strata.Laurel.StmtExprMd) (summary : Option String) (source : Strata.FileRange) (h : exprMd.val = Strata.Laurel.StmtExpr.Assert condExpr summary) : Strata.Laurel.ResolveM Strata.Laurel.StmtExprMdStrata.Laurel.Resolution.Check.assert (exprMd condExpr : Strata.Laurel.StmtExprMd) (summary : Option String) (source : Strata.FileRange) (h : exprMd.val = Strata.Laurel.StmtExpr.Assert condExpr summary) : Strata.Laurel.ResolveM Strata.Laurel.StmtExprMd
(Assert)
Γ ⊢ cond ⇐ TBool ────────────────────────────────── Γ ⊢ Assert cond ⇒ TVoid
cond is checked against TBool. assert is a statement: it
yields no value, so it synthesizes TVoid.
\frac{\Gamma \vdash \mathit{cond} \Leftarrow \mathsf{TBool}}{\Gamma \vdash \mathsf{Assume}\;\mathit{cond} \Rightarrow \mathsf{TVoid}} \quad \text{([⇒] Assume)}
def
Strata.Laurel.Resolution.Check.assume (exprMd cond : Strata.Laurel.StmtExprMd) (source : Strata.FileRange) (h : exprMd.val = Strata.Laurel.StmtExpr.Assume cond) : Strata.Laurel.ResolveM Strata.Laurel.StmtExprMdStrata.Laurel.Resolution.Check.assume (exprMd cond : Strata.Laurel.StmtExprMd) (source : Strata.FileRange) (h : exprMd.val = Strata.Laurel.StmtExpr.Assume cond) : Strata.Laurel.ResolveM Strata.Laurel.StmtExprMd
(Assume)
Γ ⊢ cond ⇐ TBool ────────────────────────────────── Γ ⊢ Assume cond ⇒ TVoid
cond is checked against TBool. assume is a statement: it
yields no value, so it synthesizes TVoid.
2.3.7. Assignment
\frac{\Gamma \vdash \mathit{targets}_i \Rightarrow T_i \quad \Gamma \vdash e \Leftarrow \mathit{ExpectedTy}}{\Gamma \vdash \mathsf{Assign}\;\mathit{targets}\;e \Rightarrow \mathit{ExpectedTy}} \quad \text{([⇒] Assign)}
where ExpectedTy = T_1 if |targets| = 1 and MultiValuedExpr [T_1; …; T_n] otherwise.
The target's declared type T_i comes from the variable's scope entry (for
Local and Field)
or from the Declare-bound parameter type. The
RHS receives ExpectedTy via Check.resolveStmtExpr, so bidirectional rules in the
RHS propagate the assignment's type into nested constructs. The
assignment synthesizes ExpectedTy — populating the surrounding
context with the target's type while the RHS is checked against it.
def
Strata.Laurel.Resolution.Synth.assign (exprMd : Strata.Laurel.StmtExprMd) (targets : List Strata.Laurel.VariableMd) (value : Strata.Laurel.StmtExprMd) (source : Strata.FileRange) (h : exprMd.val = Strata.Laurel.StmtExpr.Assign targets value) : Strata.Laurel.ResolveM (Strata.Laurel.StmtExpr × Strata.Laurel.HighTypeMd)Strata.Laurel.Resolution.Synth.assign (exprMd : Strata.Laurel.StmtExprMd) (targets : List Strata.Laurel.VariableMd) (value : Strata.Laurel.StmtExprMd) (source : Strata.FileRange) (h : exprMd.val = Strata.Laurel.StmtExpr.Assign targets value) : Strata.Laurel.ResolveM (Strata.Laurel.StmtExpr × Strata.Laurel.HighTypeMd)
(Assign)
Γ ⊢ targets_i ⇒ T_i Γ ⊢ e ⇐ ExpectedTy ───────────────────────────────────────────────────────── Γ ⊢ Assign targets e ⇒ ExpectedTy
where ExpectedTy = T_1 if |targets| = 1 and otherwise
MultiValuedExpr [T_1; …; T_n]. The target tuple type is pushed
into the RHS via Check.resolveStmtExpr, so bidirectional rules
in the RHS receive the assignment's type. The assignment
synthesizes ExpectedTy — the LHS-derived target tuple type —
so the surrounding context sees the type the RHS was checked
against.
\frac{\Gamma \vdash \mathsf{Assign}\;\mathit{targets}\;e \Rightarrow \mathit{ExpectedTy} \quad T = \mathsf{TVoid} \lor \mathit{ExpectedTy} <: T}{\Gamma \vdash \mathsf{Assign}\;\mathit{targets}\;e \Leftarrow T} \quad \text{([⇐] Assign)}
The check rule synthesizes the assignment's type via [⇒] Assign
and then runs the standard [⇐] Sub boundary check ExpectedTy <: T
— unless T = TVoid, the marker for statement position. Pushing
TVoid through subsumption would only succeed when the LHS is itself
void, which would reject every non-void assignment used as a
statement, so the subsumption is skipped and the synthesized value is
discarded.
def
Strata.Laurel.Resolution.Check.assign (exprMd : Strata.Laurel.StmtExprMd) (targets : List Strata.Laurel.VariableMd) (value : Strata.Laurel.StmtExprMd) (expected : Strata.Laurel.HighTypeMd) (source : Strata.FileRange) (h : exprMd.val = Strata.Laurel.StmtExpr.Assign targets value) : Strata.Laurel.ResolveM Strata.Laurel.StmtExprMdStrata.Laurel.Resolution.Check.assign (exprMd : Strata.Laurel.StmtExprMd) (targets : List Strata.Laurel.VariableMd) (value : Strata.Laurel.StmtExprMd) (expected : Strata.Laurel.HighTypeMd) (source : Strata.FileRange) (h : exprMd.val = Strata.Laurel.StmtExpr.Assign targets value) : Strata.Laurel.ResolveM Strata.Laurel.StmtExprMd
Check-mode rule for assignment. Synthesizes the assignment's type
by inlining the same work as Synth.assign (resolving targets,
pushing the LHS-derived ExpectedTy into the RHS via
Check.resolveStmtExpr), then runs the standard [⇐] Sub
boundary check ExpectedTy <: T against the surrounding expected
— unless T = TVoid, the marker for statement position
(e.g. last statement of a block whose value is being discarded).
Sub against TVoid would only succeed when ExpectedTy = TVoid,
which would reject every non-void assignment used as a statement,
so the subsumption is skipped there. The synthesized value is
discarded in statement position, exactly as for calls.
An unannotated declaring assignment — var x := e, i.e. an Assign
whose sole target is Declare x none — is dispatched to a dedicated
rule pair before [⇒]/[⇐] Assign. The target has no declared type
to push into the RHS, so the direction flips: the initializer is
synthesized and the binding adopts its type.
\frac{x \notin \mathrm{dom}(\Gamma) \quad \Gamma \vdash e \Rightarrow T}{\Gamma \vdash \mathsf{Assign}\;[\mathsf{.Declare}\;\langle x, \mathsf{none}\rangle]\;e \Rightarrow T \quad \dashv \quad \Gamma, x : T} \quad \text{([⇒] Decl-Synth)}
\frac{x \notin \mathrm{dom}(\Gamma) \quad \Gamma \vdash e \Rightarrow T \quad T' = \mathsf{TVoid} \lor T <:_\sim T'}{\Gamma \vdash \mathsf{Assign}\;[\mathsf{.Declare}\;\langle x, \mathsf{none}\rangle]\;e \Leftarrow T' \quad \dashv \quad \Gamma, x : T} \quad \text{([⇐] Decl-Synth)}
The adopted type T must be a value type: a \mathsf{TVoid}
initializer (a void call, a while, …) or a
\mathsf{MultiValuedExpr} (a multi-output call)
[\text{emits “cannot infer a type …”}] and binds
x : \mathsf{Unknown} instead, suppressing cascades on later uses.
As in [⇒] Var-Declare, the node is rewritten to carry
\mathsf{some}\;T, so no none annotation survives resolution.
Unannotated declared targets of a multi-target
assign var x, y := call() don't take this rule; they are recovered
component-wise from the synthesized RHS tuple inside
[⇒]/[⇐] Assign (see the docstrings above).
def
Strata.Laurel.Resolution.Synth.declInfer (exprMd : Strata.Laurel.StmtExprMd) (name : Strata.Laurel.Identifier) (vs : Strata.FileRange) (value : Strata.Laurel.StmtExprMd) (source : Strata.FileRange) (h : exprMd.val = Strata.Laurel.StmtExpr.Assign [{ val := Strata.Laurel.Variable.Declare { name := name, type := none }, source := vs }] value) : Strata.Laurel.ResolveM (Strata.Laurel.StmtExpr × Strata.Laurel.HighTypeMd)Strata.Laurel.Resolution.Synth.declInfer (exprMd : Strata.Laurel.StmtExprMd) (name : Strata.Laurel.Identifier) (vs : Strata.FileRange) (value : Strata.Laurel.StmtExprMd) (source : Strata.FileRange) (h : exprMd.val = Strata.Laurel.StmtExpr.Assign [{ val := Strata.Laurel.Variable.Declare { name := name, type := none }, source := vs }] value) : Strata.Laurel.ResolveM (Strata.Laurel.StmtExpr × Strata.Laurel.HighTypeMd)
(Decl-Synth, synth mode)
x ∉ dom(Γ) Γ ⊢ e ⇒ T ────────────────────────────────────────────── Γ ⊢ (var x := e) ⇒ T ⊣ Γ, x : T
var x := e, an unannotated declaration (Declare x none) with an
initializer. With no annotation to push into the RHS, we synthesize the
initializer's type T and adopt it for the binding. The node is rewritten
to Assign [⟨.Declare x (some T)⟩] e, so no none annotation survives
resolution. This rule handles the sole-target form; unannotated declared
targets of a multi-target assign var x, y := call() are recovered
component-wise inside Synth.assign/Check.assign. The synthesized type
is T, matching Synth.assign's single-target case.
Scoping: the initializer is synthesized before defineNameCheckDup
introduces the binding, so e cannot see the x being declared — a
self-referential var x := x + 1 reports "'x' is not defined" (or reads
an outer x if one is in scope). This is asymmetric with the annotated
path, which resolves targets first: var x : int := x + 1 accepts the
self-reference, reading the fresh (uninitialized) binding. Pinned by
selfRefNoOuter/selfRefOuterShadow in ResolutionTypeCheckTests.
def
Strata.Laurel.Resolution.Check.declInfer (exprMd : Strata.Laurel.StmtExprMd) (name : Strata.Laurel.Identifier) (vs : Strata.FileRange) (value : Strata.Laurel.StmtExprMd) (expected : Strata.Laurel.HighTypeMd) (source : Strata.FileRange) (h : exprMd.val = Strata.Laurel.StmtExpr.Assign [{ val := Strata.Laurel.Variable.Declare { name := name, type := none }, source := vs }] value) : Strata.Laurel.ResolveM Strata.Laurel.StmtExprMdStrata.Laurel.Resolution.Check.declInfer (exprMd : Strata.Laurel.StmtExprMd) (name : Strata.Laurel.Identifier) (vs : Strata.FileRange) (value : Strata.Laurel.StmtExprMd) (expected : Strata.Laurel.HighTypeMd) (source : Strata.FileRange) (h : exprMd.val = Strata.Laurel.StmtExpr.Assign [{ val := Strata.Laurel.Variable.Declare { name := name, type := none }, source := vs }] value) : Strata.Laurel.ResolveM Strata.Laurel.StmtExprMd
(Decl-Synth, check mode) var x := e (Declare x none with initializer)
where a type A is expected (e.g. as the value-producing last statement of
a checked block). Synthesizes the initializer's type and adopts it for the
binding (see Synth.declInfer), then runs the standard [⇐] Sub boundary
check T <: A against the surrounding expected — unless A = TVoid
(statement position), exactly as in Check.assign.
2.3.8. Calls
\frac{\Gamma(\mathit{callee}) = \text{static-procedure with inputs } Ts \text{ and output } [T'] \text{ (single output)} \quad \Gamma \vdash \mathit{args}_i \Leftarrow Ts_i \text{ (pairwise)}}{\Gamma \vdash \mathsf{StaticCall}\;\mathit{callee}\;\mathit{args} \Rightarrow T'} \quad \text{([⇒] Static-Call)}
\frac{\Gamma(\mathit{callee}) = \text{static-procedure with inputs } Ts \text{ and outputs } [T_1; \ldots; T_n],\; n \ge 2 \quad \Gamma \vdash \mathit{args}_i \Leftarrow Ts_i \text{ (pairwise)}}{\Gamma \vdash \mathsf{StaticCall}\;\mathit{callee}\;\mathit{args} \Rightarrow \mathsf{MultiValuedExpr}\;[T_1; \ldots; T_n]} \quad \text{([⇒] Static-Call-Multi)}
def
Strata.Laurel.Resolution.Synth.staticCall (exprMd : Strata.Laurel.StmtExprMd) (callee : Strata.Laurel.Identifier) (args : List Strata.Laurel.StmtExprMd) (source : Strata.FileRange) (h : exprMd.val = Strata.Laurel.StmtExpr.StaticCall callee args) : Strata.Laurel.ResolveM (Strata.Laurel.StmtExpr × Strata.Laurel.HighTypeMd)Strata.Laurel.Resolution.Synth.staticCall (exprMd : Strata.Laurel.StmtExprMd) (callee : Strata.Laurel.Identifier) (args : List Strata.Laurel.StmtExprMd) (source : Strata.FileRange) (h : exprMd.val = Strata.Laurel.StmtExpr.StaticCall callee args) : Strata.Laurel.ResolveM (Strata.Laurel.StmtExpr × Strata.Laurel.HighTypeMd)
Cases on the arity of the callee's declared outputs.
Γ(callee) = static-procedure with inputs Ts (Static-Call) and output [T'] (single output) Γ ⊢ args_i ⇐ Ts_i (pairwise) ────────────────────────────────────────────────────── Γ ⊢ StaticCall callee args ⇒ T' Γ(callee) = static-procedure with inputs Ts (Static-Call-Multi) and outputs [T_1; …; T_n] (n ≥ 2) Γ ⊢ args_i ⇐ Ts_i (pairwise) ────────────────────────────────────────────────────── Γ ⊢ StaticCall callee args ⇒ MultiValuedExpr [T_1; …; T_n]
A callee with zero outputs synthesizes TVoid (the n = 0 case).
The two rules differ only in output arity — argument checking is
identical. Callee is resolved against the expected kinds (parameter,
static procedure, datatype constructor, datatype destructor, constant);
each argument is checked against the corresponding parameter type. The
bidirectional push lets impure-expression arguments ({x := 1; x},
if c then …, holes) flow through their own check rules instead of
bottoming out at the synth wildcard.
When the callee resolves to a static procedure with a known parameter
count and the call supplies more arguments than it declares, an
over-arity diagnostic is emitted (the surplus arguments are still
resolved first, against Unknown, so errors inside them are reported
too). The check fires only for genuine procedures (procArity); for an
unresolved name (where paramTypes = [] purely because the name was not
found), a datatype constructor/tester, a parameter, or a constant, no
arity diagnostic is emitted — surplus arguments are checked against
Unknown, the gradual escape hatch, exactly as before, so no
spurious/duplicate diagnostic is produced. Under-arity (too few
arguments) is deliberately not flagged.
The result type is the (possibly multi-valued) declared output type
from getCallInfo.
\frac{\Gamma \vdash \mathit{target} \Rightarrow \_ \quad \Gamma(\mathit{callee}) = \text{instance- or static-procedure with inputs } [\mathit{self}; Ts] \text{ and output } [T'] \text{ (single output)} \quad \Gamma \vdash \mathit{args}_i \Leftarrow Ts_i \text{ (pairwise; self dropped)}}{\Gamma \vdash \mathsf{InstanceCall}\;\mathit{target}\;\mathit{callee}\;\mathit{args} \Rightarrow T'} \quad \text{([⇒] Instance-Call)}
\frac{\Gamma \vdash \mathit{target} \Rightarrow \_ \quad \Gamma(\mathit{callee}) = \text{instance- or static-procedure with inputs } [\mathit{self}; Ts] \text{ and outputs } [T_1; \ldots; T_n],\; n \ge 2 \quad \Gamma \vdash \mathit{args}_i \Leftarrow Ts_i \text{ (pairwise; self dropped)}}{\Gamma \vdash \mathsf{InstanceCall}\;\mathit{target}\;\mathit{callee}\;\mathit{args} \Rightarrow \mathsf{MultiValuedExpr}\;[T_1; \ldots; T_n]} \quad \text{([⇒] Instance-Call-Multi)}
The callee is resolved against either an instance procedure or a
static procedure (the latter handles uniformly-dispatched call syntax
where the receiver is forwarded as self). Output arity is forwarded
identically to
Synth.staticCall's
single-vs-multi split. In both call families the single- and multi-output
rules differ only in the output arity; argument checking is the same, and
surplus arguments (beyond the declared parameters, or when the callee is
unresolved) are checked against \mathsf{Unknown} rather than flagged as an
arity error. A zero-output (n = 0) procedure call is the third case in the
arity split: it synthesizes \mathsf{TVoid} rather than a
\mathsf{MultiValuedExpr}.
def
Strata.Laurel.Resolution.Synth.instanceCall (exprMd target : Strata.Laurel.StmtExprMd) (callee : Strata.Laurel.Identifier) (args : List Strata.Laurel.StmtExprMd) (source : Strata.FileRange) (h : exprMd.val = Strata.Laurel.StmtExpr.InstanceCall target callee args) : Strata.Laurel.ResolveM (Strata.Laurel.StmtExpr × Strata.Laurel.HighTypeMd)Strata.Laurel.Resolution.Synth.instanceCall (exprMd target : Strata.Laurel.StmtExprMd) (callee : Strata.Laurel.Identifier) (args : List Strata.Laurel.StmtExprMd) (source : Strata.FileRange) (h : exprMd.val = Strata.Laurel.StmtExpr.InstanceCall target callee args) : Strata.Laurel.ResolveM (Strata.Laurel.StmtExpr × Strata.Laurel.HighTypeMd)
Cases on the arity of the callee's declared outputs.
Γ ⊢ target ⇒ _ (Instance-Call) Γ(callee) = instance- or static-procedure with inputs [self; Ts] and output [T'] (single output) Γ ⊢ args_i ⇐ Ts_i (pairwise; self dropped) ───────────────────────────────────────── Γ ⊢ InstanceCall target callee args ⇒ T' Γ ⊢ target ⇒ _ (Instance-Call-Multi) Γ(callee) = instance- or static-procedure with inputs [self; Ts] and outputs [T_1; …; T_n] (n ≥ 2) Γ ⊢ args_i ⇐ Ts_i (pairwise; self dropped) ───────────────────────────────────────── Γ ⊢ InstanceCall target callee args ⇒ MultiValuedExpr [T_1; …; T_n]
A callee with zero outputs synthesizes TVoid (the n = 0 case).
The two rules differ only in output arity. Target is synthesized;
callee resolves to an instance or static procedure; arguments are
checked pairwise against the callee's parameter types after dropping
self. As in Synth.staticCall, supplying more arguments than the
callee declares (compared against the post-self parameter count) emits
an over-arity diagnostic when the callee genuinely resolves to a
procedure, while surplus arguments against any other resolution kind are
still checked against Unknown with no arity diagnostic. Like
Synth.staticCall, the push is bidirectional so block- and
conditional-shaped arguments route through their own check rules.
2.3.9. Operators
Operators are not a distinct kind of expression, and there are no
operator-specific typing rules. x + y parses as
\mathsf{StaticCall}\;\$\mathsf{add}\;[x; y], a call to an overloaded
built-in wrapper procedure declared in CoreDefinitionsForLaurel and
prepended to every program, so operators are typed entirely by
[⇒] Static-Call above. What used to be an operator's admissible
operand types is now just the set of declared overloads:
procedure $add(x: int, y: int) : int return intAdd(x, y); procedure $add(x: real, y: real) : real return realAdd(x, y);
Each wrapper is a thin transparent procedure delegating to a
type-specific external (intAdd, realAdd, …) that
LaurelToCoreSchemaPass recognizes and lowers to the corresponding
Core operator. The wrappers of one operator must all share a name —
the parser cannot know which overload a + denotes — while the
externals they delegate to do not.
Two consequences of typing operators as calls:
- Operand admissibility is overload selection
There is no
Numericside-condition.1 + 2.0is rejected not because a rule demands equal operand types, but because neither theintnor therealoverload of$addaccepts an(\mathsf{TInt}, \mathsf{TReal})pair — reported as no overload of '$add' matches the argument types. Likewise<on bitvectors resolves only at the widths Core provides operators for (1, 8, 16, 32, 64), rather than silently mistranslating other widths.- Preconditions come from the wrapper
Because a wrapper is an ordinary procedure it can carry a contract.
$divdeclaresrequires y != 0and delegates to Core's safe division, so a possible division by zero surfaces as a failed precondition on the call.
The gradual \mathsf{Unknown} still flows freely: it is a consistent
subtype of every parameter type, so it never rules an overload out. An
\mathsf{Unknown} argument therefore cannot discriminate between
overloads, but the other arguments still can — selection runs on the
informative arguments alone, and only an unresolved result caused by an
\mathsf{Unknown} argument is passed over silently (the argument's own
error already covers it) instead of being reported as a no-match or an
ambiguity.
Operator overload selection
-
1 + 2selects theintoverload and synthesizes\mathsf{TInt} -
1.5 + 2.5selects therealoverload and synthesizes\mathsf{TReal} -
<?> + 1selects theintoverload — the informative operand decides -
<?> + <?>is unresolved and synthesizes\mathsf{Unknown}; no error is reported -
1 + 2.0is rejected: no overload of '$add' matches the argument types
Equality is the one operator that is not a transparent wrapper.
$eq / $neq are declared external, because equality is polymorphic
and Laurel has no polymorphic types: a wrapper body would carry a
placeholder \mathsf{int} \to \mathsf{int} \to \mathsf{bool}
signature into Core and fail to unify against a composite, a datatype,
or a bool. Synth.staticCall special-cases these two names to require
only that the operands be consistent (T_l \sim T_r), and
LaurelToCoreSchemaPass lowers them straight to Core's polymorphic
equality.
\frac{\Gamma \vdash \mathit{lhs} \Rightarrow T_l \quad \Gamma \vdash \mathit{rhs} \Rightarrow T_r \quad T_l \sim T_r \quad T_l \neq \mathsf{TVoid} \quad T_r \neq \mathsf{TVoid} \quad \mathit{callee} \in \{\$\mathsf{eq}, \$\mathsf{neq}\}}{\Gamma \vdash \mathsf{StaticCall}\;\mathit{callee}\;[\mathit{lhs}; \mathit{rhs}] \Rightarrow \mathsf{TBool}} \quad \text{([⇒] Op-Eq)}
The \neq \mathsf{TVoid} premises reject void operands even though
\mathsf{TVoid} \sim \mathsf{TVoid} holds: a void expression carries no
value to compare.
Since an operator is a call, the check-mode rule for one is [⇐] Sub applied to [⇒] Static-Call: the call's synthesized result type is compared against the expected type. There is no separate operand-pushing rule, so a mixed-type operator expression reports one overload-resolution failure over the whole call rather than a mismatch against an individual operand.
2.3.10. Object forms
\frac{\mathit{ref} \text{ is a composite or datatype, or is unresolved, or is absent from } \Gamma}{\Gamma \vdash \mathsf{New}\;\mathit{ref} \Rightarrow \mathsf{UserDefined}\;\mathit{ref}} \quad \text{([⇒] New-Ok)}
\frac{\mathit{ref} \text{ resolves to a non-type kind}}{\Gamma \vdash \mathsf{New}\;\mathit{ref} \Rightarrow \mathsf{Unknown}} \quad \text{([⇒] New-Fallback)}
The \mathsf{Unknown} fallback fires only when \mathit{ref} resolves to
a present definition whose kind is neither composite nor datatype. An
unresolved or out-of-scope \mathit{ref} takes the New-Ok branch instead, so
the kind diagnostic that resolveRef already emitted is not duplicated.
def
Strata.Laurel.Resolution.Synth.new (ref : Strata.Laurel.Identifier) (typeArgs : List Strata.Laurel.HighTypeMd) (source : Strata.FileRange) : Strata.Laurel.ResolveM (Strata.Laurel.StmtExpr × Strata.Laurel.HighTypeMd)Strata.Laurel.Resolution.Synth.new (ref : Strata.Laurel.Identifier) (typeArgs : List Strata.Laurel.HighTypeMd) (source : Strata.FileRange) : Strata.Laurel.ResolveM (Strata.Laurel.StmtExpr × Strata.Laurel.HighTypeMd)
Cases on whether ref resolves to a composite/datatype.
ref is a composite or datatype, (New-Ok) or is unresolved, or is absent from Γ ────────────────────────────────────── Γ ⊢ New ref ⇒ UserDefined ref ref resolves to a non-type kind (New-Fallback) ────────────────────────────────────── Γ ⊢ New ref ⇒ Unknown
When ref resolves to a composite or datatype, the type is
UserDefined ref — or, for an explicit instantiation new C<τ…>, the
applied type Applied (UserDefined ref) [τ…], so the type checker and
MonomorphizeComposites see the concrete instantiation (mirroring
computeExprType's .New arm). A bare new C carries no type args and
keeps the plain UserDefined type. The Unknown fallback fires only
when ref resolves to a present definition whose kind is neither
composite nor datatype (e.g. a variable or procedure name); this
suppresses cascading errors after the kind diagnostic has already fired.
An unresolved ref, or one absent from scope, takes the UserDefined
branch instead — resolveRef has already reported the name, so
re-flagging it here would only duplicate that diagnostic. The explicit
type args are resolved (so a .TVar inside is reclassified and a bad
arg reported) and their count is checked against the composite's
declared type-arg arity.
\frac{\Gamma \vdash \mathit{target} \Rightarrow U \quad U \sim T \lor U <: T \lor T <: U}{\Gamma \vdash \mathsf{AsType}\;\mathit{target}\;T \Rightarrow T} \quad \text{([⇒] AsType)}
def
Strata.Laurel.Resolution.Synth.asType (exprMd target : Strata.Laurel.StmtExprMd) (ty : Strata.Laurel.HighTypeMd) (h : exprMd.val = Strata.Laurel.StmtExpr.AsType target ty) : Strata.Laurel.ResolveM (Strata.Laurel.StmtExpr × Strata.Laurel.HighTypeMd)Strata.Laurel.Resolution.Synth.asType (exprMd target : Strata.Laurel.StmtExprMd) (ty : Strata.Laurel.HighTypeMd) (h : exprMd.val = Strata.Laurel.StmtExpr.AsType target ty) : Strata.Laurel.ResolveM (Strata.Laurel.StmtExpr × Strata.Laurel.HighTypeMd)
(AsType)
Γ ⊢ target ⇒ U U ~ T ∨ U <: T ∨ T <: U ────────────────────────────────────────────── Γ ⊢ AsType target T ⇒ T
target synthesizes some type U; the cast is allowed when U and
T sit in the same lineage modulo gradual Unknown — either
consistent after unfolding aliases/constrained types (e.g. 5 as Int
where Int is a wrapper over int), or a subtype in either
direction (downcast animal as Cat when Cat extends Animal,
upcast cat as Animal). Sibling casts (Dog as Cat) and casts
between unrelated primitives ("hi" as int) are rejected. The
synthesized type is T — the user's claim is honored once the
relation check passes.
\frac{\Gamma \vdash \mathit{target} \Rightarrow U \quad U \sim T \lor U <: T \lor T <: U}{\Gamma \vdash \mathsf{IsType}\;\mathit{target}\;T \Rightarrow \mathsf{TBool}} \quad \text{([⇒] IsType)}
def
Strata.Laurel.Resolution.Synth.isType (exprMd target : Strata.Laurel.StmtExprMd) (ty : Strata.Laurel.HighTypeMd) (source : Strata.FileRange) (h : exprMd.val = Strata.Laurel.StmtExpr.IsType target ty) : Strata.Laurel.ResolveM (Strata.Laurel.StmtExpr × Strata.Laurel.HighTypeMd)Strata.Laurel.Resolution.Synth.isType (exprMd target : Strata.Laurel.StmtExprMd) (ty : Strata.Laurel.HighTypeMd) (source : Strata.FileRange) (h : exprMd.val = Strata.Laurel.StmtExpr.IsType target ty) : Strata.Laurel.ResolveM (Strata.Laurel.StmtExpr × Strata.Laurel.HighTypeMd)
(IsType)
Γ ⊢ target ⇒ U U ~ T ∨ U <: T ∨ T <: U ────────────────────────────────────────────── Γ ⊢ IsType target T ⇒ TBool
Same lineage check as AsType — is only makes sense between types
that share a lineage modulo gradual Unknown; testing 5 is Cat
is statically nonsense. The synthesized type is TBool.
\frac{\Gamma \vdash \mathit{lhs} \Rightarrow T_l \quad \Gamma \vdash \mathit{rhs} \Rightarrow T_r \quad \mathsf{isReference}\;T_l \quad \mathsf{isReference}\;T_r \quad T_l \sim T_r}{\Gamma \vdash \mathsf{ReferenceEquals}\;\mathit{lhs}\;\mathit{rhs} \Rightarrow \mathsf{TBool}} \quad \text{([⇒] RefEq)}
isReference T holds when T is a UserDefined
or Unknown type. ~ is the consistency relation
isConsistent — symmetric, with the
Unknown wildcard.
def
Strata.Laurel.Resolution.Synth.refEq (exprMd : Strata.Laurel.StmtExprMd) (expr : Strata.Laurel.StmtExpr) (lhs rhs : Strata.Laurel.StmtExprMd) (source : Strata.FileRange) (h_expr : expr = Strata.Laurel.StmtExpr.ReferenceEquals lhs rhs) (h : exprMd.val = Strata.Laurel.StmtExpr.ReferenceEquals lhs rhs) : Strata.Laurel.ResolveM (Strata.Laurel.StmtExpr × Strata.Laurel.HighTypeMd)Strata.Laurel.Resolution.Synth.refEq (exprMd : Strata.Laurel.StmtExprMd) (expr : Strata.Laurel.StmtExpr) (lhs rhs : Strata.Laurel.StmtExprMd) (source : Strata.FileRange) (h_expr : expr = Strata.Laurel.StmtExpr.ReferenceEquals lhs rhs) (h : exprMd.val = Strata.Laurel.StmtExpr.ReferenceEquals lhs rhs) : Strata.Laurel.ResolveM (Strata.Laurel.StmtExpr × Strata.Laurel.HighTypeMd)
(RefEq)
Γ ⊢ lhs ⇒ T_l Γ ⊢ rhs ⇒ T_r isReference T_l isReference T_r T_l ~ T_r ────────────────────────────────────────────────── Γ ⊢ ReferenceEquals lhs rhs ⇒ TBool
Both operands must be reference types (UserDefined or Unknown) —
reference equality is meaningless on primitives. They must also be
mutually CONSISTENT (isConsistent, symmetric), which for two
UserDefined types is NAME equality (not subtyping): Cat and Dog
are rejected, and even Cat/Animal (subtype) is rejected — only an
Unknown operand flows freely against the other via the gradual wildcard.
\frac{\Gamma \vdash \mathit{target} \Rightarrow T_t \quad \Gamma(f) = T_f \quad \Gamma \vdash \mathit{newVal} \Leftarrow T_f}{\Gamma \vdash \mathsf{PureFieldUpdate}\;\mathit{target}\;f\;\mathit{newVal} \Rightarrow T_t} \quad \text{([⇒] PureFieldUpdate)}
def
Strata.Laurel.Resolution.Synth.pureFieldUpdate (exprMd target : Strata.Laurel.StmtExprMd) (fieldName : Strata.Laurel.Identifier) (newVal : Strata.Laurel.StmtExprMd) (h : exprMd.val = Strata.Laurel.StmtExpr.PureFieldUpdate target fieldName newVal) : Strata.Laurel.ResolveM (Strata.Laurel.StmtExpr × Strata.Laurel.HighTypeMd)Strata.Laurel.Resolution.Synth.pureFieldUpdate (exprMd target : Strata.Laurel.StmtExprMd) (fieldName : Strata.Laurel.Identifier) (newVal : Strata.Laurel.StmtExprMd) (h : exprMd.val = Strata.Laurel.StmtExpr.PureFieldUpdate target fieldName newVal) : Strata.Laurel.ResolveM (Strata.Laurel.StmtExpr × Strata.Laurel.HighTypeMd)
(PureFieldUpdate)
Γ ⊢ target ⇒ T_t Γ(f) = T_f Γ ⊢ newVal ⇐ T_f ───────────────────────────────────────────────────── Γ ⊢ PureFieldUpdate target f newVal ⇒ T_t
target is synthesized, f resolved against T_t (or the enclosing
instance type), and newVal checked against the field's declared
type. The synthesized type is T_t — updating a field on a pure type
produces a new value of the same type.
2.3.11. Verification expressions
\frac{\Gamma, x : T \vdash \mathit{body} \Leftarrow \mathsf{TBool}}{\Gamma \vdash \mathsf{Quantifier}\;\mathit{mode}\;\langle x, T\rangle\;\mathit{trig}\;\mathit{body} \Rightarrow \mathsf{TBool}} \quad \text{([⇒] Quantifier)}
def
Strata.Laurel.Resolution.Synth.quantifier (exprMd : Strata.Laurel.StmtExprMd) (mode : Strata.Laurel.QuantifierMode) (param : Strata.Laurel.Parameter) (trigger : Option Strata.Laurel.StmtExprMd) (body : Strata.Laurel.StmtExprMd) (source : Strata.FileRange) (h : exprMd.val = Strata.Laurel.StmtExpr.Quantifier mode param trigger body) : Strata.Laurel.ResolveM (Strata.Laurel.StmtExpr × Strata.Laurel.HighTypeMd)Strata.Laurel.Resolution.Synth.quantifier (exprMd : Strata.Laurel.StmtExprMd) (mode : Strata.Laurel.QuantifierMode) (param : Strata.Laurel.Parameter) (trigger : Option Strata.Laurel.StmtExprMd) (body : Strata.Laurel.StmtExprMd) (source : Strata.FileRange) (h : exprMd.val = Strata.Laurel.StmtExpr.Quantifier mode param trigger body) : Strata.Laurel.ResolveM (Strata.Laurel.StmtExpr × Strata.Laurel.HighTypeMd)
(Quantifier)
Γ, x : T ⊢ body ⇐ TBool ──────────────────────────────────────────── Γ ⊢ Quantifier mode ⟨x, T⟩ trig body ⇒ TBool
Opens a fresh scope, binds x : T (in scope only for the body and
trigger), resolves the optional trigger, and checks the body against
TBool since a quantifier is a proposition. Without that body check,
forall x: int :: x + 1 would be silently accepted. The construct
itself synthesizes TBool.
\frac{\Gamma \vdash \mathit{name} \Rightarrow \_}{\Gamma \vdash \mathsf{Assigned}\;\mathit{name} \Rightarrow \mathsf{TBool}} \quad \text{([⇒] Assigned)}
def
Strata.Laurel.Resolution.Synth.assigned (exprMd name : Strata.Laurel.StmtExprMd) (source : Strata.FileRange) (h : exprMd.val = Strata.Laurel.StmtExpr.Assigned name) : Strata.Laurel.ResolveM (Strata.Laurel.StmtExpr × Strata.Laurel.HighTypeMd)Strata.Laurel.Resolution.Synth.assigned (exprMd name : Strata.Laurel.StmtExprMd) (source : Strata.FileRange) (h : exprMd.val = Strata.Laurel.StmtExpr.Assigned name) : Strata.Laurel.ResolveM (Strata.Laurel.StmtExpr × Strata.Laurel.HighTypeMd)
(Assigned)
Γ ⊢ name ⇒ _ ──────────────────────────── Γ ⊢ Assigned name ⇒ TBool
assigned x is a verification predicate that holds when x has
been definitely assigned. The construct unconditionally synthesizes
TBool; the operand's synthesized type is discarded, and Assigned
imposes no constraint on it.
The operand is still resolved (via Synth.resolveStmtExpr) purely
for its name-resolution side effects — its identifier must point at a
definition so that downstream passes can reason about the binding —
but the result type is thrown away. Assigned is meant to name a
variable or field, yet its AST field is an arbitrary StmtExpr
(Assigned (name : StmtExprMd)), so this rule does not enforce
that shape: it is not correct-by-construction, and the type checker
deliberately leaves the operand unconstrained rather than rejecting,
say, assigned (a + b).
\frac{\Gamma \vdash v \Leftarrow T}{\Gamma \vdash \mathsf{Old}\;v \Leftarrow T} \quad \text{([⇐] Old)}
def
Strata.Laurel.Resolution.Check.old (exprMd val : Strata.Laurel.StmtExprMd) (expected : Strata.Laurel.HighTypeMd) (source : Strata.FileRange) (h : exprMd.val = Strata.Laurel.StmtExpr.Old val) : Strata.Laurel.ResolveM Strata.Laurel.StmtExprMdStrata.Laurel.Resolution.Check.old (exprMd val : Strata.Laurel.StmtExprMd) (expected : Strata.Laurel.HighTypeMd) (source : Strata.FileRange) (h : exprMd.val = Strata.Laurel.StmtExpr.Old val) : Strata.Laurel.ResolveM Strata.Laurel.StmtExprMd
(Old)
Γ ⊢ v ⇐ T ─────────────── Γ ⊢ Old v ⇐ T
old(v) refers to the pre-state value of v in a postcondition.
It has the same type as v, so the surrounding expectation
propagates straight through: v is checked against the same T,
and the result is wrapped back up as Old v'.
The rule is type-transparent and deliberately does not restrict
v to an identifier or lvalue. old wraps an arbitrary expression
(Old (value : StmtExprMd)), matching Dafny, where old(this.f + g()) is legal — the pre-state is taken of the whole expression.
Whether v denotes something whose pre-state is meaningful is a
well-formedness question for the verifier's heap model, not a typing
one, so resolution only resolves names inside v and checks its
type; it imposes no syntactic shape on v.
old is type-transparent, so it also synthesizes: in operand position
(e.g. the postcondition pattern ensures counter.value == old(counter.value) + 1,
where == synthesizes its operands) v is synthesized and its type
returned unchanged.
\frac{\Gamma \vdash v \Rightarrow T}{\Gamma \vdash \mathsf{Old}\;v \Rightarrow T} \quad \text{([⇒] Old-Synth)}
def
Strata.Laurel.Resolution.Synth.old (exprMd val : Strata.Laurel.StmtExprMd) (source : Strata.FileRange) (h : exprMd.val = Strata.Laurel.StmtExpr.Old val) : Strata.Laurel.ResolveM (Strata.Laurel.StmtExpr × Strata.Laurel.HighTypeMd)Strata.Laurel.Resolution.Synth.old (exprMd val : Strata.Laurel.StmtExprMd) (source : Strata.FileRange) (h : exprMd.val = Strata.Laurel.StmtExpr.Old val) : Strata.Laurel.ResolveM (Strata.Laurel.StmtExpr × Strata.Laurel.HighTypeMd)
(Old-Synth)
Γ ⊢ v ⇒ T ─────────────── Γ ⊢ Old v ⇒ T
old is a universal morphism: it is fully type-transparent, so
old(v) has exactly the type of v and passes through every
operation. When old(...) appears in a synthesis position (e.g. as
an operand of ==/</++, which synthesize their operands — the
documented postcondition pattern ensures counter.value == old(counter.value) + 1), v is synthesized and its type T is
returned unchanged, wrapped back up as Old v'. Without this rule the
construct would fall into the synth wildcard and spuriously report
that its type cannot be synthesized.
\frac{\Gamma \vdash v \Rightarrow T \quad \mathsf{isReference}\;T}{\Gamma \vdash \mathsf{Fresh}\;v \Rightarrow \mathsf{TBool}} \quad \text{([⇒] Fresh)}
def
Strata.Laurel.Resolution.Synth.fresh (exprMd : Strata.Laurel.StmtExprMd) (expr : Strata.Laurel.StmtExpr) (val : Strata.Laurel.StmtExprMd) (source : Strata.FileRange) (h_expr : expr = Strata.Laurel.StmtExpr.Fresh val) (h : exprMd.val = Strata.Laurel.StmtExpr.Fresh val) : Strata.Laurel.ResolveM (Strata.Laurel.StmtExpr × Strata.Laurel.HighTypeMd)Strata.Laurel.Resolution.Synth.fresh (exprMd : Strata.Laurel.StmtExprMd) (expr : Strata.Laurel.StmtExpr) (val : Strata.Laurel.StmtExprMd) (source : Strata.FileRange) (h_expr : expr = Strata.Laurel.StmtExpr.Fresh val) (h : exprMd.val = Strata.Laurel.StmtExpr.Fresh val) : Strata.Laurel.ResolveM (Strata.Laurel.StmtExpr × Strata.Laurel.HighTypeMd)
(Fresh)
Γ ⊢ v ⇒ T isReference T ──────────────────────────── Γ ⊢ Fresh v ⇒ TBool
v is synthesized and must have a reference type (UserDefined or
Unknown) — Fresh only makes sense on heap-allocated references, so
fresh(5) is rejected. The construct itself synthesizes TBool.
\frac{\Gamma \vdash v \Leftarrow T \quad \Gamma \vdash \mathit{proof} \Rightarrow \_}{\Gamma \vdash \mathsf{ProveBy}\;v\;\mathit{proof} \Leftarrow T} \quad \text{([⇐] ProveBy)}
def
Strata.Laurel.Resolution.Check.proveBy (exprMd val proof : Strata.Laurel.StmtExprMd) (expected : Strata.Laurel.HighTypeMd) (source : Strata.FileRange) (h : exprMd.val = Strata.Laurel.StmtExpr.ProveBy val proof) : Strata.Laurel.ResolveM Strata.Laurel.StmtExprMdStrata.Laurel.Resolution.Check.proveBy (exprMd val proof : Strata.Laurel.StmtExprMd) (expected : Strata.Laurel.HighTypeMd) (source : Strata.FileRange) (h : exprMd.val = Strata.Laurel.StmtExpr.ProveBy val proof) : Strata.Laurel.ResolveM Strata.Laurel.StmtExprMd
(ProveBy)
Γ ⊢ v ⇐ T Γ ⊢ proof ⇒ _ ──────────────────────────── Γ ⊢ ProveBy v proof ⇐ T
ProveBy v proof has the same type as v (the proof is just a hint
for downstream verification), so the surrounding expectation
propagates into v. The proof itself has no constraint on its type
and is still synthesized.
Like old, ProveBy is type-transparent in v, so it also
synthesizes: in operand position v is synthesized for its type T,
\mathit{proof} is synthesized only for its name-resolution side
effects (its type discarded), and T is returned.
\frac{\Gamma \vdash v \Rightarrow T \quad \Gamma \vdash \mathit{proof} \Rightarrow \_}{\Gamma \vdash \mathsf{ProveBy}\;v\;\mathit{proof} \Rightarrow T} \quad \text{([⇒] ProveBy-Synth)}
def
Strata.Laurel.Resolution.Synth.proveBy (exprMd val proof : Strata.Laurel.StmtExprMd) (source : Strata.FileRange) (h : exprMd.val = Strata.Laurel.StmtExpr.ProveBy val proof) : Strata.Laurel.ResolveM (Strata.Laurel.StmtExpr × Strata.Laurel.HighTypeMd)Strata.Laurel.Resolution.Synth.proveBy (exprMd val proof : Strata.Laurel.StmtExprMd) (source : Strata.FileRange) (h : exprMd.val = Strata.Laurel.StmtExpr.ProveBy val proof) : Strata.Laurel.ResolveM (Strata.Laurel.StmtExpr × Strata.Laurel.HighTypeMd)
(ProveBy-Synth)
Γ ⊢ v ⇒ T Γ ⊢ proof ⇒ _ ──────────────────────────── Γ ⊢ ProveBy v proof ⇒ T
Like old, ProveBy v proof is type-transparent in v — the proof
is just a hint for downstream verification and carries no typing
constraint. In a synthesis position v is synthesized for its type
T, proof is synthesized only for its name-resolution side effects
(its type is discarded), and T is returned.
2.3.12. Self reference
\frac{\Gamma.\mathit{instanceTypeName} = \mathsf{some}\;T}{\Gamma \vdash \mathsf{This} \Rightarrow \mathsf{UserDefined}\;T} \quad \text{([⇒] This-Inside)}
\frac{\Gamma.\mathit{instanceTypeName} = \mathsf{none}}{\Gamma \vdash \mathsf{This} \Rightarrow \mathsf{Unknown} \quad [\text{emits “‘this’ is not allowed outside instance methods”}]} \quad \text{([⇒] This-Outside)}
def
Strata.Laurel.Resolution.Synth.this (source : Strata.FileRange) : Strata.Laurel.ResolveM (Strata.Laurel.StmtExpr × Strata.Laurel.HighTypeMd)Strata.Laurel.Resolution.Synth.this (source : Strata.FileRange) : Strata.Laurel.ResolveM (Strata.Laurel.StmtExpr × Strata.Laurel.HighTypeMd)
Cases on whether instanceTypeName is set (i.e., we're inside an
instance method).
Γ.instanceTypeName = some T (This-Inside) ─────────────────────────── Γ ⊢ This ⇒ UserDefined T Γ.instanceTypeName = none (This-Outside) ─────────────────────────── Γ ⊢ This ⇒ Unknown (emits "'this' is not allowed outside instance methods")
When instanceTypeName is set (we're inside an instance method,
populated on ResolveState by resolveInstanceProcedure for the
duration of an instance method body), This synthesizes
UserDefined T. With it, this.field and instance-method dispatch
synthesize real types instead of being wildcarded through Unknown.
Otherwise an error is emitted ("'this' is not allowed outside instance
methods") and the type collapses to Unknown to suppress cascading
errors.
2.3.13. Untyped forms
\frac{}{\Gamma \vdash \mathsf{Abstract}\,/\,\mathsf{All}\;\ldots \Rightarrow \mathsf{Unknown}} \quad \text{([⇒] Abstract / All)}
def
Strata.Laurel.Resolution.Synth.abstract (source : Strata.FileRange) : Strata.Laurel.StmtExpr × Strata.Laurel.HighTypeMdStrata.Laurel.Resolution.Synth.abstract (source : Strata.FileRange) : Strata.Laurel.StmtExpr × Strata.Laurel.HighTypeMd
Γ ⊢ Abstract ⇒ Unknown
def
Strata.Laurel.Resolution.Synth.all (source : Strata.FileRange) : Strata.Laurel.StmtExpr × Strata.Laurel.HighTypeMdStrata.Laurel.Resolution.Synth.all (source : Strata.FileRange) : Strata.Laurel.StmtExpr × Strata.Laurel.HighTypeMd
Γ ⊢ All ⇒ Unknown
2.3.14. ContractOf
\frac{\mathit{fn} = \mathsf{Var}\;(\mathsf{.Local}\;\mathit{id}) \quad \Gamma(\mathit{id}) \in \{\mathit{staticProcedure}, \mathit{instanceProcedure}, \mathit{unresolved}\}}{\Gamma \vdash \mathsf{ContractOf}\;\mathsf{Precondition}\;\mathit{fn} \Rightarrow \mathsf{TBool} \qquad \Gamma \vdash \mathsf{ContractOf}\;\mathsf{PostCondition}\;\mathit{fn} \Rightarrow \mathsf{TBool}} \quad \text{([⇒] ContractOf-Bool)}
\frac{\mathit{fn} = \mathsf{Var}\;(\mathsf{.Local}\;\mathit{id}) \quad \Gamma(\mathit{id}) \in \{\mathit{staticProcedure}, \mathit{instanceProcedure}, \mathit{unresolved}\}}{\Gamma \vdash \mathsf{ContractOf}\;\mathsf{Reads}\;\mathit{fn} \Rightarrow \mathsf{TSet}\;\mathsf{Unknown} \qquad \Gamma \vdash \mathsf{ContractOf}\;\mathsf{Modifies}\;\mathit{fn} \Rightarrow \mathsf{TSet}\;\mathsf{Unknown}} \quad \text{([⇒] ContractOf-Set)}
\frac{\mathit{fn} \text{ is not a } \mathsf{Var}\;(\mathsf{.Local}) \text{ resolving to a procedure or unresolved name}}{\Gamma \vdash \mathsf{ContractOf}\;\ldots\;\mathit{fn} \rightsquigarrow \text{error: “‘contractOf’ expected a procedure reference”}} \quad \text{([⇒] ContractOf-Error)}
The \mathit{unresolved} kind is admitted so an already-reported
name-resolution error is not duplicated; ContractOf-Error fires only when
\mathit{fn} resolves to a present non-procedure definition (or is not a
local reference at all).
def
Strata.Laurel.Resolution.Synth.contractOf (exprMd : Strata.Laurel.StmtExprMd) (ty : Strata.Laurel.ContractType) (fn : Strata.Laurel.StmtExprMd) (source : Strata.FileRange) (h : exprMd.val = Strata.Laurel.StmtExpr.ContractOf ty fn) : Strata.Laurel.ResolveM (Strata.Laurel.StmtExpr × Strata.Laurel.HighTypeMd)Strata.Laurel.Resolution.Synth.contractOf (exprMd : Strata.Laurel.StmtExprMd) (ty : Strata.Laurel.ContractType) (fn : Strata.Laurel.StmtExprMd) (source : Strata.FileRange) (h : exprMd.val = Strata.Laurel.StmtExpr.ContractOf ty fn) : Strata.Laurel.ResolveM (Strata.Laurel.StmtExpr × Strata.Laurel.HighTypeMd)
Cases on the contract type ty and on whether fn is a procedure
reference.
fn = Var (.Local id) (ContractOf-Bool)
Γ(id) ∈ {staticProcedure, instanceProcedure, unresolved}
────────────────────────────────────────────
Γ ⊢ ContractOf Precondition fn ⇒ TBool
Γ ⊢ ContractOf PostCondition fn ⇒ TBool
fn = Var (.Local id) (ContractOf-Set)
Γ(id) ∈ {staticProcedure, instanceProcedure, unresolved}
────────────────────────────────────────────
Γ ⊢ ContractOf Reads fn ⇒ TSet Unknown
Γ ⊢ ContractOf Modifies fn ⇒ TSet Unknown
fn is not a Var (.Local) resolving to a procedure (ContractOf-Error)
or unresolved name
────────────────────────────────────────────
Γ ⊢ ContractOf _ fn ↝ error: "'contractOf' expected a procedure reference"
ContractOf ty fn extracts a procedure's contract clause as a value:
its preconditions (Precondition), postconditions (PostCondition),
reads set (Reads), or modifies set (Modifies). fn must be a
direct identifier reference resolving to a procedure — a contract
belongs to a named procedure, not an arbitrary expression. The
diagnostic "'contractOf' expected a procedure reference" fires (and
the construct synthesizes Unknown to suppress cascading errors) when
fn is anything other than a Var (.Local id), or resolves to a
present definition that is not a procedure. An unresolved id, or
one absent from scope, is accepted without firing the diagnostic —
its name-resolution error was already reported.
Precondition and PostCondition are propositions, hence TBool.
Reads and Modifies are sets of heap-allocated locations —
composite/datatype references and fields. The element type is left as
Unknown for now since the rule doesn't yet recover it from fn's
declared modifies/reads clauses.
The constructor is reserved for future use — Laurel's grammar has no
contractOf production today, and the translator emits "not yet
implemented" for it. The typing rule exists so resolution remains
exhaustive over StmtExpr.
2.3.15. Holes
\frac{T_h <: T}{\Gamma \vdash \mathsf{Hole}\;d\;(\mathsf{some}\;T_h) \Leftarrow T} \quad \text{([⇐] Hole-Some)}
def
Strata.Laurel.Resolution.Check.holeSome (det : Bool) (ty expected : Strata.Laurel.HighTypeMd) (source : Strata.FileRange) : Strata.Laurel.ResolveM Strata.Laurel.StmtExprMdStrata.Laurel.Resolution.Check.holeSome (det : Bool) (ty expected : Strata.Laurel.HighTypeMd) (source : Strata.FileRange) : Strata.Laurel.ResolveM Strata.Laurel.StmtExprMd
(Hole-Some)
T_h <: T ──────────────────────────── Γ ⊢ Hole d (some T_h) ⇐ T
A typed hole carries the user's annotation T_h. The annotation is
resolved and verified against the surrounding expected type via
subsumption; the resolved annotation is preserved on the node so
downstream passes (hole elimination) can generate correctly typed
uninterpreted functions.
\frac{}{\Gamma \vdash \mathsf{Hole}\;d\;\mathsf{none} \Leftarrow T \quad \mapsto \quad \mathsf{Hole}\;d\;(\mathsf{some}\;T)} \quad \text{([⇐] Hole-None)}
def
Strata.Laurel.Resolution.Check.holeNone (det : Bool) (expected : Strata.Laurel.HighTypeMd) (source : Strata.FileRange) : Strata.Laurel.StmtExprMdStrata.Laurel.Resolution.Check.holeNone (det : Bool) (expected : Strata.Laurel.HighTypeMd) (source : Strata.FileRange) : Strata.Laurel.StmtExprMd
(Hole-None)
──────────────────────────────────────── Γ ⊢ Hole d none ⇐ T ↦ Γ ⊢ Hole d (some T)
An untyped hole in check mode records the expected type on the node so downstream passes (hole elimination) don't have to infer it again.
In synth position no expected type is available to push into the hole, so
an unannotated hole synthesizes the gradual \mathsf{Unknown} while an
annotated hole synthesizes its annotation T_h (this is what lets
<?> + 1 synthesize \mathsf{TInt}).
\frac{}{\Gamma \vdash \mathsf{Hole}\;d\;\mathsf{none} \Rightarrow \mathsf{Unknown}} \quad \text{([⇒] Hole-Synth-None)}
\frac{}{\Gamma \vdash \mathsf{Hole}\;d\;(\mathsf{some}\;T_h) \Rightarrow T_h} \quad \text{([⇒] Hole-Synth-Some)}
2.3.16. 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.
\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)}
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
Check.return) or via
named-output assignment.
def
Strata.Laurel.resolveProcedure (proc : Strata.Laurel.Procedure) : Strata.Laurel.ResolveM Strata.Laurel.ProcedureStrata.Laurel.resolveProcedure (proc : Strata.Laurel.Procedure) : Strata.Laurel.ResolveM Strata.Laurel.Procedure
(Procedure)
T_o-bar = proc.outputs.types Γ_global, params(proc) ⊢ proc.body ⇒ _ ────────────────────────────────────────────────────────── Γ_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.
def
Strata.Laurel.resolveInstanceProcedure (typeName : Strata.Laurel.Identifier) (proc : Strata.Laurel.Procedure) : Strata.Laurel.ResolveM Strata.Laurel.ProcedureStrata.Laurel.resolveInstanceProcedure (typeName : Strata.Laurel.Identifier) (proc : Strata.Laurel.Procedure) : Strata.Laurel.ResolveM Strata.Laurel.Procedure
Resolve an instance procedure on a composite type.