From e491d47237acfc9ae563eac08823e16db27a5870 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 29 Jun 2026 14:42:51 +0000 Subject: [PATCH 01/20] Update Laurel documentation --- Strata/Languages/Laurel/LaurelAST.lean | 4 +- Strata/Languages/Laurel/Resolution.lean | 2 +- docs/Testing.md | 6 +- ...{LaurelDoc.lean => LaurelDesignGuide.lean} | 115 +---- docs/verso/LaurelDesignGuideMain.lean | 18 + docs/verso/LaurelImplementationGuide.lean | 155 ++++++ docs/verso/LaurelImplementationGuideMain.lean | 18 + docs/verso/LaurelUserGuide.lean | 463 ++++++++++++++++++ ...lDocMain.lean => LaurelUserGuideMain.lean} | 4 +- docs/verso/Makefile | 2 +- docs/verso/generate.sh | 4 +- docs/verso/index.html | 14 +- docs/verso/lakefile.toml | 22 +- 13 files changed, 698 insertions(+), 129 deletions(-) rename docs/verso/{LaurelDoc.lean => LaurelDesignGuide.lean} (89%) create mode 100644 docs/verso/LaurelDesignGuideMain.lean create mode 100644 docs/verso/LaurelImplementationGuide.lean create mode 100644 docs/verso/LaurelImplementationGuideMain.lean create mode 100644 docs/verso/LaurelUserGuide.lean rename docs/verso/{LaurelDocMain.lean => LaurelUserGuideMain.lean} (74%) diff --git a/Strata/Languages/Laurel/LaurelAST.lean b/Strata/Languages/Laurel/LaurelAST.lean index fb02d7cd59..1b74656832 100644 --- a/Strata/Languages/Laurel/LaurelAST.lean +++ b/Strata/Languages/Laurel/LaurelAST.lean @@ -13,7 +13,9 @@ public import Strata.Util.FileRange open StrataDDM /- -Documentation for Laurel can be found in docs/verso/LaurelDoc.lean +Documentation for Laurel can be found in docs/verso/LaurelDesignGuide.lean +(language definition) and docs/verso/LaurelImplementationGuide.lean +(translation to Core). This module contains the Laurel AST. The high-level Laurel API is in `Strata.Languages.Laurel`. diff --git a/Strata/Languages/Laurel/Resolution.lean b/Strata/Languages/Laurel/Resolution.lean index 7398e5e4e8..d3b8c7ee36 100644 --- a/Strata/Languages/Laurel/Resolution.lean +++ b/Strata/Languages/Laurel/Resolution.lean @@ -607,7 +607,7 @@ statements are in effect position (synthesized and discarded via Each typing rule is implemented as its own helper inside the mutual block below. Helpers are grouped by section to mirror the *Typing -rules* index in `LaurelDoc.lean`: +rules* index in `LaurelDesignGuide.lean`: - Literals — `Synth.litInt`, `Synth.litBool`, `Synth.litString`, `Synth.litDecimal` - Variables — `Synth.varLocal`, `Synth.varField`, `Check.varDeclare` diff --git a/docs/Testing.md b/docs/Testing.md index 59719528f1..6e4121562b 100644 --- a/docs/Testing.md +++ b/docs/Testing.md @@ -122,9 +122,9 @@ lifting, constrained-type elimination, …) before translating to Core and verifying. Several of those passes re-run `resolve` on their output. So a diagnostic that only `testLaurel` surfaces may originate from a later pass, not the verifier. The major passes are described in the **Translation -Pipeline** section of the Laurel language manual — published at -[strata-org.github.io/Strata](https://strata-org.github.io/Strata/laurel/html-single/), -source in [`docs/verso/LaurelDoc.lean`](verso/LaurelDoc.lean) — and the full +Pipeline** section of the Laurel implementation guide — published at +[strata-org.github.io/Strata](https://strata-org.github.io/Strata/laurelimpl/html-single/), +source in [`docs/verso/LaurelImplementationGuide.lean`](verso/LaurelImplementationGuide.lean) — and the full pass list and exact ordering live in [`Strata/Languages/Laurel/LaurelCompilationPipeline.lean`](../Strata/Languages/Laurel/LaurelCompilationPipeline.lean) (`laurelPipeline`). diff --git a/docs/verso/LaurelDoc.lean b/docs/verso/LaurelDesignGuide.lean similarity index 89% rename from docs/verso/LaurelDoc.lean rename to docs/verso/LaurelDesignGuide.lean index 4de8a96ba4..ba8dfcf384 100644 --- a/docs/verso/LaurelDoc.lean +++ b/docs/verso/LaurelDesignGuide.lean @@ -24,84 +24,6 @@ open Verso.Genre.Manual.InlineLean set_option pp.rawOnError true -/-- Markdown documentation for all Laurel passes, including their - `comesBefore`/`comesAfter` ordering rationales. Note: pass - `documentation`/`reason` strings are rendered as Markdown, so avoid raw - `` text (it is treated as inline HTML and crashes Verso's - converter); use backticks for inline code instead. -/ -def laurelPipelineDocsMarkdown : String := - let entries := allPasses.map fun pass => - let base := s!"- **{pass.name}**: {pass.documentation}" - let beforeDeps := pass.comesBefore.map fun cb => - s!" - Comes before **{cb.pass.name}** because: {cb.reason}" - let afterDeps := pass.comesAfter.map fun ca => - s!" - Comes after **{ca.pass.name}** because: {ca.reason}" - let deps := beforeDeps ++ afterDeps - if deps.isEmpty then base - else base ++ "\n" ++ "\n".intercalate deps - "\n".intercalate entries.toList - -/-- Markdown dependency graph for the Laurel passes, derived from the - `comesBefore`/`comesAfter` properties. -/ -def laurelPipelineDependencyGraphMarkdown : String := Id.run do - -- Collect all edges: (source, target, reason) where source comesBefore target - let mut edges : List (String × String × String) := [] - for pass in allPasses do - -- `pass.comesBefore` declares: pass must run before cb.pass, i.e. pass → cb.pass - for cb in pass.comesBefore do - edges := edges ++ [(pass.name, cb.pass.name, cb.reason)] - -- `pass.comesAfter` declares: pass must run after ca.pass, i.e. ca.pass → pass - for ca in pass.comesAfter do - edges := edges ++ [(ca.pass.name, pass.name, ca.reason)] - - -- Deduplicate edges with the same (source, target), keeping the first reason. - edges := edges.foldl (init := []) fun acc e => - if acc.any (fun a => a.1 == e.1 && a.2.1 == e.2.1) then acc else acc ++ [e] - - -- Build the graph as a markdown list showing dependencies - let mut md := "**Dependency edges** (A → B means A must run before B):\n\n" - if edges.isEmpty then - md := md ++ "*No ordering constraints declared.*\n" - else - for (src, tgt, reason) in edges do - md := md ++ s!"- **{src}** → **{tgt}**\n - *{reason}*\n" - - -- Add a textual rendering of the pipeline order with dependency annotations - md := md ++ "\n**Pipeline execution order** (→ X: must run before X; ← X: must run after X):\n\n" - md := md ++ "```\n" - let mut idx := 1 - for pass in allPasses do - let beforeDeps := pass.comesBefore.map (s!" → {·.pass.name}") - let afterDeps := pass.comesAfter.map (s!" ← {·.pass.name}") - let deps := beforeDeps ++ afterDeps - let depStr := if deps.isEmpty then "" else String.join deps - md := md ++ s!"{idx}. {pass.name}{depStr}\n" - idx := idx + 1 - md := md ++ "```\n" - return md - -/-- Block command that generates documentation for all Laurel pipeline passes. - Usage inside a `#doc` block: `{laurelPipelineDocs}` -/ -@[block_command] -def laurelPipelineDocs : Verso.Doc.Elab.BlockCommandOf Unit := fun () => do - let md := laurelPipelineDocsMarkdown - let some ast := MD4Lean.parse md - | Lean.throwError "Failed to parse laurelPipelineDocumentation as Markdown" - let blocks ← ast.blocks.mapM (Markdown.blockFromMarkdown · (handleHeaders := Markdown.strongEmphHeaders)) - `(Verso.Doc.Block.concat #[$blocks,*]) - -/-- Block command that generates a dependency graph for the Laurel pipeline passes - based on the `comesBefore` and `comesAfter` properties. - Usage inside a `#doc` block: `{laurelPipelineDependencyGraph}` -/ -@[block_command] -def laurelPipelineDependencyGraph : Verso.Doc.Elab.BlockCommandOf Unit := fun () => do - let md := laurelPipelineDependencyGraphMarkdown - let some ast := MD4Lean.parse md - | Lean.throwError "Failed to parse laurelPipelineDependencyGraph as Markdown" - let blocks ← ast.blocks.mapM (Markdown.blockFromMarkdown · (handleHeaders := Markdown.strongEmphHeaders)) - `(Verso.Doc.Block.concat #[$blocks,*]) - --- A set-apart *example* box. Renders its contents inside a tinted, bordered -- panel with an "Example" header, so concrete examples stand out from the -- surrounding explanatory prose. Authored via the `:::example` directive below. block_extension Block.«example» (title : Option String) where @@ -166,9 +88,9 @@ def «example» : Verso.Doc.Elab.DirectiveExpanderOf LaurelExampleConfig let args ← stxs.mapM Verso.Doc.Elab.elabBlock ``(Verso.Doc.Block.other (Block.«example» $(Lean.quote title)) #[ $[ $args ],* ]) -#doc (Manual) "The Laurel Language" => +#doc (Manual) "The Laurel Language Design Guide" => %%% -shortTitle := "Laurel" +shortTitle := "Laurel Design" %%% # Introduction @@ -957,35 +879,6 @@ named-output assignment. {docstring Strata.Laurel.resolveInstanceProcedure} -# Implementation - -The static semantics of Laurel are defined by `Resolution.lean`. This is where Laurel references are resolved and where type checking is done. Calling `resolve` will produce diagnostics and a `SemanticModel` that can be used to navigate between definitions and references. -If new references or definitions are created during compilation, `resolve` must be called again to get a complete model. - -## Translation Pipeline - -The Laurel to Core translation pipeline uses these IRs: -- Laurel -- UnorderedCoreWithLaurelTypes -- CoreWithLaurelTypes -- Core - -Most of the passes are in the Laurel IR. -The transparency pass goes from `Laurel` to `UnorderedCoreWithLaurelTypes`. -The CoreGroupingAndOrdering goes from `UnorderedCoreWithLaurelTypes` to `CoreWithLaurelTypes` -And the LaurelToCoreSchemaPass goes from `CoreWithLaurelTypes` to `Core`. - -## Passes - -The following passes making up the compilation of Laurel to Core: - -{laurelPipelineDocs} - -## Pass Dependency Graph - -The following graph shows the ordering constraints between passes. - -{laurelPipelineDependencyGraph} # Differences between Laurel and Core @@ -1015,7 +908,3 @@ var y: int; var z: int; hasThreeOutputs(out x, out y, out z); ``` - -## Implementation - -In Laurel, all verification concepts, such as assume statements, pre and postconditions, and transparency of procedures, are part of the language. In Core however, there is the concept of metadata. Concepts that relate to only one or a few analyses might not be considered concepts of the Core language, and will then be represented using metadata instead of being given a typed representation in the AST. diff --git a/docs/verso/LaurelDesignGuideMain.lean b/docs/verso/LaurelDesignGuideMain.lean new file mode 100644 index 0000000000..3aa10eee02 --- /dev/null +++ b/docs/verso/LaurelDesignGuideMain.lean @@ -0,0 +1,18 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + + + +import LaurelDesignGuide +open Verso.Genre.Manual (RenderConfig manualMain) + +def config : RenderConfig where + emitTeX := false + emitHtmlSingle := .immediately + emitHtmlMulti := .no + htmlDepth := 2 + +def main := manualMain (%doc LaurelDesignGuide) (config := config) diff --git a/docs/verso/LaurelImplementationGuide.lean b/docs/verso/LaurelImplementationGuide.lean new file mode 100644 index 0000000000..be60bb235d --- /dev/null +++ b/docs/verso/LaurelImplementationGuide.lean @@ -0,0 +1,155 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import VersoManual + +import Strata.Languages.Laurel.LaurelAST +import Strata.Languages.Laurel.LaurelTypes +import Strata.Languages.Laurel.LaurelCompilationPipeline +import Strata.Languages.Laurel.HeapParameterization +import Strata.Languages.Laurel.LiftImperativeExpressions +import Strata.Languages.Laurel.ModifiesClauses + +open Strata.Laurel + +-- This gets access to most of the manual genre +open Verso.Genre Manual + +-- This gets access to Lean code that's in code blocks, elaborated in the same process and +-- environment as Verso +open Verso.Genre.Manual.InlineLean + +set_option pp.rawOnError true + +/-- Markdown documentation for all Laurel passes, including their + `comesBefore`/`comesAfter` ordering rationales. Note: pass + `documentation`/`reason` strings are rendered as Markdown, so avoid raw + `` text (it is treated as inline HTML and crashes Verso's + converter); use backticks for inline code instead. -/ +def laurelPipelineDocsMarkdown : String := + let entries := allPasses.map fun pass => + let base := s!"- **{pass.name}**: {pass.documentation}" + let beforeDeps := pass.comesBefore.map fun cb => + s!" - Comes before **{cb.pass.name}** because: {cb.reason}" + let afterDeps := pass.comesAfter.map fun ca => + s!" - Comes after **{ca.pass.name}** because: {ca.reason}" + let deps := beforeDeps ++ afterDeps + if deps.isEmpty then base + else base ++ "\n" ++ "\n".intercalate deps + "\n".intercalate entries.toList + +/-- Markdown dependency graph for the Laurel passes, derived from the + `comesBefore`/`comesAfter` properties. -/ +def laurelPipelineDependencyGraphMarkdown : String := Id.run do + -- Collect all edges: (source, target, reason) where source comesBefore target + let mut edges : List (String × String × String) := [] + for pass in allPasses do + -- `pass.comesBefore` declares: pass must run before cb.pass, i.e. pass → cb.pass + for cb in pass.comesBefore do + edges := edges ++ [(pass.name, cb.pass.name, cb.reason)] + -- `pass.comesAfter` declares: pass must run after ca.pass, i.e. ca.pass → pass + for ca in pass.comesAfter do + edges := edges ++ [(ca.pass.name, pass.name, ca.reason)] + + -- Deduplicate edges with the same (source, target), keeping the first reason. + edges := edges.foldl (init := []) fun acc e => + if acc.any (fun a => a.1 == e.1 && a.2.1 == e.2.1) then acc else acc ++ [e] + + -- Build the graph as a markdown list showing dependencies + let mut md := "**Dependency edges** (A → B means A must run before B):\n\n" + if edges.isEmpty then + md := md ++ "*No ordering constraints declared.*\n" + else + for (src, tgt, reason) in edges do + md := md ++ s!"- **{src}** → **{tgt}**\n - *{reason}*\n" + + -- Add a textual rendering of the pipeline order with dependency annotations + md := md ++ "\n**Pipeline execution order** (→ X: must run before X; ← X: must run after X):\n\n" + md := md ++ "```\n" + let mut idx := 1 + for pass in allPasses do + let beforeDeps := pass.comesBefore.map (s!" → {·.pass.name}") + let afterDeps := pass.comesAfter.map (s!" ← {·.pass.name}") + let deps := beforeDeps ++ afterDeps + let depStr := if deps.isEmpty then "" else String.join deps + md := md ++ s!"{idx}. {pass.name}{depStr}\n" + idx := idx + 1 + md := md ++ "```\n" + return md + +/-- Block command that generates documentation for all Laurel pipeline passes. + Usage inside a `#doc` block: `{laurelPipelineDocs}` -/ +@[block_command] +def laurelPipelineDocs : Verso.Doc.Elab.BlockCommandOf Unit := fun () => do + let md := laurelPipelineDocsMarkdown + let some ast := MD4Lean.parse md + | Lean.throwError "Failed to parse laurelPipelineDocumentation as Markdown" + let blocks ← ast.blocks.mapM (Markdown.blockFromMarkdown · (handleHeaders := Markdown.strongEmphHeaders)) + `(Verso.Doc.Block.concat #[$blocks,*]) + +/-- Block command that generates a dependency graph for the Laurel pipeline passes + based on the `comesBefore` and `comesAfter` properties. + Usage inside a `#doc` block: `{laurelPipelineDependencyGraph}` -/ +@[block_command] +def laurelPipelineDependencyGraph : Verso.Doc.Elab.BlockCommandOf Unit := fun () => do + let md := laurelPipelineDependencyGraphMarkdown + let some ast := MD4Lean.parse md + | Lean.throwError "Failed to parse laurelPipelineDependencyGraph as Markdown" + let blocks ← ast.blocks.mapM (Markdown.blockFromMarkdown · (handleHeaders := Markdown.strongEmphHeaders)) + `(Verso.Doc.Block.concat #[$blocks,*]) + + +#doc (Manual) "The Laurel Implementation Guide" => +%%% +shortTitle := "Laurel Implementation" +%%% + +# Language definition +The Laurel language definitions consists of its type, its grammar and its semantics. Currently the semantics is split into a static part, called the resolver, and a dynamic part. + +TODO map the different parts of the language definition to the files that implement them. + +## Resolution +The static semantics of Laurel are defined by `Resolution.lean`. This is where Laurel references are resolved and where type checking is done. Calling `resolve` will produce diagnostics and a `SemanticModel` that can be used to navigate between definitions and references. + +## Type definition +The Laurel type definition allows many more programs than are required for the language as it is documented for the user. The reason for this is the compilation of Laurel to different languages. However, despite being wide, the Laurel language type is kept as precise as possible given the flexibility that it needs. + +In the Laurel type, constructors are combined when this does not reduce precision. For example, instead of having a separate constructor for StmtExpr.Forall and for StmtExpr.Exists, there is a single StmtExpr.Quantifier with a boolean field to determine its type. A more complicated example: calls to primitive operators and to statically defined user defined functions, and to user defined instance functions, all go through the same StmtExpr.Call constructor. + +# Compilation to Core +To enable its verification analyses, Laurel compiles to Core. Compilation happens over many passes. A compilation pass may not change the semantics of the program, so it may not emit any diagnostics, errors or warnings. A compilation pass may only refer to AST nodes that relates to its business logic: it may not define AST traversals without using helper methods, to allow adding new AST nodes without breaking existing compilation passes. + +If new references or definitions are created during compilation, `Resolution.resolve` must be called again to get a complete model. + +## Translation Pipeline + +The Laurel to Core translation pipeline uses these IRs: +- Laurel +- UnorderedCoreWithLaurelTypes +- CoreWithLaurelTypes +- Core + +Most of the passes are in the Laurel IR. +The transparency pass goes from `Laurel` to `UnorderedCoreWithLaurelTypes`. +The CoreGroupingAndOrdering goes from `UnorderedCoreWithLaurelTypes` to `CoreWithLaurelTypes` +And the LaurelToCoreSchemaPass goes from `CoreWithLaurelTypes` to `Core`. + +## Passes + +The following passes making up the compilation of Laurel to Core: + +{laurelPipelineDocs} + +## Pass Dependency Graph + +The following graph shows the ordering constraints between passes. + +{laurelPipelineDependencyGraph} + +## Implementation + +In Laurel, all verification concepts, such as assume statements, pre and postconditions, and transparency of procedures, are part of the language. In Core however, there is the concept of metadata. Concepts that relate to only one or a few analyses might not be considered concepts of the Core language, and will then be represented using metadata instead of being given a typed representation in the AST. diff --git a/docs/verso/LaurelImplementationGuideMain.lean b/docs/verso/LaurelImplementationGuideMain.lean new file mode 100644 index 0000000000..e2b49f340d --- /dev/null +++ b/docs/verso/LaurelImplementationGuideMain.lean @@ -0,0 +1,18 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + + + +import LaurelImplementationGuide +open Verso.Genre.Manual (RenderConfig manualMain) + +def config : RenderConfig where + emitTeX := false + emitHtmlSingle := .immediately + emitHtmlMulti := .no + htmlDepth := 2 + +def main := manualMain (%doc LaurelImplementationGuide) (config := config) diff --git a/docs/verso/LaurelUserGuide.lean b/docs/verso/LaurelUserGuide.lean new file mode 100644 index 0000000000..49777d0064 --- /dev/null +++ b/docs/verso/LaurelUserGuide.lean @@ -0,0 +1,463 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import VersoManual + +-- This gets access to most of the manual genre +open Verso.Genre Manual + +-- This gets access to Lean code that's in code blocks, elaborated in +-- the same process and environment as Verso +open Verso.Genre.Manual.InlineLean + +#doc (Manual) "The Laurel User Guide" => +%%% +shortTitle := "Laurel User Guide" +%%% + +# Summary + +Laurel is an intermediate verification language. It is the common target for +verifiers built on top of garbage-collected, imperative source languages such +as Java, Python, and JavaScript. You usually do not write Laurel by hand; +a front-end translates your annotated source program into Laurel, and Laurel is +then checked for correctness. Understanding Laurel helps you understand what the +front-end checks and why a verification succeeds or fails. + +Laurel is built to be both *complete* and *accurate*. It is complete because you +can specify any behavior you want and have it checked against the +implementation. It is accurate because, when the underlying solver cannot decide +whether a program meets its specification, you can supply hints — extra +assertions, loop invariants, or contracts — that let it reach a definite answer. +Some properties, such as the absence of common runtime errors, are checked +without you having to state them. + +Under the hood, Laurel discharges its proof obligations using a Satisfiability +Modulo Theories (SMT) solver. For simple obligations the solver finds a proof on +its own. For harder ones it needs guidance, and most of this guide is about the +constructs you use to provide that guidance. + +## A first program + +A Laurel program is a sequence of declarations. The most important one is the +*procedure*. A procedure has input parameters, optional output parameters +introduced with `returns`, an optional contract, and a body enclosed in braces. +Statements inside the body are separated by semicolons. + +``` +program Laurel; +procedure addOne(x: int) returns (r: int) + opaque + ensures r == x + 1 +{ + r := x; + r++; + r++ +}; +``` + +The `opaque` keyword marks a procedure whose body is hidden from its callers: +callers reason about it only through its contract (`requires` / `ensures` / +`modifies`). This is the standard *modular* style — each procedure is verified +once against its contract, and call sites trust the contract rather than the +body. + +# Laurel without verification + +TODO, cover all the non-verification language parts + +## Primitive types + +Laurel provides unbounded mathematical `int` and `real` types, a `bool` type, +`string`, and fixed-width bitvectors. Because `int` is unbounded, arithmetic in +specifications behaves like ordinary mathematics: there is no overflow to reason +around when you are stating what a procedure computes. + +## Composites + +Laurel models objects with *composite* types. A composite declares mutable +fields and may declare *instance procedures* (methods). Fields are read and +written with the `#` selector, instances are created with `new`, and a method is +invoked with the same `#` syntax. + +``` +program Laurel; +composite Counter { + var count: int + procedure reset(self: Counter) + opaque + ensures self#count == 0 + modifies self + { + self#count := 0 + }; +} + +procedure useCounter() + opaque +{ + var c: Counter := new Counter; + c#reset(); + assert c#count == 0 +}; +``` + +An instance procedure takes its receiver as an explicit `self` parameter and +refers to fields through it. The contract of a method uses the same `requires` / +`ensures` / `modifies` clauses as any other procedure; here `ensures self#count +== 0` is what lets the caller conclude `c#count == 0` after `c#reset()`. + +Field selection and method calls chain, so you can reach through one object to +another: `o#inner#x` reads field `x` of the object stored in `o`'s `inner` field, +and `o#inner#isOne()` calls a method on it. + +``` +program Laurel; +composite Inner { var x: int } +composite Outer { var inner: Inner } + +procedure useOuter() + opaque +{ + var o: Outer := new Outer; + var v: int := o#inner#x +}; +``` + +# Verification fundamentals + +## Assertions + +An `assert` states a fact that Laurel must prove holds at that point in the +program. If the solver cannot prove it, verification fails and the failing +`assert` is reported. + +``` +program Laurel; +procedure checkPositive(x: int) + requires x > 0 + opaque +{ + assert x > 0; + assert x >= 1 +}; +``` + +The dual of `assert` is `assume`. An `assume` introduces a fact without proof: +from that point on, Laurel reasons as if the assumed expression is true. Assuming +something false makes everything afterwards trivially provable, which is +occasionally useful but should be used with care. + +``` +program Laurel; +procedure assumeThenProve() + opaque +{ + assume false; + assert false // provable: we assumed a contradiction +}; +``` + +Assertions are the building block behind every other verification feature in +this guide. Preconditions, postconditions, and loop invariants are all +ultimately checked by turning them into assertions at the right program points. + +## Loop invariants + +Laurel cannot know in advance how many times a loop runs, so it reasons about +loops through a *loop invariant*: a condition that holds every time the loop +guard is evaluated — on first entry and after each execution of the body. + +A loop invariant serves two purposes. Inside the loop it tells Laurel what is +true, which is what lets it prove that operations in the body are safe. After the +loop it combines with the negated guard to describe the state on exit. + +``` +program Laurel; +procedure countUp() + opaque +{ + var n: int := 5; + var i: int := 0; + while (i < n) + invariant i >= 0 + invariant i <= n + { + i := i + 1 + }; + assert i == n +}; +``` + +The two invariants together establish `i == n` after the loop: the loop exits +when `i < n` is false, so `i >= n`, and the second invariant gives `i <= n`. + +A loop invariant must hold *on entry* and be *preserved* by the body. If it fails +on entry, Laurel reports the error at the offending invariant. For example, +initializing `i` to `-1` above would break `invariant i >= 0` before the loop +even starts, and that specific invariant is flagged. + +## Preconditions + +A *precondition*, written with `requires`, states what must be true when a +procedure is called. It has two effects. It restricts callers: every call site +must prove the precondition holds for the arguments it passes. And it gives the +body an assumption to work from when proving its own obligations. + +``` +program Laurel; +procedure halve(x: int) returns (r: int) + requires x > 0 + opaque + ensures r >= 0 +{ + r := x / 2 +}; + +procedure caller() + opaque +{ + var a: int := halve(10); // ok: 10 > 0 + var b: int := halve(0) // error: precondition does not hold +}; +``` + +A procedure may have several `requires` clauses; they are conjoined. A call must +satisfy all of them. + +``` +program Laurel; +procedure addBoth(x: int, y: int) returns (r: int) + requires x > 0 + requires y > 0 + opaque + ensures r > 0 +{ + r := x + y +}; +``` + +Functions support `requires` clauses too, with the same meaning: each use of the +function must prove the requirement. + +## Postconditions + +A *postcondition*, written with `ensures`, states what a procedure guarantees +when it returns. Laurel checks the body against every `ensures` clause, and +callers may rely on those clauses without looking at the body. Postconditions are +how you say precisely what a procedure does. + +``` +program Laurel; +procedure max(x: int, y: int) returns (r: int) + opaque + ensures r >= x + ensures r >= y + ensures r == x || r == y +{ + if x > y then { r := x } + else { r := y } +}; +``` + +At a call site, the postcondition is all the caller knows about the result: + +``` +program Laurel; +procedure useMax() + opaque +{ + var m: int := max(3, 7); + assert m >= 3; + assert m >= 7 + // we cannot assert m == 7 here: the contract only promises r >= x, r >= y, + // and r == x || r == y, which does not pin m to 7. +}; +``` + +Postconditions and preconditions work together. It is common to need a +precondition in order to be able to prove a postcondition, and adding that +precondition simultaneously rules out the calls for which the procedure would not +behave as specified. + +## Quantifier + +For specifications that range over many values, Laurel provides *quantifiers*. +A `forall` states that its body holds for every value of the bound variables; an +`exists` states that there is at least one value for which the body holds. Both +take one or more typed binders and a body introduced with `=>`. + +``` +program Laurel; +procedure quantifiers() + opaque +{ + assert forall(x: int) => x + 0 == x; + assert exists(x: int) => x == 42 +}; +``` + +The implication operator `==>` is frequently used inside quantifiers to restrict +the range of interest — for instance, to say something about every index of an +array within bounds: + +``` +program Laurel; +procedure inContract(n: int) + requires n > 0 + opaque + ensures forall(i: int) => i >= 0 ==> i < n ==> i < n + 1 +{ +}; +``` + +Because a `forall` over an infinite domain (such as all integers) cannot be +checked by enumeration, the solver reasons about it logically. To control how it +instantiates a quantifier, you can attach a *trigger* — a pattern in braces that +tells the solver which terms should cause the quantified fact to fire: + +``` +program Laurel; +function P(x: int): int; +procedure withTrigger() + opaque +{ + assume forall(i: int) { P(i) } => P(i) == i + 1; + assert P(1) == 2 // the term P(1) matches the trigger, so the fact fires +}; +``` + +# Verification of object mutation + + +## Modifies clauses + +When a procedure may change the fields of objects on the heap, it must say so +with a `modifies` clause. The clause lists the references the procedure is +allowed to mutate. This *frame* is what callers rely on to know what did *not* +change across a call. + +A `modifies` clause is especially important on `opaque` procedures: without it, a +caller would have to assume the call could have changed any heap state. With it, +the caller keeps every fact about objects outside the frame. + +``` +program Laurel; +composite Container { + var value: int +} + +procedure bump(c: Container) + opaque + modifies c +{ + c#value := c#value + 1 +}; + +procedure caller() + opaque +{ + var c: Container := new Container; + var d: Container := new Container; + var x: int := d#value; + bump(c); + assert x == d#value // holds: only c is in bump's modifies clause +}; +``` + +A procedure that writes to a field it has not listed is rejected, and so is a +call that passes more permission than the caller itself holds. You can list +several references by repeating the clause (`modifies c; modifies d`), and the +wildcard `modifies *` permits modifying any object — at the cost of telling +callers that nothing on the heap is preserved. + +Objects allocated with `new` *inside* the procedure body are exempt: a freshly +allocated object may be modified freely without appearing in the `modifies` +clause, because no caller could hold any prior knowledge about it. + +``` +program Laurel; +composite Container { var value: int } + +procedure makeOne() + opaque +{ + var c: Container := new Container; + c#value := 1 // allowed: c is freshly allocated here +}; +``` + +## Old + +In a postcondition you often want to relate the state when the procedure returns +to the state when it was entered. Wrapping an expression in `old(...)` evaluates +that expression in the *pre-state* — the heap as it was on entry. This is the +standard way to specify a procedure that mutates its arguments. + +``` +program Laurel; +composite Cell { + var value: int +} + +procedure bumpCell(c: Cell) + opaque + ensures c#value == old(c#value) + 1 + modifies c +{ + c#value := c#value + 1 +}; +``` + +Here `c#value` denotes the value on return and `old(c#value)` the value on entry, +so the postcondition says the field grew by exactly one. Without `old`, the +clause would read `c#value == c#value + 1`, which no implementation can satisfy. + +`old` distributes through the structure of an expression, so you can wrap a whole +sub-expression: `old(2 * c#value + 3)` means the same as `2 * old(c#value) + 3`. +It may also appear inside quantifiers and conditionals in a postcondition: + +``` +program Laurel; +composite Cell { var value: int } + +procedure strictBump(c: Cell) + opaque + ensures forall(other: Cell) => other == c ==> other#value > old(other#value) + modifies c +{ + c#value := c#value + 1 +}; +``` + +A caller can reproduce the two-state reasoning by snapshotting the pre-state into +a local variable before the call and asserting against it afterwards: + +``` +program Laurel; +composite Cell { var value: int } + +procedure bumpCell(c: Cell) + opaque + ensures c#value == old(c#value) + 1 + modifies c +{ + c#value := c#value + 1 +}; + +procedure bumpCellCaller() + opaque +{ + var c: Cell := new Cell; + var pre: int := c#value; + bumpCell(c); + assert c#value == pre + 1 +}; +``` + +An `old(...)` that mentions nothing from the heap has no effect and Laurel warns +about it, since it cannot relate two states. The same warning is issued for a +redundant `old(old(...))`, whose inner `old` is dropped. diff --git a/docs/verso/LaurelDocMain.lean b/docs/verso/LaurelUserGuideMain.lean similarity index 74% rename from docs/verso/LaurelDocMain.lean rename to docs/verso/LaurelUserGuideMain.lean index 6328fd7de7..1177242378 100644 --- a/docs/verso/LaurelDocMain.lean +++ b/docs/verso/LaurelUserGuideMain.lean @@ -6,7 +6,7 @@ -import LaurelDoc +import LaurelUserGuide open Verso.Genre.Manual (RenderConfig manualMain) def config : RenderConfig where @@ -15,4 +15,4 @@ def config : RenderConfig where emitHtmlMulti := .no htmlDepth := 2 -def main := manualMain (%doc LaurelDoc) (config := config) +def main := manualMain (%doc LaurelUserGuide) (config := config) diff --git a/docs/verso/Makefile b/docs/verso/Makefile index 792976a10b..0e18e926c9 100644 --- a/docs/verso/Makefile +++ b/docs/verso/Makefile @@ -1,5 +1,5 @@ PORT ?= 1080 -BOOKS := ddm langdef laurel transforms +BOOKS := ddm langdef laureldesign laurelimpl laurelguide transforms .PHONY: $(BOOKS) all clean build-% serve-% diff --git a/docs/verso/generate.sh b/docs/verso/generate.sh index efdf481ebc..069805ea08 100755 --- a/docs/verso/generate.sh +++ b/docs/verso/generate.sh @@ -16,7 +16,9 @@ lake build Strata:docs cd "${curpwd}" lake exe ddm --with-html-single --output _out/ddm lake exe langdef --with-html-single --output _out/langdef -lake exe laurel --with-html-single --output _out/laurel +lake exe laureldesign --with-html-single --output _out/laureldesign +lake exe laurelimpl --with-html-single --output _out/laurelimpl +lake exe laurelguide --with-html-single --output _out/laurelguide lake exe transforms --with-html-single --output _out/transforms lake exe irtranslation --with-html-single --output _out/irtranslation cp strata-hourglass.png _out/langdef/html-single/ diff --git a/docs/verso/index.html b/docs/verso/index.html index 8520f789a1..9f4db6fd4c 100644 --- a/docs/verso/index.html +++ b/docs/verso/index.html @@ -32,9 +32,17 @@

DDM Documentation

Strata Core Language Definition Documentation

Documentation for Strata Core language definition.

- -

Laurel Language Documentation

-

Documentation for the Laurel intermediate verification language. Laurel attempts to provide features that are common to Java, Python, and JavaScript.

+ +

Laurel Language Design Guide

+

How the Laurel intermediate verification language is defined: its types, unified expression/statement model, procedures, programs, and type checking. Laurel attempts to provide features that are common to Java, Python, and JavaScript.

+ + +

Laurel Implementation Guide

+

How a checked Laurel program is lowered to Strata Core: the translation pipeline, its passes and their ordering, and the differences between Laurel and Core.

+ + +

Laurel User Guide

+

A task-oriented guide to writing Laurel specifications: assertions, loop invariants, pre- and postconditions, quantifiers, objects, modifies clauses, and old.

Core Transforms and Analysis

diff --git a/docs/verso/lakefile.toml b/docs/verso/lakefile.toml index 7c445d9057..a2986bd4f5 100644 --- a/docs/verso/lakefile.toml +++ b/docs/verso/lakefile.toml @@ -1,5 +1,5 @@ name = "StrataDoc" -defaultTargets = ["ddm", "langdef", "laurel", "transforms", "irtranslation"] +defaultTargets = ["ddm", "langdef", "laureldesign", "laurelimpl", "laurelguide", "transforms", "irtranslation"] [[require]] name = "Strata" @@ -25,11 +25,25 @@ name = "langdef" root = "LangDefDocMain" [[lean_lib]] -name = "LaurelDoc" +name = "LaurelDesignGuide" [[lean_exe]] -name = "laurel" -root = "LaurelDocMain" +name = "laureldesign" +root = "LaurelDesignGuideMain" + +[[lean_lib]] +name = "LaurelImplementationGuide" + +[[lean_exe]] +name = "laurelimpl" +root = "LaurelImplementationGuideMain" + +[[lean_lib]] +name = "LaurelUserGuide" + +[[lean_exe]] +name = "laurelguide" +root = "LaurelUserGuideMain" [[lean_lib]] name = "TransformsDoc" From 8a3901de929afba5c54dbba02e38f322d5fd3199 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Tue, 7 Jul 2026 12:19:17 +0000 Subject: [PATCH 02/20] User guide updates --- docs/verso/LaurelDesignGuide.lean | 887 ++--------------- docs/verso/LaurelDesignGuideMain.lean | 5 +- docs/verso/LaurelImplementationGuideMain.lean | 5 +- docs/verso/LaurelUserGuide.lean | 889 +++++++++++++++++- docs/verso/LaurelUserGuideMain.lean | 6 +- docs/verso/Makefile | 21 + docs/verso/generate.sh | 6 +- docs/verso/index.html | 6 +- 8 files changed, 943 insertions(+), 882 deletions(-) diff --git a/docs/verso/LaurelDesignGuide.lean b/docs/verso/LaurelDesignGuide.lean index ba8dfcf384..49fdbfaab2 100644 --- a/docs/verso/LaurelDesignGuide.lean +++ b/docs/verso/LaurelDesignGuide.lean @@ -22,869 +22,112 @@ open Verso.Genre Manual -- environment as Verso open Verso.Genre.Manual.InlineLean -set_option pp.rawOnError true - --- panel with an "Example" header, so concrete examples stand out from the --- surrounding explanatory prose. Authored via the `:::example` directive below. -block_extension Block.«example» (title : Option String) where - data := Lean.toJson (title : Option String) - traverse _ _ _ := pure none - toHtml := some fun _goI goB _id data contents => open Verso.Output.Html in do - let title : Option String := - match Lean.fromJson? (α := Option String) data with - | .ok t => t - | .error _ => none - let label := title.getD "Example" - pure {{ -
-
{{ label }}
-
{{← contents.mapM goB}}
-
- }} - extraCss := [ -r#" -.laurel-example { - border: 1px solid #98B2C0; - border-left: 4px solid #4A90E2; - border-radius: 0.4rem; - background: #F5F9FF; - margin-top: var(--verso--box-vertical-margin); - margin-bottom: var(--verso--box-vertical-margin); - overflow: hidden; -} -.laurel-example-header { - font-family: var(--verso-structure-font-family); - font-style: italic; - font-size: 0.875rem; - font-weight: bold; - color: #2A5680; - background: #E4EEF8; - padding: 0.3rem var(--verso--box-padding); -} -.laurel-example-body { - padding: 0.2rem var(--verso--box-padding); -} -"# - ] - toTeX := some fun _goI goB _id _data contents => open Verso.Output.TeX in open Verso.Doc.TeX in do - pure <| .seq <| ← contents.mapM fun b => do - pure <| .seq #[← goB b, .raw "\n"] - -/-- Configuration for the `:::example` directive: an optional title shown in the - box header (defaults to "Example"). -/ -structure LaurelExampleConfig where - title : Option String := none - -open Verso.ArgParse in -instance : Verso.ArgParse.FromArgs LaurelExampleConfig Verso.Doc.Elab.DocElabM where - fromArgs := LaurelExampleConfig.mk <$> - ((positional' `title <&> some) <|> pure none) - -/-- Sets its contents apart in a styled *example* box (see `Block.example`). - Optionally takes a title: `:::example "Arithmetic join"` … `:::`. -/ -@[directive] -def «example» : Verso.Doc.Elab.DirectiveExpanderOf LaurelExampleConfig - | {title}, stxs => do - let args ← stxs.mapM Verso.Doc.Elab.elabBlock - ``(Verso.Doc.Block.other (Block.«example» $(Lean.quote title)) #[ $[ $args ],* ]) + #doc (Manual) "The Laurel Language Design Guide" => %%% shortTitle := "Laurel Design" %%% -# Introduction +# Design Goals + +This guide describes the goals that Laurel is designed with, and the history of the decisions made to get to the language as it is now. When evolving the language, this document must be updated to advocate for the changes. Laurel is an intermediate verification language designed to serve as a target for popular garbage-collected languages that include imperative features, such as Java, Python, and JavaScript, where those languages have been extended to include verification specific constructs. Laurel tries to include any features that are common to those three languages. -This manual follows the language from the ground up: it first describes Laurel's -types, then its unified expression/statement model, then procedures and whole -programs. It then turns to type checking, done in a bidirectional way, and finally to the translation -pipeline that lowers a checked Laurel program to Strata Core. - -## Features - -In the feature lists below, items marked *(WIP)* are designed or planned but not -yet fully implemented; everything else is available today. - -Laurel enables doing various forms of analyses : -- Type checking -- Testing -- (WIP) Property-based testing -- (WIP) Bounded symbolic execution -- Unbounded symbolic execution -- (WIP) Data-flow analysis - -## Shared language features - -Here are some Laurel language features that are shared between the source languages: -- Statements such as loops and return statements -- Mutation of variables, including in expressions -- Reading and writing of fields of references -- Object oriented concepts such as inheritance, type checking, up and down casting and - dynamic dispatch -- (WIP) Error handling via exceptions -- (WIP) Procedures types and procedures as values -- (WIP) Parametric polymorphism - -Laurel does not distinguish between statements and expressions. -Expression-like or statement-like constructs can occur in the same positions. -Each statement-expression has a type, which for statement-like constructs might be void. - -## Verification features -On top of the above features, Laurel adds features that are useful specifically for verification: -- Assert and assume statements -- Loop invariants -- Pre and postconditions for procedures -- Modifies and reads clauses for procedures -- (WIP) Decreases clauses for procedures and loops -- (WIP) Immutable fields and constructors that support assigning to them -- (WIP) Constrained types -- (WIP) Type invariants -- Forall and exists expressions -- (WIP) Old and fresh expressions -- Unbounded integer and real types -- To be designed constructs for supporting proof writing - -## Verification design choices -A peculiar choice of Laurel is that it does not require imperative code to be encapsulated -using a functional specification. A reason for this is that sometimes the imperative code is -as readable as the functional specification. For example: -``` -procedure increment(counter: Counter) - // In Laurel, this ensures clause can be left out - ensures counter.value == old(counter.value) + 1 -{ - counter.value := counter.value + 1; -}; -``` - -## Internal constructors and properties -Some constructors and properties in the Laurel AST are marked for internal usage and should not be needed by Laurel users. -Having these internal properties and constructors allows us to define an incremental translation to Core which improves maintainability. - -# Types - -Laurel's types come in two groups: those a user can write — primitives, -collections, and user-defined types — and a few internal constructors the -implementation introduces that have no surface syntax. - -The {name Strata.Laurel.HighType}`HighType` type enumerates every type Laurel -tracks. Alongside the user-writable types it also includes internal constructors -(such as `Unknown` and `MultiValuedExpr`) that the compiler introduces -during resolution and later passes; these have no surface syntax. - -{docstring Strata.Laurel.HighType} +Goals: +1. Enable proving both correctness and incorrectness properties of software, through a combination of: + 1. property based testing + 2. data-flow analysis + 3. symbolic execution (aka verification), both bounded and unbounded +2. Reduce code duplication in the analysis of popular languages by being a target for compilation from those languages, and including features common to them. Note that we expect source languages to reduce their existing compilers when possible, so language features that can be compiled away don't need to be considered. +3. Minimize the amount of user code needed to enable verification. +4. Enable modular verification +5. Use complete analysis algorithms to reduce the required proof effort. +6. Enable finding proofs through an automated search. +7. Code used to enable verification may not affect execution behavior. -## User-Defined Types +# Reduce duplication between source languages +To achieve goal (2), reduce code duplication in the analysis of popular languages, Laurel contains many features shared between several languages. The following table shows which features are shared with whch input languages. -User-defined types come in two categories: composite types and constrained types. +TODO, add a table with Laurel features as rows, and a list of languages in columns (Java, Kotlin, C#, JavaScript, Python, GoLang). Split up language feature whenever relevant for the columns. -Composite types have fields and procedures, and may extend other composite types. Fields -declare whether they are mutable and specify their type. +These features should be in rows but marked as WIP: +- Try/catch and checked exception +- Procedures types and procedures as values +- Parametric polymorphism -{docstring Strata.Laurel.CompositeType} +# Enable Verification +To achieve goal 1.3, enable proving properties through verification, Laurel has the following features. +- Assertions +- Quantifiers +- Old/allocated/fresh +- Decreases clauses +- Loop invariants (more about automated proof) +- Assumptions (more about gradual verification) -{docstring Strata.Laurel.Field} +# Modular Verification +The achieve goal (4), Laurel has the following features related to modular verification. -Constrained types are defined by a base type and a constraint over the values of the base -type. Algebraic datatypes can be encoded using composite and constrained types. +## Preconditions +Preconditions enable proving the assertions in a procedure's body without having to consider the callers. This way, each assertion only needs to be proven once, instead of once for each transitive call-site. -{docstring Strata.Laurel.ConstrainedType} +## Encapsulation +Postconditions enable encapsulating the behavior of a procedure through a simpler condition. This simplifies reasoning at the call-site. -{docstring Strata.Laurel.TypeDefinition} +Since procedure can mutate references as well, once we add encapsulation through postconditions, we also need modifies clauses to enable encapsulating reference modifying procedures. -# Expressions and Statements +Reads clauses are useful to improve verification performance. The facts they prove work well together with the facts provided by modified clauses, making it easier to prove which procedure values have remained unchanged after objects were modified. -Laurel uses a unified `StmtExpr` type that contains both expression-like and statement-like -constructs. This avoids duplication of shared concepts such as conditionals and variable -declarations. +## Reduce verification through complete analysis +To achieve goal 5, Laurel has the following features. -## Operations +## Constrained types +Constrained types propagating facts through the type system. -{docstring Strata.Laurel.Operation} +TODO, add example using polymorphic types -## The StmtExpr Type +## Implicit conversions -{docstring Strata.Laurel.StmtExpr} +To be designed.. -## Metadata -All AST nodes can carry metadata via the `AstNode` wrapper. +# Minimize Verification Code +To achieve goal (3), minimize the amount of user code needed to enable verification, Laurel has the following features: -{docstring Strata.Laurel.AstNode} +## Transparent procedures +Laurel procedures are transparent by default, meaning that a call can use the body of the callee to prove facts about the result of the call. Laurel will allow any procedure to be transparent, although currently there are some restrictions. In particular, Laurel will allow procedures that contains loops or that modify the heap, to be transparent as well. -# Procedures - -Procedures are the main unit of specification and verification in Laurel. - -{docstring Strata.Laurel.Procedure} - -{docstring Strata.Laurel.Parameter} - -{docstring Strata.Laurel.Body} - -# Programs - -A Laurel program consists of procedures, global variables, type definitions, and constants. - -{docstring Strata.Laurel.Program} - -# Type checking - -Type checking is woven into the resolution pass: every -{name Strata.Laurel.StmtExpr}`StmtExpr` gets a {name Strata.Laurel.HighType}`HighType`, and -mismatches against the surrounding context become diagnostics. The implementation is in -`Resolution.lean`. - -## Design - -### Bidirectional type checking - -There are two operations on expressions, written here in standard -bidirectional notation: +By allowing any procedure to be transparent, Laurel prevents users from having to repeat the body of a procedure in a postcondition. Here's an example that shows an opaque procedure that would have been easier to define as being transparent, without any loss of readability: ``` -Γ ⊢ e ⇒ A -- "e synthesizes A" (Synth.resolveStmtExpr) -Γ ⊢ e ⇐ A -- "e checks against A" (Check.resolveStmtExpr) +procedure increment(counter: Counter) opaque + // In Laurel, this ensures clause can be left out + ensures counter.value == old(counter.value) + 1 +{ + counter.value := counter.value + 1 +}; ``` -Synthesis returns a type inferred from the expression itself; checking -verifies that the expression has a given expected type. Each construct -picks a mode based on whether its type is determined locally (synth) or -by context (check). The two judgments are connected by a single -change-of-direction rule, *subsumption*: - -$$`\frac{\Gamma \vdash e \Rightarrow A \quad A <: B}{\Gamma \vdash e \Leftarrow B} \quad \text{([⇐] Sub)}` - -The two judgments are implemented as -{name Strata.Laurel.Resolution.Synth.resolveStmtExpr}`Synth.resolveStmtExpr` and -{name Strata.Laurel.Resolution.Check.resolveStmtExpr}`Check.resolveStmtExpr`: - -{docstring Strata.Laurel.Resolution.Synth.resolveStmtExpr} - -{docstring Strata.Laurel.Resolution.Check.resolveStmtExpr} - -### Gradual typing - -The relation `<:` (used in \[⇐\] Sub) is built from three Lean functions — -{name Strata.Laurel.isSubtype}`isSubtype`, {name Strata.Laurel.isConsistent}`isConsistent`, -and {name Strata.Laurel.isConsistentSubtype}`isConsistentSubtype`: - -{docstring Strata.Laurel.isSubtype} - -{docstring Strata.Laurel.isConsistent} - -{docstring Strata.Laurel.isConsistentSubtype} - -## Typing rules - -Each construct is given as a derivation. `Γ` is the current lexical scope (see -{name Strata.Laurel.ResolveState}`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 {ref "rules-procedure"}[*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 ({name Strata.Laurel.isSubtype}`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 $`<:_\sim` below — the implementation routes every such check - through {name Strata.Laurel.isConsistentSubtype}`isConsistentSubtype`, never - bare $`<:` — so $`\mathsf{Unknown}` is admitted on either side. -- $`A \sim B` — the *consistency* relation - {name Strata.Laurel.isConsistent}`isConsistent`: symmetric, with - $`\mathsf{Unknown}` acting as a wildcard. -- $`A <:_\sim B` — the *consistent-subtype* relation - {name Strata.Laurel.isConsistentSubtype}`isConsistentSubtype`, the gradual - combination of the two above. -- $`\mathsf{Numeric}\;T` — a predicate holding when $`T` is consistent with one - of $`\mathsf{TInt}`, $`\mathsf{TReal}`, $`\mathsf{TFloat64}`, or - $`\mathsf{TBv}_w` (a bitvector of any width $`w`), with $`\mathsf{Unknown}` - admitted as the gradual escape hatch. -- $`\dashv \Gamma'` — a rule's *output scope*: the judgment threads $`\Gamma` in - and produces $`\Gamma'` out. Only \[⇐\] Var-Declare extends the scope; the - block rules thread it statement-to-statement (the $`\Gamma_{i-1} \to - \Gamma_i` chain 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. - -### Index - -- {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-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 -- {ref "rules-assignment"}[*Assignment*] — \[⇒\] Assign, \[⇐\] Assign -- {ref "rules-calls"}[*Calls*] — \[⇒\] Static-Call, \[⇒\] Static-Call-Multi, - \[⇒\] Instance-Call, \[⇒\] Instance-Call-Multi -- {ref "rules-primitive-operations"}[*Primitive operations*] — \[⇒\] Op-Bool, \[⇒\] Op-Cmp, \[⇒\] Op-Eq, - \[⇒\] Op-Arith, \[⇒\] Op-Concat; \[⇐\] Op-Arith, \[⇐\] Op-Bool -- {ref "rules-object-forms"}[*Object forms*] — \[⇒\] New-Ok, \[⇒\] New-Fallback; \[⇒\] AsType; \[⇒\] IsType; - \[⇒\] RefEq; \[⇒\] PureFieldUpdate -- {ref "rules-verification-expressions"}[*Verification expressions*] — \[⇒\] Quantifier, \[⇒\] Assigned, \[⇐\] Old, - \[⇒\] Old-Synth, \[⇒\] Fresh, \[⇐\] ProveBy, \[⇒\] ProveBy-Synth -- {ref "rules-self-reference"}[*Self reference*] — \[⇒\] This-Inside, \[⇒\] This-Outside -- {ref "rules-untyped-forms"}[*Untyped forms*] — \[⇒\] Abstract / All -- {ref "rules-contract-of"}[*ContractOf*] — \[⇒\] ContractOf-Bool, \[⇒\] ContractOf-Set, \[⇒\] ContractOf-Error -- {ref "rules-holes"}[*Holes*] — \[⇐\] Hole-Some, \[⇐\] Hole-None, \[⇒\] Hole-Synth-None, \[⇒\] Hole-Synth-Some -- {ref "rules-procedure"}[*Procedure*] — Procedure - -### Subsumption -%%% -tag := "rules-subsumption" -%%% - -$$`\frac{\Gamma \vdash e \Rightarrow A \quad A <: B}{\Gamma \vdash e \Leftarrow B} \quad \text{([⇐] Sub)}` - -Fallback in {name Strata.Laurel.Resolution.Check.resolveStmtExpr}`Check.resolveStmtExpr` whenever no bespoke check -rule applies. - -### Literals -%%% -tag := "rules-literals" -%%% - -$$`\frac{}{\Gamma \vdash \mathsf{LiteralInt}\;n \Rightarrow \mathsf{TInt}} \quad \text{([⇒] Lit-Int)}` - -{docstring Strata.Laurel.Resolution.Synth.litInt} - -$$`\frac{}{\Gamma \vdash \mathsf{LiteralBool}\;b \Rightarrow \mathsf{TBool}} \quad \text{([⇒] Lit-Bool)}` - -{docstring Strata.Laurel.Resolution.Synth.litBool} - -$$`\frac{}{\Gamma \vdash \mathsf{LiteralString}\;s \Rightarrow \mathsf{TString}} \quad \text{([⇒] Lit-String)}` - -{docstring Strata.Laurel.Resolution.Synth.litString} - -$$`\frac{}{\Gamma \vdash \mathsf{LiteralDecimal}\;d \Rightarrow \mathsf{TReal}} \quad \text{([⇒] Lit-Decimal)}` - -{docstring Strata.Laurel.Resolution.Synth.litDecimal} - -### Variables -%%% -tag := "rules-variables" -%%% - -$$`\frac{\Gamma(x) = T}{\Gamma \vdash \mathsf{Var}\;(\mathsf{.Local}\;x) \Rightarrow T} \quad \text{([⇒] Var-Local)}` - -{docstring Strata.Laurel.Resolution.Synth.varLocal} - -$$`\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)}` - -{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)}` - -$`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. - -{docstring Strata.Laurel.Resolution.Check.varDeclare} - -### Control flow -%%% -tag := "rules-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)}` - -{docstring Strata.Laurel.Resolution.Check.ifThenElse} - -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}`. - -:::example "`if` in operand position" -- `(if c then 1 else 2) == y` — both branches $`\mathsf{TInt}`, so the `if` synthesizes $`\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` (no `else`) — 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)}` - -{docstring Strata.Laurel.Resolution.Synth.ifThenElse} - -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 `Var (.Declare …)` actually extends the scope $`\Gamma_i`; 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 ''"` 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}`). - -{docstring Strata.Laurel.Resolution.Synth.emptyBlock} - -{docstring Strata.Laurel.Resolution.Synth.block} - -{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 -{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)}` - -`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. - -{docstring Strata.Laurel.Resolution.Check.exit} - -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. - -{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)}` - -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. - -{docstring Strata.Laurel.Resolution.Check.while} - -### Verification statements -%%% -tag := "rules-verification-statements" -%%% - -$$`\frac{\Gamma \vdash \mathit{cond} \Leftarrow \mathsf{TBool}}{\Gamma \vdash \mathsf{Assert}\;\mathit{cond} \Rightarrow \mathsf{TVoid}} \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)}` - -{docstring Strata.Laurel.Resolution.Check.assume} - -### Assignment -%%% -tag := "rules-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 -{name Strata.Laurel.Variable.Local}`Local` and {name Strata.Laurel.Variable.Field}`Field`) -or from the {name Strata.Laurel.Variable.Declare}`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. - -{docstring Strata.Laurel.Resolution.Synth.assign} - -$$`\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. - -{docstring Strata.Laurel.Resolution.Check.assign} - -### Calls -%%% -tag := "rules-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)}` - -{docstring Strata.Laurel.Resolution.Synth.staticCall} - -$$`\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 -{name Strata.Laurel.Resolution.Synth.staticCall}`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}`. - -{docstring Strata.Laurel.Resolution.Synth.instanceCall} - -### Primitive operations -%%% -tag := "rules-primitive-operations" -%%% - -`Numeric` abbreviates "consistent with one of {name Strata.Laurel.HighType.TInt}`TInt`, -{name Strata.Laurel.HighType.TReal}`TReal`, -{name Strata.Laurel.HighType.TFloat64}`TFloat64`, or -{name Strata.Laurel.HighType.TBv}`TBv` (a bitvector of any width)", with -`Unknown` admitted as the gradual escape hatch. - -$$`\frac{\Gamma \vdash \mathit{args}_i \Rightarrow U_i \quad U_i <: \mathsf{TBool} \quad \mathit{op} \in \{\mathsf{And}, \mathsf{Or}, \mathsf{AndThen}, \mathsf{OrElse}, \mathsf{Not}, \mathsf{Implies}\}}{\Gamma \vdash \mathsf{PrimitiveOp}\;\mathit{op}\;\mathit{args} \Rightarrow \mathsf{TBool}} \quad \text{([⇒] Op-Bool)}` - -$$`\frac{\Gamma \vdash \mathit{args}_i \Rightarrow U_i \quad \mathsf{Numeric}\;U_i \quad \mathit{op} \in \{\mathsf{Lt}, \mathsf{Leq}, \mathsf{Gt}, \mathsf{Geq}\}}{\Gamma \vdash \mathsf{PrimitiveOp}\;\mathit{op}\;\mathit{args} \Rightarrow \mathsf{TBool}} \quad \text{([⇒] Op-Cmp)}` - -$$`\frac{\Gamma \vdash \mathit{lhs} \Rightarrow T_l \quad \Gamma \vdash \mathit{rhs} \Rightarrow T_r \quad T_l \sim T_r \quad \mathit{op} \in \{\mathsf{Eq}, \mathsf{Neq}\}}{\Gamma \vdash \mathsf{PrimitiveOp}\;\mathit{op}\;[\mathit{lhs}; \mathit{rhs}] \Rightarrow \mathsf{TBool}} \quad \text{([⇒] Op-Eq)}` - -$$`\frac{\Gamma \vdash \mathit{args}_i \Rightarrow U_i \quad \mathsf{Numeric}\;U_i \quad T = \bigsqcup_i U_i \text{ (consistency join)} \quad \mathit{op} \in \{\mathsf{Neg}, \mathsf{Add}, \mathsf{Sub}, \mathsf{Mul}, \mathsf{Div}, \mathsf{Mod}, \mathsf{DivT}, \mathsf{ModT}\}}{\Gamma \vdash \mathsf{PrimitiveOp}\;\mathit{op}\;\mathit{args} \Rightarrow T} \quad \text{([⇒] Op-Arith)}` - -The arithmetic synth rule mirrors $`[⇒]\,\text{Op-Eq}` but generalised -to $`n` operands. Each operand is synthesized and required to be -$`\mathsf{Numeric}` (i.e. $`\mathsf{TInt}`, $`\mathsf{TReal}`, -$`\mathsf{TFloat64}`, $`\mathsf{TBv}_w` (a bitvector of any width), or -the gradual $`\mathsf{Unknown}`). The -result type is the *consistency join* $`\bigsqcup_i U_i` — a fold of -the operand types under -{name Strata.Laurel.isConsistent}`isConsistent`'s flat lattice: -$`\mathsf{Unknown} \sqcup T = T`, $`T \sqcup T = T`, and any other -combination is rejected. The fold runs via `join`, a pure function, so -the search has no diagnostic side-effects. - -:::example "Arithmetic operand join" -- `1 + 2` synthesizes $`\mathsf{TInt}` -- `1.5 + 2.5` synthesizes $`\mathsf{TReal}` -- ` + 1` synthesizes $`\mathsf{TInt}` — the $`\mathsf{Unknown}` operand promotes to its neighbour -- ` + ` synthesizes $`\mathsf{Unknown}` -- `1 + 2.0` is rejected: *cannot apply '+' to operands of types 'int', 'real'* -::: - -$$`\frac{\Gamma \vdash \mathit{args}_i \Rightarrow U_i \quad U_i <: \mathsf{TString} \quad \mathit{op} = \mathsf{StrConcat}}{\Gamma \vdash \mathsf{PrimitiveOp}\;\mathit{op}\;\mathit{args} \Rightarrow \mathsf{TString}} \quad \text{([⇒] Op-Concat)}` - -{docstring Strata.Laurel.Resolution.Synth.primitiveOp} - -The arithmetic and boolean families also have a check-mode rule, used -when the surrounding context provides an `expected` type. The rule -pushes the operand type into each operand via -`Check.resolveStmtExpr`, replacing the synth-then-`checkSubtype` -discipline with bidirectional check. - -$$`\frac{\mathsf{Numeric}\;T \quad \Gamma \vdash \mathit{args}_i \Leftarrow T \quad \mathit{op} \in \{\mathsf{Neg}, \mathsf{Add}, \mathsf{Sub}, \mathsf{Mul}, \mathsf{Div}, \mathsf{Mod}, \mathsf{DivT}, \mathsf{ModT}\}}{\Gamma \vdash \mathsf{PrimitiveOp}\;\mathit{op}\;\mathit{args} \Leftarrow T} \quad \text{([⇐] Op-Arith)}` - -$$`\frac{\mathsf{TBool} <: T \quad \Gamma \vdash \mathit{args}_i \Leftarrow \mathsf{TBool} \quad \mathit{op} \in \{\mathsf{And}, \mathsf{Or}, \mathsf{AndThen}, \mathsf{OrElse}, \mathsf{Not}, \mathsf{Implies}\}}{\Gamma \vdash \mathsf{PrimitiveOp}\;\mathit{op}\;\mathit{args} \Leftarrow T} \quad \text{([⇐] Op-Bool)}` - -{docstring Strata.Laurel.Resolution.Check.primitiveOp} - -### Object forms -%%% -tag := "rules-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. - -{docstring Strata.Laurel.Resolution.Synth.new} - -$$`\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)}` - -{docstring Strata.Laurel.Resolution.Synth.asType} - -$$`\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)}` - -{docstring Strata.Laurel.Resolution.Synth.isType} - -$$`\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 {name Strata.Laurel.HighType.UserDefined}`UserDefined` -or {name Strata.Laurel.HighType.Unknown}`Unknown` type. `~` is the consistency relation -{name Strata.Laurel.isConsistent}`isConsistent` — symmetric, with the -{name Strata.Laurel.HighType.Unknown}`Unknown` wildcard. - -{docstring Strata.Laurel.Resolution.Synth.refEq} - -$$`\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)}` - -{docstring Strata.Laurel.Resolution.Synth.pureFieldUpdate} - -### Verification expressions -%%% -tag := "rules-verification-expressions" -%%% +## Heap mutation in contracts +A contract in Laurel may not modify any object that exists outside of that contract, as if the contract has an empty modifies clause. However, new objects may be created and modified inside the contract. -$$`\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)}` +A common design choice in verification aware programming language is not to allow creating or modifying objects in contracts. A good reason for this is that objects are more complex to reason about than immutable data, and contracts are intended to contain easy to reason about code. Laurel still allows this because code might be declared to operate specifically through the use of reference types, and Laurel does not want to restrict users from using such code even in contracts. -{docstring Strata.Laurel.Resolution.Synth.quantifier} +A second reason for not allowing any heap modification inside contracts is that this is prone to soundness issues. From outside the contract the heap is assumed not to be modified, so if knowledge of an inside modification escapes the contract, this leads to an inconsistency. Because Laurel does not allow assigning to variable defined outside the contract, from inside the contract, no modification can escape the contract. The heap used inside a contract is a separate heap variable. -$$`\frac{\Gamma \vdash \mathit{name} \Rightarrow \_}{\Gamma \vdash \mathsf{Assigned}\;\mathit{name} \Rightarrow \mathsf{TBool}} \quad \text{([⇒] Assigned)}` +## Invoke on -{docstring Strata.Laurel.Resolution.Synth.assigned} - -$$`\frac{\Gamma \vdash v \Leftarrow T}{\Gamma \vdash \mathsf{Old}\;v \Leftarrow T} \quad \text{([⇐] Old)}` - -{docstring Strata.Laurel.Resolution.Check.old} - -`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)}` - -{docstring Strata.Laurel.Resolution.Synth.old} - -$$`\frac{\Gamma \vdash v \Rightarrow T \quad \mathsf{isReference}\;T}{\Gamma \vdash \mathsf{Fresh}\;v \Rightarrow \mathsf{TBool}} \quad \text{([⇒] Fresh)}` - -{docstring Strata.Laurel.Resolution.Synth.fresh} - -$$`\frac{\Gamma \vdash v \Leftarrow T \quad \Gamma \vdash \mathit{proof} \Rightarrow \_}{\Gamma \vdash \mathsf{ProveBy}\;v\;\mathit{proof} \Leftarrow T} \quad \text{([⇐] ProveBy)}` - -{docstring Strata.Laurel.Resolution.Check.proveBy} - -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)}` - -{docstring Strata.Laurel.Resolution.Synth.proveBy} - -### Self reference -%%% -tag := "rules-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)}` - -{docstring Strata.Laurel.Resolution.Synth.this} - -### Untyped forms -%%% -tag := "rules-untyped-forms" -%%% - -$$`\frac{}{\Gamma \vdash \mathsf{Abstract}\,/\,\mathsf{All}\;\ldots \Rightarrow \mathsf{Unknown}} \quad \text{([⇒] Abstract / All)}` - -{docstring Strata.Laurel.Resolution.Synth.abstract} - -{docstring Strata.Laurel.Resolution.Synth.all} - -### ContractOf -%%% -tag := "rules-contract-of" -%%% - -$$`\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). - -{docstring Strata.Laurel.Resolution.Synth.contractOf} - -### Holes -%%% -tag := "rules-holes" -%%% - -$$`\frac{T_h <: T}{\Gamma \vdash \mathsf{Hole}\;d\;(\mathsf{some}\;T_h) \Leftarrow T} \quad \text{([⇐] Hole-Some)}` - -{docstring Strata.Laurel.Resolution.Check.holeSome} - -$$`\frac{}{\Gamma \vdash \mathsf{Hole}\;d\;\mathsf{none} \Leftarrow T \quad \mapsto \quad \mathsf{Hole}\;d\;(\mathsf{some}\;T)} \quad \text{([⇐] Hole-None)}` - -{docstring Strata.Laurel.Resolution.Check.holeNone} - -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)}` - -### Procedure -%%% -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. - -$$`\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 -{name Strata.Laurel.Resolution.Check.return}`Check.return`) or via -named-output assignment. - -{docstring Strata.Laurel.resolveProcedure} - -{docstring Strata.Laurel.resolveInstanceProcedure} +TODO, fill in +# Naming choices # Differences between Laurel and Core -## Language design - -### Parameter lists +## Parameter lists Parameter lists. In Laurel, input and output parameters are defined in a separate list. Inout parameters are defined by repeating the parameter name in both lists. In Core, there is a single parameter list where each parameter defines its kind (in/out/inout). At the call-site, Laurel requires calls with multiple out parameters to occur inside an assignment, like this: @@ -894,7 +137,7 @@ Core uses the argument list to assign the output parameters, like this: In Laurel, an inout parameter only influences the callee's code, since it means there is a single variable that is used as input and output. On the calling side however, there is no concept of inout parameters. This is different from Core, where inout variables affect the calling side. Example of an inout being called in Core, `hasInout(inout x)`. -### Assignments to fresh and existing declarations +## Assignments to fresh and existing declarations In Laurel, assignments can have multiple targets. Each target can be either an existing variable or a local declaration. Example: ``` var x: int; diff --git a/docs/verso/LaurelDesignGuideMain.lean b/docs/verso/LaurelDesignGuideMain.lean index 3aa10eee02..62a26e29eb 100644 --- a/docs/verso/LaurelDesignGuideMain.lean +++ b/docs/verso/LaurelDesignGuideMain.lean @@ -11,8 +11,9 @@ open Verso.Genre.Manual (RenderConfig manualMain) def config : RenderConfig where emitTeX := false - emitHtmlSingle := .immediately - emitHtmlMulti := .no + -- Multi-page output so the sidebar navigation is nested. + emitHtmlSingle := .no + emitHtmlMulti := .immediately htmlDepth := 2 def main := manualMain (%doc LaurelDesignGuide) (config := config) diff --git a/docs/verso/LaurelImplementationGuideMain.lean b/docs/verso/LaurelImplementationGuideMain.lean index e2b49f340d..a06f2db3e5 100644 --- a/docs/verso/LaurelImplementationGuideMain.lean +++ b/docs/verso/LaurelImplementationGuideMain.lean @@ -11,8 +11,9 @@ open Verso.Genre.Manual (RenderConfig manualMain) def config : RenderConfig where emitTeX := false - emitHtmlSingle := .immediately - emitHtmlMulti := .no + -- Multi-page output so the sidebar navigation is nested. + emitHtmlSingle := .no + emitHtmlMulti := .immediately htmlDepth := 2 def main := manualMain (%doc LaurelImplementationGuide) (config := config) diff --git a/docs/verso/LaurelUserGuide.lean b/docs/verso/LaurelUserGuide.lean index 49777d0064..5ebc09d00a 100644 --- a/docs/verso/LaurelUserGuide.lean +++ b/docs/verso/LaurelUserGuide.lean @@ -6,6 +6,13 @@ import VersoManual +import Strata.Languages.Laurel.LaurelAST +import Strata.Languages.Laurel.LaurelTypes +import Strata.Languages.Laurel.LaurelCompilationPipeline +import Strata.Languages.Laurel.HeapParameterization +import Strata.Languages.Laurel.LiftImperativeExpressions +import Strata.Languages.Laurel.ModifiesClauses + -- This gets access to most of the manual genre open Verso.Genre Manual @@ -13,6 +20,72 @@ open Verso.Genre Manual -- the same process and environment as Verso open Verso.Genre.Manual.InlineLean +set_option pp.rawOnError true + +-- panel with an "Example" header, so concrete examples stand out from the +-- surrounding explanatory prose. Authored via the `:::example` directive below. +block_extension Block.«example» (title : Option String) where + data := Lean.toJson (title : Option String) + traverse _ _ _ := pure none + toHtml := some fun _goI goB _id data contents => open Verso.Output.Html in do + let title : Option String := + match Lean.fromJson? (α := Option String) data with + | .ok t => t + | .error _ => none + let label := title.getD "Example" + pure {{ +
+
{{ label }}
+
{{← contents.mapM goB}}
+
+ }} + extraCss := [ +r#" +.laurel-example { + border: 1px solid #98B2C0; + border-left: 4px solid #4A90E2; + border-radius: 0.4rem; + background: #F5F9FF; + margin-top: var(--verso--box-vertical-margin); + margin-bottom: var(--verso--box-vertical-margin); + overflow: hidden; +} +.laurel-example-header { + font-family: var(--verso-structure-font-family); + font-style: italic; + font-size: 0.875rem; + font-weight: bold; + color: #2A5680; + background: #E4EEF8; + padding: 0.3rem var(--verso--box-padding); +} +.laurel-example-body { + padding: 0.2rem var(--verso--box-padding); +} +"# + ] + toTeX := some fun _goI goB _id _data contents => open Verso.Output.TeX in open Verso.Doc.TeX in do + pure <| .seq <| ← contents.mapM fun b => do + pure <| .seq #[← goB b, .raw "\n"] + +/-- Configuration for the `:::example` directive: an optional title shown in the + box header (defaults to "Example"). -/ +structure LaurelExampleConfig where + title : Option String := none + +open Verso.ArgParse in +instance : Verso.ArgParse.FromArgs LaurelExampleConfig Verso.Doc.Elab.DocElabM where + fromArgs := LaurelExampleConfig.mk <$> + ((positional' `title <&> some) <|> pure none) + +/-- Sets its contents apart in a styled *example* box (see `Block.example`). + Optionally takes a title: `:::example "Arithmetic join"` … `:::`. -/ +@[directive] +def «example» : Verso.Doc.Elab.DirectiveExpanderOf LaurelExampleConfig + | {title}, stxs => do + let args ← stxs.mapM Verso.Doc.Elab.elabBlock + ``(Verso.Doc.Block.other (Block.«example» $(Lean.quote title)) #[ $[ $args ],* ]) + #doc (Manual) "The Laurel User Guide" => %%% shortTitle := "Laurel User Guide" @@ -20,6 +93,8 @@ shortTitle := "Laurel User Guide" # Summary +TODO: generalize this section since it's too verification focussed. + Laurel is an intermediate verification language. It is the common target for verifiers built on top of garbage-collected, imperative source languages such as Java, Python, and JavaScript. You usually do not write Laurel by hand; @@ -59,16 +134,721 @@ procedure addOne(x: int) returns (r: int) }; ``` -The `opaque` keyword marks a procedure whose body is hidden from its callers: -callers reason about it only through its contract (`requires` / `ensures` / -`modifies`). This is the standard *modular* style — each procedure is verified -once against its contract, and call sites trust the contract rather than the -body. +## Internal constructors and properties +Some constructors and properties in the Laurel AST are marked for internal usage and should not be needed by Laurel users. +Having these internal properties and constructors allows us to define an incremental translation to Core which improves maintainability. + +# Resolution + + +## Bidirectional type checking + +There are two operations on expressions, written here in standard +bidirectional notation: + +``` +Γ ⊢ e ⇒ A -- "e synthesizes A" (Synth.resolveStmtExpr) +Γ ⊢ e ⇐ A -- "e checks against A" (Check.resolveStmtExpr) +``` + +Synthesis returns a type inferred from the expression itself; checking +verifies that the expression has a given expected type. Each construct +picks a mode based on whether its type is determined locally (synth) or +by context (check). The two judgments are connected by a single +change-of-direction rule, *subsumption*: + +$$`\frac{\Gamma \vdash e \Rightarrow A \quad A <: B}{\Gamma \vdash e \Leftarrow B} \quad \text{([⇐] Sub)}` + +The two judgments are implemented as +{name Strata.Laurel.Resolution.Synth.resolveStmtExpr}`Synth.resolveStmtExpr` and +{name Strata.Laurel.Resolution.Check.resolveStmtExpr}`Check.resolveStmtExpr`: + +{docstring Strata.Laurel.Resolution.Synth.resolveStmtExpr} + +{docstring Strata.Laurel.Resolution.Check.resolveStmtExpr} + +## Gradual typing + +The relation `<:` (used in \[⇐\] Sub) is built from three Lean functions — +{name Strata.Laurel.isSubtype}`isSubtype`, {name Strata.Laurel.isConsistent}`isConsistent`, +and {name Strata.Laurel.isConsistentSubtype}`isConsistentSubtype`: + +{docstring Strata.Laurel.isSubtype} + +{docstring Strata.Laurel.isConsistent} + +{docstring Strata.Laurel.isConsistentSubtype} + +## Typing rules + +Each construct is given as a derivation. `Γ` is the current lexical scope (see +{name Strata.Laurel.ResolveState}`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 {ref "rules-procedure"}[*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 ({name Strata.Laurel.isSubtype}`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 $`<:_\sim` below — the implementation routes every such check + through {name Strata.Laurel.isConsistentSubtype}`isConsistentSubtype`, never + bare $`<:` — so $`\mathsf{Unknown}` is admitted on either side. +- $`A \sim B` — the *consistency* relation + {name Strata.Laurel.isConsistent}`isConsistent`: symmetric, with + $`\mathsf{Unknown}` acting as a wildcard. +- $`A <:_\sim B` — the *consistent-subtype* relation + {name Strata.Laurel.isConsistentSubtype}`isConsistentSubtype`, the gradual + combination of the two above. +- $`\mathsf{Numeric}\;T` — a predicate holding when $`T` is consistent with one + of $`\mathsf{TInt}`, $`\mathsf{TReal}`, $`\mathsf{TFloat64}`, or + $`\mathsf{TBv}_w` (a bitvector of any width $`w`), with $`\mathsf{Unknown}` + admitted as the gradual escape hatch. +- $`\dashv \Gamma'` — a rule's *output scope*: the judgment threads $`\Gamma` in + and produces $`\Gamma'` out. Only \[⇐\] Var-Declare extends the scope; the + block rules thread it statement-to-statement (the $`\Gamma_{i-1} \to + \Gamma_i` chain 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. + +### Index + +- {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-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 +- {ref "rules-assignment"}[*Assignment*] — \[⇒\] Assign, \[⇐\] Assign +- {ref "rules-calls"}[*Calls*] — \[⇒\] Static-Call, \[⇒\] Static-Call-Multi, + \[⇒\] Instance-Call, \[⇒\] Instance-Call-Multi +- {ref "rules-primitive-operations"}[*Primitive operations*] — \[⇒\] Op-Bool, \[⇒\] Op-Cmp, \[⇒\] Op-Eq, + \[⇒\] Op-Arith, \[⇒\] Op-Concat; \[⇐\] Op-Arith, \[⇐\] Op-Bool +- {ref "rules-object-forms"}[*Object forms*] — \[⇒\] New-Ok, \[⇒\] New-Fallback; \[⇒\] AsType; \[⇒\] IsType; + \[⇒\] RefEq; \[⇒\] PureFieldUpdate +- {ref "rules-verification-expressions"}[*Verification expressions*] — \[⇒\] Quantifier, \[⇒\] Assigned, \[⇐\] Old, + \[⇒\] Old-Synth, \[⇒\] Fresh, \[⇐\] ProveBy, \[⇒\] ProveBy-Synth +- {ref "rules-self-reference"}[*Self reference*] — \[⇒\] This-Inside, \[⇒\] This-Outside +- {ref "rules-untyped-forms"}[*Untyped forms*] — \[⇒\] Abstract / All +- {ref "rules-contract-of"}[*ContractOf*] — \[⇒\] ContractOf-Bool, \[⇒\] ContractOf-Set, \[⇒\] ContractOf-Error +- {ref "rules-holes"}[*Holes*] — \[⇐\] Hole-Some, \[⇐\] Hole-None, \[⇒\] Hole-Synth-None, \[⇒\] Hole-Synth-Some +- {ref "rules-procedure"}[*Procedure*] — Procedure + +### Subsumption +%%% +tag := "rules-subsumption" +%%% + +$$`\frac{\Gamma \vdash e \Rightarrow A \quad A <: B}{\Gamma \vdash e \Leftarrow B} \quad \text{([⇐] Sub)}` + +Fallback in {name Strata.Laurel.Resolution.Check.resolveStmtExpr}`Check.resolveStmtExpr` whenever no bespoke check +rule applies. + +### Literals +%%% +tag := "rules-literals" +%%% + +$$`\frac{}{\Gamma \vdash \mathsf{LiteralInt}\;n \Rightarrow \mathsf{TInt}} \quad \text{([⇒] Lit-Int)}` + +{docstring Strata.Laurel.Resolution.Synth.litInt} + +$$`\frac{}{\Gamma \vdash \mathsf{LiteralBool}\;b \Rightarrow \mathsf{TBool}} \quad \text{([⇒] Lit-Bool)}` + +{docstring Strata.Laurel.Resolution.Synth.litBool} + +$$`\frac{}{\Gamma \vdash \mathsf{LiteralString}\;s \Rightarrow \mathsf{TString}} \quad \text{([⇒] Lit-String)}` + +{docstring Strata.Laurel.Resolution.Synth.litString} + +$$`\frac{}{\Gamma \vdash \mathsf{LiteralDecimal}\;d \Rightarrow \mathsf{TReal}} \quad \text{([⇒] Lit-Decimal)}` + +{docstring Strata.Laurel.Resolution.Synth.litDecimal} + +### Variables +%%% +tag := "rules-variables" +%%% + +$$`\frac{\Gamma(x) = T}{\Gamma \vdash \mathsf{Var}\;(\mathsf{.Local}\;x) \Rightarrow T} \quad \text{([⇒] Var-Local)}` + +{docstring Strata.Laurel.Resolution.Synth.varLocal} + +$$`\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)}` + +{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)}` + +$`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. + +{docstring Strata.Laurel.Resolution.Check.varDeclare} + +### Control flow +%%% +tag := "rules-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)}` + +{docstring Strata.Laurel.Resolution.Check.ifThenElse} + +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}`. + +:::example "`if` in operand position" +- `(if c then 1 else 2) == y` — both branches $`\mathsf{TInt}`, so the `if` synthesizes $`\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` (no `else`) — 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)}` + +{docstring Strata.Laurel.Resolution.Synth.ifThenElse} + +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 `Var (.Declare …)` actually extends the scope $`\Gamma_i`; 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 ''"` 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}`). + +{docstring Strata.Laurel.Resolution.Synth.emptyBlock} + +{docstring Strata.Laurel.Resolution.Synth.block} + +{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 +{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)}` + +`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. + +{docstring Strata.Laurel.Resolution.Check.exit} + +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. + +{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)}` + +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. + +{docstring Strata.Laurel.Resolution.Check.while} + +### Verification statements +%%% +tag := "rules-verification-statements" +%%% + +$$`\frac{\Gamma \vdash \mathit{cond} \Leftarrow \mathsf{TBool}}{\Gamma \vdash \mathsf{Assert}\;\mathit{cond} \Rightarrow \mathsf{TVoid}} \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)}` + +{docstring Strata.Laurel.Resolution.Check.assume} + +### Assignment +%%% +tag := "rules-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 +{name Strata.Laurel.Variable.Local}`Local` and {name Strata.Laurel.Variable.Field}`Field`) +or from the {name Strata.Laurel.Variable.Declare}`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. + +{docstring Strata.Laurel.Resolution.Synth.assign} + +$$`\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. + +{docstring Strata.Laurel.Resolution.Check.assign} + +### Calls +%%% +tag := "rules-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)}` + +{docstring Strata.Laurel.Resolution.Synth.staticCall} + +$$`\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 +{name Strata.Laurel.Resolution.Synth.staticCall}`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}`. + +{docstring Strata.Laurel.Resolution.Synth.instanceCall} + +### Primitive operations +%%% +tag := "rules-primitive-operations" +%%% + +`Numeric` abbreviates "consistent with one of {name Strata.Laurel.HighType.TInt}`TInt`, +{name Strata.Laurel.HighType.TReal}`TReal`, +{name Strata.Laurel.HighType.TFloat64}`TFloat64`, or +{name Strata.Laurel.HighType.TBv}`TBv` (a bitvector of any width)", with +`Unknown` admitted as the gradual escape hatch. + +$$`\frac{\Gamma \vdash \mathit{args}_i \Rightarrow U_i \quad U_i <: \mathsf{TBool} \quad \mathit{op} \in \{\mathsf{And}, \mathsf{Or}, \mathsf{AndThen}, \mathsf{OrElse}, \mathsf{Not}, \mathsf{Implies}\}}{\Gamma \vdash \mathsf{PrimitiveOp}\;\mathit{op}\;\mathit{args} \Rightarrow \mathsf{TBool}} \quad \text{([⇒] Op-Bool)}` + +$$`\frac{\Gamma \vdash \mathit{args}_i \Rightarrow U_i \quad \mathsf{Numeric}\;U_i \quad \mathit{op} \in \{\mathsf{Lt}, \mathsf{Leq}, \mathsf{Gt}, \mathsf{Geq}\}}{\Gamma \vdash \mathsf{PrimitiveOp}\;\mathit{op}\;\mathit{args} \Rightarrow \mathsf{TBool}} \quad \text{([⇒] Op-Cmp)}` + +$$`\frac{\Gamma \vdash \mathit{lhs} \Rightarrow T_l \quad \Gamma \vdash \mathit{rhs} \Rightarrow T_r \quad T_l \sim T_r \quad \mathit{op} \in \{\mathsf{Eq}, \mathsf{Neq}\}}{\Gamma \vdash \mathsf{PrimitiveOp}\;\mathit{op}\;[\mathit{lhs}; \mathit{rhs}] \Rightarrow \mathsf{TBool}} \quad \text{([⇒] Op-Eq)}` + +$$`\frac{\Gamma \vdash \mathit{args}_i \Rightarrow U_i \quad \mathsf{Numeric}\;U_i \quad T = \bigsqcup_i U_i \text{ (consistency join)} \quad \mathit{op} \in \{\mathsf{Neg}, \mathsf{Add}, \mathsf{Sub}, \mathsf{Mul}, \mathsf{Div}, \mathsf{Mod}, \mathsf{DivT}, \mathsf{ModT}\}}{\Gamma \vdash \mathsf{PrimitiveOp}\;\mathit{op}\;\mathit{args} \Rightarrow T} \quad \text{([⇒] Op-Arith)}` + +The arithmetic synth rule mirrors $`[⇒]\,\text{Op-Eq}` but generalised +to $`n` operands. Each operand is synthesized and required to be +$`\mathsf{Numeric}` (i.e. $`\mathsf{TInt}`, $`\mathsf{TReal}`, +$`\mathsf{TFloat64}`, $`\mathsf{TBv}_w` (a bitvector of any width), or +the gradual $`\mathsf{Unknown}`). The +result type is the *consistency join* $`\bigsqcup_i U_i` — a fold of +the operand types under +{name Strata.Laurel.isConsistent}`isConsistent`'s flat lattice: +$`\mathsf{Unknown} \sqcup T = T`, $`T \sqcup T = T`, and any other +combination is rejected. The fold runs via `join`, a pure function, so +the search has no diagnostic side-effects. + +:::example "Arithmetic operand join" +- `1 + 2` synthesizes $`\mathsf{TInt}` +- `1.5 + 2.5` synthesizes $`\mathsf{TReal}` +- ` + 1` synthesizes $`\mathsf{TInt}` — the $`\mathsf{Unknown}` operand promotes to its neighbour +- ` + ` synthesizes $`\mathsf{Unknown}` +- `1 + 2.0` is rejected: *cannot apply '+' to operands of types 'int', 'real'* +::: + +$$`\frac{\Gamma \vdash \mathit{args}_i \Rightarrow U_i \quad U_i <: \mathsf{TString} \quad \mathit{op} = \mathsf{StrConcat}}{\Gamma \vdash \mathsf{PrimitiveOp}\;\mathit{op}\;\mathit{args} \Rightarrow \mathsf{TString}} \quad \text{([⇒] Op-Concat)}` + +{docstring Strata.Laurel.Resolution.Synth.primitiveOp} + +The arithmetic and boolean families also have a check-mode rule, used +when the surrounding context provides an `expected` type. The rule +pushes the operand type into each operand via +`Check.resolveStmtExpr`, replacing the synth-then-`checkSubtype` +discipline with bidirectional check. + +$$`\frac{\mathsf{Numeric}\;T \quad \Gamma \vdash \mathit{args}_i \Leftarrow T \quad \mathit{op} \in \{\mathsf{Neg}, \mathsf{Add}, \mathsf{Sub}, \mathsf{Mul}, \mathsf{Div}, \mathsf{Mod}, \mathsf{DivT}, \mathsf{ModT}\}}{\Gamma \vdash \mathsf{PrimitiveOp}\;\mathit{op}\;\mathit{args} \Leftarrow T} \quad \text{([⇐] Op-Arith)}` + +$$`\frac{\mathsf{TBool} <: T \quad \Gamma \vdash \mathit{args}_i \Leftarrow \mathsf{TBool} \quad \mathit{op} \in \{\mathsf{And}, \mathsf{Or}, \mathsf{AndThen}, \mathsf{OrElse}, \mathsf{Not}, \mathsf{Implies}\}}{\Gamma \vdash \mathsf{PrimitiveOp}\;\mathit{op}\;\mathit{args} \Leftarrow T} \quad \text{([⇐] Op-Bool)}` + +{docstring Strata.Laurel.Resolution.Check.primitiveOp} + +### Object forms +%%% +tag := "rules-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. + +{docstring Strata.Laurel.Resolution.Synth.new} + +$$`\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)}` + +{docstring Strata.Laurel.Resolution.Synth.asType} -# Laurel without verification +$$`\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)}` + +{docstring Strata.Laurel.Resolution.Synth.isType} + +$$`\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 {name Strata.Laurel.HighType.UserDefined}`UserDefined` +or {name Strata.Laurel.HighType.Unknown}`Unknown` type. `~` is the consistency relation +{name Strata.Laurel.isConsistent}`isConsistent` — symmetric, with the +{name Strata.Laurel.HighType.Unknown}`Unknown` wildcard. + +{docstring Strata.Laurel.Resolution.Synth.refEq} + +$$`\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)}` + +{docstring Strata.Laurel.Resolution.Synth.pureFieldUpdate} + +### Verification expressions +%%% +tag := "rules-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)}` + +{docstring Strata.Laurel.Resolution.Synth.quantifier} + +$$`\frac{\Gamma \vdash \mathit{name} \Rightarrow \_}{\Gamma \vdash \mathsf{Assigned}\;\mathit{name} \Rightarrow \mathsf{TBool}} \quad \text{([⇒] Assigned)}` + +{docstring Strata.Laurel.Resolution.Synth.assigned} + +$$`\frac{\Gamma \vdash v \Leftarrow T}{\Gamma \vdash \mathsf{Old}\;v \Leftarrow T} \quad \text{([⇐] Old)}` + +{docstring Strata.Laurel.Resolution.Check.old} + +`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)}` + +{docstring Strata.Laurel.Resolution.Synth.old} + +$$`\frac{\Gamma \vdash v \Rightarrow T \quad \mathsf{isReference}\;T}{\Gamma \vdash \mathsf{Fresh}\;v \Rightarrow \mathsf{TBool}} \quad \text{([⇒] Fresh)}` + +{docstring Strata.Laurel.Resolution.Synth.fresh} + +$$`\frac{\Gamma \vdash v \Leftarrow T \quad \Gamma \vdash \mathit{proof} \Rightarrow \_}{\Gamma \vdash \mathsf{ProveBy}\;v\;\mathit{proof} \Leftarrow T} \quad \text{([⇐] ProveBy)}` + +{docstring Strata.Laurel.Resolution.Check.proveBy} + +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)}` + +{docstring Strata.Laurel.Resolution.Synth.proveBy} + +### Self reference +%%% +tag := "rules-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)}` + +{docstring Strata.Laurel.Resolution.Synth.this} + +### Untyped forms +%%% +tag := "rules-untyped-forms" +%%% + +$$`\frac{}{\Gamma \vdash \mathsf{Abstract}\,/\,\mathsf{All}\;\ldots \Rightarrow \mathsf{Unknown}} \quad \text{([⇒] Abstract / All)}` + +{docstring Strata.Laurel.Resolution.Synth.abstract} + +{docstring Strata.Laurel.Resolution.Synth.all} + +### ContractOf +%%% +tag := "rules-contract-of" +%%% + +$$`\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). + +{docstring Strata.Laurel.Resolution.Synth.contractOf} + +### Holes +%%% +tag := "rules-holes" +%%% + +$$`\frac{T_h <: T}{\Gamma \vdash \mathsf{Hole}\;d\;(\mathsf{some}\;T_h) \Leftarrow T} \quad \text{([⇐] Hole-Some)}` + +{docstring Strata.Laurel.Resolution.Check.holeSome} + +$$`\frac{}{\Gamma \vdash \mathsf{Hole}\;d\;\mathsf{none} \Leftarrow T \quad \mapsto \quad \mathsf{Hole}\;d\;(\mathsf{some}\;T)} \quad \text{([⇐] Hole-None)}` + +{docstring Strata.Laurel.Resolution.Check.holeNone} + +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)}` + +### Procedure +%%% +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. + +$$`\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 +{name Strata.Laurel.Resolution.Check.return}`Check.return`) or via +named-output assignment. + +{docstring Strata.Laurel.resolveProcedure} + +{docstring Strata.Laurel.resolveInstanceProcedure} + +# Execution TODO, cover all the non-verification language parts +# Types + +Laurel's types come in two groups: those a user can write — primitives, +collections, and user-defined types — and a few internal constructors the +implementation introduces that have no surface syntax. + +The {name Strata.Laurel.HighType}`HighType` type enumerates every type Laurel +tracks. Alongside the user-writable types it also includes internal constructors +(such as `Unknown` and `MultiValuedExpr`) that the compiler introduces +during resolution and later passes; these have no surface syntax. + +{docstring Strata.Laurel.HighType} + +## User-Defined Types + +User-defined types come in two categories: composite types and constrained types. + +Composite types have fields and procedures, and may extend other composite types. Fields +declare whether they are mutable and specify their type. + +{docstring Strata.Laurel.CompositeType} + +{docstring Strata.Laurel.Field} + +Constrained types are defined by a base type and a constraint over the values of the base +type. Algebraic datatypes can be encoded using composite and constrained types. + +{docstring Strata.Laurel.ConstrainedType} + +{docstring Strata.Laurel.TypeDefinition} + +# Expressions and Statements + +Laurel uses a unified `StmtExpr` type that contains both expression-like and statement-like +constructs. This avoids duplication of shared concepts such as conditionals and variable +declarations. + +## Operations + +{docstring Strata.Laurel.Operation} + +## The StmtExpr Type + +{docstring Strata.Laurel.StmtExpr} + +## Metadata + +All AST nodes can carry metadata via the `AstNode` wrapper. + +{docstring Strata.Laurel.AstNode} + +# Procedures + +Procedures are the main unit of specification and verification in Laurel. + +{docstring Strata.Laurel.Procedure} + +{docstring Strata.Laurel.Parameter} + +{docstring Strata.Laurel.Body} + +# Programs + +A Laurel program consists of procedures, global variables, type definitions, and constants. + +{docstring Strata.Laurel.Program} + ## Primitive types Laurel provides unbounded mathematical `int` and `real` types, a `bool` type, @@ -115,7 +895,6 @@ another: `o#inner#x` reads field `x` of the object stored in `o`'s `inner` field and `o#inner#isOne()` calls a method on it. ``` -program Laurel; composite Inner { var x: int } composite Outer { var inner: Inner } @@ -127,7 +906,7 @@ procedure useOuter() }; ``` -# Verification fundamentals +# Verification - Fundamentals ## Assertions @@ -136,7 +915,6 @@ program. If the solver cannot prove it, verification fails and the failing `assert` is reported. ``` -program Laurel; procedure checkPositive(x: int) requires x > 0 opaque @@ -152,7 +930,6 @@ something false makes everything afterwards trivially provable, which is occasionally useful but should be used with care. ``` -program Laurel; procedure assumeThenProve() opaque { @@ -165,6 +942,10 @@ Assertions are the building block behind every other verification feature in this guide. Preconditions, postconditions, and loop invariants are all ultimately checked by turning them into assertions at the right program points. +## Erased code + +TODO, show that assignments inside a contract may not be to variables declared outside the contract. + ## Loop invariants Laurel cannot know in advance how many times a loop runs, so it reasons about @@ -176,7 +957,6 @@ true, which is what lets it prove that operations in the body are safe. After th loop it combines with the negated guard to describe the state on exit. ``` -program Laurel; procedure countUp() opaque { @@ -208,7 +988,6 @@ must prove the precondition holds for the arguments it passes. And it gives the body an assumption to work from when proving its own obligations. ``` -program Laurel; procedure halve(x: int) returns (r: int) requires x > 0 opaque @@ -229,7 +1008,6 @@ A procedure may have several `requires` clauses; they are conjoined. A call must satisfy all of them. ``` -program Laurel; procedure addBoth(x: int, y: int) returns (r: int) requires x > 0 requires y > 0 @@ -240,18 +1018,15 @@ procedure addBoth(x: int, y: int) returns (r: int) }; ``` -Functions support `requires` clauses too, with the same meaning: each use of the -function must prove the requirement. - ## Postconditions -A *postcondition*, written with `ensures`, states what a procedure guarantees -when it returns. Laurel checks the body against every `ensures` clause, and -callers may rely on those clauses without looking at the body. Postconditions are -how you say precisely what a procedure does. +A postcondition for a procedure is a condition that is guaranteed to hold after the procedure executes. Sometimes, we can capture the entire desired behavior of a procedure with a postcondition that is simpler than the procedure's implementation. A typical example of sorting a list of numbers: the end result, that the list is sorted, is simpler to describe the the algorithm to do the sorting. + +When a postcondition can capture the entire desired behavior of a procedure, and is simpler than the body, then adding it allows improving the correctness guarantee of your program, since only the simpler postcondition needs to be reviewed for correctness. Also, when postconditions are added to a procedure, callers will only be able to use the postconditions to reason about the call, and not the body. This simplifies reasoning at the call-site, improving verification results. + +In Laurel, to be explicit, a procedure with postconditions must be marked as `opaque`, indicating that its body is not visible to callers. A procedure without postconditions can also be marked `opaque`, although then callers will know nothing about the result of the call. By default Laurel procedures have a transparent body, meaning that callers can use the callee's body for reasoning about the call's result. ``` -program Laurel; procedure max(x: int, y: int) returns (r: int) opaque ensures r >= x @@ -266,7 +1041,6 @@ procedure max(x: int, y: int) returns (r: int) At a call site, the postcondition is all the caller knows about the result: ``` -program Laurel; procedure useMax() opaque { @@ -291,7 +1065,6 @@ A `forall` states that its body holds for every value of the bound variables; an take one or more typed binders and a body introduced with `=>`. ``` -program Laurel; procedure quantifiers() opaque { @@ -305,7 +1078,6 @@ the range of interest — for instance, to say something about every index of an array within bounds: ``` -program Laurel; procedure inContract(n: int) requires n > 0 opaque @@ -320,8 +1092,7 @@ instantiates a quantifier, you can attach a *trigger* — a pattern in braces th tells the solver which terms should cause the quantified fact to fire: ``` -program Laurel; -function P(x: int): int; +procedure P(x: int): int; procedure withTrigger() opaque { @@ -330,22 +1101,23 @@ procedure withTrigger() }; ``` -# Verification of object mutation +## Termination checking + +To be designed.. +## Constrained types + +TODO, fill in + +# Verification - Objects ## Modifies clauses -When a procedure may change the fields of objects on the heap, it must say so -with a `modifies` clause. The clause lists the references the procedure is -allowed to mutate. This *frame* is what callers rely on to know what did *not* -change across a call. +As previously mentioned, Laurel procedures have a transparent body by default, so callers can reason about the callee's body. This works also when the callee mutates the heap in its body. However, when we make a heap-mutatijng procedure `opaque`, and the body is no longer available for reasoning, then the caller must accept the possibility that the entire heap was mutated, meaning that nothing can be proven about the heap any more, a really bad thing. To enable heap reasoning after calling opaque heap-mutating procedures, Laurel has modifies clauses. -A `modifies` clause is especially important on `opaque` procedures: without it, a -caller would have to assume the call could have changed any heap state. With it, -the caller keeps every fact about objects outside the frame. +A modifies clause specifies the heap references that may have been modified by the procedure. Example: ``` -program Laurel; composite Container { var value: int } @@ -360,26 +1132,23 @@ procedure bump(c: Container) procedure caller() opaque { - var c: Container := new Container; - var d: Container := new Container; - var x: int := d#value; - bump(c); - assert x == d#value // holds: only c is in bump's modifies clause + var a: Container := new Container; + var b: Container := new Container; + var x: int := a#value; + var y: int := b#value; + bump(b); + assert x == a#value // holds: only b is in bump's modifies clause + assert y == b#value // fails: b is in bump's modifies clause }; ``` -A procedure that writes to a field it has not listed is rejected, and so is a -call that passes more permission than the caller itself holds. You can list -several references by repeating the clause (`modifies c; modifies d`), and the -wildcard `modifies *` permits modifying any object — at the cost of telling -callers that nothing on the heap is preserved. +A opaque procedure that writes to an object it has not listed in the modifies clause is rejected, also when this write is done through another procedure call. You can list several references by repeating the clause (`modifies c; modifies d`), and the wildcard `modifies *` permits modifying any object — at the cost of telling callers that nothing on the heap is preserved. Objects allocated with `new` *inside* the procedure body are exempt: a freshly allocated object may be modified freely without appearing in the `modifies` clause, because no caller could hold any prior knowledge about it. ``` -program Laurel; composite Container { var value: int } procedure makeOne() @@ -390,6 +1159,12 @@ procedure makeOne() }; ``` +## Reads clauses + +To be designed.. + +Reads clauses can only be specified for deterministic procedures + ## Old In a postcondition you often want to relate the state when the procedure returns @@ -398,7 +1173,6 @@ that expression in the *pre-state* — the heap as it was on entry. This is the standard way to specify a procedure that mutates its arguments. ``` -program Laurel; composite Cell { var value: int } @@ -421,7 +1195,6 @@ sub-expression: `old(2 * c#value + 3)` means the same as `2 * old(c#value) + 3`. It may also appear inside quantifiers and conditionals in a postcondition: ``` -program Laurel; composite Cell { var value: int } procedure strictBump(c: Cell) @@ -461,3 +1234,23 @@ procedure bumpCellCaller() An `old(...)` that mentions nothing from the heap has no effect and Laurel warns about it, since it cannot relate two states. The same warning is issued for a redundant `old(old(...))`, whose inner `old` is dropped. + +## Allocated and fresh + +To be designed.. + +## Immutable fields + +To be designed.. + +## Type invariants + +To be designed.. + +## Concurrency + +To be designed.. + +# Verification - Proof hints + +To be designed.. diff --git a/docs/verso/LaurelUserGuideMain.lean b/docs/verso/LaurelUserGuideMain.lean index 1177242378..4e63be4a51 100644 --- a/docs/verso/LaurelUserGuideMain.lean +++ b/docs/verso/LaurelUserGuideMain.lean @@ -11,8 +11,10 @@ open Verso.Genre.Manual (RenderConfig manualMain) def config : RenderConfig where emitTeX := false - emitHtmlSingle := .immediately - emitHtmlMulti := .no + -- Multi-page output so the sidebar navigation is nested: each top-level + -- section becomes its own page and its subsections show in the sidebar. + emitHtmlSingle := .no + emitHtmlMulti := .immediately htmlDepth := 2 def main := manualMain (%doc LaurelUserGuide) (config := config) diff --git a/docs/verso/Makefile b/docs/verso/Makefile index 0e18e926c9..3cb9217b64 100644 --- a/docs/verso/Makefile +++ b/docs/verso/Makefile @@ -12,10 +12,31 @@ build-langdef: lake exe langdef --with-html-single --output _out/langdef cp strata-hourglass.png _out/langdef/html-single/ +build-laurelguide: + lake exe laurelguide --with-html-multi --output _out/laurelguide + +build-laureldesign: + lake exe laureldesign --with-html-multi --output _out/laureldesign + +build-laurelimpl: + lake exe laurelimpl --with-html-multi --output _out/laurelimpl + serve-%: @(sleep 1 && open http://localhost:$(PORT)/) & python3 -m http.server $(PORT) -d _out/$*/html-single +serve-laurelguide: + @(sleep 1 && open http://localhost:$(PORT)/) & + python3 -m http.server $(PORT) -d _out/laurelguide/html-multi + +serve-laureldesign: + @(sleep 1 && open http://localhost:$(PORT)/) & + python3 -m http.server $(PORT) -d _out/laureldesign/html-multi + +serve-laurelimpl: + @(sleep 1 && open http://localhost:$(PORT)/) & + python3 -m http.server $(PORT) -d _out/laurelimpl/html-multi + all: ./generate.sh diff --git a/docs/verso/generate.sh b/docs/verso/generate.sh index 069805ea08..1ef08f6e8e 100755 --- a/docs/verso/generate.sh +++ b/docs/verso/generate.sh @@ -16,9 +16,9 @@ lake build Strata:docs cd "${curpwd}" lake exe ddm --with-html-single --output _out/ddm lake exe langdef --with-html-single --output _out/langdef -lake exe laureldesign --with-html-single --output _out/laureldesign -lake exe laurelimpl --with-html-single --output _out/laurelimpl -lake exe laurelguide --with-html-single --output _out/laurelguide +lake exe laureldesign --with-html-multi --output _out/laureldesign +lake exe laurelimpl --with-html-multi --output _out/laurelimpl +lake exe laurelguide --with-html-multi --output _out/laurelguide lake exe transforms --with-html-single --output _out/transforms lake exe irtranslation --with-html-single --output _out/irtranslation cp strata-hourglass.png _out/langdef/html-single/ diff --git a/docs/verso/index.html b/docs/verso/index.html index 9f4db6fd4c..6ccaa107f1 100644 --- a/docs/verso/index.html +++ b/docs/verso/index.html @@ -32,15 +32,15 @@

DDM Documentation

Strata Core Language Definition Documentation

Documentation for Strata Core language definition.

 - +

Laurel Language Design Guide

How the Laurel intermediate verification language is defined: its types, unified expression/statement model, procedures, programs, and type checking. Laurel attempts to provide features that are common to Java, Python, and JavaScript.

 - +

Laurel Implementation Guide

How a checked Laurel program is lowered to Strata Core: the translation pipeline, its passes and their ordering, and the differences between Laurel and Core.

 - +

Laurel User Guide

A task-oriented guide to writing Laurel specifications: assertions, loop invariants, pre- and postconditions, quantifiers, objects, modifies clauses, and old.

 From 3c0114c95f9dd692023154a9bac342bbc4156815 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Tue, 7 Jul 2026 12:23:08 +0000 Subject: [PATCH 03/20] Kiro improvements --- docs/verso/LaurelDesignGuide.lean | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/docs/verso/LaurelDesignGuide.lean b/docs/verso/LaurelDesignGuide.lean index 49fdbfaab2..3b931194b0 100644 --- a/docs/verso/LaurelDesignGuide.lean +++ b/docs/verso/LaurelDesignGuide.lean @@ -51,7 +51,7 @@ Goals: 7. Code used to enable verification may not affect execution behavior. # Reduce duplication between source languages -To achieve goal (2), reduce code duplication in the analysis of popular languages, Laurel contains many features shared between several languages. The following table shows which features are shared with whch input languages. +To achieve goal (2), reduce code duplication in the analysis of popular languages, Laurel contains many features shared between several languages. The following table shows which features are shared with which input languages. TODO, add a table with Laurel features as rows, and a list of languages in columns (Java, Kotlin, C#, JavaScript, Python, GoLang). Split up language feature whenever relevant for the columns. @@ -70,7 +70,7 @@ To achieve goal 1.3, enable proving properties through verification, Laurel has - Assumptions (more about gradual verification) # Modular Verification -The achieve goal (4), Laurel has the following features related to modular verification. +To achieve goal (4), Laurel has the following features related to modular verification. ## Preconditions Preconditions enable proving the assertions in a procedure's body without having to consider the callers. This way, each assertion only needs to be proven once, instead of once for each transitive call-site. @@ -78,11 +78,11 @@ Preconditions enable proving the assertions in a procedure's body without having ## Encapsulation Postconditions enable encapsulating the behavior of a procedure through a simpler condition. This simplifies reasoning at the call-site. -Since procedure can mutate references as well, once we add encapsulation through postconditions, we also need modifies clauses to enable encapsulating reference modifying procedures. +Since procedures can mutate references as well, once we add encapsulation through postconditions, we also need modifies clauses to enable encapsulating reference modifying procedures. -Reads clauses are useful to improve verification performance. The facts they prove work well together with the facts provided by modified clauses, making it easier to prove which procedure values have remained unchanged after objects were modified. +Reads clauses are useful to improve verification performance. The facts they prove work well together with the facts provided by modifies clauses, making it easier to prove which procedure values have remained unchanged after objects were modified. -## Reduce verification through complete analysis +# Reduce verification through complete analysis To achieve goal 5, Laurel has the following features. ## Constrained types @@ -115,7 +115,7 @@ procedure increment(counter: Counter) opaque ## Heap mutation in contracts A contract in Laurel may not modify any object that exists outside of that contract, as if the contract has an empty modifies clause. However, new objects may be created and modified inside the contract. -A common design choice in verification aware programming language is not to allow creating or modifying objects in contracts. A good reason for this is that objects are more complex to reason about than immutable data, and contracts are intended to contain easy to reason about code. Laurel still allows this because code might be declared to operate specifically through the use of reference types, and Laurel does not want to restrict users from using such code even in contracts. +A common design choice in verification-aware programming languages is not to allow creating or modifying objects in contracts. A good reason for this is that objects are more complex to reason about than immutable data, and contracts are intended to contain easy to reason about code. Laurel still allows creating and modifying new objects inside contracts because code might be declared to operate specifically through the use of reference types, and Laurel does not want to restrict users from using such code even in contracts. A second reason for not allowing any heap modification inside contracts is that this is prone to soundness issues. From outside the contract the heap is assumed not to be modified, so if knowledge of an inside modification escapes the contract, this leads to an inconsistency. Because Laurel does not allow assigning to variable defined outside the contract, from inside the contract, no modification can escape the contract. The heap used inside a contract is a separate heap variable. From 06bab7f96c76574db67a766970a353cd368699ca Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Tue, 7 Jul 2026 12:40:04 +0000 Subject: [PATCH 04/20] More changes --- docs/verso/LaurelDesignGuide.lean | 119 ++++++++++++++++-------------- 1 file changed, 62 insertions(+), 57 deletions(-) diff --git a/docs/verso/LaurelDesignGuide.lean b/docs/verso/LaurelDesignGuide.lean index 3b931194b0..cc8ea4caad 100644 --- a/docs/verso/LaurelDesignGuide.lean +++ b/docs/verso/LaurelDesignGuide.lean @@ -22,8 +22,6 @@ open Verso.Genre Manual -- environment as Verso open Verso.Genre.Manual.InlineLean - - #doc (Manual) "The Laurel Language Design Guide" => %%% shortTitle := "Laurel Design" @@ -44,59 +42,71 @@ Goals: 2. data-flow analysis 3. symbolic execution (aka verification), both bounded and unbounded 2. Reduce code duplication in the analysis of popular languages by being a target for compilation from those languages, and including features common to them. Note that we expect source languages to reduce their existing compilers when possible, so language features that can be compiled away don't need to be considered. -3. Minimize the amount of user code needed to enable verification. +3. Have a great user experience 4. Enable modular verification -5. Use complete analysis algorithms to reduce the required proof effort. +5. Minimize the amount of user code needed to enable verification. 6. Enable finding proofs through an automated search. -7. Code used to enable verification may not affect execution behavior. - -# Reduce duplication between source languages -To achieve goal (2), reduce code duplication in the analysis of popular languages, Laurel contains many features shared between several languages. The following table shows which features are shared with which input languages. - -TODO, add a table with Laurel features as rows, and a list of languages in columns (Java, Kotlin, C#, JavaScript, Python, GoLang). Split up language feature whenever relevant for the columns. - -These features should be in rows but marked as WIP: -- Try/catch and checked exception -- Procedures types and procedures as values -- Parametric polymorphism +7. Use complete analysis algorithms to reduce the required proof effort. +8. Code used to enable verification may not affect execution behavior. -# Enable Verification +# (1.3) Enable Verification To achieve goal 1.3, enable proving properties through verification, Laurel has the following features. - Assertions - Quantifiers - Old/allocated/fresh - Decreases clauses -- Loop invariants (more about automated proof) - Assumptions (more about gradual verification) -# Modular Verification -To achieve goal (4), Laurel has the following features related to modular verification. +# (2) Reduce duplication between source languages +To achieve goal (2), reduce code duplication in the analysis of popular languages, Laurel contains many features shared between several languages. The following table shows which features are shared with which input languages. -## Preconditions -Preconditions enable proving the assertions in a procedure's body without having to consider the callers. This way, each assertion only needs to be proven once, instead of once for each transitive call-site. +TODO, add a table with Laurel features as rows, and a list of languages in columns (Java, Kotlin, C#, JavaScript, Python, GoLang). Split up language feature whenever relevant for the columns. -## Encapsulation -Postconditions enable encapsulating the behavior of a procedure through a simpler condition. This simplifies reasoning at the call-site. +These features should be in rows but marked as WIP: +- Try/catch and checked exception +- Procedures types and procedures as values +- Parametric polymorphism -Since procedures can mutate references as well, once we add encapsulation through postconditions, we also need modifies clauses to enable encapsulating reference modifying procedures. +# (3) Great user experience -Reads clauses are useful to improve verification performance. The facts they prove work well together with the facts provided by modifies clauses, making it easier to prove which procedure values have remained unchanged after objects were modified. +## Parameter lists +Parameter lists. In Laurel, input and output parameters are defined in a separate list. Inout parameters are defined by repeating the parameter name in both lists. In Core, there is a single parameter list where each parameter defines its kind (in/out/inout). -# Reduce verification through complete analysis -To achieve goal 5, Laurel has the following features. +At the call-site, Laurel requires calls with multiple out parameters to occur inside an assignment, like this: +`assign x, y := multiOutCall(a, b)` +Core uses the argument list to assign the output parameters, like this: +`multiOutCall(a, b, out x, out y)` -## Constrained types -Constrained types propagating facts through the type system. +In Laurel, an inout parameter only influences the callee's code, since it means there is a single variable that is used as input and output. On the calling side however, there is no concept of inout parameters. This is different from Core, where inout variables affect the calling side. Example of an inout being called in Core, `hasInout(inout x)`. -TODO, add example using polymorphic types +## Assignments to fresh and existing declarations +In Laurel, assignments can have multiple targets. Each target can be either an existing variable or a local declaration. Example: +``` +var x: int; +var z: int; +assign x, var y: int, z := hasThreeOutputs() +``` +In Core, when calling a procedure with multiple outputs, each output parameter must be assigned to an existing local variable. Example: +``` +var x: int; +var y: int; +var z: int; +hasThreeOutputs(out x, out y, out z); +``` -## Implicit conversions +# (4) Modular Verification +To achieve goal (4), Laurel has the following features related to modular verification. -To be designed.. +## Preconditions +Preconditions enable proving the assertions in a procedure's body without having to consider the callers. This way, each assertion only needs to be proven once, instead of once for each transitive call-site. +## Opaque procedures +Laurel allows a procedure to be marked as opaque, which means that callers won't get access to the body of the procedure. Laurel only allows postconditions for opaque procedures. This restriction is because a postcondition can only contain information that can also be inferred from the body, and redundant information is bad for verification performance. -# Minimize Verification Code -To achieve goal (3), minimize the amount of user code needed to enable verification, Laurel has the following features: +Since modifies clauses are a type of postcondition, they are also only allowed on opaque procedures. + +# (5) Minimize Verification Code +To achieve goal (5), minimize the amount of user code needed to enable verification, Laurel has the following features: ## Transparent procedures Laurel procedures are transparent by default, meaning that a call can use the body of the callee to prove facts about the result of the call. Laurel will allow any procedure to be transparent, although currently there are some restrictions. In particular, Laurel will allow procedures that contains loops or that modify the heap, to be transparent as well. @@ -123,31 +133,26 @@ A second reason for not allowing any heap modification inside contracts is that TODO, fill in -# Naming choices +# (6) Enable finding proofs through an automated search. -# Differences between Laurel and Core +Loop invariants -## Parameter lists -Parameter lists. In Laurel, input and output parameters are defined in a separate list. Inout parameters are defined by repeating the parameter name in both lists. In Core, there is a single parameter list where each parameter defines its kind (in/out/inout). +Reads clauses are useful to improve verification performance. The facts they prove work well together with the facts provided by modifies clauses, making it easier to prove which procedure values have remained unchanged after objects were modified. -At the call-site, Laurel requires calls with multiple out parameters to occur inside an assignment, like this: -`assign x, y := multiOutCall(a, b)` -Core uses the argument list to assign the output parameters, like this: -`multiOutCall(a, b, out x, out y)` +# (7) Reduce verification through complete analysis +To achieve goal 7, Laurel has the following features. -In Laurel, an inout parameter only influences the callee's code, since it means there is a single variable that is used as input and output. On the calling side however, there is no concept of inout parameters. This is different from Core, where inout variables affect the calling side. Example of an inout being called in Core, `hasInout(inout x)`. +## Constrained types +Constrained types propagating facts through the type system. -## Assignments to fresh and existing declarations -In Laurel, assignments can have multiple targets. Each target can be either an existing variable or a local declaration. Example: -``` -var x: int; -var z: int; -assign x, var y: int, z := hasThreeOutputs() -``` -In Core, when calling a procedure with multiple outputs, each output parameter must be assigned to an existing local variable. Example: -``` -var x: int; -var y: int; -var z: int; -hasThreeOutputs(out x, out y, out z); -``` +TODO, add example using polymorphic types + +## Implicit conversions + +To be designed.. + +# (8) Verification code may not affect execution + +TODO, Rules for contracts: +- Contract code may not modify variables defined outside the contract scope. +- Contract code has an empty modifies clause. Contract code operates on a copy of the heap. From f36571c19bc4b9022c0fe8cffe49d7ae26e7fc97 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Tue, 7 Jul 2026 13:24:38 +0000 Subject: [PATCH 05/20] Updates --- docs/verso/LaurelDesignGuide.lean | 239 ++++++++++++++++++++++++------ docs/verso/LaurelUserGuide.lean | 22 +-- 2 files changed, 206 insertions(+), 55 deletions(-) diff --git a/docs/verso/LaurelDesignGuide.lean b/docs/verso/LaurelDesignGuide.lean index cc8ea4caad..2afbef7b8b 100644 --- a/docs/verso/LaurelDesignGuide.lean +++ b/docs/verso/LaurelDesignGuide.lean @@ -49,7 +49,7 @@ Goals: 7. Use complete analysis algorithms to reduce the required proof effort. 8. Code used to enable verification may not affect execution behavior. -# (1.3) Enable Verification +# Enable Verification To achieve goal 1.3, enable proving properties through verification, Laurel has the following features. - Assertions - Quantifiers @@ -57,44 +57,165 @@ To achieve goal 1.3, enable proving properties through verification, Laurel has - Decreases clauses - Assumptions (more about gradual verification) -# (2) Reduce duplication between source languages +# Prevent duplicate work To achieve goal (2), reduce code duplication in the analysis of popular languages, Laurel contains many features shared between several languages. The following table shows which features are shared with which input languages. -TODO, add a table with Laurel features as rows, and a list of languages in columns (Java, Kotlin, C#, JavaScript, Python, GoLang). Split up language feature whenever relevant for the columns. - -These features should be in rows but marked as WIP: -- Try/catch and checked exception -- Procedures types and procedures as values -- Parametric polymorphism - -# (3) Great user experience - -## Parameter lists -Parameter lists. In Laurel, input and output parameters are defined in a separate list. Inout parameters are defined by repeating the parameter name in both lists. In Core, there is a single parameter list where each parameter defines its kind (in/out/inout). - -At the call-site, Laurel requires calls with multiple out parameters to occur inside an assignment, like this: -`assign x, y := multiOutCall(a, b)` -Core uses the argument list to assign the output parameters, like this: -`multiOutCall(a, b, out x, out y)` - -In Laurel, an inout parameter only influences the callee's code, since it means there is a single variable that is used as input and output. On the calling side however, there is no concept of inout parameters. This is different from Core, where inout variables affect the calling side. Example of an inout being called in Core, `hasInout(inout x)`. - -## Assignments to fresh and existing declarations -In Laurel, assignments can have multiple targets. Each target can be either an existing variable or a local declaration. Example: -``` -var x: int; -var z: int; -assign x, var y: int, z := hasThreeOutputs() -``` -In Core, when calling a procedure with multiple outputs, each output parameter must be assigned to an existing local variable. Example: -``` -var x: int; -var y: int; -var z: int; -hasThreeOutputs(out x, out y, out z); -``` - -# (4) Modular Verification +Legend: the *Laurel* column records Laurel's own status — ✓ implemented, WIP planned but not yet implemented, ✗ not planned. The source-language columns record — ✓ directly supported, ~ partial or library-only (semantics differ, or only available through a standard library rather than the core language), — not present. + +:::table +header + * + * Feature + * Laurel + * Java + * JavaScript + * Python + * + * Reference (heap) objects + * ✓ + * ✓ + * ✓ + * ✓ + * + * Classes with instance methods + * ✓ + * ✓ + * ✓ + * ✓ + * + * Multiple supertypes for subtyping (interface conformance) + * ✓ + * ✓ + * — + * ✓ + * + * Multiple implementation inheritance (fields/methods from several parents) + * ✓ + * — + * ~ + * ✓ + * + * Value (structural) types + * ✓ + * ~ + * — + * ~ + * + * Runtime type test and cast (`is` / `as`) + * ✓ + * ✓ + * ✓ + * ✓ + * + * Reference equality + * ✓ + * ✓ + * ✓ + * ✓ + * + * Arbitrary-precision integers + * ✓ + * ~ + * ~ + * ✓ + * + * IEEE-754 64-bit floats + * ✓ + * ✓ + * ✓ + * ✓ + * + * Strings + * ✓ + * ✓ + * ✓ + * ✓ + * + * Sets and maps + * ✓ + * ✓ + * ✓ + * ✓ + * + * Fixed-width bitvector operations + * ✓ + * ✓ + * ~ + * ~ + * + * `while` loops + * ✓ + * ✓ + * ✓ + * ✓ + * + * `do`/`while` (post-test) loops + * ✓ + * ✓ + * ✓ + * — + * + * `break` / `continue` (direct statements) + * WIP + * ✓ + * ✓ + * ✓ + * + * `break` / `continue` via labelled block exit (`exit L`) + * ✓ + * ✓ + * ✓ + * ~ + * + * Increment / decrement operators (`++` / `--`) + * ✓ + * ✓ + * ✓ + * — + * + * Short-circuit boolean operators (`&&` / `||`) + * ✓ + * ✓ + * ✓ + * ✓ + * + * Algebraic datatypes / pattern matching + * ✓ + * ~ + * — + * ~ + * + * Try / catch and checked exceptions + * WIP + * ✓ + * ~ + * ~ + * + * Procedure types and procedures as values + * WIP + * ✓ + * ✓ + * ✓ + * + * Parametric polymorphism (generics) + * WIP + * ✓ + * — + * ~ +::: + +Notes on the partial (~) entries: +- *Multiple supertypes for subtyping* — Laurel's `extending` list lets a type declare several supertypes for `is`/`as` and subtyping. Java gets this from implementing multiple interfaces (and Python from its MRO). JavaScript has only a single prototype chain and no interface concept. +- *Multiple implementation inheritance* — this is the stronger form Python needs: inheriting fields and method implementations from several concrete parents, resolved by an MRO. Only Python has it fully; JavaScript relies on ad-hoc mixin patterns, and Java has none (interfaces provide default methods but no fields). +- *Value (structural) types* — Java has records and primitives; Python has frozen dataclasses and tuples; JavaScript has no value objects. +- *Arbitrary-precision integers* — only Python has them as the default `int`; Java and JavaScript expose them through a library (`BigInteger`, `BigInt`). +- *Fixed-width bitvector operations* — JavaScript's bitwise operators are 32-bit; Python integers are arbitrary width. +- *`do`/`while` loops* — Python has none. +- *`break` / `continue`* — Laurel does not yet have dedicated `break`/`continue` keywords (WIP). It already provides the more general primitive underneath them: a labelled block `{ … } L` and an `exit L` statement that jumps to the end of that block. `break` is an exit of the block wrapping the loop, and `continue` an exit of the block wrapping the loop body, so the one primitive covers both. On the labelled-exit row, Python has `break`/`continue` without labels. +- *Increment / decrement* — Python has no such operators. +- *Algebraic datatypes / pattern matching* — Java (sealed types + `switch` patterns) and Python (`match`) support a subset; JavaScript has none. +- *Exceptions* — Java has checked exceptions; JavaScript and Python have exceptions, but unchecked. + +# Modular Verification To achieve goal (4), Laurel has the following features related to modular verification. ## Preconditions @@ -105,7 +226,7 @@ Laurel allows a procedure to be marked as opaque, which means that callers won't Since modifies clauses are a type of postcondition, they are also only allowed on opaque procedures. -# (5) Minimize Verification Code +# Minimize Verification Code To achieve goal (5), minimize the amount of user code needed to enable verification, Laurel has the following features: ## Transparent procedures @@ -133,26 +254,56 @@ A second reason for not allowing any heap modification inside contracts is that TODO, fill in -# (6) Enable finding proofs through an automated search. +# Automated proof search +Goal 6 was enabling the finding of proofs through automated search. -Loop invariants +Loop invariants. These enable unbounded symbolic execution Reads clauses are useful to improve verification performance. The facts they prove work well together with the facts provided by modifies clauses, making it easier to prove which procedure values have remained unchanged after objects were modified. -# (7) Reduce verification through complete analysis -To achieve goal 7, Laurel has the following features. +# Use complete algorithms to reduce workload +To achieve goal 7, to reduce the verification work through the use of complete algorithms, Laurel has the following features. ## Constrained types Constrained types propagating facts through the type system. -TODO, add example using polymorphic types +TODO, add example using polymorphic types, like a wrapping Container that takes a `nat` and we still have the `nat` fact on the other side. ## Implicit conversions To be designed.. -# (8) Verification code may not affect execution +# Verification without side-effects + +To support goal 8, for verification code not to affect the outcome of executing the program, Laurel has rules for code that exists only for verification purposes. TODO, Rules for contracts: - Contract code may not modify variables defined outside the contract scope. - Contract code has an empty modifies clause. Contract code operates on a copy of the heap. + +# Great user experience + +## Parameter lists +Parameter lists. In Laurel, input and output parameters are defined in a separate list. Inout parameters are defined by repeating the parameter name in both lists. In Core, there is a single parameter list where each parameter defines its kind (in/out/inout). + +At the call-site, Laurel requires calls with multiple out parameters to occur inside an assignment, like this: +`assign x, y := multiOutCall(a, b)` +Core uses the argument list to assign the output parameters, like this: +`multiOutCall(a, b, out x, out y)` + +In Laurel, an inout parameter only influences the callee's code, since it means there is a single variable that is used as input and output. On the calling side however, there is no concept of inout parameters. This is different from Core, where inout variables affect the calling side. Example of an inout being called in Core, `hasInout(inout x)`. + +## Assignments to fresh and existing declarations +In Laurel, assignments can have multiple targets. Each target can be either an existing variable or a local declaration. Example: +``` +var x: int; +var z: int; +assign x, var y: int, z := hasThreeOutputs() +``` +In Core, when calling a procedure with multiple outputs, each output parameter must be assigned to an existing local variable. Example: +``` +var x: int; +var y: int; +var z: int; +hasThreeOutputs(out x, out y, out z); +``` diff --git a/docs/verso/LaurelUserGuide.lean b/docs/verso/LaurelUserGuide.lean index 5ebc09d00a..a837210588 100644 --- a/docs/verso/LaurelUserGuide.lean +++ b/docs/verso/LaurelUserGuide.lean @@ -782,7 +782,7 @@ named-output assignment. TODO, cover all the non-verification language parts -# Types +## Types Laurel's types come in two groups: those a user can write — primitives, collections, and user-defined types — and a few internal constructors the @@ -795,7 +795,7 @@ during resolution and later passes; these have no surface syntax. {docstring Strata.Laurel.HighType} -## User-Defined Types +### User-Defined Types User-defined types come in two categories: composite types and constrained types. @@ -813,27 +813,27 @@ type. Algebraic datatypes can be encoded using composite and constrained types. {docstring Strata.Laurel.TypeDefinition} -# Expressions and Statements +## Expressions and Statements Laurel uses a unified `StmtExpr` type that contains both expression-like and statement-like constructs. This avoids duplication of shared concepts such as conditionals and variable declarations. -## Operations +### Operations {docstring Strata.Laurel.Operation} -## The StmtExpr Type +### The StmtExpr Type {docstring Strata.Laurel.StmtExpr} -## Metadata +## Sources -All AST nodes can carry metadata via the `AstNode` wrapper. +All AST nodes can carry a source location via the `AstNode` wrapper. {docstring Strata.Laurel.AstNode} -# Procedures +## Procedures Procedures are the main unit of specification and verification in Laurel. @@ -843,20 +843,20 @@ Procedures are the main unit of specification and verification in Laurel. {docstring Strata.Laurel.Body} -# Programs +## Programs A Laurel program consists of procedures, global variables, type definitions, and constants. {docstring Strata.Laurel.Program} -## Primitive types +### Primitive types Laurel provides unbounded mathematical `int` and `real` types, a `bool` type, `string`, and fixed-width bitvectors. Because `int` is unbounded, arithmetic in specifications behaves like ordinary mathematics: there is no overflow to reason around when you are stating what a procedure computes. -## Composites +### Composites Laurel models objects with *composite* types. A composite declares mutable fields and may declare *instance procedures* (methods). Fields are read and From 1bef6a81f524deaf824cb4bbf95e2c4acefec201 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Tue, 7 Jul 2026 13:48:57 +0000 Subject: [PATCH 06/20] Remove Pure type for now --- .../Languages/Laurel/CoreGroupingAndOrdering.lean | 1 - Strata/Languages/Laurel/FilterPrelude.lean | 1 - .../Grammar/AbstractToConcreteTreeTranslator.lean | 1 - Strata/Languages/Laurel/LaurelAST.lean | 10 +--------- Strata/Languages/Laurel/Resolution.lean | 4 ---- Strata/Languages/Laurel/TypeAliasElim.lean | 1 - Strata/Languages/Laurel/TypeHierarchy.lean | 1 - docs/verso/LaurelDesignGuide.lean | 14 +++++++------- 8 files changed, 8 insertions(+), 25 deletions(-) diff --git a/Strata/Languages/Laurel/CoreGroupingAndOrdering.lean b/Strata/Languages/Laurel/CoreGroupingAndOrdering.lean index 791959fbe2..67311360a2 100644 --- a/Strata/Languages/Laurel/CoreGroupingAndOrdering.lean +++ b/Strata/Languages/Laurel/CoreGroupingAndOrdering.lean @@ -39,7 +39,6 @@ def collectTypeRefs : HighTypeMd → List String | ⟨.TMap k v, _⟩ => collectTypeRefs k ++ collectTypeRefs v | ⟨.Applied base args, _⟩ => collectTypeRefs base ++ args.flatMap collectTypeRefs - | ⟨.Pure base, _⟩ => collectTypeRefs base | ⟨.Intersection ts, _⟩ => ts.flatMap collectTypeRefs | ⟨.TCore name, _⟩ => [name] | _ => [] diff --git a/Strata/Languages/Laurel/FilterPrelude.lean b/Strata/Languages/Laurel/FilterPrelude.lean index ac55c92aae..008e655679 100644 --- a/Strata/Languages/Laurel/FilterPrelude.lean +++ b/Strata/Languages/Laurel/FilterPrelude.lean @@ -76,7 +76,6 @@ private partial def collectHighTypeNames (ty : HighTypeMd) : CollectM Unit := do | .TMap kt vt => collectHighTypeNames kt; collectHighTypeNames vt | .Applied base args => collectHighTypeNames base; args.forM collectHighTypeNames - | .Pure base => collectHighTypeNames base | .Intersection types => types.forM collectHighTypeNames | .TVoid | .TBool | .TInt | .TFloat64 | .TReal | .TString | .TBv _ | .Unknown | .MultiValuedExpr _ => pure () diff --git a/Strata/Languages/Laurel/Grammar/AbstractToConcreteTreeTranslator.lean b/Strata/Languages/Laurel/Grammar/AbstractToConcreteTreeTranslator.lean index 145c39694f..2dd6e1fba9 100644 --- a/Strata/Languages/Laurel/Grammar/AbstractToConcreteTreeTranslator.lean +++ b/Strata/Languages/Laurel/Grammar/AbstractToConcreteTreeTranslator.lean @@ -55,7 +55,6 @@ partial def highTypeValToArg : HighType → Arg -- Applied types are not directly representable in the grammar; -- emit the base type as a best-effort approximation highTypeToArg base - | .Pure base => highTypeToArg base | .Intersection types => match types with | [] => laurelOp "compositeType" #[ident "Unknown"] diff --git a/Strata/Languages/Laurel/LaurelAST.lean b/Strata/Languages/Laurel/LaurelAST.lean index 1b74656832..f994db65f2 100644 --- a/Strata/Languages/Laurel/LaurelAST.lean +++ b/Strata/Languages/Laurel/LaurelAST.lean @@ -162,8 +162,6 @@ inductive HighType : Type where | UserDefined (name : Identifier) /-- A generic type application, e.g. `List`. -/ | Applied (base : AstNode HighType) (typeArguments : List (AstNode HighType)) - /-- A pure (value) variant of a composite type that uses structural equality instead of reference equality. -/ - | Pure (base : AstNode HighType) /-- An intersection of types. Used for implicit intersection types, e.g. `Scientist & Scandinavian`. -/ | Intersection (types : List (AstNode HighType)) /-- Bitvector type of a given width. -/ @@ -546,7 +544,6 @@ def highEq (a : HighTypeMd) (b : HighTypeMd) : Bool := match _a: a.val, _b: b.va | HighType.TCore s1, HighType.TCore s2 => s1 == s2 | HighType.Applied b1 args1, HighType.Applied b2 args2 => highEq b1 b2 && args1.length == args2.length && (args1.attach.zip args2 |>.all (fun (a1, a2) => highEq a1.1 a2)) - | HighType.Pure b1, HighType.Pure b2 => highEq b1 b2 | HighType.Intersection ts1, HighType.Intersection ts2 => ts1.length == ts2.length && (ts1.attach.zip ts2 |>.all (fun (t1, t2) => highEq t1.1 t2)) | HighType.Unknown, HighType.Unknown => true @@ -640,7 +637,7 @@ def isSubtype (ctx : TypeLattice) (sub sup : HighTypeMd) : Bool := /- ### Variance policy (covers `isSubtype` and `isConsistent`) All child-carrying constructors are INVARIANT by design: `isConsistent` bottoms out in `highEq` (structural equality) for `TSet`, `TMap`, - `Applied`, `Pure`, and `Intersection`. So `TSet Unknown ~ + `Applied`, and `Intersection`. So `TSet Unknown ~ TSet TInt` is FALSE — `Unknown` is a wildcard only at the TOP of a type, never under a constructor. This is intentional: `TSet` / `TMap` are MUTABLE collections, where covariance would be unsound; if you don't know the @@ -652,11 +649,6 @@ def isSubtype (ctx : TypeLattice) (sub sup : HighTypeMd) : Bool := targets, so per-element consistency (letting an `Unknown` output flow into one slot) is correct rather than unsound. - `Pure b` is invariant today, but it is the one constructor where covariance - would be SOUND and desirable — it is the immutable value-view of a composite, - and immutability is exactly the condition that makes covariance safe. - TODO: Pure could be covariant once it matters (immutable value-view ⇒ covariance is sound) - `Applied` (generics) is invariant as the safe default for not-yet-designed parametric types; real variance is per-constructor and deliberately deferred. diff --git a/Strata/Languages/Laurel/Resolution.lean b/Strata/Languages/Laurel/Resolution.lean index d3b8c7ee36..4253a72155 100644 --- a/Strata/Languages/Laurel/Resolution.lean +++ b/Strata/Languages/Laurel/Resolution.lean @@ -360,9 +360,6 @@ def resolveHighType (ty : HighTypeMd) : ResolveM HighTypeMd := do let base' ← resolveHighType base let args' ← args.mapM resolveHighType pure (.Applied base' args') - | .Pure base => - let base' ← resolveHighType base - pure (.Pure base') | .Intersection tys => let tys' ← tys.mapM resolveHighType pure (.Intersection tys') @@ -2794,7 +2791,6 @@ private def collectHighType (map : Std.HashMap Nat ResolvedNode) (ty : HighTypeM | .Applied base args => let map := collectHighType map base args.foldl collectHighType map - | .Pure base => collectHighType map base | .Intersection tys => tys.foldl collectHighType map | .MultiValuedExpr tys => tys.foldl collectHighType map | _ => map diff --git a/Strata/Languages/Laurel/TypeAliasElim.lean b/Strata/Languages/Laurel/TypeAliasElim.lean index 65a3a462e2..62d71e1440 100644 --- a/Strata/Languages/Laurel/TypeAliasElim.lean +++ b/Strata/Languages/Laurel/TypeAliasElim.lean @@ -46,7 +46,6 @@ partial def resolveAliasType (amap : AliasMap) (ty : HighTypeMd) let base' := resolveAliasType amap base visited let args' := args.map (resolveAliasType amap · visited) { val := .Applied base' args', source := ty.source } - | .Pure base => { val := .Pure (resolveAliasType amap base visited), source := ty.source } | .Intersection tys => { val := .Intersection (tys.map (resolveAliasType amap · visited)), source := ty.source } | _ => ty diff --git a/Strata/Languages/Laurel/TypeHierarchy.lean b/Strata/Languages/Laurel/TypeHierarchy.lean index 0414298e6a..a61756e811 100644 --- a/Strata/Languages/Laurel/TypeHierarchy.lean +++ b/Strata/Languages/Laurel/TypeHierarchy.lean @@ -140,7 +140,6 @@ partial def compositeRefToComposite (composites : Std.HashSet String) (ty : High { ty with val := .TMap (compositeRefToComposite composites kt) (compositeRefToComposite composites vt) } | .Applied base args => { ty with val := .Applied (compositeRefToComposite composites base) (args.map (compositeRefToComposite composites ·)) } - | .Pure base => { ty with val := .Pure (compositeRefToComposite composites base) } | .Intersection tys => { ty with val := .Intersection (tys.map (compositeRefToComposite composites ·)) } | _ => ty diff --git a/docs/verso/LaurelDesignGuide.lean b/docs/verso/LaurelDesignGuide.lean index 2afbef7b8b..0be8dd51ba 100644 --- a/docs/verso/LaurelDesignGuide.lean +++ b/docs/verso/LaurelDesignGuide.lean @@ -93,12 +93,6 @@ Legend: the *Laurel* column records Laurel's own status — ✓ implemented, WIP * — * ~ * ✓ - * - * Value (structural) types - * ✓ - * ~ - * — - * ~ * * Runtime type test and cast (`is` / `as`) * ✓ @@ -171,6 +165,12 @@ Legend: the *Laurel* column records Laurel's own status — ✓ implemented, WIP * ✓ * ✓ * — + * + * Assignments in expression positions + * ✓ + * ✓ + * ✓ + * ~ * * Short-circuit boolean operators (`&&` / `||`) * ✓ @@ -206,12 +206,12 @@ Legend: the *Laurel* column records Laurel's own status — ✓ implemented, WIP Notes on the partial (~) entries: - *Multiple supertypes for subtyping* — Laurel's `extending` list lets a type declare several supertypes for `is`/`as` and subtyping. Java gets this from implementing multiple interfaces (and Python from its MRO). JavaScript has only a single prototype chain and no interface concept. - *Multiple implementation inheritance* — this is the stronger form Python needs: inheriting fields and method implementations from several concrete parents, resolved by an MRO. Only Python has it fully; JavaScript relies on ad-hoc mixin patterns, and Java has none (interfaces provide default methods but no fields). -- *Value (structural) types* — Java has records and primitives; Python has frozen dataclasses and tuples; JavaScript has no value objects. - *Arbitrary-precision integers* — only Python has them as the default `int`; Java and JavaScript expose them through a library (`BigInteger`, `BigInt`). - *Fixed-width bitvector operations* — JavaScript's bitwise operators are 32-bit; Python integers are arbitrary width. - *`do`/`while` loops* — Python has none. - *`break` / `continue`* — Laurel does not yet have dedicated `break`/`continue` keywords (WIP). It already provides the more general primitive underneath them: a labelled block `{ … } L` and an `exit L` statement that jumps to the end of that block. `break` is an exit of the block wrapping the loop, and `continue` an exit of the block wrapping the loop body, so the one primitive covers both. On the labelled-exit row, Python has `break`/`continue` without labels. - *Increment / decrement* — Python has no such operators. +- *Assignments in expression positions* — Laurel allows assignments (and other imperative constructs) to appear where an expression is expected, and lifts them out into preceding statements. Java and JavaScript treat assignment as an expression directly. In Python assignments are statements; only the walrus operator `:=` provides a restricted assignment expression. - *Algebraic datatypes / pattern matching* — Java (sealed types + `switch` patterns) and Python (`match`) support a subset; JavaScript has none. - *Exceptions* — Java has checked exceptions; JavaScript and Python have exceptions, but unchecked. From 80b05f6ec317f84e961954537ee3205d5e0de3b4 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Tue, 7 Jul 2026 13:57:12 +0000 Subject: [PATCH 07/20] Add more about type inference --- docs/verso/LaurelDesignGuide.lean | 68 ++++++++++++++++++++++++++++++- 1 file changed, 67 insertions(+), 1 deletion(-) diff --git a/docs/verso/LaurelDesignGuide.lean b/docs/verso/LaurelDesignGuide.lean index 0be8dd51ba..a60bf54955 100644 --- a/docs/verso/LaurelDesignGuide.lean +++ b/docs/verso/LaurelDesignGuide.lean @@ -269,10 +269,76 @@ Constrained types propagating facts through the type system. TODO, add example using polymorphic types, like a wrapping Container that takes a `nat` and we still have the `nat` fact on the other side. -## Implicit conversions +## Type inference + +To be designed.. but here is some subject to change content. + +Laurel can statically infer the types of variables, which, when the inferred types where otherwise not available in the source program, can enable emitting code that can be verified more efficiently. + +Here's an example related to nullable reference types: + +Input program: +``` +var foo := new Foo; +foo.x := 1; + +var bar := foo; +bar := null; +bar.x := 2 +``` + +Without type inference, we can not judge whether the variable `foo` should have type `Foo` or `Nullable`, so we have to pick defensively: +``` +datatype Nullable = from_NotNull(as_notNull: T) | from_Null + +var foo: Nullable := from_NotNull(new Foo); +as_notNull(foo).x := 1; + +var bar: Nullable := foo; +bar := null; +as_notNull(bar).x := 2 +``` + +With type inference, we can infer that `foo` is never nullable: +``` +var foo: Foo := new Foo; +foo.x := 1; + +var bar: Nullable := from_NotNull(foo); +bar := null; +as_notNull(bar).x := 2 +``` + +Note the coercion `from_NotNull` that was inserted in the assignment to `bar`. Laurel can be given a list of coercions that can be inserted automatically. Laurel can also be given a list of type coercions, which it can use to change the type annotations of variables, from for example `T` to `Nullable`. + +## Flow based types + +Flow based types allow the type of a variable to change throughout the control-flow of the program, which enables having more precise types which improves verification performance. + +Source program: +``` +var foo := new Foo; +foo.x := 1; +foo := null; +foo.x := 2; +``` + +Inferred program: +``` +var foo := new Foo; +foo.x := 1; +var foo_2: Nullabe := from_NotNull(foo); +foo_2 := null; +as_notNull(foo_2).x := 2; +``` + +## Inference of composite types To be designed.. +Useful for dynamic languages. Infers composites types based on fields assigned to values. +Composite types perform better than maps because reading from them incurs no domain check. + # Verification without side-effects To support goal 8, for verification code not to affect the outcome of executing the program, Laurel has rules for code that exists only for verification purposes. From db1634b7b79bea31caaf5f714578b9b15227b86c Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Tue, 7 Jul 2026 14:10:17 +0000 Subject: [PATCH 08/20] Add bit about frozen types --- docs/verso/LaurelDesignGuide.lean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/docs/verso/LaurelDesignGuide.lean b/docs/verso/LaurelDesignGuide.lean index a60bf54955..fb38b306ae 100644 --- a/docs/verso/LaurelDesignGuide.lean +++ b/docs/verso/LaurelDesignGuide.lean @@ -257,10 +257,12 @@ TODO, fill in # Automated proof search Goal 6 was enabling the finding of proofs through automated search. -Loop invariants. These enable unbounded symbolic execution +Loop invariants. These enable unbounded symbolic execution. TODO, say more. Reads clauses are useful to improve verification performance. The facts they prove work well together with the facts provided by modifies clauses, making it easier to prove which procedure values have remained unchanged after objects were modified. +Frozen types (To be designed). A reads clause specifies that a procedure always returns the same value, if the reads reference have the same values and if the explicit input arguments, which excludes the heap, are the same. A procedure that returns a newly created object, which has a reference counter that depends on the counter of the input heap, can thus never satisfy a reads clause. For this purpose Laurel allows erasing the counter from a reference value. A Laurel `Frozen` type takes a regular reference type, and produces a type that is the same except that it does not support reference equality or mutation of its fields. + # Use complete algorithms to reduce workload To achieve goal 7, to reduce the verification work through the use of complete algorithms, Laurel has the following features. From edde203c640aed50aa74f101a7e370432fbb9f05 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Tue, 7 Jul 2026 14:15:53 +0000 Subject: [PATCH 09/20] Add record types feature --- docs/verso/LaurelDesignGuide.lean | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/docs/verso/LaurelDesignGuide.lean b/docs/verso/LaurelDesignGuide.lean index fb38b306ae..820194285a 100644 --- a/docs/verso/LaurelDesignGuide.lean +++ b/docs/verso/LaurelDesignGuide.lean @@ -93,6 +93,12 @@ Legend: the *Laurel* column records Laurel's own status — ✓ implemented, WIP * — * ~ * ✓ + * + * Record types (immutable, structural equality) + * WIP + * ✓ + * — + * ~ * * Runtime type test and cast (`is` / `as`) * ✓ @@ -206,6 +212,7 @@ Legend: the *Laurel* column records Laurel's own status — ✓ implemented, WIP Notes on the partial (~) entries: - *Multiple supertypes for subtyping* — Laurel's `extending` list lets a type declare several supertypes for `is`/`as` and subtyping. Java gets this from implementing multiple interfaces (and Python from its MRO). JavaScript has only a single prototype chain and no interface concept. - *Multiple implementation inheritance* — this is the stronger form Python needs: inheriting fields and method implementations from several concrete parents, resolved by an MRO. Only Python has it fully; JavaScript relies on ad-hoc mixin patterns, and Java has none (interfaces provide default methods but no fields). +- *Record types* — an immutable aggregate compared by structural equality. Java has `record`s directly. Python has `@dataclass`/`NamedTuple` (~, library/decorator-based). JavaScript has no record type (the Records & Tuples proposal is not shipped). - *Arbitrary-precision integers* — only Python has them as the default `int`; Java and JavaScript expose them through a library (`BigInteger`, `BigInt`). - *Fixed-width bitvector operations* — JavaScript's bitwise operators are 32-bit; Python integers are arbitrary width. - *`do`/`while` loops* — Python has none. From d92762722094eb20a0286ad310c1f8d6152d6dd4 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Tue, 7 Jul 2026 14:16:21 +0000 Subject: [PATCH 10/20] Add sentence about frozen vs record types --- docs/verso/LaurelDesignGuide.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/verso/LaurelDesignGuide.lean b/docs/verso/LaurelDesignGuide.lean index 820194285a..6b055f4301 100644 --- a/docs/verso/LaurelDesignGuide.lean +++ b/docs/verso/LaurelDesignGuide.lean @@ -268,7 +268,7 @@ Loop invariants. These enable unbounded symbolic execution. TODO, say more. Reads clauses are useful to improve verification performance. The facts they prove work well together with the facts provided by modifies clauses, making it easier to prove which procedure values have remained unchanged after objects were modified. -Frozen types (To be designed). A reads clause specifies that a procedure always returns the same value, if the reads reference have the same values and if the explicit input arguments, which excludes the heap, are the same. A procedure that returns a newly created object, which has a reference counter that depends on the counter of the input heap, can thus never satisfy a reads clause. For this purpose Laurel allows erasing the counter from a reference value. A Laurel `Frozen` type takes a regular reference type, and produces a type that is the same except that it does not support reference equality or mutation of its fields. +Frozen types (To be designed). A reads clause specifies that a procedure always returns the same value, if the reads reference have the same values and if the explicit input arguments, which excludes the heap, are the same. A procedure that returns a newly created object, which has a reference counter that depends on the counter of the input heap, can thus never satisfy a reads clause. For this purpose Laurel allows erasing the counter from a reference value. A Laurel `Frozen` type takes a regular reference type, and produces a type that is the same except that it does not support reference equality or mutation of its fields. Record types are composite types that are frozen by default. # Use complete algorithms to reduce workload To achieve goal 7, to reduce the verification work through the use of complete algorithms, Laurel has the following features. From 2430e6ecdf0bea8dfb621b73ab033e898e0b7b77 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Tue, 7 Jul 2026 14:28:38 +0000 Subject: [PATCH 11/20] Improves --- docs/verso/LaurelDesignGuide.lean | 50 +++++++++++++++++++++++++++---- 1 file changed, 44 insertions(+), 6 deletions(-) diff --git a/docs/verso/LaurelDesignGuide.lean b/docs/verso/LaurelDesignGuide.lean index 6b055f4301..49d2652ded 100644 --- a/docs/verso/LaurelDesignGuide.lean +++ b/docs/verso/LaurelDesignGuide.lean @@ -41,7 +41,7 @@ Goals: 1. property based testing 2. data-flow analysis 3. symbolic execution (aka verification), both bounded and unbounded -2. Reduce code duplication in the analysis of popular languages by being a target for compilation from those languages, and including features common to them. Note that we expect source languages to reduce their existing compilers when possible, so language features that can be compiled away don't need to be considered. +2. Reduce code duplication in the analysis of popular languages by being a target for compilation from those languages, and including features common to them. Note that we expect source languages to reuse their existing compilers when possible, so language features that can be compiled away don't need to be considered. 3. Have a great user experience 4. Enable modular verification 5. Minimize the amount of user code needed to enable verification. @@ -207,6 +207,30 @@ Legend: the *Laurel* column records Laurel's own status — ✓ implemented, WIP * ✓ * — * ~ + * + * Reflection / runtime metaprogramming (dynamic field/method or prototype mutation) + * ✗ + * ✓ + * ✓ + * ✓ + * + * `eval` / dynamic code loading + * ✗ + * ~ + * ✓ + * ✓ + * + * Shared-memory concurrency (threads, locks, memory model) + * WIP + * ✓ + * ~ + * ✓ + * + * Garbage-collection observability (finalizers, weak references) + * ✗ + * ✓ + * ✓ + * ✓ ::: Notes on the partial (~) entries: @@ -222,6 +246,13 @@ Notes on the partial (~) entries: - *Algebraic datatypes / pattern matching* — Java (sealed types + `switch` patterns) and Python (`match`) support a subset; JavaScript has none. - *Exceptions* — Java has checked exceptions; JavaScript and Python have exceptions, but unchecked. +Notes on the not-planned (✗) entries. These are features that survive the source language's own compilation (they are not mere syntactic sugar) yet Laurel deliberately does not model, because they cannot be lowered into static Laurel constructs without either embedding a runtime interpreter or losing soundness, and they are fundamentally at odds with modular static verification. +- *Reflection / runtime metaprogramming* — all three source languages allow a program to inspect and rewrite its own structure at runtime: Java through `java.lang.reflect` and dynamic proxies, Python through `getattr`/`setattr`, `__dict__` mutation, metaclasses, and monkey-patching, and JavaScript through `Proxy`/`Reflect` and prototype mutation (`Object.setPrototypeOf`). Laurel's static and flow-based typing, and its inference of composite types from a fixed set of assigned fields, assume the set of fields and methods of a type is known statically, so arbitrary self-modification is out of scope. +- *`eval` / dynamic code loading* — code that does not exist until runtime cannot be verified ahead of time. Python (`eval`/`exec`) and JavaScript (`eval`) have it directly; Java exposes it more indirectly through scripting and dynamic class loading (~). +- *Garbage-collection observability* — finalizers and weak references (Java `finalize`/`WeakReference`, Python `__del__`/`weakref`, JavaScript `WeakRef`/`FinalizationRegistry`) expose the nondeterministic timing of collection. Laurel models the heap abstractly and does not expose when, or whether, an object is collected. + +Note on the *shared-memory concurrency* entry (WIP): Java has real shared-memory threads governed by the Java Memory Model (`synchronized`, `volatile`, happens-before); Python has threads under the GIL (✓); JavaScript is single-threaded and only achieves parallelism through workers that communicate by message passing (~). Laurel is currently sequential, and reasoning under a relaxed memory model is a large, separable piece of work, so this is planned rather than available. + # Modular Verification To achieve goal (4), Laurel has the following features related to modular verification. @@ -237,7 +268,7 @@ Since modifies clauses are a type of postcondition, they are also only allowed o To achieve goal (5), minimize the amount of user code needed to enable verification, Laurel has the following features: ## Transparent procedures -Laurel procedures are transparent by default, meaning that a call can use the body of the callee to prove facts about the result of the call. Laurel will allow any procedure to be transparent, although currently there are some restrictions. In particular, Laurel will allow procedures that contains loops or that modify the heap, to be transparent as well. +Laurel procedures are transparent by default, meaning that a call can use the body of the callee to prove facts about the result of the call. Laurel will allow any procedure to be transparent, although currently there are some restrictions. In particular, Laurel will allow procedures that contain loops or that modify the heap, to be transparent as well. By allowing any procedure to be transparent, Laurel prevents users from having to repeat the body of a procedure in a postcondition. Here's an example that shows an opaque procedure that would have been easier to define as being transparent, without any loss of readability: @@ -264,11 +295,16 @@ TODO, fill in # Automated proof search Goal 6 was enabling the finding of proofs through automated search. -Loop invariants. These enable unbounded symbolic execution. TODO, say more. +## Loop invariants +These enable unbounded symbolic execution. TODO, say more. +## Reads clauses Reads clauses are useful to improve verification performance. The facts they prove work well together with the facts provided by modifies clauses, making it easier to prove which procedure values have remained unchanged after objects were modified. -Frozen types (To be designed). A reads clause specifies that a procedure always returns the same value, if the reads reference have the same values and if the explicit input arguments, which excludes the heap, are the same. A procedure that returns a newly created object, which has a reference counter that depends on the counter of the input heap, can thus never satisfy a reads clause. For this purpose Laurel allows erasing the counter from a reference value. A Laurel `Frozen` type takes a regular reference type, and produces a type that is the same except that it does not support reference equality or mutation of its fields. Record types are composite types that are frozen by default. +## Frozen types +Frozen types (To be designed). A reads clause specifies that a procedure always returns the same value, if the reads references have the same values and if the explicit input arguments, which excludes the heap, are the same. A procedure that returns a newly created object, which has a reference counter that depends on the counter of the input heap, can thus never satisfy a reads clause. For this purpose Laurel allows erasing the counter from a reference value. A Laurel `Frozen` type takes a regular reference type, and produces a type that is the same except that it does not support reference equality or mutation of its fields. Record types are composite types that are frozen by default. + +TODO, add example with a `record Tuple..` and a `composite MutableTuple` and a `Frozen` that are all three created in and returned from different procedures that each have an empty reads clause. Returning the `MutableTuple` fails to prove the reads clause. # Use complete algorithms to reduce workload To achieve goal 7, to reduce the verification work through the use of complete algorithms, Laurel has the following features. @@ -336,7 +372,7 @@ Inferred program: ``` var foo := new Foo; foo.x := 1; -var foo_2: Nullabe := from_NotNull(foo); +var foo_2: Nullable := from_NotNull(foo); foo_2 := null; as_notNull(foo_2).x := 2; ``` @@ -352,10 +388,12 @@ Composite types perform better than maps because reading from them incurs no dom To support goal 8, for verification code not to affect the outcome of executing the program, Laurel has rules for code that exists only for verification purposes. -TODO, Rules for contracts: +Rules for contracts: - Contract code may not modify variables defined outside the contract scope. - Contract code has an empty modifies clause. Contract code operates on a copy of the heap. +TODO, add examples + # Great user experience ## Parameter lists From fe7d2b0fbefc791d60f7404718755fe32efc46a4 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Tue, 7 Jul 2026 16:32:00 +0000 Subject: [PATCH 12/20] Fixes --- docs/verso/LaurelDesignGuide.lean | 52 +++++++++++++++++-------------- 1 file changed, 29 insertions(+), 23 deletions(-) diff --git a/docs/verso/LaurelDesignGuide.lean b/docs/verso/LaurelDesignGuide.lean index 49d2652ded..8f8e09c0c3 100644 --- a/docs/verso/LaurelDesignGuide.lean +++ b/docs/verso/LaurelDesignGuide.lean @@ -39,23 +39,32 @@ Laurel tries to include any features that are common to those three languages. Goals: 1. Enable proving both correctness and incorrectness properties of software, through a combination of: 1. property based testing - 2. data-flow analysis - 3. symbolic execution (aka verification), both bounded and unbounded + 2. symbolic execution (aka verification), both bounded and unbounded + 3. data-flow analysis 2. Reduce code duplication in the analysis of popular languages by being a target for compilation from those languages, and including features common to them. Note that we expect source languages to reuse their existing compilers when possible, so language features that can be compiled away don't need to be considered. -3. Have a great user experience -4. Enable modular verification -5. Minimize the amount of user code needed to enable verification. -6. Enable finding proofs through an automated search. -7. Use complete analysis algorithms to reduce the required proof effort. -8. Code used to enable verification may not affect execution behavior. - -# Enable Verification -To achieve goal 1.3, enable proving properties through verification, Laurel has the following features. +3. Enable modular verification +4. Minimize the amount of user code needed to enable verification. +5. Enable finding proofs through an automated search. +6. Use complete analysis algorithms to reduce the required proof effort. +7. Code used to enable verification may not affect execution behavior. +8. Have a great user experience + +# Correctness checking features + +## Property-based testing +To be designed.. + +## Verification +To achieve goal 1.2, enable proving properties through verification, Laurel has the following features. - Assertions - Quantifiers -- Old/allocated/fresh -- Decreases clauses -- Assumptions (more about gradual verification) +- Old/allocated/fresh (what's allocated for?) +- Decreases clauses (relates to soundness and ghost-code as well) +- Assumptions (more about gradual verification. what about bodiless procedures?) + +## Unbounded verification +Loop invariants. +These enable unbounded symbolic execution. TODO, say more. # Prevent duplicate work To achieve goal (2), reduce code duplication in the analysis of popular languages, Laurel contains many features shared between several languages. The following table shows which features are shared with which input languages. @@ -254,7 +263,7 @@ Notes on the not-planned (✗) entries. These are features that survive the sour Note on the *shared-memory concurrency* entry (WIP): Java has real shared-memory threads governed by the Java Memory Model (`synchronized`, `volatile`, happens-before); Python has threads under the GIL (✓); JavaScript is single-threaded and only achieves parallelism through workers that communicate by message passing (~). Laurel is currently sequential, and reasoning under a relaxed memory model is a large, separable piece of work, so this is planned rather than available. # Modular Verification -To achieve goal (4), Laurel has the following features related to modular verification. +To achieve goal (3), Laurel has the following features related to modular verification. ## Preconditions Preconditions enable proving the assertions in a procedure's body without having to consider the callers. This way, each assertion only needs to be proven once, instead of once for each transitive call-site. @@ -265,10 +274,10 @@ Laurel allows a procedure to be marked as opaque, which means that callers won't Since modifies clauses are a type of postcondition, they are also only allowed on opaque procedures. # Minimize Verification Code -To achieve goal (5), minimize the amount of user code needed to enable verification, Laurel has the following features: +To achieve goal (4), minimize the amount of user code needed to enable verification, Laurel has the following features: ## Transparent procedures -Laurel procedures are transparent by default, meaning that a call can use the body of the callee to prove facts about the result of the call. Laurel will allow any procedure to be transparent, although currently there are some restrictions. In particular, Laurel will allow procedures that contain loops or that modify the heap, to be transparent as well. +Laurel procedures are transparent by default, meaning that a call can use the body of the callee to prove facts about the result of the call. Laurel aims to allow any procedure to be transparent; some restrictions still remain for now. In particular, Laurel will allow procedures that contain loops or that modify the heap to be transparent as well. By allowing any procedure to be transparent, Laurel prevents users from having to repeat the body of a procedure in a postcondition. Here's an example that shows an opaque procedure that would have been easier to define as being transparent, without any loss of readability: @@ -293,10 +302,7 @@ A second reason for not allowing any heap modification inside contracts is that TODO, fill in # Automated proof search -Goal 6 was enabling the finding of proofs through automated search. - -## Loop invariants -These enable unbounded symbolic execution. TODO, say more. +Goal 5 was enabling the finding of proofs through automated search. ## Reads clauses Reads clauses are useful to improve verification performance. The facts they prove work well together with the facts provided by modifies clauses, making it easier to prove which procedure values have remained unchanged after objects were modified. @@ -307,7 +313,7 @@ Frozen types (To be designed). A reads clause specifies that a procedure always TODO, add example with a `record Tuple..` and a `composite MutableTuple` and a `Frozen` that are all three created in and returned from different procedures that each have an empty reads clause. Returning the `MutableTuple` fails to prove the reads clause. # Use complete algorithms to reduce workload -To achieve goal 7, to reduce the verification work through the use of complete algorithms, Laurel has the following features. +To achieve goal 6, to reduce the verification work through the use of complete algorithms, Laurel has the following features. ## Constrained types Constrained types propagating facts through the type system. @@ -386,7 +392,7 @@ Composite types perform better than maps because reading from them incurs no dom # Verification without side-effects -To support goal 8, for verification code not to affect the outcome of executing the program, Laurel has rules for code that exists only for verification purposes. +To support goal 7, for verification code not to affect the outcome of executing the program, Laurel has rules for code that exists only for verification purposes. Rules for contracts: - Contract code may not modify variables defined outside the contract scope. From 910d6402e4311600fd6bd03f4589e429ff62c9b5 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Tue, 7 Jul 2026 18:34:31 +0000 Subject: [PATCH 13/20] Fill in TODO sections --- docs/verso/LaurelDesignGuide.lean | 93 ++++++++++++++++++++++++++++--- 1 file changed, 86 insertions(+), 7 deletions(-) diff --git a/docs/verso/LaurelDesignGuide.lean b/docs/verso/LaurelDesignGuide.lean index 8f8e09c0c3..7885660a53 100644 --- a/docs/verso/LaurelDesignGuide.lean +++ b/docs/verso/LaurelDesignGuide.lean @@ -63,8 +63,29 @@ To achieve goal 1.2, enable proving properties through verification, Laurel has - Assumptions (more about gradual verification. what about bodiless procedures?) ## Unbounded verification -Loop invariants. -These enable unbounded symbolic execution. TODO, say more. +Bounded symbolic execution unrolls a loop a fixed number of times, so on its own it cannot prove a property for every run of a loop whose iteration count is not statically known. Loop invariants close that gap. A `while` loop may carry one or more `invariant` clauses, each an expression that must hold when the loop is first reached and be preserved by every iteration. + +``` +procedure countUp() +{ + var n: int := 5; + var i: int := 0; + while (i < n) + invariant i >= 0 + invariant i <= n + { + i := i + 1 + }; + assert i == n +}; +``` + +The invariants let Laurel replace the loop with three obligations that stand in for it no matter how many times it runs: +1. the invariants hold on entry to the loop; +2. assuming the invariants and the guard, one iteration of the body re-establishes the invariants; +3. after the loop, the invariants together with the negation of the guard may be assumed. + +None of these obligations mentions a concrete iteration count, so an invariant strong enough to imply the property discharges it for an unbounded loop. Each invariant is checked independently and reports a failure against its own source range, so a diagnostic points at the specific invariant that does not hold rather than at the whole loop. # Prevent duplicate work To achieve goal (2), reduce code duplication in the analysis of popular languages, Laurel contains many features shared between several languages. The following table shows which features are shared with which input languages. @@ -298,8 +319,20 @@ A common design choice in verification-aware programming languages is not to all A second reason for not allowing any heap modification inside contracts is that this is prone to soundness issues. From outside the contract the heap is assumed not to be modified, so if knowledge of an inside modification escapes the contract, this leads to an inconsistency. Because Laurel does not allow assigning to variable defined outside the contract, from inside the contract, no modification can escape the contract. The heap used inside a contract is a separate heap variable. ## Invoke on +The postcondition of an opaque procedure is exposed to callers as an axiom: the ensures clause, universally quantified over the procedure's inputs. Left unrestricted, the solver may instantiate such an axiom on any matching term, which is a common cause of slow and unpredictable verification. -TODO, fill in +An `invokeOn` clause names the SMT trigger for that axiom. It takes an expression over the procedure's inputs, and the axiom is only instantiated when a term matching that expression appears in the proof context. + +``` +procedure PAndQ(x: int) + invokeOn P(x) + opaque + ensures P(x) && Q(x); +``` + +This emits the axiom `forall x. {P(x)} P(x) && Q(x)`, triggered on `P(x)`. An obligation that mentions `P(x)` pulls in `P(x) && Q(x)`, so it can establish both `P(x)` and `Q(x)`. An obligation that mentions only `Q(x)` does not match the trigger, so the axiom stays dormant and `Q(x)` is not proved. The trigger controls *when* the fact is instantiated, but not *where*: the axiom is emitted at the top level of the program, so once a matching term appears the fact becomes available to every proof obligation in the program, not just to a particular caller or region. + +This global availability is a deliberate simplification for the first version of the feature. It is enough to make an opaque procedure's postcondition usable, but it gives no control over scope: a fact intended for one caller is visible everywhere its trigger matches, which can slow down or perturb unrelated proofs. `invokeOn` is expected to evolve toward finer-grained control over where facts are made available — for example scoping a fact to specific callers, modules, or call sites — so that authors can expose a postcondition exactly where it is useful rather than program-wide. # Automated proof search Goal 5 was enabling the finding of proofs through automated search. @@ -310,15 +343,49 @@ Reads clauses are useful to improve verification performance. The facts they pro ## Frozen types Frozen types (To be designed). A reads clause specifies that a procedure always returns the same value, if the reads references have the same values and if the explicit input arguments, which excludes the heap, are the same. A procedure that returns a newly created object, which has a reference counter that depends on the counter of the input heap, can thus never satisfy a reads clause. For this purpose Laurel allows erasing the counter from a reference value. A Laurel `Frozen` type takes a regular reference type, and produces a type that is the same except that it does not support reference equality or mutation of its fields. Record types are composite types that are frozen by default. -TODO, add example with a `record Tuple..` and a `composite MutableTuple` and a `Frozen` that are all three created in and returned from different procedures that each have an empty reads clause. Returning the `MutableTuple` fails to prove the reads clause. +The following sketch (syntax illustrative — reads clauses, records, and `Frozen` are still being designed) shows why the erasure matters. Each procedure declares an empty reads clause, claiming its result depends on nothing in the heap: + +``` +record Tuple { var fst: int; var snd: int } +composite MutableTuple { var fst: int; var snd: int } + +procedure makeRecord() reads {} returns (r: Tuple) +{ return Tuple(1, 2) }; // ok: records are frozen, no reference identity + +procedure makeFrozen() reads {} returns (r: Frozen) +{ ... }; // ok: the counter is erased, so the result is heap-independent + +procedure makeMutable() reads {} returns (r: MutableTuple) +// ^^^^^^^^ fails: the new object's identity depends on the heap counter +{ return new MutableTuple(1, 2) }; +``` + +`makeRecord` and `makeFrozen` satisfy the empty reads clause because neither result carries a heap-dependent reference counter, so calling either twice with the same inputs yields equal results. `makeMutable` returns a fresh `MutableTuple` whose reference identity is drawn from the heap's allocation counter, so its result differs between calls and cannot satisfy an empty reads clause. # Use complete algorithms to reduce workload To achieve goal 6, to reduce the verification work through the use of complete algorithms, Laurel has the following features. ## Constrained types -Constrained types propagating facts through the type system. +A constrained type refines an existing type with a predicate, so that a fact established once travels through the program as part of the type instead of being re-proved at each use. It is declared with a base type, a `where` predicate, and a `witness` value that shows the constraint is inhabited. + +``` +constrained nat = x: int where x >= 0 witness 0 +``` -TODO, add example using polymorphic types, like a wrapping Container that takes a `nat` and we still have the `nat` fact on the other side. +The property that matters for reducing proof effort is that the fact survives flow through code that knows nothing about it. Consider a polymorphic `identity`, which returns its argument unchanged for any type `T`: + +``` +// syntax illustrative — generics are still in progress +procedure identity(x: T) returns (r: T) { return x }; + +procedure usesIdentity() { + var n: nat := 5; + var m: nat := identity(n); + assert m >= 0 // still available: the `nat` constraint survived the round-trip +}; +``` + +`identity` is verified once, generically, with no knowledge of `nat` or its predicate. Yet because the constraint rides along with the type, instantiating `T` with `nat` lets the caller recover `m >= 0` on the result with no extra annotation or proof at the call site. The fact is neither dropped when the value enters the generic procedure nor re-derived when it leaves. That is what lets constrained types cut proof effort across a whole program: a property proved at one point remains available everywhere the constrained value flows, even through procedures that are entirely agnostic to the constraint. ## Type inference @@ -398,7 +465,19 @@ Rules for contracts: - Contract code may not modify variables defined outside the contract scope. - Contract code has an empty modifies clause. Contract code operates on a copy of the heap. -TODO, add examples +For example, the body of the procedure below changes `p`, and that effect is declared with `modifies p`; `old(p.x)` in the ensures clause refers to the pre-state: + +``` +procedure shift(p: Point, dx: int) + opaque + ensures p.x == old(p.x) + dx + modifies p +{ + p.x := p.x + dx +}; +``` + +The ensures expression may read the heap and build temporary values while it is evaluated, but it cannot assign to `p`, to `dx`, or to any variable declared outside it, and it contributes no modifies effect of its own. Even if the postcondition called a helper that allocated and mutated a scratch object, that would run against a copy of the heap and remain invisible to callers, which still see every pre-existing object unchanged across the evaluation of the contract. As a result, adding, strengthening, or removing the ensures clause never changes how the program executes. # Great user experience From a0e1a57b952e4a0fd6e5b7b7fd9dd99b86059dc1 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 8 Jul 2026 13:35:45 +0000 Subject: [PATCH 14/20] Small changes --- docs/verso/LaurelDesignGuide.lean | 43 ++++++++++++++++++++++++------- 1 file changed, 33 insertions(+), 10 deletions(-) diff --git a/docs/verso/LaurelDesignGuide.lean b/docs/verso/LaurelDesignGuide.lean index 7885660a53..8ed20d5264 100644 --- a/docs/verso/LaurelDesignGuide.lean +++ b/docs/verso/LaurelDesignGuide.lean @@ -38,15 +38,16 @@ Laurel tries to include any features that are common to those three languages. Goals: 1. Enable proving both correctness and incorrectness properties of software, through a combination of: - 1. property based testing - 2. symbolic execution (aka verification), both bounded and unbounded - 3. data-flow analysis + 1. Property based testing + 2. Symbolic execution (aka verification), both bounded and unbounded + 3. Hybrid concrete and symbolic property checking + 3. Data-flow analysis 2. Reduce code duplication in the analysis of popular languages by being a target for compilation from those languages, and including features common to them. Note that we expect source languages to reuse their existing compilers when possible, so language features that can be compiled away don't need to be considered. 3. Enable modular verification 4. Minimize the amount of user code needed to enable verification. 5. Enable finding proofs through an automated search. 6. Use complete analysis algorithms to reduce the required proof effort. -7. Code used to enable verification may not affect execution behavior. +7. Verification must be erasable. Removing verification code may not affect execution behavior. 8. Have a great user experience # Correctness checking features @@ -55,12 +56,13 @@ Goals: To be designed.. ## Verification +Work in progress section + To achieve goal 1.2, enable proving properties through verification, Laurel has the following features. -- Assertions -- Quantifiers -- Old/allocated/fresh (what's allocated for?) -- Decreases clauses (relates to soundness and ghost-code as well) -- Assumptions (more about gradual verification. what about bodiless procedures?) +- Assertions (TODO: add some explanation of what assert enables, including an example.) +- Postconditions (TODO: add some explanation. Explain how a postcondition is usually where we want to put assertions, so we can think in terms of entire procedures) +- Quantifiers (TODO: also relate universal quantifier to soundness mode checking on procedures, and existential quantifier to bug finding mode) +- Old (TODO: explain how old can be use to express mutation using mutation free code) ## Unbounded verification Bounded symbolic execution unrolls a loop a fixed number of times, so on its own it cannot prove a property for every run of a loop whose iteration count is not statically known. Loop invariants close that gap. A `while` loop may carry one or more `invariant` clauses, each an expression that must hold when the loop is first reached and be preserved by every iteration. @@ -87,6 +89,17 @@ The invariants let Laurel replace the loop with three obligations that stand in None of these obligations mentions a concrete iteration count, so an invariant strong enough to imply the property discharges it for an unbounded loop. Each invariant is checked independently and reports a failure against its own source range, so a diagnostic points at the specific invariant that does not hold rather than at the whole loop. +## Hybrid property checking +Laurel allows bypassing the symbolic checking of properties in various ways: +- Assumptions +- Bodyless procedures + +By bypassing the symbolic check, a concrete can check (property-based testing) can be used instead. How exactly Laurel will guarantee a correct hand-off between concrete and symbolic property checking, is yet to be designed. + +## Data-flow analysis + +To be designed.. + # Prevent duplicate work To achieve goal (2), reduce code duplication in the analysis of popular languages, Laurel contains many features shared between several languages. The following table shows which features are shared with which input languages. @@ -334,6 +347,12 @@ This emits the axiom `forall x. {P(x)} P(x) && Q(x)`, triggered on `P(x)`. An ob This global availability is a deliberate simplification for the first version of the feature. It is enough to make an opaque procedure's postcondition usable, but it gives no control over scope: a fact intended for one caller is visible everywhere its trigger matches, which can slow down or perturb unrelated proofs. `invokeOn` is expected to evolve toward finer-grained control over where facts are made available — for example scoping a fact to specific callers, modules, or call sites — so that authors can expose a postcondition exactly where it is useful rather than program-wide. +## Aliasing + +Potential aliasing of heap allocated objects makes can make verification more complicated. Laurel introduced the `allocated` and `fresh` concepts that make it easier to specify which references are disjunct. + + + # Automated proof search Goal 5 was enabling the finding of proofs through automated search. @@ -457,13 +476,14 @@ To be designed.. Useful for dynamic languages. Infers composites types based on fields assigned to values. Composite types perform better than maps because reading from them incurs no domain check. -# Verification without side-effects +# Verification code must be erasable To support goal 7, for verification code not to affect the outcome of executing the program, Laurel has rules for code that exists only for verification purposes. Rules for contracts: - Contract code may not modify variables defined outside the contract scope. - Contract code has an empty modifies clause. Contract code operates on a copy of the heap. +- Contract code must terminate, so removing it does not whether execution code is reachable or not. For example, the body of the procedure below changes `p`, and that effect is declared with `modifies p`; `old(p.x)` in the ensures clause refers to the pre-state: @@ -479,6 +499,9 @@ procedure shift(p: Point, dx: int) The ensures expression may read the heap and build temporary values while it is evaluated, but it cannot assign to `p`, to `dx`, or to any variable declared outside it, and it contributes no modifies effect of its own. Even if the postcondition called a helper that allocated and mutated a scratch object, that would run against a copy of the heap and remain invisible to callers, which still see every pre-existing object unchanged across the evaluation of the contract. As a result, adding, strengthening, or removing the ensures clause never changes how the program executes. +## Decreases clauses +To enable proving that contracts terminate, Laurel uses decreasing clauses to enable proving the termination of procedure calls. + # Great user experience ## Parameter lists From df9539382547a37faeea5f13a08e7cf2ea8f60f6 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 8 Jul 2026 13:58:45 +0000 Subject: [PATCH 15/20] Resolve TODOs --- docs/verso/LaurelDesignGuide.lean | 59 ++++++++++++++++++++--- docs/verso/LaurelImplementationGuide.lean | 7 ++- 2 files changed, 59 insertions(+), 7 deletions(-) diff --git a/docs/verso/LaurelDesignGuide.lean b/docs/verso/LaurelDesignGuide.lean index 8ed20d5264..0cf3bfffe1 100644 --- a/docs/verso/LaurelDesignGuide.lean +++ b/docs/verso/LaurelDesignGuide.lean @@ -59,10 +59,53 @@ To be designed.. Work in progress section To achieve goal 1.2, enable proving properties through verification, Laurel has the following features. -- Assertions (TODO: add some explanation of what assert enables, including an example.) -- Postconditions (TODO: add some explanation. Explain how a postcondition is usually where we want to put assertions, so we can think in terms of entire procedures) -- Quantifiers (TODO: also relate universal quantifier to soundness mode checking on procedures, and existential quantifier to bug finding mode) -- Old (TODO: explain how old can be use to express mutation using mutation free code) + +### Assertions +An `assert` states a property that must hold at the point where it appears. An assertion is the basic unit of proof: everything else in this section is a way of making the facts an assertion needs available, or of stating such properties more conveniently. + +``` +procedure abs(x: int) returns (r: int) +{ + if x < 0 then { r := -x } else { r := x }; + assert r >= 0 +}; +``` + +Here the assertion holds on both branches, so it is discharged; had a branch left `r` negative, the assertion would report a failure. + +### Quantifiers +Laurel supports universal (`forall`) and existential (`exists`) quantifiers in properties, written `forall(x: T) => P(x)` and `exists(x: T) => P(x)`. They let a single property range over unboundedly many values. + +``` +procedure allNonNegativeSquares() + opaque +{ + assert forall(x: int) => x * x >= 0 +}; + +procedure someMultipleOf42() + opaque +{ + assert exists(x: int) => x == 42 +}; +``` + +The two quantifiers correspond to the two analysis modes. A universal quantifier is what soundness (correctness) checking needs: to prove a procedure correct, its properties must hold for *all* inputs and *all* reachable states, so proving a `forall` establishes the property for every case. An existential quantifier fits bug finding (incorrectness) mode: exhibiting *some* state that satisfies a property is enough to witness that a situation is reachable, for example a state that violates an intended invariant. Because unrestricted quantifier instantiation is a common cause of slow verification, a `forall` may carry an explicit trigger, written `forall(i: int) { P(i) } => …`, that tells the solver which terms may instantiate it. + +### Old +In a postcondition, `old(e)` denotes the value of the expression `e` in the procedure's pre-state, before the body ran. This lets a contract relate the final state to the initial one, which is how mutation is specified. The specification is written in a mutation-free style: `old` and the current value are both just expressions, and comparing them describes the effect of the mutation without the contract itself performing any mutation. + +``` +procedure increment(counter: Counter) + opaque + ensures counter.value == old(counter.value) + 1 + modifies counter +{ + counter.value := counter.value + 1 +}; +``` + +The postcondition `counter.value == old(counter.value) + 1` captures the mutation performed by the body, yet it is a pure comparison between two values. A caller learns exactly how the field changed relative to its prior value without the contract mutating anything, keeping verification code erasable (see goal 7). ## Unbounded verification Bounded symbolic execution unrolls a loop a fixed number of times, so on its own it cannot prove a property for every run of a loop whose iteration count is not statically known. Loop invariants close that gap. A `while` loop may carry one or more `invariant` clauses, each an expression that must hold when the loop is first reached and be preserved by every iteration. @@ -302,8 +345,12 @@ To achieve goal (3), Laurel has the following features related to modular verifi ## Preconditions Preconditions enable proving the assertions in a procedure's body without having to consider the callers. This way, each assertion only needs to be proven once, instead of once for each transitive call-site. -## Opaque procedures -Laurel allows a procedure to be marked as opaque, which means that callers won't get access to the body of the procedure. Laurel only allows postconditions for opaque procedures. This restriction is because a postcondition can only contain information that can also be inferred from the body, and redundant information is bad for verification performance. +## Postconditions and opaque procedures +Laurel allows a procedure to be marked as opaque, which means that callers won't get access to the body of the procedure. Once a procedure is opaque, Laurel allows defining postconditions for it. The postconditions will remain available to the caller. Postcondition and opaque bodies allow encapsulating the body of a procedure, making it easier to reason about by callers. + +Laurel does not allow postconditions on procedures with transparent bodies, because a postcondition can only contain information that can also be inferred from the body, and redundant information is bad for verification performance. + +For proving properties on top of a procedure's body or postconditions, define a separate procedure that calls the target one. Since modifies clauses are a type of postcondition, they are also only allowed on opaque procedures. diff --git a/docs/verso/LaurelImplementationGuide.lean b/docs/verso/LaurelImplementationGuide.lean index be60bb235d..7092e0934a 100644 --- a/docs/verso/LaurelImplementationGuide.lean +++ b/docs/verso/LaurelImplementationGuide.lean @@ -110,7 +110,12 @@ shortTitle := "Laurel Implementation" # Language definition The Laurel language definitions consists of its type, its grammar and its semantics. Currently the semantics is split into a static part, called the resolver, and a dynamic part. -TODO map the different parts of the language definition to the files that implement them. +The parts of the language definition map onto the implementation files as follows: + +- *Type* — `LaurelAST.lean` defines the Laurel AST, including the program structure (`StmtExpr`, declarations, procedures) and the type language (`HighType`). `LaurelTypes.lean` computes the `HighType` of an expression from these annotations, and `TypeHierarchy.lean` captures the subtyping relation between user-defined types. +- *Grammar* — `Grammar/LaurelGrammar.st` is the DDM dialect that defines Laurel's concrete syntax; it is loaded into Lean by `Grammar/LaurelGrammar.lean`. `Grammar/ConcreteToAbstractTreeTranslator.lean` turns the parsed concrete tree into the `LaurelAST` type, and `Grammar/AbstractToConcreteTreeTranslator.lean` goes the other way to render an AST back to concrete syntax. +- *Static semantics (resolver)* — `Resolution.lean` resolves references and type checks the program, producing diagnostics and a `SemanticModel` (defined in `SemanticModel.lean`) that links references to their definitions. +- *Dynamic semantics* — Laurel has no standalone interpreter; its runtime meaning is given operationally by the compilation to Core described below. The pass files under `Strata/Languages/Laurel/` and the pipeline in `LaurelCompilationPipeline.lean` therefore constitute the dynamic semantics, delegating to Core's own execution and verification semantics. ## Resolution The static semantics of Laurel are defined by `Resolution.lean`. This is where Laurel references are resolved and where type checking is done. Calling `resolve` will produce diagnostics and a `SemanticModel` that can be used to navigate between definitions and references. From 33149298e68fbd422002dfac682854baf07bbd99 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 9 Jul 2026 08:13:22 +0000 Subject: [PATCH 16/20] Typos --- docs/verso/LaurelDesignGuide.lean | 41 ++++++++++++++++++++++--------- 1 file changed, 29 insertions(+), 12 deletions(-) diff --git a/docs/verso/LaurelDesignGuide.lean b/docs/verso/LaurelDesignGuide.lean index 0cf3bfffe1..522a137292 100644 --- a/docs/verso/LaurelDesignGuide.lean +++ b/docs/verso/LaurelDesignGuide.lean @@ -41,7 +41,7 @@ Goals: 1. Property based testing 2. Symbolic execution (aka verification), both bounded and unbounded 3. Hybrid concrete and symbolic property checking - 3. Data-flow analysis + 4. Data-flow analysis 2. Reduce code duplication in the analysis of popular languages by being a target for compilation from those languages, and including features common to them. Note that we expect source languages to reuse their existing compilers when possible, so language features that can be compiled away don't need to be considered. 3. Enable modular verification 4. Minimize the amount of user code needed to enable verification. @@ -137,7 +137,7 @@ Laurel allows bypassing the symbolic checking of properties in various ways: - Assumptions - Bodyless procedures -By bypassing the symbolic check, a concrete can check (property-based testing) can be used instead. How exactly Laurel will guarantee a correct hand-off between concrete and symbolic property checking, is yet to be designed. +By bypassing the symbolic check, a concrete check (property-based testing) can be used instead. How exactly Laurel will guarantee a correct hand-off between concrete and symbolic property checking, is yet to be designed. ## Data-flow analysis @@ -363,8 +363,10 @@ Laurel procedures are transparent by default, meaning that a call can use the bo By allowing any procedure to be transparent, Laurel prevents users from having to repeat the body of a procedure in a postcondition. Here's an example that shows an opaque procedure that would have been easier to define as being transparent, without any loss of readability: ``` -procedure increment(counter: Counter) opaque - // In Laurel, this ensures clause can be left out +procedure increment(counter: Counter) + // In Laurel, the next three lines can be left out and callers will get the same information + opaque + modifies counter ensures counter.value == old(counter.value) + 1 { counter.value := counter.value + 1 @@ -376,7 +378,7 @@ A contract in Laurel may not modify any object that exists outside of that contr A common design choice in verification-aware programming languages is not to allow creating or modifying objects in contracts. A good reason for this is that objects are more complex to reason about than immutable data, and contracts are intended to contain easy to reason about code. Laurel still allows creating and modifying new objects inside contracts because code might be declared to operate specifically through the use of reference types, and Laurel does not want to restrict users from using such code even in contracts. -A second reason for not allowing any heap modification inside contracts is that this is prone to soundness issues. From outside the contract the heap is assumed not to be modified, so if knowledge of an inside modification escapes the contract, this leads to an inconsistency. Because Laurel does not allow assigning to variable defined outside the contract, from inside the contract, no modification can escape the contract. The heap used inside a contract is a separate heap variable. +A second reason for not allowing any heap modification inside contracts is that this is prone to soundness issues. From outside the contract the heap is assumed not to be modified, so if knowledge of an inside modification escapes the contract, this leads to an inconsistency. Because Laurel does not allow assigning to a variable defined outside the contract, from inside the contract, no modification can escape the contract. The heap used inside a contract is a separate heap variable. ## Invoke on The postcondition of an opaque procedure is exposed to callers as an axiom: the ensures clause, universally quantified over the procedure's inputs. Left unrestricted, the solver may instantiate such an axiom on any matching term, which is a common cause of slow and unpredictable verification. @@ -396,9 +398,24 @@ This global availability is a deliberate simplification for the first version of ## Aliasing -Potential aliasing of heap allocated objects makes can make verification more complicated. Laurel introduced the `allocated` and `fresh` concepts that make it easier to specify which references are disjunct. +Potential aliasing of heap-allocated objects can make verification more complicated. Laurel introduced the `allocated` and `fresh` concepts that make it easier to specify which references are disjoint. + +``` +procedure allocate() returns (r: Node) + opaque + ensures fresh(r) +{ + return new Node +}; + +procedure usesAllocate(existing: Node) { + var created: Node := allocate(); + assert created != existing // holds: `fresh(r)` tells the caller `created` + // is distinct from every object that already existed +}; +``` - +Because `allocate` ensures `fresh(r)`, the caller learns that `created` was newly allocated and therefore cannot alias `existing`, or any other reference that existed before the call, without the caller having to track allocation itself. # Automated proof search Goal 5 was enabling the finding of proofs through automated search. @@ -457,7 +474,7 @@ procedure usesIdentity() { To be designed.. but here is some subject to change content. -Laurel can statically infer the types of variables, which, when the inferred types where otherwise not available in the source program, can enable emitting code that can be verified more efficiently. +Laurel can statically infer the types of variables, which, when the inferred types were otherwise not available in the source program, can enable emitting code that can be verified more efficiently. Here's an example related to nullable reference types: @@ -471,7 +488,7 @@ bar := null; bar.x := 2 ``` -Without type inference, we can not judge whether the variable `foo` should have type `Foo` or `Nullable`, so we have to pick defensively: +Without type inference, we cannot judge whether the variable `foo` should have type `Foo` or `Nullable`, so we have to pick defensively: ``` datatype Nullable = from_NotNull(as_notNull: T) | from_Null @@ -520,7 +537,7 @@ as_notNull(foo_2).x := 2; To be designed.. -Useful for dynamic languages. Infers composites types based on fields assigned to values. +Useful for dynamic languages. Infers composite types based on fields assigned to values. Composite types perform better than maps because reading from them incurs no domain check. # Verification code must be erasable @@ -530,7 +547,7 @@ To support goal 7, for verification code not to affect the outcome of executing Rules for contracts: - Contract code may not modify variables defined outside the contract scope. - Contract code has an empty modifies clause. Contract code operates on a copy of the heap. -- Contract code must terminate, so removing it does not whether execution code is reachable or not. +- Contract code must terminate, so removing it does not affect whether execution code is reachable or not. For example, the body of the procedure below changes `p`, and that effect is declared with `modifies p`; `old(p.x)` in the ensures clause refers to the pre-state: @@ -547,7 +564,7 @@ procedure shift(p: Point, dx: int) The ensures expression may read the heap and build temporary values while it is evaluated, but it cannot assign to `p`, to `dx`, or to any variable declared outside it, and it contributes no modifies effect of its own. Even if the postcondition called a helper that allocated and mutated a scratch object, that would run against a copy of the heap and remain invisible to callers, which still see every pre-existing object unchanged across the evaluation of the contract. As a result, adding, strengthening, or removing the ensures clause never changes how the program executes. ## Decreases clauses -To enable proving that contracts terminate, Laurel uses decreasing clauses to enable proving the termination of procedure calls. +To enable proving that contracts terminate, Laurel uses decreases clauses to enable proving the termination of procedure calls. # Great user experience From f96422e32ad3c07aa0354a667324510e16369e9b Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 9 Jul 2026 08:15:09 +0000 Subject: [PATCH 17/20] Tweaks --- docs/verso/LaurelDesignGuide.lean | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/docs/verso/LaurelDesignGuide.lean b/docs/verso/LaurelDesignGuide.lean index 522a137292..bf4a75261c 100644 --- a/docs/verso/LaurelDesignGuide.lean +++ b/docs/verso/LaurelDesignGuide.lean @@ -56,8 +56,6 @@ Goals: To be designed.. ## Verification -Work in progress section - To achieve goal 1.2, enable proving properties through verification, Laurel has the following features. ### Assertions @@ -421,7 +419,7 @@ Because `allocate` ensures `fresh(r)`, the caller learns that `created` was newl Goal 5 was enabling the finding of proofs through automated search. ## Reads clauses -Reads clauses are useful to improve verification performance. The facts they prove work well together with the facts provided by modifies clauses, making it easier to prove which procedure values have remained unchanged after objects were modified. +Reads clauses are useful to improve verification performance. The facts they provide work well together with the facts provided by modifies clauses, making it easier to prove which procedure values have remained unchanged after objects were modified. ## Frozen types Frozen types (To be designed). A reads clause specifies that a procedure always returns the same value, if the reads references have the same values and if the explicit input arguments, which excludes the heap, are the same. A procedure that returns a newly created object, which has a reference counter that depends on the counter of the input heap, can thus never satisfy a reads clause. For this purpose Laurel allows erasing the counter from a reference value. A Laurel `Frozen` type takes a regular reference type, and produces a type that is the same except that it does not support reference equality or mutation of its fields. Record types are composite types that are frozen by default. @@ -569,7 +567,7 @@ To enable proving that contracts terminate, Laurel uses decreases clauses to ena # Great user experience ## Parameter lists -Parameter lists. In Laurel, input and output parameters are defined in a separate list. Inout parameters are defined by repeating the parameter name in both lists. In Core, there is a single parameter list where each parameter defines its kind (in/out/inout). +In Laurel, input and output parameters are defined in a separate list. Inout parameters are defined by repeating the parameter name in both lists. In Core, there is a single parameter list where each parameter defines its kind (in/out/inout). At the call-site, Laurel requires calls with multiple out parameters to occur inside an assignment, like this: `assign x, y := multiOutCall(a, b)` From 63c7240958fbdc59416093f95e06106ca8cdf65d Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 9 Jul 2026 08:37:58 +0000 Subject: [PATCH 18/20] Fixes --- docs/verso/LaurelDesignGuide.lean | 55 ++++++++++++++--------- docs/verso/LaurelImplementationGuide.lean | 2 +- 2 files changed, 36 insertions(+), 21 deletions(-) diff --git a/docs/verso/LaurelDesignGuide.lean b/docs/verso/LaurelDesignGuide.lean index bf4a75261c..d543b4c900 100644 --- a/docs/verso/LaurelDesignGuide.lean +++ b/docs/verso/LaurelDesignGuide.lean @@ -96,14 +96,14 @@ In a postcondition, `old(e)` denotes the value of the expression `e` in the proc ``` procedure increment(counter: Counter) opaque - ensures counter.value == old(counter.value) + 1 + ensures counter#value == old(counter#value) + 1 modifies counter { - counter.value := counter.value + 1 + counter#value := counter#value + 1 }; ``` -The postcondition `counter.value == old(counter.value) + 1` captures the mutation performed by the body, yet it is a pure comparison between two values. A caller learns exactly how the field changed relative to its prior value without the contract mutating anything, keeping verification code erasable (see goal 7). +The postcondition `counter#value == old(counter#value) + 1` captures the mutation performed by the body, yet it is a pure comparison between two values. A caller learns exactly how the field changed relative to its prior value without the contract mutating anything, keeping verification code erasable (see goal 7). ## Unbounded verification Bounded symbolic execution unrolls a loop a fixed number of times, so on its own it cannot prove a property for every run of a loop whose iteration count is not statically known. Loop invariants close that gap. A `while` loop may carry one or more `invariant` clauses, each an expression that must hold when the loop is first reached and be preserved by every iteration. @@ -365,9 +365,9 @@ procedure increment(counter: Counter) // In Laurel, the next three lines can be left out and callers will get the same information opaque modifies counter - ensures counter.value == old(counter.value) + 1 + ensures counter#value == old(counter#value) + 1 { - counter.value := counter.value + 1 + counter#value := counter#value + 1 }; ``` @@ -396,7 +396,9 @@ This global availability is a deliberate simplification for the first version of ## Aliasing -Potential aliasing of heap-allocated objects can make verification more complicated. Laurel introduced the `allocated` and `fresh` concepts that make it easier to specify which references are disjoint. +Potential aliasing of heap-allocated objects can make verification more complicated. Laurel builds on two related notions to make it easier to specify which references are disjoint. A reference is *allocated* (in a given state) when it already exists in that state's heap; internally this is the condition that the reference predates the state's allocation counter. A reference is *fresh* when it is the negation of that: newly created by the procedure and therefore not allocated in the pre-state. + +Today only `fresh` has surface syntax — the `fresh(e)` predicate, which may only target reference (impure composite) types. It is exactly what a caller needs to conclude that a returned reference cannot alias anything that was already allocated. ``` procedure allocate() returns (r: Node) @@ -413,7 +415,20 @@ procedure usesAllocate(existing: Node) { }; ``` -Because `allocate` ensures `fresh(r)`, the caller learns that `created` was newly allocated and therefore cannot alias `existing`, or any other reference that existed before the call, without the caller having to track allocation itself. +Because `allocate` ensures `fresh(r)`, the caller learns that `created` was newly allocated and therefore cannot alias `existing`, or any other reference that was already allocated before the call, without the caller having to track allocation itself. + +An `allocated(e)` predicate is planned as the dual of `fresh`. Where `fresh(e)` asserts a reference is new, `allocated(e)` will assert that a reference already existed in the current state's heap — useful, for example, in a precondition that requires an argument to be a pre-existing object rather than a fresh one. The following sketch (syntax illustrative — `allocated` is not yet implemented) shows the intended shape: + +``` +// syntax illustrative — `allocated` is planned, not yet implemented +procedure store(container: Container, item: Node) + requires allocated(item) // reject fresh items; only pre-existing ones may be stored + opaque + modifies container +{ + container#head := item +}; +``` # Automated proof search Goal 5 was enabling the finding of proofs through automated search. @@ -479,11 +494,11 @@ Here's an example related to nullable reference types: Input program: ``` var foo := new Foo; -foo.x := 1; +foo#x := 1; var bar := foo; bar := null; -bar.x := 2 +bar#x := 2 ``` Without type inference, we cannot judge whether the variable `foo` should have type `Foo` or `Nullable`, so we have to pick defensively: @@ -491,21 +506,21 @@ Without type inference, we cannot judge whether the variable `foo` should have t datatype Nullable = from_NotNull(as_notNull: T) | from_Null var foo: Nullable := from_NotNull(new Foo); -as_notNull(foo).x := 1; +as_notNull(foo)#x := 1; var bar: Nullable := foo; bar := null; -as_notNull(bar).x := 2 +as_notNull(bar)#x := 2 ``` With type inference, we can infer that `foo` is never nullable: ``` var foo: Foo := new Foo; -foo.x := 1; +foo#x := 1; var bar: Nullable := from_NotNull(foo); bar := null; -as_notNull(bar).x := 2 +as_notNull(bar)#x := 2 ``` Note the coercion `from_NotNull` that was inserted in the assignment to `bar`. Laurel can be given a list of coercions that can be inserted automatically. Laurel can also be given a list of type coercions, which it can use to change the type annotations of variables, from for example `T` to `Nullable`. @@ -517,18 +532,18 @@ Flow based types allow the type of a variable to change throughout the control-f Source program: ``` var foo := new Foo; -foo.x := 1; +foo#x := 1; foo := null; -foo.x := 2; +foo#x := 2; ``` Inferred program: ``` var foo := new Foo; -foo.x := 1; +foo#x := 1; var foo_2: Nullable := from_NotNull(foo); foo_2 := null; -as_notNull(foo_2).x := 2; +as_notNull(foo_2)#x := 2; ``` ## Inference of composite types @@ -547,15 +562,15 @@ Rules for contracts: - Contract code has an empty modifies clause. Contract code operates on a copy of the heap. - Contract code must terminate, so removing it does not affect whether execution code is reachable or not. -For example, the body of the procedure below changes `p`, and that effect is declared with `modifies p`; `old(p.x)` in the ensures clause refers to the pre-state: +For example, the body of the procedure below changes `p`, and that effect is declared with `modifies p`; `old(p#x)` in the ensures clause refers to the pre-state: ``` procedure shift(p: Point, dx: int) opaque - ensures p.x == old(p.x) + dx + ensures p#x == old(p#x) + dx modifies p { - p.x := p.x + dx + p#x := p#x + dx }; ``` diff --git a/docs/verso/LaurelImplementationGuide.lean b/docs/verso/LaurelImplementationGuide.lean index 7092e0934a..1959165795 100644 --- a/docs/verso/LaurelImplementationGuide.lean +++ b/docs/verso/LaurelImplementationGuide.lean @@ -140,7 +140,7 @@ The Laurel to Core translation pipeline uses these IRs: Most of the passes are in the Laurel IR. The transparency pass goes from `Laurel` to `UnorderedCoreWithLaurelTypes`. -The CoreGroupingAndOrdering goes from `UnorderedCoreWithLaurelTypes` to `CoreWithLaurelTypes` +The ordering pass goes from `UnorderedCoreWithLaurelTypes` to `CoreWithLaurelTypes`. And the LaurelToCoreSchemaPass goes from `CoreWithLaurelTypes` to `Core`. ## Passes From d49a0233b38cdc69aa35479353710a92f1272d72 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 9 Jul 2026 09:55:20 +0000 Subject: [PATCH 19/20] Fix code blocks in user guide --- docs/verso/LaurelUserGuide.lean | 87 ++++++++++++++++++++++++--------- 1 file changed, 65 insertions(+), 22 deletions(-) diff --git a/docs/verso/LaurelUserGuide.lean b/docs/verso/LaurelUserGuide.lean index a837210588..394ee312eb 100644 --- a/docs/verso/LaurelUserGuide.lean +++ b/docs/verso/LaurelUserGuide.lean @@ -12,6 +12,9 @@ import Strata.Languages.Laurel.LaurelCompilationPipeline import Strata.Languages.Laurel.HeapParameterization import Strata.Languages.Laurel.LiftImperativeExpressions import Strata.Languages.Laurel.ModifiesClauses +-- Provides `Strata.parseLaurelText`, used by the `laurel` code block below to +-- parse-check every example at doc-elaboration time. +import Strata.Languages.Laurel -- This gets access to most of the manual genre open Verso.Genre Manual @@ -86,6 +89,46 @@ def «example» : Verso.Doc.Elab.DirectiveExpanderOf LaurelExampleConfig let args ← stxs.mapM Verso.Doc.Elab.elabBlock ``(Verso.Doc.Block.other (Block.«example» $(Lean.quote title)) #[ $[ $args ],* ]) +/-- Configuration for the `laurel` code block. The `+unchecked` flag opts a + block out of parse checking — use it for illustrative or partial snippets + that are not intended to parse as a complete Laurel program. -/ +structure LaurelCodeConfig where + unchecked : Bool := false + +instance : Verso.ArgParse.FromArgs LaurelCodeConfig Verso.Doc.Elab.DocElabM where + fromArgs := LaurelCodeConfig.mk <$> .flag `unchecked false + +/-- A ````laurel```` code block. Renders like an ordinary code block, but also + *parse-checks* its contents at doc-elaboration time so a syntax error in an + example fails the documentation build. + + Only parsing and AST translation are run — not resolution or verification — + so examples that deliberately illustrate a verification *failure* (a failing + `assert`, a violated precondition, …) still pass, since they are + syntactically valid. A snippet that is not a complete program (it omits the + `program Laurel;` header) is wrapped before checking. Pass `+unchecked` to + skip checking entirely. -/ +@[code_block] +def laurel : Verso.Doc.Elab.CodeBlockExpanderOf LaurelCodeConfig + | config, str => do + -- `parseLaurelText` parses a bare sequence of declarations (the `.laurel.st` + -- file form), and the `program Laurel;` header is an artifact of the embedded + -- style that readers shouldn't see. Strip an optional leading `program …;` + -- header line so it is neither checked against nor rendered. + let content := str.getString + let source := + if content.startsWith "program" then + match content.splitOn "\n" with + | _header :: rest => "\n".intercalate rest + | [] => content + else content + unless config.unchecked do + try + let _ ← (Strata.parseLaurelText "" source : IO Strata.Laurel.Program) + catch e => + throwErrorAt str m!"Laurel example failed to parse:\n{e.toMessageData}" + ``(Verso.Doc.Block.code $(Lean.quote source)) + #doc (Manual) "The Laurel User Guide" => %%% shortTitle := "Laurel User Guide" @@ -122,7 +165,7 @@ A Laurel program is a sequence of declarations. The most important one is the introduced with `returns`, an optional contract, and a body enclosed in braces. Statements inside the body are separated by semicolons. -``` +```laurel program Laurel; procedure addOne(x: int) returns (r: int) opaque @@ -863,7 +906,7 @@ fields and may declare *instance procedures* (methods). Fields are read and written with the `#` selector, instances are created with `new`, and a method is invoked with the same `#` syntax. -``` +```laurel program Laurel; composite Counter { var count: int @@ -894,7 +937,7 @@ Field selection and method calls chain, so you can reach through one object to another: `o#inner#x` reads field `x` of the object stored in `o`'s `inner` field, and `o#inner#isOne()` calls a method on it. -``` +```laurel composite Inner { var x: int } composite Outer { var inner: Inner } @@ -914,7 +957,7 @@ An `assert` states a fact that Laurel must prove holds at that point in the program. If the solver cannot prove it, verification fails and the failing `assert` is reported. -``` +```laurel procedure checkPositive(x: int) requires x > 0 opaque @@ -929,7 +972,7 @@ from that point on, Laurel reasons as if the assumed expression is true. Assumin something false makes everything afterwards trivially provable, which is occasionally useful but should be used with care. -``` +```laurel procedure assumeThenProve() opaque { @@ -956,7 +999,7 @@ A loop invariant serves two purposes. Inside the loop it tells Laurel what is true, which is what lets it prove that operations in the body are safe. After the loop it combines with the negated guard to describe the state on exit. -``` +```laurel procedure countUp() opaque { @@ -987,7 +1030,7 @@ procedure is called. It has two effects. It restricts callers: every call site must prove the precondition holds for the arguments it passes. And it gives the body an assumption to work from when proving its own obligations. -``` +```laurel procedure halve(x: int) returns (r: int) requires x > 0 opaque @@ -1007,7 +1050,7 @@ procedure caller() A procedure may have several `requires` clauses; they are conjoined. A call must satisfy all of them. -``` +```laurel procedure addBoth(x: int, y: int) returns (r: int) requires x > 0 requires y > 0 @@ -1020,13 +1063,13 @@ procedure addBoth(x: int, y: int) returns (r: int) ## Postconditions -A postcondition for a procedure is a condition that is guaranteed to hold after the procedure executes. Sometimes, we can capture the entire desired behavior of a procedure with a postcondition that is simpler than the procedure's implementation. A typical example of sorting a list of numbers: the end result, that the list is sorted, is simpler to describe the the algorithm to do the sorting. +A postcondition for a procedure is a condition that is guaranteed to hold after the procedure executes. Sometimes, we can capture the entire desired behavior of a procedure with a postcondition that is simpler than the procedure's implementation. A typical example of sorting a list of numbers: the end result, that the list is sorted, is simpler to describe than the algorithm to do the sorting. When a postcondition can capture the entire desired behavior of a procedure, and is simpler than the body, then adding it allows improving the correctness guarantee of your program, since only the simpler postcondition needs to be reviewed for correctness. Also, when postconditions are added to a procedure, callers will only be able to use the postconditions to reason about the call, and not the body. This simplifies reasoning at the call-site, improving verification results. In Laurel, to be explicit, a procedure with postconditions must be marked as `opaque`, indicating that its body is not visible to callers. A procedure without postconditions can also be marked `opaque`, although then callers will know nothing about the result of the call. By default Laurel procedures have a transparent body, meaning that callers can use the callee's body for reasoning about the call's result. -``` +```laurel procedure max(x: int, y: int) returns (r: int) opaque ensures r >= x @@ -1040,7 +1083,7 @@ procedure max(x: int, y: int) returns (r: int) At a call site, the postcondition is all the caller knows about the result: -``` +```laurel procedure useMax() opaque { @@ -1064,7 +1107,7 @@ A `forall` states that its body holds for every value of the bound variables; an `exists` states that there is at least one value for which the body holds. Both take one or more typed binders and a body introduced with `=>`. -``` +```laurel procedure quantifiers() opaque { @@ -1077,7 +1120,7 @@ The implication operator `==>` is frequently used inside quantifiers to restrict the range of interest — for instance, to say something about every index of an array within bounds: -``` +```laurel procedure inContract(n: int) requires n > 0 opaque @@ -1091,7 +1134,7 @@ checked by enumeration, the solver reasons about it logically. To control how it instantiates a quantifier, you can attach a *trigger* — a pattern in braces that tells the solver which terms should cause the quantified fact to fire: -``` +```laurel procedure P(x: int): int; procedure withTrigger() opaque @@ -1113,11 +1156,11 @@ TODO, fill in ## Modifies clauses -As previously mentioned, Laurel procedures have a transparent body by default, so callers can reason about the callee's body. This works also when the callee mutates the heap in its body. However, when we make a heap-mutatijng procedure `opaque`, and the body is no longer available for reasoning, then the caller must accept the possibility that the entire heap was mutated, meaning that nothing can be proven about the heap any more, a really bad thing. To enable heap reasoning after calling opaque heap-mutating procedures, Laurel has modifies clauses. +As previously mentioned, Laurel procedures have a transparent body by default, so callers can reason about the callee's body. This works also when the callee mutates the heap in its body. However, when we make a heap-mutating procedure `opaque`, and the body is no longer available for reasoning, then the caller must accept the possibility that the entire heap was mutated, meaning that nothing can be proven about the heap any more, a really bad thing. To enable heap reasoning after calling opaque heap-mutating procedures, Laurel has modifies clauses. A modifies clause specifies the heap references that may have been modified by the procedure. Example: -``` +```laurel composite Container { var value: int } @@ -1137,18 +1180,18 @@ procedure caller() var x: int := a#value; var y: int := b#value; bump(b); - assert x == a#value // holds: only b is in bump's modifies clause + assert x == a#value; // holds: only b is in bump's modifies clause assert y == b#value // fails: b is in bump's modifies clause }; ``` -A opaque procedure that writes to an object it has not listed in the modifies clause is rejected, also when this write is done through another procedure call. You can list several references by repeating the clause (`modifies c; modifies d`), and the wildcard `modifies *` permits modifying any object — at the cost of telling callers that nothing on the heap is preserved. +An opaque procedure that writes to an object it has not listed in the modifies clause is rejected, also when this write is done through another procedure call. You can list several references by repeating the clause (`modifies c; modifies d`), and the wildcard `modifies *` permits modifying any object — at the cost of telling callers that nothing on the heap is preserved. Objects allocated with `new` *inside* the procedure body are exempt: a freshly allocated object may be modified freely without appearing in the `modifies` clause, because no caller could hold any prior knowledge about it. -``` +```laurel composite Container { var value: int } procedure makeOne() @@ -1172,7 +1215,7 @@ to the state when it was entered. Wrapping an expression in `old(...)` evaluates that expression in the *pre-state* — the heap as it was on entry. This is the standard way to specify a procedure that mutates its arguments. -``` +```laurel composite Cell { var value: int } @@ -1194,7 +1237,7 @@ clause would read `c#value == c#value + 1`, which no implementation can satisfy. sub-expression: `old(2 * c#value + 3)` means the same as `2 * old(c#value) + 3`. It may also appear inside quantifiers and conditionals in a postcondition: -``` +```laurel composite Cell { var value: int } procedure strictBump(c: Cell) @@ -1209,7 +1252,7 @@ procedure strictBump(c: Cell) A caller can reproduce the two-state reasoning by snapshotting the pre-state into a local variable before the call and asserting against it afterwards: -``` +```laurel program Laurel; composite Cell { var value: int } From 27b3dad8db2a4e849c33a065ce8fbaedde710d16 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 9 Jul 2026 10:11:57 +0000 Subject: [PATCH 20/20] Improvements to the user guide --- docs/verso/LaurelUserGuide.lean | 198 +++++++++++++++++++++++++++----- 1 file changed, 172 insertions(+), 26 deletions(-) diff --git a/docs/verso/LaurelUserGuide.lean b/docs/verso/LaurelUserGuide.lean index 394ee312eb..d5fa336df8 100644 --- a/docs/verso/LaurelUserGuide.lean +++ b/docs/verso/LaurelUserGuide.lean @@ -136,27 +136,17 @@ shortTitle := "Laurel User Guide" # Summary -TODO: generalize this section since it's too verification focussed. - -Laurel is an intermediate verification language. It is the common target for -verifiers built on top of garbage-collected, imperative source languages such +Laurel is an intermediate analysis language. It is the common target for +code analysers built on top of garbage-collected, imperative source languages such as Java, Python, and JavaScript. You usually do not write Laurel by hand; -a front-end translates your annotated source program into Laurel, and Laurel is -then checked for correctness. Understanding Laurel helps you understand what the -front-end checks and why a verification succeeds or fails. - -Laurel is built to be both *complete* and *accurate*. It is complete because you -can specify any behavior you want and have it checked against the -implementation. It is accurate because, when the underlying solver cannot decide -whether a program meets its specification, you can supply hints — extra -assertions, loop invariants, or contracts — that let it reach a definite answer. -Some properties, such as the absence of common runtime errors, are checked -without you having to state them. - -Under the hood, Laurel discharges its proof obligations using a Satisfiability -Modulo Theories (SMT) solver. For simple obligations the solver finds a proof on -its own. For harder ones it needs guidance, and most of this guide is about the -constructs you use to provide that guidance. +a front-end translates your, possibly annotated, source program into Laurel, +and Laurel is then used to analyse your sources. +Understanding Laurel helps you build such front-ends. + +Laurel out of the box supports these kinds of analysis: +- Property-based testing +- Bounded verification +- Unbounded verification ## A first program @@ -167,9 +157,9 @@ Statements inside the body are separated by semicolons. ```laurel program Laurel; -procedure addOne(x: int) returns (r: int) +procedure addTwo(x: int) returns (r: int) opaque - ensures r == x + 1 + ensures r == x + 2 { r := x; r++; @@ -183,7 +173,6 @@ Having these internal properties and constructors allows us to define an increme # Resolution - ## Bidirectional type checking There are two operations on expressions, written here in standard @@ -823,7 +812,6 @@ named-output assignment. # Execution -TODO, cover all the non-verification language parts ## Types @@ -987,7 +975,7 @@ ultimately checked by turning them into assertions at the right program points. ## Erased code -TODO, show that assignments inside a contract may not be to variables declared outside the contract. +To be designed.. ## Loop invariants @@ -1150,7 +1138,165 @@ To be designed.. ## Constrained types -TODO, fill in +A *constrained type* (a refinement type) is a base type narrowed by a +predicate. It is introduced with the `constrained` keyword and has four parts: a +name, a value binder together with its base type, a `where` predicate that +values of the type must satisfy, and a `witness` value that proves the type is +inhabited. + +```laurel +constrained nat = x: int where x >= 0 witness 0 +``` + +This declares `nat` as the integers that are at least zero. The binder `x` +ranges over the base type `int`, `x >= 0` is the constraint, and `0` is the +witness — a concrete value Laurel checks against the predicate to be sure the +type is not empty. A witness that fails its own predicate is rejected: + +```laurel +constrained bad = x: int where x > 0 witness -1 +// error: the witness -1 does not satisfy x > 0 +``` + +A constrained type is checked at every point where a value *acquires* the type, +and it is available as an assumption at every point where a value is *known* to +have the type. The rest of this section walks through those points. + +### Inputs + +A parameter of constrained type contributes a precondition. Callers must prove +the argument satisfies the constraint, and in exchange the body may assume it. + +```laurel +constrained nat = x: int where x >= 0 witness 0 + +procedure inputAssumed(n: nat) + opaque +{ + assert n >= 0 // holds: the nat constraint is assumed for inputs +}; +``` + +Passing an argument that cannot be shown to satisfy the constraint fails at the +call site, exactly like any other {ref "rules-verification-statements"}[precondition]. + +### Outputs + +An output of constrained type contributes a postcondition. The procedure must +establish the constraint on its result, and callers may then assume it. + +```laurel +constrained nat = x: int where x >= 0 witness 0 + +procedure outputValid() returns (r: nat) + opaque +{ + r := 3 // ok: 3 satisfies x >= 0 +}; +``` + +Returning a value that violates the constraint fails as a postcondition: + +```laurel +constrained nat = x: int where x >= 0 witness 0 + +procedure outputInvalid() returns (r: nat) + opaque +{ + r := -1 // error: postcondition does not hold (-1 is not a nat) +}; +``` + +Because the constraint travels with the output, a caller of an `opaque` +procedure learns it from the contract alone, without seeing the body: + +```laurel +constrained nat = x: int where x >= 0 witness 0 + +procedure opaqueNat() returns (r: nat) + opaque; + +procedure callerAssumes() + opaque +{ + var v: int := opaqueNat(); + assert v >= 0 // holds: opaqueNat's result is a nat +}; +``` + +### Local variables + +Initializing or assigning to a constrained-typed local asserts the constraint +on the assigned value. Both the initial value and every later reassignment are +checked. + +```laurel +constrained nat = x: int where x >= 0 witness 0 + +procedure assignLocal() + opaque +{ + var y: nat := 5; // ok + y := -1 // error: assignment violates the nat constraint +}; +``` + +A constrained-typed local that is *declared without an initializer* is treated +as an arbitrary value that satisfies the constraint: the constraint is assumed, +but nothing more. In particular you cannot assume it holds the witness value. + +```laurel +constrained nat = x: int where x >= 0 witness 0 + +procedure uninitialized() + opaque +{ + var y: nat; + assert y >= 0 // holds: the constraint is assumed +}; +``` + +### Quantifiers + +When a quantifier binds a variable of constrained type, the constraint is +injected into the body so the bound variable ranges only over values of the +type. For `forall` the constraint becomes an antecedent; for `exists` it becomes +a conjunct. + +```laurel +constrained nat = x: int where x >= 0 witness 0 + +procedure quantifiedNat() + opaque +{ + // provable only because n >= 0 is injected: false over all integers + assert forall(n: nat) => n + 1 > 0; + // 42 witnesses the existential and satisfies n >= 0 + assert exists(n: nat) => n == 42 +}; +``` + +### Nested constrained types + +A constrained type may refine another constrained type. The constraints then +compose: a value of the inner type must satisfy its own predicate *and* every +predicate up the chain. + +```laurel +constrained even = x: int where x % 2 == 0 witness 0 +constrained evenpos = x: even where x > 0 witness 2 + +procedure nested(x: evenpos) + opaque +{ + assert x > 0; // evenpos's own constraint + assert x % 2 == 0 // inherited from even +}; +``` + +Because algebraic datatypes can be encoded as constrained types over a base +type, this composition is what lets a value carry several layers of invariant at +once. # Verification - Objects