Document the design of Laurel#1144
Open
tautschnig wants to merge 1 commit into
Open
Conversation
Extend the rendered Laurel manual and cross-link it from the
repository entry points, so that Laurel's design rationale is
discoverable and sits alongside the auto-extracted type reference.
* docs/verso/LaurelDoc.lean — four new top-level sections:
- Design Principles (shared features only; imperative code need
not hide behind a functional spec; one AST for statements and
expressions; one AST node serves many back-ends; constructs
are not defined by their Core encoding).
- Conventions and Invariants (holes as the uniform 'unknown'
marker; reserved `$`-prefixed names; uniqueId-based
resolution; determinism of procedure calls).
- Error Correction via Holes.
- Relationship with the Python Front-End, and Known Limits and
Roadmap.
The Translation Pipeline section is expanded from four named
passes to all eleven Laurel-to-Laurel passes plus
CoreGroupingAndOrdering and the final Laurel-to-Core translation.
* docs/Architecture.md — the Laurel subsection is promoted from a
two-sentence pointer to a summary of Laurel's distinguishing
design choices, with links to the manual and to
PythonFrontend.md.
* README.md — adds a pointer to the Laurel manual and the Python
front-end guide next to the existing Architecture and Getting
Started links.
* .kiro/steering/laurel-development.md — an agent-facing playbook,
scoped via fileMatch to Strata/Languages/Laurel/** and its tests.
Covers the scope rule, explicit do/don't lists, the pipeline
order with its invariants, reserved identifier prefixes,
error-reporting rules, and a common-bugs table.
The manual still builds (`lake build laurel`).
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Contributor
There was a problem hiding this comment.
Pull request overview
This PR improves discoverability of Laurel’s design rationale by expanding the Verso-rendered Laurel manual and linking to it from repository entry points, and adds an agent-facing Laurel development playbook under .kiro/steering/.
Changes:
- Expanded
docs/verso/LaurelDoc.leanwith new sections (design principles, invariants, error recovery via holes, Python front-end relationship, roadmap) and a more detailed pipeline description. - Updated top-level documentation (
README.md,docs/Architecture.md) to link to the Laurel manual and the Python front-end guide. - Added
.kiro/steering/laurel-development.mdwith scoped guidance for editing Laurel code and tests.
Reviewed changes
Copilot reviewed 4 out of 4 changed files in this pull request and generated 6 comments.
| File | Description |
|---|---|
| README.md | Adds pointers to the Laurel manual source and Python front-end guide near other entry-point docs. |
| docs/verso/LaurelDoc.lean | Extends the Laurel manual with design/invariants sections and an expanded pipeline narrative. |
| docs/Architecture.md | Expands the Laurel architecture subsection and links to Laurel and Python documentation. |
| .kiro/steering/laurel-development.md | Adds a Laurel-specific agent playbook (scope rules, pipeline order, invariants, common bugs). |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Comment on lines
+227
to
+231
| 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. |
| 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. |
| - **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). |
| 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. |
| # Working on Laurel | ||
|
|
||
| Pointers for agents editing Laurel code. For background, read | ||
| [the rendered Laurel manual](../../docs/verso/LaurelDoc.lean) |
Comment on lines
+270
to
+287
| 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 |
olivier-aws
reviewed
May 8, 2026
Contributor
olivier-aws
left a comment
olivier-aws
left a comment
There was a problem hiding this comment.
First pass at review.
Comment on lines
+43
to
+46
| * **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. |
Contributor
There was a problem hiding this comment.
I would challenge that one. I think it is find to assume that users in many programing languages will want to write something like assert(foo()==3) where foo could modify the heap. And I think we should accept that at the source level. Then, given that it is a construct that can occur in Python/Java/TS, we should accept it in Laurel per Laurel's design principles.
Comment on lines
+74
to
+81
| ``` | ||
| FilterNonCompositeModifies → EliminateValueReturns → | ||
| HeapParameterization (needsResolves) → TypeHierarchyTransform (needsResolves) → | ||
| ModifiesClausesTransform (needsResolves) → InferHoleTypes → EliminateHoles → | ||
| DesugarShortCircuit → LiftExpressionAssignments → | ||
| EliminateReturns (needsResolves) → ConstrainedTypeElim (needsResolves) → | ||
| CoreGroupingAndOrdering → LaurelToCoreTranslator | ||
| ``` |
Contributor
There was a problem hiding this comment.
Maybe add a Do that the order in this doc must be updated if one adds a new transformation pass
| 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. |
Contributor
There was a problem hiding this comment.
Love that. I don't know if the order of the bullets matter to the coding agent, but this should come first IMO
| equivalent. | ||
| * **Mark passes that invalidate resolution with `needsResolves := true`** | ||
| in `LaurelCompilationPipeline.lean`. Otherwise subsequent passes will | ||
| trip over dangling `uniqueId`s. |
Contributor
There was a problem hiding this comment.
How do we know that a pass invalidates resolution?
| minimum: `MapStmtExpr`, `Resolution`, `HeapParameterization`, | ||
| `InferHoleTypes` / `EliminateHoles` (if the constructor can contain a | ||
| hole), `LiftImperativeExpressions`, `LaurelToCoreTranslator`, | ||
| `LaurelFormat`, and `ConcreteToAbstractTreeTranslator` + |
Contributor
There was a problem hiding this comment.
Can we have a build time check that enforces that?
|
|
||
| * **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. |
Contributor
There was a problem hiding this comment.
Does that mean that we never reject an input program but always emit a .Hole with a warning?
| * `$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. |
Contributor
There was a problem hiding this comment.
In Java, one can start an identifier with $: https://www.w3schools.com/java/java_variables_identifiers.asp. This may cause name conflict with $heap.
Comment on lines
+114
to
+116
| * 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. |
Contributor
There was a problem hiding this comment.
Can we add a principle that the error diagnostic must come with a source localization, to be really actionable?
ssomayyajula
added a commit
to ssomayyajula/Strata
that referenced
this pull request
May 8, 2026
…, strata-org#1144) Add section explaining why existing documentation efforts (PRs strata-org#1136 and strata-org#1144) are complementary but insufficient: they document WHAT the pipeline does but don't specify WHEN coercions fire, WHAT constitutes valid intermediate output, or HOW to arbitrate design disagreements. Positions both efforts as valuable (document as-is) while distinguishing the architecture spec (document should-be, precise enough for mechanical implementation). Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
ssomayyajula
added a commit
to ssomayyajula/Strata
that referenced
this pull request
May 8, 2026
Reframe as "complementary, different purpose" rather than "insufficient." Position PRs strata-org#1136/strata-org#1144 as valuable (onboarding, debugging) while distinguishing the architecture spec's prescriptive role. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Extend the rendered Laurel manual and cross-link it from the repository entry points, so that Laurel's design rationale is discoverable and sits alongside the auto-extracted type reference.
docs/verso/LaurelDoc.lean — four new top-level sections:
$-prefixed names; uniqueId-based resolution; determinism of procedure calls).docs/Architecture.md — the Laurel subsection is promoted from a two-sentence pointer to a summary of Laurel's distinguishing design choices, with links to the manual and to PythonFrontend.md.
README.md — adds a pointer to the Laurel manual and the Python front-end guide next to the existing Architecture and Getting Started links.
.kiro/steering/laurel-development.md — an agent-facing playbook, scoped via fileMatch to Strata/Languages/Laurel/** and its tests. Covers the scope rule, explicit do/don't lists, the pipeline order with its invariants, reserved identifier prefixes, error-reporting rules, and a common-bugs table.
The manual still builds (
lake build laurel).By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.