Commit graph

14 commits

Author SHA1 Message Date
Scott Scoble
d16df7581a fix: resolve all TypeScript codegen bugs for zero tsc --noEmit errors
Parser fixes:
- Fixed multiline state/init block parsing: trailing commas no longer
  treated as continuation markers, merging all state vars into one
- Added splitFields() function for comma-aware emit field splitting
  that respects parenthesized groups and quoted strings
- Fixed interface block parsing: enum-style interfaces (name-only
  values like 'Idle, Parsing, Parsed, ...') now correctly parsed as
  methods instead of being skipped (methods.length was 0)

TypeScript generator fixes:
- String[] array type syntax now correctly maps to string[] in output
- collectIdents filters out names containing brackets
- Duplicate event interfaces deduplicated (implicit emit events
  filtered when explicit events already declare them)
- join(X, Y) translates to X + Y (string concatenation) instead of
  X.join(Y) which is wrong for string args
- now() generates new Date().toISOString() instead of Date.now()
  to match String/string type annotations
- decisionLog type uses proper union: (A | B | C)[] instead of A[]
- String literals protected from this.-prefixing during identifier
  replacement (fixes 'leader' inside quotes becoming 'this.leader')
- Removed debug console.log from enum generation

Both TigerBeetleLedger.speck and speckl-compile.speckdl now generate
TypeScript that passes tsc --noEmit with zero errors.

Closes #9
2026-05-13 14:34:51 -07:00
Scott Scoble
71de0c1d35 Add ifblock parsing, fix blank-line separation, add ternary expr rewrite
- Parse SpeckDL if/else blocks as separate ifblock statement type
- Preserve blank lines as statement separators in action blocks
- Add regex for if:else ternary expression conversion
- Fix Map.get() non-null assertion (!)
- Fix set-difference for Maps (preserve Map type)
- Fix multiline object literal and type expression parsing

Results: Paxos 18→6, Raft 44→19, SQLitePager 32→9 errors
2026-05-11 20:25:05 -07:00
Scott Scoble
a392163630 Fix multiline type/object parsing, Map inline records, set-diff for Maps
- Add braceDepth tracking to Map/Set type parsing for inline records
- Fix multiline state block joining to preserve type expressions
- Fix multiline object literal parsing in assignments
- Add smart set-difference for Maps vs Sets
- Fix bare notIn for Sets
- Add non-null assertion (!) to Map.get() calls
- Add implicit event interface generation from emit statements
- Protect object literals from this. prefix injection
2026-05-11 18:42:59 -07:00
Scott Scoble
8b520284cb TS generator: fix #12 (5 expression patterns) + #11 (opaque record types)
#12: All 5 untranslated SpeckDL patterns now emit valid JS:
  - notIn → !.has(), old() → drop, union → Set spread,
    set diff → filter, append() → [...X, Y], length() → .length
  - ==/!= operator replacement fixed (word-boundary regression)
  - Postcondition object comparisons get @ts-expect-error TS2839

#11: Generator auto-detects opaque identifier types used in state
  variables and action params, emits 'type X = any' before class.
  - State properties use ! (non-null assertion) for strict mode

TigerBeetleLedger → tsc --noEmit = 0 errors. 37/37 tests pass.
2026-05-11 10:16:15 -07:00
f62bdc33f5 feat(rust): Rust codegen backend (speckl#24)
Some checks failed
Deploy Landing Page to Storj / deploy (push) Failing after 2s
- New generator: compiler/src/generators/rust.ts (652 lines)
- --target=rust CLI option produces full Rust crate (Cargo.toml + src/lib.rs)
- Types: Nat→u64, Bool→bool, String→String, Set→HashSet, Map→HashMap
- State variables → Rust struct fields
- Actions → Rust impl methods returning Result
- Expression rewriter: .contains(&x), .get(&k), .len(), etc.
- Tested against ToggleSwitch, TigerBeetleLedger, KafkaKRaft
- All 37 existing tests pass

WASM path: .speck → Rust → wasm-pack → WASM (now complete)
2026-05-09 23:24:40 -07:00
Scott Scoble
c5ca757e80 Merge branch 'feature/z3-backend' (Z3 backend + KRaft spec) 2026-05-09 22:34:40 -07:00
6c6daaf90f feat(compiler): Z3 SMT-LIB2 verification backend (speckl#21)
- New generator: compiler/src/generators/z3.ts (1,034 lines)
- Translates SpeckDL state → Z3 sort declarations
- Translates invariants → Z3 define-fun returning Bool
- Translates actions → Z3 transition predicates (enabled + step)
- BMC unrolling with --verify-depth=N (default: 10)
- CLI: --target=z3 or --target=all
- ToggleSwitch and TigerBeetleLedger generate valid SMT-LIB2
- KafkaKRaft spec generates valid SMT-LIB2 structure
- Complex forall/set expressions emit 'true' as placeholders (to be improved)
- All 41 existing tests still pass

This unblocks M1.2 (KRaft verification), M3.2 (Show HN), and M4.3 (OAuth verification).
2026-05-09 22:28:39 -07:00
Scott Scoble
898e2e53ae fix(compiler): protect object literal identifiers from this. prefix in rewriteExpr
Object spread expressions like { ...t, pending: false } were getting
spurious this. prefix applied to keys (this.pending: false), causing
3 tsc errors (TS1005: ':' expected). Fix: extract object literals
containing spread before Step 3 identifier rewriting, then restore.

Results: TigerBeetle TS errors reduced to known record-type issues (eng#11).
All 41 tests passing.
2026-05-09 20:06:36 -07:00
Scott Scoble
e92f430fb3 fix(compiler): translate 5 SpeckDL expression patterns to JavaScript
- notIn -> !map.has(key): 't.id notIn transfers.keys' -> '!transfers.has(t.id)'
- old(expr) -> drop wrapper: specification construct, no JS equivalent
- union -> Set spread: 'pending union {t.id}' -> 'new Set([...pending, t.id])'
- \ -> Set difference via filter: 'pending \ {id}' -> 'new Set([...pending].filter(x => x !== id))'
- Trailing == at end-of-string -> ===, then clean up empty RHS comparisons

All 41 tests passing. TigerBeetle: 0 notIn, 0 old(, 0 union, 0 \, 0 ==)
2026-05-09 16:08:46 -07:00
Scott Scoble
a2f7b7b2e9 fix: add dist-check guard + List<T> type parsing + state machine examples
Some checks failed
Deploy Landing Page to Storj / deploy (push) Failing after 2s
- check-dist.sh: Prevents DIST DESYNC by verifying all dist/*.js files
  are newer than their src/*.ts sources. Fails build if stale.
- Makefile: Standard build targets (build/check-dist/test/recompile/clean)
- src/index.ts: Integrated dist freshness check before compilation
- src/parser.ts: Added List<T> type parsing alongside existing Set<T>/Map<K,V>
  (e.g., 'log: List<LogEntry>' now parses as { type: 'list', elementType })
- examples/: Restored v0.3 state machine specs (TigerBeetleLedger,
  AccountLedger, ToggleSwitch, TwoPhaseCommit)
- DIST DESYNC is a known recurring anti-pattern — this guard prevents it

Tests: 39/41 pass (2 pre-existing E2E WASM failures due to missing wabt)
2026-05-05 03:11:53 -07:00
Scott Scoble
7ffd65f6b3 speckl: TypeScript state machine generator + Forgejo issue workflow spec
Some checks failed
Deploy Landing Page to Storj / deploy (push) Failing after 2s
Adds a first-class TypeScript code generator to speckl-compile that emits:
- Const enum for workflow states (IssueWorkflowState)
- Strongly-typed class with guards, state transitions, decision log
- Proper this. prefixing (state vars only, not local params)
- Enum references instead of string literals for state comparisons
- Clean tsc --noEmit compilation

Also includes:
- specs/forgejo-issue-workflow.speckdl — full workflow with 9 actions,
  8 constraints, 5 temporal verifications
- Generator deduplication of duplicate AST nodes
- Support for init block initialization of state variables

The generator was validated against the Forgejo issue workflow spec,
producing IssueWorkflow.ts that compiles with zero errors.

Refs: heartbeat conversation re: speckl-compile extensibility
2026-05-03 12:23:33 -07:00
Scott Scoble
cbee677a11 fix: support hyphenated speck names + provenance block parsing (v0.3.1)
Some checks failed
Deploy Landing Page to Storj / deploy (push) Failing after 2s
- Fixed speck name regex to allow hyphens (\w → [\w-])
- Added provenance { } block handling in parseMember()
- Updated hyphenated name test from 'My' to 'My-Service-Handler'
- All 48 tests passing (27 parser + 21 validator)
2026-05-02 23:12:27 -07:00
Scott Scoble
8facd5c6c7 Wire up compiler generators + fix parser for SpeckDL edge cases
Some checks failed
Deploy Landing Page to Storj / deploy (push) Failing after 3s
- Connected PROV-O, CycloneDX, and SPDX generators to CLI entry point
- Fixed parseAuthor regex to handle angle-bracket email format
- Fixed parseDerives to handle hyphenated names and quoted rationale
- Fixed parseSatisfies to handle hyphenated requirement IDs
- Fixed parseSource to handle ref keyword with quoted value
- Added graceful fallbacks (warn instead of throw) for parse errors
- All 5 example .speck files compile and validate successfully
2026-05-02 15:14:31 -07:00
Scott Scoble
f19a43fd5f Add SpeckDL compiler scaffold
- CLI entry point with yargs parsing for speckl-compile <file> --output-dir --bom-format
- TypeScript parser with AST types for all SpeckDL primitives
- Generator for PROV-O JSON-LD provenance graphs
- Generator for CycloneDX v1.6 BOMs
- Generator for SPDX 3.0.1 BOMs
- E2E test verifying RetryHandler.speck parsing and all output formats

All tests pass.
2026-04-29 15:12:08 -07:00