diff --git a/compiler/node_modules/.vite/vitest/results.json b/compiler/node_modules/.vite/vitest/results.json index 691508c..ff41374 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":33.913234999999986,"failed":false}],[":src/__tests__/compiler.test.ts",{"duration":11.873544000000038,"failed":false}]]} \ No newline at end of file +{"version":"2.1.9","results":[[":__tests__/parser.test.ts",{"duration":36.549328,"failed":false}],[":src/__tests__/compiler.test.ts",{"duration":13.904341000000045,"failed":false}]]} \ No newline at end of file diff --git a/compiler/src/generators/z3.ts b/compiler/src/generators/z3.ts index 44e045a..15c80a6 100644 --- a/compiler/src/generators/z3.ts +++ b/compiler/src/generators/z3.ts @@ -84,6 +84,10 @@ function emitZ3(speck: SpeckNode, options: Z3Options): string { lines.push('(set-logic ALL)'); lines.push('(set-option :produce-models true)'); + // Declare Speckl helper functions + // speckl_len: length of Array-simulated sequences + lines.push('(declare-fun speckl_len_Int ( (Array Int Int) ) Int)'); + // Step 1: Declare sorts for record types const recordTypes = collectRecordTypes(stateNode, actions); for (const [name, fields] of recordTypes) { @@ -100,6 +104,17 @@ function emitZ3(speck: SpeckNode, options: Z3Options): string { emitStateVar(lines, v, allTypeRefs); } + // Declare _post state variables for invariants that compare pre/post state + // (e.g. "currentTerm' >= currentTerm" → "currentTerm_post >= currentTerm") + const needsPostVars = invariants.some((inv: InvariantNode) => + inv.statements.some((s: InvariantStatement) => s.type === 'require' && s.expr.includes("'"))); + if (needsPostVars) { + for (const v of stateVars) { + const sort = z3Sort(v.typeExpr); + lines.push(`(declare-const ${v.name}_post ${sort})`); + } + } + // Step 3: Emit invariants as define-fun if (invariants.length > 0) { lines.push(''); @@ -395,11 +410,15 @@ function translateExpr(expr: string, stateVars: StateVar[], suffix: string): str // Handle old() wrapper — spec-level, keep inner e = e.replace(/old\(([^()]*(?:\([^()]*\)[^()]*)*)\)/g, '$1'); + // Handle prime notation for post-state: currentTerm' → currentTerm_post (invariant comparison) + e = e.replace(/\b(\w+)'/g, '$1_post'); + // Handle -> as implication (after field access cleanup to avoid false matches) e = e.replace(/->/g, '=>'); - // Handle implies(x, y) function call pattern - e = e.replace(/implies\s*\(([^,)]+),\s*([^)]+)\)/g, '(=> $1 $2)'); + // Handle function calls: length(expr), min(a,b), etc. + e = e.replace(/\blength\(([^)]+)\)/g, 'len__$1__xx'); // marker, fix later + e = e.replace(/\bmin\(([^,)]+),\s*([^)]+)\)/g, 'min__$1__$2__xx'); // Field access: a.balance → balance (drop qualifier for bound forall vars) // For record fields accessed via dot, translate to Z3-safe names @@ -478,6 +497,19 @@ function translateExpr(expr: string, stateVars: StateVar[], suffix: string): str // Convert infix to prefix e = convertToPrefix(e); + // Fix length marker: len__args__xx → Z3-compatible form + // Use declared speckl_len functions since Z3 arrays don't have built-in length + e = e.replace(/len__([^_]\S*?)__xx/g, (_, args) => { + // Determine sort from context — default to Int array length + return `(speckl_len_Int ${args})`; + }); + e = e.replace(/min__([^_]\S*?)__([^_]\S*?)__xx/g, (_, a, b) => { + return `(ite (<= ${a} ${b}) ${a} ${b})`; + }); + + // Fix i-1 → (- i 1) in SMT-LIB2 (select indices) + e = e.replace(/\b(\w+)-(\d+)\b/g, '(- $1 $2)'); + // Restore operators to SMT-LIB2 e = e.replace(/__EQ__/g, '='); e = e.replace(/__NE__/g, 'distinct'); @@ -487,6 +519,10 @@ function translateExpr(expr: string, stateVars: StateVar[], suffix: string): str // Wrap distinct e = e.replace(/\bdistinct\s+(\S+)\s+(\S+)/g, '(distinct $1 $2)'); + // Fix remaining infix = that escaped convertToPrefix (e.g. inside => bodies) + // Match: word = word or word = number, at any depth + e = e.replace(/(? state = Leader (> currentTerm 0)) + (=> (= Leader $3) (> currentTerm 0)) ) ) (define-fun LeaderCompleteness () Bool (and - commitIndex <= length(log) + commitIndex <= (speckl_len_Int log) ) ) (define-fun LogMatching () Bool (and - (forall ((i Int)) (=> (and (> i 0) (and i <= length(log) (select log i-1).term = (select log i-1).term)) (select log i-1).value = (select log i-1).value)) + (forall ((i Int)) (=> (and (> i 0) (and i <= (speckl_len_Int log) (select log (- i 1)).term = (select log (- i 1)).term)) (select log (- i 1)).value = (select log (- i 1)).value)) ) ) (define-fun LeaderAppendOnly () Bool (and - length(log') >= length(log) + (speckl_len_Int log_post) >= (speckl_len_Int log) ) ) (define-fun TermMonotonicity () Bool (and - currentTerm' >= currentTerm + currentTerm_post >= currentTerm ) ) (define-fun CommitSafety () Bool (and - commitIndex <= length(log) + commitIndex <= (speckl_len_Int log) ) )