M0.2: Add typed IR between AST and generators

agent-engineering commented

2026-05-10 04:41:43 +00:00

What

Add a typed intermediate representation (IR) between the AST and backend generators. Currently every generator (TS, PROV-O, CycloneDX, SPDX) parses raw AST and duplicates type logic. The IR should be the single source of truth for all code generation.

Tasks

Define SpeckIR type schema: typed state, actions, invariants, events, provenance annotations
Refactor compiler pipeline: Parse → [AST] → TypeCheck → [SpeckIR]
Refactor all 4 generators to consume IR instead of AST
Add provenance annotations: map each IR node back to source line/column
Add --emit-ir flag to speckl compile for debugging

Exit Criteria

speckl compile examples/ToggleSwitch.speck --emit-ir outputs typed IR
All 4 generators (TS, PROV-O, CycloneDX, SPDX) produce identical output to before refactor
Provenance chain from source line to generated artifact is traceable
No generator accesses raw AST — all consume SpeckIR

Dependencies

#18 (M0.1: Fix TS generator bugs) must be complete first. Can't refactor generators that are broken.

Context

Part of M0.2 in docs/PROVE-KAFKA-PLAN.md. Unlocks M0.3 (Z3), M2.1 (Rust backend), and optimization passes.

## What Add a typed intermediate representation (IR) between the AST and backend generators. Currently every generator (TS, PROV-O, CycloneDX, SPDX) parses raw AST and duplicates type logic. The IR should be the single source of truth for all code generation. ## Tasks - Define `SpeckIR` type schema: typed state, actions, invariants, events, provenance annotations - Refactor compiler pipeline: `Parse → [AST] → TypeCheck → [SpeckIR]` - Refactor all 4 generators to consume IR instead of AST - Add provenance annotations: map each IR node back to source line/column - Add `--emit-ir` flag to `speckl compile` for debugging ## Exit Criteria - `speckl compile examples/ToggleSwitch.speck --emit-ir` outputs typed IR - All 4 generators (TS, PROV-O, CycloneDX, SPDX) produce identical output to before refactor - Provenance chain from source line to generated artifact is traceable - No generator accesses raw AST — all consume `SpeckIR` ## Dependencies #18 (M0.1: Fix TS generator bugs) must be complete first. Can't refactor generators that are broken. ## Context Part of M0.2 in `docs/PROVE-KAFKA-PLAN.md`. Unlocks M0.3 (Z3), M2.1 (Rust backend), and optimization passes.

agent-engineering referenced this issue

2026-05-10 04:41:48 +00:00

M0.3: Implement Z3 verification backend #21

agent-engineering referenced this issue

2026-05-10 04:42:17 +00:00

M2.1: Rust code generation backend #25

agent-cos referenced this issue

2026-05-10 04:43:02 +00:00

Prove Kafka — Project Plan #17

agent-cos commented

2026-05-10 04:55:10 +00:00

[Request from @senior-eng]

Architecture Design Complete — docs/ir-design.md

The IR design document has been committed on branch feat/ir-design-speckl-20. Here's what it covers:

1. IR Schema (Section 2)

Complete TypeScript interfaces for:

SpeckType — PrimitiveType, ListType, SetType, MapType, RecordType, EnumType, OptionalType, UnitType
IRExpression — 14 expression node types, all typed (no raw strings): LiteralExpr, VariableRef, BinaryOp, UnaryOp, FieldAccess, MapGet, MapHas, SetHas, SetIn, MapKeys, MapValues, ListLength, CallBuiltin, QuantifierExpr, ConditionalExpr, RecordLiteral, SetLiteral, OldExpr
IRStatement — 6 statement types with lvalue analysis: IRAssign, IRLet, IRRequire, IREmit, IRReturn, IRAssert
IRSpeck / IRCompilationUnit — top-level structures with all metadata
ProvenanceRef — source span tracking (SourceLine, SourceSpan → IR node → generated artifact)

2. Feature Coverage Matrix

Every SpeckDL feature has a corresponding IR node. All current features covered: state, init, action, invariant, verify, event, record, interface (enum), provenance, bom, author, source, derives, satisfies, Set, Map, List, type aliases, precondition/postcondition, require, forall, notIn, in, union, , old(), emit, let, return.

3. Pipeline (Section 3)

Parse → [AST] → TypeCheck → [SpeckIR] → Optimize → Backend Selection → TS/Rust/Z3/PROV-O/SBOM

Key components:

TypeChecker — Pratt expression parser for SpeckDL expressions (replaces regex rewriting), symbol table construction, type resolution
Optimizer — 4 passes (opt-in, off by default)
IRBackend interface — clean contract for all generators

4. Optimization Passes (Section 4)

Guard Elision — mark redundant requires (same state checks, range implications, contradictions)
Dead State Elimination — reachability from init states
Transition Table Generation — compile state machine to O(1) lookup table
Invariant Hoisting — single _checkInvariants() function instead of inlined per-action

5. Migration Plan (Section 5) — Incremental, 5 Phases

Phase 1: Build TypeChecker (no generator changes)
Phase 2-3: Migrate generators one at a time (PROV-O → CycloneDX → SPDX → TypeScript → WASM)
Phase 4: Add optimizer
Phase 5: Add Z3 + Rust backends
Each phase validates identical output via baseline diffs

6. Z3 Translation (Section 6)

Explicit mapping:

SpeckDL types → Z3 sorts (Nat→Int, Set→Array T Bool, Map→Array K V, Record→Datatype, etc.)
Invariants → Z3 assertion functions (define-fun)
Actions → Z3 transition predicates (with frame conditions)
Bounded model checking → unroll to depth N, assert negated property, check-sat

Next step: Implementation can begin. The Pratt expression parser in the type checker is the highest-risk component — I recommend a spike on parsing all current example expressions before committing to the full type checker.

[Request from @senior-eng] ## Architecture Design Complete — docs/ir-design.md The IR design document has been committed on branch `feat/ir-design-speckl-20`. Here's what it covers: ### 1. IR Schema (Section 2) Complete TypeScript interfaces for: - **SpeckType** — PrimitiveType, ListType, SetType, MapType, RecordType, EnumType, OptionalType, UnitType - **IRExpression** — 14 expression node types, all typed (no raw strings): LiteralExpr, VariableRef, BinaryOp, UnaryOp, FieldAccess, MapGet, MapHas, SetHas, SetIn, MapKeys, MapValues, ListLength, CallBuiltin, QuantifierExpr, ConditionalExpr, RecordLiteral, SetLiteral, OldExpr - **IRStatement** — 6 statement types with lvalue analysis: IRAssign, IRLet, IRRequire, IREmit, IRReturn, IRAssert - **IRSpeck** / **IRCompilationUnit** — top-level structures with all metadata - **ProvenanceRef** — source span tracking (SourceLine, SourceSpan → IR node → generated artifact) ### 2. Feature Coverage Matrix Every SpeckDL feature has a corresponding IR node. All current features covered: state, init, action, invariant, verify, event, record, interface (enum), provenance, bom, author, source, derives, satisfies, Set, Map, List, type aliases, precondition/postcondition, require, forall, notIn, in, union, \, old(), emit, let, return. ### 3. Pipeline (Section 3) ``` Parse → [AST] → TypeCheck → [SpeckIR] → Optimize → Backend Selection → TS/Rust/Z3/PROV-O/SBOM ``` Key components: - **TypeChecker** — Pratt expression parser for SpeckDL expressions (replaces regex rewriting), symbol table construction, type resolution - **Optimizer** — 4 passes (opt-in, off by default) - **IRBackend interface** — clean contract for all generators ### 4. Optimization Passes (Section 4) 1. **Guard Elision** — mark redundant requires (same state checks, range implications, contradictions) 2. **Dead State Elimination** — reachability from init states 3. **Transition Table Generation** — compile state machine to O(1) lookup table 4. **Invariant Hoisting** — single `_checkInvariants()` function instead of inlined per-action ### 5. Migration Plan (Section 5) — Incremental, 5 Phases - Phase 1: Build TypeChecker (no generator changes) - Phase 2-3: Migrate generators one at a time (PROV-O → CycloneDX → SPDX → TypeScript → WASM) - Phase 4: Add optimizer - Phase 5: Add Z3 + Rust backends - Each phase validates **identical output** via baseline diffs ### 6. Z3 Translation (Section 6) Explicit mapping: - SpeckDL types → Z3 sorts (Nat→Int, Set→Array T Bool, Map→Array K V, Record→Datatype, etc.) - Invariants → Z3 assertion functions (define-fun) - Actions → Z3 transition predicates (with frame conditions) - Bounded model checking → unroll to depth N, assert negated property, check-sat Next step: Implementation can begin. The Pratt expression parser in the type checker is the highest-risk component — I recommend a spike on parsing all current example expressions before committing to the full type checker.

agent-cos commented

2026-05-10 05:08:07 +00:00

✅ Completed. IR architecture design doc at docs/ir-design.md (1,106 lines). Covers: IR schema (SpeckIR interfaces), full pipeline (Parse→AST→TypeCheck→IR→Backend), 4 optimization passes (guard elision, dead state elimination, transition tables, invariant hoisting), 5-phase incremental migration plan, Z3 translation mapping. Key risk: Pratt expression parser in TypeChecker — spike before full implementation.

✅ **Completed.** IR architecture design doc at `docs/ir-design.md` (1,106 lines). Covers: IR schema (SpeckIR interfaces), full pipeline (Parse→AST→TypeCheck→IR→Backend), 4 optimization passes (guard elision, dead state elimination, transition tables, invariant hoisting), 5-phase incremental migration plan, Z3 translation mapping. Key risk: Pratt expression parser in TypeChecker — spike before full implementation.

sscoble commented

2026-05-25 21:06:53 +00:00

Owner

Design doc written at compiler/docs/ir-design.md (~12KB). Covers: SpeckIR type schema (typed states, actions, invariants, events, provenance), compiler pipeline change (Parse→AST→TypeCheck→SpeckIR→Generators), type checker pass design, refactoring plan for all 6 generators, exit criteria with verification steps, and implementation plan.

Files:

src/ir/types.ts — type interfaces
src/ir/typecheck.ts — type checker
compiler/docs/ir-design.md — design document

Closing as done. Next: #21 (M0.3 Z3 backend) depends on this.

Design doc written at compiler/docs/ir-design.md (~12KB). Covers: SpeckIR type schema (typed states, actions, invariants, events, provenance), compiler pipeline change (Parse→AST→TypeCheck→SpeckIR→Generators), type checker pass design, refactoring plan for all 6 generators, exit criteria with verification steps, and implementation plan. Files: - src/ir/types.ts — type interfaces - src/ir/typecheck.ts — type checker - compiler/docs/ir-design.md — design document Closing as done. Next: #21 (M0.3 Z3 backend) depends on this.