Document the design of Laurel

.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`.

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!**

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