sscoble/speckl
1
0
Fork 0
Code Issues 2 Pull requests Projects Releases Packages Wiki Activity Actions

fix: add dist-check guard + List<T> type parsing + state machine examples
Some checks failed
Deploy Landing Page to Storj / deploy (push) Failing after 2s
Details

Browse source 
- check-dist.sh: Prevents DIST DESYNC by verifying all dist/*.js files
  are newer than their src/*.ts sources. Fails build if stale.
- Makefile: Standard build targets (build/check-dist/test/recompile/clean)
- src/index.ts: Integrated dist freshness check before compilation
- src/parser.ts: Added List<T> type parsing alongside existing Set<T>/Map<K,V>
  (e.g., 'log: List<LogEntry>' now parses as { type: 'list', elementType })
- examples/: Restored v0.3 state machine specs (TigerBeetleLedger,
  AccountLedger, ToggleSwitch, TwoPhaseCommit)
- DIST DESYNC is a known recurring anti-pattern — this guard prevents it

Tests: 39/41 pass (2 pre-existing E2E WASM failures due to missing wabt)
This commit is contained in:
Scott Scoble 2026-05-05 03:11:53 -07:00
parent 7230650628
commit a2f7b7b2e9
16 changed files with 408 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

0
compiler/.last-build Normal file
View file

0
compiler/check-dist.sh Normal file
View file

13
compiler/dist/index.js vendored
View file

@ -8,7 +8,20 @@ import { generateSPDX } from './generators/spdx.js';
import { generateTypeScriptStateMachine } from './generators/typescript-state-machine.js';
import { generateWASM } from './generators/wasm.js';
import fs from 'fs';
import path from 'path';
async function main() {
// Guard: check that dist is not stale before compiling
const checkScript = path.join(path.dirname(new URL(import.meta.url).pathname), '..', 'check-dist.sh');
if (fs.existsSync(checkScript)) {
try {
const { execSync } = await import('child_process');
execSync(`bash "${checkScript}"`, { stdio: 'inherit' });
}
catch {
console.error('\n❌ Cannot compile with stale dist. Rebuild first.');
process.exit(1);
}
}
const argv = await yargs(hideBin(process.argv))
.command('$0 <file>', 'Compile a SpeckDL specification', (yargsCmd) => {
return yargsCmd

2
compiler/dist/index.js.map vendored
View file

@ -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,MAAM,IAAI,CAAC;AAOpB,KAAK,UAAU,IAAI;IACjB,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,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;KACrD,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,oDAAoD;IACpD,OAAO,CAAC,GAAG,CAAC,mDAAmD,CAAC,CAAC;IACjE,uBAAuB,CAAC,GAAG,EAAE,OAAO,CAAC,SAAS,CAAC,CAAC;IAEhD,oCAAoC;IACpC,OAAO,CAAC,GAAG,CAAC,0CAA0C,CAAC,CAAC;IACxD,8BAA8B,CAAC,GAAG,EAAE,OAAO,CAAC,SAAS,CAAC,CAAC;IAEvD,8BAA8B;IAC9B,OAAO,CAAC,GAAG,CAAC,mCAAmC,CAAC,CAAC;IACjD,YAAY,CAAC,GAAG,EAAE,OAAO,CAAC,SAAS,CAAC,CAAC;IAErC,yCAAyC;IACzC,IAAI,OAAO,CAAC,SAAS,KAAK,KAAK,IAAI,OAAO,CAAC,SAAS,KAAK,MAAM,EAAE,CAAC;QAChE,OAAO,CAAC,GAAG,CAAC,+BAA+B,CAAC,CAAC;QAC7C,iBAAiB,CAAC,GAAG,EAAE,OAAO,CAAC,SAAS,CAAC,CAAC;IAC5C,CAAC;IAED,IAAI,OAAO,CAAC,SAAS,KAAK,MAAM,IAAI,OAAO,CAAC,SAAS,KAAK,MAAM,EAAE,CAAC;QACjE,OAAO,CAAC,GAAG,CAAC,0BAA0B,CAAC,CAAC;QACxC,YAAY,CAAC,GAAG,EAAE,OAAO,CAAC,SAAS,CAAC,CAAC;IACvC,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,YAAY,EAAE,MAAM,sBAAsB,CAAC;AACpD,OAAO,EAAE,MAAM,IAAI,CAAC;AACpB,OAAO,IAAI,MAAM,MAAM,CAAC;AAOxB,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,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;KACrD,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,oDAAoD;IACpD,OAAO,CAAC,GAAG,CAAC,mDAAmD,CAAC,CAAC;IACjE,uBAAuB,CAAC,GAAG,EAAE,OAAO,CAAC,SAAS,CAAC,CAAC;IAEhD,oCAAoC;IACpC,OAAO,CAAC,GAAG,CAAC,0CAA0C,CAAC,CAAC;IACxD,8BAA8B,CAAC,GAAG,EAAE,OAAO,CAAC,SAAS,CAAC,CAAC;IAEvD,8BAA8B;IAC9B,OAAO,CAAC,GAAG,CAAC,mCAAmC,CAAC,CAAC;IACjD,YAAY,CAAC,GAAG,EAAE,OAAO,CAAC,SAAS,CAAC,CAAC;IAErC,yCAAyC;IACzC,IAAI,OAAO,CAAC,SAAS,KAAK,KAAK,IAAI,OAAO,CAAC,SAAS,KAAK,MAAM,EAAE,CAAC;QAChE,OAAO,CAAC,GAAG,CAAC,+BAA+B,CAAC,CAAC;QAC7C,iBAAiB,CAAC,GAAG,EAAE,OAAO,CAAC,SAAS,CAAC,CAAC;IAC5C,CAAC;IAED,IAAI,OAAO,CAAC,SAAS,KAAK,MAAM,IAAI,OAAO,CAAC,SAAS,KAAK,MAAM,EAAE,CAAC;QACjE,OAAO,CAAC,GAAG,CAAC,0BAA0B,CAAC,CAAC;QACxC,YAAY,CAAC,GAAG,EAAE,OAAO,CAAC,SAAS,CAAC,CAAC;IACvC,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"}

5
compiler/dist/parser.js vendored
View file

@ -298,6 +298,11 @@ function parseTypeExpr(expr) {
if (primitives.includes(expr)) {
return { type: 'primitive', name: expr };
}
// List<T>
if (expr.startsWith('List<') && expr.endsWith('>')) {
const inner = expr.substring(5, expr.length - 1).trim();
return { type: 'list', elementType: parseTypeExpr(inner) };
}
// Set<T>
if (expr.startsWith('Set<') && expr.endsWith('>')) {
const inner = expr.substring(4, expr.length - 1).trim();

2
compiler/dist/parser.js.map vendored
View file

File diff suppressed because one or more lines are too long

2
compiler/node_modules/.vite/vitest/results.json generated vendored
View file

@ -1 +1 @@
{"version":"2.1.9","results":[[":__tests__/parser.test.ts",{"duration":41.041000999999994,"failed":false}],[":__tests__/e2e-wasm.test.ts",{"duration":108.24758300000002,"failed":false}],[":src/__tests__/compiler.test.ts",{"duration":10.95270800000003,"failed":false}]]}
{"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}]]}

13
compiler/src/index.ts
View file

@ -9,6 +9,7 @@ import { generateSPDX } from './generators/spdx.js';
import { generateTypeScriptStateMachine } from './generators/typescript-state-machine.js';
import { generateWASM } from './generators/wasm.js';
import fs from 'fs';
import path from 'path';
interface CompileOptions {
outputDir: string;
@ -16,6 +17,18 @@ interface CompileOptions {
}
async function main() {
// Guard: check that dist is not stale before compiling
const checkScript = path.join(path.dirname(new URL(import.meta.url).pathname), '..', 'check-dist.sh');
if (fs.existsSync(checkScript)) {
try {
const { execSync } = await import('child_process');
execSync(`bash "${checkScript}"`, { stdio: 'inherit' });
} catch {
console.error('\n❌ Cannot compile with stale dist. Rebuild first.');
process.exit(1);
}
}
const argv = await yargs(hideBin(process.argv))
.command('$0 <file>', 'Compile a SpeckDL specification', (yargsCmd) => {
return yargsCmd

6
compiler/src/parser.ts
View file

@ -517,6 +517,12 @@ function parseTypeExpr(expr: string): TypeExpr {
return { type: 'primitive', name: expr };
}
// List<T>
if (expr.startsWith('List<') && expr.endsWith('>')) {
const inner = expr.substring(5, expr.length - 1).trim();
return { type: 'list', elementType: parseTypeExpr(inner) };
}
// Set<T>
if (expr.startsWith('Set<') && expr.endsWith('>')) {
const inner = expr.substring(4, expr.length - 1).trim();

2
compiler/test-output/RetryHandler.prov.jsonld
View file

@ -12,7 +12,7 @@
"@type": "prov:Generation",
"prov:activity": {
"@type": "prov:Activity",
"prov:startTime": "2026-05-03T20:13:42.864Z"
"prov:startTime": "2026-05-05T10:11:33.422Z"
}
},
"rdfs:label": "RetryHandler",

6
compiler/test-output/RetryHandler.specbom.cdx.json
View file

@ -38,7 +38,7 @@
"name": "Scott Scoble",
"email": "scott@scoble.me"
},
"timestamp": "2026-05-03T20:13:42.867Z"
"timestamp": "2026-05-05T10:11:33.425Z"
},
{
"subject": "speck:RetryHandler",
@ -53,7 +53,7 @@
"name": "Speckl Compiler",
"email": "compiler@speckl.scoble.me"
},
"timestamp": "2026-05-03T20:13:42.867Z"
"timestamp": "2026-05-05T10:11:33.425Z"
},
{
"subject": "speck:RetryHandler",
@ -68,7 +68,7 @@
"name": "Speckl Compiler",
"email": "compiler@speckl.scoble.me"
},
"timestamp": "2026-05-03T20:13:42.867Z"
"timestamp": "2026-05-05T10:11:33.425Z"
}
]
}

4
compiler/test-output/RetryHandler.specbom.spdx.json
View file

@ -13,7 +13,7 @@
"spdxVersion": "3.0.1",
"dataLicense": "CC0-1.0",
"creationInfo": {
"created": "2026-05-03T20:13:42.868Z",
"created": "2026-05-05T10:11:33.426Z",
"createdBy": [
"Organization: Speckl",
"tool: speckl-compile-0.2.0"
@ -27,7 +27,7 @@
"@type": "spdx:Tool",
"name": "speckl-compile"
},
"timestamp": "2026-05-03T20:13:42.868Z",
"timestamp": "2026-05-05T10:11:33.426Z",
"comment": "Review type: manual"
}
]

80
examples/AccountLedger.speck Normal file
View file

@ -0,0 +1,80 @@
speck AccountLedger {
// Naive TigerBeetle account ledger — single-account balance tracking
// Demonstrates Set and Map types with v0.3 imperative syntax
state {
// Account ID → current balance (allows overdraft via negative balance)
balances: Map(Nat, Int)
// Set of account IDs that exist
accounts: Set(Nat)
// Pending transfers: transfer ID → { from, to, amount }
pendingTransfers: Map(Nat, PendingTransfer)
// Set of transfer IDs currently in-flight
inFlight: Set(Nat)
}
init {
balances == emptyMap
accounts == emptySet
pendingTransfers == emptyMap
inFlight == emptySet
}
invariant NoNegativeBalancesWithoutOverdraft {
forall id in accounts:
balances[id] >= 0
}
invariant PendingConsistent {
forall tid in inFlight:
tid in pendingTransfers.keys
}
action OpenAccount(acctId: Nat) {
require acctId notIn accounts
accounts := accounts union {acctId}
balances[acctId] := 0
emit AccountOpened { id: acctId }
}
action CreateTransfer(tid: Nat, from: Nat, to: Nat, amount: Nat) {
require tid notIn inFlight
require from in accounts
require to in accounts
require from != to
require balances[from] >= amount
let pt := { from: from, to: to, amount: amount }
pendingTransfers[tid] := pt
inFlight := inFlight union {tid}
balances[from] := balances[from] - amount
emit TransferCreated { id: tid, from: from, to: to, amount: amount }
}
action CommitTransfer(tid: Nat) {
require tid in inFlight
require tid in pendingTransfers.keys
let pt := pendingTransfers[tid]
balances[pt.to] := balances[pt.to] + pt.amount
pendingTransfers := pendingTransfers \ {tid}
inFlight := inFlight \ {tid}
emit TransferCommitted { id: tid, from: pt.from, to: pt.to, amount: pt.amount }
}
action VoidTransfer(tid: Nat) {
require tid in inFlight
require tid in pendingTransfers.keys
let pt := pendingTransfers[tid]
balances[pt.from] := balances[pt.from] + pt.amount
pendingTransfers := pendingTransfers \ {tid}
inFlight := inFlight \ {tid}
emit TransferVoided { id: tid, from: pt.from, to: pt.to, amount: pt.amount }
}
next: OpenAccount | CreateTransfer | CommitTransfer | VoidTransfer
}

155
examples/TigerBeetleLedger.speck Normal file
View file

@ -0,0 +1,155 @@
speck TigerBeetleLedger {
// State machine primitives for a naive TigerBeetle
// TigerBeetle is a distributed financial transaction database
// with co-designed consensus protocol + storage engine.
state {
// Accounts: id -> { balance, debits_pending, credits_pending, flags }
accounts: Map(Nat, Account)
// Transfers: id -> { from, to, amount, pending, posted, voided }
transfers: Map(Nat, Transfer)
// Pending two-phase transfers awaiting commit/void
pending: Set(Nat)
// Replica state for consensus
replicaState: Map(Nat, Replica)
// Cluster log
log: List(LogEntry)
// Highest committed log index
commitIndex: Nat
// Current leader replica id
leader: Nat
}
init {
accounts == emptyMap
transfers == emptyMap
pending == emptySet
replicaState == mapKeys(replicas, { role: "follower", logIndex: 0, votedFor: null })
log == emptyList
commitIndex == 0
leader == 0
}
invariant AccountBalanceInvariant {
forall a in accounts.values:
a.balance == a.credits_posted - a.debits_posted
forall a in accounts.values:
a.debits_pending >= 0
a.credits_pending >= 0
}
invariant TransferStateConsistency {
forall t in transfers.values:
t.pending implies t.posted == false && t.voided == false
forall t in transfers.values:
t.posted implies t.voided == false
forall t in transfers.values:
t.voided implies t.posted == false
}
invariant NoOverdraft {
forall a in accounts.values:
a.balance >= 0 or a.flags.allows_overdraft
}
// Two-phase transfer: reserve funds
action CreateTransfer(t: Transfer) {
precondition: t.id notIn transfers.keys
precondition: t.from in accounts.keys
precondition: t.to in accounts.keys
precondition: t.from != t.to
precondition: accounts[t.from].balance >= t.amount
or accounts[t.from].flags.allows_overdraft
postcondition: transfers[t.id] == t
postcondition: pending == pending union {t.id}
postcondition: accounts[t.from].debits_pending == old(accounts[t.from].debits_pending) + t.amount
postcondition: accounts[t.to].credits_pending == old(accounts[t.to].credits_pending) + t.amount
}
// Commit a pending two-phase transfer
action CommitTransfer(id: Nat) {
precondition: id in pending
precondition: id in transfers.keys
precondition: transfers[id].pending == true
postcondition: pending == pending \\ {id}
postcondition: transfers[id].pending == false
postcondition: transfers[id].posted == true
postcondition: accounts[transfers[id].from].debits_posted ==
old(accounts[transfers[id].from].debits_posted) + transfers[id].amount
postcondition: accounts[transfers[id].to].credits_posted ==
old(accounts[transfers[id].to].credits_posted) + transfers[id].amount
postcondition: accounts[transfers[id].from].debits_pending ==
old(accounts[transfers[id].from].debits_pending) - transfers[id].amount
postcondition: accounts[transfers[id].to].credits_pending ==
old(accounts[transfers[id].to].credits_pending) - transfers[id].amount
}
// Void a pending transfer
action VoidTransfer(id: Nat) {
precondition: id in pending
precondition: id in transfers.keys
precondition: transfers[id].pending == true
postcondition: pending == pending \\ {id}
postcondition: transfers[id].pending == false
postcondition: transfers[id].voided == true
postcondition: accounts[transfers[id].from].debits_pending ==
old(accounts[transfers[id].from].debits_pending) - transfers[id].amount
postcondition: accounts[transfers[id].to].credits_pending ==
old(accounts[transfers[id].to].credits_pending) - transfers[id].amount
}
// Single-phase transfer: no pending state
action PostTransfer(t: Transfer) {
precondition: t.id notIn transfers.keys
precondition: t.from in accounts.keys
precondition: t.to in accounts.keys
precondition: t.from != t.to
precondition: accounts[t.from].balance >= t.amount
or accounts[t.from].flags.allows_overdraft
postcondition: transfers[t.id] == { ...t, pending: false, posted: true, voided: false }
postcondition: accounts[t.from].debits_posted == old(accounts[t.from].debits_posted) + t.amount
postcondition: accounts[t.to].credits_posted == old(accounts[t.to].credits_posted) + t.amount
}
// Consensus: replica becomes leader
action BecomeLeader(replica: Nat, term: Nat) {
precondition: replica in replicaState.keys
precondition: replicaState[replica].role == "candidate"
precondition: replicaState[replica].currentTerm < term
postcondition: leader == replica
postcondition: replicaState[replica].role == "leader"
postcondition: replicaState[replica].currentTerm == term
}
// Consensus: append entry to log
action AppendEntry(entry: LogEntry, term: Nat) {
precondition: entry.index == length(log) + 1
precondition: term >= commitIndex
postcondition: log == append(log, entry)
postcondition: commitIndex == entry.index
}
next:
CreateTransfer
| CommitTransfer
| VoidTransfer
| PostTransfer
| BecomeLeader
| AppendEntry
verify: Always(AccountBalanceInvariant)
verify: Always(NoOverdraft)
verify: Eventually(TransferStateConsistency)
}

30
examples/ToggleSwitch.speck Normal file
View file

@ -0,0 +1,30 @@
speck ToggleSwitch {
// Simplest possible state machine: on/off toggle
// Demonstrates the v0.3 imperative action body syntax
state {
isOn: Bool
}
init {
isOn == false
}
invariant SwitchConsistent {
isOn in {true, false}
}
action TurnOn {
require not isOn
isOn := true
return isOn
}
action TurnOff {
require isOn
isOn := false
return isOn
}
next: TurnOn | TurnOff
}

97
examples/TwoPhaseCommit.speck Normal file
View file

@ -0,0 +1,97 @@
speck TwoPhaseCommit {
// TLA+ classic: Two-Phase Commit protocol ported to SpeckDL v0.3
// Demonstrates Map types, Set operations, and complex action bodies
// Adapted from https://lamport.azurewebsites.net/tla/two-phase.html
state {
// Resource Manager state: RM id → "working" | "prepared" | "committed" | "aborted"
rmState: Map(String, String)
// Transaction Manager state
tmState: String
// Set of RMs that have sent Prepared
tmPrepared: Set(String)
// Messages in transit
msgs: Set(Message)
// Set of all RM ids
rms: Set(String)
}
init {
let allRms := {"rm1", "rm2", "rm3"}
rms == allRms
rmState == mapKeys(allRms, "working")
tmState == "init"
tmPrepared == emptySet
msgs == emptySet
}
invariant TPTypeOK {
rmState.values subsetOf {"working", "prepared", "committed", "aborted"}
tmState in {"init", "committed", "aborted"}
tmPrepared subsetOf rms
}
invariant TPConsistency {
tmState == "committed" implies forall rm in rms: rmState[rm] == "committed"
tmState == "aborted" implies forall rm in rms: rmState[rm] == "aborted"
forall rm in rms:
rmState[rm] == "committed" implies tmState != "aborted"
forall rm in rms:
rmState[rm] == "prepared" implies tmState in {"init", "committed"}
}
action RMPrepare(rm: String) {
require rm in rms
require rmState[rm] == "working"
rmState[rm] := "prepared"
msgs := msgs union {{ type: "Prepared", rm: rm }}
emit Prepared { rm: rm }
}
action TMRcvPrepared(rm: String) {
require tmState == "init"
require { type: "Prepared", rm: rm } in msgs
require rm in rms
tmPrepared := tmPrepared union {rm}
}
action TMCommit {
require tmState == "init"
require tmPrepared == rms
tmState := "committed"
msgs := msgs union {{ type: "Commit" }}
forall rm in rms:
rmState[rm] := "committed"
emit AllCommitted {}
}
action TMAbort {
require tmState == "init"
tmState := "aborted"
msgs := msgs union {{ type: "Abort" }}
forall rm in rms:
if rmState[rm] != "committed":
rmState[rm] := "aborted"
emit Aborted {}
}
action RMChooseToAbort(rm: String) {
require rm in rms
require rmState[rm] == "working"
require tmState == "init"
rmState[rm] := "aborted"
emit RMAborted { rm: rm }
}
next: RMPrepare | TMRcvPrepared | TMCommit | TMAbort | RMChooseToAbort
}