diff --git a/README.md b/README.md index 72b9b80..f3b2ebf 100644 --- a/README.md +++ b/README.md @@ -2,7 +2,7 @@ **A judgement transport utility for AI-generated specifications.** Fulfills NIST SA-11 (human-in-the-loop for automated outputs). -Speckl is a specification language (SpeckDL) with a compiler that produces runnable software — WebAssembly, TypeScript, and provenance artifacts (PROV-O, CycloneDX, SPDX) — from a single source of truth. Write what your system should do. Prove it. Ship it. +Speckl is a specification language (SpeckDL) with a compiler that produces runnable software — TypeScript and provenance artifacts (PROV-O, CycloneDX, SPDX) — from a single source of truth. Write what your system should do. Prove it. Ship it. ## The Core Insight @@ -17,8 +17,7 @@ AI generates code at machine speed. Humans own specifications. **SpeckDL is the Speckl is a **working compiler** that turns formal specifications into multiple target representations: ``` -.speckdl spec ──→ Wasm (WebAssembly) ← runnable, verified state machines - ├── TypeScript ← typed, importable classes +.speckdl spec ──→ TypeScript ← typed, importable classes ├── PROV-O (RDF) ← W3C provenance standard ├── CycloneDX SBOM ← OWASP software bill of materials └── SPDX SBOM ← Linux Foundation SBOM standard @@ -46,7 +45,7 @@ spec ToggleSwitch { } ``` -This compiles to a runnable WebAssembly module with verified state transitions + guards, and to a type-safe TypeScript class. Both from the same spec. +This compiles to a runnable TypeScript class with verified state transitions + guards. ### Provenance Embedded at Compile Time @@ -58,12 +57,12 @@ The compiler has been validated against: | Example | Source | Status | |---------|--------|--------| -| **ToggleSwitch** | SpeckDL tutorial | ✅ All 5 artifacts | -| **AccountLedger** | Banking ledger with debit/credit | ✅ All 5 artifacts | -| **TwoPhaseCommit** | TLA+ port | ✅ All 5 artifacts | -| **Paxos** | TLA+ port | ✅ All 5 artifacts | -| **Raft** | TLA+ port | ✅ All 5 artifacts | -| **TigerBeetleLedger** | Naive TigerBeetle core | ✅ All 5 artifacts (3 TS type errors in progress) | +| **ToggleSwitch** | SpeckDL tutorial | ✅ All artifacts | +| **AccountLedger** | Banking ledger with debit/credit | ✅ All artifacts | +| **TwoPhaseCommit** | TLA+ port | ✅ All artifacts | +| **Paxos** | TLA+ port | ✅ All artifacts | +| **Raft** | TLA+ port | ✅ All artifacts | +| **TigerBeetleLedger** | Naive TigerBeetle core | ✅ All artifacts (3 TS type errors in progress) | ## Getting Started @@ -72,10 +71,10 @@ git clone https://os.scoble.me/forgejo/sscoble/speckl cd speckl/compiler npm install -# Compile an example to all 5 targets +# Compile an example node dist/index.js ../examples/ToggleSwitch.speck -o out/switch ls out/switch/ -# ToggleSwitch.wat ToggleSwitch.ts ToggleSwitch.prov-o.jsonld +# ToggleSwitch.ts ToggleSwitch.prov-o.jsonld # ToggleSwitch.cyclonedx.json ToggleSwitch.spdx.json ``` @@ -99,11 +98,10 @@ ls out/switch/ ## Validation Status -- **Compiler:** 41/41 tests passing (WASM + TypeScript codegen) -- **WASM E2E:** wabt assemble + instantiate + run verified -- **TypeScript:** Dual-target compilation — same spec produces both WASM and TS -- **TLA+ Trilogy:** TwoPhaseCommit, Paxos, Raft all compile (WAT validates through wabt) -- **Compiler Self-Spec:** `speckl-compile.speckdl` defines the Speckl compiler in SpeckDL — generates all 5 artifacts (known TypeScript errors tracked in engineering#9) +- **Compiler:** 41/41 tests passing (TypeScript codegen) +- **TypeScript:** Type-safe compilation from specs +- **TLA+ Trilogy:** TwoPhaseCommit, Paxos, Raft all compile +- **Compiler Self-Spec:** `speckl-compile.speckdl` defines the Speckl compiler in SpeckDL — generates all artifacts (known TypeScript errors tracked in engineering#9) ## Known Issues diff --git a/compiler/__tests__/e2e-wasm.test.ts b/compiler/__tests__/e2e-wasm.test.ts deleted file mode 100644 index aef5625..0000000 --- a/compiler/__tests__/e2e-wasm.test.ts +++ /dev/null @@ -1,203 +0,0 @@ -import { describe, it, expect } from 'vitest'; -import { parseSpeckContent } from '../src/parser.js'; -import { generateWASM } from '../src/generators/wasm.js'; -import { createHostImports, bindMemory, readScalarState } from '../src/runtime/wasm-host.js'; -import fs from 'fs'; -import path from 'path'; -import os from 'os'; - -// Dynamic import wabt since it's a CommonJS module -async function loadWabt() { - const wabt = await import('wabt'); - return wabt.default(); -} - -describe('SpeckDL WASM E2E', () => { - it('should compile Counter speck to WAT, assemble to WASM, and run in Node.js', async () => { - // A minimal scalar-only speck that we can fully compile and run - // NOTE: Parser requires braces on the SAME line as block keywords - const speckSource = `speck Counter { - author: "Speckl Compiler v0.3" - source: document ref "WASM-E2E" - review: automated - - state: { - count: Nat := 0 - maxCount: Nat := 10 - } - - init: { - count := 0 - maxCount := 10 - } - - action Increment() { - require count < maxCount - count := count + 1 - } - - action Decrement() { - require count > 0 - count := count - 1 - } - - action Reset() { - count := 0 - } - - action GetCount() { - return count - } -}`; - - // 1. Parse - const ast = parseSpeckContent(speckSource); - expect(ast.specks).toHaveLength(1); - expect(ast.specks[0].name).toBe('Counter'); - - // 2. Generate WAT to temp dir - const tmpDir = fs.mkdtempSync(path.join(os.tmpdir(), 'speckl-wasm-e2e-')); - generateWASM(ast, tmpDir); - - const watPath = path.join(tmpDir, 'Counter.wat'); - expect(fs.existsSync(watPath)).toBe(true); - - const watContent = fs.readFileSync(watPath, 'utf-8'); - expect(watContent).toContain('(module'); - expect(watContent).toContain('(export "init")'); - expect(watContent).toContain('(export "Increment")'); - expect(watContent).toContain('(export "Decrement")'); - expect(watContent).toContain('(export "Reset")'); - expect(watContent).toContain('(export "GetCount")'); - expect(watContent).toContain('(export "getState")'); - expect(watContent).toContain('(export "memory")'); - - // 3. Assemble WAT → WASM using wabt - const wabtModule = await loadWabt(); - const wasmModule = wabtModule.parseWat('Counter.wat', watContent); - wasmModule.resolveNames(); - wasmModule.validate({ features: {} }); - const binaryOutput = wasmModule.toBinary({ log: false, write_debug_names: false }); - const wasmBytes = binaryOutput.buffer; - - expect(wasmBytes.length).toBeGreaterThan(0); - expect(wasmBytes.length).toBeGreaterThan(50); // Not just empty header - - // 4. Instantiate with host runtime - const hostState = { - maps: new Map(), - sets: new Map(), - nextHandle: 1, - memory: null as WebAssembly.Memory | null, - }; - const imports = { speckl: createHostImports(hostState) }; - - const wasm = await WebAssembly.instantiate(wasmBytes, imports); - const memory = wasm.instance.exports.memory as WebAssembly.Memory; - bindMemory(hostState, memory); - - // 5. Verify exports - expect(typeof wasm.instance.exports.init).toBe('function'); - expect(typeof wasm.instance.exports.Increment).toBe('function'); - expect(typeof wasm.instance.exports.Decrement).toBe('function'); - expect(typeof wasm.instance.exports.Reset).toBe('function'); - expect(typeof wasm.instance.exports.GetCount).toBe('function'); - expect(typeof wasm.instance.exports.getState).toBe('function'); - expect(memory).toBeInstanceOf(WebAssembly.Memory); - - // 6. Run init - (wasm.instance.exports.init as Function)(); - - // 7. Verify initial state via getState - const stateResult = (wasm.instance.exports.getState as Function)(); - // getState returns i32 i32 (ptr, len) - expect(stateResult).toBeDefined(); - - // Read memory directly to verify state - const scalarState = readScalarState(memory, ['count', 'maxCount']); - expect(scalarState.count).toBe(0); - expect(scalarState.maxCount).toBe(10); - - // 8. Run Increment 3 times, calling getState after each to sync memory - for (let i = 0; i < 3; i++) { - const ret = (wasm.instance.exports.Increment as Function)(); - expect(ret).toBe(1); // Success - (wasm.instance.exports.getState as Function)(); // Sync globals to memory - } - - const afterIncrement = readScalarState(memory, ['count', 'maxCount']); - expect(afterIncrement.count).toBe(3); - expect(afterIncrement.maxCount).toBe(10); - - // 9. Run Decrement once - const decRet = (wasm.instance.exports.Decrement as Function)(); - expect(decRet).toBe(1); // Success - (wasm.instance.exports.getState as Function)(); - - const afterDecrement = readScalarState(memory, ['count', 'maxCount']); - expect(afterDecrement.count).toBe(2); - - // 10. Run GetCount — should return current count (global, not memory) - const getRet = (wasm.instance.exports.GetCount as Function)(); - expect(getRet).toBe(2); - - // 11. Run Reset - const resetRet = (wasm.instance.exports.Reset as Function)(); - expect(resetRet).toBe(1); // Success - (wasm.instance.exports.getState as Function)(); - - const afterReset = readScalarState(memory, ['count', 'maxCount']); - expect(afterReset.count).toBe(0); - - // 12. Guard test: Decrement at 0 should fail - const guardFail = (wasm.instance.exports.Decrement as Function)(); - expect(guardFail).toBe(0); // Guard failed → return 0 - - // 13. Guard test: Increment at maxCount should fail - // First increment to max - for (let i = 0; i < 10; i++) { - (wasm.instance.exports.Increment as Function)(); - } - (wasm.instance.exports.getState as Function)(); - const atMax = readScalarState(memory, ['count', 'maxCount']); - expect(atMax.count).toBe(10); - - const maxGuardFail = (wasm.instance.exports.Increment as Function)(); - expect(maxGuardFail).toBe(0); // Guard failed → return 0 - - // Cleanup - fs.rmSync(tmpDir, { recursive: true, force: true }); - }, 30000); // 30s timeout for wabt compilation - - it('should compile TigerBeetle speck to valid WAT that wabt accepts', async () => { - // Load the full TigerBeetle speck from file - const speckPath = path.join(__dirname, 'tigerbeetle.speck'); - const speckSource = fs.readFileSync(speckPath, 'utf-8'); - - const ast = parseSpeckContent(speckSource); - expect(ast.specks).toHaveLength(1); - expect(ast.specks[0].name).toBe('TigerBeetle'); - - const tmpDir = fs.mkdtempSync(path.join(os.tmpdir(), 'speckl-wasm-e2e-tb-')); - generateWASM(ast, tmpDir); - - const watPath = path.join(tmpDir, 'TigerBeetle.wat'); - expect(fs.existsSync(watPath)).toBe(true); - - const watContent = fs.readFileSync(watPath, 'utf-8'); - - // Validate with wabt - const wabtModule = await loadWabt(); - const wasmModule = wabtModule.parseWat('TigerBeetle.wat', watContent); - - // These should not throw - wasmModule.resolveNames(); - wasmModule.validate({ features: {} }); - const binaryOutput = wasmModule.toBinary({ log: false, write_debug_names: false }); - - expect(binaryOutput.buffer.length).toBeGreaterThan(100); - - // Cleanup - fs.rmSync(tmpDir, { recursive: true, force: true }); - }, 30000); -}); diff --git a/compiler/__tests__/parser.test.ts b/compiler/__tests__/parser.test.ts index 58af7b0..e16b091 100644 --- a/compiler/__tests__/parser.test.ts +++ b/compiler/__tests__/parser.test.ts @@ -1,6 +1,5 @@ import { describe, it, expect } from 'vitest'; import { parseSpeckContent, parseSpeckFile } from '../src/parser.js'; -import { generateWASM } from '../src/generators/wasm.js'; describe('SpeckDL Parser', () => { describe('parseSpeckContent', () => { @@ -525,76 +524,4 @@ speck Second { } }); }); - - describe('WASM Codegen', () => { - it('should generate WAT for TigerBeetle with all exports', () => { - const ast = parseSpeckFile('./__tests__/tigerbeetle.speck'); - const fs = require('fs'); - const os = require('os'); - const path = require('path'); - const tmpDir = fs.mkdtempSync(path.join(os.tmpdir(), 'speckl-wasm-test-')); - - generateWASM(ast, tmpDir); - - const watPath = path.join(tmpDir, 'TigerBeetle.wat'); - expect(fs.existsSync(watPath)).toBe(true); - - const wat = fs.readFileSync(watPath, 'utf-8'); - - // Module structure - expect(wat).toContain('(module'); - expect(wat).toContain('(memory (export "memory")'); - - // Host imports - expect(wat).toContain('(import "speckl" "map_create"'); - expect(wat).toContain('(import "speckl" "set_create"'); - - // State globals - expect(wat).toContain('(global $nextId'); - expect(wat).toContain('(global $accounts'); - expect(wat).toContain('(global $transfers'); - expect(wat).toContain('(global $ledgerOpen'); - - // init export - expect(wat).toContain('(func $init (export "init")'); - - // Action exports - expect(wat).toContain('(func $CreateAccount (export "CreateAccount")'); - expect(wat).toContain('(func $Transfer (export "Transfer")'); - expect(wat).toContain('(func $CloseAccount (export "CloseAccount")'); - expect(wat).toContain('(func $CloseLedger (export "CloseLedger")'); - - // getState export - expect(wat).toContain('(func $getState (export "getState")'); - - // Constraint stub - expect(wat).toContain('(func $checkConstraints (export "checkConstraints")'); - - // Scalar init values - expect(wat).toContain('(i32.const 1)'); // nextId default - expect(wat).toContain('(call $map_create)'); - expect(wat).toContain('(call $set_create)'); - - fs.rmSync(tmpDir, { recursive: true }); - }); - - it('should emit scalar guard expressions as WASM comparison', () => { - const ast = parseSpeckFile('./__tests__/tigerbeetle.speck'); - const fs = require('fs'); - const os = require('os'); - const path = require('path'); - const tmpDir = fs.mkdtempSync(path.join(os.tmpdir(), 'speckl-wasm-test-')); - - generateWASM(ast, tmpDir); - const wat = fs.readFileSync(path.join(tmpDir, 'TigerBeetle.wat'), 'utf-8'); - - // ledgerOpen == true should compile to i32.eq - expect(wat).toContain('(i32.eq (global.get $ledgerOpen) (i32.const 1))'); - - // nextId + 1 should compile to i32.add - expect(wat).toContain('(i32.add (global.get $nextId) (i32.const 1))'); - - fs.rmSync(tmpDir, { recursive: true }); - }); - }); }); diff --git a/compiler/dist/index.js b/compiler/dist/index.js index 8b381dd..fd84422 100644 --- a/compiler/dist/index.js +++ b/compiler/dist/index.js @@ -6,7 +6,6 @@ import { generateProvenanceGraph } from './generators/provenance.js'; import { generateCycloneDX } from './generators/cyclonedx.js'; import { generateSPDX } from './generators/spdx.js'; import { generateTypeScriptStateMachine } from './generators/typescript-state-machine.js'; -import { generateWASM } from './generators/wasm.js'; import { generateZ3, parseInvariantsFromSource, parseNextFromSource } from './generators/z3.js'; import fs from 'fs'; import path from 'path'; @@ -102,9 +101,6 @@ async function main() { if (options.target !== 'z3') { console.log('\nGenerating TypeScript state machine...'); generateTypeScriptStateMachine(ast, options.outputDir); - // Generate WASM state machine - console.log('\nGenerating WebAssembly (WAT)...'); - generateWASM(ast, options.outputDir); // Generate BOM based on format selection if (options.bomFormat === 'cdx' || options.bomFormat === 'both') { console.log('\nGenerating CycloneDX BOM...'); diff --git a/compiler/dist/index.js.map b/compiler/dist/index.js.map index 9bf7dac..89612d3 100644 --- a/compiler/dist/index.js.map +++ b/compiler/dist/index.js.map @@ -1 +1 @@ -{"version":3,"file":"index.js","sourceRoot":"","sources":["../src/index.ts"],"names":[],"mappings":";AAEA,OAAO,KAAK,MAAM,OAAO,CAAC;AAC1B,OAAO,EAAE,OAAO,EAAE,MAAM,eAAe,CAAC;AACxC,OAAO,EAAE,cAAc,EAAE,MAAM,aAAa,CAAC;AAC7C,OAAO,EAAE,uBAAuB,EAAE,MAAM,4BAA4B,CAAC;AACrE,OAAO,EAAE,iBAAiB,EAAE,MAAM,2BAA2B,CAAC;AAC9D,OAAO,EAAE,YAAY,EAAE,MAAM,sBAAsB,CAAC;AACpD,OAAO,EAAE,8BAA8B,EAAE,MAAM,0CAA0C,CAAC;AAC1F,OAAO,EAAE,YAAY,EAAE,MAAM,sBAAsB,CAAC;AACpD,OAAO,EAAE,UAAU,EAAa,yBAAyB,EAAE,mBAAmB,EAAE,MAAM,oBAAoB,CAAC;AAC3G,OAAO,EAAE,MAAM,IAAI,CAAC;AACpB,OAAO,IAAI,MAAM,MAAM,CAAC;AASxB,KAAK,UAAU,IAAI;IACjB,uDAAuD;IACvD,MAAM,WAAW,GAAG,IAAI,CAAC,IAAI,CAAC,IAAI,CAAC,OAAO,CAAC,IAAI,GAAG,CAAC,MAAM,CAAC,IAAI,CAAC,GAAG,CAAC,CAAC,QAAQ,CAAC,EAAE,IAAI,EAAE,eAAe,CAAC,CAAC;IACtG,IAAI,EAAE,CAAC,UAAU,CAAC,WAAW,CAAC,EAAE,CAAC;QAC/B,IAAI,CAAC;YACH,MAAM,EAAE,QAAQ,EAAE,GAAG,MAAM,MAAM,CAAC,eAAe,CAAC,CAAC;YACnD,QAAQ,CAAC,SAAS,WAAW,GAAG,EAAE,EAAE,KAAK,EAAE,SAAS,EAAE,CAAC,CAAC;QAC1D,CAAC;QAAC,MAAM,CAAC;YACP,OAAO,CAAC,KAAK,CAAC,oDAAoD,CAAC,CAAC;YACpE,OAAO,CAAC,IAAI,CAAC,CAAC,CAAC,CAAC;QAClB,CAAC;IACH,CAAC;IAED,MAAM,IAAI,GAAG,MAAM,KAAK,CAAC,OAAO,CAAC,OAAO,CAAC,IAAI,CAAC,CAAC;SAC5C,OAAO,CAAC,WAAW,EAAE,iCAAiC,EAAE,CAAC,QAAQ,EAAE,EAAE;QACpE,OAAO,QAAQ;aACZ,UAAU,CAAC,MAAM,EAAE;YAClB,QAAQ,EAAE,yBAAyB;YACnC,IAAI,EAAE,QAAQ;YACd,YAAY,EAAE,IAAI;SACnB,CAAC;aACD,MAAM,CAAC,YAAY,EAAE;YACpB,KAAK,EAAE,GAAG;YACV,QAAQ,EAAE,yCAAyC;YACnD,IAAI,EAAE,QAAQ;YACd,OAAO,EAAE,OAAO;SACjB,CAAC;aACD,MAAM,CAAC,QAAQ,EAAE;YAChB,KAAK,EAAE,GAAG;YACV,QAAQ,EAAE,oBAAoB;YAC9B,IAAI,EAAE,QAAQ;YACd,OAAO,EAAE,CAAC,YAAY,EAAE,IAAI,EAAE,KAAK,CAAC;YACpC,OAAO,EAAE,YAAqB;SAC/B,CAAC;aACD,MAAM,CAAC,cAAc,EAAE;YACtB,KAAK,EAAE,GAAG;YACV,QAAQ,EAAE,kDAAkD;YAC5D,IAAI,EAAE,QAAQ;YACd,OAAO,EAAE,EAAE;SACZ,CAAC;aACD,MAAM,CAAC,YAAY,EAAE;YACpB,KAAK,EAAE,GAAG;YACV,QAAQ,EAAE,mBAAmB;YAC7B,IAAI,EAAE,QAAQ;YACd,OAAO,EAAE,CAAC,KAAK,EAAE,MAAM,EAAE,MAAM,CAAC;YAChC,OAAO,EAAE,MAAe;SACzB,CAAC,CAAC;IACP,CAAC,CAAC;SACD,IAAI,EAAE;SACN,IAAI,CAAC;IAER,MAAM,IAAI,GAAG,IAAI,CAAC,IAAc,CAAC;IACjC,MAAM,OAAO,GAAG;QACd,SAAS,EAAE,IAAI,CAAC,SAAmB;QACnC,SAAS,EAAE,IAAI,CAAC,SAAoC;QACpD,MAAM,EAAE,IAAI,CAAC,MAAqC;QAClD,WAAW,EAAE,IAAI,CAAC,WAAqB;KACxC,CAAC;IAEF,OAAO,CAAC,GAAG,CAAC,aAAa,IAAI,KAAK,CAAC,CAAC;IAEpC,uBAAuB;IACvB,MAAM,GAAG,GAAG,cAAc,CAAC,IAAI,CAAC,CAAC;IAEjC,MAAM,UAAU,GAAG,GAAG,CAAC,MAAM,CAAC,MAAM,CAAC;IACrC,MAAM,WAAW,GAAG,GAAG,CAAC,MAAM,CAAC,MAAM,CAAC,CAAC,GAAG,EAAE,CAAC,EAAE,EAAE,CAAC,GAAG,GAAG,CAAC,CAAC,OAAO,CAAC,MAAM,EAAE,CAAC,CAAC,CAAC;IAC7E,OAAO,CAAC,GAAG,CAAC,4BAA4B,UAAU,cAAc,WAAW,YAAY,CAAC,CAAC;IAEzF,iCAAiC;IACjC,IAAI,CAAC,EAAE,CAAC,UAAU,CAAC,OAAO,CAAC,SAAS,CAAC,EAAE,CAAC;QACtC,EAAE,CAAC,SAAS,CAAC,OAAO,CAAC,SAAS,EAAE,EAAE,SAAS,EAAE,IAAI,EAAE,CAAC,CAAC;IACvD,CAAC;IAED,oFAAoF;IACpF,MAAM,SAAS,GAAG,EAAE,CAAC,YAAY,CAAC,IAAI,EAAE,OAAO,CAAC,CAAC;IAEjD,mEAAmE;IACnE,IAAI,OAAO,CAAC,MAAM,KAAK,IAAI,EAAE,CAAC;QAC5B,OAAO,CAAC,GAAG,CAAC,mDAAmD,CAAC,CAAC;QACjE,uBAAuB,CAAC,GAAG,EAAE,OAAO,CAAC,SAAS,CAAC,CAAC;IAClD,CAAC;IAED,8CAA8C;IAC9C,IAAI,OAAO,CAAC,MAAM,KAAK,IAAI,IAAI,OAAO,CAAC,MAAM,KAAK,KAAK,EAAE,CAAC;QACxD,OAAO,CAAC,GAAG,CAAC,6BAA6B,CAAC,CAAC;QAC3C,kDAAkD;QAClD,KAAK,MAAM,KAAK,IAAI,GAAG,CAAC,MAAM,EAAE,CAAC;YAC/B,MAAM,UAAU,GAAG,yBAAyB,CAAC,SAAS,EAAE,KAAK,CAAC,IAAI,CAAC,CAAC;YACpE,MAAM,QAAQ,GAAG,mBAAmB,CAAC,SAAS,EAAE,KAAK,CAAC,IAAI,CAAC,CAAC;YAC5D,kDAAkD;YACjD,KAAa,CAAC,WAAW,GAAG,UAAU,CAAC;YACvC,KAAa,CAAC,KAAK,GAAG,QAAQ,CAAC;QAClC,CAAC;QACD,MAAM,SAAS,GAAc,EAAE,WAAW,EAAE,OAAO,CAAC,WAAW,EAAE,CAAC;QAClE,UAAU,CAAC,GAAG,EAAE,OAAO,CAAC,SAAS,EAAE,SAAS,CAAC,CAAC;IAChD,CAAC;IAED,mDAAmD;IACnD,IAAI,OAAO,CAAC,MAAM,KAAK,IAAI,EAAE,CAAC;QAC5B,OAAO,CAAC,GAAG,CAAC,0CAA0C,CAAC,CAAC;QACxD,8BAA8B,CAAC,GAAG,EAAE,OAAO,CAAC,SAAS,CAAC,CAAC;QAEvD,8BAA8B;QAC9B,OAAO,CAAC,GAAG,CAAC,mCAAmC,CAAC,CAAC;QACjD,YAAY,CAAC,GAAG,EAAE,OAAO,CAAC,SAAS,CAAC,CAAC;QAErC,yCAAyC;QACzC,IAAI,OAAO,CAAC,SAAS,KAAK,KAAK,IAAI,OAAO,CAAC,SAAS,KAAK,MAAM,EAAE,CAAC;YAChE,OAAO,CAAC,GAAG,CAAC,+BAA+B,CAAC,CAAC;YAC7C,iBAAiB,CAAC,GAAG,EAAE,OAAO,CAAC,SAAS,CAAC,CAAC;QAC5C,CAAC;QAED,IAAI,OAAO,CAAC,SAAS,KAAK,MAAM,IAAI,OAAO,CAAC,SAAS,KAAK,MAAM,EAAE,CAAC;YACjE,OAAO,CAAC,GAAG,CAAC,0BAA0B,CAAC,CAAC;YACxC,YAAY,CAAC,GAAG,EAAE,OAAO,CAAC,SAAS,CAAC,CAAC;QACvC,CAAC;IACH,CAAC;IAED,OAAO,CAAC,GAAG,CAAC,mCAAmC,OAAO,CAAC,SAAS,GAAG,CAAC,CAAC;AACvE,CAAC;AAED,IAAI,EAAE,CAAC,KAAK,CAAC,CAAC,GAAG,EAAE,EAAE;IACnB,OAAO,CAAC,KAAK,CAAC,qBAAqB,EAAE,GAAG,CAAC,CAAC;IAC1C,OAAO,CAAC,IAAI,CAAC,CAAC,CAAC,CAAC;AAClB,CAAC,CAAC,CAAC"} \ No newline at end of file +{"version":3,"file":"index.js","sourceRoot":"","sources":["../src/index.ts"],"names":[],"mappings":";AAEA,OAAO,KAAK,MAAM,OAAO,CAAC;AAC1B,OAAO,EAAE,OAAO,EAAE,MAAM,eAAe,CAAC;AACxC,OAAO,EAAE,cAAc,EAAE,MAAM,aAAa,CAAC;AAC7C,OAAO,EAAE,uBAAuB,EAAE,MAAM,4BAA4B,CAAC;AACrE,OAAO,EAAE,iBAAiB,EAAE,MAAM,2BAA2B,CAAC;AAC9D,OAAO,EAAE,YAAY,EAAE,MAAM,sBAAsB,CAAC;AACpD,OAAO,EAAE,8BAA8B,EAAE,MAAM,0CAA0C,CAAC;AAC1F,OAAO,EAAE,UAAU,EAAa,yBAAyB,EAAE,mBAAmB,EAAE,MAAM,oBAAoB,CAAC;AAC3G,OAAO,EAAE,MAAM,IAAI,CAAC;AACpB,OAAO,IAAI,MAAM,MAAM,CAAC;AASxB,KAAK,UAAU,IAAI;IACjB,uDAAuD;IACvD,MAAM,WAAW,GAAG,IAAI,CAAC,IAAI,CAAC,IAAI,CAAC,OAAO,CAAC,IAAI,GAAG,CAAC,MAAM,CAAC,IAAI,CAAC,GAAG,CAAC,CAAC,QAAQ,CAAC,EAAE,IAAI,EAAE,eAAe,CAAC,CAAC;IACtG,IAAI,EAAE,CAAC,UAAU,CAAC,WAAW,CAAC,EAAE,CAAC;QAC/B,IAAI,CAAC;YACH,MAAM,EAAE,QAAQ,EAAE,GAAG,MAAM,MAAM,CAAC,eAAe,CAAC,CAAC;YACnD,QAAQ,CAAC,SAAS,WAAW,GAAG,EAAE,EAAE,KAAK,EAAE,SAAS,EAAE,CAAC,CAAC;QAC1D,CAAC;QAAC,MAAM,CAAC;YACP,OAAO,CAAC,KAAK,CAAC,oDAAoD,CAAC,CAAC;YACpE,OAAO,CAAC,IAAI,CAAC,CAAC,CAAC,CAAC;QAClB,CAAC;IACH,CAAC;IAED,MAAM,IAAI,GAAG,MAAM,KAAK,CAAC,OAAO,CAAC,OAAO,CAAC,IAAI,CAAC,CAAC;SAC5C,OAAO,CAAC,WAAW,EAAE,iCAAiC,EAAE,CAAC,QAAQ,EAAE,EAAE;QACpE,OAAO,QAAQ;aACZ,UAAU,CAAC,MAAM,EAAE;YAClB,QAAQ,EAAE,yBAAyB;YACnC,IAAI,EAAE,QAAQ;YACd,YAAY,EAAE,IAAI;SACnB,CAAC;aACD,MAAM,CAAC,YAAY,EAAE;YACpB,KAAK,EAAE,GAAG;YACV,QAAQ,EAAE,yCAAyC;YACnD,IAAI,EAAE,QAAQ;YACd,OAAO,EAAE,OAAO;SACjB,CAAC;aACD,MAAM,CAAC,QAAQ,EAAE;YAChB,KAAK,EAAE,GAAG;YACV,QAAQ,EAAE,oBAAoB;YAC9B,IAAI,EAAE,QAAQ;YACd,OAAO,EAAE,CAAC,YAAY,EAAE,IAAI,EAAE,KAAK,CAAC;YACpC,OAAO,EAAE,YAAqB;SAC/B,CAAC;aACD,MAAM,CAAC,cAAc,EAAE;YACtB,KAAK,EAAE,GAAG;YACV,QAAQ,EAAE,kDAAkD;YAC5D,IAAI,EAAE,QAAQ;YACd,OAAO,EAAE,EAAE;SACZ,CAAC;aACD,MAAM,CAAC,YAAY,EAAE;YACpB,KAAK,EAAE,GAAG;YACV,QAAQ,EAAE,mBAAmB;YAC7B,IAAI,EAAE,QAAQ;YACd,OAAO,EAAE,CAAC,KAAK,EAAE,MAAM,EAAE,MAAM,CAAC;YAChC,OAAO,EAAE,MAAe;SACzB,CAAC,CAAC;IACP,CAAC,CAAC;SACD,IAAI,EAAE;SACN,IAAI,CAAC;IAER,MAAM,IAAI,GAAG,IAAI,CAAC,IAAc,CAAC;IACjC,MAAM,OAAO,GAAG;QACd,SAAS,EAAE,IAAI,CAAC,SAAmB;QACnC,SAAS,EAAE,IAAI,CAAC,SAAoC;QACpD,MAAM,EAAE,IAAI,CAAC,MAAqC;QAClD,WAAW,EAAE,IAAI,CAAC,WAAqB;KACxC,CAAC;IAEF,OAAO,CAAC,GAAG,CAAC,aAAa,IAAI,KAAK,CAAC,CAAC;IAEpC,uBAAuB;IACvB,MAAM,GAAG,GAAG,cAAc,CAAC,IAAI,CAAC,CAAC;IAEjC,MAAM,UAAU,GAAG,GAAG,CAAC,MAAM,CAAC,MAAM,CAAC;IACrC,MAAM,WAAW,GAAG,GAAG,CAAC,MAAM,CAAC,MAAM,CAAC,CAAC,GAAG,EAAE,CAAC,EAAE,EAAE,CAAC,GAAG,GAAG,CAAC,CAAC,OAAO,CAAC,MAAM,EAAE,CAAC,CAAC,CAAC;IAC7E,OAAO,CAAC,GAAG,CAAC,4BAA4B,UAAU,cAAc,WAAW,YAAY,CAAC,CAAC;IAEzF,iCAAiC;IACjC,IAAI,CAAC,EAAE,CAAC,UAAU,CAAC,OAAO,CAAC,SAAS,CAAC,EAAE,CAAC;QACtC,EAAE,CAAC,SAAS,CAAC,OAAO,CAAC,SAAS,EAAE,EAAE,SAAS,EAAE,IAAI,EAAE,CAAC,CAAC;IACvD,CAAC;IAED,oFAAoF;IACpF,MAAM,SAAS,GAAG,EAAE,CAAC,YAAY,CAAC,IAAI,EAAE,OAAO,CAAC,CAAC;IAEjD,mEAAmE;IACnE,IAAI,OAAO,CAAC,MAAM,KAAK,IAAI,EAAE,CAAC;QAC5B,OAAO,CAAC,GAAG,CAAC,mDAAmD,CAAC,CAAC;QACjE,uBAAuB,CAAC,GAAG,EAAE,OAAO,CAAC,SAAS,CAAC,CAAC;IAClD,CAAC;IAED,8CAA8C;IAC9C,IAAI,OAAO,CAAC,MAAM,KAAK,IAAI,IAAI,OAAO,CAAC,MAAM,KAAK,KAAK,EAAE,CAAC;QACxD,OAAO,CAAC,GAAG,CAAC,6BAA6B,CAAC,CAAC;QAC3C,kDAAkD;QAClD,KAAK,MAAM,KAAK,IAAI,GAAG,CAAC,MAAM,EAAE,CAAC;YAC/B,MAAM,UAAU,GAAG,yBAAyB,CAAC,SAAS,EAAE,KAAK,CAAC,IAAI,CAAC,CAAC;YACpE,MAAM,QAAQ,GAAG,mBAAmB,CAAC,SAAS,EAAE,KAAK,CAAC,IAAI,CAAC,CAAC;YAC5D,kDAAkD;YACjD,KAAa,CAAC,WAAW,GAAG,UAAU,CAAC;YACvC,KAAa,CAAC,KAAK,GAAG,QAAQ,CAAC;QAClC,CAAC;QACD,MAAM,SAAS,GAAc,EAAE,WAAW,EAAE,OAAO,CAAC,WAAW,EAAE,CAAC;QAClE,UAAU,CAAC,GAAG,EAAE,OAAO,CAAC,SAAS,EAAE,SAAS,CAAC,CAAC;IAChD,CAAC;IAED,mDAAmD;IACnD,IAAI,OAAO,CAAC,MAAM,KAAK,IAAI,EAAE,CAAC;QAC5B,OAAO,CAAC,GAAG,CAAC,0CAA0C,CAAC,CAAC;QACxD,8BAA8B,CAAC,GAAG,EAAE,OAAO,CAAC,SAAS,CAAC,CAAC;QAEvD,yCAAyC;QACzC,IAAI,OAAO,CAAC,SAAS,KAAK,KAAK,IAAI,OAAO,CAAC,SAAS,KAAK,MAAM,EAAE,CAAC;YAChE,OAAO,CAAC,GAAG,CAAC,+BAA+B,CAAC,CAAC;YAC7C,iBAAiB,CAAC,GAAG,EAAE,OAAO,CAAC,SAAS,CAAC,CAAC;QAC5C,CAAC;QAED,IAAI,OAAO,CAAC,SAAS,KAAK,MAAM,IAAI,OAAO,CAAC,SAAS,KAAK,MAAM,EAAE,CAAC;YACjE,OAAO,CAAC,GAAG,CAAC,0BAA0B,CAAC,CAAC;YACxC,YAAY,CAAC,GAAG,EAAE,OAAO,CAAC,SAAS,CAAC,CAAC;QACvC,CAAC;IACH,CAAC;IAED,OAAO,CAAC,GAAG,CAAC,mCAAmC,OAAO,CAAC,SAAS,GAAG,CAAC,CAAC;AACvE,CAAC;AAED,IAAI,EAAE,CAAC,KAAK,CAAC,CAAC,GAAG,EAAE,EAAE;IACnB,OAAO,CAAC,KAAK,CAAC,qBAAqB,EAAE,GAAG,CAAC,CAAC;IAC1C,OAAO,CAAC,IAAI,CAAC,CAAC,CAAC,CAAC;AAClB,CAAC,CAAC,CAAC"} \ No newline at end of file diff --git a/compiler/src/generators/typescript-state-machine.ts b/compiler/src/generators/typescript-state-machine.ts index 08d23a5..e857f5d 100644 --- a/compiler/src/generators/typescript-state-machine.ts +++ b/compiler/src/generators/typescript-state-machine.ts @@ -329,7 +329,7 @@ function rewriteExpr(expr: string, stateVarNames: Set, mapVarNames: Set< // Step 2: Replace state enum literals with enum refs BEFORE identifier replacement const allStateValues = new Set(knownStateValues); // Add common fallback states - ['Open','Grooming','Groomed','Assigned','InProgress','InReview','Merged','Blocked','Closed','Idle','Parsing','Parsed','ProvenanceGenerated','BOMsGenerated','TypeScriptGenerated','WASMGenerated','Done'].forEach(s => allStateValues.add(s)); + ['Open','Grooming','Groomed','Assigned','InProgress','InReview','Merged','Blocked','Closed','Idle','Parsing','Parsed','ProvenanceGenerated','BOMsGenerated','TypeScriptGenerated','Done'].forEach(s => allStateValues.add(s)); if (allStateValues.size > 0) { const stateValueRegex = new RegExp('\\b(' + Array.from(allStateValues).join('|') + ')\\b', 'g'); ts = ts.replace(stateValueRegex, `${stateEnumName}.$1`); @@ -441,7 +441,7 @@ function cleanName(s: string): string { function replaceStateWithEnum(expr: string, enumName: string, knownStateValues: string[]): string { const allStateValues = new Set(knownStateValues); - ['Open','Grooming','Groomed','Assigned','InProgress','InReview','Merged','Blocked','Closed','Idle','Parsing','Parsed','ProvenanceGenerated','BOMsGenerated','TypeScriptGenerated','WASMGenerated','Done'].forEach(s => allStateValues.add(s)); + ['Open','Grooming','Groomed','Assigned','InProgress','InReview','Merged','Blocked','Closed','Idle','Parsing','Parsed','ProvenanceGenerated','BOMsGenerated','TypeScriptGenerated','Done'].forEach(s => allStateValues.add(s)); if (allStateValues.size === 0) return expr; const stateValueRegex = new RegExp('\\b(' + Array.from(allStateValues).join('|') + ')\\b', 'g'); return expr.replace(stateValueRegex, `${enumName}.$1`); diff --git a/compiler/src/generators/wasm.ts b/compiler/src/generators/wasm.ts deleted file mode 100644 index 700ddc1..0000000 --- a/compiler/src/generators/wasm.ts +++ /dev/null @@ -1,472 +0,0 @@ -import { AST, SpeckNode, StateNode, InitNode, ActionNode, EventNode } from '../parser.js'; -import fs from 'fs'; -import path from 'path'; - -/** - * Generate WebAssembly Text (WAT) from a SpeckDL state machine spec. - * - * Emits a .wat file per speck with: - * - Linear memory for scalar state (Nat/Int/Real/Bool) - * - Imported host functions for Map and Set - * - Exported `init()` — calls host to init Maps/Sets + sets scalars - * - Exported action functions (one per action) - * - Exported `getState()` — serializes scalars into memory - * - Exported `checkConstraints()` — runtime guard stubs - * - * Compile to .wasm with: wat2wasm .wat -o .wasm - * - * Host runtime (JS): see `speckl/runtime/wasm-host.js` - */ - -// --------------------------------------------------------------------------- -// Host imports required by generated modules -// --------------------------------------------------------------------------- -const HOST_IMPORTS = [ - '(import "speckl" "map_create" (func $map_create (result i32)))', - '(import "speckl" "map_set" (func $map_set (param i32 i32 i32)))', - '(import "speckl" "map_get" (func $map_get (param i32 i32) (result i32)))', - '(import "speckl" "map_has" (func $map_has (param i32 i32) (result i32)))', - '(import "speckl" "map_remove" (func $map_remove (param i32 i32)))', - '(import "speckl" "set_create" (func $set_create (result i32)))', - '(import "speckl" "set_add" (func $set_add (param i32 i32)))', - '(import "speckl" "set_has" (func $set_has (param i32 i32) (result i32)))', - '(import "speckl" "set_size" (func $set_size (param i32) (result i32)))', - '(import "speckl" "alloc" (func $alloc (param i32) (result i32)))', - '(import "speckl" "write_i32" (func $write_i32 (param i32 i32)))', - '(import "speckl" "write_f64" (func $write_f64 (param i32 f64)))', -]; - -export function generateWASM(ast: AST, outputDir: string): void { - for (const speck of ast.specks) { - const hasStateMachine = speck.members.some(m => - m.type === 'state' || m.type === 'init' || m.type === 'action' - ); - if (!hasStateMachine) continue; - - const wat = emitSpeckWAT(speck); - const filename = `${speck.name}.wat`; - const filepath = path.join(outputDir, filename); - fs.writeFileSync(filepath, wat); - console.log(`Generated WAT: ${filepath}`); - } -} - -function emitSpeckWAT(speck: SpeckNode): string { - const stateNode = speck.members.find(m => m.type === 'state') as StateNode | undefined; - const initNode = speck.members.find(m => m.type === 'init') as InitNode | undefined; - const actions = speck.members.filter(m => m.type === 'action') as ActionNode[]; - const events = speck.members.filter(m => m.type === 'event') as EventNode[]; - - const stateVars = stateNode?.variables ?? []; - - // ------------------------------------------------------------------------- - // 1. Memory layout for scalar state variables - // ------------------------------------------------------------------------- - // Each scalar gets 8 bytes (i64/f64 slot). Map/Set handles are i32 refs - // stored in globals. - // - // Layout: [0..8) var0, [8..16) var1, ... then string pool for getState() - // - const scalarVars = stateVars.filter(v => isScalarType(v.typeExpr)); - const refVars = stateVars.filter(v => !isScalarType(v.typeExpr)); - - const memSize = Math.max(1, Math.ceil((scalarVars.length * 8 + 1024) / 65536)); - - // ------------------------------------------------------------------------- - // 2. Globals: one per state variable - // ------------------------------------------------------------------------- - const globals = stateVars.map((v, i) => { - if (isScalarType(v.typeExpr)) { - const wasmType = wasmTypeOf(v.typeExpr); - const initVal = initValueFor(v.name, v.typeExpr, v.defaultInit, initNode); - return `(global $${v.name} (mut ${wasmType}) (${wasmType}.const ${initVal}))`; - } else { - // Map or Set — store as i32 handle (0 = uninitialized) - return `(global $${v.name} (mut i32) (i32.const 0))`; - } - }).join('\n'); - - // ------------------------------------------------------------------------- - // 3. init() export - // ------------------------------------------------------------------------- - const initBody = emitInitBody(stateVars, initNode); - - // ------------------------------------------------------------------------- - // 4. Action exports - // ------------------------------------------------------------------------- - const actionFuncs = actions.map(a => emitActionWAT(a, stateVars)).join('\n\n'); - - // ------------------------------------------------------------------------- - // 5. getState() export — write scalars to memory, return ptr+len - // ------------------------------------------------------------------------- - const getStateBody = emitGetState(scalarVars); - - // ------------------------------------------------------------------------- - // 6. checkConstraints() stub - // ------------------------------------------------------------------------- - const checkConstraints = ` - ;; checkConstraints — runtime constraint evaluation stub - (func $checkConstraints (export "checkConstraints") (result i32) - ;; TODO: evaluate constraint expressions at runtime - (i32.const 1) - )`; - - // ------------------------------------------------------------------------- - // 7. Assemble module - // ------------------------------------------------------------------------- - const module = - `;; Auto-generated by speckl-compile from ${speck.name}\n` + - `;; Compile: wat2wasm ${speck.name}.wat -o ${speck.name}.wasm\n\n` + - `(module\n` + - ` ;; Host imports for Map/Set/alloc\n` + - ` ${HOST_IMPORTS.join('\n ')}\n\n` + - ` ;; Linear memory (exported so host can read state)\n` + - ` (memory (export "memory") ${memSize})\n\n` + - ` ;; State globals\n` + - ` ${globals}\n\n` + - ` ;; ---- init ----\n` + - ` (func $init (export "init")\n` + - ` ${initBody}\n` + - ` )\n\n` + - ` ;; ---- Actions ----\n` + - ` ${actionFuncs}\n\n` + - ` ;; ---- getState ----\n` + - ` (func $getState (export "getState") (result i32 i32)\n` + - ` ${getStateBody}\n` + - ` )\n\n` + - ` ${checkConstraints}\n` + - `)`; - - return module; -} - -// ============================================================================= -// init() body generation -// ============================================================================= -function emitInitBody( - stateVars: StateNode['variables'], - initNode: InitNode | undefined -): string { - const lines: string[] = []; - - for (const v of stateVars) { - if (isScalarType(v.typeExpr)) { - const val = initValueFor(v.name, v.typeExpr, v.defaultInit, initNode); - const wasmType = wasmTypeOf(v.typeExpr); - lines.push(`(${wasmType}.const ${val})`); - lines.push(`(global.set $${v.name})`); - } else if (isMapType(v.typeExpr)) { - lines.push(`(call $map_create)`); - lines.push(`(global.set $${v.name})`); - } else if (isSetType(v.typeExpr)) { - lines.push(`(call $set_create)`); - lines.push(`(global.set $${v.name})`); - } - } - - return lines.join('\n '); -} - -// ============================================================================= -// Action function generation -// ============================================================================= -function emitActionWAT(action: ActionNode, stateVars: StateNode['variables']): string { - const scalarStateNames = new Set( - stateVars.filter(v => isScalarType(v.typeExpr)).map(v => v.name) - ); - const mapStateNames = new Set( - stateVars.filter(v => isMapType(v.typeExpr)).map(v => v.name) - ); - const setStateNames = new Set( - stateVars.filter(v => isSetType(v.typeExpr)).map(v => v.name) - ); - - // Params: SpeckDL Nat/Int → i32, Real → f64, Bool → i32 - const params = action.params.map(p => { - const t = wasmTypeOf(p.type); - return `(param $${p.name} ${t})`; - }).join(' '); - - const localLines: string[] = []; - const bodyLines: string[] = []; - - for (const stmt of action.statements) { - switch (stmt.type) { - case 'require': { - // Emit guard: if !condition → return 0 (failure indicator) - // For now, require guards that reference only scalar state variables - // and simple comparisons are emitted. Complex ones trap/return 0. - const guard = emitGuardExpr(stmt.expr, scalarStateNames, mapStateNames, setStateNames); - bodyLines.push(`;; require: ${stmt.expr}`); - bodyLines.push(guard); - break; - } - case 'assign': { - bodyLines.push(`;; ${stmt.target} := ${stmt.expr}`); - bodyLines.push(emitAssignment(stmt.target, stmt.expr, scalarStateNames, mapStateNames)); - break; - } - case 'let': { - // let name := expr — allocate local, compute expr, store - const wasmT = inferExprType(stmt.expr, scalarStateNames); - localLines.push(`(local $${stmt.name} ${wasmT})`); - bodyLines.push(emitExpr(stmt.expr, scalarStateNames)); - bodyLines.push(`(local.set $${stmt.name})`); - break; - } - case 'emit': { - // emit → decision log push (host call stub for now) - bodyLines.push(`;; emit ${stmt.event} { ... }`); - // TODO: structured emit via host - break; - } - case 'return': { - bodyLines.push(emitExpr(stmt.expr, scalarStateNames)); - bodyLines.push(`(return)`); - break; - } - } - } - - // Default return: i32.const 1 for success if action returns void - const hasReturn = action.statements.some(s => s.type === 'return'); - if (!hasReturn) { - bodyLines.push(`(i32.const 1)`); - } - - const locals = localLines.length ? `\n ${localLines.join('\n ')}` : ''; - - return ` ;; action: ${action.name}\n` + - ` (func $${action.name} (export "${action.name}") ${params} (result i32)\n` + - ` ${locals}\n` + - ` ${bodyLines.join('\n ')}\n` + - ` )`; -} - -// ============================================================================= -// Expression / guard emission (simplified — covers common scalar patterns) -// ============================================================================= -function emitGuardExpr( - expr: string, - scalars: Set, - maps: Set, - sets: Set -): string { - // Very simple pattern: "x >= 0", "x == true", "x != y", etc. - const m = expr.match(/^\s*(\w+)\s*(>=|<=|>|<|==|!=)\s*(.+?)\s*$/); - if (!m) { - // Can't compile guard — just comment, no stack effect - return `;; Complex guard not compiled: ${expr}`; - } - - const [, left, op, rightRaw] = m; - const right = rightRaw.trim(); - - if (!scalars.has(left)) { - return `;; Guard on non-scalar not compiled: ${expr}`; - } - - const lhs = `(global.get $${left})`; - - // Parse right side - let rhs: string; - const rightNum = parseFloat(right); - if (!isNaN(rightNum)) { - rhs = `(i32.const ${rightNum})`; - } else if (right === 'true') { - rhs = `(i32.const 1)`; - } else if (right === 'false') { - rhs = `(i32.const 0)`; - } else if (scalars.has(right)) { - rhs = `(global.get $${right})`; - } else { - return `;; Complex right-hand side not compiled: ${expr}`; - } - - const comparison = (() => { - switch (op) { - case '>=': return `(i32.ge_s ${lhs} ${rhs})`; - case '<=': return `(i32.le_s ${lhs} ${rhs})`; - case '>': return `(i32.gt_s ${lhs} ${rhs})`; - case '<': return `(i32.lt_s ${lhs} ${rhs})`; - case '==': return `(i32.eq ${lhs} ${rhs})`; - case '!=': return `(i32.ne ${lhs} ${rhs})`; - default: return `(i32.const 1)`; - } - })(); - - // If guard fails (comparison is FALSE), return 0 - return `${comparison}\n (i32.eqz)\n (if (then (return (i32.const 0))))`; -} - -function emitExpr(expr: string, scalars: Set): string { - // Handle: nextId + 1, nextId, numeric literals, etc. - expr = expr.trim(); - - // Simple numeric literal - const num = parseFloat(expr); - if (!isNaN(num) && !expr.match(/\w/)) { - return `(i32.const ${num})`; - } - - // Simple variable reference - if (/^\w+$/.test(expr) && scalars.has(expr)) { - return `(global.get $${expr})`; - } - - // Binary op: left + right, left - right, left * right - const binOp = expr.match(/^(\w+)\s*([+\-*/])\s*(.+)$/); - if (binOp) { - const [, left, op, right] = binOp; - const lhs = scalars.has(left) ? `(global.get $${left})` : `(i32.const ${parseFloat(left)})`; - const rhsNum = parseFloat(right.trim()); - const rhs = isNaN(rhsNum) - ? (scalars.has(right.trim()) ? `(global.get $${right.trim()})` : `(i32.const 0) ;; uncompiled`) - : `(i32.const ${rhsNum})`; - switch (op) { - case '+': return `(i32.add ${lhs} ${rhs})`; - case '-': return `(i32.sub ${lhs} ${rhs})`; - case '*': return `(i32.mul ${lhs} ${rhs})`; - default: return `(i32.const 0) ;; uncompiled op ${op}`; - } - } - - return `(i32.const 0) ;; uncompiled expr: ${expr}`; -} - -function inferExprType(expr: string, scalars: Set): string { - // Default to i32; we could infer from variable types but that's future work - return 'i32'; -} - -function emitAssignment( - target: string, - expr: string, - scalars: Set, - maps: Set -): string { - // Scalar assignment: this.x = expr - if (scalars.has(target)) { - return `${emitExpr(expr, scalars)}\n (global.set $${target})`; - } - - // Map assignment: accounts[id] := expr — host call - const mapAssign = target.match(/^(\w+)\[(.+)\]$/); - if (mapAssign && maps.has(mapAssign[1])) { - const mapName = mapAssign[1]; - const keyExpr = mapAssign[2]; - // For now: map_set(map_handle, key_handle, value_handle) - // This needs boxing; simplified version just marks as stub - return `;; Map assignment not yet compiled: ${target} := ${expr}`; - } - - // Record field assignment: accounts[id].field := expr - const recordAssign = target.match(/^(\w+)\[(.+)\]\.(\w+)$/); - if (recordAssign && maps.has(recordAssign[1])) { - return `;; Record field assignment not yet compiled: ${target} := ${expr}`; - } - - return `;; Unrecognized assignment target: ${target}`; -} - -// ============================================================================= -// getState() — serialize scalar state to memory -// ============================================================================= -function emitGetState(scalarVars: StateNode['variables']): string { - const lines: string[] = []; - let offset = 0; - - for (const v of scalarVars) { - const t = wasmTypeOf(v.typeExpr); - if (t === 'i32') { - lines.push(`(i32.const ${offset})`); - lines.push(`(global.get $${v.name})`); - lines.push(`(i32.store)`); - offset += 4; - } else if (t === 'f64') { - lines.push(`(i32.const ${offset})`); - lines.push(`(global.get $${v.name})`); - lines.push(`(f64.store)`); - offset += 8; - } else { - // i64 - lines.push(`(i32.const ${offset})`); - lines.push(`(global.get $${v.name})`); - lines.push(`(i64.store)`); - offset += 8; - } - } - - // Return (ptr, len) - lines.push(`(i32.const 0)`); // ptr = 0 - lines.push(`(i32.const ${offset})`); // len = total bytes written - - return lines.join('\n '); -} - -// ============================================================================= -// Type helpers -// ============================================================================= -function isScalarType(t: any): boolean { - if (t.type === 'primitive') { - return ['Nat', 'Int', 'Real', 'Bool'].includes(t.name); - } - if (t.type === 'ident') return true; // opaque ident → i32 handle - return false; -} - -function isMapType(t: any): boolean { - return t.type === 'map'; -} - -function isSetType(t: any): boolean { - return t.type === 'set'; -} - -function wasmTypeOf(t: any): string { - if (t.type === 'primitive') { - if (t.name === 'Nat') return 'i32'; - if (t.name === 'Int') return 'i32'; - if (t.name === 'Real') return 'f64'; - if (t.name === 'Bool') return 'i32'; - if (t.name === 'String') return 'i32'; // ptr - if (t.name === 'Bytes') return 'i32'; // ptr - return 'i32'; - } - if (t.type === 'ident') return 'i32'; - if (t.type === 'map') return 'i32'; // handle - if (t.type === 'set') return 'i32'; // handle - return 'i32'; -} - -function initValueFor( - varName: string, - typeExpr: any, - defaultInit: string | undefined, - initNode: InitNode | undefined -): string { - // Use initNode assignment if present - const initAssign = initNode?.assignments.find(a => a.name === varName); - if (initAssign) { - const expr = initAssign.expr.trim(); - if (expr === 'true') return '1'; - if (expr === 'false') return '0'; - if (expr === 'Map.empty()') return '0'; // will be replaced by host call - if (expr === 'Set.empty()') return '0'; - const num = parseFloat(expr); - if (!isNaN(num)) return String(num); - return '0'; - } - - // Fallback to defaultInit - if (defaultInit) { - if (defaultInit === 'true') return '1'; - if (defaultInit === 'false') return '0'; - const num = parseFloat(defaultInit); - if (!isNaN(num)) return String(num); - } - - // Default zero - if (typeExpr.type === 'primitive' && typeExpr.name === 'Real') return '0.0'; - return '0'; -} diff --git a/compiler/src/generators/z3.ts b/compiler/src/generators/z3.ts index 19bde51..c8992f8 100644 --- a/compiler/src/generators/z3.ts +++ b/compiler/src/generators/z3.ts @@ -392,6 +392,22 @@ function translateExpr(expr: string, stateVars: StateVar[], suffix: string): str // Handle old() wrapper — spec-level, keep inner e = e.replace(/old\(([^()]*(?:\([^()]*\)[^()]*)*)\)/g, '$1'); + // Handle implies(x, y) function call pattern + e = e.replace(/implies\s*\(([^,)]+),\s*([^)]+)\)/g, '(=> $1 $2)'); + + // Field access: a.balance → balance (drop qualifier for bound forall vars) + // For record fields accessed via dot, translate to Z3-safe names + e = e.replace(/(\w+)\.([\w_]+)/g, (_, obj, field) => { + // If the object is a state variable (map), .field is an accessor we can't resolve + // For bound forall variables, just use the field name + if (stateVarNames.has(obj)) { + // Accessing field on opaque sort — use a compound name + return `${obj}_${field}`; + } + // For bound variables in forall, just emit the field + return `${obj}_${field}`; + }); + // Handle notIn BEFORE general patterns e = e.replace(/(\S+)\s+notIn\s+(\S+)\.keys/g, '(not (select $2 $1))'); @@ -449,6 +465,10 @@ function translateExpr(expr: string, stateVars: StateVar[], suffix: string): str e = e.replace(/>=/g, '__GE__'); e = e.replace(/<=/g, '__LE__'); + // Replace && and || with and/or for SMT-LIB2 + e = e.replace(/&&/g, 'and'); + e = e.replace(/\|\|/g, 'or'); + // Convert infix to prefix e = convertToPrefix(e); @@ -940,11 +960,36 @@ function parseInvariantBody(content: string): InvariantStatement[] { const statements: InvariantStatement[] = []; const lines = content.split('\n'); - for (const rawLine of lines) { + let i = 0; + while (i < lines.length) { + const rawLine = lines[i]; const line = rawLine.trim(); - if (!line || line.startsWith('//')) continue; + if (!line || line.startsWith('//')) { i++; continue; } - // forall var in domain: expr + // forall var in domain: (body on next line(s)) + const forallHeaderMatch = line.match(/^forall\s+(\w+)\s+in\s+([.\w]+):\s*$/); + if (forallHeaderMatch) { + const bodyLines: string[] = []; + i++; + while (i < lines.length) { + const nextLine = lines[i]; + if (!nextLine.trim() || nextLine.trim().startsWith('//')) { i++; continue; } + if (/^forall\s+/.test(nextLine.trim()) || !/^\s+/.test(nextLine)) break; + bodyLines.push(nextLine.trim()); + i++; + } + if (bodyLines.length > 0) { + statements.push({ + type: 'forall', + var: forallHeaderMatch[1], + domain: forallHeaderMatch[2], + expr: bodyLines.join(' '), + }); + } + continue; + } + + // forall var in domain: expr (single line) const forallMatch = line.match(/^forall\s+(\w+)\s+in\s+([.\w]+):\s*(.+)$/); if (forallMatch) { statements.push({ @@ -953,28 +998,32 @@ function parseInvariantBody(content: string): InvariantStatement[] { domain: forallMatch[2], expr: forallMatch[3].trim(), }); - continue; + i++; continue; } // forall var1, var2 in domain1, domain2: expr (complex) const complexForallMatch = line.match(/^forall\s+([\w,\s]+)\s+in\s+([\w\s.,]+):\s*(.+)$/); if (complexForallMatch) { - const vars = complexForallMatch[1].split(',').map(s => s.trim()).filter(Boolean); - const domains = complexForallMatch[2].split(',').map(s => s.trim()).filter(Boolean); + const vars = complexForallMatch[1].split(',').map((s: string) => s.trim()).filter(Boolean); + const domains = complexForallMatch[2].split(',').map((s: string) => s.trim()).filter(Boolean); if (vars.length > 1 || domains.length > 1) { statements.push({ type: 'forall_complex', - vars, - domains, + vars, domains, expr: complexForallMatch[3].trim(), }); - continue; + i++; continue; } - // Fall through to simple forall + statements.push({ + type: 'forall', + var: vars[0], domain: domains[0], + expr: complexForallMatch[3].trim(), + }); + i++; continue; } - // Simple require-style expression statements.push({ type: 'require', expr: line }); + i++; } return statements; diff --git a/compiler/src/index.ts b/compiler/src/index.ts index e61be9c..ad93801 100644 --- a/compiler/src/index.ts +++ b/compiler/src/index.ts @@ -7,7 +7,6 @@ import { generateProvenanceGraph } from './generators/provenance.js'; import { generateCycloneDX } from './generators/cyclonedx.js'; import { generateSPDX } from './generators/spdx.js'; import { generateTypeScriptStateMachine } from './generators/typescript-state-machine.js'; -import { generateWASM } from './generators/wasm.js'; import { generateZ3, Z3Options, parseInvariantsFromSource, parseNextFromSource } from './generators/z3.js'; import fs from 'fs'; import path from 'path'; @@ -121,10 +120,6 @@ async function main() { console.log('\nGenerating TypeScript state machine...'); generateTypeScriptStateMachine(ast, options.outputDir); - // Generate WASM state machine - console.log('\nGenerating WebAssembly (WAT)...'); - generateWASM(ast, options.outputDir); - // Generate BOM based on format selection if (options.bomFormat === 'cdx' || options.bomFormat === 'both') { console.log('\nGenerating CycloneDX BOM...'); diff --git a/compiler/src/runtime/wasm-host.ts b/compiler/src/runtime/wasm-host.ts deleted file mode 100644 index 513892b..0000000 --- a/compiler/src/runtime/wasm-host.ts +++ /dev/null @@ -1,165 +0,0 @@ -/** - * Speckl WASM Host Runtime - * - * Provides JS-side implementations for imported host functions used by - * Speckl-generated WASM modules: - * - map_create, map_set, map_get, map_has, map_remove - * - set_create, set_add, set_has, set_size - * - alloc, write_i32, write_f64 - * - * Usage: - * const wasmModule = await WebAssembly.instantiate(bytes, { - * speckl: createHostImports() - * }); - * wasmModule.exports.init(); - * wasmModule.exports.CreateAccount(100.0); - * const state = getStateFromMemory(wasmModule); - */ - -interface HostState { - maps: Map>; - sets: Map>; - nextHandle: number; - memory: WebAssembly.Memory | null; -} - -function createHostState(): HostState { - return { - maps: new Map(), - sets: new Map(), - nextHandle: 1, - memory: null, - }; -} - -export function createHostImports(state: HostState = createHostState()) { - return { - // ---- Map operations ---- - map_create: (): number => { - const handle = state.nextHandle++; - state.maps.set(handle, new Map()); - return handle; - }, - - map_set: (mapHandle: number, keyHandle: number, valueHandle: number): void => { - const map = state.maps.get(mapHandle); - if (!map) throw new Error(`Map handle ${mapHandle} not found`); - // For now, keys and values are simple i32 handles; boxing layer comes later - map.set(keyHandle, valueHandle); - }, - - map_get: (mapHandle: number, keyHandle: number): number => { - const map = state.maps.get(mapHandle); - if (!map) return 0; - return map.has(keyHandle) ? (map.get(keyHandle) ?? 0) : 0; - }, - - map_has: (mapHandle: number, keyHandle: number): number => { - const map = state.maps.get(mapHandle); - if (!map) return 0; - return map.has(keyHandle) ? 1 : 0; - }, - - map_remove: (mapHandle: number, keyHandle: number): void => { - const map = state.maps.get(mapHandle); - if (map) map.delete(keyHandle); - }, - - // ---- Set operations ---- - set_create: (): number => { - const handle = state.nextHandle++; - state.sets.set(handle, new Set()); - return handle; - }, - - set_add: (setHandle: number, valueHandle: number): void => { - const set = state.sets.get(setHandle); - if (!set) throw new Error(`Set handle ${setHandle} not found`); - set.add(valueHandle); - }, - - set_has: (setHandle: number, valueHandle: number): number => { - const set = state.sets.get(setHandle); - if (!set) return 0; - return set.has(valueHandle) ? 1 : 0; - }, - - set_size: (setHandle: number): number => { - const set = state.sets.get(setHandle); - if (!set) return 0; - return set.size; - }, - - // ---- Memory helpers ---- - alloc: (size: number): number => { - // Simple bump allocator: for now, just return 0 (stack allocation handled by compiler) - // Future: maintain bump pointer in memory - return 0; - }, - - write_i32: (ptr: number, value: number): void => { - if (!state.memory) throw new Error('Memory not bound'); - const view = new DataView(state.memory.buffer); - view.setInt32(ptr, value, true); // little-endian - }, - - write_f64: (ptr: number, value: number): void => { - if (!state.memory) throw new Error('Memory not bound'); - const view = new DataView(state.memory.buffer); - view.setFloat64(ptr, value, true); - }, - }; -} - -/** - * Bind a WASM memory export to the host state so write_i32/write_f64 work. - */ -export function bindMemory(state: HostState, memory: WebAssembly.Memory): void { - state.memory = memory; -} - -/** - * Read scalar state from WASM memory after getState() has been called. - * Layout matches emitGetState(): [nextId: i32][ledgerOpen: i32]... - */ -export function readScalarState(memory: WebAssembly.Memory, varNames: string[]): Record { - const view = new DataView(memory.buffer); - const result: Record = {}; - let offset = 0; - - for (const name of varNames) { - // All current scalars are i32 in TigerBeetle; extend for f64 later - result[name] = view.getInt32(offset, true); - offset += 4; - } - - return result; -} - -/** - * High-level helper: instantiate a Speckl WASM module from WAT text. - * Requires `wat2wasm` or a WAT parser. For now, expects pre-compiled .wasm bytes. - */ -export async function instantiateSpeckl( - wasmBytes: BufferSource, - varNames: string[] -): Promise<{ - exports: WebAssembly.Exports; - state: HostState; - getScalarState: () => Record; -}> { - const hostState = createHostState(); - const imports = { speckl: createHostImports(hostState) }; - - const wasm = await WebAssembly.instantiate(wasmBytes, imports); - const memory = wasm.instance.exports.memory as WebAssembly.Memory; - bindMemory(hostState, memory); - - const getScalarState = () => readScalarState(memory, varNames); - - return { - exports: wasm.instance.exports, - state: hostState, - getScalarState, - }; -} diff --git a/reference-agent/src/smes/verification-sme.ts b/reference-agent/src/smes/verification-sme.ts index f096a25..9cd6b72 100644 --- a/reference-agent/src/smes/verification-sme.ts +++ b/reference-agent/src/smes/verification-sme.ts @@ -30,7 +30,7 @@ export class VerificationSME extends SME { this.compileConstraint(c.expression, speck) ); - // In production, this would invoke Z3 via subprocess or WASM. + // In production, this would invoke Z3 via subprocess. // For the reference implementation, we simulate the result. const z3Result = this.simulateZ3(speck, z3Assertions); diff --git a/reference-agent/src/types.ts b/reference-agent/src/types.ts index 7c09802..5b6f524 100644 --- a/reference-agent/src/types.ts +++ b/reference-agent/src/types.ts @@ -99,7 +99,7 @@ export interface Task { export type TaskType = | "verify_speck" // Run Z3 verification on a Speck | "compile_to_dst" // Compile verified Speck to DST - | "compile_to_wasm" // Compile DST to WASM + | "compile_to_typescript" // Compile DST to TypeScript | "generate_code" // Generate code from verified Speck | "generate_docs" // Generate documentation from provenance graph | "integrate" // Integration/glue code @@ -142,7 +142,7 @@ export interface TaskResult { export interface ProvenanceNode { id: string; - type: "speck" | "z3_assertion" | "dst" | "wasm" | "code" | "docs" | "event"; + type: "speck" | "z3_assertion" | "dst" | "code" | "docs" | "event"; label: string; metadata: Record; }