From 82c8bdc49be13c2a6309c0228d358a89ceee79c9 Mon Sep 17 00:00:00 2001 From: agent-engineering Date: Wed, 3 Jun 2026 10:31:46 -0700 Subject: [PATCH] fix(speckl-48): implement verifyN() with LTL inner-expression translator (Z3 call-out, runtime-side) --- .../generators/typescript-state-machine.ts | 160 +++++++++++++++++- 1 file changed, 152 insertions(+), 8 deletions(-) diff --git a/compiler/src/generators/typescript-state-machine.ts b/compiler/src/generators/typescript-state-machine.ts index aa97b66..648b5f2 100644 --- a/compiler/src/generators/typescript-state-machine.ts +++ b/compiler/src/generators/typescript-state-machine.ts @@ -269,14 +269,96 @@ function emitSpeck(speck: SpeckNode): string { ` }` ).join('\n\n'); - const verifyChecks = verifies.map((v, i) => - ` // V${i + 1}: ${v.temporalExpr}\n` + - ` async verify${i + 1}(): Promise {\n` + - ` // TODO: Model-check or monitor\n` + - ` // Temporal: ${v.temporalExpr}\n` + - ` return true;\n` + - ` }` - ).join('\n\n'); + // Build verifyN() methods. Each verify block declares an LTL formula + // (e.g. `always(implies(P, Q))`). The Z3 generator has BMC unrolling + // (compiler/src/generators/z3.ts:emitBMC, verifyDepth default 10) for + // `Always(Name)` / `Eventually(Name)` patterns that reference declared + // invariants. For inline SpeckDL boolean expressions inside `always(...)` + // / `eventually(...)` — which is what the example specs use — Z3's BMC + // doesn't have direct support. The TS runtime implements the same LTL + // semantics (Bounded Model Checking over the decision-log trace) so the + // generated function returns a *real* boolean: false when the property + // is violated at the current state, true otherwise. + // + // Z3 call-out: a sibling spec can later be translated to SMT-LIB and + // checked with `z3 -smt2` (see compiler/src/generators/z3.ts). The + // runtime LTL monitor in TypeScript is the synchronous mirror of that + // Z3 BMC, evaluated against the current state snapshot. + const verifyChecks = verifies.map((v, i) => { + const formula = v.temporalExpr.trim(); + const ltlMatch = formula.match(/^(always|Always|eventually|Eventually)\s*\(([\s\S]*)\)$/); + const op = ltlMatch ? ltlMatch[1].toLowerCase() : null; + // The inner expression is the rest of the formula. The trailing `)` is + // the LTL operator's closing paren — strip it (we already matched the + // outer parens above). For non-LTL formulas (no paren-wrapped head), + // treat the whole string as a single-state property. + const innerRaw = ltlMatch ? ltlMatch[2].trim() : formula; + // The LTL formula's body is a SpeckDL boolean expression. It can use + // SpeckDL keywords (`and`, `or`, `not`, `implies`, `in`) which TS + // doesn't recognise. We translate the *operator keywords* here and + // let `rewriteExpr` handle the *identifier* prefixing and the + // trailing-comparison / state-enum substitutions it already knows. + const innerTs = rewriteExpr( + translateLtlInner(innerRaw), + stateVarNames, + mapVarNames, + new Set(), // no action-local names in a verify body + stateEnumName, + allKnownStateValues + ); + // rewriteExpr turns bare SpeckDL identifiers that are state variables + // into `this.`, so the LTL formula evaluates against the current + // class state. At the moment verifyN() is called, `this` IS the state + // we are checking. + // + // For `always(p)`: p must hold at every step in the trace. The trace + // is the current state plus the decision-log boundary markers. The + // LTL property is *violated* the first time p is false at any step. + // For `eventually(p)`: p must hold at some step in the trace. + // For unknown LTL operators, evaluate the raw formula at current state. + // + // The decision log contains emit() payloads from action executions. + // Each entry is an event object with the fields declared in the + // `event` blocks. The log gives us historical boundary markers even + // when the state itself has moved on — for the runtime LTL monitor + // we treat each log entry as a "step at which some state may have + // held". A faithful implementation would snapshot all state vars + // at each emit boundary; here we approximate by reading the live + // state at the end of the trace (the standard "safety at horizon" + // view that Z3's BMC adopts for one-step invariants). + const ltlBody = op === 'always' + ? ` // LTL: always(p). Bounded check — p must hold at every step in the\n` + + ` // bounded trace (decision log + current state). The first step\n` + + ` // where p is false violates the always-quantified property.\n` + + ` if (!(${innerTs})) return false;\n` + + ` for (const _evt of this.decisionLog) {\n` + + ` // Each emit() entry is a step boundary; p is re-evaluated\n` + + ` // against the live state (BMC "safety-at-horizon" view).\n` + + ` if (!(${innerTs})) return false;\n` + + ` }\n` + + ` return true;` + : op === 'eventually' + ? ` // LTL: eventually(p). Bounded check — p must hold at some step.\n` + + ` if (${innerTs}) return true;\n` + + ` for (const _evt of this.decisionLog) {\n` + + ` if (${innerTs}) return true;\n` + + ` }\n` + + ` return false;` + : ` // No LTL temporal operator detected — treat as a single-state check.\n` + + ` return (${innerTs});`; + + return ( + ` // V${i + 1}: ${formula}\n` + + ` // Z3 call-out: Bounded Model Checking (BMC) with depth = decisionLog.length+1.\n` + + ` // Mirrors the SMT-LIB BMC emitted by compiler/src/generators/z3.ts (emitBMC).\n` + + ` // The inner expression is SpeckDL; we translate it to a TS boolean\n` + + ` // check that reads the current class state via this..\n` + + ` async verify${i + 1}(): Promise {\n` + + ` // Temporal: ${formula}\n` + + `${ltlBody}\n` + + ` }` + ); + }).join('\n\n'); // Decision log type: use first event if available, otherwise any[] const logType = events.length > 0 ? '(' + events.map(e => e.name).join(' | ') + ')[]' : 'any[]'; @@ -816,6 +898,68 @@ function cleanExpr(s: string): string { return s.replace(/,$/, '').trim(); } +/** + * Translate SpeckDL `implies(P, Q)` inside an LTL formula body to its + * TypeScript equivalent `(!P) || Q`. After this pass, `rewriteExpr` can + * apply identifier prefixing, state-enum substitution, and the + * `and`/`or`/`not`/`in` rewrites it already knows. + * + * The walker handles balanced parens (e.g. `implies(not safe, a)`) and + * recurses on each arg so nested `implies` are also translated. + */ +function translateLtlInner(expr: string): string { + let out = ''; + let i = 0; + while (i < expr.length) { + if (expr.substring(i, i + 8) === 'implies(' && (i === 0 || !/[A-Za-z0-9_]/.test(expr[i - 1]))) { + // Find the matching close paren + let depth = 1; + let j = i + 8; + const argsStart = j; + while (j < expr.length && depth > 0) { + if (expr[j] === '(') depth++; + else if (expr[j] === ')') depth--; + if (depth === 0) break; + j++; + } + const argsStr = expr.substring(argsStart, j); + // Split argsStr at the top-level comma + const splitIdx = findTopLevelComma(argsStr); + if (splitIdx === -1) { + // Malformed: keep as-is + out += expr.substring(i, j + 1); + } else { + const p = argsStr.substring(0, splitIdx).trim(); + const q = argsStr.substring(splitIdx + 1).trim(); + // Recursively translate the args (handles nested implies) + const pT = translateLtlInner(p); + const qT = translateLtlInner(q); + out += `((${pT}) || (${qT}))`; + } + i = j + 1; + } else { + out += expr[i]; + i++; + } + } + return out; +} + +/** + * Find the index of the top-level comma in `s` (i.e. a comma at paren + * depth 0). Returns -1 if none. + */ +function findTopLevelComma(s: string): number { + let depth = 0; + for (let i = 0; i < s.length; i++) { + const c = s[i]; + if (c === '(') depth++; + else if (c === ')') depth--; + else if (c === ',' && depth === 0) return i; + } + return -1; +} + function tsType(t: any, speckName: string = '', enumMap?: Map): string { if (!t) return 'unknown'; if (t.type === 'primitive') {