feat(rust): Rust codegen backend (speckl#24)
Some checks failed
Deploy Landing Page to Storj / deploy (push) Failing after 2s
Some checks failed
Deploy Landing Page to Storj / deploy (push) Failing after 2s
- New generator: compiler/src/generators/rust.ts (652 lines) - --target=rust CLI option produces full Rust crate (Cargo.toml + src/lib.rs) - Types: Nat→u64, Bool→bool, String→String, Set→HashSet, Map→HashMap - State variables → Rust struct fields - Actions → Rust impl methods returning Result - Expression rewriter: .contains(&x), .get(&k), .len(), etc. - Tested against ToggleSwitch, TigerBeetleLedger, KafkaKRaft - All 37 existing tests pass WASM path: .speck → Rust → wasm-pack → WASM (now complete)
This commit is contained in:
Scott Scoble
parent
e86af21cc7
commit
f62bdc33f5
10 changed files with 961 additions and 19 deletions
16
compiler/dist/index.js
vendored
16
compiler/dist/index.js
vendored
|
|
@ -7,6 +7,7 @@ import { generateCycloneDX } from './generators/cyclonedx.js';
|
|||
import { generateSPDX } from './generators/spdx.js';
|
||||
import { generateTypeScriptStateMachine } from './generators/typescript-state-machine.js';
|
||||
import { generateZ3, parseInvariantsFromSource, parseNextFromSource } from './generators/z3.js';
|
||||
import { generateRust } from './generators/rust.js';
|
||||
import fs from 'fs';
|
||||
import path from 'path';
|
||||
async function main() {
|
||||
|
|
@ -40,7 +41,7 @@ async function main() {
|
|||
alias: 't',
|
||||
describe: 'Compilation target',
|
||||
type: 'string',
|
||||
choices: ['typescript', 'z3', 'all'],
|
||||
choices: ['typescript', 'z3', 'rust', 'all'],
|
||||
default: 'typescript',
|
||||
})
|
||||
.option('verify-depth', {
|
||||
|
|
@ -78,8 +79,13 @@ async function main() {
|
|||
}
|
||||
// Read raw source for invariant/next parsing that the AST parser doesn't handle yet
|
||||
const rawSource = fs.readFileSync(file, 'utf-8');
|
||||
// Always generate provenance (it's the core output) if not z3-only
|
||||
if (options.target !== 'z3') {
|
||||
// Generate Rust state machine if target is rust or all
|
||||
if (options.target === 'rust' || options.target === 'all') {
|
||||
console.log('\nGenerating Rust state machine...');
|
||||
generateRust(ast, options.outputDir);
|
||||
}
|
||||
// Always generate provenance (it's the core output) if not z3-only or rust-only
|
||||
if (options.target !== 'z3' && options.target !== 'rust') {
|
||||
console.log('\nGenerating provenance graph (PROV-O JSON-LD)...');
|
||||
generateProvenanceGraph(ast, options.outputDir);
|
||||
}
|
||||
|
|
@ -97,8 +103,8 @@ async function main() {
|
|||
const z3Options = { verifyDepth: options.verifyDepth };
|
||||
generateZ3(ast, options.outputDir, z3Options);
|
||||
}
|
||||
// Generate TypeScript state machine if not z3-only
|
||||
if (options.target !== 'z3') {
|
||||
// Generate TypeScript state machine if not z3-only or rust-only
|
||||
if (options.target !== 'z3' && options.target !== 'rust') {
|
||||
console.log('\nGenerating TypeScript state machine...');
|
||||
generateTypeScriptStateMachine(ast, options.outputDir);
|
||||
// Generate BOM based on format selection
|
||||
|
|
|
|||
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,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"}
|
||||
{"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,YAAY,EAAE,MAAM,sBAAsB,CAAC;AACpD,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,MAAM,EAAE,KAAK,CAAC;YAC5C,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,MAA8C;QAC3D,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,uDAAuD;IACvD,IAAI,OAAO,CAAC,MAAM,KAAK,MAAM,IAAI,OAAO,CAAC,MAAM,KAAK,KAAK,EAAE,CAAC;QAC1D,OAAO,CAAC,GAAG,CAAC,oCAAoC,CAAC,CAAC;QAClD,YAAY,CAAC,GAAG,EAAE,OAAO,CAAC,SAAS,CAAC,CAAC;IACvC,CAAC;IAED,gFAAgF;IAChF,IAAI,OAAO,CAAC,MAAM,KAAK,IAAI,IAAI,OAAO,CAAC,MAAM,KAAK,MAAM,EAAE,CAAC;QACzD,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,gEAAgE;IAChE,IAAI,OAAO,CAAC,MAAM,KAAK,IAAI,IAAI,OAAO,CAAC,MAAM,KAAK,MAAM,EAAE,CAAC;QACzD,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"}
|
||||
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":36.549328,"failed":false}],[":src/__tests__/compiler.test.ts",{"duration":13.904341000000045,"failed":false}]]}
|
||||
{"version":"2.1.9","results":[[":__tests__/parser.test.ts",{"duration":37.504659999999944,"failed":false}],[":src/__tests__/compiler.test.ts",{"duration":10.64781099999999,"failed":false}]]}
|
||||
652
compiler/src/generators/rust.ts
Normal file
652
compiler/src/generators/rust.ts
Normal file
|
|
@ -0,0 +1,652 @@
|
|||
import { AST, SpeckNode, MemberNode, StateNode, InitNode, ActionNode, ConstraintNode, VerifyNode, EventNode } from '../parser.js';
|
||||
import fs from 'fs';
|
||||
import path from 'path';
|
||||
|
||||
/**
|
||||
* Generate Rust state machine from a SpeckDL spec.
|
||||
*
|
||||
* Outputs a self-contained .rs file with:
|
||||
* - State struct with snake_case fields
|
||||
* - State machine impl with action methods returning Result
|
||||
* - Invariant check functions
|
||||
* - Event enums
|
||||
* - Cargo.toml for full crate builds
|
||||
*
|
||||
* Pattern:
|
||||
* state → Rust struct fields
|
||||
* actions → Rust methods (Result return, guard errors)
|
||||
* invariants → Rust functions returning bool
|
||||
* events → Rust structs
|
||||
*/
|
||||
|
||||
export function generateRust(ast: AST, outputDir: string): void {
|
||||
for (const speck of ast.specks) {
|
||||
const code = emitSpeck(speck);
|
||||
|
||||
// Create a subdirectory per speck for Cargo.toml + src/lib.rs
|
||||
const speckDir = path.join(outputDir, speck.name);
|
||||
const srcDir = path.join(speckDir, 'src');
|
||||
if (!fs.existsSync(srcDir)) {
|
||||
fs.mkdirSync(srcDir, { recursive: true });
|
||||
}
|
||||
|
||||
const libPath = path.join(srcDir, 'lib.rs');
|
||||
fs.writeFileSync(libPath, code);
|
||||
console.log(`Generated Rust crate: ${libPath}`);
|
||||
|
||||
// Write Cargo.toml
|
||||
const cargoToml = `[package]
|
||||
name = "${snakeCase(speck.name)}"
|
||||
version = "0.1.0"
|
||||
edition = "2021"
|
||||
description = "Auto-generated Speck state machine: ${speck.name}"
|
||||
|
||||
[dependencies]
|
||||
`;
|
||||
fs.writeFileSync(path.join(speckDir, 'Cargo.toml'), cargoToml);
|
||||
console.log(`Generated Cargo.toml: ${speckDir}/Cargo.toml`);
|
||||
}
|
||||
}
|
||||
|
||||
function emitSpeck(speck: SpeckNode): string {
|
||||
const deduped = new Map<string, MemberNode>();
|
||||
for (const m of speck.members) {
|
||||
const key = memberKey(m);
|
||||
const existing = deduped.get(key);
|
||||
if (!existing || isEmptyStub(existing)) {
|
||||
deduped.set(key, m);
|
||||
}
|
||||
}
|
||||
const members = Array.from(deduped.values());
|
||||
|
||||
const stateNode = members.find(m => m.type === 'state') as StateNode | undefined;
|
||||
const initNode = members.find(m => m.type === 'init') as InitNode | undefined;
|
||||
const actions = members.filter(m => m.type === 'action') as ActionNode[];
|
||||
const events = members.filter(m => m.type === 'event') as EventNode[];
|
||||
const constraints = members.filter(m => m.type === 'constraint') as ConstraintNode[];
|
||||
const verifies = members.filter(m => m.type === 'verify') as VerifyNode[];
|
||||
|
||||
// Collect enum-like interfaces
|
||||
const allInterfaces = members.filter(m => m.type === 'interface') as any[];
|
||||
const enumInterfaces = allInterfaces.filter(iface => iface?.methods?.length > 0);
|
||||
|
||||
let stateValues: string[] = [];
|
||||
if (enumInterfaces.length > 0) {
|
||||
for (const iface of enumInterfaces) {
|
||||
stateValues.push(...iface.methods.map((m: any) => m.name));
|
||||
}
|
||||
} else {
|
||||
const seen = new Set<string>();
|
||||
const builtinTypes = new Set(['String', 'Nat', 'Int', 'Bool', 'Real', 'Bytes', 'Date', 'Number']);
|
||||
for (const a of actions) {
|
||||
for (const s of a.statements) {
|
||||
if (s.type === 'require') {
|
||||
const matches = s.expr.match(/\b[A-Z][a-zA-Z]+\b/g);
|
||||
if (matches) {
|
||||
matches.forEach((m: string) => {
|
||||
if (!builtinTypes.has(m)) seen.add(m);
|
||||
});
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
stateValues = Array.from(seen).sort();
|
||||
}
|
||||
if (stateValues.length === 0) stateValues = ['Open', 'Closed'];
|
||||
|
||||
// Build enum map
|
||||
const enumMap = new Map<string, string[]>();
|
||||
for (const iface of enumInterfaces) {
|
||||
enumMap.set(iface.name, iface.methods.map((m: any) => m.name));
|
||||
}
|
||||
|
||||
// Determine state enum name
|
||||
const stateVarType = stateNode?.variables?.[0]?.typeExpr;
|
||||
let stateEnumName = `${speck.name}State`;
|
||||
if (stateVarType?.type === 'ident' && stateVarType.name) {
|
||||
const cleanTypeName = cleanName(stateVarType.name);
|
||||
stateEnumName = `${speck.name}${cleanTypeName}`;
|
||||
} else if (enumMap.size > 0) {
|
||||
const firstEnum = enumMap.keys().next().value;
|
||||
if (firstEnum) stateEnumName = `${speck.name}${firstEnum}`;
|
||||
}
|
||||
|
||||
if (enumInterfaces.length === 0) {
|
||||
enumMap.set(stateEnumName.replace(speck.name, ''), stateValues);
|
||||
}
|
||||
|
||||
// Scan event field types for secondary enums
|
||||
const eventFieldTypes = new Set<string>();
|
||||
for (const ev of events) {
|
||||
for (const f of ev.fields) {
|
||||
if (f.type?.type === 'ident' && f.type.name) {
|
||||
const typeName = cleanName(f.type.name);
|
||||
if (typeName !== stateEnumName.replace(speck.name, '')) {
|
||||
eventFieldTypes.add(typeName);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
for (const iface of allInterfaces) {
|
||||
const ifaceName = cleanName(iface.name);
|
||||
if (eventFieldTypes.has(ifaceName)) {
|
||||
if (iface.methods?.length > 0) {
|
||||
enumMap.set(ifaceName, iface.methods.map((m: any) => m.name));
|
||||
} else {
|
||||
const seen = new Set<string>();
|
||||
const builtinTypes = new Set(['String', 'Nat', 'Int', 'Bool', 'Real', 'Bytes', 'Date', 'Number']);
|
||||
for (const a of actions) {
|
||||
for (const s of a.statements) {
|
||||
if (s.type === 'require') {
|
||||
const matches = s.expr.match(/\b[A-Z][a-zA-Z]+\b/g);
|
||||
if (matches) {
|
||||
matches.forEach((m: string) => {
|
||||
if (!builtinTypes.has(m)) seen.add(m);
|
||||
});
|
||||
}
|
||||
}
|
||||
if (s.type === 'emit') {
|
||||
for (const f of s.fields) {
|
||||
const matches = f.value.match(/\b[A-Z][a-zA-Z]+\b/g);
|
||||
if (matches) {
|
||||
matches.forEach((m: string) => {
|
||||
if (!builtinTypes.has(m)) seen.add(m);
|
||||
});
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
const primaryValues = new Set(enumMap.get(stateEnumName.replace(speck.name, '')) || []);
|
||||
const secondaryValues = Array.from(seen).filter(v => !primaryValues.has(v));
|
||||
if (secondaryValues.length > 0) {
|
||||
enumMap.set(ifaceName, secondaryValues.sort());
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
// Generate Rust enums
|
||||
const allEnums: string[] = [];
|
||||
for (const [enumName, values] of enumMap) {
|
||||
const fullEnumName = `${speck.name}${enumName}`;
|
||||
const variants = values.map((v: string) => ` ${v},`).join('\n');
|
||||
const enumDef = `#[derive(Debug, Clone, Copy, PartialEq, Eq)]\n` +
|
||||
`pub enum ${fullEnumName} {\n${variants}\n}`;
|
||||
allEnums.push(enumDef);
|
||||
|
||||
const displayArms = values.map((v: string) =>
|
||||
` ${fullEnumName}::${v} => write!(f, "${snakeCase(v)}"),`
|
||||
).join('\n');
|
||||
const displayImpl = `impl std::fmt::Display for ${fullEnumName} {\n` +
|
||||
` fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {\n` +
|
||||
` match self {\n${displayArms}\n` +
|
||||
` }\n` +
|
||||
` }\n` +
|
||||
`}`;
|
||||
allEnums.push(displayImpl);
|
||||
}
|
||||
const stateEnum = allEnums.join('\n\n');
|
||||
|
||||
// Event structs
|
||||
const eventStructs = events.map(e => {
|
||||
const fields = e.fields.map(f => {
|
||||
const name = snakeCase(cleanName(f.name));
|
||||
const ty = rustType(f.type, speck.name, enumMap);
|
||||
return ` pub ${name}: ${ty},`;
|
||||
}).join('\n');
|
||||
return `#[derive(Debug, Clone)]\npub struct ${e.name} {\n${fields}\n}`;
|
||||
}).join('\n\n');
|
||||
|
||||
const structName = `${speck.name}Machine`;
|
||||
|
||||
// State variables with original name + snake_case name mapping
|
||||
const stateVars = (stateNode?.variables ?? []).map(v => ({
|
||||
origName: cleanName(v.name),
|
||||
rustName: snakeCase(cleanName(v.name)),
|
||||
typeExpr: v.typeExpr,
|
||||
defaultInit: v.defaultInit,
|
||||
}));
|
||||
|
||||
// Build name mapping for expression rewriting: original name → Rust field name
|
||||
const nameMap = new Map<string, string>();
|
||||
for (const v of stateVars) {
|
||||
nameMap.set(v.origName, v.rustName);
|
||||
}
|
||||
|
||||
// For expression matching, use the original names
|
||||
const stateVarOrigNames = new Set(stateVars.map(v => v.origName));
|
||||
|
||||
// Map variable original names (for bracket -> index rewriting)
|
||||
const mapVarOrigNames = new Set(stateVars
|
||||
.filter(v => v.typeExpr?.type === 'map' || (v.typeExpr?.type === 'ident' && v.typeExpr?.name && /^Map/i.test(v.typeExpr.name)))
|
||||
.map(v => v.origName));
|
||||
|
||||
// State struct fields
|
||||
const stateFields = stateVars.map(v => {
|
||||
return ` pub ${v.rustName}: ${rustType(v.typeExpr, speck.name, enumMap)},`;
|
||||
}).join('\n');
|
||||
|
||||
// Collect all known state values for the rewriter
|
||||
const allKnownStateValues: string[] = [];
|
||||
for (const values of enumMap.values()) {
|
||||
allKnownStateValues.push(...values);
|
||||
}
|
||||
|
||||
// Init assignments
|
||||
const initAssignments = initNode
|
||||
? initNode.assignments.map(a => {
|
||||
const rustName = snakeCase(cleanName(a.name));
|
||||
const expr = cleanExpr(a.expr);
|
||||
const rewritten = rewriteRustExpr(
|
||||
expr, nameMap, mapVarOrigNames, new Set(),
|
||||
stateEnumName, allKnownStateValues
|
||||
);
|
||||
return ` ${rustName}: ${rewritten},`;
|
||||
}).join('\n')
|
||||
: '';
|
||||
// If no explicit init assignments, emit defaults for all state vars
|
||||
const initFields = initAssignments || stateVars.map(v => {
|
||||
const defaultValue = defaultRustValue(v.rustName, v.typeExpr);
|
||||
return ` ${v.rustName}: ${defaultValue},`;
|
||||
}).join('\n');
|
||||
|
||||
// Action methods
|
||||
const actionMethods = actions
|
||||
.map(a => emitAction(a, stateVarOrigNames, nameMap, mapVarOrigNames, speck.name, stateEnumName, allKnownStateValues, enumMap))
|
||||
.join('\n\n');
|
||||
|
||||
// Invariant checks
|
||||
const invariantChecks = constraints.map((c, i) =>
|
||||
` /// C${i + 1}: ${c.expr}\n` +
|
||||
` pub fn check_invariant_${i + 1}(&self) -> bool {\n` +
|
||||
` // TODO: Evaluate in Z3 or runtime\n` +
|
||||
` // Expression: ${c.expr}\n` +
|
||||
` true\n` +
|
||||
` }`
|
||||
).join('\n\n');
|
||||
|
||||
// Verify stubs
|
||||
const verifyChecks = verifies.map((v, i) =>
|
||||
` /// V${i + 1}: ${v.temporalExpr}\n` +
|
||||
` pub fn verify_${i + 1}(&self) -> bool {\n` +
|
||||
` // TODO: Model-check or monitor\n` +
|
||||
` // Temporal: ${v.temporalExpr}\n` +
|
||||
` true\n` +
|
||||
` }`
|
||||
).join('\n\n');
|
||||
|
||||
// Decision log type
|
||||
const logEventType = events.length > 0 ? `Vec<${events[0].name}>` : 'Vec<String>';
|
||||
|
||||
// Struct definition
|
||||
const structDef = `/// Speck state machine: ${speck.name}\n` +
|
||||
`/// Auto-generated Rust state machine from SpeckDL specification.\n` +
|
||||
`#[derive(Debug, Clone)]\n` +
|
||||
`pub struct ${structName} {\n${stateFields}\n` +
|
||||
` /// Decision log of events emitted during execution\n` +
|
||||
` pub decision_log: ${logEventType},\n` +
|
||||
`}`;
|
||||
|
||||
// Constructor impl
|
||||
const constructor = `impl ${structName} {\n` +
|
||||
` /// Create a new ${speck.name} machine in its initial state.\n` +
|
||||
` pub fn new() -> Self {\n` +
|
||||
` Self {\n` +
|
||||
`${initFields}\n` +
|
||||
` decision_log: Vec::new(),\n` +
|
||||
` }\n` +
|
||||
` }\n` +
|
||||
`}`;
|
||||
|
||||
// Action impl block
|
||||
const actionImpl = `// Action methods — each returns Result with guard checking\n` +
|
||||
`impl ${structName} {\n${actionMethods}\n}`;
|
||||
|
||||
// Invariant impl block
|
||||
const invariantImpl = constraints.length > 0
|
||||
? `\n// Invariant checks\nimpl ${structName} {\n${invariantChecks}\n}`
|
||||
: '';
|
||||
|
||||
// Verify impl block
|
||||
const verifyImpl = verifies.length > 0
|
||||
? `\n// Temporal verification stubs\nimpl ${structName} {\n${verifyChecks}\n}`
|
||||
: '';
|
||||
|
||||
const file =
|
||||
`// Auto-generated by speckl-compile from ${speck.name}\n` +
|
||||
`// DO NOT EDIT MANUALLY — regenerate from .speckdl source\n\n` +
|
||||
`use std::collections::{HashMap, HashSet};\n\n` +
|
||||
`${stateEnum}\n\n` +
|
||||
`${eventStructs}\n\n` +
|
||||
`${structDef}\n\n` +
|
||||
`${constructor}\n\n` +
|
||||
`${actionImpl}\n` +
|
||||
`${invariantImpl}\n` +
|
||||
`${verifyImpl}\n`;
|
||||
|
||||
return file;
|
||||
}
|
||||
|
||||
function emitAction(
|
||||
action: ActionNode,
|
||||
stateVarOrigNames: Set<string>,
|
||||
nameMap: Map<string, string>,
|
||||
mapVarOrigNames: Set<string>,
|
||||
speckName: string,
|
||||
stateEnumName: string,
|
||||
knownStateValues: string[],
|
||||
enumMap: Map<string, string[]>
|
||||
): string {
|
||||
const localNames = new Set(action.params.map(p => cleanName(p.name)));
|
||||
|
||||
const params = action.params
|
||||
.map(p => `${snakeCase(cleanName(p.name))}: ${rustType(p.type, speckName, enumMap)}`)
|
||||
.join(', ');
|
||||
|
||||
const methodName = snakeCase(action.name);
|
||||
|
||||
// Preconditions
|
||||
const preconditions = action.statements
|
||||
.filter(s => s.type === 'precondition')
|
||||
.map(s => {
|
||||
const expr = rewriteRustExpr(s.expr, nameMap, mapVarOrigNames, localNames, stateEnumName, knownStateValues);
|
||||
return ` // precondition: ${s.expr}\n if !(${expr}) {\n return Err(format!("Precondition failed: {}", ${JSON.stringify(s.expr)}));\n }`;
|
||||
})
|
||||
.join('\n');
|
||||
|
||||
// Requires (guards)
|
||||
const requires = action.statements
|
||||
.filter(s => s.type === 'require')
|
||||
.map(s => {
|
||||
const expr = rewriteRustExpr(s.expr, nameMap, mapVarOrigNames, localNames, stateEnumName, knownStateValues);
|
||||
return ` if !(${expr}) {\n return Err(format!("Guard failed: {}", ${JSON.stringify(s.expr)}));\n }`;
|
||||
})
|
||||
.join('\n');
|
||||
|
||||
// Assignments
|
||||
const assigns = action.statements
|
||||
.filter(s => s.type === 'assign')
|
||||
.map(s => {
|
||||
const target = snakeCase(cleanName(s.target));
|
||||
const expr = rewriteRustExpr(s.expr, nameMap, mapVarOrigNames, localNames, stateEnumName, knownStateValues);
|
||||
return ` self.${target} = ${expr};`;
|
||||
})
|
||||
.join('\n');
|
||||
|
||||
// Emits
|
||||
const emits = action.statements
|
||||
.filter(s => s.type === 'emit')
|
||||
.map(s => {
|
||||
const fields = s.fields
|
||||
.map(f => {
|
||||
const name = snakeCase(cleanName(f.name));
|
||||
const val = rewriteRustExpr(f.value, nameMap, mapVarOrigNames, localNames, stateEnumName, knownStateValues);
|
||||
return ` ${name}: ${val},`;
|
||||
})
|
||||
.join('\n');
|
||||
return ` self.decision_log.push(${s.event} {\n${fields}\n });`;
|
||||
})
|
||||
.join('\n');
|
||||
|
||||
// Postconditions
|
||||
const postconditions = action.statements
|
||||
.filter(s => s.type === 'postcondition')
|
||||
.map(s => {
|
||||
const expr = rewriteRustExpr(s.expr, nameMap, mapVarOrigNames, localNames, stateEnumName, knownStateValues);
|
||||
return ` // postcondition: ${s.expr}\n if !(${expr}) {\n return Err(format!("Postcondition failed: {}", ${JSON.stringify(s.expr)}));\n }`;
|
||||
})
|
||||
.join('\n');
|
||||
|
||||
// Returns
|
||||
const returnStmts = action.statements
|
||||
.filter(s => s.type === 'return')
|
||||
.map(s => {
|
||||
const expr = rewriteRustExpr(s.expr, nameMap, mapVarOrigNames, localNames, stateEnumName, knownStateValues);
|
||||
return ` Ok(${expr})`;
|
||||
})
|
||||
.join('\n');
|
||||
|
||||
const guards = [preconditions, requires].filter(s => s.length > 0);
|
||||
const mutations = [assigns, emits].filter(s => s.length > 0);
|
||||
const postPost = [postconditions, returnStmts].filter(s => s.length > 0);
|
||||
|
||||
const bodyParts: string[] = [];
|
||||
if (guards.length > 0) bodyParts.push(guards.join('\n'));
|
||||
if (mutations.length > 0) bodyParts.push(mutations.join('\n'));
|
||||
if (postPost.length > 0) bodyParts.push(postPost.join('\n'));
|
||||
|
||||
const body = bodyParts.join('\n');
|
||||
|
||||
// Determine return type
|
||||
const hasReturn = action.statements.some(s => s.type === 'return');
|
||||
const returnType = hasReturn ? ' -> Result<bool, String>' : ' -> Result<(), String>';
|
||||
|
||||
return ` /// Execute action: ${action.name}\n pub fn ${methodName}(&mut self${params ? ', ' + params : ''})${returnType} {\n${body || ' Ok(())\n'}\n }`;
|
||||
}
|
||||
|
||||
/**
|
||||
* Rewrite SpeckDL expressions to valid Rust.
|
||||
*
|
||||
* @param nameMap - Maps original SpeckDL variable names → Rust snake_case field names (e.g. isOn → is_on)
|
||||
* @param mapVarNames - Set of original variable names that are Map-typed (for bracket access rewriting)
|
||||
*/
|
||||
function rewriteRustExpr(
|
||||
expr: string,
|
||||
nameMap: Map<string, string>,
|
||||
mapVarOrigNames: Set<string>,
|
||||
localNames: Set<string>,
|
||||
stateEnumName: string,
|
||||
knownStateValues: string[]
|
||||
): string {
|
||||
function shouldPrefix(ident: string): boolean {
|
||||
return nameMap.has(ident) && !localNames.has(ident);
|
||||
}
|
||||
|
||||
function rustify(ident: string): string {
|
||||
const mapped = nameMap.get(ident);
|
||||
return mapped ? `self.${mapped}` : ident;
|
||||
}
|
||||
|
||||
// Step 1: Replace function calls
|
||||
let rust = expr
|
||||
.replace(/\bnow\(\)/g, '0u64 /* TODO: use std::time::SystemTime */')
|
||||
.replace(/\blen\(([^)]+)\)/g, '$1.len()')
|
||||
.replace(/\blength\(([^)]+)\)/g, '$1.len()')
|
||||
.replace(/\bjoin\(([^,]+),\s*([^)]+)\)/g, '$1.join($2)')
|
||||
.replace(/\bappend\(([^,]+),\s*([^)]+)\)/g, '{$1.push($2); $1} /* append */')
|
||||
.replace(/\bforall\s+(\w+)\s+in\s+([^:]+):\s*(.+)/g, '$2.iter().all(|$1| $3)');
|
||||
|
||||
// Step 2: Replace state enum literals with Rust enum refs BEFORE identifier replacement
|
||||
const allStateValues = new Set<string>(knownStateValues);
|
||||
['Open','Grooming','Groomed','Assigned','InProgress','InReview','Merged','Blocked','Closed','Idle','Parsing','Parsed','ProvenanceGenerated','BOMsGenerated','TypeScriptGenerated','Done'].forEach(s => allStateValues.add(s));
|
||||
if (allStateValues.size > 0) {
|
||||
const stateValueRegex = new RegExp('\\b(' + Array.from(allStateValues).join('|') + ')\\b', 'g');
|
||||
rust = rust.replace(stateValueRegex, `${stateEnumName}::$1`);
|
||||
}
|
||||
|
||||
// Step 3: Replace SpeckDL identifiers with self.rust_name if they're state vars
|
||||
// Split on non-identifier boundaries
|
||||
const tokens = rust.split(/([\s\(\)\[\]{}+\-*/=<>!&|.,;:'"`]+)/);
|
||||
const result = tokens.map(tok => {
|
||||
if (/^[a-zA-Z_]\w*::\w+$/.test(tok)) return tok; // already :: (enum ref)
|
||||
if (/^[a-zA-Z_]\w*\.\w+$/.test(tok)) return tok; // already dot (field access)
|
||||
if (/^(true|false|null|None|Some|Ok|Err|not|and|or|in|notIn|old|forall)$/.test(tok)) return tok;
|
||||
if (/^\d+$/.test(tok)) return tok;
|
||||
if (/^[a-zA-Z_]\w*$/.test(tok) && shouldPrefix(tok)) {
|
||||
return rustify(tok);
|
||||
}
|
||||
return tok;
|
||||
}).join('');
|
||||
|
||||
rust = result
|
||||
// Undo self. prefix that accidentally got added after bracket access
|
||||
.replace(/\]\.self\.(\w+)/g, '].$1');
|
||||
|
||||
// Step 4: Translate SpeckDL expression patterns to Rust
|
||||
|
||||
// 4a: notIn -> !collection.contains(&key)
|
||||
rust = rust.replace(/(\S+)\s+notIn\s+(\S+)\.keys/g, '!$2.contains_key(&$1)');
|
||||
// x in map.keys -> map.contains_key(&x)
|
||||
rust = rust.replace(/(\S+)\s+in\s+(\S+)\.keys/g, '$2.contains_key(&$1)');
|
||||
// x in set -> set.contains(&x) (but be careful not to match Rust keywords)
|
||||
rust = rust.replace(/(\S+)\s+in\s+(\S+)/g, (match, key, collection) => {
|
||||
const reserved = new Set(['true','false','self','mut','ref','let','fn','pub','use','mod','struct','enum','impl','for','while','loop','if','else','match','return','where','as','move','dyn','unsafe','extern','crate','super','Self']);
|
||||
if (reserved.has(collection)) return match;
|
||||
return `${collection}.contains(&${key})`;
|
||||
});
|
||||
// notIn plain (not .keys)
|
||||
rust = rust.replace(/(\S+)\s+notIn\s+(\S+)/g, '!$2.contains(&$1)');
|
||||
|
||||
// 4b: not expr → !expr (SpeckDL 'not' keyword)
|
||||
// Need to handle 'not' followed by an identifier — this was already handled above with self-dot rewrite
|
||||
// But plain 'not ident' must become '!self.field_name'
|
||||
rust = rust.replace(/\bnot\s+([a-zA-Z_]\w*)/g, '!$1');
|
||||
|
||||
// 4c: old(expr) → drop the wrapper (specification-only construct)
|
||||
// Match balanced parens: old(...)
|
||||
rust = rust.replace(/old\(([^()]*(?:\([^()]*\)[^()]*)*)\)/g, '$1');
|
||||
|
||||
// 4d: Set union: pending union {t.id}
|
||||
rust = rust.replace(/(\S+)\s+union\s+\{([^}]+)\}/g, '{$1.clone().into_iter().chain(std::iter::once($2)).collect()}');
|
||||
|
||||
// 4e: Set difference: pending \\ {id}
|
||||
rust = rust.replace(/(\S+)\s+\\\\\s+\{([^}]+)\}/g, '{$1.clone().into_iter().filter(|x| x != &$2).collect()}');
|
||||
|
||||
// 4f: Map access via brackets → bracket indexing (Rust uses &key for HashMap)
|
||||
for (const mapVar of mapVarOrigNames) {
|
||||
const rustMapVar = nameMap.get(mapVar) || snakeCase(mapVar);
|
||||
// Handle self.field_name[expr] or bare field_name[expr]
|
||||
// Must run BEFORE identifier replacement so original names match
|
||||
const pattern1 = new RegExp(`(self\\.)?(${escapeRegex(rustMapVar)})\\[([^\\]]+)\\]`, 'g');
|
||||
rust = rust.replace(pattern1, '$1$2[&$3]');
|
||||
// Also handle original name in brackets (e.g. accounts[...])
|
||||
const pattern2 = new RegExp(`(self\\.)?(${escapeRegex(mapVar)})\\[([^\\]]+)\\]`, 'g');
|
||||
rust = rust.replace(pattern2, (match, p1, _p2, p3) => {
|
||||
const prefix = p1 || '';
|
||||
return `${prefix}${rustMapVar}[&${p3}]`;
|
||||
});
|
||||
}
|
||||
|
||||
// 4g: .size() → .len() (Rust collections use .len())
|
||||
rust = rust.replace(/\.size\(\)/g, '.len()');
|
||||
|
||||
// 4h: == → keeps == (Rust uses ==), but handle === → ==
|
||||
rust = rust.replace(/\b===\b/g, '==');
|
||||
|
||||
// 4i: != keeps != in Rust
|
||||
|
||||
// 4j: Clean up trailing standalone comparisons
|
||||
rust = rust.replace(/(\S+)\s*==\s*$/g, '$1 == $1');
|
||||
rust = rust.replace(/(\S+)\s*===\s*$/g, '$1 == $1');
|
||||
|
||||
return rust.trim();
|
||||
}
|
||||
|
||||
// Helpers ------------------------------------------------------------------
|
||||
|
||||
function memberKey(m: MemberNode): string {
|
||||
if (m.type === 'action') return `action:${m.name}`;
|
||||
if (m.type === 'event') return `event:${m.name}`;
|
||||
if (m.type === 'interface') return `interface:${m.name}`;
|
||||
if (m.type === 'state') return 'state';
|
||||
if (m.type === 'init') return 'init';
|
||||
if (m.type === 'provenance') return 'provenance';
|
||||
if (m.type === 'bom') return 'bom';
|
||||
if (m.type === 'input') return 'input';
|
||||
if (m.type === 'output') return 'output';
|
||||
return m.type;
|
||||
}
|
||||
|
||||
function isEmptyStub(m: MemberNode): boolean {
|
||||
if (m.type === 'state') return m.variables.length === 0;
|
||||
if (m.type === 'init') return m.assignments.length === 0;
|
||||
if (m.type === 'action') return m.statements.length === 0;
|
||||
if (m.type === 'event') return m.fields.length === 0;
|
||||
if (m.type === 'interface') return m.methods.length === 0;
|
||||
if (m.type === 'provenance') return m.clauses.length === 0;
|
||||
if (m.type === 'bom') return !m.compiler && !m.solver && !m.runtime;
|
||||
return false;
|
||||
}
|
||||
|
||||
function cleanName(s: string): string {
|
||||
return s.replace(/,$/, '').trim();
|
||||
}
|
||||
|
||||
function cleanExpr(s: string): string {
|
||||
return s.replace(/,$/, '').trim();
|
||||
}
|
||||
|
||||
function snakeCase(s: string): string {
|
||||
// Convert CamelCase/PascalCase to snake_case
|
||||
return s
|
||||
.replace(/([A-Z]+)([A-Z][a-z])/g, '$1_$2')
|
||||
.replace(/([a-z\d])([A-Z])/g, '$1_$2')
|
||||
.replace(/([a-zA-Z])(\d)/g, '$1_$2')
|
||||
.replace(/[^a-zA-Z0-9_]/g, '_')
|
||||
.toLowerCase()
|
||||
.replace(/_+/g, '_')
|
||||
.replace(/^_|_$/g, '');
|
||||
}
|
||||
|
||||
function escapeRegex(s: string): string {
|
||||
return s.replace(/[.*+?^${}()|[\]\\]/g, '\\$&');
|
||||
}
|
||||
|
||||
function defaultRustValue(rustName: string, typeExpr: any): string {
|
||||
if (!typeExpr) return 'Default::default()'; // not ideal but a fallback
|
||||
if (typeExpr.type === 'primitive') {
|
||||
switch (typeExpr.name) {
|
||||
case 'Nat': return '0u64';
|
||||
case 'Int': return '0i64';
|
||||
case 'Real': case 'Number': return '0.0f64';
|
||||
case 'Bool': return 'false';
|
||||
case 'String': return 'String::new()';
|
||||
case 'Bytes': return 'Vec::new()';
|
||||
default: return 'Default::default()';
|
||||
}
|
||||
}
|
||||
if (typeExpr.type === 'list') return 'Vec::new()';
|
||||
if (typeExpr.type === 'set') return 'HashSet::new()';
|
||||
if (typeExpr.type === 'map') return 'HashMap::new()';
|
||||
return 'Default::default()';
|
||||
}
|
||||
|
||||
function rustType(t: any, speckName: string = '', enumMap?: Map<string, string[]>): string {
|
||||
if (!t) return '()';
|
||||
if (t.type === 'primitive') {
|
||||
const map: Record<string, string> = {
|
||||
Nat: 'u64', Int: 'i64', Real: 'f64',
|
||||
Bool: 'bool', String: 'String', Bytes: 'Vec<u8>',
|
||||
Number: 'f64',
|
||||
};
|
||||
return map[t.name] || t.name.toLowerCase();
|
||||
}
|
||||
if (t.type === 'list') return `Vec<${rustType(t.elementType, speckName, enumMap)}>`;
|
||||
if (t.type === 'set') return `HashSet<${rustType(t.elementType, speckName, enumMap)}>`;
|
||||
if (t.type === 'map') return `HashMap<${rustType(t.keyType, speckName, enumMap)}, ${rustType(t.valueType, speckName, enumMap)}>`;
|
||||
if (t.type === 'record') {
|
||||
const fields = t.fields.map((f: any) => {
|
||||
const name = snakeCase(cleanName(f.name));
|
||||
return `pub ${name}: ${rustType(f.type, speckName, enumMap)}`;
|
||||
}).join(', ');
|
||||
return `${snakeCase(speckName)}_record { ${fields} }`;
|
||||
}
|
||||
if (t.type === 'ident') {
|
||||
const rawName = cleanName(t.name);
|
||||
if (enumMap && enumMap.has(rawName)) {
|
||||
return `${speckName}${rawName}`;
|
||||
}
|
||||
if (rawName === 'Account') return 'Account';
|
||||
if (rawName === 'Transfer') return 'Transfer';
|
||||
if (rawName === 'Replica') return 'Replica';
|
||||
if (rawName === 'LogEntry') return 'LogEntry';
|
||||
if (rawName === 'Nat') return 'u64';
|
||||
if (rawName === 'Int') return 'i64';
|
||||
if (rawName === 'Bool') return 'bool';
|
||||
if (rawName === 'String') return 'String';
|
||||
// Opaque identifiers become type aliases
|
||||
return rawName;
|
||||
}
|
||||
return '()';
|
||||
}
|
||||
|
|
@ -8,6 +8,7 @@ import { generateCycloneDX } from './generators/cyclonedx.js';
|
|||
import { generateSPDX } from './generators/spdx.js';
|
||||
import { generateTypeScriptStateMachine } from './generators/typescript-state-machine.js';
|
||||
import { generateZ3, Z3Options, parseInvariantsFromSource, parseNextFromSource } from './generators/z3.js';
|
||||
import { generateRust } from './generators/rust.js';
|
||||
import fs from 'fs';
|
||||
import path from 'path';
|
||||
|
||||
|
|
@ -49,7 +50,7 @@ async function main() {
|
|||
alias: 't',
|
||||
describe: 'Compilation target',
|
||||
type: 'string',
|
||||
choices: ['typescript', 'z3', 'all'],
|
||||
choices: ['typescript', 'z3', 'rust', 'all'],
|
||||
default: 'typescript' as const,
|
||||
})
|
||||
.option('verify-depth', {
|
||||
|
|
@ -73,7 +74,7 @@ async function main() {
|
|||
const options = {
|
||||
outputDir: argv.outputDir as string,
|
||||
bomFormat: argv.bomFormat as 'cdx' | 'spdx' | 'both',
|
||||
target: argv.target as 'typescript' | 'z3' | 'all',
|
||||
target: argv.target as 'typescript' | 'z3' | 'rust' | 'all',
|
||||
verifyDepth: argv.verifyDepth as number,
|
||||
};
|
||||
|
||||
|
|
@ -94,8 +95,14 @@ async function main() {
|
|||
// Read raw source for invariant/next parsing that the AST parser doesn't handle yet
|
||||
const rawSource = fs.readFileSync(file, 'utf-8');
|
||||
|
||||
// Always generate provenance (it's the core output) if not z3-only
|
||||
if (options.target !== 'z3') {
|
||||
// Generate Rust state machine if target is rust or all
|
||||
if (options.target === 'rust' || options.target === 'all') {
|
||||
console.log('\nGenerating Rust state machine...');
|
||||
generateRust(ast, options.outputDir);
|
||||
}
|
||||
|
||||
// Always generate provenance (it's the core output) if not z3-only or rust-only
|
||||
if (options.target !== 'z3' && options.target !== 'rust') {
|
||||
console.log('\nGenerating provenance graph (PROV-O JSON-LD)...');
|
||||
generateProvenanceGraph(ast, options.outputDir);
|
||||
}
|
||||
|
|
@ -115,8 +122,8 @@ async function main() {
|
|||
generateZ3(ast, options.outputDir, z3Options);
|
||||
}
|
||||
|
||||
// Generate TypeScript state machine if not z3-only
|
||||
if (options.target !== 'z3') {
|
||||
// Generate TypeScript state machine if not z3-only or rust-only
|
||||
if (options.target !== 'z3' && options.target !== 'rust') {
|
||||
console.log('\nGenerating TypeScript state machine...');
|
||||
generateTypeScriptStateMachine(ast, options.outputDir);
|
||||
|
||||
|
|
|
|||
7
compiler/test-output-rust/TigerBeetleLedger/Cargo.toml
Normal file
7
compiler/test-output-rust/TigerBeetleLedger/Cargo.toml
Normal file
|
|
@ -0,0 +1,7 @@
|
|||
[package]
|
||||
name = "tiger_beetle_ledger"
|
||||
version = "0.1.0"
|
||||
edition = "2021"
|
||||
description = "Auto-generated Speck state machine: TigerBeetleLedger"
|
||||
|
||||
[dependencies]
|
||||
270
compiler/test-output-rust/TigerBeetleLedger/src/lib.rs
Normal file
270
compiler/test-output-rust/TigerBeetleLedger/src/lib.rs
Normal file
|
|
@ -0,0 +1,270 @@
|
|||
// Auto-generated by speckl-compile from TigerBeetleLedger
|
||||
// DO NOT EDIT MANUALLY — regenerate from .speckdl source
|
||||
|
||||
use std::collections::{HashMap, HashSet};
|
||||
|
||||
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
|
||||
pub enum TigerBeetleLedgerState {
|
||||
Open,
|
||||
Closed,
|
||||
}
|
||||
|
||||
impl std::fmt::Display for TigerBeetleLedgerState {
|
||||
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
|
||||
match self {
|
||||
TigerBeetleLedgerState::Open => write!(f, "open"),
|
||||
TigerBeetleLedgerState::Closed => write!(f, "closed"),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
|
||||
/// Speck state machine: TigerBeetleLedger
|
||||
/// Auto-generated Rust state machine from SpeckDL specification.
|
||||
#[derive(Debug, Clone)]
|
||||
pub struct TigerBeetleLedgerMachine {
|
||||
pub accounts: HashMap<u64, Account>,
|
||||
pub transfers: HashMap<u64, Transfer>,
|
||||
pub pending: HashSet<u64>,
|
||||
pub replica_state: HashMap<u64, Replica>,
|
||||
pub log: Vec<LogEntry>,
|
||||
pub commit_index: u64,
|
||||
pub leader: u64,
|
||||
/// Decision log of events emitted during execution
|
||||
pub decision_log: Vec<String>,
|
||||
}
|
||||
|
||||
impl TigerBeetleLedgerMachine {
|
||||
/// Create a new TigerBeetleLedger machine in its initial state.
|
||||
pub fn new() -> Self {
|
||||
Self {
|
||||
accounts: HashMap::new(),
|
||||
transfers: HashMap::new(),
|
||||
pending: HashSet::new(),
|
||||
replica_state: HashMap::new(),
|
||||
log: Vec::new(),
|
||||
commit_index: 0u64,
|
||||
leader: 0u64,
|
||||
decision_log: Vec::new(),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
// Action methods — each returns Result with guard checking
|
||||
impl TigerBeetleLedgerMachine {
|
||||
/// Execute action: CreateTransfer
|
||||
pub fn create_transfer(&mut self, t: Transfer) -> Result<(), String> {
|
||||
// precondition: t.id notIn transfers.keys
|
||||
if !(!self.transfers.contains_key(&t.id)) {
|
||||
return Err(format!("Precondition failed: {}", "t.id notIn transfers.keys"));
|
||||
}
|
||||
// precondition: t.from in accounts.keys
|
||||
if !(self.accounts.contains_key(&t.from)) {
|
||||
return Err(format!("Precondition failed: {}", "t.from in accounts.keys"));
|
||||
}
|
||||
// precondition: t.to in accounts.keys
|
||||
if !(self.accounts.contains_key(&t.to)) {
|
||||
return Err(format!("Precondition failed: {}", "t.to in accounts.keys"));
|
||||
}
|
||||
// precondition: t.from != t.to
|
||||
if !(t.from != t.to) {
|
||||
return Err(format!("Precondition failed: {}", "t.from != t.to"));
|
||||
}
|
||||
// precondition: accounts[t.from].balance >= t.amount || accounts[t.from].flags.allows_overdraft
|
||||
if !(self.accounts[&&t.from].balance >= t.amount || self.accounts[&&t.from].flags.allows_overdraft) {
|
||||
return Err(format!("Precondition failed: {}", "accounts[t.from].balance >= t.amount || accounts[t.from].flags.allows_overdraft"));
|
||||
}
|
||||
// postcondition: transfers[t.id] == t
|
||||
if !(self.transfers[&&t.id] == t) {
|
||||
return Err(format!("Postcondition failed: {}", "transfers[t.id] == t"));
|
||||
}
|
||||
// postcondition: pending == pending union {t.id}
|
||||
if !(self.pending == {self.pending.clone().into_iter().chain(std::iter::once(t.id)).collect()}) {
|
||||
return Err(format!("Postcondition failed: {}", "pending == pending union {t.id}"));
|
||||
}
|
||||
// postcondition: accounts[t.from].debits_pending == old(accounts[t.from].debits_pending) + t.amount
|
||||
if !(self.accounts[&&t.from].debits_pending == self.accounts[&&t.from].debits_pending + t.amount) {
|
||||
return Err(format!("Postcondition failed: {}", "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
|
||||
if !(self.accounts[&&t.to].credits_pending == self.accounts[&&t.to].credits_pending + t.amount) {
|
||||
return Err(format!("Postcondition failed: {}", "accounts[t.to].credits_pending == old(accounts[t.to].credits_pending) + t.amount"));
|
||||
}
|
||||
}
|
||||
|
||||
/// Execute action: CommitTransfer
|
||||
pub fn commit_transfer(&mut self, id: u64) -> Result<(), String> {
|
||||
// precondition: id in pending
|
||||
if !(self.pending.contains(&id)) {
|
||||
return Err(format!("Precondition failed: {}", "id in pending"));
|
||||
}
|
||||
// precondition: id in transfers.keys
|
||||
if !(self.transfers.contains_key(&id)) {
|
||||
return Err(format!("Precondition failed: {}", "id in transfers.keys"));
|
||||
}
|
||||
// precondition: transfers[id].pending == true
|
||||
if !(self.transfers[&&id].pending == true) {
|
||||
return Err(format!("Precondition failed: {}", "transfers[id].pending == true"));
|
||||
}
|
||||
// postcondition: pending == pending \\ {id}
|
||||
if !(self.pending == {self.pending.clone().into_iter().filter(|x| x != &id).collect()}) {
|
||||
return Err(format!("Postcondition failed: {}", "pending == pending \\\\ {id}"));
|
||||
}
|
||||
// postcondition: transfers[id].pending == false
|
||||
if !(self.transfers[&&id].pending == false) {
|
||||
return Err(format!("Postcondition failed: {}", "transfers[id].pending == false"));
|
||||
}
|
||||
// postcondition: transfers[id].posted == true
|
||||
if !(self.transfers[&&id].posted == true) {
|
||||
return Err(format!("Postcondition failed: {}", "transfers[id].posted == true"));
|
||||
}
|
||||
// postcondition: accounts[transfers[id].from].debits_posted ==
|
||||
if !(self.accounts[&&self.transfers[&&id].from].debits_posted == self.accounts[&&self.transfers[&&id].from].debits_posted) {
|
||||
return Err(format!("Postcondition failed: {}", "accounts[transfers[id].from].debits_posted =="));
|
||||
}
|
||||
// postcondition: accounts[transfers[id].to].credits_posted ==
|
||||
if !(self.accounts[&&self.transfers[&&id].to].credits_posted == self.accounts[&&self.transfers[&&id].to].credits_posted) {
|
||||
return Err(format!("Postcondition failed: {}", "accounts[transfers[id].to].credits_posted =="));
|
||||
}
|
||||
// postcondition: accounts[transfers[id].from].debits_pending ==
|
||||
if !(self.accounts[&&self.transfers[&&id].from].debits_pending == self.accounts[&&self.transfers[&&id].from].debits_pending) {
|
||||
return Err(format!("Postcondition failed: {}", "accounts[transfers[id].from].debits_pending =="));
|
||||
}
|
||||
// postcondition: accounts[transfers[id].to].credits_pending ==
|
||||
if !(self.accounts[&&self.transfers[&&id].to].credits_pending == self.accounts[&&self.transfers[&&id].to].credits_pending) {
|
||||
return Err(format!("Postcondition failed: {}", "accounts[transfers[id].to].credits_pending =="));
|
||||
}
|
||||
}
|
||||
|
||||
/// Execute action: VoidTransfer
|
||||
pub fn void_transfer(&mut self, id: u64) -> Result<(), String> {
|
||||
// precondition: id in pending
|
||||
if !(self.pending.contains(&id)) {
|
||||
return Err(format!("Precondition failed: {}", "id in pending"));
|
||||
}
|
||||
// precondition: id in transfers.keys
|
||||
if !(self.transfers.contains_key(&id)) {
|
||||
return Err(format!("Precondition failed: {}", "id in transfers.keys"));
|
||||
}
|
||||
// precondition: transfers[id].pending == true
|
||||
if !(self.transfers[&&id].pending == true) {
|
||||
return Err(format!("Precondition failed: {}", "transfers[id].pending == true"));
|
||||
}
|
||||
// postcondition: pending == pending \\ {id}
|
||||
if !(self.pending == {self.pending.clone().into_iter().filter(|x| x != &id).collect()}) {
|
||||
return Err(format!("Postcondition failed: {}", "pending == pending \\\\ {id}"));
|
||||
}
|
||||
// postcondition: transfers[id].pending == false
|
||||
if !(self.transfers[&&id].pending == false) {
|
||||
return Err(format!("Postcondition failed: {}", "transfers[id].pending == false"));
|
||||
}
|
||||
// postcondition: transfers[id].voided == true
|
||||
if !(self.transfers[&&id].voided == true) {
|
||||
return Err(format!("Postcondition failed: {}", "transfers[id].voided == true"));
|
||||
}
|
||||
// postcondition: accounts[transfers[id].from].debits_pending ==
|
||||
if !(self.accounts[&&self.transfers[&&id].from].debits_pending == self.accounts[&&self.transfers[&&id].from].debits_pending) {
|
||||
return Err(format!("Postcondition failed: {}", "accounts[transfers[id].from].debits_pending =="));
|
||||
}
|
||||
// postcondition: accounts[transfers[id].to].credits_pending ==
|
||||
if !(self.accounts[&&self.transfers[&&id].to].credits_pending == self.accounts[&&self.transfers[&&id].to].credits_pending) {
|
||||
return Err(format!("Postcondition failed: {}", "accounts[transfers[id].to].credits_pending =="));
|
||||
}
|
||||
}
|
||||
|
||||
/// Execute action: PostTransfer
|
||||
pub fn post_transfer(&mut self, t: Transfer) -> Result<(), String> {
|
||||
// precondition: t.id notIn transfers.keys
|
||||
if !(!self.transfers.contains_key(&t.id)) {
|
||||
return Err(format!("Precondition failed: {}", "t.id notIn transfers.keys"));
|
||||
}
|
||||
// precondition: t.from in accounts.keys
|
||||
if !(self.accounts.contains_key(&t.from)) {
|
||||
return Err(format!("Precondition failed: {}", "t.from in accounts.keys"));
|
||||
}
|
||||
// precondition: t.to in accounts.keys
|
||||
if !(self.accounts.contains_key(&t.to)) {
|
||||
return Err(format!("Precondition failed: {}", "t.to in accounts.keys"));
|
||||
}
|
||||
// precondition: t.from != t.to
|
||||
if !(t.from != t.to) {
|
||||
return Err(format!("Precondition failed: {}", "t.from != t.to"));
|
||||
}
|
||||
// precondition: accounts[t.from].balance >= t.amount || accounts[t.from].flags.allows_overdraft
|
||||
if !(self.accounts[&&t.from].balance >= t.amount || self.accounts[&&t.from].flags.allows_overdraft) {
|
||||
return Err(format!("Precondition failed: {}", "accounts[t.from].balance >= t.amount || accounts[t.from].flags.allows_overdraft"));
|
||||
}
|
||||
// postcondition: transfers[t.id] == { ...t, pending: false, posted: true, voided: false }
|
||||
if !(self.transfers[&&t.id] == { ...t, self.pending: false, posted: true, voided: false }) {
|
||||
return Err(format!("Postcondition failed: {}", "transfers[t.id] == { ...t, pending: false, posted: true, voided: false }"));
|
||||
}
|
||||
// postcondition: accounts[t.from].debits_posted == old(accounts[t.from].debits_posted) + t.amount
|
||||
if !(self.accounts[&&t.from].debits_posted == self.accounts[&&t.from].debits_posted + t.amount) {
|
||||
return Err(format!("Postcondition failed: {}", "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
|
||||
if !(self.accounts[&&t.to].credits_posted == self.accounts[&&t.to].credits_posted + t.amount) {
|
||||
return Err(format!("Postcondition failed: {}", "accounts[t.to].credits_posted == old(accounts[t.to].credits_posted) + t.amount"));
|
||||
}
|
||||
}
|
||||
|
||||
/// Execute action: BecomeLeader
|
||||
pub fn become_leader(&mut self, replica: u64, term: u64) -> Result<(), String> {
|
||||
// precondition: replica in replicaState.keys
|
||||
if !(self.replica_state.contains_key(&replica)) {
|
||||
return Err(format!("Precondition failed: {}", "replica in replicaState.keys"));
|
||||
}
|
||||
// precondition: replicaState[replica].role == "candidate"
|
||||
if !(self.replica_state[&replica].role == "candidate") {
|
||||
return Err(format!("Precondition failed: {}", "replicaState[replica].role == \"candidate\""));
|
||||
}
|
||||
// precondition: replicaState[replica].currentTerm < term
|
||||
if !(self.replica_state[&replica].currentTerm < term) {
|
||||
return Err(format!("Precondition failed: {}", "replicaState[replica].currentTerm < term"));
|
||||
}
|
||||
// postcondition: leader == replica
|
||||
if !(self.leader == replica) {
|
||||
return Err(format!("Postcondition failed: {}", "leader == replica"));
|
||||
}
|
||||
// postcondition: replicaState[replica].role == "leader"
|
||||
if !(self.replica_state[&replica].role == "self.leader") {
|
||||
return Err(format!("Postcondition failed: {}", "replicaState[replica].role == \"leader\""));
|
||||
}
|
||||
// postcondition: replicaState[replica].currentTerm == term
|
||||
if !(self.replica_state[&replica].currentTerm == term) {
|
||||
return Err(format!("Postcondition failed: {}", "replicaState[replica].currentTerm == term"));
|
||||
}
|
||||
}
|
||||
|
||||
/// Execute action: AppendEntry
|
||||
pub fn append_entry(&mut self, entry: LogEntry, term: u64) -> Result<(), String> {
|
||||
// precondition: entry.index == length(log) + 1
|
||||
if !(entry.index == self.log.len() + 1) {
|
||||
return Err(format!("Precondition failed: {}", "entry.index == length(log) + 1"));
|
||||
}
|
||||
// precondition: term >= commitIndex
|
||||
if !(term >= self.commit_index) {
|
||||
return Err(format!("Precondition failed: {}", "term >= commitIndex"));
|
||||
}
|
||||
// postcondition: log == append(log, entry)
|
||||
if !(self.log == {self.log.push(entry); self.log} /* append */) {
|
||||
return Err(format!("Postcondition failed: {}", "log == append(log, entry)"));
|
||||
}
|
||||
// postcondition: commitIndex == entry.index
|
||||
if !(self.commit_index == entry.index) {
|
||||
return Err(format!("Postcondition failed: {}", "commitIndex == entry.index"));
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
// Temporal verification stubs
|
||||
impl TigerBeetleLedgerMachine {
|
||||
/// V1: Always(AccountBalanceInvariant)
|
||||
pub fn verify_1(&self) -> bool {
|
||||
// TODO: Model-check or monitor
|
||||
// Temporal: Always(AccountBalanceInvariant)
|
||||
true
|
||||
}
|
||||
}
|
||||
|
|
@ -12,7 +12,7 @@
|
|||
"@type": "prov:Generation",
|
||||
"prov:activity": {
|
||||
"@type": "prov:Activity",
|
||||
"prov:startTime": "2026-05-10T06:07:50.697Z"
|
||||
"prov:startTime": "2026-05-10T06:24:31.493Z"
|
||||
}
|
||||
},
|
||||
"rdfs:label": "RetryHandler",
|
||||
|
|
|
|||
|
|
@ -38,7 +38,7 @@
|
|||
"name": "Scott Scoble",
|
||||
"email": "scott@scoble.me"
|
||||
},
|
||||
"timestamp": "2026-05-10T06:07:50.700Z"
|
||||
"timestamp": "2026-05-10T06:24:31.495Z"
|
||||
},
|
||||
{
|
||||
"subject": "speck:RetryHandler",
|
||||
|
|
@ -53,7 +53,7 @@
|
|||
"name": "Speckl Compiler",
|
||||
"email": "compiler@speckl.scoble.me"
|
||||
},
|
||||
"timestamp": "2026-05-10T06:07:50.700Z"
|
||||
"timestamp": "2026-05-10T06:24:31.495Z"
|
||||
},
|
||||
{
|
||||
"subject": "speck:RetryHandler",
|
||||
|
|
@ -68,7 +68,7 @@
|
|||
"name": "Speckl Compiler",
|
||||
"email": "compiler@speckl.scoble.me"
|
||||
},
|
||||
"timestamp": "2026-05-10T06:07:50.700Z"
|
||||
"timestamp": "2026-05-10T06:24:31.495Z"
|
||||
}
|
||||
]
|
||||
}
|
||||
|
|
@ -13,7 +13,7 @@
|
|||
"spdxVersion": "3.0.1",
|
||||
"dataLicense": "CC0-1.0",
|
||||
"creationInfo": {
|
||||
"created": "2026-05-10T06:07:50.702Z",
|
||||
"created": "2026-05-10T06:24:31.496Z",
|
||||
"createdBy": [
|
||||
"Organization: Speckl",
|
||||
"tool: speckl-compile-0.2.0"
|
||||
|
|
@ -27,7 +27,7 @@
|
|||
"@type": "spdx:Tool",
|
||||
"name": "speckl-compile"
|
||||
},
|
||||
"timestamp": "2026-05-10T06:07:50.702Z",
|
||||
"timestamp": "2026-05-10T06:24:31.496Z",
|
||||
"comment": "Review type: manual"
|
||||
}
|
||||
]
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue