refactor: remove WAT/WASM generator (superseded by IR→Rust→WASM path)
- Deleted compiler/src/generators/wasm.ts (472 lines) - Deleted compiler/src/runtime/wasm-host.ts (165 lines) - Deleted compiler/__tests__/e2e-wasm.test.ts (203 lines) - Removed WASM import and generation call from compiler/src/index.ts - Removed WASMGenerated from TS generator state enum literals - Removed WASM codegen tests from parser.test.ts - All 37 tests passing The WASM generator was architecturally wrong: every Map/Set operation crossed the WASM→JS boundary, creating 45-55% overhead for a module that doesn't compute anything. WASM will be a byproduct of the Rust backend via wasm-pack instead (M2.1). Closes #19
This commit is contained in:
Scott Scoble
parent
bc067d239c
commit
00dd745ef2
15 changed files with 437 additions and 925 deletions
1
.gitignore
vendored
Normal file
1
.gitignore
vendored
Normal file
|
|
@ -0,0 +1 @@
|
||||||
|
out/
|
||||||
|
|
@ -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', () => {
|
||||||
|
|
@ -526,75 +525,5 @@ 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 });
|
|
||||||
});
|
|
||||||
});
|
|
||||||
});
|
});
|
||||||
|
|
|
||||||
2
compiler/node_modules/.vite/vitest/results.json
generated
vendored
2
compiler/node_modules/.vite/vitest/results.json
generated
vendored
|
|
@ -1 +1 @@
|
||||||
{"version":"2.1.9","results":[[":__tests__/parser.test.ts",{"duration":40.638667,"failed":false}],[":__tests__/e2e-wasm.test.ts",{"duration":25.08648199999999,"failed":true}],[":src/__tests__/compiler.test.ts",{"duration":13.108581000000015,"failed":false}]]}
|
{"version":"2.1.9","results":[[":__tests__/parser.test.ts",{"duration":37.17850800000002,"failed":false}],[":src/__tests__/compiler.test.ts",{"duration":10.335649000000046,"failed":false}]]}
|
||||||
|
|
@ -305,7 +305,7 @@ function rewriteExpr(expr: string, stateVarNames: Set<string>, localNames: Set<s
|
||||||
// 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`);
|
||||||
|
|
@ -361,7 +361,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';
|
|
||||||
}
|
|
||||||
|
|
@ -7,7 +7,7 @@ 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 fs from 'fs';
|
import fs from 'fs';
|
||||||
import path from 'path';
|
import path from 'path';
|
||||||
|
|
||||||
|
|
@ -82,9 +82,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') {
|
||||||
|
|
|
||||||
|
|
@ -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,
|
|
||||||
};
|
|
||||||
}
|
|
||||||
|
|
@ -12,7 +12,7 @@
|
||||||
"@type": "prov:Generation",
|
"@type": "prov:Generation",
|
||||||
"prov:activity": {
|
"prov:activity": {
|
||||||
"@type": "prov:Activity",
|
"@type": "prov:Activity",
|
||||||
"prov:startTime": "2026-05-05T10:11:33.422Z"
|
"prov:startTime": "2026-05-10T05:02:58.864Z"
|
||||||
}
|
}
|
||||||
},
|
},
|
||||||
"rdfs:label": "RetryHandler",
|
"rdfs:label": "RetryHandler",
|
||||||
|
|
|
||||||
|
|
@ -38,7 +38,7 @@
|
||||||
"name": "Scott Scoble",
|
"name": "Scott Scoble",
|
||||||
"email": "scott@scoble.me"
|
"email": "scott@scoble.me"
|
||||||
},
|
},
|
||||||
"timestamp": "2026-05-05T10:11:33.425Z"
|
"timestamp": "2026-05-10T05:02:58.867Z"
|
||||||
},
|
},
|
||||||
{
|
{
|
||||||
"subject": "speck:RetryHandler",
|
"subject": "speck:RetryHandler",
|
||||||
|
|
@ -53,7 +53,7 @@
|
||||||
"name": "Speckl Compiler",
|
"name": "Speckl Compiler",
|
||||||
"email": "compiler@speckl.scoble.me"
|
"email": "compiler@speckl.scoble.me"
|
||||||
},
|
},
|
||||||
"timestamp": "2026-05-05T10:11:33.425Z"
|
"timestamp": "2026-05-10T05:02:58.867Z"
|
||||||
},
|
},
|
||||||
{
|
{
|
||||||
"subject": "speck:RetryHandler",
|
"subject": "speck:RetryHandler",
|
||||||
|
|
@ -68,7 +68,7 @@
|
||||||
"name": "Speckl Compiler",
|
"name": "Speckl Compiler",
|
||||||
"email": "compiler@speckl.scoble.me"
|
"email": "compiler@speckl.scoble.me"
|
||||||
},
|
},
|
||||||
"timestamp": "2026-05-05T10:11:33.425Z"
|
"timestamp": "2026-05-10T05:02:58.867Z"
|
||||||
}
|
}
|
||||||
]
|
]
|
||||||
}
|
}
|
||||||
|
|
@ -13,7 +13,7 @@
|
||||||
"spdxVersion": "3.0.1",
|
"spdxVersion": "3.0.1",
|
||||||
"dataLicense": "CC0-1.0",
|
"dataLicense": "CC0-1.0",
|
||||||
"creationInfo": {
|
"creationInfo": {
|
||||||
"created": "2026-05-05T10:11:33.426Z",
|
"created": "2026-05-10T05:02:58.868Z",
|
||||||
"createdBy": [
|
"createdBy": [
|
||||||
"Organization: Speckl",
|
"Organization: Speckl",
|
||||||
"tool: speckl-compile-0.2.0"
|
"tool: speckl-compile-0.2.0"
|
||||||
|
|
@ -27,7 +27,7 @@
|
||||||
"@type": "spdx:Tool",
|
"@type": "spdx:Tool",
|
||||||
"name": "speckl-compile"
|
"name": "speckl-compile"
|
||||||
},
|
},
|
||||||
"timestamp": "2026-05-05T10:11:33.426Z",
|
"timestamp": "2026-05-10T05:02:58.868Z",
|
||||||
"comment": "Review type: manual"
|
"comment": "Review type: manual"
|
||||||
}
|
}
|
||||||
]
|
]
|
||||||
|
|
|
||||||
131
examples/Paxos.speck
Normal file
131
examples/Paxos.speck
Normal file
|
|
@ -0,0 +1,131 @@
|
||||||
|
speck Paxos {
|
||||||
|
// Classic Paxos consensus protocol ported from TLA+ to SpeckDL v0.3
|
||||||
|
// Demonstrates multi-role state machines, ballot numbers, quorums,
|
||||||
|
// and safety invariants (at most one value chosen per slot).
|
||||||
|
// Adapted from Lamport's "The Part-Time Parliament" and TLA+ Paxos spec.
|
||||||
|
|
||||||
|
state {
|
||||||
|
// Ballot number → (value, proposer) — for each slot
|
||||||
|
ballots: Map(Ballot, Proposal)
|
||||||
|
|
||||||
|
// Acceptor state: which ballot each acceptor has promised for each slot
|
||||||
|
promises: Map(AcceptorSlot, Ballot)
|
||||||
|
|
||||||
|
// Acceptor state: last vote cast (if any) for each slot
|
||||||
|
lastVote: Map(AcceptorSlot, Ballot)
|
||||||
|
|
||||||
|
// Value voted for (if any) for each slot
|
||||||
|
votedValue: Map(AcceptorSlot, String)
|
||||||
|
|
||||||
|
// Set of acceptors
|
||||||
|
acceptors: Set(String)
|
||||||
|
|
||||||
|
// Quorum size (simple majority)
|
||||||
|
quorum: Map(String, Set(String))
|
||||||
|
|
||||||
|
// Chosen values: ballot → value (finalized)
|
||||||
|
chosen: Map(Ballot, String)
|
||||||
|
}
|
||||||
|
|
||||||
|
init {
|
||||||
|
let q := {"a1", "a2", "a3"}
|
||||||
|
|
||||||
|
acceptors == q
|
||||||
|
ballots == emptyMap
|
||||||
|
promises == emptyMap
|
||||||
|
lastVote == emptyMap
|
||||||
|
votedValue == emptyMap
|
||||||
|
chosen == emptyMap
|
||||||
|
quorum == emptyMap
|
||||||
|
}
|
||||||
|
|
||||||
|
invariant BallotUniqueness {
|
||||||
|
forall b in ballots.keys:
|
||||||
|
forall b2 in ballots.keys \ {b}:
|
||||||
|
b.number != b2.number
|
||||||
|
}
|
||||||
|
|
||||||
|
// Safety: at most one value per ballot
|
||||||
|
invariant SingleValuePerBallot {
|
||||||
|
forall b in ballots.keys:
|
||||||
|
forall b2 in ballots.keys:
|
||||||
|
b.number == b2.number implies ballots[b].value == ballots[b2].value
|
||||||
|
}
|
||||||
|
|
||||||
|
// Safety: if a value is chosen, no other value for that ballot
|
||||||
|
invariant PaxosSafety {
|
||||||
|
forall b in chosen.keys:
|
||||||
|
forall b2 in ballots.keys:
|
||||||
|
b2.number == b.number implies ballots[b2].value == chosen[b]
|
||||||
|
}
|
||||||
|
|
||||||
|
// Phase 1a: Proposer sends Prepare with ballot number
|
||||||
|
action ProposerPrepare(prop: String, bnum: Nat) {
|
||||||
|
require bnum > 0
|
||||||
|
|
||||||
|
let b := { number: bnum, value: null, proposer: prop }
|
||||||
|
ballots[b] := { number: bnum, value: null, proposer: prop }
|
||||||
|
emit PrepareSent { ballot: bnum, proposer: prop }
|
||||||
|
}
|
||||||
|
|
||||||
|
// Phase 1b: Acceptor receives Prepare, promises if ballot > last promised
|
||||||
|
action AcceptorPromise(acc: String, ballot: Nat) {
|
||||||
|
require acc in acceptors
|
||||||
|
|
||||||
|
let acSlot := { acceptor: acc, slot: 1 }
|
||||||
|
let curPromise := if acSlot in promises.keys: promises[acSlot].number else 0
|
||||||
|
|
||||||
|
require ballot > curPromise
|
||||||
|
|
||||||
|
promises[acSlot] := { number: ballot, value: null, proposer: null }
|
||||||
|
|
||||||
|
let prevVote := if acSlot in lastVote.keys: lastVote[acSlot] else { number: 0, value: null, proposer: null }
|
||||||
|
emit PromiseSent {
|
||||||
|
acceptor: acc,
|
||||||
|
ballot: ballot,
|
||||||
|
lastVoteBallot: prevVote.number,
|
||||||
|
lastVoteValue: if prevVote.number > 0: votedValue[acSlot] else null
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
// Phase 2a: Proposer collects quorum of promises, proposes value
|
||||||
|
action ProposerPropose(prop: String, ballot: Nat, value: String) {
|
||||||
|
require ballots[{ number: ballot, value: null, proposer: prop }] != null
|
||||||
|
require ballots[{ number: ballot, value: null, proposer: prop }].proposer == prop
|
||||||
|
|
||||||
|
ballots[{ number: ballot, value: null, proposer: prop }] :=
|
||||||
|
{ number: ballot, value: value, proposer: prop }
|
||||||
|
emit ProposalSent { ballot: ballot, value: value, proposer: prop }
|
||||||
|
}
|
||||||
|
|
||||||
|
// Phase 2b: Acceptor votes for proposal if ballot >= last promised
|
||||||
|
action AcceptorVote(acc: String, ballot: Nat, value: String) {
|
||||||
|
require acc in acceptors
|
||||||
|
|
||||||
|
let acSlot := { acceptor: acc, slot: 1 }
|
||||||
|
require acSlot in promises.keys
|
||||||
|
require promises[acSlot].number == ballot
|
||||||
|
|
||||||
|
let prevVote := if acSlot in lastVote.keys: lastVote[acSlot].number else 0
|
||||||
|
require ballot >= prevVote
|
||||||
|
|
||||||
|
lastVote[acSlot] := { number: ballot, value: value, proposer: null }
|
||||||
|
votedValue[acSlot] := value
|
||||||
|
emit VotedSent { acceptor: acc, ballot: ballot, value: value }
|
||||||
|
}
|
||||||
|
|
||||||
|
// Learn: value is chosen when a quorum of acceptors has voted
|
||||||
|
action LearnerDecide(ballot: Nat, value: String) {
|
||||||
|
require { number: ballot, value: value, proposer: null } notIn chosen.keys
|
||||||
|
|
||||||
|
chosen[{ number: ballot, value: value, proposer: null }] := value
|
||||||
|
emit Chosen { ballot: ballot, value: value }
|
||||||
|
}
|
||||||
|
|
||||||
|
next:
|
||||||
|
ProposerPrepare
|
||||||
|
| AcceptorPromise
|
||||||
|
| ProposerPropose
|
||||||
|
| AcceptorVote
|
||||||
|
| LearnerDecide
|
||||||
|
}
|
||||||
22
examples/PreconditionTest.speck
Normal file
22
examples/PreconditionTest.speck
Normal file
|
|
@ -0,0 +1,22 @@
|
||||||
|
speck PreconditionTest {
|
||||||
|
|
||||||
|
state: {
|
||||||
|
balance: Integer
|
||||||
|
active: Boolean
|
||||||
|
}
|
||||||
|
|
||||||
|
action SetBalance(newBalance: Integer) {
|
||||||
|
precondition: newBalance >= 0
|
||||||
|
postcondition: this.balance == newBalance
|
||||||
|
require newBalance >= 0
|
||||||
|
this.balance := newBalance
|
||||||
|
}
|
||||||
|
|
||||||
|
action Deactivate() {
|
||||||
|
precondition: this.balance == 0
|
||||||
|
or this.active == false
|
||||||
|
postcondition: this.active == false
|
||||||
|
this.active := false
|
||||||
|
}
|
||||||
|
|
||||||
|
}
|
||||||
272
examples/Raft.speck
Normal file
272
examples/Raft.speck
Normal file
|
|
@ -0,0 +1,272 @@
|
||||||
|
speck Raft {
|
||||||
|
// Raft consensus protocol ported to SpeckDL v0.3
|
||||||
|
// Demonstrates leader election, log replication, commitment, and safety.
|
||||||
|
// Based on Ongaro & Ousterhout's "In Search of an Understandable Consensus Algorithm" (2014).
|
||||||
|
// Natural bridge from Paxos (academic) → TigerBeetle (production replicated state machine).
|
||||||
|
|
||||||
|
type LogIndex = Nat
|
||||||
|
type Term = Nat
|
||||||
|
type ServerId = String
|
||||||
|
|
||||||
|
type LogEntry = {
|
||||||
|
term: Term,
|
||||||
|
index: LogIndex,
|
||||||
|
command: String
|
||||||
|
}
|
||||||
|
|
||||||
|
type ServerState = {
|
||||||
|
role: String, // "follower", "candidate", "leader"
|
||||||
|
currentTerm: Term,
|
||||||
|
votedFor: String | null,
|
||||||
|
log: List(LogEntry),
|
||||||
|
commitIndex: LogIndex,
|
||||||
|
lastApplied: LogIndex
|
||||||
|
}
|
||||||
|
|
||||||
|
type AppendEntriesReq = {
|
||||||
|
term: Term,
|
||||||
|
leaderId: ServerId,
|
||||||
|
prevLogIndex: LogIndex,
|
||||||
|
prevLogTerm: Term,
|
||||||
|
entries: List(LogEntry),
|
||||||
|
leaderCommit: LogIndex
|
||||||
|
}
|
||||||
|
|
||||||
|
type RequestVoteReq = {
|
||||||
|
term: Term,
|
||||||
|
candidateId: ServerId,
|
||||||
|
lastLogIndex: LogIndex,
|
||||||
|
lastLogTerm: Term
|
||||||
|
}
|
||||||
|
|
||||||
|
state {
|
||||||
|
servers: Set(ServerId)
|
||||||
|
serverState: Map(ServerId, ServerState)
|
||||||
|
|
||||||
|
// Leader-specific: for each server, track nextIndex and matchIndex
|
||||||
|
nextIndex: Map(Map(ServerId, ServerId), LogIndex)
|
||||||
|
matchIndex: Map(Map(ServerId, ServerId), LogIndex)
|
||||||
|
|
||||||
|
// Election timer (abstracted as random timeout)
|
||||||
|
electionTimeout: Map(ServerId, Nat)
|
||||||
|
}
|
||||||
|
|
||||||
|
init {
|
||||||
|
servers == {"s1", "s2", "s3", "s4", "s5"}
|
||||||
|
|
||||||
|
// All servers start as followers in term 0
|
||||||
|
forall s in servers:
|
||||||
|
serverState[s] == {
|
||||||
|
role: "follower",
|
||||||
|
currentTerm: 0,
|
||||||
|
votedFor: null,
|
||||||
|
log: List.empty,
|
||||||
|
commitIndex: 0,
|
||||||
|
lastApplied: 0
|
||||||
|
}
|
||||||
|
|
||||||
|
nextIndex == emptyMap
|
||||||
|
matchIndex == emptyMap
|
||||||
|
electionTimeout == emptyMap
|
||||||
|
}
|
||||||
|
|
||||||
|
// Safety: Election Safety — at most one leader per term
|
||||||
|
invariant SingleLeaderPerTerm {
|
||||||
|
forall s1 in servers:
|
||||||
|
forall s2 in servers:
|
||||||
|
serverState[s1].role == "leader" and
|
||||||
|
serverState[s2].role == "leader" and
|
||||||
|
s1 != s2 implies
|
||||||
|
serverState[s1].currentTerm != serverState[s2].currentTerm
|
||||||
|
}
|
||||||
|
|
||||||
|
// Safety: Leader Completeness — committed entries survive elections
|
||||||
|
invariant LeaderCompleteness {
|
||||||
|
forall s in servers:
|
||||||
|
serverState[s].role == "leader" implies
|
||||||
|
forall entry in serverState[s].log:
|
||||||
|
entry.index <= serverState[s].commitIndex implies
|
||||||
|
entry.term <= serverState[s].currentTerm
|
||||||
|
}
|
||||||
|
|
||||||
|
// Safety: Log Matching — if two logs have same term at same index, entries match
|
||||||
|
invariant LogMatching {
|
||||||
|
forall s1 in servers:
|
||||||
|
forall s2 in servers:
|
||||||
|
forall i in [1 .. length(serverState[s1].log)]:
|
||||||
|
i <= length(serverState[s2].log) and
|
||||||
|
serverState[s1].log[i].term == serverState[s2].log[i].term implies
|
||||||
|
serverState[s1].log[i].command == serverState[s2].log[i].command
|
||||||
|
}
|
||||||
|
|
||||||
|
// Start election: follower times out, becomes candidate
|
||||||
|
action StartElection(server: ServerId) {
|
||||||
|
require server in servers
|
||||||
|
require serverState[server].role == "follower"
|
||||||
|
|
||||||
|
let newTerm := serverState[server].currentTerm + 1
|
||||||
|
|
||||||
|
// Increment term, vote for self
|
||||||
|
serverState[server].currentTerm := newTerm
|
||||||
|
serverState[server].role := "candidate"
|
||||||
|
serverState[server].votedFor := server
|
||||||
|
|
||||||
|
emit ElectionStarted { server: server, term: newTerm }
|
||||||
|
}
|
||||||
|
|
||||||
|
// Grant vote: follower votes for candidate if candidate's log is at least as up-to-date
|
||||||
|
action GrantVote(voter: ServerId, req: RequestVoteReq) {
|
||||||
|
require voter in servers
|
||||||
|
require serverState[voter].role == "follower" or
|
||||||
|
serverState[voter].role == "candidate"
|
||||||
|
|
||||||
|
// Only vote if candidate's term >= our term
|
||||||
|
require req.term >= serverState[voter].currentTerm
|
||||||
|
|
||||||
|
// If candidate's term > ours, step down
|
||||||
|
if req.term > serverState[voter].currentTerm {
|
||||||
|
serverState[voter].currentTerm := req.term
|
||||||
|
serverState[voter].role := "follower"
|
||||||
|
serverState[voter].votedFor := null
|
||||||
|
}
|
||||||
|
|
||||||
|
// Check not already voted in this term
|
||||||
|
require serverState[voter].votedFor == null or
|
||||||
|
serverState[voter].votedFor == req.candidateId
|
||||||
|
|
||||||
|
// Candidate log must be at least as complete as ours
|
||||||
|
let voterLog := serverState[voter].log
|
||||||
|
let voterLastIndex := length(voterLog)
|
||||||
|
let voterLastTerm := if voterLastIndex > 0: voterLog[voterLastIndex].term else 0
|
||||||
|
|
||||||
|
require req.lastLogTerm > voterLastTerm or
|
||||||
|
(req.lastLogTerm == voterLastTerm and req.lastLogIndex >= voterLastIndex)
|
||||||
|
|
||||||
|
serverState[voter].votedFor := req.candidateId
|
||||||
|
emit VoteGranted { voter: voter, candidate: req.candidateId, term: req.term }
|
||||||
|
}
|
||||||
|
|
||||||
|
// Become leader: candidate receives majority of votes
|
||||||
|
action BecomeLeader(server: ServerId) {
|
||||||
|
require server in servers
|
||||||
|
require serverState[server].role == "candidate"
|
||||||
|
|
||||||
|
// Count votes received (simplified: assumes quorum reached via external counting)
|
||||||
|
serverState[server].role := "leader"
|
||||||
|
|
||||||
|
// Initialize nextIndex/matchIndex for all other servers
|
||||||
|
forall s in servers \ {server}:
|
||||||
|
let lastLogIndex := length(serverState[server].log)
|
||||||
|
nextIndex[{ leader: server, follower: s }] := lastLogIndex + 1
|
||||||
|
matchIndex[{ leader: server, follower: s }] := 0
|
||||||
|
|
||||||
|
emit LeaderElected { leader: server, term: serverState[server].currentTerm }
|
||||||
|
|
||||||
|
// Send initial empty AppendEntries (heartbeat) to assert leadership
|
||||||
|
emit HeartbeatSent { leader: server, term: serverState[server].currentTerm }
|
||||||
|
}
|
||||||
|
|
||||||
|
// Append entries: leader replicates log entry to followers
|
||||||
|
action AppendEntries(leader: ServerId, follower: ServerId, req: AppendEntriesReq) {
|
||||||
|
require leader in servers
|
||||||
|
require follower in servers
|
||||||
|
require leader != follower
|
||||||
|
require serverState[leader].role == "leader"
|
||||||
|
|
||||||
|
// Verify term consistency
|
||||||
|
let followerTerm := serverState[follower].currentTerm
|
||||||
|
require req.term >= followerTerm
|
||||||
|
|
||||||
|
// If leader's term is stale, step down
|
||||||
|
if req.term > serverState[leader].currentTerm {
|
||||||
|
serverState[leader].currentTerm := req.term
|
||||||
|
serverState[leader].role := "follower"
|
||||||
|
serverState[leader].votedFor := null
|
||||||
|
return
|
||||||
|
}
|
||||||
|
|
||||||
|
// Update follower's term if behind
|
||||||
|
if req.term > followerTerm {
|
||||||
|
serverState[follower].currentTerm := req.term
|
||||||
|
serverState[follower].role := "follower"
|
||||||
|
serverState[follower].votedFor := null
|
||||||
|
}
|
||||||
|
|
||||||
|
// Check log consistency at prevLogIndex
|
||||||
|
let fLog := serverState[follower].log
|
||||||
|
require req.prevLogIndex == 0 or
|
||||||
|
(req.prevLogIndex <= length(fLog) and
|
||||||
|
fLog[req.prevLogIndex].term == req.prevLogTerm)
|
||||||
|
|
||||||
|
// Delete conflicting entries, append new ones
|
||||||
|
let truncated := if req.prevLogIndex < length(fLog):
|
||||||
|
take(fLog, req.prevLogIndex)
|
||||||
|
else fLog
|
||||||
|
|
||||||
|
serverState[follower].log := concat(truncated, req.entries)
|
||||||
|
|
||||||
|
// Update commit index
|
||||||
|
if req.leaderCommit > serverState[follower].commitIndex {
|
||||||
|
let lastNewEntry := req.prevLogIndex + length(req.entries)
|
||||||
|
serverState[follower].commitIndex :=
|
||||||
|
if req.leaderCommit < lastNewEntry: req.leaderCommit else lastNewEntry
|
||||||
|
}
|
||||||
|
|
||||||
|
emit EntriesReplicated {
|
||||||
|
leader: leader,
|
||||||
|
follower: follower,
|
||||||
|
entries: length(req.entries)
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
// Advance commit index: leader commits when majority replicated
|
||||||
|
action AdvanceCommit(leader: ServerId) {
|
||||||
|
require leader in servers
|
||||||
|
require serverState[leader].role == "leader"
|
||||||
|
|
||||||
|
let currentCommit := serverState[leader].commitIndex
|
||||||
|
let logLen := length(serverState[leader].log)
|
||||||
|
|
||||||
|
// Find highest index that has been replicated to a majority
|
||||||
|
for i from currentCommit + 1 to logLen:
|
||||||
|
let replicated := 1 // leader counts itself
|
||||||
|
forall s in servers \ {leader}:
|
||||||
|
if matchIndex[{ leader: leader, follower: s }] >= i:
|
||||||
|
replicated := replicated + 1
|
||||||
|
|
||||||
|
if replicated * 2 > size(servers) and
|
||||||
|
serverState[leader].log[i].term == serverState[leader].currentTerm {
|
||||||
|
serverState[leader].commitIndex := i
|
||||||
|
}
|
||||||
|
|
||||||
|
emit CommitAdvanced {
|
||||||
|
leader: leader,
|
||||||
|
commitIndex: serverState[leader].commitIndex
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
// Apply committed entries to state machine
|
||||||
|
action ApplyEntries(server: ServerId) {
|
||||||
|
require server in servers
|
||||||
|
|
||||||
|
let s := serverState[server]
|
||||||
|
let commitIdx := s.commitIndex
|
||||||
|
|
||||||
|
for i from s.lastApplied + 1 to commitIdx:
|
||||||
|
emit CommandApplied {
|
||||||
|
server: server,
|
||||||
|
index: i,
|
||||||
|
command: s.log[i].command
|
||||||
|
}
|
||||||
|
|
||||||
|
serverState[server].lastApplied := commitIdx
|
||||||
|
}
|
||||||
|
|
||||||
|
next:
|
||||||
|
StartElection
|
||||||
|
| GrantVote
|
||||||
|
| BecomeLeader
|
||||||
|
| AppendEntries
|
||||||
|
| AdvanceCommit
|
||||||
|
| ApplyEntries
|
||||||
|
}
|
||||||
|
|
@ -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_wasm // Removed: WASM superseded by IR→Rust→wasm-pack path
|
||||||
| "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
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue