diff --git a/compiler/dist/index.js b/compiler/dist/index.js index 724435a..8b381dd 100644 --- a/compiler/dist/index.js +++ b/compiler/dist/index.js @@ -7,6 +7,7 @@ import { generateCycloneDX } from './generators/cyclonedx.js'; import { generateSPDX } from './generators/spdx.js'; import { generateTypeScriptStateMachine } from './generators/typescript-state-machine.js'; import { 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 +36,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 +64,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 +77,43 @@ 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 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); + } + 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..9bf7dac 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,YAAY,EAAE,MAAM,sBAAsB,CAAC;AACpD,OAAO,EAAE,UAAU,EAAa,yBAAyB,EAAE,mBAAmB,EAAE,MAAM,oBAAoB,CAAC;AAC3G,OAAO,EAAE,MAAM,IAAI,CAAC;AACpB,OAAO,IAAI,MAAM,MAAM,CAAC;AASxB,KAAK,UAAU,IAAI;IACjB,uDAAuD;IACvD,MAAM,WAAW,GAAG,IAAI,CAAC,IAAI,CAAC,IAAI,CAAC,OAAO,CAAC,IAAI,GAAG,CAAC,MAAM,CAAC,IAAI,CAAC,GAAG,CAAC,CAAC,QAAQ,CAAC,EAAE,IAAI,EAAE,eAAe,CAAC,CAAC;IACtG,IAAI,EAAE,CAAC,UAAU,CAAC,WAAW,CAAC,EAAE,CAAC;QAC/B,IAAI,CAAC;YACH,MAAM,EAAE,QAAQ,EAAE,GAAG,MAAM,MAAM,CAAC,eAAe,CAAC,CAAC;YACnD,QAAQ,CAAC,SAAS,WAAW,GAAG,EAAE,EAAE,KAAK,EAAE,SAAS,EAAE,CAAC,CAAC;QAC1D,CAAC;QAAC,MAAM,CAAC;YACP,OAAO,CAAC,KAAK,CAAC,oDAAoD,CAAC,CAAC;YACpE,OAAO,CAAC,IAAI,CAAC,CAAC,CAAC,CAAC;QAClB,CAAC;IACH,CAAC;IAED,MAAM,IAAI,GAAG,MAAM,KAAK,CAAC,OAAO,CAAC,OAAO,CAAC,IAAI,CAAC,CAAC;SAC5C,OAAO,CAAC,WAAW,EAAE,iCAAiC,EAAE,CAAC,QAAQ,EAAE,EAAE;QACpE,OAAO,QAAQ;aACZ,UAAU,CAAC,MAAM,EAAE;YAClB,QAAQ,EAAE,yBAAyB;YACnC,IAAI,EAAE,QAAQ;YACd,YAAY,EAAE,IAAI;SACnB,CAAC;aACD,MAAM,CAAC,YAAY,EAAE;YACpB,KAAK,EAAE,GAAG;YACV,QAAQ,EAAE,yCAAyC;YACnD,IAAI,EAAE,QAAQ;YACd,OAAO,EAAE,OAAO;SACjB,CAAC;aACD,MAAM,CAAC,QAAQ,EAAE;YAChB,KAAK,EAAE,GAAG;YACV,QAAQ,EAAE,oBAAoB;YAC9B,IAAI,EAAE,QAAQ;YACd,OAAO,EAAE,CAAC,YAAY,EAAE,IAAI,EAAE,KAAK,CAAC;YACpC,OAAO,EAAE,YAAqB;SAC/B,CAAC;aACD,MAAM,CAAC,cAAc,EAAE;YACtB,KAAK,EAAE,GAAG;YACV,QAAQ,EAAE,kDAAkD;YAC5D,IAAI,EAAE,QAAQ;YACd,OAAO,EAAE,EAAE;SACZ,CAAC;aACD,MAAM,CAAC,YAAY,EAAE;YACpB,KAAK,EAAE,GAAG;YACV,QAAQ,EAAE,mBAAmB;YAC7B,IAAI,EAAE,QAAQ;YACd,OAAO,EAAE,CAAC,KAAK,EAAE,MAAM,EAAE,MAAM,CAAC;YAChC,OAAO,EAAE,MAAe;SACzB,CAAC,CAAC;IACP,CAAC,CAAC;SACD,IAAI,EAAE;SACN,IAAI,CAAC;IAER,MAAM,IAAI,GAAG,IAAI,CAAC,IAAc,CAAC;IACjC,MAAM,OAAO,GAAG;QACd,SAAS,EAAE,IAAI,CAAC,SAAmB;QACnC,SAAS,EAAE,IAAI,CAAC,SAAoC;QACpD,MAAM,EAAE,IAAI,CAAC,MAAqC;QAClD,WAAW,EAAE,IAAI,CAAC,WAAqB;KACxC,CAAC;IAEF,OAAO,CAAC,GAAG,CAAC,aAAa,IAAI,KAAK,CAAC,CAAC;IAEpC,uBAAuB;IACvB,MAAM,GAAG,GAAG,cAAc,CAAC,IAAI,CAAC,CAAC;IAEjC,MAAM,UAAU,GAAG,GAAG,CAAC,MAAM,CAAC,MAAM,CAAC;IACrC,MAAM,WAAW,GAAG,GAAG,CAAC,MAAM,CAAC,MAAM,CAAC,CAAC,GAAG,EAAE,CAAC,EAAE,EAAE,CAAC,GAAG,GAAG,CAAC,CAAC,OAAO,CAAC,MAAM,EAAE,CAAC,CAAC,CAAC;IAC7E,OAAO,CAAC,GAAG,CAAC,4BAA4B,UAAU,cAAc,WAAW,YAAY,CAAC,CAAC;IAEzF,iCAAiC;IACjC,IAAI,CAAC,EAAE,CAAC,UAAU,CAAC,OAAO,CAAC,SAAS,CAAC,EAAE,CAAC;QACtC,EAAE,CAAC,SAAS,CAAC,OAAO,CAAC,SAAS,EAAE,EAAE,SAAS,EAAE,IAAI,EAAE,CAAC,CAAC;IACvD,CAAC;IAED,oFAAoF;IACpF,MAAM,SAAS,GAAG,EAAE,CAAC,YAAY,CAAC,IAAI,EAAE,OAAO,CAAC,CAAC;IAEjD,mEAAmE;IACnE,IAAI,OAAO,CAAC,MAAM,KAAK,IAAI,EAAE,CAAC;QAC5B,OAAO,CAAC,GAAG,CAAC,mDAAmD,CAAC,CAAC;QACjE,uBAAuB,CAAC,GAAG,EAAE,OAAO,CAAC,SAAS,CAAC,CAAC;IAClD,CAAC;IAED,8CAA8C;IAC9C,IAAI,OAAO,CAAC,MAAM,KAAK,IAAI,IAAI,OAAO,CAAC,MAAM,KAAK,KAAK,EAAE,CAAC;QACxD,OAAO,CAAC,GAAG,CAAC,6BAA6B,CAAC,CAAC;QAC3C,kDAAkD;QAClD,KAAK,MAAM,KAAK,IAAI,GAAG,CAAC,MAAM,EAAE,CAAC;YAC/B,MAAM,UAAU,GAAG,yBAAyB,CAAC,SAAS,EAAE,KAAK,CAAC,IAAI,CAAC,CAAC;YACpE,MAAM,QAAQ,GAAG,mBAAmB,CAAC,SAAS,EAAE,KAAK,CAAC,IAAI,CAAC,CAAC;YAC5D,kDAAkD;YACjD,KAAa,CAAC,WAAW,GAAG,UAAU,CAAC;YACvC,KAAa,CAAC,KAAK,GAAG,QAAQ,CAAC;QAClC,CAAC;QACD,MAAM,SAAS,GAAc,EAAE,WAAW,EAAE,OAAO,CAAC,WAAW,EAAE,CAAC;QAClE,UAAU,CAAC,GAAG,EAAE,OAAO,CAAC,SAAS,EAAE,SAAS,CAAC,CAAC;IAChD,CAAC;IAED,mDAAmD;IACnD,IAAI,OAAO,CAAC,MAAM,KAAK,IAAI,EAAE,CAAC;QAC5B,OAAO,CAAC,GAAG,CAAC,0CAA0C,CAAC,CAAC;QACxD,8BAA8B,CAAC,GAAG,EAAE,OAAO,CAAC,SAAS,CAAC,CAAC;QAEvD,8BAA8B;QAC9B,OAAO,CAAC,GAAG,CAAC,mCAAmC,CAAC,CAAC;QACjD,YAAY,CAAC,GAAG,EAAE,OAAO,CAAC,SAAS,CAAC,CAAC;QAErC,yCAAyC;QACzC,IAAI,OAAO,CAAC,SAAS,KAAK,KAAK,IAAI,OAAO,CAAC,SAAS,KAAK,MAAM,EAAE,CAAC;YAChE,OAAO,CAAC,GAAG,CAAC,+BAA+B,CAAC,CAAC;YAC7C,iBAAiB,CAAC,GAAG,EAAE,OAAO,CAAC,SAAS,CAAC,CAAC;QAC5C,CAAC;QAED,IAAI,OAAO,CAAC,SAAS,KAAK,MAAM,IAAI,OAAO,CAAC,SAAS,KAAK,MAAM,EAAE,CAAC;YACjE,OAAO,CAAC,GAAG,CAAC,0BAA0B,CAAC,CAAC;YACxC,YAAY,CAAC,GAAG,EAAE,OAAO,CAAC,SAAS,CAAC,CAAC;QACvC,CAAC;IACH,CAAC;IAED,OAAO,CAAC,GAAG,CAAC,mCAAmC,OAAO,CAAC,SAAS,GAAG,CAAC,CAAC;AACvE,CAAC;AAED,IAAI,EAAE,CAAC,KAAK,CAAC,CAAC,GAAG,EAAE,EAAE;IACnB,OAAO,CAAC,KAAK,CAAC,qBAAqB,EAAE,GAAG,CAAC,CAAC;IAC1C,OAAO,CAAC,IAAI,CAAC,CAAC,CAAC,CAAC;AAClB,CAAC,CAAC,CAAC"} \ 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..1743f3c 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":49.959937000000025,"failed":false}],[":__tests__/e2e-wasm.test.ts",{"duration":90.40252399999997,"failed":false}],[":src/__tests__/compiler.test.ts",{"duration":11.602408000000025,"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..19bde51 --- /dev/null +++ b/compiler/src/generators/z3.ts @@ -0,0 +1,1034 @@ +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 + if (actions.length > 0 || (nextNode && nextNode.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, return clean sort name + const clean = t.name.startsWith('ident:') ? t.name.substring(6) : t.name; + 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 { + // Strip ident: prefix from sort names + const cleanName = name.startsWith('ident:') ? name.substring(6) : name; + + 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 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__'); + + // 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'); + + for (const rawLine of lines) { + const line = rawLine.trim(); + if (!line || line.startsWith('//')) continue; + + // forall var in domain: expr + 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(), + }); + 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 => s.trim()).filter(Boolean); + const domains = complexForallMatch[2].split(',').map(s => s.trim()).filter(Boolean); + if (vars.length > 1 || domains.length > 1) { + statements.push({ + type: 'forall_complex', + vars, + domains, + expr: complexForallMatch[3].trim(), + }); + continue; + } + // Fall through to simple forall + } + + // Simple require-style expression + statements.push({ type: 'require', expr: line }); + } + + 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 87244a8..e61be9c 100644 --- a/compiler/src/index.ts +++ b/compiler/src/index.ts @@ -8,12 +8,15 @@ 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, 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 +46,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 +74,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,27 +92,49 @@ 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 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); + // 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 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); + } + + 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..3d92765 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:28:00.665Z" } }, "rdfs:label": "RetryHandler", diff --git a/compiler/test-output/RetryHandler.specbom.cdx.json b/compiler/test-output/RetryHandler.specbom.cdx.json index a691b56..4e90d17 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:28:00.667Z" }, { "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:28:00.667Z" }, { "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:28:00.667Z" } ] } \ 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..95c4171 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:28:00.668Z", "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:28:00.669Z", "comment": "Review type: manual" } ] diff --git a/out/KafkaKRaft.prov.jsonld b/out/KafkaKRaft.prov.jsonld index f1e2b06..41f0ab8 100644 --- a/out/KafkaKRaft.prov.jsonld +++ b/out/KafkaKRaft.prov.jsonld @@ -12,7 +12,7 @@ "@type": "prov:Generation", "prov:activity": { "@type": "prov:Activity", - "prov:startTime": "2026-05-10T05:19:29.457Z" + "prov:startTime": "2026-05-10T05:28:26.203Z" } }, "rdfs:label": "KafkaKRaft", diff --git a/out/KafkaKRaft.smt2 b/out/KafkaKRaft.smt2 new file mode 100644 index 0000000..508d0c8 --- /dev/null +++ b/out/KafkaKRaft.smt2 @@ -0,0 +1,120 @@ +; 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 + true + ) +) +(define-fun LeaderCompleteness () Bool + (and + true + ) +) +(define-fun LogMatching () Bool + (and + true + ) +) +(define-fun LeaderAppendOnly () Bool + (and + true + ) +) +(define-fun TermMonotonicity () Bool + (and + currentTerm' >= currentTerm + ) +) +(define-fun CommitSafety () Bool + (and + true + ) +) + +; --- Action Transition Predicates --- +(define-fun RequestVoteEnabled () Bool + (and + state = Candidate + currentTerm >= lastLogTerm + ) +) +(define-fun RequestVoteStep () Bool + (and + (= votesGranted_post (store votesGranted candidate true)) + ) +) +(define-fun HandleRequestVoteRequestEnabled () Bool + (and + currentTerm >= candidateTerm + ) +) +(define-fun HandleRequestVoteRequestStep () Bool + (and + (= votedFor_post Some(candidate)) + ) +) +(define-fun BecomeLeaderEnabled () Bool + (and + state = Candidate + votesGranted.size() >= 3 + ) +) +(define-fun BecomeLeaderStep () Bool + (and + (= state_post Leader) + (= commitIndex_post length(log)) + ) +) +(define-fun AppendEntriesEnabled () Bool + (and + state = Leader + ) +) +(define-fun AppendEntriesStep () Bool + (and + (= log_post append(log, newEntry)) + ) +) +; Next transition relation: RequestVote | HandleRequestVoteRequest | BecomeLeader | AppendEntries +(define-fun Next () Bool + (or + (and (RequestVoteEnabled) (RequestVoteStep)) + (and (HandleRequestVoteRequestEnabled) (HandleRequestVoteRequestStep)) + (and (BecomeLeaderEnabled) (BecomeLeaderStep)) + (and (AppendEntriesEnabled) (AppendEntriesStep)) + ; Stuttering step + (and + (= currentTerm_post currentTerm) + (= state_post state) + (= votedFor_post votedFor) + (= log_post log) + (= commitIndex_post commitIndex) + (= nextIndex_post nextIndex) + (= matchIndex_post matchIndex) + (= votesGranted_post votesGranted) + ) + ) +) + +(check-sat) +(get-model) diff --git a/out/KafkaKRaft.specbom.cdx.json b/out/KafkaKRaft.specbom.cdx.json index d64e55e..4c0cd54 100644 --- a/out/KafkaKRaft.specbom.cdx.json +++ b/out/KafkaKRaft.specbom.cdx.json @@ -24,7 +24,7 @@ "author": { "name": "Speckl Compiler v0.3" }, - "timestamp": "2026-05-10T05:19:29.464Z" + "timestamp": "2026-05-10T05:28:26.209Z" }, { "subject": "speck:KafkaKRaft", @@ -39,7 +39,7 @@ "name": "Speckl Compiler", "email": "compiler@speckl.scoble.me" }, - "timestamp": "2026-05-10T05:19:29.464Z" + "timestamp": "2026-05-10T05:28:26.209Z" }, { "subject": "speck:KafkaKRaft", @@ -54,7 +54,7 @@ "name": "Speckl Compiler", "email": "compiler@speckl.scoble.me" }, - "timestamp": "2026-05-10T05:19:29.464Z" + "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 index 90ff567..01ffa09 100644 --- a/out/KafkaKRaft.specbom.spdx.json +++ b/out/KafkaKRaft.specbom.spdx.json @@ -13,7 +13,7 @@ "spdxVersion": "3.0.1", "dataLicense": "CC0-1.0", "creationInfo": { - "created": "2026-05-10T05:19:29.464Z", + "created": "2026-05-10T05:28:26.210Z", "createdBy": [ "Organization: Speckl", "tool: speckl-compile-0.2.0" @@ -27,7 +27,7 @@ "@type": "spdx:Tool", "name": "speckl-compile" }, - "timestamp": "2026-05-10T05:19:29.464Z", + "timestamp": "2026-05-10T05:28:26.210Z", "comment": "Review type: hybrid" } ] diff --git a/out/TigerBeetleLedger.smt2 b/out/TigerBeetleLedger.smt2 new file mode 100644 index 0000000..274cb9c --- /dev/null +++ b/out/TigerBeetleLedger.smt2 @@ -0,0 +1,3456 @@ +; 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 (select accounts.values: a) + (- a.balance = a.credits_posted a.debits_posted) + forall (select accounts.values: a) + a.debits_pending >= 0 + a.credits_pending >= 0 + ) +) +(define-fun TransferStateConsistency () Bool + (and + forall (select transfers.values: t) + t.pending implies t.posted = false && t.voided = false + forall (select transfers.values: t) + t.posted implies t.voided = false + forall (select transfers.values: t) + t.voided implies t.posted = false + ) +) +(define-fun NoOverdraft () Bool + (and + forall (select accounts.values: a) + (or a.balance >= 0 a.flags.allows_overdraft) + ) +) + +; --- Action Transition Predicates --- +(define-fun CreateTransferEnabled () Bool + (and + (not (select transfers t.id)) + (select accounts.keys t.from) + (select accounts.keys t.to) + t.from distinct t.to + (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 + (not (select transfers t.id)) + (select accounts.keys t.from) + (select accounts.keys t.to) + t.from distinct t.to + (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 + (not (select transfers_0 t.id)) + (select accounts_0.keys t.from) + (select accounts_0.keys t.to) + t.from distinct t.to + (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_0.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_0.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 + (not (select transfers_0 t.id)) + (select accounts_0.keys t.from) + (select accounts_0.keys t.to) + t.from distinct t.to + (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_0.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 + (not (select transfers_1 t.id)) + (select accounts_1.keys t.from) + (select accounts_1.keys t.to) + t.from distinct t.to + (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_1.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_1.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 + (not (select transfers_1 t.id)) + (select accounts_1.keys t.from) + (select accounts_1.keys t.to) + t.from distinct t.to + (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_1.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 + (not (select transfers_2 t.id)) + (select accounts_2.keys t.from) + (select accounts_2.keys t.to) + t.from distinct t.to + (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_2.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_2.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 + (not (select transfers_2 t.id)) + (select accounts_2.keys t.from) + (select accounts_2.keys t.to) + t.from distinct t.to + (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_2.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 + (not (select transfers_3 t.id)) + (select accounts_3.keys t.from) + (select accounts_3.keys t.to) + t.from distinct t.to + (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_3.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_3.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 + (not (select transfers_3 t.id)) + (select accounts_3.keys t.from) + (select accounts_3.keys t.to) + t.from distinct t.to + (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_3.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 + (not (select transfers_4 t.id)) + (select accounts_4.keys t.from) + (select accounts_4.keys t.to) + t.from distinct t.to + (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_4.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_4.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 + (not (select transfers_4 t.id)) + (select accounts_4.keys t.from) + (select accounts_4.keys t.to) + t.from distinct t.to + (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_4.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 + (not (select transfers_5 t.id)) + (select accounts_5.keys t.from) + (select accounts_5.keys t.to) + t.from distinct t.to + (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_5.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_5.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 + (not (select transfers_5 t.id)) + (select accounts_5.keys t.from) + (select accounts_5.keys t.to) + t.from distinct t.to + (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_5.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 + (not (select transfers_6 t.id)) + (select accounts_6.keys t.from) + (select accounts_6.keys t.to) + t.from distinct t.to + (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_6.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_6.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 + (not (select transfers_6 t.id)) + (select accounts_6.keys t.from) + (select accounts_6.keys t.to) + t.from distinct t.to + (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_6.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 + (not (select transfers_7 t.id)) + (select accounts_7.keys t.from) + (select accounts_7.keys t.to) + t.from distinct t.to + (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_7.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_7.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 + (not (select transfers_7 t.id)) + (select accounts_7.keys t.from) + (select accounts_7.keys t.to) + t.from distinct t.to + (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_7.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 + (not (select transfers_8 t.id)) + (select accounts_8.keys t.from) + (select accounts_8.keys t.to) + t.from distinct t.to + (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_8.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_8.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 + (not (select transfers_8 t.id)) + (select accounts_8.keys t.from) + (select accounts_8.keys t.to) + t.from distinct t.to + (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_8.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 + (not (select transfers_9 t.id)) + (select accounts_9.keys t.from) + (select accounts_9.keys t.to) + t.from distinct t.to + (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_9.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_9.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 + (not (select transfers_9 t.id)) + (select accounts_9.keys t.from) + (select accounts_9.keys t.to) + t.from distinct t.to + (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_9.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 (select accounts_0.values: a) + (- a.balance = a.credits_posted a.debits_posted) + forall (select accounts_0.values: a) + a.debits_pending >= 0 + a.credits_pending >= 0 + ) +) +(define-fun AccountBalanceInvariant_1 () Bool + (and + forall (select accounts_1.values: a) + (- a.balance = a.credits_posted a.debits_posted) + forall (select accounts_1.values: a) + a.debits_pending >= 0 + a.credits_pending >= 0 + ) +) +(define-fun AccountBalanceInvariant_2 () Bool + (and + forall (select accounts_2.values: a) + (- a.balance = a.credits_posted a.debits_posted) + forall (select accounts_2.values: a) + a.debits_pending >= 0 + a.credits_pending >= 0 + ) +) +(define-fun AccountBalanceInvariant_3 () Bool + (and + forall (select accounts_3.values: a) + (- a.balance = a.credits_posted a.debits_posted) + forall (select accounts_3.values: a) + a.debits_pending >= 0 + a.credits_pending >= 0 + ) +) +(define-fun AccountBalanceInvariant_4 () Bool + (and + forall (select accounts_4.values: a) + (- a.balance = a.credits_posted a.debits_posted) + forall (select accounts_4.values: a) + a.debits_pending >= 0 + a.credits_pending >= 0 + ) +) +(define-fun AccountBalanceInvariant_5 () Bool + (and + forall (select accounts_5.values: a) + (- a.balance = a.credits_posted a.debits_posted) + forall (select accounts_5.values: a) + a.debits_pending >= 0 + a.credits_pending >= 0 + ) +) +(define-fun AccountBalanceInvariant_6 () Bool + (and + forall (select accounts_6.values: a) + (- a.balance = a.credits_posted a.debits_posted) + forall (select accounts_6.values: a) + a.debits_pending >= 0 + a.credits_pending >= 0 + ) +) +(define-fun AccountBalanceInvariant_7 () Bool + (and + forall (select accounts_7.values: a) + (- a.balance = a.credits_posted a.debits_posted) + forall (select accounts_7.values: a) + a.debits_pending >= 0 + a.credits_pending >= 0 + ) +) +(define-fun AccountBalanceInvariant_8 () Bool + (and + forall (select accounts_8.values: a) + (- a.balance = a.credits_posted a.debits_posted) + forall (select accounts_8.values: a) + a.debits_pending >= 0 + a.credits_pending >= 0 + ) +) +(define-fun AccountBalanceInvariant_9 () Bool + (and + forall (select accounts_9.values: a) + (- a.balance = a.credits_posted a.debits_posted) + forall (select accounts_9.values: a) + a.debits_pending >= 0 + a.credits_pending >= 0 + ) +) +(define-fun AccountBalanceInvariant_10 () Bool + (and + forall (select accounts_10.values: a) + (- a.balance = a.credits_posted a.debits_posted) + forall (select accounts_10.values: a) + 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 + (not (select transfers_0 t.id)) + (select accounts_0.keys t.from) + (select accounts_0.keys t.to) + t.from distinct t.to + (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_0.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_0.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 + (not (select transfers_0 t.id)) + (select accounts_0.keys t.from) + (select accounts_0.keys t.to) + t.from distinct t.to + (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_0.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 + (not (select transfers_1 t.id)) + (select accounts_1.keys t.from) + (select accounts_1.keys t.to) + t.from distinct t.to + (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_1.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_1.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 + (not (select transfers_1 t.id)) + (select accounts_1.keys t.from) + (select accounts_1.keys t.to) + t.from distinct t.to + (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_1.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 + (not (select transfers_2 t.id)) + (select accounts_2.keys t.from) + (select accounts_2.keys t.to) + t.from distinct t.to + (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_2.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_2.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 + (not (select transfers_2 t.id)) + (select accounts_2.keys t.from) + (select accounts_2.keys t.to) + t.from distinct t.to + (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_2.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 + (not (select transfers_3 t.id)) + (select accounts_3.keys t.from) + (select accounts_3.keys t.to) + t.from distinct t.to + (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_3.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_3.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 + (not (select transfers_3 t.id)) + (select accounts_3.keys t.from) + (select accounts_3.keys t.to) + t.from distinct t.to + (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_3.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 + (not (select transfers_4 t.id)) + (select accounts_4.keys t.from) + (select accounts_4.keys t.to) + t.from distinct t.to + (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_4.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_4.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 + (not (select transfers_4 t.id)) + (select accounts_4.keys t.from) + (select accounts_4.keys t.to) + t.from distinct t.to + (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_4.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 + (not (select transfers_5 t.id)) + (select accounts_5.keys t.from) + (select accounts_5.keys t.to) + t.from distinct t.to + (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_5.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_5.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 + (not (select transfers_5 t.id)) + (select accounts_5.keys t.from) + (select accounts_5.keys t.to) + t.from distinct t.to + (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_5.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 + (not (select transfers_6 t.id)) + (select accounts_6.keys t.from) + (select accounts_6.keys t.to) + t.from distinct t.to + (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_6.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_6.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 + (not (select transfers_6 t.id)) + (select accounts_6.keys t.from) + (select accounts_6.keys t.to) + t.from distinct t.to + (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_6.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 + (not (select transfers_7 t.id)) + (select accounts_7.keys t.from) + (select accounts_7.keys t.to) + t.from distinct t.to + (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_7.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_7.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 + (not (select transfers_7 t.id)) + (select accounts_7.keys t.from) + (select accounts_7.keys t.to) + t.from distinct t.to + (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_7.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 + (not (select transfers_8 t.id)) + (select accounts_8.keys t.from) + (select accounts_8.keys t.to) + t.from distinct t.to + (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_8.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_8.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 + (not (select transfers_8 t.id)) + (select accounts_8.keys t.from) + (select accounts_8.keys t.to) + t.from distinct t.to + (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_8.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 + (not (select transfers_9 t.id)) + (select accounts_9.keys t.from) + (select accounts_9.keys t.to) + t.from distinct t.to + (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_9.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_9.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 + (not (select transfers_9 t.id)) + (select accounts_9.keys t.from) + (select accounts_9.keys t.to) + t.from distinct t.to + (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_9.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 (select accounts_0.values: a) + (or a.balance >= 0 a.flags.allows_overdraft) + ) +) +(define-fun NoOverdraft_1 () Bool + (and + forall (select accounts_1.values: a) + (or a.balance >= 0 a.flags.allows_overdraft) + ) +) +(define-fun NoOverdraft_2 () Bool + (and + forall (select accounts_2.values: a) + (or a.balance >= 0 a.flags.allows_overdraft) + ) +) +(define-fun NoOverdraft_3 () Bool + (and + forall (select accounts_3.values: a) + (or a.balance >= 0 a.flags.allows_overdraft) + ) +) +(define-fun NoOverdraft_4 () Bool + (and + forall (select accounts_4.values: a) + (or a.balance >= 0 a.flags.allows_overdraft) + ) +) +(define-fun NoOverdraft_5 () Bool + (and + forall (select accounts_5.values: a) + (or a.balance >= 0 a.flags.allows_overdraft) + ) +) +(define-fun NoOverdraft_6 () Bool + (and + forall (select accounts_6.values: a) + (or a.balance >= 0 a.flags.allows_overdraft) + ) +) +(define-fun NoOverdraft_7 () Bool + (and + forall (select accounts_7.values: a) + (or a.balance >= 0 a.flags.allows_overdraft) + ) +) +(define-fun NoOverdraft_8 () Bool + (and + forall (select accounts_8.values: a) + (or a.balance >= 0 a.flags.allows_overdraft) + ) +) +(define-fun NoOverdraft_9 () Bool + (and + forall (select accounts_9.values: a) + (or a.balance >= 0 a.flags.allows_overdraft) + ) +) +(define-fun NoOverdraft_10 () Bool + (and + forall (select accounts_10.values: a) + (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 + (not (select transfers_0 t.id)) + (select accounts_0.keys t.from) + (select accounts_0.keys t.to) + t.from distinct t.to + (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_0.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_0.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 + (not (select transfers_0 t.id)) + (select accounts_0.keys t.from) + (select accounts_0.keys t.to) + t.from distinct t.to + (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_0.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 + (not (select transfers_1 t.id)) + (select accounts_1.keys t.from) + (select accounts_1.keys t.to) + t.from distinct t.to + (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_1.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_1.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 + (not (select transfers_1 t.id)) + (select accounts_1.keys t.from) + (select accounts_1.keys t.to) + t.from distinct t.to + (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_1.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 + (not (select transfers_2 t.id)) + (select accounts_2.keys t.from) + (select accounts_2.keys t.to) + t.from distinct t.to + (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_2.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_2.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 + (not (select transfers_2 t.id)) + (select accounts_2.keys t.from) + (select accounts_2.keys t.to) + t.from distinct t.to + (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_2.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 + (not (select transfers_3 t.id)) + (select accounts_3.keys t.from) + (select accounts_3.keys t.to) + t.from distinct t.to + (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_3.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_3.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 + (not (select transfers_3 t.id)) + (select accounts_3.keys t.from) + (select accounts_3.keys t.to) + t.from distinct t.to + (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_3.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 + (not (select transfers_4 t.id)) + (select accounts_4.keys t.from) + (select accounts_4.keys t.to) + t.from distinct t.to + (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_4.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_4.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 + (not (select transfers_4 t.id)) + (select accounts_4.keys t.from) + (select accounts_4.keys t.to) + t.from distinct t.to + (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_4.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 + (not (select transfers_5 t.id)) + (select accounts_5.keys t.from) + (select accounts_5.keys t.to) + t.from distinct t.to + (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_5.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_5.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 + (not (select transfers_5 t.id)) + (select accounts_5.keys t.from) + (select accounts_5.keys t.to) + t.from distinct t.to + (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_5.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 + (not (select transfers_6 t.id)) + (select accounts_6.keys t.from) + (select accounts_6.keys t.to) + t.from distinct t.to + (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_6.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_6.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 + (not (select transfers_6 t.id)) + (select accounts_6.keys t.from) + (select accounts_6.keys t.to) + t.from distinct t.to + (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_6.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 + (not (select transfers_7 t.id)) + (select accounts_7.keys t.from) + (select accounts_7.keys t.to) + t.from distinct t.to + (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_7.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_7.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 + (not (select transfers_7 t.id)) + (select accounts_7.keys t.from) + (select accounts_7.keys t.to) + t.from distinct t.to + (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_7.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 + (not (select transfers_8 t.id)) + (select accounts_8.keys t.from) + (select accounts_8.keys t.to) + t.from distinct t.to + (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_8.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_8.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 + (not (select transfers_8 t.id)) + (select accounts_8.keys t.from) + (select accounts_8.keys t.to) + t.from distinct t.to + (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_8.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 + (not (select transfers_9 t.id)) + (select accounts_9.keys t.from) + (select accounts_9.keys t.to) + t.from distinct t.to + (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_9.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_9.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 + (not (select transfers_9 t.id)) + (select accounts_9.keys t.from) + (select accounts_9.keys t.to) + t.from distinct t.to + (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_9.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 (select transfers_0.values: t) + t.pending_0 implies t.posted = false && t.voided = false + forall (select transfers_0.values: t) + t.posted implies t.voided = false + forall (select transfers_0.values: t) + t.voided implies t.posted = false + ) +) +(define-fun TransferStateConsistency_1 () Bool + (and + forall (select transfers_1.values: t) + t.pending_1 implies t.posted = false && t.voided = false + forall (select transfers_1.values: t) + t.posted implies t.voided = false + forall (select transfers_1.values: t) + t.voided implies t.posted = false + ) +) +(define-fun TransferStateConsistency_2 () Bool + (and + forall (select transfers_2.values: t) + t.pending_2 implies t.posted = false && t.voided = false + forall (select transfers_2.values: t) + t.posted implies t.voided = false + forall (select transfers_2.values: t) + t.voided implies t.posted = false + ) +) +(define-fun TransferStateConsistency_3 () Bool + (and + forall (select transfers_3.values: t) + t.pending_3 implies t.posted = false && t.voided = false + forall (select transfers_3.values: t) + t.posted implies t.voided = false + forall (select transfers_3.values: t) + t.voided implies t.posted = false + ) +) +(define-fun TransferStateConsistency_4 () Bool + (and + forall (select transfers_4.values: t) + t.pending_4 implies t.posted = false && t.voided = false + forall (select transfers_4.values: t) + t.posted implies t.voided = false + forall (select transfers_4.values: t) + t.voided implies t.posted = false + ) +) +(define-fun TransferStateConsistency_5 () Bool + (and + forall (select transfers_5.values: t) + t.pending_5 implies t.posted = false && t.voided = false + forall (select transfers_5.values: t) + t.posted implies t.voided = false + forall (select transfers_5.values: t) + t.voided implies t.posted = false + ) +) +(define-fun TransferStateConsistency_6 () Bool + (and + forall (select transfers_6.values: t) + t.pending_6 implies t.posted = false && t.voided = false + forall (select transfers_6.values: t) + t.posted implies t.voided = false + forall (select transfers_6.values: t) + t.voided implies t.posted = false + ) +) +(define-fun TransferStateConsistency_7 () Bool + (and + forall (select transfers_7.values: t) + t.pending_7 implies t.posted = false && t.voided = false + forall (select transfers_7.values: t) + t.posted implies t.voided = false + forall (select transfers_7.values: t) + t.voided implies t.posted = false + ) +) +(define-fun TransferStateConsistency_8 () Bool + (and + forall (select transfers_8.values: t) + t.pending_8 implies t.posted = false && t.voided = false + forall (select transfers_8.values: t) + t.posted implies t.voided = false + forall (select transfers_8.values: t) + t.voided implies t.posted = false + ) +) +(define-fun TransferStateConsistency_9 () Bool + (and + forall (select transfers_9.values: t) + t.pending_9 implies t.posted = false && t.voided = false + forall (select transfers_9.values: t) + t.posted implies t.voided = false + forall (select transfers_9.values: t) + t.voided implies t.posted = false + ) +) +(define-fun TransferStateConsistency_10 () Bool + (and + forall (select transfers_10.values: t) + t.pending_10 implies t.posted = false && t.voided = false + forall (select transfers_10.values: t) + t.posted implies t.voided = false + forall (select transfers_10.values: t) + 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..b440717 --- /dev/null +++ b/out/ToggleSwitch.smt2 @@ -0,0 +1,52 @@ +; 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)) + ) +) + +; --- Action Transition Predicates --- +(define-fun TurnOnEnabled () Bool + (and + (not isOn) + ) +) +(define-fun TurnOnStep () Bool + (and + (= isOn_post true) + ) +) +(define-fun TurnOffEnabled () Bool + (and + isOn + ) +) +(define-fun TurnOffStep () Bool + (and + (= isOn_post false) + ) +) +; Next transition relation: TurnOn | TurnOff +(define-fun Next () Bool + (or + (and (TurnOnEnabled) (TurnOnStep)) + (and (TurnOffEnabled) (TurnOffStep)) + ; Stuttering step + (and + (= isOn_post isOn) + ) + ) +) + +(check-sat) +(get-model)