fix(ts,rust): real constraint/verify expressions, dedup fix, implies translation
TS backend: - Constraint checks now emit real forall→every() translation (was 'return true') - Verify: implies(p,q) now (!p || q) (was (p || q) — wrong logic) - Verify: 'in' operator now pre-tokenized to avoid || splitting the regex - memberKey dedup fix: verify/constraint nodes now keyed by expression (was: all verify nodes deduped to 1, all constraints to 1) Rust backend: - Constraint checks: forall→iter().all(), implies()→(!p || q), nil→sentinel - Verify checks: always()/eventually() with decision_log iteration - Same memberKey dedup fix applied All 8 constraints + 6 verify blocks now emit in both TS and Rust. 57/57 tests pass.
This commit is contained in:
Scott Scoble
parent
3ca5a8d21a
commit
37cdc59180
2 changed files with 142 additions and 27 deletions
|
|
@ -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<string, MemberNode>();
|
||||
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;
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -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<string>, mapVarNames: Set<
|
|||
|
||||
// 5a: x in <map>.keys -> <map>.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 <set> -> <set>.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;
|
||||
}
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue