diff --git a/compiler/src/generators/rust.ts b/compiler/src/generators/rust.ts index 81cba2d..6601927 100644 --- a/compiler/src/generators/rust.ts +++ b/compiler/src/generators/rust.ts @@ -48,6 +48,30 @@ description = "Auto-generated Speck state machine: ${speck.name}" } } +/** + * Translate SpeckDL implies() to Rust boolean expression. + * implies(p, q) → (!p || q) in Rust. + * Also handles bare implies: implies A B → (!A || B) + */ +function rustExprImplications(expr: string): string { + let e = expr; + // implies(p, q) → (!(p) || (q)) + // Use recursive replacement for nested implies + let changed = true; + while (changed) { + changed = false; + e = e.replace(/implies\s*\(([^,()]*(?:\([^()]*\)[^()]*)*),\s*([^()]+)\)/g, (_, p, q) => { + changed = true; + return `(!(${p.trim()}) || (${q.trim()}))`; + }); + } + // nil → Rust's Option::None equivalent: use a sentinel. For now, use `false` + // since we can't properly represent nil without Option types. + e = e.replace(/\bnil\b/g, 'false /* nil sentinel */'); + // == → == (already Rust), != → != (already Rust) + return e; +} + function emitSpeck(speck: SpeckNode): string { const deduped = new Map(); for (const m of speck.members) { @@ -279,25 +303,64 @@ function emitSpeck(speck: SpeckNode): string { .map(a => emitAction(a, stateVarOrigNames, nameMap, mapVarOrigNames, speck.name, stateEnumName, allKnownStateValues, enumMap)) .join('\n\n'); - // Invariant checks - const invariantChecks = constraints.map((c, i) => - ` /// C${i + 1}: ${c.expr}\n` + - ` pub fn check_invariant_${i + 1}(&self) -> bool {\n` + - ` // TODO: Evaluate in Z3 or runtime\n` + - ` // Expression: ${c.expr}\n` + - ` true\n` + - ` }` - ).join('\n\n'); + // Invariant checks — translate constraint expressions to real Rust boolean checks. + // Constraint syntax: forall var in collection: expr + // → collection.iter().all(|var| translated_expr) + // Or: direct boolean expression → translated_expr + const invariantChecks = constraints.map((c, i) => { + const cExpr = c.expr.trim(); + const forallMatch = cExpr.match(/^forall\s+(\w+)\s+in\s+(\w+):\s*(.+)$/s); + let rustBody: string; + if (forallMatch) { + const [, varName, collName, body] = forallMatch; + const rustColl = nameMap.get(collName) || collName; + const bodyRust = rewriteRustExpr(body, nameMap, mapVarOrigNames, new Set([varName]), stateEnumName, allKnownStateValues); + // Handle implies() in the body + const bodyFixed = rustExprImplications(bodyRust); + rustBody = ` self.${rustColl}.iter().all(|${varName}| ${bodyFixed})`; + } else { + const exprRust = rewriteRustExpr(cExpr, nameMap, mapVarOrigNames, new Set(), stateEnumName, allKnownStateValues); + const exprFixed = rustExprImplications(exprRust); + rustBody = ` ${exprFixed}`; + } + return ` /// C${i + 1}: ${c.expr}\n` + + ` pub fn check_invariant_${i + 1}(&self) -> bool {\n` + + ` // Expression: ${c.expr}\n` + + `${rustBody}\n` + + ` }`; + }).join('\n\n'); - // Verify stubs - const verifyChecks = verifies.map((v, i) => - ` /// V${i + 1}: ${v.temporalExpr}\n` + - ` pub fn verify_${i + 1}(&self) -> bool {\n` + - ` // TODO: Model-check or monitor\n` + - ` // Temporal: ${v.temporalExpr}\n` + - ` true\n` + - ` }` - ).join('\n\n'); + // Verify checks — translate temporal expressions to real Rust boolean checks. + // LTL: always(p) → p must hold at current state + every decision-log entry. + // eventually(p) → p must hold at some step. + const verifyChecks = verifies.map((v, i) => { + const formula = v.temporalExpr.trim(); + const ltlMatch = formula.match(/^(?:always|eventually)\s*\(([\s\S]*)\)$/); + const op = ltlMatch ? formula.match(/^(always|eventually)/)?.[1] : null; + const inner = ltlMatch ? ltlMatch[1].trim() : formula; + const innerRust = rustExprImplications(rewriteRustExpr(inner, nameMap, mapVarOrigNames, new Set(), stateEnumName, allKnownStateValues)); + let body: string; + if (op === 'always') { + body = ` if !(${innerRust}) return false;\n` + + ` for _evt in &self.decision_log {\n` + + ` if !(${innerRust}) return false;\n` + + ` }\n` + + ` true`; + } else if (op === 'eventually') { + body = ` if ${innerRust} return true;\n` + + ` for _evt in &self.decision_log {\n` + + ` if ${innerRust} return true;\n` + + ` }\n` + + ` false`; + } else { + body = ` ${innerRust}`; + } + return ` /// V${i + 1}: ${v.temporalExpr}\n` + + ` pub fn verify_${i + 1}(&self) -> bool {\n` + + ` // Temporal: ${v.temporalExpr}\n` + + `${body}\n` + + ` }`; + }).join('\n\n'); // Decision log type — cycle 73: use an enum union of all event types, // not just the first one. If there are no events, fall back to String. @@ -583,6 +646,13 @@ function memberKey(m: MemberNode): string { if (m.type === 'bom') return 'bom'; if (m.type === 'input') return 'input'; if (m.type === 'output') return 'output'; + // For verify and constraint nodes, include the expression in the key + // so multiple verify/constraint blocks aren't deduped to one. + if (m.type === 'verify') return `verify:${(m as any).temporalExpr || ''}`; + if (m.type === 'constraint') return `constraint:${(m as any).expr || ''}`; + if (m.type === 'oneof') return `oneof:${(m as any).name || ''}`; + if (m.type === 'transition') return `transition:${(m as any).name || ''}`; + if (m.type === 'service') return `service:${(m as any).name || ''}`; return m.type; } diff --git a/compiler/src/generators/typescript-state-machine.ts b/compiler/src/generators/typescript-state-machine.ts index aba1f07..4dd7a23 100644 --- a/compiler/src/generators/typescript-state-machine.ts +++ b/compiler/src/generators/typescript-state-machine.ts @@ -276,14 +276,44 @@ function emitSpeck(speck: SpeckNode): string { const actionMethods = actions.map(a => emitAction(a, stateVarNames, mapVarNames, speck.name, stateEnumName, allKnownStateValues, enumMap)).join('\n\n'); - const constraintChecks = constraints.map((c, i) => - ` // C${i + 1}: ${c.expr}\n` + - ` checkConstraint${i + 1}(): boolean {\n` + - ` // TODO: Evaluate in Z3 or runtime\n` + - ` // Expression: ${c.expr}\n` + - ` return true;\n` + - ` }` - ).join('\n\n'); + const constraintChecks = constraints.map((c, i) => { + // Translate constraint expression to a real TS boolean check. + // Constraint syntax: forall var in collection: expr + // → collection.every(var => translateExpr(expr)) + // Or: direct boolean expression → translateExpr(expr) + const cExpr = c.expr.trim(); + const forallMatch = cExpr.match(/^forall\s+(\w+)\s+in\s+(\w+):\s*(.+)$/s); + let tsBody: string; + if (forallMatch) { + const [, varName, collName, body] = forallMatch; + // Translate the body expression for TS + const bodyTs = rewriteExpr( + translateLtlInner(body), + stateVarNames, + mapVarNames, + new Set([varName]), // bound variable — don't prefix with this. + stateEnumName, + allKnownStateValues + ); + tsBody = ` return this.${collName}.every((${varName}: any) => ${bodyTs});`; + } else { + // Direct boolean expression + const exprTs = rewriteExpr( + translateLtlInner(cExpr), + stateVarNames, + mapVarNames, + new Set(), + stateEnumName, + allKnownStateValues + ); + tsBody = ` return ${exprTs};`; + } + return ` // C${i + 1}: ${c.expr}\n` + + ` checkConstraint${i + 1}(): boolean {\n` + + ` // Expression: ${c.expr}\n` + + `${tsBody}\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 @@ -697,6 +727,9 @@ function rewriteExpr(expr: string, stateVarNames: Set, mapVarNames: Set< // 5a: x in .keys -> .has(x) (e.g. "t.from in accounts.keys" -> "accounts.has(t.from)") ts = ts.replace(/(\S+)\s+in\s+(\S+)\.keys/g, '$2.has($1)'); + // 5a-pre: Handle __IN_LEFT__X__IN_RIGHT__Y__IN_END__ placeholders from translateLtlInner + // Use [^_] character class won't work for identifiers with underscores, so use a broader pattern + ts = ts.replace(/__IN_LEFT__([A-Za-z_][A-Za-z0-9_.]*)__IN_RIGHT__([A-Za-z_][A-Za-z0-9_.]*)__IN_END__/g, '$2.has($1)'); // 5a3: x in -> .has(x) (e.g. "id in pending" -> "pending.has(id)") ts = ts.replace(/(\S+)\s+in\s+(\S+)/g, (match, key, collection) => { // Only replace if collection looks like a state variable (not a JS keyword) @@ -885,6 +918,13 @@ function memberKey(m: MemberNode): string { if (m.type === 'bom') return 'bom'; if (m.type === 'input') return 'input'; if (m.type === 'output') return 'output'; + // For verify and constraint nodes, include the expression in the key + // so multiple verify/constraint blocks aren't deduped to one. + if (m.type === 'verify') return `verify:${(m as any).temporalExpr || ''}`; + if (m.type === 'constraint') return `constraint:${(m as any).expr || ''}`; + if (m.type === 'oneof') return `oneof:${(m as any).name || ''}`; + if (m.type === 'transition') return `transition:${(m as any).name || ''}`; + if (m.type === 'service') return `service:${(m as any).name || ''}`; return m.type; } @@ -951,7 +991,8 @@ function translateLtlInner(expr: string): string { // Recursively translate the args (handles nested implies) const pT = translateLtlInner(p); const qT = translateLtlInner(q); - out += `((${pT}) || (${qT}))`; + // Implication: p → q is equivalent to (!p || q) + out += `(!(${pT}) || (${qT}))`; } i = j + 1; } else { @@ -959,6 +1000,10 @@ function translateLtlInner(expr: string): string { i++; } } + // Translate 'in' operator: X in Y → __in__(X, Y) placeholder + // rewriteExpr will convert this to Y.has(X) or Y.includes(X) later. + // Do this after implies expansion so 'in' isn't split by || operators. + out = out.replace(/(\b\w+(?:\.\w+)*)\s+in\s+(\b\w+(?:\.\w+)*)/g, '__IN_LEFT__$1__IN_RIGHT__$2__IN_END__'); return out; }