Commit graph

120 commits

Author SHA1 Message Date
Scott Scoble
0ab3174314 feat(speckl): state as <Name> message override (cycle 59)
Adds 'state as <MessageName> { ... }' syntax for the .proto generator.
When the 'as' clause is present, the generator emits
  message <MessageName> { ... }
instead of the default
  message <SpeckName>State { ... }.

Why: the federated-meetup consumer (internal/types/types.go and friends)
imports 'pb.StateSnapshot', not 'pb.FederatedMeetupState'. The previous
default of namespacing by speck name broke the migration: the generated
proto would have compiled cleanly in protoc but the consuming Go code
would not have built. With this override, the Speckl-generated proto
emits the exact message name the consumer expects.

The default behavior (no 'as' clause) is unchanged, so existing specs
that relied on the old convention (e.g. tests, examples) still work.

Tests: 2 new parser tests, both green. All 48 tests pass. tsc build clean.

Reference: .hermes/skills/spec-compiler-dogfood/references/
  speckl-federated-meetup-protobuf-migration.md
— the build break last session was caused by the missing override.
2026-06-28 21:55:54 -07:00
Scott Scoble
b65bf0e206 feat(speckl): transition envelope (cycle 58)
Adds 'transition Name { ... }' as a top-level member of a speck
block. The AST node is TransitionNode with fields[] plus optional
payloadOneof and typeDiscriminator references. Two field names
have special meaning:

  payload: <OneofName>  →  the generator will emit the referenced
                            oneof's variants inline as
                            'oneof payload { ... }' inside the
                            message body (i.e. payload becomes a
                            proto oneof, not a regular field)
  type:    <EnumName>   →  the discriminator enum for the variants

All other fields are emitted as ordinary proto message fields.

This is the shape federated-meetup needs for its Transition message:
  message Transition {
    TransitionType type = 1;
    StateRoot prior_state = 2;
    oneof payload {
      CreateGroupPayload create_group = 10;
      ...
    }
    Multisig steward_signatures = 31;
    bytes hlc = 32;
    fixed32 branch_id = 33;
    google.protobuf.Timestamp signed_at = 30;
  }

The next cycle (64) will wire the .proto generator to emit this shape
from a TransitionNode. Cycle 58 is parser-only — 3 new tests cover
regular fields, payload+type references, and trailing punctuation
tolerance. All 46 tests (39 baseline + 4 oneof + 3 transition) pass.
tsc build clean.
2026-06-28 21:53:38 -07:00
Scott Scoble
0e42961525 feat(speckl): oneof syntax for proto wire-format discriminated unions (cycle 57)
Adds 'oneof Name { field: Type, ... }' as a top-level member of a
speck block, alongside interface, event, service, etc. The AST node
is OneofNode with a variants array of { fieldName, typeName }. The
parser supports multi-line blocks, comments, and trailing commas /
semicolons. Generator integration is a follow-up cycle (proto/TS).

Motivation: federated-meetup's Transition message needs a oneof for
the 15+ payload variants (create_group, add_steward, ...). Without
oneof syntax, the consumer Go code has to hand-roll
'Transition_AddHostPeer' wrapper messages for each event type.
With oneof, the generated .proto emits a real proto3 oneof and the
generated Go bindings have a single 'isXXX()' discriminator API
that matches the consumer's expectations.

Tests: 4 new parser tests covering happy path, trailing punctuation,
comments, and coexistence with other member types. All 43 tests
(39 baseline + 4 new) pass; tsc build clean.

Reference: spec-compiler-dogfood skill, references/speckl-federated-
meetup-protobuf-migration.md — the prior build break was caused by
proto message-shape mismatches between the generated .proto and the
consumer Go code. oneof syntax is the first of 5 compiler extensions
needed to make Speckl-generated proto bindings a drop-in for the
handwritten proto/federated_meetup/v1/{state,rpc}.proto.
2026-06-28 21:49:26 -07:00
Scott Scoble
adc5b75bff feat(protobuf): honor speck.protoPackage and speck.goPackage overrides
The .proto backend previously emitted:
  package speckl.<name>.v1;
  option go_package = "github.com/sscoble/<name>/proto/.../v1;...v1";
hard-coded. Both fields are now overridable via the SpeckNode's
protoPackage / goPackage fields (populated by top-of-file metadata in
the .speckdl; see upcoming cycle 57 for the related oneof syntax which
will also be reading from the same SpeckNode).

For federated-meetup the overrides are:
  proto_package: "federated_meetup.v1"
  go_package:    "github.com/sscoble/federated-meetup/proto/...;federated_meetupv1"

The consumer Go code (internal/types/types.go, internal/group/) imports
"federated_meetup/v1" — without this override, the generated proto
would emit package "speckl.federated_meetup.v1" and the bindings
would not match the imports, breaking the consuming project's build.

Picks up a half-applied change left in the working tree from the
v0.6 review-v2 session. dist/ is gitignored; tsc build was clean
and all 39 baseline parser tests pass.
2026-06-28 21:49:19 -07:00
hermes
69f668db7c feat(speckl): protobuf backend + service block + record interface fields
- parser.ts: distinguish enum / record / service kinds in interface blocks
- parser.ts: add service { rpc X(R) returns (R); } syntax
- generators/protobuf.ts: emit proto3 (enums, messages, services) from .speckdl
- index.ts: add --target protobuf choice

Dogfood: FederatedMeetup.speckdl → 188-line .proto → buf generate →
working Go + ConnectRPC code with zero glue.

Closes speckl#61 (parser drops field declarations).
2026-06-28 01:25:54 -07:00
Scott Scoble
e6f95ddf0b fix(parser): parse multi-line input/output blocks as record types (speckl#57)
Multi-line `input: { ... }` and `output: { ... }` blocks fell through
to parseMember which returned `{ type: 'ident', name: '{' }` instead of
a record with fields. Broke RetryHandler.speck and similar real specks.

Fix: add `input:`/`output:` to blockStarters, dispatch to new
parseInputOutputBlock() that brace-counts across newlines, strips
line comments, and delegates to parseTypeExpr's record branch.

CoS-verified-live-close (cycle 126 pattern): subagent hit max_iterations
on the brace-count edge case. CoS applied focused fix + 2 new tests.
39/39 vitest pass.

Test evidence:
- RetryHandler.speck: input typeExpr.type='record' 4 fields
- 37 prior tests + 2 new = 39 passing
2026-06-09 13:53:02 -07:00
agent-engineering
d5eea7e7c7 fix(parser): multi-line verify: bodies — join depth-aware lines into temporalExpr (speckl#54)
- Add 'verify:' to the parseSpeck dispatch condition so multi-line verify:
  blocks reach the multi-line parser
- New parseVerifyColonBlock helper collects continuation lines using the
  same break-condition list as the existing skip-loop, with depth-balanced
  counter for (), [], {}
- Joins the parts with single spaces and returns a VerifyNode with a
  well-formed temporalExpr
- Closes sscoble/speckl#54 — unblocks B2 PR stack (#47 + #48 already closed)
- Pre-existing LTL inner-identifier scoping bug remains in #55 (out of scope)
2026-06-03 12:09:19 -07:00
agent-engineering
82c8bdc49b fix(speckl-48): implement verifyN() with LTL inner-expression translator (Z3 call-out, runtime-side) 2026-06-03 10:31:46 -07:00
Scott Scoble
39823c425e Add SEO attribution: author meta tag, JSON-LD structured data, 'Created by Scott Scoble' branding
Some checks failed
Deploy Landing Page to Storj / deploy (push) Failing after 3s
- Adds <meta name='author' content='Scott Scoble'> to landing page head
- Adds JSON-LD SoftwareSourceCode structured data with author, repo, license, keywords
- Updates hero subtitle to 'A Judgement Transport Utility by Scott Scoble'
- Updates OG description with 'Created by Scott Scoble'
- Updates OG site_name to 'Speckl by Scott Scoble'
- Keywords include 'scott-scoble' for name association
2026-05-23 18:14:32 -07:00
Scott Scoble
02a61f1d33 feat: add PromptOptimizer spec and functional runtime
PromptOptimizer.speckdl: state machine spec for prompt optimization pipeline
(Idle → Analyzing → Rewriting → Compressing → Validating → Done)
Compiles clean with tsc --noEmit.

PromptOptimizer-runtime.ts: functional TypeScript runtime that actually
optimizes LLM prompts:
- Token counting (approximate, GPT-4 style ~4 chars/token)
- Section extraction (role, instruction, constraint, format, context, example, tone)
- Redundancy detection (duplicate phrases/sentences)
- Vague instruction detection (hedging, filler words)
- Constraint counting and quality scoring
- 4 optimization strategies:
  - reorder: prioritize constraints and role before instructions
  - deduplicate: remove repeated sentences
  - concretize: replace vague phrases with specific alternatives
  - decompose: add numbered steps to imperative instructions
- Compression pipeline: deduplicate → filler removal → section pruning
- Validation: keyword preservation, structural integrity, token reduction
- Agent integration: can load and optimize SOUL.md/AGENTS.md files

Demo shows 8% reduction on SOUL.md, 5% on AGENTS.md (both already
well-structured). Higher gains on verbose prompts (13-30% reduction).
2026-05-13 21:14:55 -07:00
Scott Scoble
35583630cb fix: SQL optimizer runtime — predicate pushdown, FROM/JOIN dedup, cost model
- Predicate pushdown now splits AND predicates and pushes each to
  the correct side of the join (left table vs right table)
- FROM clause no longer duplicates tables that appear in JOINs
- Constant folding no longer mangles date literals (skips strings)
- Cost model: hash join uses build/probe costs, nested_loop uses
  per-row probe cost instead of cartesian product
- Physical operator selection defaults to hash join for medium+ tables
- Two-pass SQL generation: collect join tables first, then emit FROM
- Demo shows 86% cost reduction on users/orders query, 25% on
  departments/employees query from ekeric13/sql-query-optimization-guide
2026-05-13 18:06:30 -07:00
Scott Scoble
a910f07377 feat: add SQL query optimizer with functional runtime
SQLOptimizer.speckdl: state machine spec for the optimizer pipeline
(Parsing → Rewriting → Planning → Generating → Done, plus Failed)

SQLOptimizer-runtime.ts: working TypeScript runtime that actually
optimizes SQL queries:
- Parses SELECT/FROM/JOIN/WHERE/GROUP BY/ORDER BY/LIMIT
- Builds plan trees with cardinality estimation
- Predicate pushdown (splits AND predicates per table)
- Constant folding (evaluates arithmetic in predicates)
- Column pruning
- Physical operator selection (hash/merge/nested_loop joins)
- Cost estimation per plan node
- SQL generation from optimized plan tree

Known issues:
- Predicate pushdown needs to split AND predicates per table
- FROM clause duplicate when both listed and joined
- Cost model needs tuning (hash join startup cost shouldn't exceed
  nested loop savings for medium inputs)

Both files pass tsc --noEmit clean.
2026-05-13 17:00:46 -07:00
Scott Scoble
06232494ed feat: add SQL query optimizer spec (SQLOptimizer.speckdl)
Models a cost-based SQL optimizer pipeline: parse → rewrite → plan → execute.
Exercises state-dependent transforms, cost models, conditional emits,
plan caching, and rollback semantics. Passes tsc --noEmit clean.
2026-05-13 16:51:01 -07:00
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
dbde01ccb5 Iterative ternary if/else rewrite, Raft partial fix
- Replaced complex ternary regex with simpler iterative approach
- Raft: 3 errors → 9 errors (regression due to multiline let detection)
- Fixed simple single-line ternary expressions

Progress: 12 specs at 0 errors, Raft needs multiline let parsing
2026-05-11 21:30:38 -07:00
Scott Scoble
52be7b1c6d Fix SQLitePager, improve and/or rewrite, add emptySet
- SQLitePager: 4 errors → 0 errors
- Added emptySet → new Set() rewrite
- Fix and/or regex to avoid matching method calls like .or()
- Progress: 12 specs at 0 errors
2026-05-11 21:27:36 -07:00
Scott Scoble
832feb47b3 Fix SQLiteWAL: Map literals, nested bracket access, and/or, comments
- Added and/or -> &&/|| rewrite
- Strip // comments before TS processing
- Fix [a..b] range syntax to array literal
- Fix nested Map bracket access (rewrite inner expressions)
- Fix Map assignment index expression rewriting
- Convert {k: v} Map literals to new Map([[k, v]])
- SQLiteWAL: 19 errors -> 0 errors

Progress: 11 specs at 0 errors
2026-05-11 21:24:50 -07:00
Scott Scoble
7f417d37e0 Add not->! rewrite, Integer/Boolean types, ToggleSwitch 0 errors
- Added not -> ! negation rewrite (step 5d1)
- Added Integer and Boolean primitive type mappings
- ToggleSwitch: 3 errors → 0 errors
- PreconditionTest: partial fix (Integer type resolved)

Progress: 9 specs at 0 errors, 124 total remaining
2026-05-11 21:17:06 -07:00
Scott Scoble
a1efbadbd1 Preserve statement order, fix notIn with object literals, Paxos now 0 errors
- Replaced grouped statement emission with per-statement switch preserving order
- Moved notIn rewrite BEFORE object literal restoration to protect { } blocks
- Fixed if/else ternary expression regex for complex cases
- Paxos: 6 errors → 0 errors
- Total: 168 → 124 errors across 7 specs
2026-05-11 20:54:39 -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
29d4c83d76 feat: SQLite WAL concurrency model spec (speckl#36)
Some checks failed
Deploy Landing Page to Storj / deploy (push) Failing after 2s
2026-05-10 01:05:14 -07:00
0cefe0f694 fix(z3): robust = conversion + SQLite pager spec (DB.2)
Some checks failed
Deploy Landing Page to Storj / deploy (push) Failing after 2s
- Fixed infix = conversion regex: global replace replaces restrictive lookbehind version
- Also catches = inside =>, and, or bodies (not just depth 0)
- Fixed implies keyword support in expression translation
- Fixed SQLitePager.speck: implies→->, string-typed enum comparison fix
- All specs (ToggleSwitch, KafkaKRaft, SQLitePager) produce zero-error SMT-LIB2
- All 37 tests pass
2026-05-10 01:02:00 -07:00
c12f40ee7d feat: SQLite pager state machine spec (speckl#35) 2026-05-10 00:52:22 -07:00
45d82e2ea0 docs: SQLite research + blog post for Prove SQLite project
Some checks failed
Deploy Landing Page to Storj / deploy (push) Failing after 2s
- docs/db-sqlite-reference.md (32KB): pager FSM (7 states, 15 transitions),
  WAL concurrency model, ~50 VDBE opcodes, B-Tree cell layout, 37 formal invariants,
  notable CVEs, formal verification precedents
- docs/blog-07-prove-sqlite.md (1,164 words): framing blog post, all 6 sections
2026-05-10 00:49:15 -07:00
07dfdfbda0 docs: Prove SQLite project plan — pager, WAL, VDBE, B-Tree
Some checks failed
Deploy Landing Page to Storj / deploy (push) Failing after 2s
Sequel to Prove Kafka. Targets SQLite's core state machines for
formal verification: pager (transaction lifecycle, journal modes),
WAL (concurrent read/write, checkpoint), VDBE (bytecode engine),
and B-Tree (page organization, splits, merges).

12 milestones across 3 phases, documented invariants per layer.
2026-05-10 00:45:13 -07:00
34b8de549f docs: GP architecture — SIR schema, extraction protocol, validation engine, compilation layer
Some checks failed
Deploy Landing Page to Storj / deploy (push) Failing after 2s
The four design docs from the GP architecture research thread. These define Speckl's
general-purpose architecture: conversation → SIR → deterministic compile, with domain
plugins for state machines, data schemas, and workflows.

- sir-schema.md (48KB): Central IR data structure with ~20 interfaces, 8 domain element tables
- extraction-protocol.md (47KB): How conversation populates the SIR
- validation-engine.md (39KB): SIR validation before compilation
- compilation-layer.md (43KB): How validated SIRs compile to deterministic artifacts

Phase strategy: build GP core now, ship state machines first, layer data schemas
and workflows on the same architecture (no rewrites).
2026-05-09 23:46:57 -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
e86af21cc7 landing: update for Z3 backend, KRaft spec, remove WAT WASM generator
- Replace WASM pipeline artifact with Z3 Verification (SMT-LIB2)
- Add Kafka KRaft as flagship example (141 lines, 6 invariants)
- Add Status & Roadmap section (TS codegen ✅, Z3 ✅, OAuth2 ✅, Rust 🚧, WASM 📋)
- Remove WAT/WASM quickstart commands; add --target=z3 example
- Update example count to 14, include OAuth2AuthorizationCode and PreconditionTest
- Remove remaining WASM/WAT references in meta tags, comments, copy
- Keep "Don't replace Kafka. Prove it." positioning
2026-05-09 23:10:55 -07:00
506c192b77 docs: update plan with M0.3 completion and M1.2 status
Some checks failed
Deploy Landing Page to Storj / deploy (push) Failing after 2s
2026-05-09 23:10:31 -07:00
40eef36a10 feat(z3): zero-error SMT-LIB2 output + BMC verify blocks for KRaft
Some checks failed
Deploy Landing Page to Storj / deploy (push) Failing after 3s
- Declare speckl_len_Int helper for list/sequence lengths
- Fix infix = inside => bodies (final pass regex)
- Handle prime notation: currentTerm' → currentTerm_post
- Handle length() calls: length(log) → (speckl_len_Int log)
- Handle min(): (ite (<= a b) a b) instead of unsupported 'min'
- Handle subtraction: i-1 → (- i 1)
- Declare _post state vars when invariants compare pre/post
- Added 3 BMC verify blocks to KRaft spec (TermMonotonicity, CommitSafety, LeaderCompleteness)
- Z3 returns clean sat with zero errors for all specs
- All 37 tests pass
2026-05-09 23:07:56 -07:00
7e5a8fe2cb Merge branch 'feature/z3-backend'
Some checks failed
Deploy Landing Page to Storj / deploy (push) Failing after 2s
Z3 backend: clean SMT-LIB2 output, Z3 returns sat with model
KRaft spec: 4/6 invariants with real expressions
All 37 tests pass
2026-05-09 22:38:54 -07:00
25fbdfc7a9 fix(z3): clean SMT-LIB2 output — Z3 returns sat with model (zero sort errors)
- Sanitize sort names: Option(NodeId) → Option_NodeId
- Emit action transition predicates only for verify/BMC mode
- Handle -> implication operator in translateExpr
- Fleshed out KRaft invariant bodies (4/6 now have real expressions)
- ToggleSwitch: clean sat with model
- TigerBeetleLedger: sat with model
- KafkaKRaft: sat with model
- All 37 tests pass
2026-05-09 22:38:47 -07:00
Scott Scoble
c5ca757e80 Merge branch 'feature/z3-backend' (Z3 backend + KRaft spec) 2026-05-09 22:34:40 -07:00
Scott Scoble
534f13734c Merge branch 'fix/ts-generator-bugs'
# Conflicts:
#	compiler/node_modules/.vite/vitest/results.json
#	compiler/test-output/RetryHandler.prov.jsonld
#	compiler/test-output/RetryHandler.specbom.cdx.json
#	compiler/test-output/RetryHandler.specbom.spdx.json
2026-05-09 22:28:57 -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
582ef92586 feat: KRaft consensus protocol spec (speckl#23) 2026-05-09 22:19:32 -07:00
6ea0aef76b docs: update PROVE-KAFKA-PLAN with milestone completions
M0.1 ✅, M0.2 ✅, M1.1 research ✅, M3.1 draft ✅, M4.3 ✅
Next: M0.3 (Z3 backend) unblocks M1.2, M3.2, M4.3 verification
2026-05-09 22:09:27 -07:00
1cbad9d756 fix(compiler): translate Map/Set expression patterns to JavaScript (#18)
- x in someSet → someSet.has(x)
- x in someMap.keys → someMap.has(x)
- x notIn someMap.keys → !someMap.has(x)
- m[k] → m.get(k) for Map state variables
- s.size() → s.size (property, not method)
- Track Map-typed state variables via mapVarNames for accurate .get() translation
- Thread mapVarNames through emitAction and rewriteExpr

All 41 tests passing. TigerBeetleLedger now generates correct TypeScript
with .get() for Map access and .has() for Set membership.

Part of M0.1: Fix TS generator bugs (speckl#18)
2026-05-09 22:07:32 -07:00
00dd745ef2 refactor: remove WAT/WASM generator (superseded by IR→Rust→WASM path)
- Deleted compiler/src/generators/wasm.ts (472 lines)
- Deleted compiler/src/runtime/wasm-host.ts (165 lines)
- Deleted compiler/__tests__/e2e-wasm.test.ts (203 lines)
- Removed WASM import and generation call from compiler/src/index.ts
- Removed WASMGenerated from TS generator state enum literals
- Removed WASM codegen tests from parser.test.ts
- All 37 tests passing

The WASM generator was architecturally wrong: every Map/Set operation
crossed the WASM→JS boundary, creating 45-55% overhead for a module
that doesn't compute anything. WASM will be a byproduct of the Rust
backend via wasm-pack instead (M2.1).

Closes #19
2026-05-09 22:03:20 -07:00
Scott Scoble
03de892259 docs: comprehensive KRaft protocol reference for speckl#22
M1.1 research deliverable — detailed reference document covering:

- Complete Raft state machine (TLA+ spec): 10 actions with preconditions
- KRaft state hierarchy: 7 states (Unattached, Prospective, Candidate,
  Follower, Leader, Resigned, Detached) with per-state variables
- Detailed transition table with triggers and preconditions
- Pre-Vote protocol (KIP-996) mechanics and verification targets
- Resignation protocol (graceful leader step-down)
- 6 vanilla Raft invariants (I1-I6) formalized for Z3
- 6 KRaft-specific invariants (K1-K6) including observer consistency
- Snapshot invariants (KIP-630)
- 4 known Raft/KRaft bugs with verification targets
- 7 open verification targets for SpeckDL/Z3
- Producer acks and consumer group semantics (deferred to M1.3)
- Message types and KIP reference table
2026-05-09 21:54:09 -07:00
14cd892e8a feat: OAuth 2.0 authorization code flow with PKCE spec 2026-05-09 21:51:51 -07:00
1d536136b8 docs: KRaft protocol reference for M1.1 spec writing 2026-05-09 21:51:35 -07:00
6e770de885 =docs: add issue tracking table (#18-#32), close epic #17 2026-05-09 21:43:18 -07:00
7928c2b1da docs: Prove Kafka project plan (4 phases, 12 milestones, dependency graph only) 2026-05-09 21:40:21 -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
c3ade18feb fix(parser): parse parenthetical type syntax Map(K,V), Set(T), List(T)
parseTypeExpr only handled angle-bracket generics (Map<K,V>, Set<T>, List<T>)
but SpeckDL canonical syntax uses parentheses: Map(Nat, Account), Set(Nat), List(LogEntry).

This caused two bugs:
1. State property types emitted as raw strings (accounts: Map(Nat, Account))
2. Parametric types treated as enum interface names (TigerBeetleLedgerMap(Nat, Account))

Added List(T), Set(T), Map(K,V) handlers alongside existing angle-bracket handlers.
All 41/41 tests passing. TigerBeetle now generates clean TS types:
- accounts: Map<number, Account> (was Map(Nat, Account))
- pending: Set<number> (was Set(Nat))
- log: LogEntry[] (was List(LogEntry))
2026-05-09 18:09:31 -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
9de0a5ca0f feat(compiler): parse precondition/postcondition in action blocks
- Add 'precondition' and 'postcondition' ActionStatement types
- Parse precondition: expr and postcondition: expr in action bodies
- Support 'or' continuation lines for multi-clause pre/postconditions
- TigerBeetleLedger now parses 21 preconditions + 24 postconditions
  (previously all dropped, resulting in empty action bodies)
- All 41 existing tests pass

Addresses marcus/engineering#9 (parser gap)
Does NOT wire into generators yet — TypeScript/WASM output
will be empty for pre/postconditions. Generator wiring
is follow-up work.
2026-05-09 09:12:15 -07:00