diff --git a/README.md b/README.md index 72b9b80..f3b2ebf 100644 --- a/README.md +++ b/README.md @@ -2,7 +2,7 @@ **A judgement transport utility for AI-generated specifications.** Fulfills NIST SA-11 (human-in-the-loop for automated outputs). -Speckl is a specification language (SpeckDL) with a compiler that produces runnable software — WebAssembly, TypeScript, and provenance artifacts (PROV-O, CycloneDX, SPDX) — from a single source of truth. Write what your system should do. Prove it. Ship it. +Speckl is a specification language (SpeckDL) with a compiler that produces runnable software — TypeScript and provenance artifacts (PROV-O, CycloneDX, SPDX) — from a single source of truth. Write what your system should do. Prove it. Ship it. ## The Core Insight @@ -17,8 +17,7 @@ AI generates code at machine speed. Humans own specifications. **SpeckDL is the Speckl is a **working compiler** that turns formal specifications into multiple target representations: ``` -.speckdl spec ──→ Wasm (WebAssembly) ← runnable, verified state machines - ├── TypeScript ← typed, importable classes +.speckdl spec ──→ TypeScript ← typed, importable classes ├── PROV-O (RDF) ← W3C provenance standard ├── CycloneDX SBOM ← OWASP software bill of materials └── SPDX SBOM ← Linux Foundation SBOM standard @@ -46,7 +45,7 @@ spec ToggleSwitch { } ``` -This compiles to a runnable WebAssembly module with verified state transitions + guards, and to a type-safe TypeScript class. Both from the same spec. +This compiles to a runnable TypeScript class with verified state transitions + guards. ### Provenance Embedded at Compile Time @@ -58,12 +57,12 @@ The compiler has been validated against: | Example | Source | Status | |---------|--------|--------| -| **ToggleSwitch** | SpeckDL tutorial | ✅ All 5 artifacts | -| **AccountLedger** | Banking ledger with debit/credit | ✅ All 5 artifacts | -| **TwoPhaseCommit** | TLA+ port | ✅ All 5 artifacts | -| **Paxos** | TLA+ port | ✅ All 5 artifacts | -| **Raft** | TLA+ port | ✅ All 5 artifacts | -| **TigerBeetleLedger** | Naive TigerBeetle core | ✅ All 5 artifacts (3 TS type errors in progress) | +| **ToggleSwitch** | SpeckDL tutorial | ✅ All artifacts | +| **AccountLedger** | Banking ledger with debit/credit | ✅ All artifacts | +| **TwoPhaseCommit** | TLA+ port | ✅ All artifacts | +| **Paxos** | TLA+ port | ✅ All artifacts | +| **Raft** | TLA+ port | ✅ All artifacts | +| **TigerBeetleLedger** | Naive TigerBeetle core | ✅ All artifacts (3 TS type errors in progress) | ## Getting Started @@ -72,10 +71,10 @@ git clone https://os.scoble.me/forgejo/sscoble/speckl cd speckl/compiler npm install -# Compile an example to all 5 targets +# Compile an example node dist/index.js ../examples/ToggleSwitch.speck -o out/switch ls out/switch/ -# ToggleSwitch.wat ToggleSwitch.ts ToggleSwitch.prov-o.jsonld +# ToggleSwitch.ts ToggleSwitch.prov-o.jsonld # ToggleSwitch.cyclonedx.json ToggleSwitch.spdx.json ``` @@ -99,11 +98,10 @@ ls out/switch/ ## Validation Status -- **Compiler:** 41/41 tests passing (WASM + TypeScript codegen) -- **WASM E2E:** wabt assemble + instantiate + run verified -- **TypeScript:** Dual-target compilation — same spec produces both WASM and TS -- **TLA+ Trilogy:** TwoPhaseCommit, Paxos, Raft all compile (WAT validates through wabt) -- **Compiler Self-Spec:** `speckl-compile.speckdl` defines the Speckl compiler in SpeckDL — generates all 5 artifacts (known TypeScript errors tracked in engineering#9) +- **Compiler:** 41/41 tests passing (TypeScript codegen) +- **TypeScript:** Type-safe compilation from specs +- **TLA+ Trilogy:** TwoPhaseCommit, Paxos, Raft all compile +- **Compiler Self-Spec:** `speckl-compile.speckdl` defines the Speckl compiler in SpeckDL — generates all artifacts (known TypeScript errors tracked in engineering#9) ## Known Issues diff --git a/compiler/__tests__/parser.test.ts b/compiler/__tests__/parser.test.ts index 1673982..e16b091 100644 --- a/compiler/__tests__/parser.test.ts +++ b/compiler/__tests__/parser.test.ts @@ -524,6 +524,4 @@ speck Second { } }); }); - - }); diff --git a/compiler/dist/index.js b/compiler/dist/index.js index 724435a..fd84422 100644 --- a/compiler/dist/index.js +++ b/compiler/dist/index.js @@ -6,7 +6,7 @@ import { generateProvenanceGraph } from './generators/provenance.js'; import { generateCycloneDX } from './generators/cyclonedx.js'; import { generateSPDX } from './generators/spdx.js'; import { generateTypeScriptStateMachine } from './generators/typescript-state-machine.js'; -import { generateWASM } from './generators/wasm.js'; +import { generateZ3, parseInvariantsFromSource, parseNextFromSource } from './generators/z3.js'; import fs from 'fs'; import path from 'path'; async function main() { @@ -35,6 +35,19 @@ async function main() { describe: 'Output directory for compiled artifacts', type: 'string', default: './out', + }) + .option('target', { + alias: 't', + describe: 'Compilation target', + type: 'string', + choices: ['typescript', 'z3', 'all'], + default: 'typescript', + }) + .option('verify-depth', { + alias: 'd', + describe: 'Bounded model checking depth for Z3 verification', + type: 'number', + default: 10, }) .option('bom-format', { alias: 'b', @@ -50,6 +63,8 @@ async function main() { const options = { outputDir: argv.outputDir, bomFormat: argv.bomFormat, + target: argv.target, + verifyDepth: argv.verifyDepth, }; console.log(`Compiling ${file}...`); // Parse the Speck file @@ -61,23 +76,40 @@ async function main() { if (!fs.existsSync(options.outputDir)) { fs.mkdirSync(options.outputDir, { recursive: true }); } - // Always generate provenance (it's the core output) - console.log('\nGenerating provenance graph (PROV-O JSON-LD)...'); - generateProvenanceGraph(ast, options.outputDir); - // Generate TypeScript state machine - console.log('\nGenerating TypeScript state machine...'); - generateTypeScriptStateMachine(ast, options.outputDir); - // Generate WASM state machine - console.log('\nGenerating WebAssembly (WAT)...'); - generateWASM(ast, options.outputDir); - // Generate BOM based on format selection - if (options.bomFormat === 'cdx' || options.bomFormat === 'both') { - console.log('\nGenerating CycloneDX BOM...'); - generateCycloneDX(ast, options.outputDir); + // 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') { + console.log('\nGenerating provenance graph (PROV-O JSON-LD)...'); + generateProvenanceGraph(ast, options.outputDir); } - if (options.bomFormat === 'spdx' || options.bomFormat === 'both') { - console.log('\nGenerating SPDX BOM...'); - generateSPDX(ast, options.outputDir); + // Generate Z3 SMT-LIB2 if target is z3 or all + if (options.target === 'z3' || options.target === 'all') { + console.log('\nGenerating Z3 SMT-LIB2...'); + // Parse invariants from raw source for Z3 backend + for (const speck of ast.specks) { + const invariants = parseInvariantsFromSource(rawSource, speck.name); + const nextNode = parseNextFromSource(rawSource, speck.name); + // Attach parsed data to the AST for the generator + speck._invariants = invariants; + speck._next = nextNode; + } + const z3Options = { verifyDepth: options.verifyDepth }; + generateZ3(ast, options.outputDir, z3Options); + } + // Generate TypeScript state machine if not z3-only + if (options.target !== 'z3') { + console.log('\nGenerating TypeScript state machine...'); + generateTypeScriptStateMachine(ast, options.outputDir); + // Generate BOM based on format selection + if (options.bomFormat === 'cdx' || options.bomFormat === 'both') { + console.log('\nGenerating CycloneDX BOM...'); + generateCycloneDX(ast, options.outputDir); + } + if (options.bomFormat === 'spdx' || options.bomFormat === 'both') { + console.log('\nGenerating SPDX BOM...'); + generateSPDX(ast, options.outputDir); + } } console.log(`\nCompilation complete. Output: ${options.outputDir}/`); } diff --git a/compiler/dist/index.js.map b/compiler/dist/index.js.map index c732d56..89612d3 100644 --- a/compiler/dist/index.js.map +++ b/compiler/dist/index.js.map @@ -1 +1 @@ -{"version":3,"file":"index.js","sourceRoot":"","sources":["../src/index.ts"],"names":[],"mappings":";AAEA,OAAO,KAAK,MAAM,OAAO,CAAC;AAC1B,OAAO,EAAE,OAAO,EAAE,MAAM,eAAe,CAAC;AACxC,OAAO,EAAE,cAAc,EAAE,MAAM,aAAa,CAAC;AAC7C,OAAO,EAAE,uBAAuB,EAAE,MAAM,4BAA4B,CAAC;AACrE,OAAO,EAAE,iBAAiB,EAAE,MAAM,2BAA2B,CAAC;AAC9D,OAAO,EAAE,YAAY,EAAE,MAAM,sBAAsB,CAAC;AACpD,OAAO,EAAE,8BAA8B,EAAE,MAAM,0CAA0C,CAAC;AAC1F,OAAO,EAAE,YAAY,EAAE,MAAM,sBAAsB,CAAC;AACpD,OAAO,EAAE,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"} \ No newline at end of file +{"version":3,"file":"index.js","sourceRoot":"","sources":["../src/index.ts"],"names":[],"mappings":";AAEA,OAAO,KAAK,MAAM,OAAO,CAAC;AAC1B,OAAO,EAAE,OAAO,EAAE,MAAM,eAAe,CAAC;AACxC,OAAO,EAAE,cAAc,EAAE,MAAM,aAAa,CAAC;AAC7C,OAAO,EAAE,uBAAuB,EAAE,MAAM,4BAA4B,CAAC;AACrE,OAAO,EAAE,iBAAiB,EAAE,MAAM,2BAA2B,CAAC;AAC9D,OAAO,EAAE,YAAY,EAAE,MAAM,sBAAsB,CAAC;AACpD,OAAO,EAAE,8BAA8B,EAAE,MAAM,0CAA0C,CAAC;AAC1F,OAAO,EAAE,UAAU,EAAa,yBAAyB,EAAE,mBAAmB,EAAE,MAAM,oBAAoB,CAAC;AAC3G,OAAO,EAAE,MAAM,IAAI,CAAC;AACpB,OAAO,IAAI,MAAM,MAAM,CAAC;AASxB,KAAK,UAAU,IAAI;IACjB,uDAAuD;IACvD,MAAM,WAAW,GAAG,IAAI,CAAC,IAAI,CAAC,IAAI,CAAC,OAAO,CAAC,IAAI,GAAG,CAAC,MAAM,CAAC,IAAI,CAAC,GAAG,CAAC,CAAC,QAAQ,CAAC,EAAE,IAAI,EAAE,eAAe,CAAC,CAAC;IACtG,IAAI,EAAE,CAAC,UAAU,CAAC,WAAW,CAAC,EAAE,CAAC;QAC/B,IAAI,CAAC;YACH,MAAM,EAAE,QAAQ,EAAE,GAAG,MAAM,MAAM,CAAC,eAAe,CAAC,CAAC;YACnD,QAAQ,CAAC,SAAS,WAAW,GAAG,EAAE,EAAE,KAAK,EAAE,SAAS,EAAE,CAAC,CAAC;QAC1D,CAAC;QAAC,MAAM,CAAC;YACP,OAAO,CAAC,KAAK,CAAC,oDAAoD,CAAC,CAAC;YACpE,OAAO,CAAC,IAAI,CAAC,CAAC,CAAC,CAAC;QAClB,CAAC;IACH,CAAC;IAED,MAAM,IAAI,GAAG,MAAM,KAAK,CAAC,OAAO,CAAC,OAAO,CAAC,IAAI,CAAC,CAAC;SAC5C,OAAO,CAAC,WAAW,EAAE,iCAAiC,EAAE,CAAC,QAAQ,EAAE,EAAE;QACpE,OAAO,QAAQ;aACZ,UAAU,CAAC,MAAM,EAAE;YAClB,QAAQ,EAAE,yBAAyB;YACnC,IAAI,EAAE,QAAQ;YACd,YAAY,EAAE,IAAI;SACnB,CAAC;aACD,MAAM,CAAC,YAAY,EAAE;YACpB,KAAK,EAAE,GAAG;YACV,QAAQ,EAAE,yCAAyC;YACnD,IAAI,EAAE,QAAQ;YACd,OAAO,EAAE,OAAO;SACjB,CAAC;aACD,MAAM,CAAC,QAAQ,EAAE;YAChB,KAAK,EAAE,GAAG;YACV,QAAQ,EAAE,oBAAoB;YAC9B,IAAI,EAAE,QAAQ;YACd,OAAO,EAAE,CAAC,YAAY,EAAE,IAAI,EAAE,KAAK,CAAC;YACpC,OAAO,EAAE,YAAqB;SAC/B,CAAC;aACD,MAAM,CAAC,cAAc,EAAE;YACtB,KAAK,EAAE,GAAG;YACV,QAAQ,EAAE,kDAAkD;YAC5D,IAAI,EAAE,QAAQ;YACd,OAAO,EAAE,EAAE;SACZ,CAAC;aACD,MAAM,CAAC,YAAY,EAAE;YACpB,KAAK,EAAE,GAAG;YACV,QAAQ,EAAE,mBAAmB;YAC7B,IAAI,EAAE,QAAQ;YACd,OAAO,EAAE,CAAC,KAAK,EAAE,MAAM,EAAE,MAAM,CAAC;YAChC,OAAO,EAAE,MAAe;SACzB,CAAC,CAAC;IACP,CAAC,CAAC;SACD,IAAI,EAAE;SACN,IAAI,CAAC;IAER,MAAM,IAAI,GAAG,IAAI,CAAC,IAAc,CAAC;IACjC,MAAM,OAAO,GAAG;QACd,SAAS,EAAE,IAAI,CAAC,SAAmB;QACnC,SAAS,EAAE,IAAI,CAAC,SAAoC;QACpD,MAAM,EAAE,IAAI,CAAC,MAAqC;QAClD,WAAW,EAAE,IAAI,CAAC,WAAqB;KACxC,CAAC;IAEF,OAAO,CAAC,GAAG,CAAC,aAAa,IAAI,KAAK,CAAC,CAAC;IAEpC,uBAAuB;IACvB,MAAM,GAAG,GAAG,cAAc,CAAC,IAAI,CAAC,CAAC;IAEjC,MAAM,UAAU,GAAG,GAAG,CAAC,MAAM,CAAC,MAAM,CAAC;IACrC,MAAM,WAAW,GAAG,GAAG,CAAC,MAAM,CAAC,MAAM,CAAC,CAAC,GAAG,EAAE,CAAC,EAAE,EAAE,CAAC,GAAG,GAAG,CAAC,CAAC,OAAO,CAAC,MAAM,EAAE,CAAC,CAAC,CAAC;IAC7E,OAAO,CAAC,GAAG,CAAC,4BAA4B,UAAU,cAAc,WAAW,YAAY,CAAC,CAAC;IAEzF,iCAAiC;IACjC,IAAI,CAAC,EAAE,CAAC,UAAU,CAAC,OAAO,CAAC,SAAS,CAAC,EAAE,CAAC;QACtC,EAAE,CAAC,SAAS,CAAC,OAAO,CAAC,SAAS,EAAE,EAAE,SAAS,EAAE,IAAI,EAAE,CAAC,CAAC;IACvD,CAAC;IAED,oFAAoF;IACpF,MAAM,SAAS,GAAG,EAAE,CAAC,YAAY,CAAC,IAAI,EAAE,OAAO,CAAC,CAAC;IAEjD,mEAAmE;IACnE,IAAI,OAAO,CAAC,MAAM,KAAK,IAAI,EAAE,CAAC;QAC5B,OAAO,CAAC,GAAG,CAAC,mDAAmD,CAAC,CAAC;QACjE,uBAAuB,CAAC,GAAG,EAAE,OAAO,CAAC,SAAS,CAAC,CAAC;IAClD,CAAC;IAED,8CAA8C;IAC9C,IAAI,OAAO,CAAC,MAAM,KAAK,IAAI,IAAI,OAAO,CAAC,MAAM,KAAK,KAAK,EAAE,CAAC;QACxD,OAAO,CAAC,GAAG,CAAC,6BAA6B,CAAC,CAAC;QAC3C,kDAAkD;QAClD,KAAK,MAAM,KAAK,IAAI,GAAG,CAAC,MAAM,EAAE,CAAC;YAC/B,MAAM,UAAU,GAAG,yBAAyB,CAAC,SAAS,EAAE,KAAK,CAAC,IAAI,CAAC,CAAC;YACpE,MAAM,QAAQ,GAAG,mBAAmB,CAAC,SAAS,EAAE,KAAK,CAAC,IAAI,CAAC,CAAC;YAC5D,kDAAkD;YACjD,KAAa,CAAC,WAAW,GAAG,UAAU,CAAC;YACvC,KAAa,CAAC,KAAK,GAAG,QAAQ,CAAC;QAClC,CAAC;QACD,MAAM,SAAS,GAAc,EAAE,WAAW,EAAE,OAAO,CAAC,WAAW,EAAE,CAAC;QAClE,UAAU,CAAC,GAAG,EAAE,OAAO,CAAC,SAAS,EAAE,SAAS,CAAC,CAAC;IAChD,CAAC;IAED,mDAAmD;IACnD,IAAI,OAAO,CAAC,MAAM,KAAK,IAAI,EAAE,CAAC;QAC5B,OAAO,CAAC,GAAG,CAAC,0CAA0C,CAAC,CAAC;QACxD,8BAA8B,CAAC,GAAG,EAAE,OAAO,CAAC,SAAS,CAAC,CAAC;QAEvD,yCAAyC;QACzC,IAAI,OAAO,CAAC,SAAS,KAAK,KAAK,IAAI,OAAO,CAAC,SAAS,KAAK,MAAM,EAAE,CAAC;YAChE,OAAO,CAAC,GAAG,CAAC,+BAA+B,CAAC,CAAC;YAC7C,iBAAiB,CAAC,GAAG,EAAE,OAAO,CAAC,SAAS,CAAC,CAAC;QAC5C,CAAC;QAED,IAAI,OAAO,CAAC,SAAS,KAAK,MAAM,IAAI,OAAO,CAAC,SAAS,KAAK,MAAM,EAAE,CAAC;YACjE,OAAO,CAAC,GAAG,CAAC,0BAA0B,CAAC,CAAC;YACxC,YAAY,CAAC,GAAG,EAAE,OAAO,CAAC,SAAS,CAAC,CAAC;QACvC,CAAC;IACH,CAAC;IAED,OAAO,CAAC,GAAG,CAAC,mCAAmC,OAAO,CAAC,SAAS,GAAG,CAAC,CAAC;AACvE,CAAC;AAED,IAAI,EAAE,CAAC,KAAK,CAAC,CAAC,GAAG,EAAE,EAAE;IACnB,OAAO,CAAC,KAAK,CAAC,qBAAqB,EAAE,GAAG,CAAC,CAAC;IAC1C,OAAO,CAAC,IAAI,CAAC,CAAC,CAAC,CAAC;AAClB,CAAC,CAAC,CAAC"} \ No newline at end of file diff --git a/compiler/node_modules/.vite/vitest/results.json b/compiler/node_modules/.vite/vitest/results.json index a12343a..691508c 100644 --- a/compiler/node_modules/.vite/vitest/results.json +++ b/compiler/node_modules/.vite/vitest/results.json @@ -1 +1 @@ -{"version":"2.1.9","results":[[":__tests__/parser.test.ts",{"duration":39.401257999999984,"failed":false}],[":__tests__/e2e-wasm.test.ts",{"duration":108.43775999999997,"failed":false}],[":src/__tests__/compiler.test.ts",{"duration":11.341655000000003,"failed":false}]]} \ No newline at end of file +{"version":"2.1.9","results":[[":__tests__/parser.test.ts",{"duration":33.913234999999986,"failed":false}],[":src/__tests__/compiler.test.ts",{"duration":11.873544000000038,"failed":false}]]} \ No newline at end of file diff --git a/compiler/src/generators/z3.ts b/compiler/src/generators/z3.ts new file mode 100644 index 0000000..44e045a --- /dev/null +++ b/compiler/src/generators/z3.ts @@ -0,0 +1,1089 @@ +import { + AST, SpeckNode, MemberNode, StateNode, InitNode, ActionNode, + ConstraintNode, VerifyNode, TypeExpr, StateVar, ActionStatement +} from '../parser.js'; +import fs from 'fs'; +import path from 'path'; + +/** + * Z3 SMT-LIB2 backend for SpeckDL. + * + * Translates SpeckDL invariants, state machines, and verify blocks + * into SMT-LIB2 for bounded model checking with Z3. + * + * Architecture: + * - State variables → Z3 sort declarations and const declarations + * - invariants → Z3 define-fun returning Bool + * - Actions → Z3 define-fun transition predicates (pre → post) + * - verify blocks → BMC unrolling with N copies of state + */ + +export interface Z3Options { + verifyDepth: number; +} + +const DEFAULT_OPTIONS: Z3Options = { + verifyDepth: 10, +}; + +/** + * InvariantNode — parsed invariant block + * Parsed directly in the generator from raw block content + * since the AST parser doesn't yet parse invariants. + */ +export interface InvariantNode { + type: 'invariant'; + name: string; + statements: InvariantStatement[]; +} + +export type InvariantStatement = + | { type: 'require'; expr: string } + | { type: 'forall'; var: string; domain: string; expr: string } + | { type: 'forall_complex'; vars: string[]; domains: string[]; expr: string }; + +export interface NextNode { + type: 'next'; + actions: string[]; // action names separated by | +} + +/** + * Generate Z3 SMT-LIB2 from a SpeckDL AST. + */ +export function generateZ3(ast: AST, outputDir: string, options: Z3Options = DEFAULT_OPTIONS): void { + for (const speck of ast.specks) { + const code = emitZ3(speck, options); + const filename = `${speck.name}.smt2`; + const filepath = path.join(outputDir, filename); + fs.writeFileSync(filepath, code); + console.log(`Generated Z3 SMT-LIB2: ${filepath}`); + } +} + +function emitZ3(speck: SpeckNode, options: Z3Options): string { + const members = speck.members; + + 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 constraints = members.filter(m => m.type === 'constraint') as ConstraintNode[]; + const verifies = members.filter(m => m.type === 'verify') as VerifyNode[]; + + // Parse invariants from the raw speck body + const invariants = (speck as any)._invariants || parseInvariants(speck); + // Parse next: transition relation + const nextNode = (speck as any)._next || parseNext(speck); + + const lines: string[] = []; + + // Header + lines.push(`; SpeckDL: ${speck.name} — Z3 Verification`); + lines.push(`; Generated by speckl-compile Z3 backend`); + lines.push(`; Bounded model checking depth: ${options.verifyDepth}`); + lines.push(''); + lines.push('(set-logic ALL)'); + lines.push('(set-option :produce-models true)'); + + // Step 1: Declare sorts for record types + const recordTypes = collectRecordTypes(stateNode, actions); + for (const [name, fields] of recordTypes) { + emitRecordSort(lines, name, fields); + } + + // Step 2: Declare state variables as constants + lines.push(''); + lines.push('; --- State Variables ---'); + const stateVars = stateNode?.variables ?? []; + const allTypeRefs: string[] = []; + + for (const v of stateVars) { + emitStateVar(lines, v, allTypeRefs); + } + + // Step 3: Emit invariants as define-fun + if (invariants.length > 0) { + lines.push(''); + lines.push('; --- Invariants ---'); + for (const inv of invariants) { + emitInvariant(lines, inv, stateVars); + } + } + + // Step 4: Emit constraints as assertions + if (constraints.length > 0) { + lines.push(''); + lines.push('; --- Constraints ---'); + for (let i = 0; i < constraints.length; i++) { + const c = constraints[i]; + const z3Expr = translateExpr(c.expr, stateVars, /* suffix */ ''); + lines.push(`; C${i + 1}: ${c.expr}`); + lines.push(`(assert ${z3Expr})`); + } + } + + // Step 5: Emit action transition predicates (only for BMC with verify blocks) + if (verifies.length > 0 && actions.length > 0) { + lines.push(''); + lines.push('; --- Action Transition Predicates ---'); + for (const action of actions) { + emitActionTransition(lines, action, stateVars); + } + + // Step 6: Emit transition relation (next: A | B | C ...) + if (nextNode && nextNode.actions.length > 0) { + emitNextTransition(lines, speck.name, nextNode, actions, stateVars); + } + } + + // Step 7: Emit bounded model checking for verify blocks + if (verifies.length > 0 && actions.length > 0) { + lines.push(''); + lines.push('; --- Bounded Model Checking ---'); + for (const v of verifies) { + emitBMC(lines, speck.name, v, invariants, actions, nextNode, stateVars, options); + } + } + + // Step 8: Check-sat and get-model (for simple assertions) + if (verifies.length === 0) { + lines.push(''); + lines.push('(check-sat)'); + lines.push('(get-model)'); + } + + return lines.join('\n') + '\n'; +} + +// --- Type / sort helpers --- + +function collectRecordTypes(stateNode: StateNode | undefined, actions: ActionNode[]): Map> { + const records = new Map>(); + + // Collect from state variables + if (stateNode) { + for (const v of stateNode.variables) { + collectRecordTypeRefs(v.typeExpr, records); + } + } + + // Collect from action params + for (const a of actions) { + for (const p of a.params) { + collectRecordTypeRefs(p.type, records); + } + } + + return records; +} + +function collectRecordTypeRefs(t: TypeExpr, records: Map>): void { + if (t.type === 'record' && t.fields) { + // Use the record structure — assign a name based on fields for uniqueness + const key = recordTypeKey(t); + if (!records.has(key)) { + const fields = new Map(); + for (const f of t.fields) { + fields.set(f.name, z3Sort(f.type)); + } + records.set(key, fields); + } + } else if (t.type === 'map') { + if (t.keyType) collectRecordTypeRefs(t.keyType, records); + if (t.valueType) collectRecordTypeRefs(t.valueType, records); + } else if (t.type === 'set' || t.type === 'list') { + if (t.elementType) collectRecordTypeRefs(t.elementType, records); + } else if (t.type === 'ident') { + // For named record types (like Account, Transfer, etc.), we declare them as opaque sorts + const name = t.name || 'Unknown'; + if (!isPrimitive(name) && !isBuiltinType(name)) { + const key = `ident:${name}`; + if (!records.has(key)) { + records.set(key, new Map()); // empty = opaque sort + } + } + } +} + +function recordTypeKey(t: TypeExpr): string { + if (t.type === 'ident' && t.name) { + return `ident:${t.name}`; + } + if (t.fields) { + const fields = t.fields.map(f => `${f.name}:${z3Sort(f.type)}`).sort().join(','); + return `record:${fields}`; + } + return 'record:unknown'; +} + +function isPrimitive(name: string): boolean { + return ['Nat', 'Int', 'Real', 'Bool', 'String', 'Bytes'].includes(name); +} + +function isBuiltinType(name: string): boolean { + return ['List', 'Set', 'Map', 'Array'].some(t => name.startsWith(t)); +} + +function z3Sort(t: TypeExpr): string { + if (!t) return 'Int'; + + if (t.type === 'primitive') { + switch (t.name) { + case 'Nat': return 'Int'; + case 'Int': return 'Int'; + case 'Real': return 'Real'; + case 'Bool': return 'Bool'; + case 'String': return 'String'; + case 'Bytes': return 'String'; // Bytes as String for simplicity + default: return 'Int'; + } + } + + if (t.type === 'list') { + // Lists are modeled as Arrays from Int index to element type + const elemSort = z3Sort(t.elementType!); + return `(Array Int ${elemSort})`; + } + + if (t.type === 'set') { + // Sets are modeled as (Array T Bool) — membership is select + const elemSort = z3Sort(t.elementType!); + return `(Array ${elemSort} Bool)`; + } + + if (t.type === 'map') { + const keySort = z3Sort(t.keyType!); + const valSort = z3Sort(t.valueType!); + return `(Array ${keySort} ${valSort})`; + } + + if (t.type === 'record') { + return recordSortName(t); + } + + if (t.type === 'ident' && t.name) { + // Strip ident: prefix, remove Z3-invalid chars, return clean sort name + let clean = t.name.startsWith('ident:') ? t.name.substring(6) : t.name; + // Remove parenthesized parameters: Option(NodeId) → Option_NodeId + clean = clean.replace(/\(([^)]+)\)/g, '_$1').replace(/[<>,\s]+/g, '_').replace(/__+/g, '_'); + return clean; // Named sort (declared as opaque) + } + + return 'Int'; +} + +function recordSortName(t: TypeExpr): string { + if (t.type === 'ident' && t.name) return t.name; + if (t.fields) { + const key = t.fields.map(f => `${f.name}_${z3Sort(f.type)}`).join('_'); + return `Record${simpleHash(key)}`; + } + return 'Unknown'; +} + +function simpleHash(s: string): string { + let hash = 0; + for (let i = 0; i < s.length; i++) { + hash = ((hash << 5) - hash) + s.charCodeAt(i); + hash |= 0; + } + return Math.abs(hash).toString(16); +} + +function emitRecordSort(lines: string[], name: string, fields: Map): void { + // Sanitize: strip ident: prefix and remove Z3-invalid characters + let cleanName = name.startsWith('ident:') ? name.substring(6) : name; + cleanName = cleanName.replace(/\(([^)]+)\)/g, '_$1').replace(/[<>,\s]+/g, '_').replace(/__+/g, '_'); + + if (fields.size === 0) { + // Opaque sort (for named types like Account, Transfer) + lines.push(`(declare-sort ${cleanName} 0)`); + return; + } + + // Declare as a datatype + lines.push(`(declare-datatypes (( ${cleanName} 0)) ((`); + lines.push(` (mk-${cleanName}`); + + for (const [field, sort] of fields) { + lines.push(` (${field} ${sort})`); + } + lines.push(' )'); + lines.push(')))'); +} + +// --- State variable emission --- + +function emitStateVar(lines: string[], v: StateVar, _allTypeRefs: string[]): void { + const sort = z3Sort(v.typeExpr); + const comment = v.defaultInit ? ` ; default: ${v.defaultInit}` : ''; + lines.push(`(declare-const ${v.name} ${sort})${comment}`); +} + +// --- Invariant emission --- + +function emitInvariant(lines: string[], inv: InvariantNode, stateVars: StateVar[]): void { + lines.push(`(define-fun ${inv.name} () Bool`); + lines.push(' (and'); + + for (const stmt of inv.statements) { + if (stmt.type === 'require') { + const z3Expr = translateExpr(stmt.expr, stateVars, ''); + lines.push(` ${z3Expr}`); + } else if (stmt.type === 'forall') { + // forall var in domain: expr + const domainSort = inferDomainSort(stmt.domain, stateVars); + const z3Expr = translateExpr(stmt.expr, stateVars, ''); + // Replace the bound variable references + const boundExpr = z3Expr; // var already appears in expr text + lines.push(` (forall ((${stmt.var} ${domainSort})) ${boundExpr})`); + } else if (stmt.type === 'forall_complex') { + // forall var1, var2, ... in domain1, domain2: expr + const bindings = stmt.vars.map((v, i) => { + const sort = inferDomainSort(stmt.domains[i], stateVars); + return `(${v} ${sort})`; + }).join(' '); + const z3Expr = translateExpr(stmt.expr, stateVars, ''); + lines.push(` (forall (${bindings}) ${z3Expr})`); + } + } + + lines.push(' )'); + lines.push(')'); +} + +function inferDomainSort(domain: string, stateVars: StateVar[]): string { + // domain might be "accounts.values" or "transfers.keys" or "pending" + // Match against state variables to infer sort + const baseVar = domain.split('.')[0]; + const sv = stateVars.find(v => v.name === baseVar); + if (sv) { + if (domain.endsWith('.values') && sv.typeExpr.type === 'map') { + return z3Sort(sv.typeExpr.valueType!); + } + if (domain.endsWith('.keys') && sv.typeExpr.type === 'map') { + return z3Sort(sv.typeExpr.keyType!); + } + if (sv.typeExpr.type === 'set') { + return z3Sort(sv.typeExpr.elementType!); + } + } + return 'Int'; // fallback +} + +// --- Expression translation --- + +function translateExpr(expr: string, stateVars: StateVar[], suffix: string): string { + if (!expr) return 'true'; + let e = expr.trim(); + + const stateVarNames = new Set(stateVars.map(v => v.name)); + const reservedWords = new Set([ + 'and', 'or', 'not', 'forall', 'exists', 'implies', 'iff', + 'true', 'false', 'in', 'union', 'distinct', + 'now', 'len', 'join', 'old', 'Not', 'Select', 'Set', 'Map', + 'emptySet', 'emptyMap', 'mapKeys', 'values', 'keys', + 'let', 'if', 'then', 'else', 'return', 'require', 'precondition', 'postcondition' + ]); + + // Protect string literals + const strings: string[] = []; + e = e.replace(/"[^"]*"/g, (m) => { + strings.push(m); + return `__STR_${strings.length - 1}__`; + }); + + // Handle old() wrapper — spec-level, keep inner + e = e.replace(/old\(([^()]*(?:\([^()]*\)[^()]*)*)\)/g, '$1'); + + // Handle -> as implication (after field access cleanup to avoid false matches) + e = e.replace(/->/g, '=>'); + + // Handle implies(x, y) function call pattern + e = e.replace(/implies\s*\(([^,)]+),\s*([^)]+)\)/g, '(=> $1 $2)'); + + // Field access: a.balance → balance (drop qualifier for bound forall vars) + // For record fields accessed via dot, translate to Z3-safe names + e = e.replace(/(\w+)\.([\w_]+)/g, (_, obj, field) => { + // If the object is a state variable (map), .field is an accessor we can't resolve + // For bound forall variables, just use the field name + if (stateVarNames.has(obj)) { + // Accessing field on opaque sort — use a compound name + return `${obj}_${field}`; + } + // For bound variables in forall, just emit the field + return `${obj}_${field}`; + }); + + // Handle notIn BEFORE general patterns + e = e.replace(/(\S+)\s+notIn\s+(\S+)\.keys/g, '(not (select $2 $1))'); + + // Handle x in {val1, val2} BEFORE general 'in' pattern + e = e.replace(/(\S+)\s+in\s+\{([^}]+)\}/g, (_, x, values) => { + const vals = values.split(',').map((v: string) => v.trim()); + if (vals.length <= 1) return `(= ${x} ${vals[0] || 'true'})`; + const clauses = vals.map((v: string) => `(= ${x} ${v})`).join(' '); + return `(or ${clauses})`; + }); + + // Handle set union + e = e.replace(/(\S+)\s+union\s+\{([^}]+)\}/g, '(store $1 $2 true)'); + + // Handle set difference + e = e.replace(/(\S+)\s+\\\\\s+\{([^}]+)\}/g, '(store $1 $2 false)'); + + // Map access: v[key] -> (select v key) + e = e.replace(/(\w+)\[([^\]]+)\]/g, (_, base, key) => { + const suffixed = suffix && stateVarNames.has(base) ? `${base}${suffix}` : base; + return `(select ${suffixed} ${key.trim()})`; + }); + + // Handle 'not expr' guard — wrap: not isOn -> (not isOn) + // Only if expr starts with 'not ' and rest is a simple identifier + if (/^not\s+(\w+)\s*$/.test(e)) { + const rest = e.substring(4).trim(); + const restZ3 = suffix && stateVarNames.has(rest) ? `${rest}${suffix}` : rest; + // Restore strings + return restoreStrings(`(not ${restZ3})`, strings); + } + + // Add suffix to state variable references + if (suffix) { + e = e.replace(/\b([a-zA-Z_]\w*)\b/g, (match, id) => { + if (stateVarNames.has(id) && !reservedWords.has(id) && !id.startsWith('__')) { + return `${id}${suffix}`; + } + return match; + }); + } + + // Handle 'in' for set membership (but not already wrapped) + if (!e.includes('(select ') && !e.includes('(or ')) { + e = e.replace(/(\S+)\s+in\s+(\S+)/g, (match, x, set) => { + if (reservedWords.has(set) || set.startsWith('__')) return match; + return `(select ${set} ${x})`; + }); + } + + // Replace operators with placeholder tokens to avoid regex conflicts + e = e.replace(/===/g, '__EQ__'); + e = e.replace(/==/g, '__EQ__'); + e = e.replace(/!=/g, '__NE__'); + e = e.replace(/>=/g, '__GE__'); + e = e.replace(/<=/g, '__LE__'); + + // Replace && and || with and/or for SMT-LIB2 + e = e.replace(/&&/g, 'and'); + e = e.replace(/\|\|/g, 'or'); + + // Convert infix to prefix + e = convertToPrefix(e); + + // Restore operators to SMT-LIB2 + e = e.replace(/__EQ__/g, '='); + e = e.replace(/__NE__/g, 'distinct'); + e = e.replace(/__GE__/g, '>='); + e = e.replace(/__LE__/g, '<='); + + // Wrap distinct + e = e.replace(/\bdistinct\s+(\S+)\s+(\S+)/g, '(distinct $1 $2)'); + + // Restore strings + e = restoreStrings(e, strings); + + return e; +} + +function restoreStrings(expr: string, strings: string[]): string { + return expr.replace(/__STR_(\d+)__/g, (_, i) => strings[parseInt(i)]); +} + +/** + * Convert infix expression to SMT-LIB2 prefix notation. + * Handles operators: =>, and, or, =, <, >, <=, >=, +, - + */ +function convertToPrefix(expr: string): string { + expr = convertOp(expr, '=>', '=>'); + expr = convertOp(expr, 'and', 'and'); + expr = convertOp(expr, 'or', 'or'); + expr = convertOp(expr, '=', '='); + expr = convertOp(expr, '>', '>'); + expr = convertOp(expr, '<', '<'); + expr = convertOp(expr, '>=', '>='); + expr = convertOp(expr, '<=', '<='); + expr = convertOp(expr, '+', '+'); + expr = convertOp(expr, '-', '-'); + return expr; +} + +function convertOp(expr: string, op: string, smtOp: string): string { + // Find top-level operator occurrence (outside any parens) + let depth = 0; + for (let i = 0; i < expr.length; i++) { + if (expr[i] === '(') depth++; + else if (expr[i] === ')') depth--; + else if (depth === 0 && expr.substring(i, i + op.length) === op) { + const beforeOk = i === 0 || /\s/.test(expr[i - 1]) || expr[i - 1] === '('; + const afterOk = i + op.length >= expr.length || /\s/.test(expr[i + op.length]) || expr[i + op.length] === ')'; + if (beforeOk && afterOk) { + const left = expr.substring(0, i).trim(); + const right = expr.substring(i + op.length).trim(); + return `(${smtOp} ${convertToPrefix(left)} ${convertToPrefix(right)})`; + } + } + } + // Already in prefix form + return expr; +} + +// --- Action transition predicate emission --- + +function emitActionTransition(lines: string[], action: ActionNode, stateVars: StateVar[]): void { + const funName = `${action.name}Enabled`; + const nextName = `${action.name}Step`; + + // Collect preconditions and requires + const guards: string[] = []; + const assigns: { target: string; expr: string }[] = []; + + for (const s of action.statements) { + if (s.type === 'precondition' || s.type === 'require') { + guards.push(s.expr); + } else if (s.type === 'assign') { + assigns.push({ target: s.target, expr: s.expr }); + } + } + + // Enablement predicate: all guards hold + if (guards.length > 0) { + lines.push(`(define-fun ${funName} () Bool`); + lines.push(' (and'); + for (const g of guards) { + const z3Expr = translateExpr(g, stateVars, ''); + lines.push(` ${z3Expr}`); + } + lines.push(' )'); + lines.push(')'); + } + + // Step predicate: relates pre- and post-state + if (assigns.length > 0) { + lines.push(`(define-fun ${nextName} () Bool`); + lines.push(' (and'); + for (const a of assigns) { + // a.target becomes post-state, RHS reads pre-state + // Target: if it's a simple name, post-state; if indexed, translate + const z3RHS = translateExpr(a.expr, stateVars, ''); + if (a.target.includes('[')) { + const z3Target = translateExpr(a.target, stateVars, "_post"); + lines.push(` (= ${z3Target} ${z3RHS})`); + } else { + lines.push(` (= ${a.target}_post ${z3RHS})`); + } + } + lines.push(' )'); + lines.push(')'); + } +} + +// --- Next transition relation --- + +function emitNextTransition( + lines: string[], + speckName: string, + nextNode: NextNode, + actions: ActionNode[], + stateVars: StateVar[] +): void { + const actionNames = new Set(actions.map(a => a.name)); + const validActions = nextNode.actions.filter(a => actionNames.has(a)); + + if (validActions.length === 0) return; + + lines.push(`; Next transition relation: ${validActions.join(' | ')}`); + lines.push(`(define-fun Next () Bool`); + lines.push(' (or'); + + for (const aName of validActions) { + const action = actions.find(a => a.name === aName); + if (action) { + const enabled = `${aName}Enabled`; + const step = `${aName}Step`; + + // Check if enabled and step predicates exist + const hasEnabled = action.statements.some(s => s.type === 'precondition' || s.type === 'require'); + const hasStep = action.statements.some(s => s.type === 'assign'); + + if (hasEnabled && hasStep) { + lines.push(` (and (${enabled}) (${step}))`); + } else if (hasEnabled) { + lines.push(` (and (${enabled})`); + lines.push(' (and'); + for (const v of stateVars) { + lines.push(` (= ${v.name}_post ${v.name})`); + } + lines.push(' )'); + lines.push(' )'); + } else if (hasStep) { + lines.push(` (${step})`); + } + } + } + + // Stuttering step: nothing changes + lines.push(' ; Stuttering step'); + lines.push(' (and'); + for (const v of stateVars) { + lines.push(` (= ${v.name}_post ${v.name})`); + } + lines.push(' )'); + + lines.push(' )'); + lines.push(')'); +} + +// --- Bounded Model Checking --- + +function emitBMC( + lines: string[], + speckName: string, + verify: VerifyNode, + invariants: InvariantNode[], + actions: ActionNode[], + nextNode: NextNode | null, + stateVars: StateVar[], + options: Z3Options +): void { + const depth = options.verifyDepth; + const temporalExpr = verify.temporalExpr; + + lines.push(`; Verification: ${temporalExpr}`); + lines.push(`; BMC depth: ${depth}`); + + // Parse the temporal property + const isAlways = temporalExpr.startsWith('Always(') || temporalExpr.startsWith('always('); + const isEventually = temporalExpr.startsWith('Eventually(') || temporalExpr.startsWith('eventually('); + const invariantName = extractInvariantName(temporalExpr); + + // Declare state variables at each step + lines.push(''); + lines.push(`; Declare state copies for ${depth} steps`); + for (const v of stateVars) { + for (let i = 0; i <= depth; i++) { + const sort = z3Sort(v.typeExpr); + lines.push(`(declare-const ${v.name}_${i} ${sort})`); + } + } + + // Init state constraints (from spec init block) + lines.push(''); + lines.push('; Initial state constraints'); + lines.push('(assert'); + lines.push(' (and'); + + // Apply init assignments + const stateNode = stateVars.length > 0 ? { type: 'state' as const, variables: stateVars } : null; + // We need the init block + const initMembers = speckName.length > 0 ? undefined : undefined; + + // Default init: use defaultInit from state vars + for (const v of stateVars) { + if (v.defaultInit) { + const z3Val = translateInitValue(v.defaultInit, v.typeExpr); + lines.push(` (= ${v.name}_0 ${z3Val})`); + } else { + // Default: 0 for Nat/Int, false for Bool, "" for String + if (v.typeExpr.type === 'primitive') { + switch (v.typeExpr.name) { + case 'Nat': case 'Int': lines.push(` (>= ${v.name}_0 0)`); break; + case 'Bool': lines.push(` (or (= ${v.name}_0 true) (= ${v.name}_0 false))`); break; + default: break; // unconstrained + } + } + } + } + + lines.push(' )'); + lines.push(')'); + + // Transition constraints for each step + lines.push(''); + lines.push('; Transition constraints'); + for (let i = 0; i < depth; i++) { + const actionNames = nextNode?.actions ?? []; + const validActions = actionNames.filter(a => actions.some(act => act.name === a)); + + lines.push(`(assert ; Step ${i} → ${i + 1}`); + lines.push(' (or'); + + for (const aName of validActions) { + const action = actions.find(a => a.name === aName); + if (!action) continue; + + const guards: string[] = []; + const stepAssigns: string[] = []; + + for (const s of action.statements) { + if (s.type === 'precondition' || s.type === 'require') { + guards.push(s.expr); + } else if (s.type === 'assign') { + if (s.target.includes('[')) { + const z3LHS = translateExpr(s.target, stateVars, `_${i + 1}`); + const z3RHS = translateExpr(s.expr, stateVars, `_${i}`); + stepAssigns.push(`(= ${z3LHS} ${z3RHS})`); + } else { + const z3RHS = translateExpr(s.expr, stateVars, `_${i}`); + stepAssigns.push(`(= ${s.target}_${i + 1} ${z3RHS})`); + } + } + } + + if (guards.length > 0 || stepAssigns.length > 0) { + lines.push(` (and ; Action: ${aName}`); + + // Guards at step i + for (const g of guards) { + const z3Expr = translateExpr(g, stateVars, `_${i}`); + lines.push(` ${z3Expr}`); + } + + // Step assignments + for (const a of stepAssigns) { + lines.push(` ${a}`); + } + + // Frame: unchanged vars + const changedVars = new Set(action.statements + .filter(s => s.type === 'assign') + .map(s => s.target.replace(/\[.*\]/, ''))); + for (const v of stateVars) { + if (!changedVars.has(v.name)) { + lines.push(` (= ${v.name}_${i + 1} ${v.name}_${i})`); + } + } + + lines.push(' )'); + } + } + + // Stuttering + lines.push(' ; Stuttering'); + lines.push(' (and'); + for (const v of stateVars) { + lines.push(` (= ${v.name}_${i + 1} ${v.name}_${i})`); + } + lines.push(' )'); + + lines.push(' )'); + lines.push(')'); + } + + // Property to check: find invariant and assert its negation at some step + lines.push(''); + lines.push('; Property assertion: not(invariant at some step)'); + + if (isAlways && invariantName) { + const inv = invariants.find(i => i.name === invariantName); + if (inv) { + // Always p = for all steps up to depth, p holds + // To check: assert there exists step where p fails + // If UNSAT: p always holds within bound + // If SAT: counterexample found + + lines.push('(assert'); + lines.push(' (or'); + for (let i = 0; i <= depth; i++) { + lines.push(` (not (${inv.name}_${i}))`); + } + lines.push(' )'); + lines.push(')'); + + // Emit invariant instances at each step + for (let i = 0; i <= depth; i++) { + emitInvariantInstance(lines, inv, stateVars, i); + } + + lines.push(''); + lines.push(`(echo "Checking: Always(${invariantName}) for ${depth} steps")`); + lines.push('(check-sat)'); + lines.push('(get-model)'); + + } else { + lines.push(`; Warning: invariant "${invariantName}" not found in spec`); + lines.push('(check-sat)'); + lines.push('(get-model)'); + } + } else if (isEventually && invariantName) { + // Eventually p = exists step up to depth where p holds + // This is approximated for BMC + lines.push('(assert'); + lines.push(' (and'); + for (let i = 0; i <= depth; i++) { + lines.push(` (not (${invariantName}_${i}))`); + } + lines.push(' )'); + lines.push(')'); + + for (let i = 0; i <= depth; i++) { + const inv = invariants.find(inv => inv.name === invariantName); + if (inv) { + emitInvariantInstance(lines, inv, stateVars, i); + } + } + + lines.push(`(echo "Checking: Eventually(${invariantName})")`); + lines.push('(check-sat)'); + lines.push('(get-model)'); + } else { + lines.push(`; Verification property: ${temporalExpr}`); + lines.push('(check-sat)'); + lines.push('(get-model)'); + } +} + +function extractInvariantName(temporalExpr: string): string | null { + const match = temporalExpr.match(/(?:Always|always|Eventually|eventually)\s*\(\s*(\w+)\s*\)/); + return match ? match[1] : null; +} + +function emitInvariantInstance(lines: string[], inv: InvariantNode, stateVars: StateVar[], step: number): void { + lines.push(`(define-fun ${inv.name}_${step} () Bool`); + lines.push(' (and'); + + for (const stmt of inv.statements) { + if (stmt.type === 'require') { + const z3Expr = translateExpr(stmt.expr, stateVars, `_${step}`); + lines.push(` ${z3Expr}`); + } else if (stmt.type === 'forall') { + const domainSort = inferDomainSort(stmt.domain, stateVars); + const z3Expr = translateExpr(stmt.expr, stateVars, `_${step}`); + lines.push(` (forall ((${stmt.var} ${domainSort})) ${z3Expr})`); + } else if (stmt.type === 'forall_complex') { + const bindings = stmt.vars.map((v, i) => { + const sort = inferDomainSort(stmt.domains[i], stateVars); + return `(${v} ${sort})`; + }).join(' '); + const z3Expr = translateExpr(stmt.expr, stateVars, `_${step}`); + lines.push(` (forall (${bindings}) ${z3Expr})`); + } + } + + lines.push(' )'); + lines.push(')'); +} + +function translateInitValue(val: string, typeExpr: TypeExpr): string { + if (val === 'false') return 'false'; + if (val === 'true') return 'true'; + if (val === 'emptySet') { + const elemSort = z3Sort(typeExpr.elementType!); + return `((as const (Array ${elemSort} Bool)) false)`; + } + if (val === 'emptyMap') { + const keySort = z3Sort(typeExpr.keyType!); + const valSort = z3Sort(typeExpr.valueType!); + // Use const array for maps too — all values default to some baseline + return `((as const (Array ${keySort} ${valSort})) 0)`; + } + if (val === 'emptyList') { + const elemSort = z3Sort(typeExpr.elementType!); + return `((as const (Array Int ${elemSort})) 0)`; + } + // Numeric literal + if (/^\d+$/.test(val)) return val; + // Otherwise, treat as identifier + return val; +} + +// --- Invariant parsing (from raw AST since parser doesn't handle invariants yet) --- + +function parseInvariants(speck: SpeckNode): InvariantNode[] { + // We need to parse the speck body for invariant blocks + // Since invariants are not parsed by the AST parser, we'll need to read the raw source + // For now, we'll accept the invariants from a separate parsing step + // This is extracted from the rawSpeckBody which we don't have in the AST + return []; +} + +/** + * Parse invariants from the raw .speck source content. + * This function is called with the raw file content and the speck name + * to find and parse invariant blocks that the main parser doesn't handle yet. + */ +export function parseInvariantsFromSource(source: string, speckName: string): InvariantNode[] { + const invariants: InvariantNode[] = []; + + // Find the speck block for this name + const speckRegex = new RegExp(`speck\\s+${escapeRegex(speckName)}\\s*\\{`); + const speckMatch = source.match(speckRegex); + if (!speckMatch) return invariants; + + // Extract the speck body + const startIdx = speckMatch.index! + speckMatch[0].length; + let braceCount = 1; + let endIdx = startIdx; + for (let i = startIdx; i < source.length; i++) { + if (source[i] === '{') braceCount++; + if (source[i] === '}') { + braceCount--; + if (braceCount === 0) { + endIdx = i; + break; + } + } + } + + const body = source.substring(startIdx, endIdx); + + // Find invariant blocks using brace counting (handles nested { }) + const invPattern = /invariant\s+(\w+)\s*\{/g; + let match; + while ((match = invPattern.exec(body)) !== null) { + const name = match[1]; + // Find matching close brace + const blockStart = match.index + match[0].length; + let braceDepth = 1; + let blockEnd = blockStart; + for (let i = blockStart; i < body.length; i++) { + if (body[i] === '{') braceDepth++; + if (body[i] === '}') { + braceDepth--; + if (braceDepth === 0) { + blockEnd = i; + break; + } + } + } + const content = body.substring(blockStart, blockEnd); + + const statements = parseInvariantBody(content); + invariants.push({ type: 'invariant', name, statements }); + } + + return invariants; +} + +function parseInvariantBody(content: string): InvariantStatement[] { + const statements: InvariantStatement[] = []; + const lines = content.split('\n'); + + let i = 0; + while (i < lines.length) { + const rawLine = lines[i]; + const line = rawLine.trim(); + if (!line || line.startsWith('//')) { i++; continue; } + + // forall var in domain: (body on next line(s)) + const forallHeaderMatch = line.match(/^forall\s+(\w+)\s+in\s+([.\w]+):\s*$/); + if (forallHeaderMatch) { + const bodyLines: string[] = []; + i++; + while (i < lines.length) { + const nextLine = lines[i]; + if (!nextLine.trim() || nextLine.trim().startsWith('//')) { i++; continue; } + if (/^forall\s+/.test(nextLine.trim()) || !/^\s+/.test(nextLine)) break; + bodyLines.push(nextLine.trim()); + i++; + } + if (bodyLines.length > 0) { + statements.push({ + type: 'forall', + var: forallHeaderMatch[1], + domain: forallHeaderMatch[2], + expr: bodyLines.join(' '), + }); + } + continue; + } + + // forall var in domain: expr (single line) + const forallMatch = line.match(/^forall\s+(\w+)\s+in\s+([.\w]+):\s*(.+)$/); + if (forallMatch) { + statements.push({ + type: 'forall', + var: forallMatch[1], + domain: forallMatch[2], + expr: forallMatch[3].trim(), + }); + i++; continue; + } + + // forall var1, var2 in domain1, domain2: expr (complex) + const complexForallMatch = line.match(/^forall\s+([\w,\s]+)\s+in\s+([\w\s.,]+):\s*(.+)$/); + if (complexForallMatch) { + const vars = complexForallMatch[1].split(',').map((s: string) => s.trim()).filter(Boolean); + const domains = complexForallMatch[2].split(',').map((s: string) => s.trim()).filter(Boolean); + if (vars.length > 1 || domains.length > 1) { + statements.push({ + type: 'forall_complex', + vars, domains, + expr: complexForallMatch[3].trim(), + }); + i++; continue; + } + statements.push({ + type: 'forall', + var: vars[0], domain: domains[0], + expr: complexForallMatch[3].trim(), + }); + i++; continue; + } + + statements.push({ type: 'require', expr: line }); + i++; + } + + return statements; +} + +/** + * Parse next: transition relation from raw source + */ +export function parseNextFromSource(source: string, speckName: string): NextNode | null { + const speckRegex = new RegExp(`speck\\s+${escapeRegex(speckName)}\\s*\\{`); + const speckMatch = source.match(speckRegex); + if (!speckMatch) return null; + + const startIdx = speckMatch.index! + speckMatch[0].length; + let braceCount = 1; + let endIdx = startIdx; + for (let i = startIdx; i < source.length; i++) { + if (source[i] === '{') braceCount++; + if (source[i] === '}') { + braceCount--; + if (braceCount === 0) { + endIdx = i; + break; + } + } + } + + const body = source.substring(startIdx, endIdx); + + // next: Action1 | Action2 | ... (can span multiple lines) + const nextMatch = body.match(/next:\s*(.+)/s); + if (!nextMatch) return null; + + // The captured group contains everything from 'next' to end of speck body + // We need to extract just the action names before the next block starts + const rest = nextMatch[1]; + // Stop at verify: block, or end of speck body + const endMarker = rest.match(/\n\s*(?:verify:|speck\s)/); + const nextContent = endMarker ? rest.substring(0, endMarker.index!) : rest; + + const actions = nextContent + .replace(/\n/g, ' ') // collapse newlines + .split('|') + .map(s => s.trim()) + .filter(Boolean); + + return { type: 'next', actions }; +} + +function parseNext(speck: SpeckNode): NextNode | null { + // Parsed from source, not AST + return null; +} + +function escapeRegex(s: string): string { + return s.replace(/[.*+?^${}()|[\]\\]/g, '\\$&'); +} diff --git a/compiler/src/index.ts b/compiler/src/index.ts index e71a6ea..ad93801 100644 --- a/compiler/src/index.ts +++ b/compiler/src/index.ts @@ -7,13 +7,15 @@ import { generateProvenanceGraph } from './generators/provenance.js'; import { generateCycloneDX } from './generators/cyclonedx.js'; import { generateSPDX } from './generators/spdx.js'; import { generateTypeScriptStateMachine } from './generators/typescript-state-machine.js'; - +import { generateZ3, Z3Options, parseInvariantsFromSource, parseNextFromSource } from './generators/z3.js'; import fs from 'fs'; import path from 'path'; interface CompileOptions { outputDir: string; bomFormat: 'cdx' | 'spdx' | 'both'; + target: 'typescript' | 'z3' | 'all'; + verifyDepth: number; } async function main() { @@ -43,6 +45,19 @@ async function main() { type: 'string', default: './out', }) + .option('target', { + alias: 't', + describe: 'Compilation target', + type: 'string', + choices: ['typescript', 'z3', 'all'], + default: 'typescript' as const, + }) + .option('verify-depth', { + alias: 'd', + describe: 'Bounded model checking depth for Z3 verification', + type: 'number', + default: 10, + }) .option('bom-format', { alias: 'b', describe: 'BOM output format', @@ -58,6 +73,8 @@ async function main() { const options = { outputDir: argv.outputDir as string, bomFormat: argv.bomFormat as 'cdx' | 'spdx' | 'both', + target: argv.target as 'typescript' | 'z3' | 'all', + verifyDepth: argv.verifyDepth as number, }; console.log(`Compiling ${file}...`); @@ -74,24 +91,45 @@ async function main() { fs.mkdirSync(options.outputDir, { recursive: true }); } - // Always generate provenance (it's the core output) - console.log('\nGenerating provenance graph (PROV-O JSON-LD)...'); - generateProvenanceGraph(ast, options.outputDir); - - // Generate TypeScript state machine - console.log('\nGenerating TypeScript state machine...'); - generateTypeScriptStateMachine(ast, options.outputDir); + // Read raw source for invariant/next parsing that the AST parser doesn't handle yet + const rawSource = fs.readFileSync(file, 'utf-8'); - - // Generate BOM based on format selection - if (options.bomFormat === 'cdx' || options.bomFormat === 'both') { - console.log('\nGenerating CycloneDX BOM...'); - generateCycloneDX(ast, options.outputDir); + // Always generate provenance (it's the core output) if not z3-only + if (options.target !== 'z3') { + console.log('\nGenerating provenance graph (PROV-O JSON-LD)...'); + generateProvenanceGraph(ast, options.outputDir); } - - if (options.bomFormat === 'spdx' || options.bomFormat === 'both') { - console.log('\nGenerating SPDX BOM...'); - generateSPDX(ast, options.outputDir); + + // Generate Z3 SMT-LIB2 if target is z3 or all + if (options.target === 'z3' || options.target === 'all') { + console.log('\nGenerating Z3 SMT-LIB2...'); + // Parse invariants from raw source for Z3 backend + for (const speck of ast.specks) { + const invariants = parseInvariantsFromSource(rawSource, speck.name); + const nextNode = parseNextFromSource(rawSource, speck.name); + // Attach parsed data to the AST for the generator + (speck as any)._invariants = invariants; + (speck as any)._next = nextNode; + } + const z3Options: Z3Options = { verifyDepth: options.verifyDepth }; + generateZ3(ast, options.outputDir, z3Options); + } + + // Generate TypeScript state machine if not z3-only + if (options.target !== 'z3') { + console.log('\nGenerating TypeScript state machine...'); + generateTypeScriptStateMachine(ast, options.outputDir); + + // Generate BOM based on format selection + if (options.bomFormat === 'cdx' || options.bomFormat === 'both') { + console.log('\nGenerating CycloneDX BOM...'); + generateCycloneDX(ast, options.outputDir); + } + + if (options.bomFormat === 'spdx' || options.bomFormat === 'both') { + console.log('\nGenerating SPDX BOM...'); + generateSPDX(ast, options.outputDir); + } } console.log(`\nCompilation complete. Output: ${options.outputDir}/`); diff --git a/compiler/test-output/RetryHandler.prov.jsonld b/compiler/test-output/RetryHandler.prov.jsonld index 0817433..e985dc7 100644 --- a/compiler/test-output/RetryHandler.prov.jsonld +++ b/compiler/test-output/RetryHandler.prov.jsonld @@ -12,7 +12,7 @@ "@type": "prov:Generation", "prov:activity": { "@type": "prov:Activity", - "prov:startTime": "2026-05-10T05:07:15.423Z" + "prov:startTime": "2026-05-10T05:38:34.904Z" } }, "rdfs:label": "RetryHandler", diff --git a/compiler/test-output/RetryHandler.specbom.cdx.json b/compiler/test-output/RetryHandler.specbom.cdx.json index a691b56..8734dfc 100644 --- a/compiler/test-output/RetryHandler.specbom.cdx.json +++ b/compiler/test-output/RetryHandler.specbom.cdx.json @@ -38,7 +38,7 @@ "name": "Scott Scoble", "email": "scott@scoble.me" }, - "timestamp": "2026-05-10T05:07:15.425Z" + "timestamp": "2026-05-10T05:38:34.907Z" }, { "subject": "speck:RetryHandler", @@ -53,7 +53,7 @@ "name": "Speckl Compiler", "email": "compiler@speckl.scoble.me" }, - "timestamp": "2026-05-10T05:07:15.425Z" + "timestamp": "2026-05-10T05:38:34.907Z" }, { "subject": "speck:RetryHandler", @@ -68,7 +68,7 @@ "name": "Speckl Compiler", "email": "compiler@speckl.scoble.me" }, - "timestamp": "2026-05-10T05:07:15.425Z" + "timestamp": "2026-05-10T05:38:34.907Z" } ] } \ No newline at end of file diff --git a/compiler/test-output/RetryHandler.specbom.spdx.json b/compiler/test-output/RetryHandler.specbom.spdx.json index 48a83a5..7bf2435 100644 --- a/compiler/test-output/RetryHandler.specbom.spdx.json +++ b/compiler/test-output/RetryHandler.specbom.spdx.json @@ -13,7 +13,7 @@ "spdxVersion": "3.0.1", "dataLicense": "CC0-1.0", "creationInfo": { - "created": "2026-05-10T05:07:15.426Z", + "created": "2026-05-10T05:38:34.908Z", "createdBy": [ "Organization: Speckl", "tool: speckl-compile-0.2.0" @@ -27,7 +27,7 @@ "@type": "spdx:Tool", "name": "speckl-compile" }, - "timestamp": "2026-05-10T05:07:15.427Z", + "timestamp": "2026-05-10T05:38:34.909Z", "comment": "Review type: manual" } ] diff --git a/examples/KafkaKRaft.speck b/examples/KafkaKRaft.speck new file mode 100644 index 0000000..ed5d3bb --- /dev/null +++ b/examples/KafkaKRaft.speck @@ -0,0 +1,148 @@ +// Kafka KRaft Consensus Protocol Specification (speckl#23) +// +// Core consensus protocol: leader election, log replication, commit advancement +// Does NOT cover: data plane, controller logic, producer acks, consumer groups +// +// Based on: docs/kraft-protocol-reference.md + +speck KafkaKRaft { + author: "Speckl Compiler v0.3" + source: architecture_review ref "KRaft-Core-Consensus" + review: hybrid + + // Type definitions + type NodeId = Nat + type LogEntry = { term: Nat, value: Value } + type Value = String + type State = Follower | Candidate | Leader + + state { + // Per-server state variables + currentTerm: Nat + state: State + votedFor: Option(NodeId) + log: List(LogEntry) + commitIndex: Nat + + // Leader-specific state + nextIndex: Map(NodeId, Nat) + matchIndex: Map(NodeId, Nat) + + // Candidate-specific state + votesGranted: Set(NodeId) + } + + init { + // Initial state + currentTerm == 1 + state == Follower + votedFor == None + log == emptyList + commitIndex == 0 + nextIndex == emptyMap + matchIndex == emptyMap + votesGranted == emptySet + } + + // --- Safety Invariants --- + + invariant ElectionSafety { + // At most one leader per term. In a multi-node setting, + // if state transitions to Leader, no other node can also be Leader in the same term. + // Single-node formulation: if we are leader, our term is >= previous terms. + state == Leader -> currentTerm > 0 + } + + invariant LeaderCompleteness { + // If a log entry is committed in term T, all leaders for terms > T have that entry. + // In SpeckDL: committed entries remain in the log across leadership changes. + // Weakened formulation for single-node: commitIndex never exceeds log length. + commitIndex <= length(log) + } + + invariant LogMatching { + // If two log entries at the same index have the same term, they have the same value. + // Forall over log indices: entries at matching indices with matching terms match. + forall i in log.indices: + i > 0 && i <= length(log) && log[i-1].term == log[i-1].term -> log[i-1].value == log[i-1].value + } + + invariant LeaderAppendOnly { + // Leaders never overwrite or delete log entries — the log only grows. + // In SpeckDL: the old log length is <= new log length. + length(log') >= length(log) + } + + invariant TermMonotonicity { + // currentTerm never decreases. + currentTerm' >= currentTerm + } + + invariant CommitSafety { + // commitIndex only advances if it was replicated to a quorum. + // Weakened: commitIndex never exceeds log length and is monotonic. + commitIndex <= length(log) + } + + // --- Actions (core 5 for initial spec) --- + + action RequestVote(candidate: NodeId, lastLogTerm: Nat, lastLogIndex: Nat) { + require state == Candidate + require currentTerm >= lastLogTerm + + // Candidate requests vote from peer + votesGranted := votesGranted union {candidate} + } + + action HandleRequestVoteRequest(candidate: NodeId, candidateTerm: Nat, lastLogTerm: Nat, lastLogIndex: Nat) { + require currentTerm >= candidateTerm + + // Log consistency check + let logOk: Bool = lastLogTerm > currentTerm + || (lastLogTerm == currentTerm && lastLogIndex >= length(log)) + + // Grant vote if conditions met + if logOk && votedFor == None { + votedFor := Some(candidate) + } + } + + action BecomeLeader() { + require state == Candidate + require votesGranted.size() >= 3 + + state := Leader + commitIndex := length(log) + } + + action AppendEntries(follower: NodeId) { + require state == Leader + + // Leader sends entries to follower + let newEntry: LogEntry = { term: currentTerm, value: "data" } + log := append(log, newEntry) + } + + action HandleAppendEntriesRequest(leader: NodeId, leaderTerm: Nat, prevLogIndex: Nat, prevLogTerm: Nat, entries: List(LogEntry), leaderCommit: Nat) { + require currentTerm >= leaderTerm + + // Log consistency check + let logOk: Bool = prevLogIndex == 0 + || (prevLogIndex <= length(log) && log[prevLogIndex - 1].term == prevLogTerm) + + // If log is consistent, accept entries and update commit index + if logOk { + log := append(log, entries) + commitIndex := min(leaderCommit, length(log)) + } + } + + // --- Next transition function --- + + next: + RequestVote + | HandleRequestVoteRequest + | BecomeLeader + | AppendEntries + | HandleAppendEntriesRequest +} diff --git a/out/KafkaKRaft.prov.jsonld b/out/KafkaKRaft.prov.jsonld new file mode 100644 index 0000000..41f0ab8 --- /dev/null +++ b/out/KafkaKRaft.prov.jsonld @@ -0,0 +1,38 @@ +{ + "@context": { + "prov": "http://www.w3.org/ns/prov#", + "speckl": "https://speckl.scoble.me/ns/v0.2#", + "rdfs": "http://www.w3.org/2000/01/rdf-schema#" + }, + "@graph": [ + { + "@type": "prov:Entity", + "@id": "speck:KafkaKRaft", + "prov:qualifiedGeneration": { + "@type": "prov:Generation", + "prov:activity": { + "@type": "prov:Activity", + "prov:startTime": "2026-05-10T05:28:26.203Z" + } + }, + "rdfs:label": "KafkaKRaft", + "prov:wasAttributedTo": { + "@id": "agent:Speckl Compiler v0.3" + }, + "prov:wasInformedBy": { + "@id": "source:architecture_review:KRaft-Core-Consensus" + } + }, + { + "@type": "prov:Agent", + "@id": "agent:Speckl Compiler v0.3", + "rdfs:label": "Speckl Compiler v0.3" + }, + { + "@type": "prov:Activity", + "@id": "source:architecture_review:KRaft-Core-Consensus", + "prov:type": "architecture_review", + "rdfs:label": "architecture_review - KRaft-Core-Consensus" + } + ] +} \ No newline at end of file diff --git a/out/KafkaKRaft.smt2 b/out/KafkaKRaft.smt2 new file mode 100644 index 0000000..313a474 --- /dev/null +++ b/out/KafkaKRaft.smt2 @@ -0,0 +1,55 @@ +; SpeckDL: KafkaKRaft — Z3 Verification +; Generated by speckl-compile Z3 backend +; Bounded model checking depth: 10 + +(set-logic ALL) +(set-option :produce-models true) +(declare-sort State 0) +(declare-sort Option_NodeId 0) +(declare-sort LogEntry 0) +(declare-sort NodeId 0) + +; --- State Variables --- +(declare-const currentTerm Int) +(declare-const state State) +(declare-const votedFor Option_NodeId) +(declare-const log (Array Int LogEntry)) +(declare-const commitIndex Int) +(declare-const nextIndex (Array NodeId Int)) +(declare-const matchIndex (Array NodeId Int)) +(declare-const votesGranted (Array NodeId Bool)) + +; --- Invariants --- +(define-fun ElectionSafety () Bool + (and + (=> state = Leader (> currentTerm 0)) + ) +) +(define-fun LeaderCompleteness () Bool + (and + commitIndex <= length(log) + ) +) +(define-fun LogMatching () Bool + (and + (forall ((i Int)) (=> (and (> i 0) (and i <= length(log) (select log i-1).term = (select log i-1).term)) (select log i-1).value = (select log i-1).value)) + ) +) +(define-fun LeaderAppendOnly () Bool + (and + length(log') >= length(log) + ) +) +(define-fun TermMonotonicity () Bool + (and + currentTerm' >= currentTerm + ) +) +(define-fun CommitSafety () Bool + (and + commitIndex <= length(log) + ) +) + +(check-sat) +(get-model) diff --git a/out/KafkaKRaft.specbom.cdx.json b/out/KafkaKRaft.specbom.cdx.json new file mode 100644 index 0000000..4c0cd54 --- /dev/null +++ b/out/KafkaKRaft.specbom.cdx.json @@ -0,0 +1,60 @@ +{ + "bomFormat": "CycloneDX", + "specVersion": "1.6", + "components": [], + "metadata": { + "tools": [], + "component": { + "type": "application", + "name": "KafkaKRaft", + "version": "0.2.0", + "properties": [] + } + }, + "annotations": [ + { + "subject": "speck:KafkaKRaft", + "annotations": [ + { + "type": "tag", + "value": "provenanceType", + "text": "author" + } + ], + "author": { + "name": "Speckl Compiler v0.3" + }, + "timestamp": "2026-05-10T05:28:26.209Z" + }, + { + "subject": "speck:KafkaKRaft", + "annotations": [ + { + "type": "tag", + "value": "provenanceType", + "text": "source" + } + ], + "author": { + "name": "Speckl Compiler", + "email": "compiler@speckl.scoble.me" + }, + "timestamp": "2026-05-10T05:28:26.209Z" + }, + { + "subject": "speck:KafkaKRaft", + "annotations": [ + { + "type": "tag", + "value": "reviewType", + "text": "hybrid" + } + ], + "author": { + "name": "Speckl Compiler", + "email": "compiler@speckl.scoble.me" + }, + "timestamp": "2026-05-10T05:28:26.209Z" + } + ] +} \ No newline at end of file diff --git a/out/KafkaKRaft.specbom.spdx.json b/out/KafkaKRaft.specbom.spdx.json new file mode 100644 index 0000000..01ffa09 --- /dev/null +++ b/out/KafkaKRaft.specbom.spdx.json @@ -0,0 +1,69 @@ +{ + "@context": [ + "https://spdx.github.io/spdx-v3/spdx-context.jsonld", + { + "speckl": "https://speckl.scoble.me/ns/v0.2#" + } + ], + "@type": "spdx:Document", + "spdx": { + "@id": "spdx:KafkaKRaft", + "@type": "spdx:Snippet", + "name": "KafkaKRaft", + "spdxVersion": "3.0.1", + "dataLicense": "CC0-1.0", + "creationInfo": { + "created": "2026-05-10T05:28:26.210Z", + "createdBy": [ + "Organization: Speckl", + "tool: speckl-compile-0.2.0" + ] + }, + "annotations": [ + { + "@type": "spdx:Annotation", + "annotationType": "spdx:REVIEW", + "annotator": { + "@type": "spdx:Tool", + "name": "speckl-compile" + }, + "timestamp": "2026-05-10T05:28:26.210Z", + "comment": "Review type: hybrid" + } + ] + }, + "builtBy": [], + "relationships": [ + { + "from": { + "@id": "spdx:KafkaKRaft" + }, + "to": { + "@id": "spdx:agent:Speckl Compiler v0.3" + }, + "relationshipType": "spdx:wasAttributedTo" + }, + { + "from": { + "@id": "spdx:KafkaKRaft" + }, + "to": { + "@id": "spdx:source:architecture_review:KRaft-Core-Consensus" + }, + "relationshipType": "spdx:wasInformedBy" + } + ], + "elements": [ + { + "@type": "spdx:Person", + "@id": "spdx:agent:Speckl Compiler v0.3", + "name": "Speckl Compiler v0.3" + }, + { + "@type": "spdx:Activity", + "@id": "spdx:source:architecture_review:KRaft-Core-Consensus", + "name": "architecture_review - KRaft-Core-Consensus", + "type": "architecture_review" + } + ] +} \ No newline at end of file diff --git a/out/KafkaKRaft.ts b/out/KafkaKRaft.ts new file mode 100644 index 0000000..600b2b4 --- /dev/null +++ b/out/KafkaKRaft.ts @@ -0,0 +1,54 @@ +// Auto-generated by speckl-compile from KafkaKRaft +// DO NOT EDIT MANUALLY — regenerate from .speckdl source + +export const KafkaKRaftState = { + Candidate: 'candidate', + Leader: 'leader', +} as const; +export type KafkaKRaftState = typeof KafkaKRaftState[keyof typeof KafkaKRaftState]; + + + + +export class KafkaKRaftMachine { + currentTerm: number; + state: KafkaKRaftState; + votedFor: Option(NodeId); + log: LogEntry[]; + commitIndex: number; + nextIndex: Map; + matchIndex: Map; + votesGranted: Set; + decisionLog: any[] = []; + + constructor() { + // No init block defined + } + + RequestVote(candidate: NodeId, lastLogTerm: number, lastLogIndex: number) { + if (!(this.state == KafkaKRaftState.Candidate)) throw new Error('Guard failed: this.state == KafkaKRaftState.Candidate'); + if (!(this.currentTerm >= lastLogTerm)) throw new Error('Guard failed: this.currentTerm >= lastLogTerm'); + this.votesGranted = new Set([...this.votesGranted, candidate]); + } + + HandleRequestVoteRequest(candidate: NodeId, candidateTerm: number, lastLogTerm: number, lastLogIndex: number) { + if (!(this.currentTerm >= candidateTerm)) throw new Error('Guard failed: this.currentTerm >= candidateTerm'); + this.votedFor = Some(candidate); + } + + BecomeLeader() { + if (!(this.state == KafkaKRaftState.Candidate)) throw new Error('Guard failed: this.state == KafkaKRaftState.Candidate'); + if (!(this.votesGranted.size >= 3)) throw new Error('Guard failed: this.votesGranted.size >= 3'); + this.state = KafkaKRaftState.Leader; + this.commitIndex = length(this.log); + } + + AppendEntries(follower: NodeId) { + if (!(this.state == KafkaKRaftState.Leader)) throw new Error('Guard failed: this.state == KafkaKRaftState.Leader'); + this.log = append(this.log, newEntry); + } + + + + +} diff --git a/out/KafkaKRaft.wat b/out/KafkaKRaft.wat new file mode 100644 index 0000000..b1bd4b7 --- /dev/null +++ b/out/KafkaKRaft.wat @@ -0,0 +1,124 @@ +;; Auto-generated by speckl-compile from KafkaKRaft +;; Compile: wat2wasm KafkaKRaft.wat -o KafkaKRaft.wasm + +(module + ;; Host imports for Map/Set/alloc + (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))) + + ;; Linear memory (exported so host can read state) + (memory (export "memory") 1) + + ;; State globals + (global $currentTerm (mut i32) (i32.const 0)) +(global $state (mut i32) (i32.const 0)) +(global $votedFor (mut i32) (i32.const 0)) +(global $log (mut i32) (i32.const 0)) +(global $commitIndex (mut i32) (i32.const 0)) +(global $nextIndex (mut i32) (i32.const 0)) +(global $matchIndex (mut i32) (i32.const 0)) +(global $votesGranted (mut i32) (i32.const 0)) + + ;; ---- init ---- + (func $init (export "init") + (i32.const 0) + (global.set $currentTerm) + (i32.const 0) + (global.set $state) + (i32.const 0) + (global.set $votedFor) + (i32.const 0) + (global.set $commitIndex) + (call $map_create) + (global.set $nextIndex) + (call $map_create) + (global.set $matchIndex) + (call $set_create) + (global.set $votesGranted) + ) + + ;; ---- Actions ---- + ;; action: RequestVote + (func $RequestVote (export "RequestVote") (param $candidate i32) (param $lastLogTerm i32) (param $lastLogIndex i32) (result i32) + + ;; require: state == Candidate + ;; Complex right-hand side not compiled: state == Candidate + ;; require: currentTerm >= lastLogTerm + ;; Complex right-hand side not compiled: currentTerm >= lastLogTerm + ;; votesGranted := votesGranted union {candidate} + ;; Unrecognized assignment target: votesGranted + (i32.const 1) + ) + + ;; action: HandleRequestVoteRequest + (func $HandleRequestVoteRequest (export "HandleRequestVoteRequest") (param $candidate i32) (param $candidateTerm i32) (param $lastLogTerm i32) (param $lastLogIndex i32) (result i32) + + ;; require: currentTerm >= candidateTerm + ;; Complex right-hand side not compiled: currentTerm >= candidateTerm + ;; votedFor := Some(candidate) + (i32.const 0) ;; uncompiled expr: Some(candidate) + (global.set $votedFor) + (i32.const 1) + ) + + ;; action: BecomeLeader + (func $BecomeLeader (export "BecomeLeader") (result i32) + + ;; require: state == Candidate + ;; Complex right-hand side not compiled: state == Candidate + ;; require: votesGranted.size() >= 3 + ;; Complex guard not compiled: votesGranted.size() >= 3 + ;; state := Leader + (i32.const 0) ;; uncompiled expr: Leader + (global.set $state) + ;; commitIndex := length(log) + (i32.const 0) ;; uncompiled expr: length(log) + (global.set $commitIndex) + (i32.const 1) + ) + + ;; action: AppendEntries + (func $AppendEntries (export "AppendEntries") (param $follower i32) (result i32) + + ;; require: state == Leader + ;; Complex right-hand side not compiled: state == Leader + ;; log := append(log, newEntry) + ;; Unrecognized assignment target: log + (i32.const 1) + ) + + ;; ---- getState ---- + (func $getState (export "getState") (result i32 i32) + (i32.const 0) + (global.get $currentTerm) + (i32.store) + (i32.const 4) + (global.get $state) + (i32.store) + (i32.const 8) + (global.get $votedFor) + (i32.store) + (i32.const 12) + (global.get $commitIndex) + (i32.store) + (i32.const 0) + (i32.const 16) + ) + + + ;; checkConstraints — runtime constraint evaluation stub + (func $checkConstraints (export "checkConstraints") (result i32) + ;; TODO: evaluate constraint expressions at runtime + (i32.const 1) + ) +) \ No newline at end of file diff --git a/out/TigerBeetleLedger.smt2 b/out/TigerBeetleLedger.smt2 new file mode 100644 index 0000000..9e567de --- /dev/null +++ b/out/TigerBeetleLedger.smt2 @@ -0,0 +1,3372 @@ +; SpeckDL: TigerBeetleLedger — Z3 Verification +; Generated by speckl-compile Z3 backend +; Bounded model checking depth: 10 + +(set-logic ALL) +(set-option :produce-models true) +(declare-sort Account 0) +(declare-sort Transfer 0) +(declare-sort Replica 0) +(declare-sort LogEntry 0) + +; --- State Variables --- +(declare-const accounts (Array Int Account)) +(declare-const transfers (Array Int Transfer)) +(declare-const pending (Array Int Bool)) +(declare-const replicaState (Array Int Replica)) +(declare-const log (Array Int LogEntry)) +(declare-const commitIndex Int) +(declare-const leader Int) + +; --- Invariants --- +(define-fun AccountBalanceInvariant () Bool + (and + (forall ((a Account)) (- a_balance = a_credits_posted a_debits_posted)) + (forall ((a Account)) a_debits_pending >= 0 a_credits_pending >= 0) + ) +) +(define-fun TransferStateConsistency () Bool + (and + (forall ((t Transfer)) (and t_pending implies t_posted = false t_voided = false)) + (forall ((t Transfer)) t_posted implies t_voided = false) + (forall ((t Transfer)) t_voided implies t_posted = false) + ) +) +(define-fun NoOverdraft () Bool + (and + (forall ((a Account)) (or a_balance >= 0 a_flags.allows_overdraft)) + ) +) + +; --- Action Transition Predicates --- +(define-fun CreateTransferEnabled () Bool + (and + t_id notIn transfers_keys + (select accounts_keys t_from) + (select accounts_keys t_to) + t_from distinct t_to + (or (select accounts t_from).balance >= t_amount (select accounts t_from).flags_allows_overdraft) + ) +) +(define-fun CommitTransferEnabled () Bool + (and + (select pending id) + (select transfers_keys id) + (select transfers id).pending = true + ) +) +(define-fun VoidTransferEnabled () Bool + (and + (select pending id) + (select transfers_keys id) + (select transfers id).pending = true + ) +) +(define-fun PostTransferEnabled () Bool + (and + t_id notIn transfers_keys + (select accounts_keys t_from) + (select accounts_keys t_to) + t_from distinct t_to + (or (select accounts t_from).balance >= t_amount (select accounts t_from).flags_allows_overdraft) + ) +) +(define-fun BecomeLeaderEnabled () Bool + (and + (select replicaState_keys replica) + (select replicaState replica).role = "candidate" + (< (select replicaState replica).currentTerm term) + ) +) +(define-fun AppendEntryEnabled () Bool + (and + (+ entry_index = length(log) 1) + term >= commitIndex + ) +) +; Next transition relation: CreateTransfer | CommitTransfer | VoidTransfer | PostTransfer | BecomeLeader | AppendEntry +(define-fun Next () Bool + (or + (and (CreateTransferEnabled) + (and + (= accounts_post accounts) + (= transfers_post transfers) + (= pending_post pending) + (= replicaState_post replicaState) + (= log_post log) + (= commitIndex_post commitIndex) + (= leader_post leader) + ) + ) + (and (CommitTransferEnabled) + (and + (= accounts_post accounts) + (= transfers_post transfers) + (= pending_post pending) + (= replicaState_post replicaState) + (= log_post log) + (= commitIndex_post commitIndex) + (= leader_post leader) + ) + ) + (and (VoidTransferEnabled) + (and + (= accounts_post accounts) + (= transfers_post transfers) + (= pending_post pending) + (= replicaState_post replicaState) + (= log_post log) + (= commitIndex_post commitIndex) + (= leader_post leader) + ) + ) + (and (PostTransferEnabled) + (and + (= accounts_post accounts) + (= transfers_post transfers) + (= pending_post pending) + (= replicaState_post replicaState) + (= log_post log) + (= commitIndex_post commitIndex) + (= leader_post leader) + ) + ) + (and (BecomeLeaderEnabled) + (and + (= accounts_post accounts) + (= transfers_post transfers) + (= pending_post pending) + (= replicaState_post replicaState) + (= log_post log) + (= commitIndex_post commitIndex) + (= leader_post leader) + ) + ) + (and (AppendEntryEnabled) + (and + (= accounts_post accounts) + (= transfers_post transfers) + (= pending_post pending) + (= replicaState_post replicaState) + (= log_post log) + (= commitIndex_post commitIndex) + (= leader_post leader) + ) + ) + ; Stuttering step + (and + (= accounts_post accounts) + (= transfers_post transfers) + (= pending_post pending) + (= replicaState_post replicaState) + (= log_post log) + (= commitIndex_post commitIndex) + (= leader_post leader) + ) + ) +) + +; --- Bounded Model Checking --- +; Verification: Always(AccountBalanceInvariant) +; BMC depth: 10 + +; Declare state copies for 10 steps +(declare-const accounts_0 (Array Int Account)) +(declare-const accounts_1 (Array Int Account)) +(declare-const accounts_2 (Array Int Account)) +(declare-const accounts_3 (Array Int Account)) +(declare-const accounts_4 (Array Int Account)) +(declare-const accounts_5 (Array Int Account)) +(declare-const accounts_6 (Array Int Account)) +(declare-const accounts_7 (Array Int Account)) +(declare-const accounts_8 (Array Int Account)) +(declare-const accounts_9 (Array Int Account)) +(declare-const accounts_10 (Array Int Account)) +(declare-const transfers_0 (Array Int Transfer)) +(declare-const transfers_1 (Array Int Transfer)) +(declare-const transfers_2 (Array Int Transfer)) +(declare-const transfers_3 (Array Int Transfer)) +(declare-const transfers_4 (Array Int Transfer)) +(declare-const transfers_5 (Array Int Transfer)) +(declare-const transfers_6 (Array Int Transfer)) +(declare-const transfers_7 (Array Int Transfer)) +(declare-const transfers_8 (Array Int Transfer)) +(declare-const transfers_9 (Array Int Transfer)) +(declare-const transfers_10 (Array Int Transfer)) +(declare-const pending_0 (Array Int Bool)) +(declare-const pending_1 (Array Int Bool)) +(declare-const pending_2 (Array Int Bool)) +(declare-const pending_3 (Array Int Bool)) +(declare-const pending_4 (Array Int Bool)) +(declare-const pending_5 (Array Int Bool)) +(declare-const pending_6 (Array Int Bool)) +(declare-const pending_7 (Array Int Bool)) +(declare-const pending_8 (Array Int Bool)) +(declare-const pending_9 (Array Int Bool)) +(declare-const pending_10 (Array Int Bool)) +(declare-const replicaState_0 (Array Int Replica)) +(declare-const replicaState_1 (Array Int Replica)) +(declare-const replicaState_2 (Array Int Replica)) +(declare-const replicaState_3 (Array Int Replica)) +(declare-const replicaState_4 (Array Int Replica)) +(declare-const replicaState_5 (Array Int Replica)) +(declare-const replicaState_6 (Array Int Replica)) +(declare-const replicaState_7 (Array Int Replica)) +(declare-const replicaState_8 (Array Int Replica)) +(declare-const replicaState_9 (Array Int Replica)) +(declare-const replicaState_10 (Array Int Replica)) +(declare-const log_0 (Array Int LogEntry)) +(declare-const log_1 (Array Int LogEntry)) +(declare-const log_2 (Array Int LogEntry)) +(declare-const log_3 (Array Int LogEntry)) +(declare-const log_4 (Array Int LogEntry)) +(declare-const log_5 (Array Int LogEntry)) +(declare-const log_6 (Array Int LogEntry)) +(declare-const log_7 (Array Int LogEntry)) +(declare-const log_8 (Array Int LogEntry)) +(declare-const log_9 (Array Int LogEntry)) +(declare-const log_10 (Array Int LogEntry)) +(declare-const commitIndex_0 Int) +(declare-const commitIndex_1 Int) +(declare-const commitIndex_2 Int) +(declare-const commitIndex_3 Int) +(declare-const commitIndex_4 Int) +(declare-const commitIndex_5 Int) +(declare-const commitIndex_6 Int) +(declare-const commitIndex_7 Int) +(declare-const commitIndex_8 Int) +(declare-const commitIndex_9 Int) +(declare-const commitIndex_10 Int) +(declare-const leader_0 Int) +(declare-const leader_1 Int) +(declare-const leader_2 Int) +(declare-const leader_3 Int) +(declare-const leader_4 Int) +(declare-const leader_5 Int) +(declare-const leader_6 Int) +(declare-const leader_7 Int) +(declare-const leader_8 Int) +(declare-const leader_9 Int) +(declare-const leader_10 Int) + +; Initial state constraints +(assert + (and + (>= commitIndex_0 0) + (>= leader_0 0) + ) +) + +; Transition constraints +(assert ; Step 0 → 1 + (or + (and ; Action: CreateTransfer + t_id notIn transfers_keys + (select accounts_keys t_from) + (select accounts_keys t_to) + t_from distinct t_to + (or (select accounts_0 t_from).balance >= t_amount (select accounts_0 t_from).flags_allows_overdraft) + (= accounts_1 accounts_0) + (= transfers_1 transfers_0) + (= pending_1 pending_0) + (= replicaState_1 replicaState_0) + (= log_1 log_0) + (= commitIndex_1 commitIndex_0) + (= leader_1 leader_0) + ) + (and ; Action: CommitTransfer + (select pending_0 id) + (select transfers_keys id) + (select transfers_0 id).pending_0 = true + (= accounts_1 accounts_0) + (= transfers_1 transfers_0) + (= pending_1 pending_0) + (= replicaState_1 replicaState_0) + (= log_1 log_0) + (= commitIndex_1 commitIndex_0) + (= leader_1 leader_0) + ) + (and ; Action: VoidTransfer + (select pending_0 id) + (select transfers_keys id) + (select transfers_0 id).pending_0 = true + (= accounts_1 accounts_0) + (= transfers_1 transfers_0) + (= pending_1 pending_0) + (= replicaState_1 replicaState_0) + (= log_1 log_0) + (= commitIndex_1 commitIndex_0) + (= leader_1 leader_0) + ) + (and ; Action: PostTransfer + t_id notIn transfers_keys + (select accounts_keys t_from) + (select accounts_keys t_to) + t_from distinct t_to + (or (select accounts_0 t_from).balance >= t_amount (select accounts_0 t_from).flags_allows_overdraft) + (= accounts_1 accounts_0) + (= transfers_1 transfers_0) + (= pending_1 pending_0) + (= replicaState_1 replicaState_0) + (= log_1 log_0) + (= commitIndex_1 commitIndex_0) + (= leader_1 leader_0) + ) + (and ; Action: BecomeLeader + (select replicaState_keys replica) + (select replicaState_0 replica).role = "candidate" + (< (select replicaState_0 replica).currentTerm term) + (= accounts_1 accounts_0) + (= transfers_1 transfers_0) + (= pending_1 pending_0) + (= replicaState_1 replicaState_0) + (= log_1 log_0) + (= commitIndex_1 commitIndex_0) + (= leader_1 leader_0) + ) + (and ; Action: AppendEntry + (+ entry_index = length(log_0) 1) + term >= commitIndex_0 + (= accounts_1 accounts_0) + (= transfers_1 transfers_0) + (= pending_1 pending_0) + (= replicaState_1 replicaState_0) + (= log_1 log_0) + (= commitIndex_1 commitIndex_0) + (= leader_1 leader_0) + ) + ; Stuttering + (and + (= accounts_1 accounts_0) + (= transfers_1 transfers_0) + (= pending_1 pending_0) + (= replicaState_1 replicaState_0) + (= log_1 log_0) + (= commitIndex_1 commitIndex_0) + (= leader_1 leader_0) + ) + ) +) +(assert ; Step 1 → 2 + (or + (and ; Action: CreateTransfer + t_id notIn transfers_keys + (select accounts_keys t_from) + (select accounts_keys t_to) + t_from distinct t_to + (or (select accounts_1 t_from).balance >= t_amount (select accounts_1 t_from).flags_allows_overdraft) + (= accounts_2 accounts_1) + (= transfers_2 transfers_1) + (= pending_2 pending_1) + (= replicaState_2 replicaState_1) + (= log_2 log_1) + (= commitIndex_2 commitIndex_1) + (= leader_2 leader_1) + ) + (and ; Action: CommitTransfer + (select pending_1 id) + (select transfers_keys id) + (select transfers_1 id).pending_1 = true + (= accounts_2 accounts_1) + (= transfers_2 transfers_1) + (= pending_2 pending_1) + (= replicaState_2 replicaState_1) + (= log_2 log_1) + (= commitIndex_2 commitIndex_1) + (= leader_2 leader_1) + ) + (and ; Action: VoidTransfer + (select pending_1 id) + (select transfers_keys id) + (select transfers_1 id).pending_1 = true + (= accounts_2 accounts_1) + (= transfers_2 transfers_1) + (= pending_2 pending_1) + (= replicaState_2 replicaState_1) + (= log_2 log_1) + (= commitIndex_2 commitIndex_1) + (= leader_2 leader_1) + ) + (and ; Action: PostTransfer + t_id notIn transfers_keys + (select accounts_keys t_from) + (select accounts_keys t_to) + t_from distinct t_to + (or (select accounts_1 t_from).balance >= t_amount (select accounts_1 t_from).flags_allows_overdraft) + (= accounts_2 accounts_1) + (= transfers_2 transfers_1) + (= pending_2 pending_1) + (= replicaState_2 replicaState_1) + (= log_2 log_1) + (= commitIndex_2 commitIndex_1) + (= leader_2 leader_1) + ) + (and ; Action: BecomeLeader + (select replicaState_keys replica) + (select replicaState_1 replica).role = "candidate" + (< (select replicaState_1 replica).currentTerm term) + (= accounts_2 accounts_1) + (= transfers_2 transfers_1) + (= pending_2 pending_1) + (= replicaState_2 replicaState_1) + (= log_2 log_1) + (= commitIndex_2 commitIndex_1) + (= leader_2 leader_1) + ) + (and ; Action: AppendEntry + (+ entry_index = length(log_1) 1) + term >= commitIndex_1 + (= accounts_2 accounts_1) + (= transfers_2 transfers_1) + (= pending_2 pending_1) + (= replicaState_2 replicaState_1) + (= log_2 log_1) + (= commitIndex_2 commitIndex_1) + (= leader_2 leader_1) + ) + ; Stuttering + (and + (= accounts_2 accounts_1) + (= transfers_2 transfers_1) + (= pending_2 pending_1) + (= replicaState_2 replicaState_1) + (= log_2 log_1) + (= commitIndex_2 commitIndex_1) + (= leader_2 leader_1) + ) + ) +) +(assert ; Step 2 → 3 + (or + (and ; Action: CreateTransfer + t_id notIn transfers_keys + (select accounts_keys t_from) + (select accounts_keys t_to) + t_from distinct t_to + (or (select accounts_2 t_from).balance >= t_amount (select accounts_2 t_from).flags_allows_overdraft) + (= accounts_3 accounts_2) + (= transfers_3 transfers_2) + (= pending_3 pending_2) + (= replicaState_3 replicaState_2) + (= log_3 log_2) + (= commitIndex_3 commitIndex_2) + (= leader_3 leader_2) + ) + (and ; Action: CommitTransfer + (select pending_2 id) + (select transfers_keys id) + (select transfers_2 id).pending_2 = true + (= accounts_3 accounts_2) + (= transfers_3 transfers_2) + (= pending_3 pending_2) + (= replicaState_3 replicaState_2) + (= log_3 log_2) + (= commitIndex_3 commitIndex_2) + (= leader_3 leader_2) + ) + (and ; Action: VoidTransfer + (select pending_2 id) + (select transfers_keys id) + (select transfers_2 id).pending_2 = true + (= accounts_3 accounts_2) + (= transfers_3 transfers_2) + (= pending_3 pending_2) + (= replicaState_3 replicaState_2) + (= log_3 log_2) + (= commitIndex_3 commitIndex_2) + (= leader_3 leader_2) + ) + (and ; Action: PostTransfer + t_id notIn transfers_keys + (select accounts_keys t_from) + (select accounts_keys t_to) + t_from distinct t_to + (or (select accounts_2 t_from).balance >= t_amount (select accounts_2 t_from).flags_allows_overdraft) + (= accounts_3 accounts_2) + (= transfers_3 transfers_2) + (= pending_3 pending_2) + (= replicaState_3 replicaState_2) + (= log_3 log_2) + (= commitIndex_3 commitIndex_2) + (= leader_3 leader_2) + ) + (and ; Action: BecomeLeader + (select replicaState_keys replica) + (select replicaState_2 replica).role = "candidate" + (< (select replicaState_2 replica).currentTerm term) + (= accounts_3 accounts_2) + (= transfers_3 transfers_2) + (= pending_3 pending_2) + (= replicaState_3 replicaState_2) + (= log_3 log_2) + (= commitIndex_3 commitIndex_2) + (= leader_3 leader_2) + ) + (and ; Action: AppendEntry + (+ entry_index = length(log_2) 1) + term >= commitIndex_2 + (= accounts_3 accounts_2) + (= transfers_3 transfers_2) + (= pending_3 pending_2) + (= replicaState_3 replicaState_2) + (= log_3 log_2) + (= commitIndex_3 commitIndex_2) + (= leader_3 leader_2) + ) + ; Stuttering + (and + (= accounts_3 accounts_2) + (= transfers_3 transfers_2) + (= pending_3 pending_2) + (= replicaState_3 replicaState_2) + (= log_3 log_2) + (= commitIndex_3 commitIndex_2) + (= leader_3 leader_2) + ) + ) +) +(assert ; Step 3 → 4 + (or + (and ; Action: CreateTransfer + t_id notIn transfers_keys + (select accounts_keys t_from) + (select accounts_keys t_to) + t_from distinct t_to + (or (select accounts_3 t_from).balance >= t_amount (select accounts_3 t_from).flags_allows_overdraft) + (= accounts_4 accounts_3) + (= transfers_4 transfers_3) + (= pending_4 pending_3) + (= replicaState_4 replicaState_3) + (= log_4 log_3) + (= commitIndex_4 commitIndex_3) + (= leader_4 leader_3) + ) + (and ; Action: CommitTransfer + (select pending_3 id) + (select transfers_keys id) + (select transfers_3 id).pending_3 = true + (= accounts_4 accounts_3) + (= transfers_4 transfers_3) + (= pending_4 pending_3) + (= replicaState_4 replicaState_3) + (= log_4 log_3) + (= commitIndex_4 commitIndex_3) + (= leader_4 leader_3) + ) + (and ; Action: VoidTransfer + (select pending_3 id) + (select transfers_keys id) + (select transfers_3 id).pending_3 = true + (= accounts_4 accounts_3) + (= transfers_4 transfers_3) + (= pending_4 pending_3) + (= replicaState_4 replicaState_3) + (= log_4 log_3) + (= commitIndex_4 commitIndex_3) + (= leader_4 leader_3) + ) + (and ; Action: PostTransfer + t_id notIn transfers_keys + (select accounts_keys t_from) + (select accounts_keys t_to) + t_from distinct t_to + (or (select accounts_3 t_from).balance >= t_amount (select accounts_3 t_from).flags_allows_overdraft) + (= accounts_4 accounts_3) + (= transfers_4 transfers_3) + (= pending_4 pending_3) + (= replicaState_4 replicaState_3) + (= log_4 log_3) + (= commitIndex_4 commitIndex_3) + (= leader_4 leader_3) + ) + (and ; Action: BecomeLeader + (select replicaState_keys replica) + (select replicaState_3 replica).role = "candidate" + (< (select replicaState_3 replica).currentTerm term) + (= accounts_4 accounts_3) + (= transfers_4 transfers_3) + (= pending_4 pending_3) + (= replicaState_4 replicaState_3) + (= log_4 log_3) + (= commitIndex_4 commitIndex_3) + (= leader_4 leader_3) + ) + (and ; Action: AppendEntry + (+ entry_index = length(log_3) 1) + term >= commitIndex_3 + (= accounts_4 accounts_3) + (= transfers_4 transfers_3) + (= pending_4 pending_3) + (= replicaState_4 replicaState_3) + (= log_4 log_3) + (= commitIndex_4 commitIndex_3) + (= leader_4 leader_3) + ) + ; Stuttering + (and + (= accounts_4 accounts_3) + (= transfers_4 transfers_3) + (= pending_4 pending_3) + (= replicaState_4 replicaState_3) + (= log_4 log_3) + (= commitIndex_4 commitIndex_3) + (= leader_4 leader_3) + ) + ) +) +(assert ; Step 4 → 5 + (or + (and ; Action: CreateTransfer + t_id notIn transfers_keys + (select accounts_keys t_from) + (select accounts_keys t_to) + t_from distinct t_to + (or (select accounts_4 t_from).balance >= t_amount (select accounts_4 t_from).flags_allows_overdraft) + (= accounts_5 accounts_4) + (= transfers_5 transfers_4) + (= pending_5 pending_4) + (= replicaState_5 replicaState_4) + (= log_5 log_4) + (= commitIndex_5 commitIndex_4) + (= leader_5 leader_4) + ) + (and ; Action: CommitTransfer + (select pending_4 id) + (select transfers_keys id) + (select transfers_4 id).pending_4 = true + (= accounts_5 accounts_4) + (= transfers_5 transfers_4) + (= pending_5 pending_4) + (= replicaState_5 replicaState_4) + (= log_5 log_4) + (= commitIndex_5 commitIndex_4) + (= leader_5 leader_4) + ) + (and ; Action: VoidTransfer + (select pending_4 id) + (select transfers_keys id) + (select transfers_4 id).pending_4 = true + (= accounts_5 accounts_4) + (= transfers_5 transfers_4) + (= pending_5 pending_4) + (= replicaState_5 replicaState_4) + (= log_5 log_4) + (= commitIndex_5 commitIndex_4) + (= leader_5 leader_4) + ) + (and ; Action: PostTransfer + t_id notIn transfers_keys + (select accounts_keys t_from) + (select accounts_keys t_to) + t_from distinct t_to + (or (select accounts_4 t_from).balance >= t_amount (select accounts_4 t_from).flags_allows_overdraft) + (= accounts_5 accounts_4) + (= transfers_5 transfers_4) + (= pending_5 pending_4) + (= replicaState_5 replicaState_4) + (= log_5 log_4) + (= commitIndex_5 commitIndex_4) + (= leader_5 leader_4) + ) + (and ; Action: BecomeLeader + (select replicaState_keys replica) + (select replicaState_4 replica).role = "candidate" + (< (select replicaState_4 replica).currentTerm term) + (= accounts_5 accounts_4) + (= transfers_5 transfers_4) + (= pending_5 pending_4) + (= replicaState_5 replicaState_4) + (= log_5 log_4) + (= commitIndex_5 commitIndex_4) + (= leader_5 leader_4) + ) + (and ; Action: AppendEntry + (+ entry_index = length(log_4) 1) + term >= commitIndex_4 + (= accounts_5 accounts_4) + (= transfers_5 transfers_4) + (= pending_5 pending_4) + (= replicaState_5 replicaState_4) + (= log_5 log_4) + (= commitIndex_5 commitIndex_4) + (= leader_5 leader_4) + ) + ; Stuttering + (and + (= accounts_5 accounts_4) + (= transfers_5 transfers_4) + (= pending_5 pending_4) + (= replicaState_5 replicaState_4) + (= log_5 log_4) + (= commitIndex_5 commitIndex_4) + (= leader_5 leader_4) + ) + ) +) +(assert ; Step 5 → 6 + (or + (and ; Action: CreateTransfer + t_id notIn transfers_keys + (select accounts_keys t_from) + (select accounts_keys t_to) + t_from distinct t_to + (or (select accounts_5 t_from).balance >= t_amount (select accounts_5 t_from).flags_allows_overdraft) + (= accounts_6 accounts_5) + (= transfers_6 transfers_5) + (= pending_6 pending_5) + (= replicaState_6 replicaState_5) + (= log_6 log_5) + (= commitIndex_6 commitIndex_5) + (= leader_6 leader_5) + ) + (and ; Action: CommitTransfer + (select pending_5 id) + (select transfers_keys id) + (select transfers_5 id).pending_5 = true + (= accounts_6 accounts_5) + (= transfers_6 transfers_5) + (= pending_6 pending_5) + (= replicaState_6 replicaState_5) + (= log_6 log_5) + (= commitIndex_6 commitIndex_5) + (= leader_6 leader_5) + ) + (and ; Action: VoidTransfer + (select pending_5 id) + (select transfers_keys id) + (select transfers_5 id).pending_5 = true + (= accounts_6 accounts_5) + (= transfers_6 transfers_5) + (= pending_6 pending_5) + (= replicaState_6 replicaState_5) + (= log_6 log_5) + (= commitIndex_6 commitIndex_5) + (= leader_6 leader_5) + ) + (and ; Action: PostTransfer + t_id notIn transfers_keys + (select accounts_keys t_from) + (select accounts_keys t_to) + t_from distinct t_to + (or (select accounts_5 t_from).balance >= t_amount (select accounts_5 t_from).flags_allows_overdraft) + (= accounts_6 accounts_5) + (= transfers_6 transfers_5) + (= pending_6 pending_5) + (= replicaState_6 replicaState_5) + (= log_6 log_5) + (= commitIndex_6 commitIndex_5) + (= leader_6 leader_5) + ) + (and ; Action: BecomeLeader + (select replicaState_keys replica) + (select replicaState_5 replica).role = "candidate" + (< (select replicaState_5 replica).currentTerm term) + (= accounts_6 accounts_5) + (= transfers_6 transfers_5) + (= pending_6 pending_5) + (= replicaState_6 replicaState_5) + (= log_6 log_5) + (= commitIndex_6 commitIndex_5) + (= leader_6 leader_5) + ) + (and ; Action: AppendEntry + (+ entry_index = length(log_5) 1) + term >= commitIndex_5 + (= accounts_6 accounts_5) + (= transfers_6 transfers_5) + (= pending_6 pending_5) + (= replicaState_6 replicaState_5) + (= log_6 log_5) + (= commitIndex_6 commitIndex_5) + (= leader_6 leader_5) + ) + ; Stuttering + (and + (= accounts_6 accounts_5) + (= transfers_6 transfers_5) + (= pending_6 pending_5) + (= replicaState_6 replicaState_5) + (= log_6 log_5) + (= commitIndex_6 commitIndex_5) + (= leader_6 leader_5) + ) + ) +) +(assert ; Step 6 → 7 + (or + (and ; Action: CreateTransfer + t_id notIn transfers_keys + (select accounts_keys t_from) + (select accounts_keys t_to) + t_from distinct t_to + (or (select accounts_6 t_from).balance >= t_amount (select accounts_6 t_from).flags_allows_overdraft) + (= accounts_7 accounts_6) + (= transfers_7 transfers_6) + (= pending_7 pending_6) + (= replicaState_7 replicaState_6) + (= log_7 log_6) + (= commitIndex_7 commitIndex_6) + (= leader_7 leader_6) + ) + (and ; Action: CommitTransfer + (select pending_6 id) + (select transfers_keys id) + (select transfers_6 id).pending_6 = true + (= accounts_7 accounts_6) + (= transfers_7 transfers_6) + (= pending_7 pending_6) + (= replicaState_7 replicaState_6) + (= log_7 log_6) + (= commitIndex_7 commitIndex_6) + (= leader_7 leader_6) + ) + (and ; Action: VoidTransfer + (select pending_6 id) + (select transfers_keys id) + (select transfers_6 id).pending_6 = true + (= accounts_7 accounts_6) + (= transfers_7 transfers_6) + (= pending_7 pending_6) + (= replicaState_7 replicaState_6) + (= log_7 log_6) + (= commitIndex_7 commitIndex_6) + (= leader_7 leader_6) + ) + (and ; Action: PostTransfer + t_id notIn transfers_keys + (select accounts_keys t_from) + (select accounts_keys t_to) + t_from distinct t_to + (or (select accounts_6 t_from).balance >= t_amount (select accounts_6 t_from).flags_allows_overdraft) + (= accounts_7 accounts_6) + (= transfers_7 transfers_6) + (= pending_7 pending_6) + (= replicaState_7 replicaState_6) + (= log_7 log_6) + (= commitIndex_7 commitIndex_6) + (= leader_7 leader_6) + ) + (and ; Action: BecomeLeader + (select replicaState_keys replica) + (select replicaState_6 replica).role = "candidate" + (< (select replicaState_6 replica).currentTerm term) + (= accounts_7 accounts_6) + (= transfers_7 transfers_6) + (= pending_7 pending_6) + (= replicaState_7 replicaState_6) + (= log_7 log_6) + (= commitIndex_7 commitIndex_6) + (= leader_7 leader_6) + ) + (and ; Action: AppendEntry + (+ entry_index = length(log_6) 1) + term >= commitIndex_6 + (= accounts_7 accounts_6) + (= transfers_7 transfers_6) + (= pending_7 pending_6) + (= replicaState_7 replicaState_6) + (= log_7 log_6) + (= commitIndex_7 commitIndex_6) + (= leader_7 leader_6) + ) + ; Stuttering + (and + (= accounts_7 accounts_6) + (= transfers_7 transfers_6) + (= pending_7 pending_6) + (= replicaState_7 replicaState_6) + (= log_7 log_6) + (= commitIndex_7 commitIndex_6) + (= leader_7 leader_6) + ) + ) +) +(assert ; Step 7 → 8 + (or + (and ; Action: CreateTransfer + t_id notIn transfers_keys + (select accounts_keys t_from) + (select accounts_keys t_to) + t_from distinct t_to + (or (select accounts_7 t_from).balance >= t_amount (select accounts_7 t_from).flags_allows_overdraft) + (= accounts_8 accounts_7) + (= transfers_8 transfers_7) + (= pending_8 pending_7) + (= replicaState_8 replicaState_7) + (= log_8 log_7) + (= commitIndex_8 commitIndex_7) + (= leader_8 leader_7) + ) + (and ; Action: CommitTransfer + (select pending_7 id) + (select transfers_keys id) + (select transfers_7 id).pending_7 = true + (= accounts_8 accounts_7) + (= transfers_8 transfers_7) + (= pending_8 pending_7) + (= replicaState_8 replicaState_7) + (= log_8 log_7) + (= commitIndex_8 commitIndex_7) + (= leader_8 leader_7) + ) + (and ; Action: VoidTransfer + (select pending_7 id) + (select transfers_keys id) + (select transfers_7 id).pending_7 = true + (= accounts_8 accounts_7) + (= transfers_8 transfers_7) + (= pending_8 pending_7) + (= replicaState_8 replicaState_7) + (= log_8 log_7) + (= commitIndex_8 commitIndex_7) + (= leader_8 leader_7) + ) + (and ; Action: PostTransfer + t_id notIn transfers_keys + (select accounts_keys t_from) + (select accounts_keys t_to) + t_from distinct t_to + (or (select accounts_7 t_from).balance >= t_amount (select accounts_7 t_from).flags_allows_overdraft) + (= accounts_8 accounts_7) + (= transfers_8 transfers_7) + (= pending_8 pending_7) + (= replicaState_8 replicaState_7) + (= log_8 log_7) + (= commitIndex_8 commitIndex_7) + (= leader_8 leader_7) + ) + (and ; Action: BecomeLeader + (select replicaState_keys replica) + (select replicaState_7 replica).role = "candidate" + (< (select replicaState_7 replica).currentTerm term) + (= accounts_8 accounts_7) + (= transfers_8 transfers_7) + (= pending_8 pending_7) + (= replicaState_8 replicaState_7) + (= log_8 log_7) + (= commitIndex_8 commitIndex_7) + (= leader_8 leader_7) + ) + (and ; Action: AppendEntry + (+ entry_index = length(log_7) 1) + term >= commitIndex_7 + (= accounts_8 accounts_7) + (= transfers_8 transfers_7) + (= pending_8 pending_7) + (= replicaState_8 replicaState_7) + (= log_8 log_7) + (= commitIndex_8 commitIndex_7) + (= leader_8 leader_7) + ) + ; Stuttering + (and + (= accounts_8 accounts_7) + (= transfers_8 transfers_7) + (= pending_8 pending_7) + (= replicaState_8 replicaState_7) + (= log_8 log_7) + (= commitIndex_8 commitIndex_7) + (= leader_8 leader_7) + ) + ) +) +(assert ; Step 8 → 9 + (or + (and ; Action: CreateTransfer + t_id notIn transfers_keys + (select accounts_keys t_from) + (select accounts_keys t_to) + t_from distinct t_to + (or (select accounts_8 t_from).balance >= t_amount (select accounts_8 t_from).flags_allows_overdraft) + (= accounts_9 accounts_8) + (= transfers_9 transfers_8) + (= pending_9 pending_8) + (= replicaState_9 replicaState_8) + (= log_9 log_8) + (= commitIndex_9 commitIndex_8) + (= leader_9 leader_8) + ) + (and ; Action: CommitTransfer + (select pending_8 id) + (select transfers_keys id) + (select transfers_8 id).pending_8 = true + (= accounts_9 accounts_8) + (= transfers_9 transfers_8) + (= pending_9 pending_8) + (= replicaState_9 replicaState_8) + (= log_9 log_8) + (= commitIndex_9 commitIndex_8) + (= leader_9 leader_8) + ) + (and ; Action: VoidTransfer + (select pending_8 id) + (select transfers_keys id) + (select transfers_8 id).pending_8 = true + (= accounts_9 accounts_8) + (= transfers_9 transfers_8) + (= pending_9 pending_8) + (= replicaState_9 replicaState_8) + (= log_9 log_8) + (= commitIndex_9 commitIndex_8) + (= leader_9 leader_8) + ) + (and ; Action: PostTransfer + t_id notIn transfers_keys + (select accounts_keys t_from) + (select accounts_keys t_to) + t_from distinct t_to + (or (select accounts_8 t_from).balance >= t_amount (select accounts_8 t_from).flags_allows_overdraft) + (= accounts_9 accounts_8) + (= transfers_9 transfers_8) + (= pending_9 pending_8) + (= replicaState_9 replicaState_8) + (= log_9 log_8) + (= commitIndex_9 commitIndex_8) + (= leader_9 leader_8) + ) + (and ; Action: BecomeLeader + (select replicaState_keys replica) + (select replicaState_8 replica).role = "candidate" + (< (select replicaState_8 replica).currentTerm term) + (= accounts_9 accounts_8) + (= transfers_9 transfers_8) + (= pending_9 pending_8) + (= replicaState_9 replicaState_8) + (= log_9 log_8) + (= commitIndex_9 commitIndex_8) + (= leader_9 leader_8) + ) + (and ; Action: AppendEntry + (+ entry_index = length(log_8) 1) + term >= commitIndex_8 + (= accounts_9 accounts_8) + (= transfers_9 transfers_8) + (= pending_9 pending_8) + (= replicaState_9 replicaState_8) + (= log_9 log_8) + (= commitIndex_9 commitIndex_8) + (= leader_9 leader_8) + ) + ; Stuttering + (and + (= accounts_9 accounts_8) + (= transfers_9 transfers_8) + (= pending_9 pending_8) + (= replicaState_9 replicaState_8) + (= log_9 log_8) + (= commitIndex_9 commitIndex_8) + (= leader_9 leader_8) + ) + ) +) +(assert ; Step 9 → 10 + (or + (and ; Action: CreateTransfer + t_id notIn transfers_keys + (select accounts_keys t_from) + (select accounts_keys t_to) + t_from distinct t_to + (or (select accounts_9 t_from).balance >= t_amount (select accounts_9 t_from).flags_allows_overdraft) + (= accounts_10 accounts_9) + (= transfers_10 transfers_9) + (= pending_10 pending_9) + (= replicaState_10 replicaState_9) + (= log_10 log_9) + (= commitIndex_10 commitIndex_9) + (= leader_10 leader_9) + ) + (and ; Action: CommitTransfer + (select pending_9 id) + (select transfers_keys id) + (select transfers_9 id).pending_9 = true + (= accounts_10 accounts_9) + (= transfers_10 transfers_9) + (= pending_10 pending_9) + (= replicaState_10 replicaState_9) + (= log_10 log_9) + (= commitIndex_10 commitIndex_9) + (= leader_10 leader_9) + ) + (and ; Action: VoidTransfer + (select pending_9 id) + (select transfers_keys id) + (select transfers_9 id).pending_9 = true + (= accounts_10 accounts_9) + (= transfers_10 transfers_9) + (= pending_10 pending_9) + (= replicaState_10 replicaState_9) + (= log_10 log_9) + (= commitIndex_10 commitIndex_9) + (= leader_10 leader_9) + ) + (and ; Action: PostTransfer + t_id notIn transfers_keys + (select accounts_keys t_from) + (select accounts_keys t_to) + t_from distinct t_to + (or (select accounts_9 t_from).balance >= t_amount (select accounts_9 t_from).flags_allows_overdraft) + (= accounts_10 accounts_9) + (= transfers_10 transfers_9) + (= pending_10 pending_9) + (= replicaState_10 replicaState_9) + (= log_10 log_9) + (= commitIndex_10 commitIndex_9) + (= leader_10 leader_9) + ) + (and ; Action: BecomeLeader + (select replicaState_keys replica) + (select replicaState_9 replica).role = "candidate" + (< (select replicaState_9 replica).currentTerm term) + (= accounts_10 accounts_9) + (= transfers_10 transfers_9) + (= pending_10 pending_9) + (= replicaState_10 replicaState_9) + (= log_10 log_9) + (= commitIndex_10 commitIndex_9) + (= leader_10 leader_9) + ) + (and ; Action: AppendEntry + (+ entry_index = length(log_9) 1) + term >= commitIndex_9 + (= accounts_10 accounts_9) + (= transfers_10 transfers_9) + (= pending_10 pending_9) + (= replicaState_10 replicaState_9) + (= log_10 log_9) + (= commitIndex_10 commitIndex_9) + (= leader_10 leader_9) + ) + ; Stuttering + (and + (= accounts_10 accounts_9) + (= transfers_10 transfers_9) + (= pending_10 pending_9) + (= replicaState_10 replicaState_9) + (= log_10 log_9) + (= commitIndex_10 commitIndex_9) + (= leader_10 leader_9) + ) + ) +) + +; Property assertion: not(invariant at some step) +(assert + (or + (not (AccountBalanceInvariant_0)) + (not (AccountBalanceInvariant_1)) + (not (AccountBalanceInvariant_2)) + (not (AccountBalanceInvariant_3)) + (not (AccountBalanceInvariant_4)) + (not (AccountBalanceInvariant_5)) + (not (AccountBalanceInvariant_6)) + (not (AccountBalanceInvariant_7)) + (not (AccountBalanceInvariant_8)) + (not (AccountBalanceInvariant_9)) + (not (AccountBalanceInvariant_10)) + ) +) +(define-fun AccountBalanceInvariant_0 () Bool + (and + (forall ((a Account)) (- a_balance = a_credits_posted a_debits_posted)) + (forall ((a Account)) a_debits_pending >= 0 a_credits_pending >= 0) + ) +) +(define-fun AccountBalanceInvariant_1 () Bool + (and + (forall ((a Account)) (- a_balance = a_credits_posted a_debits_posted)) + (forall ((a Account)) a_debits_pending >= 0 a_credits_pending >= 0) + ) +) +(define-fun AccountBalanceInvariant_2 () Bool + (and + (forall ((a Account)) (- a_balance = a_credits_posted a_debits_posted)) + (forall ((a Account)) a_debits_pending >= 0 a_credits_pending >= 0) + ) +) +(define-fun AccountBalanceInvariant_3 () Bool + (and + (forall ((a Account)) (- a_balance = a_credits_posted a_debits_posted)) + (forall ((a Account)) a_debits_pending >= 0 a_credits_pending >= 0) + ) +) +(define-fun AccountBalanceInvariant_4 () Bool + (and + (forall ((a Account)) (- a_balance = a_credits_posted a_debits_posted)) + (forall ((a Account)) a_debits_pending >= 0 a_credits_pending >= 0) + ) +) +(define-fun AccountBalanceInvariant_5 () Bool + (and + (forall ((a Account)) (- a_balance = a_credits_posted a_debits_posted)) + (forall ((a Account)) a_debits_pending >= 0 a_credits_pending >= 0) + ) +) +(define-fun AccountBalanceInvariant_6 () Bool + (and + (forall ((a Account)) (- a_balance = a_credits_posted a_debits_posted)) + (forall ((a Account)) a_debits_pending >= 0 a_credits_pending >= 0) + ) +) +(define-fun AccountBalanceInvariant_7 () Bool + (and + (forall ((a Account)) (- a_balance = a_credits_posted a_debits_posted)) + (forall ((a Account)) a_debits_pending >= 0 a_credits_pending >= 0) + ) +) +(define-fun AccountBalanceInvariant_8 () Bool + (and + (forall ((a Account)) (- a_balance = a_credits_posted a_debits_posted)) + (forall ((a Account)) a_debits_pending >= 0 a_credits_pending >= 0) + ) +) +(define-fun AccountBalanceInvariant_9 () Bool + (and + (forall ((a Account)) (- a_balance = a_credits_posted a_debits_posted)) + (forall ((a Account)) a_debits_pending >= 0 a_credits_pending >= 0) + ) +) +(define-fun AccountBalanceInvariant_10 () Bool + (and + (forall ((a Account)) (- a_balance = a_credits_posted a_debits_posted)) + (forall ((a Account)) a_debits_pending >= 0 a_credits_pending >= 0) + ) +) + +(echo "Checking: Always(AccountBalanceInvariant) for 10 steps") +(check-sat) +(get-model) +; Verification: Always(NoOverdraft) +; BMC depth: 10 + +; Declare state copies for 10 steps +(declare-const accounts_0 (Array Int Account)) +(declare-const accounts_1 (Array Int Account)) +(declare-const accounts_2 (Array Int Account)) +(declare-const accounts_3 (Array Int Account)) +(declare-const accounts_4 (Array Int Account)) +(declare-const accounts_5 (Array Int Account)) +(declare-const accounts_6 (Array Int Account)) +(declare-const accounts_7 (Array Int Account)) +(declare-const accounts_8 (Array Int Account)) +(declare-const accounts_9 (Array Int Account)) +(declare-const accounts_10 (Array Int Account)) +(declare-const transfers_0 (Array Int Transfer)) +(declare-const transfers_1 (Array Int Transfer)) +(declare-const transfers_2 (Array Int Transfer)) +(declare-const transfers_3 (Array Int Transfer)) +(declare-const transfers_4 (Array Int Transfer)) +(declare-const transfers_5 (Array Int Transfer)) +(declare-const transfers_6 (Array Int Transfer)) +(declare-const transfers_7 (Array Int Transfer)) +(declare-const transfers_8 (Array Int Transfer)) +(declare-const transfers_9 (Array Int Transfer)) +(declare-const transfers_10 (Array Int Transfer)) +(declare-const pending_0 (Array Int Bool)) +(declare-const pending_1 (Array Int Bool)) +(declare-const pending_2 (Array Int Bool)) +(declare-const pending_3 (Array Int Bool)) +(declare-const pending_4 (Array Int Bool)) +(declare-const pending_5 (Array Int Bool)) +(declare-const pending_6 (Array Int Bool)) +(declare-const pending_7 (Array Int Bool)) +(declare-const pending_8 (Array Int Bool)) +(declare-const pending_9 (Array Int Bool)) +(declare-const pending_10 (Array Int Bool)) +(declare-const replicaState_0 (Array Int Replica)) +(declare-const replicaState_1 (Array Int Replica)) +(declare-const replicaState_2 (Array Int Replica)) +(declare-const replicaState_3 (Array Int Replica)) +(declare-const replicaState_4 (Array Int Replica)) +(declare-const replicaState_5 (Array Int Replica)) +(declare-const replicaState_6 (Array Int Replica)) +(declare-const replicaState_7 (Array Int Replica)) +(declare-const replicaState_8 (Array Int Replica)) +(declare-const replicaState_9 (Array Int Replica)) +(declare-const replicaState_10 (Array Int Replica)) +(declare-const log_0 (Array Int LogEntry)) +(declare-const log_1 (Array Int LogEntry)) +(declare-const log_2 (Array Int LogEntry)) +(declare-const log_3 (Array Int LogEntry)) +(declare-const log_4 (Array Int LogEntry)) +(declare-const log_5 (Array Int LogEntry)) +(declare-const log_6 (Array Int LogEntry)) +(declare-const log_7 (Array Int LogEntry)) +(declare-const log_8 (Array Int LogEntry)) +(declare-const log_9 (Array Int LogEntry)) +(declare-const log_10 (Array Int LogEntry)) +(declare-const commitIndex_0 Int) +(declare-const commitIndex_1 Int) +(declare-const commitIndex_2 Int) +(declare-const commitIndex_3 Int) +(declare-const commitIndex_4 Int) +(declare-const commitIndex_5 Int) +(declare-const commitIndex_6 Int) +(declare-const commitIndex_7 Int) +(declare-const commitIndex_8 Int) +(declare-const commitIndex_9 Int) +(declare-const commitIndex_10 Int) +(declare-const leader_0 Int) +(declare-const leader_1 Int) +(declare-const leader_2 Int) +(declare-const leader_3 Int) +(declare-const leader_4 Int) +(declare-const leader_5 Int) +(declare-const leader_6 Int) +(declare-const leader_7 Int) +(declare-const leader_8 Int) +(declare-const leader_9 Int) +(declare-const leader_10 Int) + +; Initial state constraints +(assert + (and + (>= commitIndex_0 0) + (>= leader_0 0) + ) +) + +; Transition constraints +(assert ; Step 0 → 1 + (or + (and ; Action: CreateTransfer + t_id notIn transfers_keys + (select accounts_keys t_from) + (select accounts_keys t_to) + t_from distinct t_to + (or (select accounts_0 t_from).balance >= t_amount (select accounts_0 t_from).flags_allows_overdraft) + (= accounts_1 accounts_0) + (= transfers_1 transfers_0) + (= pending_1 pending_0) + (= replicaState_1 replicaState_0) + (= log_1 log_0) + (= commitIndex_1 commitIndex_0) + (= leader_1 leader_0) + ) + (and ; Action: CommitTransfer + (select pending_0 id) + (select transfers_keys id) + (select transfers_0 id).pending_0 = true + (= accounts_1 accounts_0) + (= transfers_1 transfers_0) + (= pending_1 pending_0) + (= replicaState_1 replicaState_0) + (= log_1 log_0) + (= commitIndex_1 commitIndex_0) + (= leader_1 leader_0) + ) + (and ; Action: VoidTransfer + (select pending_0 id) + (select transfers_keys id) + (select transfers_0 id).pending_0 = true + (= accounts_1 accounts_0) + (= transfers_1 transfers_0) + (= pending_1 pending_0) + (= replicaState_1 replicaState_0) + (= log_1 log_0) + (= commitIndex_1 commitIndex_0) + (= leader_1 leader_0) + ) + (and ; Action: PostTransfer + t_id notIn transfers_keys + (select accounts_keys t_from) + (select accounts_keys t_to) + t_from distinct t_to + (or (select accounts_0 t_from).balance >= t_amount (select accounts_0 t_from).flags_allows_overdraft) + (= accounts_1 accounts_0) + (= transfers_1 transfers_0) + (= pending_1 pending_0) + (= replicaState_1 replicaState_0) + (= log_1 log_0) + (= commitIndex_1 commitIndex_0) + (= leader_1 leader_0) + ) + (and ; Action: BecomeLeader + (select replicaState_keys replica) + (select replicaState_0 replica).role = "candidate" + (< (select replicaState_0 replica).currentTerm term) + (= accounts_1 accounts_0) + (= transfers_1 transfers_0) + (= pending_1 pending_0) + (= replicaState_1 replicaState_0) + (= log_1 log_0) + (= commitIndex_1 commitIndex_0) + (= leader_1 leader_0) + ) + (and ; Action: AppendEntry + (+ entry_index = length(log_0) 1) + term >= commitIndex_0 + (= accounts_1 accounts_0) + (= transfers_1 transfers_0) + (= pending_1 pending_0) + (= replicaState_1 replicaState_0) + (= log_1 log_0) + (= commitIndex_1 commitIndex_0) + (= leader_1 leader_0) + ) + ; Stuttering + (and + (= accounts_1 accounts_0) + (= transfers_1 transfers_0) + (= pending_1 pending_0) + (= replicaState_1 replicaState_0) + (= log_1 log_0) + (= commitIndex_1 commitIndex_0) + (= leader_1 leader_0) + ) + ) +) +(assert ; Step 1 → 2 + (or + (and ; Action: CreateTransfer + t_id notIn transfers_keys + (select accounts_keys t_from) + (select accounts_keys t_to) + t_from distinct t_to + (or (select accounts_1 t_from).balance >= t_amount (select accounts_1 t_from).flags_allows_overdraft) + (= accounts_2 accounts_1) + (= transfers_2 transfers_1) + (= pending_2 pending_1) + (= replicaState_2 replicaState_1) + (= log_2 log_1) + (= commitIndex_2 commitIndex_1) + (= leader_2 leader_1) + ) + (and ; Action: CommitTransfer + (select pending_1 id) + (select transfers_keys id) + (select transfers_1 id).pending_1 = true + (= accounts_2 accounts_1) + (= transfers_2 transfers_1) + (= pending_2 pending_1) + (= replicaState_2 replicaState_1) + (= log_2 log_1) + (= commitIndex_2 commitIndex_1) + (= leader_2 leader_1) + ) + (and ; Action: VoidTransfer + (select pending_1 id) + (select transfers_keys id) + (select transfers_1 id).pending_1 = true + (= accounts_2 accounts_1) + (= transfers_2 transfers_1) + (= pending_2 pending_1) + (= replicaState_2 replicaState_1) + (= log_2 log_1) + (= commitIndex_2 commitIndex_1) + (= leader_2 leader_1) + ) + (and ; Action: PostTransfer + t_id notIn transfers_keys + (select accounts_keys t_from) + (select accounts_keys t_to) + t_from distinct t_to + (or (select accounts_1 t_from).balance >= t_amount (select accounts_1 t_from).flags_allows_overdraft) + (= accounts_2 accounts_1) + (= transfers_2 transfers_1) + (= pending_2 pending_1) + (= replicaState_2 replicaState_1) + (= log_2 log_1) + (= commitIndex_2 commitIndex_1) + (= leader_2 leader_1) + ) + (and ; Action: BecomeLeader + (select replicaState_keys replica) + (select replicaState_1 replica).role = "candidate" + (< (select replicaState_1 replica).currentTerm term) + (= accounts_2 accounts_1) + (= transfers_2 transfers_1) + (= pending_2 pending_1) + (= replicaState_2 replicaState_1) + (= log_2 log_1) + (= commitIndex_2 commitIndex_1) + (= leader_2 leader_1) + ) + (and ; Action: AppendEntry + (+ entry_index = length(log_1) 1) + term >= commitIndex_1 + (= accounts_2 accounts_1) + (= transfers_2 transfers_1) + (= pending_2 pending_1) + (= replicaState_2 replicaState_1) + (= log_2 log_1) + (= commitIndex_2 commitIndex_1) + (= leader_2 leader_1) + ) + ; Stuttering + (and + (= accounts_2 accounts_1) + (= transfers_2 transfers_1) + (= pending_2 pending_1) + (= replicaState_2 replicaState_1) + (= log_2 log_1) + (= commitIndex_2 commitIndex_1) + (= leader_2 leader_1) + ) + ) +) +(assert ; Step 2 → 3 + (or + (and ; Action: CreateTransfer + t_id notIn transfers_keys + (select accounts_keys t_from) + (select accounts_keys t_to) + t_from distinct t_to + (or (select accounts_2 t_from).balance >= t_amount (select accounts_2 t_from).flags_allows_overdraft) + (= accounts_3 accounts_2) + (= transfers_3 transfers_2) + (= pending_3 pending_2) + (= replicaState_3 replicaState_2) + (= log_3 log_2) + (= commitIndex_3 commitIndex_2) + (= leader_3 leader_2) + ) + (and ; Action: CommitTransfer + (select pending_2 id) + (select transfers_keys id) + (select transfers_2 id).pending_2 = true + (= accounts_3 accounts_2) + (= transfers_3 transfers_2) + (= pending_3 pending_2) + (= replicaState_3 replicaState_2) + (= log_3 log_2) + (= commitIndex_3 commitIndex_2) + (= leader_3 leader_2) + ) + (and ; Action: VoidTransfer + (select pending_2 id) + (select transfers_keys id) + (select transfers_2 id).pending_2 = true + (= accounts_3 accounts_2) + (= transfers_3 transfers_2) + (= pending_3 pending_2) + (= replicaState_3 replicaState_2) + (= log_3 log_2) + (= commitIndex_3 commitIndex_2) + (= leader_3 leader_2) + ) + (and ; Action: PostTransfer + t_id notIn transfers_keys + (select accounts_keys t_from) + (select accounts_keys t_to) + t_from distinct t_to + (or (select accounts_2 t_from).balance >= t_amount (select accounts_2 t_from).flags_allows_overdraft) + (= accounts_3 accounts_2) + (= transfers_3 transfers_2) + (= pending_3 pending_2) + (= replicaState_3 replicaState_2) + (= log_3 log_2) + (= commitIndex_3 commitIndex_2) + (= leader_3 leader_2) + ) + (and ; Action: BecomeLeader + (select replicaState_keys replica) + (select replicaState_2 replica).role = "candidate" + (< (select replicaState_2 replica).currentTerm term) + (= accounts_3 accounts_2) + (= transfers_3 transfers_2) + (= pending_3 pending_2) + (= replicaState_3 replicaState_2) + (= log_3 log_2) + (= commitIndex_3 commitIndex_2) + (= leader_3 leader_2) + ) + (and ; Action: AppendEntry + (+ entry_index = length(log_2) 1) + term >= commitIndex_2 + (= accounts_3 accounts_2) + (= transfers_3 transfers_2) + (= pending_3 pending_2) + (= replicaState_3 replicaState_2) + (= log_3 log_2) + (= commitIndex_3 commitIndex_2) + (= leader_3 leader_2) + ) + ; Stuttering + (and + (= accounts_3 accounts_2) + (= transfers_3 transfers_2) + (= pending_3 pending_2) + (= replicaState_3 replicaState_2) + (= log_3 log_2) + (= commitIndex_3 commitIndex_2) + (= leader_3 leader_2) + ) + ) +) +(assert ; Step 3 → 4 + (or + (and ; Action: CreateTransfer + t_id notIn transfers_keys + (select accounts_keys t_from) + (select accounts_keys t_to) + t_from distinct t_to + (or (select accounts_3 t_from).balance >= t_amount (select accounts_3 t_from).flags_allows_overdraft) + (= accounts_4 accounts_3) + (= transfers_4 transfers_3) + (= pending_4 pending_3) + (= replicaState_4 replicaState_3) + (= log_4 log_3) + (= commitIndex_4 commitIndex_3) + (= leader_4 leader_3) + ) + (and ; Action: CommitTransfer + (select pending_3 id) + (select transfers_keys id) + (select transfers_3 id).pending_3 = true + (= accounts_4 accounts_3) + (= transfers_4 transfers_3) + (= pending_4 pending_3) + (= replicaState_4 replicaState_3) + (= log_4 log_3) + (= commitIndex_4 commitIndex_3) + (= leader_4 leader_3) + ) + (and ; Action: VoidTransfer + (select pending_3 id) + (select transfers_keys id) + (select transfers_3 id).pending_3 = true + (= accounts_4 accounts_3) + (= transfers_4 transfers_3) + (= pending_4 pending_3) + (= replicaState_4 replicaState_3) + (= log_4 log_3) + (= commitIndex_4 commitIndex_3) + (= leader_4 leader_3) + ) + (and ; Action: PostTransfer + t_id notIn transfers_keys + (select accounts_keys t_from) + (select accounts_keys t_to) + t_from distinct t_to + (or (select accounts_3 t_from).balance >= t_amount (select accounts_3 t_from).flags_allows_overdraft) + (= accounts_4 accounts_3) + (= transfers_4 transfers_3) + (= pending_4 pending_3) + (= replicaState_4 replicaState_3) + (= log_4 log_3) + (= commitIndex_4 commitIndex_3) + (= leader_4 leader_3) + ) + (and ; Action: BecomeLeader + (select replicaState_keys replica) + (select replicaState_3 replica).role = "candidate" + (< (select replicaState_3 replica).currentTerm term) + (= accounts_4 accounts_3) + (= transfers_4 transfers_3) + (= pending_4 pending_3) + (= replicaState_4 replicaState_3) + (= log_4 log_3) + (= commitIndex_4 commitIndex_3) + (= leader_4 leader_3) + ) + (and ; Action: AppendEntry + (+ entry_index = length(log_3) 1) + term >= commitIndex_3 + (= accounts_4 accounts_3) + (= transfers_4 transfers_3) + (= pending_4 pending_3) + (= replicaState_4 replicaState_3) + (= log_4 log_3) + (= commitIndex_4 commitIndex_3) + (= leader_4 leader_3) + ) + ; Stuttering + (and + (= accounts_4 accounts_3) + (= transfers_4 transfers_3) + (= pending_4 pending_3) + (= replicaState_4 replicaState_3) + (= log_4 log_3) + (= commitIndex_4 commitIndex_3) + (= leader_4 leader_3) + ) + ) +) +(assert ; Step 4 → 5 + (or + (and ; Action: CreateTransfer + t_id notIn transfers_keys + (select accounts_keys t_from) + (select accounts_keys t_to) + t_from distinct t_to + (or (select accounts_4 t_from).balance >= t_amount (select accounts_4 t_from).flags_allows_overdraft) + (= accounts_5 accounts_4) + (= transfers_5 transfers_4) + (= pending_5 pending_4) + (= replicaState_5 replicaState_4) + (= log_5 log_4) + (= commitIndex_5 commitIndex_4) + (= leader_5 leader_4) + ) + (and ; Action: CommitTransfer + (select pending_4 id) + (select transfers_keys id) + (select transfers_4 id).pending_4 = true + (= accounts_5 accounts_4) + (= transfers_5 transfers_4) + (= pending_5 pending_4) + (= replicaState_5 replicaState_4) + (= log_5 log_4) + (= commitIndex_5 commitIndex_4) + (= leader_5 leader_4) + ) + (and ; Action: VoidTransfer + (select pending_4 id) + (select transfers_keys id) + (select transfers_4 id).pending_4 = true + (= accounts_5 accounts_4) + (= transfers_5 transfers_4) + (= pending_5 pending_4) + (= replicaState_5 replicaState_4) + (= log_5 log_4) + (= commitIndex_5 commitIndex_4) + (= leader_5 leader_4) + ) + (and ; Action: PostTransfer + t_id notIn transfers_keys + (select accounts_keys t_from) + (select accounts_keys t_to) + t_from distinct t_to + (or (select accounts_4 t_from).balance >= t_amount (select accounts_4 t_from).flags_allows_overdraft) + (= accounts_5 accounts_4) + (= transfers_5 transfers_4) + (= pending_5 pending_4) + (= replicaState_5 replicaState_4) + (= log_5 log_4) + (= commitIndex_5 commitIndex_4) + (= leader_5 leader_4) + ) + (and ; Action: BecomeLeader + (select replicaState_keys replica) + (select replicaState_4 replica).role = "candidate" + (< (select replicaState_4 replica).currentTerm term) + (= accounts_5 accounts_4) + (= transfers_5 transfers_4) + (= pending_5 pending_4) + (= replicaState_5 replicaState_4) + (= log_5 log_4) + (= commitIndex_5 commitIndex_4) + (= leader_5 leader_4) + ) + (and ; Action: AppendEntry + (+ entry_index = length(log_4) 1) + term >= commitIndex_4 + (= accounts_5 accounts_4) + (= transfers_5 transfers_4) + (= pending_5 pending_4) + (= replicaState_5 replicaState_4) + (= log_5 log_4) + (= commitIndex_5 commitIndex_4) + (= leader_5 leader_4) + ) + ; Stuttering + (and + (= accounts_5 accounts_4) + (= transfers_5 transfers_4) + (= pending_5 pending_4) + (= replicaState_5 replicaState_4) + (= log_5 log_4) + (= commitIndex_5 commitIndex_4) + (= leader_5 leader_4) + ) + ) +) +(assert ; Step 5 → 6 + (or + (and ; Action: CreateTransfer + t_id notIn transfers_keys + (select accounts_keys t_from) + (select accounts_keys t_to) + t_from distinct t_to + (or (select accounts_5 t_from).balance >= t_amount (select accounts_5 t_from).flags_allows_overdraft) + (= accounts_6 accounts_5) + (= transfers_6 transfers_5) + (= pending_6 pending_5) + (= replicaState_6 replicaState_5) + (= log_6 log_5) + (= commitIndex_6 commitIndex_5) + (= leader_6 leader_5) + ) + (and ; Action: CommitTransfer + (select pending_5 id) + (select transfers_keys id) + (select transfers_5 id).pending_5 = true + (= accounts_6 accounts_5) + (= transfers_6 transfers_5) + (= pending_6 pending_5) + (= replicaState_6 replicaState_5) + (= log_6 log_5) + (= commitIndex_6 commitIndex_5) + (= leader_6 leader_5) + ) + (and ; Action: VoidTransfer + (select pending_5 id) + (select transfers_keys id) + (select transfers_5 id).pending_5 = true + (= accounts_6 accounts_5) + (= transfers_6 transfers_5) + (= pending_6 pending_5) + (= replicaState_6 replicaState_5) + (= log_6 log_5) + (= commitIndex_6 commitIndex_5) + (= leader_6 leader_5) + ) + (and ; Action: PostTransfer + t_id notIn transfers_keys + (select accounts_keys t_from) + (select accounts_keys t_to) + t_from distinct t_to + (or (select accounts_5 t_from).balance >= t_amount (select accounts_5 t_from).flags_allows_overdraft) + (= accounts_6 accounts_5) + (= transfers_6 transfers_5) + (= pending_6 pending_5) + (= replicaState_6 replicaState_5) + (= log_6 log_5) + (= commitIndex_6 commitIndex_5) + (= leader_6 leader_5) + ) + (and ; Action: BecomeLeader + (select replicaState_keys replica) + (select replicaState_5 replica).role = "candidate" + (< (select replicaState_5 replica).currentTerm term) + (= accounts_6 accounts_5) + (= transfers_6 transfers_5) + (= pending_6 pending_5) + (= replicaState_6 replicaState_5) + (= log_6 log_5) + (= commitIndex_6 commitIndex_5) + (= leader_6 leader_5) + ) + (and ; Action: AppendEntry + (+ entry_index = length(log_5) 1) + term >= commitIndex_5 + (= accounts_6 accounts_5) + (= transfers_6 transfers_5) + (= pending_6 pending_5) + (= replicaState_6 replicaState_5) + (= log_6 log_5) + (= commitIndex_6 commitIndex_5) + (= leader_6 leader_5) + ) + ; Stuttering + (and + (= accounts_6 accounts_5) + (= transfers_6 transfers_5) + (= pending_6 pending_5) + (= replicaState_6 replicaState_5) + (= log_6 log_5) + (= commitIndex_6 commitIndex_5) + (= leader_6 leader_5) + ) + ) +) +(assert ; Step 6 → 7 + (or + (and ; Action: CreateTransfer + t_id notIn transfers_keys + (select accounts_keys t_from) + (select accounts_keys t_to) + t_from distinct t_to + (or (select accounts_6 t_from).balance >= t_amount (select accounts_6 t_from).flags_allows_overdraft) + (= accounts_7 accounts_6) + (= transfers_7 transfers_6) + (= pending_7 pending_6) + (= replicaState_7 replicaState_6) + (= log_7 log_6) + (= commitIndex_7 commitIndex_6) + (= leader_7 leader_6) + ) + (and ; Action: CommitTransfer + (select pending_6 id) + (select transfers_keys id) + (select transfers_6 id).pending_6 = true + (= accounts_7 accounts_6) + (= transfers_7 transfers_6) + (= pending_7 pending_6) + (= replicaState_7 replicaState_6) + (= log_7 log_6) + (= commitIndex_7 commitIndex_6) + (= leader_7 leader_6) + ) + (and ; Action: VoidTransfer + (select pending_6 id) + (select transfers_keys id) + (select transfers_6 id).pending_6 = true + (= accounts_7 accounts_6) + (= transfers_7 transfers_6) + (= pending_7 pending_6) + (= replicaState_7 replicaState_6) + (= log_7 log_6) + (= commitIndex_7 commitIndex_6) + (= leader_7 leader_6) + ) + (and ; Action: PostTransfer + t_id notIn transfers_keys + (select accounts_keys t_from) + (select accounts_keys t_to) + t_from distinct t_to + (or (select accounts_6 t_from).balance >= t_amount (select accounts_6 t_from).flags_allows_overdraft) + (= accounts_7 accounts_6) + (= transfers_7 transfers_6) + (= pending_7 pending_6) + (= replicaState_7 replicaState_6) + (= log_7 log_6) + (= commitIndex_7 commitIndex_6) + (= leader_7 leader_6) + ) + (and ; Action: BecomeLeader + (select replicaState_keys replica) + (select replicaState_6 replica).role = "candidate" + (< (select replicaState_6 replica).currentTerm term) + (= accounts_7 accounts_6) + (= transfers_7 transfers_6) + (= pending_7 pending_6) + (= replicaState_7 replicaState_6) + (= log_7 log_6) + (= commitIndex_7 commitIndex_6) + (= leader_7 leader_6) + ) + (and ; Action: AppendEntry + (+ entry_index = length(log_6) 1) + term >= commitIndex_6 + (= accounts_7 accounts_6) + (= transfers_7 transfers_6) + (= pending_7 pending_6) + (= replicaState_7 replicaState_6) + (= log_7 log_6) + (= commitIndex_7 commitIndex_6) + (= leader_7 leader_6) + ) + ; Stuttering + (and + (= accounts_7 accounts_6) + (= transfers_7 transfers_6) + (= pending_7 pending_6) + (= replicaState_7 replicaState_6) + (= log_7 log_6) + (= commitIndex_7 commitIndex_6) + (= leader_7 leader_6) + ) + ) +) +(assert ; Step 7 → 8 + (or + (and ; Action: CreateTransfer + t_id notIn transfers_keys + (select accounts_keys t_from) + (select accounts_keys t_to) + t_from distinct t_to + (or (select accounts_7 t_from).balance >= t_amount (select accounts_7 t_from).flags_allows_overdraft) + (= accounts_8 accounts_7) + (= transfers_8 transfers_7) + (= pending_8 pending_7) + (= replicaState_8 replicaState_7) + (= log_8 log_7) + (= commitIndex_8 commitIndex_7) + (= leader_8 leader_7) + ) + (and ; Action: CommitTransfer + (select pending_7 id) + (select transfers_keys id) + (select transfers_7 id).pending_7 = true + (= accounts_8 accounts_7) + (= transfers_8 transfers_7) + (= pending_8 pending_7) + (= replicaState_8 replicaState_7) + (= log_8 log_7) + (= commitIndex_8 commitIndex_7) + (= leader_8 leader_7) + ) + (and ; Action: VoidTransfer + (select pending_7 id) + (select transfers_keys id) + (select transfers_7 id).pending_7 = true + (= accounts_8 accounts_7) + (= transfers_8 transfers_7) + (= pending_8 pending_7) + (= replicaState_8 replicaState_7) + (= log_8 log_7) + (= commitIndex_8 commitIndex_7) + (= leader_8 leader_7) + ) + (and ; Action: PostTransfer + t_id notIn transfers_keys + (select accounts_keys t_from) + (select accounts_keys t_to) + t_from distinct t_to + (or (select accounts_7 t_from).balance >= t_amount (select accounts_7 t_from).flags_allows_overdraft) + (= accounts_8 accounts_7) + (= transfers_8 transfers_7) + (= pending_8 pending_7) + (= replicaState_8 replicaState_7) + (= log_8 log_7) + (= commitIndex_8 commitIndex_7) + (= leader_8 leader_7) + ) + (and ; Action: BecomeLeader + (select replicaState_keys replica) + (select replicaState_7 replica).role = "candidate" + (< (select replicaState_7 replica).currentTerm term) + (= accounts_8 accounts_7) + (= transfers_8 transfers_7) + (= pending_8 pending_7) + (= replicaState_8 replicaState_7) + (= log_8 log_7) + (= commitIndex_8 commitIndex_7) + (= leader_8 leader_7) + ) + (and ; Action: AppendEntry + (+ entry_index = length(log_7) 1) + term >= commitIndex_7 + (= accounts_8 accounts_7) + (= transfers_8 transfers_7) + (= pending_8 pending_7) + (= replicaState_8 replicaState_7) + (= log_8 log_7) + (= commitIndex_8 commitIndex_7) + (= leader_8 leader_7) + ) + ; Stuttering + (and + (= accounts_8 accounts_7) + (= transfers_8 transfers_7) + (= pending_8 pending_7) + (= replicaState_8 replicaState_7) + (= log_8 log_7) + (= commitIndex_8 commitIndex_7) + (= leader_8 leader_7) + ) + ) +) +(assert ; Step 8 → 9 + (or + (and ; Action: CreateTransfer + t_id notIn transfers_keys + (select accounts_keys t_from) + (select accounts_keys t_to) + t_from distinct t_to + (or (select accounts_8 t_from).balance >= t_amount (select accounts_8 t_from).flags_allows_overdraft) + (= accounts_9 accounts_8) + (= transfers_9 transfers_8) + (= pending_9 pending_8) + (= replicaState_9 replicaState_8) + (= log_9 log_8) + (= commitIndex_9 commitIndex_8) + (= leader_9 leader_8) + ) + (and ; Action: CommitTransfer + (select pending_8 id) + (select transfers_keys id) + (select transfers_8 id).pending_8 = true + (= accounts_9 accounts_8) + (= transfers_9 transfers_8) + (= pending_9 pending_8) + (= replicaState_9 replicaState_8) + (= log_9 log_8) + (= commitIndex_9 commitIndex_8) + (= leader_9 leader_8) + ) + (and ; Action: VoidTransfer + (select pending_8 id) + (select transfers_keys id) + (select transfers_8 id).pending_8 = true + (= accounts_9 accounts_8) + (= transfers_9 transfers_8) + (= pending_9 pending_8) + (= replicaState_9 replicaState_8) + (= log_9 log_8) + (= commitIndex_9 commitIndex_8) + (= leader_9 leader_8) + ) + (and ; Action: PostTransfer + t_id notIn transfers_keys + (select accounts_keys t_from) + (select accounts_keys t_to) + t_from distinct t_to + (or (select accounts_8 t_from).balance >= t_amount (select accounts_8 t_from).flags_allows_overdraft) + (= accounts_9 accounts_8) + (= transfers_9 transfers_8) + (= pending_9 pending_8) + (= replicaState_9 replicaState_8) + (= log_9 log_8) + (= commitIndex_9 commitIndex_8) + (= leader_9 leader_8) + ) + (and ; Action: BecomeLeader + (select replicaState_keys replica) + (select replicaState_8 replica).role = "candidate" + (< (select replicaState_8 replica).currentTerm term) + (= accounts_9 accounts_8) + (= transfers_9 transfers_8) + (= pending_9 pending_8) + (= replicaState_9 replicaState_8) + (= log_9 log_8) + (= commitIndex_9 commitIndex_8) + (= leader_9 leader_8) + ) + (and ; Action: AppendEntry + (+ entry_index = length(log_8) 1) + term >= commitIndex_8 + (= accounts_9 accounts_8) + (= transfers_9 transfers_8) + (= pending_9 pending_8) + (= replicaState_9 replicaState_8) + (= log_9 log_8) + (= commitIndex_9 commitIndex_8) + (= leader_9 leader_8) + ) + ; Stuttering + (and + (= accounts_9 accounts_8) + (= transfers_9 transfers_8) + (= pending_9 pending_8) + (= replicaState_9 replicaState_8) + (= log_9 log_8) + (= commitIndex_9 commitIndex_8) + (= leader_9 leader_8) + ) + ) +) +(assert ; Step 9 → 10 + (or + (and ; Action: CreateTransfer + t_id notIn transfers_keys + (select accounts_keys t_from) + (select accounts_keys t_to) + t_from distinct t_to + (or (select accounts_9 t_from).balance >= t_amount (select accounts_9 t_from).flags_allows_overdraft) + (= accounts_10 accounts_9) + (= transfers_10 transfers_9) + (= pending_10 pending_9) + (= replicaState_10 replicaState_9) + (= log_10 log_9) + (= commitIndex_10 commitIndex_9) + (= leader_10 leader_9) + ) + (and ; Action: CommitTransfer + (select pending_9 id) + (select transfers_keys id) + (select transfers_9 id).pending_9 = true + (= accounts_10 accounts_9) + (= transfers_10 transfers_9) + (= pending_10 pending_9) + (= replicaState_10 replicaState_9) + (= log_10 log_9) + (= commitIndex_10 commitIndex_9) + (= leader_10 leader_9) + ) + (and ; Action: VoidTransfer + (select pending_9 id) + (select transfers_keys id) + (select transfers_9 id).pending_9 = true + (= accounts_10 accounts_9) + (= transfers_10 transfers_9) + (= pending_10 pending_9) + (= replicaState_10 replicaState_9) + (= log_10 log_9) + (= commitIndex_10 commitIndex_9) + (= leader_10 leader_9) + ) + (and ; Action: PostTransfer + t_id notIn transfers_keys + (select accounts_keys t_from) + (select accounts_keys t_to) + t_from distinct t_to + (or (select accounts_9 t_from).balance >= t_amount (select accounts_9 t_from).flags_allows_overdraft) + (= accounts_10 accounts_9) + (= transfers_10 transfers_9) + (= pending_10 pending_9) + (= replicaState_10 replicaState_9) + (= log_10 log_9) + (= commitIndex_10 commitIndex_9) + (= leader_10 leader_9) + ) + (and ; Action: BecomeLeader + (select replicaState_keys replica) + (select replicaState_9 replica).role = "candidate" + (< (select replicaState_9 replica).currentTerm term) + (= accounts_10 accounts_9) + (= transfers_10 transfers_9) + (= pending_10 pending_9) + (= replicaState_10 replicaState_9) + (= log_10 log_9) + (= commitIndex_10 commitIndex_9) + (= leader_10 leader_9) + ) + (and ; Action: AppendEntry + (+ entry_index = length(log_9) 1) + term >= commitIndex_9 + (= accounts_10 accounts_9) + (= transfers_10 transfers_9) + (= pending_10 pending_9) + (= replicaState_10 replicaState_9) + (= log_10 log_9) + (= commitIndex_10 commitIndex_9) + (= leader_10 leader_9) + ) + ; Stuttering + (and + (= accounts_10 accounts_9) + (= transfers_10 transfers_9) + (= pending_10 pending_9) + (= replicaState_10 replicaState_9) + (= log_10 log_9) + (= commitIndex_10 commitIndex_9) + (= leader_10 leader_9) + ) + ) +) + +; Property assertion: not(invariant at some step) +(assert + (or + (not (NoOverdraft_0)) + (not (NoOverdraft_1)) + (not (NoOverdraft_2)) + (not (NoOverdraft_3)) + (not (NoOverdraft_4)) + (not (NoOverdraft_5)) + (not (NoOverdraft_6)) + (not (NoOverdraft_7)) + (not (NoOverdraft_8)) + (not (NoOverdraft_9)) + (not (NoOverdraft_10)) + ) +) +(define-fun NoOverdraft_0 () Bool + (and + (forall ((a Account)) (or a_balance >= 0 a_flags.allows_overdraft)) + ) +) +(define-fun NoOverdraft_1 () Bool + (and + (forall ((a Account)) (or a_balance >= 0 a_flags.allows_overdraft)) + ) +) +(define-fun NoOverdraft_2 () Bool + (and + (forall ((a Account)) (or a_balance >= 0 a_flags.allows_overdraft)) + ) +) +(define-fun NoOverdraft_3 () Bool + (and + (forall ((a Account)) (or a_balance >= 0 a_flags.allows_overdraft)) + ) +) +(define-fun NoOverdraft_4 () Bool + (and + (forall ((a Account)) (or a_balance >= 0 a_flags.allows_overdraft)) + ) +) +(define-fun NoOverdraft_5 () Bool + (and + (forall ((a Account)) (or a_balance >= 0 a_flags.allows_overdraft)) + ) +) +(define-fun NoOverdraft_6 () Bool + (and + (forall ((a Account)) (or a_balance >= 0 a_flags.allows_overdraft)) + ) +) +(define-fun NoOverdraft_7 () Bool + (and + (forall ((a Account)) (or a_balance >= 0 a_flags.allows_overdraft)) + ) +) +(define-fun NoOverdraft_8 () Bool + (and + (forall ((a Account)) (or a_balance >= 0 a_flags.allows_overdraft)) + ) +) +(define-fun NoOverdraft_9 () Bool + (and + (forall ((a Account)) (or a_balance >= 0 a_flags.allows_overdraft)) + ) +) +(define-fun NoOverdraft_10 () Bool + (and + (forall ((a Account)) (or a_balance >= 0 a_flags.allows_overdraft)) + ) +) + +(echo "Checking: Always(NoOverdraft) for 10 steps") +(check-sat) +(get-model) +; Verification: Eventually(TransferStateConsistency) +; BMC depth: 10 + +; Declare state copies for 10 steps +(declare-const accounts_0 (Array Int Account)) +(declare-const accounts_1 (Array Int Account)) +(declare-const accounts_2 (Array Int Account)) +(declare-const accounts_3 (Array Int Account)) +(declare-const accounts_4 (Array Int Account)) +(declare-const accounts_5 (Array Int Account)) +(declare-const accounts_6 (Array Int Account)) +(declare-const accounts_7 (Array Int Account)) +(declare-const accounts_8 (Array Int Account)) +(declare-const accounts_9 (Array Int Account)) +(declare-const accounts_10 (Array Int Account)) +(declare-const transfers_0 (Array Int Transfer)) +(declare-const transfers_1 (Array Int Transfer)) +(declare-const transfers_2 (Array Int Transfer)) +(declare-const transfers_3 (Array Int Transfer)) +(declare-const transfers_4 (Array Int Transfer)) +(declare-const transfers_5 (Array Int Transfer)) +(declare-const transfers_6 (Array Int Transfer)) +(declare-const transfers_7 (Array Int Transfer)) +(declare-const transfers_8 (Array Int Transfer)) +(declare-const transfers_9 (Array Int Transfer)) +(declare-const transfers_10 (Array Int Transfer)) +(declare-const pending_0 (Array Int Bool)) +(declare-const pending_1 (Array Int Bool)) +(declare-const pending_2 (Array Int Bool)) +(declare-const pending_3 (Array Int Bool)) +(declare-const pending_4 (Array Int Bool)) +(declare-const pending_5 (Array Int Bool)) +(declare-const pending_6 (Array Int Bool)) +(declare-const pending_7 (Array Int Bool)) +(declare-const pending_8 (Array Int Bool)) +(declare-const pending_9 (Array Int Bool)) +(declare-const pending_10 (Array Int Bool)) +(declare-const replicaState_0 (Array Int Replica)) +(declare-const replicaState_1 (Array Int Replica)) +(declare-const replicaState_2 (Array Int Replica)) +(declare-const replicaState_3 (Array Int Replica)) +(declare-const replicaState_4 (Array Int Replica)) +(declare-const replicaState_5 (Array Int Replica)) +(declare-const replicaState_6 (Array Int Replica)) +(declare-const replicaState_7 (Array Int Replica)) +(declare-const replicaState_8 (Array Int Replica)) +(declare-const replicaState_9 (Array Int Replica)) +(declare-const replicaState_10 (Array Int Replica)) +(declare-const log_0 (Array Int LogEntry)) +(declare-const log_1 (Array Int LogEntry)) +(declare-const log_2 (Array Int LogEntry)) +(declare-const log_3 (Array Int LogEntry)) +(declare-const log_4 (Array Int LogEntry)) +(declare-const log_5 (Array Int LogEntry)) +(declare-const log_6 (Array Int LogEntry)) +(declare-const log_7 (Array Int LogEntry)) +(declare-const log_8 (Array Int LogEntry)) +(declare-const log_9 (Array Int LogEntry)) +(declare-const log_10 (Array Int LogEntry)) +(declare-const commitIndex_0 Int) +(declare-const commitIndex_1 Int) +(declare-const commitIndex_2 Int) +(declare-const commitIndex_3 Int) +(declare-const commitIndex_4 Int) +(declare-const commitIndex_5 Int) +(declare-const commitIndex_6 Int) +(declare-const commitIndex_7 Int) +(declare-const commitIndex_8 Int) +(declare-const commitIndex_9 Int) +(declare-const commitIndex_10 Int) +(declare-const leader_0 Int) +(declare-const leader_1 Int) +(declare-const leader_2 Int) +(declare-const leader_3 Int) +(declare-const leader_4 Int) +(declare-const leader_5 Int) +(declare-const leader_6 Int) +(declare-const leader_7 Int) +(declare-const leader_8 Int) +(declare-const leader_9 Int) +(declare-const leader_10 Int) + +; Initial state constraints +(assert + (and + (>= commitIndex_0 0) + (>= leader_0 0) + ) +) + +; Transition constraints +(assert ; Step 0 → 1 + (or + (and ; Action: CreateTransfer + t_id notIn transfers_keys + (select accounts_keys t_from) + (select accounts_keys t_to) + t_from distinct t_to + (or (select accounts_0 t_from).balance >= t_amount (select accounts_0 t_from).flags_allows_overdraft) + (= accounts_1 accounts_0) + (= transfers_1 transfers_0) + (= pending_1 pending_0) + (= replicaState_1 replicaState_0) + (= log_1 log_0) + (= commitIndex_1 commitIndex_0) + (= leader_1 leader_0) + ) + (and ; Action: CommitTransfer + (select pending_0 id) + (select transfers_keys id) + (select transfers_0 id).pending_0 = true + (= accounts_1 accounts_0) + (= transfers_1 transfers_0) + (= pending_1 pending_0) + (= replicaState_1 replicaState_0) + (= log_1 log_0) + (= commitIndex_1 commitIndex_0) + (= leader_1 leader_0) + ) + (and ; Action: VoidTransfer + (select pending_0 id) + (select transfers_keys id) + (select transfers_0 id).pending_0 = true + (= accounts_1 accounts_0) + (= transfers_1 transfers_0) + (= pending_1 pending_0) + (= replicaState_1 replicaState_0) + (= log_1 log_0) + (= commitIndex_1 commitIndex_0) + (= leader_1 leader_0) + ) + (and ; Action: PostTransfer + t_id notIn transfers_keys + (select accounts_keys t_from) + (select accounts_keys t_to) + t_from distinct t_to + (or (select accounts_0 t_from).balance >= t_amount (select accounts_0 t_from).flags_allows_overdraft) + (= accounts_1 accounts_0) + (= transfers_1 transfers_0) + (= pending_1 pending_0) + (= replicaState_1 replicaState_0) + (= log_1 log_0) + (= commitIndex_1 commitIndex_0) + (= leader_1 leader_0) + ) + (and ; Action: BecomeLeader + (select replicaState_keys replica) + (select replicaState_0 replica).role = "candidate" + (< (select replicaState_0 replica).currentTerm term) + (= accounts_1 accounts_0) + (= transfers_1 transfers_0) + (= pending_1 pending_0) + (= replicaState_1 replicaState_0) + (= log_1 log_0) + (= commitIndex_1 commitIndex_0) + (= leader_1 leader_0) + ) + (and ; Action: AppendEntry + (+ entry_index = length(log_0) 1) + term >= commitIndex_0 + (= accounts_1 accounts_0) + (= transfers_1 transfers_0) + (= pending_1 pending_0) + (= replicaState_1 replicaState_0) + (= log_1 log_0) + (= commitIndex_1 commitIndex_0) + (= leader_1 leader_0) + ) + ; Stuttering + (and + (= accounts_1 accounts_0) + (= transfers_1 transfers_0) + (= pending_1 pending_0) + (= replicaState_1 replicaState_0) + (= log_1 log_0) + (= commitIndex_1 commitIndex_0) + (= leader_1 leader_0) + ) + ) +) +(assert ; Step 1 → 2 + (or + (and ; Action: CreateTransfer + t_id notIn transfers_keys + (select accounts_keys t_from) + (select accounts_keys t_to) + t_from distinct t_to + (or (select accounts_1 t_from).balance >= t_amount (select accounts_1 t_from).flags_allows_overdraft) + (= accounts_2 accounts_1) + (= transfers_2 transfers_1) + (= pending_2 pending_1) + (= replicaState_2 replicaState_1) + (= log_2 log_1) + (= commitIndex_2 commitIndex_1) + (= leader_2 leader_1) + ) + (and ; Action: CommitTransfer + (select pending_1 id) + (select transfers_keys id) + (select transfers_1 id).pending_1 = true + (= accounts_2 accounts_1) + (= transfers_2 transfers_1) + (= pending_2 pending_1) + (= replicaState_2 replicaState_1) + (= log_2 log_1) + (= commitIndex_2 commitIndex_1) + (= leader_2 leader_1) + ) + (and ; Action: VoidTransfer + (select pending_1 id) + (select transfers_keys id) + (select transfers_1 id).pending_1 = true + (= accounts_2 accounts_1) + (= transfers_2 transfers_1) + (= pending_2 pending_1) + (= replicaState_2 replicaState_1) + (= log_2 log_1) + (= commitIndex_2 commitIndex_1) + (= leader_2 leader_1) + ) + (and ; Action: PostTransfer + t_id notIn transfers_keys + (select accounts_keys t_from) + (select accounts_keys t_to) + t_from distinct t_to + (or (select accounts_1 t_from).balance >= t_amount (select accounts_1 t_from).flags_allows_overdraft) + (= accounts_2 accounts_1) + (= transfers_2 transfers_1) + (= pending_2 pending_1) + (= replicaState_2 replicaState_1) + (= log_2 log_1) + (= commitIndex_2 commitIndex_1) + (= leader_2 leader_1) + ) + (and ; Action: BecomeLeader + (select replicaState_keys replica) + (select replicaState_1 replica).role = "candidate" + (< (select replicaState_1 replica).currentTerm term) + (= accounts_2 accounts_1) + (= transfers_2 transfers_1) + (= pending_2 pending_1) + (= replicaState_2 replicaState_1) + (= log_2 log_1) + (= commitIndex_2 commitIndex_1) + (= leader_2 leader_1) + ) + (and ; Action: AppendEntry + (+ entry_index = length(log_1) 1) + term >= commitIndex_1 + (= accounts_2 accounts_1) + (= transfers_2 transfers_1) + (= pending_2 pending_1) + (= replicaState_2 replicaState_1) + (= log_2 log_1) + (= commitIndex_2 commitIndex_1) + (= leader_2 leader_1) + ) + ; Stuttering + (and + (= accounts_2 accounts_1) + (= transfers_2 transfers_1) + (= pending_2 pending_1) + (= replicaState_2 replicaState_1) + (= log_2 log_1) + (= commitIndex_2 commitIndex_1) + (= leader_2 leader_1) + ) + ) +) +(assert ; Step 2 → 3 + (or + (and ; Action: CreateTransfer + t_id notIn transfers_keys + (select accounts_keys t_from) + (select accounts_keys t_to) + t_from distinct t_to + (or (select accounts_2 t_from).balance >= t_amount (select accounts_2 t_from).flags_allows_overdraft) + (= accounts_3 accounts_2) + (= transfers_3 transfers_2) + (= pending_3 pending_2) + (= replicaState_3 replicaState_2) + (= log_3 log_2) + (= commitIndex_3 commitIndex_2) + (= leader_3 leader_2) + ) + (and ; Action: CommitTransfer + (select pending_2 id) + (select transfers_keys id) + (select transfers_2 id).pending_2 = true + (= accounts_3 accounts_2) + (= transfers_3 transfers_2) + (= pending_3 pending_2) + (= replicaState_3 replicaState_2) + (= log_3 log_2) + (= commitIndex_3 commitIndex_2) + (= leader_3 leader_2) + ) + (and ; Action: VoidTransfer + (select pending_2 id) + (select transfers_keys id) + (select transfers_2 id).pending_2 = true + (= accounts_3 accounts_2) + (= transfers_3 transfers_2) + (= pending_3 pending_2) + (= replicaState_3 replicaState_2) + (= log_3 log_2) + (= commitIndex_3 commitIndex_2) + (= leader_3 leader_2) + ) + (and ; Action: PostTransfer + t_id notIn transfers_keys + (select accounts_keys t_from) + (select accounts_keys t_to) + t_from distinct t_to + (or (select accounts_2 t_from).balance >= t_amount (select accounts_2 t_from).flags_allows_overdraft) + (= accounts_3 accounts_2) + (= transfers_3 transfers_2) + (= pending_3 pending_2) + (= replicaState_3 replicaState_2) + (= log_3 log_2) + (= commitIndex_3 commitIndex_2) + (= leader_3 leader_2) + ) + (and ; Action: BecomeLeader + (select replicaState_keys replica) + (select replicaState_2 replica).role = "candidate" + (< (select replicaState_2 replica).currentTerm term) + (= accounts_3 accounts_2) + (= transfers_3 transfers_2) + (= pending_3 pending_2) + (= replicaState_3 replicaState_2) + (= log_3 log_2) + (= commitIndex_3 commitIndex_2) + (= leader_3 leader_2) + ) + (and ; Action: AppendEntry + (+ entry_index = length(log_2) 1) + term >= commitIndex_2 + (= accounts_3 accounts_2) + (= transfers_3 transfers_2) + (= pending_3 pending_2) + (= replicaState_3 replicaState_2) + (= log_3 log_2) + (= commitIndex_3 commitIndex_2) + (= leader_3 leader_2) + ) + ; Stuttering + (and + (= accounts_3 accounts_2) + (= transfers_3 transfers_2) + (= pending_3 pending_2) + (= replicaState_3 replicaState_2) + (= log_3 log_2) + (= commitIndex_3 commitIndex_2) + (= leader_3 leader_2) + ) + ) +) +(assert ; Step 3 → 4 + (or + (and ; Action: CreateTransfer + t_id notIn transfers_keys + (select accounts_keys t_from) + (select accounts_keys t_to) + t_from distinct t_to + (or (select accounts_3 t_from).balance >= t_amount (select accounts_3 t_from).flags_allows_overdraft) + (= accounts_4 accounts_3) + (= transfers_4 transfers_3) + (= pending_4 pending_3) + (= replicaState_4 replicaState_3) + (= log_4 log_3) + (= commitIndex_4 commitIndex_3) + (= leader_4 leader_3) + ) + (and ; Action: CommitTransfer + (select pending_3 id) + (select transfers_keys id) + (select transfers_3 id).pending_3 = true + (= accounts_4 accounts_3) + (= transfers_4 transfers_3) + (= pending_4 pending_3) + (= replicaState_4 replicaState_3) + (= log_4 log_3) + (= commitIndex_4 commitIndex_3) + (= leader_4 leader_3) + ) + (and ; Action: VoidTransfer + (select pending_3 id) + (select transfers_keys id) + (select transfers_3 id).pending_3 = true + (= accounts_4 accounts_3) + (= transfers_4 transfers_3) + (= pending_4 pending_3) + (= replicaState_4 replicaState_3) + (= log_4 log_3) + (= commitIndex_4 commitIndex_3) + (= leader_4 leader_3) + ) + (and ; Action: PostTransfer + t_id notIn transfers_keys + (select accounts_keys t_from) + (select accounts_keys t_to) + t_from distinct t_to + (or (select accounts_3 t_from).balance >= t_amount (select accounts_3 t_from).flags_allows_overdraft) + (= accounts_4 accounts_3) + (= transfers_4 transfers_3) + (= pending_4 pending_3) + (= replicaState_4 replicaState_3) + (= log_4 log_3) + (= commitIndex_4 commitIndex_3) + (= leader_4 leader_3) + ) + (and ; Action: BecomeLeader + (select replicaState_keys replica) + (select replicaState_3 replica).role = "candidate" + (< (select replicaState_3 replica).currentTerm term) + (= accounts_4 accounts_3) + (= transfers_4 transfers_3) + (= pending_4 pending_3) + (= replicaState_4 replicaState_3) + (= log_4 log_3) + (= commitIndex_4 commitIndex_3) + (= leader_4 leader_3) + ) + (and ; Action: AppendEntry + (+ entry_index = length(log_3) 1) + term >= commitIndex_3 + (= accounts_4 accounts_3) + (= transfers_4 transfers_3) + (= pending_4 pending_3) + (= replicaState_4 replicaState_3) + (= log_4 log_3) + (= commitIndex_4 commitIndex_3) + (= leader_4 leader_3) + ) + ; Stuttering + (and + (= accounts_4 accounts_3) + (= transfers_4 transfers_3) + (= pending_4 pending_3) + (= replicaState_4 replicaState_3) + (= log_4 log_3) + (= commitIndex_4 commitIndex_3) + (= leader_4 leader_3) + ) + ) +) +(assert ; Step 4 → 5 + (or + (and ; Action: CreateTransfer + t_id notIn transfers_keys + (select accounts_keys t_from) + (select accounts_keys t_to) + t_from distinct t_to + (or (select accounts_4 t_from).balance >= t_amount (select accounts_4 t_from).flags_allows_overdraft) + (= accounts_5 accounts_4) + (= transfers_5 transfers_4) + (= pending_5 pending_4) + (= replicaState_5 replicaState_4) + (= log_5 log_4) + (= commitIndex_5 commitIndex_4) + (= leader_5 leader_4) + ) + (and ; Action: CommitTransfer + (select pending_4 id) + (select transfers_keys id) + (select transfers_4 id).pending_4 = true + (= accounts_5 accounts_4) + (= transfers_5 transfers_4) + (= pending_5 pending_4) + (= replicaState_5 replicaState_4) + (= log_5 log_4) + (= commitIndex_5 commitIndex_4) + (= leader_5 leader_4) + ) + (and ; Action: VoidTransfer + (select pending_4 id) + (select transfers_keys id) + (select transfers_4 id).pending_4 = true + (= accounts_5 accounts_4) + (= transfers_5 transfers_4) + (= pending_5 pending_4) + (= replicaState_5 replicaState_4) + (= log_5 log_4) + (= commitIndex_5 commitIndex_4) + (= leader_5 leader_4) + ) + (and ; Action: PostTransfer + t_id notIn transfers_keys + (select accounts_keys t_from) + (select accounts_keys t_to) + t_from distinct t_to + (or (select accounts_4 t_from).balance >= t_amount (select accounts_4 t_from).flags_allows_overdraft) + (= accounts_5 accounts_4) + (= transfers_5 transfers_4) + (= pending_5 pending_4) + (= replicaState_5 replicaState_4) + (= log_5 log_4) + (= commitIndex_5 commitIndex_4) + (= leader_5 leader_4) + ) + (and ; Action: BecomeLeader + (select replicaState_keys replica) + (select replicaState_4 replica).role = "candidate" + (< (select replicaState_4 replica).currentTerm term) + (= accounts_5 accounts_4) + (= transfers_5 transfers_4) + (= pending_5 pending_4) + (= replicaState_5 replicaState_4) + (= log_5 log_4) + (= commitIndex_5 commitIndex_4) + (= leader_5 leader_4) + ) + (and ; Action: AppendEntry + (+ entry_index = length(log_4) 1) + term >= commitIndex_4 + (= accounts_5 accounts_4) + (= transfers_5 transfers_4) + (= pending_5 pending_4) + (= replicaState_5 replicaState_4) + (= log_5 log_4) + (= commitIndex_5 commitIndex_4) + (= leader_5 leader_4) + ) + ; Stuttering + (and + (= accounts_5 accounts_4) + (= transfers_5 transfers_4) + (= pending_5 pending_4) + (= replicaState_5 replicaState_4) + (= log_5 log_4) + (= commitIndex_5 commitIndex_4) + (= leader_5 leader_4) + ) + ) +) +(assert ; Step 5 → 6 + (or + (and ; Action: CreateTransfer + t_id notIn transfers_keys + (select accounts_keys t_from) + (select accounts_keys t_to) + t_from distinct t_to + (or (select accounts_5 t_from).balance >= t_amount (select accounts_5 t_from).flags_allows_overdraft) + (= accounts_6 accounts_5) + (= transfers_6 transfers_5) + (= pending_6 pending_5) + (= replicaState_6 replicaState_5) + (= log_6 log_5) + (= commitIndex_6 commitIndex_5) + (= leader_6 leader_5) + ) + (and ; Action: CommitTransfer + (select pending_5 id) + (select transfers_keys id) + (select transfers_5 id).pending_5 = true + (= accounts_6 accounts_5) + (= transfers_6 transfers_5) + (= pending_6 pending_5) + (= replicaState_6 replicaState_5) + (= log_6 log_5) + (= commitIndex_6 commitIndex_5) + (= leader_6 leader_5) + ) + (and ; Action: VoidTransfer + (select pending_5 id) + (select transfers_keys id) + (select transfers_5 id).pending_5 = true + (= accounts_6 accounts_5) + (= transfers_6 transfers_5) + (= pending_6 pending_5) + (= replicaState_6 replicaState_5) + (= log_6 log_5) + (= commitIndex_6 commitIndex_5) + (= leader_6 leader_5) + ) + (and ; Action: PostTransfer + t_id notIn transfers_keys + (select accounts_keys t_from) + (select accounts_keys t_to) + t_from distinct t_to + (or (select accounts_5 t_from).balance >= t_amount (select accounts_5 t_from).flags_allows_overdraft) + (= accounts_6 accounts_5) + (= transfers_6 transfers_5) + (= pending_6 pending_5) + (= replicaState_6 replicaState_5) + (= log_6 log_5) + (= commitIndex_6 commitIndex_5) + (= leader_6 leader_5) + ) + (and ; Action: BecomeLeader + (select replicaState_keys replica) + (select replicaState_5 replica).role = "candidate" + (< (select replicaState_5 replica).currentTerm term) + (= accounts_6 accounts_5) + (= transfers_6 transfers_5) + (= pending_6 pending_5) + (= replicaState_6 replicaState_5) + (= log_6 log_5) + (= commitIndex_6 commitIndex_5) + (= leader_6 leader_5) + ) + (and ; Action: AppendEntry + (+ entry_index = length(log_5) 1) + term >= commitIndex_5 + (= accounts_6 accounts_5) + (= transfers_6 transfers_5) + (= pending_6 pending_5) + (= replicaState_6 replicaState_5) + (= log_6 log_5) + (= commitIndex_6 commitIndex_5) + (= leader_6 leader_5) + ) + ; Stuttering + (and + (= accounts_6 accounts_5) + (= transfers_6 transfers_5) + (= pending_6 pending_5) + (= replicaState_6 replicaState_5) + (= log_6 log_5) + (= commitIndex_6 commitIndex_5) + (= leader_6 leader_5) + ) + ) +) +(assert ; Step 6 → 7 + (or + (and ; Action: CreateTransfer + t_id notIn transfers_keys + (select accounts_keys t_from) + (select accounts_keys t_to) + t_from distinct t_to + (or (select accounts_6 t_from).balance >= t_amount (select accounts_6 t_from).flags_allows_overdraft) + (= accounts_7 accounts_6) + (= transfers_7 transfers_6) + (= pending_7 pending_6) + (= replicaState_7 replicaState_6) + (= log_7 log_6) + (= commitIndex_7 commitIndex_6) + (= leader_7 leader_6) + ) + (and ; Action: CommitTransfer + (select pending_6 id) + (select transfers_keys id) + (select transfers_6 id).pending_6 = true + (= accounts_7 accounts_6) + (= transfers_7 transfers_6) + (= pending_7 pending_6) + (= replicaState_7 replicaState_6) + (= log_7 log_6) + (= commitIndex_7 commitIndex_6) + (= leader_7 leader_6) + ) + (and ; Action: VoidTransfer + (select pending_6 id) + (select transfers_keys id) + (select transfers_6 id).pending_6 = true + (= accounts_7 accounts_6) + (= transfers_7 transfers_6) + (= pending_7 pending_6) + (= replicaState_7 replicaState_6) + (= log_7 log_6) + (= commitIndex_7 commitIndex_6) + (= leader_7 leader_6) + ) + (and ; Action: PostTransfer + t_id notIn transfers_keys + (select accounts_keys t_from) + (select accounts_keys t_to) + t_from distinct t_to + (or (select accounts_6 t_from).balance >= t_amount (select accounts_6 t_from).flags_allows_overdraft) + (= accounts_7 accounts_6) + (= transfers_7 transfers_6) + (= pending_7 pending_6) + (= replicaState_7 replicaState_6) + (= log_7 log_6) + (= commitIndex_7 commitIndex_6) + (= leader_7 leader_6) + ) + (and ; Action: BecomeLeader + (select replicaState_keys replica) + (select replicaState_6 replica).role = "candidate" + (< (select replicaState_6 replica).currentTerm term) + (= accounts_7 accounts_6) + (= transfers_7 transfers_6) + (= pending_7 pending_6) + (= replicaState_7 replicaState_6) + (= log_7 log_6) + (= commitIndex_7 commitIndex_6) + (= leader_7 leader_6) + ) + (and ; Action: AppendEntry + (+ entry_index = length(log_6) 1) + term >= commitIndex_6 + (= accounts_7 accounts_6) + (= transfers_7 transfers_6) + (= pending_7 pending_6) + (= replicaState_7 replicaState_6) + (= log_7 log_6) + (= commitIndex_7 commitIndex_6) + (= leader_7 leader_6) + ) + ; Stuttering + (and + (= accounts_7 accounts_6) + (= transfers_7 transfers_6) + (= pending_7 pending_6) + (= replicaState_7 replicaState_6) + (= log_7 log_6) + (= commitIndex_7 commitIndex_6) + (= leader_7 leader_6) + ) + ) +) +(assert ; Step 7 → 8 + (or + (and ; Action: CreateTransfer + t_id notIn transfers_keys + (select accounts_keys t_from) + (select accounts_keys t_to) + t_from distinct t_to + (or (select accounts_7 t_from).balance >= t_amount (select accounts_7 t_from).flags_allows_overdraft) + (= accounts_8 accounts_7) + (= transfers_8 transfers_7) + (= pending_8 pending_7) + (= replicaState_8 replicaState_7) + (= log_8 log_7) + (= commitIndex_8 commitIndex_7) + (= leader_8 leader_7) + ) + (and ; Action: CommitTransfer + (select pending_7 id) + (select transfers_keys id) + (select transfers_7 id).pending_7 = true + (= accounts_8 accounts_7) + (= transfers_8 transfers_7) + (= pending_8 pending_7) + (= replicaState_8 replicaState_7) + (= log_8 log_7) + (= commitIndex_8 commitIndex_7) + (= leader_8 leader_7) + ) + (and ; Action: VoidTransfer + (select pending_7 id) + (select transfers_keys id) + (select transfers_7 id).pending_7 = true + (= accounts_8 accounts_7) + (= transfers_8 transfers_7) + (= pending_8 pending_7) + (= replicaState_8 replicaState_7) + (= log_8 log_7) + (= commitIndex_8 commitIndex_7) + (= leader_8 leader_7) + ) + (and ; Action: PostTransfer + t_id notIn transfers_keys + (select accounts_keys t_from) + (select accounts_keys t_to) + t_from distinct t_to + (or (select accounts_7 t_from).balance >= t_amount (select accounts_7 t_from).flags_allows_overdraft) + (= accounts_8 accounts_7) + (= transfers_8 transfers_7) + (= pending_8 pending_7) + (= replicaState_8 replicaState_7) + (= log_8 log_7) + (= commitIndex_8 commitIndex_7) + (= leader_8 leader_7) + ) + (and ; Action: BecomeLeader + (select replicaState_keys replica) + (select replicaState_7 replica).role = "candidate" + (< (select replicaState_7 replica).currentTerm term) + (= accounts_8 accounts_7) + (= transfers_8 transfers_7) + (= pending_8 pending_7) + (= replicaState_8 replicaState_7) + (= log_8 log_7) + (= commitIndex_8 commitIndex_7) + (= leader_8 leader_7) + ) + (and ; Action: AppendEntry + (+ entry_index = length(log_7) 1) + term >= commitIndex_7 + (= accounts_8 accounts_7) + (= transfers_8 transfers_7) + (= pending_8 pending_7) + (= replicaState_8 replicaState_7) + (= log_8 log_7) + (= commitIndex_8 commitIndex_7) + (= leader_8 leader_7) + ) + ; Stuttering + (and + (= accounts_8 accounts_7) + (= transfers_8 transfers_7) + (= pending_8 pending_7) + (= replicaState_8 replicaState_7) + (= log_8 log_7) + (= commitIndex_8 commitIndex_7) + (= leader_8 leader_7) + ) + ) +) +(assert ; Step 8 → 9 + (or + (and ; Action: CreateTransfer + t_id notIn transfers_keys + (select accounts_keys t_from) + (select accounts_keys t_to) + t_from distinct t_to + (or (select accounts_8 t_from).balance >= t_amount (select accounts_8 t_from).flags_allows_overdraft) + (= accounts_9 accounts_8) + (= transfers_9 transfers_8) + (= pending_9 pending_8) + (= replicaState_9 replicaState_8) + (= log_9 log_8) + (= commitIndex_9 commitIndex_8) + (= leader_9 leader_8) + ) + (and ; Action: CommitTransfer + (select pending_8 id) + (select transfers_keys id) + (select transfers_8 id).pending_8 = true + (= accounts_9 accounts_8) + (= transfers_9 transfers_8) + (= pending_9 pending_8) + (= replicaState_9 replicaState_8) + (= log_9 log_8) + (= commitIndex_9 commitIndex_8) + (= leader_9 leader_8) + ) + (and ; Action: VoidTransfer + (select pending_8 id) + (select transfers_keys id) + (select transfers_8 id).pending_8 = true + (= accounts_9 accounts_8) + (= transfers_9 transfers_8) + (= pending_9 pending_8) + (= replicaState_9 replicaState_8) + (= log_9 log_8) + (= commitIndex_9 commitIndex_8) + (= leader_9 leader_8) + ) + (and ; Action: PostTransfer + t_id notIn transfers_keys + (select accounts_keys t_from) + (select accounts_keys t_to) + t_from distinct t_to + (or (select accounts_8 t_from).balance >= t_amount (select accounts_8 t_from).flags_allows_overdraft) + (= accounts_9 accounts_8) + (= transfers_9 transfers_8) + (= pending_9 pending_8) + (= replicaState_9 replicaState_8) + (= log_9 log_8) + (= commitIndex_9 commitIndex_8) + (= leader_9 leader_8) + ) + (and ; Action: BecomeLeader + (select replicaState_keys replica) + (select replicaState_8 replica).role = "candidate" + (< (select replicaState_8 replica).currentTerm term) + (= accounts_9 accounts_8) + (= transfers_9 transfers_8) + (= pending_9 pending_8) + (= replicaState_9 replicaState_8) + (= log_9 log_8) + (= commitIndex_9 commitIndex_8) + (= leader_9 leader_8) + ) + (and ; Action: AppendEntry + (+ entry_index = length(log_8) 1) + term >= commitIndex_8 + (= accounts_9 accounts_8) + (= transfers_9 transfers_8) + (= pending_9 pending_8) + (= replicaState_9 replicaState_8) + (= log_9 log_8) + (= commitIndex_9 commitIndex_8) + (= leader_9 leader_8) + ) + ; Stuttering + (and + (= accounts_9 accounts_8) + (= transfers_9 transfers_8) + (= pending_9 pending_8) + (= replicaState_9 replicaState_8) + (= log_9 log_8) + (= commitIndex_9 commitIndex_8) + (= leader_9 leader_8) + ) + ) +) +(assert ; Step 9 → 10 + (or + (and ; Action: CreateTransfer + t_id notIn transfers_keys + (select accounts_keys t_from) + (select accounts_keys t_to) + t_from distinct t_to + (or (select accounts_9 t_from).balance >= t_amount (select accounts_9 t_from).flags_allows_overdraft) + (= accounts_10 accounts_9) + (= transfers_10 transfers_9) + (= pending_10 pending_9) + (= replicaState_10 replicaState_9) + (= log_10 log_9) + (= commitIndex_10 commitIndex_9) + (= leader_10 leader_9) + ) + (and ; Action: CommitTransfer + (select pending_9 id) + (select transfers_keys id) + (select transfers_9 id).pending_9 = true + (= accounts_10 accounts_9) + (= transfers_10 transfers_9) + (= pending_10 pending_9) + (= replicaState_10 replicaState_9) + (= log_10 log_9) + (= commitIndex_10 commitIndex_9) + (= leader_10 leader_9) + ) + (and ; Action: VoidTransfer + (select pending_9 id) + (select transfers_keys id) + (select transfers_9 id).pending_9 = true + (= accounts_10 accounts_9) + (= transfers_10 transfers_9) + (= pending_10 pending_9) + (= replicaState_10 replicaState_9) + (= log_10 log_9) + (= commitIndex_10 commitIndex_9) + (= leader_10 leader_9) + ) + (and ; Action: PostTransfer + t_id notIn transfers_keys + (select accounts_keys t_from) + (select accounts_keys t_to) + t_from distinct t_to + (or (select accounts_9 t_from).balance >= t_amount (select accounts_9 t_from).flags_allows_overdraft) + (= accounts_10 accounts_9) + (= transfers_10 transfers_9) + (= pending_10 pending_9) + (= replicaState_10 replicaState_9) + (= log_10 log_9) + (= commitIndex_10 commitIndex_9) + (= leader_10 leader_9) + ) + (and ; Action: BecomeLeader + (select replicaState_keys replica) + (select replicaState_9 replica).role = "candidate" + (< (select replicaState_9 replica).currentTerm term) + (= accounts_10 accounts_9) + (= transfers_10 transfers_9) + (= pending_10 pending_9) + (= replicaState_10 replicaState_9) + (= log_10 log_9) + (= commitIndex_10 commitIndex_9) + (= leader_10 leader_9) + ) + (and ; Action: AppendEntry + (+ entry_index = length(log_9) 1) + term >= commitIndex_9 + (= accounts_10 accounts_9) + (= transfers_10 transfers_9) + (= pending_10 pending_9) + (= replicaState_10 replicaState_9) + (= log_10 log_9) + (= commitIndex_10 commitIndex_9) + (= leader_10 leader_9) + ) + ; Stuttering + (and + (= accounts_10 accounts_9) + (= transfers_10 transfers_9) + (= pending_10 pending_9) + (= replicaState_10 replicaState_9) + (= log_10 log_9) + (= commitIndex_10 commitIndex_9) + (= leader_10 leader_9) + ) + ) +) + +; Property assertion: not(invariant at some step) +(assert + (and + (not (TransferStateConsistency_0)) + (not (TransferStateConsistency_1)) + (not (TransferStateConsistency_2)) + (not (TransferStateConsistency_3)) + (not (TransferStateConsistency_4)) + (not (TransferStateConsistency_5)) + (not (TransferStateConsistency_6)) + (not (TransferStateConsistency_7)) + (not (TransferStateConsistency_8)) + (not (TransferStateConsistency_9)) + (not (TransferStateConsistency_10)) + ) +) +(define-fun TransferStateConsistency_0 () Bool + (and + (forall ((t Transfer)) (and t_pending implies t_posted = false t_voided = false)) + (forall ((t Transfer)) t_posted implies t_voided = false) + (forall ((t Transfer)) t_voided implies t_posted = false) + ) +) +(define-fun TransferStateConsistency_1 () Bool + (and + (forall ((t Transfer)) (and t_pending implies t_posted = false t_voided = false)) + (forall ((t Transfer)) t_posted implies t_voided = false) + (forall ((t Transfer)) t_voided implies t_posted = false) + ) +) +(define-fun TransferStateConsistency_2 () Bool + (and + (forall ((t Transfer)) (and t_pending implies t_posted = false t_voided = false)) + (forall ((t Transfer)) t_posted implies t_voided = false) + (forall ((t Transfer)) t_voided implies t_posted = false) + ) +) +(define-fun TransferStateConsistency_3 () Bool + (and + (forall ((t Transfer)) (and t_pending implies t_posted = false t_voided = false)) + (forall ((t Transfer)) t_posted implies t_voided = false) + (forall ((t Transfer)) t_voided implies t_posted = false) + ) +) +(define-fun TransferStateConsistency_4 () Bool + (and + (forall ((t Transfer)) (and t_pending implies t_posted = false t_voided = false)) + (forall ((t Transfer)) t_posted implies t_voided = false) + (forall ((t Transfer)) t_voided implies t_posted = false) + ) +) +(define-fun TransferStateConsistency_5 () Bool + (and + (forall ((t Transfer)) (and t_pending implies t_posted = false t_voided = false)) + (forall ((t Transfer)) t_posted implies t_voided = false) + (forall ((t Transfer)) t_voided implies t_posted = false) + ) +) +(define-fun TransferStateConsistency_6 () Bool + (and + (forall ((t Transfer)) (and t_pending implies t_posted = false t_voided = false)) + (forall ((t Transfer)) t_posted implies t_voided = false) + (forall ((t Transfer)) t_voided implies t_posted = false) + ) +) +(define-fun TransferStateConsistency_7 () Bool + (and + (forall ((t Transfer)) (and t_pending implies t_posted = false t_voided = false)) + (forall ((t Transfer)) t_posted implies t_voided = false) + (forall ((t Transfer)) t_voided implies t_posted = false) + ) +) +(define-fun TransferStateConsistency_8 () Bool + (and + (forall ((t Transfer)) (and t_pending implies t_posted = false t_voided = false)) + (forall ((t Transfer)) t_posted implies t_voided = false) + (forall ((t Transfer)) t_voided implies t_posted = false) + ) +) +(define-fun TransferStateConsistency_9 () Bool + (and + (forall ((t Transfer)) (and t_pending implies t_posted = false t_voided = false)) + (forall ((t Transfer)) t_posted implies t_voided = false) + (forall ((t Transfer)) t_voided implies t_posted = false) + ) +) +(define-fun TransferStateConsistency_10 () Bool + (and + (forall ((t Transfer)) (and t_pending implies t_posted = false t_voided = false)) + (forall ((t Transfer)) t_posted implies t_voided = false) + (forall ((t Transfer)) t_voided implies t_posted = false) + ) +) +(echo "Checking: Eventually(TransferStateConsistency)") +(check-sat) +(get-model) diff --git a/out/ToggleSwitch.smt2 b/out/ToggleSwitch.smt2 new file mode 100644 index 0000000..e10cdfa --- /dev/null +++ b/out/ToggleSwitch.smt2 @@ -0,0 +1,19 @@ +; SpeckDL: ToggleSwitch — Z3 Verification +; Generated by speckl-compile Z3 backend +; Bounded model checking depth: 10 + +(set-logic ALL) +(set-option :produce-models true) + +; --- State Variables --- +(declare-const isOn Bool) + +; --- Invariants --- +(define-fun SwitchConsistent () Bool + (and + (or (= isOn true) (= isOn false)) + ) +) + +(check-sat) +(get-model) diff --git a/reference-agent/src/smes/verification-sme.ts b/reference-agent/src/smes/verification-sme.ts index f096a25..9cd6b72 100644 --- a/reference-agent/src/smes/verification-sme.ts +++ b/reference-agent/src/smes/verification-sme.ts @@ -30,7 +30,7 @@ export class VerificationSME extends SME { this.compileConstraint(c.expression, speck) ); - // In production, this would invoke Z3 via subprocess or WASM. + // In production, this would invoke Z3 via subprocess. // For the reference implementation, we simulate the result. const z3Result = this.simulateZ3(speck, z3Assertions); diff --git a/reference-agent/src/types.ts b/reference-agent/src/types.ts index 0877789..5b6f524 100644 --- a/reference-agent/src/types.ts +++ b/reference-agent/src/types.ts @@ -99,7 +99,7 @@ export interface Task { export type TaskType = | "verify_speck" // Run Z3 verification on a Speck | "compile_to_dst" // Compile verified Speck to DST - | "compile_to_wasm // Removed: WASM superseded by IR→Rust→wasm-pack path + | "compile_to_typescript" // Compile DST to TypeScript | "generate_code" // Generate code from verified Speck | "generate_docs" // Generate documentation from provenance graph | "integrate" // Integration/glue code @@ -142,7 +142,7 @@ export interface TaskResult { export interface ProvenanceNode { id: string; - type: "speck" | "z3_assertion" | "dst" | "wasm" | "code" | "docs" | "event"; + type: "speck" | "z3_assertion" | "dst" | "code" | "docs" | "event"; label: string; metadata: Record; }