Merge branch 'feature/z3-backend' (Z3 backend + KRaft spec)
This commit is contained in:
Scott Scoble
parent
6c6daaf90f
commit
c5ca757e80
12 changed files with 81 additions and 956 deletions
32
README.md
32
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).
|
**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
|
## 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:
|
Speckl is a **working compiler** that turns formal specifications into multiple target representations:
|
||||||
|
|
||||||
```
|
```
|
||||||
.speckdl spec ──→ Wasm (WebAssembly) ← runnable, verified state machines
|
.speckdl spec ──→ TypeScript ← typed, importable classes
|
||||||
├── TypeScript ← typed, importable classes
|
|
||||||
├── PROV-O (RDF) ← W3C provenance standard
|
├── PROV-O (RDF) ← W3C provenance standard
|
||||||
├── CycloneDX SBOM ← OWASP software bill of materials
|
├── CycloneDX SBOM ← OWASP software bill of materials
|
||||||
└── SPDX SBOM ← Linux Foundation SBOM standard
|
└── 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
|
### Provenance Embedded at Compile Time
|
||||||
|
|
||||||
|
|
@ -58,12 +57,12 @@ The compiler has been validated against:
|
||||||
|
|
||||||
| Example | Source | Status |
|
| Example | Source | Status |
|
||||||
|---------|--------|--------|
|
|---------|--------|--------|
|
||||||
| **ToggleSwitch** | SpeckDL tutorial | ✅ All 5 artifacts |
|
| **ToggleSwitch** | SpeckDL tutorial | ✅ All artifacts |
|
||||||
| **AccountLedger** | Banking ledger with debit/credit | ✅ All 5 artifacts |
|
| **AccountLedger** | Banking ledger with debit/credit | ✅ All artifacts |
|
||||||
| **TwoPhaseCommit** | TLA+ port | ✅ All 5 artifacts |
|
| **TwoPhaseCommit** | TLA+ port | ✅ All artifacts |
|
||||||
| **Paxos** | TLA+ port | ✅ All 5 artifacts |
|
| **Paxos** | TLA+ port | ✅ All artifacts |
|
||||||
| **Raft** | TLA+ port | ✅ All 5 artifacts |
|
| **Raft** | TLA+ port | ✅ All artifacts |
|
||||||
| **TigerBeetleLedger** | Naive TigerBeetle core | ✅ All 5 artifacts (3 TS type errors in progress) |
|
| **TigerBeetleLedger** | Naive TigerBeetle core | ✅ All artifacts (3 TS type errors in progress) |
|
||||||
|
|
||||||
## Getting Started
|
## Getting Started
|
||||||
|
|
||||||
|
|
@ -72,10 +71,10 @@ git clone https://os.scoble.me/forgejo/sscoble/speckl
|
||||||
cd speckl/compiler
|
cd speckl/compiler
|
||||||
npm install
|
npm install
|
||||||
|
|
||||||
# Compile an example to all 5 targets
|
# Compile an example
|
||||||
node dist/index.js ../examples/ToggleSwitch.speck -o out/switch
|
node dist/index.js ../examples/ToggleSwitch.speck -o out/switch
|
||||||
ls 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
|
# ToggleSwitch.cyclonedx.json ToggleSwitch.spdx.json
|
||||||
```
|
```
|
||||||
|
|
||||||
|
|
@ -99,11 +98,10 @@ ls out/switch/
|
||||||
|
|
||||||
## Validation Status
|
## Validation Status
|
||||||
|
|
||||||
- **Compiler:** 41/41 tests passing (WASM + TypeScript codegen)
|
- **Compiler:** 41/41 tests passing (TypeScript codegen)
|
||||||
- **WASM E2E:** wabt assemble + instantiate + run verified
|
- **TypeScript:** Type-safe compilation from specs
|
||||||
- **TypeScript:** Dual-target compilation — same spec produces both WASM and TS
|
- **TLA+ Trilogy:** TwoPhaseCommit, Paxos, Raft all compile
|
||||||
- **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 artifacts (known TypeScript errors tracked in engineering#9)
|
||||||
- **Compiler Self-Spec:** `speckl-compile.speckdl` defines the Speckl compiler in SpeckDL — generates all 5 artifacts (known TypeScript errors tracked in engineering#9)
|
|
||||||
|
|
||||||
## Known Issues
|
## Known Issues
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -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);
|
|
||||||
});
|
|
||||||
|
|
@ -1,6 +1,5 @@
|
||||||
import { describe, it, expect } from 'vitest';
|
import { describe, it, expect } from 'vitest';
|
||||||
import { parseSpeckContent, parseSpeckFile } from '../src/parser.js';
|
import { parseSpeckContent, parseSpeckFile } from '../src/parser.js';
|
||||||
import { generateWASM } from '../src/generators/wasm.js';
|
|
||||||
|
|
||||||
describe('SpeckDL Parser', () => {
|
describe('SpeckDL Parser', () => {
|
||||||
describe('parseSpeckContent', () => {
|
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 });
|
|
||||||
});
|
|
||||||
});
|
|
||||||
});
|
});
|
||||||
|
|
|
||||||
4
compiler/dist/index.js
vendored
4
compiler/dist/index.js
vendored
|
|
@ -6,7 +6,6 @@ import { generateProvenanceGraph } from './generators/provenance.js';
|
||||||
import { generateCycloneDX } from './generators/cyclonedx.js';
|
import { generateCycloneDX } from './generators/cyclonedx.js';
|
||||||
import { generateSPDX } from './generators/spdx.js';
|
import { generateSPDX } from './generators/spdx.js';
|
||||||
import { generateTypeScriptStateMachine } from './generators/typescript-state-machine.js';
|
import { generateTypeScriptStateMachine } from './generators/typescript-state-machine.js';
|
||||||
import { generateWASM } from './generators/wasm.js';
|
|
||||||
import { generateZ3, parseInvariantsFromSource, parseNextFromSource } from './generators/z3.js';
|
import { generateZ3, parseInvariantsFromSource, parseNextFromSource } from './generators/z3.js';
|
||||||
import fs from 'fs';
|
import fs from 'fs';
|
||||||
import path from 'path';
|
import path from 'path';
|
||||||
|
|
@ -102,9 +101,6 @@ async function main() {
|
||||||
if (options.target !== 'z3') {
|
if (options.target !== 'z3') {
|
||||||
console.log('\nGenerating TypeScript state machine...');
|
console.log('\nGenerating TypeScript state machine...');
|
||||||
generateTypeScriptStateMachine(ast, options.outputDir);
|
generateTypeScriptStateMachine(ast, options.outputDir);
|
||||||
// Generate WASM state machine
|
|
||||||
console.log('\nGenerating WebAssembly (WAT)...');
|
|
||||||
generateWASM(ast, options.outputDir);
|
|
||||||
// Generate BOM based on format selection
|
// Generate BOM based on format selection
|
||||||
if (options.bomFormat === 'cdx' || options.bomFormat === 'both') {
|
if (options.bomFormat === 'cdx' || options.bomFormat === 'both') {
|
||||||
console.log('\nGenerating CycloneDX BOM...');
|
console.log('\nGenerating CycloneDX BOM...');
|
||||||
|
|
|
||||||
2
compiler/dist/index.js.map
vendored
2
compiler/dist/index.js.map
vendored
|
|
@ -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"}
|
{"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"}
|
||||||
|
|
@ -329,7 +329,7 @@ function rewriteExpr(expr: string, stateVarNames: Set<string>, mapVarNames: Set<
|
||||||
// Step 2: Replace state enum literals with enum refs BEFORE identifier replacement
|
// Step 2: Replace state enum literals with enum refs BEFORE identifier replacement
|
||||||
const allStateValues = new Set<string>(knownStateValues);
|
const allStateValues = new Set<string>(knownStateValues);
|
||||||
// Add common fallback states
|
// 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) {
|
if (allStateValues.size > 0) {
|
||||||
const stateValueRegex = new RegExp('\\b(' + Array.from(allStateValues).join('|') + ')\\b', 'g');
|
const stateValueRegex = new RegExp('\\b(' + Array.from(allStateValues).join('|') + ')\\b', 'g');
|
||||||
ts = ts.replace(stateValueRegex, `${stateEnumName}.$1`);
|
ts = ts.replace(stateValueRegex, `${stateEnumName}.$1`);
|
||||||
|
|
@ -441,7 +441,7 @@ function cleanName(s: string): string {
|
||||||
|
|
||||||
function replaceStateWithEnum(expr: string, enumName: string, knownStateValues: string[]): string {
|
function replaceStateWithEnum(expr: string, enumName: string, knownStateValues: string[]): string {
|
||||||
const allStateValues = new Set<string>(knownStateValues);
|
const allStateValues = new Set<string>(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;
|
if (allStateValues.size === 0) return expr;
|
||||||
const stateValueRegex = new RegExp('\\b(' + Array.from(allStateValues).join('|') + ')\\b', 'g');
|
const stateValueRegex = new RegExp('\\b(' + Array.from(allStateValues).join('|') + ')\\b', 'g');
|
||||||
return expr.replace(stateValueRegex, `${enumName}.$1`);
|
return expr.replace(stateValueRegex, `${enumName}.$1`);
|
||||||
|
|
|
||||||
|
|
@ -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<K,V> and Set<T>
|
|
||||||
* - 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 <file>.wat -o <file>.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<string>,
|
|
||||||
maps: Set<string>,
|
|
||||||
sets: Set<string>
|
|
||||||
): 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>): 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>): 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<string>,
|
|
||||||
maps: Set<string>
|
|
||||||
): 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';
|
|
||||||
}
|
|
||||||
|
|
@ -392,6 +392,22 @@ function translateExpr(expr: string, stateVars: StateVar[], suffix: string): str
|
||||||
// Handle old() wrapper — spec-level, keep inner
|
// Handle old() wrapper — spec-level, keep inner
|
||||||
e = e.replace(/old\(([^()]*(?:\([^()]*\)[^()]*)*)\)/g, '$1');
|
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
|
// Handle notIn BEFORE general patterns
|
||||||
e = e.replace(/(\S+)\s+notIn\s+(\S+)\.keys/g, '(not (select $2 $1))');
|
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, '__GE__');
|
||||||
e = e.replace(/<=/g, '__LE__');
|
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
|
// Convert infix to prefix
|
||||||
e = convertToPrefix(e);
|
e = convertToPrefix(e);
|
||||||
|
|
||||||
|
|
@ -940,11 +960,36 @@ function parseInvariantBody(content: string): InvariantStatement[] {
|
||||||
const statements: InvariantStatement[] = [];
|
const statements: InvariantStatement[] = [];
|
||||||
const lines = content.split('\n');
|
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();
|
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*(.+)$/);
|
const forallMatch = line.match(/^forall\s+(\w+)\s+in\s+([.\w]+):\s*(.+)$/);
|
||||||
if (forallMatch) {
|
if (forallMatch) {
|
||||||
statements.push({
|
statements.push({
|
||||||
|
|
@ -953,28 +998,32 @@ function parseInvariantBody(content: string): InvariantStatement[] {
|
||||||
domain: forallMatch[2],
|
domain: forallMatch[2],
|
||||||
expr: forallMatch[3].trim(),
|
expr: forallMatch[3].trim(),
|
||||||
});
|
});
|
||||||
continue;
|
i++; continue;
|
||||||
}
|
}
|
||||||
|
|
||||||
// forall var1, var2 in domain1, domain2: expr (complex)
|
// forall var1, var2 in domain1, domain2: expr (complex)
|
||||||
const complexForallMatch = line.match(/^forall\s+([\w,\s]+)\s+in\s+([\w\s.,]+):\s*(.+)$/);
|
const complexForallMatch = line.match(/^forall\s+([\w,\s]+)\s+in\s+([\w\s.,]+):\s*(.+)$/);
|
||||||
if (complexForallMatch) {
|
if (complexForallMatch) {
|
||||||
const vars = complexForallMatch[1].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 => s.trim()).filter(Boolean);
|
const domains = complexForallMatch[2].split(',').map((s: string) => s.trim()).filter(Boolean);
|
||||||
if (vars.length > 1 || domains.length > 1) {
|
if (vars.length > 1 || domains.length > 1) {
|
||||||
statements.push({
|
statements.push({
|
||||||
type: 'forall_complex',
|
type: 'forall_complex',
|
||||||
vars,
|
vars, domains,
|
||||||
domains,
|
|
||||||
expr: complexForallMatch[3].trim(),
|
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 });
|
statements.push({ type: 'require', expr: line });
|
||||||
|
i++;
|
||||||
}
|
}
|
||||||
|
|
||||||
return statements;
|
return statements;
|
||||||
|
|
|
||||||
|
|
@ -7,7 +7,6 @@ import { generateProvenanceGraph } from './generators/provenance.js';
|
||||||
import { generateCycloneDX } from './generators/cyclonedx.js';
|
import { generateCycloneDX } from './generators/cyclonedx.js';
|
||||||
import { generateSPDX } from './generators/spdx.js';
|
import { generateSPDX } from './generators/spdx.js';
|
||||||
import { generateTypeScriptStateMachine } from './generators/typescript-state-machine.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 { generateZ3, Z3Options, parseInvariantsFromSource, parseNextFromSource } from './generators/z3.js';
|
||||||
import fs from 'fs';
|
import fs from 'fs';
|
||||||
import path from 'path';
|
import path from 'path';
|
||||||
|
|
@ -121,10 +120,6 @@ async function main() {
|
||||||
console.log('\nGenerating TypeScript state machine...');
|
console.log('\nGenerating TypeScript state machine...');
|
||||||
generateTypeScriptStateMachine(ast, options.outputDir);
|
generateTypeScriptStateMachine(ast, options.outputDir);
|
||||||
|
|
||||||
// Generate WASM state machine
|
|
||||||
console.log('\nGenerating WebAssembly (WAT)...');
|
|
||||||
generateWASM(ast, options.outputDir);
|
|
||||||
|
|
||||||
// Generate BOM based on format selection
|
// Generate BOM based on format selection
|
||||||
if (options.bomFormat === 'cdx' || options.bomFormat === 'both') {
|
if (options.bomFormat === 'cdx' || options.bomFormat === 'both') {
|
||||||
console.log('\nGenerating CycloneDX BOM...');
|
console.log('\nGenerating CycloneDX BOM...');
|
||||||
|
|
|
||||||
|
|
@ -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<number, Map<number, any>>;
|
|
||||||
sets: Map<number, Set<any>>;
|
|
||||||
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<string, number> {
|
|
||||||
const view = new DataView(memory.buffer);
|
|
||||||
const result: Record<string, number> = {};
|
|
||||||
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<string, number>;
|
|
||||||
}> {
|
|
||||||
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,
|
|
||||||
};
|
|
||||||
}
|
|
||||||
|
|
@ -30,7 +30,7 @@ export class VerificationSME extends SME {
|
||||||
this.compileConstraint(c.expression, speck)
|
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.
|
// For the reference implementation, we simulate the result.
|
||||||
const z3Result = this.simulateZ3(speck, z3Assertions);
|
const z3Result = this.simulateZ3(speck, z3Assertions);
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -99,7 +99,7 @@ export interface Task {
|
||||||
export type TaskType =
|
export type TaskType =
|
||||||
| "verify_speck" // Run Z3 verification on a Speck
|
| "verify_speck" // Run Z3 verification on a Speck
|
||||||
| "compile_to_dst" // Compile verified Speck to DST
|
| "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_code" // Generate code from verified Speck
|
||||||
| "generate_docs" // Generate documentation from provenance graph
|
| "generate_docs" // Generate documentation from provenance graph
|
||||||
| "integrate" // Integration/glue code
|
| "integrate" // Integration/glue code
|
||||||
|
|
@ -142,7 +142,7 @@ export interface TaskResult {
|
||||||
|
|
||||||
export interface ProvenanceNode {
|
export interface ProvenanceNode {
|
||||||
id: string;
|
id: string;
|
||||||
type: "speck" | "z3_assertion" | "dst" | "wasm" | "code" | "docs" | "event";
|
type: "speck" | "z3_assertion" | "dst" | "code" | "docs" | "event";
|
||||||
label: string;
|
label: string;
|
||||||
metadata: Record<string, unknown>;
|
metadata: Record<string, unknown>;
|
||||||
}
|
}
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue