diff --git a/.kiro/steering/laurel-development.md b/.kiro/steering/laurel-development.md new file mode 100644 index 0000000000..499ddb36a1 --- /dev/null +++ b/.kiro/steering/laurel-development.md @@ -0,0 +1,139 @@ +--- +inclusion: fileMatch +fileMatchPattern: ['Strata/Languages/Laurel/**/*.lean', 'StrataTest/Languages/Laurel/**/*.lean'] +--- + +# Working on Laurel + +Pointers for agents editing Laurel code. For background, read +[the rendered Laurel manual](../../docs/verso/LaurelDoc.lean) +(sections *Design Principles*, *Conventions and Invariants*, +*Translation Pipeline*, and *Known Limits and Roadmap*). + +## Scope rules + +Laurel is *the* language for features shared between imperative, +garbage-collected source languages (Java, Python, JavaScript, TypeScript). + +* If a feature is only needed for one source language, put it in that + front-end's translator, not in Laurel. +* If a feature is deductive-verification specific (e.g. opacity, + `decreases`), it is OK to add to Laurel — Laurel targets multiple + analyses but carries verification-specific annotations. +* Feature design is about user expressivity, not about how it lowers to + Core. The Core encoding can change (see the heap rewrite in PR #338) + without altering Laurel semantics. + +## Do not + +* **Do not split `StmtExpr` into separate statement and expression + types.** The unified AST is deliberate and reduces duplication of + constructs like `IfThenElse` and `Block`. +* **Do not invent a new "I don't know" type of node.** Use `.Hole` with a + deterministic flag and let `InferHoleTypes` + `EliminateHoles` handle + it. Adding a second unknown-node kind breaks every downstream pass. +* **Do not add side tables for metadata.** `AstNode` already carries + `source`; if you need more, key it on post-resolution `uniqueId`. +* **Do not resolve identifiers by textual name** in any pass after + resolution. Use `uniqueId`. +* **Do not encode Python-specific type information in Laurel types.** + Python's `Any` lives in `Strata/Languages/Python/`; Laurel sees it as + a single composite type with constructors, and that is the intended + abstraction. +* **Do not lift procedure calls into assert/contract bodies.** Pure + contexts must remain pure. If a front-end wants to check a property + about a procedure call's result, it must first bind the result to a + local. + +## Do + +* **Use `.Hole` to recover from errors in translators.** Emit a + diagnostic and a hole in place of the problematic sub-expression; the + rest of the program still compiles and the user sees a useful error. +* **When you add a `StmtExpr` constructor, update every pass.** At + minimum: `MapStmtExpr`, `Resolution`, `HeapParameterization`, + `InferHoleTypes` / `EliminateHoles` (if the constructor can contain a + hole), `LiftImperativeExpressions`, `LaurelToCoreTranslator`, + `LaurelFormat`, and `ConcreteToAbstractTreeTranslator` + + `AbstractToConcreteTreeTranslator`. Missing one produces the classic + "holes should have been eliminated before translation" error or + equivalent. +* **Mark passes that invalidate resolution with `needsResolves := true`** + in `LaurelCompilationPipeline.lean`. Otherwise subsequent passes will + trip over dangling `uniqueId`s. +* **Keep the translation to Core "dumb".** If a Laurel → Core case needs + non-trivial work, the work probably belongs in an earlier + Laurel → Laurel pass. +* **Add an `Examples/` test for any new construct.** The + `StrataTest/Languages/Laurel/Examples/Fundamentals/T*.lean` tests are + numbered by convention; add to the appropriate theme or create a new + `T` number. + +## Pipeline order (`LaurelCompilationPipeline.lean`) + +``` +FilterNonCompositeModifies → EliminateValueReturns → +HeapParameterization (needsResolves) → TypeHierarchyTransform (needsResolves) → +ModifiesClausesTransform (needsResolves) → InferHoleTypes → EliminateHoles → +DesugarShortCircuit → LiftExpressionAssignments → +EliminateReturns (needsResolves) → ConstrainedTypeElim (needsResolves) → +CoreGroupingAndOrdering → LaurelToCoreTranslator +``` + +Invariants across passes: + +1. After `Resolution`, every identifier reference has a `uniqueId` that + matches some declaration. +2. After `EliminateHoles`, the program contains no deterministic holes. + Non-deterministic holes are translated to havocs. +3. After `LiftExpressionAssignments`, every statement-like `StmtExpr` + sits in a statement position. Expression positions contain only + expression-like constructors. +4. After `LaurelToCoreTranslator`, the result is a valid Core program. + +Breaking any of these invariants is almost always a bug, not a deliberate +relaxation. + +## Reserved identifier prefixes + +Emit these from passes; do **not** accept them as user identifiers: + +* `$heap`, `$heap_in` — heap parameters. +* `$hole_N` — uninterpreted functions generated by `EliminateHoles`. +* `$__ty_unused_N` — fresh type variables used as "unknown type" + placeholders. +* `$` prefix in general — reserved for translator-generated names. + +## Error reporting + +* Collect diagnostics; do not abort on the first error if you can + meaningfully continue with a hole. +* Resolution errors abort the pipeline before Core to avoid duplicate + diagnostics. If your pass produces resolution errors, add them to the + Laurel diagnostics list and let the pipeline do the early return. +* The Laurel pipeline is meant to produce user-actionable diagnostics. + "Not yet implemented" is an acceptable diagnostic for an unreachable + case; a panic is not. + +## Common bugs + +| Symptom | Likely cause | +|---------|--------------| +| `holes should have been eliminated before translation` | New translator case emits a hole inside a container (e.g., `Block`, `PureFieldUpdate`) that `EliminateHoles` does not descend into. | +| `Resolution failed: 'X' is not defined` after a Laurel → Laurel pass | Pass generated a fresh identifier without adding a declaration, or rewrote a reference without re-running resolution. Mark the pass `needsResolves := true`. | +| `calls to procedures are not supported in functions or contracts` | A procedure call reached a pure-context `StmtExpr` (inside an `Assert`, `Assume`, `Quantifier`, or a contract expression). The upstream translator must bind the call to a local first. | +| `Impossible to unify` at Core type-check time | A Laurel type slipped through to Core without being lowered; check that every Laurel-specific `HighType` is handled in `LaurelToCoreTranslator.translateType`. | +| `could not infer type` inside `translateType` | A `HighType.Unknown` survived because `InferHoleTypes` could not pick it up. Either the hole had no context, or the containing constructor is not traversed by the inference pass. | +| Build times blow up | A recursive pass over `StmtExpr` was written without a termination proof. Use the helpers in `MapStmtExpr.lean` rather than hand-rolling traversal when possible. | + +## Useful starting points + +* Authoritative AST: `Strata/Languages/Laurel/Laurel.lean`. +* Pipeline orchestrator: + `Strata/Languages/Laurel/LaurelCompilationPipeline.lean`. +* Unified AST traversal helpers: `Strata/Languages/Laurel/MapStmtExpr.lean`. +* Resolution: `Strata/Languages/Laurel/Resolution.lean`. +* Final translation: `Strata/Languages/Laurel/LaurelToCoreTranslator.lean`. +* Generated docs: open + `docs/api/.lake/build/doc/Strata/Languages/Laurel/Laurel.html` or + rebuild the Verso manual from `docs/verso/LaurelDoc.lean`. diff --git a/README.md b/README.md index e0b0ad4a11..6993bccd03 100644 --- a/README.md +++ b/README.md @@ -13,6 +13,11 @@ Strata. Also see the [Architecture](docs/Architecture.md) document that introduces some terminology and describes Strata's components, and a [Getting Started](docs/GettingStarted.md) guide that describes how to create a new dialect and analysis using existing features. +Language-specific manuals live alongside the code: the +[Laurel manual](docs/verso/LaurelDoc.lean) (rendered via +`docs/verso/generate.sh`) documents Strata's intermediate verification +language, and the [Python front-end guide](docs/PythonFrontend.md) +describes how Python is compiled through Laurel. **N.B.: Strata is under active development, and there may be breaking changes!** diff --git a/docs/Architecture.md b/docs/Architecture.md index 5ba11a8798..da11b0258f 100644 --- a/docs/Architecture.md +++ b/docs/Architecture.md @@ -58,8 +58,16 @@ The C_Simp dialect ([`Strata.Languages.C_Simp`](../Strata//Languages/C_Simp/)) i ### Laurel -The Laurel dialect is supposed to serve as an intermediate verification language for at least Java, Python, JavaScript. It is translated to Strata Core during its deductive verification. -Please refer to the description in the [`Strata.Languages.Laurel.Laurel`](../Strata/Languages/Laurel/Laurel.lean). +The Laurel dialect is an intermediate verification language (IVL) that serves as a compilation target for popular imperative, garbage-collected languages — Java, Python, JavaScript, and TypeScript. Laurel is translated to Strata Core for deductive verification, with planned support for model checking, property-based testing, and data-flow analysis. + +Key design choices that differentiate Laurel from Strata Core: + +- **Features shared across source languages.** A feature is added to Laurel only when it is useful for Java and at least one other source language. Language-specific constructs (e.g. Python's `__getattr__`) are handled by the corresponding front-end translator, not by Laurel itself. +- **A unified `StmtExpr` AST.** Statements and expressions share a single type, eliminating duplication for shared constructs such as `IfThenElse` and `Block`. +- **Imperative code may be transparent.** Unlike some IVLs, Laurel does not require imperative code to hide behind a functional specification; a Laurel procedure's body can be visible to its callers. +- **Translator-neutral semantics.** Features that are specific to one back-end (e.g. opacity, which is a deductive-verification concept) are carried as annotations but not baked into the core AST, so that model checkers and data-flow analyses do not need to know about them. + +For full documentation — design principles, conventions, the compilation pipeline, and all `{docstring}`-extracted type references — see **[The Laurel Language manual](./verso/LaurelDoc.lean)** (rendered HTML under `docs/api/.lake/build/doc/Strata/Languages/Laurel/Laurel.html` after running `docs/verso/generate.sh`). For how the Python front-end uses Laurel, see [`docs/PythonFrontend.md`](PythonFrontend.md). ### SMTLib diff --git a/docs/verso/LaurelDoc.lean b/docs/verso/LaurelDoc.lean index 4d153eb439..39760390f9 100644 --- a/docs/verso/LaurelDoc.lean +++ b/docs/verso/LaurelDoc.lean @@ -84,6 +84,72 @@ share a single implementation type, the StmtExpr. This reduces duplication for c like conditionals and variable declarations. Each StmtExpr has a user facing type, which for statement-like constructs could be void. +# Design Principles + +These principles recur in design discussions on Laurel pull requests and issues. Proposed +features or refactorings that violate them tend to be pushed back. + +## Shared between source languages, or don't add it + +The defining criterion for a Laurel feature is that it is "useful for Java and something +else". Features that make sense only for one source language (for example, nominal +subtyping specifically for Java generics, or Python's `__getattr__`) belong in the +source-language translator, not in Laurel. Front-ends are expected to encode +language-specific constructs using Laurel's primitives. + +Concrete instances of the principle: + +- Inheritance is in Laurel because Java, Python and TypeScript all use it. +- Closures and thunks are not first-class in Laurel; they are modelled through the dynamic + dispatch mechanism — a caller can encode a closure as a composite with a named method and + use `InstanceCall`. +- Manual memory management is out of scope in the short term. + +## Imperative code need not hide behind a functional specification + +Laurel does not require imperative code to be encapsulated using a functional specification. +Sometimes the imperative code is as readable as, or more readable than, a functional +specification would be. + +Consequences of this decision: + +- A Laurel procedure body may be transparent to its callers. There is no requirement that a + caller only see an `ensures` clause; if the body has no postcondition the caller can see + (and reason about) the implementation. This is the origin of the transparent / opaque / + `Body.External` distinction. +- Statements are allowed in expression positions in principle. The compilation pipeline has + to lift them out eventually (see Lifting Expression Assignments below), but the AST + admits programs in which an assignment appears as part of an expression. The fact that + Core cannot represent such programs is not Laurel's problem. + +## One AST for statements and expressions + +Laurel has a single algebraic type `StmtExpr` that mixes statement-like (`Assign`, `While`, +`Return`, …) and expression-like (`LiteralInt`, `PrimitiveOp`, `IfThenElse`, …) +constructors. Every `StmtExpr` has a user-facing type which, for statement-like +constructors, is `void`. A conditional therefore only needs to be defined once, instead of +once for the expression language and once for the statement language. + +The same choice drives why blocks can occur inside expressions: the machinery that handles +a block of statements is exactly the machinery that handles a block used as an +expression-with-side-effects. + +## One AST node, many back-ends + +Because Laurel targets multiple analyses — deductive verification, and in the future model +checking, property-based testing, and data-flow analysis — semantic features that are +specific to one discharge strategy must not leak into the AST. Opacity, for example, is a +concept connected to deductive verification: it is about how to generate VCs that don't +include too much irrelevant information. Analyses other than deductive verification should +not need to take opacity into account. + +## Constructs are not defined by their Core encoding + +Laurel features are designed in terms of user expressivity, not in terms of how they lower +to Core. The Core encoding of a Laurel construct can change, and has changed (the heap +encoding was rewritten to use datatypes instead of axioms), without altering the meaning of +the construct in Laurel. + # Types Laurel's type system includes primitive types, collection types, and user-defined types. @@ -146,11 +212,94 @@ A Laurel program consists of procedures, global variables, type definitions, and {docstring Strata.Laurel.Program} +# Conventions and Invariants + +## Holes are the uniform "unknown" marker + +The `.Hole` constructor of `StmtExpr` is how Laurel represents any expression whose +identity is not yet known. It is used by front-end translators when a construct has no +Laurel encoding yet, by error-recovery paths when an error is encountered (so the rest of +the program can still compile and produce useful diagnostics), and by specification +pipelines that cannot materialise a precondition. + +Two pipeline passes close the loop: `InferHoleTypes` labels every hole with the type its +context demands, and `EliminateHoles` replaces deterministic holes with calls to freshly +generated uninterpreted functions, and non-deterministic holes with havocs. + +The invariant is that any hole that survives past `EliminateHoles` is a pipeline bug. If a +new translator case introduces holes inside a constructor the elimination pass does not +traverse, that is where the fix has to go. + +## Reserved identifier prefixes + +Laurel programs are usually built by deserialization rather than by the Laurel parser, so +the parser itself does not need to police reserved names. Nevertheless, the following +prefixes are reserved for translator-generated identifiers and user programs must not use +them: + +- `$heap` — the current heap value inside a procedure body. +- `$heap_in` — the input heap of a heap-mutating procedure. +- `$hole_N` — a freshly generated uninterpreted function replacing a deterministic hole. +- `$__ty_unused_N` — a fresh type variable used as an "unknown type" placeholder. +- `$` prefix in general — reserved for translator-generated names. + +## Identifier resolution by unique ID + +After the Resolution pass, every identifier reference carries a `uniqueId : Option Nat` +that matches some declaration. Passes must not resolve identifiers by looking at textual +names; post-resolution, the `uniqueId` is authoritative. If a pass needs to know the owning +type of a field, it should use the field's `uniqueId` to look up its declaration in the +model rather than walking back through the composite type hierarchy. + +## Determinism of procedure calls + +A procedure modelled as a Core function is deterministic: two calls with the same arguments +produce the same result. A procedure modelled via axiomatic postconditions is +non-deterministic unless explicitly declared otherwise. This is why `Body.External` does +not imply transparency: external bodies can still be non-deterministic. + # Translation Pipeline Laurel programs are verified by translating them to Strata Core and then invoking the Core -verification pipeline. The translation involves several passes, each transforming the Laurel -program before the final conversion to Core. +verification pipeline. The translation involves several Laurel-to-Laurel lowering passes, +each annotated with whether it invalidates resolution (and therefore causes a re-run of the +resolver), followed by an ordering step and a final "dumb" translation to Core. + +The passes run in the following order: + +1. `FilterNonCompositeModifies` — strip modifies clauses on non-composite reads. +2. `EliminateValueReturns` — remove `Return` from statement positions where values are + returned. +3. `HeapParameterization` (invalidates resolution) — add `$heap` and `$heap_in` parameters + to procedures that read or mutate the heap, and rewrite field reads/writes. +4. `TypeHierarchyTransform` (invalidates resolution) — add a `TypeTag` field to composites + and emit `extends` facts for the inheritance hierarchy. +5. `ModifiesClausesTransform` (invalidates resolution) — translate modifies clauses into + ensures clauses. +6. `InferHoleTypes` — assign a type to every `Hole` from its context. +7. `EliminateHoles` — replace deterministic holes with calls to freshly generated + uninterpreted functions; non-deterministic holes become havocs. +8. `DesugarShortCircuit` — desugar `&&` and `||` into conditional expressions. +9. `LiftExpressionAssignments` — hoist statement-like `StmtExpr`s out of expression + positions. +10. `EliminateReturns` (invalidates resolution) — remove `Return` from any remaining + expression contexts. +11. `ConstrainedTypeElim` (invalidates resolution) — peel constrained types down to their + base types plus generated axioms. + +After these Laurel-to-Laurel passes, `CoreGroupingAndOrdering` groups datatypes and +procedures into strongly-connected components so that mutually-recursive definitions can be +emitted together. The final step, the Laurel-to-Core translator, is a largely one-to-one +mapping because all the heavy lifting has already been done by the passes above. + +The pipeline stops early if resolution fails. This is a simple way to avoid duplicate +diagnostics: without the early return, resolution errors reported by Laurel would also be +reported by Core. A better solution that lets some resolution errors from Laurel coexist +with verification errors from Core is imaginable, but would need more design work. + +The pipeline is intended to be executable: all passes, including the heap and the hole +elimination, avoid axioms in favour of explicit datatypes so that translated programs can +in principle be run with concrete values. ## Heap Parameterization @@ -181,3 +330,67 @@ The final translation converts Laurel types, expressions, statements, and proced their Strata Core equivalents. Procedures with bodies that only have constructs supported by Core expressions are translated to a Core function, while other procedures become Core procedures. + +It is called a "dumb" translation because, after all the earlier passes have run, the +remaining work is nearly one-to-one. A transparent Laurel procedure whose body fits in a +Core function becomes a Core function with a body. An opaque or postcondition-bearing +procedure becomes a Core function without a body plus an axiom derived from the +postcondition. + +Limitations, each a known work item: + +- Postconditions on Laurel functions are rejected because Core functions do not yet + support postconditions. +- Core procedures are always opaque to callers; a transparent Laurel procedure whose body + is not a Core function cannot currently retain transparency across the translation. + +# Error Correction via Holes + +When a front-end translator encounters an error in user code, it does not abort the +compilation. Instead it emits a `.Hole` in place of the problematic sub-expression and +records a diagnostic. The rest of the program continues to compile. This is what permits, +for instance, `pyAnalyzeLaurel` to produce useful output on partially broken input. + +An error-correcting parser can turn `3 +` into `3 + ?`, where `?` is a hole; an +error-correcting resolver can turn an ill-typed assignment `var y: bool := x` (with `x : +int`) into `var y: bool := ?`. The pipeline's hole infrastructure then ensures that `?` +does not produce further cascading diagnostics — any interaction with `?` is handled +uniformly. + +# Relationship with the Python Front-End + +Laurel is used as the compilation target for Strata's Python front-end. Every Python user +value is boxed into the Laurel datatype `Any`, which has constructors for each Python base +type (`from_int`, `from_str`, `from_bool`, …) and for exceptions. All user-visible +variables and procedure inputs/outputs are typed `Any` at the Laurel level. The Python-to- +Laurel translator inserts tag assertions (`Any..isfrom_int(x)`) before unwrapping +(`Any..as_int!(x)`). + +Laurel's type system is intentionally not the place where Python's type annotations are +enforced. The Python-to-Laurel translator turns those annotations into tag assertions. +Adding PEP 484-style typing features to Laurel is therefore neither necessary nor +obviously desirable for the Python path. It is, however, useful for the Java path, where +type checking inside Laurel's resolver is on the roadmap. + +# Known Limits and Roadmap + +Items that come up repeatedly in Laurel design discussions and are shared context for +anyone working on Laurel: + +- No flow-sensitive narrowing. The Core type checker is flow-insensitive; constructs like + Python's `isinstance(x, T)` do not refine the type of `x` in the then-branch. Narrowing + happens by inserting tag checks, and is the translator's responsibility. +- No first-class closures. Encode via composites with named methods. +- Aliasing is not modelled for pure-value container types. The Python front-end uses + value-semantics `ListAny` / `DictStrAny`; this is a known latent unsoundness. +- `InstanceCall` is only partially implemented in the translator. The plan is to lower it + to `StaticCall` in an earlier pass. +- Type checking in Laurel's resolver is work in progress. The intent is for + `resolveStmtExpr` to return a `HighTypeMd` alongside the resolved expression so that + each constructor can check its children's types during resolution. +- A Contract-and-Proof pass is planned. It will split Laurel procedures into a function + (the specification) and a proof (the implementation) before lowering, so that contracts + are lowered uniformly rather than handled case-by-case in the translator. +- Holes that survive the pipeline are not allowed. A hole must either be typed and + eliminated, or turned into a diagnostic; the invariant is that nothing reaches Core in + hole form.